%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : PHI044_1 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.90WvoSEeLu true
% Computer : n027.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:49:08 PM UTC 2025
% Result : Unsatisfiable 4.68s 1.26s
% Output : Refutation 4.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PHI044_1 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.90WvoSEeLu true
% 0.13/0.34 % Computer : n027.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:57:23 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.13/0.35 % 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 FO mode
% 0.54/0.63 % Total configuration time : 435
% 0.54/0.63 % Estimated wc time : 1092
% 0.54/0.63 % Estimated cpu time (7 cpus) : 156.0
% 0.55/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 4.68/1.26 % Solved by fo/fo13.sh.
% 4.68/1.26 % done 653 iterations in 0.493s
% 4.68/1.26 % SZS status Unsatisfiable for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 4.68/1.26 % SZS output start Refutation
% 4.68/1.26 thf(option_type, type, option: $tType).
% 4.68/1.26 thf(option_set_type, type, option_set: $tType).
% 4.68/1.26 thf(weakly_better_type, type, weakly_better: option_set > option_set > $o).
% 4.68/1.26 thf(sk__2_type, type, sk__2: option_set > option > option).
% 4.68/1.26 thf(zip_tseitin_3_type, type, zip_tseitin_3: option > option_set > option > $o).
% 4.68/1.26 thf(sk__1_type, type, sk__1: option_set > option > option > option).
% 4.68/1.26 thf(zip_tseitin_2_type, type, zip_tseitin_2: option > option_set > option >
% 4.68/1.26 option > $o).
% 4.68/1.26 thf(zip_tseitin_1_type, type, zip_tseitin_1: option > option > option > $o).
% 4.68/1.26 thf(sk__8_type, type, sk__8: option).
% 4.68/1.26 thf(subset_type, type, subset: option_set > option_set > $o).
% 4.68/1.26 thf(permitted_preference_type, type, permitted_preference: option > option > $o).
% 4.68/1.26 thf(sk__12_type, type, sk__12: option_set).
% 4.68/1.26 thf(required_preference_type, type, required_preference: option > option > $o).
% 4.68/1.26 thf(sk__type, type, sk_: option_set > option_set > option).
% 4.68/1.26 thf(sk__9_type, type, sk__9: option_set).
% 4.68/1.26 thf(sk__4_type, type, sk__4: option_set > option > option).
% 4.68/1.26 thf(sk__11_type, type, sk__11: option_set).
% 4.68/1.26 thf(sk__5_type, type, sk__5: option_set > option > option).
% 4.68/1.26 thf(better_type, type, better: option_set > option_set > $o).
% 4.68/1.26 thf(sk__6_type, type, sk__6: option).
% 4.68/1.26 thf(zip_tseitin_0_type, type, zip_tseitin_0: option > option_set > option > $o).
% 4.68/1.26 thf(member_type, type, member: option > option_set > $o).
% 4.68/1.26 thf(sk__7_type, type, sk__7: option).
% 4.68/1.26 thf(sk__3_type, type, sk__3: option > option_set > option_set > option).
% 4.68/1.26 thf(sk__10_type, type, sk__10: option_set).
% 4.68/1.26 thf(existence_of_dominated_diversity, axiom,
% 4.68/1.26 (?[X:option,Y:option,Z:option,A:option_set,B:option_set,C:option_set,
% 4.68/1.26 D:option_set]:
% 4.68/1.26 ( ( ![U:option]:
% 4.68/1.26 ( ( member @ U @ D ) <=>
% 4.68/1.26 ( ( ( U ) = ( X ) ) | ( ( U ) = ( Y ) ) | ( ( U ) = ( Z ) ) ) ) ) &
% 4.68/1.26 ( ![U:option]:
% 4.68/1.26 ( ( member @ U @ C ) <=> ( ( ( U ) = ( X ) ) | ( ( U ) = ( Y ) ) ) ) ) &
% 4.68/1.26 ( ![U:option]: ( ( member @ U @ B ) <=> ( ( U ) = ( Z ) ) ) ) &
% 4.68/1.26 ( ![U:option]: ( ( member @ U @ A ) <=> ( ( U ) = ( X ) ) ) ) &
% 4.68/1.26 ( member @ Z @ D ) & ( member @ Y @ D ) & ( member @ X @ D ) &
% 4.68/1.26 ( member @ Y @ C ) & ( member @ X @ C ) & ( member @ Z @ B ) &
% 4.68/1.26 ( member @ X @ A ) & ( required_preference @ Z @ Y ) &
% 4.68/1.26 ( required_preference @ Z @ X ) & ( permitted_preference @ Y @ X ) &
% 4.68/1.26 ( permitted_preference @ X @ Y ) ))).
% 4.68/1.26 thf(zip_derived_cl35, plain, ( (member @ sk__7 @ sk__11)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl34, plain, ( (member @ sk__6 @ sk__11)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl32, plain, ( (member @ sk__6 @ sk__9)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl32, plain, ( (member @ sk__6 @ sk__9)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl32, plain, ( (member @ sk__6 @ sk__9)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl35, plain, ( (member @ sk__7 @ sk__11)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl29, plain, ( (permitted_preference @ sk__7 @ sk__6)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(value_of_rational_diversity, axiom,
% 4.68/1.26 (![X:option,Y:option,U:option_set,V:option_set]:
% 4.68/1.26 ( ( ( ![Z:option]: ( ( member @ Z @ V ) => ( ( Z ) = ( X ) ) ) ) &
% 4.68/1.26 ( ![Z:option]:
% 4.68/1.26 ( ( member @ Z @ U ) => ( ( ( Z ) = ( Y ) ) | ( ( Z ) = ( X ) ) ) ) ) &
% 4.68/1.26 ( member @ X @ V ) & ( member @ Y @ U ) & ( member @ X @ U ) &
% 4.68/1.26 ( permitted_preference @ Y @ X ) & ( permitted_preference @ X @ Y ) ) =>
% 4.68/1.26 ( better @ U @ V ) ))).
% 4.68/1.26 thf(zf_stmt_0, axiom,
% 4.68/1.26 (![Z:option,U:option_set,Y:option,X:option]:
% 4.68/1.26 ( ( ( member @ Z @ U ) => ( zip_tseitin_1 @ Z @ Y @ X ) ) =>
% 4.68/1.26 ( zip_tseitin_2 @ Z @ U @ Y @ X ) ))).
% 4.68/1.26 thf(zip_derived_cl11, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option, X3 : option]:
% 4.68/1.26 ( (zip_tseitin_2 @ X0 @ X1 @ X2 @ X3) | (member @ X0 @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_0])).
% 4.68/1.26 thf(zf_stmt_1, axiom,
% 4.68/1.26 (![Z:option,V:option_set,X:option]:
% 4.68/1.26 ( ( ( member @ Z @ V ) => ( ( Z ) = ( X ) ) ) =>
% 4.68/1.26 ( zip_tseitin_0 @ Z @ V @ X ) ))).
% 4.68/1.26 thf(zip_derived_cl7, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option]:
% 4.68/1.26 ( (zip_tseitin_0 @ X0 @ X1 @ X2) | (member @ X0 @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.68/1.26 thf(zf_stmt_2, type, zip_tseitin_2 :
% 4.68/1.26 option > option_set > option > option > $o).
% 4.68/1.26 thf(zf_stmt_3, type, zip_tseitin_1 : option > option > option > $o).
% 4.68/1.26 thf(zf_stmt_4, axiom,
% 4.68/1.26 (![Z:option,Y:option,X:option]:
% 4.68/1.26 ( ( ( ( Z ) = ( X ) ) | ( ( Z ) = ( Y ) ) ) =>
% 4.68/1.26 ( zip_tseitin_1 @ Z @ Y @ X ) ))).
% 4.68/1.26 thf(zf_stmt_5, type, zip_tseitin_0 : option > option_set > option > $o).
% 4.68/1.26 thf(zf_stmt_6, axiom,
% 4.68/1.26 (![X:option,Y:option,U:option_set,V:option_set]:
% 4.68/1.26 ( ( ( permitted_preference @ X @ Y ) & ( permitted_preference @ Y @ X ) &
% 4.68/1.26 ( member @ X @ U ) & ( member @ Y @ U ) & ( member @ X @ V ) &
% 4.68/1.26 ( ![Z:option]: ( zip_tseitin_2 @ Z @ U @ Y @ X ) ) &
% 4.68/1.26 ( ![Z:option]: ( zip_tseitin_0 @ Z @ V @ X ) ) ) =>
% 4.68/1.26 ( better @ U @ V ) ))).
% 4.68/1.26 thf(zip_derived_cl12, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option, X2 : option, X3 : option_set]:
% 4.68/1.26 (~ (zip_tseitin_2 @ (sk__1 @ X0 @ X1 @ X2) @ X0 @ X1 @ X2)
% 4.68/1.26 | ~ (member @ X1 @ X0)
% 4.68/1.26 | ~ (member @ X2 @ X0)
% 4.68/1.26 | ~ (permitted_preference @ X1 @ X2)
% 4.68/1.26 | ~ (permitted_preference @ X2 @ X1)
% 4.68/1.26 | ~ (member @ X2 @ X3)
% 4.68/1.26 | ~ (zip_tseitin_0 @ (sk__2 @ X3 @ X2) @ X3 @ X2)
% 4.68/1.26 | (better @ X0 @ X3))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_6])).
% 4.68/1.26 thf(zip_derived_cl90, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option, X3 : option_set]:
% 4.68/1.26 ( (member @ (sk__2 @ X1 @ X0) @ X1)
% 4.68/1.26 | ~ (zip_tseitin_2 @ (sk__1 @ X3 @ X2 @ X0) @ X3 @ X2 @ X0)
% 4.68/1.26 | ~ (member @ X2 @ X3)
% 4.68/1.26 | ~ (member @ X0 @ X3)
% 4.68/1.26 | ~ (permitted_preference @ X2 @ X0)
% 4.68/1.26 | ~ (permitted_preference @ X0 @ X2)
% 4.68/1.26 | ~ (member @ X0 @ X1)
% 4.68/1.26 | (better @ X3 @ X1))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl12])).
% 4.68/1.26 thf(zip_derived_cl190, plain,
% 4.68/1.26 (![X0 : option, X1 : option, X2 : option_set, X3 : option_set]:
% 4.68/1.26 ( (member @ (sk__1 @ X2 @ X1 @ X0) @ X2)
% 4.68/1.26 | (member @ (sk__2 @ X3 @ X0) @ X3)
% 4.68/1.26 | ~ (member @ X1 @ X2)
% 4.68/1.26 | ~ (member @ X0 @ X2)
% 4.68/1.26 | ~ (permitted_preference @ X1 @ X0)
% 4.68/1.26 | ~ (permitted_preference @ X0 @ X1)
% 4.68/1.26 | ~ (member @ X0 @ X3)
% 4.68/1.26 | (better @ X2 @ X3))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl11, zip_derived_cl90])).
% 4.68/1.26 thf(zip_derived_cl334, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (member @ (sk__1 @ X0 @ sk__7 @ sk__6) @ X0)
% 4.68/1.26 | (member @ (sk__2 @ X1 @ sk__6) @ X1)
% 4.68/1.26 | ~ (member @ sk__7 @ X0)
% 4.68/1.26 | ~ (member @ sk__6 @ X0)
% 4.68/1.26 | ~ (permitted_preference @ sk__6 @ sk__7)
% 4.68/1.26 | ~ (member @ sk__6 @ X1)
% 4.68/1.26 | (better @ X0 @ X1))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl29, zip_derived_cl190])).
% 4.68/1.26 thf(zip_derived_cl28, plain, ( (permitted_preference @ sk__6 @ sk__7)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl336, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (member @ (sk__1 @ X0 @ sk__7 @ sk__6) @ X0)
% 4.68/1.26 | (member @ (sk__2 @ X1 @ sk__6) @ X1)
% 4.68/1.26 | ~ (member @ sk__7 @ X0)
% 4.68/1.26 | ~ (member @ sk__6 @ X0)
% 4.68/1.26 | ~ (member @ sk__6 @ X1)
% 4.68/1.26 | (better @ X0 @ X1))),
% 4.68/1.26 inference('demod', [status(thm)], [zip_derived_cl334, zip_derived_cl28])).
% 4.68/1.26 thf(zip_derived_cl574, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 ( (member @ (sk__1 @ sk__11 @ sk__7 @ sk__6) @ sk__11)
% 4.68/1.26 | (member @ (sk__2 @ X0 @ sk__6) @ X0)
% 4.68/1.26 | ~ (member @ sk__6 @ sk__11)
% 4.68/1.26 | ~ (member @ sk__6 @ X0)
% 4.68/1.26 | (better @ sk__11 @ X0))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl35, zip_derived_cl336])).
% 4.68/1.26 thf(zip_derived_cl34, plain, ( (member @ sk__6 @ sk__11)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl576, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 ( (member @ (sk__1 @ sk__11 @ sk__7 @ sk__6) @ sk__11)
% 4.68/1.26 | (member @ (sk__2 @ X0 @ sk__6) @ X0)
% 4.68/1.26 | ~ (member @ sk__6 @ X0)
% 4.68/1.26 | (better @ sk__11 @ X0))),
% 4.68/1.26 inference('demod', [status(thm)], [zip_derived_cl574, zip_derived_cl34])).
% 4.68/1.26 thf(zip_derived_cl729, plain,
% 4.68/1.26 (( (member @ (sk__1 @ sk__11 @ sk__7 @ sk__6) @ sk__11)
% 4.68/1.26 | (member @ (sk__2 @ sk__9 @ sk__6) @ sk__9)
% 4.68/1.26 | (better @ sk__11 @ sk__9))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl32, zip_derived_cl576])).
% 4.68/1.26 thf(zip_derived_cl42, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (((X0) = (sk__7)) | ((X0) = (sk__6)) | ~ (member @ X0 @ sk__11))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl794, plain,
% 4.68/1.26 (( (better @ sk__11 @ sk__9)
% 4.68/1.26 | (member @ (sk__2 @ sk__9 @ sk__6) @ sk__9)
% 4.68/1.26 | ((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__7))
% 4.68/1.26 | ((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl729, zip_derived_cl42])).
% 4.68/1.26 thf(zip_derived_cl37, plain,
% 4.68/1.26 (![X0 : option]: (((X0) = (sk__6)) | ~ (member @ X0 @ sk__9))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl816, plain,
% 4.68/1.26 ((((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6))
% 4.68/1.26 | ((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__7))
% 4.68/1.26 | (better @ sk__11 @ sk__9)
% 4.68/1.26 | ((sk__2 @ sk__9 @ sk__6) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl794, zip_derived_cl37])).
% 4.68/1.26 thf(zip_derived_cl90, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option, X3 : option_set]:
% 4.68/1.26 ( (member @ (sk__2 @ X1 @ X0) @ X1)
% 4.68/1.26 | ~ (zip_tseitin_2 @ (sk__1 @ X3 @ X2 @ X0) @ X3 @ X2 @ X0)
% 4.68/1.26 | ~ (member @ X2 @ X3)
% 4.68/1.26 | ~ (member @ X0 @ X3)
% 4.68/1.26 | ~ (permitted_preference @ X2 @ X0)
% 4.68/1.26 | ~ (permitted_preference @ X0 @ X2)
% 4.68/1.26 | ~ (member @ X0 @ X1)
% 4.68/1.26 | (better @ X3 @ X1))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl12])).
% 4.68/1.26 thf(zip_derived_cl821, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 (((sk__2 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | (better @ sk__11 @ sk__9)
% 4.68/1.26 | ((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6))
% 4.68/1.26 | (member @ (sk__2 @ X0 @ sk__6) @ X0)
% 4.68/1.26 | ~ (zip_tseitin_2 @ sk__7 @ sk__11 @ sk__7 @ sk__6)
% 4.68/1.26 | ~ (member @ sk__7 @ sk__11)
% 4.68/1.26 | ~ (member @ sk__6 @ sk__11)
% 4.68/1.26 | ~ (permitted_preference @ sk__7 @ sk__6)
% 4.68/1.26 | ~ (permitted_preference @ sk__6 @ sk__7)
% 4.68/1.26 | ~ (member @ sk__6 @ X0)
% 4.68/1.26 | (better @ sk__11 @ X0))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl816, zip_derived_cl90])).
% 4.68/1.26 thf(zip_derived_cl9, plain,
% 4.68/1.26 (![X0 : option, X1 : option, X2 : option]:
% 4.68/1.26 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | ((X0) != (X1)))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_4])).
% 4.68/1.26 thf(zip_derived_cl60, plain,
% 4.68/1.26 (![X0 : option, X1 : option]: (zip_tseitin_1 @ X1 @ X1 @ X0)),
% 4.68/1.26 inference('eq_res', [status(thm)], [zip_derived_cl9])).
% 4.68/1.26 thf(zip_derived_cl10, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option, X3 : option]:
% 4.68/1.26 ( (zip_tseitin_2 @ X0 @ X1 @ X2 @ X3)
% 4.68/1.26 | ~ (zip_tseitin_1 @ X0 @ X2 @ X3))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_0])).
% 4.68/1.26 thf(zip_derived_cl78, plain,
% 4.68/1.26 (![X0 : option, X1 : option, X2 : option_set]:
% 4.68/1.26 (zip_tseitin_2 @ X1 @ X2 @ X1 @ X0)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl60, zip_derived_cl10])).
% 4.68/1.26 thf(zip_derived_cl35, plain, ( (member @ sk__7 @ sk__11)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl34, plain, ( (member @ sk__6 @ sk__11)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl29, plain, ( (permitted_preference @ sk__7 @ sk__6)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl28, plain, ( (permitted_preference @ sk__6 @ sk__7)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl839, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 (((sk__2 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | (better @ sk__11 @ sk__9)
% 4.68/1.26 | ((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6))
% 4.68/1.26 | (member @ (sk__2 @ X0 @ sk__6) @ X0)
% 4.68/1.26 | ~ (member @ sk__6 @ X0)
% 4.68/1.26 | (better @ sk__11 @ X0))),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl821, zip_derived_cl78, zip_derived_cl35,
% 4.68/1.26 zip_derived_cl34, zip_derived_cl29, zip_derived_cl28])).
% 4.68/1.26 thf(zip_derived_cl26, plain, ( (member @ sk__7 @ sk__12)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(subset, axiom,
% 4.68/1.26 (![A:option_set,B:option_set]:
% 4.68/1.26 ( ( subset @ A @ B ) <=>
% 4.68/1.26 ( ![X:option]: ( ( member @ X @ A ) => ( member @ X @ B ) ) ) ))).
% 4.68/1.26 thf(zip_derived_cl2, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (subset @ X0 @ X1) | (member @ (sk_ @ X1 @ X0) @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [subset])).
% 4.68/1.26 thf(zip_derived_cl42, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (((X0) = (sk__7)) | ((X0) = (sk__6)) | ~ (member @ X0 @ sk__11))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl64, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 ( (subset @ sk__11 @ X0)
% 4.68/1.26 | ((sk_ @ X0 @ sk__11) = (sk__7))
% 4.68/1.26 | ((sk_ @ X0 @ sk__11) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl42])).
% 4.68/1.26 thf(zip_derived_cl1, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (subset @ X0 @ X1) | ~ (member @ (sk_ @ X1 @ X0) @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [subset])).
% 4.68/1.26 thf(zip_derived_cl106, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 (((sk_ @ X0 @ sk__11) = (sk__6))
% 4.68/1.26 | (subset @ sk__11 @ X0)
% 4.68/1.26 | (subset @ sk__11 @ X0)
% 4.68/1.26 | ~ (member @ sk__7 @ X0))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl64, zip_derived_cl1])).
% 4.68/1.26 thf(zip_derived_cl109, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 (~ (member @ sk__7 @ X0)
% 4.68/1.26 | (subset @ sk__11 @ X0)
% 4.68/1.26 | ((sk_ @ X0 @ sk__11) = (sk__6)))),
% 4.68/1.26 inference('simplify', [status(thm)], [zip_derived_cl106])).
% 4.68/1.26 thf(zip_derived_cl171, plain,
% 4.68/1.26 (( (subset @ sk__11 @ sk__12) | ((sk_ @ sk__12 @ sk__11) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl26, zip_derived_cl109])).
% 4.68/1.26 thf(zip_derived_cl1, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (subset @ X0 @ X1) | ~ (member @ (sk_ @ X1 @ X0) @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [subset])).
% 4.68/1.26 thf(zip_derived_cl173, plain,
% 4.68/1.26 (( (subset @ sk__11 @ sk__12)
% 4.68/1.26 | (subset @ sk__11 @ sk__12)
% 4.68/1.26 | ~ (member @ sk__6 @ sk__12))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl171, zip_derived_cl1])).
% 4.68/1.26 thf(zip_derived_cl27, plain, ( (member @ sk__6 @ sk__12)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl176, plain,
% 4.68/1.26 (( (subset @ sk__11 @ sk__12) | (subset @ sk__11 @ sk__12))),
% 4.68/1.26 inference('demod', [status(thm)], [zip_derived_cl173, zip_derived_cl27])).
% 4.68/1.26 thf(zip_derived_cl177, plain, ( (subset @ sk__11 @ sk__12)),
% 4.68/1.26 inference('simplify', [status(thm)], [zip_derived_cl176])).
% 4.68/1.26 thf(harmlessness_of_expansions, axiom,
% 4.68/1.26 (![X:option_set,Y:option_set]:
% 4.68/1.26 ( ( subset @ X @ Y ) => ( weakly_better @ Y @ X ) ))).
% 4.68/1.26 thf(zip_derived_cl16, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (weakly_better @ X0 @ X1) | ~ (subset @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [harmlessness_of_expansions])).
% 4.68/1.26 thf(zip_derived_cl182, plain, ( (weakly_better @ sk__12 @ sk__11)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl177, zip_derived_cl16])).
% 4.68/1.26 thf(zip_derived_cl25, plain, ( (member @ sk__8 @ sk__12)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl2, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (subset @ X0 @ X1) | (member @ (sk_ @ X1 @ X0) @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [subset])).
% 4.68/1.26 thf(zip_derived_cl39, plain,
% 4.68/1.26 (![X0 : option]: (((X0) = (sk__8)) | ~ (member @ X0 @ sk__10))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl51, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 ( (subset @ sk__10 @ X0) | ((sk_ @ X0 @ sk__10) = (sk__8)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl39])).
% 4.68/1.26 thf(zip_derived_cl1, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (subset @ X0 @ X1) | ~ (member @ (sk_ @ X1 @ X0) @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [subset])).
% 4.68/1.26 thf(zip_derived_cl72, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 ( (subset @ sk__10 @ X0)
% 4.68/1.26 | (subset @ sk__10 @ X0)
% 4.68/1.26 | ~ (member @ sk__8 @ X0))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl51, zip_derived_cl1])).
% 4.68/1.26 thf(zip_derived_cl74, plain,
% 4.68/1.26 (![X0 : option_set]: (~ (member @ sk__8 @ X0) | (subset @ sk__10 @ X0))),
% 4.68/1.26 inference('simplify', [status(thm)], [zip_derived_cl72])).
% 4.68/1.26 thf(zip_derived_cl100, plain, ( (subset @ sk__10 @ sk__12)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl25, zip_derived_cl74])).
% 4.68/1.26 thf(zip_derived_cl16, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (weakly_better @ X0 @ X1) | ~ (subset @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [harmlessness_of_expansions])).
% 4.68/1.26 thf(zip_derived_cl102, plain, ( (weakly_better @ sk__12 @ sk__10)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl16])).
% 4.68/1.26 thf(better, axiom,
% 4.68/1.26 (![X:option_set,Y:option_set]:
% 4.68/1.26 ( ( better @ X @ Y ) <=>
% 4.68/1.26 ( ( weakly_better @ X @ Y ) & ( ~( weakly_better @ Y @ X ) ) ) ))).
% 4.68/1.26 thf(zip_derived_cl5, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (better @ X0 @ X1)
% 4.68/1.26 | (weakly_better @ X1 @ X0)
% 4.68/1.26 | ~ (weakly_better @ X0 @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [better])).
% 4.68/1.26 thf(zip_derived_cl104, plain,
% 4.68/1.26 (( (better @ sk__12 @ sk__10) | (weakly_better @ sk__10 @ sk__12))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl102, zip_derived_cl5])).
% 4.68/1.26 thf(zip_derived_cl104, plain,
% 4.68/1.26 (( (better @ sk__12 @ sk__10) | (weakly_better @ sk__10 @ sk__12))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl102, zip_derived_cl5])).
% 4.68/1.26 thf(zip_derived_cl104, plain,
% 4.68/1.26 (( (better @ sk__12 @ sk__10) | (weakly_better @ sk__10 @ sk__12))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl102, zip_derived_cl5])).
% 4.68/1.26 thf(zip_derived_cl33, plain, ( (member @ sk__8 @ sk__10)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl104, plain,
% 4.68/1.26 (( (better @ sk__12 @ sk__10) | (weakly_better @ sk__10 @ sk__12))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl102, zip_derived_cl5])).
% 4.68/1.26 thf(insignificance_of_dominated_options, axiom,
% 4.68/1.26 (![X:option_set,Y:option_set]:
% 4.68/1.26 ( ( ( subset @ X @ Y ) &
% 4.68/1.26 ( ?[U:option]:
% 4.68/1.26 ( ( ![V:option]:
% 4.68/1.26 ( ( ( member @ V @ Y ) & ( ~( member @ V @ X ) ) ) =>
% 4.68/1.26 ( required_preference @ U @ V ) ) ) &
% 4.68/1.26 ( member @ U @ X ) ) ) ) =>
% 4.68/1.26 ( ~( better @ Y @ X ) ) ))).
% 4.68/1.26 thf(zip_derived_cl15, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set, X2 : option]:
% 4.68/1.26 (~ (better @ X0 @ X1)
% 4.68/1.26 | ~ (member @ X2 @ X1)
% 4.68/1.26 | (member @ (sk__3 @ X2 @ X0 @ X1) @ X0)
% 4.68/1.26 | ~ (subset @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [insignificance_of_dominated_options])).
% 4.68/1.26 thf(zip_derived_cl136, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 ( (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | ~ (member @ X0 @ sk__10)
% 4.68/1.26 | (member @ (sk__3 @ X0 @ sk__12 @ sk__10) @ sk__12)
% 4.68/1.26 | ~ (subset @ sk__10 @ sk__12))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl104, zip_derived_cl15])).
% 4.68/1.26 thf(zip_derived_cl100, plain, ( (subset @ sk__10 @ sk__12)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl25, zip_derived_cl74])).
% 4.68/1.26 thf(zip_derived_cl137, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 ( (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | ~ (member @ X0 @ sk__10)
% 4.68/1.26 | (member @ (sk__3 @ X0 @ sk__12 @ sk__10) @ sk__12))),
% 4.68/1.26 inference('demod', [status(thm)], [zip_derived_cl136, zip_derived_cl100])).
% 4.68/1.26 thf(zip_derived_cl290, plain,
% 4.68/1.26 (( (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | (member @ (sk__3 @ sk__8 @ sk__12 @ sk__10) @ sk__12))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl33, zip_derived_cl137])).
% 4.68/1.26 thf(zip_derived_cl21, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (((X0) = (sk__8))
% 4.68/1.26 | ((X0) = (sk__7))
% 4.68/1.26 | ((X0) = (sk__6))
% 4.68/1.26 | ~ (member @ X0 @ sk__12))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl292, plain,
% 4.68/1.26 (( (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__8))
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__7))
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl290, zip_derived_cl21])).
% 4.68/1.26 thf(zip_derived_cl14, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set, X2 : option]:
% 4.68/1.26 (~ (better @ X0 @ X1)
% 4.68/1.26 | ~ (member @ X2 @ X1)
% 4.68/1.26 | ~ (member @ (sk__3 @ X2 @ X0 @ X1) @ X1)
% 4.68/1.26 | ~ (subset @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [insignificance_of_dominated_options])).
% 4.68/1.26 thf(zip_derived_cl371, plain,
% 4.68/1.26 ((((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__6))
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__7))
% 4.68/1.26 | (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | ~ (better @ sk__12 @ sk__10)
% 4.68/1.26 | ~ (member @ sk__8 @ sk__10)
% 4.68/1.26 | ~ (member @ sk__8 @ sk__10)
% 4.68/1.26 | ~ (subset @ sk__10 @ sk__12))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl292, zip_derived_cl14])).
% 4.68/1.26 thf(zip_derived_cl33, plain, ( (member @ sk__8 @ sk__10)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl33, plain, ( (member @ sk__8 @ sk__10)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl100, plain, ( (subset @ sk__10 @ sk__12)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl25, zip_derived_cl74])).
% 4.68/1.26 thf(zip_derived_cl380, plain,
% 4.68/1.26 ((((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__6))
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__7))
% 4.68/1.26 | (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | ~ (better @ sk__12 @ sk__10))),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl371, zip_derived_cl33, zip_derived_cl33,
% 4.68/1.26 zip_derived_cl100])).
% 4.68/1.26 thf(zip_derived_cl4, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 (~ (weakly_better @ X0 @ X1) | ~ (better @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [better])).
% 4.68/1.26 thf(zip_derived_cl477, plain,
% 4.68/1.26 ((~ (better @ sk__12 @ sk__10)
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__7))
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__6)))),
% 4.68/1.26 inference('clc', [status(thm)], [zip_derived_cl380, zip_derived_cl4])).
% 4.68/1.26 thf(zip_derived_cl478, plain,
% 4.68/1.26 (( (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__7))
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl104, zip_derived_cl477])).
% 4.68/1.26 thf(zip_derived_cl13, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set, X2 : option]:
% 4.68/1.26 (~ (better @ X0 @ X1)
% 4.68/1.26 | ~ (member @ X2 @ X1)
% 4.68/1.26 | ~ (required_preference @ X2 @ (sk__3 @ X2 @ X0 @ X1))
% 4.68/1.26 | ~ (subset @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [insignificance_of_dominated_options])).
% 4.68/1.26 thf(zip_derived_cl479, plain,
% 4.68/1.26 ((((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__6))
% 4.68/1.26 | (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | ~ (better @ sk__12 @ sk__10)
% 4.68/1.26 | ~ (member @ sk__8 @ sk__10)
% 4.68/1.26 | ~ (required_preference @ sk__8 @ sk__7)
% 4.68/1.26 | ~ (subset @ sk__10 @ sk__12))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl478, zip_derived_cl13])).
% 4.68/1.26 thf(zip_derived_cl33, plain, ( (member @ sk__8 @ sk__10)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl31, plain, ( (required_preference @ sk__8 @ sk__7)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl100, plain, ( (subset @ sk__10 @ sk__12)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl25, zip_derived_cl74])).
% 4.68/1.26 thf(zip_derived_cl487, plain,
% 4.68/1.26 ((((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__6))
% 4.68/1.26 | (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | ~ (better @ sk__12 @ sk__10))),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl479, zip_derived_cl33, zip_derived_cl31,
% 4.68/1.26 zip_derived_cl100])).
% 4.68/1.26 thf(zip_derived_cl4, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 (~ (weakly_better @ X0 @ X1) | ~ (better @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [better])).
% 4.68/1.26 thf(zip_derived_cl505, plain,
% 4.68/1.26 ((~ (better @ sk__12 @ sk__10)
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__6)))),
% 4.68/1.26 inference('clc', [status(thm)], [zip_derived_cl487, zip_derived_cl4])).
% 4.68/1.26 thf(zip_derived_cl506, plain,
% 4.68/1.26 (( (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | ((sk__3 @ sk__8 @ sk__12 @ sk__10) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl104, zip_derived_cl505])).
% 4.68/1.26 thf(zip_derived_cl13, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set, X2 : option]:
% 4.68/1.26 (~ (better @ X0 @ X1)
% 4.68/1.26 | ~ (member @ X2 @ X1)
% 4.68/1.26 | ~ (required_preference @ X2 @ (sk__3 @ X2 @ X0 @ X1))
% 4.68/1.26 | ~ (subset @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [insignificance_of_dominated_options])).
% 4.68/1.26 thf(zip_derived_cl507, plain,
% 4.68/1.26 (( (weakly_better @ sk__10 @ sk__12)
% 4.68/1.26 | ~ (better @ sk__12 @ sk__10)
% 4.68/1.26 | ~ (member @ sk__8 @ sk__10)
% 4.68/1.26 | ~ (required_preference @ sk__8 @ sk__6)
% 4.68/1.26 | ~ (subset @ sk__10 @ sk__12))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl506, zip_derived_cl13])).
% 4.68/1.26 thf(zip_derived_cl33, plain, ( (member @ sk__8 @ sk__10)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl30, plain, ( (required_preference @ sk__8 @ sk__6)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl100, plain, ( (subset @ sk__10 @ sk__12)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl25, zip_derived_cl74])).
% 4.68/1.26 thf(zip_derived_cl514, plain,
% 4.68/1.26 (( (weakly_better @ sk__10 @ sk__12) | ~ (better @ sk__12 @ sk__10))),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl507, zip_derived_cl33, zip_derived_cl30,
% 4.68/1.26 zip_derived_cl100])).
% 4.68/1.26 thf(zip_derived_cl4, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 (~ (weakly_better @ X0 @ X1) | ~ (better @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [better])).
% 4.68/1.26 thf(zip_derived_cl523, plain, (~ (better @ sk__12 @ sk__10)),
% 4.68/1.26 inference('clc', [status(thm)], [zip_derived_cl514, zip_derived_cl4])).
% 4.68/1.26 thf(zip_derived_cl524, plain, ( (weakly_better @ sk__10 @ sk__12)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl104, zip_derived_cl523])).
% 4.68/1.26 thf(transitivity_of_weakly_better_freedom_of_choice, axiom,
% 4.68/1.26 (![X:option_set,Y:option_set,Z:option_set]:
% 4.68/1.26 ( ( ( weakly_better @ X @ Y ) & ( weakly_better @ Y @ Z ) ) =>
% 4.68/1.26 ( weakly_better @ X @ Z ) ))).
% 4.68/1.26 thf(zip_derived_cl20, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set, X2 : option_set]:
% 4.68/1.26 (~ (weakly_better @ X0 @ X1)
% 4.68/1.26 | ~ (weakly_better @ X1 @ X2)
% 4.68/1.26 | (weakly_better @ X0 @ X2))),
% 4.68/1.26 inference('cnf', [status(esa)],
% 4.68/1.26 [transitivity_of_weakly_better_freedom_of_choice])).
% 4.68/1.26 thf(zip_derived_cl527, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 (~ (weakly_better @ sk__12 @ X0) | (weakly_better @ sk__10 @ X0))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl524, zip_derived_cl20])).
% 4.68/1.26 thf(zip_derived_cl533, plain, ( (weakly_better @ sk__10 @ sk__11)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl182, zip_derived_cl527])).
% 4.68/1.26 thf(parity_of_no_choice_situations, axiom,
% 4.68/1.26 (![X:option,Y:option,U:option_set,V:option_set]:
% 4.68/1.26 ( ( ( ![Z:option]: ( ( member @ Z @ V ) <=> ( ( Z ) = ( Y ) ) ) ) &
% 4.68/1.26 ( ![Z:option]: ( ( member @ Z @ U ) <=> ( ( Z ) = ( X ) ) ) ) ) =>
% 4.68/1.26 ( ~( better @ U @ V ) ) ))).
% 4.68/1.26 thf(zf_stmt_7, axiom,
% 4.68/1.26 (![Z:option,V:option_set,Y:option]:
% 4.68/1.26 ( ( ( member @ Z @ V ) <=> ( ( Z ) = ( Y ) ) ) =>
% 4.68/1.26 ( zip_tseitin_3 @ Z @ V @ Y ) ))).
% 4.68/1.26 thf(zip_derived_cl18, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option]:
% 4.68/1.26 ( (zip_tseitin_3 @ X0 @ X1 @ X2) | ((X0) = (X2)) | (member @ X0 @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_7])).
% 4.68/1.26 thf(zip_derived_cl27, plain, ( (member @ sk__6 @ sk__12)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl2, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (subset @ X0 @ X1) | (member @ (sk_ @ X1 @ X0) @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [subset])).
% 4.68/1.26 thf(zip_derived_cl37, plain,
% 4.68/1.26 (![X0 : option]: (((X0) = (sk__6)) | ~ (member @ X0 @ sk__9))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl50, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 ( (subset @ sk__9 @ X0) | ((sk_ @ X0 @ sk__9) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl2, zip_derived_cl37])).
% 4.68/1.26 thf(zip_derived_cl1, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (subset @ X0 @ X1) | ~ (member @ (sk_ @ X1 @ X0) @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [subset])).
% 4.68/1.26 thf(zip_derived_cl67, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 ( (subset @ sk__9 @ X0)
% 4.68/1.26 | (subset @ sk__9 @ X0)
% 4.68/1.26 | ~ (member @ sk__6 @ X0))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl50, zip_derived_cl1])).
% 4.68/1.26 thf(zip_derived_cl69, plain,
% 4.68/1.26 (![X0 : option_set]: (~ (member @ sk__6 @ X0) | (subset @ sk__9 @ X0))),
% 4.68/1.26 inference('simplify', [status(thm)], [zip_derived_cl67])).
% 4.68/1.26 thf(zip_derived_cl87, plain, ( (subset @ sk__9 @ sk__12)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl27, zip_derived_cl69])).
% 4.68/1.26 thf(zip_derived_cl16, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (weakly_better @ X0 @ X1) | ~ (subset @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [harmlessness_of_expansions])).
% 4.68/1.26 thf(zip_derived_cl92, plain, ( (weakly_better @ sk__12 @ sk__9)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl87, zip_derived_cl16])).
% 4.68/1.26 thf(zip_derived_cl527, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 (~ (weakly_better @ sk__12 @ X0) | (weakly_better @ sk__10 @ X0))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl524, zip_derived_cl20])).
% 4.68/1.26 thf(zip_derived_cl531, plain, ( (weakly_better @ sk__10 @ sk__9)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl92, zip_derived_cl527])).
% 4.68/1.26 thf(zip_derived_cl5, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 ( (better @ X0 @ X1)
% 4.68/1.26 | (weakly_better @ X1 @ X0)
% 4.68/1.26 | ~ (weakly_better @ X0 @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [better])).
% 4.68/1.26 thf(zip_derived_cl535, plain,
% 4.68/1.26 (( (better @ sk__10 @ sk__9) | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl531, zip_derived_cl5])).
% 4.68/1.26 thf(zip_derived_cl535, plain,
% 4.68/1.26 (( (better @ sk__10 @ sk__9) | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl531, zip_derived_cl5])).
% 4.68/1.26 thf(zip_derived_cl535, plain,
% 4.68/1.26 (( (better @ sk__10 @ sk__9) | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl531, zip_derived_cl5])).
% 4.68/1.26 thf(zip_derived_cl18, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option]:
% 4.68/1.26 ( (zip_tseitin_3 @ X0 @ X1 @ X2) | ((X0) = (X2)) | (member @ X0 @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_7])).
% 4.68/1.26 thf(zip_derived_cl18, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option]:
% 4.68/1.26 ( (zip_tseitin_3 @ X0 @ X1 @ X2) | ((X0) = (X2)) | (member @ X0 @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_7])).
% 4.68/1.26 thf(zf_stmt_8, type, zip_tseitin_3 : option > option_set > option > $o).
% 4.68/1.26 thf(zf_stmt_9, axiom,
% 4.68/1.26 (![X:option,Y:option,U:option_set,V:option_set]:
% 4.68/1.26 ( ( ( ![Z:option]: ( zip_tseitin_3 @ Z @ U @ X ) ) &
% 4.68/1.26 ( ![Z:option]: ( zip_tseitin_3 @ Z @ V @ Y ) ) ) =>
% 4.68/1.26 ( ~( better @ U @ V ) ) ))).
% 4.68/1.26 thf(zip_derived_cl19, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option, X2 : option_set, X3 : option]:
% 4.68/1.26 (~ (zip_tseitin_3 @ (sk__4 @ X0 @ X1) @ X0 @ X1)
% 4.68/1.26 | ~ (zip_tseitin_3 @ (sk__5 @ X2 @ X3) @ X2 @ X3)
% 4.68/1.26 | ~ (better @ X0 @ X2))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_9])).
% 4.68/1.26 thf(zip_derived_cl80, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option, X3 : option_set]:
% 4.68/1.26 ( (member @ (sk__4 @ X1 @ X0) @ X1)
% 4.68/1.26 | ((sk__4 @ X1 @ X0) = (X0))
% 4.68/1.26 | ~ (zip_tseitin_3 @ (sk__5 @ X3 @ X2) @ X3 @ X2)
% 4.68/1.26 | ~ (better @ X1 @ X3))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl18, zip_derived_cl19])).
% 4.68/1.26 thf(zip_derived_cl134, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option_set, X3 : option]:
% 4.68/1.26 ( (member @ (sk__5 @ X1 @ X0) @ X1)
% 4.68/1.26 | ((sk__5 @ X1 @ X0) = (X0))
% 4.68/1.26 | (member @ (sk__4 @ X2 @ X3) @ X2)
% 4.68/1.26 | ((sk__4 @ X2 @ X3) = (X3))
% 4.68/1.26 | ~ (better @ X2 @ X1))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl18, zip_derived_cl80])).
% 4.68/1.26 thf(zip_derived_cl551, plain,
% 4.68/1.26 (![X0 : option, X1 : option]:
% 4.68/1.26 ( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | (member @ (sk__5 @ sk__9 @ X0) @ sk__9)
% 4.68/1.26 | ((sk__5 @ sk__9 @ X0) = (X0))
% 4.68/1.26 | (member @ (sk__4 @ sk__10 @ X1) @ sk__10)
% 4.68/1.26 | ((sk__4 @ sk__10 @ X1) = (X1)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl535, zip_derived_cl134])).
% 4.68/1.26 thf(zip_derived_cl37, plain,
% 4.68/1.26 (![X0 : option]: (((X0) = (sk__6)) | ~ (member @ X0 @ sk__9))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl1741, plain,
% 4.68/1.26 (![X0 : option, X1 : option]:
% 4.68/1.26 (((sk__4 @ sk__10 @ X1) = (X1))
% 4.68/1.26 | (member @ (sk__4 @ sk__10 @ X1) @ sk__10)
% 4.68/1.26 | ((sk__5 @ sk__9 @ X0) = (X0))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ((sk__5 @ sk__9 @ X0) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl551, zip_derived_cl37])).
% 4.68/1.26 thf(zip_derived_cl39, plain,
% 4.68/1.26 (![X0 : option]: (((X0) = (sk__8)) | ~ (member @ X0 @ sk__10))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl1810, plain,
% 4.68/1.26 (![X0 : option, X1 : option]:
% 4.68/1.26 (((sk__5 @ sk__9 @ X1) = (sk__6))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ((sk__5 @ sk__9 @ X1) = (X1))
% 4.68/1.26 | ((sk__4 @ sk__10 @ X0) = (X0))
% 4.68/1.26 | ((sk__4 @ sk__10 @ X0) = (sk__8)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl1741, zip_derived_cl39])).
% 4.68/1.26 thf(zip_derived_cl1948, plain,
% 4.68/1.26 (![X0 : option, X1 : option]:
% 4.68/1.26 (((sk__6) != (X0))
% 4.68/1.26 | ((sk__4 @ sk__10 @ X1) = (sk__8))
% 4.68/1.26 | ((sk__4 @ sk__10 @ X1) = (X1))
% 4.68/1.26 | ((sk__5 @ sk__9 @ X0) = (X0))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('eq_fact', [status(thm)], [zip_derived_cl1810])).
% 4.68/1.26 thf(zip_derived_cl1987, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 ( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ((sk__5 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | ((sk__4 @ sk__10 @ X0) = (X0))
% 4.68/1.26 | ((sk__4 @ sk__10 @ X0) = (sk__8)))),
% 4.68/1.26 inference('eq_res', [status(thm)], [zip_derived_cl1948])).
% 4.68/1.26 thf(zip_derived_cl2023, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (((X0) != (sk__8))
% 4.68/1.26 | ((sk__4 @ sk__10 @ X0) = (sk__8))
% 4.68/1.26 | ((sk__5 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('eq_fact', [status(thm)], [zip_derived_cl1987])).
% 4.68/1.26 thf(zip_derived_cl2057, plain,
% 4.68/1.26 (( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ((sk__5 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | ((sk__4 @ sk__10 @ sk__8) = (sk__8)))),
% 4.68/1.26 inference('eq_res', [status(thm)], [zip_derived_cl2023])).
% 4.68/1.26 thf(zip_derived_cl80, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option, X3 : option_set]:
% 4.68/1.26 ( (member @ (sk__4 @ X1 @ X0) @ X1)
% 4.68/1.26 | ((sk__4 @ X1 @ X0) = (X0))
% 4.68/1.26 | ~ (zip_tseitin_3 @ (sk__5 @ X3 @ X2) @ X3 @ X2)
% 4.68/1.26 | ~ (better @ X1 @ X3))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl18, zip_derived_cl19])).
% 4.68/1.26 thf(zip_derived_cl2094, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option]:
% 4.68/1.26 (((sk__4 @ sk__10 @ sk__8) = (sk__8))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | (member @ (sk__4 @ X0 @ X1) @ X0)
% 4.68/1.26 | ((sk__4 @ X0 @ X1) = (X1))
% 4.68/1.26 | ~ (zip_tseitin_3 @ sk__6 @ sk__9 @ sk__6)
% 4.68/1.26 | ~ (better @ X0 @ sk__9))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl2057, zip_derived_cl80])).
% 4.68/1.26 thf(zip_derived_cl32, plain, ( (member @ sk__6 @ sk__9)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl17, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option]:
% 4.68/1.26 ( (zip_tseitin_3 @ X0 @ X1 @ X2)
% 4.68/1.26 | ((X0) != (X2))
% 4.68/1.26 | ~ (member @ X0 @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_7])).
% 4.68/1.26 thf(zip_derived_cl79, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option]:
% 4.68/1.26 (~ (member @ X1 @ X0) | (zip_tseitin_3 @ X1 @ X0 @ X1))),
% 4.68/1.26 inference('eq_res', [status(thm)], [zip_derived_cl17])).
% 4.68/1.26 thf(zip_derived_cl125, plain, ( (zip_tseitin_3 @ sk__6 @ sk__9 @ sk__6)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl32, zip_derived_cl79])).
% 4.68/1.26 thf(zip_derived_cl2109, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option]:
% 4.68/1.26 (((sk__4 @ sk__10 @ sk__8) = (sk__8))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | (member @ (sk__4 @ X0 @ X1) @ X0)
% 4.68/1.26 | ((sk__4 @ X0 @ X1) = (X1))
% 4.68/1.26 | ~ (better @ X0 @ sk__9))),
% 4.68/1.26 inference('demod', [status(thm)], [zip_derived_cl2094, zip_derived_cl125])).
% 4.68/1.26 thf(zip_derived_cl2916, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 ( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ((sk__4 @ sk__10 @ sk__8) = (sk__8))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | (member @ (sk__4 @ sk__10 @ X0) @ sk__10)
% 4.68/1.26 | ((sk__4 @ sk__10 @ X0) = (X0)))),
% 4.68/1.26 inference('s_sup-', [status(thm)],
% 4.68/1.26 [zip_derived_cl535, zip_derived_cl2109])).
% 4.68/1.26 thf(zip_derived_cl2930, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (((sk__4 @ sk__10 @ X0) = (X0))
% 4.68/1.26 | (member @ (sk__4 @ sk__10 @ X0) @ sk__10)
% 4.68/1.26 | ((sk__4 @ sk__10 @ sk__8) = (sk__8))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('simplify', [status(thm)], [zip_derived_cl2916])).
% 4.68/1.26 thf(zip_derived_cl39, plain,
% 4.68/1.26 (![X0 : option]: (((X0) = (sk__8)) | ~ (member @ X0 @ sk__10))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl2932, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 ( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ((sk__4 @ sk__10 @ sk__8) = (sk__8))
% 4.68/1.26 | ((sk__4 @ sk__10 @ X0) = (X0))
% 4.68/1.26 | ((sk__4 @ sk__10 @ X0) = (sk__8)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl2930, zip_derived_cl39])).
% 4.68/1.26 thf(zip_derived_cl3037, plain,
% 4.68/1.26 ((((sk__8) != (sk__8))
% 4.68/1.26 | ((sk__4 @ sk__10 @ sk__8) = (sk__8))
% 4.68/1.26 | ((sk__4 @ sk__10 @ sk__8) = (sk__8))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('eq_fact', [status(thm)], [zip_derived_cl2932])).
% 4.68/1.26 thf(zip_derived_cl3043, plain,
% 4.68/1.26 (( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ((sk__4 @ sk__10 @ sk__8) = (sk__8)))),
% 4.68/1.26 inference('simplify', [status(thm)], [zip_derived_cl3037])).
% 4.68/1.26 thf(zip_derived_cl19, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option, X2 : option_set, X3 : option]:
% 4.68/1.26 (~ (zip_tseitin_3 @ (sk__4 @ X0 @ X1) @ X0 @ X1)
% 4.68/1.26 | ~ (zip_tseitin_3 @ (sk__5 @ X2 @ X3) @ X2 @ X3)
% 4.68/1.26 | ~ (better @ X0 @ X2))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_9])).
% 4.68/1.26 thf(zip_derived_cl3138, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set]:
% 4.68/1.26 ( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ~ (zip_tseitin_3 @ sk__8 @ sk__10 @ sk__8)
% 4.68/1.26 | ~ (zip_tseitin_3 @ (sk__5 @ X1 @ X0) @ X1 @ X0)
% 4.68/1.26 | ~ (better @ sk__10 @ X1))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3043, zip_derived_cl19])).
% 4.68/1.26 thf(zip_derived_cl33, plain, ( (member @ sk__8 @ sk__10)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl79, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option]:
% 4.68/1.26 (~ (member @ X1 @ X0) | (zip_tseitin_3 @ X1 @ X0 @ X1))),
% 4.68/1.26 inference('eq_res', [status(thm)], [zip_derived_cl17])).
% 4.68/1.26 thf(zip_derived_cl130, plain, ( (zip_tseitin_3 @ sk__8 @ sk__10 @ sk__8)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl33, zip_derived_cl79])).
% 4.68/1.26 thf(zip_derived_cl3149, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set]:
% 4.68/1.26 ( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ~ (zip_tseitin_3 @ (sk__5 @ X1 @ X0) @ X1 @ X0)
% 4.68/1.26 | ~ (better @ sk__10 @ X1))),
% 4.68/1.26 inference('demod', [status(thm)], [zip_derived_cl3138, zip_derived_cl130])).
% 4.68/1.26 thf(zip_derived_cl3191, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 ( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ~ (zip_tseitin_3 @ (sk__5 @ sk__9 @ X0) @ sk__9 @ X0))),
% 4.68/1.26 inference('s_sup-', [status(thm)],
% 4.68/1.26 [zip_derived_cl535, zip_derived_cl3149])).
% 4.68/1.26 thf(zip_derived_cl3193, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (~ (zip_tseitin_3 @ (sk__5 @ sk__9 @ X0) @ sk__9 @ X0)
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('simplify', [status(thm)], [zip_derived_cl3191])).
% 4.68/1.26 thf(zip_derived_cl3194, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 ( (member @ (sk__5 @ sk__9 @ X0) @ sk__9)
% 4.68/1.26 | ((sk__5 @ sk__9 @ X0) = (X0))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl18, zip_derived_cl3193])).
% 4.68/1.26 thf(zip_derived_cl37, plain,
% 4.68/1.26 (![X0 : option]: (((X0) = (sk__6)) | ~ (member @ X0 @ sk__9))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl3221, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 ( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ((sk__5 @ sk__9 @ X0) = (X0))
% 4.68/1.26 | ((sk__5 @ sk__9 @ X0) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3194, zip_derived_cl37])).
% 4.68/1.26 thf(zip_derived_cl3386, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (((X0) != (sk__6))
% 4.68/1.26 | ((sk__5 @ sk__9 @ X0) = (sk__6))
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('eq_fact', [status(thm)], [zip_derived_cl3221])).
% 4.68/1.26 thf(zip_derived_cl3423, plain,
% 4.68/1.26 (( (weakly_better @ sk__9 @ sk__10) | ((sk__5 @ sk__9 @ sk__6) = (sk__6)))),
% 4.68/1.26 inference('eq_res', [status(thm)], [zip_derived_cl3386])).
% 4.68/1.26 thf(zip_derived_cl3193, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (~ (zip_tseitin_3 @ (sk__5 @ sk__9 @ X0) @ sk__9 @ X0)
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('simplify', [status(thm)], [zip_derived_cl3191])).
% 4.68/1.26 thf(zip_derived_cl3436, plain,
% 4.68/1.26 (( (weakly_better @ sk__9 @ sk__10)
% 4.68/1.26 | ~ (zip_tseitin_3 @ sk__6 @ sk__9 @ sk__6)
% 4.68/1.26 | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('s_sup-', [status(thm)],
% 4.68/1.26 [zip_derived_cl3423, zip_derived_cl3193])).
% 4.68/1.26 thf(zip_derived_cl125, plain, ( (zip_tseitin_3 @ sk__6 @ sk__9 @ sk__6)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl32, zip_derived_cl79])).
% 4.68/1.26 thf(zip_derived_cl3451, plain,
% 4.68/1.26 (( (weakly_better @ sk__9 @ sk__10) | (weakly_better @ sk__9 @ sk__10))),
% 4.68/1.26 inference('demod', [status(thm)], [zip_derived_cl3436, zip_derived_cl125])).
% 4.68/1.26 thf(zip_derived_cl3452, plain, ( (weakly_better @ sk__9 @ sk__10)),
% 4.68/1.26 inference('simplify', [status(thm)], [zip_derived_cl3451])).
% 4.68/1.26 thf(zip_derived_cl20, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set, X2 : option_set]:
% 4.68/1.26 (~ (weakly_better @ X0 @ X1)
% 4.68/1.26 | ~ (weakly_better @ X1 @ X2)
% 4.68/1.26 | (weakly_better @ X0 @ X2))),
% 4.68/1.26 inference('cnf', [status(esa)],
% 4.68/1.26 [transitivity_of_weakly_better_freedom_of_choice])).
% 4.68/1.26 thf(zip_derived_cl3460, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 (~ (weakly_better @ sk__10 @ X0) | (weakly_better @ sk__9 @ X0))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3452, zip_derived_cl20])).
% 4.68/1.26 thf(zip_derived_cl3474, plain, ( (weakly_better @ sk__9 @ sk__11)),
% 4.68/1.26 inference('s_sup-', [status(thm)],
% 4.68/1.26 [zip_derived_cl533, zip_derived_cl3460])).
% 4.68/1.26 thf(zip_derived_cl4, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option_set]:
% 4.68/1.26 (~ (weakly_better @ X0 @ X1) | ~ (better @ X1 @ X0))),
% 4.68/1.26 inference('cnf', [status(esa)], [better])).
% 4.68/1.26 thf(zip_derived_cl3476, plain, (~ (better @ sk__11 @ sk__9)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3474, zip_derived_cl4])).
% 4.68/1.26 thf(zip_derived_cl3907, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 (((sk__2 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | ((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6))
% 4.68/1.26 | (member @ (sk__2 @ X0 @ sk__6) @ X0)
% 4.68/1.26 | ~ (member @ sk__6 @ X0)
% 4.68/1.26 | (better @ sk__11 @ X0))),
% 4.68/1.26 inference('demod', [status(thm)], [zip_derived_cl839, zip_derived_cl3476])).
% 4.68/1.26 thf(zip_derived_cl3908, plain,
% 4.68/1.26 ((((sk__2 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | ((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6))
% 4.68/1.26 | (member @ (sk__2 @ sk__9 @ sk__6) @ sk__9)
% 4.68/1.26 | (better @ sk__11 @ sk__9))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl32, zip_derived_cl3907])).
% 4.68/1.26 thf(zip_derived_cl3476, plain, (~ (better @ sk__11 @ sk__9)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3474, zip_derived_cl4])).
% 4.68/1.26 thf(zip_derived_cl3911, plain,
% 4.68/1.26 ((((sk__2 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | ((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6))
% 4.68/1.26 | (member @ (sk__2 @ sk__9 @ sk__6) @ sk__9))),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl3908, zip_derived_cl3476])).
% 4.68/1.26 thf(zip_derived_cl36, plain,
% 4.68/1.26 (![X0 : option]: ( (member @ X0 @ sk__9) | ((X0) != (sk__6)))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl3914, plain,
% 4.68/1.26 (( (member @ (sk__2 @ sk__9 @ sk__6) @ sk__9)
% 4.68/1.26 | ((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6)))),
% 4.68/1.26 inference('clc', [status(thm)], [zip_derived_cl3911, zip_derived_cl36])).
% 4.68/1.26 thf(zip_derived_cl37, plain,
% 4.68/1.26 (![X0 : option]: (((X0) = (sk__6)) | ~ (member @ X0 @ sk__9))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl3916, plain,
% 4.68/1.26 ((((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6))
% 4.68/1.26 | ((sk__2 @ sk__9 @ sk__6) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3914, zip_derived_cl37])).
% 4.68/1.26 thf(zip_derived_cl90, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option, X3 : option_set]:
% 4.68/1.26 ( (member @ (sk__2 @ X1 @ X0) @ X1)
% 4.68/1.26 | ~ (zip_tseitin_2 @ (sk__1 @ X3 @ X2 @ X0) @ X3 @ X2 @ X0)
% 4.68/1.26 | ~ (member @ X2 @ X3)
% 4.68/1.26 | ~ (member @ X0 @ X3)
% 4.68/1.26 | ~ (permitted_preference @ X2 @ X0)
% 4.68/1.26 | ~ (permitted_preference @ X0 @ X2)
% 4.68/1.26 | ~ (member @ X0 @ X1)
% 4.68/1.26 | (better @ X3 @ X1))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl7, zip_derived_cl12])).
% 4.68/1.26 thf(zip_derived_cl3919, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 (((sk__2 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | (member @ (sk__2 @ X0 @ sk__6) @ X0)
% 4.68/1.26 | ~ (zip_tseitin_2 @ sk__6 @ sk__11 @ sk__7 @ sk__6)
% 4.68/1.26 | ~ (member @ sk__7 @ sk__11)
% 4.68/1.26 | ~ (member @ sk__6 @ sk__11)
% 4.68/1.26 | ~ (permitted_preference @ sk__7 @ sk__6)
% 4.68/1.26 | ~ (permitted_preference @ sk__6 @ sk__7)
% 4.68/1.26 | ~ (member @ sk__6 @ X0)
% 4.68/1.26 | (better @ sk__11 @ X0))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3916, zip_derived_cl90])).
% 4.68/1.26 thf(zip_derived_cl8, plain,
% 4.68/1.26 (![X0 : option, X1 : option, X2 : option]:
% 4.68/1.26 ( (zip_tseitin_1 @ X0 @ X1 @ X2) | ((X0) != (X2)))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_4])).
% 4.68/1.26 thf(zip_derived_cl59, plain,
% 4.68/1.26 (![X0 : option, X1 : option]: (zip_tseitin_1 @ X0 @ X1 @ X0)),
% 4.68/1.26 inference('eq_res', [status(thm)], [zip_derived_cl8])).
% 4.68/1.26 thf(zip_derived_cl10, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option, X3 : option]:
% 4.68/1.26 ( (zip_tseitin_2 @ X0 @ X1 @ X2 @ X3)
% 4.68/1.26 | ~ (zip_tseitin_1 @ X0 @ X2 @ X3))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_0])).
% 4.68/1.26 thf(zip_derived_cl77, plain,
% 4.68/1.26 (![X0 : option, X1 : option, X2 : option_set]:
% 4.68/1.26 (zip_tseitin_2 @ X0 @ X2 @ X1 @ X0)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl59, zip_derived_cl10])).
% 4.68/1.26 thf(zip_derived_cl35, plain, ( (member @ sk__7 @ sk__11)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl34, plain, ( (member @ sk__6 @ sk__11)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl29, plain, ( (permitted_preference @ sk__7 @ sk__6)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl28, plain, ( (permitted_preference @ sk__6 @ sk__7)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl3942, plain,
% 4.68/1.26 (![X0 : option_set]:
% 4.68/1.26 (((sk__2 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | (member @ (sk__2 @ X0 @ sk__6) @ X0)
% 4.68/1.26 | ~ (member @ sk__6 @ X0)
% 4.68/1.26 | (better @ sk__11 @ X0))),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl3919, zip_derived_cl77, zip_derived_cl35,
% 4.68/1.26 zip_derived_cl34, zip_derived_cl29, zip_derived_cl28])).
% 4.68/1.26 thf(zip_derived_cl3978, plain,
% 4.68/1.26 ((((sk__2 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | (member @ (sk__2 @ sk__9 @ sk__6) @ sk__9)
% 4.68/1.26 | (better @ sk__11 @ sk__9))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl32, zip_derived_cl3942])).
% 4.68/1.26 thf(zip_derived_cl3476, plain, (~ (better @ sk__11 @ sk__9)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3474, zip_derived_cl4])).
% 4.68/1.26 thf(zip_derived_cl3981, plain,
% 4.68/1.26 ((((sk__2 @ sk__9 @ sk__6) = (sk__6))
% 4.68/1.26 | (member @ (sk__2 @ sk__9 @ sk__6) @ sk__9))),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl3978, zip_derived_cl3476])).
% 4.68/1.26 thf(zip_derived_cl36, plain,
% 4.68/1.26 (![X0 : option]: ( (member @ X0 @ sk__9) | ((X0) != (sk__6)))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl3984, plain, ( (member @ (sk__2 @ sk__9 @ sk__6) @ sk__9)),
% 4.68/1.26 inference('clc', [status(thm)], [zip_derived_cl3981, zip_derived_cl36])).
% 4.68/1.26 thf(zip_derived_cl37, plain,
% 4.68/1.26 (![X0 : option]: (((X0) = (sk__6)) | ~ (member @ X0 @ sk__9))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl3986, plain, (((sk__2 @ sk__9 @ sk__6) = (sk__6))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3984, zip_derived_cl37])).
% 4.68/1.26 thf(zip_derived_cl12, plain,
% 4.68/1.26 (![X0 : option_set, X1 : option, X2 : option, X3 : option_set]:
% 4.68/1.26 (~ (zip_tseitin_2 @ (sk__1 @ X0 @ X1 @ X2) @ X0 @ X1 @ X2)
% 4.68/1.26 | ~ (member @ X1 @ X0)
% 4.68/1.26 | ~ (member @ X2 @ X0)
% 4.68/1.26 | ~ (permitted_preference @ X1 @ X2)
% 4.68/1.26 | ~ (permitted_preference @ X2 @ X1)
% 4.68/1.26 | ~ (member @ X2 @ X3)
% 4.68/1.26 | ~ (zip_tseitin_0 @ (sk__2 @ X3 @ X2) @ X3 @ X2)
% 4.68/1.26 | (better @ X0 @ X3))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_6])).
% 4.68/1.26 thf(zip_derived_cl3997, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set]:
% 4.68/1.26 (~ (zip_tseitin_2 @ (sk__1 @ X1 @ X0 @ sk__6) @ X1 @ X0 @ sk__6)
% 4.68/1.26 | ~ (member @ X0 @ X1)
% 4.68/1.26 | ~ (member @ sk__6 @ X1)
% 4.68/1.26 | ~ (permitted_preference @ X0 @ sk__6)
% 4.68/1.26 | ~ (permitted_preference @ sk__6 @ X0)
% 4.68/1.26 | ~ (member @ sk__6 @ sk__9)
% 4.68/1.26 | ~ (zip_tseitin_0 @ sk__6 @ sk__9 @ sk__6)
% 4.68/1.26 | (better @ X1 @ sk__9))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3986, zip_derived_cl12])).
% 4.68/1.26 thf(zip_derived_cl32, plain, ( (member @ sk__6 @ sk__9)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl6, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option]:
% 4.68/1.26 ( (zip_tseitin_0 @ X0 @ X1 @ X2) | ((X0) != (X2)))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_1])).
% 4.68/1.26 thf(zip_derived_cl58, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set]: (zip_tseitin_0 @ X0 @ X1 @ X0)),
% 4.68/1.26 inference('eq_res', [status(thm)], [zip_derived_cl6])).
% 4.68/1.26 thf(zip_derived_cl4000, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set]:
% 4.68/1.26 (~ (zip_tseitin_2 @ (sk__1 @ X1 @ X0 @ sk__6) @ X1 @ X0 @ sk__6)
% 4.68/1.26 | ~ (member @ X0 @ X1)
% 4.68/1.26 | ~ (member @ sk__6 @ X1)
% 4.68/1.26 | ~ (permitted_preference @ X0 @ sk__6)
% 4.68/1.26 | ~ (permitted_preference @ sk__6 @ X0)
% 4.68/1.26 | (better @ X1 @ sk__9))),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl3997, zip_derived_cl32, zip_derived_cl58])).
% 4.68/1.26 thf(zip_derived_cl4009, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (~ (zip_tseitin_2 @ (sk__1 @ sk__11 @ X0 @ sk__6) @ sk__11 @ X0 @
% 4.68/1.26 sk__6)
% 4.68/1.26 | ~ (member @ X0 @ sk__11)
% 4.68/1.26 | ~ (permitted_preference @ X0 @ sk__6)
% 4.68/1.26 | ~ (permitted_preference @ sk__6 @ X0)
% 4.68/1.26 | (better @ sk__11 @ sk__9))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl34, zip_derived_cl4000])).
% 4.68/1.26 thf(zip_derived_cl3476, plain, (~ (better @ sk__11 @ sk__9)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl3474, zip_derived_cl4])).
% 4.68/1.26 thf(zip_derived_cl4012, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (~ (zip_tseitin_2 @ (sk__1 @ sk__11 @ X0 @ sk__6) @ sk__11 @ X0 @
% 4.68/1.26 sk__6)
% 4.68/1.26 | ~ (member @ X0 @ sk__11)
% 4.68/1.26 | ~ (permitted_preference @ X0 @ sk__6)
% 4.68/1.26 | ~ (permitted_preference @ sk__6 @ X0))),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl4009, zip_derived_cl3476])).
% 4.68/1.26 thf(zip_derived_cl4028, plain,
% 4.68/1.26 ((~ (zip_tseitin_2 @ (sk__1 @ sk__11 @ sk__7 @ sk__6) @ sk__11 @ sk__7 @
% 4.68/1.26 sk__6)
% 4.68/1.26 | ~ (permitted_preference @ sk__7 @ sk__6)
% 4.68/1.26 | ~ (permitted_preference @ sk__6 @ sk__7))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl35, zip_derived_cl4012])).
% 4.68/1.26 thf(zip_derived_cl29, plain, ( (permitted_preference @ sk__7 @ sk__6)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl28, plain, ( (permitted_preference @ sk__6 @ sk__7)),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl4030, plain,
% 4.68/1.26 (~ (zip_tseitin_2 @ (sk__1 @ sk__11 @ sk__7 @ sk__6) @ sk__11 @ sk__7 @
% 4.68/1.26 sk__6)),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl4028, zip_derived_cl29, zip_derived_cl28])).
% 4.68/1.26 thf(zip_derived_cl11, plain,
% 4.68/1.26 (![X0 : option, X1 : option_set, X2 : option, X3 : option]:
% 4.68/1.26 ( (zip_tseitin_2 @ X0 @ X1 @ X2 @ X3) | (member @ X0 @ X1))),
% 4.68/1.26 inference('cnf', [status(esa)], [zf_stmt_0])).
% 4.68/1.26 thf(zip_derived_cl4030, plain,
% 4.68/1.26 (~ (zip_tseitin_2 @ (sk__1 @ sk__11 @ sk__7 @ sk__6) @ sk__11 @ sk__7 @
% 4.68/1.26 sk__6)),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl4028, zip_derived_cl29, zip_derived_cl28])).
% 4.68/1.26 thf(zip_derived_cl4031, plain,
% 4.68/1.26 ( (member @ (sk__1 @ sk__11 @ sk__7 @ sk__6) @ sk__11)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl11, zip_derived_cl4030])).
% 4.68/1.26 thf(zip_derived_cl42, plain,
% 4.68/1.26 (![X0 : option]:
% 4.68/1.26 (((X0) = (sk__7)) | ((X0) = (sk__6)) | ~ (member @ X0 @ sk__11))),
% 4.68/1.26 inference('cnf', [status(esa)], [existence_of_dominated_diversity])).
% 4.68/1.26 thf(zip_derived_cl4061, plain,
% 4.68/1.26 ((((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__7))
% 4.68/1.26 | ((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6)))),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl4031, zip_derived_cl42])).
% 4.68/1.26 thf(zip_derived_cl4030, plain,
% 4.68/1.26 (~ (zip_tseitin_2 @ (sk__1 @ sk__11 @ sk__7 @ sk__6) @ sk__11 @ sk__7 @
% 4.68/1.26 sk__6)),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl4028, zip_derived_cl29, zip_derived_cl28])).
% 4.68/1.26 thf(zip_derived_cl4115, plain,
% 4.68/1.26 ((((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6))
% 4.68/1.26 | ~ (zip_tseitin_2 @ sk__7 @ sk__11 @ sk__7 @ sk__6))),
% 4.68/1.26 inference('s_sup-', [status(thm)],
% 4.68/1.26 [zip_derived_cl4061, zip_derived_cl4030])).
% 4.68/1.26 thf(zip_derived_cl78, plain,
% 4.68/1.26 (![X0 : option, X1 : option, X2 : option_set]:
% 4.68/1.26 (zip_tseitin_2 @ X1 @ X2 @ X1 @ X0)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl60, zip_derived_cl10])).
% 4.68/1.26 thf(zip_derived_cl4130, plain,
% 4.68/1.26 (((sk__1 @ sk__11 @ sk__7 @ sk__6) = (sk__6))),
% 4.68/1.26 inference('demod', [status(thm)], [zip_derived_cl4115, zip_derived_cl78])).
% 4.68/1.26 thf(zip_derived_cl77, plain,
% 4.68/1.26 (![X0 : option, X1 : option, X2 : option_set]:
% 4.68/1.26 (zip_tseitin_2 @ X0 @ X2 @ X1 @ X0)),
% 4.68/1.26 inference('s_sup-', [status(thm)], [zip_derived_cl59, zip_derived_cl10])).
% 4.68/1.26 thf(zip_derived_cl4137, plain, ($false),
% 4.68/1.26 inference('demod', [status(thm)],
% 4.68/1.26 [zip_derived_cl4030, zip_derived_cl4130, zip_derived_cl77])).
% 4.68/1.26
% 4.68/1.26 % SZS output end Refutation
% 4.68/1.26
% 4.68/1.26
% 4.68/1.26 % Terminating...
% 5.17/1.35 % Runner terminated.
% 5.17/1.35 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------