%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : MGT039+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 : n002.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:24 AM UTC 2026 % Result : Theorem 14.93s 2.72s % Output : Proof 25.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT039+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.11/0.36 % Computer : n002.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Mon Sep 7 12:56:22 UTC 2026 % 0.11/0.36 % CPUTime : % 0.11/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.67/0.73 ________ _____ % 0.67/0.73 ___ __ \_________(_)________________________________ % 0.67/0.73 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.67/0.73 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.67/0.73 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.67/0.73 % 0.67/0.73 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.67/0.73 (2023-06-19) % 0.67/0.73 % 0.67/0.73 (c) Philipp Rümmer, 2009-2023 % 0.67/0.73 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.67/0.73 Amanda Stjerna. % 0.67/0.73 Free software under BSD-3-Clause. % 0.67/0.73 % 0.67/0.73 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.67/0.73 % 0.67/0.73 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.67/0.75 Running up to 7 provers in parallel. % 0.67/0.76 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.67/0.76 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.67/0.76 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.67/0.76 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.67/0.76 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.67/0.76 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.67/0.76 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.81/1.20 Prover 4: Preprocessing ... % 3.25/1.23 Prover 1: Preprocessing ... % 3.25/1.28 Prover 6: Preprocessing ... % 3.25/1.28 Prover 2: Preprocessing ... % 3.25/1.28 Prover 5: Preprocessing ... % 3.25/1.28 Prover 0: Preprocessing ... % 3.25/1.28 Prover 3: Preprocessing ... % 7.08/1.70 Prover 1: Constructing countermodel ... % 7.08/1.70 Prover 6: Proving ... % 7.08/1.71 Prover 5: Proving ... % 7.08/1.71 Prover 2: Proving ... % 7.08/1.72 Prover 3: Constructing countermodel ... % 7.82/1.81 Prover 4: Constructing countermodel ... % 8.61/1.96 Prover 0: Proving ... % 8.61/2.02 Prover 3: gave up % 8.61/2.03 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 9.63/2.09 Prover 7: Preprocessing ... % 10.94/2.23 Prover 7: Warning: ignoring some quantifiers % 10.94/2.26 Prover 7: Constructing countermodel ... % 12.55/2.42 Prover 7: gave up % 12.55/2.43 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 12.55/2.48 Prover 8: Preprocessing ... % 14.12/2.67 Prover 8: Warning: ignoring some quantifiers % 14.12/2.68 Prover 8: Constructing countermodel ... % 14.93/2.72 Prover 2: proved (1957ms) % 14.93/2.72 % 14.93/2.72 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.93/2.72 % 14.93/2.72 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 14.93/2.72 Prover 5: stopped % 14.93/2.72 Prover 6: stopped % 14.93/2.73 Prover 0: stopped % 14.93/2.74 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 14.93/2.74 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 14.93/2.74 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 14.93/2.75 Prover 10: Preprocessing ... % 14.93/2.78 Prover 16: Preprocessing ... % 15.70/2.80 Prover 11: Preprocessing ... % 15.70/2.81 Prover 13: Preprocessing ... % 15.70/2.82 Prover 16: Warning: ignoring some quantifiers % 15.70/2.82 Prover 16: Constructing countermodel ... % 15.70/2.83 Prover 10: Warning: ignoring some quantifiers % 15.70/2.84 Prover 10: Constructing countermodel ... % 15.70/2.88 Prover 10: gave up % 15.70/2.89 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 16.50/2.93 Prover 19: Preprocessing ... % 16.50/2.95 Prover 13: Warning: ignoring some quantifiers % 16.50/2.98 Prover 13: Constructing countermodel ... % 17.70/3.10 Prover 19: Warning: ignoring some quantifiers % 17.70/3.13 Prover 19: Constructing countermodel ... % 18.86/3.20 Prover 11: Constructing countermodel ... % 19.63/3.37 Prover 16: gave up % 24.35/3.93 Prover 13: Found proof (size 138) % 24.35/3.93 Prover 13: proved (1200ms) % 24.35/3.93 Prover 8: stopped % 24.35/3.93 Prover 1: stopped % 24.35/3.93 Prover 19: stopped % 24.35/3.93 Prover 11: stopped % 24.35/3.93 Prover 4: stopped % 24.35/3.93 % 24.35/3.93 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 24.35/3.93 % 24.35/3.95 % SZS output start Proof for theBenchmark % 24.35/3.95 Assumptions after simplification: % 24.35/3.95 --------------------------------- % 24.35/3.95 % 24.35/3.95 (l8) % 24.35/3.98 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ! [v1: $i] : ! % 24.35/3.98 [v2: $i] : ( ~ (critical_point(v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 24.35/3.98 greater(v1, v2) | ~ in_environment(v0, v1) | ~ environment(v0) | % 24.35/3.98 selection_favors(efficient_producers, first_movers, v1)) & ! [v0: $i] : ! % 24.35/3.98 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ in_environment(v0, v1) | ~ % 24.35/3.98 environment(v0) | selection_favors(efficient_producers, first_movers, v1) | % 24.35/3.98 ? [v2: $i] : (critical_point(v0) = v2 & $i(v2) & ~ greater(v1, v2))) % 24.35/3.98 % 24.35/3.98 (mp3_favoured_trategy) % 24.35/3.98 $i(efficient_producers) & $i(first_movers) & ! [v0: $i] : ( ~ $i(v0) | ~ % 24.35/3.98 propagation_strategy(efficient_producers) | ~ % 24.35/3.98 propagation_strategy(first_movers) | ~ observational_period(v0) | % 24.35/3.98 selection_favors(efficient_producers, first_movers, v0) | ? [v1: $i] : ? % 24.35/3.98 [v2: $i] : (end_time(v1) = v2 & $i(v2) & $i(v1) & in_environment(v0, v1) & % 24.35/3.98 environment(v1) & ~ selection_favors(efficient_producers, first_movers, % 24.35/3.98 v2))) % 24.35/3.98 % 24.35/3.98 (mp4_critical_point) % 24.35/3.99 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (critical_point(v1) = v2) | ~ % 24.35/3.99 $i(v1) | ~ $i(v0) | ~ slow_change(v0) | ~ in_environment(v0, v1) | ~ % 24.35/3.99 environment(v1) | ~ observational_period(v0) | ? [v3: $i] : ($i(v3) & % 24.35/3.99 greater(v3, v2) & in_environment(v1, v3))) & ! [v0: $i] : ! [v1: $i] : ( % 24.35/3.99 ~ $i(v1) | ~ $i(v0) | ~ slow_change(v0) | ~ in_environment(v0, v1) | ~ % 24.35/3.99 environment(v1) | ~ observational_period(v0) | ? [v2: $i] : ? [v3: $i] : % 24.35/3.99 (critical_point(v1) = v2 & $i(v3) & $i(v2) & greater(v3, v2) & % 24.35/3.99 in_environment(v1, v3))) % 24.35/3.99 % 24.35/3.99 (mp_beginning_and_ending) % 24.35/3.99 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (start_time(v0) = v2) | ~ % 24.35/3.99 $i(v1) | ~ $i(v0) | ~ greater(v1, v2) | ~ environment(v0) | ? [v3: $i] : % 24.35/3.99 (end_time(v0) = v3 & $i(v3) & (greater_or_equal(v3, v1) | greater(v1, v3)))) % 24.35/3.99 & ? [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ environment(v1) | ? % 24.35/3.99 [v2: $i] : ? [v3: $i] : (start_time(v1) = v2 & end_time(v1) = v3 & $i(v3) & % 24.35/3.99 $i(v2) & ( ~ greater(v0, v2) | greater_or_equal(v3, v0) | greater(v0, % 24.35/3.99 v3)))) % 24.35/3.99 % 24.35/3.99 (mp_environment_end_point) % 24.35/3.99 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (end_time(v0) = v2) | ~ $i(v1) % 24.35/3.99 | ~ $i(v0) | ~ in_environment(v0, v1) | ~ environment(v0) | % 24.35/3.99 greater_or_equal(v2, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 24.35/3.99 $i(v0) | ~ in_environment(v0, v1) | ~ environment(v0) | ? [v2: $i] : % 24.35/3.99 (end_time(v0) = v2 & $i(v2) & greater_or_equal(v2, v1))) % 24.35/3.99 % 24.35/3.99 (mp_greater_or_equal) % 24.35/3.99 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ % 24.35/3.99 greater_or_equal(v0, v1) | greater(v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( % 24.35/3.99 ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) | greater_or_equal(v0, v1)) & ? % 24.35/3.99 [v0: $i] : ( ~ $i(v0) | greater_or_equal(v0, v0)) % 24.35/3.99 % 24.35/4.00 (mp_greater_transitivity) % 24.35/4.00 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 24.35/4.00 ~ greater(v1, v2) | ~ greater(v0, v1) | greater(v0, v2)) % 24.35/4.00 % 24.35/4.00 (mp_organizational_sets1) % 24.35/4.00 $i(first_movers) & propagation_strategy(first_movers) % 24.35/4.00 % 24.35/4.00 (mp_organizational_sets2) % 24.35/4.00 $i(efficient_producers) & propagation_strategy(efficient_producers) % 24.35/4.00 % 24.35/4.00 (mp_time_in_environment) % 24.35/4.00 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (start_time(v0) = v2) | ~ % 24.35/4.00 $i(v1) | ~ $i(v0) | ~ greater_or_equal(v1, v2) | ~ environment(v0) | % 24.35/4.00 in_environment(v0, v1) | ? [v3: $i] : (end_time(v0) = v3 & $i(v3) & ~ % 24.35/4.00 greater_or_equal(v3, v1))) & ? [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 24.35/4.00 $i(v0) | ~ environment(v1) | in_environment(v1, v0) | ? [v2: $i] : ? [v3: % 24.35/4.00 $i] : (start_time(v1) = v2 & end_time(v1) = v3 & $i(v3) & $i(v2) & ( ~ % 24.35/4.00 greater_or_equal(v3, v0) | ~ greater_or_equal(v0, v2)))) % 24.35/4.00 % 24.35/4.00 (mp_time_of_critical_point) % 24.35/4.00 ! [v0: $i] : ! [v1: $i] : ( ~ (start_time(v0) = v1) | ~ $i(v0) | ~ % 24.35/4.00 environment(v0) | ? [v2: $i] : (critical_point(v0) = v2 & $i(v2) & % 24.35/4.00 greater_or_equal(v2, v1))) & ! [v0: $i] : ( ~ $i(v0) | ~ environment(v0) % 24.35/4.00 | ? [v1: $i] : ? [v2: $i] : (start_time(v0) = v2 & critical_point(v0) = v1 % 24.35/4.00 & $i(v2) & $i(v1) & greater_or_equal(v1, v2))) % 24.35/4.00 % 24.35/4.00 (prove_t8) % 24.35/4.00 $i(efficient_producers) & $i(first_movers) & ? [v0: $i] : ($i(v0) & % 24.35/4.00 slow_change(v0) & observational_period(v0) & ~ % 24.35/4.00 selection_favors(efficient_producers, first_movers, v0)) % 24.35/4.00 % 24.35/4.00 (function-axioms) % 24.35/4.01 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (start_time(v2) = v1) % 24.35/4.01 | ~ (start_time(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 % 24.35/4.01 = v0 | ~ (critical_point(v2) = v1) | ~ (critical_point(v2) = v0)) & ! % 24.35/4.01 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (end_time(v2) = v1) | ~ % 24.35/4.01 (end_time(v2) = v0)) % 24.35/4.01 % 24.35/4.01 Those formulas are unsatisfiable: % 24.35/4.01 --------------------------------- % 24.35/4.01 % 24.35/4.01 Begin of proof % 24.35/4.01 | % 24.35/4.01 | ALPHA: (mp3_favoured_trategy) implies: % 24.35/4.01 | (1) ! [v0: $i] : ( ~ $i(v0) | ~ propagation_strategy(efficient_producers) % 24.35/4.01 | | ~ propagation_strategy(first_movers) | ~ observational_period(v0) % 24.35/4.01 | | selection_favors(efficient_producers, first_movers, v0) | ? [v1: % 24.35/4.01 | $i] : ? [v2: $i] : (end_time(v1) = v2 & $i(v2) & $i(v1) & % 24.35/4.01 | in_environment(v0, v1) & environment(v1) & ~ % 24.35/4.01 | selection_favors(efficient_producers, first_movers, v2))) % 24.35/4.01 | % 24.35/4.01 | ALPHA: (mp4_critical_point) implies: % 24.35/4.01 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ slow_change(v0) % 24.35/4.01 | | ~ in_environment(v0, v1) | ~ environment(v1) | ~ % 24.35/4.01 | observational_period(v0) | ? [v2: $i] : ? [v3: $i] : % 24.35/4.01 | (critical_point(v1) = v2 & $i(v3) & $i(v2) & greater(v3, v2) & % 24.35/4.01 | in_environment(v1, v3))) % 24.35/4.02 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (critical_point(v1) = v2) % 24.35/4.02 | | ~ $i(v1) | ~ $i(v0) | ~ slow_change(v0) | ~ in_environment(v0, % 24.35/4.02 | v1) | ~ environment(v1) | ~ observational_period(v0) | ? [v3: % 24.35/4.02 | $i] : ($i(v3) & greater(v3, v2) & in_environment(v1, v3))) % 24.35/4.02 | % 24.35/4.02 | ALPHA: (mp_organizational_sets1) implies: % 24.35/4.02 | (4) propagation_strategy(first_movers) % 24.35/4.02 | % 24.35/4.02 | ALPHA: (mp_organizational_sets2) implies: % 24.35/4.02 | (5) propagation_strategy(efficient_producers) % 24.35/4.02 | % 24.35/4.02 | ALPHA: (mp_time_in_environment) implies: % 24.35/4.02 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (start_time(v0) = v2) | % 24.35/4.02 | ~ $i(v1) | ~ $i(v0) | ~ greater_or_equal(v1, v2) | ~ % 24.35/4.02 | environment(v0) | in_environment(v0, v1) | ? [v3: $i] : % 24.35/4.02 | (end_time(v0) = v3 & $i(v3) & ~ greater_or_equal(v3, v1))) % 24.35/4.02 | % 24.35/4.02 | ALPHA: (mp_environment_end_point) implies: % 24.35/4.02 | (7) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 24.35/4.02 | in_environment(v0, v1) | ~ environment(v0) | ? [v2: $i] : % 24.35/4.02 | (end_time(v0) = v2 & $i(v2) & greater_or_equal(v2, v1))) % 24.35/4.02 | % 24.35/4.02 | ALPHA: (mp_time_of_critical_point) implies: % 24.35/4.02 | (8) ! [v0: $i] : ( ~ $i(v0) | ~ environment(v0) | ? [v1: $i] : ? [v2: % 24.35/4.02 | $i] : (start_time(v0) = v2 & critical_point(v0) = v1 & $i(v2) & % 24.35/4.02 | $i(v1) & greater_or_equal(v1, v2))) % 24.35/4.02 | % 24.35/4.02 | ALPHA: (mp_greater_or_equal) implies: % 24.35/4.02 | (9) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ greater(v0, v1) % 24.35/4.02 | | greater_or_equal(v0, v1)) % 24.35/4.02 | (10) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ % 24.35/4.02 | greater_or_equal(v0, v1) | greater(v0, v1)) % 24.35/4.02 | % 24.35/4.02 | ALPHA: (mp_beginning_and_ending) implies: % 24.35/4.02 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (start_time(v0) = v2) | % 24.35/4.03 | ~ $i(v1) | ~ $i(v0) | ~ greater(v1, v2) | ~ environment(v0) | ? % 24.35/4.03 | [v3: $i] : (end_time(v0) = v3 & $i(v3) & (greater_or_equal(v3, v1) | % 24.35/4.03 | greater(v1, v3)))) % 24.35/4.03 | % 24.35/4.03 | ALPHA: (l8) implies: % 24.35/4.03 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (critical_point(v0) = % 24.35/4.03 | v2) | ~ $i(v1) | ~ $i(v0) | ~ greater(v1, v2) | ~ % 24.35/4.03 | in_environment(v0, v1) | ~ environment(v0) | % 24.35/4.03 | selection_favors(efficient_producers, first_movers, v1)) % 24.35/4.03 | % 24.35/4.03 | ALPHA: (prove_t8) implies: % 24.35/4.03 | (13) ? [v0: $i] : ($i(v0) & slow_change(v0) & observational_period(v0) & % 24.35/4.03 | ~ selection_favors(efficient_producers, first_movers, v0)) % 24.35/4.03 | % 24.35/4.03 | ALPHA: (function-axioms) implies: % 25.09/4.03 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (end_time(v2) % 25.09/4.03 | = v1) | ~ (end_time(v2) = v0)) % 25.09/4.03 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 25.09/4.03 | (critical_point(v2) = v1) | ~ (critical_point(v2) = v0)) % 25.09/4.03 | % 25.09/4.03 | DELTA: instantiating (13) with fresh symbol all_14_0 gives: % 25.09/4.03 | (16) $i(all_14_0) & slow_change(all_14_0) & observational_period(all_14_0) % 25.09/4.03 | & ~ selection_favors(efficient_producers, first_movers, all_14_0) % 25.09/4.03 | % 25.09/4.03 | ALPHA: (16) implies: % 25.09/4.03 | (17) ~ selection_favors(efficient_producers, first_movers, all_14_0) % 25.09/4.03 | (18) observational_period(all_14_0) % 25.09/4.03 | (19) slow_change(all_14_0) % 25.09/4.03 | (20) $i(all_14_0) % 25.09/4.03 | % 25.09/4.03 | GROUND_INST: instantiating (1) with all_14_0, simplifying with (4), (5), (17), % 25.09/4.03 | (18), (20) gives: % 25.09/4.03 | (21) ? [v0: $i] : ? [v1: $i] : (end_time(v0) = v1 & $i(v1) & $i(v0) & % 25.09/4.03 | in_environment(all_14_0, v0) & environment(v0) & ~ % 25.09/4.03 | selection_favors(efficient_producers, first_movers, v1)) % 25.09/4.03 | % 25.09/4.03 | DELTA: instantiating (21) with fresh symbols all_25_0, all_25_1 gives: % 25.09/4.03 | (22) end_time(all_25_1) = all_25_0 & $i(all_25_0) & $i(all_25_1) & % 25.09/4.03 | in_environment(all_14_0, all_25_1) & environment(all_25_1) & ~ % 25.09/4.03 | selection_favors(efficient_producers, first_movers, all_25_0) % 25.09/4.03 | % 25.09/4.03 | ALPHA: (22) implies: % 25.09/4.04 | (23) ~ selection_favors(efficient_producers, first_movers, all_25_0) % 25.09/4.04 | (24) environment(all_25_1) % 25.09/4.04 | (25) in_environment(all_14_0, all_25_1) % 25.09/4.04 | (26) $i(all_25_1) % 25.09/4.04 | (27) end_time(all_25_1) = all_25_0 % 25.09/4.04 | % 25.09/4.04 | GROUND_INST: instantiating (8) with all_25_1, simplifying with (24), (26) % 25.09/4.04 | gives: % 25.09/4.04 | (28) ? [v0: $i] : ? [v1: $i] : (start_time(all_25_1) = v1 & % 25.09/4.04 | critical_point(all_25_1) = v0 & $i(v1) & $i(v0) & % 25.09/4.04 | greater_or_equal(v0, v1)) % 25.09/4.04 | % 25.09/4.04 | GROUND_INST: instantiating (2) with all_14_0, all_25_1, simplifying with (18), % 25.09/4.04 | (19), (20), (24), (25), (26) gives: % 25.09/4.04 | (29) ? [v0: $i] : ? [v1: $i] : (critical_point(all_25_1) = v0 & $i(v1) & % 25.09/4.04 | $i(v0) & greater(v1, v0) & in_environment(all_25_1, v1)) % 25.09/4.04 | % 25.09/4.04 | DELTA: instantiating (29) with fresh symbols all_32_0, all_32_1 gives: % 25.09/4.04 | (30) critical_point(all_25_1) = all_32_1 & $i(all_32_0) & $i(all_32_1) & % 25.09/4.04 | greater(all_32_0, all_32_1) & in_environment(all_25_1, all_32_0) % 25.09/4.04 | % 25.09/4.04 | ALPHA: (30) implies: % 25.09/4.04 | (31) in_environment(all_25_1, all_32_0) % 25.09/4.04 | (32) greater(all_32_0, all_32_1) % 25.09/4.04 | (33) $i(all_32_0) % 25.09/4.04 | (34) critical_point(all_25_1) = all_32_1 % 25.09/4.04 | % 25.09/4.04 | DELTA: instantiating (28) with fresh symbols all_34_0, all_34_1 gives: % 25.09/4.04 | (35) start_time(all_25_1) = all_34_0 & critical_point(all_25_1) = all_34_1 % 25.09/4.04 | & $i(all_34_0) & $i(all_34_1) & greater_or_equal(all_34_1, all_34_0) % 25.09/4.04 | % 25.09/4.04 | ALPHA: (35) implies: % 25.09/4.04 | (36) greater_or_equal(all_34_1, all_34_0) % 25.09/4.04 | (37) $i(all_34_1) % 25.09/4.04 | (38) $i(all_34_0) % 25.09/4.04 | (39) critical_point(all_25_1) = all_34_1 % 25.09/4.04 | (40) start_time(all_25_1) = all_34_0 % 25.09/4.04 | % 25.09/4.04 | GROUND_INST: instantiating (15) with all_32_1, all_34_1, all_25_1, simplifying % 25.09/4.04 | with (34), (39) gives: % 25.09/4.04 | (41) all_34_1 = all_32_1 % 25.09/4.04 | % 25.09/4.04 | REDUCE: (37), (41) imply: % 25.09/4.04 | (42) $i(all_32_1) % 25.09/4.04 | % 25.09/4.04 | REDUCE: (36), (41) imply: % 25.09/4.04 | (43) greater_or_equal(all_32_1, all_34_0) % 25.09/4.04 | % 25.09/4.04 | GROUND_INST: instantiating (7) with all_25_1, all_32_0, simplifying with (24), % 25.09/4.04 | (26), (31), (33) gives: % 25.09/4.04 | (44) ? [v0: $i] : (end_time(all_25_1) = v0 & $i(v0) & greater_or_equal(v0, % 25.09/4.04 | all_32_0)) % 25.09/4.04 | % 25.09/4.05 | GROUND_INST: instantiating (9) with all_32_0, all_32_1, simplifying with (32), % 25.09/4.05 | (33), (42) gives: % 25.09/4.05 | (45) greater_or_equal(all_32_0, all_32_1) % 25.09/4.05 | % 25.09/4.05 | GROUND_INST: instantiating (10) with all_32_1, all_34_0, simplifying with % 25.09/4.05 | (38), (42), (43) gives: % 25.09/4.05 | (46) all_34_0 = all_32_1 | greater(all_32_1, all_34_0) % 25.09/4.05 | % 25.09/4.05 | GROUND_INST: instantiating (3) with all_14_0, all_25_1, all_32_1, simplifying % 25.09/4.05 | with (18), (19), (20), (24), (25), (26), (34) gives: % 25.09/4.05 | (47) ? [v0: $i] : ($i(v0) & greater(v0, all_32_1) & % 25.09/4.05 | in_environment(all_25_1, v0)) % 25.09/4.05 | % 25.09/4.05 | GROUND_INST: instantiating (12) with all_25_1, all_32_0, all_32_1, simplifying % 25.09/4.05 | with (24), (26), (31), (32), (33), (34) gives: % 25.09/4.05 | (48) selection_favors(efficient_producers, first_movers, all_32_0) % 25.09/4.05 | % 25.09/4.05 | GROUND_INST: instantiating (6) with all_25_1, all_32_1, all_34_0, simplifying % 25.09/4.05 | with (24), (26), (40), (42), (43) gives: % 25.09/4.05 | (49) in_environment(all_25_1, all_32_1) | ? [v0: $i] : (end_time(all_25_1) % 25.09/4.05 | = v0 & $i(v0) & ~ greater_or_equal(v0, all_32_1)) % 25.09/4.05 | % 25.09/4.05 | DELTA: instantiating (44) with fresh symbol all_46_0 gives: % 25.09/4.05 | (50) end_time(all_25_1) = all_46_0 & $i(all_46_0) & % 25.09/4.05 | greater_or_equal(all_46_0, all_32_0) % 25.09/4.05 | % 25.09/4.05 | ALPHA: (50) implies: % 25.09/4.05 | (51) greater_or_equal(all_46_0, all_32_0) % 25.09/4.05 | (52) $i(all_46_0) % 25.09/4.05 | (53) end_time(all_25_1) = all_46_0 % 25.09/4.05 | % 25.09/4.05 | DELTA: instantiating (47) with fresh symbol all_48_0 gives: % 25.09/4.05 | (54) $i(all_48_0) & greater(all_48_0, all_32_1) & in_environment(all_25_1, % 25.09/4.05 | all_48_0) % 25.09/4.05 | % 25.09/4.05 | ALPHA: (54) implies: % 25.09/4.05 | (55) in_environment(all_25_1, all_48_0) % 25.09/4.05 | (56) $i(all_48_0) % 25.09/4.05 | % 25.09/4.05 | GROUND_INST: instantiating (14) with all_25_0, all_46_0, all_25_1, simplifying % 25.09/4.05 | with (27), (53) gives: % 25.09/4.05 | (57) all_46_0 = all_25_0 % 25.09/4.05 | % 25.09/4.05 | REDUCE: (52), (57) imply: % 25.09/4.05 | (58) $i(all_25_0) % 25.09/4.05 | % 25.09/4.05 | REDUCE: (51), (57) imply: % 25.09/4.05 | (59) greater_or_equal(all_25_0, all_32_0) % 25.09/4.05 | % 25.09/4.05 | GROUND_INST: instantiating (7) with all_25_1, all_48_0, simplifying with (24), % 25.09/4.05 | (26), (55), (56) gives: % 25.09/4.05 | (60) ? [v0: $i] : (end_time(all_25_1) = v0 & $i(v0) & greater_or_equal(v0, % 25.09/4.05 | all_48_0)) % 25.09/4.05 | % 25.09/4.05 | GROUND_INST: instantiating (10) with all_25_0, all_32_0, simplifying with % 25.09/4.05 | (33), (58), (59) gives: % 25.09/4.05 | (61) all_32_0 = all_25_0 | greater(all_25_0, all_32_0) % 25.09/4.05 | % 25.09/4.05 | DELTA: instantiating (60) with fresh symbol all_60_0 gives: % 25.09/4.05 | (62) end_time(all_25_1) = all_60_0 & $i(all_60_0) & % 25.09/4.05 | greater_or_equal(all_60_0, all_48_0) % 25.09/4.05 | % 25.09/4.06 | ALPHA: (62) implies: % 25.09/4.06 | (63) end_time(all_25_1) = all_60_0 % 25.09/4.06 | % 25.09/4.06 | GROUND_INST: instantiating (14) with all_25_0, all_60_0, all_25_1, simplifying % 25.09/4.06 | with (27), (63) gives: % 25.09/4.06 | (64) all_60_0 = all_25_0 % 25.09/4.06 | % 25.09/4.06 | BETA: splitting (49) gives: % 25.09/4.06 | % 25.09/4.06 | Case 1: % 25.09/4.06 | | % 25.09/4.06 | | (65) in_environment(all_25_1, all_32_1) % 25.09/4.06 | | % 25.09/4.06 | | GROUND_INST: instantiating (7) with all_25_1, all_32_1, simplifying with % 25.09/4.06 | | (24), (26), (42), (65) gives: % 25.09/4.06 | | (66) ? [v0: $i] : (end_time(all_25_1) = v0 & $i(v0) & % 25.09/4.06 | | greater_or_equal(v0, all_32_1)) % 25.09/4.06 | | % 25.09/4.06 | | DELTA: instantiating (66) with fresh symbol all_106_0 gives: % 25.09/4.06 | | (67) end_time(all_25_1) = all_106_0 & $i(all_106_0) & % 25.09/4.06 | | greater_or_equal(all_106_0, all_32_1) % 25.09/4.06 | | % 25.09/4.06 | | ALPHA: (67) implies: % 25.09/4.06 | | (68) greater_or_equal(all_106_0, all_32_1) % 25.09/4.06 | | (69) $i(all_106_0) % 25.09/4.06 | | (70) end_time(all_25_1) = all_106_0 % 25.09/4.06 | | % 25.09/4.06 | | GROUND_INST: instantiating (14) with all_25_0, all_106_0, all_25_1, % 25.09/4.06 | | simplifying with (27), (70) gives: % 25.09/4.06 | | (71) all_106_0 = all_25_0 % 25.09/4.06 | | % 25.09/4.06 | | REDUCE: (68), (71) imply: % 25.09/4.07 | | (72) greater_or_equal(all_25_0, all_32_1) % 25.09/4.07 | | % 25.09/4.07 | | BETA: splitting (46) gives: % 25.09/4.07 | | % 25.09/4.07 | | Case 1: % 25.09/4.07 | | | % 25.09/4.07 | | | (73) greater(all_32_1, all_34_0) % 25.09/4.07 | | | % 25.09/4.07 | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_32_0, % 25.09/4.07 | | | all_32_1, all_34_0, simplifying with (32), (33), (38), (42), % 25.09/4.07 | | | (73) gives: % 25.09/4.07 | | | (74) greater(all_32_0, all_34_0) % 25.09/4.07 | | | % 25.09/4.07 | | | BETA: splitting (61) gives: % 25.09/4.07 | | | % 25.09/4.07 | | | Case 1: % 25.09/4.07 | | | | % 25.09/4.07 | | | | (75) greater(all_25_0, all_32_0) % 25.09/4.07 | | | | % 25.09/4.07 | | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_25_0, % 25.09/4.07 | | | | all_32_0, all_34_0, simplifying with (33), (38), (58), % 25.09/4.07 | | | | (74), (75) gives: % 25.09/4.07 | | | | (76) greater(all_25_0, all_34_0) % 25.09/4.07 | | | | % 25.09/4.07 | | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_25_0, % 25.09/4.07 | | | | all_32_0, all_32_1, simplifying with (32), (33), (42), % 25.09/4.07 | | | | (58), (75) gives: % 25.09/4.07 | | | | (77) greater(all_25_0, all_32_1) % 25.09/4.07 | | | | % 25.09/4.07 | | | | GROUND_INST: instantiating (11) with all_25_1, all_25_0, all_34_0, % 25.09/4.07 | | | | simplifying with (24), (26), (40), (58), (76) gives: % 25.09/4.07 | | | | (78) ? [v0: $i] : (end_time(all_25_1) = v0 & $i(v0) & % 25.09/4.07 | | | | (greater_or_equal(v0, all_25_0) | greater(all_25_0, v0))) % 25.09/4.07 | | | | % 25.09/4.07 | | | | GROUND_INST: instantiating (9) with all_25_0, all_34_0, simplifying with % 25.09/4.07 | | | | (38), (58), (76) gives: % 25.09/4.07 | | | | (79) greater_or_equal(all_25_0, all_34_0) % 25.09/4.07 | | | | % 25.09/4.07 | | | | DELTA: instantiating (78) with fresh symbol all_150_0 gives: % 25.09/4.07 | | | | (80) end_time(all_25_1) = all_150_0 & $i(all_150_0) & % 25.09/4.07 | | | | (greater_or_equal(all_150_0, all_25_0) | greater(all_25_0, % 25.09/4.07 | | | | all_150_0)) % 25.09/4.07 | | | | % 25.09/4.07 | | | | ALPHA: (80) implies: % 25.09/4.07 | | | | (81) $i(all_150_0) % 25.09/4.07 | | | | (82) end_time(all_25_1) = all_150_0 % 25.09/4.07 | | | | (83) greater_or_equal(all_150_0, all_25_0) | greater(all_25_0, % 25.09/4.07 | | | | all_150_0) % 25.09/4.07 | | | | % 25.09/4.07 | | | | GROUND_INST: instantiating (14) with all_25_0, all_150_0, all_25_1, % 25.09/4.07 | | | | simplifying with (27), (82) gives: % 25.09/4.07 | | | | (84) all_150_0 = all_25_0 % 25.09/4.07 | | | | % 25.09/4.07 | | | | GROUND_INST: instantiating (6) with all_25_1, all_25_0, all_34_0, % 25.09/4.07 | | | | simplifying with (24), (26), (40), (58), (79) gives: % 25.09/4.07 | | | | (85) in_environment(all_25_1, all_25_0) | ? [v0: $i] : % 25.09/4.07 | | | | (end_time(all_25_1) = v0 & $i(v0) & ~ greater_or_equal(v0, % 25.09/4.07 | | | | all_25_0)) % 25.09/4.07 | | | | % 25.09/4.07 | | | | BETA: splitting (83) gives: % 25.09/4.07 | | | | % 25.09/4.07 | | | | Case 1: % 25.09/4.07 | | | | | % 25.09/4.07 | | | | | (86) greater_or_equal(all_150_0, all_25_0) % 25.09/4.07 | | | | | % 25.09/4.07 | | | | | REDUCE: (84), (86) imply: % 25.09/4.07 | | | | | (87) greater_or_equal(all_25_0, all_25_0) % 25.09/4.07 | | | | | % 25.09/4.07 | | | | | BETA: splitting (85) gives: % 25.09/4.07 | | | | | % 25.09/4.07 | | | | | Case 1: % 25.09/4.07 | | | | | | % 25.09/4.07 | | | | | | (88) in_environment(all_25_1, all_25_0) % 25.09/4.07 | | | | | | % 25.09/4.07 | | | | | | GROUND_INST: instantiating (12) with all_25_1, all_25_0, all_32_1, % 25.09/4.07 | | | | | | simplifying with (23), (24), (26), (34), (58), (77), % 25.09/4.07 | | | | | | (88) gives: % 25.09/4.07 | | | | | | (89) $false % 25.09/4.08 | | | | | | % 25.09/4.08 | | | | | | CLOSE: (89) is inconsistent. % 25.09/4.08 | | | | | | % 25.09/4.08 | | | | | Case 2: % 25.09/4.08 | | | | | | % 25.09/4.08 | | | | | | (90) ? [v0: $i] : (end_time(all_25_1) = v0 & $i(v0) & ~ % 25.09/4.08 | | | | | | greater_or_equal(v0, all_25_0)) % 25.09/4.08 | | | | | | % 25.09/4.08 | | | | | | DELTA: instantiating (90) with fresh symbol all_225_0 gives: % 25.09/4.08 | | | | | | (91) end_time(all_25_1) = all_225_0 & $i(all_225_0) & ~ % 25.09/4.08 | | | | | | greater_or_equal(all_225_0, all_25_0) % 25.09/4.08 | | | | | | % 25.09/4.08 | | | | | | ALPHA: (91) implies: % 25.09/4.08 | | | | | | (92) ~ greater_or_equal(all_225_0, all_25_0) % 25.09/4.08 | | | | | | (93) end_time(all_25_1) = all_225_0 % 25.09/4.08 | | | | | | % 25.09/4.08 | | | | | | GROUND_INST: instantiating (14) with all_25_0, all_225_0, all_25_1, % 25.09/4.08 | | | | | | simplifying with (27), (93) gives: % 25.09/4.08 | | | | | | (94) all_225_0 = all_25_0 % 25.09/4.08 | | | | | | % 25.09/4.08 | | | | | | REDUCE: (92), (94) imply: % 25.09/4.08 | | | | | | (95) ~ greater_or_equal(all_25_0, all_25_0) % 25.09/4.08 | | | | | | % 25.09/4.08 | | | | | | PRED_UNIFY: (87), (95) imply: % 25.09/4.08 | | | | | | (96) $false % 25.09/4.08 | | | | | | % 25.09/4.08 | | | | | | CLOSE: (96) is inconsistent. % 25.09/4.08 | | | | | | % 25.09/4.08 | | | | | End of split % 25.09/4.08 | | | | | % 25.09/4.08 | | | | Case 2: % 25.09/4.08 | | | | | % 25.09/4.08 | | | | | (97) ~ greater_or_equal(all_150_0, all_25_0) % 25.09/4.08 | | | | | (98) greater(all_25_0, all_150_0) % 25.09/4.08 | | | | | % 25.09/4.08 | | | | | REDUCE: (84), (98) imply: % 25.09/4.08 | | | | | (99) greater(all_25_0, all_25_0) % 25.09/4.08 | | | | | % 25.09/4.08 | | | | | REDUCE: (84), (97) imply: % 25.09/4.08 | | | | | (100) ~ greater_or_equal(all_25_0, all_25_0) % 25.09/4.08 | | | | | % 25.09/4.08 | | | | | GROUND_INST: instantiating (9) with all_25_0, all_25_0, simplifying % 25.09/4.08 | | | | | with (58), (99), (100) gives: % 25.09/4.08 | | | | | (101) $false % 25.09/4.08 | | | | | % 25.09/4.08 | | | | | CLOSE: (101) is inconsistent. % 25.09/4.08 | | | | | % 25.09/4.08 | | | | End of split % 25.09/4.08 | | | | % 25.09/4.08 | | | Case 2: % 25.09/4.08 | | | | % 25.09/4.08 | | | | (102) all_32_0 = all_25_0 % 25.09/4.08 | | | | % 25.09/4.08 | | | | REDUCE: (48), (102) imply: % 25.09/4.08 | | | | (103) selection_favors(efficient_producers, first_movers, all_25_0) % 25.09/4.08 | | | | % 25.09/4.08 | | | | PRED_UNIFY: (23), (103) imply: % 25.09/4.08 | | | | (104) $false % 25.09/4.08 | | | | % 25.09/4.08 | | | | CLOSE: (104) is inconsistent. % 25.09/4.08 | | | | % 25.09/4.08 | | | End of split % 25.09/4.08 | | | % 25.09/4.08 | | Case 2: % 25.09/4.08 | | | % 25.09/4.08 | | | (105) all_34_0 = all_32_1 % 25.09/4.08 | | | % 25.09/4.08 | | | REDUCE: (40), (105) imply: % 25.09/4.08 | | | (106) start_time(all_25_1) = all_32_1 % 25.09/4.08 | | | % 25.09/4.08 | | | GROUND_INST: instantiating (6) with all_25_1, all_25_0, all_32_1, % 25.09/4.08 | | | simplifying with (24), (26), (58), (72), (106) gives: % 25.09/4.08 | | | (107) in_environment(all_25_1, all_25_0) | ? [v0: $i] : % 25.09/4.08 | | | (end_time(all_25_1) = v0 & $i(v0) & ~ greater_or_equal(v0, % 25.09/4.08 | | | all_25_0)) % 25.09/4.08 | | | % 25.09/4.08 | | | BETA: splitting (61) gives: % 25.09/4.08 | | | % 25.09/4.08 | | | Case 1: % 25.09/4.08 | | | | % 25.09/4.08 | | | | (108) greater(all_25_0, all_32_0) % 25.09/4.08 | | | | % 25.09/4.08 | | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_25_0, % 25.09/4.08 | | | | all_32_0, all_32_1, simplifying with (32), (33), (42), % 25.09/4.08 | | | | (58), (108) gives: % 25.09/4.08 | | | | (109) greater(all_25_0, all_32_1) % 25.09/4.08 | | | | % 25.09/4.09 | | | | GROUND_INST: instantiating (11) with all_25_1, all_25_0, all_32_1, % 25.09/4.09 | | | | simplifying with (24), (26), (58), (106), (109) gives: % 25.09/4.09 | | | | (110) ? [v0: $i] : (end_time(all_25_1) = v0 & $i(v0) & % 25.09/4.09 | | | | (greater_or_equal(v0, all_25_0) | greater(all_25_0, v0))) % 25.09/4.09 | | | | % 25.09/4.09 | | | | DELTA: instantiating (110) with fresh symbol all_137_0 gives: % 25.09/4.09 | | | | (111) end_time(all_25_1) = all_137_0 & $i(all_137_0) & % 25.09/4.09 | | | | (greater_or_equal(all_137_0, all_25_0) | greater(all_25_0, % 25.09/4.09 | | | | all_137_0)) % 25.09/4.09 | | | | % 25.09/4.09 | | | | ALPHA: (111) implies: % 25.09/4.09 | | | | (112) $i(all_137_0) % 25.09/4.09 | | | | (113) end_time(all_25_1) = all_137_0 % 25.09/4.09 | | | | (114) greater_or_equal(all_137_0, all_25_0) | greater(all_25_0, % 25.09/4.09 | | | | all_137_0) % 25.09/4.09 | | | | % 25.09/4.09 | | | | GROUND_INST: instantiating (14) with all_25_0, all_137_0, all_25_1, % 25.09/4.09 | | | | simplifying with (27), (113) gives: % 25.09/4.09 | | | | (115) all_137_0 = all_25_0 % 25.09/4.09 | | | | % 25.09/4.09 | | | | BETA: splitting (107) gives: % 25.09/4.09 | | | | % 25.09/4.09 | | | | Case 1: % 25.09/4.09 | | | | | % 25.09/4.09 | | | | | (116) in_environment(all_25_1, all_25_0) % 25.09/4.09 | | | | | % 25.09/4.09 | | | | | GROUND_INST: instantiating (12) with all_25_1, all_25_0, all_32_1, % 25.09/4.09 | | | | | simplifying with (23), (24), (26), (34), (58), (109), % 25.09/4.09 | | | | | (116) gives: % 25.09/4.09 | | | | | (117) $false % 25.09/4.09 | | | | | % 25.09/4.09 | | | | | CLOSE: (117) is inconsistent. % 25.09/4.09 | | | | | % 25.09/4.09 | | | | Case 2: % 25.09/4.09 | | | | | % 25.09/4.09 | | | | | (118) ? [v0: $i] : (end_time(all_25_1) = v0 & $i(v0) & ~ % 25.09/4.09 | | | | | greater_or_equal(v0, all_25_0)) % 25.09/4.09 | | | | | % 25.09/4.09 | | | | | DELTA: instantiating (118) with fresh symbol all_164_0 gives: % 25.09/4.09 | | | | | (119) end_time(all_25_1) = all_164_0 & $i(all_164_0) & ~ % 25.09/4.09 | | | | | greater_or_equal(all_164_0, all_25_0) % 25.09/4.09 | | | | | % 25.09/4.09 | | | | | ALPHA: (119) implies: % 25.09/4.09 | | | | | (120) ~ greater_or_equal(all_164_0, all_25_0) % 25.09/4.09 | | | | | (121) $i(all_164_0) % 25.09/4.09 | | | | | (122) end_time(all_25_1) = all_164_0 % 25.09/4.09 | | | | | % 25.09/4.09 | | | | | GROUND_INST: instantiating (14) with all_25_0, all_164_0, all_25_1, % 25.09/4.09 | | | | | simplifying with (27), (122) gives: % 25.09/4.09 | | | | | (123) all_164_0 = all_25_0 % 25.09/4.09 | | | | | % 25.09/4.09 | | | | | REDUCE: (120), (123) imply: % 25.09/4.09 | | | | | (124) ~ greater_or_equal(all_25_0, all_25_0) % 25.09/4.09 | | | | | % 25.09/4.09 | | | | | BETA: splitting (114) gives: % 25.09/4.09 | | | | | % 25.09/4.09 | | | | | Case 1: % 25.09/4.09 | | | | | | % 25.09/4.09 | | | | | | (125) greater_or_equal(all_137_0, all_25_0) % 25.09/4.09 | | | | | | % 25.09/4.09 | | | | | | REDUCE: (115), (125) imply: % 25.09/4.09 | | | | | | (126) greater_or_equal(all_25_0, all_25_0) % 25.09/4.09 | | | | | | % 25.09/4.09 | | | | | | PRED_UNIFY: (124), (126) imply: % 25.09/4.09 | | | | | | (127) $false % 25.09/4.09 | | | | | | % 25.09/4.09 | | | | | | CLOSE: (127) is inconsistent. % 25.09/4.09 | | | | | | % 25.09/4.09 | | | | | Case 2: % 25.09/4.09 | | | | | | % 25.09/4.09 | | | | | | (128) ~ greater_or_equal(all_137_0, all_25_0) % 25.09/4.09 | | | | | | (129) greater(all_25_0, all_137_0) % 25.09/4.09 | | | | | | % 25.09/4.09 | | | | | | REDUCE: (115), (129) imply: % 25.09/4.09 | | | | | | (130) greater(all_25_0, all_25_0) % 25.09/4.09 | | | | | | % 25.09/4.09 | | | | | | GROUND_INST: instantiating (9) with all_25_0, all_25_0, simplifying % 25.09/4.09 | | | | | | with (58), (124), (130) gives: % 25.09/4.09 | | | | | | (131) $false % 25.09/4.09 | | | | | | % 25.09/4.09 | | | | | | CLOSE: (131) is inconsistent. % 25.09/4.09 | | | | | | % 25.09/4.09 | | | | | End of split % 25.09/4.09 | | | | | % 25.09/4.09 | | | | End of split % 25.09/4.09 | | | | % 25.09/4.09 | | | Case 2: % 25.09/4.09 | | | | % 25.09/4.09 | | | | (132) all_32_0 = all_25_0 % 25.09/4.09 | | | | % 25.09/4.09 | | | | REDUCE: (48), (132) imply: % 25.09/4.09 | | | | (133) selection_favors(efficient_producers, first_movers, all_25_0) % 25.09/4.09 | | | | % 25.09/4.09 | | | | PRED_UNIFY: (23), (133) imply: % 25.09/4.09 | | | | (134) $false % 25.09/4.10 | | | | % 25.09/4.10 | | | | CLOSE: (134) is inconsistent. % 25.09/4.10 | | | | % 25.09/4.10 | | | End of split % 25.09/4.10 | | | % 25.09/4.10 | | End of split % 25.09/4.10 | | % 25.09/4.10 | Case 2: % 25.09/4.10 | | % 25.09/4.10 | | (135) ? [v0: $i] : (end_time(all_25_1) = v0 & $i(v0) & ~ % 25.09/4.10 | | greater_or_equal(v0, all_32_1)) % 25.09/4.10 | | % 25.09/4.10 | | DELTA: instantiating (135) with fresh symbol all_100_0 gives: % 25.09/4.10 | | (136) end_time(all_25_1) = all_100_0 & $i(all_100_0) & ~ % 25.09/4.10 | | greater_or_equal(all_100_0, all_32_1) % 25.09/4.10 | | % 25.09/4.10 | | ALPHA: (136) implies: % 25.09/4.10 | | (137) end_time(all_25_1) = all_100_0 % 25.09/4.10 | | (138) $i(all_100_0) % 25.09/4.10 | | (139) ~ greater_or_equal(all_100_0, all_32_1) % 25.09/4.10 | | % 25.09/4.10 | | GROUND_INST: instantiating (14) with all_25_0, all_100_0, all_25_1, % 25.09/4.10 | | simplifying with (27), (137) gives: % 25.09/4.10 | | (140) all_100_0 = all_25_0 % 25.09/4.10 | | % 25.09/4.10 | | REDUCE: (139), (140) imply: % 25.09/4.10 | | (141) ~ greater_or_equal(all_25_0, all_32_1) % 25.09/4.10 | | % 25.09/4.10 | | BETA: splitting (61) gives: % 25.09/4.10 | | % 25.09/4.10 | | Case 1: % 25.09/4.10 | | | % 25.09/4.10 | | | (142) greater(all_25_0, all_32_0) % 25.09/4.10 | | | % 25.09/4.10 | | | GROUND_INST: instantiating (mp_greater_transitivity) with all_25_0, % 25.09/4.10 | | | all_32_0, all_32_1, simplifying with (32), (33), (42), (58), % 25.09/4.10 | | | (142) gives: % 25.09/4.10 | | | (143) greater(all_25_0, all_32_1) % 25.09/4.10 | | | % 25.09/4.10 | | | GROUND_INST: instantiating (9) with all_25_0, all_32_1, simplifying with % 25.09/4.10 | | | (42), (58), (141), (143) gives: % 25.09/4.10 | | | (144) $false % 25.09/4.10 | | | % 25.09/4.10 | | | CLOSE: (144) is inconsistent. % 25.09/4.10 | | | % 25.09/4.10 | | Case 2: % 25.09/4.10 | | | % 25.09/4.10 | | | (145) all_32_0 = all_25_0 % 25.09/4.10 | | | % 25.09/4.10 | | | REDUCE: (45), (145) imply: % 25.09/4.10 | | | (146) greater_or_equal(all_25_0, all_32_1) % 25.09/4.10 | | | % 25.09/4.10 | | | PRED_UNIFY: (141), (146) imply: % 25.09/4.10 | | | (147) $false % 25.09/4.10 | | | % 25.09/4.10 | | | CLOSE: (147) is inconsistent. % 25.09/4.10 | | | % 25.09/4.10 | | End of split % 25.09/4.10 | | % 25.09/4.10 | End of split % 25.09/4.10 | % 25.09/4.10 End of proof % 25.09/4.10 % SZS output end Proof for theBenchmark % 25.09/4.10 % 25.09/4.10 3371ms %------------------------------------------------------------------------------