%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SEU829^1 : TPTP v9.2.0. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.uO9LxVepww 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 : Thu Oct 2 04:56:42 PM UTC 2025
% Result : Theorem 0.55s 0.75s
% Output : Refutation 0.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SEU829^1 : TPTP v9.2.0. Released v3.7.0.
% 0.04/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.uO9LxVepww true
% 0.13/0.34 % Computer : n004.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 1 16:13:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % Running portfolio for 300 s
% 0.13/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Number of cores: 8
% 0.13/0.34 % Python version: Python 3.6.8
% 0.13/0.35 % Running in HO mode
% 0.53/0.66 % Total configuration time : 828
% 0.53/0.66 % Estimated wc time : 1656
% 0.53/0.66 % Estimated cpu time (8 cpus) : 207.0
% 0.54/0.71 % /export/starexec/sandbox/solver/bin/lams/40_c.s.sh running for 80s
% 0.54/0.72 % /export/starexec/sandbox/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.54/0.72 % /export/starexec/sandbox/solver/bin/lams/40_c_ic.sh running for 80s
% 0.54/0.73 % /export/starexec/sandbox/solver/bin/lams/15_e_short1.sh running for 30s
% 0.55/0.74 % /export/starexec/sandbox/solver/bin/lams/40_noforms.sh running for 90s
% 0.55/0.74 % /export/starexec/sandbox/solver/bin/lams/40_b.comb.sh running for 70s
% 0.55/0.74 % /export/starexec/sandbox/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.55/0.75 % Solved by lams/35_full_unif4.sh.
% 0.55/0.75 % done 11 iterations in 0.011s
% 0.55/0.75 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.55/0.75 % SZS output start Refutation
% 0.55/0.75 thf('#sk3_type', type, '#sk3': $i).
% 0.55/0.75 thf(powerset_type, type, powerset: ($i > $o) > ($i > $o) > $o).
% 0.55/0.75 thf(subseteq_type, type, subseteq: ($i > $o) > ($i > $o) > $o).
% 0.55/0.75 thf('#sk1_type', type, '#sk1': $i > $o).
% 0.55/0.75 thf(emptyset_type, type, emptyset: $i > $o).
% 0.55/0.75 thf('#sk2_type', type, '#sk2': $i).
% 0.55/0.75 thf(emptyset, axiom,(( emptyset ) = (^[X:$i]: ( $false )))).
% 0.55/0.75 thf('0', plain, (( emptyset ) = ( ^[X:$i]: ( $false ) )),
% 0.55/0.75 inference('simplify_rw_rule', [status(thm)], [emptyset])).
% 0.55/0.75 thf('1', plain, (( emptyset ) = ( ^[V_1:$i]: ( $false ) )),
% 0.55/0.75 define([status(thm)])).
% 0.55/0.75 thf(poserset, axiom,(( powerset ) =
% 0.55/0.75 (^[X:( $i > $o ),Y:( $i > $o )]: ( subseteq @ Y @ X )))).
% 0.55/0.75 thf(subseteq, axiom,(( subseteq ) =
% 0.55/0.75 (^[X:( $i > $o ),Y:( $i > $o )]: ( ![U:$i]: ( ( X @ U ) => ( Y @ U ) ) )))).
% 0.55/0.75 thf('2', plain,
% 0.55/0.75 (( subseteq ) =
% 0.55/0.75 ( ^[X:( $i > $o ),Y:( $i > $o )]:
% 0.55/0.75 ( ![U:$i]: ( ( X @ U ) => ( Y @ U ) ) ) )),
% 0.55/0.75 inference('simplify_rw_rule', [status(thm)], [subseteq])).
% 0.55/0.75 thf('3', plain,
% 0.55/0.75 (( subseteq ) =
% 0.55/0.75 ( ^[V_1:( $i > $o ),V_2:( $i > $o )]:
% 0.55/0.75 ( ![X4:$i]: ( ( V_1 @ X4 ) => ( V_2 @ X4 ) ) ) )),
% 0.55/0.75 define([status(thm)])).
% 0.55/0.75 thf('4', plain,
% 0.55/0.75 (( powerset ) = ( ^[X:( $i > $o ),Y:( $i > $o )]: ( subseteq @ Y @ X ) )),
% 0.55/0.75 inference('simplify_rw_rule', [status(thm)], [poserset, '3'])).
% 0.55/0.75 thf('5', plain,
% 0.55/0.75 (( powerset ) =
% 0.55/0.75 ( ^[V_1:( $i > $o ),V_2:( $i > $o )]: ( subseteq @ V_2 @ V_1 ) )),
% 0.55/0.75 define([status(thm)])).
% 0.55/0.75 thf(conj, conjecture,
% 0.55/0.75 (( powerset @ emptyset ) = ( ^[X:( $i > $o )]: ( ( X ) = ( emptyset ) ) ))).
% 0.55/0.75 thf(zf_stmt_0, conjecture,
% 0.55/0.75 (( ^[V_1:( $i > $o )]: ( ![X4:$i]: ( ~( V_1 @ X4 ) ) ) ) =
% 0.55/0.75 ( ^[V_2:( $i > $o )]: ( ( V_2 ) = ( ^[V_3:$i]: ( $false ) ) ) ))).
% 0.55/0.75 thf(zf_stmt_1, negated_conjecture,
% 0.55/0.75 (( ^[V_1:( $i > $o )]: ( ![X4:$i]: ( ~( V_1 @ X4 ) ) ) ) !=
% 0.55/0.75 ( ^[V_2:( $i > $o )]: ( ( V_2 ) = ( ^[V_3:$i]: ( $false ) ) ) )),
% 0.55/0.75 inference('cnf.neg', [status(esa)], [zf_stmt_0])).
% 0.55/0.75 thf(zip_derived_cl0, plain,
% 0.55/0.75 ((((^[Y0 : $i > $o]: (((!!) @ (^[Y1 : $i]: (((~) @ (Y0 @ Y1))))))))
% 0.55/0.75 != ((^[Y0 : $i > $o]: (((Y0) = ((^[Y1 : $i]: ($false))))))))),
% 0.55/0.75 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.55/0.75 thf(zip_derived_cl1, plain,
% 0.55/0.75 (((((!!) @ (^[Y0 : $i]: (((~) @ ('#sk1' @ Y0))))))
% 0.55/0.75 != ((((^[Y0 : $i]: ('#sk1' @ Y0))) = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('neg_ext', [status(thm)], [zip_derived_cl0])).
% 0.55/0.75 thf(zip_derived_cl2, plain,
% 0.55/0.75 (((((!!) @ (^[Y0 : $i]: (((~) @ ('#sk1' @ Y0))))))
% 0.55/0.75 != ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('ho_norm', [status(thm)], [zip_derived_cl1])).
% 0.55/0.75 thf(zip_derived_cl3, plain,
% 0.55/0.75 (![X-81 : $i]:
% 0.55/0.75 ( ((^[Y0 : $i]: (((~) @ ('#sk1' @ Y0)))) @ X-81)
% 0.55/0.75 | ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('forall_hoist', [status(thm)], [zip_derived_cl2])).
% 0.55/0.75 thf(zip_derived_cl7, plain,
% 0.55/0.75 (![X-81 : $i]:
% 0.55/0.75 ( (((~) @ ('#sk1' @ X-81))) | ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('ho_norm', [status(thm)], [zip_derived_cl3])).
% 0.55/0.75 thf(zip_derived_cl8, plain,
% 0.55/0.75 (![X0 : $i]:
% 0.55/0.75 ( (((~) @ ('#sk1' @ X0))) | ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('cannonize vars', [status(thm)], [zip_derived_cl7])).
% 0.55/0.75 thf(zip_derived_cl9, plain,
% 0.55/0.75 (![X0 : $i]: (~ ('#sk1' @ X0) | (('#sk1') = ((^[Y0 : $i]: ($false)))))),
% 0.55/0.75 inference('simplify nested equalities', [status(thm)], [zip_derived_cl8])).
% 0.55/0.75 thf(zip_derived_cl2, plain,
% 0.55/0.75 (((((!!) @ (^[Y0 : $i]: (((~) @ ('#sk1' @ Y0))))))
% 0.55/0.75 != ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('ho_norm', [status(thm)], [zip_derived_cl1])).
% 0.55/0.75 thf(zip_derived_cl4, plain,
% 0.55/0.75 ((((^[Y0 : $i]: (((~) @ ('#sk1' @ Y0)))) @ '#sk2')
% 0.55/0.75 != ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('quantifier_rw', [status(thm)], [zip_derived_cl2])).
% 0.55/0.75 thf(zip_derived_cl5, plain,
% 0.55/0.75 (((((~) @ ('#sk1' @ '#sk2'))) != ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('ho_norm', [status(thm)], [zip_derived_cl4])).
% 0.55/0.75 thf(zip_derived_cl6, plain,
% 0.55/0.75 ((('#sk1' @ '#sk2') = ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('simplify nested equalities', [status(thm)], [zip_derived_cl5])).
% 0.55/0.75 thf(zip_derived_cl6, plain,
% 0.55/0.75 ((('#sk1' @ '#sk2') = ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('simplify nested equalities', [status(thm)], [zip_derived_cl5])).
% 0.55/0.75 thf(zip_derived_cl12, plain,
% 0.55/0.75 (((('#sk1') = ((^[Y0 : $i]: ($false)))) | ~ ('#sk1' @ '#sk2'))),
% 0.55/0.75 inference('eq_hoist', [status(thm)], [zip_derived_cl6])).
% 0.55/0.75 thf(zip_derived_cl18, plain,
% 0.55/0.75 (![X1 : $i]:
% 0.55/0.75 ((('#sk1' @ X1) = ((^[Y0 : $i]: ($false)) @ X1)) | ~ ('#sk1' @ '#sk2'))),
% 0.55/0.75 inference('ho_complete_eq', [status(thm)], [zip_derived_cl12])).
% 0.55/0.75 thf(zip_derived_cl19, plain,
% 0.55/0.75 (![X1 : $i]: (~ ('#sk1' @ X1) | ~ ('#sk1' @ '#sk2'))),
% 0.55/0.75 inference('ho_norm', [status(thm)], [zip_derived_cl18])).
% 0.55/0.75 thf(zip_derived_cl22, plain, (~ ('#sk1' @ '#sk2')),
% 0.55/0.75 inference('condensation', [status(thm)], [zip_derived_cl19])).
% 0.55/0.75 thf(zip_derived_cl23, plain, (~ ((('#sk1') = ((^[Y0 : $i]: ($false)))))),
% 0.55/0.75 inference('demod', [status(thm)], [zip_derived_cl6, zip_derived_cl22])).
% 0.55/0.75 thf(zip_derived_cl24, plain, ((('#sk1') != ((^[Y0 : $i]: ($false))))),
% 0.55/0.75 inference('simplify nested equalities', [status(thm)], [zip_derived_cl23])).
% 0.55/0.75 thf(zip_derived_cl31, plain, (![X0 : $i]: ~ ('#sk1' @ X0)),
% 0.55/0.75 inference('simplify_reflect-', [status(thm)],
% 0.55/0.75 [zip_derived_cl9, zip_derived_cl24])).
% 0.55/0.75 thf(zip_derived_cl22, plain, (~ ('#sk1' @ '#sk2')),
% 0.55/0.75 inference('condensation', [status(thm)], [zip_derived_cl19])).
% 0.55/0.75 thf(zip_derived_cl6, plain,
% 0.55/0.75 ((('#sk1' @ '#sk2') = ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('simplify nested equalities', [status(thm)], [zip_derived_cl5])).
% 0.55/0.75 thf(zip_derived_cl10, plain,
% 0.55/0.75 (( ('#sk1' @ '#sk2') | ~ ((('#sk1') = ((^[Y0 : $i]: ($false))))))),
% 0.55/0.75 inference('eq_elim', [status(thm)], [zip_derived_cl6])).
% 0.55/0.75 thf(zip_derived_cl13, plain,
% 0.55/0.75 (( ('#sk1' @ '#sk2') | (('#sk1') != ((^[Y0 : $i]: ($false)))))),
% 0.55/0.75 inference('simplify nested equalities', [status(thm)], [zip_derived_cl10])).
% 0.55/0.75 thf(zip_derived_cl15, plain, (( ('#sk1' @ '#sk2') | ('#sk1' @ '#sk3'))),
% 0.55/0.75 inference('neg_ext', [status(thm)], [zip_derived_cl13])).
% 0.55/0.75 thf(zip_derived_cl26, plain, ( ('#sk1' @ '#sk3')),
% 0.55/0.75 inference('sup+', [status(thm)], [zip_derived_cl22, zip_derived_cl15])).
% 0.55/0.75 thf(zip_derived_cl32, plain, ($false),
% 0.55/0.75 inference('sup+', [status(thm)], [zip_derived_cl31, zip_derived_cl26])).
% 0.55/0.75
% 0.55/0.75 % SZS output end Refutation
% 0.55/0.75
% 0.55/0.75
% 0.55/0.75 % Terminating...
% 0.65/0.84 % Runner terminated.
% 0.65/0.85 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------