%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM441+6 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.4YiBg0Jo6u true
% Computer : n016.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 4.04s 1.21s
% Output : Refutation 4.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.20 % Problem : NUM441+6 : TPTP v9.2.0. Released v4.0.0.
% 0.12/0.21 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.4YiBg0Jo6u true
% 0.14/0.44 % Computer : n016.cluster.edu
% 0.14/0.44 % Model : x86_64 x86_64
% 0.14/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.44 % Memory : 8042.1875MB
% 0.14/0.44 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.44 % CPULimit : 300
% 0.14/0.44 % WCLimit : 300
% 0.14/0.44 % DateTime : Wed Oct 1 16:52:23 EDT 2025
% 0.14/0.44 % CPUTime :
% 0.14/0.44 % Running portfolio for 300 s
% 0.14/0.44 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.44 % Number of cores: 8
% 0.14/0.44 % Python version: Python 3.6.8
% 0.14/0.44 % Running in FO mode
% 0.47/0.65 % Total configuration time : 435
% 0.47/0.65 % Estimated wc time : 1092
% 0.47/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.49/0.73 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.49/0.73 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.49/0.75 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.49/0.75 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.49/0.76 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.49/0.78 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.49/0.78 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 4.04/1.20 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 4.04/1.21 % Solved by fo/fo6_bce.sh.
% 4.04/1.21 % BCE start: 221
% 4.04/1.21 % BCE eliminated: 1
% 4.04/1.21 % PE start: 220
% 4.04/1.21 logic: eq
% 4.04/1.21 % PE eliminated: 12
% 4.04/1.21 % done 297 iterations in 0.428s
% 4.04/1.21 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 4.04/1.21 % SZS output start Refutation
% 4.04/1.21 thf(smndt0_type, type, smndt0: $i > $i).
% 4.04/1.21 thf(xB_type, type, xB: $i).
% 4.04/1.21 thf(isOpen0_type, type, isOpen0: $i > $o).
% 4.04/1.21 thf(sdtasdt0_type, type, sdtasdt0: $i > $i > $i).
% 4.04/1.21 thf(aInteger0_type, type, aInteger0: $i > $o).
% 4.04/1.21 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $o).
% 4.04/1.21 thf(sdtbsmnsldt0_type, type, sdtbsmnsldt0: $i > $i > $i).
% 4.04/1.21 thf(zip_tseitin_8_type, type, zip_tseitin_8: $i > $o).
% 4.04/1.21 thf(cS1395_type, type, cS1395: $i).
% 4.04/1.21 thf(sz00_type, type, sz00: $i).
% 4.04/1.21 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 4.04/1.21 thf(szAzrzSzezqlpdtcmdtrp0_type, type, szAzrzSzezqlpdtcmdtrp0: $i > $i > $i).
% 4.04/1.21 thf(stldt0_type, type, stldt0: $i > $i).
% 4.04/1.21 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 4.04/1.21 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 4.04/1.21 thf(aDivisorOf0_type, type, aDivisorOf0: $i > $i > $o).
% 4.04/1.21 thf(sdteqdtlpzmzozddtrp0_type, type, sdteqdtlpzmzozddtrp0: $i > $i > $i > $o).
% 4.04/1.21 thf(isClosed0_type, type, isClosed0: $i > $o).
% 4.04/1.21 thf(aSet0_type, type, aSet0: $i > $o).
% 4.04/1.21 thf(sdtslmnbsdt0_type, type, sdtslmnbsdt0: $i > $i > $i).
% 4.04/1.21 thf(xA_type, type, xA: $i).
% 4.04/1.21 thf(zip_tseitin_9_type, type, zip_tseitin_9: $i > $o).
% 4.04/1.21 thf(m__, conjecture,
% 4.04/1.21 (( ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) <=>
% 4.04/1.21 ( ( ( aElementOf0 @ W0 @ xB ) | ( aElementOf0 @ W0 @ xA ) ) &
% 4.04/1.21 ( aInteger0 @ W0 ) ) ) ) &
% 4.04/1.21 ( aSet0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) =>
% 4.04/1.21 ( ( isClosed0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) |
% 4.04/1.21 ( ( ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 4.04/1.21 ( ( ~( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) &
% 4.04/1.21 ( aInteger0 @ W0 ) ) ) ) &
% 4.04/1.21 ( aSet0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) =>
% 4.04/1.21 ( ( isOpen0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) |
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) =>
% 4.04/1.21 ( ?[W1:$i]:
% 4.04/1.21 ( ( aInteger0 @ W1 ) & ( ( W1 ) != ( sz00 ) ) &
% 4.04/1.21 ( ( ( ![W2:$i]:
% 4.04/1.21 ( ( ( aElementOf0 @
% 4.04/1.21 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 4.04/1.21 ( ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) &
% 4.04/1.21 ( aDivisorOf0 @
% 4.04/1.21 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( ?[W3:$i]:
% 4.04/1.21 ( ( aInteger0 @ W3 ) &
% 4.04/1.21 ( ( sdtasdt0 @ W1 @ W3 ) =
% 4.04/1.21 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) ) ) &
% 4.04/1.21 ( aInteger0 @ W2 ) ) ) &
% 4.04/1.21 ( ( ( ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) |
% 4.04/1.21 ( aDivisorOf0 @
% 4.04/1.21 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 4.04/1.21 ( ?[W3:$i]:
% 4.04/1.21 ( ( aInteger0 @ W3 ) &
% 4.04/1.21 ( ( sdtasdt0 @ W1 @ W3 ) =
% 4.04/1.21 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) ) ) ) &
% 4.04/1.21 ( aInteger0 @ W2 ) ) =>
% 4.04/1.21 ( aElementOf0 @
% 4.04/1.21 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) ) ) &
% 4.04/1.21 ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) =>
% 4.04/1.21 ( ( aSubsetOf0 @
% 4.04/1.21 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @
% 4.04/1.21 ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) |
% 4.04/1.21 ( ![W2:$i]:
% 4.04/1.21 ( ( aElementOf0 @
% 4.04/1.21 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 4.04/1.21 ( aElementOf0 @
% 4.04/1.21 W2 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) ) ) ) ) ) ) ) ) ) ))).
% 4.04/1.21 thf(zf_stmt_0, type, zip_tseitin_9 : $i > $o).
% 4.04/1.21 thf(zf_stmt_1, axiom,
% 4.04/1.21 (![W0:$i]:
% 4.04/1.21 ( ( zip_tseitin_9 @ W0 ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) &
% 4.04/1.21 ( ~( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) ))).
% 4.04/1.21 thf(zf_stmt_2, type, zip_tseitin_8 : $i > $o).
% 4.04/1.21 thf(zf_stmt_3, axiom,
% 4.04/1.21 (![W0:$i]:
% 4.04/1.21 ( ( zip_tseitin_8 @ W0 ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) & ( zip_tseitin_7 @ W0 ) ) ))).
% 4.04/1.21 thf(zf_stmt_4, type, zip_tseitin_7 : $i > $o).
% 4.04/1.21 thf(zf_stmt_5, axiom,
% 4.04/1.21 (![W0:$i]:
% 4.04/1.21 ( ( zip_tseitin_7 @ W0 ) <=>
% 4.04/1.21 ( ( aElementOf0 @ W0 @ xA ) | ( aElementOf0 @ W0 @ xB ) ) ))).
% 4.04/1.21 thf(zf_stmt_6, conjecture,
% 4.04/1.21 (( ( aSet0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) <=>
% 4.04/1.21 ( zip_tseitin_8 @ W0 ) ) ) ) =>
% 4.04/1.21 ( ( ( ( aSet0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 4.04/1.21 ( zip_tseitin_9 @ W0 ) ) ) ) =>
% 4.04/1.21 ( ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) =>
% 4.04/1.21 ( ?[W1:$i]:
% 4.04/1.21 ( ( ( ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) &
% 4.04/1.21 ( ![W2:$i]:
% 4.04/1.21 ( ( ( ( aInteger0 @ W2 ) &
% 4.04/1.21 ( ( ?[W3:$i]:
% 4.04/1.21 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 4.04/1.21 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( aInteger0 @ W3 ) ) ) |
% 4.04/1.21 ( aDivisorOf0 @
% 4.04/1.21 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 4.04/1.21 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) =>
% 4.04/1.21 ( aElementOf0 @
% 4.04/1.21 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) &
% 4.04/1.21 ( ( aElementOf0 @
% 4.04/1.21 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 4.04/1.21 ( ( aInteger0 @ W2 ) &
% 4.04/1.21 ( ?[W3:$i]:
% 4.04/1.21 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 4.04/1.21 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( aInteger0 @ W3 ) ) ) &
% 4.04/1.21 ( aDivisorOf0 @
% 4.04/1.21 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) ) ) ) =>
% 4.04/1.21 ( ( ![W2:$i]:
% 4.04/1.21 ( ( aElementOf0 @
% 4.04/1.21 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 4.04/1.21 ( aElementOf0 @
% 4.04/1.21 W2 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) ) |
% 4.04/1.21 ( aSubsetOf0 @
% 4.04/1.21 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @
% 4.04/1.21 ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) ) &
% 4.04/1.21 ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) |
% 4.04/1.21 ( isOpen0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) ) |
% 4.04/1.21 ( isClosed0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ))).
% 4.04/1.21 thf(zf_stmt_7, negated_conjecture,
% 4.04/1.21 (~( ( ( aSet0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) <=>
% 4.04/1.21 ( zip_tseitin_8 @ W0 ) ) ) ) =>
% 4.04/1.21 ( ( ( ( aSet0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 4.04/1.21 ( zip_tseitin_9 @ W0 ) ) ) ) =>
% 4.04/1.21 ( ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) =>
% 4.04/1.21 ( ?[W1:$i]:
% 4.04/1.21 ( ( ( ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) &
% 4.04/1.21 ( ![W2:$i]:
% 4.04/1.21 ( ( ( ( aInteger0 @ W2 ) &
% 4.04/1.21 ( ( ?[W3:$i]:
% 4.04/1.21 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 4.04/1.21 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( aInteger0 @ W3 ) ) ) |
% 4.04/1.21 ( aDivisorOf0 @
% 4.04/1.21 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 4.04/1.21 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) =>
% 4.04/1.21 ( aElementOf0 @
% 4.04/1.21 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) &
% 4.04/1.21 ( ( aElementOf0 @
% 4.04/1.21 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 4.04/1.21 ( ( aInteger0 @ W2 ) &
% 4.04/1.21 ( ?[W3:$i]:
% 4.04/1.21 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 4.04/1.21 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( aInteger0 @ W3 ) ) ) &
% 4.04/1.21 ( aDivisorOf0 @
% 4.04/1.21 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) ) ) ) =>
% 4.04/1.21 ( ( ![W2:$i]:
% 4.04/1.21 ( ( aElementOf0 @
% 4.04/1.21 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 4.04/1.21 ( aElementOf0 @
% 4.04/1.21 W2 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) ) |
% 4.04/1.21 ( aSubsetOf0 @
% 4.04/1.21 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @
% 4.04/1.21 ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) ) &
% 4.04/1.21 ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) |
% 4.04/1.21 ( isOpen0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) ) |
% 4.04/1.21 ( isClosed0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) )),
% 4.04/1.21 inference('cnf.neg', [status(esa)], [zf_stmt_6])).
% 4.04/1.21 thf(zip_derived_cl219, plain,
% 4.04/1.21 (~ (isOpen0 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))),
% 4.04/1.21 inference('cnf', [status(esa)], [zf_stmt_7])).
% 4.04/1.21 thf(m__1883, axiom,
% 4.04/1.21 (( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xA ) ) ) ) ) &
% 4.04/1.21 ( aSubsetOf0 @ ( stldt0 @ xB ) @ cS1395 ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xB ) ) ) ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) =>
% 4.04/1.21 ( aElementOf0 @ W0 @ cS1395 ) ) ) &
% 4.04/1.21 ( aSubsetOf0 @ ( stldt0 @ xA ) @ cS1395 ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xA ) ) ) ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) &
% 4.04/1.21 ( ( aElementOf0 @ W0 @ xA ) | ( aElementOf0 @ W0 @ xB ) ) ) ) ) &
% 4.04/1.21 ( aSet0 @ cS1395 ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) &
% 4.04/1.21 ( ~( aElementOf0 @ W0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) ) ) ) &
% 4.04/1.21 ( ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) =
% 4.04/1.21 ( sdtslmnbsdt0 @ ( stldt0 @ xA ) @ ( stldt0 @ xB ) ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xB ) ) ) ) ) &
% 4.04/1.21 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) &
% 4.04/1.21 ( aSet0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) &
% 4.04/1.21 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) =>
% 4.04/1.21 ( aElementOf0 @ W0 @ cS1395 ) ) ) &
% 4.04/1.21 ( aSet0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sdtbsmnsldt0 @ xA @ xB ) ) ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) & ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) &
% 4.04/1.21 ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) ) ) ) &
% 4.04/1.21 ( aSet0 @ ( stldt0 @ xB ) ) & ( aSet0 @ ( stldt0 @ xA ) ))).
% 4.04/1.21 thf(zip_derived_cl170, plain,
% 4.04/1.21 (((stldt0 @ (sdtbsmnsldt0 @ xA @ xB))
% 4.04/1.21 = (sdtslmnbsdt0 @ (stldt0 @ xA) @ (stldt0 @ xB)))),
% 4.04/1.21 inference('cnf', [status(esa)], [m__1883])).
% 4.04/1.21 thf(mInterOpen, axiom,
% 4.04/1.21 (![W0:$i,W1:$i]:
% 4.04/1.21 ( ( ( aSubsetOf0 @ W0 @ cS1395 ) & ( aSubsetOf0 @ W1 @ cS1395 ) &
% 4.04/1.21 ( isOpen0 @ W0 ) & ( isOpen0 @ W1 ) ) =>
% 4.04/1.21 ( isOpen0 @ ( sdtslmnbsdt0 @ W0 @ W1 ) ) ))).
% 4.04/1.21 thf(zip_derived_cl104, plain,
% 4.04/1.21 (![X0 : $i, X1 : $i]:
% 4.04/1.21 (~ (isOpen0 @ X0)
% 4.04/1.21 | ~ (aSubsetOf0 @ X0 @ cS1395)
% 4.04/1.21 | ~ (aSubsetOf0 @ X1 @ cS1395)
% 4.04/1.21 | ~ (isOpen0 @ X1)
% 4.04/1.21 | (isOpen0 @ (sdtslmnbsdt0 @ X0 @ X1)))),
% 4.04/1.21 inference('cnf', [status(esa)], [mInterOpen])).
% 4.04/1.21 thf(zip_derived_cl2671, plain,
% 4.04/1.21 ((~ (isOpen0 @ (stldt0 @ xA))
% 4.04/1.21 | ~ (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)
% 4.04/1.21 | ~ (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)
% 4.04/1.21 | ~ (isOpen0 @ (stldt0 @ xB))
% 4.04/1.21 | (isOpen0 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB))))),
% 4.04/1.21 inference('s_sup+', [status(thm)], [zip_derived_cl170, zip_derived_cl104])).
% 4.04/1.21 thf(m__1826, axiom,
% 4.04/1.21 (( isOpen0 @ ( stldt0 @ xB ) ) &
% 4.04/1.21 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xB ) => ( aElementOf0 @ W0 @ cS1395 ) ) ) &
% 4.04/1.21 ( aSubsetOf0 @ xB @ cS1395 ) & ( isClosed0 @ xA ) &
% 4.04/1.21 ( aSubsetOf0 @ xA @ cS1395 ) & ( aSet0 @ cS1395 ) &
% 4.04/1.21 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) &
% 4.04/1.21 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ xA ) => ( aElementOf0 @ W0 @ cS1395 ) ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xB ) ) ) ) ) &
% 4.04/1.21 ( aSet0 @ xB ) & ( isClosed0 @ xB ) &
% 4.04/1.21 ( ![W0:$i]: ( ( aElementOf0 @ W0 @ cS1395 ) <=> ( aInteger0 @ W0 ) ) ) &
% 4.04/1.21 ( isOpen0 @ ( stldt0 @ xA ) ) & ( aSet0 @ xA ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) =>
% 4.04/1.21 ( ?[W1:$i]:
% 4.04/1.21 ( ( aSubsetOf0 @
% 4.04/1.21 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @ ( stldt0 @ xA ) ) &
% 4.04/1.21 ( ![W2:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 4.04/1.21 ( aElementOf0 @ W2 @ ( stldt0 @ xA ) ) ) ) &
% 4.04/1.21 ( ![W2:$i]:
% 4.04/1.21 ( ( ( ( aInteger0 @ W2 ) &
% 4.04/1.21 ( ( ?[W3:$i]:
% 4.04/1.21 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 4.04/1.21 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( aInteger0 @ W3 ) ) ) |
% 4.04/1.21 ( aDivisorOf0 @ W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 4.04/1.21 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) =>
% 4.04/1.21 ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) &
% 4.04/1.21 ( ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 4.04/1.21 ( ( aInteger0 @ W2 ) &
% 4.04/1.21 ( ?[W3:$i]:
% 4.04/1.21 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 4.04/1.21 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( aInteger0 @ W3 ) ) ) &
% 4.04/1.21 ( aDivisorOf0 @ W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) ) ) &
% 4.04/1.21 ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) &
% 4.04/1.21 ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ xB ) ) =>
% 4.04/1.21 ( ?[W1:$i]:
% 4.04/1.21 ( ( aSubsetOf0 @
% 4.04/1.21 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @ ( stldt0 @ xB ) ) &
% 4.04/1.21 ( ![W2:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 4.04/1.21 ( aElementOf0 @ W2 @ ( stldt0 @ xB ) ) ) ) &
% 4.04/1.21 ( ![W2:$i]:
% 4.04/1.21 ( ( ( ( aInteger0 @ W2 ) &
% 4.04/1.21 ( ( ?[W3:$i]:
% 4.04/1.21 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 4.04/1.21 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( aInteger0 @ W3 ) ) ) |
% 4.04/1.21 ( aDivisorOf0 @ W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 4.04/1.21 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) =>
% 4.04/1.21 ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) &
% 4.04/1.21 ( ( aElementOf0 @ W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 4.04/1.21 ( ( aInteger0 @ W2 ) &
% 4.04/1.21 ( ?[W3:$i]:
% 4.04/1.21 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 4.04/1.21 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( aInteger0 @ W3 ) ) ) &
% 4.04/1.21 ( aDivisorOf0 @ W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 4.04/1.21 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) ) ) &
% 4.04/1.21 ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) &
% 4.04/1.21 ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) &
% 4.04/1.21 ( ![W0:$i]:
% 4.04/1.21 ( ( aElementOf0 @ W0 @ ( stldt0 @ xA ) ) <=>
% 4.04/1.21 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ xA ) ) ) ) ) &
% 4.04/1.21 ( aSet0 @ ( stldt0 @ xB ) ) & ( aSet0 @ ( stldt0 @ xA ) ))).
% 4.04/1.21 thf(zip_derived_cl137, plain, ( (isOpen0 @ (stldt0 @ xA))),
% 4.04/1.21 inference('cnf', [status(esa)], [m__1826])).
% 4.04/1.21 thf(zip_derived_cl182, plain, ( (aSubsetOf0 @ (stldt0 @ xA) @ cS1395)),
% 4.04/1.21 inference('cnf', [status(esa)], [m__1883])).
% 4.04/1.21 thf(zip_derived_cl187, plain, ( (aSubsetOf0 @ (stldt0 @ xB) @ cS1395)),
% 4.04/1.21 inference('cnf', [status(esa)], [m__1883])).
% 4.04/1.21 thf(zip_derived_cl153, plain, ( (isOpen0 @ (stldt0 @ xB))),
% 4.04/1.21 inference('cnf', [status(esa)], [m__1826])).
% 4.04/1.21 thf(zip_derived_cl2672, plain,
% 4.04/1.21 ( (isOpen0 @ (stldt0 @ (sdtbsmnsldt0 @ xA @ xB)))),
% 4.04/1.21 inference('demod', [status(thm)],
% 4.04/1.21 [zip_derived_cl2671, zip_derived_cl137, zip_derived_cl182,
% 4.04/1.21 zip_derived_cl187, zip_derived_cl153])).
% 4.04/1.21 thf(zip_derived_cl2673, plain, ($false),
% 4.04/1.21 inference('demod', [status(thm)], [zip_derived_cl219, zip_derived_cl2672])).
% 4.04/1.21
% 4.04/1.21 % SZS output end Refutation
% 4.04/1.21
% 4.04/1.21
% 4.04/1.21 % Terminating...
% 4.27/1.28 % Runner terminated.
% 4.27/1.29 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------