%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT039+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n009.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:19 AM UTC 2026 % Result : Theorem 50.06s 50.38s % Output : Proof 51.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT039+2 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : duper %s % 0.09/0.34 % Computer : n009.cluster.edu % 0.09/0.34 % Model : x86_64 x86_64 % 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.34 % Memory : 8046.5625MB % 0.09/0.34 % OS : Linux 6.8.0-71-generic % 0.09/0.34 % CPULimit : 300 % 0.09/0.34 % WCLimit : 300 % 0.09/0.34 % DateTime : Mon Sep 7 12:55:52 UTC 2026 % 0.09/0.35 % CPUTime : % 50.06/50.38 SZS status Theorem for theBenchmark.p % 50.06/50.38 SZS output start Proof for theBenchmark.p % 50.06/50.38 Clause #0 (by assumption #[]): Eq % 50.06/50.38 (∀ (E S1 S2 T : Iota), % 50.06/50.38 And (And (environment E) (subpopulations S1 S2 E T)) (greater (growth_rate S2 T) (growth_rate S1 T)) → % 50.06/50.38 selection_favors S2 S1 T) % 50.06/50.38 True % 50.06/50.38 Clause #1 (by assumption #[]): Eq % 50.06/50.38 (∀ (E S1 S2 T : Iota), % 50.06/50.38 And % 50.06/50.38 (And (And (And (environment E) (subpopulation S1 E T)) (subpopulation S2 E T)) % 50.06/50.38 (greater (cardinality_at_time S1 T) zero)) % 50.06/50.38 (Eq (cardinality_at_time S2 T) zero) → % 50.06/50.38 selection_favors S1 S2 T) % 50.06/50.38 True % 50.06/50.38 Clause #2 (by assumption #[]): Eq % 50.06/50.38 (∀ (P : Iota), % 50.06/50.38 And % 50.06/50.38 (And (And (observational_period P) (propagation_strategy first_movers)) % 50.06/50.38 (propagation_strategy efficient_producers)) % 50.06/50.38 (∀ (E : Iota), % 50.06/50.38 And (environment E) (in_environment P E) → selection_favors efficient_producers first_movers (end_time E)) → % 50.06/50.38 selection_favors efficient_producers first_movers P) % 50.06/50.38 True % 50.06/50.38 Clause #3 (by assumption #[]): Eq % 50.06/50.38 (∀ (P : Iota), % 50.06/50.38 And (observational_period P) (slow_change P) → % 50.06/50.38 ∀ (E : Iota), % 50.06/50.38 And (environment E) (in_environment P E) → % 50.06/50.38 Exists fun T => And (in_environment E T) (greater T (critical_point E))) % 50.06/50.38 True % 50.06/50.38 Clause #4 (by assumption #[]): Eq (propagation_strategy first_movers) True % 50.06/50.38 Clause #5 (by assumption #[]): Eq (propagation_strategy efficient_producers) True % 50.06/50.38 Clause #6 (by assumption #[]): Eq % 50.06/50.38 (∀ (E T : Iota), % 50.06/50.38 And (And (environment E) (greater_or_equal T (start_time E))) (greater_or_equal (end_time E) T) → % 50.06/50.38 in_environment E T) % 50.06/50.38 True % 50.06/50.38 Clause #7 (by assumption #[]): Eq (∀ (E T : Iota), And (environment E) (in_environment E T) → greater_or_equal (end_time E) T) True % 50.06/50.38 Clause #8 (by assumption #[]): Eq % 50.06/50.38 (∀ (E T : Iota), % 50.06/50.38 And (And (And (environment E) (in_environment E T)) (greater (cardinality_at_time first_movers T) zero)) % 50.06/50.38 (greater (cardinality_at_time efficient_producers T) zero) → % 50.06/50.38 subpopulations first_movers efficient_producers E T) % 50.06/50.38 True % 50.06/50.38 Clause #9 (by assumption #[]): Eq % 50.06/50.38 (∀ (E T : Iota), % 50.06/50.38 And (environment E) (in_environment E T) → greater_or_equal (cardinality_at_time first_movers T) zero) % 50.06/50.38 True % 50.06/50.38 Clause #10 (by assumption #[]): Eq % 50.06/50.38 (∀ (E T : Iota), % 50.06/50.38 And (environment E) (in_environment E T) → % 50.06/50.38 And (subpopulation first_movers E T) (subpopulation efficient_producers E T)) % 50.06/50.38 True % 50.06/50.38 Clause #11 (by assumption #[]): Eq (∀ (E : Iota), environment E → greater_or_equal (critical_point E) (appear efficient_producers E)) True % 50.06/50.38 Clause #12 (by assumption #[]): Eq (∀ (E : Iota), environment E → greater_or_equal (critical_point E) (start_time E)) True % 50.06/50.38 Clause #13 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (greater X Y) (greater Y Z) → greater X Z) True % 50.06/50.38 Clause #15 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (greater_or_equal X Y) (Or (greater X Y) (Eq X Y))) True % 50.06/50.38 Clause #16 (by assumption #[]): Eq % 50.06/50.38 (∀ (E Tc : Iota), % 50.06/50.38 And (environment E) (Eq Tc (critical_point E)) → % 50.06/50.38 And (Not (greater (growth_rate efficient_producers Tc) (growth_rate first_movers Tc))) % 50.06/50.38 (∀ (T : Iota), % 50.06/50.38 And (subpopulations first_movers efficient_producers E T) (greater T Tc) → % 50.06/50.38 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 50.06/50.38 True % 50.06/50.38 Clause #17 (by assumption #[]): Eq % 50.06/50.38 (∀ (E T : Iota), % 50.06/50.38 And (And (environment E) (in_environment E T)) (greater_or_equal T (appear efficient_producers E)) → % 50.06/50.38 greater (cardinality_at_time efficient_producers T) zero) % 50.06/50.38 True % 50.06/50.38 Clause #18 (by assumption #[]): Eq % 50.06/50.38 (Not % 50.06/50.38 (∀ (P : Iota), And (observational_period P) (slow_change P) → selection_favors efficient_producers first_movers P)) % 50.06/50.38 True % 50.06/50.38 Clause #19 (by clausification #[2]): ∀ (a : Iota), % 50.06/50.38 Eq % 50.06/50.38 (And % 50.06/50.38 (And (And (observational_period a) (propagation_strategy first_movers)) % 50.06/50.38 (propagation_strategy efficient_producers)) % 50.06/50.38 (∀ (E : Iota), % 50.06/50.38 And (environment E) (in_environment a E) → selection_favors efficient_producers first_movers (end_time E)) → % 50.06/50.38 selection_favors efficient_producers first_movers a) % 50.15/50.42 True % 50.15/50.42 Clause #20 (by clausification #[19]): ∀ (a : Iota), % 50.15/50.42 Or % 50.15/50.42 (Eq % 50.15/50.42 (And % 50.15/50.42 (And (And (observational_period a) (propagation_strategy first_movers)) % 50.15/50.42 (propagation_strategy efficient_producers)) % 50.15/50.42 (∀ (E : Iota), % 50.15/50.42 And (environment E) (in_environment a E) → selection_favors efficient_producers first_movers (end_time E))) % 50.15/50.42 False) % 50.15/50.42 (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.42 Clause #21 (by clausification #[20]): ∀ (a : Iota), % 50.15/50.42 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.42 (Or % 50.15/50.42 (Eq % 50.15/50.42 (And (And (observational_period a) (propagation_strategy first_movers)) % 50.15/50.42 (propagation_strategy efficient_producers)) % 50.15/50.42 False) % 50.15/50.42 (Eq % 50.15/50.42 (∀ (E : Iota), % 50.15/50.42 And (environment E) (in_environment a E) → selection_favors efficient_producers first_movers (end_time E)) % 50.15/50.42 False)) % 50.15/50.42 Clause #22 (by clausification #[21]): ∀ (a : Iota), % 50.15/50.42 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.42 (Or % 50.15/50.42 (Eq % 50.15/50.42 (∀ (E : Iota), % 50.15/50.42 And (environment E) (in_environment a E) → selection_favors efficient_producers first_movers (end_time E)) % 50.15/50.42 False) % 50.15/50.42 (Or (Eq (And (observational_period a) (propagation_strategy first_movers)) False) % 50.15/50.42 (Eq (propagation_strategy efficient_producers) False))) % 50.15/50.42 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), % 50.15/50.42 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.42 (Or (Eq (And (observational_period a) (propagation_strategy first_movers)) False) % 50.15/50.42 (Or (Eq (propagation_strategy efficient_producers) False) % 50.15/50.42 (Eq % 50.15/50.42 (Not % 50.15/50.42 (And (environment (skS.0 0 a a_1)) (in_environment a (skS.0 0 a a_1)) → % 50.15/50.42 selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1)))) % 50.15/50.42 True))) % 50.15/50.42 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), % 50.15/50.42 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.42 (Or (Eq (propagation_strategy efficient_producers) False) % 50.15/50.42 (Or % 50.15/50.42 (Eq % 50.15/50.42 (Not % 50.15/50.42 (And (environment (skS.0 0 a a_1)) (in_environment a (skS.0 0 a a_1)) → % 50.15/50.42 selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1)))) % 50.15/50.42 True) % 50.15/50.42 (Or (Eq (observational_period a) False) (Eq (propagation_strategy first_movers) False)))) % 50.15/50.42 Clause #25 (by clausification #[24]): ∀ (a a_1 : Iota), % 50.15/50.42 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.42 (Or (Eq (propagation_strategy efficient_producers) False) % 50.15/50.42 (Or (Eq (observational_period a) False) % 50.15/50.42 (Or (Eq (propagation_strategy first_movers) False) % 50.15/50.42 (Eq % 50.15/50.42 (And (environment (skS.0 0 a a_1)) (in_environment a (skS.0 0 a a_1)) → % 50.15/50.42 selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) % 50.15/50.42 False)))) % 50.15/50.42 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), % 50.15/50.42 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.42 (Or (Eq (propagation_strategy efficient_producers) False) % 50.15/50.42 (Or (Eq (observational_period a) False) % 50.15/50.42 (Or (Eq (propagation_strategy first_movers) False) % 50.15/50.42 (Eq (And (environment (skS.0 0 a a_1)) (in_environment a (skS.0 0 a a_1))) True)))) % 50.15/50.42 Clause #27 (by clausification #[25]): ∀ (a a_1 : Iota), % 50.15/50.42 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.42 (Or (Eq (propagation_strategy efficient_producers) False) % 50.15/50.42 (Or (Eq (observational_period a) False) % 50.15/50.42 (Or (Eq (propagation_strategy first_movers) False) % 50.15/50.42 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) False)))) % 50.15/50.42 Clause #28 (by clausification #[26]): ∀ (a a_1 : Iota), % 50.15/50.42 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.42 (Or (Eq (propagation_strategy efficient_producers) False) % 50.15/50.42 (Or (Eq (observational_period a) False) % 50.15/50.42 (Or (Eq (propagation_strategy first_movers) False) (Eq (in_environment a (skS.0 0 a a_1)) True)))) % 50.15/50.42 Clause #29 (by clausification #[26]): ∀ (a a_1 : Iota), % 50.15/50.47 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.47 (Or (Eq (propagation_strategy efficient_producers) False) % 50.15/50.47 (Or (Eq (observational_period a) False) % 50.15/50.47 (Or (Eq (propagation_strategy first_movers) False) (Eq (environment (skS.0 0 a a_1)) True)))) % 50.15/50.47 Clause #30 (by forward demodulation #[28, 5]): ∀ (a a_1 : Iota), % 50.15/50.47 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.47 (Or (Eq True False) % 50.15/50.47 (Or (Eq (observational_period a) False) % 50.15/50.47 (Or (Eq (propagation_strategy first_movers) False) (Eq (in_environment a (skS.0 0 a a_1)) True)))) % 50.15/50.47 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), % 50.15/50.47 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.47 (Or (Eq (observational_period a) False) % 50.15/50.47 (Or (Eq (propagation_strategy first_movers) False) (Eq (in_environment a (skS.0 0 a a_1)) True))) % 50.15/50.47 Clause #32 (by forward demodulation #[31, 4]): ∀ (a a_1 : Iota), % 50.15/50.47 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.47 (Or (Eq (observational_period a) False) (Or (Eq True False) (Eq (in_environment a (skS.0 0 a a_1)) True))) % 50.15/50.47 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), % 50.15/50.47 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.15/50.47 (Or (Eq (observational_period a) False) (Eq (in_environment a (skS.0 0 a a_1)) True)) % 50.15/50.47 Clause #34 (by clausification #[6]): ∀ (a : Iota), % 50.15/50.47 Eq % 50.15/50.47 (∀ (T : Iota), % 50.15/50.47 And (And (environment a) (greater_or_equal T (start_time a))) (greater_or_equal (end_time a) T) → % 50.15/50.47 in_environment a T) % 50.15/50.47 True % 50.15/50.47 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), % 50.15/50.47 Eq % 50.15/50.47 (And (And (environment a) (greater_or_equal a_1 (start_time a))) (greater_or_equal (end_time a) a_1) → % 50.15/50.47 in_environment a a_1) % 50.15/50.47 True % 50.15/50.47 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), % 50.15/50.47 Or (Eq (And (And (environment a) (greater_or_equal a_1 (start_time a))) (greater_or_equal (end_time a) a_1)) False) % 50.15/50.47 (Eq (in_environment a a_1) True) % 50.15/50.47 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), % 50.15/50.47 Or (Eq (in_environment a a_1) True) % 50.15/50.47 (Or (Eq (And (environment a) (greater_or_equal a_1 (start_time a))) False) % 50.15/50.47 (Eq (greater_or_equal (end_time a) a_1) False)) % 50.15/50.47 Clause #38 (by clausification #[37]): ∀ (a a_1 : Iota), % 50.15/50.47 Or (Eq (in_environment a a_1) True) % 50.15/50.47 (Or (Eq (greater_or_equal (end_time a) a_1) False) % 50.15/50.47 (Or (Eq (environment a) False) (Eq (greater_or_equal a_1 (start_time a)) False))) % 50.15/50.47 Clause #39 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (T : Iota), And (environment a) (in_environment a T) → greater_or_equal (end_time a) T) True % 50.15/50.47 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), Eq (And (environment a) (in_environment a a_1) → greater_or_equal (end_time a) a_1) True % 50.15/50.47 Clause #41 (by clausification #[40]): ∀ (a a_1 : Iota), % 50.15/50.47 Or (Eq (And (environment a) (in_environment a a_1)) False) (Eq (greater_or_equal (end_time a) a_1) True) % 50.15/50.47 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), % 50.15/50.47 Or (Eq (greater_or_equal (end_time a) a_1) True) (Or (Eq (environment a) False) (Eq (in_environment a a_1) False)) % 50.15/50.47 Clause #43 (by clausification #[0]): ∀ (a : Iota), % 50.15/50.47 Eq % 50.15/50.47 (∀ (S1 S2 T : Iota), % 50.15/50.47 And (And (environment a) (subpopulations S1 S2 a T)) (greater (growth_rate S2 T) (growth_rate S1 T)) → % 50.15/50.47 selection_favors S2 S1 T) % 50.15/50.47 True % 50.15/50.47 Clause #44 (by clausification #[43]): ∀ (a a_1 : Iota), % 50.15/50.47 Eq % 50.15/50.47 (∀ (S2 T : Iota), % 50.15/50.47 And (And (environment a) (subpopulations a_1 S2 a T)) (greater (growth_rate S2 T) (growth_rate a_1 T)) → % 50.15/50.47 selection_favors S2 a_1 T) % 50.15/50.47 True % 50.15/50.47 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 : Iota), % 50.15/50.47 Eq % 50.15/50.47 (∀ (T : Iota), % 50.15/50.47 And (And (environment a) (subpopulations a_1 a_2 a T)) (greater (growth_rate a_2 T) (growth_rate a_1 T)) → % 50.15/50.47 selection_favors a_2 a_1 T) % 50.15/50.47 True % 50.15/50.47 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 a_3 : Iota), % 50.15/50.47 Eq % 50.15/50.47 (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)) → % 50.15/50.47 selection_favors a_2 a_1 a_3) % 50.15/50.47 True % 50.15/50.47 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 : Iota), % 50.25/50.52 Or % 50.25/50.52 (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))) % 50.25/50.52 False) % 50.25/50.52 (Eq (selection_favors a_2 a_1 a_3) True) % 50.25/50.52 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 : Iota), % 50.25/50.52 Or (Eq (selection_favors a a_1 a_2) True) % 50.25/50.52 (Or (Eq (And (environment a_3) (subpopulations a_1 a a_3 a_2)) False) % 50.25/50.52 (Eq (greater (growth_rate a a_2) (growth_rate a_1 a_2)) False)) % 50.25/50.52 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 : Iota), % 50.25/50.52 Or (Eq (selection_favors a a_1 a_2) True) % 50.25/50.52 (Or (Eq (greater (growth_rate a a_2) (growth_rate a_1 a_2)) False) % 50.25/50.52 (Or (Eq (environment a_3) False) (Eq (subpopulations a_1 a a_3 a_2) False))) % 50.25/50.52 Clause #56 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (greater a Y) (greater Y Z) → greater a Z) True % 50.25/50.52 Clause #57 (by clausification #[56]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (greater a a_1) (greater a_1 Z) → greater a Z) True % 50.25/50.52 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 : Iota), Eq (And (greater a a_1) (greater a_1 a_2) → greater a a_2) True % 50.25/50.52 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (greater a a_1) (greater a_1 a_2)) False) (Eq (greater a a_2) True) % 50.25/50.52 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 : Iota), Or (Eq (greater a a_1) True) (Or (Eq (greater a a_2) False) (Eq (greater a_2 a_1) False)) % 50.25/50.52 Clause #61 (by clausification #[12]): ∀ (a : Iota), Eq (environment a → greater_or_equal (critical_point a) (start_time a)) True % 50.25/50.52 Clause #62 (by clausification #[61]): ∀ (a : Iota), Or (Eq (environment a) False) (Eq (greater_or_equal (critical_point a) (start_time a)) True) % 50.25/50.52 Clause #63 (by clausification #[18]): Eq (∀ (P : Iota), And (observational_period P) (slow_change P) → selection_favors efficient_producers first_movers P) % 50.25/50.52 False % 50.25/50.52 Clause #64 (by clausification #[63]): ∀ (a : Iota), % 50.25/50.52 Eq % 50.25/50.52 (Not % 50.25/50.52 (And (observational_period (skS.0 1 a)) (slow_change (skS.0 1 a)) → % 50.25/50.52 selection_favors efficient_producers first_movers (skS.0 1 a))) % 50.25/50.52 True % 50.25/50.52 Clause #65 (by clausification #[64]): ∀ (a : Iota), % 50.25/50.52 Eq % 50.25/50.52 (And (observational_period (skS.0 1 a)) (slow_change (skS.0 1 a)) → % 50.25/50.52 selection_favors efficient_producers first_movers (skS.0 1 a)) % 50.25/50.52 False % 50.25/50.52 Clause #66 (by clausification #[65]): ∀ (a : Iota), Eq (And (observational_period (skS.0 1 a)) (slow_change (skS.0 1 a))) True % 50.25/50.52 Clause #67 (by clausification #[65]): ∀ (a : Iota), Eq (selection_favors efficient_producers first_movers (skS.0 1 a)) False % 50.25/50.52 Clause #68 (by clausification #[66]): ∀ (a : Iota), Eq (slow_change (skS.0 1 a)) True % 50.25/50.52 Clause #69 (by clausification #[66]): ∀ (a : Iota), Eq (observational_period (skS.0 1 a)) True % 50.25/50.52 Clause #70 (by superposition #[69, 33]): ∀ (a a_1 : Iota), % 50.25/50.52 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a)) True) % 50.25/50.52 (Or (Eq True False) (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) a_1)) True)) % 50.25/50.52 Clause #71 (by clausification #[1]): ∀ (a : Iota), % 50.25/50.52 Eq % 50.25/50.52 (∀ (S1 S2 T : Iota), % 50.25/50.52 And % 50.25/50.52 (And (And (And (environment a) (subpopulation S1 a T)) (subpopulation S2 a T)) % 50.25/50.52 (greater (cardinality_at_time S1 T) zero)) % 50.25/50.52 (Eq (cardinality_at_time S2 T) zero) → % 50.25/50.52 selection_favors S1 S2 T) % 50.25/50.52 True % 50.25/50.52 Clause #72 (by clausification #[71]): ∀ (a a_1 : Iota), % 50.25/50.52 Eq % 50.25/50.52 (∀ (S2 T : Iota), % 50.25/50.52 And % 50.25/50.52 (And (And (And (environment a) (subpopulation a_1 a T)) (subpopulation S2 a T)) % 50.25/50.52 (greater (cardinality_at_time a_1 T) zero)) % 50.25/50.52 (Eq (cardinality_at_time S2 T) zero) → % 50.25/50.52 selection_favors a_1 S2 T) % 50.25/50.52 True % 50.25/50.52 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), % 50.25/50.52 Eq % 50.25/50.52 (∀ (T : Iota), % 50.25/50.52 And % 50.25/50.52 (And (And (And (environment a) (subpopulation a_1 a T)) (subpopulation a_2 a T)) % 50.25/50.52 (greater (cardinality_at_time a_1 T) zero)) % 50.25/50.52 (Eq (cardinality_at_time a_2 T) zero) → % 50.25/50.52 selection_favors a_1 a_2 T) % 50.25/50.52 True % 50.25/50.52 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), % 50.25/50.52 Eq % 50.25/50.52 (And % 50.25/50.52 (And (And (And (environment a) (subpopulation a_1 a a_2)) (subpopulation a_3 a a_2)) % 50.25/50.56 (greater (cardinality_at_time a_1 a_2) zero)) % 50.25/50.56 (Eq (cardinality_at_time a_3 a_2) zero) → % 50.25/50.56 selection_favors a_1 a_3 a_2) % 50.25/50.56 True % 50.25/50.56 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 a_3 : Iota), % 50.25/50.56 Or % 50.25/50.56 (Eq % 50.25/50.56 (And % 50.25/50.56 (And (And (And (environment a) (subpopulation a_1 a a_2)) (subpopulation a_3 a a_2)) % 50.25/50.56 (greater (cardinality_at_time a_1 a_2) zero)) % 50.25/50.56 (Eq (cardinality_at_time a_3 a_2) zero)) % 50.25/50.56 False) % 50.25/50.56 (Eq (selection_favors a_1 a_3 a_2) True) % 50.25/50.56 Clause #76 (by clausification #[75]): ∀ (a a_1 a_2 a_3 : Iota), % 50.25/50.56 Or (Eq (selection_favors a a_1 a_2) True) % 50.25/50.56 (Or % 50.25/50.56 (Eq % 50.25/50.56 (And (And (And (environment a_3) (subpopulation a a_3 a_2)) (subpopulation a_1 a_3 a_2)) % 50.25/50.56 (greater (cardinality_at_time a a_2) zero)) % 50.25/50.56 False) % 50.25/50.56 (Eq (Eq (cardinality_at_time a_1 a_2) zero) False)) % 50.25/50.56 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 : Iota), % 50.25/50.56 Or (Eq (selection_favors a a_1 a_2) True) % 50.25/50.56 (Or (Eq (Eq (cardinality_at_time a_1 a_2) zero) False) % 50.25/50.56 (Or (Eq (And (And (environment a_3) (subpopulation a a_3 a_2)) (subpopulation a_1 a_3 a_2)) False) % 50.25/50.56 (Eq (greater (cardinality_at_time a a_2) zero) False))) % 50.25/50.56 Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 a_3 : Iota), % 50.25/50.56 Or (Eq (selection_favors a a_1 a_2) True) % 50.25/50.56 (Or (Eq (And (And (environment a_3) (subpopulation a a_3 a_2)) (subpopulation a_1 a_3 a_2)) False) % 50.25/50.56 (Or (Eq (greater (cardinality_at_time a a_2) zero) False) (Ne (cardinality_at_time a_1 a_2) zero))) % 50.25/50.56 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 a_3 : Iota), % 50.25/50.56 Or (Eq (selection_favors a a_1 a_2) True) % 50.25/50.56 (Or (Eq (greater (cardinality_at_time a a_2) zero) False) % 50.25/50.56 (Or (Ne (cardinality_at_time a_1 a_2) zero) % 50.25/50.56 (Or (Eq (And (environment a_3) (subpopulation a a_3 a_2)) False) (Eq (subpopulation a_1 a_3 a_2) False)))) % 50.25/50.56 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 a_3 : Iota), % 50.25/50.56 Or (Eq (selection_favors a a_1 a_2) True) % 50.25/50.56 (Or (Eq (greater (cardinality_at_time a a_2) zero) False) % 50.25/50.56 (Or (Ne (cardinality_at_time a_1 a_2) zero) % 50.25/50.56 (Or (Eq (subpopulation a_1 a_3 a_2) False) % 50.25/50.56 (Or (Eq (environment a_3) False) (Eq (subpopulation a a_3 a_2) False))))) % 50.25/50.56 Clause #81 (by clausification #[17]): ∀ (a : Iota), % 50.25/50.56 Eq % 50.25/50.56 (∀ (T : Iota), % 50.25/50.56 And (And (environment a) (in_environment a T)) (greater_or_equal T (appear efficient_producers a)) → % 50.25/50.56 greater (cardinality_at_time efficient_producers T) zero) % 50.25/50.56 True % 50.25/50.56 Clause #82 (by clausification #[81]): ∀ (a a_1 : Iota), % 50.25/50.56 Eq % 50.25/50.56 (And (And (environment a) (in_environment a a_1)) (greater_or_equal a_1 (appear efficient_producers a)) → % 50.25/50.56 greater (cardinality_at_time efficient_producers a_1) zero) % 50.25/50.56 True % 50.25/50.56 Clause #83 (by clausification #[82]): ∀ (a a_1 : Iota), % 50.25/50.56 Or (Eq (And (And (environment a) (in_environment a a_1)) (greater_or_equal a_1 (appear efficient_producers a))) False) % 50.25/50.56 (Eq (greater (cardinality_at_time efficient_producers a_1) zero) True) % 50.25/50.56 Clause #84 (by clausification #[83]): ∀ (a a_1 : Iota), % 50.25/50.56 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 50.25/50.56 (Or (Eq (And (environment a_1) (in_environment a_1 a)) False) % 50.25/50.56 (Eq (greater_or_equal a (appear efficient_producers a_1)) False)) % 50.25/50.56 Clause #85 (by clausification #[84]): ∀ (a a_1 : Iota), % 50.25/50.56 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 50.25/50.56 (Or (Eq (greater_or_equal a (appear efficient_producers a_1)) False) % 50.25/50.56 (Or (Eq (environment a_1) False) (Eq (in_environment a_1 a) False))) % 50.25/50.56 Clause #86 (by clausification #[11]): ∀ (a : Iota), Eq (environment a → greater_or_equal (critical_point a) (appear efficient_producers a)) True % 50.25/50.56 Clause #87 (by clausification #[86]): ∀ (a : Iota), % 50.25/50.56 Or (Eq (environment a) False) (Eq (greater_or_equal (critical_point a) (appear efficient_producers a)) True) % 50.25/50.56 Clause #88 (by clausification #[9]): ∀ (a : Iota), % 50.25/50.56 Eq % 50.25/50.56 (∀ (T : Iota), % 50.25/50.56 And (environment a) (in_environment a T) → greater_or_equal (cardinality_at_time first_movers T) zero) % 50.35/50.61 True % 50.35/50.61 Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota), % 50.35/50.61 Eq (And (environment a) (in_environment a a_1) → greater_or_equal (cardinality_at_time first_movers a_1) zero) True % 50.35/50.61 Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota), % 50.35/50.61 Or (Eq (And (environment a) (in_environment a a_1)) False) % 50.35/50.61 (Eq (greater_or_equal (cardinality_at_time first_movers a_1) zero) True) % 50.35/50.61 Clause #91 (by clausification #[90]): ∀ (a a_1 : Iota), % 50.35/50.61 Or (Eq (greater_or_equal (cardinality_at_time first_movers a) zero) True) % 50.35/50.61 (Or (Eq (environment a_1) False) (Eq (in_environment a_1 a) False)) % 50.35/50.61 Clause #92 (by clausification #[8]): ∀ (a : Iota), % 50.35/50.61 Eq % 50.35/50.61 (∀ (T : Iota), % 50.35/50.61 And (And (And (environment a) (in_environment a T)) (greater (cardinality_at_time first_movers T) zero)) % 50.35/50.61 (greater (cardinality_at_time efficient_producers T) zero) → % 50.35/50.61 subpopulations first_movers efficient_producers a T) % 50.35/50.61 True % 50.35/50.61 Clause #93 (by clausification #[92]): ∀ (a a_1 : Iota), % 50.35/50.61 Eq % 50.35/50.61 (And (And (And (environment a) (in_environment a a_1)) (greater (cardinality_at_time first_movers a_1) zero)) % 50.35/50.61 (greater (cardinality_at_time efficient_producers a_1) zero) → % 50.35/50.61 subpopulations first_movers efficient_producers a a_1) % 50.35/50.61 True % 50.35/50.61 Clause #94 (by clausification #[93]): ∀ (a a_1 : Iota), % 50.35/50.61 Or % 50.35/50.61 (Eq % 50.35/50.61 (And (And (And (environment a) (in_environment a a_1)) (greater (cardinality_at_time first_movers a_1) zero)) % 50.35/50.61 (greater (cardinality_at_time efficient_producers a_1) zero)) % 50.35/50.61 False) % 50.35/50.61 (Eq (subpopulations first_movers efficient_producers a a_1) True) % 50.35/50.61 Clause #95 (by clausification #[94]): ∀ (a a_1 : Iota), % 50.35/50.61 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 50.35/50.61 (Or % 50.35/50.61 (Eq (And (And (environment a) (in_environment a a_1)) (greater (cardinality_at_time first_movers a_1) zero)) % 50.35/50.61 False) % 50.35/50.61 (Eq (greater (cardinality_at_time efficient_producers a_1) zero) False)) % 50.35/50.61 Clause #96 (by clausification #[95]): ∀ (a a_1 : Iota), % 50.35/50.61 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 50.35/50.61 (Or (Eq (greater (cardinality_at_time efficient_producers a_1) zero) False) % 50.35/50.61 (Or (Eq (And (environment a) (in_environment a a_1)) False) % 50.35/50.61 (Eq (greater (cardinality_at_time first_movers a_1) zero) False))) % 50.35/50.61 Clause #97 (by clausification #[96]): ∀ (a a_1 : Iota), % 50.35/50.61 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 50.35/50.61 (Or (Eq (greater (cardinality_at_time efficient_producers a_1) zero) False) % 50.35/50.61 (Or (Eq (greater (cardinality_at_time first_movers a_1) zero) False) % 50.35/50.61 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False)))) % 50.35/50.61 Clause #98 (by clausification #[3]): ∀ (a : Iota), % 50.35/50.61 Eq % 50.35/50.61 (And (observational_period a) (slow_change a) → % 50.35/50.61 ∀ (E : Iota), % 50.35/50.61 And (environment E) (in_environment a E) → % 50.35/50.61 Exists fun T => And (in_environment E T) (greater T (critical_point E))) % 50.35/50.61 True % 50.35/50.61 Clause #99 (by clausification #[98]): ∀ (a : Iota), % 50.35/50.61 Or (Eq (And (observational_period a) (slow_change a)) False) % 50.35/50.61 (Eq % 50.35/50.61 (∀ (E : Iota), % 50.35/50.61 And (environment E) (in_environment a E) → % 50.35/50.61 Exists fun T => And (in_environment E T) (greater T (critical_point E))) % 50.35/50.61 True) % 50.35/50.61 Clause #100 (by clausification #[99]): ∀ (a : Iota), % 50.35/50.61 Or % 50.35/50.61 (Eq % 50.35/50.61 (∀ (E : Iota), % 50.35/50.61 And (environment E) (in_environment a E) → % 50.35/50.61 Exists fun T => And (in_environment E T) (greater T (critical_point E))) % 50.35/50.61 True) % 50.35/50.61 (Or (Eq (observational_period a) False) (Eq (slow_change a) False)) % 50.35/50.61 Clause #101 (by clausification #[100]): ∀ (a a_1 : Iota), % 50.35/50.61 Or (Eq (observational_period a) False) % 50.35/50.61 (Or (Eq (slow_change a) False) % 50.35/50.61 (Eq % 50.35/50.61 (And (environment a_1) (in_environment a a_1) → % 50.35/50.61 Exists fun T => And (in_environment a_1 T) (greater T (critical_point a_1))) % 50.35/50.61 True)) % 50.35/50.61 Clause #102 (by clausification #[101]): ∀ (a a_1 : Iota), % 50.35/50.61 Or (Eq (observational_period a) False) % 50.35/50.61 (Or (Eq (slow_change a) False) % 50.35/50.61 (Or (Eq (And (environment a_1) (in_environment a a_1)) False) % 50.35/50.61 (Eq (Exists fun T => And (in_environment a_1 T) (greater T (critical_point a_1))) True))) % 50.35/50.66 Clause #103 (by clausification #[102]): ∀ (a a_1 : Iota), % 50.35/50.66 Or (Eq (observational_period a) False) % 50.35/50.66 (Or (Eq (slow_change a) False) % 50.35/50.66 (Or (Eq (Exists fun T => And (in_environment a_1 T) (greater T (critical_point a_1))) True) % 50.35/50.66 (Or (Eq (environment a_1) False) (Eq (in_environment a a_1) False)))) % 50.35/50.66 Clause #104 (by clausification #[103]): ∀ (a a_1 a_2 : Iota), % 50.35/50.66 Or (Eq (observational_period a) False) % 50.35/50.66 (Or (Eq (slow_change a) False) % 50.35/50.66 (Or (Eq (environment a_1) False) % 50.35/50.66 (Or (Eq (in_environment a a_1) False) % 50.35/50.66 (Eq (And (in_environment a_1 (skS.0 2 a_1 a_2)) (greater (skS.0 2 a_1 a_2) (critical_point a_1))) True)))) % 50.35/50.66 Clause #105 (by clausification #[104]): ∀ (a a_1 a_2 : Iota), % 50.35/50.66 Or (Eq (observational_period a) False) % 50.35/50.66 (Or (Eq (slow_change a) False) % 50.35/50.66 (Or (Eq (environment a_1) False) % 50.35/50.66 (Or (Eq (in_environment a a_1) False) (Eq (greater (skS.0 2 a_1 a_2) (critical_point a_1)) True)))) % 50.35/50.66 Clause #106 (by clausification #[104]): ∀ (a a_1 a_2 : Iota), % 50.35/50.66 Or (Eq (observational_period a) False) % 50.35/50.66 (Or (Eq (slow_change a) False) % 50.35/50.66 (Or (Eq (environment a_1) False) % 50.35/50.66 (Or (Eq (in_environment a a_1) False) (Eq (in_environment a_1 (skS.0 2 a_1 a_2)) True)))) % 50.35/50.66 Clause #107 (by superposition #[105, 69]): ∀ (a a_1 a_2 : Iota), % 50.35/50.66 Or (Eq (slow_change (skS.0 1 a)) False) % 50.35/50.66 (Or (Eq (environment a_1) False) % 50.35/50.66 (Or (Eq (in_environment (skS.0 1 a) a_1) False) % 50.35/50.66 (Or (Eq (greater (skS.0 2 a_1 a_2) (critical_point a_1)) True) (Eq False True)))) % 50.35/50.66 Clause #108 (by clausification #[10]): ∀ (a : Iota), % 50.35/50.66 Eq % 50.35/50.66 (∀ (T : Iota), % 50.35/50.66 And (environment a) (in_environment a T) → % 50.35/50.66 And (subpopulation first_movers a T) (subpopulation efficient_producers a T)) % 50.35/50.66 True % 50.35/50.66 Clause #109 (by clausification #[108]): ∀ (a a_1 : Iota), % 50.35/50.66 Eq % 50.35/50.66 (And (environment a) (in_environment a a_1) → % 50.35/50.66 And (subpopulation first_movers a a_1) (subpopulation efficient_producers a a_1)) % 50.35/50.66 True % 50.35/50.66 Clause #110 (by clausification #[109]): ∀ (a a_1 : Iota), % 50.35/50.66 Or (Eq (And (environment a) (in_environment a a_1)) False) % 50.35/50.66 (Eq (And (subpopulation first_movers a a_1) (subpopulation efficient_producers a a_1)) True) % 50.35/50.66 Clause #111 (by clausification #[110]): ∀ (a a_1 : Iota), % 50.35/50.66 Or (Eq (And (subpopulation first_movers a a_1) (subpopulation efficient_producers a a_1)) True) % 50.35/50.66 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False)) % 50.35/50.66 Clause #112 (by clausification #[111]): ∀ (a a_1 : Iota), % 50.35/50.66 Or (Eq (environment a) False) % 50.35/50.66 (Or (Eq (in_environment a a_1) False) (Eq (subpopulation efficient_producers a a_1) True)) % 50.35/50.66 Clause #113 (by clausification #[111]): ∀ (a a_1 : Iota), % 50.35/50.66 Or (Eq (environment a) False) (Or (Eq (in_environment a a_1) False) (Eq (subpopulation first_movers a a_1) True)) % 50.35/50.66 Clause #114 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (greater_or_equal a Y) (Or (greater a Y) (Eq a Y))) True % 50.35/50.66 Clause #115 (by clausification #[114]): ∀ (a a_1 : Iota), Eq (Iff (greater_or_equal a a_1) (Or (greater a a_1) (Eq a a_1))) True % 50.35/50.66 Clause #116 (by clausification #[115]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (Or (greater a a_1) (Eq a a_1)) False) % 50.35/50.66 Clause #117 (by clausification #[115]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Eq (Or (greater a a_1) (Eq a a_1)) True) % 50.35/50.66 Clause #118 (by clausification #[116]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (Eq a a_1) False) % 50.35/50.66 Clause #119 (by clausification #[116]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (greater a a_1) False) % 50.35/50.66 Clause #120 (by clausification #[118]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Ne a a_1) % 50.35/50.66 Clause #121 (by destructive equality resolution #[120]): ∀ (a : Iota), Eq (greater_or_equal a a) True % 50.35/50.66 Clause #123 (by superposition #[121, 38]): ∀ (a : Iota), % 50.35/50.66 Or (Eq (in_environment a (end_time a)) True) % 50.35/50.66 (Or (Eq True False) (Or (Eq (environment a) False) (Eq (greater_or_equal (end_time a) (start_time a)) False))) % 50.35/50.66 Clause #124 (by clausification #[117]): ∀ (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)) % 50.45/50.70 Clause #125 (by clausification #[124]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Or (Eq (greater a a_1) True) (Eq a a_1)) % 50.45/50.70 Clause #127 (by clausification #[16]): ∀ (a : Iota), % 50.45/50.70 Eq % 50.45/50.70 (∀ (Tc : Iota), % 50.45/50.70 And (environment a) (Eq Tc (critical_point a)) → % 50.45/50.70 And (Not (greater (growth_rate efficient_producers Tc) (growth_rate first_movers Tc))) % 50.45/50.70 (∀ (T : Iota), % 50.45/50.70 And (subpopulations first_movers efficient_producers a T) (greater T Tc) → % 50.45/50.70 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 50.45/50.70 True % 50.45/50.70 Clause #128 (by clausification #[127]): ∀ (a a_1 : Iota), % 50.45/50.70 Eq % 50.45/50.70 (And (environment a) (Eq a_1 (critical_point a)) → % 50.45/50.70 And (Not (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1))) % 50.45/50.70 (∀ (T : Iota), % 50.45/50.70 And (subpopulations first_movers efficient_producers a T) (greater T a_1) → % 50.45/50.70 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 50.45/50.70 True % 50.45/50.70 Clause #129 (by clausification #[128]): ∀ (a a_1 : Iota), % 50.45/50.70 Or (Eq (And (environment a) (Eq a_1 (critical_point a))) False) % 50.45/50.70 (Eq % 50.45/50.70 (And (Not (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1))) % 50.45/50.70 (∀ (T : Iota), % 50.45/50.70 And (subpopulations first_movers efficient_producers a T) (greater T a_1) → % 50.45/50.70 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 50.45/50.70 True) % 50.45/50.70 Clause #130 (by clausification #[129]): ∀ (a a_1 : Iota), % 50.45/50.70 Or % 50.45/50.70 (Eq % 50.45/50.70 (And (Not (greater (growth_rate efficient_producers a) (growth_rate first_movers a))) % 50.45/50.70 (∀ (T : Iota), % 50.45/50.70 And (subpopulations first_movers efficient_producers a_1 T) (greater T a) → % 50.45/50.70 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 50.45/50.70 True) % 50.45/50.70 (Or (Eq (environment a_1) False) (Eq (Eq a (critical_point a_1)) False)) % 50.45/50.70 Clause #131 (by clausification #[130]): ∀ (a a_1 : Iota), % 50.45/50.70 Or (Eq (environment a) False) % 50.45/50.70 (Or (Eq (Eq a_1 (critical_point a)) False) % 50.45/50.70 (Eq % 50.45/50.70 (∀ (T : Iota), % 50.45/50.70 And (subpopulations first_movers efficient_producers a T) (greater T a_1) → % 50.45/50.70 greater (growth_rate efficient_producers T) (growth_rate first_movers T)) % 50.45/50.70 True)) % 50.45/50.70 Clause #133 (by clausification #[131]): ∀ (a a_1 : Iota), % 50.45/50.70 Or (Eq (environment a) False) % 50.45/50.70 (Or % 50.45/50.70 (Eq % 50.45/50.70 (∀ (T : Iota), % 50.45/50.70 And (subpopulations first_movers efficient_producers a T) (greater T a_1) → % 50.45/50.70 greater (growth_rate efficient_producers T) (growth_rate first_movers T)) % 50.45/50.70 True) % 50.45/50.70 (Ne a_1 (critical_point a))) % 50.45/50.70 Clause #134 (by clausification #[133]): ∀ (a a_1 a_2 : Iota), % 50.45/50.70 Or (Eq (environment a) False) % 50.45/50.70 (Or (Ne a_1 (critical_point a)) % 50.45/50.70 (Eq % 50.45/50.70 (And (subpopulations first_movers efficient_producers a a_2) (greater a_2 a_1) → % 50.45/50.70 greater (growth_rate efficient_producers a_2) (growth_rate first_movers a_2)) % 50.45/50.70 True)) % 50.45/50.70 Clause #135 (by clausification #[134]): ∀ (a a_1 a_2 : Iota), % 50.45/50.70 Or (Eq (environment a) False) % 50.45/50.70 (Or (Ne a_1 (critical_point a)) % 50.45/50.70 (Or (Eq (And (subpopulations first_movers efficient_producers a a_2) (greater a_2 a_1)) False) % 50.45/50.70 (Eq (greater (growth_rate efficient_producers a_2) (growth_rate first_movers a_2)) True))) % 50.45/50.70 Clause #136 (by clausification #[135]): ∀ (a a_1 a_2 : Iota), % 50.45/50.70 Or (Eq (environment a) False) % 50.45/50.70 (Or (Ne a_1 (critical_point a)) % 50.45/50.70 (Or (Eq (greater (growth_rate efficient_producers a_2) (growth_rate first_movers a_2)) True) % 50.45/50.70 (Or (Eq (subpopulations first_movers efficient_producers a a_2) False) (Eq (greater a_2 a_1) False)))) % 50.45/50.70 Clause #137 (by destructive equality resolution #[136]): ∀ (a a_1 : Iota), % 50.45/50.70 Or (Eq (environment a) False) % 50.45/50.70 (Or (Eq (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1)) True) % 50.45/50.70 (Or (Eq (subpopulations first_movers efficient_producers a a_1) False) % 50.45/50.70 (Eq (greater a_1 (critical_point a)) False))) % 50.45/50.70 Clause #139 (by clausification #[123]): ∀ (a : Iota), % 50.45/50.75 Or (Eq (in_environment a (end_time a)) True) % 50.45/50.75 (Or (Eq (environment a) False) (Eq (greater_or_equal (end_time a) (start_time a)) False)) % 50.45/50.75 Clause #144 (by forward demodulation #[29, 5]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.45/50.75 (Or (Eq True False) % 50.45/50.75 (Or (Eq (observational_period a) False) % 50.45/50.75 (Or (Eq (propagation_strategy first_movers) False) (Eq (environment (skS.0 0 a a_1)) True)))) % 50.45/50.75 Clause #145 (by clausification #[144]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.45/50.75 (Or (Eq (observational_period a) False) % 50.45/50.75 (Or (Eq (propagation_strategy first_movers) False) (Eq (environment (skS.0 0 a a_1)) True))) % 50.45/50.75 Clause #146 (by forward demodulation #[145, 4]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.45/50.75 (Or (Eq (observational_period a) False) (Or (Eq True False) (Eq (environment (skS.0 0 a a_1)) True))) % 50.45/50.75 Clause #147 (by clausification #[146]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.45/50.75 (Or (Eq (observational_period a) False) (Eq (environment (skS.0 0 a a_1)) True)) % 50.45/50.75 Clause #148 (by superposition #[147, 69]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a)) True) % 50.45/50.75 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) True) (Eq False True)) % 50.45/50.75 Clause #149 (by forward demodulation #[27, 5]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.45/50.75 (Or (Eq True False) % 50.45/50.75 (Or (Eq (observational_period a) False) % 50.45/50.75 (Or (Eq (propagation_strategy first_movers) False) % 50.45/50.75 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) False)))) % 50.45/50.75 Clause #150 (by clausification #[149]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.45/50.75 (Or (Eq (observational_period a) False) % 50.45/50.75 (Or (Eq (propagation_strategy first_movers) False) % 50.45/50.75 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) False))) % 50.45/50.75 Clause #151 (by forward demodulation #[150, 4]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.45/50.75 (Or (Eq (observational_period a) False) % 50.45/50.75 (Or (Eq True False) (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) False))) % 50.45/50.75 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers a) True) % 50.45/50.75 (Or (Eq (observational_period a) False) % 50.45/50.75 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) False)) % 50.45/50.75 Clause #153 (by superposition #[152, 69]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a)) True) % 50.45/50.75 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.45/50.75 (Eq False True)) % 50.45/50.75 Clause #154 (by superposition #[106, 69]): ∀ (a a_1 a_2 : Iota), % 50.45/50.75 Or (Eq (slow_change (skS.0 1 a)) False) % 50.45/50.75 (Or (Eq (environment a_1) False) % 50.45/50.75 (Or (Eq (in_environment (skS.0 1 a) a_1) False) % 50.45/50.75 (Or (Eq (in_environment a_1 (skS.0 2 a_1 a_2)) True) (Eq False True)))) % 50.45/50.75 Clause #155 (by clausification #[148]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a)) True) % 50.45/50.75 (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) True) % 50.45/50.75 Clause #156 (by forward demodulation #[155, 67]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) True) % 50.45/50.75 Clause #157 (by clausification #[156]): ∀ (a a_1 : Iota), Eq (environment (skS.0 0 (skS.0 1 a) a_1)) True % 50.45/50.75 Clause #158 (by superposition #[157, 42]): ∀ (a a_1 a_2 : Iota), % 50.45/50.75 Or (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) a_2) True) % 50.45/50.75 (Or (Eq True False) (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) a_2) False)) % 50.45/50.75 Clause #160 (by superposition #[157, 62]): ∀ (a a_1 : Iota), % 50.45/50.75 Or (Eq True False) % 50.45/50.75 (Eq (greater_or_equal (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.55/50.81 Clause #161 (by superposition #[157, 87]): ∀ (a a_1 : Iota), % 50.55/50.81 Or (Eq True False) % 50.55/50.81 (Eq % 50.55/50.81 (greater_or_equal (critical_point (skS.0 0 (skS.0 1 a) a_1)) % 50.55/50.81 (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.55/50.81 True) % 50.55/50.81 Clause #162 (by superposition #[157, 91]): ∀ (a a_1 a_2 : Iota), % 50.55/50.81 Or (Eq (greater_or_equal (cardinality_at_time first_movers a) zero) True) % 50.55/50.81 (Or (Eq True False) (Eq (in_environment (skS.0 0 (skS.0 1 a_1) a_2) a) False)) % 50.55/50.81 Clause #163 (by superposition #[157, 112]): ∀ (a a_1 a_2 : Iota), % 50.55/50.81 Or (Eq True False) % 50.55/50.81 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) a_2) False) % 50.55/50.81 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) a_2) True)) % 50.55/50.81 Clause #164 (by superposition #[157, 113]): ∀ (a a_1 a_2 : Iota), % 50.55/50.81 Or (Eq True False) % 50.55/50.81 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) a_2) False) % 50.55/50.81 (Eq (subpopulation first_movers (skS.0 0 (skS.0 1 a) a_1) a_2) True)) % 50.55/50.81 Clause #165 (by superposition #[157, 137]): ∀ (a a_1 a_2 : Iota), % 50.55/50.81 Or (Eq True False) % 50.55/50.81 (Or (Eq (greater (growth_rate efficient_producers a) (growth_rate first_movers a)) True) % 50.55/50.81 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_1) a_2) a) False) % 50.55/50.81 (Eq (greater a (critical_point (skS.0 0 (skS.0 1 a_1) a_2))) False))) % 50.55/50.81 Clause #166 (by superposition #[157, 139]): ∀ (a a_1 : Iota), % 50.55/50.81 Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.55/50.81 (Or (Eq True False) % 50.55/50.81 (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) False)) % 50.55/50.81 Clause #169 (by clausification #[162]): ∀ (a a_1 a_2 : Iota), % 50.55/50.81 Or (Eq (greater_or_equal (cardinality_at_time first_movers a) zero) True) % 50.55/50.81 (Eq (in_environment (skS.0 0 (skS.0 1 a_1) a_2) a) False) % 50.55/50.81 Clause #170 (by clausification #[153]): ∀ (a a_1 : Iota), % 50.55/50.81 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a)) True) % 50.55/50.81 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.55/50.81 Clause #171 (by forward demodulation #[170, 67]): ∀ (a a_1 : Iota), % 50.55/50.81 Or (Eq False True) (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.55/50.81 Clause #172 (by clausification #[171]): ∀ (a a_1 : Iota), Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) False % 50.55/50.81 Clause #173 (by clausification #[160]): ∀ (a a_1 : Iota), % 50.55/50.81 Eq (greater_or_equal (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) True % 50.55/50.81 Clause #174 (by superposition #[173, 125]): ∀ (a a_1 : Iota), % 50.55/50.81 Or (Eq True False) % 50.55/50.81 (Or (Eq (greater (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.55/50.81 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1)))) % 50.55/50.81 Clause #175 (by clausification #[70]): ∀ (a a_1 : Iota), % 50.55/50.81 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a)) True) % 50.55/50.81 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) a_1)) True) % 50.55/50.81 Clause #176 (by forward demodulation #[175, 67]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) a_1)) True) % 50.55/50.81 Clause #177 (by clausification #[176]): ∀ (a a_1 : Iota), Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) a_1)) True % 50.55/50.81 Clause #178 (by clausification #[161]): ∀ (a a_1 : Iota), % 50.55/50.81 Eq % 50.55/50.81 (greater_or_equal (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.55/50.81 True % 50.55/50.81 Clause #180 (by superposition #[178, 125]): ∀ (a a_1 : Iota), % 50.55/50.81 Or (Eq True False) % 50.55/50.81 (Or % 50.55/50.81 (Eq (greater (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.55/50.81 True) % 50.55/50.81 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1)))) % 50.55/50.81 Clause #181 (by clausification #[154]): ∀ (a a_1 a_2 : Iota), % 50.55/50.81 Or (Eq (slow_change (skS.0 1 a)) False) % 50.55/50.81 (Or (Eq (environment a_1) False) % 50.55/50.81 (Or (Eq (in_environment (skS.0 1 a) a_1) False) (Eq (in_environment a_1 (skS.0 2 a_1 a_2)) True))) % 50.55/50.87 Clause #182 (by forward demodulation #[181, 68]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq True False) % 50.55/50.87 (Or (Eq (environment a) False) % 50.55/50.87 (Or (Eq (in_environment (skS.0 1 a_1) a) False) (Eq (in_environment a (skS.0 2 a a_2)) True))) % 50.55/50.87 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq (environment a) False) % 50.55/50.87 (Or (Eq (in_environment (skS.0 1 a_1) a) False) (Eq (in_environment a (skS.0 2 a a_2)) True)) % 50.55/50.87 Clause #184 (by superposition #[183, 157]): ∀ (a a_1 a_2 a_3 : Iota), % 50.55/50.87 Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a_1) a_2)) False) % 50.55/50.87 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a_1) a_2) (skS.0 2 (skS.0 0 (skS.0 1 a_1) a_2) a_3)) True) % 50.55/50.87 (Eq False True)) % 50.55/50.87 Clause #185 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq (slow_change (skS.0 1 a)) False) % 50.55/50.87 (Or (Eq (environment a_1) False) % 50.55/50.87 (Or (Eq (in_environment (skS.0 1 a) a_1) False) (Eq (greater (skS.0 2 a_1 a_2) (critical_point a_1)) True))) % 50.55/50.87 Clause #186 (by forward demodulation #[185, 68]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq True False) % 50.55/50.87 (Or (Eq (environment a) False) % 50.55/50.87 (Or (Eq (in_environment (skS.0 1 a_1) a) False) (Eq (greater (skS.0 2 a a_2) (critical_point a)) True))) % 50.55/50.87 Clause #187 (by clausification #[186]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq (environment a) False) % 50.55/50.87 (Or (Eq (in_environment (skS.0 1 a_1) a) False) (Eq (greater (skS.0 2 a a_2) (critical_point a)) True)) % 50.55/50.87 Clause #188 (by superposition #[187, 157]): ∀ (a a_1 a_2 a_3 : Iota), % 50.55/50.87 Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a_1) a_2)) False) % 50.55/50.87 (Or (Eq (greater (skS.0 2 (skS.0 0 (skS.0 1 a_1) a_2) a_3) (critical_point (skS.0 0 (skS.0 1 a_1) a_2))) True) % 50.55/50.87 (Eq False True)) % 50.55/50.87 Clause #189 (by clausification #[164]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) a_2) False) % 50.55/50.87 (Eq (subpopulation first_movers (skS.0 0 (skS.0 1 a) a_1) a_2) True) % 50.55/50.87 Clause #190 (by clausification #[163]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) a_2) False) % 50.55/50.87 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) a_2) True) % 50.55/50.87 Clause #191 (by clausification #[158]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) a_2) True) % 50.55/50.87 (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) a_2) False) % 50.55/50.87 Clause #193 (by clausification #[165]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq (greater (growth_rate efficient_producers a) (growth_rate first_movers a)) True) % 50.55/50.87 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_1) a_2) a) False) % 50.55/50.87 (Eq (greater a (critical_point (skS.0 0 (skS.0 1 a_1) a_2))) False)) % 50.55/50.87 Clause #196 (by clausification #[184]): ∀ (a a_1 a_2 a_3 : Iota), % 50.55/50.87 Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a_1) a_2)) False) % 50.55/50.87 (Eq (in_environment (skS.0 0 (skS.0 1 a_1) a_2) (skS.0 2 (skS.0 0 (skS.0 1 a_1) a_2) a_3)) True) % 50.55/50.87 Clause #197 (by superposition #[196, 177]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) True) (Eq False True) % 50.55/50.87 Clause #198 (by clausification #[166]): ∀ (a a_1 : Iota), % 50.55/50.87 Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.55/50.87 (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.55/50.87 Clause #199 (by clausification #[197]): ∀ (a a_1 a_2 : Iota), Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) True % 50.55/50.87 Clause #203 (by superposition #[199, 191]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) True) % 50.55/50.87 (Eq True False) % 50.55/50.87 Clause #206 (by clausification #[203]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) True % 50.55/50.87 Clause #208 (by superposition #[206, 125]): ∀ (a a_1 a_2 : Iota), % 50.55/50.87 Or (Eq True False) % 50.55/50.87 (Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) True) % 50.55/50.87 (Eq (end_time (skS.0 0 (skS.0 1 a) a_1)) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2))) % 50.65/50.93 Clause #211 (by clausification #[174]): ∀ (a a_1 : Iota), % 50.65/50.93 Or (Eq (greater (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/50.93 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/50.93 Clause #221 (by clausification #[188]): ∀ (a a_1 a_2 a_3 : Iota), % 50.65/50.93 Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a_1) a_2)) False) % 50.65/50.93 (Eq (greater (skS.0 2 (skS.0 0 (skS.0 1 a_1) a_2) a_3) (critical_point (skS.0 0 (skS.0 1 a_1) a_2))) True) % 50.65/50.93 Clause #222 (by superposition #[221, 177]): ∀ (a a_1 a_2 : Iota), % 50.65/50.93 Or (Eq (greater (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2) (critical_point (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/50.93 (Eq False True) % 50.65/50.93 Clause #223 (by clausification #[222]): ∀ (a a_1 a_2 : Iota), % 50.65/50.93 Eq (greater (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2) (critical_point (skS.0 0 (skS.0 1 a) a_1))) True % 50.65/50.93 Clause #234 (by clausification #[180]): ∀ (a a_1 : Iota), % 50.65/50.93 Or % 50.65/50.93 (Eq (greater (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.65/50.93 True) % 50.65/50.93 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.65/50.93 Clause #252 (by clausification #[208]): ∀ (a a_1 a_2 : Iota), % 50.65/50.93 Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) True) % 50.65/50.93 (Eq (end_time (skS.0 0 (skS.0 1 a) a_1)) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) % 50.65/50.93 Clause #253 (by superposition #[252, 60]): ∀ (a a_1 a_2 a_3 : Iota), % 50.65/50.93 Or (Eq (end_time (skS.0 0 (skS.0 1 a) a_1)) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) % 50.65/50.93 (Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) a_3) True) % 50.65/50.93 (Or (Eq True False) (Eq (greater (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2) a_3) False))) % 50.65/50.93 Clause #265 (by clausification #[253]): ∀ (a a_1 a_2 a_3 : Iota), % 50.65/50.93 Or (Eq (end_time (skS.0 0 (skS.0 1 a) a_1)) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) % 50.65/50.93 (Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) a_3) True) % 50.65/50.93 (Eq (greater (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2) a_3) False)) % 50.65/50.93 Clause #266 (by superposition #[265, 223]): ∀ (a a_1 a_2 : Iota), % 50.65/50.93 Or (Eq (end_time (skS.0 0 (skS.0 1 a) a_1)) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) % 50.65/50.93 (Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/50.93 (Eq False True)) % 50.65/50.93 Clause #269 (by clausification #[266]): ∀ (a a_1 a_2 : Iota), % 50.65/50.93 Or (Eq (end_time (skS.0 0 (skS.0 1 a) a_1)) (skS.0 2 (skS.0 0 (skS.0 1 a) a_1) a_2)) % 50.65/50.93 (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/50.93 Clause #276 (by superposition #[269, 223]): ∀ (a a_1 : Iota), % 50.65/50.93 Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/50.93 (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/50.93 Clause #298 (by eliminate duplicate literals #[276]): ∀ (a a_1 : Iota), Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) True % 50.65/50.93 Clause #300 (by superposition #[298, 60]): ∀ (a a_1 a_2 : Iota), % 50.65/50.93 Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) a_2) True) % 50.65/50.93 (Or (Eq True False) (Eq (greater (critical_point (skS.0 0 (skS.0 1 a) a_1)) a_2) False)) % 50.65/50.93 Clause #301 (by superposition #[298, 119]): ∀ (a a_1 : Iota), % 50.65/50.93 Or (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/50.93 (Eq True False) % 50.65/50.93 Clause #302 (by clausification #[301]): ∀ (a a_1 : Iota), % 50.65/50.93 Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) True % 50.65/50.93 Clause #306 (by clausification #[300]): ∀ (a a_1 a_2 : Iota), % 50.65/50.93 Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) a_2) True) % 50.65/50.93 (Eq (greater (critical_point (skS.0 0 (skS.0 1 a) a_1)) a_2) False) % 50.65/50.93 Clause #307 (by superposition #[306, 211]): ∀ (a a_1 : Iota), % 50.65/50.93 Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/50.93 (Or (Eq False True) (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1)))) % 50.65/51.00 Clause #308 (by superposition #[306, 234]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/51.00 (Or (Eq False True) % 50.65/51.00 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1)))) % 50.65/51.00 Clause #310 (by clausification #[307]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/51.00 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 Clause #313 (by superposition #[310, 119]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Or (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/51.00 (Eq True False)) % 50.65/51.00 Clause #314 (by clausification #[313]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/51.00 Clause #315 (by superposition #[314, 198]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True) (Eq True False)) % 50.65/51.00 Clause #319 (by clausification #[315]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/51.00 Clause #320 (by superposition #[319, 169]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Or (Eq (greater_or_equal (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 50.65/51.00 (Eq True False)) % 50.65/51.00 Clause #321 (by superposition #[319, 189]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Or (Eq True False) % 50.65/51.00 (Eq (subpopulation first_movers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True)) % 50.65/51.00 Clause #322 (by superposition #[319, 190]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Or (Eq True False) % 50.65/51.00 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True)) % 50.65/51.00 Clause #324 (by clausification #[320]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Eq (greater_or_equal (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 50.65/51.00 Clause #325 (by superposition #[324, 125]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Or (Eq True False) % 50.65/51.00 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 50.65/51.00 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))) % 50.65/51.00 Clause #326 (by clausification #[322]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/51.00 Clause #327 (by clausification #[321]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 (Eq (subpopulation first_movers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/51.00 Clause #345 (by clausification #[308]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) True) % 50.65/51.00 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.65/51.00 Clause #347 (by superposition #[345, 119]): ∀ (a a_1 : Iota), % 50.65/51.00 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Or % 50.78/51.05 (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 True) % 50.78/51.05 (Eq True False)) % 50.78/51.05 Clause #348 (by clausification #[347]): ∀ (a a_1 : Iota), % 50.78/51.05 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 True) % 50.78/51.05 Clause #349 (by superposition #[348, 85]): ∀ (a a_1 : Iota), % 50.78/51.05 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 50.78/51.05 (Or (Eq True False) % 50.78/51.05 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 50.78/51.05 (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 50.78/51.05 Clause #359 (by clausification #[325]): ∀ (a a_1 : Iota), % 50.78/51.05 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 50.78/51.05 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)) % 50.78/51.05 Clause #428 (by clausification #[349]): ∀ (a a_1 : Iota), % 50.78/51.05 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 50.78/51.05 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 50.78/51.05 (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 50.78/51.05 Clause #429 (by forward demodulation #[428, 157]): ∀ (a a_1 : Iota), % 50.78/51.05 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 50.78/51.05 (Or (Eq True False) (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 50.78/51.05 Clause #430 (by clausification #[429]): ∀ (a a_1 : Iota), % 50.78/51.05 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 50.78/51.05 (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False)) % 50.78/51.05 Clause #431 (by superposition #[430, 319]): ∀ (a a_1 : Iota), % 50.78/51.05 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 50.78/51.05 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) (Eq False True))) % 50.78/51.05 Clause #432 (by clausification #[431]): ∀ (a a_1 : Iota), % 50.78/51.05 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 50.78/51.05 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1)))) % 50.78/51.05 Clause #433 (by superposition #[432, 80]): ∀ (a a_1 a_2 a_3 : Iota), % 50.78/51.05 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.05 (Or (Eq (selection_favors efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.78/51.05 (Or (Eq True False) % 50.78/51.05 (Or (Ne (cardinality_at_time a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.78/51.05 (Or (Eq (subpopulation a_2 a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.78/51.05 (Or (Eq (environment a_3) False) % 50.78/51.05 (Eq (subpopulation efficient_producers a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))))) % 50.78/51.11 Clause #434 (by superposition #[432, 97]): ∀ (a a_1 a_2 : Iota), % 50.78/51.11 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.78/51.11 (Or (Eq True False) % 50.78/51.11 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) False) % 50.78/51.11 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))))) % 50.78/51.11 Clause #469 (by clausification #[434]): ∀ (a a_1 a_2 : Iota), % 50.78/51.11 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.78/51.11 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) False) % 50.78/51.11 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 50.78/51.11 Clause #470 (by superposition #[469, 359]): ∀ (a a_1 a_2 : Iota), % 50.78/51.11 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.78/51.11 (Or (Eq (environment a_2) False) % 50.78/51.11 (Or (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.78/51.11 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq False True) % 50.78/51.11 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))))))) % 50.78/51.11 Clause #477 (by clausification #[433]): ∀ (a a_1 a_2 a_3 : Iota), % 50.78/51.11 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (selection_favors efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.78/51.11 (Or (Ne (cardinality_at_time a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.78/51.11 (Or (Eq (subpopulation a_2 a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.78/51.11 (Or (Eq (environment a_3) False) % 50.78/51.11 (Eq (subpopulation efficient_producers a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))))) % 50.78/51.11 Clause #484 (by clausification #[470]): ∀ (a a_1 a_2 : Iota), % 50.78/51.11 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.78/51.11 (Or (Eq (environment a_2) False) % 50.78/51.11 (Or (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.78/51.11 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)))))) % 50.78/51.11 Clause #485 (by eliminate duplicate literals #[484]): ∀ (a a_1 a_2 : Iota), % 50.78/51.11 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.78/51.11 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.78/51.11 (Or (Eq (environment a_2) False) % 50.78/51.11 (Or (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.78/51.11 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))))) % 50.78/51.11 Clause #486 (by superposition #[485, 157]): ∀ (a a_1 a_2 a_3 : Iota), % 50.78/51.11 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or % 50.88/51.16 (Eq % 50.88/51.16 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 50.88/51.16 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 True) % 50.88/51.16 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a_2) a_3) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.88/51.16 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) (Eq False True))))) % 50.88/51.16 Clause #496 (by clausification #[486]): ∀ (a a_1 a_2 a_3 : Iota), % 50.88/51.16 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or % 50.88/51.16 (Eq % 50.88/51.16 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 50.88/51.16 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 True) % 50.88/51.16 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a_2) a_3) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.88/51.16 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)))) % 50.88/51.16 Clause #497 (by superposition #[496, 319]): ∀ (a a_1 : Iota), % 50.88/51.16 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or % 50.88/51.16 (Eq % 50.88/51.16 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) % 50.88/51.16 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 True) % 50.88/51.16 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.88/51.16 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) (Eq False True))))) % 50.88/51.16 Clause #498 (by clausification #[497]): ∀ (a a_1 : Iota), % 50.88/51.16 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or % 50.88/51.16 (Eq % 50.88/51.16 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) % 50.88/51.16 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 True) % 50.88/51.16 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.88/51.16 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1)))))) % 50.88/51.16 Clause #499 (by eliminate duplicate literals #[498]): ∀ (a a_1 : Iota), % 50.88/51.16 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or % 50.88/51.16 (Eq % 50.88/51.16 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) % 50.88/51.16 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 True) % 50.88/51.16 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))) % 50.88/51.16 Clause #500 (by superposition #[499, 193]): ∀ (a a_1 : Iota), % 50.88/51.16 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.88/51.16 (Or % 50.88/51.16 (Eq % 50.88/51.16 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 50.88/51.16 True) % 50.88/51.16 (Or (Eq True False) % 50.88/51.16 (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) False))))) % 50.88/51.16 Clause #501 (by clausification #[500]): ∀ (a a_1 : Iota), % 50.88/51.16 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.88/51.16 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.22 (Or % 50.95/51.22 (Eq % 50.95/51.22 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 50.95/51.22 True) % 50.95/51.22 (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) False)))) % 50.95/51.22 Clause #502 (by forward demodulation #[501, 298]): ∀ (a a_1 : Iota), % 50.95/51.22 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.22 (Or % 50.95/51.22 (Eq % 50.95/51.22 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 50.95/51.22 True) % 50.95/51.22 (Eq True False)))) % 50.95/51.22 Clause #503 (by clausification #[502]): ∀ (a a_1 : Iota), % 50.95/51.22 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.22 (Eq % 50.95/51.22 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 50.95/51.22 True))) % 50.95/51.22 Clause #504 (by superposition #[503, 49]): ∀ (a a_1 a_2 : Iota), % 50.95/51.22 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.22 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.95/51.22 (Or (Eq True False) % 50.95/51.22 (Or (Eq (environment a_2) False) % 50.95/51.22 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))))) % 50.95/51.22 Clause #510 (by clausification #[504]): ∀ (a a_1 a_2 : Iota), % 50.95/51.22 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.22 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.95/51.22 (Or (Eq (environment a_2) False) % 50.95/51.22 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 50.95/51.22 Clause #511 (by forward demodulation #[510, 172]): ∀ (a a_1 a_2 : Iota), % 50.95/51.22 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.22 (Or (Eq False True) % 50.95/51.22 (Or (Eq (environment a_2) False) % 50.95/51.22 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 50.95/51.22 Clause #512 (by clausification #[511]): ∀ (a a_1 a_2 : Iota), % 50.95/51.22 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.22 (Or (Eq (environment a_2) False) % 50.95/51.22 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 50.95/51.22 Clause #513 (by superposition #[512, 157]): ∀ (a a_1 a_2 a_3 : Iota), % 50.95/51.22 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.22 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.27 (Or % 50.95/51.27 (Eq % 50.95/51.27 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 50.95/51.27 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 False) % 50.95/51.27 (Eq False True)))) % 50.95/51.27 Clause #515 (by clausification #[513]): ∀ (a a_1 a_2 a_3 : Iota), % 50.95/51.27 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.27 (Eq % 50.95/51.27 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 50.95/51.27 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 False))) % 50.95/51.27 Clause #516 (by superposition #[515, 499]): ∀ (a a_1 : Iota), % 50.95/51.27 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq False True) (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)))))) % 50.95/51.27 Clause #518 (by clausification #[516]): ∀ (a a_1 : Iota), % 50.95/51.27 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))))) % 50.95/51.27 Clause #519 (by eliminate duplicate literals #[518]): ∀ (a a_1 : Iota), % 50.95/51.27 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)) % 50.95/51.27 Clause #522 (by superposition #[519, 477]): ∀ (a a_1 a_2 : Iota), % 50.95/51.27 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.95/51.27 (Or (Ne zero zero) % 50.95/51.27 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.95/51.27 (Or (Eq (environment a_2) False) % 50.95/51.27 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))))))) % 50.95/51.27 Clause #527 (by eliminate duplicate literals #[522]): ∀ (a a_1 a_2 : Iota), % 50.95/51.27 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 50.95/51.27 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 50.95/51.27 (Or (Ne zero zero) % 50.95/51.27 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 50.95/51.27 (Or (Eq (environment a_2) False) % 51.05/51.32 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))))) % 51.05/51.32 Clause #528 (by eliminate resolved literals #[527]): ∀ (a a_1 a_2 : Iota), % 51.05/51.32 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.05/51.32 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.05/51.32 (Or (Eq (environment a_2) False) % 51.05/51.32 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 51.05/51.32 Clause #529 (by forward demodulation #[528, 172]): ∀ (a a_1 a_2 : Iota), % 51.05/51.32 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq False True) % 51.05/51.32 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.05/51.32 (Or (Eq (environment a_2) False) % 51.05/51.32 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 51.05/51.32 Clause #530 (by clausification #[529]): ∀ (a a_1 a_2 : Iota), % 51.05/51.32 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.05/51.32 (Or (Eq (environment a_2) False) % 51.05/51.32 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.05/51.32 Clause #531 (by superposition #[530, 327]): ∀ (a a_1 : Iota), % 51.05/51.32 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.05/51.32 (Or % 51.05/51.32 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.05/51.32 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) (Eq False True))))) % 51.05/51.32 Clause #532 (by clausification #[531]): ∀ (a a_1 : Iota), % 51.05/51.32 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.05/51.32 (Or % 51.05/51.32 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.05/51.32 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1)))))) % 51.05/51.32 Clause #533 (by eliminate duplicate literals #[532]): ∀ (a a_1 : Iota), % 51.05/51.32 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.05/51.32 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.05/51.32 Clause #534 (by forward demodulation #[533, 157]): ∀ (a a_1 : Iota), % 51.05/51.32 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq True False) % 51.05/51.32 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.05/51.32 Clause #535 (by clausification #[534]): ∀ (a a_1 : Iota), % 51.05/51.32 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.32 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False)) % 51.05/51.38 Clause #536 (by superposition #[535, 326]): ∀ (a a_1 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) (Eq False True))) % 51.05/51.38 Clause #537 (by clausification #[536]): ∀ (a a_1 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.05/51.38 Clause #538 (by eliminate duplicate literals #[537]): ∀ (a a_1 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 Clause #541 (by superposition #[538, 85]): ∀ (a a_1 a_2 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Or (Eq (greater (cardinality_at_time efficient_producers a_2) zero) True) % 51.05/51.38 (Or (Eq (greater_or_equal a_2 (critical_point (skS.0 0 (skS.0 1 a) a_1))) False) % 51.05/51.38 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.05/51.38 (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) a_2) False)))) % 51.05/51.38 Clause #543 (by forward demodulation #[541, 157]): ∀ (a a_1 a_2 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Or (Eq (greater (cardinality_at_time efficient_producers a_2) zero) True) % 51.05/51.38 (Or (Eq (greater_or_equal a_2 (critical_point (skS.0 0 (skS.0 1 a) a_1))) False) % 51.05/51.38 (Or (Eq True False) (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) a_2) False)))) % 51.05/51.38 Clause #544 (by clausification #[543]): ∀ (a a_1 a_2 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Or (Eq (greater (cardinality_at_time efficient_producers a_2) zero) True) % 51.05/51.38 (Or (Eq (greater_or_equal a_2 (critical_point (skS.0 0 (skS.0 1 a) a_1))) False) % 51.05/51.38 (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) a_2) False))) % 51.05/51.38 Clause #546 (by superposition #[544, 302]): ∀ (a a_1 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.05/51.38 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) (Eq False True))) % 51.05/51.38 Clause #548 (by clausification #[546]): ∀ (a a_1 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.05/51.38 (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False)) % 51.05/51.38 Clause #549 (by superposition #[548, 319]): ∀ (a a_1 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.05/51.38 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) (Eq False True))) % 51.05/51.38 Clause #550 (by clausification #[549]): ∀ (a a_1 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.05/51.38 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.05/51.38 Clause #551 (by eliminate duplicate literals #[550]): ∀ (a a_1 : Iota), % 51.05/51.38 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.05/51.38 (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.15/51.44 Clause #552 (by superposition #[551, 80]): ∀ (a a_1 a_2 a_3 : Iota), % 51.15/51.44 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.44 (Or (Eq (selection_favors efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.15/51.44 (Or (Eq True False) % 51.15/51.44 (Or (Ne (cardinality_at_time a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.15/51.44 (Or (Eq (subpopulation a_2 a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.15/51.44 (Or (Eq (environment a_3) False) % 51.15/51.44 (Eq (subpopulation efficient_producers a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))))) % 51.15/51.44 Clause #553 (by superposition #[551, 97]): ∀ (a a_1 a_2 : Iota), % 51.15/51.44 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.44 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.15/51.44 (Or (Eq True False) % 51.15/51.44 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) False) % 51.15/51.44 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 51.15/51.44 Clause #571 (by clausification #[552]): ∀ (a a_1 a_2 a_3 : Iota), % 51.15/51.44 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.44 (Or (Eq (selection_favors efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.15/51.44 (Or (Ne (cardinality_at_time a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.15/51.44 (Or (Eq (subpopulation a_2 a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.15/51.44 (Or (Eq (environment a_3) False) % 51.15/51.44 (Eq (subpopulation efficient_producers a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 51.15/51.44 Clause #572 (by clausification #[553]): ∀ (a a_1 a_2 : Iota), % 51.15/51.44 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.44 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.15/51.44 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) False) % 51.15/51.44 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.15/51.44 Clause #573 (by superposition #[572, 359]): ∀ (a a_1 a_2 : Iota), % 51.15/51.44 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.44 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.15/51.44 (Or (Eq (environment a_2) False) % 51.15/51.44 (Or (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.15/51.44 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.44 (Or (Eq False True) (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)))))) % 51.15/51.44 Clause #578 (by clausification #[573]): ∀ (a a_1 a_2 : Iota), % 51.15/51.44 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.44 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.15/51.44 (Or (Eq (environment a_2) False) % 51.15/51.44 (Or (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.15/51.44 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.44 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))))) % 51.15/51.44 Clause #579 (by eliminate duplicate literals #[578]): ∀ (a a_1 a_2 : Iota), % 51.15/51.44 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.44 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.15/51.44 (Or (Eq (environment a_2) False) % 51.15/51.44 (Or (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.15/51.44 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)))) % 51.15/51.44 Clause #580 (by superposition #[579, 157]): ∀ (a a_1 a_2 a_3 : Iota), % 51.15/51.44 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.44 (Or % 51.15/51.44 (Eq % 51.15/51.44 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 51.15/51.49 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 True) % 51.15/51.49 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a_2) a_3) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.15/51.49 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) (Eq False True)))) % 51.15/51.49 Clause #581 (by clausification #[580]): ∀ (a a_1 a_2 a_3 : Iota), % 51.15/51.49 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (Or % 51.15/51.49 (Eq % 51.15/51.49 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 51.15/51.49 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 True) % 51.15/51.49 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a_2) a_3) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.15/51.49 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))) % 51.15/51.49 Clause #582 (by superposition #[581, 319]): ∀ (a a_1 : Iota), % 51.15/51.49 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (Or % 51.15/51.49 (Eq % 51.15/51.49 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 True) % 51.15/51.49 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.15/51.49 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) (Eq False True)))) % 51.15/51.49 Clause #584 (by clausification #[582]): ∀ (a a_1 : Iota), % 51.15/51.49 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (Or % 51.15/51.49 (Eq % 51.15/51.49 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 True) % 51.15/51.49 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.15/51.49 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))))) % 51.15/51.49 Clause #585 (by eliminate duplicate literals #[584]): ∀ (a a_1 : Iota), % 51.15/51.49 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (Or % 51.15/51.49 (Eq % 51.15/51.49 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 True) % 51.15/51.49 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)) % 51.15/51.49 Clause #586 (by superposition #[585, 193]): ∀ (a a_1 : Iota), % 51.15/51.49 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.15/51.49 (Or % 51.15/51.49 (Eq % 51.15/51.49 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.15/51.49 True) % 51.15/51.49 (Or (Eq True False) % 51.15/51.49 (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.15/51.49 Clause #587 (by clausification #[586]): ∀ (a a_1 : Iota), % 51.15/51.49 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.15/51.49 (Or % 51.15/51.49 (Eq % 51.15/51.49 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.15/51.49 True) % 51.15/51.49 (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.15/51.49 Clause #588 (by forward demodulation #[587, 298]): ∀ (a a_1 : Iota), % 51.15/51.49 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.15/51.49 (Or % 51.15/51.49 (Eq % 51.15/51.49 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.15/51.49 True) % 51.15/51.49 (Eq True False))) % 51.15/51.49 Clause #589 (by clausification #[588]): ∀ (a a_1 : Iota), % 51.15/51.49 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.15/51.49 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.25/51.54 (Eq % 51.25/51.54 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.25/51.54 True)) % 51.25/51.54 Clause #590 (by superposition #[589, 49]): ∀ (a a_1 a_2 : Iota), % 51.25/51.54 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.25/51.54 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.25/51.54 (Or (Eq True False) % 51.25/51.54 (Or (Eq (environment a_2) False) % 51.25/51.54 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 51.25/51.54 Clause #596 (by clausification #[590]): ∀ (a a_1 a_2 : Iota), % 51.25/51.54 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.25/51.54 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.25/51.54 (Or (Eq (environment a_2) False) % 51.25/51.54 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.25/51.54 Clause #597 (by forward demodulation #[596, 172]): ∀ (a a_1 a_2 : Iota), % 51.25/51.54 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.25/51.54 (Or (Eq False True) % 51.25/51.54 (Or (Eq (environment a_2) False) % 51.25/51.54 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.25/51.54 Clause #598 (by clausification #[597]): ∀ (a a_1 a_2 : Iota), % 51.25/51.54 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.25/51.54 (Or (Eq (environment a_2) False) % 51.25/51.54 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.25/51.54 Clause #599 (by superposition #[598, 157]): ∀ (a a_1 a_2 a_3 : Iota), % 51.25/51.54 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.25/51.54 (Or % 51.25/51.54 (Eq % 51.25/51.54 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 51.25/51.54 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 False) % 51.25/51.54 (Eq False True))) % 51.25/51.54 Clause #602 (by clausification #[599]): ∀ (a a_1 a_2 a_3 : Iota), % 51.25/51.54 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.25/51.54 (Eq % 51.25/51.54 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 51.25/51.54 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 False)) % 51.25/51.54 Clause #603 (by superposition #[602, 585]): ∀ (a a_1 : Iota), % 51.25/51.54 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.25/51.54 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Or (Eq False True) (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)))) % 51.25/51.54 Clause #606 (by clausification #[603]): ∀ (a a_1 : Iota), % 51.25/51.54 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.25/51.54 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))) % 51.25/51.54 Clause #607 (by eliminate duplicate literals #[606]): ∀ (a a_1 : Iota), % 51.25/51.54 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.25/51.54 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.35/51.60 Clause #610 (by superposition #[607, 571]): ∀ (a a_1 a_2 : Iota), % 51.35/51.60 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.60 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.60 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.35/51.60 (Or (Ne zero zero) % 51.35/51.60 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.35/51.60 (Or (Eq (environment a_2) False) % 51.35/51.60 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))))) % 51.35/51.60 Clause #616 (by eliminate duplicate literals #[610]): ∀ (a a_1 a_2 : Iota), % 51.35/51.60 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.60 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.35/51.60 (Or (Ne zero zero) % 51.35/51.60 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.35/51.60 (Or (Eq (environment a_2) False) % 51.35/51.60 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 51.35/51.60 Clause #617 (by eliminate resolved literals #[616]): ∀ (a a_1 a_2 : Iota), % 51.35/51.60 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.60 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.35/51.60 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.35/51.60 (Or (Eq (environment a_2) False) % 51.35/51.60 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.35/51.60 Clause #618 (by forward demodulation #[617, 172]): ∀ (a a_1 a_2 : Iota), % 51.35/51.60 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.60 (Or (Eq False True) % 51.35/51.60 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.35/51.60 (Or (Eq (environment a_2) False) % 51.35/51.60 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.35/51.60 Clause #619 (by clausification #[618]): ∀ (a a_1 a_2 : Iota), % 51.35/51.60 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.60 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.35/51.60 (Or (Eq (environment a_2) False) % 51.35/51.60 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.35/51.60 Clause #620 (by superposition #[619, 327]): ∀ (a a_1 : Iota), % 51.35/51.60 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.60 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.35/51.60 (Or (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.35/51.60 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) (Eq False True)))) % 51.35/51.60 Clause #621 (by clausification #[620]): ∀ (a a_1 : Iota), % 51.35/51.60 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.60 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.35/51.60 (Or (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.35/51.60 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))))) % 51.35/51.60 Clause #622 (by eliminate duplicate literals #[621]): ∀ (a a_1 : Iota), % 51.35/51.60 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.60 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.35/51.60 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False)) % 51.35/51.60 Clause #623 (by forward demodulation #[622, 157]): ∀ (a a_1 : Iota), % 51.35/51.60 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.60 (Or (Eq True False) % 51.35/51.60 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False)) % 51.35/51.60 Clause #624 (by clausification #[623]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.66 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.35/51.66 Clause #625 (by superposition #[624, 326]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.66 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) (Eq False True)) % 51.35/51.66 Clause #626 (by clausification #[625]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.66 (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.66 Clause #627 (by eliminate duplicate literals #[626]): ∀ (a a_1 : Iota), Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (start_time (skS.0 0 (skS.0 1 a) a_1)) % 51.35/51.66 Clause #630 (by backward demodulation #[627, 198]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.35/51.66 (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) False) % 51.35/51.66 Clause #675 (by superposition #[630, 302]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True) (Eq False True) % 51.35/51.66 Clause #676 (by clausification #[675]): ∀ (a a_1 : Iota), Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True % 51.35/51.66 Clause #678 (by superposition #[676, 430]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.66 (Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.35/51.66 (Eq True False)) % 51.35/51.66 Clause #679 (by superposition #[676, 169]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq (greater_or_equal (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.35/51.66 (Eq True False) % 51.35/51.66 Clause #680 (by superposition #[676, 189]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq True False) % 51.35/51.66 (Eq (subpopulation first_movers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.35/51.66 Clause #681 (by superposition #[676, 190]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq True False) % 51.35/51.66 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.35/51.66 Clause #683 (by clausification #[679]): ∀ (a a_1 : Iota), % 51.35/51.66 Eq (greater_or_equal (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True % 51.35/51.66 Clause #684 (by superposition #[683, 125]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq True False) % 51.35/51.66 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.35/51.66 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)) % 51.35/51.66 Clause #685 (by clausification #[681]): ∀ (a a_1 : Iota), % 51.35/51.66 Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True % 51.35/51.66 Clause #686 (by clausification #[680]): ∀ (a a_1 : Iota), Eq (subpopulation first_movers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) True % 51.35/51.66 Clause #689 (by clausification #[684]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.35/51.66 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.35/51.66 Clause #695 (by clausification #[678]): ∀ (a a_1 : Iota), % 51.35/51.66 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.66 (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.35/51.66 Clause #696 (by superposition #[695, 80]): ∀ (a a_1 a_2 a_3 : Iota), % 51.35/51.66 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.35/51.66 (Or (Eq (selection_favors efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.35/51.66 (Or (Eq True False) % 51.35/51.66 (Or (Ne (cardinality_at_time a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.45/51.71 (Or (Eq (subpopulation a_2 a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.45/51.71 (Or (Eq (environment a_3) False) % 51.45/51.71 (Eq (subpopulation efficient_producers a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))))) % 51.45/51.71 Clause #697 (by superposition #[695, 97]): ∀ (a a_1 a_2 : Iota), % 51.45/51.71 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.71 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.45/51.71 (Or (Eq True False) % 51.45/51.71 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) False) % 51.45/51.71 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 51.45/51.71 Clause #708 (by clausification #[697]): ∀ (a a_1 a_2 : Iota), % 51.45/51.71 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.71 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.45/51.71 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) False) % 51.45/51.71 (Or (Eq (environment a_2) False) (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.45/51.71 Clause #709 (by superposition #[708, 689]): ∀ (a a_1 a_2 : Iota), % 51.45/51.71 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.71 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.45/51.71 (Or (Eq (environment a_2) False) % 51.45/51.71 (Or (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.45/51.71 (Or (Eq False True) (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))))) % 51.45/51.71 Clause #710 (by clausification #[709]): ∀ (a a_1 a_2 : Iota), % 51.45/51.71 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.71 (Or (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.45/51.71 (Or (Eq (environment a_2) False) % 51.45/51.71 (Or (Eq (in_environment a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.45/51.71 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)))) % 51.45/51.71 Clause #711 (by superposition #[710, 157]): ∀ (a a_1 a_2 a_3 : Iota), % 51.45/51.71 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.71 (Or % 51.45/51.71 (Eq % 51.45/51.71 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 51.45/51.71 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.71 True) % 51.45/51.71 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a_2) a_3) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.45/51.71 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) (Eq False True)))) % 51.45/51.71 Clause #713 (by clausification #[696]): ∀ (a a_1 a_2 a_3 : Iota), % 51.45/51.71 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.71 (Or (Eq (selection_favors efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.45/51.71 (Or (Ne (cardinality_at_time a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.45/51.71 (Or (Eq (subpopulation a_2 a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.45/51.71 (Or (Eq (environment a_3) False) % 51.45/51.71 (Eq (subpopulation efficient_producers a_3 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 51.45/51.71 Clause #714 (by clausification #[711]): ∀ (a a_1 a_2 a_3 : Iota), % 51.45/51.71 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.71 (Or % 51.45/51.71 (Eq % 51.45/51.71 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 51.45/51.71 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.71 True) % 51.45/51.71 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a_2) a_3) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.45/51.71 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))) % 51.45/51.71 Clause #715 (by superposition #[714, 676]): ∀ (a a_1 : Iota), % 51.45/51.71 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (Or % 51.45/51.76 (Eq % 51.45/51.76 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 True) % 51.45/51.76 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) (Eq False True))) % 51.45/51.76 Clause #716 (by clausification #[715]): ∀ (a a_1 : Iota), % 51.45/51.76 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (Or % 51.45/51.76 (Eq % 51.45/51.76 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 True) % 51.45/51.76 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)) % 51.45/51.76 Clause #717 (by superposition #[716, 193]): ∀ (a a_1 : Iota), % 51.45/51.76 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.45/51.76 (Or % 51.45/51.76 (Eq % 51.45/51.76 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.45/51.76 True) % 51.45/51.76 (Or (Eq True False) % 51.45/51.76 (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.45/51.76 Clause #718 (by clausification #[717]): ∀ (a a_1 : Iota), % 51.45/51.76 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.45/51.76 (Or % 51.45/51.76 (Eq % 51.45/51.76 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.45/51.76 True) % 51.45/51.76 (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.45/51.76 Clause #719 (by forward demodulation #[718, 298]): ∀ (a a_1 : Iota), % 51.45/51.76 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.45/51.76 (Or % 51.45/51.76 (Eq % 51.45/51.76 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.45/51.76 True) % 51.45/51.76 (Eq True False))) % 51.45/51.76 Clause #720 (by clausification #[719]): ∀ (a a_1 : Iota), % 51.45/51.76 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.45/51.76 (Eq % 51.45/51.76 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.45/51.76 True)) % 51.45/51.76 Clause #721 (by superposition #[720, 49]): ∀ (a a_1 a_2 : Iota), % 51.45/51.76 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.45/51.76 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.45/51.76 (Or (Eq True False) % 51.45/51.76 (Or (Eq (environment a_2) False) % 51.45/51.76 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 51.45/51.76 Clause #727 (by clausification #[721]): ∀ (a a_1 a_2 : Iota), % 51.45/51.76 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.45/51.76 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.45/51.76 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.45/51.76 (Or (Eq (environment a_2) False) % 51.45/51.76 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.45/51.76 Clause #728 (by forward demodulation #[727, 172]): ∀ (a a_1 a_2 : Iota), % 51.45/51.76 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.55/51.82 (Or (Eq False True) % 51.55/51.82 (Or (Eq (environment a_2) False) % 51.55/51.82 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.55/51.82 Clause #729 (by clausification #[728]): ∀ (a a_1 a_2 : Iota), % 51.55/51.82 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.55/51.82 (Or (Eq (environment a_2) False) % 51.55/51.82 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.55/51.82 Clause #730 (by superposition #[729, 157]): ∀ (a a_1 a_2 a_3 : Iota), % 51.55/51.82 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.55/51.82 (Or % 51.55/51.82 (Eq % 51.55/51.82 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 51.55/51.82 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 False) % 51.55/51.82 (Eq False True))) % 51.55/51.82 Clause #731 (by clausification #[730]): ∀ (a a_1 a_2 a_3 : Iota), % 51.55/51.82 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.55/51.82 (Eq % 51.55/51.82 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 51.55/51.82 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 False)) % 51.55/51.82 Clause #732 (by superposition #[731, 716]): ∀ (a a_1 : Iota), % 51.55/51.82 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.55/51.82 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Or (Eq False True) (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)))) % 51.55/51.82 Clause #733 (by clausification #[732]): ∀ (a a_1 : Iota), % 51.55/51.82 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.55/51.82 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero))) % 51.55/51.82 Clause #734 (by eliminate duplicate literals #[733]): ∀ (a a_1 : Iota), % 51.55/51.82 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.55/51.82 Clause #737 (by superposition #[734, 713]): ∀ (a a_1 a_2 : Iota), % 51.55/51.82 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.55/51.82 (Or (Ne zero zero) % 51.55/51.82 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.55/51.82 (Or (Eq (environment a_2) False) % 51.55/51.82 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))))) % 51.55/51.82 Clause #742 (by eliminate duplicate literals #[737]): ∀ (a a_1 a_2 : Iota), % 51.55/51.82 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.82 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.55/51.82 (Or (Ne zero zero) % 51.55/51.82 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.55/51.82 (Or (Eq (environment a_2) False) % 51.55/51.82 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))))) % 51.55/51.82 Clause #743 (by eliminate resolved literals #[742]): ∀ (a a_1 a_2 : Iota), % 51.55/51.87 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.87 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.55/51.87 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.55/51.87 (Or (Eq (environment a_2) False) % 51.55/51.87 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.55/51.87 Clause #744 (by forward demodulation #[743, 172]): ∀ (a a_1 a_2 : Iota), % 51.55/51.87 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.87 (Or (Eq False True) % 51.55/51.87 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.55/51.87 (Or (Eq (environment a_2) False) % 51.55/51.87 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.55/51.87 Clause #745 (by clausification #[744]): ∀ (a a_1 a_2 : Iota), % 51.55/51.87 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.87 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.55/51.87 (Or (Eq (environment a_2) False) % 51.55/51.87 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.55/51.87 Clause #746 (by superposition #[745, 686]): ∀ (a a_1 : Iota), % 51.55/51.87 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.87 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.55/51.87 (Or (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.55/51.87 (Eq False True))) % 51.55/51.87 Clause #747 (by clausification #[746]): ∀ (a a_1 : Iota), % 51.55/51.87 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.87 (Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.55/51.87 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False)) % 51.55/51.87 Clause #748 (by forward demodulation #[747, 157]): ∀ (a a_1 : Iota), % 51.55/51.87 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.87 (Or (Eq True False) % 51.55/51.87 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False)) % 51.55/51.87 Clause #749 (by clausification #[748]): ∀ (a a_1 : Iota), % 51.55/51.87 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.87 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.55/51.87 Clause #750 (by superposition #[749, 685]): ∀ (a a_1 : Iota), % 51.55/51.87 Or (Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1))) % 51.55/51.87 (Eq False True) % 51.55/51.87 Clause #751 (by clausification #[750]): ∀ (a a_1 : Iota), Eq (critical_point (skS.0 0 (skS.0 1 a) a_1)) (appear efficient_producers (skS.0 0 (skS.0 1 a) a_1)) % 51.55/51.87 Clause #766 (by superposition #[751, 85]): ∀ (a a_1 a_2 : Iota), % 51.55/51.87 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 51.55/51.87 (Or (Eq (greater_or_equal a (critical_point (skS.0 0 (skS.0 1 a_1) a_2))) False) % 51.55/51.87 (Or (Eq (environment (skS.0 0 (skS.0 1 a_1) a_2)) False) % 51.55/51.87 (Eq (in_environment (skS.0 0 (skS.0 1 a_1) a_2) a) False))) % 51.55/51.87 Clause #768 (by forward demodulation #[766, 157]): ∀ (a a_1 a_2 : Iota), % 51.55/51.87 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 51.55/51.87 (Or (Eq (greater_or_equal a (critical_point (skS.0 0 (skS.0 1 a_1) a_2))) False) % 51.55/51.87 (Or (Eq True False) (Eq (in_environment (skS.0 0 (skS.0 1 a_1) a_2) a) False))) % 51.55/51.87 Clause #769 (by clausification #[768]): ∀ (a a_1 a_2 : Iota), % 51.55/51.87 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 51.55/51.87 (Or (Eq (greater_or_equal a (critical_point (skS.0 0 (skS.0 1 a_1) a_2))) False) % 51.55/51.87 (Eq (in_environment (skS.0 0 (skS.0 1 a_1) a_2) a) False)) % 51.55/51.87 Clause #771 (by superposition #[769, 302]): ∀ (a a_1 : Iota), % 51.55/51.87 Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.65/51.92 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) (Eq False True)) % 51.65/51.92 Clause #773 (by clausification #[771]): ∀ (a a_1 : Iota), % 51.65/51.92 Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.65/51.92 (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.65/51.92 Clause #774 (by superposition #[773, 676]): ∀ (a a_1 : Iota), % 51.65/51.92 Or (Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True) % 51.65/51.92 (Eq False True) % 51.65/51.92 Clause #775 (by clausification #[774]): ∀ (a a_1 : Iota), Eq (greater (cardinality_at_time efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) True % 51.65/51.92 Clause #777 (by superposition #[775, 80]): ∀ (a a_1 a_2 a_3 : Iota), % 51.65/51.92 Or (Eq (selection_favors efficient_producers a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) True) % 51.65/51.92 (Or (Eq True False) % 51.65/51.92 (Or (Ne (cardinality_at_time a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) zero) % 51.65/51.92 (Or (Eq (subpopulation a a_3 (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False) % 51.65/51.92 (Or (Eq (environment a_3) False) % 51.65/51.92 (Eq (subpopulation efficient_producers a_3 (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False))))) % 51.65/51.92 Clause #778 (by superposition #[775, 97]): ∀ (a a_1 a_2 : Iota), % 51.65/51.92 Or (Eq (subpopulations first_movers efficient_producers a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) True) % 51.65/51.92 (Or (Eq True False) % 51.65/51.92 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a_1) a_2))) zero) False) % 51.65/51.92 (Or (Eq (environment a) False) (Eq (in_environment a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False)))) % 51.65/51.92 Clause #785 (by clausification #[778]): ∀ (a a_1 a_2 : Iota), % 51.65/51.92 Or (Eq (subpopulations first_movers efficient_producers a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) True) % 51.65/51.92 (Or (Eq (greater (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a_1) a_2))) zero) False) % 51.65/51.92 (Or (Eq (environment a) False) (Eq (in_environment a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False))) % 51.65/51.92 Clause #786 (by superposition #[785, 689]): ∀ (a a_1 a_2 : Iota), % 51.65/51.92 Or (Eq (subpopulations first_movers efficient_producers a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) True) % 51.65/51.92 (Or (Eq (environment a) False) % 51.65/51.92 (Or (Eq (in_environment a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False) % 51.65/51.92 (Or (Eq False True) (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a_1) a_2))) zero)))) % 51.65/51.92 Clause #787 (by clausification #[786]): ∀ (a a_1 a_2 : Iota), % 51.65/51.92 Or (Eq (subpopulations first_movers efficient_producers a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) True) % 51.65/51.92 (Or (Eq (environment a) False) % 51.65/51.92 (Or (Eq (in_environment a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False) % 51.65/51.92 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a_1) a_2))) zero))) % 51.65/51.92 Clause #788 (by superposition #[787, 157]): ∀ (a a_1 a_2 a_3 : Iota), % 51.65/51.92 Or % 51.65/51.92 (Eq % 51.65/51.92 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a_2) a_3))) % 51.65/51.92 True) % 51.65/51.92 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a_2) a_3))) False) % 51.65/51.92 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a_2) a_3))) zero) (Eq False True))) % 51.65/51.92 Clause #801 (by clausification #[777]): ∀ (a a_1 a_2 a_3 : Iota), % 51.65/51.92 Or (Eq (selection_favors efficient_producers a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) True) % 51.65/51.92 (Or (Ne (cardinality_at_time a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) zero) % 51.65/51.92 (Or (Eq (subpopulation a a_3 (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False) % 51.65/51.92 (Or (Eq (environment a_3) False) % 51.65/51.92 (Eq (subpopulation efficient_producers a_3 (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False)))) % 51.65/51.92 Clause #806 (by clausification #[788]): ∀ (a a_1 a_2 a_3 : Iota), % 51.65/51.92 Or % 51.65/51.92 (Eq % 51.65/51.92 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a_2) a_3))) % 51.65/51.92 True) % 51.65/51.92 (Or (Eq (in_environment (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a_2) a_3))) False) % 51.65/51.97 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a_2) a_3))) zero)) % 51.65/51.97 Clause #807 (by superposition #[806, 676]): ∀ (a a_1 : Iota), % 51.65/51.97 Or % 51.65/51.97 (Eq (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.65/51.97 True) % 51.65/51.97 (Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) (Eq False True)) % 51.65/51.97 Clause #808 (by clausification #[807]): ∀ (a a_1 : Iota), % 51.65/51.97 Or % 51.65/51.97 (Eq (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.65/51.97 True) % 51.65/51.97 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.65/51.97 Clause #809 (by superposition #[808, 193]): ∀ (a a_1 : Iota), % 51.65/51.97 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.65/51.97 (Or % 51.65/51.97 (Eq % 51.65/51.97 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.65/51.97 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.65/51.97 True) % 51.65/51.97 (Or (Eq True False) % 51.65/51.97 (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.65/51.97 Clause #810 (by clausification #[809]): ∀ (a a_1 : Iota), % 51.65/51.97 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.65/51.97 (Or % 51.65/51.97 (Eq % 51.65/51.97 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.65/51.97 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.65/51.97 True) % 51.65/51.97 (Eq (greater (end_time (skS.0 0 (skS.0 1 a) a_1)) (critical_point (skS.0 0 (skS.0 1 a) a_1))) False)) % 51.65/51.97 Clause #811 (by forward demodulation #[810, 298]): ∀ (a a_1 : Iota), % 51.65/51.97 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.65/51.97 (Or % 51.65/51.97 (Eq % 51.65/51.97 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.65/51.97 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.65/51.97 True) % 51.65/51.97 (Eq True False)) % 51.65/51.97 Clause #812 (by clausification #[811]): ∀ (a a_1 : Iota), % 51.65/51.97 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.65/51.97 (Eq % 51.65/51.97 (greater (growth_rate efficient_producers (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.65/51.97 (growth_rate first_movers (end_time (skS.0 0 (skS.0 1 a) a_1)))) % 51.65/51.97 True) % 51.65/51.97 Clause #813 (by superposition #[812, 49]): ∀ (a a_1 a_2 : Iota), % 51.65/51.97 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.65/51.97 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.65/51.97 (Or (Eq True False) % 51.65/51.97 (Or (Eq (environment a_2) False) % 51.65/51.97 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.65/51.97 Clause #819 (by clausification #[813]): ∀ (a a_1 a_2 : Iota), % 51.65/51.97 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.65/51.97 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.65/51.97 (Or (Eq (environment a_2) False) % 51.65/51.97 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.65/51.97 Clause #820 (by forward demodulation #[819, 172]): ∀ (a a_1 a_2 : Iota), % 51.65/51.97 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.65/51.97 (Or (Eq False True) % 51.65/51.97 (Or (Eq (environment a_2) False) % 51.65/51.97 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.65/51.97 Clause #821 (by clausification #[820]): ∀ (a a_1 a_2 : Iota), % 51.65/51.97 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.65/51.97 (Or (Eq (environment a_2) False) % 51.65/51.97 (Eq (subpopulations first_movers efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)) % 51.65/51.97 Clause #822 (by superposition #[821, 157]): ∀ (a a_1 a_2 a_3 : Iota), % 51.65/51.97 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.65/51.97 (Or % 51.65/51.97 (Eq % 51.65/51.97 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) % 51.65/51.97 (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.78/52.02 False) % 51.78/52.02 (Eq False True)) % 51.78/52.02 Clause #823 (by clausification #[822]): ∀ (a a_1 a_2 a_3 : Iota), % 51.78/52.02 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.78/52.02 (Eq % 51.78/52.02 (subpopulations first_movers efficient_producers (skS.0 0 (skS.0 1 a_2) a_3) (end_time (skS.0 0 (skS.0 1 a) a_1))) % 51.78/52.02 False) % 51.78/52.02 Clause #824 (by superposition #[823, 808]): ∀ (a a_1 : Iota), % 51.78/52.02 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.78/52.02 (Or (Eq False True) (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero)) % 51.78/52.02 Clause #825 (by clausification #[824]): ∀ (a a_1 : Iota), % 51.78/52.02 Or (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.78/52.02 (Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero) % 51.78/52.02 Clause #826 (by eliminate duplicate literals #[825]): ∀ (a a_1 : Iota), Eq (cardinality_at_time first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) zero % 51.78/52.02 Clause #840 (by superposition #[826, 801]): ∀ (a a_1 a_2 : Iota), % 51.78/52.02 Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.78/52.02 (Or (Ne zero zero) % 51.78/52.02 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.78/52.02 (Or (Eq (environment a_2) False) % 51.78/52.02 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False)))) % 51.78/52.02 Clause #843 (by eliminate resolved literals #[840]): ∀ (a a_1 a_2 : Iota), % 51.78/52.02 Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 1 a) a_1))) True) % 51.78/52.02 (Or (Eq (subpopulation first_movers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.78/52.02 (Or (Eq (environment a_2) False) % 51.78/52.02 (Eq (subpopulation efficient_producers a_2 (end_time (skS.0 0 (skS.0 1 a) a_1))) False))) % 51.78/52.02 Clause #844 (by forward demodulation #[843, 172]): ∀ (a a_1 a_2 : Iota), % 51.78/52.02 Or (Eq False True) % 51.78/52.02 (Or (Eq (subpopulation first_movers a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False) % 51.78/52.02 (Or (Eq (environment a) False) % 51.78/52.02 (Eq (subpopulation efficient_producers a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False))) % 51.78/52.02 Clause #845 (by clausification #[844]): ∀ (a a_1 a_2 : Iota), % 51.78/52.02 Or (Eq (subpopulation first_movers a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False) % 51.78/52.02 (Or (Eq (environment a) False) % 51.78/52.02 (Eq (subpopulation efficient_producers a (end_time (skS.0 0 (skS.0 1 a_1) a_2))) False)) % 51.78/52.02 Clause #846 (by superposition #[845, 686]): ∀ (a a_1 : Iota), % 51.78/52.02 Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.78/52.02 (Or (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.78/52.02 (Eq False True)) % 51.78/52.02 Clause #847 (by clausification #[846]): ∀ (a a_1 : Iota), % 51.78/52.02 Or (Eq (environment (skS.0 0 (skS.0 1 a) a_1)) False) % 51.78/52.02 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.78/52.02 Clause #848 (by forward demodulation #[847, 157]): ∀ (a a_1 : Iota), % 51.78/52.02 Or (Eq True False) % 51.78/52.02 (Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False) % 51.78/52.02 Clause #849 (by clausification #[848]): ∀ (a a_1 : Iota), % 51.78/52.02 Eq (subpopulation efficient_producers (skS.0 0 (skS.0 1 a) a_1) (end_time (skS.0 0 (skS.0 1 a) a_1))) False % 51.78/52.02 Clause #850 (by superposition #[849, 685]): Eq False True % 51.78/52.02 Clause #853 (by clausification #[850]): False % 51.78/52.02 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------