%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM437+5 : 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.MmFymTGgsJ true
% Computer : n014.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 118.89s 17.64s
% Output : Refutation 118.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : NUM437+5 : TPTP v9.2.0. Released v4.0.0.
% 0.11/0.15 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.MmFymTGgsJ true
% 0.13/0.36 % Computer : n014.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Wed Oct 1 16:41:38 EDT 2025
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Running portfolio for 300 s
% 0.13/0.36 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.36 % Number of cores: 8
% 0.13/0.37 % Python version: Python 3.6.8
% 0.13/0.37 % Running in FO mode
% 0.54/0.68 % Total configuration time : 435
% 0.54/0.68 % Estimated wc time : 1092
% 0.54/0.68 % Estimated cpu time (7 cpus) : 156.0
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.56/0.77 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.56/0.77 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.56/0.78 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.56/0.78 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.56/0.80 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 118.89/17.64 % Solved by fo/fo7.sh.
% 118.89/17.64 % done 10294 iterations in 16.842s
% 118.89/17.64 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 118.89/17.64 % SZS output start Refutation
% 118.89/17.64 thf(smndt0_type, type, smndt0: $i > $i).
% 118.89/17.64 thf(isOpen0_type, type, isOpen0: $i > $o).
% 118.89/17.64 thf(sk__15_type, type, sk__15: $i).
% 118.89/17.64 thf(sdtasdt0_type, type, sdtasdt0: $i > $i > $i).
% 118.89/17.64 thf(aInteger0_type, type, aInteger0: $i > $o).
% 118.89/17.64 thf(sk__12_type, type, sk__12: $i > $i > $i).
% 118.89/17.64 thf(sdtbsmnsldt0_type, type, sdtbsmnsldt0: $i > $i > $i).
% 118.89/17.64 thf(sk__14_type, type, sk__14: $i > $i).
% 118.89/17.64 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $i > $o).
% 118.89/17.64 thf(cS1395_type, type, cS1395: $i).
% 118.89/17.64 thf(sz00_type, type, sz00: $i).
% 118.89/17.64 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 118.89/17.64 thf(sbsmnsldt0_type, type, sbsmnsldt0: $i > $i).
% 118.89/17.64 thf(szAzrzSzezqlpdtcmdtrp0_type, type, szAzrzSzezqlpdtcmdtrp0: $i > $i > $i).
% 118.89/17.64 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $i > $o).
% 118.89/17.64 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 118.89/17.64 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 118.89/17.64 thf(xS_type, type, xS: $i).
% 118.89/17.64 thf(aDivisorOf0_type, type, aDivisorOf0: $i > $i > $o).
% 118.89/17.64 thf(sdteqdtlpzmzozddtrp0_type, type, sdteqdtlpzmzozddtrp0: $i > $i > $i > $o).
% 118.89/17.64 thf(sk__16_type, type, sk__16: $i > $i).
% 118.89/17.64 thf(zip_tseitin_8_type, type, zip_tseitin_8: $i > $o).
% 118.89/17.64 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $i > $o).
% 118.89/17.64 thf(aSet0_type, type, aSet0: $i > $o).
% 118.89/17.64 thf(sdtslmnbsdt0_type, type, sdtslmnbsdt0: $i > $i > $i).
% 118.89/17.64 thf(m__, conjecture,
% 118.89/17.64 (( ( ![W0:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) <=>
% 118.89/17.64 ( ( ?[W1:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W1 @ xS ) & ( aElementOf0 @ W0 @ W1 ) ) ) &
% 118.89/17.64 ( aInteger0 @ W0 ) ) ) ) &
% 118.89/17.64 ( aSet0 @ ( sbsmnsldt0 @ xS ) ) ) =>
% 118.89/17.64 ( ( isOpen0 @ ( sbsmnsldt0 @ xS ) ) |
% 118.89/17.64 ( ![W0:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) =>
% 118.89/17.64 ( ?[W1:$i]:
% 118.89/17.64 ( ( aInteger0 @ W1 ) & ( ( W1 ) != ( sz00 ) ) &
% 118.89/17.64 ( ( ( ![W2:$i]:
% 118.89/17.64 ( ( ( aElementOf0 @
% 118.89/17.64 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 118.89/17.64 ( ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) &
% 118.89/17.64 ( aDivisorOf0 @
% 118.89/17.64 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 118.89/17.64 ( ?[W3:$i]:
% 118.89/17.64 ( ( aInteger0 @ W3 ) &
% 118.89/17.64 ( ( sdtasdt0 @ W1 @ W3 ) =
% 118.89/17.64 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) ) ) &
% 118.89/17.64 ( aInteger0 @ W2 ) ) ) &
% 118.89/17.64 ( ( ( ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) |
% 118.89/17.64 ( aDivisorOf0 @
% 118.89/17.64 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 118.89/17.64 ( ?[W3:$i]:
% 118.89/17.64 ( ( aInteger0 @ W3 ) &
% 118.89/17.64 ( ( sdtasdt0 @ W1 @ W3 ) =
% 118.89/17.64 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) ) ) ) &
% 118.89/17.64 ( aInteger0 @ W2 ) ) =>
% 118.89/17.64 ( aElementOf0 @
% 118.89/17.64 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) ) ) &
% 118.89/17.64 ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) =>
% 118.89/17.64 ( ( aSubsetOf0 @
% 118.89/17.64 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @ ( sbsmnsldt0 @ xS ) ) |
% 118.89/17.64 ( ![W2:$i]:
% 118.89/17.64 ( ( aElementOf0 @
% 118.89/17.64 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 118.89/17.64 ( aElementOf0 @ W2 @ ( sbsmnsldt0 @ xS ) ) ) ) ) ) ) ) ) ) ))).
% 118.89/17.64 thf(zf_stmt_0, type, zip_tseitin_8 : $i > $o).
% 118.89/17.64 thf(zf_stmt_1, axiom,
% 118.89/17.64 (![W0:$i]:
% 118.89/17.64 ( ( zip_tseitin_8 @ W0 ) <=>
% 118.89/17.64 ( ( aInteger0 @ W0 ) & ( ?[W1:$i]: ( zip_tseitin_7 @ W1 @ W0 ) ) ) ))).
% 118.89/17.64 thf(zf_stmt_2, type, zip_tseitin_7 : $i > $i > $o).
% 118.89/17.64 thf(zf_stmt_3, axiom,
% 118.89/17.64 (![W1:$i,W0:$i]:
% 118.89/17.64 ( ( zip_tseitin_7 @ W1 @ W0 ) <=>
% 118.89/17.64 ( ( aElementOf0 @ W0 @ W1 ) & ( aElementOf0 @ W1 @ xS ) ) ))).
% 118.89/17.64 thf(zf_stmt_4, conjecture,
% 118.89/17.64 (( ( aSet0 @ ( sbsmnsldt0 @ xS ) ) &
% 118.89/17.64 ( ![W0:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) <=>
% 118.89/17.64 ( zip_tseitin_8 @ W0 ) ) ) ) =>
% 118.89/17.64 ( ( ![W0:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) =>
% 118.89/17.64 ( ?[W1:$i]:
% 118.89/17.64 ( ( ( ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) &
% 118.89/17.64 ( ![W2:$i]:
% 118.89/17.64 ( ( ( ( aInteger0 @ W2 ) &
% 118.89/17.64 ( ( ?[W3:$i]:
% 118.89/17.64 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 118.89/17.64 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 118.89/17.64 ( aInteger0 @ W3 ) ) ) |
% 118.89/17.64 ( aDivisorOf0 @
% 118.89/17.64 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 118.89/17.64 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) =>
% 118.89/17.64 ( aElementOf0 @
% 118.89/17.64 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) &
% 118.89/17.64 ( ( aElementOf0 @
% 118.89/17.64 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 118.89/17.64 ( ( aInteger0 @ W2 ) &
% 118.89/17.64 ( ?[W3:$i]:
% 118.89/17.64 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 118.89/17.64 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 118.89/17.64 ( aInteger0 @ W3 ) ) ) &
% 118.89/17.64 ( aDivisorOf0 @
% 118.89/17.64 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 118.89/17.64 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) ) ) ) =>
% 118.89/17.64 ( ( ![W2:$i]:
% 118.89/17.64 ( ( aElementOf0 @
% 118.89/17.64 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 118.89/17.64 ( aElementOf0 @ W2 @ ( sbsmnsldt0 @ xS ) ) ) ) |
% 118.89/17.64 ( aSubsetOf0 @
% 118.89/17.64 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @ ( sbsmnsldt0 @ xS ) ) ) ) &
% 118.89/17.64 ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) |
% 118.89/17.64 ( isOpen0 @ ( sbsmnsldt0 @ xS ) ) ))).
% 118.89/17.64 thf(zf_stmt_5, negated_conjecture,
% 118.89/17.64 (~( ( ( aSet0 @ ( sbsmnsldt0 @ xS ) ) &
% 118.89/17.64 ( ![W0:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) <=>
% 118.89/17.64 ( zip_tseitin_8 @ W0 ) ) ) ) =>
% 118.89/17.64 ( ( ![W0:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) =>
% 118.89/17.64 ( ?[W1:$i]:
% 118.89/17.64 ( ( ( ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) &
% 118.89/17.64 ( ![W2:$i]:
% 118.89/17.64 ( ( ( ( aInteger0 @ W2 ) &
% 118.89/17.64 ( ( ?[W3:$i]:
% 118.89/17.64 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 118.89/17.64 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 118.89/17.64 ( aInteger0 @ W3 ) ) ) |
% 118.89/17.64 ( aDivisorOf0 @
% 118.89/17.64 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 118.89/17.64 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) =>
% 118.89/17.64 ( aElementOf0 @
% 118.89/17.64 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) &
% 118.89/17.64 ( ( aElementOf0 @
% 118.89/17.64 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 118.89/17.64 ( ( aInteger0 @ W2 ) &
% 118.89/17.64 ( ?[W3:$i]:
% 118.89/17.64 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 118.89/17.64 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 118.89/17.64 ( aInteger0 @ W3 ) ) ) &
% 118.89/17.64 ( aDivisorOf0 @
% 118.89/17.64 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 118.89/17.64 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) ) ) ) =>
% 118.89/17.64 ( ( ![W2:$i]:
% 118.89/17.64 ( ( aElementOf0 @
% 118.89/17.64 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 118.89/17.64 ( aElementOf0 @ W2 @ ( sbsmnsldt0 @ xS ) ) ) ) |
% 118.89/17.64 ( aSubsetOf0 @
% 118.89/17.64 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @
% 118.89/17.64 ( sbsmnsldt0 @ xS ) ) ) ) &
% 118.89/17.64 ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) |
% 118.89/17.64 ( isOpen0 @ ( sbsmnsldt0 @ xS ) ) ) )),
% 118.89/17.64 inference('cnf.neg', [status(esa)], [zf_stmt_4])).
% 118.89/17.64 thf(zip_derived_cl133, plain,
% 118.89/17.64 (![X2 : $i]:
% 118.89/17.64 ( (aElementOf0 @ (sk__16 @ X2) @
% 118.89/17.64 (szAzrzSzezqlpdtcmdtrp0 @ sk__15 @ X2))
% 118.89/17.64 | ((X2) = (sz00))
% 118.89/17.64 | ~ (aInteger0 @ X2))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_5])).
% 118.89/17.64 thf(zip_derived_cl127, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 ( (zip_tseitin_7 @ (sk__14 @ X0) @ X0) | ~ (zip_tseitin_8 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_1])).
% 118.89/17.64 thf(zip_derived_cl123, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 ( (aElementOf0 @ X0 @ X1) | ~ (zip_tseitin_7 @ X1 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_3])).
% 118.89/17.64 thf(zip_derived_cl127, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 ( (zip_tseitin_7 @ (sk__14 @ X0) @ X0) | ~ (zip_tseitin_8 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_1])).
% 118.89/17.64 thf(zip_derived_cl123, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 ( (aElementOf0 @ X0 @ X1) | ~ (zip_tseitin_7 @ X1 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_3])).
% 118.89/17.64 thf(zip_derived_cl127, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 ( (zip_tseitin_7 @ (sk__14 @ X0) @ X0) | ~ (zip_tseitin_8 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_1])).
% 118.89/17.64 thf(zip_derived_cl124, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 ( (aElementOf0 @ X0 @ xS) | ~ (zip_tseitin_7 @ X0 @ X1))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_3])).
% 118.89/17.64 thf(zip_derived_cl216, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (zip_tseitin_8 @ X0) | (aElementOf0 @ (sk__14 @ X0) @ xS))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl127, zip_derived_cl124])).
% 118.89/17.64 thf(m__1750, axiom,
% 118.89/17.64 (( ![W0:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W0 @ xS ) =>
% 118.89/17.64 ( ( aSet0 @ cS1395 ) &
% 118.89/17.64 ( ![W1:$i]: ( ( aElementOf0 @ W1 @ cS1395 ) <=> ( aInteger0 @ W1 ) ) ) &
% 118.89/17.64 ( aSet0 @ W0 ) &
% 118.89/17.64 ( ![W1:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W1 @ W0 ) => ( aElementOf0 @ W1 @ cS1395 ) ) ) &
% 118.89/17.64 ( aSubsetOf0 @ W0 @ cS1395 ) &
% 118.89/17.64 ( ![W1:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W1 @ W0 ) =>
% 118.89/17.64 ( ?[W2:$i]:
% 118.89/17.64 ( ( aSubsetOf0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W1 @ W2 ) @ W0 ) &
% 118.89/17.64 ( ![W3:$i]:
% 118.89/17.64 ( ( aElementOf0 @
% 118.89/17.64 W3 @ ( szAzrzSzezqlpdtcmdtrp0 @ W1 @ W2 ) ) =>
% 118.89/17.64 ( aElementOf0 @ W3 @ W0 ) ) ) &
% 118.89/17.64 ( ![W3:$i]:
% 118.89/17.64 ( ( ( ( aInteger0 @ W3 ) &
% 118.89/17.64 ( ( ?[W4:$i]:
% 118.89/17.64 ( ( ( sdtasdt0 @ W2 @ W4 ) =
% 118.89/17.64 ( sdtpldt0 @ W3 @ ( smndt0 @ W1 ) ) ) &
% 118.89/17.64 ( aInteger0 @ W4 ) ) ) |
% 118.89/17.64 ( aDivisorOf0 @
% 118.89/17.64 W2 @ ( sdtpldt0 @ W3 @ ( smndt0 @ W1 ) ) ) |
% 118.89/17.64 ( sdteqdtlpzmzozddtrp0 @ W3 @ W1 @ W2 ) ) ) =>
% 118.89/17.64 ( aElementOf0 @
% 118.89/17.64 W3 @ ( szAzrzSzezqlpdtcmdtrp0 @ W1 @ W2 ) ) ) &
% 118.89/17.64 ( ( aElementOf0 @
% 118.89/17.64 W3 @ ( szAzrzSzezqlpdtcmdtrp0 @ W1 @ W2 ) ) =>
% 118.89/17.64 ( ( aInteger0 @ W3 ) &
% 118.89/17.64 ( ?[W4:$i]:
% 118.89/17.64 ( ( ( sdtasdt0 @ W2 @ W4 ) =
% 118.89/17.64 ( sdtpldt0 @ W3 @ ( smndt0 @ W1 ) ) ) &
% 118.89/17.64 ( aInteger0 @ W4 ) ) ) &
% 118.89/17.64 ( aDivisorOf0 @
% 118.89/17.64 W2 @ ( sdtpldt0 @ W3 @ ( smndt0 @ W1 ) ) ) &
% 118.89/17.64 ( sdteqdtlpzmzozddtrp0 @ W3 @ W1 @ W2 ) ) ) ) ) &
% 118.89/17.64 ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W1 @ W2 ) ) &
% 118.89/17.64 ( ( W2 ) != ( sz00 ) ) & ( aInteger0 @ W2 ) ) ) ) ) &
% 118.89/17.64 ( isOpen0 @ W0 ) ) ) ) &
% 118.89/17.64 ( aSet0 @ xS ))).
% 118.89/17.64 thf(zip_derived_cl107, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ X0 @ X1)
% 118.89/17.64 | (aElementOf0 @ X0 @ cS1395)
% 118.89/17.64 | ~ (aElementOf0 @ X1 @ xS))),
% 118.89/17.64 inference('cnf', [status(esa)], [m__1750])).
% 118.89/17.64 thf(zip_derived_cl233, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 (~ (zip_tseitin_8 @ X0)
% 118.89/17.64 | (aElementOf0 @ X1 @ cS1395)
% 118.89/17.64 | ~ (aElementOf0 @ X1 @ (sk__14 @ X0)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl216, zip_derived_cl107])).
% 118.89/17.64 thf(zip_derived_cl359, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 (~ (zip_tseitin_7 @ (sk__14 @ X0) @ X1)
% 118.89/17.64 | (aElementOf0 @ X1 @ cS1395)
% 118.89/17.64 | ~ (zip_tseitin_8 @ X0))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl123, zip_derived_cl233])).
% 118.89/17.64 thf(zip_derived_cl362, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (zip_tseitin_8 @ X0)
% 118.89/17.64 | ~ (zip_tseitin_8 @ X0)
% 118.89/17.64 | (aElementOf0 @ X0 @ cS1395))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl127, zip_derived_cl359])).
% 118.89/17.64 thf(zip_derived_cl363, plain,
% 118.89/17.64 (![X0 : $i]: ( (aElementOf0 @ X0 @ cS1395) | ~ (zip_tseitin_8 @ X0))),
% 118.89/17.64 inference('simplify', [status(thm)], [zip_derived_cl362])).
% 118.89/17.64 thf(zip_derived_cl144, plain, ( (aElementOf0 @ sk__15 @ (sbsmnsldt0 @ xS))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_5])).
% 118.89/17.64 thf(mIntersection, axiom,
% 118.89/17.64 (![W0:$i,W1:$i]:
% 118.89/17.64 ( ( ( aSubsetOf0 @ W1 @ cS1395 ) & ( aSubsetOf0 @ W0 @ cS1395 ) ) =>
% 118.89/17.64 ( ![W2:$i]:
% 118.89/17.64 ( ( ( W2 ) = ( sdtslmnbsdt0 @ W0 @ W1 ) ) <=>
% 118.89/17.64 ( ( ![W3:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W3 @ W2 ) <=>
% 118.89/17.64 ( ( aElementOf0 @ W3 @ W1 ) & ( aElementOf0 @ W3 @ W0 ) &
% 118.89/17.64 ( aInteger0 @ W3 ) ) ) ) &
% 118.89/17.64 ( aSet0 @ W2 ) ) ) ) ))).
% 118.89/17.64 thf(zf_stmt_6, axiom,
% 118.89/17.64 (![W3:$i,W1:$i,W0:$i]:
% 118.89/17.64 ( ( zip_tseitin_1 @ W3 @ W1 @ W0 ) <=>
% 118.89/17.64 ( ( aInteger0 @ W3 ) & ( aElementOf0 @ W3 @ W0 ) &
% 118.89/17.64 ( aElementOf0 @ W3 @ W1 ) ) ))).
% 118.89/17.64 thf(zip_derived_cl59, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i, X2 : $i]:
% 118.89/17.64 ( (zip_tseitin_1 @ X0 @ X1 @ X2)
% 118.89/17.64 | ~ (aElementOf0 @ X0 @ X1)
% 118.89/17.64 | ~ (aElementOf0 @ X0 @ X2)
% 118.89/17.64 | ~ (aInteger0 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_6])).
% 118.89/17.64 thf(zip_derived_cl423, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (aInteger0 @ sk__15)
% 118.89/17.64 | ~ (aElementOf0 @ sk__15 @ X0)
% 118.89/17.64 | (zip_tseitin_1 @ sk__15 @ (sbsmnsldt0 @ xS) @ X0))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl144, zip_derived_cl59])).
% 118.89/17.64 thf(zip_derived_cl126, plain,
% 118.89/17.64 (![X0 : $i]: ( (aInteger0 @ X0) | ~ (zip_tseitin_8 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_1])).
% 118.89/17.64 thf(zip_derived_cl144, plain, ( (aElementOf0 @ sk__15 @ (sbsmnsldt0 @ xS))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_5])).
% 118.89/17.64 thf(mUnion, axiom,
% 118.89/17.64 (![W0:$i,W1:$i]:
% 118.89/17.64 ( ( ( aSubsetOf0 @ W1 @ cS1395 ) & ( aSubsetOf0 @ W0 @ cS1395 ) ) =>
% 118.89/17.64 ( ![W2:$i]:
% 118.89/17.64 ( ( ( W2 ) = ( sdtbsmnsldt0 @ W0 @ W1 ) ) <=>
% 118.89/17.64 ( ( ![W3:$i]:
% 118.89/17.64 ( ( aElementOf0 @ W3 @ W2 ) <=>
% 118.89/17.64 ( ( ( aElementOf0 @ W3 @ W1 ) | ( aElementOf0 @ W3 @ W0 ) ) &
% 118.89/17.64 ( aInteger0 @ W3 ) ) ) ) &
% 118.89/17.64 ( aSet0 @ W2 ) ) ) ) ))).
% 118.89/17.64 thf(zf_stmt_7, axiom,
% 118.89/17.64 (![W3:$i,W1:$i,W0:$i]:
% 118.89/17.64 ( ( zip_tseitin_0 @ W3 @ W1 @ W0 ) <=>
% 118.89/17.64 ( ( aInteger0 @ W3 ) &
% 118.89/17.64 ( ( aElementOf0 @ W3 @ W0 ) | ( aElementOf0 @ W3 @ W1 ) ) ) ))).
% 118.89/17.64 thf(zip_derived_cl49, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i, X2 : $i]:
% 118.89/17.64 ( (zip_tseitin_0 @ X0 @ X1 @ X2)
% 118.89/17.64 | ~ (aElementOf0 @ X0 @ X1)
% 118.89/17.64 | ~ (aInteger0 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_7])).
% 118.89/17.64 thf(zip_derived_cl178, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (aInteger0 @ sk__15)
% 118.89/17.64 | (zip_tseitin_0 @ sk__15 @ (sbsmnsldt0 @ xS) @ X0))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl144, zip_derived_cl49])).
% 118.89/17.64 thf(zip_derived_cl188, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (zip_tseitin_8 @ sk__15)
% 118.89/17.64 | (zip_tseitin_0 @ sk__15 @ (sbsmnsldt0 @ xS) @ X0))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl126, zip_derived_cl178])).
% 118.89/17.64 thf(zip_derived_cl144, plain, ( (aElementOf0 @ sk__15 @ (sbsmnsldt0 @ xS))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_5])).
% 118.89/17.64 thf(zip_derived_cl131, plain,
% 118.89/17.64 (![X1 : $i]:
% 118.89/17.64 ( (zip_tseitin_8 @ X1) | ~ (aElementOf0 @ X1 @ (sbsmnsldt0 @ xS)))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_5])).
% 118.89/17.64 thf(zip_derived_cl151, plain, ( (zip_tseitin_8 @ sk__15)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl144, zip_derived_cl131])).
% 118.89/17.64 thf(zip_derived_cl189, plain,
% 118.89/17.64 (![X0 : $i]: (zip_tseitin_0 @ sk__15 @ (sbsmnsldt0 @ xS) @ X0)),
% 118.89/17.64 inference('demod', [status(thm)], [zip_derived_cl188, zip_derived_cl151])).
% 118.89/17.64 thf(zip_derived_cl47, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i, X2 : $i]:
% 118.89/17.64 ( (aInteger0 @ X0) | ~ (zip_tseitin_0 @ X0 @ X1 @ X2))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_7])).
% 118.89/17.64 thf(zip_derived_cl190, plain, ( (aInteger0 @ sk__15)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl189, zip_derived_cl47])).
% 118.89/17.64 thf(zip_derived_cl426, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ sk__15 @ X0)
% 118.89/17.64 | (zip_tseitin_1 @ sk__15 @ (sbsmnsldt0 @ xS) @ X0))),
% 118.89/17.64 inference('demod', [status(thm)], [zip_derived_cl423, zip_derived_cl190])).
% 118.89/17.64 thf(zip_derived_cl445, plain,
% 118.89/17.64 ((~ (zip_tseitin_8 @ sk__15)
% 118.89/17.64 | (zip_tseitin_1 @ sk__15 @ (sbsmnsldt0 @ xS) @ cS1395))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl363, zip_derived_cl426])).
% 118.89/17.64 thf(zip_derived_cl151, plain, ( (zip_tseitin_8 @ sk__15)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl144, zip_derived_cl131])).
% 118.89/17.64 thf(zip_derived_cl449, plain,
% 118.89/17.64 ( (zip_tseitin_1 @ sk__15 @ (sbsmnsldt0 @ xS) @ cS1395)),
% 118.89/17.64 inference('demod', [status(thm)], [zip_derived_cl445, zip_derived_cl151])).
% 118.89/17.64 thf(zip_derived_cl57, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i, X2 : $i]:
% 118.89/17.64 ( (aElementOf0 @ X0 @ X1) | ~ (zip_tseitin_1 @ X0 @ X2 @ X1))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_6])).
% 118.89/17.64 thf(zip_derived_cl454, plain, ( (aElementOf0 @ sk__15 @ cS1395)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl449, zip_derived_cl57])).
% 118.89/17.64 thf(zip_derived_cl59, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i, X2 : $i]:
% 118.89/17.64 ( (zip_tseitin_1 @ X0 @ X1 @ X2)
% 118.89/17.64 | ~ (aElementOf0 @ X0 @ X1)
% 118.89/17.64 | ~ (aElementOf0 @ X0 @ X2)
% 118.89/17.64 | ~ (aInteger0 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_6])).
% 118.89/17.64 thf(zip_derived_cl456, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (aInteger0 @ sk__15)
% 118.89/17.64 | ~ (aElementOf0 @ sk__15 @ X0)
% 118.89/17.64 | (zip_tseitin_1 @ sk__15 @ cS1395 @ X0))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl454, zip_derived_cl59])).
% 118.89/17.64 thf(zip_derived_cl190, plain, ( (aInteger0 @ sk__15)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl189, zip_derived_cl47])).
% 118.89/17.64 thf(zip_derived_cl464, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ sk__15 @ X0)
% 118.89/17.64 | (zip_tseitin_1 @ sk__15 @ cS1395 @ X0))),
% 118.89/17.64 inference('demod', [status(thm)], [zip_derived_cl456, zip_derived_cl190])).
% 118.89/17.64 thf(zip_derived_cl474, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (zip_tseitin_7 @ X0 @ sk__15)
% 118.89/17.64 | (zip_tseitin_1 @ sk__15 @ cS1395 @ X0))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl123, zip_derived_cl464])).
% 118.89/17.64 thf(zip_derived_cl483, plain,
% 118.89/17.64 ((~ (zip_tseitin_8 @ sk__15)
% 118.89/17.64 | (zip_tseitin_1 @ sk__15 @ cS1395 @ (sk__14 @ sk__15)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl127, zip_derived_cl474])).
% 118.89/17.64 thf(zip_derived_cl151, plain, ( (zip_tseitin_8 @ sk__15)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl144, zip_derived_cl131])).
% 118.89/17.64 thf(zip_derived_cl484, plain,
% 118.89/17.64 ( (zip_tseitin_1 @ sk__15 @ cS1395 @ (sk__14 @ sk__15))),
% 118.89/17.64 inference('demod', [status(thm)], [zip_derived_cl483, zip_derived_cl151])).
% 118.89/17.64 thf(zip_derived_cl57, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i, X2 : $i]:
% 118.89/17.64 ( (aElementOf0 @ X0 @ X1) | ~ (zip_tseitin_1 @ X0 @ X2 @ X1))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_6])).
% 118.89/17.64 thf(zip_derived_cl537, plain, ( (aElementOf0 @ sk__15 @ (sk__14 @ sk__15))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl484, zip_derived_cl57])).
% 118.89/17.64 thf(zip_derived_cl537, plain, ( (aElementOf0 @ sk__15 @ (sk__14 @ sk__15))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl484, zip_derived_cl57])).
% 118.89/17.64 thf(zip_derived_cl216, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (zip_tseitin_8 @ X0) | (aElementOf0 @ (sk__14 @ X0) @ xS))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl127, zip_derived_cl124])).
% 118.89/17.64 thf(zip_derived_cl125, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 ( (zip_tseitin_7 @ X0 @ X1)
% 118.89/17.64 | ~ (aElementOf0 @ X0 @ xS)
% 118.89/17.64 | ~ (aElementOf0 @ X1 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_3])).
% 118.89/17.64 thf(zip_derived_cl227, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 (~ (zip_tseitin_8 @ X0)
% 118.89/17.64 | ~ (aElementOf0 @ X1 @ (sk__14 @ X0))
% 118.89/17.64 | (zip_tseitin_7 @ (sk__14 @ X0) @ X1))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl216, zip_derived_cl125])).
% 118.89/17.64 thf(zip_derived_cl546, plain,
% 118.89/17.64 (( (zip_tseitin_7 @ (sk__14 @ sk__15) @ sk__15)
% 118.89/17.64 | ~ (zip_tseitin_8 @ sk__15))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl537, zip_derived_cl227])).
% 118.89/17.64 thf(zip_derived_cl151, plain, ( (zip_tseitin_8 @ sk__15)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl144, zip_derived_cl131])).
% 118.89/17.64 thf(zip_derived_cl557, plain,
% 118.89/17.64 ( (zip_tseitin_7 @ (sk__14 @ sk__15) @ sk__15)),
% 118.89/17.64 inference('demod', [status(thm)], [zip_derived_cl546, zip_derived_cl151])).
% 118.89/17.64 thf(zip_derived_cl124, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 ( (aElementOf0 @ X0 @ xS) | ~ (zip_tseitin_7 @ X0 @ X1))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_3])).
% 118.89/17.64 thf(zip_derived_cl566, plain, ( (aElementOf0 @ (sk__14 @ sk__15) @ xS)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl557, zip_derived_cl124])).
% 118.89/17.64 thf(zip_derived_cl120, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i, X2 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ X0 @ X1)
% 118.89/17.64 | (aElementOf0 @ X2 @ X1)
% 118.89/17.64 | ~ (aElementOf0 @ X2 @
% 118.89/17.64 (szAzrzSzezqlpdtcmdtrp0 @ X0 @ (sk__12 @ X0 @ X1)))
% 118.89/17.64 | ~ (aElementOf0 @ X1 @ xS))),
% 118.89/17.64 inference('cnf', [status(esa)], [m__1750])).
% 118.89/17.64 thf(zip_derived_cl1412, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ X1 @
% 118.89/17.64 (szAzrzSzezqlpdtcmdtrp0 @ X0 @ (sk__12 @ X0 @ (sk__14 @ sk__15))))
% 118.89/17.64 | (aElementOf0 @ X1 @ (sk__14 @ sk__15))
% 118.89/17.64 | ~ (aElementOf0 @ X0 @ (sk__14 @ sk__15)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl566, zip_derived_cl120])).
% 118.89/17.64 thf(zip_derived_cl4128, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 ( (aElementOf0 @ X0 @ (sk__14 @ sk__15))
% 118.89/17.64 | ~ (aElementOf0 @ X0 @
% 118.89/17.64 (szAzrzSzezqlpdtcmdtrp0 @ sk__15 @
% 118.89/17.64 (sk__12 @ sk__15 @ (sk__14 @ sk__15)))))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl537, zip_derived_cl1412])).
% 118.89/17.64 thf(zip_derived_cl103880, plain,
% 118.89/17.64 ((~ (aInteger0 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15)))
% 118.89/17.64 | ((sk__12 @ sk__15 @ (sk__14 @ sk__15)) = (sz00))
% 118.89/17.64 | (aElementOf0 @ (sk__16 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15))) @
% 118.89/17.64 (sk__14 @ sk__15)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl133, zip_derived_cl4128])).
% 118.89/17.64 thf(zip_derived_cl537, plain, ( (aElementOf0 @ sk__15 @ (sk__14 @ sk__15))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl484, zip_derived_cl57])).
% 118.89/17.64 thf(zip_derived_cl566, plain, ( (aElementOf0 @ (sk__14 @ sk__15) @ xS)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl557, zip_derived_cl124])).
% 118.89/17.64 thf(zip_derived_cl109, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ X0 @ X1)
% 118.89/17.64 | (aInteger0 @ (sk__12 @ X0 @ X1))
% 118.89/17.64 | ~ (aElementOf0 @ X1 @ xS))),
% 118.89/17.64 inference('cnf', [status(esa)], [m__1750])).
% 118.89/17.64 thf(zip_derived_cl656, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 ( (aInteger0 @ (sk__12 @ X0 @ (sk__14 @ sk__15)))
% 118.89/17.64 | ~ (aElementOf0 @ X0 @ (sk__14 @ sk__15)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl566, zip_derived_cl109])).
% 118.89/17.64 thf(zip_derived_cl1673, plain,
% 118.89/17.64 ( (aInteger0 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl537, zip_derived_cl656])).
% 118.89/17.64 thf(zip_derived_cl103905, plain,
% 118.89/17.64 ((((sk__12 @ sk__15 @ (sk__14 @ sk__15)) = (sz00))
% 118.89/17.64 | (aElementOf0 @ (sk__16 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15))) @
% 118.89/17.64 (sk__14 @ sk__15)))),
% 118.89/17.64 inference('demod', [status(thm)],
% 118.89/17.64 [zip_derived_cl103880, zip_derived_cl1673])).
% 118.89/17.64 thf(zip_derived_cl537, plain, ( (aElementOf0 @ sk__15 @ (sk__14 @ sk__15))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl484, zip_derived_cl57])).
% 118.89/17.64 thf(zip_derived_cl216, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (zip_tseitin_8 @ X0) | (aElementOf0 @ (sk__14 @ X0) @ xS))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl127, zip_derived_cl124])).
% 118.89/17.64 thf(zip_derived_cl110, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ X0 @ X1)
% 118.89/17.64 | ((sk__12 @ X0 @ X1) != (sz00))
% 118.89/17.64 | ~ (aElementOf0 @ X1 @ xS))),
% 118.89/17.64 inference('cnf', [status(esa)], [m__1750])).
% 118.89/17.64 thf(zip_derived_cl229, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 (~ (zip_tseitin_8 @ X0)
% 118.89/17.64 | ((sk__12 @ X1 @ (sk__14 @ X0)) != (sz00))
% 118.89/17.64 | ~ (aElementOf0 @ X1 @ (sk__14 @ X0)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl216, zip_derived_cl110])).
% 118.89/17.64 thf(zip_derived_cl547, plain,
% 118.89/17.64 ((((sk__12 @ sk__15 @ (sk__14 @ sk__15)) != (sz00))
% 118.89/17.64 | ~ (zip_tseitin_8 @ sk__15))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl537, zip_derived_cl229])).
% 118.89/17.64 thf(zip_derived_cl151, plain, ( (zip_tseitin_8 @ sk__15)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl144, zip_derived_cl131])).
% 118.89/17.64 thf(zip_derived_cl558, plain,
% 118.89/17.64 (((sk__12 @ sk__15 @ (sk__14 @ sk__15)) != (sz00))),
% 118.89/17.64 inference('demod', [status(thm)], [zip_derived_cl547, zip_derived_cl151])).
% 118.89/17.64 thf(zip_derived_cl103906, plain,
% 118.89/17.64 ( (aElementOf0 @ (sk__16 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15))) @
% 118.89/17.64 (sk__14 @ sk__15))),
% 118.89/17.64 inference('simplify_reflect-', [status(thm)],
% 118.89/17.64 [zip_derived_cl103905, zip_derived_cl558])).
% 118.89/17.64 thf(zip_derived_cl566, plain, ( (aElementOf0 @ (sk__14 @ sk__15) @ xS)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl557, zip_derived_cl124])).
% 118.89/17.64 thf(zip_derived_cl125, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 ( (zip_tseitin_7 @ X0 @ X1)
% 118.89/17.64 | ~ (aElementOf0 @ X0 @ xS)
% 118.89/17.64 | ~ (aElementOf0 @ X1 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_3])).
% 118.89/17.64 thf(zip_derived_cl653, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ X0 @ (sk__14 @ sk__15))
% 118.89/17.64 | (zip_tseitin_7 @ (sk__14 @ sk__15) @ X0))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl566, zip_derived_cl125])).
% 118.89/17.64 thf(zip_derived_cl110425, plain,
% 118.89/17.64 ( (zip_tseitin_7 @ (sk__14 @ sk__15) @
% 118.89/17.64 (sk__16 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15))))),
% 118.89/17.64 inference('sup-', [status(thm)],
% 118.89/17.64 [zip_derived_cl103906, zip_derived_cl653])).
% 118.89/17.64 thf(zip_derived_cl128, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 ( (zip_tseitin_8 @ X0)
% 118.89/17.64 | ~ (zip_tseitin_7 @ X1 @ X0)
% 118.89/17.64 | ~ (aInteger0 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_1])).
% 118.89/17.64 thf(zip_derived_cl126228, plain,
% 118.89/17.64 ((~ (aInteger0 @ (sk__16 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15))))
% 118.89/17.64 | (zip_tseitin_8 @ (sk__16 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15)))))),
% 118.89/17.64 inference('sup-', [status(thm)],
% 118.89/17.64 [zip_derived_cl110425, zip_derived_cl128])).
% 118.89/17.64 thf(zip_derived_cl133, plain,
% 118.89/17.64 (![X2 : $i]:
% 118.89/17.64 ( (aElementOf0 @ (sk__16 @ X2) @
% 118.89/17.64 (szAzrzSzezqlpdtcmdtrp0 @ sk__15 @ X2))
% 118.89/17.64 | ((X2) = (sz00))
% 118.89/17.64 | ~ (aInteger0 @ X2))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_5])).
% 118.89/17.64 thf(zip_derived_cl537, plain, ( (aElementOf0 @ sk__15 @ (sk__14 @ sk__15))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl484, zip_derived_cl57])).
% 118.89/17.64 thf(zip_derived_cl566, plain, ( (aElementOf0 @ (sk__14 @ sk__15) @ xS)),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl557, zip_derived_cl124])).
% 118.89/17.64 thf(zip_derived_cl115, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i, X2 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ X0 @ X1)
% 118.89/17.64 | (aInteger0 @ X2)
% 118.89/17.64 | ~ (aElementOf0 @ X2 @
% 118.89/17.64 (szAzrzSzezqlpdtcmdtrp0 @ X0 @ (sk__12 @ X0 @ X1)))
% 118.89/17.64 | ~ (aElementOf0 @ X1 @ xS))),
% 118.89/17.64 inference('cnf', [status(esa)], [m__1750])).
% 118.89/17.64 thf(zip_derived_cl658, plain,
% 118.89/17.64 (![X0 : $i, X1 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ X1 @
% 118.89/17.64 (szAzrzSzezqlpdtcmdtrp0 @ X0 @ (sk__12 @ X0 @ (sk__14 @ sk__15))))
% 118.89/17.64 | (aInteger0 @ X1)
% 118.89/17.64 | ~ (aElementOf0 @ X0 @ (sk__14 @ sk__15)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl566, zip_derived_cl115])).
% 118.89/17.64 thf(zip_derived_cl1000, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 ( (aInteger0 @ X0)
% 118.89/17.64 | ~ (aElementOf0 @ X0 @
% 118.89/17.64 (szAzrzSzezqlpdtcmdtrp0 @ sk__15 @
% 118.89/17.64 (sk__12 @ sk__15 @ (sk__14 @ sk__15)))))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl537, zip_derived_cl658])).
% 118.89/17.64 thf(zip_derived_cl103879, plain,
% 118.89/17.64 ((~ (aInteger0 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15)))
% 118.89/17.64 | ((sk__12 @ sk__15 @ (sk__14 @ sk__15)) = (sz00))
% 118.89/17.64 | (aInteger0 @ (sk__16 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15)))))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl133, zip_derived_cl1000])).
% 118.89/17.64 thf(zip_derived_cl1673, plain,
% 118.89/17.64 ( (aInteger0 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl537, zip_derived_cl656])).
% 118.89/17.64 thf(zip_derived_cl103903, plain,
% 118.89/17.64 ((((sk__12 @ sk__15 @ (sk__14 @ sk__15)) = (sz00))
% 118.89/17.64 | (aInteger0 @ (sk__16 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15)))))),
% 118.89/17.64 inference('demod', [status(thm)],
% 118.89/17.64 [zip_derived_cl103879, zip_derived_cl1673])).
% 118.89/17.64 thf(zip_derived_cl558, plain,
% 118.89/17.64 (((sk__12 @ sk__15 @ (sk__14 @ sk__15)) != (sz00))),
% 118.89/17.64 inference('demod', [status(thm)], [zip_derived_cl547, zip_derived_cl151])).
% 118.89/17.64 thf(zip_derived_cl103904, plain,
% 118.89/17.64 ( (aInteger0 @ (sk__16 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15))))),
% 118.89/17.64 inference('simplify_reflect-', [status(thm)],
% 118.89/17.64 [zip_derived_cl103903, zip_derived_cl558])).
% 118.89/17.64 thf(zip_derived_cl126324, plain,
% 118.89/17.64 ( (zip_tseitin_8 @ (sk__16 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15))))),
% 118.89/17.64 inference('demod', [status(thm)],
% 118.89/17.64 [zip_derived_cl126228, zip_derived_cl103904])).
% 118.89/17.64 thf(zip_derived_cl130, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 ( (aElementOf0 @ X0 @ (sbsmnsldt0 @ xS)) | ~ (zip_tseitin_8 @ X0))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_5])).
% 118.89/17.64 thf(zip_derived_cl134, plain,
% 118.89/17.64 (![X2 : $i]:
% 118.89/17.64 (~ (aElementOf0 @ (sk__16 @ X2) @ (sbsmnsldt0 @ xS))
% 118.89/17.64 | ((X2) = (sz00))
% 118.89/17.64 | ~ (aInteger0 @ X2))),
% 118.89/17.64 inference('cnf', [status(esa)], [zf_stmt_5])).
% 118.89/17.64 thf(zip_derived_cl277, plain,
% 118.89/17.64 (![X0 : $i]:
% 118.89/17.64 (~ (zip_tseitin_8 @ (sk__16 @ X0))
% 118.89/17.64 | ~ (aInteger0 @ X0)
% 118.89/17.64 | ((X0) = (sz00)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl130, zip_derived_cl134])).
% 118.89/17.64 thf(zip_derived_cl126364, plain,
% 118.89/17.64 ((((sk__12 @ sk__15 @ (sk__14 @ sk__15)) = (sz00))
% 118.89/17.64 | ~ (aInteger0 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15))))),
% 118.89/17.64 inference('sup-', [status(thm)],
% 118.89/17.64 [zip_derived_cl126324, zip_derived_cl277])).
% 118.89/17.64 thf(zip_derived_cl1673, plain,
% 118.89/17.64 ( (aInteger0 @ (sk__12 @ sk__15 @ (sk__14 @ sk__15)))),
% 118.89/17.64 inference('sup-', [status(thm)], [zip_derived_cl537, zip_derived_cl656])).
% 118.89/17.64 thf(zip_derived_cl126377, plain,
% 118.89/17.64 (((sk__12 @ sk__15 @ (sk__14 @ sk__15)) = (sz00))),
% 118.89/17.64 inference('demod', [status(thm)],
% 118.89/17.64 [zip_derived_cl126364, zip_derived_cl1673])).
% 118.89/17.64 thf(zip_derived_cl558, plain,
% 118.89/17.64 (((sk__12 @ sk__15 @ (sk__14 @ sk__15)) != (sz00))),
% 118.89/17.64 inference('demod', [status(thm)], [zip_derived_cl547, zip_derived_cl151])).
% 118.89/17.64 thf(zip_derived_cl126378, plain, ($false),
% 118.89/17.64 inference('simplify_reflect-', [status(thm)],
% 118.89/17.64 [zip_derived_cl126377, zip_derived_cl558])).
% 118.89/17.64
% 118.89/17.64 % SZS output end Refutation
% 118.89/17.64
% 118.89/17.64
% 118.89/17.64 % Terminating...
% 119.69/17.74 % Runner terminated.
% 119.69/17.75 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------