%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT033+2 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n015.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:02:56 AM UTC 2026
% Result : CounterSatisfiable 15.61s 5.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT033+2 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.05 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.11/0.37 % Computer : n015.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.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 7 12:28:30 UTC 2026
% 0.11/0.38 % CPUTime :
% 15.61/5.21
% 15.61/5.21 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.61/5.21
% 15.61/5.21 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.61/5.22 %$ subpopulation > selection_favors > in_environment > greater_or_equal > greater > environment > number_of_organizations > cardinality_at_time > appear > #nlpp > start_time > zero > t > first_movers > efficient_producers > e > an_organisation > #skF_2 > #skF_3 > #skF_1
% 15.61/5.22
% 15.61/5.22 %Foreground sorts:
% 15.61/5.22
% 15.61/5.22
% 15.61/5.22 %Background operators:
% 15.61/5.22
% 15.61/5.22
% 15.61/5.22 %Foreground operators:
% 15.61/5.22 tff(greater, type, greater: ($i * $i) > $o).
% 15.61/5.22 tff(number_of_organizations, type, number_of_organizations: ($i * $i) > $i).
% 15.61/5.22 tff(in_environment, type, in_environment: ($i * $i) > $o).
% 15.61/5.22 tff(t, type, t: $i).
% 15.61/5.22 tff(appear, type, appear: ($i * $i) > $i).
% 15.61/5.22 tff(efficient_producers, type, efficient_producers: $i).
% 15.61/5.22 tff(cardinality_at_time, type, cardinality_at_time: ($i * $i) > $i).
% 15.61/5.22 tff('#skF_2', type, '#skF_2': $i).
% 15.61/5.22 tff('#skF_3', type, '#skF_3': $i).
% 15.61/5.22 tff(environment, type, environment: $i > $o).
% 15.61/5.22 tff(start_time, type, start_time: $i > $i).
% 15.61/5.22 tff(first_movers, type, first_movers: $i).
% 15.61/5.22 tff(an_organisation, type, an_organisation: $i).
% 15.61/5.22 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o).
% 15.61/5.22 tff(e, type, e: $i).
% 15.61/5.22 tff('#skF_1', type, '#skF_1': ($i * $i) > $i).
% 15.61/5.22 tff(subpopulation, type, subpopulation: ($i * $i * $i) > $o).
% 15.61/5.22 tff(selection_favors, type, selection_favors: ($i * $i * $i) > $o).
% 15.61/5.22 tff(zero, type, zero: $i).
% 15.61/5.22
% 15.61/5.22 %Saturated clause set:
% 15.61/5.23 tff(c_5739, plain, (![Y_491, E_361, E_493]: (in_environment('#skF_2', Y_491) | ~greater(Y_491, appear(an_organisation, E_361)) | ~greater(start_time(E_493), Y_491) | ~environment(E_493) | ~greater('#skF_3', appear(first_movers, E_493)) | ~greater(start_time(E_493), '#skF_3') | ~greater(appear(an_organisation, E_493), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_493)) | ~in_environment('#skF_2', start_time(E_361)) | ~environment(E_361) | ~greater('#skF_3', appear(first_movers, E_361)) | ~greater(appear(an_organisation, E_361), '#skF_3')))).
% 15.61/5.23 tff(c_5740, plain, (![Y_491, E_348, E_493]: (in_environment('#skF_2', Y_491) | ~greater(Y_491, start_time(E_348)) | ~greater(start_time(E_493), Y_491) | ~environment(E_493) | ~greater('#skF_3', appear(first_movers, E_493)) | ~greater(start_time(E_493), '#skF_3') | ~greater(appear(an_organisation, E_493), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_493)) | ~environment(E_348) | ~greater('#skF_3', appear(first_movers, E_348)) | ~greater(start_time(E_348), '#skF_3') | ~greater(appear(an_organisation, E_348), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_348))))).
% 15.61/5.23 tff(c_5334, plain, (![Y_449, E_348, E_451]: (in_environment('#skF_2', Y_449) | ~greater(Y_449, start_time(E_348)) | ~greater(appear(an_organisation, E_451), Y_449) | ~in_environment('#skF_2', start_time(E_451)) | ~environment(E_451) | ~greater('#skF_3', appear(first_movers, E_451)) | ~greater(appear(an_organisation, E_451), '#skF_3') | ~environment(E_348) | ~greater('#skF_3', appear(first_movers, E_348)) | ~greater(start_time(E_348), '#skF_3') | ~greater(appear(an_organisation, E_348), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_348))))).
% 15.61/5.23 tff(c_5816, plain, (![E_45, E_500]: (in_environment('#skF_2', appear(first_movers, E_45)) | ~greater(start_time(E_500), appear(first_movers, E_45)) | ~environment(E_500) | ~greater('#skF_3', appear(first_movers, E_500)) | ~greater(start_time(E_500), '#skF_3') | ~greater(appear(an_organisation, E_500), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_500)) | ~greater(appear(an_organisation, E_45), start_time('#skF_2')) | appear(first_movers, E_45)=appear(an_organisation, E_45) | ~environment(E_45)))).
% 15.61/5.23 tff(c_5741, plain, (![Y_491, E_261, E_493]: (in_environment('#skF_2', Y_491) | ~greater(Y_491, appear(first_movers, E_261)) | ~greater(start_time(E_493), Y_491) | ~environment(E_493) | ~greater('#skF_3', appear(first_movers, E_493)) | ~greater(start_time(E_493), '#skF_3') | ~greater(appear(an_organisation, E_493), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_493)) | ~in_environment('#skF_2', appear(an_organisation, E_261)) | ~environment(E_261) | ~greater('#skF_3', appear(first_movers, E_261))))).
% 15.61/5.23 tff(c_5333, plain, (![Y_449, E_361, E_451]: (in_environment('#skF_2', Y_449) | ~greater(Y_449, appear(an_organisation, E_361)) | ~greater(appear(an_organisation, E_451), Y_449) | ~in_environment('#skF_2', start_time(E_451)) | ~environment(E_451) | ~greater('#skF_3', appear(first_movers, E_451)) | ~greater(appear(an_organisation, E_451), '#skF_3') | ~in_environment('#skF_2', start_time(E_361)) | ~environment(E_361) | ~greater('#skF_3', appear(first_movers, E_361)) | ~greater(appear(an_organisation, E_361), '#skF_3')))).
% 15.61/5.23 tff(c_4583, plain, (![Y_393, E_348, E_395]: (in_environment('#skF_2', Y_393) | ~greater(Y_393, start_time(E_348)) | ~greater(appear(first_movers, E_395), Y_393) | ~in_environment('#skF_2', appear(an_organisation, E_395)) | ~environment(E_395) | ~greater('#skF_3', appear(first_movers, E_395)) | ~environment(E_348) | ~greater('#skF_3', appear(first_movers, E_348)) | ~greater(start_time(E_348), '#skF_3') | ~greater(appear(an_organisation, E_348), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_348))))).
% 15.61/5.23 tff(c_5819, plain, (![E_43, E_500]: (in_environment('#skF_2', appear(first_movers, E_43)) | ~greater(start_time(E_500), appear(first_movers, E_43)) | ~environment(E_500) | ~greater('#skF_3', appear(first_movers, E_500)) | ~greater(start_time(E_500), '#skF_3') | ~greater(appear(an_organisation, E_500), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_500)) | ~greater(start_time(E_43), start_time('#skF_2')) | appear(first_movers, E_43)=start_time(E_43) | ~environment(E_43)))).
% 15.61/5.23 tff(c_6515, plain, (![X_51, E_571]: (in_environment('#skF_2', X_51) | ~greater(start_time(E_571), X_51) | ~environment(E_571) | ~greater('#skF_3', appear(first_movers, E_571)) | ~greater(start_time(E_571), '#skF_3') | ~greater(appear(an_organisation, E_571), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_571)) | ~greater(X_51, appear(efficient_producers, e))))).
% 15.61/5.24 tff(c_5742, plain, (![Y_491, E_248, E_493]: (in_environment('#skF_2', Y_491) | ~greater(Y_491, appear(first_movers, E_248)) | ~greater(start_time(E_493), Y_491) | ~environment(E_493) | ~greater('#skF_3', appear(first_movers, E_493)) | ~greater(start_time(E_493), '#skF_3') | ~greater(appear(an_organisation, E_493), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_493)) | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater('#skF_3', appear(first_movers, E_248))))).
% 15.61/5.24 tff(c_4352, plain, (![Y_377, E_348, E_379]: (in_environment('#skF_2', Y_377) | ~greater(Y_377, start_time(E_348)) | ~greater(appear(first_movers, E_379), Y_377) | ~in_environment('#skF_2', start_time(E_379)) | ~environment(E_379) | ~greater('#skF_3', appear(first_movers, E_379)) | ~environment(E_348) | ~greater('#skF_3', appear(first_movers, E_348)) | ~greater(start_time(E_348), '#skF_3') | ~greater(appear(an_organisation, E_348), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_348))))).
% 15.61/5.24 tff(c_5405, plain, (![E_45, E_458]: (in_environment('#skF_2', appear(first_movers, E_45)) | ~greater(appear(an_organisation, E_458), appear(first_movers, E_45)) | ~in_environment('#skF_2', start_time(E_458)) | ~environment(E_458) | ~greater('#skF_3', appear(first_movers, E_458)) | ~greater(appear(an_organisation, E_458), '#skF_3') | ~greater(appear(an_organisation, E_45), start_time('#skF_2')) | appear(first_movers, E_45)=appear(an_organisation, E_45) | ~environment(E_45)))).
% 15.61/5.24 tff(c_5335, plain, (![Y_449, E_261, E_451]: (in_environment('#skF_2', Y_449) | ~greater(Y_449, appear(first_movers, E_261)) | ~greater(appear(an_organisation, E_451), Y_449) | ~in_environment('#skF_2', start_time(E_451)) | ~environment(E_451) | ~greater('#skF_3', appear(first_movers, E_451)) | ~greater(appear(an_organisation, E_451), '#skF_3') | ~in_environment('#skF_2', appear(an_organisation, E_261)) | ~environment(E_261) | ~greater('#skF_3', appear(first_movers, E_261))))).
% 15.61/5.24 tff(c_4582, plain, (![Y_393, E_361, E_395]: (in_environment('#skF_2', Y_393) | ~greater(Y_393, appear(an_organisation, E_361)) | ~greater(appear(first_movers, E_395), Y_393) | ~in_environment('#skF_2', appear(an_organisation, E_395)) | ~environment(E_395) | ~greater('#skF_3', appear(first_movers, E_395)) | ~in_environment('#skF_2', start_time(E_361)) | ~environment(E_361) | ~greater('#skF_3', appear(first_movers, E_361)) | ~greater(appear(an_organisation, E_361), '#skF_3')))).
% 15.61/5.24 tff(c_5408, plain, (![E_43, E_458]: (in_environment('#skF_2', appear(first_movers, E_43)) | ~greater(appear(an_organisation, E_458), appear(first_movers, E_43)) | ~in_environment('#skF_2', start_time(E_458)) | ~environment(E_458) | ~greater('#skF_3', appear(first_movers, E_458)) | ~greater(appear(an_organisation, E_458), '#skF_3') | ~greater(start_time(E_43), start_time('#skF_2')) | appear(first_movers, E_43)=start_time(E_43) | ~environment(E_43)))).
% 15.61/5.24 tff(c_6372, plain, (![X_51, E_550]: (in_environment('#skF_2', X_51) | ~greater(appear(an_organisation, E_550), X_51) | ~in_environment('#skF_2', start_time(E_550)) | ~environment(E_550) | ~greater('#skF_3', appear(first_movers, E_550)) | ~greater(appear(an_organisation, E_550), '#skF_3') | ~greater(X_51, appear(efficient_producers, e))))).
% 15.61/5.24 tff(c_3836, plain, (![E_132, E_350]: (in_environment('#skF_2', appear(first_movers, E_132)) | ~in_environment('#skF_2', appear(an_organisation, E_132)) | ~environment(E_132) | ~greater(start_time(E_350), appear(first_movers, E_132)) | ~environment(E_350) | ~greater('#skF_3', appear(first_movers, E_350)) | ~greater(start_time(E_350), '#skF_3') | ~greater(appear(an_organisation, E_350), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_350))))).
% 15.61/5.24 tff(c_5336, plain, (![Y_449, E_248, E_451]: (in_environment('#skF_2', Y_449) | ~greater(Y_449, appear(first_movers, E_248)) | ~greater(appear(an_organisation, E_451), Y_449) | ~in_environment('#skF_2', start_time(E_451)) | ~environment(E_451) | ~greater('#skF_3', appear(first_movers, E_451)) | ~greater(appear(an_organisation, E_451), '#skF_3') | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater('#skF_3', appear(first_movers, E_248))))).
% 15.61/5.24 tff(c_4767, plain, (![E_45, E_405]: (in_environment('#skF_2', appear(first_movers, E_45)) | ~greater(appear(first_movers, E_405), appear(first_movers, E_45)) | ~in_environment('#skF_2', appear(an_organisation, E_405)) | ~environment(E_405) | ~greater('#skF_3', appear(first_movers, E_405)) | ~greater(appear(an_organisation, E_45), start_time('#skF_2')) | appear(first_movers, E_45)=appear(an_organisation, E_45) | ~environment(E_45)))).
% 15.61/5.24 tff(c_3839, plain, (![E_125, E_350]: (in_environment('#skF_2', appear(first_movers, E_125)) | ~in_environment('#skF_2', start_time(E_125)) | ~environment(E_125) | ~greater(start_time(E_350), appear(first_movers, E_125)) | ~environment(E_350) | ~greater('#skF_3', appear(first_movers, E_350)) | ~greater(start_time(E_350), '#skF_3') | ~greater(appear(an_organisation, E_350), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_350))))).
% 15.61/5.24 tff(c_4351, plain, (![Y_377, E_361, E_379]: (in_environment('#skF_2', Y_377) | ~greater(Y_377, appear(an_organisation, E_361)) | ~greater(appear(first_movers, E_379), Y_377) | ~in_environment('#skF_2', start_time(E_379)) | ~environment(E_379) | ~greater('#skF_3', appear(first_movers, E_379)) | ~in_environment('#skF_2', start_time(E_361)) | ~environment(E_361) | ~greater('#skF_3', appear(first_movers, E_361)) | ~greater(appear(an_organisation, E_361), '#skF_3')))).
% 15.61/5.24 tff(c_4536, plain, (![E_45, E_389]: (in_environment('#skF_2', appear(first_movers, E_45)) | ~greater(appear(first_movers, E_389), appear(first_movers, E_45)) | ~in_environment('#skF_2', start_time(E_389)) | ~environment(E_389) | ~greater('#skF_3', appear(first_movers, E_389)) | ~greater(appear(an_organisation, E_45), start_time('#skF_2')) | appear(first_movers, E_45)=appear(an_organisation, E_45) | ~environment(E_45)))).
% 15.61/5.24 tff(c_3841, plain, (![Y_30, E_350, Y_171]: (in_environment('#skF_2', Y_30) | ~greater(Y_30, start_time(E_350)) | ~greater(Y_171, Y_30) | ~greater(Y_171, '#skF_3') | ~greater('#skF_3', Y_171) | ~environment(E_350) | ~greater('#skF_3', appear(first_movers, E_350)) | ~greater(start_time(E_350), '#skF_3') | ~greater(appear(an_organisation, E_350), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_350))))).
% 15.61/5.24 tff(c_4584, plain, (![Y_393, E_261, E_395]: (in_environment('#skF_2', Y_393) | ~greater(Y_393, appear(first_movers, E_261)) | ~greater(appear(first_movers, E_395), Y_393) | ~in_environment('#skF_2', appear(an_organisation, E_395)) | ~environment(E_395) | ~greater('#skF_3', appear(first_movers, E_395)) | ~in_environment('#skF_2', appear(an_organisation, E_261)) | ~environment(E_261) | ~greater('#skF_3', appear(first_movers, E_261))))).
% 15.61/5.24 tff(c_4770, plain, (![E_43, E_405]: (in_environment('#skF_2', appear(first_movers, E_43)) | ~greater(appear(first_movers, E_405), appear(first_movers, E_43)) | ~in_environment('#skF_2', appear(an_organisation, E_405)) | ~environment(E_405) | ~greater('#skF_3', appear(first_movers, E_405)) | ~greater(start_time(E_43), start_time('#skF_2')) | appear(first_movers, E_43)=start_time(E_43) | ~environment(E_43)))).
% 15.61/5.25 tff(c_6168, plain, (![X_51, E_525]: (in_environment('#skF_2', X_51) | ~greater(appear(first_movers, E_525), X_51) | ~in_environment('#skF_2', appear(an_organisation, E_525)) | ~environment(E_525) | ~greater('#skF_3', appear(first_movers, E_525)) | ~greater(X_51, appear(efficient_producers, e))))).
% 15.61/5.25 tff(c_5563, plain, (![E_5, E_470]: (selection_favors(first_movers, '#skF_1'(E_5, start_time(E_470)), start_time(E_470)) | cardinality_at_time('#skF_1'(E_5, start_time(E_470)), start_time(E_470))!=zero | ~subpopulation(first_movers, E_5, start_time(E_470)) | appear(first_movers, E_470)=start_time(E_470) | ~environment(E_470) | ~greater(number_of_organizations(E_5, start_time(E_470)), zero) | ~environment(E_5)))).
% 15.61/5.25 tff(c_4585, plain, (![Y_393, E_248, E_395]: (in_environment('#skF_2', Y_393) | ~greater(Y_393, appear(first_movers, E_248)) | ~greater(appear(first_movers, E_395), Y_393) | ~in_environment('#skF_2', appear(an_organisation, E_395)) | ~environment(E_395) | ~greater('#skF_3', appear(first_movers, E_395)) | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater('#skF_3', appear(first_movers, E_248))))).
% 15.61/5.25 tff(c_5743, plain, (![Y_491, Y_169, E_493]: (in_environment('#skF_2', Y_491) | ~greater(Y_491, Y_169) | ~greater(start_time(E_493), Y_491) | ~environment(E_493) | ~greater('#skF_3', appear(first_movers, E_493)) | ~greater(start_time(E_493), '#skF_3') | ~greater(appear(an_organisation, E_493), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_493)) | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.25 tff(c_4539, plain, (![E_43, E_389]: (in_environment('#skF_2', appear(first_movers, E_43)) | ~greater(appear(first_movers, E_389), appear(first_movers, E_43)) | ~in_environment('#skF_2', start_time(E_389)) | ~environment(E_389) | ~greater('#skF_3', appear(first_movers, E_389)) | ~greater(start_time(E_43), start_time('#skF_2')) | appear(first_movers, E_43)=start_time(E_43) | ~environment(E_43)))).
% 15.61/5.25 tff(c_5081, plain, (![E_5]: (selection_favors(first_movers, '#skF_1'(E_5, appear(an_organisation, '#skF_2')), appear(an_organisation, '#skF_2')) | cardinality_at_time('#skF_1'(E_5, appear(an_organisation, '#skF_2')), appear(an_organisation, '#skF_2'))!=zero | ~subpopulation(first_movers, E_5, appear(an_organisation, '#skF_2')) | ~greater(number_of_organizations(E_5, appear(an_organisation, '#skF_2')), zero) | ~environment(E_5)))).
% 15.61/5.25 tff(c_4353, plain, (![Y_377, E_261, E_379]: (in_environment('#skF_2', Y_377) | ~greater(Y_377, appear(first_movers, E_261)) | ~greater(appear(first_movers, E_379), Y_377) | ~in_environment('#skF_2', start_time(E_379)) | ~environment(E_379) | ~greater('#skF_3', appear(first_movers, E_379)) | ~in_environment('#skF_2', appear(an_organisation, E_261)) | ~environment(E_261) | ~greater('#skF_3', appear(first_movers, E_261))))).
% 15.61/5.25 tff(c_3380, plain, (![E_318]: (selection_favors(efficient_producers, '#skF_1'(E_318, appear(an_organisation, '#skF_2')), appear(an_organisation, '#skF_2')) | cardinality_at_time('#skF_1'(E_318, appear(an_organisation, '#skF_2')), appear(an_organisation, '#skF_2'))!=zero | ~subpopulation(efficient_producers, E_318, appear(an_organisation, '#skF_2')) | ~greater(number_of_organizations(E_318, appear(an_organisation, '#skF_2')), zero) | ~environment(E_318)))).
% 15.61/5.25 tff(c_4172, plain, (![E_132, E_363]: (in_environment('#skF_2', appear(first_movers, E_132)) | ~in_environment('#skF_2', appear(an_organisation, E_132)) | ~environment(E_132) | ~greater(appear(an_organisation, E_363), appear(first_movers, E_132)) | ~in_environment('#skF_2', start_time(E_363)) | ~environment(E_363) | ~greater('#skF_3', appear(first_movers, E_363)) | ~greater(appear(an_organisation, E_363), '#skF_3')))).
% 15.61/5.25 tff(c_5957, plain, (![X_51, E_504]: (in_environment('#skF_2', X_51) | ~greater(appear(first_movers, E_504), X_51) | ~in_environment('#skF_2', start_time(E_504)) | ~environment(E_504) | ~greater('#skF_3', appear(first_movers, E_504)) | ~greater(X_51, appear(efficient_producers, e))))).
% 15.61/5.25 tff(c_4354, plain, (![Y_377, E_248, E_379]: (in_environment('#skF_2', Y_377) | ~greater(Y_377, appear(first_movers, E_248)) | ~greater(appear(first_movers, E_379), Y_377) | ~in_environment('#skF_2', start_time(E_379)) | ~environment(E_379) | ~greater('#skF_3', appear(first_movers, E_379)) | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater('#skF_3', appear(first_movers, E_248))))).
% 15.61/5.25 tff(c_5826, plain, (![E_500]: (~greater(start_time(E_500), appear(efficient_producers, '#skF_2')) | ~environment(E_500) | ~greater('#skF_3', appear(first_movers, E_500)) | ~greater(start_time(E_500), '#skF_3') | ~greater(appear(an_organisation, E_500), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_500))))).
% 15.61/5.25 tff(c_5744, plain, (![Y_491, E_493]: (in_environment('#skF_2', Y_491) | ~greater(Y_491, appear(an_organisation, '#skF_2')) | ~greater(start_time(E_493), Y_491) | ~environment(E_493) | ~greater('#skF_3', appear(first_movers, E_493)) | ~greater(start_time(E_493), '#skF_3') | ~greater(appear(an_organisation, E_493), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_493))))).
% 15.61/5.25 tff(c_5790, plain, (![E_497]: (~greater(start_time(E_497), appear(efficient_producers, e)) | ~environment(E_497) | ~greater('#skF_3', appear(first_movers, E_497)) | ~greater(start_time(E_497), '#skF_3') | ~greater(appear(an_organisation, E_497), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_497))))).
% 15.61/5.25 tff(c_5748, plain, (![Y_491, E_493]: (in_environment('#skF_2', Y_491) | ~greater(Y_491, start_time('#skF_2')) | ~greater(start_time(E_493), Y_491) | ~environment(E_493) | ~greater('#skF_3', appear(first_movers, E_493)) | ~greater(start_time(E_493), '#skF_3') | ~greater(appear(an_organisation, E_493), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_493))))).
% 15.61/5.25 tff(c_5749, plain, (![Y_491, E_493]: (in_environment('#skF_2', Y_491) | ~greater(Y_491, '#skF_3') | ~greater(start_time(E_493), Y_491) | ~environment(E_493) | ~greater('#skF_3', appear(first_movers, E_493)) | ~greater(start_time(E_493), '#skF_3') | ~greater(appear(an_organisation, E_493), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_493))))).
% 15.61/5.25 tff(c_3853, plain, (![Y_30, Y_113, E_350]: (in_environment('#skF_2', Y_30) | ~in_environment('#skF_2', Y_113) | ~greater(Y_30, Y_113) | ~greater(start_time(E_350), Y_30) | ~environment(E_350) | ~greater('#skF_3', appear(first_movers, E_350)) | ~greater(start_time(E_350), '#skF_3') | ~greater(appear(an_organisation, E_350), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_350))))).
% 15.61/5.25 tff(c_4178, plain, (![E_125, E_363]: (in_environment('#skF_2', appear(first_movers, E_125)) | ~in_environment('#skF_2', start_time(E_125)) | ~environment(E_125) | ~greater(appear(an_organisation, E_363), appear(first_movers, E_125)) | ~in_environment('#skF_2', start_time(E_363)) | ~environment(E_363) | ~greater('#skF_3', appear(first_movers, E_363)) | ~greater(appear(an_organisation, E_363), '#skF_3')))).
% 15.61/5.25 tff(c_3848, plain, (![Y_166, E_350]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, start_time(E_350)) | ~greater(appear(an_organisation, '#skF_2'), Y_166) | ~environment(E_350) | ~greater('#skF_3', appear(first_movers, E_350)) | ~greater(start_time(E_350), '#skF_3') | ~greater(appear(an_organisation, E_350), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_350))))).
% 15.61/5.25 tff(c_4183, plain, (![Y_30, E_363, Y_171]: (in_environment('#skF_2', Y_30) | ~greater(Y_30, appear(an_organisation, E_363)) | ~greater(Y_171, Y_30) | ~greater(Y_171, '#skF_3') | ~greater('#skF_3', Y_171) | ~in_environment('#skF_2', start_time(E_363)) | ~environment(E_363) | ~greater('#skF_3', appear(first_movers, E_363)) | ~greater(appear(an_organisation, E_363), '#skF_3')))).
% 15.61/5.25 tff(c_5618, plain, (![E_19]: (selection_favors(first_movers, efficient_producers, start_time(E_19)) | cardinality_at_time(efficient_producers, start_time(E_19))!=zero | appear(first_movers, E_19)=start_time(E_19) | ~environment(E_19)))).
% 15.61/5.25 tff(c_3849, plain, (![Y_166, E_350]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, start_time(E_350)) | ~greater(start_time('#skF_2'), Y_166) | ~environment(E_350) | ~greater('#skF_3', appear(first_movers, E_350)) | ~greater(start_time(E_350), '#skF_3') | ~greater(appear(an_organisation, E_350), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_350))))).
% 15.61/5.26 tff(c_5597, plain, (![E_19]: (selection_favors(first_movers, first_movers, start_time(E_19)) | cardinality_at_time(first_movers, start_time(E_19))!=zero | appear(first_movers, E_19)=start_time(E_19) | ~environment(E_19)))).
% 15.61/5.26 tff(c_5547, plain, (![S2_107, E_19, E_109]: (selection_favors(first_movers, S2_107, start_time(E_19)) | cardinality_at_time(S2_107, start_time(E_19))!=zero | ~subpopulation(S2_107, E_109, start_time(E_19)) | ~subpopulation(first_movers, E_109, start_time(E_19)) | ~environment(E_109) | appear(first_movers, E_19)=start_time(E_19) | ~environment(E_19)))).
% 15.61/5.26 tff(c_3840, plain, (![E_350]: ('#skF_1'('#skF_2', start_time(E_350))=first_movers | '#skF_1'('#skF_2', start_time(E_350))=efficient_producers | ~environment(E_350) | ~greater('#skF_3', appear(first_movers, E_350)) | ~greater(start_time(E_350), '#skF_3') | ~greater(appear(an_organisation, E_350), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_350))))).
% 15.61/5.26 tff(c_3689, plain, (![E_339]: ('#skF_1'('#skF_2', appear(first_movers, E_339))=first_movers | '#skF_1'('#skF_2', appear(first_movers, E_339))=efficient_producers | ~in_environment('#skF_2', appear(first_movers, E_339)) | ~greater(appear(an_organisation, E_339), start_time('#skF_2')) | appear(first_movers, E_339)=appear(an_organisation, E_339) | ~environment(E_339)))).
% 15.61/5.26 tff(c_5337, plain, (![Y_449, Y_169, E_451]: (in_environment('#skF_2', Y_449) | ~greater(Y_449, Y_169) | ~greater(appear(an_organisation, E_451), Y_449) | ~in_environment('#skF_2', start_time(E_451)) | ~environment(E_451) | ~greater('#skF_3', appear(first_movers, E_451)) | ~greater(appear(an_organisation, E_451), '#skF_3') | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.26 tff(c_3690, plain, (![E_339, Y_209]: (in_environment('#skF_2', appear(first_movers, E_339)) | ~greater(Y_209, appear(first_movers, E_339)) | ~greater(Y_209, '#skF_3') | ~greater('#skF_3', Y_209) | ~greater(appear(an_organisation, E_339), start_time('#skF_2')) | appear(first_movers, E_339)=appear(an_organisation, E_339) | ~environment(E_339)))).
% 15.61/5.26 tff(c_2626, plain, (![E_132, E_263]: (in_environment('#skF_2', appear(first_movers, E_132)) | ~in_environment('#skF_2', appear(an_organisation, E_132)) | ~environment(E_132) | ~greater(appear(first_movers, E_263), appear(first_movers, E_132)) | ~in_environment('#skF_2', appear(an_organisation, E_263)) | ~environment(E_263) | ~greater('#skF_3', appear(first_movers, E_263))))).
% 15.61/5.26 tff(c_5415, plain, (![E_458]: (~greater(appear(an_organisation, E_458), appear(efficient_producers, '#skF_2')) | ~in_environment('#skF_2', start_time(E_458)) | ~environment(E_458) | ~greater('#skF_3', appear(first_movers, E_458)) | ~greater(appear(an_organisation, E_458), '#skF_3')))).
% 15.61/5.26 tff(c_5338, plain, (![Y_449, E_451]: (in_environment('#skF_2', Y_449) | ~greater(Y_449, appear(an_organisation, '#skF_2')) | ~greater(appear(an_organisation, E_451), Y_449) | ~in_environment('#skF_2', start_time(E_451)) | ~environment(E_451) | ~greater('#skF_3', appear(first_movers, E_451)) | ~greater(appear(an_organisation, E_451), '#skF_3')))).
% 15.61/5.26 tff(c_5379, plain, (![E_455]: (~greater(appear(an_organisation, E_455), appear(efficient_producers, e)) | ~in_environment('#skF_2', start_time(E_455)) | ~environment(E_455) | ~greater('#skF_3', appear(first_movers, E_455)) | ~greater(appear(an_organisation, E_455), '#skF_3')))).
% 15.61/5.26 tff(c_5342, plain, (![Y_449, E_451]: (in_environment('#skF_2', Y_449) | ~greater(Y_449, start_time('#skF_2')) | ~greater(appear(an_organisation, E_451), Y_449) | ~in_environment('#skF_2', start_time(E_451)) | ~environment(E_451) | ~greater('#skF_3', appear(first_movers, E_451)) | ~greater(appear(an_organisation, E_451), '#skF_3')))).
% 15.61/5.26 tff(c_5343, plain, (![Y_449, E_451]: (in_environment('#skF_2', Y_449) | ~greater(Y_449, '#skF_3') | ~greater(appear(an_organisation, E_451), Y_449) | ~in_environment('#skF_2', start_time(E_451)) | ~environment(E_451) | ~greater('#skF_3', appear(first_movers, E_451)) | ~greater(appear(an_organisation, E_451), '#skF_3')))).
% 15.61/5.26 tff(c_4192, plain, (![Y_30, Y_113, E_363]: (in_environment('#skF_2', Y_30) | ~in_environment('#skF_2', Y_113) | ~greater(Y_30, Y_113) | ~greater(appear(an_organisation, E_363), Y_30) | ~in_environment('#skF_2', start_time(E_363)) | ~environment(E_363) | ~greater('#skF_3', appear(first_movers, E_363)) | ~greater(appear(an_organisation, E_363), '#skF_3')))).
% 15.61/5.26 tff(c_5311, plain, (![E_361]: (in_environment('#skF_2', appear(an_organisation, E_361)) | ~in_environment('#skF_2', start_time(E_361)) | ~environment(E_361) | ~greater('#skF_3', appear(first_movers, E_361)) | ~greater(appear(an_organisation, E_361), appear(efficient_producers, e))))).
% 15.61/5.26 tff(c_2577, plain, (![E_261, E_248]: (in_environment('#skF_2', appear(first_movers, E_261)) | ~in_environment('#skF_2', appear(an_organisation, E_261)) | ~environment(E_261) | ~greater(appear(first_movers, E_248), appear(first_movers, E_261)) | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater('#skF_3', appear(first_movers, E_248))))).
% 15.61/5.26 tff(c_5231, plain, (![S2_3, E_1]: (selection_favors(efficient_producers, S2_3, appear(an_organisation, '#skF_2')) | cardinality_at_time(S2_3, appear(an_organisation, '#skF_2'))!=zero | ~subpopulation(S2_3, E_1, appear(an_organisation, '#skF_2')) | ~subpopulation(efficient_producers, E_1, appear(an_organisation, '#skF_2')) | ~environment(E_1)))).
% 15.61/5.26 tff(c_5108, plain, (![E_5]: (selection_favors('#skF_1'(E_5, appear(an_organisation, '#skF_2')), first_movers, appear(an_organisation, '#skF_2')) | ~subpopulation('#skF_1'(E_5, appear(an_organisation, '#skF_2')), '#skF_2', appear(an_organisation, '#skF_2')) | ~greater(number_of_organizations(E_5, appear(an_organisation, '#skF_2')), zero) | ~environment(E_5)))).
% 15.61/5.26 tff(c_3850, plain, (![Y_166, E_350]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, start_time(E_350)) | ~greater('#skF_3', Y_166) | ~environment(E_350) | ~greater('#skF_3', appear(first_movers, E_350)) | ~greater(start_time(E_350), '#skF_3') | ~greater(appear(an_organisation, E_350), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_350))))).
% 15.61/5.26 tff(c_2828, plain, (![E_5]: (selection_favors('#skF_1'(E_5, appear(an_organisation, '#skF_2')), efficient_producers, appear(an_organisation, '#skF_2')) | ~subpopulation('#skF_1'(E_5, appear(an_organisation, '#skF_2')), '#skF_2', appear(an_organisation, '#skF_2')) | ~greater(number_of_organizations(E_5, appear(an_organisation, '#skF_2')), zero) | ~environment(E_5)))).
% 15.61/5.26 tff(c_3208, plain, (![E_307]: ('#skF_1'('#skF_2', appear(first_movers, E_307))=first_movers | '#skF_1'('#skF_2', appear(first_movers, E_307))=efficient_producers | ~in_environment('#skF_2', appear(first_movers, E_307)) | ~greater(start_time(E_307), start_time('#skF_2')) | appear(first_movers, E_307)=start_time(E_307) | ~environment(E_307)))).
% 15.61/5.26 tff(c_4187, plain, (![Y_166, E_363]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, appear(an_organisation, E_363)) | ~greater(appear(an_organisation, '#skF_2'), Y_166) | ~in_environment('#skF_2', start_time(E_363)) | ~environment(E_363) | ~greater('#skF_3', appear(first_movers, E_363)) | ~greater(appear(an_organisation, E_363), '#skF_3')))).
% 15.61/5.26 tff(c_3388, plain, (![E_318]: (selection_favors(efficient_producers, '#skF_1'(E_318, start_time('#skF_2')), start_time('#skF_2')) | cardinality_at_time('#skF_1'(E_318, start_time('#skF_2')), start_time('#skF_2'))!=zero | ~subpopulation(efficient_producers, E_318, start_time('#skF_2')) | ~greater(number_of_organizations(E_318, start_time('#skF_2')), zero) | ~environment(E_318)))).
% 15.61/5.26 tff(c_2629, plain, (![E_125, E_263]: (in_environment('#skF_2', appear(first_movers, E_125)) | ~in_environment('#skF_2', start_time(E_125)) | ~environment(E_125) | ~greater(appear(first_movers, E_263), appear(first_movers, E_125)) | ~in_environment('#skF_2', appear(an_organisation, E_263)) | ~environment(E_263) | ~greater('#skF_3', appear(first_movers, E_263))))).
% 15.61/5.26 tff(c_5105, plain, (selection_favors(first_movers, first_movers, appear(an_organisation, '#skF_2')))).
% 15.61/5.26 tff(c_5097, plain, (selection_favors(first_movers, efficient_producers, appear(an_organisation, '#skF_2')))).
% 15.61/5.26 tff(c_5098, plain, (subpopulation(first_movers, '#skF_2', appear(an_organisation, '#skF_2')))).
% 15.61/5.26 tff(c_5019, plain, (![E_423]: ('#skF_1'('#skF_2', appear(an_organisation, E_423))=first_movers | '#skF_1'('#skF_2', appear(an_organisation, E_423))=efficient_producers | ~environment(E_423) | ~greater('#skF_3', appear(first_movers, E_423)) | ~greater(appear(an_organisation, E_423), '#skF_3') | ~greater(start_time(E_423), '#skF_3') | ~greater('#skF_3', start_time(E_423))))).
% 15.61/5.26 tff(c_5065, plain, (![S2_3, E_1]: (selection_favors(first_movers, S2_3, appear(an_organisation, '#skF_2')) | cardinality_at_time(S2_3, appear(an_organisation, '#skF_2'))!=zero | ~subpopulation(S2_3, E_1, appear(an_organisation, '#skF_2')) | ~subpopulation(first_movers, E_1, appear(an_organisation, '#skF_2')) | ~environment(E_1)))).
% 15.61/5.26 tff(c_5062, plain, (![E_346]: (in_environment('#skF_2', start_time(E_346)) | ~in_environment('#skF_2', appear(an_organisation, E_346)) | ~environment(E_346) | ~greater('#skF_3', appear(first_movers, E_346)) | ~greater(start_time(E_346), appear(efficient_producers, e))))).
% 15.61/5.26 tff(c_4179, plain, (![E_363]: ('#skF_1'('#skF_2', appear(an_organisation, E_363))=first_movers | '#skF_1'('#skF_2', appear(an_organisation, E_363))=efficient_producers | ~in_environment('#skF_2', start_time(E_363)) | ~environment(E_363) | ~greater('#skF_3', appear(first_movers, E_363)) | ~greater(appear(an_organisation, E_363), '#skF_3')))).
% 15.61/5.26 tff(c_3209, plain, (![E_307, Y_209]: (in_environment('#skF_2', appear(first_movers, E_307)) | ~greater(Y_209, appear(first_movers, E_307)) | ~greater(Y_209, '#skF_3') | ~greater('#skF_3', Y_209) | ~greater(start_time(E_307), start_time('#skF_2')) | appear(first_movers, E_307)=start_time(E_307) | ~environment(E_307)))).
% 15.61/5.26 tff(c_4903, plain, (![X_51, Y_360]: (in_environment('#skF_2', X_51) | ~greater(Y_360, X_51) | ~greater(Y_360, '#skF_3') | ~greater('#skF_3', Y_360) | ~greater(X_51, appear(efficient_producers, e))))).
% 15.61/5.26 tff(c_2457, plain, (![E_125, E_250]: (in_environment('#skF_2', appear(first_movers, E_125)) | ~in_environment('#skF_2', start_time(E_125)) | ~environment(E_125) | ~greater(appear(first_movers, E_250), appear(first_movers, E_125)) | ~in_environment('#skF_2', start_time(E_250)) | ~environment(E_250) | ~greater('#skF_3', appear(first_movers, E_250))))).
% 15.61/5.26 tff(c_4188, plain, (![Y_166, E_363]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, appear(an_organisation, E_363)) | ~greater(start_time('#skF_2'), Y_166) | ~in_environment('#skF_2', start_time(E_363)) | ~environment(E_363) | ~greater('#skF_3', appear(first_movers, E_363)) | ~greater(appear(an_organisation, E_363), '#skF_3')))).
% 15.61/5.26 tff(c_3702, plain, (![E_339]: (cardinality_at_time('#skF_1'('#skF_2', appear(first_movers, E_339)), t)!=zero | ~in_environment('#skF_2', appear(first_movers, E_339)) | ~greater(appear(an_organisation, E_339), start_time('#skF_2')) | appear(first_movers, E_339)=appear(an_organisation, E_339) | ~environment(E_339)))).
% 15.61/5.26 tff(c_3695, plain, (![E_339]: (in_environment('#skF_2', appear(first_movers, E_339)) | ~greater(appear(an_organisation, '#skF_2'), appear(first_movers, E_339)) | ~greater(appear(an_organisation, E_339), start_time('#skF_2')) | appear(first_movers, E_339)=appear(an_organisation, E_339) | ~environment(E_339)))).
% 15.61/5.27 tff(c_2634, plain, (![Y_30, E_263, Y_171]: (in_environment('#skF_2', Y_30) | ~greater(Y_30, appear(first_movers, E_263)) | ~greater(Y_171, Y_30) | ~greater(Y_171, '#skF_3') | ~greater('#skF_3', Y_171) | ~in_environment('#skF_2', appear(an_organisation, E_263)) | ~environment(E_263) | ~greater('#skF_3', appear(first_movers, E_263))))).
% 15.61/5.27 tff(c_3697, plain, (![E_339]: (in_environment('#skF_2', appear(first_movers, E_339)) | ~greater(start_time('#skF_2'), appear(first_movers, E_339)) | ~greater(appear(an_organisation, E_339), start_time('#skF_2')) | appear(first_movers, E_339)=appear(an_organisation, E_339) | ~environment(E_339)))).
% 15.61/5.27 tff(c_3221, plain, (![E_307]: (cardinality_at_time('#skF_1'('#skF_2', appear(first_movers, E_307)), t)!=zero | ~in_environment('#skF_2', appear(first_movers, E_307)) | ~greater(start_time(E_307), start_time('#skF_2')) | appear(first_movers, E_307)=start_time(E_307) | ~environment(E_307)))).
% 15.61/5.27 tff(c_4777, plain, (![E_405]: (~greater(appear(first_movers, E_405), appear(efficient_producers, '#skF_2')) | ~in_environment('#skF_2', appear(an_organisation, E_405)) | ~environment(E_405) | ~greater('#skF_3', appear(first_movers, E_405))))).
% 15.61/5.27 tff(c_4587, plain, (![Y_393, E_395]: (in_environment('#skF_2', Y_393) | ~greater(Y_393, appear(an_organisation, '#skF_2')) | ~greater(appear(first_movers, E_395), Y_393) | ~in_environment('#skF_2', appear(an_organisation, E_395)) | ~environment(E_395) | ~greater('#skF_3', appear(first_movers, E_395))))).
% 15.61/5.27 tff(c_4586, plain, (![Y_393, Y_169, E_395]: (in_environment('#skF_2', Y_393) | ~greater(Y_393, Y_169) | ~greater(appear(first_movers, E_395), Y_393) | ~in_environment('#skF_2', appear(an_organisation, E_395)) | ~environment(E_395) | ~greater('#skF_3', appear(first_movers, E_395)) | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.27 tff(c_4646, plain, (![E_399]: (~greater(appear(first_movers, E_399), appear(efficient_producers, e)) | ~in_environment('#skF_2', appear(an_organisation, E_399)) | ~environment(E_399) | ~greater('#skF_3', appear(first_movers, E_399))))).
% 15.61/5.27 tff(c_4588, plain, (![Y_393, E_395]: (in_environment('#skF_2', Y_393) | ~greater(Y_393, start_time('#skF_2')) | ~greater(appear(first_movers, E_395), Y_393) | ~in_environment('#skF_2', appear(an_organisation, E_395)) | ~environment(E_395) | ~greater('#skF_3', appear(first_movers, E_395))))).
% 15.61/5.27 tff(c_4592, plain, (![Y_393, E_395]: (in_environment('#skF_2', Y_393) | ~greater(Y_393, '#skF_3') | ~greater(appear(first_movers, E_395), Y_393) | ~in_environment('#skF_2', appear(an_organisation, E_395)) | ~environment(E_395) | ~greater('#skF_3', appear(first_movers, E_395))))).
% 15.61/5.27 tff(c_2643, plain, (![Y_30, Y_113, E_263]: (in_environment('#skF_2', Y_30) | ~in_environment('#skF_2', Y_113) | ~greater(Y_30, Y_113) | ~greater(appear(first_movers, E_263), Y_30) | ~in_environment('#skF_2', appear(an_organisation, E_263)) | ~environment(E_263) | ~greater('#skF_3', appear(first_movers, E_263))))).
% 15.61/5.27 tff(c_2886, plain, (![X_278, E_261]: (cardinality_at_time(X_278, appear(first_movers, E_261))=zero | ~greater(appear(X_278, '#skF_2'), appear(efficient_producers, e)) | ~in_environment('#skF_2', appear(an_organisation, E_261)) | ~environment(E_261) | ~greater('#skF_3', appear(first_movers, E_261))))).
% 15.61/5.27 tff(c_4546, plain, (![E_389]: (~greater(appear(first_movers, E_389), appear(efficient_producers, '#skF_2')) | ~in_environment('#skF_2', start_time(E_389)) | ~environment(E_389) | ~greater('#skF_3', appear(first_movers, E_389))))).
% 15.61/5.27 tff(c_4356, plain, (![Y_377, E_379]: (in_environment('#skF_2', Y_377) | ~greater(Y_377, appear(an_organisation, '#skF_2')) | ~greater(appear(first_movers, E_379), Y_377) | ~in_environment('#skF_2', start_time(E_379)) | ~environment(E_379) | ~greater('#skF_3', appear(first_movers, E_379))))).
% 15.61/5.27 tff(c_4355, plain, (![Y_377, Y_169, E_379]: (in_environment('#skF_2', Y_377) | ~greater(Y_377, Y_169) | ~greater(appear(first_movers, E_379), Y_377) | ~in_environment('#skF_2', start_time(E_379)) | ~environment(E_379) | ~greater('#skF_3', appear(first_movers, E_379)) | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.27 tff(c_4415, plain, (![E_383]: (~greater(appear(first_movers, E_383), appear(efficient_producers, e)) | ~in_environment('#skF_2', start_time(E_383)) | ~environment(E_383) | ~greater('#skF_3', appear(first_movers, E_383))))).
% 15.61/5.27 tff(c_4357, plain, (![Y_377, E_379]: (in_environment('#skF_2', Y_377) | ~greater(Y_377, start_time('#skF_2')) | ~greater(appear(first_movers, E_379), Y_377) | ~in_environment('#skF_2', start_time(E_379)) | ~environment(E_379) | ~greater('#skF_3', appear(first_movers, E_379))))).
% 15.61/5.27 tff(c_4361, plain, (![Y_377, E_379]: (in_environment('#skF_2', Y_377) | ~greater(Y_377, '#skF_3') | ~greater(appear(first_movers, E_379), Y_377) | ~in_environment('#skF_2', start_time(E_379)) | ~environment(E_379) | ~greater('#skF_3', appear(first_movers, E_379))))).
% 15.61/5.27 tff(c_2471, plain, (![Y_30, Y_113, E_250]: (in_environment('#skF_2', Y_30) | ~in_environment('#skF_2', Y_113) | ~greater(Y_30, Y_113) | ~greater(appear(first_movers, E_250), Y_30) | ~in_environment('#skF_2', start_time(E_250)) | ~environment(E_250) | ~greater('#skF_3', appear(first_movers, E_250))))).
% 15.61/5.27 tff(c_2199, plain, (![E_33]: ('#skF_1'(E_33, appear(efficient_producers, e))=first_movers | '#skF_1'(E_33, appear(efficient_producers, e))=efficient_producers | ~in_environment(E_33, appear(efficient_producers, e)) | appear(first_movers, E_33)=appear(an_organisation, E_33) | ~environment(E_33)))).
% 15.61/5.27 tff(c_3698, plain, (![E_339]: (in_environment('#skF_2', appear(first_movers, E_339)) | ~greater('#skF_3', appear(first_movers, E_339)) | ~greater(appear(an_organisation, E_339), start_time('#skF_2')) | appear(first_movers, E_339)=appear(an_organisation, E_339) | ~environment(E_339)))).
% 15.61/5.27 tff(c_3214, plain, (![E_307]: (in_environment('#skF_2', appear(first_movers, E_307)) | ~greater(appear(an_organisation, '#skF_2'), appear(first_movers, E_307)) | ~greater(start_time(E_307), start_time('#skF_2')) | appear(first_movers, E_307)=start_time(E_307) | ~environment(E_307)))).
% 15.61/5.27 tff(c_3708, plain, (![X_26, E_339]: (greater(X_26, appear(an_organisation, '#skF_2')) | ~greater(X_26, appear(first_movers, E_339)) | ~greater(appear(an_organisation, E_339), start_time('#skF_2')) | appear(first_movers, E_339)=appear(an_organisation, E_339) | ~environment(E_339)))).
% 15.61/5.27 tff(c_4281, plain, (![X_51]: (in_environment('#skF_2', X_51) | ~greater(appear(an_organisation, '#skF_2'), X_51) | ~greater(X_51, appear(efficient_producers, e))))).
% 15.61/5.27 tff(c_3390, plain, (![E_316]: (selection_favors('#skF_1'(E_316, start_time('#skF_2')), efficient_producers, start_time('#skF_2')) | ~subpopulation('#skF_1'(E_316, start_time('#skF_2')), '#skF_2', start_time('#skF_2')) | ~greater(number_of_organizations(E_316, start_time('#skF_2')), zero) | ~environment(E_316)))).
% 15.61/5.27 tff(c_4189, plain, (![Y_166, E_363]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, appear(an_organisation, E_363)) | ~greater('#skF_3', Y_166) | ~in_environment('#skF_2', start_time(E_363)) | ~environment(E_363) | ~greater('#skF_3', appear(first_movers, E_363)) | ~greater(appear(an_organisation, E_363), '#skF_3')))).
% 15.61/5.27 tff(c_2889, plain, (![X_278, E_248]: (cardinality_at_time(X_278, appear(first_movers, E_248))=zero | ~greater(appear(X_278, '#skF_2'), appear(efficient_producers, e)) | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater('#skF_3', appear(first_movers, E_248))))).
% 15.61/5.27 tff(c_4099, plain, (![E_361]: (in_environment('#skF_2', appear(an_organisation, E_361)) | ~in_environment('#skF_2', start_time(E_361)) | ~environment(E_361) | ~greater('#skF_3', appear(first_movers, E_361)) | ~greater(appear(an_organisation, E_361), start_time('#skF_2'))))).
% 15.61/5.27 tff(c_4102, plain, (![E_361]: (in_environment('#skF_2', appear(an_organisation, E_361)) | ~in_environment('#skF_2', start_time(E_361)) | ~environment(E_361) | ~greater('#skF_3', appear(first_movers, E_361)) | ~greater(appear(an_organisation, E_361), '#skF_3')))).
% 15.61/5.27 tff(c_2746, plain, (![E_248, Y_274]: (in_environment('#skF_2', appear(an_organisation, E_248)) | ~in_environment('#skF_2', Y_274) | ~greater(appear(an_organisation, E_248), Y_274) | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater('#skF_3', appear(first_movers, E_248))))).
% 15.61/5.27 tff(c_2462, plain, (![Y_30, E_250, Y_171]: (in_environment('#skF_2', Y_30) | ~greater(Y_30, appear(first_movers, E_250)) | ~greater(Y_171, Y_30) | ~greater(Y_171, '#skF_3') | ~greater('#skF_3', Y_171) | ~in_environment('#skF_2', start_time(E_250)) | ~environment(E_250) | ~greater('#skF_3', appear(first_movers, E_250))))).
% 15.61/5.27 tff(c_4047, plain, (![E_356]: (~greater(appear(an_organisation, E_356), appear(efficient_producers, e)) | appear(first_movers, E_356)=appear(an_organisation, E_356) | ~environment(E_356)))).
% 15.61/5.27 tff(c_3216, plain, (![E_307]: (in_environment('#skF_2', appear(first_movers, E_307)) | ~greater(start_time('#skF_2'), appear(first_movers, E_307)) | ~greater(start_time(E_307), start_time('#skF_2')) | appear(first_movers, E_307)=start_time(E_307) | ~environment(E_307)))).
% 15.61/5.27 tff(c_3884, plain, (![X_51]: (in_environment('#skF_2', X_51) | ~greater(start_time('#skF_2'), X_51) | ~greater(X_51, appear(efficient_producers, e))))).
% 15.61/5.27 tff(c_3784, plain, (![E_348]: (in_environment('#skF_2', start_time(E_348)) | ~environment(E_348) | ~greater('#skF_3', appear(first_movers, E_348)) | ~greater(start_time(E_348), '#skF_3') | ~greater(appear(an_organisation, E_348), '#skF_3') | ~greater('#skF_3', appear(an_organisation, E_348))))).
% 15.61/5.27 tff(c_3769, plain, (![E_346]: (in_environment('#skF_2', start_time(E_346)) | ~in_environment('#skF_2', appear(an_organisation, E_346)) | ~environment(E_346) | ~greater('#skF_3', appear(first_movers, E_346)) | ~greater(start_time(E_346), start_time('#skF_2'))))).
% 15.61/5.27 tff(c_3775, plain, (![E_346]: (in_environment('#skF_2', start_time(E_346)) | ~in_environment('#skF_2', appear(an_organisation, E_346)) | ~environment(E_346) | ~greater('#skF_3', appear(first_movers, E_346)) | ~greater(start_time(E_346), '#skF_3')))).
% 15.61/5.27 tff(c_2633, plain, (![E_263, Y_113]: (in_environment('#skF_2', start_time(E_263)) | ~in_environment('#skF_2', Y_113) | ~greater(start_time(E_263), Y_113) | ~in_environment('#skF_2', appear(an_organisation, E_263)) | ~environment(E_263) | ~greater('#skF_3', appear(first_movers, E_263))))).
% 15.61/5.27 tff(c_2119, plain, (![E_5]: (selection_favors(efficient_producers, '#skF_1'(E_5, '#skF_3'), '#skF_3') | cardinality_at_time('#skF_1'(E_5, '#skF_3'), '#skF_3')!=zero | ~subpopulation(efficient_producers, E_5, '#skF_3') | ~greater(number_of_organizations(E_5, '#skF_3'), zero) | ~environment(E_5)))).
% 15.61/5.27 tff(c_3217, plain, (![E_307]: (in_environment('#skF_2', appear(first_movers, E_307)) | ~greater('#skF_3', appear(first_movers, E_307)) | ~greater(start_time(E_307), start_time('#skF_2')) | appear(first_movers, E_307)=start_time(E_307) | ~environment(E_307)))).
% 15.61/5.27 tff(c_3227, plain, (![X_26, E_307]: (greater(X_26, appear(an_organisation, '#skF_2')) | ~greater(X_26, appear(first_movers, E_307)) | ~greater(start_time(E_307), start_time('#skF_2')) | appear(first_movers, E_307)=start_time(E_307) | ~environment(E_307)))).
% 15.61/5.27 tff(c_3729, plain, (![X_51]: (in_environment('#skF_2', X_51) | ~greater('#skF_3', X_51) | ~greater(X_51, appear(efficient_producers, e))))).
% 15.61/5.27 tff(c_789, plain, (![E_45]: (greater(appear(first_movers, E_45), appear(an_organisation, '#skF_2')) | ~greater(appear(an_organisation, E_45), start_time('#skF_2')) | appear(first_movers, E_45)=appear(an_organisation, E_45) | ~environment(E_45)))).
% 15.61/5.28 tff(c_2638, plain, (![Y_166, E_263]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, appear(first_movers, E_263)) | ~greater(appear(an_organisation, '#skF_2'), Y_166) | ~in_environment('#skF_2', appear(an_organisation, E_263)) | ~environment(E_263) | ~greater('#skF_3', appear(first_movers, E_263))))).
% 15.61/5.28 tff(c_1761, plain, (![E_202]: (cardinality_at_time('#skF_1'(E_202, appear(efficient_producers, e)), t)!=zero | ~in_environment(E_202, appear(efficient_producers, e)) | appear(first_movers, E_202)=appear(an_organisation, E_202) | ~environment(E_202)))).
% 15.61/5.28 tff(c_2466, plain, (![Y_166, E_250]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, appear(first_movers, E_250)) | ~greater(appear(an_organisation, '#skF_2'), Y_166) | ~in_environment('#skF_2', start_time(E_250)) | ~environment(E_250) | ~greater('#skF_3', appear(first_movers, E_250))))).
% 15.61/5.28 tff(c_3592, plain, (![E_332]: (~greater(start_time(E_332), appear(efficient_producers, e)) | appear(first_movers, E_332)=start_time(E_332) | ~environment(E_332)))).
% 15.61/5.28 tff(c_3442, plain, (![E_324, E_33]: (in_environment(E_324, appear(first_movers, E_33)) | ~in_environment(E_324, appear(an_organisation, E_33)) | ~environment(E_324) | ~greater(start_time(E_324), appear(efficient_producers, e)) | ~environment(E_33)))).
% 15.61/5.28 tff(c_3459, plain, (cardinality_at_time(first_movers, start_time('#skF_2'))!=zero)).
% 15.61/5.28 tff(c_3250, plain, (![E_5, T_6]: (selection_favors('#skF_1'(E_5, T_6), first_movers, T_6) | cardinality_at_time(first_movers, T_6)!=zero | ~in_environment(E_5, T_6) | ~greater(number_of_organizations(E_5, T_6), zero) | ~environment(E_5)))).
% 15.61/5.28 tff(c_2587, plain, (![E_19, E_261]: (in_environment(E_19, appear(first_movers, E_261)) | ~in_environment(E_19, appear(an_organisation, E_261)) | ~environment(E_261) | ~greater(start_time(E_19), appear(first_movers, E_261)) | ~environment(E_19)))).
% 15.61/5.28 tff(c_2639, plain, (![Y_166, E_263]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, appear(first_movers, E_263)) | ~greater(start_time('#skF_2'), Y_166) | ~in_environment('#skF_2', appear(an_organisation, E_263)) | ~environment(E_263) | ~greater('#skF_3', appear(first_movers, E_263))))).
% 15.61/5.28 tff(c_3090, plain, (![E_5, T_6]: (selection_favors('#skF_1'(E_5, T_6), efficient_producers, T_6) | cardinality_at_time(efficient_producers, T_6)!=zero | ~in_environment(E_5, T_6) | ~greater(number_of_organizations(E_5, T_6), zero) | ~environment(E_5)))).
% 15.61/5.28 tff(c_3386, plain, (![E_316]: (selection_favors('#skF_1'(E_316, '#skF_3'), efficient_producers, '#skF_3') | ~subpopulation('#skF_1'(E_316, '#skF_3'), '#skF_2', '#skF_3') | ~greater(number_of_organizations(E_316, '#skF_3'), zero) | ~environment(E_316)))).
% 15.61/5.28 tff(c_918, plain, (![E_145, T_6, E_5]: (selection_favors('#skF_1'(E_145, T_6), '#skF_1'(E_5, T_6), T_6) | cardinality_at_time('#skF_1'(E_5, T_6), T_6)!=zero | ~subpopulation('#skF_1'(E_145, T_6), E_5, T_6) | ~greater(number_of_organizations(E_145, T_6), zero) | ~environment(E_145) | ~greater(number_of_organizations(E_5, T_6), zero) | ~environment(E_5)))).
% 15.61/5.28 tff(c_3359, plain, (selection_favors(efficient_producers, efficient_producers, appear(an_organisation, '#skF_2')))).
% 15.61/5.28 tff(c_3345, plain, (selection_favors(efficient_producers, first_movers, appear(an_organisation, '#skF_2')))).
% 15.61/5.28 tff(c_3318, plain, (![X_26]: (greater(X_26, appear(an_organisation, '#skF_2')) | ~greater(X_26, appear(efficient_producers, e))))).
% 15.61/5.28 tff(c_3230, plain, (greater(appear(efficient_producers, e), appear(an_organisation, '#skF_2')))).
% 15.61/5.28 tff(c_919, plain, (![E_145, T_25, E_24]: (selection_favors('#skF_1'(E_145, T_25), first_movers, T_25) | cardinality_at_time(first_movers, T_25)!=zero | ~subpopulation('#skF_1'(E_145, T_25), E_24, T_25) | ~greater(number_of_organizations(E_145, T_25), zero) | ~environment(E_145) | ~in_environment(E_24, T_25) | ~environment(E_24)))).
% 15.61/5.28 tff(c_794, plain, (![E_43]: (greater(appear(first_movers, E_43), appear(an_organisation, '#skF_2')) | ~greater(start_time(E_43), start_time('#skF_2')) | appear(first_movers, E_43)=start_time(E_43) | ~environment(E_43)))).
% 15.61/5.28 tff(c_3155, plain, (![X_304]: (cardinality_at_time(X_304, appear(an_organisation, '#skF_2'))=zero | ~greater(appear(X_304, '#skF_2'), '#skF_3')))).
% 15.61/5.28 tff(c_3136, plain, (![X_302, E_303]: (cardinality_at_time(X_302, appear(an_organisation, '#skF_2'))=zero | ~in_environment(E_303, appear(an_organisation, '#skF_2')) | ~environment(E_303) | ~greater(appear(X_302, E_303), '#skF_3')))).
% 15.61/5.28 tff(c_671, plain, (![X_11, E_10]: (cardinality_at_time(X_11, appear(an_organisation, '#skF_2'))=zero | ~in_environment(E_10, appear(an_organisation, '#skF_2')) | ~environment(E_10) | ~greater(appear(X_11, E_10), start_time('#skF_2'))))).
% 15.61/5.28 tff(c_2467, plain, (![Y_166, E_250]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, appear(first_movers, E_250)) | ~greater(start_time('#skF_2'), Y_166) | ~in_environment('#skF_2', start_time(E_250)) | ~environment(E_250) | ~greater('#skF_3', appear(first_movers, E_250))))).
% 15.61/5.28 tff(c_2583, plain, (![E_261]: (in_environment('#skF_2', appear(first_movers, E_261)) | ~in_environment('#skF_2', appear(an_organisation, E_261)) | ~environment(E_261) | ~greater(appear(an_organisation, '#skF_2'), appear(first_movers, E_261))))).
% 15.61/5.28 tff(c_3046, plain, (![E_294]: (~greater(appear(an_organisation, E_294), '#skF_3') | appear(first_movers, E_294)=appear(an_organisation, E_294) | ~environment(E_294)))).
% 15.61/5.28 tff(c_920, plain, (![E_145, T_25, E_24]: (selection_favors('#skF_1'(E_145, T_25), efficient_producers, T_25) | cardinality_at_time(efficient_producers, T_25)!=zero | ~subpopulation('#skF_1'(E_145, T_25), E_24, T_25) | ~greater(number_of_organizations(E_145, T_25), zero) | ~environment(E_145) | ~in_environment(E_24, T_25) | ~environment(E_24)))).
% 15.61/5.28 tff(c_2982, plain, (![E_19]: (in_environment(E_19, appear(an_organisation, '#skF_2')) | ~in_environment(E_19, start_time('#skF_2')) | ~greater(appear(an_organisation, '#skF_2'), start_time(E_19)) | ~environment(E_19)))).
% 15.61/5.28 tff(c_2751, plain, (![E_272, Y_274]: (in_environment(E_272, appear(an_organisation, '#skF_2')) | ~in_environment(E_272, start_time('#skF_2')) | ~in_environment(E_272, Y_274) | ~environment(E_272) | ~greater(appear(an_organisation, '#skF_2'), Y_274)))).
% 15.61/5.28 tff(c_2950, plain, (![E_287, E_33]: (in_environment(E_287, appear(first_movers, E_33)) | ~in_environment(E_287, start_time(E_33)) | ~environment(E_287) | ~greater(start_time(E_287), appear(efficient_producers, e)) | ~environment(E_33)))).
% 15.61/5.28 tff(c_2420, plain, (![E_19, E_248]: (in_environment(E_19, appear(first_movers, E_248)) | ~in_environment(E_19, start_time(E_248)) | ~environment(E_248) | ~greater(start_time(E_19), appear(first_movers, E_248)) | ~environment(E_19)))).
% 15.61/5.28 tff(c_2580, plain, (![E_261, Y_169]: (in_environment('#skF_2', appear(first_movers, E_261)) | ~in_environment('#skF_2', appear(an_organisation, E_261)) | ~environment(E_261) | ~greater(Y_169, appear(first_movers, E_261)) | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.28 tff(c_909, plain, (![E_22]: ('#skF_1'(E_22, appear(first_movers, E_22))=first_movers | '#skF_1'(E_22, appear(first_movers, E_22))=efficient_producers | ~in_environment(E_22, appear(first_movers, E_22)) | ~environment(E_22)))).
% 15.61/5.28 tff(c_2894, plain, (![X_278, E_280]: (cardinality_at_time(X_278, start_time('#skF_2'))=zero | ~in_environment(E_280, start_time('#skF_2')) | ~environment(E_280) | ~greater(appear(X_278, E_280), appear(efficient_producers, e))))).
% 15.61/5.28 tff(c_2873, plain, (![X_26]: (greater(X_26, zero) | ~greater(X_26, number_of_organizations('#skF_2', appear(an_organisation, '#skF_2')))))).
% 15.61/5.28 tff(c_176, plain, (![X_72, E_33, E_74]: (cardinality_at_time(X_72, appear(first_movers, E_33))=zero | ~in_environment(E_74, appear(first_movers, E_33)) | ~environment(E_74) | ~greater(appear(X_72, E_74), appear(efficient_producers, e)) | ~environment(E_33)))).
% 15.61/5.28 tff(c_2823, plain, (greater(number_of_organizations('#skF_2', appear(an_organisation, '#skF_2')), zero))).
% 15.61/5.28 tff(c_2822, plain, (subpopulation(efficient_producers, '#skF_2', appear(an_organisation, '#skF_2')))).
% 15.61/5.28 tff(c_2766, plain, ('#skF_1'('#skF_2', appear(an_organisation, '#skF_2'))=efficient_producers)).
% 15.61/5.28 tff(c_2640, plain, (![Y_166, E_263]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, appear(first_movers, E_263)) | ~greater('#skF_3', Y_166) | ~in_environment('#skF_2', appear(an_organisation, E_263)) | ~environment(E_263) | ~greater('#skF_3', appear(first_movers, E_263))))).
% 15.61/5.28 tff(c_908, plain, (![E_80]: ('#skF_1'(E_80, appear(an_organisation, E_80))=first_movers | '#skF_1'(E_80, appear(an_organisation, E_80))=efficient_producers | ~in_environment(E_80, appear(an_organisation, E_80)) | ~environment(E_80)))).
% 15.61/5.28 tff(c_503, plain, (![E_110, E_22, Y_113]: (in_environment(E_110, appear(an_organisation, E_22)) | ~in_environment(E_110, appear(first_movers, E_22)) | ~in_environment(E_110, Y_113) | ~environment(E_110) | ~greater(appear(an_organisation, E_22), Y_113) | ~environment(E_22)))).
% 15.61/5.28 tff(c_2715, plain, (![E_269]: (in_environment(E_269, start_time('#skF_2')) | ~in_environment(E_269, appear(an_organisation, '#skF_2')) | ~environment(E_269) | ~greater(start_time(E_269), '#skF_3')))).
% 15.61/5.28 tff(c_2696, plain, (![E_19]: (in_environment(E_19, start_time('#skF_2')) | ~in_environment(E_19, appear(an_organisation, '#skF_2')) | ~greater(start_time(E_19), start_time('#skF_2')) | ~environment(E_19)))).
% 15.61/5.28 tff(c_2413, plain, (![E_248, Y_169]: (in_environment('#skF_2', appear(first_movers, E_248)) | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater(Y_169, appear(first_movers, E_248)) | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.28 tff(c_2523, plain, (![E_254, X_29]: (in_environment(E_254, start_time('#skF_2')) | ~in_environment(E_254, X_29) | ~in_environment(E_254, appear(an_organisation, '#skF_2')) | ~environment(E_254) | ~greater(X_29, start_time('#skF_2'))))).
% 15.61/5.28 tff(c_2586, plain, (![E_261]: (in_environment('#skF_2', appear(first_movers, E_261)) | ~in_environment('#skF_2', appear(an_organisation, E_261)) | ~environment(E_261) | ~greater(start_time('#skF_2'), appear(first_movers, E_261))))).
% 15.61/5.28 tff(c_2590, plain, (![E_261]: (in_environment('#skF_2', appear(first_movers, E_261)) | ~in_environment('#skF_2', appear(an_organisation, E_261)) | ~environment(E_261) | ~greater('#skF_3', appear(first_movers, E_261))))).
% 15.61/5.28 tff(c_745, plain, (![E_131, E_132, X_29]: (in_environment(E_131, appear(first_movers, E_132)) | ~in_environment(E_131, X_29) | ~in_environment(E_131, appear(an_organisation, E_132)) | ~environment(E_131) | ~environment(E_132) | ~greater(X_29, appear(first_movers, E_132))))).
% 15.61/5.28 tff(c_2416, plain, (![E_248]: (in_environment('#skF_2', appear(first_movers, E_248)) | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater(appear(an_organisation, '#skF_2'), appear(first_movers, E_248))))).
% 15.61/5.28 tff(c_1679, plain, (![E_43]: (in_environment(E_43, appear(first_movers, E_43)) | ~greater(start_time(E_43), appear(first_movers, E_43)) | appear(first_movers, E_43)=start_time(E_43) | ~environment(E_43)))).
% 15.61/5.29 tff(c_2519, plain, (![E_254]: (in_environment(E_254, start_time('#skF_2')) | ~in_environment(E_254, '#skF_3') | ~in_environment(E_254, appear(an_organisation, '#skF_2')) | ~environment(E_254)))).
% 15.61/5.29 tff(c_744, plain, (![E_131, T2_133]: (in_environment(E_131, start_time('#skF_2')) | ~greater_or_equal(T2_133, start_time('#skF_2')) | ~in_environment(E_131, T2_133) | ~in_environment(E_131, appear(an_organisation, '#skF_2')) | ~environment(E_131)))).
% 15.61/5.29 tff(c_2468, plain, (![Y_166, E_250]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, appear(first_movers, E_250)) | ~greater('#skF_3', Y_166) | ~in_environment('#skF_2', start_time(E_250)) | ~environment(E_250) | ~greater('#skF_3', appear(first_movers, E_250))))).
% 15.61/5.29 tff(c_2419, plain, (![E_248]: (in_environment('#skF_2', appear(first_movers, E_248)) | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater(start_time('#skF_2'), appear(first_movers, E_248))))).
% 15.61/5.29 tff(c_2423, plain, (![E_248]: (in_environment('#skF_2', appear(first_movers, E_248)) | ~in_environment('#skF_2', start_time(E_248)) | ~environment(E_248) | ~greater('#skF_3', appear(first_movers, E_248))))).
% 15.61/5.29 tff(c_647, plain, (![E_124, E_125, X_29]: (in_environment(E_124, appear(first_movers, E_125)) | ~in_environment(E_124, X_29) | ~in_environment(E_124, start_time(E_125)) | ~environment(E_124) | ~environment(E_125) | ~greater(X_29, appear(first_movers, E_125))))).
% 15.61/5.29 tff(c_1710, plain, (![X_51, E_33]: (greater(X_51, appear(an_organisation, E_33)) | appear(first_movers, E_33)=appear(an_organisation, E_33) | ~greater(X_51, appear(efficient_producers, e)) | ~environment(E_33)))).
% 15.61/5.29 tff(c_2385, plain, (![Y_169]: ('#skF_1'('#skF_2', Y_169)=first_movers | '#skF_1'('#skF_2', Y_169)=efficient_producers | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.29 tff(c_2231, plain, (![X_51]: ('#skF_1'('#skF_2', X_51)=first_movers | '#skF_1'('#skF_2', X_51)=efficient_producers | ~in_environment('#skF_2', X_51) | ~greater(X_51, '#skF_3')))).
% 15.61/5.29 tff(c_2366, plain, (![X_26]: (greater(X_26, zero) | ~greater(X_26, number_of_organizations('#skF_2', '#skF_3'))))).
% 15.61/5.29 tff(c_2300, plain, (greater(number_of_organizations('#skF_2', '#skF_3'), zero))).
% 15.61/5.29 tff(c_2299, plain, (subpopulation(efficient_producers, '#skF_2', '#skF_3'))).
% 15.61/5.29 tff(c_504, plain, (![E_110, E_20, Y_113]: (in_environment(E_110, start_time(E_20)) | ~in_environment(E_110, appear(first_movers, E_20)) | ~in_environment(E_110, Y_113) | ~environment(E_110) | ~greater(start_time(E_20), Y_113) | ~environment(E_20)))).
% 15.61/5.29 tff(c_2254, plain, (selection_favors(efficient_producers, efficient_producers, start_time('#skF_2')))).
% 15.61/5.29 tff(c_2239, plain, ('#skF_1'('#skF_2', '#skF_3')=efficient_producers)).
% 15.61/5.29 tff(c_1828, plain, (![S2_3, E_1]: (selection_favors(efficient_producers, S2_3, start_time('#skF_2')) | cardinality_at_time(S2_3, start_time('#skF_2'))!=zero | ~subpopulation(S2_3, E_1, start_time('#skF_2')) | ~subpopulation(efficient_producers, E_1, start_time('#skF_2')) | ~environment(E_1)))).
% 15.61/5.29 tff(c_2205, plain, (![X_26]: ('#skF_1'('#skF_2', X_26)=first_movers | '#skF_1'('#skF_2', X_26)=efficient_producers | ~in_environment('#skF_2', X_26) | ~greater(X_26, start_time('#skF_2'))))).
% 15.61/5.29 tff(c_907, plain, (![E_80, X_29]: ('#skF_1'(E_80, X_29)=first_movers | '#skF_1'(E_80, X_29)=efficient_producers | ~in_environment(E_80, X_29) | ~environment(E_80) | ~greater(X_29, appear(an_organisation, E_80))))).
% 15.61/5.29 tff(c_273, plain, (![E_89]: (cardinality_at_time(first_movers, appear(an_organisation, E_89))=zero | ~in_environment(E_89, appear(an_organisation, E_89)) | appear(first_movers, E_89)=appear(an_organisation, E_89) | ~environment(E_89)))).
% 15.61/5.29 tff(c_2168, plain, (cardinality_at_time(first_movers, '#skF_3')!=zero)).
% 15.61/5.29 tff(c_2167, plain, (selection_favors(efficient_producers, efficient_producers, '#skF_3'))).
% 15.61/5.29 tff(c_2102, plain, (![Y_225]: (~greater(Y_225, appear(efficient_producers, '#skF_2')) | ~greater(Y_225, '#skF_3') | ~greater('#skF_3', Y_225)))).
% 15.61/5.29 tff(c_1085, plain, (![S2_107, E_109]: (selection_favors(efficient_producers, S2_107, '#skF_3') | cardinality_at_time(S2_107, '#skF_3')!=zero | ~subpopulation(S2_107, E_109, '#skF_3') | ~subpopulation(efficient_producers, E_109, '#skF_3') | ~environment(E_109)))).
% 15.61/5.29 tff(c_1800, plain, (![Y_207, Y_209]: (in_environment('#skF_2', Y_207) | ~greater(Y_207, appear(an_organisation, '#skF_2')) | ~greater(Y_209, Y_207) | ~greater(Y_209, '#skF_3') | ~greater('#skF_3', Y_209)))).
% 15.61/5.29 tff(c_2057, plain, (![E_222]: (~greater(start_time(E_222), '#skF_3') | appear(first_movers, E_222)=start_time(E_222) | ~environment(E_222)))).
% 15.61/5.29 tff(c_1799, plain, (![Y_207, Y_169, Y_209]: (in_environment('#skF_2', Y_207) | ~greater(Y_207, Y_169) | ~greater(Y_209, Y_207) | ~greater(Y_209, '#skF_3') | ~greater('#skF_3', Y_209) | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.29 tff(c_1927, plain, (![Y_217]: (~greater(Y_217, appear(efficient_producers, e)) | ~greater(Y_217, '#skF_3') | ~greater('#skF_3', Y_217)))).
% 15.61/5.29 tff(c_1801, plain, (![Y_207, Y_209]: (in_environment('#skF_2', Y_207) | ~greater(Y_207, start_time('#skF_2')) | ~greater(Y_209, Y_207) | ~greater(Y_209, '#skF_3') | ~greater('#skF_3', Y_209)))).
% 15.61/5.29 tff(c_264, plain, (![X_26, E_87, X_88]: (greater(X_26, zero) | ~greater(X_26, number_of_organizations(E_87, X_88)) | ~in_environment(E_87, X_88) | ~environment(E_87) | ~greater(X_88, appear(an_organisation, E_87))))).
% 15.61/5.29 tff(c_1805, plain, (![Y_207, Y_209]: (in_environment('#skF_2', Y_207) | ~greater(Y_207, '#skF_3') | ~greater(Y_209, Y_207) | ~greater(Y_209, '#skF_3') | ~greater('#skF_3', Y_209)))).
% 15.61/5.29 tff(c_1813, plain, (cardinality_at_time(efficient_producers, start_time('#skF_2'))=zero)).
% 15.61/5.29 tff(c_1786, plain, (![X_205]: (cardinality_at_time(X_205, start_time('#skF_2'))=zero | ~greater(appear(X_205, '#skF_2'), '#skF_3')))).
% 15.61/5.29 tff(c_1169, plain, (![Y_30, Y_113, Y_171]: (in_environment('#skF_2', Y_30) | ~in_environment('#skF_2', Y_113) | ~greater(Y_30, Y_113) | ~greater(Y_171, Y_30) | ~greater(Y_171, '#skF_3') | ~greater('#skF_3', Y_171)))).
% 15.61/5.29 tff(c_397, plain, (![X_72, E_74]: (cardinality_at_time(X_72, start_time('#skF_2'))=zero | ~in_environment(E_74, start_time('#skF_2')) | ~environment(E_74) | ~greater(appear(X_72, E_74), '#skF_3')))).
% 15.61/5.29 tff(c_377, plain, (![X_51, E_33]: (greater(X_51, start_time(E_33)) | appear(first_movers, E_33)=start_time(E_33) | ~greater(X_51, appear(efficient_producers, e)) | ~environment(E_33)))).
% 15.61/5.29 tff(c_1711, plain, (![E_33]: (greater(appear(efficient_producers, e), appear(an_organisation, E_33)) | appear(first_movers, E_33)=appear(an_organisation, E_33) | ~environment(E_33)))).
% 15.61/5.29 tff(c_275, plain, (![X_26, E_89]: (greater(X_26, appear(an_organisation, E_89)) | ~greater(X_26, appear(first_movers, E_89)) | appear(first_movers, E_89)=appear(an_organisation, E_89) | ~environment(E_89)))).
% 15.61/5.29 tff(c_1680, plain, (![E_33]: (~greater(appear(first_movers, E_33), start_time('#skF_2')) | ~environment(E_33)))).
% 15.61/5.29 tff(c_1580, plain, (![E_19, Y_193]: (in_environment(E_19, Y_193) | ~greater(Y_193, start_time(E_19)) | ~greater(start_time(E_19), Y_193) | ~environment(E_19)))).
% 15.61/5.29 tff(c_1490, plain, (![Y_185, Y_169]: (in_environment('#skF_2', Y_185) | ~greater(Y_185, Y_169) | ~greater(appear(an_organisation, '#skF_2'), Y_185) | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.29 tff(c_1123, plain, (![E_19, Y_166, Y_168]: (in_environment(E_19, Y_166) | ~in_environment(E_19, Y_168) | ~greater(Y_166, Y_168) | ~greater(start_time(E_19), Y_166) | ~environment(E_19)))).
% 15.61/5.29 tff(c_1553, plain, (~greater(appear(an_organisation, '#skF_2'), appear(efficient_producers, '#skF_2')))).
% 15.61/5.29 tff(c_1491, plain, (![Y_185]: (in_environment('#skF_2', Y_185) | ~greater(Y_185, appear(an_organisation, '#skF_2')) | ~greater(appear(an_organisation, '#skF_2'), Y_185)))).
% 15.61/5.29 tff(c_249, plain, (![X_26, E_86]: (greater(X_26, zero) | ~greater(X_26, number_of_organizations(E_86, appear(an_organisation, E_86))) | ~in_environment(E_86, appear(an_organisation, E_86)) | ~environment(E_86)))).
% 15.61/5.29 tff(c_1492, plain, (![Y_185]: (in_environment('#skF_2', Y_185) | ~greater(Y_185, start_time('#skF_2')) | ~greater(appear(an_organisation, '#skF_2'), Y_185)))).
% 15.61/5.29 tff(c_1496, plain, (![Y_185]: (in_environment('#skF_2', Y_185) | ~greater(Y_185, '#skF_3') | ~greater(appear(an_organisation, '#skF_2'), Y_185)))).
% 15.61/5.29 tff(c_1119, plain, (![Y_166, Y_168]: (in_environment('#skF_2', Y_166) | ~in_environment('#skF_2', Y_168) | ~greater(Y_166, Y_168) | ~greater(appear(an_organisation, '#skF_2'), Y_166)))).
% 15.61/5.29 tff(c_1398, plain, (~greater(start_time('#skF_2'), appear(efficient_producers, '#skF_2')))).
% 15.61/5.29 tff(c_1325, plain, (![Y_176, Y_169]: (in_environment('#skF_2', Y_176) | ~greater(Y_176, Y_169) | ~greater(start_time('#skF_2'), Y_176) | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.29 tff(c_1326, plain, (![Y_176]: (in_environment('#skF_2', Y_176) | ~greater(Y_176, appear(an_organisation, '#skF_2')) | ~greater(start_time('#skF_2'), Y_176)))).
% 15.61/5.29 tff(c_1327, plain, (![Y_176]: (in_environment('#skF_2', Y_176) | ~greater(Y_176, start_time('#skF_2')) | ~greater(start_time('#skF_2'), Y_176)))).
% 15.61/5.29 tff(c_227, plain, (![X_26, E_82]: (greater(X_26, zero) | ~greater(X_26, number_of_organizations(E_82, appear(first_movers, E_82))) | ~in_environment(E_82, appear(first_movers, E_82)) | ~environment(E_82)))).
% 15.61/5.29 tff(c_1331, plain, (![Y_176]: (in_environment('#skF_2', Y_176) | ~greater(Y_176, '#skF_3') | ~greater(start_time('#skF_2'), Y_176)))).
% 15.61/5.29 tff(c_1122, plain, (![Y_166, Y_168]: (in_environment('#skF_2', Y_166) | ~in_environment('#skF_2', Y_168) | ~greater(Y_166, Y_168) | ~greater(start_time('#skF_2'), Y_166)))).
% 15.61/5.30 tff(c_1137, plain, (![Y_169]: (in_environment('#skF_2', Y_169) | ~greater(Y_169, appear(an_organisation, '#skF_2')) | ~greater('#skF_3', Y_169)))).
% 15.61/5.30 tff(c_1141, plain, (![Y_169]: (in_environment('#skF_2', Y_169) | ~greater(Y_169, start_time('#skF_2')) | ~greater('#skF_3', Y_169)))).
% 15.61/5.30 tff(c_1166, plain, (![Y_166, Y_171]: (in_environment('#skF_2', Y_166) | ~greater(Y_166, Y_171) | ~greater('#skF_3', Y_166) | ~greater(Y_171, '#skF_3') | ~greater('#skF_3', Y_171)))).
% 15.61/5.30 tff(c_1173, plain, (~greater('#skF_3', appear(efficient_producers, '#skF_2')))).
% 15.61/5.30 tff(c_1142, plain, (![Y_169]: (in_environment('#skF_2', Y_169) | ~greater(Y_169, '#skF_3') | ~greater('#skF_3', Y_169)))).
% 15.61/5.30 tff(c_1126, plain, (![Y_166, Y_168]: (in_environment('#skF_2', Y_166) | ~in_environment('#skF_2', Y_168) | ~greater(Y_166, Y_168) | ~greater('#skF_3', Y_166)))).
% 15.61/5.30 tff(c_505, plain, (![E_110, Y_30, X_29, Y_113]: (in_environment(E_110, Y_30) | ~in_environment(E_110, X_29) | ~in_environment(E_110, Y_113) | ~environment(E_110) | ~greater(Y_30, Y_113) | ~greater(X_29, Y_30)))).
% 15.61/5.30 tff(c_1107, plain, (~in_environment('#skF_2', appear(efficient_producers, e)))).
% 16.00/5.30 tff(c_1017, plain, (![X_51]: (cardinality_at_time('#skF_1'('#skF_2', X_51), t)!=zero | ~in_environment('#skF_2', X_51) | ~greater(X_51, '#skF_3')))).
% 16.00/5.30 tff(c_1100, plain, (~in_environment('#skF_2', appear(efficient_producers, '#skF_2')))).
% 16.00/5.30 tff(c_1086, plain, (greater(zero, zero))).
% 16.00/5.30 tff(c_991, plain, (![X_26]: (cardinality_at_time('#skF_1'('#skF_2', X_26), t)!=zero | ~in_environment('#skF_2', X_26) | ~greater(X_26, start_time('#skF_2'))))).
% 16.00/5.30 tff(c_972, plain, (~greater(zero, appear(efficient_producers, e)))).
% 16.00/5.30 tff(c_261, plain, (![E_87, X_88]: (cardinality_at_time('#skF_1'(E_87, X_88), t)!=zero | ~in_environment(E_87, X_88) | ~environment(E_87) | ~greater(X_88, appear(an_organisation, E_87))))).
% 16.00/5.30 tff(c_947, plain, (~greater(appear(an_organisation, '#skF_2'), appear(efficient_producers, e)))).
% 16.00/5.30 tff(c_940, plain, (subpopulation(efficient_producers, '#skF_2', start_time('#skF_2')))).
% 16.00/5.30 tff(c_921, plain, ('#skF_1'('#skF_2', start_time('#skF_2'))=efficient_producers)).
% 16.00/5.30 tff(c_392, plain, (![E_5, T_6, S2_107, E_109]: (selection_favors('#skF_1'(E_5, T_6), S2_107, T_6) | cardinality_at_time(S2_107, T_6)!=zero | ~subpopulation(S2_107, E_109, T_6) | ~subpopulation('#skF_1'(E_5, T_6), E_109, T_6) | ~environment(E_109) | ~greater(number_of_organizations(E_5, T_6), zero) | ~environment(E_5)))).
% 16.00/5.30 tff(c_842, plain, (![E_5, T_6]: ('#skF_1'(E_5, T_6)=first_movers | '#skF_1'(E_5, T_6)=efficient_producers | ~greater(number_of_organizations(E_5, T_6), zero) | ~environment(E_5)))).
% 16.00/5.30 tff(c_689, plain, (![E_19]: (in_environment(E_19, start_time('#skF_2')) | ~in_environment(E_19, '#skF_3') | ~greater(start_time('#skF_2'), start_time(E_19)) | ~environment(E_19)))).
% 16.00/5.30 tff(c_394, plain, (![E_19]: (in_environment(E_19, '#skF_3') | ~greater_or_equal(start_time(E_19), '#skF_3') | ~in_environment(E_19, start_time('#skF_2')) | ~environment(E_19)))).
% 16.00/5.30 tff(c_381, plain, (![E_33]: (greater(appear(efficient_producers, e), start_time(E_33)) | appear(first_movers, E_33)=start_time(E_33) | ~environment(E_33)))).
% 16.00/5.30 tff(c_843, plain, (~greater(zero, start_time('#skF_2')))).
% 16.00/5.30 tff(c_819, plain, (![X_26]: (greater(X_26, appear(an_organisation, '#skF_2')) | ~greater(X_26, appear(efficient_producers, '#skF_2'))))).
% 16.00/5.30 tff(c_832, plain, (~greater(start_time('#skF_2'), start_time('#skF_2')))).
% 16.00/5.30 tff(c_818, plain, (cardinality_at_time(efficient_producers, appear(an_organisation, '#skF_2'))=zero)).
% 16.00/5.30 tff(c_800, plain, (greater(appear(efficient_producers, '#skF_2'), appear(an_organisation, '#skF_2')))).
% 16.00/5.30 tff(c_672, plain, (![X_26, X_127]: (greater(X_26, appear(an_organisation, '#skF_2')) | ~greater(X_26, X_127) | ~greater(X_127, start_time('#skF_2'))))).
% 16.00/5.30 tff(c_327, plain, (![E_95, E_22, T2_98]: (in_environment(E_95, appear(first_movers, E_22)) | ~greater_or_equal(T2_98, appear(first_movers, E_22)) | ~in_environment(E_95, T2_98) | ~in_environment(E_95, appear(an_organisation, E_22)) | ~environment(E_95) | ~environment(E_22)))).
% 16.00/5.30 tff(c_714, plain, (cardinality_at_time(first_movers, appear(an_organisation, '#skF_2'))=zero)).
% 16.00/5.30 tff(c_452, plain, (![T_12]: (cardinality_at_time(first_movers, T_12)=zero | ~greater(start_time('#skF_2'), T_12) | ~in_environment('#skF_2', T_12)))).
% 16.00/5.30 tff(c_673, plain, (~greater(appear(an_organisation, '#skF_2'), '#skF_3'))).
% 16.00/5.30 tff(c_502, plain, (![E_110, Y_113]: (in_environment(E_110, start_time('#skF_2')) | ~in_environment(E_110, '#skF_3') | ~in_environment(E_110, Y_113) | ~environment(E_110) | ~greater(start_time('#skF_2'), Y_113)))).
% 16.00/5.30 tff(c_657, plain, (![X_26]: (greater(X_26, appear(an_organisation, '#skF_2')) | ~greater(X_26, start_time('#skF_2'))))).
% 16.00/5.30 tff(c_635, plain, (greater(start_time('#skF_2'), appear(an_organisation, '#skF_2')))).
% 16.00/5.30 tff(c_328, plain, (![E_95, E_20, T2_98]: (in_environment(E_95, appear(first_movers, E_20)) | ~greater_or_equal(T2_98, appear(first_movers, E_20)) | ~in_environment(E_95, T2_98) | ~in_environment(E_95, start_time(E_20)) | ~environment(E_95) | ~environment(E_20)))).
% 16.00/5.30 tff(c_631, plain, (![X_26]: (greater(X_26, zero) | ~greater(X_26, number_of_organizations('#skF_2', start_time('#skF_2')))))).
% 16.00/5.30 tff(c_610, plain, (greater(number_of_organizations('#skF_2', start_time('#skF_2')), zero))).
% 16.00/5.30 tff(c_398, plain, (![X_26, X_55]: (greater(X_26, start_time('#skF_2')) | ~greater(X_26, X_55) | ~greater(X_55, '#skF_3')))).
% 16.00/5.30 tff(c_155, plain, (![X_26, E_70, T_71]: (greater(X_26, zero) | ~greater(X_26, cardinality_at_time('#skF_1'(E_70, T_71), T_71)) | ~greater(number_of_organizations(E_70, T_71), zero) | ~environment(E_70)))).
% 16.00/5.30 tff(c_553, plain, (in_environment('#skF_2', appear(an_organisation, '#skF_2')))).
% 16.00/5.30 tff(c_554, plain, (in_environment('#skF_2', start_time('#skF_2')))).
% 16.00/5.30 tff(c_456, plain, (![X_51]: (greater(X_51, start_time('#skF_2')) | ~greater(X_51, appear(efficient_producers, e))))).
% 16.00/5.30 tff(c_395, plain, (![E_95, T2_98]: (in_environment(E_95, '#skF_3') | ~greater_or_equal(T2_98, '#skF_3') | ~in_environment(E_95, T2_98) | ~in_environment(E_95, start_time('#skF_2')) | ~environment(E_95)))).
% 16.00/5.30 tff(c_399, plain, (![X_51]: (greater(X_51, start_time('#skF_2')) | ~greater(X_51, '#skF_3')))).
% 16.00/5.30 tff(c_460, plain, (greater_or_equal(start_time('#skF_2'), appear(an_organisation, '#skF_2')))).
% 16.00/5.30 tff(c_329, plain, (![E_95, X_29, T2_98, Y_30]: (in_environment(E_95, X_29) | ~greater_or_equal(T2_98, X_29) | ~in_environment(E_95, T2_98) | ~in_environment(E_95, Y_30) | ~environment(E_95) | ~greater(X_29, Y_30)))).
% 16.00/5.30 tff(c_462, plain, (greater(appear(efficient_producers, e), start_time('#skF_2')))).
% 16.00/5.30 tff(c_396, plain, (~greater(start_time('#skF_2'), appear(efficient_producers, e)))).
% 16.00/5.30 tff(c_450, plain, (~greater(start_time('#skF_2'), '#skF_3'))).
% 16.00/5.30 tff(c_400, plain, (greater('#skF_3', start_time('#skF_2')))).
% 16.00/5.30 tff(c_401, plain, (greater_or_equal('#skF_3', start_time('#skF_2')))).
% 16.00/5.30 tff(c_393, plain, (appear(first_movers, '#skF_2')=start_time('#skF_2'))).
% 16.00/5.30 tff(c_2, plain, (![S1_2, S2_3, T_4, E_1]: (selection_favors(S1_2, S2_3, T_4) | cardinality_at_time(S2_3, T_4)!=zero | ~greater(cardinality_at_time(S1_2, T_4), zero) | ~subpopulation(S2_3, E_1, T_4) | ~subpopulation(S1_2, E_1, T_4) | ~environment(E_1)))).
% 16.00/5.30 tff(c_145, plain, (![X_26, E_69]: (greater(X_26, start_time(E_69)) | ~greater(X_26, appear(first_movers, E_69)) | appear(first_movers, E_69)=start_time(E_69) | ~environment(E_69)))).
% 16.00/5.30 tff(c_363, plain, (cardinality_at_time(first_movers, t)!=zero)).
% 16.00/5.31 tff(c_347, plain, (![E_19]: (cardinality_at_time(first_movers, start_time(E_19))=zero | appear(first_movers, E_19)=start_time(E_19) | ~environment(E_19)))).
% 16.00/5.31 tff(c_14, plain, (![E_15, T_18, T1_16, T2_17]: (in_environment(E_15, T_18) | ~greater_or_equal(T_18, T1_16) | ~greater_or_equal(T2_17, T_18) | ~in_environment(E_15, T2_17) | ~in_environment(E_15, T1_16) | ~environment(E_15)))).
% 16.00/5.31 tff(c_315, plain, (~greater('#skF_3', appear(efficient_producers, e)))).
% 16.00/5.31 tff(c_135, plain, (![X_26, E_64, X_63]: (greater(X_26, appear(first_movers, E_64)) | ~greater(X_26, X_63) | ~greater(X_63, appear(efficient_producers, e)) | ~environment(E_64)))).
% 16.00/5.31 tff(c_224, plain, (![E_82]: (cardinality_at_time('#skF_1'(E_82, appear(first_movers, E_82)), t)!=zero | ~in_environment(E_82, appear(first_movers, E_82)) | ~environment(E_82)))).
% 16.00/5.31 tff(c_246, plain, (![E_86]: (cardinality_at_time('#skF_1'(E_86, appear(an_organisation, E_86)), t)!=zero | ~in_environment(E_86, appear(an_organisation, E_86)) | ~environment(E_86)))).
% 16.00/5.31 tff(c_81, plain, (![E_45]: (appear(first_movers, E_45)=appear(an_organisation, E_45) | greater(appear(first_movers, E_45), appear(an_organisation, E_45)) | ~environment(E_45)))).
% 16.00/5.31 tff(c_211, plain, (![E_80, X_29]: (greater(number_of_organizations(E_80, X_29), zero) | ~in_environment(E_80, X_29) | ~environment(E_80) | ~greater(X_29, appear(an_organisation, E_80))))).
% 16.00/5.31 tff(c_212, plain, (![E_80]: (greater(number_of_organizations(E_80, appear(an_organisation, E_80)), zero) | ~in_environment(E_80, appear(an_organisation, E_80)) | ~environment(E_80)))).
% 16.00/5.31 tff(c_42, plain, (![X_35, T_36, E_34]: (first_movers=X_35 | efficient_producers=X_35 | ~greater(cardinality_at_time(X_35, T_36), zero) | ~subpopulation(X_35, E_34, T_36) | ~environment(E_34)))).
% 16.00/5.31 tff(c_210, plain, (![E_22]: (greater(number_of_organizations(E_22, appear(first_movers, E_22)), zero) | ~in_environment(E_22, appear(first_movers, E_22)) | ~environment(E_22)))).
% 16.00/5.31 tff(c_38, plain, (![E_31, T_32]: (greater(number_of_organizations(E_31, T_32), zero) | ~greater_or_equal(T_32, appear(an_organisation, E_31)) | ~in_environment(E_31, T_32) | ~environment(E_31)))).
% 16.00/5.31 tff(c_196, plain, (![E_33]: (~greater(appear(first_movers, E_33), '#skF_3') | ~environment(E_33)))).
% 16.00/5.31 tff(c_156, plain, (![E_70, T_71]: (cardinality_at_time('#skF_1'(E_70, T_71), t)!=zero | ~greater(number_of_organizations(E_70, T_71), zero) | ~environment(E_70)))).
% 16.00/5.31 tff(c_189, plain, (cardinality_at_time(efficient_producers, t)!=zero)).
% 16.00/5.31 tff(c_181, plain, (cardinality_at_time(efficient_producers, '#skF_3')=zero)).
% 16.00/5.31 tff(c_10, plain, (![X_11, T_12, E_10]: (cardinality_at_time(X_11, T_12)=zero | ~greater(appear(X_11, E_10), T_12) | ~in_environment(E_10, T_12) | ~environment(E_10)))).
% 16.00/5.31 tff(c_4, plain, (![E_5, T_6]: (greater(cardinality_at_time('#skF_1'(E_5, T_6), T_6), zero) | ~greater(number_of_organizations(E_5, T_6), zero) | ~environment(E_5)))).
% 16.00/5.31 tff(c_75, plain, (![E_43]: (appear(first_movers, E_43)=start_time(E_43) | greater(appear(first_movers, E_43), start_time(E_43)) | ~environment(E_43)))).
% 16.00/5.31 tff(c_6, plain, (![E_5, T_6]: (subpopulation('#skF_1'(E_5, T_6), E_5, T_6) | ~greater(number_of_organizations(E_5, T_6), zero) | ~environment(E_5)))).
% 16.00/5.31 tff(c_94, plain, (![X_51, E_23]: (greater(X_51, zero) | ~greater(X_51, number_of_organizations(e, appear(an_organisation, E_23))) | ~environment(E_23)))).
% 16.00/5.31 tff(c_136, plain, (~greater(zero, '#skF_3'))).
% 16.00/5.31 tff(c_95, plain, (![X_51, E_33]: (greater(X_51, appear(first_movers, E_33)) | ~greater(X_51, appear(efficient_producers, e)) | ~environment(E_33)))).
% 16.00/5.31 tff(c_128, plain, (~greater('#skF_3', '#skF_3'))).
% 16.00/5.31 tff(c_20, plain, (![E_21]: (in_environment(E_21, appear(an_organisation, E_21)) | ~in_environment(E_21, appear(first_movers, E_21)) | ~environment(E_21)))).
% 16.00/5.31 tff(c_109, plain, (~environment(e))).
% 16.00/5.31 tff(c_12, plain, (![E_13, T_14]: (in_environment(E_13, T_14) | ~greater(number_of_organizations(E_13, T_14), zero) | ~environment(E_13)))).
% 16.00/5.31 tff(c_28, plain, (![E_24, T_25]: (subpopulation(first_movers, E_24, T_25) | ~in_environment(E_24, T_25) | ~environment(E_24)))).
% 16.00/5.31 tff(c_97, plain, (![X_51]: (greater(X_51, '#skF_3') | ~greater(X_51, appear(efficient_producers, '#skF_2'))))).
% 16.00/5.31 tff(c_30, plain, (![X_26, Z_28, Y_27]: (greater(X_26, Z_28) | ~greater(Y_27, Z_28) | ~greater(X_26, Y_27)))).
% 16.00/5.31 tff(c_8, plain, (![X_8, T_9]: (~greater(cardinality_at_time(X_8, T_9), zero) | cardinality_at_time(X_8, t)!=zero))).
% 16.00/5.31 tff(c_26, plain, (![E_24, T_25]: (subpopulation(efficient_producers, E_24, T_25) | ~in_environment(E_24, T_25) | ~environment(E_24)))).
% 16.00/5.31 tff(c_24, plain, (![E_23]: (greater(number_of_organizations(e, appear(an_organisation, E_23)), zero) | ~environment(E_23)))).
% 16.00/5.31 tff(c_22, plain, (![E_22]: (greater_or_equal(appear(first_movers, E_22), appear(an_organisation, E_22)) | ~environment(E_22)))).
% 16.00/5.31 tff(c_40, plain, (![E_33]: (greater(appear(efficient_producers, e), appear(first_movers, E_33)) | ~environment(E_33)))).
% 16.00/5.31 tff(c_18, plain, (![E_20]: (greater_or_equal(appear(first_movers, E_20), start_time(E_20)) | ~environment(E_20)))).
% 16.00/5.31 tff(c_32, plain, (![Y_30, X_29]: (Y_30=X_29 | greater(X_29, Y_30) | ~greater_or_equal(X_29, Y_30)))).
% 16.00/5.31 tff(c_36, plain, (![X_29, Y_30]: (~greater(X_29, Y_30) | greater_or_equal(X_29, Y_30)))).
% 16.00/5.31 tff(c_16, plain, (![E_19]: (in_environment(E_19, start_time(E_19)) | ~environment(E_19)))).
% 16.00/5.31 tff(c_46, plain, (greater(appear(efficient_producers, '#skF_2'), '#skF_3'))).
% 16.00/5.31 tff(c_44, plain, (~selection_favors(first_movers, efficient_producers, '#skF_3'))).
% 16.00/5.31 tff(c_34, plain, (![Y_30]: (greater_or_equal(Y_30, Y_30)))).
% 16.00/5.31 tff(c_50, plain, (in_environment('#skF_2', '#skF_3'))).
% 16.00/5.31 tff(c_52, plain, (environment('#skF_2'))).
% 16.00/5.31 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.00/5.31
%------------------------------------------------------------------------------