%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : MGT029+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n011.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:17:22 AM UTC 2026 % Result : Theorem 54.35s 7.84s % Output : Proof 68.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT029+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.36 % Computer : n011.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Mon Sep 7 12:16:00 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.38 OpenJDK 64-Bit Server VM warning: Options -Xverify:none and -noverify were deprecated in JDK 13 and will likely be removed in a future release. % 0.71/0.72 ________ _____ % 0.71/0.72 ___ __ \_________(_)________________________________ % 0.71/0.72 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.71/0.72 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.71/0.72 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.71/0.72 % 0.71/0.72 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.71/0.72 (2023-06-19) % 0.71/0.72 % 0.71/0.72 (c) Philipp Rümmer, 2009-2023 % 0.71/0.72 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.71/0.72 Amanda Stjerna. % 0.71/0.72 Free software under BSD-3-Clause. % 0.71/0.72 % 0.71/0.72 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.71/0.72 % 0.71/0.72 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.71/0.75 Running up to 7 provers in parallel. % 0.71/0.76 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.71/0.76 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.71/0.76 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.71/0.76 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.71/0.76 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.71/0.76 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.71/0.76 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.09/1.35 Prover 4: Preprocessing ... % 3.09/1.35 Prover 1: Preprocessing ... % 3.81/1.42 Prover 3: Preprocessing ... % 3.81/1.42 Prover 6: Preprocessing ... % 3.81/1.42 Prover 5: Preprocessing ... % 3.81/1.43 Prover 0: Preprocessing ... % 3.81/1.43 Prover 2: Preprocessing ... % 6.14/1.73 Prover 1: Constructing countermodel ... % 6.14/1.79 Prover 3: Constructing countermodel ... % 6.92/1.81 Prover 5: Proving ... % 6.92/1.82 Prover 2: Proving ... % 6.92/1.89 Prover 6: Proving ... % 8.82/2.10 Prover 0: Proving ... % 8.82/2.13 Prover 4: Constructing countermodel ... % 13.22/2.67 Prover 3: gave up % 13.22/2.67 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 14.00/2.76 Prover 7: Preprocessing ... % 14.80/2.81 Prover 7: Warning: ignoring some quantifiers % 14.80/2.81 Prover 7: Constructing countermodel ... % 15.64/2.95 Prover 7: gave up % 15.64/2.95 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 15.64/2.98 Prover 8: Preprocessing ... % 16.60/3.08 Prover 8: Warning: ignoring some quantifiers % 16.60/3.08 Prover 8: Constructing countermodel ... % 20.32/3.52 Prover 8: gave up % 20.32/3.52 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 20.32/3.57 Prover 9: Preprocessing ... % 22.77/3.85 Prover 9: Constructing countermodel ... % 29.83/4.76 Prover 1: gave up % 29.83/4.76 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 30.59/4.84 Prover 10: Preprocessing ... % 31.39/4.90 Prover 10: Warning: ignoring some quantifiers % 31.39/4.91 Prover 10: Constructing countermodel ... % 31.39/4.94 Prover 10: gave up % 31.39/4.94 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 31.39/4.98 Prover 11: Preprocessing ... % 33.77/5.27 Prover 11: Constructing countermodel ... % 54.35/7.84 Prover 2: proved (7075ms) % 54.35/7.84 % 54.35/7.84 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 54.35/7.84 % 54.35/7.84 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 54.35/7.84 Prover 9: stopped % 54.35/7.85 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 54.35/7.85 Prover 6: stopped % 54.35/7.85 Prover 0: stopped % 54.35/7.85 Prover 5: stopped % 54.35/7.85 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 54.35/7.87 Prover 13: Preprocessing ... % 54.35/7.89 Prover 13: Warning: ignoring some quantifiers % 54.35/7.89 Prover 13: Constructing countermodel ... % 55.12/7.92 Prover 16: Preprocessing ... % 55.12/7.93 Prover 19: Preprocessing ... % 55.12/8.00 Prover 16: Warning: ignoring some quantifiers % 55.12/8.00 Prover 16: Constructing countermodel ... % 55.12/8.02 Prover 19: Warning: ignoring some quantifiers % 55.12/8.04 Prover 19: Constructing countermodel ... % 59.05/8.48 Prover 19: gave up % 66.19/9.49 Prover 16: Found proof (size 1213) % 66.19/9.49 Prover 16: proved (1646ms) % 66.19/9.49 Prover 13: stopped % 66.89/9.50 Prover 4: stopped % 66.89/9.50 Prover 11: stopped % 66.89/9.50 % 66.89/9.50 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 66.89/9.50 % 66.89/9.55 % SZS output start Proof for theBenchmark % 66.89/9.55 Assumptions after simplification: % 66.89/9.55 --------------------------------- % 66.89/9.55 % 66.89/9.55 (a4) % 66.89/9.60 ! [v0: $i] : ( ~ $i(v0) | ~ stable(v0) | ~ environment(v0) | ? [v1: $i] : % 66.89/9.60 ? [v2: $i] : (equilibrium(v0) = v1 & $i(v2) & $i(v1) & greater_or_equal(v2, % 66.89/9.60 v1) & in_environment(v0, v2))) % 67.31/9.60 % 67.31/9.60 (l1) % 67.31/9.60 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ( ~ $i(v0) | ~ % 67.31/9.60 stable(v0) | ~ environment(v0) | ? [v1: $i] : ($i(v1) & in_environment(v0, % 67.31/9.60 v1) & ! [v2: $i] : ( ~ $i(v2) | ~ subpopulations(first_movers, % 67.31/9.60 efficient_producers, v0, v2) | ~ greater_or_equal(v2, v1) | ? [v3: % 67.31/9.60 $i] : ? [v4: $i] : (growth_rate(efficient_producers, v2) = v3 & % 67.31/9.60 growth_rate(first_movers, v2) = v4 & $i(v4) & $i(v3) & greater(v3, % 67.31/9.60 v4))))) % 67.31/9.60 % 67.31/9.60 (l6) % 67.31/9.61 $i(zero) & $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ! [v1: % 67.31/9.61 $i] : ( ~ $i(v1) | ~ $i(v0) | ~ subpopulations(first_movers, % 67.31/9.61 efficient_producers, v0, v1) | ~ environment(v0) | ? [v2: $i] : ? [v3: % 67.31/9.61 $i] : ? [v4: $i] : ((v4 = zero & v3 = zero & % 67.31/9.61 growth_rate(efficient_producers, v1) = zero & growth_rate(first_movers, % 67.31/9.61 v1) = zero) | (equilibrium(v0) = v2 & $i(v2) & ~ greater_or_equal(v1, % 67.31/9.61 v2)) | (growth_rate(efficient_producers, v1) = v4 & % 67.31/9.61 growth_rate(first_movers, v1) = v3 & $i(v4) & $i(v3) & greater(v4, zero) % 67.31/9.61 & greater(zero, v3)) | (growth_rate(efficient_producers, v1) = v4 & % 67.31/9.61 growth_rate(first_movers, v1) = v3 & $i(v4) & $i(v3) & greater(v3, zero) % 67.31/9.61 & greater(zero, v4)))) % 67.31/9.61 % 67.31/9.61 (mp_greater_or_equal) % 67.31/9.61 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ % 67.31/9.61 greater_or_equal(v0, v1) | greater(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( % 67.31/9.61 ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | greater_or_equal(v0, v1)) & ? % 67.31/9.61 [v0: $i] : ( ~ $i(v0) | greater_or_equal(v0, v0)) % 67.31/9.61 % 67.31/9.61 (mp_greater_transitivity) % 67.31/9.61 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.31/9.61 ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 67.31/9.61 % 67.31/9.61 (mp_times_in_environment) % 67.31/9.62 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ $i(v2) | ~ $i(v1) | % 67.31/9.62 ~ $i(v0) | ~ in_environment(v0, v2) | ~ in_environment(v0, v1) | % 67.31/9.62 greater(v2, v1) | greater(v1, v2)) % 67.31/9.62 % 67.31/9.62 (prove_l11) % 67.31/9.62 $i(zero) & $i(efficient_producers) & $i(first_movers) & ? [v0: $i] : ($i(v0) % 67.31/9.62 & stable(v0) & environment(v0) & ! [v1: $i] : ( ~ $i(v1) | ~ % 67.31/9.62 in_environment(v0, v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ($i(v2) % 67.31/9.62 & subpopulations(first_movers, efficient_producers, v0, v2) & % 67.31/9.62 greater_or_equal(v2, v1) & ((growth_rate(efficient_producers, v2) = v3 & % 67.31/9.62 $i(v3) & ~ greater(v3, zero)) | (growth_rate(first_movers, v2) = v4 % 67.31/9.62 & $i(v4) & ~ greater(zero, v4)))))) % 67.31/9.62 % 67.31/9.62 (function-axioms) % 67.31/9.62 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 67.31/9.62 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) & ! [v0: $i] : % 67.31/9.62 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) = v1) | ~ % 67.31/9.62 (equilibrium(v2) = v0)) % 67.31/9.62 % 67.31/9.62 Those formulas are unsatisfiable: % 67.31/9.62 --------------------------------- % 67.31/9.62 % 67.31/9.62 Begin of proof % 67.31/9.62 | % 67.31/9.62 | ALPHA: (mp_greater_or_equal) implies: % 67.31/9.63 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) % 67.31/9.63 | | greater_or_equal(v0, v1)) % 67.31/9.63 | (2) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ % 67.31/9.63 | greater_or_equal(v0, v1) | greater(v0, v1)) % 67.31/9.63 | % 67.31/9.63 | ALPHA: (l6) implies: % 67.31/9.63 | (3) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 67.31/9.63 | subpopulations(first_movers, efficient_producers, v0, v1) | ~ % 67.31/9.63 | environment(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ((v4 = % 67.31/9.63 | zero & v3 = zero & growth_rate(efficient_producers, v1) = zero & % 67.31/9.63 | growth_rate(first_movers, v1) = zero) | (equilibrium(v0) = v2 & % 67.31/9.63 | $i(v2) & ~ greater_or_equal(v1, v2)) | % 67.31/9.63 | (growth_rate(efficient_producers, v1) = v4 & % 67.31/9.63 | growth_rate(first_movers, v1) = v3 & $i(v4) & $i(v3) & % 67.31/9.63 | greater(v4, zero) & greater(zero, v3)) | % 67.31/9.63 | (growth_rate(efficient_producers, v1) = v4 & % 67.31/9.63 | growth_rate(first_movers, v1) = v3 & $i(v4) & $i(v3) & % 67.31/9.63 | greater(v3, zero) & greater(zero, v4)))) % 67.31/9.63 | % 67.31/9.63 | ALPHA: (l1) implies: % 67.31/9.63 | (4) ! [v0: $i] : ( ~ $i(v0) | ~ stable(v0) | ~ environment(v0) | ? [v1: % 67.31/9.63 | $i] : ($i(v1) & in_environment(v0, v1) & ! [v2: $i] : ( ~ $i(v2) | % 67.31/9.63 | ~ subpopulations(first_movers, efficient_producers, v0, v2) | ~ % 67.31/9.63 | greater_or_equal(v2, v1) | ? [v3: $i] : ? [v4: $i] : % 67.31/9.63 | (growth_rate(efficient_producers, v2) = v3 & % 67.31/9.63 | growth_rate(first_movers, v2) = v4 & $i(v4) & $i(v3) & % 67.31/9.63 | greater(v3, v4))))) % 67.31/9.63 | % 67.31/9.63 | ALPHA: (prove_l11) implies: % 67.31/9.63 | (5) $i(zero) % 67.31/9.64 | (6) ? [v0: $i] : ($i(v0) & stable(v0) & environment(v0) & ! [v1: $i] : ( % 67.31/9.64 | ~ $i(v1) | ~ in_environment(v0, v1) | ? [v2: $i] : ? [v3: $i] : % 67.31/9.64 | ? [v4: $i] : ($i(v2) & subpopulations(first_movers, % 67.31/9.64 | efficient_producers, v0, v2) & greater_or_equal(v2, v1) & % 67.31/9.64 | ((growth_rate(efficient_producers, v2) = v3 & $i(v3) & ~ % 67.31/9.64 | greater(v3, zero)) | (growth_rate(first_movers, v2) = v4 & % 67.31/9.64 | $i(v4) & ~ greater(zero, v4)))))) % 67.31/9.64 | % 67.31/9.64 | ALPHA: (function-axioms) implies: % 67.31/9.64 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 67.31/9.64 | (equilibrium(v2) = v1) | ~ (equilibrium(v2) = v0)) % 67.31/9.64 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 67.31/9.64 | (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 67.31/9.64 | % 67.31/9.64 | DELTA: instantiating (6) with fresh symbol all_11_0 gives: % 67.31/9.64 | (9) $i(all_11_0) & stable(all_11_0) & environment(all_11_0) & ! [v0: $i] : % 67.31/9.64 | ( ~ $i(v0) | ~ in_environment(all_11_0, v0) | ? [v1: $i] : ? [v2: % 67.31/9.64 | $i] : ? [v3: $i] : ($i(v1) & subpopulations(first_movers, % 67.31/9.64 | efficient_producers, all_11_0, v1) & greater_or_equal(v1, v0) & % 67.31/9.64 | ((growth_rate(efficient_producers, v1) = v2 & $i(v2) & ~ % 67.31/9.64 | greater(v2, zero)) | (growth_rate(first_movers, v1) = v3 & % 67.31/9.64 | $i(v3) & ~ greater(zero, v3))))) % 67.31/9.64 | % 67.31/9.64 | ALPHA: (9) implies: % 67.31/9.64 | (10) environment(all_11_0) % 67.31/9.64 | (11) stable(all_11_0) % 67.31/9.64 | (12) $i(all_11_0) % 67.31/9.65 | (13) ! [v0: $i] : ( ~ $i(v0) | ~ in_environment(all_11_0, v0) | ? [v1: % 67.31/9.65 | $i] : ? [v2: $i] : ? [v3: $i] : ($i(v1) & % 67.31/9.65 | subpopulations(first_movers, efficient_producers, all_11_0, v1) & % 67.31/9.65 | greater_or_equal(v1, v0) & ((growth_rate(efficient_producers, v1) % 67.31/9.65 | = v2 & $i(v2) & ~ greater(v2, zero)) | % 67.31/9.65 | (growth_rate(first_movers, v1) = v3 & $i(v3) & ~ greater(zero, % 67.31/9.65 | v3))))) % 67.31/9.65 | % 67.31/9.65 | GROUND_INST: instantiating (a4) with all_11_0, simplifying with (10), (11), % 67.31/9.65 | (12) gives: % 67.31/9.65 | (14) ? [v0: $i] : ? [v1: $i] : (equilibrium(all_11_0) = v0 & $i(v1) & % 67.31/9.65 | $i(v0) & greater_or_equal(v1, v0) & in_environment(all_11_0, v1)) % 67.31/9.65 | % 67.31/9.65 | GROUND_INST: instantiating (4) with all_11_0, simplifying with (10), (11), % 67.31/9.65 | (12) gives: % 67.31/9.65 | (15) ? [v0: $i] : ($i(v0) & in_environment(all_11_0, v0) & ! [v1: $i] : ( % 67.31/9.65 | ~ $i(v1) | ~ subpopulations(first_movers, efficient_producers, % 67.31/9.65 | all_11_0, v1) | ~ greater_or_equal(v1, v0) | ? [v2: $i] : ? % 67.31/9.65 | [v3: $i] : (growth_rate(efficient_producers, v1) = v2 & % 67.31/9.65 | growth_rate(first_movers, v1) = v3 & $i(v3) & $i(v2) & % 67.31/9.65 | greater(v2, v3)))) % 67.31/9.65 | % 67.31/9.65 | DELTA: instantiating (14) with fresh symbols all_19_0, all_19_1 gives: % 67.31/9.65 | (16) equilibrium(all_11_0) = all_19_1 & $i(all_19_0) & $i(all_19_1) & % 67.31/9.65 | greater_or_equal(all_19_0, all_19_1) & in_environment(all_11_0, % 67.31/9.65 | all_19_0) % 67.31/9.65 | % 67.31/9.65 | ALPHA: (16) implies: % 67.31/9.65 | (17) in_environment(all_11_0, all_19_0) % 67.31/9.65 | (18) greater_or_equal(all_19_0, all_19_1) % 67.31/9.65 | (19) $i(all_19_1) % 67.31/9.66 | (20) $i(all_19_0) % 67.31/9.66 | (21) equilibrium(all_11_0) = all_19_1 % 67.31/9.66 | % 67.31/9.66 | DELTA: instantiating (15) with fresh symbol all_21_0 gives: % 67.31/9.66 | (22) $i(all_21_0) & in_environment(all_11_0, all_21_0) & ! [v0: $i] : ( ~ % 67.31/9.66 | $i(v0) | ~ subpopulations(first_movers, efficient_producers, % 67.31/9.66 | all_11_0, v0) | ~ greater_or_equal(v0, all_21_0) | ? [v1: $i] : % 67.31/9.66 | ? [v2: $i] : (growth_rate(efficient_producers, v0) = v1 & % 67.31/9.66 | growth_rate(first_movers, v0) = v2 & $i(v2) & $i(v1) & greater(v1, % 67.31/9.66 | v2))) % 67.31/9.66 | % 67.31/9.66 | ALPHA: (22) implies: % 67.31/9.66 | (23) in_environment(all_11_0, all_21_0) % 67.31/9.66 | (24) $i(all_21_0) % 67.31/9.66 | (25) ! [v0: $i] : ( ~ $i(v0) | ~ subpopulations(first_movers, % 67.31/9.66 | efficient_producers, all_11_0, v0) | ~ greater_or_equal(v0, % 67.31/9.66 | all_21_0) | ? [v1: $i] : ? [v2: $i] : % 67.31/9.66 | (growth_rate(efficient_producers, v0) = v1 & % 67.31/9.66 | growth_rate(first_movers, v0) = v2 & $i(v2) & $i(v1) & greater(v1, % 67.31/9.66 | v2))) % 67.31/9.66 | % 67.31/9.66 | GROUND_INST: instantiating (13) with all_19_0, simplifying with (17), (20) % 67.31/9.66 | gives: % 67.31/9.66 | (26) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v0) & % 67.31/9.66 | subpopulations(first_movers, efficient_producers, all_11_0, v0) & % 67.31/9.66 | greater_or_equal(v0, all_19_0) & ((growth_rate(efficient_producers, % 67.31/9.66 | v0) = v1 & $i(v1) & ~ greater(v1, zero)) | % 67.31/9.66 | (growth_rate(first_movers, v0) = v2 & $i(v2) & ~ greater(zero, % 67.31/9.66 | v2)))) % 67.31/9.66 | % 67.31/9.66 | GROUND_INST: instantiating (mp_times_in_environment) with all_11_0, all_19_0, % 67.31/9.66 | all_21_0, simplifying with (12), (17), (20), (23), (24) gives: % 67.31/9.67 | (27) all_21_0 = all_19_0 | greater(all_21_0, all_19_0) | greater(all_19_0, % 67.31/9.67 | all_21_0) % 67.31/9.67 | % 67.31/9.67 | GROUND_INST: instantiating (13) with all_21_0, simplifying with (23), (24) % 67.31/9.67 | gives: % 67.31/9.67 | (28) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ($i(v0) & % 67.31/9.67 | subpopulations(first_movers, efficient_producers, all_11_0, v0) & % 67.31/9.67 | greater_or_equal(v0, all_21_0) & ((growth_rate(efficient_producers, % 67.31/9.67 | v0) = v1 & $i(v1) & ~ greater(v1, zero)) | % 67.31/9.67 | (growth_rate(first_movers, v0) = v2 & $i(v2) & ~ greater(zero, % 67.31/9.67 | v2)))) % 67.31/9.67 | % 67.31/9.67 | GROUND_INST: instantiating (2) with all_19_0, all_19_1, simplifying with (18), % 67.31/9.67 | (19), (20) gives: % 67.31/9.67 | (29) all_19_0 = all_19_1 | greater(all_19_0, all_19_1) % 67.31/9.67 | % 67.31/9.67 | DELTA: instantiating (28) with fresh symbols all_29_0, all_29_1, all_29_2 % 67.31/9.67 | gives: % 67.31/9.67 | (30) $i(all_29_2) & subpopulations(first_movers, efficient_producers, % 67.31/9.67 | all_11_0, all_29_2) & greater_or_equal(all_29_2, all_21_0) & % 67.31/9.67 | ((growth_rate(efficient_producers, all_29_2) = all_29_1 & $i(all_29_1) % 67.31/9.67 | & ~ greater(all_29_1, zero)) | (growth_rate(first_movers, % 67.31/9.67 | all_29_2) = all_29_0 & $i(all_29_0) & ~ greater(zero, % 67.31/9.67 | all_29_0))) % 67.31/9.67 | % 67.31/9.67 | ALPHA: (30) implies: % 67.31/9.67 | (31) greater_or_equal(all_29_2, all_21_0) % 67.31/9.67 | (32) subpopulations(first_movers, efficient_producers, all_11_0, all_29_2) % 67.31/9.67 | (33) $i(all_29_2) % 67.31/9.67 | (34) (growth_rate(efficient_producers, all_29_2) = all_29_1 & $i(all_29_1) % 67.31/9.67 | & ~ greater(all_29_1, zero)) | (growth_rate(first_movers, all_29_2) % 67.31/9.67 | = all_29_0 & $i(all_29_0) & ~ greater(zero, all_29_0)) % 67.31/9.67 | % 67.31/9.67 | DELTA: instantiating (26) with fresh symbols all_31_0, all_31_1, all_31_2 % 67.31/9.67 | gives: % 67.31/9.67 | (35) $i(all_31_2) & subpopulations(first_movers, efficient_producers, % 67.31/9.67 | all_11_0, all_31_2) & greater_or_equal(all_31_2, all_19_0) & % 67.31/9.67 | ((growth_rate(efficient_producers, all_31_2) = all_31_1 & $i(all_31_1) % 67.31/9.67 | & ~ greater(all_31_1, zero)) | (growth_rate(first_movers, % 67.31/9.67 | all_31_2) = all_31_0 & $i(all_31_0) & ~ greater(zero, % 67.31/9.67 | all_31_0))) % 67.31/9.67 | % 67.31/9.67 | ALPHA: (35) implies: % 67.31/9.67 | (36) greater_or_equal(all_31_2, all_19_0) % 67.31/9.67 | (37) subpopulations(first_movers, efficient_producers, all_11_0, all_31_2) % 67.31/9.67 | (38) $i(all_31_2) % 67.31/9.68 | (39) (growth_rate(efficient_producers, all_31_2) = all_31_1 & $i(all_31_1) % 67.31/9.68 | & ~ greater(all_31_1, zero)) | (growth_rate(first_movers, all_31_2) % 67.31/9.68 | = all_31_0 & $i(all_31_0) & ~ greater(zero, all_31_0)) % 67.31/9.68 | % 67.31/9.68 | GROUND_INST: instantiating (2) with all_29_2, all_21_0, simplifying with (24), % 67.31/9.68 | (31), (33) gives: % 67.31/9.68 | (40) all_29_2 = all_21_0 | greater(all_29_2, all_21_0) % 67.31/9.68 | % 67.31/9.68 | GROUND_INST: instantiating (2) with all_31_2, all_19_0, simplifying with (20), % 67.31/9.68 | (36), (38) gives: % 67.31/9.68 | (41) all_31_2 = all_19_0 | greater(all_31_2, all_19_0) % 67.31/9.68 | % 67.31/9.68 | GROUND_INST: instantiating (3) with all_11_0, all_29_2, simplifying with (10), % 67.31/9.68 | (12), (32), (33) gives: % 67.31/9.68 | (42) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ((v2 = zero & v1 = zero & % 67.31/9.68 | growth_rate(efficient_producers, all_29_2) = zero & % 67.31/9.68 | growth_rate(first_movers, all_29_2) = zero) | % 67.31/9.68 | (equilibrium(all_11_0) = v0 & $i(v0) & ~ greater_or_equal(all_29_2, % 67.31/9.68 | v0)) | (growth_rate(efficient_producers, all_29_2) = v2 & % 67.31/9.68 | growth_rate(first_movers, all_29_2) = v1 & $i(v2) & $i(v1) & % 67.31/9.68 | greater(v2, zero) & greater(zero, v1)) | % 67.31/9.68 | (growth_rate(efficient_producers, all_29_2) = v2 & % 67.31/9.68 | growth_rate(first_movers, all_29_2) = v1 & $i(v2) & $i(v1) & % 67.31/9.68 | greater(v1, zero) & greater(zero, v2))) % 67.31/9.68 | % 67.31/9.68 | GROUND_INST: instantiating (25) with all_29_2, simplifying with (31), (32), % 67.31/9.68 | (33) gives: % 67.31/9.68 | (43) ? [v0: $i] : ? [v1: $i] : (growth_rate(efficient_producers, % 67.31/9.68 | all_29_2) = v0 & growth_rate(first_movers, all_29_2) = v1 & $i(v1) % 67.31/9.68 | & $i(v0) & greater(v0, v1)) % 67.31/9.68 | % 67.31/9.68 | GROUND_INST: instantiating (3) with all_11_0, all_31_2, simplifying with (10), % 67.31/9.68 | (12), (37), (38) gives: % 67.31/9.69 | (44) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ((v2 = zero & v1 = zero & % 67.31/9.69 | growth_rate(efficient_producers, all_31_2) = zero & % 67.31/9.69 | growth_rate(first_movers, all_31_2) = zero) | % 67.31/9.69 | (equilibrium(all_11_0) = v0 & $i(v0) & ~ greater_or_equal(all_31_2, % 67.31/9.69 | v0)) | (growth_rate(efficient_producers, all_31_2) = v2 & % 67.31/9.69 | growth_rate(first_movers, all_31_2) = v1 & $i(v2) & $i(v1) & % 67.31/9.69 | greater(v2, zero) & greater(zero, v1)) | % 67.31/9.69 | (growth_rate(efficient_producers, all_31_2) = v2 & % 67.31/9.69 | growth_rate(first_movers, all_31_2) = v1 & $i(v2) & $i(v1) & % 67.31/9.69 | greater(v1, zero) & greater(zero, v2))) % 67.31/9.69 | % 67.31/9.69 | GROUND_INST: instantiating (25) with all_31_2, simplifying with (37), (38) % 67.31/9.69 | gives: % 67.31/9.69 | (45) ~ greater_or_equal(all_31_2, all_21_0) | ? [v0: $i] : ? [v1: $i] : % 67.31/9.69 | (growth_rate(efficient_producers, all_31_2) = v0 & % 67.31/9.69 | growth_rate(first_movers, all_31_2) = v1 & $i(v1) & $i(v0) & % 67.31/9.69 | greater(v0, v1)) % 67.31/9.69 | % 67.31/9.69 | DELTA: instantiating (43) with fresh symbols all_38_0, all_38_1 gives: % 67.31/9.69 | (46) growth_rate(efficient_producers, all_29_2) = all_38_1 & % 67.31/9.69 | growth_rate(first_movers, all_29_2) = all_38_0 & $i(all_38_0) & % 67.31/9.69 | $i(all_38_1) & greater(all_38_1, all_38_0) % 67.31/9.69 | % 67.31/9.69 | ALPHA: (46) implies: % 67.31/9.69 | (47) greater(all_38_1, all_38_0) % 67.31/9.69 | (48) growth_rate(first_movers, all_29_2) = all_38_0 % 67.31/9.69 | (49) growth_rate(efficient_producers, all_29_2) = all_38_1 % 67.31/9.69 | % 67.31/9.69 | DELTA: instantiating (44) with fresh symbols all_40_0, all_40_1, all_40_2 % 67.31/9.69 | gives: % 67.31/9.69 | (50) (all_40_0 = zero & all_40_1 = zero & growth_rate(efficient_producers, % 67.31/9.69 | all_31_2) = zero & growth_rate(first_movers, all_31_2) = zero) | % 67.31/9.69 | (equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 67.31/9.69 | greater_or_equal(all_31_2, all_40_2)) | % 67.31/9.69 | (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 67.31/9.69 | growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 67.31/9.69 | $i(all_40_1) & greater(all_40_0, zero) & greater(zero, all_40_1)) | % 67.31/9.69 | (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 67.31/9.69 | growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 67.31/9.69 | $i(all_40_1) & greater(all_40_1, zero) & greater(zero, all_40_0)) % 67.31/9.69 | % 67.31/9.69 | DELTA: instantiating (42) with fresh symbols all_41_0, all_41_1, all_41_2 % 67.31/9.69 | gives: % 67.31/9.69 | (51) (all_41_0 = zero & all_41_1 = zero & growth_rate(efficient_producers, % 67.31/9.69 | all_29_2) = zero & growth_rate(first_movers, all_29_2) = zero) | % 67.31/9.69 | (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 67.31/9.69 | greater_or_equal(all_29_2, all_41_2)) | % 67.31/9.69 | (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 67.31/9.69 | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 67.31/9.69 | $i(all_41_1) & greater(all_41_0, zero) & greater(zero, all_41_1)) | % 67.31/9.69 | (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 67.31/9.69 | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 67.31/9.69 | $i(all_41_1) & greater(all_41_1, zero) & greater(zero, all_41_0)) % 67.31/9.69 | % 67.31/9.69 | GROUND_INST: instantiating (8) with all_38_0, all_38_1, all_29_2, % 67.31/9.69 | first_movers, simplifying with (48) gives: % 67.31/9.69 | (52) all_38_0 = all_38_1 | ~ (growth_rate(first_movers, all_29_2) = % 67.31/9.69 | all_38_1) % 67.31/9.69 | % 67.31/9.69 | BETA: splitting (34) gives: % 67.31/9.69 | % 67.31/9.69 | Case 1: % 67.31/9.69 | | % 67.31/9.69 | | (53) growth_rate(efficient_producers, all_29_2) = all_29_1 & $i(all_29_1) % 67.31/9.69 | | & ~ greater(all_29_1, zero) % 67.31/9.70 | | % 67.31/9.70 | | ALPHA: (53) implies: % 67.31/9.70 | | (54) ~ greater(all_29_1, zero) % 67.31/9.70 | | (55) growth_rate(efficient_producers, all_29_2) = all_29_1 % 67.31/9.70 | | % 67.31/9.70 | | GROUND_INST: instantiating (8) with all_38_1, all_29_1, all_29_2, % 67.31/9.70 | | efficient_producers, simplifying with (49), (55) gives: % 67.79/9.70 | | (56) all_38_1 = all_29_1 % 67.79/9.70 | | % 67.79/9.70 | | REDUCE: (47), (56) imply: % 67.79/9.70 | | (57) greater(all_29_1, all_38_0) % 67.79/9.70 | | % 67.79/9.70 | | PRED_UNIFY: (54), (57) imply: % 67.79/9.70 | | (58) ~ (all_38_0 = zero) % 67.79/9.70 | | % 67.79/9.70 | | BETA: splitting (29) gives: % 67.79/9.70 | | % 67.79/9.70 | | Case 1: % 67.79/9.70 | | | % 67.79/9.70 | | | (59) greater(all_19_0, all_19_1) % 67.79/9.70 | | | % 67.79/9.70 | | | BETA: splitting (27) gives: % 67.79/9.70 | | | % 67.79/9.70 | | | Case 1: % 67.79/9.70 | | | | % 67.79/9.70 | | | | (60) greater(all_21_0, all_19_0) % 67.79/9.70 | | | | % 67.79/9.70 | | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_21_0, % 67.79/9.70 | | | | all_19_0, all_19_1, simplifying with (19), (20), (24), % 67.79/9.70 | | | | (59), (60) gives: % 67.79/9.70 | | | | (61) greater(all_21_0, all_19_1) % 67.79/9.70 | | | | % 67.79/9.70 | | | | REF_CLOSE: (1), (5), (7), (8), (19), (21), (24), (33), (40), (48), (51), % 67.79/9.70 | | | | (52), (54), (55), (56), (57), (58), (61), % 67.79/9.70 | | | | (mp_greater_transitivity) are inconsistent by sub-proof #15. % 67.79/9.70 | | | | % 67.79/9.70 | | | Case 2: % 67.79/9.70 | | | | % 67.79/9.70 | | | | (62) ~ greater(all_21_0, all_19_0) % 67.79/9.70 | | | | (63) all_21_0 = all_19_0 | greater(all_19_0, all_21_0) % 67.79/9.70 | | | | % 67.79/9.70 | | | | BETA: splitting (39) gives: % 67.79/9.70 | | | | % 67.79/9.70 | | | | Case 1: % 67.79/9.70 | | | | | % 67.79/9.70 | | | | | (64) growth_rate(efficient_producers, all_31_2) = all_31_1 & % 67.79/9.70 | | | | | $i(all_31_1) & ~ greater(all_31_1, zero) % 67.79/9.70 | | | | | % 67.79/9.70 | | | | | ALPHA: (64) implies: % 67.79/9.70 | | | | | (65) ~ greater(all_31_1, zero) % 67.79/9.70 | | | | | (66) growth_rate(efficient_producers, all_31_2) = all_31_1 % 67.79/9.70 | | | | | % 67.79/9.70 | | | | | BETA: splitting (45) gives: % 67.79/9.70 | | | | | % 67.79/9.70 | | | | | Case 1: % 67.79/9.70 | | | | | | % 67.79/9.70 | | | | | | (67) ~ greater_or_equal(all_31_2, all_21_0) % 67.79/9.70 | | | | | | % 67.79/9.70 | | | | | | PRED_UNIFY: (36), (67) imply: % 67.79/9.70 | | | | | | (68) ~ (all_21_0 = all_19_0) % 67.79/9.70 | | | | | | % 67.79/9.71 | | | | | | REF_CLOSE: (1), (20), (24), (38), (41), (63), (67), (68), % 67.79/9.71 | | | | | | (mp_greater_transitivity) are inconsistent by sub-proof % 67.79/9.71 | | | | | | #14. % 67.79/9.71 | | | | | | % 67.79/9.71 | | | | | Case 2: % 67.79/9.71 | | | | | | % 67.79/9.71 | | | | | | (69) greater_or_equal(all_31_2, all_21_0) % 67.79/9.71 | | | | | | (70) ? [v0: $i] : ? [v1: $i] : % 67.79/9.71 | | | | | | (growth_rate(efficient_producers, all_31_2) = v0 & % 67.79/9.71 | | | | | | growth_rate(first_movers, all_31_2) = v1 & $i(v1) & $i(v0) % 67.79/9.71 | | | | | | & greater(v0, v1)) % 67.79/9.71 | | | | | | % 67.79/9.71 | | | | | | DELTA: instantiating (70) with fresh symbols all_106_0, all_106_1 % 67.79/9.71 | | | | | | gives: % 67.79/9.71 | | | | | | (71) growth_rate(efficient_producers, all_31_2) = all_106_1 & % 67.79/9.71 | | | | | | growth_rate(first_movers, all_31_2) = all_106_0 & % 67.79/9.71 | | | | | | $i(all_106_0) & $i(all_106_1) & greater(all_106_1, % 67.79/9.71 | | | | | | all_106_0) % 67.79/9.71 | | | | | | % 67.79/9.71 | | | | | | ALPHA: (71) implies: % 67.79/9.71 | | | | | | (72) greater(all_106_1, all_106_0) % 67.79/9.71 | | | | | | (73) $i(all_106_0) % 67.79/9.71 | | | | | | (74) growth_rate(first_movers, all_31_2) = all_106_0 % 67.79/9.71 | | | | | | (75) growth_rate(efficient_producers, all_31_2) = all_106_1 % 67.79/9.71 | | | | | | % 67.79/9.71 | | | | | | GROUND_INST: instantiating (8) with all_31_1, all_106_1, all_31_2, % 67.79/9.71 | | | | | | efficient_producers, simplifying with (66), (75) gives: % 67.79/9.71 | | | | | | (76) all_106_1 = all_31_1 % 67.79/9.71 | | | | | | % 67.79/9.71 | | | | | | REDUCE: (72), (76) imply: % 67.79/9.71 | | | | | | (77) greater(all_31_1, all_106_0) % 67.79/9.71 | | | | | | % 67.79/9.71 | | | | | | PRED_UNIFY: (65), (77) imply: % 67.79/9.71 | | | | | | (78) ~ (all_106_0 = zero) % 67.79/9.71 | | | | | | % 67.79/9.71 | | | | | | GROUND_INST: instantiating (2) with all_31_2, all_21_0, simplifying % 67.79/9.71 | | | | | | with (24), (38), (69) gives: % 67.79/9.71 | | | | | | (79) all_31_2 = all_21_0 | greater(all_31_2, all_21_0) % 67.79/9.71 | | | | | | % 67.79/9.71 | | | | | | BETA: splitting (41) gives: % 67.79/9.71 | | | | | | % 67.79/9.71 | | | | | | Case 1: % 67.79/9.71 | | | | | | | % 67.79/9.71 | | | | | | | (80) greater(all_31_2, all_19_0) % 67.79/9.71 | | | | | | | % 67.79/9.71 | | | | | | | PRED_UNIFY: (62), (80) imply: % 67.79/9.71 | | | | | | | (81) ~ (all_31_2 = all_21_0) % 67.79/9.71 | | | | | | | % 67.79/9.71 | | | | | | | BETA: splitting (79) gives: % 67.79/9.71 | | | | | | | % 67.79/9.71 | | | | | | | Case 1: % 67.79/9.71 | | | | | | | | % 67.79/9.71 | | | | | | | | % 67.79/9.71 | | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with % 67.79/9.71 | | | | | | | | all_31_2, all_19_0, all_19_1, simplifying with % 67.79/9.71 | | | | | | | | (19), (20), (38), (59), (80) gives: % 67.79/9.71 | | | | | | | | (82) greater(all_31_2, all_19_1) % 67.79/9.71 | | | | | | | | % 67.79/9.71 | | | | | | | | BETA: splitting (52) gives: % 67.79/9.71 | | | | | | | | % 67.79/9.71 | | | | | | | | Case 1: % 67.79/9.71 | | | | | | | | | % 67.79/9.71 | | | | | | | | | % 67.79/9.71 | | | | | | | | | GROUND_INST: instantiating (1) with all_31_2, all_19_1, % 67.79/9.71 | | | | | | | | | simplifying with (19), (38), (82) gives: % 67.79/9.71 | | | | | | | | | (83) greater_or_equal(all_31_2, all_19_1) % 67.79/9.71 | | | | | | | | | % 67.79/9.71 | | | | | | | | | DELTA: instantiating (70) with fresh symbols all_106_0, % 67.79/9.71 | | | | | | | | | all_106_1 gives: % 67.79/9.71 | | | | | | | | | (84) growth_rate(efficient_producers, all_31_2) = all_106_1 % 67.79/9.71 | | | | | | | | | & growth_rate(first_movers, all_31_2) = all_106_0 & % 67.79/9.71 | | | | | | | | | $i(all_106_0) & $i(all_106_1) & greater(all_106_1, % 67.79/9.71 | | | | | | | | | all_106_0) % 67.79/9.71 | | | | | | | | | % 67.79/9.71 | | | | | | | | | REF_CLOSE: (5), (7), (8), (21), (50), (65), (66), (83), (84), % 67.79/9.71 | | | | | | | | | (mp_greater_transitivity) are inconsistent by % 67.79/9.71 | | | | | | | | | sub-proof #11. % 67.79/9.71 | | | | | | | | | % 67.79/9.72 | | | | | | | | Case 2: % 67.79/9.72 | | | | | | | | | % 67.79/9.72 | | | | | | | | | (85) all_38_0 = all_38_1 % 67.79/9.72 | | | | | | | | | % 67.79/9.72 | | | | | | | | | COMBINE_EQS: (56), (85) imply: % 67.79/9.72 | | | | | | | | | (86) all_38_0 = all_29_1 % 67.79/9.72 | | | | | | | | | % 67.79/9.72 | | | | | | | | | REDUCE: (58), (86) imply: % 67.79/9.72 | | | | | | | | | (87) ~ (all_29_1 = zero) % 67.79/9.72 | | | | | | | | | % 67.79/9.72 | | | | | | | | | BETA: splitting (51) gives: % 67.79/9.72 | | | | | | | | | % 67.79/9.72 | | | | | | | | | Case 1: % 67.79/9.72 | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | (88) (all_41_0 = zero & all_41_1 = zero & % 67.79/9.72 | | | | | | | | | | growth_rate(efficient_producers, all_29_2) = zero % 67.79/9.72 | | | | | | | | | | & growth_rate(first_movers, all_29_2) = zero) | % 67.79/9.72 | | | | | | | | | | (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & % 67.79/9.72 | | | | | | | | | | ~ greater_or_equal(all_29_2, all_41_2)) % 67.79/9.72 | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | BETA: splitting (88) gives: % 67.79/9.72 | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | Case 1: % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | (89) all_41_0 = zero & all_41_1 = zero & % 67.79/9.72 | | | | | | | | | | | growth_rate(efficient_producers, all_29_2) = zero % 67.79/9.72 | | | | | | | | | | | & growth_rate(first_movers, all_29_2) = zero % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | ALPHA: (89) implies: % 67.79/9.72 | | | | | | | | | | | (90) growth_rate(efficient_producers, all_29_2) = zero % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | REF_CLOSE: (8), (55), (87), (90) are inconsistent by % 67.79/9.72 | | | | | | | | | | | sub-proof #10. % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | Case 2: % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | (91) equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & % 67.79/9.72 | | | | | | | | | | | ~ greater_or_equal(all_29_2, all_41_2) % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | ALPHA: (91) implies: % 67.79/9.72 | | | | | | | | | | | (92) $i(all_41_2) % 67.79/9.72 | | | | | | | | | | | (93) equilibrium(all_11_0) = all_41_2 % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | GROUND_INST: instantiating (7) with all_19_1, all_41_2, % 67.79/9.72 | | | | | | | | | | | all_11_0, simplifying with (21), (93) gives: % 67.79/9.72 | | | | | | | | | | | (94) all_41_2 = all_19_1 % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | GROUND_INST: instantiating (1) with all_31_2, all_19_1, % 67.79/9.72 | | | | | | | | | | | simplifying with (19), (38), (82) gives: % 67.79/9.72 | | | | | | | | | | | (95) greater_or_equal(all_31_2, all_19_1) % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | DELTA: instantiating (70) with fresh symbols all_106_0, % 67.79/9.72 | | | | | | | | | | | all_106_1 gives: % 67.79/9.72 | | | | | | | | | | | (96) growth_rate(efficient_producers, all_31_2) = % 67.79/9.72 | | | | | | | | | | | all_106_1 & growth_rate(first_movers, all_31_2) = % 67.79/9.72 | | | | | | | | | | | all_106_0 & $i(all_106_0) & $i(all_106_1) & % 67.79/9.72 | | | | | | | | | | | greater(all_106_1, all_106_0) % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | REF_CLOSE: (5), (7), (8), (21), (50), (65), (66), (95), (96), % 67.79/9.72 | | | | | | | | | | | (mp_greater_transitivity) are inconsistent by % 67.79/9.72 | | | | | | | | | | | sub-proof #11. % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | End of split % 67.79/9.72 | | | | | | | | | | % 67.79/9.72 | | | | | | | | | Case 2: % 67.79/9.72 | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | (97) (growth_rate(efficient_producers, all_29_2) = % 67.79/9.72 | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 67.79/9.72 | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 67.79/9.72 | | | | | | | | | | greater(all_41_0, zero) & greater(zero, all_41_1)) % 67.79/9.72 | | | | | | | | | | | (growth_rate(efficient_producers, all_29_2) = % 67.79/9.72 | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 67.79/9.72 | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 67.79/9.72 | | | | | | | | | | greater(all_41_1, zero) & greater(zero, all_41_0)) % 67.79/9.72 | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | BETA: splitting (97) gives: % 67.79/9.72 | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | Case 1: % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | (98) growth_rate(efficient_producers, all_29_2) = % 67.79/9.72 | | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 67.79/9.72 | | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 67.79/9.72 | | | | | | | | | | | greater(all_41_0, zero) & greater(zero, all_41_1) % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | ALPHA: (98) implies: % 67.79/9.72 | | | | | | | | | | | (99) greater(all_41_0, zero) % 67.79/9.72 | | | | | | | | | | | (100) growth_rate(efficient_producers, all_29_2) = % 67.79/9.72 | | | | | | | | | | | all_41_0 % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | | REF_CLOSE: (8), (54), (55), (99), (100) are inconsistent by % 67.79/9.72 | | | | | | | | | | | sub-proof #19. % 67.79/9.72 | | | | | | | | | | | % 67.79/9.72 | | | | | | | | | | Case 2: % 67.79/9.72 | | | | | | | | | | | % 67.79/9.73 | | | | | | | | | | | (101) growth_rate(efficient_producers, all_29_2) = % 67.79/9.73 | | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 67.79/9.73 | | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 67.79/9.73 | | | | | | | | | | | greater(all_41_1, zero) & greater(zero, all_41_0) % 67.79/9.73 | | | | | | | | | | | % 67.79/9.73 | | | | | | | | | | | ALPHA: (101) implies: % 67.79/9.73 | | | | | | | | | | | (102) greater(all_41_1, zero) % 67.79/9.73 | | | | | | | | | | | (103) $i(all_41_1) % 67.79/9.73 | | | | | | | | | | | (104) $i(all_41_0) % 67.79/9.73 | | | | | | | | | | | (105) growth_rate(first_movers, all_29_2) = all_41_1 % 67.79/9.73 | | | | | | | | | | | (106) growth_rate(efficient_producers, all_29_2) = % 67.79/9.73 | | | | | | | | | | | all_41_0 % 67.79/9.73 | | | | | | | | | | | % 67.79/9.73 | | | | | | | | | | | REF_CLOSE: (5), (8), (48), (54), (55), (57), (102), (103), % 67.79/9.73 | | | | | | | | | | | (104), (105), (106), (mp_greater_transitivity) are % 67.79/9.73 | | | | | | | | | | | inconsistent by sub-proof #18. % 67.79/9.73 | | | | | | | | | | | % 67.79/9.73 | | | | | | | | | | End of split % 67.79/9.73 | | | | | | | | | | % 67.79/9.73 | | | | | | | | | End of split % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | End of split % 67.79/9.73 | | | | | | | | % 67.79/9.73 | | | | | | | Case 2: % 67.79/9.73 | | | | | | | | % 67.79/9.73 | | | | | | | | (107) all_31_2 = all_21_0 % 67.79/9.73 | | | | | | | | % 67.79/9.73 | | | | | | | | REDUCE: (81), (107) imply: % 67.79/9.73 | | | | | | | | (108) $false % 67.79/9.73 | | | | | | | | % 67.79/9.73 | | | | | | | | CLOSE: (108) is inconsistent. % 67.79/9.73 | | | | | | | | % 67.79/9.73 | | | | | | | End of split % 67.79/9.73 | | | | | | | % 67.79/9.73 | | | | | | Case 2: % 67.79/9.73 | | | | | | | % 67.79/9.73 | | | | | | | (109) all_31_2 = all_19_0 % 67.79/9.73 | | | | | | | % 67.79/9.73 | | | | | | | REDUCE: (66), (109) imply: % 67.79/9.73 | | | | | | | (110) growth_rate(efficient_producers, all_19_0) = all_31_1 % 67.79/9.73 | | | | | | | % 67.79/9.73 | | | | | | | REDUCE: (74), (109) imply: % 67.79/9.73 | | | | | | | (111) growth_rate(first_movers, all_19_0) = all_106_0 % 67.79/9.73 | | | | | | | % 67.79/9.73 | | | | | | | BETA: splitting (50) gives: % 67.79/9.73 | | | | | | | % 67.79/9.73 | | | | | | | Case 1: % 67.79/9.73 | | | | | | | | % 67.79/9.73 | | | | | | | | (112) (all_40_0 = zero & all_40_1 = zero & % 67.79/9.73 | | | | | | | | growth_rate(efficient_producers, all_31_2) = zero & % 67.79/9.73 | | | | | | | | growth_rate(first_movers, all_31_2) = zero) | % 67.79/9.73 | | | | | | | | (equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 67.79/9.73 | | | | | | | | greater_or_equal(all_31_2, all_40_2)) % 67.79/9.73 | | | | | | | | % 67.79/9.73 | | | | | | | | BETA: splitting (112) gives: % 67.79/9.73 | | | | | | | | % 67.79/9.73 | | | | | | | | Case 1: % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | | (113) all_40_0 = zero & all_40_1 = zero & % 67.79/9.73 | | | | | | | | | growth_rate(efficient_producers, all_31_2) = zero & % 67.79/9.73 | | | | | | | | | growth_rate(first_movers, all_31_2) = zero % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | | ALPHA: (113) implies: % 67.79/9.73 | | | | | | | | | (114) growth_rate(first_movers, all_31_2) = zero % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | | REDUCE: (109), (114) imply: % 67.79/9.73 | | | | | | | | | (115) growth_rate(first_movers, all_19_0) = zero % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | | GROUND_INST: instantiating (8) with zero, all_106_0, all_19_0, % 67.79/9.73 | | | | | | | | | first_movers, simplifying with (111), (115) gives: % 67.79/9.73 | | | | | | | | | (116) all_106_0 = zero % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | | REDUCE: (78), (116) imply: % 67.79/9.73 | | | | | | | | | (117) $false % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | | CLOSE: (117) is inconsistent. % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | Case 2: % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | | (118) equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 67.79/9.73 | | | | | | | | | greater_or_equal(all_31_2, all_40_2) % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | | ALPHA: (118) implies: % 67.79/9.73 | | | | | | | | | (119) ~ greater_or_equal(all_31_2, all_40_2) % 67.79/9.73 | | | | | | | | | (120) equilibrium(all_11_0) = all_40_2 % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | | REDUCE: (109), (119) imply: % 67.79/9.73 | | | | | | | | | (121) ~ greater_or_equal(all_19_0, all_40_2) % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | | REF_CLOSE: (7), (18), (21), (120), (121) are inconsistent by % 67.79/9.73 | | | | | | | | | sub-proof #9. % 67.79/9.73 | | | | | | | | | % 67.79/9.73 | | | | | | | | End of split % 67.79/9.73 | | | | | | | | % 67.79/9.73 | | | | | | | Case 2: % 67.79/9.73 | | | | | | | | % 67.79/9.74 | | | | | | | | (122) (growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.74 | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 67.79/9.74 | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_0, zero) % 67.79/9.74 | | | | | | | | & greater(zero, all_40_1)) | % 67.79/9.74 | | | | | | | | (growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.74 | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 67.79/9.74 | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_1, zero) % 67.79/9.74 | | | | | | | | & greater(zero, all_40_0)) % 67.79/9.74 | | | | | | | | % 67.79/9.74 | | | | | | | | BETA: splitting (122) gives: % 67.79/9.74 | | | | | | | | % 67.79/9.74 | | | | | | | | Case 1: % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | (123) growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.74 | | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 67.79/9.74 | | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_0, zero) % 67.79/9.74 | | | | | | | | | & greater(zero, all_40_1) % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | ALPHA: (123) implies: % 67.79/9.74 | | | | | | | | | (124) greater(all_40_0, zero) % 67.79/9.74 | | | | | | | | | (125) growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | REF_CLOSE: (8), (65), (66), (124), (125) are inconsistent by % 67.79/9.74 | | | | | | | | | sub-proof #12. % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | Case 2: % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | (126) growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.74 | | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 67.79/9.74 | | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_1, zero) % 67.79/9.74 | | | | | | | | | & greater(zero, all_40_0) % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | ALPHA: (126) implies: % 67.79/9.74 | | | | | | | | | (127) greater(all_40_1, zero) % 67.79/9.74 | | | | | | | | | (128) $i(all_40_0) % 67.79/9.74 | | | | | | | | | (129) growth_rate(first_movers, all_31_2) = all_40_1 % 67.79/9.74 | | | | | | | | | (130) growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | REDUCE: (109), (130) imply: % 67.79/9.74 | | | | | | | | | (131) growth_rate(efficient_producers, all_19_0) = all_40_0 % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | REDUCE: (109), (129) imply: % 67.79/9.74 | | | | | | | | | (132) growth_rate(first_movers, all_19_0) = all_40_1 % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | GROUND_INST: instantiating (8) with all_40_1, all_106_0, % 67.79/9.74 | | | | | | | | | all_19_0, first_movers, simplifying with (111), % 67.79/9.74 | | | | | | | | | (132) gives: % 67.79/9.74 | | | | | | | | | (133) all_106_0 = all_40_1 % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | GROUND_INST: instantiating (8) with all_31_1, all_40_0, % 67.79/9.74 | | | | | | | | | all_19_0, efficient_producers, simplifying with % 67.79/9.74 | | | | | | | | | (110), (131) gives: % 67.79/9.74 | | | | | | | | | (134) all_40_0 = all_31_1 % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | REDUCE: (73), (133) imply: % 67.79/9.74 | | | | | | | | | (135) $i(all_40_1) % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | REDUCE: (128), (134) imply: % 67.79/9.74 | | | | | | | | | (136) $i(all_31_1) % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | REDUCE: (77), (133) imply: % 67.79/9.74 | | | | | | | | | (137) greater(all_31_1, all_40_1) % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with % 67.79/9.74 | | | | | | | | | all_31_1, all_40_1, zero, simplifying with (5), % 67.79/9.74 | | | | | | | | | (65), (127), (135), (136), (137) gives: % 67.79/9.74 | | | | | | | | | (138) $false % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | | CLOSE: (138) is inconsistent. % 67.79/9.74 | | | | | | | | | % 67.79/9.74 | | | | | | | | End of split % 67.79/9.74 | | | | | | | | % 67.79/9.74 | | | | | | | End of split % 67.79/9.74 | | | | | | | % 67.79/9.74 | | | | | | End of split % 67.79/9.74 | | | | | | % 67.79/9.74 | | | | | End of split % 67.79/9.74 | | | | | % 67.79/9.74 | | | | Case 2: % 67.79/9.74 | | | | | % 67.79/9.74 | | | | | (139) growth_rate(first_movers, all_31_2) = all_31_0 & $i(all_31_0) % 67.79/9.74 | | | | | & ~ greater(zero, all_31_0) % 67.79/9.74 | | | | | % 67.79/9.74 | | | | | ALPHA: (139) implies: % 67.79/9.74 | | | | | (140) ~ greater(zero, all_31_0) % 67.79/9.74 | | | | | (141) growth_rate(first_movers, all_31_2) = all_31_0 % 67.79/9.74 | | | | | % 67.79/9.74 | | | | | BETA: splitting (45) gives: % 67.79/9.74 | | | | | % 67.79/9.74 | | | | | Case 1: % 67.79/9.74 | | | | | | % 67.79/9.74 | | | | | | (142) ~ greater_or_equal(all_31_2, all_21_0) % 67.79/9.74 | | | | | | % 67.79/9.74 | | | | | | PRED_UNIFY: (36), (142) imply: % 67.79/9.75 | | | | | | (143) ~ (all_21_0 = all_19_0) % 67.79/9.75 | | | | | | % 67.79/9.75 | | | | | | REF_CLOSE: (1), (20), (24), (38), (41), (63), (142), (143), % 67.79/9.75 | | | | | | (mp_greater_transitivity) are inconsistent by sub-proof % 67.79/9.75 | | | | | | #14. % 67.79/9.75 | | | | | | % 67.79/9.75 | | | | | Case 2: % 67.79/9.75 | | | | | | % 67.79/9.75 | | | | | | (144) ? [v0: $i] : ? [v1: $i] : % 67.79/9.75 | | | | | | (growth_rate(efficient_producers, all_31_2) = v0 & % 67.79/9.75 | | | | | | growth_rate(first_movers, all_31_2) = v1 & $i(v1) & % 67.79/9.75 | | | | | | $i(v0) & greater(v0, v1)) % 67.79/9.75 | | | | | | % 67.79/9.75 | | | | | | DELTA: instantiating (144) with fresh symbols all_106_0, all_106_1 % 67.79/9.75 | | | | | | gives: % 67.79/9.75 | | | | | | (145) growth_rate(efficient_producers, all_31_2) = all_106_1 & % 67.79/9.75 | | | | | | growth_rate(first_movers, all_31_2) = all_106_0 & % 67.79/9.75 | | | | | | $i(all_106_0) & $i(all_106_1) & greater(all_106_1, % 67.79/9.75 | | | | | | all_106_0) % 67.79/9.75 | | | | | | % 67.79/9.75 | | | | | | ALPHA: (145) implies: % 67.79/9.75 | | | | | | (146) greater(all_106_1, all_106_0) % 67.79/9.75 | | | | | | (147) $i(all_106_1) % 67.79/9.75 | | | | | | (148) growth_rate(first_movers, all_31_2) = all_106_0 % 67.79/9.75 | | | | | | (149) growth_rate(efficient_producers, all_31_2) = all_106_1 % 67.79/9.75 | | | | | | % 67.79/9.75 | | | | | | GROUND_INST: instantiating (8) with all_31_0, all_106_0, all_31_2, % 67.79/9.75 | | | | | | first_movers, simplifying with (141), (148) gives: % 67.79/9.75 | | | | | | (150) all_106_0 = all_31_0 % 67.79/9.75 | | | | | | % 67.79/9.75 | | | | | | REDUCE: (146), (150) imply: % 67.79/9.75 | | | | | | (151) greater(all_106_1, all_31_0) % 67.79/9.75 | | | | | | % 67.79/9.75 | | | | | | PRED_UNIFY: (140), (151) imply: % 67.79/9.75 | | | | | | (152) ~ (all_106_1 = zero) % 67.79/9.75 | | | | | | % 67.79/9.75 | | | | | | BETA: splitting (41) gives: % 67.79/9.75 | | | | | | % 67.79/9.75 | | | | | | Case 1: % 67.79/9.75 | | | | | | | % 67.79/9.75 | | | | | | | (153) greater(all_31_2, all_19_0) % 67.79/9.75 | | | | | | | % 67.79/9.75 | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with % 67.79/9.75 | | | | | | | all_31_2, all_19_0, all_19_1, simplifying with (19), % 67.79/9.75 | | | | | | | (20), (38), (59), (153) gives: % 67.79/9.75 | | | | | | | (154) greater(all_31_2, all_19_1) % 67.79/9.75 | | | | | | | % 67.79/9.75 | | | | | | | BETA: splitting (52) gives: % 67.79/9.75 | | | | | | | % 67.79/9.75 | | | | | | | Case 1: % 67.79/9.75 | | | | | | | | % 67.79/9.75 | | | | | | | | % 67.79/9.75 | | | | | | | | GROUND_INST: instantiating (1) with all_31_2, all_19_1, % 67.79/9.75 | | | | | | | | simplifying with (19), (38), (154) gives: % 67.79/9.75 | | | | | | | | (155) greater_or_equal(all_31_2, all_19_1) % 67.79/9.75 | | | | | | | | % 67.79/9.75 | | | | | | | | DELTA: instantiating (144) with fresh symbols all_106_0, % 67.79/9.75 | | | | | | | | all_106_1 gives: % 67.79/9.75 | | | | | | | | (156) growth_rate(efficient_producers, all_31_2) = all_106_1 % 67.79/9.75 | | | | | | | | & growth_rate(first_movers, all_31_2) = all_106_0 & % 67.79/9.75 | | | | | | | | $i(all_106_0) & $i(all_106_1) & greater(all_106_1, % 67.79/9.75 | | | | | | | | all_106_0) % 67.79/9.75 | | | | | | | | % 67.79/9.75 | | | | | | | | REF_CLOSE: (5), (7), (8), (21), (50), (140), (141), (155), % 67.79/9.75 | | | | | | | | (156), (mp_greater_transitivity) are inconsistent by % 67.79/9.75 | | | | | | | | sub-proof #7. % 67.79/9.75 | | | | | | | | % 67.79/9.75 | | | | | | | Case 2: % 67.79/9.75 | | | | | | | | % 67.79/9.75 | | | | | | | | (157) all_38_0 = all_38_1 % 67.79/9.75 | | | | | | | | % 67.79/9.75 | | | | | | | | COMBINE_EQS: (56), (157) imply: % 67.79/9.75 | | | | | | | | (158) all_38_0 = all_29_1 % 67.79/9.75 | | | | | | | | % 67.79/9.75 | | | | | | | | REDUCE: (58), (158) imply: % 67.79/9.75 | | | | | | | | (159) ~ (all_29_1 = zero) % 67.79/9.75 | | | | | | | | % 67.79/9.75 | | | | | | | | BETA: splitting (51) gives: % 67.79/9.75 | | | | | | | | % 67.79/9.75 | | | | | | | | Case 1: % 67.79/9.75 | | | | | | | | | % 67.79/9.75 | | | | | | | | | (160) (all_41_0 = zero & all_41_1 = zero & % 67.79/9.75 | | | | | | | | | growth_rate(efficient_producers, all_29_2) = zero & % 67.79/9.75 | | | | | | | | | growth_rate(first_movers, all_29_2) = zero) | % 67.79/9.75 | | | | | | | | | (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 67.79/9.75 | | | | | | | | | greater_or_equal(all_29_2, all_41_2)) % 67.79/9.75 | | | | | | | | | % 67.79/9.75 | | | | | | | | | BETA: splitting (160) gives: % 67.79/9.75 | | | | | | | | | % 67.79/9.75 | | | | | | | | | Case 1: % 67.79/9.75 | | | | | | | | | | % 67.79/9.75 | | | | | | | | | | (161) all_41_0 = zero & all_41_1 = zero & % 67.79/9.75 | | | | | | | | | | growth_rate(efficient_producers, all_29_2) = zero & % 67.79/9.75 | | | | | | | | | | growth_rate(first_movers, all_29_2) = zero % 67.79/9.75 | | | | | | | | | | % 67.79/9.75 | | | | | | | | | | ALPHA: (161) implies: % 67.79/9.76 | | | | | | | | | | (162) growth_rate(efficient_producers, all_29_2) = zero % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | REF_CLOSE: (8), (55), (159), (162) are inconsistent by % 67.79/9.76 | | | | | | | | | | sub-proof #10. % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | Case 2: % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | (163) equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & % 67.79/9.76 | | | | | | | | | | ~ greater_or_equal(all_29_2, all_41_2) % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | ALPHA: (163) implies: % 67.79/9.76 | | | | | | | | | | (164) $i(all_41_2) % 67.79/9.76 | | | | | | | | | | (165) equilibrium(all_11_0) = all_41_2 % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | GROUND_INST: instantiating (7) with all_19_1, all_41_2, % 67.79/9.76 | | | | | | | | | | all_11_0, simplifying with (21), (165) gives: % 67.79/9.76 | | | | | | | | | | (166) all_41_2 = all_19_1 % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | GROUND_INST: instantiating (1) with all_31_2, all_19_1, % 67.79/9.76 | | | | | | | | | | simplifying with (19), (38), (154) gives: % 67.79/9.76 | | | | | | | | | | (167) greater_or_equal(all_31_2, all_19_1) % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | DELTA: instantiating (144) with fresh symbols all_106_0, % 67.79/9.76 | | | | | | | | | | all_106_1 gives: % 67.79/9.76 | | | | | | | | | | (168) growth_rate(efficient_producers, all_31_2) = % 67.79/9.76 | | | | | | | | | | all_106_1 & growth_rate(first_movers, all_31_2) = % 67.79/9.76 | | | | | | | | | | all_106_0 & $i(all_106_0) & $i(all_106_1) & % 67.79/9.76 | | | | | | | | | | greater(all_106_1, all_106_0) % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | REF_CLOSE: (5), (7), (8), (21), (50), (140), (141), (167), % 67.79/9.76 | | | | | | | | | | (168), (mp_greater_transitivity) are inconsistent % 67.79/9.76 | | | | | | | | | | by sub-proof #7. % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | End of split % 67.79/9.76 | | | | | | | | | % 67.79/9.76 | | | | | | | | Case 2: % 67.79/9.76 | | | | | | | | | % 67.79/9.76 | | | | | | | | | (169) (growth_rate(efficient_producers, all_29_2) = % 67.79/9.76 | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 67.79/9.76 | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 67.79/9.76 | | | | | | | | | greater(all_41_0, zero) & greater(zero, all_41_1)) % 67.79/9.76 | | | | | | | | | | (growth_rate(efficient_producers, all_29_2) = % 67.79/9.76 | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 67.79/9.76 | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 67.79/9.76 | | | | | | | | | greater(all_41_1, zero) & greater(zero, all_41_0)) % 67.79/9.76 | | | | | | | | | % 67.79/9.76 | | | | | | | | | BETA: splitting (169) gives: % 67.79/9.76 | | | | | | | | | % 67.79/9.76 | | | | | | | | | Case 1: % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | (170) growth_rate(efficient_producers, all_29_2) = % 67.79/9.76 | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 67.79/9.76 | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 67.79/9.76 | | | | | | | | | | greater(all_41_0, zero) & greater(zero, all_41_1) % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | ALPHA: (170) implies: % 67.79/9.76 | | | | | | | | | | (171) greater(all_41_0, zero) % 67.79/9.76 | | | | | | | | | | (172) growth_rate(efficient_producers, all_29_2) = % 67.79/9.76 | | | | | | | | | | all_41_0 % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | REF_CLOSE: (8), (54), (55), (171), (172) are inconsistent by % 67.79/9.76 | | | | | | | | | | sub-proof #19. % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | Case 2: % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | (173) growth_rate(efficient_producers, all_29_2) = % 67.79/9.76 | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 67.79/9.76 | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 67.79/9.76 | | | | | | | | | | greater(all_41_1, zero) & greater(zero, all_41_0) % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | ALPHA: (173) implies: % 67.79/9.76 | | | | | | | | | | (174) greater(all_41_1, zero) % 67.79/9.76 | | | | | | | | | | (175) $i(all_41_1) % 67.79/9.76 | | | | | | | | | | (176) $i(all_41_0) % 67.79/9.76 | | | | | | | | | | (177) growth_rate(first_movers, all_29_2) = all_41_1 % 67.79/9.76 | | | | | | | | | | (178) growth_rate(efficient_producers, all_29_2) = % 67.79/9.76 | | | | | | | | | | all_41_0 % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | | REF_CLOSE: (5), (8), (48), (54), (55), (57), (174), (175), % 67.79/9.76 | | | | | | | | | | (176), (177), (178), (mp_greater_transitivity) are % 67.79/9.76 | | | | | | | | | | inconsistent by sub-proof #18. % 67.79/9.76 | | | | | | | | | | % 67.79/9.76 | | | | | | | | | End of split % 67.79/9.76 | | | | | | | | | % 67.79/9.76 | | | | | | | | End of split % 67.79/9.76 | | | | | | | | % 67.79/9.76 | | | | | | | End of split % 67.79/9.76 | | | | | | | % 67.79/9.76 | | | | | | Case 2: % 67.79/9.76 | | | | | | | % 67.79/9.76 | | | | | | | (179) all_31_2 = all_19_0 % 67.79/9.76 | | | | | | | % 67.79/9.76 | | | | | | | REDUCE: (149), (179) imply: % 67.79/9.76 | | | | | | | (180) growth_rate(efficient_producers, all_19_0) = all_106_1 % 67.79/9.76 | | | | | | | % 67.79/9.76 | | | | | | | REDUCE: (141), (179) imply: % 67.79/9.77 | | | | | | | (181) growth_rate(first_movers, all_19_0) = all_31_0 % 67.79/9.77 | | | | | | | % 67.79/9.77 | | | | | | | BETA: splitting (50) gives: % 67.79/9.77 | | | | | | | % 67.79/9.77 | | | | | | | Case 1: % 67.79/9.77 | | | | | | | | % 67.79/9.77 | | | | | | | | (182) (all_40_0 = zero & all_40_1 = zero & % 67.79/9.77 | | | | | | | | growth_rate(efficient_producers, all_31_2) = zero & % 67.79/9.77 | | | | | | | | growth_rate(first_movers, all_31_2) = zero) | % 67.79/9.77 | | | | | | | | (equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 67.79/9.77 | | | | | | | | greater_or_equal(all_31_2, all_40_2)) % 67.79/9.77 | | | | | | | | % 67.79/9.77 | | | | | | | | BETA: splitting (182) gives: % 67.79/9.77 | | | | | | | | % 67.79/9.77 | | | | | | | | Case 1: % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | (183) all_40_0 = zero & all_40_1 = zero & % 67.79/9.77 | | | | | | | | | growth_rate(efficient_producers, all_31_2) = zero & % 67.79/9.77 | | | | | | | | | growth_rate(first_movers, all_31_2) = zero % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | ALPHA: (183) implies: % 67.79/9.77 | | | | | | | | | (184) growth_rate(efficient_producers, all_31_2) = zero % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | REDUCE: (179), (184) imply: % 67.79/9.77 | | | | | | | | | (185) growth_rate(efficient_producers, all_19_0) = zero % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | GROUND_INST: instantiating (8) with zero, all_106_1, all_19_0, % 67.79/9.77 | | | | | | | | | efficient_producers, simplifying with (180), (185) % 67.79/9.77 | | | | | | | | | gives: % 67.79/9.77 | | | | | | | | | (186) all_106_1 = zero % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | REDUCE: (152), (186) imply: % 67.79/9.77 | | | | | | | | | (187) $false % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | CLOSE: (187) is inconsistent. % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | Case 2: % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | (188) equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 67.79/9.77 | | | | | | | | | greater_or_equal(all_31_2, all_40_2) % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | ALPHA: (188) implies: % 67.79/9.77 | | | | | | | | | (189) ~ greater_or_equal(all_31_2, all_40_2) % 67.79/9.77 | | | | | | | | | (190) equilibrium(all_11_0) = all_40_2 % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | REDUCE: (179), (189) imply: % 67.79/9.77 | | | | | | | | | (191) ~ greater_or_equal(all_19_0, all_40_2) % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | REF_CLOSE: (7), (18), (21), (190), (191) are inconsistent by % 67.79/9.77 | | | | | | | | | sub-proof #9. % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | End of split % 67.79/9.77 | | | | | | | | % 67.79/9.77 | | | | | | | Case 2: % 67.79/9.77 | | | | | | | | % 67.79/9.77 | | | | | | | | (192) (growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.77 | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 67.79/9.77 | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_0, zero) % 67.79/9.77 | | | | | | | | & greater(zero, all_40_1)) | % 67.79/9.77 | | | | | | | | (growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.77 | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 67.79/9.77 | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_1, zero) % 67.79/9.77 | | | | | | | | & greater(zero, all_40_0)) % 67.79/9.77 | | | | | | | | % 67.79/9.77 | | | | | | | | BETA: splitting (192) gives: % 67.79/9.77 | | | | | | | | % 67.79/9.77 | | | | | | | | Case 1: % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | (193) growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.77 | | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 67.79/9.77 | | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_0, zero) % 67.79/9.77 | | | | | | | | | & greater(zero, all_40_1) % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | ALPHA: (193) implies: % 67.79/9.77 | | | | | | | | | (194) greater(zero, all_40_1) % 67.79/9.77 | | | | | | | | | (195) growth_rate(first_movers, all_31_2) = all_40_1 % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | REF_CLOSE: (8), (140), (141), (194), (195) are inconsistent by % 67.79/9.77 | | | | | | | | | sub-proof #8. % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | Case 2: % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | (196) growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.77 | | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 67.79/9.77 | | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_1, zero) % 67.79/9.77 | | | | | | | | | & greater(zero, all_40_0) % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | ALPHA: (196) implies: % 67.79/9.77 | | | | | | | | | (197) greater(zero, all_40_0) % 67.79/9.77 | | | | | | | | | (198) $i(all_40_1) % 67.79/9.77 | | | | | | | | | (199) growth_rate(first_movers, all_31_2) = all_40_1 % 67.79/9.77 | | | | | | | | | (200) growth_rate(efficient_producers, all_31_2) = all_40_0 % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | REDUCE: (179), (200) imply: % 67.79/9.77 | | | | | | | | | (201) growth_rate(efficient_producers, all_19_0) = all_40_0 % 67.79/9.77 | | | | | | | | | % 67.79/9.77 | | | | | | | | | REDUCE: (179), (199) imply: % 67.79/9.78 | | | | | | | | | (202) growth_rate(first_movers, all_19_0) = all_40_1 % 67.79/9.78 | | | | | | | | | % 67.79/9.78 | | | | | | | | | GROUND_INST: instantiating (8) with all_31_0, all_40_1, % 67.79/9.78 | | | | | | | | | all_19_0, first_movers, simplifying with (181), % 67.79/9.78 | | | | | | | | | (202) gives: % 67.79/9.78 | | | | | | | | | (203) all_40_1 = all_31_0 % 67.79/9.78 | | | | | | | | | % 67.79/9.78 | | | | | | | | | GROUND_INST: instantiating (8) with all_40_0, all_106_1, % 67.79/9.78 | | | | | | | | | all_19_0, efficient_producers, simplifying with % 67.79/9.78 | | | | | | | | | (180), (201) gives: % 67.79/9.78 | | | | | | | | | (204) all_106_1 = all_40_0 % 67.79/9.78 | | | | | | | | | % 67.79/9.78 | | | | | | | | | REDUCE: (147), (204) imply: % 67.79/9.78 | | | | | | | | | (205) $i(all_40_0) % 67.79/9.78 | | | | | | | | | % 67.79/9.78 | | | | | | | | | REDUCE: (198), (203) imply: % 67.79/9.78 | | | | | | | | | (206) $i(all_31_0) % 67.79/9.78 | | | | | | | | | % 67.79/9.78 | | | | | | | | | REDUCE: (151), (204) imply: % 67.79/9.78 | | | | | | | | | (207) greater(all_40_0, all_31_0) % 67.79/9.78 | | | | | | | | | % 67.79/9.78 | | | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with zero, % 67.79/9.78 | | | | | | | | | all_40_0, all_31_0, simplifying with (5), (140), % 67.79/9.78 | | | | | | | | | (197), (205), (206), (207) gives: % 67.79/9.78 | | | | | | | | | (208) $false % 67.79/9.78 | | | | | | | | | % 67.79/9.78 | | | | | | | | | CLOSE: (208) is inconsistent. % 67.79/9.78 | | | | | | | | | % 67.79/9.78 | | | | | | | | End of split % 67.79/9.78 | | | | | | | | % 67.79/9.78 | | | | | | | End of split % 67.79/9.78 | | | | | | | % 67.79/9.78 | | | | | | End of split % 67.79/9.78 | | | | | | % 67.79/9.78 | | | | | End of split % 67.79/9.78 | | | | | % 67.79/9.78 | | | | End of split % 67.79/9.78 | | | | % 67.79/9.78 | | | End of split % 67.79/9.78 | | | % 67.79/9.78 | | Case 2: % 67.79/9.78 | | | % 67.79/9.78 | | | (209) all_19_0 = all_19_1 % 67.79/9.78 | | | % 67.79/9.78 | | | REDUCE: (36), (209) imply: % 67.79/9.78 | | | (210) greater_or_equal(all_31_2, all_19_1) % 67.79/9.78 | | | % 67.79/9.78 | | | BETA: splitting (27) gives: % 67.79/9.78 | | | % 67.79/9.78 | | | Case 1: % 67.79/9.78 | | | | % 67.79/9.78 | | | | (211) greater(all_21_0, all_19_0) % 67.79/9.78 | | | | % 67.79/9.78 | | | | REDUCE: (209), (211) imply: % 67.79/9.78 | | | | (212) greater(all_21_0, all_19_1) % 67.79/9.78 | | | | % 67.79/9.78 | | | | REF_CLOSE: (1), (5), (7), (8), (19), (21), (24), (33), (40), (48), (51), % 67.79/9.78 | | | | (52), (54), (55), (56), (57), (58), (212), % 67.79/9.78 | | | | (mp_greater_transitivity) are inconsistent by sub-proof #15. % 67.79/9.78 | | | | % 67.79/9.78 | | | Case 2: % 67.79/9.78 | | | | % 67.79/9.78 | | | | (213) all_21_0 = all_19_0 | greater(all_19_0, all_21_0) % 67.79/9.78 | | | | % 67.79/9.78 | | | | REF_CLOSE: (1), (5), (7), (8), (19), (21), (24), (38), (39), (41), (45), % 67.79/9.78 | | | | (50), (209), (210), (213), (mp_greater_transitivity) are % 67.79/9.78 | | | | inconsistent by sub-proof #5. % 67.79/9.78 | | | | % 67.79/9.78 | | | End of split % 67.79/9.78 | | | % 67.79/9.78 | | End of split % 67.79/9.78 | | % 67.79/9.78 | Case 2: % 67.79/9.78 | | % 67.79/9.78 | | (214) growth_rate(first_movers, all_29_2) = all_29_0 & $i(all_29_0) & ~ % 67.79/9.78 | | greater(zero, all_29_0) % 67.79/9.78 | | % 67.79/9.78 | | ALPHA: (214) implies: % 67.79/9.78 | | (215) ~ greater(zero, all_29_0) % 67.79/9.78 | | (216) growth_rate(first_movers, all_29_2) = all_29_0 % 67.79/9.78 | | % 67.79/9.78 | | GROUND_INST: instantiating (8) with all_38_0, all_29_0, all_29_2, % 67.79/9.78 | | first_movers, simplifying with (48), (216) gives: % 67.79/9.78 | | (217) all_38_0 = all_29_0 % 67.79/9.78 | | % 67.79/9.78 | | REDUCE: (47), (217) imply: % 67.79/9.78 | | (218) greater(all_38_1, all_29_0) % 67.79/9.78 | | % 67.79/9.78 | | PRED_UNIFY: (215), (218) imply: % 67.79/9.79 | | (219) ~ (all_38_1 = zero) % 67.79/9.79 | | % 67.79/9.79 | | BETA: splitting (29) gives: % 67.79/9.79 | | % 67.79/9.79 | | Case 1: % 67.79/9.79 | | | % 67.79/9.79 | | | (220) greater(all_19_0, all_19_1) % 67.79/9.79 | | | % 67.79/9.79 | | | BETA: splitting (27) gives: % 67.79/9.79 | | | % 67.79/9.79 | | | Case 1: % 67.79/9.79 | | | | % 67.79/9.79 | | | | (221) greater(all_21_0, all_19_0) % 67.79/9.79 | | | | % 67.79/9.79 | | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_21_0, % 67.79/9.79 | | | | all_19_0, all_19_1, simplifying with (19), (20), (24), % 67.79/9.79 | | | | (220), (221) gives: % 67.79/9.79 | | | | (222) greater(all_21_0, all_19_1) % 67.79/9.79 | | | | % 67.79/9.79 | | | | REF_CLOSE: (1), (5), (7), (8), (19), (21), (24), (33), (40), (49), (51), % 67.79/9.79 | | | | (215), (216), (218), (219), (222), (mp_greater_transitivity) % 67.79/9.79 | | | | are inconsistent by sub-proof #3. % 67.79/9.79 | | | | % 67.79/9.79 | | | Case 2: % 67.79/9.79 | | | | % 67.79/9.79 | | | | (223) ~ greater(all_21_0, all_19_0) % 67.79/9.79 | | | | (224) all_21_0 = all_19_0 | greater(all_19_0, all_21_0) % 67.79/9.79 | | | | % 67.79/9.79 | | | | BETA: splitting (39) gives: % 67.79/9.79 | | | | % 67.79/9.79 | | | | Case 1: % 67.79/9.79 | | | | | % 67.79/9.79 | | | | | (225) growth_rate(efficient_producers, all_31_2) = all_31_1 & % 67.79/9.79 | | | | | $i(all_31_1) & ~ greater(all_31_1, zero) % 67.79/9.79 | | | | | % 67.79/9.79 | | | | | ALPHA: (225) implies: % 67.79/9.79 | | | | | (226) ~ greater(all_31_1, zero) % 67.79/9.79 | | | | | (227) growth_rate(efficient_producers, all_31_2) = all_31_1 % 67.79/9.79 | | | | | % 67.79/9.79 | | | | | BETA: splitting (45) gives: % 67.79/9.79 | | | | | % 67.79/9.79 | | | | | Case 1: % 67.79/9.79 | | | | | | % 67.79/9.79 | | | | | | (228) ~ greater_or_equal(all_31_2, all_21_0) % 67.79/9.79 | | | | | | % 67.79/9.79 | | | | | | PRED_UNIFY: (36), (228) imply: % 67.79/9.79 | | | | | | (229) ~ (all_21_0 = all_19_0) % 67.79/9.79 | | | | | | % 67.79/9.79 | | | | | | REF_CLOSE: (1), (20), (24), (38), (41), (224), (228), (229), % 67.79/9.79 | | | | | | (mp_greater_transitivity) are inconsistent by sub-proof % 67.79/9.79 | | | | | | #14. % 67.79/9.79 | | | | | | % 67.79/9.79 | | | | | Case 2: % 67.79/9.79 | | | | | | % 67.79/9.79 | | | | | | (230) greater_or_equal(all_31_2, all_21_0) % 67.79/9.79 | | | | | | (231) ? [v0: $i] : ? [v1: $i] : % 67.79/9.79 | | | | | | (growth_rate(efficient_producers, all_31_2) = v0 & % 67.79/9.79 | | | | | | growth_rate(first_movers, all_31_2) = v1 & $i(v1) & % 67.79/9.79 | | | | | | $i(v0) & greater(v0, v1)) % 67.79/9.79 | | | | | | % 67.79/9.79 | | | | | | DELTA: instantiating (231) with fresh symbols all_106_0, all_106_1 % 67.79/9.79 | | | | | | gives: % 67.79/9.79 | | | | | | (232) growth_rate(efficient_producers, all_31_2) = all_106_1 & % 67.79/9.79 | | | | | | growth_rate(first_movers, all_31_2) = all_106_0 & % 67.79/9.79 | | | | | | $i(all_106_0) & $i(all_106_1) & greater(all_106_1, % 67.79/9.79 | | | | | | all_106_0) % 67.79/9.79 | | | | | | % 67.79/9.79 | | | | | | ALPHA: (232) implies: % 67.79/9.79 | | | | | | (233) greater(all_106_1, all_106_0) % 67.79/9.79 | | | | | | (234) $i(all_106_0) % 67.79/9.79 | | | | | | (235) growth_rate(first_movers, all_31_2) = all_106_0 % 67.79/9.79 | | | | | | (236) growth_rate(efficient_producers, all_31_2) = all_106_1 % 67.79/9.79 | | | | | | % 67.79/9.80 | | | | | | GROUND_INST: instantiating (8) with all_31_1, all_106_1, all_31_2, % 67.79/9.80 | | | | | | efficient_producers, simplifying with (227), (236) % 67.79/9.80 | | | | | | gives: % 67.79/9.80 | | | | | | (237) all_106_1 = all_31_1 % 67.79/9.80 | | | | | | % 67.79/9.80 | | | | | | REDUCE: (233), (237) imply: % 67.79/9.80 | | | | | | (238) greater(all_31_1, all_106_0) % 67.79/9.80 | | | | | | % 67.79/9.80 | | | | | | PRED_UNIFY: (226), (238) imply: % 67.79/9.80 | | | | | | (239) ~ (all_106_0 = zero) % 67.79/9.80 | | | | | | % 68.26/9.80 | | | | | | GROUND_INST: instantiating (2) with all_31_2, all_21_0, simplifying % 68.26/9.80 | | | | | | with (24), (38), (230) gives: % 68.26/9.80 | | | | | | (240) all_31_2 = all_21_0 | greater(all_31_2, all_21_0) % 68.26/9.80 | | | | | | % 68.26/9.80 | | | | | | BETA: splitting (41) gives: % 68.26/9.80 | | | | | | % 68.26/9.80 | | | | | | Case 1: % 68.26/9.80 | | | | | | | % 68.26/9.80 | | | | | | | (241) greater(all_31_2, all_19_0) % 68.26/9.80 | | | | | | | % 68.26/9.80 | | | | | | | PRED_UNIFY: (223), (241) imply: % 68.26/9.80 | | | | | | | (242) ~ (all_31_2 = all_21_0) % 68.26/9.80 | | | | | | | % 68.26/9.80 | | | | | | | BETA: splitting (240) gives: % 68.26/9.80 | | | | | | | % 68.26/9.80 | | | | | | | Case 1: % 68.26/9.80 | | | | | | | | % 68.26/9.80 | | | | | | | | % 68.26/9.80 | | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with % 68.26/9.80 | | | | | | | | all_31_2, all_19_0, all_19_1, simplifying with % 68.26/9.80 | | | | | | | | (19), (20), (38), (220), (241) gives: % 68.26/9.80 | | | | | | | | (243) greater(all_31_2, all_19_1) % 68.26/9.80 | | | | | | | | % 68.26/9.80 | | | | | | | | BETA: splitting (52) gives: % 68.26/9.80 | | | | | | | | % 68.26/9.80 | | | | | | | | Case 1: % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | | GROUND_INST: instantiating (1) with all_31_2, all_19_1, % 68.26/9.80 | | | | | | | | | simplifying with (19), (38), (243) gives: % 68.26/9.80 | | | | | | | | | (244) greater_or_equal(all_31_2, all_19_1) % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | | DELTA: instantiating (231) with fresh symbols all_106_0, % 68.26/9.80 | | | | | | | | | all_106_1 gives: % 68.26/9.80 | | | | | | | | | (245) growth_rate(efficient_producers, all_31_2) = % 68.26/9.80 | | | | | | | | | all_106_1 & growth_rate(first_movers, all_31_2) = % 68.26/9.80 | | | | | | | | | all_106_0 & $i(all_106_0) & $i(all_106_1) & % 68.26/9.80 | | | | | | | | | greater(all_106_1, all_106_0) % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | | REF_CLOSE: (5), (7), (8), (21), (50), (226), (227), (244), % 68.26/9.80 | | | | | | | | | (245), (mp_greater_transitivity) are inconsistent % 68.26/9.80 | | | | | | | | | by sub-proof #11. % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | Case 2: % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | | (246) all_38_0 = all_38_1 % 68.26/9.80 | | | | | | | | | (247) growth_rate(first_movers, all_29_2) = all_38_1 % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | | COMBINE_EQS: (217), (246) imply: % 68.26/9.80 | | | | | | | | | (248) all_38_1 = all_29_0 % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | | REDUCE: (219), (248) imply: % 68.26/9.80 | | | | | | | | | (249) ~ (all_29_0 = zero) % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | | REDUCE: (49), (248) imply: % 68.26/9.80 | | | | | | | | | (250) growth_rate(efficient_producers, all_29_2) = all_29_0 % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | | BETA: splitting (51) gives: % 68.26/9.80 | | | | | | | | | % 68.26/9.80 | | | | | | | | | Case 1: % 68.26/9.80 | | | | | | | | | | % 68.26/9.80 | | | | | | | | | | (251) (all_41_0 = zero & all_41_1 = zero & % 68.26/9.80 | | | | | | | | | | growth_rate(efficient_producers, all_29_2) = zero % 68.26/9.80 | | | | | | | | | | & growth_rate(first_movers, all_29_2) = zero) | % 68.26/9.80 | | | | | | | | | | (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & % 68.26/9.80 | | | | | | | | | | ~ greater_or_equal(all_29_2, all_41_2)) % 68.26/9.80 | | | | | | | | | | % 68.26/9.80 | | | | | | | | | | BETA: splitting (251) gives: % 68.26/9.80 | | | | | | | | | | % 68.26/9.80 | | | | | | | | | | Case 1: % 68.26/9.80 | | | | | | | | | | | % 68.26/9.80 | | | | | | | | | | | (252) all_41_0 = zero & all_41_1 = zero & % 68.26/9.80 | | | | | | | | | | | growth_rate(efficient_producers, all_29_2) = zero % 68.26/9.80 | | | | | | | | | | | & growth_rate(first_movers, all_29_2) = zero % 68.26/9.80 | | | | | | | | | | | % 68.26/9.80 | | | | | | | | | | | ALPHA: (252) implies: % 68.26/9.80 | | | | | | | | | | | (253) growth_rate(efficient_producers, all_29_2) = zero % 68.26/9.80 | | | | | | | | | | | % 68.26/9.80 | | | | | | | | | | | REF_CLOSE: (8), (249), (250), (253) are inconsistent by % 68.26/9.80 | | | | | | | | | | | sub-proof #2. % 68.26/9.80 | | | | | | | | | | | % 68.26/9.80 | | | | | | | | | | Case 2: % 68.26/9.80 | | | | | | | | | | | % 68.26/9.80 | | | | | | | | | | | (254) equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & % 68.26/9.80 | | | | | | | | | | | ~ greater_or_equal(all_29_2, all_41_2) % 68.26/9.80 | | | | | | | | | | | % 68.26/9.80 | | | | | | | | | | | ALPHA: (254) implies: % 68.26/9.80 | | | | | | | | | | | (255) $i(all_41_2) % 68.26/9.80 | | | | | | | | | | | (256) equilibrium(all_11_0) = all_41_2 % 68.26/9.80 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | | GROUND_INST: instantiating (7) with all_19_1, all_41_2, % 68.26/9.81 | | | | | | | | | | | all_11_0, simplifying with (21), (256) gives: % 68.26/9.81 | | | | | | | | | | | (257) all_41_2 = all_19_1 % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | | GROUND_INST: instantiating (1) with all_31_2, all_19_1, % 68.26/9.81 | | | | | | | | | | | simplifying with (19), (38), (243) gives: % 68.26/9.81 | | | | | | | | | | | (258) greater_or_equal(all_31_2, all_19_1) % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | | DELTA: instantiating (231) with fresh symbols all_106_0, % 68.26/9.81 | | | | | | | | | | | all_106_1 gives: % 68.26/9.81 | | | | | | | | | | | (259) growth_rate(efficient_producers, all_31_2) = % 68.26/9.81 | | | | | | | | | | | all_106_1 & growth_rate(first_movers, all_31_2) = % 68.26/9.81 | | | | | | | | | | | all_106_0 & $i(all_106_0) & $i(all_106_1) & % 68.26/9.81 | | | | | | | | | | | greater(all_106_1, all_106_0) % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | | REF_CLOSE: (5), (7), (8), (21), (50), (226), (227), (258), % 68.26/9.81 | | | | | | | | | | | (259), (mp_greater_transitivity) are inconsistent % 68.26/9.81 | | | | | | | | | | | by sub-proof #11. % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | End of split % 68.26/9.81 | | | | | | | | | | % 68.26/9.81 | | | | | | | | | Case 2: % 68.26/9.81 | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | (260) (growth_rate(efficient_producers, all_29_2) = % 68.26/9.81 | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 68.26/9.81 | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 68.26/9.81 | | | | | | | | | | greater(all_41_0, zero) & greater(zero, % 68.26/9.81 | | | | | | | | | | all_41_1)) | (growth_rate(efficient_producers, % 68.26/9.81 | | | | | | | | | | all_29_2) = all_41_0 & % 68.26/9.81 | | | | | | | | | | growth_rate(first_movers, all_29_2) = all_41_1 & % 68.26/9.81 | | | | | | | | | | $i(all_41_0) & $i(all_41_1) & greater(all_41_1, % 68.26/9.81 | | | | | | | | | | zero) & greater(zero, all_41_0)) % 68.26/9.81 | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | BETA: splitting (260) gives: % 68.26/9.81 | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | Case 1: % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | | (261) growth_rate(efficient_producers, all_29_2) = % 68.26/9.81 | | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 68.26/9.81 | | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 68.26/9.81 | | | | | | | | | | | greater(all_41_0, zero) & greater(zero, all_41_1) % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | | ALPHA: (261) implies: % 68.26/9.81 | | | | | | | | | | | (262) greater(zero, all_41_1) % 68.26/9.81 | | | | | | | | | | | (263) growth_rate(first_movers, all_29_2) = all_41_1 % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | | REF_CLOSE: (8), (215), (216), (262), (263) are inconsistent % 68.26/9.81 | | | | | | | | | | | by sub-proof #4. % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | Case 2: % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | | (264) growth_rate(efficient_producers, all_29_2) = % 68.26/9.81 | | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 68.26/9.81 | | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 68.26/9.81 | | | | | | | | | | | greater(all_41_1, zero) & greater(zero, all_41_0) % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | | ALPHA: (264) implies: % 68.26/9.81 | | | | | | | | | | | (265) greater(zero, all_41_0) % 68.26/9.81 | | | | | | | | | | | (266) growth_rate(efficient_producers, all_29_2) = % 68.26/9.81 | | | | | | | | | | | all_41_0 % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | | REF_CLOSE: (8), (215), (250), (265), (266) are inconsistent % 68.26/9.81 | | | | | | | | | | | by sub-proof #1. % 68.26/9.81 | | | | | | | | | | | % 68.26/9.81 | | | | | | | | | | End of split % 68.26/9.81 | | | | | | | | | | % 68.26/9.81 | | | | | | | | | End of split % 68.26/9.81 | | | | | | | | | % 68.26/9.81 | | | | | | | | End of split % 68.26/9.81 | | | | | | | | % 68.26/9.81 | | | | | | | Case 2: % 68.26/9.81 | | | | | | | | % 68.26/9.81 | | | | | | | | (267) all_31_2 = all_21_0 % 68.26/9.81 | | | | | | | | % 68.26/9.81 | | | | | | | | REDUCE: (242), (267) imply: % 68.26/9.81 | | | | | | | | (268) $false % 68.26/9.81 | | | | | | | | % 68.26/9.81 | | | | | | | | CLOSE: (268) is inconsistent. % 68.26/9.81 | | | | | | | | % 68.26/9.81 | | | | | | | End of split % 68.26/9.81 | | | | | | | % 68.26/9.81 | | | | | | Case 2: % 68.26/9.81 | | | | | | | % 68.26/9.81 | | | | | | | (269) all_31_2 = all_19_0 % 68.26/9.81 | | | | | | | % 68.26/9.81 | | | | | | | REDUCE: (227), (269) imply: % 68.26/9.81 | | | | | | | (270) growth_rate(efficient_producers, all_19_0) = all_31_1 % 68.26/9.81 | | | | | | | % 68.26/9.81 | | | | | | | REDUCE: (235), (269) imply: % 68.26/9.81 | | | | | | | (271) growth_rate(first_movers, all_19_0) = all_106_0 % 68.26/9.81 | | | | | | | % 68.26/9.81 | | | | | | | BETA: splitting (50) gives: % 68.26/9.81 | | | | | | | % 68.26/9.81 | | | | | | | Case 1: % 68.26/9.81 | | | | | | | | % 68.26/9.81 | | | | | | | | (272) (all_40_0 = zero & all_40_1 = zero & % 68.26/9.81 | | | | | | | | growth_rate(efficient_producers, all_31_2) = zero & % 68.26/9.81 | | | | | | | | growth_rate(first_movers, all_31_2) = zero) | % 68.26/9.81 | | | | | | | | (equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.26/9.81 | | | | | | | | greater_or_equal(all_31_2, all_40_2)) % 68.26/9.81 | | | | | | | | % 68.26/9.81 | | | | | | | | BETA: splitting (272) gives: % 68.26/9.81 | | | | | | | | % 68.26/9.81 | | | | | | | | Case 1: % 68.26/9.81 | | | | | | | | | % 68.26/9.82 | | | | | | | | | (273) all_40_0 = zero & all_40_1 = zero & % 68.26/9.82 | | | | | | | | | growth_rate(efficient_producers, all_31_2) = zero & % 68.26/9.82 | | | | | | | | | growth_rate(first_movers, all_31_2) = zero % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | ALPHA: (273) implies: % 68.26/9.82 | | | | | | | | | (274) growth_rate(first_movers, all_31_2) = zero % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | REDUCE: (269), (274) imply: % 68.26/9.82 | | | | | | | | | (275) growth_rate(first_movers, all_19_0) = zero % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | GROUND_INST: instantiating (8) with zero, all_106_0, all_19_0, % 68.26/9.82 | | | | | | | | | first_movers, simplifying with (271), (275) gives: % 68.26/9.82 | | | | | | | | | (276) all_106_0 = zero % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | REDUCE: (239), (276) imply: % 68.26/9.82 | | | | | | | | | (277) $false % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | CLOSE: (277) is inconsistent. % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | Case 2: % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | (278) equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.26/9.82 | | | | | | | | | greater_or_equal(all_31_2, all_40_2) % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | ALPHA: (278) implies: % 68.26/9.82 | | | | | | | | | (279) ~ greater_or_equal(all_31_2, all_40_2) % 68.26/9.82 | | | | | | | | | (280) equilibrium(all_11_0) = all_40_2 % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | REDUCE: (269), (279) imply: % 68.26/9.82 | | | | | | | | | (281) ~ greater_or_equal(all_19_0, all_40_2) % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | REF_CLOSE: (7), (18), (21), (280), (281) are inconsistent by % 68.26/9.82 | | | | | | | | | sub-proof #9. % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | End of split % 68.26/9.82 | | | | | | | | % 68.26/9.82 | | | | | | | Case 2: % 68.26/9.82 | | | | | | | | % 68.26/9.82 | | | | | | | | (282) (growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.82 | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 68.26/9.82 | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_0, zero) % 68.26/9.82 | | | | | | | | & greater(zero, all_40_1)) | % 68.26/9.82 | | | | | | | | (growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.82 | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 68.26/9.82 | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_1, zero) % 68.26/9.82 | | | | | | | | & greater(zero, all_40_0)) % 68.26/9.82 | | | | | | | | % 68.26/9.82 | | | | | | | | BETA: splitting (282) gives: % 68.26/9.82 | | | | | | | | % 68.26/9.82 | | | | | | | | Case 1: % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | (283) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.82 | | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 68.26/9.82 | | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_0, zero) % 68.26/9.82 | | | | | | | | | & greater(zero, all_40_1) % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | ALPHA: (283) implies: % 68.26/9.82 | | | | | | | | | (284) greater(all_40_0, zero) % 68.26/9.82 | | | | | | | | | (285) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | REF_CLOSE: (8), (226), (227), (284), (285) are inconsistent by % 68.26/9.82 | | | | | | | | | sub-proof #12. % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | Case 2: % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | (286) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.82 | | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 68.26/9.82 | | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_1, zero) % 68.26/9.82 | | | | | | | | | & greater(zero, all_40_0) % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | ALPHA: (286) implies: % 68.26/9.82 | | | | | | | | | (287) greater(all_40_1, zero) % 68.26/9.82 | | | | | | | | | (288) $i(all_40_0) % 68.26/9.82 | | | | | | | | | (289) growth_rate(first_movers, all_31_2) = all_40_1 % 68.26/9.82 | | | | | | | | | (290) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | REDUCE: (269), (290) imply: % 68.26/9.82 | | | | | | | | | (291) growth_rate(efficient_producers, all_19_0) = all_40_0 % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | REDUCE: (269), (289) imply: % 68.26/9.82 | | | | | | | | | (292) growth_rate(first_movers, all_19_0) = all_40_1 % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | GROUND_INST: instantiating (8) with all_40_1, all_106_0, % 68.26/9.82 | | | | | | | | | all_19_0, first_movers, simplifying with (271), % 68.26/9.82 | | | | | | | | | (292) gives: % 68.26/9.82 | | | | | | | | | (293) all_106_0 = all_40_1 % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | GROUND_INST: instantiating (8) with all_31_1, all_40_0, % 68.26/9.82 | | | | | | | | | all_19_0, efficient_producers, simplifying with % 68.26/9.82 | | | | | | | | | (270), (291) gives: % 68.26/9.82 | | | | | | | | | (294) all_40_0 = all_31_1 % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | REDUCE: (234), (293) imply: % 68.26/9.82 | | | | | | | | | (295) $i(all_40_1) % 68.26/9.82 | | | | | | | | | % 68.26/9.82 | | | | | | | | | REDUCE: (288), (294) imply: % 68.26/9.83 | | | | | | | | | (296) $i(all_31_1) % 68.26/9.83 | | | | | | | | | % 68.26/9.83 | | | | | | | | | REDUCE: (238), (293) imply: % 68.26/9.83 | | | | | | | | | (297) greater(all_31_1, all_40_1) % 68.26/9.83 | | | | | | | | | % 68.26/9.83 | | | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with % 68.26/9.83 | | | | | | | | | all_31_1, all_40_1, zero, simplifying with (5), % 68.26/9.83 | | | | | | | | | (226), (287), (295), (296), (297) gives: % 68.26/9.83 | | | | | | | | | (298) $false % 68.26/9.83 | | | | | | | | | % 68.26/9.83 | | | | | | | | | CLOSE: (298) is inconsistent. % 68.26/9.83 | | | | | | | | | % 68.26/9.83 | | | | | | | | End of split % 68.26/9.83 | | | | | | | | % 68.26/9.83 | | | | | | | End of split % 68.26/9.83 | | | | | | | % 68.26/9.83 | | | | | | End of split % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | End of split % 68.26/9.83 | | | | | % 68.26/9.83 | | | | Case 2: % 68.26/9.83 | | | | | % 68.26/9.83 | | | | | (299) growth_rate(first_movers, all_31_2) = all_31_0 & $i(all_31_0) % 68.26/9.83 | | | | | & ~ greater(zero, all_31_0) % 68.26/9.83 | | | | | % 68.26/9.83 | | | | | ALPHA: (299) implies: % 68.26/9.83 | | | | | (300) ~ greater(zero, all_31_0) % 68.26/9.83 | | | | | (301) growth_rate(first_movers, all_31_2) = all_31_0 % 68.26/9.83 | | | | | % 68.26/9.83 | | | | | BETA: splitting (45) gives: % 68.26/9.83 | | | | | % 68.26/9.83 | | | | | Case 1: % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | (302) ~ greater_or_equal(all_31_2, all_21_0) % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | PRED_UNIFY: (36), (302) imply: % 68.26/9.83 | | | | | | (303) ~ (all_21_0 = all_19_0) % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | REF_CLOSE: (1), (20), (24), (38), (41), (224), (302), (303), % 68.26/9.83 | | | | | | (mp_greater_transitivity) are inconsistent by sub-proof % 68.26/9.83 | | | | | | #14. % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | Case 2: % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | (304) ? [v0: $i] : ? [v1: $i] : % 68.26/9.83 | | | | | | (growth_rate(efficient_producers, all_31_2) = v0 & % 68.26/9.83 | | | | | | growth_rate(first_movers, all_31_2) = v1 & $i(v1) & % 68.26/9.83 | | | | | | $i(v0) & greater(v0, v1)) % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | DELTA: instantiating (304) with fresh symbols all_106_0, all_106_1 % 68.26/9.83 | | | | | | gives: % 68.26/9.83 | | | | | | (305) growth_rate(efficient_producers, all_31_2) = all_106_1 & % 68.26/9.83 | | | | | | growth_rate(first_movers, all_31_2) = all_106_0 & % 68.26/9.83 | | | | | | $i(all_106_0) & $i(all_106_1) & greater(all_106_1, % 68.26/9.83 | | | | | | all_106_0) % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | ALPHA: (305) implies: % 68.26/9.83 | | | | | | (306) greater(all_106_1, all_106_0) % 68.26/9.83 | | | | | | (307) $i(all_106_1) % 68.26/9.83 | | | | | | (308) growth_rate(first_movers, all_31_2) = all_106_0 % 68.26/9.83 | | | | | | (309) growth_rate(efficient_producers, all_31_2) = all_106_1 % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | GROUND_INST: instantiating (8) with all_31_0, all_106_0, all_31_2, % 68.26/9.83 | | | | | | first_movers, simplifying with (301), (308) gives: % 68.26/9.83 | | | | | | (310) all_106_0 = all_31_0 % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | REDUCE: (306), (310) imply: % 68.26/9.83 | | | | | | (311) greater(all_106_1, all_31_0) % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | PRED_UNIFY: (300), (311) imply: % 68.26/9.83 | | | | | | (312) ~ (all_106_1 = zero) % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | BETA: splitting (41) gives: % 68.26/9.83 | | | | | | % 68.26/9.83 | | | | | | Case 1: % 68.26/9.83 | | | | | | | % 68.26/9.83 | | | | | | | (313) greater(all_31_2, all_19_0) % 68.26/9.83 | | | | | | | % 68.26/9.83 | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with % 68.26/9.83 | | | | | | | all_31_2, all_19_0, all_19_1, simplifying with (19), % 68.26/9.83 | | | | | | | (20), (38), (220), (313) gives: % 68.26/9.83 | | | | | | | (314) greater(all_31_2, all_19_1) % 68.26/9.83 | | | | | | | % 68.26/9.83 | | | | | | | BETA: splitting (52) gives: % 68.26/9.83 | | | | | | | % 68.26/9.83 | | | | | | | Case 1: % 68.26/9.83 | | | | | | | | % 68.26/9.83 | | | | | | | | % 68.26/9.83 | | | | | | | | GROUND_INST: instantiating (1) with all_31_2, all_19_1, % 68.26/9.83 | | | | | | | | simplifying with (19), (38), (314) gives: % 68.26/9.83 | | | | | | | | (315) greater_or_equal(all_31_2, all_19_1) % 68.26/9.83 | | | | | | | | % 68.26/9.83 | | | | | | | | DELTA: instantiating (304) with fresh symbols all_106_0, % 68.26/9.83 | | | | | | | | all_106_1 gives: % 68.26/9.83 | | | | | | | | (316) growth_rate(efficient_producers, all_31_2) = all_106_1 % 68.26/9.83 | | | | | | | | & growth_rate(first_movers, all_31_2) = all_106_0 & % 68.26/9.83 | | | | | | | | $i(all_106_0) & $i(all_106_1) & greater(all_106_1, % 68.26/9.83 | | | | | | | | all_106_0) % 68.26/9.83 | | | | | | | | % 68.26/9.83 | | | | | | | | REF_CLOSE: (5), (7), (8), (21), (50), (300), (301), (315), % 68.26/9.83 | | | | | | | | (316), (mp_greater_transitivity) are inconsistent by % 68.26/9.83 | | | | | | | | sub-proof #7. % 68.26/9.83 | | | | | | | | % 68.26/9.83 | | | | | | | Case 2: % 68.26/9.83 | | | | | | | | % 68.26/9.84 | | | | | | | | (317) all_38_0 = all_38_1 % 68.26/9.84 | | | | | | | | (318) growth_rate(first_movers, all_29_2) = all_38_1 % 68.26/9.84 | | | | | | | | % 68.26/9.84 | | | | | | | | COMBINE_EQS: (217), (317) imply: % 68.26/9.84 | | | | | | | | (319) all_38_1 = all_29_0 % 68.26/9.84 | | | | | | | | % 68.26/9.84 | | | | | | | | REDUCE: (219), (319) imply: % 68.26/9.84 | | | | | | | | (320) ~ (all_29_0 = zero) % 68.26/9.84 | | | | | | | | % 68.26/9.84 | | | | | | | | REDUCE: (49), (319) imply: % 68.26/9.84 | | | | | | | | (321) growth_rate(efficient_producers, all_29_2) = all_29_0 % 68.26/9.84 | | | | | | | | % 68.26/9.84 | | | | | | | | BETA: splitting (51) gives: % 68.26/9.84 | | | | | | | | % 68.26/9.84 | | | | | | | | Case 1: % 68.26/9.84 | | | | | | | | | % 68.26/9.84 | | | | | | | | | (322) (all_41_0 = zero & all_41_1 = zero & % 68.26/9.84 | | | | | | | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.26/9.84 | | | | | | | | | growth_rate(first_movers, all_29_2) = zero) | % 68.26/9.84 | | | | | | | | | (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.26/9.84 | | | | | | | | | greater_or_equal(all_29_2, all_41_2)) % 68.26/9.84 | | | | | | | | | % 68.26/9.84 | | | | | | | | | BETA: splitting (322) gives: % 68.26/9.84 | | | | | | | | | % 68.26/9.84 | | | | | | | | | Case 1: % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | (323) all_41_0 = zero & all_41_1 = zero & % 68.26/9.84 | | | | | | | | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.26/9.84 | | | | | | | | | | growth_rate(first_movers, all_29_2) = zero % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | ALPHA: (323) implies: % 68.26/9.84 | | | | | | | | | | (324) growth_rate(efficient_producers, all_29_2) = zero % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | REF_CLOSE: (8), (320), (321), (324) are inconsistent by % 68.26/9.84 | | | | | | | | | | sub-proof #2. % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | Case 2: % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | (325) equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & % 68.26/9.84 | | | | | | | | | | ~ greater_or_equal(all_29_2, all_41_2) % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | ALPHA: (325) implies: % 68.26/9.84 | | | | | | | | | | (326) $i(all_41_2) % 68.26/9.84 | | | | | | | | | | (327) equilibrium(all_11_0) = all_41_2 % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | GROUND_INST: instantiating (7) with all_19_1, all_41_2, % 68.26/9.84 | | | | | | | | | | all_11_0, simplifying with (21), (327) gives: % 68.26/9.84 | | | | | | | | | | (328) all_41_2 = all_19_1 % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | GROUND_INST: instantiating (1) with all_31_2, all_19_1, % 68.26/9.84 | | | | | | | | | | simplifying with (19), (38), (314) gives: % 68.26/9.84 | | | | | | | | | | (329) greater_or_equal(all_31_2, all_19_1) % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | DELTA: instantiating (304) with fresh symbols all_106_0, % 68.26/9.84 | | | | | | | | | | all_106_1 gives: % 68.26/9.84 | | | | | | | | | | (330) growth_rate(efficient_producers, all_31_2) = % 68.26/9.84 | | | | | | | | | | all_106_1 & growth_rate(first_movers, all_31_2) = % 68.26/9.84 | | | | | | | | | | all_106_0 & $i(all_106_0) & $i(all_106_1) & % 68.26/9.84 | | | | | | | | | | greater(all_106_1, all_106_0) % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | REF_CLOSE: (5), (7), (8), (21), (50), (300), (301), (329), % 68.26/9.84 | | | | | | | | | | (330), (mp_greater_transitivity) are inconsistent % 68.26/9.84 | | | | | | | | | | by sub-proof #7. % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | End of split % 68.26/9.84 | | | | | | | | | % 68.26/9.84 | | | | | | | | Case 2: % 68.26/9.84 | | | | | | | | | % 68.26/9.84 | | | | | | | | | (331) (growth_rate(efficient_producers, all_29_2) = % 68.26/9.84 | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 68.26/9.84 | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 68.26/9.84 | | | | | | | | | greater(all_41_0, zero) & greater(zero, all_41_1)) % 68.26/9.84 | | | | | | | | | | (growth_rate(efficient_producers, all_29_2) = % 68.26/9.84 | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 68.26/9.84 | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 68.26/9.84 | | | | | | | | | greater(all_41_1, zero) & greater(zero, all_41_0)) % 68.26/9.84 | | | | | | | | | % 68.26/9.84 | | | | | | | | | BETA: splitting (331) gives: % 68.26/9.84 | | | | | | | | | % 68.26/9.84 | | | | | | | | | Case 1: % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | (332) growth_rate(efficient_producers, all_29_2) = % 68.26/9.84 | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 68.26/9.84 | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 68.26/9.84 | | | | | | | | | | greater(all_41_0, zero) & greater(zero, all_41_1) % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | ALPHA: (332) implies: % 68.26/9.84 | | | | | | | | | | (333) greater(zero, all_41_1) % 68.26/9.84 | | | | | | | | | | (334) growth_rate(first_movers, all_29_2) = all_41_1 % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | REF_CLOSE: (8), (215), (216), (333), (334) are inconsistent % 68.26/9.84 | | | | | | | | | | by sub-proof #4. % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | Case 2: % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | (335) growth_rate(efficient_producers, all_29_2) = % 68.26/9.84 | | | | | | | | | | all_41_0 & growth_rate(first_movers, all_29_2) = % 68.26/9.84 | | | | | | | | | | all_41_1 & $i(all_41_0) & $i(all_41_1) & % 68.26/9.84 | | | | | | | | | | greater(all_41_1, zero) & greater(zero, all_41_0) % 68.26/9.84 | | | | | | | | | | % 68.26/9.84 | | | | | | | | | | ALPHA: (335) implies: % 68.26/9.84 | | | | | | | | | | (336) greater(zero, all_41_0) % 68.26/9.85 | | | | | | | | | | (337) growth_rate(efficient_producers, all_29_2) = % 68.26/9.85 | | | | | | | | | | all_41_0 % 68.26/9.85 | | | | | | | | | | % 68.26/9.85 | | | | | | | | | | REF_CLOSE: (8), (215), (321), (336), (337) are inconsistent % 68.26/9.85 | | | | | | | | | | by sub-proof #1. % 68.26/9.85 | | | | | | | | | | % 68.26/9.85 | | | | | | | | | End of split % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | End of split % 68.26/9.85 | | | | | | | | % 68.26/9.85 | | | | | | | End of split % 68.26/9.85 | | | | | | | % 68.26/9.85 | | | | | | Case 2: % 68.26/9.85 | | | | | | | % 68.26/9.85 | | | | | | | (338) all_31_2 = all_19_0 % 68.26/9.85 | | | | | | | % 68.26/9.85 | | | | | | | REDUCE: (309), (338) imply: % 68.26/9.85 | | | | | | | (339) growth_rate(efficient_producers, all_19_0) = all_106_1 % 68.26/9.85 | | | | | | | % 68.26/9.85 | | | | | | | REDUCE: (301), (338) imply: % 68.26/9.85 | | | | | | | (340) growth_rate(first_movers, all_19_0) = all_31_0 % 68.26/9.85 | | | | | | | % 68.26/9.85 | | | | | | | BETA: splitting (50) gives: % 68.26/9.85 | | | | | | | % 68.26/9.85 | | | | | | | Case 1: % 68.26/9.85 | | | | | | | | % 68.26/9.85 | | | | | | | | (341) (all_40_0 = zero & all_40_1 = zero & % 68.26/9.85 | | | | | | | | growth_rate(efficient_producers, all_31_2) = zero & % 68.26/9.85 | | | | | | | | growth_rate(first_movers, all_31_2) = zero) | % 68.26/9.85 | | | | | | | | (equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.26/9.85 | | | | | | | | greater_or_equal(all_31_2, all_40_2)) % 68.26/9.85 | | | | | | | | % 68.26/9.85 | | | | | | | | BETA: splitting (341) gives: % 68.26/9.85 | | | | | | | | % 68.26/9.85 | | | | | | | | Case 1: % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | (342) all_40_0 = zero & all_40_1 = zero & % 68.26/9.85 | | | | | | | | | growth_rate(efficient_producers, all_31_2) = zero & % 68.26/9.85 | | | | | | | | | growth_rate(first_movers, all_31_2) = zero % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | ALPHA: (342) implies: % 68.26/9.85 | | | | | | | | | (343) growth_rate(efficient_producers, all_31_2) = zero % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | REDUCE: (338), (343) imply: % 68.26/9.85 | | | | | | | | | (344) growth_rate(efficient_producers, all_19_0) = zero % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | GROUND_INST: instantiating (8) with zero, all_106_1, all_19_0, % 68.26/9.85 | | | | | | | | | efficient_producers, simplifying with (339), (344) % 68.26/9.85 | | | | | | | | | gives: % 68.26/9.85 | | | | | | | | | (345) all_106_1 = zero % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | REDUCE: (312), (345) imply: % 68.26/9.85 | | | | | | | | | (346) $false % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | CLOSE: (346) is inconsistent. % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | Case 2: % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | (347) equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.26/9.85 | | | | | | | | | greater_or_equal(all_31_2, all_40_2) % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | ALPHA: (347) implies: % 68.26/9.85 | | | | | | | | | (348) ~ greater_or_equal(all_31_2, all_40_2) % 68.26/9.85 | | | | | | | | | (349) equilibrium(all_11_0) = all_40_2 % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | REDUCE: (338), (348) imply: % 68.26/9.85 | | | | | | | | | (350) ~ greater_or_equal(all_19_0, all_40_2) % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | REF_CLOSE: (7), (18), (21), (349), (350) are inconsistent by % 68.26/9.85 | | | | | | | | | sub-proof #9. % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | End of split % 68.26/9.85 | | | | | | | | % 68.26/9.85 | | | | | | | Case 2: % 68.26/9.85 | | | | | | | | % 68.26/9.85 | | | | | | | | (351) (growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.85 | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 68.26/9.85 | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_0, zero) % 68.26/9.85 | | | | | | | | & greater(zero, all_40_1)) | % 68.26/9.85 | | | | | | | | (growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.85 | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 68.26/9.85 | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_1, zero) % 68.26/9.85 | | | | | | | | & greater(zero, all_40_0)) % 68.26/9.85 | | | | | | | | % 68.26/9.85 | | | | | | | | BETA: splitting (351) gives: % 68.26/9.85 | | | | | | | | % 68.26/9.85 | | | | | | | | Case 1: % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | (352) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.85 | | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 68.26/9.85 | | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_0, zero) % 68.26/9.85 | | | | | | | | | & greater(zero, all_40_1) % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | ALPHA: (352) implies: % 68.26/9.85 | | | | | | | | | (353) greater(zero, all_40_1) % 68.26/9.85 | | | | | | | | | (354) growth_rate(first_movers, all_31_2) = all_40_1 % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | REF_CLOSE: (8), (300), (301), (353), (354) are inconsistent by % 68.26/9.85 | | | | | | | | | sub-proof #8. % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | Case 2: % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | (355) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.85 | | | | | | | | | & growth_rate(first_movers, all_31_2) = all_40_1 & % 68.26/9.85 | | | | | | | | | $i(all_40_0) & $i(all_40_1) & greater(all_40_1, zero) % 68.26/9.85 | | | | | | | | | & greater(zero, all_40_0) % 68.26/9.85 | | | | | | | | | % 68.26/9.85 | | | | | | | | | ALPHA: (355) implies: % 68.26/9.85 | | | | | | | | | (356) greater(zero, all_40_0) % 68.26/9.85 | | | | | | | | | (357) $i(all_40_1) % 68.26/9.86 | | | | | | | | | (358) growth_rate(first_movers, all_31_2) = all_40_1 % 68.26/9.86 | | | | | | | | | (359) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.26/9.86 | | | | | | | | | % 68.26/9.86 | | | | | | | | | REDUCE: (338), (359) imply: % 68.26/9.86 | | | | | | | | | (360) growth_rate(efficient_producers, all_19_0) = all_40_0 % 68.26/9.86 | | | | | | | | | % 68.26/9.86 | | | | | | | | | REDUCE: (338), (358) imply: % 68.26/9.86 | | | | | | | | | (361) growth_rate(first_movers, all_19_0) = all_40_1 % 68.26/9.86 | | | | | | | | | % 68.26/9.86 | | | | | | | | | GROUND_INST: instantiating (8) with all_31_0, all_40_1, % 68.26/9.86 | | | | | | | | | all_19_0, first_movers, simplifying with (340), % 68.26/9.86 | | | | | | | | | (361) gives: % 68.26/9.86 | | | | | | | | | (362) all_40_1 = all_31_0 % 68.26/9.86 | | | | | | | | | % 68.26/9.86 | | | | | | | | | GROUND_INST: instantiating (8) with all_40_0, all_106_1, % 68.26/9.86 | | | | | | | | | all_19_0, efficient_producers, simplifying with % 68.26/9.86 | | | | | | | | | (339), (360) gives: % 68.26/9.86 | | | | | | | | | (363) all_106_1 = all_40_0 % 68.26/9.86 | | | | | | | | | % 68.26/9.86 | | | | | | | | | REDUCE: (307), (363) imply: % 68.26/9.86 | | | | | | | | | (364) $i(all_40_0) % 68.26/9.86 | | | | | | | | | % 68.26/9.86 | | | | | | | | | REDUCE: (357), (362) imply: % 68.26/9.86 | | | | | | | | | (365) $i(all_31_0) % 68.26/9.86 | | | | | | | | | % 68.26/9.86 | | | | | | | | | REDUCE: (311), (363) imply: % 68.26/9.86 | | | | | | | | | (366) greater(all_40_0, all_31_0) % 68.26/9.86 | | | | | | | | | % 68.26/9.86 | | | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with zero, % 68.26/9.86 | | | | | | | | | all_40_0, all_31_0, simplifying with (5), (300), % 68.26/9.86 | | | | | | | | | (356), (364), (365), (366) gives: % 68.26/9.86 | | | | | | | | | (367) $false % 68.26/9.86 | | | | | | | | | % 68.26/9.86 | | | | | | | | | CLOSE: (367) is inconsistent. % 68.26/9.86 | | | | | | | | | % 68.26/9.86 | | | | | | | | End of split % 68.26/9.86 | | | | | | | | % 68.26/9.86 | | | | | | | End of split % 68.26/9.86 | | | | | | | % 68.26/9.86 | | | | | | End of split % 68.26/9.86 | | | | | | % 68.26/9.86 | | | | | End of split % 68.26/9.86 | | | | | % 68.26/9.86 | | | | End of split % 68.26/9.86 | | | | % 68.26/9.86 | | | End of split % 68.26/9.86 | | | % 68.26/9.86 | | Case 2: % 68.26/9.86 | | | % 68.26/9.86 | | | (368) all_19_0 = all_19_1 % 68.26/9.86 | | | % 68.26/9.86 | | | REDUCE: (36), (368) imply: % 68.26/9.86 | | | (369) greater_or_equal(all_31_2, all_19_1) % 68.26/9.86 | | | % 68.26/9.86 | | | BETA: splitting (27) gives: % 68.26/9.86 | | | % 68.26/9.86 | | | Case 1: % 68.26/9.86 | | | | % 68.26/9.86 | | | | (370) greater(all_21_0, all_19_0) % 68.26/9.86 | | | | % 68.26/9.86 | | | | REDUCE: (368), (370) imply: % 68.26/9.86 | | | | (371) greater(all_21_0, all_19_1) % 68.26/9.86 | | | | % 68.26/9.86 | | | | REF_CLOSE: (1), (5), (7), (8), (19), (21), (24), (33), (40), (49), (51), % 68.26/9.86 | | | | (215), (216), (218), (219), (371), (mp_greater_transitivity) % 68.26/9.86 | | | | are inconsistent by sub-proof #3. % 68.26/9.86 | | | | % 68.26/9.86 | | | Case 2: % 68.26/9.86 | | | | % 68.26/9.86 | | | | (372) all_21_0 = all_19_0 | greater(all_19_0, all_21_0) % 68.26/9.86 | | | | % 68.26/9.86 | | | | REF_CLOSE: (1), (5), (7), (8), (19), (21), (24), (38), (39), (41), (45), % 68.26/9.86 | | | | (50), (368), (369), (372), (mp_greater_transitivity) are % 68.26/9.86 | | | | inconsistent by sub-proof #5. % 68.26/9.86 | | | | % 68.26/9.86 | | | End of split % 68.26/9.86 | | | % 68.26/9.86 | | End of split % 68.26/9.86 | | % 68.26/9.86 | End of split % 68.26/9.86 | % 68.26/9.86 End of proof % 68.26/9.86 % 68.26/9.86 Sub-proof #1 shows that the following formulas are inconsistent: % 68.26/9.86 ---------------------------------------------------------------- % 68.26/9.86 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.26/9.86 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.26/9.86 (2) growth_rate(efficient_producers, all_29_2) = all_29_0 % 68.26/9.86 (3) growth_rate(efficient_producers, all_29_2) = all_41_0 % 68.26/9.86 (4) ~ greater(zero, all_29_0) % 68.26/9.86 (5) greater(zero, all_41_0) % 68.26/9.86 % 68.26/9.86 Begin of proof % 68.26/9.86 | % 68.26/9.86 | PRED_UNIFY: (4), (5) imply: % 68.26/9.86 | (6) ~ (all_41_0 = all_29_0) % 68.26/9.86 | % 68.26/9.87 | GROUND_INST: instantiating (1) with all_29_0, all_41_0, all_29_2, % 68.26/9.87 | efficient_producers, simplifying with (2), (3) gives: % 68.26/9.87 | (7) all_41_0 = all_29_0 % 68.26/9.87 | % 68.26/9.87 | REDUCE: (6), (7) imply: % 68.26/9.87 | (8) $false % 68.26/9.87 | % 68.26/9.87 | CLOSE: (8) is inconsistent. % 68.26/9.87 | % 68.26/9.87 End of proof % 68.26/9.87 % 68.26/9.87 Sub-proof #2 shows that the following formulas are inconsistent: % 68.26/9.87 ---------------------------------------------------------------- % 68.26/9.87 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.26/9.87 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.26/9.87 (2) growth_rate(efficient_producers, all_29_2) = all_29_0 % 68.26/9.87 (3) growth_rate(efficient_producers, all_29_2) = zero % 68.26/9.87 (4) ~ (all_29_0 = zero) % 68.26/9.87 % 68.26/9.87 Begin of proof % 68.26/9.87 | % 68.26/9.87 | GROUND_INST: instantiating (1) with zero, all_29_0, all_29_2, % 68.26/9.87 | efficient_producers, simplifying with (2), (3) gives: % 68.26/9.87 | (5) all_29_0 = zero % 68.26/9.87 | % 68.26/9.87 | REDUCE: (4), (5) imply: % 68.26/9.87 | (6) $false % 68.26/9.87 | % 68.26/9.87 | CLOSE: (6) is inconsistent. % 68.26/9.87 | % 68.26/9.87 End of proof % 68.26/9.87 % 68.26/9.87 Sub-proof #3 shows that the following formulas are inconsistent: % 68.26/9.87 ---------------------------------------------------------------- % 68.26/9.87 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.26/9.87 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.26/9.87 (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 68.26/9.87 = v1) | ~ (equilibrium(v2) = v0)) % 68.26/9.87 (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 68.26/9.87 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 68.26/9.87 (4) $i(all_29_2) % 68.26/9.87 (5) growth_rate(efficient_producers, all_29_2) = all_38_1 % 68.26/9.87 (6) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 68.26/9.87 greater_or_equal(v0, v1)) % 68.26/9.87 (7) (all_41_0 = zero & all_41_1 = zero & growth_rate(efficient_producers, % 68.26/9.87 all_29_2) = zero & growth_rate(first_movers, all_29_2) = zero) | % 68.26/9.87 (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.26/9.87 greater_or_equal(all_29_2, all_41_2)) | % 68.26/9.87 (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.26/9.87 growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.26/9.87 $i(all_41_1) & greater(all_41_0, zero) & greater(zero, all_41_1)) | % 68.26/9.87 (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.26/9.87 growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.26/9.87 $i(all_41_1) & greater(all_41_1, zero) & greater(zero, all_41_0)) % 68.26/9.87 (8) $i(zero) % 68.26/9.87 (9) all_29_2 = all_21_0 | greater(all_29_2, all_21_0) % 68.26/9.87 (10) greater(all_21_0, all_19_1) % 68.26/9.87 (11) greater(all_38_1, all_29_0) % 68.26/9.87 (12) $i(all_19_1) % 68.26/9.87 (13) ~ greater(zero, all_29_0) % 68.26/9.87 (14) growth_rate(first_movers, all_29_2) = all_29_0 % 68.26/9.87 (15) $i(all_21_0) % 68.26/9.87 (16) equilibrium(all_11_0) = all_19_1 % 68.26/9.87 (17) ~ (all_38_1 = zero) % 68.26/9.87 % 68.26/9.87 Begin of proof % 68.26/9.87 | % 68.26/9.87 | GROUND_INST: instantiating (6) with all_21_0, all_19_1, simplifying with (10), % 68.26/9.87 | (12), (15) gives: % 68.26/9.87 | (18) greater_or_equal(all_21_0, all_19_1) % 68.26/9.87 | % 68.26/9.87 | BETA: splitting (9) gives: % 68.26/9.87 | % 68.26/9.87 | Case 1: % 68.26/9.87 | | % 68.26/9.87 | | (19) greater(all_29_2, all_21_0) % 68.26/9.87 | | % 68.26/9.88 | | GROUND_INST: instantiating (3) with all_29_2, all_21_0, all_19_1, % 68.26/9.88 | | simplifying with (4), (10), (12), (15), (19) gives: % 68.26/9.88 | | (20) greater(all_29_2, all_19_1) % 68.26/9.88 | | % 68.26/9.88 | | BETA: splitting (7) gives: % 68.26/9.88 | | % 68.26/9.88 | | Case 1: % 68.26/9.88 | | | % 68.26/9.88 | | | (21) (all_41_0 = zero & all_41_1 = zero & % 68.26/9.88 | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.26/9.88 | | | growth_rate(first_movers, all_29_2) = zero) | % 68.26/9.88 | | | (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.26/9.88 | | | greater_or_equal(all_29_2, all_41_2)) % 68.26/9.88 | | | % 68.26/9.88 | | | BETA: splitting (21) gives: % 68.26/9.88 | | | % 68.26/9.88 | | | Case 1: % 68.26/9.88 | | | | % 68.26/9.88 | | | | (22) all_41_0 = zero & all_41_1 = zero & % 68.26/9.88 | | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.26/9.88 | | | | growth_rate(first_movers, all_29_2) = zero % 68.26/9.88 | | | | % 68.26/9.88 | | | | ALPHA: (22) implies: % 68.26/9.88 | | | | (23) growth_rate(efficient_producers, all_29_2) = zero % 68.26/9.88 | | | | % 68.26/9.88 | | | | GROUND_INST: instantiating (1) with all_38_1, zero, all_29_2, % 68.26/9.88 | | | | efficient_producers, simplifying with (5), (23) gives: % 68.26/9.88 | | | | (24) all_38_1 = zero % 68.26/9.88 | | | | % 68.26/9.88 | | | | REDUCE: (17), (24) imply: % 68.26/9.88 | | | | (25) $false % 68.26/9.88 | | | | % 68.26/9.88 | | | | CLOSE: (25) is inconsistent. % 68.26/9.88 | | | | % 68.26/9.88 | | | Case 2: % 68.26/9.88 | | | | % 68.26/9.88 | | | | (26) equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.26/9.88 | | | | greater_or_equal(all_29_2, all_41_2) % 68.26/9.88 | | | | % 68.26/9.88 | | | | ALPHA: (26) implies: % 68.26/9.88 | | | | (27) ~ greater_or_equal(all_29_2, all_41_2) % 68.26/9.88 | | | | (28) $i(all_41_2) % 68.26/9.88 | | | | (29) equilibrium(all_11_0) = all_41_2 % 68.26/9.88 | | | | % 68.26/9.88 | | | | REF_CLOSE: (2), (4), (6), (16), (20), (27), (28), (29) are inconsistent % 68.26/9.88 | | | | by sub-proof #20. % 68.26/9.88 | | | | % 68.26/9.88 | | | End of split % 68.26/9.88 | | | % 68.26/9.88 | | Case 2: % 68.26/9.88 | | | % 68.26/9.88 | | | (30) (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.26/9.88 | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.26/9.88 | | | $i(all_41_1) & greater(all_41_0, zero) & greater(zero, % 68.26/9.88 | | | all_41_1)) | (growth_rate(efficient_producers, all_29_2) = % 68.26/9.88 | | | all_41_0 & growth_rate(first_movers, all_29_2) = all_41_1 & % 68.26/9.88 | | | $i(all_41_0) & $i(all_41_1) & greater(all_41_1, zero) & % 68.26/9.88 | | | greater(zero, all_41_0)) % 68.26/9.88 | | | % 68.26/9.88 | | | BETA: splitting (30) gives: % 68.26/9.88 | | | % 68.26/9.88 | | | Case 1: % 68.26/9.88 | | | | % 68.26/9.88 | | | | (31) growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.26/9.88 | | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.26/9.88 | | | | $i(all_41_1) & greater(all_41_0, zero) & greater(zero, all_41_1) % 68.26/9.88 | | | | % 68.26/9.88 | | | | ALPHA: (31) implies: % 68.26/9.88 | | | | (32) greater(zero, all_41_1) % 68.26/9.88 | | | | (33) growth_rate(first_movers, all_29_2) = all_41_1 % 68.26/9.88 | | | | % 68.26/9.88 | | | | REF_CLOSE: (1), (13), (14), (32), (33) are inconsistent by sub-proof #4. % 68.26/9.88 | | | | % 68.26/9.88 | | | Case 2: % 68.26/9.88 | | | | % 68.26/9.88 | | | | (34) growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.26/9.88 | | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.26/9.88 | | | | $i(all_41_1) & greater(all_41_1, zero) & greater(zero, all_41_0) % 68.26/9.88 | | | | % 68.26/9.88 | | | | ALPHA: (34) implies: % 68.26/9.88 | | | | (35) greater(zero, all_41_0) % 68.26/9.88 | | | | (36) $i(all_41_1) % 68.26/9.88 | | | | (37) $i(all_41_0) % 68.26/9.88 | | | | (38) growth_rate(first_movers, all_29_2) = all_41_1 % 68.26/9.88 | | | | (39) growth_rate(efficient_producers, all_29_2) = all_41_0 % 68.26/9.88 | | | | % 68.26/9.88 | | | | GROUND_INST: instantiating (1) with all_29_0, all_41_1, all_29_2, % 68.26/9.88 | | | | first_movers, simplifying with (14), (38) gives: % 68.26/9.88 | | | | (40) all_41_1 = all_29_0 % 68.26/9.88 | | | | % 68.26/9.88 | | | | GROUND_INST: instantiating (1) with all_38_1, all_41_0, all_29_2, % 68.26/9.88 | | | | efficient_producers, simplifying with (5), (39) gives: % 68.26/9.88 | | | | (41) all_41_0 = all_38_1 % 68.26/9.88 | | | | % 68.26/9.88 | | | | REDUCE: (37), (41) imply: % 68.26/9.88 | | | | (42) $i(all_38_1) % 68.26/9.88 | | | | % 68.26/9.89 | | | | REDUCE: (36), (40) imply: % 68.26/9.89 | | | | (43) $i(all_29_0) % 68.26/9.89 | | | | % 68.26/9.89 | | | | REDUCE: (35), (41) imply: % 68.26/9.89 | | | | (44) greater(zero, all_38_1) % 68.26/9.89 | | | | % 68.26/9.89 | | | | GROUND_INST: instantiating (3) with zero, all_38_1, all_29_0, % 68.26/9.89 | | | | simplifying with (8), (11), (13), (42), (43), (44) gives: % 68.26/9.89 | | | | (45) $false % 68.26/9.89 | | | | % 68.26/9.89 | | | | CLOSE: (45) is inconsistent. % 68.26/9.89 | | | | % 68.26/9.89 | | | End of split % 68.26/9.89 | | | % 68.26/9.89 | | End of split % 68.26/9.89 | | % 68.26/9.89 | Case 2: % 68.26/9.89 | | % 68.26/9.89 | | (46) all_29_2 = all_21_0 % 68.26/9.89 | | % 68.26/9.89 | | REDUCE: (5), (46) imply: % 68.26/9.89 | | (47) growth_rate(efficient_producers, all_21_0) = all_38_1 % 68.26/9.89 | | % 68.26/9.89 | | REDUCE: (14), (46) imply: % 68.26/9.89 | | (48) growth_rate(first_movers, all_21_0) = all_29_0 % 68.26/9.89 | | % 68.26/9.89 | | BETA: splitting (7) gives: % 68.26/9.89 | | % 68.26/9.89 | | Case 1: % 68.26/9.89 | | | % 68.26/9.89 | | | (49) (all_41_0 = zero & all_41_1 = zero & % 68.26/9.89 | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.26/9.89 | | | growth_rate(first_movers, all_29_2) = zero) | % 68.26/9.89 | | | (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.26/9.89 | | | greater_or_equal(all_29_2, all_41_2)) % 68.26/9.89 | | | % 68.26/9.89 | | | BETA: splitting (49) gives: % 68.26/9.89 | | | % 68.26/9.89 | | | Case 1: % 68.26/9.89 | | | | % 68.26/9.89 | | | | (50) all_41_0 = zero & all_41_1 = zero & % 68.26/9.89 | | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.26/9.89 | | | | growth_rate(first_movers, all_29_2) = zero % 68.26/9.89 | | | | % 68.26/9.89 | | | | ALPHA: (50) implies: % 68.26/9.89 | | | | (51) growth_rate(efficient_producers, all_29_2) = zero % 68.26/9.89 | | | | % 68.26/9.89 | | | | REDUCE: (46), (51) imply: % 68.26/9.89 | | | | (52) growth_rate(efficient_producers, all_21_0) = zero % 68.26/9.89 | | | | % 68.26/9.89 | | | | GROUND_INST: instantiating (1) with zero, all_38_1, all_21_0, % 68.26/9.89 | | | | efficient_producers, simplifying with (47), (52) gives: % 68.26/9.89 | | | | (53) all_38_1 = zero % 68.26/9.89 | | | | % 68.26/9.89 | | | | REDUCE: (17), (53) imply: % 68.26/9.89 | | | | (54) $false % 68.26/9.89 | | | | % 68.26/9.89 | | | | CLOSE: (54) is inconsistent. % 68.26/9.89 | | | | % 68.26/9.89 | | | Case 2: % 68.26/9.89 | | | | % 68.26/9.89 | | | | (55) equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.26/9.89 | | | | greater_or_equal(all_29_2, all_41_2) % 68.26/9.89 | | | | % 68.26/9.89 | | | | ALPHA: (55) implies: % 68.26/9.89 | | | | (56) ~ greater_or_equal(all_29_2, all_41_2) % 68.26/9.89 | | | | (57) equilibrium(all_11_0) = all_41_2 % 68.26/9.89 | | | | % 68.26/9.89 | | | | REDUCE: (46), (56) imply: % 68.26/9.89 | | | | (58) ~ greater_or_equal(all_21_0, all_41_2) % 68.26/9.89 | | | | % 68.26/9.89 | | | | REF_CLOSE: (2), (16), (18), (57), (58) are inconsistent by sub-proof % 68.26/9.89 | | | | #16. % 68.26/9.89 | | | | % 68.26/9.89 | | | End of split % 68.26/9.89 | | | % 68.26/9.89 | | Case 2: % 68.26/9.89 | | | % 68.26/9.89 | | | (59) (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.26/9.89 | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.26/9.89 | | | $i(all_41_1) & greater(all_41_0, zero) & greater(zero, % 68.26/9.89 | | | all_41_1)) | (growth_rate(efficient_producers, all_29_2) = % 68.26/9.89 | | | all_41_0 & growth_rate(first_movers, all_29_2) = all_41_1 & % 68.26/9.89 | | | $i(all_41_0) & $i(all_41_1) & greater(all_41_1, zero) & % 68.26/9.89 | | | greater(zero, all_41_0)) % 68.26/9.89 | | | % 68.26/9.89 | | | BETA: splitting (59) gives: % 68.26/9.89 | | | % 68.26/9.89 | | | Case 1: % 68.26/9.89 | | | | % 68.26/9.89 | | | | (60) growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.26/9.89 | | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.26/9.89 | | | | $i(all_41_1) & greater(all_41_0, zero) & greater(zero, all_41_1) % 68.26/9.89 | | | | % 68.26/9.89 | | | | ALPHA: (60) implies: % 68.26/9.89 | | | | (61) greater(zero, all_41_1) % 68.26/9.89 | | | | (62) growth_rate(first_movers, all_29_2) = all_41_1 % 68.26/9.89 | | | | % 68.26/9.89 | | | | REDUCE: (46), (62) imply: % 68.26/9.89 | | | | (63) growth_rate(first_movers, all_21_0) = all_41_1 % 68.26/9.89 | | | | % 68.26/9.89 | | | | PRED_UNIFY: (13), (61) imply: % 68.26/9.89 | | | | (64) ~ (all_41_1 = all_29_0) % 68.26/9.89 | | | | % 68.26/9.89 | | | | GROUND_INST: instantiating (1) with all_29_0, all_41_1, all_21_0, % 68.26/9.89 | | | | first_movers, simplifying with (48), (63) gives: % 68.26/9.89 | | | | (65) all_41_1 = all_29_0 % 68.26/9.89 | | | | % 68.26/9.89 | | | | REDUCE: (64), (65) imply: % 68.26/9.89 | | | | (66) $false % 68.26/9.89 | | | | % 68.26/9.89 | | | | CLOSE: (66) is inconsistent. % 68.26/9.89 | | | | % 68.26/9.89 | | | Case 2: % 68.26/9.89 | | | | % 68.26/9.90 | | | | (67) growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.26/9.90 | | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.26/9.90 | | | | $i(all_41_1) & greater(all_41_1, zero) & greater(zero, all_41_0) % 68.26/9.90 | | | | % 68.26/9.90 | | | | ALPHA: (67) implies: % 68.26/9.90 | | | | (68) greater(zero, all_41_0) % 68.26/9.90 | | | | (69) $i(all_41_1) % 68.26/9.90 | | | | (70) $i(all_41_0) % 68.26/9.90 | | | | (71) growth_rate(first_movers, all_29_2) = all_41_1 % 68.26/9.90 | | | | (72) growth_rate(efficient_producers, all_29_2) = all_41_0 % 68.26/9.90 | | | | % 68.70/9.90 | | | | REDUCE: (46), (72) imply: % 68.70/9.90 | | | | (73) growth_rate(efficient_producers, all_21_0) = all_41_0 % 68.70/9.90 | | | | % 68.70/9.90 | | | | REDUCE: (46), (71) imply: % 68.70/9.90 | | | | (74) growth_rate(first_movers, all_21_0) = all_41_1 % 68.70/9.90 | | | | % 68.70/9.90 | | | | GROUND_INST: instantiating (1) with all_29_0, all_41_1, all_21_0, % 68.70/9.90 | | | | first_movers, simplifying with (48), (74) gives: % 68.70/9.90 | | | | (75) all_41_1 = all_29_0 % 68.70/9.90 | | | | % 68.70/9.90 | | | | GROUND_INST: instantiating (1) with all_38_1, all_41_0, all_21_0, % 68.70/9.90 | | | | efficient_producers, simplifying with (47), (73) gives: % 68.70/9.90 | | | | (76) all_41_0 = all_38_1 % 68.70/9.90 | | | | % 68.70/9.90 | | | | REDUCE: (70), (76) imply: % 68.70/9.90 | | | | (77) $i(all_38_1) % 68.70/9.90 | | | | % 68.70/9.90 | | | | REDUCE: (69), (75) imply: % 68.70/9.90 | | | | (78) $i(all_29_0) % 68.70/9.90 | | | | % 68.70/9.90 | | | | REDUCE: (68), (76) imply: % 68.70/9.90 | | | | (79) greater(zero, all_38_1) % 68.70/9.90 | | | | % 68.70/9.90 | | | | GROUND_INST: instantiating (3) with zero, all_38_1, all_29_0, % 68.70/9.90 | | | | simplifying with (8), (11), (13), (77), (78), (79) gives: % 68.70/9.90 | | | | (80) $false % 68.70/9.90 | | | | % 68.70/9.90 | | | | CLOSE: (80) is inconsistent. % 68.70/9.90 | | | | % 68.70/9.90 | | | End of split % 68.70/9.90 | | | % 68.70/9.90 | | End of split % 68.70/9.90 | | % 68.70/9.90 | End of split % 68.70/9.90 | % 68.70/9.90 End of proof % 68.70/9.90 % 68.70/9.90 Sub-proof #4 shows that the following formulas are inconsistent: % 68.70/9.90 ---------------------------------------------------------------- % 68.70/9.90 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/9.90 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/9.90 (2) growth_rate(first_movers, all_29_2) = all_41_1 % 68.70/9.90 (3) greater(zero, all_41_1) % 68.70/9.90 (4) ~ greater(zero, all_29_0) % 68.70/9.90 (5) growth_rate(first_movers, all_29_2) = all_29_0 % 68.70/9.90 % 68.70/9.90 Begin of proof % 68.70/9.90 | % 68.70/9.90 | PRED_UNIFY: (3), (4) imply: % 68.70/9.90 | (6) ~ (all_41_1 = all_29_0) % 68.70/9.90 | % 68.70/9.90 | GROUND_INST: instantiating (1) with all_29_0, all_41_1, all_29_2, % 68.70/9.90 | first_movers, simplifying with (2), (5) gives: % 68.70/9.90 | (7) all_41_1 = all_29_0 % 68.70/9.90 | % 68.70/9.90 | REDUCE: (6), (7) imply: % 68.70/9.90 | (8) $false % 68.70/9.90 | % 68.70/9.90 | CLOSE: (8) is inconsistent. % 68.70/9.90 | % 68.70/9.90 End of proof % 68.70/9.90 % 68.70/9.90 Sub-proof #5 shows that the following formulas are inconsistent: % 68.70/9.90 ---------------------------------------------------------------- % 68.70/9.90 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/9.90 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/9.90 (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 68.70/9.90 = v1) | ~ (equilibrium(v2) = v0)) % 68.70/9.90 (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 68.70/9.90 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 68.70/9.90 (4) ~ greater_or_equal(all_31_2, all_21_0) | ? [v0: $i] : ? [v1: $i] : % 68.70/9.90 (growth_rate(efficient_producers, all_31_2) = v0 & % 68.70/9.90 growth_rate(first_movers, all_31_2) = v1 & $i(v1) & $i(v0) & % 68.70/9.90 greater(v0, v1)) % 68.70/9.90 (5) all_21_0 = all_19_0 | greater(all_19_0, all_21_0) % 68.70/9.91 (6) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 68.70/9.91 greater_or_equal(v0, v1)) % 68.70/9.91 (7) (all_40_0 = zero & all_40_1 = zero & growth_rate(efficient_producers, % 68.70/9.91 all_31_2) = zero & growth_rate(first_movers, all_31_2) = zero) | % 68.70/9.91 (equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.70/9.91 greater_or_equal(all_31_2, all_40_2)) | % 68.70/9.91 (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.91 growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.91 $i(all_40_1) & greater(all_40_0, zero) & greater(zero, all_40_1)) | % 68.70/9.91 (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.91 growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.91 $i(all_40_1) & greater(all_40_1, zero) & greater(zero, all_40_0)) % 68.70/9.91 (8) $i(zero) % 68.70/9.91 (9) all_31_2 = all_19_0 | greater(all_31_2, all_19_0) % 68.70/9.91 (10) $i(all_31_2) % 68.70/9.91 (11) all_19_0 = all_19_1 % 68.70/9.91 (12) (growth_rate(efficient_producers, all_31_2) = all_31_1 & $i(all_31_1) & % 68.70/9.91 ~ greater(all_31_1, zero)) | (growth_rate(first_movers, all_31_2) = % 68.70/9.91 all_31_0 & $i(all_31_0) & ~ greater(zero, all_31_0)) % 68.70/9.91 (13) $i(all_19_1) % 68.70/9.91 (14) $i(all_21_0) % 68.70/9.91 (15) equilibrium(all_11_0) = all_19_1 % 68.70/9.91 (16) greater_or_equal(all_31_2, all_19_1) % 68.70/9.91 % 68.70/9.91 Begin of proof % 68.70/9.91 | % 68.70/9.91 | BETA: splitting (12) gives: % 68.70/9.91 | % 68.70/9.91 | Case 1: % 68.70/9.91 | | % 68.70/9.91 | | (17) growth_rate(efficient_producers, all_31_2) = all_31_1 & $i(all_31_1) % 68.70/9.91 | | & ~ greater(all_31_1, zero) % 68.70/9.91 | | % 68.70/9.91 | | ALPHA: (17) implies: % 68.70/9.91 | | (18) ~ greater(all_31_1, zero) % 68.70/9.91 | | (19) growth_rate(efficient_producers, all_31_2) = all_31_1 % 68.70/9.91 | | % 68.70/9.91 | | BETA: splitting (4) gives: % 68.70/9.91 | | % 68.70/9.91 | | Case 1: % 68.70/9.91 | | | % 68.70/9.91 | | | (20) ~ greater_or_equal(all_31_2, all_21_0) % 68.70/9.91 | | | % 68.70/9.91 | | | PRED_UNIFY: (16), (20) imply: % 68.70/9.91 | | | (21) ~ (all_21_0 = all_19_1) % 68.70/9.91 | | | % 68.70/9.91 | | | REF_CLOSE: (3), (5), (6), (9), (10), (11), (13), (14), (20), (21) are % 68.70/9.91 | | | inconsistent by sub-proof #6. % 68.70/9.91 | | | % 68.70/9.91 | | Case 2: % 68.70/9.91 | | | % 68.70/9.91 | | | (22) ? [v0: $i] : ? [v1: $i] : (growth_rate(efficient_producers, % 68.70/9.91 | | | all_31_2) = v0 & growth_rate(first_movers, all_31_2) = v1 & % 68.70/9.91 | | | $i(v1) & $i(v0) & greater(v0, v1)) % 68.70/9.91 | | | % 68.70/9.91 | | | DELTA: instantiating (22) with fresh symbols all_106_0, all_106_1 gives: % 68.70/9.91 | | | (23) growth_rate(efficient_producers, all_31_2) = all_106_1 & % 68.70/9.91 | | | growth_rate(first_movers, all_31_2) = all_106_0 & $i(all_106_0) & % 68.70/9.91 | | | $i(all_106_1) & greater(all_106_1, all_106_0) % 68.70/9.91 | | | % 68.70/9.91 | | | REF_CLOSE: (1), (2), (3), (7), (8), (15), (16), (18), (19), (23) are % 68.70/9.91 | | | inconsistent by sub-proof #11. % 68.70/9.91 | | | % 68.70/9.91 | | End of split % 68.70/9.91 | | % 68.70/9.91 | Case 2: % 68.70/9.91 | | % 68.70/9.91 | | (24) growth_rate(first_movers, all_31_2) = all_31_0 & $i(all_31_0) & ~ % 68.70/9.91 | | greater(zero, all_31_0) % 68.70/9.91 | | % 68.70/9.91 | | ALPHA: (24) implies: % 68.70/9.91 | | (25) ~ greater(zero, all_31_0) % 68.70/9.91 | | (26) growth_rate(first_movers, all_31_2) = all_31_0 % 68.70/9.91 | | % 68.70/9.91 | | BETA: splitting (4) gives: % 68.70/9.91 | | % 68.70/9.91 | | Case 1: % 68.70/9.91 | | | % 68.70/9.91 | | | (27) ~ greater_or_equal(all_31_2, all_21_0) % 68.70/9.91 | | | % 68.70/9.91 | | | PRED_UNIFY: (16), (27) imply: % 68.70/9.91 | | | (28) ~ (all_21_0 = all_19_1) % 68.70/9.91 | | | % 68.70/9.91 | | | REF_CLOSE: (3), (5), (6), (9), (10), (11), (13), (14), (27), (28) are % 68.70/9.91 | | | inconsistent by sub-proof #6. % 68.70/9.91 | | | % 68.70/9.91 | | Case 2: % 68.70/9.91 | | | % 68.70/9.91 | | | (29) ? [v0: $i] : ? [v1: $i] : (growth_rate(efficient_producers, % 68.70/9.91 | | | all_31_2) = v0 & growth_rate(first_movers, all_31_2) = v1 & % 68.70/9.91 | | | $i(v1) & $i(v0) & greater(v0, v1)) % 68.70/9.91 | | | % 68.70/9.91 | | | DELTA: instantiating (29) with fresh symbols all_106_0, all_106_1 gives: % 68.70/9.92 | | | (30) growth_rate(efficient_producers, all_31_2) = all_106_1 & % 68.70/9.92 | | | growth_rate(first_movers, all_31_2) = all_106_0 & $i(all_106_0) & % 68.70/9.92 | | | $i(all_106_1) & greater(all_106_1, all_106_0) % 68.70/9.92 | | | % 68.70/9.92 | | | REF_CLOSE: (1), (2), (3), (7), (8), (15), (16), (25), (26), (30) are % 68.70/9.92 | | | inconsistent by sub-proof #7. % 68.70/9.92 | | | % 68.70/9.92 | | End of split % 68.70/9.92 | | % 68.70/9.92 | End of split % 68.70/9.92 | % 68.70/9.92 End of proof % 68.70/9.92 % 68.70/9.92 Sub-proof #6 shows that the following formulas are inconsistent: % 68.70/9.92 ---------------------------------------------------------------- % 68.70/9.92 (1) ~ greater_or_equal(all_31_2, all_21_0) % 68.70/9.92 (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 68.70/9.92 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 68.70/9.92 (3) all_21_0 = all_19_0 | greater(all_19_0, all_21_0) % 68.70/9.92 (4) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 68.70/9.92 greater_or_equal(v0, v1)) % 68.70/9.92 (5) ~ (all_21_0 = all_19_1) % 68.70/9.92 (6) all_31_2 = all_19_0 | greater(all_31_2, all_19_0) % 68.70/9.92 (7) $i(all_31_2) % 68.70/9.92 (8) all_19_0 = all_19_1 % 68.70/9.92 (9) $i(all_19_1) % 68.70/9.92 (10) $i(all_21_0) % 68.70/9.92 % 68.70/9.92 Begin of proof % 68.70/9.92 | % 68.70/9.92 | BETA: splitting (3) gives: % 68.70/9.92 | % 68.70/9.92 | Case 1: % 68.70/9.92 | | % 68.70/9.92 | | (11) greater(all_19_0, all_21_0) % 68.70/9.92 | | % 68.70/9.92 | | REDUCE: (8), (11) imply: % 68.70/9.92 | | (12) greater(all_19_1, all_21_0) % 68.70/9.92 | | % 68.70/9.92 | | GROUND_INST: instantiating (4) with all_19_1, all_21_0, simplifying with % 68.70/9.92 | | (9), (10), (12) gives: % 68.70/9.92 | | (13) greater_or_equal(all_19_1, all_21_0) % 68.70/9.92 | | % 68.70/9.92 | | PRED_UNIFY: (1), (13) imply: % 68.70/9.92 | | (14) ~ (all_31_2 = all_19_1) % 68.70/9.92 | | % 68.70/9.92 | | BETA: splitting (6) gives: % 68.70/9.92 | | % 68.70/9.92 | | Case 1: % 68.70/9.92 | | | % 68.70/9.92 | | | (15) greater(all_31_2, all_19_0) % 68.70/9.92 | | | % 68.70/9.92 | | | REDUCE: (8), (15) imply: % 68.70/9.92 | | | (16) greater(all_31_2, all_19_1) % 68.70/9.92 | | | % 68.70/9.92 | | | GROUND_INST: instantiating (2) with all_31_2, all_19_1, all_21_0, % 68.70/9.92 | | | simplifying with (7), (9), (10), (12), (16) gives: % 68.70/9.92 | | | (17) greater(all_31_2, all_21_0) % 68.70/9.92 | | | % 68.70/9.92 | | | GROUND_INST: instantiating (4) with all_31_2, all_21_0, simplifying with % 68.70/9.92 | | | (1), (7), (10), (17) gives: % 68.70/9.92 | | | (18) $false % 68.70/9.92 | | | % 68.70/9.92 | | | CLOSE: (18) is inconsistent. % 68.70/9.92 | | | % 68.70/9.92 | | Case 2: % 68.70/9.92 | | | % 68.70/9.92 | | | (19) all_31_2 = all_19_0 % 68.70/9.92 | | | % 68.70/9.92 | | | COMBINE_EQS: (8), (19) imply: % 68.70/9.92 | | | (20) all_31_2 = all_19_1 % 68.70/9.92 | | | % 68.70/9.92 | | | REDUCE: (14), (20) imply: % 68.70/9.92 | | | (21) $false % 68.70/9.92 | | | % 68.70/9.92 | | | CLOSE: (21) is inconsistent. % 68.70/9.92 | | | % 68.70/9.92 | | End of split % 68.70/9.92 | | % 68.70/9.92 | Case 2: % 68.70/9.92 | | % 68.70/9.92 | | (22) all_21_0 = all_19_0 % 68.70/9.92 | | % 68.70/9.92 | | COMBINE_EQS: (8), (22) imply: % 68.70/9.92 | | (23) all_21_0 = all_19_1 % 68.70/9.92 | | % 68.70/9.92 | | REDUCE: (5), (23) imply: % 68.70/9.92 | | (24) $false % 68.70/9.92 | | % 68.70/9.92 | | CLOSE: (24) is inconsistent. % 68.70/9.92 | | % 68.70/9.92 | End of split % 68.70/9.92 | % 68.70/9.92 End of proof % 68.70/9.92 % 68.70/9.92 Sub-proof #7 shows that the following formulas are inconsistent: % 68.70/9.92 ---------------------------------------------------------------- % 68.70/9.92 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/9.92 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/9.92 (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 68.70/9.92 = v1) | ~ (equilibrium(v2) = v0)) % 68.70/9.92 (3) ~ greater(zero, all_31_0) % 68.70/9.92 (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 68.70/9.92 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 68.70/9.93 (5) (all_40_0 = zero & all_40_1 = zero & growth_rate(efficient_producers, % 68.70/9.93 all_31_2) = zero & growth_rate(first_movers, all_31_2) = zero) | % 68.70/9.93 (equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.70/9.93 greater_or_equal(all_31_2, all_40_2)) | % 68.70/9.93 (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.93 growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.93 $i(all_40_1) & greater(all_40_0, zero) & greater(zero, all_40_1)) | % 68.70/9.93 (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.93 growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.93 $i(all_40_1) & greater(all_40_1, zero) & greater(zero, all_40_0)) % 68.70/9.93 (6) $i(zero) % 68.70/9.93 (7) growth_rate(first_movers, all_31_2) = all_31_0 % 68.70/9.93 (8) growth_rate(efficient_producers, all_31_2) = all_106_1 & % 68.70/9.93 growth_rate(first_movers, all_31_2) = all_106_0 & $i(all_106_0) & % 68.70/9.93 $i(all_106_1) & greater(all_106_1, all_106_0) % 68.70/9.93 (9) equilibrium(all_11_0) = all_19_1 % 68.70/9.93 (10) greater_or_equal(all_31_2, all_19_1) % 68.70/9.93 % 68.70/9.93 Begin of proof % 68.70/9.93 | % 68.70/9.93 | ALPHA: (8) implies: % 68.70/9.93 | (11) greater(all_106_1, all_106_0) % 68.70/9.93 | (12) $i(all_106_1) % 68.70/9.93 | (13) growth_rate(first_movers, all_31_2) = all_106_0 % 68.70/9.93 | (14) growth_rate(efficient_producers, all_31_2) = all_106_1 % 68.70/9.93 | % 68.70/9.93 | GROUND_INST: instantiating (1) with all_31_0, all_106_0, all_31_2, % 68.70/9.93 | first_movers, simplifying with (7), (13) gives: % 68.70/9.93 | (15) all_106_0 = all_31_0 % 68.70/9.93 | % 68.70/9.93 | REDUCE: (11), (15) imply: % 68.70/9.93 | (16) greater(all_106_1, all_31_0) % 68.70/9.93 | % 68.70/9.93 | PRED_UNIFY: (3), (16) imply: % 68.70/9.93 | (17) ~ (all_106_1 = zero) % 68.70/9.93 | % 68.70/9.93 | BETA: splitting (5) gives: % 68.70/9.93 | % 68.70/9.93 | Case 1: % 68.70/9.93 | | % 68.70/9.93 | | (18) (all_40_0 = zero & all_40_1 = zero & % 68.70/9.93 | | growth_rate(efficient_producers, all_31_2) = zero & % 68.70/9.93 | | growth_rate(first_movers, all_31_2) = zero) | % 68.70/9.93 | | (equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.70/9.93 | | greater_or_equal(all_31_2, all_40_2)) % 68.70/9.93 | | % 68.70/9.93 | | BETA: splitting (18) gives: % 68.70/9.93 | | % 68.70/9.93 | | Case 1: % 68.70/9.93 | | | % 68.70/9.93 | | | (19) all_40_0 = zero & all_40_1 = zero & % 68.70/9.93 | | | growth_rate(efficient_producers, all_31_2) = zero & % 68.70/9.93 | | | growth_rate(first_movers, all_31_2) = zero % 68.70/9.93 | | | % 68.70/9.93 | | | ALPHA: (19) implies: % 68.70/9.93 | | | (20) growth_rate(efficient_producers, all_31_2) = zero % 68.70/9.93 | | | % 68.70/9.93 | | | GROUND_INST: instantiating (1) with all_106_1, zero, all_31_2, % 68.70/9.93 | | | efficient_producers, simplifying with (14), (20) gives: % 68.70/9.93 | | | (21) all_106_1 = zero % 68.70/9.93 | | | % 68.70/9.93 | | | REDUCE: (17), (21) imply: % 68.70/9.93 | | | (22) $false % 68.70/9.93 | | | % 68.70/9.93 | | | CLOSE: (22) is inconsistent. % 68.70/9.93 | | | % 68.70/9.93 | | Case 2: % 68.70/9.93 | | | % 68.70/9.93 | | | (23) equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.70/9.93 | | | greater_or_equal(all_31_2, all_40_2) % 68.70/9.93 | | | % 68.70/9.93 | | | ALPHA: (23) implies: % 68.70/9.93 | | | (24) ~ greater_or_equal(all_31_2, all_40_2) % 68.70/9.93 | | | (25) equilibrium(all_11_0) = all_40_2 % 68.70/9.93 | | | % 68.70/9.93 | | | REF_CLOSE: (2), (9), (10), (24), (25) are inconsistent by sub-proof #13. % 68.70/9.93 | | | % 68.70/9.93 | | End of split % 68.70/9.93 | | % 68.70/9.93 | Case 2: % 68.70/9.93 | | % 68.70/9.93 | | (26) (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.93 | | growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.93 | | $i(all_40_1) & greater(all_40_0, zero) & greater(zero, all_40_1)) % 68.70/9.93 | | | (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.93 | | growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.93 | | $i(all_40_1) & greater(all_40_1, zero) & greater(zero, all_40_0)) % 68.70/9.93 | | % 68.70/9.93 | | BETA: splitting (26) gives: % 68.70/9.93 | | % 68.70/9.93 | | Case 1: % 68.70/9.93 | | | % 68.70/9.93 | | | (27) growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.93 | | | growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.93 | | | $i(all_40_1) & greater(all_40_0, zero) & greater(zero, all_40_1) % 68.70/9.93 | | | % 68.70/9.93 | | | ALPHA: (27) implies: % 68.70/9.93 | | | (28) greater(zero, all_40_1) % 68.70/9.93 | | | (29) growth_rate(first_movers, all_31_2) = all_40_1 % 68.70/9.93 | | | % 68.70/9.93 | | | REF_CLOSE: (1), (3), (7), (28), (29) are inconsistent by sub-proof #8. % 68.70/9.93 | | | % 68.70/9.93 | | Case 2: % 68.70/9.93 | | | % 68.70/9.93 | | | (30) growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.93 | | | growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.93 | | | $i(all_40_1) & greater(all_40_1, zero) & greater(zero, all_40_0) % 68.70/9.93 | | | % 68.70/9.93 | | | ALPHA: (30) implies: % 68.70/9.93 | | | (31) greater(zero, all_40_0) % 68.70/9.93 | | | (32) $i(all_40_1) % 68.70/9.93 | | | (33) growth_rate(first_movers, all_31_2) = all_40_1 % 68.70/9.93 | | | (34) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.70/9.93 | | | % 68.70/9.94 | | | GROUND_INST: instantiating (1) with all_31_0, all_40_1, all_31_2, % 68.70/9.94 | | | first_movers, simplifying with (7), (33) gives: % 68.70/9.94 | | | (35) all_40_1 = all_31_0 % 68.70/9.94 | | | % 68.70/9.94 | | | GROUND_INST: instantiating (1) with all_106_1, all_40_0, all_31_2, % 68.70/9.94 | | | efficient_producers, simplifying with (14), (34) gives: % 68.70/9.94 | | | (36) all_106_1 = all_40_0 % 68.70/9.94 | | | % 68.70/9.94 | | | REDUCE: (12), (36) imply: % 68.70/9.94 | | | (37) $i(all_40_0) % 68.70/9.94 | | | % 68.70/9.94 | | | REDUCE: (32), (35) imply: % 68.70/9.94 | | | (38) $i(all_31_0) % 68.70/9.94 | | | % 68.70/9.94 | | | REDUCE: (16), (36) imply: % 68.70/9.94 | | | (39) greater(all_40_0, all_31_0) % 68.70/9.94 | | | % 68.70/9.94 | | | GROUND_INST: instantiating (4) with zero, all_40_0, all_31_0, simplifying % 68.70/9.94 | | | with (3), (6), (31), (37), (38), (39) gives: % 68.70/9.94 | | | (40) $false % 68.70/9.94 | | | % 68.70/9.94 | | | CLOSE: (40) is inconsistent. % 68.70/9.94 | | | % 68.70/9.94 | | End of split % 68.70/9.94 | | % 68.70/9.94 | End of split % 68.70/9.94 | % 68.70/9.94 End of proof % 68.70/9.94 % 68.70/9.94 Sub-proof #8 shows that the following formulas are inconsistent: % 68.70/9.94 ---------------------------------------------------------------- % 68.70/9.94 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/9.94 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/9.94 (2) ~ greater(zero, all_31_0) % 68.70/9.94 (3) growth_rate(first_movers, all_31_2) = all_31_0 % 68.70/9.94 (4) growth_rate(first_movers, all_31_2) = all_40_1 % 68.70/9.94 (5) greater(zero, all_40_1) % 68.70/9.94 % 68.70/9.94 Begin of proof % 68.70/9.94 | % 68.70/9.94 | PRED_UNIFY: (2), (5) imply: % 68.70/9.94 | (6) ~ (all_40_1 = all_31_0) % 68.70/9.94 | % 68.70/9.94 | GROUND_INST: instantiating (1) with all_31_0, all_40_1, all_31_2, % 68.70/9.94 | first_movers, simplifying with (3), (4) gives: % 68.70/9.94 | (7) all_40_1 = all_31_0 % 68.70/9.94 | % 68.70/9.94 | REDUCE: (6), (7) imply: % 68.70/9.94 | (8) $false % 68.70/9.94 | % 68.70/9.94 | CLOSE: (8) is inconsistent. % 68.70/9.94 | % 68.70/9.94 End of proof % 68.70/9.94 % 68.70/9.94 Sub-proof #9 shows that the following formulas are inconsistent: % 68.70/9.94 ---------------------------------------------------------------- % 68.70/9.94 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 68.70/9.94 = v1) | ~ (equilibrium(v2) = v0)) % 68.70/9.94 (2) equilibrium(all_11_0) = all_40_2 % 68.70/9.94 (3) greater_or_equal(all_19_0, all_19_1) % 68.70/9.94 (4) ~ greater_or_equal(all_19_0, all_40_2) % 68.70/9.94 (5) equilibrium(all_11_0) = all_19_1 % 68.70/9.94 % 68.70/9.94 Begin of proof % 68.70/9.94 | % 68.70/9.94 | GROUND_INST: instantiating (1) with all_19_1, all_40_2, all_11_0, simplifying % 68.70/9.94 | with (2), (5) gives: % 68.70/9.94 | (6) all_40_2 = all_19_1 % 68.70/9.94 | % 68.70/9.94 | PRED_UNIFY: (3), (4) imply: % 68.70/9.94 | (7) ~ (all_40_2 = all_19_1) % 68.70/9.94 | % 68.70/9.94 | REDUCE: (6), (7) imply: % 68.70/9.94 | (8) $false % 68.70/9.94 | % 68.70/9.94 | CLOSE: (8) is inconsistent. % 68.70/9.94 | % 68.70/9.94 End of proof % 68.70/9.94 % 68.70/9.94 Sub-proof #10 shows that the following formulas are inconsistent: % 68.70/9.94 ---------------------------------------------------------------- % 68.70/9.94 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/9.94 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/9.94 (2) growth_rate(efficient_producers, all_29_2) = all_29_1 % 68.70/9.94 (3) growth_rate(efficient_producers, all_29_2) = zero % 68.70/9.94 (4) ~ (all_29_1 = zero) % 68.70/9.94 % 68.70/9.94 Begin of proof % 68.70/9.94 | % 68.70/9.94 | GROUND_INST: instantiating (1) with all_29_1, zero, all_29_2, % 68.70/9.94 | efficient_producers, simplifying with (2), (3) gives: % 68.70/9.94 | (5) all_29_1 = zero % 68.70/9.94 | % 68.70/9.94 | REDUCE: (4), (5) imply: % 68.70/9.94 | (6) $false % 68.70/9.94 | % 68.70/9.94 | CLOSE: (6) is inconsistent. % 68.70/9.94 | % 68.70/9.94 End of proof % 68.70/9.94 % 68.70/9.94 Sub-proof #11 shows that the following formulas are inconsistent: % 68.70/9.94 ---------------------------------------------------------------- % 68.70/9.94 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/9.94 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/9.94 (2) ~ greater(all_31_1, zero) % 68.70/9.94 (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 68.70/9.94 = v1) | ~ (equilibrium(v2) = v0)) % 68.70/9.94 (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 68.70/9.94 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 68.70/9.95 (5) (all_40_0 = zero & all_40_1 = zero & growth_rate(efficient_producers, % 68.70/9.95 all_31_2) = zero & growth_rate(first_movers, all_31_2) = zero) | % 68.70/9.95 (equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.70/9.95 greater_or_equal(all_31_2, all_40_2)) | % 68.70/9.95 (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.95 growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.95 $i(all_40_1) & greater(all_40_0, zero) & greater(zero, all_40_1)) | % 68.70/9.95 (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.95 growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.95 $i(all_40_1) & greater(all_40_1, zero) & greater(zero, all_40_0)) % 68.70/9.95 (6) $i(zero) % 68.70/9.95 (7) growth_rate(efficient_producers, all_31_2) = all_31_1 % 68.70/9.95 (8) equilibrium(all_11_0) = all_19_1 % 68.70/9.95 (9) growth_rate(efficient_producers, all_31_2) = all_106_1 & % 68.70/9.95 growth_rate(first_movers, all_31_2) = all_106_0 & $i(all_106_0) & % 68.70/9.95 $i(all_106_1) & greater(all_106_1, all_106_0) % 68.70/9.95 (10) greater_or_equal(all_31_2, all_19_1) % 68.70/9.95 % 68.70/9.95 Begin of proof % 68.70/9.95 | % 68.70/9.95 | ALPHA: (9) implies: % 68.70/9.95 | (11) greater(all_106_1, all_106_0) % 68.70/9.95 | (12) $i(all_106_0) % 68.70/9.95 | (13) growth_rate(first_movers, all_31_2) = all_106_0 % 68.70/9.95 | (14) growth_rate(efficient_producers, all_31_2) = all_106_1 % 68.70/9.95 | % 68.70/9.95 | GROUND_INST: instantiating (1) with all_31_1, all_106_1, all_31_2, % 68.70/9.95 | efficient_producers, simplifying with (7), (14) gives: % 68.70/9.95 | (15) all_106_1 = all_31_1 % 68.70/9.95 | % 68.70/9.95 | REDUCE: (11), (15) imply: % 68.70/9.95 | (16) greater(all_31_1, all_106_0) % 68.70/9.95 | % 68.70/9.95 | PRED_UNIFY: (2), (16) imply: % 68.70/9.95 | (17) ~ (all_106_0 = zero) % 68.70/9.95 | % 68.70/9.95 | BETA: splitting (5) gives: % 68.70/9.95 | % 68.70/9.95 | Case 1: % 68.70/9.95 | | % 68.70/9.95 | | (18) (all_40_0 = zero & all_40_1 = zero & % 68.70/9.95 | | growth_rate(efficient_producers, all_31_2) = zero & % 68.70/9.95 | | growth_rate(first_movers, all_31_2) = zero) | % 68.70/9.95 | | (equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.70/9.95 | | greater_or_equal(all_31_2, all_40_2)) % 68.70/9.95 | | % 68.70/9.95 | | BETA: splitting (18) gives: % 68.70/9.95 | | % 68.70/9.95 | | Case 1: % 68.70/9.95 | | | % 68.70/9.95 | | | (19) all_40_0 = zero & all_40_1 = zero & % 68.70/9.95 | | | growth_rate(efficient_producers, all_31_2) = zero & % 68.70/9.95 | | | growth_rate(first_movers, all_31_2) = zero % 68.70/9.95 | | | % 68.70/9.95 | | | ALPHA: (19) implies: % 68.70/9.95 | | | (20) growth_rate(first_movers, all_31_2) = zero % 68.70/9.95 | | | % 68.70/9.95 | | | GROUND_INST: instantiating (1) with all_106_0, zero, all_31_2, % 68.70/9.95 | | | first_movers, simplifying with (13), (20) gives: % 68.70/9.95 | | | (21) all_106_0 = zero % 68.70/9.95 | | | % 68.70/9.95 | | | REDUCE: (17), (21) imply: % 68.70/9.95 | | | (22) $false % 68.70/9.95 | | | % 68.70/9.95 | | | CLOSE: (22) is inconsistent. % 68.70/9.95 | | | % 68.70/9.95 | | Case 2: % 68.70/9.95 | | | % 68.70/9.95 | | | (23) equilibrium(all_11_0) = all_40_2 & $i(all_40_2) & ~ % 68.70/9.95 | | | greater_or_equal(all_31_2, all_40_2) % 68.70/9.95 | | | % 68.70/9.95 | | | ALPHA: (23) implies: % 68.70/9.95 | | | (24) ~ greater_or_equal(all_31_2, all_40_2) % 68.70/9.95 | | | (25) equilibrium(all_11_0) = all_40_2 % 68.70/9.95 | | | % 68.70/9.95 | | | REF_CLOSE: (3), (8), (10), (24), (25) are inconsistent by sub-proof #13. % 68.70/9.95 | | | % 68.70/9.95 | | End of split % 68.70/9.95 | | % 68.70/9.95 | Case 2: % 68.70/9.95 | | % 68.70/9.95 | | (26) (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.95 | | growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.95 | | $i(all_40_1) & greater(all_40_0, zero) & greater(zero, all_40_1)) % 68.70/9.95 | | | (growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.95 | | growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.95 | | $i(all_40_1) & greater(all_40_1, zero) & greater(zero, all_40_0)) % 68.70/9.95 | | % 68.70/9.95 | | BETA: splitting (26) gives: % 68.70/9.95 | | % 68.70/9.95 | | Case 1: % 68.70/9.95 | | | % 68.70/9.95 | | | (27) growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.95 | | | growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.95 | | | $i(all_40_1) & greater(all_40_0, zero) & greater(zero, all_40_1) % 68.70/9.95 | | | % 68.70/9.95 | | | ALPHA: (27) implies: % 68.70/9.95 | | | (28) greater(all_40_0, zero) % 68.70/9.95 | | | (29) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.70/9.95 | | | % 68.70/9.95 | | | REF_CLOSE: (1), (2), (7), (28), (29) are inconsistent by sub-proof #12. % 68.70/9.95 | | | % 68.70/9.95 | | Case 2: % 68.70/9.95 | | | % 68.70/9.95 | | | (30) growth_rate(efficient_producers, all_31_2) = all_40_0 & % 68.70/9.95 | | | growth_rate(first_movers, all_31_2) = all_40_1 & $i(all_40_0) & % 68.70/9.95 | | | $i(all_40_1) & greater(all_40_1, zero) & greater(zero, all_40_0) % 68.70/9.95 | | | % 68.70/9.96 | | | ALPHA: (30) implies: % 68.70/9.96 | | | (31) greater(all_40_1, zero) % 68.70/9.96 | | | (32) $i(all_40_0) % 68.70/9.96 | | | (33) growth_rate(first_movers, all_31_2) = all_40_1 % 68.70/9.96 | | | (34) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.70/9.96 | | | % 68.70/9.96 | | | GROUND_INST: instantiating (1) with all_106_0, all_40_1, all_31_2, % 68.70/9.96 | | | first_movers, simplifying with (13), (33) gives: % 68.70/9.96 | | | (35) all_106_0 = all_40_1 % 68.70/9.96 | | | % 68.70/9.96 | | | GROUND_INST: instantiating (1) with all_31_1, all_40_0, all_31_2, % 68.70/9.96 | | | efficient_producers, simplifying with (7), (34) gives: % 68.70/9.96 | | | (36) all_40_0 = all_31_1 % 68.70/9.96 | | | % 68.70/9.96 | | | REDUCE: (12), (35) imply: % 68.70/9.96 | | | (37) $i(all_40_1) % 68.70/9.96 | | | % 68.70/9.96 | | | REDUCE: (32), (36) imply: % 68.70/9.96 | | | (38) $i(all_31_1) % 68.70/9.96 | | | % 68.70/9.96 | | | REDUCE: (16), (35) imply: % 68.70/9.96 | | | (39) greater(all_31_1, all_40_1) % 68.70/9.96 | | | % 68.70/9.96 | | | GROUND_INST: instantiating (4) with all_31_1, all_40_1, zero, simplifying % 68.70/9.96 | | | with (2), (6), (31), (37), (38), (39) gives: % 68.70/9.96 | | | (40) $false % 68.70/9.96 | | | % 68.70/9.96 | | | CLOSE: (40) is inconsistent. % 68.70/9.96 | | | % 68.70/9.96 | | End of split % 68.70/9.96 | | % 68.70/9.96 | End of split % 68.70/9.96 | % 68.70/9.96 End of proof % 68.70/9.96 % 68.70/9.96 Sub-proof #12 shows that the following formulas are inconsistent: % 68.70/9.96 ---------------------------------------------------------------- % 68.70/9.96 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/9.96 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/9.96 (2) ~ greater(all_31_1, zero) % 68.70/9.96 (3) growth_rate(efficient_producers, all_31_2) = all_40_0 % 68.70/9.96 (4) growth_rate(efficient_producers, all_31_2) = all_31_1 % 68.70/9.96 (5) greater(all_40_0, zero) % 68.70/9.96 % 68.70/9.96 Begin of proof % 68.70/9.96 | % 68.70/9.96 | PRED_UNIFY: (2), (5) imply: % 68.70/9.96 | (6) ~ (all_40_0 = all_31_1) % 68.70/9.96 | % 68.70/9.96 | GROUND_INST: instantiating (1) with all_31_1, all_40_0, all_31_2, % 68.70/9.96 | efficient_producers, simplifying with (3), (4) gives: % 68.70/9.96 | (7) all_40_0 = all_31_1 % 68.70/9.96 | % 68.70/9.96 | REDUCE: (6), (7) imply: % 68.70/9.96 | (8) $false % 68.70/9.96 | % 68.70/9.96 | CLOSE: (8) is inconsistent. % 68.70/9.96 | % 68.70/9.96 End of proof % 68.70/9.96 % 68.70/9.96 Sub-proof #13 shows that the following formulas are inconsistent: % 68.70/9.96 ---------------------------------------------------------------- % 68.70/9.96 (1) ~ greater_or_equal(all_31_2, all_40_2) % 68.70/9.96 (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 68.70/9.96 = v1) | ~ (equilibrium(v2) = v0)) % 68.70/9.96 (3) equilibrium(all_11_0) = all_40_2 % 68.70/9.96 (4) equilibrium(all_11_0) = all_19_1 % 68.70/9.96 (5) greater_or_equal(all_31_2, all_19_1) % 68.70/9.96 % 68.70/9.96 Begin of proof % 68.70/9.96 | % 68.70/9.96 | GROUND_INST: instantiating (2) with all_19_1, all_40_2, all_11_0, simplifying % 68.70/9.96 | with (3), (4) gives: % 68.70/9.96 | (6) all_40_2 = all_19_1 % 68.70/9.96 | % 68.70/9.96 | PRED_UNIFY: (1), (5) imply: % 68.70/9.96 | (7) ~ (all_40_2 = all_19_1) % 68.70/9.96 | % 68.70/9.96 | REDUCE: (6), (7) imply: % 68.70/9.96 | (8) $false % 68.70/9.96 | % 68.70/9.96 | CLOSE: (8) is inconsistent. % 68.70/9.96 | % 68.70/9.96 End of proof % 68.70/9.96 % 68.70/9.96 Sub-proof #14 shows that the following formulas are inconsistent: % 68.70/9.96 ---------------------------------------------------------------- % 68.70/9.96 (1) ~ greater_or_equal(all_31_2, all_21_0) % 68.70/9.96 (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 68.70/9.96 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 68.70/9.96 (3) all_21_0 = all_19_0 | greater(all_19_0, all_21_0) % 68.70/9.96 (4) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 68.70/9.96 greater_or_equal(v0, v1)) % 68.70/9.96 (5) all_31_2 = all_19_0 | greater(all_31_2, all_19_0) % 68.70/9.96 (6) ~ (all_21_0 = all_19_0) % 68.70/9.96 (7) $i(all_31_2) % 68.70/9.96 (8) $i(all_19_0) % 68.70/9.96 (9) $i(all_21_0) % 68.70/9.96 % 68.70/9.96 Begin of proof % 68.70/9.96 | % 68.70/9.96 | BETA: splitting (3) gives: % 68.70/9.96 | % 68.70/9.96 | Case 1: % 68.70/9.96 | | % 68.70/9.96 | | (10) greater(all_19_0, all_21_0) % 68.70/9.96 | | % 68.70/9.96 | | GROUND_INST: instantiating (4) with all_19_0, all_21_0, simplifying with % 68.70/9.96 | | (8), (9), (10) gives: % 68.70/9.96 | | (11) greater_or_equal(all_19_0, all_21_0) % 68.70/9.96 | | % 68.70/9.97 | | PRED_UNIFY: (1), (11) imply: % 68.70/9.97 | | (12) ~ (all_31_2 = all_19_0) % 68.70/9.97 | | % 68.70/9.97 | | BETA: splitting (5) gives: % 68.70/9.97 | | % 68.70/9.97 | | Case 1: % 68.70/9.97 | | | % 68.70/9.97 | | | (13) greater(all_31_2, all_19_0) % 68.70/9.97 | | | % 68.70/9.97 | | | GROUND_INST: instantiating (2) with all_31_2, all_19_0, all_21_0, % 68.70/9.97 | | | simplifying with (7), (8), (9), (10), (13) gives: % 68.70/9.97 | | | (14) greater(all_31_2, all_21_0) % 68.70/9.97 | | | % 68.70/9.97 | | | GROUND_INST: instantiating (4) with all_31_2, all_21_0, simplifying with % 68.70/9.97 | | | (1), (7), (9), (14) gives: % 68.70/9.97 | | | (15) $false % 68.70/9.97 | | | % 68.70/9.97 | | | CLOSE: (15) is inconsistent. % 68.70/9.97 | | | % 68.70/9.97 | | Case 2: % 68.70/9.97 | | | % 68.70/9.97 | | | (16) all_31_2 = all_19_0 % 68.70/9.97 | | | % 68.70/9.97 | | | REDUCE: (12), (16) imply: % 68.70/9.97 | | | (17) $false % 68.70/9.97 | | | % 68.70/9.97 | | | CLOSE: (17) is inconsistent. % 68.70/9.97 | | | % 68.70/9.97 | | End of split % 68.70/9.97 | | % 68.70/9.97 | Case 2: % 68.70/9.97 | | % 68.70/9.97 | | (18) all_21_0 = all_19_0 % 68.70/9.97 | | % 68.70/9.97 | | REDUCE: (6), (18) imply: % 68.70/9.97 | | (19) $false % 68.70/9.97 | | % 68.70/9.97 | | CLOSE: (19) is inconsistent. % 68.70/9.97 | | % 68.70/9.97 | End of split % 68.70/9.97 | % 68.70/9.97 End of proof % 68.70/9.97 % 68.70/9.97 Sub-proof #15 shows that the following formulas are inconsistent: % 68.70/9.97 ---------------------------------------------------------------- % 68.70/9.97 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/9.97 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/9.97 (2) growth_rate(efficient_producers, all_29_2) = all_29_1 % 68.70/9.97 (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 68.70/9.97 = v1) | ~ (equilibrium(v2) = v0)) % 68.70/9.97 (4) ~ greater(all_29_1, zero) % 68.70/9.97 (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 68.70/9.97 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 68.70/9.97 (6) all_38_0 = all_38_1 | ~ (growth_rate(first_movers, all_29_2) = all_38_1) % 68.70/9.97 (7) $i(all_29_2) % 68.70/9.97 (8) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 68.70/9.97 greater_or_equal(v0, v1)) % 68.70/9.97 (9) (all_41_0 = zero & all_41_1 = zero & growth_rate(efficient_producers, % 68.70/9.97 all_29_2) = zero & growth_rate(first_movers, all_29_2) = zero) | % 68.70/9.97 (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.70/9.97 greater_or_equal(all_29_2, all_41_2)) | % 68.70/9.97 (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/9.97 growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.70/9.97 $i(all_41_1) & greater(all_41_0, zero) & greater(zero, all_41_1)) | % 68.70/9.97 (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/9.97 growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.70/9.97 $i(all_41_1) & greater(all_41_1, zero) & greater(zero, all_41_0)) % 68.70/9.97 (10) all_38_1 = all_29_1 % 68.70/9.97 (11) $i(zero) % 68.70/9.97 (12) all_29_2 = all_21_0 | greater(all_29_2, all_21_0) % 68.70/9.97 (13) growth_rate(first_movers, all_29_2) = all_38_0 % 68.70/9.97 (14) greater(all_21_0, all_19_1) % 68.70/9.97 (15) ~ (all_38_0 = zero) % 68.70/9.97 (16) $i(all_19_1) % 68.70/9.97 (17) $i(all_21_0) % 68.70/9.97 (18) equilibrium(all_11_0) = all_19_1 % 68.70/9.97 (19) greater(all_29_1, all_38_0) % 68.70/9.97 % 68.70/9.97 Begin of proof % 68.70/9.97 | % 68.70/9.97 | GROUND_INST: instantiating (8) with all_21_0, all_19_1, simplifying with (14), % 68.70/9.97 | (16), (17) gives: % 68.70/9.97 | (20) greater_or_equal(all_21_0, all_19_1) % 68.70/9.97 | % 68.70/9.97 | BETA: splitting (12) gives: % 68.70/9.97 | % 68.70/9.97 | Case 1: % 68.70/9.97 | | % 68.70/9.97 | | (21) greater(all_29_2, all_21_0) % 68.70/9.97 | | % 68.70/9.97 | | GROUND_INST: instantiating (5) with all_29_2, all_21_0, all_19_1, % 68.70/9.97 | | simplifying with (7), (14), (16), (17), (21) gives: % 68.70/9.97 | | (22) greater(all_29_2, all_19_1) % 68.70/9.97 | | % 68.70/9.97 | | BETA: splitting (6) gives: % 68.70/9.97 | | % 68.70/9.97 | | Case 1: % 68.70/9.97 | | | % 68.70/9.97 | | | (23) ~ (growth_rate(first_movers, all_29_2) = all_38_1) % 68.70/9.97 | | | % 68.70/9.97 | | | REDUCE: (10), (23) imply: % 68.70/9.97 | | | (24) ~ (growth_rate(first_movers, all_29_2) = all_29_1) % 68.70/9.97 | | | % 68.70/9.97 | | | BETA: splitting (9) gives: % 68.70/9.97 | | | % 68.70/9.97 | | | Case 1: % 68.70/9.97 | | | | % 68.70/9.98 | | | | (25) (all_41_0 = zero & all_41_1 = zero & % 68.70/9.98 | | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.70/9.98 | | | | growth_rate(first_movers, all_29_2) = zero) | % 68.70/9.98 | | | | (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.70/9.98 | | | | greater_or_equal(all_29_2, all_41_2)) % 68.70/9.98 | | | | % 68.70/9.98 | | | | BETA: splitting (25) gives: % 68.70/9.98 | | | | % 68.70/9.98 | | | | Case 1: % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | (26) all_41_0 = zero & all_41_1 = zero & % 68.70/9.98 | | | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.70/9.98 | | | | | growth_rate(first_movers, all_29_2) = zero % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | ALPHA: (26) implies: % 68.70/9.98 | | | | | (27) growth_rate(first_movers, all_29_2) = zero % 68.70/9.98 | | | | | (28) growth_rate(efficient_producers, all_29_2) = zero % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | PRED_UNIFY: (24), (27) imply: % 68.70/9.98 | | | | | (29) ~ (all_29_1 = zero) % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | GROUND_INST: instantiating (1) with all_29_1, zero, all_29_2, % 68.70/9.98 | | | | | efficient_producers, simplifying with (2), (28) gives: % 68.70/9.98 | | | | | (30) all_29_1 = zero % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | REDUCE: (29), (30) imply: % 68.70/9.98 | | | | | (31) $false % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | CLOSE: (31) is inconsistent. % 68.70/9.98 | | | | | % 68.70/9.98 | | | | Case 2: % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | (32) equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.70/9.98 | | | | | greater_or_equal(all_29_2, all_41_2) % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | ALPHA: (32) implies: % 68.70/9.98 | | | | | (33) ~ greater_or_equal(all_29_2, all_41_2) % 68.70/9.98 | | | | | (34) $i(all_41_2) % 68.70/9.98 | | | | | (35) equilibrium(all_11_0) = all_41_2 % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | REF_CLOSE: (3), (7), (8), (18), (22), (33), (34), (35) are % 68.70/9.98 | | | | | inconsistent by sub-proof #20. % 68.70/9.98 | | | | | % 68.70/9.98 | | | | End of split % 68.70/9.98 | | | | % 68.70/9.98 | | | Case 2: % 68.70/9.98 | | | | % 68.70/9.98 | | | | (36) (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/9.98 | | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) % 68.70/9.98 | | | | & $i(all_41_1) & greater(all_41_0, zero) & greater(zero, % 68.70/9.98 | | | | all_41_1)) | (growth_rate(efficient_producers, all_29_2) = % 68.70/9.98 | | | | all_41_0 & growth_rate(first_movers, all_29_2) = all_41_1 & % 68.70/9.98 | | | | $i(all_41_0) & $i(all_41_1) & greater(all_41_1, zero) & % 68.70/9.98 | | | | greater(zero, all_41_0)) % 68.70/9.98 | | | | % 68.70/9.98 | | | | BETA: splitting (36) gives: % 68.70/9.98 | | | | % 68.70/9.98 | | | | Case 1: % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | (37) growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/9.98 | | | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) % 68.70/9.98 | | | | | & $i(all_41_1) & greater(all_41_0, zero) & greater(zero, % 68.70/9.98 | | | | | all_41_1) % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | ALPHA: (37) implies: % 68.70/9.98 | | | | | (38) greater(all_41_0, zero) % 68.70/9.98 | | | | | (39) growth_rate(efficient_producers, all_29_2) = all_41_0 % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | REF_CLOSE: (1), (2), (4), (38), (39) are inconsistent by sub-proof % 68.70/9.98 | | | | | #19. % 68.70/9.98 | | | | | % 68.70/9.98 | | | | Case 2: % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | (40) growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/9.98 | | | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) % 68.70/9.98 | | | | | & $i(all_41_1) & greater(all_41_1, zero) & greater(zero, % 68.70/9.98 | | | | | all_41_0) % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | ALPHA: (40) implies: % 68.70/9.98 | | | | | (41) greater(all_41_1, zero) % 68.70/9.98 | | | | | (42) $i(all_41_1) % 68.70/9.98 | | | | | (43) $i(all_41_0) % 68.70/9.98 | | | | | (44) growth_rate(first_movers, all_29_2) = all_41_1 % 68.70/9.98 | | | | | (45) growth_rate(efficient_producers, all_29_2) = all_41_0 % 68.70/9.98 | | | | | % 68.70/9.98 | | | | | REF_CLOSE: (1), (2), (4), (5), (11), (13), (19), (41), (42), (43), % 68.70/9.98 | | | | | (44), (45) are inconsistent by sub-proof #18. % 68.70/9.98 | | | | | % 68.70/9.98 | | | | End of split % 68.70/9.98 | | | | % 68.70/9.98 | | | End of split % 68.70/9.98 | | | % 68.70/9.98 | | Case 2: % 68.70/9.98 | | | % 68.70/9.98 | | | (46) all_38_0 = all_38_1 % 68.70/9.98 | | | % 68.70/9.98 | | | COMBINE_EQS: (10), (46) imply: % 68.70/9.98 | | | (47) all_38_0 = all_29_1 % 68.70/9.98 | | | % 68.70/9.98 | | | REDUCE: (15), (47) imply: % 68.70/9.98 | | | (48) ~ (all_29_1 = zero) % 68.70/9.98 | | | % 68.70/9.98 | | | BETA: splitting (9) gives: % 68.70/9.98 | | | % 68.70/9.98 | | | Case 1: % 68.70/9.98 | | | | % 68.70/9.98 | | | | (49) (all_41_0 = zero & all_41_1 = zero & % 68.70/9.98 | | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.70/9.98 | | | | growth_rate(first_movers, all_29_2) = zero) | % 68.70/9.98 | | | | (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.70/9.98 | | | | greater_or_equal(all_29_2, all_41_2)) % 68.70/9.98 | | | | % 68.70/9.98 | | | | BETA: splitting (49) gives: % 68.70/9.98 | | | | % 68.70/9.98 | | | | Case 1: % 68.70/9.98 | | | | | % 68.70/9.99 | | | | | (50) all_41_0 = zero & all_41_1 = zero & % 68.70/9.99 | | | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.70/9.99 | | | | | growth_rate(first_movers, all_29_2) = zero % 68.70/9.99 | | | | | % 68.70/9.99 | | | | | ALPHA: (50) implies: % 68.70/9.99 | | | | | (51) growth_rate(efficient_producers, all_29_2) = zero % 68.70/9.99 | | | | | % 68.70/9.99 | | | | | GROUND_INST: instantiating (1) with all_29_1, zero, all_29_2, % 68.70/9.99 | | | | | efficient_producers, simplifying with (2), (51) gives: % 68.70/9.99 | | | | | (52) all_29_1 = zero % 68.70/9.99 | | | | | % 68.70/9.99 | | | | | REDUCE: (48), (52) imply: % 68.70/9.99 | | | | | (53) $false % 68.70/9.99 | | | | | % 68.70/9.99 | | | | | CLOSE: (53) is inconsistent. % 68.70/9.99 | | | | | % 68.70/9.99 | | | | Case 2: % 68.70/9.99 | | | | | % 68.70/9.99 | | | | | (54) equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.70/9.99 | | | | | greater_or_equal(all_29_2, all_41_2) % 68.70/9.99 | | | | | % 68.70/9.99 | | | | | ALPHA: (54) implies: % 68.70/9.99 | | | | | (55) ~ greater_or_equal(all_29_2, all_41_2) % 68.70/9.99 | | | | | (56) $i(all_41_2) % 68.70/9.99 | | | | | (57) equilibrium(all_11_0) = all_41_2 % 68.70/9.99 | | | | | % 68.70/9.99 | | | | | REF_CLOSE: (3), (7), (8), (18), (22), (55), (56), (57) are % 68.70/9.99 | | | | | inconsistent by sub-proof #20. % 68.70/9.99 | | | | | % 68.70/9.99 | | | | End of split % 68.70/9.99 | | | | % 68.70/9.99 | | | Case 2: % 68.70/9.99 | | | | % 68.70/9.99 | | | | (58) (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/9.99 | | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) % 68.70/9.99 | | | | & $i(all_41_1) & greater(all_41_0, zero) & greater(zero, % 68.70/9.99 | | | | all_41_1)) | (growth_rate(efficient_producers, all_29_2) = % 68.70/9.99 | | | | all_41_0 & growth_rate(first_movers, all_29_2) = all_41_1 & % 68.70/9.99 | | | | $i(all_41_0) & $i(all_41_1) & greater(all_41_1, zero) & % 68.70/9.99 | | | | greater(zero, all_41_0)) % 68.70/9.99 | | | | % 68.70/9.99 | | | | REF_CLOSE: (1), (2), (4), (5), (11), (13), (19), (58) are inconsistent % 68.70/9.99 | | | | by sub-proof #17. % 68.70/9.99 | | | | % 68.70/9.99 | | | End of split % 68.70/9.99 | | | % 68.70/9.99 | | End of split % 68.70/9.99 | | % 68.70/9.99 | Case 2: % 68.70/9.99 | | % 68.70/9.99 | | (59) all_29_2 = all_21_0 % 68.70/9.99 | | % 68.70/9.99 | | REDUCE: (13), (59) imply: % 68.70/9.99 | | (60) growth_rate(first_movers, all_21_0) = all_38_0 % 68.70/9.99 | | % 68.70/9.99 | | BETA: splitting (9) gives: % 68.70/9.99 | | % 68.70/9.99 | | Case 1: % 68.70/9.99 | | | % 68.70/9.99 | | | (61) (all_41_0 = zero & all_41_1 = zero & % 68.70/9.99 | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.70/9.99 | | | growth_rate(first_movers, all_29_2) = zero) | % 68.70/9.99 | | | (equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.70/9.99 | | | greater_or_equal(all_29_2, all_41_2)) % 68.70/9.99 | | | % 68.70/9.99 | | | BETA: splitting (61) gives: % 68.70/9.99 | | | % 68.70/9.99 | | | Case 1: % 68.70/9.99 | | | | % 68.70/9.99 | | | | (62) all_41_0 = zero & all_41_1 = zero & % 68.70/9.99 | | | | growth_rate(efficient_producers, all_29_2) = zero & % 68.70/9.99 | | | | growth_rate(first_movers, all_29_2) = zero % 68.70/9.99 | | | | % 68.70/9.99 | | | | ALPHA: (62) implies: % 68.70/9.99 | | | | (63) growth_rate(first_movers, all_29_2) = zero % 68.70/9.99 | | | | % 68.70/9.99 | | | | REDUCE: (59), (63) imply: % 68.70/9.99 | | | | (64) growth_rate(first_movers, all_21_0) = zero % 68.70/9.99 | | | | % 68.70/9.99 | | | | GROUND_INST: instantiating (1) with zero, all_38_0, all_21_0, % 68.70/9.99 | | | | first_movers, simplifying with (60), (64) gives: % 68.70/9.99 | | | | (65) all_38_0 = zero % 68.70/9.99 | | | | % 68.70/9.99 | | | | REDUCE: (15), (65) imply: % 68.70/9.99 | | | | (66) $false % 68.70/9.99 | | | | % 68.70/9.99 | | | | CLOSE: (66) is inconsistent. % 68.70/9.99 | | | | % 68.70/9.99 | | | Case 2: % 68.70/9.99 | | | | % 68.70/9.99 | | | | (67) equilibrium(all_11_0) = all_41_2 & $i(all_41_2) & ~ % 68.70/9.99 | | | | greater_or_equal(all_29_2, all_41_2) % 68.70/9.99 | | | | % 68.70/9.99 | | | | ALPHA: (67) implies: % 68.70/9.99 | | | | (68) ~ greater_or_equal(all_29_2, all_41_2) % 68.70/9.99 | | | | (69) equilibrium(all_11_0) = all_41_2 % 68.70/9.99 | | | | % 68.70/9.99 | | | | REDUCE: (59), (68) imply: % 68.70/9.99 | | | | (70) ~ greater_or_equal(all_21_0, all_41_2) % 68.70/9.99 | | | | % 68.70/9.99 | | | | REF_CLOSE: (3), (18), (20), (69), (70) are inconsistent by sub-proof % 68.70/9.99 | | | | #16. % 68.70/9.99 | | | | % 68.70/9.99 | | | End of split % 68.70/9.99 | | | % 68.70/9.99 | | Case 2: % 68.70/9.99 | | | % 68.70/10.00 | | | (71) (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/10.00 | | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.70/10.00 | | | $i(all_41_1) & greater(all_41_0, zero) & greater(zero, % 68.70/10.00 | | | all_41_1)) | (growth_rate(efficient_producers, all_29_2) = % 68.70/10.00 | | | all_41_0 & growth_rate(first_movers, all_29_2) = all_41_1 & % 68.70/10.00 | | | $i(all_41_0) & $i(all_41_1) & greater(all_41_1, zero) & % 68.70/10.00 | | | greater(zero, all_41_0)) % 68.70/10.00 | | | % 68.70/10.00 | | | REF_CLOSE: (1), (2), (4), (5), (11), (13), (19), (71) are inconsistent by % 68.70/10.00 | | | sub-proof #17. % 68.70/10.00 | | | % 68.70/10.00 | | End of split % 68.70/10.00 | | % 68.70/10.00 | End of split % 68.70/10.00 | % 68.70/10.00 End of proof % 68.70/10.00 % 68.70/10.00 Sub-proof #16 shows that the following formulas are inconsistent: % 68.70/10.00 ---------------------------------------------------------------- % 68.70/10.00 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 68.70/10.00 = v1) | ~ (equilibrium(v2) = v0)) % 68.70/10.00 (2) greater_or_equal(all_21_0, all_19_1) % 68.70/10.00 (3) equilibrium(all_11_0) = all_41_2 % 68.70/10.00 (4) ~ greater_or_equal(all_21_0, all_41_2) % 68.70/10.00 (5) equilibrium(all_11_0) = all_19_1 % 68.70/10.00 % 68.70/10.00 Begin of proof % 68.70/10.00 | % 68.70/10.00 | GROUND_INST: instantiating (1) with all_19_1, all_41_2, all_11_0, simplifying % 68.70/10.00 | with (3), (5) gives: % 68.70/10.00 | (6) all_41_2 = all_19_1 % 68.70/10.00 | % 68.70/10.00 | PRED_UNIFY: (2), (4) imply: % 68.70/10.00 | (7) ~ (all_41_2 = all_19_1) % 68.70/10.00 | % 68.70/10.00 | REDUCE: (6), (7) imply: % 68.70/10.00 | (8) $false % 68.70/10.00 | % 68.70/10.00 | CLOSE: (8) is inconsistent. % 68.70/10.00 | % 68.70/10.00 End of proof % 68.70/10.00 % 68.70/10.00 Sub-proof #17 shows that the following formulas are inconsistent: % 68.70/10.00 ---------------------------------------------------------------- % 68.70/10.00 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/10.00 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/10.00 (2) growth_rate(efficient_producers, all_29_2) = all_29_1 % 68.70/10.00 (3) ~ greater(all_29_1, zero) % 68.70/10.00 (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 68.70/10.00 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 68.70/10.00 (5) $i(zero) % 68.70/10.00 (6) growth_rate(first_movers, all_29_2) = all_38_0 % 68.70/10.00 (7) (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/10.00 growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.70/10.00 $i(all_41_1) & greater(all_41_0, zero) & greater(zero, all_41_1)) | % 68.70/10.00 (growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/10.00 growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.70/10.00 $i(all_41_1) & greater(all_41_1, zero) & greater(zero, all_41_0)) % 68.70/10.00 (8) greater(all_29_1, all_38_0) % 68.70/10.00 % 68.70/10.00 Begin of proof % 68.70/10.00 | % 68.70/10.00 | BETA: splitting (7) gives: % 68.70/10.00 | % 68.70/10.00 | Case 1: % 68.70/10.00 | | % 68.70/10.00 | | (9) growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/10.00 | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.70/10.00 | | $i(all_41_1) & greater(all_41_0, zero) & greater(zero, all_41_1) % 68.70/10.00 | | % 68.70/10.00 | | ALPHA: (9) implies: % 68.70/10.00 | | (10) greater(all_41_0, zero) % 68.70/10.00 | | (11) growth_rate(efficient_producers, all_29_2) = all_41_0 % 68.70/10.00 | | % 68.70/10.00 | | REF_CLOSE: (1), (2), (3), (10), (11) are inconsistent by sub-proof #19. % 68.70/10.00 | | % 68.70/10.00 | Case 2: % 68.70/10.00 | | % 68.70/10.00 | | (12) growth_rate(efficient_producers, all_29_2) = all_41_0 & % 68.70/10.00 | | growth_rate(first_movers, all_29_2) = all_41_1 & $i(all_41_0) & % 68.70/10.00 | | $i(all_41_1) & greater(all_41_1, zero) & greater(zero, all_41_0) % 68.70/10.00 | | % 68.70/10.00 | | ALPHA: (12) implies: % 68.70/10.00 | | (13) greater(all_41_1, zero) % 68.70/10.00 | | (14) $i(all_41_1) % 68.70/10.00 | | (15) $i(all_41_0) % 68.70/10.00 | | (16) growth_rate(first_movers, all_29_2) = all_41_1 % 68.70/10.00 | | (17) growth_rate(efficient_producers, all_29_2) = all_41_0 % 68.70/10.00 | | % 68.70/10.00 | | REF_CLOSE: (1), (2), (3), (4), (5), (6), (8), (13), (14), (15), (16), (17) % 68.70/10.00 | | are inconsistent by sub-proof #18. % 68.70/10.00 | | % 68.70/10.00 | End of split % 68.70/10.00 | % 68.70/10.00 End of proof % 68.70/10.00 % 68.70/10.00 Sub-proof #18 shows that the following formulas are inconsistent: % 68.70/10.00 ---------------------------------------------------------------- % 68.70/10.00 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/10.00 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/10.00 (2) growth_rate(efficient_producers, all_29_2) = all_29_1 % 68.70/10.00 (3) ~ greater(all_29_1, zero) % 68.70/10.01 (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 68.70/10.01 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 68.70/10.01 (5) $i(all_41_0) % 68.70/10.01 (6) greater(all_41_1, zero) % 68.70/10.01 (7) $i(zero) % 68.70/10.01 (8) growth_rate(first_movers, all_29_2) = all_41_1 % 68.70/10.01 (9) growth_rate(efficient_producers, all_29_2) = all_41_0 % 68.70/10.01 (10) $i(all_41_1) % 68.70/10.01 (11) growth_rate(first_movers, all_29_2) = all_38_0 % 68.70/10.01 (12) greater(all_29_1, all_38_0) % 68.70/10.01 % 68.70/10.01 Begin of proof % 68.70/10.01 | % 68.70/10.01 | GROUND_INST: instantiating (1) with all_38_0, all_41_1, all_29_2, % 68.70/10.01 | first_movers, simplifying with (8), (11) gives: % 68.70/10.01 | (13) all_41_1 = all_38_0 % 68.70/10.01 | % 68.70/10.01 | GROUND_INST: instantiating (1) with all_29_1, all_41_0, all_29_2, % 68.70/10.01 | efficient_producers, simplifying with (2), (9) gives: % 68.70/10.01 | (14) all_41_0 = all_29_1 % 68.70/10.01 | % 68.70/10.01 | REDUCE: (5), (14) imply: % 68.70/10.01 | (15) $i(all_29_1) % 68.70/10.01 | % 68.70/10.01 | REDUCE: (10), (13) imply: % 68.70/10.01 | (16) $i(all_38_0) % 68.70/10.01 | % 68.70/10.01 | REDUCE: (6), (13) imply: % 68.70/10.01 | (17) greater(all_38_0, zero) % 68.70/10.01 | % 68.70/10.01 | GROUND_INST: instantiating (4) with all_29_1, all_38_0, zero, simplifying with % 68.70/10.01 | (3), (7), (12), (15), (16), (17) gives: % 68.70/10.01 | (18) $false % 68.70/10.01 | % 68.70/10.01 | CLOSE: (18) is inconsistent. % 68.70/10.01 | % 68.70/10.01 End of proof % 68.70/10.01 % 68.70/10.01 Sub-proof #19 shows that the following formulas are inconsistent: % 68.70/10.01 ---------------------------------------------------------------- % 68.70/10.01 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.70/10.01 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 68.70/10.01 (2) growth_rate(efficient_producers, all_29_2) = all_29_1 % 68.70/10.01 (3) greater(all_41_0, zero) % 68.70/10.01 (4) ~ greater(all_29_1, zero) % 68.70/10.01 (5) growth_rate(efficient_producers, all_29_2) = all_41_0 % 68.70/10.01 % 68.70/10.01 Begin of proof % 68.70/10.01 | % 68.70/10.01 | PRED_UNIFY: (3), (4) imply: % 68.70/10.01 | (6) ~ (all_41_0 = all_29_1) % 68.70/10.01 | % 68.70/10.01 | GROUND_INST: instantiating (1) with all_29_1, all_41_0, all_29_2, % 68.70/10.01 | efficient_producers, simplifying with (2), (5) gives: % 68.70/10.01 | (7) all_41_0 = all_29_1 % 68.70/10.01 | % 68.70/10.01 | REDUCE: (6), (7) imply: % 68.70/10.01 | (8) $false % 68.70/10.01 | % 68.70/10.01 | CLOSE: (8) is inconsistent. % 68.70/10.01 | % 68.70/10.01 End of proof % 68.70/10.01 % 68.70/10.01 Sub-proof #20 shows that the following formulas are inconsistent: % 68.70/10.01 ---------------------------------------------------------------- % 68.70/10.01 (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 68.70/10.01 = v1) | ~ (equilibrium(v2) = v0)) % 68.70/10.01 (2) equilibrium(all_11_0) = all_41_2 % 68.70/10.01 (3) $i(all_29_2) % 68.70/10.01 (4) greater(all_29_2, all_19_1) % 68.70/10.01 (5) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 68.70/10.01 greater_or_equal(v0, v1)) % 68.70/10.01 (6) $i(all_41_2) % 68.70/10.01 (7) equilibrium(all_11_0) = all_19_1 % 68.70/10.01 (8) ~ greater_or_equal(all_29_2, all_41_2) % 68.70/10.01 % 68.70/10.01 Begin of proof % 68.70/10.01 | % 68.70/10.01 | GROUND_INST: instantiating (1) with all_19_1, all_41_2, all_11_0, simplifying % 68.70/10.01 | with (2), (7) gives: % 68.70/10.01 | (9) all_41_2 = all_19_1 % 68.70/10.01 | % 68.70/10.01 | REDUCE: (6), (9) imply: % 68.70/10.01 | (10) $i(all_19_1) % 68.70/10.01 | % 68.70/10.01 | REDUCE: (8), (9) imply: % 68.70/10.01 | (11) ~ greater_or_equal(all_29_2, all_19_1) % 68.70/10.01 | % 68.70/10.01 | GROUND_INST: instantiating (5) with all_29_2, all_19_1, simplifying with (3), % 68.70/10.01 | (4), (10), (11) gives: % 68.70/10.01 | (12) $false % 68.70/10.01 | % 68.70/10.01 | CLOSE: (12) is inconsistent. % 68.70/10.01 | % 68.70/10.01 End of proof % 68.70/10.01 % SZS output end Proof for theBenchmark % 68.70/10.01 % 68.70/10.01 9289ms %------------------------------------------------------------------------------