%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : GEO461+1 : TPTP v9.2.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.rfuMfoH1Qz true
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:34:47 PM UTC 2025
% Result : Theorem 238.45s 36.68s
% Output : Refutation 238.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 15
% Syntax : Number of formulae : 71 ( 71 unt; 0 typ; 0 def)
% Number of atoms : 71 ( 70 equ; 0 cnn)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4152 ( 4 ~; 0 |; 0 &;4148 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 35 ( 33 usr; 28 con; 0-2 aty)
% Number of variables : 88 ( 0 ^; 88 !; 0 ?; 88 :)
% Comments :
%------------------------------------------------------------------------------
thf(realu_add_type,type,
realu_add: $i ).
thf(sk__3941_type,type,
sk__3941: $i ).
thf(sk__3942_type,type,
sk__3942: $i ).
thf(c__type,type,
c_: $i ).
thf(numeral_type,type,
numeral: $i ).
thf(distance_type,type,
distance: $i ).
thf(pastecart_type,type,
pastecart: $i ).
thf(sk__3945_type,type,
sk__3945: $i ).
thf(card_type,type,
card: $i ).
thf(realu_abs_type,type,
realu_abs: $i ).
thf(fun_type,type,
fun: $i > $i > $i ).
thf(sk__3943_type,type,
sk__3943: $i ).
thf(vectoru_sub_type,type,
vectoru_sub: $i ).
thf(prod_type,type,
prod: $i > $i > $i ).
thf(realu_mul_type,type,
realu_mul: $i ).
thf(sqrt_type,type,
sqrt: $i ).
thf(u_0_type,type,
u_0: $i ).
thf(vectoru_norm_type,type,
vectoru_norm: $i ).
thf(num_type,type,
num: $i ).
thf(sk__3944_type,type,
sk__3944: $i ).
thf(realu_ofu_num_type,type,
realu_ofu_num: $i ).
thf(bit0_type,type,
bit0: $i ).
thf(bool_type,type,
bool: $i ).
thf(s_type,type,
s: $i > $i > $i ).
thf(vec_type,type,
vec: $i ).
thf(bit1_type,type,
bit1: $i ).
thf(i_type,type,
i: $i > $i > $i ).
thf(real_type,type,
real: $i ).
thf(cart_type,type,
cart: $i > $i > $i ).
thf(suc_type,type,
suc: $i ).
thf(realu_pow_type,type,
realu_pow: $i ).
thf(finite_sum_type,type,
finite_sum: $i > $i > $i ).
thf(univ_type,type,
univ: $i ).
thf(aDISTu_PASTECARTu_CANCELu_conjunct1,conjecture,
! [Q121316: $i,Q121317: $i,X: $i,Y: $i,YI_: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( prod @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) @ real ) @ distance ) @ ( s @ ( prod @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( prod @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( fun @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( prod @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) ) ) @ c_ ) @ ( s @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121317 ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121316 ) @ ( fun @ ( cart @ real @ Q121317 ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ Q121316 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q121317 ) @ Y ) ) ) ) ) @ ( s @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121317 ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121316 ) @ ( fun @ ( cart @ real @ Q121317 ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ Q121316 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q121317 ) @ YI_ ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ ( prod @ ( cart @ real @ Q121317 ) @ ( cart @ real @ Q121317 ) ) @ real ) @ distance ) @ ( s @ ( prod @ ( cart @ real @ Q121317 ) @ ( cart @ real @ Q121317 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121317 ) @ ( prod @ ( cart @ real @ Q121317 ) @ ( cart @ real @ Q121317 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121317 ) @ ( fun @ ( cart @ real @ Q121317 ) @ ( prod @ ( cart @ real @ Q121317 ) @ ( cart @ real @ Q121317 ) ) ) ) @ c_ ) @ ( s @ ( cart @ real @ Q121317 ) @ Y ) ) ) @ ( s @ ( cart @ real @ Q121317 ) @ YI_ ) ) ) ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ! [Q121316: $i,Q121317: $i,X: $i,Y: $i,YI_: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( prod @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) @ real ) @ distance ) @ ( s @ ( prod @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( prod @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( fun @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( prod @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) ) ) @ c_ ) @ ( s @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121317 ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121316 ) @ ( fun @ ( cart @ real @ Q121317 ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ Q121316 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q121317 ) @ Y ) ) ) ) ) @ ( s @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121317 ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121316 ) @ ( fun @ ( cart @ real @ Q121317 ) @ ( cart @ real @ ( finite_sum @ Q121316 @ Q121317 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ Q121316 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q121317 ) @ YI_ ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ ( prod @ ( cart @ real @ Q121317 ) @ ( cart @ real @ Q121317 ) ) @ real ) @ distance ) @ ( s @ ( prod @ ( cart @ real @ Q121317 ) @ ( cart @ real @ Q121317 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121317 ) @ ( prod @ ( cart @ real @ Q121317 ) @ ( cart @ real @ Q121317 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121317 ) @ ( fun @ ( cart @ real @ Q121317 ) @ ( prod @ ( cart @ real @ Q121317 ) @ ( cart @ real @ Q121317 ) ) ) ) @ c_ ) @ ( s @ ( cart @ real @ Q121317 ) @ Y ) ) ) @ ( s @ ( cart @ real @ Q121317 ) @ YI_ ) ) ) ) ) ),
inference('cnf.neg',[status(esa)],[aDISTu_PASTECARTu_CANCELu_conjunct1]) ).
thf(zip_derived_cl7708,plain,
( ( s @ real @ ( i @ ( s @ ( fun @ ( prod @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) @ real ) @ distance ) @ ( s @ ( prod @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( prod @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( fun @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( prod @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) ) ) @ c_ ) @ ( s @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3941 ) @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ sk__3941 ) @ sk__3943 ) ) ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3944 ) ) ) ) ) @ ( s @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3941 ) @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ sk__3941 ) @ sk__3943 ) ) ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3945 ) ) ) ) ) ) )
!= ( s @ real @ ( i @ ( s @ ( fun @ ( prod @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ sk__3942 ) ) @ real ) @ distance ) @ ( s @ ( prod @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ sk__3942 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( prod @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ sk__3942 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( fun @ ( cart @ real @ sk__3942 ) @ ( prod @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ sk__3942 ) ) ) ) @ c_ ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3944 ) ) ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3945 ) ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(adist,axiom,
! [Q100698: $i,X: $i,Y: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( prod @ ( cart @ real @ Q100698 ) @ ( cart @ real @ Q100698 ) ) @ real ) @ distance ) @ ( s @ ( prod @ ( cart @ real @ Q100698 ) @ ( cart @ real @ Q100698 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q100698 ) @ ( prod @ ( cart @ real @ Q100698 ) @ ( cart @ real @ Q100698 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q100698 ) @ ( fun @ ( cart @ real @ Q100698 ) @ ( prod @ ( cart @ real @ Q100698 ) @ ( cart @ real @ Q100698 ) ) ) ) @ c_ ) @ ( s @ ( cart @ real @ Q100698 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q100698 ) @ Y ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q100698 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ Q100698 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q100698 ) @ ( cart @ real @ Q100698 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q100698 ) @ ( fun @ ( cart @ real @ Q100698 ) @ ( cart @ real @ Q100698 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ Q100698 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q100698 ) @ Y ) ) ) ) ) ) ).
thf(zip_derived_cl6949,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( prod @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) @ real ) @ distance ) @ ( s @ ( prod @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( prod @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X0 ) @ ( prod @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) ) ) @ c_ ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X0 ) @ X2 ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X0 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X0 ) @ X2 ) ) ) ) ) ),
inference(cnf,[status(esa)],[adist]) ).
thf(zip_derived_cl6949_001,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( prod @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) @ real ) @ distance ) @ ( s @ ( prod @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( prod @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X0 ) @ ( prod @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) ) ) @ c_ ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X0 ) @ X2 ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X0 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X0 ) @ X2 ) ) ) ) ) ),
inference(cnf,[status(esa)],[adist]) ).
thf(zip_derived_cl10128,plain,
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( fun @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3941 ) @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ sk__3941 ) @ sk__3943 ) ) ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3944 ) ) ) ) ) @ ( s @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3941 ) @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ ( finite_sum @ sk__3941 @ sk__3942 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ sk__3941 ) @ sk__3943 ) ) ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3945 ) ) ) ) ) ) )
!= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ sk__3942 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ sk__3942 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ sk__3942 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3944 ) ) ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3945 ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7708,zip_derived_cl6949,zip_derived_cl6949]) ).
thf(aPASTECARTu_SUB,axiom,
! [M: $i,N: $i,X1: $i,Y1: $i,X2: $i,Y2: $i] :
( ( s @ ( cart @ real @ ( finite_sum @ M @ N ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ M @ N ) ) @ ( cart @ real @ ( finite_sum @ M @ N ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ M @ N ) ) @ ( fun @ ( cart @ real @ ( finite_sum @ M @ N ) ) @ ( cart @ real @ ( finite_sum @ M @ N ) ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ ( finite_sum @ M @ N ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ N ) @ ( cart @ real @ ( finite_sum @ M @ N ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ M ) @ ( fun @ ( cart @ real @ N ) @ ( cart @ real @ ( finite_sum @ M @ N ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ M ) @ X1 ) ) ) @ ( s @ ( cart @ real @ N ) @ Y1 ) ) ) ) ) @ ( s @ ( cart @ real @ ( finite_sum @ M @ N ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ N ) @ ( cart @ real @ ( finite_sum @ M @ N ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ M ) @ ( fun @ ( cart @ real @ N ) @ ( cart @ real @ ( finite_sum @ M @ N ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ M ) @ X2 ) ) ) @ ( s @ ( cart @ real @ N ) @ Y2 ) ) ) ) )
= ( s @ ( cart @ real @ ( finite_sum @ M @ N ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ N ) @ ( cart @ real @ ( finite_sum @ M @ N ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ M ) @ ( fun @ ( cart @ real @ N ) @ ( cart @ real @ ( finite_sum @ M @ N ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ M ) @ ( i @ ( s @ ( fun @ ( cart @ real @ M ) @ ( cart @ real @ M ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ M ) @ ( fun @ ( cart @ real @ M ) @ ( cart @ real @ M ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ M ) @ X1 ) ) ) @ ( s @ ( cart @ real @ M ) @ X2 ) ) ) ) ) @ ( s @ ( cart @ real @ N ) @ ( i @ ( s @ ( fun @ ( cart @ real @ N ) @ ( cart @ real @ N ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ N ) @ ( fun @ ( cart @ real @ N ) @ ( cart @ real @ N ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ N ) @ Y1 ) ) ) @ ( s @ ( cart @ real @ N ) @ Y2 ) ) ) ) ) ) ).
thf(zip_derived_cl7691,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( s @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) @ ( fun @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X1 ) @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X1 ) @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ X0 ) @ X2 ) ) ) @ ( s @ ( cart @ real @ X1 ) @ X4 ) ) ) ) ) @ ( s @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X1 ) @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X1 ) @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ X0 ) @ X3 ) ) ) @ ( s @ ( cart @ real @ X1 ) @ X5 ) ) ) ) )
= ( s @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X1 ) @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X1 ) @ ( cart @ real @ ( finite_sum @ X0 @ X1 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ X0 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ X0 ) @ X2 ) ) ) @ ( s @ ( cart @ real @ X0 ) @ X3 ) ) ) ) ) @ ( s @ ( cart @ real @ X1 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X1 ) @ ( cart @ real @ X1 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X1 ) @ ( fun @ ( cart @ real @ X1 ) @ ( cart @ real @ X1 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ X1 ) @ X4 ) ) ) @ ( s @ ( cart @ real @ X1 ) @ X5 ) ) ) ) ) ),
inference(cnf,[status(esa)],[aPASTECARTu_SUB]) ).
thf(aVECTORu_SUBu_REFL,axiom,
! [Q99591: $i,X: $i] :
( ( s @ ( cart @ real @ Q99591 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q99591 ) @ ( cart @ real @ Q99591 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q99591 ) @ ( fun @ ( cart @ real @ Q99591 ) @ ( cart @ real @ Q99591 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ Q99591 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q99591 ) @ X ) ) )
= ( s @ ( cart @ real @ Q99591 ) @ ( i @ ( s @ ( fun @ num @ ( cart @ real @ Q99591 ) ) @ vec ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) ).
thf(zip_derived_cl6883,plain,
! [X0: $i,X1: $i] :
( ( s @ ( cart @ real @ X0 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) )
= ( s @ ( cart @ real @ X0 ) @ ( i @ ( s @ ( fun @ num @ ( cart @ real @ X0 ) ) @ vec ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ),
inference(cnf,[status(esa)],[aVECTORu_SUBu_REFL]) ).
thf(aNUMERAL,axiom,
! [N0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ N0 ) ) )
= ( s @ num @ N0 ) ) ).
thf(zip_derived_cl647,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl8528,plain,
! [X0: $i,X1: $i] :
( ( s @ ( cart @ real @ X0 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X0 ) @ ( cart @ real @ X0 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) )
= ( s @ ( cart @ real @ X0 ) @ ( i @ ( s @ ( fun @ num @ ( cart @ real @ X0 ) ) @ vec ) @ ( s @ num @ u_0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6883,zip_derived_cl647]) ).
thf(aNORMu_PASTECART,axiom,
! [Q121103: $i,Q121104: $i,X: $i,Y: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ Q121103 @ Q121104 ) ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ ( finite_sum @ Q121103 @ Q121104 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121104 ) @ ( cart @ real @ ( finite_sum @ Q121103 @ Q121104 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121103 ) @ ( fun @ ( cart @ real @ Q121104 ) @ ( cart @ real @ ( finite_sum @ Q121103 @ Q121104 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ Q121103 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q121104 ) @ Y ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ sqrt ) @ ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_add ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121103 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ Q121103 ) @ X ) ) ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) ) ) ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121104 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ Q121104 ) @ Y ) ) ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl7701,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ X0 @ X2 ) ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ ( finite_sum @ X0 @ X2 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X2 ) @ ( cart @ real @ ( finite_sum @ X0 @ X2 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X2 ) @ ( cart @ real @ ( finite_sum @ X0 @ X2 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X2 ) @ X3 ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ sqrt ) @ ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_add ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) ) ) ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X2 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X2 ) @ X3 ) ) ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[aNORMu_PASTECART]) ).
thf(aARITHu_SUCu_conjunct1,axiom,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ).
thf(zip_derived_cl1255,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct1]) ).
thf(aARITHu_SUCu_conjunct3,axiom,
! [N0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ N0 ) ) ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ N0 ) ) ) ) ) ) ).
thf(zip_derived_cl1257,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ X0 ) ) ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ X0 ) ) ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct3]) ).
thf(zip_derived_cl1255_002,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct1]) ).
thf(aCARDu_BOOL,axiom,
( ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl4041,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[aCARDu_BOOL]) ).
thf(zip_derived_cl1255_003,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct1]) ).
thf(zip_derived_cl1257_004,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ X0 ) ) ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ X0 ) ) ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct3]) ).
thf(zip_derived_cl1255_005,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct1]) ).
thf(zip_derived_cl647_006,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl8497,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4041,zip_derived_cl1255,zip_derived_cl1257,zip_derived_cl1255,zip_derived_cl647]) ).
thf(zip_derived_cl647_007,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl1255_008,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct1]) ).
thf(zip_derived_cl1257_009,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ X0 ) ) ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ X0 ) ) ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct3]) ).
thf(zip_derived_cl1255_010,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct1]) ).
thf(zip_derived_cl8497_011,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4041,zip_derived_cl1255,zip_derived_cl1257,zip_derived_cl1255,zip_derived_cl647]) ).
thf(zip_derived_cl647_012,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl10147,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ X0 @ X2 ) ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ ( finite_sum @ X0 @ X2 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X2 ) @ ( cart @ real @ ( finite_sum @ X0 @ X2 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X2 ) @ ( cart @ real @ ( finite_sum @ X0 @ X2 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X2 ) @ X3 ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ sqrt ) @ ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_add ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) ) ) ) ) ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X2 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X2 ) @ X3 ) ) ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) ) ) ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7701,zip_derived_cl1255,zip_derived_cl1257,zip_derived_cl1255,zip_derived_cl8497,zip_derived_cl647,zip_derived_cl1255,zip_derived_cl1257,zip_derived_cl1255,zip_derived_cl8497,zip_derived_cl647]) ).
thf(aNORMu_0,axiom,
! [Q102146: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q102146 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ Q102146 ) @ ( i @ ( s @ ( fun @ num @ ( cart @ real @ Q102146 ) ) @ vec ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) ).
thf(zip_derived_cl7005,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X0 ) @ ( i @ ( s @ ( fun @ num @ ( cart @ real @ X0 ) ) @ vec ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ),
inference(cnf,[status(esa)],[aNORMu_0]) ).
thf(zip_derived_cl647_013,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl647_014,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl8377,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X0 ) @ ( i @ ( s @ ( fun @ num @ ( cart @ real @ X0 ) ) @ vec ) @ ( s @ num @ u_0 ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ u_0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7005,zip_derived_cl647,zip_derived_cl647]) ).
thf(aREALu_POWu_2,axiom,
! [X: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ X ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_mul ) @ ( s @ real @ X ) ) ) @ ( s @ real @ X ) ) ) ) ).
thf(zip_derived_cl2090,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ X0 ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_mul ) @ ( s @ real @ X0 ) ) ) @ ( s @ real @ X0 ) ) ) ),
inference(cnf,[status(esa)],[aREALu_POWu_2]) ).
thf(zip_derived_cl1255_015,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct1]) ).
thf(zip_derived_cl647_016,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl8113,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ X0 ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_mul ) @ ( s @ real @ X0 ) ) ) @ ( s @ real @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2090,zip_derived_cl1255,zip_derived_cl647]) ).
thf(zip_derived_cl1257_017,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ X0 ) ) ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ X0 ) ) ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct3]) ).
thf(zip_derived_cl1255_018,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct1]) ).
thf(zip_derived_cl8163,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ X0 ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_mul ) @ ( s @ real @ X0 ) ) ) @ ( s @ real @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl8113,zip_derived_cl1257,zip_derived_cl1255]) ).
thf(zip_derived_cl8497_019,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4041,zip_derived_cl1255,zip_derived_cl1257,zip_derived_cl1255,zip_derived_cl647]) ).
thf(zip_derived_cl8500,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ X0 ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_mul ) @ ( s @ real @ X0 ) ) ) @ ( s @ real @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl8163,zip_derived_cl8497]) ).
thf(aREALu_MULu_RZERO,axiom,
! [X: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_mul ) @ ( s @ real @ X ) ) ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) ).
thf(zip_derived_cl2045,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_mul ) @ ( s @ real @ X0 ) ) ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ),
inference(cnf,[status(esa)],[aREALu_MULu_RZERO]) ).
thf(zip_derived_cl647_020,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl647_021,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl8284,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_mul ) @ ( s @ real @ X0 ) ) ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ u_0 ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ u_0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2045,zip_derived_cl647,zip_derived_cl647]) ).
thf(aREALu_ADDu_LID,axiom,
! [X: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_add ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) @ ( s @ real @ X ) ) )
= ( s @ real @ X ) ) ).
thf(zip_derived_cl1981,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_add ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) @ ( s @ real @ X0 ) ) )
= ( s @ real @ X0 ) ),
inference(cnf,[status(esa)],[aREALu_ADDu_LID]) ).
thf(zip_derived_cl647_022,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl7969,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_add ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ u_0 ) ) ) ) ) @ ( s @ real @ X0 ) ) )
= ( s @ real @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl1981,zip_derived_cl647]) ).
thf(aPOWu_2u_SQRTu_ABS,axiom,
! [X: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ sqrt ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ X ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ realu_abs ) @ ( s @ real @ X ) ) ) ) ).
thf(zip_derived_cl6820,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ sqrt ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ X0 ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ realu_abs ) @ ( s @ real @ X0 ) ) ) ),
inference(cnf,[status(esa)],[aPOWu_2u_SQRTu_ABS]) ).
thf(zip_derived_cl1255_023,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct1]) ).
thf(zip_derived_cl1257_024,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ X0 ) ) ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ X0 ) ) ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct3]) ).
thf(zip_derived_cl1255_025,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ),
inference(cnf,[status(esa)],[aARITHu_SUCu_conjunct1]) ).
thf(zip_derived_cl8497_026,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4041,zip_derived_cl1255,zip_derived_cl1257,zip_derived_cl1255,zip_derived_cl647]) ).
thf(zip_derived_cl647_027,plain,
! [X0: $i] :
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ X0 ) ) )
= ( s @ num @ X0 ) ),
inference(cnf,[status(esa)],[aNUMERAL]) ).
thf(zip_derived_cl8884,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ sqrt ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ X0 ) ) ) @ ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ realu_abs ) @ ( s @ real @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6820,zip_derived_cl1255,zip_derived_cl1257,zip_derived_cl1255,zip_derived_cl8497,zip_derived_cl647]) ).
thf(aREALu_ABSu_NORM,axiom,
! [Q102710: $i,X: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ realu_abs ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q102710 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ Q102710 ) @ X ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q102710 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ Q102710 ) @ X ) ) ) ) ).
thf(zip_derived_cl7033,plain,
! [X0: $i,X1: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ realu_abs ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) ),
inference(cnf,[status(esa)],[aREALu_ABSu_NORM]) ).
thf(zip_derived_cl10720,plain,
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ sk__3942 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ sk__3942 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ sk__3942 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3944 ) ) ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3945 ) ) ) ) )
!= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ sk__3942 ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ sk__3942 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( fun @ ( cart @ real @ sk__3942 ) @ ( cart @ real @ sk__3942 ) ) ) @ vectoru_sub ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3944 ) ) ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3945 ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl10128,zip_derived_cl7691,zip_derived_cl8528,zip_derived_cl10147,zip_derived_cl8377,zip_derived_cl8500,zip_derived_cl8284,zip_derived_cl7969,zip_derived_cl8884,zip_derived_cl7033]) ).
thf(zip_derived_cl10721,plain,
$false,
inference(simplify,[status(thm)],[zip_derived_cl10720]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.14 % Problem : GEO461+1 : TPTP v9.2.0. Released v7.0.0.
% 0.03/0.14 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.rfuMfoH1Qz true
% 0.10/0.35 % Computer : n023.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8042.1875MB
% 0.10/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Wed Oct 1 17:43:53 EDT 2025
% 0.10/0.35 % CPUTime :
% 0.10/0.35 % Running portfolio for 300 s
% 0.10/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Number of cores: 8
% 0.10/0.35 % Python version: Python 3.6.8
% 0.10/0.35 % Running in FO mode
% 0.34/0.53 % Total configuration time : 435
% 0.34/0.53 % Estimated wc time : 1092
% 0.34/0.53 % Estimated cpu time (7 cpus) : 156.0
% 0.36/0.62 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.36/0.62 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.36/0.63 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.36/0.63 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.36/0.63 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.36/0.63 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.36/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 238.45/36.68 % Solved by fo/fo13.sh.
% 238.45/36.68 % done 0 iterations in 35.972s
% 238.45/36.68 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 238.45/36.68 % SZS output start Refutation
% See solution above
% 238.45/36.69
% 238.45/36.69
% 238.45/36.69 % Terminating...
% 238.45/36.73 % Runner terminated.
% 238.45/36.74 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------