%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEV629+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.tSHOQPVlgo true
% Computer : n020.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:15 PM UTC 2026
% Result : Theorem 3.05s 1.08s
% Output : Refutation 3.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV629+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.tSHOQPVlgo true
% 0.17/0.35 % Computer : n020.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Tue May 5 06:23:19 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 % Running portfolio for 300 s
% 0.17/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.35 % Number of cores: 8
% 0.20/0.36 % Python version: Python 3.6.8
% 0.20/0.36 % Running in FO mode
% 0.57/0.67 % Total configuration time : 435
% 0.57/0.67 % Estimated wc time : 1092
% 0.57/0.67 % Estimated cpu time (7 cpus) : 156.0
% 0.57/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.57/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.57/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.57/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.58/1.01 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 3.05/1.08 % Solved by fo/fo7.sh.
% 3.05/1.08 % done 185 iterations in 0.287s
% 3.05/1.08 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 3.05/1.08 % SZS output start Refutation
% 3.05/1.08 thf(c_24__type__35378_type, type, c_24__type__35378: $i).
% 3.05/1.08 thf(sk__8_type, type, sk__8: $i > $i > $i > $i).
% 3.05/1.08 thf(cHahnSets_2eset__subset___24a1_type, type, cHahnSets_2eset__subset___24a1:
% 3.05/1.08 $i > $i).
% 3.05/1.08 thf(p_type, type, p: $i > $o).
% 3.05/1.08 thf(cHahnSets_2eset__subset_type, type, cHahnSets_2eset__subset: $i).
% 3.05/1.08 thf(happ_type, type, happ: $i > $i > $i).
% 3.05/1.08 thf(cHahnSets_2eset__subset___24a3_type, type, cHahnSets_2eset__subset___24a3:
% 3.05/1.08 $i > $i > $i > $o).
% 3.05/1.08 thf(cA_type, type, cA: $i).
% 3.05/1.08 thf(cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2_type, type,
% 3.05/1.08 cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2: $i > $i > $o).
% 3.05/1.08 thf(t_type, type, t: $i > $i > $o).
% 3.05/1.08 thf(sk__2_type, type, sk__2: $i > $i > $i).
% 3.05/1.08 thf('$_def_Coq.Relations.Relation_Definitions.reflexive', axiom,
% 3.05/1.08 (![V0__A:$i,V1__R:$i]:
% 3.05/1.08 ( ( cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2 @
% 3.05/1.08 V0__A @ V1__R ) <=>
% 3.05/1.08 ( ![V2__x:$i]:
% 3.05/1.08 ( ( t @ V2__x @ V0__A ) =>
% 3.05/1.08 ( p @ ( happ @ ( happ @ V1__R @ V2__x ) @ V2__x ) ) ) ) ))).
% 3.05/1.08 thf(zip_derived_cl8, plain,
% 3.05/1.08 (![X0 : $i, X1 : $i]:
% 3.05/1.08 ( (cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2 @ X0 @
% 3.05/1.08 X1)
% 3.05/1.08 | ~ (p @ (happ @ (happ @ X1 @ (sk__2 @ X1 @ X0)) @ (sk__2 @ X1 @ X0))))),
% 3.05/1.08 inference('cnf', [status(esa)],
% 3.05/1.08 [$_def_Coq.Relations.Relation_Definitions.reflexive])).
% 3.05/1.08 thf('_HAMMER_GOAL', conjecture,
% 3.05/1.08 (cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2 @
% 3.05/1.08 c_24__type__35378 @ ( cHahnSets_2eset__subset___24a1 @ cA ))).
% 3.05/1.08 thf(zf_stmt_0, negated_conjecture,
% 3.05/1.08 (~( cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2 @
% 3.05/1.08 c_24__type__35378 @ ( cHahnSets_2eset__subset___24a1 @ cA ) )),
% 3.05/1.08 inference('cnf.neg', [status(esa)], [_HAMMER_GOAL])).
% 3.05/1.08 thf(zip_derived_cl96, plain,
% 3.05/1.08 (~ (cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2 @
% 3.05/1.08 c_24__type__35378 @ (cHahnSets_2eset__subset___24a1 @ cA))),
% 3.05/1.08 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.05/1.08 thf('$adef_HahnSets.set_subset_$a1', axiom,
% 3.05/1.08 (![V_24X1:$i]:
% 3.05/1.08 ( ( happ @ cHahnSets_2eset__subset @ V_24X1 ) =
% 3.05/1.08 ( cHahnSets_2eset__subset___24a1 @ V_24X1 ) ))).
% 3.05/1.08 thf(zip_derived_cl86, plain,
% 3.05/1.08 (![X0 : $i]:
% 3.05/1.08 ((happ @ cHahnSets_2eset__subset @ X0)
% 3.05/1.08 = (cHahnSets_2eset__subset___24a1 @ X0))),
% 3.05/1.08 inference('cnf', [status(esa)], [$adef_HahnSets.set_subset_$a1])).
% 3.05/1.08 thf(zip_derived_cl99, plain,
% 3.05/1.08 (~ (cCoq_2eRelations_2eRelation__Definitions_2ereflexive___24a2 @
% 3.05/1.08 c_24__type__35378 @ (happ @ cHahnSets_2eset__subset @ cA))),
% 3.05/1.08 inference('demod', [status(thm)], [zip_derived_cl96, zip_derived_cl86])).
% 3.05/1.08 thf(zip_derived_cl218, plain,
% 3.05/1.08 (~ (p @
% 3.05/1.08 (happ @
% 3.05/1.08 (happ @ (happ @ cHahnSets_2eset__subset @ cA) @
% 3.05/1.08 (sk__2 @ (happ @ cHahnSets_2eset__subset @ cA) @ c_24__type__35378)) @
% 3.05/1.08 (sk__2 @ (happ @ cHahnSets_2eset__subset @ cA) @ c_24__type__35378)))),
% 3.05/1.08 inference('sup-', [status(thm)], [zip_derived_cl8, zip_derived_cl99])).
% 3.05/1.08 thf('$_def_HahnSets.set_subset', axiom,
% 3.05/1.08 (![V0__A:$i,V1__s:$i,V2__s_27:$i]:
% 3.05/1.08 ( ( cHahnSets_2eset__subset___24a3 @ V0__A @ V1__s @ V2__s_27 ) <=>
% 3.05/1.08 ( ![V3__x:$i]:
% 3.05/1.08 ( ( t @ V3__x @ V0__A ) =>
% 3.05/1.08 ( ( p @ ( happ @ V1__s @ V3__x ) ) =>
% 3.05/1.08 ( p @ ( happ @ V2__s_27 @ V3__x ) ) ) ) ) ))).
% 3.05/1.08 thf(zip_derived_cl26, plain,
% 3.05/1.08 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.05/1.08 ( (cHahnSets_2eset__subset___24a3 @ X0 @ X1 @ X2)
% 3.05/1.08 | (p @ (happ @ X1 @ (sk__8 @ X2 @ X1 @ X0))))),
% 3.05/1.08 inference('cnf', [status(esa)], [$_def_HahnSets.set_subset])).
% 3.05/1.08 thf(zip_derived_cl27, plain,
% 3.05/1.08 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.05/1.08 ( (cHahnSets_2eset__subset___24a3 @ X0 @ X1 @ X2)
% 3.05/1.08 | ~ (p @ (happ @ X2 @ (sk__8 @ X2 @ X1 @ X0))))),
% 3.05/1.08 inference('cnf', [status(esa)], [$_def_HahnSets.set_subset])).
% 3.05/1.08 thf(zip_derived_cl301, plain,
% 3.05/1.08 (![X0 : $i, X1 : $i]:
% 3.05/1.08 ( (cHahnSets_2eset__subset___24a3 @ X0 @ X1 @ X1)
% 3.05/1.08 | (cHahnSets_2eset__subset___24a3 @ X0 @ X1 @ X1))),
% 3.05/1.08 inference('sup-', [status(thm)], [zip_derived_cl26, zip_derived_cl27])).
% 3.05/1.08 thf(zip_derived_cl305, plain,
% 3.05/1.08 (![X0 : $i, X1 : $i]: (cHahnSets_2eset__subset___24a3 @ X0 @ X1 @ X1)),
% 3.05/1.08 inference('simplify', [status(thm)], [zip_derived_cl301])).
% 3.05/1.08 thf('$adef_HahnSets.set_subset_$a3', axiom,
% 3.05/1.08 (![V_24X1:$i,V_24X2:$i,V_24X3:$i]:
% 3.05/1.08 ( ( p @
% 3.05/1.08 ( happ @
% 3.05/1.08 ( happ @ ( happ @ cHahnSets_2eset__subset @ V_24X1 ) @ V_24X2 ) @
% 3.05/1.08 V_24X3 ) ) <=>
% 3.05/1.08 ( cHahnSets_2eset__subset___24a3 @ V_24X1 @ V_24X2 @ V_24X3 ) ))).
% 3.05/1.08 thf(zip_derived_cl91, plain,
% 3.05/1.08 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.05/1.08 ( (p @
% 3.05/1.08 (happ @ (happ @ (happ @ cHahnSets_2eset__subset @ X0) @ X1) @ X2))
% 3.05/1.08 | ~ (cHahnSets_2eset__subset___24a3 @ X0 @ X1 @ X2))),
% 3.05/1.08 inference('cnf', [status(esa)], [$adef_HahnSets.set_subset_$a3])).
% 3.05/1.08 thf(zip_derived_cl319, plain,
% 3.05/1.08 (![X0 : $i, X1 : $i]:
% 3.05/1.08 (p @
% 3.05/1.08 (happ @ (happ @ (happ @ cHahnSets_2eset__subset @ X1) @ X0) @ X0))),
% 3.05/1.08 inference('sup-', [status(thm)], [zip_derived_cl305, zip_derived_cl91])).
% 3.05/1.08 thf(zip_derived_cl336, plain, ($false),
% 3.05/1.08 inference('demod', [status(thm)], [zip_derived_cl218, zip_derived_cl319])).
% 3.05/1.08
% 3.05/1.08 % SZS output end Refutation
% 3.05/1.08
% 3.05/1.08
% 3.05/1.08 % Terminating...
% 3.63/1.17 % Runner terminated.
% 3.63/1.18 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------