%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : GEO460+1 : TPTP v9.2.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.Zgj0cQmYYO true
% Computer : n031.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 198.31s 29.05s
% Output : Refutation 198.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 12
% Syntax : Number of formulae : 61 ( 61 unt; 0 typ; 0 def)
% Number of atoms : 61 ( 60 equ; 0 cnn)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2666 ( 4 ~; 0 |; 0 &;2662 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 29 ( 27 usr; 23 con; 0-2 aty)
% Number of variables : 55 ( 0 ^; 55 !; 0 ?; 55 :)
% Comments :
%------------------------------------------------------------------------------
thf(realu_add_type,type,
realu_add: $i ).
thf(numeral_type,type,
numeral: $i ).
thf(pastecart_type,type,
pastecart: $i ).
thf(card_type,type,
card: $i ).
thf(fun_type,type,
fun: $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__3943_type,type,
sk__3943: $i ).
thf(realu_ofu_num_type,type,
realu_ofu_num: $i ).
thf(bit0_type,type,
bit0: $i ).
thf(bool_type,type,
bool: $i ).
thf(sk__3942_type,type,
sk__3942: $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(dot_type,type,
dot: $i ).
thf(real_type,type,
real: $i ).
thf(cart_type,type,
cart: $i > $i > $i ).
thf(sk__3941_type,type,
sk__3941: $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(aNORMu_PASTECARTu_0u_conjunct0,conjecture,
! [Q121218: $i,Q121215: $i,X: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ Q121215 @ Q121218 ) ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ ( finite_sum @ Q121215 @ Q121218 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121218 ) @ ( cart @ real @ ( finite_sum @ Q121215 @ Q121218 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121215 ) @ ( fun @ ( cart @ real @ Q121218 ) @ ( cart @ real @ ( finite_sum @ Q121215 @ Q121218 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ Q121215 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q121218 ) @ ( i @ ( s @ ( fun @ num @ ( cart @ real @ Q121218 ) ) @ vec ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121215 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ Q121215 ) @ X ) ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ! [Q121218: $i,Q121215: $i,X: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ Q121215 @ Q121218 ) ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ ( finite_sum @ Q121215 @ Q121218 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121218 ) @ ( cart @ real @ ( finite_sum @ Q121215 @ Q121218 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121215 ) @ ( fun @ ( cart @ real @ Q121218 ) @ ( cart @ real @ ( finite_sum @ Q121215 @ Q121218 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ Q121215 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q121218 ) @ ( i @ ( s @ ( fun @ num @ ( cart @ real @ Q121218 ) ) @ vec ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q121215 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ Q121215 ) @ X ) ) ) ),
inference('cnf.neg',[status(esa)],[aNORMu_PASTECARTu_0u_conjunct0]) ).
thf(zip_derived_cl7705,plain,
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ sk__3942 @ sk__3941 ) ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ ( finite_sum @ sk__3942 @ sk__3941 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3941 ) @ ( cart @ real @ ( finite_sum @ sk__3942 @ sk__3941 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( fun @ ( cart @ real @ sk__3941 ) @ ( cart @ real @ ( finite_sum @ sk__3942 @ sk__3941 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3943 ) ) ) @ ( s @ ( cart @ real @ sk__3941 ) @ ( i @ ( s @ ( fun @ num @ ( cart @ real @ sk__3941 ) ) @ vec ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) )
!= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3943 ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
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_cl8546,plain,
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ ( finite_sum @ sk__3942 @ sk__3941 ) ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ ( finite_sum @ sk__3942 @ sk__3941 ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3941 ) @ ( cart @ real @ ( finite_sum @ sk__3942 @ sk__3941 ) ) ) @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ ( fun @ ( cart @ real @ sk__3941 ) @ ( cart @ real @ ( finite_sum @ sk__3942 @ sk__3941 ) ) ) ) @ pastecart ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3943 ) ) ) @ ( s @ ( cart @ real @ sk__3941 ) @ ( i @ ( s @ ( fun @ num @ ( cart @ real @ sk__3941 ) ) @ vec ) @ ( s @ num @ u_0 ) ) ) ) ) ) )
!= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3943 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7705,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(aTWO,axiom,
( ( 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 @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl690,plain,
( ( 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 @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ numeral ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit1 ) @ ( s @ num @ u_0 ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[aTWO]) ).
thf(zip_derived_cl1255_001,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_002,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_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_cl647_004,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_cl7954,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) )
= ( 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_cl690,zip_derived_cl1255,zip_derived_cl647,zip_derived_cl1255,zip_derived_cl647]) ).
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_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_cl7954_006,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) )
= ( 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_cl690,zip_derived_cl1255,zip_derived_cl647,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_cl8049,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_cl7954,zip_derived_cl647]) ).
thf(zip_derived_cl8050,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7954,zip_derived_cl8049]) ).
thf(zip_derived_cl647_008,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_009,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_cl8050_010,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7954,zip_derived_cl8049]) ).
thf(zip_derived_cl647_011,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_cl9694,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_cl8050,zip_derived_cl647,zip_derived_cl1255,zip_derived_cl8050,zip_derived_cl647]) ).
thf(aNORMu_POWu_2,axiom,
! [Q102322: $i,X: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ num @ real ) ) @ realu_pow ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q102322 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ Q102322 ) @ 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 @ ( cart @ real @ Q102322 ) @ real ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q102322 ) @ ( fun @ ( cart @ real @ Q102322 ) @ real ) ) @ dot ) @ ( s @ ( cart @ real @ Q102322 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q102322 ) @ X ) ) ) ) ).
thf(zip_derived_cl7016,plain,
! [X0: $i,X1: $i] :
( ( 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 @ ( cart @ real @ X0 ) @ real ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X0 ) @ real ) ) @ dot ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) ),
inference(cnf,[status(esa)],[aNORMu_POWu_2]) ).
thf(zip_derived_cl1255_012,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_cl8050_013,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) )
= ( s @ num @ ( i @ ( s @ ( fun @ ( fun @ bool @ bool ) @ num ) @ card ) @ ( s @ ( fun @ bool @ bool ) @ univ ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7954,zip_derived_cl8049]) ).
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_cl8385,plain,
! [X0: $i,X1: $i] :
( ( 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 @ ( cart @ real @ X0 ) @ real ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X0 ) @ real ) ) @ dot ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl7016,zip_derived_cl1255,zip_derived_cl8050,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_015,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_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_cl7984,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_017,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_cl7954_018,plain,
( ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ bit0 ) @ ( s @ num @ ( i @ ( s @ ( fun @ num @ num ) @ suc ) @ ( s @ num @ u_0 ) ) ) ) )
= ( 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_cl690,zip_derived_cl1255,zip_derived_cl647,zip_derived_cl1255,zip_derived_cl647]) ).
thf(zip_derived_cl647_019,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_cl8028,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_cl2090,zip_derived_cl1255,zip_derived_cl7954,zip_derived_cl647]) ).
thf(zip_derived_cl8049_020,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_cl7954,zip_derived_cl647]) ).
thf(zip_derived_cl8055,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_cl8028,zip_derived_cl8049]) ).
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_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_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_cl8008,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_RID,axiom,
! [X: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_add ) @ ( 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 @ X ) ) ).
thf(zip_derived_cl2029,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_add ) @ ( 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 @ X0 ) ),
inference(cnf,[status(esa)],[aREALu_ADDu_RID]) ).
thf(zip_derived_cl647_023,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_cl7942,plain,
! [X0: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ ( i @ ( s @ ( fun @ real @ ( fun @ real @ real ) ) @ realu_add ) @ ( s @ real @ X0 ) ) ) @ ( s @ real @ ( i @ ( s @ ( fun @ num @ real ) @ realu_ofu_num ) @ ( s @ num @ u_0 ) ) ) ) )
= ( s @ real @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2029,zip_derived_cl647]) ).
thf(avectoru_norm,axiom,
! [Q100593: $i,X: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q100593 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ Q100593 ) @ X ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ sqrt ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ Q100593 ) @ real ) @ ( i @ ( s @ ( fun @ ( cart @ real @ Q100593 ) @ ( fun @ ( cart @ real @ Q100593 ) @ real ) ) @ dot ) @ ( s @ ( cart @ real @ Q100593 ) @ X ) ) ) @ ( s @ ( cart @ real @ Q100593 ) @ X ) ) ) ) ) ) ).
thf(zip_derived_cl6940,plain,
! [X0: $i,X1: $i] :
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) )
= ( s @ real @ ( i @ ( s @ ( fun @ real @ real ) @ sqrt ) @ ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ real ) @ ( i @ ( s @ ( fun @ ( cart @ real @ X0 ) @ ( fun @ ( cart @ real @ X0 ) @ real ) ) @ dot ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) @ ( s @ ( cart @ real @ X0 ) @ X1 ) ) ) ) ) ),
inference(cnf,[status(esa)],[avectoru_norm]) ).
thf(zip_derived_cl9697,plain,
( ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3943 ) ) )
!= ( s @ real @ ( i @ ( s @ ( fun @ ( cart @ real @ sk__3942 ) @ real ) @ vectoru_norm ) @ ( s @ ( cart @ real @ sk__3942 ) @ sk__3943 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl8546,zip_derived_cl9694,zip_derived_cl8385,zip_derived_cl7984,zip_derived_cl8055,zip_derived_cl8008,zip_derived_cl7942,zip_derived_cl6940]) ).
thf(zip_derived_cl9698,plain,
$false,
inference(simplify,[status(thm)],[zip_derived_cl9697]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO460+1 : TPTP v9.2.0. Released v7.0.0.
% 0.07/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.Zgj0cQmYYO true
% 0.13/0.34 % Computer : n031.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 1 17:43:23 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % Running portfolio for 300 s
% 0.13/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.35 % Running in FO mode
% 0.42/0.60 % Total configuration time : 435
% 0.42/0.60 % Estimated wc time : 1092
% 0.42/0.60 % Estimated cpu time (7 cpus) : 156.0
% 0.47/0.69 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.47/0.72 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.47/0.72 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.47/0.72 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.47/0.73 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.47/0.73 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.47/0.73 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 198.31/29.05 % Solved by fo/fo13.sh.
% 198.31/29.05 % done 0 iterations in 28.287s
% 198.31/29.05 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 198.31/29.05 % SZS output start Refutation
% See solution above
% 198.31/29.05
% 198.31/29.05
% 198.31/29.05 % Terminating...
% 198.31/29.10 % Runner terminated.
% 198.31/29.11 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------