%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : MGT030+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 : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:17:22 AM UTC 2026 % Result : Theorem 7.86s 1.87s % Output : Proof 12.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT030+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 : n001.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:23:52 UTC 2026 % 0.09/0.36 % CPUTime : % 0.12/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.66/0.72 ________ _____ % 0.66/0.72 ___ __ \_________(_)________________________________ % 0.66/0.72 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.66/0.72 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.66/0.72 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.66/0.72 % 0.66/0.72 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.66/0.72 (2023-06-19) % 0.66/0.72 % 0.66/0.72 (c) Philipp Rümmer, 2009-2023 % 0.66/0.72 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.66/0.72 Amanda Stjerna. % 0.66/0.72 Free software under BSD-3-Clause. % 0.66/0.72 % 0.66/0.72 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.66/0.72 % 0.66/0.72 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.66/0.74 Running up to 7 provers in parallel. % 0.66/0.75 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.66/0.75 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.66/0.75 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.66/0.75 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.66/0.75 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.66/0.75 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.66/0.75 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.68/1.14 Prover 1: Preprocessing ... % 2.68/1.14 Prover 4: Preprocessing ... % 3.14/1.20 Prover 2: Preprocessing ... % 3.14/1.20 Prover 5: Preprocessing ... % 3.14/1.20 Prover 3: Preprocessing ... % 3.14/1.20 Prover 6: Preprocessing ... % 3.14/1.20 Prover 0: Preprocessing ... % 5.50/1.53 Prover 1: Constructing countermodel ... % 5.50/1.53 Prover 2: Proving ... % 5.50/1.53 Prover 6: Proving ... % 5.50/1.53 Prover 5: Constructing countermodel ... % 5.50/1.53 Prover 3: Constructing countermodel ... % 7.05/1.71 Prover 4: Constructing countermodel ... % 7.05/1.73 Prover 0: Proving ... % 7.86/1.87 Prover 3: proved (1115ms) % 7.86/1.87 % 7.86/1.87 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.86/1.87 % 7.86/1.87 Prover 5: stopped % 7.86/1.88 Prover 6: stopped % 7.86/1.88 Prover 2: stopped % 7.86/1.88 Prover 0: stopped % 7.86/1.88 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 7.86/1.88 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 7.86/1.88 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 7.86/1.88 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 7.86/1.88 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 8.61/1.92 Prover 11: Preprocessing ... % 8.61/1.93 Prover 7: Preprocessing ... % 8.61/1.94 Prover 10: Preprocessing ... % 8.61/1.94 Prover 8: Preprocessing ... % 8.61/1.95 Prover 13: Preprocessing ... % 8.61/2.03 Prover 10: Constructing countermodel ... % 8.61/2.03 Prover 8: Warning: ignoring some quantifiers % 8.61/2.04 Prover 8: Constructing countermodel ... % 8.61/2.06 Prover 7: Constructing countermodel ... % 9.85/2.12 Prover 13: Constructing countermodel ... % 10.66/2.17 Prover 11: Constructing countermodel ... % 10.95/2.23 Prover 1: Found proof (size 70) % 10.95/2.23 Prover 1: proved (1486ms) % 10.95/2.24 Prover 10: stopped % 10.95/2.24 Prover 8: stopped % 10.95/2.24 Prover 13: stopped % 10.95/2.24 Prover 11: stopped % 10.95/2.24 Prover 4: stopped % 10.95/2.24 Prover 7: stopped % 10.95/2.24 % 10.95/2.24 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.95/2.24 % 10.95/2.25 % SZS output start Proof for theBenchmark % 10.95/2.25 Assumptions after simplification: % 10.95/2.25 --------------------------------- % 10.95/2.25 % 10.95/2.25 (l1) % 10.95/2.28 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ( ~ (stable(v0) = % 10.95/2.28 0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & environment(v0) = v1) | ? % 10.95/2.28 [v1: $i] : (in_environment(v0, v1) = 0 & $i(v1) & ! [v2: $i] : ! [v3: $i] % 10.95/2.28 : ! [v4: $i] : ! [v5: int] : (v5 = 0 | ~ % 10.95/2.28 (growth_rate(efficient_producers, v2) = v3) | ~ % 10.95/2.28 (growth_rate(first_movers, v2) = v4) | ~ (greater(v3, v4) = v5) | ~ % 10.95/2.28 $i(v2) | ? [v6: any] : ? [v7: any] : (subpopulations(first_movers, % 10.95/2.28 efficient_producers, v0, v2) = v6 & greater_or_equal(v2, v1) = v7 & % 10.95/2.28 ( ~ (v7 = 0) | ~ (v6 = 0)))))) % 10.95/2.28 % 10.95/2.28 (mp_earliest_time_growth_rate_exceeds) % 10.95/2.29 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ( ~ % 10.95/2.29 (environment(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] % 10.95/2.29 : ? [v4: int] : ( ~ (v4 = 0) & in_environment(v0, v1) = 0 & % 10.95/2.29 growth_rate(efficient_producers, v1) = v2 & growth_rate(first_movers, v1) % 10.95/2.29 = v3 & greater(v2, v3) = v4 & $i(v3) & $i(v2) & $i(v1) & ! [v5: $i] : ! % 10.95/2.29 [v6: $i] : ! [v7: $i] : ! [v8: int] : (v8 = 0 | ~ % 10.95/2.29 (growth_rate(efficient_producers, v5) = v6) | ~ % 10.95/2.29 (growth_rate(first_movers, v5) = v7) | ~ (greater(v6, v7) = v8) | ~ % 10.95/2.29 $i(v5) | ? [v9: any] : ? [v10: any] : (subpopulations(first_movers, % 10.95/2.29 efficient_producers, v0, v5) = v9 & greater(v5, v1) = v10 & ( ~ (v10 % 10.95/2.29 = 0) | ~ (v9 = 0))))) | ! [v1: $i] : ( ~ (in_environment(v0, v1) % 10.95/2.29 = 0) | ~ $i(v1) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 10.95/2.29 int] : ( ~ (v5 = 0) & subpopulations(first_movers, efficient_producers, % 10.95/2.29 v0, v2) = 0 & greater_or_equal(v2, v1) = 0 & % 10.95/2.29 growth_rate(efficient_producers, v2) = v3 & growth_rate(first_movers, % 10.95/2.29 v2) = v4 & greater(v3, v4) = v5 & $i(v4) & $i(v3) & $i(v2)))) % 10.95/2.29 % 10.95/2.29 (prove_l12) % 11.56/2.30 $i(efficient_producers) & $i(first_movers) & ? [v0: $i] : (stable(v0) = 0 & % 11.56/2.30 environment(v0) = 0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 11.56/2.30 [v4: int] : (v4 = 0 | ~ (growth_rate(efficient_producers, v1) = v2) | ~ % 11.56/2.30 (growth_rate(first_movers, v1) = v3) | ~ (greater(v2, v3) = v4) | ~ % 11.56/2.30 $i(v1) | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: int] : ( ~ (v8 % 11.56/2.30 = 0) & subpopulations(first_movers, efficient_producers, v0, v5) = 0 & % 11.56/2.30 growth_rate(efficient_producers, v5) = v6 & growth_rate(first_movers, % 11.56/2.30 v5) = v7 & greater(v6, v7) = v8 & greater(v5, v1) = 0 & $i(v7) & % 11.56/2.30 $i(v6) & $i(v5)) | ? [v5: int] : ( ~ (v5 = 0) & in_environment(v0, v1) % 11.56/2.30 = v5))) % 11.56/2.30 % 11.56/2.30 (function-axioms) % 11.56/2.31 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 11.56/2.31 [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (subpopulations(v5, v4, % 11.56/2.31 v3, v2) = v1) | ~ (subpopulations(v5, v4, v3, v2) = v0)) & ! [v0: % 11.56/2.31 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 11.56/2.31 : (v1 = v0 | ~ (in_environment(v3, v2) = v1) | ~ (in_environment(v3, v2) = % 11.56/2.31 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 11.56/2.31 $i] : ! [v3: $i] : (v1 = v0 | ~ (greater_or_equal(v3, v2) = v1) | ~ % 11.56/2.31 (greater_or_equal(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 11.56/2.31 ! [v3: $i] : (v1 = v0 | ~ (growth_rate(v3, v2) = v1) | ~ (growth_rate(v3, % 11.56/2.31 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 11.56/2.31 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (greater(v3, v2) = v1) | ~ % 11.56/2.31 (greater(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 11.56/2.31 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (stable(v2) = v1) | ~ % 11.56/2.31 (stable(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 11.56/2.31 : ! [v2: $i] : (v1 = v0 | ~ (environment(v2) = v1) | ~ (environment(v2) = % 11.56/2.31 v0)) % 11.56/2.31 % 11.56/2.31 Those formulas are unsatisfiable: % 11.56/2.31 --------------------------------- % 11.56/2.31 % 11.56/2.31 Begin of proof % 11.56/2.31 | % 11.56/2.31 | ALPHA: (mp_earliest_time_growth_rate_exceeds) implies: % 11.56/2.31 | (1) ! [v0: $i] : ( ~ (environment(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ? % 11.56/2.31 | [v2: $i] : ? [v3: $i] : ? [v4: int] : ( ~ (v4 = 0) & % 11.56/2.31 | in_environment(v0, v1) = 0 & growth_rate(efficient_producers, v1) = % 11.56/2.31 | v2 & growth_rate(first_movers, v1) = v3 & greater(v2, v3) = v4 & % 11.56/2.31 | $i(v3) & $i(v2) & $i(v1) & ! [v5: $i] : ! [v6: $i] : ! [v7: $i] % 11.56/2.31 | : ! [v8: int] : (v8 = 0 | ~ (growth_rate(efficient_producers, v5) % 11.56/2.31 | = v6) | ~ (growth_rate(first_movers, v5) = v7) | ~ % 11.56/2.31 | (greater(v6, v7) = v8) | ~ $i(v5) | ? [v9: any] : ? [v10: any] % 11.56/2.31 | : (subpopulations(first_movers, efficient_producers, v0, v5) = v9 % 11.56/2.31 | & greater(v5, v1) = v10 & ( ~ (v10 = 0) | ~ (v9 = 0))))) | ! % 11.56/2.31 | [v1: $i] : ( ~ (in_environment(v0, v1) = 0) | ~ $i(v1) | ? [v2: $i] % 11.56/2.32 | : ? [v3: $i] : ? [v4: $i] : ? [v5: int] : ( ~ (v5 = 0) & % 11.56/2.32 | subpopulations(first_movers, efficient_producers, v0, v2) = 0 & % 11.56/2.32 | greater_or_equal(v2, v1) = 0 & growth_rate(efficient_producers, % 11.56/2.32 | v2) = v3 & growth_rate(first_movers, v2) = v4 & greater(v3, v4) % 11.56/2.32 | = v5 & $i(v4) & $i(v3) & $i(v2)))) % 11.56/2.32 | % 11.56/2.32 | ALPHA: (l1) implies: % 11.56/2.32 | (2) ! [v0: $i] : ( ~ (stable(v0) = 0) | ~ $i(v0) | ? [v1: int] : ( ~ (v1 % 11.56/2.32 | = 0) & environment(v0) = v1) | ? [v1: $i] : (in_environment(v0, % 11.56/2.32 | v1) = 0 & $i(v1) & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 11.56/2.32 | [v5: int] : (v5 = 0 | ~ (growth_rate(efficient_producers, v2) = % 11.56/2.32 | v3) | ~ (growth_rate(first_movers, v2) = v4) | ~ (greater(v3, % 11.56/2.32 | v4) = v5) | ~ $i(v2) | ? [v6: any] : ? [v7: any] : % 11.56/2.32 | (subpopulations(first_movers, efficient_producers, v0, v2) = v6 & % 11.56/2.32 | greater_or_equal(v2, v1) = v7 & ( ~ (v7 = 0) | ~ (v6 = 0)))))) % 11.56/2.32 | % 11.56/2.32 | ALPHA: (prove_l12) implies: % 11.56/2.32 | (3) ? [v0: $i] : (stable(v0) = 0 & environment(v0) = 0 & $i(v0) & ! [v1: % 11.56/2.32 | $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ % 11.56/2.32 | (growth_rate(efficient_producers, v1) = v2) | ~ % 11.56/2.32 | (growth_rate(first_movers, v1) = v3) | ~ (greater(v2, v3) = v4) | % 11.56/2.32 | ~ $i(v1) | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: int] : % 11.56/2.32 | ( ~ (v8 = 0) & subpopulations(first_movers, efficient_producers, % 11.56/2.32 | v0, v5) = 0 & growth_rate(efficient_producers, v5) = v6 & % 11.56/2.32 | growth_rate(first_movers, v5) = v7 & greater(v6, v7) = v8 & % 11.56/2.32 | greater(v5, v1) = 0 & $i(v7) & $i(v6) & $i(v5)) | ? [v5: int] : % 11.56/2.32 | ( ~ (v5 = 0) & in_environment(v0, v1) = v5))) % 11.56/2.32 | % 11.56/2.32 | ALPHA: (function-axioms) implies: % 11.56/2.32 | (4) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 11.56/2.32 | (v1 = v0 | ~ (environment(v2) = v1) | ~ (environment(v2) = v0)) % 11.56/2.33 | (5) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 11.56/2.33 | ! [v3: $i] : (v1 = v0 | ~ (greater(v3, v2) = v1) | ~ (greater(v3, % 11.56/2.33 | v2) = v0)) % 11.56/2.33 | (6) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 11.56/2.33 | ! [v3: $i] : (v1 = v0 | ~ (greater_or_equal(v3, v2) = v1) | ~ % 11.56/2.33 | (greater_or_equal(v3, v2) = v0)) % 11.56/2.33 | (7) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 11.56/2.33 | ! [v3: $i] : (v1 = v0 | ~ (in_environment(v3, v2) = v1) | ~ % 11.56/2.33 | (in_environment(v3, v2) = v0)) % 11.56/2.33 | (8) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 11.56/2.33 | ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 11.56/2.33 | (subpopulations(v5, v4, v3, v2) = v1) | ~ (subpopulations(v5, v4, % 11.56/2.33 | v3, v2) = v0)) % 11.56/2.33 | % 11.56/2.33 | DELTA: instantiating (3) with fresh symbol all_6_0 gives: % 11.56/2.33 | (9) stable(all_6_0) = 0 & environment(all_6_0) = 0 & $i(all_6_0) & ! [v0: % 11.56/2.33 | $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 11.56/2.33 | (growth_rate(efficient_producers, v0) = v1) | ~ % 11.56/2.33 | (growth_rate(first_movers, v0) = v2) | ~ (greater(v1, v2) = v3) | ~ % 11.56/2.33 | $i(v0) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: int] : ( ~ % 11.56/2.33 | (v7 = 0) & subpopulations(first_movers, efficient_producers, % 11.56/2.33 | all_6_0, v4) = 0 & growth_rate(efficient_producers, v4) = v5 & % 11.56/2.33 | growth_rate(first_movers, v4) = v6 & greater(v5, v6) = v7 & % 11.56/2.33 | greater(v4, v0) = 0 & $i(v6) & $i(v5) & $i(v4)) | ? [v4: int] : ( % 11.56/2.33 | ~ (v4 = 0) & in_environment(all_6_0, v0) = v4)) % 11.56/2.33 | % 11.56/2.33 | ALPHA: (9) implies: % 11.56/2.33 | (10) $i(all_6_0) % 11.56/2.33 | (11) environment(all_6_0) = 0 % 11.56/2.33 | (12) stable(all_6_0) = 0 % 11.56/2.34 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 11.56/2.34 | (growth_rate(efficient_producers, v0) = v1) | ~ % 11.56/2.34 | (growth_rate(first_movers, v0) = v2) | ~ (greater(v1, v2) = v3) | % 11.56/2.34 | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: int] : % 11.56/2.34 | ( ~ (v7 = 0) & subpopulations(first_movers, efficient_producers, % 11.56/2.34 | all_6_0, v4) = 0 & growth_rate(efficient_producers, v4) = v5 & % 11.56/2.34 | growth_rate(first_movers, v4) = v6 & greater(v5, v6) = v7 & % 11.56/2.34 | greater(v4, v0) = 0 & $i(v6) & $i(v5) & $i(v4)) | ? [v4: int] : ( % 11.56/2.34 | ~ (v4 = 0) & in_environment(all_6_0, v0) = v4)) % 11.56/2.34 | % 11.56/2.34 | GROUND_INST: instantiating (1) with all_6_0, simplifying with (10), (11) % 11.56/2.34 | gives: % 11.56/2.34 | (14) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ( ~ (v3 = 0) % 11.56/2.34 | & in_environment(all_6_0, v0) = 0 & growth_rate(efficient_producers, % 11.56/2.34 | v0) = v1 & growth_rate(first_movers, v0) = v2 & greater(v1, v2) = % 11.56/2.34 | v3 & $i(v2) & $i(v1) & $i(v0) & ! [v4: $i] : ! [v5: $i] : ! [v6: % 11.56/2.34 | $i] : ! [v7: int] : (v7 = 0 | ~ % 11.56/2.34 | (growth_rate(efficient_producers, v4) = v5) | ~ % 11.56/2.34 | (growth_rate(first_movers, v4) = v6) | ~ (greater(v5, v6) = v7) | % 11.56/2.34 | ~ $i(v4) | ? [v8: any] : ? [v9: any] : % 11.56/2.34 | (subpopulations(first_movers, efficient_producers, all_6_0, v4) = % 11.56/2.34 | v8 & greater(v4, v0) = v9 & ( ~ (v9 = 0) | ~ (v8 = 0))))) | ! % 11.56/2.34 | [v0: $i] : ( ~ (in_environment(all_6_0, v0) = 0) | ~ $i(v0) | ? [v1: % 11.56/2.34 | $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: int] : ( ~ (v4 = 0) & % 11.56/2.34 | subpopulations(first_movers, efficient_producers, all_6_0, v1) = 0 % 11.56/2.34 | & greater_or_equal(v1, v0) = 0 & growth_rate(efficient_producers, % 11.56/2.34 | v1) = v2 & growth_rate(first_movers, v1) = v3 & greater(v2, v3) % 11.56/2.34 | = v4 & $i(v3) & $i(v2) & $i(v1))) % 11.56/2.34 | % 11.56/2.34 | GROUND_INST: instantiating (2) with all_6_0, simplifying with (10), (12) % 11.56/2.34 | gives: % 11.56/2.34 | (15) ? [v0: int] : ( ~ (v0 = 0) & environment(all_6_0) = v0) | ? [v0: $i] % 11.56/2.34 | : (in_environment(all_6_0, v0) = 0 & $i(v0) & ! [v1: $i] : ! [v2: % 11.56/2.35 | $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ % 11.56/2.35 | (growth_rate(efficient_producers, v1) = v2) | ~ % 11.56/2.35 | (growth_rate(first_movers, v1) = v3) | ~ (greater(v2, v3) = v4) | % 11.56/2.35 | ~ $i(v1) | ? [v5: any] : ? [v6: any] : % 11.56/2.35 | (subpopulations(first_movers, efficient_producers, all_6_0, v1) = % 11.56/2.35 | v5 & greater_or_equal(v1, v0) = v6 & ( ~ (v6 = 0) | ~ (v5 = % 11.56/2.35 | 0))))) % 11.56/2.35 | % 11.56/2.35 | BETA: splitting (15) gives: % 11.56/2.35 | % 11.56/2.35 | Case 1: % 11.56/2.35 | | % 11.56/2.35 | | (16) ? [v0: int] : ( ~ (v0 = 0) & environment(all_6_0) = v0) % 11.56/2.35 | | % 11.56/2.35 | | DELTA: instantiating (16) with fresh symbol all_15_0 gives: % 11.56/2.35 | | (17) ~ (all_15_0 = 0) & environment(all_6_0) = all_15_0 % 11.56/2.35 | | % 11.56/2.35 | | ALPHA: (17) implies: % 11.56/2.35 | | (18) ~ (all_15_0 = 0) % 11.56/2.35 | | (19) environment(all_6_0) = all_15_0 % 11.56/2.35 | | % 11.56/2.35 | | GROUND_INST: instantiating (4) with 0, all_15_0, all_6_0, simplifying with % 11.56/2.35 | | (11), (19) gives: % 11.56/2.35 | | (20) all_15_0 = 0 % 11.56/2.35 | | % 11.56/2.35 | | REDUCE: (18), (20) imply: % 11.56/2.35 | | (21) $false % 11.56/2.35 | | % 11.56/2.35 | | CLOSE: (21) is inconsistent. % 11.56/2.35 | | % 11.56/2.35 | Case 2: % 11.56/2.35 | | % 11.56/2.35 | | (22) ? [v0: $i] : (in_environment(all_6_0, v0) = 0 & $i(v0) & ! [v1: % 11.56/2.35 | | $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | ~ % 11.56/2.35 | | (growth_rate(efficient_producers, v1) = v2) | ~ % 11.56/2.35 | | (growth_rate(first_movers, v1) = v3) | ~ (greater(v2, v3) = v4) % 11.56/2.35 | | | ~ $i(v1) | ? [v5: any] : ? [v6: any] : % 11.56/2.35 | | (subpopulations(first_movers, efficient_producers, all_6_0, v1) % 11.56/2.35 | | = v5 & greater_or_equal(v1, v0) = v6 & ( ~ (v6 = 0) | ~ (v5 = % 11.56/2.35 | | 0))))) % 11.56/2.35 | | % 11.56/2.35 | | DELTA: instantiating (22) with fresh symbol all_15_0 gives: % 11.56/2.35 | | (23) in_environment(all_6_0, all_15_0) = 0 & $i(all_15_0) & ! [v0: $i] : % 11.56/2.35 | | ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 11.56/2.35 | | (growth_rate(efficient_producers, v0) = v1) | ~ % 11.56/2.35 | | (growth_rate(first_movers, v0) = v2) | ~ (greater(v1, v2) = v3) | % 11.56/2.35 | | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 11.56/2.35 | | (subpopulations(first_movers, efficient_producers, all_6_0, v0) = % 11.56/2.35 | | v4 & greater_or_equal(v0, all_15_0) = v5 & ( ~ (v5 = 0) | ~ (v4 % 11.56/2.35 | | = 0)))) % 11.56/2.35 | | % 11.56/2.35 | | ALPHA: (23) implies: % 11.56/2.35 | | (24) $i(all_15_0) % 11.56/2.35 | | (25) in_environment(all_6_0, all_15_0) = 0 % 11.56/2.36 | | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | % 11.56/2.36 | | ~ (growth_rate(efficient_producers, v0) = v1) | ~ % 11.56/2.36 | | (growth_rate(first_movers, v0) = v2) | ~ (greater(v1, v2) = v3) | % 11.56/2.36 | | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 11.56/2.36 | | (subpopulations(first_movers, efficient_producers, all_6_0, v0) = % 11.56/2.36 | | v4 & greater_or_equal(v0, all_15_0) = v5 & ( ~ (v5 = 0) | ~ (v4 % 11.56/2.36 | | = 0)))) % 11.56/2.36 | | % 11.56/2.36 | | BETA: splitting (14) gives: % 11.56/2.36 | | % 11.56/2.36 | | Case 1: % 11.56/2.36 | | | % 11.56/2.36 | | | (27) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ( ~ (v3 = % 11.56/2.36 | | | 0) & in_environment(all_6_0, v0) = 0 & % 11.56/2.36 | | | growth_rate(efficient_producers, v0) = v1 & % 11.56/2.36 | | | growth_rate(first_movers, v0) = v2 & greater(v1, v2) = v3 & % 11.56/2.36 | | | $i(v2) & $i(v1) & $i(v0) & ! [v4: $i] : ! [v5: $i] : ! [v6: % 11.56/2.36 | | | $i] : ! [v7: int] : (v7 = 0 | ~ % 11.56/2.36 | | | (growth_rate(efficient_producers, v4) = v5) | ~ % 11.56/2.36 | | | (growth_rate(first_movers, v4) = v6) | ~ (greater(v5, v6) = % 11.56/2.36 | | | v7) | ~ $i(v4) | ? [v8: any] : ? [v9: any] : % 11.56/2.36 | | | (subpopulations(first_movers, efficient_producers, all_6_0, % 11.56/2.36 | | | v4) = v8 & greater(v4, v0) = v9 & ( ~ (v9 = 0) | ~ (v8 = % 11.56/2.36 | | | 0))))) % 11.56/2.36 | | | % 11.56/2.36 | | | DELTA: instantiating (27) with fresh symbols all_24_0, all_24_1, all_24_2, % 11.56/2.36 | | | all_24_3 gives: % 11.56/2.36 | | | (28) ~ (all_24_0 = 0) & in_environment(all_6_0, all_24_3) = 0 & % 11.56/2.36 | | | growth_rate(efficient_producers, all_24_3) = all_24_2 & % 11.56/2.36 | | | growth_rate(first_movers, all_24_3) = all_24_1 & greater(all_24_2, % 11.56/2.36 | | | all_24_1) = all_24_0 & $i(all_24_1) & $i(all_24_2) & % 11.56/2.36 | | | $i(all_24_3) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 11.56/2.36 | | | int] : (v3 = 0 | ~ (growth_rate(efficient_producers, v0) = v1) % 11.56/2.36 | | | | ~ (growth_rate(first_movers, v0) = v2) | ~ (greater(v1, v2) % 11.56/2.36 | | | = v3) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 11.56/2.36 | | | (subpopulations(first_movers, efficient_producers, all_6_0, v0) % 11.56/2.36 | | | = v4 & greater(v0, all_24_3) = v5 & ( ~ (v5 = 0) | ~ (v4 = % 11.56/2.36 | | | 0)))) % 11.56/2.36 | | | % 11.56/2.36 | | | ALPHA: (28) implies: % 11.56/2.36 | | | (29) ~ (all_24_0 = 0) % 11.56/2.36 | | | (30) $i(all_24_3) % 11.56/2.36 | | | (31) greater(all_24_2, all_24_1) = all_24_0 % 11.56/2.36 | | | (32) growth_rate(first_movers, all_24_3) = all_24_1 % 11.56/2.36 | | | (33) growth_rate(efficient_producers, all_24_3) = all_24_2 % 11.56/2.36 | | | (34) in_environment(all_6_0, all_24_3) = 0 % 11.56/2.36 | | | (35) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | % 11.56/2.36 | | | ~ (growth_rate(efficient_producers, v0) = v1) | ~ % 11.56/2.36 | | | (growth_rate(first_movers, v0) = v2) | ~ (greater(v1, v2) = v3) % 11.56/2.37 | | | | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 11.56/2.37 | | | (subpopulations(first_movers, efficient_producers, all_6_0, v0) % 11.56/2.37 | | | = v4 & greater(v0, all_24_3) = v5 & ( ~ (v5 = 0) | ~ (v4 = % 11.56/2.37 | | | 0)))) % 11.56/2.37 | | | % 11.56/2.37 | | | GROUND_INST: instantiating (13) with all_24_3, all_24_2, all_24_1, % 11.56/2.37 | | | all_24_0, simplifying with (30), (31), (32), (33) gives: % 11.56/2.37 | | | (36) all_24_0 = 0 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 11.56/2.37 | | | int] : ( ~ (v3 = 0) & subpopulations(first_movers, % 11.56/2.37 | | | efficient_producers, all_6_0, v0) = 0 & % 11.56/2.37 | | | growth_rate(efficient_producers, v0) = v1 & % 11.56/2.37 | | | growth_rate(first_movers, v0) = v2 & greater(v1, v2) = v3 & % 11.56/2.37 | | | greater(v0, all_24_3) = 0 & $i(v2) & $i(v1) & $i(v0)) | ? [v0: % 11.56/2.37 | | | int] : ( ~ (v0 = 0) & in_environment(all_6_0, all_24_3) = v0) % 11.56/2.37 | | | % 11.56/2.37 | | | BETA: splitting (36) gives: % 11.56/2.37 | | | % 11.56/2.37 | | | Case 1: % 11.56/2.37 | | | | % 11.56/2.37 | | | | (37) all_24_0 = 0 % 11.56/2.37 | | | | % 11.56/2.37 | | | | REDUCE: (29), (37) imply: % 11.56/2.37 | | | | (38) $false % 11.56/2.37 | | | | % 11.56/2.37 | | | | CLOSE: (38) is inconsistent. % 11.56/2.37 | | | | % 11.56/2.37 | | | Case 2: % 11.56/2.37 | | | | % 11.56/2.37 | | | | (39) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ( ~ (v3 % 11.56/2.37 | | | | = 0) & subpopulations(first_movers, efficient_producers, % 11.56/2.37 | | | | all_6_0, v0) = 0 & growth_rate(efficient_producers, v0) = v1 % 11.56/2.37 | | | | & growth_rate(first_movers, v0) = v2 & greater(v1, v2) = v3 & % 11.56/2.37 | | | | greater(v0, all_24_3) = 0 & $i(v2) & $i(v1) & $i(v0)) | ? % 11.56/2.37 | | | | [v0: int] : ( ~ (v0 = 0) & in_environment(all_6_0, all_24_3) = % 11.56/2.37 | | | | v0) % 11.56/2.37 | | | | % 11.56/2.37 | | | | BETA: splitting (39) gives: % 11.56/2.37 | | | | % 11.56/2.37 | | | | Case 1: % 11.56/2.37 | | | | | % 11.56/2.37 | | | | | (40) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ( ~ % 11.56/2.37 | | | | | (v3 = 0) & subpopulations(first_movers, efficient_producers, % 11.56/2.37 | | | | | all_6_0, v0) = 0 & growth_rate(efficient_producers, v0) = % 11.56/2.37 | | | | | v1 & growth_rate(first_movers, v0) = v2 & greater(v1, v2) = % 11.56/2.37 | | | | | v3 & greater(v0, all_24_3) = 0 & $i(v2) & $i(v1) & $i(v0)) % 11.56/2.37 | | | | | % 11.56/2.37 | | | | | DELTA: instantiating (40) with fresh symbols all_48_0, all_48_1, % 11.56/2.37 | | | | | all_48_2, all_48_3 gives: % 11.56/2.37 | | | | | (41) ~ (all_48_0 = 0) & subpopulations(first_movers, % 11.56/2.37 | | | | | efficient_producers, all_6_0, all_48_3) = 0 & % 11.56/2.37 | | | | | growth_rate(efficient_producers, all_48_3) = all_48_2 & % 11.56/2.37 | | | | | growth_rate(first_movers, all_48_3) = all_48_1 & % 11.56/2.37 | | | | | greater(all_48_2, all_48_1) = all_48_0 & greater(all_48_3, % 11.56/2.37 | | | | | all_24_3) = 0 & $i(all_48_1) & $i(all_48_2) & $i(all_48_3) % 11.56/2.37 | | | | | % 11.56/2.37 | | | | | ALPHA: (41) implies: % 11.56/2.37 | | | | | (42) ~ (all_48_0 = 0) % 11.56/2.37 | | | | | (43) $i(all_48_3) % 11.56/2.37 | | | | | (44) greater(all_48_3, all_24_3) = 0 % 11.56/2.37 | | | | | (45) greater(all_48_2, all_48_1) = all_48_0 % 11.56/2.37 | | | | | (46) growth_rate(first_movers, all_48_3) = all_48_1 % 11.56/2.37 | | | | | (47) growth_rate(efficient_producers, all_48_3) = all_48_2 % 11.56/2.37 | | | | | (48) subpopulations(first_movers, efficient_producers, all_6_0, % 11.56/2.37 | | | | | all_48_3) = 0 % 11.56/2.37 | | | | | % 11.56/2.38 | | | | | GROUND_INST: instantiating (26) with all_48_3, all_48_2, all_48_1, % 11.56/2.38 | | | | | all_48_0, simplifying with (43), (45), (46), (47) gives: % 11.56/2.38 | | | | | (49) all_48_0 = 0 | ? [v0: any] : ? [v1: any] : % 11.56/2.38 | | | | | (subpopulations(first_movers, efficient_producers, all_6_0, % 11.56/2.38 | | | | | all_48_3) = v0 & greater_or_equal(all_48_3, all_15_0) = v1 % 11.56/2.38 | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0))) % 11.56/2.38 | | | | | % 11.56/2.38 | | | | | GROUND_INST: instantiating (35) with all_48_3, all_48_2, all_48_1, % 11.56/2.38 | | | | | all_48_0, simplifying with (43), (45), (46), (47) gives: % 11.56/2.38 | | | | | (50) all_48_0 = 0 | ? [v0: any] : ? [v1: any] : % 11.56/2.38 | | | | | (subpopulations(first_movers, efficient_producers, all_6_0, % 11.56/2.38 | | | | | all_48_3) = v0 & greater(all_48_3, all_24_3) = v1 & ( ~ % 11.56/2.38 | | | | | (v1 = 0) | ~ (v0 = 0))) % 11.56/2.38 | | | | | % 11.56/2.38 | | | | | BETA: splitting (50) gives: % 11.56/2.38 | | | | | % 11.56/2.38 | | | | | Case 1: % 11.56/2.38 | | | | | | % 11.56/2.38 | | | | | | (51) all_48_0 = 0 % 11.56/2.38 | | | | | | % 11.56/2.38 | | | | | | REDUCE: (42), (51) imply: % 11.56/2.38 | | | | | | (52) $false % 11.56/2.38 | | | | | | % 11.56/2.38 | | | | | | CLOSE: (52) is inconsistent. % 11.56/2.38 | | | | | | % 11.56/2.38 | | | | | Case 2: % 11.56/2.38 | | | | | | % 11.56/2.38 | | | | | | (53) ? [v0: any] : ? [v1: any] : (subpopulations(first_movers, % 11.56/2.38 | | | | | | efficient_producers, all_6_0, all_48_3) = v0 & % 11.56/2.38 | | | | | | greater(all_48_3, all_24_3) = v1 & ( ~ (v1 = 0) | ~ (v0 = % 11.56/2.38 | | | | | | 0))) % 11.56/2.38 | | | | | | % 11.56/2.38 | | | | | | DELTA: instantiating (53) with fresh symbols all_65_0, all_65_1 % 11.56/2.38 | | | | | | gives: % 11.56/2.38 | | | | | | (54) subpopulations(first_movers, efficient_producers, all_6_0, % 11.56/2.38 | | | | | | all_48_3) = all_65_1 & greater(all_48_3, all_24_3) = % 11.56/2.38 | | | | | | all_65_0 & ( ~ (all_65_0 = 0) | ~ (all_65_1 = 0)) % 11.56/2.38 | | | | | | % 11.56/2.38 | | | | | | ALPHA: (54) implies: % 11.56/2.38 | | | | | | (55) greater(all_48_3, all_24_3) = all_65_0 % 11.56/2.38 | | | | | | (56) subpopulations(first_movers, efficient_producers, all_6_0, % 11.56/2.38 | | | | | | all_48_3) = all_65_1 % 11.56/2.38 | | | | | | (57) ~ (all_65_0 = 0) | ~ (all_65_1 = 0) % 11.56/2.38 | | | | | | % 11.56/2.38 | | | | | | BETA: splitting (49) gives: % 11.56/2.38 | | | | | | % 11.56/2.38 | | | | | | Case 1: % 11.56/2.38 | | | | | | | % 11.56/2.38 | | | | | | | (58) all_48_0 = 0 % 11.56/2.38 | | | | | | | % 11.56/2.38 | | | | | | | REDUCE: (42), (58) imply: % 11.56/2.38 | | | | | | | (59) $false % 11.56/2.38 | | | | | | | % 11.56/2.38 | | | | | | | CLOSE: (59) is inconsistent. % 11.56/2.38 | | | | | | | % 11.56/2.38 | | | | | | Case 2: % 11.56/2.38 | | | | | | | % 11.56/2.38 | | | | | | | (60) ? [v0: any] : ? [v1: any] : % 11.56/2.38 | | | | | | | (subpopulations(first_movers, efficient_producers, % 11.56/2.38 | | | | | | | all_6_0, all_48_3) = v0 & greater_or_equal(all_48_3, % 11.56/2.38 | | | | | | | all_15_0) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 11.56/2.38 | | | | | | | % 11.56/2.38 | | | | | | | DELTA: instantiating (60) with fresh symbols all_70_0, all_70_1 % 11.56/2.38 | | | | | | | gives: % 11.56/2.38 | | | | | | | (61) subpopulations(first_movers, efficient_producers, all_6_0, % 11.56/2.38 | | | | | | | all_48_3) = all_70_1 & greater_or_equal(all_48_3, % 11.56/2.38 | | | | | | | all_15_0) = all_70_0 & ( ~ (all_70_0 = 0) | ~ (all_70_1 % 11.56/2.38 | | | | | | | = 0)) % 11.56/2.38 | | | | | | | % 11.56/2.38 | | | | | | | ALPHA: (61) implies: % 11.56/2.38 | | | | | | | (62) subpopulations(first_movers, efficient_producers, all_6_0, % 11.56/2.38 | | | | | | | all_48_3) = all_70_1 % 11.56/2.38 | | | | | | | % 11.56/2.38 | | | | | | | GROUND_INST: instantiating (5) with 0, all_65_0, all_24_3, % 11.56/2.38 | | | | | | | all_48_3, simplifying with (44), (55) gives: % 11.56/2.38 | | | | | | | (63) all_65_0 = 0 % 11.56/2.38 | | | | | | | % 11.56/2.39 | | | | | | | GROUND_INST: instantiating (8) with 0, all_70_1, all_48_3, % 11.56/2.39 | | | | | | | all_6_0, efficient_producers, first_movers, % 11.56/2.39 | | | | | | | simplifying with (48), (62) gives: % 11.56/2.39 | | | | | | | (64) all_70_1 = 0 % 11.56/2.39 | | | | | | | % 11.56/2.39 | | | | | | | GROUND_INST: instantiating (8) with all_65_1, all_70_1, all_48_3, % 11.56/2.39 | | | | | | | all_6_0, efficient_producers, first_movers, % 11.56/2.39 | | | | | | | simplifying with (56), (62) gives: % 11.56/2.39 | | | | | | | (65) all_70_1 = all_65_1 % 11.56/2.39 | | | | | | | % 11.56/2.39 | | | | | | | COMBINE_EQS: (64), (65) imply: % 11.56/2.39 | | | | | | | (66) all_65_1 = 0 % 11.56/2.39 | | | | | | | % 11.56/2.39 | | | | | | | BETA: splitting (57) gives: % 11.56/2.39 | | | | | | | % 11.56/2.39 | | | | | | | Case 1: % 11.56/2.39 | | | | | | | | % 11.56/2.39 | | | | | | | | (67) ~ (all_65_0 = 0) % 11.56/2.39 | | | | | | | | % 11.56/2.39 | | | | | | | | REDUCE: (63), (67) imply: % 11.56/2.39 | | | | | | | | (68) $false % 11.56/2.39 | | | | | | | | % 11.56/2.39 | | | | | | | | CLOSE: (68) is inconsistent. % 11.56/2.39 | | | | | | | | % 11.56/2.39 | | | | | | | Case 2: % 11.56/2.39 | | | | | | | | % 11.56/2.39 | | | | | | | | (69) ~ (all_65_1 = 0) % 11.56/2.39 | | | | | | | | % 11.56/2.39 | | | | | | | | REDUCE: (66), (69) imply: % 11.56/2.39 | | | | | | | | (70) $false % 11.56/2.39 | | | | | | | | % 11.56/2.39 | | | | | | | | CLOSE: (70) is inconsistent. % 11.56/2.39 | | | | | | | | % 11.56/2.39 | | | | | | | End of split % 11.56/2.39 | | | | | | | % 11.56/2.39 | | | | | | End of split % 11.56/2.39 | | | | | | % 11.56/2.39 | | | | | End of split % 11.56/2.39 | | | | | % 11.56/2.39 | | | | Case 2: % 11.56/2.39 | | | | | % 11.56/2.39 | | | | | (71) ? [v0: int] : ( ~ (v0 = 0) & in_environment(all_6_0, % 11.56/2.39 | | | | | all_24_3) = v0) % 11.56/2.39 | | | | | % 11.56/2.39 | | | | | DELTA: instantiating (71) with fresh symbol all_48_0 gives: % 11.56/2.39 | | | | | (72) ~ (all_48_0 = 0) & in_environment(all_6_0, all_24_3) = % 11.56/2.39 | | | | | all_48_0 % 11.56/2.39 | | | | | % 11.56/2.39 | | | | | ALPHA: (72) implies: % 11.56/2.39 | | | | | (73) ~ (all_48_0 = 0) % 11.56/2.39 | | | | | (74) in_environment(all_6_0, all_24_3) = all_48_0 % 11.56/2.39 | | | | | % 11.56/2.39 | | | | | GROUND_INST: instantiating (7) with 0, all_48_0, all_24_3, all_6_0, % 11.56/2.39 | | | | | simplifying with (34), (74) gives: % 11.56/2.39 | | | | | (75) all_48_0 = 0 % 11.56/2.39 | | | | | % 11.56/2.39 | | | | | REDUCE: (73), (75) imply: % 11.56/2.39 | | | | | (76) $false % 11.56/2.39 | | | | | % 11.56/2.39 | | | | | CLOSE: (76) is inconsistent. % 11.56/2.39 | | | | | % 11.56/2.39 | | | | End of split % 11.56/2.39 | | | | % 11.56/2.39 | | | End of split % 11.56/2.39 | | | % 11.56/2.39 | | Case 2: % 11.56/2.39 | | | % 11.56/2.39 | | | (77) ! [v0: $i] : ( ~ (in_environment(all_6_0, v0) = 0) | ~ $i(v0) | % 11.56/2.39 | | | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: int] : ( ~ (v4 % 11.56/2.39 | | | = 0) & subpopulations(first_movers, efficient_producers, % 11.56/2.39 | | | all_6_0, v1) = 0 & greater_or_equal(v1, v0) = 0 & % 11.56/2.39 | | | growth_rate(efficient_producers, v1) = v2 & % 11.56/2.39 | | | growth_rate(first_movers, v1) = v3 & greater(v2, v3) = v4 & % 11.56/2.39 | | | $i(v3) & $i(v2) & $i(v1))) % 11.56/2.39 | | | % 11.56/2.39 | | | GROUND_INST: instantiating (77) with all_15_0, simplifying with (24), (25) % 11.56/2.39 | | | gives: % 11.56/2.40 | | | (78) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: int] : ( ~ (v3 = % 11.56/2.40 | | | 0) & subpopulations(first_movers, efficient_producers, % 11.56/2.40 | | | all_6_0, v0) = 0 & greater_or_equal(v0, all_15_0) = 0 & % 11.56/2.40 | | | growth_rate(efficient_producers, v0) = v1 & % 11.56/2.40 | | | growth_rate(first_movers, v0) = v2 & greater(v1, v2) = v3 & % 11.56/2.40 | | | $i(v2) & $i(v1) & $i(v0)) % 11.56/2.40 | | | % 11.56/2.40 | | | DELTA: instantiating (78) with fresh symbols all_25_0, all_25_1, all_25_2, % 11.56/2.40 | | | all_25_3 gives: % 11.56/2.40 | | | (79) ~ (all_25_0 = 0) & subpopulations(first_movers, % 11.56/2.40 | | | efficient_producers, all_6_0, all_25_3) = 0 & % 11.56/2.40 | | | greater_or_equal(all_25_3, all_15_0) = 0 & % 11.56/2.40 | | | growth_rate(efficient_producers, all_25_3) = all_25_2 & % 11.56/2.40 | | | growth_rate(first_movers, all_25_3) = all_25_1 & greater(all_25_2, % 11.56/2.40 | | | all_25_1) = all_25_0 & $i(all_25_1) & $i(all_25_2) & % 11.56/2.40 | | | $i(all_25_3) % 11.56/2.40 | | | % 11.56/2.40 | | | ALPHA: (79) implies: % 11.56/2.40 | | | (80) ~ (all_25_0 = 0) % 11.56/2.40 | | | (81) $i(all_25_3) % 11.56/2.40 | | | (82) greater(all_25_2, all_25_1) = all_25_0 % 11.56/2.40 | | | (83) growth_rate(first_movers, all_25_3) = all_25_1 % 11.56/2.40 | | | (84) growth_rate(efficient_producers, all_25_3) = all_25_2 % 11.56/2.40 | | | (85) greater_or_equal(all_25_3, all_15_0) = 0 % 11.56/2.40 | | | (86) subpopulations(first_movers, efficient_producers, all_6_0, % 11.56/2.40 | | | all_25_3) = 0 % 11.56/2.40 | | | % 12.07/2.40 | | | GROUND_INST: instantiating (26) with all_25_3, all_25_2, all_25_1, % 12.07/2.40 | | | all_25_0, simplifying with (81), (82), (83), (84) gives: % 12.07/2.40 | | | (87) all_25_0 = 0 | ? [v0: any] : ? [v1: any] : % 12.07/2.40 | | | (subpopulations(first_movers, efficient_producers, all_6_0, % 12.07/2.40 | | | all_25_3) = v0 & greater_or_equal(all_25_3, all_15_0) = v1 & ( % 12.07/2.40 | | | ~ (v1 = 0) | ~ (v0 = 0))) % 12.07/2.40 | | | % 12.07/2.40 | | | BETA: splitting (87) gives: % 12.07/2.40 | | | % 12.07/2.40 | | | Case 1: % 12.07/2.40 | | | | % 12.07/2.40 | | | | (88) all_25_0 = 0 % 12.07/2.40 | | | | % 12.07/2.40 | | | | REDUCE: (80), (88) imply: % 12.07/2.40 | | | | (89) $false % 12.07/2.40 | | | | % 12.07/2.40 | | | | CLOSE: (89) is inconsistent. % 12.07/2.40 | | | | % 12.07/2.40 | | | Case 2: % 12.07/2.40 | | | | % 12.07/2.40 | | | | (90) ? [v0: any] : ? [v1: any] : (subpopulations(first_movers, % 12.07/2.40 | | | | efficient_producers, all_6_0, all_25_3) = v0 & % 12.07/2.40 | | | | greater_or_equal(all_25_3, all_15_0) = v1 & ( ~ (v1 = 0) | ~ % 12.07/2.40 | | | | (v0 = 0))) % 12.07/2.40 | | | | % 12.07/2.40 | | | | DELTA: instantiating (90) with fresh symbols all_34_0, all_34_1 gives: % 12.07/2.40 | | | | (91) subpopulations(first_movers, efficient_producers, all_6_0, % 12.07/2.40 | | | | all_25_3) = all_34_1 & greater_or_equal(all_25_3, all_15_0) = % 12.07/2.40 | | | | all_34_0 & ( ~ (all_34_0 = 0) | ~ (all_34_1 = 0)) % 12.07/2.40 | | | | % 12.07/2.40 | | | | ALPHA: (91) implies: % 12.07/2.40 | | | | (92) greater_or_equal(all_25_3, all_15_0) = all_34_0 % 12.07/2.40 | | | | (93) subpopulations(first_movers, efficient_producers, all_6_0, % 12.07/2.40 | | | | all_25_3) = all_34_1 % 12.07/2.40 | | | | (94) ~ (all_34_0 = 0) | ~ (all_34_1 = 0) % 12.07/2.40 | | | | % 12.07/2.40 | | | | GROUND_INST: instantiating (6) with 0, all_34_0, all_15_0, all_25_3, % 12.07/2.40 | | | | simplifying with (85), (92) gives: % 12.07/2.40 | | | | (95) all_34_0 = 0 % 12.07/2.40 | | | | % 12.07/2.40 | | | | GROUND_INST: instantiating (8) with 0, all_34_1, all_25_3, all_6_0, % 12.07/2.40 | | | | efficient_producers, first_movers, simplifying with (86), % 12.07/2.40 | | | | (93) gives: % 12.07/2.40 | | | | (96) all_34_1 = 0 % 12.07/2.40 | | | | % 12.07/2.40 | | | | BETA: splitting (94) gives: % 12.07/2.40 | | | | % 12.07/2.40 | | | | Case 1: % 12.07/2.40 | | | | | % 12.07/2.41 | | | | | (97) ~ (all_34_0 = 0) % 12.07/2.41 | | | | | % 12.07/2.41 | | | | | REDUCE: (95), (97) imply: % 12.07/2.41 | | | | | (98) $false % 12.07/2.41 | | | | | % 12.07/2.41 | | | | | CLOSE: (98) is inconsistent. % 12.07/2.41 | | | | | % 12.07/2.41 | | | | Case 2: % 12.07/2.41 | | | | | % 12.07/2.41 | | | | | (99) ~ (all_34_1 = 0) % 12.07/2.41 | | | | | % 12.07/2.41 | | | | | REDUCE: (96), (99) imply: % 12.07/2.41 | | | | | (100) $false % 12.07/2.41 | | | | | % 12.07/2.41 | | | | | CLOSE: (100) is inconsistent. % 12.07/2.41 | | | | | % 12.07/2.41 | | | | End of split % 12.07/2.41 | | | | % 12.07/2.41 | | | End of split % 12.07/2.41 | | | % 12.07/2.41 | | End of split % 12.07/2.41 | | % 12.07/2.41 | End of split % 12.07/2.41 | % 12.07/2.41 End of proof % 12.07/2.41 % SZS output end Proof for theBenchmark % 12.07/2.41 % 12.07/2.41 1687ms %------------------------------------------------------------------------------