Metis---2.4.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : MGT033-2 : TPTP v9.3.0. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %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:15:45 AM UTC 2026

% Result   : Satisfiable 0.56s 0.85s
% Output   : Saturation 0.66s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : MGT033-2 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03  % Command  : metis --show proof --show saturation %s
% 0.09/0.35  % Computer : n004.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:27:00 UTC 2026
% 0.13/0.36  % CPUTime  : 
% 0.13/0.36  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.56/0.85  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.56/0.85  
% 0.56/0.85  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.56/0.85  |- ~(cardinality_at_time $D $C = zero) \/ ~environment $A \/
% 0.56/0.85     ~greater (cardinality_at_time $B $C) zero \/ ~subpopulation $B $A $C \/
% 0.56/0.85     ~subpopulation $D $A $C \/ selection_favors $B $D $C
% 0.56/0.85  |- ~environment $A \/ ~greater (number_of_organizations $A $B) zero \/
% 0.56/0.85     subpopulation (sk1 $B $A) $A $B
% 0.56/0.85  |- ~environment $A \/ ~greater (number_of_organizations $A $B) zero \/
% 0.56/0.85     greater (cardinality_at_time (sk1 $B $A) $B) zero
% 0.56/0.85  |- ~(cardinality_at_time $A t = zero) \/
% 0.56/0.85     ~greater (cardinality_at_time $A $B) zero
% 0.56/0.85  |- ~environment $A \/ ~greater (appear $C $A) $B \/
% 0.56/0.85     ~in_environment $A $B \/ cardinality_at_time $C $B = zero
% 0.56/0.85  |- ~environment $A \/ ~greater (number_of_organizations $A $B) zero \/
% 0.56/0.85     in_environment $A $B
% 0.56/0.85  |- ~environment $A \/ ~greater_or_equal $C $D \/ ~greater_or_equal $D $B \/
% 0.56/0.85     ~in_environment $A $B \/ ~in_environment $A $C \/ in_environment $A $D
% 0.56/0.85  |- ~environment $A \/ in_environment $A (start_time $A)
% 0.56/0.85  |- ~environment $A \/
% 0.56/0.85     greater_or_equal (appear first_movers $A) (start_time $A)
% 0.56/0.85  |- ~environment $A \/ ~in_environment $A (appear first_movers $A) \/
% 0.56/0.85     in_environment $A (appear an_organisation $A)
% 0.56/0.85  |- ~environment $A \/
% 0.56/0.85     greater_or_equal (appear first_movers $A) (appear an_organisation $A)
% 0.56/0.85  |- ~environment $A \/
% 0.56/0.85     greater (number_of_organizations e (appear an_organisation $A)) zero
% 0.56/0.85  |- ~environment $A \/ ~in_environment $A $B \/
% 0.56/0.85     subpopulation first_movers $A $B
% 0.56/0.85  |- ~environment $A \/ ~in_environment $A $B \/
% 0.56/0.85     subpopulation efficient_producers $A $B
% 0.56/0.85  |- ~greater $A $B \/ ~greater $B $C \/ greater $A $C
% 0.56/0.85  |- ~greater_or_equal $A $B \/ $A = $B \/ greater $A $B
% 0.56/0.85  |- ~greater $A $B \/ greater_or_equal $A $B
% 0.56/0.85  |- greater_or_equal $B $B
% 0.56/0.85  |- ~environment $A \/ ~greater_or_equal $B (appear an_organisation $A) \/
% 0.56/0.85     ~in_environment $A $B \/ greater (number_of_organizations $A $B) zero
% 0.56/0.85  |- ~environment $A \/
% 0.56/0.85     greater (appear efficient_producers e) (appear first_movers $A)
% 0.56/0.85  |- ~environment $A \/ ~greater (cardinality_at_time $B $C) zero \/
% 0.56/0.85     ~subpopulation $B $A $C \/ $B = efficient_producers \/ $B = first_movers
% 0.56/0.85  |- ~(cardinality_at_time $D $C = zero) \/ ~environment $A \/
% 0.56/0.85     ~greater zero zero \/ ~subpopulation $D $A $C \/
% 0.56/0.85     selection_favors $D $D $C
% 0.56/0.85  |- ~environment $A \/ ~greater_or_equal $C $D \/ ~greater_or_equal $D $C \/
% 0.56/0.85     ~in_environment $A $C \/ in_environment $A $D
% 0.56/0.85  |- environment sk2
% 0.56/0.85  |- in_environment sk2 sk3
% 0.56/0.85  |- greater_or_equal sk3 (appear first_movers sk2)
% 0.56/0.85  |- greater (appear efficient_producers sk2) sk3
% 0.56/0.85  |- ~selection_favors first_movers efficient_producers sk3
% 0.56/0.85  |- in_environment sk2 (start_time sk2)
% 0.56/0.85  |- greater_or_equal (appear first_movers sk2) (start_time sk2)
% 0.56/0.85  |- greater (appear efficient_producers e) (appear first_movers sk2)
% 0.56/0.85  |- greater_or_equal (appear first_movers sk2) (appear an_organisation sk2)
% 0.56/0.85  |- greater (number_of_organizations e (appear an_organisation sk2)) zero
% 0.56/0.85  |- greater_or_equal (appear efficient_producers e)
% 0.56/0.85       (appear first_movers sk2)
% 0.56/0.85  |- greater_or_equal (appear efficient_producers sk2) sk3
% 0.56/0.85  |- greater_or_equal
% 0.56/0.85       (number_of_organizations e (appear an_organisation sk2)) zero
% 0.56/0.85  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.85     greater (appear first_movers sk2) (appear an_organisation sk2)
% 0.56/0.85  |- appear first_movers sk2 = start_time sk2 \/
% 0.56/0.85     greater (appear first_movers sk2) (start_time sk2)
% 0.56/0.85  |- sk3 = appear first_movers sk2 \/ greater sk3 (appear first_movers sk2)
% 0.56/0.85  |- subpopulation first_movers sk2 sk3
% 0.56/0.85  |- subpopulation first_movers sk2 (start_time sk2)
% 0.56/0.85  |- subpopulation efficient_producers sk2 sk3
% 0.56/0.86  |- subpopulation efficient_producers sk2 (start_time sk2)
% 0.56/0.86  |- ~environment e \/ in_environment e (appear an_organisation sk2)
% 0.56/0.86  |- ~greater (appear first_movers sk2) $_21 \/
% 0.56/0.86     greater (appear efficient_producers e) $_21
% 0.56/0.86  |- ~greater sk3 $_21 \/ greater (appear efficient_producers sk2) $_21
% 0.56/0.86  |- ~greater (appear an_organisation sk2) $_21 \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     greater (appear first_movers sk2) $_21
% 0.56/0.86  |- ~greater (start_time sk2) $_21 \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     greater (appear first_movers sk2) $_21
% 0.56/0.86  |- ~greater zero $_21 \/
% 0.56/0.86     greater (number_of_organizations e (appear an_organisation sk2)) $_21
% 0.56/0.86  |- ~greater $_19 (appear efficient_producers e) \/
% 0.56/0.86     greater $_19 (appear first_movers sk2)
% 0.56/0.86  |- ~greater $_19 (appear efficient_producers sk2) \/ greater $_19 sk3
% 0.56/0.86  |- ~greater $_19 (appear first_movers sk2) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     greater $_19 (appear an_organisation sk2)
% 0.56/0.86  |- ~greater $_19 (appear first_movers sk2) \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     greater $_19 (start_time sk2)
% 0.56/0.86  |- ~greater $_19
% 0.56/0.86        (number_of_organizations e (appear an_organisation sk2)) \/
% 0.56/0.86     greater $_19 zero
% 0.56/0.86  |- ~greater $_19 sk3 \/ sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater $_19 (appear first_movers sk2)
% 0.56/0.86  |- sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (appear efficient_producers sk2) (appear first_movers sk2)
% 0.56/0.86  |- ~greater $A (appear efficient_producers sk2) \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ greater $A (appear first_movers sk2)
% 0.56/0.86  |- ~greater (appear first_movers sk2) $C \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (appear efficient_producers sk2) $C
% 0.56/0.86  |- sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater_or_equal (appear efficient_producers sk2)
% 0.56/0.86       (appear first_movers sk2)
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     greater (appear efficient_producers e) (appear an_organisation sk2)
% 0.56/0.86  |- appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     greater (appear efficient_producers e) (start_time sk2)
% 0.56/0.86  |- ~greater $A (appear efficient_producers e) \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/ greater $A (start_time sk2)
% 0.56/0.86  |- ~greater (start_time sk2) $C \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     greater (appear efficient_producers e) $C
% 0.56/0.86  |- appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     greater_or_equal (appear efficient_producers e) (start_time sk2)
% 0.56/0.86  |- ~greater $A (appear efficient_producers e) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     greater $A (appear an_organisation sk2)
% 0.56/0.86  |- ~greater (appear an_organisation sk2) $C \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     greater (appear efficient_producers e) $C
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     greater_or_equal (appear efficient_producers e)
% 0.56/0.86       (appear an_organisation sk2)
% 0.56/0.86  |- ~environment e \/
% 0.56/0.86     subpopulation (sk1 (appear an_organisation sk2) e) e
% 0.56/0.86       (appear an_organisation sk2)
% 0.56/0.86  |- appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (appear efficient_producers sk2) (start_time sk2)
% 0.56/0.86  |- appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ greater sk3 (start_time sk2)
% 0.56/0.86  |- ~greater $A sk3 \/ appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ greater $A (start_time sk2)
% 0.56/0.86  |- appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ greater_or_equal sk3 (start_time sk2)
% 0.56/0.86  |- ~greater $A (appear efficient_producers sk2) \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ greater $A (start_time sk2)
% 0.56/0.86  |- ~greater (start_time sk2) $C \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (appear efficient_producers sk2) $C
% 0.56/0.86  |- appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater_or_equal (appear efficient_producers sk2) (start_time sk2)
% 0.56/0.86  |- ~environment e \/
% 0.56/0.86     greater
% 0.56/0.86       (cardinality_at_time (sk1 (appear an_organisation sk2) e)
% 0.56/0.86          (appear an_organisation sk2)) zero
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (appear efficient_producers sk2) (appear an_organisation sk2)
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater sk3 (appear an_organisation sk2)
% 0.56/0.86  |- ~greater $A sk3 \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ greater $A (appear an_organisation sk2)
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater_or_equal sk3 (appear an_organisation sk2)
% 0.56/0.86  |- ~greater $A (appear efficient_producers sk2) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ greater $A (appear an_organisation sk2)
% 0.56/0.86  |- ~greater (appear an_organisation sk2) $C \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (appear efficient_producers sk2) $C
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater_or_equal (appear efficient_producers sk2)
% 0.56/0.86       (appear an_organisation sk2)
% 0.56/0.86  |- ~in_environment sk2 (appear efficient_producers e) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     greater (number_of_organizations sk2 (appear efficient_producers e))
% 0.56/0.86       zero
% 0.56/0.86  |- ~in_environment sk2 (appear efficient_producers sk2) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (number_of_organizations sk2 (appear efficient_producers sk2))
% 0.56/0.86       zero
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (number_of_organizations sk2 sk3) zero
% 0.56/0.86  |- ~environment $_41 \/
% 0.56/0.86     ~in_environment $_41 (appear an_organisation $_41) \/
% 0.56/0.86     greater (number_of_organizations $_41 (appear an_organisation $_41))
% 0.56/0.86       zero
% 0.56/0.86  |- ~greater $A (number_of_organizations sk2 sk3) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ greater $A zero
% 0.56/0.86  |- ~greater zero $C \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (number_of_organizations sk2 sk3) $C
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater_or_equal (number_of_organizations sk2 sk3) zero
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (cardinality_at_time (sk1 sk3 sk2) sk3) zero
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ subpopulation (sk1 sk3 sk2) sk2 sk3
% 0.56/0.86  |- ~greater $A (cardinality_at_time (sk1 sk3 sk2) sk3) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ greater $A zero
% 0.56/0.86  |- ~greater zero $C \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater (cardinality_at_time (sk1 sk3 sk2) sk3) $C
% 0.56/0.86  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     greater_or_equal (cardinality_at_time (sk1 sk3 sk2) sk3) zero
% 0.56/0.86  |- ~(cardinality_at_time (sk1 sk3 sk2) t = zero) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2
% 0.56/0.86  |- ~environment e \/ ~in_environment e (appear an_organisation sk2) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.56/0.86     zero
% 0.56/0.86  |- ~environment e \/ ~in_environment e (appear first_movers sk2) \/
% 0.56/0.86     cardinality_at_time efficient_producers (appear first_movers sk2) = zero
% 0.56/0.86  |- ~environment e \/ ~in_environment e (start_time sk2) \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     cardinality_at_time efficient_producers (start_time sk2) = zero
% 0.56/0.86  |- cardinality_at_time efficient_producers sk3 = zero
% 0.56/0.86  |- appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     cardinality_at_time efficient_producers (start_time sk2) = zero \/
% 0.56/0.86     sk3 = appear first_movers sk2
% 0.56/0.86  |- appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     cardinality_at_time first_movers (start_time sk2) = zero
% 0.56/0.86  |- ~(cardinality_at_time efficient_producers t = zero) \/
% 0.56/0.86     ~greater zero zero
% 0.56/0.86  |- ~(cardinality_at_time first_movers t = zero) \/ ~greater zero zero \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (appear an_organisation sk2)
% 0.56/0.86        (appear efficient_producers e) \/
% 0.56/0.86     ~in_environment $_51 (appear efficient_producers e) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     in_environment $_51 (appear an_organisation sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (start_time sk2) (appear efficient_producers e) \/
% 0.56/0.86     ~in_environment $_51 (appear efficient_producers e) \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     in_environment $_51 (start_time sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (appear an_organisation sk2)
% 0.56/0.86        (appear efficient_producers sk2) \/
% 0.56/0.86     ~in_environment $_51 (appear efficient_producers sk2) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     in_environment $_51 (appear an_organisation sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (start_time sk2) (appear efficient_producers sk2) \/
% 0.56/0.86     ~in_environment $_51 (appear efficient_producers sk2) \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/ in_environment $_51 (start_time sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (appear an_organisation sk2)
% 0.56/0.86        (appear first_movers sk2) \/
% 0.56/0.86     ~in_environment $_51 (appear first_movers sk2) \/
% 0.56/0.86     in_environment $_51 (appear an_organisation sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (start_time sk2) (appear first_movers sk2) \/
% 0.56/0.86     ~in_environment $_51 (appear first_movers sk2) \/
% 0.56/0.86     in_environment $_51 (start_time sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (appear an_organisation sk2)
% 0.56/0.86        (appear efficient_producers e) \/
% 0.56/0.86     ~in_environment $_51 (appear an_organisation sk2) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     in_environment $_51 (appear efficient_producers e)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (start_time sk2) (appear efficient_producers e) \/
% 0.56/0.86     ~in_environment $_51 (start_time sk2) \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     in_environment $_51 (appear efficient_producers e)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (appear an_organisation sk2)
% 0.56/0.86        (appear efficient_producers sk2) \/
% 0.56/0.86     ~in_environment $_51 (appear an_organisation sk2) \/
% 0.56/0.86     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     in_environment $_51 (appear efficient_producers sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal sk3 (appear efficient_producers sk2) \/
% 0.56/0.86     ~in_environment $_51 sk3 \/
% 0.56/0.86     in_environment $_51 (appear efficient_producers sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (start_time sk2) (appear efficient_producers sk2) \/
% 0.56/0.86     ~in_environment $_51 (start_time sk2) \/
% 0.56/0.86     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.86     sk3 = appear first_movers sk2 \/
% 0.56/0.86     in_environment $_51 (appear efficient_producers sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (appear an_organisation sk2)
% 0.56/0.86        (appear first_movers sk2) \/
% 0.56/0.86     ~in_environment $_51 (appear an_organisation sk2) \/
% 0.56/0.86     in_environment $_51 (appear first_movers sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal (start_time sk2) (appear first_movers sk2) \/
% 0.56/0.86     ~in_environment $_51 (start_time sk2) \/
% 0.56/0.86     in_environment $_51 (appear first_movers sk2)
% 0.56/0.86  |- ~environment $_51 \/
% 0.56/0.86     ~greater_or_equal zero
% 0.56/0.86        (number_of_organizations e (appear an_organisation sk2)) \/
% 0.56/0.86     ~in_environment $_51 zero \/
% 0.56/0.86     in_environment $_51
% 0.56/0.86       (number_of_organizations e (appear an_organisation sk2))
% 0.56/0.87  |- ~environment $_51 \/
% 0.56/0.87     ~greater_or_equal zero (number_of_organizations sk2 sk3) \/
% 0.56/0.87     ~in_environment $_51 zero \/
% 0.56/0.87     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment $_51 (number_of_organizations sk2 sk3)
% 0.56/0.87  |- ~greater_or_equal $_53 sk3 \/ ~greater_or_equal sk3 $_53 \/
% 0.56/0.87     in_environment sk2 $_53
% 0.56/0.87  |- ~greater_or_equal $_53 (start_time sk2) \/
% 0.56/0.87     ~greater_or_equal (start_time sk2) $_53 \/ in_environment sk2 $_53
% 0.56/0.87  |- ~greater_or_equal sk3 (appear efficient_producers sk2) \/
% 0.56/0.87     in_environment sk2 (appear efficient_producers sk2)
% 0.56/0.87  |- ~greater zero zero \/
% 0.56/0.87     selection_favors efficient_producers efficient_producers sk3
% 0.56/0.87  |- ~(cardinality_at_time efficient_producers (start_time sk2) = zero) \/
% 0.56/0.87     ~greater zero zero \/
% 0.56/0.87     selection_favors efficient_producers efficient_producers
% 0.56/0.87       (start_time sk2)
% 0.56/0.87  |- ~(cardinality_at_time first_movers sk3 = zero) \/ ~greater zero zero \/
% 0.56/0.87     selection_favors first_movers first_movers sk3
% 0.56/0.87  |- ~(cardinality_at_time first_movers (start_time sk2) = zero) \/
% 0.56/0.87     ~greater zero zero \/
% 0.56/0.87     selection_favors first_movers first_movers (start_time sk2)
% 0.56/0.87  |- ~greater zero zero \/ appear first_movers sk2 = start_time sk2 \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     selection_favors efficient_producers efficient_producers
% 0.56/0.87       (start_time sk2)
% 0.56/0.87  |- ~greater zero zero \/ appear first_movers sk2 = start_time sk2 \/
% 0.56/0.87     selection_favors first_movers first_movers (start_time sk2)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal (appear an_organisation sk2) $_86 \/
% 0.56/0.87     ~in_environment $_85 $_86 \/
% 0.56/0.87     ~in_environment $_85 (appear efficient_producers e) \/
% 0.56/0.87     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.87     in_environment $_85 (appear an_organisation sk2)
% 0.56/0.87  |- ~environment $_85 \/ ~greater_or_equal (appear first_movers sk2) $_86 \/
% 0.56/0.87     ~in_environment $_85 $_86 \/
% 0.56/0.87     ~in_environment $_85 (appear efficient_producers e) \/
% 0.56/0.87     in_environment $_85 (appear first_movers sk2)
% 0.56/0.87  |- ~environment $_85 \/ ~greater_or_equal (start_time sk2) $_86 \/
% 0.56/0.87     ~in_environment $_85 $_86 \/
% 0.56/0.87     ~in_environment $_85 (appear efficient_producers e) \/
% 0.56/0.87     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.87     in_environment $_85 (start_time sk2)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal (appear an_organisation sk2) $_86 \/
% 0.56/0.87     ~in_environment $_85 $_86 \/
% 0.56/0.87     ~in_environment $_85 (appear efficient_producers sk2) \/
% 0.56/0.87     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment $_85 (appear an_organisation sk2)
% 0.56/0.87  |- ~environment $_85 \/ ~greater_or_equal (appear first_movers sk2) $_86 \/
% 0.56/0.87     ~in_environment $_85 $_86 \/
% 0.56/0.87     ~in_environment $_85 (appear efficient_producers sk2) \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment $_85 (appear first_movers sk2)
% 0.56/0.87  |- ~environment $_85 \/ ~greater_or_equal (start_time sk2) $_86 \/
% 0.56/0.87     ~in_environment $_85 $_86 \/
% 0.56/0.87     ~in_environment $_85 (appear efficient_producers sk2) \/
% 0.56/0.87     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/ in_environment $_85 (start_time sk2)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal (appear an_organisation sk2) $_86 \/
% 0.56/0.87     ~in_environment $_85 $_86 \/
% 0.56/0.87     ~in_environment $_85 (appear first_movers sk2) \/
% 0.56/0.87     in_environment $_85 (appear an_organisation sk2)
% 0.56/0.87  |- ~environment $_85 \/ ~greater_or_equal (start_time sk2) $_86 \/
% 0.56/0.87     ~in_environment $_85 $_86 \/
% 0.56/0.87     ~in_environment $_85 (appear first_movers sk2) \/
% 0.56/0.87     in_environment $_85 (start_time sk2)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal $_87 (appear efficient_producers e) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/
% 0.56/0.87     ~in_environment $_85 (appear an_organisation sk2) \/
% 0.56/0.87     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.87     in_environment $_85 (appear efficient_producers e)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal $_87 (appear efficient_producers e) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/
% 0.56/0.87     ~in_environment $_85 (appear first_movers sk2) \/
% 0.56/0.87     in_environment $_85 (appear efficient_producers e)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal $_87 (appear efficient_producers e) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/ ~in_environment $_85 (start_time sk2) \/
% 0.56/0.87     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.87     in_environment $_85 (appear efficient_producers e)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal $_87 (appear efficient_producers sk2) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/
% 0.56/0.87     ~in_environment $_85 (appear an_organisation sk2) \/
% 0.56/0.87     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment $_85 (appear efficient_producers sk2)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal $_87 (appear efficient_producers sk2) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/
% 0.56/0.87     ~in_environment $_85 (appear first_movers sk2) \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment $_85 (appear efficient_producers sk2)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal $_87 (appear efficient_producers sk2) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/ ~in_environment $_85 sk3 \/
% 0.56/0.87     in_environment $_85 (appear efficient_producers sk2)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal $_87 (appear efficient_producers sk2) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/ ~in_environment $_85 (start_time sk2) \/
% 0.56/0.87     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment $_85 (appear efficient_producers sk2)
% 0.56/0.87  |- ~environment $_85 \/ ~greater_or_equal $_87 (appear first_movers sk2) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/
% 0.56/0.87     ~in_environment $_85 (appear an_organisation sk2) \/
% 0.56/0.87     in_environment $_85 (appear first_movers sk2)
% 0.56/0.87  |- ~environment $_85 \/ ~greater_or_equal $_87 (appear first_movers sk2) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/ ~in_environment $_85 (start_time sk2) \/
% 0.56/0.87     in_environment $_85 (appear first_movers sk2)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal $_87
% 0.56/0.87        (number_of_organizations e (appear an_organisation sk2)) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/ ~in_environment $_85 zero \/
% 0.56/0.87     in_environment $_85
% 0.56/0.87       (number_of_organizations e (appear an_organisation sk2))
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal $_87 (number_of_organizations sk2 sk3) \/
% 0.56/0.87     ~in_environment $_85 $_87 \/ ~in_environment $_85 zero \/
% 0.56/0.87     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment $_85 (number_of_organizations sk2 sk3)
% 0.56/0.87  |- ~greater_or_equal $_87 $_88 \/ ~greater_or_equal $_88 sk3 \/
% 0.56/0.87     ~in_environment sk2 $_87 \/ in_environment sk2 $_88
% 0.56/0.87  |- ~greater_or_equal $_87 $_88 \/
% 0.56/0.87     ~greater_or_equal $_88 (start_time sk2) \/ ~in_environment sk2 $_87 \/
% 0.56/0.87     in_environment sk2 $_88
% 0.56/0.87  |- ~greater_or_equal $_88 $_86 \/ ~greater_or_equal sk3 $_88 \/
% 0.56/0.87     ~in_environment sk2 $_86 \/ in_environment sk2 $_88
% 0.56/0.87  |- ~greater_or_equal $_88 $_86 \/
% 0.56/0.87     ~greater_or_equal (start_time sk2) $_88 \/ ~in_environment sk2 $_86 \/
% 0.56/0.87     in_environment sk2 $_88
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal (appear first_movers sk2)
% 0.56/0.87        (appear efficient_producers e) \/
% 0.56/0.87     ~in_environment $_85 (appear efficient_producers e) \/
% 0.56/0.87     in_environment $_85 (appear first_movers sk2)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal (appear first_movers sk2)
% 0.56/0.87        (appear efficient_producers e) \/
% 0.56/0.87     ~in_environment $_85 (appear first_movers sk2) \/
% 0.56/0.87     in_environment $_85 (appear efficient_producers e)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal (appear first_movers sk2)
% 0.56/0.87        (appear efficient_producers sk2) \/
% 0.56/0.87     ~in_environment $_85 (appear efficient_producers sk2) \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment $_85 (appear first_movers sk2)
% 0.56/0.87  |- ~environment $_85 \/
% 0.56/0.87     ~greater_or_equal (appear first_movers sk2)
% 0.56/0.87        (appear efficient_producers sk2) \/
% 0.56/0.87     ~in_environment $_85 (appear first_movers sk2) \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment $_85 (appear efficient_producers sk2)
% 0.56/0.87  |- ~greater_or_equal $_93 (appear efficient_producers sk2) \/
% 0.56/0.87     ~in_environment sk2 $_93 \/
% 0.56/0.87     in_environment sk2 (appear efficient_producers sk2)
% 0.56/0.87  |- ~greater_or_equal $_94 sk3 \/ ~greater_or_equal (start_time sk2) $_94 \/
% 0.56/0.87     in_environment sk2 $_94
% 0.56/0.87  |- ~greater_or_equal sk3 (appear efficient_producers e) \/
% 0.56/0.87     in_environment sk2 (appear efficient_producers e)
% 0.56/0.87  |- in_environment sk2 (appear first_movers sk2)
% 0.56/0.87  |- ~greater_or_equal sk3 (cardinality_at_time (sk1 sk3 sk2) sk3) \/
% 0.56/0.87     ~in_environment sk2 zero \/
% 0.56/0.87     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment sk2 (cardinality_at_time (sk1 sk3 sk2) sk3)
% 0.56/0.87  |- ~greater_or_equal sk3
% 0.56/0.87        (number_of_organizations e (appear an_organisation sk2)) \/
% 0.56/0.87     ~in_environment sk2 zero \/
% 0.56/0.87     in_environment sk2
% 0.56/0.87       (number_of_organizations e (appear an_organisation sk2))
% 0.56/0.87  |- ~greater_or_equal sk3 (number_of_organizations sk2 sk3) \/
% 0.56/0.87     ~in_environment sk2 zero \/
% 0.56/0.87     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.87     sk3 = appear first_movers sk2 \/
% 0.56/0.87     in_environment sk2 (number_of_organizations sk2 sk3)
% 0.56/0.87  |- ~greater_or_equal $_98 (start_time sk2) \/ ~greater_or_equal sk3 $_98 \/
% 0.56/0.87     in_environment sk2 $_98
% 0.56/0.87  |- ~greater_or_equal $D $B \/
% 0.56/0.87     ~greater_or_equal (appear first_movers sk2) $D \/
% 0.56/0.87     ~in_environment sk2 $B \/ in_environment sk2 $D
% 0.56/0.87  |- ~greater_or_equal $C $D \/
% 0.56/0.87     ~greater_or_equal $D (appear first_movers sk2) \/
% 0.56/0.87     ~in_environment sk2 $C \/ in_environment sk2 $D
% 0.56/0.87  |- ~greater_or_equal $D (appear first_movers sk2) \/
% 0.56/0.87     ~greater_or_equal (appear first_movers sk2) $D \/ in_environment sk2 $D
% 0.56/0.87  |- subpopulation efficient_producers sk2 (appear first_movers sk2)
% 0.56/0.87  |- subpopulation first_movers sk2 (appear first_movers sk2)
% 0.56/0.87  |- in_environment sk2 (appear an_organisation sk2)
% 0.56/0.87  |- ~greater_or_equal $_88 (appear first_movers sk2) \/
% 0.56/0.87     ~greater_or_equal sk3 $_88 \/ in_environment sk2 $_88
% 0.56/0.87  |- ~greater_or_equal $_88 sk3 \/
% 0.56/0.87     ~greater_or_equal (appear first_movers sk2) $_88 \/
% 0.56/0.87     in_environment sk2 $_88
% 0.56/0.87  |- ~greater_or_equal $_88 (appear first_movers sk2) \/
% 0.56/0.87     ~greater_or_equal (start_time sk2) $_88 \/ in_environment sk2 $_88
% 0.56/0.87  |- cardinality_at_time efficient_producers (appear first_movers sk2) =
% 0.56/0.87     zero \/ sk3 = appear first_movers sk2
% 0.56/0.87  |- greater (number_of_organizations sk2 (appear first_movers sk2)) zero
% 0.56/0.87  |- ~greater_or_equal $D $B \/
% 0.56/0.87     ~greater_or_equal (appear an_organisation sk2) $D \/
% 0.56/0.87     ~in_environment sk2 $B \/ in_environment sk2 $D
% 0.56/0.87  |- ~greater_or_equal $C $D \/
% 0.56/0.87     ~greater_or_equal $D (appear an_organisation sk2) \/
% 0.56/0.87     ~in_environment sk2 $C \/ in_environment sk2 $D
% 0.56/0.87  |- ~greater_or_equal $D (appear an_organisation sk2) \/
% 0.56/0.87     ~greater_or_equal (appear an_organisation sk2) $D \/
% 0.56/0.87     in_environment sk2 $D
% 0.56/0.87  |- subpopulation efficient_producers sk2 (appear an_organisation sk2)
% 0.56/0.87  |- subpopulation first_movers sk2 (appear an_organisation sk2)
% 0.56/0.87  |- greater (number_of_organizations sk2 (appear an_organisation sk2)) zero
% 0.56/0.87  |- ~greater_or_equal $_88 (appear an_organisation sk2) \/
% 0.56/0.87     ~greater_or_equal sk3 $_88 \/ in_environment sk2 $_88
% 0.56/0.87  |- ~greater_or_equal $_88 sk3 \/
% 0.56/0.87     ~greater_or_equal (appear an_organisation sk2) $_88 \/
% 0.56/0.87     in_environment sk2 $_88
% 0.56/0.87  |- ~greater_or_equal $_88 (appear an_organisation sk2) \/
% 0.56/0.87     ~greater_or_equal (start_time sk2) $_88 \/ in_environment sk2 $_88
% 0.56/0.87  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.87     cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.56/0.87     zero \/ sk3 = appear first_movers sk2
% 0.56/0.87  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.87     cardinality_at_time first_movers (appear an_organisation sk2) = zero
% 0.56/0.87  |- ~(cardinality_at_time efficient_producers (appear first_movers sk2) =
% 0.56/0.87       zero) \/ ~greater zero zero \/
% 0.56/0.87     selection_favors efficient_producers efficient_producers
% 0.56/0.87       (appear first_movers sk2)
% 0.56/0.87  |- ~(cardinality_at_time first_movers (appear an_organisation sk2) =
% 0.56/0.87       zero) \/ ~greater zero zero \/
% 0.56/0.87     selection_favors first_movers first_movers (appear an_organisation sk2)
% 0.56/0.87  |- ~greater $A
% 0.56/0.87        (number_of_organizations sk2 (appear an_organisation sk2)) \/
% 0.56/0.87     greater $A zero
% 0.56/0.87  |- ~greater zero $C \/
% 0.56/0.87     greater (number_of_organizations sk2 (appear an_organisation sk2)) $C
% 0.56/0.87  |- greater_or_equal
% 0.56/0.87       (number_of_organizations sk2 (appear an_organisation sk2)) zero
% 0.56/0.87  |- greater
% 0.56/0.87       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.87          (appear an_organisation sk2)) zero
% 0.56/0.87  |- subpopulation (sk1 (appear an_organisation sk2) sk2) sk2
% 0.56/0.87       (appear an_organisation sk2)
% 0.56/0.87  |- ~greater_or_equal sk3
% 0.56/0.87        (number_of_organizations sk2 (appear an_organisation sk2)) \/
% 0.56/0.87     ~in_environment sk2 zero \/
% 0.56/0.87     in_environment sk2
% 0.56/0.87       (number_of_organizations sk2 (appear an_organisation sk2))
% 0.56/0.87  |- ~environment $A \/
% 0.56/0.87     ~greater_or_equal $C
% 0.56/0.87        (number_of_organizations sk2 (appear an_organisation sk2)) \/
% 0.56/0.87     ~in_environment $A $C \/ ~in_environment $A zero \/
% 0.56/0.87     in_environment $A
% 0.56/0.87       (number_of_organizations sk2 (appear an_organisation sk2))
% 0.56/0.87  |- ~environment $A \/
% 0.56/0.87     ~greater_or_equal zero
% 0.56/0.87        (number_of_organizations sk2 (appear an_organisation sk2)) \/
% 0.56/0.87     ~in_environment $A zero \/
% 0.56/0.87     in_environment $A
% 0.56/0.87       (number_of_organizations sk2 (appear an_organisation sk2))
% 0.56/0.87  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.56/0.87     ~greater zero zero \/
% 0.56/0.87     selection_favors first_movers first_movers (appear first_movers sk2)
% 0.56/0.87  |- ~greater $A (number_of_organizations sk2 (appear first_movers sk2)) \/
% 0.56/0.87     greater $A zero
% 0.56/0.87  |- ~greater zero $C \/
% 0.56/0.87     greater (number_of_organizations sk2 (appear first_movers sk2)) $C
% 0.56/0.87  |- greater_or_equal (number_of_organizations sk2 (appear first_movers sk2))
% 0.56/0.87       zero
% 0.56/0.87  |- greater
% 0.56/0.87       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.87          (appear first_movers sk2)) zero
% 0.56/0.87  |- subpopulation (sk1 (appear first_movers sk2) sk2) sk2
% 0.56/0.87       (appear first_movers sk2)
% 0.56/0.87  |- ~greater_or_equal sk3
% 0.56/0.87        (number_of_organizations sk2 (appear first_movers sk2)) \/
% 0.56/0.87     ~in_environment sk2 zero \/
% 0.56/0.87     in_environment sk2
% 0.56/0.87       (number_of_organizations sk2 (appear first_movers sk2))
% 0.56/0.88  |- ~environment $A \/
% 0.56/0.88     ~greater_or_equal $C
% 0.56/0.88        (number_of_organizations sk2 (appear first_movers sk2)) \/
% 0.56/0.88     ~in_environment $A $C \/ ~in_environment $A zero \/
% 0.56/0.88     in_environment $A
% 0.56/0.88       (number_of_organizations sk2 (appear first_movers sk2))
% 0.56/0.88  |- ~environment $A \/
% 0.56/0.88     ~greater_or_equal zero
% 0.56/0.88        (number_of_organizations sk2 (appear first_movers sk2)) \/
% 0.56/0.88     ~in_environment $A zero \/
% 0.56/0.88     in_environment $A
% 0.56/0.88       (number_of_organizations sk2 (appear first_movers sk2))
% 0.56/0.88  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.56/0.88       zero) \/ ~greater zero zero \/
% 0.56/0.88     selection_favors efficient_producers efficient_producers
% 0.56/0.88       (appear an_organisation sk2)
% 0.56/0.88  |- ~greater $A
% 0.56/0.88        (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88           (appear first_movers sk2)) \/ greater $A zero
% 0.56/0.88  |- ~greater zero $C \/
% 0.56/0.88     greater
% 0.56/0.88       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88          (appear first_movers sk2)) $C
% 0.56/0.88  |- greater_or_equal
% 0.56/0.88       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88          (appear first_movers sk2)) zero
% 0.56/0.88  |- ~(cardinality_at_time (sk1 (appear first_movers sk2) sk2) t = zero)
% 0.56/0.88  |- ~greater_or_equal sk3
% 0.56/0.88        (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88           (appear first_movers sk2)) \/ ~in_environment sk2 zero \/
% 0.56/0.88     in_environment sk2
% 0.56/0.88       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88          (appear first_movers sk2))
% 0.56/0.88  |- ~environment $A \/
% 0.56/0.88     ~greater_or_equal $C
% 0.56/0.88        (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88           (appear first_movers sk2)) \/ ~in_environment $A $C \/
% 0.56/0.88     ~in_environment $A zero \/
% 0.56/0.88     in_environment $A
% 0.56/0.88       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88          (appear first_movers sk2))
% 0.56/0.88  |- ~environment $A \/
% 0.56/0.88     ~greater_or_equal zero
% 0.56/0.88        (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88           (appear first_movers sk2)) \/ ~in_environment $A zero \/
% 0.56/0.88     in_environment $A
% 0.56/0.88       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88          (appear first_movers sk2))
% 0.56/0.88  |- ~greater $A
% 0.56/0.88        (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88           (appear an_organisation sk2)) \/ greater $A zero
% 0.56/0.88  |- ~greater zero $C \/
% 0.56/0.88     greater
% 0.56/0.88       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88          (appear an_organisation sk2)) $C
% 0.56/0.88  |- greater_or_equal
% 0.56/0.88       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88          (appear an_organisation sk2)) zero
% 0.56/0.88  |- ~(cardinality_at_time (sk1 (appear an_organisation sk2) sk2) t = zero)
% 0.56/0.88  |- ~greater_or_equal sk3
% 0.56/0.88        (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88           (appear an_organisation sk2)) \/ ~in_environment sk2 zero \/
% 0.56/0.88     in_environment sk2
% 0.56/0.88       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88          (appear an_organisation sk2))
% 0.56/0.88  |- ~environment $A \/
% 0.56/0.88     ~greater_or_equal $C
% 0.56/0.88        (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88           (appear an_organisation sk2)) \/ ~in_environment $A $C \/
% 0.56/0.88     ~in_environment $A zero \/
% 0.56/0.88     in_environment $A
% 0.56/0.88       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88          (appear an_organisation sk2))
% 0.56/0.88  |- ~environment $A \/
% 0.56/0.88     ~greater_or_equal zero
% 0.56/0.88        (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88           (appear an_organisation sk2)) \/ ~in_environment $A zero \/
% 0.56/0.88     in_environment $A
% 0.56/0.88       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88          (appear an_organisation sk2))
% 0.56/0.88  |- ~(cardinality_at_time first_movers t = zero) \/ ~greater zero zero \/
% 0.56/0.88     appear first_movers sk2 = appear an_organisation sk2
% 0.56/0.88  |- ~greater zero zero \/ sk3 = appear first_movers sk2 \/
% 0.56/0.88     selection_favors efficient_producers efficient_producers
% 0.56/0.88       (appear first_movers sk2)
% 0.56/0.88  |- ~greater zero zero \/
% 0.56/0.88     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.88     selection_favors first_movers first_movers (appear an_organisation sk2)
% 0.56/0.88  |- ~greater_or_equal (start_time sk2) (appear efficient_producers e) \/
% 0.56/0.88     in_environment sk2 (appear efficient_producers e)
% 0.56/0.88  |- ~greater_or_equal (start_time sk2) (appear efficient_producers sk2) \/
% 0.56/0.88     sk3 = appear first_movers sk2 \/
% 0.56/0.88     in_environment sk2 (appear efficient_producers sk2)
% 0.56/0.88  |- ~greater_or_equal $_117 (start_time sk2) \/
% 0.56/0.88     ~greater_or_equal (appear an_organisation sk2) $_117 \/
% 0.56/0.88     in_environment sk2 $_117
% 0.56/0.88  |- ~greater_or_equal $_117 (start_time sk2) \/
% 0.56/0.88     ~greater_or_equal (appear first_movers sk2) $_117 \/
% 0.56/0.88     in_environment sk2 $_117
% 0.56/0.88  |- ~environment $_121 \/
% 0.56/0.88     ~in_environment $_121 (appear efficient_producers e) \/
% 0.56/0.88     ~in_environment $_121 (start_time sk2) \/
% 0.56/0.88     in_environment $_121 (appear first_movers sk2)
% 0.56/0.88  |- ~environment $_121 \/
% 0.56/0.88     ~in_environment $_121 (appear efficient_producers sk2) \/
% 0.56/0.88     ~in_environment $_121 (start_time sk2) \/
% 0.56/0.88     sk3 = appear first_movers sk2 \/
% 0.56/0.88     in_environment $_121 (appear first_movers sk2)
% 0.56/0.88  |- ~environment $_121 \/ ~in_environment $_121 sk3 \/
% 0.56/0.88     ~in_environment $_121 (start_time sk2) \/
% 0.56/0.88     in_environment $_121 (appear first_movers sk2)
% 0.56/0.88  |- ~environment $_125 \/
% 0.56/0.88     ~in_environment $_125 (appear an_organisation sk2) \/
% 0.56/0.88     ~in_environment $_125 (appear efficient_producers e) \/
% 0.56/0.88     in_environment $_125 (appear first_movers sk2)
% 0.56/0.88  |- ~greater_or_equal $_133 (appear an_organisation sk2) \/
% 0.56/0.88     ~greater_or_equal (appear first_movers sk2) $_133 \/
% 0.56/0.88     in_environment sk2 $_133
% 0.56/0.88  |- ~greater_or_equal $_142 (appear efficient_producers e) \/
% 0.56/0.88     ~in_environment sk2 $_142 \/
% 0.56/0.88     in_environment sk2 (appear efficient_producers e)
% 0.56/0.88  |- ~greater_or_equal $_143 (appear first_movers sk2) \/
% 0.56/0.88     ~greater_or_equal (appear an_organisation sk2) $_143 \/
% 0.56/0.88     in_environment sk2 $_143
% 0.56/0.88  |- ~greater_or_equal (appear an_organisation sk2)
% 0.56/0.88        (appear efficient_producers e) \/
% 0.56/0.88     in_environment sk2 (appear efficient_producers e)
% 0.56/0.88  |- ~greater_or_equal (appear an_organisation sk2)
% 0.56/0.88        (appear efficient_producers sk2) \/ sk3 = appear first_movers sk2 \/
% 0.56/0.88     in_environment sk2 (appear efficient_producers sk2)
% 0.56/0.88  |- ~environment $_153 \/
% 0.56/0.88     ~in_environment $_153 (appear an_organisation sk2) \/
% 0.56/0.88     ~in_environment $_153 (appear efficient_producers sk2) \/
% 0.56/0.88     sk3 = appear first_movers sk2 \/
% 0.56/0.88     in_environment $_153 (appear first_movers sk2)
% 0.56/0.88  |- ~(cardinality_at_time $_166 (appear an_organisation sk2) = zero) \/
% 0.56/0.88     ~environment $_163 \/
% 0.56/0.88     ~subpopulation $_166 $_163 (appear an_organisation sk2) \/
% 0.56/0.88     ~subpopulation (sk1 (appear an_organisation sk2) sk2) $_163
% 0.56/0.88        (appear an_organisation sk2) \/
% 0.56/0.88     selection_favors (sk1 (appear an_organisation sk2) sk2) $_166
% 0.56/0.88       (appear an_organisation sk2)
% 0.56/0.88  |- ~(cardinality_at_time $_166 (appear first_movers sk2) = zero) \/
% 0.56/0.88     ~environment $_163 \/
% 0.56/0.88     ~subpopulation $_166 $_163 (appear first_movers sk2) \/
% 0.56/0.88     ~subpopulation (sk1 (appear first_movers sk2) sk2) $_163
% 0.56/0.88        (appear first_movers sk2) \/
% 0.56/0.88     selection_favors (sk1 (appear first_movers sk2) sk2) $_166
% 0.56/0.88       (appear first_movers sk2)
% 0.56/0.88  |- ~(cardinality_at_time $_166 sk3 = zero) \/ ~environment $_163 \/
% 0.56/0.88     ~subpopulation $_166 $_163 sk3 \/
% 0.56/0.88     ~subpopulation (sk1 sk3 sk2) $_163 sk3 \/
% 0.56/0.88     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.88     sk3 = appear first_movers sk2 \/
% 0.56/0.88     selection_favors (sk1 sk3 sk2) $_166 sk3
% 0.56/0.88  |- ~(cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88         (appear an_organisation sk2) = zero) \/
% 0.56/0.88     ~greater (cardinality_at_time $_164 (appear an_organisation sk2))
% 0.56/0.88        zero \/ ~subpopulation $_164 sk2 (appear an_organisation sk2) \/
% 0.56/0.88     selection_favors $_164 (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88       (appear an_organisation sk2)
% 0.56/0.88  |- ~(cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88         (appear first_movers sk2) = zero) \/
% 0.56/0.88     ~greater (cardinality_at_time $_164 (appear first_movers sk2)) zero \/
% 0.56/0.88     ~subpopulation $_164 sk2 (appear first_movers sk2) \/
% 0.56/0.88     selection_favors $_164 (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88       (appear first_movers sk2)
% 0.56/0.88  |- ~(cardinality_at_time (sk1 sk3 sk2) sk3 = zero) \/
% 0.56/0.88     ~greater (cardinality_at_time $_164 sk3) zero \/
% 0.56/0.88     ~subpopulation $_164 sk2 sk3 \/
% 0.56/0.88     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.88     sk3 = appear first_movers sk2 \/
% 0.56/0.88     selection_favors $_164 (sk1 sk3 sk2) sk3
% 0.56/0.88  |- ~(cardinality_at_time $_166 (appear an_organisation sk2) = zero) \/
% 0.56/0.88     ~environment $_163 \/ ~greater zero zero \/
% 0.56/0.88     ~subpopulation $_166 $_163 (appear an_organisation sk2) \/
% 0.56/0.88     ~subpopulation efficient_producers $_163 (appear an_organisation sk2) \/
% 0.56/0.88     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.88     sk3 = appear first_movers sk2 \/
% 0.56/0.88     selection_favors efficient_producers $_166 (appear an_organisation sk2)
% 0.56/0.88  |- ~(cardinality_at_time $_166 (appear first_movers sk2) = zero) \/
% 0.56/0.88     ~environment $_163 \/ ~greater zero zero \/
% 0.56/0.88     ~subpopulation $_166 $_163 (appear first_movers sk2) \/
% 0.56/0.88     ~subpopulation efficient_producers $_163 (appear first_movers sk2) \/
% 0.56/0.88     sk3 = appear first_movers sk2 \/
% 0.56/0.88     selection_favors efficient_producers $_166 (appear first_movers sk2)
% 0.56/0.88  |- ~(cardinality_at_time $_166 sk3 = zero) \/ ~environment $_163 \/
% 0.56/0.88     ~greater zero zero \/ ~subpopulation $_166 $_163 sk3 \/
% 0.56/0.88     ~subpopulation efficient_producers $_163 sk3 \/
% 0.56/0.88     selection_favors efficient_producers $_166 sk3
% 0.56/0.88  |- ~(cardinality_at_time $_166 (start_time sk2) = zero) \/
% 0.56/0.88     ~environment $_163 \/ ~greater zero zero \/
% 0.56/0.88     ~subpopulation $_166 $_163 (start_time sk2) \/
% 0.56/0.88     ~subpopulation efficient_producers $_163 (start_time sk2) \/
% 0.56/0.88     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.88     sk3 = appear first_movers sk2 \/
% 0.56/0.88     selection_favors efficient_producers $_166 (start_time sk2)
% 0.56/0.88  |- ~(cardinality_at_time $_166 (appear an_organisation sk2) = zero) \/
% 0.56/0.88     ~environment $_163 \/ ~greater zero zero \/
% 0.56/0.88     ~subpopulation $_166 $_163 (appear an_organisation sk2) \/
% 0.56/0.88     ~subpopulation first_movers $_163 (appear an_organisation sk2) \/
% 0.56/0.88     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.56/0.88     selection_favors first_movers $_166 (appear an_organisation sk2)
% 0.56/0.88  |- ~(cardinality_at_time $_166 (start_time sk2) = zero) \/
% 0.56/0.88     ~environment $_163 \/ ~greater zero zero \/
% 0.56/0.88     ~subpopulation $_166 $_163 (start_time sk2) \/
% 0.56/0.88     ~subpopulation first_movers $_163 (start_time sk2) \/
% 0.56/0.88     appear first_movers sk2 = start_time sk2 \/
% 0.56/0.88     selection_favors first_movers $_166 (start_time sk2)
% 0.56/0.88  |- ~(cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88         (appear an_organisation sk2) = zero) \/
% 0.56/0.88     selection_favors (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.88       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.56/0.88  |- ~(cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88         (appear first_movers sk2) = zero) \/
% 0.56/0.88     selection_favors (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88       (sk1 (appear first_movers sk2) sk2) (appear first_movers sk2)
% 0.56/0.88  |- ~(cardinality_at_time first_movers sk3 = zero) \/ ~greater zero zero \/
% 0.56/0.88     selection_favors efficient_producers first_movers sk3
% 0.56/0.88  |- ~(cardinality_at_time $_170 sk3 = zero) \/ ~greater zero zero \/
% 0.56/0.88     ~subpopulation $_170 sk2 sk3 \/
% 0.56/0.88     selection_favors efficient_producers $_170 sk3
% 0.56/0.88  |- sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.88     sk1 (appear first_movers sk2) sk2 = first_movers
% 0.56/0.88  |- ~(cardinality_at_time efficient_producers (appear first_movers sk2) =
% 0.56/0.88       zero) \/ sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.88     selection_favors (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88       (sk1 (appear first_movers sk2) sk2) (appear first_movers sk2)
% 0.56/0.88  |- ~(cardinality_at_time efficient_producers (appear first_movers sk2) =
% 0.56/0.88       zero) \/
% 0.56/0.88     ~greater (cardinality_at_time $_164 (appear first_movers sk2)) zero \/
% 0.56/0.88     ~subpopulation $_164 sk2 (appear first_movers sk2) \/
% 0.56/0.88     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.88     selection_favors $_164 (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88       (appear first_movers sk2)
% 0.56/0.88  |- ~greater_or_equal sk3
% 0.56/0.88        (cardinality_at_time efficient_producers
% 0.56/0.88           (appear first_movers sk2)) \/ ~in_environment sk2 zero \/
% 0.56/0.88     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.88     in_environment sk2
% 0.56/0.88       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88          (appear first_movers sk2))
% 0.56/0.88  |- ~greater $A
% 0.56/0.88        (cardinality_at_time efficient_producers
% 0.56/0.88           (appear first_movers sk2)) \/
% 0.56/0.88     sk1 (appear first_movers sk2) sk2 = first_movers \/ greater $A zero
% 0.56/0.88  |- ~(cardinality_at_time efficient_producers t = zero) \/
% 0.56/0.88     sk1 (appear first_movers sk2) sk2 = first_movers
% 0.56/0.88  |- sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.88     greater_or_equal
% 0.56/0.88       (cardinality_at_time efficient_producers (appear first_movers sk2))
% 0.56/0.88       zero
% 0.56/0.88  |- sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.88     greater
% 0.56/0.88       (cardinality_at_time efficient_producers (appear first_movers sk2))
% 0.56/0.88       zero
% 0.56/0.88  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.56/0.88     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.88     selection_favors (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88       (sk1 (appear first_movers sk2) sk2) (appear first_movers sk2)
% 0.56/0.88  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.56/0.88     ~greater (cardinality_at_time $_164 (appear first_movers sk2)) zero \/
% 0.56/0.88     ~subpopulation $_164 sk2 (appear first_movers sk2) \/
% 0.56/0.88     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.88     selection_favors $_164 (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88       (appear first_movers sk2)
% 0.56/0.88  |- ~greater_or_equal sk3
% 0.56/0.88        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.88     ~in_environment sk2 zero \/
% 0.56/0.88     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.88     in_environment sk2
% 0.56/0.88       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.88          (appear first_movers sk2))
% 0.56/0.89  |- ~greater $A
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.89     greater $A zero
% 0.56/0.89  |- ~(cardinality_at_time first_movers t = zero) \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = efficient_producers
% 0.56/0.89  |- sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.89     greater_or_equal
% 0.56/0.89       (cardinality_at_time first_movers (appear first_movers sk2)) zero
% 0.56/0.89  |- sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.89     greater (cardinality_at_time first_movers (appear first_movers sk2))
% 0.56/0.89       zero
% 0.56/0.89  |- ~greater_or_equal sk3
% 0.56/0.89        (cardinality_at_time efficient_producers
% 0.56/0.89           (appear first_movers sk2)) \/ ~in_environment sk2 zero \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     in_environment sk2
% 0.56/0.89       (cardinality_at_time efficient_producers (appear first_movers sk2))
% 0.56/0.89  |- ~environment $A \/
% 0.56/0.89     ~greater_or_equal $C
% 0.56/0.89        (cardinality_at_time efficient_producers
% 0.56/0.89           (appear first_movers sk2)) \/ ~in_environment $A $C \/
% 0.56/0.89     ~in_environment $A zero \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     in_environment $A
% 0.56/0.89       (cardinality_at_time efficient_producers (appear first_movers sk2))
% 0.56/0.89  |- ~environment $A \/
% 0.56/0.89     ~greater_or_equal zero
% 0.56/0.89        (cardinality_at_time efficient_producers
% 0.56/0.89           (appear first_movers sk2)) \/ ~in_environment $A zero \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     in_environment $A
% 0.56/0.89       (cardinality_at_time efficient_producers (appear first_movers sk2))
% 0.56/0.89  |- ~greater zero $C \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.89     greater (cardinality_at_time first_movers (appear first_movers sk2)) $C
% 0.56/0.89  |- ~(cardinality_at_time $D (appear first_movers sk2) = zero) \/
% 0.56/0.89     ~environment $A \/ ~subpopulation $D $A (appear first_movers sk2) \/
% 0.56/0.89     ~subpopulation first_movers $A (appear first_movers sk2) \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.89     selection_favors first_movers $D (appear first_movers sk2)
% 0.56/0.89  |- ~greater zero $C \/ sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     greater
% 0.56/0.89       (cardinality_at_time efficient_producers (appear first_movers sk2)) $C
% 0.56/0.89  |- ~(cardinality_at_time $D (appear first_movers sk2) = zero) \/
% 0.56/0.89     ~environment $A \/ ~subpopulation $D $A (appear first_movers sk2) \/
% 0.56/0.89     ~subpopulation efficient_producers $A (appear first_movers sk2) \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     selection_favors efficient_producers $D (appear first_movers sk2)
% 0.56/0.89  |- sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/ greater zero zero
% 0.56/0.89  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.56/0.89     selection_favors (sk1 (appear first_movers sk2) sk2)
% 0.56/0.89       (sk1 (appear first_movers sk2) sk2) (appear first_movers sk2)
% 0.56/0.89  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.56/0.89     ~greater (cardinality_at_time $_164 (appear first_movers sk2)) zero \/
% 0.56/0.89     ~subpopulation $_164 sk2 (appear first_movers sk2) \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.56/0.89     selection_favors $_164 (sk1 (appear first_movers sk2) sk2)
% 0.56/0.89       (appear first_movers sk2)
% 0.56/0.89  |- ~greater_or_equal sk3
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     ~in_environment sk2 zero \/ sk3 = appear first_movers sk2 \/
% 0.56/0.89     greater zero zero \/
% 0.56/0.89     in_environment sk2
% 0.56/0.89       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.89          (appear first_movers sk2))
% 0.56/0.89  |- ~greater $A
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/ greater $A zero \/ greater zero zero
% 0.56/0.89  |- ~(cardinality_at_time first_movers t = zero) \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/ greater zero zero
% 0.56/0.89  |- sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.56/0.89     greater_or_equal
% 0.56/0.89       (cardinality_at_time first_movers (appear first_movers sk2)) zero
% 0.56/0.89  |- sk3 = appear first_movers sk2 \/
% 0.56/0.89     greater (cardinality_at_time first_movers (appear first_movers sk2))
% 0.56/0.89       zero \/ greater zero zero
% 0.56/0.89  |- ~greater zero $C \/ sk3 = appear first_movers sk2 \/
% 0.56/0.89     greater (cardinality_at_time first_movers (appear first_movers sk2))
% 0.56/0.89       $C \/ greater zero zero
% 0.56/0.89  |- ~(cardinality_at_time $D (appear first_movers sk2) = zero) \/
% 0.56/0.89     ~environment $A \/ ~subpopulation $D $A (appear first_movers sk2) \/
% 0.56/0.89     ~subpopulation first_movers $A (appear first_movers sk2) \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.56/0.89     selection_favors first_movers $D (appear first_movers sk2)
% 0.56/0.89  |- ~greater_or_equal sk3
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     ~in_environment sk2 zero \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.89     in_environment sk2
% 0.56/0.89       (cardinality_at_time first_movers (appear first_movers sk2))
% 0.56/0.89  |- ~environment $A \/
% 0.56/0.89     ~greater_or_equal $C
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     ~in_environment $A $C \/ ~in_environment $A zero \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.89     in_environment $A
% 0.56/0.89       (cardinality_at_time first_movers (appear first_movers sk2))
% 0.56/0.89  |- ~environment $A \/
% 0.56/0.89     ~greater_or_equal zero
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     ~in_environment $A zero \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.89     in_environment $A
% 0.56/0.89       (cardinality_at_time first_movers (appear first_movers sk2))
% 0.56/0.89  |- ~greater_or_equal sk3
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     ~in_environment sk2 zero \/ sk3 = appear first_movers sk2 \/
% 0.56/0.89     greater zero zero \/
% 0.56/0.89     in_environment sk2
% 0.56/0.89       (cardinality_at_time first_movers (appear first_movers sk2))
% 0.56/0.89  |- ~environment $A \/
% 0.56/0.89     ~greater_or_equal $C
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     ~in_environment $A $C \/ ~in_environment $A zero \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.56/0.89     in_environment $A
% 0.56/0.89       (cardinality_at_time first_movers (appear first_movers sk2))
% 0.56/0.89  |- ~environment $A \/
% 0.56/0.89     ~greater_or_equal zero
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     ~in_environment $A zero \/ sk3 = appear first_movers sk2 \/
% 0.56/0.89     greater zero zero \/
% 0.56/0.89     in_environment $A
% 0.56/0.89       (cardinality_at_time first_movers (appear first_movers sk2))
% 0.56/0.89  |- sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/
% 0.56/0.89     selection_favors (sk1 (appear first_movers sk2) sk2)
% 0.56/0.89       (sk1 (appear first_movers sk2) sk2) (appear first_movers sk2)
% 0.56/0.89  |- sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/
% 0.56/0.89     selection_favors efficient_producers (sk1 (appear first_movers sk2) sk2)
% 0.56/0.89       (appear first_movers sk2)
% 0.56/0.89  |- sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/
% 0.56/0.89     selection_favors efficient_producers efficient_producers
% 0.56/0.89       (appear first_movers sk2)
% 0.56/0.89  |- ~greater_or_equal sk3 zero \/ ~in_environment sk2 zero \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/
% 0.56/0.89     in_environment sk2
% 0.56/0.89       (cardinality_at_time efficient_producers (appear first_movers sk2))
% 0.56/0.89  |- ~greater_or_equal sk3 zero \/ ~in_environment sk2 zero \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     sk3 = appear first_movers sk2 \/
% 0.56/0.89     in_environment sk2
% 0.56/0.89       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.89          (appear first_movers sk2))
% 0.56/0.89  |- ~environment $_185 \/
% 0.56/0.89     ~greater_or_equal zero
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     ~in_environment $_185 zero \/ sk3 = appear first_movers sk2 \/
% 0.56/0.89     greater zero zero \/
% 0.56/0.89     in_environment $_185
% 0.56/0.89       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.89          (appear first_movers sk2))
% 0.56/0.89  |- ~environment $_185 \/
% 0.56/0.89     ~greater_or_equal zero
% 0.56/0.89        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.56/0.89     ~in_environment $_185 zero \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.56/0.89     in_environment $_185
% 0.56/0.89       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.89          (appear first_movers sk2))
% 0.56/0.89  |- ~environment $_185 \/
% 0.56/0.89     ~greater_or_equal zero
% 0.56/0.89        (cardinality_at_time efficient_producers
% 0.56/0.89           (appear first_movers sk2)) \/ ~in_environment $_185 zero \/
% 0.56/0.89     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.56/0.89     in_environment $_185
% 0.56/0.89       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.56/0.89          (appear first_movers sk2))
% 0.56/0.89  |- sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = first_movers
% 0.56/0.89  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.56/0.89       zero) \/ sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.56/0.89     selection_favors (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.89       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.56/0.89  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.56/0.89       zero) \/
% 0.56/0.89     ~greater (cardinality_at_time $_164 (appear an_organisation sk2))
% 0.56/0.89        zero \/ ~subpopulation $_164 sk2 (appear an_organisation sk2) \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.56/0.89     selection_favors $_164 (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.89       (appear an_organisation sk2)
% 0.56/0.89  |- ~greater_or_equal sk3
% 0.56/0.89        (cardinality_at_time efficient_producers
% 0.56/0.89           (appear an_organisation sk2)) \/ ~in_environment sk2 zero \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.56/0.89     in_environment sk2
% 0.56/0.89       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.89          (appear an_organisation sk2))
% 0.56/0.89  |- ~greater $A
% 0.56/0.89        (cardinality_at_time efficient_producers
% 0.56/0.89           (appear an_organisation sk2)) \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = first_movers \/ greater $A zero
% 0.56/0.89  |- ~(cardinality_at_time efficient_producers t = zero) \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = first_movers
% 0.56/0.89  |- sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.56/0.89     greater_or_equal
% 0.56/0.89       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.56/0.89       zero
% 0.56/0.89  |- sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.56/0.89     greater
% 0.56/0.89       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.56/0.89       zero
% 0.56/0.89  |- ~(cardinality_at_time first_movers (appear an_organisation sk2) =
% 0.56/0.89       zero) \/ sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.56/0.89     selection_favors (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.89       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.56/0.89  |- ~(cardinality_at_time first_movers (appear an_organisation sk2) =
% 0.56/0.89       zero) \/
% 0.56/0.89     ~greater (cardinality_at_time $_164 (appear an_organisation sk2))
% 0.56/0.89        zero \/ ~subpopulation $_164 sk2 (appear an_organisation sk2) \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.56/0.89     selection_favors $_164 (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.89       (appear an_organisation sk2)
% 0.56/0.89  |- ~greater_or_equal sk3
% 0.56/0.89        (cardinality_at_time first_movers (appear an_organisation sk2)) \/
% 0.56/0.89     ~in_environment sk2 zero \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.56/0.89     in_environment sk2
% 0.56/0.89       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.56/0.89          (appear an_organisation sk2))
% 0.56/0.89  |- ~greater $A
% 0.56/0.89        (cardinality_at_time first_movers (appear an_organisation sk2)) \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.56/0.89     greater $A zero
% 0.56/0.89  |- ~(cardinality_at_time first_movers t = zero) \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = efficient_producers
% 0.56/0.89  |- sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.56/0.89     greater_or_equal
% 0.56/0.89       (cardinality_at_time first_movers (appear an_organisation sk2)) zero
% 0.56/0.89  |- sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.56/0.89     greater (cardinality_at_time first_movers (appear an_organisation sk2))
% 0.56/0.89       zero
% 0.56/0.89  |- ~greater zero $C \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.56/0.89     greater
% 0.56/0.89       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.56/0.89       $C
% 0.56/0.89  |- ~(cardinality_at_time $D (appear an_organisation sk2) = zero) \/
% 0.56/0.89     ~environment $A \/ ~subpopulation $D $A (appear an_organisation sk2) \/
% 0.56/0.89     ~subpopulation efficient_producers $A (appear an_organisation sk2) \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.56/0.89     selection_favors efficient_producers $D (appear an_organisation sk2)
% 0.56/0.89  |- ~greater_or_equal sk3
% 0.56/0.89        (cardinality_at_time first_movers (appear an_organisation sk2)) \/
% 0.56/0.89     ~in_environment sk2 zero \/
% 0.56/0.89     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.56/0.89     in_environment sk2
% 0.56/0.89       (cardinality_at_time first_movers (appear an_organisation sk2))
% 0.56/0.90  |- ~environment $A \/
% 0.56/0.90     ~greater_or_equal $C
% 0.56/0.90        (cardinality_at_time first_movers (appear an_organisation sk2)) \/
% 0.56/0.90     ~in_environment $A $C \/ ~in_environment $A zero \/
% 0.56/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.56/0.90     in_environment $A
% 0.56/0.90       (cardinality_at_time first_movers (appear an_organisation sk2))
% 0.56/0.90  |- ~environment $A \/
% 0.56/0.90     ~greater_or_equal zero
% 0.56/0.90        (cardinality_at_time first_movers (appear an_organisation sk2)) \/
% 0.56/0.90     ~in_environment $A zero \/
% 0.56/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.56/0.90     in_environment $A
% 0.56/0.90       (cardinality_at_time first_movers (appear an_organisation sk2))
% 0.56/0.90  |- ~greater_or_equal sk3
% 0.56/0.90        (cardinality_at_time efficient_producers
% 0.56/0.90           (appear an_organisation sk2)) \/ ~in_environment sk2 zero \/
% 0.56/0.90     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.56/0.90     in_environment sk2
% 0.56/0.90       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.56/0.90  |- ~environment $A \/
% 0.56/0.90     ~greater_or_equal $C
% 0.56/0.90        (cardinality_at_time efficient_producers
% 0.56/0.90           (appear an_organisation sk2)) \/ ~in_environment $A $C \/
% 0.56/0.90     ~in_environment $A zero \/
% 0.56/0.90     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.56/0.90     in_environment $A
% 0.56/0.90       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.56/0.90  |- ~environment $A \/
% 0.56/0.90     ~greater_or_equal zero
% 0.56/0.90        (cardinality_at_time efficient_producers
% 0.56/0.90           (appear an_organisation sk2)) \/ ~in_environment $A zero \/
% 0.56/0.90     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.56/0.90     in_environment $A
% 0.56/0.90       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.66/0.90  |- ~greater zero $C \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.90     greater (cardinality_at_time first_movers (appear an_organisation sk2))
% 0.66/0.90       $C
% 0.66/0.90  |- ~(cardinality_at_time $D (appear an_organisation sk2) = zero) \/
% 0.66/0.90     ~environment $A \/ ~subpopulation $D $A (appear an_organisation sk2) \/
% 0.66/0.90     ~subpopulation first_movers $A (appear an_organisation sk2) \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.90     selection_favors first_movers $D (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.90     greater zero zero
% 0.66/0.90  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.66/0.90       zero) \/ appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.90       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.66/0.90  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.66/0.90       zero) \/
% 0.66/0.90     ~greater (cardinality_at_time $_164 (appear an_organisation sk2))
% 0.66/0.90        zero \/ ~subpopulation $_164 sk2 (appear an_organisation sk2) \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero \/
% 0.66/0.90     selection_favors $_164 (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- ~greater_or_equal sk3
% 0.66/0.90        (cardinality_at_time efficient_producers
% 0.66/0.90           (appear an_organisation sk2)) \/ ~in_environment sk2 zero \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero \/
% 0.66/0.90     in_environment sk2
% 0.66/0.90       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.90          (appear an_organisation sk2))
% 0.66/0.90  |- ~greater $A
% 0.66/0.90        (cardinality_at_time efficient_producers
% 0.66/0.90           (appear an_organisation sk2)) \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater $A zero \/ greater zero zero
% 0.66/0.90  |- ~(cardinality_at_time efficient_producers t = zero) \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero \/
% 0.66/0.90     greater_or_equal
% 0.66/0.90       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.66/0.90       zero
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater
% 0.66/0.90       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.66/0.90       zero \/ greater zero zero
% 0.66/0.90  |- ~greater zero $C \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater
% 0.66/0.90       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.66/0.90       $C \/ greater zero zero
% 0.66/0.90  |- ~(cardinality_at_time $D (appear an_organisation sk2) = zero) \/
% 0.66/0.90     ~environment $A \/ ~subpopulation $D $A (appear an_organisation sk2) \/
% 0.66/0.90     ~subpopulation efficient_producers $A (appear an_organisation sk2) \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero \/
% 0.66/0.90     selection_favors efficient_producers $D (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/ greater zero zero
% 0.66/0.90  |- ~(cardinality_at_time first_movers sk3 = zero) \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors efficient_producers first_movers sk3
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors efficient_producers efficient_producers
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors first_movers first_movers (appear an_organisation sk2)
% 0.66/0.90  |- ~(cardinality_at_time first_movers t = zero) \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors efficient_producers efficient_producers
% 0.66/0.90       (appear first_movers sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     appear first_movers sk2 = start_time sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors efficient_producers efficient_producers
% 0.66/0.90       (start_time sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     appear first_movers sk2 = start_time sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors first_movers first_movers (start_time sk2)
% 0.66/0.90  |- ~(cardinality_at_time first_movers sk3 = zero) \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors first_movers first_movers sk3
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors efficient_producers efficient_producers sk3
% 0.66/0.90  |- ~(cardinality_at_time efficient_producers t = zero) \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2
% 0.66/0.90  |- ~greater_or_equal sk3
% 0.66/0.90        (cardinality_at_time efficient_producers
% 0.66/0.90           (appear an_organisation sk2)) \/ ~in_environment sk2 zero \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero \/
% 0.66/0.90     in_environment sk2
% 0.66/0.90       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.66/0.90  |- ~environment $A \/
% 0.66/0.90     ~greater_or_equal $C
% 0.66/0.90        (cardinality_at_time efficient_producers
% 0.66/0.90           (appear an_organisation sk2)) \/ ~in_environment $A $C \/
% 0.66/0.90     ~in_environment $A zero \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero \/
% 0.66/0.90     in_environment $A
% 0.66/0.90       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.66/0.90  |- ~environment $A \/
% 0.66/0.90     ~greater_or_equal zero
% 0.66/0.90        (cardinality_at_time efficient_producers
% 0.66/0.90           (appear an_organisation sk2)) \/ ~in_environment $A zero \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero \/
% 0.66/0.90     in_environment $A
% 0.66/0.90       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.90       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors efficient_producers
% 0.66/0.90       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.90       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.90     selection_favors first_movers (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.90     selection_favors first_movers first_movers (appear an_organisation sk2)
% 0.66/0.90  |- ~greater_or_equal sk3 zero \/ ~in_environment sk2 zero \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     in_environment sk2
% 0.66/0.90       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.66/0.90  |- ~greater_or_equal sk3 zero \/ ~in_environment sk2 zero \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.90     in_environment sk2
% 0.66/0.90       (cardinality_at_time first_movers (appear an_organisation sk2))
% 0.66/0.90  |- ~greater_or_equal sk3 zero \/ ~in_environment sk2 zero \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     in_environment sk2
% 0.66/0.90       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.90          (appear an_organisation sk2))
% 0.66/0.90  |- ~greater_or_equal sk3 zero \/ ~in_environment sk2 zero \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.90     in_environment sk2
% 0.66/0.90       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.90          (appear an_organisation sk2))
% 0.66/0.90  |- ~(cardinality_at_time $_199 (appear an_organisation sk2) = zero) \/
% 0.66/0.90     ~subpopulation $_199 sk2 (appear an_organisation sk2) \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2) $_199
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- ~(cardinality_at_time $_199 (appear an_organisation sk2) = zero) \/
% 0.66/0.90     ~environment $_198 \/
% 0.66/0.90     ~subpopulation $_199 $_198 (appear an_organisation sk2) \/
% 0.66/0.90     ~subpopulation efficient_producers $_198 (appear an_organisation sk2) \/
% 0.66/0.90     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2) $_199
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- ~(cardinality_at_time $_199 (appear an_organisation sk2) = zero) \/
% 0.66/0.90     ~environment $_198 \/
% 0.66/0.90     ~subpopulation $_199 $_198 (appear an_organisation sk2) \/
% 0.66/0.90     ~subpopulation first_movers $_198 (appear an_organisation sk2) \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2) $_199
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- ~(cardinality_at_time $_199 (appear an_organisation sk2) = zero) \/
% 0.66/0.90     ~environment $_198 \/
% 0.66/0.90     ~subpopulation $_199 $_198 (appear an_organisation sk2) \/
% 0.66/0.90     ~subpopulation efficient_producers $_198 (appear an_organisation sk2) \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2) $_199
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.66/0.90       zero) \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.90       efficient_producers (appear an_organisation sk2)
% 0.66/0.90  |- ~(cardinality_at_time first_movers (appear an_organisation sk2) =
% 0.66/0.90       zero) \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2) first_movers
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.90       efficient_producers (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     selection_favors (sk1 (appear an_organisation sk2) sk2) first_movers
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     greater zero zero \/
% 0.66/0.90     selection_favors efficient_producers first_movers
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.90     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.90     selection_favors efficient_producers first_movers
% 0.66/0.90       (appear an_organisation sk2)
% 0.66/0.90  |- ~(cardinality_at_time $_202 (appear first_movers sk2) = zero) \/
% 0.66/0.90     ~subpopulation $_202 sk2 (appear first_movers sk2) \/
% 0.66/0.90     selection_favors (sk1 (appear first_movers sk2) sk2) $_202
% 0.66/0.90       (appear first_movers sk2)
% 0.66/0.90  |- ~(cardinality_at_time $_202 (appear first_movers sk2) = zero) \/
% 0.66/0.90     ~environment $_201 \/
% 0.66/0.90     ~subpopulation $_202 $_201 (appear first_movers sk2) \/
% 0.66/0.90     ~subpopulation first_movers $_201 (appear first_movers sk2) \/
% 0.66/0.90     sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.66/0.90     selection_favors (sk1 (appear first_movers sk2) sk2) $_202
% 0.66/0.90       (appear first_movers sk2)
% 0.66/0.90  |- ~(cardinality_at_time $_202 (appear first_movers sk2) = zero) \/
% 0.66/0.90     ~environment $_201 \/
% 0.66/0.90     ~subpopulation $_202 $_201 (appear first_movers sk2) \/
% 0.66/0.90     ~subpopulation first_movers $_201 (appear first_movers sk2) \/
% 0.66/0.90     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.66/0.90     selection_favors (sk1 (appear first_movers sk2) sk2) $_202
% 0.66/0.90       (appear first_movers sk2)
% 0.66/0.90  |- ~(cardinality_at_time $_202 (appear first_movers sk2) = zero) \/
% 0.66/0.90     ~environment $_201 \/
% 0.66/0.90     ~subpopulation $_202 $_201 (appear first_movers sk2) \/
% 0.66/0.90     ~subpopulation efficient_producers $_201 (appear first_movers sk2) \/
% 0.66/0.90     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.66/0.90     selection_favors (sk1 (appear first_movers sk2) sk2) $_202
% 0.66/0.90       (appear first_movers sk2)
% 0.66/0.90  |- ~(cardinality_at_time efficient_producers (appear first_movers sk2) =
% 0.66/0.90       zero) \/
% 0.66/0.90     selection_favors (sk1 (appear first_movers sk2) sk2) efficient_producers
% 0.66/0.90       (appear first_movers sk2)
% 0.66/0.91  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.66/0.91     selection_favors (sk1 (appear first_movers sk2) sk2) first_movers
% 0.66/0.91       (appear first_movers sk2)
% 0.66/0.91  |- sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors (sk1 (appear first_movers sk2) sk2) efficient_producers
% 0.66/0.91       (appear first_movers sk2)
% 0.66/0.91  |- sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.66/0.91     selection_favors first_movers efficient_producers
% 0.66/0.91       (appear first_movers sk2)
% 0.66/0.91  |- sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors first_movers efficient_producers
% 0.66/0.91       (appear first_movers sk2)
% 0.66/0.91  |- ~environment $_210 \/
% 0.66/0.91     ~greater_or_equal zero
% 0.66/0.91        (cardinality_at_time efficient_producers
% 0.66/0.91           (appear an_organisation sk2)) \/ ~in_environment $_210 zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     greater zero zero \/
% 0.66/0.91     in_environment $_210
% 0.66/0.91       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91          (appear an_organisation sk2))
% 0.66/0.91  |- ~environment $_210 \/
% 0.66/0.91     ~greater_or_equal zero
% 0.66/0.91        (cardinality_at_time first_movers (appear an_organisation sk2)) \/
% 0.66/0.91     ~in_environment $_210 zero \/
% 0.66/0.91     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.91     in_environment $_210
% 0.66/0.91       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91          (appear an_organisation sk2))
% 0.66/0.91  |- ~environment $_210 \/
% 0.66/0.91     ~greater_or_equal zero
% 0.66/0.91        (cardinality_at_time efficient_producers
% 0.66/0.91           (appear an_organisation sk2)) \/ ~in_environment $_210 zero \/
% 0.66/0.91     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.91     in_environment $_210
% 0.66/0.91       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91          (appear an_organisation sk2))
% 0.66/0.91  |- ~(cardinality_at_time $_214 (start_time sk2) = zero) \/
% 0.66/0.91     ~greater zero zero \/ ~subpopulation $_214 sk2 (start_time sk2) \/
% 0.66/0.91     appear first_movers sk2 = start_time sk2 \/
% 0.66/0.91     selection_favors first_movers $_214 (start_time sk2)
% 0.66/0.91  |- ~(cardinality_at_time efficient_producers (start_time sk2) = zero) \/
% 0.66/0.91     ~greater zero zero \/ appear first_movers sk2 = start_time sk2 \/
% 0.66/0.91     selection_favors first_movers efficient_producers (start_time sk2)
% 0.66/0.91  |- ~greater zero zero \/ appear first_movers sk2 = start_time sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors first_movers efficient_producers (start_time sk2)
% 0.66/0.91  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     appear first_movers sk2 = start_time sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors first_movers efficient_producers (start_time sk2)
% 0.66/0.91  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.66/0.91     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.66/0.91     selection_favors first_movers first_movers (appear first_movers sk2)
% 0.66/0.91  |- ~environment $_224 \/ ~in_environment $_224 zero \/
% 0.66/0.91     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     in_environment $_224
% 0.66/0.91       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.91          (appear first_movers sk2))
% 0.66/0.91  |- ~(cardinality_at_time $_227 sk3 = zero) \/
% 0.66/0.91     ~subpopulation $_227 sk2 sk3 \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors (sk1 sk3 sk2) $_227 sk3
% 0.66/0.91  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors (sk1 sk3 sk2) efficient_producers sk3
% 0.66/0.91  |- ~(cardinality_at_time first_movers sk3 = zero) \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors (sk1 sk3 sk2) first_movers sk3
% 0.66/0.91  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk1 sk3 sk2 = efficient_producers \/ sk3 = appear first_movers sk2
% 0.66/0.91  |- ~(cardinality_at_time $_166 sk3 = zero) \/ ~environment $_163 \/
% 0.66/0.91     ~subpopulation $_166 $_163 sk3 \/
% 0.66/0.91     ~subpopulation efficient_producers $_163 sk3 \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors (sk1 sk3 sk2) $_166 sk3
% 0.66/0.91  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors (sk1 sk3 sk2) (sk1 sk3 sk2) sk3
% 0.66/0.91  |- ~environment $_51 \/ ~in_environment $_51 zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     in_environment $_51 (cardinality_at_time (sk1 sk3 sk2) sk3)
% 0.66/0.91  |- ~greater_or_equal sk3 zero \/ ~in_environment sk2 zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     in_environment sk2 (cardinality_at_time (sk1 sk3 sk2) sk3)
% 0.66/0.91  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers (sk1 sk3 sk2) sk3
% 0.66/0.91  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.66/0.91     ~greater zero zero \/ sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers first_movers
% 0.66/0.91       (appear first_movers sk2)
% 0.66/0.91  |- ~(cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.91         (appear first_movers sk2) = zero) \/ ~greater zero zero \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers (sk1 (appear first_movers sk2) sk2)
% 0.66/0.91       (appear first_movers sk2)
% 0.66/0.91  |- ~(cardinality_at_time $_231 (appear first_movers sk2) = zero) \/
% 0.66/0.91     ~greater zero zero \/
% 0.66/0.91     ~subpopulation $_231 sk2 (appear first_movers sk2) \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers $_231 (appear first_movers sk2)
% 0.66/0.91  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.66/0.91     ~greater zero zero \/
% 0.66/0.91     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers (sk1 (appear first_movers sk2) sk2)
% 0.66/0.91       (appear first_movers sk2)
% 0.66/0.91  |- ~environment $_233 \/ ~in_environment $_233 zero \/
% 0.66/0.91     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     in_environment $_233
% 0.66/0.91       (cardinality_at_time efficient_producers (appear first_movers sk2))
% 0.66/0.91  |- ~environment $_241 \/ ~in_environment $_241 zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     in_environment $_241
% 0.66/0.91       (cardinality_at_time efficient_producers (appear an_organisation sk2))
% 0.66/0.91  |- ~(cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91         (appear an_organisation sk2) = zero) \/ ~greater zero zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     selection_favors first_movers (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91       (appear an_organisation sk2)
% 0.66/0.91  |- ~(cardinality_at_time $_244 (appear an_organisation sk2) = zero) \/
% 0.66/0.91     ~greater zero zero \/
% 0.66/0.91     ~subpopulation $_244 sk2 (appear an_organisation sk2) \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     selection_favors first_movers $_244 (appear an_organisation sk2)
% 0.66/0.91  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.66/0.91       zero) \/ ~greater zero zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.91     selection_favors first_movers (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91       (appear an_organisation sk2)
% 0.66/0.91  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors first_movers (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91       (appear an_organisation sk2)
% 0.66/0.91  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.66/0.91       zero) \/ ~greater zero zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     selection_favors first_movers efficient_producers
% 0.66/0.91       (appear an_organisation sk2)
% 0.66/0.91  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors first_movers efficient_producers
% 0.66/0.91       (appear an_organisation sk2)
% 0.66/0.91  |- ~environment $_246 \/ ~in_environment $_246 zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     in_environment $_246
% 0.66/0.91       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91          (appear an_organisation sk2))
% 0.66/0.91  |- ~environment $_247 \/ ~in_environment $_247 zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.91     in_environment $_247
% 0.66/0.91       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91          (appear an_organisation sk2))
% 0.66/0.91  |- ~environment $_249 \/ ~in_environment $_249 zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.91     in_environment $_249
% 0.66/0.91       (cardinality_at_time first_movers (appear an_organisation sk2))
% 0.66/0.91  |- ~(cardinality_at_time efficient_producers (appear first_movers sk2) =
% 0.66/0.91       zero) \/ sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.66/0.91     selection_favors efficient_producers efficient_producers
% 0.66/0.91       (appear first_movers sk2)
% 0.66/0.91  |- ~(cardinality_at_time $_255 (start_time sk2) = zero) \/
% 0.66/0.91     ~greater zero zero \/ ~subpopulation $_255 sk2 (start_time sk2) \/
% 0.66/0.91     appear first_movers sk2 = start_time sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers $_255 (start_time sk2)
% 0.66/0.91  |- ~greater zero zero \/ appear first_movers sk2 = start_time sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers first_movers (start_time sk2)
% 0.66/0.91  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     appear first_movers sk2 = start_time sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers first_movers (start_time sk2)
% 0.66/0.91  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.66/0.91     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.66/0.91     selection_favors first_movers (sk1 (appear first_movers sk2) sk2)
% 0.66/0.91       (appear first_movers sk2)
% 0.66/0.91  |- ~(cardinality_at_time first_movers (appear an_organisation sk2) =
% 0.66/0.91       zero) \/ sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.91     selection_favors first_movers first_movers (appear an_organisation sk2)
% 0.66/0.91  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.66/0.91       zero) \/ sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.91     selection_favors efficient_producers efficient_producers
% 0.66/0.91       (appear an_organisation sk2)
% 0.66/0.91  |- ~(cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91         (appear an_organisation sk2) = zero) \/ ~greater zero zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers
% 0.66/0.91       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.66/0.91  |- ~(cardinality_at_time $_270 (appear an_organisation sk2) = zero) \/
% 0.66/0.91     ~greater zero zero \/
% 0.66/0.91     ~subpopulation $_270 sk2 (appear an_organisation sk2) \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers $_270 (appear an_organisation sk2)
% 0.66/0.91  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers first_movers
% 0.66/0.91       (appear an_organisation sk2)
% 0.66/0.91  |- appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/
% 0.66/0.91     selection_favors efficient_producers
% 0.66/0.91       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.66/0.91  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.66/0.91     selection_favors first_movers first_movers (appear first_movers sk2)
% 0.66/0.91  |- ~(cardinality_at_time efficient_producers (appear first_movers sk2) =
% 0.66/0.91       zero) \/ sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.66/0.91     selection_favors efficient_producers (sk1 (appear first_movers sk2) sk2)
% 0.66/0.91       (appear first_movers sk2)
% 0.66/0.91  |- ~environment $_284 \/
% 0.66/0.91     ~greater_or_equal $_285
% 0.66/0.91        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.66/0.91     ~in_environment $_284 $_285 \/ ~in_environment $_284 zero \/
% 0.66/0.91     sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.66/0.91     in_environment $_284
% 0.66/0.91       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.91          (appear first_movers sk2))
% 0.66/0.91  |- ~environment $_284 \/
% 0.66/0.91     ~greater_or_equal $_285
% 0.66/0.91        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.66/0.91     ~in_environment $_284 $_285 \/ ~in_environment $_284 zero \/
% 0.66/0.91     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.66/0.91     in_environment $_284
% 0.66/0.91       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.91          (appear first_movers sk2))
% 0.66/0.91  |- ~environment $_284 \/
% 0.66/0.91     ~greater_or_equal $_285
% 0.66/0.91        (cardinality_at_time efficient_producers
% 0.66/0.91           (appear first_movers sk2)) \/ ~in_environment $_284 $_285 \/
% 0.66/0.91     ~in_environment $_284 zero \/
% 0.66/0.91     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.66/0.91     in_environment $_284
% 0.66/0.91       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.91          (appear first_movers sk2))
% 0.66/0.91  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.66/0.91       zero) \/ sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.91     selection_favors efficient_producers
% 0.66/0.91       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.66/0.91  |- ~(cardinality_at_time first_movers (appear an_organisation sk2) =
% 0.66/0.91       zero) \/ sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.91     selection_favors first_movers (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91       (appear an_organisation sk2)
% 0.66/0.91  |- ~environment $_289 \/
% 0.66/0.91     ~greater_or_equal $_290
% 0.66/0.91        (cardinality_at_time efficient_producers
% 0.66/0.91           (appear an_organisation sk2)) \/ ~in_environment $_289 $_290 \/
% 0.66/0.91     ~in_environment $_289 zero \/
% 0.66/0.91     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.91     greater zero zero \/
% 0.66/0.91     in_environment $_289
% 0.66/0.91       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91          (appear an_organisation sk2))
% 0.66/0.91  |- ~environment $_289 \/
% 0.66/0.91     ~greater_or_equal $_290
% 0.66/0.91        (cardinality_at_time first_movers (appear an_organisation sk2)) \/
% 0.66/0.91     ~in_environment $_289 $_290 \/ ~in_environment $_289 zero \/
% 0.66/0.91     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.91     in_environment $_289
% 0.66/0.91       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.91          (appear an_organisation sk2))
% 0.66/0.92  |- ~environment $_289 \/
% 0.66/0.92     ~greater_or_equal $_290
% 0.66/0.92        (cardinality_at_time efficient_producers
% 0.66/0.92           (appear an_organisation sk2)) \/ ~in_environment $_289 $_290 \/
% 0.66/0.92     ~in_environment $_289 zero \/
% 0.66/0.92     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.92     in_environment $_289
% 0.66/0.92       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.92          (appear an_organisation sk2))
% 0.66/0.92  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.66/0.92     sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.66/0.92     selection_favors first_movers (sk1 (appear first_movers sk2) sk2)
% 0.66/0.92       (appear first_movers sk2)
% 0.66/0.92  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.66/0.92       zero) \/ appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.92     greater zero zero \/
% 0.66/0.92     selection_favors efficient_producers efficient_producers
% 0.66/0.92       (appear an_organisation sk2)
% 0.66/0.92  |- ~environment $_297 \/
% 0.66/0.92     ~in_environment $_297
% 0.66/0.92        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.66/0.92     ~in_environment $_297 zero \/
% 0.66/0.92     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.66/0.92     in_environment $_297
% 0.66/0.92       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.92          (appear first_movers sk2))
% 0.66/0.92  |- ~environment $_300 \/
% 0.66/0.92     ~in_environment $_300
% 0.66/0.92        (cardinality_at_time efficient_producers
% 0.66/0.92           (appear first_movers sk2)) \/ ~in_environment $_300 zero \/
% 0.66/0.92     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.66/0.92     in_environment $_300
% 0.66/0.92       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.92          (appear first_movers sk2))
% 0.66/0.92  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.66/0.92       zero) \/ appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.92     greater zero zero \/
% 0.66/0.92     selection_favors efficient_producers
% 0.66/0.92       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.66/0.92  |- ~environment $_308 \/
% 0.66/0.92     ~in_environment $_308
% 0.66/0.92        (cardinality_at_time efficient_producers
% 0.66/0.92           (appear an_organisation sk2)) \/ ~in_environment $_308 zero \/
% 0.66/0.92     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.92     in_environment $_308
% 0.66/0.92       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.92          (appear an_organisation sk2))
% 0.66/0.92  |- ~environment $_311 \/
% 0.66/0.92     ~in_environment $_311
% 0.66/0.92        (cardinality_at_time first_movers (appear an_organisation sk2)) \/
% 0.66/0.92     ~in_environment $_311 zero \/
% 0.66/0.92     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.92     in_environment $_311
% 0.66/0.92       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.92          (appear an_organisation sk2))
% 0.66/0.92  |- ~(cardinality_at_time first_movers (appear first_movers sk2) = zero) \/
% 0.66/0.92     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.66/0.92     selection_favors efficient_producers first_movers
% 0.66/0.92       (appear first_movers sk2)
% 0.66/0.92  |- ~(cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.92         (appear first_movers sk2) = zero) \/
% 0.66/0.92     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.66/0.92     selection_favors efficient_producers (sk1 (appear first_movers sk2) sk2)
% 0.66/0.92       (appear first_movers sk2)
% 0.66/0.92  |- ~(cardinality_at_time $_315 (appear first_movers sk2) = zero) \/
% 0.66/0.92     ~subpopulation $_315 sk2 (appear first_movers sk2) \/
% 0.66/0.92     sk1 (appear first_movers sk2) sk2 = first_movers \/
% 0.66/0.92     selection_favors efficient_producers $_315 (appear first_movers sk2)
% 0.66/0.92  |- ~(cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.92         (appear first_movers sk2) = zero) \/
% 0.66/0.92     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.66/0.92     selection_favors first_movers (sk1 (appear first_movers sk2) sk2)
% 0.66/0.92       (appear first_movers sk2)
% 0.66/0.92  |- ~(cardinality_at_time $_318 (appear first_movers sk2) = zero) \/
% 0.66/0.92     ~subpopulation $_318 sk2 (appear first_movers sk2) \/
% 0.66/0.92     sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.66/0.92     selection_favors first_movers $_318 (appear first_movers sk2)
% 0.66/0.92  |- ~(cardinality_at_time efficient_producers (appear first_movers sk2) =
% 0.66/0.92       zero) \/ sk1 (appear first_movers sk2) sk2 = efficient_producers \/
% 0.66/0.92     selection_favors first_movers efficient_producers
% 0.66/0.92       (appear first_movers sk2)
% 0.66/0.92  |- ~environment $_320 \/
% 0.66/0.92     ~in_environment $_320
% 0.66/0.92        (cardinality_at_time first_movers (appear first_movers sk2)) \/
% 0.66/0.92     ~in_environment $_320 zero \/ sk3 = appear first_movers sk2 \/
% 0.66/0.92     greater zero zero \/
% 0.66/0.92     in_environment $_320
% 0.66/0.92       (cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.92          (appear first_movers sk2))
% 0.66/0.92  |- ~(cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.92         (appear an_organisation sk2) = zero) \/
% 0.66/0.92     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.92     selection_favors first_movers (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.92       (appear an_organisation sk2)
% 0.66/0.92  |- ~(cardinality_at_time $_324 (appear an_organisation sk2) = zero) \/
% 0.66/0.92     ~subpopulation $_324 sk2 (appear an_organisation sk2) \/
% 0.66/0.92     sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.92     selection_favors first_movers $_324 (appear an_organisation sk2)
% 0.66/0.92  |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) =
% 0.66/0.92       zero) \/ sk1 (appear an_organisation sk2) sk2 = efficient_producers \/
% 0.66/0.92     selection_favors first_movers efficient_producers
% 0.66/0.92       (appear an_organisation sk2)
% 0.66/0.92  |- ~(cardinality_at_time first_movers (appear an_organisation sk2) =
% 0.66/0.92       zero) \/ sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.92     selection_favors efficient_producers first_movers
% 0.66/0.92       (appear an_organisation sk2)
% 0.66/0.92  |- ~(cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.92         (appear an_organisation sk2) = zero) \/
% 0.66/0.92     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.92     selection_favors efficient_producers
% 0.66/0.92       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.66/0.92  |- ~(cardinality_at_time $_327 (appear an_organisation sk2) = zero) \/
% 0.66/0.92     ~subpopulation $_327 sk2 (appear an_organisation sk2) \/
% 0.66/0.92     sk1 (appear an_organisation sk2) sk2 = first_movers \/
% 0.66/0.92     selection_favors efficient_producers $_327 (appear an_organisation sk2)
% 0.66/0.92  |- ~environment $_331 \/
% 0.66/0.92     ~in_environment $_331
% 0.66/0.92        (cardinality_at_time efficient_producers
% 0.66/0.92           (appear an_organisation sk2)) \/ ~in_environment $_331 zero \/
% 0.66/0.92     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.92     greater zero zero \/
% 0.66/0.92     in_environment $_331
% 0.66/0.92       (cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.92          (appear an_organisation sk2))
% 0.66/0.92  |- ~(cardinality_at_time (sk1 (appear first_movers sk2) sk2)
% 0.66/0.92         (appear first_movers sk2) = zero) \/
% 0.66/0.92     sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.66/0.92     selection_favors first_movers (sk1 (appear first_movers sk2) sk2)
% 0.66/0.92       (appear first_movers sk2)
% 0.66/0.92  |- ~(cardinality_at_time $_337 (appear first_movers sk2) = zero) \/
% 0.66/0.92     ~subpopulation $_337 sk2 (appear first_movers sk2) \/
% 0.66/0.92     sk3 = appear first_movers sk2 \/ greater zero zero \/
% 0.66/0.92     selection_favors first_movers $_337 (appear first_movers sk2)
% 0.66/0.92  |- ~(cardinality_at_time (sk1 (appear an_organisation sk2) sk2)
% 0.66/0.92         (appear an_organisation sk2) = zero) \/
% 0.66/0.92     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.92     greater zero zero \/
% 0.66/0.92     selection_favors efficient_producers
% 0.66/0.92       (sk1 (appear an_organisation sk2) sk2) (appear an_organisation sk2)
% 0.66/0.92  |- ~(cardinality_at_time $_340 (appear an_organisation sk2) = zero) \/
% 0.66/0.92     ~subpopulation $_340 sk2 (appear an_organisation sk2) \/
% 0.66/0.92     appear first_movers sk2 = appear an_organisation sk2 \/
% 0.66/0.92     greater zero zero \/
% 0.66/0.92     selection_favors efficient_producers $_340 (appear an_organisation sk2)
% 0.66/0.92  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.66/0.92  
%------------------------------------------------------------------------------