%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM451+6 : TPTP v9.2.0. Released v4.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.lxFhFVUHrZ true
% Computer : n003.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:47:01 PM UTC 2025
% Result : Theorem 65.74s 10.41s
% Output : Refutation 66.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 21
% Syntax : Number of formulae : 732 ( 412 unt; 0 typ; 0 def)
% Number of atoms : 1485 ( 569 equ; 0 cnn)
% Maximal formula atoms : 26 ( 2 avg)
% Number of connectives : 6268 ( 637 ~; 671 |; 56 &;4878 @)
% ( 6 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 22 ( 20 usr; 7 con; 0-3 aty)
% Number of variables : 406 ( 0 ^; 397 !; 9 ?; 406 :)
% Comments :
%------------------------------------------------------------------------------
thf(smndt0_type,type,
smndt0: $i > $i ).
thf(sdtasdt0_type,type,
sdtasdt0: $i > $i > $i ).
thf(aInteger0_type,type,
aInteger0: $i > $o ).
thf(sz10_type,type,
sz10: $i ).
thf(xS_type,type,
xS: $i ).
thf(xp_type,type,
xp: $i ).
thf(cS2076_type,type,
cS2076: $i ).
thf(sz00_type,type,
sz00: $i ).
thf(sdtpldt0_type,type,
sdtpldt0: $i > $i > $i ).
thf(sbsmnsldt0_type,type,
sbsmnsldt0: $i > $i ).
thf(szAzrzSzezqlpdtcmdtrp0_type,type,
szAzrzSzezqlpdtcmdtrp0: $i > $i > $i ).
thf(stldt0_type,type,
stldt0: $i > $i ).
thf(aSubsetOf0_type,type,
aSubsetOf0: $i > $i > $o ).
thf(aElementOf0_type,type,
aElementOf0: $i > $i > $o ).
thf(aDivisorOf0_type,type,
aDivisorOf0: $i > $i > $o ).
thf(sdteqdtlpzmzozddtrp0_type,type,
sdteqdtlpzmzozddtrp0: $i > $i > $i > $o ).
thf(cS2200_type,type,
cS2200: $i ).
thf(sk__25_type,type,
sk__25: $i > $i ).
thf(aSet0_type,type,
aSet0: $i > $o ).
thf(sk__type,type,
sk_: $i > $i > $i ).
thf(mMulOne,axiom,
! [W0: $i] :
( ( aInteger0 @ W0 )
=> ( ( ( sdtasdt0 @ W0 @ sz10 )
= W0 )
& ( W0
= ( sdtasdt0 @ sz10 @ W0 ) ) ) ) ).
thf(zip_derived_cl14,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ X0 @ sz10 )
= X0 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulOne]) ).
thf(mAddComm,axiom,
! [W0: $i,W1: $i] :
( ( ( aInteger0 @ W0 )
& ( aInteger0 @ W1 ) )
=> ( ( sdtpldt0 @ W0 @ W1 )
= ( sdtpldt0 @ W1 @ W0 ) ) ) ).
thf(zip_derived_cl7,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ X0 @ X1 )
= ( sdtpldt0 @ X1 @ X0 ) ) ),
inference(cnf,[status(esa)],[mAddComm]) ).
thf(mEquModRef,axiom,
! [W0: $i,W1: $i] :
( ( ( aInteger0 @ W0 )
& ( aInteger0 @ W1 )
& ( W1 != sz00 ) )
=> ( sdteqdtlpzmzozddtrp0 @ W0 @ W0 @ W1 ) ) ).
thf(zip_derived_cl30,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( X1 = sz00 )
| ( sdteqdtlpzmzozddtrp0 @ X0 @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[mEquModRef]) ).
thf(m__2171,axiom,
( ( aSubsetOf0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) )
& ! [W0: $i] :
( ( aElementOf0 @ W0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) )
=> ( aElementOf0 @ W0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) )
& ! [W0: $i] :
( ( aElementOf0 @ W0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) )
<=> ( ( aInteger0 @ W0 )
& ~ ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) ) )
& ! [W0: $i] :
( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) )
<=> ( ( aInteger0 @ W0 )
& ? [W1: $i] :
( ( aElementOf0 @ W0 @ W1 )
& ( aElementOf0 @ W1 @ xS ) ) ) )
& ( aSet0 @ ( sbsmnsldt0 @ xS ) )
& ! [W0: $i] :
( ( ( ( aInteger0 @ W0 )
& ( ? [W1: $i] :
( ( ( sdtasdt0 @ xp @ W1 )
= ( sdtpldt0 @ W0 @ ( smndt0 @ sz10 ) ) )
& ( aInteger0 @ W1 ) )
| ( aDivisorOf0 @ xp @ ( sdtpldt0 @ W0 @ ( smndt0 @ sz10 ) ) )
| ( sdteqdtlpzmzozddtrp0 @ W0 @ sz10 @ xp ) ) )
=> ( aElementOf0 @ W0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) ) )
& ( ( aElementOf0 @ W0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) )
=> ( ( aInteger0 @ W0 )
& ? [W1: $i] :
( ( ( sdtasdt0 @ xp @ W1 )
= ( sdtpldt0 @ W0 @ ( smndt0 @ sz10 ) ) )
& ( aInteger0 @ W1 ) )
& ( aDivisorOf0 @ xp @ ( sdtpldt0 @ W0 @ ( smndt0 @ sz10 ) ) )
& ( sdteqdtlpzmzozddtrp0 @ W0 @ sz10 @ xp ) ) ) )
& ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) )
& ( xp != sz00 )
& ( aInteger0 @ xp ) ) ).
thf(zip_derived_cl195,plain,
! [X0: $i] :
( ( aElementOf0 @ X0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) )
| ~ ( sdteqdtlpzmzozddtrp0 @ X0 @ sz10 @ xp )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl1572,plain,
( ( xp = sz00 )
| ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ sz10 )
| ( aElementOf0 @ sz10 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) )
| ~ ( aInteger0 @ sz10 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl30,zip_derived_cl195]) ).
thf(zip_derived_cl192,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(mIntOne,axiom,
aInteger0 @ sz10 ).
thf(zip_derived_cl2,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl2_001,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl1573,plain,
( ( xp = sz00 )
| ( aElementOf0 @ sz10 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1572,zip_derived_cl192,zip_derived_cl2,zip_derived_cl2]) ).
thf(zip_derived_cl193,plain,
xp != sz00,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl1574,plain,
aElementOf0 @ sz10 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1573,zip_derived_cl193]) ).
thf(zip_derived_cl200,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ xp @ ( sk__25 @ X0 ) )
= ( sdtpldt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aElementOf0 @ X0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) ) ),
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl3643,plain,
( ( sdtasdt0 @ xp @ ( sk__25 @ sz10 ) )
= ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1574,zip_derived_cl200]) ).
thf(mAddNeg,axiom,
! [W0: $i] :
( ( aInteger0 @ W0 )
=> ( ( ( sdtpldt0 @ W0 @ ( smndt0 @ W0 ) )
= sz00 )
& ( sz00
= ( sdtpldt0 @ ( smndt0 @ W0 ) @ W0 ) ) ) ) ).
thf(zip_derived_cl10,plain,
! [X0: $i] :
( ( ( sdtpldt0 @ X0 @ ( smndt0 @ X0 ) )
= sz00 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mAddNeg]) ).
thf(zip_derived_cl3643_002,plain,
( ( sdtasdt0 @ xp @ ( sk__25 @ sz10 ) )
= ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1574,zip_derived_cl200]) ).
thf(mZeroDiv,axiom,
! [W0: $i,W1: $i] :
( ( ( aInteger0 @ W0 )
& ( aInteger0 @ W1 ) )
=> ( ( ( sdtasdt0 @ W0 @ W1 )
= sz00 )
=> ( ( W0 = sz00 )
| ( W1 = sz00 ) ) ) ) ).
thf(zip_derived_cl22,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( X1 = sz00 )
| ( ( sdtasdt0 @ X0 @ X1 )
!= sz00 ) ),
inference(cnf,[status(esa)],[mZeroDiv]) ).
thf(zip_derived_cl3654,plain,
( ( xp = sz00 )
| ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ ( sk__25 @ sz10 ) )
| ( ( sk__25 @ sz10 )
= sz00 )
| ( ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) )
!= sz00 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl3643,zip_derived_cl22]) ).
thf(zip_derived_cl192_003,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl1574_004,plain,
aElementOf0 @ sz10 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1573,zip_derived_cl193]) ).
thf(zip_derived_cl199,plain,
! [X0: $i] :
( ( aInteger0 @ ( sk__25 @ X0 ) )
| ~ ( aElementOf0 @ X0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) ) ),
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl1617,plain,
aInteger0 @ ( sk__25 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl1574,zip_derived_cl199]) ).
thf(zip_derived_cl3673,plain,
( ( xp = sz00 )
| ( ( sk__25 @ sz10 )
= sz00 )
| ( ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) )
!= sz00 ) ),
inference(demod,[status(thm)],[zip_derived_cl3654,zip_derived_cl192,zip_derived_cl1617]) ).
thf(zip_derived_cl193_005,plain,
xp != sz00,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl3674,plain,
( ( ( sk__25 @ sz10 )
= sz00 )
| ( ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) )
!= sz00 ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl3673,zip_derived_cl193]) ).
thf(zip_derived_cl4052,plain,
( ~ ( aInteger0 @ sz10 )
| ( ( sk__25 @ sz10 )
= sz00 )
| ( sz00 != sz00 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl10,zip_derived_cl3674]) ).
thf(zip_derived_cl2_006,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl4058,plain,
( ( ( sk__25 @ sz10 )
= sz00 )
| ( sz00 != sz00 ) ),
inference(demod,[status(thm)],[zip_derived_cl4052,zip_derived_cl2]) ).
thf(zip_derived_cl4059,plain,
( ( sk__25 @ sz10 )
= sz00 ),
inference(simplify,[status(thm)],[zip_derived_cl4058]) ).
thf(zip_derived_cl10_007,plain,
! [X0: $i] :
( ( ( sdtpldt0 @ X0 @ ( smndt0 @ X0 ) )
= sz00 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mAddNeg]) ).
thf(zip_derived_cl201,plain,
! [X0: $i] :
( ( aDivisorOf0 @ xp @ ( sdtpldt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aElementOf0 @ X0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) ) ),
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl388,plain,
( ~ ( aInteger0 @ sz10 )
| ( aDivisorOf0 @ xp @ sz00 )
| ~ ( aElementOf0 @ sz10 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl10,zip_derived_cl201]) ).
thf(zip_derived_cl2_008,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl394,plain,
( ( aDivisorOf0 @ xp @ sz00 )
| ~ ( aElementOf0 @ sz10 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) ) ),
inference(demod,[status(thm)],[zip_derived_cl388,zip_derived_cl2]) ).
thf(zip_derived_cl1574_009,plain,
aElementOf0 @ sz10 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1573,zip_derived_cl193]) ).
thf(zip_derived_cl1611,plain,
aDivisorOf0 @ xp @ sz00,
inference(demod,[status(thm)],[zip_derived_cl394,zip_derived_cl1574]) ).
thf(mDivisor,axiom,
! [W0: $i] :
( ( aInteger0 @ W0 )
=> ! [W1: $i] :
( ( aDivisorOf0 @ W1 @ W0 )
<=> ( ( aInteger0 @ W1 )
& ( W1 != sz00 )
& ? [W2: $i] :
( ( ( sdtasdt0 @ W1 @ W2 )
= W0 )
& ( aInteger0 @ W2 ) ) ) ) ) ).
thf(zip_derived_cl24,plain,
! [X0: $i,X1: $i] :
( ~ ( aDivisorOf0 @ X0 @ X1 )
| ( ( sdtasdt0 @ X0 @ ( sk_ @ X0 @ X1 ) )
= X1 )
| ~ ( aInteger0 @ X1 ) ),
inference(cnf,[status(esa)],[mDivisor]) ).
thf(zip_derived_cl1689,plain,
( ( ( sdtasdt0 @ xp @ ( sk_ @ xp @ sz00 ) )
= sz00 )
| ~ ( aInteger0 @ sz00 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1611,zip_derived_cl24]) ).
thf(mIntZero,axiom,
aInteger0 @ sz00 ).
thf(zip_derived_cl1,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl1692,plain,
( ( sdtasdt0 @ xp @ ( sk_ @ xp @ sz00 ) )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl1689,zip_derived_cl1]) ).
thf(zip_derived_cl1692_010,plain,
( ( sdtasdt0 @ xp @ ( sk_ @ xp @ sz00 ) )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl1689,zip_derived_cl1]) ).
thf(zip_derived_cl22_011,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( X1 = sz00 )
| ( ( sdtasdt0 @ X0 @ X1 )
!= sz00 ) ),
inference(cnf,[status(esa)],[mZeroDiv]) ).
thf(zip_derived_cl1900,plain,
( ( xp = sz00 )
| ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ ( sk_ @ xp @ sz00 ) )
| ( ( sk_ @ xp @ sz00 )
= sz00 )
| ( sz00 != sz00 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1692,zip_derived_cl22]) ).
thf(zip_derived_cl192_012,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl1611_013,plain,
aDivisorOf0 @ xp @ sz00,
inference(demod,[status(thm)],[zip_derived_cl394,zip_derived_cl1574]) ).
thf(zip_derived_cl25,plain,
! [X0: $i,X1: $i] :
( ~ ( aDivisorOf0 @ X0 @ X1 )
| ( aInteger0 @ ( sk_ @ X0 @ X1 ) )
| ~ ( aInteger0 @ X1 ) ),
inference(cnf,[status(esa)],[mDivisor]) ).
thf(zip_derived_cl1690,plain,
( ( aInteger0 @ ( sk_ @ xp @ sz00 ) )
| ~ ( aInteger0 @ sz00 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1611,zip_derived_cl25]) ).
thf(zip_derived_cl1_014,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl1693,plain,
aInteger0 @ ( sk_ @ xp @ sz00 ),
inference(demod,[status(thm)],[zip_derived_cl1690,zip_derived_cl1]) ).
thf(zip_derived_cl1913,plain,
( ( xp = sz00 )
| ( ( sk_ @ xp @ sz00 )
= sz00 )
| ( sz00 != sz00 ) ),
inference(demod,[status(thm)],[zip_derived_cl1900,zip_derived_cl192,zip_derived_cl1693]) ).
thf(zip_derived_cl1914,plain,
( ( ( sk_ @ xp @ sz00 )
= sz00 )
| ( xp = sz00 ) ),
inference(simplify,[status(thm)],[zip_derived_cl1913]) ).
thf(zip_derived_cl193_015,plain,
xp != sz00,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl1915,plain,
( ( sk_ @ xp @ sz00 )
= sz00 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1914,zip_derived_cl193]) ).
thf(zip_derived_cl1952,plain,
( ( sdtasdt0 @ xp @ sz00 )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl1692,zip_derived_cl1915]) ).
thf(zip_derived_cl4090,plain,
( sz00
= ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3643,zip_derived_cl4059,zip_derived_cl1952]) ).
thf(zip_derived_cl10_016,plain,
! [X0: $i] :
( ( ( sdtpldt0 @ X0 @ ( smndt0 @ X0 ) )
= sz00 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mAddNeg]) ).
thf(mAddAsso,axiom,
! [W0: $i,W1: $i,W2: $i] :
( ( ( aInteger0 @ W0 )
& ( aInteger0 @ W1 )
& ( aInteger0 @ W2 ) )
=> ( ( sdtpldt0 @ W0 @ ( sdtpldt0 @ W1 @ W2 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ W0 @ W1 ) @ W2 ) ) ) ).
thf(zip_derived_cl6,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mAddAsso]) ).
thf(zip_derived_cl337,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ ( sdtpldt0 @ X1 @ X0 ) )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ X1 @ X0 ) ) )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ ( smndt0 @ ( sdtpldt0 @ X1 @ X0 ) ) ) )
= sz00 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl10,zip_derived_cl6]) ).
thf(mIntPlus,axiom,
! [W0: $i,W1: $i] :
( ( ( aInteger0 @ W0 )
& ( aInteger0 @ W1 ) )
=> ( aInteger0 @ ( sdtpldt0 @ W0 @ W1 ) ) ) ).
thf(zip_derived_cl4,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtpldt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntPlus]) ).
thf(zip_derived_cl5773,plain,
! [X0: $i,X1: $i] :
( ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ ( smndt0 @ ( sdtpldt0 @ X1 @ X0 ) ) ) )
= sz00 )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ X1 @ X0 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(clc,[status(thm)],[zip_derived_cl337,zip_derived_cl4]) ).
thf(zip_derived_cl5792,plain,
( ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz00 ) ) )
= sz00 )
| ~ ( aInteger0 @ ( smndt0 @ sz00 ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl4090,zip_derived_cl5773]) ).
thf(mMulMinOne,axiom,
! [W0: $i] :
( ( aInteger0 @ W0 )
=> ( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ W0 )
= ( smndt0 @ W0 ) )
& ( ( smndt0 @ W0 )
= ( sdtasdt0 @ W0 @ ( smndt0 @ sz10 ) ) ) ) ) ).
thf(zip_derived_cl20,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(mMulZero,axiom,
! [W0: $i] :
( ( aInteger0 @ W0 )
=> ( ( ( sdtasdt0 @ W0 @ sz00 )
= sz00 )
& ( sz00
= ( sdtasdt0 @ sz00 @ W0 ) ) ) ) ).
thf(zip_derived_cl18,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ X0 @ sz00 )
= sz00 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulZero]) ).
thf(zip_derived_cl343,plain,
( ~ ( aInteger0 @ sz00 )
| ( ( smndt0 @ sz00 )
= sz00 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl20,zip_derived_cl18]) ).
thf(zip_derived_cl1_017,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(m__2079,axiom,
( ( ( stldt0 @ ( sbsmnsldt0 @ xS ) )
= cS2076 )
& ! [W0: $i] :
( ( aElementOf0 @ W0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) )
<=> ( ( W0 = sz10 )
| ( W0
= ( smndt0 @ sz10 ) ) ) )
& ! [W0: $i] :
( ( aElementOf0 @ W0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) )
<=> ( ( aInteger0 @ W0 )
& ~ ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) ) )
& ( aSet0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) )
& ! [W0: $i] :
( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) )
<=> ( ( aInteger0 @ W0 )
& ? [W1: $i] :
( ( aElementOf0 @ W0 @ W1 )
& ( aElementOf0 @ W1 @ xS ) ) ) )
& ( aSet0 @ ( sbsmnsldt0 @ xS ) ) ) ).
thf(zip_derived_cl145,plain,
! [X0: $i] :
( ( aElementOf0 @ X0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) )
| ( X0
!= ( smndt0 @ sz10 ) ) ),
inference(cnf,[status(esa)],[m__2079]) ).
thf(zip_derived_cl147,plain,
( ( stldt0 @ ( sbsmnsldt0 @ xS ) )
= cS2076 ),
inference(cnf,[status(esa)],[m__2079]) ).
thf(zip_derived_cl236,plain,
! [X0: $i] :
( ( aElementOf0 @ X0 @ cS2076 )
| ( X0
!= ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl145,zip_derived_cl147]) ).
thf(zip_derived_cl289,plain,
aElementOf0 @ ( smndt0 @ sz10 ) @ cS2076,
inference(eq_res,[status(thm)],[zip_derived_cl236]) ).
thf(zip_derived_cl142,plain,
! [X0: $i] :
( ( aInteger0 @ X0 )
| ~ ( aElementOf0 @ X0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) ),
inference(cnf,[status(esa)],[m__2079]) ).
thf(zip_derived_cl147_018,plain,
( ( stldt0 @ ( sbsmnsldt0 @ xS ) )
= cS2076 ),
inference(cnf,[status(esa)],[m__2079]) ).
thf(zip_derived_cl228,plain,
! [X0: $i] :
( ( aInteger0 @ X0 )
| ~ ( aElementOf0 @ X0 @ cS2076 ) ),
inference(demod,[status(thm)],[zip_derived_cl142,zip_derived_cl147]) ).
thf(zip_derived_cl291,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl344,plain,
( ( smndt0 @ sz00 )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl343,zip_derived_cl1,zip_derived_cl291]) ).
thf(zip_derived_cl344_019,plain,
( ( smndt0 @ sz00 )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl343,zip_derived_cl1,zip_derived_cl291]) ).
thf(zip_derived_cl1_020,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl2_021,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl291_022,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl5873,plain,
( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ sz00 ) )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl5792,zip_derived_cl344,zip_derived_cl344,zip_derived_cl1,zip_derived_cl2,zip_derived_cl291]) ).
thf(zip_derived_cl5950,plain,
( ~ ( aInteger0 @ sz00 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz00 @ ( smndt0 @ sz10 ) ) )
= sz00 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl7,zip_derived_cl5873]) ).
thf(zip_derived_cl1_023,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl291_024,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl5955,plain,
( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz00 @ ( smndt0 @ sz10 ) ) )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl5950,zip_derived_cl1,zip_derived_cl291]) ).
thf(zip_derived_cl7_025,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ X0 @ X1 )
= ( sdtpldt0 @ X1 @ X0 ) ) ),
inference(cnf,[status(esa)],[mAddComm]) ).
thf(zip_derived_cl6_026,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mAddAsso]) ).
thf(zip_derived_cl295,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ ( sdtpldt0 @ X1 @ X0 ) )
| ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl7,zip_derived_cl6]) ).
thf(zip_derived_cl301,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ ( sdtpldt0 @ X1 @ X0 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl295]) ).
thf(zip_derived_cl4_027,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtpldt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntPlus]) ).
thf(zip_derived_cl4969,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl301,zip_derived_cl4]) ).
thf(zip_derived_cl5983,plain,
( ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ sz00 )
| ( ( sdtpldt0 @ sz00 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ sz10 ) )
= sz00 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl5955,zip_derived_cl4969]) ).
thf(zip_derived_cl2_028,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl291_029,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl1_030,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl6000,plain,
( ( sdtpldt0 @ sz00 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ sz10 ) )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl5983,zip_derived_cl2,zip_derived_cl291,zip_derived_cl1]) ).
thf(mAddZero,axiom,
! [W0: $i] :
( ( aInteger0 @ W0 )
=> ( ( ( sdtpldt0 @ W0 @ sz00 )
= W0 )
& ( W0
= ( sdtpldt0 @ sz00 @ W0 ) ) ) ) ).
thf(zip_derived_cl9,plain,
! [X0: $i] :
( ( X0
= ( sdtpldt0 @ sz00 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mAddZero]) ).
thf(zip_derived_cl6_031,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mAddAsso]) ).
thf(zip_derived_cl323,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ sz00 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ sz00 @ ( sdtpldt0 @ X0 @ X1 ) )
= ( sdtpldt0 @ X0 @ X1 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl9,zip_derived_cl6]) ).
thf(zip_derived_cl1_032,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl329,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ sz00 @ ( sdtpldt0 @ X0 @ X1 ) )
= ( sdtpldt0 @ X0 @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl323,zip_derived_cl1]) ).
thf(zip_derived_cl330,plain,
! [X0: $i,X1: $i] :
( ( ( sdtpldt0 @ sz00 @ ( sdtpldt0 @ X0 @ X1 ) )
= ( sdtpldt0 @ X0 @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl329]) ).
thf(zip_derived_cl6180,plain,
( ( sz00
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ sz10 ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl6000,zip_derived_cl330]) ).
thf(zip_derived_cl2_033,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl291_034,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl6212,plain,
( sz00
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl6180,zip_derived_cl2,zip_derived_cl291]) ).
thf(zip_derived_cl10_035,plain,
! [X0: $i] :
( ( ( sdtpldt0 @ X0 @ ( smndt0 @ X0 ) )
= sz00 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mAddNeg]) ).
thf(zip_derived_cl6_036,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mAddAsso]) ).
thf(zip_derived_cl335,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ ( smndt0 @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ ( smndt0 @ X1 ) @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl10,zip_derived_cl6]) ).
thf(zip_derived_cl340,plain,
! [X0: $i,X1: $i] :
( ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ ( smndt0 @ X1 ) @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ ( smndt0 @ X1 ) )
| ~ ( aInteger0 @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl335]) ).
thf(mIntNeg,axiom,
! [W0: $i] :
( ( aInteger0 @ W0 )
=> ( aInteger0 @ ( smndt0 @ W0 ) ) ) ).
thf(zip_derived_cl3,plain,
! [X0: $i] :
( ( aInteger0 @ ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mIntNeg]) ).
thf(zip_derived_cl6001,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ ( smndt0 @ X1 ) @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl340,zip_derived_cl3]) ).
thf(zip_derived_cl6230,plain,
( ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ sz10 )
| ( ( sdtpldt0 @ sz10 @ sz00 )
= ( sdtpldt0 @ sz00 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl6212,zip_derived_cl6001]) ).
thf(zip_derived_cl2_037,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl2_038,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl6253,plain,
( ( sdtpldt0 @ sz10 @ sz00 )
= ( sdtpldt0 @ sz00 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl6230,zip_derived_cl2,zip_derived_cl2]) ).
thf(zip_derived_cl8,plain,
! [X0: $i] :
( ( ( sdtpldt0 @ X0 @ sz00 )
= X0 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mAddZero]) ).
thf(zip_derived_cl6302,plain,
( ( ( sdtpldt0 @ sz00 @ sz10 )
= sz10 )
| ~ ( aInteger0 @ sz10 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl6253,zip_derived_cl8]) ).
thf(zip_derived_cl2_039,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl6317,plain,
( ( sdtpldt0 @ sz00 @ sz10 )
= sz10 ),
inference(demod,[status(thm)],[zip_derived_cl6302,zip_derived_cl2]) ).
thf(zip_derived_cl1574_040,plain,
aElementOf0 @ sz10 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1573,zip_derived_cl193]) ).
thf(zip_derived_cl201_041,plain,
! [X0: $i] :
( ( aDivisorOf0 @ xp @ ( sdtpldt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aElementOf0 @ X0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) ) ),
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl1618,plain,
aDivisorOf0 @ xp @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1574,zip_derived_cl201]) ).
thf(zip_derived_cl24_042,plain,
! [X0: $i,X1: $i] :
( ~ ( aDivisorOf0 @ X0 @ X1 )
| ( ( sdtasdt0 @ X0 @ ( sk_ @ X0 @ X1 ) )
= X1 )
| ~ ( aInteger0 @ X1 ) ),
inference(cnf,[status(esa)],[mDivisor]) ).
thf(zip_derived_cl1673,plain,
( ( ( sdtasdt0 @ xp @ ( sk_ @ xp @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ) )
= ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1618,zip_derived_cl24]) ).
thf(mDistrib,axiom,
! [W0: $i,W1: $i,W2: $i] :
( ( ( aInteger0 @ W0 )
& ( aInteger0 @ W1 )
& ( aInteger0 @ W2 ) )
=> ( ( ( sdtasdt0 @ W0 @ ( sdtpldt0 @ W1 @ W2 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ W0 @ W1 ) @ ( sdtasdt0 @ W0 @ W2 ) ) )
& ( ( sdtasdt0 @ ( sdtpldt0 @ W0 @ W1 ) @ W2 )
= ( sdtpldt0 @ ( sdtasdt0 @ W0 @ W2 ) @ ( sdtasdt0 @ W1 @ W2 ) ) ) ) ) ).
thf(zip_derived_cl16,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ X0 ) @ ( sdtasdt0 @ X1 @ X2 ) ) ) ),
inference(cnf,[status(esa)],[mDistrib]) ).
thf(zip_derived_cl1853,plain,
! [X0: $i] :
( ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ ( sk_ @ xp @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ) )
| ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ xp @ ( sdtpldt0 @ ( sk_ @ xp @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ) @ X0 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) @ ( sdtasdt0 @ xp @ X0 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1673,zip_derived_cl16]) ).
thf(zip_derived_cl192_043,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl1871,plain,
! [X0: $i] :
( ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ ( sk_ @ xp @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ) )
| ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ xp @ ( sdtpldt0 @ ( sk_ @ xp @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ) @ X0 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) @ ( sdtasdt0 @ xp @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1853,zip_derived_cl192]) ).
thf(zip_derived_cl4090_044,plain,
( sz00
= ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3643,zip_derived_cl4059,zip_derived_cl1952]) ).
thf(zip_derived_cl1_045,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl4090_046,plain,
( sz00
= ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3643,zip_derived_cl4059,zip_derived_cl1952]) ).
thf(zip_derived_cl1915_047,plain,
( ( sk_ @ xp @ sz00 )
= sz00 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1914,zip_derived_cl193]) ).
thf(zip_derived_cl1_048,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl4090_049,plain,
( sz00
= ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3643,zip_derived_cl4059,zip_derived_cl1952]) ).
thf(zip_derived_cl1915_050,plain,
( ( sk_ @ xp @ sz00 )
= sz00 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1914,zip_derived_cl193]) ).
thf(zip_derived_cl4090_051,plain,
( sz00
= ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3643,zip_derived_cl4059,zip_derived_cl1952]) ).
thf(zip_derived_cl54755,plain,
! [X0: $i] :
( ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ xp @ ( sdtpldt0 @ sz00 @ X0 ) )
= ( sdtpldt0 @ sz00 @ ( sdtasdt0 @ xp @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1871,zip_derived_cl4090,zip_derived_cl1,zip_derived_cl4090,zip_derived_cl1915,zip_derived_cl1,zip_derived_cl4090,zip_derived_cl1915,zip_derived_cl4090]) ).
thf(zip_derived_cl54856,plain,
( ~ ( aInteger0 @ sz10 )
| ( ( sdtasdt0 @ xp @ sz10 )
= ( sdtpldt0 @ sz00 @ ( sdtasdt0 @ xp @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl6317,zip_derived_cl54755]) ).
thf(zip_derived_cl2_052,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl54874,plain,
( ( sdtasdt0 @ xp @ sz10 )
= ( sdtpldt0 @ sz00 @ ( sdtasdt0 @ xp @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl54856,zip_derived_cl2]) ).
thf(zip_derived_cl54999,plain,
( ~ ( aInteger0 @ xp )
| ( xp
= ( sdtpldt0 @ sz00 @ xp ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl14,zip_derived_cl54874]) ).
thf(zip_derived_cl192_053,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl55004,plain,
( xp
= ( sdtpldt0 @ sz00 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl54999,zip_derived_cl192]) ).
thf(zip_derived_cl14_054,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ X0 @ sz10 )
= X0 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulOne]) ).
thf(zip_derived_cl17,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ ( sdtpldt0 @ X1 @ X0 ) @ X2 )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ X2 ) @ ( sdtasdt0 @ X0 @ X2 ) ) ) ),
inference(cnf,[status(esa)],[mDistrib]) ).
thf(zip_derived_cl549,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ sz10 )
| ( ( sdtasdt0 @ ( sdtpldt0 @ X1 @ X0 ) @ sz10 )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ sz10 ) @ X0 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl14,zip_derived_cl17]) ).
thf(zip_derived_cl2_055,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl568,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ ( sdtpldt0 @ X1 @ X0 ) @ sz10 )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ sz10 ) @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl549,zip_derived_cl2]) ).
thf(zip_derived_cl569,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ ( sdtpldt0 @ X1 @ X0 ) @ sz10 )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ sz10 ) @ X0 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl568]) ).
thf(zip_derived_cl55257,plain,
( ( ( sdtasdt0 @ xp @ sz10 )
= ( sdtpldt0 @ ( sdtasdt0 @ sz00 @ sz10 ) @ xp ) )
| ~ ( aInteger0 @ sz00 )
| ~ ( aInteger0 @ xp ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55004,zip_derived_cl569]) ).
thf(zip_derived_cl1952_056,plain,
( ( sdtasdt0 @ xp @ sz00 )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl1692,zip_derived_cl1915]) ).
thf(mMulComm,axiom,
! [W0: $i,W1: $i] :
( ( ( aInteger0 @ W0 )
& ( aInteger0 @ W1 ) )
=> ( ( sdtasdt0 @ W0 @ W1 )
= ( sdtasdt0 @ W1 @ W0 ) ) ) ).
thf(zip_derived_cl13,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ X0 @ X1 )
= ( sdtasdt0 @ X1 @ X0 ) ) ),
inference(cnf,[status(esa)],[mMulComm]) ).
thf(zip_derived_cl1959,plain,
( ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ sz00 )
| ( sz00
= ( sdtasdt0 @ sz00 @ xp ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1952,zip_derived_cl13]) ).
thf(zip_derived_cl192_057,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl1_058,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl1972,plain,
( sz00
= ( sdtasdt0 @ sz00 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl1959,zip_derived_cl192,zip_derived_cl1]) ).
thf(zip_derived_cl19,plain,
! [X0: $i] :
( ( sz00
= ( sdtasdt0 @ sz00 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulZero]) ).
thf(mMulAsso,axiom,
! [W0: $i,W1: $i,W2: $i] :
( ( ( aInteger0 @ W0 )
& ( aInteger0 @ W1 )
& ( aInteger0 @ W2 ) )
=> ( ( sdtasdt0 @ W0 @ ( sdtasdt0 @ W1 @ W2 ) )
= ( sdtasdt0 @ ( sdtasdt0 @ W0 @ W1 ) @ W2 ) ) ) ).
thf(zip_derived_cl12,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ X1 @ ( sdtasdt0 @ X0 @ X2 ) )
= ( sdtasdt0 @ ( sdtasdt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mMulAsso]) ).
thf(zip_derived_cl410,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ sz00 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ sz00 @ ( sdtasdt0 @ X1 @ X0 ) )
= ( sdtasdt0 @ sz00 @ X0 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl19,zip_derived_cl12]) ).
thf(zip_derived_cl1_059,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl423,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ sz00 @ ( sdtasdt0 @ X1 @ X0 ) )
= ( sdtasdt0 @ sz00 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl410,zip_derived_cl1]) ).
thf(zip_derived_cl424,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ sz00 @ ( sdtasdt0 @ X1 @ X0 ) )
= ( sdtasdt0 @ sz00 @ X0 ) )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl423]) ).
thf(zip_derived_cl7745,plain,
( ( ( sdtasdt0 @ sz00 @ sz00 )
= sz00 )
| ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ sz00 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl1972,zip_derived_cl424]) ).
thf(zip_derived_cl192_060,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl1_061,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl7769,plain,
( ( sdtasdt0 @ sz00 @ sz00 )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl7745,zip_derived_cl192,zip_derived_cl1]) ).
thf(zip_derived_cl15,plain,
! [X0: $i] :
( ( X0
= ( sdtasdt0 @ sz10 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulOne]) ).
thf(zip_derived_cl12_062,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ X1 @ ( sdtasdt0 @ X0 @ X2 ) )
= ( sdtasdt0 @ ( sdtasdt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mMulAsso]) ).
thf(zip_derived_cl411,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ sz10 @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ X0 @ X1 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl15,zip_derived_cl12]) ).
thf(zip_derived_cl2_063,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl425,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ sz10 @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ X0 @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl411,zip_derived_cl2]) ).
thf(zip_derived_cl426,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ sz10 @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ X0 @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl425]) ).
thf(zip_derived_cl7884,plain,
( ( ( sdtasdt0 @ sz10 @ sz00 )
= sz00 )
| ~ ( aInteger0 @ sz00 )
| ~ ( aInteger0 @ sz00 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl7769,zip_derived_cl426]) ).
thf(zip_derived_cl1_064,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl1_065,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl7910,plain,
( ( sdtasdt0 @ sz10 @ sz00 )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl7884,zip_derived_cl1,zip_derived_cl1]) ).
thf(zip_derived_cl13_066,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ X0 @ X1 )
= ( sdtasdt0 @ X1 @ X0 ) ) ),
inference(cnf,[status(esa)],[mMulComm]) ).
thf(zip_derived_cl7942,plain,
( ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ sz00 )
| ( sz00
= ( sdtasdt0 @ sz00 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl7910,zip_derived_cl13]) ).
thf(zip_derived_cl2_067,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl1_068,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl7961,plain,
( sz00
= ( sdtasdt0 @ sz00 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl7942,zip_derived_cl2,zip_derived_cl1]) ).
thf(zip_derived_cl55004_069,plain,
( xp
= ( sdtpldt0 @ sz00 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl54999,zip_derived_cl192]) ).
thf(zip_derived_cl1_070,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl192_071,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl55291,plain,
( ( sdtasdt0 @ xp @ sz10 )
= xp ),
inference(demod,[status(thm)],[zip_derived_cl55257,zip_derived_cl7961,zip_derived_cl55004,zip_derived_cl1,zip_derived_cl192]) ).
thf(zip_derived_cl20_072,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl12_073,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ X1 @ ( sdtasdt0 @ X0 @ X2 ) )
= ( sdtasdt0 @ ( sdtasdt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mMulAsso]) ).
thf(zip_derived_cl412,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl20,zip_derived_cl12]) ).
thf(zip_derived_cl291_074,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl427,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl412,zip_derived_cl291]) ).
thf(zip_derived_cl428,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl427]) ).
thf(zip_derived_cl55518,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ xp )
= ( sdtasdt0 @ ( smndt0 @ xp ) @ sz10 ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ xp ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55291,zip_derived_cl428]) ).
thf(zip_derived_cl2_075,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl192_076,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl55594,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ xp )
= ( sdtasdt0 @ ( smndt0 @ xp ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl55518,zip_derived_cl2,zip_derived_cl192]) ).
thf(zip_derived_cl14_077,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ X0 @ sz10 )
= X0 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulOne]) ).
thf(zip_derived_cl428_078,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl427]) ).
thf(zip_derived_cl8044,plain,
! [X0: $i] :
( ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ sz10 ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl14,zip_derived_cl428]) ).
thf(zip_derived_cl2_079,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl8070,plain,
! [X0: $i] :
( ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ sz10 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl8044,zip_derived_cl2]) ).
thf(zip_derived_cl8071,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ sz10 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl8070]) ).
thf(zip_derived_cl20_080,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl8564,plain,
! [X0: $i] :
( ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ ( smndt0 @ X0 ) @ sz10 )
= ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl8071,zip_derived_cl20]) ).
thf(zip_derived_cl8633,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ X0 ) @ sz10 )
= ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl8564]) ).
thf(zip_derived_cl55745,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ xp )
= ( smndt0 @ xp ) )
| ~ ( aInteger0 @ xp ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55594,zip_derived_cl8633]) ).
thf(zip_derived_cl192_081,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl55812,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ xp )
= ( smndt0 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl55745,zip_derived_cl192]) ).
thf(zip_derived_cl55812_082,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ xp )
= ( smndt0 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl55745,zip_derived_cl192]) ).
thf(zip_derived_cl21,plain,
! [X0: $i] :
( ( ( smndt0 @ X0 )
= ( sdtasdt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl16_083,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ X0 ) @ ( sdtasdt0 @ X1 @ X2 ) ) ) ),
inference(cnf,[status(esa)],[mDistrib]) ).
thf(zip_derived_cl492,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ ( smndt0 @ X0 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl21,zip_derived_cl16]) ).
thf(zip_derived_cl291_084,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl512,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ ( smndt0 @ X0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl492,zip_derived_cl291]) ).
thf(zip_derived_cl513,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ ( smndt0 @ X0 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl512]) ).
thf(zip_derived_cl55828,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ xp @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ xp ) @ ( smndt0 @ ( smndt0 @ sz10 ) ) ) )
| ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55812,zip_derived_cl513]) ).
thf(zip_derived_cl3_085,plain,
! [X0: $i] :
( ( aInteger0 @ ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mIntNeg]) ).
thf(zip_derived_cl6212_086,plain,
( sz00
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl6180,zip_derived_cl2,zip_derived_cl291]) ).
thf(zip_derived_cl11,plain,
! [X0: $i] :
( ( sz00
= ( sdtpldt0 @ ( smndt0 @ X0 ) @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mAddNeg]) ).
thf(zip_derived_cl6_087,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mAddAsso]) ).
thf(zip_derived_cl369,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ ( smndt0 @ X1 ) )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ ( smndt0 @ X1 ) @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11,zip_derived_cl6]) ).
thf(zip_derived_cl377,plain,
! [X0: $i,X1: $i] :
( ( ( sdtpldt0 @ ( smndt0 @ X1 ) @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ ( smndt0 @ X1 ) )
| ~ ( aInteger0 @ X1 ) ),
inference(simplify,[status(thm)],[zip_derived_cl369]) ).
thf(zip_derived_cl3_088,plain,
! [X0: $i] :
( ( aInteger0 @ ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mIntNeg]) ).
thf(zip_derived_cl6576,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ ( smndt0 @ X1 ) @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl377,zip_derived_cl3]) ).
thf(zip_derived_cl6626,plain,
( ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ sz10 )
| ( ( sdtpldt0 @ ( smndt0 @ ( smndt0 @ sz10 ) ) @ sz00 )
= ( sdtpldt0 @ sz00 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl6212,zip_derived_cl6576]) ).
thf(zip_derived_cl291_089,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl2_090,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl6317_091,plain,
( ( sdtpldt0 @ sz00 @ sz10 )
= sz10 ),
inference(demod,[status(thm)],[zip_derived_cl6302,zip_derived_cl2]) ).
thf(zip_derived_cl6665,plain,
( ( sdtpldt0 @ ( smndt0 @ ( smndt0 @ sz10 ) ) @ sz00 )
= sz10 ),
inference(demod,[status(thm)],[zip_derived_cl6626,zip_derived_cl291,zip_derived_cl2,zip_derived_cl6317]) ).
thf(zip_derived_cl8_092,plain,
! [X0: $i] :
( ( ( sdtpldt0 @ X0 @ sz00 )
= X0 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mAddZero]) ).
thf(zip_derived_cl6740,plain,
( ( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ ( smndt0 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl6665,zip_derived_cl8]) ).
thf(zip_derived_cl6783,plain,
( ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl3,zip_derived_cl6740]) ).
thf(zip_derived_cl291_093,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl6788,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl192_094,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl291_095,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl55918,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ xp @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ xp ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl55828,zip_derived_cl6788,zip_derived_cl192,zip_derived_cl291]) ).
thf(zip_derived_cl7_096,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ X0 @ X1 )
= ( sdtpldt0 @ X1 @ X0 ) ) ),
inference(cnf,[status(esa)],[mAddComm]) ).
thf(zip_derived_cl55812_097,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ xp )
= ( smndt0 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl55745,zip_derived_cl192]) ).
thf(zip_derived_cl21_098,plain,
! [X0: $i] :
( ( ( smndt0 @ X0 )
= ( sdtasdt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl16_099,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ X0 ) @ ( sdtasdt0 @ X1 @ X2 ) ) ) ),
inference(cnf,[status(esa)],[mDistrib]) ).
thf(zip_derived_cl501,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ X1 ) )
= ( sdtpldt0 @ ( smndt0 @ X0 ) @ ( sdtasdt0 @ X0 @ X1 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl21,zip_derived_cl16]) ).
thf(zip_derived_cl291_100,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl527,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ X1 ) )
= ( sdtpldt0 @ ( smndt0 @ X0 ) @ ( sdtasdt0 @ X0 @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl501,zip_derived_cl291]) ).
thf(zip_derived_cl528,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ X1 ) )
= ( sdtpldt0 @ ( smndt0 @ X0 ) @ ( sdtasdt0 @ X0 @ X1 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl527]) ).
thf(zip_derived_cl55830,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ xp ) )
= ( sdtpldt0 @ ( smndt0 @ ( smndt0 @ sz10 ) ) @ ( smndt0 @ xp ) ) )
| ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55812,zip_derived_cl528]) ).
thf(zip_derived_cl6788_101,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl192_102,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl291_103,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl55920,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ xp ) )
= ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) ),
inference(demod,[status(thm)],[zip_derived_cl55830,zip_derived_cl6788,zip_derived_cl192,zip_derived_cl291]) ).
thf(zip_derived_cl59264,plain,
( ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ xp @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl7,zip_derived_cl55920]) ).
thf(zip_derived_cl192_104,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl291_105,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl59266,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ xp @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) ),
inference(demod,[status(thm)],[zip_derived_cl59264,zip_derived_cl192,zip_derived_cl291]) ).
thf(zip_derived_cl60196,plain,
( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= ( sdtpldt0 @ ( smndt0 @ xp ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl55918,zip_derived_cl59266]) ).
thf(zip_derived_cl6576_106,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ ( smndt0 @ X1 ) @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl377,zip_derived_cl3]) ).
thf(zip_derived_cl60353,plain,
( ~ ( aInteger0 @ ( smndt0 @ xp ) )
| ~ ( aInteger0 @ sz10 )
| ( ( sdtpldt0 @ ( smndt0 @ ( smndt0 @ xp ) ) @ ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) )
= ( sdtpldt0 @ sz00 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl60196,zip_derived_cl6576]) ).
thf(zip_derived_cl55812_107,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ xp )
= ( smndt0 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl55745,zip_derived_cl192]) ).
thf(mIntMult,axiom,
! [W0: $i,W1: $i] :
( ( ( aInteger0 @ W0 )
& ( aInteger0 @ W1 ) )
=> ( aInteger0 @ ( sdtasdt0 @ W0 @ W1 ) ) ) ).
thf(zip_derived_cl5,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtasdt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntMult]) ).
thf(zip_derived_cl55822,plain,
( ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ xp )
| ( aInteger0 @ ( smndt0 @ xp ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55812,zip_derived_cl5]) ).
thf(zip_derived_cl291_108,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl192_109,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl55911,plain,
aInteger0 @ ( smndt0 @ xp ),
inference(demod,[status(thm)],[zip_derived_cl55822,zip_derived_cl291,zip_derived_cl192]) ).
thf(zip_derived_cl2_110,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl55812_111,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ xp )
= ( smndt0 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl55745,zip_derived_cl192]) ).
thf(zip_derived_cl428_112,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl427]) ).
thf(zip_derived_cl55826,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ xp ) )
= ( sdtasdt0 @ ( smndt0 @ ( smndt0 @ sz10 ) ) @ xp ) )
| ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55812,zip_derived_cl428]) ).
thf(zip_derived_cl6788_113,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl55004_114,plain,
( xp
= ( sdtpldt0 @ sz00 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl54999,zip_derived_cl192]) ).
thf(zip_derived_cl15_115,plain,
! [X0: $i] :
( ( X0
= ( sdtasdt0 @ sz10 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulOne]) ).
thf(zip_derived_cl16_116,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ X0 ) @ ( sdtasdt0 @ X1 @ X2 ) ) ) ),
inference(cnf,[status(esa)],[mDistrib]) ).
thf(zip_derived_cl494,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ sz10 @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ sz10 @ X1 ) @ X0 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl15,zip_derived_cl16]) ).
thf(zip_derived_cl2_117,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl516,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ sz10 @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ sz10 @ X1 ) @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl494,zip_derived_cl2]) ).
thf(zip_derived_cl517,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ sz10 @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ sz10 @ X1 ) @ X0 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl516]) ).
thf(zip_derived_cl55254,plain,
( ( ( sdtasdt0 @ sz10 @ xp )
= ( sdtpldt0 @ ( sdtasdt0 @ sz10 @ sz00 ) @ xp ) )
| ~ ( aInteger0 @ sz00 )
| ~ ( aInteger0 @ xp ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55004,zip_derived_cl517]) ).
thf(zip_derived_cl7910_118,plain,
( ( sdtasdt0 @ sz10 @ sz00 )
= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl7884,zip_derived_cl1,zip_derived_cl1]) ).
thf(zip_derived_cl55004_119,plain,
( xp
= ( sdtpldt0 @ sz00 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl54999,zip_derived_cl192]) ).
thf(zip_derived_cl1_120,plain,
aInteger0 @ sz00,
inference(cnf,[status(esa)],[mIntZero]) ).
thf(zip_derived_cl192_121,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl55288,plain,
( ( sdtasdt0 @ sz10 @ xp )
= xp ),
inference(demod,[status(thm)],[zip_derived_cl55254,zip_derived_cl7910,zip_derived_cl55004,zip_derived_cl1,zip_derived_cl192]) ).
thf(zip_derived_cl192_122,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl291_123,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl55916,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ xp ) )
= xp ),
inference(demod,[status(thm)],[zip_derived_cl55826,zip_derived_cl6788,zip_derived_cl55288,zip_derived_cl192,zip_derived_cl291]) ).
thf(zip_derived_cl20_124,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl56945,plain,
( ( xp
= ( smndt0 @ ( smndt0 @ xp ) ) )
| ~ ( aInteger0 @ ( smndt0 @ xp ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55916,zip_derived_cl20]) ).
thf(zip_derived_cl55911_125,plain,
aInteger0 @ ( smndt0 @ xp ),
inference(demod,[status(thm)],[zip_derived_cl55822,zip_derived_cl291,zip_derived_cl192]) ).
thf(zip_derived_cl57022,plain,
( xp
= ( smndt0 @ ( smndt0 @ xp ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56945,zip_derived_cl55911]) ).
thf(zip_derived_cl6317_126,plain,
( ( sdtpldt0 @ sz00 @ sz10 )
= sz10 ),
inference(demod,[status(thm)],[zip_derived_cl6302,zip_derived_cl2]) ).
thf(zip_derived_cl60392,plain,
( ( sdtpldt0 @ xp @ ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) )
= sz10 ),
inference(demod,[status(thm)],[zip_derived_cl60353,zip_derived_cl55911,zip_derived_cl2,zip_derived_cl57022,zip_derived_cl6317]) ).
thf(zip_derived_cl6788_127,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl8071_128,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ sz10 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl8070]) ).
thf(zip_derived_cl8567,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= ( sdtasdt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl6788,zip_derived_cl8071]) ).
thf(zip_derived_cl291_129,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl8569,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= ( sdtasdt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl8567,zip_derived_cl291]) ).
thf(zip_derived_cl8569_130,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= ( sdtasdt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl8567,zip_derived_cl291]) ).
thf(zip_derived_cl21_131,plain,
! [X0: $i] :
( ( ( smndt0 @ X0 )
= ( sdtasdt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl8736,plain,
( ( ( smndt0 @ ( smndt0 @ sz10 ) )
= ( sdtasdt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl8569,zip_derived_cl21]) ).
thf(zip_derived_cl6788_132,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl291_133,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl8761,plain,
( sz10
= ( sdtasdt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl8736,zip_derived_cl6788,zip_derived_cl291]) ).
thf(zip_derived_cl8765,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= sz10 ),
inference(demod,[status(thm)],[zip_derived_cl8569,zip_derived_cl8761]) ).
thf(zip_derived_cl513_134,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ ( smndt0 @ X0 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl512]) ).
thf(zip_derived_cl11102,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ ( smndt0 @ ( smndt0 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl8765,zip_derived_cl513]) ).
thf(zip_derived_cl6788_135,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl291_136,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl291_137,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl11151,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11102,zip_derived_cl6788,zip_derived_cl291,zip_derived_cl291]) ).
thf(zip_derived_cl20_138,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl11238,plain,
( ( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11151,zip_derived_cl20]) ).
thf(zip_derived_cl8071_139,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ sz10 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl8070]) ).
thf(zip_derived_cl20_140,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl8537,plain,
( ~ ( aInteger0 @ sz10 )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ sz10 )
= ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ sz10 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl8071,zip_derived_cl20]) ).
thf(zip_derived_cl2_141,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl2_142,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl8588,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ sz10 )
= ( smndt0 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl8537,zip_derived_cl2,zip_derived_cl2]) ).
thf(zip_derived_cl14_143,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ X0 @ sz10 )
= X0 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulOne]) ).
thf(zip_derived_cl16_144,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ X0 ) @ ( sdtasdt0 @ X1 @ X2 ) ) ) ),
inference(cnf,[status(esa)],[mDistrib]) ).
thf(zip_derived_cl491,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ sz10 )
| ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ sz10 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ X0 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl14,zip_derived_cl16]) ).
thf(zip_derived_cl2_145,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl510,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ sz10 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl491,zip_derived_cl2]) ).
thf(zip_derived_cl511,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ sz10 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ X0 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl510]) ).
thf(zip_derived_cl10698,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl8588,zip_derived_cl511]) ).
thf(zip_derived_cl2_146,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl291_147,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl10742,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl10698,zip_derived_cl2,zip_derived_cl291]) ).
thf(zip_derived_cl16_148,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ X0 ) @ ( sdtasdt0 @ X1 @ X2 ) ) ) ),
inference(cnf,[status(esa)],[mDistrib]) ).
thf(zip_derived_cl4_149,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtpldt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntPlus]) ).
thf(zip_derived_cl484,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ ( sdtasdt0 @ X2 @ X1 ) )
| ~ ( aInteger0 @ ( sdtasdt0 @ X2 @ X0 ) )
| ( aInteger0 @ ( sdtasdt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl16,zip_derived_cl4]) ).
thf(zip_derived_cl5_150,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtasdt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntMult]) ).
thf(zip_derived_cl9453,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( aInteger0 @ ( sdtasdt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) )
| ~ ( aInteger0 @ ( sdtasdt0 @ X2 @ X0 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X0 ) ),
inference(clc,[status(thm)],[zip_derived_cl484,zip_derived_cl5]) ).
thf(zip_derived_cl5_151,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtasdt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntMult]) ).
thf(zip_derived_cl9454,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtasdt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl9453,zip_derived_cl5]) ).
thf(zip_derived_cl10961,plain,
( ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ sz10 )
| ( aInteger0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl10742,zip_derived_cl9454]) ).
thf(zip_derived_cl2_152,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl291_153,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl2_154,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl10995,plain,
aInteger0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10961,zip_derived_cl2,zip_derived_cl291,zip_derived_cl2]) ).
thf(zip_derived_cl11273,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11238,zip_derived_cl10995]) ).
thf(zip_derived_cl21_155,plain,
! [X0: $i] :
( ( ( smndt0 @ X0 )
= ( sdtasdt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl428_156,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl427]) ).
thf(zip_derived_cl8045,plain,
! [X0: $i] :
( ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ X0 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ X0 ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl21,zip_derived_cl428]) ).
thf(zip_derived_cl291_157,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl8072,plain,
! [X0: $i] :
( ~ ( aInteger0 @ X0 )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ X0 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl8045,zip_derived_cl291]) ).
thf(zip_derived_cl8073,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ X0 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl8072]) ).
thf(zip_derived_cl11469,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11273,zip_derived_cl8073]) ).
thf(zip_derived_cl10742_158,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl10698,zip_derived_cl2,zip_derived_cl291]) ).
thf(zip_derived_cl10995_159,plain,
aInteger0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10961,zip_derived_cl2,zip_derived_cl291,zip_derived_cl2]) ).
thf(zip_derived_cl11492,plain,
( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11469,zip_derived_cl10742,zip_derived_cl10995]) ).
thf(zip_derived_cl428_160,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl427]) ).
thf(zip_derived_cl11800,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11492,zip_derived_cl428]) ).
thf(zip_derived_cl11151_161,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11102,zip_derived_cl6788,zip_derived_cl291,zip_derived_cl291]) ).
thf(zip_derived_cl291_162,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl11151_163,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11102,zip_derived_cl6788,zip_derived_cl291,zip_derived_cl291]) ).
thf(zip_derived_cl5_164,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtasdt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntMult]) ).
thf(zip_derived_cl11209,plain,
( ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
| ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11151,zip_derived_cl5]) ).
thf(zip_derived_cl291_165,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl10995_166,plain,
aInteger0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10961,zip_derived_cl2,zip_derived_cl291,zip_derived_cl2]) ).
thf(zip_derived_cl11244,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl11836,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11800,zip_derived_cl11151,zip_derived_cl291,zip_derived_cl11244]) ).
thf(zip_derived_cl513_167,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ ( smndt0 @ X0 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl512]) ).
thf(zip_derived_cl13496,plain,
( ( ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11836,zip_derived_cl513]) ).
thf(zip_derived_cl11492_168,plain,
( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11469,zip_derived_cl10742,zip_derived_cl10995]) ).
thf(zip_derived_cl21_169,plain,
! [X0: $i] :
( ( ( smndt0 @ X0 )
= ( sdtasdt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl11826,plain,
( ( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11492,zip_derived_cl21]) ).
thf(zip_derived_cl11244_170,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl11862,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11826,zip_derived_cl11244]) ).
thf(zip_derived_cl11273_171,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11238,zip_derived_cl10995]) ).
thf(zip_derived_cl11862_172,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11826,zip_derived_cl11244]) ).
thf(zip_derived_cl11867,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11273,zip_derived_cl11862]) ).
thf(zip_derived_cl291_173,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl10995_174,plain,
aInteger0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10961,zip_derived_cl2,zip_derived_cl291,zip_derived_cl2]) ).
thf(zip_derived_cl11862_175,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11826,zip_derived_cl11244]) ).
thf(zip_derived_cl11865,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl13539,plain,
( ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl13496,zip_derived_cl11862,zip_derived_cl11867,zip_derived_cl291,zip_derived_cl11865]) ).
thf(zip_derived_cl511_176,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ sz10 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ X0 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl510]) ).
thf(zip_derived_cl23275,plain,
( ( ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ sz10 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl13539,zip_derived_cl511]) ).
thf(zip_derived_cl7_177,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ X0 @ X1 )
= ( sdtpldt0 @ X1 @ X0 ) ) ),
inference(cnf,[status(esa)],[mAddComm]) ).
thf(zip_derived_cl10742_178,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl10698,zip_derived_cl2,zip_derived_cl291]) ).
thf(zip_derived_cl11862_179,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11826,zip_derived_cl11244]) ).
thf(zip_derived_cl11864,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl10742,zip_derived_cl11862]) ).
thf(zip_derived_cl513_180,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ ( smndt0 @ X0 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl512]) ).
thf(zip_derived_cl12553,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( smndt0 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11864,zip_derived_cl513]) ).
thf(zip_derived_cl6788_181,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl11244_182,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl291_183,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl12592,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl12553,zip_derived_cl6788,zip_derived_cl11244,zip_derived_cl291]) ).
thf(zip_derived_cl20266,plain,
( ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl7,zip_derived_cl12592]) ).
thf(zip_derived_cl291_184,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl11244_185,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl11151_186,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11102,zip_derived_cl6788,zip_derived_cl291,zip_derived_cl291]) ).
thf(zip_derived_cl11862_187,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11826,zip_derived_cl11244]) ).
thf(zip_derived_cl11866,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11151,zip_derived_cl11862]) ).
thf(zip_derived_cl14_188,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ X0 @ sz10 )
= X0 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulOne]) ).
thf(zip_derived_cl16_189,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtasdt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X1 @ X0 ) @ ( sdtasdt0 @ X1 @ X2 ) ) ) ),
inference(cnf,[status(esa)],[mDistrib]) ).
thf(zip_derived_cl500,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ sz10 @ X1 ) )
= ( sdtpldt0 @ X0 @ ( sdtasdt0 @ X0 @ X1 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl14,zip_derived_cl16]) ).
thf(zip_derived_cl2_190,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl525,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ sz10 @ X1 ) )
= ( sdtpldt0 @ X0 @ ( sdtasdt0 @ X0 @ X1 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl500,zip_derived_cl2]) ).
thf(zip_derived_cl526,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ sz10 @ X1 ) )
= ( sdtpldt0 @ X0 @ ( sdtasdt0 @ X0 @ X1 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl525]) ).
thf(zip_derived_cl13578,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11866,zip_derived_cl526]) ).
thf(zip_derived_cl11862_191,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11826,zip_derived_cl11244]) ).
thf(zip_derived_cl6576_192,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ ( smndt0 @ X1 ) @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl377,zip_derived_cl3]) ).
thf(zip_derived_cl11883,plain,
( ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ( ( sdtpldt0 @ ( smndt0 @ ( smndt0 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ sz00 @ ( smndt0 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11862,zip_derived_cl6576]) ).
thf(zip_derived_cl291_193,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl291_194,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl6788_195,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl4090_196,plain,
( sz00
= ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3643,zip_derived_cl4059,zip_derived_cl1952]) ).
thf(zip_derived_cl6576_197,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ ( smndt0 @ X1 ) @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl377,zip_derived_cl3]) ).
thf(zip_derived_cl6620,plain,
( ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ sz00 )
= ( sdtpldt0 @ sz00 @ ( smndt0 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl4090,zip_derived_cl6576]) ).
thf(zip_derived_cl2_198,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl291_199,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl6659,plain,
( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ sz00 )
= ( sdtpldt0 @ sz00 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6620,zip_derived_cl2,zip_derived_cl291]) ).
thf(zip_derived_cl8_200,plain,
! [X0: $i] :
( ( ( sdtpldt0 @ X0 @ sz00 )
= X0 )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mAddZero]) ).
thf(zip_derived_cl7197,plain,
( ( ( sdtpldt0 @ sz00 @ ( smndt0 @ sz10 ) )
= ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl6659,zip_derived_cl8]) ).
thf(zip_derived_cl291_201,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl7225,plain,
( ( sdtpldt0 @ sz00 @ ( smndt0 @ sz10 ) )
= ( smndt0 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl7197,zip_derived_cl291]) ).
thf(zip_derived_cl11929,plain,
( ( sdtpldt0 @ sz10 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( smndt0 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11883,zip_derived_cl291,zip_derived_cl291,zip_derived_cl6788,zip_derived_cl7225]) ).
thf(zip_derived_cl8765_202,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= sz10 ),
inference(demod,[status(thm)],[zip_derived_cl8569,zip_derived_cl8761]) ).
thf(zip_derived_cl11865_203,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl291_204,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl13619,plain,
( sz10
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl13578,zip_derived_cl11929,zip_derived_cl8765,zip_derived_cl11865,zip_derived_cl291]) ).
thf(zip_derived_cl8588_205,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ sz10 )
= ( smndt0 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl8537,zip_derived_cl2,zip_derived_cl2]) ).
thf(zip_derived_cl20272,plain,
( ( smndt0 @ sz10 )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl20266,zip_derived_cl291,zip_derived_cl11244,zip_derived_cl13619,zip_derived_cl8588]) ).
thf(zip_derived_cl11836_206,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11800,zip_derived_cl11151,zip_derived_cl291,zip_derived_cl11244]) ).
thf(zip_derived_cl11865_207,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl11865_208,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl23340,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( sdtpldt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl23275,zip_derived_cl20272,zip_derived_cl11836,zip_derived_cl11865,zip_derived_cl11865]) ).
thf(zip_derived_cl6_209,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mAddAsso]) ).
thf(zip_derived_cl6_210,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mAddAsso]) ).
thf(zip_derived_cl284,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ ( sdtpldt0 @ X2 @ X1 ) )
| ~ ( aInteger0 @ X3 )
| ( ( sdtpldt0 @ ( sdtpldt0 @ X2 @ X1 ) @ ( sdtpldt0 @ X0 @ X3 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) @ X3 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl6,zip_derived_cl6]) ).
thf(zip_derived_cl285,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ( sdtpldt0 @ ( sdtpldt0 @ X2 @ X1 ) @ ( sdtpldt0 @ X0 @ X3 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) @ X3 ) )
| ~ ( aInteger0 @ X3 )
| ~ ( aInteger0 @ ( sdtpldt0 @ X2 @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl284]) ).
thf(zip_derived_cl4_211,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtpldt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntPlus]) ).
thf(zip_derived_cl4392,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X3 )
| ( ( sdtpldt0 @ ( sdtpldt0 @ X2 @ X1 ) @ ( sdtpldt0 @ X0 @ X3 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) @ X3 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl285,zip_derived_cl4]) ).
thf(zip_derived_cl24390,plain,
( ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ( ( sdtpldt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl23340,zip_derived_cl4392]) ).
thf(zip_derived_cl2_212,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl11244_213,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl2_214,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl11865_215,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl11866_216,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11151,zip_derived_cl11862]) ).
thf(zip_derived_cl513_217,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ ( smndt0 @ X0 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl512]) ).
thf(zip_derived_cl13577,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( smndt0 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11866,zip_derived_cl513]) ).
thf(zip_derived_cl6788_218,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl11865_219,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl291_220,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl13618,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl13577,zip_derived_cl6788,zip_derived_cl11865,zip_derived_cl291]) ).
thf(zip_derived_cl7_221,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ X0 @ X1 )
= ( sdtpldt0 @ X1 @ X0 ) ) ),
inference(cnf,[status(esa)],[mAddComm]) ).
thf(zip_derived_cl11864_222,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl10742,zip_derived_cl11862]) ).
thf(zip_derived_cl511_223,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ sz10 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ X0 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl510]) ).
thf(zip_derived_cl12552,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11864,zip_derived_cl511]) ).
thf(zip_derived_cl11244_224,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl291_225,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl12591,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl12552,zip_derived_cl11244,zip_derived_cl291]) ).
thf(zip_derived_cl15930,plain,
( ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl7,zip_derived_cl12591]) ).
thf(zip_derived_cl2_226,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl11244_227,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl15936,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl15930,zip_derived_cl2,zip_derived_cl11244]) ).
thf(zip_derived_cl11864_228,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl10742,zip_derived_cl11862]) ).
thf(zip_derived_cl526_229,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ sz10 @ X1 ) )
= ( sdtpldt0 @ X0 @ ( sdtasdt0 @ X0 @ X1 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl525]) ).
thf(zip_derived_cl13080,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11864,zip_derived_cl526]) ).
thf(zip_derived_cl11244_230,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl291_231,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl13132,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl13080,zip_derived_cl11244,zip_derived_cl291]) ).
thf(zip_derived_cl16232,plain,
( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl15936,zip_derived_cl13132]) ).
thf(zip_derived_cl21782,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl13618,zip_derived_cl16232]) ).
thf(zip_derived_cl11866_232,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11151,zip_derived_cl11862]) ).
thf(zip_derived_cl528_233,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ X1 ) )
= ( sdtpldt0 @ ( smndt0 @ X0 ) @ ( sdtasdt0 @ X0 @ X1 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl527]) ).
thf(zip_derived_cl13579,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtpldt0 @ ( smndt0 @ ( smndt0 @ sz10 ) ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11866,zip_derived_cl528]) ).
thf(zip_derived_cl6788_234,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl11865_235,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl291_236,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl13620,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl13579,zip_derived_cl6788,zip_derived_cl11865,zip_derived_cl291]) ).
thf(zip_derived_cl22178,plain,
( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl21782,zip_derived_cl13620]) ).
thf(zip_derived_cl11929_237,plain,
( ( sdtpldt0 @ sz10 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( smndt0 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11883,zip_derived_cl291,zip_derived_cl291,zip_derived_cl6788,zip_derived_cl7225]) ).
thf(zip_derived_cl24443,plain,
( ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl24390,zip_derived_cl2,zip_derived_cl11244,zip_derived_cl2,zip_derived_cl11865,zip_derived_cl22178,zip_derived_cl11929]) ).
thf(zip_derived_cl21_238,plain,
! [X0: $i] :
( ( ( smndt0 @ X0 )
= ( sdtasdt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(m__,conjecture,
? [W0: $i] :
( ~ ( ( ( W0 = sz10 )
| ( W0
= ( smndt0 @ sz10 ) ) )
& ( aElementOf0 @ W0 @ cS2200 ) )
& ( ( aElementOf0 @ W0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) )
| ( ( ( sdteqdtlpzmzozddtrp0 @ W0 @ sz10 @ xp )
| ( aDivisorOf0 @ xp @ ( sdtpldt0 @ W0 @ ( smndt0 @ sz10 ) ) )
| ? [W1: $i] :
( ( ( sdtasdt0 @ xp @ W1 )
= ( sdtpldt0 @ W0 @ ( smndt0 @ sz10 ) ) )
& ( aInteger0 @ W1 ) ) )
& ( aInteger0 @ W0 ) ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ? [W0: $i] :
( ~ ( ( ( W0 = sz10 )
| ( W0
= ( smndt0 @ sz10 ) ) )
& ( aElementOf0 @ W0 @ cS2200 ) )
& ( ( aElementOf0 @ W0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz10 @ xp ) )
| ( ( ( sdteqdtlpzmzozddtrp0 @ W0 @ sz10 @ xp )
| ( aDivisorOf0 @ xp @ ( sdtpldt0 @ W0 @ ( smndt0 @ sz10 ) ) )
| ? [W1: $i] :
( ( ( sdtasdt0 @ xp @ W1 )
= ( sdtpldt0 @ W0 @ ( smndt0 @ sz10 ) ) )
& ( aInteger0 @ W1 ) ) )
& ( aInteger0 @ W0 ) ) ) ),
inference('cnf.neg',[status(esa)],[m__]) ).
thf(zip_derived_cl214,plain,
! [X0: $i,X1: $i] :
( ( X0
= ( smndt0 @ sz10 ) )
| ( X0 = sz10 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtasdt0 @ xp @ X1 )
!= ( sdtpldt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl1382,plain,
! [X0: $i] :
( ~ ( aInteger0 @ xp )
| ( X0
= ( smndt0 @ sz10 ) )
| ( X0 = sz10 )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ( ( smndt0 @ xp )
!= ( sdtpldt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl21,zip_derived_cl214]) ).
thf(zip_derived_cl192_239,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl291_240,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl1393,plain,
! [X0: $i] :
( ( X0
= ( smndt0 @ sz10 ) )
| ( X0 = sz10 )
| ( ( smndt0 @ xp )
!= ( sdtpldt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl1382,zip_derived_cl192,zip_derived_cl291]) ).
thf(zip_derived_cl24684,plain,
( ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( smndt0 @ sz10 ) )
| ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= sz10 )
| ( ( smndt0 @ xp )
!= ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl24443,zip_derived_cl1393]) ).
thf(zip_derived_cl7_241,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ X0 @ X1 )
= ( sdtpldt0 @ X1 @ X0 ) ) ),
inference(cnf,[status(esa)],[mAddComm]) ).
thf(zip_derived_cl21782_242,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl13618,zip_derived_cl16232]) ).
thf(zip_derived_cl9454_243,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtasdt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl9453,zip_derived_cl5]) ).
thf(zip_derived_cl21836,plain,
( ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ( aInteger0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl21782,zip_derived_cl9454]) ).
thf(zip_derived_cl11865_244,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl291_245,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl291_246,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl21898,plain,
aInteger0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl21836,zip_derived_cl11865,zip_derived_cl291,zip_derived_cl291]) ).
thf(zip_derived_cl22102,plain,
( ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ( aInteger0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl7,zip_derived_cl21898]) ).
thf(zip_derived_cl2_247,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl11244_248,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl22108,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl22102,zip_derived_cl2,zip_derived_cl11244]) ).
thf(zip_derived_cl24738,plain,
( ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( smndt0 @ sz10 ) )
| ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= sz10 )
| ( ( smndt0 @ xp )
!= ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl24684,zip_derived_cl22108]) ).
thf(zip_derived_cl55916_249,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ xp ) )
= xp ),
inference(demod,[status(thm)],[zip_derived_cl55826,zip_derived_cl6788,zip_derived_cl55288,zip_derived_cl192,zip_derived_cl291]) ).
thf(zip_derived_cl511_250,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ sz10 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ X0 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl510]) ).
thf(zip_derived_cl56885,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ xp ) @ sz10 ) )
= ( sdtpldt0 @ xp @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ xp ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55916,zip_derived_cl511]) ).
thf(zip_derived_cl55911_251,plain,
aInteger0 @ ( smndt0 @ xp ),
inference(demod,[status(thm)],[zip_derived_cl55822,zip_derived_cl291,zip_derived_cl192]) ).
thf(zip_derived_cl291_252,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl56956,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ xp ) @ sz10 ) )
= ( sdtpldt0 @ xp @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56885,zip_derived_cl55911,zip_derived_cl291]) ).
thf(zip_derived_cl60196_253,plain,
( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= ( sdtpldt0 @ ( smndt0 @ xp ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl55918,zip_derived_cl59266]) ).
thf(zip_derived_cl55916_254,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ xp ) )
= xp ),
inference(demod,[status(thm)],[zip_derived_cl55826,zip_derived_cl6788,zip_derived_cl55288,zip_derived_cl192,zip_derived_cl291]) ).
thf(zip_derived_cl526_255,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ sz10 @ X1 ) )
= ( sdtpldt0 @ X0 @ ( sdtasdt0 @ X0 @ X1 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl525]) ).
thf(zip_derived_cl56887,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ xp ) )
| ~ ( aInteger0 @ ( smndt0 @ xp ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55916,zip_derived_cl526]) ).
thf(zip_derived_cl55911_256,plain,
aInteger0 @ ( smndt0 @ xp ),
inference(demod,[status(thm)],[zip_derived_cl55822,zip_derived_cl291,zip_derived_cl192]) ).
thf(zip_derived_cl291_257,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl56958,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl56887,zip_derived_cl55911,zip_derived_cl291]) ).
thf(zip_derived_cl60333,plain,
( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ xp )
= ( sdtpldt0 @ xp @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56956,zip_derived_cl60196,zip_derived_cl56958]) ).
thf(zip_derived_cl6576_258,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ ( smndt0 @ X1 ) @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl377,zip_derived_cl3]) ).
thf(zip_derived_cl60435,plain,
( ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ xp )
| ( ( sdtpldt0 @ ( smndt0 @ ( smndt0 @ sz10 ) ) @ ( sdtpldt0 @ xp @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ sz00 @ xp ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl60333,zip_derived_cl6576]) ).
thf(zip_derived_cl291_259,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl192_260,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl6788_261,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl55004_262,plain,
( xp
= ( sdtpldt0 @ sz00 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl54999,zip_derived_cl192]) ).
thf(zip_derived_cl60483,plain,
( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ xp @ ( smndt0 @ sz10 ) ) )
= xp ),
inference(demod,[status(thm)],[zip_derived_cl60435,zip_derived_cl291,zip_derived_cl192,zip_derived_cl6788,zip_derived_cl55004]) ).
thf(zip_derived_cl6_263,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X2 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ X1 @ X0 ) @ X2 ) ) ),
inference(cnf,[status(esa)],[mAddAsso]) ).
thf(zip_derived_cl215,plain,
! [X0: $i] :
( ( X0
= ( smndt0 @ sz10 ) )
| ( X0 = sz10 )
| ~ ( aDivisorOf0 @ xp @ ( sdtpldt0 @ X0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl770,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ X1 @ X0 )
= ( smndt0 @ sz10 ) )
| ( ( sdtpldt0 @ X1 @ X0 )
= sz10 )
| ~ ( aDivisorOf0 @ xp @ ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ ( smndt0 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ X1 @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl6,zip_derived_cl215]) ).
thf(zip_derived_cl291_264,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl778,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ X1 @ X0 )
= ( smndt0 @ sz10 ) )
| ( ( sdtpldt0 @ X1 @ X0 )
= sz10 )
| ~ ( aDivisorOf0 @ xp @ ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ ( smndt0 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ X1 @ X0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl770,zip_derived_cl291]) ).
thf(zip_derived_cl4_265,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtpldt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntPlus]) ).
thf(zip_derived_cl28056,plain,
! [X0: $i,X1: $i] :
( ~ ( aDivisorOf0 @ xp @ ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ ( smndt0 @ sz10 ) ) ) )
| ( ( sdtpldt0 @ X1 @ X0 )
= sz10 )
| ( ( sdtpldt0 @ X1 @ X0 )
= ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 ) ),
inference(clc,[status(thm)],[zip_derived_cl778,zip_derived_cl4]) ).
thf(zip_derived_cl60617,plain,
( ~ ( aDivisorOf0 @ xp @ xp )
| ( ( sdtpldt0 @ sz10 @ xp )
= sz10 )
| ( ( sdtpldt0 @ sz10 @ xp )
= ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ xp )
| ~ ( aInteger0 @ sz10 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl60483,zip_derived_cl28056]) ).
thf(zip_derived_cl55291_266,plain,
( ( sdtasdt0 @ xp @ sz10 )
= xp ),
inference(demod,[status(thm)],[zip_derived_cl55257,zip_derived_cl7961,zip_derived_cl55004,zip_derived_cl1,zip_derived_cl192]) ).
thf(zip_derived_cl23,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ( X0 = sz00 )
| ( ( sdtasdt0 @ X0 @ X2 )
!= X1 )
| ~ ( aInteger0 @ X2 )
| ( aDivisorOf0 @ X0 @ X1 )
| ~ ( aInteger0 @ X1 ) ),
inference(cnf,[status(esa)],[mDivisor]) ).
thf(zip_derived_cl663,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ ( sdtasdt0 @ X1 @ X0 ) )
| ( aDivisorOf0 @ X1 @ ( sdtasdt0 @ X1 @ X0 ) )
| ~ ( aInteger0 @ X0 )
| ( X1 = sz00 )
| ~ ( aInteger0 @ X1 ) ),
inference(eq_res,[status(thm)],[zip_derived_cl23]) ).
thf(zip_derived_cl5_267,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtasdt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntMult]) ).
thf(zip_derived_cl24091,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ( X1 = sz00 )
| ~ ( aInteger0 @ X0 )
| ( aDivisorOf0 @ X1 @ ( sdtasdt0 @ X1 @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl663,zip_derived_cl5]) ).
thf(zip_derived_cl55541,plain,
( ~ ( aInteger0 @ xp )
| ( xp = sz00 )
| ~ ( aInteger0 @ sz10 )
| ( aDivisorOf0 @ xp @ xp ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl55291,zip_derived_cl24091]) ).
thf(zip_derived_cl192_268,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl2_269,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl55617,plain,
( ( xp = sz00 )
| ( aDivisorOf0 @ xp @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl55541,zip_derived_cl192,zip_derived_cl2]) ).
thf(zip_derived_cl193_270,plain,
xp != sz00,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl55618,plain,
aDivisorOf0 @ xp @ xp,
inference('simplify_reflect-',[status(thm)],[zip_derived_cl55617,zip_derived_cl193]) ).
thf(zip_derived_cl192_271,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl2_272,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl60661,plain,
( ( ( sdtpldt0 @ sz10 @ xp )
= sz10 )
| ( ( sdtpldt0 @ sz10 @ xp )
= ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl60617,zip_derived_cl55618,zip_derived_cl192,zip_derived_cl2]) ).
thf(zip_derived_cl6576_273,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ ( smndt0 @ X1 ) @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl377,zip_derived_cl3]) ).
thf(zip_derived_cl60839,plain,
( ( ( sdtpldt0 @ sz10 @ xp )
= sz10 )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ xp )
| ( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= ( sdtpldt0 @ sz00 @ xp ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl60661,zip_derived_cl6576]) ).
thf(zip_derived_cl2_274,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl192_275,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl55004_276,plain,
( xp
= ( sdtpldt0 @ sz00 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl54999,zip_derived_cl192]) ).
thf(zip_derived_cl60875,plain,
( ( ( sdtpldt0 @ sz10 @ xp )
= sz10 )
| ( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= xp ) ),
inference(demod,[status(thm)],[zip_derived_cl60839,zip_derived_cl2,zip_derived_cl192,zip_derived_cl55004]) ).
thf(zip_derived_cl11862_277,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11826,zip_derived_cl11244]) ).
thf(zip_derived_cl60985,plain,
( ( ( sdtpldt0 @ sz10 @ xp )
= sz10 )
| ( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= xp ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl60875,zip_derived_cl11862]) ).
thf(zip_derived_cl11867_278,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11273,zip_derived_cl11862]) ).
thf(zip_derived_cl61136,plain,
( ( ( sdtpldt0 @ sz10 @ xp )
= sz10 )
| ( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl60985,zip_derived_cl11867]) ).
thf(zip_derived_cl6576_279,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 )
| ( ( sdtpldt0 @ ( smndt0 @ X1 ) @ ( sdtpldt0 @ X1 @ X0 ) )
= ( sdtpldt0 @ sz00 @ X0 ) ) ),
inference(clc,[status(thm)],[zip_derived_cl377,zip_derived_cl3]) ).
thf(zip_derived_cl61583,plain,
( ( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ xp )
| ( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ sz10 )
= ( sdtpldt0 @ sz00 @ xp ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl61136,zip_derived_cl6576]) ).
thf(zip_derived_cl2_280,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl192_281,plain,
aInteger0 @ xp,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl6212_282,plain,
( sz00
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl6180,zip_derived_cl2,zip_derived_cl291]) ).
thf(zip_derived_cl55004_283,plain,
( xp
= ( sdtpldt0 @ sz00 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl54999,zip_derived_cl192]) ).
thf(zip_derived_cl61623,plain,
( ( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) )
| ( sz00 = xp ) ),
inference(demod,[status(thm)],[zip_derived_cl61583,zip_derived_cl2,zip_derived_cl192,zip_derived_cl6212,zip_derived_cl55004]) ).
thf(zip_derived_cl193_284,plain,
xp != sz00,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl61624,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl61624_285,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl61624_286,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl61717,plain,
( ( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= ( smndt0 @ sz10 ) )
| ( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= sz10 )
| ( ( smndt0 @ xp )
!= ( smndt0 @ xp ) ) ),
inference(demod,[status(thm)],[zip_derived_cl24738,zip_derived_cl61624,zip_derived_cl61624,zip_derived_cl61624]) ).
thf(zip_derived_cl61718,plain,
( ( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= sz10 )
| ( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= ( smndt0 @ sz10 ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl61717]) ).
thf(zip_derived_cl5773_287,plain,
! [X0: $i,X1: $i] :
( ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ ( smndt0 @ ( sdtpldt0 @ X1 @ X0 ) ) ) )
= sz00 )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ X1 @ X0 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(clc,[status(thm)],[zip_derived_cl337,zip_derived_cl4]) ).
thf(zip_derived_cl66869,plain,
( ( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= sz10 )
| ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ ( smndt0 @ xp ) @ ( smndt0 @ ( smndt0 @ sz10 ) ) ) )
= sz00 )
| ~ ( aInteger0 @ ( smndt0 @ ( smndt0 @ sz10 ) ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( smndt0 @ xp ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl61718,zip_derived_cl5773]) ).
thf(zip_derived_cl6788_288,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl60196_289,plain,
( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= ( sdtpldt0 @ ( smndt0 @ xp ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl55918,zip_derived_cl59266]) ).
thf(zip_derived_cl13539_290,plain,
( ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl13496,zip_derived_cl11862,zip_derived_cl11867,zip_derived_cl291,zip_derived_cl11865]) ).
thf(zip_derived_cl4969_291,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl301,zip_derived_cl4]) ).
thf(zip_derived_cl11273_292,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11238,zip_derived_cl10995]) ).
thf(zip_derived_cl8071_293,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ sz10 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl8070]) ).
thf(zip_derived_cl11468,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11273,zip_derived_cl8071]) ).
thf(zip_derived_cl11151_294,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11102,zip_derived_cl6788,zip_derived_cl291,zip_derived_cl291]) ).
thf(zip_derived_cl10995_295,plain,
aInteger0 @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10961,zip_derived_cl2,zip_derived_cl291,zip_derived_cl2]) ).
thf(zip_derived_cl11491,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11468,zip_derived_cl11151,zip_derived_cl10995]) ).
thf(zip_derived_cl511_296,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ sz10 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ X0 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl510]) ).
thf(zip_derived_cl11504,plain,
( ( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11491,zip_derived_cl511]) ).
thf(zip_derived_cl2_297,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl11244_298,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl11539,plain,
( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11504,zip_derived_cl2,zip_derived_cl11244]) ).
thf(zip_derived_cl428_299,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl427]) ).
thf(zip_derived_cl15494,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11539,zip_derived_cl428]) ).
thf(zip_derived_cl11244_300,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl11244_301,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl15547,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl15494,zip_derived_cl11244,zip_derived_cl11244]) ).
thf(zip_derived_cl11491_302,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11468,zip_derived_cl11151,zip_derived_cl10995]) ).
thf(zip_derived_cl428_303,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl427]) ).
thf(zip_derived_cl11503,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ sz10 ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11491,zip_derived_cl428]) ).
thf(zip_derived_cl10742_304,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl10698,zip_derived_cl2,zip_derived_cl291]) ).
thf(zip_derived_cl2_305,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl11244_306,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl11538,plain,
( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11503,zip_derived_cl10742,zip_derived_cl2,zip_derived_cl11244]) ).
thf(zip_derived_cl11862_307,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11826,zip_derived_cl11244]) ).
thf(zip_derived_cl14434,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl11538,zip_derived_cl11862]) ).
thf(zip_derived_cl511_308,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ sz10 ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ X0 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl510]) ).
thf(zip_derived_cl14440,plain,
( ( ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl14434,zip_derived_cl511]) ).
thf(zip_derived_cl2_309,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl11865_310,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl14484,plain,
( ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl14440,zip_derived_cl2,zip_derived_cl11865]) ).
thf(zip_derived_cl11492_311,plain,
( ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11469,zip_derived_cl10742,zip_derived_cl10995]) ).
thf(zip_derived_cl11862_312,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11826,zip_derived_cl11244]) ).
thf(zip_derived_cl11868,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11492,zip_derived_cl11862]) ).
thf(zip_derived_cl513_313,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ X0 @ ( sdtpldt0 @ X1 @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtasdt0 @ X0 @ X1 ) @ ( smndt0 @ X0 ) ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl512]) ).
thf(zip_derived_cl12628,plain,
( ( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11868,zip_derived_cl513]) ).
thf(zip_derived_cl11862_314,plain,
( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11826,zip_derived_cl11244]) ).
thf(zip_derived_cl291_315,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl11244_316,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl12667,plain,
( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl12628,zip_derived_cl11862,zip_derived_cl291,zip_derived_cl11244]) ).
thf(zip_derived_cl26501,plain,
( ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl14484,zip_derived_cl12667]) ).
thf(zip_derived_cl27901,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl15547,zip_derived_cl26501]) ).
thf(zip_derived_cl27971,plain,
( ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ sz10 )
| ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl4969,zip_derived_cl27901]) ).
thf(zip_derived_cl11244_317,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl2_318,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl2_319,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl22178_320,plain,
( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl21782,zip_derived_cl13620]) ).
thf(zip_derived_cl27981,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl27971,zip_derived_cl11244,zip_derived_cl2,zip_derived_cl2,zip_derived_cl22178]) ).
thf(zip_derived_cl27901_321,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl15547,zip_derived_cl26501]) ).
thf(zip_derived_cl20_322,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl27963,plain,
( ( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( smndt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl27901,zip_derived_cl20]) ).
thf(zip_derived_cl11539_323,plain,
( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11504,zip_derived_cl2,zip_derived_cl11244]) ).
thf(zip_derived_cl5_324,plain,
! [X0: $i,X1: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtasdt0 @ X0 @ X1 ) ) ),
inference(cnf,[status(esa)],[mIntMult]) ).
thf(zip_derived_cl15490,plain,
( ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ( aInteger0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11539,zip_derived_cl5]) ).
thf(zip_derived_cl11244_325,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl11244_326,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl15542,plain,
aInteger0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl15490,zip_derived_cl11244,zip_derived_cl11244]) ).
thf(zip_derived_cl28050,plain,
( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( smndt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl27963,zip_derived_cl15542]) ).
thf(zip_derived_cl30155,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( smndt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl27981,zip_derived_cl28050]) ).
thf(zip_derived_cl428_327,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl427]) ).
thf(zip_derived_cl30159,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtasdt0 @ ( smndt0 @ ( smndt0 @ sz10 ) ) @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
| ~ ( aInteger0 @ ( smndt0 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl30155,zip_derived_cl428]) ).
thf(zip_derived_cl6788_328,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl4969_329,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( ( sdtpldt0 @ X1 @ ( sdtpldt0 @ X0 @ X2 ) )
= ( sdtpldt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl301,zip_derived_cl4]) ).
thf(zip_derived_cl11539_330,plain,
( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11504,zip_derived_cl2,zip_derived_cl11244]) ).
thf(zip_derived_cl426_331,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ sz10 @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ X0 @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl425]) ).
thf(zip_derived_cl15493,plain,
( ( ( sdtasdt0 @ sz10 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl11539,zip_derived_cl426]) ).
thf(zip_derived_cl11244_332,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl11244_333,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl15546,plain,
( ( sdtasdt0 @ sz10 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl15493,zip_derived_cl11244,zip_derived_cl11244]) ).
thf(zip_derived_cl23455,plain,
( ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ sz10 )
| ( ( sdtasdt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl4969,zip_derived_cl15546]) ).
thf(zip_derived_cl11244_334,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl2_335,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl2_336,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl22178_337,plain,
( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl21782,zip_derived_cl13620]) ).
thf(zip_derived_cl22178_338,plain,
( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl21782,zip_derived_cl13620]) ).
thf(zip_derived_cl23465,plain,
( ( sdtasdt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl23455,zip_derived_cl11244,zip_derived_cl2,zip_derived_cl2,zip_derived_cl22178,zip_derived_cl22178]) ).
thf(zip_derived_cl23465_339,plain,
( ( sdtasdt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl23455,zip_derived_cl11244,zip_derived_cl2,zip_derived_cl2,zip_derived_cl22178,zip_derived_cl22178]) ).
thf(zip_derived_cl9454_340,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X2 )
| ~ ( aInteger0 @ X1 )
| ( aInteger0 @ ( sdtasdt0 @ X2 @ ( sdtpldt0 @ X1 @ X0 ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl9453,zip_derived_cl5]) ).
thf(zip_derived_cl24015,plain,
( ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ sz10 )
| ~ ( aInteger0 @ sz10 )
| ( aInteger0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl23465,zip_derived_cl9454]) ).
thf(zip_derived_cl22108_341,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl22102,zip_derived_cl2,zip_derived_cl11244]) ).
thf(zip_derived_cl2_342,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl2_343,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl24079,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl24015,zip_derived_cl22108,zip_derived_cl2,zip_derived_cl2]) ).
thf(zip_derived_cl291_344,plain,
aInteger0 @ ( smndt0 @ sz10 ),
inference('s_sup-',[status(thm)],[zip_derived_cl289,zip_derived_cl228]) ).
thf(zip_derived_cl30235,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl30159,zip_derived_cl6788,zip_derived_cl23465,zip_derived_cl24079,zip_derived_cl291]) ).
thf(zip_derived_cl30155_345,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( smndt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl27981,zip_derived_cl28050]) ).
thf(zip_derived_cl20_346,plain,
! [X0: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ X0 )
= ( smndt0 @ X0 ) )
| ~ ( aInteger0 @ X0 ) ),
inference(cnf,[status(esa)],[mMulMinOne]) ).
thf(zip_derived_cl30218,plain,
( ( ( smndt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( smndt0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl30155,zip_derived_cl20]) ).
thf(zip_derived_cl24079_347,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl24015,zip_derived_cl22108,zip_derived_cl2,zip_derived_cl2]) ).
thf(zip_derived_cl30294,plain,
( ( smndt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( smndt0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl30218,zip_derived_cl24079]) ).
thf(zip_derived_cl26501_348,plain,
( ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl14484,zip_derived_cl12667]) ).
thf(zip_derived_cl428_349,plain,
! [X0: $i,X1: $i] :
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ X0 @ X1 ) )
= ( sdtasdt0 @ ( smndt0 @ X0 ) @ X1 ) )
| ~ ( aInteger0 @ X1 )
| ~ ( aInteger0 @ X0 ) ),
inference(simplify,[status(thm)],[zip_derived_cl427]) ).
thf(zip_derived_cl26505,plain,
( ( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtasdt0 @ ( smndt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl26501,zip_derived_cl428]) ).
thf(zip_derived_cl11867_350,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11273,zip_derived_cl11862]) ).
thf(zip_derived_cl11539_351,plain,
( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11504,zip_derived_cl2,zip_derived_cl11244]) ).
thf(zip_derived_cl11244_352,plain,
aInteger0 @ ( sdtpldt0 @ sz10 @ sz10 ),
inference(demod,[status(thm)],[zip_derived_cl11209,zip_derived_cl291,zip_derived_cl10995]) ).
thf(zip_derived_cl11865_353,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl26573,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl26505,zip_derived_cl11867,zip_derived_cl11539,zip_derived_cl11244,zip_derived_cl11865]) ).
thf(zip_derived_cl28050_354,plain,
( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( smndt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl27963,zip_derived_cl15542]) ).
thf(zip_derived_cl30294_355,plain,
( ( smndt0 @ ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( smndt0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl30218,zip_derived_cl24079]) ).
thf(zip_derived_cl30300,plain,
( ( sdtasdt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( smndt0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl28050,zip_derived_cl30294]) ).
thf(zip_derived_cl33057,plain,
( ( sdtasdt0 @ ( smndt0 @ sz10 ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ) )
= ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl26573,zip_derived_cl30300]) ).
thf(zip_derived_cl34734,plain,
( ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ sz10 ) @ ( sdtpldt0 @ sz10 @ sz10 ) )
= ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl30235,zip_derived_cl30294,zip_derived_cl33057]) ).
thf(zip_derived_cl34736,plain,
( ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl13539,zip_derived_cl34734]) ).
thf(zip_derived_cl61624_356,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl57022_357,plain,
( xp
= ( smndt0 @ ( smndt0 @ xp ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56945,zip_derived_cl55911]) ).
thf(zip_derived_cl61624_358,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl57022_359,plain,
( xp
= ( smndt0 @ ( smndt0 @ xp ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56945,zip_derived_cl55911]) ).
thf(zip_derived_cl61624_360,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl61756,plain,
( ( sdtasdt0 @ xp @ xp )
= ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl34736,zip_derived_cl61624,zip_derived_cl57022,zip_derived_cl61624,zip_derived_cl57022,zip_derived_cl61624]) ).
thf(zip_derived_cl6788_361,plain,
( sz10
= ( smndt0 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6783,zip_derived_cl291]) ).
thf(zip_derived_cl2_362,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl2_363,plain,
aInteger0 @ sz10,
inference(cnf,[status(esa)],[mIntOne]) ).
thf(zip_derived_cl55911_364,plain,
aInteger0 @ ( smndt0 @ xp ),
inference(demod,[status(thm)],[zip_derived_cl55822,zip_derived_cl291,zip_derived_cl192]) ).
thf(zip_derived_cl66915,plain,
( ( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= sz10 )
| ( ( sdtasdt0 @ xp @ xp )
= sz00 ) ),
inference(demod,[status(thm)],[zip_derived_cl66869,zip_derived_cl6788,zip_derived_cl60196,zip_derived_cl61756,zip_derived_cl6788,zip_derived_cl2,zip_derived_cl2,zip_derived_cl55911]) ).
thf(zip_derived_cl34736_365,plain,
( ( sdtasdt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
= ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl13539,zip_derived_cl34734]) ).
thf(zip_derived_cl22_366,plain,
! [X0: $i,X1: $i] :
( ( X0 = sz00 )
| ~ ( aInteger0 @ X0 )
| ~ ( aInteger0 @ X1 )
| ( X1 = sz00 )
| ( ( sdtasdt0 @ X0 @ X1 )
!= sz00 ) ),
inference(cnf,[status(esa)],[mZeroDiv]) ).
thf(zip_derived_cl35057,plain,
( ( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= sz00 )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ~ ( aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
| ( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= sz00 )
| ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
!= sz00 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl34736,zip_derived_cl22]) ).
thf(zip_derived_cl11865_367,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl11865_368,plain,
aInteger0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl10995,zip_derived_cl11862]) ).
thf(zip_derived_cl35130,plain,
( ( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= sz00 )
| ( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= sz00 )
| ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
!= sz00 ) ),
inference(demod,[status(thm)],[zip_derived_cl35057,zip_derived_cl11865,zip_derived_cl11865]) ).
thf(zip_derived_cl35131,plain,
( ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) )
!= sz00 )
| ( ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) )
= sz00 ) ),
inference(simplify,[status(thm)],[zip_derived_cl35130]) ).
thf(zip_derived_cl61624_369,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl61624_370,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl57022_371,plain,
( xp
= ( smndt0 @ ( smndt0 @ xp ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56945,zip_derived_cl55911]) ).
thf(zip_derived_cl61762,plain,
( ( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) )
!= sz00 )
| ( xp = sz00 ) ),
inference(demod,[status(thm)],[zip_derived_cl35131,zip_derived_cl61624,zip_derived_cl61624,zip_derived_cl57022]) ).
thf(zip_derived_cl193_372,plain,
xp != sz00,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl61763,plain,
( ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) )
!= sz00 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61762,zip_derived_cl193]) ).
thf(zip_derived_cl61756_373,plain,
( ( sdtasdt0 @ xp @ xp )
= ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl34736,zip_derived_cl61624,zip_derived_cl57022,zip_derived_cl61624,zip_derived_cl57022,zip_derived_cl61624]) ).
thf(zip_derived_cl64611,plain,
( ( sdtasdt0 @ xp @ xp )
!= sz00 ),
inference(demod,[status(thm)],[zip_derived_cl61763,zip_derived_cl61756]) ).
thf(zip_derived_cl66916,plain,
( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= sz10 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl66915,zip_derived_cl64611]) ).
thf(zip_derived_cl20272_374,plain,
( ( smndt0 @ sz10 )
= ( sdtpldt0 @ ( smndt0 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl20266,zip_derived_cl291,zip_derived_cl11244,zip_derived_cl13619,zip_derived_cl8588]) ).
thf(zip_derived_cl61624_375,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl57022_376,plain,
( xp
= ( smndt0 @ ( smndt0 @ xp ) ) ),
inference(demod,[status(thm)],[zip_derived_cl56945,zip_derived_cl55911]) ).
thf(zip_derived_cl61687,plain,
( ( smndt0 @ sz10 )
= ( sdtpldt0 @ xp @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl20272,zip_derived_cl61624,zip_derived_cl57022]) ).
thf(zip_derived_cl66946,plain,
( ( smndt0 @ sz10 )
= sz10 ),
inference(demod,[status(thm)],[zip_derived_cl60392,zip_derived_cl66916,zip_derived_cl61687]) ).
thf(zip_derived_cl55288_377,plain,
( ( sdtasdt0 @ sz10 @ xp )
= xp ),
inference(demod,[status(thm)],[zip_derived_cl55254,zip_derived_cl7910,zip_derived_cl55004,zip_derived_cl1,zip_derived_cl192]) ).
thf(zip_derived_cl67368,plain,
( xp
= ( smndt0 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl55812,zip_derived_cl66946,zip_derived_cl55288]) ).
thf(zip_derived_cl24443_378,plain,
( ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ ( sdtpldt0 @ sz10 @ sz10 ) ) @ ( smndt0 @ sz10 ) )
= ( sdtpldt0 @ sz10 @ sz10 ) ),
inference(demod,[status(thm)],[zip_derived_cl24390,zip_derived_cl2,zip_derived_cl11244,zip_derived_cl2,zip_derived_cl11865,zip_derived_cl22178,zip_derived_cl11929]) ).
thf(zip_derived_cl61624_379,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl61624_380,plain,
( ( sdtpldt0 @ sz10 @ sz10 )
= ( smndt0 @ xp ) ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl61623,zip_derived_cl193]) ).
thf(zip_derived_cl61713,plain,
( ( sdtpldt0 @ ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) ) @ ( smndt0 @ sz10 ) )
= ( smndt0 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl24443,zip_derived_cl61624,zip_derived_cl61624]) ).
thf(zip_derived_cl66916_381,plain,
( ( sdtpldt0 @ sz10 @ ( smndt0 @ xp ) )
= sz10 ),
inference('simplify_reflect-',[status(thm)],[zip_derived_cl66915,zip_derived_cl64611]) ).
thf(zip_derived_cl4090_382,plain,
( sz00
= ( sdtpldt0 @ sz10 @ ( smndt0 @ sz10 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3643,zip_derived_cl4059,zip_derived_cl1952]) ).
thf(zip_derived_cl66948,plain,
( sz00
= ( smndt0 @ xp ) ),
inference(demod,[status(thm)],[zip_derived_cl61713,zip_derived_cl66916,zip_derived_cl4090]) ).
thf(zip_derived_cl67646,plain,
xp = sz00,
inference(demod,[status(thm)],[zip_derived_cl67368,zip_derived_cl66948]) ).
thf(zip_derived_cl193_383,plain,
xp != sz00,
inference(cnf,[status(esa)],[m__2171]) ).
thf(zip_derived_cl67647,plain,
$false,
inference('simplify_reflect-',[status(thm)],[zip_derived_cl67646,zip_derived_cl193]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.39 % Problem : NUM451+6 : TPTP v9.2.0. Released v4.0.0.
% 0.13/0.40 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.lxFhFVUHrZ true
% 0.20/0.63 % Computer : n003.cluster.edu
% 0.20/0.63 % Model : x86_64 x86_64
% 0.20/0.63 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.63 % Memory : 8042.1875MB
% 0.20/0.63 % OS : Linux 3.10.0-693.el7.x86_64
% 0.20/0.63 % CPULimit : 300
% 0.20/0.63 % WCLimit : 300
% 0.20/0.63 % DateTime : Wed Oct 1 16:41:53 EDT 2025
% 0.20/0.63 % CPUTime :
% 0.20/0.63 % Running portfolio for 300 s
% 0.20/0.63 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.63 % Number of cores: 8
% 0.20/0.63 % Python version: Python 3.6.8
% 0.20/0.64 % Running in FO mode
% 0.24/0.94 % Total configuration time : 435
% 0.24/0.94 % Estimated wc time : 1092
% 0.24/0.94 % Estimated cpu time (7 cpus) : 156.0
% 0.24/1.00 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.24/1.03 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.24/1.03 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.24/1.04 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.24/1.06 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.24/1.06 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.24/1.06 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 65.74/10.41 % Solved by fo/fo13.sh.
% 65.74/10.41 % done 7068 iterations in 9.291s
% 65.74/10.41 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 65.74/10.41 % SZS output start Refutation
% See solution above
% 66.38/10.41
% 66.38/10.41
% 66.38/10.41 % Terminating...
% 66.38/10.47 % Runner terminated.
% 66.38/10.48 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------