%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEV667+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.KxPHTRjRN8 true
% Computer : n027.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:18 PM UTC 2026
% Result : Theorem 3.62s 1.15s
% Output : Refutation 3.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV667+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.KxPHTRjRN8 true
% 0.16/0.35 % Computer : n027.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % WCLimit : 300
% 0.16/0.35 % DateTime : Tue May 5 08:03:04 EDT 2026
% 0.16/0.35 % CPUTime :
% 0.16/0.35 % Running portfolio for 300 s
% 0.16/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.35 % Number of cores: 8
% 0.20/0.35 % Python version: Python 3.6.8
% 0.20/0.36 % Running in FO mode
% 0.53/0.64 % Total configuration time : 435
% 0.53/0.64 % Estimated wc time : 1092
% 0.53/0.64 % 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.74 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.74 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.54/0.75 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.54/0.76 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.54/0.76 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 3.01/1.02 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 3.62/1.15 % Solved by fo/fo7.sh.
% 3.62/1.15 % done 327 iterations in 0.383s
% 3.62/1.15 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 3.62/1.15 % SZS output start Refutation
% 3.62/1.15 thf(sk__19_type, type, sk__19: $i).
% 3.62/1.15 thf(cCoq_2eRelations_2eRelation__Definitions_2erelation___24t_type, type,
% 3.62/1.15 cCoq_2eRelations_2eRelation__Definitions_2erelation___24t: $i > $i > $o).
% 3.62/1.15 thf(cS___24a2_type, type, cS___24a2: $i > $i > $o).
% 3.62/1.15 thf(cQuotients_2eInducedFunction2_2eprojf_type, type, cQuotients_2eInducedFunction2_2eprojf:
% 3.62/1.15 $i).
% 3.62/1.15 thf(cS_type, type, cS: $i).
% 3.62/1.15 thf(cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2_type, type,
% 3.62/1.15 cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2: $i > $i > $o).
% 3.62/1.15 thf(cf_type, type, cf: $i).
% 3.62/1.15 thf(cB_type, type, cB: $i).
% 3.62/1.15 thf(p_type, type, p: $i > $o).
% 3.62/1.15 thf(cf___24a1_type, type, cf___24a1: $i > $i).
% 3.62/1.15 thf(cQuotients_2eInducedFunction2_2eprojf___24a1_type, type, cQuotients_2eInducedFunction2_2eprojf___24a1:
% 3.62/1.15 $i > $i).
% 3.62/1.15 thf(cType___24t_type, type, cType___24t: $i > $o).
% 3.62/1.15 thf(cA___24t_type, type, cA___24t: $i > $o).
% 3.62/1.15 thf(sk__20_type, type, sk__20: $i).
% 3.62/1.15 thf(cR___24a2_type, type, cR___24a2: $i > $i > $o).
% 3.62/1.15 thf(c_24__type__163663___24t_type, type, c_24__type__163663___24t: $i > $o).
% 3.62/1.15 thf(happ_type, type, happ: $i > $i > $i).
% 3.62/1.15 thf(cB___24t_type, type, cB___24t: $i > $o).
% 3.62/1.15 thf(t_type, type, t: $i > $i > $o).
% 3.62/1.15 thf(cQuotients_2equotient__projection___24a3_type, type, cQuotients_2equotient__projection___24a3:
% 3.62/1.15 $i > $i > $i > $i).
% 3.62/1.15 thf('$_type_163663', axiom,
% 3.62/1.15 (![Vvar__163664:$i]:
% 3.62/1.15 ( ( c_24__type__163663___24t @ Vvar__163664 ) <=>
% 3.62/1.15 ( ![Vv__CANONICAL__0:$i]:
% 3.62/1.15 ( ( cA___24t @ Vv__CANONICAL__0 ) =>
% 3.62/1.15 ( cB___24t @ ( happ @ Vvar__163664 @ Vv__CANONICAL__0 ) ) ) ) ))).
% 3.62/1.15 thf(zip_derived_cl1, plain,
% 3.62/1.15 (![X0 : $i, X1 : $i]:
% 3.62/1.15 (~ (cA___24t @ X0)
% 3.62/1.15 | (cB___24t @ (happ @ X1 @ X0))
% 3.62/1.15 | ~ (c_24__type__163663___24t @ X1))),
% 3.62/1.15 inference('cnf', [status(esa)], [$_type_163663])).
% 3.62/1.15 thf('_HAMMER_GOAL', conjecture,
% 3.62/1.15 (![V0__a1:$i]:
% 3.62/1.15 ( ( cA___24t @ V0__a1 ) =>
% 3.62/1.15 ( ![V1__a2:$i]:
% 3.62/1.15 ( ( cA___24t @ V1__a2 ) =>
% 3.62/1.15 ( ( cR___24a2 @ V0__a1 @ V1__a2 ) =>
% 3.62/1.15 ( ( cQuotients_2eInducedFunction2_2eprojf___24a1 @ V0__a1 ) =
% 3.62/1.15 ( cQuotients_2eInducedFunction2_2eprojf___24a1 @ V1__a2 ) ) ) ) ) ))).
% 3.62/1.15 thf(zf_stmt_0, negated_conjecture,
% 3.62/1.15 (~( ![V0__a1:$i]:
% 3.62/1.15 ( ( cA___24t @ V0__a1 ) =>
% 3.62/1.15 ( ![V1__a2:$i]:
% 3.62/1.15 ( ( cA___24t @ V1__a2 ) =>
% 3.62/1.15 ( ( cR___24a2 @ V0__a1 @ V1__a2 ) =>
% 3.62/1.15 ( ( cQuotients_2eInducedFunction2_2eprojf___24a1 @ V0__a1 ) =
% 3.62/1.15 ( cQuotients_2eInducedFunction2_2eprojf___24a1 @ V1__a2 ) ) ) ) ) ) )),
% 3.62/1.15 inference('cnf.neg', [status(esa)], [_HAMMER_GOAL])).
% 3.62/1.15 thf(zip_derived_cl84, plain, ( (cA___24t @ sk__19)),
% 3.62/1.15 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.62/1.15 thf(zip_derived_cl119, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 (~ (c_24__type__163663___24t @ X0)
% 3.62/1.15 | (cB___24t @ (happ @ X0 @ sk__19)))),
% 3.62/1.15 inference('sup+', [status(thm)], [zip_derived_cl1, zip_derived_cl84])).
% 3.62/1.15 thf('$tdef_B', axiom,
% 3.62/1.15 (![V_24Y:$i]: ( ( cB___24t @ V_24Y ) <=> ( t @ V_24Y @ cB ) ))).
% 3.62/1.15 thf(zip_derived_cl76, plain,
% 3.62/1.15 (![X0 : $i]: ( (t @ X0 @ cB) | ~ (cB___24t @ X0))),
% 3.62/1.15 inference('cnf', [status(esa)], [$tdef_B])).
% 3.62/1.15 thf(zip_derived_cl128, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 (~ (c_24__type__163663___24t @ X0) | (t @ (happ @ X0 @ sk__19) @ cB))),
% 3.62/1.15 inference('sup-', [status(thm)], [zip_derived_cl119, zip_derived_cl76])).
% 3.62/1.15 thf(zip_derived_cl1, plain,
% 3.62/1.15 (![X0 : $i, X1 : $i]:
% 3.62/1.15 (~ (cA___24t @ X0)
% 3.62/1.15 | (cB___24t @ (happ @ X1 @ X0))
% 3.62/1.15 | ~ (c_24__type__163663___24t @ X1))),
% 3.62/1.15 inference('cnf', [status(esa)], [$_type_163663])).
% 3.62/1.15 thf(zip_derived_cl87, plain, ( (cA___24t @ sk__20)),
% 3.62/1.15 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.62/1.15 thf(zip_derived_cl120, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 (~ (c_24__type__163663___24t @ X0)
% 3.62/1.15 | (cB___24t @ (happ @ X0 @ sk__20)))),
% 3.62/1.15 inference('sup+', [status(thm)], [zip_derived_cl1, zip_derived_cl87])).
% 3.62/1.15 thf(zip_derived_cl76, plain,
% 3.62/1.15 (![X0 : $i]: ( (t @ X0 @ cB) | ~ (cB___24t @ X0))),
% 3.62/1.15 inference('cnf', [status(esa)], [$tdef_B])).
% 3.62/1.15 thf(zip_derived_cl130, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 (~ (c_24__type__163663___24t @ X0) | (t @ (happ @ X0 @ sk__20) @ cB))),
% 3.62/1.15 inference('sup-', [status(thm)], [zip_derived_cl120, zip_derived_cl76])).
% 3.62/1.15 thf(equivS, axiom,
% 3.62/1.15 (cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2 @ cB @ cS)).
% 3.62/1.15 thf(zip_derived_cl66, plain,
% 3.62/1.15 ( (cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2 @ cB @
% 3.62/1.15 cS)),
% 3.62/1.15 inference('cnf', [status(esa)], [equivS])).
% 3.62/1.15 thf(zip_derived_cl85, plain, ( (cR___24a2 @ sk__19 @ sk__20)),
% 3.62/1.15 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.62/1.15 thf(well_defined2, axiom,
% 3.62/1.15 (![V0__a1:$i]:
% 3.62/1.15 ( ( cA___24t @ V0__a1 ) =>
% 3.62/1.15 ( ![V1__a2:$i]:
% 3.62/1.15 ( ( cA___24t @ V1__a2 ) =>
% 3.62/1.15 ( ( cR___24a2 @ V0__a1 @ V1__a2 ) =>
% 3.62/1.15 ( cS___24a2 @ ( cf___24a1 @ V0__a1 ) @ ( cf___24a1 @ V1__a2 ) ) ) ) ) ))).
% 3.62/1.15 thf(zip_derived_cl67, plain,
% 3.62/1.15 (![X0 : $i, X1 : $i]:
% 3.62/1.15 (~ (cA___24t @ X0)
% 3.62/1.15 | (cS___24a2 @ (cf___24a1 @ X1) @ (cf___24a1 @ X0))
% 3.62/1.15 | ~ (cR___24a2 @ X1 @ X0)
% 3.62/1.15 | ~ (cA___24t @ X1))),
% 3.62/1.15 inference('cnf', [status(esa)], [well_defined2])).
% 3.62/1.15 thf(zip_derived_cl137, plain,
% 3.62/1.15 ((~ (cA___24t @ sk__19)
% 3.62/1.15 | (cS___24a2 @ (cf___24a1 @ sk__19) @ (cf___24a1 @ sk__20))
% 3.62/1.15 | ~ (cA___24t @ sk__20))),
% 3.62/1.15 inference('sup-', [status(thm)], [zip_derived_cl85, zip_derived_cl67])).
% 3.62/1.15 thf(zip_derived_cl84, plain, ( (cA___24t @ sk__19)),
% 3.62/1.15 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.62/1.15 thf('$adef_f_$a1', axiom,
% 3.62/1.15 (![V_24X1:$i]: ( ( happ @ cf @ V_24X1 ) = ( cf___24a1 @ V_24X1 ) ))).
% 3.62/1.15 thf(zip_derived_cl71, plain,
% 3.62/1.15 (![X0 : $i]: ((happ @ cf @ X0) = (cf___24a1 @ X0))),
% 3.62/1.15 inference('cnf', [status(esa)], [$adef_f_$a1])).
% 3.62/1.15 thf(zip_derived_cl71, plain,
% 3.62/1.15 (![X0 : $i]: ((happ @ cf @ X0) = (cf___24a1 @ X0))),
% 3.62/1.15 inference('cnf', [status(esa)], [$adef_f_$a1])).
% 3.62/1.15 thf(zip_derived_cl87, plain, ( (cA___24t @ sk__20)),
% 3.62/1.15 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.62/1.15 thf(zip_derived_cl138, plain,
% 3.62/1.15 ( (cS___24a2 @ (happ @ cf @ sk__19) @ (happ @ cf @ sk__20))),
% 3.62/1.15 inference('demod', [status(thm)],
% 3.62/1.15 [zip_derived_cl137, zip_derived_cl84, zip_derived_cl71,
% 3.62/1.15 zip_derived_cl71, zip_derived_cl87])).
% 3.62/1.15 thf('$adef_S_$a2', axiom,
% 3.62/1.15 (![V_24X1:$i,V_24X2:$i]:
% 3.62/1.15 ( ( p @ ( happ @ ( happ @ cS @ V_24X1 ) @ V_24X2 ) ) <=>
% 3.62/1.15 ( cS___24a2 @ V_24X1 @ V_24X2 ) ))).
% 3.62/1.15 thf(zip_derived_cl70, plain,
% 3.62/1.15 (![X0 : $i, X1 : $i]:
% 3.62/1.15 ( (p @ (happ @ (happ @ cS @ X0) @ X1)) | ~ (cS___24a2 @ X0 @ X1))),
% 3.62/1.15 inference('cnf', [status(esa)], [$adef_S_$a2])).
% 3.62/1.15 thf(zip_derived_cl141, plain,
% 3.62/1.15 ( (p @ (happ @ (happ @ cS @ (happ @ cf @ sk__19)) @ (happ @ cf @ sk__20)))),
% 3.62/1.15 inference('sup-', [status(thm)], [zip_derived_cl138, zip_derived_cl70])).
% 3.62/1.15 thf(Quotients.quotient_projection_collapses_R, axiom,
% 3.62/1.15 (![V0__A:$i]:
% 3.62/1.15 ( ( cType___24t @ V0__A ) =>
% 3.62/1.15 ( ![V1__R:$i]:
% 3.62/1.15 ( ( cCoq_2eRelations_2eRelation__Definitions_2erelation___24t @
% 3.62/1.15 V0__A @ V1__R ) =>
% 3.62/1.15 ( ( cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2 @
% 3.62/1.15 V0__A @ V1__R ) =>
% 3.62/1.15 ( ![V3__x1:$i]:
% 3.62/1.15 ( ( t @ V3__x1 @ V0__A ) =>
% 3.62/1.15 ( ![V4__x2:$i]:
% 3.62/1.15 ( ( t @ V4__x2 @ V0__A ) =>
% 3.62/1.15 ( ( p @ ( happ @ ( happ @ V1__R @ V3__x1 ) @ V4__x2 ) ) =>
% 3.62/1.15 ( ( cQuotients_2equotient__projection___24a3 @
% 3.62/1.15 V0__A @ V1__R @ V3__x1 ) =
% 3.62/1.15 ( cQuotients_2equotient__projection___24a3 @
% 3.62/1.15 V0__A @ V1__R @ V4__x2 ) ) ) ) ) ) ) ) ) ) ))).
% 3.62/1.15 thf(zip_derived_cl61, plain,
% 3.62/1.15 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 3.62/1.15 (~ (cCoq_2eRelations_2eRelation__Definitions_2erelation___24t @ X0 @
% 3.62/1.15 X1)
% 3.62/1.15 | ~ (t @ X2 @ X0)
% 3.62/1.15 | ((cQuotients_2equotient__projection___24a3 @ X0 @ X1 @ X3)
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ X0 @ X1 @ X2))
% 3.62/1.15 | ~ (p @ (happ @ (happ @ X1 @ X3) @ X2))
% 3.62/1.15 | ~ (t @ X3 @ X0)
% 3.62/1.15 | ~ (cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2 @
% 3.62/1.15 X0 @ X1)
% 3.62/1.15 | ~ (cType___24t @ X0))),
% 3.62/1.15 inference('cnf', [status(esa)],
% 3.62/1.15 [Quotients.quotient_projection_collapses_R])).
% 3.62/1.15 thf(zip_derived_cl253, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 (~ (cType___24t @ X0)
% 3.62/1.15 | ~ (cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2 @
% 3.62/1.15 X0 @ cS)
% 3.62/1.15 | ~ (t @ (happ @ cf @ sk__19) @ X0)
% 3.62/1.15 | ((cQuotients_2equotient__projection___24a3 @ X0 @ cS @
% 3.62/1.15 (happ @ cf @ sk__19))
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ X0 @ cS @
% 3.62/1.15 (happ @ cf @ sk__20)))
% 3.62/1.15 | ~ (t @ (happ @ cf @ sk__20) @ X0)
% 3.62/1.15 | ~ (cCoq_2eRelations_2eRelation__Definitions_2erelation___24t @
% 3.62/1.15 X0 @ cS))),
% 3.62/1.15 inference('sup-', [status(thm)], [zip_derived_cl141, zip_derived_cl61])).
% 3.62/1.15 thf(zip_derived_cl588, plain,
% 3.62/1.15 ((~ (cCoq_2eRelations_2eRelation__Definitions_2erelation___24t @ cB @ cS)
% 3.62/1.15 | ~ (t @ (happ @ cf @ sk__20) @ cB)
% 3.62/1.15 | ((cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (happ @ cf @ sk__19))
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (happ @ cf @ sk__20)))
% 3.62/1.15 | ~ (t @ (happ @ cf @ sk__19) @ cB)
% 3.62/1.15 | ~ (cType___24t @ cB))),
% 3.62/1.15 inference('sup-', [status(thm)], [zip_derived_cl66, zip_derived_cl253])).
% 3.62/1.15 thf('$_typeof_S', axiom,
% 3.62/1.15 (cCoq_2eRelations_2eRelation__Definitions_2erelation___24t @ cB @ cS)).
% 3.62/1.15 thf(zip_derived_cl31, plain,
% 3.62/1.15 ( (cCoq_2eRelations_2eRelation__Definitions_2erelation___24t @ cB @ cS)),
% 3.62/1.15 inference('cnf', [status(esa)], [$_typeof_S])).
% 3.62/1.15 thf(zip_derived_cl71, plain,
% 3.62/1.15 (![X0 : $i]: ((happ @ cf @ X0) = (cf___24a1 @ X0))),
% 3.62/1.15 inference('cnf', [status(esa)], [$adef_f_$a1])).
% 3.62/1.15 thf('$adef_Quotients.InducedFunction2.projf_$a1', axiom,
% 3.62/1.15 (![V_24X1:$i]:
% 3.62/1.15 ( ( happ @ cQuotients_2eInducedFunction2_2eprojf @ V_24X1 ) =
% 3.62/1.15 ( cQuotients_2eInducedFunction2_2eprojf___24a1 @ V_24X1 ) ))).
% 3.62/1.15 thf(zip_derived_cl68, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 ((happ @ cQuotients_2eInducedFunction2_2eprojf @ X0)
% 3.62/1.15 = (cQuotients_2eInducedFunction2_2eprojf___24a1 @ X0))),
% 3.62/1.15 inference('cnf', [status(esa)],
% 3.62/1.15 [$adef_Quotients.InducedFunction2.projf_$a1])).
% 3.62/1.15 thf('$_def_Quotients.InducedFunction2.projf', axiom,
% 3.62/1.15 (![V0__a:$i]:
% 3.62/1.15 ( ( cQuotients_2eInducedFunction2_2eprojf___24a1 @ V0__a ) =
% 3.62/1.15 ( cQuotients_2equotient__projection___24a3 @
% 3.62/1.15 cB @ cS @ ( cf___24a1 @ V0__a ) ) ))).
% 3.62/1.15 thf(zip_derived_cl0, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 ((cQuotients_2eInducedFunction2_2eprojf___24a1 @ X0)
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (cf___24a1 @ X0)))),
% 3.62/1.15 inference('cnf', [status(esa)], [$_def_Quotients.InducedFunction2.projf])).
% 3.62/1.15 thf(zip_derived_cl102, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 ((happ @ cQuotients_2eInducedFunction2_2eprojf @ X0)
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (cf___24a1 @ X0)))),
% 3.62/1.15 inference('sup+', [status(thm)], [zip_derived_cl68, zip_derived_cl0])).
% 3.62/1.15 thf(zip_derived_cl103, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 ((happ @ cQuotients_2eInducedFunction2_2eprojf @ X0)
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (happ @ cf @ X0)))),
% 3.62/1.15 inference('sup+', [status(thm)], [zip_derived_cl71, zip_derived_cl102])).
% 3.62/1.15 thf('$_typeof_B', axiom, (cType___24t @ cB)).
% 3.62/1.15 thf(zip_derived_cl28, plain, ( (cType___24t @ cB)),
% 3.62/1.15 inference('cnf', [status(esa)], [$_typeof_B])).
% 3.62/1.15 thf(zip_derived_cl589, plain,
% 3.62/1.15 ((~ (t @ (happ @ cf @ sk__20) @ cB)
% 3.62/1.15 | ((happ @ cQuotients_2eInducedFunction2_2eprojf @ sk__19)
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (happ @ cf @ sk__20)))
% 3.62/1.15 | ~ (t @ (happ @ cf @ sk__19) @ cB))),
% 3.62/1.15 inference('demod', [status(thm)],
% 3.62/1.15 [zip_derived_cl588, zip_derived_cl31, zip_derived_cl103,
% 3.62/1.15 zip_derived_cl28])).
% 3.62/1.15 thf(zip_derived_cl590, plain,
% 3.62/1.15 ((~ (c_24__type__163663___24t @ cf)
% 3.62/1.15 | ~ (t @ (happ @ cf @ sk__19) @ cB)
% 3.62/1.15 | ((happ @ cQuotients_2eInducedFunction2_2eprojf @ sk__19)
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (happ @ cf @ sk__20))))),
% 3.62/1.15 inference('sup-', [status(thm)], [zip_derived_cl130, zip_derived_cl589])).
% 3.62/1.15 thf('$_typeof_f', axiom, (c_24__type__163663___24t @ cf)).
% 3.62/1.15 thf(zip_derived_cl32, plain, ( (c_24__type__163663___24t @ cf)),
% 3.62/1.15 inference('cnf', [status(esa)], [$_typeof_f])).
% 3.62/1.15 thf(zip_derived_cl591, plain,
% 3.62/1.15 ((~ (t @ (happ @ cf @ sk__19) @ cB)
% 3.62/1.15 | ((happ @ cQuotients_2eInducedFunction2_2eprojf @ sk__19)
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (happ @ cf @ sk__20))))),
% 3.62/1.15 inference('demod', [status(thm)], [zip_derived_cl590, zip_derived_cl32])).
% 3.62/1.15 thf(zip_derived_cl592, plain,
% 3.62/1.15 ((~ (c_24__type__163663___24t @ cf)
% 3.62/1.15 | ((happ @ cQuotients_2eInducedFunction2_2eprojf @ sk__19)
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (happ @ cf @ sk__20))))),
% 3.62/1.15 inference('sup-', [status(thm)], [zip_derived_cl128, zip_derived_cl591])).
% 3.62/1.15 thf(zip_derived_cl32, plain, ( (c_24__type__163663___24t @ cf)),
% 3.62/1.15 inference('cnf', [status(esa)], [$_typeof_f])).
% 3.62/1.15 thf(zip_derived_cl593, plain,
% 3.62/1.15 (((happ @ cQuotients_2eInducedFunction2_2eprojf @ sk__19)
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (happ @ cf @ sk__20)))),
% 3.62/1.15 inference('demod', [status(thm)], [zip_derived_cl592, zip_derived_cl32])).
% 3.62/1.15 thf(zip_derived_cl103, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 ((happ @ cQuotients_2eInducedFunction2_2eprojf @ X0)
% 3.62/1.15 = (cQuotients_2equotient__projection___24a3 @ cB @ cS @
% 3.62/1.15 (happ @ cf @ X0)))),
% 3.62/1.15 inference('sup+', [status(thm)], [zip_derived_cl71, zip_derived_cl102])).
% 3.62/1.15 thf(zip_derived_cl619, plain,
% 3.62/1.15 (((happ @ cQuotients_2eInducedFunction2_2eprojf @ sk__20)
% 3.62/1.15 = (happ @ cQuotients_2eInducedFunction2_2eprojf @ sk__19))),
% 3.62/1.15 inference('sup+', [status(thm)], [zip_derived_cl593, zip_derived_cl103])).
% 3.62/1.15 thf(zip_derived_cl86, plain,
% 3.62/1.15 (((cQuotients_2eInducedFunction2_2eprojf___24a1 @ sk__19)
% 3.62/1.15 != (cQuotients_2eInducedFunction2_2eprojf___24a1 @ sk__20))),
% 3.62/1.15 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.62/1.15 thf(zip_derived_cl68, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 ((happ @ cQuotients_2eInducedFunction2_2eprojf @ X0)
% 3.62/1.15 = (cQuotients_2eInducedFunction2_2eprojf___24a1 @ X0))),
% 3.62/1.15 inference('cnf', [status(esa)],
% 3.62/1.15 [$adef_Quotients.InducedFunction2.projf_$a1])).
% 3.62/1.15 thf(zip_derived_cl68, plain,
% 3.62/1.15 (![X0 : $i]:
% 3.62/1.15 ((happ @ cQuotients_2eInducedFunction2_2eprojf @ X0)
% 3.62/1.15 = (cQuotients_2eInducedFunction2_2eprojf___24a1 @ X0))),
% 3.62/1.15 inference('cnf', [status(esa)],
% 3.62/1.15 [$adef_Quotients.InducedFunction2.projf_$a1])).
% 3.62/1.15 thf(zip_derived_cl97, plain,
% 3.62/1.15 (((happ @ cQuotients_2eInducedFunction2_2eprojf @ sk__19)
% 3.62/1.15 != (happ @ cQuotients_2eInducedFunction2_2eprojf @ sk__20))),
% 3.62/1.15 inference('demod', [status(thm)],
% 3.62/1.15 [zip_derived_cl86, zip_derived_cl68, zip_derived_cl68])).
% 3.62/1.15 thf(zip_derived_cl626, plain, ($false),
% 3.62/1.15 inference('simplify_reflect-', [status(thm)],
% 3.62/1.15 [zip_derived_cl619, zip_derived_cl97])).
% 3.62/1.15
% 3.62/1.15 % SZS output end Refutation
% 3.62/1.15
% 3.62/1.15
% 3.62/1.15 % Terminating...
% 4.07/1.28 % Runner terminated.
% 4.07/1.28 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------