%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : MGT039-2 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.yFbTPuKqV6 true
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:25:13 AM UTC 2026
% Result : Unsatisfiable 3.80s 1.18s
% Output : Refutation 3.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT039-2 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.05 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.yFbTPuKqV6 true
% 0.09/0.37 % Computer : n027.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 7 13:00:00 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Running portfolio for 300 s
% 0.09/0.37 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.38 % Number of cores: 8
% 0.09/0.38 % Python version: Python 3.12.3
% 0.09/0.38 % Running in FO mode
% 0.44/0.66 % Total configuration time : 435
% 0.44/0.66 % Estimated wc time : 1092
% 0.44/0.66 % Estimated cpu time (7 cpus) : 156.0
% 0.47/0.78 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.47/0.79 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.47/0.79 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.47/0.79 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.47/0.79 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.47/0.79 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.47/0.79 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.48/0.83 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 3.80/1.18 % Solved by fo/fo7.sh.
% 3.80/1.18 % done 271 iterations in 0.355s
% 3.80/1.18 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 3.80/1.18 % SZS output start Refutation
% 3.80/1.18 thf(selection_favors_type, type, selection_favors: $i > $i > $i > $o).
% 3.80/1.18 thf(first_movers_type, type, first_movers: $i).
% 3.80/1.18 thf(zero_type, type, zero: $i).
% 3.80/1.18 thf(appear_type, type, appear: $i > $i > $i).
% 3.80/1.18 thf(growth_rate_type, type, growth_rate: $i > $i > $i).
% 3.80/1.18 thf(slow_change_type, type, slow_change: $i > $o).
% 3.80/1.18 thf(propagation_strategy_type, type, propagation_strategy: $i > $o).
% 3.80/1.18 thf(cardinality_at_time_type, type, cardinality_at_time: $i > $i > $i).
% 3.80/1.18 thf(greater_or_equal_type, type, greater_or_equal: $i > $i > $o).
% 3.80/1.18 thf(environment_type, type, environment: $i > $o).
% 3.80/1.18 thf(start_time_type, type, start_time: $i > $i).
% 3.80/1.18 thf(subpopulation_type, type, subpopulation: $i > $i > $i > $o).
% 3.80/1.18 thf(observational_period_type, type, observational_period: $i > $o).
% 3.80/1.18 thf(efficient_producers_type, type, efficient_producers: $i).
% 3.80/1.18 thf(sk2_type, type, sk2: $i > $i > $i).
% 3.80/1.18 thf(in_environment_type, type, in_environment: $i > $i > $o).
% 3.80/1.18 thf(subpopulations_type, type, subpopulations: $i > $i > $i > $i > $o).
% 3.80/1.18 thf(sk1_type, type, sk1: $i > $i).
% 3.80/1.18 thf(critical_point_type, type, critical_point: $i > $i).
% 3.80/1.18 thf(greater_type, type, greater: $i > $i > $o).
% 3.80/1.18 thf(sk3_type, type, sk3: $i).
% 3.80/1.18 thf(end_time_type, type, end_time: $i > $i).
% 3.80/1.18 thf(mp_time_of_critical_point_49, axiom,
% 3.80/1.18 (( ~( environment @ A ) ) |
% 3.80/1.18 ( greater_or_equal @ ( critical_point @ A ) @ ( start_time @ A ) ))).
% 3.80/1.18 thf(zip_derived_cl16, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | (greater_or_equal @ (critical_point @ X0) @ (start_time @ X0)))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_time_of_critical_point_49])).
% 3.80/1.18 thf(mp_greater_or_equal_52, axiom,
% 3.80/1.18 (( ~( greater_or_equal @ A @ B ) ) | ( greater @ A @ B ) |
% 3.80/1.18 ( ( A ) = ( B ) ))).
% 3.80/1.18 thf(zip_derived_cl19, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (greater_or_equal @ X0 @ X1) | (greater @ X0 @ X1) | ((X0) = (X1)))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_greater_or_equal_52])).
% 3.80/1.18 thf(zip_derived_cl36, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ((critical_point @ X0) = (start_time @ X0))
% 3.80/1.18 | (greater @ (critical_point @ X0) @ (start_time @ X0)))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl16, zip_derived_cl19])).
% 3.80/1.18 thf(mp3_favoured_trategy_36, axiom,
% 3.80/1.18 (( ~( observational_period @ A ) ) |
% 3.80/1.18 ( ~( propagation_strategy @ first_movers ) ) |
% 3.80/1.18 ( ~( propagation_strategy @ efficient_producers ) ) |
% 3.80/1.18 ( in_environment @ A @ ( sk1 @ A ) ) |
% 3.80/1.18 ( selection_favors @ efficient_producers @ first_movers @ A ))).
% 3.80/1.18 thf(zip_derived_cl3, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (observational_period @ X0)
% 3.80/1.18 | ~ (propagation_strategy @ first_movers)
% 3.80/1.18 | ~ (propagation_strategy @ efficient_producers)
% 3.80/1.18 | (in_environment @ X0 @ (sk1 @ X0))
% 3.80/1.18 | (selection_favors @ efficient_producers @ first_movers @ X0))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp3_favoured_trategy_36])).
% 3.80/1.18 thf(mp_organizational_sets1_40, axiom, (propagation_strategy @ first_movers)).
% 3.80/1.18 thf(zip_derived_cl7, plain, ( (propagation_strategy @ first_movers)),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_organizational_sets1_40])).
% 3.80/1.18 thf(mp_organizational_sets2_41, axiom,
% 3.80/1.18 (propagation_strategy @ efficient_producers)).
% 3.80/1.18 thf(zip_derived_cl8, plain, ( (propagation_strategy @ efficient_producers)),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_organizational_sets2_41])).
% 3.80/1.18 thf(zip_derived_cl68, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (observational_period @ X0)
% 3.80/1.18 | (in_environment @ X0 @ (sk1 @ X0))
% 3.80/1.18 | (selection_favors @ efficient_producers @ first_movers @ X0))),
% 3.80/1.18 inference('demod', [status(thm)],
% 3.80/1.18 [zip_derived_cl3, zip_derived_cl7, zip_derived_cl8])).
% 3.80/1.18 thf(prove_t8_58, conjecture, (~( observational_period @ sk3 ))).
% 3.80/1.18 thf(zf_stmt_0, negated_conjecture, (observational_period @ sk3),
% 3.80/1.18 inference('cnf.neg', [status(esa)], [prove_t8_58])).
% 3.80/1.18 thf(zip_derived_cl25, plain, ( (observational_period @ sk3)),
% 3.80/1.18 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.80/1.18 thf(zip_derived_cl69, plain,
% 3.80/1.18 (( (selection_favors @ efficient_producers @ first_movers @ sk3)
% 3.80/1.18 | (in_environment @ sk3 @ (sk1 @ sk3)))),
% 3.80/1.18 inference('sup+', [status(thm)], [zip_derived_cl68, zip_derived_cl25])).
% 3.80/1.18 thf(prove_t8_60, conjecture,
% 3.80/1.18 (selection_favors @ efficient_producers @ first_movers @ sk3)).
% 3.80/1.18 thf(zf_stmt_1, negated_conjecture,
% 3.80/1.18 (~( selection_favors @ efficient_producers @ first_movers @ sk3 )),
% 3.80/1.18 inference('cnf.neg', [status(esa)], [prove_t8_60])).
% 3.80/1.18 thf(zip_derived_cl27, plain,
% 3.80/1.18 (~ (selection_favors @ efficient_producers @ first_movers @ sk3)),
% 3.80/1.18 inference('cnf', [status(esa)], [zf_stmt_1])).
% 3.80/1.18 thf(zip_derived_cl92, plain, ( (in_environment @ sk3 @ (sk1 @ sk3))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl69, zip_derived_cl27])).
% 3.80/1.18 thf(mp4_critical_point_39, axiom,
% 3.80/1.18 (( ~( observational_period @ A ) ) | ( ~( slow_change @ A ) ) |
% 3.80/1.18 ( ~( environment @ B ) ) | ( ~( in_environment @ A @ B ) ) |
% 3.80/1.18 ( greater @ ( sk2 @ B @ A ) @ ( critical_point @ B ) ))).
% 3.80/1.18 thf(zip_derived_cl6, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (observational_period @ X0)
% 3.80/1.18 | ~ (slow_change @ X0)
% 3.80/1.18 | ~ (environment @ X1)
% 3.80/1.18 | ~ (in_environment @ X0 @ X1)
% 3.80/1.18 | (greater @ (sk2 @ X1 @ X0) @ (critical_point @ X1)))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp4_critical_point_39])).
% 3.80/1.18 thf(zip_derived_cl94, plain,
% 3.80/1.18 (( (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.18 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.18 | ~ (slow_change @ sk3)
% 3.80/1.18 | ~ (observational_period @ sk3))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl92, zip_derived_cl6])).
% 3.80/1.18 thf(mp3_favoured_trategy_35, axiom,
% 3.80/1.18 (( ~( observational_period @ A ) ) |
% 3.80/1.18 ( ~( propagation_strategy @ first_movers ) ) |
% 3.80/1.18 ( ~( propagation_strategy @ efficient_producers ) ) |
% 3.80/1.18 ( environment @ ( sk1 @ A ) ) |
% 3.80/1.18 ( selection_favors @ efficient_producers @ first_movers @ A ))).
% 3.80/1.18 thf(zip_derived_cl2, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (observational_period @ X0)
% 3.80/1.18 | ~ (propagation_strategy @ first_movers)
% 3.80/1.18 | ~ (propagation_strategy @ efficient_producers)
% 3.80/1.18 | (environment @ (sk1 @ X0))
% 3.80/1.18 | (selection_favors @ efficient_producers @ first_movers @ X0))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp3_favoured_trategy_35])).
% 3.80/1.18 thf(zip_derived_cl7, plain, ( (propagation_strategy @ first_movers)),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_organizational_sets1_40])).
% 3.80/1.18 thf(zip_derived_cl8, plain, ( (propagation_strategy @ efficient_producers)),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_organizational_sets2_41])).
% 3.80/1.18 thf(zip_derived_cl62, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (observational_period @ X0)
% 3.80/1.18 | (environment @ (sk1 @ X0))
% 3.80/1.18 | (selection_favors @ efficient_producers @ first_movers @ X0))),
% 3.80/1.18 inference('demod', [status(thm)],
% 3.80/1.18 [zip_derived_cl2, zip_derived_cl7, zip_derived_cl8])).
% 3.80/1.18 thf(zip_derived_cl25, plain, ( (observational_period @ sk3)),
% 3.80/1.18 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.80/1.18 thf(zip_derived_cl63, plain,
% 3.80/1.18 (( (selection_favors @ efficient_producers @ first_movers @ sk3)
% 3.80/1.18 | (environment @ (sk1 @ sk3)))),
% 3.80/1.18 inference('sup+', [status(thm)], [zip_derived_cl62, zip_derived_cl25])).
% 3.80/1.18 thf(zip_derived_cl27, plain,
% 3.80/1.18 (~ (selection_favors @ efficient_producers @ first_movers @ sk3)),
% 3.80/1.18 inference('cnf', [status(esa)], [zf_stmt_1])).
% 3.80/1.18 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.18 thf(prove_t8_59, conjecture, (~( slow_change @ sk3 ))).
% 3.80/1.18 thf(zf_stmt_2, negated_conjecture, (slow_change @ sk3),
% 3.80/1.18 inference('cnf.neg', [status(esa)], [prove_t8_59])).
% 3.80/1.18 thf(zip_derived_cl26, plain, ( (slow_change @ sk3)),
% 3.80/1.18 inference('cnf', [status(esa)], [zf_stmt_2])).
% 3.80/1.18 thf(zip_derived_cl25, plain, ( (observational_period @ sk3)),
% 3.80/1.18 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.80/1.18 thf(zip_derived_cl100, plain,
% 3.80/1.18 ( (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ (critical_point @ (sk1 @ sk3)))),
% 3.80/1.18 inference('demod', [status(thm)],
% 3.80/1.18 [zip_derived_cl94, zip_derived_cl65, zip_derived_cl26,
% 3.80/1.18 zip_derived_cl25])).
% 3.80/1.18 thf(mp_greater_transitivity_50, axiom,
% 3.80/1.18 (( ~( greater @ A @ B ) ) | ( ~( greater @ B @ C ) ) | ( greater @ A @ C ))).
% 3.80/1.18 thf(zip_derived_cl17, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.80/1.18 (~ (greater @ X0 @ X1) | ~ (greater @ X1 @ X2) | (greater @ X0 @ X2))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_greater_transitivity_50])).
% 3.80/1.18 thf(zip_derived_cl114, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 ( (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ X0)
% 3.80/1.18 | ~ (greater @ (critical_point @ (sk1 @ sk3)) @ X0))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl17])).
% 3.80/1.18 thf(zip_derived_cl117, plain,
% 3.80/1.18 ((((critical_point @ (sk1 @ sk3)) = (start_time @ (sk1 @ sk3)))
% 3.80/1.18 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.18 | (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ (start_time @ (sk1 @ sk3))))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl36, zip_derived_cl114])).
% 3.80/1.18 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.18 thf(zip_derived_cl119, plain,
% 3.80/1.18 ((((critical_point @ (sk1 @ sk3)) = (start_time @ (sk1 @ sk3)))
% 3.80/1.18 | (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ (start_time @ (sk1 @ sk3))))),
% 3.80/1.18 inference('demod', [status(thm)], [zip_derived_cl117, zip_derived_cl65])).
% 3.80/1.18 thf(zip_derived_cl92, plain, ( (in_environment @ sk3 @ (sk1 @ sk3))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl69, zip_derived_cl27])).
% 3.80/1.18 thf(mp4_critical_point_38, axiom,
% 3.80/1.18 (( ~( observational_period @ A ) ) | ( ~( slow_change @ A ) ) |
% 3.80/1.18 ( ~( environment @ B ) ) | ( ~( in_environment @ A @ B ) ) |
% 3.80/1.18 ( in_environment @ B @ ( sk2 @ B @ A ) ))).
% 3.80/1.18 thf(zip_derived_cl5, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (observational_period @ X0)
% 3.80/1.18 | ~ (slow_change @ X0)
% 3.80/1.18 | ~ (environment @ X1)
% 3.80/1.18 | ~ (in_environment @ X0 @ X1)
% 3.80/1.18 | (in_environment @ X1 @ (sk2 @ X1 @ X0)))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp4_critical_point_38])).
% 3.80/1.18 thf(zip_derived_cl93, plain,
% 3.80/1.18 (( (in_environment @ (sk1 @ sk3) @ (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.18 | ~ (slow_change @ sk3)
% 3.80/1.18 | ~ (observational_period @ sk3))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl92, zip_derived_cl5])).
% 3.80/1.18 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.18 thf(zip_derived_cl26, plain, ( (slow_change @ sk3)),
% 3.80/1.18 inference('cnf', [status(esa)], [zf_stmt_2])).
% 3.80/1.18 thf(zip_derived_cl25, plain, ( (observational_period @ sk3)),
% 3.80/1.18 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.80/1.18 thf(zip_derived_cl99, plain,
% 3.80/1.18 ( (in_environment @ (sk1 @ sk3) @ (sk2 @ (sk1 @ sk3) @ sk3))),
% 3.80/1.18 inference('demod', [status(thm)],
% 3.80/1.18 [zip_derived_cl93, zip_derived_cl65, zip_derived_cl26,
% 3.80/1.18 zip_derived_cl25])).
% 3.80/1.18 thf(mp_environment_end_point_43, axiom,
% 3.80/1.18 (( ~( environment @ A ) ) | ( ~( in_environment @ A @ B ) ) |
% 3.80/1.18 ( greater_or_equal @ ( end_time @ A ) @ B ))).
% 3.80/1.18 thf(zip_derived_cl10, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (in_environment @ X0 @ X1)
% 3.80/1.18 | (greater_or_equal @ (end_time @ X0) @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_environment_end_point_43])).
% 3.80/1.18 thf(zip_derived_cl19, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (greater_or_equal @ X0 @ X1) | (greater @ X0 @ X1) | ((X0) = (X1)))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_greater_or_equal_52])).
% 3.80/1.18 thf(zip_derived_cl40, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (in_environment @ X1 @ X0)
% 3.80/1.18 | ~ (environment @ X1)
% 3.80/1.18 | ((end_time @ X1) = (X0))
% 3.80/1.18 | (greater @ (end_time @ X1) @ X0))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl10, zip_derived_cl19])).
% 3.80/1.18 thf(zip_derived_cl106, plain,
% 3.80/1.18 (( (greater @ (end_time @ (sk1 @ sk3)) @ (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | ~ (environment @ (sk1 @ sk3)))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl99, zip_derived_cl40])).
% 3.80/1.18 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.18 thf(zip_derived_cl110, plain,
% 3.80/1.18 (( (greater @ (end_time @ (sk1 @ sk3)) @ (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3)))),
% 3.80/1.18 inference('demod', [status(thm)], [zip_derived_cl106, zip_derived_cl65])).
% 3.80/1.18 thf(zip_derived_cl17, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.80/1.18 (~ (greater @ X0 @ X1) | ~ (greater @ X1 @ X2) | (greater @ X0 @ X2))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_greater_transitivity_50])).
% 3.80/1.18 thf(zip_derived_cl115, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | (greater @ (end_time @ (sk1 @ sk3)) @ X0)
% 3.80/1.18 | ~ (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ X0))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl110, zip_derived_cl17])).
% 3.80/1.18 thf(zip_derived_cl236, plain,
% 3.80/1.18 ((((critical_point @ (sk1 @ sk3)) = (start_time @ (sk1 @ sk3)))
% 3.80/1.18 | (greater @ (end_time @ (sk1 @ sk3)) @ (start_time @ (sk1 @ sk3)))
% 3.80/1.18 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3)))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl119, zip_derived_cl115])).
% 3.80/1.18 thf(mp_greater_or_equal_53, axiom,
% 3.80/1.18 (( ~( greater @ A @ B ) ) | ( greater_or_equal @ A @ B ))).
% 3.80/1.18 thf(zip_derived_cl20, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (greater @ X0 @ X1) | (greater_or_equal @ X0 @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_greater_or_equal_53])).
% 3.80/1.18 thf(mp_time_in_environment_42, axiom,
% 3.80/1.18 (( ~( environment @ A ) ) |
% 3.80/1.18 ( ~( greater_or_equal @ B @ ( start_time @ A ) ) ) |
% 3.80/1.18 ( ~( greater_or_equal @ ( end_time @ A ) @ B ) ) |
% 3.80/1.18 ( in_environment @ A @ B ))).
% 3.80/1.18 thf(zip_derived_cl9, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (greater_or_equal @ X1 @ (start_time @ X0))
% 3.80/1.18 | ~ (greater_or_equal @ (end_time @ X0) @ X1)
% 3.80/1.18 | (in_environment @ X0 @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_time_in_environment_42])).
% 3.80/1.18 thf(zip_derived_cl34, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (greater @ X1 @ (start_time @ X0))
% 3.80/1.18 | (in_environment @ X0 @ X1)
% 3.80/1.18 | ~ (greater_or_equal @ (end_time @ X0) @ X1)
% 3.80/1.18 | ~ (environment @ X0))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl9])).
% 3.80/1.18 thf(zip_derived_cl247, plain,
% 3.80/1.18 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | ((critical_point @ (sk1 @ sk3)) = (start_time @ (sk1 @ sk3)))
% 3.80/1.18 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.18 | ~ (greater_or_equal @ (end_time @ (sk1 @ sk3)) @
% 3.80/1.18 (end_time @ (sk1 @ sk3)))
% 3.80/1.18 | (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3))))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl236, zip_derived_cl34])).
% 3.80/1.18 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.18 thf(mp_greater_or_equal_54, axiom,
% 3.80/1.18 (( ( A ) != ( B ) ) | ( greater_or_equal @ A @ B ))).
% 3.80/1.18 thf(zip_derived_cl21, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]: (((X1) != (X0)) | (greater_or_equal @ X1 @ X0))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_greater_or_equal_54])).
% 3.80/1.18 thf(zip_derived_cl29, plain, (![X0 : $i]: (greater_or_equal @ X0 @ X0)),
% 3.80/1.18 inference('eq_res', [status(thm)], [zip_derived_cl21])).
% 3.80/1.18 thf(zip_derived_cl253, plain,
% 3.80/1.18 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | ((critical_point @ (sk1 @ sk3)) = (start_time @ (sk1 @ sk3)))
% 3.80/1.18 | (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3))))),
% 3.80/1.18 inference('demod', [status(thm)],
% 3.80/1.18 [zip_derived_cl247, zip_derived_cl65, zip_derived_cl29])).
% 3.80/1.18 thf(zip_derived_cl20, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (greater @ X0 @ X1) | (greater_or_equal @ X0 @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_greater_or_equal_53])).
% 3.80/1.18 thf(zip_derived_cl29, plain, (![X0 : $i]: (greater_or_equal @ X0 @ X0)),
% 3.80/1.18 inference('eq_res', [status(thm)], [zip_derived_cl21])).
% 3.80/1.18 thf(zip_derived_cl9, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (greater_or_equal @ X1 @ (start_time @ X0))
% 3.80/1.18 | ~ (greater_or_equal @ (end_time @ X0) @ X1)
% 3.80/1.18 | (in_environment @ X0 @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_time_in_environment_42])).
% 3.80/1.18 thf(zip_derived_cl35, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 ( (in_environment @ X0 @ (start_time @ X0))
% 3.80/1.18 | ~ (greater_or_equal @ (end_time @ X0) @ (start_time @ X0))
% 3.80/1.18 | ~ (environment @ X0))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl29, zip_derived_cl9])).
% 3.80/1.18 thf(zip_derived_cl42, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (greater @ (end_time @ X0) @ (start_time @ X0))
% 3.80/1.18 | ~ (environment @ X0)
% 3.80/1.18 | (in_environment @ X0 @ (start_time @ X0)))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl35])).
% 3.80/1.18 thf(zip_derived_cl10, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (in_environment @ X0 @ X1)
% 3.80/1.18 | (greater_or_equal @ (end_time @ X0) @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_environment_end_point_43])).
% 3.80/1.18 thf(zip_derived_cl9, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (greater_or_equal @ X1 @ (start_time @ X0))
% 3.80/1.18 | ~ (greater_or_equal @ (end_time @ X0) @ X1)
% 3.80/1.18 | (in_environment @ X0 @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_time_in_environment_42])).
% 3.80/1.18 thf(zip_derived_cl41, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (in_environment @ X1 @ (start_time @ X0))
% 3.80/1.18 | ~ (environment @ X1)
% 3.80/1.18 | (in_environment @ X0 @ (end_time @ X1))
% 3.80/1.18 | ~ (greater_or_equal @ (end_time @ X0) @ (end_time @ X1))
% 3.80/1.18 | ~ (environment @ X0))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl10, zip_derived_cl9])).
% 3.80/1.18 thf(zip_derived_cl82, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (greater @ (end_time @ X0) @ (start_time @ X0))
% 3.80/1.18 | ~ (environment @ X0)
% 3.80/1.18 | ~ (greater_or_equal @ (end_time @ X0) @ (end_time @ X0))
% 3.80/1.18 | (in_environment @ X0 @ (end_time @ X0))
% 3.80/1.18 | ~ (environment @ X0))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl42, zip_derived_cl41])).
% 3.80/1.18 thf(zip_derived_cl29, plain, (![X0 : $i]: (greater_or_equal @ X0 @ X0)),
% 3.80/1.18 inference('eq_res', [status(thm)], [zip_derived_cl21])).
% 3.80/1.18 thf(zip_derived_cl83, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (greater @ (end_time @ X0) @ (start_time @ X0))
% 3.80/1.18 | ~ (environment @ X0)
% 3.80/1.18 | (in_environment @ X0 @ (end_time @ X0))
% 3.80/1.18 | ~ (environment @ X0))),
% 3.80/1.18 inference('demod', [status(thm)], [zip_derived_cl82, zip_derived_cl29])).
% 3.80/1.18 thf(zip_derived_cl84, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 ( (in_environment @ X0 @ (end_time @ X0))
% 3.80/1.18 | ~ (greater @ (end_time @ X0) @ (start_time @ X0))
% 3.80/1.18 | ~ (environment @ X0))),
% 3.80/1.18 inference('simplify', [status(thm)], [zip_derived_cl83])).
% 3.80/1.18 thf(zip_derived_cl268, plain,
% 3.80/1.18 ((~ (greater @ (end_time @ (sk1 @ sk3)) @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.18 | (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.18 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.18 | (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3))))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl253, zip_derived_cl84])).
% 3.80/1.18 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.18 thf(zip_derived_cl286, plain,
% 3.80/1.18 ((~ (greater @ (end_time @ (sk1 @ sk3)) @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.18 | (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.18 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3))))),
% 3.80/1.18 inference('demod', [status(thm)], [zip_derived_cl268, zip_derived_cl65])).
% 3.80/1.18 thf(zip_derived_cl287, plain,
% 3.80/1.18 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.18 | ~ (greater @ (end_time @ (sk1 @ sk3)) @
% 3.80/1.18 (critical_point @ (sk1 @ sk3))))),
% 3.80/1.18 inference('simplify', [status(thm)], [zip_derived_cl286])).
% 3.80/1.18 thf(zip_derived_cl100, plain,
% 3.80/1.18 ( (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ (critical_point @ (sk1 @ sk3)))),
% 3.80/1.18 inference('demod', [status(thm)],
% 3.80/1.18 [zip_derived_cl94, zip_derived_cl65, zip_derived_cl26,
% 3.80/1.18 zip_derived_cl25])).
% 3.80/1.18 thf(zip_derived_cl115, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.18 | (greater @ (end_time @ (sk1 @ sk3)) @ X0)
% 3.80/1.18 | ~ (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ X0))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl110, zip_derived_cl17])).
% 3.80/1.18 thf(zip_derived_cl235, plain,
% 3.80/1.18 (( (greater @ (end_time @ (sk1 @ sk3)) @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.18 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3)))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl115])).
% 3.80/1.18 thf(zip_derived_cl344, plain,
% 3.80/1.18 (( (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.18 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3)))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl287, zip_derived_cl235])).
% 3.80/1.18 thf(zip_derived_cl99, plain,
% 3.80/1.18 ( (in_environment @ (sk1 @ sk3) @ (sk2 @ (sk1 @ sk3) @ sk3))),
% 3.80/1.18 inference('demod', [status(thm)],
% 3.80/1.18 [zip_derived_cl93, zip_derived_cl65, zip_derived_cl26,
% 3.80/1.18 zip_derived_cl25])).
% 3.80/1.18 thf(zip_derived_cl345, plain,
% 3.80/1.18 (( (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.18 | (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3))))),
% 3.80/1.18 inference('sup+', [status(thm)], [zip_derived_cl344, zip_derived_cl99])).
% 3.80/1.18 thf(zip_derived_cl355, plain,
% 3.80/1.18 ( (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))),
% 3.80/1.18 inference('simplify', [status(thm)], [zip_derived_cl345])).
% 3.80/1.18 thf(mp_subpopulations_47, axiom,
% 3.80/1.18 (( ~( environment @ A ) ) | ( ~( in_environment @ A @ B ) ) |
% 3.80/1.18 ( subpopulation @ efficient_producers @ A @ B ))).
% 3.80/1.18 thf(zip_derived_cl14, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (in_environment @ X0 @ X1)
% 3.80/1.18 | (subpopulation @ efficient_producers @ X0 @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_subpopulations_47])).
% 3.80/1.18 thf(zip_derived_cl360, plain,
% 3.80/1.18 (( (subpopulation @ efficient_producers @ (sk1 @ sk3) @
% 3.80/1.18 (end_time @ (sk1 @ sk3)))
% 3.80/1.18 | ~ (environment @ (sk1 @ sk3)))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl355, zip_derived_cl14])).
% 3.80/1.18 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.18 thf(zip_derived_cl365, plain,
% 3.80/1.18 ( (subpopulation @ efficient_producers @ (sk1 @ sk3) @
% 3.80/1.18 (end_time @ (sk1 @ sk3)))),
% 3.80/1.18 inference('demod', [status(thm)], [zip_derived_cl360, zip_derived_cl65])).
% 3.80/1.18 thf(zip_derived_cl355, plain,
% 3.80/1.18 ( (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))),
% 3.80/1.18 inference('simplify', [status(thm)], [zip_derived_cl345])).
% 3.80/1.18 thf(zip_derived_cl355, plain,
% 3.80/1.18 ( (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))),
% 3.80/1.18 inference('simplify', [status(thm)], [zip_derived_cl345])).
% 3.80/1.18 thf(mp_first_movers_exist_45, axiom,
% 3.80/1.18 (( ~( environment @ A ) ) | ( ~( in_environment @ A @ B ) ) |
% 3.80/1.18 ( greater_or_equal @ ( cardinality_at_time @ first_movers @ B ) @ zero ))).
% 3.80/1.18 thf(zip_derived_cl12, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (in_environment @ X0 @ X1)
% 3.80/1.18 | (greater_or_equal @ (cardinality_at_time @ first_movers @ X1) @
% 3.80/1.18 zero))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_first_movers_exist_45])).
% 3.80/1.18 thf(zip_derived_cl358, plain,
% 3.80/1.18 (( (greater_or_equal @
% 3.80/1.18 (cardinality_at_time @ first_movers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.18 zero)
% 3.80/1.18 | ~ (environment @ (sk1 @ sk3)))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl355, zip_derived_cl12])).
% 3.80/1.18 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.18 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.18 thf(zip_derived_cl363, plain,
% 3.80/1.18 ( (greater_or_equal @
% 3.80/1.18 (cardinality_at_time @ first_movers @ (end_time @ (sk1 @ sk3))) @ zero)),
% 3.80/1.18 inference('demod', [status(thm)], [zip_derived_cl358, zip_derived_cl65])).
% 3.80/1.18 thf(zip_derived_cl19, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (greater_or_equal @ X0 @ X1) | (greater @ X0 @ X1) | ((X0) = (X1)))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_greater_or_equal_52])).
% 3.80/1.18 thf(zip_derived_cl368, plain,
% 3.80/1.18 ((((cardinality_at_time @ first_movers @ (end_time @ (sk1 @ sk3)))
% 3.80/1.18 = (zero))
% 3.80/1.18 | (greater @
% 3.80/1.18 (cardinality_at_time @ first_movers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.18 zero))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl363, zip_derived_cl19])).
% 3.80/1.18 thf(mp_contains_FM_and_EP_44, axiom,
% 3.80/1.18 (( ~( environment @ A ) ) | ( ~( in_environment @ A @ B ) ) |
% 3.80/1.18 ( ~( greater @ ( cardinality_at_time @ first_movers @ B ) @ zero ) ) |
% 3.80/1.18 ( ~( greater @ ( cardinality_at_time @ efficient_producers @ B ) @ zero ) ) |
% 3.80/1.18 ( subpopulations @ first_movers @ efficient_producers @ A @ B ))).
% 3.80/1.18 thf(zip_derived_cl11, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (in_environment @ X0 @ X1)
% 3.80/1.18 | ~ (greater @ (cardinality_at_time @ first_movers @ X1) @ zero)
% 3.80/1.18 | ~ (greater @ (cardinality_at_time @ efficient_producers @ X1) @
% 3.80/1.18 zero)
% 3.80/1.18 | (subpopulations @ first_movers @ efficient_producers @ X0 @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_contains_FM_and_EP_44])).
% 3.80/1.18 thf(zip_derived_cl371, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (((cardinality_at_time @ first_movers @ (end_time @ (sk1 @ sk3)))
% 3.80/1.18 = (zero))
% 3.80/1.18 | (subpopulations @ first_movers @ efficient_producers @ X0 @
% 3.80/1.18 (end_time @ (sk1 @ sk3)))
% 3.80/1.18 | ~ (greater @
% 3.80/1.18 (cardinality_at_time @ efficient_producers @
% 3.80/1.18 (end_time @ (sk1 @ sk3))) @
% 3.80/1.18 zero)
% 3.80/1.18 | ~ (in_environment @ X0 @ (end_time @ (sk1 @ sk3)))
% 3.80/1.18 | ~ (environment @ X0))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl368, zip_derived_cl11])).
% 3.80/1.18 thf(zip_derived_cl20, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (greater @ X0 @ X1) | (greater_or_equal @ X0 @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_greater_or_equal_53])).
% 3.80/1.18 thf(zip_derived_cl16, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | (greater_or_equal @ (critical_point @ X0) @ (start_time @ X0)))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_time_of_critical_point_49])).
% 3.80/1.18 thf(zip_derived_cl9, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ~ (greater_or_equal @ X1 @ (start_time @ X0))
% 3.80/1.18 | ~ (greater_or_equal @ (end_time @ X0) @ X1)
% 3.80/1.18 | (in_environment @ X0 @ X1))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_time_in_environment_42])).
% 3.80/1.18 thf(zip_derived_cl37, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | (in_environment @ X0 @ (critical_point @ X0))
% 3.80/1.18 | ~ (greater_or_equal @ (end_time @ X0) @ (critical_point @ X0))
% 3.80/1.18 | ~ (environment @ X0))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl16, zip_derived_cl9])).
% 3.80/1.18 thf(zip_derived_cl38, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (greater_or_equal @ (end_time @ X0) @ (critical_point @ X0))
% 3.80/1.18 | (in_environment @ X0 @ (critical_point @ X0))
% 3.80/1.18 | ~ (environment @ X0))),
% 3.80/1.18 inference('simplify', [status(thm)], [zip_derived_cl37])).
% 3.80/1.18 thf(zip_derived_cl46, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (greater @ (end_time @ X0) @ (critical_point @ X0))
% 3.80/1.18 | ~ (environment @ X0)
% 3.80/1.18 | (in_environment @ X0 @ (critical_point @ X0)))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl38])).
% 3.80/1.18 thf(mp_critical_point_after_EP_48, axiom,
% 3.80/1.18 (( ~( environment @ A ) ) |
% 3.80/1.18 ( greater_or_equal @
% 3.80/1.18 ( critical_point @ A ) @ ( appear @ efficient_producers @ A ) ))).
% 3.80/1.18 thf(zip_derived_cl15, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | (greater_or_equal @ (critical_point @ X0) @
% 3.80/1.18 (appear @ efficient_producers @ X0)))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_critical_point_after_EP_48])).
% 3.80/1.18 thf(zip_derived_cl19, plain,
% 3.80/1.18 (![X0 : $i, X1 : $i]:
% 3.80/1.18 (~ (greater_or_equal @ X0 @ X1) | (greater @ X0 @ X1) | ((X0) = (X1)))),
% 3.80/1.18 inference('cnf', [status(esa)], [mp_greater_or_equal_52])).
% 3.80/1.18 thf(zip_derived_cl39, plain,
% 3.80/1.18 (![X0 : $i]:
% 3.80/1.18 (~ (environment @ X0)
% 3.80/1.18 | ((critical_point @ X0) = (appear @ efficient_producers @ X0))
% 3.80/1.18 | (greater @ (critical_point @ X0) @
% 3.80/1.18 (appear @ efficient_producers @ X0)))),
% 3.80/1.18 inference('sup-', [status(thm)], [zip_derived_cl15, zip_derived_cl19])).
% 3.80/1.18 thf(zip_derived_cl114, plain,
% 3.80/1.19 (![X0 : $i]:
% 3.80/1.19 ( (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ X0)
% 3.80/1.19 | ~ (greater @ (critical_point @ (sk1 @ sk3)) @ X0))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl17])).
% 3.80/1.19 thf(zip_derived_cl118, plain,
% 3.80/1.19 ((((critical_point @ (sk1 @ sk3))
% 3.80/1.19 = (appear @ efficient_producers @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.19 | (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @
% 3.80/1.19 (appear @ efficient_producers @ (sk1 @ sk3))))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl39, zip_derived_cl114])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl120, plain,
% 3.80/1.19 ((((critical_point @ (sk1 @ sk3))
% 3.80/1.19 = (appear @ efficient_producers @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @
% 3.80/1.19 (appear @ efficient_producers @ (sk1 @ sk3))))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl118, zip_derived_cl65])).
% 3.80/1.19 thf(zip_derived_cl115, plain,
% 3.80/1.19 (![X0 : $i]:
% 3.80/1.19 (((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | (greater @ (end_time @ (sk1 @ sk3)) @ X0)
% 3.80/1.19 | ~ (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ X0))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl110, zip_derived_cl17])).
% 3.80/1.19 thf(zip_derived_cl237, plain,
% 3.80/1.19 ((((critical_point @ (sk1 @ sk3))
% 3.80/1.19 = (appear @ efficient_producers @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @ (end_time @ (sk1 @ sk3)) @
% 3.80/1.19 (appear @ efficient_producers @ (sk1 @ sk3)))
% 3.80/1.19 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3)))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl120, zip_derived_cl115])).
% 3.80/1.19 thf(zip_derived_cl20, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (greater @ X0 @ X1) | (greater_or_equal @ X0 @ X1))),
% 3.80/1.19 inference('cnf', [status(esa)], [mp_greater_or_equal_53])).
% 3.80/1.19 thf(t6_57, axiom,
% 3.80/1.19 (( ~( environment @ A ) ) | ( ~( in_environment @ A @ B ) ) |
% 3.80/1.19 ( ~( greater_or_equal @ B @ ( appear @ efficient_producers @ A ) ) ) |
% 3.80/1.19 ( greater @ ( cardinality_at_time @ efficient_producers @ B ) @ zero ))).
% 3.80/1.19 thf(zip_derived_cl24, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (environment @ X0)
% 3.80/1.19 | ~ (in_environment @ X0 @ X1)
% 3.80/1.19 | ~ (greater_or_equal @ X1 @ (appear @ efficient_producers @ X0))
% 3.80/1.19 | (greater @ (cardinality_at_time @ efficient_producers @ X1) @ zero))),
% 3.80/1.19 inference('cnf', [status(esa)], [t6_57])).
% 3.80/1.19 thf(zip_derived_cl87, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (greater @ X1 @ (appear @ efficient_producers @ X0))
% 3.80/1.19 | (greater @ (cardinality_at_time @ efficient_producers @ X1) @ zero)
% 3.80/1.19 | ~ (in_environment @ X0 @ X1)
% 3.80/1.19 | ~ (environment @ X0))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl24])).
% 3.80/1.19 thf(zip_derived_cl295, plain,
% 3.80/1.19 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | ((critical_point @ (sk1 @ sk3))
% 3.80/1.19 = (appear @ efficient_producers @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.19 | ~ (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl237, zip_derived_cl87])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl297, plain,
% 3.80/1.19 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | ((critical_point @ (sk1 @ sk3))
% 3.80/1.19 = (appear @ efficient_producers @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl295, zip_derived_cl65])).
% 3.80/1.19 thf(zip_derived_cl355, plain,
% 3.80/1.19 ( (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))),
% 3.80/1.19 inference('simplify', [status(thm)], [zip_derived_cl345])).
% 3.80/1.19 thf(zip_derived_cl560, plain,
% 3.80/1.19 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | ((critical_point @ (sk1 @ sk3))
% 3.80/1.19 = (appear @ efficient_producers @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl297, zip_derived_cl355])).
% 3.80/1.19 thf(zip_derived_cl355, plain,
% 3.80/1.19 ( (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))),
% 3.80/1.19 inference('simplify', [status(thm)], [zip_derived_cl345])).
% 3.80/1.19 thf(zip_derived_cl10, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (environment @ X0)
% 3.80/1.19 | ~ (in_environment @ X0 @ X1)
% 3.80/1.19 | (greater_or_equal @ (end_time @ X0) @ X1))),
% 3.80/1.19 inference('cnf', [status(esa)], [mp_environment_end_point_43])).
% 3.80/1.19 thf(zip_derived_cl24, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (environment @ X0)
% 3.80/1.19 | ~ (in_environment @ X0 @ X1)
% 3.80/1.19 | ~ (greater_or_equal @ X1 @ (appear @ efficient_producers @ X0))
% 3.80/1.19 | (greater @ (cardinality_at_time @ efficient_producers @ X1) @ zero))),
% 3.80/1.19 inference('cnf', [status(esa)], [t6_57])).
% 3.80/1.19 thf(zip_derived_cl89, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (in_environment @ X1 @ (appear @ efficient_producers @ X0))
% 3.80/1.19 | ~ (environment @ X1)
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @ (end_time @ X1)) @
% 3.80/1.19 zero)
% 3.80/1.19 | ~ (in_environment @ X0 @ (end_time @ X1))
% 3.80/1.19 | ~ (environment @ X0))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl10, zip_derived_cl24])).
% 3.80/1.19 thf(zip_derived_cl362, plain,
% 3.80/1.19 ((~ (environment @ (sk1 @ sk3))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero)
% 3.80/1.19 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.19 | ~ (in_environment @ (sk1 @ sk3) @
% 3.80/1.19 (appear @ efficient_producers @ (sk1 @ sk3))))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl355, zip_derived_cl89])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl367, plain,
% 3.80/1.19 (( (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero)
% 3.80/1.19 | ~ (in_environment @ (sk1 @ sk3) @
% 3.80/1.19 (appear @ efficient_producers @ (sk1 @ sk3))))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl362, zip_derived_cl65, zip_derived_cl65])).
% 3.80/1.19 thf(zip_derived_cl573, plain,
% 3.80/1.19 ((~ (in_environment @ (sk1 @ sk3) @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero)
% 3.80/1.19 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl560, zip_derived_cl367])).
% 3.80/1.19 thf(zip_derived_cl585, plain,
% 3.80/1.19 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero)
% 3.80/1.19 | ~ (in_environment @ (sk1 @ sk3) @ (critical_point @ (sk1 @ sk3))))),
% 3.80/1.19 inference('simplify', [status(thm)], [zip_derived_cl573])).
% 3.80/1.19 thf(zip_derived_cl586, plain,
% 3.80/1.19 ((~ (environment @ (sk1 @ sk3))
% 3.80/1.19 | ~ (greater @ (end_time @ (sk1 @ sk3)) @
% 3.80/1.19 (critical_point @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero)
% 3.80/1.19 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3)))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl46, zip_derived_cl585])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl588, plain,
% 3.80/1.19 ((~ (greater @ (end_time @ (sk1 @ sk3)) @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero)
% 3.80/1.19 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3)))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl586, zip_derived_cl65])).
% 3.80/1.19 thf(zip_derived_cl235, plain,
% 3.80/1.19 (( (greater @ (end_time @ (sk1 @ sk3)) @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.19 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3)))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl115])).
% 3.80/1.19 thf(zip_derived_cl590, plain,
% 3.80/1.19 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl588, zip_derived_cl235])).
% 3.80/1.19 thf(zip_derived_cl20, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (greater @ X0 @ X1) | (greater_or_equal @ X0 @ X1))),
% 3.80/1.19 inference('cnf', [status(esa)], [mp_greater_or_equal_53])).
% 3.80/1.19 thf(zip_derived_cl99, plain,
% 3.80/1.19 ( (in_environment @ (sk1 @ sk3) @ (sk2 @ (sk1 @ sk3) @ sk3))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl93, zip_derived_cl65, zip_derived_cl26,
% 3.80/1.19 zip_derived_cl25])).
% 3.80/1.19 thf(zip_derived_cl120, plain,
% 3.80/1.19 ((((critical_point @ (sk1 @ sk3))
% 3.80/1.19 = (appear @ efficient_producers @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @
% 3.80/1.19 (appear @ efficient_producers @ (sk1 @ sk3))))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl118, zip_derived_cl65])).
% 3.80/1.19 thf(zip_derived_cl87, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (greater @ X1 @ (appear @ efficient_producers @ X0))
% 3.80/1.19 | (greater @ (cardinality_at_time @ efficient_producers @ X1) @ zero)
% 3.80/1.19 | ~ (in_environment @ X0 @ X1)
% 3.80/1.19 | ~ (environment @ X0))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl24])).
% 3.80/1.19 thf(zip_derived_cl137, plain,
% 3.80/1.19 ((((critical_point @ (sk1 @ sk3))
% 3.80/1.19 = (appear @ efficient_producers @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.19 | ~ (in_environment @ (sk1 @ sk3) @ (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (sk2 @ (sk1 @ sk3) @ sk3)) @
% 3.80/1.19 zero))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl120, zip_derived_cl87])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl99, plain,
% 3.80/1.19 ( (in_environment @ (sk1 @ sk3) @ (sk2 @ (sk1 @ sk3) @ sk3))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl93, zip_derived_cl65, zip_derived_cl26,
% 3.80/1.19 zip_derived_cl25])).
% 3.80/1.19 thf(zip_derived_cl138, plain,
% 3.80/1.19 ((((critical_point @ (sk1 @ sk3))
% 3.80/1.19 = (appear @ efficient_producers @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (sk2 @ (sk1 @ sk3) @ sk3)) @
% 3.80/1.19 zero))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl137, zip_derived_cl65, zip_derived_cl99])).
% 3.80/1.19 thf(zip_derived_cl24, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (environment @ X0)
% 3.80/1.19 | ~ (in_environment @ X0 @ X1)
% 3.80/1.19 | ~ (greater_or_equal @ X1 @ (appear @ efficient_producers @ X0))
% 3.80/1.19 | (greater @ (cardinality_at_time @ efficient_producers @ X1) @ zero))),
% 3.80/1.19 inference('cnf', [status(esa)], [t6_57])).
% 3.80/1.19 thf(zip_derived_cl140, plain,
% 3.80/1.19 (![X0 : $i]:
% 3.80/1.19 (~ (greater_or_equal @ X0 @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (sk2 @ (sk1 @ sk3) @ sk3)) @
% 3.80/1.19 zero)
% 3.80/1.19 | (greater @ (cardinality_at_time @ efficient_producers @ X0) @ zero)
% 3.80/1.19 | ~ (in_environment @ (sk1 @ sk3) @ X0)
% 3.80/1.19 | ~ (environment @ (sk1 @ sk3)))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl138, zip_derived_cl24])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl147, plain,
% 3.80/1.19 (![X0 : $i]:
% 3.80/1.19 (~ (greater_or_equal @ X0 @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (sk2 @ (sk1 @ sk3) @ sk3)) @
% 3.80/1.19 zero)
% 3.80/1.19 | (greater @ (cardinality_at_time @ efficient_producers @ X0) @ zero)
% 3.80/1.19 | ~ (in_environment @ (sk1 @ sk3) @ X0))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl140, zip_derived_cl65])).
% 3.80/1.19 thf(zip_derived_cl529, plain,
% 3.80/1.19 (( (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (sk2 @ (sk1 @ sk3) @ sk3)) @
% 3.80/1.19 zero)
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (sk2 @ (sk1 @ sk3) @ sk3)) @
% 3.80/1.19 zero)
% 3.80/1.19 | ~ (greater_or_equal @ (sk2 @ (sk1 @ sk3) @ sk3) @
% 3.80/1.19 (critical_point @ (sk1 @ sk3))))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl99, zip_derived_cl147])).
% 3.80/1.19 thf(zip_derived_cl533, plain,
% 3.80/1.19 ((~ (greater_or_equal @ (sk2 @ (sk1 @ sk3) @ sk3) @
% 3.80/1.19 (critical_point @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (sk2 @ (sk1 @ sk3) @ sk3)) @
% 3.80/1.19 zero))),
% 3.80/1.19 inference('simplify', [status(thm)], [zip_derived_cl529])).
% 3.80/1.19 thf(zip_derived_cl535, plain,
% 3.80/1.19 ((~ (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (sk2 @ (sk1 @ sk3) @ sk3)) @
% 3.80/1.19 zero))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl20, zip_derived_cl533])).
% 3.80/1.19 thf(zip_derived_cl100, plain,
% 3.80/1.19 ( (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ (critical_point @ (sk1 @ sk3)))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl94, zip_derived_cl65, zip_derived_cl26,
% 3.80/1.19 zip_derived_cl25])).
% 3.80/1.19 thf(zip_derived_cl536, plain,
% 3.80/1.19 ( (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @ (sk2 @ (sk1 @ sk3) @ sk3)) @
% 3.80/1.19 zero)),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl535, zip_derived_cl100])).
% 3.80/1.19 thf(zip_derived_cl603, plain,
% 3.80/1.19 (( (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero)
% 3.80/1.19 | (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero))),
% 3.80/1.19 inference('sup+', [status(thm)], [zip_derived_cl590, zip_derived_cl536])).
% 3.80/1.19 thf(zip_derived_cl607, plain,
% 3.80/1.19 ( (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero)),
% 3.80/1.19 inference('simplify', [status(thm)], [zip_derived_cl603])).
% 3.80/1.19 thf(zip_derived_cl750, plain,
% 3.80/1.19 (![X0 : $i]:
% 3.80/1.19 (((cardinality_at_time @ first_movers @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 = (zero))
% 3.80/1.19 | (subpopulations @ first_movers @ efficient_producers @ X0 @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (in_environment @ X0 @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (environment @ X0))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl371, zip_derived_cl607])).
% 3.80/1.19 thf(zip_derived_cl751, plain,
% 3.80/1.19 ((~ (environment @ (sk1 @ sk3))
% 3.80/1.19 | (subpopulations @ first_movers @ efficient_producers @
% 3.80/1.19 (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ((cardinality_at_time @ first_movers @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 = (zero)))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl355, zip_derived_cl750])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl752, plain,
% 3.80/1.19 (( (subpopulations @ first_movers @ efficient_producers @ (sk1 @ sk3) @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ((cardinality_at_time @ first_movers @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 = (zero)))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl751, zip_derived_cl65])).
% 3.80/1.19 thf(mp2_favour_members_34, axiom,
% 3.80/1.19 (( ~( environment @ A ) ) | ( ~( subpopulation @ B @ A @ C ) ) |
% 3.80/1.19 ( ~( subpopulation @ D @ A @ C ) ) |
% 3.80/1.19 ( ~( greater @ ( cardinality_at_time @ B @ C ) @ zero ) ) |
% 3.80/1.19 ( ( cardinality_at_time @ D @ C ) != ( zero ) ) |
% 3.80/1.19 ( selection_favors @ B @ D @ C ))).
% 3.80/1.19 thf(zip_derived_cl1, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 3.80/1.19 (~ (environment @ X0)
% 3.80/1.19 | ~ (subpopulation @ X1 @ X0 @ X2)
% 3.80/1.19 | ~ (subpopulation @ X3 @ X0 @ X2)
% 3.80/1.19 | ~ (greater @ (cardinality_at_time @ X1 @ X2) @ zero)
% 3.80/1.19 | ((cardinality_at_time @ X3 @ X2) != (zero))
% 3.80/1.19 | (selection_favors @ X1 @ X3 @ X2))),
% 3.80/1.19 inference('cnf', [status(esa)], [mp2_favour_members_34])).
% 3.80/1.19 thf(zip_derived_cl753, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (((zero) != (zero))
% 3.80/1.19 | (subpopulations @ first_movers @ efficient_producers @
% 3.80/1.19 (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | (selection_favors @ X0 @ first_movers @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (greater @
% 3.80/1.19 (cardinality_at_time @ X0 @ (end_time @ (sk1 @ sk3))) @ zero)
% 3.80/1.19 | ~ (subpopulation @ first_movers @ X1 @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (subpopulation @ X0 @ X1 @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (environment @ X1))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl752, zip_derived_cl1])).
% 3.80/1.19 thf(zip_derived_cl758, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (environment @ X1)
% 3.80/1.19 | ~ (subpopulation @ X0 @ X1 @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (subpopulation @ first_movers @ X1 @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (greater @
% 3.80/1.19 (cardinality_at_time @ X0 @ (end_time @ (sk1 @ sk3))) @ zero)
% 3.80/1.19 | (selection_favors @ X0 @ first_movers @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | (subpopulations @ first_movers @ efficient_producers @
% 3.80/1.19 (sk1 @ sk3) @ (end_time @ (sk1 @ sk3))))),
% 3.80/1.19 inference('simplify', [status(thm)], [zip_derived_cl753])).
% 3.80/1.19 thf(zip_derived_cl895, plain,
% 3.80/1.19 (( (subpopulations @ first_movers @ efficient_producers @ (sk1 @ sk3) @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | (selection_favors @ efficient_producers @ first_movers @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero)
% 3.80/1.19 | ~ (subpopulation @ first_movers @ (sk1 @ sk3) @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (environment @ (sk1 @ sk3)))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl365, zip_derived_cl758])).
% 3.80/1.19 thf(zip_derived_cl607, plain,
% 3.80/1.19 ( (greater @
% 3.80/1.19 (cardinality_at_time @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 zero)),
% 3.80/1.19 inference('simplify', [status(thm)], [zip_derived_cl603])).
% 3.80/1.19 thf(zip_derived_cl355, plain,
% 3.80/1.19 ( (in_environment @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))),
% 3.80/1.19 inference('simplify', [status(thm)], [zip_derived_cl345])).
% 3.80/1.19 thf(mp_subpopulations_46, axiom,
% 3.80/1.19 (( ~( environment @ A ) ) | ( ~( in_environment @ A @ B ) ) |
% 3.80/1.19 ( subpopulation @ first_movers @ A @ B ))).
% 3.80/1.19 thf(zip_derived_cl13, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 (~ (environment @ X0)
% 3.80/1.19 | ~ (in_environment @ X0 @ X1)
% 3.80/1.19 | (subpopulation @ first_movers @ X0 @ X1))),
% 3.80/1.19 inference('cnf', [status(esa)], [mp_subpopulations_46])).
% 3.80/1.19 thf(zip_derived_cl359, plain,
% 3.80/1.19 (( (subpopulation @ first_movers @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (environment @ (sk1 @ sk3)))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl355, zip_derived_cl13])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl364, plain,
% 3.80/1.19 ( (subpopulation @ first_movers @ (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl359, zip_derived_cl65])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl898, plain,
% 3.80/1.19 (( (subpopulations @ first_movers @ efficient_producers @ (sk1 @ sk3) @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | (selection_favors @ efficient_producers @ first_movers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl895, zip_derived_cl607, zip_derived_cl364,
% 3.80/1.19 zip_derived_cl65])).
% 3.80/1.19 thf(mp3_favoured_trategy_37, axiom,
% 3.80/1.19 (( ~( observational_period @ A ) ) |
% 3.80/1.19 ( ~( propagation_strategy @ first_movers ) ) |
% 3.80/1.19 ( ~( propagation_strategy @ efficient_producers ) ) |
% 3.80/1.19 ( ~( selection_favors @
% 3.80/1.19 efficient_producers @ first_movers @ ( end_time @ ( sk1 @ A ) ) ) ) |
% 3.80/1.19 ( selection_favors @ efficient_producers @ first_movers @ A ))).
% 3.80/1.19 thf(zip_derived_cl4, plain,
% 3.80/1.19 (![X0 : $i]:
% 3.80/1.19 (~ (observational_period @ X0)
% 3.80/1.19 | ~ (propagation_strategy @ first_movers)
% 3.80/1.19 | ~ (propagation_strategy @ efficient_producers)
% 3.80/1.19 | ~ (selection_favors @ efficient_producers @ first_movers @
% 3.80/1.19 (end_time @ (sk1 @ X0)))
% 3.80/1.19 | (selection_favors @ efficient_producers @ first_movers @ X0))),
% 3.80/1.19 inference('cnf', [status(esa)], [mp3_favoured_trategy_37])).
% 3.80/1.19 thf(zip_derived_cl7, plain, ( (propagation_strategy @ first_movers)),
% 3.80/1.19 inference('cnf', [status(esa)], [mp_organizational_sets1_40])).
% 3.80/1.19 thf(zip_derived_cl8, plain, ( (propagation_strategy @ efficient_producers)),
% 3.80/1.19 inference('cnf', [status(esa)], [mp_organizational_sets2_41])).
% 3.80/1.19 thf(zip_derived_cl75, plain,
% 3.80/1.19 (![X0 : $i]:
% 3.80/1.19 (~ (observational_period @ X0)
% 3.80/1.19 | ~ (selection_favors @ efficient_producers @ first_movers @
% 3.80/1.19 (end_time @ (sk1 @ X0)))
% 3.80/1.19 | (selection_favors @ efficient_producers @ first_movers @ X0))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl4, zip_derived_cl7, zip_derived_cl8])).
% 3.80/1.19 thf(zip_derived_cl905, plain,
% 3.80/1.19 (( (subpopulations @ first_movers @ efficient_producers @ (sk1 @ sk3) @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | (selection_favors @ efficient_producers @ first_movers @ sk3)
% 3.80/1.19 | ~ (observational_period @ sk3))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl898, zip_derived_cl75])).
% 3.80/1.19 thf(zip_derived_cl27, plain,
% 3.80/1.19 (~ (selection_favors @ efficient_producers @ first_movers @ sk3)),
% 3.80/1.19 inference('cnf', [status(esa)], [zf_stmt_1])).
% 3.80/1.19 thf(zip_derived_cl25, plain, ( (observational_period @ sk3)),
% 3.80/1.19 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.80/1.19 thf(zip_derived_cl906, plain,
% 3.80/1.19 ( (subpopulations @ first_movers @ efficient_producers @ (sk1 @ sk3) @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl905, zip_derived_cl27, zip_derived_cl25])).
% 3.80/1.19 thf(zip_derived_cl235, plain,
% 3.80/1.19 (( (greater @ (end_time @ (sk1 @ sk3)) @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.19 | ((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3)))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl115])).
% 3.80/1.19 thf(d1_56, axiom,
% 3.80/1.19 (( ~( environment @ A ) ) | ( ( B ) != ( critical_point @ A ) ) |
% 3.80/1.19 ( ~( subpopulations @ first_movers @ efficient_producers @ A @ C ) ) |
% 3.80/1.19 ( ~( greater @ C @ B ) ) |
% 3.80/1.19 ( greater @
% 3.80/1.19 ( growth_rate @ efficient_producers @ C ) @
% 3.80/1.19 ( growth_rate @ first_movers @ C ) ))).
% 3.80/1.19 thf(zip_derived_cl23, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.80/1.19 (~ (environment @ X0)
% 3.80/1.19 | ((X1) != (critical_point @ X0))
% 3.80/1.19 | ~ (subpopulations @ first_movers @ efficient_producers @ X0 @ X2)
% 3.80/1.19 | ~ (greater @ X2 @ X1)
% 3.80/1.19 | (greater @ (growth_rate @ efficient_producers @ X2) @
% 3.80/1.19 (growth_rate @ first_movers @ X2)))),
% 3.80/1.19 inference('cnf', [status(esa)], [d1_56])).
% 3.80/1.19 thf(zip_derived_cl220, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 ( (greater @ (growth_rate @ efficient_producers @ X0) @
% 3.80/1.19 (growth_rate @ first_movers @ X0))
% 3.80/1.19 | ~ (greater @ X0 @ (critical_point @ X1))
% 3.80/1.19 | ~ (subpopulations @ first_movers @ efficient_producers @ X1 @ X0)
% 3.80/1.19 | ~ (environment @ X1))),
% 3.80/1.19 inference('eq_res', [status(thm)], [zip_derived_cl23])).
% 3.80/1.19 thf(zip_derived_cl239, plain,
% 3.80/1.19 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.19 | ~ (subpopulations @ first_movers @ efficient_producers @
% 3.80/1.19 (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (growth_rate @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 (growth_rate @ first_movers @ (end_time @ (sk1 @ sk3)))))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl235, zip_derived_cl220])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl240, plain,
% 3.80/1.19 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | ~ (subpopulations @ first_movers @ efficient_producers @
% 3.80/1.19 (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (growth_rate @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 (growth_rate @ first_movers @ (end_time @ (sk1 @ sk3)))))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl239, zip_derived_cl65])).
% 3.80/1.19 thf(zip_derived_cl906, plain,
% 3.80/1.19 ( (subpopulations @ first_movers @ efficient_producers @ (sk1 @ sk3) @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl905, zip_derived_cl27, zip_derived_cl25])).
% 3.80/1.19 thf(zip_derived_cl907, plain,
% 3.80/1.19 ((((end_time @ (sk1 @ sk3)) = (sk2 @ (sk1 @ sk3) @ sk3))
% 3.80/1.19 | (greater @
% 3.80/1.19 (growth_rate @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 (growth_rate @ first_movers @ (end_time @ (sk1 @ sk3)))))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl240, zip_derived_cl906])).
% 3.80/1.19 thf(zip_derived_cl100, plain,
% 3.80/1.19 ( (greater @ (sk2 @ (sk1 @ sk3) @ sk3) @ (critical_point @ (sk1 @ sk3)))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl94, zip_derived_cl65, zip_derived_cl26,
% 3.80/1.19 zip_derived_cl25])).
% 3.80/1.19 thf(zip_derived_cl917, plain,
% 3.80/1.19 (( (greater @ (end_time @ (sk1 @ sk3)) @ (critical_point @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (growth_rate @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 (growth_rate @ first_movers @ (end_time @ (sk1 @ sk3)))))),
% 3.80/1.19 inference('sup+', [status(thm)], [zip_derived_cl907, zip_derived_cl100])).
% 3.80/1.19 thf(zip_derived_cl220, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i]:
% 3.80/1.19 ( (greater @ (growth_rate @ efficient_producers @ X0) @
% 3.80/1.19 (growth_rate @ first_movers @ X0))
% 3.80/1.19 | ~ (greater @ X0 @ (critical_point @ X1))
% 3.80/1.19 | ~ (subpopulations @ first_movers @ efficient_producers @ X1 @ X0)
% 3.80/1.19 | ~ (environment @ X1))),
% 3.80/1.19 inference('eq_res', [status(thm)], [zip_derived_cl23])).
% 3.80/1.19 thf(zip_derived_cl941, plain,
% 3.80/1.19 (( (greater @
% 3.80/1.19 (growth_rate @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 (growth_rate @ first_movers @ (end_time @ (sk1 @ sk3))))
% 3.80/1.19 | ~ (environment @ (sk1 @ sk3))
% 3.80/1.19 | ~ (subpopulations @ first_movers @ efficient_producers @
% 3.80/1.19 (sk1 @ sk3) @ (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | (greater @
% 3.80/1.19 (growth_rate @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 (growth_rate @ first_movers @ (end_time @ (sk1 @ sk3)))))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl917, zip_derived_cl220])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl906, plain,
% 3.80/1.19 ( (subpopulations @ first_movers @ efficient_producers @ (sk1 @ sk3) @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl905, zip_derived_cl27, zip_derived_cl25])).
% 3.80/1.19 thf(zip_derived_cl946, plain,
% 3.80/1.19 (( (greater @
% 3.80/1.19 (growth_rate @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 (growth_rate @ first_movers @ (end_time @ (sk1 @ sk3))))
% 3.80/1.19 | (greater @
% 3.80/1.19 (growth_rate @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 (growth_rate @ first_movers @ (end_time @ (sk1 @ sk3)))))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl941, zip_derived_cl65, zip_derived_cl906])).
% 3.80/1.19 thf(zip_derived_cl947, plain,
% 3.80/1.19 ( (greater @
% 3.80/1.19 (growth_rate @ efficient_producers @ (end_time @ (sk1 @ sk3))) @
% 3.80/1.19 (growth_rate @ first_movers @ (end_time @ (sk1 @ sk3))))),
% 3.80/1.19 inference('simplify', [status(thm)], [zip_derived_cl946])).
% 3.80/1.19 thf(mp1_high_growth_rates_33, axiom,
% 3.80/1.19 (( ~( environment @ A ) ) | ( ~( subpopulations @ B @ C @ A @ D ) ) |
% 3.80/1.19 ( ~( greater @ ( growth_rate @ C @ D ) @ ( growth_rate @ B @ D ) ) ) |
% 3.80/1.19 ( selection_favors @ C @ B @ D ))).
% 3.80/1.19 thf(zip_derived_cl0, plain,
% 3.80/1.19 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 3.80/1.19 (~ (environment @ X0)
% 3.80/1.19 | ~ (subpopulations @ X1 @ X2 @ X0 @ X3)
% 3.80/1.19 | ~ (greater @ (growth_rate @ X2 @ X3) @ (growth_rate @ X1 @ X3))
% 3.80/1.19 | (selection_favors @ X2 @ X1 @ X3))),
% 3.80/1.19 inference('cnf', [status(esa)], [mp1_high_growth_rates_33])).
% 3.80/1.19 thf(zip_derived_cl952, plain,
% 3.80/1.19 (![X0 : $i]:
% 3.80/1.19 ( (selection_favors @ efficient_producers @ first_movers @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (subpopulations @ first_movers @ efficient_producers @ X0 @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))
% 3.80/1.19 | ~ (environment @ X0))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl947, zip_derived_cl0])).
% 3.80/1.19 thf(zip_derived_cl965, plain,
% 3.80/1.19 ((~ (environment @ (sk1 @ sk3))
% 3.80/1.19 | (selection_favors @ efficient_producers @ first_movers @
% 3.80/1.19 (end_time @ (sk1 @ sk3))))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl906, zip_derived_cl952])).
% 3.80/1.19 thf(zip_derived_cl65, plain, ( (environment @ (sk1 @ sk3))),
% 3.80/1.19 inference('clc', [status(thm)], [zip_derived_cl63, zip_derived_cl27])).
% 3.80/1.19 thf(zip_derived_cl966, plain,
% 3.80/1.19 ( (selection_favors @ efficient_producers @ first_movers @
% 3.80/1.19 (end_time @ (sk1 @ sk3)))),
% 3.80/1.19 inference('demod', [status(thm)], [zip_derived_cl965, zip_derived_cl65])).
% 3.80/1.19 thf(zip_derived_cl75, plain,
% 3.80/1.19 (![X0 : $i]:
% 3.80/1.19 (~ (observational_period @ X0)
% 3.80/1.19 | ~ (selection_favors @ efficient_producers @ first_movers @
% 3.80/1.19 (end_time @ (sk1 @ X0)))
% 3.80/1.19 | (selection_favors @ efficient_producers @ first_movers @ X0))),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl4, zip_derived_cl7, zip_derived_cl8])).
% 3.80/1.19 thf(zip_derived_cl967, plain,
% 3.80/1.19 (( (selection_favors @ efficient_producers @ first_movers @ sk3)
% 3.80/1.19 | ~ (observational_period @ sk3))),
% 3.80/1.19 inference('sup-', [status(thm)], [zip_derived_cl966, zip_derived_cl75])).
% 3.80/1.19 thf(zip_derived_cl27, plain,
% 3.80/1.19 (~ (selection_favors @ efficient_producers @ first_movers @ sk3)),
% 3.80/1.19 inference('cnf', [status(esa)], [zf_stmt_1])).
% 3.80/1.19 thf(zip_derived_cl25, plain, ( (observational_period @ sk3)),
% 3.80/1.19 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.80/1.19 thf(zip_derived_cl968, plain, ($false),
% 3.80/1.19 inference('demod', [status(thm)],
% 3.80/1.19 [zip_derived_cl967, zip_derived_cl27, zip_derived_cl25])).
% 3.80/1.19
% 3.80/1.19 % SZS output end Refutation
% 3.80/1.19
% 3.80/1.19
% 3.80/1.19 % Terminating...
% 1.87/1.24 % Runner terminated.
% 1.87/1.26 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------