%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT026+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:06:16 AM UTC 2026 % Result : Theorem 12.56s 12.86s % Output : Proof 13.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT026+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.05 % Command : duper %s % 0.10/0.36 % Computer : n010.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Mon Sep 7 12:11:56 UTC 2026 % 0.10/0.36 % CPUTime : % 12.56/12.86 SZS status Theorem for theBenchmark.p % 12.56/12.86 SZS output start Proof for theBenchmark.p % 12.56/12.86 Clause #0 (by assumption #[]): Eq % 12.56/12.86 (∀ (E S1 S2 T : Iota), % 12.56/12.86 And (And (environment E) (subpopulations S1 S2 E T)) (greater (growth_rate S2 T) (growth_rate S1 T)) → % 12.56/12.86 selection_favors S2 S1 T) % 12.56/12.86 True % 12.56/12.86 Clause #1 (by assumption #[]): Eq % 12.56/12.86 (∀ (E S1 S2 T : Iota), % 12.56/12.86 And % 12.56/12.86 (And (And (And (environment E) (subpopulation S1 E T)) (subpopulation S2 E T)) % 12.56/12.86 (greater (cardinality_at_time S1 T) zero)) % 12.56/12.86 (Eq (cardinality_at_time S2 T) zero) → % 12.56/12.86 selection_favors S1 S2 T) % 12.56/12.86 True % 12.56/12.86 Clause #2 (by assumption #[]): Eq % 12.56/12.86 (∀ (E T : Iota), % 12.56/12.86 And (And (And (environment E) (in_environment E T)) (greater (cardinality_at_time first_movers T) zero)) % 12.56/12.86 (greater (cardinality_at_time efficient_producers T) zero) → % 12.56/12.86 subpopulations first_movers efficient_producers E T) % 12.56/12.86 True % 12.56/12.86 Clause #3 (by assumption #[]): Eq % 12.56/12.86 (∀ (E T : Iota), % 12.56/12.86 And (environment E) (in_environment E T) → greater_or_equal (cardinality_at_time first_movers T) zero) % 12.56/12.86 True % 12.56/12.86 Clause #4 (by assumption #[]): Eq % 12.56/12.86 (∀ (E T : Iota), % 12.56/12.86 And (environment E) (in_environment E T) → % 12.56/12.86 And (subpopulation first_movers E T) (subpopulation efficient_producers E T)) % 12.56/12.86 True % 12.56/12.86 Clause #5 (by assumption #[]): Eq (∀ (E : Iota), environment E → greater_or_equal (critical_point E) (appear efficient_producers E)) True % 12.56/12.86 Clause #6 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (greater X Y) (greater Y Z) → greater X Z) True % 12.56/12.86 Clause #7 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (greater_or_equal X Y) (Or (greater X Y) (Eq X Y))) True % 12.56/12.86 Clause #8 (by assumption #[]): Eq % 12.56/12.86 (∀ (E Tc : Iota), % 12.56/12.86 And (environment E) (Eq Tc (critical_point E)) → % 12.56/12.86 And (Not (greater (growth_rate efficient_producers Tc) (growth_rate first_movers Tc))) % 12.56/12.86 (∀ (T : Iota), % 12.56/12.86 And (subpopulations first_movers efficient_producers E T) (greater T Tc) → % 12.56/12.86 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 12.56/12.86 True % 12.56/12.86 Clause #9 (by assumption #[]): Eq % 12.56/12.86 (∀ (E T : Iota), % 12.56/12.86 And (And (environment E) (in_environment E T)) (greater_or_equal T (appear efficient_producers E)) → % 12.56/12.86 greater (cardinality_at_time efficient_producers T) zero) % 12.56/12.86 True % 12.56/12.86 Clause #10 (by assumption #[]): Eq % 12.56/12.86 (Not % 12.56/12.86 (∀ (E T : Iota), % 12.56/12.86 And (And (environment E) (in_environment E T)) (greater T (critical_point E)) → % 12.56/12.86 selection_favors efficient_producers first_movers T)) % 12.56/12.86 True % 12.56/12.86 Clause #11 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (greater a Y) (greater Y Z) → greater a Z) True % 12.56/12.86 Clause #12 (by clausification #[11]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (greater a a_1) (greater a_1 Z) → greater a Z) True % 12.56/12.86 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 : Iota), Eq (And (greater a a_1) (greater a_1 a_2) → greater a a_2) True % 12.56/12.86 Clause #14 (by clausification #[13]): ∀ (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) % 12.56/12.86 Clause #15 (by clausification #[14]): ∀ (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)) % 12.56/12.86 Clause #16 (by clausification #[10]): Eq % 12.56/12.86 (∀ (E T : Iota), % 12.56/12.86 And (And (environment E) (in_environment E T)) (greater T (critical_point E)) → % 12.56/12.86 selection_favors efficient_producers first_movers T) % 12.56/12.86 False % 12.56/12.86 Clause #17 (by clausification #[16]): ∀ (a : Iota), % 12.56/12.86 Eq % 12.56/12.86 (Not % 12.56/12.86 (∀ (T : Iota), % 12.56/12.86 And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) T)) (greater T (critical_point (skS.0 0 a))) → % 12.56/12.86 selection_favors efficient_producers first_movers T)) % 12.56/12.86 True % 12.56/12.86 Clause #18 (by clausification #[17]): ∀ (a : Iota), % 12.56/12.86 Eq % 12.56/12.86 (∀ (T : Iota), % 12.56/12.86 And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) T)) (greater T (critical_point (skS.0 0 a))) → % 12.56/12.86 selection_favors efficient_producers first_movers T) % 12.56/12.86 False % 12.56/12.86 Clause #19 (by clausification #[18]): ∀ (a a_1 : Iota), % 12.56/12.86 Eq % 12.56/12.86 (Not % 12.56/12.86 (And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (skS.0 1 a a_1))) % 12.66/12.91 (greater (skS.0 1 a a_1) (critical_point (skS.0 0 a))) → % 12.66/12.91 selection_favors efficient_producers first_movers (skS.0 1 a a_1))) % 12.66/12.91 True % 12.66/12.91 Clause #20 (by clausification #[19]): ∀ (a a_1 : Iota), % 12.66/12.91 Eq % 12.66/12.91 (And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (skS.0 1 a a_1))) % 12.66/12.91 (greater (skS.0 1 a a_1) (critical_point (skS.0 0 a))) → % 12.66/12.91 selection_favors efficient_producers first_movers (skS.0 1 a a_1)) % 12.66/12.91 False % 12.66/12.91 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), % 12.66/12.91 Eq % 12.66/12.91 (And (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (skS.0 1 a a_1))) % 12.66/12.91 (greater (skS.0 1 a a_1) (critical_point (skS.0 0 a)))) % 12.66/12.91 True % 12.66/12.91 Clause #22 (by clausification #[20]): ∀ (a a_1 : Iota), Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) False % 12.66/12.91 Clause #23 (by clausification #[21]): ∀ (a a_1 : Iota), Eq (greater (skS.0 1 a a_1) (critical_point (skS.0 0 a))) True % 12.66/12.91 Clause #24 (by clausification #[21]): ∀ (a a_1 : Iota), Eq (And (environment (skS.0 0 a)) (in_environment (skS.0 0 a) (skS.0 1 a a_1))) True % 12.66/12.91 Clause #25 (by superposition #[23, 15]): ∀ (a a_1 a_2 : Iota), % 12.66/12.91 Or (Eq (greater (skS.0 1 a a_1) a_2) True) (Or (Eq True False) (Eq (greater (critical_point (skS.0 0 a)) a_2) False)) % 12.66/12.91 Clause #26 (by clausification #[3]): ∀ (a : Iota), % 12.66/12.91 Eq % 12.66/12.91 (∀ (T : Iota), % 12.66/12.91 And (environment a) (in_environment a T) → greater_or_equal (cardinality_at_time first_movers T) zero) % 12.66/12.91 True % 12.66/12.91 Clause #27 (by clausification #[26]): ∀ (a a_1 : Iota), % 12.66/12.91 Eq (And (environment a) (in_environment a a_1) → greater_or_equal (cardinality_at_time first_movers a_1) zero) True % 12.66/12.91 Clause #28 (by clausification #[27]): ∀ (a a_1 : Iota), % 12.66/12.91 Or (Eq (And (environment a) (in_environment a a_1)) False) % 12.66/12.91 (Eq (greater_or_equal (cardinality_at_time first_movers a_1) zero) True) % 12.66/12.91 Clause #29 (by clausification #[28]): ∀ (a a_1 : Iota), % 12.66/12.91 Or (Eq (greater_or_equal (cardinality_at_time first_movers a) zero) True) % 12.66/12.91 (Or (Eq (environment a_1) False) (Eq (in_environment a_1 a) False)) % 12.66/12.91 Clause #30 (by clausification #[2]): ∀ (a : Iota), % 12.66/12.91 Eq % 12.66/12.91 (∀ (T : Iota), % 12.66/12.91 And (And (And (environment a) (in_environment a T)) (greater (cardinality_at_time first_movers T) zero)) % 12.66/12.91 (greater (cardinality_at_time efficient_producers T) zero) → % 12.66/12.91 subpopulations first_movers efficient_producers a T) % 12.66/12.91 True % 12.66/12.91 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), % 12.66/12.91 Eq % 12.66/12.91 (And (And (And (environment a) (in_environment a a_1)) (greater (cardinality_at_time first_movers a_1) zero)) % 12.66/12.91 (greater (cardinality_at_time efficient_producers a_1) zero) → % 12.66/12.91 subpopulations first_movers efficient_producers a a_1) % 12.66/12.91 True % 12.66/12.91 Clause #32 (by clausification #[31]): ∀ (a a_1 : Iota), % 12.66/12.91 Or % 12.66/12.91 (Eq % 12.66/12.91 (And (And (And (environment a) (in_environment a a_1)) (greater (cardinality_at_time first_movers a_1) zero)) % 12.66/12.91 (greater (cardinality_at_time efficient_producers a_1) zero)) % 12.66/12.91 False) % 12.66/12.91 (Eq (subpopulations first_movers efficient_producers a a_1) True) % 12.66/12.91 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), % 12.66/12.91 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 12.66/12.91 (Or % 12.66/12.91 (Eq (And (And (environment a) (in_environment a a_1)) (greater (cardinality_at_time first_movers a_1) zero)) % 12.66/12.91 False) % 12.66/12.91 (Eq (greater (cardinality_at_time efficient_producers a_1) zero) False)) % 12.66/12.91 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), % 12.66/12.91 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 12.66/12.91 (Or (Eq (greater (cardinality_at_time efficient_producers a_1) zero) False) % 12.66/12.91 (Or (Eq (And (environment a) (in_environment a a_1)) False) % 12.66/12.91 (Eq (greater (cardinality_at_time first_movers a_1) zero) False))) % 12.66/12.91 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), % 12.66/12.91 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 12.66/12.91 (Or (Eq (greater (cardinality_at_time efficient_producers a_1) zero) False) % 12.66/12.91 (Or (Eq (greater (cardinality_at_time first_movers a_1) zero) False) % 12.66/12.91 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False)))) % 12.66/12.91 Clause #36 (by clausification #[5]): ∀ (a : Iota), Eq (environment a → greater_or_equal (critical_point a) (appear efficient_producers a)) True % 12.66/12.95 Clause #37 (by clausification #[36]): ∀ (a : Iota), % 12.66/12.95 Or (Eq (environment a) False) (Eq (greater_or_equal (critical_point a) (appear efficient_producers a)) True) % 12.66/12.95 Clause #38 (by clausification #[0]): ∀ (a : Iota), % 12.66/12.95 Eq % 12.66/12.95 (∀ (S1 S2 T : Iota), % 12.66/12.95 And (And (environment a) (subpopulations S1 S2 a T)) (greater (growth_rate S2 T) (growth_rate S1 T)) → % 12.66/12.95 selection_favors S2 S1 T) % 12.66/12.95 True % 12.66/12.95 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), % 12.66/12.95 Eq % 12.66/12.95 (∀ (S2 T : Iota), % 12.66/12.95 And (And (environment a) (subpopulations a_1 S2 a T)) (greater (growth_rate S2 T) (growth_rate a_1 T)) → % 12.66/12.95 selection_favors S2 a_1 T) % 12.66/12.95 True % 12.66/12.95 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 12.66/12.95 Eq % 12.66/12.95 (∀ (T : Iota), % 12.66/12.95 And (And (environment a) (subpopulations a_1 a_2 a T)) (greater (growth_rate a_2 T) (growth_rate a_1 T)) → % 12.66/12.95 selection_favors a_2 a_1 T) % 12.66/12.95 True % 12.66/12.95 Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/12.95 Eq % 12.66/12.95 (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)) → % 12.66/12.95 selection_favors a_2 a_1 a_3) % 12.66/12.95 True % 12.66/12.95 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/12.95 Or % 12.66/12.95 (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))) % 12.66/12.95 False) % 12.66/12.95 (Eq (selection_favors a_2 a_1 a_3) True) % 12.66/12.95 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/12.95 Or (Eq (selection_favors a a_1 a_2) True) % 12.66/12.95 (Or (Eq (And (environment a_3) (subpopulations a_1 a a_3 a_2)) False) % 12.66/12.95 (Eq (greater (growth_rate a a_2) (growth_rate a_1 a_2)) False)) % 12.66/12.95 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/12.95 Or (Eq (selection_favors a a_1 a_2) True) % 12.66/12.95 (Or (Eq (greater (growth_rate a a_2) (growth_rate a_1 a_2)) False) % 12.66/12.95 (Or (Eq (environment a_3) False) (Eq (subpopulations a_1 a a_3 a_2) False))) % 12.66/12.95 Clause #45 (by clausification #[9]): ∀ (a : Iota), % 12.66/12.95 Eq % 12.66/12.95 (∀ (T : Iota), % 12.66/12.95 And (And (environment a) (in_environment a T)) (greater_or_equal T (appear efficient_producers a)) → % 12.66/12.95 greater (cardinality_at_time efficient_producers T) zero) % 12.66/12.95 True % 12.66/12.95 Clause #46 (by clausification #[45]): ∀ (a a_1 : Iota), % 12.66/12.95 Eq % 12.66/12.95 (And (And (environment a) (in_environment a a_1)) (greater_or_equal a_1 (appear efficient_producers a)) → % 12.66/12.95 greater (cardinality_at_time efficient_producers a_1) zero) % 12.66/12.95 True % 12.66/12.95 Clause #47 (by clausification #[46]): ∀ (a a_1 : Iota), % 12.66/12.95 Or (Eq (And (And (environment a) (in_environment a a_1)) (greater_or_equal a_1 (appear efficient_producers a))) False) % 12.66/12.95 (Eq (greater (cardinality_at_time efficient_producers a_1) zero) True) % 12.66/12.95 Clause #48 (by clausification #[47]): ∀ (a a_1 : Iota), % 12.66/12.95 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 12.66/12.95 (Or (Eq (And (environment a_1) (in_environment a_1 a)) False) % 12.66/12.95 (Eq (greater_or_equal a (appear efficient_producers a_1)) False)) % 12.66/12.95 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), % 12.66/12.95 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 12.66/12.95 (Or (Eq (greater_or_equal a (appear efficient_producers a_1)) False) % 12.66/12.95 (Or (Eq (environment a_1) False) (Eq (in_environment a_1 a) False))) % 12.66/12.95 Clause #50 (by clausification #[1]): ∀ (a : Iota), % 12.66/12.95 Eq % 12.66/12.95 (∀ (S1 S2 T : Iota), % 12.66/12.95 And % 12.66/12.95 (And (And (And (environment a) (subpopulation S1 a T)) (subpopulation S2 a T)) % 12.66/12.95 (greater (cardinality_at_time S1 T) zero)) % 12.66/12.95 (Eq (cardinality_at_time S2 T) zero) → % 12.66/12.95 selection_favors S1 S2 T) % 12.66/12.95 True % 12.66/12.95 Clause #51 (by clausification #[50]): ∀ (a a_1 : Iota), % 12.66/12.95 Eq % 12.66/12.95 (∀ (S2 T : Iota), % 12.66/12.95 And % 12.66/12.95 (And (And (And (environment a) (subpopulation a_1 a T)) (subpopulation S2 a T)) % 12.66/12.95 (greater (cardinality_at_time a_1 T) zero)) % 12.66/12.95 (Eq (cardinality_at_time S2 T) zero) → % 12.66/12.95 selection_favors a_1 S2 T) % 12.66/12.95 True % 12.66/12.95 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), % 12.66/12.95 Eq % 12.66/12.95 (∀ (T : Iota), % 12.66/13.00 And % 12.66/13.00 (And (And (And (environment a) (subpopulation a_1 a T)) (subpopulation a_2 a T)) % 12.66/13.00 (greater (cardinality_at_time a_1 T) zero)) % 12.66/13.00 (Eq (cardinality_at_time a_2 T) zero) → % 12.66/13.00 selection_favors a_1 a_2 T) % 12.66/13.00 True % 12.66/13.00 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/13.00 Eq % 12.66/13.00 (And % 12.66/13.00 (And (And (And (environment a) (subpopulation a_1 a a_2)) (subpopulation a_3 a a_2)) % 12.66/13.00 (greater (cardinality_at_time a_1 a_2) zero)) % 12.66/13.00 (Eq (cardinality_at_time a_3 a_2) zero) → % 12.66/13.00 selection_favors a_1 a_3 a_2) % 12.66/13.00 True % 12.66/13.00 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/13.00 Or % 12.66/13.00 (Eq % 12.66/13.00 (And % 12.66/13.00 (And (And (And (environment a) (subpopulation a_1 a a_2)) (subpopulation a_3 a a_2)) % 12.66/13.00 (greater (cardinality_at_time a_1 a_2) zero)) % 12.66/13.00 (Eq (cardinality_at_time a_3 a_2) zero)) % 12.66/13.00 False) % 12.66/13.00 (Eq (selection_favors a_1 a_3 a_2) True) % 12.66/13.00 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/13.00 Or (Eq (selection_favors a a_1 a_2) True) % 12.66/13.00 (Or % 12.66/13.00 (Eq % 12.66/13.00 (And (And (And (environment a_3) (subpopulation a a_3 a_2)) (subpopulation a_1 a_3 a_2)) % 12.66/13.00 (greater (cardinality_at_time a a_2) zero)) % 12.66/13.00 False) % 12.66/13.00 (Eq (Eq (cardinality_at_time a_1 a_2) zero) False)) % 12.66/13.00 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/13.00 Or (Eq (selection_favors a a_1 a_2) True) % 12.66/13.00 (Or (Eq (Eq (cardinality_at_time a_1 a_2) zero) False) % 12.66/13.00 (Or (Eq (And (And (environment a_3) (subpopulation a a_3 a_2)) (subpopulation a_1 a_3 a_2)) False) % 12.66/13.00 (Eq (greater (cardinality_at_time a a_2) zero) False))) % 12.66/13.00 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/13.00 Or (Eq (selection_favors a a_1 a_2) True) % 12.66/13.00 (Or (Eq (And (And (environment a_3) (subpopulation a a_3 a_2)) (subpopulation a_1 a_3 a_2)) False) % 12.66/13.00 (Or (Eq (greater (cardinality_at_time a a_2) zero) False) (Ne (cardinality_at_time a_1 a_2) zero))) % 12.66/13.00 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/13.00 Or (Eq (selection_favors a a_1 a_2) True) % 12.66/13.00 (Or (Eq (greater (cardinality_at_time a a_2) zero) False) % 12.66/13.00 (Or (Ne (cardinality_at_time a_1 a_2) zero) % 12.66/13.00 (Or (Eq (And (environment a_3) (subpopulation a a_3 a_2)) False) (Eq (subpopulation a_1 a_3 a_2) False)))) % 12.66/13.00 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 a_3 : Iota), % 12.66/13.00 Or (Eq (selection_favors a a_1 a_2) True) % 12.66/13.00 (Or (Eq (greater (cardinality_at_time a a_2) zero) False) % 12.66/13.00 (Or (Ne (cardinality_at_time a_1 a_2) zero) % 12.66/13.00 (Or (Eq (subpopulation a_1 a_3 a_2) False) % 12.66/13.00 (Or (Eq (environment a_3) False) (Eq (subpopulation a a_3 a_2) False))))) % 12.66/13.00 Clause #60 (by clausification #[4]): ∀ (a : Iota), % 12.66/13.00 Eq % 12.66/13.00 (∀ (T : Iota), % 12.66/13.00 And (environment a) (in_environment a T) → % 12.66/13.00 And (subpopulation first_movers a T) (subpopulation efficient_producers a T)) % 12.66/13.00 True % 12.66/13.00 Clause #61 (by clausification #[60]): ∀ (a a_1 : Iota), % 12.66/13.00 Eq % 12.66/13.00 (And (environment a) (in_environment a a_1) → % 12.66/13.00 And (subpopulation first_movers a a_1) (subpopulation efficient_producers a a_1)) % 12.66/13.00 True % 12.66/13.00 Clause #62 (by clausification #[61]): ∀ (a a_1 : Iota), % 12.66/13.00 Or (Eq (And (environment a) (in_environment a a_1)) False) % 12.66/13.00 (Eq (And (subpopulation first_movers a a_1) (subpopulation efficient_producers a a_1)) True) % 12.66/13.00 Clause #63 (by clausification #[62]): ∀ (a a_1 : Iota), % 12.66/13.00 Or (Eq (And (subpopulation first_movers a a_1) (subpopulation efficient_producers a a_1)) True) % 12.66/13.00 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False)) % 12.66/13.00 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), % 12.66/13.00 Or (Eq (environment a) False) % 12.66/13.00 (Or (Eq (in_environment a a_1) False) (Eq (subpopulation efficient_producers a a_1) True)) % 12.66/13.00 Clause #65 (by clausification #[63]): ∀ (a a_1 : Iota), % 12.66/13.00 Or (Eq (environment a) False) (Or (Eq (in_environment a a_1) False) (Eq (subpopulation first_movers a a_1) True)) % 12.66/13.00 Clause #66 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (greater_or_equal a Y) (Or (greater a Y) (Eq a Y))) True % 12.66/13.00 Clause #67 (by clausification #[66]): ∀ (a a_1 : Iota), Eq (Iff (greater_or_equal a a_1) (Or (greater a a_1) (Eq a a_1))) True % 12.79/13.04 Clause #68 (by clausification #[67]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (Or (greater a a_1) (Eq a a_1)) False) % 12.79/13.04 Clause #69 (by clausification #[67]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Eq (Or (greater a a_1) (Eq a a_1)) True) % 12.79/13.04 Clause #71 (by clausification #[68]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (greater a a_1) False) % 12.79/13.04 Clause #75 (by superposition #[71, 23]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal (skS.0 1 a a_1) (critical_point (skS.0 0 a))) True) (Eq False True) % 12.79/13.04 Clause #76 (by clausification #[69]): ∀ (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)) % 12.79/13.04 Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Or (Eq (greater a a_1) True) (Eq a a_1)) % 12.79/13.04 Clause #80 (by clausification #[75]): ∀ (a a_1 : Iota), Eq (greater_or_equal (skS.0 1 a a_1) (critical_point (skS.0 0 a))) True % 12.79/13.04 Clause #83 (by clausification #[8]): ∀ (a : Iota), % 12.79/13.04 Eq % 12.79/13.04 (∀ (Tc : Iota), % 12.79/13.04 And (environment a) (Eq Tc (critical_point a)) → % 12.79/13.04 And (Not (greater (growth_rate efficient_producers Tc) (growth_rate first_movers Tc))) % 12.79/13.04 (∀ (T : Iota), % 12.79/13.04 And (subpopulations first_movers efficient_producers a T) (greater T Tc) → % 12.79/13.04 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 12.79/13.04 True % 12.79/13.04 Clause #84 (by clausification #[83]): ∀ (a a_1 : Iota), % 12.79/13.04 Eq % 12.79/13.04 (And (environment a) (Eq a_1 (critical_point a)) → % 12.79/13.04 And (Not (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1))) % 12.79/13.04 (∀ (T : Iota), % 12.79/13.04 And (subpopulations first_movers efficient_producers a T) (greater T a_1) → % 12.79/13.04 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 12.79/13.04 True % 12.79/13.04 Clause #85 (by clausification #[84]): ∀ (a a_1 : Iota), % 12.79/13.04 Or (Eq (And (environment a) (Eq a_1 (critical_point a))) False) % 12.79/13.04 (Eq % 12.79/13.04 (And (Not (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1))) % 12.79/13.04 (∀ (T : Iota), % 12.79/13.04 And (subpopulations first_movers efficient_producers a T) (greater T a_1) → % 12.79/13.04 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 12.79/13.04 True) % 12.79/13.04 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), % 12.79/13.04 Or % 12.79/13.04 (Eq % 12.79/13.04 (And (Not (greater (growth_rate efficient_producers a) (growth_rate first_movers a))) % 12.79/13.04 (∀ (T : Iota), % 12.79/13.04 And (subpopulations first_movers efficient_producers a_1 T) (greater T a) → % 12.79/13.04 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 12.79/13.04 True) % 12.79/13.04 (Or (Eq (environment a_1) False) (Eq (Eq a (critical_point a_1)) False)) % 12.79/13.04 Clause #87 (by clausification #[86]): ∀ (a a_1 : Iota), % 12.79/13.04 Or (Eq (environment a) False) % 12.79/13.04 (Or (Eq (Eq a_1 (critical_point a)) False) % 12.79/13.04 (Eq % 12.79/13.04 (∀ (T : Iota), % 12.79/13.04 And (subpopulations first_movers efficient_producers a T) (greater T a_1) → % 12.79/13.04 greater (growth_rate efficient_producers T) (growth_rate first_movers T)) % 12.79/13.04 True)) % 12.79/13.04 Clause #89 (by clausification #[87]): ∀ (a a_1 : Iota), % 12.79/13.04 Or (Eq (environment a) False) % 12.79/13.04 (Or % 12.79/13.04 (Eq % 12.79/13.04 (∀ (T : Iota), % 12.79/13.04 And (subpopulations first_movers efficient_producers a T) (greater T a_1) → % 12.79/13.04 greater (growth_rate efficient_producers T) (growth_rate first_movers T)) % 12.79/13.04 True) % 12.79/13.04 (Ne a_1 (critical_point a))) % 12.79/13.04 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 : Iota), % 12.79/13.04 Or (Eq (environment a) False) % 12.79/13.04 (Or (Ne a_1 (critical_point a)) % 12.79/13.04 (Eq % 12.79/13.04 (And (subpopulations first_movers efficient_producers a a_2) (greater a_2 a_1) → % 12.79/13.04 greater (growth_rate efficient_producers a_2) (growth_rate first_movers a_2)) % 12.79/13.04 True)) % 12.79/13.04 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), % 12.79/13.04 Or (Eq (environment a) False) % 12.79/13.04 (Or (Ne a_1 (critical_point a)) % 12.79/13.04 (Or (Eq (And (subpopulations first_movers efficient_producers a a_2) (greater a_2 a_1)) False) % 12.79/13.04 (Eq (greater (growth_rate efficient_producers a_2) (growth_rate first_movers a_2)) True))) % 12.79/13.09 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), % 12.79/13.09 Or (Eq (environment a) False) % 12.79/13.09 (Or (Ne a_1 (critical_point a)) % 12.79/13.09 (Or (Eq (greater (growth_rate efficient_producers a_2) (growth_rate first_movers a_2)) True) % 12.79/13.09 (Or (Eq (subpopulations first_movers efficient_producers a a_2) False) (Eq (greater a_2 a_1) False)))) % 12.79/13.09 Clause #93 (by destructive equality resolution #[92]): ∀ (a a_1 : Iota), % 12.79/13.09 Or (Eq (environment a) False) % 12.79/13.09 (Or (Eq (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1)) True) % 12.79/13.09 (Or (Eq (subpopulations first_movers efficient_producers a a_1) False) % 12.79/13.09 (Eq (greater a_1 (critical_point a)) False))) % 12.79/13.09 Clause #97 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), Or (Eq (greater (skS.0 1 a a_1) a_2) True) (Eq (greater (critical_point (skS.0 0 a)) a_2) False) % 12.79/13.09 Clause #98 (by clausification #[24]): ∀ (a a_1 : Iota), Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) True % 12.79/13.09 Clause #99 (by clausification #[24]): ∀ (a : Iota), Eq (environment (skS.0 0 a)) True % 12.79/13.09 Clause #100 (by superposition #[99, 29]): ∀ (a a_1 : Iota), % 12.79/13.09 Or (Eq (greater_or_equal (cardinality_at_time first_movers a) zero) True) % 12.79/13.09 (Or (Eq True False) (Eq (in_environment (skS.0 0 a_1) a) False)) % 12.79/13.09 Clause #101 (by superposition #[99, 37]): ∀ (a : Iota), % 12.79/13.09 Or (Eq True False) (Eq (greater_or_equal (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) True) % 12.79/13.09 Clause #102 (by superposition #[99, 64]): ∀ (a a_1 : Iota), % 12.79/13.09 Or (Eq True False) % 12.79/13.09 (Or (Eq (in_environment (skS.0 0 a) a_1) False) (Eq (subpopulation efficient_producers (skS.0 0 a) a_1) True)) % 12.79/13.09 Clause #103 (by superposition #[99, 65]): ∀ (a a_1 : Iota), % 12.79/13.09 Or (Eq True False) % 12.79/13.09 (Or (Eq (in_environment (skS.0 0 a) a_1) False) (Eq (subpopulation first_movers (skS.0 0 a) a_1) True)) % 12.79/13.09 Clause #105 (by superposition #[99, 93]): ∀ (a a_1 : Iota), % 12.79/13.09 Or (Eq True False) % 12.79/13.09 (Or (Eq (greater (growth_rate efficient_producers a) (growth_rate first_movers a)) True) % 12.79/13.09 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) a) False) % 12.79/13.09 (Eq (greater a (critical_point (skS.0 0 a_1))) False))) % 12.79/13.09 Clause #107 (by clausification #[100]): ∀ (a a_1 : Iota), % 12.79/13.09 Or (Eq (greater_or_equal (cardinality_at_time first_movers a) zero) True) (Eq (in_environment (skS.0 0 a_1) a) False) % 12.79/13.09 Clause #108 (by superposition #[107, 98]): ∀ (a a_1 : Iota), % 12.79/13.09 Or (Eq (greater_or_equal (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) True) (Eq False True) % 12.79/13.09 Clause #110 (by clausification #[108]): ∀ (a a_1 : Iota), Eq (greater_or_equal (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) True % 12.79/13.09 Clause #111 (by superposition #[110, 77]): ∀ (a a_1 : Iota), % 12.79/13.09 Or (Eq True False) % 12.79/13.09 (Or (Eq (greater (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) True) % 12.79/13.09 (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero)) % 12.79/13.09 Clause #112 (by clausification #[101]): ∀ (a : Iota), Eq (greater_or_equal (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) True % 12.79/13.09 Clause #114 (by superposition #[112, 77]): ∀ (a : Iota), % 12.79/13.09 Or (Eq True False) % 12.79/13.09 (Or (Eq (greater (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) True) % 12.79/13.09 (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a)))) % 12.79/13.09 Clause #115 (by clausification #[102]): ∀ (a a_1 : Iota), % 12.79/13.09 Or (Eq (in_environment (skS.0 0 a) a_1) False) (Eq (subpopulation efficient_producers (skS.0 0 a) a_1) True) % 12.79/13.09 Clause #116 (by superposition #[115, 98]): ∀ (a a_1 : Iota), Or (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq False True) % 12.79/13.09 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True % 12.79/13.09 Clause #118 (by clausification #[103]): ∀ (a a_1 : Iota), Or (Eq (in_environment (skS.0 0 a) a_1) False) (Eq (subpopulation first_movers (skS.0 0 a) a_1) True) % 12.79/13.09 Clause #119 (by superposition #[118, 98]): ∀ (a a_1 : Iota), Or (Eq (subpopulation first_movers (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq False True) % 12.89/13.15 Clause #121 (by clausification #[119]): ∀ (a a_1 : Iota), Eq (subpopulation first_movers (skS.0 0 a) (skS.0 1 a a_1)) True % 12.89/13.15 Clause #123 (by clausification #[111]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (greater (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) True) % 12.89/13.15 (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.89/13.15 Clause #129 (by clausification #[105]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (greater (growth_rate efficient_producers a) (growth_rate first_movers a)) True) % 12.89/13.15 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) a) False) % 12.89/13.15 (Eq (greater a (critical_point (skS.0 0 a_1))) False)) % 12.89/13.15 Clause #130 (by clausification #[114]): ∀ (a : Iota), % 12.89/13.15 Or (Eq (greater (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) True) % 12.89/13.15 (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 Clause #131 (by superposition #[130, 97]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Or (Eq (greater (skS.0 1 a a_1) (appear efficient_producers (skS.0 0 a))) True) (Eq True False)) % 12.89/13.15 Clause #135 (by clausification #[131]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Eq (greater (skS.0 1 a a_1) (appear efficient_producers (skS.0 0 a))) True) % 12.89/13.15 Clause #137 (by superposition #[135, 71]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Or (Eq (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers (skS.0 0 a))) True) (Eq True False)) % 12.89/13.15 Clause #138 (by clausification #[137]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Eq (greater_or_equal (skS.0 1 a a_1) (appear efficient_producers (skS.0 0 a))) True) % 12.89/13.15 Clause #139 (by superposition #[138, 49]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 1 a a_1)) zero) True) % 12.89/13.15 (Or (Eq True False) % 12.89/13.15 (Or (Eq (environment (skS.0 0 a)) False) (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False)))) % 12.89/13.15 Clause #148 (by clausification #[139]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 1 a a_1)) zero) True) % 12.89/13.15 (Or (Eq (environment (skS.0 0 a)) False) (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False))) % 12.89/13.15 Clause #149 (by forward demodulation #[148, 99]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 1 a a_1)) zero) True) % 12.89/13.15 (Or (Eq True False) (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False))) % 12.89/13.15 Clause #150 (by clausification #[149]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 1 a a_1)) zero) True) % 12.89/13.15 (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False)) % 12.89/13.15 Clause #151 (by superposition #[150, 98]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 1 a a_1)) zero) True) (Eq False True)) % 12.89/13.15 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Eq (greater (cardinality_at_time efficient_producers (skS.0 1 a a_1)) zero) True) % 12.89/13.15 Clause #153 (by superposition #[152, 35]): ∀ (a a_1 a_2 : Iota), % 12.89/13.15 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.89/13.15 (Or (Eq (subpopulations first_movers efficient_producers a_1 (skS.0 1 a a_2)) True) % 12.89/13.15 (Or (Eq True False) % 12.89/13.15 (Or (Eq (greater (cardinality_at_time first_movers (skS.0 1 a a_2)) zero) False) % 12.89/13.15 (Or (Eq (environment a_1) False) (Eq (in_environment a_1 (skS.0 1 a a_2)) False))))) % 12.89/13.15 Clause #154 (by superposition #[152, 59]): ∀ (a a_1 a_2 a_3 : Iota), % 12.96/13.20 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.20 (Or (Eq (selection_favors efficient_producers a_1 (skS.0 1 a a_2)) True) % 12.96/13.20 (Or (Eq True False) % 12.96/13.20 (Or (Ne (cardinality_at_time a_1 (skS.0 1 a a_2)) zero) % 12.96/13.20 (Or (Eq (subpopulation a_1 a_3 (skS.0 1 a a_2)) False) % 12.96/13.20 (Or (Eq (environment a_3) False) (Eq (subpopulation efficient_producers a_3 (skS.0 1 a a_2)) False)))))) % 12.96/13.20 Clause #157 (by clausification #[153]): ∀ (a a_1 a_2 : Iota), % 12.96/13.20 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.20 (Or (Eq (subpopulations first_movers efficient_producers a_1 (skS.0 1 a a_2)) True) % 12.96/13.20 (Or (Eq (greater (cardinality_at_time first_movers (skS.0 1 a a_2)) zero) False) % 12.96/13.20 (Or (Eq (environment a_1) False) (Eq (in_environment a_1 (skS.0 1 a a_2)) False)))) % 12.96/13.20 Clause #158 (by superposition #[157, 123]): ∀ (a a_1 a_2 : Iota), % 12.96/13.20 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.20 (Or (Eq (subpopulations first_movers efficient_producers a_1 (skS.0 1 a a_2)) True) % 12.96/13.20 (Or (Eq (environment a_1) False) % 12.96/13.20 (Or (Eq (in_environment a_1 (skS.0 1 a a_2)) False) % 12.96/13.20 (Or (Eq False True) (Eq (cardinality_at_time first_movers (skS.0 1 a a_2)) zero))))) % 12.96/13.20 Clause #163 (by clausification #[158]): ∀ (a a_1 a_2 : Iota), % 12.96/13.20 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.20 (Or (Eq (subpopulations first_movers efficient_producers a_1 (skS.0 1 a a_2)) True) % 12.96/13.20 (Or (Eq (environment a_1) False) % 12.96/13.20 (Or (Eq (in_environment a_1 (skS.0 1 a a_2)) False) % 12.96/13.20 (Eq (cardinality_at_time first_movers (skS.0 1 a a_2)) zero)))) % 12.96/13.20 Clause #164 (by superposition #[163, 99]): ∀ (a a_1 a_2 : Iota), % 12.96/13.20 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.20 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) (skS.0 1 a a_2)) True) % 12.96/13.20 (Or (Eq (in_environment (skS.0 0 a_1) (skS.0 1 a a_2)) False) % 12.96/13.20 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_2)) zero) (Eq False True)))) % 12.96/13.20 Clause #165 (by clausification #[164]): ∀ (a a_1 a_2 : Iota), % 12.96/13.20 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.20 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) (skS.0 1 a a_2)) True) % 12.96/13.20 (Or (Eq (in_environment (skS.0 0 a_1) (skS.0 1 a a_2)) False) % 12.96/13.20 (Eq (cardinality_at_time first_movers (skS.0 1 a a_2)) zero))) % 12.96/13.20 Clause #166 (by superposition #[165, 98]): ∀ (a a_1 : Iota), % 12.96/13.20 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.20 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) % 12.96/13.20 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) (Eq False True))) % 12.96/13.20 Clause #167 (by clausification #[154]): ∀ (a a_1 a_2 a_3 : Iota), % 12.96/13.20 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.20 (Or (Eq (selection_favors efficient_producers a_1 (skS.0 1 a a_2)) True) % 12.96/13.20 (Or (Ne (cardinality_at_time a_1 (skS.0 1 a a_2)) zero) % 12.96/13.20 (Or (Eq (subpopulation a_1 a_3 (skS.0 1 a a_2)) False) % 12.96/13.20 (Or (Eq (environment a_3) False) (Eq (subpopulation efficient_producers a_3 (skS.0 1 a a_2)) False))))) % 12.96/13.20 Clause #168 (by clausification #[166]): ∀ (a a_1 : Iota), % 12.96/13.20 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.20 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) % 12.96/13.20 (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero)) % 12.96/13.20 Clause #169 (by superposition #[168, 129]): ∀ (a a_1 : Iota), % 12.96/13.20 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.20 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.20 (Or % 12.96/13.20 (Eq (greater (growth_rate efficient_producers (skS.0 1 a a_1)) (growth_rate first_movers (skS.0 1 a a_1))) True) % 12.96/13.20 (Or (Eq True False) (Eq (greater (skS.0 1 a a_1) (critical_point (skS.0 0 a))) False)))) % 12.96/13.20 Clause #170 (by clausification #[169]): ∀ (a a_1 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Or % 12.96/13.24 (Eq (greater (growth_rate efficient_producers (skS.0 1 a a_1)) (growth_rate first_movers (skS.0 1 a a_1))) True) % 12.96/13.24 (Eq (greater (skS.0 1 a a_1) (critical_point (skS.0 0 a))) False))) % 12.96/13.24 Clause #171 (by forward demodulation #[170, 23]): ∀ (a a_1 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Or % 12.96/13.24 (Eq (greater (growth_rate efficient_producers (skS.0 1 a a_1)) (growth_rate first_movers (skS.0 1 a a_1))) True) % 12.96/13.24 (Eq True False))) % 12.96/13.24 Clause #172 (by clausification #[171]): ∀ (a a_1 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Eq (greater (growth_rate efficient_producers (skS.0 1 a a_1)) (growth_rate first_movers (skS.0 1 a a_1))) True)) % 12.96/13.24 Clause #173 (by superposition #[172, 44]): ∀ (a a_1 a_2 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 12.96/13.24 (Or (Eq True False) % 12.96/13.24 (Or (Eq (environment a_2) False) % 12.96/13.24 (Eq (subpopulations first_movers efficient_producers a_2 (skS.0 1 a a_1)) False))))) % 12.96/13.24 Clause #179 (by clausification #[173]): ∀ (a a_1 a_2 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 12.96/13.24 (Or (Eq (environment a_2) False) % 12.96/13.24 (Eq (subpopulations first_movers efficient_producers a_2 (skS.0 1 a a_1)) False)))) % 12.96/13.24 Clause #180 (by forward demodulation #[179, 22]): ∀ (a a_1 a_2 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Or (Eq False True) % 12.96/13.24 (Or (Eq (environment a_2) False) % 12.96/13.24 (Eq (subpopulations first_movers efficient_producers a_2 (skS.0 1 a a_1)) False)))) % 12.96/13.24 Clause #181 (by clausification #[180]): ∀ (a a_1 a_2 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Or (Eq (environment a_2) False) % 12.96/13.24 (Eq (subpopulations first_movers efficient_producers a_2 (skS.0 1 a a_1)) False))) % 12.96/13.24 Clause #182 (by superposition #[181, 99]): ∀ (a a_1 a_2 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_2) (skS.0 1 a a_1)) False) (Eq False True))) % 12.96/13.24 Clause #184 (by clausification #[182]): ∀ (a a_1 a_2 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_2) (skS.0 1 a a_1)) False)) % 12.96/13.24 Clause #185 (by superposition #[184, 168]): ∀ (a a_1 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq False True) (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero)))) % 12.96/13.24 Clause #186 (by clausification #[185]): ∀ (a a_1 : Iota), % 12.96/13.24 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.24 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.24 (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero))) % 12.96/13.30 Clause #187 (by eliminate duplicate literals #[186]): ∀ (a a_1 : Iota), % 12.96/13.30 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 12.96/13.30 Clause #190 (by superposition #[187, 167]): ∀ (a a_1 a_2 : Iota), % 12.96/13.30 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 12.96/13.30 (Or (Ne zero zero) % 12.96/13.30 (Or (Eq (subpopulation first_movers a_2 (skS.0 1 a a_1)) False) % 12.96/13.30 (Or (Eq (environment a_2) False) (Eq (subpopulation efficient_producers a_2 (skS.0 1 a a_1)) False)))))) % 12.96/13.30 Clause #194 (by eliminate duplicate literals #[190]): ∀ (a a_1 a_2 : Iota), % 12.96/13.30 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 12.96/13.30 (Or (Ne zero zero) % 12.96/13.30 (Or (Eq (subpopulation first_movers a_2 (skS.0 1 a a_1)) False) % 12.96/13.30 (Or (Eq (environment a_2) False) (Eq (subpopulation efficient_producers a_2 (skS.0 1 a a_1)) False))))) % 12.96/13.30 Clause #195 (by eliminate resolved literals #[194]): ∀ (a a_1 a_2 : Iota), % 12.96/13.30 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 12.96/13.30 (Or (Eq (subpopulation first_movers a_2 (skS.0 1 a a_1)) False) % 12.96/13.30 (Or (Eq (environment a_2) False) (Eq (subpopulation efficient_producers a_2 (skS.0 1 a a_1)) False)))) % 12.96/13.30 Clause #196 (by superposition #[195, 121]): ∀ (a a_1 : Iota), % 12.96/13.30 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 12.96/13.30 (Or (Eq (environment (skS.0 0 a)) False) % 12.96/13.30 (Or (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False) (Eq False True)))) % 12.96/13.30 Clause #197 (by clausification #[196]): ∀ (a a_1 : Iota), % 12.96/13.30 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 12.96/13.30 (Or (Eq (environment (skS.0 0 a)) False) % 12.96/13.30 (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False))) % 12.96/13.30 Clause #198 (by forward demodulation #[197, 22]): ∀ (a a_1 : Iota), % 12.96/13.30 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Or (Eq False True) % 12.96/13.30 (Or (Eq (environment (skS.0 0 a)) False) % 12.96/13.30 (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False))) % 12.96/13.30 Clause #199 (by clausification #[198]): ∀ (a a_1 : Iota), % 12.96/13.30 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Or (Eq (environment (skS.0 0 a)) False) (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False)) % 12.96/13.30 Clause #200 (by forward demodulation #[199, 99]): ∀ (a a_1 : Iota), % 12.96/13.30 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Or (Eq True False) (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False)) % 12.96/13.30 Clause #201 (by clausification #[200]): ∀ (a a_1 : Iota), % 12.96/13.30 Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) % 12.96/13.30 (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False) % 12.96/13.30 Clause #202 (by superposition #[201, 117]): ∀ (a : Iota), Or (Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a))) (Eq False True) % 12.96/13.30 Clause #203 (by clausification #[202]): ∀ (a : Iota), Eq (critical_point (skS.0 0 a)) (appear efficient_producers (skS.0 0 a)) % 12.96/13.30 Clause #221 (by superposition #[203, 49]): ∀ (a a_1 : Iota), % 12.96/13.30 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 12.96/13.30 (Or (Eq (greater_or_equal a (critical_point (skS.0 0 a_1))) False) % 12.96/13.30 (Or (Eq (environment (skS.0 0 a_1)) False) (Eq (in_environment (skS.0 0 a_1) a) False))) % 12.96/13.30 Clause #223 (by forward demodulation #[221, 99]): ∀ (a a_1 : Iota), % 12.96/13.30 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 13.06/13.35 (Or (Eq (greater_or_equal a (critical_point (skS.0 0 a_1))) False) % 13.06/13.35 (Or (Eq True False) (Eq (in_environment (skS.0 0 a_1) a) False))) % 13.06/13.35 Clause #224 (by clausification #[223]): ∀ (a a_1 : Iota), % 13.06/13.35 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 13.06/13.35 (Or (Eq (greater_or_equal a (critical_point (skS.0 0 a_1))) False) (Eq (in_environment (skS.0 0 a_1) a) False)) % 13.06/13.35 Clause #225 (by superposition #[224, 80]): ∀ (a a_1 : Iota), % 13.06/13.35 Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 1 a a_1)) zero) True) % 13.06/13.35 (Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False) (Eq False True)) % 13.06/13.35 Clause #227 (by clausification #[225]): ∀ (a a_1 : Iota), % 13.06/13.35 Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 1 a a_1)) zero) True) % 13.06/13.35 (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False) % 13.06/13.35 Clause #228 (by superposition #[227, 98]): ∀ (a a_1 : Iota), Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 1 a a_1)) zero) True) (Eq False True) % 13.06/13.35 Clause #229 (by clausification #[228]): ∀ (a a_1 : Iota), Eq (greater (cardinality_at_time efficient_producers (skS.0 1 a a_1)) zero) True % 13.06/13.35 Clause #231 (by superposition #[229, 35]): ∀ (a a_1 a_2 : Iota), % 13.06/13.35 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 1 a_1 a_2)) True) % 13.06/13.35 (Or (Eq True False) % 13.06/13.35 (Or (Eq (greater (cardinality_at_time first_movers (skS.0 1 a_1 a_2)) zero) False) % 13.06/13.35 (Or (Eq (environment a) False) (Eq (in_environment a (skS.0 1 a_1 a_2)) False)))) % 13.06/13.35 Clause #232 (by superposition #[229, 59]): ∀ (a a_1 a_2 a_3 : Iota), % 13.06/13.35 Or (Eq (selection_favors efficient_producers a (skS.0 1 a_1 a_2)) True) % 13.06/13.35 (Or (Eq True False) % 13.06/13.35 (Or (Ne (cardinality_at_time a (skS.0 1 a_1 a_2)) zero) % 13.06/13.35 (Or (Eq (subpopulation a a_3 (skS.0 1 a_1 a_2)) False) % 13.06/13.35 (Or (Eq (environment a_3) False) (Eq (subpopulation efficient_producers a_3 (skS.0 1 a_1 a_2)) False))))) % 13.06/13.35 Clause #239 (by clausification #[231]): ∀ (a a_1 a_2 : Iota), % 13.06/13.35 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 1 a_1 a_2)) True) % 13.06/13.35 (Or (Eq (greater (cardinality_at_time first_movers (skS.0 1 a_1 a_2)) zero) False) % 13.06/13.35 (Or (Eq (environment a) False) (Eq (in_environment a (skS.0 1 a_1 a_2)) False))) % 13.06/13.35 Clause #240 (by superposition #[239, 123]): ∀ (a a_1 a_2 : Iota), % 13.06/13.35 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 1 a_1 a_2)) True) % 13.06/13.35 (Or (Eq (environment a) False) % 13.06/13.35 (Or (Eq (in_environment a (skS.0 1 a_1 a_2)) False) % 13.06/13.35 (Or (Eq False True) (Eq (cardinality_at_time first_movers (skS.0 1 a_1 a_2)) zero)))) % 13.06/13.35 Clause #241 (by clausification #[240]): ∀ (a a_1 a_2 : Iota), % 13.06/13.35 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 1 a_1 a_2)) True) % 13.06/13.35 (Or (Eq (environment a) False) % 13.06/13.35 (Or (Eq (in_environment a (skS.0 1 a_1 a_2)) False) % 13.06/13.35 (Eq (cardinality_at_time first_movers (skS.0 1 a_1 a_2)) zero))) % 13.06/13.35 Clause #242 (by superposition #[241, 99]): ∀ (a a_1 a_2 : Iota), % 13.06/13.35 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a_1 a_2)) True) % 13.06/13.35 (Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a_1 a_2)) False) % 13.06/13.35 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a_1 a_2)) zero) (Eq False True))) % 13.06/13.35 Clause #243 (by clausification #[242]): ∀ (a a_1 a_2 : Iota), % 13.06/13.35 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a_1 a_2)) True) % 13.06/13.35 (Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a_1 a_2)) False) % 13.06/13.35 (Eq (cardinality_at_time first_movers (skS.0 1 a_1 a_2)) zero)) % 13.06/13.35 Clause #244 (by superposition #[243, 98]): ∀ (a a_1 : Iota), % 13.06/13.35 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) % 13.06/13.35 (Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) (Eq False True)) % 13.06/13.35 Clause #245 (by clausification #[244]): ∀ (a a_1 : Iota), % 13.06/13.35 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True) % 13.06/13.35 (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.35 Clause #246 (by superposition #[245, 129]): ∀ (a a_1 : Iota), % 13.06/13.35 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Or (Eq (greater (growth_rate efficient_producers (skS.0 1 a a_1)) (growth_rate first_movers (skS.0 1 a a_1))) True) % 13.06/13.39 (Or (Eq True False) (Eq (greater (skS.0 1 a a_1) (critical_point (skS.0 0 a))) False))) % 13.06/13.39 Clause #247 (by clausification #[246]): ∀ (a a_1 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Or (Eq (greater (growth_rate efficient_producers (skS.0 1 a a_1)) (growth_rate first_movers (skS.0 1 a a_1))) True) % 13.06/13.39 (Eq (greater (skS.0 1 a a_1) (critical_point (skS.0 0 a))) False)) % 13.06/13.39 Clause #248 (by forward demodulation #[247, 23]): ∀ (a a_1 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Or (Eq (greater (growth_rate efficient_producers (skS.0 1 a a_1)) (growth_rate first_movers (skS.0 1 a a_1))) True) % 13.06/13.39 (Eq True False)) % 13.06/13.39 Clause #249 (by clausification #[248]): ∀ (a a_1 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Eq (greater (growth_rate efficient_producers (skS.0 1 a a_1)) (growth_rate first_movers (skS.0 1 a a_1))) True) % 13.06/13.39 Clause #250 (by superposition #[249, 44]): ∀ (a a_1 a_2 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 13.06/13.39 (Or (Eq True False) % 13.06/13.39 (Or (Eq (environment a_2) False) % 13.06/13.39 (Eq (subpopulations first_movers efficient_producers a_2 (skS.0 1 a a_1)) False)))) % 13.06/13.39 Clause #256 (by clausification #[250]): ∀ (a a_1 a_2 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 13.06/13.39 (Or (Eq (environment a_2) False) % 13.06/13.39 (Eq (subpopulations first_movers efficient_producers a_2 (skS.0 1 a a_1)) False))) % 13.06/13.39 Clause #257 (by forward demodulation #[256, 22]): ∀ (a a_1 a_2 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Or (Eq False True) % 13.06/13.39 (Or (Eq (environment a_2) False) % 13.06/13.39 (Eq (subpopulations first_movers efficient_producers a_2 (skS.0 1 a a_1)) False))) % 13.06/13.39 Clause #258 (by clausification #[257]): ∀ (a a_1 a_2 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Or (Eq (environment a_2) False) (Eq (subpopulations first_movers efficient_producers a_2 (skS.0 1 a a_1)) False)) % 13.06/13.39 Clause #259 (by superposition #[258, 99]): ∀ (a a_1 a_2 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_2) (skS.0 1 a a_1)) False) (Eq False True)) % 13.06/13.39 Clause #260 (by clausification #[259]): ∀ (a a_1 a_2 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_2) (skS.0 1 a a_1)) False) % 13.06/13.39 Clause #261 (by superposition #[260, 245]): ∀ (a a_1 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Or (Eq False True) (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero)) % 13.06/13.39 Clause #262 (by clausification #[261]): ∀ (a a_1 : Iota), % 13.06/13.39 Or (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 (Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero) % 13.06/13.39 Clause #263 (by eliminate duplicate literals #[262]): ∀ (a a_1 : Iota), Eq (cardinality_at_time first_movers (skS.0 1 a a_1)) zero % 13.06/13.39 Clause #278 (by clausification #[232]): ∀ (a a_1 a_2 a_3 : Iota), % 13.06/13.39 Or (Eq (selection_favors efficient_producers a (skS.0 1 a_1 a_2)) True) % 13.06/13.39 (Or (Ne (cardinality_at_time a (skS.0 1 a_1 a_2)) zero) % 13.06/13.39 (Or (Eq (subpopulation a a_3 (skS.0 1 a_1 a_2)) False) % 13.06/13.39 (Or (Eq (environment a_3) False) (Eq (subpopulation efficient_producers a_3 (skS.0 1 a_1 a_2)) False)))) % 13.06/13.39 Clause #279 (by superposition #[278, 263]): ∀ (a a_1 a_2 : Iota), % 13.06/13.39 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 13.06/13.39 (Or (Ne zero zero) % 13.06/13.39 (Or (Eq (subpopulation first_movers a_2 (skS.0 1 a a_1)) False) % 13.06/13.39 (Or (Eq (environment a_2) False) (Eq (subpopulation efficient_producers a_2 (skS.0 1 a a_1)) False)))) % 13.16/13.42 Clause #280 (by eliminate resolved literals #[279]): ∀ (a a_1 a_2 : Iota), % 13.16/13.42 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 13.16/13.42 (Or (Eq (subpopulation first_movers a_2 (skS.0 1 a a_1)) False) % 13.16/13.42 (Or (Eq (environment a_2) False) (Eq (subpopulation efficient_producers a_2 (skS.0 1 a a_1)) False))) % 13.16/13.42 Clause #281 (by superposition #[280, 121]): ∀ (a a_1 : Iota), % 13.16/13.42 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 13.16/13.42 (Or (Eq (environment (skS.0 0 a)) False) % 13.16/13.42 (Or (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False) (Eq False True))) % 13.16/13.42 Clause #282 (by clausification #[281]): ∀ (a a_1 : Iota), % 13.16/13.42 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 a a_1)) True) % 13.16/13.42 (Or (Eq (environment (skS.0 0 a)) False) (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False)) % 13.16/13.42 Clause #283 (by forward demodulation #[282, 22]): ∀ (a a_1 : Iota), % 13.16/13.42 Or (Eq False True) % 13.16/13.42 (Or (Eq (environment (skS.0 0 a)) False) (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False)) % 13.16/13.42 Clause #284 (by clausification #[283]): ∀ (a a_1 : Iota), % 13.16/13.42 Or (Eq (environment (skS.0 0 a)) False) (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False) % 13.16/13.42 Clause #285 (by forward demodulation #[284, 99]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False) % 13.16/13.42 Clause #286 (by clausification #[285]): ∀ (a a_1 : Iota), Eq (subpopulation efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) False % 13.16/13.42 Clause #287 (by superposition #[286, 117]): Eq False True % 13.16/13.42 Clause #288 (by clausification #[287]): False % 13.16/13.42 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------