%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NUM528+3 : 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.GWjNBQmLQn true
% Computer : n006.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:20 PM UTC 2025
% Result : Theorem 44.34s 6.97s
% Output : Refutation 44.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : NUM528+3 : TPTP v9.2.0. Released v4.0.0.
% 0.04/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.GWjNBQmLQn true
% 0.14/0.35 % Computer : n006.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 1 16:36:08 EDT 2025
% 0.14/0.35 % CPUTime :
% 0.14/0.35 % Running portfolio for 300 s
% 0.14/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.36 % Number of cores: 8
% 0.22/0.36 % Python version: Python 3.6.8
% 0.22/0.36 % Running in FO mode
% 0.56/0.66 % Total configuration time : 435
% 0.56/0.66 % Estimated wc time : 1092
% 0.56/0.66 % Estimated cpu time (7 cpus) : 156.0
% 0.56/0.71 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.56/0.72 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.56/0.74 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 44.34/6.97 % Solved by fo/fo3_bce.sh.
% 44.34/6.97 % BCE start: 108
% 44.34/6.97 % BCE eliminated: 1
% 44.34/6.97 % PE start: 107
% 44.34/6.97 logic: eq
% 44.34/6.97 % PE eliminated: -9
% 44.34/6.97 % done 4099 iterations in 6.209s
% 44.34/6.97 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 44.34/6.97 % SZS output start Refutation
% 44.34/6.97 thf(aNaturalNumber0_type, type, aNaturalNumber0: $i > $o).
% 44.34/6.97 thf(sdtsldt0_type, type, sdtsldt0: $i > $i > $i).
% 44.34/6.97 thf(sk__8_type, type, sk__8: $i).
% 44.34/6.97 thf(sz10_type, type, sz10: $i).
% 44.34/6.97 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 44.34/6.97 thf(sdtasdt0_type, type, sdtasdt0: $i > $i > $i).
% 44.34/6.97 thf(sk__7_type, type, sk__7: $i).
% 44.34/6.97 thf(isPrime0_type, type, isPrime0: $i > $o).
% 44.34/6.97 thf(xn_type, type, xn: $i).
% 44.34/6.97 thf(zip_tseitin_0_type, type, zip_tseitin_0: $o).
% 44.34/6.97 thf(sz00_type, type, sz00: $i).
% 44.34/6.97 thf(xq_type, type, xq: $i).
% 44.34/6.97 thf(xm_type, type, xm: $i).
% 44.34/6.97 thf(doDivides0_type, type, doDivides0: $i > $i > $o).
% 44.34/6.97 thf(xp_type, type, xp: $i).
% 44.34/6.97 thf(sdtlseqdt0_type, type, sdtlseqdt0: $i > $i > $o).
% 44.34/6.97 thf(zip_tseitin_2_type, type, zip_tseitin_2: $o).
% 44.34/6.97 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $o).
% 44.34/6.97 thf(m__3059, axiom,
% 44.34/6.97 (( ( xq ) = ( sdtsldt0 @ xn @ xp ) ) &
% 44.34/6.97 ( ( xn ) = ( sdtasdt0 @ xp @ xq ) ) & ( aNaturalNumber0 @ xq ))).
% 44.34/6.97 thf(zip_derived_cl96, plain, (((xn) = (sdtasdt0 @ xp @ xq))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3059])).
% 44.34/6.97 thf(mMulAsso, axiom,
% 44.34/6.97 (![W0:$i,W1:$i,W2:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W0 ) & ( aNaturalNumber0 @ W1 ) &
% 44.34/6.97 ( aNaturalNumber0 @ W2 ) ) =>
% 44.34/6.97 ( ( sdtasdt0 @ ( sdtasdt0 @ W0 @ W1 ) @ W2 ) =
% 44.34/6.97 ( sdtasdt0 @ W0 @ ( sdtasdt0 @ W1 @ W2 ) ) ) ))).
% 44.34/6.97 thf(zip_derived_cl11, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X2)
% 44.34/6.97 | ((sdtasdt0 @ (sdtasdt0 @ X1 @ X0) @ X2)
% 44.34/6.97 = (sdtasdt0 @ X1 @ (sdtasdt0 @ X0 @ X2))))),
% 44.34/6.97 inference('cnf', [status(esa)], [mMulAsso])).
% 44.34/6.97 thf(zip_derived_cl1125, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtasdt0 @ xn @ X0) = (sdtasdt0 @ xp @ (sdtasdt0 @ xq @ X0)))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ xp)
% 44.34/6.97 | ~ (aNaturalNumber0 @ xq))),
% 44.34/6.97 inference('sup+', [status(thm)], [zip_derived_cl96, zip_derived_cl11])).
% 44.34/6.97 thf(m__2987, axiom,
% 44.34/6.97 (( ( xp ) != ( sz00 ) ) & ( ( xm ) != ( sz00 ) ) &
% 44.34/6.97 ( ( xn ) != ( sz00 ) ) & ( aNaturalNumber0 @ xp ) &
% 44.34/6.97 ( aNaturalNumber0 @ xm ) & ( aNaturalNumber0 @ xn ))).
% 44.34/6.97 thf(zip_derived_cl74, plain, ( (aNaturalNumber0 @ xp)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl97, plain, ( (aNaturalNumber0 @ xq)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3059])).
% 44.34/6.97 thf(zip_derived_cl1143, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtasdt0 @ xn @ X0) = (sdtasdt0 @ xp @ (sdtasdt0 @ xq @ X0)))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl1125, zip_derived_cl74, zip_derived_cl97])).
% 44.34/6.97 thf(m__3082, axiom,
% 44.34/6.97 (( sdtasdt0 @ xm @ xm ) = ( sdtasdt0 @ xp @ ( sdtasdt0 @ xq @ xq ) ))).
% 44.34/6.97 thf(zip_derived_cl98, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xp @ (sdtasdt0 @ xq @ xq)))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3082])).
% 44.34/6.97 thf(zip_derived_cl11216, plain,
% 44.34/6.97 ((((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xn @ xq))
% 44.34/6.97 | ~ (aNaturalNumber0 @ xq))),
% 44.34/6.97 inference('sup+', [status(thm)], [zip_derived_cl1143, zip_derived_cl98])).
% 44.34/6.97 thf(zip_derived_cl97, plain, ( (aNaturalNumber0 @ xq)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3059])).
% 44.34/6.97 thf(zip_derived_cl11294, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl11216, zip_derived_cl97])).
% 44.34/6.97 thf(m__3046, axiom,
% 44.34/6.97 (( doDivides0 @ xp @ xn ) &
% 44.34/6.97 ( ?[W0:$i]:
% 44.34/6.97 ( ( ( xn ) = ( sdtasdt0 @ xp @ W0 ) ) & ( aNaturalNumber0 @ W0 ) ) ) &
% 44.34/6.97 ( doDivides0 @ xp @ ( sdtasdt0 @ xn @ xn ) ) &
% 44.34/6.97 ( ?[W0:$i]:
% 44.34/6.97 ( ( ( sdtasdt0 @ xn @ xn ) = ( sdtasdt0 @ xp @ W0 ) ) &
% 44.34/6.97 ( aNaturalNumber0 @ W0 ) ) ))).
% 44.34/6.97 thf(zip_derived_cl89, plain,
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) = (sdtasdt0 @ xp @ sk__7))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3046])).
% 44.34/6.97 thf(m__3014, axiom,
% 44.34/6.97 (( sdtasdt0 @ xp @ ( sdtasdt0 @ xm @ xm ) ) = ( sdtasdt0 @ xn @ xn ))).
% 44.34/6.97 thf(zip_derived_cl84, plain,
% 44.34/6.97 (((sdtasdt0 @ xp @ (sdtasdt0 @ xm @ xm)) = (sdtasdt0 @ xn @ xn))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3014])).
% 44.34/6.97 thf(mMulCanc, axiom,
% 44.34/6.97 (![W0:$i]:
% 44.34/6.97 ( ( aNaturalNumber0 @ W0 ) =>
% 44.34/6.97 ( ( ( W0 ) != ( sz00 ) ) =>
% 44.34/6.97 ( ![W1:$i,W2:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W1 ) & ( aNaturalNumber0 @ W2 ) ) =>
% 44.34/6.97 ( ( ( ( sdtasdt0 @ W0 @ W1 ) = ( sdtasdt0 @ W0 @ W2 ) ) |
% 44.34/6.97 ( ( sdtasdt0 @ W1 @ W0 ) = ( sdtasdt0 @ W2 @ W0 ) ) ) =>
% 44.34/6.97 ( ( W1 ) = ( W2 ) ) ) ) ) ) ))).
% 44.34/6.97 thf(zip_derived_cl21, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 44.34/6.97 (((X0) = (sz00))
% 44.34/6.97 | ((sdtasdt0 @ X0 @ X2) != (sdtasdt0 @ X0 @ X1))
% 44.34/6.97 | ((X2) = (X1))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X2)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0))),
% 44.34/6.97 inference('cnf', [status(esa)], [mMulCanc])).
% 44.34/6.97 thf(zip_derived_cl1577, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ xp @ X0))
% 44.34/6.97 | ~ (aNaturalNumber0 @ xp)
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtasdt0 @ xm @ xm))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ((sdtasdt0 @ xm @ xm) = (X0))
% 44.34/6.97 | ((xp) = (sz00)))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl84, zip_derived_cl21])).
% 44.34/6.97 thf(zip_derived_cl74, plain, ( (aNaturalNumber0 @ xp)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl1612, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ xp @ X0))
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtasdt0 @ xm @ xm))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ((sdtasdt0 @ xm @ xm) = (X0))
% 44.34/6.97 | ((xp) = (sz00)))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl1577, zip_derived_cl74])).
% 44.34/6.97 thf(zip_derived_cl71, plain, (((xp) != (sz00))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl1613, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ xp @ X0))
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtasdt0 @ xm @ xm))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ((sdtasdt0 @ xm @ xm) = (X0)))),
% 44.34/6.97 inference('simplify_reflect-', [status(thm)],
% 44.34/6.97 [zip_derived_cl1612, zip_derived_cl71])).
% 44.34/6.97 thf(zip_derived_cl11294, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl11216, zip_derived_cl97])).
% 44.34/6.97 thf(mSortsB_02, axiom,
% 44.34/6.97 (![W0:$i,W1:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W0 ) & ( aNaturalNumber0 @ W1 ) ) =>
% 44.34/6.97 ( aNaturalNumber0 @ ( sdtasdt0 @ W0 @ W1 ) ) ))).
% 44.34/6.97 thf(zip_derived_cl5, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | (aNaturalNumber0 @ (sdtasdt0 @ X0 @ X1)))),
% 44.34/6.97 inference('cnf', [status(esa)], [mSortsB_02])).
% 44.34/6.97 thf(zip_derived_cl98, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xp @ (sdtasdt0 @ xq @ xq)))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3082])).
% 44.34/6.97 thf(zip_derived_cl5, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | (aNaturalNumber0 @ (sdtasdt0 @ X0 @ X1)))),
% 44.34/6.97 inference('cnf', [status(esa)], [mSortsB_02])).
% 44.34/6.97 thf(zip_derived_cl1104, plain,
% 44.34/6.97 (( (aNaturalNumber0 @ (sdtasdt0 @ xm @ xm))
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtasdt0 @ xq @ xq))
% 44.34/6.97 | ~ (aNaturalNumber0 @ xp))),
% 44.34/6.97 inference('sup+', [status(thm)], [zip_derived_cl98, zip_derived_cl5])).
% 44.34/6.97 thf(zip_derived_cl74, plain, ( (aNaturalNumber0 @ xp)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl1109, plain,
% 44.34/6.97 (( (aNaturalNumber0 @ (sdtasdt0 @ xm @ xm))
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtasdt0 @ xq @ xq)))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl1104, zip_derived_cl74])).
% 44.34/6.97 thf(zip_derived_cl9462, plain,
% 44.34/6.97 ((~ (aNaturalNumber0 @ xq)
% 44.34/6.97 | ~ (aNaturalNumber0 @ xq)
% 44.34/6.97 | (aNaturalNumber0 @ (sdtasdt0 @ xm @ xm)))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl1109])).
% 44.34/6.97 thf(zip_derived_cl97, plain, ( (aNaturalNumber0 @ xq)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3059])).
% 44.34/6.97 thf(zip_derived_cl97, plain, ( (aNaturalNumber0 @ xq)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3059])).
% 44.34/6.97 thf(zip_derived_cl9465, plain, ( (aNaturalNumber0 @ (sdtasdt0 @ xm @ xm))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl9462, zip_derived_cl97, zip_derived_cl97])).
% 44.34/6.97 thf(zip_derived_cl11294, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl11216, zip_derived_cl97])).
% 44.34/6.97 thf(zip_derived_cl11665, plain, ( (aNaturalNumber0 @ (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl9465, zip_derived_cl11294])).
% 44.34/6.97 thf(zip_derived_cl11294, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl11216, zip_derived_cl97])).
% 44.34/6.97 thf(zip_derived_cl33444, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ xp @ X0))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ((sdtasdt0 @ xn @ xq) = (X0)))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl1613, zip_derived_cl11294, zip_derived_cl11665,
% 44.34/6.97 zip_derived_cl11294])).
% 44.34/6.97 thf(zip_derived_cl33465, plain,
% 44.34/6.97 ((((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ xn @ xn))
% 44.34/6.97 | ((sdtasdt0 @ xn @ xq) = (sk__7))
% 44.34/6.97 | ~ (aNaturalNumber0 @ sk__7))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl89, zip_derived_cl33444])).
% 44.34/6.97 thf(zip_derived_cl90, plain, ( (aNaturalNumber0 @ sk__7)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3046])).
% 44.34/6.97 thf(zip_derived_cl33487, plain,
% 44.34/6.97 ((((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ xn @ xn))
% 44.34/6.97 | ((sdtasdt0 @ xn @ xq) = (sk__7)))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl33465, zip_derived_cl90])).
% 44.34/6.97 thf(zip_derived_cl33488, plain, (((sdtasdt0 @ xn @ xq) = (sk__7))),
% 44.34/6.97 inference('simplify', [status(thm)], [zip_derived_cl33487])).
% 44.34/6.97 thf(zip_derived_cl33489, plain, (((sdtasdt0 @ xm @ xm) = (sk__7))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl11294, zip_derived_cl33488])).
% 44.34/6.97 thf(zip_derived_cl11294, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl11216, zip_derived_cl97])).
% 44.34/6.97 thf(zip_derived_cl75, plain, ( (aNaturalNumber0 @ xm)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl76, plain, ( (aNaturalNumber0 @ xn)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(mLETotal, axiom,
% 44.34/6.97 (![W0:$i,W1:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W0 ) & ( aNaturalNumber0 @ W1 ) ) =>
% 44.34/6.97 ( ( sdtlseqdt0 @ W0 @ W1 ) |
% 44.34/6.97 ( ( ( W1 ) != ( W0 ) ) & ( sdtlseqdt0 @ W1 @ W0 ) ) ) ))).
% 44.34/6.97 thf(zip_derived_cl35, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | (sdtlseqdt0 @ X0 @ X1)
% 44.34/6.97 | (sdtlseqdt0 @ X1 @ X0))),
% 44.34/6.97 inference('cnf', [status(esa)], [mLETotal])).
% 44.34/6.97 thf(zip_derived_cl1096, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 ( (sdtlseqdt0 @ X0 @ xn)
% 44.34/6.97 | (sdtlseqdt0 @ xn @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl76, zip_derived_cl35])).
% 44.34/6.97 thf(zip_derived_cl2216, plain,
% 44.34/6.97 (( (sdtlseqdt0 @ xn @ xm) | (sdtlseqdt0 @ xm @ xn))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl75, zip_derived_cl1096])).
% 44.34/6.97 thf(m__, conjecture,
% 44.34/6.97 (( ( xm ) != ( xn ) ) &
% 44.34/6.97 ( ( sdtlseqdt0 @ xm @ xn ) |
% 44.34/6.97 ( ?[W0:$i]:
% 44.34/6.97 ( ( ( sdtpldt0 @ xm @ W0 ) = ( xn ) ) & ( aNaturalNumber0 @ W0 ) ) ) ))).
% 44.34/6.97 thf(zf_stmt_0, negated_conjecture,
% 44.34/6.97 (~( ( ( xm ) != ( xn ) ) &
% 44.34/6.97 ( ( sdtlseqdt0 @ xm @ xn ) |
% 44.34/6.97 ( ?[W0:$i]:
% 44.34/6.97 ( ( ( sdtpldt0 @ xm @ W0 ) = ( xn ) ) & ( aNaturalNumber0 @ W0 ) ) ) ) )),
% 44.34/6.97 inference('cnf.neg', [status(esa)], [m__])).
% 44.34/6.97 thf(zip_derived_cl106, plain, ((((xm) = (xn)) | ~ (sdtlseqdt0 @ xm @ xn))),
% 44.34/6.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 44.34/6.97 thf(zip_derived_cl2234, plain, (( (sdtlseqdt0 @ xn @ xm) | ((xm) = (xn)))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl2216, zip_derived_cl106])).
% 44.34/6.97 thf(m__3152, axiom,
% 44.34/6.97 (( ( sdtlseqdt0 @ xn @ xm ) |
% 44.34/6.97 ( ?[W0:$i]:
% 44.34/6.97 ( ( aNaturalNumber0 @ W0 ) & ( ( sdtpldt0 @ xn @ W0 ) = ( xm ) ) ) ) ) =>
% 44.34/6.97 ( ( sdtlseqdt0 @ ( sdtasdt0 @ xn @ xn ) @ ( sdtasdt0 @ xm @ xm ) ) &
% 44.34/6.97 ( ?[W0:$i]:
% 44.34/6.97 ( ( aNaturalNumber0 @ W0 ) &
% 44.34/6.97 ( ( sdtpldt0 @ ( sdtasdt0 @ xn @ xn ) @ W0 ) =
% 44.34/6.97 ( sdtasdt0 @ xm @ xm ) ) ) ) ))).
% 44.34/6.97 thf(zf_stmt_1, axiom,
% 44.34/6.97 (( ( ?[W0:$i]:
% 44.34/6.97 ( ( ( sdtpldt0 @ xn @ W0 ) = ( xm ) ) & ( aNaturalNumber0 @ W0 ) ) ) |
% 44.34/6.97 ( sdtlseqdt0 @ xn @ xm ) ) =>
% 44.34/6.97 ( zip_tseitin_0 ))).
% 44.34/6.97 thf(zip_derived_cl100, plain,
% 44.34/6.97 (( (zip_tseitin_0) | ~ (sdtlseqdt0 @ xn @ xm))),
% 44.34/6.97 inference('cnf', [status(esa)], [zf_stmt_1])).
% 44.34/6.97 thf(zf_stmt_2, type, zip_tseitin_2 : $o).
% 44.34/6.97 thf(zf_stmt_3, axiom,
% 44.34/6.97 (( zip_tseitin_2 ) =>
% 44.34/6.97 ( ( ?[W0:$i]: ( zip_tseitin_1 @ W0 ) ) &
% 44.34/6.97 ( sdtlseqdt0 @ ( sdtasdt0 @ xn @ xn ) @ ( sdtasdt0 @ xm @ xm ) ) ))).
% 44.34/6.97 thf(zf_stmt_4, type, zip_tseitin_1 : $i > $o).
% 44.34/6.97 thf(zf_stmt_5, axiom,
% 44.34/6.97 (![W0:$i]:
% 44.34/6.97 ( ( zip_tseitin_1 @ W0 ) =>
% 44.34/6.97 ( ( ( sdtpldt0 @ ( sdtasdt0 @ xn @ xn ) @ W0 ) = ( sdtasdt0 @ xm @ xm ) ) &
% 44.34/6.97 ( aNaturalNumber0 @ W0 ) ) ))).
% 44.34/6.97 thf(zf_stmt_6, type, zip_tseitin_0 : $o).
% 44.34/6.97 thf(zf_stmt_7, axiom, (( zip_tseitin_0 ) => ( zip_tseitin_2 ))).
% 44.34/6.97 thf(zip_derived_cl105, plain, (( (zip_tseitin_2) | ~ (zip_tseitin_0))),
% 44.34/6.97 inference('cnf', [status(esa)], [zf_stmt_7])).
% 44.34/6.97 thf(zip_derived_cl103, plain,
% 44.34/6.97 (( (zip_tseitin_1 @ sk__8) | ~ (zip_tseitin_2))),
% 44.34/6.97 inference('cnf', [status(esa)], [zf_stmt_3])).
% 44.34/6.97 thf(zip_derived_cl826, plain,
% 44.34/6.97 ((~ (zip_tseitin_0) | (zip_tseitin_1 @ sk__8))),
% 44.34/6.97 inference('dp-resolution', [status(thm)],
% 44.34/6.97 [zip_derived_cl105, zip_derived_cl103])).
% 44.34/6.97 thf(zip_derived_cl101, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtpldt0 @ (sdtasdt0 @ xn @ xn) @ X0) = (sdtasdt0 @ xm @ xm))
% 44.34/6.97 | ~ (zip_tseitin_1 @ X0))),
% 44.34/6.97 inference('cnf', [status(esa)], [zf_stmt_5])).
% 44.34/6.97 thf(zip_derived_cl828, plain,
% 44.34/6.97 ((~ (zip_tseitin_0)
% 44.34/6.97 | ((sdtpldt0 @ (sdtasdt0 @ xn @ xn) @ sk__8) = (sdtasdt0 @ xm @ xm)))),
% 44.34/6.97 inference('dp-resolution', [status(thm)],
% 44.34/6.97 [zip_derived_cl826, zip_derived_cl101])).
% 44.34/6.97 thf(zip_derived_cl834, plain,
% 44.34/6.97 ((~ (sdtlseqdt0 @ xn @ xm)
% 44.34/6.97 | ((sdtpldt0 @ (sdtasdt0 @ xn @ xn) @ sk__8) = (sdtasdt0 @ xm @ xm)))),
% 44.34/6.97 inference('dp-resolution', [status(thm)],
% 44.34/6.97 [zip_derived_cl100, zip_derived_cl828])).
% 44.34/6.97 thf(zip_derived_cl2314, plain,
% 44.34/6.97 ((((xm) = (xn))
% 44.34/6.97 | ((sdtpldt0 @ (sdtasdt0 @ xn @ xn) @ sk__8) = (sdtasdt0 @ xm @ xm)))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl2234, zip_derived_cl834])).
% 44.34/6.97 thf(zip_derived_cl11719, plain,
% 44.34/6.97 ((((sdtpldt0 @ (sdtasdt0 @ xn @ xn) @ sk__8) = (sdtasdt0 @ xn @ xq))
% 44.34/6.97 | ((xm) = (xn)))),
% 44.34/6.97 inference('sup+', [status(thm)],
% 44.34/6.97 [zip_derived_cl11294, zip_derived_cl2314])).
% 44.34/6.97 thf(zip_derived_cl33488, plain, (((sdtasdt0 @ xn @ xq) = (sk__7))),
% 44.34/6.97 inference('simplify', [status(thm)], [zip_derived_cl33487])).
% 44.34/6.97 thf(zip_derived_cl33493, plain,
% 44.34/6.97 ((((sdtpldt0 @ (sdtasdt0 @ xn @ xn) @ sk__8) = (sk__7)) | ((xm) = (xn)))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl11719, zip_derived_cl33488])).
% 44.34/6.97 thf(mDefLE, axiom,
% 44.34/6.97 (![W0:$i,W1:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W0 ) & ( aNaturalNumber0 @ W1 ) ) =>
% 44.34/6.97 ( ( sdtlseqdt0 @ W0 @ W1 ) <=>
% 44.34/6.97 ( ?[W2:$i]:
% 44.34/6.97 ( ( ( sdtpldt0 @ W0 @ W2 ) = ( W1 ) ) & ( aNaturalNumber0 @ W2 ) ) ) ) ))).
% 44.34/6.97 thf(zip_derived_cl27, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | (sdtlseqdt0 @ X0 @ X1)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X2)
% 44.34/6.97 | ((sdtpldt0 @ X0 @ X2) != (X1)))),
% 44.34/6.97 inference('cnf', [status(esa)], [mDefLE])).
% 44.34/6.97 thf(zip_derived_cl1156, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | (sdtlseqdt0 @ X1 @ (sdtpldt0 @ X1 @ X0))
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtpldt0 @ X1 @ X0))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1))),
% 44.34/6.97 inference('eq_res', [status(thm)], [zip_derived_cl27])).
% 44.34/6.97 thf(mSortsB, axiom,
% 44.34/6.97 (![W0:$i,W1:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W0 ) & ( aNaturalNumber0 @ W1 ) ) =>
% 44.34/6.97 ( aNaturalNumber0 @ ( sdtpldt0 @ W0 @ W1 ) ) ))).
% 44.34/6.97 thf(zip_derived_cl4, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | (aNaturalNumber0 @ (sdtpldt0 @ X0 @ X1)))),
% 44.34/6.97 inference('cnf', [status(esa)], [mSortsB])).
% 44.34/6.97 thf(zip_derived_cl12951, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | (sdtlseqdt0 @ X1 @ (sdtpldt0 @ X1 @ X0))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0))),
% 44.34/6.97 inference('clc', [status(thm)], [zip_derived_cl1156, zip_derived_cl4])).
% 44.34/6.97 thf(zip_derived_cl34800, plain,
% 44.34/6.97 (( (sdtlseqdt0 @ (sdtasdt0 @ xn @ xn) @ sk__7)
% 44.34/6.97 | ((xm) = (xn))
% 44.34/6.97 | ~ (aNaturalNumber0 @ sk__8)
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtasdt0 @ xn @ xn)))),
% 44.34/6.97 inference('sup+', [status(thm)],
% 44.34/6.97 [zip_derived_cl33493, zip_derived_cl12951])).
% 44.34/6.97 thf(zip_derived_cl2234, plain, (( (sdtlseqdt0 @ xn @ xm) | ((xm) = (xn)))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl2216, zip_derived_cl106])).
% 44.34/6.97 thf(zip_derived_cl100, plain,
% 44.34/6.97 (( (zip_tseitin_0) | ~ (sdtlseqdt0 @ xn @ xm))),
% 44.34/6.97 inference('cnf', [status(esa)], [zf_stmt_1])).
% 44.34/6.97 thf(zip_derived_cl826, plain,
% 44.34/6.97 ((~ (zip_tseitin_0) | (zip_tseitin_1 @ sk__8))),
% 44.34/6.97 inference('dp-resolution', [status(thm)],
% 44.34/6.97 [zip_derived_cl105, zip_derived_cl103])).
% 44.34/6.97 thf(zip_derived_cl102, plain,
% 44.34/6.97 (![X0 : $i]: ( (aNaturalNumber0 @ X0) | ~ (zip_tseitin_1 @ X0))),
% 44.34/6.97 inference('cnf', [status(esa)], [zf_stmt_5])).
% 44.34/6.97 thf(zip_derived_cl829, plain,
% 44.34/6.97 ((~ (zip_tseitin_0) | (aNaturalNumber0 @ sk__8))),
% 44.34/6.97 inference('dp-resolution', [status(thm)],
% 44.34/6.97 [zip_derived_cl826, zip_derived_cl102])).
% 44.34/6.97 thf(zip_derived_cl835, plain,
% 44.34/6.97 ((~ (sdtlseqdt0 @ xn @ xm) | (aNaturalNumber0 @ sk__8))),
% 44.34/6.97 inference('dp-resolution', [status(thm)],
% 44.34/6.97 [zip_derived_cl100, zip_derived_cl829])).
% 44.34/6.97 thf(zip_derived_cl2315, plain,
% 44.34/6.97 ((((xm) = (xn)) | (aNaturalNumber0 @ sk__8))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl2234, zip_derived_cl835])).
% 44.34/6.97 thf(m_AddZero, axiom,
% 44.34/6.97 (![W0:$i]:
% 44.34/6.97 ( ( aNaturalNumber0 @ W0 ) =>
% 44.34/6.97 ( ( ( sdtpldt0 @ W0 @ sz00 ) = ( W0 ) ) &
% 44.34/6.97 ( ( W0 ) = ( sdtpldt0 @ sz00 @ W0 ) ) ) ))).
% 44.34/6.97 thf(zip_derived_cl8, plain,
% 44.34/6.97 (![X0 : $i]: (((sdtpldt0 @ X0 @ sz00) = (X0)) | ~ (aNaturalNumber0 @ X0))),
% 44.34/6.97 inference('cnf', [status(esa)], [m_AddZero])).
% 44.34/6.97 thf(zip_derived_cl99, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 ( (zip_tseitin_0)
% 44.34/6.97 | ((sdtpldt0 @ xn @ X0) != (xm))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0))),
% 44.34/6.97 inference('cnf', [status(esa)], [zf_stmt_1])).
% 44.34/6.97 thf(zip_derived_cl829, plain,
% 44.34/6.97 ((~ (zip_tseitin_0) | (aNaturalNumber0 @ sk__8))),
% 44.34/6.97 inference('dp-resolution', [status(thm)],
% 44.34/6.97 [zip_derived_cl826, zip_derived_cl102])).
% 44.34/6.97 thf(zip_derived_cl832, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ((sdtpldt0 @ xn @ X0) != (xm))
% 44.34/6.97 | (aNaturalNumber0 @ sk__8))),
% 44.34/6.97 inference('dp-resolution', [status(thm)],
% 44.34/6.97 [zip_derived_cl99, zip_derived_cl829])).
% 44.34/6.97 thf(zip_derived_cl882, plain,
% 44.34/6.97 ((((xn) != (xm))
% 44.34/6.97 | ~ (aNaturalNumber0 @ xn)
% 44.34/6.97 | (aNaturalNumber0 @ sk__8)
% 44.34/6.97 | ~ (aNaturalNumber0 @ sz00))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl8, zip_derived_cl832])).
% 44.34/6.97 thf(zip_derived_cl76, plain, ( (aNaturalNumber0 @ xn)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(mSortsC, axiom, (aNaturalNumber0 @ sz00)).
% 44.34/6.97 thf(zip_derived_cl1, plain, ( (aNaturalNumber0 @ sz00)),
% 44.34/6.97 inference('cnf', [status(esa)], [mSortsC])).
% 44.34/6.97 thf(zip_derived_cl886, plain,
% 44.34/6.97 ((((xn) != (xm)) | (aNaturalNumber0 @ sk__8))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl882, zip_derived_cl76, zip_derived_cl1])).
% 44.34/6.97 thf(zip_derived_cl2321, plain, ( (aNaturalNumber0 @ sk__8)),
% 44.34/6.97 inference('clc', [status(thm)], [zip_derived_cl2315, zip_derived_cl886])).
% 44.34/6.97 thf(zip_derived_cl89, plain,
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) = (sdtasdt0 @ xp @ sk__7))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3046])).
% 44.34/6.97 thf(zip_derived_cl5, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | (aNaturalNumber0 @ (sdtasdt0 @ X0 @ X1)))),
% 44.34/6.97 inference('cnf', [status(esa)], [mSortsB_02])).
% 44.34/6.97 thf(zip_derived_cl898, plain,
% 44.34/6.97 (( (aNaturalNumber0 @ (sdtasdt0 @ xn @ xn))
% 44.34/6.97 | ~ (aNaturalNumber0 @ sk__7)
% 44.34/6.97 | ~ (aNaturalNumber0 @ xp))),
% 44.34/6.97 inference('sup+', [status(thm)], [zip_derived_cl89, zip_derived_cl5])).
% 44.34/6.97 thf(zip_derived_cl90, plain, ( (aNaturalNumber0 @ sk__7)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3046])).
% 44.34/6.97 thf(zip_derived_cl74, plain, ( (aNaturalNumber0 @ xp)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl899, plain, ( (aNaturalNumber0 @ (sdtasdt0 @ xn @ xn))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl898, zip_derived_cl90, zip_derived_cl74])).
% 44.34/6.97 thf(zip_derived_cl34875, plain,
% 44.34/6.97 (( (sdtlseqdt0 @ (sdtasdt0 @ xn @ xn) @ sk__7) | ((xm) = (xn)))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl34800, zip_derived_cl2321, zip_derived_cl899])).
% 44.34/6.97 thf(mLEAsym, axiom,
% 44.34/6.97 (![W0:$i,W1:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W0 ) & ( aNaturalNumber0 @ W1 ) ) =>
% 44.34/6.97 ( ( ( sdtlseqdt0 @ W0 @ W1 ) & ( sdtlseqdt0 @ W1 @ W0 ) ) =>
% 44.34/6.97 ( ( W0 ) = ( W1 ) ) ) ))).
% 44.34/6.97 thf(zip_derived_cl32, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | ((X0) = (X1))
% 44.34/6.97 | ~ (sdtlseqdt0 @ X1 @ X0)
% 44.34/6.97 | ~ (sdtlseqdt0 @ X0 @ X1))),
% 44.34/6.97 inference('cnf', [status(esa)], [mLEAsym])).
% 44.34/6.97 thf(zip_derived_cl45232, plain,
% 44.34/6.97 ((((xm) = (xn))
% 44.34/6.97 | ~ (sdtlseqdt0 @ sk__7 @ (sdtasdt0 @ xn @ xn))
% 44.34/6.97 | ((sk__7) = (sdtasdt0 @ xn @ xn))
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtasdt0 @ xn @ xn))
% 44.34/6.97 | ~ (aNaturalNumber0 @ sk__7))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl34875, zip_derived_cl32])).
% 44.34/6.97 thf(zip_derived_cl899, plain, ( (aNaturalNumber0 @ (sdtasdt0 @ xn @ xn))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl898, zip_derived_cl90, zip_derived_cl74])).
% 44.34/6.97 thf(zip_derived_cl90, plain, ( (aNaturalNumber0 @ sk__7)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3046])).
% 44.34/6.97 thf(zip_derived_cl45249, plain,
% 44.34/6.97 ((((xm) = (xn))
% 44.34/6.97 | ~ (sdtlseqdt0 @ sk__7 @ (sdtasdt0 @ xn @ xn))
% 44.34/6.97 | ((sk__7) = (sdtasdt0 @ xn @ xn)))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl45232, zip_derived_cl899, zip_derived_cl90])).
% 44.34/6.97 thf(m_MulUnit, axiom,
% 44.34/6.97 (![W0:$i]:
% 44.34/6.97 ( ( aNaturalNumber0 @ W0 ) =>
% 44.34/6.97 ( ( ( sdtasdt0 @ W0 @ sz10 ) = ( W0 ) ) &
% 44.34/6.97 ( ( W0 ) = ( sdtasdt0 @ sz10 @ W0 ) ) ) ))).
% 44.34/6.97 thf(zip_derived_cl13, plain,
% 44.34/6.97 (![X0 : $i]: (((X0) = (sdtasdt0 @ sz10 @ X0)) | ~ (aNaturalNumber0 @ X0))),
% 44.34/6.97 inference('cnf', [status(esa)], [m_MulUnit])).
% 44.34/6.97 thf(zip_derived_cl84, plain,
% 44.34/6.97 (((sdtasdt0 @ xp @ (sdtasdt0 @ xm @ xm)) = (sdtasdt0 @ xn @ xn))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3014])).
% 44.34/6.97 thf(zip_derived_cl20, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i, X2 : $i]:
% 44.34/6.97 (((X0) = (sz00))
% 44.34/6.97 | ((sdtasdt0 @ X2 @ X0) != (sdtasdt0 @ X1 @ X0))
% 44.34/6.97 | ((X2) = (X1))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X2)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0))),
% 44.34/6.97 inference('cnf', [status(esa)], [mMulCanc])).
% 44.34/6.97 thf(zip_derived_cl1482, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ X0 @ (sdtasdt0 @ xm @ xm)))
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtasdt0 @ xm @ xm))
% 44.34/6.97 | ~ (aNaturalNumber0 @ xp)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ((xp) = (X0))
% 44.34/6.97 | ((sdtasdt0 @ xm @ xm) = (sz00)))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl84, zip_derived_cl20])).
% 44.34/6.97 thf(zip_derived_cl74, plain, ( (aNaturalNumber0 @ xp)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl1517, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ X0 @ (sdtasdt0 @ xm @ xm)))
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtasdt0 @ xm @ xm))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ((xp) = (X0))
% 44.34/6.97 | ((sdtasdt0 @ xm @ xm) = (sz00)))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl1482, zip_derived_cl74])).
% 44.34/6.97 thf(zip_derived_cl11294, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl11216, zip_derived_cl97])).
% 44.34/6.97 thf(zip_derived_cl11294, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl11216, zip_derived_cl97])).
% 44.34/6.97 thf(zip_derived_cl11665, plain, ( (aNaturalNumber0 @ (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl9465, zip_derived_cl11294])).
% 44.34/6.97 thf(zip_derived_cl11294, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl11216, zip_derived_cl97])).
% 44.34/6.97 thf(zip_derived_cl30415, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ X0 @ (sdtasdt0 @ xn @ xq)))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ((xp) = (X0))
% 44.34/6.97 | ((sdtasdt0 @ xn @ xq) = (sz00)))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl1517, zip_derived_cl11294, zip_derived_cl11294,
% 44.34/6.97 zip_derived_cl11665, zip_derived_cl11294])).
% 44.34/6.97 thf(zip_derived_cl11294, plain,
% 44.34/6.97 (((sdtasdt0 @ xm @ xm) = (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)], [zip_derived_cl11216, zip_derived_cl97])).
% 44.34/6.97 thf(mZeroMul, axiom,
% 44.34/6.97 (![W0:$i,W1:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W0 ) & ( aNaturalNumber0 @ W1 ) ) =>
% 44.34/6.97 ( ( ( sdtasdt0 @ W0 @ W1 ) = ( sz00 ) ) =>
% 44.34/6.97 ( ( ( W0 ) = ( sz00 ) ) | ( ( W1 ) = ( sz00 ) ) ) ) ))).
% 44.34/6.97 thf(zip_derived_cl24, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (((X0) = (sz00))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | ((X1) = (sz00))
% 44.34/6.97 | ((sdtasdt0 @ X0 @ X1) != (sz00)))),
% 44.34/6.97 inference('cnf', [status(esa)], [mZeroMul])).
% 44.34/6.97 thf(zip_derived_cl11670, plain,
% 44.34/6.97 ((((sdtasdt0 @ xn @ xq) != (sz00))
% 44.34/6.97 | ((xm) = (sz00))
% 44.34/6.97 | ~ (aNaturalNumber0 @ xm)
% 44.34/6.97 | ~ (aNaturalNumber0 @ xm)
% 44.34/6.97 | ((xm) = (sz00)))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl11294, zip_derived_cl24])).
% 44.34/6.97 thf(zip_derived_cl75, plain, ( (aNaturalNumber0 @ xm)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl75, plain, ( (aNaturalNumber0 @ xm)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl11724, plain,
% 44.34/6.97 ((((sdtasdt0 @ xn @ xq) != (sz00)) | ((xm) = (sz00)) | ((xm) = (sz00)))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl11670, zip_derived_cl75, zip_derived_cl75])).
% 44.34/6.97 thf(zip_derived_cl11725, plain,
% 44.34/6.97 ((((xm) = (sz00)) | ((sdtasdt0 @ xn @ xq) != (sz00)))),
% 44.34/6.97 inference('simplify', [status(thm)], [zip_derived_cl11724])).
% 44.34/6.97 thf(zip_derived_cl72, plain, (((xm) != (sz00))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl11726, plain, (((sdtasdt0 @ xn @ xq) != (sz00))),
% 44.34/6.97 inference('simplify_reflect-', [status(thm)],
% 44.34/6.97 [zip_derived_cl11725, zip_derived_cl72])).
% 44.34/6.97 thf(zip_derived_cl30416, plain,
% 44.34/6.97 (![X0 : $i]:
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ X0 @ (sdtasdt0 @ xn @ xq)))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ((xp) = (X0)))),
% 44.34/6.97 inference('simplify_reflect-', [status(thm)],
% 44.34/6.97 [zip_derived_cl30415, zip_derived_cl11726])).
% 44.34/6.97 thf(zip_derived_cl30423, plain,
% 44.34/6.97 ((((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ xn @ xq))
% 44.34/6.97 | ~ (aNaturalNumber0 @ (sdtasdt0 @ xn @ xq))
% 44.34/6.97 | ((xp) = (sz10))
% 44.34/6.97 | ~ (aNaturalNumber0 @ sz10))),
% 44.34/6.97 inference('sup-', [status(thm)], [zip_derived_cl13, zip_derived_cl30416])).
% 44.34/6.97 thf(zip_derived_cl11665, plain, ( (aNaturalNumber0 @ (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl9465, zip_derived_cl11294])).
% 44.34/6.97 thf(mSortsC_01, axiom,
% 44.34/6.97 (( ( sz10 ) != ( sz00 ) ) & ( aNaturalNumber0 @ sz10 ))).
% 44.34/6.97 thf(zip_derived_cl3, plain, ( (aNaturalNumber0 @ sz10)),
% 44.34/6.97 inference('cnf', [status(esa)], [mSortsC_01])).
% 44.34/6.97 thf(zip_derived_cl30449, plain,
% 44.34/6.97 ((((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ xn @ xq)) | ((xp) = (sz10)))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl30423, zip_derived_cl11665, zip_derived_cl3])).
% 44.34/6.97 thf(m__3025, axiom,
% 44.34/6.97 (( isPrime0 @ xp ) &
% 44.34/6.97 ( ![W0:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W0 ) &
% 44.34/6.97 ( ( ?[W1:$i]:
% 44.34/6.97 ( ( ( xp ) = ( sdtasdt0 @ W0 @ W1 ) ) & ( aNaturalNumber0 @ W1 ) ) ) |
% 44.34/6.97 ( doDivides0 @ W0 @ xp ) ) ) =>
% 44.34/6.97 ( ( ( W0 ) = ( sz10 ) ) | ( ( W0 ) = ( xp ) ) ) ) ) &
% 44.34/6.97 ( ( xp ) != ( sz10 ) ))).
% 44.34/6.97 thf(zip_derived_cl85, plain, (((xp) != (sz10))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3025])).
% 44.34/6.97 thf(zip_derived_cl30450, plain,
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) != (sdtasdt0 @ xn @ xq))),
% 44.34/6.97 inference('simplify_reflect-', [status(thm)],
% 44.34/6.97 [zip_derived_cl30449, zip_derived_cl85])).
% 44.34/6.97 thf(zip_derived_cl33488, plain, (((sdtasdt0 @ xn @ xq) = (sk__7))),
% 44.34/6.97 inference('simplify', [status(thm)], [zip_derived_cl33487])).
% 44.34/6.97 thf(zip_derived_cl33509, plain, (((sdtasdt0 @ xn @ xn) != (sk__7))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl30450, zip_derived_cl33488])).
% 44.34/6.97 thf(zip_derived_cl45250, plain,
% 44.34/6.97 ((((xm) = (xn)) | ~ (sdtlseqdt0 @ sk__7 @ (sdtasdt0 @ xn @ xn)))),
% 44.34/6.97 inference('simplify_reflect-', [status(thm)],
% 44.34/6.97 [zip_derived_cl45249, zip_derived_cl33509])).
% 44.34/6.97 thf(zip_derived_cl89, plain,
% 44.34/6.97 (((sdtasdt0 @ xn @ xn) = (sdtasdt0 @ xp @ sk__7))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3046])).
% 44.34/6.97 thf(mMulComm, axiom,
% 44.34/6.97 (![W0:$i,W1:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W0 ) & ( aNaturalNumber0 @ W1 ) ) =>
% 44.34/6.97 ( ( sdtasdt0 @ W0 @ W1 ) = ( sdtasdt0 @ W1 @ W0 ) ) ))).
% 44.34/6.97 thf(zip_derived_cl10, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | ((sdtasdt0 @ X0 @ X1) = (sdtasdt0 @ X1 @ X0)))),
% 44.34/6.97 inference('cnf', [status(esa)], [mMulComm])).
% 44.34/6.97 thf(mMonMul2, axiom,
% 44.34/6.97 (![W0:$i,W1:$i]:
% 44.34/6.97 ( ( ( aNaturalNumber0 @ W0 ) & ( aNaturalNumber0 @ W1 ) ) =>
% 44.34/6.97 ( ( ( W0 ) != ( sz00 ) ) => ( sdtlseqdt0 @ W1 @ ( sdtasdt0 @ W1 @ W0 ) ) ) ))).
% 44.34/6.97 thf(zip_derived_cl46, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (((X0) = (sz00))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | (sdtlseqdt0 @ X1 @ (sdtasdt0 @ X1 @ X0)))),
% 44.34/6.97 inference('cnf', [status(esa)], [mMonMul2])).
% 44.34/6.97 thf(zip_derived_cl1840, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 ( (sdtlseqdt0 @ X0 @ (sdtasdt0 @ X1 @ X0))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | ((X1) = (sz00)))),
% 44.34/6.97 inference('sup+', [status(thm)], [zip_derived_cl10, zip_derived_cl46])).
% 44.34/6.97 thf(zip_derived_cl1856, plain,
% 44.34/6.97 (![X0 : $i, X1 : $i]:
% 44.34/6.97 (((X1) = (sz00))
% 44.34/6.97 | ~ (aNaturalNumber0 @ X0)
% 44.34/6.97 | ~ (aNaturalNumber0 @ X1)
% 44.34/6.97 | (sdtlseqdt0 @ X0 @ (sdtasdt0 @ X1 @ X0)))),
% 44.34/6.97 inference('simplify', [status(thm)], [zip_derived_cl1840])).
% 44.34/6.97 thf(zip_derived_cl40051, plain,
% 44.34/6.97 (( (sdtlseqdt0 @ sk__7 @ (sdtasdt0 @ xn @ xn))
% 44.34/6.97 | ~ (aNaturalNumber0 @ xp)
% 44.34/6.97 | ~ (aNaturalNumber0 @ sk__7)
% 44.34/6.97 | ((xp) = (sz00)))),
% 44.34/6.97 inference('sup+', [status(thm)], [zip_derived_cl89, zip_derived_cl1856])).
% 44.34/6.97 thf(zip_derived_cl74, plain, ( (aNaturalNumber0 @ xp)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl90, plain, ( (aNaturalNumber0 @ sk__7)),
% 44.34/6.97 inference('cnf', [status(esa)], [m__3046])).
% 44.34/6.97 thf(zip_derived_cl40125, plain,
% 44.34/6.97 (( (sdtlseqdt0 @ sk__7 @ (sdtasdt0 @ xn @ xn)) | ((xp) = (sz00)))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl40051, zip_derived_cl74, zip_derived_cl90])).
% 44.34/6.97 thf(zip_derived_cl71, plain, (((xp) != (sz00))),
% 44.34/6.97 inference('cnf', [status(esa)], [m__2987])).
% 44.34/6.97 thf(zip_derived_cl40126, plain,
% 44.34/6.97 ( (sdtlseqdt0 @ sk__7 @ (sdtasdt0 @ xn @ xn))),
% 44.34/6.97 inference('simplify_reflect-', [status(thm)],
% 44.34/6.97 [zip_derived_cl40125, zip_derived_cl71])).
% 44.34/6.97 thf(zip_derived_cl50225, plain, (((xm) = (xn))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl45250, zip_derived_cl40126])).
% 44.34/6.97 thf(zip_derived_cl50225, plain, (((xm) = (xn))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl45250, zip_derived_cl40126])).
% 44.34/6.97 thf(zip_derived_cl50355, plain, (((sdtasdt0 @ xn @ xn) = (sk__7))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl33489, zip_derived_cl50225, zip_derived_cl50225])).
% 44.34/6.97 thf(zip_derived_cl33509, plain, (((sdtasdt0 @ xn @ xn) != (sk__7))),
% 44.34/6.97 inference('demod', [status(thm)],
% 44.34/6.97 [zip_derived_cl30450, zip_derived_cl33488])).
% 44.34/6.97 thf(zip_derived_cl50356, plain, ($false),
% 44.34/6.97 inference('simplify_reflect-', [status(thm)],
% 44.34/6.97 [zip_derived_cl50355, zip_derived_cl33509])).
% 44.34/6.97
% 44.34/6.97 % SZS output end Refutation
% 44.34/6.97
% 44.34/6.97
% 44.34/6.97 % Terminating...
% 44.84/7.07 % Runner terminated.
% 44.84/7.07 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------