%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MGT033-2 : TPTP v9.3.0. Released v2.4.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 : n010.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 : Satisfiable 13.12s 4.93s % 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.4.0. % 0.00/0.04 % 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.12/0.38 % Computer : n010.cluster.edu % 0.12/0.38 % Model : x86_64 x86_64 % 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.38 % Memory : 8046.5625MB % 0.12/0.38 % OS : Linux 6.8.0-71-generic % 0.12/0.38 % CPULimit : 300 % 0.12/0.38 % WCLimit : 300 % 0.12/0.38 % DateTime : Mon Sep 7 12:28:10 UTC 2026 % 0.12/0.38 % CPUTime : % 13.12/4.93 % 13.12/4.93 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.12/4.93 % 13.12/4.93 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.12/4.94 %$ subpopulation > selection_favors > in_environment > greater_or_equal > greater > environment > sk1 > number_of_organizations > cardinality_at_time > appear > #nlpp > start_time > zero > t > sk3 > sk2 > first_movers > efficient_producers > e > an_organisation % 13.12/4.94 % 13.12/4.94 %Foreground sorts: % 13.12/4.94 % 13.12/4.94 % 13.12/4.94 %Background operators: % 13.12/4.94 % 13.12/4.94 % 13.12/4.94 %Foreground operators: % 13.12/4.94 tff(greater, type, greater: ($i * $i) > $o). % 13.12/4.94 tff(number_of_organizations, type, number_of_organizations: ($i * $i) > $i). % 13.12/4.94 tff(in_environment, type, in_environment: ($i * $i) > $o). % 13.12/4.94 tff(t, type, t: $i). % 13.12/4.94 tff(sk2, type, sk2: $i). % 13.12/4.94 tff(appear, type, appear: ($i * $i) > $i). % 13.12/4.94 tff(efficient_producers, type, efficient_producers: $i). % 13.12/4.94 tff(cardinality_at_time, type, cardinality_at_time: ($i * $i) > $i). % 13.12/4.94 tff(environment, type, environment: $i > $o). % 13.12/4.94 tff(start_time, type, start_time: $i > $i). % 13.12/4.94 tff(first_movers, type, first_movers: $i). % 13.12/4.94 tff(sk3, type, sk3: $i). % 13.12/4.94 tff(an_organisation, type, an_organisation: $i). % 13.12/4.94 tff(greater_or_equal, type, greater_or_equal: ($i * $i) > $o). % 13.12/4.94 tff(e, type, e: $i). % 13.12/4.94 tff(subpopulation, type, subpopulation: ($i * $i * $i) > $o). % 13.12/4.94 tff(selection_favors, type, selection_favors: ($i * $i * $i) > $o). % 13.12/4.94 tff(sk1, type, sk1: ($i * $i) > $i). % 13.12/4.94 tff(zero, type, zero: $i). % 13.12/4.94 % 13.12/4.94 %Saturated clause set: % 13.12/4.94 tff(c_5667, plain, (![B_495, A_333, A_497]: (in_environment(sk2, B_495) | ~greater(B_495, start_time(A_333)) | ~greater(start_time(A_497), B_495) | ~environment(A_497) | ~greater(sk3, appear(first_movers, A_497)) | ~greater(start_time(A_497), sk3) | ~greater(appear(an_organisation, A_497), sk3) | ~greater(sk3, appear(an_organisation, A_497)) | ~environment(A_333) | ~greater(sk3, appear(first_movers, A_333)) | ~greater(start_time(A_333), sk3) | ~greater(appear(an_organisation, A_333), sk3) | ~greater(sk3, appear(an_organisation, A_333))))). % 13.12/4.94 tff(c_5668, plain, (![B_495, A_352, A_497]: (in_environment(sk2, B_495) | ~greater(B_495, appear(an_organisation, A_352)) | ~greater(start_time(A_497), B_495) | ~environment(A_497) | ~greater(sk3, appear(first_movers, A_497)) | ~greater(start_time(A_497), sk3) | ~greater(appear(an_organisation, A_497), sk3) | ~greater(sk3, appear(an_organisation, A_497)) | ~in_environment(sk2, start_time(A_352)) | ~environment(A_352) | ~greater(sk3, appear(first_movers, A_352)) | ~greater(appear(an_organisation, A_352), sk3)))). % 13.12/4.94 tff(c_5280, plain, (![B_455, A_333, A_457]: (in_environment(sk2, B_455) | ~greater(B_455, start_time(A_333)) | ~greater(appear(an_organisation, A_457), B_455) | ~in_environment(sk2, start_time(A_457)) | ~environment(A_457) | ~greater(sk3, appear(first_movers, A_457)) | ~greater(appear(an_organisation, A_457), sk3) | ~environment(A_333) | ~greater(sk3, appear(first_movers, A_333)) | ~greater(start_time(A_333), sk3) | ~greater(appear(an_organisation, A_333), sk3) | ~greater(sk3, appear(an_organisation, A_333))))). % 13.12/4.94 tff(c_5756, plain, (![A_52, A_507]: (in_environment(sk2, appear(first_movers, A_52)) | ~greater(start_time(A_507), appear(first_movers, A_52)) | ~environment(A_507) | ~greater(sk3, appear(first_movers, A_507)) | ~greater(start_time(A_507), sk3) | ~greater(appear(an_organisation, A_507), sk3) | ~greater(sk3, appear(an_organisation, A_507)) | ~greater(appear(an_organisation, A_52), start_time(sk2)) | appear(first_movers, A_52)=appear(an_organisation, A_52) | ~environment(A_52)))). % 13.12/4.94 tff(c_5669, plain, (![B_495, A_259, A_497]: (in_environment(sk2, B_495) | ~greater(B_495, appear(first_movers, A_259)) | ~greater(start_time(A_497), B_495) | ~environment(A_497) | ~greater(sk3, appear(first_movers, A_497)) | ~greater(start_time(A_497), sk3) | ~greater(appear(an_organisation, A_497), sk3) | ~greater(sk3, appear(an_organisation, A_497)) | ~in_environment(sk2, appear(an_organisation, A_259)) | ~environment(A_259) | ~greater(sk3, appear(first_movers, A_259))))). % 13.12/4.94 tff(c_4439, plain, (![B_35, A_393, A_261]: (in_environment(sk2, B_35) | ~greater(B_35, start_time(A_393)) | ~greater(appear(first_movers, A_261), B_35) | ~in_environment(sk2, appear(an_organisation, A_261)) | ~environment(A_261) | ~greater(sk3, appear(first_movers, A_261)) | ~environment(A_393) | ~greater(sk3, appear(first_movers, A_393)) | ~greater(start_time(A_393), sk3) | ~greater(appear(an_organisation, A_393), sk3) | ~greater(sk3, appear(an_organisation, A_393))))). % 13.12/4.94 tff(c_5757, plain, (![A_50, A_507]: (in_environment(sk2, appear(first_movers, A_50)) | ~greater(start_time(A_507), appear(first_movers, A_50)) | ~environment(A_507) | ~greater(sk3, appear(first_movers, A_507)) | ~greater(start_time(A_507), sk3) | ~greater(appear(an_organisation, A_507), sk3) | ~greater(sk3, appear(an_organisation, A_507)) | ~greater(start_time(A_50), start_time(sk2)) | appear(first_movers, A_50)=start_time(A_50) | ~environment(A_50)))). % 13.12/4.94 tff(c_5281, plain, (![B_455, A_352, A_457]: (in_environment(sk2, B_455) | ~greater(B_455, appear(an_organisation, A_352)) | ~greater(appear(an_organisation, A_457), B_455) | ~in_environment(sk2, start_time(A_457)) | ~environment(A_457) | ~greater(sk3, appear(first_movers, A_457)) | ~greater(appear(an_organisation, A_457), sk3) | ~in_environment(sk2, start_time(A_352)) | ~environment(A_352) | ~greater(sk3, appear(first_movers, A_352)) | ~greater(appear(an_organisation, A_352), sk3)))). % 13.12/4.94 tff(c_6311, plain, (![A_56, A_562]: (in_environment(sk2, A_56) | ~greater(start_time(A_562), A_56) | ~environment(A_562) | ~greater(sk3, appear(first_movers, A_562)) | ~greater(start_time(A_562), sk3) | ~greater(appear(an_organisation, A_562), sk3) | ~greater(sk3, appear(an_organisation, A_562)) | ~greater(A_56, appear(efficient_producers, e))))). % 13.12/4.94 tff(c_5670, plain, (![B_495, A_232, A_497]: (in_environment(sk2, B_495) | ~greater(B_495, appear(first_movers, A_232)) | ~greater(start_time(A_497), B_495) | ~environment(A_497) | ~greater(sk3, appear(first_movers, A_497)) | ~greater(start_time(A_497), sk3) | ~greater(appear(an_organisation, A_497), sk3) | ~greater(sk3, appear(an_organisation, A_497)) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(sk3, appear(first_movers, A_232))))). % 13.12/4.94 tff(c_4440, plain, (![B_35, A_393, A_236]: (in_environment(sk2, B_35) | ~greater(B_35, start_time(A_393)) | ~greater(appear(first_movers, A_236), B_35) | ~in_environment(sk2, start_time(A_236)) | ~environment(A_236) | ~greater(sk3, appear(first_movers, A_236)) | ~environment(A_393) | ~greater(sk3, appear(first_movers, A_393)) | ~greater(start_time(A_393), sk3) | ~greater(appear(an_organisation, A_393), sk3) | ~greater(sk3, appear(an_organisation, A_393))))). % 13.12/4.94 tff(c_5374, plain, (![A_52, A_468]: (in_environment(sk2, appear(first_movers, A_52)) | ~greater(appear(an_organisation, A_468), appear(first_movers, A_52)) | ~in_environment(sk2, start_time(A_468)) | ~environment(A_468) | ~greater(sk3, appear(first_movers, A_468)) | ~greater(appear(an_organisation, A_468), sk3) | ~greater(appear(an_organisation, A_52), start_time(sk2)) | appear(first_movers, A_52)=appear(an_organisation, A_52) | ~environment(A_52)))). % 13.12/4.94 tff(c_5282, plain, (![B_455, A_259, A_457]: (in_environment(sk2, B_455) | ~greater(B_455, appear(first_movers, A_259)) | ~greater(appear(an_organisation, A_457), B_455) | ~in_environment(sk2, start_time(A_457)) | ~environment(A_457) | ~greater(sk3, appear(first_movers, A_457)) | ~greater(appear(an_organisation, A_457), sk3) | ~in_environment(sk2, appear(an_organisation, A_259)) | ~environment(A_259) | ~greater(sk3, appear(first_movers, A_259))))). % 13.12/4.94 tff(c_5375, plain, (![A_50, A_468]: (in_environment(sk2, appear(first_movers, A_50)) | ~greater(appear(an_organisation, A_468), appear(first_movers, A_50)) | ~in_environment(sk2, start_time(A_468)) | ~environment(A_468) | ~greater(sk3, appear(first_movers, A_468)) | ~greater(appear(an_organisation, A_468), sk3) | ~greater(start_time(A_50), start_time(sk2)) | appear(first_movers, A_50)=start_time(A_50) | ~environment(A_50)))). % 13.12/4.94 tff(c_6168, plain, (![A_56, A_543]: (in_environment(sk2, A_56) | ~greater(appear(an_organisation, A_543), A_56) | ~in_environment(sk2, start_time(A_543)) | ~environment(A_543) | ~greater(sk3, appear(first_movers, A_543)) | ~greater(appear(an_organisation, A_543), sk3) | ~greater(A_56, appear(efficient_producers, e))))). % 13.12/4.95 tff(c_4271, plain, (![B_380, A_352, A_382]: (in_environment(sk2, B_380) | ~greater(B_380, appear(an_organisation, A_352)) | ~greater(appear(first_movers, A_382), B_380) | ~in_environment(sk2, appear(an_organisation, A_382)) | ~environment(A_382) | ~greater(sk3, appear(first_movers, A_382)) | ~in_environment(sk2, start_time(A_352)) | ~environment(A_352) | ~greater(sk3, appear(first_movers, A_352)) | ~greater(appear(an_organisation, A_352), sk3)))). % 13.12/4.95 tff(c_5283, plain, (![B_455, A_232, A_457]: (in_environment(sk2, B_455) | ~greater(B_455, appear(first_movers, A_232)) | ~greater(appear(an_organisation, A_457), B_455) | ~in_environment(sk2, start_time(A_457)) | ~environment(A_457) | ~greater(sk3, appear(first_movers, A_457)) | ~greater(appear(an_organisation, A_457), sk3) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(sk3, appear(first_movers, A_232))))). % 13.12/4.95 tff(c_4446, plain, (![A_131, A_393]: (in_environment(sk2, appear(first_movers, A_131)) | ~in_environment(sk2, appear(an_organisation, A_131)) | ~environment(A_131) | ~greater(start_time(A_393), appear(first_movers, A_131)) | ~environment(A_393) | ~greater(sk3, appear(first_movers, A_393)) | ~greater(start_time(A_393), sk3) | ~greater(appear(an_organisation, A_393), sk3) | ~greater(sk3, appear(an_organisation, A_393))))). % 13.12/4.95 tff(c_4365, plain, (![A_52, A_389]: (in_environment(sk2, appear(first_movers, A_52)) | ~greater(appear(first_movers, A_389), appear(first_movers, A_52)) | ~in_environment(sk2, appear(an_organisation, A_389)) | ~environment(A_389) | ~greater(sk3, appear(first_movers, A_389)) | ~greater(appear(an_organisation, A_52), start_time(sk2)) | appear(first_movers, A_52)=appear(an_organisation, A_52) | ~environment(A_52)))). % 13.12/4.95 tff(c_4452, plain, (![A_126, A_393]: (in_environment(sk2, appear(first_movers, A_126)) | ~in_environment(sk2, start_time(A_126)) | ~environment(A_126) | ~greater(start_time(A_393), appear(first_movers, A_126)) | ~environment(A_393) | ~greater(sk3, appear(first_movers, A_393)) | ~greater(start_time(A_393), sk3) | ~greater(appear(an_organisation, A_393), sk3) | ~greater(sk3, appear(an_organisation, A_393))))). % 13.12/4.95 tff(c_5671, plain, (![B_495, B_165, A_497]: (in_environment(sk2, B_495) | ~greater(B_495, B_165) | ~greater(start_time(A_497), B_495) | ~environment(A_497) | ~greater(sk3, appear(first_movers, A_497)) | ~greater(start_time(A_497), sk3) | ~greater(appear(an_organisation, A_497), sk3) | ~greater(sk3, appear(an_organisation, A_497)) | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.95 tff(c_4222, plain, (![A_52, A_377]: (in_environment(sk2, appear(first_movers, A_52)) | ~greater(appear(first_movers, A_377), appear(first_movers, A_52)) | ~in_environment(sk2, start_time(A_377)) | ~environment(A_377) | ~greater(sk3, appear(first_movers, A_377)) | ~greater(appear(an_organisation, A_52), start_time(sk2)) | appear(first_movers, A_52)=appear(an_organisation, A_52) | ~environment(A_52)))). % 13.12/4.95 tff(c_4453, plain, (![B_35, A_393, B_167]: (in_environment(sk2, B_35) | ~greater(B_35, start_time(A_393)) | ~greater(B_167, B_35) | ~greater(B_167, sk3) | ~greater(sk3, B_167) | ~environment(A_393) | ~greater(sk3, appear(first_movers, A_393)) | ~greater(start_time(A_393), sk3) | ~greater(appear(an_organisation, A_393), sk3) | ~greater(sk3, appear(an_organisation, A_393))))). % 13.12/4.95 tff(c_4125, plain, (![B_366, A_352, A_368]: (in_environment(sk2, B_366) | ~greater(B_366, appear(an_organisation, A_352)) | ~greater(appear(first_movers, A_368), B_366) | ~in_environment(sk2, start_time(A_368)) | ~environment(A_368) | ~greater(sk3, appear(first_movers, A_368)) | ~in_environment(sk2, start_time(A_352)) | ~environment(A_352) | ~greater(sk3, appear(first_movers, A_352)) | ~greater(appear(an_organisation, A_352), sk3)))). % 13.12/4.95 tff(c_4272, plain, (![B_380, A_259, A_382]: (in_environment(sk2, B_380) | ~greater(B_380, appear(first_movers, A_259)) | ~greater(appear(first_movers, A_382), B_380) | ~in_environment(sk2, appear(an_organisation, A_382)) | ~environment(A_382) | ~greater(sk3, appear(first_movers, A_382)) | ~in_environment(sk2, appear(an_organisation, A_259)) | ~environment(A_259) | ~greater(sk3, appear(first_movers, A_259))))). % 13.12/4.95 tff(c_4366, plain, (![A_50, A_389]: (in_environment(sk2, appear(first_movers, A_50)) | ~greater(appear(first_movers, A_389), appear(first_movers, A_50)) | ~in_environment(sk2, appear(an_organisation, A_389)) | ~environment(A_389) | ~greater(sk3, appear(first_movers, A_389)) | ~greater(start_time(A_50), start_time(sk2)) | appear(first_movers, A_50)=start_time(A_50) | ~environment(A_50)))). % 13.12/4.95 tff(c_5874, plain, (![A_56, A_505]: (in_environment(sk2, A_56) | ~greater(appear(first_movers, A_505), A_56) | ~in_environment(sk2, appear(an_organisation, A_505)) | ~environment(A_505) | ~greater(sk3, appear(first_movers, A_505)) | ~greater(A_56, appear(efficient_producers, e))))). % 13.12/4.95 tff(c_4223, plain, (![A_50, A_377]: (in_environment(sk2, appear(first_movers, A_50)) | ~greater(appear(first_movers, A_377), appear(first_movers, A_50)) | ~in_environment(sk2, start_time(A_377)) | ~environment(A_377) | ~greater(sk3, appear(first_movers, A_377)) | ~greater(start_time(A_50), start_time(sk2)) | appear(first_movers, A_50)=start_time(A_50) | ~environment(A_50)))). % 13.12/4.95 tff(c_3984, plain, (![A_131, A_354]: (in_environment(sk2, appear(first_movers, A_131)) | ~in_environment(sk2, appear(an_organisation, A_131)) | ~environment(A_131) | ~greater(appear(an_organisation, A_354), appear(first_movers, A_131)) | ~in_environment(sk2, start_time(A_354)) | ~environment(A_354) | ~greater(sk3, appear(first_movers, A_354)) | ~greater(appear(an_organisation, A_354), sk3)))). % 13.12/4.95 tff(c_5795, plain, (![A_56, A_472]: (in_environment(sk2, A_56) | ~greater(appear(first_movers, A_472), A_56) | ~in_environment(sk2, start_time(A_472)) | ~environment(A_472) | ~greater(sk3, appear(first_movers, A_472)) | ~greater(A_56, appear(efficient_producers, e))))). % 13.12/4.95 tff(c_5766, plain, (![A_507]: (~greater(start_time(A_507), appear(efficient_producers, sk2)) | ~environment(A_507) | ~greater(sk3, appear(first_movers, A_507)) | ~greater(start_time(A_507), sk3) | ~greater(appear(an_organisation, A_507), sk3) | ~greater(sk3, appear(an_organisation, A_507))))). % 13.12/4.95 tff(c_5672, plain, (![B_495, A_497]: (in_environment(sk2, B_495) | ~greater(B_495, appear(an_organisation, sk2)) | ~greater(start_time(A_497), B_495) | ~environment(A_497) | ~greater(sk3, appear(first_movers, A_497)) | ~greater(start_time(A_497), sk3) | ~greater(appear(an_organisation, A_497), sk3) | ~greater(sk3, appear(an_organisation, A_497))))). % 13.12/4.95 tff(c_4273, plain, (![B_380, A_232, A_382]: (in_environment(sk2, B_380) | ~greater(B_380, appear(first_movers, A_232)) | ~greater(appear(first_movers, A_382), B_380) | ~in_environment(sk2, appear(an_organisation, A_382)) | ~environment(A_382) | ~greater(sk3, appear(first_movers, A_382)) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(sk3, appear(first_movers, A_232))))). % 13.12/4.95 tff(c_5718, plain, (![A_501]: (~greater(start_time(A_501), appear(efficient_producers, e)) | ~environment(A_501) | ~greater(sk3, appear(first_movers, A_501)) | ~greater(start_time(A_501), sk3) | ~greater(appear(an_organisation, A_501), sk3) | ~greater(sk3, appear(an_organisation, A_501))))). % 13.12/4.95 tff(c_5673, plain, (![B_495, A_497]: (in_environment(sk2, B_495) | ~greater(B_495, start_time(sk2)) | ~greater(start_time(A_497), B_495) | ~environment(A_497) | ~greater(sk3, appear(first_movers, A_497)) | ~greater(start_time(A_497), sk3) | ~greater(appear(an_organisation, A_497), sk3) | ~greater(sk3, appear(an_organisation, A_497))))). % 13.12/4.95 tff(c_5677, plain, (![B_495, A_497]: (in_environment(sk2, B_495) | ~greater(B_495, sk3) | ~greater(start_time(A_497), B_495) | ~environment(A_497) | ~greater(sk3, appear(first_movers, A_497)) | ~greater(start_time(A_497), sk3) | ~greater(appear(an_organisation, A_497), sk3) | ~greater(sk3, appear(an_organisation, A_497))))). % 13.12/4.95 tff(c_4469, plain, (![B_35, B_116, A_393]: (in_environment(sk2, B_35) | ~in_environment(sk2, B_116) | ~greater(B_35, B_116) | ~greater(start_time(A_393), B_35) | ~environment(A_393) | ~greater(sk3, appear(first_movers, A_393)) | ~greater(start_time(A_393), sk3) | ~greater(appear(an_organisation, A_393), sk3) | ~greater(sk3, appear(an_organisation, A_393))))). % 13.12/4.95 tff(c_3993, plain, (![A_126, A_354]: (in_environment(sk2, appear(first_movers, A_126)) | ~in_environment(sk2, start_time(A_126)) | ~environment(A_126) | ~greater(appear(an_organisation, A_354), appear(first_movers, A_126)) | ~in_environment(sk2, start_time(A_354)) | ~environment(A_354) | ~greater(sk3, appear(first_movers, A_354)) | ~greater(appear(an_organisation, A_354), sk3)))). % 13.12/4.95 tff(c_5284, plain, (![B_455, B_165, A_457]: (in_environment(sk2, B_455) | ~greater(B_455, B_165) | ~greater(appear(an_organisation, A_457), B_455) | ~in_environment(sk2, start_time(A_457)) | ~environment(A_457) | ~greater(sk3, appear(first_movers, A_457)) | ~greater(appear(an_organisation, A_457), sk3) | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.95 tff(c_4458, plain, (![B_162, A_393]: (in_environment(sk2, B_162) | ~greater(B_162, start_time(A_393)) | ~greater(appear(an_organisation, sk2), B_162) | ~environment(A_393) | ~greater(sk3, appear(first_movers, A_393)) | ~greater(start_time(A_393), sk3) | ~greater(appear(an_organisation, A_393), sk3) | ~greater(sk3, appear(an_organisation, A_393))))). % 13.12/4.95 tff(c_3994, plain, (![B_35, A_354, B_167]: (in_environment(sk2, B_35) | ~greater(B_35, appear(an_organisation, A_354)) | ~greater(B_167, B_35) | ~greater(B_167, sk3) | ~greater(sk3, B_167) | ~in_environment(sk2, start_time(A_354)) | ~environment(A_354) | ~greater(sk3, appear(first_movers, A_354)) | ~greater(appear(an_organisation, A_354), sk3)))). % 13.12/4.95 tff(c_4126, plain, (![B_366, A_259, A_368]: (in_environment(sk2, B_366) | ~greater(B_366, appear(first_movers, A_259)) | ~greater(appear(first_movers, A_368), B_366) | ~in_environment(sk2, start_time(A_368)) | ~environment(A_368) | ~greater(sk3, appear(first_movers, A_368)) | ~in_environment(sk2, appear(an_organisation, A_259)) | ~environment(A_259) | ~greater(sk3, appear(first_movers, A_259))))). % 13.12/4.95 tff(c_4459, plain, (![B_162, A_393]: (in_environment(sk2, B_162) | ~greater(B_162, start_time(A_393)) | ~greater(start_time(sk2), B_162) | ~environment(A_393) | ~greater(sk3, appear(first_movers, A_393)) | ~greater(start_time(A_393), sk3) | ~greater(appear(an_organisation, A_393), sk3) | ~greater(sk3, appear(an_organisation, A_393))))). % 13.12/4.95 tff(c_4454, plain, (![A_393]: (sk1(start_time(A_393), sk2)=first_movers | sk1(start_time(A_393), sk2)=efficient_producers | ~environment(A_393) | ~greater(sk3, appear(first_movers, A_393)) | ~greater(start_time(A_393), sk3) | ~greater(appear(an_organisation, A_393), sk3) | ~greater(sk3, appear(an_organisation, A_393))))). % 13.12/4.95 tff(c_3505, plain, (![A_318]: (sk1(appear(first_movers, A_318), sk2)=first_movers | sk1(appear(first_movers, A_318), sk2)=efficient_producers | ~in_environment(sk2, appear(first_movers, A_318)) | ~greater(appear(an_organisation, A_318), start_time(sk2)) | appear(first_movers, A_318)=appear(an_organisation, A_318) | ~environment(A_318)))). % 13.12/4.95 tff(c_4466, plain, (![B_162, A_393]: (in_environment(sk2, B_162) | ~greater(B_162, start_time(A_393)) | ~greater(sk3, B_162) | ~environment(A_393) | ~greater(sk3, appear(first_movers, A_393)) | ~greater(start_time(A_393), sk3) | ~greater(appear(an_organisation, A_393), sk3) | ~greater(sk3, appear(an_organisation, A_393))))). % 13.12/4.95 tff(c_4916, plain, (![A_420]: (sk1(appear(an_organisation, A_420), sk2)=first_movers | sk1(appear(an_organisation, A_420), sk2)=efficient_producers | ~environment(A_420) | ~greater(sk3, appear(first_movers, A_420)) | ~greater(appear(an_organisation, A_420), sk3) | ~greater(start_time(A_420), sk3) | ~greater(sk3, start_time(A_420))))). % 13.12/4.96 tff(c_3500, plain, (![A_318, B_230]: (in_environment(sk2, appear(first_movers, A_318)) | ~greater(B_230, appear(first_movers, A_318)) | ~greater(B_230, sk3) | ~greater(sk3, B_230) | ~greater(appear(an_organisation, A_318), start_time(sk2)) | appear(first_movers, A_318)=appear(an_organisation, A_318) | ~environment(A_318)))). % 13.12/4.96 tff(c_4127, plain, (![B_366, A_232, A_368]: (in_environment(sk2, B_366) | ~greater(B_366, appear(first_movers, A_232)) | ~greater(appear(first_movers, A_368), B_366) | ~in_environment(sk2, start_time(A_368)) | ~environment(A_368) | ~greater(sk3, appear(first_movers, A_368)) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(sk3, appear(first_movers, A_232))))). % 13.12/4.96 tff(c_5384, plain, (![A_468]: (~greater(appear(an_organisation, A_468), appear(efficient_producers, sk2)) | ~in_environment(sk2, start_time(A_468)) | ~environment(A_468) | ~greater(sk3, appear(first_movers, A_468)) | ~greater(appear(an_organisation, A_468), sk3)))). % 13.12/4.96 tff(c_5285, plain, (![B_455, A_457]: (in_environment(sk2, B_455) | ~greater(B_455, appear(an_organisation, sk2)) | ~greater(appear(an_organisation, A_457), B_455) | ~in_environment(sk2, start_time(A_457)) | ~environment(A_457) | ~greater(sk3, appear(first_movers, A_457)) | ~greater(appear(an_organisation, A_457), sk3)))). % 13.12/4.96 tff(c_5052, plain, (![A_427, A_5]: (selection_favors(first_movers, sk1(start_time(A_427), A_5), start_time(A_427)) | cardinality_at_time(sk1(start_time(A_427), A_5), start_time(A_427))!=zero | ~subpopulation(first_movers, A_5, start_time(A_427)) | appear(first_movers, A_427)=start_time(A_427) | ~environment(A_427) | ~greater(number_of_organizations(A_5, start_time(A_427)), zero) | ~environment(A_5)))). % 13.12/4.96 tff(c_5342, plain, (![A_463]: (~greater(appear(an_organisation, A_463), appear(efficient_producers, e)) | ~in_environment(sk2, start_time(A_463)) | ~environment(A_463) | ~greater(sk3, appear(first_movers, A_463)) | ~greater(appear(an_organisation, A_463), sk3)))). % 13.12/4.96 tff(c_5286, plain, (![B_455, A_457]: (in_environment(sk2, B_455) | ~greater(B_455, start_time(sk2)) | ~greater(appear(an_organisation, A_457), B_455) | ~in_environment(sk2, start_time(A_457)) | ~environment(A_457) | ~greater(sk3, appear(first_movers, A_457)) | ~greater(appear(an_organisation, A_457), sk3)))). % 13.12/4.96 tff(c_5290, plain, (![B_455, A_457]: (in_environment(sk2, B_455) | ~greater(B_455, sk3) | ~greater(appear(an_organisation, A_457), B_455) | ~in_environment(sk2, start_time(A_457)) | ~environment(A_457) | ~greater(sk3, appear(first_movers, A_457)) | ~greater(appear(an_organisation, A_457), sk3)))). % 13.12/4.96 tff(c_2496, plain, (![A_131, A_261]: (in_environment(sk2, appear(first_movers, A_131)) | ~in_environment(sk2, appear(an_organisation, A_131)) | ~environment(A_131) | ~greater(appear(first_movers, A_261), appear(first_movers, A_131)) | ~in_environment(sk2, appear(an_organisation, A_261)) | ~environment(A_261) | ~greater(sk3, appear(first_movers, A_261))))). % 13.12/4.96 tff(c_4013, plain, (![B_35, B_116, A_354]: (in_environment(sk2, B_35) | ~in_environment(sk2, B_116) | ~greater(B_35, B_116) | ~greater(appear(an_organisation, A_354), B_35) | ~in_environment(sk2, start_time(A_354)) | ~environment(A_354) | ~greater(sk3, appear(first_movers, A_354)) | ~greater(appear(an_organisation, A_354), sk3)))). % 13.12/4.96 tff(c_5258, plain, (![A_352]: (in_environment(sk2, appear(an_organisation, A_352)) | ~in_environment(sk2, start_time(A_352)) | ~environment(A_352) | ~greater(sk3, appear(first_movers, A_352)) | ~greater(appear(an_organisation, A_352), appear(efficient_producers, e))))). % 13.12/4.96 tff(c_4578, plain, (![A_7]: (selection_favors(sk1(appear(an_organisation, sk2), A_7), first_movers, appear(an_organisation, sk2)) | ~subpopulation(sk1(appear(an_organisation, sk2), A_7), sk2, appear(an_organisation, sk2)) | ~greater(number_of_organizations(A_7, appear(an_organisation, sk2)), zero) | ~environment(A_7)))). % 13.12/4.96 tff(c_4794, plain, (![A_5]: (selection_favors(efficient_producers, sk1(appear(an_organisation, sk2), A_5), appear(an_organisation, sk2)) | cardinality_at_time(sk1(appear(an_organisation, sk2), A_5), appear(an_organisation, sk2))!=zero | ~subpopulation(efficient_producers, A_5, appear(an_organisation, sk2)) | ~greater(number_of_organizations(A_5, appear(an_organisation, sk2)), zero) | ~environment(A_5)))). % 13.12/4.96 tff(c_2607, plain, (![A_7]: (selection_favors(sk1(appear(an_organisation, sk2), A_7), efficient_producers, appear(an_organisation, sk2)) | ~subpopulation(sk1(appear(an_organisation, sk2), A_7), sk2, appear(an_organisation, sk2)) | ~greater(number_of_organizations(A_7, appear(an_organisation, sk2)), zero) | ~environment(A_7)))). % 13.12/4.96 tff(c_3086, plain, (![A_295]: (sk1(appear(first_movers, A_295), sk2)=first_movers | sk1(appear(first_movers, A_295), sk2)=efficient_producers | ~in_environment(sk2, appear(first_movers, A_295)) | ~greater(start_time(A_295), start_time(sk2)) | appear(first_movers, A_295)=start_time(A_295) | ~environment(A_295)))). % 13.12/4.96 tff(c_2505, plain, (![A_126, A_261]: (in_environment(sk2, appear(first_movers, A_126)) | ~in_environment(sk2, start_time(A_126)) | ~environment(A_126) | ~greater(appear(first_movers, A_261), appear(first_movers, A_126)) | ~in_environment(sk2, appear(an_organisation, A_261)) | ~environment(A_261) | ~greater(sk3, appear(first_movers, A_261))))). % 13.12/4.96 tff(c_4005, plain, (![B_162, A_354]: (in_environment(sk2, B_162) | ~greater(B_162, appear(an_organisation, A_354)) | ~greater(appear(an_organisation, sk2), B_162) | ~in_environment(sk2, start_time(A_354)) | ~environment(A_354) | ~greater(sk3, appear(first_movers, A_354)) | ~greater(appear(an_organisation, A_354), sk3)))). % 13.12/4.96 tff(c_4552, plain, (![A_5]: (selection_favors(first_movers, sk1(appear(an_organisation, sk2), A_5), appear(an_organisation, sk2)) | cardinality_at_time(sk1(appear(an_organisation, sk2), A_5), appear(an_organisation, sk2))!=zero | ~subpopulation(first_movers, A_5, appear(an_organisation, sk2)) | ~greater(number_of_organizations(A_5, appear(an_organisation, sk2)), zero) | ~environment(A_5)))). % 13.12/4.96 tff(c_2506, plain, (![B_35, A_261, B_167]: (in_environment(sk2, B_35) | ~greater(B_35, appear(first_movers, A_261)) | ~greater(B_167, B_35) | ~greater(B_167, sk3) | ~greater(sk3, B_167) | ~in_environment(sk2, appear(an_organisation, A_261)) | ~environment(A_261) | ~greater(sk3, appear(first_movers, A_261))))). % 13.12/4.96 tff(c_5107, plain, (![A_20]: (selection_favors(first_movers, first_movers, start_time(A_20)) | cardinality_at_time(first_movers, start_time(A_20))!=zero | appear(first_movers, A_20)=start_time(A_20) | ~environment(A_20)))). % 13.12/4.96 tff(c_2443, plain, (![A_259, A_232]: (in_environment(sk2, appear(first_movers, A_259)) | ~in_environment(sk2, appear(an_organisation, A_259)) | ~environment(A_259) | ~greater(appear(first_movers, A_232), appear(first_movers, A_259)) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(sk3, appear(first_movers, A_232))))). % 13.12/4.96 tff(c_5080, plain, (![A_20]: (selection_favors(first_movers, efficient_producers, start_time(A_20)) | cardinality_at_time(efficient_producers, start_time(A_20))!=zero | appear(first_movers, A_20)=start_time(A_20) | ~environment(A_20)))). % 13.12/4.96 tff(c_5036, plain, (![D_4, A_151, A_1]: (selection_favors(first_movers, D_4, start_time(A_151)) | cardinality_at_time(D_4, start_time(A_151))!=zero | ~subpopulation(D_4, A_1, start_time(A_151)) | ~subpopulation(first_movers, A_1, start_time(A_151)) | ~environment(A_1) | appear(first_movers, A_151)=start_time(A_151) | ~environment(A_151)))). % 13.12/4.96 tff(c_5033, plain, (![A_330]: (in_environment(sk2, start_time(A_330)) | ~in_environment(sk2, appear(an_organisation, A_330)) | ~environment(A_330) | ~greater(sk3, appear(first_movers, A_330)) | ~greater(start_time(A_330), appear(efficient_producers, e))))). % 13.12/4.96 tff(c_4274, plain, (![B_380, B_165, A_382]: (in_environment(sk2, B_380) | ~greater(B_380, B_165) | ~greater(appear(first_movers, A_382), B_380) | ~in_environment(sk2, appear(an_organisation, A_382)) | ~environment(A_382) | ~greater(sk3, appear(first_movers, A_382)) | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.96 tff(c_3998, plain, (![A_354]: (sk1(appear(an_organisation, A_354), sk2)=first_movers | sk1(appear(an_organisation, A_354), sk2)=efficient_producers | ~in_environment(sk2, start_time(A_354)) | ~environment(A_354) | ~greater(sk3, appear(first_movers, A_354)) | ~greater(appear(an_organisation, A_354), sk3)))). % 13.12/4.96 tff(c_3081, plain, (![A_295, B_230]: (in_environment(sk2, appear(first_movers, A_295)) | ~greater(B_230, appear(first_movers, A_295)) | ~greater(B_230, sk3) | ~greater(sk3, B_230) | ~greater(start_time(A_295), start_time(sk2)) | appear(first_movers, A_295)=start_time(A_295) | ~environment(A_295)))). % 13.12/4.96 tff(c_4771, plain, (![A_56, B_408]: (in_environment(sk2, A_56) | ~greater(B_408, A_56) | ~greater(B_408, sk3) | ~greater(sk3, B_408) | ~greater(A_56, appear(efficient_producers, e))))). % 13.12/4.96 tff(c_4773, plain, (![D_4, A_1]: (selection_favors(efficient_producers, D_4, appear(an_organisation, sk2)) | cardinality_at_time(D_4, appear(an_organisation, sk2))!=zero | ~subpopulation(D_4, A_1, appear(an_organisation, sk2)) | ~subpopulation(efficient_producers, A_1, appear(an_organisation, sk2)) | ~environment(A_1)))). % 13.12/4.96 tff(c_2233, plain, (![A_126, A_236]: (in_environment(sk2, appear(first_movers, A_126)) | ~in_environment(sk2, start_time(A_126)) | ~environment(A_126) | ~greater(appear(first_movers, A_236), appear(first_movers, A_126)) | ~in_environment(sk2, start_time(A_236)) | ~environment(A_236) | ~greater(sk3, appear(first_movers, A_236))))). % 13.12/4.96 tff(c_4006, plain, (![B_162, A_354]: (in_environment(sk2, B_162) | ~greater(B_162, appear(an_organisation, A_354)) | ~greater(start_time(sk2), B_162) | ~in_environment(sk2, start_time(A_354)) | ~environment(A_354) | ~greater(sk3, appear(first_movers, A_354)) | ~greater(appear(an_organisation, A_354), sk3)))). % 13.12/4.96 tff(c_2234, plain, (![B_35, A_236, B_167]: (in_environment(sk2, B_35) | ~greater(B_35, appear(first_movers, A_236)) | ~greater(B_167, B_35) | ~greater(B_167, sk3) | ~greater(sk3, B_167) | ~in_environment(sk2, start_time(A_236)) | ~environment(A_236) | ~greater(sk3, appear(first_movers, A_236))))). % 13.12/4.96 tff(c_4128, plain, (![B_366, B_165, A_368]: (in_environment(sk2, B_366) | ~greater(B_366, B_165) | ~greater(appear(first_movers, A_368), B_366) | ~in_environment(sk2, start_time(A_368)) | ~environment(A_368) | ~greater(sk3, appear(first_movers, A_368)) | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.96 tff(c_3514, plain, (![A_318]: (cardinality_at_time(sk1(appear(first_movers, A_318), sk2), t)!=zero | ~in_environment(sk2, appear(first_movers, A_318)) | ~greater(appear(an_organisation, A_318), start_time(sk2)) | appear(first_movers, A_318)=appear(an_organisation, A_318) | ~environment(A_318)))). % 13.12/4.96 tff(c_3581, plain, (![A_5]: (selection_favors(efficient_producers, sk1(start_time(sk2), A_5), start_time(sk2)) | cardinality_at_time(sk1(start_time(sk2), A_5), start_time(sk2))!=zero | ~subpopulation(efficient_producers, A_5, start_time(sk2)) | ~greater(number_of_organizations(A_5, start_time(sk2)), zero) | ~environment(A_5)))). % 13.12/4.96 tff(c_4575, plain, (selection_favors(first_movers, first_movers, appear(an_organisation, sk2)))). % 13.12/4.96 tff(c_4567, plain, (selection_favors(first_movers, efficient_producers, appear(an_organisation, sk2)))). % 13.12/4.96 tff(c_4568, plain, (subpopulation(first_movers, sk2, appear(an_organisation, sk2)))). % 13.12/4.96 tff(c_4536, plain, (![D_4, A_1]: (selection_favors(first_movers, D_4, appear(an_organisation, sk2)) | cardinality_at_time(D_4, appear(an_organisation, sk2))!=zero | ~subpopulation(D_4, A_1, appear(an_organisation, sk2)) | ~subpopulation(first_movers, A_1, appear(an_organisation, sk2)) | ~environment(A_1)))). % 13.12/4.96 tff(c_4010, plain, (![B_162, A_354]: (in_environment(sk2, B_162) | ~greater(B_162, appear(an_organisation, A_354)) | ~greater(sk3, B_162) | ~in_environment(sk2, start_time(A_354)) | ~environment(A_354) | ~greater(sk3, appear(first_movers, A_354)) | ~greater(appear(an_organisation, A_354), sk3)))). % 13.12/4.96 tff(c_3509, plain, (![A_318]: (in_environment(sk2, appear(first_movers, A_318)) | ~greater(appear(an_organisation, sk2), appear(first_movers, A_318)) | ~greater(appear(an_organisation, A_318), start_time(sk2)) | appear(first_movers, A_318)=appear(an_organisation, A_318) | ~environment(A_318)))). % 13.12/4.96 tff(c_3510, plain, (![A_318]: (in_environment(sk2, appear(first_movers, A_318)) | ~greater(start_time(sk2), appear(first_movers, A_318)) | ~greater(appear(an_organisation, A_318), start_time(sk2)) | appear(first_movers, A_318)=appear(an_organisation, A_318) | ~environment(A_318)))). % 13.12/4.96 tff(c_3095, plain, (![A_295]: (cardinality_at_time(sk1(appear(first_movers, A_295), sk2), t)!=zero | ~in_environment(sk2, appear(first_movers, A_295)) | ~greater(start_time(A_295), start_time(sk2)) | appear(first_movers, A_295)=start_time(A_295) | ~environment(A_295)))). % 13.12/4.97 tff(c_3638, plain, (![A_333]: (in_environment(sk2, start_time(A_333)) | ~environment(A_333) | ~greater(sk3, appear(first_movers, A_333)) | ~greater(start_time(A_333), sk3) | ~greater(appear(an_organisation, A_333), sk3) | ~greater(sk3, appear(an_organisation, A_333))))). % 13.12/4.97 tff(c_2514, plain, (![B_162, A_261]: (in_environment(sk2, B_162) | ~greater(B_162, appear(first_movers, A_261)) | ~greater(appear(an_organisation, sk2), B_162) | ~in_environment(sk2, appear(an_organisation, A_261)) | ~environment(A_261) | ~greater(sk3, appear(first_movers, A_261))))). % 13.12/4.97 tff(c_4375, plain, (![A_389]: (~greater(appear(first_movers, A_389), appear(efficient_producers, sk2)) | ~in_environment(sk2, appear(an_organisation, A_389)) | ~environment(A_389) | ~greater(sk3, appear(first_movers, A_389))))). % 13.12/4.97 tff(c_4275, plain, (![B_380, A_382]: (in_environment(sk2, B_380) | ~greater(B_380, appear(an_organisation, sk2)) | ~greater(appear(first_movers, A_382), B_380) | ~in_environment(sk2, appear(an_organisation, A_382)) | ~environment(A_382) | ~greater(sk3, appear(first_movers, A_382))))). % 13.12/4.97 tff(c_4334, plain, (![A_386]: (~greater(appear(first_movers, A_386), appear(efficient_producers, e)) | ~in_environment(sk2, appear(an_organisation, A_386)) | ~environment(A_386) | ~greater(sk3, appear(first_movers, A_386))))). % 13.12/4.97 tff(c_4276, plain, (![B_380, A_382]: (in_environment(sk2, B_380) | ~greater(B_380, start_time(sk2)) | ~greater(appear(first_movers, A_382), B_380) | ~in_environment(sk2, appear(an_organisation, A_382)) | ~environment(A_382) | ~greater(sk3, appear(first_movers, A_382))))). % 13.12/4.97 tff(c_4280, plain, (![B_380, A_382]: (in_environment(sk2, B_380) | ~greater(B_380, sk3) | ~greater(appear(first_movers, A_382), B_380) | ~in_environment(sk2, appear(an_organisation, A_382)) | ~environment(A_382) | ~greater(sk3, appear(first_movers, A_382))))). % 13.12/4.97 tff(c_2522, plain, (![B_35, B_116, A_261]: (in_environment(sk2, B_35) | ~in_environment(sk2, B_116) | ~greater(B_35, B_116) | ~greater(appear(first_movers, A_261), B_35) | ~in_environment(sk2, appear(an_organisation, A_261)) | ~environment(A_261) | ~greater(sk3, appear(first_movers, A_261))))). % 13.12/4.97 tff(c_1844, plain, (![A_40]: (sk1(appear(efficient_producers, e), A_40)=first_movers | sk1(appear(efficient_producers, e), A_40)=efficient_producers | ~in_environment(A_40, appear(efficient_producers, e)) | appear(first_movers, A_40)=appear(an_organisation, A_40) | ~environment(A_40)))). % 13.12/4.97 tff(c_4232, plain, (![A_377]: (~greater(appear(first_movers, A_377), appear(efficient_producers, sk2)) | ~in_environment(sk2, start_time(A_377)) | ~environment(A_377) | ~greater(sk3, appear(first_movers, A_377))))). % 13.12/4.97 tff(c_4129, plain, (![B_366, A_368]: (in_environment(sk2, B_366) | ~greater(B_366, appear(an_organisation, sk2)) | ~greater(appear(first_movers, A_368), B_366) | ~in_environment(sk2, start_time(A_368)) | ~environment(A_368) | ~greater(sk3, appear(first_movers, A_368))))). % 13.12/4.97 tff(c_4188, plain, (![A_372]: (~greater(appear(first_movers, A_372), appear(efficient_producers, e)) | ~in_environment(sk2, start_time(A_372)) | ~environment(A_372) | ~greater(sk3, appear(first_movers, A_372))))). % 13.12/4.97 tff(c_2499, plain, (![C_77, A_261]: (cardinality_at_time(C_77, appear(first_movers, A_261))=zero | ~greater(appear(C_77, sk2), appear(efficient_producers, e)) | ~in_environment(sk2, appear(an_organisation, A_261)) | ~environment(A_261) | ~greater(sk3, appear(first_movers, A_261))))). % 13.12/4.97 tff(c_4130, plain, (![B_366, A_368]: (in_environment(sk2, B_366) | ~greater(B_366, start_time(sk2)) | ~greater(appear(first_movers, A_368), B_366) | ~in_environment(sk2, start_time(A_368)) | ~environment(A_368) | ~greater(sk3, appear(first_movers, A_368))))). % 13.12/4.97 tff(c_4134, plain, (![B_366, A_368]: (in_environment(sk2, B_366) | ~greater(B_366, sk3) | ~greater(appear(first_movers, A_368), B_366) | ~in_environment(sk2, start_time(A_368)) | ~environment(A_368) | ~greater(sk3, appear(first_movers, A_368))))). % 13.12/4.97 tff(c_2250, plain, (![B_35, B_116, A_236]: (in_environment(sk2, B_35) | ~in_environment(sk2, B_116) | ~greater(B_35, B_116) | ~greater(appear(first_movers, A_236), B_35) | ~in_environment(sk2, start_time(A_236)) | ~environment(A_236) | ~greater(sk3, appear(first_movers, A_236))))). % 13.12/4.97 tff(c_3511, plain, (![A_318]: (in_environment(sk2, appear(first_movers, A_318)) | ~greater(sk3, appear(first_movers, A_318)) | ~greater(appear(an_organisation, A_318), start_time(sk2)) | appear(first_movers, A_318)=appear(an_organisation, A_318) | ~environment(A_318)))). % 13.12/4.97 tff(c_3090, plain, (![A_295]: (in_environment(sk2, appear(first_movers, A_295)) | ~greater(appear(an_organisation, sk2), appear(first_movers, A_295)) | ~greater(start_time(A_295), start_time(sk2)) | appear(first_movers, A_295)=start_time(A_295) | ~environment(A_295)))). % 13.12/4.97 tff(c_4075, plain, (![A_56]: (in_environment(sk2, A_56) | ~greater(appear(an_organisation, sk2), A_56) | ~greater(A_56, appear(efficient_producers, e))))). % 13.12/4.97 tff(c_3233, plain, (![A_308]: (selection_favors(sk1(start_time(sk2), A_308), efficient_producers, start_time(sk2)) | ~subpopulation(sk1(start_time(sk2), A_308), sk2, start_time(sk2)) | ~greater(number_of_organizations(A_308, start_time(sk2)), zero) | ~environment(A_308)))). % 13.12/4.97 tff(c_2242, plain, (![B_162, A_236]: (in_environment(sk2, B_162) | ~greater(B_162, appear(first_movers, A_236)) | ~greater(appear(an_organisation, sk2), B_162) | ~in_environment(sk2, start_time(A_236)) | ~environment(A_236) | ~greater(sk3, appear(first_movers, A_236))))). % 13.12/4.97 tff(c_2355, plain, (![C_245, A_232]: (cardinality_at_time(C_245, appear(first_movers, A_232))=zero | ~greater(appear(C_245, sk2), appear(efficient_producers, e)) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(sk3, appear(first_movers, A_232))))). % 13.12/4.97 tff(c_3917, plain, (![A_352]: (in_environment(sk2, appear(an_organisation, A_352)) | ~in_environment(sk2, start_time(A_352)) | ~environment(A_352) | ~greater(sk3, appear(first_movers, A_352)) | ~greater(appear(an_organisation, A_352), start_time(sk2))))). % 13.12/4.97 tff(c_3920, plain, (![A_352]: (in_environment(sk2, appear(an_organisation, A_352)) | ~in_environment(sk2, start_time(A_352)) | ~environment(A_352) | ~greater(sk3, appear(first_movers, A_352)) | ~greater(appear(an_organisation, A_352), sk3)))). % 13.12/4.97 tff(c_2623, plain, (![A_232, B_266]: (in_environment(sk2, appear(an_organisation, A_232)) | ~in_environment(sk2, B_266) | ~greater(appear(an_organisation, A_232), B_266) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(sk3, appear(first_movers, A_232))))). % 13.12/4.97 tff(c_2518, plain, (![B_162, A_261]: (in_environment(sk2, B_162) | ~greater(B_162, appear(first_movers, A_261)) | ~greater(start_time(sk2), B_162) | ~in_environment(sk2, appear(an_organisation, A_261)) | ~environment(A_261) | ~greater(sk3, appear(first_movers, A_261))))). % 13.12/4.97 tff(c_3520, plain, (![A_29, A_318]: (greater(A_29, appear(an_organisation, sk2)) | ~greater(A_29, appear(first_movers, A_318)) | ~greater(appear(an_organisation, A_318), start_time(sk2)) | appear(first_movers, A_318)=appear(an_organisation, A_318) | ~environment(A_318)))). % 13.12/4.97 tff(c_3091, plain, (![A_295]: (in_environment(sk2, appear(first_movers, A_295)) | ~greater(start_time(sk2), appear(first_movers, A_295)) | ~greater(start_time(A_295), start_time(sk2)) | appear(first_movers, A_295)=start_time(A_295) | ~environment(A_295)))). % 13.12/4.97 tff(c_3852, plain, (![A_56]: (in_environment(sk2, A_56) | ~greater(start_time(sk2), A_56) | ~greater(A_56, appear(efficient_producers, e))))). % 13.12/4.97 tff(c_3823, plain, (![A_343]: (~greater(appear(an_organisation, A_343), appear(efficient_producers, e)) | appear(first_movers, A_343)=appear(an_organisation, A_343) | ~environment(A_343)))). % 13.12/4.97 tff(c_2446, plain, (![A_259, B_165]: (in_environment(sk2, appear(first_movers, A_259)) | ~in_environment(sk2, appear(an_organisation, A_259)) | ~environment(A_259) | ~greater(B_165, appear(first_movers, A_259)) | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.97 tff(c_2519, plain, (![B_162, A_261]: (in_environment(sk2, B_162) | ~greater(B_162, appear(first_movers, A_261)) | ~greater(sk3, B_162) | ~in_environment(sk2, appear(an_organisation, A_261)) | ~environment(A_261) | ~greater(sk3, appear(first_movers, A_261))))). % 13.12/4.97 tff(c_2246, plain, (![B_162, A_236]: (in_environment(sk2, B_162) | ~greater(B_162, appear(first_movers, A_236)) | ~greater(start_time(sk2), B_162) | ~in_environment(sk2, start_time(A_236)) | ~environment(A_236) | ~greater(sk3, appear(first_movers, A_236))))). % 13.12/4.97 tff(c_3617, plain, (![A_330]: (in_environment(sk2, start_time(A_330)) | ~in_environment(sk2, appear(an_organisation, A_330)) | ~environment(A_330) | ~greater(sk3, appear(first_movers, A_330)) | ~greater(start_time(A_330), start_time(sk2))))). % 13.12/4.97 tff(c_3623, plain, (![A_330]: (in_environment(sk2, start_time(A_330)) | ~in_environment(sk2, appear(an_organisation, A_330)) | ~environment(A_330) | ~greater(sk3, appear(first_movers, A_330)) | ~greater(start_time(A_330), sk3)))). % 13.12/4.97 tff(c_2043, plain, (![A_5]: (selection_favors(efficient_producers, sk1(sk3, A_5), sk3) | cardinality_at_time(sk1(sk3, A_5), sk3)!=zero | ~subpopulation(efficient_producers, A_5, sk3) | ~greater(number_of_organizations(A_5, sk3), zero) | ~environment(A_5)))). % 13.12/4.97 tff(c_2510, plain, (![A_261, B_116]: (in_environment(sk2, start_time(A_261)) | ~in_environment(sk2, B_116) | ~greater(start_time(A_261), B_116) | ~in_environment(sk2, appear(an_organisation, A_261)) | ~environment(A_261) | ~greater(sk3, appear(first_movers, A_261))))). % 13.12/4.97 tff(c_3092, plain, (![A_295]: (in_environment(sk2, appear(first_movers, A_295)) | ~greater(sk3, appear(first_movers, A_295)) | ~greater(start_time(A_295), start_time(sk2)) | appear(first_movers, A_295)=start_time(A_295) | ~environment(A_295)))). % 13.12/4.97 tff(c_3101, plain, (![A_29, A_295]: (greater(A_29, appear(an_organisation, sk2)) | ~greater(A_29, appear(first_movers, A_295)) | ~greater(start_time(A_295), start_time(sk2)) | appear(first_movers, A_295)=start_time(A_295) | ~environment(A_295)))). % 13.12/4.97 tff(c_913, plain, (![D_4, A_1]: (selection_favors(efficient_producers, D_4, start_time(sk2)) | cardinality_at_time(D_4, start_time(sk2))!=zero | ~subpopulation(D_4, A_1, start_time(sk2)) | ~subpopulation(efficient_producers, A_1, start_time(sk2)) | ~environment(A_1)))). % 13.12/4.97 tff(c_3563, plain, (![A_56]: (in_environment(sk2, A_56) | ~greater(sk3, A_56) | ~greater(A_56, appear(efficient_producers, e))))). % 13.12/4.97 tff(c_2115, plain, (![A_232, B_165]: (in_environment(sk2, appear(first_movers, A_232)) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(B_165, appear(first_movers, A_232)) | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.97 tff(c_2247, plain, (![B_162, A_236]: (in_environment(sk2, B_162) | ~greater(B_162, appear(first_movers, A_236)) | ~greater(sk3, B_162) | ~in_environment(sk2, start_time(A_236)) | ~environment(A_236) | ~greater(sk3, appear(first_movers, A_236))))). % 13.12/4.97 tff(c_726, plain, (![A_52]: (greater(appear(first_movers, A_52), appear(an_organisation, sk2)) | ~greater(appear(an_organisation, A_52), start_time(sk2)) | appear(first_movers, A_52)=appear(an_organisation, A_52) | ~environment(A_52)))). % 13.12/4.97 tff(c_3446, plain, (![A_316]: (~greater(start_time(A_316), appear(efficient_producers, e)) | appear(first_movers, A_316)=start_time(A_316) | ~environment(A_316)))). % 13.12/4.97 tff(c_2095, plain, (![B_228, B_165, B_230]: (in_environment(sk2, B_228) | ~greater(B_228, B_165) | ~greater(B_230, B_228) | ~greater(B_230, sk3) | ~greater(sk3, B_230) | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.97 tff(c_1480, plain, (![A_195]: (cardinality_at_time(sk1(appear(efficient_producers, e), A_195), t)!=zero | ~in_environment(A_195, appear(efficient_producers, e)) | appear(first_movers, A_195)=appear(an_organisation, A_195) | ~environment(A_195)))). % 13.12/4.97 tff(c_847, plain, (![B_6, A_144, A_5]: (selection_favors(sk1(B_6, A_144), sk1(B_6, A_5), B_6) | cardinality_at_time(sk1(B_6, A_5), B_6)!=zero | ~subpopulation(sk1(B_6, A_144), A_5, B_6) | ~greater(number_of_organizations(A_144, B_6), zero) | ~environment(A_144) | ~greater(number_of_organizations(A_5, B_6), zero) | ~environment(A_5)))). % 13.12/4.97 tff(c_2837, plain, (![A_283, A_40]: (in_environment(A_283, appear(first_movers, A_40)) | ~in_environment(A_283, appear(an_organisation, A_40)) | ~environment(A_283) | ~greater(start_time(A_283), appear(efficient_producers, e)) | ~environment(A_40)))). % 13.12/4.97 tff(c_2812, plain, (![B_6, A_5]: (selection_favors(sk1(B_6, A_5), efficient_producers, B_6) | cardinality_at_time(efficient_producers, B_6)!=zero | ~in_environment(A_5, B_6) | ~greater(number_of_organizations(A_5, B_6), zero) | ~environment(A_5)))). % 13.12/4.97 tff(c_3178, plain, (cardinality_at_time(first_movers, start_time(sk2))!=zero)). % 13.12/4.97 tff(c_2947, plain, (![B_6, A_5]: (selection_favors(sk1(B_6, A_5), first_movers, B_6) | cardinality_at_time(first_movers, B_6)!=zero | ~in_environment(A_5, B_6) | ~greater(number_of_organizations(A_5, B_6), zero) | ~environment(A_5)))). % 13.12/4.97 tff(c_1954, plain, (![A_7]: (selection_favors(sk1(sk3, A_7), efficient_producers, sk3) | ~subpopulation(sk1(sk3, A_7), sk2, sk3) | ~greater(number_of_organizations(A_7, sk3), zero) | ~environment(A_7)))). % 13.12/4.97 tff(c_3148, plain, (selection_favors(efficient_producers, efficient_producers, appear(an_organisation, sk2)))). % 13.12/4.97 tff(c_730, plain, (![A_50]: (greater(appear(first_movers, A_50), appear(an_organisation, sk2)) | ~greater(start_time(A_50), start_time(sk2)) | appear(first_movers, A_50)=start_time(A_50) | ~environment(A_50)))). % 13.12/4.97 tff(c_3042, plain, (selection_favors(efficient_producers, first_movers, appear(an_organisation, sk2)))). % 13.12/4.97 tff(c_3011, plain, (![A_29]: (greater(A_29, appear(an_organisation, sk2)) | ~greater(A_29, appear(efficient_producers, e))))). % 13.12/4.97 tff(c_2927, plain, (greater(appear(efficient_producers, e), appear(an_organisation, sk2)))). % 13.12/4.97 tff(c_849, plain, (![B_26, A_144, A_25]: (selection_favors(sk1(B_26, A_144), first_movers, B_26) | cardinality_at_time(first_movers, B_26)!=zero | ~subpopulation(sk1(B_26, A_144), A_25, B_26) | ~greater(number_of_organizations(A_144, B_26), zero) | ~environment(A_144) | ~in_environment(A_25, B_26) | ~environment(A_25)))). % 13.12/4.97 tff(c_2917, plain, (![A_286]: (~greater(appear(an_organisation, A_286), sk3) | appear(first_movers, A_286)=appear(an_organisation, A_286) | ~environment(A_286)))). % 13.12/4.97 tff(c_2449, plain, (![A_259]: (in_environment(sk2, appear(first_movers, A_259)) | ~in_environment(sk2, appear(an_organisation, A_259)) | ~environment(A_259) | ~greater(appear(an_organisation, sk2), appear(first_movers, A_259))))). % 13.12/4.97 tff(c_2453, plain, (![A_20, A_259]: (in_environment(A_20, appear(first_movers, A_259)) | ~in_environment(A_20, appear(an_organisation, A_259)) | ~environment(A_259) | ~greater(start_time(A_20), appear(first_movers, A_259)) | ~environment(A_20)))). % 13.12/4.97 tff(c_2826, plain, (selection_favors(efficient_producers, efficient_producers, start_time(sk2)))). % 13.12/4.97 tff(c_848, plain, (![B_28, A_144, A_27]: (selection_favors(sk1(B_28, A_144), efficient_producers, B_28) | cardinality_at_time(efficient_producers, B_28)!=zero | ~subpopulation(sk1(B_28, A_144), A_27, B_28) | ~greater(number_of_organizations(A_144, B_28), zero) | ~environment(A_144) | ~in_environment(A_27, B_28) | ~environment(A_27)))). % 13.12/4.97 tff(c_2781, plain, (![A_20]: (in_environment(A_20, appear(an_organisation, sk2)) | ~in_environment(A_20, start_time(sk2)) | ~greater(appear(an_organisation, sk2), start_time(A_20)) | ~environment(A_20)))). % 13.12/4.98 tff(c_2628, plain, (![A_264, B_266]: (in_environment(A_264, appear(an_organisation, sk2)) | ~in_environment(A_264, start_time(sk2)) | ~in_environment(A_264, B_266) | ~environment(A_264) | ~greater(appear(an_organisation, sk2), B_266)))). % 13.12/4.98 tff(c_2404, plain, (![A_253, A_40]: (in_environment(A_253, appear(first_movers, A_40)) | ~in_environment(A_253, start_time(A_40)) | ~environment(A_253) | ~greater(start_time(A_253), appear(efficient_producers, e)) | ~environment(A_40)))). % 13.12/4.98 tff(c_2739, plain, (![C_271]: (cardinality_at_time(C_271, appear(an_organisation, sk2))=zero | ~greater(appear(C_271, sk2), sk3)))). % 13.12/4.98 tff(c_2720, plain, (![C_269, A_270]: (cardinality_at_time(C_269, appear(an_organisation, sk2))=zero | ~in_environment(A_270, appear(an_organisation, sk2)) | ~environment(A_270) | ~greater(appear(C_269, A_270), sk3)))). % 13.12/4.98 tff(c_628, plain, (![C_13, A_11]: (cardinality_at_time(C_13, appear(an_organisation, sk2))=zero | ~in_environment(A_11, appear(an_organisation, sk2)) | ~environment(A_11) | ~greater(appear(C_13, A_11), start_time(sk2))))). % 13.12/4.98 tff(c_838, plain, (![A_23]: (sk1(appear(first_movers, A_23), A_23)=first_movers | sk1(appear(first_movers, A_23), A_23)=efficient_producers | ~in_environment(A_23, appear(first_movers, A_23)) | ~environment(A_23)))). % 13.12/4.98 tff(c_2670, plain, (![A_29]: (greater(A_29, zero) | ~greater(A_29, number_of_organizations(sk2, appear(an_organisation, sk2)))))). % 13.12/4.98 tff(c_2602, plain, (greater(number_of_organizations(sk2, appear(an_organisation, sk2)), zero))). % 13.12/4.98 tff(c_466, plain, (![A_113, A_23, B_116]: (in_environment(A_113, appear(an_organisation, A_23)) | ~in_environment(A_113, appear(first_movers, A_23)) | ~in_environment(A_113, B_116) | ~environment(A_113) | ~greater(appear(an_organisation, A_23), B_116) | ~environment(A_23)))). % 13.12/4.98 tff(c_2601, plain, (subpopulation(efficient_producers, sk2, appear(an_organisation, sk2)))). % 13.12/4.98 tff(c_2557, plain, (sk1(appear(an_organisation, sk2), sk2)=efficient_producers)). % 13.12/4.98 tff(c_837, plain, (![A_88]: (sk1(appear(an_organisation, A_88), A_88)=first_movers | sk1(appear(an_organisation, A_88), A_88)=efficient_producers | ~in_environment(A_88, appear(an_organisation, A_88)) | ~environment(A_88)))). % 13.12/4.98 tff(c_2452, plain, (![A_259]: (in_environment(sk2, appear(first_movers, A_259)) | ~in_environment(sk2, appear(an_organisation, A_259)) | ~environment(A_259) | ~greater(start_time(sk2), appear(first_movers, A_259))))). % 13.12/4.98 tff(c_2456, plain, (![A_259]: (in_environment(sk2, appear(first_movers, A_259)) | ~in_environment(sk2, appear(an_organisation, A_259)) | ~environment(A_259) | ~greater(sk3, appear(first_movers, A_259))))). % 13.12/4.98 tff(c_681, plain, (![A_130, A_131, A_34]: (in_environment(A_130, appear(first_movers, A_131)) | ~in_environment(A_130, A_34) | ~in_environment(A_130, appear(an_organisation, A_131)) | ~environment(A_130) | ~environment(A_131) | ~greater(A_34, appear(first_movers, A_131))))). % 13.12/4.98 tff(c_2118, plain, (![A_232]: (in_environment(sk2, appear(first_movers, A_232)) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(appear(an_organisation, sk2), appear(first_movers, A_232))))). % 13.12/4.98 tff(c_1274, plain, (![A_50]: (in_environment(A_50, appear(first_movers, A_50)) | ~greater(start_time(A_50), appear(first_movers, A_50)) | appear(first_movers, A_50)=start_time(A_50) | ~environment(A_50)))). % 13.12/4.98 tff(c_2122, plain, (![A_20, A_232]: (in_environment(A_20, appear(first_movers, A_232)) | ~in_environment(A_20, start_time(A_232)) | ~environment(A_232) | ~greater(start_time(A_20), appear(first_movers, A_232)) | ~environment(A_20)))). % 13.12/4.98 tff(c_2360, plain, (![C_245, A_247]: (cardinality_at_time(C_245, start_time(sk2))=zero | ~in_environment(A_247, start_time(sk2)) | ~environment(A_247) | ~greater(appear(C_245, A_247), appear(efficient_producers, e))))). % 13.12/4.98 tff(c_2380, plain, (![B_249]: (~greater(B_249, appear(efficient_producers, sk2)) | ~greater(B_249, sk3) | ~greater(sk3, B_249)))). % 13.12/4.98 tff(c_2096, plain, (![B_228, B_230]: (in_environment(sk2, B_228) | ~greater(B_228, appear(an_organisation, sk2)) | ~greater(B_230, B_228) | ~greater(B_230, sk3) | ~greater(sk3, B_230)))). % 13.12/4.98 tff(c_164, plain, (![C_77, A_40, A_79]: (cardinality_at_time(C_77, appear(first_movers, A_40))=zero | ~in_environment(A_79, appear(first_movers, A_40)) | ~environment(A_79) | ~greater(appear(C_77, A_79), appear(efficient_producers, e)) | ~environment(A_40)))). % 13.12/4.98 tff(c_2121, plain, (![A_232]: (in_environment(sk2, appear(first_movers, A_232)) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(start_time(sk2), appear(first_movers, A_232))))). % 13.12/4.98 tff(c_2319, plain, (![A_242]: (in_environment(A_242, start_time(sk2)) | ~in_environment(A_242, appear(an_organisation, sk2)) | ~environment(A_242) | ~greater(start_time(A_242), sk3)))). % 13.12/4.98 tff(c_2310, plain, (![A_20]: (in_environment(A_20, start_time(sk2)) | ~in_environment(A_20, appear(an_organisation, sk2)) | ~greater(start_time(A_20), start_time(sk2)) | ~environment(A_20)))). % 13.12/4.98 tff(c_2279, plain, (![B_238]: (~greater(B_238, appear(efficient_producers, e)) | ~greater(B_238, sk3) | ~greater(sk3, B_238)))). % 13.12/4.98 tff(c_2066, plain, (![A_224, A_34]: (in_environment(A_224, start_time(sk2)) | ~in_environment(A_224, A_34) | ~in_environment(A_224, appear(an_organisation, sk2)) | ~environment(A_224) | ~greater(A_34, start_time(sk2))))). % 13.12/4.98 tff(c_2100, plain, (![B_228, B_230]: (in_environment(sk2, B_228) | ~greater(B_228, start_time(sk2)) | ~greater(B_230, B_228) | ~greater(B_230, sk3) | ~greater(sk3, B_230)))). % 13.12/4.98 tff(c_2125, plain, (![A_232]: (in_environment(sk2, appear(first_movers, A_232)) | ~in_environment(sk2, start_time(A_232)) | ~environment(A_232) | ~greater(sk3, appear(first_movers, A_232))))). % 13.12/4.98 tff(c_2101, plain, (![B_228, B_230]: (in_environment(sk2, B_228) | ~greater(B_228, sk3) | ~greater(B_230, B_228) | ~greater(B_230, sk3) | ~greater(sk3, B_230)))). % 13.12/4.98 tff(c_601, plain, (![A_125, A_126, A_34]: (in_environment(A_125, appear(first_movers, A_126)) | ~in_environment(A_125, A_34) | ~in_environment(A_125, start_time(A_126)) | ~environment(A_125) | ~environment(A_126) | ~greater(A_34, appear(first_movers, A_126))))). % 13.12/4.98 tff(c_1093, plain, (![B_35, B_116, B_167]: (in_environment(sk2, B_35) | ~in_environment(sk2, B_116) | ~greater(B_35, B_116) | ~greater(B_167, B_35) | ~greater(B_167, sk3) | ~greater(sk3, B_167)))). % 13.12/4.98 tff(c_2062, plain, (![A_224]: (in_environment(A_224, start_time(sk2)) | ~in_environment(A_224, sk3) | ~in_environment(A_224, appear(an_organisation, sk2)) | ~environment(A_224)))). % 13.12/4.98 tff(c_2049, plain, (cardinality_at_time(first_movers, sk3)!=zero)). % 13.12/4.98 tff(c_491, plain, (![A_16, C_18]: (in_environment(A_16, start_time(sk2)) | ~greater_or_equal(C_18, start_time(sk2)) | ~in_environment(A_16, C_18) | ~in_environment(A_16, appear(an_organisation, sk2)) | ~environment(A_16)))). % 13.12/4.98 tff(c_2042, plain, (selection_favors(efficient_producers, efficient_producers, sk3))). % 13.12/4.98 tff(c_2027, plain, (![D_100, A_102]: (selection_favors(efficient_producers, D_100, sk3) | cardinality_at_time(D_100, sk3)!=zero | ~subpopulation(D_100, A_102, sk3) | ~subpopulation(efficient_producers, A_102, sk3) | ~environment(A_102)))). % 13.12/4.98 tff(c_2012, plain, (![B_165]: (sk1(B_165, sk2)=first_movers | sk1(B_165, sk2)=efficient_producers | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.98 tff(c_1876, plain, (![A_29]: (sk1(A_29, sk2)=first_movers | sk1(A_29, sk2)=efficient_producers | ~in_environment(sk2, A_29) | ~greater(A_29, sk3)))). % 13.12/4.98 tff(c_1993, plain, (![A_29]: (greater(A_29, zero) | ~greater(A_29, number_of_organizations(sk2, sk3))))). % 13.12/4.98 tff(c_1949, plain, (greater(number_of_organizations(sk2, sk3), zero))). % 13.12/4.98 tff(c_1948, plain, (subpopulation(efficient_producers, sk2, sk3))). % 13.12/4.98 tff(c_1884, plain, (sk1(sk3, sk2)=efficient_producers)). % 13.12/4.98 tff(c_1850, plain, (![A_29]: (sk1(A_29, sk2)=first_movers | sk1(A_29, sk2)=efficient_producers | ~in_environment(sk2, A_29) | ~greater(A_29, start_time(sk2))))). % 13.12/4.98 tff(c_836, plain, (![A_34, A_88]: (sk1(A_34, A_88)=first_movers | sk1(A_34, A_88)=efficient_producers | ~in_environment(A_88, A_34) | ~environment(A_88) | ~greater(A_34, appear(an_organisation, A_88))))). % 13.12/4.98 tff(c_1422, plain, (![A_56, A_40]: (greater(A_56, appear(an_organisation, A_40)) | appear(first_movers, A_40)=appear(an_organisation, A_40) | ~greater(A_56, appear(efficient_producers, e)) | ~environment(A_40)))). % 13.12/4.98 tff(c_1360, plain, (![B_188, B_165]: (in_environment(sk2, B_188) | ~greater(B_188, B_165) | ~greater(appear(an_organisation, sk2), B_188) | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.98 tff(c_1731, plain, (![A_204]: (~greater(start_time(A_204), sk3) | appear(first_movers, A_204)=start_time(A_204) | ~environment(A_204)))). % 13.12/4.98 tff(c_467, plain, (![A_113, A_21, B_116]: (in_environment(A_113, start_time(A_21)) | ~in_environment(A_113, appear(first_movers, A_21)) | ~in_environment(A_113, B_116) | ~environment(A_113) | ~greater(start_time(A_21), B_116) | ~environment(A_21)))). % 13.12/4.98 tff(c_1120, plain, (![B_169, B_165]: (in_environment(sk2, B_169) | ~greater(B_169, B_165) | ~greater(start_time(sk2), B_169) | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.98 tff(c_1596, plain, (![A_20]: (in_environment(A_20, start_time(sk2)) | ~in_environment(A_20, sk3) | ~greater(start_time(sk2), start_time(A_20)) | ~environment(A_20)))). % 13.12/4.98 tff(c_465, plain, (![A_113, B_116]: (in_environment(A_113, start_time(sk2)) | ~in_environment(A_113, sk3) | ~in_environment(A_113, B_116) | ~environment(A_113) | ~greater(start_time(sk2), B_116)))). % 13.12/4.98 tff(c_273, plain, (![A_96]: (cardinality_at_time(first_movers, appear(an_organisation, A_96))=zero | ~in_environment(A_96, appear(an_organisation, A_96)) | appear(first_movers, A_96)=appear(an_organisation, A_96) | ~environment(A_96)))). % 13.12/4.98 tff(c_1090, plain, (![B_162, B_167]: (in_environment(sk2, B_162) | ~greater(B_162, B_167) | ~greater(sk3, B_162) | ~greater(B_167, sk3) | ~greater(sk3, B_167)))). % 13.12/4.98 tff(c_1423, plain, (![A_40]: (greater(appear(efficient_producers, e), appear(an_organisation, A_40)) | appear(first_movers, A_40)=appear(an_organisation, A_40) | ~environment(A_40)))). % 13.12/4.98 tff(c_1436, plain, (~greater(appear(an_organisation, sk2), appear(efficient_producers, sk2)))). % 13.12/4.98 tff(c_1361, plain, (![B_188]: (in_environment(sk2, B_188) | ~greater(B_188, appear(an_organisation, sk2)) | ~greater(appear(an_organisation, sk2), B_188)))). % 13.12/4.98 tff(c_275, plain, (![A_29, A_96]: (greater(A_29, appear(an_organisation, A_96)) | ~greater(A_29, appear(first_movers, A_96)) | appear(first_movers, A_96)=appear(an_organisation, A_96) | ~environment(A_96)))). % 13.12/4.98 tff(c_1362, plain, (![B_188]: (in_environment(sk2, B_188) | ~greater(B_188, start_time(sk2)) | ~greater(appear(an_organisation, sk2), B_188)))). % 13.12/4.98 tff(c_1366, plain, (![B_188]: (in_environment(sk2, B_188) | ~greater(B_188, sk3) | ~greater(appear(an_organisation, sk2), B_188)))). % 13.12/4.98 tff(c_1045, plain, (![B_162, B_164]: (in_environment(sk2, B_162) | ~in_environment(sk2, B_164) | ~greater(B_162, B_164) | ~greater(appear(an_organisation, sk2), B_162)))). % 13.12/4.98 tff(c_290, plain, (![A_29, A_97, A_98]: (greater(A_29, zero) | ~greater(A_29, number_of_organizations(A_97, A_98)) | ~in_environment(A_97, A_98) | ~environment(A_97) | ~greater(A_98, appear(an_organisation, A_97))))). % 13.12/4.98 tff(c_1048, plain, (![B_162, B_164]: (in_environment(sk2, B_162) | ~in_environment(sk2, B_164) | ~greater(B_162, B_164) | ~greater(start_time(sk2), B_162)))). % 13.12/4.98 tff(c_1302, plain, (greater(zero, zero))). % 13.12/4.98 tff(c_1300, plain, (cardinality_at_time(efficient_producers, start_time(sk2))=zero)). % 13.12/4.98 tff(c_1289, plain, (![C_180]: (cardinality_at_time(C_180, start_time(sk2))=zero | ~greater(appear(C_180, sk2), sk3)))). % 13.12/4.98 tff(c_507, plain, (![C_13, A_11]: (cardinality_at_time(C_13, start_time(sk2))=zero | ~in_environment(A_11, start_time(sk2)) | ~environment(A_11) | ~greater(appear(C_13, A_11), sk3)))). % 13.12/4.98 tff(c_1127, plain, (![A_20, B_169]: (in_environment(A_20, B_169) | ~greater(B_169, start_time(A_20)) | ~greater(start_time(A_20), B_169) | ~environment(A_20)))). % 13.12/4.98 tff(c_1245, plain, (~greater(start_time(sk2), appear(efficient_producers, sk2)))). % 13.12/4.98 tff(c_1123, plain, (![B_169]: (in_environment(sk2, B_169) | ~greater(B_169, appear(an_organisation, sk2)) | ~greater(start_time(sk2), B_169)))). % 13.12/4.98 tff(c_264, plain, (![A_29, A_95]: (greater(A_29, zero) | ~greater(A_29, number_of_organizations(A_95, appear(an_organisation, A_95))) | ~in_environment(A_95, appear(an_organisation, A_95)) | ~environment(A_95)))). % 13.12/4.98 tff(c_1063, plain, (![B_165]: (in_environment(sk2, B_165) | ~greater(B_165, appear(an_organisation, sk2)) | ~greater(sk3, B_165)))). % 13.12/4.98 tff(c_1126, plain, (![B_169]: (in_environment(sk2, B_169) | ~greater(B_169, start_time(sk2)) | ~greater(start_time(sk2), B_169)))). % 13.12/4.98 tff(c_1130, plain, (![B_169]: (in_environment(sk2, B_169) | ~greater(B_169, sk3) | ~greater(start_time(sk2), B_169)))). % 13.12/4.98 tff(c_1067, plain, (![B_165]: (in_environment(sk2, B_165) | ~greater(B_165, start_time(sk2)) | ~greater(sk3, B_165)))). % 13.12/4.98 tff(c_1049, plain, (![A_20, B_162, B_164]: (in_environment(A_20, B_162) | ~in_environment(A_20, B_164) | ~greater(B_162, B_164) | ~greater(start_time(A_20), B_162) | ~environment(A_20)))). % 13.12/4.98 tff(c_1096, plain, (~greater(sk3, appear(efficient_producers, sk2)))). % 13.12/4.98 tff(c_1068, plain, (![B_165]: (in_environment(sk2, B_165) | ~greater(B_165, sk3) | ~greater(sk3, B_165)))). % 13.12/4.98 tff(c_1052, plain, (![B_162, B_164]: (in_environment(sk2, B_162) | ~in_environment(sk2, B_164) | ~greater(B_162, B_164) | ~greater(sk3, B_162)))). % 13.12/4.98 tff(c_468, plain, (![A_113, B_35, A_34, B_116]: (in_environment(A_113, B_35) | ~in_environment(A_113, A_34) | ~in_environment(A_113, B_116) | ~environment(A_113) | ~greater(B_35, B_116) | ~greater(A_34, B_35)))). % 13.12/4.98 tff(c_1033, plain, (~in_environment(sk2, appear(efficient_producers, sk2)))). % 13.12/4.98 tff(c_1032, plain, (~in_environment(sk2, appear(efficient_producers, e)))). % 13.12/4.98 tff(c_798, plain, (![A_29, A_139]: (greater(A_29, start_time(A_139)) | ~greater(A_29, appear(efficient_producers, e)) | appear(first_movers, A_139)=start_time(A_139) | ~environment(A_139)))). % 13.12/4.98 tff(c_1017, plain, (![A_29]: (cardinality_at_time(sk1(A_29, sk2), t)!=zero | ~in_environment(sk2, A_29) | ~greater(A_29, sk3)))). % 13.12/4.98 tff(c_985, plain, (![A_29]: (cardinality_at_time(sk1(A_29, sk2), t)!=zero | ~in_environment(sk2, A_29) | ~greater(A_29, start_time(sk2))))). % 13.12/4.98 tff(c_233, plain, (![A_29, A_90]: (greater(A_29, zero) | ~greater(A_29, number_of_organizations(A_90, appear(first_movers, A_90))) | ~in_environment(A_90, appear(first_movers, A_90)) | ~environment(A_90)))). % 13.12/4.98 tff(c_287, plain, (![A_98, A_97]: (cardinality_at_time(sk1(A_98, A_97), t)!=zero | ~in_environment(A_97, A_98) | ~environment(A_97) | ~greater(A_98, appear(an_organisation, A_97))))). % 13.12/4.98 tff(c_949, plain, (![A_40]: (~greater(appear(first_movers, A_40), start_time(sk2)) | ~environment(A_40)))). % 13.12/4.98 tff(c_948, plain, (~greater(appear(an_organisation, sk2), appear(efficient_producers, e)))). % 13.12/4.98 tff(c_930, plain, (![A_20]: (cardinality_at_time(first_movers, start_time(A_20))=zero | appear(first_movers, A_20)=start_time(A_20) | ~environment(A_20)))). % 13.12/4.98 tff(c_919, plain, (~greater(zero, appear(efficient_producers, e)))). % 13.12/4.98 tff(c_446, plain, (![A_16, C_18]: (in_environment(A_16, sk3) | ~greater_or_equal(C_18, sk3) | ~in_environment(A_16, C_18) | ~in_environment(A_16, start_time(sk2)) | ~environment(A_16)))). % 13.12/4.98 tff(c_869, plain, (subpopulation(efficient_producers, sk2, start_time(sk2)))). % 13.12/4.98 tff(c_850, plain, (sk1(start_time(sk2), sk2)=efficient_producers)). % 13.12/4.99 tff(c_296, plain, (![B_8, A_7, D_100, A_102]: (selection_favors(sk1(B_8, A_7), D_100, B_8) | cardinality_at_time(D_100, B_8)!=zero | ~subpopulation(D_100, A_102, B_8) | ~subpopulation(sk1(B_8, A_7), A_102, B_8) | ~environment(A_102) | ~greater(number_of_organizations(A_7, B_8), zero) | ~environment(A_7)))). % 13.12/4.99 tff(c_778, plain, (![B_6, A_5]: (sk1(B_6, A_5)=first_movers | sk1(B_6, A_5)=efficient_producers | ~greater(number_of_organizations(A_5, B_6), zero) | ~environment(A_5)))). % 13.12/4.99 tff(c_370, plain, (![A_20]: (in_environment(A_20, sk3) | ~greater_or_equal(start_time(A_20), sk3) | ~in_environment(A_20, start_time(sk2)) | ~environment(A_20)))). % 13.12/4.99 tff(c_780, plain, (~greater(zero, start_time(sk2)))). % 13.12/4.99 tff(c_368, plain, (![A_40]: (greater(appear(efficient_producers, e), start_time(A_40)) | appear(first_movers, A_40)=start_time(A_40) | ~environment(A_40)))). % 13.12/4.99 tff(c_755, plain, (![A_29]: (greater(A_29, appear(an_organisation, sk2)) | ~greater(A_29, appear(efficient_producers, sk2))))). % 13.12/4.99 tff(c_768, plain, (~greater(start_time(sk2), start_time(sk2)))). % 13.12/4.99 tff(c_754, plain, (cardinality_at_time(efficient_producers, appear(an_organisation, sk2))=zero)). % 13.12/4.99 tff(c_736, plain, (greater(appear(efficient_producers, sk2), appear(an_organisation, sk2)))). % 13.12/4.99 tff(c_629, plain, (![A_29, A_128]: (greater(A_29, appear(an_organisation, sk2)) | ~greater(A_29, A_128) | ~greater(A_128, start_time(sk2))))). % 13.12/4.99 tff(c_669, plain, (cardinality_at_time(first_movers, t)!=zero)). % 13.12/4.99 tff(c_245, plain, (![A_91, A_23, C_94]: (in_environment(A_91, appear(first_movers, A_23)) | ~greater_or_equal(C_94, appear(first_movers, A_23)) | ~in_environment(A_91, C_94) | ~in_environment(A_91, appear(an_organisation, A_23)) | ~environment(A_91) | ~environment(A_23)))). % 13.12/4.99 tff(c_652, plain, (cardinality_at_time(first_movers, appear(an_organisation, sk2))=zero)). % 13.12/4.99 tff(c_427, plain, (![B_12]: (cardinality_at_time(first_movers, B_12)=zero | ~greater(start_time(sk2), B_12) | ~in_environment(sk2, B_12)))). % 13.12/4.99 tff(c_630, plain, (~greater(appear(an_organisation, sk2), sk3))). % 13.12/4.99 tff(c_614, plain, (![A_29]: (greater(A_29, appear(an_organisation, sk2)) | ~greater(A_29, start_time(sk2))))). % 13.12/4.99 tff(c_605, plain, (greater(start_time(sk2), appear(an_organisation, sk2)))). % 13.12/4.99 tff(c_246, plain, (![A_91, A_21, C_94]: (in_environment(A_91, appear(first_movers, A_21)) | ~greater_or_equal(C_94, appear(first_movers, A_21)) | ~in_environment(A_91, C_94) | ~in_environment(A_91, start_time(A_21)) | ~environment(A_91) | ~environment(A_21)))). % 13.12/4.99 tff(c_586, plain, (![A_29]: (greater(A_29, zero) | ~greater(A_29, number_of_organizations(sk2, start_time(sk2)))))). % 13.12/4.99 tff(c_565, plain, (greater(number_of_organizations(sk2, start_time(sk2)), zero))). % 13.12/4.99 tff(c_508, plain, (![A_29, A_117]: (greater(A_29, start_time(sk2)) | ~greater(A_29, A_117) | ~greater(A_117, sk3)))). % 13.12/4.99 tff(c_431, plain, (![A_56]: (greater(A_56, start_time(sk2)) | ~greater(A_56, appear(efficient_producers, e))))). % 13.12/4.99 tff(c_517, plain, (in_environment(sk2, appear(an_organisation, sk2)))). % 13.12/4.99 tff(c_188, plain, (![A_29, B_80, A_81]: (greater(A_29, zero) | ~greater(A_29, cardinality_at_time(sk1(B_80, A_81), B_80)) | ~greater(number_of_organizations(A_81, B_80), zero) | ~environment(A_81)))). % 13.12/4.99 tff(c_518, plain, (in_environment(sk2, start_time(sk2)))). % 13.12/4.99 tff(c_374, plain, (![A_29]: (greater(A_29, start_time(sk2)) | ~greater(A_29, sk3)))). % 13.12/4.99 tff(c_435, plain, (greater_or_equal(start_time(sk2), appear(an_organisation, sk2)))). % 13.12/4.99 tff(c_437, plain, (greater(appear(efficient_producers, e), start_time(sk2)))). % 13.12/4.99 tff(c_372, plain, (~greater(start_time(sk2), appear(efficient_producers, e)))). % 13.12/4.99 tff(c_247, plain, (![A_91, A_34, C_94, B_35]: (in_environment(A_91, A_34) | ~greater_or_equal(C_94, A_34) | ~in_environment(A_91, C_94) | ~in_environment(A_91, B_35) | ~environment(A_91) | ~greater(A_34, B_35)))). % 13.12/4.99 tff(c_425, plain, (~greater(start_time(sk2), sk3))). % 13.12/4.99 tff(c_375, plain, (greater(sk3, start_time(sk2)))). % 13.12/4.99 tff(c_376, plain, (greater_or_equal(sk3, start_time(sk2)))). % 13.12/4.99 tff(c_369, plain, (appear(first_movers, sk2)=start_time(sk2))). % 13.12/4.99 tff(c_144, plain, (![A_29, A_76]: (greater(A_29, start_time(A_76)) | ~greater(A_29, appear(first_movers, A_76)) | appear(first_movers, A_76)=start_time(A_76) | ~environment(A_76)))). % 13.12/4.99 tff(c_230, plain, (![A_90]: (cardinality_at_time(sk1(appear(first_movers, A_90), A_90), t)!=zero | ~in_environment(A_90, appear(first_movers, A_90)) | ~environment(A_90)))). % 13.12/4.99 tff(c_261, plain, (![A_95]: (cardinality_at_time(sk1(appear(an_organisation, A_95), A_95), t)!=zero | ~in_environment(A_95, appear(an_organisation, A_95)) | ~environment(A_95)))). % 13.12/4.99 tff(c_334, plain, (~greater(sk3, appear(efficient_producers, e)))). % 13.12/4.99 tff(c_137, plain, (![A_29, A_75, A_74]: (greater(A_29, appear(first_movers, A_75)) | ~greater(A_29, A_74) | ~greater(A_74, appear(efficient_producers, e)) | ~environment(A_75)))). % 13.12/4.99 tff(c_2, plain, (![B_2, D_4, C_3, A_1]: (selection_favors(B_2, D_4, C_3) | cardinality_at_time(D_4, C_3)!=zero | ~greater(cardinality_at_time(B_2, C_3), zero) | ~subpopulation(D_4, A_1, C_3) | ~subpopulation(B_2, A_1, C_3) | ~environment(A_1)))). % 13.12/4.99 tff(c_217, plain, (![A_88, A_34]: (greater(number_of_organizations(A_88, A_34), zero) | ~in_environment(A_88, A_34) | ~environment(A_88) | ~greater(A_34, appear(an_organisation, A_88))))). % 13.12/4.99 tff(c_80, plain, (![A_52]: (appear(first_movers, A_52)=appear(an_organisation, A_52) | greater(appear(first_movers, A_52), appear(an_organisation, A_52)) | ~environment(A_52)))). % 13.12/4.99 tff(c_218, plain, (![A_88]: (greater(number_of_organizations(A_88, appear(an_organisation, A_88)), zero) | ~in_environment(A_88, appear(an_organisation, A_88)) | ~environment(A_88)))). % 13.12/4.99 tff(c_14, plain, (![A_16, D_19, B_17, C_18]: (in_environment(A_16, D_19) | ~greater_or_equal(D_19, B_17) | ~greater_or_equal(C_18, D_19) | ~in_environment(A_16, C_18) | ~in_environment(A_16, B_17) | ~environment(A_16)))). % 13.12/4.99 tff(c_216, plain, (![A_23]: (greater(number_of_organizations(A_23, appear(first_movers, A_23)), zero) | ~in_environment(A_23, appear(first_movers, A_23)) | ~environment(A_23)))). % 13.12/4.99 tff(c_38, plain, (![A_38, B_39]: (greater(number_of_organizations(A_38, B_39), zero) | ~greater_or_equal(B_39, appear(an_organisation, A_38)) | ~in_environment(A_38, B_39) | ~environment(A_38)))). % 13.12/4.99 tff(c_202, plain, (![A_40]: (~greater(appear(first_movers, A_40), sk3) | ~environment(A_40)))). % 13.12/4.99 tff(c_194, plain, (~greater(zero, sk3))). % 13.12/4.99 tff(c_42, plain, (![B_42, C_43, A_41]: (first_movers=B_42 | efficient_producers=B_42 | ~greater(cardinality_at_time(B_42, C_43), zero) | ~subpopulation(B_42, A_41, C_43) | ~environment(A_41)))). % 13.12/4.99 tff(c_187, plain, (![B_80, A_81]: (cardinality_at_time(sk1(B_80, A_81), t)!=zero | ~greater(number_of_organizations(A_81, B_80), zero) | ~environment(A_81)))). % 13.12/4.99 tff(c_177, plain, (cardinality_at_time(efficient_producers, t)!=zero)). % 13.12/4.99 tff(c_6, plain, (![B_8, A_7]: (greater(cardinality_at_time(sk1(B_8, A_7), B_8), zero) | ~greater(number_of_organizations(A_7, B_8), zero) | ~environment(A_7)))). % 13.12/4.99 tff(c_169, plain, (cardinality_at_time(efficient_producers, sk3)=zero)). % 13.12/4.99 tff(c_10, plain, (![C_13, B_12, A_11]: (cardinality_at_time(C_13, B_12)=zero | ~greater(appear(C_13, A_11), B_12) | ~in_environment(A_11, B_12) | ~environment(A_11)))). % 13.12/4.99 tff(c_74, plain, (![A_50]: (appear(first_movers, A_50)=start_time(A_50) | greater(appear(first_movers, A_50), start_time(A_50)) | ~environment(A_50)))). % 13.12/4.99 tff(c_91, plain, (![A_56, A_40]: (greater(A_56, appear(first_movers, A_40)) | ~greater(A_56, appear(efficient_producers, e)) | ~environment(A_40)))). % 13.12/4.99 tff(c_4, plain, (![B_6, A_5]: (subpopulation(sk1(B_6, A_5), A_5, B_6) | ~greater(number_of_organizations(A_5, B_6), zero) | ~environment(A_5)))). % 13.12/4.99 tff(c_90, plain, (![A_56, A_24]: (greater(A_56, zero) | ~greater(A_56, number_of_organizations(e, appear(an_organisation, A_24))) | ~environment(A_24)))). % 13.12/4.99 tff(c_128, plain, (~greater(sk3, sk3))). % 13.12/4.99 tff(c_20, plain, (![A_22]: (in_environment(A_22, appear(an_organisation, A_22)) | ~in_environment(A_22, appear(first_movers, A_22)) | ~environment(A_22)))). % 13.12/4.99 tff(c_109, plain, (~environment(e))). % 13.12/4.99 tff(c_12, plain, (![A_14, B_15]: (in_environment(A_14, B_15) | ~greater(number_of_organizations(A_14, B_15), zero) | ~environment(A_14)))). % 13.12/4.99 tff(c_28, plain, (![A_27, B_28]: (subpopulation(efficient_producers, A_27, B_28) | ~in_environment(A_27, B_28) | ~environment(A_27)))). % 13.12/4.99 tff(c_92, plain, (![A_56]: (greater(A_56, sk3) | ~greater(A_56, appear(efficient_producers, sk2))))). % 13.12/4.99 tff(c_8, plain, (![A_9, B_10]: (~greater(cardinality_at_time(A_9, B_10), zero) | cardinality_at_time(A_9, t)!=zero))). % 13.12/4.99 tff(c_30, plain, (![A_29, C_31, B_30]: (greater(A_29, C_31) | ~greater(B_30, C_31) | ~greater(A_29, B_30)))). % 13.12/4.99 tff(c_26, plain, (![A_25, B_26]: (subpopulation(first_movers, A_25, B_26) | ~in_environment(A_25, B_26) | ~environment(A_25)))). % 13.12/4.99 tff(c_24, plain, (![A_24]: (greater(number_of_organizations(e, appear(an_organisation, A_24)), zero) | ~environment(A_24)))). % 13.12/4.99 tff(c_22, plain, (![A_23]: (greater_or_equal(appear(first_movers, A_23), appear(an_organisation, A_23)) | ~environment(A_23)))). % 13.12/4.99 tff(c_40, plain, (![A_40]: (greater(appear(efficient_producers, e), appear(first_movers, A_40)) | ~environment(A_40)))). % 13.12/4.99 tff(c_18, plain, (![A_21]: (greater_or_equal(appear(first_movers, A_21), start_time(A_21)) | ~environment(A_21)))). % 13.12/4.99 tff(c_32, plain, (![B_33, A_32]: (B_33=A_32 | greater(A_32, B_33) | ~greater_or_equal(A_32, B_33)))). % 13.12/4.99 tff(c_16, plain, (![A_20]: (in_environment(A_20, start_time(A_20)) | ~environment(A_20)))). % 13.12/4.99 tff(c_34, plain, (![A_34, B_35]: (greater_or_equal(A_34, B_35) | ~greater(A_34, B_35)))). % 13.12/4.99 tff(c_50, plain, (greater(appear(efficient_producers, sk2), sk3))). % 13.12/4.99 tff(c_52, plain, (~selection_favors(first_movers, efficient_producers, sk3))). % 13.12/4.99 tff(c_36, plain, (![B_37]: (greater_or_equal(B_37, B_37)))). % 13.12/4.99 tff(c_46, plain, (in_environment(sk2, sk3))). % 13.12/4.99 tff(c_44, plain, (environment(sk2))). % 13.12/4.99 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.12/4.99 %------------------------------------------------------------------------------