%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : MGT035+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 : n019.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:23 AM UTC 2026 % Result : Theorem 144.13s 19.12s % Output : Proof 147.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT035+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.09/0.35 % Computer : n019.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 12:33:52 UTC 2026 % 0.09/0.35 % CPUTime : % 0.13/0.37 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.52/0.59 ________ _____ % 0.52/0.59 ___ __ \_________(_)________________________________ % 0.52/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.52/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.52/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.52/0.59 % 0.52/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.52/0.59 (2023-06-19) % 0.52/0.59 % 0.52/0.59 (c) Philipp Rümmer, 2009-2023 % 0.52/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.52/0.59 Amanda Stjerna. % 0.52/0.59 Free software under BSD-3-Clause. % 0.52/0.59 % 0.52/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.52/0.59 % 0.52/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.52/0.61 Running up to 7 provers in parallel. % 0.52/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.52/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.52/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.52/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.52/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.52/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.52/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 1.87/1.05 Prover 4: Preprocessing ... % 1.87/1.06 Prover 2: Preprocessing ... % 3.22/1.08 Prover 5: Preprocessing ... % 3.22/1.09 Prover 1: Preprocessing ... % 3.22/1.10 Prover 3: Preprocessing ... % 3.22/1.14 Prover 0: Preprocessing ... % 3.22/1.14 Prover 6: Preprocessing ... % 6.53/1.51 Prover 6: Proving ... % 6.53/1.57 Prover 2: Proving ... % 6.53/1.57 Prover 5: Proving ... % 6.53/1.59 Prover 3: Constructing countermodel ... % 7.34/1.63 Prover 1: Constructing countermodel ... % 8.85/1.89 Prover 4: Constructing countermodel ... % 9.64/1.95 Prover 0: Proving ... % 13.57/2.46 Prover 3: gave up % 13.57/2.47 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 14.36/2.56 Prover 7: Preprocessing ... % 15.94/2.70 Prover 7: Warning: ignoring some quantifiers % 15.94/2.73 Prover 7: Constructing countermodel ... % 16.74/2.88 Prover 7: gave up % 16.74/2.88 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 17.55/2.99 Prover 8: Preprocessing ... % 18.85/3.13 Prover 8: Warning: ignoring some quantifiers % 18.85/3.14 Prover 8: Constructing countermodel ... % 19.85/3.22 Prover 1: gave up % 19.85/3.23 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 19.85/3.27 Prover 9: Preprocessing ... % 21.44/3.47 Prover 9: Constructing countermodel ... % 24.63/3.83 Prover 8: gave up % 24.63/3.83 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 25.45/3.94 Prover 10: Preprocessing ... % 25.45/4.04 Prover 10: Warning: ignoring some quantifiers % 25.45/4.05 Prover 10: Constructing countermodel ... % 26.79/4.13 Prover 10: gave up % 26.79/4.13 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 27.75/4.21 Prover 11: Preprocessing ... % 29.32/4.40 Prover 11: Constructing countermodel ... % 60.62/8.47 Prover 2: stopped % 60.62/8.47 Prover 12: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=2024365391 % 61.39/8.57 Prover 12: Preprocessing ... % 62.20/8.65 Prover 12: Proving ... % 75.50/10.33 Prover 12: stopped % 75.50/10.33 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 75.50/10.37 Prover 13: Preprocessing ... % 76.30/10.43 Prover 13: Warning: ignoring some quantifiers % 76.30/10.44 Prover 13: Constructing countermodel ... % 104.06/13.95 Prover 5: stopped % 104.06/13.95 Prover 14: Options: -triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=414236379 % 104.06/13.99 Prover 14: Preprocessing ... % 105.83/14.17 Prover 14: Proving ... % 111.79/14.98 Prover 13: stopped % 111.79/14.98 Prover 15: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=723048181 % 112.57/15.04 Prover 15: Preprocessing ... % 113.55/15.18 Prover 15: Proving ... % 134.71/17.87 Prover 6: stopped % 135.49/17.91 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 135.49/17.93 Prover 16: Preprocessing ... % 135.49/17.95 Prover 16: Warning: ignoring some quantifiers % 135.49/17.96 Prover 16: Constructing countermodel ... % 144.13/19.11 Prover 16: Found proof (size 934) % 144.13/19.11 Prover 16: proved (1240ms) % 144.13/19.11 Prover 0: stopped % 144.13/19.11 Prover 14: stopped % 144.13/19.11 Prover 15: stopped % 144.13/19.11 Prover 9: stopped % 144.13/19.12 Prover 4: stopped % 144.13/19.12 Prover 11: stopped % 144.13/19.12 % 144.13/19.12 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 144.13/19.12 % 145.14/19.18 % SZS output start Proof for theBenchmark % 145.14/19.19 Assumptions after simplification: % 145.14/19.19 --------------------------------- % 145.14/19.19 % 145.14/19.19 (a4) % 145.56/19.25 ! [v0: $i] : ( ~ $i(v0) | ~ stable(v0) | ~ environment(v0) | ? [v1: $i] : % 145.56/19.25 ? [v2: $i] : (equilibrium(v0) = v1 & $i(v2) & $i(v1) & greater_or_equal(v2, % 145.56/19.25 v1) & in_environment(v0, v2))) % 145.56/19.25 % 145.56/19.25 (d2) % 145.56/19.26 $i(zero) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) % 145.56/19.26 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ subpopulations(v1, v2, v0, v3) | ~ % 145.56/19.26 environment(v0) | ? [v4: $i] : ? [v5: $i] : (( ~ outcompetes(v2, v1, v3) | % 145.56/19.26 (growth_rate(v2, v3) = v4 & growth_rate(v1, v3) = v5 & $i(v5) & $i(v4) & % 145.56/19.26 greater_or_equal(v4, zero) & greater(zero, v5))) & (outcompetes(v2, % 145.56/19.26 v1, v3) | (growth_rate(v2, v3) = v4 & $i(v4) & ~ greater_or_equal(v4, % 145.56/19.26 zero)) | (growth_rate(v1, v3) = v5 & $i(v5) & ~ greater(zero, % 145.56/19.26 v5))))) % 145.56/19.26 % 145.56/19.26 (l1) % 145.56/19.27 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ( ~ $i(v0) | ~ % 145.56/19.27 stable(v0) | ~ environment(v0) | ? [v1: $i] : ($i(v1) & in_environment(v0, % 145.56/19.27 v1) & ! [v2: $i] : ( ~ $i(v2) | ~ subpopulations(first_movers, % 145.56/19.27 efficient_producers, v0, v2) | ~ greater_or_equal(v2, v1) | ? [v3: % 145.56/19.27 $i] : ? [v4: $i] : (growth_rate(efficient_producers, v2) = v3 & % 145.56/19.27 growth_rate(first_movers, v2) = v4 & $i(v4) & $i(v3) & greater(v3, % 145.56/19.27 v4))))) % 145.56/19.27 % 145.56/19.27 (l6) % 145.56/19.28 $i(efficient_producers) & $i(first_movers) & $i(zero) & ! [v0: $i] : ! [v1: % 145.56/19.28 $i] : ( ~ $i(v1) | ~ $i(v0) | ~ subpopulations(first_movers, % 145.56/19.28 efficient_producers, v0, v1) | ~ environment(v0) | ? [v2: $i] : ? [v3: % 145.56/19.28 $i] : ? [v4: $i] : ((v4 = zero & v3 = zero & % 145.56/19.28 growth_rate(efficient_producers, v1) = zero & growth_rate(first_movers, % 145.56/19.28 v1) = zero) | (equilibrium(v0) = v2 & $i(v2) & ~ greater_or_equal(v1, % 145.56/19.28 v2)) | (growth_rate(efficient_producers, v1) = v4 & % 145.56/19.28 growth_rate(first_movers, v1) = v3 & $i(v4) & $i(v3) & greater(v4, zero) % 145.56/19.28 & greater(zero, v3)) | (growth_rate(efficient_producers, v1) = v4 & % 145.56/19.28 growth_rate(first_movers, v1) = v3 & $i(v4) & $i(v3) & greater(v3, zero) % 145.56/19.28 & greater(zero, v4)))) % 145.56/19.28 % 145.56/19.28 (mp_greater_or_equal) % 145.56/19.28 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ % 145.56/19.28 greater_or_equal(v0, v1) | greater(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( % 145.56/19.28 ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | greater_or_equal(v0, v1)) & ? % 145.56/19.28 [v0: $i] : ( ~ $i(v0) | greater_or_equal(v0, v0)) % 145.56/19.28 % 145.56/19.28 (mp_greater_transitivity) % 145.56/19.28 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 145.56/19.28 ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 145.56/19.28 % 145.56/19.28 (mp_times_in_environment) % 145.56/19.28 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | ~ $i(v2) | ~ $i(v1) | % 145.56/19.28 ~ $i(v0) | ~ in_environment(v0, v2) | ~ in_environment(v0, v1) | % 145.56/19.28 greater(v2, v1) | greater(v1, v2)) % 145.56/19.28 % 145.56/19.28 (prove_t4) % 145.56/19.29 $i(efficient_producers) & $i(first_movers) & ? [v0: $i] : ($i(v0) & % 145.56/19.29 stable(v0) & environment(v0) & ! [v1: $i] : ( ~ $i(v1) | ~ % 145.56/19.29 in_environment(v0, v1) | ? [v2: $i] : ($i(v2) & % 145.56/19.29 subpopulations(first_movers, efficient_producers, v0, v2) & % 145.56/19.29 greater_or_equal(v2, v1) & ~ outcompetes(efficient_producers, % 145.56/19.29 first_movers, v2)))) % 145.56/19.29 % 145.56/19.29 (function-axioms) % 145.56/19.29 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 145.56/19.29 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) & ! [v0: $i] : % 145.56/19.29 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) = v1) | ~ % 145.56/19.29 (equilibrium(v2) = v0)) % 145.56/19.29 % 145.56/19.29 Those formulas are unsatisfiable: % 145.56/19.29 --------------------------------- % 145.56/19.29 % 145.56/19.29 Begin of proof % 145.56/19.29 | % 145.56/19.29 | ALPHA: (mp_greater_or_equal) implies: % 145.56/19.29 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) % 145.56/19.29 | | greater_or_equal(v0, v1)) % 145.56/19.30 | (2) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ % 145.56/19.30 | greater_or_equal(v0, v1) | greater(v0, v1)) % 145.56/19.30 | % 145.56/19.30 | ALPHA: (d2) implies: % 145.86/19.30 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 145.86/19.30 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ subpopulations(v1, v2, v0, v3) | % 145.86/19.30 | ~ environment(v0) | ? [v4: $i] : ? [v5: $i] : (( ~ outcompetes(v2, % 145.86/19.30 | v1, v3) | (growth_rate(v2, v3) = v4 & growth_rate(v1, v3) = v5 % 145.86/19.30 | & $i(v5) & $i(v4) & greater_or_equal(v4, zero) & greater(zero, % 145.86/19.30 | v5))) & (outcompetes(v2, v1, v3) | (growth_rate(v2, v3) = v4 % 145.86/19.30 | & $i(v4) & ~ greater_or_equal(v4, zero)) | (growth_rate(v1, % 145.86/19.30 | v3) = v5 & $i(v5) & ~ greater(zero, v5))))) % 145.86/19.30 | % 145.86/19.30 | ALPHA: (l6) implies: % 145.86/19.30 | (4) $i(zero) % 145.86/19.30 | (5) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 145.86/19.30 | subpopulations(first_movers, efficient_producers, v0, v1) | ~ % 145.86/19.30 | environment(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ((v4 = % 145.86/19.30 | zero & v3 = zero & growth_rate(efficient_producers, v1) = zero & % 145.86/19.30 | growth_rate(first_movers, v1) = zero) | (equilibrium(v0) = v2 & % 145.86/19.30 | $i(v2) & ~ greater_or_equal(v1, v2)) | % 145.86/19.30 | (growth_rate(efficient_producers, v1) = v4 & % 145.86/19.30 | growth_rate(first_movers, v1) = v3 & $i(v4) & $i(v3) & % 145.86/19.30 | greater(v4, zero) & greater(zero, v3)) | % 145.86/19.30 | (growth_rate(efficient_producers, v1) = v4 & % 145.86/19.30 | growth_rate(first_movers, v1) = v3 & $i(v4) & $i(v3) & % 145.86/19.30 | greater(v3, zero) & greater(zero, v4)))) % 145.86/19.30 | % 145.86/19.30 | ALPHA: (l1) implies: % 145.86/19.30 | (6) ! [v0: $i] : ( ~ $i(v0) | ~ stable(v0) | ~ environment(v0) | ? [v1: % 145.86/19.30 | $i] : ($i(v1) & in_environment(v0, v1) & ! [v2: $i] : ( ~ $i(v2) | % 145.86/19.30 | ~ subpopulations(first_movers, efficient_producers, v0, v2) | ~ % 145.86/19.30 | greater_or_equal(v2, v1) | ? [v3: $i] : ? [v4: $i] : % 145.86/19.30 | (growth_rate(efficient_producers, v2) = v3 & % 145.86/19.30 | growth_rate(first_movers, v2) = v4 & $i(v4) & $i(v3) & % 145.86/19.31 | greater(v3, v4))))) % 145.86/19.31 | % 145.86/19.31 | ALPHA: (prove_t4) implies: % 145.86/19.31 | (7) $i(first_movers) % 145.86/19.31 | (8) $i(efficient_producers) % 145.86/19.31 | (9) ? [v0: $i] : ($i(v0) & stable(v0) & environment(v0) & ! [v1: $i] : ( % 145.86/19.31 | ~ $i(v1) | ~ in_environment(v0, v1) | ? [v2: $i] : ($i(v2) & % 145.86/19.31 | subpopulations(first_movers, efficient_producers, v0, v2) & % 145.86/19.31 | greater_or_equal(v2, v1) & ~ outcompetes(efficient_producers, % 145.86/19.31 | first_movers, v2)))) % 145.86/19.31 | % 145.86/19.31 | ALPHA: (function-axioms) implies: % 145.86/19.31 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 145.86/19.31 | (equilibrium(v2) = v1) | ~ (equilibrium(v2) = v0)) % 145.86/19.31 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 145.86/19.31 | (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 145.86/19.31 | % 145.86/19.31 | DELTA: instantiating (9) with fresh symbol all_12_0 gives: % 145.86/19.31 | (12) $i(all_12_0) & stable(all_12_0) & environment(all_12_0) & ! [v0: $i] % 145.86/19.31 | : ( ~ $i(v0) | ~ in_environment(all_12_0, v0) | ? [v1: $i] : ($i(v1) % 145.86/19.31 | & subpopulations(first_movers, efficient_producers, all_12_0, v1) % 145.86/19.31 | & greater_or_equal(v1, v0) & ~ outcompetes(efficient_producers, % 145.86/19.31 | first_movers, v1))) % 145.86/19.31 | % 145.86/19.31 | ALPHA: (12) implies: % 145.86/19.31 | (13) environment(all_12_0) % 145.86/19.31 | (14) stable(all_12_0) % 145.86/19.31 | (15) $i(all_12_0) % 145.86/19.31 | (16) ! [v0: $i] : ( ~ $i(v0) | ~ in_environment(all_12_0, v0) | ? [v1: % 145.86/19.31 | $i] : ($i(v1) & subpopulations(first_movers, efficient_producers, % 145.86/19.31 | all_12_0, v1) & greater_or_equal(v1, v0) & ~ % 145.86/19.31 | outcompetes(efficient_producers, first_movers, v1))) % 145.86/19.31 | % 145.86/19.32 | GROUND_INST: instantiating (a4) with all_12_0, simplifying with (13), (14), % 145.86/19.32 | (15) gives: % 145.86/19.32 | (17) ? [v0: $i] : ? [v1: $i] : (equilibrium(all_12_0) = v0 & $i(v1) & % 145.86/19.32 | $i(v0) & greater_or_equal(v1, v0) & in_environment(all_12_0, v1)) % 145.86/19.32 | % 145.86/19.32 | GROUND_INST: instantiating (6) with all_12_0, simplifying with (13), (14), % 145.86/19.32 | (15) gives: % 145.86/19.32 | (18) ? [v0: $i] : ($i(v0) & in_environment(all_12_0, v0) & ! [v1: $i] : ( % 145.86/19.32 | ~ $i(v1) | ~ subpopulations(first_movers, efficient_producers, % 145.86/19.32 | all_12_0, v1) | ~ greater_or_equal(v1, v0) | ? [v2: $i] : ? % 145.86/19.32 | [v3: $i] : (growth_rate(efficient_producers, v1) = v2 & % 145.86/19.32 | growth_rate(first_movers, v1) = v3 & $i(v3) & $i(v2) & % 145.86/19.32 | greater(v2, v3)))) % 145.86/19.32 | % 145.86/19.32 | DELTA: instantiating (17) with fresh symbols all_20_0, all_20_1 gives: % 145.86/19.32 | (19) equilibrium(all_12_0) = all_20_1 & $i(all_20_0) & $i(all_20_1) & % 145.86/19.32 | greater_or_equal(all_20_0, all_20_1) & in_environment(all_12_0, % 145.86/19.32 | all_20_0) % 145.86/19.32 | % 145.86/19.32 | ALPHA: (19) implies: % 145.86/19.32 | (20) in_environment(all_12_0, all_20_0) % 145.86/19.32 | (21) greater_or_equal(all_20_0, all_20_1) % 145.86/19.32 | (22) $i(all_20_1) % 145.86/19.32 | (23) $i(all_20_0) % 145.86/19.32 | (24) equilibrium(all_12_0) = all_20_1 % 145.86/19.32 | % 145.86/19.32 | DELTA: instantiating (18) with fresh symbol all_22_0 gives: % 145.86/19.32 | (25) $i(all_22_0) & in_environment(all_12_0, all_22_0) & ! [v0: $i] : ( ~ % 145.86/19.32 | $i(v0) | ~ subpopulations(first_movers, efficient_producers, % 145.86/19.32 | all_12_0, v0) | ~ greater_or_equal(v0, all_22_0) | ? [v1: $i] : % 145.86/19.32 | ? [v2: $i] : (growth_rate(efficient_producers, v0) = v1 & % 145.86/19.32 | growth_rate(first_movers, v0) = v2 & $i(v2) & $i(v1) & greater(v1, % 145.86/19.32 | v2))) % 145.86/19.32 | % 145.86/19.32 | ALPHA: (25) implies: % 145.86/19.32 | (26) in_environment(all_12_0, all_22_0) % 145.86/19.32 | (27) $i(all_22_0) % 145.86/19.32 | (28) ! [v0: $i] : ( ~ $i(v0) | ~ subpopulations(first_movers, % 145.86/19.32 | efficient_producers, all_12_0, v0) | ~ greater_or_equal(v0, % 145.86/19.33 | all_22_0) | ? [v1: $i] : ? [v2: $i] : % 145.86/19.33 | (growth_rate(efficient_producers, v0) = v1 & % 145.86/19.33 | growth_rate(first_movers, v0) = v2 & $i(v2) & $i(v1) & greater(v1, % 145.86/19.33 | v2))) % 145.86/19.33 | % 145.86/19.33 | GROUND_INST: instantiating (16) with all_20_0, simplifying with (20), (23) % 145.86/19.33 | gives: % 145.86/19.33 | (29) ? [v0: $i] : ($i(v0) & subpopulations(first_movers, % 145.86/19.33 | efficient_producers, all_12_0, v0) & greater_or_equal(v0, % 145.86/19.33 | all_20_0) & ~ outcompetes(efficient_producers, first_movers, v0)) % 145.86/19.33 | % 145.86/19.33 | GROUND_INST: instantiating (mp_times_in_environment) with all_12_0, all_20_0, % 145.86/19.33 | all_22_0, simplifying with (15), (20), (23), (26), (27) gives: % 145.86/19.33 | (30) all_22_0 = all_20_0 | greater(all_22_0, all_20_0) | greater(all_20_0, % 145.86/19.33 | all_22_0) % 145.86/19.33 | % 145.86/19.33 | GROUND_INST: instantiating (16) with all_22_0, simplifying with (26), (27) % 145.86/19.33 | gives: % 145.86/19.33 | (31) ? [v0: $i] : ($i(v0) & subpopulations(first_movers, % 145.86/19.33 | efficient_producers, all_12_0, v0) & greater_or_equal(v0, % 145.86/19.33 | all_22_0) & ~ outcompetes(efficient_producers, first_movers, v0)) % 145.86/19.33 | % 145.86/19.33 | GROUND_INST: instantiating (2) with all_20_0, all_20_1, simplifying with (21), % 145.86/19.33 | (22), (23) gives: % 145.86/19.33 | (32) all_20_0 = all_20_1 | greater(all_20_0, all_20_1) % 145.86/19.33 | % 145.86/19.33 | DELTA: instantiating (31) with fresh symbol all_30_0 gives: % 145.86/19.33 | (33) $i(all_30_0) & subpopulations(first_movers, efficient_producers, % 145.86/19.33 | all_12_0, all_30_0) & greater_or_equal(all_30_0, all_22_0) & ~ % 145.86/19.33 | outcompetes(efficient_producers, first_movers, all_30_0) % 145.86/19.33 | % 145.86/19.33 | ALPHA: (33) implies: % 145.86/19.33 | (34) ~ outcompetes(efficient_producers, first_movers, all_30_0) % 145.86/19.33 | (35) greater_or_equal(all_30_0, all_22_0) % 145.86/19.33 | (36) subpopulations(first_movers, efficient_producers, all_12_0, all_30_0) % 145.86/19.33 | (37) $i(all_30_0) % 145.86/19.33 | % 145.86/19.33 | DELTA: instantiating (29) with fresh symbol all_32_0 gives: % 145.86/19.33 | (38) $i(all_32_0) & subpopulations(first_movers, efficient_producers, % 145.86/19.33 | all_12_0, all_32_0) & greater_or_equal(all_32_0, all_20_0) & ~ % 145.86/19.33 | outcompetes(efficient_producers, first_movers, all_32_0) % 145.86/19.33 | % 145.86/19.33 | ALPHA: (38) implies: % 145.86/19.33 | (39) ~ outcompetes(efficient_producers, first_movers, all_32_0) % 145.86/19.33 | (40) greater_or_equal(all_32_0, all_20_0) % 145.86/19.33 | (41) subpopulations(first_movers, efficient_producers, all_12_0, all_32_0) % 145.86/19.33 | (42) $i(all_32_0) % 145.86/19.33 | % 145.86/19.33 | GROUND_INST: instantiating (2) with all_30_0, all_22_0, simplifying with (27), % 145.86/19.33 | (35), (37) gives: % 145.86/19.33 | (43) all_30_0 = all_22_0 | greater(all_30_0, all_22_0) % 145.86/19.33 | % 145.86/19.34 | GROUND_INST: instantiating (2) with all_32_0, all_20_0, simplifying with (23), % 145.86/19.34 | (40), (42) gives: % 145.86/19.34 | (44) all_32_0 = all_20_0 | greater(all_32_0, all_20_0) % 145.86/19.34 | % 145.86/19.34 | GROUND_INST: instantiating (3) with all_12_0, first_movers, % 145.86/19.34 | efficient_producers, all_30_0, simplifying with (7), (8), (13), % 145.86/19.34 | (15), (36), (37) gives: % 145.86/19.34 | (45) ? [v0: $i] : ? [v1: $i] : (( ~ outcompetes(efficient_producers, % 145.86/19.34 | first_movers, all_30_0) | (growth_rate(efficient_producers, % 145.86/19.34 | all_30_0) = v0 & growth_rate(first_movers, all_30_0) = v1 & % 145.86/19.34 | $i(v1) & $i(v0) & greater_or_equal(v0, zero) & greater(zero, % 145.86/19.34 | v1))) & (outcompetes(efficient_producers, first_movers, % 145.86/19.34 | all_30_0) | (growth_rate(efficient_producers, all_30_0) = v0 & % 145.86/19.34 | $i(v0) & ~ greater_or_equal(v0, zero)) | % 145.86/19.34 | (growth_rate(first_movers, all_30_0) = v1 & $i(v1) & ~ % 145.86/19.34 | greater(zero, v1)))) % 145.86/19.34 | % 145.86/19.34 | GROUND_INST: instantiating (5) with all_12_0, all_30_0, simplifying with (13), % 145.86/19.34 | (15), (36), (37) gives: % 145.86/19.34 | (46) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ((v2 = zero & v1 = zero & % 145.86/19.34 | growth_rate(efficient_producers, all_30_0) = zero & % 145.86/19.34 | growth_rate(first_movers, all_30_0) = zero) | % 145.86/19.34 | (equilibrium(all_12_0) = v0 & $i(v0) & ~ greater_or_equal(all_30_0, % 145.86/19.34 | v0)) | (growth_rate(efficient_producers, all_30_0) = v2 & % 145.86/19.34 | growth_rate(first_movers, all_30_0) = v1 & $i(v2) & $i(v1) & % 145.86/19.34 | greater(v2, zero) & greater(zero, v1)) | % 145.86/19.34 | (growth_rate(efficient_producers, all_30_0) = v2 & % 145.86/19.34 | growth_rate(first_movers, all_30_0) = v1 & $i(v2) & $i(v1) & % 145.86/19.34 | greater(v1, zero) & greater(zero, v2))) % 145.86/19.34 | % 145.86/19.34 | GROUND_INST: instantiating (28) with all_30_0, simplifying with (35), (36), % 145.86/19.34 | (37) gives: % 145.86/19.34 | (47) ? [v0: $i] : ? [v1: $i] : (growth_rate(efficient_producers, % 145.86/19.34 | all_30_0) = v0 & growth_rate(first_movers, all_30_0) = v1 & $i(v1) % 145.86/19.34 | & $i(v0) & greater(v0, v1)) % 145.86/19.34 | % 145.86/19.34 | GROUND_INST: instantiating (3) with all_12_0, first_movers, % 145.86/19.34 | efficient_producers, all_32_0, simplifying with (7), (8), (13), % 145.86/19.34 | (15), (41), (42) gives: % 145.86/19.35 | (48) ? [v0: $i] : ? [v1: $i] : (( ~ outcompetes(efficient_producers, % 145.86/19.35 | first_movers, all_32_0) | (growth_rate(efficient_producers, % 145.86/19.35 | all_32_0) = v0 & growth_rate(first_movers, all_32_0) = v1 & % 145.86/19.35 | $i(v1) & $i(v0) & greater_or_equal(v0, zero) & greater(zero, % 145.86/19.35 | v1))) & (outcompetes(efficient_producers, first_movers, % 145.86/19.35 | all_32_0) | (growth_rate(efficient_producers, all_32_0) = v0 & % 145.86/19.35 | $i(v0) & ~ greater_or_equal(v0, zero)) | % 145.86/19.35 | (growth_rate(first_movers, all_32_0) = v1 & $i(v1) & ~ % 145.86/19.35 | greater(zero, v1)))) % 145.86/19.35 | % 145.86/19.35 | GROUND_INST: instantiating (5) with all_12_0, all_32_0, simplifying with (13), % 145.86/19.35 | (15), (41), (42) gives: % 145.86/19.35 | (49) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ((v2 = zero & v1 = zero & % 145.86/19.35 | growth_rate(efficient_producers, all_32_0) = zero & % 145.86/19.35 | growth_rate(first_movers, all_32_0) = zero) | % 145.86/19.35 | (equilibrium(all_12_0) = v0 & $i(v0) & ~ greater_or_equal(all_32_0, % 145.86/19.35 | v0)) | (growth_rate(efficient_producers, all_32_0) = v2 & % 145.86/19.35 | growth_rate(first_movers, all_32_0) = v1 & $i(v2) & $i(v1) & % 145.86/19.35 | greater(v2, zero) & greater(zero, v1)) | % 145.86/19.35 | (growth_rate(efficient_producers, all_32_0) = v2 & % 145.86/19.35 | growth_rate(first_movers, all_32_0) = v1 & $i(v2) & $i(v1) & % 145.86/19.35 | greater(v1, zero) & greater(zero, v2))) % 145.86/19.35 | % 145.86/19.35 | GROUND_INST: instantiating (28) with all_32_0, simplifying with (41), (42) % 145.86/19.35 | gives: % 145.86/19.35 | (50) ~ greater_or_equal(all_32_0, all_22_0) | ? [v0: $i] : ? [v1: $i] : % 145.86/19.35 | (growth_rate(efficient_producers, all_32_0) = v0 & % 145.86/19.35 | growth_rate(first_movers, all_32_0) = v1 & $i(v1) & $i(v0) & % 145.86/19.35 | greater(v0, v1)) % 145.86/19.35 | % 145.86/19.35 | DELTA: instantiating (47) with fresh symbols all_39_0, all_39_1 gives: % 145.86/19.35 | (51) growth_rate(efficient_producers, all_30_0) = all_39_1 & % 145.86/19.35 | growth_rate(first_movers, all_30_0) = all_39_0 & $i(all_39_0) & % 145.86/19.35 | $i(all_39_1) & greater(all_39_1, all_39_0) % 145.86/19.35 | % 145.86/19.35 | ALPHA: (51) implies: % 145.86/19.35 | (52) greater(all_39_1, all_39_0) % 145.86/19.35 | (53) $i(all_39_1) % 145.86/19.35 | (54) $i(all_39_0) % 145.86/19.35 | (55) growth_rate(first_movers, all_30_0) = all_39_0 % 145.86/19.35 | (56) growth_rate(efficient_producers, all_30_0) = all_39_1 % 145.86/19.35 | % 145.86/19.35 | DELTA: instantiating (48) with fresh symbols all_41_0, all_41_1 gives: % 145.86/19.36 | (57) ( ~ outcompetes(efficient_producers, first_movers, all_32_0) | % 145.86/19.36 | (growth_rate(efficient_producers, all_32_0) = all_41_1 & % 145.86/19.36 | growth_rate(first_movers, all_32_0) = all_41_0 & $i(all_41_0) & % 145.86/19.36 | $i(all_41_1) & greater_or_equal(all_41_1, zero) & greater(zero, % 145.86/19.36 | all_41_0))) & (outcompetes(efficient_producers, first_movers, % 145.86/19.36 | all_32_0) | (growth_rate(efficient_producers, all_32_0) = all_41_1 % 145.86/19.36 | & $i(all_41_1) & ~ greater_or_equal(all_41_1, zero)) | % 145.86/19.36 | (growth_rate(first_movers, all_32_0) = all_41_0 & $i(all_41_0) & ~ % 145.86/19.36 | greater(zero, all_41_0))) % 145.86/19.36 | % 145.86/19.36 | ALPHA: (57) implies: % 145.86/19.36 | (58) outcompetes(efficient_producers, first_movers, all_32_0) | % 145.86/19.36 | (growth_rate(efficient_producers, all_32_0) = all_41_1 & $i(all_41_1) % 145.86/19.36 | & ~ greater_or_equal(all_41_1, zero)) | (growth_rate(first_movers, % 145.86/19.36 | all_32_0) = all_41_0 & $i(all_41_0) & ~ greater(zero, all_41_0)) % 145.86/19.36 | % 145.86/19.36 | DELTA: instantiating (45) with fresh symbols all_42_0, all_42_1 gives: % 145.86/19.36 | (59) ( ~ outcompetes(efficient_producers, first_movers, all_30_0) | % 145.86/19.36 | (growth_rate(efficient_producers, all_30_0) = all_42_1 & % 145.86/19.36 | growth_rate(first_movers, all_30_0) = all_42_0 & $i(all_42_0) & % 145.86/19.36 | $i(all_42_1) & greater_or_equal(all_42_1, zero) & greater(zero, % 145.86/19.36 | all_42_0))) & (outcompetes(efficient_producers, first_movers, % 145.86/19.36 | all_30_0) | (growth_rate(efficient_producers, all_30_0) = all_42_1 % 145.86/19.36 | & $i(all_42_1) & ~ greater_or_equal(all_42_1, zero)) | % 145.86/19.36 | (growth_rate(first_movers, all_30_0) = all_42_0 & $i(all_42_0) & ~ % 145.86/19.36 | greater(zero, all_42_0))) % 145.86/19.36 | % 145.86/19.36 | ALPHA: (59) implies: % 145.86/19.36 | (60) outcompetes(efficient_producers, first_movers, all_30_0) | % 145.86/19.36 | (growth_rate(efficient_producers, all_30_0) = all_42_1 & $i(all_42_1) % 145.86/19.36 | & ~ greater_or_equal(all_42_1, zero)) | (growth_rate(first_movers, % 145.86/19.36 | all_30_0) = all_42_0 & $i(all_42_0) & ~ greater(zero, all_42_0)) % 145.86/19.36 | % 145.86/19.36 | DELTA: instantiating (46) with fresh symbols all_43_0, all_43_1, all_43_2 % 145.86/19.36 | gives: % 145.86/19.36 | (61) (all_43_0 = zero & all_43_1 = zero & growth_rate(efficient_producers, % 145.86/19.36 | all_30_0) = zero & growth_rate(first_movers, all_30_0) = zero) | % 145.86/19.36 | (equilibrium(all_12_0) = all_43_2 & $i(all_43_2) & ~ % 145.86/19.36 | greater_or_equal(all_30_0, all_43_2)) | % 145.86/19.36 | (growth_rate(efficient_producers, all_30_0) = all_43_0 & % 145.86/19.36 | growth_rate(first_movers, all_30_0) = all_43_1 & $i(all_43_0) & % 145.86/19.36 | $i(all_43_1) & greater(all_43_0, zero) & greater(zero, all_43_1)) | % 145.86/19.36 | (growth_rate(efficient_producers, all_30_0) = all_43_0 & % 145.86/19.36 | growth_rate(first_movers, all_30_0) = all_43_1 & $i(all_43_0) & % 145.86/19.36 | $i(all_43_1) & greater(all_43_1, zero) & greater(zero, all_43_0)) % 145.86/19.36 | % 145.86/19.36 | DELTA: instantiating (49) with fresh symbols all_44_0, all_44_1, all_44_2 % 145.86/19.36 | gives: % 145.86/19.36 | (62) (all_44_0 = zero & all_44_1 = zero & growth_rate(efficient_producers, % 145.86/19.36 | all_32_0) = zero & growth_rate(first_movers, all_32_0) = zero) | % 145.86/19.36 | (equilibrium(all_12_0) = all_44_2 & $i(all_44_2) & ~ % 145.86/19.36 | greater_or_equal(all_32_0, all_44_2)) | % 145.86/19.36 | (growth_rate(efficient_producers, all_32_0) = all_44_0 & % 145.86/19.36 | growth_rate(first_movers, all_32_0) = all_44_1 & $i(all_44_0) & % 145.86/19.36 | $i(all_44_1) & greater(all_44_0, zero) & greater(zero, all_44_1)) | % 145.86/19.37 | (growth_rate(efficient_producers, all_32_0) = all_44_0 & % 145.86/19.37 | growth_rate(first_movers, all_32_0) = all_44_1 & $i(all_44_0) & % 145.86/19.37 | $i(all_44_1) & greater(all_44_1, zero) & greater(zero, all_44_0)) % 145.86/19.37 | % 145.86/19.37 | GROUND_INST: instantiating (11) with all_39_0, all_39_1, all_30_0, % 145.86/19.37 | first_movers, simplifying with (55) gives: % 145.86/19.37 | (63) all_39_0 = all_39_1 | ~ (growth_rate(first_movers, all_30_0) = % 145.86/19.37 | all_39_1) % 145.86/19.37 | % 145.86/19.37 | GROUND_INST: instantiating (1) with all_39_1, all_39_0, simplifying with (52), % 145.86/19.37 | (53), (54) gives: % 145.86/19.37 | (64) greater_or_equal(all_39_1, all_39_0) % 145.86/19.37 | % 145.86/19.37 | BETA: splitting (32) gives: % 145.86/19.37 | % 145.86/19.37 | Case 1: % 145.86/19.37 | | % 145.86/19.37 | | (65) greater(all_20_0, all_20_1) % 145.86/19.37 | | % 145.86/19.37 | | BETA: splitting (30) gives: % 145.86/19.37 | | % 145.86/19.37 | | Case 1: % 145.86/19.37 | | | % 145.86/19.37 | | | (66) greater(all_22_0, all_20_0) % 145.86/19.37 | | | % 145.86/19.37 | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_22_0, % 145.86/19.37 | | | all_20_0, all_20_1, simplifying with (22), (23), (27), (65), % 145.86/19.37 | | | (66) gives: % 145.86/19.37 | | | (67) greater(all_22_0, all_20_1) % 145.86/19.37 | | | % 145.86/19.37 | | | REF_CLOSE: (1), (4), (10), (11), (22), (24), (27), (34), (37), (43), (52), % 145.86/19.37 | | | (55), (56), (60), (61), (63), (64), (67), % 145.86/19.37 | | | (mp_greater_transitivity) are inconsistent by sub-proof #8. % 145.86/19.37 | | | % 145.86/19.37 | | Case 2: % 145.86/19.37 | | | % 145.86/19.38 | | | (68) ~ greater(all_22_0, all_20_0) % 145.86/19.38 | | | (69) all_22_0 = all_20_0 | greater(all_20_0, all_22_0) % 145.86/19.38 | | | % 145.86/19.38 | | | BETA: splitting (50) gives: % 145.86/19.38 | | | % 145.86/19.38 | | | Case 1: % 145.86/19.38 | | | | % 145.86/19.38 | | | | (70) ~ greater_or_equal(all_32_0, all_22_0) % 145.86/19.38 | | | | % 145.86/19.38 | | | | PRED_UNIFY: (40), (70) imply: % 145.86/19.38 | | | | (71) ~ (all_22_0 = all_20_0) % 145.86/19.38 | | | | % 145.86/19.38 | | | | BETA: splitting (69) gives: % 145.86/19.38 | | | | % 145.86/19.38 | | | | Case 1: % 145.86/19.38 | | | | | % 145.86/19.38 | | | | | (72) greater(all_20_0, all_22_0) % 145.86/19.38 | | | | | % 145.86/19.38 | | | | | GROUND_INST: instantiating (1) with all_20_0, all_22_0, simplifying % 145.86/19.38 | | | | | with (23), (27), (72) gives: % 145.86/19.38 | | | | | (73) greater_or_equal(all_20_0, all_22_0) % 145.86/19.38 | | | | | % 145.86/19.38 | | | | | PRED_UNIFY: (70), (73) imply: % 145.86/19.38 | | | | | (74) ~ (all_32_0 = all_20_0) % 145.86/19.38 | | | | | % 145.86/19.38 | | | | | BETA: splitting (44) gives: % 145.86/19.38 | | | | | % 145.86/19.38 | | | | | Case 1: % 145.86/19.38 | | | | | | % 145.86/19.38 | | | | | | (75) greater(all_32_0, all_20_0) % 145.86/19.38 | | | | | | % 145.86/19.38 | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_32_0, % 145.86/19.38 | | | | | | all_20_0, all_22_0, simplifying with (23), (27), (42), % 145.86/19.38 | | | | | | (72), (75) gives: % 145.86/19.38 | | | | | | (76) greater(all_32_0, all_22_0) % 145.86/19.38 | | | | | | % 145.86/19.38 | | | | | | GROUND_INST: instantiating (1) with all_32_0, all_22_0, simplifying % 145.86/19.38 | | | | | | with (27), (42), (70), (76) gives: % 145.86/19.38 | | | | | | (77) $false % 145.86/19.38 | | | | | | % 145.86/19.38 | | | | | | CLOSE: (77) is inconsistent. % 145.86/19.38 | | | | | | % 145.86/19.38 | | | | | Case 2: % 145.86/19.38 | | | | | | % 145.86/19.38 | | | | | | (78) all_32_0 = all_20_0 % 145.86/19.38 | | | | | | % 145.86/19.38 | | | | | | REDUCE: (74), (78) imply: % 145.86/19.38 | | | | | | (79) $false % 145.86/19.38 | | | | | | % 145.86/19.38 | | | | | | CLOSE: (79) is inconsistent. % 145.86/19.38 | | | | | | % 145.86/19.38 | | | | | End of split % 145.86/19.38 | | | | | % 145.86/19.38 | | | | Case 2: % 145.86/19.38 | | | | | % 145.86/19.38 | | | | | (80) all_22_0 = all_20_0 % 145.86/19.38 | | | | | % 145.86/19.38 | | | | | REDUCE: (71), (80) imply: % 145.86/19.38 | | | | | (81) $false % 145.86/19.38 | | | | | % 145.86/19.38 | | | | | CLOSE: (81) is inconsistent. % 145.86/19.38 | | | | | % 145.86/19.38 | | | | End of split % 145.86/19.38 | | | | % 145.86/19.38 | | | Case 2: % 145.86/19.38 | | | | % 145.86/19.38 | | | | (82) greater_or_equal(all_32_0, all_22_0) % 145.86/19.39 | | | | (83) ? [v0: $i] : ? [v1: $i] : (growth_rate(efficient_producers, % 145.86/19.39 | | | | all_32_0) = v0 & growth_rate(first_movers, all_32_0) = v1 & % 145.86/19.39 | | | | $i(v1) & $i(v0) & greater(v0, v1)) % 145.86/19.39 | | | | % 145.86/19.39 | | | | DELTA: instantiating (83) with fresh symbols all_83_0, all_83_1 gives: % 145.86/19.39 | | | | (84) growth_rate(efficient_producers, all_32_0) = all_83_1 & % 145.86/19.39 | | | | growth_rate(first_movers, all_32_0) = all_83_0 & $i(all_83_0) & % 145.86/19.39 | | | | $i(all_83_1) & greater(all_83_1, all_83_0) % 145.86/19.39 | | | | % 145.86/19.39 | | | | ALPHA: (84) implies: % 145.86/19.39 | | | | (85) greater(all_83_1, all_83_0) % 145.86/19.39 | | | | (86) $i(all_83_1) % 145.86/19.39 | | | | (87) $i(all_83_0) % 145.86/19.39 | | | | (88) growth_rate(first_movers, all_32_0) = all_83_0 % 145.86/19.39 | | | | (89) growth_rate(efficient_producers, all_32_0) = all_83_1 % 145.86/19.39 | | | | % 145.86/19.39 | | | | GROUND_INST: instantiating (1) with all_83_1, all_83_0, simplifying with % 145.86/19.39 | | | | (85), (86), (87) gives: % 145.86/19.39 | | | | (90) greater_or_equal(all_83_1, all_83_0) % 145.86/19.39 | | | | % 145.86/19.39 | | | | GROUND_INST: instantiating (2) with all_32_0, all_22_0, simplifying with % 145.86/19.39 | | | | (27), (42), (82) gives: % 145.86/19.39 | | | | (91) all_32_0 = all_22_0 | greater(all_32_0, all_22_0) % 145.86/19.39 | | | | % 145.86/19.39 | | | | BETA: splitting (44) gives: % 145.86/19.39 | | | | % 145.86/19.39 | | | | Case 1: % 145.86/19.39 | | | | | % 145.86/19.39 | | | | | (92) greater(all_32_0, all_20_0) % 145.86/19.39 | | | | | % 145.86/19.39 | | | | | PRED_UNIFY: (68), (92) imply: % 145.86/19.39 | | | | | (93) ~ (all_32_0 = all_22_0) % 145.86/19.39 | | | | | % 145.86/19.39 | | | | | BETA: splitting (91) gives: % 145.86/19.39 | | | | | % 145.86/19.39 | | | | | Case 1: % 145.86/19.39 | | | | | | % 145.86/19.39 | | | | | | % 145.86/19.39 | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_32_0, % 145.86/19.39 | | | | | | all_20_0, all_20_1, simplifying with (22), (23), (42), % 145.86/19.39 | | | | | | (65), (92) gives: % 145.86/19.39 | | | | | | (94) greater(all_32_0, all_20_1) % 145.86/19.39 | | | | | | % 145.86/19.39 | | | | | | GROUND_INST: instantiating (1) with all_32_0, all_20_1, simplifying % 145.86/19.39 | | | | | | with (22), (42), (94) gives: % 145.86/19.39 | | | | | | (95) greater_or_equal(all_32_0, all_20_1) % 145.86/19.39 | | | | | | % 145.86/19.39 | | | | | | BETA: splitting (58) gives: % 145.86/19.39 | | | | | | % 145.86/19.39 | | | | | | Case 1: % 145.86/19.39 | | | | | | | % 145.86/19.39 | | | | | | | (96) outcompetes(efficient_producers, first_movers, all_32_0) % 145.86/19.39 | | | | | | | % 145.86/19.39 | | | | | | | PRED_UNIFY: (39), (96) imply: % 145.86/19.39 | | | | | | | (97) $false % 145.86/19.39 | | | | | | | % 145.86/19.39 | | | | | | | CLOSE: (97) is inconsistent. % 145.86/19.39 | | | | | | | % 145.86/19.39 | | | | | | Case 2: % 145.86/19.39 | | | | | | | % 145.86/19.39 | | | | | | | (98) (growth_rate(efficient_producers, all_32_0) = all_41_1 & % 145.86/19.39 | | | | | | | $i(all_41_1) & ~ greater_or_equal(all_41_1, zero)) | % 145.86/19.39 | | | | | | | (growth_rate(first_movers, all_32_0) = all_41_0 & % 145.86/19.39 | | | | | | | $i(all_41_0) & ~ greater(zero, all_41_0)) % 145.86/19.39 | | | | | | | % 145.86/19.39 | | | | | | | BETA: splitting (62) gives: % 145.86/19.39 | | | | | | | % 145.86/19.39 | | | | | | | Case 1: % 145.86/19.39 | | | | | | | | % 145.86/19.40 | | | | | | | | (99) (all_44_0 = zero & all_44_1 = zero & % 145.86/19.40 | | | | | | | | growth_rate(efficient_producers, all_32_0) = zero & % 145.86/19.40 | | | | | | | | growth_rate(first_movers, all_32_0) = zero) | % 145.86/19.40 | | | | | | | | (equilibrium(all_12_0) = all_44_2 & $i(all_44_2) & ~ % 145.86/19.40 | | | | | | | | greater_or_equal(all_32_0, all_44_2)) % 145.86/19.40 | | | | | | | | % 145.86/19.40 | | | | | | | | BETA: splitting (99) gives: % 145.86/19.40 | | | | | | | | % 145.86/19.40 | | | | | | | | Case 1: % 145.86/19.40 | | | | | | | | | % 145.86/19.40 | | | | | | | | | (100) all_44_0 = zero & all_44_1 = zero & % 145.86/19.40 | | | | | | | | | growth_rate(efficient_producers, all_32_0) = zero & % 145.86/19.40 | | | | | | | | | growth_rate(first_movers, all_32_0) = zero % 145.86/19.40 | | | | | | | | | % 145.86/19.40 | | | | | | | | | ALPHA: (100) implies: % 146.35/19.40 | | | | | | | | | (101) growth_rate(first_movers, all_32_0) = zero % 146.35/19.40 | | | | | | | | | (102) growth_rate(efficient_producers, all_32_0) = zero % 146.35/19.40 | | | | | | | | | % 146.35/19.40 | | | | | | | | | REF_CLOSE: (11), (85), (88), (89), (90), (98), (101), (102) % 146.35/19.40 | | | | | | | | | are inconsistent by sub-proof #5. % 146.35/19.40 | | | | | | | | | % 146.35/19.40 | | | | | | | | Case 2: % 146.35/19.40 | | | | | | | | | % 146.35/19.40 | | | | | | | | | (103) equilibrium(all_12_0) = all_44_2 & $i(all_44_2) & ~ % 146.35/19.40 | | | | | | | | | greater_or_equal(all_32_0, all_44_2) % 146.35/19.40 | | | | | | | | | % 146.35/19.40 | | | | | | | | | ALPHA: (103) implies: % 146.35/19.40 | | | | | | | | | (104) ~ greater_or_equal(all_32_0, all_44_2) % 146.35/19.40 | | | | | | | | | (105) equilibrium(all_12_0) = all_44_2 % 146.35/19.40 | | | | | | | | | % 146.35/19.40 | | | | | | | | | REF_CLOSE: (10), (24), (95), (104), (105) are inconsistent by % 146.35/19.40 | | | | | | | | | sub-proof #4. % 146.35/19.40 | | | | | | | | | % 146.35/19.40 | | | | | | | | End of split % 146.35/19.40 | | | | | | | | % 146.35/19.40 | | | | | | | Case 2: % 146.35/19.40 | | | | | | | | % 146.35/19.40 | | | | | | | | (106) (growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.40 | | | | | | | | & growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.40 | | | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_0, zero) % 146.35/19.40 | | | | | | | | & greater(zero, all_44_1)) | % 146.35/19.40 | | | | | | | | (growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.40 | | | | | | | | & growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.40 | | | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_1, zero) % 146.35/19.40 | | | | | | | | & greater(zero, all_44_0)) % 146.35/19.40 | | | | | | | | % 146.35/19.40 | | | | | | | | BETA: splitting (106) gives: % 146.35/19.40 | | | | | | | | % 146.35/19.40 | | | | | | | | Case 1: % 146.35/19.40 | | | | | | | | | % 146.35/19.40 | | | | | | | | | (107) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.40 | | | | | | | | | & growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.40 | | | | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_0, zero) % 146.35/19.40 | | | | | | | | | & greater(zero, all_44_1) % 146.35/19.40 | | | | | | | | | % 146.35/19.40 | | | | | | | | | ALPHA: (107) implies: % 146.35/19.40 | | | | | | | | | (108) greater(zero, all_44_1) % 146.35/19.40 | | | | | | | | | (109) greater(all_44_0, zero) % 146.35/19.40 | | | | | | | | | (110) growth_rate(first_movers, all_32_0) = all_44_1 % 146.35/19.40 | | | | | | | | | (111) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | | GROUND_INST: instantiating (11) with all_83_0, all_44_1, % 146.35/19.41 | | | | | | | | | all_32_0, first_movers, simplifying with (88), % 146.35/19.41 | | | | | | | | | (110) gives: % 146.35/19.41 | | | | | | | | | (112) all_83_0 = all_44_1 % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | | GROUND_INST: instantiating (11) with all_83_1, all_44_0, % 146.35/19.41 | | | | | | | | | all_32_0, efficient_producers, simplifying with % 146.35/19.41 | | | | | | | | | (89), (111) gives: % 146.35/19.41 | | | | | | | | | (113) all_83_1 = all_44_0 % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | | REDUCE: (86), (113) imply: % 146.35/19.41 | | | | | | | | | (114) $i(all_44_0) % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | | GROUND_INST: instantiating (1) with all_44_0, zero, simplifying % 146.35/19.41 | | | | | | | | | with (4), (109), (114) gives: % 146.35/19.41 | | | | | | | | | (115) greater_or_equal(all_44_0, zero) % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | | REF_CLOSE: (11), (98), (108), (110), (111), (115) are % 146.35/19.41 | | | | | | | | | inconsistent by sub-proof #3. % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | Case 2: % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | | (116) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.41 | | | | | | | | | & growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.41 | | | | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_1, zero) % 146.35/19.41 | | | | | | | | | & greater(zero, all_44_0) % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | | ALPHA: (116) implies: % 146.35/19.41 | | | | | | | | | (117) greater(zero, all_44_0) % 146.35/19.41 | | | | | | | | | (118) greater(all_44_1, zero) % 146.35/19.41 | | | | | | | | | (119) growth_rate(first_movers, all_32_0) = all_44_1 % 146.35/19.41 | | | | | | | | | (120) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | | GROUND_INST: instantiating (11) with all_83_0, all_44_1, % 146.35/19.41 | | | | | | | | | all_32_0, first_movers, simplifying with (88), % 146.35/19.41 | | | | | | | | | (119) gives: % 146.35/19.41 | | | | | | | | | (121) all_83_0 = all_44_1 % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | | GROUND_INST: instantiating (11) with all_83_1, all_44_0, % 146.35/19.41 | | | | | | | | | all_32_0, efficient_producers, simplifying with % 146.35/19.41 | | | | | | | | | (89), (120) gives: % 146.35/19.41 | | | | | | | | | (122) all_83_1 = all_44_0 % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | | REF_CLOSE: (1), (4), (11), (85), (86), (87), (98), (117), % 146.35/19.41 | | | | | | | | | (118), (119), (120), (121), (122), % 146.35/19.41 | | | | | | | | | (mp_greater_transitivity) are inconsistent by % 146.35/19.41 | | | | | | | | | sub-proof #1. % 146.35/19.41 | | | | | | | | | % 146.35/19.41 | | | | | | | | End of split % 146.35/19.41 | | | | | | | | % 146.35/19.41 | | | | | | | End of split % 146.35/19.41 | | | | | | | % 146.35/19.41 | | | | | | End of split % 146.35/19.41 | | | | | | % 146.35/19.41 | | | | | Case 2: % 146.35/19.41 | | | | | | % 146.35/19.41 | | | | | | (123) all_32_0 = all_22_0 % 146.35/19.41 | | | | | | % 146.35/19.41 | | | | | | REDUCE: (93), (123) imply: % 146.35/19.41 | | | | | | (124) $false % 146.35/19.41 | | | | | | % 146.35/19.41 | | | | | | CLOSE: (124) is inconsistent. % 146.35/19.41 | | | | | | % 146.35/19.41 | | | | | End of split % 146.35/19.41 | | | | | % 146.35/19.41 | | | | Case 2: % 146.35/19.41 | | | | | % 146.35/19.41 | | | | | (125) all_32_0 = all_20_0 % 146.35/19.42 | | | | | % 146.35/19.42 | | | | | REDUCE: (89), (125) imply: % 146.35/19.42 | | | | | (126) growth_rate(efficient_producers, all_20_0) = all_83_1 % 146.35/19.42 | | | | | % 146.35/19.42 | | | | | REDUCE: (88), (125) imply: % 146.35/19.42 | | | | | (127) growth_rate(first_movers, all_20_0) = all_83_0 % 146.35/19.42 | | | | | % 146.35/19.42 | | | | | BETA: splitting (58) gives: % 146.35/19.42 | | | | | % 146.35/19.42 | | | | | Case 1: % 146.35/19.42 | | | | | | % 146.35/19.42 | | | | | | (128) outcompetes(efficient_producers, first_movers, all_32_0) % 146.35/19.42 | | | | | | % 146.35/19.42 | | | | | | PRED_UNIFY: (39), (128) imply: % 146.35/19.42 | | | | | | (129) $false % 146.35/19.42 | | | | | | % 146.35/19.42 | | | | | | CLOSE: (129) is inconsistent. % 146.35/19.42 | | | | | | % 146.35/19.42 | | | | | Case 2: % 146.35/19.42 | | | | | | % 146.35/19.42 | | | | | | (130) (growth_rate(efficient_producers, all_32_0) = all_41_1 & % 146.35/19.42 | | | | | | $i(all_41_1) & ~ greater_or_equal(all_41_1, zero)) | % 146.35/19.42 | | | | | | (growth_rate(first_movers, all_32_0) = all_41_0 & % 146.35/19.42 | | | | | | $i(all_41_0) & ~ greater(zero, all_41_0)) % 146.35/19.42 | | | | | | % 146.35/19.42 | | | | | | BETA: splitting (62) gives: % 146.35/19.42 | | | | | | % 146.35/19.42 | | | | | | Case 1: % 146.35/19.42 | | | | | | | % 146.35/19.42 | | | | | | | (131) (all_44_0 = zero & all_44_1 = zero & % 146.35/19.42 | | | | | | | growth_rate(efficient_producers, all_32_0) = zero & % 146.35/19.42 | | | | | | | growth_rate(first_movers, all_32_0) = zero) | % 146.35/19.42 | | | | | | | (equilibrium(all_12_0) = all_44_2 & $i(all_44_2) & ~ % 146.35/19.42 | | | | | | | greater_or_equal(all_32_0, all_44_2)) % 146.35/19.42 | | | | | | | % 146.35/19.42 | | | | | | | BETA: splitting (131) gives: % 146.35/19.42 | | | | | | | % 146.35/19.42 | | | | | | | Case 1: % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | | (132) all_44_0 = zero & all_44_1 = zero & % 146.35/19.42 | | | | | | | | growth_rate(efficient_producers, all_32_0) = zero & % 146.35/19.42 | | | | | | | | growth_rate(first_movers, all_32_0) = zero % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | | ALPHA: (132) implies: % 146.35/19.42 | | | | | | | | (133) growth_rate(first_movers, all_32_0) = zero % 146.35/19.42 | | | | | | | | (134) growth_rate(efficient_producers, all_32_0) = zero % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | | REF_CLOSE: (11), (85), (88), (89), (90), (130), (133), (134) are % 146.35/19.42 | | | | | | | | inconsistent by sub-proof #5. % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | Case 2: % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | | (135) equilibrium(all_12_0) = all_44_2 & $i(all_44_2) & ~ % 146.35/19.42 | | | | | | | | greater_or_equal(all_32_0, all_44_2) % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | | ALPHA: (135) implies: % 146.35/19.42 | | | | | | | | (136) ~ greater_or_equal(all_32_0, all_44_2) % 146.35/19.42 | | | | | | | | (137) equilibrium(all_12_0) = all_44_2 % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | | REDUCE: (125), (136) imply: % 146.35/19.42 | | | | | | | | (138) ~ greater_or_equal(all_20_0, all_44_2) % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | | GROUND_INST: instantiating (10) with all_20_1, all_44_2, % 146.35/19.42 | | | | | | | | all_12_0, simplifying with (24), (137) gives: % 146.35/19.42 | | | | | | | | (139) all_44_2 = all_20_1 % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | | PRED_UNIFY: (21), (138) imply: % 146.35/19.42 | | | | | | | | (140) ~ (all_44_2 = all_20_1) % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | | REDUCE: (139), (140) imply: % 146.35/19.42 | | | | | | | | (141) $false % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | | CLOSE: (141) is inconsistent. % 146.35/19.42 | | | | | | | | % 146.35/19.42 | | | | | | | End of split % 146.35/19.42 | | | | | | | % 146.35/19.42 | | | | | | Case 2: % 146.35/19.42 | | | | | | | % 146.35/19.42 | | | | | | | (142) (growth_rate(efficient_producers, all_32_0) = all_44_0 & % 146.35/19.42 | | | | | | | growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.42 | | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_0, zero) & % 146.35/19.42 | | | | | | | greater(zero, all_44_1)) | % 146.35/19.42 | | | | | | | (growth_rate(efficient_producers, all_32_0) = all_44_0 & % 146.35/19.42 | | | | | | | growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.42 | | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_1, zero) & % 146.35/19.42 | | | | | | | greater(zero, all_44_0)) % 146.35/19.43 | | | | | | | % 146.35/19.43 | | | | | | | BETA: splitting (142) gives: % 146.35/19.43 | | | | | | | % 146.35/19.43 | | | | | | | Case 1: % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | (143) growth_rate(efficient_producers, all_32_0) = all_44_0 & % 146.35/19.43 | | | | | | | | growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.43 | | | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_0, zero) & % 146.35/19.43 | | | | | | | | greater(zero, all_44_1) % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | ALPHA: (143) implies: % 146.35/19.43 | | | | | | | | (144) greater(zero, all_44_1) % 146.35/19.43 | | | | | | | | (145) greater(all_44_0, zero) % 146.35/19.43 | | | | | | | | (146) growth_rate(first_movers, all_32_0) = all_44_1 % 146.35/19.43 | | | | | | | | (147) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | REDUCE: (125), (147) imply: % 146.35/19.43 | | | | | | | | (148) growth_rate(efficient_producers, all_20_0) = all_44_0 % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | GROUND_INST: instantiating (11) with all_83_1, all_44_0, % 146.35/19.43 | | | | | | | | all_20_0, efficient_producers, simplifying with % 146.35/19.43 | | | | | | | | (126), (148) gives: % 146.35/19.43 | | | | | | | | (149) all_83_1 = all_44_0 % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | REDUCE: (86), (149) imply: % 146.35/19.43 | | | | | | | | (150) $i(all_44_0) % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | GROUND_INST: instantiating (1) with all_44_0, zero, simplifying % 146.35/19.43 | | | | | | | | with (4), (145), (150) gives: % 146.35/19.43 | | | | | | | | (151) greater_or_equal(all_44_0, zero) % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | REF_CLOSE: (11), (130), (144), (146), (147), (151) are % 146.35/19.43 | | | | | | | | inconsistent by sub-proof #3. % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | Case 2: % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | (152) growth_rate(efficient_producers, all_32_0) = all_44_0 & % 146.35/19.43 | | | | | | | | growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.43 | | | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_1, zero) & % 146.35/19.43 | | | | | | | | greater(zero, all_44_0) % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | ALPHA: (152) implies: % 146.35/19.43 | | | | | | | | (153) greater(zero, all_44_0) % 146.35/19.43 | | | | | | | | (154) greater(all_44_1, zero) % 146.35/19.43 | | | | | | | | (155) growth_rate(first_movers, all_32_0) = all_44_1 % 146.35/19.43 | | | | | | | | (156) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | REDUCE: (125), (156) imply: % 146.35/19.43 | | | | | | | | (157) growth_rate(efficient_producers, all_20_0) = all_44_0 % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | REDUCE: (125), (155) imply: % 146.35/19.43 | | | | | | | | (158) growth_rate(first_movers, all_20_0) = all_44_1 % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | GROUND_INST: instantiating (11) with all_83_0, all_44_1, % 146.35/19.43 | | | | | | | | all_20_0, first_movers, simplifying with (127), % 146.35/19.43 | | | | | | | | (158) gives: % 146.35/19.43 | | | | | | | | (159) all_83_0 = all_44_1 % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | GROUND_INST: instantiating (11) with all_83_1, all_44_0, % 146.35/19.43 | | | | | | | | all_20_0, efficient_producers, simplifying with % 146.35/19.43 | | | | | | | | (126), (157) gives: % 146.35/19.43 | | | | | | | | (160) all_83_1 = all_44_0 % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | | REF_CLOSE: (1), (4), (11), (85), (86), (87), (130), (153), % 146.35/19.43 | | | | | | | | (154), (155), (156), (159), (160), % 146.35/19.43 | | | | | | | | (mp_greater_transitivity) are inconsistent by % 146.35/19.43 | | | | | | | | sub-proof #1. % 146.35/19.43 | | | | | | | | % 146.35/19.43 | | | | | | | End of split % 146.35/19.43 | | | | | | | % 146.35/19.43 | | | | | | End of split % 146.35/19.43 | | | | | | % 146.35/19.43 | | | | | End of split % 146.35/19.43 | | | | | % 146.35/19.43 | | | | End of split % 146.35/19.43 | | | | % 146.35/19.43 | | | End of split % 146.35/19.43 | | | % 146.35/19.43 | | End of split % 146.35/19.43 | | % 146.35/19.43 | Case 2: % 146.35/19.43 | | % 146.35/19.43 | | (161) all_20_0 = all_20_1 % 146.35/19.44 | | % 146.35/19.44 | | REDUCE: (40), (161) imply: % 146.35/19.44 | | (162) greater_or_equal(all_32_0, all_20_1) % 146.35/19.44 | | % 146.35/19.44 | | BETA: splitting (30) gives: % 146.35/19.44 | | % 146.35/19.44 | | Case 1: % 146.35/19.44 | | | % 146.35/19.44 | | | (163) greater(all_22_0, all_20_0) % 146.35/19.44 | | | % 146.35/19.44 | | | REDUCE: (161), (163) imply: % 146.35/19.44 | | | (164) greater(all_22_0, all_20_1) % 146.35/19.44 | | | % 146.35/19.44 | | | REF_CLOSE: (1), (4), (10), (11), (22), (24), (27), (34), (37), (43), (52), % 146.35/19.44 | | | (55), (56), (60), (61), (63), (64), (164), % 146.35/19.44 | | | (mp_greater_transitivity) are inconsistent by sub-proof #8. % 146.35/19.44 | | | % 146.35/19.44 | | Case 2: % 146.35/19.44 | | | % 146.35/19.44 | | | (165) all_22_0 = all_20_0 | greater(all_20_0, all_22_0) % 146.35/19.44 | | | % 146.35/19.44 | | | BETA: splitting (50) gives: % 146.35/19.44 | | | % 146.35/19.44 | | | Case 1: % 146.35/19.44 | | | | % 146.35/19.44 | | | | (166) ~ greater_or_equal(all_32_0, all_22_0) % 146.35/19.44 | | | | % 146.35/19.44 | | | | PRED_UNIFY: (162), (166) imply: % 146.35/19.44 | | | | (167) ~ (all_22_0 = all_20_1) % 146.35/19.44 | | | | % 146.35/19.44 | | | | BETA: splitting (165) gives: % 146.35/19.44 | | | | % 146.35/19.44 | | | | Case 1: % 146.35/19.44 | | | | | % 146.35/19.44 | | | | | (168) greater(all_20_0, all_22_0) % 146.35/19.44 | | | | | % 146.35/19.44 | | | | | REDUCE: (161), (168) imply: % 146.35/19.44 | | | | | (169) greater(all_20_1, all_22_0) % 146.35/19.44 | | | | | % 146.35/19.44 | | | | | GROUND_INST: instantiating (1) with all_20_1, all_22_0, simplifying % 146.35/19.44 | | | | | with (22), (27), (169) gives: % 146.35/19.44 | | | | | (170) greater_or_equal(all_20_1, all_22_0) % 146.35/19.44 | | | | | % 146.35/19.44 | | | | | PRED_UNIFY: (166), (170) imply: % 146.35/19.44 | | | | | (171) ~ (all_32_0 = all_20_1) % 146.35/19.44 | | | | | % 146.35/19.44 | | | | | BETA: splitting (44) gives: % 146.35/19.44 | | | | | % 146.35/19.44 | | | | | Case 1: % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | | (172) greater(all_32_0, all_20_0) % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | | REDUCE: (161), (172) imply: % 146.35/19.44 | | | | | | (173) greater(all_32_0, all_20_1) % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_32_0, % 146.35/19.44 | | | | | | all_20_1, all_22_0, simplifying with (22), (27), (42), % 146.35/19.44 | | | | | | (169), (173) gives: % 146.35/19.44 | | | | | | (174) greater(all_32_0, all_22_0) % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | | GROUND_INST: instantiating (1) with all_32_0, all_22_0, simplifying % 146.35/19.44 | | | | | | with (27), (42), (166), (174) gives: % 146.35/19.44 | | | | | | (175) $false % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | | CLOSE: (175) is inconsistent. % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | Case 2: % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | | (176) all_32_0 = all_20_0 % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | | COMBINE_EQS: (161), (176) imply: % 146.35/19.44 | | | | | | (177) all_32_0 = all_20_1 % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | | REDUCE: (171), (177) imply: % 146.35/19.44 | | | | | | (178) $false % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | | CLOSE: (178) is inconsistent. % 146.35/19.44 | | | | | | % 146.35/19.44 | | | | | End of split % 146.35/19.44 | | | | | % 146.35/19.44 | | | | Case 2: % 146.35/19.44 | | | | | % 146.35/19.44 | | | | | (179) all_22_0 = all_20_0 % 146.35/19.44 | | | | | % 146.35/19.44 | | | | | COMBINE_EQS: (161), (179) imply: % 146.35/19.44 | | | | | (180) all_22_0 = all_20_1 % 146.35/19.44 | | | | | % 146.35/19.44 | | | | | REDUCE: (167), (180) imply: % 146.35/19.44 | | | | | (181) $false % 146.35/19.44 | | | | | % 146.35/19.44 | | | | | CLOSE: (181) is inconsistent. % 146.35/19.44 | | | | | % 146.35/19.44 | | | | End of split % 146.35/19.44 | | | | % 146.35/19.44 | | | Case 2: % 146.35/19.44 | | | | % 146.35/19.45 | | | | (182) ? [v0: $i] : ? [v1: $i] : (growth_rate(efficient_producers, % 146.35/19.45 | | | | all_32_0) = v0 & growth_rate(first_movers, all_32_0) = v1 & % 146.35/19.45 | | | | $i(v1) & $i(v0) & greater(v0, v1)) % 146.35/19.45 | | | | % 146.35/19.45 | | | | DELTA: instantiating (182) with fresh symbols all_83_0, all_83_1 gives: % 146.35/19.45 | | | | (183) growth_rate(efficient_producers, all_32_0) = all_83_1 & % 146.35/19.45 | | | | growth_rate(first_movers, all_32_0) = all_83_0 & $i(all_83_0) & % 146.35/19.45 | | | | $i(all_83_1) & greater(all_83_1, all_83_0) % 146.35/19.45 | | | | % 146.35/19.45 | | | | ALPHA: (183) implies: % 146.35/19.45 | | | | (184) greater(all_83_1, all_83_0) % 146.35/19.45 | | | | (185) $i(all_83_1) % 146.35/19.45 | | | | (186) $i(all_83_0) % 146.35/19.45 | | | | (187) growth_rate(first_movers, all_32_0) = all_83_0 % 146.35/19.45 | | | | (188) growth_rate(efficient_producers, all_32_0) = all_83_1 % 146.35/19.45 | | | | % 146.35/19.45 | | | | GROUND_INST: instantiating (1) with all_83_1, all_83_0, simplifying with % 146.35/19.45 | | | | (184), (185), (186) gives: % 146.35/19.45 | | | | (189) greater_or_equal(all_83_1, all_83_0) % 146.35/19.45 | | | | % 146.35/19.45 | | | | BETA: splitting (58) gives: % 146.35/19.45 | | | | % 146.35/19.45 | | | | Case 1: % 146.35/19.45 | | | | | % 146.35/19.45 | | | | | (190) outcompetes(efficient_producers, first_movers, all_32_0) % 146.35/19.45 | | | | | % 146.35/19.45 | | | | | PRED_UNIFY: (39), (190) imply: % 146.35/19.45 | | | | | (191) $false % 146.35/19.45 | | | | | % 146.35/19.45 | | | | | CLOSE: (191) is inconsistent. % 146.35/19.45 | | | | | % 146.35/19.45 | | | | Case 2: % 146.35/19.45 | | | | | % 146.35/19.45 | | | | | (192) (growth_rate(efficient_producers, all_32_0) = all_41_1 & % 146.35/19.45 | | | | | $i(all_41_1) & ~ greater_or_equal(all_41_1, zero)) | % 146.35/19.45 | | | | | (growth_rate(first_movers, all_32_0) = all_41_0 & % 146.35/19.45 | | | | | $i(all_41_0) & ~ greater(zero, all_41_0)) % 146.35/19.45 | | | | | % 146.35/19.45 | | | | | BETA: splitting (62) gives: % 146.35/19.45 | | | | | % 146.35/19.45 | | | | | Case 1: % 146.35/19.45 | | | | | | % 146.35/19.45 | | | | | | (193) (all_44_0 = zero & all_44_1 = zero & % 146.35/19.45 | | | | | | growth_rate(efficient_producers, all_32_0) = zero & % 146.35/19.45 | | | | | | growth_rate(first_movers, all_32_0) = zero) | % 146.35/19.45 | | | | | | (equilibrium(all_12_0) = all_44_2 & $i(all_44_2) & ~ % 146.35/19.45 | | | | | | greater_or_equal(all_32_0, all_44_2)) % 146.35/19.45 | | | | | | % 146.35/19.45 | | | | | | BETA: splitting (193) gives: % 146.35/19.45 | | | | | | % 146.35/19.45 | | | | | | Case 1: % 146.35/19.45 | | | | | | | % 146.35/19.45 | | | | | | | (194) all_44_0 = zero & all_44_1 = zero & % 146.35/19.45 | | | | | | | growth_rate(efficient_producers, all_32_0) = zero & % 146.35/19.45 | | | | | | | growth_rate(first_movers, all_32_0) = zero % 146.35/19.45 | | | | | | | % 146.35/19.45 | | | | | | | ALPHA: (194) implies: % 146.35/19.45 | | | | | | | (195) growth_rate(first_movers, all_32_0) = zero % 146.35/19.45 | | | | | | | (196) growth_rate(efficient_producers, all_32_0) = zero % 146.35/19.45 | | | | | | | % 146.35/19.45 | | | | | | | GROUND_INST: instantiating (11) with all_83_0, zero, all_32_0, % 146.35/19.45 | | | | | | | first_movers, simplifying with (187), (195) gives: % 146.35/19.45 | | | | | | | (197) all_83_0 = zero % 146.35/19.45 | | | | | | | % 146.35/19.45 | | | | | | | GROUND_INST: instantiating (11) with all_83_1, zero, all_32_0, % 146.35/19.45 | | | | | | | efficient_producers, simplifying with (188), (196) % 146.35/19.45 | | | | | | | gives: % 146.35/19.45 | | | | | | | (198) all_83_1 = zero % 146.35/19.45 | | | | | | | % 146.35/19.45 | | | | | | | REDUCE: (189), (197), (198) imply: % 146.35/19.45 | | | | | | | (199) greater_or_equal(zero, zero) % 146.35/19.45 | | | | | | | % 146.35/19.45 | | | | | | | REDUCE: (184), (197), (198) imply: % 146.35/19.45 | | | | | | | (200) greater(zero, zero) % 146.35/19.45 | | | | | | | % 146.35/19.45 | | | | | | | BETA: splitting (192) gives: % 146.35/19.45 | | | | | | | % 146.35/19.45 | | | | | | | Case 1: % 146.35/19.45 | | | | | | | | % 146.35/19.45 | | | | | | | | (201) growth_rate(efficient_producers, all_32_0) = all_41_1 & % 146.35/19.45 | | | | | | | | $i(all_41_1) & ~ greater_or_equal(all_41_1, zero) % 146.35/19.45 | | | | | | | | % 146.35/19.45 | | | | | | | | ALPHA: (201) implies: % 146.35/19.45 | | | | | | | | (202) ~ greater_or_equal(all_41_1, zero) % 146.35/19.45 | | | | | | | | (203) growth_rate(efficient_producers, all_32_0) = all_41_1 % 146.35/19.45 | | | | | | | | % 146.35/19.45 | | | | | | | | REF_CLOSE: (11), (196), (199), (202), (203) are inconsistent by % 146.35/19.45 | | | | | | | | sub-proof #7. % 146.35/19.45 | | | | | | | | % 146.35/19.45 | | | | | | | Case 2: % 146.35/19.45 | | | | | | | | % 146.35/19.45 | | | | | | | | (204) growth_rate(first_movers, all_32_0) = all_41_0 & % 146.35/19.45 | | | | | | | | $i(all_41_0) & ~ greater(zero, all_41_0) % 146.35/19.45 | | | | | | | | % 146.35/19.45 | | | | | | | | ALPHA: (204) implies: % 146.35/19.45 | | | | | | | | (205) ~ greater(zero, all_41_0) % 146.35/19.45 | | | | | | | | (206) growth_rate(first_movers, all_32_0) = all_41_0 % 146.35/19.46 | | | | | | | | % 146.35/19.46 | | | | | | | | REF_CLOSE: (11), (195), (200), (205), (206) are inconsistent by % 146.35/19.46 | | | | | | | | sub-proof #6. % 146.35/19.46 | | | | | | | | % 146.35/19.46 | | | | | | | End of split % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | Case 2: % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | (207) equilibrium(all_12_0) = all_44_2 & $i(all_44_2) & ~ % 146.35/19.46 | | | | | | | greater_or_equal(all_32_0, all_44_2) % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | ALPHA: (207) implies: % 146.35/19.46 | | | | | | | (208) ~ greater_or_equal(all_32_0, all_44_2) % 146.35/19.46 | | | | | | | (209) equilibrium(all_12_0) = all_44_2 % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | REF_CLOSE: (10), (24), (162), (208), (209) are inconsistent by % 146.35/19.46 | | | | | | | sub-proof #4. % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | End of split % 146.35/19.46 | | | | | | % 146.35/19.46 | | | | | Case 2: % 146.35/19.46 | | | | | | % 146.35/19.46 | | | | | | (210) (growth_rate(efficient_producers, all_32_0) = all_44_0 & % 146.35/19.46 | | | | | | growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.46 | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_0, zero) & % 146.35/19.46 | | | | | | greater(zero, all_44_1)) | % 146.35/19.46 | | | | | | (growth_rate(efficient_producers, all_32_0) = all_44_0 & % 146.35/19.46 | | | | | | growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.46 | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_1, zero) & % 146.35/19.46 | | | | | | greater(zero, all_44_0)) % 146.35/19.46 | | | | | | % 146.35/19.46 | | | | | | BETA: splitting (210) gives: % 146.35/19.46 | | | | | | % 146.35/19.46 | | | | | | Case 1: % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | (211) growth_rate(efficient_producers, all_32_0) = all_44_0 & % 146.35/19.46 | | | | | | | growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.46 | | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_0, zero) & % 146.35/19.46 | | | | | | | greater(zero, all_44_1) % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | ALPHA: (211) implies: % 146.35/19.46 | | | | | | | (212) greater(zero, all_44_1) % 146.35/19.46 | | | | | | | (213) greater(all_44_0, zero) % 146.35/19.46 | | | | | | | (214) growth_rate(first_movers, all_32_0) = all_44_1 % 146.35/19.46 | | | | | | | (215) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | GROUND_INST: instantiating (11) with all_83_0, all_44_1, all_32_0, % 146.35/19.46 | | | | | | | first_movers, simplifying with (187), (214) gives: % 146.35/19.46 | | | | | | | (216) all_83_0 = all_44_1 % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | GROUND_INST: instantiating (11) with all_83_1, all_44_0, all_32_0, % 146.35/19.46 | | | | | | | efficient_producers, simplifying with (188), (215) % 146.35/19.46 | | | | | | | gives: % 146.35/19.46 | | | | | | | (217) all_83_1 = all_44_0 % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | REDUCE: (185), (217) imply: % 146.35/19.46 | | | | | | | (218) $i(all_44_0) % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | GROUND_INST: instantiating (1) with all_44_0, zero, simplifying % 146.35/19.46 | | | | | | | with (4), (213), (218) gives: % 146.35/19.46 | | | | | | | (219) greater_or_equal(all_44_0, zero) % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | REF_CLOSE: (11), (192), (212), (214), (215), (219) are % 146.35/19.46 | | | | | | | inconsistent by sub-proof #3. % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | Case 2: % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | (220) growth_rate(efficient_producers, all_32_0) = all_44_0 & % 146.35/19.46 | | | | | | | growth_rate(first_movers, all_32_0) = all_44_1 & % 146.35/19.46 | | | | | | | $i(all_44_0) & $i(all_44_1) & greater(all_44_1, zero) & % 146.35/19.46 | | | | | | | greater(zero, all_44_0) % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | ALPHA: (220) implies: % 146.35/19.46 | | | | | | | (221) greater(zero, all_44_0) % 146.35/19.46 | | | | | | | (222) greater(all_44_1, zero) % 146.35/19.46 | | | | | | | (223) growth_rate(first_movers, all_32_0) = all_44_1 % 146.35/19.46 | | | | | | | (224) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | GROUND_INST: instantiating (11) with all_83_0, all_44_1, all_32_0, % 146.35/19.46 | | | | | | | first_movers, simplifying with (187), (223) gives: % 146.35/19.46 | | | | | | | (225) all_83_0 = all_44_1 % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | GROUND_INST: instantiating (11) with all_83_1, all_44_0, all_32_0, % 146.35/19.46 | | | | | | | efficient_producers, simplifying with (188), (224) % 146.35/19.46 | | | | | | | gives: % 146.35/19.46 | | | | | | | (226) all_83_1 = all_44_0 % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | REDUCE: (186), (225) imply: % 146.35/19.46 | | | | | | | (227) $i(all_44_1) % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | REDUCE: (185), (226) imply: % 146.35/19.46 | | | | | | | (228) $i(all_44_0) % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | REDUCE: (184), (225), (226) imply: % 146.35/19.46 | | | | | | | (229) greater(all_44_0, all_44_1) % 146.35/19.46 | | | | | | | % 146.35/19.46 | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with % 146.35/19.46 | | | | | | | all_44_1, zero, all_44_1, simplifying with (4), % 146.35/19.46 | | | | | | | (222), (227) gives: % 146.35/19.47 | | | | | | | (230) ~ greater(zero, all_44_1) | greater(all_44_1, all_44_1) % 146.35/19.47 | | | | | | | % 146.35/19.47 | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with % 146.35/19.47 | | | | | | | all_44_0, all_44_1, zero, simplifying with (4), % 146.35/19.47 | | | | | | | (222), (227), (228), (229) gives: % 146.35/19.47 | | | | | | | (231) greater(all_44_0, zero) % 146.35/19.47 | | | | | | | % 146.35/19.47 | | | | | | | GROUND_INST: instantiating (mp_greater_transitivity) with zero, % 146.35/19.47 | | | | | | | all_44_0, all_44_1, simplifying with (4), (221), % 146.35/19.47 | | | | | | | (227), (228), (229) gives: % 146.35/19.47 | | | | | | | (232) greater(zero, all_44_1) % 146.35/19.47 | | | | | | | % 146.35/19.47 | | | | | | | REF_CLOSE: (1), (4), (11), (192), (223), (224), (228), (230), % 146.35/19.47 | | | | | | | (231), (232) are inconsistent by sub-proof #2. % 146.35/19.47 | | | | | | | % 146.35/19.47 | | | | | | End of split % 146.35/19.47 | | | | | | % 146.35/19.47 | | | | | End of split % 146.35/19.47 | | | | | % 146.35/19.47 | | | | End of split % 146.35/19.47 | | | | % 146.35/19.47 | | | End of split % 146.35/19.47 | | | % 146.35/19.47 | | End of split % 146.35/19.47 | | % 146.35/19.47 | End of split % 146.35/19.47 | % 146.35/19.47 End of proof % 146.35/19.47 % 146.35/19.47 Sub-proof #1 shows that the following formulas are inconsistent: % 146.35/19.47 ---------------------------------------------------------------- % 146.35/19.47 (1) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.47 (2) $i(all_83_0) % 146.35/19.47 (3) (growth_rate(efficient_producers, all_32_0) = all_41_1 & $i(all_41_1) & % 146.35/19.47 ~ greater_or_equal(all_41_1, zero)) | (growth_rate(first_movers, % 146.35/19.47 all_32_0) = all_41_0 & $i(all_41_0) & ~ greater(zero, all_41_0)) % 146.35/19.47 (4) $i(zero) % 146.35/19.47 (5) all_83_0 = all_44_1 % 146.35/19.47 (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 146.35/19.47 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 146.35/19.47 (7) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 146.35/19.47 greater_or_equal(v0, v1)) % 146.35/19.47 (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.35/19.47 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.35/19.47 (9) all_83_1 = all_44_0 % 146.35/19.47 (10) growth_rate(first_movers, all_32_0) = all_44_1 % 146.35/19.47 (11) $i(all_83_1) % 146.35/19.47 (12) greater(zero, all_44_0) % 146.35/19.47 (13) greater(all_83_1, all_83_0) % 146.35/19.47 (14) greater(all_44_1, zero) % 146.35/19.47 % 146.35/19.47 Begin of proof % 146.35/19.47 | % 146.35/19.47 | REDUCE: (2), (5) imply: % 146.35/19.47 | (15) $i(all_44_1) % 146.35/19.47 | % 146.35/19.47 | REDUCE: (9), (11) imply: % 146.35/19.47 | (16) $i(all_44_0) % 146.35/19.47 | % 146.35/19.47 | REDUCE: (5), (9), (13) imply: % 146.35/19.47 | (17) greater(all_44_0, all_44_1) % 146.35/19.47 | % 146.35/19.47 | GROUND_INST: instantiating (6) with all_44_1, zero, all_44_1, simplifying with % 146.35/19.47 | (4), (14), (15) gives: % 146.35/19.47 | (18) ~ greater(zero, all_44_1) | greater(all_44_1, all_44_1) % 146.35/19.47 | % 146.35/19.47 | GROUND_INST: instantiating (6) with all_44_0, all_44_1, zero, simplifying with % 146.35/19.47 | (4), (14), (15), (16), (17) gives: % 146.35/19.47 | (19) greater(all_44_0, zero) % 146.35/19.47 | % 146.35/19.47 | GROUND_INST: instantiating (6) with zero, all_44_0, all_44_1, simplifying with % 146.35/19.47 | (4), (12), (15), (16), (17) gives: % 146.35/19.47 | (20) greater(zero, all_44_1) % 146.35/19.47 | % 146.35/19.47 | REF_CLOSE: (1), (3), (4), (7), (8), (10), (16), (18), (19), (20) are % 146.35/19.47 | inconsistent by sub-proof #2. % 146.35/19.47 | % 146.35/19.47 End of proof % 146.35/19.47 % 146.35/19.47 Sub-proof #2 shows that the following formulas are inconsistent: % 146.35/19.47 ---------------------------------------------------------------- % 146.35/19.47 (1) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.48 (2) (growth_rate(efficient_producers, all_32_0) = all_41_1 & $i(all_41_1) & % 146.35/19.48 ~ greater_or_equal(all_41_1, zero)) | (growth_rate(first_movers, % 146.35/19.48 all_32_0) = all_41_0 & $i(all_41_0) & ~ greater(zero, all_41_0)) % 146.35/19.48 (3) $i(zero) % 146.35/19.48 (4) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 146.35/19.48 greater_or_equal(v0, v1)) % 146.35/19.48 (5) $i(all_44_0) % 146.35/19.48 (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.35/19.48 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.35/19.48 (7) growth_rate(first_movers, all_32_0) = all_44_1 % 146.35/19.48 (8) greater(zero, all_44_1) % 146.35/19.48 (9) ~ greater(zero, all_44_1) | greater(all_44_1, all_44_1) % 146.35/19.48 (10) greater(all_44_0, zero) % 146.35/19.48 % 146.35/19.48 Begin of proof % 146.35/19.48 | % 146.35/19.48 | BETA: splitting (9) gives: % 146.35/19.48 | % 146.35/19.48 | Case 1: % 146.35/19.48 | | % 146.35/19.48 | | (11) ~ greater(zero, all_44_1) % 146.35/19.48 | | % 146.35/19.48 | | PRED_UNIFY: (8), (11) imply: % 146.35/19.48 | | (12) $false % 146.35/19.48 | | % 146.35/19.48 | | CLOSE: (12) is inconsistent. % 146.35/19.48 | | % 146.35/19.48 | Case 2: % 146.35/19.48 | | % 146.35/19.48 | | % 146.35/19.48 | | GROUND_INST: instantiating (4) with all_44_0, zero, simplifying with (3), % 146.35/19.48 | | (5), (10) gives: % 146.35/19.48 | | (13) greater_or_equal(all_44_0, zero) % 146.35/19.48 | | % 146.35/19.48 | | REF_CLOSE: (1), (2), (6), (7), (8), (13) are inconsistent by sub-proof #3. % 146.35/19.48 | | % 146.35/19.48 | End of split % 146.35/19.48 | % 146.35/19.48 End of proof % 146.35/19.48 % 146.35/19.48 Sub-proof #3 shows that the following formulas are inconsistent: % 146.35/19.48 ---------------------------------------------------------------- % 146.35/19.48 (1) growth_rate(efficient_producers, all_32_0) = all_44_0 % 146.35/19.48 (2) (growth_rate(efficient_producers, all_32_0) = all_41_1 & $i(all_41_1) & % 146.35/19.48 ~ greater_or_equal(all_41_1, zero)) | (growth_rate(first_movers, % 146.35/19.48 all_32_0) = all_41_0 & $i(all_41_0) & ~ greater(zero, all_41_0)) % 146.35/19.48 (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.35/19.48 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.35/19.48 (4) growth_rate(first_movers, all_32_0) = all_44_1 % 146.35/19.48 (5) greater(zero, all_44_1) % 146.35/19.48 (6) greater_or_equal(all_44_0, zero) % 146.35/19.48 % 146.35/19.48 Begin of proof % 146.35/19.48 | % 146.35/19.48 | BETA: splitting (2) gives: % 146.35/19.48 | % 146.35/19.48 | Case 1: % 146.35/19.48 | | % 146.35/19.48 | | (7) growth_rate(efficient_producers, all_32_0) = all_41_1 & $i(all_41_1) % 146.35/19.48 | | & ~ greater_or_equal(all_41_1, zero) % 146.35/19.48 | | % 146.35/19.48 | | ALPHA: (7) implies: % 146.35/19.48 | | (8) ~ greater_or_equal(all_41_1, zero) % 146.35/19.48 | | (9) growth_rate(efficient_producers, all_32_0) = all_41_1 % 146.35/19.48 | | % 146.35/19.48 | | GROUND_INST: instantiating (3) with all_44_0, all_41_1, all_32_0, % 146.35/19.48 | | efficient_producers, simplifying with (1), (9) gives: % 146.35/19.48 | | (10) all_44_0 = all_41_1 % 146.35/19.48 | | % 146.35/19.48 | | PRED_UNIFY: (6), (8) imply: % 146.35/19.48 | | (11) ~ (all_44_0 = all_41_1) % 146.35/19.48 | | % 146.35/19.48 | | REDUCE: (10), (11) imply: % 146.35/19.48 | | (12) $false % 146.35/19.48 | | % 146.35/19.48 | | CLOSE: (12) is inconsistent. % 146.35/19.48 | | % 146.35/19.48 | Case 2: % 146.35/19.48 | | % 146.35/19.48 | | (13) growth_rate(first_movers, all_32_0) = all_41_0 & $i(all_41_0) & ~ % 146.35/19.48 | | greater(zero, all_41_0) % 146.35/19.48 | | % 146.35/19.48 | | ALPHA: (13) implies: % 146.35/19.48 | | (14) ~ greater(zero, all_41_0) % 146.35/19.48 | | (15) growth_rate(first_movers, all_32_0) = all_41_0 % 146.35/19.48 | | % 146.35/19.48 | | GROUND_INST: instantiating (3) with all_44_1, all_41_0, all_32_0, % 146.35/19.48 | | first_movers, simplifying with (4), (15) gives: % 146.35/19.48 | | (16) all_44_1 = all_41_0 % 146.35/19.48 | | % 146.35/19.48 | | PRED_UNIFY: (5), (14) imply: % 146.35/19.48 | | (17) ~ (all_44_1 = all_41_0) % 146.35/19.48 | | % 146.35/19.48 | | REDUCE: (16), (17) imply: % 146.35/19.48 | | (18) $false % 146.35/19.48 | | % 146.35/19.48 | | CLOSE: (18) is inconsistent. % 146.35/19.48 | | % 146.35/19.48 | End of split % 146.35/19.48 | % 146.35/19.48 End of proof % 146.35/19.48 % 146.35/19.48 Sub-proof #4 shows that the following formulas are inconsistent: % 146.35/19.48 ---------------------------------------------------------------- % 146.35/19.48 (1) equilibrium(all_12_0) = all_44_2 % 146.35/19.48 (2) ~ greater_or_equal(all_32_0, all_44_2) % 146.35/19.49 (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 146.35/19.49 = v1) | ~ (equilibrium(v2) = v0)) % 146.35/19.49 (4) equilibrium(all_12_0) = all_20_1 % 146.35/19.49 (5) greater_or_equal(all_32_0, all_20_1) % 146.35/19.49 % 146.35/19.49 Begin of proof % 146.35/19.49 | % 146.35/19.49 | GROUND_INST: instantiating (3) with all_20_1, all_44_2, all_12_0, simplifying % 146.35/19.49 | with (1), (4) gives: % 146.35/19.49 | (6) all_44_2 = all_20_1 % 146.35/19.49 | % 146.35/19.49 | PRED_UNIFY: (2), (5) imply: % 146.35/19.49 | (7) ~ (all_44_2 = all_20_1) % 146.35/19.49 | % 146.35/19.49 | REDUCE: (6), (7) imply: % 146.35/19.49 | (8) $false % 146.35/19.49 | % 146.35/19.49 | CLOSE: (8) is inconsistent. % 146.35/19.49 | % 146.35/19.49 End of proof % 146.35/19.49 % 146.35/19.49 Sub-proof #5 shows that the following formulas are inconsistent: % 146.35/19.49 ---------------------------------------------------------------- % 146.35/19.49 (1) growth_rate(first_movers, all_32_0) = zero % 146.35/19.49 (2) growth_rate(efficient_producers, all_32_0) = all_83_1 % 146.35/19.49 (3) (growth_rate(efficient_producers, all_32_0) = all_41_1 & $i(all_41_1) & % 146.35/19.49 ~ greater_or_equal(all_41_1, zero)) | (growth_rate(first_movers, % 146.35/19.49 all_32_0) = all_41_0 & $i(all_41_0) & ~ greater(zero, all_41_0)) % 146.35/19.49 (4) growth_rate(efficient_producers, all_32_0) = zero % 146.35/19.49 (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.35/19.49 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.35/19.49 (6) greater_or_equal(all_83_1, all_83_0) % 146.35/19.49 (7) growth_rate(first_movers, all_32_0) = all_83_0 % 146.35/19.49 (8) greater(all_83_1, all_83_0) % 146.35/19.49 % 146.35/19.49 Begin of proof % 146.35/19.49 | % 146.35/19.49 | GROUND_INST: instantiating (5) with all_83_0, zero, all_32_0, first_movers, % 146.35/19.49 | simplifying with (1), (7) gives: % 146.35/19.49 | (9) all_83_0 = zero % 146.35/19.49 | % 146.35/19.49 | GROUND_INST: instantiating (5) with all_83_1, zero, all_32_0, % 146.35/19.49 | efficient_producers, simplifying with (2), (4) gives: % 146.35/19.49 | (10) all_83_1 = zero % 146.35/19.49 | % 146.35/19.49 | REDUCE: (6), (9), (10) imply: % 146.35/19.49 | (11) greater_or_equal(zero, zero) % 146.35/19.49 | % 146.35/19.49 | REDUCE: (8), (9), (10) imply: % 146.35/19.49 | (12) greater(zero, zero) % 146.35/19.49 | % 146.35/19.49 | BETA: splitting (3) gives: % 146.35/19.49 | % 146.35/19.49 | Case 1: % 146.35/19.49 | | % 146.35/19.49 | | (13) growth_rate(efficient_producers, all_32_0) = all_41_1 & $i(all_41_1) % 146.35/19.49 | | & ~ greater_or_equal(all_41_1, zero) % 146.35/19.49 | | % 146.35/19.49 | | ALPHA: (13) implies: % 146.35/19.49 | | (14) ~ greater_or_equal(all_41_1, zero) % 146.35/19.49 | | (15) growth_rate(efficient_producers, all_32_0) = all_41_1 % 146.35/19.49 | | % 146.35/19.49 | | REF_CLOSE: (4), (5), (11), (14), (15) are inconsistent by sub-proof #7. % 146.35/19.49 | | % 146.35/19.49 | Case 2: % 146.35/19.49 | | % 146.35/19.49 | | (16) growth_rate(first_movers, all_32_0) = all_41_0 & $i(all_41_0) & ~ % 146.35/19.49 | | greater(zero, all_41_0) % 146.35/19.49 | | % 146.35/19.49 | | ALPHA: (16) implies: % 146.35/19.49 | | (17) ~ greater(zero, all_41_0) % 146.35/19.49 | | (18) growth_rate(first_movers, all_32_0) = all_41_0 % 146.35/19.49 | | % 146.35/19.49 | | REF_CLOSE: (1), (5), (12), (17), (18) are inconsistent by sub-proof #6. % 146.35/19.49 | | % 146.35/19.49 | End of split % 146.35/19.49 | % 146.35/19.49 End of proof % 146.35/19.49 % 146.35/19.49 Sub-proof #6 shows that the following formulas are inconsistent: % 146.35/19.49 ---------------------------------------------------------------- % 146.35/19.49 (1) growth_rate(first_movers, all_32_0) = zero % 146.35/19.49 (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.35/19.49 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.35/19.49 (3) ~ greater(zero, all_41_0) % 146.35/19.49 (4) greater(zero, zero) % 146.35/19.49 (5) growth_rate(first_movers, all_32_0) = all_41_0 % 146.35/19.49 % 146.35/19.49 Begin of proof % 146.35/19.49 | % 146.35/19.49 | GROUND_INST: instantiating (2) with zero, all_41_0, all_32_0, first_movers, % 146.35/19.49 | simplifying with (1), (5) gives: % 146.35/19.49 | (6) all_41_0 = zero % 146.35/19.49 | % 146.35/19.49 | PRED_UNIFY: (3), (4) imply: % 146.35/19.49 | (7) ~ (all_41_0 = zero) % 146.35/19.49 | % 146.35/19.49 | REDUCE: (6), (7) imply: % 146.35/19.49 | (8) $false % 146.35/19.49 | % 146.35/19.49 | CLOSE: (8) is inconsistent. % 146.35/19.49 | % 146.35/19.49 End of proof % 146.35/19.49 % 146.35/19.49 Sub-proof #7 shows that the following formulas are inconsistent: % 146.35/19.49 ---------------------------------------------------------------- % 146.35/19.49 (1) growth_rate(efficient_producers, all_32_0) = zero % 146.35/19.49 (2) greater_or_equal(zero, zero) % 146.35/19.49 (3) ~ greater_or_equal(all_41_1, zero) % 146.35/19.49 (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.35/19.49 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.35/19.50 (5) growth_rate(efficient_producers, all_32_0) = all_41_1 % 146.35/19.50 % 146.35/19.50 Begin of proof % 146.35/19.50 | % 146.35/19.50 | GROUND_INST: instantiating (4) with zero, all_41_1, all_32_0, % 146.35/19.50 | efficient_producers, simplifying with (1), (5) gives: % 146.35/19.50 | (6) all_41_1 = zero % 146.35/19.50 | % 146.35/19.50 | PRED_UNIFY: (2), (3) imply: % 146.35/19.50 | (7) ~ (all_41_1 = zero) % 146.35/19.50 | % 146.35/19.50 | REDUCE: (6), (7) imply: % 146.35/19.50 | (8) $false % 146.35/19.50 | % 146.35/19.50 | CLOSE: (8) is inconsistent. % 146.35/19.50 | % 146.35/19.50 End of proof % 146.35/19.50 % 146.35/19.50 Sub-proof #8 shows that the following formulas are inconsistent: % 146.35/19.50 ---------------------------------------------------------------- % 146.35/19.50 (1) $i(all_20_1) % 146.35/19.50 (2) all_39_0 = all_39_1 | ~ (growth_rate(first_movers, all_30_0) = all_39_1) % 146.35/19.50 (3) $i(zero) % 146.84/19.50 (4) greater(all_39_1, all_39_0) % 146.84/19.50 (5) growth_rate(efficient_producers, all_30_0) = all_39_1 % 146.84/19.50 (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 146.84/19.50 = v1) | ~ (equilibrium(v2) = v0)) % 146.84/19.50 (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 146.84/19.50 $i(v0) | ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 146.84/19.50 (8) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 146.84/19.50 greater_or_equal(v0, v1)) % 146.84/19.50 (9) $i(all_22_0) % 146.84/19.50 (10) growth_rate(first_movers, all_30_0) = all_39_0 % 146.84/19.50 (11) $i(all_30_0) % 146.84/19.50 (12) outcompetes(efficient_producers, first_movers, all_30_0) | % 146.84/19.50 (growth_rate(efficient_producers, all_30_0) = all_42_1 & $i(all_42_1) & % 146.84/19.50 ~ greater_or_equal(all_42_1, zero)) | (growth_rate(first_movers, % 146.84/19.50 all_30_0) = all_42_0 & $i(all_42_0) & ~ greater(zero, all_42_0)) % 146.84/19.50 (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.84/19.50 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.84/19.50 (14) all_30_0 = all_22_0 | greater(all_30_0, all_22_0) % 146.84/19.50 (15) greater_or_equal(all_39_1, all_39_0) % 146.84/19.50 (16) ~ outcompetes(efficient_producers, first_movers, all_30_0) % 146.84/19.50 (17) equilibrium(all_12_0) = all_20_1 % 146.84/19.50 (18) (all_43_0 = zero & all_43_1 = zero & growth_rate(efficient_producers, % 146.84/19.50 all_30_0) = zero & growth_rate(first_movers, all_30_0) = zero) | % 146.84/19.50 (equilibrium(all_12_0) = all_43_2 & $i(all_43_2) & ~ % 146.84/19.50 greater_or_equal(all_30_0, all_43_2)) | % 146.84/19.50 (growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.50 growth_rate(first_movers, all_30_0) = all_43_1 & $i(all_43_0) & % 146.84/19.50 $i(all_43_1) & greater(all_43_0, zero) & greater(zero, all_43_1)) | % 146.84/19.50 (growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.50 growth_rate(first_movers, all_30_0) = all_43_1 & $i(all_43_0) & % 146.84/19.50 $i(all_43_1) & greater(all_43_1, zero) & greater(zero, all_43_0)) % 146.84/19.50 (19) greater(all_22_0, all_20_1) % 146.84/19.50 % 146.84/19.50 Begin of proof % 146.84/19.50 | % 146.84/19.50 | GROUND_INST: instantiating (8) with all_22_0, all_20_1, simplifying with (1), % 146.84/19.50 | (9), (19) gives: % 146.84/19.50 | (20) greater_or_equal(all_22_0, all_20_1) % 146.84/19.50 | % 146.84/19.50 | BETA: splitting (14) gives: % 146.84/19.50 | % 146.84/19.50 | Case 1: % 146.84/19.50 | | % 146.84/19.50 | | (21) greater(all_30_0, all_22_0) % 146.84/19.50 | | % 146.84/19.50 | | GROUND_INST: instantiating (7) with all_30_0, all_22_0, all_20_1, % 146.84/19.50 | | simplifying with (1), (9), (11), (19), (21) gives: % 146.84/19.50 | | (22) greater(all_30_0, all_20_1) % 146.84/19.50 | | % 146.84/19.50 | | GROUND_INST: instantiating (8) with all_30_0, all_20_1, simplifying with % 146.84/19.50 | | (1), (11), (22) gives: % 146.84/19.50 | | (23) greater_or_equal(all_30_0, all_20_1) % 146.84/19.50 | | % 146.84/19.50 | | BETA: splitting (12) gives: % 146.84/19.50 | | % 146.84/19.50 | | Case 1: % 146.84/19.50 | | | % 146.84/19.50 | | | (24) outcompetes(efficient_producers, first_movers, all_30_0) % 146.84/19.50 | | | % 146.84/19.50 | | | PRED_UNIFY: (16), (24) imply: % 146.84/19.50 | | | (25) $false % 146.84/19.50 | | | % 146.84/19.50 | | | CLOSE: (25) is inconsistent. % 146.84/19.50 | | | % 146.84/19.50 | | Case 2: % 146.84/19.50 | | | % 146.84/19.50 | | | (26) (growth_rate(efficient_producers, all_30_0) = all_42_1 & % 146.84/19.50 | | | $i(all_42_1) & ~ greater_or_equal(all_42_1, zero)) | % 146.84/19.50 | | | (growth_rate(first_movers, all_30_0) = all_42_0 & $i(all_42_0) & % 146.84/19.50 | | | ~ greater(zero, all_42_0)) % 146.84/19.50 | | | % 146.84/19.50 | | | BETA: splitting (2) gives: % 146.84/19.50 | | | % 146.84/19.50 | | | Case 1: % 146.84/19.50 | | | | % 146.84/19.50 | | | | (27) ~ (growth_rate(first_movers, all_30_0) = all_39_1) % 146.84/19.50 | | | | % 146.84/19.50 | | | | BETA: splitting (18) gives: % 146.84/19.50 | | | | % 146.84/19.50 | | | | Case 1: % 146.84/19.50 | | | | | % 146.84/19.51 | | | | | (28) (all_43_0 = zero & all_43_1 = zero & % 146.84/19.51 | | | | | growth_rate(efficient_producers, all_30_0) = zero & % 146.84/19.51 | | | | | growth_rate(first_movers, all_30_0) = zero) | % 146.84/19.51 | | | | | (equilibrium(all_12_0) = all_43_2 & $i(all_43_2) & ~ % 146.84/19.51 | | | | | greater_or_equal(all_30_0, all_43_2)) % 146.84/19.51 | | | | | % 146.84/19.51 | | | | | BETA: splitting (28) gives: % 146.84/19.51 | | | | | % 146.84/19.51 | | | | | Case 1: % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | (29) all_43_0 = zero & all_43_1 = zero & % 146.84/19.51 | | | | | | growth_rate(efficient_producers, all_30_0) = zero & % 146.84/19.51 | | | | | | growth_rate(first_movers, all_30_0) = zero % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | ALPHA: (29) implies: % 146.84/19.51 | | | | | | (30) growth_rate(first_movers, all_30_0) = zero % 146.84/19.51 | | | | | | (31) growth_rate(efficient_producers, all_30_0) = zero % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | PRED_UNIFY: (27), (30) imply: % 146.84/19.51 | | | | | | (32) ~ (all_39_1 = zero) % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | GROUND_INST: instantiating (13) with all_39_1, zero, all_30_0, % 146.84/19.51 | | | | | | efficient_producers, simplifying with (5), (31) gives: % 146.84/19.51 | | | | | | (33) all_39_1 = zero % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | REDUCE: (32), (33) imply: % 146.84/19.51 | | | | | | (34) $false % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | CLOSE: (34) is inconsistent. % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | Case 2: % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | (35) equilibrium(all_12_0) = all_43_2 & $i(all_43_2) & ~ % 146.84/19.51 | | | | | | greater_or_equal(all_30_0, all_43_2) % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | ALPHA: (35) implies: % 146.84/19.51 | | | | | | (36) ~ greater_or_equal(all_30_0, all_43_2) % 146.84/19.51 | | | | | | (37) equilibrium(all_12_0) = all_43_2 % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | REF_CLOSE: (6), (17), (23), (36), (37) are inconsistent by sub-proof % 146.84/19.51 | | | | | | #18. % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | End of split % 146.84/19.51 | | | | | % 146.84/19.51 | | | | Case 2: % 146.84/19.51 | | | | | % 146.84/19.51 | | | | | (38) (growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.51 | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.51 | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_0, zero) & % 146.84/19.51 | | | | | greater(zero, all_43_1)) | (growth_rate(efficient_producers, % 146.84/19.51 | | | | | all_30_0) = all_43_0 & growth_rate(first_movers, all_30_0) % 146.84/19.51 | | | | | = all_43_1 & $i(all_43_0) & $i(all_43_1) & greater(all_43_1, % 146.84/19.51 | | | | | zero) & greater(zero, all_43_0)) % 146.84/19.51 | | | | | % 146.84/19.51 | | | | | BETA: splitting (38) gives: % 146.84/19.51 | | | | | % 146.84/19.51 | | | | | Case 1: % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | (39) growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.51 | | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.51 | | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_0, zero) & % 146.84/19.51 | | | | | | greater(zero, all_43_1) % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | ALPHA: (39) implies: % 146.84/19.51 | | | | | | (40) greater(zero, all_43_1) % 146.84/19.51 | | | | | | (41) greater(all_43_0, zero) % 146.84/19.51 | | | | | | (42) growth_rate(first_movers, all_30_0) = all_43_1 % 146.84/19.51 | | | | | | (43) growth_rate(efficient_producers, all_30_0) = all_43_0 % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | GROUND_INST: instantiating (13) with all_39_0, all_43_1, all_30_0, % 146.84/19.51 | | | | | | first_movers, simplifying with (10), (42) gives: % 146.84/19.51 | | | | | | (44) all_43_1 = all_39_0 % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | GROUND_INST: instantiating (13) with all_39_1, all_43_0, all_30_0, % 146.84/19.51 | | | | | | efficient_producers, simplifying with (5), (43) gives: % 146.84/19.51 | | | | | | (45) all_43_0 = all_39_1 % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | REDUCE: (41), (45) imply: % 146.84/19.51 | | | | | | (46) greater(all_39_1, zero) % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | REDUCE: (40), (44) imply: % 146.84/19.51 | | | | | | (47) greater(zero, all_39_0) % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | REF_CLOSE: (3), (5), (8), (10), (13), (26), (46), (47) are % 146.84/19.51 | | | | | | inconsistent by sub-proof #16. % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | Case 2: % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | (48) growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.51 | | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.51 | | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_1, zero) & % 146.84/19.51 | | | | | | greater(zero, all_43_0) % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | ALPHA: (48) implies: % 146.84/19.51 | | | | | | (49) greater(zero, all_43_0) % 146.84/19.51 | | | | | | (50) greater(all_43_1, zero) % 146.84/19.51 | | | | | | (51) $i(all_43_1) % 146.84/19.51 | | | | | | (52) $i(all_43_0) % 146.84/19.51 | | | | | | (53) growth_rate(first_movers, all_30_0) = all_43_1 % 146.84/19.51 | | | | | | (54) growth_rate(efficient_producers, all_30_0) = all_43_0 % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | GROUND_INST: instantiating (13) with all_39_0, all_43_1, all_30_0, % 146.84/19.51 | | | | | | first_movers, simplifying with (10), (53) gives: % 146.84/19.51 | | | | | | (55) all_43_1 = all_39_0 % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | GROUND_INST: instantiating (13) with all_39_1, all_43_0, all_30_0, % 146.84/19.51 | | | | | | efficient_producers, simplifying with (5), (54) gives: % 146.84/19.51 | | | | | | (56) all_43_0 = all_39_1 % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | REDUCE: (52), (56) imply: % 146.84/19.51 | | | | | | (57) $i(all_39_1) % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | REDUCE: (51), (55) imply: % 146.84/19.51 | | | | | | (58) $i(all_39_0) % 146.84/19.51 | | | | | | % 146.84/19.51 | | | | | | REDUCE: (50), (55) imply: % 146.84/19.52 | | | | | | (59) greater(all_39_0, zero) % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | REDUCE: (49), (56) imply: % 146.84/19.52 | | | | | | (60) greater(zero, all_39_1) % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | GROUND_INST: instantiating (7) with zero, all_39_1, all_39_0, % 146.84/19.52 | | | | | | simplifying with (3), (4), (57), (58), (60) gives: % 146.84/19.52 | | | | | | (61) greater(zero, all_39_0) % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | GROUND_INST: instantiating (7) with all_39_1, all_39_0, zero, % 146.84/19.52 | | | | | | simplifying with (3), (4), (57), (58), (59) gives: % 146.84/19.52 | | | | | | (62) greater(all_39_1, zero) % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | REF_CLOSE: (3), (5), (8), (10), (13), (26), (61), (62) are % 146.84/19.52 | | | | | | inconsistent by sub-proof #16. % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | End of split % 146.84/19.52 | | | | | % 146.84/19.52 | | | | End of split % 146.84/19.52 | | | | % 146.84/19.52 | | | Case 2: % 146.84/19.52 | | | | % 146.84/19.52 | | | | (63) all_39_0 = all_39_1 % 146.84/19.52 | | | | % 146.84/19.52 | | | | REDUCE: (10), (63) imply: % 146.84/19.52 | | | | (64) growth_rate(first_movers, all_30_0) = all_39_1 % 146.84/19.52 | | | | % 146.84/19.52 | | | | REDUCE: (15), (63) imply: % 146.84/19.52 | | | | (65) greater_or_equal(all_39_1, all_39_1) % 146.84/19.52 | | | | % 146.84/19.52 | | | | REDUCE: (4), (63) imply: % 146.84/19.52 | | | | (66) greater(all_39_1, all_39_1) % 146.84/19.52 | | | | % 146.84/19.52 | | | | BETA: splitting (18) gives: % 146.84/19.52 | | | | % 146.84/19.52 | | | | Case 1: % 146.84/19.52 | | | | | % 146.84/19.52 | | | | | (67) (all_43_0 = zero & all_43_1 = zero & % 146.84/19.52 | | | | | growth_rate(efficient_producers, all_30_0) = zero & % 146.84/19.52 | | | | | growth_rate(first_movers, all_30_0) = zero) | % 146.84/19.52 | | | | | (equilibrium(all_12_0) = all_43_2 & $i(all_43_2) & ~ % 146.84/19.52 | | | | | greater_or_equal(all_30_0, all_43_2)) % 146.84/19.52 | | | | | % 146.84/19.52 | | | | | BETA: splitting (67) gives: % 146.84/19.52 | | | | | % 146.84/19.52 | | | | | Case 1: % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | (68) all_43_0 = zero & all_43_1 = zero & % 146.84/19.52 | | | | | | growth_rate(efficient_producers, all_30_0) = zero & % 146.84/19.52 | | | | | | growth_rate(first_movers, all_30_0) = zero % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | REF_CLOSE: (5), (13), (26), (64), (65), (66), (68) are inconsistent % 146.84/19.52 | | | | | | by sub-proof #15. % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | Case 2: % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | (69) equilibrium(all_12_0) = all_43_2 & $i(all_43_2) & ~ % 146.84/19.52 | | | | | | greater_or_equal(all_30_0, all_43_2) % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | ALPHA: (69) implies: % 146.84/19.52 | | | | | | (70) ~ greater_or_equal(all_30_0, all_43_2) % 146.84/19.52 | | | | | | (71) equilibrium(all_12_0) = all_43_2 % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | REF_CLOSE: (6), (17), (23), (70), (71) are inconsistent by sub-proof % 146.84/19.52 | | | | | | #18. % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | End of split % 146.84/19.52 | | | | | % 146.84/19.52 | | | | Case 2: % 146.84/19.52 | | | | | % 146.84/19.52 | | | | | (72) (growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.52 | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.52 | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_0, zero) & % 146.84/19.52 | | | | | greater(zero, all_43_1)) | (growth_rate(efficient_producers, % 146.84/19.52 | | | | | all_30_0) = all_43_0 & growth_rate(first_movers, all_30_0) % 146.84/19.52 | | | | | = all_43_1 & $i(all_43_0) & $i(all_43_1) & greater(all_43_1, % 146.84/19.52 | | | | | zero) & greater(zero, all_43_0)) % 146.84/19.52 | | | | | % 146.84/19.52 | | | | | BETA: splitting (72) gives: % 146.84/19.52 | | | | | % 146.84/19.52 | | | | | Case 1: % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | (73) growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.52 | | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.52 | | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_0, zero) & % 146.84/19.52 | | | | | | greater(zero, all_43_1) % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | ALPHA: (73) implies: % 146.84/19.52 | | | | | | (74) greater(zero, all_43_1) % 146.84/19.52 | | | | | | (75) greater(all_43_0, zero) % 146.84/19.52 | | | | | | (76) growth_rate(first_movers, all_30_0) = all_43_1 % 146.84/19.52 | | | | | | (77) growth_rate(efficient_producers, all_30_0) = all_43_0 % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | GROUND_INST: instantiating (13) with all_39_1, all_43_1, all_30_0, % 146.84/19.52 | | | | | | first_movers, simplifying with (64), (76) gives: % 146.84/19.52 | | | | | | (78) all_43_1 = all_39_1 % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | GROUND_INST: instantiating (13) with all_39_1, all_43_0, all_30_0, % 146.84/19.52 | | | | | | efficient_producers, simplifying with (5), (77) gives: % 146.84/19.52 | | | | | | (79) all_43_0 = all_39_1 % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | REDUCE: (75), (79) imply: % 146.84/19.52 | | | | | | (80) greater(all_39_1, zero) % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | REDUCE: (74), (78) imply: % 146.84/19.52 | | | | | | (81) greater(zero, all_39_1) % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | BETA: splitting (26) gives: % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | Case 1: % 146.84/19.52 | | | | | | | % 146.84/19.52 | | | | | | | (82) growth_rate(efficient_producers, all_30_0) = all_42_1 & % 146.84/19.52 | | | | | | | $i(all_42_1) & ~ greater_or_equal(all_42_1, zero) % 146.84/19.52 | | | | | | | % 146.84/19.52 | | | | | | | REF_CLOSE: (3), (5), (8), (13), (80), (82) are inconsistent by % 146.84/19.52 | | | | | | | sub-proof #17. % 146.84/19.52 | | | | | | | % 146.84/19.52 | | | | | | Case 2: % 146.84/19.52 | | | | | | | % 146.84/19.52 | | | | | | | (83) growth_rate(first_movers, all_30_0) = all_42_0 & % 146.84/19.52 | | | | | | | $i(all_42_0) & ~ greater(zero, all_42_0) % 146.84/19.52 | | | | | | | % 146.84/19.52 | | | | | | | REF_CLOSE: (13), (64), (81), (83) are inconsistent by sub-proof % 146.84/19.52 | | | | | | | #14. % 146.84/19.52 | | | | | | | % 146.84/19.52 | | | | | | End of split % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | Case 2: % 146.84/19.52 | | | | | | % 146.84/19.52 | | | | | | (84) growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.52 | | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.52 | | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_1, zero) & % 146.84/19.52 | | | | | | greater(zero, all_43_0) % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | ALPHA: (84) implies: % 146.84/19.53 | | | | | | (85) greater(zero, all_43_0) % 146.84/19.53 | | | | | | (86) greater(all_43_1, zero) % 146.84/19.53 | | | | | | (87) growth_rate(first_movers, all_30_0) = all_43_1 % 146.84/19.53 | | | | | | (88) growth_rate(efficient_producers, all_30_0) = all_43_0 % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | GROUND_INST: instantiating (13) with all_39_1, all_43_1, all_30_0, % 146.84/19.53 | | | | | | first_movers, simplifying with (64), (87) gives: % 146.84/19.53 | | | | | | (89) all_43_1 = all_39_1 % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | GROUND_INST: instantiating (13) with all_39_1, all_43_0, all_30_0, % 146.84/19.53 | | | | | | efficient_producers, simplifying with (5), (88) gives: % 146.84/19.53 | | | | | | (90) all_43_0 = all_39_1 % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | REDUCE: (86), (89) imply: % 146.84/19.53 | | | | | | (91) greater(all_39_1, zero) % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | REDUCE: (85), (90) imply: % 146.84/19.53 | | | | | | (92) greater(zero, all_39_1) % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | BETA: splitting (26) gives: % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | Case 1: % 146.84/19.53 | | | | | | | % 146.84/19.53 | | | | | | | (93) growth_rate(efficient_producers, all_30_0) = all_42_1 & % 146.84/19.53 | | | | | | | $i(all_42_1) & ~ greater_or_equal(all_42_1, zero) % 146.84/19.53 | | | | | | | % 146.84/19.53 | | | | | | | REF_CLOSE: (3), (5), (8), (13), (91), (93) are inconsistent by % 146.84/19.53 | | | | | | | sub-proof #17. % 146.84/19.53 | | | | | | | % 146.84/19.53 | | | | | | Case 2: % 146.84/19.53 | | | | | | | % 146.84/19.53 | | | | | | | (94) growth_rate(first_movers, all_30_0) = all_42_0 & % 146.84/19.53 | | | | | | | $i(all_42_0) & ~ greater(zero, all_42_0) % 146.84/19.53 | | | | | | | % 146.84/19.53 | | | | | | | REF_CLOSE: (13), (64), (92), (94) are inconsistent by sub-proof % 146.84/19.53 | | | | | | | #14. % 146.84/19.53 | | | | | | | % 146.84/19.53 | | | | | | End of split % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | End of split % 146.84/19.53 | | | | | % 146.84/19.53 | | | | End of split % 146.84/19.53 | | | | % 146.84/19.53 | | | End of split % 146.84/19.53 | | | % 146.84/19.53 | | End of split % 146.84/19.53 | | % 146.84/19.53 | Case 2: % 146.84/19.53 | | % 146.84/19.53 | | (95) all_30_0 = all_22_0 % 146.84/19.53 | | % 146.84/19.53 | | REDUCE: (5), (95) imply: % 146.84/19.53 | | (96) growth_rate(efficient_producers, all_22_0) = all_39_1 % 146.84/19.53 | | % 146.84/19.53 | | REDUCE: (10), (95) imply: % 146.84/19.53 | | (97) growth_rate(first_movers, all_22_0) = all_39_0 % 146.84/19.53 | | % 146.84/19.53 | | BETA: splitting (12) gives: % 146.84/19.53 | | % 146.84/19.53 | | Case 1: % 146.84/19.53 | | | % 146.84/19.53 | | | (98) outcompetes(efficient_producers, first_movers, all_30_0) % 146.84/19.53 | | | % 146.84/19.53 | | | PRED_UNIFY: (16), (98) imply: % 146.84/19.53 | | | (99) $false % 146.84/19.53 | | | % 146.84/19.53 | | | CLOSE: (99) is inconsistent. % 146.84/19.53 | | | % 146.84/19.53 | | Case 2: % 146.84/19.53 | | | % 146.84/19.53 | | | (100) (growth_rate(efficient_producers, all_30_0) = all_42_1 & % 146.84/19.53 | | | $i(all_42_1) & ~ greater_or_equal(all_42_1, zero)) | % 146.84/19.53 | | | (growth_rate(first_movers, all_30_0) = all_42_0 & $i(all_42_0) & % 146.84/19.53 | | | ~ greater(zero, all_42_0)) % 146.84/19.53 | | | % 146.84/19.53 | | | BETA: splitting (2) gives: % 146.84/19.53 | | | % 146.84/19.53 | | | Case 1: % 146.84/19.53 | | | | % 146.84/19.53 | | | | (101) ~ (growth_rate(first_movers, all_30_0) = all_39_1) % 146.84/19.53 | | | | % 146.84/19.53 | | | | REDUCE: (95), (101) imply: % 146.84/19.53 | | | | (102) ~ (growth_rate(first_movers, all_22_0) = all_39_1) % 146.84/19.53 | | | | % 146.84/19.53 | | | | BETA: splitting (18) gives: % 146.84/19.53 | | | | % 146.84/19.53 | | | | Case 1: % 146.84/19.53 | | | | | % 146.84/19.53 | | | | | (103) (all_43_0 = zero & all_43_1 = zero & % 146.84/19.53 | | | | | growth_rate(efficient_producers, all_30_0) = zero & % 146.84/19.53 | | | | | growth_rate(first_movers, all_30_0) = zero) | % 146.84/19.53 | | | | | (equilibrium(all_12_0) = all_43_2 & $i(all_43_2) & ~ % 146.84/19.53 | | | | | greater_or_equal(all_30_0, all_43_2)) % 146.84/19.53 | | | | | % 146.84/19.53 | | | | | BETA: splitting (103) gives: % 146.84/19.53 | | | | | % 146.84/19.53 | | | | | Case 1: % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | (104) all_43_0 = zero & all_43_1 = zero & % 146.84/19.53 | | | | | | growth_rate(efficient_producers, all_30_0) = zero & % 146.84/19.53 | | | | | | growth_rate(first_movers, all_30_0) = zero % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | ALPHA: (104) implies: % 146.84/19.53 | | | | | | (105) growth_rate(first_movers, all_30_0) = zero % 146.84/19.53 | | | | | | (106) growth_rate(efficient_producers, all_30_0) = zero % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | REDUCE: (95), (106) imply: % 146.84/19.53 | | | | | | (107) growth_rate(efficient_producers, all_22_0) = zero % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | REDUCE: (95), (105) imply: % 146.84/19.53 | | | | | | (108) growth_rate(first_movers, all_22_0) = zero % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | PRED_UNIFY: (102), (108) imply: % 146.84/19.53 | | | | | | (109) ~ (all_39_1 = zero) % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | GROUND_INST: instantiating (13) with all_39_1, zero, all_22_0, % 146.84/19.53 | | | | | | efficient_producers, simplifying with (96), (107) % 146.84/19.53 | | | | | | gives: % 146.84/19.53 | | | | | | (110) all_39_1 = zero % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | REDUCE: (109), (110) imply: % 146.84/19.53 | | | | | | (111) $false % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | CLOSE: (111) is inconsistent. % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | Case 2: % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | (112) equilibrium(all_12_0) = all_43_2 & $i(all_43_2) & ~ % 146.84/19.53 | | | | | | greater_or_equal(all_30_0, all_43_2) % 146.84/19.53 | | | | | | % 146.84/19.53 | | | | | | ALPHA: (112) implies: % 146.84/19.54 | | | | | | (113) ~ greater_or_equal(all_30_0, all_43_2) % 146.84/19.54 | | | | | | (114) equilibrium(all_12_0) = all_43_2 % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REDUCE: (95), (113) imply: % 146.84/19.54 | | | | | | (115) ~ greater_or_equal(all_22_0, all_43_2) % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REF_CLOSE: (6), (17), (20), (114), (115) are inconsistent by % 146.84/19.54 | | | | | | sub-proof #13. % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | End of split % 146.84/19.54 | | | | | % 146.84/19.54 | | | | Case 2: % 146.84/19.54 | | | | | % 146.84/19.54 | | | | | (116) (growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.54 | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.54 | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_0, zero) & % 146.84/19.54 | | | | | greater(zero, all_43_1)) | % 146.84/19.54 | | | | | (growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.54 | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.54 | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_1, zero) & % 146.84/19.54 | | | | | greater(zero, all_43_0)) % 146.84/19.54 | | | | | % 146.84/19.54 | | | | | BETA: splitting (116) gives: % 146.84/19.54 | | | | | % 146.84/19.54 | | | | | Case 1: % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | (117) growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.54 | | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.54 | | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_0, zero) & % 146.84/19.54 | | | | | | greater(zero, all_43_1) % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | ALPHA: (117) implies: % 146.84/19.54 | | | | | | (118) greater(zero, all_43_1) % 146.84/19.54 | | | | | | (119) greater(all_43_0, zero) % 146.84/19.54 | | | | | | (120) growth_rate(first_movers, all_30_0) = all_43_1 % 146.84/19.54 | | | | | | (121) growth_rate(efficient_producers, all_30_0) = all_43_0 % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REDUCE: (95), (121) imply: % 146.84/19.54 | | | | | | (122) growth_rate(efficient_producers, all_22_0) = all_43_0 % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REDUCE: (95), (120) imply: % 146.84/19.54 | | | | | | (123) growth_rate(first_movers, all_22_0) = all_43_1 % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REF_CLOSE: (3), (8), (13), (95), (96), (97), (100), (118), (119), % 146.84/19.54 | | | | | | (122), (123) are inconsistent by sub-proof #10. % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | Case 2: % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | (124) growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.54 | | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.54 | | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_1, zero) & % 146.84/19.54 | | | | | | greater(zero, all_43_0) % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | ALPHA: (124) implies: % 146.84/19.54 | | | | | | (125) greater(zero, all_43_0) % 146.84/19.54 | | | | | | (126) greater(all_43_1, zero) % 146.84/19.54 | | | | | | (127) $i(all_43_1) % 146.84/19.54 | | | | | | (128) $i(all_43_0) % 146.84/19.54 | | | | | | (129) growth_rate(first_movers, all_30_0) = all_43_1 % 146.84/19.54 | | | | | | (130) growth_rate(efficient_producers, all_30_0) = all_43_0 % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REDUCE: (95), (130) imply: % 146.84/19.54 | | | | | | (131) growth_rate(efficient_producers, all_22_0) = all_43_0 % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REDUCE: (95), (129) imply: % 146.84/19.54 | | | | | | (132) growth_rate(first_movers, all_22_0) = all_43_1 % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | GROUND_INST: instantiating (13) with all_39_0, all_43_1, all_22_0, % 146.84/19.54 | | | | | | first_movers, simplifying with (97), (132) gives: % 146.84/19.54 | | | | | | (133) all_43_1 = all_39_0 % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | GROUND_INST: instantiating (13) with all_39_1, all_43_0, all_22_0, % 146.84/19.54 | | | | | | efficient_producers, simplifying with (96), (131) % 146.84/19.54 | | | | | | gives: % 146.84/19.54 | | | | | | (134) all_43_0 = all_39_1 % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REDUCE: (128), (134) imply: % 146.84/19.54 | | | | | | (135) $i(all_39_1) % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REDUCE: (127), (133) imply: % 146.84/19.54 | | | | | | (136) $i(all_39_0) % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REDUCE: (126), (133) imply: % 146.84/19.54 | | | | | | (137) greater(all_39_0, zero) % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | REDUCE: (125), (134) imply: % 146.84/19.54 | | | | | | (138) greater(zero, all_39_1) % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | GROUND_INST: instantiating (7) with zero, all_39_1, all_39_0, % 146.84/19.54 | | | | | | simplifying with (3), (4), (135), (136), (138) gives: % 146.84/19.54 | | | | | | (139) greater(zero, all_39_0) % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | GROUND_INST: instantiating (7) with all_39_1, all_39_0, zero, % 146.84/19.54 | | | | | | simplifying with (3), (4), (135), (136), (137) gives: % 146.84/19.54 | | | | | | (140) greater(all_39_1, zero) % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | BETA: splitting (100) gives: % 146.84/19.54 | | | | | | % 146.84/19.54 | | | | | | Case 1: % 146.84/19.54 | | | | | | | % 146.84/19.54 | | | | | | | (141) growth_rate(efficient_producers, all_30_0) = all_42_1 & % 146.84/19.54 | | | | | | | $i(all_42_1) & ~ greater_or_equal(all_42_1, zero) % 146.84/19.54 | | | | | | | % 146.84/19.54 | | | | | | | REF_CLOSE: (3), (8), (13), (95), (96), (140), (141) are % 146.84/19.54 | | | | | | | inconsistent by sub-proof #9. % 146.84/19.54 | | | | | | | % 146.84/19.54 | | | | | | Case 2: % 146.84/19.54 | | | | | | | % 146.84/19.54 | | | | | | | (142) growth_rate(first_movers, all_30_0) = all_42_0 & % 146.84/19.54 | | | | | | | $i(all_42_0) & ~ greater(zero, all_42_0) % 146.84/19.54 | | | | | | | % 146.84/19.54 | | | | | | | ALPHA: (142) implies: % 146.84/19.54 | | | | | | | (143) ~ greater(zero, all_42_0) % 146.84/19.55 | | | | | | | (144) growth_rate(first_movers, all_30_0) = all_42_0 % 146.84/19.55 | | | | | | | % 146.84/19.55 | | | | | | | REDUCE: (95), (144) imply: % 146.84/19.55 | | | | | | | (145) growth_rate(first_movers, all_22_0) = all_42_0 % 146.84/19.55 | | | | | | | % 146.84/19.55 | | | | | | | REF_CLOSE: (13), (97), (139), (143), (145) are inconsistent by % 146.84/19.55 | | | | | | | sub-proof #11. % 146.84/19.55 | | | | | | | % 146.84/19.55 | | | | | | End of split % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | End of split % 146.84/19.55 | | | | | % 146.84/19.55 | | | | End of split % 146.84/19.55 | | | | % 146.84/19.55 | | | Case 2: % 146.84/19.55 | | | | % 146.84/19.55 | | | | (146) all_39_0 = all_39_1 % 146.84/19.55 | | | | (147) growth_rate(first_movers, all_30_0) = all_39_1 % 146.84/19.55 | | | | % 146.84/19.55 | | | | REDUCE: (97), (146) imply: % 146.84/19.55 | | | | (148) growth_rate(first_movers, all_22_0) = all_39_1 % 146.84/19.55 | | | | % 146.84/19.55 | | | | REDUCE: (15), (146) imply: % 146.84/19.55 | | | | (149) greater_or_equal(all_39_1, all_39_1) % 146.84/19.55 | | | | % 146.84/19.55 | | | | REDUCE: (4), (146) imply: % 146.84/19.55 | | | | (150) greater(all_39_1, all_39_1) % 146.84/19.55 | | | | % 146.84/19.55 | | | | BETA: splitting (18) gives: % 146.84/19.55 | | | | % 146.84/19.55 | | | | Case 1: % 146.84/19.55 | | | | | % 146.84/19.55 | | | | | (151) (all_43_0 = zero & all_43_1 = zero & % 146.84/19.55 | | | | | growth_rate(efficient_producers, all_30_0) = zero & % 146.84/19.55 | | | | | growth_rate(first_movers, all_30_0) = zero) | % 146.84/19.55 | | | | | (equilibrium(all_12_0) = all_43_2 & $i(all_43_2) & ~ % 146.84/19.55 | | | | | greater_or_equal(all_30_0, all_43_2)) % 146.84/19.55 | | | | | % 146.84/19.55 | | | | | BETA: splitting (151) gives: % 146.84/19.55 | | | | | % 146.84/19.55 | | | | | Case 1: % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | (152) all_43_0 = zero & all_43_1 = zero & % 146.84/19.55 | | | | | | growth_rate(efficient_producers, all_30_0) = zero & % 146.84/19.55 | | | | | | growth_rate(first_movers, all_30_0) = zero % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | REF_CLOSE: (5), (13), (100), (147), (149), (150), (152) are % 146.84/19.55 | | | | | | inconsistent by sub-proof #15. % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | Case 2: % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | (153) equilibrium(all_12_0) = all_43_2 & $i(all_43_2) & ~ % 146.84/19.55 | | | | | | greater_or_equal(all_30_0, all_43_2) % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | ALPHA: (153) implies: % 146.84/19.55 | | | | | | (154) ~ greater_or_equal(all_30_0, all_43_2) % 146.84/19.55 | | | | | | (155) equilibrium(all_12_0) = all_43_2 % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | REDUCE: (95), (154) imply: % 146.84/19.55 | | | | | | (156) ~ greater_or_equal(all_22_0, all_43_2) % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | REF_CLOSE: (6), (17), (20), (155), (156) are inconsistent by % 146.84/19.55 | | | | | | sub-proof #13. % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | End of split % 146.84/19.55 | | | | | % 146.84/19.55 | | | | Case 2: % 146.84/19.55 | | | | | % 146.84/19.55 | | | | | (157) (growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.55 | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.55 | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_0, zero) & % 146.84/19.55 | | | | | greater(zero, all_43_1)) | % 146.84/19.55 | | | | | (growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.55 | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.55 | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_1, zero) & % 146.84/19.55 | | | | | greater(zero, all_43_0)) % 146.84/19.55 | | | | | % 146.84/19.55 | | | | | BETA: splitting (157) gives: % 146.84/19.55 | | | | | % 146.84/19.55 | | | | | Case 1: % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | (158) growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.55 | | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.55 | | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_0, zero) & % 146.84/19.55 | | | | | | greater(zero, all_43_1) % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | ALPHA: (158) implies: % 146.84/19.55 | | | | | | (159) greater(zero, all_43_1) % 146.84/19.55 | | | | | | (160) greater(all_43_0, zero) % 146.84/19.55 | | | | | | (161) growth_rate(first_movers, all_30_0) = all_43_1 % 146.84/19.55 | | | | | | (162) growth_rate(efficient_producers, all_30_0) = all_43_0 % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | REDUCE: (95), (162) imply: % 146.84/19.55 | | | | | | (163) growth_rate(efficient_producers, all_22_0) = all_43_0 % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | REDUCE: (95), (161) imply: % 146.84/19.55 | | | | | | (164) growth_rate(first_movers, all_22_0) = all_43_1 % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | REF_CLOSE: (3), (8), (13), (95), (96), (97), (100), (159), (160), % 146.84/19.55 | | | | | | (163), (164) are inconsistent by sub-proof #10. % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | Case 2: % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | (165) growth_rate(efficient_producers, all_30_0) = all_43_0 & % 146.84/19.55 | | | | | | growth_rate(first_movers, all_30_0) = all_43_1 & % 146.84/19.55 | | | | | | $i(all_43_0) & $i(all_43_1) & greater(all_43_1, zero) & % 146.84/19.55 | | | | | | greater(zero, all_43_0) % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | ALPHA: (165) implies: % 146.84/19.55 | | | | | | (166) greater(zero, all_43_0) % 146.84/19.55 | | | | | | (167) greater(all_43_1, zero) % 146.84/19.55 | | | | | | (168) growth_rate(first_movers, all_30_0) = all_43_1 % 146.84/19.55 | | | | | | (169) growth_rate(efficient_producers, all_30_0) = all_43_0 % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | REDUCE: (95), (169) imply: % 146.84/19.55 | | | | | | (170) growth_rate(efficient_producers, all_22_0) = all_43_0 % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | REDUCE: (95), (168) imply: % 146.84/19.55 | | | | | | (171) growth_rate(first_movers, all_22_0) = all_43_1 % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | GROUND_INST: instantiating (13) with all_39_1, all_43_1, all_22_0, % 146.84/19.55 | | | | | | first_movers, simplifying with (148), (171) gives: % 146.84/19.55 | | | | | | (172) all_43_1 = all_39_1 % 146.84/19.55 | | | | | | % 146.84/19.55 | | | | | | GROUND_INST: instantiating (13) with all_39_1, all_43_0, all_22_0, % 146.84/19.55 | | | | | | efficient_producers, simplifying with (96), (170) % 146.84/19.55 | | | | | | gives: % 146.84/19.56 | | | | | | (173) all_43_0 = all_39_1 % 146.84/19.56 | | | | | | % 146.84/19.56 | | | | | | REDUCE: (167), (172) imply: % 146.84/19.56 | | | | | | (174) greater(all_39_1, zero) % 146.84/19.56 | | | | | | % 146.84/19.56 | | | | | | REDUCE: (166), (173) imply: % 146.84/19.56 | | | | | | (175) greater(zero, all_39_1) % 146.84/19.56 | | | | | | % 146.84/19.56 | | | | | | BETA: splitting (100) gives: % 146.84/19.56 | | | | | | % 146.84/19.56 | | | | | | Case 1: % 146.84/19.56 | | | | | | | % 146.84/19.56 | | | | | | | (176) growth_rate(efficient_producers, all_30_0) = all_42_1 & % 146.84/19.56 | | | | | | | $i(all_42_1) & ~ greater_or_equal(all_42_1, zero) % 146.84/19.56 | | | | | | | % 146.84/19.56 | | | | | | | REF_CLOSE: (3), (8), (13), (95), (96), (174), (176) are % 146.84/19.56 | | | | | | | inconsistent by sub-proof #9. % 146.84/19.56 | | | | | | | % 146.84/19.56 | | | | | | Case 2: % 146.84/19.56 | | | | | | | % 146.84/19.56 | | | | | | | (177) growth_rate(first_movers, all_30_0) = all_42_0 & % 146.84/19.56 | | | | | | | $i(all_42_0) & ~ greater(zero, all_42_0) % 146.84/19.56 | | | | | | | % 146.84/19.56 | | | | | | | REF_CLOSE: (13), (147), (175), (177) are inconsistent by sub-proof % 146.84/19.56 | | | | | | | #14. % 146.84/19.56 | | | | | | | % 146.84/19.56 | | | | | | End of split % 146.84/19.56 | | | | | | % 146.84/19.56 | | | | | End of split % 146.84/19.56 | | | | | % 146.84/19.56 | | | | End of split % 146.84/19.56 | | | | % 146.84/19.56 | | | End of split % 146.84/19.56 | | | % 146.84/19.56 | | End of split % 146.84/19.56 | | % 146.84/19.56 | End of split % 146.84/19.56 | % 146.84/19.56 End of proof % 146.84/19.56 % 146.84/19.56 Sub-proof #9 shows that the following formulas are inconsistent: % 146.84/19.56 ---------------------------------------------------------------- % 146.84/19.56 (1) $i(zero) % 146.84/19.56 (2) growth_rate(efficient_producers, all_22_0) = all_39_1 % 146.84/19.56 (3) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 146.84/19.56 greater_or_equal(v0, v1)) % 146.84/19.56 (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.84/19.56 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.84/19.56 (5) all_30_0 = all_22_0 % 146.84/19.56 (6) growth_rate(efficient_producers, all_30_0) = all_42_1 & $i(all_42_1) & ~ % 146.84/19.56 greater_or_equal(all_42_1, zero) % 146.84/19.56 (7) greater(all_39_1, zero) % 146.84/19.56 % 146.84/19.56 Begin of proof % 146.84/19.56 | % 146.84/19.56 | ALPHA: (6) implies: % 146.84/19.56 | (8) ~ greater_or_equal(all_42_1, zero) % 146.84/19.56 | (9) $i(all_42_1) % 146.84/19.56 | (10) growth_rate(efficient_producers, all_30_0) = all_42_1 % 146.84/19.56 | % 146.84/19.56 | REDUCE: (5), (10) imply: % 146.84/19.56 | (11) growth_rate(efficient_producers, all_22_0) = all_42_1 % 146.84/19.56 | % 146.84/19.56 | REF_CLOSE: (1), (2), (3), (4), (7), (8), (9), (11) are inconsistent by % 146.84/19.56 | sub-proof #12. % 146.84/19.56 | % 146.84/19.56 End of proof % 146.84/19.56 % 146.84/19.56 Sub-proof #10 shows that the following formulas are inconsistent: % 146.84/19.56 ---------------------------------------------------------------- % 146.84/19.56 (1) greater(zero, all_43_1) % 146.84/19.56 (2) $i(zero) % 146.84/19.56 (3) greater(all_43_0, zero) % 146.84/19.56 (4) growth_rate(efficient_producers, all_22_0) = all_39_1 % 146.84/19.56 (5) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 146.84/19.56 greater_or_equal(v0, v1)) % 146.84/19.56 (6) growth_rate(first_movers, all_22_0) = all_39_0 % 146.84/19.56 (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.84/19.56 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.84/19.56 (8) (growth_rate(efficient_producers, all_30_0) = all_42_1 & $i(all_42_1) & % 146.84/19.56 ~ greater_or_equal(all_42_1, zero)) | (growth_rate(first_movers, % 146.84/19.56 all_30_0) = all_42_0 & $i(all_42_0) & ~ greater(zero, all_42_0)) % 146.84/19.56 (9) all_30_0 = all_22_0 % 146.84/19.56 (10) growth_rate(efficient_producers, all_22_0) = all_43_0 % 146.84/19.56 (11) growth_rate(first_movers, all_22_0) = all_43_1 % 146.84/19.56 % 146.84/19.56 Begin of proof % 146.84/19.56 | % 146.84/19.56 | GROUND_INST: instantiating (7) with all_39_0, all_43_1, all_22_0, % 146.84/19.56 | first_movers, simplifying with (6), (11) gives: % 146.84/19.56 | (12) all_43_1 = all_39_0 % 146.84/19.56 | % 146.84/19.56 | GROUND_INST: instantiating (7) with all_39_1, all_43_0, all_22_0, % 146.84/19.56 | efficient_producers, simplifying with (4), (10) gives: % 146.84/19.56 | (13) all_43_0 = all_39_1 % 146.84/19.56 | % 146.84/19.56 | REDUCE: (3), (13) imply: % 146.84/19.56 | (14) greater(all_39_1, zero) % 146.84/19.56 | % 146.84/19.56 | REDUCE: (1), (12) imply: % 146.84/19.56 | (15) greater(zero, all_39_0) % 146.84/19.56 | % 146.84/19.56 | BETA: splitting (8) gives: % 146.84/19.56 | % 146.84/19.56 | Case 1: % 146.84/19.56 | | % 146.84/19.56 | | (16) growth_rate(efficient_producers, all_30_0) = all_42_1 & $i(all_42_1) % 146.84/19.56 | | & ~ greater_or_equal(all_42_1, zero) % 146.84/19.56 | | % 146.84/19.56 | | ALPHA: (16) implies: % 146.84/19.56 | | (17) ~ greater_or_equal(all_42_1, zero) % 146.84/19.56 | | (18) $i(all_42_1) % 146.84/19.57 | | (19) growth_rate(efficient_producers, all_30_0) = all_42_1 % 146.84/19.57 | | % 146.84/19.57 | | REDUCE: (9), (19) imply: % 146.84/19.57 | | (20) growth_rate(efficient_producers, all_22_0) = all_42_1 % 146.84/19.57 | | % 146.84/19.57 | | REF_CLOSE: (2), (4), (5), (7), (14), (17), (18), (20) are inconsistent by % 146.84/19.57 | | sub-proof #12. % 146.84/19.57 | | % 146.84/19.57 | Case 2: % 146.84/19.57 | | % 146.84/19.57 | | (21) growth_rate(first_movers, all_30_0) = all_42_0 & $i(all_42_0) & ~ % 146.84/19.57 | | greater(zero, all_42_0) % 146.84/19.57 | | % 146.84/19.57 | | ALPHA: (21) implies: % 146.84/19.57 | | (22) ~ greater(zero, all_42_0) % 146.84/19.57 | | (23) growth_rate(first_movers, all_30_0) = all_42_0 % 146.84/19.57 | | % 146.84/19.57 | | REDUCE: (9), (23) imply: % 146.84/19.57 | | (24) growth_rate(first_movers, all_22_0) = all_42_0 % 146.84/19.57 | | % 146.84/19.57 | | REF_CLOSE: (6), (7), (15), (22), (24) are inconsistent by sub-proof #11. % 146.84/19.57 | | % 146.84/19.57 | End of split % 146.84/19.57 | % 146.84/19.57 End of proof % 146.84/19.57 % 146.84/19.57 Sub-proof #11 shows that the following formulas are inconsistent: % 146.84/19.57 ---------------------------------------------------------------- % 146.84/19.57 (1) growth_rate(first_movers, all_22_0) = all_39_0 % 146.84/19.57 (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.84/19.57 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.84/19.57 (3) growth_rate(first_movers, all_22_0) = all_42_0 % 146.84/19.57 (4) greater(zero, all_39_0) % 146.84/19.57 (5) ~ greater(zero, all_42_0) % 146.84/19.57 % 146.84/19.57 Begin of proof % 146.84/19.57 | % 146.84/19.57 | GROUND_INST: instantiating (2) with all_39_0, all_42_0, all_22_0, % 146.84/19.57 | first_movers, simplifying with (1), (3) gives: % 146.84/19.57 | (6) all_42_0 = all_39_0 % 146.84/19.57 | % 146.84/19.57 | PRED_UNIFY: (4), (5) imply: % 146.84/19.57 | (7) ~ (all_42_0 = all_39_0) % 146.84/19.57 | % 146.84/19.57 | REDUCE: (6), (7) imply: % 146.84/19.57 | (8) $false % 146.84/19.57 | % 146.84/19.57 | CLOSE: (8) is inconsistent. % 146.84/19.57 | % 146.84/19.57 End of proof % 146.84/19.57 % 146.84/19.57 Sub-proof #12 shows that the following formulas are inconsistent: % 146.84/19.57 ---------------------------------------------------------------- % 146.84/19.57 (1) $i(zero) % 146.84/19.57 (2) growth_rate(efficient_producers, all_22_0) = all_39_1 % 146.84/19.57 (3) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 146.84/19.57 greater_or_equal(v0, v1)) % 146.84/19.57 (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.84/19.57 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.84/19.57 (5) ~ greater_or_equal(all_42_1, zero) % 146.84/19.57 (6) $i(all_42_1) % 146.84/19.57 (7) growth_rate(efficient_producers, all_22_0) = all_42_1 % 146.84/19.57 (8) greater(all_39_1, zero) % 146.84/19.57 % 146.84/19.57 Begin of proof % 146.84/19.57 | % 146.84/19.57 | GROUND_INST: instantiating (4) with all_39_1, all_42_1, all_22_0, % 146.84/19.57 | efficient_producers, simplifying with (2), (7) gives: % 146.84/19.57 | (9) all_42_1 = all_39_1 % 146.84/19.57 | % 146.84/19.58 | REDUCE: (6), (9) imply: % 146.84/19.58 | (10) $i(all_39_1) % 146.84/19.58 | % 146.84/19.58 | REDUCE: (5), (9) imply: % 146.84/19.58 | (11) ~ greater_or_equal(all_39_1, zero) % 146.84/19.58 | % 146.84/19.58 | GROUND_INST: instantiating (3) with all_39_1, zero, simplifying with (1), (8), % 146.84/19.58 | (10), (11) gives: % 146.84/19.58 | (12) $false % 146.84/19.58 | % 146.84/19.58 | CLOSE: (12) is inconsistent. % 146.84/19.58 | % 146.84/19.58 End of proof % 146.84/19.58 % 146.84/19.58 Sub-proof #13 shows that the following formulas are inconsistent: % 146.84/19.58 ---------------------------------------------------------------- % 146.84/19.58 (1) equilibrium(all_12_0) = all_43_2 % 146.84/19.58 (2) ~ greater_or_equal(all_22_0, all_43_2) % 146.84/19.58 (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 146.84/19.58 = v1) | ~ (equilibrium(v2) = v0)) % 146.84/19.58 (4) greater_or_equal(all_22_0, all_20_1) % 146.84/19.58 (5) equilibrium(all_12_0) = all_20_1 % 146.84/19.58 % 146.84/19.58 Begin of proof % 146.84/19.58 | % 146.84/19.58 | GROUND_INST: instantiating (3) with all_20_1, all_43_2, all_12_0, simplifying % 146.84/19.58 | with (1), (5) gives: % 146.84/19.58 | (6) all_43_2 = all_20_1 % 146.84/19.58 | % 146.84/19.58 | PRED_UNIFY: (2), (4) imply: % 146.84/19.58 | (7) ~ (all_43_2 = all_20_1) % 146.84/19.58 | % 146.84/19.58 | REDUCE: (6), (7) imply: % 146.84/19.58 | (8) $false % 146.84/19.58 | % 146.84/19.58 | CLOSE: (8) is inconsistent. % 146.84/19.58 | % 146.84/19.58 End of proof % 146.84/19.58 % 146.84/19.58 Sub-proof #14 shows that the following formulas are inconsistent: % 146.84/19.58 ---------------------------------------------------------------- % 146.84/19.58 (1) growth_rate(first_movers, all_30_0) = all_42_0 & $i(all_42_0) & ~ % 146.84/19.58 greater(zero, all_42_0) % 146.84/19.58 (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.84/19.58 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.84/19.58 (3) growth_rate(first_movers, all_30_0) = all_39_1 % 146.84/19.58 (4) greater(zero, all_39_1) % 146.84/19.58 % 146.84/19.58 Begin of proof % 146.84/19.58 | % 146.84/19.58 | ALPHA: (1) implies: % 146.84/19.58 | (5) ~ greater(zero, all_42_0) % 146.84/19.58 | (6) growth_rate(first_movers, all_30_0) = all_42_0 % 146.84/19.58 | % 146.84/19.58 | GROUND_INST: instantiating (2) with all_39_1, all_42_0, all_30_0, % 146.84/19.58 | first_movers, simplifying with (3), (6) gives: % 146.84/19.58 | (7) all_42_0 = all_39_1 % 146.84/19.58 | % 146.84/19.58 | PRED_UNIFY: (4), (5) imply: % 146.84/19.58 | (8) ~ (all_42_0 = all_39_1) % 146.84/19.58 | % 146.84/19.58 | REDUCE: (7), (8) imply: % 146.84/19.58 | (9) $false % 146.84/19.58 | % 146.84/19.58 | CLOSE: (9) is inconsistent. % 146.84/19.58 | % 146.84/19.58 End of proof % 146.84/19.58 % 146.84/19.58 Sub-proof #15 shows that the following formulas are inconsistent: % 146.84/19.58 ---------------------------------------------------------------- % 146.84/19.58 (1) growth_rate(efficient_producers, all_30_0) = all_39_1 % 146.84/19.58 (2) greater(all_39_1, all_39_1) % 146.84/19.58 (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.84/19.58 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.84/19.58 (4) all_43_0 = zero & all_43_1 = zero & growth_rate(efficient_producers, % 146.84/19.58 all_30_0) = zero & growth_rate(first_movers, all_30_0) = zero % 146.84/19.58 (5) (growth_rate(efficient_producers, all_30_0) = all_42_1 & $i(all_42_1) & % 146.84/19.58 ~ greater_or_equal(all_42_1, zero)) | (growth_rate(first_movers, % 146.84/19.58 all_30_0) = all_42_0 & $i(all_42_0) & ~ greater(zero, all_42_0)) % 146.84/19.58 (6) greater_or_equal(all_39_1, all_39_1) % 146.84/19.58 (7) growth_rate(first_movers, all_30_0) = all_39_1 % 146.84/19.58 % 146.84/19.58 Begin of proof % 146.84/19.58 | % 146.84/19.58 | ALPHA: (4) implies: % 146.84/19.58 | (8) growth_rate(efficient_producers, all_30_0) = zero % 146.84/19.58 | % 146.84/19.58 | GROUND_INST: instantiating (3) with all_39_1, zero, all_30_0, % 146.84/19.58 | efficient_producers, simplifying with (1), (8) gives: % 146.84/19.58 | (9) all_39_1 = zero % 146.84/19.58 | % 146.84/19.58 | REDUCE: (7), (9) imply: % 146.84/19.58 | (10) growth_rate(first_movers, all_30_0) = zero % 146.84/19.58 | % 146.84/19.58 | REDUCE: (6), (9) imply: % 146.84/19.58 | (11) greater_or_equal(zero, zero) % 146.84/19.58 | % 146.84/19.58 | REDUCE: (2), (9) imply: % 146.84/19.58 | (12) greater(zero, zero) % 146.84/19.58 | % 146.84/19.58 | BETA: splitting (5) gives: % 146.84/19.58 | % 146.84/19.58 | Case 1: % 146.84/19.58 | | % 146.84/19.59 | | (13) growth_rate(efficient_producers, all_30_0) = all_42_1 & $i(all_42_1) % 146.84/19.59 | | & ~ greater_or_equal(all_42_1, zero) % 146.84/19.59 | | % 146.84/19.59 | | ALPHA: (13) implies: % 146.84/19.59 | | (14) ~ greater_or_equal(all_42_1, zero) % 146.84/19.59 | | (15) growth_rate(efficient_producers, all_30_0) = all_42_1 % 146.84/19.59 | | % 146.84/19.59 | | GROUND_INST: instantiating (3) with zero, all_42_1, all_30_0, % 146.84/19.59 | | efficient_producers, simplifying with (8), (15) gives: % 146.84/19.59 | | (16) all_42_1 = zero % 146.84/19.59 | | % 146.84/19.59 | | PRED_UNIFY: (11), (14) imply: % 146.84/19.59 | | (17) ~ (all_42_1 = zero) % 146.84/19.59 | | % 146.84/19.59 | | REDUCE: (16), (17) imply: % 146.84/19.59 | | (18) $false % 146.84/19.59 | | % 146.84/19.59 | | CLOSE: (18) is inconsistent. % 146.84/19.59 | | % 146.84/19.59 | Case 2: % 146.84/19.59 | | % 146.84/19.59 | | (19) growth_rate(first_movers, all_30_0) = all_42_0 & $i(all_42_0) & ~ % 146.84/19.59 | | greater(zero, all_42_0) % 146.84/19.59 | | % 146.84/19.59 | | ALPHA: (19) implies: % 146.84/19.59 | | (20) ~ greater(zero, all_42_0) % 146.84/19.59 | | (21) growth_rate(first_movers, all_30_0) = all_42_0 % 146.84/19.59 | | % 146.84/19.59 | | GROUND_INST: instantiating (3) with zero, all_42_0, all_30_0, first_movers, % 146.84/19.59 | | simplifying with (10), (21) gives: % 146.84/19.59 | | (22) all_42_0 = zero % 146.84/19.59 | | % 146.84/19.59 | | PRED_UNIFY: (12), (20) imply: % 146.84/19.59 | | (23) ~ (all_42_0 = zero) % 146.84/19.59 | | % 146.84/19.59 | | REDUCE: (22), (23) imply: % 146.84/19.59 | | (24) $false % 146.84/19.59 | | % 146.84/19.59 | | CLOSE: (24) is inconsistent. % 146.84/19.59 | | % 146.84/19.59 | End of split % 146.84/19.59 | % 146.84/19.59 End of proof % 146.84/19.59 % 146.84/19.59 Sub-proof #16 shows that the following formulas are inconsistent: % 146.84/19.59 ---------------------------------------------------------------- % 146.84/19.59 (1) $i(zero) % 146.84/19.59 (2) growth_rate(efficient_producers, all_30_0) = all_39_1 % 146.84/19.59 (3) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 146.84/19.59 greater_or_equal(v0, v1)) % 146.84/19.59 (4) growth_rate(first_movers, all_30_0) = all_39_0 % 146.84/19.59 (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.84/19.59 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.84/19.59 (6) (growth_rate(efficient_producers, all_30_0) = all_42_1 & $i(all_42_1) & % 146.84/19.59 ~ greater_or_equal(all_42_1, zero)) | (growth_rate(first_movers, % 146.84/19.59 all_30_0) = all_42_0 & $i(all_42_0) & ~ greater(zero, all_42_0)) % 146.84/19.59 (7) greater(zero, all_39_0) % 146.84/19.59 (8) greater(all_39_1, zero) % 146.84/19.59 % 146.84/19.59 Begin of proof % 146.84/19.59 | % 146.84/19.59 | BETA: splitting (6) gives: % 146.84/19.59 | % 146.84/19.59 | Case 1: % 146.84/19.59 | | % 146.84/19.59 | | (9) growth_rate(efficient_producers, all_30_0) = all_42_1 & $i(all_42_1) % 146.84/19.59 | | & ~ greater_or_equal(all_42_1, zero) % 146.84/19.59 | | % 146.84/19.59 | | REF_CLOSE: (1), (2), (3), (5), (8), (9) are inconsistent by sub-proof #17. % 146.84/19.59 | | % 146.84/19.59 | Case 2: % 146.84/19.59 | | % 146.84/19.59 | | (10) growth_rate(first_movers, all_30_0) = all_42_0 & $i(all_42_0) & ~ % 146.84/19.59 | | greater(zero, all_42_0) % 146.84/19.59 | | % 146.84/19.59 | | ALPHA: (10) implies: % 146.84/19.59 | | (11) ~ greater(zero, all_42_0) % 146.84/19.59 | | (12) growth_rate(first_movers, all_30_0) = all_42_0 % 146.84/19.59 | | % 146.84/19.59 | | GROUND_INST: instantiating (5) with all_39_0, all_42_0, all_30_0, % 146.84/19.59 | | first_movers, simplifying with (4), (12) gives: % 146.84/19.59 | | (13) all_42_0 = all_39_0 % 146.84/19.59 | | % 146.84/19.59 | | PRED_UNIFY: (7), (11) imply: % 146.84/19.59 | | (14) ~ (all_42_0 = all_39_0) % 146.84/19.59 | | % 146.84/19.59 | | REDUCE: (13), (14) imply: % 146.84/19.59 | | (15) $false % 146.84/19.59 | | % 146.84/19.59 | | CLOSE: (15) is inconsistent. % 146.84/19.59 | | % 146.84/19.59 | End of split % 146.84/19.59 | % 146.84/19.59 End of proof % 146.84/19.59 % 146.84/19.59 Sub-proof #17 shows that the following formulas are inconsistent: % 146.84/19.59 ---------------------------------------------------------------- % 146.84/19.59 (1) $i(zero) % 146.84/19.59 (2) growth_rate(efficient_producers, all_30_0) = all_39_1 % 146.84/19.59 (3) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | % 146.84/19.59 greater_or_equal(v0, v1)) % 146.84/19.60 (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 146.84/19.60 (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, v2) = v0)) % 146.84/19.60 (5) growth_rate(efficient_producers, all_30_0) = all_42_1 & $i(all_42_1) & ~ % 146.84/19.60 greater_or_equal(all_42_1, zero) % 146.84/19.60 (6) greater(all_39_1, zero) % 146.84/19.60 % 146.84/19.60 Begin of proof % 146.84/19.60 | % 146.84/19.60 | ALPHA: (5) implies: % 146.84/19.60 | (7) ~ greater_or_equal(all_42_1, zero) % 146.84/19.60 | (8) $i(all_42_1) % 147.35/19.60 | (9) growth_rate(efficient_producers, all_30_0) = all_42_1 % 147.35/19.60 | % 147.35/19.60 | GROUND_INST: instantiating (4) with all_39_1, all_42_1, all_30_0, % 147.35/19.60 | efficient_producers, simplifying with (2), (9) gives: % 147.35/19.60 | (10) all_42_1 = all_39_1 % 147.35/19.60 | % 147.35/19.60 | REDUCE: (8), (10) imply: % 147.35/19.60 | (11) $i(all_39_1) % 147.35/19.60 | % 147.35/19.60 | REDUCE: (7), (10) imply: % 147.35/19.60 | (12) ~ greater_or_equal(all_39_1, zero) % 147.35/19.60 | % 147.35/19.60 | GROUND_INST: instantiating (3) with all_39_1, zero, simplifying with (1), (6), % 147.35/19.60 | (11), (12) gives: % 147.35/19.60 | (13) $false % 147.35/19.60 | % 147.35/19.60 | CLOSE: (13) is inconsistent. % 147.35/19.60 | % 147.35/19.60 End of proof % 147.35/19.60 % 147.35/19.60 Sub-proof #18 shows that the following formulas are inconsistent: % 147.35/19.60 ---------------------------------------------------------------- % 147.35/19.60 (1) ~ greater_or_equal(all_30_0, all_43_2) % 147.35/19.60 (2) equilibrium(all_12_0) = all_43_2 % 147.35/19.60 (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (equilibrium(v2) % 147.35/19.60 = v1) | ~ (equilibrium(v2) = v0)) % 147.35/19.60 (4) equilibrium(all_12_0) = all_20_1 % 147.35/19.60 (5) greater_or_equal(all_30_0, all_20_1) % 147.35/19.60 % 147.35/19.60 Begin of proof % 147.35/19.60 | % 147.35/19.60 | GROUND_INST: instantiating (3) with all_20_1, all_43_2, all_12_0, simplifying % 147.35/19.60 | with (2), (4) gives: % 147.35/19.60 | (6) all_43_2 = all_20_1 % 147.35/19.60 | % 147.35/19.60 | PRED_UNIFY: (1), (5) imply: % 147.35/19.60 | (7) ~ (all_43_2 = all_20_1) % 147.35/19.60 | % 147.35/19.60 | REDUCE: (6), (7) imply: % 147.35/19.60 | (8) $false % 147.35/19.60 | % 147.35/19.60 | CLOSE: (8) is inconsistent. % 147.35/19.60 | % 147.35/19.60 End of proof % 147.35/19.60 % SZS output end Proof for theBenchmark % 147.35/19.60 % 147.35/19.60 19011ms %------------------------------------------------------------------------------