%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT034+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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:06:17 AM UTC 2026 % Result : Theorem 67.65s 68.02s % Output : Proof 68.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT034+2 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.05 % Command : duper %s % 0.09/0.36 % Computer : n029.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 12:33:27 UTC 2026 % 0.09/0.36 % CPUTime : % 67.65/68.02 SZS status Theorem for theBenchmark.p % 67.65/68.02 SZS output start Proof for theBenchmark.p % 67.65/68.02 Clause #0 (by assumption #[]): Eq % 67.65/68.02 (∀ (E S1 S2 T : Iota), % 67.65/68.02 And (And (environment E) (subpopulations S1 S2 E T)) (greater (growth_rate S2 T) (growth_rate S1 T)) → % 67.65/68.02 selection_favors S2 S1 T) % 67.65/68.02 True % 67.65/68.02 Clause #1 (by assumption #[]): Eq % 67.65/68.02 (∀ (E T : Iota), % 67.65/68.02 And (environment E) (subpopulations first_movers efficient_producers E T) → % 67.65/68.02 Not (decreases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T)))) % 67.65/68.02 True % 67.65/68.02 Clause #2 (by assumption #[]): Eq % 67.65/68.02 (∀ (E : Iota), % 67.65/68.02 And (environment E) (in_environment E (critical_point E)) → % 67.65/68.02 subpopulations first_movers efficient_producers E (critical_point E)) % 67.65/68.02 True % 67.65/68.02 Clause #3 (by assumption #[]): Eq % 67.65/68.02 (∀ (E : Iota), % 67.65/68.02 And (environment E) (in_environment E (appear efficient_producers E)) → % 67.65/68.02 subpopulations first_movers efficient_producers E (appear efficient_producers E)) % 67.65/68.02 True % 67.65/68.02 Clause #4 (by assumption #[]): Eq % 67.65/68.02 (∀ (T : Iota), % 67.65/68.02 And (decreases (difference (founding_rate first_movers T) (founding_rate efficient_producers T))) % 67.65/68.02 (Not (decreases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T)))) → % 67.65/68.02 decreases (difference (growth_rate first_movers T) (growth_rate efficient_producers T))) % 67.65/68.02 True % 67.65/68.02 Clause #5 (by assumption #[]): Eq % 67.65/68.02 (∀ (E T To : Iota), % 67.65/68.02 And % 67.65/68.02 (And % 67.65/68.02 (And (And (environment E) (in_environment E To)) % 67.65/68.02 (greater_or_equal (difference (growth_rate first_movers To) (growth_rate efficient_producers To)) zero)) % 67.65/68.02 (greater_or_equal T (appear efficient_producers E))) % 67.65/68.02 (greater To T) → % 67.65/68.02 decreases (difference (growth_rate first_movers T) (growth_rate efficient_producers T)) → % 67.65/68.02 greater (difference (growth_rate first_movers T) (growth_rate efficient_producers T)) zero) % 67.65/68.02 True % 67.65/68.02 Clause #6 (by assumption #[]): Eq % 67.65/68.02 (∀ (T : Iota), % 67.65/68.02 Iff (greater zero (difference (growth_rate first_movers T) (growth_rate efficient_producers T))) % 67.65/68.02 (greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 67.65/68.02 True % 67.65/68.02 Clause #7 (by assumption #[]): Eq % 67.65/68.02 (∀ (T : Iota), % 67.65/68.02 Iff (greater (difference (growth_rate first_movers T) (growth_rate efficient_producers T)) zero) % 67.65/68.02 (greater (growth_rate first_movers T) (growth_rate efficient_producers T))) % 67.65/68.02 True % 67.65/68.02 Clause #11 (by assumption #[]): Eq % 67.65/68.02 (∀ (E T : Iota), % 67.65/68.02 And % 67.65/68.02 (And (And (environment E) (in_environment E (critical_point E))) % 67.65/68.02 (greater_or_equal T (appear efficient_producers E))) % 67.65/68.02 (greater (critical_point E) T) → % 67.65/68.02 in_environment E T) % 67.65/68.02 True % 67.65/68.02 Clause #13 (by assumption #[]): Eq % 67.65/68.02 (∀ (E T : Iota), % 67.65/68.02 And (environment E) (subpopulations first_movers efficient_producers E T) → % 67.65/68.02 subpopulations efficient_producers first_movers E T) % 67.65/68.02 True % 67.65/68.02 Clause #14 (by assumption #[]): Eq % 67.65/68.02 (∀ (E T : Iota), % 67.65/68.02 And (environment E) (subpopulations first_movers efficient_producers E T) → % 67.65/68.02 greater_or_equal T (appear efficient_producers E)) % 67.65/68.02 True % 67.65/68.02 Clause #15 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (greater_or_equal X Y) (Or (greater X Y) (Eq X Y))) True % 67.65/68.02 Clause #16 (by assumption #[]): Eq % 67.65/68.02 (∀ (E T : Iota), % 67.65/68.02 And (And (environment E) (subpopulations first_movers efficient_producers E T)) % 67.65/68.02 (Not (greater zero (difference (growth_rate first_movers T) (growth_rate efficient_producers T)))) → % 67.65/68.02 greater_or_equal (difference (growth_rate first_movers T) (growth_rate efficient_producers T)) zero) % 67.65/68.02 True % 67.65/68.02 Clause #17 (by assumption #[]): Eq % 67.65/68.02 (∀ (E Tc : Iota), % 67.65/68.02 And (environment E) (Eq Tc (critical_point E)) → % 67.65/68.02 And (Not (greater (growth_rate efficient_producers Tc) (growth_rate first_movers Tc))) % 67.65/68.02 (∀ (T : Iota), % 67.65/68.02 And (subpopulations first_movers efficient_producers E T) (greater T Tc) → % 67.65/68.02 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 67.65/68.02 True % 67.65/68.02 Clause #18 (by assumption #[]): Eq % 67.65/68.02 (∀ (E T1 T2 T : Iota), % 67.65/68.02 And % 67.65/68.02 (And % 67.65/68.02 (And (And (environment E) (subpopulations first_movers efficient_producers E T1)) % 67.78/68.06 (subpopulations first_movers efficient_producers E T2)) % 67.78/68.06 (greater_or_equal T T1)) % 67.78/68.06 (greater_or_equal T2 T) → % 67.78/68.06 subpopulations first_movers efficient_producers E T) % 67.78/68.06 True % 67.78/68.06 Clause #19 (by assumption #[]): Eq % 67.78/68.06 (∀ (E T : Iota), % 67.78/68.06 And (environment E) (subpopulations first_movers efficient_producers E T) → % 67.78/68.06 decreases (difference (founding_rate first_movers T) (founding_rate efficient_producers T))) % 67.78/68.06 True % 67.78/68.06 Clause #20 (by assumption #[]): Eq % 67.78/68.06 (Not % 67.78/68.06 (∀ (E T : Iota), % 67.78/68.06 And % 67.78/68.06 (And (And (environment E) (in_environment E (critical_point E))) % 67.78/68.06 (greater_or_equal T (appear efficient_producers E))) % 67.78/68.06 (greater (critical_point E) T) → % 67.78/68.06 selection_favors first_movers efficient_producers T)) % 67.78/68.06 True % 67.78/68.06 Clause #21 (by clausification #[11]): ∀ (a : Iota), % 67.78/68.06 Eq % 67.78/68.06 (∀ (T : Iota), % 67.78/68.06 And % 67.78/68.06 (And (And (environment a) (in_environment a (critical_point a))) % 67.78/68.06 (greater_or_equal T (appear efficient_producers a))) % 67.78/68.06 (greater (critical_point a) T) → % 67.78/68.06 in_environment a T) % 67.78/68.06 True % 67.78/68.06 Clause #22 (by clausification #[21]): ∀ (a a_1 : Iota), % 67.78/68.06 Eq % 67.78/68.06 (And % 67.78/68.06 (And (And (environment a) (in_environment a (critical_point a))) % 67.78/68.06 (greater_or_equal a_1 (appear efficient_producers a))) % 67.78/68.06 (greater (critical_point a) a_1) → % 67.78/68.06 in_environment a a_1) % 67.78/68.06 True % 67.78/68.06 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), % 67.78/68.06 Or % 67.78/68.06 (Eq % 67.78/68.06 (And % 67.78/68.06 (And (And (environment a) (in_environment a (critical_point a))) % 67.78/68.06 (greater_or_equal a_1 (appear efficient_producers a))) % 67.78/68.06 (greater (critical_point a) a_1)) % 67.78/68.06 False) % 67.78/68.06 (Eq (in_environment a a_1) True) % 67.78/68.06 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), % 67.78/68.06 Or (Eq (in_environment a a_1) True) % 67.78/68.06 (Or % 67.78/68.06 (Eq % 67.78/68.06 (And (And (environment a) (in_environment a (critical_point a))) % 67.78/68.06 (greater_or_equal a_1 (appear efficient_producers a))) % 67.78/68.06 False) % 67.78/68.06 (Eq (greater (critical_point a) a_1) False)) % 67.78/68.06 Clause #25 (by clausification #[24]): ∀ (a a_1 : Iota), % 67.78/68.06 Or (Eq (in_environment a a_1) True) % 67.78/68.06 (Or (Eq (greater (critical_point a) a_1) False) % 67.78/68.06 (Or (Eq (And (environment a) (in_environment a (critical_point a))) False) % 67.78/68.06 (Eq (greater_or_equal a_1 (appear efficient_producers a)) False))) % 67.78/68.06 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), % 67.78/68.06 Or (Eq (in_environment a a_1) True) % 67.78/68.06 (Or (Eq (greater (critical_point a) a_1) False) % 67.78/68.06 (Or (Eq (greater_or_equal a_1 (appear efficient_producers a)) False) % 67.78/68.06 (Or (Eq (environment a) False) (Eq (in_environment a (critical_point a)) False)))) % 67.78/68.06 Clause #40 (by clausification #[20]): Eq % 67.78/68.06 (∀ (E T : Iota), % 67.78/68.06 And % 67.78/68.06 (And (And (environment E) (in_environment E (critical_point E))) % 67.78/68.06 (greater_or_equal T (appear efficient_producers E))) % 67.78/68.06 (greater (critical_point E) T) → % 67.78/68.06 selection_favors first_movers efficient_producers T) % 67.78/68.06 False % 67.78/68.06 Clause #41 (by clausification #[40]): ∀ (a : Iota), % 67.78/68.06 Eq % 67.78/68.06 (Not % 67.78/68.06 (∀ (T : Iota), % 67.78/68.06 And % 67.78/68.06 (And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (critical_point (skS.0 0 a)))) % 67.78/68.06 (greater_or_equal T (appear efficient_producers (skS.0 0 a)))) % 67.78/68.06 (greater (critical_point (skS.0 0 a)) T) → % 67.78/68.06 selection_favors first_movers efficient_producers T)) % 67.78/68.06 True % 67.78/68.06 Clause #42 (by clausification #[41]): ∀ (a : Iota), % 67.78/68.06 Eq % 67.78/68.06 (∀ (T : Iota), % 67.78/68.06 And % 67.78/68.06 (And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (critical_point (skS.0 0 a)))) % 67.78/68.06 (greater_or_equal T (appear efficient_producers (skS.0 0 a)))) % 67.78/68.06 (greater (critical_point (skS.0 0 a)) T) → % 67.78/68.06 selection_favors first_movers efficient_producers T) % 67.78/68.06 False % 67.78/68.06 Clause #43 (by clausification #[42]): ∀ (a a_1 : Iota), % 67.78/68.06 Eq % 67.78/68.06 (Not % 67.78/68.06 (And % 67.78/68.06 (And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (critical_point (skS.0 0 a)))) % 67.78/68.06 (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers (skS.0 0 a)))) % 67.78/68.06 (greater (critical_point (skS.0 0 a)) (skS.0 1 a a_1)) → % 67.78/68.10 selection_favors first_movers efficient_producers (skS.0 1 a a_1))) % 67.78/68.10 True % 67.78/68.10 Clause #44 (by clausification #[43]): ∀ (a a_1 : Iota), % 67.78/68.10 Eq % 67.78/68.10 (And % 67.78/68.10 (And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (critical_point (skS.0 0 a)))) % 67.78/68.10 (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers (skS.0 0 a)))) % 67.78/68.10 (greater (critical_point (skS.0 0 a)) (skS.0 1 a a_1)) → % 67.78/68.10 selection_favors first_movers efficient_producers (skS.0 1 a a_1)) % 67.78/68.10 False % 67.78/68.10 Clause #45 (by clausification #[44]): ∀ (a a_1 : Iota), % 67.78/68.10 Eq % 67.78/68.10 (And % 67.78/68.10 (And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (critical_point (skS.0 0 a)))) % 67.78/68.10 (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers (skS.0 0 a)))) % 67.78/68.10 (greater (critical_point (skS.0 0 a)) (skS.0 1 a a_1))) % 67.78/68.10 True % 67.78/68.10 Clause #46 (by clausification #[44]): ∀ (a a_1 : Iota), Eq (selection_favors first_movers efficient_producers (skS.0 1 a a_1)) False % 67.78/68.10 Clause #47 (by clausification #[45]): ∀ (a a_1 : Iota), Eq (greater (critical_point (skS.0 0 a)) (skS.0 1 a a_1)) True % 67.78/68.10 Clause #48 (by clausification #[45]): ∀ (a a_1 : Iota), % 67.78/68.10 Eq % 67.78/68.10 (And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (critical_point (skS.0 0 a)))) % 67.78/68.10 (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers (skS.0 0 a)))) % 67.78/68.10 True % 67.78/68.10 Clause #50 (by clausification #[0]): ∀ (a : Iota), % 67.78/68.10 Eq % 67.78/68.10 (∀ (S1 S2 T : Iota), % 67.78/68.10 And (And (environment a) (subpopulations S1 S2 a T)) (greater (growth_rate S2 T) (growth_rate S1 T)) → % 67.78/68.10 selection_favors S2 S1 T) % 67.78/68.10 True % 67.78/68.10 Clause #51 (by clausification #[50]): ∀ (a a_1 : Iota), % 67.78/68.10 Eq % 67.78/68.10 (∀ (S2 T : Iota), % 67.78/68.10 And (And (environment a) (subpopulations a_1 S2 a T)) (greater (growth_rate S2 T) (growth_rate a_1 T)) → % 67.78/68.10 selection_favors S2 a_1 T) % 67.78/68.10 True % 67.78/68.10 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), % 67.78/68.10 Eq % 67.78/68.10 (∀ (T : Iota), % 67.78/68.10 And (And (environment a) (subpopulations a_1 a_2 a T)) (greater (growth_rate a_2 T) (growth_rate a_1 T)) → % 67.78/68.10 selection_favors a_2 a_1 T) % 67.78/68.10 True % 67.78/68.10 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 : Iota), % 67.78/68.10 Eq % 67.78/68.10 (And (And (environment a) (subpopulations a_1 a_2 a a_3)) (greater (growth_rate a_2 a_3) (growth_rate a_1 a_3)) → % 67.78/68.10 selection_favors a_2 a_1 a_3) % 67.78/68.10 True % 67.78/68.10 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 : Iota), % 67.78/68.10 Or % 67.78/68.10 (Eq (And (And (environment a) (subpopulations a_1 a_2 a a_3)) (greater (growth_rate a_2 a_3) (growth_rate a_1 a_3))) % 67.78/68.10 False) % 67.78/68.10 (Eq (selection_favors a_2 a_1 a_3) True) % 67.78/68.10 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 a_3 : Iota), % 67.78/68.10 Or (Eq (selection_favors a a_1 a_2) True) % 67.78/68.10 (Or (Eq (And (environment a_3) (subpopulations a_1 a a_3 a_2)) False) % 67.78/68.10 (Eq (greater (growth_rate a a_2) (growth_rate a_1 a_2)) False)) % 67.78/68.10 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 : Iota), % 67.78/68.10 Or (Eq (selection_favors a a_1 a_2) True) % 67.78/68.10 (Or (Eq (greater (growth_rate a a_2) (growth_rate a_1 a_2)) False) % 67.78/68.10 (Or (Eq (environment a_3) False) (Eq (subpopulations a_1 a a_3 a_2) False))) % 67.78/68.10 Clause #57 (by clausification #[2]): ∀ (a : Iota), % 67.78/68.10 Eq % 67.78/68.10 (And (environment a) (in_environment a (critical_point a)) → % 67.78/68.10 subpopulations first_movers efficient_producers a (critical_point a)) % 67.78/68.10 True % 67.78/68.10 Clause #58 (by clausification #[57]): ∀ (a : Iota), % 67.78/68.10 Or (Eq (And (environment a) (in_environment a (critical_point a))) False) % 67.78/68.10 (Eq (subpopulations first_movers efficient_producers a (critical_point a)) True) % 67.78/68.10 Clause #59 (by clausification #[58]): ∀ (a : Iota), % 67.78/68.10 Or (Eq (subpopulations first_movers efficient_producers a (critical_point a)) True) % 67.78/68.10 (Or (Eq (environment a) False) (Eq (in_environment a (critical_point a)) False)) % 67.78/68.10 Clause #60 (by clausification #[14]): ∀ (a : Iota), % 67.78/68.10 Eq % 67.78/68.10 (∀ (T : Iota), % 67.78/68.10 And (environment a) (subpopulations first_movers efficient_producers a T) → % 67.78/68.10 greater_or_equal T (appear efficient_producers a)) % 67.78/68.10 True % 67.78/68.10 Clause #61 (by clausification #[60]): ∀ (a a_1 : Iota), % 67.78/68.10 Eq % 67.78/68.10 (And (environment a) (subpopulations first_movers efficient_producers a a_1) → % 67.88/68.14 greater_or_equal a_1 (appear efficient_producers a)) % 67.88/68.14 True % 67.88/68.14 Clause #62 (by clausification #[61]): ∀ (a a_1 : Iota), % 67.88/68.14 Or (Eq (And (environment a) (subpopulations first_movers efficient_producers a a_1)) False) % 67.88/68.14 (Eq (greater_or_equal a_1 (appear efficient_producers a)) True) % 67.88/68.14 Clause #63 (by clausification #[62]): ∀ (a a_1 : Iota), % 67.88/68.14 Or (Eq (greater_or_equal a (appear efficient_producers a_1)) True) % 67.88/68.14 (Or (Eq (environment a_1) False) (Eq (subpopulations first_movers efficient_producers a_1 a) False)) % 67.88/68.14 Clause #64 (by clausification #[13]): ∀ (a : Iota), % 67.88/68.14 Eq % 67.88/68.14 (∀ (T : Iota), % 67.88/68.14 And (environment a) (subpopulations first_movers efficient_producers a T) → % 67.88/68.14 subpopulations efficient_producers first_movers a T) % 67.88/68.14 True % 67.88/68.14 Clause #65 (by clausification #[64]): ∀ (a a_1 : Iota), % 67.88/68.14 Eq % 67.88/68.14 (And (environment a) (subpopulations first_movers efficient_producers a a_1) → % 67.88/68.14 subpopulations efficient_producers first_movers a a_1) % 67.88/68.14 True % 67.88/68.14 Clause #66 (by clausification #[65]): ∀ (a a_1 : Iota), % 67.88/68.14 Or (Eq (And (environment a) (subpopulations first_movers efficient_producers a a_1)) False) % 67.88/68.14 (Eq (subpopulations efficient_producers first_movers a a_1) True) % 67.88/68.14 Clause #67 (by clausification #[66]): ∀ (a a_1 : Iota), % 67.88/68.14 Or (Eq (subpopulations efficient_producers first_movers a a_1) True) % 67.88/68.14 (Or (Eq (environment a) False) (Eq (subpopulations first_movers efficient_producers a a_1) False)) % 67.88/68.14 Clause #74 (by clausification #[3]): ∀ (a : Iota), % 67.88/68.14 Eq % 67.88/68.14 (And (environment a) (in_environment a (appear efficient_producers a)) → % 67.88/68.14 subpopulations first_movers efficient_producers a (appear efficient_producers a)) % 67.88/68.14 True % 67.88/68.14 Clause #75 (by clausification #[74]): ∀ (a : Iota), % 67.88/68.14 Or (Eq (And (environment a) (in_environment a (appear efficient_producers a))) False) % 67.88/68.14 (Eq (subpopulations first_movers efficient_producers a (appear efficient_producers a)) True) % 67.88/68.14 Clause #76 (by clausification #[75]): ∀ (a : Iota), % 67.88/68.14 Or (Eq (subpopulations first_movers efficient_producers a (appear efficient_producers a)) True) % 67.88/68.14 (Or (Eq (environment a) False) (Eq (in_environment a (appear efficient_producers a)) False)) % 67.88/68.14 Clause #77 (by clausification #[1]): ∀ (a : Iota), % 67.88/68.14 Eq % 67.88/68.14 (∀ (T : Iota), % 67.88/68.14 And (environment a) (subpopulations first_movers efficient_producers a T) → % 67.88/68.14 Not (decreases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T)))) % 67.88/68.14 True % 67.88/68.14 Clause #78 (by clausification #[77]): ∀ (a a_1 : Iota), % 67.88/68.14 Eq % 67.88/68.14 (And (environment a) (subpopulations first_movers efficient_producers a a_1) → % 67.88/68.14 Not (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1)))) % 67.88/68.14 True % 67.88/68.14 Clause #79 (by clausification #[78]): ∀ (a a_1 : Iota), % 67.88/68.14 Or (Eq (And (environment a) (subpopulations first_movers efficient_producers a a_1)) False) % 67.88/68.14 (Eq (Not (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1)))) % 67.88/68.14 True) % 67.88/68.14 Clause #80 (by clausification #[79]): ∀ (a a_1 : Iota), % 67.88/68.14 Or (Eq (Not (decreases (difference (disbanding_rate first_movers a) (disbanding_rate efficient_producers a)))) True) % 67.88/68.14 (Or (Eq (environment a_1) False) (Eq (subpopulations first_movers efficient_producers a_1 a) False)) % 67.88/68.14 Clause #81 (by clausification #[80]): ∀ (a a_1 : Iota), % 67.88/68.14 Or (Eq (environment a) False) % 67.88/68.14 (Or (Eq (subpopulations first_movers efficient_producers a a_1) False) % 67.88/68.14 (Eq (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) False)) % 67.88/68.14 Clause #82 (by clausification #[4]): ∀ (a : Iota), % 67.88/68.14 Eq % 67.88/68.14 (And (decreases (difference (founding_rate first_movers a) (founding_rate efficient_producers a))) % 67.88/68.14 (Not (decreases (difference (disbanding_rate first_movers a) (disbanding_rate efficient_producers a)))) → % 67.88/68.14 decreases (difference (growth_rate first_movers a) (growth_rate efficient_producers a))) % 67.88/68.14 True % 67.88/68.14 Clause #83 (by clausification #[82]): ∀ (a : Iota), % 67.88/68.14 Or % 67.88/68.14 (Eq % 67.88/68.14 (And (decreases (difference (founding_rate first_movers a) (founding_rate efficient_producers a))) % 67.88/68.18 (Not (decreases (difference (disbanding_rate first_movers a) (disbanding_rate efficient_producers a))))) % 67.88/68.18 False) % 67.88/68.18 (Eq (decreases (difference (growth_rate first_movers a) (growth_rate efficient_producers a))) True) % 67.88/68.18 Clause #84 (by clausification #[83]): ∀ (a : Iota), % 67.88/68.18 Or (Eq (decreases (difference (growth_rate first_movers a) (growth_rate efficient_producers a))) True) % 67.88/68.18 (Or (Eq (decreases (difference (founding_rate first_movers a) (founding_rate efficient_producers a))) False) % 67.88/68.18 (Eq (Not (decreases (difference (disbanding_rate first_movers a) (disbanding_rate efficient_producers a)))) % 67.88/68.18 False)) % 67.88/68.18 Clause #85 (by clausification #[84]): ∀ (a : Iota), % 67.88/68.18 Or (Eq (decreases (difference (growth_rate first_movers a) (growth_rate efficient_producers a))) True) % 67.88/68.18 (Or (Eq (decreases (difference (founding_rate first_movers a) (founding_rate efficient_producers a))) False) % 67.88/68.18 (Eq (decreases (difference (disbanding_rate first_movers a) (disbanding_rate efficient_producers a))) True)) % 67.88/68.18 Clause #86 (by clausification #[18]): ∀ (a : Iota), % 67.88/68.18 Eq % 67.88/68.18 (∀ (T1 T2 T : Iota), % 67.88/68.18 And % 67.88/68.18 (And % 67.88/68.18 (And (And (environment a) (subpopulations first_movers efficient_producers a T1)) % 67.88/68.18 (subpopulations first_movers efficient_producers a T2)) % 67.88/68.18 (greater_or_equal T T1)) % 67.88/68.18 (greater_or_equal T2 T) → % 67.88/68.18 subpopulations first_movers efficient_producers a T) % 67.88/68.18 True % 67.88/68.18 Clause #87 (by clausification #[86]): ∀ (a a_1 : Iota), % 67.88/68.18 Eq % 67.88/68.18 (∀ (T2 T : Iota), % 67.88/68.18 And % 67.88/68.18 (And % 67.88/68.18 (And (And (environment a) (subpopulations first_movers efficient_producers a a_1)) % 67.88/68.18 (subpopulations first_movers efficient_producers a T2)) % 67.88/68.18 (greater_or_equal T a_1)) % 67.88/68.18 (greater_or_equal T2 T) → % 67.88/68.18 subpopulations first_movers efficient_producers a T) % 67.88/68.18 True % 67.88/68.18 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 : Iota), % 67.88/68.18 Eq % 67.88/68.18 (∀ (T : Iota), % 67.88/68.18 And % 67.88/68.18 (And % 67.88/68.18 (And (And (environment a) (subpopulations first_movers efficient_producers a a_1)) % 67.88/68.18 (subpopulations first_movers efficient_producers a a_2)) % 67.88/68.18 (greater_or_equal T a_1)) % 67.88/68.18 (greater_or_equal a_2 T) → % 67.88/68.18 subpopulations first_movers efficient_producers a T) % 67.88/68.18 True % 67.88/68.18 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 : Iota), % 67.88/68.18 Eq % 67.88/68.18 (And % 67.88/68.18 (And % 67.88/68.18 (And (And (environment a) (subpopulations first_movers efficient_producers a a_1)) % 67.88/68.18 (subpopulations first_movers efficient_producers a a_2)) % 67.88/68.18 (greater_or_equal a_3 a_1)) % 67.88/68.18 (greater_or_equal a_2 a_3) → % 67.88/68.18 subpopulations first_movers efficient_producers a a_3) % 67.88/68.18 True % 67.88/68.18 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 : Iota), % 67.88/68.18 Or % 67.88/68.18 (Eq % 67.88/68.18 (And % 67.88/68.18 (And % 67.88/68.18 (And (And (environment a) (subpopulations first_movers efficient_producers a a_1)) % 67.88/68.18 (subpopulations first_movers efficient_producers a a_2)) % 67.88/68.18 (greater_or_equal a_3 a_1)) % 67.88/68.18 (greater_or_equal a_2 a_3)) % 67.88/68.18 False) % 67.88/68.18 (Eq (subpopulations first_movers efficient_producers a a_3) True) % 67.88/68.18 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 a_3 : Iota), % 67.88/68.18 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 67.88/68.18 (Or % 67.88/68.18 (Eq % 67.88/68.18 (And % 67.88/68.18 (And (And (environment a) (subpopulations first_movers efficient_producers a a_2)) % 67.88/68.18 (subpopulations first_movers efficient_producers a a_3)) % 67.88/68.18 (greater_or_equal a_1 a_2)) % 67.88/68.18 False) % 67.88/68.18 (Eq (greater_or_equal a_3 a_1) False)) % 67.88/68.18 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 a_3 : Iota), % 67.88/68.18 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 67.88/68.18 (Or (Eq (greater_or_equal a_2 a_1) False) % 67.88/68.18 (Or % 67.88/68.18 (Eq % 67.88/68.18 (And (And (environment a) (subpopulations first_movers efficient_producers a a_3)) % 67.88/68.18 (subpopulations first_movers efficient_producers a a_2)) % 67.88/68.18 False) % 67.88/68.18 (Eq (greater_or_equal a_1 a_3) False))) % 67.88/68.18 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 a_3 : Iota), % 67.88/68.18 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 67.95/68.21 (Or (Eq (greater_or_equal a_2 a_1) False) % 67.95/68.21 (Or (Eq (greater_or_equal a_1 a_3) False) % 67.95/68.21 (Or (Eq (And (environment a) (subpopulations first_movers efficient_producers a a_3)) False) % 67.95/68.21 (Eq (subpopulations first_movers efficient_producers a a_2) False)))) % 67.95/68.21 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 a_3 : Iota), % 67.95/68.21 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 67.95/68.21 (Or (Eq (greater_or_equal a_2 a_1) False) % 67.95/68.21 (Or (Eq (greater_or_equal a_1 a_3) False) % 67.95/68.21 (Or (Eq (subpopulations first_movers efficient_producers a a_2) False) % 67.95/68.21 (Or (Eq (environment a) False) (Eq (subpopulations first_movers efficient_producers a a_3) False))))) % 67.95/68.21 Clause #95 (by clausification #[19]): ∀ (a : Iota), % 67.95/68.21 Eq % 67.95/68.21 (∀ (T : Iota), % 67.95/68.21 And (environment a) (subpopulations first_movers efficient_producers a T) → % 67.95/68.21 decreases (difference (founding_rate first_movers T) (founding_rate efficient_producers T))) % 67.95/68.21 True % 67.95/68.21 Clause #96 (by clausification #[95]): ∀ (a a_1 : Iota), % 67.95/68.21 Eq % 67.95/68.21 (And (environment a) (subpopulations first_movers efficient_producers a a_1) → % 67.95/68.21 decreases (difference (founding_rate first_movers a_1) (founding_rate efficient_producers a_1))) % 67.95/68.21 True % 67.95/68.21 Clause #97 (by clausification #[96]): ∀ (a a_1 : Iota), % 67.95/68.21 Or (Eq (And (environment a) (subpopulations first_movers efficient_producers a a_1)) False) % 67.95/68.21 (Eq (decreases (difference (founding_rate first_movers a_1) (founding_rate efficient_producers a_1))) True) % 67.95/68.21 Clause #98 (by clausification #[97]): ∀ (a a_1 : Iota), % 67.95/68.21 Or (Eq (decreases (difference (founding_rate first_movers a) (founding_rate efficient_producers a))) True) % 67.95/68.21 (Or (Eq (environment a_1) False) (Eq (subpopulations first_movers efficient_producers a_1 a) False)) % 67.95/68.21 Clause #99 (by clausification #[16]): ∀ (a : Iota), % 67.95/68.21 Eq % 67.95/68.21 (∀ (T : Iota), % 67.95/68.21 And (And (environment a) (subpopulations first_movers efficient_producers a T)) % 67.95/68.21 (Not (greater zero (difference (growth_rate first_movers T) (growth_rate efficient_producers T)))) → % 67.95/68.21 greater_or_equal (difference (growth_rate first_movers T) (growth_rate efficient_producers T)) zero) % 67.95/68.21 True % 67.95/68.21 Clause #100 (by clausification #[99]): ∀ (a a_1 : Iota), % 67.95/68.21 Eq % 67.95/68.21 (And (And (environment a) (subpopulations first_movers efficient_producers a a_1)) % 67.95/68.21 (Not (greater zero (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)))) → % 67.95/68.21 greater_or_equal (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)) zero) % 67.95/68.21 True % 67.95/68.21 Clause #101 (by clausification #[100]): ∀ (a a_1 : Iota), % 67.95/68.21 Or % 67.95/68.21 (Eq % 67.95/68.21 (And (And (environment a) (subpopulations first_movers efficient_producers a a_1)) % 67.95/68.21 (Not (greater zero (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1))))) % 67.95/68.21 False) % 67.95/68.21 (Eq (greater_or_equal (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)) zero) True) % 67.95/68.21 Clause #102 (by clausification #[101]): ∀ (a a_1 : Iota), % 67.95/68.21 Or (Eq (greater_or_equal (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) True) % 67.95/68.21 (Or (Eq (And (environment a_1) (subpopulations first_movers efficient_producers a_1 a)) False) % 67.95/68.21 (Eq (Not (greater zero (difference (growth_rate first_movers a) (growth_rate efficient_producers a)))) False)) % 67.95/68.21 Clause #103 (by clausification #[102]): ∀ (a a_1 : Iota), % 67.95/68.21 Or (Eq (greater_or_equal (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) True) % 67.95/68.21 (Or (Eq (Not (greater zero (difference (growth_rate first_movers a) (growth_rate efficient_producers a)))) False) % 67.95/68.21 (Or (Eq (environment a_1) False) (Eq (subpopulations first_movers efficient_producers a_1 a) False))) % 67.95/68.21 Clause #104 (by clausification #[103]): ∀ (a a_1 : Iota), % 67.95/68.21 Or (Eq (greater_or_equal (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) True) % 67.95/68.21 (Or (Eq (environment a_1) False) % 67.95/68.21 (Or (Eq (subpopulations first_movers efficient_producers a_1 a) False) % 67.95/68.25 (Eq (greater zero (difference (growth_rate first_movers a) (growth_rate efficient_producers a))) True))) % 67.95/68.25 Clause #105 (by clausification #[5]): ∀ (a : Iota), % 67.95/68.25 Eq % 67.95/68.25 (∀ (T To : Iota), % 67.95/68.25 And % 67.95/68.25 (And % 67.95/68.25 (And (And (environment a) (in_environment a To)) % 67.95/68.25 (greater_or_equal (difference (growth_rate first_movers To) (growth_rate efficient_producers To)) zero)) % 67.95/68.25 (greater_or_equal T (appear efficient_producers a))) % 67.95/68.25 (greater To T) → % 67.95/68.25 decreases (difference (growth_rate first_movers T) (growth_rate efficient_producers T)) → % 67.95/68.25 greater (difference (growth_rate first_movers T) (growth_rate efficient_producers T)) zero) % 67.95/68.25 True % 67.95/68.25 Clause #106 (by clausification #[105]): ∀ (a a_1 : Iota), % 67.95/68.25 Eq % 67.95/68.25 (∀ (To : Iota), % 67.95/68.25 And % 67.95/68.25 (And % 67.95/68.25 (And (And (environment a) (in_environment a To)) % 67.95/68.25 (greater_or_equal (difference (growth_rate first_movers To) (growth_rate efficient_producers To)) zero)) % 67.95/68.25 (greater_or_equal a_1 (appear efficient_producers a))) % 67.95/68.25 (greater To a_1) → % 67.95/68.25 decreases (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)) → % 67.95/68.25 greater (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)) zero) % 67.95/68.25 True % 67.95/68.25 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 67.95/68.25 Eq % 67.95/68.25 (And % 67.95/68.25 (And % 67.95/68.25 (And (And (environment a) (in_environment a a_1)) % 67.95/68.25 (greater_or_equal (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)) zero)) % 67.95/68.25 (greater_or_equal a_2 (appear efficient_producers a))) % 67.95/68.25 (greater a_1 a_2) → % 67.95/68.25 decreases (difference (growth_rate first_movers a_2) (growth_rate efficient_producers a_2)) → % 67.95/68.25 greater (difference (growth_rate first_movers a_2) (growth_rate efficient_producers a_2)) zero) % 67.95/68.25 True % 67.95/68.25 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 67.95/68.25 Or % 67.95/68.25 (Eq % 67.95/68.25 (And % 67.95/68.25 (And % 67.95/68.25 (And (And (environment a) (in_environment a a_1)) % 67.95/68.25 (greater_or_equal (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)) zero)) % 67.95/68.25 (greater_or_equal a_2 (appear efficient_producers a))) % 67.95/68.25 (greater a_1 a_2)) % 67.95/68.25 False) % 67.95/68.25 (Eq % 67.95/68.25 (decreases (difference (growth_rate first_movers a_2) (growth_rate efficient_producers a_2)) → % 67.95/68.25 greater (difference (growth_rate first_movers a_2) (growth_rate efficient_producers a_2)) zero) % 67.95/68.25 True) % 67.95/68.25 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 : Iota), % 67.95/68.25 Or % 67.95/68.25 (Eq % 67.95/68.25 (decreases (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) → % 67.95/68.25 greater (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) % 67.95/68.25 True) % 67.95/68.25 (Or % 67.95/68.25 (Eq % 67.95/68.25 (And % 67.95/68.25 (And (And (environment a_1) (in_environment a_1 a_2)) % 67.95/68.25 (greater_or_equal (difference (growth_rate first_movers a_2) (growth_rate efficient_producers a_2)) zero)) % 67.95/68.25 (greater_or_equal a (appear efficient_producers a_1))) % 67.95/68.25 False) % 67.95/68.25 (Eq (greater a_2 a) False)) % 67.95/68.25 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 : Iota), % 67.95/68.25 Or % 67.95/68.25 (Eq % 67.95/68.25 (And % 67.95/68.25 (And (And (environment a) (in_environment a a_1)) % 67.95/68.25 (greater_or_equal (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)) zero)) % 67.95/68.25 (greater_or_equal a_2 (appear efficient_producers a))) % 67.95/68.25 False) % 67.95/68.25 (Or (Eq (greater a_1 a_2) False) % 67.95/68.25 (Or (Eq (decreases (difference (growth_rate first_movers a_2) (growth_rate efficient_producers a_2))) False) % 67.95/68.25 (Eq (greater (difference (growth_rate first_movers a_2) (growth_rate efficient_producers a_2)) zero) True))) % 67.95/68.25 Clause #111 (by clausification #[110]): ∀ (a a_1 a_2 : Iota), % 67.95/68.25 Or (Eq (greater a a_1) False) % 67.95/68.25 (Or (Eq (decreases (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1))) False) % 67.95/68.25 (Or (Eq (greater (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)) zero) True) % 67.95/68.25 (Or % 67.95/68.25 (Eq % 67.95/68.25 (And (And (environment a_2) (in_environment a_2 a)) % 67.95/68.29 (greater_or_equal (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero)) % 67.95/68.29 False) % 67.95/68.29 (Eq (greater_or_equal a_1 (appear efficient_producers a_2)) False)))) % 67.95/68.29 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 : Iota), % 67.95/68.29 Or (Eq (greater a a_1) False) % 67.95/68.29 (Or (Eq (decreases (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1))) False) % 67.95/68.29 (Or (Eq (greater (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)) zero) True) % 67.95/68.29 (Or (Eq (greater_or_equal a_1 (appear efficient_producers a_2)) False) % 67.95/68.29 (Or (Eq (And (environment a_2) (in_environment a_2 a)) False) % 67.95/68.29 (Eq (greater_or_equal (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) % 67.95/68.29 False))))) % 67.95/68.29 Clause #113 (by clausification #[112]): ∀ (a a_1 a_2 : Iota), % 67.95/68.29 Or (Eq (greater a a_1) False) % 67.95/68.29 (Or (Eq (decreases (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1))) False) % 67.95/68.29 (Or (Eq (greater (difference (growth_rate first_movers a_1) (growth_rate efficient_producers a_1)) zero) True) % 67.95/68.29 (Or (Eq (greater_or_equal a_1 (appear efficient_producers a_2)) False) % 67.95/68.29 (Or % 67.95/68.29 (Eq (greater_or_equal (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) % 67.95/68.29 False) % 67.95/68.29 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 a) False)))))) % 67.95/68.29 Clause #114 (by superposition #[113, 47]): ∀ (a a_1 a_2 : Iota), % 67.95/68.29 Or % 67.95/68.29 (Eq % 67.95/68.29 (decreases % 67.95/68.29 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 67.95/68.29 False) % 67.95/68.29 (Or % 67.95/68.29 (Eq % 67.95/68.29 (greater % 67.95/68.29 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 67.95/68.29 zero) % 67.95/68.29 True) % 67.95/68.29 (Or (Eq (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers a_2)) False) % 67.95/68.29 (Or % 67.95/68.29 (Eq % 67.95/68.29 (greater_or_equal % 67.95/68.29 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 67.95/68.29 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 67.95/68.29 zero) % 67.95/68.29 False) % 67.95/68.29 (Or (Eq (environment a_2) False) % 67.95/68.29 (Or (Eq (in_environment a_2 (critical_point (skS.0 0 a))) False) (Eq False True)))))) % 67.95/68.29 Clause #115 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (greater_or_equal a Y) (Or (greater a Y) (Eq a Y))) True % 67.95/68.29 Clause #116 (by clausification #[115]): ∀ (a a_1 : Iota), Eq (Iff (greater_or_equal a a_1) (Or (greater a a_1) (Eq a a_1))) True % 67.95/68.29 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (Or (greater a a_1) (Eq a a_1)) False) % 67.95/68.29 Clause #118 (by clausification #[116]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Eq (Or (greater a a_1) (Eq a a_1)) True) % 67.95/68.29 Clause #119 (by clausification #[117]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (Eq a a_1) False) % 67.95/68.29 Clause #120 (by clausification #[117]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (greater a a_1) False) % 67.95/68.29 Clause #121 (by clausification #[119]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Ne a a_1) % 67.95/68.29 Clause #122 (by destructive equality resolution #[121]): ∀ (a : Iota), Eq (greater_or_equal a a) True % 67.95/68.29 Clause #125 (by superposition #[120, 47]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal (critical_point (skS.0 0 a)) (skS.0 1 a a_1)) True) (Eq False True) % 67.95/68.29 Clause #126 (by clausification #[118]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Or (Eq (greater a a_1) True) (Eq (Eq a a_1) True)) % 67.95/68.29 Clause #127 (by clausification #[126]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Or (Eq (greater a a_1) True) (Eq a a_1)) % 67.95/68.29 Clause #130 (by clausification #[7]): ∀ (a : Iota), % 67.95/68.29 Eq % 67.95/68.29 (Iff (greater (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) % 67.95/68.29 (greater (growth_rate first_movers a) (growth_rate efficient_producers a))) % 68.05/68.33 True % 68.05/68.33 Clause #131 (by clausification #[130]): ∀ (a : Iota), % 68.05/68.33 Or (Eq (greater (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) True) % 68.05/68.33 (Eq (greater (growth_rate first_movers a) (growth_rate efficient_producers a)) False) % 68.05/68.33 Clause #132 (by clausification #[130]): ∀ (a : Iota), % 68.05/68.33 Or (Eq (greater (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) False) % 68.05/68.33 (Eq (greater (growth_rate first_movers a) (growth_rate efficient_producers a)) True) % 68.05/68.33 Clause #133 (by clausification #[6]): ∀ (a : Iota), % 68.05/68.33 Eq % 68.05/68.33 (Iff (greater zero (difference (growth_rate first_movers a) (growth_rate efficient_producers a))) % 68.05/68.33 (greater (growth_rate efficient_producers a) (growth_rate first_movers a))) % 68.05/68.33 True % 68.05/68.33 Clause #135 (by clausification #[133]): ∀ (a : Iota), % 68.05/68.33 Or (Eq (greater zero (difference (growth_rate first_movers a) (growth_rate efficient_producers a))) False) % 68.05/68.33 (Eq (greater (growth_rate efficient_producers a) (growth_rate first_movers a)) True) % 68.05/68.33 Clause #136 (by clausification #[125]): ∀ (a a_1 : Iota), Eq (greater_or_equal (critical_point (skS.0 0 a)) (skS.0 1 a a_1)) True % 68.05/68.33 Clause #138 (by superposition #[136, 94]): ∀ (a a_1 a_2 a_3 : Iota), % 68.05/68.33 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 1 a_1 a_2)) True) % 68.05/68.33 (Or (Eq True False) % 68.05/68.33 (Or (Eq (greater_or_equal (skS.0 1 a_1 a_2) a_3) False) % 68.05/68.33 (Or (Eq (subpopulations first_movers efficient_producers a (critical_point (skS.0 0 a_1))) False) % 68.05/68.33 (Or (Eq (environment a) False) (Eq (subpopulations first_movers efficient_producers a a_3) False))))) % 68.05/68.33 Clause #141 (by clausification #[17]): ∀ (a : Iota), % 68.05/68.33 Eq % 68.05/68.33 (∀ (Tc : Iota), % 68.05/68.33 And (environment a) (Eq Tc (critical_point a)) → % 68.05/68.33 And (Not (greater (growth_rate efficient_producers Tc) (growth_rate first_movers Tc))) % 68.05/68.33 (∀ (T : Iota), % 68.05/68.33 And (subpopulations first_movers efficient_producers a T) (greater T Tc) → % 68.05/68.33 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 68.05/68.33 True % 68.05/68.33 Clause #142 (by clausification #[141]): ∀ (a a_1 : Iota), % 68.05/68.33 Eq % 68.05/68.33 (And (environment a) (Eq a_1 (critical_point a)) → % 68.05/68.33 And (Not (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1))) % 68.05/68.33 (∀ (T : Iota), % 68.05/68.33 And (subpopulations first_movers efficient_producers a T) (greater T a_1) → % 68.05/68.33 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 68.05/68.33 True % 68.05/68.33 Clause #143 (by clausification #[142]): ∀ (a a_1 : Iota), % 68.05/68.33 Or (Eq (And (environment a) (Eq a_1 (critical_point a))) False) % 68.05/68.33 (Eq % 68.05/68.33 (And (Not (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1))) % 68.05/68.33 (∀ (T : Iota), % 68.05/68.33 And (subpopulations first_movers efficient_producers a T) (greater T a_1) → % 68.05/68.33 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 68.05/68.33 True) % 68.05/68.33 Clause #144 (by clausification #[143]): ∀ (a a_1 : Iota), % 68.05/68.33 Or % 68.05/68.33 (Eq % 68.05/68.33 (And (Not (greater (growth_rate efficient_producers a) (growth_rate first_movers a))) % 68.05/68.33 (∀ (T : Iota), % 68.05/68.33 And (subpopulations first_movers efficient_producers a_1 T) (greater T a) → % 68.05/68.33 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 68.05/68.33 True) % 68.05/68.33 (Or (Eq (environment a_1) False) (Eq (Eq a (critical_point a_1)) False)) % 68.05/68.33 Clause #146 (by clausification #[144]): ∀ (a a_1 : Iota), % 68.05/68.33 Or (Eq (environment a) False) % 68.05/68.33 (Or (Eq (Eq a_1 (critical_point a)) False) % 68.05/68.33 (Eq (Not (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1))) True)) % 68.05/68.33 Clause #152 (by clausification #[48]): ∀ (a a_1 : Iota), Eq (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers (skS.0 0 a))) True % 68.05/68.33 Clause #153 (by clausification #[48]): ∀ (a : Iota), Eq (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (critical_point (skS.0 0 a)))) True % 68.05/68.33 Clause #157 (by clausification #[146]): ∀ (a a_1 : Iota), % 68.05/68.33 Or (Eq (environment a) False) % 68.05/68.33 (Or (Eq (Not (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1))) True) % 68.05/68.38 (Ne a_1 (critical_point a))) % 68.05/68.38 Clause #158 (by clausification #[157]): ∀ (a a_1 : Iota), % 68.05/68.38 Or (Eq (environment a) False) % 68.05/68.38 (Or (Ne a_1 (critical_point a)) % 68.05/68.38 (Eq (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1)) False)) % 68.05/68.38 Clause #159 (by destructive equality resolution #[158]): ∀ (a : Iota), % 68.05/68.38 Or (Eq (environment a) False) % 68.05/68.38 (Eq (greater (growth_rate efficient_producers (critical_point a)) (growth_rate first_movers (critical_point a))) % 68.05/68.38 False) % 68.05/68.38 Clause #160 (by clausification #[153]): ∀ (a : Iota), Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) True % 68.05/68.38 Clause #161 (by clausification #[153]): ∀ (a : Iota), Eq (environment (skS.0 0 a)) True % 68.05/68.38 Clause #164 (by superposition #[161, 59]): ∀ (a : Iota), % 68.05/68.38 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (critical_point (skS.0 0 a))) True) % 68.05/68.38 (Or (Eq True False) (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False)) % 68.05/68.38 Clause #165 (by superposition #[161, 63]): ∀ (a a_1 : Iota), % 68.05/68.38 Or (Eq (greater_or_equal a (appear efficient_producers (skS.0 0 a_1))) True) % 68.05/68.38 (Or (Eq True False) (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) a) False)) % 68.05/68.38 Clause #166 (by superposition #[161, 67]): ∀ (a a_1 : Iota), % 68.05/68.38 Or (Eq (subpopulations efficient_producers first_movers (skS.0 0 a) a_1) True) % 68.05/68.38 (Or (Eq True False) (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False)) % 68.05/68.38 Clause #167 (by superposition #[161, 76]): ∀ (a : Iota), % 68.05/68.38 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.05/68.38 (Or (Eq True False) (Eq (in_environment (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) False)) % 68.05/68.38 Clause #168 (by superposition #[161, 81]): ∀ (a a_1 : Iota), % 68.05/68.38 Or (Eq True False) % 68.05/68.38 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 68.05/68.38 (Eq (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) False)) % 68.05/68.38 Clause #169 (by superposition #[161, 98]): ∀ (a a_1 : Iota), % 68.05/68.38 Or (Eq (decreases (difference (founding_rate first_movers a) (founding_rate efficient_producers a))) True) % 68.05/68.38 (Or (Eq True False) (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) a) False)) % 68.05/68.38 Clause #170 (by superposition #[161, 104]): ∀ (a a_1 : Iota), % 68.05/68.38 Or (Eq (greater_or_equal (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) True) % 68.05/68.38 (Or (Eq True False) % 68.05/68.38 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) a) False) % 68.05/68.38 (Eq (greater zero (difference (growth_rate first_movers a) (growth_rate efficient_producers a))) True))) % 68.05/68.38 Clause #172 (by superposition #[161, 159]): ∀ (a : Iota), % 68.05/68.38 Or (Eq True False) % 68.05/68.38 (Eq % 68.05/68.38 (greater (growth_rate efficient_producers (critical_point (skS.0 0 a))) % 68.05/68.38 (growth_rate first_movers (critical_point (skS.0 0 a)))) % 68.05/68.38 False) % 68.05/68.38 Clause #186 (by clausification #[172]): ∀ (a : Iota), % 68.05/68.38 Eq % 68.05/68.38 (greater (growth_rate efficient_producers (critical_point (skS.0 0 a))) % 68.05/68.38 (growth_rate first_movers (critical_point (skS.0 0 a)))) % 68.05/68.38 False % 68.05/68.38 Clause #187 (by clausification #[169]): ∀ (a a_1 : Iota), % 68.05/68.38 Or (Eq (decreases (difference (founding_rate first_movers a) (founding_rate efficient_producers a))) True) % 68.05/68.38 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) a) False) % 68.05/68.38 Clause #188 (by clausification #[168]): ∀ (a a_1 : Iota), % 68.05/68.38 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 68.05/68.38 (Eq (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) False) % 68.05/68.38 Clause #189 (by clausification #[114]): ∀ (a a_1 a_2 : Iota), % 68.05/68.38 Or % 68.05/68.38 (Eq % 68.05/68.38 (decreases % 68.05/68.38 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 68.05/68.38 False) % 68.05/68.38 (Or % 68.05/68.38 (Eq % 68.05/68.38 (greater % 68.05/68.38 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.15/68.42 zero) % 68.15/68.42 True) % 68.15/68.42 (Or (Eq (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers a_2)) False) % 68.15/68.42 (Or % 68.15/68.42 (Eq % 68.15/68.42 (greater_or_equal % 68.15/68.42 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.15/68.42 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.15/68.42 zero) % 68.15/68.42 False) % 68.15/68.42 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (critical_point (skS.0 0 a))) False))))) % 68.15/68.42 Clause #190 (by clausification #[165]): ∀ (a a_1 : Iota), % 68.15/68.42 Or (Eq (greater_or_equal a (appear efficient_producers (skS.0 0 a_1))) True) % 68.15/68.42 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) a) False) % 68.15/68.42 Clause #191 (by clausification #[166]): ∀ (a a_1 : Iota), % 68.15/68.42 Or (Eq (subpopulations efficient_producers first_movers (skS.0 0 a) a_1) True) % 68.15/68.42 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 68.15/68.42 Clause #194 (by clausification #[170]): ∀ (a a_1 : Iota), % 68.15/68.42 Or (Eq (greater_or_equal (difference (growth_rate first_movers a) (growth_rate efficient_producers a)) zero) True) % 68.15/68.42 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) a) False) % 68.15/68.42 (Eq (greater zero (difference (growth_rate first_movers a) (growth_rate efficient_producers a))) True)) % 68.15/68.42 Clause #201 (by clausification #[164]): ∀ (a : Iota), % 68.15/68.42 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (critical_point (skS.0 0 a))) True) % 68.15/68.42 (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False) % 68.15/68.42 Clause #202 (by forward demodulation #[201, 160]): ∀ (a : Iota), % 68.15/68.42 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (critical_point (skS.0 0 a))) True) % 68.15/68.42 (Eq True False) % 68.15/68.42 Clause #203 (by clausification #[202]): ∀ (a : Iota), Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (critical_point (skS.0 0 a))) True % 68.15/68.42 Clause #206 (by superposition #[203, 190]): ∀ (a : Iota), % 68.15/68.42 Or (Eq (greater_or_equal (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) True) (Eq True False) % 68.15/68.42 Clause #209 (by superposition #[203, 194]): ∀ (a : Iota), % 68.15/68.42 Or % 68.15/68.42 (Eq % 68.15/68.42 (greater_or_equal % 68.15/68.42 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.15/68.42 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.15/68.42 zero) % 68.15/68.42 True) % 68.15/68.42 (Or (Eq True False) % 68.15/68.42 (Eq % 68.15/68.42 (greater zero % 68.15/68.42 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.15/68.42 (growth_rate efficient_producers (critical_point (skS.0 0 a))))) % 68.15/68.42 True)) % 68.15/68.42 Clause #211 (by clausification #[206]): ∀ (a : Iota), Eq (greater_or_equal (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) True % 68.15/68.42 Clause #214 (by superposition #[211, 127]): ∀ (a : Iota), % 68.15/68.42 Or (Eq True False) % 68.15/68.42 (Or (Eq (greater (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) True) % 68.15/68.42 (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a)))) % 68.15/68.42 Clause #215 (by clausification #[138]): ∀ (a a_1 a_2 a_3 : Iota), % 68.15/68.42 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 1 a_1 a_2)) True) % 68.15/68.42 (Or (Eq (greater_or_equal (skS.0 1 a_1 a_2) a_3) False) % 68.15/68.42 (Or (Eq (subpopulations first_movers efficient_producers a (critical_point (skS.0 0 a_1))) False) % 68.15/68.42 (Or (Eq (environment a) False) (Eq (subpopulations first_movers efficient_producers a a_3) False)))) % 68.15/68.42 Clause #216 (by superposition #[215, 152]): ∀ (a a_1 a_2 : Iota), % 68.15/68.42 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 1 a_1 a_2)) True) % 68.15/68.42 (Or (Eq (subpopulations first_movers efficient_producers a (critical_point (skS.0 0 a_1))) False) % 68.15/68.42 (Or (Eq (environment a) False) % 68.15/68.42 (Or (Eq (subpopulations first_movers efficient_producers a (appear efficient_producers (skS.0 0 a_1))) False) % 68.15/68.42 (Eq False True)))) % 68.15/68.42 Clause #221 (by clausification #[214]): ∀ (a : Iota), % 68.15/68.42 Or (Eq (greater (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) True) % 68.15/68.42 (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.15/68.42 Clause #222 (by superposition #[221, 26]): ∀ (a : Iota), % 68.15/68.46 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.15/68.46 (Or (Eq (in_environment (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.15/68.46 (Or (Eq True False) % 68.15/68.46 (Or % 68.15/68.46 (Eq (greater_or_equal (appear efficient_producers (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.15/68.46 False) % 68.15/68.46 (Or (Eq (environment (skS.0 0 a)) False) % 68.15/68.46 (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False))))) % 68.15/68.46 Clause #231 (by clausification #[167]): ∀ (a : Iota), % 68.15/68.46 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.15/68.46 (Eq (in_environment (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) False) % 68.15/68.46 Clause #254 (by clausification #[216]): ∀ (a a_1 a_2 : Iota), % 68.15/68.46 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 1 a_1 a_2)) True) % 68.15/68.46 (Or (Eq (subpopulations first_movers efficient_producers a (critical_point (skS.0 0 a_1))) False) % 68.15/68.46 (Or (Eq (environment a) False) % 68.15/68.46 (Eq (subpopulations first_movers efficient_producers a (appear efficient_producers (skS.0 0 a_1))) False))) % 68.15/68.46 Clause #255 (by superposition #[254, 203]): ∀ (a a_1 : Iota), % 68.15/68.46 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) % 68.15/68.46 (Or (Eq (environment (skS.0 0 a)) False) % 68.15/68.46 (Or % 68.15/68.46 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) % 68.15/68.46 False) % 68.15/68.46 (Eq False True))) % 68.15/68.46 Clause #263 (by clausification #[209]): ∀ (a : Iota), % 68.15/68.46 Or % 68.15/68.46 (Eq % 68.15/68.46 (greater_or_equal % 68.15/68.46 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.15/68.46 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.15/68.46 zero) % 68.15/68.46 True) % 68.15/68.46 (Eq % 68.15/68.46 (greater zero % 68.15/68.46 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.15/68.46 (growth_rate efficient_producers (critical_point (skS.0 0 a))))) % 68.15/68.46 True) % 68.15/68.46 Clause #266 (by superposition #[263, 127]): ∀ (a : Iota), % 68.15/68.46 Or % 68.15/68.46 (Eq % 68.15/68.46 (greater zero % 68.15/68.46 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.15/68.46 (growth_rate efficient_producers (critical_point (skS.0 0 a))))) % 68.15/68.46 True) % 68.15/68.46 (Or (Eq True False) % 68.15/68.46 (Or % 68.15/68.46 (Eq % 68.15/68.46 (greater % 68.15/68.46 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.15/68.46 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.15/68.46 zero) % 68.15/68.46 True) % 68.15/68.46 (Eq % 68.15/68.46 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.15/68.46 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.15/68.46 zero))) % 68.15/68.46 Clause #270 (by clausification #[255]): ∀ (a a_1 : Iota), % 68.15/68.46 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) % 68.15/68.46 (Or (Eq (environment (skS.0 0 a)) False) % 68.15/68.46 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) False)) % 68.15/68.46 Clause #271 (by forward demodulation #[270, 161]): ∀ (a a_1 : Iota), % 68.15/68.46 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) % 68.15/68.46 (Or (Eq True False) % 68.15/68.46 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) False)) % 68.15/68.46 Clause #272 (by clausification #[271]): ∀ (a a_1 : Iota), % 68.15/68.46 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) % 68.15/68.46 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) False) % 68.15/68.46 Clause #273 (by clausification #[266]): ∀ (a : Iota), % 68.15/68.46 Or % 68.15/68.46 (Eq % 68.15/68.46 (greater zero % 68.15/68.46 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.15/68.46 (growth_rate efficient_producers (critical_point (skS.0 0 a))))) % 68.15/68.46 True) % 68.15/68.46 (Or % 68.15/68.46 (Eq % 68.15/68.46 (greater % 68.15/68.46 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.15/68.46 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.15/68.46 zero) % 68.15/68.46 True) % 68.15/68.46 (Eq % 68.15/68.46 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 zero)) % 68.25/68.50 Clause #274 (by superposition #[273, 132]): ∀ (a : Iota), % 68.25/68.50 Or % 68.25/68.50 (Eq % 68.25/68.50 (greater zero % 68.25/68.50 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a))))) % 68.25/68.50 True) % 68.25/68.50 (Or % 68.25/68.50 (Eq % 68.25/68.50 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 zero) % 68.25/68.50 (Or (Eq True False) % 68.25/68.50 (Eq % 68.25/68.50 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 True))) % 68.25/68.50 Clause #277 (by clausification #[274]): ∀ (a : Iota), % 68.25/68.50 Or % 68.25/68.50 (Eq % 68.25/68.50 (greater zero % 68.25/68.50 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a))))) % 68.25/68.50 True) % 68.25/68.50 (Or % 68.25/68.50 (Eq % 68.25/68.50 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 zero) % 68.25/68.50 (Eq % 68.25/68.50 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 True)) % 68.25/68.50 Clause #278 (by superposition #[277, 135]): ∀ (a : Iota), % 68.25/68.50 Or % 68.25/68.50 (Eq % 68.25/68.50 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 zero) % 68.25/68.50 (Or % 68.25/68.50 (Eq % 68.25/68.50 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 True) % 68.25/68.50 (Or (Eq True False) % 68.25/68.50 (Eq % 68.25/68.50 (greater (growth_rate efficient_producers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate first_movers (critical_point (skS.0 0 a)))) % 68.25/68.50 True))) % 68.25/68.50 Clause #281 (by clausification #[278]): ∀ (a : Iota), % 68.25/68.50 Or % 68.25/68.50 (Eq % 68.25/68.50 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 zero) % 68.25/68.50 (Or % 68.25/68.50 (Eq % 68.25/68.50 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 True) % 68.25/68.50 (Eq % 68.25/68.50 (greater (growth_rate efficient_producers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate first_movers (critical_point (skS.0 0 a)))) % 68.25/68.50 True)) % 68.25/68.50 Clause #282 (by forward demodulation #[281, 186]): ∀ (a : Iota), % 68.25/68.50 Or % 68.25/68.50 (Eq % 68.25/68.50 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 zero) % 68.25/68.50 (Or % 68.25/68.50 (Eq % 68.25/68.50 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 True) % 68.25/68.50 (Eq False True)) % 68.25/68.50 Clause #283 (by clausification #[282]): ∀ (a : Iota), % 68.25/68.50 Or % 68.25/68.50 (Eq % 68.25/68.50 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 zero) % 68.25/68.50 (Eq % 68.25/68.50 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.50 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.50 True) % 68.25/68.50 Clause #288 (by clausification #[222]): ∀ (a : Iota), % 68.25/68.50 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.50 (Or (Eq (in_environment (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.25/68.50 (Or % 68.25/68.50 (Eq (greater_or_equal (appear efficient_producers (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) False) % 68.25/68.50 (Or (Eq (environment (skS.0 0 a)) False) (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False)))) % 68.25/68.50 Clause #289 (by forward demodulation #[288, 161]): ∀ (a : Iota), % 68.25/68.50 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.50 (Or (Eq (in_environment (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.25/68.55 (Or % 68.25/68.55 (Eq (greater_or_equal (appear efficient_producers (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) False) % 68.25/68.55 (Or (Eq True False) (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False)))) % 68.25/68.55 Clause #290 (by clausification #[289]): ∀ (a : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Or (Eq (in_environment (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.25/68.55 (Or % 68.25/68.55 (Eq (greater_or_equal (appear efficient_producers (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) False) % 68.25/68.55 (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False))) % 68.25/68.55 Clause #291 (by forward demodulation #[290, 160]): ∀ (a : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Or (Eq (in_environment (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.25/68.55 (Or % 68.25/68.55 (Eq (greater_or_equal (appear efficient_producers (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) False) % 68.25/68.55 (Eq True False))) % 68.25/68.55 Clause #292 (by clausification #[291]): ∀ (a : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Or (Eq (in_environment (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.25/68.55 (Eq (greater_or_equal (appear efficient_producers (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) False)) % 68.25/68.55 Clause #293 (by superposition #[292, 122]): ∀ (a : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Or (Eq (in_environment (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) (Eq False True)) % 68.25/68.55 Clause #318 (by clausification #[293]): ∀ (a : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Eq (in_environment (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.25/68.55 Clause #319 (by superposition #[318, 231]): ∀ (a : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.25/68.55 (Eq True False)) % 68.25/68.55 Clause #324 (by clausification #[319]): ∀ (a : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (appear efficient_producers (skS.0 0 a))) True) % 68.25/68.55 Clause #325 (by superposition #[324, 272]): ∀ (a a_1 : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq True False)) % 68.25/68.55 Clause #337 (by clausification #[325]): ∀ (a a_1 : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) % 68.25/68.55 Clause #338 (by superposition #[337, 187]): ∀ (a a_1 : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Or % 68.25/68.55 (Eq % 68.25/68.55 (decreases % 68.25/68.55 (difference (founding_rate first_movers (skS.0 1 a a_1)) (founding_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.55 True) % 68.25/68.55 (Eq True False)) % 68.25/68.55 Clause #339 (by superposition #[337, 188]): ∀ (a a_1 : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Or (Eq True False) % 68.25/68.55 (Eq % 68.25/68.55 (decreases % 68.25/68.55 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 68.25/68.55 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.55 False)) % 68.25/68.55 Clause #341 (by superposition #[337, 191]): ∀ (a a_1 : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Or (Eq (subpopulations efficient_producers first_movers (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq True False)) % 68.25/68.55 Clause #344 (by clausification #[341]): ∀ (a a_1 : Iota), % 68.25/68.55 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.55 (Eq (subpopulations efficient_producers first_movers (skS.0 0 a) (skS.0 1 a a_1)) True) % 68.25/68.59 Clause #351 (by clausification #[339]): ∀ (a a_1 : Iota), % 68.25/68.59 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.59 (Eq % 68.25/68.59 (decreases % 68.25/68.59 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 68.25/68.59 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.59 False) % 68.25/68.59 Clause #352 (by clausification #[338]): ∀ (a a_1 : Iota), % 68.25/68.59 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.59 (Eq % 68.25/68.59 (decreases % 68.25/68.59 (difference (founding_rate first_movers (skS.0 1 a a_1)) (founding_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.59 True) % 68.25/68.59 Clause #353 (by superposition #[352, 85]): ∀ (a a_1 : Iota), % 68.25/68.59 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.59 (Or % 68.25/68.59 (Eq % 68.25/68.59 (decreases % 68.25/68.59 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.59 True) % 68.25/68.59 (Or (Eq True False) % 68.25/68.59 (Eq % 68.25/68.59 (decreases % 68.25/68.59 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 68.25/68.59 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.59 True))) % 68.25/68.59 Clause #376 (by clausification #[353]): ∀ (a a_1 : Iota), % 68.25/68.59 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.59 (Or % 68.25/68.59 (Eq % 68.25/68.59 (decreases % 68.25/68.59 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.59 True) % 68.25/68.59 (Eq % 68.25/68.59 (decreases % 68.25/68.59 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 68.25/68.59 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.59 True)) % 68.25/68.59 Clause #377 (by superposition #[376, 351]): ∀ (a a_1 : Iota), % 68.25/68.59 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.59 (Or % 68.25/68.59 (Eq % 68.25/68.59 (decreases % 68.25/68.59 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.59 True) % 68.25/68.59 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) (Eq True False))) % 68.25/68.59 Clause #378 (by clausification #[377]): ∀ (a a_1 : Iota), % 68.25/68.59 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.59 (Or % 68.25/68.59 (Eq % 68.25/68.59 (decreases % 68.25/68.59 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.59 True) % 68.25/68.59 (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a)))) % 68.25/68.59 Clause #379 (by eliminate duplicate literals #[378]): ∀ (a a_1 : Iota), % 68.25/68.59 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.59 (Eq % 68.25/68.59 (decreases % 68.25/68.59 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 68.25/68.59 True) % 68.25/68.59 Clause #380 (by superposition #[379, 189]): ∀ (a a_1 a_2 : Iota), % 68.25/68.59 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.59 (Or (Eq True False) % 68.25/68.59 (Or % 68.25/68.59 (Eq % 68.25/68.59 (greater % 68.25/68.59 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.25/68.59 zero) % 68.25/68.59 True) % 68.25/68.59 (Or (Eq (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers a_2)) False) % 68.25/68.59 (Or % 68.25/68.59 (Eq % 68.25/68.59 (greater_or_equal % 68.25/68.59 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.25/68.59 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.25/68.59 zero) % 68.25/68.59 False) % 68.25/68.59 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (critical_point (skS.0 0 a))) False)))))) % 68.25/68.59 Clause #429 (by clausification #[380]): ∀ (a a_1 a_2 : Iota), % 68.25/68.59 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.25/68.59 (Or % 68.25/68.59 (Eq % 68.25/68.59 (greater % 68.25/68.59 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.25/68.59 zero) % 68.25/68.59 True) % 68.25/68.59 (Or (Eq (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers a_2)) False) % 68.25/68.59 (Or % 68.25/68.59 (Eq % 68.25/68.59 (greater_or_equal % 68.25/68.59 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.63 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.63 zero) % 68.35/68.63 False) % 68.35/68.63 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (critical_point (skS.0 0 a))) False))))) % 68.35/68.63 Clause #430 (by superposition #[429, 152]): ∀ (a a_1 : Iota), % 68.35/68.63 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater % 68.35/68.63 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.35/68.63 zero) % 68.35/68.63 True) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater_or_equal % 68.35/68.63 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.63 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.63 zero) % 68.35/68.63 False) % 68.35/68.63 (Or (Eq (environment (skS.0 0 a)) False) % 68.35/68.63 (Or (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False) (Eq False True))))) % 68.35/68.63 Clause #639 (by clausification #[430]): ∀ (a a_1 : Iota), % 68.35/68.63 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater % 68.35/68.63 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.35/68.63 zero) % 68.35/68.63 True) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater_or_equal % 68.35/68.63 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.63 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.63 zero) % 68.35/68.63 False) % 68.35/68.63 (Or (Eq (environment (skS.0 0 a)) False) (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False)))) % 68.35/68.63 Clause #640 (by forward demodulation #[639, 161]): ∀ (a a_1 : Iota), % 68.35/68.63 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater % 68.35/68.63 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.35/68.63 zero) % 68.35/68.63 True) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater_or_equal % 68.35/68.63 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.63 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.63 zero) % 68.35/68.63 False) % 68.35/68.63 (Or (Eq True False) (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False)))) % 68.35/68.63 Clause #641 (by clausification #[640]): ∀ (a a_1 : Iota), % 68.35/68.63 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater % 68.35/68.63 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.35/68.63 zero) % 68.35/68.63 True) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater_or_equal % 68.35/68.63 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.63 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.63 zero) % 68.35/68.63 False) % 68.35/68.63 (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False))) % 68.35/68.63 Clause #642 (by forward demodulation #[641, 160]): ∀ (a a_1 : Iota), % 68.35/68.63 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater % 68.35/68.63 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.35/68.63 zero) % 68.35/68.63 True) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater_or_equal % 68.35/68.63 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.63 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.63 zero) % 68.35/68.63 False) % 68.35/68.63 (Eq True False))) % 68.35/68.63 Clause #643 (by clausification #[642]): ∀ (a a_1 : Iota), % 68.35/68.63 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.63 (Or % 68.35/68.63 (Eq % 68.35/68.63 (greater % 68.35/68.63 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.35/68.63 zero) % 68.35/68.63 True) % 68.35/68.63 (Eq % 68.35/68.63 (greater_or_equal % 68.35/68.63 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.63 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.67 zero) % 68.35/68.67 False)) % 68.35/68.67 Clause #646 (by superposition #[643, 283]): ∀ (a a_1 : Iota), % 68.35/68.67 Or % 68.35/68.67 (Eq % 68.35/68.67 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.67 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.67 True) % 68.35/68.67 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.67 (Or % 68.35/68.67 (Eq % 68.35/68.67 (greater % 68.35/68.67 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.35/68.67 zero) % 68.35/68.67 True) % 68.35/68.67 (Eq (greater_or_equal zero zero) False))) % 68.35/68.67 Clause #894 (by forward demodulation #[646, 122]): ∀ (a a_1 : Iota), % 68.35/68.67 Or % 68.35/68.67 (Eq % 68.35/68.67 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.67 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.67 True) % 68.35/68.67 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.67 (Or % 68.35/68.67 (Eq % 68.35/68.67 (greater % 68.35/68.67 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.35/68.67 zero) % 68.35/68.67 True) % 68.35/68.67 (Eq True False))) % 68.35/68.67 Clause #895 (by clausification #[894]): ∀ (a a_1 : Iota), % 68.35/68.67 Or % 68.35/68.67 (Eq % 68.35/68.67 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.67 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.67 True) % 68.35/68.67 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.67 (Eq % 68.35/68.67 (greater % 68.35/68.67 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.35/68.67 zero) % 68.35/68.67 True)) % 68.35/68.67 Clause #896 (by superposition #[895, 132]): ∀ (a a_1 : Iota), % 68.35/68.67 Or % 68.35/68.67 (Eq % 68.35/68.67 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.67 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.67 True) % 68.35/68.67 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.67 (Or (Eq True False) % 68.35/68.67 (Eq (greater (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.35/68.67 True))) % 68.35/68.67 Clause #909 (by clausification #[896]): ∀ (a a_1 : Iota), % 68.35/68.67 Or % 68.35/68.67 (Eq % 68.35/68.67 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.67 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.67 True) % 68.35/68.67 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.67 (Eq (greater (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) True)) % 68.35/68.67 Clause #910 (by superposition #[909, 56]): ∀ (a a_1 a_2 : Iota), % 68.35/68.67 Or % 68.35/68.67 (Eq % 68.35/68.67 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.67 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.67 True) % 68.35/68.67 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.67 (Or (Eq (selection_favors first_movers efficient_producers (skS.0 1 a a_1)) True) % 68.35/68.67 (Or (Eq True False) % 68.35/68.67 (Or (Eq (environment a_2) False) % 68.35/68.67 (Eq (subpopulations efficient_producers first_movers a_2 (skS.0 1 a a_1)) False))))) % 68.35/68.67 Clause #929 (by clausification #[910]): ∀ (a a_1 a_2 : Iota), % 68.35/68.67 Or % 68.35/68.67 (Eq % 68.35/68.67 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.67 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.67 True) % 68.35/68.67 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.67 (Or (Eq (selection_favors first_movers efficient_producers (skS.0 1 a a_1)) True) % 68.35/68.67 (Or (Eq (environment a_2) False) % 68.35/68.67 (Eq (subpopulations efficient_producers first_movers a_2 (skS.0 1 a a_1)) False)))) % 68.35/68.67 Clause #930 (by forward demodulation #[929, 46]): ∀ (a a_1 a_2 : Iota), % 68.35/68.67 Or % 68.35/68.67 (Eq % 68.35/68.67 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.35/68.67 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.35/68.67 True) % 68.35/68.67 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.35/68.67 (Or (Eq False True) % 68.35/68.67 (Or (Eq (environment a_1) False) % 68.35/68.67 (Eq (subpopulations efficient_producers first_movers a_1 (skS.0 1 a a_2)) False)))) % 68.45/68.72 Clause #931 (by clausification #[930]): ∀ (a a_1 a_2 : Iota), % 68.45/68.72 Or % 68.45/68.72 (Eq % 68.45/68.72 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.45/68.72 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.45/68.72 True) % 68.45/68.72 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 (Or (Eq (environment a_1) False) % 68.45/68.72 (Eq (subpopulations efficient_producers first_movers a_1 (skS.0 1 a a_2)) False))) % 68.45/68.72 Clause #932 (by superposition #[931, 161]): ∀ (a a_1 a_2 : Iota), % 68.45/68.72 Or % 68.45/68.72 (Eq % 68.45/68.72 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.45/68.72 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.45/68.72 True) % 68.45/68.72 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 (Or (Eq (subpopulations efficient_producers first_movers (skS.0 0 a_1) (skS.0 1 a a_2)) False) (Eq False True))) % 68.45/68.72 Clause #933 (by clausification #[932]): ∀ (a a_1 a_2 : Iota), % 68.45/68.72 Or % 68.45/68.72 (Eq % 68.45/68.72 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.45/68.72 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.45/68.72 True) % 68.45/68.72 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 (Eq (subpopulations efficient_producers first_movers (skS.0 0 a_1) (skS.0 1 a a_2)) False)) % 68.45/68.72 Clause #934 (by superposition #[933, 344]): ∀ (a : Iota), % 68.45/68.72 Or % 68.45/68.72 (Eq % 68.45/68.72 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.45/68.72 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.45/68.72 True) % 68.45/68.72 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) (Eq False True))) % 68.45/68.72 Clause #937 (by clausification #[934]): ∀ (a : Iota), % 68.45/68.72 Or % 68.45/68.72 (Eq % 68.45/68.72 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.45/68.72 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.45/68.72 True) % 68.45/68.72 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a)))) % 68.45/68.72 Clause #938 (by eliminate duplicate literals #[937]): ∀ (a : Iota), % 68.45/68.72 Or % 68.45/68.72 (Eq % 68.45/68.72 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.45/68.72 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.45/68.72 True) % 68.45/68.72 (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 Clause #940 (by superposition #[938, 131]): ∀ (a : Iota), % 68.45/68.72 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 (Or % 68.45/68.72 (Eq % 68.45/68.72 (greater % 68.45/68.72 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.45/68.72 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.45/68.72 zero) % 68.45/68.72 True) % 68.45/68.72 (Eq True False)) % 68.45/68.72 Clause #948 (by clausification #[940]): ∀ (a : Iota), % 68.45/68.72 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 (Eq % 68.45/68.72 (greater % 68.45/68.72 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.45/68.72 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.45/68.72 zero) % 68.45/68.72 True) % 68.45/68.72 Clause #951 (by superposition #[948, 120]): ∀ (a : Iota), % 68.45/68.72 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 (Or % 68.45/68.72 (Eq % 68.45/68.72 (greater_or_equal % 68.45/68.72 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.45/68.72 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.45/68.72 zero) % 68.45/68.72 True) % 68.45/68.72 (Eq True False)) % 68.45/68.72 Clause #954 (by clausification #[951]): ∀ (a : Iota), % 68.45/68.72 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 (Eq % 68.45/68.72 (greater_or_equal % 68.45/68.72 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.45/68.72 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.45/68.72 zero) % 68.45/68.72 True) % 68.45/68.72 Clause #955 (by superposition #[954, 643]): ∀ (a a_1 : Iota), % 68.45/68.72 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.72 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Or % 68.45/68.76 (Eq % 68.45/68.76 (greater % 68.45/68.76 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.45/68.76 zero) % 68.45/68.76 True) % 68.45/68.76 (Eq True False))) % 68.45/68.76 Clause #998 (by clausification #[955]): ∀ (a a_1 : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Eq % 68.45/68.76 (greater % 68.45/68.76 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.45/68.76 zero) % 68.45/68.76 True)) % 68.45/68.76 Clause #999 (by eliminate duplicate literals #[998]): ∀ (a a_1 : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Eq % 68.45/68.76 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.45/68.76 zero) % 68.45/68.76 True) % 68.45/68.76 Clause #1000 (by superposition #[999, 132]): ∀ (a a_1 : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Or (Eq True False) % 68.45/68.76 (Eq (greater (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) True)) % 68.45/68.76 Clause #1004 (by clausification #[1000]): ∀ (a a_1 : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Eq (greater (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) True) % 68.45/68.76 Clause #1005 (by superposition #[1004, 56]): ∀ (a a_1 a_2 : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Or (Eq (selection_favors first_movers efficient_producers (skS.0 1 a a_1)) True) % 68.45/68.76 (Or (Eq True False) % 68.45/68.76 (Or (Eq (environment a_2) False) % 68.45/68.76 (Eq (subpopulations efficient_producers first_movers a_2 (skS.0 1 a a_1)) False)))) % 68.45/68.76 Clause #1019 (by clausification #[1005]): ∀ (a a_1 a_2 : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Or (Eq (selection_favors first_movers efficient_producers (skS.0 1 a a_1)) True) % 68.45/68.76 (Or (Eq (environment a_2) False) % 68.45/68.76 (Eq (subpopulations efficient_producers first_movers a_2 (skS.0 1 a a_1)) False))) % 68.45/68.76 Clause #1020 (by forward demodulation #[1019, 46]): ∀ (a a_1 a_2 : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Or (Eq False True) % 68.45/68.76 (Or (Eq (environment a_1) False) % 68.45/68.76 (Eq (subpopulations efficient_producers first_movers a_1 (skS.0 1 a a_2)) False))) % 68.45/68.76 Clause #1021 (by clausification #[1020]): ∀ (a a_1 a_2 : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Or (Eq (environment a_1) False) (Eq (subpopulations efficient_producers first_movers a_1 (skS.0 1 a a_2)) False)) % 68.45/68.76 Clause #1022 (by superposition #[1021, 161]): ∀ (a a_1 a_2 : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Or (Eq (subpopulations efficient_producers first_movers (skS.0 0 a_1) (skS.0 1 a a_2)) False) (Eq False True)) % 68.45/68.76 Clause #1023 (by clausification #[1022]): ∀ (a a_1 a_2 : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Eq (subpopulations efficient_producers first_movers (skS.0 0 a_1) (skS.0 1 a a_2)) False) % 68.45/68.76 Clause #1024 (by superposition #[1023, 344]): ∀ (a : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) (Eq False True)) % 68.45/68.76 Clause #1028 (by clausification #[1024]): ∀ (a : Iota), % 68.45/68.76 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 68.45/68.76 Clause #1029 (by eliminate duplicate literals #[1028]): ∀ (a : Iota), Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a)) % 68.45/68.76 Clause #1030 (by backward demodulation #[1029, 152]): ∀ (a a_1 : Iota), Eq (greater_or_equal (skS.0 1 a a_1) (critical_point (skS.0 0 a))) True % 68.45/68.76 Clause #1042 (by backward demodulation #[1029, 272]): ∀ (a a_1 : Iota), % 68.55/68.81 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) % 68.55/68.81 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (critical_point (skS.0 0 a))) False) % 68.55/68.81 Clause #1102 (by forward demodulation #[1042, 203]): ∀ (a a_1 : Iota), % 68.55/68.81 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq True False) % 68.55/68.81 Clause #1103 (by clausification #[1102]): ∀ (a a_1 : Iota), Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True % 68.55/68.81 Clause #1105 (by superposition #[1103, 187]): ∀ (a a_1 : Iota), % 68.55/68.81 Or % 68.55/68.81 (Eq % 68.55/68.81 (decreases % 68.55/68.81 (difference (founding_rate first_movers (skS.0 1 a a_1)) (founding_rate efficient_producers (skS.0 1 a a_1)))) % 68.55/68.81 True) % 68.55/68.81 (Eq True False) % 68.55/68.81 Clause #1106 (by superposition #[1103, 188]): ∀ (a a_1 : Iota), % 68.55/68.81 Or (Eq True False) % 68.55/68.81 (Eq % 68.55/68.81 (decreases % 68.55/68.81 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 68.55/68.81 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 68.55/68.81 False) % 68.55/68.81 Clause #1107 (by superposition #[1103, 191]): ∀ (a a_1 : Iota), % 68.55/68.81 Or (Eq (subpopulations efficient_producers first_movers (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq True False) % 68.55/68.81 Clause #1111 (by clausification #[1107]): ∀ (a a_1 : Iota), Eq (subpopulations efficient_producers first_movers (skS.0 0 a) (skS.0 1 a a_1)) True % 68.55/68.81 Clause #1112 (by clausification #[1106]): ∀ (a a_1 : Iota), % 68.55/68.81 Eq % 68.55/68.81 (decreases % 68.55/68.81 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 68.55/68.81 False % 68.55/68.81 Clause #1113 (by clausification #[1105]): ∀ (a a_1 : Iota), % 68.55/68.81 Eq % 68.55/68.81 (decreases % 68.55/68.81 (difference (founding_rate first_movers (skS.0 1 a a_1)) (founding_rate efficient_producers (skS.0 1 a a_1)))) % 68.55/68.81 True % 68.55/68.81 Clause #1114 (by superposition #[1113, 85]): ∀ (a a_1 : Iota), % 68.55/68.81 Or % 68.55/68.81 (Eq % 68.55/68.81 (decreases % 68.55/68.81 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 68.55/68.81 True) % 68.55/68.81 (Or (Eq True False) % 68.55/68.81 (Eq % 68.55/68.81 (decreases % 68.55/68.81 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 68.55/68.81 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 68.55/68.81 True)) % 68.55/68.81 Clause #1177 (by clausification #[1114]): ∀ (a a_1 : Iota), % 68.55/68.81 Or % 68.55/68.81 (Eq % 68.55/68.81 (decreases % 68.55/68.81 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 68.55/68.81 True) % 68.55/68.81 (Eq % 68.55/68.81 (decreases % 68.55/68.81 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 68.55/68.81 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 68.55/68.81 True) % 68.55/68.81 Clause #1178 (by superposition #[1177, 1112]): ∀ (a a_1 : Iota), % 68.55/68.81 Or % 68.55/68.81 (Eq % 68.55/68.81 (decreases % 68.55/68.81 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 68.55/68.81 True) % 68.55/68.81 (Eq True False) % 68.55/68.81 Clause #1179 (by clausification #[1178]): ∀ (a a_1 : Iota), % 68.55/68.81 Eq % 68.55/68.81 (decreases % 68.55/68.81 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1)))) % 68.55/68.81 True % 68.55/68.81 Clause #1180 (by backward demodulation #[1179, 189]): ∀ (a a_1 a_2 : Iota), % 68.55/68.81 Or (Eq True False) % 68.55/68.81 (Or % 68.55/68.81 (Eq % 68.55/68.81 (greater % 68.55/68.81 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.81 zero) % 68.55/68.81 True) % 68.55/68.81 (Or (Eq (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers a_2)) False) % 68.55/68.81 (Or % 68.55/68.81 (Eq % 68.55/68.81 (greater_or_equal % 68.55/68.81 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.81 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.81 zero) % 68.55/68.81 False) % 68.55/68.81 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (critical_point (skS.0 0 a))) False))))) % 68.55/68.81 Clause #1411 (by clausification #[1180]): ∀ (a a_1 a_2 : Iota), % 68.55/68.81 Or % 68.55/68.81 (Eq % 68.55/68.81 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.81 zero) % 68.55/68.81 True) % 68.55/68.81 (Or (Eq (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers a_2)) False) % 68.55/68.85 (Or % 68.55/68.85 (Eq % 68.55/68.85 (greater_or_equal % 68.55/68.85 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.85 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.85 zero) % 68.55/68.85 False) % 68.55/68.85 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (critical_point (skS.0 0 a))) False)))) % 68.55/68.85 Clause #1412 (by superposition #[1411, 1029]): ∀ (a a_1 a_2 : Iota), % 68.55/68.85 Or % 68.55/68.85 (Eq % 68.55/68.85 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.85 zero) % 68.55/68.85 True) % 68.55/68.85 (Or (Eq (greater_or_equal (skS.0 1 a a_1) (critical_point (skS.0 0 a_2))) False) % 68.55/68.85 (Or % 68.55/68.85 (Eq % 68.55/68.85 (greater_or_equal % 68.55/68.85 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.85 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.85 zero) % 68.55/68.85 False) % 68.55/68.85 (Or (Eq (environment (skS.0 0 a_2)) False) % 68.55/68.85 (Eq (in_environment (skS.0 0 a_2) (critical_point (skS.0 0 a))) False)))) % 68.55/68.85 Clause #1530 (by forward demodulation #[1412, 161]): ∀ (a a_1 a_2 : Iota), % 68.55/68.85 Or % 68.55/68.85 (Eq % 68.55/68.85 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.85 zero) % 68.55/68.85 True) % 68.55/68.85 (Or (Eq (greater_or_equal (skS.0 1 a a_1) (critical_point (skS.0 0 a_2))) False) % 68.55/68.85 (Or % 68.55/68.85 (Eq % 68.55/68.85 (greater_or_equal % 68.55/68.85 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.85 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.85 zero) % 68.55/68.85 False) % 68.55/68.85 (Or (Eq True False) (Eq (in_environment (skS.0 0 a_2) (critical_point (skS.0 0 a))) False)))) % 68.55/68.85 Clause #1531 (by clausification #[1530]): ∀ (a a_1 a_2 : Iota), % 68.55/68.85 Or % 68.55/68.85 (Eq % 68.55/68.85 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.85 zero) % 68.55/68.85 True) % 68.55/68.85 (Or (Eq (greater_or_equal (skS.0 1 a a_1) (critical_point (skS.0 0 a_2))) False) % 68.55/68.85 (Or % 68.55/68.85 (Eq % 68.55/68.85 (greater_or_equal % 68.55/68.85 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.85 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.85 zero) % 68.55/68.85 False) % 68.55/68.85 (Eq (in_environment (skS.0 0 a_2) (critical_point (skS.0 0 a))) False))) % 68.55/68.85 Clause #1532 (by superposition #[1531, 1030]): ∀ (a a_1 : Iota), % 68.55/68.85 Or % 68.55/68.85 (Eq % 68.55/68.85 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.85 zero) % 68.55/68.85 True) % 68.55/68.85 (Or % 68.55/68.85 (Eq % 68.55/68.85 (greater_or_equal % 68.55/68.85 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.85 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.85 zero) % 68.55/68.85 False) % 68.55/68.85 (Or (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False) (Eq False True))) % 68.55/68.85 Clause #1533 (by clausification #[1532]): ∀ (a a_1 : Iota), % 68.55/68.85 Or % 68.55/68.85 (Eq % 68.55/68.85 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.85 zero) % 68.55/68.85 True) % 68.55/68.85 (Or % 68.55/68.85 (Eq % 68.55/68.85 (greater_or_equal % 68.55/68.85 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.85 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.85 zero) % 68.55/68.85 False) % 68.55/68.85 (Eq (in_environment (skS.0 0 a) (critical_point (skS.0 0 a))) False)) % 68.55/68.85 Clause #1534 (by forward demodulation #[1533, 160]): ∀ (a a_1 : Iota), % 68.55/68.85 Or % 68.55/68.85 (Eq % 68.55/68.85 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.85 zero) % 68.55/68.85 True) % 68.55/68.85 (Or % 68.55/68.85 (Eq % 68.55/68.85 (greater_or_equal % 68.55/68.85 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.85 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.85 zero) % 68.55/68.85 False) % 68.55/68.85 (Eq True False)) % 68.55/68.85 Clause #1535 (by clausification #[1534]): ∀ (a a_1 : Iota), % 68.55/68.85 Or % 68.55/68.85 (Eq % 68.55/68.85 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.89 zero) % 68.55/68.89 True) % 68.55/68.89 (Eq % 68.55/68.89 (greater_or_equal % 68.55/68.89 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.89 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.89 zero) % 68.55/68.89 False) % 68.55/68.89 Clause #1538 (by superposition #[1535, 283]): ∀ (a a_1 : Iota), % 68.55/68.89 Or % 68.55/68.89 (Eq % 68.55/68.89 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.89 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.89 True) % 68.55/68.89 (Or % 68.55/68.89 (Eq % 68.55/68.89 (greater % 68.55/68.89 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.89 zero) % 68.55/68.89 True) % 68.55/68.89 (Eq (greater_or_equal zero zero) False)) % 68.55/68.89 Clause #1643 (by forward demodulation #[1538, 122]): ∀ (a a_1 : Iota), % 68.55/68.89 Or % 68.55/68.89 (Eq % 68.55/68.89 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.89 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.89 True) % 68.55/68.89 (Or % 68.55/68.89 (Eq % 68.55/68.89 (greater % 68.55/68.89 (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.89 zero) % 68.55/68.89 True) % 68.55/68.89 (Eq True False)) % 68.55/68.89 Clause #1644 (by clausification #[1643]): ∀ (a a_1 : Iota), % 68.55/68.89 Or % 68.55/68.89 (Eq % 68.55/68.89 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.89 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.89 True) % 68.55/68.89 (Eq % 68.55/68.89 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.55/68.89 zero) % 68.55/68.89 True) % 68.55/68.89 Clause #1645 (by superposition #[1644, 132]): ∀ (a a_1 : Iota), % 68.55/68.89 Or % 68.55/68.89 (Eq % 68.55/68.89 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.89 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.89 True) % 68.55/68.89 (Or (Eq True False) % 68.55/68.89 (Eq (greater (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) True)) % 68.55/68.89 Clause #1649 (by clausification #[1645]): ∀ (a a_1 : Iota), % 68.55/68.89 Or % 68.55/68.89 (Eq % 68.55/68.89 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.89 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.89 True) % 68.55/68.89 (Eq (greater (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) True) % 68.55/68.89 Clause #1650 (by superposition #[1649, 56]): ∀ (a a_1 a_2 : Iota), % 68.55/68.89 Or % 68.55/68.89 (Eq % 68.55/68.89 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.89 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.89 True) % 68.55/68.89 (Or (Eq (selection_favors first_movers efficient_producers (skS.0 1 a a_1)) True) % 68.55/68.89 (Or (Eq True False) % 68.55/68.89 (Or (Eq (environment a_2) False) % 68.55/68.89 (Eq (subpopulations efficient_producers first_movers a_2 (skS.0 1 a a_1)) False)))) % 68.55/68.89 Clause #1674 (by clausification #[1650]): ∀ (a a_1 a_2 : Iota), % 68.55/68.89 Or % 68.55/68.89 (Eq % 68.55/68.89 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.89 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.89 True) % 68.55/68.89 (Or (Eq (selection_favors first_movers efficient_producers (skS.0 1 a a_1)) True) % 68.55/68.89 (Or (Eq (environment a_2) False) % 68.55/68.89 (Eq (subpopulations efficient_producers first_movers a_2 (skS.0 1 a a_1)) False))) % 68.55/68.89 Clause #1675 (by forward demodulation #[1674, 46]): ∀ (a a_1 a_2 : Iota), % 68.55/68.89 Or % 68.55/68.89 (Eq % 68.55/68.89 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.89 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.89 True) % 68.55/68.89 (Or (Eq False True) % 68.55/68.89 (Or (Eq (environment a_1) False) % 68.55/68.89 (Eq (subpopulations efficient_producers first_movers a_1 (skS.0 1 a a_2)) False))) % 68.55/68.89 Clause #1676 (by clausification #[1675]): ∀ (a a_1 a_2 : Iota), % 68.55/68.89 Or % 68.55/68.89 (Eq % 68.55/68.89 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.55/68.89 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.55/68.89 True) % 68.55/68.89 (Or (Eq (environment a_1) False) (Eq (subpopulations efficient_producers first_movers a_1 (skS.0 1 a a_2)) False)) % 68.55/68.89 Clause #1677 (by superposition #[1676, 161]): ∀ (a a_1 a_2 : Iota), % 68.55/68.89 Or % 68.55/68.89 (Eq % 68.55/68.89 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.65/68.93 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.65/68.93 True) % 68.65/68.93 (Or (Eq (subpopulations efficient_producers first_movers (skS.0 0 a_1) (skS.0 1 a a_2)) False) (Eq False True)) % 68.65/68.93 Clause #1680 (by clausification #[1677]): ∀ (a a_1 a_2 : Iota), % 68.65/68.93 Or % 68.65/68.93 (Eq % 68.65/68.93 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.65/68.93 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.65/68.93 True) % 68.65/68.93 (Eq (subpopulations efficient_producers first_movers (skS.0 0 a_1) (skS.0 1 a a_2)) False) % 68.65/68.93 Clause #1681 (by superposition #[1680, 1111]): ∀ (a : Iota), % 68.65/68.93 Or % 68.65/68.93 (Eq % 68.65/68.93 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.65/68.93 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.65/68.93 True) % 68.65/68.93 (Eq False True) % 68.65/68.93 Clause #1682 (by clausification #[1681]): ∀ (a : Iota), % 68.65/68.93 Eq % 68.65/68.93 (greater (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.65/68.93 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.65/68.93 True % 68.65/68.93 Clause #1686 (by superposition #[1682, 131]): ∀ (a : Iota), % 68.65/68.93 Or % 68.65/68.93 (Eq % 68.65/68.93 (greater % 68.65/68.93 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.65/68.93 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.65/68.93 zero) % 68.65/68.93 True) % 68.65/68.93 (Eq True False) % 68.65/68.93 Clause #1693 (by clausification #[1686]): ∀ (a : Iota), % 68.65/68.93 Eq % 68.65/68.93 (greater % 68.65/68.93 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.65/68.93 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.65/68.93 zero) % 68.65/68.93 True % 68.65/68.93 Clause #1696 (by superposition #[1693, 120]): ∀ (a : Iota), % 68.65/68.93 Or % 68.65/68.93 (Eq % 68.65/68.93 (greater_or_equal % 68.65/68.93 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.65/68.93 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.65/68.93 zero) % 68.65/68.93 True) % 68.65/68.93 (Eq True False) % 68.65/68.93 Clause #1700 (by clausification #[1696]): ∀ (a : Iota), % 68.65/68.93 Eq % 68.65/68.93 (greater_or_equal % 68.65/68.93 (difference (growth_rate first_movers (critical_point (skS.0 0 a))) % 68.65/68.93 (growth_rate efficient_producers (critical_point (skS.0 0 a)))) % 68.65/68.93 zero) % 68.65/68.93 True % 68.65/68.93 Clause #1701 (by backward demodulation #[1700, 1535]): ∀ (a a_1 : Iota), % 68.65/68.93 Or % 68.65/68.93 (Eq % 68.65/68.93 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.65/68.93 zero) % 68.65/68.93 True) % 68.65/68.93 (Eq True False) % 68.65/68.93 Clause #1707 (by clausification #[1701]): ∀ (a a_1 : Iota), % 68.65/68.93 Eq % 68.65/68.93 (greater (difference (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) % 68.65/68.93 zero) % 68.65/68.93 True % 68.65/68.93 Clause #1708 (by superposition #[1707, 132]): ∀ (a a_1 : Iota), % 68.65/68.93 Or (Eq True False) % 68.65/68.93 (Eq (greater (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) True) % 68.65/68.93 Clause #1712 (by clausification #[1708]): ∀ (a a_1 : Iota), % 68.65/68.93 Eq (greater (growth_rate first_movers (skS.0 1 a a_1)) (growth_rate efficient_producers (skS.0 1 a a_1))) True % 68.65/68.93 Clause #1717 (by superposition #[1712, 56]): ∀ (a a_1 a_2 : Iota), % 68.65/68.93 Or (Eq (selection_favors first_movers efficient_producers (skS.0 1 a a_1)) True) % 68.65/68.93 (Or (Eq True False) % 68.65/68.93 (Or (Eq (environment a_2) False) % 68.65/68.93 (Eq (subpopulations efficient_producers first_movers a_2 (skS.0 1 a a_1)) False))) % 68.65/68.93 Clause #1745 (by clausification #[1717]): ∀ (a a_1 a_2 : Iota), % 68.65/68.93 Or (Eq (selection_favors first_movers efficient_producers (skS.0 1 a a_1)) True) % 68.65/68.93 (Or (Eq (environment a_2) False) (Eq (subpopulations efficient_producers first_movers a_2 (skS.0 1 a a_1)) False)) % 68.65/68.93 Clause #1746 (by forward demodulation #[1745, 46]): ∀ (a a_1 a_2 : Iota), % 68.65/68.93 Or (Eq False True) % 68.65/68.93 (Or (Eq (environment a) False) (Eq (subpopulations efficient_producers first_movers a (skS.0 1 a_1 a_2)) False)) % 68.65/68.93 Clause #1747 (by clausification #[1746]): ∀ (a a_1 a_2 : Iota), % 68.65/68.93 Or (Eq (environment a) False) (Eq (subpopulations efficient_producers first_movers a (skS.0 1 a_1 a_2)) False) % 68.65/68.93 Clause #1748 (by superposition #[1747, 161]): ∀ (a a_1 a_2 : Iota), % 68.65/68.93 Or (Eq (subpopulations efficient_producers first_movers (skS.0 0 a) (skS.0 1 a_1 a_2)) False) (Eq False True) % 68.65/68.94 Clause #1749 (by clausification #[1748]): ∀ (a a_1 a_2 : Iota), Eq (subpopulations efficient_producers first_movers (skS.0 0 a) (skS.0 1 a_1 a_2)) False % 68.65/68.94 Clause #1750 (by superposition #[1749, 1111]): Eq False True % 68.65/68.94 Clause #1751 (by clausification #[1750]): False % 68.65/68.94 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------