%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : MGT033+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n020.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 : CounterSatisfiable 0.56s 0.89s % Output : Saturation 0.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT033+2 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : metis --show proof --show saturation %s % 0.11/0.37 % Computer : n020.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Mon Sep 7 12:26:43 UTC 2026 % 0.11/0.37 % CPUTime : % 0.11/0.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.56/0.89 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.56/0.89 % 0.56/0.89 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.56/0.89 |- ~(cardinality_at_time $S2 $T = zero) \/ ~environment $E \/ % 0.56/0.89 ~greater (cardinality_at_time $S1 $T) zero \/ % 0.56/0.89 ~subpopulation $S1 $E $T \/ ~subpopulation $S2 $E $T \/ % 0.56/0.89 selection_favors $S1 $S2 $T % 0.56/0.89 |- ~environment $E \/ ~greater (number_of_organizations $E $T) zero \/ % 0.56/0.89 greater (cardinality_at_time (skolemFOFtoCNF_S $E $T) $T) zero % 0.56/0.89 |- ~environment $E \/ ~greater (number_of_organizations $E $T) zero \/ % 0.56/0.89 subpopulation (skolemFOFtoCNF_S $E $T) $E $T % 0.56/0.89 |- ~(cardinality_at_time $X t = zero) \/ % 0.56/0.89 ~greater (cardinality_at_time $X $T) zero % 0.56/0.89 |- ~environment $E \/ ~greater (appear $X $E) $T \/ % 0.56/0.89 ~in_environment $E $T \/ cardinality_at_time $X $T = zero % 0.56/0.89 |- ~environment $E \/ ~greater (number_of_organizations $E $T) zero \/ % 0.56/0.89 in_environment $E $T % 0.56/0.89 |- ~environment $E \/ ~greater_or_equal $T $T1 \/ % 0.56/0.89 ~greater_or_equal $T2 $T \/ ~in_environment $E $T1 \/ % 0.56/0.89 ~in_environment $E $T2 \/ in_environment $E $T % 0.56/0.89 |- ~environment $E \/ in_environment $E (start_time $E) % 0.56/0.89 |- ~environment $E \/ % 0.56/0.89 greater_or_equal (appear first_movers $E) (start_time $E) % 0.56/0.89 |- ~environment $E \/ ~in_environment $E (appear first_movers $E) \/ % 0.56/0.89 in_environment $E (appear an_organisation $E) % 0.56/0.89 |- ~environment $E \/ % 0.56/0.89 greater_or_equal (appear first_movers $E) (appear an_organisation $E) % 0.56/0.89 |- ~environment $E \/ % 0.56/0.89 greater (number_of_organizations e (appear an_organisation $E)) zero % 0.56/0.89 |- ~environment $E \/ ~in_environment $E $T \/ % 0.56/0.89 subpopulation efficient_producers $E $T % 0.56/0.89 |- ~environment $E \/ ~in_environment $E $T \/ % 0.56/0.89 subpopulation first_movers $E $T % 0.56/0.89 |- ~greater $X $Y \/ ~greater $Y $Z \/ greater $X $Z % 0.56/0.89 |- greater_or_equal $Y $Y % 0.56/0.89 |- ~greater $X $Y \/ greater_or_equal $X $Y % 0.56/0.89 |- ~greater_or_equal $X $Y \/ $X = $Y \/ greater $X $Y % 0.56/0.89 |- ~environment $E \/ ~greater_or_equal $T (appear an_organisation $E) \/ % 0.56/0.89 ~in_environment $E $T \/ greater (number_of_organizations $E $T) zero % 0.56/0.89 |- ~environment $E \/ % 0.56/0.89 greater (appear efficient_producers e) (appear first_movers $E) % 0.56/0.89 |- ~environment $E \/ ~greater (cardinality_at_time $X $T) zero \/ % 0.56/0.89 ~subpopulation $X $E $T \/ $X = efficient_producers \/ $X = first_movers % 0.56/0.89 |- ~(cardinality_at_time $S2 $T = zero) \/ ~environment $E \/ % 0.56/0.89 ~greater zero zero \/ ~subpopulation $S2 $E $T \/ % 0.56/0.89 selection_favors $S2 $S2 $T % 0.56/0.89 |- ~environment $E \/ ~greater_or_equal $T $T2 \/ % 0.56/0.89 ~greater_or_equal $T2 $T \/ ~in_environment $E $T2 \/ % 0.56/0.89 in_environment $E $T % 0.56/0.89 |- ~selection_favors first_movers efficient_producers skolemFOFtoCNF_T % 0.56/0.89 |- environment skolemFOFtoCNF_E % 0.56/0.89 |- greater (appear efficient_producers skolemFOFtoCNF_E) skolemFOFtoCNF_T % 0.56/0.89 |- greater_or_equal skolemFOFtoCNF_T (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 |- in_environment skolemFOFtoCNF_E skolemFOFtoCNF_T % 0.56/0.89 |- in_environment skolemFOFtoCNF_E (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- greater (appear efficient_producers e) % 0.56/0.89 (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 |- greater_or_equal (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- greater_or_equal (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- greater % 0.56/0.89 (number_of_organizations e (appear an_organisation skolemFOFtoCNF_E)) % 0.56/0.89 zero % 0.56/0.89 |- greater_or_equal (appear efficient_producers e) % 0.56/0.89 (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 |- greater_or_equal (appear efficient_producers skolemFOFtoCNF_E) % 0.56/0.89 skolemFOFtoCNF_T % 0.56/0.89 |- greater_or_equal % 0.56/0.89 (number_of_organizations e (appear an_organisation skolemFOFtoCNF_E)) % 0.56/0.89 zero % 0.56/0.89 |- ~environment e \/ % 0.56/0.89 in_environment e (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- subpopulation efficient_producers skolemFOFtoCNF_E skolemFOFtoCNF_T % 0.56/0.89 |- subpopulation efficient_producers skolemFOFtoCNF_E % 0.56/0.89 (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- subpopulation first_movers skolemFOFtoCNF_E skolemFOFtoCNF_T % 0.56/0.89 |- subpopulation first_movers skolemFOFtoCNF_E % 0.56/0.89 (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater skolemFOFtoCNF_T (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater (appear first_movers skolemFOFtoCNF_E) $_21 \/ % 0.56/0.89 greater (appear efficient_producers e) $_21 % 0.56/0.89 |- ~greater skolemFOFtoCNF_T $_21 \/ % 0.56/0.89 greater (appear efficient_producers skolemFOFtoCNF_E) $_21 % 0.56/0.89 |- ~greater (appear an_organisation skolemFOFtoCNF_E) $_21 \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear first_movers skolemFOFtoCNF_E) $_21 % 0.56/0.89 |- ~greater (start_time skolemFOFtoCNF_E) $_21 \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear first_movers skolemFOFtoCNF_E) $_21 % 0.56/0.89 |- ~greater zero $_21 \/ % 0.56/0.89 greater % 0.56/0.89 (number_of_organizations e (appear an_organisation skolemFOFtoCNF_E)) % 0.56/0.89 $_21 % 0.56/0.89 |- ~greater $_19 (appear efficient_producers e) \/ % 0.56/0.89 greater $_19 (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater $_19 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.56/0.89 greater $_19 skolemFOFtoCNF_T % 0.56/0.89 |- ~greater $_19 (appear first_movers skolemFOFtoCNF_E) \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 greater $_19 (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater $_19 (appear first_movers skolemFOFtoCNF_E) \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 greater $_19 (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater $_19 % 0.56/0.89 (number_of_organizations e % 0.56/0.89 (appear an_organisation skolemFOFtoCNF_E)) \/ greater $_19 zero % 0.56/0.89 |- ~greater $_19 skolemFOFtoCNF_T \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater $_19 (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 |- skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear efficient_producers skolemFOFtoCNF_E) % 0.56/0.89 (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater $X (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater $X (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater (appear first_movers skolemFOFtoCNF_E) $Z \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear efficient_producers skolemFOFtoCNF_E) $Z % 0.56/0.89 |- skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater_or_equal (appear efficient_producers skolemFOFtoCNF_E) % 0.56/0.89 (appear first_movers skolemFOFtoCNF_E) % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear efficient_producers e) % 0.56/0.89 (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear efficient_producers e) (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater $X (appear efficient_producers e) \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 greater $X (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater (start_time skolemFOFtoCNF_E) $Z \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear efficient_producers e) $Z % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 greater_or_equal (appear efficient_producers e) % 0.56/0.89 (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater $X (appear efficient_producers e) \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 greater $X (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater (appear an_organisation skolemFOFtoCNF_E) $Z \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear efficient_producers e) $Z % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 greater_or_equal (appear efficient_producers e) % 0.56/0.89 (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- ~environment e \/ % 0.56/0.89 subpopulation % 0.56/0.89 (skolemFOFtoCNF_S e (appear an_organisation skolemFOFtoCNF_E)) e % 0.56/0.89 (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- ~environment e \/ % 0.56/0.89 greater % 0.56/0.89 (cardinality_at_time % 0.56/0.89 (skolemFOFtoCNF_S e (appear an_organisation skolemFOFtoCNF_E)) % 0.56/0.89 (appear an_organisation skolemFOFtoCNF_E)) zero % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear efficient_producers skolemFOFtoCNF_E) % 0.56/0.89 (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear efficient_producers skolemFOFtoCNF_E) % 0.56/0.89 (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater $X (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater $X (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater (start_time skolemFOFtoCNF_E) $Z \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear efficient_producers skolemFOFtoCNF_E) $Z % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater_or_equal (appear efficient_producers skolemFOFtoCNF_E) % 0.56/0.89 (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater $X (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater $X (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater (appear an_organisation skolemFOFtoCNF_E) $Z \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater (appear efficient_producers skolemFOFtoCNF_E) $Z % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = % 0.56/0.89 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater_or_equal (appear efficient_producers skolemFOFtoCNF_E) % 0.56/0.89 (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.89 |- appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater skolemFOFtoCNF_T (start_time skolemFOFtoCNF_E) % 0.56/0.89 |- ~greater $X skolemFOFtoCNF_T \/ % 0.56/0.89 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.89 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.89 greater $X (start_time skolemFOFtoCNF_E) % 0.56/0.90 |- appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.56/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.90 greater_or_equal skolemFOFtoCNF_T (start_time skolemFOFtoCNF_E) % 0.56/0.90 |- appear first_movers skolemFOFtoCNF_E = % 0.56/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.90 greater skolemFOFtoCNF_T (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.90 |- ~greater $X skolemFOFtoCNF_T \/ % 0.56/0.90 appear first_movers skolemFOFtoCNF_E = % 0.56/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.90 greater $X (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.90 |- appear first_movers skolemFOFtoCNF_E = % 0.56/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.90 greater_or_equal skolemFOFtoCNF_T % 0.56/0.90 (appear an_organisation skolemFOFtoCNF_E) % 0.56/0.90 |- ~in_environment skolemFOFtoCNF_E (appear efficient_producers e) \/ % 0.56/0.90 appear first_movers skolemFOFtoCNF_E = % 0.56/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.90 greater % 0.56/0.90 (number_of_organizations skolemFOFtoCNF_E % 0.56/0.90 (appear efficient_producers e)) zero % 0.56/0.90 |- ~in_environment skolemFOFtoCNF_E % 0.56/0.90 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.56/0.90 appear first_movers skolemFOFtoCNF_E = % 0.56/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.90 greater % 0.56/0.90 (number_of_organizations skolemFOFtoCNF_E % 0.56/0.90 (appear efficient_producers skolemFOFtoCNF_E)) zero % 0.56/0.90 |- appear first_movers skolemFOFtoCNF_E = % 0.56/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.90 greater (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) zero % 0.56/0.90 |- ~environment $_39 \/ % 0.56/0.90 ~in_environment $_39 (appear an_organisation $_39) \/ % 0.56/0.90 greater (number_of_organizations $_39 (appear an_organisation $_39)) % 0.56/0.90 zero % 0.56/0.90 |- ~greater $X % 0.56/0.90 (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) \/ % 0.56/0.90 appear first_movers skolemFOFtoCNF_E = % 0.56/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.56/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.56/0.90 greater $X zero % 0.65/0.90 |- ~greater zero $Z \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 greater (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) $Z % 0.65/0.90 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 greater_or_equal % 0.65/0.90 (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) zero % 0.65/0.90 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 greater % 0.65/0.90 (cardinality_at_time % 0.65/0.90 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.90 skolemFOFtoCNF_T) zero % 0.65/0.90 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 subpopulation (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.90 skolemFOFtoCNF_E skolemFOFtoCNF_T % 0.65/0.90 |- ~greater $X % 0.65/0.90 (cardinality_at_time % 0.65/0.90 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.90 skolemFOFtoCNF_T) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 greater $X zero % 0.65/0.90 |- ~greater zero $Z \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 greater % 0.65/0.90 (cardinality_at_time % 0.65/0.90 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.90 skolemFOFtoCNF_T) $Z % 0.65/0.90 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 greater_or_equal % 0.65/0.90 (cardinality_at_time % 0.65/0.90 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.90 skolemFOFtoCNF_T) zero % 0.65/0.90 |- ~(cardinality_at_time % 0.65/0.90 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) t = zero) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E % 0.65/0.90 |- ~environment e \/ % 0.65/0.90 ~in_environment e (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 cardinality_at_time efficient_producers % 0.65/0.90 (appear an_organisation skolemFOFtoCNF_E) = zero % 0.65/0.90 |- ~environment e \/ % 0.65/0.90 ~in_environment e (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 cardinality_at_time efficient_producers % 0.65/0.90 (appear first_movers skolemFOFtoCNF_E) = zero % 0.65/0.90 |- ~environment e \/ ~in_environment e (start_time skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 cardinality_at_time efficient_producers (start_time skolemFOFtoCNF_E) = % 0.65/0.90 zero % 0.65/0.90 |- cardinality_at_time efficient_producers skolemFOFtoCNF_T = zero % 0.65/0.90 |- appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 cardinality_at_time efficient_producers (start_time skolemFOFtoCNF_E) = % 0.65/0.90 zero \/ skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E % 0.65/0.90 |- appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 cardinality_at_time first_movers (start_time skolemFOFtoCNF_E) = zero % 0.65/0.90 |- ~(cardinality_at_time efficient_producers t = zero) \/ % 0.65/0.90 ~greater zero zero % 0.65/0.90 |- ~(cardinality_at_time first_movers t = zero) \/ ~greater zero zero \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.90 (appear efficient_producers e) \/ % 0.65/0.90 ~in_environment $_50 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_50 (appear efficient_producers e) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (start_time skolemFOFtoCNF_E) % 0.65/0.90 (appear efficient_producers e) \/ % 0.65/0.90 ~in_environment $_50 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_50 (appear efficient_producers e) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.90 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_50 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_50 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.90 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_50 skolemFOFtoCNF_T \/ % 0.65/0.90 in_environment $_50 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (start_time skolemFOFtoCNF_E) % 0.65/0.90 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_50 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_50 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.90 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_50 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.90 in_environment $_50 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (start_time skolemFOFtoCNF_E) % 0.65/0.90 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_50 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.90 in_environment $_50 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal zero % 0.65/0.90 (number_of_organizations e % 0.65/0.90 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.90 ~in_environment $_50 zero \/ % 0.65/0.90 in_environment $_50 % 0.65/0.90 (number_of_organizations e (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal zero % 0.65/0.90 (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) \/ % 0.65/0.90 ~in_environment $_50 zero \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_50 % 0.65/0.90 (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.90 (appear efficient_producers e) \/ % 0.65/0.90 ~in_environment $_50 (appear efficient_producers e) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_50 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (start_time skolemFOFtoCNF_E) % 0.65/0.90 (appear efficient_producers e) \/ % 0.65/0.90 ~in_environment $_50 (appear efficient_producers e) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_50 (start_time skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.90 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_50 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_50 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (start_time skolemFOFtoCNF_E) % 0.65/0.90 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_50 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_50 (start_time skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.90 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_50 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 in_environment $_50 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_50 \/ % 0.65/0.90 ~greater_or_equal (start_time skolemFOFtoCNF_E) % 0.65/0.90 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_50 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 in_environment $_50 (start_time skolemFOFtoCNF_E) % 0.65/0.90 |- ~greater_or_equal $_51 skolemFOFtoCNF_T \/ % 0.65/0.90 ~greater_or_equal skolemFOFtoCNF_T $_51 \/ % 0.65/0.90 in_environment skolemFOFtoCNF_E $_51 % 0.65/0.90 |- ~greater_or_equal $_51 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.90 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_51 \/ % 0.65/0.90 in_environment skolemFOFtoCNF_E $_51 % 0.65/0.90 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.90 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 in_environment skolemFOFtoCNF_E % 0.65/0.90 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.90 |- ~greater zero zero \/ % 0.65/0.90 selection_favors efficient_producers efficient_producers % 0.65/0.90 skolemFOFtoCNF_T % 0.65/0.90 |- ~(cardinality_at_time efficient_producers % 0.65/0.90 (start_time skolemFOFtoCNF_E) = zero) \/ ~greater zero zero \/ % 0.65/0.90 selection_favors efficient_producers efficient_producers % 0.65/0.90 (start_time skolemFOFtoCNF_E) % 0.65/0.90 |- ~(cardinality_at_time first_movers skolemFOFtoCNF_T = zero) \/ % 0.65/0.90 ~greater zero zero \/ % 0.65/0.90 selection_favors first_movers first_movers skolemFOFtoCNF_T % 0.65/0.90 |- ~(cardinality_at_time first_movers (start_time skolemFOFtoCNF_E) = % 0.65/0.90 zero) \/ ~greater zero zero \/ % 0.65/0.90 selection_favors first_movers first_movers (start_time skolemFOFtoCNF_E) % 0.65/0.90 |- ~greater zero zero \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 selection_favors efficient_producers efficient_producers % 0.65/0.90 (start_time skolemFOFtoCNF_E) % 0.65/0.90 |- ~greater zero zero \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 selection_favors first_movers first_movers (start_time skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 (appear efficient_producers e) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ % 0.65/0.90 ~in_environment $_85 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_85 (appear efficient_producers e) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 (appear efficient_producers e) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ % 0.65/0.90 ~in_environment $_85 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 in_environment $_85 (appear efficient_producers e) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 (appear efficient_producers e) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ % 0.65/0.90 ~in_environment $_85 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_85 (appear efficient_producers e) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ % 0.65/0.90 ~in_environment $_85 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_85 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ % 0.65/0.90 ~in_environment $_85 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_85 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ ~in_environment $_85 skolemFOFtoCNF_T \/ % 0.65/0.90 in_environment $_85 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ % 0.65/0.90 ~in_environment $_85 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_85 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ % 0.65/0.90 ~in_environment $_85 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.90 in_environment $_85 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ % 0.65/0.90 ~in_environment $_85 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.90 in_environment $_85 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 % 0.65/0.90 (number_of_organizations e % 0.65/0.90 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ ~in_environment $_85 zero \/ % 0.65/0.90 in_environment $_85 % 0.65/0.90 (number_of_organizations e (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal $_88 % 0.65/0.90 (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) \/ % 0.65/0.90 ~in_environment $_85 $_88 \/ ~in_environment $_85 zero \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_85 % 0.65/0.90 (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $_87 \/ % 0.65/0.90 ~in_environment $_85 $_87 \/ % 0.65/0.90 ~in_environment $_85 (appear efficient_producers e) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_85 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) $_87 \/ % 0.65/0.90 ~in_environment $_85 $_87 \/ % 0.65/0.90 ~in_environment $_85 (appear efficient_producers e) \/ % 0.65/0.90 in_environment $_85 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_87 \/ % 0.65/0.90 ~in_environment $_85 $_87 \/ % 0.65/0.90 ~in_environment $_85 (appear efficient_producers e) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_85 (start_time skolemFOFtoCNF_E) % 0.65/0.90 |- ~environment $_85 \/ % 0.65/0.90 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $_87 \/ % 0.65/0.90 ~in_environment $_85 $_87 \/ % 0.65/0.90 ~in_environment $_85 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.90 appear first_movers skolemFOFtoCNF_E = % 0.65/0.90 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.90 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.90 in_environment $_85 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.91 |- ~environment $_85 \/ % 0.65/0.91 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) $_87 \/ % 0.65/0.91 ~in_environment $_85 $_87 \/ % 0.65/0.91 ~in_environment $_85 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.91 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.91 in_environment $_85 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 |- ~environment $_85 \/ % 0.65/0.91 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_87 \/ % 0.65/0.91 ~in_environment $_85 $_87 \/ % 0.65/0.91 ~in_environment $_85 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.91 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.91 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.91 in_environment $_85 (start_time skolemFOFtoCNF_E) % 0.65/0.91 |- ~environment $_85 \/ % 0.65/0.91 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $_87 \/ % 0.65/0.91 ~in_environment $_85 $_87 \/ % 0.65/0.91 ~in_environment $_85 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.91 in_environment $_85 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.91 |- ~environment $_85 \/ % 0.65/0.91 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_87 \/ % 0.65/0.91 ~in_environment $_85 $_87 \/ % 0.65/0.91 ~in_environment $_85 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.91 in_environment $_85 (start_time skolemFOFtoCNF_E) % 0.65/0.91 |- ~greater_or_equal $_86 skolemFOFtoCNF_T \/ % 0.65/0.91 ~greater_or_equal $_88 $_86 \/ ~in_environment skolemFOFtoCNF_E $_88 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $_86 % 0.65/0.91 |- ~greater_or_equal $_86 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.91 ~greater_or_equal $_88 $_86 \/ ~in_environment skolemFOFtoCNF_E $_88 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $_86 % 0.65/0.91 |- ~greater_or_equal $_86 $_87 \/ % 0.65/0.91 ~greater_or_equal skolemFOFtoCNF_T $_86 \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E $_87 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $_86 % 0.65/0.91 |- ~greater_or_equal $_86 $_87 \/ % 0.65/0.91 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_86 \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E $_87 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $_86 % 0.65/0.91 |- ~environment $_85 \/ % 0.65/0.91 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 (appear efficient_producers e) \/ % 0.65/0.91 ~in_environment $_85 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.91 in_environment $_85 (appear efficient_producers e) % 0.65/0.91 |- ~environment $_85 \/ % 0.65/0.91 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 (appear efficient_producers e) \/ % 0.65/0.91 ~in_environment $_85 (appear efficient_producers e) \/ % 0.65/0.91 in_environment $_85 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 |- ~environment $_85 \/ % 0.65/0.91 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.91 ~in_environment $_85 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.91 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.91 in_environment $_85 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.91 |- ~environment $_85 \/ % 0.65/0.91 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.91 ~in_environment $_85 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.91 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.91 in_environment $_85 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 |- ~greater_or_equal $_92 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E $_92 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E % 0.65/0.91 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.91 |- ~greater_or_equal $_91 skolemFOFtoCNF_T \/ % 0.65/0.91 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_91 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $_91 % 0.65/0.91 |- ~greater_or_equal skolemFOFtoCNF_T (appear efficient_producers e) \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E (appear efficient_producers e) % 0.65/0.91 |- in_environment skolemFOFtoCNF_E (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.91 skolemFOFtoCNF_T) \/ ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.91 appear first_movers skolemFOFtoCNF_E = % 0.65/0.91 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.91 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.91 skolemFOFtoCNF_T) % 0.65/0.91 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.91 (number_of_organizations e % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E % 0.65/0.91 (number_of_organizations e (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.91 appear first_movers skolemFOFtoCNF_E = % 0.65/0.91 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.91 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.91 |- ~greater_or_equal $_95 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.91 ~greater_or_equal skolemFOFtoCNF_T $_95 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $_95 % 0.65/0.91 |- ~greater_or_equal $T $T1 \/ % 0.65/0.91 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) $T \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E $T1 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $T % 0.65/0.91 |- ~greater_or_equal $T (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.91 ~greater_or_equal $T2 $T \/ ~in_environment skolemFOFtoCNF_E $T2 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $T % 0.65/0.91 |- ~greater_or_equal $T (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.91 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) $T \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $T % 0.65/0.91 |- subpopulation first_movers skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 |- subpopulation efficient_producers skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 |- in_environment skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.91 |- ~greater_or_equal $_86 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.91 ~greater_or_equal skolemFOFtoCNF_T $_86 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $_86 % 0.65/0.91 |- ~greater_or_equal $_86 skolemFOFtoCNF_T \/ % 0.65/0.91 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) $_86 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $_86 % 0.65/0.91 |- cardinality_at_time efficient_producers % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E) = zero \/ % 0.65/0.91 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E % 0.65/0.91 |- greater % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) zero % 0.65/0.91 |- ~(cardinality_at_time efficient_producers % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.91 ~greater zero zero \/ % 0.65/0.91 selection_favors efficient_producers efficient_producers % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 |- ~greater_or_equal $T $T1 \/ % 0.65/0.91 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $T \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E $T1 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $T % 0.65/0.91 |- ~greater_or_equal $T (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.91 ~greater_or_equal $T2 $T \/ ~in_environment skolemFOFtoCNF_E $T2 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $T % 0.65/0.91 |- ~greater_or_equal $T (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.91 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $T \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $T % 0.65/0.91 |- subpopulation first_movers skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.91 |- subpopulation efficient_producers skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.91 |- greater % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) zero % 0.65/0.91 |- ~greater_or_equal $_86 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.91 ~greater_or_equal skolemFOFtoCNF_T $_86 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $_86 % 0.65/0.91 |- ~greater_or_equal $_86 skolemFOFtoCNF_T \/ % 0.65/0.91 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $_86 \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E $_86 % 0.65/0.91 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.91 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.91 cardinality_at_time efficient_producers % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E) = zero \/ % 0.65/0.91 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E % 0.65/0.91 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.91 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.91 cardinality_at_time first_movers % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E) = zero % 0.65/0.91 |- ~(cardinality_at_time efficient_producers % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.91 ~greater zero zero \/ % 0.65/0.91 selection_favors efficient_producers efficient_producers % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.91 |- ~(cardinality_at_time first_movers % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.91 ~greater zero zero \/ % 0.65/0.91 selection_favors first_movers first_movers % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 |- ~greater $X % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) \/ greater $X zero % 0.65/0.91 |- ~greater zero $Z \/ % 0.65/0.91 greater % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) $Z % 0.65/0.91 |- greater_or_equal % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) zero % 0.65/0.91 |- greater % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) zero % 0.65/0.91 |- subpopulation % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.91 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 |- ~environment $E \/ % 0.65/0.91 ~greater_or_equal $T2 % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment $E $T2 \/ ~in_environment $E zero \/ % 0.65/0.91 in_environment $E % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 |- ~environment $E \/ % 0.65/0.91 ~greater_or_equal zero % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment $E zero \/ % 0.65/0.91 in_environment $E % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 |- ~greater $X % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) \/ greater $X zero % 0.65/0.91 |- ~greater zero $Z \/ % 0.65/0.91 greater % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) $Z % 0.65/0.91 |- greater_or_equal % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) zero % 0.65/0.91 |- ~(cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) t = zero) % 0.65/0.91 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 |- ~environment $E \/ % 0.65/0.91 ~greater_or_equal $T2 % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment $E $T2 \/ ~in_environment $E zero \/ % 0.65/0.91 in_environment $E % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 |- ~environment $E \/ % 0.65/0.91 ~greater_or_equal zero % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment $E zero \/ % 0.65/0.91 in_environment $E % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.91 |- ~(cardinality_at_time first_movers % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.91 ~greater zero zero \/ % 0.65/0.91 selection_favors first_movers first_movers % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.91 |- ~greater $X % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) \/ greater $X zero % 0.65/0.91 |- ~greater zero $Z \/ % 0.65/0.91 greater % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) $Z % 0.65/0.91 |- greater_or_equal % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) zero % 0.65/0.91 |- greater % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) zero % 0.65/0.91 |- subpopulation % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.91 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 |- ~environment $E \/ % 0.65/0.91 ~greater_or_equal $T2 % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment $E $T2 \/ ~in_environment $E zero \/ % 0.65/0.91 in_environment $E % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 |- ~environment $E \/ % 0.65/0.91 ~greater_or_equal zero % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment $E zero \/ % 0.65/0.91 in_environment $E % 0.65/0.91 (number_of_organizations skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 |- ~greater $X % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) \/ greater $X zero % 0.65/0.91 |- ~greater zero $Z \/ % 0.65/0.91 greater % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) $Z % 0.65/0.91 |- greater_or_equal % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) zero % 0.65/0.91 |- ~(cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) t = zero) % 0.65/0.91 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.91 in_environment skolemFOFtoCNF_E % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 |- ~environment $E \/ % 0.65/0.91 ~greater_or_equal $T2 % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.91 ~in_environment $E $T2 \/ ~in_environment $E zero \/ % 0.65/0.91 in_environment $E % 0.65/0.91 (cardinality_at_time % 0.65/0.91 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.91 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.92 |- ~environment $E \/ % 0.65/0.92 ~greater_or_equal zero % 0.65/0.92 (cardinality_at_time % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.92 ~in_environment $E zero \/ % 0.65/0.92 in_environment $E % 0.65/0.92 (cardinality_at_time % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.92 |- ~(cardinality_at_time first_movers t = zero) \/ ~greater zero zero \/ % 0.65/0.92 appear first_movers skolemFOFtoCNF_E = % 0.65/0.92 appear an_organisation skolemFOFtoCNF_E % 0.65/0.92 |- ~greater zero zero \/ % 0.65/0.92 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.92 selection_favors efficient_producers efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~greater zero zero \/ % 0.65/0.92 appear first_movers skolemFOFtoCNF_E = % 0.65/0.92 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.92 selection_favors first_movers first_movers % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.92 |- ~greater_or_equal $_112 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.92 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $_112 \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E $_112 % 0.65/0.92 |- ~greater_or_equal $_112 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.92 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) $_112 \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E $_112 % 0.65/0.92 |- ~greater_or_equal (start_time skolemFOFtoCNF_E) % 0.65/0.92 (appear efficient_producers e) \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E (appear efficient_producers e) % 0.65/0.92 |- ~greater_or_equal (start_time skolemFOFtoCNF_E) % 0.65/0.92 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.92 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E % 0.65/0.92 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.92 |- ~greater_or_equal $_116 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_116 \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E $_116 % 0.65/0.92 |- ~greater_or_equal $_116 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_116 \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E $_116 % 0.65/0.92 |- ~environment $_122 \/ % 0.65/0.92 ~in_environment $_122 (appear efficient_producers e) \/ % 0.65/0.92 ~in_environment $_122 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.92 in_environment $_122 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~environment $_122 \/ % 0.65/0.92 ~in_environment $_122 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.92 ~in_environment $_122 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.92 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.92 in_environment $_122 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~environment $_122 \/ ~in_environment $_122 skolemFOFtoCNF_T \/ % 0.65/0.92 ~in_environment $_122 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.92 in_environment $_122 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~environment $_126 \/ % 0.65/0.92 ~in_environment $_126 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 ~in_environment $_126 (appear efficient_producers e) \/ % 0.65/0.92 in_environment $_126 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~greater_or_equal $_135 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 ~greater_or_equal (appear first_movers skolemFOFtoCNF_E) $_135 \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E $_135 % 0.65/0.92 |- ~greater_or_equal $_139 (appear efficient_producers e) \/ % 0.65/0.92 ~in_environment skolemFOFtoCNF_E $_139 \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E (appear efficient_producers e) % 0.65/0.92 |- ~greater_or_equal $_138 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $_138 \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E $_138 % 0.65/0.92 |- ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.92 (appear efficient_producers e) \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E (appear efficient_producers e) % 0.65/0.92 |- ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.92 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.92 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E % 0.65/0.92 (appear efficient_producers skolemFOFtoCNF_E) % 0.65/0.92 |- ~environment $_147 \/ % 0.65/0.92 ~in_environment $_147 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 ~in_environment $_147 (appear efficient_producers skolemFOFtoCNF_E) \/ % 0.65/0.92 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.92 in_environment $_147 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time $_166 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.92 zero) \/ ~environment $_164 \/ % 0.65/0.92 ~subpopulation $_166 $_164 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 ~subpopulation % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) $_164 % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 selection_favors % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) $_166 % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time $_166 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.92 zero) \/ ~environment $_164 \/ % 0.65/0.92 ~subpopulation $_166 $_164 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 ~subpopulation % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) $_164 % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 selection_favors % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) $_166 % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time $_166 skolemFOFtoCNF_T = zero) \/ % 0.65/0.92 ~environment $_164 \/ ~subpopulation $_166 $_164 skolemFOFtoCNF_T \/ % 0.65/0.92 ~subpopulation (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.92 $_164 skolemFOFtoCNF_T \/ % 0.65/0.92 appear first_movers skolemFOFtoCNF_E = % 0.65/0.92 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.92 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.92 selection_favors (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.92 $_166 skolemFOFtoCNF_T % 0.65/0.92 |- ~(cardinality_at_time % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.92 ~greater % 0.65/0.92 (cardinality_at_time $_165 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.92 zero \/ % 0.65/0.92 ~subpopulation $_165 skolemFOFtoCNF_E % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 selection_favors $_165 % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.92 ~greater % 0.65/0.92 (cardinality_at_time $_165 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 zero \/ % 0.65/0.92 ~subpopulation $_165 skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 selection_favors $_165 % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.92 skolemFOFtoCNF_T = zero) \/ % 0.65/0.92 ~greater (cardinality_at_time $_165 skolemFOFtoCNF_T) zero \/ % 0.65/0.92 ~subpopulation $_165 skolemFOFtoCNF_E skolemFOFtoCNF_T \/ % 0.65/0.92 appear first_movers skolemFOFtoCNF_E = % 0.65/0.92 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.92 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.92 selection_favors $_165 % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) skolemFOFtoCNF_T % 0.65/0.92 |- ~(cardinality_at_time $_166 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.92 zero) \/ ~environment $_164 \/ ~greater zero zero \/ % 0.65/0.92 ~subpopulation $_166 $_164 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 ~subpopulation efficient_producers $_164 % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 appear first_movers skolemFOFtoCNF_E = % 0.65/0.92 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.92 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.92 selection_favors efficient_producers $_166 % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time $_166 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.92 zero) \/ ~environment $_164 \/ ~greater zero zero \/ % 0.65/0.92 ~subpopulation $_166 $_164 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 ~subpopulation efficient_producers $_164 % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.92 selection_favors efficient_producers $_166 % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time $_166 skolemFOFtoCNF_T = zero) \/ % 0.65/0.92 ~environment $_164 \/ ~greater zero zero \/ % 0.65/0.92 ~subpopulation $_166 $_164 skolemFOFtoCNF_T \/ % 0.65/0.92 ~subpopulation efficient_producers $_164 skolemFOFtoCNF_T \/ % 0.65/0.92 selection_favors efficient_producers $_166 skolemFOFtoCNF_T % 0.65/0.92 |- ~(cardinality_at_time $_166 (start_time skolemFOFtoCNF_E) = zero) \/ % 0.65/0.92 ~environment $_164 \/ ~greater zero zero \/ % 0.65/0.92 ~subpopulation $_166 $_164 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.92 ~subpopulation efficient_producers $_164 % 0.65/0.92 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.92 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.92 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.92 selection_favors efficient_producers $_166 (start_time skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time $_166 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.92 zero) \/ ~environment $_164 \/ ~greater zero zero \/ % 0.65/0.92 ~subpopulation $_166 $_164 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 ~subpopulation first_movers $_164 % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.92 appear first_movers skolemFOFtoCNF_E = % 0.65/0.92 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.92 selection_favors first_movers $_166 % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time $_166 (start_time skolemFOFtoCNF_E) = zero) \/ % 0.65/0.92 ~environment $_164 \/ ~greater zero zero \/ % 0.65/0.92 ~subpopulation $_166 $_164 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.92 ~subpopulation first_movers $_164 (start_time skolemFOFtoCNF_E) \/ % 0.65/0.92 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.92 selection_favors first_movers $_166 (start_time skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.92 selection_favors % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.92 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.92 selection_favors % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time first_movers skolemFOFtoCNF_T = zero) \/ % 0.65/0.92 ~greater zero zero \/ % 0.65/0.92 selection_favors efficient_producers first_movers skolemFOFtoCNF_T % 0.65/0.92 |- ~(cardinality_at_time $_171 skolemFOFtoCNF_T = zero) \/ % 0.65/0.92 ~greater zero zero \/ % 0.65/0.92 ~subpopulation $_171 skolemFOFtoCNF_E skolemFOFtoCNF_T \/ % 0.65/0.92 selection_favors efficient_producers $_171 skolemFOFtoCNF_T % 0.65/0.92 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers % 0.65/0.92 |- ~(cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 selection_favors % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.92 ~greater % 0.65/0.92 (cardinality_at_time $_165 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 zero \/ % 0.65/0.92 ~subpopulation $_165 skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 selection_favors $_165 % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.92 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E % 0.65/0.92 (cardinality_at_time % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 |- ~greater $X % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 greater $X zero % 0.65/0.92 |- ~(cardinality_at_time efficient_producers t = zero) \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers % 0.65/0.92 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 greater_or_equal % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) zero % 0.65/0.92 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 greater % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) zero % 0.65/0.92 |- ~(cardinality_at_time first_movers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.92 selection_favors % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~(cardinality_at_time first_movers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.92 ~greater % 0.65/0.92 (cardinality_at_time $_165 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 zero \/ % 0.65/0.92 ~subpopulation $_165 skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.92 selection_favors $_165 % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.92 (cardinality_at_time first_movers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.92 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E % 0.65/0.92 (cardinality_at_time % 0.65/0.92 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 |- ~greater $X % 0.65/0.92 (cardinality_at_time first_movers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.92 greater $X zero % 0.65/0.92 |- ~(cardinality_at_time first_movers t = zero) \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = efficient_producers % 0.65/0.92 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.92 greater_or_equal % 0.65/0.92 (cardinality_at_time first_movers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) zero % 0.65/0.92 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.92 greater % 0.65/0.92 (cardinality_at_time first_movers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) zero % 0.65/0.92 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.92 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 in_environment skolemFOFtoCNF_E % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 |- ~environment $E \/ % 0.65/0.92 ~greater_or_equal $T2 % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.92 ~in_environment $E $T2 \/ ~in_environment $E zero \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 in_environment $E % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 |- ~environment $E \/ % 0.65/0.92 ~greater_or_equal zero % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.92 ~in_environment $E zero \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 in_environment $E % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.92 |- ~greater zero $Z \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.92 greater % 0.65/0.92 (cardinality_at_time first_movers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) $Z % 0.65/0.92 |- ~(cardinality_at_time $S2 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.92 zero) \/ ~environment $E \/ % 0.65/0.92 ~subpopulation $S2 $E (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 ~subpopulation first_movers $E (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.92 selection_favors first_movers $S2 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.92 |- ~greater zero $Z \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 greater % 0.65/0.92 (cardinality_at_time efficient_producers % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E)) $Z % 0.65/0.92 |- ~(cardinality_at_time $S2 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.92 zero) \/ ~environment $E \/ % 0.65/0.92 ~subpopulation $S2 $E (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 ~subpopulation efficient_producers $E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.92 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.92 selection_favors efficient_producers $S2 % 0.65/0.92 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.93 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater zero zero % 0.65/0.93 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 in_environment skolemFOFtoCNF_E % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 |- ~environment $E \/ % 0.65/0.93 ~greater_or_equal $T2 % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment $E $T2 \/ ~in_environment $E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 in_environment $E % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 |- ~environment $E \/ % 0.65/0.93 ~greater_or_equal zero % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment $E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 in_environment $E % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 |- ~(cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater zero zero \/ % 0.65/0.93 selection_favors % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.93 |- ~(cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.93 ~greater % 0.65/0.93 (cardinality_at_time $_165 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 zero \/ % 0.65/0.93 ~subpopulation $_165 skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater zero zero \/ % 0.65/0.93 selection_favors $_165 % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.93 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater zero zero \/ % 0.65/0.93 in_environment skolemFOFtoCNF_E % 0.65/0.93 (cardinality_at_time % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 |- ~greater $X % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater $X zero \/ greater zero zero % 0.65/0.93 |- ~(cardinality_at_time first_movers t = zero) \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater zero zero % 0.65/0.93 |- skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater zero zero \/ % 0.65/0.93 greater_or_equal % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) zero % 0.65/0.93 |- skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) zero \/ greater zero zero % 0.65/0.93 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater zero zero \/ % 0.65/0.93 in_environment skolemFOFtoCNF_E % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 |- ~environment $E \/ % 0.65/0.93 ~greater_or_equal $T2 % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment $E $T2 \/ ~in_environment $E zero \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater zero zero \/ % 0.65/0.93 in_environment $E % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 |- ~environment $E \/ % 0.65/0.93 ~greater_or_equal zero % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment $E zero \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater zero zero \/ % 0.65/0.93 in_environment $E % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 |- ~greater zero $Z \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) $Z \/ greater zero zero % 0.65/0.93 |- ~(cardinality_at_time $S2 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.93 zero) \/ ~environment $E \/ % 0.65/0.93 ~subpopulation $S2 $E (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.93 ~subpopulation first_movers $E (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 greater zero zero \/ % 0.65/0.93 selection_favors first_movers $S2 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.93 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 selection_favors % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.93 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 selection_favors efficient_producers % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.93 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 selection_favors efficient_producers efficient_producers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.93 |- ~greater_or_equal skolemFOFtoCNF_T zero \/ % 0.65/0.93 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 in_environment skolemFOFtoCNF_E % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 |- ~greater_or_equal skolemFOFtoCNF_T zero \/ % 0.65/0.93 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.93 in_environment skolemFOFtoCNF_E % 0.65/0.93 (cardinality_at_time % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.93 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers % 0.65/0.93 |- ~(cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 selection_favors % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.93 |- ~(cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.93 ~greater % 0.65/0.93 (cardinality_at_time $_165 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 zero \/ % 0.65/0.93 ~subpopulation $_165 skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 selection_favors $_165 % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.93 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 in_environment skolemFOFtoCNF_E % 0.65/0.93 (cardinality_at_time % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 |- ~greater $X % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 greater $X zero % 0.65/0.93 |- ~(cardinality_at_time efficient_producers t = zero) \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers % 0.65/0.93 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 greater_or_equal % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) zero % 0.65/0.93 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 greater % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) zero % 0.65/0.93 |- ~(cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 selection_favors % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.93 |- ~(cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.93 ~greater % 0.65/0.93 (cardinality_at_time $_165 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 zero \/ % 0.65/0.93 ~subpopulation $_165 skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 selection_favors $_165 % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.93 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 in_environment skolemFOFtoCNF_E % 0.65/0.93 (cardinality_at_time % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 |- ~greater $X % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 greater $X zero % 0.65/0.93 |- ~(cardinality_at_time first_movers t = zero) \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers % 0.65/0.93 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 greater_or_equal % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) zero % 0.65/0.93 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 greater % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) zero % 0.65/0.93 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 in_environment skolemFOFtoCNF_E % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 |- ~environment $E \/ % 0.65/0.93 ~greater_or_equal $T2 % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment $E $T2 \/ ~in_environment $E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 in_environment $E % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 |- ~environment $E \/ % 0.65/0.93 ~greater_or_equal zero % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment $E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 in_environment $E % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 |- ~greater zero $Z \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 greater % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) $Z % 0.65/0.93 |- ~(cardinality_at_time $S2 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.93 zero) \/ ~environment $E \/ % 0.65/0.93 ~subpopulation $S2 $E (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.93 ~subpopulation first_movers $E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 selection_favors first_movers $S2 % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.93 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.93 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 greater zero zero % 0.65/0.93 |- ~greater zero $Z \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 greater % 0.65/0.93 (cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) $Z % 0.65/0.93 |- ~(cardinality_at_time $S2 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.93 zero) \/ ~environment $E \/ % 0.65/0.93 ~subpopulation $S2 $E (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.93 ~subpopulation efficient_producers $E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.93 selection_favors efficient_producers $S2 % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.93 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 in_environment skolemFOFtoCNF_E % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 |- ~environment $E \/ % 0.65/0.93 ~greater_or_equal $T2 % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment $E $T2 \/ ~in_environment $E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 in_environment $E % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 |- ~environment $E \/ % 0.65/0.93 ~greater_or_equal zero % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.93 ~in_environment $E zero \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 in_environment $E % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 |- ~greater_or_equal skolemFOFtoCNF_T zero \/ % 0.65/0.93 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.93 appear first_movers skolemFOFtoCNF_E = % 0.65/0.93 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.93 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.93 in_environment skolemFOFtoCNF_E % 0.65/0.93 (cardinality_at_time first_movers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 |- ~(cardinality_at_time efficient_producers % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.93 appear first_movers skolemFOFtoCNF_E = % 0.65/0.93 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.93 selection_favors % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.93 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.94 ~greater % 0.65/0.94 (cardinality_at_time $_165 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 zero \/ % 0.65/0.94 ~subpopulation $_165 skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.94 selection_favors $_165 % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.94 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.94 in_environment skolemFOFtoCNF_E % 0.65/0.94 (cardinality_at_time % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 |- ~greater $X % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater $X zero \/ % 0.65/0.94 greater zero zero % 0.65/0.94 |- ~(cardinality_at_time efficient_producers t = zero) \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.94 greater_or_equal % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) zero % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 greater % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) zero \/ % 0.65/0.94 greater zero zero % 0.65/0.94 |- ~greater_or_equal skolemFOFtoCNF_T % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.94 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.94 in_environment skolemFOFtoCNF_E % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 |- ~environment $E \/ % 0.65/0.94 ~greater_or_equal $T2 % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.94 ~in_environment $E $T2 \/ ~in_environment $E zero \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.94 in_environment $E % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 |- ~environment $E \/ % 0.65/0.94 ~greater_or_equal zero % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.94 ~in_environment $E zero \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.94 in_environment $E % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 |- ~greater zero $Z \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 greater % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) $Z \/ greater zero zero % 0.65/0.94 |- ~(cardinality_at_time $S2 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.94 zero) \/ ~environment $E \/ % 0.65/0.94 ~subpopulation $S2 $E (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.94 ~subpopulation efficient_producers $E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.94 selection_favors efficient_producers $S2 % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 greater zero zero % 0.65/0.94 |- ~(cardinality_at_time first_movers skolemFOFtoCNF_T = zero) \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors efficient_producers first_movers skolemFOFtoCNF_T % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors efficient_producers efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors first_movers first_movers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time first_movers t = zero) \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors efficient_producers efficient_producers % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors first_movers first_movers (start_time skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors efficient_producers efficient_producers % 0.65/0.94 (start_time skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time first_movers skolemFOFtoCNF_T = zero) \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors first_movers first_movers skolemFOFtoCNF_T % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors efficient_producers efficient_producers % 0.65/0.94 skolemFOFtoCNF_T % 0.65/0.94 |- ~(cardinality_at_time efficient_producers t = zero) \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.94 selection_favors first_movers % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.94 selection_favors first_movers first_movers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~greater_or_equal skolemFOFtoCNF_T zero \/ % 0.65/0.94 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 in_environment skolemFOFtoCNF_E % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 |- ~greater_or_equal skolemFOFtoCNF_T zero \/ % 0.65/0.94 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 in_environment skolemFOFtoCNF_E % 0.65/0.94 (cardinality_at_time % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 |- ~greater_or_equal skolemFOFtoCNF_T zero \/ % 0.65/0.94 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.94 in_environment skolemFOFtoCNF_E % 0.65/0.94 (cardinality_at_time % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors efficient_producers % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~environment $_198 \/ % 0.65/0.94 ~greater_or_equal zero % 0.65/0.94 (cardinality_at_time first_movers % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.94 ~in_environment $_198 zero \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 greater zero zero \/ % 0.65/0.94 in_environment $_198 % 0.65/0.94 (cardinality_at_time % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.94 |- ~environment $_198 \/ % 0.65/0.94 ~greater_or_equal zero % 0.65/0.94 (cardinality_at_time first_movers % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.94 ~in_environment $_198 zero \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.94 in_environment $_198 % 0.65/0.94 (cardinality_at_time % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.94 |- ~environment $_198 \/ % 0.65/0.94 ~greater_or_equal zero % 0.65/0.94 (cardinality_at_time efficient_producers % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.94 ~in_environment $_198 zero \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.94 in_environment $_198 % 0.65/0.94 (cardinality_at_time % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.94 |- ~(cardinality_at_time $_200 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.94 zero) \/ % 0.65/0.94 ~subpopulation $_200 skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) $_200 % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time $_200 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.94 zero) \/ ~environment $_199 \/ % 0.65/0.94 ~subpopulation $_200 $_199 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.94 ~subpopulation efficient_producers $_199 % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.94 appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) $_200 % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time $_200 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.94 zero) \/ ~environment $_199 \/ % 0.65/0.94 ~subpopulation $_200 $_199 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.94 ~subpopulation first_movers $_199 % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) $_200 % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time $_200 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.94 zero) \/ ~environment $_199 \/ % 0.65/0.94 ~subpopulation $_200 $_199 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.94 ~subpopulation efficient_producers $_199 % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) $_200 % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time first_movers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) first_movers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) efficient_producers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E)) first_movers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.94 selection_favors efficient_producers first_movers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.94 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.94 selection_favors efficient_producers first_movers % 0.65/0.94 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time $_203 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.94 zero) \/ % 0.65/0.94 ~subpopulation $_203 skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) $_203 % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time $_203 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.94 zero) \/ ~environment $_202 \/ % 0.65/0.94 ~subpopulation $_203 $_202 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.94 ~subpopulation first_movers $_202 % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.94 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.94 greater zero zero \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) $_203 % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time $_203 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.94 zero) \/ ~environment $_202 \/ % 0.65/0.94 ~subpopulation $_203 $_202 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.94 ~subpopulation first_movers $_202 % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) $_203 % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.94 |- ~(cardinality_at_time $_203 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.94 zero) \/ ~environment $_202 \/ % 0.65/0.94 ~subpopulation $_203 $_202 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.94 ~subpopulation efficient_producers $_202 % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.94 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.94 selection_favors % 0.65/0.94 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E)) $_203 % 0.65/0.94 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time efficient_producers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 selection_favors % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) efficient_producers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 selection_favors % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) efficient_producers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 greater zero zero \/ % 0.65/0.95 selection_favors first_movers efficient_producers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors first_movers efficient_producers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~environment $_210 \/ % 0.65/0.95 ~greater_or_equal zero % 0.65/0.95 (cardinality_at_time efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.95 ~in_environment $_210 zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.95 in_environment $_210 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 |- ~environment $_210 \/ % 0.65/0.95 ~greater_or_equal zero % 0.65/0.95 (cardinality_at_time first_movers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.95 ~in_environment $_210 zero \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 in_environment $_210 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 |- ~environment $_210 \/ % 0.65/0.95 ~greater_or_equal zero % 0.65/0.95 (cardinality_at_time efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.95 ~in_environment $_210 zero \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 in_environment $_210 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 |- ~(cardinality_at_time $_214 (start_time skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 ~greater zero zero \/ % 0.65/0.95 ~subpopulation $_214 skolemFOFtoCNF_E (start_time skolemFOFtoCNF_E) \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors first_movers $_214 (start_time skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time efficient_producers % 0.65/0.95 (start_time skolemFOFtoCNF_E) = zero) \/ ~greater zero zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors first_movers efficient_producers % 0.65/0.95 (start_time skolemFOFtoCNF_E) % 0.65/0.95 |- ~greater zero zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors first_movers efficient_producers % 0.65/0.95 (start_time skolemFOFtoCNF_E) % 0.65/0.95 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors first_movers efficient_producers % 0.65/0.95 (start_time skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time $_224 skolemFOFtoCNF_T = zero) \/ % 0.65/0.95 ~subpopulation $_224 skolemFOFtoCNF_E skolemFOFtoCNF_T \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.95 $_224 skolemFOFtoCNF_T % 0.65/0.95 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.95 efficient_producers skolemFOFtoCNF_T % 0.65/0.95 |- ~(cardinality_at_time first_movers skolemFOFtoCNF_T = zero) \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.95 first_movers skolemFOFtoCNF_T % 0.65/0.95 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T = % 0.65/0.95 efficient_producers \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E % 0.65/0.95 |- ~(cardinality_at_time $_166 skolemFOFtoCNF_T = zero) \/ % 0.65/0.95 ~environment $_164 \/ ~subpopulation $_166 $_164 skolemFOFtoCNF_T \/ % 0.65/0.95 ~subpopulation efficient_producers $_164 skolemFOFtoCNF_T \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.95 $_166 skolemFOFtoCNF_T % 0.65/0.95 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) skolemFOFtoCNF_T % 0.65/0.95 |- ~environment $_50 \/ ~in_environment $_50 zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 in_environment $_50 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.95 skolemFOFtoCNF_T) % 0.65/0.95 |- ~greater_or_equal skolemFOFtoCNF_T zero \/ % 0.65/0.95 ~in_environment skolemFOFtoCNF_E zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 in_environment skolemFOFtoCNF_E % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) % 0.65/0.95 skolemFOFtoCNF_T) % 0.65/0.95 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E skolemFOFtoCNF_T) skolemFOFtoCNF_T % 0.65/0.95 |- ~(cardinality_at_time first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 ~greater zero zero \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 ~greater zero zero \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time $_228 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.95 zero) \/ ~greater zero zero \/ % 0.65/0.95 ~subpopulation $_228 skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers $_228 % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 ~greater zero zero \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~environment $_236 \/ ~in_environment $_236 zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 in_environment $_236 % 0.65/0.95 (cardinality_at_time first_movers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 |- ~(cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 ~greater zero zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors first_movers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time $_239 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.95 zero) \/ ~greater zero zero \/ % 0.65/0.95 ~subpopulation $_239 skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors first_movers $_239 % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 ~greater zero zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 selection_favors first_movers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors first_movers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 ~greater zero zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors first_movers efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors first_movers efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- ~environment $_241 \/ ~in_environment $_241 zero \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 in_environment $_241 % 0.65/0.95 (cardinality_at_time efficient_producers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 |- ~environment $_243 \/ ~in_environment $_243 zero \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 in_environment $_243 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 |- ~(cardinality_at_time efficient_producers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 selection_favors efficient_producers efficient_producers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 selection_favors first_movers first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~environment $_248 \/ ~in_environment $_248 zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 in_environment $_248 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 |- ~environment $_251 \/ ~in_environment $_251 zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 in_environment $_251 % 0.65/0.95 (cardinality_at_time efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 |- ~(cardinality_at_time $_253 (start_time skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 ~greater zero zero \/ % 0.65/0.95 ~subpopulation $_253 skolemFOFtoCNF_E (start_time skolemFOFtoCNF_E) \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers $_253 (start_time skolemFOFtoCNF_E) % 0.65/0.95 |- ~greater zero zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers first_movers % 0.65/0.95 (start_time skolemFOFtoCNF_E) % 0.65/0.95 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = start_time skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers first_movers % 0.65/0.95 (start_time skolemFOFtoCNF_E) % 0.65/0.95 |- ~environment $_263 \/ ~in_environment $_263 zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 in_environment $_263 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 |- ~(cardinality_at_time efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 selection_favors efficient_producers efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time first_movers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 selection_favors first_movers first_movers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 ~greater zero zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time $_268 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.95 zero) \/ ~greater zero zero \/ % 0.65/0.95 ~subpopulation $_268 skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers $_268 % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers first_movers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 selection_favors efficient_producers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time efficient_producers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 selection_favors efficient_producers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 selection_favors first_movers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~environment $_279 \/ % 0.65/0.95 ~greater_or_equal $_280 % 0.65/0.95 (cardinality_at_time first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.95 ~in_environment $_279 $_280 \/ ~in_environment $_279 zero \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 greater zero zero \/ % 0.65/0.95 in_environment $_279 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 |- ~environment $_279 \/ % 0.65/0.95 ~greater_or_equal $_280 % 0.65/0.95 (cardinality_at_time first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.95 ~in_environment $_279 $_280 \/ ~in_environment $_279 zero \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 in_environment $_279 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 |- ~environment $_279 \/ % 0.65/0.95 ~greater_or_equal $_280 % 0.65/0.95 (cardinality_at_time efficient_producers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.95 ~in_environment $_279 $_280 \/ ~in_environment $_279 zero \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 in_environment $_279 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.95 |- ~(cardinality_at_time efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 selection_favors efficient_producers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time first_movers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 selection_favors first_movers % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.95 |- ~(cardinality_at_time first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.95 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.95 greater zero zero \/ % 0.65/0.95 selection_favors first_movers first_movers % 0.65/0.95 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.95 |- ~environment $_288 \/ % 0.65/0.95 ~greater_or_equal $_289 % 0.65/0.95 (cardinality_at_time efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.95 ~in_environment $_288 $_289 \/ ~in_environment $_288 zero \/ % 0.65/0.95 appear first_movers skolemFOFtoCNF_E = % 0.65/0.95 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.95 in_environment $_288 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 |- ~environment $_288 \/ % 0.65/0.95 ~greater_or_equal $_289 % 0.65/0.95 (cardinality_at_time first_movers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.95 ~in_environment $_288 $_289 \/ ~in_environment $_288 zero \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.95 in_environment $_288 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 |- ~environment $_288 \/ % 0.65/0.95 ~greater_or_equal $_289 % 0.65/0.95 (cardinality_at_time efficient_producers % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.95 ~in_environment $_288 $_289 \/ ~in_environment $_288 zero \/ % 0.65/0.95 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.95 in_environment $_288 % 0.65/0.95 (cardinality_at_time % 0.65/0.95 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.95 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 |- ~(cardinality_at_time efficient_producers % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 appear first_movers skolemFOFtoCNF_E = % 0.65/0.96 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.96 selection_favors efficient_producers efficient_producers % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time first_movers % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.96 greater zero zero \/ % 0.65/0.96 selection_favors first_movers % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.96 |- ~environment $_297 \/ % 0.65/0.96 ~in_environment $_297 % 0.65/0.96 (cardinality_at_time first_movers % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.96 ~in_environment $_297 zero \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.96 in_environment $_297 % 0.65/0.96 (cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 |- ~environment $_300 \/ % 0.65/0.96 ~in_environment $_300 % 0.65/0.96 (cardinality_at_time efficient_producers % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.96 ~in_environment $_300 zero \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.96 in_environment $_300 % 0.65/0.96 (cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 |- ~(cardinality_at_time efficient_producers % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 appear first_movers skolemFOFtoCNF_E = % 0.65/0.96 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.96 selection_favors efficient_producers % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.96 |- ~environment $_308 \/ % 0.65/0.96 ~in_environment $_308 % 0.65/0.96 (cardinality_at_time efficient_producers % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.96 ~in_environment $_308 zero \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.96 in_environment $_308 % 0.65/0.96 (cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 |- ~environment $_311 \/ % 0.65/0.96 ~in_environment $_311 % 0.65/0.96 (cardinality_at_time first_movers % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.96 ~in_environment $_311 zero \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.96 in_environment $_311 % 0.65/0.96 (cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 |- ~(cardinality_at_time first_movers % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.96 selection_favors efficient_producers first_movers % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.96 selection_favors efficient_producers % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time $_315 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.96 zero) \/ % 0.65/0.96 ~subpopulation $_315 skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.96 selection_favors efficient_producers $_315 % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.96 selection_favors first_movers % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time $_318 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.96 zero) \/ % 0.65/0.96 ~subpopulation $_318 skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.96 selection_favors first_movers $_318 % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time efficient_producers % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.96 selection_favors first_movers efficient_producers % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.96 |- ~environment $_320 \/ % 0.65/0.96 ~in_environment $_320 % 0.65/0.96 (cardinality_at_time first_movers % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) \/ % 0.65/0.96 ~in_environment $_320 zero \/ % 0.65/0.96 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.96 greater zero zero \/ % 0.65/0.96 in_environment $_320 % 0.65/0.96 (cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 |- ~(cardinality_at_time first_movers % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.96 selection_favors efficient_producers first_movers % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.96 selection_favors efficient_producers % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time $_324 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.96 zero) \/ % 0.65/0.96 ~subpopulation $_324 skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = first_movers \/ % 0.65/0.96 selection_favors efficient_producers $_324 % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.96 selection_favors first_movers % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time $_327 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.96 zero) \/ % 0.65/0.96 ~subpopulation $_327 skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.96 selection_favors first_movers $_327 % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time efficient_producers % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = efficient_producers \/ % 0.65/0.96 selection_favors first_movers efficient_producers % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.96 |- ~environment $_331 \/ % 0.65/0.96 ~in_environment $_331 % 0.65/0.96 (cardinality_at_time efficient_producers % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) \/ % 0.65/0.96 ~in_environment $_331 zero \/ % 0.65/0.96 appear first_movers skolemFOFtoCNF_E = % 0.65/0.96 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.96 in_environment $_331 % 0.65/0.96 (cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 |- ~(cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.96 greater zero zero \/ % 0.65/0.96 selection_favors first_movers % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E)) % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time $_335 (appear first_movers skolemFOFtoCNF_E) = % 0.65/0.96 zero) \/ % 0.65/0.96 ~subpopulation $_335 skolemFOFtoCNF_E % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) \/ % 0.65/0.96 skolemFOFtoCNF_T = appear first_movers skolemFOFtoCNF_E \/ % 0.65/0.96 greater zero zero \/ % 0.65/0.96 selection_favors first_movers $_335 % 0.65/0.96 (appear first_movers skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.65/0.96 appear first_movers skolemFOFtoCNF_E = % 0.65/0.96 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.96 selection_favors efficient_producers % 0.65/0.96 (skolemFOFtoCNF_S skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E)) % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.96 |- ~(cardinality_at_time $_340 (appear an_organisation skolemFOFtoCNF_E) = % 0.65/0.96 zero) \/ % 0.65/0.96 ~subpopulation $_340 skolemFOFtoCNF_E % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.65/0.96 appear first_movers skolemFOFtoCNF_E = % 0.65/0.96 appear an_organisation skolemFOFtoCNF_E \/ greater zero zero \/ % 0.65/0.96 selection_favors efficient_producers $_340 % 0.65/0.96 (appear an_organisation skolemFOFtoCNF_E) % 0.65/0.96 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.65/0.96 %------------------------------------------------------------------------------