%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM449+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.m4RfYVQYPB true
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:47:00 PM UTC 2025
% Result : Theorem 3.33s 1.35s
% Output : Refutation 3.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : NUM449+6 : TPTP v9.2.0. Released v4.0.0.
% 0.03/0.14 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.m4RfYVQYPB true
% 0.12/0.35 % Computer : n028.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Wed Oct 1 16:32:38 EDT 2025
% 0.12/0.35 % CPUTime :
% 0.12/0.35 % Running portfolio for 300 s
% 0.12/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.35 % Number of cores: 8
% 0.12/0.35 % Python version: Python 3.6.8
% 0.12/0.35 % Running in FO mode
% 0.41/0.62 % Total configuration time : 435
% 0.41/0.62 % Estimated wc time : 1092
% 0.41/0.62 % Estimated cpu time (7 cpus) : 156.0
% 0.49/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.49/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.49/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.49/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.49/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.50/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.50/0.82 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 3.33/1.35 % Solved by fo/fo13.sh.
% 3.33/1.35 % done 525 iterations in 0.526s
% 3.33/1.35 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 3.33/1.35 % SZS output start Refutation
% 3.33/1.35 thf(smndt0_type, type, smndt0: $i > $i).
% 3.33/1.35 thf(isOpen0_type, type, isOpen0: $i > $o).
% 3.33/1.35 thf(sdtasdt0_type, type, sdtasdt0: $i > $i > $i).
% 3.33/1.35 thf(aInteger0_type, type, aInteger0: $i > $o).
% 3.33/1.35 thf(cS2043_type, type, cS2043: $i).
% 3.33/1.35 thf(xS_type, type, xS: $i).
% 3.33/1.35 thf(isFinite0_type, type, isFinite0: $i > $o).
% 3.33/1.35 thf(cS1395_type, type, cS1395: $i).
% 3.33/1.35 thf(sz00_type, type, sz00: $i).
% 3.33/1.35 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 3.33/1.35 thf(sbsmnsldt0_type, type, sbsmnsldt0: $i > $i).
% 3.33/1.35 thf(szAzrzSzezqlpdtcmdtrp0_type, type, szAzrzSzezqlpdtcmdtrp0: $i > $i > $i).
% 3.33/1.35 thf(stldt0_type, type, stldt0: $i > $i).
% 3.33/1.35 thf(sk__14_type, type, sk__14: $i > $i).
% 3.33/1.35 thf(aSubsetOf0_type, type, aSubsetOf0: $i > $i > $o).
% 3.33/1.35 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 3.33/1.35 thf(zip_tseitin_8_type, type, zip_tseitin_8: $i > $o).
% 3.33/1.35 thf(sk__13_type, type, sk__13: $i > $i).
% 3.33/1.35 thf(isPrime0_type, type, isPrime0: $i > $o).
% 3.33/1.35 thf(aDivisorOf0_type, type, aDivisorOf0: $i > $i > $o).
% 3.33/1.35 thf(zip_tseitin_9_type, type, zip_tseitin_9: $i > $o).
% 3.33/1.35 thf(sdteqdtlpzmzozddtrp0_type, type, sdteqdtlpzmzozddtrp0: $i > $i > $i > $o).
% 3.33/1.35 thf(isClosed0_type, type, isClosed0: $i > $o).
% 3.33/1.35 thf(zip_tseitin_7_type, type, zip_tseitin_7: $i > $i > $o).
% 3.33/1.35 thf(aSet0_type, type, aSet0: $i > $o).
% 3.33/1.35 thf(m__, conjecture,
% 3.33/1.35 (( ( ![W0:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) <=>
% 3.33/1.35 ( ( ?[W1:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W1 @ xS ) & ( aElementOf0 @ W0 @ W1 ) ) ) &
% 3.33/1.35 ( aInteger0 @ W0 ) ) ) ) &
% 3.33/1.35 ( aSet0 @ ( sbsmnsldt0 @ xS ) ) ) =>
% 3.33/1.35 ( ( isClosed0 @ ( sbsmnsldt0 @ xS ) ) |
% 3.33/1.35 ( ( ![W0:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) <=>
% 3.33/1.35 ( ( ~( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) ) &
% 3.33/1.35 ( aInteger0 @ W0 ) ) ) ) =>
% 3.33/1.35 ( ( isOpen0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) |
% 3.33/1.35 ( ![W0:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) =>
% 3.33/1.35 ( ?[W1:$i]:
% 3.33/1.35 ( ( aInteger0 @ W1 ) & ( ( W1 ) != ( sz00 ) ) &
% 3.33/1.35 ( ( ( ![W2:$i]:
% 3.33/1.35 ( ( ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 3.33/1.35 ( ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) &
% 3.33/1.35 ( aDivisorOf0 @
% 3.33/1.35 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 3.33/1.35 ( ?[W3:$i]:
% 3.33/1.35 ( ( aInteger0 @ W3 ) &
% 3.33/1.35 ( ( sdtasdt0 @ W1 @ W3 ) =
% 3.33/1.35 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) ) ) &
% 3.33/1.35 ( aInteger0 @ W2 ) ) ) &
% 3.33/1.35 ( ( ( ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) |
% 3.33/1.35 ( aDivisorOf0 @
% 3.33/1.35 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 3.33/1.35 ( ?[W3:$i]:
% 3.33/1.35 ( ( aInteger0 @ W3 ) &
% 3.33/1.35 ( ( sdtasdt0 @ W1 @ W3 ) =
% 3.33/1.35 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) ) ) ) &
% 3.33/1.35 ( aInteger0 @ W2 ) ) =>
% 3.33/1.35 ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) ) ) &
% 3.33/1.35 ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) =>
% 3.33/1.35 ( ( aSubsetOf0 @
% 3.33/1.35 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @
% 3.33/1.35 ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) |
% 3.33/1.35 ( ![W2:$i]:
% 3.33/1.35 ( ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 3.33/1.35 ( aElementOf0 @
% 3.33/1.35 W2 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) ) ) ) ) ) ) ) ) ) ) ))).
% 3.33/1.35 thf(zf_stmt_0, type, zip_tseitin_9 : $i > $o).
% 3.33/1.35 thf(zf_stmt_1, axiom,
% 3.33/1.35 (![W0:$i]:
% 3.33/1.35 ( ( zip_tseitin_9 @ W0 ) <=>
% 3.33/1.35 ( ( aInteger0 @ W0 ) & ( ~( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) ) ) ))).
% 3.33/1.35 thf(zf_stmt_2, type, zip_tseitin_8 : $i > $o).
% 3.33/1.35 thf(zf_stmt_3, axiom,
% 3.33/1.35 (![W0:$i]:
% 3.33/1.35 ( ( zip_tseitin_8 @ W0 ) <=>
% 3.33/1.35 ( ( aInteger0 @ W0 ) & ( ?[W1:$i]: ( zip_tseitin_7 @ W1 @ W0 ) ) ) ))).
% 3.33/1.35 thf(zf_stmt_4, type, zip_tseitin_7 : $i > $i > $o).
% 3.33/1.35 thf(zf_stmt_5, axiom,
% 3.33/1.35 (![W1:$i,W0:$i]:
% 3.33/1.35 ( ( zip_tseitin_7 @ W1 @ W0 ) <=>
% 3.33/1.35 ( ( aElementOf0 @ W0 @ W1 ) & ( aElementOf0 @ W1 @ xS ) ) ))).
% 3.33/1.35 thf(zf_stmt_6, conjecture,
% 3.33/1.35 (( ( aSet0 @ ( sbsmnsldt0 @ xS ) ) &
% 3.33/1.35 ( ![W0:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) <=>
% 3.33/1.35 ( zip_tseitin_8 @ W0 ) ) ) ) =>
% 3.33/1.35 ( ( ( ![W0:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) <=>
% 3.33/1.35 ( zip_tseitin_9 @ W0 ) ) ) =>
% 3.33/1.35 ( ( ![W0:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) =>
% 3.33/1.35 ( ?[W1:$i]:
% 3.33/1.35 ( ( ( ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) &
% 3.33/1.35 ( ![W2:$i]:
% 3.33/1.35 ( ( ( ( aInteger0 @ W2 ) &
% 3.33/1.35 ( ( ?[W3:$i]:
% 3.33/1.35 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 3.33/1.35 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 3.33/1.35 ( aInteger0 @ W3 ) ) ) |
% 3.33/1.35 ( aDivisorOf0 @
% 3.33/1.35 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 3.33/1.35 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) =>
% 3.33/1.35 ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) &
% 3.33/1.35 ( ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 3.33/1.35 ( ( aInteger0 @ W2 ) &
% 3.33/1.35 ( ?[W3:$i]:
% 3.33/1.35 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 3.33/1.35 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 3.33/1.35 ( aInteger0 @ W3 ) ) ) &
% 3.33/1.35 ( aDivisorOf0 @
% 3.33/1.35 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 3.33/1.35 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) ) ) ) =>
% 3.33/1.35 ( ( ![W2:$i]:
% 3.33/1.35 ( ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 3.33/1.35 ( aElementOf0 @
% 3.33/1.35 W2 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) ) ) |
% 3.33/1.35 ( aSubsetOf0 @
% 3.33/1.35 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @
% 3.33/1.35 ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) ) ) &
% 3.33/1.35 ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) |
% 3.33/1.35 ( isOpen0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) ) ) |
% 3.33/1.35 ( isClosed0 @ ( sbsmnsldt0 @ xS ) ) ))).
% 3.33/1.35 thf(zf_stmt_7, negated_conjecture,
% 3.33/1.35 (~( ( ( aSet0 @ ( sbsmnsldt0 @ xS ) ) &
% 3.33/1.35 ( ![W0:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W0 @ ( sbsmnsldt0 @ xS ) ) <=>
% 3.33/1.35 ( zip_tseitin_8 @ W0 ) ) ) ) =>
% 3.33/1.35 ( ( ( ![W0:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) <=>
% 3.33/1.35 ( zip_tseitin_9 @ W0 ) ) ) =>
% 3.33/1.35 ( ( ![W0:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) =>
% 3.33/1.35 ( ?[W1:$i]:
% 3.33/1.35 ( ( ( ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) &
% 3.33/1.35 ( ![W2:$i]:
% 3.33/1.35 ( ( ( ( aInteger0 @ W2 ) &
% 3.33/1.35 ( ( ?[W3:$i]:
% 3.33/1.35 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 3.33/1.35 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 3.33/1.35 ( aInteger0 @ W3 ) ) ) |
% 3.33/1.35 ( aDivisorOf0 @
% 3.33/1.35 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) |
% 3.33/1.35 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) =>
% 3.33/1.35 ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) &
% 3.33/1.35 ( ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 3.33/1.35 ( ( aInteger0 @ W2 ) &
% 3.33/1.35 ( ?[W3:$i]:
% 3.33/1.35 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 3.33/1.35 ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 3.33/1.35 ( aInteger0 @ W3 ) ) ) &
% 3.33/1.35 ( aDivisorOf0 @
% 3.33/1.35 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ W0 ) ) ) &
% 3.33/1.35 ( sdteqdtlpzmzozddtrp0 @ W2 @ W0 @ W1 ) ) ) ) ) ) =>
% 3.33/1.35 ( ( ![W2:$i]:
% 3.33/1.35 ( ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) =>
% 3.33/1.35 ( aElementOf0 @
% 3.33/1.35 W2 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) ) ) |
% 3.33/1.35 ( aSubsetOf0 @
% 3.33/1.35 ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @
% 3.33/1.35 ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) ) ) &
% 3.33/1.35 ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) |
% 3.33/1.35 ( isOpen0 @ ( stldt0 @ ( sbsmnsldt0 @ xS ) ) ) ) ) |
% 3.33/1.35 ( isClosed0 @ ( sbsmnsldt0 @ xS ) ) ) )),
% 3.33/1.35 inference('cnf.neg', [status(esa)], [zf_stmt_6])).
% 3.33/1.35 thf(zip_derived_cl177, plain, (~ (isClosed0 @ (sbsmnsldt0 @ xS))),
% 3.33/1.35 inference('cnf', [status(esa)], [zf_stmt_7])).
% 3.33/1.35 thf(mUnionSClosed, axiom,
% 3.33/1.35 (![W0:$i]:
% 3.33/1.35 ( ( ( aSet0 @ W0 ) & ( isFinite0 @ W0 ) &
% 3.33/1.35 ( ![W1:$i]:
% 3.33/1.35 ( ( aElementOf0 @ W1 @ W0 ) =>
% 3.33/1.35 ( ( aSubsetOf0 @ W1 @ cS1395 ) & ( isClosed0 @ W1 ) ) ) ) ) =>
% 3.33/1.35 ( isClosed0 @ ( sbsmnsldt0 @ W0 ) ) ))).
% 3.33/1.35 thf(zip_derived_cl106, plain,
% 3.33/1.35 (![X0 : $i]:
% 3.33/1.35 ( (isClosed0 @ (sbsmnsldt0 @ X0))
% 3.33/1.35 | (aElementOf0 @ (sk__13 @ X0) @ X0)
% 3.33/1.35 | ~ (isFinite0 @ X0)
% 3.33/1.35 | ~ (aSet0 @ X0))),
% 3.33/1.35 inference('cnf', [status(esa)], [mUnionSClosed])).
% 3.33/1.35 thf(m__2046, axiom,
% 3.33/1.35 (( ( xS ) = ( cS2043 ) ) &
% 3.33/1.35 ( ![W0:$i]:
% 3.33/1.35 ( ( ( ?[W1:$i]:
% 3.33/1.35 ( ( ( ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz00 @ W1 ) ) &
% 3.33/1.35 ( ![W2:$i]:
% 3.33/1.35 ( ( ( ( aInteger0 @ W2 ) &
% 3.33/1.35 ( ( ?[W3:$i]:
% 3.33/1.35 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 3.33/1.35 ( sdtpldt0 @ W2 @ ( smndt0 @ sz00 ) ) ) &
% 3.33/1.35 ( aInteger0 @ W3 ) ) ) |
% 3.33/1.35 ( aDivisorOf0 @
% 3.33/1.35 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ sz00 ) ) ) |
% 3.33/1.35 ( sdteqdtlpzmzozddtrp0 @ W2 @ sz00 @ W1 ) ) ) =>
% 3.33/1.35 ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz00 @ W1 ) ) ) &
% 3.33/1.35 ( ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz00 @ W1 ) ) =>
% 3.33/1.35 ( ( aInteger0 @ W2 ) &
% 3.33/1.35 ( ?[W3:$i]:
% 3.33/1.35 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 3.33/1.35 ( sdtpldt0 @ W2 @ ( smndt0 @ sz00 ) ) ) &
% 3.33/1.35 ( aInteger0 @ W3 ) ) ) &
% 3.33/1.35 ( aDivisorOf0 @
% 3.33/1.35 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ sz00 ) ) ) &
% 3.33/1.35 ( sdteqdtlpzmzozddtrp0 @ W2 @ sz00 @ W1 ) ) ) ) ) ) =>
% 3.33/1.35 ( ( szAzrzSzezqlpdtcmdtrp0 @ sz00 @ W1 ) = ( W0 ) ) ) &
% 3.33/1.35 ( isPrime0 @ W1 ) & ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) =>
% 3.33/1.35 ( aElementOf0 @ W0 @ xS ) ) &
% 3.33/1.35 ( ( aElementOf0 @ W0 @ xS ) =>
% 3.33/1.35 ( ?[W1:$i]:
% 3.33/1.35 ( ( ( szAzrzSzezqlpdtcmdtrp0 @ sz00 @ W1 ) = ( W0 ) ) &
% 3.33/1.35 ( ![W2:$i]:
% 3.33/1.35 ( ( ( ( aInteger0 @ W2 ) &
% 3.33/1.35 ( ( ?[W3:$i]:
% 3.33/1.35 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 3.33/1.35 ( sdtpldt0 @ W2 @ ( smndt0 @ sz00 ) ) ) &
% 3.33/1.35 ( aInteger0 @ W3 ) ) ) |
% 3.33/1.35 ( aDivisorOf0 @
% 3.33/1.35 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ sz00 ) ) ) |
% 3.33/1.35 ( sdteqdtlpzmzozddtrp0 @ W2 @ sz00 @ W1 ) ) ) =>
% 3.33/1.35 ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz00 @ W1 ) ) ) &
% 3.33/1.35 ( ( aElementOf0 @
% 3.33/1.35 W2 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz00 @ W1 ) ) =>
% 3.33/1.35 ( ( aInteger0 @ W2 ) &
% 3.33/1.35 ( ?[W3:$i]:
% 3.33/1.35 ( ( ( sdtasdt0 @ W1 @ W3 ) =
% 3.33/1.35 ( sdtpldt0 @ W2 @ ( smndt0 @ sz00 ) ) ) &
% 3.33/1.35 ( aInteger0 @ W3 ) ) ) &
% 3.33/1.35 ( aDivisorOf0 @
% 3.33/1.35 W1 @ ( sdtpldt0 @ W2 @ ( smndt0 @ sz00 ) ) ) &
% 3.33/1.35 ( sdteqdtlpzmzozddtrp0 @ W2 @ sz00 @ W1 ) ) ) ) ) &
% 3.33/1.35 ( aSet0 @ ( szAzrzSzezqlpdtcmdtrp0 @ sz00 @ W1 ) ) &
% 3.33/1.35 ( isPrime0 @ W1 ) & ( ( W1 ) != ( sz00 ) ) & ( aInteger0 @ W1 ) ) ) ) ) ) &
% 3.33/1.35 ( aSet0 @ xS ))).
% 3.33/1.35 thf(zip_derived_cl121, plain,
% 3.33/1.35 (![X0 : $i]:
% 3.33/1.35 (((szAzrzSzezqlpdtcmdtrp0 @ sz00 @ (sk__14 @ X0)) = (X0))
% 3.33/1.35 | ~ (aElementOf0 @ X0 @ xS))),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2046])).
% 3.33/1.35 thf(zip_derived_cl1593, plain,
% 3.33/1.35 ((~ (aSet0 @ xS)
% 3.33/1.35 | ~ (isFinite0 @ xS)
% 3.33/1.35 | (isClosed0 @ (sbsmnsldt0 @ xS))
% 3.33/1.35 | ((szAzrzSzezqlpdtcmdtrp0 @ sz00 @ (sk__14 @ (sk__13 @ xS)))
% 3.33/1.35 = (sk__13 @ xS)))),
% 3.33/1.35 inference('s_sup-', [status(thm)], [zip_derived_cl106, zip_derived_cl121])).
% 3.33/1.35 thf(zip_derived_cl110, plain, ( (aSet0 @ xS)),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2046])).
% 3.33/1.35 thf(m__2117, axiom, (isFinite0 @ xS)).
% 3.33/1.35 thf(zip_derived_cl148, plain, ( (isFinite0 @ xS)),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2117])).
% 3.33/1.35 thf(zip_derived_cl177, plain, (~ (isClosed0 @ (sbsmnsldt0 @ xS))),
% 3.33/1.35 inference('cnf', [status(esa)], [zf_stmt_7])).
% 3.33/1.35 thf(zip_derived_cl1610, plain,
% 3.33/1.35 (((szAzrzSzezqlpdtcmdtrp0 @ sz00 @ (sk__14 @ (sk__13 @ xS)))
% 3.33/1.35 = (sk__13 @ xS))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl1593, zip_derived_cl110, zip_derived_cl148,
% 3.33/1.35 zip_derived_cl177])).
% 3.33/1.35 thf(zip_derived_cl1610, plain,
% 3.33/1.35 (((szAzrzSzezqlpdtcmdtrp0 @ sz00 @ (sk__14 @ (sk__13 @ xS)))
% 3.33/1.35 = (sk__13 @ xS))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl1593, zip_derived_cl110, zip_derived_cl148,
% 3.33/1.35 zip_derived_cl177])).
% 3.33/1.35 thf(mArSeqClosed, axiom,
% 3.33/1.35 (![W0:$i,W1:$i]:
% 3.33/1.35 ( ( ( aInteger0 @ W0 ) & ( aInteger0 @ W1 ) & ( ( W1 ) != ( sz00 ) ) ) =>
% 3.33/1.35 ( ( aSubsetOf0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) @ cS1395 ) &
% 3.33/1.35 ( isClosed0 @ ( szAzrzSzezqlpdtcmdtrp0 @ W0 @ W1 ) ) ) ))).
% 3.33/1.35 thf(zip_derived_cl108, plain,
% 3.33/1.35 (![X0 : $i, X1 : $i]:
% 3.33/1.35 (~ (aInteger0 @ X0)
% 3.33/1.35 | ~ (aInteger0 @ X1)
% 3.33/1.35 | ((X1) = (sz00))
% 3.33/1.35 | (aSubsetOf0 @ (szAzrzSzezqlpdtcmdtrp0 @ X0 @ X1) @ cS1395))),
% 3.33/1.35 inference('cnf', [status(esa)], [mArSeqClosed])).
% 3.33/1.35 thf(zip_derived_cl2129, plain,
% 3.33/1.35 ((~ (aInteger0 @ sz00)
% 3.33/1.35 | ~ (aInteger0 @ (sk__14 @ (sk__13 @ xS)))
% 3.33/1.35 | ((sk__14 @ (sk__13 @ xS)) = (sz00))
% 3.33/1.35 | (aSubsetOf0 @ (sk__13 @ xS) @ cS1395))),
% 3.33/1.35 inference('s_sup+', [status(thm)],
% 3.33/1.35 [zip_derived_cl1610, zip_derived_cl108])).
% 3.33/1.35 thf(mIntZero, axiom, (aInteger0 @ sz00)).
% 3.33/1.35 thf(zip_derived_cl1, plain, ( (aInteger0 @ sz00)),
% 3.33/1.35 inference('cnf', [status(esa)], [mIntZero])).
% 3.33/1.35 thf(zip_derived_cl106, plain,
% 3.33/1.35 (![X0 : $i]:
% 3.33/1.35 ( (isClosed0 @ (sbsmnsldt0 @ X0))
% 3.33/1.35 | (aElementOf0 @ (sk__13 @ X0) @ X0)
% 3.33/1.35 | ~ (isFinite0 @ X0)
% 3.33/1.35 | ~ (aSet0 @ X0))),
% 3.33/1.35 inference('cnf', [status(esa)], [mUnionSClosed])).
% 3.33/1.35 thf(zip_derived_cl133, plain,
% 3.33/1.35 (![X0 : $i]: ( (aInteger0 @ (sk__14 @ X0)) | ~ (aElementOf0 @ X0 @ xS))),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2046])).
% 3.33/1.35 thf(zip_derived_cl1596, plain,
% 3.33/1.35 ((~ (aSet0 @ xS)
% 3.33/1.35 | ~ (isFinite0 @ xS)
% 3.33/1.35 | (isClosed0 @ (sbsmnsldt0 @ xS))
% 3.33/1.35 | (aInteger0 @ (sk__14 @ (sk__13 @ xS))))),
% 3.33/1.35 inference('s_sup-', [status(thm)], [zip_derived_cl106, zip_derived_cl133])).
% 3.33/1.35 thf(zip_derived_cl110, plain, ( (aSet0 @ xS)),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2046])).
% 3.33/1.35 thf(zip_derived_cl148, plain, ( (isFinite0 @ xS)),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2117])).
% 3.33/1.35 thf(zip_derived_cl177, plain, (~ (isClosed0 @ (sbsmnsldt0 @ xS))),
% 3.33/1.35 inference('cnf', [status(esa)], [zf_stmt_7])).
% 3.33/1.35 thf(zip_derived_cl1613, plain, ( (aInteger0 @ (sk__14 @ (sk__13 @ xS)))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl1596, zip_derived_cl110, zip_derived_cl148,
% 3.33/1.35 zip_derived_cl177])).
% 3.33/1.35 thf(zip_derived_cl2131, plain,
% 3.33/1.35 ((((sk__14 @ (sk__13 @ xS)) = (sz00))
% 3.33/1.35 | (aSubsetOf0 @ (sk__13 @ xS) @ cS1395))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl2129, zip_derived_cl1, zip_derived_cl1613])).
% 3.33/1.35 thf(zip_derived_cl1610, plain,
% 3.33/1.35 (((szAzrzSzezqlpdtcmdtrp0 @ sz00 @ (sk__14 @ (sk__13 @ xS)))
% 3.33/1.35 = (sk__13 @ xS))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl1593, zip_derived_cl110, zip_derived_cl148,
% 3.33/1.35 zip_derived_cl177])).
% 3.33/1.35 thf(zip_derived_cl109, plain,
% 3.33/1.35 (![X0 : $i, X1 : $i]:
% 3.33/1.35 (~ (aInteger0 @ X0)
% 3.33/1.35 | ~ (aInteger0 @ X1)
% 3.33/1.35 | ((X1) = (sz00))
% 3.33/1.35 | (isClosed0 @ (szAzrzSzezqlpdtcmdtrp0 @ X0 @ X1)))),
% 3.33/1.35 inference('cnf', [status(esa)], [mArSeqClosed])).
% 3.33/1.35 thf(zip_derived_cl1620, plain,
% 3.33/1.35 ((~ (aInteger0 @ sz00)
% 3.33/1.35 | ~ (aInteger0 @ (sk__14 @ (sk__13 @ xS)))
% 3.33/1.35 | ((sk__14 @ (sk__13 @ xS)) = (sz00))
% 3.33/1.35 | (isClosed0 @ (sk__13 @ xS)))),
% 3.33/1.35 inference('s_sup+', [status(thm)],
% 3.33/1.35 [zip_derived_cl1610, zip_derived_cl109])).
% 3.33/1.35 thf(zip_derived_cl1, plain, ( (aInteger0 @ sz00)),
% 3.33/1.35 inference('cnf', [status(esa)], [mIntZero])).
% 3.33/1.35 thf(zip_derived_cl1613, plain, ( (aInteger0 @ (sk__14 @ (sk__13 @ xS)))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl1596, zip_derived_cl110, zip_derived_cl148,
% 3.33/1.35 zip_derived_cl177])).
% 3.33/1.35 thf(zip_derived_cl1622, plain,
% 3.33/1.35 ((((sk__14 @ (sk__13 @ xS)) = (sz00)) | (isClosed0 @ (sk__13 @ xS)))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl1620, zip_derived_cl1, zip_derived_cl1613])).
% 3.33/1.35 thf(zip_derived_cl107, plain,
% 3.33/1.35 (![X0 : $i]:
% 3.33/1.35 ( (isClosed0 @ (sbsmnsldt0 @ X0))
% 3.33/1.35 | ~ (isClosed0 @ (sk__13 @ X0))
% 3.33/1.35 | ~ (aSubsetOf0 @ (sk__13 @ X0) @ cS1395)
% 3.33/1.35 | ~ (isFinite0 @ X0)
% 3.33/1.35 | ~ (aSet0 @ X0))),
% 3.33/1.35 inference('cnf', [status(esa)], [mUnionSClosed])).
% 3.33/1.35 thf(zip_derived_cl1709, plain,
% 3.33/1.35 ((((sk__14 @ (sk__13 @ xS)) = (sz00))
% 3.33/1.35 | (isClosed0 @ (sbsmnsldt0 @ xS))
% 3.33/1.35 | ~ (aSubsetOf0 @ (sk__13 @ xS) @ cS1395)
% 3.33/1.35 | ~ (isFinite0 @ xS)
% 3.33/1.35 | ~ (aSet0 @ xS))),
% 3.33/1.35 inference('s_sup-', [status(thm)],
% 3.33/1.35 [zip_derived_cl1622, zip_derived_cl107])).
% 3.33/1.35 thf(zip_derived_cl177, plain, (~ (isClosed0 @ (sbsmnsldt0 @ xS))),
% 3.33/1.35 inference('cnf', [status(esa)], [zf_stmt_7])).
% 3.33/1.35 thf(zip_derived_cl148, plain, ( (isFinite0 @ xS)),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2117])).
% 3.33/1.35 thf(zip_derived_cl110, plain, ( (aSet0 @ xS)),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2046])).
% 3.33/1.35 thf(zip_derived_cl1710, plain,
% 3.33/1.35 ((((sk__14 @ (sk__13 @ xS)) = (sz00))
% 3.33/1.35 | ~ (aSubsetOf0 @ (sk__13 @ xS) @ cS1395))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl1709, zip_derived_cl177, zip_derived_cl148,
% 3.33/1.35 zip_derived_cl110])).
% 3.33/1.35 thf(zip_derived_cl2132, plain, (((sk__14 @ (sk__13 @ xS)) = (sz00))),
% 3.33/1.35 inference('clc', [status(thm)], [zip_derived_cl2131, zip_derived_cl1710])).
% 3.33/1.35 thf(zip_derived_cl2133, plain,
% 3.33/1.35 (((szAzrzSzezqlpdtcmdtrp0 @ sz00 @ sz00) = (sk__13 @ xS))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl1610, zip_derived_cl2132])).
% 3.33/1.35 thf(zip_derived_cl106, plain,
% 3.33/1.35 (![X0 : $i]:
% 3.33/1.35 ( (isClosed0 @ (sbsmnsldt0 @ X0))
% 3.33/1.35 | (aElementOf0 @ (sk__13 @ X0) @ X0)
% 3.33/1.35 | ~ (isFinite0 @ X0)
% 3.33/1.35 | ~ (aSet0 @ X0))),
% 3.33/1.35 inference('cnf', [status(esa)], [mUnionSClosed])).
% 3.33/1.35 thf(zip_derived_cl2161, plain,
% 3.33/1.35 (( (isClosed0 @ (sbsmnsldt0 @ xS))
% 3.33/1.35 | (aElementOf0 @ (szAzrzSzezqlpdtcmdtrp0 @ sz00 @ sz00) @ xS)
% 3.33/1.35 | ~ (isFinite0 @ xS)
% 3.33/1.35 | ~ (aSet0 @ xS))),
% 3.33/1.35 inference('s_sup+', [status(thm)],
% 3.33/1.35 [zip_derived_cl2133, zip_derived_cl106])).
% 3.33/1.35 thf(zip_derived_cl148, plain, ( (isFinite0 @ xS)),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2117])).
% 3.33/1.35 thf(zip_derived_cl110, plain, ( (aSet0 @ xS)),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2046])).
% 3.33/1.35 thf(zip_derived_cl2163, plain,
% 3.33/1.35 (( (isClosed0 @ (sbsmnsldt0 @ xS))
% 3.33/1.35 | (aElementOf0 @ (szAzrzSzezqlpdtcmdtrp0 @ sz00 @ sz00) @ xS))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl2161, zip_derived_cl148, zip_derived_cl110])).
% 3.33/1.35 thf(zip_derived_cl2132, plain, (((sk__14 @ (sk__13 @ xS)) = (sz00))),
% 3.33/1.35 inference('clc', [status(thm)], [zip_derived_cl2131, zip_derived_cl1710])).
% 3.33/1.35 thf(zip_derived_cl132, plain,
% 3.33/1.35 (![X0 : $i]: (((sk__14 @ X0) != (sz00)) | ~ (aElementOf0 @ X0 @ xS))),
% 3.33/1.35 inference('cnf', [status(esa)], [m__2046])).
% 3.33/1.35 thf(zip_derived_cl2139, plain,
% 3.33/1.35 ((((sz00) != (sz00)) | ~ (aElementOf0 @ (sk__13 @ xS) @ xS))),
% 3.33/1.35 inference('s_sup-', [status(thm)],
% 3.33/1.35 [zip_derived_cl2132, zip_derived_cl132])).
% 3.33/1.35 thf(zip_derived_cl2141, plain, (~ (aElementOf0 @ (sk__13 @ xS) @ xS)),
% 3.33/1.35 inference('simplify', [status(thm)], [zip_derived_cl2139])).
% 3.33/1.35 thf(zip_derived_cl2133, plain,
% 3.33/1.35 (((szAzrzSzezqlpdtcmdtrp0 @ sz00 @ sz00) = (sk__13 @ xS))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl1610, zip_derived_cl2132])).
% 3.33/1.35 thf(zip_derived_cl2165, plain,
% 3.33/1.35 (~ (aElementOf0 @ (szAzrzSzezqlpdtcmdtrp0 @ sz00 @ sz00) @ xS)),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl2141, zip_derived_cl2133])).
% 3.33/1.35 thf(zip_derived_cl2196, plain, ( (isClosed0 @ (sbsmnsldt0 @ xS))),
% 3.33/1.35 inference('demod', [status(thm)],
% 3.33/1.35 [zip_derived_cl2163, zip_derived_cl2165])).
% 3.33/1.35 thf(zip_derived_cl2197, plain, ($false),
% 3.33/1.35 inference('demod', [status(thm)], [zip_derived_cl177, zip_derived_cl2196])).
% 3.33/1.35
% 3.33/1.35 % SZS output end Refutation
% 3.33/1.35
% 3.33/1.35
% 3.33/1.35 % Terminating...
% 3.99/1.55 % Runner terminated.
% 3.99/1.57 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------