%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEV643+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.tpDw1GrTur true
% Computer : n015.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:16 PM UTC 2026
% Result : Theorem 230.91s 33.78s
% Output : Refutation 230.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV643+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.tpDw1GrTur true
% 0.16/0.34 % Computer : n015.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 07:04:16 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 % Running portfolio for 300 s
% 0.16/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Number of cores: 8
% 0.16/0.34 % Python version: Python 3.6.8
% 0.16/0.34 % Running in FO mode
% 0.46/0.61 % Total configuration time : 435
% 0.46/0.61 % Estimated wc time : 1092
% 0.46/0.61 % Estimated cpu time (7 cpus) : 156.0
% 0.55/0.69 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.70 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.71 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.73 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.74 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.74 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 230.91/33.78 % Solved by fo/fo3_bce.sh.
% 230.91/33.78 % BCE start: 424
% 230.91/33.78 % BCE eliminated: 101
% 230.91/33.78 % PE start: 323
% 230.91/33.78 logic: eq
% 230.91/33.78 % PE eliminated: -4
% 230.91/33.78 % done 9632 iterations in 33.051s
% 230.91/33.78 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 230.91/33.78 % SZS output start Refutation
% 230.91/33.78 thf(happ_type, type, happ: $i > $i > $i).
% 230.91/33.78 thf(c_24__type__193___24t_type, type, c_24__type__193___24t: $i > $i > $o).
% 230.91/33.78 thf(c_24__type__64607___24t_type, type, c_24__type__64607___24t: $i > $o).
% 230.91/33.78 thf(cCoq_2eInit_2eDatatypes_2elength___24a2_type, type, cCoq_2eInit_2eDatatypes_2elength___24a2:
% 230.91/33.78 $i > $i > $i).
% 230.91/33.78 thf(p_type, type, p: $i > $o).
% 230.91/33.78 thf(cType___24t_type, type, cType___24t: $i > $o).
% 230.91/33.78 thf(cp_type, type, cp: $i).
% 230.91/33.78 thf(cT___24t_type, type, cT___24t: $i > $o).
% 230.91/33.78 thf(cCoq_2eInit_2eDatatypes_2elist___24t_type, type, cCoq_2eInit_2eDatatypes_2elist___24t:
% 230.91/33.78 $i > $i > $o).
% 230.91/33.78 thf(cCoq_2eInit_2eDatatypes_2ebool___24t_type, type, cCoq_2eInit_2eDatatypes_2ebool___24t:
% 230.91/33.78 $i > $o).
% 230.91/33.78 thf(cl_type, type, cl: $i).
% 230.91/33.78 thf(cCoq_2eLists_2eList_2efilter___24a3_type, type, cCoq_2eLists_2eList_2efilter___24a3:
% 230.91/33.78 $i > $i > $i > $i).
% 230.91/33.78 thf(t_type, type, t: $i > $i > $o).
% 230.91/33.78 thf(sk__25_type, type, sk__25: $i > $i > $i).
% 230.91/33.78 thf(cT_type, type, cT: $i).
% 230.91/33.78 thf(cCoq_2eInit_2ePeano_2ele___24a2_type, type, cCoq_2eInit_2ePeano_2ele___24a2:
% 230.91/33.78 $i > $i > $i).
% 230.91/33.78 thf(clist__utils_2ecount___24a3_type, type, clist__utils_2ecount___24a3:
% 230.91/33.78 $i > $i > $i > $i).
% 230.91/33.78 thf('$_type_193', axiom,
% 230.91/33.78 (![Vv__CANONICAL__0:$i,Vvar__194:$i]:
% 230.91/33.78 ( ( c_24__type__193___24t @ Vv__CANONICAL__0 @ Vvar__194 ) <=>
% 230.91/33.78 ( ![Vv__CANONICAL__1:$i]:
% 230.91/33.78 ( ( t @ Vv__CANONICAL__1 @ Vv__CANONICAL__0 ) =>
% 230.91/33.78 ( cCoq_2eInit_2eDatatypes_2ebool___24t @
% 230.91/33.78 ( happ @ Vvar__194 @ Vv__CANONICAL__1 ) ) ) ) ))).
% 230.91/33.78 thf(zip_derived_cl108, plain,
% 230.91/33.78 (![X0 : $i, X1 : $i]:
% 230.91/33.78 ( (c_24__type__193___24t @ X0 @ X1) | (t @ (sk__25 @ X1 @ X0) @ X0))),
% 230.91/33.78 inference('cnf', [status(esa)], [$_type_193])).
% 230.91/33.78 thf('$tdef_T', axiom,
% 230.91/33.78 (![V_24Y:$i]: ( ( cT___24t @ V_24Y ) <=> ( t @ V_24Y @ cT ) ))).
% 230.91/33.78 thf(zip_derived_cl416, plain,
% 230.91/33.78 (![X0 : $i]: ( (cT___24t @ X0) | ~ (t @ X0 @ cT))),
% 230.91/33.78 inference('cnf', [status(esa)], [$tdef_T])).
% 230.91/33.78 thf('$_type_64607', axiom,
% 230.91/33.78 (![Vvar__64608:$i]:
% 230.91/33.78 ( ( c_24__type__64607___24t @ Vvar__64608 ) <=>
% 230.91/33.78 ( ![Vv__CANONICAL__0:$i]:
% 230.91/33.78 ( ( cT___24t @ Vv__CANONICAL__0 ) =>
% 230.91/33.78 ( cCoq_2eInit_2eDatatypes_2ebool___24t @
% 230.91/33.78 ( happ @ Vvar__64608 @ Vv__CANONICAL__0 ) ) ) ) ))).
% 230.91/33.78 thf(zip_derived_cl113, plain,
% 230.91/33.78 (![X0 : $i, X1 : $i]:
% 230.91/33.78 (~ (cT___24t @ X0)
% 230.91/33.78 | (cCoq_2eInit_2eDatatypes_2ebool___24t @ (happ @ X1 @ X0))
% 230.91/33.78 | ~ (c_24__type__64607___24t @ X1))),
% 230.91/33.78 inference('cnf', [status(esa)], [$_type_64607])).
% 230.91/33.78 thf(zip_derived_cl2701, plain,
% 230.91/33.78 (![X0 : $i, X1 : $i]:
% 230.91/33.78 (~ (t @ X0 @ cT)
% 230.91/33.78 | ~ (c_24__type__64607___24t @ X1)
% 230.91/33.78 | (cCoq_2eInit_2eDatatypes_2ebool___24t @ (happ @ X1 @ X0)))),
% 230.91/33.78 inference('dp-resolution', [status(thm)],
% 230.91/33.78 [zip_derived_cl416, zip_derived_cl113])).
% 230.91/33.78 thf(zip_derived_cl107, plain,
% 230.91/33.78 (![X0 : $i, X1 : $i]:
% 230.91/33.78 ( (c_24__type__193___24t @ X0 @ X1)
% 230.91/33.78 | ~ (cCoq_2eInit_2eDatatypes_2ebool___24t @
% 230.91/33.78 (happ @ X1 @ (sk__25 @ X1 @ X0))))),
% 230.91/33.78 inference('cnf', [status(esa)], [$_type_193])).
% 230.91/33.78 thf(zip_derived_cl2839, plain,
% 230.91/33.78 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 230.91/33.78 (((happ @ X1 @ X0) != (happ @ X2 @ (sk__25 @ X2 @ X3)))
% 230.91/33.78 | ~ (c_24__type__64607___24t @ X1)
% 230.91/33.78 | ~ (t @ X0 @ cT)
% 230.91/33.78 | (c_24__type__193___24t @ X3 @ X2))),
% 230.91/33.78 inference('dp-resolution', [status(thm)],
% 230.91/33.78 [zip_derived_cl2701, zip_derived_cl107])).
% 230.91/33.78 thf(zip_derived_cl3949, plain,
% 230.91/33.78 (![X0 : $i, X1 : $i]:
% 230.91/33.78 ( (c_24__type__193___24t @ X1 @ X0)
% 230.91/33.78 | ~ (t @ (sk__25 @ X0 @ X1) @ cT)
% 230.91/33.78 | ~ (c_24__type__64607___24t @ X0))),
% 230.91/33.78 inference('eq_res', [status(thm)], [zip_derived_cl2839])).
% 230.91/33.78 thf(zip_derived_cl7572, plain,
% 230.91/33.78 (![X0 : $i]:
% 230.91/33.78 ( (c_24__type__193___24t @ cT @ X0)
% 230.91/33.78 | ~ (c_24__type__64607___24t @ X0)
% 230.91/33.78 | (c_24__type__193___24t @ cT @ X0))),
% 230.91/33.78 inference('sup-', [status(thm)], [zip_derived_cl108, zip_derived_cl3949])).
% 230.91/33.78 thf(zip_derived_cl7573, plain,
% 230.91/33.78 (![X0 : $i]:
% 230.91/33.78 (~ (c_24__type__64607___24t @ X0) | (c_24__type__193___24t @ cT @ X0))),
% 230.91/33.78 inference('simplify', [status(thm)], [zip_derived_cl7572])).
% 230.91/33.78 thf('_HAMMER_GOAL', conjecture,
% 230.91/33.78 (p @
% 230.91/33.78 ( cCoq_2eInit_2ePeano_2ele___24a2 @
% 230.91/33.78 ( cCoq_2eInit_2eDatatypes_2elength___24a2 @
% 230.91/33.78 cT @ ( cCoq_2eLists_2eList_2efilter___24a3 @ cT @ cp @ cl ) ) @
% 230.91/33.78 ( cCoq_2eInit_2eDatatypes_2elength___24a2 @ cT @ cl ) ))).
% 230.91/33.78 thf(zf_stmt_0, negated_conjecture,
% 230.91/33.78 (~( p @
% 230.91/33.78 ( cCoq_2eInit_2ePeano_2ele___24a2 @
% 230.91/33.78 ( cCoq_2eInit_2eDatatypes_2elength___24a2 @
% 230.91/33.78 cT @ ( cCoq_2eLists_2eList_2efilter___24a3 @ cT @ cp @ cl ) ) @
% 230.91/33.78 ( cCoq_2eInit_2eDatatypes_2elength___24a2 @ cT @ cl ) ) )),
% 230.91/33.78 inference('cnf.neg', [status(esa)], [_HAMMER_GOAL])).
% 230.91/33.78 thf(zip_derived_cl423, plain,
% 230.91/33.78 (~ (p @
% 230.91/33.78 (cCoq_2eInit_2ePeano_2ele___24a2 @
% 230.91/33.78 (cCoq_2eInit_2eDatatypes_2elength___24a2 @ cT @
% 230.91/33.78 (cCoq_2eLists_2eList_2efilter___24a3 @ cT @ cp @ cl)) @
% 230.91/33.78 (cCoq_2eInit_2eDatatypes_2elength___24a2 @ cT @ cl)))),
% 230.91/33.78 inference('cnf', [status(esa)], [zf_stmt_0])).
% 230.91/33.78 thf(list_utils.length_filter, axiom,
% 230.91/33.78 (![V0__X:$i]:
% 230.91/33.78 ( ( cType___24t @ V0__X ) =>
% 230.91/33.78 ( ![V1__p:$i]:
% 230.91/33.78 ( ( c_24__type__193___24t @ V0__X @ V1__p ) =>
% 230.91/33.78 ( ![V2__l:$i]:
% 230.91/33.78 ( ( cCoq_2eInit_2eDatatypes_2elist___24t @ V0__X @ V2__l ) =>
% 230.91/33.78 ( ( cCoq_2eInit_2eDatatypes_2elength___24a2 @
% 230.91/33.78 V0__X @
% 230.91/33.78 ( cCoq_2eLists_2eList_2efilter___24a3 @
% 230.91/33.78 V0__X @ V1__p @ V2__l ) ) =
% 230.91/33.78 ( clist__utils_2ecount___24a3 @ V0__X @ V1__p @ V2__l ) ) ) ) ) ) ))).
% 230.91/33.78 thf(zip_derived_cl412, plain,
% 230.91/33.78 (![X0 : $i, X1 : $i, X2 : $i]:
% 230.91/33.78 (~ (c_24__type__193___24t @ X0 @ X1)
% 230.91/33.78 | ((cCoq_2eInit_2eDatatypes_2elength___24a2 @ X0 @
% 230.91/33.78 (cCoq_2eLists_2eList_2efilter___24a3 @ X0 @ X1 @ X2))
% 230.91/33.78 = (clist__utils_2ecount___24a3 @ X0 @ X1 @ X2))
% 230.91/33.78 | ~ (cCoq_2eInit_2eDatatypes_2elist___24t @ X0 @ X2)
% 230.91/33.78 | ~ (cType___24t @ X0))),
% 230.91/33.78 inference('cnf', [status(esa)], [list_utils.length_filter])).
% 230.91/33.78 thf(list_utils.count_le, axiom,
% 230.91/33.78 (![V0__X:$i]:
% 230.91/33.78 ( ( cType___24t @ V0__X ) =>
% 230.91/33.78 ( ![V1__p:$i]:
% 230.91/33.78 ( ( c_24__type__193___24t @ V0__X @ V1__p ) =>
% 230.91/33.78 ( ![V2__l:$i]:
% 230.91/33.78 ( ( cCoq_2eInit_2eDatatypes_2elist___24t @ V0__X @ V2__l ) =>
% 230.91/33.78 ( p @
% 230.91/33.78 ( cCoq_2eInit_2ePeano_2ele___24a2 @
% 230.91/33.78 ( clist__utils_2ecount___24a3 @ V0__X @ V1__p @ V2__l ) @
% 230.91/33.78 ( cCoq_2eInit_2eDatatypes_2elength___24a2 @ V0__X @ V2__l ) ) ) ) ) ) ) ))).
% 230.91/33.78 thf(zip_derived_cl410, plain,
% 230.91/33.78 (![X0 : $i, X1 : $i, X2 : $i]:
% 230.91/33.78 (~ (c_24__type__193___24t @ X0 @ X1)
% 230.91/33.78 | (p @
% 230.91/33.78 (cCoq_2eInit_2ePeano_2ele___24a2 @
% 230.91/33.78 (clist__utils_2ecount___24a3 @ X0 @ X1 @ X2) @
% 230.91/33.78 (cCoq_2eInit_2eDatatypes_2elength___24a2 @ X0 @ X2)))
% 230.91/33.78 | ~ (cCoq_2eInit_2eDatatypes_2elist___24t @ X0 @ X2)
% 230.91/33.78 | ~ (cType___24t @ X0))),
% 230.91/33.78 inference('cnf', [status(esa)], [list_utils.count_le])).
% 230.91/33.78 thf(zip_derived_cl5128, plain,
% 230.91/33.78 (![X0 : $i, X1 : $i, X2 : $i]:
% 230.91/33.78 ( (p @
% 230.91/33.78 (cCoq_2eInit_2ePeano_2ele___24a2 @
% 230.91/33.78 (cCoq_2eInit_2eDatatypes_2elength___24a2 @ X2 @
% 230.91/33.78 (cCoq_2eLists_2eList_2efilter___24a3 @ X2 @ X1 @ X0)) @
% 230.91/33.78 (cCoq_2eInit_2eDatatypes_2elength___24a2 @ X2 @ X0)))
% 230.91/33.78 | ~ (cType___24t @ X2)
% 230.91/33.78 | ~ (cCoq_2eInit_2eDatatypes_2elist___24t @ X2 @ X0)
% 230.91/33.78 | ~ (c_24__type__193___24t @ X2 @ X1)
% 230.91/33.78 | ~ (cType___24t @ X2)
% 230.91/33.78 | ~ (cCoq_2eInit_2eDatatypes_2elist___24t @ X2 @ X0)
% 230.91/33.78 | ~ (c_24__type__193___24t @ X2 @ X1))),
% 230.91/33.78 inference('sup+', [status(thm)], [zip_derived_cl412, zip_derived_cl410])).
% 230.91/33.78 thf(zip_derived_cl5131, plain,
% 230.91/33.78 (![X0 : $i, X1 : $i, X2 : $i]:
% 230.91/33.78 (~ (c_24__type__193___24t @ X2 @ X1)
% 230.91/33.78 | ~ (cCoq_2eInit_2eDatatypes_2elist___24t @ X2 @ X0)
% 230.91/33.78 | ~ (cType___24t @ X2)
% 230.91/33.78 | (p @
% 230.91/33.78 (cCoq_2eInit_2ePeano_2ele___24a2 @
% 230.91/33.78 (cCoq_2eInit_2eDatatypes_2elength___24a2 @ X2 @
% 230.91/33.78 (cCoq_2eLists_2eList_2efilter___24a3 @ X2 @ X1 @ X0)) @
% 230.91/33.78 (cCoq_2eInit_2eDatatypes_2elength___24a2 @ X2 @ X0))))),
% 230.91/33.78 inference('simplify', [status(thm)], [zip_derived_cl5128])).
% 230.91/33.78 thf(zip_derived_cl177445, plain,
% 230.91/33.78 ((~ (cType___24t @ cT)
% 230.91/33.78 | ~ (cCoq_2eInit_2eDatatypes_2elist___24t @ cT @ cl)
% 230.91/33.78 | ~ (c_24__type__193___24t @ cT @ cp))),
% 230.91/33.78 inference('sup+', [status(thm)], [zip_derived_cl423, zip_derived_cl5131])).
% 230.91/33.78 thf('$_typeof_T', axiom, (cType___24t @ cT)).
% 230.91/33.78 thf(zip_derived_cl119, plain, ( (cType___24t @ cT)),
% 230.91/33.78 inference('cnf', [status(esa)], [$_typeof_T])).
% 230.91/33.78 thf('$_typeof_l', axiom, (cCoq_2eInit_2eDatatypes_2elist___24t @ cT @ cl)).
% 230.91/33.78 thf(zip_derived_cl120, plain,
% 230.91/33.78 ( (cCoq_2eInit_2eDatatypes_2elist___24t @ cT @ cl)),
% 230.91/33.78 inference('cnf', [status(esa)], [$_typeof_l])).
% 230.91/33.78 thf(zip_derived_cl177458, plain, (~ (c_24__type__193___24t @ cT @ cp)),
% 230.91/33.78 inference('demod', [status(thm)],
% 230.91/33.78 [zip_derived_cl177445, zip_derived_cl119, zip_derived_cl120])).
% 230.91/33.78 thf(zip_derived_cl177496, plain, (~ (c_24__type__64607___24t @ cp)),
% 230.91/33.78 inference('sup-', [status(thm)],
% 230.91/33.78 [zip_derived_cl7573, zip_derived_cl177458])).
% 230.91/33.78 thf('$_typeof_p', axiom, (c_24__type__64607___24t @ cp)).
% 230.91/33.78 thf(zip_derived_cl121, plain, ( (c_24__type__64607___24t @ cp)),
% 230.91/33.78 inference('cnf', [status(esa)], [$_typeof_p])).
% 230.91/33.78 thf(zip_derived_cl177497, plain, ($false),
% 230.91/33.78 inference('demod', [status(thm)],
% 230.91/33.78 [zip_derived_cl177496, zip_derived_cl121])).
% 230.91/33.78
% 230.91/33.78 % SZS output end Refutation
% 230.91/33.78
% 230.91/33.78
% 230.91/33.78 % Terminating...
% 231.58/33.89 % Runner terminated.
% 34.44/33.90 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------