%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP194+1 : TPTP v9.3.1. Released v2.0.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:47 PM UTC 2026
% Result : Theorem 1.93s 0.96s
% Output : CNFRefutation 1.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 9
% Syntax : Number of formulae : 670 ( 53 unt; 1 def)
% Number of atoms : 2627 ( 727 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 2583 (1096 ~;1458 |; 21 &)
% ( 2 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 2 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 1100 ( 0 sgn1095 !; 5 ?;1024 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( ( group_member(X2,X0)
& group_member(X1,X0) )
=> group_member(multiply(X0,X1,X2),X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRP007+0.ax',total_function) ).
fof(f2,axiom,
! [X0,X1,X2,X3] :
( ( group_member(X3,X0)
& group_member(X2,X0)
& group_member(X1,X0) )
=> multiply(X0,multiply(X0,X1,X2),X3) = multiply(X0,X1,multiply(X0,X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRP007+0.ax',associativity) ).
fof(f3,axiom,
! [X0] :
( group_member(X0,f)
=> group_member(phi(X0),h) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism1) ).
fof(f4,axiom,
! [X0,X1] :
( ( group_member(X1,f)
& group_member(X0,f) )
=> multiply(h,phi(X0),phi(X1)) = phi(multiply(f,X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',homomorphism2) ).
fof(f5,axiom,
! [X0] :
( group_member(X0,h)
=> ? [X1] :
( phi(X1) = X0
& group_member(X1,f) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',surjective) ).
fof(f6,axiom,
! [X0,X1] :
( left_zero(X0,X1)
<=> ( ! [X2] :
( group_member(X2,X0)
=> multiply(X0,X1,X2) = X1 )
& group_member(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_zero) ).
fof(f7,axiom,
left_zero(f,f_left_zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_zero_for_f) ).
fof(f8,conjecture,
left_zero(h,phi(f_left_zero)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_left_zero_h) ).
fof(f9,negated_conjecture,
~ left_zero(h,phi(f_left_zero)),
inference(negated_conjecture,[status(cth)],[f8]) ).
fof(f10,plain,
~ left_zero(h,phi(f_left_zero)),
inference(flattening,[],[f9]) ).
fof(f11,plain,
! [X0,X1,X2] :
( ~ group_member(X2,X0)
| ~ group_member(X1,X0)
| group_member(multiply(X0,X1,X2),X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f12,plain,
! [X0,X1,X2] :
( ~ group_member(X2,X0)
| ~ group_member(X1,X0)
| group_member(multiply(X0,X1,X2),X0) ),
inference(flattening,[],[f11]) ).
fof(f13,plain,
! [X0,X1,X2,X3] :
( ~ group_member(X3,X0)
| ~ group_member(X2,X0)
| ~ group_member(X1,X0)
| multiply(X0,multiply(X0,X1,X2),X3) = multiply(X0,X1,multiply(X0,X2,X3)) ),
inference(ennf_transformation,[],[f2]) ).
fof(f14,plain,
! [X0,X1,X2,X3] :
( ~ group_member(X3,X0)
| ~ group_member(X2,X0)
| ~ group_member(X1,X0)
| multiply(X0,multiply(X0,X1,X2),X3) = multiply(X0,X1,multiply(X0,X2,X3)) ),
inference(flattening,[],[f13]) ).
fof(f15,plain,
! [X0] :
( ~ group_member(X0,f)
| group_member(phi(X0),h) ),
inference(ennf_transformation,[],[f3]) ).
fof(f16,plain,
! [X0,X1] :
( ~ group_member(X1,f)
| ~ group_member(X0,f)
| multiply(h,phi(X0),phi(X1)) = phi(multiply(f,X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f17,plain,
! [X0,X1] :
( ~ group_member(X1,f)
| ~ group_member(X0,f)
| multiply(h,phi(X0),phi(X1)) = phi(multiply(f,X0,X1)) ),
inference(flattening,[],[f16]) ).
fof(f18,plain,
! [X0] :
( ~ group_member(X0,h)
| ? [X1] :
( phi(X1) = X0
& group_member(X1,f) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f19,plain,
! [X0,X1] :
( left_zero(X0,X1)
<=> ( ! [X2] :
( ~ group_member(X2,X0)
| multiply(X0,X1,X2) = X1 )
& group_member(X1,X0) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f20,plain,
! [X0] :
( ~ group_member(X0,h)
| ( phi(sK0(X0)) = X0
& group_member(sK0(X0),f) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f18]) ).
fof(f21,plain,
! [X0,X1] :
( ( ~ left_zero(X0,X1)
| ( ! [X2] :
( ~ group_member(X2,X0)
| multiply(X0,X1,X2) = X1 )
& group_member(X1,X0) ) )
& ( ? [X2] :
( group_member(X2,X0)
& multiply(X0,X1,X2) != X1 )
| ~ group_member(X1,X0)
| left_zero(X0,X1) ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f22,plain,
! [X0,X1] :
( ( ~ left_zero(X0,X1)
| ( ! [X2] :
( ~ group_member(X2,X0)
| multiply(X0,X1,X2) = X1 )
& group_member(X1,X0) ) )
& ( ? [X2] :
( group_member(X2,X0)
& multiply(X0,X1,X2) != X1 )
| ~ group_member(X1,X0)
| left_zero(X0,X1) ) ),
inference(flattening,[],[f21]) ).
fof(f23,plain,
! [X0,X1] :
( ( ~ left_zero(X0,X1)
| ( ! [X3] :
( ~ group_member(X3,X0)
| multiply(X0,X1,X3) = X1 )
& group_member(X1,X0) ) )
& ( ? [X2] :
( group_member(X2,X0)
& multiply(X0,X1,X2) != X1 )
| ~ group_member(X1,X0)
| left_zero(X0,X1) ) ),
inference(rectify,[],[f22]) ).
fof(f24,plain,
! [X0,X1] :
( ( ~ left_zero(X0,X1)
| ( ! [X3] :
( ~ group_member(X3,X0)
| multiply(X0,X1,X3) = X1 )
& group_member(X1,X0) ) )
& ( ( group_member(sK1(X0,X1),X0)
& multiply(X0,X1,sK1(X0,X1)) != X1 )
| ~ group_member(X1,X0)
| left_zero(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f23]) ).
fof(f25,plain,
! [X2,X0,X1] :
( ~ group_member(X2,X0)
| ~ group_member(X1,X0)
| group_member(multiply(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f12]) ).
fof(f26,plain,
! [X2,X3,X0,X1] :
( ~ group_member(X3,X0)
| ~ group_member(X2,X0)
| ~ group_member(X1,X0)
| multiply(X0,multiply(X0,X1,X2),X3) = multiply(X0,X1,multiply(X0,X2,X3)) ),
inference(cnf_transformation,[],[f14]) ).
fof(f27,plain,
! [X0] :
( ~ group_member(X0,f)
| group_member(phi(X0),h) ),
inference(cnf_transformation,[],[f15]) ).
fof(f28,plain,
! [X0,X1] :
( ~ group_member(X1,f)
| ~ group_member(X0,f)
| multiply(h,phi(X0),phi(X1)) = phi(multiply(f,X0,X1)) ),
inference(cnf_transformation,[],[f17]) ).
fof(f29,plain,
! [X0] :
( ~ group_member(X0,h)
| phi(sK0(X0)) = X0 ),
inference(cnf_transformation,[],[f20]) ).
fof(f30,plain,
! [X0] :
( ~ group_member(X0,h)
| group_member(sK0(X0),f) ),
inference(cnf_transformation,[],[f20]) ).
fof(f31,plain,
! [X3,X0,X1] :
( ~ left_zero(X0,X1)
| ~ group_member(X3,X0)
| multiply(X0,X1,X3) = X1 ),
inference(cnf_transformation,[],[f24]) ).
fof(f32,plain,
! [X0,X1] :
( ~ left_zero(X0,X1)
| group_member(X1,X0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f33,plain,
! [X0,X1] :
( group_member(sK1(X0,X1),X0)
| ~ group_member(X1,X0)
| left_zero(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f34,plain,
! [X0,X1] :
( multiply(X0,X1,sK1(X0,X1)) != X1
| ~ group_member(X1,X0)
| left_zero(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f35,plain,
left_zero(f,f_left_zero),
inference(cnf_transformation,[],[f7]) ).
fof(f36,plain,
~ left_zero(h,phi(f_left_zero)),
inference(cnf_transformation,[],[f10]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i,X2: $i] :
( group_member(multiply(X1,X0,X2),X1)
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X1,multiply(X1,X0,X2),X3) = multiply(X1,X0,multiply(X1,X2,X3)) )
| ~ group_member(X3,X1)
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_51,plain,
! [X0: $i] :
( group_member(phi(X0),h)
| ~ group_member(X0,f) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,phi(X0),phi(X1)) = phi(multiply(f,X0,X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_53,plain,
! [X0: $i] :
( group_member(sK0(X0),f)
| ~ group_member(X0,h) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_54,plain,
! [X0: $i] :
( ( phi(sK0(X0)) = X0 )
| ~ group_member(X0,h) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( left_zero(X0,X1)
| ~ group_member(X1,X0)
| ( multiply(X0,X1,sK1(X0,X1)) != X1 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( left_zero(X1,X0)
| group_member(sK1(X1,X0),X1)
| ~ group_member(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] :
( group_member(X1,X0)
| ~ left_zero(X0,X1) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X1,X2,X0) = X2 )
| ~ left_zero(X1,X2)
| ~ group_member(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_59,plain,
left_zero(f,f_left_zero),
inference(cnf_transformation,[],[f35]) ).
tcf(c_60,negated_conjecture,
~ left_zero(h,phi(f_left_zero)),
inference(cnf_transformation,[],[f36]) ).
tcf(c_276,definition,
iPr_def_10 = phi(f_left_zero),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_277,negated_conjecture,
~ left_zero(h,iPr_def_10),
inference(demodulation,[status(thm)],[c_60,c_276]) ).
tcf(c_485,plain,
group_member(f_left_zero,f),
inference(superposition,[status(thm)],[c_59,c_57]) ).
tcf(c_490,plain,
( group_member(iPr_def_10,h)
| ~ group_member(f_left_zero,f) ),
inference(superposition,[status(thm)],[c_276,c_51]) ).
tcf(c_491,plain,
group_member(iPr_def_10,h),
inference(forward_subsumption_resolution,[status(thm)],[c_490,c_485]) ).
tcf(c_502,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,phi(sK0(X0)),phi(X1)) = phi(multiply(f,sK0(X0),X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_503,plain,
! [X0: $i] :
( ( multiply(h,phi(f_left_zero),phi(X0)) = phi(multiply(f,f_left_zero,X0)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_52]) ).
tcf(c_504,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,phi(X0)) = phi(multiply(f,f_left_zero,X0)) )
| ~ group_member(X0,f) ),
inference(light_normalisation,[status(thm)],[c_503,c_276]) ).
tcf(c_516,plain,
! [X0: $i] :
( ( phi(sK0(phi(X0))) = phi(X0) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_54]) ).
tcf(c_517,plain,
phi(sK0(iPr_def_10)) = iPr_def_10,
inference(superposition,[status(thm)],[c_491,c_54]) ).
tcf(c_527,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,phi(sK1(f,X0)),phi(X1)) = phi(multiply(f,sK1(f,X0),X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_52]) ).
tcf(c_528,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( phi(sK0(sK1(h,X0))) = sK1(h,X0) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_54]) ).
tcf(c_544,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,phi(multiply(f,X0,X1)),phi(X2)) = phi(multiply(f,multiply(f,X0,X1),X2)) )
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_52]) ).
tcf(c_545,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(multiply(h,X0,X1))) = multiply(h,X0,X1) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_54]) ).
tcf(c_561,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X1,X3,multiply(X1,X0,X2)) = X3 )
| ~ left_zero(X1,X3)
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(superposition,[status(thm)],[c_49,c_58]) ).
tcf(c_562,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(X0)) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_58]) ).
tcf(c_563,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(X0)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_58]) ).
tcf(c_564,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(X1,X0)
| ( multiply(X1,X2,sK1(X1,X0)) = X2 )
| ~ left_zero(X1,X2)
| ~ group_member(X0,X1) ),
inference(superposition,[status(thm)],[c_56,c_58]) ).
tcf(c_565,plain,
! [X0: $i] :
( ( multiply(f,X0,f_left_zero) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_58]) ).
tcf(c_566,plain,
! [X0: $i] :
( ( multiply(h,X0,iPr_def_10) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_58]) ).
tcf(c_595,plain,
multiply(f,f_left_zero,f_left_zero) = f_left_zero,
inference(superposition,[status(thm)],[c_59,c_565]) ).
tcf(c_605,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(multiply(f,X0,X1)))) = phi(multiply(f,X0,X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_516]) ).
tcf(c_606,plain,
! [X0: $i] :
( ( phi(sK0(phi(sK0(X0)))) = phi(sK0(X0)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_516]) ).
tcf(c_607,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( phi(sK0(phi(sK1(f,X0)))) = phi(sK1(f,X0)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_516]) ).
tcf(c_608,plain,
phi(sK0(phi(f_left_zero))) = phi(f_left_zero),
inference(superposition,[status(thm)],[c_485,c_516]) ).
tcf(c_626,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(sK0(multiply(h,X0,X1))))) = phi(sK0(multiply(h,X0,X1))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_606]) ).
tcf(c_627,plain,
! [X0: $i] :
( ( phi(sK0(phi(sK0(phi(X0))))) = phi(sK0(phi(X0))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_606]) ).
tcf(c_628,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( phi(sK0(phi(sK0(sK1(h,X0))))) = phi(sK0(sK1(h,X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_606]) ).
tcf(c_629,plain,
phi(sK0(phi(sK0(iPr_def_10)))) = phi(sK0(iPr_def_10)),
inference(superposition,[status(thm)],[c_491,c_606]) ).
tcf(c_661,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,iPr_def_10,phi(multiply(f,X0,X1))) = phi(multiply(f,f_left_zero,multiply(f,X0,X1))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_504]) ).
tcf(c_662,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,phi(sK0(X0))) = phi(multiply(f,f_left_zero,sK0(X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_504]) ).
tcf(c_663,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(h,iPr_def_10,phi(sK1(f,X0))) = phi(multiply(f,f_left_zero,sK1(f,X0))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_504]) ).
tcf(c_664,plain,
multiply(h,iPr_def_10,phi(f_left_zero)) = phi(multiply(f,f_left_zero,f_left_zero)),
inference(superposition,[status(thm)],[c_485,c_504]) ).
tcf(c_665,plain,
multiply(h,iPr_def_10,iPr_def_10) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_664,c_276,c_595]) ).
tcf(c_684,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(multiply(f,X0,X1))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_562]) ).
tcf(c_685,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(X0))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_562]) ).
tcf(c_686,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,phi(sK1(f,X0))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_562]) ).
tcf(c_687,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(f_left_zero)) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_562]) ).
tcf(c_709,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(multiply(h,X0,X1))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_563]) ).
tcf(c_710,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(X0))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_563]) ).
tcf(c_711,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,sK0(sK1(h,X0))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_563]) ).
tcf(c_712,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(iPr_def_10)) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_563]) ).
tcf(c_738,plain,
multiply(f,f_left_zero,sK0(iPr_def_10)) = f_left_zero,
inference(superposition,[status(thm)],[c_59,c_712]) ).
tcf(c_766,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X1,multiply(X1,multiply(X1,X0,X2),X3),X4) = multiply(X1,multiply(X1,X0,X2),multiply(X1,X3,X4)) )
| ~ group_member(X4,X1)
| ~ group_member(X3,X1)
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(superposition,[status(thm)],[c_49,c_50]) ).
tcf(c_767,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,multiply(h,phi(X0),X1),X2) = multiply(h,phi(X0),multiply(h,X1,X2)) )
| ~ group_member(X2,h)
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_50]) ).
tcf(c_768,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,multiply(f,sK0(X0),X1),X2) = multiply(f,sK0(X0),multiply(f,X1,X2)) )
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_50]) ).
tcf(c_769,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( left_zero(X1,X0)
| ( multiply(X1,multiply(X1,sK1(X1,X0),X2),X3) = multiply(X1,sK1(X1,X0),multiply(X1,X2,X3)) )
| ~ group_member(X3,X1)
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(superposition,[status(thm)],[c_56,c_50]) ).
tcf(c_770,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,multiply(f,f_left_zero,X0),X1) = multiply(f,f_left_zero,multiply(f,X0,X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_50]) ).
tcf(c_771,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,multiply(h,iPr_def_10,X0),X1) = multiply(h,iPr_def_10,multiply(h,X0,X1)) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_491,c_50]) ).
tcf(c_806,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(sK0(phi(multiply(f,X0,X1)))))) = phi(sK0(phi(multiply(f,X0,X1)))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_627]) ).
tcf(c_807,plain,
! [X0: $i] :
( ( phi(sK0(phi(sK0(phi(sK0(X0)))))) = phi(sK0(phi(sK0(X0)))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_627]) ).
tcf(c_808,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( phi(sK0(phi(sK0(phi(sK1(f,X0)))))) = phi(sK0(phi(sK1(f,X0)))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_627]) ).
tcf(c_809,plain,
phi(sK0(phi(sK0(phi(f_left_zero))))) = phi(sK0(phi(f_left_zero))),
inference(superposition,[status(thm)],[c_485,c_627]) ).
tcf(c_831,plain,
! [X0: $i,X1: $i] :
( left_zero(h,multiply(h,X0,X1))
| ( phi(sK0(sK1(h,multiply(h,X0,X1)))) = sK1(h,multiply(h,X0,X1)) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_528]) ).
tcf(c_832,plain,
! [X0: $i] :
( left_zero(h,phi(X0))
| ( phi(sK0(sK1(h,phi(X0)))) = sK1(h,phi(X0)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_528]) ).
tcf(c_833,plain,
! [X0: $i] :
( left_zero(h,X0)
| left_zero(h,sK1(h,X0))
| ( phi(sK0(sK1(h,sK1(h,X0)))) = sK1(h,sK1(h,X0)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_528]) ).
tcf(c_834,plain,
( left_zero(h,iPr_def_10)
| ( phi(sK0(sK1(h,iPr_def_10))) = sK1(h,iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_491,c_528]) ).
tcf(c_835,plain,
phi(sK0(sK1(h,iPr_def_10))) = sK1(h,iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_834,c_277]) ).
tcf(c_882,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(multiply(h,X0,X1)))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_685]) ).
tcf(c_883,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(phi(X0)))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_685]) ).
tcf(c_884,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,phi(sK0(sK1(h,X0)))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_685]) ).
tcf(c_885,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(iPr_def_10))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_685]) ).
tcf(c_902,plain,
( group_member(sK1(h,iPr_def_10),h)
| ~ group_member(sK0(sK1(h,iPr_def_10)),f) ),
inference(superposition,[status(thm)],[c_835,c_51]) ).
tcf(c_919,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(multiply(f,X0,X1)))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_710]) ).
tcf(c_920,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(sK0(X0)))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_710]) ).
tcf(c_921,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,sK0(phi(sK1(f,X0)))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_710]) ).
tcf(c_922,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(f_left_zero))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_710]) ).
tcf(c_951,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,iPr_def_10,phi(sK0(multiply(h,X0,X1)))) = phi(multiply(f,f_left_zero,sK0(multiply(h,X0,X1)))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_662]) ).
tcf(c_952,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,phi(sK0(phi(X0)))) = phi(multiply(f,f_left_zero,sK0(phi(X0)))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_662]) ).
tcf(c_953,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(h,iPr_def_10,phi(sK0(sK1(h,X0)))) = phi(multiply(f,f_left_zero,sK0(sK1(h,X0)))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_662]) ).
tcf(c_954,plain,
multiply(h,iPr_def_10,phi(sK0(iPr_def_10))) = phi(multiply(f,f_left_zero,sK0(iPr_def_10))),
inference(superposition,[status(thm)],[c_491,c_662]) ).
tcf(c_972,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(sK0(phi(sK0(multiply(h,X0,X1))))))) = phi(sK0(phi(sK0(multiply(h,X0,X1))))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_807]) ).
tcf(c_973,plain,
! [X0: $i] :
( ( phi(sK0(phi(sK0(phi(sK0(phi(X0))))))) = phi(sK0(phi(sK0(phi(X0))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_807]) ).
tcf(c_974,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( phi(sK0(phi(sK0(phi(sK0(sK1(h,X0))))))) = phi(sK0(phi(sK0(sK1(h,X0))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_807]) ).
tcf(c_975,plain,
phi(sK0(phi(sK0(phi(sK0(iPr_def_10)))))) = phi(sK0(phi(sK0(iPr_def_10)))),
inference(superposition,[status(thm)],[c_491,c_807]) ).
tcf(c_1000,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(phi(multiply(f,X0,X1))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_883]) ).
tcf(c_1001,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(phi(sK0(X0))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_883]) ).
tcf(c_1002,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,phi(sK0(phi(sK1(f,X0))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_883]) ).
tcf(c_1003,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(phi(f_left_zero)))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_883]) ).
tcf(c_1054,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(sK0(multiply(h,X0,X1))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_920]) ).
tcf(c_1055,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(sK0(phi(X0))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_920]) ).
tcf(c_1056,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,sK0(phi(sK0(sK1(h,X0))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_920]) ).
tcf(c_1057,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(sK0(iPr_def_10)))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_920]) ).
tcf(c_1079,plain,
! [X0: $i,X1: $i] :
( left_zero(f,multiply(f,X0,X1))
| ( phi(sK0(phi(sK1(f,multiply(f,X0,X1))))) = phi(sK1(f,multiply(f,X0,X1))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_607]) ).
tcf(c_1080,plain,
! [X0: $i] :
( left_zero(f,sK0(X0))
| ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_607]) ).
tcf(c_1081,plain,
! [X0: $i] :
( left_zero(f,X0)
| left_zero(f,sK1(f,X0))
| ( phi(sK0(phi(sK1(f,sK1(f,X0))))) = phi(sK1(f,sK1(f,X0))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_607]) ).
tcf(c_1103,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(phi(sK0(multiply(h,X0,X1)))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1001]) ).
tcf(c_1104,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(phi(sK0(phi(X0)))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1001]) ).
tcf(c_1105,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,phi(sK0(phi(sK0(sK1(h,X0)))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1001]) ).
tcf(c_1106,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(phi(sK0(iPr_def_10))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_1001]) ).
tcf(c_1142,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(sK0(phi(multiply(f,X0,X1)))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1055]) ).
tcf(c_1143,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(sK0(phi(sK0(X0)))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1055]) ).
tcf(c_1144,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,sK0(phi(sK0(phi(sK1(f,X0)))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1055]) ).
tcf(c_1145,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(sK0(phi(f_left_zero))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_1055]) ).
tcf(c_1166,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( phi(sK0(multiply(h,multiply(h,X0,X1),X2))) = multiply(h,multiply(h,X0,X1),X2) )
| ~ group_member(X2,h)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_545]) ).
tcf(c_1167,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(multiply(h,phi(X0),X1))) = multiply(h,phi(X0),X1) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_545]) ).
tcf(c_1168,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( phi(sK0(multiply(h,sK1(h,X0),X1))) = multiply(h,sK1(h,X0),X1) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_545]) ).
tcf(c_1169,plain,
! [X0: $i] :
( ( phi(sK0(multiply(h,iPr_def_10,X0))) = multiply(h,iPr_def_10,X0) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_491,c_545]) ).
tcf(c_1208,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(multiply(h,iPr_def_10,multiply(h,X0,X1)))) = multiply(h,iPr_def_10,multiply(h,X0,X1)) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1169]) ).
tcf(c_1209,plain,
! [X0: $i] :
( ( phi(sK0(multiply(h,iPr_def_10,phi(X0)))) = multiply(h,iPr_def_10,phi(X0)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1169]) ).
tcf(c_1210,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( phi(sK0(multiply(h,iPr_def_10,sK1(h,X0)))) = multiply(h,iPr_def_10,sK1(h,X0)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1169]) ).
tcf(c_1211,plain,
phi(sK0(multiply(h,iPr_def_10,iPr_def_10))) = multiply(h,iPr_def_10,iPr_def_10),
inference(superposition,[status(thm)],[c_491,c_1169]) ).
tcf(c_1230,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,phi(sK0(X2)),phi(multiply(f,X0,X1))) = phi(multiply(f,sK0(X2),multiply(f,X0,X1))) )
| ~ group_member(X2,h)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_502]) ).
tcf(c_1231,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,phi(sK0(X1)),phi(sK0(X0))) = phi(multiply(f,sK0(X1),sK0(X0))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_502]) ).
tcf(c_1232,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,phi(sK0(X1)),phi(sK1(f,X0))) = phi(multiply(f,sK0(X1),sK1(f,X0))) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_502]) ).
tcf(c_1233,plain,
! [X0: $i] :
( ( multiply(h,phi(sK0(X0)),phi(f_left_zero)) = phi(multiply(f,sK0(X0),f_left_zero)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_485,c_502]) ).
tcf(c_1234,plain,
! [X0: $i] :
( ( multiply(h,phi(sK0(X0)),iPr_def_10) = phi(multiply(f,sK0(X0),f_left_zero)) )
| ~ group_member(X0,h) ),
inference(light_normalisation,[status(thm)],[c_1233,c_276]) ).
tcf(c_1286,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(multiply(h,iPr_def_10,phi(multiply(f,X0,X1))))) = multiply(h,iPr_def_10,phi(multiply(f,X0,X1))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1209]) ).
tcf(c_1287,plain,
! [X0: $i] :
( ( phi(sK0(multiply(h,iPr_def_10,phi(sK0(X0))))) = multiply(h,iPr_def_10,phi(sK0(X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1209]) ).
tcf(c_1288,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( phi(sK0(multiply(h,iPr_def_10,phi(sK1(f,X0))))) = multiply(h,iPr_def_10,phi(sK1(f,X0))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1209]) ).
tcf(c_1289,plain,
phi(sK0(multiply(h,iPr_def_10,phi(f_left_zero)))) = multiply(h,iPr_def_10,phi(f_left_zero)),
inference(superposition,[status(thm)],[c_485,c_1209]) ).
tcf(c_1310,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(f,f_left_zero,sK1(f,X0)) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_59,c_564]) ).
tcf(c_1321,plain,
! [X0: $i,X1: $i] :
( left_zero(f,multiply(f,X0,X1))
| ( multiply(f,f_left_zero,sK1(f,multiply(f,X0,X1))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1310]) ).
tcf(c_1322,plain,
! [X0: $i] :
( left_zero(f,sK0(X0))
| ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1310]) ).
tcf(c_1323,plain,
! [X0: $i] :
( left_zero(f,X0)
| left_zero(f,sK1(f,X0))
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1310]) ).
tcf(c_1362,plain,
! [X0: $i] :
( group_member(sK0(X0),f)
| ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1322,c_57]) ).
tcf(c_1363,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ( multiply(f,sK0(X0),sK1(f,X1)) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1322,c_564]) ).
tcf(c_1364,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),sK0(iPr_def_10)) = sK0(X0) )
| ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1322,c_712]) ).
tcf(c_1365,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),f_left_zero) = sK0(X0) )
| ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1322,c_565]) ).
tcf(c_1387,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,phi(sK0(multiply(h,X0,X1))),iPr_def_10) = phi(multiply(f,sK0(multiply(h,X0,X1)),f_left_zero)) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1234]) ).
tcf(c_1388,plain,
! [X0: $i] :
( ( multiply(h,phi(sK0(phi(X0))),iPr_def_10) = phi(multiply(f,sK0(phi(X0)),f_left_zero)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1234]) ).
tcf(c_1389,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(h,phi(sK0(sK1(h,X0))),iPr_def_10) = phi(multiply(f,sK0(sK1(h,X0)),f_left_zero)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1234]) ).
tcf(c_1390,plain,
multiply(h,phi(sK0(iPr_def_10)),iPr_def_10) = phi(multiply(f,sK0(iPr_def_10),f_left_zero)),
inference(superposition,[status(thm)],[c_491,c_1234]) ).
tcf(c_1391,plain,
phi(multiply(f,sK0(iPr_def_10),f_left_zero)) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_1390,c_517,c_665]) ).
tcf(c_1412,plain,
( left_zero(h,iPr_def_10)
| ( phi(sK0(sK1(h,phi(f_left_zero)))) = sK1(h,phi(f_left_zero)) )
| ~ group_member(f_left_zero,f) ),
inference(superposition,[status(thm)],[c_276,c_832]) ).
tcf(c_1413,plain,
( left_zero(h,iPr_def_10)
| ( phi(sK0(sK1(h,phi(sK0(iPr_def_10))))) = sK1(h,phi(sK0(iPr_def_10))) )
| ~ group_member(sK0(iPr_def_10),f) ),
inference(superposition,[status(thm)],[c_517,c_832]) ).
tcf(c_1414,plain,
( left_zero(h,sK1(h,iPr_def_10))
| ( phi(sK0(sK1(h,phi(sK0(sK1(h,iPr_def_10)))))) = sK1(h,phi(sK0(sK1(h,iPr_def_10)))) )
| ~ group_member(sK0(sK1(h,iPr_def_10)),f) ),
inference(superposition,[status(thm)],[c_835,c_832]) ).
tcf(c_1415,plain,
( left_zero(h,iPr_def_10)
| ( phi(sK0(sK1(h,phi(multiply(f,sK0(iPr_def_10),f_left_zero))))) = sK1(h,phi(multiply(f,sK0(iPr_def_10),f_left_zero))) )
| ~ group_member(multiply(f,sK0(iPr_def_10),f_left_zero),f) ),
inference(superposition,[status(thm)],[c_1391,c_832]) ).
tcf(c_1416,plain,
! [X0: $i] :
( group_member(phi(X0),h)
| ( phi(sK0(sK1(h,phi(X0)))) = sK1(h,phi(X0)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_832,c_57]) ).
tcf(c_1417,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( phi(sK0(sK1(h,phi(X0)))) = sK1(h,phi(X0)) )
| ( multiply(h,phi(X0),sK1(h,X1)) = phi(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_832,c_564]) ).
tcf(c_1418,plain,
! [X0: $i] :
( ( multiply(h,phi(X0),iPr_def_10) = phi(X0) )
| ( phi(sK0(sK1(h,phi(X0)))) = sK1(h,phi(X0)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_832,c_566]) ).
tcf(c_1427,plain,
( left_zero(h,sK1(h,iPr_def_10))
| ( phi(sK0(sK1(h,sK1(h,iPr_def_10)))) = sK1(h,sK1(h,iPr_def_10)) )
| ~ group_member(sK0(sK1(h,iPr_def_10)),f) ),
inference(light_normalisation,[status(thm)],[c_1414,c_835]) ).
tcf(c_1446,plain,
( left_zero(h,sK1(h,iPr_def_10))
| ( phi(sK0(sK1(h,sK1(h,iPr_def_10)))) = sK1(h,sK1(h,iPr_def_10)) )
| ~ group_member(sK1(h,iPr_def_10),h) ),
inference(superposition,[status(thm)],[c_53,c_1427]) ).
tcf(c_1459,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,iPr_def_10,phi(sK0(phi(multiply(f,X0,X1))))) = phi(multiply(f,f_left_zero,sK0(phi(multiply(f,X0,X1))))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_952]) ).
tcf(c_1460,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,phi(sK0(phi(sK0(X0))))) = phi(multiply(f,f_left_zero,sK0(phi(sK0(X0))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_952]) ).
tcf(c_1461,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(h,iPr_def_10,phi(sK0(phi(sK1(f,X0))))) = phi(multiply(f,f_left_zero,sK0(phi(sK1(f,X0))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_952]) ).
tcf(c_1462,plain,
multiply(h,iPr_def_10,phi(sK0(phi(f_left_zero)))) = phi(multiply(f,f_left_zero,sK0(phi(f_left_zero)))),
inference(superposition,[status(thm)],[c_485,c_952]) ).
tcf(c_1480,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(sK0(phi(sK0(phi(multiply(f,X0,X1)))))))) = phi(sK0(phi(sK0(phi(multiply(f,X0,X1)))))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_973]) ).
tcf(c_1481,plain,
! [X0: $i] :
( ( phi(sK0(phi(sK0(phi(sK0(phi(sK0(X0)))))))) = phi(sK0(phi(sK0(phi(sK0(X0)))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_973]) ).
tcf(c_1482,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( phi(sK0(phi(sK0(phi(sK0(phi(sK1(f,X0)))))))) = phi(sK0(phi(sK0(phi(sK1(f,X0)))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_973]) ).
tcf(c_1483,plain,
phi(sK0(phi(sK0(phi(sK0(phi(f_left_zero))))))) = phi(sK0(phi(sK0(phi(f_left_zero))))),
inference(superposition,[status(thm)],[c_485,c_973]) ).
tcf(c_1527,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(phi(sK0(phi(multiply(f,X0,X1))))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1104]) ).
tcf(c_1528,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(phi(sK0(phi(sK0(X0))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1104]) ).
tcf(c_1529,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,phi(sK0(phi(sK0(phi(sK1(f,X0))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1104]) ).
tcf(c_1530,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(phi(sK0(phi(f_left_zero)))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_1104]) ).
tcf(c_1554,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(sK0(phi(sK0(multiply(h,X0,X1))))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1143]) ).
tcf(c_1555,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(sK0(phi(sK0(phi(X0))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1143]) ).
tcf(c_1556,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,sK0(phi(sK0(phi(sK0(sK1(h,X0))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1143]) ).
tcf(c_1557,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(sK0(phi(sK0(iPr_def_10)))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_1143]) ).
tcf(c_1588,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(multiply(h,iPr_def_10,phi(sK0(multiply(h,X0,X1)))))) = multiply(h,iPr_def_10,phi(sK0(multiply(h,X0,X1)))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1287]) ).
tcf(c_1589,plain,
! [X0: $i] :
( ( phi(sK0(multiply(h,iPr_def_10,phi(sK0(phi(X0)))))) = multiply(h,iPr_def_10,phi(sK0(phi(X0)))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1287]) ).
tcf(c_1590,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( phi(sK0(multiply(h,iPr_def_10,phi(sK0(sK1(h,X0)))))) = multiply(h,iPr_def_10,phi(sK0(sK1(h,X0)))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1287]) ).
tcf(c_1591,plain,
phi(sK0(multiply(h,iPr_def_10,phi(sK0(iPr_def_10))))) = multiply(h,iPr_def_10,phi(sK0(iPr_def_10))),
inference(superposition,[status(thm)],[c_491,c_1287]) ).
tcf(c_1608,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,phi(sK0(phi(multiply(f,X0,X1)))),iPr_def_10) = phi(multiply(f,sK0(phi(multiply(f,X0,X1))),f_left_zero)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1388]) ).
tcf(c_1609,plain,
! [X0: $i] :
( ( multiply(h,phi(sK0(phi(sK0(X0)))),iPr_def_10) = phi(multiply(f,sK0(phi(sK0(X0))),f_left_zero)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1388]) ).
tcf(c_1610,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(h,phi(sK0(phi(sK1(f,X0)))),iPr_def_10) = phi(multiply(f,sK0(phi(sK1(f,X0))),f_left_zero)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1388]) ).
tcf(c_1611,plain,
multiply(h,phi(sK0(phi(f_left_zero))),iPr_def_10) = phi(multiply(f,sK0(phi(f_left_zero)),f_left_zero)),
inference(superposition,[status(thm)],[c_485,c_1388]) ).
tcf(c_1632,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(f,X2)
| ( multiply(h,phi(sK1(f,X2)),phi(multiply(f,X0,X1))) = phi(multiply(f,sK1(f,X2),multiply(f,X0,X1))) )
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_527]) ).
tcf(c_1633,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(h,phi(sK1(f,X1)),phi(sK0(X0))) = phi(multiply(f,sK1(f,X1),sK0(X0))) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_527]) ).
tcf(c_1634,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| left_zero(f,X0)
| ( multiply(h,phi(sK1(f,X1)),phi(sK1(f,X0))) = phi(multiply(f,sK1(f,X1),sK1(f,X0))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_527]) ).
tcf(c_1635,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(h,phi(sK1(f,X0)),phi(f_left_zero)) = phi(multiply(f,sK1(f,X0),f_left_zero)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_527]) ).
tcf(c_1636,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(h,phi(sK1(f,X0)),iPr_def_10) = phi(multiply(f,sK1(f,X0),f_left_zero)) )
| ~ group_member(X0,f) ),
inference(light_normalisation,[status(thm)],[c_1635,c_276]) ).
tcf(c_1683,plain,
! [X0: $i,X1: $i] :
( left_zero(h,multiply(h,X0,X1))
| ( phi(sK0(phi(sK0(sK1(h,multiply(h,X0,X1)))))) = phi(sK0(sK1(h,multiply(h,X0,X1)))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_628]) ).
tcf(c_1684,plain,
! [X0: $i] :
( left_zero(h,phi(X0))
| ( phi(sK0(phi(sK0(sK1(h,phi(X0)))))) = phi(sK0(sK1(h,phi(X0)))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_628]) ).
tcf(c_1685,plain,
! [X0: $i] :
( left_zero(h,X0)
| left_zero(h,sK1(h,X0))
| ( phi(sK0(phi(sK0(sK1(h,sK1(h,X0)))))) = phi(sK0(sK1(h,sK1(h,X0)))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_628]) ).
tcf(c_1686,plain,
( left_zero(h,iPr_def_10)
| ( phi(sK0(phi(sK0(sK1(h,iPr_def_10))))) = phi(sK0(sK1(h,iPr_def_10))) ) ),
inference(superposition,[status(thm)],[c_491,c_628]) ).
tcf(c_1727,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( phi(sK0(sK1(h,phi(X0)))) = sK1(h,phi(X0)) )
| ( multiply(h,phi(X0),phi(sK1(f,X1))) = phi(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_832,c_686]) ).
tcf(c_1742,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(f,f_left_zero,sK0(sK1(h,X0))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_59,c_711]) ).
tcf(c_1743,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ( multiply(f,sK0(X0),sK0(sK1(h,X1))) = sK0(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1322,c_711]) ).
tcf(c_1760,plain,
! [X0: $i,X1: $i] :
( left_zero(h,multiply(h,X0,X1))
| ( multiply(f,f_left_zero,sK0(sK1(h,multiply(h,X0,X1)))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1742]) ).
tcf(c_1761,plain,
! [X0: $i] :
( left_zero(h,phi(X0))
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(X0)))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1742]) ).
tcf(c_1762,plain,
! [X0: $i] :
( left_zero(h,X0)
| left_zero(h,sK1(h,X0))
| ( multiply(f,f_left_zero,sK0(sK1(h,sK1(h,X0)))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1742]) ).
tcf(c_1763,plain,
( left_zero(h,iPr_def_10)
| ( multiply(f,f_left_zero,sK0(sK1(h,iPr_def_10))) = f_left_zero ) ),
inference(superposition,[status(thm)],[c_491,c_1742]) ).
tcf(c_1764,plain,
multiply(f,f_left_zero,sK0(sK1(h,iPr_def_10))) = f_left_zero,
inference(forward_subsumption_resolution,[status(thm)],[c_1763,c_277]) ).
tcf(c_1803,plain,
( left_zero(h,iPr_def_10)
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(f_left_zero)))) = f_left_zero )
| ~ group_member(f_left_zero,f) ),
inference(superposition,[status(thm)],[c_276,c_1761]) ).
tcf(c_1804,plain,
( left_zero(h,iPr_def_10)
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(sK0(iPr_def_10))))) = f_left_zero )
| ~ group_member(sK0(iPr_def_10),f) ),
inference(superposition,[status(thm)],[c_517,c_1761]) ).
tcf(c_1805,plain,
( left_zero(h,sK1(h,iPr_def_10))
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(sK0(sK1(h,iPr_def_10)))))) = f_left_zero )
| ~ group_member(sK0(sK1(h,iPr_def_10)),f) ),
inference(superposition,[status(thm)],[c_835,c_1761]) ).
tcf(c_1806,plain,
( left_zero(h,iPr_def_10)
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(multiply(f,sK0(iPr_def_10),f_left_zero))))) = f_left_zero )
| ~ group_member(multiply(f,sK0(iPr_def_10),f_left_zero),f) ),
inference(superposition,[status(thm)],[c_1391,c_1761]) ).
tcf(c_1807,plain,
! [X0: $i] :
( group_member(phi(X0),h)
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(X0)))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1761,c_57]) ).
tcf(c_1808,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(h,phi(X0),sK1(h,X1)) = phi(X0) )
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(X0)))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1761,c_564]) ).
tcf(c_1809,plain,
! [X0: $i] :
( ( multiply(h,phi(X0),iPr_def_10) = phi(X0) )
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(X0)))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1761,c_566]) ).
tcf(c_1810,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(X0)))) = f_left_zero )
| ( multiply(h,phi(X0),phi(sK1(f,X1))) = phi(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1761,c_686]) ).
tcf(c_1820,plain,
( left_zero(h,sK1(h,iPr_def_10))
| ( multiply(f,f_left_zero,sK0(sK1(h,sK1(h,iPr_def_10)))) = f_left_zero )
| ~ group_member(sK0(sK1(h,iPr_def_10)),f) ),
inference(light_normalisation,[status(thm)],[c_1805,c_835]) ).
tcf(c_1850,plain,
( left_zero(h,sK1(h,iPr_def_10))
| ( multiply(f,f_left_zero,sK0(sK1(h,sK1(h,iPr_def_10)))) = f_left_zero )
| ~ group_member(sK1(h,iPr_def_10),h) ),
inference(superposition,[status(thm)],[c_53,c_1820]) ).
tcf(c_1860,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(phi(sK0(phi(sK0(multiply(h,X0,X1)))))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1528]) ).
tcf(c_1861,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(phi(sK0(phi(sK0(phi(X0)))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1528]) ).
tcf(c_1862,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,phi(sK0(phi(sK0(phi(sK0(sK1(h,X0)))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1528]) ).
tcf(c_1863,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(phi(sK0(phi(sK0(iPr_def_10))))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_1528]) ).
tcf(c_1889,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(sK0(phi(sK0(phi(multiply(f,X0,X1)))))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1555]) ).
tcf(c_1890,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(sK0(phi(sK0(phi(sK0(X0)))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1555]) ).
tcf(c_1891,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,sK0(phi(sK0(phi(sK0(phi(sK1(f,X0)))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1555]) ).
tcf(c_1892,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(sK0(phi(sK0(phi(f_left_zero))))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_1555]) ).
tcf(c_1924,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X1,X4,multiply(X1,multiply(X1,X0,X2),X3)) = X4 )
| ~ left_zero(X1,X4)
| ~ group_member(X3,X1)
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(superposition,[status(thm)],[c_49,c_561]) ).
tcf(c_1925,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,multiply(h,phi(X0),X1)) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_561]) ).
tcf(c_1926,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,sK0(X0),X1)) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_561]) ).
tcf(c_1927,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( left_zero(X1,X0)
| ( multiply(X1,X3,multiply(X1,sK1(X1,X0),X2)) = X3 )
| ~ left_zero(X1,X3)
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(superposition,[status(thm)],[c_56,c_561]) ).
tcf(c_1928,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,f_left_zero,X0)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_561]) ).
tcf(c_1929,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,multiply(h,iPr_def_10,X0)) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_491,c_561]) ).
tcf(c_1992,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,f_left_zero,multiply(f,X0,X1))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1928]) ).
tcf(c_1993,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,f_left_zero,sK0(X0))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1928]) ).
tcf(c_1994,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,multiply(f,f_left_zero,sK1(f,X0))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1928]) ).
tcf(c_1995,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,f_left_zero,f_left_zero)) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_1928]) ).
tcf(c_2020,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,multiply(h,iPr_def_10,multiply(h,X0,X1))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1929]) ).
tcf(c_2021,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,multiply(h,iPr_def_10,phi(X0))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1929]) ).
tcf(c_2022,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,multiply(h,iPr_def_10,sK1(h,X0))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1929]) ).
tcf(c_2023,plain,
! [X0: $i] :
( ( multiply(h,X0,multiply(h,iPr_def_10,iPr_def_10)) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_1929]) ).
tcf(c_2067,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,f_left_zero,sK0(multiply(h,X0,X1)))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1993]) ).
tcf(c_2068,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,f_left_zero,sK0(phi(X0)))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1993]) ).
tcf(c_2069,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,multiply(f,f_left_zero,sK0(sK1(h,X0)))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1993]) ).
tcf(c_2070,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,f_left_zero,sK0(iPr_def_10))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_1993]) ).
tcf(c_2115,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(h,phi(multiply(f,multiply(f,X0,X1),X2)),phi(X3)) = phi(multiply(f,multiply(f,multiply(f,X0,X1),X2),X3)) )
| ~ group_member(X3,f)
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_544]) ).
tcf(c_2116,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,phi(multiply(f,sK0(X0),X1)),phi(X2)) = phi(multiply(f,multiply(f,sK0(X0),X1),X2)) )
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_544]) ).
tcf(c_2117,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(f,X0)
| ( multiply(h,phi(multiply(f,sK1(f,X0),X1)),phi(X2)) = phi(multiply(f,multiply(f,sK1(f,X0),X1),X2)) )
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_544]) ).
tcf(c_2118,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,phi(multiply(f,f_left_zero,X0)),phi(X1)) = phi(multiply(f,multiply(f,f_left_zero,X0),X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_544]) ).
tcf(c_2146,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,multiply(h,iPr_def_10,phi(multiply(f,X0,X1)))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_2021]) ).
tcf(c_2147,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,multiply(h,iPr_def_10,phi(sK0(X0)))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_2021]) ).
tcf(c_2148,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,multiply(h,iPr_def_10,phi(sK1(f,X0)))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_2021]) ).
tcf(c_2149,plain,
! [X0: $i] :
( ( multiply(h,X0,multiply(h,iPr_def_10,phi(f_left_zero))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_2021]) ).
tcf(c_2171,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,f_left_zero,sK0(phi(multiply(f,X0,X1))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_2068]) ).
tcf(c_2172,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,f_left_zero,sK0(phi(sK0(X0))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_2068]) ).
tcf(c_2173,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,multiply(f,f_left_zero,sK0(phi(sK1(f,X0))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_2068]) ).
tcf(c_2174,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,f_left_zero,sK0(phi(f_left_zero)))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_2068]) ).
tcf(c_2195,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,multiply(h,iPr_def_10,phi(sK0(multiply(h,X0,X1))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_2147]) ).
tcf(c_2196,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,multiply(h,iPr_def_10,phi(sK0(phi(X0))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_2147]) ).
tcf(c_2197,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,multiply(h,iPr_def_10,phi(sK0(sK1(h,X0))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_2147]) ).
tcf(c_2198,plain,
! [X0: $i] :
( ( multiply(h,X0,multiply(h,iPr_def_10,phi(sK0(iPr_def_10)))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_2147]) ).
tcf(c_2224,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,f_left_zero,sK0(phi(sK0(multiply(h,X0,X1)))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_2172]) ).
tcf(c_2225,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,f_left_zero,sK0(phi(sK0(phi(X0)))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_2172]) ).
tcf(c_2226,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,X0)))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_2172]) ).
tcf(c_2227,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,f_left_zero,sK0(phi(sK0(iPr_def_10))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_2172]) ).
tcf(c_2250,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,multiply(h,iPr_def_10,phi(sK0(phi(multiply(f,X0,X1)))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_2196]) ).
tcf(c_2251,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,multiply(h,iPr_def_10,phi(sK0(phi(sK0(X0)))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_2196]) ).
tcf(c_2252,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,multiply(h,iPr_def_10,phi(sK0(phi(sK1(f,X0)))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_2196]) ).
tcf(c_2253,plain,
! [X0: $i] :
( ( multiply(h,X0,multiply(h,iPr_def_10,phi(sK0(phi(f_left_zero))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_2196]) ).
tcf(c_2323,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( phi(sK0(phi(multiply(f,multiply(f,X0,X1),X2)))) = phi(multiply(f,multiply(f,X0,X1),X2)) )
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_605]) ).
tcf(c_2324,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(multiply(f,sK0(X0),X1)))) = phi(multiply(f,sK0(X0),X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_605]) ).
tcf(c_2325,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( phi(sK0(phi(multiply(f,sK1(f,X0),X1)))) = phi(multiply(f,sK1(f,X0),X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_605]) ).
tcf(c_2326,plain,
! [X0: $i] :
( ( phi(sK0(phi(multiply(f,f_left_zero,X0)))) = phi(multiply(f,f_left_zero,X0)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_605]) ).
tcf(c_2371,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(multiply(f,f_left_zero,multiply(f,X0,X1))))) = phi(multiply(f,f_left_zero,multiply(f,X0,X1))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_2326]) ).
tcf(c_2372,plain,
! [X0: $i] :
( ( phi(sK0(phi(multiply(f,f_left_zero,sK0(X0))))) = phi(multiply(f,f_left_zero,sK0(X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_2326]) ).
tcf(c_2373,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( phi(sK0(phi(multiply(f,f_left_zero,sK1(f,X0))))) = phi(multiply(f,f_left_zero,sK1(f,X0))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_2326]) ).
tcf(c_2374,plain,
phi(sK0(phi(multiply(f,f_left_zero,f_left_zero)))) = phi(multiply(f,f_left_zero,f_left_zero)),
inference(superposition,[status(thm)],[c_485,c_2326]) ).
tcf(c_2391,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(multiply(f,f_left_zero,sK0(multiply(h,X0,X1)))))) = phi(multiply(f,f_left_zero,sK0(multiply(h,X0,X1)))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_2372]) ).
tcf(c_2392,plain,
! [X0: $i] :
( ( phi(sK0(phi(multiply(f,f_left_zero,sK0(phi(X0)))))) = phi(multiply(f,f_left_zero,sK0(phi(X0)))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_2372]) ).
tcf(c_2393,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( phi(sK0(phi(multiply(f,f_left_zero,sK0(sK1(h,X0)))))) = phi(multiply(f,f_left_zero,sK0(sK1(h,X0)))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_2372]) ).
tcf(c_2394,plain,
phi(sK0(phi(multiply(f,f_left_zero,sK0(iPr_def_10))))) = phi(multiply(f,f_left_zero,sK0(iPr_def_10))),
inference(superposition,[status(thm)],[c_491,c_2372]) ).
tcf(c_2415,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(X0)))) = f_left_zero )
| ( multiply(h,phi(X0),phi(sK0(sK1(h,X1)))) = phi(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1761,c_884]) ).
tcf(c_2416,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( phi(sK0(sK1(h,phi(X0)))) = sK1(h,phi(X0)) )
| ( multiply(h,phi(X0),phi(sK0(sK1(h,X1)))) = phi(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_832,c_884]) ).
tcf(c_2437,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,X0)))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_59,c_921]) ).
tcf(c_2438,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ( multiply(f,sK0(X0),sK0(phi(sK1(f,X1)))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1322,c_921]) ).
tcf(c_2455,plain,
! [X0: $i,X1: $i] :
( left_zero(f,multiply(f,X0,X1))
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,multiply(f,X0,X1))))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_2437]) ).
tcf(c_2456,plain,
! [X0: $i] :
( left_zero(f,sK0(X0))
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_2437]) ).
tcf(c_2457,plain,
! [X0: $i] :
( left_zero(f,X0)
| left_zero(f,sK1(f,X0))
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK1(f,X0))))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_2437]) ).
tcf(c_2479,plain,
! [X0: $i] :
( group_member(sK0(X0),f)
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_2456,c_57]) ).
tcf(c_2480,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,sK0(X0),sK1(f,X1)) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_2456,c_564]) ).
tcf(c_2481,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),sK0(iPr_def_10)) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_2456,c_712]) ).
tcf(c_2482,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),f_left_zero) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_2456,c_565]) ).
tcf(c_2483,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ( multiply(f,sK0(X0),sK0(phi(sK1(f,X1)))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_2456,c_921]) ).
tcf(c_2484,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,sK0(X0),sK0(sK1(h,X1))) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_2456,c_711]) ).
tcf(c_2554,plain,
! [X0: $i] :
( group_member(sK0(X0),f)
| ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1080,c_57]) ).
tcf(c_2555,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ( multiply(f,sK0(X0),sK1(f,X1)) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1080,c_564]) ).
tcf(c_2556,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),sK0(iPr_def_10)) = sK0(X0) )
| ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1080,c_712]) ).
tcf(c_2557,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),f_left_zero) = sK0(X0) )
| ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1080,c_565]) ).
tcf(c_2558,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ( multiply(f,sK0(X0),sK0(phi(sK1(f,X1)))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1080,c_921]) ).
tcf(c_2559,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ( multiply(f,sK0(X0),sK0(sK1(h,X1))) = sK0(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1080,c_711]) ).
tcf(c_2595,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( phi(sK0(multiply(h,phi(multiply(f,X0,X1)),X2))) = multiply(h,phi(multiply(f,X0,X1)),X2) )
| ~ group_member(X2,h)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1167]) ).
tcf(c_2596,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(multiply(h,phi(sK0(X0)),X1))) = multiply(h,phi(sK0(X0)),X1) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1167]) ).
tcf(c_2597,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( phi(sK0(multiply(h,phi(sK1(f,X0)),X1))) = multiply(h,phi(sK1(f,X0)),X1) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1167]) ).
tcf(c_2598,plain,
! [X0: $i] :
( ( phi(sK0(multiply(h,phi(f_left_zero),X0))) = multiply(h,phi(f_left_zero),X0) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_485,c_1167]) ).
tcf(c_2618,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,iPr_def_10,phi(sK0(phi(sK0(multiply(h,X0,X1)))))) = phi(multiply(f,f_left_zero,sK0(phi(sK0(multiply(h,X0,X1)))))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1460]) ).
tcf(c_2619,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,phi(sK0(phi(sK0(phi(X0)))))) = phi(multiply(f,f_left_zero,sK0(phi(sK0(phi(X0)))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1460]) ).
tcf(c_2620,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(h,iPr_def_10,phi(sK0(phi(sK0(sK1(h,X0)))))) = phi(multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,X0)))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1460]) ).
tcf(c_2621,plain,
multiply(h,iPr_def_10,phi(sK0(phi(sK0(iPr_def_10))))) = phi(multiply(f,f_left_zero,sK0(phi(sK0(iPr_def_10))))),
inference(superposition,[status(thm)],[c_491,c_1460]) ).
tcf(c_2662,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( phi(sK0(phi(sK0(multiply(h,multiply(h,X0,X1),X2))))) = phi(sK0(multiply(h,multiply(h,X0,X1),X2))) )
| ~ group_member(X2,h)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_626]) ).
tcf(c_2663,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(sK0(multiply(h,phi(X0),X1))))) = phi(sK0(multiply(h,phi(X0),X1))) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_626]) ).
tcf(c_2664,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( phi(sK0(phi(sK0(multiply(h,sK1(h,X0),X1))))) = phi(sK0(multiply(h,sK1(h,X0),X1))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_626]) ).
tcf(c_2665,plain,
! [X0: $i] :
( ( phi(sK0(phi(sK0(multiply(h,iPr_def_10,X0))))) = phi(sK0(multiply(h,iPr_def_10,X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_491,c_626]) ).
tcf(c_2691,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(sK0(phi(sK0(phi(sK0(multiply(h,X0,X1))))))))) = phi(sK0(phi(sK0(phi(sK0(multiply(h,X0,X1))))))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1481]) ).
tcf(c_2692,plain,
! [X0: $i] :
( ( phi(sK0(phi(sK0(phi(sK0(phi(sK0(phi(X0))))))))) = phi(sK0(phi(sK0(phi(sK0(phi(X0))))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1481]) ).
tcf(c_2693,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( phi(sK0(phi(sK0(phi(sK0(phi(sK0(sK1(h,X0))))))))) = phi(sK0(phi(sK0(phi(sK0(sK1(h,X0))))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1481]) ).
tcf(c_2694,plain,
phi(sK0(phi(sK0(phi(sK0(phi(sK0(iPr_def_10)))))))) = phi(sK0(phi(sK0(phi(sK0(iPr_def_10)))))),
inference(superposition,[status(thm)],[c_491,c_1481]) ).
tcf(c_2711,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(multiply(h,iPr_def_10,phi(sK0(phi(multiply(f,X0,X1))))))) = multiply(h,iPr_def_10,phi(sK0(phi(multiply(f,X0,X1))))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1589]) ).
tcf(c_2712,plain,
! [X0: $i] :
( ( phi(sK0(multiply(h,iPr_def_10,phi(sK0(phi(sK0(X0))))))) = multiply(h,iPr_def_10,phi(sK0(phi(sK0(X0))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1589]) ).
tcf(c_2713,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( phi(sK0(multiply(h,iPr_def_10,phi(sK0(phi(sK1(f,X0))))))) = multiply(h,iPr_def_10,phi(sK0(phi(sK1(f,X0))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1589]) ).
tcf(c_2714,plain,
phi(sK0(multiply(h,iPr_def_10,phi(sK0(phi(f_left_zero)))))) = multiply(h,iPr_def_10,phi(sK0(phi(f_left_zero)))),
inference(superposition,[status(thm)],[c_485,c_1589]) ).
tcf(c_2752,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,phi(sK0(phi(sK0(multiply(h,X0,X1))))),iPr_def_10) = phi(multiply(f,sK0(phi(sK0(multiply(h,X0,X1)))),f_left_zero)) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1609]) ).
tcf(c_2753,plain,
! [X0: $i] :
( ( multiply(h,phi(sK0(phi(sK0(phi(X0))))),iPr_def_10) = phi(multiply(f,sK0(phi(sK0(phi(X0)))),f_left_zero)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1609]) ).
tcf(c_2754,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(h,phi(sK0(phi(sK0(sK1(h,X0))))),iPr_def_10) = phi(multiply(f,sK0(phi(sK0(sK1(h,X0)))),f_left_zero)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1609]) ).
tcf(c_2755,plain,
multiply(h,phi(sK0(phi(sK0(iPr_def_10)))),iPr_def_10) = phi(multiply(f,sK0(phi(sK0(iPr_def_10))),f_left_zero)),
inference(superposition,[status(thm)],[c_491,c_1609]) ).
tcf(c_2774,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(phi(sK0(phi(sK0(phi(multiply(f,X0,X1))))))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1861]) ).
tcf(c_2775,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(phi(sK0(phi(sK0(phi(sK0(X0))))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1861]) ).
tcf(c_2776,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,phi(sK0(phi(sK0(phi(sK0(phi(sK1(f,X0))))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1861]) ).
tcf(c_2777,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(phi(sK0(phi(sK0(phi(f_left_zero)))))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_1861]) ).
tcf(c_2797,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(sK0(multiply(h,iPr_def_10,multiply(h,X0,X1)))))) = phi(sK0(multiply(h,iPr_def_10,multiply(h,X0,X1)))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_2665]) ).
tcf(c_2798,plain,
! [X0: $i] :
( ( phi(sK0(phi(sK0(multiply(h,iPr_def_10,phi(X0)))))) = phi(sK0(multiply(h,iPr_def_10,phi(X0)))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_2665]) ).
tcf(c_2799,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( phi(sK0(phi(sK0(multiply(h,iPr_def_10,sK1(h,X0)))))) = phi(sK0(multiply(h,iPr_def_10,sK1(h,X0)))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_2665]) ).
tcf(c_2800,plain,
phi(sK0(phi(sK0(multiply(h,iPr_def_10,iPr_def_10))))) = phi(sK0(multiply(h,iPr_def_10,iPr_def_10))),
inference(superposition,[status(thm)],[c_491,c_2665]) ).
tcf(c_2841,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(sK0(phi(sK0(phi(sK0(multiply(h,X0,X1))))))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1890]) ).
tcf(c_2842,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(sK0(phi(sK0(phi(sK0(phi(X0))))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1890]) ).
tcf(c_2843,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,sK0(phi(sK0(phi(sK0(phi(sK0(sK1(h,X0))))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1890]) ).
tcf(c_2844,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(sK0(phi(sK0(phi(sK0(iPr_def_10)))))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_1890]) ).
tcf(c_2866,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,f_left_zero,sK0(phi(sK0(phi(multiply(f,X0,X1))))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_2225]) ).
tcf(c_2867,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,f_left_zero,sK0(phi(sK0(phi(sK0(X0))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_2225]) ).
tcf(c_2868,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,X0))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_2225]) ).
tcf(c_2869,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,f_left_zero,sK0(phi(sK0(phi(f_left_zero)))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_2225]) ).
tcf(c_2893,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,multiply(h,iPr_def_10,phi(sK0(phi(sK0(multiply(h,X0,X1))))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_2251]) ).
tcf(c_2894,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,multiply(h,iPr_def_10,phi(sK0(phi(sK0(phi(X0))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_2251]) ).
tcf(c_2895,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,multiply(h,iPr_def_10,phi(sK0(phi(sK0(sK1(h,X0))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_2251]) ).
tcf(c_2896,plain,
! [X0: $i] :
( ( multiply(h,X0,multiply(h,iPr_def_10,phi(sK0(phi(sK0(iPr_def_10)))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_2251]) ).
tcf(c_2930,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(multiply(f,f_left_zero,sK0(phi(multiply(f,X0,X1))))))) = phi(multiply(f,f_left_zero,sK0(phi(multiply(f,X0,X1))))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_2392]) ).
tcf(c_2931,plain,
! [X0: $i] :
( ( phi(sK0(phi(multiply(f,f_left_zero,sK0(phi(sK0(X0))))))) = phi(multiply(f,f_left_zero,sK0(phi(sK0(X0))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_2392]) ).
tcf(c_2932,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( phi(sK0(phi(multiply(f,f_left_zero,sK0(phi(sK1(f,X0))))))) = phi(multiply(f,f_left_zero,sK0(phi(sK1(f,X0))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_2392]) ).
tcf(c_2933,plain,
phi(sK0(phi(multiply(f,f_left_zero,sK0(phi(f_left_zero)))))) = phi(multiply(f,f_left_zero,sK0(phi(f_left_zero)))),
inference(superposition,[status(thm)],[c_485,c_2392]) ).
tcf(c_2952,plain,
! [X0: $i,X1: $i] :
( ( phi(sK0(phi(sK0(multiply(h,iPr_def_10,phi(multiply(f,X0,X1))))))) = phi(sK0(multiply(h,iPr_def_10,phi(multiply(f,X0,X1))))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_2798]) ).
tcf(c_2953,plain,
! [X0: $i] :
( ( phi(sK0(phi(sK0(multiply(h,iPr_def_10,phi(sK0(X0))))))) = phi(sK0(multiply(h,iPr_def_10,phi(sK0(X0))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_2798]) ).
tcf(c_2954,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( phi(sK0(phi(sK0(multiply(h,iPr_def_10,phi(sK1(f,X0))))))) = phi(sK0(multiply(h,iPr_def_10,phi(sK1(f,X0))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_2798]) ).
tcf(c_2955,plain,
phi(sK0(phi(sK0(multiply(h,iPr_def_10,phi(f_left_zero)))))) = phi(sK0(multiply(h,iPr_def_10,phi(f_left_zero)))),
inference(superposition,[status(thm)],[c_485,c_2798]) ).
tcf(c_2974,plain,
! [X0: $i,X1: $i] :
( left_zero(f,multiply(f,X0,X1))
| ( multiply(h,iPr_def_10,phi(sK1(f,multiply(f,X0,X1)))) = phi(multiply(f,f_left_zero,sK1(f,multiply(f,X0,X1)))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_663]) ).
tcf(c_2975,plain,
! [X0: $i] :
( left_zero(f,sK0(X0))
| ( multiply(h,iPr_def_10,phi(sK1(f,sK0(X0)))) = phi(multiply(f,f_left_zero,sK1(f,sK0(X0)))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_663]) ).
tcf(c_2976,plain,
! [X0: $i] :
( left_zero(f,X0)
| left_zero(f,sK1(f,X0))
| ( multiply(h,iPr_def_10,phi(sK1(f,sK1(f,X0)))) = phi(multiply(f,f_left_zero,sK1(f,sK1(f,X0)))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_663]) ).
tcf(c_3027,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(h,X3,phi(multiply(f,multiply(f,X0,X1),X2))) = X3 )
| ~ left_zero(h,X3)
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_684]) ).
tcf(c_3028,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(multiply(f,sK0(X0),X1))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_684]) ).
tcf(c_3029,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(f,X0)
| ( multiply(h,X2,phi(multiply(f,sK1(f,X0),X1))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_684]) ).
tcf(c_3030,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(multiply(f,f_left_zero,X0))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_684]) ).
tcf(c_3075,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(multiply(f,f_left_zero,multiply(f,X0,X1)))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_3030]) ).
tcf(c_3076,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(multiply(f,f_left_zero,sK0(X0)))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_3030]) ).
tcf(c_3077,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,phi(multiply(f,f_left_zero,sK1(f,X0)))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_3030]) ).
tcf(c_3078,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(multiply(f,f_left_zero,f_left_zero))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_3030]) ).
tcf(c_3115,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(multiply(f,f_left_zero,sK0(multiply(h,X0,X1))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_3076]) ).
tcf(c_3116,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(multiply(f,f_left_zero,sK0(phi(X0))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_3076]) ).
tcf(c_3117,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,phi(multiply(f,f_left_zero,sK0(sK1(h,X0))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_3076]) ).
tcf(c_3118,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(multiply(f,f_left_zero,sK0(iPr_def_10)))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_3076]) ).
tcf(c_3139,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(multiply(f,f_left_zero,sK0(phi(multiply(f,X0,X1)))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_3116]) ).
tcf(c_3140,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(multiply(f,f_left_zero,sK0(phi(sK0(X0)))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_3116]) ).
tcf(c_3141,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,phi(multiply(f,f_left_zero,sK0(phi(sK1(f,X0)))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_3116]) ).
tcf(c_3142,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(multiply(f,f_left_zero,sK0(phi(f_left_zero))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_3116]) ).
tcf(c_3164,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,iPr_def_10,phi(multiply(f,multiply(f,X0,X1),X2))) = phi(multiply(f,f_left_zero,multiply(f,multiply(f,X0,X1),X2))) )
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_661]) ).
tcf(c_3165,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,iPr_def_10,phi(multiply(f,sK0(X0),X1))) = phi(multiply(f,f_left_zero,multiply(f,sK0(X0),X1))) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_661]) ).
tcf(c_3166,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,iPr_def_10,phi(multiply(f,sK1(f,X0),X1))) = phi(multiply(f,f_left_zero,multiply(f,sK1(f,X0),X1))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_661]) ).
tcf(c_3167,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,phi(multiply(f,f_left_zero,X0))) = phi(multiply(f,f_left_zero,multiply(f,f_left_zero,X0))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_661]) ).
tcf(c_3191,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(multiply(f,f_left_zero,sK0(phi(sK0(multiply(h,X0,X1))))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_3140]) ).
tcf(c_3192,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(multiply(f,f_left_zero,sK0(phi(sK0(phi(X0))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_3140]) ).
tcf(c_3193,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,phi(multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,X0))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_3140]) ).
tcf(c_3194,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(multiply(f,f_left_zero,sK0(phi(sK0(iPr_def_10)))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_3140]) ).
tcf(c_3234,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(f,X3,sK0(multiply(h,multiply(h,X0,X1),X2))) = X3 )
| ~ left_zero(f,X3)
| ~ group_member(X2,h)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_709]) ).
tcf(c_3235,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(multiply(h,phi(X0),X1))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_709]) ).
tcf(c_3236,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(h,X0)
| ( multiply(f,X2,sK0(multiply(h,sK1(h,X0),X1))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_709]) ).
tcf(c_3237,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(multiply(h,iPr_def_10,X0))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_491,c_709]) ).
tcf(c_3280,plain,
! [X0: $i,X1: $i] :
( left_zero(f,multiply(f,X0,X1))
| ( phi(sK0(phi(sK0(phi(sK1(f,multiply(f,X0,X1))))))) = phi(sK0(phi(sK1(f,multiply(f,X0,X1))))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_808]) ).
tcf(c_3281,plain,
! [X0: $i] :
( left_zero(f,sK0(X0))
| ( phi(sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = phi(sK0(phi(sK1(f,sK0(X0))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_808]) ).
tcf(c_3282,plain,
! [X0: $i] :
( left_zero(f,X0)
| left_zero(f,sK1(f,X0))
| ( phi(sK0(phi(sK0(phi(sK1(f,sK1(f,X0))))))) = phi(sK0(phi(sK1(f,sK1(f,X0))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_808]) ).
tcf(c_3306,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(X0)))) = f_left_zero )
| ( multiply(h,phi(X0),phi(sK0(phi(sK1(f,X1))))) = phi(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1761,c_1002]) ).
tcf(c_3307,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( phi(sK0(sK1(h,phi(X0)))) = sK1(h,phi(X0)) )
| ( multiply(h,phi(X0),phi(sK0(phi(sK1(f,X1))))) = phi(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_832,c_1002]) ).
tcf(c_3326,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(multiply(h,iPr_def_10,multiply(h,X0,X1)))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_3237]) ).
tcf(c_3327,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(multiply(h,iPr_def_10,phi(X0)))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_3237]) ).
tcf(c_3328,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,sK0(multiply(h,iPr_def_10,sK1(h,X0)))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_3237]) ).
tcf(c_3329,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(multiply(h,iPr_def_10,iPr_def_10))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_3237]) ).
tcf(c_3373,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(multiply(h,iPr_def_10,phi(multiply(f,X0,X1))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_3327]) ).
tcf(c_3374,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(multiply(h,iPr_def_10,phi(sK0(X0))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_3327]) ).
tcf(c_3375,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,sK0(multiply(h,iPr_def_10,phi(sK1(f,X0))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_3327]) ).
tcf(c_3376,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(multiply(h,iPr_def_10,phi(f_left_zero)))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_3327]) ).
tcf(c_3397,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(multiply(h,iPr_def_10,phi(sK0(multiply(h,X0,X1)))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_3374]) ).
tcf(c_3398,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(multiply(h,iPr_def_10,phi(sK0(phi(X0)))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_3374]) ).
tcf(c_3399,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,sK0(multiply(h,iPr_def_10,phi(sK0(sK1(h,X0)))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_3374]) ).
tcf(c_3400,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(multiply(h,iPr_def_10,phi(sK0(iPr_def_10))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_3374]) ).
tcf(c_3420,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,iPr_def_10,phi(multiply(f,f_left_zero,multiply(f,X0,X1)))) = phi(multiply(f,f_left_zero,multiply(f,f_left_zero,multiply(f,X0,X1)))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_3167]) ).
tcf(c_3421,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,phi(multiply(f,f_left_zero,sK0(X0)))) = phi(multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(X0)))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_3167]) ).
tcf(c_3422,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(h,iPr_def_10,phi(multiply(f,f_left_zero,sK1(f,X0)))) = phi(multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,X0)))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_3167]) ).
tcf(c_3423,plain,
multiply(h,iPr_def_10,phi(multiply(f,f_left_zero,f_left_zero))) = phi(multiply(f,f_left_zero,multiply(f,f_left_zero,f_left_zero))),
inference(superposition,[status(thm)],[c_485,c_3167]) ).
tcf(c_3479,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(multiply(h,iPr_def_10,phi(sK0(phi(multiply(f,X0,X1))))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_3398]) ).
tcf(c_3480,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(multiply(h,iPr_def_10,phi(sK0(phi(sK0(X0))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_3398]) ).
tcf(c_3481,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,sK0(multiply(h,iPr_def_10,phi(sK0(phi(sK1(f,X0))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_3398]) ).
tcf(c_3482,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(multiply(h,iPr_def_10,phi(sK0(phi(f_left_zero)))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_3398]) ).
tcf(c_3505,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,X0))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_59,c_1056]) ).
tcf(c_3506,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ( multiply(f,sK0(X0),sK0(phi(sK0(sK1(h,X1))))) = sK0(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1080,c_1056]) ).
tcf(c_3507,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ( multiply(f,sK0(X0),sK0(phi(sK0(sK1(h,X1))))) = sK0(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_2456,c_1056]) ).
tcf(c_3508,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ( multiply(f,sK0(X0),sK0(phi(sK0(sK1(h,X1))))) = sK0(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1322,c_1056]) ).
tcf(c_3546,plain,
! [X0: $i,X1: $i] :
( left_zero(h,multiply(h,X0,X1))
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,multiply(h,X0,X1)))))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_3505]) ).
tcf(c_3547,plain,
! [X0: $i] :
( left_zero(h,phi(X0))
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(X0)))))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_3505]) ).
tcf(c_3548,plain,
! [X0: $i] :
( left_zero(h,X0)
| left_zero(h,sK1(h,X0))
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,sK1(h,X0)))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_3505]) ).
tcf(c_3549,plain,
( left_zero(h,iPr_def_10)
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,iPr_def_10))))) = f_left_zero ) ),
inference(superposition,[status(thm)],[c_491,c_3505]) ).
tcf(c_3571,plain,
( left_zero(h,iPr_def_10)
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(f_left_zero)))))) = f_left_zero )
| ~ group_member(f_left_zero,f) ),
inference(superposition,[status(thm)],[c_276,c_3547]) ).
tcf(c_3572,plain,
( left_zero(h,iPr_def_10)
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(sK0(iPr_def_10))))))) = f_left_zero )
| ~ group_member(sK0(iPr_def_10),f) ),
inference(superposition,[status(thm)],[c_517,c_3547]) ).
tcf(c_3573,plain,
( left_zero(h,sK1(h,iPr_def_10))
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(sK0(sK1(h,iPr_def_10)))))))) = f_left_zero )
| ~ group_member(sK0(sK1(h,iPr_def_10)),f) ),
inference(superposition,[status(thm)],[c_835,c_3547]) ).
tcf(c_3574,plain,
( left_zero(h,iPr_def_10)
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(multiply(f,sK0(iPr_def_10),f_left_zero))))))) = f_left_zero )
| ~ group_member(multiply(f,sK0(iPr_def_10),f_left_zero),f) ),
inference(superposition,[status(thm)],[c_1391,c_3547]) ).
tcf(c_3575,plain,
! [X0: $i] :
( group_member(phi(X0),h)
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(X0)))))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_3547,c_57]) ).
tcf(c_3576,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(h,phi(X0),sK1(h,X1)) = phi(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(X0)))))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_3547,c_564]) ).
tcf(c_3577,plain,
! [X0: $i] :
( ( multiply(h,phi(X0),iPr_def_10) = phi(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(X0)))))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_3547,c_566]) ).
tcf(c_3578,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(X0)))))) = f_left_zero )
| ( multiply(h,phi(X0),phi(sK0(phi(sK1(f,X1))))) = phi(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_3547,c_1002]) ).
tcf(c_3579,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(h,phi(X0),phi(sK0(sK1(h,X1)))) = phi(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(X0)))))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_3547,c_884]) ).
tcf(c_3580,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(h,phi(X0),phi(sK1(f,X1))) = phi(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(X0)))))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_3547,c_686]) ).
tcf(c_3590,plain,
( left_zero(h,sK1(h,iPr_def_10))
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,sK1(h,iPr_def_10)))))) = f_left_zero )
| ~ group_member(sK0(sK1(h,iPr_def_10)),f) ),
inference(light_normalisation,[status(thm)],[c_3573,c_835]) ).
tcf(c_3653,plain,
( left_zero(h,sK1(h,iPr_def_10))
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,sK1(h,iPr_def_10)))))) = f_left_zero )
| ~ group_member(sK1(h,iPr_def_10),h) ),
inference(superposition,[status(thm)],[c_53,c_3590]) ).
tcf(c_3665,plain,
! [X0: $i,X1: $i] :
( left_zero(h,multiply(h,X0,X1))
| ( phi(sK0(multiply(h,iPr_def_10,sK1(h,multiply(h,X0,X1))))) = multiply(h,iPr_def_10,sK1(h,multiply(h,X0,X1))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1210]) ).
tcf(c_3666,plain,
! [X0: $i] :
( left_zero(h,phi(X0))
| ( phi(sK0(multiply(h,iPr_def_10,sK1(h,phi(X0))))) = multiply(h,iPr_def_10,sK1(h,phi(X0))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1210]) ).
tcf(c_3667,plain,
! [X0: $i] :
( left_zero(h,X0)
| left_zero(h,sK1(h,X0))
| ( phi(sK0(multiply(h,iPr_def_10,sK1(h,sK1(h,X0))))) = multiply(h,iPr_def_10,sK1(h,sK1(h,X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1210]) ).
tcf(c_3668,plain,
( left_zero(h,iPr_def_10)
| ( phi(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10)))) = multiply(h,iPr_def_10,sK1(h,iPr_def_10)) ) ),
inference(superposition,[status(thm)],[c_491,c_1210]) ).
tcf(c_3669,plain,
phi(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10)))) = multiply(h,iPr_def_10,sK1(h,iPr_def_10)),
inference(forward_subsumption_resolution,[status(thm)],[c_3668,c_277]) ).
tcf(c_3684,plain,
( left_zero(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10)))
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))))))))) = f_left_zero )
| ~ group_member(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))),f) ),
inference(superposition,[status(thm)],[c_3669,c_3547]) ).
tcf(c_3685,plain,
( left_zero(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10)))
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))))))) = f_left_zero )
| ~ group_member(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))),f) ),
inference(superposition,[status(thm)],[c_3669,c_1761]) ).
tcf(c_3686,plain,
( left_zero(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10)))
| ( phi(sK0(sK1(h,phi(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))))))) = sK1(h,phi(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))))) )
| ~ group_member(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))),f) ),
inference(superposition,[status(thm)],[c_3669,c_832]) ).
tcf(c_3687,plain,
( group_member(multiply(h,iPr_def_10,sK1(h,iPr_def_10)),h)
| ~ group_member(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))),f) ),
inference(superposition,[status(thm)],[c_3669,c_51]) ).
tcf(c_3690,plain,
( left_zero(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10)))
| ( multiply(f,f_left_zero,sK0(sK1(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10))))) = f_left_zero )
| ~ group_member(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))),f) ),
inference(light_normalisation,[status(thm)],[c_3685,c_3669]) ).
tcf(c_3694,plain,
( left_zero(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10)))
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10))))))) = f_left_zero )
| ~ group_member(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))),f) ),
inference(light_normalisation,[status(thm)],[c_3684,c_3669]) ).
tcf(c_3698,plain,
( left_zero(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10)))
| ( phi(sK0(sK1(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10))))) = sK1(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10))) )
| ~ group_member(sK0(multiply(h,iPr_def_10,sK1(h,iPr_def_10))),f) ),
inference(light_normalisation,[status(thm)],[c_3686,c_3669]) ).
tcf(c_3722,plain,
! [X0: $i] :
( left_zero(f,X0)
| group_member(sK1(f,X0),f)
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1323,c_57]) ).
tcf(c_3723,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| left_zero(f,X0)
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ( multiply(f,sK1(f,X0),sK1(f,X1)) = sK1(f,X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1323,c_564]) ).
tcf(c_3724,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(f,sK1(f,X0),sK0(iPr_def_10)) = sK1(f,X0) )
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1323,c_712]) ).
tcf(c_3725,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(f,sK1(f,X0),f_left_zero) = sK1(f,X0) )
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1323,c_565]) ).
tcf(c_3726,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| left_zero(h,X1)
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ( multiply(f,sK1(f,X0),sK0(phi(sK0(sK1(h,X1))))) = sK1(f,X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1323,c_1056]) ).
tcf(c_3727,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| left_zero(f,X0)
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ( multiply(f,sK1(f,X0),sK0(phi(sK1(f,X1)))) = sK1(f,X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1323,c_921]) ).
tcf(c_3728,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| left_zero(h,X1)
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ( multiply(f,sK1(f,X0),sK0(sK1(h,X1))) = sK1(f,X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1323,c_711]) ).
tcf(c_3801,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(h,X3,multiply(h,phi(multiply(f,X0,X1)),X2)) = X3 )
| ~ left_zero(h,X3)
| ~ group_member(X2,h)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1925]) ).
tcf(c_3802,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,multiply(h,phi(sK0(X0)),X1)) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1925]) ).
tcf(c_3803,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(f,X0)
| ( multiply(h,X2,multiply(h,phi(sK1(f,X0)),X1)) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1925]) ).
tcf(c_3804,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,multiply(h,phi(f_left_zero),X0)) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_485,c_1925]) ).
tcf(c_3837,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(f,X3,multiply(f,sK0(X2),multiply(f,X0,X1))) = X3 )
| ~ left_zero(f,X3)
| ~ group_member(X2,h)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1926]) ).
tcf(c_3838,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,sK0(X1),sK0(X0))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1926]) ).
tcf(c_3839,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(f,X0)
| ( multiply(f,X2,multiply(f,sK0(X1),sK1(f,X0))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1926]) ).
tcf(c_3840,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,sK0(X0),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_485,c_1926]) ).
tcf(c_3903,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,sK0(multiply(h,X0,X1)),f_left_zero)) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_3840]) ).
tcf(c_3904,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,sK0(phi(X0)),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_3840]) ).
tcf(c_3905,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,multiply(f,sK0(sK1(h,X0)),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_3840]) ).
tcf(c_3906,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,sK0(iPr_def_10),f_left_zero)) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_3840]) ).
tcf(c_3928,plain,
multiply(f,f_left_zero,multiply(f,sK0(iPr_def_10),f_left_zero)) = f_left_zero,
inference(superposition,[status(thm)],[c_59,c_3906]) ).
tcf(c_3929,plain,
! [X0: $i] :
( ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ( multiply(f,sK0(X0),multiply(f,sK0(iPr_def_10),f_left_zero)) = sK0(X0) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1080,c_3906]) ).
tcf(c_3930,plain,
! [X0: $i] :
( ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ( multiply(f,sK0(X0),multiply(f,sK0(iPr_def_10),f_left_zero)) = sK0(X0) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_2456,c_3906]) ).
tcf(c_3931,plain,
! [X0: $i] :
( ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ( multiply(f,sK0(X0),multiply(f,sK0(iPr_def_10),f_left_zero)) = sK0(X0) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1322,c_3906]) ).
tcf(c_3932,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ( multiply(f,sK1(f,X0),multiply(f,sK0(iPr_def_10),f_left_zero)) = sK1(f,X0) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1323,c_3906]) ).
tcf(c_3957,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,sK0(phi(multiply(f,X0,X1))),f_left_zero)) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_3904]) ).
tcf(c_3958,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,sK0(phi(sK0(X0))),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_3904]) ).
tcf(c_3959,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,multiply(f,sK0(phi(sK1(f,X0))),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_3904]) ).
tcf(c_3960,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,sK0(phi(f_left_zero)),f_left_zero)) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_3904]) ).
tcf(c_4004,plain,
( left_zero(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10)))
| ( multiply(f,f_left_zero,sK0(sK1(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10))))) = f_left_zero )
| ~ group_member(multiply(h,iPr_def_10,sK1(h,iPr_def_10)),h) ),
inference(superposition,[status(thm)],[c_53,c_3690]) ).
tcf(c_4014,plain,
( left_zero(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10)))
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10))))))) = f_left_zero )
| ~ group_member(multiply(h,iPr_def_10,sK1(h,iPr_def_10)),h) ),
inference(superposition,[status(thm)],[c_53,c_3694]) ).
tcf(c_4024,plain,
( left_zero(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10)))
| ( phi(sK0(sK1(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10))))) = sK1(h,multiply(h,iPr_def_10,sK1(h,iPr_def_10))) )
| ~ group_member(multiply(h,iPr_def_10,sK1(h,iPr_def_10)),h) ),
inference(superposition,[status(thm)],[c_53,c_3698]) ).
tcf(c_4034,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,sK0(phi(sK0(multiply(h,X0,X1)))),f_left_zero)) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_3958]) ).
tcf(c_4035,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,sK0(phi(sK0(phi(X0)))),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_3958]) ).
tcf(c_4036,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,multiply(f,sK0(phi(sK0(sK1(h,X0)))),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_3958]) ).
tcf(c_4037,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,sK0(phi(sK0(iPr_def_10))),f_left_zero)) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_3958]) ).
tcf(c_4059,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,sK0(phi(sK0(phi(multiply(f,X0,X1))))),f_left_zero)) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_4035]) ).
tcf(c_4060,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,sK0(phi(sK0(phi(sK0(X0))))),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_4035]) ).
tcf(c_4061,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,multiply(f,sK0(phi(sK0(phi(sK1(f,X0))))),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_4035]) ).
tcf(c_4062,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,sK0(phi(sK0(phi(f_left_zero)))),f_left_zero)) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_4035]) ).
tcf(c_4085,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(h,multiply(h,phi(multiply(f,X0,X1)),X2),X3) = multiply(h,phi(multiply(f,X0,X1)),multiply(h,X2,X3)) )
| ~ group_member(X3,h)
| ~ group_member(X2,h)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_767]) ).
tcf(c_4086,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,multiply(h,phi(sK0(X0)),X1),X2) = multiply(h,phi(sK0(X0)),multiply(h,X1,X2)) )
| ~ group_member(X2,h)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_767]) ).
tcf(c_4087,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(f,X0)
| ( multiply(h,multiply(h,phi(sK1(f,X0)),X1),X2) = multiply(h,phi(sK1(f,X0)),multiply(h,X1,X2)) )
| ~ group_member(X2,h)
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_767]) ).
tcf(c_4088,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,multiply(h,phi(f_left_zero),X0),X1) = multiply(h,phi(f_left_zero),multiply(h,X0,X1)) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_485,c_767]) ).
tcf(c_4121,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,X0))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_59,c_1994]) ).
tcf(c_4122,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ( multiply(f,sK0(X0),multiply(f,f_left_zero,sK1(f,X1))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1080,c_1994]) ).
tcf(c_4123,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ( multiply(f,sK0(X0),multiply(f,f_left_zero,sK1(f,X1))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_2456,c_1994]) ).
tcf(c_4124,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ( multiply(f,sK0(X0),multiply(f,f_left_zero,sK1(f,X1))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1322,c_1994]) ).
tcf(c_4125,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| left_zero(f,X0)
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ( multiply(f,sK1(f,X0),multiply(f,f_left_zero,sK1(f,X1))) = sK1(f,X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1323,c_1994]) ).
tcf(c_4175,plain,
! [X0: $i,X1: $i] :
( left_zero(f,multiply(f,X0,X1))
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,multiply(f,X0,X1)))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_4121]) ).
tcf(c_4176,plain,
! [X0: $i] :
( left_zero(f,sK0(X0))
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_4121]) ).
tcf(c_4177,plain,
! [X0: $i] :
( left_zero(f,X0)
| left_zero(f,sK1(f,X0))
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK1(f,X0)))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_4121]) ).
tcf(c_4216,plain,
! [X0: $i] :
( group_member(sK0(X0),f)
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_4176,c_57]) ).
tcf(c_4217,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,sK0(X0),sK1(f,X1)) = sK0(X0) )
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_4176,c_564]) ).
tcf(c_4218,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),multiply(f,sK0(iPr_def_10),f_left_zero)) = sK0(X0) )
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_4176,c_3906]) ).
tcf(c_4219,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),sK0(iPr_def_10)) = sK0(X0) )
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_4176,c_712]) ).
tcf(c_4220,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),f_left_zero) = sK0(X0) )
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_4176,c_565]) ).
tcf(c_4221,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ( multiply(f,sK0(X0),multiply(f,f_left_zero,sK1(f,X1))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_4176,c_1994]) ).
tcf(c_4222,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ( multiply(f,sK0(X0),sK0(phi(sK0(sK1(h,X1))))) = sK0(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_4176,c_1056]) ).
tcf(c_4223,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,sK0(X0),sK0(phi(sK1(f,X1)))) = sK0(X0) )
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_4176,c_921]) ).
tcf(c_4224,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,sK0(X0),sK0(sK1(h,X1))) = sK0(X0) )
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_4176,c_711]) ).
tcf(c_4311,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,sK0(multiply(h,X0,X1)),f_left_zero) = sK0(multiply(h,X0,X1)) )
| ( multiply(f,f_left_zero,sK1(f,sK0(multiply(h,X0,X1)))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1365]) ).
tcf(c_4312,plain,
! [X0: $i] :
( ( multiply(f,sK0(phi(X0)),f_left_zero) = sK0(phi(X0)) )
| ( multiply(f,f_left_zero,sK1(f,sK0(phi(X0)))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1365]) ).
tcf(c_4313,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(f,sK0(sK1(h,X0)),f_left_zero) = sK0(sK1(h,X0)) )
| ( multiply(f,f_left_zero,sK1(f,sK0(sK1(h,X0)))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1365]) ).
tcf(c_4314,plain,
( ( multiply(f,sK0(iPr_def_10),f_left_zero) = sK0(iPr_def_10) )
| ( multiply(f,f_left_zero,sK1(f,sK0(iPr_def_10))) = f_left_zero ) ),
inference(superposition,[status(thm)],[c_491,c_1365]) ).
tcf(c_4353,plain,
! [X0: $i,X1: $i] :
( left_zero(f,multiply(f,X0,X1))
| ( multiply(h,phi(sK1(f,multiply(f,X0,X1))),iPr_def_10) = phi(multiply(f,sK1(f,multiply(f,X0,X1)),f_left_zero)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_1636]) ).
tcf(c_4354,plain,
! [X0: $i] :
( left_zero(f,sK0(X0))
| ( multiply(h,phi(sK1(f,sK0(X0))),iPr_def_10) = phi(multiply(f,sK1(f,sK0(X0)),f_left_zero)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_1636]) ).
tcf(c_4355,plain,
! [X0: $i] :
( left_zero(f,X0)
| left_zero(f,sK1(f,X0))
| ( multiply(h,phi(sK1(f,sK1(f,X0))),iPr_def_10) = phi(multiply(f,sK1(f,sK1(f,X0)),f_left_zero)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_1636]) ).
tcf(c_4396,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(X0)))))) = f_left_zero )
| ( multiply(h,phi(X0),multiply(h,iPr_def_10,sK1(h,X1))) = phi(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_3547,c_2022]) ).
tcf(c_4397,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(X0)))) = f_left_zero )
| ( multiply(h,phi(X0),multiply(h,iPr_def_10,sK1(h,X1))) = phi(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1761,c_2022]) ).
tcf(c_4398,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( phi(sK0(sK1(h,phi(X0)))) = sK1(h,phi(X0)) )
| ( multiply(h,phi(X0),multiply(h,iPr_def_10,sK1(h,X1))) = phi(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_832,c_2022]) ).
tcf(c_4423,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(phi(sK0(phi(sK0(phi(sK0(multiply(h,X0,X1)))))))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_2775]) ).
tcf(c_4424,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(phi(sK0(phi(sK0(phi(sK0(phi(X0)))))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_2775]) ).
tcf(c_4425,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,phi(sK0(phi(sK0(phi(sK0(phi(sK0(sK1(h,X0)))))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_2775]) ).
tcf(c_4426,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(phi(sK0(phi(sK0(phi(sK0(iPr_def_10))))))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_2775]) ).
tcf(c_4447,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(sK0(phi(sK0(phi(sK0(phi(multiply(f,X0,X1)))))))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_2842]) ).
tcf(c_4448,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(sK0(phi(sK0(phi(sK0(phi(sK0(X0)))))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_2842]) ).
tcf(c_4449,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,sK0(phi(sK0(phi(sK0(phi(sK0(phi(sK1(f,X0)))))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_2842]) ).
tcf(c_4450,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(sK0(phi(sK0(phi(sK0(phi(f_left_zero))))))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_2842]) ).
tcf(c_4471,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,f_left_zero,sK0(phi(sK0(phi(sK0(multiply(h,X0,X1)))))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_2867]) ).
tcf(c_4472,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,f_left_zero,sK0(phi(sK0(phi(sK0(phi(X0)))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_2867]) ).
tcf(c_4473,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,multiply(f,f_left_zero,sK0(phi(sK0(phi(sK0(sK1(h,X0)))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_2867]) ).
tcf(c_4474,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,f_left_zero,sK0(phi(sK0(phi(sK0(iPr_def_10))))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_2867]) ).
tcf(c_4513,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,multiply(h,iPr_def_10,phi(sK0(phi(sK0(phi(multiply(f,X0,X1)))))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_2894]) ).
tcf(c_4514,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,multiply(h,iPr_def_10,phi(sK0(phi(sK0(phi(sK0(X0)))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_2894]) ).
tcf(c_4515,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,multiply(h,iPr_def_10,phi(sK0(phi(sK0(phi(sK1(f,X0)))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_2894]) ).
tcf(c_4516,plain,
! [X0: $i] :
( ( multiply(h,X0,multiply(h,iPr_def_10,phi(sK0(phi(sK0(phi(f_left_zero))))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_2894]) ).
tcf(c_4538,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(multiply(f,f_left_zero,sK0(phi(sK0(phi(multiply(f,X0,X1)))))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_3192]) ).
tcf(c_4539,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(multiply(f,f_left_zero,sK0(phi(sK0(phi(sK0(X0)))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_3192]) ).
tcf(c_4540,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,phi(multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,X0)))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_3192]) ).
tcf(c_4541,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(multiply(f,f_left_zero,sK0(phi(sK0(phi(f_left_zero))))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_3192]) ).
tcf(c_4567,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(multiply(h,iPr_def_10,phi(sK0(phi(sK0(multiply(h,X0,X1)))))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_3480]) ).
tcf(c_4568,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(multiply(h,iPr_def_10,phi(sK0(phi(sK0(phi(X0)))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_3480]) ).
tcf(c_4569,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,sK0(multiply(h,iPr_def_10,phi(sK0(phi(sK0(sK1(h,X0)))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_3480]) ).
tcf(c_4570,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(multiply(h,iPr_def_10,phi(sK0(phi(sK0(iPr_def_10))))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_3480]) ).
tcf(c_4606,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,multiply(f,sK0(phi(sK0(phi(sK0(multiply(h,X0,X1)))))),f_left_zero)) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_4060]) ).
tcf(c_4607,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,multiply(f,sK0(phi(sK0(phi(sK0(phi(X0)))))),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_4060]) ).
tcf(c_4608,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,multiply(f,sK0(phi(sK0(phi(sK0(sK1(h,X0)))))),f_left_zero)) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_4060]) ).
tcf(c_4609,plain,
! [X0: $i] :
( ( multiply(f,X0,multiply(f,sK0(phi(sK0(phi(sK0(iPr_def_10))))),f_left_zero)) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_4060]) ).
tcf(c_4654,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(f,multiply(f,sK0(X2),multiply(f,X0,X1)),X3) = multiply(f,sK0(X2),multiply(f,multiply(f,X0,X1),X3)) )
| ~ group_member(X3,f)
| ~ group_member(X2,h)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_768]) ).
tcf(c_4655,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,multiply(f,sK0(X1),sK0(X0)),X2) = multiply(f,sK0(X1),multiply(f,sK0(X0),X2)) )
| ~ group_member(X2,f)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_768]) ).
tcf(c_4656,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(f,X0)
| ( multiply(f,multiply(f,sK0(X1),sK1(f,X0)),X2) = multiply(f,sK0(X1),multiply(f,sK1(f,X0),X2)) )
| ~ group_member(X2,f)
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_768]) ).
tcf(c_4657,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,multiply(f,sK0(X0),f_left_zero),X1) = multiply(f,sK0(X0),multiply(f,f_left_zero,X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_485,c_768]) ).
tcf(c_4685,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,multiply(f,f_left_zero,multiply(f,X0,X1)),X2) = multiply(f,f_left_zero,multiply(f,multiply(f,X0,X1),X2)) )
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_770]) ).
tcf(c_4686,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,multiply(f,f_left_zero,sK0(X0)),X1) = multiply(f,f_left_zero,multiply(f,sK0(X0),X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_770]) ).
tcf(c_4687,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,multiply(f,f_left_zero,sK1(f,X0)),X1) = multiply(f,f_left_zero,multiply(f,sK1(f,X0),X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_770]) ).
tcf(c_4688,plain,
! [X0: $i] :
( ( multiply(f,multiply(f,f_left_zero,f_left_zero),X0) = multiply(f,f_left_zero,multiply(f,f_left_zero,X0)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_770]) ).
tcf(c_4689,plain,
! [X0: $i] :
( ( multiply(f,f_left_zero,multiply(f,f_left_zero,X0)) = multiply(f,f_left_zero,X0) )
| ~ group_member(X0,f) ),
inference(light_normalisation,[status(thm)],[c_4688,c_595]) ).
tcf(c_4713,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,multiply(h,iPr_def_10,multiply(h,X0,X1)),X2) = multiply(h,iPr_def_10,multiply(h,multiply(h,X0,X1),X2)) )
| ~ group_member(X2,h)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_771]) ).
tcf(c_4714,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,multiply(h,iPr_def_10,phi(X0)),X1) = multiply(h,iPr_def_10,multiply(h,phi(X0),X1)) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_771]) ).
tcf(c_4715,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,multiply(h,iPr_def_10,sK1(h,X0)),X1) = multiply(h,iPr_def_10,multiply(h,sK1(h,X0),X1)) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_771]) ).
tcf(c_4716,plain,
! [X0: $i] :
( ( multiply(h,multiply(h,iPr_def_10,iPr_def_10),X0) = multiply(h,iPr_def_10,multiply(h,iPr_def_10,X0)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_491,c_771]) ).
tcf(c_4717,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,X0)) = multiply(h,iPr_def_10,X0) )
| ~ group_member(X0,h) ),
inference(light_normalisation,[status(thm)],[c_4716,c_665]) ).
tcf(c_4764,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(h,X3,phi(sK0(multiply(h,multiply(h,X0,X1),X2)))) = X3 )
| ~ left_zero(h,X3)
| ~ group_member(X2,h)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_882]) ).
tcf(c_4765,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(multiply(h,phi(X0),X1)))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_882]) ).
tcf(c_4766,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(h,X0)
| ( multiply(h,X2,phi(sK0(multiply(h,sK1(h,X0),X1)))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_882]) ).
tcf(c_4767,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(multiply(h,iPr_def_10,X0)))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_491,c_882]) ).
tcf(c_4820,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(f,X3,sK0(phi(multiply(f,multiply(f,X0,X1),X2)))) = X3 )
| ~ left_zero(f,X3)
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_919]) ).
tcf(c_4821,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(multiply(f,sK0(X0),X1)))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_919]) ).
tcf(c_4822,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(f,X0)
| ( multiply(f,X2,sK0(phi(multiply(f,sK1(f,X0),X1)))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_919]) ).
tcf(c_4823,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(multiply(f,f_left_zero,X0)))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_919]) ).
tcf(c_4848,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,f_left_zero,multiply(f,f_left_zero,multiply(f,X0,X1))) = multiply(f,f_left_zero,multiply(f,X0,X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_4689]) ).
tcf(c_4849,plain,
! [X0: $i] :
( ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(X0))) = multiply(f,f_left_zero,sK0(X0)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_4689]) ).
tcf(c_4850,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,X0))) = multiply(f,f_left_zero,sK1(f,X0)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_4689]) ).
tcf(c_4851,plain,
multiply(f,f_left_zero,multiply(f,f_left_zero,f_left_zero)) = multiply(f,f_left_zero,f_left_zero),
inference(superposition,[status(thm)],[c_485,c_4689]) ).
tcf(c_4877,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,multiply(h,X0,X1))) = multiply(h,iPr_def_10,multiply(h,X0,X1)) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_4717]) ).
tcf(c_4878,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(X0))) = multiply(h,iPr_def_10,phi(X0)) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_4717]) ).
tcf(c_4879,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,sK1(h,X0))) = multiply(h,iPr_def_10,sK1(h,X0)) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_4717]) ).
tcf(c_4880,plain,
multiply(h,iPr_def_10,multiply(h,iPr_def_10,iPr_def_10)) = multiply(h,iPr_def_10,iPr_def_10),
inference(superposition,[status(thm)],[c_491,c_4717]) ).
tcf(c_4897,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(multiply(h,X0,X1)))) = multiply(f,f_left_zero,sK0(multiply(h,X0,X1))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_4849]) ).
tcf(c_4898,plain,
! [X0: $i] :
( ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(phi(X0)))) = multiply(f,f_left_zero,sK0(phi(X0))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_4849]) ).
tcf(c_4899,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(sK1(h,X0)))) = multiply(f,f_left_zero,sK0(sK1(h,X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_4849]) ).
tcf(c_4900,plain,
multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(iPr_def_10))) = multiply(f,f_left_zero,sK0(iPr_def_10)),
inference(superposition,[status(thm)],[c_491,c_4849]) ).
tcf(c_4934,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(multiply(f,X0,X1)))) = multiply(h,iPr_def_10,phi(multiply(f,X0,X1))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_4878]) ).
tcf(c_4935,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(sK0(X0)))) = multiply(h,iPr_def_10,phi(sK0(X0))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_4878]) ).
tcf(c_4936,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(sK1(f,X0)))) = multiply(h,iPr_def_10,phi(sK1(f,X0))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_4878]) ).
tcf(c_4937,plain,
multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(f_left_zero))) = multiply(h,iPr_def_10,phi(f_left_zero)),
inference(superposition,[status(thm)],[c_485,c_4878]) ).
tcf(c_4956,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(multiply(h,iPr_def_10,multiply(h,X0,X1))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_4767]) ).
tcf(c_4957,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(multiply(h,iPr_def_10,phi(X0))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_4767]) ).
tcf(c_4958,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,phi(sK0(multiply(h,iPr_def_10,sK1(h,X0))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_4767]) ).
tcf(c_4959,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(multiply(h,iPr_def_10,iPr_def_10)))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_4767]) ).
tcf(c_4989,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(multiply(f,f_left_zero,multiply(f,X0,X1))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_4823]) ).
tcf(c_4990,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(multiply(f,f_left_zero,sK0(X0))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_4823]) ).
tcf(c_4991,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,sK0(phi(multiply(f,f_left_zero,sK1(f,X0))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_4823]) ).
tcf(c_4992,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(multiply(f,f_left_zero,f_left_zero)))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_4823]) ).
tcf(c_5011,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(phi(multiply(f,X0,X1))))) = multiply(f,f_left_zero,sK0(phi(multiply(f,X0,X1)))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_4898]) ).
tcf(c_5012,plain,
! [X0: $i] :
( ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(phi(sK0(X0))))) = multiply(f,f_left_zero,sK0(phi(sK0(X0)))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_4898]) ).
tcf(c_5013,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(phi(sK1(f,X0))))) = multiply(f,f_left_zero,sK0(phi(sK1(f,X0)))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_4898]) ).
tcf(c_5014,plain,
multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(phi(f_left_zero)))) = multiply(f,f_left_zero,sK0(phi(f_left_zero))),
inference(superposition,[status(thm)],[c_485,c_4898]) ).
tcf(c_5031,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(sK0(multiply(h,X0,X1))))) = multiply(h,iPr_def_10,phi(sK0(multiply(h,X0,X1)))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_4935]) ).
tcf(c_5032,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(sK0(phi(X0))))) = multiply(h,iPr_def_10,phi(sK0(phi(X0)))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_4935]) ).
tcf(c_5033,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(sK0(sK1(h,X0))))) = multiply(h,iPr_def_10,phi(sK0(sK1(h,X0)))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_4935]) ).
tcf(c_5034,plain,
multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(sK0(iPr_def_10)))) = multiply(h,iPr_def_10,phi(sK0(iPr_def_10))),
inference(superposition,[status(thm)],[c_491,c_4935]) ).
tcf(c_5058,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(multiply(h,iPr_def_10,phi(multiply(f,X0,X1)))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_4957]) ).
tcf(c_5059,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(multiply(h,iPr_def_10,phi(sK0(X0)))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_4957]) ).
tcf(c_5060,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,phi(sK0(multiply(h,iPr_def_10,phi(sK1(f,X0)))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_4957]) ).
tcf(c_5061,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(multiply(h,iPr_def_10,phi(f_left_zero))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_4957]) ).
tcf(c_5125,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(multiply(f,f_left_zero,sK0(multiply(h,X0,X1)))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_4990]) ).
tcf(c_5126,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(multiply(f,f_left_zero,sK0(phi(X0)))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_4990]) ).
tcf(c_5127,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,sK0(phi(multiply(f,f_left_zero,sK0(sK1(h,X0)))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_4990]) ).
tcf(c_5128,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(multiply(f,f_left_zero,sK0(iPr_def_10))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_4990]) ).
tcf(c_5150,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(multiply(h,iPr_def_10,phi(sK0(multiply(h,X0,X1))))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_5059]) ).
tcf(c_5151,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(multiply(h,iPr_def_10,phi(sK0(phi(X0))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_5059]) ).
tcf(c_5152,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,X1,phi(sK0(multiply(h,iPr_def_10,phi(sK0(sK1(h,X0))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_5059]) ).
tcf(c_5153,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(multiply(h,iPr_def_10,phi(sK0(iPr_def_10)))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_491,c_5059]) ).
tcf(c_5174,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(multiply(f,f_left_zero,sK0(phi(multiply(f,X0,X1))))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_5126]) ).
tcf(c_5175,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(multiply(f,f_left_zero,sK0(phi(sK0(X0))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_5126]) ).
tcf(c_5176,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,X1,sK0(phi(multiply(f,f_left_zero,sK0(phi(sK1(f,X0))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_5126]) ).
tcf(c_5177,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(multiply(f,f_left_zero,sK0(phi(f_left_zero)))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_485,c_5126]) ).
tcf(c_5202,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( left_zero(X1,X3)
| ( multiply(X1,multiply(X1,sK1(X1,X3),multiply(X1,X0,X2)),X4) = multiply(X1,sK1(X1,X3),multiply(X1,multiply(X1,X0,X2),X4)) )
| ~ group_member(X4,X1)
| ~ group_member(X3,X1)
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(superposition,[status(thm)],[c_49,c_769]) ).
tcf(c_5203,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(h,X1)
| ( multiply(h,multiply(h,sK1(h,X1),phi(X0)),X2) = multiply(h,sK1(h,X1),multiply(h,phi(X0),X2)) )
| ~ group_member(X2,h)
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_769]) ).
tcf(c_5204,plain,
! [X0: $i,X1: $i,X2: $i] :
( left_zero(f,X1)
| ( multiply(f,multiply(f,sK1(f,X1),sK0(X0)),X2) = multiply(f,sK1(f,X1),multiply(f,sK0(X0),X2)) )
| ~ group_member(X2,f)
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_769]) ).
tcf(c_5205,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( left_zero(X1,X2)
| left_zero(X1,X0)
| ( multiply(X1,multiply(X1,sK1(X1,X2),sK1(X1,X0)),X3) = multiply(X1,sK1(X1,X2),multiply(X1,sK1(X1,X0),X3)) )
| ~ group_member(X3,X1)
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(superposition,[status(thm)],[c_56,c_769]) ).
tcf(c_5206,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(f,multiply(f,sK1(f,X0),f_left_zero),X1) = multiply(f,sK1(f,X0),multiply(f,f_left_zero,X1)) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_485,c_769]) ).
tcf(c_5207,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(h,multiply(h,sK1(h,X0),iPr_def_10),X1) = multiply(h,sK1(h,X0),multiply(h,iPr_def_10,X1)) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_491,c_769]) ).
tcf(c_5257,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(phi(sK0(multiply(h,X0,X1)))))) = multiply(f,f_left_zero,sK0(phi(sK0(multiply(h,X0,X1))))) )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_5012]) ).
tcf(c_5258,plain,
! [X0: $i] :
( ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(phi(sK0(phi(X0)))))) = multiply(f,f_left_zero,sK0(phi(sK0(phi(X0))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_5012]) ).
tcf(c_5259,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,X0)))))) = multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,X0))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_5012]) ).
tcf(c_5260,plain,
multiply(f,f_left_zero,multiply(f,f_left_zero,sK0(phi(sK0(iPr_def_10))))) = multiply(f,f_left_zero,sK0(phi(sK0(iPr_def_10)))),
inference(superposition,[status(thm)],[c_491,c_5012]) ).
tcf(c_5287,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(sK0(phi(multiply(f,X0,X1)))))) = multiply(h,iPr_def_10,phi(sK0(phi(multiply(f,X0,X1))))) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_5032]) ).
tcf(c_5288,plain,
! [X0: $i] :
( ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(sK0(phi(sK0(X0)))))) = multiply(h,iPr_def_10,phi(sK0(phi(sK0(X0))))) )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_5032]) ).
tcf(c_5289,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(sK0(phi(sK1(f,X0)))))) = multiply(h,iPr_def_10,phi(sK0(phi(sK1(f,X0))))) )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_5032]) ).
tcf(c_5290,plain,
multiply(h,iPr_def_10,multiply(h,iPr_def_10,phi(sK0(phi(f_left_zero))))) = multiply(h,iPr_def_10,phi(sK0(phi(f_left_zero)))),
inference(superposition,[status(thm)],[c_485,c_5032]) ).
tcf(c_5326,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(h,X2,phi(sK0(multiply(h,iPr_def_10,phi(sK0(phi(multiply(f,X0,X1)))))))) = X2 )
| ~ left_zero(h,X2)
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_5151]) ).
tcf(c_5327,plain,
! [X0: $i,X1: $i] :
( ( multiply(h,X1,phi(sK0(multiply(h,iPr_def_10,phi(sK0(phi(sK0(X0)))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_5151]) ).
tcf(c_5328,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X0)
| ( multiply(h,X1,phi(sK0(multiply(h,iPr_def_10,phi(sK0(phi(sK1(f,X0)))))))) = X1 )
| ~ left_zero(h,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_5151]) ).
tcf(c_5329,plain,
! [X0: $i] :
( ( multiply(h,X0,phi(sK0(multiply(h,iPr_def_10,phi(sK0(phi(f_left_zero))))))) = X0 )
| ~ left_zero(h,X0) ),
inference(superposition,[status(thm)],[c_485,c_5151]) ).
tcf(c_5363,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(f,X2,sK0(phi(multiply(f,f_left_zero,sK0(phi(sK0(multiply(h,X0,X1)))))))) = X2 )
| ~ left_zero(f,X2)
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_5175]) ).
tcf(c_5364,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,X1,sK0(phi(multiply(f,f_left_zero,sK0(phi(sK0(phi(X0)))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_5175]) ).
tcf(c_5365,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X0)
| ( multiply(f,X1,sK0(phi(multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,X0)))))))) = X1 )
| ~ left_zero(f,X1)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_5175]) ).
tcf(c_5366,plain,
! [X0: $i] :
( ( multiply(f,X0,sK0(phi(multiply(f,f_left_zero,sK0(phi(sK0(iPr_def_10))))))) = X0 )
| ~ left_zero(f,X0) ),
inference(superposition,[status(thm)],[c_491,c_5175]) ).
tcf(c_5390,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,f_left_zero,sK0(phi(sK0(sK1(h,phi(X0)))))) = f_left_zero )
| ( multiply(h,phi(X0),phi(sK0(phi(sK0(sK1(h,X1)))))) = phi(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_3547,c_1105]) ).
tcf(c_5391,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,f_left_zero,sK0(sK1(h,phi(X0)))) = f_left_zero )
| ( multiply(h,phi(X0),phi(sK0(phi(sK0(sK1(h,X1)))))) = phi(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1761,c_1105]) ).
tcf(c_5392,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( phi(sK0(sK1(h,phi(X0)))) = sK1(h,phi(X0)) )
| ( multiply(h,phi(X0),phi(sK0(phi(sK0(sK1(h,X1)))))) = phi(X0) )
| ~ group_member(X1,h)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_832,c_1105]) ).
tcf(c_5436,plain,
! [X0: $i] :
( left_zero(f,X0)
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,X0)))))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_59,c_1144]) ).
tcf(c_5437,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,multiply(f,f_left_zero,sK1(f,sK0(X0)))) = f_left_zero )
| ( multiply(f,sK0(X0),sK0(phi(sK0(phi(sK1(f,X1)))))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_4176,c_1144]) ).
tcf(c_5438,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( phi(sK0(phi(sK1(f,sK0(X0))))) = phi(sK1(f,sK0(X0))) )
| ( multiply(f,sK0(X0),sK0(phi(sK0(phi(sK1(f,X1)))))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1080,c_1144]) ).
tcf(c_5439,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK0(phi(sK1(f,sK0(X0))))) = f_left_zero )
| ( multiply(f,sK0(X0),sK0(phi(sK0(phi(sK1(f,X1)))))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_2456,c_1144]) ).
tcf(c_5440,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK1(f,sK0(X0))) = f_left_zero )
| ( multiply(f,sK0(X0),sK0(phi(sK0(phi(sK1(f,X1)))))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_1322,c_1144]) ).
tcf(c_5441,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| left_zero(f,X0)
| ( multiply(f,f_left_zero,sK1(f,sK1(f,X0))) = f_left_zero )
| ( multiply(f,sK1(f,X0),sK0(phi(sK0(phi(sK1(f,X1)))))) = sK1(f,X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_1323,c_1144]) ).
tcf(c_5495,plain,
! [X0: $i,X1: $i] :
( left_zero(f,multiply(f,X0,X1))
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,multiply(f,X0,X1))))))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_49,c_5436]) ).
tcf(c_5496,plain,
! [X0: $i] :
( left_zero(f,sK0(X0))
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_53,c_5436]) ).
tcf(c_5497,plain,
! [X0: $i] :
( left_zero(f,X0)
| left_zero(f,sK1(f,X0))
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK1(f,X0))))))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_56,c_5436]) ).
tcf(c_5519,plain,
! [X0: $i] :
( group_member(sK0(X0),f)
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_5496,c_57]) ).
tcf(c_5520,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,sK0(X0),sK1(f,X1)) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_5496,c_564]) ).
tcf(c_5521,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),multiply(f,sK0(iPr_def_10),f_left_zero)) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_5496,c_3906]) ).
tcf(c_5522,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),sK0(iPr_def_10)) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_5496,c_712]) ).
tcf(c_5523,plain,
! [X0: $i] :
( ( multiply(f,sK0(X0),f_left_zero) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_5496,c_565]) ).
tcf(c_5524,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ( multiply(f,sK0(X0),sK0(phi(sK0(phi(sK1(f,X1)))))) = sK0(X0) )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_5496,c_1144]) ).
tcf(c_5525,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,sK0(X0),multiply(f,f_left_zero,sK1(f,X1))) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_5496,c_1994]) ).
tcf(c_5526,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,sK0(X0),sK0(phi(sK0(sK1(h,X1))))) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_5496,c_1056]) ).
tcf(c_5527,plain,
! [X0: $i,X1: $i] :
( left_zero(f,X1)
| ( multiply(f,sK0(X0),sK0(phi(sK1(f,X1)))) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ~ group_member(X1,f)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_5496,c_921]) ).
tcf(c_5528,plain,
! [X0: $i,X1: $i] :
( left_zero(h,X1)
| ( multiply(f,sK0(X0),sK0(sK1(h,X1))) = sK0(X0) )
| ( multiply(f,f_left_zero,sK0(phi(sK0(phi(sK1(f,sK0(X0))))))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_5496,c_711]) ).
tcf(c_5643,plain,
! [X0: $i,X1: $i] :
( ( multiply(f,sK0(multiply(h,X0,X1)),sK0(iPr_def_10)) = sK0(multiply(h,X0,X1)) )
| ( multiply(f,f_left_zero,sK1(f,sK0(multiply(h,X0,X1)))) = f_left_zero )
| ~ group_member(X1,h)
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_49,c_1364]) ).
tcf(c_5644,plain,
! [X0: $i] :
( ( multiply(f,sK0(phi(X0)),sK0(iPr_def_10)) = sK0(phi(X0)) )
| ( multiply(f,f_left_zero,sK1(f,sK0(phi(X0)))) = f_left_zero )
| ~ group_member(X0,f) ),
inference(superposition,[status(thm)],[c_51,c_1364]) ).
tcf(c_5645,plain,
! [X0: $i] :
( left_zero(h,X0)
| ( multiply(f,sK0(sK1(h,X0)),sK0(iPr_def_10)) = sK0(sK1(h,X0)) )
| ( multiply(f,f_left_zero,sK1(f,sK0(sK1(h,X0)))) = f_left_zero )
| ~ group_member(X0,h) ),
inference(superposition,[status(thm)],[c_56,c_1364]) ).
tcf(c_5646,plain,
( ( multiply(f,sK0(iPr_def_10),sK0(iPr_def_10)) = sK0(iPr_def_10) )
| ( multiply(f,f_left_zero,sK1(f,sK0(iPr_def_10))) = f_left_zero ) ),
inference(superposition,[status(thm)],[c_491,c_1364]) ).
tcf(c_5673,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_5646,c_5645,c_5644,c_5643,c_5528,c_5527,c_5526,c_5525,c_5524,c_5523,c_5522,c_5521,c_5520,c_5519,c_5497,c_5496,c_5495,c_5441,c_5440,c_5439,c_5438,c_5437,c_5436,c_5392,c_5391,c_5390,c_5366,c_5365,c_5364,c_5363,c_5329,c_5328,c_5327,c_5326,c_5290,c_5289,c_5288,c_5287,c_5260,c_5259,c_5258,c_5257,c_5207,c_5206,c_5205,c_5204,c_5203,c_5202,c_5177,c_5176,c_5175,c_5174,c_5153,c_5152,c_5151,c_5150,c_5128,c_5127,c_5126,c_5125,c_5061,c_5060,c_5059,c_5058,c_5034,c_5033,c_5032,c_5031,c_5014,c_5013,c_5012,c_5011,c_4992,c_4991,c_4990,c_4989,c_4959,c_4958,c_4957,c_4956,c_4937,c_4936,c_4935,c_4934,c_4900,c_4899,c_4898,c_4897,c_4880,c_4879,c_4878,c_4877,c_4851,c_4850,c_4849,c_4848,c_4823,c_4822,c_4821,c_4820,c_4767,c_4766,c_4765,c_4764,c_4717,c_4716,c_4715,c_4714,c_4713,c_4689,c_4688,c_4687,c_4686,c_4685,c_4657,c_4656,c_4655,c_4654,c_4609,c_4608,c_4607,c_4606,c_4570,c_4569,c_4568,c_4567,c_4541,c_4540,c_4539,c_4538,c_4516,c_4515,c_4514,c_4513,c_4474,c_4473,c_4472,c_4471,c_4450,c_4449,c_4448,c_4447,c_4426,c_4425,c_4424,c_4423,c_4398,c_4397,c_4396,c_4355,c_4354,c_4353,c_4314,c_4313,c_4312,c_4311,c_4224,c_4223,c_4222,c_4221,c_4220,c_4219,c_4218,c_4217,c_4216,c_4177,c_4176,c_4175,c_4125,c_4124,c_4123,c_4122,c_4121,c_4088,c_4087,c_4086,c_4085,c_4062,c_4061,c_4060,c_4059,c_4037,c_4036,c_4035,c_4034,c_4024,c_4014,c_4004,c_3960,c_3959,c_3958,c_3957,c_3932,c_3931,c_3930,c_3929,c_3928,c_3906,c_3905,c_3904,c_3903,c_3840,c_3839,c_3838,c_3837,c_3804,c_3803,c_3802,c_3801,c_3728,c_3727,c_3726,c_3725,c_3724,c_3723,c_3722,c_3698,c_3694,c_3690,c_3687,c_3686,c_3685,c_3684,c_3669,c_3668,c_3667,c_3666,c_3665,c_3653,c_3590,c_3580,c_3579,c_3578,c_3577,c_3576,c_3575,c_3574,c_3573,c_3572,c_3571,c_3549,c_3548,c_3547,c_3546,c_3508,c_3507,c_3506,c_3505,c_3482,c_3481,c_3480,c_3479,c_3423,c_3422,c_3421,c_3420,c_3400,c_3399,c_3398,c_3397,c_3376,c_3375,c_3374,c_3373,c_3329,c_3328,c_3327,c_3326,c_3307,c_3306,c_3282,c_3281,c_3280,c_3237,c_3236,c_3235,c_3234,c_3194,c_3193,c_3192,c_3191,c_3167,c_3166,c_3165,c_3164,c_3142,c_3141,c_3140,c_3139,c_3118,c_3117,c_3116,c_3115,c_3078,c_3077,c_3076,c_3075,c_3030,c_3029,c_3028,c_3027,c_2976,c_2975,c_2974,c_2955,c_2954,c_2953,c_2952,c_2933,c_2932,c_2931,c_2930,c_2896,c_2895,c_2894,c_2893,c_2869,c_2868,c_2867,c_2866,c_2844,c_2843,c_2842,c_2841,c_2800,c_2799,c_2798,c_2797,c_2777,c_2776,c_2775,c_2774,c_2755,c_2754,c_2753,c_2752,c_2714,c_2713,c_2712,c_2711,c_2694,c_2693,c_2692,c_2691,c_2665,c_2664,c_2663,c_2662,c_2621,c_2620,c_2619,c_2618,c_2598,c_2597,c_2596,c_2595,c_2559,c_2558,c_2557,c_2556,c_2555,c_2554,c_2484,c_2483,c_2482,c_2481,c_2480,c_2479,c_2457,c_2456,c_2455,c_2438,c_2437,c_2416,c_2415,c_2394,c_2393,c_2392,c_2391,c_2374,c_2373,c_2372,c_2371,c_2326,c_2325,c_2324,c_2323,c_2253,c_2252,c_2251,c_2250,c_2227,c_2226,c_2225,c_2224,c_2198,c_2197,c_2196,c_2195,c_2174,c_2173,c_2172,c_2171,c_2149,c_2148,c_2147,c_2146,c_2118,c_2117,c_2116,c_2115,c_2070,c_2069,c_2068,c_2067,c_2023,c_2022,c_2021,c_2020,c_1995,c_1994,c_1993,c_1992,c_1929,c_1928,c_1927,c_1926,c_1925,c_1924,c_1892,c_1891,c_1890,c_1889,c_1863,c_1862,c_1861,c_1860,c_1850,c_1820,c_1810,c_1809,c_1808,c_1807,c_1806,c_1805,c_1804,c_1803,c_1764,c_1763,c_1762,c_1761,c_1760,c_1743,c_1742,c_1727,c_1686,c_1685,c_1684,c_1683,c_1636,c_1635,c_1634,c_1633,c_1632,c_1611,c_1610,c_1609,c_1608,c_1591,c_1590,c_1589,c_1588,c_1557,c_1556,c_1555,c_1554,c_1530,c_1529,c_1528,c_1527,c_1483,c_1482,c_1481,c_1480,c_1462,c_1461,c_1460,c_1459,c_1446,c_1427,c_1418,c_1417,c_1416,c_1415,c_1414,c_1413,c_1412,c_1391,c_1390,c_1389,c_1388,c_1387,c_1365,c_1364,c_1363,c_1362,c_1323,c_1322,c_1321,c_1310,c_1289,c_1288,c_1287,c_1286,c_1234,c_1233,c_1232,c_1231,c_1230,c_1211,c_1210,c_1209,c_1208,c_1169,c_1168,c_1167,c_1166,c_1145,c_1144,c_1143,c_1142,c_1106,c_1105,c_1104,c_1103,c_1081,c_1080,c_1079,c_1057,c_1056,c_1055,c_1054,c_1003,c_1002,c_1001,c_1000,c_975,c_974,c_973,c_972,c_954,c_953,c_952,c_951,c_922,c_921,c_920,c_919,c_902,c_885,c_884,c_883,c_882,c_835,c_834,c_833,c_832,c_831,c_809,c_808,c_807,c_806,c_771,c_770,c_769,c_768,c_767,c_766,c_738,c_712,c_711,c_710,c_709,c_687,c_686,c_685,c_684,c_665,c_664,c_663,c_662,c_661,c_629,c_628,c_627,c_626,c_608,c_607,c_606,c_605,c_595,c_566,c_565,c_564,c_563,c_562,c_561,c_545,c_544,c_528,c_527,c_517,c_516,c_504,c_503,c_502,c_491,c_490,c_277,c_276,c_485,c_59,c_58,c_57,c_56,c_55,c_54,c_53,c_52,c_51,c_50,c_49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP194+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/0.29 % Computer : n012.cluster.edu
% 0.04/0.29 % Model : x86_64 x86_64
% 0.04/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.29 % Memory : 8046.5625MB
% 0.04/0.29 % OS : Linux 6.8.0-71-generic
% 0.04/0.29 % CPULimit : 300
% 0.04/0.29 % WCLimit : 300
% 0.04/0.29 % DateTime : Wed Sep 23 14:06:21 UTC 2026
% 0.04/0.29 % CPUTime :
% 0.04/0.29 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/0.31 Running first-order theorem proving
% 0.04/0.31 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/0.32
% 0.04/0.32 % ======== iProver multi-core TPTP/SMT =========
% 0.04/0.32
% 0.04/0.32 % Detected problem language: tptp
% 0.06/0.33 % Proving...
% 1.93/0.96 % SZS status Started for theBenchmark.p
% 1.93/0.96 % SZS status Theorem for theBenchmark.p
% 1.93/0.96
% 1.93/0.96 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.93/0.96
% 1.93/0.96 % ------ iProver source info
% 1.93/0.96
% 1.93/0.96 % git: date: 2026-07-19 20:42:38 +0200
% 1.93/0.96 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.93/0.96 % git: non_committed_changes: false
% 1.93/0.96
% 1.93/0.96 % ------ Parsing...
% 1.93/0.96 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.93/0.96
% 1.93/0.96 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 1.93/0.96
% 1.93/0.96 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 1.93/0.96
% 1.93/0.96 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 1.93/0.96 % ------ Proving...
% 1.93/0.96 % ------ Problem Properties
% 1.93/0.96
% 1.93/0.96 %
% 1.93/0.96 % clauses 13
% 1.93/0.96 % conjectures 1
% 1.93/0.96 % EPR 3
% 1.93/0.96 % Horn 12
% 1.93/0.96 % unary 3
% 1.93/0.96 % binary 4
% 1.93/0.96 % lits 30
% 1.93/0.96 % lits eq 6
% 1.93/0.96 % fd_pure 0
% 1.93/0.96 % fd_pseudo 0
% 1.93/0.96 % fd_cond 0
% 1.93/0.96 % fd_pseudo_cond 0
% 1.93/0.96 % AC symbols 0
% 1.93/0.96
% 1.93/0.96 % ------ Schedule dynamic 5 is on
% 1.93/0.96
% 1.93/0.96 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 1.93/0.96
% 1.93/0.96
% 1.93/0.96 % ------
% 1.93/0.96 % Current options:
% 1.93/0.96 % ------
% 1.93/0.96
% 1.93/0.96
% 1.93/0.96 %
% 1.93/0.96
% 1.93/0.96 % ------ Proving...
% 1.93/0.96 %
% 1.93/0.96
% 1.93/0.96 % SZS status Theorem for theBenchmark.p
% 1.93/0.96
% 1.93/0.96 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.93/0.97
% 1.93/0.97
%------------------------------------------------------------------------------