%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SET047^1 : TPTP v9.2.0. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.n9hF8FdTtl true
% Computer : n009.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:51:19 PM UTC 2025
% Result : Theorem 0.52s 0.74s
% Output : Refutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET047^1 : TPTP v9.2.0. Released v8.1.0.
% 0.07/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.n9hF8FdTtl true
% 0.13/0.34 % Computer : n009.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 13:20:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % Running portfolio for 300 s
% 0.13/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.35 % Running in HO mode
% 0.45/0.62 % Total configuration time : 828
% 0.45/0.62 % Estimated wc time : 1656
% 0.45/0.62 % Estimated cpu time (8 cpus) : 207.0
% 0.51/0.65 % /export/starexec/sandbox2/solver/bin/lams/40_c.s.sh running for 80s
% 0.51/0.67 % /export/starexec/sandbox2/solver/bin/lams/35_full_unif4.sh running for 80s
% 0.52/0.68 % /export/starexec/sandbox2/solver/bin/lams/40_c_ic.sh running for 80s
% 0.52/0.69 % /export/starexec/sandbox2/solver/bin/lams/15_e_short1.sh running for 30s
% 0.52/0.70 % /export/starexec/sandbox2/solver/bin/lams/40_noforms.sh running for 90s
% 0.52/0.71 % /export/starexec/sandbox2/solver/bin/lams/40_b.comb.sh running for 70s
% 0.52/0.71 % /export/starexec/sandbox2/solver/bin/lams/20_acsne_simpl.sh running for 40s
% 0.52/0.72 % /export/starexec/sandbox2/solver/bin/lams/30_sp5.sh running for 60s
% 0.52/0.74 % Solved by lams/35_full_unif4.sh.
% 0.52/0.74 % done 53 iterations in 0.048s
% 0.52/0.74 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.52/0.74 % SZS output start Refutation
% 0.52/0.74 thf(mworld_type, type, mworld: $tType).
% 0.52/0.74 thf(mforall_di_type, type, mforall_di: ($i > mworld > $o) > mworld > $o).
% 0.52/0.74 thf('#sk2_type', type, '#sk2': $i).
% 0.52/0.74 thf(element_type, type, element: $i > $i > mworld > $o).
% 0.52/0.74 thf(mactual_type, type, mactual: mworld).
% 0.52/0.74 thf(mequiv_type, type, mequiv: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.52/0.74 thf(mlocal_type, type, mlocal: (mworld > $o) > $o).
% 0.52/0.74 thf(set_equal_type, type, set_equal: $i > $i > mworld > $o).
% 0.52/0.74 thf('#sk1_type', type, '#sk1': $i).
% 0.52/0.74 thf('#sk3_type', type, '#sk3': $i > $i > $i).
% 0.52/0.74 thf(mforall_di_def, axiom,(( mforall_di ) =
% 0.52/0.74 (^[A:( $i > mworld > $o ),W:mworld]: ( ![X:$i]: ( A @ X @ W ) )))).
% 0.52/0.74 thf('0', plain,
% 0.52/0.74 (( mforall_di ) =
% 0.52/0.74 ( ^[A:( $i > mworld > $o ),W:mworld]: ( ![X:$i]: ( A @ X @ W ) ) )),
% 0.52/0.74 inference('simplify_rw_rule', [status(thm)], [mforall_di_def])).
% 0.52/0.74 thf('1', plain,
% 0.52/0.74 (( mforall_di ) =
% 0.52/0.74 ( ^[V_1:( $i > mworld > $o ),V_2:mworld]:
% 0.52/0.74 ( ![X4:$i]: ( V_1 @ X4 @ V_2 ) ) )),
% 0.52/0.74 define([status(thm)])).
% 0.52/0.74 thf(mequiv_def, axiom,(( mequiv ) =
% 0.52/0.74 (^[A:( mworld > $o ),B:( mworld > $o ),W:mworld]:
% 0.52/0.74 ( ( A @ W ) <=> ( B @ W ) )))).
% 0.52/0.74 thf('2', plain,
% 0.52/0.74 (( mequiv ) =
% 0.52/0.74 ( ^[A:( mworld > $o ),B:( mworld > $o ),W:mworld]:
% 0.52/0.74 ( ( A @ W ) <=> ( B @ W ) ) )),
% 0.52/0.74 inference('simplify_rw_rule', [status(thm)], [mequiv_def])).
% 0.52/0.74 thf('3', plain,
% 0.52/0.74 (( mequiv ) =
% 0.52/0.74 ( ^[V_1:( mworld > $o ),V_2:( mworld > $o ),V_3:mworld]:
% 0.52/0.74 ( ( V_1 @ V_3 ) <=> ( V_2 @ V_3 ) ) )),
% 0.52/0.74 define([status(thm)])).
% 0.52/0.74 thf(mlocal_def, axiom,(( mlocal ) =
% 0.52/0.74 (^[Phi:( mworld > $o )]: ( Phi @ mactual )))).
% 0.52/0.74 thf('4', plain, (( mlocal ) = ( ^[Phi:( mworld > $o )]: ( Phi @ mactual ) )),
% 0.52/0.74 inference('simplify_rw_rule', [status(thm)], [mlocal_def])).
% 0.52/0.74 thf('5', plain, (( mlocal ) = ( ^[V_1:( mworld > $o )]: ( V_1 @ mactual ) )),
% 0.52/0.74 define([status(thm)])).
% 0.52/0.74 thf(pel43, conjecture,
% 0.52/0.74 (mlocal @
% 0.52/0.74 ( mforall_di @
% 0.52/0.74 ( ^[X:$i]:
% 0.52/0.74 ( mforall_di @
% 0.52/0.74 ( ^[Y:$i]:
% 0.52/0.74 ( mequiv @ ( set_equal @ X @ Y ) @ ( set_equal @ Y @ X ) ) ) ) ) ))).
% 0.52/0.74 thf(zf_stmt_0, conjecture,
% 0.52/0.74 (![X4:$i,X6:$i]:
% 0.52/0.74 ( ( set_equal @ X4 @ X6 @ mactual ) <=> ( set_equal @ X6 @ X4 @ mactual ) ))).
% 0.52/0.74 thf(zf_stmt_1, negated_conjecture,
% 0.52/0.74 (~( ![X4:$i,X6:$i]:
% 0.52/0.74 ( ( set_equal @ X4 @ X6 @ mactual ) <=>
% 0.52/0.74 ( set_equal @ X6 @ X4 @ mactual ) ) )),
% 0.52/0.74 inference('cnf.neg', [status(esa)], [zf_stmt_0])).
% 0.52/0.74 thf(zip_derived_cl1, plain,
% 0.52/0.74 (~ (((!!) @ (^[Y0 : $i]:
% 0.52/0.74 (((!!) @ (^[Y1 : $i]:
% 0.52/0.74 (((set_equal @ Y0 @ Y1 @ mactual) <=>
% 0.52/0.74 (set_equal @ Y1 @ Y0 @ mactual)))))))))),
% 0.52/0.74 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.52/0.74 thf(zip_derived_cl2, plain,
% 0.52/0.74 (~ (((!!) @ (^[Y0 : $i]:
% 0.52/0.74 (((set_equal @ '#sk1' @ Y0 @ mactual) <=> (set_equal @
% 0.52/0.74 Y0 @ '#sk1' @ mactual))))))),
% 0.52/0.74 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl1])).
% 0.52/0.74 thf(zip_derived_cl3, plain,
% 0.52/0.74 (~ (((set_equal @ '#sk1' @ '#sk2' @ mactual) <=> (set_equal @ '#sk2' @
% 0.52/0.74 '#sk1' @ mactual)))),
% 0.52/0.74 inference('lazy_cnf_exists', [status(thm)], [zip_derived_cl2])).
% 0.52/0.74 thf(zip_derived_cl4, plain,
% 0.52/0.74 (((set_equal @ '#sk1' @ '#sk2' @ mactual)
% 0.52/0.74 != (set_equal @ '#sk2' @ '#sk1' @ mactual))),
% 0.52/0.74 inference('simplify nested equalities', [status(thm)], [zip_derived_cl3])).
% 0.52/0.74 thf(zip_derived_cl5, plain,
% 0.52/0.74 (( (set_equal @ '#sk1' @ '#sk2' @ mactual)
% 0.52/0.74 | (set_equal @ '#sk2' @ '#sk1' @ mactual))),
% 0.52/0.74 inference('eq_elim', [status(thm)], [zip_derived_cl4])).
% 0.52/0.74 thf(pel43_1, axiom,
% 0.52/0.74 (mlocal @
% 0.52/0.74 ( mforall_di @
% 0.52/0.74 ( ^[X:$i]:
% 0.52/0.74 ( mforall_di @
% 0.52/0.74 ( ^[Y:$i]:
% 0.52/0.74 ( mequiv @
% 0.52/0.74 ( set_equal @ X @ Y ) @
% 0.52/0.74 ( mforall_di @
% 0.52/0.74 ( ^[Z:$i]:
% 0.52/0.74 ( mequiv @ ( element @ Z @ X ) @ ( element @ Z @ Y ) ) ) ) ) ) ) ) ))).
% 0.52/0.74 thf(zf_stmt_2, axiom,
% 0.52/0.74 (![X4:$i,X6:$i]:
% 0.52/0.74 ( ( set_equal @ X4 @ X6 @ mactual ) <=>
% 0.52/0.74 ( ![X8:$i]:
% 0.52/0.74 ( ( element @ X8 @ X4 @ mactual ) <=> ( element @ X8 @ X6 @ mactual ) ) ) ))).
% 0.52/0.74 thf(zip_derived_cl0, plain,
% 0.52/0.74 ( (((!!) @ (^[Y0 : $i]:
% 0.52/0.74 (((!!) @ (^[Y1 : $i]:
% 0.52/0.74 (((set_equal @ Y0 @ Y1 @ mactual) <=>
% 0.52/0.74 (((!!) @ (^[Y2 : $i]:
% 0.52/0.74 (((element @ Y2 @ Y0 @
% 0.52/0.74 mactual) <=> (element @ Y2 @
% 0.52/0.74 Y1 @ mactual))))))))))))))),
% 0.52/0.74 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.52/0.74 thf(zip_derived_cl12, plain,
% 0.52/0.74 (![X2 : $i]:
% 0.52/0.74 (((!!) @ (^[Y0 : $i]:
% 0.52/0.74 (((set_equal @ X2 @ Y0 @ mactual) <=>
% 0.52/0.74 (((!!) @ (^[Y1 : $i]:
% 0.52/0.74 (((element @ Y1 @ X2 @ mactual) <=>
% 0.52/0.74 (element @ Y1 @ Y0 @ mactual)))))))))))),
% 0.52/0.74 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl0])).
% 0.52/0.74 thf(zip_derived_cl13, plain,
% 0.52/0.74 (![X2 : $i, X4 : $i]:
% 0.52/0.74 (((set_equal @ X2 @ X4 @ mactual) <=>
% 0.52/0.74 (((!!) @ (^[Y0 : $i]:
% 0.52/0.74 (((element @ Y0 @ X2 @ mactual) <=> (element @ Y0 @
% 0.52/0.74 X4 @ mactual))))))))),
% 0.52/0.74 inference('lazy_cnf_forall', [status(thm)], [zip_derived_cl12])).
% 0.52/0.74 thf(zip_derived_cl14, plain,
% 0.52/0.74 (![X2 : $i, X4 : $i]:
% 0.52/0.74 ((set_equal @ X2 @ X4 @ mactual)
% 0.52/0.74 = (((!!) @ (^[Y0 : $i]:
% 0.52/0.74 (((element @ Y0 @ X2 @ mactual) <=> (element @ Y0 @
% 0.52/0.74 X4 @ mactual)))))))),
% 0.52/0.74 inference('simplify nested equalities', [status(thm)], [zip_derived_cl13])).
% 0.52/0.74 thf(zip_derived_cl15, plain,
% 0.52/0.74 (![X-81 : $i, X2 : $i, X4 : $i]:
% 0.52/0.74 ( ((^[Y0 : $i]:
% 0.52/0.74 (((element @ Y0 @ X2 @ mactual) <=> (element @ Y0 @ X4 @
% 0.52/0.74 mactual)))) @
% 0.52/0.74 X-81)
% 0.52/0.74 | ~ (set_equal @ X2 @ X4 @ mactual))),
% 0.52/0.74 inference('forall_hoist', [status(thm)], [zip_derived_cl14])).
% 0.52/0.74 thf(zip_derived_cl18, plain,
% 0.52/0.74 (![X-81 : $i, X2 : $i, X4 : $i]:
% 0.52/0.74 ( (((element @ X-81 @ X2 @ mactual) <=> (element @ X-81 @ X4 @
% 0.52/0.74 mactual)))
% 0.52/0.74 | ~ (set_equal @ X2 @ X4 @ mactual))),
% 0.52/0.74 inference('ho_norm', [status(thm)], [zip_derived_cl15])).
% 0.52/0.74 thf(zip_derived_cl19, plain,
% 0.52/0.74 (![X2 : $i, X4 : $i, X5 : $i]:
% 0.52/0.74 ( (((element @ X5 @ X2 @ mactual) <=> (element @ X5 @ X4 @ mactual)))
% 0.52/0.74 | ~ (set_equal @ X2 @ X4 @ mactual))),
% 0.52/0.74 inference('cannonize vars', [status(thm)], [zip_derived_cl18])).
% 0.52/0.74 thf(zip_derived_cl20, plain,
% 0.52/0.74 (![X2 : $i, X4 : $i, X5 : $i]:
% 0.52/0.74 (((element @ X5 @ X2 @ mactual) = (element @ X5 @ X4 @ mactual))
% 0.52/0.74 | ~ (set_equal @ X2 @ X4 @ mactual))),
% 0.52/0.74 inference('simplify nested equalities', [status(thm)], [zip_derived_cl19])).
% 0.52/0.74 thf(zip_derived_cl38, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ( (set_equal @ '#sk1' @ '#sk2' @ mactual)
% 0.52/0.74 | ((element @ X0 @ '#sk2' @ mactual)
% 0.52/0.74 = (element @ X0 @ '#sk1' @ mactual)))),
% 0.52/0.74 inference('sup-', [status(thm)], [zip_derived_cl5, zip_derived_cl20])).
% 0.52/0.74 thf(zip_derived_cl20, plain,
% 0.52/0.74 (![X2 : $i, X4 : $i, X5 : $i]:
% 0.52/0.74 (((element @ X5 @ X2 @ mactual) = (element @ X5 @ X4 @ mactual))
% 0.52/0.74 | ~ (set_equal @ X2 @ X4 @ mactual))),
% 0.52/0.74 inference('simplify nested equalities', [status(thm)], [zip_derived_cl19])).
% 0.52/0.74 thf(zip_derived_cl44, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ((element @ X0 @ '#sk2' @ mactual) = (element @ X0 @ '#sk1' @ mactual))),
% 0.52/0.74 inference('clc', [status(thm)], [zip_derived_cl38, zip_derived_cl20])).
% 0.52/0.74 thf(zip_derived_cl44, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ((element @ X0 @ '#sk2' @ mactual) = (element @ X0 @ '#sk1' @ mactual))),
% 0.52/0.74 inference('clc', [status(thm)], [zip_derived_cl38, zip_derived_cl20])).
% 0.52/0.74 thf(zip_derived_cl44, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ((element @ X0 @ '#sk2' @ mactual) = (element @ X0 @ '#sk1' @ mactual))),
% 0.52/0.74 inference('clc', [status(thm)], [zip_derived_cl38, zip_derived_cl20])).
% 0.52/0.74 thf(zip_derived_cl14, plain,
% 0.52/0.74 (![X2 : $i, X4 : $i]:
% 0.52/0.74 ((set_equal @ X2 @ X4 @ mactual)
% 0.52/0.74 = (((!!) @ (^[Y0 : $i]:
% 0.52/0.74 (((element @ Y0 @ X2 @ mactual) <=> (element @ Y0 @
% 0.52/0.74 X4 @ mactual)))))))),
% 0.52/0.74 inference('simplify nested equalities', [status(thm)], [zip_derived_cl13])).
% 0.52/0.74 thf(zip_derived_cl16, plain,
% 0.52/0.74 (![X2 : $i, X4 : $i]:
% 0.52/0.74 ((set_equal @ X2 @ X4 @ mactual)
% 0.52/0.74 = ((^[Y0 : $i]:
% 0.52/0.74 (((element @ Y0 @ X2 @ mactual) <=> (element @ Y0 @ X4 @
% 0.52/0.74 mactual)))) @
% 0.52/0.74 ('#sk3' @ X2 @ X4)))),
% 0.52/0.74 inference('quantifier_rw', [status(thm)], [zip_derived_cl14])).
% 0.52/0.74 thf(zip_derived_cl17, plain,
% 0.52/0.74 (![X2 : $i, X4 : $i]:
% 0.52/0.74 ((set_equal @ X2 @ X4 @ mactual)
% 0.52/0.74 = (((element @ ('#sk3' @ X2 @ X4) @ X2 @ mactual) <=> (element @
% 0.52/0.74 ('#sk3' @ X2 @ X4) @ X4 @ mactual))))),
% 0.52/0.74 inference('ho_norm', [status(thm)], [zip_derived_cl16])).
% 0.52/0.74 thf(zip_derived_cl46, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ((set_equal @ X0 @ '#sk1' @ mactual)
% 0.52/0.74 = (((element @ ('#sk3' @ X0 @ '#sk1') @ X0 @ mactual) <=>
% 0.52/0.74 (element @ ('#sk3' @ X0 @ '#sk1') @ '#sk2' @ mactual))))),
% 0.52/0.74 inference('sup+', [status(thm)], [zip_derived_cl44, zip_derived_cl17])).
% 0.52/0.74 thf(zip_derived_cl61, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ( (set_equal @ X0 @ '#sk1' @ mactual)
% 0.52/0.74 | ~ (((element @ ('#sk3' @ X0 @ '#sk1') @ X0 @ mactual) <=>
% 0.52/0.74 (element @ ('#sk3' @ X0 @ '#sk1') @ '#sk2' @ mactual))))),
% 0.52/0.74 inference('eq_elim', [status(thm)], [zip_derived_cl46])).
% 0.52/0.74 thf(zip_derived_cl66, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ( (set_equal @ X0 @ '#sk1' @ mactual)
% 0.52/0.74 | ((element @ ('#sk3' @ X0 @ '#sk1') @ X0 @ mactual)
% 0.52/0.74 != (element @ ('#sk3' @ X0 @ '#sk1') @ '#sk2' @ mactual)))),
% 0.52/0.74 inference('simplify nested equalities', [status(thm)], [zip_derived_cl61])).
% 0.52/0.74 thf(zip_derived_cl304, plain,
% 0.52/0.74 ((((element @ ('#sk3' @ '#sk2' @ '#sk1') @ '#sk1' @ mactual)
% 0.52/0.74 != (element @ ('#sk3' @ '#sk2' @ '#sk1') @ '#sk2' @ mactual))
% 0.52/0.74 | (set_equal @ '#sk2' @ '#sk1' @ mactual))),
% 0.52/0.74 inference('sup-', [status(thm)], [zip_derived_cl44, zip_derived_cl66])).
% 0.52/0.74 thf(zip_derived_cl4, plain,
% 0.52/0.74 (((set_equal @ '#sk1' @ '#sk2' @ mactual)
% 0.52/0.74 != (set_equal @ '#sk2' @ '#sk1' @ mactual))),
% 0.52/0.74 inference('simplify nested equalities', [status(thm)], [zip_derived_cl3])).
% 0.52/0.74 thf(zip_derived_cl44, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ((element @ X0 @ '#sk2' @ mactual) = (element @ X0 @ '#sk1' @ mactual))),
% 0.52/0.74 inference('clc', [status(thm)], [zip_derived_cl38, zip_derived_cl20])).
% 0.52/0.74 thf(zip_derived_cl44, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ((element @ X0 @ '#sk2' @ mactual) = (element @ X0 @ '#sk1' @ mactual))),
% 0.52/0.74 inference('clc', [status(thm)], [zip_derived_cl38, zip_derived_cl20])).
% 0.52/0.74 thf(zip_derived_cl17, plain,
% 0.52/0.74 (![X2 : $i, X4 : $i]:
% 0.52/0.74 ((set_equal @ X2 @ X4 @ mactual)
% 0.52/0.74 = (((element @ ('#sk3' @ X2 @ X4) @ X2 @ mactual) <=> (element @
% 0.52/0.74 ('#sk3' @ X2 @ X4) @ X4 @ mactual))))),
% 0.52/0.74 inference('ho_norm', [status(thm)], [zip_derived_cl16])).
% 0.52/0.74 thf(zip_derived_cl45, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ((set_equal @ X0 @ '#sk2' @ mactual)
% 0.52/0.74 = (((element @ ('#sk3' @ X0 @ '#sk2') @ X0 @ mactual) <=>
% 0.52/0.74 (element @ ('#sk3' @ X0 @ '#sk2') @ '#sk1' @ mactual))))),
% 0.52/0.74 inference('sup+', [status(thm)], [zip_derived_cl44, zip_derived_cl17])).
% 0.52/0.74 thf(zip_derived_cl52, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ( (set_equal @ X0 @ '#sk2' @ mactual)
% 0.52/0.74 | ~ (((element @ ('#sk3' @ X0 @ '#sk2') @ X0 @ mactual) <=>
% 0.52/0.74 (element @ ('#sk3' @ X0 @ '#sk2') @ '#sk1' @ mactual))))),
% 0.52/0.74 inference('eq_elim', [status(thm)], [zip_derived_cl45])).
% 0.52/0.74 thf(zip_derived_cl57, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ( (set_equal @ X0 @ '#sk2' @ mactual)
% 0.52/0.74 | ((element @ ('#sk3' @ X0 @ '#sk2') @ X0 @ mactual)
% 0.52/0.74 != (element @ ('#sk3' @ X0 @ '#sk2') @ '#sk1' @ mactual)))),
% 0.52/0.74 inference('simplify nested equalities', [status(thm)], [zip_derived_cl52])).
% 0.52/0.74 thf(zip_derived_cl93, plain,
% 0.52/0.74 ((((element @ ('#sk3' @ '#sk1' @ '#sk2') @ '#sk2' @ mactual)
% 0.52/0.74 != (element @ ('#sk3' @ '#sk1' @ '#sk2') @ '#sk1' @ mactual))
% 0.52/0.74 | (set_equal @ '#sk1' @ '#sk2' @ mactual))),
% 0.52/0.74 inference('sup-', [status(thm)], [zip_derived_cl44, zip_derived_cl57])).
% 0.52/0.74 thf(zip_derived_cl44, plain,
% 0.52/0.74 (![X0 : $i]:
% 0.52/0.74 ((element @ X0 @ '#sk2' @ mactual) = (element @ X0 @ '#sk1' @ mactual))),
% 0.52/0.74 inference('clc', [status(thm)], [zip_derived_cl38, zip_derived_cl20])).
% 0.52/0.74 thf(zip_derived_cl116, plain, ( (set_equal @ '#sk1' @ '#sk2' @ mactual)),
% 0.52/0.74 inference('clc', [status(thm)], [zip_derived_cl93, zip_derived_cl44])).
% 0.52/0.74 thf(zip_derived_cl117, plain, (~ (set_equal @ '#sk2' @ '#sk1' @ mactual)),
% 0.52/0.74 inference('demod', [status(thm)], [zip_derived_cl4, zip_derived_cl116])).
% 0.52/0.74 thf(zip_derived_cl315, plain,
% 0.52/0.74 (((element @ ('#sk3' @ '#sk2' @ '#sk1') @ '#sk1' @ mactual)
% 0.52/0.74 != (element @ ('#sk3' @ '#sk2' @ '#sk1') @ '#sk2' @ mactual))),
% 0.52/0.74 inference('demod', [status(thm)], [zip_derived_cl304, zip_derived_cl117])).
% 0.52/0.74 thf(zip_derived_cl424, plain,
% 0.52/0.74 (((element @ ('#sk3' @ '#sk2' @ '#sk1') @ '#sk2' @ mactual)
% 0.52/0.74 != (element @ ('#sk3' @ '#sk2' @ '#sk1') @ '#sk2' @ mactual))),
% 0.52/0.74 inference('sup-', [status(thm)], [zip_derived_cl44, zip_derived_cl315])).
% 0.52/0.74 thf(zip_derived_cl431, plain, ($false),
% 0.52/0.74 inference('simplify', [status(thm)], [zip_derived_cl424])).
% 0.52/0.74
% 0.52/0.74 % SZS output end Refutation
% 0.52/0.74
% 0.52/0.74
% 0.52/0.74 % Terminating...
% 0.54/0.81 % Runner terminated.
% 1.85/0.82 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------