%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:06:16 AM UTC 2026 % Result : Theorem 24.37s 24.62s % Output : Proof 24.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.05 % Command : duper %s % 0.12/0.36 % Computer : n015.cluster.edu % 0.12/0.36 % Model : x86_64 x86_64 % 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.36 % Memory : 8046.5625MB % 0.12/0.36 % OS : Linux 6.8.0-71-generic % 0.12/0.36 % CPULimit : 300 % 0.12/0.36 % WCLimit : 300 % 0.12/0.36 % DateTime : Mon Sep 7 12:16:30 UTC 2026 % 0.12/0.36 % CPUTime : % 24.37/24.62 SZS status Theorem for theBenchmark.p % 24.37/24.62 SZS output start Proof for theBenchmark.p % 24.37/24.62 Clause #0 (by assumption #[]): Eq % 24.37/24.62 (∀ (E To : Iota), % 24.37/24.62 And (And (And (environment E) (stable E)) (in_environment E To)) % 24.37/24.62 (∀ (T : Iota), % 24.37/24.62 And (greater (cardinality_at_time first_movers T) zero) (greater_or_equal T To) → % 24.37/24.62 greater zero (growth_rate first_movers T)) → % 24.37/24.62 contracts_from To first_movers) % 24.37/24.62 True % 24.37/24.62 Clause #1 (by assumption #[]): Eq % 24.37/24.62 (∀ (E T : Iota), % 24.37/24.62 And (And (And (environment E) (in_environment E T)) (greater (cardinality_at_time first_movers T) zero)) % 24.37/24.62 (greater (cardinality_at_time efficient_producers T) zero) → % 24.37/24.62 subpopulations first_movers efficient_producers E T) % 24.37/24.62 True % 24.37/24.62 Clause #2 (by assumption #[]): Eq % 24.37/24.62 (∀ (E T1 T2 : Iota), % 24.37/24.62 And (And (And (environment E) (stable E)) (in_environment E T1)) (greater T2 T1) → in_environment E T2) % 24.37/24.62 True % 24.37/24.62 Clause #3 (by assumption #[]): Eq (∀ (E : Iota), And (environment E) (stable E) → in_environment E (appear efficient_producers E)) True % 24.37/24.62 Clause #4 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (greater X Y) (greater Y Z) → greater X Z) True % 24.37/24.62 Clause #5 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (greater_or_equal X Y) (Or (greater X Y) (Eq X Y))) True % 24.37/24.62 Clause #6 (by assumption #[]): Eq % 24.37/24.62 (∀ (E T : Iota), % 24.37/24.62 And (And (environment E) (in_environment E T)) (greater_or_equal T (appear efficient_producers E)) → % 24.37/24.62 greater (cardinality_at_time efficient_producers T) zero) % 24.37/24.62 True % 24.37/24.62 Clause #7 (by assumption #[]): Eq % 24.37/24.62 (∀ (E : Iota), % 24.37/24.62 And (environment E) (stable E) → % 24.37/24.62 Exists fun To => % 24.37/24.62 And (greater To (appear efficient_producers E)) % 24.37/24.62 (∀ (T : Iota), % 24.37/24.62 And (subpopulations first_movers efficient_producers E T) (greater_or_equal T To) → % 24.37/24.62 greater zero (growth_rate first_movers T))) % 24.37/24.62 True % 24.37/24.62 Clause #8 (by assumption #[]): Eq % 24.37/24.62 (Not % 24.37/24.62 (∀ (E : Iota), % 24.37/24.62 And (environment E) (stable E) → % 24.37/24.62 Exists fun To => And (greater To (appear efficient_producers E)) (contracts_from To first_movers))) % 24.37/24.62 True % 24.37/24.62 Clause #9 (by clausification #[0]): ∀ (a : Iota), % 24.37/24.62 Eq % 24.37/24.62 (∀ (To : Iota), % 24.37/24.62 And (And (And (environment a) (stable a)) (in_environment a To)) % 24.37/24.62 (∀ (T : Iota), % 24.37/24.62 And (greater (cardinality_at_time first_movers T) zero) (greater_or_equal T To) → % 24.37/24.62 greater zero (growth_rate first_movers T)) → % 24.37/24.62 contracts_from To first_movers) % 24.37/24.62 True % 24.37/24.62 Clause #10 (by clausification #[9]): ∀ (a a_1 : Iota), % 24.37/24.62 Eq % 24.37/24.62 (And (And (And (environment a) (stable a)) (in_environment a a_1)) % 24.37/24.62 (∀ (T : Iota), % 24.37/24.62 And (greater (cardinality_at_time first_movers T) zero) (greater_or_equal T a_1) → % 24.37/24.62 greater zero (growth_rate first_movers T)) → % 24.37/24.62 contracts_from a_1 first_movers) % 24.37/24.62 True % 24.37/24.62 Clause #11 (by clausification #[10]): ∀ (a a_1 : Iota), % 24.37/24.62 Or % 24.37/24.62 (Eq % 24.37/24.62 (And (And (And (environment a) (stable a)) (in_environment a a_1)) % 24.37/24.62 (∀ (T : Iota), % 24.37/24.62 And (greater (cardinality_at_time first_movers T) zero) (greater_or_equal T a_1) → % 24.37/24.62 greater zero (growth_rate first_movers T))) % 24.37/24.62 False) % 24.37/24.62 (Eq (contracts_from a_1 first_movers) True) % 24.37/24.62 Clause #12 (by clausification #[11]): ∀ (a a_1 : Iota), % 24.37/24.62 Or (Eq (contracts_from a first_movers) True) % 24.37/24.62 (Or (Eq (And (And (environment a_1) (stable a_1)) (in_environment a_1 a)) False) % 24.37/24.62 (Eq % 24.37/24.62 (∀ (T : Iota), % 24.37/24.62 And (greater (cardinality_at_time first_movers T) zero) (greater_or_equal T a) → % 24.37/24.62 greater zero (growth_rate first_movers T)) % 24.37/24.62 False)) % 24.37/24.62 Clause #13 (by clausification #[12]): ∀ (a a_1 : Iota), % 24.37/24.62 Or (Eq (contracts_from a first_movers) True) % 24.37/24.62 (Or % 24.37/24.62 (Eq % 24.37/24.62 (∀ (T : Iota), % 24.37/24.62 And (greater (cardinality_at_time first_movers T) zero) (greater_or_equal T a) → % 24.37/24.62 greater zero (growth_rate first_movers T)) % 24.37/24.62 False) % 24.37/24.62 (Or (Eq (And (environment a_1) (stable a_1)) False) (Eq (in_environment a_1 a) False))) % 24.37/24.62 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 : Iota), % 24.37/24.62 Or (Eq (contracts_from a first_movers) True) % 24.37/24.67 (Or (Eq (And (environment a_1) (stable a_1)) False) % 24.37/24.67 (Or (Eq (in_environment a_1 a) False) % 24.37/24.67 (Eq % 24.37/24.67 (Not % 24.37/24.67 (And (greater (cardinality_at_time first_movers (skS.0 0 a a_2)) zero) % 24.37/24.67 (greater_or_equal (skS.0 0 a a_2) a) → % 24.37/24.67 greater zero (growth_rate first_movers (skS.0 0 a a_2)))) % 24.37/24.67 True))) % 24.37/24.67 Clause #15 (by clausification #[14]): ∀ (a a_1 a_2 : Iota), % 24.37/24.67 Or (Eq (contracts_from a first_movers) True) % 24.37/24.67 (Or (Eq (in_environment a_1 a) False) % 24.37/24.67 (Or % 24.37/24.67 (Eq % 24.37/24.67 (Not % 24.37/24.67 (And (greater (cardinality_at_time first_movers (skS.0 0 a a_2)) zero) % 24.37/24.67 (greater_or_equal (skS.0 0 a a_2) a) → % 24.37/24.67 greater zero (growth_rate first_movers (skS.0 0 a a_2)))) % 24.37/24.67 True) % 24.37/24.67 (Or (Eq (environment a_1) False) (Eq (stable a_1) False)))) % 24.37/24.67 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 : Iota), % 24.37/24.67 Or (Eq (contracts_from a first_movers) True) % 24.37/24.67 (Or (Eq (in_environment a_1 a) False) % 24.37/24.67 (Or (Eq (environment a_1) False) % 24.37/24.67 (Or (Eq (stable a_1) False) % 24.37/24.67 (Eq % 24.37/24.67 (And (greater (cardinality_at_time first_movers (skS.0 0 a a_2)) zero) % 24.37/24.67 (greater_or_equal (skS.0 0 a a_2) a) → % 24.37/24.67 greater zero (growth_rate first_movers (skS.0 0 a a_2))) % 24.37/24.67 False)))) % 24.37/24.67 Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 : Iota), % 24.37/24.67 Or (Eq (contracts_from a first_movers) True) % 24.37/24.67 (Or (Eq (in_environment a_1 a) False) % 24.37/24.67 (Or (Eq (environment a_1) False) % 24.37/24.67 (Or (Eq (stable a_1) False) % 24.37/24.67 (Eq % 24.37/24.67 (And (greater (cardinality_at_time first_movers (skS.0 0 a a_2)) zero) (greater_or_equal (skS.0 0 a a_2) a)) % 24.37/24.67 True)))) % 24.37/24.67 Clause #18 (by clausification #[16]): ∀ (a a_1 a_2 : Iota), % 24.37/24.67 Or (Eq (contracts_from a first_movers) True) % 24.37/24.67 (Or (Eq (in_environment a_1 a) False) % 24.37/24.67 (Or (Eq (environment a_1) False) % 24.37/24.67 (Or (Eq (stable a_1) False) (Eq (greater zero (growth_rate first_movers (skS.0 0 a a_2))) False)))) % 24.37/24.67 Clause #19 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), % 24.37/24.67 Or (Eq (contracts_from a first_movers) True) % 24.37/24.67 (Or (Eq (in_environment a_1 a) False) % 24.37/24.67 (Or (Eq (environment a_1) False) (Or (Eq (stable a_1) False) (Eq (greater_or_equal (skS.0 0 a a_2) a) True)))) % 24.37/24.67 Clause #20 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), % 24.37/24.67 Or (Eq (contracts_from a first_movers) True) % 24.37/24.67 (Or (Eq (in_environment a_1 a) False) % 24.37/24.67 (Or (Eq (environment a_1) False) % 24.37/24.67 (Or (Eq (stable a_1) False) (Eq (greater (cardinality_at_time first_movers (skS.0 0 a a_2)) zero) True)))) % 24.37/24.67 Clause #21 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (greater a Y) (greater Y Z) → greater a Z) True % 24.37/24.67 Clause #22 (by clausification #[21]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (greater a a_1) (greater a_1 Z) → greater a Z) True % 24.37/24.67 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 : Iota), Eq (And (greater a a_1) (greater a_1 a_2) → greater a a_2) True % 24.37/24.67 Clause #24 (by clausification #[23]): ∀ (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) % 24.37/24.67 Clause #25 (by clausification #[24]): ∀ (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)) % 24.37/24.67 Clause #26 (by clausification #[3]): ∀ (a : Iota), Eq (And (environment a) (stable a) → in_environment a (appear efficient_producers a)) True % 24.37/24.67 Clause #27 (by clausification #[26]): ∀ (a : Iota), Or (Eq (And (environment a) (stable a)) False) (Eq (in_environment a (appear efficient_producers a)) True) % 24.37/24.67 Clause #28 (by clausification #[27]): ∀ (a : Iota), % 24.37/24.67 Or (Eq (in_environment a (appear efficient_producers a)) True) (Or (Eq (environment a) False) (Eq (stable a) False)) % 24.37/24.67 Clause #29 (by clausification #[2]): ∀ (a : Iota), % 24.37/24.67 Eq % 24.37/24.67 (∀ (T1 T2 : Iota), % 24.37/24.67 And (And (And (environment a) (stable a)) (in_environment a T1)) (greater T2 T1) → in_environment a T2) % 24.37/24.67 True % 24.37/24.67 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), % 24.37/24.67 Eq % 24.37/24.67 (∀ (T2 : Iota), % 24.37/24.67 And (And (And (environment a) (stable a)) (in_environment a a_1)) (greater T2 a_1) → in_environment a T2) % 24.47/24.71 True % 24.47/24.71 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 : Iota), % 24.47/24.71 Eq (And (And (And (environment a) (stable a)) (in_environment a a_1)) (greater a_2 a_1) → in_environment a a_2) True % 24.47/24.71 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), % 24.47/24.71 Or (Eq (And (And (And (environment a) (stable a)) (in_environment a a_1)) (greater a_2 a_1)) False) % 24.47/24.71 (Eq (in_environment a a_2) True) % 24.47/24.71 Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 : Iota), % 24.47/24.71 Or (Eq (in_environment a a_1) True) % 24.47/24.71 (Or (Eq (And (And (environment a) (stable a)) (in_environment a a_2)) False) (Eq (greater a_1 a_2) False)) % 24.47/24.71 Clause #34 (by clausification #[33]): ∀ (a a_1 a_2 : Iota), % 24.47/24.71 Or (Eq (in_environment a a_1) True) % 24.47/24.71 (Or (Eq (greater a_1 a_2) False) (Or (Eq (And (environment a) (stable a)) False) (Eq (in_environment a a_2) False))) % 24.47/24.71 Clause #35 (by clausification #[34]): ∀ (a a_1 a_2 : Iota), % 24.47/24.71 Or (Eq (in_environment a a_1) True) % 24.47/24.71 (Or (Eq (greater a_1 a_2) False) % 24.47/24.71 (Or (Eq (in_environment a a_2) False) (Or (Eq (environment a) False) (Eq (stable a) False)))) % 24.47/24.71 Clause #36 (by clausification #[6]): ∀ (a : Iota), % 24.47/24.71 Eq % 24.47/24.71 (∀ (T : Iota), % 24.47/24.71 And (And (environment a) (in_environment a T)) (greater_or_equal T (appear efficient_producers a)) → % 24.47/24.71 greater (cardinality_at_time efficient_producers T) zero) % 24.47/24.71 True % 24.47/24.71 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), % 24.47/24.71 Eq % 24.47/24.71 (And (And (environment a) (in_environment a a_1)) (greater_or_equal a_1 (appear efficient_producers a)) → % 24.47/24.71 greater (cardinality_at_time efficient_producers a_1) zero) % 24.47/24.71 True % 24.47/24.71 Clause #38 (by clausification #[37]): ∀ (a a_1 : Iota), % 24.47/24.71 Or (Eq (And (And (environment a) (in_environment a a_1)) (greater_or_equal a_1 (appear efficient_producers a))) False) % 24.47/24.71 (Eq (greater (cardinality_at_time efficient_producers a_1) zero) True) % 24.47/24.71 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), % 24.47/24.71 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 24.47/24.71 (Or (Eq (And (environment a_1) (in_environment a_1 a)) False) % 24.47/24.71 (Eq (greater_or_equal a (appear efficient_producers a_1)) False)) % 24.47/24.71 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), % 24.47/24.71 Or (Eq (greater (cardinality_at_time efficient_producers a) zero) True) % 24.47/24.71 (Or (Eq (greater_or_equal a (appear efficient_producers a_1)) False) % 24.47/24.71 (Or (Eq (environment a_1) False) (Eq (in_environment a_1 a) False))) % 24.47/24.71 Clause #41 (by clausification #[1]): ∀ (a : Iota), % 24.47/24.71 Eq % 24.47/24.71 (∀ (T : Iota), % 24.47/24.71 And (And (And (environment a) (in_environment a T)) (greater (cardinality_at_time first_movers T) zero)) % 24.47/24.71 (greater (cardinality_at_time efficient_producers T) zero) → % 24.47/24.71 subpopulations first_movers efficient_producers a T) % 24.47/24.71 True % 24.47/24.71 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), % 24.47/24.71 Eq % 24.47/24.71 (And (And (And (environment a) (in_environment a a_1)) (greater (cardinality_at_time first_movers a_1) zero)) % 24.47/24.71 (greater (cardinality_at_time efficient_producers a_1) zero) → % 24.47/24.71 subpopulations first_movers efficient_producers a a_1) % 24.47/24.71 True % 24.47/24.71 Clause #43 (by clausification #[42]): ∀ (a a_1 : Iota), % 24.47/24.71 Or % 24.47/24.71 (Eq % 24.47/24.71 (And (And (And (environment a) (in_environment a a_1)) (greater (cardinality_at_time first_movers a_1) zero)) % 24.47/24.71 (greater (cardinality_at_time efficient_producers a_1) zero)) % 24.47/24.71 False) % 24.47/24.71 (Eq (subpopulations first_movers efficient_producers a a_1) True) % 24.47/24.71 Clause #44 (by clausification #[43]): ∀ (a a_1 : Iota), % 24.47/24.71 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 24.47/24.71 (Or % 24.47/24.71 (Eq (And (And (environment a) (in_environment a a_1)) (greater (cardinality_at_time first_movers a_1) zero)) % 24.47/24.71 False) % 24.47/24.71 (Eq (greater (cardinality_at_time efficient_producers a_1) zero) False)) % 24.47/24.71 Clause #45 (by clausification #[44]): ∀ (a a_1 : Iota), % 24.47/24.71 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 24.47/24.71 (Or (Eq (greater (cardinality_at_time efficient_producers a_1) zero) False) % 24.47/24.71 (Or (Eq (And (environment a) (in_environment a a_1)) False) % 24.47/24.71 (Eq (greater (cardinality_at_time first_movers a_1) zero) False))) % 24.47/24.77 Clause #46 (by clausification #[45]): ∀ (a a_1 : Iota), % 24.47/24.77 Or (Eq (subpopulations first_movers efficient_producers a a_1) True) % 24.47/24.77 (Or (Eq (greater (cardinality_at_time efficient_producers a_1) zero) False) % 24.47/24.77 (Or (Eq (greater (cardinality_at_time first_movers a_1) zero) False) % 24.47/24.77 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False)))) % 24.47/24.77 Clause #47 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (greater_or_equal a Y) (Or (greater a Y) (Eq a Y))) True % 24.47/24.77 Clause #48 (by clausification #[47]): ∀ (a a_1 : Iota), Eq (Iff (greater_or_equal a a_1) (Or (greater a a_1) (Eq a a_1))) True % 24.47/24.77 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (Or (greater a a_1) (Eq a a_1)) False) % 24.47/24.77 Clause #50 (by clausification #[48]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Eq (Or (greater a a_1) (Eq a a_1)) True) % 24.47/24.77 Clause #51 (by clausification #[49]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (Eq a a_1) False) % 24.47/24.77 Clause #52 (by clausification #[49]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (greater a a_1) False) % 24.47/24.77 Clause #53 (by clausification #[51]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Ne a a_1) % 24.47/24.77 Clause #54 (by destructive equality resolution #[53]): ∀ (a : Iota), Eq (greater_or_equal a a) True % 24.47/24.77 Clause #56 (by clausification #[50]): ∀ (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)) % 24.47/24.77 Clause #57 (by clausification #[56]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Or (Eq (greater a a_1) True) (Eq a a_1)) % 24.47/24.77 Clause #60 (by clausification #[8]): Eq % 24.47/24.77 (∀ (E : Iota), % 24.47/24.77 And (environment E) (stable E) → % 24.47/24.77 Exists fun To => And (greater To (appear efficient_producers E)) (contracts_from To first_movers)) % 24.47/24.77 False % 24.47/24.77 Clause #61 (by clausification #[60]): ∀ (a : Iota), % 24.47/24.77 Eq % 24.47/24.77 (Not % 24.47/24.77 (And (environment (skS.0 1 a)) (stable (skS.0 1 a)) → % 24.47/24.77 Exists fun To => And (greater To (appear efficient_producers (skS.0 1 a))) (contracts_from To first_movers))) % 24.47/24.77 True % 24.47/24.77 Clause #62 (by clausification #[61]): ∀ (a : Iota), % 24.47/24.77 Eq % 24.47/24.77 (And (environment (skS.0 1 a)) (stable (skS.0 1 a)) → % 24.47/24.77 Exists fun To => And (greater To (appear efficient_producers (skS.0 1 a))) (contracts_from To first_movers)) % 24.47/24.77 False % 24.47/24.77 Clause #63 (by clausification #[62]): ∀ (a : Iota), Eq (And (environment (skS.0 1 a)) (stable (skS.0 1 a))) True % 24.47/24.77 Clause #64 (by clausification #[62]): ∀ (a : Iota), % 24.47/24.77 Eq (Exists fun To => And (greater To (appear efficient_producers (skS.0 1 a))) (contracts_from To first_movers)) False % 24.47/24.77 Clause #65 (by clausification #[63]): ∀ (a : Iota), Eq (stable (skS.0 1 a)) True % 24.47/24.77 Clause #66 (by clausification #[63]): ∀ (a : Iota), Eq (environment (skS.0 1 a)) True % 24.47/24.77 Clause #67 (by clausification #[7]): ∀ (a : Iota), % 24.47/24.77 Eq % 24.47/24.77 (And (environment a) (stable a) → % 24.47/24.77 Exists fun To => % 24.47/24.77 And (greater To (appear efficient_producers a)) % 24.47/24.77 (∀ (T : Iota), % 24.47/24.77 And (subpopulations first_movers efficient_producers a T) (greater_or_equal T To) → % 24.47/24.77 greater zero (growth_rate first_movers T))) % 24.47/24.77 True % 24.47/24.77 Clause #68 (by clausification #[67]): ∀ (a : Iota), % 24.47/24.77 Or (Eq (And (environment a) (stable a)) False) % 24.47/24.77 (Eq % 24.47/24.77 (Exists fun To => % 24.47/24.77 And (greater To (appear efficient_producers a)) % 24.47/24.77 (∀ (T : Iota), % 24.47/24.77 And (subpopulations first_movers efficient_producers a T) (greater_or_equal T To) → % 24.47/24.77 greater zero (growth_rate first_movers T))) % 24.47/24.77 True) % 24.47/24.77 Clause #69 (by clausification #[68]): ∀ (a : Iota), % 24.47/24.77 Or % 24.47/24.77 (Eq % 24.47/24.77 (Exists fun To => % 24.47/24.77 And (greater To (appear efficient_producers a)) % 24.47/24.77 (∀ (T : Iota), % 24.47/24.77 And (subpopulations first_movers efficient_producers a T) (greater_or_equal T To) → % 24.47/24.77 greater zero (growth_rate first_movers T))) % 24.47/24.77 True) % 24.47/24.77 (Or (Eq (environment a) False) (Eq (stable a) False)) % 24.47/24.77 Clause #70 (by clausification #[69]): ∀ (a a_1 : Iota), % 24.47/24.77 Or (Eq (environment a) False) % 24.47/24.77 (Or (Eq (stable a) False) % 24.57/24.82 (Eq % 24.57/24.82 (And (greater (skS.0 2 a a_1) (appear efficient_producers a)) % 24.57/24.82 (∀ (T : Iota), % 24.57/24.82 And (subpopulations first_movers efficient_producers a T) (greater_or_equal T (skS.0 2 a a_1)) → % 24.57/24.82 greater zero (growth_rate first_movers T))) % 24.57/24.82 True)) % 24.57/24.82 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), % 24.57/24.82 Or (Eq (environment a) False) % 24.57/24.82 (Or (Eq (stable a) False) % 24.57/24.82 (Eq % 24.57/24.82 (∀ (T : Iota), % 24.57/24.82 And (subpopulations first_movers efficient_producers a T) (greater_or_equal T (skS.0 2 a a_1)) → % 24.57/24.82 greater zero (growth_rate first_movers T)) % 24.57/24.82 True)) % 24.57/24.82 Clause #72 (by clausification #[70]): ∀ (a a_1 : Iota), % 24.57/24.82 Or (Eq (environment a) False) % 24.57/24.82 (Or (Eq (stable a) False) (Eq (greater (skS.0 2 a a_1) (appear efficient_producers a)) True)) % 24.57/24.82 Clause #73 (by clausification #[71]): ∀ (a a_1 a_2 : Iota), % 24.57/24.82 Or (Eq (environment a) False) % 24.57/24.82 (Or (Eq (stable a) False) % 24.57/24.82 (Eq % 24.57/24.82 (And (subpopulations first_movers efficient_producers a a_1) (greater_or_equal a_1 (skS.0 2 a a_2)) → % 24.57/24.82 greater zero (growth_rate first_movers a_1)) % 24.57/24.82 True)) % 24.57/24.82 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 : Iota), % 24.57/24.82 Or (Eq (environment a) False) % 24.57/24.82 (Or (Eq (stable a) False) % 24.57/24.82 (Or % 24.57/24.82 (Eq (And (subpopulations first_movers efficient_producers a a_1) (greater_or_equal a_1 (skS.0 2 a a_2))) False) % 24.57/24.82 (Eq (greater zero (growth_rate first_movers a_1)) True))) % 24.57/24.82 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 : Iota), % 24.57/24.82 Or (Eq (environment a) False) % 24.57/24.82 (Or (Eq (stable a) False) % 24.57/24.82 (Or (Eq (greater zero (growth_rate first_movers a_1)) True) % 24.57/24.82 (Or (Eq (subpopulations first_movers efficient_producers a a_1) False) % 24.57/24.82 (Eq (greater_or_equal a_1 (skS.0 2 a a_2)) False)))) % 24.57/24.82 Clause #76 (by superposition #[66, 28]): ∀ (a : Iota), % 24.57/24.82 Or (Eq (in_environment (skS.0 1 a) (appear efficient_producers (skS.0 1 a))) True) % 24.57/24.82 (Or (Eq True False) (Eq (stable (skS.0 1 a)) False)) % 24.57/24.82 Clause #77 (by superposition #[66, 75]): ∀ (a a_1 a_2 : Iota), % 24.57/24.82 Or (Eq (stable (skS.0 1 a)) False) % 24.57/24.82 (Or (Eq (greater zero (growth_rate first_movers a_1)) True) % 24.57/24.82 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 1 a) a_1) False) % 24.57/24.82 (Or (Eq (greater_or_equal a_1 (skS.0 2 (skS.0 1 a) a_2)) False) (Eq False True)))) % 24.57/24.82 Clause #78 (by clausification #[64]): ∀ (a a_1 : Iota), Eq (And (greater a (appear efficient_producers (skS.0 1 a_1))) (contracts_from a first_movers)) False % 24.57/24.82 Clause #79 (by clausification #[78]): ∀ (a a_1 : Iota), % 24.57/24.82 Or (Eq (greater a (appear efficient_producers (skS.0 1 a_1))) False) (Eq (contracts_from a first_movers) False) % 24.57/24.82 Clause #82 (by superposition #[72, 66]): ∀ (a a_1 : Iota), % 24.57/24.82 Or (Eq (stable (skS.0 1 a)) False) % 24.57/24.82 (Or (Eq (greater (skS.0 2 (skS.0 1 a) a_1) (appear efficient_producers (skS.0 1 a))) True) (Eq False True)) % 24.57/24.82 Clause #83 (by clausification #[76]): ∀ (a : Iota), % 24.57/24.82 Or (Eq (in_environment (skS.0 1 a) (appear efficient_producers (skS.0 1 a))) True) (Eq (stable (skS.0 1 a)) False) % 24.57/24.82 Clause #84 (by forward demodulation #[83, 65]): ∀ (a : Iota), Or (Eq (in_environment (skS.0 1 a) (appear efficient_producers (skS.0 1 a))) True) (Eq True False) % 24.57/24.82 Clause #85 (by clausification #[84]): ∀ (a : Iota), Eq (in_environment (skS.0 1 a) (appear efficient_producers (skS.0 1 a))) True % 24.57/24.82 Clause #99 (by clausification #[77]): ∀ (a a_1 a_2 : Iota), % 24.57/24.82 Or (Eq (stable (skS.0 1 a)) False) % 24.57/24.82 (Or (Eq (greater zero (growth_rate first_movers a_1)) True) % 24.57/24.82 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 1 a) a_1) False) % 24.57/24.82 (Eq (greater_or_equal a_1 (skS.0 2 (skS.0 1 a) a_2)) False))) % 24.57/24.82 Clause #100 (by forward demodulation #[99, 65]): ∀ (a a_1 a_2 : Iota), % 24.57/24.82 Or (Eq True False) % 24.57/24.82 (Or (Eq (greater zero (growth_rate first_movers a)) True) % 24.57/24.82 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 1 a_1) a) False) % 24.57/24.82 (Eq (greater_or_equal a (skS.0 2 (skS.0 1 a_1) a_2)) False))) % 24.57/24.82 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 : Iota), % 24.57/24.82 Or (Eq (greater zero (growth_rate first_movers a)) True) % 24.57/24.88 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 1 a_1) a) False) % 24.57/24.88 (Eq (greater_or_equal a (skS.0 2 (skS.0 1 a_1) a_2)) False)) % 24.57/24.88 Clause #105 (by clausification #[82]): ∀ (a a_1 : Iota), % 24.57/24.88 Or (Eq (stable (skS.0 1 a)) False) % 24.57/24.88 (Eq (greater (skS.0 2 (skS.0 1 a) a_1) (appear efficient_producers (skS.0 1 a))) True) % 24.57/24.88 Clause #106 (by forward demodulation #[105, 65]): ∀ (a a_1 : Iota), % 24.57/24.88 Or (Eq True False) (Eq (greater (skS.0 2 (skS.0 1 a) a_1) (appear efficient_producers (skS.0 1 a))) True) % 24.57/24.88 Clause #107 (by clausification #[106]): ∀ (a a_1 : Iota), Eq (greater (skS.0 2 (skS.0 1 a) a_1) (appear efficient_producers (skS.0 1 a))) True % 24.57/24.88 Clause #108 (by superposition #[107, 79]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (contracts_from (skS.0 2 (skS.0 1 a) a_1) first_movers) False) % 24.57/24.88 Clause #110 (by superposition #[107, 35]): ∀ (a a_1 a_2 : Iota), % 24.57/24.88 Or (Eq (in_environment a (skS.0 2 (skS.0 1 a_1) a_2)) True) % 24.57/24.88 (Or (Eq True False) % 24.57/24.88 (Or (Eq (in_environment a (appear efficient_producers (skS.0 1 a_1))) False) % 24.57/24.88 (Or (Eq (environment a) False) (Eq (stable a) False)))) % 24.57/24.88 Clause #111 (by superposition #[107, 52]): ∀ (a a_1 : Iota), % 24.57/24.88 Or (Eq (greater_or_equal (skS.0 2 (skS.0 1 a) a_1) (appear efficient_producers (skS.0 1 a))) True) (Eq True False) % 24.57/24.88 Clause #112 (by clausification #[108]): ∀ (a a_1 : Iota), Eq (contracts_from (skS.0 2 (skS.0 1 a) a_1) first_movers) False % 24.57/24.88 Clause #120 (by clausification #[111]): ∀ (a a_1 : Iota), Eq (greater_or_equal (skS.0 2 (skS.0 1 a) a_1) (appear efficient_producers (skS.0 1 a))) True % 24.57/24.88 Clause #121 (by superposition #[120, 40]): ∀ (a a_1 : Iota), % 24.57/24.88 Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 2 (skS.0 1 a) a_1)) zero) True) % 24.57/24.88 (Or (Eq True False) % 24.57/24.88 (Or (Eq (environment (skS.0 1 a)) False) (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) False))) % 24.57/24.88 Clause #124 (by clausification #[110]): ∀ (a a_1 a_2 : Iota), % 24.57/24.88 Or (Eq (in_environment a (skS.0 2 (skS.0 1 a_1) a_2)) True) % 24.57/24.88 (Or (Eq (in_environment a (appear efficient_producers (skS.0 1 a_1))) False) % 24.57/24.88 (Or (Eq (environment a) False) (Eq (stable a) False))) % 24.57/24.88 Clause #125 (by superposition #[124, 85]): ∀ (a a_1 : Iota), % 24.57/24.88 Or (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) True) % 24.57/24.88 (Or (Eq (environment (skS.0 1 a)) False) (Or (Eq (stable (skS.0 1 a)) False) (Eq False True))) % 24.57/24.88 Clause #126 (by clausification #[125]): ∀ (a a_1 : Iota), % 24.57/24.88 Or (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) True) % 24.57/24.88 (Or (Eq (environment (skS.0 1 a)) False) (Eq (stable (skS.0 1 a)) False)) % 24.57/24.88 Clause #127 (by forward demodulation #[126, 66]): ∀ (a a_1 : Iota), % 24.57/24.88 Or (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) True) % 24.57/24.88 (Or (Eq True False) (Eq (stable (skS.0 1 a)) False)) % 24.57/24.88 Clause #128 (by clausification #[127]): ∀ (a a_1 : Iota), Or (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) True) (Eq (stable (skS.0 1 a)) False) % 24.57/24.88 Clause #129 (by forward demodulation #[128, 65]): ∀ (a a_1 : Iota), Or (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) True) (Eq True False) % 24.57/24.88 Clause #130 (by clausification #[129]): ∀ (a a_1 : Iota), Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) True % 24.57/24.88 Clause #131 (by superposition #[130, 19]): ∀ (a a_1 a_2 : Iota), % 24.57/24.88 Or (Eq (contracts_from (skS.0 2 (skS.0 1 a) a_1) first_movers) True) % 24.57/24.88 (Or (Eq True False) % 24.57/24.88 (Or (Eq (environment (skS.0 1 a)) False) % 24.57/24.88 (Or (Eq (stable (skS.0 1 a)) False) % 24.57/24.88 (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) True)))) % 24.57/24.88 Clause #132 (by superposition #[130, 18]): ∀ (a a_1 a_2 : Iota), % 24.57/24.88 Or (Eq (contracts_from (skS.0 2 (skS.0 1 a) a_1) first_movers) True) % 24.57/24.88 (Or (Eq True False) % 24.57/24.88 (Or (Eq (environment (skS.0 1 a)) False) % 24.57/24.88 (Or (Eq (stable (skS.0 1 a)) False) % 24.57/24.88 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2))) False)))) % 24.57/24.88 Clause #133 (by superposition #[130, 20]): ∀ (a a_1 a_2 : Iota), % 24.57/24.88 Or (Eq (contracts_from (skS.0 2 (skS.0 1 a) a_1) first_movers) True) % 24.57/24.88 (Or (Eq True False) % 24.67/24.94 (Or (Eq (environment (skS.0 1 a)) False) % 24.67/24.94 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/24.94 (Eq (greater (cardinality_at_time first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True)))) % 24.67/24.94 Clause #156 (by clausification #[121]): ∀ (a a_1 : Iota), % 24.67/24.94 Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 2 (skS.0 1 a) a_1)) zero) True) % 24.67/24.94 (Or (Eq (environment (skS.0 1 a)) False) (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) False)) % 24.67/24.94 Clause #157 (by forward demodulation #[156, 66]): ∀ (a a_1 : Iota), % 24.67/24.94 Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 2 (skS.0 1 a) a_1)) zero) True) % 24.67/24.94 (Or (Eq True False) (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) False)) % 24.67/24.94 Clause #158 (by clausification #[157]): ∀ (a a_1 : Iota), % 24.67/24.94 Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 2 (skS.0 1 a) a_1)) zero) True) % 24.67/24.94 (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) False) % 24.67/24.94 Clause #159 (by superposition #[158, 130]): ∀ (a a_1 : Iota), % 24.67/24.94 Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 2 (skS.0 1 a) a_1)) zero) True) (Eq False True) % 24.67/24.94 Clause #160 (by clausification #[159]): ∀ (a a_1 : Iota), Eq (greater (cardinality_at_time efficient_producers (skS.0 2 (skS.0 1 a) a_1)) zero) True % 24.67/24.94 Clause #162 (by superposition #[160, 46]): ∀ (a a_1 a_2 : Iota), % 24.67/24.94 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 2 (skS.0 1 a_1) a_2)) True) % 24.67/24.94 (Or (Eq True False) % 24.67/24.94 (Or (Eq (greater (cardinality_at_time first_movers (skS.0 2 (skS.0 1 a_1) a_2)) zero) False) % 24.67/24.94 (Or (Eq (environment a) False) (Eq (in_environment a (skS.0 2 (skS.0 1 a_1) a_2)) False)))) % 24.67/24.94 Clause #178 (by clausification #[162]): ∀ (a a_1 a_2 : Iota), % 24.67/24.94 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 2 (skS.0 1 a_1) a_2)) True) % 24.67/24.94 (Or (Eq (greater (cardinality_at_time first_movers (skS.0 2 (skS.0 1 a_1) a_2)) zero) False) % 24.67/24.94 (Or (Eq (environment a) False) (Eq (in_environment a (skS.0 2 (skS.0 1 a_1) a_2)) False))) % 24.67/24.94 Clause #179 (by clausification #[131]): ∀ (a a_1 a_2 : Iota), % 24.67/24.94 Or (Eq (contracts_from (skS.0 2 (skS.0 1 a) a_1) first_movers) True) % 24.67/24.94 (Or (Eq (environment (skS.0 1 a)) False) % 24.67/24.94 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/24.94 (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) True))) % 24.67/24.94 Clause #180 (by forward demodulation #[179, 112]): ∀ (a a_1 a_2 : Iota), % 24.67/24.94 Or (Eq False True) % 24.67/24.94 (Or (Eq (environment (skS.0 1 a)) False) % 24.67/24.94 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/24.94 (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) True))) % 24.67/24.94 Clause #181 (by clausification #[180]): ∀ (a a_1 a_2 : Iota), % 24.67/24.94 Or (Eq (environment (skS.0 1 a)) False) % 24.67/24.94 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/24.94 (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) True)) % 24.67/24.94 Clause #182 (by forward demodulation #[181, 66]): ∀ (a a_1 a_2 : Iota), % 24.67/24.94 Or (Eq True False) % 24.67/24.94 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/24.94 (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) True)) % 24.67/24.94 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 : Iota), % 24.67/24.94 Or (Eq (stable (skS.0 1 a)) False) % 24.67/24.94 (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) True) % 24.67/24.94 Clause #184 (by forward demodulation #[183, 65]): ∀ (a a_1 a_2 : Iota), % 24.67/24.94 Or (Eq True False) (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) True) % 24.67/24.94 Clause #185 (by clausification #[184]): ∀ (a a_1 a_2 : Iota), Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) True % 24.67/24.94 Clause #186 (by superposition #[185, 57]): ∀ (a a_1 a_2 : Iota), % 24.67/24.94 Or (Eq True False) % 24.67/24.94 (Or (Eq (greater (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) True) % 24.67/24.94 (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1))) % 24.67/24.94 Clause #187 (by clausification #[133]): ∀ (a a_1 a_2 : Iota), % 24.67/24.94 Or (Eq (contracts_from (skS.0 2 (skS.0 1 a) a_1) first_movers) True) % 24.67/24.94 (Or (Eq (environment (skS.0 1 a)) False) % 24.67/25.00 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/25.00 (Eq (greater (cardinality_at_time first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True))) % 24.67/25.00 Clause #188 (by forward demodulation #[187, 112]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq False True) % 24.67/25.00 (Or (Eq (environment (skS.0 1 a)) False) % 24.67/25.00 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/25.00 (Eq (greater (cardinality_at_time first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True))) % 24.67/25.00 Clause #189 (by clausification #[188]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq (environment (skS.0 1 a)) False) % 24.67/25.00 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/25.00 (Eq (greater (cardinality_at_time first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True)) % 24.67/25.00 Clause #190 (by forward demodulation #[189, 66]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq True False) % 24.67/25.00 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/25.00 (Eq (greater (cardinality_at_time first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True)) % 24.67/25.00 Clause #191 (by clausification #[190]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq (stable (skS.0 1 a)) False) % 24.67/25.00 (Eq (greater (cardinality_at_time first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True) % 24.67/25.00 Clause #192 (by forward demodulation #[191, 65]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq True False) (Eq (greater (cardinality_at_time first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True) % 24.67/25.00 Clause #193 (by clausification #[192]): ∀ (a a_1 a_2 : Iota), Eq (greater (cardinality_at_time first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True % 24.67/25.00 Clause #202 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq (contracts_from (skS.0 2 (skS.0 1 a) a_1) first_movers) True) % 24.67/25.00 (Or (Eq (environment (skS.0 1 a)) False) % 24.67/25.00 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/25.00 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2))) False))) % 24.67/25.00 Clause #203 (by forward demodulation #[202, 112]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq False True) % 24.67/25.00 (Or (Eq (environment (skS.0 1 a)) False) % 24.67/25.00 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/25.00 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2))) False))) % 24.67/25.00 Clause #204 (by clausification #[203]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq (environment (skS.0 1 a)) False) % 24.67/25.00 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/25.00 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2))) False)) % 24.67/25.00 Clause #205 (by forward demodulation #[204, 66]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq True False) % 24.67/25.00 (Or (Eq (stable (skS.0 1 a)) False) % 24.67/25.00 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2))) False)) % 24.67/25.00 Clause #206 (by clausification #[205]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq (stable (skS.0 1 a)) False) % 24.67/25.00 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2))) False) % 24.67/25.00 Clause #207 (by forward demodulation #[206, 65]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq True False) (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2))) False) % 24.67/25.00 Clause #208 (by clausification #[207]): ∀ (a a_1 a_2 : Iota), Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2))) False % 24.67/25.00 Clause #211 (by clausification #[186]): ∀ (a a_1 a_2 : Iota), % 24.67/25.00 Or (Eq (greater (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) True) % 24.67/25.00 (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.67/25.00 Clause #212 (by superposition #[211, 25]): ∀ (a a_1 a_2 a_3 : Iota), % 24.67/25.00 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.67/25.00 (Or (Eq (greater (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) a_3) True) % 24.67/25.00 (Or (Eq True False) (Eq (greater (skS.0 2 (skS.0 1 a) a_1) a_3) False))) % 24.67/25.00 Clause #213 (by superposition #[211, 35]): ∀ (a a_1 a_2 a_3 : Iota), % 24.67/25.00 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.67/25.00 (Or (Eq (in_environment a_3 (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.67/25.00 (Or (Eq True False) % 24.67/25.00 (Or (Eq (in_environment a_3 (skS.0 2 (skS.0 1 a) a_1)) False) % 24.67/25.00 (Or (Eq (environment a_3) False) (Eq (stable a_3) False))))) % 24.67/25.00 Clause #218 (by clausification #[212]): ∀ (a a_1 a_2 a_3 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (greater (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) a_3) True) % 24.80/25.06 (Eq (greater (skS.0 2 (skS.0 1 a) a_1) a_3) False)) % 24.80/25.06 Clause #219 (by superposition #[218, 107]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (greater (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (appear efficient_producers (skS.0 1 a))) True) % 24.80/25.06 (Eq False True)) % 24.80/25.06 Clause #220 (by clausification #[219]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Eq (greater (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (appear efficient_producers (skS.0 1 a))) True) % 24.80/25.06 Clause #224 (by superposition #[220, 52]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (appear efficient_producers (skS.0 1 a))) True) % 24.80/25.06 (Eq True False)) % 24.80/25.06 Clause #226 (by clausification #[224]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (appear efficient_producers (skS.0 1 a))) True) % 24.80/25.06 Clause #227 (by superposition #[226, 40]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True) % 24.80/25.06 (Or (Eq True False) % 24.80/25.06 (Or (Eq (environment (skS.0 1 a)) False) % 24.80/25.06 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) False)))) % 24.80/25.06 Clause #239 (by clausification #[213]): ∀ (a a_1 a_2 a_3 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (in_environment a_3 (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.80/25.06 (Or (Eq (in_environment a_3 (skS.0 2 (skS.0 1 a) a_1)) False) % 24.80/25.06 (Or (Eq (environment a_3) False) (Eq (stable a_3) False)))) % 24.80/25.06 Clause #240 (by superposition #[239, 130]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.80/25.06 (Or (Eq (environment (skS.0 1 a)) False) (Or (Eq (stable (skS.0 1 a)) False) (Eq False True)))) % 24.80/25.06 Clause #253 (by clausification #[240]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.80/25.06 (Or (Eq (environment (skS.0 1 a)) False) (Eq (stable (skS.0 1 a)) False))) % 24.80/25.06 Clause #254 (by forward demodulation #[253, 66]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.80/25.06 (Or (Eq True False) (Eq (stable (skS.0 1 a)) False))) % 24.80/25.06 Clause #255 (by clausification #[254]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) (Eq (stable (skS.0 1 a)) False)) % 24.80/25.06 Clause #256 (by forward demodulation #[255, 65]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) (Eq True False)) % 24.80/25.06 Clause #257 (by clausification #[256]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.80/25.06 Clause #262 (by clausification #[227]): ∀ (a a_1 a_2 : Iota), % 24.80/25.06 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.06 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True) % 24.80/25.06 (Or (Eq (environment (skS.0 1 a)) False) % 24.80/25.06 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) False))) % 24.80/25.12 Clause #263 (by forward demodulation #[262, 66]): ∀ (a a_1 a_2 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True) % 24.80/25.12 (Or (Eq True False) (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) False))) % 24.80/25.12 Clause #264 (by clausification #[263]): ∀ (a a_1 a_2 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True) % 24.80/25.12 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) False)) % 24.80/25.12 Clause #265 (by superposition #[264, 257]): ∀ (a a_1 a_2 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True) % 24.80/25.12 (Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) (Eq False True))) % 24.80/25.12 Clause #266 (by clausification #[265]): ∀ (a a_1 a_2 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True) % 24.80/25.12 (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1))) % 24.80/25.12 Clause #267 (by eliminate duplicate literals #[266]): ∀ (a a_1 a_2 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Eq (greater (cardinality_at_time efficient_producers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) True) % 24.80/25.12 Clause #268 (by superposition #[267, 46]): ∀ (a a_1 a_2 a_3 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Or (Eq (subpopulations first_movers efficient_producers a_3 (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.80/25.12 (Or (Eq True False) % 24.80/25.12 (Or (Eq (greater (cardinality_at_time first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) False) % 24.80/25.12 (Or (Eq (environment a_3) False) (Eq (in_environment a_3 (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) False))))) % 24.80/25.12 Clause #331 (by clausification #[268]): ∀ (a a_1 a_2 a_3 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Or (Eq (subpopulations first_movers efficient_producers a_3 (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.80/25.12 (Or (Eq (greater (cardinality_at_time first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) zero) False) % 24.80/25.12 (Or (Eq (environment a_3) False) (Eq (in_environment a_3 (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) False)))) % 24.80/25.12 Clause #332 (by forward demodulation #[331, 193]): ∀ (a a_1 a_2 a_3 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Or (Eq (subpopulations first_movers efficient_producers a_3 (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.80/25.12 (Or (Eq True False) % 24.80/25.12 (Or (Eq (environment a_3) False) (Eq (in_environment a_3 (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) False)))) % 24.80/25.12 Clause #333 (by clausification #[332]): ∀ (a a_1 a_2 a_3 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Or (Eq (subpopulations first_movers efficient_producers a_3 (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.80/25.12 (Or (Eq (environment a_3) False) (Eq (in_environment a_3 (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) False))) % 24.80/25.12 Clause #334 (by superposition #[333, 66]): ∀ (a a_1 a_2 a_3 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Or % 24.80/25.12 (Eq (subpopulations first_movers efficient_producers (skS.0 1 a_3) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.80/25.12 (Or (Eq (in_environment (skS.0 1 a_3) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) False) (Eq False True))) % 24.80/25.12 Clause #337 (by clausification #[334]): ∀ (a a_1 a_2 a_3 : Iota), % 24.80/25.12 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.80/25.12 (Or % 24.80/25.12 (Eq (subpopulations first_movers efficient_producers (skS.0 1 a_3) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.90/25.18 (Eq (in_environment (skS.0 1 a_3) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) False)) % 24.90/25.18 Clause #338 (by superposition #[337, 257]): ∀ (a a_1 a_2 : Iota), % 24.90/25.18 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.90/25.18 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.90/25.18 (Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) (Eq False True))) % 24.90/25.18 Clause #340 (by clausification #[338]): ∀ (a a_1 a_2 : Iota), % 24.90/25.18 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.90/25.18 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.90/25.18 (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1))) % 24.90/25.18 Clause #341 (by eliminate duplicate literals #[340]): ∀ (a a_1 a_2 : Iota), % 24.90/25.18 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.90/25.18 (Eq (subpopulations first_movers efficient_producers (skS.0 1 a) (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2)) True) % 24.90/25.18 Clause #342 (by superposition #[341, 101]): ∀ (a a_1 a_2 a_3 : Iota), % 24.90/25.18 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.90/25.18 (Or (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2))) True) % 24.90/25.18 (Or (Eq True False) % 24.90/25.18 (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_3)) False))) % 24.90/25.18 Clause #343 (by clausification #[342]): ∀ (a a_1 a_2 a_3 : Iota), % 24.90/25.18 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.90/25.18 (Or (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2))) True) % 24.90/25.18 (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_3)) False)) % 24.90/25.18 Clause #344 (by forward demodulation #[343, 208]): ∀ (a a_1 a_2 a_3 : Iota), % 24.90/25.18 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.90/25.18 (Or (Eq False True) (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_3)) False)) % 24.90/25.18 Clause #345 (by clausification #[344]): ∀ (a a_1 a_2 a_3 : Iota), % 24.90/25.18 Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) % 24.90/25.18 (Eq (greater_or_equal (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_3)) False) % 24.90/25.18 Clause #346 (by superposition #[345, 185]): ∀ (a a_1 a_2 : Iota), Or (Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1)) (Eq False True) % 24.90/25.18 Clause #351 (by clausification #[346]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 0 (skS.0 2 (skS.0 1 a) a_1) a_2) (skS.0 2 (skS.0 1 a) a_1) % 24.90/25.18 Clause #353 (by backward demodulation #[351, 193]): ∀ (a a_1 : Iota), Eq (greater (cardinality_at_time first_movers (skS.0 2 (skS.0 1 a) a_1)) zero) True % 24.90/25.18 Clause #357 (by backward demodulation #[351, 208]): ∀ (a a_1 : Iota), Eq (greater zero (growth_rate first_movers (skS.0 2 (skS.0 1 a) a_1))) False % 24.90/25.18 Clause #381 (by backward demodulation #[353, 178]): ∀ (a a_1 a_2 : Iota), % 24.90/25.18 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 2 (skS.0 1 a_1) a_2)) True) % 24.90/25.18 (Or (Eq True False) (Or (Eq (environment a) False) (Eq (in_environment a (skS.0 2 (skS.0 1 a_1) a_2)) False))) % 24.90/25.18 Clause #390 (by clausification #[381]): ∀ (a a_1 a_2 : Iota), % 24.90/25.18 Or (Eq (subpopulations first_movers efficient_producers a (skS.0 2 (skS.0 1 a_1) a_2)) True) % 24.90/25.18 (Or (Eq (environment a) False) (Eq (in_environment a (skS.0 2 (skS.0 1 a_1) a_2)) False)) % 24.90/25.18 Clause #391 (by superposition #[390, 66]): ∀ (a a_1 a_2 : Iota), % 24.90/25.18 Or (Eq (subpopulations first_movers efficient_producers (skS.0 1 a) (skS.0 2 (skS.0 1 a_1) a_2)) True) % 24.90/25.18 (Or (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a_1) a_2)) False) (Eq False True)) % 24.90/25.18 Clause #392 (by clausification #[391]): ∀ (a a_1 a_2 : Iota), % 24.90/25.18 Or (Eq (subpopulations first_movers efficient_producers (skS.0 1 a) (skS.0 2 (skS.0 1 a_1) a_2)) True) % 24.90/25.18 (Eq (in_environment (skS.0 1 a) (skS.0 2 (skS.0 1 a_1) a_2)) False) % 24.90/25.18 Clause #393 (by superposition #[392, 130]): ∀ (a a_1 : Iota), % 24.90/25.18 Or (Eq (subpopulations first_movers efficient_producers (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) True) (Eq False True) % 24.90/25.20 Clause #394 (by clausification #[393]): ∀ (a a_1 : Iota), Eq (subpopulations first_movers efficient_producers (skS.0 1 a) (skS.0 2 (skS.0 1 a) a_1)) True % 24.90/25.20 Clause #395 (by superposition #[394, 101]): ∀ (a a_1 a_2 : Iota), % 24.90/25.20 Or (Eq (greater zero (growth_rate first_movers (skS.0 2 (skS.0 1 a) a_1))) True) % 24.90/25.20 (Or (Eq True False) (Eq (greater_or_equal (skS.0 2 (skS.0 1 a) a_1) (skS.0 2 (skS.0 1 a) a_2)) False)) % 24.90/25.20 Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 : Iota), % 24.90/25.20 Or (Eq (greater zero (growth_rate first_movers (skS.0 2 (skS.0 1 a) a_1))) True) % 24.90/25.20 (Eq (greater_or_equal (skS.0 2 (skS.0 1 a) a_1) (skS.0 2 (skS.0 1 a) a_2)) False) % 24.90/25.20 Clause #397 (by forward demodulation #[396, 357]): ∀ (a a_1 a_2 : Iota), % 24.90/25.20 Or (Eq False True) (Eq (greater_or_equal (skS.0 2 (skS.0 1 a) a_1) (skS.0 2 (skS.0 1 a) a_2)) False) % 24.90/25.20 Clause #398 (by clausification #[397]): ∀ (a a_1 a_2 : Iota), Eq (greater_or_equal (skS.0 2 (skS.0 1 a) a_1) (skS.0 2 (skS.0 1 a) a_2)) False % 24.90/25.20 Clause #399 (by superposition #[398, 54]): Eq False True % 24.90/25.20 Clause #402 (by clausification #[399]): False % 24.90/25.20 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------