%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : RNG109+1 : 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.WwrowV9g0P true
% Computer : n025.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:50:33 PM UTC 2025
% Result : Theorem 135.61s 20.01s
% Output : Refutation 135.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : RNG109+1 : TPTP v9.2.0. Released v4.0.0.
% 0.06/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.WwrowV9g0P true
% 0.14/0.34 % Computer : n025.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Oct 1 17:24:23 EDT 2025
% 0.14/0.34 % CPUTime :
% 0.14/0.34 % Running portfolio for 300 s
% 0.14/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.34 % Number of cores: 8
% 0.14/0.34 % Python version: Python 3.6.8
% 0.14/0.34 % Running in FO mode
% 0.46/0.63 % Total configuration time : 435
% 0.46/0.63 % Estimated wc time : 1092
% 0.46/0.63 % Estimated cpu time (7 cpus) : 156.0
% 0.53/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.53/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.53/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.53/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.53/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.53/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.53/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 135.61/20.01 % Solved by fo/fo5.sh.
% 135.61/20.01 % done 11108 iterations in 19.231s
% 135.61/20.01 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 135.61/20.01 % SZS output start Refutation
% 135.61/20.01 thf(smndt0_type, type, smndt0: $i > $i).
% 135.61/20.01 thf(sdtasdt0_type, type, sdtasdt0: $i > $i > $i).
% 135.61/20.01 thf(aElement0_type, type, aElement0: $i > $o).
% 135.61/20.01 thf(sdtpldt1_type, type, sdtpldt1: $i > $i > $i).
% 135.61/20.01 thf(sz10_type, type, sz10: $i).
% 135.61/20.01 thf(xa_type, type, xa: $i).
% 135.61/20.01 thf(sz00_type, type, sz00: $i).
% 135.61/20.01 thf(sdtpldt0_type, type, sdtpldt0: $i > $i > $i).
% 135.61/20.01 thf(slsdtgt0_type, type, slsdtgt0: $i > $i).
% 135.61/20.01 thf(aIdeal0_type, type, aIdeal0: $i > $o).
% 135.61/20.01 thf(sk__15_type, type, sk__15: $i > $i > $i).
% 135.61/20.01 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $i > $i > $o).
% 135.61/20.01 thf(doDivides0_type, type, doDivides0: $i > $i > $o).
% 135.61/20.01 thf(aElementOf0_type, type, aElementOf0: $i > $i > $o).
% 135.61/20.01 thf(aSet0_type, type, aSet0: $i > $o).
% 135.61/20.01 thf(xb_type, type, xb: $i).
% 135.61/20.01 thf(xI_type, type, xI: $i).
% 135.61/20.01 thf(mDefPrIdeal, axiom,
% 135.61/20.01 (![W0:$i]:
% 135.61/20.01 ( ( aElement0 @ W0 ) =>
% 135.61/20.01 ( ![W1:$i]:
% 135.61/20.01 ( ( ( W1 ) = ( slsdtgt0 @ W0 ) ) <=>
% 135.61/20.01 ( ( aSet0 @ W1 ) &
% 135.61/20.01 ( ![W2:$i]:
% 135.61/20.01 ( ( aElementOf0 @ W2 @ W1 ) <=>
% 135.61/20.01 ( ?[W3:$i]:
% 135.61/20.01 ( ( ( sdtasdt0 @ W0 @ W3 ) = ( W2 ) ) & ( aElement0 @ W3 ) ) ) ) ) ) ) ) ))).
% 135.61/20.01 thf(zip_derived_cl92, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (((X1) != (slsdtgt0 @ X0)) | (aSet0 @ X1) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mDefPrIdeal])).
% 135.61/20.01 thf(zip_derived_cl120, plain,
% 135.61/20.01 (![X0 : $i]: (~ (aElement0 @ X0) | (aSet0 @ (slsdtgt0 @ X0)))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl92])).
% 135.61/20.01 thf(zip_derived_cl120, plain,
% 135.61/20.01 (![X0 : $i]: (~ (aElement0 @ X0) | (aSet0 @ (slsdtgt0 @ X0)))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl92])).
% 135.61/20.01 thf(m__2203, axiom,
% 135.61/20.01 (( aElementOf0 @ xb @ ( slsdtgt0 @ xb ) ) &
% 135.61/20.01 ( aElementOf0 @ sz00 @ ( slsdtgt0 @ xb ) ) &
% 135.61/20.01 ( aElementOf0 @ xa @ ( slsdtgt0 @ xa ) ) &
% 135.61/20.01 ( aElementOf0 @ sz00 @ ( slsdtgt0 @ xa ) ))).
% 135.61/20.01 thf(zip_derived_cl102, plain, ( (aElementOf0 @ xa @ (slsdtgt0 @ xa))),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2203])).
% 135.61/20.01 thf(mMulZero, axiom,
% 135.61/20.01 (![W0:$i]:
% 135.61/20.01 ( ( aElement0 @ W0 ) =>
% 135.61/20.01 ( ( ( sdtasdt0 @ W0 @ sz00 ) = ( sz00 ) ) &
% 135.61/20.01 ( ( sz00 ) = ( sdtasdt0 @ sz00 @ W0 ) ) ) ))).
% 135.61/20.01 thf(zip_derived_cl21, plain,
% 135.61/20.01 (![X0 : $i]: (((sz00) = (sdtasdt0 @ sz00 @ X0)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mMulZero])).
% 135.61/20.01 thf(mDefDiv, axiom,
% 135.61/20.01 (![W0:$i,W1:$i]:
% 135.61/20.01 ( ( ( aElement0 @ W0 ) & ( aElement0 @ W1 ) ) =>
% 135.61/20.01 ( ( doDivides0 @ W0 @ W1 ) <=>
% 135.61/20.01 ( ?[W2:$i]:
% 135.61/20.01 ( ( ( sdtasdt0 @ W0 @ W2 ) = ( W1 ) ) & ( aElement0 @ W2 ) ) ) ) ))).
% 135.61/20.01 thf(zip_derived_cl74, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | (doDivides0 @ X0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X2)
% 135.61/20.01 | ((sdtasdt0 @ X0 @ X2) != (X1)))),
% 135.61/20.01 inference('cnf', [status(esa)], [mDefDiv])).
% 135.61/20.01 thf(zip_derived_cl1223, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (((sz00) != (X0))
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | (doDivides0 @ sz00 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ sz00))),
% 135.61/20.01 inference('sup-', [status(thm)], [zip_derived_cl21, zip_derived_cl74])).
% 135.61/20.01 thf(mSortsC, axiom, (aElement0 @ sz00)).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl1235, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (((sz00) != (X0))
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | (doDivides0 @ sz00 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl1223, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl1236, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | (doDivides0 @ sz00 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ((sz00) != (X0)))),
% 135.61/20.01 inference('simplify', [status(thm)], [zip_derived_cl1235])).
% 135.61/20.01 thf(zip_derived_cl1348, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((sz00) != (X0)) | (doDivides0 @ sz00 @ X0) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('condensation', [status(thm)], [zip_derived_cl1236])).
% 135.61/20.01 thf(zip_derived_cl1351, plain,
% 135.61/20.01 ((~ (aElement0 @ sz00) | (doDivides0 @ sz00 @ sz00))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl1348])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl1352, plain, ( (doDivides0 @ sz00 @ sz00)),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl1351, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl72, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ((sdtasdt0 @ X0 @ (sk__15 @ X1 @ X0)) = (X1))
% 135.61/20.01 | ~ (doDivides0 @ X0 @ X1))),
% 135.61/20.01 inference('cnf', [status(esa)], [mDefDiv])).
% 135.61/20.01 thf(zip_derived_cl2510, plain,
% 135.61/20.01 ((((sdtasdt0 @ sz00 @ (sk__15 @ sz00 @ sz00)) = (sz00))
% 135.61/20.01 | ~ (aElement0 @ sz00)
% 135.61/20.01 | ~ (aElement0 @ sz00))),
% 135.61/20.01 inference('sup-', [status(thm)], [zip_derived_cl1352, zip_derived_cl72])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl2523, plain,
% 135.61/20.01 (((sdtasdt0 @ sz00 @ (sk__15 @ sz00 @ sz00)) = (sz00))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl2510, zip_derived_cl1, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl89, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 135.61/20.01 (((X1) != (slsdtgt0 @ X0))
% 135.61/20.01 | (aElementOf0 @ X2 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X3)
% 135.61/20.01 | ((sdtasdt0 @ X0 @ X3) != (X2))
% 135.61/20.01 | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mDefPrIdeal])).
% 135.61/20.01 thf(zip_derived_cl1217, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ((sdtasdt0 @ X0 @ X1) != (X2))
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | (aElementOf0 @ X2 @ (slsdtgt0 @ X0)))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl89])).
% 135.61/20.01 thf(zip_derived_cl9201, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((sz00) != (X0))
% 135.61/20.01 | (aElementOf0 @ X0 @ (slsdtgt0 @ sz00))
% 135.61/20.01 | ~ (aElement0 @ (sk__15 @ sz00 @ sz00))
% 135.61/20.01 | ~ (aElement0 @ sz00))),
% 135.61/20.01 inference('sup-', [status(thm)], [zip_derived_cl2523, zip_derived_cl1217])).
% 135.61/20.01 thf(zip_derived_cl1352, plain, ( (doDivides0 @ sz00 @ sz00)),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl1351, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl73, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | (aElement0 @ (sk__15 @ X1 @ X0))
% 135.61/20.01 | ~ (doDivides0 @ X0 @ X1))),
% 135.61/20.01 inference('cnf', [status(esa)], [mDefDiv])).
% 135.61/20.01 thf(zip_derived_cl1353, plain,
% 135.61/20.01 (( (aElement0 @ (sk__15 @ sz00 @ sz00))
% 135.61/20.01 | ~ (aElement0 @ sz00)
% 135.61/20.01 | ~ (aElement0 @ sz00))),
% 135.61/20.01 inference('sup-', [status(thm)], [zip_derived_cl1352, zip_derived_cl73])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl1359, plain, ( (aElement0 @ (sk__15 @ sz00 @ sz00))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl1353, zip_derived_cl1, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl9223, plain,
% 135.61/20.01 (![X0 : $i]: (((sz00) != (X0)) | (aElementOf0 @ X0 @ (slsdtgt0 @ sz00)))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl9201, zip_derived_cl1359, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl9237, plain, ( (aElementOf0 @ sz00 @ (slsdtgt0 @ sz00))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl9223])).
% 135.61/20.01 thf(mAddComm, axiom,
% 135.61/20.01 (![W0:$i,W1:$i]:
% 135.61/20.01 ( ( ( aElement0 @ W0 ) & ( aElement0 @ W1 ) ) =>
% 135.61/20.01 ( ( sdtpldt0 @ W0 @ W1 ) = ( sdtpldt0 @ W1 @ W0 ) ) ))).
% 135.61/20.01 thf(zip_derived_cl6, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ((sdtpldt0 @ X0 @ X1) = (sdtpldt0 @ X1 @ X0)))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAddComm])).
% 135.61/20.01 thf(zip_derived_cl6, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ((sdtpldt0 @ X0 @ X1) = (sdtpldt0 @ X1 @ X0)))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAddComm])).
% 135.61/20.01 thf(m__2091, axiom, (( aElement0 @ xb ) & ( aElement0 @ xa ))).
% 135.61/20.01 thf(zip_derived_cl95, plain, ( (aElement0 @ xa)),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2091])).
% 135.61/20.01 thf(zip_derived_cl205, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((sdtpldt0 @ xa @ X0) = (sdtpldt0 @ X0 @ xa)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl95])).
% 135.61/20.01 thf(mAddZero, axiom,
% 135.61/20.01 (![W0:$i]:
% 135.61/20.01 ( ( aElement0 @ W0 ) =>
% 135.61/20.01 ( ( ( sdtpldt0 @ W0 @ sz00 ) = ( W0 ) ) &
% 135.61/20.01 ( ( W0 ) = ( sdtpldt0 @ sz00 @ W0 ) ) ) ))).
% 135.61/20.01 thf(zip_derived_cl8, plain,
% 135.61/20.01 (![X0 : $i]: (((sdtpldt0 @ X0 @ sz00) = (X0)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAddZero])).
% 135.61/20.01 thf(zip_derived_cl10058, plain,
% 135.61/20.01 ((((sdtpldt0 @ sz00 @ xa) = (xa))
% 135.61/20.01 | ~ (aElement0 @ sz00)
% 135.61/20.01 | ~ (aElement0 @ xa))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl205, zip_derived_cl8])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl95, plain, ( (aElement0 @ xa)),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2091])).
% 135.61/20.01 thf(zip_derived_cl10126, plain, (((sdtpldt0 @ sz00 @ xa) = (xa))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl10058, zip_derived_cl1, zip_derived_cl95])).
% 135.61/20.01 thf(zip_derived_cl20, plain,
% 135.61/20.01 (![X0 : $i]: (((sdtasdt0 @ X0 @ sz00) = (sz00)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mMulZero])).
% 135.61/20.01 thf(mAMDistr, axiom,
% 135.61/20.01 (![W0:$i,W1:$i,W2:$i]:
% 135.61/20.01 ( ( ( aElement0 @ W0 ) & ( aElement0 @ W1 ) & ( aElement0 @ W2 ) ) =>
% 135.61/20.01 ( ( ( sdtasdt0 @ W0 @ ( sdtpldt0 @ W1 @ W2 ) ) =
% 135.61/20.01 ( sdtpldt0 @ ( sdtasdt0 @ W0 @ W1 ) @ ( sdtasdt0 @ W0 @ W2 ) ) ) &
% 135.61/20.01 ( ( sdtasdt0 @ ( sdtpldt0 @ W1 @ W2 ) @ W0 ) =
% 135.61/20.01 ( sdtpldt0 @ ( sdtasdt0 @ W1 @ W0 ) @ ( sdtasdt0 @ W2 @ W0 ) ) ) ) ))).
% 135.61/20.01 thf(zip_derived_cl17, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X2)
% 135.61/20.01 | ((sdtasdt0 @ (sdtpldt0 @ X0 @ X2) @ X1)
% 135.61/20.01 = (sdtpldt0 @ (sdtasdt0 @ X0 @ X1) @ (sdtasdt0 @ X2 @ X1))))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAMDistr])).
% 135.61/20.01 thf(zip_derived_cl787, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (((sdtasdt0 @ (sdtpldt0 @ X1 @ X0) @ sz00)
% 135.61/20.01 = (sdtpldt0 @ (sdtasdt0 @ X1 @ sz00) @ sz00))
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ sz00)
% 135.61/20.01 | ~ (aElement0 @ X1))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl20, zip_derived_cl17])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl805, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (((sdtasdt0 @ (sdtpldt0 @ X1 @ X0) @ sz00)
% 135.61/20.01 = (sdtpldt0 @ (sdtasdt0 @ X1 @ sz00) @ sz00))
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1))),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl787, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl806, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ((sdtasdt0 @ (sdtpldt0 @ X1 @ X0) @ sz00)
% 135.61/20.01 = (sdtpldt0 @ (sdtasdt0 @ X1 @ sz00) @ sz00)))),
% 135.61/20.01 inference('simplify', [status(thm)], [zip_derived_cl805])).
% 135.61/20.01 thf(zip_derived_cl91783, plain,
% 135.61/20.01 ((((sdtasdt0 @ xa @ sz00) = (sdtpldt0 @ (sdtasdt0 @ sz00 @ sz00) @ sz00))
% 135.61/20.01 | ~ (aElement0 @ xa)
% 135.61/20.01 | ~ (aElement0 @ sz00))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl10126, zip_derived_cl806])).
% 135.61/20.01 thf(mMulComm, axiom,
% 135.61/20.01 (![W0:$i,W1:$i]:
% 135.61/20.01 ( ( ( aElement0 @ W0 ) & ( aElement0 @ W1 ) ) =>
% 135.61/20.01 ( ( sdtasdt0 @ W0 @ W1 ) = ( sdtasdt0 @ W1 @ W0 ) ) ))).
% 135.61/20.01 thf(zip_derived_cl12, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ((sdtasdt0 @ X0 @ X1) = (sdtasdt0 @ X1 @ X0)))),
% 135.61/20.01 inference('cnf', [status(esa)], [mMulComm])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl365, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((sdtasdt0 @ sz00 @ X0) = (sdtasdt0 @ X0 @ sz00))
% 135.61/20.01 | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl12, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl21, plain,
% 135.61/20.01 (![X0 : $i]: (((sz00) = (sdtasdt0 @ sz00 @ X0)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mMulZero])).
% 135.61/20.01 thf(zip_derived_cl20651, plain,
% 135.61/20.01 ((((sz00) = (sdtasdt0 @ sz00 @ sz00))
% 135.61/20.01 | ~ (aElement0 @ sz00)
% 135.61/20.01 | ~ (aElement0 @ sz00))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl365, zip_derived_cl21])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl20727, plain, (((sz00) = (sdtasdt0 @ sz00 @ sz00))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl20651, zip_derived_cl1, zip_derived_cl1])).
% 135.61/20.01 thf(mSortsU, axiom,
% 135.61/20.01 (![W0:$i]: ( ( aElement0 @ W0 ) => ( aElement0 @ ( smndt0 @ W0 ) ) ))).
% 135.61/20.01 thf(zip_derived_cl3, plain,
% 135.61/20.01 (![X0 : $i]: ( (aElement0 @ (smndt0 @ X0)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsU])).
% 135.61/20.01 thf(mAddInvr, axiom,
% 135.61/20.01 (![W0:$i]:
% 135.61/20.01 ( ( aElement0 @ W0 ) =>
% 135.61/20.01 ( ( ( sdtpldt0 @ W0 @ ( smndt0 @ W0 ) ) = ( sz00 ) ) &
% 135.61/20.01 ( ( sz00 ) = ( sdtpldt0 @ ( smndt0 @ W0 ) @ W0 ) ) ) ))).
% 135.61/20.01 thf(zip_derived_cl10, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((sdtpldt0 @ X0 @ (smndt0 @ X0)) = (sz00)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAddInvr])).
% 135.61/20.01 thf(zip_derived_cl9, plain,
% 135.61/20.01 (![X0 : $i]: (((X0) = (sdtpldt0 @ sz00 @ X0)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAddZero])).
% 135.61/20.01 thf(zip_derived_cl132, plain,
% 135.61/20.01 ((((smndt0 @ sz00) = (sz00))
% 135.61/20.01 | ~ (aElement0 @ sz00)
% 135.61/20.01 | ~ (aElement0 @ (smndt0 @ sz00)))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl10, zip_derived_cl9])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl135, plain,
% 135.61/20.01 ((((smndt0 @ sz00) = (sz00)) | ~ (aElement0 @ (smndt0 @ sz00)))),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl132, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl149, plain,
% 135.61/20.01 ((~ (aElement0 @ sz00) | ((smndt0 @ sz00) = (sz00)))),
% 135.61/20.01 inference('sup-', [status(thm)], [zip_derived_cl3, zip_derived_cl135])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl150, plain, (((smndt0 @ sz00) = (sz00))),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl149, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl10, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((sdtpldt0 @ X0 @ (smndt0 @ X0)) = (sz00)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAddInvr])).
% 135.61/20.01 thf(zip_derived_cl152, plain,
% 135.61/20.01 ((((sdtpldt0 @ sz00 @ sz00) = (sz00)) | ~ (aElement0 @ sz00))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl150, zip_derived_cl10])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl154, plain, (((sdtpldt0 @ sz00 @ sz00) = (sz00))),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl152, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl95, plain, ( (aElement0 @ xa)),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2091])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl91996, plain, (((sdtasdt0 @ xa @ sz00) = (sz00))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl91783, zip_derived_cl20727, zip_derived_cl154,
% 135.61/20.01 zip_derived_cl95, zip_derived_cl1])).
% 135.61/20.01 thf(mMulUnit, axiom,
% 135.61/20.01 (![W0:$i]:
% 135.61/20.01 ( ( aElement0 @ W0 ) =>
% 135.61/20.01 ( ( ( sdtasdt0 @ W0 @ sz10 ) = ( W0 ) ) &
% 135.61/20.01 ( ( W0 ) = ( sdtasdt0 @ sz10 @ W0 ) ) ) ))).
% 135.61/20.01 thf(zip_derived_cl14, plain,
% 135.61/20.01 (![X0 : $i]: (((sdtasdt0 @ X0 @ sz10) = (X0)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mMulUnit])).
% 135.61/20.01 thf(zip_derived_cl16, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X2)
% 135.61/20.01 | ((sdtasdt0 @ X1 @ (sdtpldt0 @ X0 @ X2))
% 135.61/20.01 = (sdtpldt0 @ (sdtasdt0 @ X1 @ X0) @ (sdtasdt0 @ X1 @ X2))))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAMDistr])).
% 135.61/20.01 thf(zip_derived_cl659, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (((sdtasdt0 @ X0 @ (sdtpldt0 @ sz10 @ X1))
% 135.61/20.01 = (sdtpldt0 @ X0 @ (sdtasdt0 @ X0 @ X1)))
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ sz10))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl14, zip_derived_cl16])).
% 135.61/20.01 thf(mSortsC_01, axiom, (aElement0 @ sz10)).
% 135.61/20.01 thf(zip_derived_cl2, plain, ( (aElement0 @ sz10)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC_01])).
% 135.61/20.01 thf(zip_derived_cl680, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (((sdtasdt0 @ X0 @ (sdtpldt0 @ sz10 @ X1))
% 135.61/20.01 = (sdtpldt0 @ X0 @ (sdtasdt0 @ X0 @ X1)))
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl659, zip_derived_cl2])).
% 135.61/20.01 thf(zip_derived_cl681, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ((sdtasdt0 @ X0 @ (sdtpldt0 @ sz10 @ X1))
% 135.61/20.01 = (sdtpldt0 @ X0 @ (sdtasdt0 @ X0 @ X1))))),
% 135.61/20.01 inference('simplify', [status(thm)], [zip_derived_cl680])).
% 135.61/20.01 thf(zip_derived_cl92221, plain,
% 135.61/20.01 ((((sdtasdt0 @ xa @ (sdtpldt0 @ sz10 @ sz00)) = (sdtpldt0 @ xa @ sz00))
% 135.61/20.01 | ~ (aElement0 @ xa)
% 135.61/20.01 | ~ (aElement0 @ sz00))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl91996, zip_derived_cl681])).
% 135.61/20.01 thf(zip_derived_cl95, plain, ( (aElement0 @ xa)),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2091])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl92307, plain,
% 135.61/20.01 (((sdtasdt0 @ xa @ (sdtpldt0 @ sz10 @ sz00)) = (sdtpldt0 @ xa @ sz00))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl92221, zip_derived_cl95, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl107016, plain,
% 135.61/20.01 ((((sdtasdt0 @ xa @ (sdtpldt0 @ sz00 @ sz10)) = (sdtpldt0 @ xa @ sz00))
% 135.61/20.01 | ~ (aElement0 @ sz00)
% 135.61/20.01 | ~ (aElement0 @ sz10))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl92307])).
% 135.61/20.01 thf(zip_derived_cl6, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ((sdtpldt0 @ X0 @ X1) = (sdtpldt0 @ X1 @ X0)))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAddComm])).
% 135.61/20.01 thf(zip_derived_cl2, plain, ( (aElement0 @ sz10)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC_01])).
% 135.61/20.01 thf(zip_derived_cl201, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((sdtpldt0 @ sz10 @ X0) = (sdtpldt0 @ X0 @ sz10))
% 135.61/20.01 | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl2])).
% 135.61/20.01 thf(zip_derived_cl8, plain,
% 135.61/20.01 (![X0 : $i]: (((sdtpldt0 @ X0 @ sz00) = (X0)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAddZero])).
% 135.61/20.01 thf(zip_derived_cl9134, plain,
% 135.61/20.01 ((((sdtpldt0 @ sz00 @ sz10) = (sz10))
% 135.61/20.01 | ~ (aElement0 @ sz00)
% 135.61/20.01 | ~ (aElement0 @ sz10))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl201, zip_derived_cl8])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl2, plain, ( (aElement0 @ sz10)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC_01])).
% 135.61/20.01 thf(zip_derived_cl9161, plain, (((sdtpldt0 @ sz00 @ sz10) = (sz10))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl9134, zip_derived_cl1, zip_derived_cl2])).
% 135.61/20.01 thf(zip_derived_cl91996, plain, (((sdtasdt0 @ xa @ sz00) = (sz00))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl91783, zip_derived_cl20727, zip_derived_cl154,
% 135.61/20.01 zip_derived_cl95, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl14, plain,
% 135.61/20.01 (![X0 : $i]: (((sdtasdt0 @ X0 @ sz10) = (X0)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mMulUnit])).
% 135.61/20.01 thf(zip_derived_cl16, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X2)
% 135.61/20.01 | ((sdtasdt0 @ X1 @ (sdtpldt0 @ X0 @ X2))
% 135.61/20.01 = (sdtpldt0 @ (sdtasdt0 @ X1 @ X0) @ (sdtasdt0 @ X1 @ X2))))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAMDistr])).
% 135.61/20.01 thf(zip_derived_cl651, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (((sdtasdt0 @ X0 @ (sdtpldt0 @ X1 @ sz10))
% 135.61/20.01 = (sdtpldt0 @ (sdtasdt0 @ X0 @ X1) @ X0))
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ sz10)
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl14, zip_derived_cl16])).
% 135.61/20.01 thf(zip_derived_cl2, plain, ( (aElement0 @ sz10)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC_01])).
% 135.61/20.01 thf(zip_derived_cl668, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (((sdtasdt0 @ X0 @ (sdtpldt0 @ X1 @ sz10))
% 135.61/20.01 = (sdtpldt0 @ (sdtasdt0 @ X0 @ X1) @ X0))
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1))),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl651, zip_derived_cl2])).
% 135.61/20.01 thf(zip_derived_cl669, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X1)
% 135.61/20.01 | ~ (aElement0 @ X0)
% 135.61/20.01 | ((sdtasdt0 @ X0 @ (sdtpldt0 @ X1 @ sz10))
% 135.61/20.01 = (sdtpldt0 @ (sdtasdt0 @ X0 @ X1) @ X0)))),
% 135.61/20.01 inference('simplify', [status(thm)], [zip_derived_cl668])).
% 135.61/20.01 thf(zip_derived_cl92220, plain,
% 135.61/20.01 ((((sdtasdt0 @ xa @ (sdtpldt0 @ sz00 @ sz10)) = (sdtpldt0 @ sz00 @ xa))
% 135.61/20.01 | ~ (aElement0 @ xa)
% 135.61/20.01 | ~ (aElement0 @ sz00))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl91996, zip_derived_cl669])).
% 135.61/20.01 thf(zip_derived_cl9161, plain, (((sdtpldt0 @ sz00 @ sz10) = (sz10))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl9134, zip_derived_cl1, zip_derived_cl2])).
% 135.61/20.01 thf(zip_derived_cl10126, plain, (((sdtpldt0 @ sz00 @ xa) = (xa))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl10058, zip_derived_cl1, zip_derived_cl95])).
% 135.61/20.01 thf(zip_derived_cl95, plain, ( (aElement0 @ xa)),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2091])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl92306, plain, (((sdtasdt0 @ xa @ sz10) = (xa))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl92220, zip_derived_cl9161, zip_derived_cl10126,
% 135.61/20.01 zip_derived_cl95, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl2, plain, ( (aElement0 @ sz10)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC_01])).
% 135.61/20.01 thf(zip_derived_cl107063, plain, (((xa) = (sdtpldt0 @ xa @ sz00))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl107016, zip_derived_cl9161,
% 135.61/20.01 zip_derived_cl92306, zip_derived_cl1, zip_derived_cl2])).
% 135.61/20.01 thf(mDefSSum, axiom,
% 135.61/20.01 (![W0:$i,W1:$i]:
% 135.61/20.01 ( ( ( aSet0 @ W1 ) & ( aSet0 @ W0 ) ) =>
% 135.61/20.01 ( ![W2:$i]:
% 135.61/20.01 ( ( ( W2 ) = ( sdtpldt1 @ W0 @ W1 ) ) <=>
% 135.61/20.01 ( ( ![W3:$i]:
% 135.61/20.01 ( ( aElementOf0 @ W3 @ W2 ) <=>
% 135.61/20.01 ( ?[W4:$i,W5:$i]:
% 135.61/20.01 ( ( aElementOf0 @ W4 @ W0 ) & ( aElementOf0 @ W5 @ W1 ) &
% 135.61/20.01 ( ( sdtpldt0 @ W4 @ W5 ) = ( W3 ) ) ) ) ) ) &
% 135.61/20.01 ( aSet0 @ W2 ) ) ) ) ))).
% 135.61/20.01 thf(zf_stmt_0, axiom,
% 135.61/20.01 (![W5:$i,W4:$i,W3:$i,W1:$i,W0:$i]:
% 135.61/20.01 ( ( zip_tseitin_2 @ W5 @ W4 @ W3 @ W1 @ W0 ) <=>
% 135.61/20.01 ( ( ( sdtpldt0 @ W4 @ W5 ) = ( W3 ) ) & ( aElementOf0 @ W5 @ W1 ) &
% 135.61/20.01 ( aElementOf0 @ W4 @ W0 ) ) ))).
% 135.61/20.01 thf(zip_derived_cl34, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 135.61/20.01 ( (zip_tseitin_2 @ X0 @ X1 @ X2 @ X3 @ X4)
% 135.61/20.01 | ~ (aElementOf0 @ X1 @ X4)
% 135.61/20.01 | ~ (aElementOf0 @ X0 @ X3)
% 135.61/20.01 | ((sdtpldt0 @ X1 @ X0) != (X2)))),
% 135.61/20.01 inference('cnf', [status(esa)], [zf_stmt_0])).
% 135.61/20.01 thf(zip_derived_cl107178, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i]:
% 135.61/20.01 (((xa) != (X0))
% 135.61/20.01 | ~ (aElementOf0 @ sz00 @ X1)
% 135.61/20.01 | ~ (aElementOf0 @ xa @ X2)
% 135.61/20.01 | (zip_tseitin_2 @ sz00 @ xa @ X0 @ X1 @ X2))),
% 135.61/20.01 inference('sup-', [status(thm)], [zip_derived_cl107063, zip_derived_cl34])).
% 135.61/20.01 thf(zip_derived_cl191913, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 ( (zip_tseitin_2 @ sz00 @ xa @ X1 @ (slsdtgt0 @ sz00) @ X0)
% 135.61/20.01 | ~ (aElementOf0 @ xa @ X0)
% 135.61/20.01 | ((xa) != (X1)))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl9237, zip_derived_cl107178])).
% 135.61/20.01 thf(zip_derived_cl192484, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((xa) != (X0))
% 135.61/20.01 | (zip_tseitin_2 @ sz00 @ xa @ X0 @ (slsdtgt0 @ sz00) @
% 135.61/20.01 (slsdtgt0 @ xa)))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl102, zip_derived_cl191913])).
% 135.61/20.01 thf(zip_derived_cl192505, plain,
% 135.61/20.01 ( (zip_tseitin_2 @ sz00 @ xa @ xa @ (slsdtgt0 @ sz00) @ (slsdtgt0 @ xa))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl192484])).
% 135.61/20.01 thf(zf_stmt_1, type, zip_tseitin_2 : $i > $i > $i > $i > $i > $o).
% 135.61/20.01 thf(zf_stmt_2, axiom,
% 135.61/20.01 (![W0:$i,W1:$i]:
% 135.61/20.01 ( ( ( aSet0 @ W0 ) & ( aSet0 @ W1 ) ) =>
% 135.61/20.01 ( ![W2:$i]:
% 135.61/20.01 ( ( ( W2 ) = ( sdtpldt1 @ W0 @ W1 ) ) <=>
% 135.61/20.01 ( ( aSet0 @ W2 ) &
% 135.61/20.01 ( ![W3:$i]:
% 135.61/20.01 ( ( aElementOf0 @ W3 @ W2 ) <=>
% 135.61/20.01 ( ?[W4:$i,W5:$i]: ( zip_tseitin_2 @ W5 @ W4 @ W3 @ W1 @ W0 ) ) ) ) ) ) ) ))).
% 135.61/20.01 thf(zip_derived_cl37, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 135.61/20.01 (~ (aSet0 @ X0)
% 135.61/20.01 | ~ (aSet0 @ X1)
% 135.61/20.01 | ~ (zip_tseitin_2 @ X2 @ X3 @ X4 @ X1 @ X0)
% 135.61/20.01 | (aElementOf0 @ X4 @ X5)
% 135.61/20.01 | ((X5) != (sdtpldt1 @ X0 @ X1)))),
% 135.61/20.01 inference('cnf', [status(esa)], [zf_stmt_2])).
% 135.61/20.01 thf(zip_derived_cl1184, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 135.61/20.01 ( (aElementOf0 @ X2 @ (sdtpldt1 @ X1 @ X0))
% 135.61/20.01 | ~ (zip_tseitin_2 @ X4 @ X3 @ X2 @ X0 @ X1)
% 135.61/20.01 | ~ (aSet0 @ X0)
% 135.61/20.01 | ~ (aSet0 @ X1))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl37])).
% 135.61/20.01 thf(zip_derived_cl192790, plain,
% 135.61/20.01 ((~ (aSet0 @ (slsdtgt0 @ xa))
% 135.61/20.01 | ~ (aSet0 @ (slsdtgt0 @ sz00))
% 135.61/20.01 | (aElementOf0 @ xa @ (sdtpldt1 @ (slsdtgt0 @ xa) @ (slsdtgt0 @ sz00))))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl192505, zip_derived_cl1184])).
% 135.61/20.01 thf(m__2174, axiom,
% 135.61/20.01 (( ( xI ) = ( sdtpldt1 @ ( slsdtgt0 @ xa ) @ ( slsdtgt0 @ xb ) ) ) &
% 135.61/20.01 ( aIdeal0 @ xI ))).
% 135.61/20.01 thf(zip_derived_cl98, plain,
% 135.61/20.01 (((xI) = (sdtpldt1 @ (slsdtgt0 @ xa) @ (slsdtgt0 @ xb)))),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2174])).
% 135.61/20.01 thf(zip_derived_cl120, plain,
% 135.61/20.01 (![X0 : $i]: (~ (aElement0 @ X0) | (aSet0 @ (slsdtgt0 @ X0)))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl92])).
% 135.61/20.01 thf(zip_derived_cl120, plain,
% 135.61/20.01 (![X0 : $i]: (~ (aElement0 @ X0) | (aSet0 @ (slsdtgt0 @ X0)))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl92])).
% 135.61/20.01 thf(zip_derived_cl103, plain, ( (aElementOf0 @ sz00 @ (slsdtgt0 @ xa))),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2203])).
% 135.61/20.01 thf(zip_derived_cl100, plain, ( (aElementOf0 @ xb @ (slsdtgt0 @ xb))),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2203])).
% 135.61/20.01 thf(zip_derived_cl6, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 (~ (aElement0 @ X0)
% 135.61/20.01 | ~ (aElement0 @ X1)
% 135.61/20.01 | ((sdtpldt0 @ X0 @ X1) = (sdtpldt0 @ X1 @ X0)))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAddComm])).
% 135.61/20.01 thf(zip_derived_cl94, plain, ( (aElement0 @ xb)),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2091])).
% 135.61/20.01 thf(zip_derived_cl206, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((sdtpldt0 @ xb @ X0) = (sdtpldt0 @ X0 @ xb)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl94])).
% 135.61/20.01 thf(zip_derived_cl8, plain,
% 135.61/20.01 (![X0 : $i]: (((sdtpldt0 @ X0 @ sz00) = (X0)) | ~ (aElement0 @ X0))),
% 135.61/20.01 inference('cnf', [status(esa)], [mAddZero])).
% 135.61/20.01 thf(zip_derived_cl10222, plain,
% 135.61/20.01 ((((sdtpldt0 @ sz00 @ xb) = (xb))
% 135.61/20.01 | ~ (aElement0 @ sz00)
% 135.61/20.01 | ~ (aElement0 @ xb))),
% 135.61/20.01 inference('sup+', [status(thm)], [zip_derived_cl206, zip_derived_cl8])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl94, plain, ( (aElement0 @ xb)),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2091])).
% 135.61/20.01 thf(zip_derived_cl10292, plain, (((sdtpldt0 @ sz00 @ xb) = (xb))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl10222, zip_derived_cl1, zip_derived_cl94])).
% 135.61/20.01 thf(zip_derived_cl34, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 135.61/20.01 ( (zip_tseitin_2 @ X0 @ X1 @ X2 @ X3 @ X4)
% 135.61/20.01 | ~ (aElementOf0 @ X1 @ X4)
% 135.61/20.01 | ~ (aElementOf0 @ X0 @ X3)
% 135.61/20.01 | ((sdtpldt0 @ X1 @ X0) != (X2)))),
% 135.61/20.01 inference('cnf', [status(esa)], [zf_stmt_0])).
% 135.61/20.01 thf(zip_derived_cl10330, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i]:
% 135.61/20.01 (((xb) != (X0))
% 135.61/20.01 | ~ (aElementOf0 @ xb @ X1)
% 135.61/20.01 | ~ (aElementOf0 @ sz00 @ X2)
% 135.61/20.01 | (zip_tseitin_2 @ xb @ sz00 @ X0 @ X1 @ X2))),
% 135.61/20.01 inference('sup-', [status(thm)], [zip_derived_cl10292, zip_derived_cl34])).
% 135.61/20.01 thf(zip_derived_cl17437, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i]:
% 135.61/20.01 ( (zip_tseitin_2 @ xb @ sz00 @ X1 @ (slsdtgt0 @ xb) @ X0)
% 135.61/20.01 | ~ (aElementOf0 @ sz00 @ X0)
% 135.61/20.01 | ((xb) != (X1)))),
% 135.61/20.01 inference('sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl10330])).
% 135.61/20.01 thf(zip_derived_cl17455, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((xb) != (X0))
% 135.61/20.01 | (zip_tseitin_2 @ xb @ sz00 @ X0 @ (slsdtgt0 @ xb) @
% 135.61/20.01 (slsdtgt0 @ xa)))),
% 135.61/20.01 inference('sup-', [status(thm)], [zip_derived_cl103, zip_derived_cl17437])).
% 135.61/20.01 thf(zip_derived_cl17473, plain,
% 135.61/20.01 ( (zip_tseitin_2 @ xb @ sz00 @ xb @ (slsdtgt0 @ xb) @ (slsdtgt0 @ xa))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl17455])).
% 135.61/20.01 thf(zip_derived_cl1184, plain,
% 135.61/20.01 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 135.61/20.01 ( (aElementOf0 @ X2 @ (sdtpldt1 @ X1 @ X0))
% 135.61/20.01 | ~ (zip_tseitin_2 @ X4 @ X3 @ X2 @ X0 @ X1)
% 135.61/20.01 | ~ (aSet0 @ X0)
% 135.61/20.01 | ~ (aSet0 @ X1))),
% 135.61/20.01 inference('eq_res', [status(thm)], [zip_derived_cl37])).
% 135.61/20.01 thf(zip_derived_cl124144, plain,
% 135.61/20.01 ((~ (aSet0 @ (slsdtgt0 @ xa))
% 135.61/20.01 | ~ (aSet0 @ (slsdtgt0 @ xb))
% 135.61/20.01 | (aElementOf0 @ xb @ (sdtpldt1 @ (slsdtgt0 @ xa) @ (slsdtgt0 @ xb))))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl17473, zip_derived_cl1184])).
% 135.61/20.01 thf(zip_derived_cl98, plain,
% 135.61/20.01 (((xI) = (sdtpldt1 @ (slsdtgt0 @ xa) @ (slsdtgt0 @ xb)))),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2174])).
% 135.61/20.01 thf(zip_derived_cl124161, plain,
% 135.61/20.01 ((~ (aSet0 @ (slsdtgt0 @ xa))
% 135.61/20.01 | ~ (aSet0 @ (slsdtgt0 @ xb))
% 135.61/20.01 | (aElementOf0 @ xb @ xI))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl124144, zip_derived_cl98])).
% 135.61/20.01 thf(zip_derived_cl126450, plain,
% 135.61/20.01 ((~ (aElement0 @ xa)
% 135.61/20.01 | (aElementOf0 @ xb @ xI)
% 135.61/20.01 | ~ (aSet0 @ (slsdtgt0 @ xb)))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl120, zip_derived_cl124161])).
% 135.61/20.01 thf(zip_derived_cl95, plain, ( (aElement0 @ xa)),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2091])).
% 135.61/20.01 thf(zip_derived_cl126463, plain,
% 135.61/20.01 (( (aElementOf0 @ xb @ xI) | ~ (aSet0 @ (slsdtgt0 @ xb)))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl126450, zip_derived_cl95])).
% 135.61/20.01 thf(zip_derived_cl126465, plain,
% 135.61/20.01 ((~ (aElement0 @ xb) | (aElementOf0 @ xb @ xI))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl120, zip_derived_cl126463])).
% 135.61/20.01 thf(zip_derived_cl94, plain, ( (aElement0 @ xb)),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2091])).
% 135.61/20.01 thf(zip_derived_cl126478, plain, ( (aElementOf0 @ xb @ xI)),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl126465, zip_derived_cl94])).
% 135.61/20.01 thf(m__, conjecture,
% 135.61/20.01 (?[W0:$i]:
% 135.61/20.01 ( ( ( W0 ) != ( sz00 ) ) &
% 135.61/20.01 ( aElementOf0 @
% 135.61/20.01 W0 @ ( sdtpldt1 @ ( slsdtgt0 @ xa ) @ ( slsdtgt0 @ xb ) ) ) ))).
% 135.61/20.01 thf(zf_stmt_3, negated_conjecture,
% 135.61/20.01 (~( ?[W0:$i]:
% 135.61/20.01 ( ( ( W0 ) != ( sz00 ) ) &
% 135.61/20.01 ( aElementOf0 @
% 135.61/20.01 W0 @ ( sdtpldt1 @ ( slsdtgt0 @ xa ) @ ( slsdtgt0 @ xb ) ) ) ) )),
% 135.61/20.01 inference('cnf.neg', [status(esa)], [m__])).
% 135.61/20.01 thf(zip_derived_cl104, plain,
% 135.61/20.01 (![X0 : $i]:
% 135.61/20.01 (((X0) = (sz00))
% 135.61/20.01 | ~ (aElementOf0 @ X0 @
% 135.61/20.01 (sdtpldt1 @ (slsdtgt0 @ xa) @ (slsdtgt0 @ xb))))),
% 135.61/20.01 inference('cnf', [status(esa)], [zf_stmt_3])).
% 135.61/20.01 thf(zip_derived_cl98, plain,
% 135.61/20.01 (((xI) = (sdtpldt1 @ (slsdtgt0 @ xa) @ (slsdtgt0 @ xb)))),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2174])).
% 135.61/20.01 thf(zip_derived_cl105, plain,
% 135.61/20.01 (![X0 : $i]: (((X0) = (sz00)) | ~ (aElementOf0 @ X0 @ xI))),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl104, zip_derived_cl98])).
% 135.61/20.01 thf(zip_derived_cl126487, plain, (((xb) = (sz00))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl126478, zip_derived_cl105])).
% 135.61/20.01 thf(zip_derived_cl126505, plain,
% 135.61/20.01 (((xI) = (sdtpldt1 @ (slsdtgt0 @ xa) @ (slsdtgt0 @ sz00)))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl98, zip_derived_cl126487])).
% 135.61/20.01 thf(zip_derived_cl192837, plain,
% 135.61/20.01 ((~ (aSet0 @ (slsdtgt0 @ xa))
% 135.61/20.01 | ~ (aSet0 @ (slsdtgt0 @ sz00))
% 135.61/20.01 | (aElementOf0 @ xa @ xI))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl192790, zip_derived_cl126505])).
% 135.61/20.01 thf(zip_derived_cl192853, plain,
% 135.61/20.01 ((~ (aElement0 @ xa)
% 135.61/20.01 | (aElementOf0 @ xa @ xI)
% 135.61/20.01 | ~ (aSet0 @ (slsdtgt0 @ sz00)))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl120, zip_derived_cl192837])).
% 135.61/20.01 thf(zip_derived_cl95, plain, ( (aElement0 @ xa)),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2091])).
% 135.61/20.01 thf(zip_derived_cl192866, plain,
% 135.61/20.01 (( (aElementOf0 @ xa @ xI) | ~ (aSet0 @ (slsdtgt0 @ sz00)))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl192853, zip_derived_cl95])).
% 135.61/20.01 thf(zip_derived_cl192868, plain,
% 135.61/20.01 ((~ (aElement0 @ sz00) | (aElementOf0 @ xa @ xI))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl120, zip_derived_cl192866])).
% 135.61/20.01 thf(zip_derived_cl1, plain, ( (aElement0 @ sz00)),
% 135.61/20.01 inference('cnf', [status(esa)], [mSortsC])).
% 135.61/20.01 thf(zip_derived_cl192883, plain, ( (aElementOf0 @ xa @ xI)),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl192868, zip_derived_cl1])).
% 135.61/20.01 thf(zip_derived_cl105, plain,
% 135.61/20.01 (![X0 : $i]: (((X0) = (sz00)) | ~ (aElementOf0 @ X0 @ xI))),
% 135.61/20.01 inference('demod', [status(thm)], [zip_derived_cl104, zip_derived_cl98])).
% 135.61/20.01 thf(zip_derived_cl192897, plain, (((xa) = (sz00))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl192883, zip_derived_cl105])).
% 135.61/20.01 thf(m__2110, axiom, (( ( xa ) != ( sz00 ) ) | ( ( xb ) != ( sz00 ) ))).
% 135.61/20.01 thf(zip_derived_cl96, plain, ((((xa) != (sz00)) | ((xb) != (sz00)))),
% 135.61/20.01 inference('cnf', [status(esa)], [m__2110])).
% 135.61/20.01 thf(zip_derived_cl126487, plain, (((xb) = (sz00))),
% 135.61/20.01 inference('sup-', [status(thm)],
% 135.61/20.01 [zip_derived_cl126478, zip_derived_cl105])).
% 135.61/20.01 thf(zip_derived_cl126502, plain, ((((xa) != (sz00)) | ((sz00) != (sz00)))),
% 135.61/20.01 inference('demod', [status(thm)],
% 135.61/20.01 [zip_derived_cl96, zip_derived_cl126487])).
% 135.61/20.01 thf(zip_derived_cl126503, plain, (((xa) != (sz00))),
% 135.61/20.01 inference('simplify', [status(thm)], [zip_derived_cl126502])).
% 135.61/20.01 thf(zip_derived_cl192921, plain, ($false),
% 135.61/20.01 inference('simplify_reflect-', [status(thm)],
% 135.61/20.01 [zip_derived_cl192897, zip_derived_cl126503])).
% 135.61/20.01
% 135.61/20.01 % SZS output end Refutation
% 135.61/20.01
% 135.61/20.01
% 135.61/20.01 % Terminating...
% 136.02/20.09 % Runner terminated.
% 136.02/20.10 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------