%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM440+6 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.ArlXftiQxl true
% Computer : n026.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:46:59 PM UTC 2025
% Result : Theorem 18.26s 3.20s
% Output : Refutation 18.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.10 % Problem : NUM440+6 : TPTP v9.2.0. Released v4.0.0.
% 0.02/0.11 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.ArlXftiQxl true
% 0.12/0.31 % Computer : n026.cluster.edu
% 0.12/0.31 % Model : x86_64 x86_64
% 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31 % Memory : 8042.1875MB
% 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31 % CPULimit : 300
% 0.12/0.31 % WCLimit : 300
% 0.12/0.31 % DateTime : Wed Oct 1 16:30:38 EDT 2025
% 0.12/0.31 % CPUTime :
% 0.12/0.31 % Running portfolio for 300 s
% 0.12/0.31 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.31 % Number of cores: 8
% 0.12/0.32 % Python version: Python 3.6.8
% 0.12/0.32 % Running in FO mode
% 0.47/0.56 % Total configuration time : 435
% 0.47/0.56 % Estimated wc time : 1092
% 0.47/0.56 % Estimated cpu time (7 cpus) : 156.0
% 0.48/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.48/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.48/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.48/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.48/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.48/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.48/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 18.26/3.20 % Solved by fo/fo6_bce.sh.
% 18.26/3.20 % BCE start: 1473
% 18.26/3.20 % BCE eliminated: 0
% 18.26/3.20 % PE start: 1473
% 18.26/3.20 logic: eq
% 18.26/3.20 % PE eliminated: 10
% 18.26/3.20 % done 1735 iterations in 2.467s
% 18.26/3.20 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 18.26/3.20 % SZS output start Refutation
% 18.26/3.20 thf(smndt0_type, type, smndt0: $i > $i).
% 18.26/3.20 thf(xB_type, type, xB: $i).
% 18.26/3.20 thf(zip_tseitin_10_type, type, zip_tseitin_10: $i > $o).
% 18.26/3.20 thf(isOpen0_type, type, isOpen0: $i > $o).
% 18.26/3.20 thf(sdtasdt0_type, type, sdtasdt0: $i > $i > $i).
% 18.26/3.20 thf(sk__19_type, type, sk__19: $i).
% 18.26/3.20 thf(aInteger0_type, type, aInteger0: $i > $o).
% 18.26/3.20 thf(zip_tseitin_12_type, type, zip_tseitin_12: $i > $o).
% 18.26/3.20 thf(sdtbsmnsldt0_type, type, sdtbsmnsldt0: $i > $i > $i).
% 18.26/3.20 thf(cS1395_type, type, cS1395: $i).
% 18.26/3.20 thf(sz00_type, type, sz00: $i).
% 18.26/3.20 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 18.26/3.20 thf(szAzrzSzezqlpdtcmdtrp0_type, type, szAzrzSzezqlpdtcmdtrp0: $i > $i > $i).
% 18.26/3.20 thf(stldt0_type, type, stldt0: $i > $i).
% 18.26/3.20 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 18.26/3.20 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 18.26/3.20 thf(zip_tseitin_8_type, type, zip_tseitin_8: $i > $o).
% 18.26/3.20 thf(aDivisorOf0_type, type, aDivisorOf0: $i > $i > $o).
% 18.26/3.20 thf(zip_tseitin_9_type, type, zip_tseitin_9: $i > $o).
% 18.26/3.20 thf(zip_tseitin_11_type, type, zip_tseitin_11: $i > $o).
% 18.26/3.20 thf(sdteqdtlpzmzozddtrp0_type, type, sdteqdtlpzmzozddtrp0: $i > $i > $i > $o).
% 18.26/3.20 thf(isClosed0_type, type, isClosed0: $i > $o).
% 18.26/3.20 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $o).
% 18.26/3.20 thf(sk__2_type, type, sk__2: $i > $i > $i).
% 18.26/3.20 thf(aSet0_type, type, aSet0: $i > $o).
% 18.26/3.20 thf(sdtslmnbsdt0_type, type, sdtslmnbsdt0: $i > $i > $i).
% 18.26/3.20 thf(xA_type, type, xA: $i).
% 18.26/3.20 thf(m__, conjecture,
% 18.26/3.20 (( ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) <=>
% 18.26/3.20 ( ( ( aElementOf0 @ W0 @ xB ) | ( aElementOf0 @ W0 @ xA ) ) &
% 18.26/3.20 ( aInteger0 @ W0 ) ) ) ) &
% 18.26/3.20 ( aSet0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) =>
% 18.26/3.20 ( ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 18.26/3.20 ( ( ~( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) &
% 18.26/3.20 ( aInteger0 @ W0 ) ) ) ) &
% 18.26/3.20 ( aSet0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) <=>
% 18.26/3.20 ( ( ~( aElementOf0 @ W0 @ xA ) ) & ( aInteger0 @ W0 ) ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) <=>
% 18.26/3.20 ( ( ~( aElementOf0 @ W0 @ xB ) ) & ( aInteger0 @ W0 ) ) ) ) =>
% 18.26/3.20 ( ( ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) =
% 18.26/3.20 ( sdtslmnbsdt0 @ ( stldt0 @ xA ) @ ( stldt0 @ xB ) ) ) |
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) &
% 18.26/3.20 ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) &
% 18.26/3.20 ( aInteger0 @ W0 ) ) ) ) ) ) ) ) ) &
% 18.26/3.20 ( ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) <=>
% 18.26/3.20 ( ( ~( aElementOf0 @ W0 @ xB ) ) & ( aInteger0 @ W0 ) ) ) ) &
% 18.26/3.20 ( aSet0 @ ( stldt0 @ xB ) ) ) =>
% 18.26/3.20 ( ( ( ![W0:$i]: ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) &
% 18.26/3.20 ( aSet0 @ cS1395 ) ) =>
% 18.26/3.20 ( ( aSubsetOf0 @ ( stldt0 @ xB ) @ cS1395 ) |
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) =>
% 18.26/3.20 ( aElementOf0 @ W0 @ cS1395 ) ) ) ) ) ) &
% 18.26/3.20 ( ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) <=>
% 18.26/3.20 ( ( ~( aElementOf0 @ W0 @ xA ) ) & ( aInteger0 @ W0 ) ) ) ) &
% 18.26/3.20 ( aSet0 @ ( stldt0 @ xA ) ) ) =>
% 18.26/3.20 ( ( ( ![W0:$i]: ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) &
% 18.26/3.20 ( aSet0 @ cS1395 ) ) =>
% 18.26/3.20 ( ( aSubsetOf0 @ ( stldt0 @ xA ) @ cS1395 ) |
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) =>
% 18.26/3.20 ( aElementOf0 @ W0 @ cS1395 ) ) ) ) ) ))).
% 18.26/3.20 thf(zf_stmt_0, type, zip_tseitin_12 : $i > $o).
% 18.26/3.20 thf(zf_stmt_1, axiom,
% 18.26/3.20 (![W0:$i]:
% 18.26/3.20 ( ( zip_tseitin_12 @ W0 ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) & ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) &
% 18.26/3.20 ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) ) ))).
% 18.26/3.20 thf(zf_stmt_2, type, zip_tseitin_11 : $i > $o).
% 18.26/3.20 thf(zf_stmt_3, axiom,
% 18.26/3.20 (![W0:$i]:
% 18.26/3.20 ( ( zip_tseitin_11 @ W0 ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xB ) ) ) ))).
% 18.26/3.20 thf(zf_stmt_4, type, zip_tseitin_10 : $i > $o).
% 18.26/3.20 thf(zf_stmt_5, axiom,
% 18.26/3.20 (![W0:$i]:
% 18.26/3.20 ( ( zip_tseitin_10 @ W0 ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xA ) ) ) ))).
% 18.26/3.20 thf(zf_stmt_6, type, zip_tseitin_9 : $i > $o).
% 18.26/3.20 thf(zf_stmt_7, axiom,
% 18.26/3.20 (![W0:$i]:
% 18.26/3.20 ( ( zip_tseitin_9 @ W0 ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) &
% 18.26/3.20 ( ~( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) ))).
% 18.26/3.20 thf(zf_stmt_8, type, zip_tseitin_8 : $i > $o).
% 18.26/3.20 thf(zf_stmt_9, axiom,
% 18.26/3.20 (![W0:$i]:
% 18.26/3.20 ( ( zip_tseitin_8 @ W0 ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) & ( zip_tseitin_7 @ W0 ) ) ))).
% 18.26/3.20 thf(zf_stmt_10, type, zip_tseitin_7 : $i > $o).
% 18.26/3.20 thf(zf_stmt_11, axiom,
% 18.26/3.20 (![W0:$i]:
% 18.26/3.20 ( ( zip_tseitin_7 @ W0 ) <=>
% 18.26/3.20 ( ( aElementOf0 @ W0 @ xA ) | ( aElementOf0 @ W0 @ xB ) ) ))).
% 18.26/3.20 thf(zf_stmt_12, conjecture,
% 18.26/3.20 (( ( ( aSet0 @ ( stldt0 @ xA ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xA ) ) ) ) ) ) =>
% 18.26/3.20 ( ( ( aSet0 @ cS1395 ) &
% 18.26/3.20 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) =>
% 18.26/3.20 ( aElementOf0 @ W0 @ cS1395 ) ) ) |
% 18.26/3.20 ( aSubsetOf0 @ ( stldt0 @ xA ) @ cS1395 ) ) ) ) &
% 18.26/3.20 ( ( ( aSet0 @ ( stldt0 @ xB ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xB ) ) ) ) ) ) =>
% 18.26/3.20 ( ( ( aSet0 @ cS1395 ) &
% 18.26/3.20 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) =>
% 18.26/3.20 ( aElementOf0 @ W0 @ cS1395 ) ) ) |
% 18.26/3.20 ( aSubsetOf0 @ ( stldt0 @ xB ) @ cS1395 ) ) ) ) &
% 18.26/3.20 ( ( ( aSet0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) <=>
% 18.26/3.20 ( zip_tseitin_8 @ W0 ) ) ) ) =>
% 18.26/3.20 ( ( ( aSet0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 18.26/3.20 ( zip_tseitin_9 @ W0 ) ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) <=>
% 18.26/3.20 ( zip_tseitin_10 @ W0 ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) <=>
% 18.26/3.20 ( zip_tseitin_11 @ W0 ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 18.26/3.20 ( zip_tseitin_12 @ W0 ) ) ) |
% 18.26/3.20 ( ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) =
% 18.26/3.20 ( sdtslmnbsdt0 @ ( stldt0 @ xA ) @ ( stldt0 @ xB ) ) ) ) ) ) ) ))).
% 18.26/3.20 thf(zf_stmt_13, negated_conjecture,
% 18.26/3.20 (~( ( ( ( aSet0 @ ( stldt0 @ xA ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xA ) ) ) ) ) ) =>
% 18.26/3.20 ( ( ( aSet0 @ cS1395 ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) =>
% 18.26/3.20 ( aElementOf0 @ W0 @ cS1395 ) ) ) |
% 18.26/3.20 ( aSubsetOf0 @ ( stldt0 @ xA ) @ cS1395 ) ) ) ) &
% 18.26/3.20 ( ( ( aSet0 @ ( stldt0 @ xB ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xB ) ) ) ) ) ) =>
% 18.26/3.20 ( ( ( aSet0 @ cS1395 ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) =>
% 18.26/3.20 ( aElementOf0 @ W0 @ cS1395 ) ) ) |
% 18.26/3.20 ( aSubsetOf0 @ ( stldt0 @ xB ) @ cS1395 ) ) ) ) &
% 18.26/3.20 ( ( ( aSet0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) <=>
% 18.26/3.20 ( zip_tseitin_8 @ W0 ) ) ) ) =>
% 18.26/3.20 ( ( ( aSet0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 18.26/3.20 ( zip_tseitin_9 @ W0 ) ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) <=>
% 18.26/3.20 ( zip_tseitin_10 @ W0 ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) <=>
% 18.26/3.20 ( zip_tseitin_11 @ W0 ) ) ) =>
% 18.26/3.20 ( ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @
% 18.26/3.20 W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 18.26/3.20 ( zip_tseitin_12 @ W0 ) ) ) |
% 18.26/3.20 ( ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) =
% 18.26/3.20 ( sdtslmnbsdt0 @ ( stldt0 @ xA ) @ ( stldt0 @ xB ) ) ) ) ) ) ) ) )),
% 18.26/3.20 inference('cnf.neg', [status(esa)], [zf_stmt_12])).
% 18.26/3.20 thf(zip_derived_cl885, plain,
% 18.26/3.20 (![X6 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (aElementOf0 @ X6 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | ~ (zip_tseitin_9 @ X6))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_13])).
% 18.26/3.20 thf(mSubset, axiom,
% 18.26/3.20 (![W0:$i]:
% 18.26/3.20 ( ( aSet0 @ W0 ) =>
% 18.26/3.20 ( ![W1:$i]:
% 18.26/3.20 ( ( aSubsetOf0 @ W1 @ W0 ) <=>
% 18.26/3.20 ( ( aSet0 @ W1 ) &
% 18.26/3.20 ( ![W2:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W2 @ W1 ) => ( aElementOf0 @ W2 @ W0 ) ) ) ) ) ) ))).
% 18.26/3.20 thf(zip_derived_cl43, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ X0 @ X1) @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(m__1826, axiom,
% 18.26/3.20 (( isOpen0 @ ( stldt0 @ xB ) ) &
% 18.26/3.20 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xB ) => ( aElementOf0 @ W0 @ cS1395 ) ) ) &
% 18.26/3.20 ( aSubsetOf0 @ xB @ cS1395 ) & ( isClosed0 @ xA ) &
% 18.26/3.20 ( aSubsetOf0 @ xA @ cS1395 ) & ( aSet0 @ cS1395 ) &
% 18.26/3.20 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) &
% 18.26/3.20 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xA ) => ( aElementOf0 @ W0 @ cS1395 ) ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xB ) ) ) ) ) &
% 18.26/3.20 ( aSet0 @ xB ) & ( isClosed0 @ xB ) &
% 18.26/3.20 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) &
% 18.26/3.20 ( isOpen0 @ ( stldt0 @ xA ) ) & ( aSet0 @ xA ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) =>
% 18.26/3.20 ( ?[W1:$i]:
% 18.26/3.20 ( ( aSubsetOf0 @
% 18.26/3.20 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @ ( stldt0 @ xA ) ) &
% 18.26/3.20 ( ![W2:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 18.26/3.20 ( aElementOf0 @ W2 @ ( stldt0 @ xA ) ) ) ) &
% 18.26/3.20 ( ![W2:$i]:
% 18.26/3.20 ( ( ( ( aInteger0 @ W2 ) &
% 18.26/3.20 ( ( ?[W3:$i]:
% 18.26/3.20 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 18.26/3.20 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 18.26/3.20 ( aInteger0 @ W3 ) ) ) |
% 18.26/3.20 ( aDivisorOf0 @ W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 18.26/3.20 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) =>
% 18.26/3.20 ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) &
% 18.26/3.20 ( ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 18.26/3.20 ( ( aInteger0 @ W2 ) &
% 18.26/3.20 ( ?[W3:$i]:
% 18.26/3.20 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 18.26/3.20 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 18.26/3.20 ( aInteger0 @ W3 ) ) ) &
% 18.26/3.20 ( aDivisorOf0 @ W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 18.26/3.20 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) ) ) &
% 18.26/3.20 ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) &
% 18.26/3.20 ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) =>
% 18.26/3.20 ( ?[W1:$i]:
% 18.26/3.20 ( ( aSubsetOf0 @
% 18.26/3.20 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @ ( stldt0 @ xB ) ) &
% 18.26/3.20 ( ![W2:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 18.26/3.20 ( aElementOf0 @ W2 @ ( stldt0 @ xB ) ) ) ) &
% 18.26/3.20 ( ![W2:$i]:
% 18.26/3.20 ( ( ( ( aInteger0 @ W2 ) &
% 18.26/3.20 ( ( ?[W3:$i]:
% 18.26/3.20 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 18.26/3.20 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 18.26/3.20 ( aInteger0 @ W3 ) ) ) |
% 18.26/3.20 ( aDivisorOf0 @ W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 18.26/3.20 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) =>
% 18.26/3.20 ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) &
% 18.26/3.20 ( ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 18.26/3.20 ( ( aInteger0 @ W2 ) &
% 18.26/3.20 ( ?[W3:$i]:
% 18.26/3.20 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 18.26/3.20 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 18.26/3.20 ( aInteger0 @ W3 ) ) ) &
% 18.26/3.20 ( aDivisorOf0 @ W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 18.26/3.20 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) ) ) &
% 18.26/3.20 ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) &
% 18.26/3.20 ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) &
% 18.26/3.20 ( ![W0:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) <=>
% 18.26/3.20 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xA ) ) ) ) ) &
% 18.26/3.20 ( aSet0 @ ( stldt0 @ xB ) ) & ( aSet0 @ ( stldt0 @ xA ) ))).
% 18.26/3.20 thf(zip_derived_cl138, plain,
% 18.26/3.20 (![X0 : $i]: ( (aElementOf0 @ X0 @ cS1395) | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl108, plain,
% 18.26/3.20 (![X0 : $i]: ( (aInteger0 @ X0) | ~ (aElementOf0 @ X0 @ (stldt0 @ xA)))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl4998, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ cS1395) | ~ (aElementOf0 @ X0 @ (stldt0 @ xA)))),
% 18.26/3.20 inference('s_sup+', [status(thm)], [zip_derived_cl138, zip_derived_cl108])).
% 18.26/3.20 thf(zip_derived_cl5037, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ (stldt0 @ xA) @ X0)
% 18.26/3.20 | ~ (aSet0 @ (stldt0 @ xA))
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ (stldt0 @ xA) @ X0) @ cS1395))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl43, zip_derived_cl4998])).
% 18.26/3.20 thf(zip_derived_cl105, plain, ( (aSet0 @ (stldt0 @ xA))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5046, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ (stldt0 @ xA) @ X0)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ (stldt0 @ xA) @ X0) @ cS1395))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5037, zip_derived_cl105])).
% 18.26/3.20 thf(zip_derived_cl42, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | ~ (aElementOf0 @ (sk__2 @ X0 @ X1) @ X1)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl7663, plain,
% 18.26/3.20 (( (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | ~ (aSet0 @ cS1395)
% 18.26/3.20 | ~ (aSet0 @ (stldt0 @ xA))
% 18.26/3.20 | (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | ~ (aSet0 @ cS1395))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl5046, zip_derived_cl42])).
% 18.26/3.20 thf(zip_derived_cl148, plain, ( (aSet0 @ cS1395)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl105, plain, ( (aSet0 @ (stldt0 @ xA))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl148, plain, ( (aSet0 @ cS1395)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl7665, plain,
% 18.26/3.20 (( (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | (aSubsetOf0 @ (stldt0 @ xA) @ cS1395))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7663, zip_derived_cl148, zip_derived_cl105,
% 18.26/3.20 zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl7666, plain, ( (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl7665])).
% 18.26/3.20 thf(zip_derived_cl7678, plain,
% 18.26/3.20 (![X6 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (aElementOf0 @ X6 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | ~ (zip_tseitin_9 @ X6))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl885, zip_derived_cl7666])).
% 18.26/3.20 thf(zip_derived_cl43, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ X0 @ X1) @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl143, plain,
% 18.26/3.20 (![X0 : $i]: ( (aInteger0 @ X0) | ~ (aElementOf0 @ X0 @ (stldt0 @ xB)))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl138, plain,
% 18.26/3.20 (![X0 : $i]: ( (aElementOf0 @ X0 @ cS1395) | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5030, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (stldt0 @ xB)) | (aElementOf0 @ X0 @ cS1395))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl143, zip_derived_cl138])).
% 18.26/3.20 thf(zip_derived_cl5038, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ (stldt0 @ xB) @ X0)
% 18.26/3.20 | ~ (aSet0 @ (stldt0 @ xB))
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ (stldt0 @ xB) @ X0) @ cS1395))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl43, zip_derived_cl5030])).
% 18.26/3.20 thf(zip_derived_cl106, plain, ( (aSet0 @ (stldt0 @ xB))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5047, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ (stldt0 @ xB) @ X0)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ (stldt0 @ xB) @ X0) @ cS1395))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5038, zip_derived_cl106])).
% 18.26/3.20 thf(zip_derived_cl42, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | ~ (aElementOf0 @ (sk__2 @ X0 @ X1) @ X1)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl8556, plain,
% 18.26/3.20 (( (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | ~ (aSet0 @ cS1395)
% 18.26/3.20 | ~ (aSet0 @ (stldt0 @ xB))
% 18.26/3.20 | (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | ~ (aSet0 @ cS1395))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl5047, zip_derived_cl42])).
% 18.26/3.20 thf(zip_derived_cl148, plain, ( (aSet0 @ cS1395)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl106, plain, ( (aSet0 @ (stldt0 @ xB))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl148, plain, ( (aSet0 @ cS1395)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl8558, plain,
% 18.26/3.20 (( (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (aSubsetOf0 @ (stldt0 @ xB) @ cS1395))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl8556, zip_derived_cl148, zip_derived_cl106,
% 18.26/3.20 zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl8559, plain, ( (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl8558])).
% 18.26/3.20 thf(zip_derived_cl8575, plain,
% 18.26/3.20 (![X6 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X6 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | ~ (zip_tseitin_9 @ X6))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7678, zip_derived_cl8559])).
% 18.26/3.20 thf(zip_derived_cl162, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (zip_tseitin_9 @ X0)
% 18.26/3.20 | (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_7])).
% 18.26/3.20 thf(zip_derived_cl8941, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('s_sup+', [status(thm)],
% 18.26/3.20 [zip_derived_cl8575, zip_derived_cl162])).
% 18.26/3.20 thf(zip_derived_cl882, plain,
% 18.26/3.20 ((~ (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (zip_tseitin_12 @ sk__19)
% 18.26/3.20 | (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_13])).
% 18.26/3.20 thf(zip_derived_cl7666, plain, ( (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl7665])).
% 18.26/3.20 thf(zip_derived_cl7675, plain,
% 18.26/3.20 ((~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (zip_tseitin_12 @ sk__19)
% 18.26/3.20 | (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl882, zip_derived_cl7666])).
% 18.26/3.20 thf(zip_derived_cl8559, plain, ( (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl8558])).
% 18.26/3.20 thf(zip_derived_cl8572, plain,
% 18.26/3.20 (( (zip_tseitin_12 @ sk__19)
% 18.26/3.20 | (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7675, zip_derived_cl8559])).
% 18.26/3.20 thf(zip_derived_cl169, plain,
% 18.26/3.20 (![X0 : $i]: ( (aInteger0 @ X0) | ~ (zip_tseitin_12 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_1])).
% 18.26/3.20 thf(zip_derived_cl8616, plain,
% 18.26/3.20 (( (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | (aInteger0 @ sk__19))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8572, zip_derived_cl169])).
% 18.26/3.20 thf(zip_derived_cl886, plain,
% 18.26/3.20 (![X7 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (zip_tseitin_9 @ X7)
% 18.26/3.20 | ~ (aElementOf0 @ X7 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_13])).
% 18.26/3.20 thf(zip_derived_cl7666, plain, ( (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl7665])).
% 18.26/3.20 thf(zip_derived_cl7679, plain,
% 18.26/3.20 (![X7 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (zip_tseitin_9 @ X7)
% 18.26/3.20 | ~ (aElementOf0 @ X7 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl886, zip_derived_cl7666])).
% 18.26/3.20 thf(zip_derived_cl8559, plain, ( (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl8558])).
% 18.26/3.20 thf(zip_derived_cl8576, plain,
% 18.26/3.20 (![X7 : $i]:
% 18.26/3.20 ( (zip_tseitin_9 @ X7)
% 18.26/3.20 | ~ (aElementOf0 @ X7 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7679, zip_derived_cl8559])).
% 18.26/3.20 thf(zip_derived_cl160, plain,
% 18.26/3.20 (![X0 : $i]: ( (aInteger0 @ X0) | ~ (zip_tseitin_9 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_7])).
% 18.26/3.20 thf(zip_derived_cl8706, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | (aInteger0 @ X0))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8576, zip_derived_cl160])).
% 18.26/3.20 thf(zip_derived_cl8811, plain,
% 18.26/3.20 (( (aInteger0 @ sk__19) | (aInteger0 @ sk__19))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8616, zip_derived_cl8706])).
% 18.26/3.20 thf(zip_derived_cl8817, plain, ( (aInteger0 @ sk__19)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl8811])).
% 18.26/3.20 thf(zip_derived_cl107, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (stldt0 @ xA))
% 18.26/3.20 | (aElementOf0 @ X0 @ xA)
% 18.26/3.20 | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl8818, plain,
% 18.26/3.20 (( (aElementOf0 @ sk__19 @ (stldt0 @ xA)) | (aElementOf0 @ sk__19 @ xA))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8817, zip_derived_cl107])).
% 18.26/3.20 thf(zip_derived_cl142, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (stldt0 @ xB))
% 18.26/3.20 | (aElementOf0 @ X0 @ xB)
% 18.26/3.20 | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl108, plain,
% 18.26/3.20 (![X0 : $i]: ( (aInteger0 @ X0) | ~ (aElementOf0 @ X0 @ (stldt0 @ xA)))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5705, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ xB)
% 18.26/3.20 | (aElementOf0 @ X0 @ (stldt0 @ xB))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ (stldt0 @ xA)))),
% 18.26/3.20 inference('s_sup+', [status(thm)], [zip_derived_cl142, zip_derived_cl108])).
% 18.26/3.20 thf(zip_derived_cl172, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (zip_tseitin_12 @ X0)
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ (stldt0 @ xB))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ (stldt0 @ xA))
% 18.26/3.20 | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_1])).
% 18.26/3.20 thf(zip_derived_cl108, plain,
% 18.26/3.20 (![X0 : $i]: ( (aInteger0 @ X0) | ~ (aElementOf0 @ X0 @ (stldt0 @ xA)))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5286, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (stldt0 @ xA))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ (stldt0 @ xB))
% 18.26/3.20 | (zip_tseitin_12 @ X0))),
% 18.26/3.20 inference('clc', [status(thm)], [zip_derived_cl172, zip_derived_cl108])).
% 18.26/3.20 thf(zip_derived_cl881, plain,
% 18.26/3.20 ((~ (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | ~ (zip_tseitin_12 @ sk__19)
% 18.26/3.20 | ~ (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_13])).
% 18.26/3.20 thf(zip_derived_cl5865, plain,
% 18.26/3.20 ((~ (aElementOf0 @ sk__19 @ (stldt0 @ xB))
% 18.26/3.20 | ~ (aElementOf0 @ sk__19 @ (stldt0 @ xA))
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | ~ (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl5286, zip_derived_cl881])).
% 18.26/3.20 thf(zip_derived_cl5883, plain,
% 18.26/3.20 ((~ (aElementOf0 @ sk__19 @ (stldt0 @ xA))
% 18.26/3.20 | (aElementOf0 @ sk__19 @ xB)
% 18.26/3.20 | ~ (aElementOf0 @ sk__19 @ (stldt0 @ xA))
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | ~ (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl5705, zip_derived_cl5865])).
% 18.26/3.20 thf(zip_derived_cl5885, plain,
% 18.26/3.20 ((~ (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | (aElementOf0 @ sk__19 @ xB)
% 18.26/3.20 | ~ (aElementOf0 @ sk__19 @ (stldt0 @ xA)))),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl5883])).
% 18.26/3.20 thf(zip_derived_cl7666, plain, ( (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl7665])).
% 18.26/3.20 thf(zip_derived_cl7707, plain,
% 18.26/3.20 ((~ (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (aElementOf0 @ sk__19 @ xB)
% 18.26/3.20 | ~ (aElementOf0 @ sk__19 @ (stldt0 @ xA)))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl5885, zip_derived_cl7666])).
% 18.26/3.20 thf(zip_derived_cl8559, plain, ( (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl8558])).
% 18.26/3.20 thf(zip_derived_cl8579, plain,
% 18.26/3.20 ((~ (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | (aElementOf0 @ sk__19 @ xB)
% 18.26/3.20 | ~ (aElementOf0 @ sk__19 @ (stldt0 @ xA)))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7707, zip_derived_cl8559])).
% 18.26/3.20 thf(zip_derived_cl9134, plain,
% 18.26/3.20 (( (aElementOf0 @ sk__19 @ xA)
% 18.26/3.20 | ~ (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | (aElementOf0 @ sk__19 @ xB))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8818, zip_derived_cl8579])).
% 18.26/3.20 thf(zip_derived_cl9278, plain,
% 18.26/3.20 ((~ (aInteger0 @ sk__19)
% 18.26/3.20 | (aElementOf0 @ sk__19 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | (aElementOf0 @ sk__19 @ xA)
% 18.26/3.20 | (aElementOf0 @ sk__19 @ xB))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8941, zip_derived_cl9134])).
% 18.26/3.20 thf(zip_derived_cl8817, plain, ( (aInteger0 @ sk__19)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl8811])).
% 18.26/3.20 thf(zip_derived_cl9281, plain,
% 18.26/3.20 (( (aElementOf0 @ sk__19 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | (aElementOf0 @ sk__19 @ xA)
% 18.26/3.20 | (aElementOf0 @ sk__19 @ xB))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl9278, zip_derived_cl8817])).
% 18.26/3.20 thf(zip_derived_cl877, plain,
% 18.26/3.20 (![X1 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (zip_tseitin_8 @ X1)
% 18.26/3.20 | ~ (aElementOf0 @ X1 @ (sdtbsmnsldt0 @ xA @ xB)))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_13])).
% 18.26/3.20 thf(zip_derived_cl7666, plain, ( (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl7665])).
% 18.26/3.20 thf(zip_derived_cl7670, plain,
% 18.26/3.20 (![X1 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (zip_tseitin_8 @ X1)
% 18.26/3.20 | ~ (aElementOf0 @ X1 @ (sdtbsmnsldt0 @ xA @ xB)))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl877, zip_derived_cl7666])).
% 18.26/3.20 thf(zip_derived_cl8559, plain, ( (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl8558])).
% 18.26/3.20 thf(zip_derived_cl8567, plain,
% 18.26/3.20 (![X1 : $i]:
% 18.26/3.20 ( (zip_tseitin_8 @ X1)
% 18.26/3.20 | ~ (aElementOf0 @ X1 @ (sdtbsmnsldt0 @ xA @ xB)))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7670, zip_derived_cl8559])).
% 18.26/3.20 thf(zip_derived_cl158, plain,
% 18.26/3.20 (![X0 : $i]: ( (zip_tseitin_7 @ X0) | ~ (zip_tseitin_8 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_9])).
% 18.26/3.20 thf(zip_derived_cl154, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ xB)
% 18.26/3.20 | (aElementOf0 @ X0 @ xA)
% 18.26/3.20 | ~ (zip_tseitin_7 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_11])).
% 18.26/3.20 thf(zip_derived_cl4351, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (zip_tseitin_8 @ X0)
% 18.26/3.20 | (aElementOf0 @ X0 @ xA)
% 18.26/3.20 | (aElementOf0 @ X0 @ xB))),
% 18.26/3.20 inference('dp-resolution', [status(thm)],
% 18.26/3.20 [zip_derived_cl158, zip_derived_cl154])).
% 18.26/3.20 thf(zip_derived_cl8687, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | (aElementOf0 @ X0 @ xA)
% 18.26/3.20 | (aElementOf0 @ X0 @ xB))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8567, zip_derived_cl4351])).
% 18.26/3.20 thf(zip_derived_cl9426, plain,
% 18.26/3.20 (( (aElementOf0 @ sk__19 @ xB) | (aElementOf0 @ sk__19 @ xA))),
% 18.26/3.20 inference('clc', [status(thm)], [zip_derived_cl9281, zip_derived_cl8687])).
% 18.26/3.20 thf(zip_derived_cl144, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ xB) | ~ (aElementOf0 @ X0 @ (stldt0 @ xB)))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl9428, plain,
% 18.26/3.20 (( (aElementOf0 @ sk__19 @ xA) | ~ (aElementOf0 @ sk__19 @ (stldt0 @ xB)))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl9426, zip_derived_cl144])).
% 18.26/3.20 thf(zip_derived_cl8572, plain,
% 18.26/3.20 (( (zip_tseitin_12 @ sk__19)
% 18.26/3.20 | (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7675, zip_derived_cl8559])).
% 18.26/3.20 thf(zip_derived_cl171, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (stldt0 @ xB)) | ~ (zip_tseitin_12 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_1])).
% 18.26/3.20 thf(zip_derived_cl8618, plain,
% 18.26/3.20 (( (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | (aElementOf0 @ sk__19 @ (stldt0 @ xB)))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8572, zip_derived_cl171])).
% 18.26/3.20 thf(zip_derived_cl8576, plain,
% 18.26/3.20 (![X7 : $i]:
% 18.26/3.20 ( (zip_tseitin_9 @ X7)
% 18.26/3.20 | ~ (aElementOf0 @ X7 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7679, zip_derived_cl8559])).
% 18.26/3.20 thf(zip_derived_cl9426, plain,
% 18.26/3.20 (( (aElementOf0 @ sk__19 @ xB) | (aElementOf0 @ sk__19 @ xA))),
% 18.26/3.20 inference('clc', [status(thm)], [zip_derived_cl9281, zip_derived_cl8687])).
% 18.26/3.20 thf(zip_derived_cl876, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 18.26/3.20 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | ~ (zip_tseitin_8 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_13])).
% 18.26/3.20 thf(zip_derived_cl7666, plain, ( (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl7665])).
% 18.26/3.20 thf(zip_derived_cl7669, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 18.26/3.20 | (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | ~ (zip_tseitin_8 @ X0))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl876, zip_derived_cl7666])).
% 18.26/3.20 thf(zip_derived_cl8559, plain, ( (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl8558])).
% 18.26/3.20 thf(zip_derived_cl8566, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | ~ (zip_tseitin_8 @ X0))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7669, zip_derived_cl8559])).
% 18.26/3.20 thf(zip_derived_cl156, plain,
% 18.26/3.20 (![X0 : $i]: ( (zip_tseitin_7 @ X0) | ~ (aElementOf0 @ X0 @ xB))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_11])).
% 18.26/3.20 thf(zip_derived_cl159, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (zip_tseitin_8 @ X0) | ~ (zip_tseitin_7 @ X0) | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_9])).
% 18.26/3.20 thf(zip_derived_cl4353, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ xB)
% 18.26/3.20 | ~ (aInteger0 @ X0)
% 18.26/3.20 | (zip_tseitin_8 @ X0))),
% 18.26/3.20 inference('dp-resolution', [status(thm)],
% 18.26/3.20 [zip_derived_cl156, zip_derived_cl159])).
% 18.26/3.20 thf(zip_derived_cl8884, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ xB)
% 18.26/3.20 | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('s_sup+', [status(thm)],
% 18.26/3.20 [zip_derived_cl8566, zip_derived_cl4353])).
% 18.26/3.20 thf(zip_derived_cl43, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ X0 @ X1) @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl152, plain,
% 18.26/3.20 (![X0 : $i]: ( (aElementOf0 @ X0 @ cS1395) | ~ (aElementOf0 @ X0 @ xB))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5043, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ xB @ X0)
% 18.26/3.20 | ~ (aSet0 @ xB)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ xB @ X0) @ cS1395))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl43, zip_derived_cl152])).
% 18.26/3.20 thf(zip_derived_cl141, plain, ( (aSet0 @ xB)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5052, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ xB @ X0)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ xB @ X0) @ cS1395))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5043, zip_derived_cl141])).
% 18.26/3.20 thf(zip_derived_cl139, plain,
% 18.26/3.20 (![X0 : $i]: ( (aInteger0 @ X0) | ~ (aElementOf0 @ X0 @ cS1395))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl43, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ X0 @ X1) @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl43, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ X0 @ X1) @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl42, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | ~ (aElementOf0 @ (sk__2 @ X0 @ X1) @ X1)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl5045, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X0)
% 18.26/3.20 | ~ (aSet0 @ X0)
% 18.26/3.20 | ~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X0)
% 18.26/3.20 | ~ (aSet0 @ X0))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl43, zip_derived_cl42])).
% 18.26/3.20 thf(zip_derived_cl5054, plain,
% 18.26/3.20 (![X0 : $i]: ( (aSubsetOf0 @ X0 @ X0) | ~ (aSet0 @ X0))),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl5045])).
% 18.26/3.20 thf(mComplement, axiom,
% 18.26/3.20 (![W0:$i]:
% 18.26/3.20 ( ( aSubsetOf0 @ W0 @ cS1395 ) =>
% 18.26/3.20 ( ![W1:$i]:
% 18.26/3.20 ( ( ( W1 ) = ( stldt0 @ W0 ) ) <=>
% 18.26/3.20 ( ( aSet0 @ W1 ) &
% 18.26/3.20 ( ![W2:$i]:
% 18.26/3.20 ( ( aElementOf0 @ W2 @ W1 ) <=>
% 18.26/3.20 ( ( aInteger0 @ W2 ) & ( ~( aElementOf0 @ W2 @ W0 ) ) ) ) ) ) ) ) ))).
% 18.26/3.20 thf(zip_derived_cl85, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 18.26/3.20 (((X1) != (stldt0 @ X0))
% 18.26/3.20 | (aInteger0 @ X2)
% 18.26/3.20 | ~ (aElementOf0 @ X2 @ X1)
% 18.26/3.20 | ~ (aSubsetOf0 @ X0 @ cS1395))),
% 18.26/3.20 inference('cnf', [status(esa)], [mComplement])).
% 18.26/3.20 thf(zip_derived_cl5248, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ X0 @ cS1395)
% 18.26/3.20 | ~ (aElementOf0 @ X1 @ (stldt0 @ X0))
% 18.26/3.20 | (aInteger0 @ X1))),
% 18.26/3.20 inference('eq_res', [status(thm)], [zip_derived_cl85])).
% 18.26/3.20 thf(zip_derived_cl5279, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ cS1395)
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ (stldt0 @ cS1395))
% 18.26/3.20 | (aInteger0 @ X0))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl5054, zip_derived_cl5248])).
% 18.26/3.20 thf(zip_derived_cl148, plain, ( (aSet0 @ cS1395)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5282, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (stldt0 @ cS1395)) | (aInteger0 @ X0))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5279, zip_derived_cl148])).
% 18.26/3.20 thf(mAddZero, axiom,
% 18.26/3.20 (![W0:$i]:
% 18.26/3.20 ( ( aInteger0 @ W0 ) =>
% 18.26/3.20 ( ( ( sdtpldt0 @ W0 @ sz00 ) = ( W0 ) ) &
% 18.26/3.20 ( ( W0 ) = ( sdtpldt0 @ sz00 @ W0 ) ) ) ))).
% 18.26/3.20 thf(zip_derived_cl8, plain,
% 18.26/3.20 (![X0 : $i]: (((sdtpldt0 @ X0 @ sz00) = (X0)) | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [mAddZero])).
% 18.26/3.20 thf(zip_derived_cl138, plain,
% 18.26/3.20 (![X0 : $i]: ( (aElementOf0 @ X0 @ cS1395) | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(mIntPlus, axiom,
% 18.26/3.20 (![W0:$i,W1:$i]:
% 18.26/3.20 ( ( ( aInteger0 @ W0 ) & ( aInteger0 @ W1 ) ) =>
% 18.26/3.20 ( aInteger0 @ ( sdtpldt0 @ W0 @ W1 ) ) ))).
% 18.26/3.20 thf(zip_derived_cl4, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aInteger0 @ X0)
% 18.26/3.20 | ~ (aInteger0 @ X1)
% 18.26/3.20 | (aInteger0 @ (sdtpldt0 @ X0 @ X1)))),
% 18.26/3.20 inference('cnf', [status(esa)], [mIntPlus])).
% 18.26/3.20 thf(zip_derived_cl4910, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 ( (aElementOf0 @ (sdtpldt0 @ X1 @ X0) @ cS1395)
% 18.26/3.20 | ~ (aInteger0 @ X1)
% 18.26/3.20 | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('s_sup+', [status(thm)], [zip_derived_cl138, zip_derived_cl4])).
% 18.26/3.20 thf(zip_derived_cl5054, plain,
% 18.26/3.20 (![X0 : $i]: ( (aSubsetOf0 @ X0 @ X0) | ~ (aSet0 @ X0))),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl5045])).
% 18.26/3.20 thf(zip_derived_cl86, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 18.26/3.20 (((X1) != (stldt0 @ X0))
% 18.26/3.20 | ~ (aElementOf0 @ X2 @ X0)
% 18.26/3.20 | ~ (aElementOf0 @ X2 @ X1)
% 18.26/3.20 | ~ (aSubsetOf0 @ X0 @ cS1395))),
% 18.26/3.20 inference('cnf', [status(esa)], [mComplement])).
% 18.26/3.20 thf(zip_derived_cl5077, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ X0 @ cS1395)
% 18.26/3.20 | ~ (aElementOf0 @ X1 @ (stldt0 @ X0))
% 18.26/3.20 | ~ (aElementOf0 @ X1 @ X0))),
% 18.26/3.20 inference('eq_res', [status(thm)], [zip_derived_cl86])).
% 18.26/3.20 thf(zip_derived_cl5078, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ cS1395)
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ (stldt0 @ cS1395))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ cS1395))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl5054, zip_derived_cl5077])).
% 18.26/3.20 thf(zip_derived_cl148, plain, ( (aSet0 @ cS1395)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5081, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (stldt0 @ cS1395))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ cS1395))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5078, zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl5109, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aInteger0 @ X0)
% 18.26/3.20 | ~ (aInteger0 @ X1)
% 18.26/3.20 | ~ (aElementOf0 @ (sdtpldt0 @ X1 @ X0) @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl4910, zip_derived_cl5081])).
% 18.26/3.20 thf(zip_derived_cl5228, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aInteger0 @ X0)
% 18.26/3.20 | ~ (aInteger0 @ sz00)
% 18.26/3.20 | ~ (aInteger0 @ X0)
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl8, zip_derived_cl5109])).
% 18.26/3.20 thf(mIntZero, axiom, (aInteger0 @ sz00)).
% 18.26/3.20 thf(zip_derived_cl1, plain, ( (aInteger0 @ sz00)),
% 18.26/3.20 inference('cnf', [status(esa)], [mIntZero])).
% 18.26/3.20 thf(zip_derived_cl5238, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aInteger0 @ X0)
% 18.26/3.20 | ~ (aInteger0 @ X0)
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5228, zip_derived_cl1])).
% 18.26/3.20 thf(zip_derived_cl5239, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (stldt0 @ cS1395)) | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl5238])).
% 18.26/3.20 thf(zip_derived_cl5293, plain,
% 18.26/3.20 (![X0 : $i]: ~ (aElementOf0 @ X0 @ (stldt0 @ cS1395))),
% 18.26/3.20 inference('clc', [status(thm)], [zip_derived_cl5282, zip_derived_cl5239])).
% 18.26/3.20 thf(zip_derived_cl5294, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ (stldt0 @ cS1395) @ X0)
% 18.26/3.20 | ~ (aSet0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl43, zip_derived_cl5293])).
% 18.26/3.20 thf(zip_derived_cl5054, plain,
% 18.26/3.20 (![X0 : $i]: ( (aSubsetOf0 @ X0 @ X0) | ~ (aSet0 @ X0))),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl5045])).
% 18.26/3.20 thf(zip_derived_cl87, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (((X1) != (stldt0 @ X0))
% 18.26/3.20 | (aSet0 @ X1)
% 18.26/3.20 | ~ (aSubsetOf0 @ X0 @ cS1395))),
% 18.26/3.20 inference('cnf', [status(esa)], [mComplement])).
% 18.26/3.20 thf(zip_derived_cl5170, plain,
% 18.26/3.20 (![X0 : $i]: (~ (aSubsetOf0 @ X0 @ cS1395) | (aSet0 @ (stldt0 @ X0)))),
% 18.26/3.20 inference('eq_res', [status(thm)], [zip_derived_cl87])).
% 18.26/3.20 thf(zip_derived_cl5171, plain,
% 18.26/3.20 ((~ (aSet0 @ cS1395) | (aSet0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl5054, zip_derived_cl5170])).
% 18.26/3.20 thf(zip_derived_cl148, plain, ( (aSet0 @ cS1395)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5174, plain, ( (aSet0 @ (stldt0 @ cS1395))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5171, zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl5295, plain,
% 18.26/3.20 (![X0 : $i]: (~ (aSet0 @ X0) | (aSubsetOf0 @ (stldt0 @ cS1395) @ X0))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl5294, zip_derived_cl5174])).
% 18.26/3.20 thf(zip_derived_cl84, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 18.26/3.20 (((X1) != (stldt0 @ X0))
% 18.26/3.20 | (aElementOf0 @ X2 @ X1)
% 18.26/3.20 | (aElementOf0 @ X2 @ X0)
% 18.26/3.20 | ~ (aInteger0 @ X2)
% 18.26/3.20 | ~ (aSubsetOf0 @ X0 @ cS1395))),
% 18.26/3.20 inference('cnf', [status(esa)], [mComplement])).
% 18.26/3.20 thf(zip_derived_cl5224, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ X0 @ cS1395)
% 18.26/3.20 | ~ (aInteger0 @ X1)
% 18.26/3.20 | (aElementOf0 @ X1 @ X0)
% 18.26/3.20 | (aElementOf0 @ X1 @ (stldt0 @ X0)))),
% 18.26/3.20 inference('eq_res', [status(thm)], [zip_derived_cl84])).
% 18.26/3.20 thf(zip_derived_cl6190, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ cS1395)
% 18.26/3.20 | ~ (aInteger0 @ X0)
% 18.26/3.20 | (aElementOf0 @ X0 @ (stldt0 @ cS1395))
% 18.26/3.20 | (aElementOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl5295, zip_derived_cl5224])).
% 18.26/3.20 thf(zip_derived_cl148, plain, ( (aSet0 @ cS1395)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5293, plain,
% 18.26/3.20 (![X0 : $i]: ~ (aElementOf0 @ X0 @ (stldt0 @ cS1395))),
% 18.26/3.20 inference('clc', [status(thm)], [zip_derived_cl5282, zip_derived_cl5239])).
% 18.26/3.20 thf(zip_derived_cl6195, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aInteger0 @ X0)
% 18.26/3.20 | (aElementOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl6190, zip_derived_cl148, zip_derived_cl5293])).
% 18.26/3.20 thf(zip_derived_cl42, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | ~ (aElementOf0 @ (sk__2 @ X0 @ X1) @ X1)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl6204, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aInteger0 @ (sk__2 @ X0 @ (stldt0 @ (stldt0 @ cS1395))))
% 18.26/3.20 | ~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | ~ (aSet0 @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl6195, zip_derived_cl42])).
% 18.26/3.20 thf(zip_derived_cl5295, plain,
% 18.26/3.20 (![X0 : $i]: (~ (aSet0 @ X0) | (aSubsetOf0 @ (stldt0 @ cS1395) @ X0))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl5294, zip_derived_cl5174])).
% 18.26/3.20 thf(zip_derived_cl5170, plain,
% 18.26/3.20 (![X0 : $i]: (~ (aSubsetOf0 @ X0 @ cS1395) | (aSet0 @ (stldt0 @ X0)))),
% 18.26/3.20 inference('eq_res', [status(thm)], [zip_derived_cl87])).
% 18.26/3.20 thf(zip_derived_cl5312, plain,
% 18.26/3.20 ((~ (aSet0 @ cS1395) | (aSet0 @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl5295, zip_derived_cl5170])).
% 18.26/3.20 thf(zip_derived_cl148, plain, ( (aSet0 @ cS1395)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5333, plain, ( (aSet0 @ (stldt0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5312, zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl6205, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aInteger0 @ (sk__2 @ X0 @ (stldt0 @ (stldt0 @ cS1395))))
% 18.26/3.20 | ~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl6204, zip_derived_cl5333])).
% 18.26/3.20 thf(zip_derived_cl6525, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ (sk__2 @ X0 @ (stldt0 @ (stldt0 @ cS1395))) @ cS1395)
% 18.26/3.20 | ~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl139, zip_derived_cl6205])).
% 18.26/3.20 thf(zip_derived_cl7421, plain,
% 18.26/3.20 (( (aSubsetOf0 @ xB @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | ~ (aSet0 @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | ~ (aSet0 @ xB)
% 18.26/3.20 | (aSubsetOf0 @ xB @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl5052, zip_derived_cl6525])).
% 18.26/3.20 thf(zip_derived_cl5333, plain, ( (aSet0 @ (stldt0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5312, zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl141, plain, ( (aSet0 @ xB)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl7424, plain,
% 18.26/3.20 (( (aSubsetOf0 @ xB @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | (aSubsetOf0 @ xB @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7421, zip_derived_cl5333, zip_derived_cl141])).
% 18.26/3.20 thf(zip_derived_cl7425, plain,
% 18.26/3.20 ( (aSubsetOf0 @ xB @ (stldt0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl7424])).
% 18.26/3.20 thf(zip_derived_cl44, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | (aElementOf0 @ X2 @ X1)
% 18.26/3.20 | ~ (aElementOf0 @ X2 @ X0)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl7426, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ xB)
% 18.26/3.20 | ~ (aSet0 @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl7425, zip_derived_cl44])).
% 18.26/3.20 thf(zip_derived_cl5333, plain, ( (aSet0 @ (stldt0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5312, zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl7428, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ xB))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7426, zip_derived_cl5333])).
% 18.26/3.20 thf(zip_derived_cl5295, plain,
% 18.26/3.20 (![X0 : $i]: (~ (aSet0 @ X0) | (aSubsetOf0 @ (stldt0 @ cS1395) @ X0))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl5294, zip_derived_cl5174])).
% 18.26/3.20 thf(zip_derived_cl5248, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ X0 @ cS1395)
% 18.26/3.20 | ~ (aElementOf0 @ X1 @ (stldt0 @ X0))
% 18.26/3.20 | (aInteger0 @ X1))),
% 18.26/3.20 inference('eq_res', [status(thm)], [zip_derived_cl85])).
% 18.26/3.20 thf(zip_derived_cl5313, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ cS1395)
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | (aInteger0 @ X0))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl5295, zip_derived_cl5248])).
% 18.26/3.20 thf(zip_derived_cl148, plain, ( (aSet0 @ cS1395)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5334, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | (aInteger0 @ X0))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5313, zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl7434, plain,
% 18.26/3.20 (![X0 : $i]: (~ (aElementOf0 @ X0 @ xB) | (aInteger0 @ X0))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl7428, zip_derived_cl5334])).
% 18.26/3.20 thf(zip_derived_cl9015, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ xB)
% 18.26/3.20 | (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB)))),
% 18.26/3.20 inference('clc', [status(thm)], [zip_derived_cl8884, zip_derived_cl7434])).
% 18.26/3.20 thf(zip_derived_cl161, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | ~ (zip_tseitin_9 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_7])).
% 18.26/3.20 thf(zip_derived_cl9017, plain,
% 18.26/3.20 (![X0 : $i]: (~ (aElementOf0 @ X0 @ xB) | ~ (zip_tseitin_9 @ X0))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl9015, zip_derived_cl161])).
% 18.26/3.20 thf(zip_derived_cl9438, plain,
% 18.26/3.20 (( (aElementOf0 @ sk__19 @ xA) | ~ (zip_tseitin_9 @ sk__19))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl9426, zip_derived_cl9017])).
% 18.26/3.20 thf(zip_derived_cl8566, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | ~ (zip_tseitin_8 @ X0))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7669, zip_derived_cl8559])).
% 18.26/3.20 thf(zip_derived_cl155, plain,
% 18.26/3.20 (![X0 : $i]: ( (zip_tseitin_7 @ X0) | ~ (aElementOf0 @ X0 @ xA))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_11])).
% 18.26/3.20 thf(zip_derived_cl159, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (zip_tseitin_8 @ X0) | ~ (zip_tseitin_7 @ X0) | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_9])).
% 18.26/3.20 thf(zip_derived_cl4352, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ xA)
% 18.26/3.20 | ~ (aInteger0 @ X0)
% 18.26/3.20 | (zip_tseitin_8 @ X0))),
% 18.26/3.20 inference('dp-resolution', [status(thm)],
% 18.26/3.20 [zip_derived_cl155, zip_derived_cl159])).
% 18.26/3.20 thf(zip_derived_cl8883, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ xA)
% 18.26/3.20 | ~ (aInteger0 @ X0))),
% 18.26/3.20 inference('s_sup+', [status(thm)],
% 18.26/3.20 [zip_derived_cl8566, zip_derived_cl4352])).
% 18.26/3.20 thf(zip_derived_cl43, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ X0 @ X1) @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl145, plain,
% 18.26/3.20 (![X0 : $i]: ( (aElementOf0 @ X0 @ cS1395) | ~ (aElementOf0 @ X0 @ xA))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5040, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ xA @ X0)
% 18.26/3.20 | ~ (aSet0 @ xA)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ xA @ X0) @ cS1395))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl43, zip_derived_cl145])).
% 18.26/3.20 thf(zip_derived_cl136, plain, ( (aSet0 @ xA)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl5049, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ xA @ X0)
% 18.26/3.20 | (aElementOf0 @ (sk__2 @ xA @ X0) @ cS1395))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5040, zip_derived_cl136])).
% 18.26/3.20 thf(zip_derived_cl6525, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ (sk__2 @ X0 @ (stldt0 @ (stldt0 @ cS1395))) @ cS1395)
% 18.26/3.20 | ~ (aSet0 @ X0)
% 18.26/3.20 | (aSubsetOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl139, zip_derived_cl6205])).
% 18.26/3.20 thf(zip_derived_cl7343, plain,
% 18.26/3.20 (( (aSubsetOf0 @ xA @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | ~ (aSet0 @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | ~ (aSet0 @ xA)
% 18.26/3.20 | (aSubsetOf0 @ xA @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl5049, zip_derived_cl6525])).
% 18.26/3.20 thf(zip_derived_cl5333, plain, ( (aSet0 @ (stldt0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5312, zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl136, plain, ( (aSet0 @ xA)),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl7346, plain,
% 18.26/3.20 (( (aSubsetOf0 @ xA @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | (aSubsetOf0 @ xA @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7343, zip_derived_cl5333, zip_derived_cl136])).
% 18.26/3.20 thf(zip_derived_cl7347, plain,
% 18.26/3.20 ( (aSubsetOf0 @ xA @ (stldt0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('simplify', [status(thm)], [zip_derived_cl7346])).
% 18.26/3.20 thf(zip_derived_cl44, plain,
% 18.26/3.20 (![X0 : $i, X1 : $i, X2 : $i]:
% 18.26/3.20 (~ (aSubsetOf0 @ X0 @ X1)
% 18.26/3.20 | (aElementOf0 @ X2 @ X1)
% 18.26/3.20 | ~ (aElementOf0 @ X2 @ X0)
% 18.26/3.20 | ~ (aSet0 @ X1))),
% 18.26/3.20 inference('cnf', [status(esa)], [mSubset])).
% 18.26/3.20 thf(zip_derived_cl7348, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ xA)
% 18.26/3.20 | ~ (aSet0 @ (stldt0 @ (stldt0 @ cS1395))))),
% 18.26/3.20 inference('s_sup-', [status(thm)], [zip_derived_cl7347, zip_derived_cl44])).
% 18.26/3.20 thf(zip_derived_cl5333, plain, ( (aSet0 @ (stldt0 @ (stldt0 @ cS1395)))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5312, zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl7350, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | ~ (aElementOf0 @ X0 @ xA))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7348, zip_derived_cl5333])).
% 18.26/3.20 thf(zip_derived_cl5334, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (stldt0 @ (stldt0 @ cS1395)))
% 18.26/3.20 | (aInteger0 @ X0))),
% 18.26/3.20 inference('demod', [status(thm)], [zip_derived_cl5313, zip_derived_cl148])).
% 18.26/3.20 thf(zip_derived_cl7353, plain,
% 18.26/3.20 (![X0 : $i]: (~ (aElementOf0 @ X0 @ xA) | (aInteger0 @ X0))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl7350, zip_derived_cl5334])).
% 18.26/3.20 thf(zip_derived_cl8967, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ xA)
% 18.26/3.20 | (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB)))),
% 18.26/3.20 inference('clc', [status(thm)], [zip_derived_cl8883, zip_derived_cl7353])).
% 18.26/3.20 thf(zip_derived_cl161, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ (sdtbsmnsldt0 @ xA @ xB))
% 18.26/3.20 | ~ (zip_tseitin_9 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_7])).
% 18.26/3.20 thf(zip_derived_cl8969, plain,
% 18.26/3.20 (![X0 : $i]: (~ (aElementOf0 @ X0 @ xA) | ~ (zip_tseitin_9 @ X0))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8967, zip_derived_cl161])).
% 18.26/3.20 thf(zip_derived_cl9468, plain, (~ (zip_tseitin_9 @ sk__19)),
% 18.26/3.20 inference('clc', [status(thm)], [zip_derived_cl9438, zip_derived_cl8969])).
% 18.26/3.20 thf(zip_derived_cl9470, plain,
% 18.26/3.20 (~ (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8576, zip_derived_cl9468])).
% 18.26/3.20 thf(zip_derived_cl9484, plain, ( (aElementOf0 @ sk__19 @ (stldt0 @ xB))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8618, zip_derived_cl9470])).
% 18.26/3.20 thf(zip_derived_cl9533, plain, ( (aElementOf0 @ sk__19 @ xA)),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl9428, zip_derived_cl9484])).
% 18.26/3.20 thf(zip_derived_cl109, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 (~ (aElementOf0 @ X0 @ xA) | ~ (aElementOf0 @ X0 @ (stldt0 @ xA)))),
% 18.26/3.20 inference('cnf', [status(esa)], [m__1826])).
% 18.26/3.20 thf(zip_derived_cl9553, plain, (~ (aElementOf0 @ sk__19 @ (stldt0 @ xA))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl9533, zip_derived_cl109])).
% 18.26/3.20 thf(zip_derived_cl8572, plain,
% 18.26/3.20 (( (zip_tseitin_12 @ sk__19)
% 18.26/3.20 | (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl7675, zip_derived_cl8559])).
% 18.26/3.20 thf(zip_derived_cl170, plain,
% 18.26/3.20 (![X0 : $i]:
% 18.26/3.20 ( (aElementOf0 @ X0 @ (stldt0 @ xA)) | ~ (zip_tseitin_12 @ X0))),
% 18.26/3.20 inference('cnf', [status(esa)], [zf_stmt_1])).
% 18.26/3.20 thf(zip_derived_cl8617, plain,
% 18.26/3.20 (( (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))
% 18.26/3.20 | (aElementOf0 @ sk__19 @ (stldt0 @ xA)))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8572, zip_derived_cl170])).
% 18.26/3.20 thf(zip_derived_cl9470, plain,
% 18.26/3.20 (~ (aElementOf0 @ sk__19 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8576, zip_derived_cl9468])).
% 18.26/3.20 thf(zip_derived_cl9483, plain, ( (aElementOf0 @ sk__19 @ (stldt0 @ xA))),
% 18.26/3.20 inference('s_sup-', [status(thm)],
% 18.26/3.20 [zip_derived_cl8617, zip_derived_cl9470])).
% 18.26/3.20 thf(zip_derived_cl9567, plain, ($false),
% 18.26/3.20 inference('demod', [status(thm)],
% 18.26/3.20 [zip_derived_cl9553, zip_derived_cl9483])).
% 18.26/3.20
% 18.26/3.20 % SZS output end Refutation
% 18.26/3.20
% 18.26/3.20
% 18.26/3.20 % Terminating...
% 19.05/3.30 % Runner terminated.
% 19.05/3.32 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------