%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEV641+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.0JEAzHn8bu true
% Computer : n012.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 28.76s 4.54s
% Output : Refutation 28.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : SEV641+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.07 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.0JEAzHn8bu true
% 0.07/0.25 % Computer : n012.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % WCLimit : 300
% 0.07/0.25 % DateTime : Tue May 5 06:59:30 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.07/0.25 % Running portfolio for 300 s
% 0.07/0.25 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.25 % Number of cores: 8
% 0.07/0.25 % Python version: Python 3.6.8
% 0.07/0.25 % Running in FO mode
% 0.14/0.41 % Total configuration time : 435
% 0.14/0.41 % Estimated wc time : 1092
% 0.14/0.41 % Estimated cpu time (7 cpus) : 156.0
% 0.52/0.47 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.52/0.47 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.52/0.47 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.52/0.47 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.52/0.47 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.52/0.47 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.52/0.49 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 28.76/4.54 % Solved by fo/fo7.sh.
% 28.76/4.54 % done 1767 iterations in 4.055s
% 28.76/4.54 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 28.76/4.54 % SZS output start Refutation
% 28.76/4.54 thf(happ_type, type, happ: $i > $i > $i).
% 28.76/4.54 thf(cCoq_2eLists_2eList_2eIn___24a3_type, type, cCoq_2eLists_2eList_2eIn___24a3:
% 28.76/4.54 $i > $i > $i > $i).
% 28.76/4.54 thf(cCoq_2eInit_2eDatatypes_2etrue_type, type, cCoq_2eInit_2eDatatypes_2etrue:
% 28.76/4.54 $i).
% 28.76/4.54 thf(cCoq_2eInit_2eDatatypes_2elist___24t_type, type, cCoq_2eInit_2eDatatypes_2elist___24t:
% 28.76/4.54 $i > $i > $o).
% 28.76/4.54 thf(p_type, type, p: $i > $o).
% 28.76/4.54 thf(c_24__type__193___24t_type, type, c_24__type__193___24t: $i > $i > $o).
% 28.76/4.54 thf(cType___24t_type, type, cType___24t: $i > $o).
% 28.76/4.54 thf(cp_type, type, cp: $i).
% 28.76/4.54 thf(sk__6_type, type, sk__6: $i > $i > $i > $i).
% 28.76/4.54 thf(cCoq_2eLists_2eList_2eincl___24a3_type, type, cCoq_2eLists_2eList_2eincl___24a3:
% 28.76/4.54 $i > $i > $i > $i).
% 28.76/4.54 thf(cX___24t_type, type, cX___24t: $i > $o).
% 28.76/4.54 thf(sk__32_type, type, sk__32: $i > $i > $i).
% 28.76/4.54 thf(cCoq_2eInit_2eDatatypes_2ebool___24t_type, type, cCoq_2eInit_2eDatatypes_2ebool___24t:
% 28.76/4.54 $i > $o).
% 28.76/4.54 thf(cCoq_2eLists_2eList_2efilter___24a3_type, type, cCoq_2eLists_2eList_2efilter___24a3:
% 28.76/4.54 $i > $i > $i > $i).
% 28.76/4.54 thf(cl_type, type, cl: $i).
% 28.76/4.54 thf(t_type, type, t: $i > $i > $o).
% 28.76/4.54 thf(c_24__type__1___24t_type, type, c_24__type__1___24t: $i > $o).
% 28.76/4.54 thf(cX_type, type, cX: $i).
% 28.76/4.54 thf('$_def_Coq.Lists.List.incl', axiom,
% 28.76/4.54 (![V0__A:$i,V1__l:$i,V2__m:$i]:
% 28.76/4.54 ( ( p @ ( cCoq_2eLists_2eList_2eincl___24a3 @ V0__A @ V1__l @ V2__m ) ) <=>
% 28.76/4.54 ( ![V3__a:$i]:
% 28.76/4.54 ( ( t @ V3__a @ V0__A ) =>
% 28.76/4.54 ( ( p @ ( cCoq_2eLists_2eList_2eIn___24a3 @ V0__A @ V3__a @ V1__l ) ) =>
% 28.76/4.54 ( p @ ( cCoq_2eLists_2eList_2eIn___24a3 @ V0__A @ V3__a @ V2__m ) ) ) ) ) ))).
% 28.76/4.54 thf(zip_derived_cl33, plain,
% 28.76/4.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 28.76/4.54 ( (p @ (cCoq_2eLists_2eList_2eincl___24a3 @ X0 @ X1 @ X2))
% 28.76/4.54 | ~ (p @
% 28.76/4.54 (cCoq_2eLists_2eList_2eIn___24a3 @ X0 @
% 28.76/4.54 (sk__6 @ X2 @ X1 @ X0) @ X2)))),
% 28.76/4.54 inference('cnf', [status(esa)], [$_def_Coq.Lists.List.incl])).
% 28.76/4.54 thf('_HAMMER_GOAL', conjecture,
% 28.76/4.54 (p @
% 28.76/4.54 ( cCoq_2eLists_2eList_2eincl___24a3 @
% 28.76/4.54 cX @ ( cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl ) @ cl ))).
% 28.76/4.54 thf(zf_stmt_0, negated_conjecture,
% 28.76/4.54 (~( p @
% 28.76/4.54 ( cCoq_2eLists_2eList_2eincl___24a3 @
% 28.76/4.54 cX @ ( cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl ) @ cl ) )),
% 28.76/4.54 inference('cnf.neg', [status(esa)], [_HAMMER_GOAL])).
% 28.76/4.54 thf(zip_derived_cl445, plain,
% 28.76/4.54 (~ (p @
% 28.76/4.54 (cCoq_2eLists_2eList_2eincl___24a3 @ cX @
% 28.76/4.54 (cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl) @ cl))),
% 28.76/4.54 inference('cnf', [status(esa)], [zf_stmt_0])).
% 28.76/4.54 thf(zip_derived_cl3531, plain,
% 28.76/4.54 (~ (p @
% 28.76/4.54 (cCoq_2eLists_2eList_2eIn___24a3 @ cX @
% 28.76/4.54 (sk__6 @ cl @
% 28.76/4.54 (cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl) @ cX) @
% 28.76/4.54 cl))),
% 28.76/4.54 inference('sup-', [status(thm)], [zip_derived_cl33, zip_derived_cl445])).
% 28.76/4.54 thf(zip_derived_cl32, plain,
% 28.76/4.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 28.76/4.54 ( (p @ (cCoq_2eLists_2eList_2eincl___24a3 @ X0 @ X1 @ X2))
% 28.76/4.54 | (p @
% 28.76/4.54 (cCoq_2eLists_2eList_2eIn___24a3 @ X0 @ (sk__6 @ X2 @ X1 @ X0) @
% 28.76/4.54 X1)))),
% 28.76/4.54 inference('cnf', [status(esa)], [$_def_Coq.Lists.List.incl])).
% 28.76/4.54 thf(zip_derived_cl445, plain,
% 28.76/4.54 (~ (p @
% 28.76/4.54 (cCoq_2eLists_2eList_2eincl___24a3 @ cX @
% 28.76/4.54 (cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl) @ cl))),
% 28.76/4.54 inference('cnf', [status(esa)], [zf_stmt_0])).
% 28.76/4.54 thf(zip_derived_cl1259, plain,
% 28.76/4.54 ( (p @
% 28.76/4.54 (cCoq_2eLists_2eList_2eIn___24a3 @ cX @
% 28.76/4.54 (sk__6 @ cl @ (cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl) @
% 28.76/4.54 cX) @
% 28.76/4.54 (cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl)))),
% 28.76/4.54 inference('sup-', [status(thm)], [zip_derived_cl32, zip_derived_cl445])).
% 28.76/4.54 thf(Coq.Lists.List.filter_In, axiom,
% 28.76/4.54 (![V0__A:$i]:
% 28.76/4.54 ( ( cType___24t @ V0__A ) =>
% 28.76/4.54 ( ![V1__f:$i]:
% 28.76/4.54 ( ( c_24__type__193___24t @ V0__A @ V1__f ) =>
% 28.76/4.54 ( ![V2__x:$i]:
% 28.76/4.54 ( ( t @ V2__x @ V0__A ) =>
% 28.76/4.54 ( ![V3__l:$i]:
% 28.76/4.54 ( ( cCoq_2eInit_2eDatatypes_2elist___24t @ V0__A @ V3__l ) =>
% 28.76/4.54 ( ( p @
% 28.76/4.54 ( cCoq_2eLists_2eList_2eIn___24a3 @
% 28.76/4.54 V0__A @ V2__x @
% 28.76/4.54 ( cCoq_2eLists_2eList_2efilter___24a3 @
% 28.76/4.54 V0__A @ V1__f @ V3__l ) ) ) <=>
% 28.76/4.54 ( ( p @
% 28.76/4.54 ( cCoq_2eLists_2eList_2eIn___24a3 @
% 28.76/4.54 V0__A @ V2__x @ V3__l ) ) &
% 28.76/4.54 ( ( happ @ V1__f @ V2__x ) =
% 28.76/4.54 ( cCoq_2eInit_2eDatatypes_2etrue ) ) ) ) ) ) ) ) ) ) ))).
% 28.76/4.54 thf(zip_derived_cl244, plain,
% 28.76/4.54 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 28.76/4.54 (~ (c_24__type__193___24t @ X0 @ X1)
% 28.76/4.54 | ~ (cCoq_2eInit_2eDatatypes_2elist___24t @ X0 @ X2)
% 28.76/4.54 | ~ (p @
% 28.76/4.54 (cCoq_2eLists_2eList_2eIn___24a3 @ X0 @ X3 @
% 28.76/4.54 (cCoq_2eLists_2eList_2efilter___24a3 @ X0 @ X1 @ X2)))
% 28.76/4.54 | (p @ (cCoq_2eLists_2eList_2eIn___24a3 @ X0 @ X3 @ X2))
% 28.76/4.54 | ~ (t @ X3 @ X0)
% 28.76/4.54 | ~ (cType___24t @ X0))),
% 28.76/4.54 inference('cnf', [status(esa)], [Coq.Lists.List.filter_In])).
% 28.76/4.54 thf(zip_derived_cl17031, plain,
% 28.76/4.54 ((~ (cType___24t @ cX)
% 28.76/4.54 | ~ (t @
% 28.76/4.54 (sk__6 @ cl @
% 28.76/4.54 (cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl) @ cX) @
% 28.76/4.54 cX)
% 28.76/4.54 | (p @
% 28.76/4.54 (cCoq_2eLists_2eList_2eIn___24a3 @ cX @
% 28.76/4.54 (sk__6 @ cl @
% 28.76/4.54 (cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl) @ cX) @
% 28.76/4.54 cl))
% 28.76/4.54 | ~ (cCoq_2eInit_2eDatatypes_2elist___24t @ cX @ cl)
% 28.76/4.54 | ~ (c_24__type__193___24t @ cX @ cp))),
% 28.76/4.54 inference('sup-', [status(thm)], [zip_derived_cl1259, zip_derived_cl244])).
% 28.76/4.54 thf('$_typeof_X', axiom, (cType___24t @ cX)).
% 28.76/4.54 thf(zip_derived_cl134, plain, ( (cType___24t @ cX)),
% 28.76/4.54 inference('cnf', [status(esa)], [$_typeof_X])).
% 28.76/4.54 thf(zip_derived_cl34, plain,
% 28.76/4.54 (![X0 : $i, X1 : $i, X2 : $i]:
% 28.76/4.54 ( (p @ (cCoq_2eLists_2eList_2eincl___24a3 @ X0 @ X1 @ X2))
% 28.76/4.54 | (t @ (sk__6 @ X2 @ X1 @ X0) @ X0))),
% 28.76/4.54 inference('cnf', [status(esa)], [$_def_Coq.Lists.List.incl])).
% 28.76/4.54 thf(zip_derived_cl445, plain,
% 28.76/4.54 (~ (p @
% 28.76/4.54 (cCoq_2eLists_2eList_2eincl___24a3 @ cX @
% 28.76/4.54 (cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl) @ cl))),
% 28.76/4.54 inference('cnf', [status(esa)], [zf_stmt_0])).
% 28.76/4.54 thf(zip_derived_cl927, plain,
% 28.76/4.54 ( (t @
% 28.76/4.54 (sk__6 @ cl @ (cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl) @
% 28.76/4.54 cX) @
% 28.76/4.54 cX)),
% 28.76/4.54 inference('sup-', [status(thm)], [zip_derived_cl34, zip_derived_cl445])).
% 28.76/4.54 thf('$_typeof_l', axiom, (cCoq_2eInit_2eDatatypes_2elist___24t @ cX @ cl)).
% 28.76/4.54 thf(zip_derived_cl135, plain,
% 28.76/4.54 ( (cCoq_2eInit_2eDatatypes_2elist___24t @ cX @ cl)),
% 28.76/4.54 inference('cnf', [status(esa)], [$_typeof_l])).
% 28.76/4.54 thf('$_type_193', axiom,
% 28.76/4.54 (![Vv__CANONICAL__0:$i,Vvar__194:$i]:
% 28.76/4.54 ( ( c_24__type__193___24t @ Vv__CANONICAL__0 @ Vvar__194 ) <=>
% 28.76/4.54 ( ![Vv__CANONICAL__1:$i]:
% 28.76/4.54 ( ( t @ Vv__CANONICAL__1 @ Vv__CANONICAL__0 ) =>
% 28.76/4.54 ( cCoq_2eInit_2eDatatypes_2ebool___24t @
% 28.76/4.54 ( happ @ Vvar__194 @ Vv__CANONICAL__1 ) ) ) ) ))).
% 28.76/4.54 thf(zip_derived_cl124, plain,
% 28.76/4.54 (![X0 : $i, X1 : $i]:
% 28.76/4.54 ( (c_24__type__193___24t @ X0 @ X1) | (t @ (sk__32 @ X1 @ X0) @ X0))),
% 28.76/4.54 inference('cnf', [status(esa)], [$_type_193])).
% 28.76/4.54 thf('$tdef_X', axiom,
% 28.76/4.54 (![V_24Y:$i]: ( ( cX___24t @ V_24Y ) <=> ( t @ V_24Y @ cX ) ))).
% 28.76/4.54 thf(zip_derived_cl444, plain,
% 28.76/4.54 (![X0 : $i]: ( (cX___24t @ X0) | ~ (t @ X0 @ cX))),
% 28.76/4.54 inference('cnf', [status(esa)], [$tdef_X])).
% 28.76/4.54 thf(zip_derived_cl523, plain,
% 28.76/4.54 (![X0 : $i]:
% 28.76/4.54 ( (c_24__type__193___24t @ cX @ X0) | (cX___24t @ (sk__32 @ X0 @ cX)))),
% 28.76/4.54 inference('sup-', [status(thm)], [zip_derived_cl124, zip_derived_cl444])).
% 28.76/4.54 thf('$_type_1', axiom,
% 28.76/4.54 (![Vvar__2:$i]:
% 28.76/4.54 ( ( c_24__type__1___24t @ Vvar__2 ) <=>
% 28.76/4.54 ( ![Vv__CANONICAL__0:$i]:
% 28.76/4.54 ( ( cX___24t @ Vv__CANONICAL__0 ) =>
% 28.76/4.54 ( cCoq_2eInit_2eDatatypes_2ebool___24t @
% 28.76/4.54 ( happ @ Vvar__2 @ Vv__CANONICAL__0 ) ) ) ) ))).
% 28.76/4.54 thf(zip_derived_cl119, plain,
% 28.76/4.54 (![X0 : $i, X1 : $i]:
% 28.76/4.54 (~ (cX___24t @ X0)
% 28.76/4.54 | (cCoq_2eInit_2eDatatypes_2ebool___24t @ (happ @ X1 @ X0))
% 28.76/4.54 | ~ (c_24__type__1___24t @ X1))),
% 28.76/4.54 inference('cnf', [status(esa)], [$_type_1])).
% 28.76/4.54 thf('$_typeof_p', axiom, (c_24__type__1___24t @ cp)).
% 28.76/4.54 thf(zip_derived_cl136, plain, ( (c_24__type__1___24t @ cp)),
% 28.76/4.54 inference('cnf', [status(esa)], [$_typeof_p])).
% 28.76/4.54 thf(zip_derived_cl533, plain,
% 28.76/4.54 (![X0 : $i]:
% 28.76/4.54 ( (cCoq_2eInit_2eDatatypes_2ebool___24t @ (happ @ cp @ X0))
% 28.76/4.54 | ~ (cX___24t @ X0))),
% 28.76/4.54 inference('sup+', [status(thm)], [zip_derived_cl119, zip_derived_cl136])).
% 28.76/4.54 thf(zip_derived_cl725, plain,
% 28.76/4.54 (![X0 : $i]:
% 28.76/4.54 ( (c_24__type__193___24t @ cX @ X0)
% 28.76/4.54 | (cCoq_2eInit_2eDatatypes_2ebool___24t @
% 28.76/4.54 (happ @ cp @ (sk__32 @ X0 @ cX))))),
% 28.76/4.54 inference('sup-', [status(thm)], [zip_derived_cl523, zip_derived_cl533])).
% 28.76/4.54 thf(zip_derived_cl123, plain,
% 28.76/4.54 (![X0 : $i, X1 : $i]:
% 28.76/4.54 ( (c_24__type__193___24t @ X0 @ X1)
% 28.76/4.54 | ~ (cCoq_2eInit_2eDatatypes_2ebool___24t @
% 28.76/4.54 (happ @ X1 @ (sk__32 @ X1 @ X0))))),
% 28.76/4.54 inference('cnf', [status(esa)], [$_type_193])).
% 28.76/4.54 thf(zip_derived_cl804, plain,
% 28.76/4.54 (( (c_24__type__193___24t @ cX @ cp) | (c_24__type__193___24t @ cX @ cp))),
% 28.76/4.54 inference('sup-', [status(thm)], [zip_derived_cl725, zip_derived_cl123])).
% 28.76/4.54 thf(zip_derived_cl818, plain, ( (c_24__type__193___24t @ cX @ cp)),
% 28.76/4.54 inference('simplify', [status(thm)], [zip_derived_cl804])).
% 28.76/4.54 thf(zip_derived_cl17048, plain,
% 28.76/4.54 ( (p @
% 28.76/4.54 (cCoq_2eLists_2eList_2eIn___24a3 @ cX @
% 28.76/4.54 (sk__6 @ cl @ (cCoq_2eLists_2eList_2efilter___24a3 @ cX @ cp @ cl) @
% 28.76/4.54 cX) @
% 28.76/4.54 cl))),
% 28.76/4.54 inference('demod', [status(thm)],
% 28.76/4.54 [zip_derived_cl17031, zip_derived_cl134, zip_derived_cl927,
% 28.76/4.54 zip_derived_cl135, zip_derived_cl818])).
% 28.76/4.54 thf(zip_derived_cl17050, plain, ($false),
% 28.76/4.54 inference('demod', [status(thm)],
% 28.76/4.54 [zip_derived_cl3531, zip_derived_cl17048])).
% 28.76/4.54
% 28.76/4.54 % SZS output end Refutation
% 28.76/4.54
% 28.76/4.54
% 28.76/4.54 % Terminating...
% 29.42/4.64 % Runner terminated.
% 29.42/4.65 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------