%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : MGT020+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 : n004.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:20 AM UTC 2026 % Result : Theorem 15.72s 2.82s % Output : Proof 22.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT020+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.36 % Computer : n004.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Mon Sep 7 12:00:45 UTC 2026 % 0.10/0.37 % CPUTime : % 0.14/0.38 OpenJDK 64-Bit Server VM warning: Options -Xverify:none and -noverify were deprecated in JDK 13 and will likely be removed in a future release. % 0.69/0.73 ________ _____ % 0.69/0.73 ___ __ \_________(_)________________________________ % 0.69/0.73 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.69/0.73 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.69/0.73 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.69/0.73 % 0.69/0.73 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.69/0.73 (2023-06-19) % 0.69/0.73 % 0.69/0.73 (c) Philipp Rümmer, 2009-2023 % 0.69/0.73 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.69/0.73 Amanda Stjerna. % 0.69/0.73 Free software under BSD-3-Clause. % 0.69/0.73 % 0.69/0.73 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.69/0.73 % 0.69/0.73 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.69/0.75 Running up to 7 provers in parallel. % 0.69/0.76 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.69/0.76 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.69/0.76 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.69/0.76 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.69/0.76 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.69/0.76 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.69/0.76 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.20/1.23 Prover 1: Preprocessing ... % 3.20/1.24 Prover 4: Preprocessing ... % 3.95/1.32 Prover 0: Preprocessing ... % 3.95/1.32 Prover 5: Preprocessing ... % 3.95/1.32 Prover 3: Preprocessing ... % 3.95/1.32 Prover 6: Preprocessing ... % 3.95/1.32 Prover 2: Preprocessing ... % 7.09/1.80 Prover 3: Constructing countermodel ... % 7.87/1.81 Prover 6: Constructing countermodel ... % 7.87/1.84 Prover 5: Proving ... % 7.87/1.84 Prover 1: Constructing countermodel ... % 8.66/1.92 Prover 2: Proving ... % 9.69/2.04 Prover 4: Constructing countermodel ... % 10.49/2.14 Prover 0: Proving ... % 10.99/2.20 Prover 3: gave up % 10.99/2.21 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 10.99/2.25 Prover 7: Preprocessing ... % 10.99/2.30 Prover 6: gave up % 11.78/2.30 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 11.78/2.33 Prover 8: Preprocessing ... % 12.57/2.40 Prover 8: Warning: ignoring some quantifiers % 12.57/2.40 Prover 1: gave up % 12.57/2.41 Prover 8: Constructing countermodel ... % 12.57/2.41 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 12.57/2.46 Prover 7: Constructing countermodel ... % 12.57/2.47 Prover 9: Preprocessing ... % 13.34/2.59 Prover 8: gave up % 13.34/2.59 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 14.15/2.62 Prover 7: gave up % 14.15/2.63 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 14.15/2.69 Prover 10: Preprocessing ... % 14.92/2.70 Prover 11: Preprocessing ... % 14.92/2.78 Prover 10: Constructing countermodel ... % 15.72/2.82 Prover 0: proved (2060ms) % 15.72/2.82 % 15.72/2.82 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.72/2.82 % 15.72/2.83 Prover 5: stopped % 15.72/2.83 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 15.72/2.83 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 15.72/2.84 Prover 2: stopped % 15.72/2.84 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 15.72/2.85 Prover 10: gave up % 15.72/2.87 Prover 16: Preprocessing ... % 16.53/2.91 Prover 13: Preprocessing ... % 16.53/2.92 Prover 16: Warning: ignoring some quantifiers % 16.53/2.92 Prover 19: Preprocessing ... % 16.53/2.92 Prover 16: Constructing countermodel ... % 16.53/2.97 Prover 9: Constructing countermodel ... % 16.53/2.98 Prover 9: stopped % 16.53/3.03 Prover 13: Warning: ignoring some quantifiers % 16.53/3.03 Prover 13: Constructing countermodel ... % 17.54/3.09 Prover 19: Warning: ignoring some quantifiers % 17.54/3.11 Prover 19: Constructing countermodel ... % 17.54/3.12 Prover 11: Constructing countermodel ... % 18.79/3.29 Prover 16: gave up % 21.17/3.56 Prover 13: Found proof (size 92) % 21.17/3.56 Prover 13: proved (731ms) % 21.17/3.56 Prover 19: stopped % 21.17/3.56 Prover 11: stopped % 21.17/3.56 Prover 4: stopped % 21.17/3.56 % 21.17/3.56 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 21.17/3.56 % 21.17/3.59 % SZS output start Proof for theBenchmark % 21.17/3.60 Assumptions after simplification: % 21.17/3.60 --------------------------------- % 21.17/3.60 % 21.17/3.60 (a8) % 21.84/3.65 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ! [v1: $i] : ( ~ % 21.84/3.65 (initial_FM_EP(v0) = v1) | ~ $i(v0) | ~ environment(v0) | ? [v2: $i] : ? % 21.84/3.65 [v3: $i] : (disbanding_rate(efficient_producers, v1) = v3 & % 21.84/3.65 disbanding_rate(first_movers, v1) = v2 & $i(v3) & $i(v2) & greater(v2, % 21.84/3.65 v3))) & ! [v0: $i] : ( ~ $i(v0) | ~ environment(v0) | ? [v1: $i] : ? % 21.84/3.65 [v2: $i] : ? [v3: $i] : (initial_FM_EP(v0) = v1 & % 21.84/3.65 disbanding_rate(efficient_producers, v1) = v3 & % 21.84/3.65 disbanding_rate(first_movers, v1) = v2 & $i(v3) & $i(v2) & $i(v1) & % 21.84/3.65 greater(v2, v3))) % 21.84/3.65 % 21.84/3.66 (l3) % 21.84/3.66 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ! [v1: $i] : ! % 21.84/3.66 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 21.84/3.66 (disbanding_rate(efficient_producers, v1) = v3) | ~ % 21.84/3.66 (disbanding_rate(first_movers, v1) = v2) | ~ (difference(v2, v3) = v4) | ~ % 21.84/3.66 $i(v1) | ~ $i(v0) | ~ decreases(v4) | ~ subpopulations(first_movers, % 21.84/3.67 efficient_producers, v0, v1) | ~ environment(v0)) & ! [v0: $i] : ! [v1: % 21.84/3.67 $i] : ( ~ $i(v1) | ~ $i(v0) | ~ subpopulations(first_movers, % 21.84/3.67 efficient_producers, v0, v1) | ~ environment(v0) | ? [v2: $i] : ? [v3: % 21.84/3.67 $i] : ? [v4: $i] : (disbanding_rate(efficient_producers, v1) = v3 & % 21.84/3.67 disbanding_rate(first_movers, v1) = v2 & difference(v2, v3) = v4 & $i(v4) % 21.84/3.67 & $i(v3) & $i(v2) & ~ decreases(v4))) % 21.84/3.67 % 21.84/3.67 (mp_earliest_time_point) % 21.84/3.68 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ! [v1: $i] : ! % 21.84/3.68 [v2: $i] : ( ~ (initial_FM_EP(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 21.84/3.68 subpopulations(first_movers, efficient_producers, v0, v1) | ~ % 21.84/3.68 environment(v0) | greater_or_equal(v1, v2)) & ! [v0: $i] : ! [v1: $i] : ( % 21.84/3.68 ~ (initial_FM_EP(v0) = v1) | ~ $i(v0) | ~ in_environment(v0, v1) | ~ % 21.84/3.68 environment(v0) | subpopulations(first_movers, efficient_producers, v0, v1)) % 21.84/3.68 & ? [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ environment(v1) | ? % 21.84/3.68 [v2: $i] : (initial_FM_EP(v1) = v2 & $i(v2) & ( ~ in_environment(v1, v2) | % 21.84/3.68 subpopulations(first_movers, efficient_producers, v1, v2)) & ( ~ % 21.84/3.68 subpopulations(first_movers, efficient_producers, v1, v0) | % 21.84/3.68 greater_or_equal(v0, v2)))) % 21.84/3.68 % 21.84/3.68 (mp_greater_or_equal) % 21.84/3.68 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ % 21.84/3.68 greater_or_equal(v0, v1) | greater(v0, v1)) % 21.84/3.68 % 21.84/3.68 (mp_initial_time) % 21.84/3.68 ! [v0: $i] : ! [v1: $i] : ( ~ (start_time(v0) = v1) | ~ $i(v0) | ~ % 21.84/3.68 environment(v0) | ? [v2: $i] : (initial_FM_EP(v0) = v2 & $i(v2) & % 21.84/3.68 greater_or_equal(v2, v1))) & ! [v0: $i] : ( ~ $i(v0) | ~ environment(v0) % 21.84/3.68 | ? [v1: $i] : ? [v2: $i] : (start_time(v0) = v2 & initial_FM_EP(v0) = v1 % 21.84/3.68 & $i(v2) & $i(v1) & greater_or_equal(v1, v2))) % 21.84/3.68 % 21.84/3.68 (mp_positive_function_difference) % 21.84/3.70 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ! [v1: $i] : ! % 21.84/3.70 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] % 21.84/3.70 : ! [v8: $i] : ( ~ (disbanding_rate(efficient_producers, v1) = v6) | ~ % 21.84/3.70 (disbanding_rate(first_movers, v3) = v8) | ~ (disbanding_rate(first_movers, % 21.84/3.70 v2) = v4) | ~ (disbanding_rate(first_movers, v1) = v5) | ~ % 21.84/3.70 (difference(v5, v6) = v7) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 21.84/3.70 ~ greater_or_equal(v3, v1) | ~ greater_or_equal(v1, v2) | ~ % 21.84/3.70 subpopulations(first_movers, efficient_producers, v0, v3) | ~ % 21.84/3.70 environment(v0) | decreases(v7) | ? [v9: $i] : ? [v10: $i] : % 21.84/3.70 (disbanding_rate(efficient_producers, v3) = v10 & % 21.84/3.70 disbanding_rate(efficient_producers, v2) = v9 & $i(v10) & $i(v9) & ( ~ % 21.84/3.70 greater(v4, v9) | greater(v8, v10)))) & ! [v0: $i] : ! [v1: $i] : ! % 21.84/3.70 [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 21.84/3.70 greater_or_equal(v3, v1) | ~ greater_or_equal(v1, v2) | ~ % 21.84/3.70 subpopulations(first_movers, efficient_producers, v0, v3) | ~ % 22.33/3.70 environment(v0) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? % 22.33/3.70 [v8: $i] : ? [v9: $i] : ? [v10: $i] : % 22.33/3.70 (disbanding_rate(efficient_producers, v3) = v10 & % 22.33/3.70 disbanding_rate(efficient_producers, v2) = v5 & % 22.33/3.70 disbanding_rate(efficient_producers, v1) = v7 & % 22.33/3.70 disbanding_rate(first_movers, v3) = v9 & disbanding_rate(first_movers, v2) % 22.33/3.70 = v4 & disbanding_rate(first_movers, v1) = v6 & difference(v6, v7) = v8 & % 22.33/3.70 $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & ( ~ % 22.33/3.70 greater(v4, v5) | greater(v9, v10) | decreases(v8)))) % 22.33/3.70 % 22.33/3.70 (mp_time_point_occurs) % 22.33/3.70 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ! [v1: $i] : ( ~ % 22.33/3.70 $i(v1) | ~ $i(v0) | ~ subpopulations(first_movers, efficient_producers, % 22.33/3.70 v0, v1) | ~ environment(v0) | in_environment(v0, v1)) % 22.33/3.70 % 22.33/3.70 (mp_times_in_order) % 22.33/3.70 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (start_time(v0) = % 22.33/3.70 v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ greater(v2, v1) | ~ % 22.33/3.70 greater_or_equal(v1, v3) | ~ in_environment(v0, v2) | ~ environment(v0) | % 22.33/3.70 in_environment(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 22.33/3.70 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ greater(v2, v1) | ~ in_environment(v0, % 22.33/3.70 v2) | ~ environment(v0) | in_environment(v0, v1) | ? [v3: $i] : % 22.33/3.70 (start_time(v0) = v3 & $i(v3) & ~ greater_or_equal(v1, v3))) % 22.33/3.70 % 22.33/3.71 (prove_l2) % 22.33/3.71 $i(efficient_producers) & $i(first_movers) & ? [v0: $i] : ? [v1: $i] : ? % 22.33/3.71 [v2: $i] : ? [v3: $i] : (disbanding_rate(efficient_producers, v1) = v3 & % 22.33/3.71 disbanding_rate(first_movers, v1) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 22.33/3.71 subpopulations(first_movers, efficient_producers, v0, v1) & environment(v0) % 22.33/3.71 & ~ greater(v2, v3)) % 22.33/3.71 % 22.33/3.71 (function-axioms) % 22.33/3.71 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.33/3.71 (disbanding_rate(v3, v2) = v1) | ~ (disbanding_rate(v3, v2) = v0)) & ! % 22.33/3.71 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.33/3.71 (difference(v3, v2) = v1) | ~ (difference(v3, v2) = v0)) & ! [v0: $i] : ! % 22.33/3.71 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (start_time(v2) = v1) | ~ % 22.33/3.71 (start_time(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 22.33/3.71 | ~ (initial_FM_EP(v2) = v1) | ~ (initial_FM_EP(v2) = v0)) % 22.33/3.71 % 22.33/3.71 Further assumptions not needed in the proof: % 22.33/3.71 -------------------------------------------- % 22.33/3.71 a10, mp_greater_transitivity % 22.33/3.71 % 22.33/3.71 Those formulas are unsatisfiable: % 22.33/3.71 --------------------------------- % 22.33/3.71 % 22.33/3.71 Begin of proof % 22.33/3.72 | % 22.33/3.72 | ALPHA: (l3) implies: % 22.33/3.72 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 22.33/3.72 | subpopulations(first_movers, efficient_producers, v0, v1) | ~ % 22.33/3.72 | environment(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 22.33/3.72 | (disbanding_rate(efficient_producers, v1) = v3 & % 22.33/3.72 | disbanding_rate(first_movers, v1) = v2 & difference(v2, v3) = v4 & % 22.33/3.72 | $i(v4) & $i(v3) & $i(v2) & ~ decreases(v4))) % 22.33/3.72 | % 22.33/3.72 | ALPHA: (mp_earliest_time_point) implies: % 22.33/3.73 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ (initial_FM_EP(v0) = v1) | ~ $i(v0) | % 22.33/3.73 | ~ in_environment(v0, v1) | ~ environment(v0) | % 22.33/3.73 | subpopulations(first_movers, efficient_producers, v0, v1)) % 22.33/3.73 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (initial_FM_EP(v0) = v2) % 22.33/3.73 | | ~ $i(v1) | ~ $i(v0) | ~ subpopulations(first_movers, % 22.33/3.73 | efficient_producers, v0, v1) | ~ environment(v0) | % 22.33/3.73 | greater_or_equal(v1, v2)) % 22.33/3.73 | % 22.33/3.73 | ALPHA: (mp_positive_function_difference) implies: % 22.33/3.74 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 22.33/3.74 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ greater_or_equal(v3, v1) | ~ % 22.33/3.74 | greater_or_equal(v1, v2) | ~ subpopulations(first_movers, % 22.33/3.74 | efficient_producers, v0, v3) | ~ environment(v0) | ? [v4: $i] : % 22.33/3.74 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 22.33/3.74 | ? [v10: $i] : (disbanding_rate(efficient_producers, v3) = v10 & % 22.33/3.74 | disbanding_rate(efficient_producers, v2) = v5 & % 22.33/3.74 | disbanding_rate(efficient_producers, v1) = v7 & % 22.33/3.74 | disbanding_rate(first_movers, v3) = v9 & % 22.33/3.74 | disbanding_rate(first_movers, v2) = v4 & % 22.33/3.74 | disbanding_rate(first_movers, v1) = v6 & difference(v6, v7) = v8 & % 22.33/3.74 | $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & ( ~ % 22.33/3.74 | greater(v4, v5) | greater(v9, v10) | decreases(v8)))) % 22.33/3.74 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 22.33/3.74 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ( ~ % 22.33/3.74 | (disbanding_rate(efficient_producers, v1) = v6) | ~ % 22.33/3.74 | (disbanding_rate(first_movers, v3) = v8) | ~ % 22.33/3.74 | (disbanding_rate(first_movers, v2) = v4) | ~ % 22.33/3.74 | (disbanding_rate(first_movers, v1) = v5) | ~ (difference(v5, v6) = % 22.33/3.74 | v7) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 22.33/3.74 | greater_or_equal(v3, v1) | ~ greater_or_equal(v1, v2) | ~ % 22.33/3.74 | subpopulations(first_movers, efficient_producers, v0, v3) | ~ % 22.33/3.74 | environment(v0) | decreases(v7) | ? [v9: $i] : ? [v10: $i] : % 22.33/3.74 | (disbanding_rate(efficient_producers, v3) = v10 & % 22.33/3.74 | disbanding_rate(efficient_producers, v2) = v9 & $i(v10) & $i(v9) & % 22.33/3.74 | ( ~ greater(v4, v9) | greater(v8, v10)))) % 22.33/3.74 | % 22.33/3.74 | ALPHA: (mp_time_point_occurs) implies: % 22.33/3.75 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 22.33/3.75 | subpopulations(first_movers, efficient_producers, v0, v1) | ~ % 22.33/3.75 | environment(v0) | in_environment(v0, v1)) % 22.33/3.75 | % 22.33/3.75 | ALPHA: (mp_initial_time) implies: % 22.33/3.75 | (7) ! [v0: $i] : ( ~ $i(v0) | ~ environment(v0) | ? [v1: $i] : ? [v2: % 22.33/3.75 | $i] : (start_time(v0) = v2 & initial_FM_EP(v0) = v1 & $i(v2) & % 22.33/3.75 | $i(v1) & greater_or_equal(v1, v2))) % 22.33/3.75 | % 22.33/3.75 | ALPHA: (mp_times_in_order) implies: % 22.33/3.75 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 22.33/3.75 | (start_time(v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 22.33/3.75 | greater(v2, v1) | ~ greater_or_equal(v1, v3) | ~ in_environment(v0, % 22.33/3.75 | v2) | ~ environment(v0) | in_environment(v0, v1)) % 22.33/3.75 | % 22.33/3.75 | ALPHA: (a8) implies: % 22.33/3.75 | (9) ! [v0: $i] : ( ~ $i(v0) | ~ environment(v0) | ? [v1: $i] : ? [v2: % 22.33/3.75 | $i] : ? [v3: $i] : (initial_FM_EP(v0) = v1 & % 22.33/3.75 | disbanding_rate(efficient_producers, v1) = v3 & % 22.33/3.75 | disbanding_rate(first_movers, v1) = v2 & $i(v3) & $i(v2) & $i(v1) & % 22.33/3.75 | greater(v2, v3))) % 22.33/3.75 | % 22.33/3.75 | ALPHA: (prove_l2) implies: % 22.33/3.76 | (10) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 22.33/3.76 | (disbanding_rate(efficient_producers, v1) = v3 & % 22.33/3.76 | disbanding_rate(first_movers, v1) = v2 & $i(v3) & $i(v2) & $i(v1) & % 22.33/3.76 | $i(v0) & subpopulations(first_movers, efficient_producers, v0, v1) & % 22.33/3.76 | environment(v0) & ~ greater(v2, v3)) % 22.33/3.76 | % 22.33/3.76 | ALPHA: (function-axioms) implies: % 22.33/3.76 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 22.33/3.76 | (initial_FM_EP(v2) = v1) | ~ (initial_FM_EP(v2) = v0)) % 22.33/3.76 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.33/3.76 | (difference(v3, v2) = v1) | ~ (difference(v3, v2) = v0)) % 22.33/3.76 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 22.33/3.76 | (disbanding_rate(v3, v2) = v1) | ~ (disbanding_rate(v3, v2) = v0)) % 22.33/3.76 | % 22.33/3.76 | DELTA: instantiating (10) with fresh symbols all_16_0, all_16_1, all_16_2, % 22.33/3.76 | all_16_3 gives: % 22.33/3.76 | (14) disbanding_rate(efficient_producers, all_16_2) = all_16_0 & % 22.33/3.76 | disbanding_rate(first_movers, all_16_2) = all_16_1 & $i(all_16_0) & % 22.33/3.76 | $i(all_16_1) & $i(all_16_2) & $i(all_16_3) & % 22.33/3.76 | subpopulations(first_movers, efficient_producers, all_16_3, all_16_2) % 22.33/3.76 | & environment(all_16_3) & ~ greater(all_16_1, all_16_0) % 22.33/3.76 | % 22.33/3.76 | ALPHA: (14) implies: % 22.33/3.77 | (15) ~ greater(all_16_1, all_16_0) % 22.33/3.77 | (16) environment(all_16_3) % 22.33/3.77 | (17) subpopulations(first_movers, efficient_producers, all_16_3, all_16_2) % 22.33/3.77 | (18) $i(all_16_3) % 22.33/3.77 | (19) $i(all_16_2) % 22.33/3.77 | (20) disbanding_rate(first_movers, all_16_2) = all_16_1 % 22.33/3.77 | (21) disbanding_rate(efficient_producers, all_16_2) = all_16_0 % 22.33/3.77 | % 22.33/3.77 | GROUND_INST: instantiating (9) with all_16_3, simplifying with (16), (18) % 22.33/3.77 | gives: % 22.33/3.77 | (22) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (initial_FM_EP(all_16_3) = % 22.33/3.77 | v0 & disbanding_rate(efficient_producers, v0) = v2 & % 22.33/3.77 | disbanding_rate(first_movers, v0) = v1 & $i(v2) & $i(v1) & $i(v0) & % 22.33/3.77 | greater(v1, v2)) % 22.33/3.77 | % 22.33/3.77 | GROUND_INST: instantiating (7) with all_16_3, simplifying with (16), (18) % 22.33/3.77 | gives: % 22.33/3.77 | (23) ? [v0: $i] : ? [v1: $i] : (start_time(all_16_3) = v1 & % 22.33/3.77 | initial_FM_EP(all_16_3) = v0 & $i(v1) & $i(v0) & % 22.33/3.77 | greater_or_equal(v0, v1)) % 22.33/3.77 | % 22.33/3.77 | GROUND_INST: instantiating (6) with all_16_3, all_16_2, simplifying with (16), % 22.33/3.77 | (17), (18), (19) gives: % 22.33/3.77 | (24) in_environment(all_16_3, all_16_2) % 22.33/3.77 | % 22.33/3.77 | GROUND_INST: instantiating (1) with all_16_3, all_16_2, simplifying with (16), % 22.33/3.78 | (17), (18), (19) gives: % 22.33/3.78 | (25) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.33/3.78 | (disbanding_rate(efficient_producers, all_16_2) = v1 & % 22.33/3.78 | disbanding_rate(first_movers, all_16_2) = v0 & difference(v0, v1) = % 22.33/3.78 | v2 & $i(v2) & $i(v1) & $i(v0) & ~ decreases(v2)) % 22.33/3.78 | % 22.33/3.78 | DELTA: instantiating (23) with fresh symbols all_24_0, all_24_1 gives: % 22.33/3.78 | (26) start_time(all_16_3) = all_24_0 & initial_FM_EP(all_16_3) = all_24_1 & % 22.33/3.78 | $i(all_24_0) & $i(all_24_1) & greater_or_equal(all_24_1, all_24_0) % 22.33/3.78 | % 22.33/3.78 | ALPHA: (26) implies: % 22.33/3.78 | (27) greater_or_equal(all_24_1, all_24_0) % 22.33/3.78 | (28) $i(all_24_0) % 22.33/3.78 | (29) initial_FM_EP(all_16_3) = all_24_1 % 22.33/3.78 | (30) start_time(all_16_3) = all_24_0 % 22.33/3.78 | % 22.33/3.78 | DELTA: instantiating (25) with fresh symbols all_26_0, all_26_1, all_26_2 % 22.33/3.78 | gives: % 22.33/3.78 | (31) disbanding_rate(efficient_producers, all_16_2) = all_26_1 & % 22.33/3.78 | disbanding_rate(first_movers, all_16_2) = all_26_2 & % 22.33/3.78 | difference(all_26_2, all_26_1) = all_26_0 & $i(all_26_0) & % 22.33/3.78 | $i(all_26_1) & $i(all_26_2) & ~ decreases(all_26_0) % 22.33/3.78 | % 22.33/3.78 | ALPHA: (31) implies: % 22.33/3.78 | (32) disbanding_rate(first_movers, all_16_2) = all_26_2 % 22.33/3.78 | (33) disbanding_rate(efficient_producers, all_16_2) = all_26_1 % 22.33/3.78 | % 22.33/3.78 | DELTA: instantiating (22) with fresh symbols all_28_0, all_28_1, all_28_2 % 22.33/3.78 | gives: % 22.33/3.78 | (34) initial_FM_EP(all_16_3) = all_28_2 & % 22.33/3.78 | disbanding_rate(efficient_producers, all_28_2) = all_28_0 & % 22.33/3.78 | disbanding_rate(first_movers, all_28_2) = all_28_1 & $i(all_28_0) & % 22.33/3.78 | $i(all_28_1) & $i(all_28_2) & greater(all_28_1, all_28_0) % 22.33/3.78 | % 22.33/3.78 | ALPHA: (34) implies: % 22.33/3.79 | (35) greater(all_28_1, all_28_0) % 22.33/3.79 | (36) $i(all_28_2) % 22.33/3.79 | (37) disbanding_rate(first_movers, all_28_2) = all_28_1 % 22.33/3.79 | (38) disbanding_rate(efficient_producers, all_28_2) = all_28_0 % 22.33/3.79 | (39) initial_FM_EP(all_16_3) = all_28_2 % 22.33/3.79 | % 22.33/3.79 | GROUND_INST: instantiating (13) with all_16_1, all_26_2, all_16_2, % 22.33/3.79 | first_movers, simplifying with (20), (32) gives: % 22.33/3.79 | (40) all_26_2 = all_16_1 % 22.33/3.79 | % 22.33/3.79 | GROUND_INST: instantiating (13) with all_16_0, all_26_1, all_16_2, % 22.33/3.79 | efficient_producers, simplifying with (21), (33) gives: % 22.33/3.79 | (41) all_26_1 = all_16_0 % 22.33/3.79 | % 22.33/3.79 | GROUND_INST: instantiating (11) with all_24_1, all_28_2, all_16_3, simplifying % 22.33/3.79 | with (29), (39) gives: % 22.33/3.79 | (42) all_28_2 = all_24_1 % 22.33/3.79 | % 22.33/3.79 | REDUCE: (38), (42) imply: % 22.33/3.79 | (43) disbanding_rate(efficient_producers, all_24_1) = all_28_0 % 22.33/3.79 | % 22.33/3.79 | REDUCE: (37), (42) imply: % 22.33/3.79 | (44) disbanding_rate(first_movers, all_24_1) = all_28_1 % 22.33/3.79 | % 22.33/3.79 | REDUCE: (36), (42) imply: % 22.33/3.79 | (45) $i(all_24_1) % 22.33/3.79 | % 22.33/3.79 | GROUND_INST: instantiating (3) with all_16_3, all_16_2, all_24_1, simplifying % 22.33/3.79 | with (16), (17), (18), (19), (29) gives: % 22.33/3.79 | (46) greater_or_equal(all_16_2, all_24_1) % 22.33/3.79 | % 22.33/3.80 | GROUND_INST: instantiating (4) with all_16_3, all_24_1, all_24_0, all_16_2, % 22.33/3.80 | simplifying with (16), (17), (18), (19), (27), (28), (45), (46) % 22.33/3.80 | gives: % 22.82/3.80 | (47) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 22.82/3.80 | ? [v5: $i] : ? [v6: $i] : (disbanding_rate(efficient_producers, % 22.82/3.80 | all_24_0) = v1 & disbanding_rate(efficient_producers, all_24_1) = % 22.82/3.80 | v3 & disbanding_rate(efficient_producers, all_16_2) = v6 & % 22.82/3.80 | disbanding_rate(first_movers, all_24_0) = v0 & % 22.82/3.80 | disbanding_rate(first_movers, all_24_1) = v2 & % 22.82/3.80 | disbanding_rate(first_movers, all_16_2) = v5 & difference(v2, v3) = % 22.82/3.80 | v4 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 22.82/3.80 | ( ~ greater(v0, v1) | greater(v5, v6) | decreases(v4))) % 22.82/3.80 | % 22.82/3.80 | GROUND_INST: instantiating (mp_greater_or_equal) with all_16_2, all_24_1, % 22.82/3.80 | simplifying with (19), (45), (46) gives: % 22.82/3.80 | (48) all_24_1 = all_16_2 | greater(all_16_2, all_24_1) % 22.82/3.80 | % 22.82/3.80 | DELTA: instantiating (47) with fresh symbols all_45_0, all_45_1, all_45_2, % 22.82/3.80 | all_45_3, all_45_4, all_45_5, all_45_6 gives: % 22.82/3.80 | (49) disbanding_rate(efficient_producers, all_24_0) = all_45_5 & % 22.82/3.80 | disbanding_rate(efficient_producers, all_24_1) = all_45_3 & % 22.82/3.80 | disbanding_rate(efficient_producers, all_16_2) = all_45_0 & % 22.82/3.80 | disbanding_rate(first_movers, all_24_0) = all_45_6 & % 22.82/3.80 | disbanding_rate(first_movers, all_24_1) = all_45_4 & % 22.82/3.80 | disbanding_rate(first_movers, all_16_2) = all_45_1 & % 22.82/3.80 | difference(all_45_4, all_45_3) = all_45_2 & $i(all_45_0) & % 22.82/3.80 | $i(all_45_1) & $i(all_45_2) & $i(all_45_3) & $i(all_45_4) & % 22.82/3.81 | $i(all_45_5) & $i(all_45_6) & ( ~ greater(all_45_6, all_45_5) | % 22.82/3.81 | greater(all_45_1, all_45_0) | decreases(all_45_2)) % 22.82/3.81 | % 22.82/3.81 | ALPHA: (49) implies: % 22.82/3.81 | (50) difference(all_45_4, all_45_3) = all_45_2 % 22.82/3.81 | (51) disbanding_rate(first_movers, all_16_2) = all_45_1 % 22.82/3.81 | (52) disbanding_rate(first_movers, all_24_1) = all_45_4 % 22.82/3.81 | (53) disbanding_rate(efficient_producers, all_16_2) = all_45_0 % 22.82/3.81 | (54) disbanding_rate(efficient_producers, all_24_1) = all_45_3 % 22.82/3.81 | % 22.82/3.81 | GROUND_INST: instantiating (13) with all_16_1, all_45_1, all_16_2, % 22.82/3.81 | first_movers, simplifying with (20), (51) gives: % 22.82/3.81 | (55) all_45_1 = all_16_1 % 22.82/3.81 | % 22.82/3.81 | GROUND_INST: instantiating (13) with all_28_1, all_45_4, all_24_1, % 22.82/3.81 | first_movers, simplifying with (44), (52) gives: % 22.82/3.81 | (56) all_45_4 = all_28_1 % 22.82/3.81 | % 22.82/3.81 | GROUND_INST: instantiating (13) with all_16_0, all_45_0, all_16_2, % 22.82/3.81 | efficient_producers, simplifying with (21), (53) gives: % 22.82/3.81 | (57) all_45_0 = all_16_0 % 22.82/3.81 | % 22.82/3.81 | GROUND_INST: instantiating (13) with all_28_0, all_45_3, all_24_1, % 22.82/3.81 | efficient_producers, simplifying with (43), (54) gives: % 22.82/3.81 | (58) all_45_3 = all_28_0 % 22.82/3.81 | % 22.82/3.81 | REDUCE: (50), (56), (58) imply: % 22.82/3.81 | (59) difference(all_28_1, all_28_0) = all_45_2 % 22.82/3.81 | % 22.82/3.81 | BETA: splitting (48) gives: % 22.82/3.81 | % 22.82/3.81 | Case 1: % 22.82/3.81 | | % 22.82/3.81 | | (60) greater(all_16_2, all_24_1) % 22.82/3.82 | | % 22.82/3.82 | | GROUND_INST: instantiating (8) with all_16_3, all_24_1, all_16_2, all_24_0, % 22.82/3.82 | | simplifying with (16), (18), (19), (24), (27), (30), (45), (60) % 22.82/3.82 | | gives: % 22.82/3.82 | | (61) in_environment(all_16_3, all_24_1) % 22.82/3.82 | | % 22.82/3.82 | | GROUND_INST: instantiating (2) with all_16_3, all_24_1, simplifying with % 22.82/3.82 | | (16), (18), (29), (61) gives: % 22.82/3.82 | | (62) subpopulations(first_movers, efficient_producers, all_16_3, % 22.82/3.82 | | all_24_1) % 22.82/3.82 | | % 22.82/3.82 | | GROUND_INST: instantiating (3) with all_16_3, all_24_1, all_24_1, % 22.82/3.82 | | simplifying with (16), (18), (29), (45), (62) gives: % 22.82/3.82 | | (63) greater_or_equal(all_24_1, all_24_1) % 22.82/3.82 | | % 22.82/3.82 | | GROUND_INST: instantiating (1) with all_16_3, all_24_1, simplifying with % 22.82/3.82 | | (16), (18), (45), (62) gives: % 22.82/3.82 | | (64) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 22.82/3.82 | | (disbanding_rate(efficient_producers, all_24_1) = v1 & % 22.82/3.82 | | disbanding_rate(first_movers, all_24_1) = v0 & difference(v0, v1) % 22.82/3.82 | | = v2 & $i(v2) & $i(v1) & $i(v0) & ~ decreases(v2)) % 22.82/3.82 | | % 22.82/3.82 | | DELTA: instantiating (64) with fresh symbols all_97_0, all_97_1, all_97_2 % 22.82/3.82 | | gives: % 22.82/3.82 | | (65) disbanding_rate(efficient_producers, all_24_1) = all_97_1 & % 22.82/3.82 | | disbanding_rate(first_movers, all_24_1) = all_97_2 & % 22.82/3.82 | | difference(all_97_2, all_97_1) = all_97_0 & $i(all_97_0) & % 22.82/3.82 | | $i(all_97_1) & $i(all_97_2) & ~ decreases(all_97_0) % 22.82/3.82 | | % 22.82/3.82 | | ALPHA: (65) implies: % 22.82/3.83 | | (66) ~ decreases(all_97_0) % 22.82/3.83 | | (67) difference(all_97_2, all_97_1) = all_97_0 % 22.82/3.83 | | (68) disbanding_rate(first_movers, all_24_1) = all_97_2 % 22.82/3.83 | | (69) disbanding_rate(efficient_producers, all_24_1) = all_97_1 % 22.82/3.83 | | % 22.82/3.83 | | GROUND_INST: instantiating (13) with all_28_1, all_97_2, all_24_1, % 22.82/3.83 | | first_movers, simplifying with (44), (68) gives: % 22.82/3.83 | | (70) all_97_2 = all_28_1 % 22.82/3.83 | | % 22.82/3.83 | | GROUND_INST: instantiating (13) with all_28_0, all_97_1, all_24_1, % 22.82/3.83 | | efficient_producers, simplifying with (43), (69) gives: % 22.82/3.83 | | (71) all_97_1 = all_28_0 % 22.82/3.83 | | % 22.82/3.83 | | REDUCE: (67), (70), (71) imply: % 22.82/3.83 | | (72) difference(all_28_1, all_28_0) = all_97_0 % 22.82/3.83 | | % 22.82/3.83 | | GROUND_INST: instantiating (12) with all_45_2, all_97_0, all_28_0, all_28_1, % 22.82/3.83 | | simplifying with (59), (72) gives: % 22.82/3.83 | | (73) all_97_0 = all_45_2 % 22.82/3.83 | | % 22.82/3.83 | | REDUCE: (66), (73) imply: % 22.82/3.83 | | (74) ~ decreases(all_45_2) % 22.82/3.83 | | % 22.82/3.83 | | GROUND_INST: instantiating (5) with all_16_3, all_24_1, all_24_1, all_16_2, % 22.82/3.83 | | all_28_1, all_28_1, all_28_0, all_45_2, all_16_1, simplifying % 22.82/3.83 | | with (16), (17), (18), (19), (20), (43), (44), (45), (46), % 22.82/3.83 | | (59), (63), (74) gives: % 22.82/3.84 | | (75) ? [v0: $i] : ? [v1: $i] : (disbanding_rate(efficient_producers, % 22.82/3.84 | | all_24_1) = v0 & disbanding_rate(efficient_producers, all_16_2) % 22.82/3.84 | | = v1 & $i(v1) & $i(v0) & ( ~ greater(all_28_1, v0) | % 22.82/3.84 | | greater(all_16_1, v1))) % 22.82/3.84 | | % 22.82/3.84 | | GROUND_INST: instantiating (4) with all_16_3, all_24_1, all_24_1, all_16_2, % 22.82/3.84 | | simplifying with (16), (17), (18), (19), (45), (46), (63) % 22.82/3.84 | | gives: % 22.82/3.84 | | (76) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] % 22.82/3.84 | | : ? [v5: $i] : ? [v6: $i] : (disbanding_rate(efficient_producers, % 22.82/3.84 | | all_24_1) = v3 & disbanding_rate(efficient_producers, all_24_1) % 22.82/3.84 | | = v1 & disbanding_rate(efficient_producers, all_16_2) = v6 & % 22.82/3.84 | | disbanding_rate(first_movers, all_24_1) = v2 & % 22.82/3.84 | | disbanding_rate(first_movers, all_24_1) = v0 & % 22.82/3.84 | | disbanding_rate(first_movers, all_16_2) = v5 & difference(v2, v3) % 22.82/3.84 | | = v4 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 22.82/3.84 | | $i(v0) & ( ~ greater(v0, v1) | greater(v5, v6) | decreases(v4))) % 22.82/3.84 | | % 22.82/3.84 | | DELTA: instantiating (75) with fresh symbols all_112_0, all_112_1 gives: % 22.82/3.84 | | (77) disbanding_rate(efficient_producers, all_24_1) = all_112_1 & % 22.82/3.84 | | disbanding_rate(efficient_producers, all_16_2) = all_112_0 & % 22.82/3.84 | | $i(all_112_0) & $i(all_112_1) & ( ~ greater(all_28_1, all_112_1) | % 22.82/3.84 | | greater(all_16_1, all_112_0)) % 22.82/3.84 | | % 22.82/3.84 | | ALPHA: (77) implies: % 22.82/3.84 | | (78) disbanding_rate(efficient_producers, all_16_2) = all_112_0 % 22.82/3.84 | | (79) disbanding_rate(efficient_producers, all_24_1) = all_112_1 % 22.82/3.85 | | (80) ~ greater(all_28_1, all_112_1) | greater(all_16_1, all_112_0) % 22.82/3.85 | | % 22.82/3.85 | | DELTA: instantiating (76) with fresh symbols all_114_0, all_114_1, % 22.82/3.85 | | all_114_2, all_114_3, all_114_4, all_114_5, all_114_6 gives: % 22.82/3.85 | | (81) disbanding_rate(efficient_producers, all_24_1) = all_114_3 & % 22.82/3.85 | | disbanding_rate(efficient_producers, all_24_1) = all_114_5 & % 22.82/3.85 | | disbanding_rate(efficient_producers, all_16_2) = all_114_0 & % 22.82/3.85 | | disbanding_rate(first_movers, all_24_1) = all_114_4 & % 22.82/3.85 | | disbanding_rate(first_movers, all_24_1) = all_114_6 & % 22.82/3.85 | | disbanding_rate(first_movers, all_16_2) = all_114_1 & % 22.82/3.85 | | difference(all_114_4, all_114_3) = all_114_2 & $i(all_114_0) & % 22.82/3.85 | | $i(all_114_1) & $i(all_114_2) & $i(all_114_3) & $i(all_114_4) & % 22.82/3.85 | | $i(all_114_5) & $i(all_114_6) & ( ~ greater(all_114_6, all_114_5) | % 22.82/3.85 | | greater(all_114_1, all_114_0) | decreases(all_114_2)) % 22.82/3.85 | | % 22.82/3.85 | | ALPHA: (81) implies: % 22.82/3.85 | | (82) disbanding_rate(efficient_producers, all_16_2) = all_114_0 % 22.82/3.85 | | (83) disbanding_rate(efficient_producers, all_24_1) = all_114_5 % 22.82/3.85 | | (84) disbanding_rate(efficient_producers, all_24_1) = all_114_3 % 22.82/3.85 | | % 22.82/3.85 | | GROUND_INST: instantiating (13) with all_16_0, all_114_0, all_16_2, % 22.82/3.85 | | efficient_producers, simplifying with (21), (82) gives: % 22.82/3.85 | | (85) all_114_0 = all_16_0 % 22.82/3.85 | | % 22.82/3.85 | | GROUND_INST: instantiating (13) with all_112_0, all_114_0, all_16_2, % 22.82/3.86 | | efficient_producers, simplifying with (78), (82) gives: % 22.82/3.86 | | (86) all_114_0 = all_112_0 % 22.82/3.86 | | % 22.82/3.86 | | GROUND_INST: instantiating (13) with all_112_1, all_114_5, all_24_1, % 22.82/3.86 | | efficient_producers, simplifying with (79), (83) gives: % 22.82/3.86 | | (87) all_114_5 = all_112_1 % 22.82/3.86 | | % 22.82/3.86 | | GROUND_INST: instantiating (13) with all_28_0, all_114_3, all_24_1, % 22.82/3.86 | | efficient_producers, simplifying with (43), (84) gives: % 22.82/3.86 | | (88) all_114_3 = all_28_0 % 22.82/3.86 | | % 22.82/3.86 | | GROUND_INST: instantiating (13) with all_114_5, all_114_3, all_24_1, % 22.82/3.86 | | efficient_producers, simplifying with (83), (84) gives: % 22.82/3.86 | | (89) all_114_3 = all_114_5 % 22.82/3.86 | | % 22.82/3.86 | | COMBINE_EQS: (85), (86) imply: % 22.82/3.86 | | (90) all_112_0 = all_16_0 % 22.82/3.86 | | % 22.82/3.86 | | COMBINE_EQS: (88), (89) imply: % 22.82/3.86 | | (91) all_114_5 = all_28_0 % 22.82/3.86 | | % 22.82/3.86 | | SIMP: (91) implies: % 22.82/3.86 | | (92) all_114_5 = all_28_0 % 22.82/3.86 | | % 22.82/3.86 | | COMBINE_EQS: (87), (92) imply: % 22.82/3.86 | | (93) all_112_1 = all_28_0 % 22.82/3.86 | | % 22.82/3.86 | | SIMP: (93) implies: % 22.82/3.86 | | (94) all_112_1 = all_28_0 % 22.82/3.86 | | % 22.82/3.86 | | BETA: splitting (80) gives: % 22.82/3.86 | | % 22.82/3.86 | | Case 1: % 22.82/3.86 | | | % 22.82/3.86 | | | (95) ~ greater(all_28_1, all_112_1) % 22.82/3.86 | | | % 22.82/3.86 | | | REDUCE: (94), (95) imply: % 22.82/3.86 | | | (96) ~ greater(all_28_1, all_28_0) % 22.82/3.86 | | | % 22.82/3.86 | | | PRED_UNIFY: (35), (96) imply: % 22.82/3.86 | | | (97) $false % 22.82/3.87 | | | % 22.82/3.87 | | | CLOSE: (97) is inconsistent. % 22.82/3.87 | | | % 22.82/3.87 | | Case 2: % 22.82/3.87 | | | % 22.82/3.87 | | | (98) greater(all_16_1, all_112_0) % 22.82/3.87 | | | % 22.82/3.87 | | | REDUCE: (90), (98) imply: % 22.82/3.87 | | | (99) greater(all_16_1, all_16_0) % 22.82/3.87 | | | % 22.82/3.87 | | | PRED_UNIFY: (15), (99) imply: % 22.82/3.87 | | | (100) $false % 22.82/3.87 | | | % 22.82/3.87 | | | CLOSE: (100) is inconsistent. % 22.82/3.87 | | | % 22.82/3.87 | | End of split % 22.82/3.87 | | % 22.82/3.87 | Case 2: % 22.82/3.87 | | % 22.82/3.87 | | (101) all_24_1 = all_16_2 % 22.82/3.87 | | % 22.82/3.87 | | REDUCE: (43), (101) imply: % 22.82/3.87 | | (102) disbanding_rate(efficient_producers, all_16_2) = all_28_0 % 22.82/3.87 | | % 22.82/3.87 | | REDUCE: (44), (101) imply: % 22.82/3.87 | | (103) disbanding_rate(first_movers, all_16_2) = all_28_1 % 22.82/3.87 | | % 22.82/3.87 | | GROUND_INST: instantiating (13) with all_16_1, all_28_1, all_16_2, % 22.82/3.87 | | first_movers, simplifying with (20), (103) gives: % 22.82/3.87 | | (104) all_28_1 = all_16_1 % 22.82/3.87 | | % 22.82/3.87 | | GROUND_INST: instantiating (13) with all_16_0, all_28_0, all_16_2, % 22.82/3.87 | | efficient_producers, simplifying with (21), (102) gives: % 22.82/3.87 | | (105) all_28_0 = all_16_0 % 22.82/3.87 | | % 22.82/3.87 | | REDUCE: (35), (104), (105) imply: % 22.82/3.87 | | (106) greater(all_16_1, all_16_0) % 22.82/3.87 | | % 22.82/3.87 | | PRED_UNIFY: (15), (106) imply: % 22.82/3.87 | | (107) $false % 22.82/3.87 | | % 22.82/3.87 | | CLOSE: (107) is inconsistent. % 22.82/3.87 | | % 22.82/3.87 | End of split % 22.82/3.87 | % 22.82/3.87 End of proof % 22.82/3.88 % SZS output end Proof for theBenchmark % 22.82/3.88 % 22.82/3.88 3146ms %------------------------------------------------------------------------------