%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEV609+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.s9ZFv93T7J true
% Computer : n004.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 : Tue May 5 06:56:14 PM UTC 2026
% Result : Theorem 23.92s 4.05s
% Output : Refutation 23.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SEV609+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.15 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.s9ZFv93T7J true
% 0.17/0.36 % Computer : n004.cluster.edu
% 0.17/0.36 % Model : x86_64 x86_64
% 0.17/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.36 % Memory : 8042.1875MB
% 0.17/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.36 % CPULimit : 300
% 0.17/0.36 % WCLimit : 300
% 0.17/0.36 % DateTime : Tue May 5 05:29:17 EDT 2026
% 0.17/0.36 % CPUTime :
% 0.17/0.36 % Running portfolio for 300 s
% 0.17/0.36 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.36 % Number of cores: 8
% 0.17/0.36 % Python version: Python 3.6.8
% 0.17/0.37 % Running in FO mode
% 0.52/0.65 % Total configuration time : 435
% 0.52/0.65 % Estimated wc time : 1092
% 0.52/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.71 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.73 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.73 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.75 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.54/0.76 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.54/0.76 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.54/0.76 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 23.92/4.05 % Solved by fo/fo3_bce.sh.
% 23.92/4.05 % BCE start: 535
% 23.92/4.05 % BCE eliminated: 157
% 23.92/4.05 % PE start: 378
% 23.92/4.05 logic: eq
% 23.92/4.05 % PE eliminated: 19
% 23.92/4.05 % done 2094 iterations in 3.299s
% 23.92/4.05 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 23.92/4.05 % SZS output start Refutation
% 23.92/4.05 thf(sk__140_type, type, sk__140: $i).
% 23.92/4.05 thf(cLambda_2eResiduals_2eresiduals___24a3_type, type, cLambda_2eResiduals_2eresiduals___24a3:
% 23.92/4.05 $i > $i > $i > $o).
% 23.92/4.05 thf(sk__139_type, type, sk__139: $i).
% 23.92/4.05 thf(sk__138_type, type, sk__138: $i).
% 23.92/4.05 thf(sk__141_type, type, sk__141: $i).
% 23.92/4.05 thf(cLambda_2eRedexes_2ecomp___24a2_type, type, cLambda_2eRedexes_2ecomp___24a2:
% 23.92/4.05 $i > $i > $o).
% 23.92/4.05 thf(cLambda_2eRedexes_2eregular___24a1_type, type, cLambda_2eRedexes_2eregular___24a1:
% 23.92/4.05 $i > $o).
% 23.92/4.05 thf(sk__136_type, type, sk__136: $i).
% 23.92/4.05 thf(sk__135_type, type, sk__135: $i > $i > $i).
% 23.92/4.05 thf(sk__137_type, type, sk__137: $i).
% 23.92/4.05 thf(cLambda_2eRedexes_2esub___24a2_type, type, cLambda_2eRedexes_2esub___24a2:
% 23.92/4.05 $i > $i > $o).
% 23.92/4.05 thf(cLambda_2eRedexes_2eredexes___24t_type, type, cLambda_2eRedexes_2eredexes___24t:
% 23.92/4.05 $i > $o).
% 23.92/4.05 thf('_HAMMER_GOAL', conjecture,
% 23.92/4.05 (![V0__U:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V0__U ) =>
% 23.92/4.05 ( ![V1__V:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V1__V ) =>
% 23.92/4.05 ( ![V2__W:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V2__W ) =>
% 23.92/4.05 ( ( cLambda_2eRedexes_2esub___24a2 @ V1__V @ V0__U ) =>
% 23.92/4.05 ( ( cLambda_2eRedexes_2eregular___24a1 @ V0__U ) =>
% 23.92/4.05 ( ![V5__UV:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V5__UV ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V0__U @ V1__V @ V5__UV ) =>
% 23.92/4.05 ( ![V7__WV:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V7__WV ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V2__W @ V1__V @ V7__WV ) =>
% 23.92/4.05 ( ![V9__WU:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V9__WU ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V7__WV @ V5__UV @ V9__WU ) =>
% 23.92/4.05 ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V2__W @ V0__U @ V9__WU ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))).
% 23.92/4.05 thf(zf_stmt_0, negated_conjecture,
% 23.92/4.05 (~( ![V0__U:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V0__U ) =>
% 23.92/4.05 ( ![V1__V:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V1__V ) =>
% 23.92/4.05 ( ![V2__W:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V2__W ) =>
% 23.92/4.05 ( ( cLambda_2eRedexes_2esub___24a2 @ V1__V @ V0__U ) =>
% 23.92/4.05 ( ( cLambda_2eRedexes_2eregular___24a1 @ V0__U ) =>
% 23.92/4.05 ( ![V5__UV:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V5__UV ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V0__U @ V1__V @ V5__UV ) =>
% 23.92/4.05 ( ![V7__WV:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V7__WV ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V2__W @ V1__V @ V7__WV ) =>
% 23.92/4.05 ( ![V9__WU:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @
% 23.92/4.05 V9__WU ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3
% 23.92/4.05 @ V7__WV @ V5__UV @ V9__WU ) =>
% 23.92/4.05 ( cLambda_2eResiduals_2eresiduals___24a3
% 23.92/4.05 @ V2__W @ V0__U @ V9__WU ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )),
% 23.92/4.05 inference('cnf.neg', [status(esa)], [_HAMMER_GOAL])).
% 23.92/4.05 thf(zip_derived_cl528, plain,
% 23.92/4.05 (~ (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ sk__136 @ sk__141)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(Lambda.Residuals.residuals_intro, axiom,
% 23.92/4.05 (![V0__U:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V0__U ) =>
% 23.92/4.05 ( ![V1__V:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V1__V ) =>
% 23.92/4.05 ( ( cLambda_2eRedexes_2ecomp___24a2 @ V0__U @ V1__V ) =>
% 23.92/4.05 ( ( cLambda_2eRedexes_2eregular___24a1 @ V1__V ) =>
% 23.92/4.05 ( ?[V4__W:$i]:
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V0__U @ V1__V @ V4__W ) &
% 23.92/4.05 ( cLambda_2eRedexes_2eredexes___24t @ V4__W ) ) ) ) ) ) ) ))).
% 23.92/4.05 thf(zip_derived_cl500, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eregular___24a1 @ X0)
% 23.92/4.05 | (cLambda_2eRedexes_2eredexes___24t @ (sk__135 @ X0 @ X1))
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ X1 @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1))),
% 23.92/4.05 inference('cnf', [status(esa)], [Lambda.Residuals.residuals_intro])).
% 23.92/4.05 thf(zip_derived_cl499, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eregular___24a1 @ X0)
% 23.92/4.05 | (cLambda_2eResiduals_2eresiduals___24a3 @ X1 @ X0 @
% 23.92/4.05 (sk__135 @ X0 @ X1))
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ X1 @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1))),
% 23.92/4.05 inference('cnf', [status(esa)], [Lambda.Residuals.residuals_intro])).
% 23.92/4.05 thf(zip_derived_cl527, plain,
% 23.92/4.05 ( (cLambda_2eResiduals_2eresiduals___24a3 @ sk__140 @ sk__139 @ sk__141)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(Lambda.Residuals.residuals_function, axiom,
% 23.92/4.05 (![V0__U:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V0__U ) =>
% 23.92/4.05 ( ![V1__V:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V1__V ) =>
% 23.92/4.05 ( ![V2__W:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V2__W ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V0__U @ V1__V @ V2__W ) =>
% 23.92/4.05 ( ![V4__W_27:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V4__W_27 ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V0__U @ V1__V @ V4__W_27 ) =>
% 23.92/4.05 ( ( V4__W_27 ) = ( V2__W ) ) ) ) ) ) ) ) ) ) ))).
% 23.92/4.05 thf(zip_derived_cl441, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ X1 @ X0 @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X3)
% 23.92/4.05 | ((X3) = (X2))
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ X1 @ X0 @ X3)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1))),
% 23.92/4.05 inference('cnf', [status(esa)], [Lambda.Residuals.residuals_function])).
% 23.92/4.05 thf(zip_derived_cl5856, plain,
% 23.92/4.05 (![X0 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ sk__140)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__141)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ sk__140 @ sk__139 @ X0)
% 23.92/4.05 | ((X0) = (sk__141))
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__139))),
% 23.92/4.05 inference('sup-', [status(thm)], [zip_derived_cl527, zip_derived_cl441])).
% 23.92/4.05 thf(zip_derived_cl526, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__140)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl529, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__141)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl531, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__139)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl5862, plain,
% 23.92/4.05 (![X0 : $i]:
% 23.92/4.05 (~ (cLambda_2eResiduals_2eresiduals___24a3 @ sk__140 @ sk__139 @ X0)
% 23.92/4.05 | ((X0) = (sk__141))
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X0))),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl5856, zip_derived_cl526, zip_derived_cl529,
% 23.92/4.05 zip_derived_cl531])).
% 23.92/4.05 thf(zip_derived_cl525, plain,
% 23.92/4.05 ( (cLambda_2eResiduals_2eresiduals___24a3 @ sk__136 @ sk__137 @ sk__139)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl530, plain,
% 23.92/4.05 ( (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ sk__137 @ sk__140)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(Cube.prism1, axiom,
% 23.92/4.05 (![V0__U:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V0__U ) =>
% 23.92/4.05 ( ![V1__V:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V1__V ) =>
% 23.92/4.05 ( ![V2__W:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V2__W ) =>
% 23.92/4.05 ( ( cLambda_2eRedexes_2esub___24a2 @ V1__V @ V0__U ) =>
% 23.92/4.05 ( ![V4__UV:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V4__UV ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V0__U @ V1__V @ V4__UV ) =>
% 23.92/4.05 ( ![V6__WV:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V6__WV ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V2__W @ V1__V @ V6__WV ) =>
% 23.92/4.05 ( ![V8__WU:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V8__WU ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V2__W @ V0__U @ V8__WU ) =>
% 23.92/4.05 ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V6__WV @ V4__UV @ V8__WU ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))).
% 23.92/4.05 thf(zip_derived_cl297, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2esub___24a2 @ X0 @ X1)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X2)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ X3 @ X0 @ X4)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X5)
% 23.92/4.05 | (cLambda_2eResiduals_2eresiduals___24a3 @ X4 @ X2 @ X5)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ X3 @ X1 @ X5)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X4)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ X1 @ X0 @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X3)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1))),
% 23.92/4.05 inference('cnf', [status(esa)], [Cube.prism1])).
% 23.92/4.05 thf(zip_derived_cl5328, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__138)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ X0 @ sk__137 @ X1)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__140)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ X0 @ X2)
% 23.92/4.05 | (cLambda_2eResiduals_2eresiduals___24a3 @ sk__140 @ X1 @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2esub___24a2 @ sk__137 @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__137))),
% 23.92/4.05 inference('sup-', [status(thm)], [zip_derived_cl530, zip_derived_cl297])).
% 23.92/4.05 thf(zip_derived_cl524, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__138)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl526, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__140)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl534, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__137)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl5338, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ X0 @ sk__137 @ X1)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ X0 @ X2)
% 23.92/4.05 | (cLambda_2eResiduals_2eresiduals___24a3 @ sk__140 @ X1 @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2esub___24a2 @ sk__137 @ X0))),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl5328, zip_derived_cl524, zip_derived_cl526,
% 23.92/4.05 zip_derived_cl534])).
% 23.92/4.05 thf(zip_derived_cl13904, plain,
% 23.92/4.05 (![X0 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2esub___24a2 @ sk__137 @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__139)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | (cLambda_2eResiduals_2eresiduals___24a3 @ sk__140 @ sk__139 @ X0)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ sk__136 @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__136))),
% 23.92/4.05 inference('sup-', [status(thm)], [zip_derived_cl525, zip_derived_cl5338])).
% 23.92/4.05 thf(zip_derived_cl533, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2esub___24a2 @ sk__137 @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl531, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__139)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl523, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl13910, plain,
% 23.92/4.05 (![X0 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | (cLambda_2eResiduals_2eresiduals___24a3 @ sk__140 @ sk__139 @ X0)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ sk__136 @ X0))),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl13904, zip_derived_cl533, zip_derived_cl531,
% 23.92/4.05 zip_derived_cl523])).
% 23.92/4.05 thf(zip_derived_cl13932, plain,
% 23.92/4.05 (![X0 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ((X0) = (sk__141))
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ sk__136 @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X0))),
% 23.92/4.05 inference('sup+', [status(thm)],
% 23.92/4.05 [zip_derived_cl5862, zip_derived_cl13910])).
% 23.92/4.05 thf(zip_derived_cl13947, plain,
% 23.92/4.05 (![X0 : $i]:
% 23.92/4.05 (~ (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ sk__136 @ X0)
% 23.92/4.05 | ((X0) = (sk__141))
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X0))),
% 23.92/4.05 inference('simplify', [status(thm)], [zip_derived_cl13932])).
% 23.92/4.05 thf(zip_derived_cl13974, plain,
% 23.92/4.05 ((~ (cLambda_2eRedexes_2eredexes___24t @ sk__138)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ sk__138 @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eregular___24a1 @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ (sk__135 @ sk__136 @ sk__138))
% 23.92/4.05 | ((sk__135 @ sk__136 @ sk__138) = (sk__141)))),
% 23.92/4.05 inference('sup-', [status(thm)], [zip_derived_cl499, zip_derived_cl13947])).
% 23.92/4.05 thf(zip_derived_cl524, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__138)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl530, plain,
% 23.92/4.05 ( (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ sk__137 @ sk__140)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(Lambda.Residuals.residuals_comp, axiom,
% 23.92/4.05 (![V0__U:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V0__U ) =>
% 23.92/4.05 ( ![V1__V:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V1__V ) =>
% 23.92/4.05 ( ![V2__W:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V2__W ) =>
% 23.92/4.05 ( ( cLambda_2eResiduals_2eresiduals___24a3 @
% 23.92/4.05 V0__U @ V1__V @ V2__W ) =>
% 23.92/4.05 ( cLambda_2eRedexes_2ecomp___24a2 @ V0__U @ V1__V ) ) ) ) ) ) ))).
% 23.92/4.05 thf(zip_derived_cl440, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | (cLambda_2eRedexes_2ecomp___24a2 @ X1 @ X0)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ X1 @ X0 @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1))),
% 23.92/4.05 inference('cnf', [status(esa)], [Lambda.Residuals.residuals_comp])).
% 23.92/4.05 thf(zip_derived_cl5095, plain,
% 23.92/4.05 ((~ (cLambda_2eRedexes_2eredexes___24t @ sk__138)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__140)
% 23.92/4.05 | (cLambda_2eRedexes_2ecomp___24a2 @ sk__138 @ sk__137)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__137))),
% 23.92/4.05 inference('sup-', [status(thm)], [zip_derived_cl530, zip_derived_cl440])).
% 23.92/4.05 thf(zip_derived_cl524, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__138)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl526, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__140)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl534, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__137)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl5098, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2ecomp___24a2 @ sk__138 @ sk__137)),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl5095, zip_derived_cl524, zip_derived_cl526,
% 23.92/4.05 zip_derived_cl534])).
% 23.92/4.05 thf(zip_derived_cl525, plain,
% 23.92/4.05 ( (cLambda_2eResiduals_2eresiduals___24a3 @ sk__136 @ sk__137 @ sk__139)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl440, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | (cLambda_2eRedexes_2ecomp___24a2 @ X1 @ X0)
% 23.92/4.05 | ~ (cLambda_2eResiduals_2eresiduals___24a3 @ X1 @ X0 @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X2)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1))),
% 23.92/4.05 inference('cnf', [status(esa)], [Lambda.Residuals.residuals_comp])).
% 23.92/4.05 thf(zip_derived_cl5094, plain,
% 23.92/4.05 ((~ (cLambda_2eRedexes_2eredexes___24t @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__139)
% 23.92/4.05 | (cLambda_2eRedexes_2ecomp___24a2 @ sk__136 @ sk__137)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__137))),
% 23.92/4.05 inference('sup-', [status(thm)], [zip_derived_cl525, zip_derived_cl440])).
% 23.92/4.05 thf(zip_derived_cl523, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl531, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__139)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl534, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__137)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl5097, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2ecomp___24a2 @ sk__136 @ sk__137)),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl5094, zip_derived_cl523, zip_derived_cl531,
% 23.92/4.05 zip_derived_cl534])).
% 23.92/4.05 thf(Lambda.Redexes.comp_sym, axiom,
% 23.92/4.05 (![V0__U:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V0__U ) =>
% 23.92/4.05 ( ![V1__V:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V1__V ) =>
% 23.92/4.05 ( ( cLambda_2eRedexes_2ecomp___24a2 @ V0__U @ V1__V ) =>
% 23.92/4.05 ( cLambda_2eRedexes_2ecomp___24a2 @ V1__V @ V0__U ) ) ) ) ))).
% 23.92/4.05 thf(zip_derived_cl340, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | (cLambda_2eRedexes_2ecomp___24a2 @ X0 @ X1)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ X1 @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1))),
% 23.92/4.05 inference('cnf', [status(esa)], [Lambda.Redexes.comp_sym])).
% 23.92/4.05 thf(zip_derived_cl5103, plain,
% 23.92/4.05 ((~ (cLambda_2eRedexes_2eredexes___24t @ sk__136)
% 23.92/4.05 | (cLambda_2eRedexes_2ecomp___24a2 @ sk__137 @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__137))),
% 23.92/4.05 inference('sup-', [status(thm)], [zip_derived_cl5097, zip_derived_cl340])).
% 23.92/4.05 thf(zip_derived_cl523, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl534, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__137)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl5104, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2ecomp___24a2 @ sk__137 @ sk__136)),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl5103, zip_derived_cl523, zip_derived_cl534])).
% 23.92/4.05 thf(Lambda.Redexes.comp_trans, axiom,
% 23.92/4.05 (![V0__U:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V0__U ) =>
% 23.92/4.05 ( ![V1__V:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V1__V ) =>
% 23.92/4.05 ( ( cLambda_2eRedexes_2ecomp___24a2 @ V0__U @ V1__V ) =>
% 23.92/4.05 ( ![V3__W:$i]:
% 23.92/4.05 ( ( cLambda_2eRedexes_2eredexes___24t @ V3__W ) =>
% 23.92/4.05 ( ( cLambda_2eRedexes_2ecomp___24a2 @ V1__V @ V3__W ) =>
% 23.92/4.05 ( cLambda_2eRedexes_2ecomp___24a2 @ V0__U @ V3__W ) ) ) ) ) ) ) ))).
% 23.92/4.05 thf(zip_derived_cl341, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i, X2 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ X0 @ X1)
% 23.92/4.05 | (cLambda_2eRedexes_2ecomp___24a2 @ X2 @ X1)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ X2 @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X2))),
% 23.92/4.05 inference('cnf', [status(esa)], [Lambda.Redexes.comp_trans])).
% 23.92/4.05 thf(zip_derived_cl5148, plain,
% 23.92/4.05 (![X0 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ X0 @ sk__137)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__136)
% 23.92/4.05 | (cLambda_2eRedexes_2ecomp___24a2 @ X0 @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__137))),
% 23.92/4.05 inference('sup-', [status(thm)], [zip_derived_cl5104, zip_derived_cl341])).
% 23.92/4.05 thf(zip_derived_cl523, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl534, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__137)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl5160, plain,
% 23.92/4.05 (![X0 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ X0 @ sk__137)
% 23.92/4.05 | (cLambda_2eRedexes_2ecomp___24a2 @ X0 @ sk__136))),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl5148, zip_derived_cl523, zip_derived_cl534])).
% 23.92/4.05 thf(zip_derived_cl5170, plain,
% 23.92/4.05 (( (cLambda_2eRedexes_2ecomp___24a2 @ sk__138 @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__138))),
% 23.92/4.05 inference('sup-', [status(thm)], [zip_derived_cl5098, zip_derived_cl5160])).
% 23.92/4.05 thf(zip_derived_cl524, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__138)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl5173, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2ecomp___24a2 @ sk__138 @ sk__136)),
% 23.92/4.05 inference('demod', [status(thm)], [zip_derived_cl5170, zip_derived_cl524])).
% 23.92/4.05 thf(zip_derived_cl532, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eregular___24a1 @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl523, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl13975, plain,
% 23.92/4.05 ((~ (cLambda_2eRedexes_2eredexes___24t @ (sk__135 @ sk__136 @ sk__138))
% 23.92/4.05 | ((sk__135 @ sk__136 @ sk__138) = (sk__141)))),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl13974, zip_derived_cl524, zip_derived_cl5173,
% 23.92/4.05 zip_derived_cl532, zip_derived_cl523])).
% 23.92/4.05 thf(zip_derived_cl13978, plain,
% 23.92/4.05 ((~ (cLambda_2eRedexes_2eredexes___24t @ sk__138)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ sk__138 @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eregular___24a1 @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__136)
% 23.92/4.05 | ((sk__135 @ sk__136 @ sk__138) = (sk__141)))),
% 23.92/4.05 inference('sup-', [status(thm)], [zip_derived_cl500, zip_derived_cl13975])).
% 23.92/4.05 thf(zip_derived_cl524, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__138)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl5173, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2ecomp___24a2 @ sk__138 @ sk__136)),
% 23.92/4.05 inference('demod', [status(thm)], [zip_derived_cl5170, zip_derived_cl524])).
% 23.92/4.05 thf(zip_derived_cl532, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eregular___24a1 @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl523, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl13979, plain,
% 23.92/4.05 (((sk__135 @ sk__136 @ sk__138) = (sk__141))),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl13978, zip_derived_cl524, zip_derived_cl5173,
% 23.92/4.05 zip_derived_cl532, zip_derived_cl523])).
% 23.92/4.05 thf(zip_derived_cl499, plain,
% 23.92/4.05 (![X0 : $i, X1 : $i]:
% 23.92/4.05 (~ (cLambda_2eRedexes_2eredexes___24t @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eregular___24a1 @ X0)
% 23.92/4.05 | (cLambda_2eResiduals_2eresiduals___24a3 @ X1 @ X0 @
% 23.92/4.05 (sk__135 @ X0 @ X1))
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ X1 @ X0)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ X1))),
% 23.92/4.05 inference('cnf', [status(esa)], [Lambda.Residuals.residuals_intro])).
% 23.92/4.05 thf(zip_derived_cl13981, plain,
% 23.92/4.05 (( (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ sk__136 @ sk__141)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__138)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2ecomp___24a2 @ sk__138 @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eregular___24a1 @ sk__136)
% 23.92/4.05 | ~ (cLambda_2eRedexes_2eredexes___24t @ sk__136))),
% 23.92/4.05 inference('sup+', [status(thm)], [zip_derived_cl13979, zip_derived_cl499])).
% 23.92/4.05 thf(zip_derived_cl524, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__138)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl5173, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2ecomp___24a2 @ sk__138 @ sk__136)),
% 23.92/4.05 inference('demod', [status(thm)], [zip_derived_cl5170, zip_derived_cl524])).
% 23.92/4.05 thf(zip_derived_cl532, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eregular___24a1 @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl523, plain,
% 23.92/4.05 ( (cLambda_2eRedexes_2eredexes___24t @ sk__136)),
% 23.92/4.05 inference('cnf', [status(esa)], [zf_stmt_0])).
% 23.92/4.05 thf(zip_derived_cl13983, plain,
% 23.92/4.05 ( (cLambda_2eResiduals_2eresiduals___24a3 @ sk__138 @ sk__136 @ sk__141)),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl13981, zip_derived_cl524, zip_derived_cl5173,
% 23.92/4.05 zip_derived_cl532, zip_derived_cl523])).
% 23.92/4.05 thf(zip_derived_cl13985, plain, ($false),
% 23.92/4.05 inference('demod', [status(thm)],
% 23.92/4.05 [zip_derived_cl528, zip_derived_cl13983])).
% 23.92/4.05
% 23.92/4.05 % SZS output end Refutation
% 23.92/4.05
% 23.92/4.05
% 23.92/4.05 % Terminating...
% 24.62/4.16 % Runner terminated.
% 24.62/4.18 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------