%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT037+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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:18 AM UTC 2026 % Result : Theorem 40.83s 41.11s % Output : Proof 42.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT037+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : duper %s % 0.10/0.36 % Computer : n027.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:46:00 UTC 2026 % 0.10/0.36 % CPUTime : % 40.83/41.11 SZS status Theorem for theBenchmark.p % 40.83/41.11 SZS output start Proof for theBenchmark.p % 40.83/41.11 Clause #0 (by assumption #[]): Eq % 40.83/41.11 (∀ (E T : Iota), % 40.83/41.11 And (And (environment E) (greater_or_equal T (appear efficient_producers E))) % 40.83/41.11 (Eq (cardinality_at_time efficient_producers T) zero) → % 40.83/41.11 Exists fun To => % 40.83/41.11 And (And (And (greater To (appear efficient_producers E)) (in_environment E To)) (greater T To)) % 40.83/41.11 (greater zero (growth_rate efficient_producers To))) % 40.83/41.11 True % 40.83/41.11 Clause #1 (by assumption #[]): Eq % 40.83/41.11 (∀ (E T : Iota), % 40.83/41.11 And (And (environment E) (in_environment E T)) (greater (appear an_organisation E) T) → % 40.83/41.11 Eq (number_of_organizations E T) zero) % 40.83/41.11 True % 40.83/41.11 Clause #2 (by assumption #[]): Eq % 40.83/41.11 (∀ (E T : Iota), % 40.83/41.11 And (And (environment E) (in_environment E T)) (Not (decreases (number_of_organizations E T))) → % 40.83/41.11 Exists fun X => % 40.83/41.11 And (And (subpopulation X E T) (greater (cardinality_at_time X T) zero)) (Not (greater zero (growth_rate X T)))) % 40.83/41.11 True % 40.83/41.11 Clause #3 (by assumption #[]): Eq % 40.83/41.11 (∀ (E T X : Iota), % 40.83/41.11 And (And (And (environment E) (in_environment E T)) (Eq (number_of_organizations E T) zero)) (subpopulation X E T) → % 40.83/41.11 Eq (cardinality_at_time X T) zero) % 40.83/41.11 True % 40.83/41.11 Clause #4 (by assumption #[]): Eq % 40.83/41.11 (∀ (E T : Iota), % 40.83/41.11 And (environment E) (in_environment E T) → % 40.83/41.11 And (subpopulation first_movers E T) (subpopulation efficient_producers E T)) % 40.83/41.11 True % 40.83/41.11 Clause #5 (by assumption #[]): Eq (∀ (S T : Iota), Eq (cardinality_at_time S T) zero → Not (greater zero (growth_rate S T))) True % 40.83/41.11 Clause #6 (by assumption #[]): Eq % 40.83/41.11 (∀ (E T : Iota), % 40.83/41.11 And (environment E) (in_environment E T) → % 40.83/41.11 Or (Eq (cardinality_at_time efficient_producers T) zero) % 40.83/41.11 (greater (cardinality_at_time efficient_producers T) zero)) % 40.83/41.11 True % 40.83/41.11 Clause #7 (by assumption #[]): Eq (∀ (X : Iota), constant X → Not (decreases X)) True % 40.83/41.11 Clause #8 (by assumption #[]): Eq % 40.83/41.11 (∀ (E T : Iota), % 40.83/41.11 And (environment E) (in_environment E T) → % 40.83/41.11 Or (greater_or_equal T (appear an_organisation E)) (greater (appear an_organisation E) T)) % 40.83/41.11 True % 40.83/41.11 Clause #9 (by assumption #[]): Eq % 40.83/41.11 (∀ (E T : Iota), % 40.83/41.11 And (And (environment E) (in_environment E T)) (greater (number_of_organizations E T) zero) → % 40.83/41.11 And (greater (equilibrium E) T → decreases (resources E T)) % 40.83/41.11 (Not (greater (equilibrium E) T) → constant (resources E T))) % 40.83/41.11 True % 40.83/41.11 Clause #10 (by assumption #[]): Eq % 40.83/41.11 (∀ (E T : Iota), % 40.83/41.11 And (And (environment E) (in_environment E T)) (greater_or_equal T (appear an_organisation E)) → % 40.83/41.11 greater (number_of_organizations E T) zero) % 40.83/41.11 True % 40.83/41.11 Clause #11 (by assumption #[]): Eq % 40.83/41.11 (∀ (E T : Iota), % 40.83/41.11 And (environment E) (in_environment E T) → % 40.83/41.11 And (decreases (resources E T) → Not (decreases (number_of_organizations E T))) % 40.83/41.11 (constant (resources E T) → constant (number_of_organizations E T))) % 40.83/41.11 True % 40.83/41.11 Clause #12 (by assumption #[]): Eq % 40.83/41.11 (∀ (E S1 S2 T : Iota), % 40.83/41.11 And (And (And (environment E) (in_environment E T)) (Not (greater zero (growth_rate S1 T)))) % 40.83/41.11 (greater (resilience S2) (resilience S1)) → % 40.83/41.11 Not (greater zero (growth_rate S2 T))) % 40.83/41.11 True % 40.83/41.11 Clause #13 (by assumption #[]): Eq (greater (resilience efficient_producers) (resilience first_movers)) True % 40.83/41.11 Clause #14 (by assumption #[]): Eq % 40.83/41.11 (∀ (E X T : Iota), % 40.83/41.11 And (And (environment E) (subpopulation X E T)) (greater (cardinality_at_time X T) zero) → % 40.83/41.11 Or (Eq X efficient_producers) (Eq X first_movers)) % 40.83/41.11 True % 40.83/41.11 Clause #15 (by assumption #[]): Eq % 40.83/41.11 (Not % 40.83/41.11 (∀ (E T : Iota), % 40.83/41.11 And (And (environment E) (in_environment E T)) (greater_or_equal T (appear efficient_producers E)) → % 40.83/41.11 greater (cardinality_at_time efficient_producers T) zero)) % 40.83/41.11 True % 40.83/41.11 Clause #16 (by clausification #[7]): ∀ (a : Iota), Eq (constant a → Not (decreases a)) True % 40.83/41.11 Clause #17 (by clausification #[16]): ∀ (a : Iota), Or (Eq (constant a) False) (Eq (Not (decreases a)) True) % 40.83/41.11 Clause #18 (by clausification #[17]): ∀ (a : Iota), Or (Eq (constant a) False) (Eq (decreases a) False) % 40.83/41.11 Clause #19 (by clausification #[10]): ∀ (a : Iota), % 40.83/41.11 Eq % 40.93/41.17 (∀ (T : Iota), % 40.93/41.17 And (And (environment a) (in_environment a T)) (greater_or_equal T (appear an_organisation a)) → % 40.93/41.17 greater (number_of_organizations a T) zero) % 40.93/41.17 True % 40.93/41.17 Clause #20 (by clausification #[19]): ∀ (a a_1 : Iota), % 40.93/41.17 Eq % 40.93/41.17 (And (And (environment a) (in_environment a a_1)) (greater_or_equal a_1 (appear an_organisation a)) → % 40.93/41.17 greater (number_of_organizations a a_1) zero) % 40.93/41.17 True % 40.93/41.17 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), % 40.93/41.17 Or (Eq (And (And (environment a) (in_environment a a_1)) (greater_or_equal a_1 (appear an_organisation a))) False) % 40.93/41.17 (Eq (greater (number_of_organizations a a_1) zero) True) % 40.93/41.17 Clause #22 (by clausification #[21]): ∀ (a a_1 : Iota), % 40.93/41.17 Or (Eq (greater (number_of_organizations a a_1) zero) True) % 40.93/41.17 (Or (Eq (And (environment a) (in_environment a a_1)) False) % 40.93/41.17 (Eq (greater_or_equal a_1 (appear an_organisation a)) False)) % 40.93/41.17 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), % 40.93/41.17 Or (Eq (greater (number_of_organizations a a_1) zero) True) % 40.93/41.17 (Or (Eq (greater_or_equal a_1 (appear an_organisation a)) False) % 40.93/41.17 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False))) % 40.93/41.17 Clause #24 (by clausification #[1]): ∀ (a : Iota), % 40.93/41.17 Eq % 40.93/41.17 (∀ (T : Iota), % 40.93/41.17 And (And (environment a) (in_environment a T)) (greater (appear an_organisation a) T) → % 40.93/41.17 Eq (number_of_organizations a T) zero) % 40.93/41.17 True % 40.93/41.17 Clause #25 (by clausification #[24]): ∀ (a a_1 : Iota), % 40.93/41.17 Eq % 40.93/41.17 (And (And (environment a) (in_environment a a_1)) (greater (appear an_organisation a) a_1) → % 40.93/41.17 Eq (number_of_organizations a a_1) zero) % 40.93/41.17 True % 40.93/41.17 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), % 40.93/41.17 Or (Eq (And (And (environment a) (in_environment a a_1)) (greater (appear an_organisation a) a_1)) False) % 40.93/41.17 (Eq (Eq (number_of_organizations a a_1) zero) True) % 40.93/41.17 Clause #27 (by clausification #[26]): ∀ (a a_1 : Iota), % 40.93/41.17 Or (Eq (Eq (number_of_organizations a a_1) zero) True) % 40.93/41.17 (Or (Eq (And (environment a) (in_environment a a_1)) False) (Eq (greater (appear an_organisation a) a_1) False)) % 40.93/41.17 Clause #28 (by clausification #[27]): ∀ (a a_1 : Iota), % 40.93/41.17 Or (Eq (And (environment a) (in_environment a a_1)) False) % 40.93/41.17 (Or (Eq (greater (appear an_organisation a) a_1) False) (Eq (number_of_organizations a a_1) zero)) % 40.93/41.17 Clause #29 (by clausification #[28]): ∀ (a a_1 : Iota), % 40.93/41.17 Or (Eq (greater (appear an_organisation a) a_1) False) % 40.93/41.17 (Or (Eq (number_of_organizations a a_1) zero) (Or (Eq (environment a) False) (Eq (in_environment a a_1) False))) % 40.93/41.17 Clause #30 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (T : Iota), Eq (cardinality_at_time a T) zero → Not (greater zero (growth_rate a T))) True % 40.93/41.17 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), Eq (Eq (cardinality_at_time a a_1) zero → Not (greater zero (growth_rate a a_1))) True % 40.93/41.17 Clause #32 (by clausification #[31]): ∀ (a a_1 : Iota), Or (Eq (Eq (cardinality_at_time a a_1) zero) False) (Eq (Not (greater zero (growth_rate a a_1))) True) % 40.93/41.17 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), Or (Eq (Not (greater zero (growth_rate a a_1))) True) (Ne (cardinality_at_time a a_1) zero) % 40.93/41.17 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), Or (Ne (cardinality_at_time a a_1) zero) (Eq (greater zero (growth_rate a a_1)) False) % 40.93/41.17 Clause #35 (by clausification #[0]): ∀ (a : Iota), % 40.93/41.17 Eq % 40.93/41.17 (∀ (T : Iota), % 40.93/41.17 And (And (environment a) (greater_or_equal T (appear efficient_producers a))) % 40.93/41.17 (Eq (cardinality_at_time efficient_producers T) zero) → % 40.93/41.17 Exists fun To => % 40.93/41.17 And (And (And (greater To (appear efficient_producers a)) (in_environment a To)) (greater T To)) % 40.93/41.17 (greater zero (growth_rate efficient_producers To))) % 40.93/41.17 True % 40.93/41.17 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), % 40.93/41.17 Eq % 40.93/41.17 (And (And (environment a) (greater_or_equal a_1 (appear efficient_producers a))) % 40.93/41.17 (Eq (cardinality_at_time efficient_producers a_1) zero) → % 40.93/41.17 Exists fun To => % 40.93/41.17 And (And (And (greater To (appear efficient_producers a)) (in_environment a To)) (greater a_1 To)) % 40.93/41.17 (greater zero (growth_rate efficient_producers To))) % 40.98/41.25 True % 40.98/41.25 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), % 40.98/41.25 Or % 40.98/41.25 (Eq % 40.98/41.25 (And (And (environment a) (greater_or_equal a_1 (appear efficient_producers a))) % 40.98/41.25 (Eq (cardinality_at_time efficient_producers a_1) zero)) % 40.98/41.25 False) % 40.98/41.25 (Eq % 40.98/41.25 (Exists fun To => % 40.98/41.25 And (And (And (greater To (appear efficient_producers a)) (in_environment a To)) (greater a_1 To)) % 40.98/41.25 (greater zero (growth_rate efficient_producers To))) % 40.98/41.25 True) % 40.98/41.25 Clause #38 (by clausification #[37]): ∀ (a a_1 : Iota), % 40.98/41.25 Or % 40.98/41.25 (Eq % 40.98/41.25 (Exists fun To => % 40.98/41.25 And (And (And (greater To (appear efficient_producers a)) (in_environment a To)) (greater a_1 To)) % 40.98/41.25 (greater zero (growth_rate efficient_producers To))) % 40.98/41.25 True) % 40.98/41.25 (Or (Eq (And (environment a) (greater_or_equal a_1 (appear efficient_producers a))) False) % 40.98/41.25 (Eq (Eq (cardinality_at_time efficient_producers a_1) zero) False)) % 40.98/41.25 Clause #39 (by clausification #[38]): ∀ (a a_1 a_2 : Iota), % 40.98/41.25 Or (Eq (And (environment a) (greater_or_equal a_1 (appear efficient_producers a))) False) % 40.98/41.25 (Or (Eq (Eq (cardinality_at_time efficient_producers a_1) zero) False) % 40.98/41.25 (Eq % 40.98/41.25 (And % 40.98/41.25 (And (And (greater (skS.0 0 a a_1 a_2) (appear efficient_producers a)) (in_environment a (skS.0 0 a a_1 a_2))) % 40.98/41.25 (greater a_1 (skS.0 0 a a_1 a_2))) % 40.98/41.25 (greater zero (growth_rate efficient_producers (skS.0 0 a a_1 a_2)))) % 40.98/41.25 True)) % 40.98/41.25 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 40.98/41.25 Or (Eq (Eq (cardinality_at_time efficient_producers a) zero) False) % 40.98/41.25 (Or % 40.98/41.25 (Eq % 40.98/41.25 (And % 40.98/41.25 (And % 40.98/41.25 (And (greater (skS.0 0 a_1 a a_2) (appear efficient_producers a_1)) % 40.98/41.25 (in_environment a_1 (skS.0 0 a_1 a a_2))) % 40.98/41.25 (greater a (skS.0 0 a_1 a a_2))) % 40.98/41.25 (greater zero (growth_rate efficient_producers (skS.0 0 a_1 a a_2)))) % 40.98/41.25 True) % 40.98/41.25 (Or (Eq (environment a_1) False) (Eq (greater_or_equal a (appear efficient_producers a_1)) False))) % 40.98/41.25 Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 : Iota), % 40.98/41.25 Or % 40.98/41.25 (Eq % 40.98/41.25 (And % 40.98/41.25 (And (And (greater (skS.0 0 a a_1 a_2) (appear efficient_producers a)) (in_environment a (skS.0 0 a a_1 a_2))) % 40.98/41.25 (greater a_1 (skS.0 0 a a_1 a_2))) % 40.98/41.25 (greater zero (growth_rate efficient_producers (skS.0 0 a a_1 a_2)))) % 40.98/41.25 True) % 40.98/41.25 (Or (Eq (environment a) False) % 40.98/41.25 (Or (Eq (greater_or_equal a_1 (appear efficient_producers a)) False) % 40.98/41.25 (Ne (cardinality_at_time efficient_producers a_1) zero))) % 40.98/41.25 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 : Iota), % 40.98/41.25 Or (Eq (environment a) False) % 40.98/41.25 (Or (Eq (greater_or_equal a_1 (appear efficient_producers a)) False) % 40.98/41.25 (Or (Ne (cardinality_at_time efficient_producers a_1) zero) % 40.98/41.25 (Eq (greater zero (growth_rate efficient_producers (skS.0 0 a a_1 a_2))) True))) % 40.98/41.25 Clause #43 (by clausification #[41]): ∀ (a a_1 a_2 : Iota), % 40.98/41.25 Or (Eq (environment a) False) % 40.98/41.25 (Or (Eq (greater_or_equal a_1 (appear efficient_producers a)) False) % 40.98/41.25 (Or (Ne (cardinality_at_time efficient_producers a_1) zero) % 40.98/41.25 (Eq % 40.98/41.25 (And (And (greater (skS.0 0 a a_1 a_2) (appear efficient_producers a)) (in_environment a (skS.0 0 a a_1 a_2))) % 40.98/41.25 (greater a_1 (skS.0 0 a a_1 a_2))) % 40.98/41.25 True))) % 40.98/41.25 Clause #44 (by clausification #[15]): Eq % 40.98/41.25 (∀ (E T : Iota), % 40.98/41.25 And (And (environment E) (in_environment E T)) (greater_or_equal T (appear efficient_producers E)) → % 40.98/41.25 greater (cardinality_at_time efficient_producers T) zero) % 40.98/41.25 False % 40.98/41.25 Clause #45 (by clausification #[44]): ∀ (a : Iota), % 40.98/41.25 Eq % 40.98/41.25 (Not % 40.98/41.25 (∀ (T : Iota), % 40.98/41.25 And (And (environment (skS.0 1 a)) (in_environment (skS.0 1 a) T)) % 40.98/41.25 (greater_or_equal T (appear efficient_producers (skS.0 1 a))) → % 40.98/41.25 greater (cardinality_at_time efficient_producers T) zero)) % 40.98/41.25 True % 40.98/41.25 Clause #46 (by clausification #[45]): ∀ (a : Iota), % 40.98/41.25 Eq % 40.98/41.25 (∀ (T : Iota), % 40.98/41.25 And (And (environment (skS.0 1 a)) (in_environment (skS.0 1 a) T)) % 40.98/41.25 (greater_or_equal T (appear efficient_producers (skS.0 1 a))) → % 40.98/41.25 greater (cardinality_at_time efficient_producers T) zero) % 41.08/41.33 False % 41.08/41.33 Clause #47 (by clausification #[46]): ∀ (a a_1 : Iota), % 41.08/41.33 Eq % 41.08/41.33 (Not % 41.08/41.33 (And (And (environment (skS.0 1 a)) (in_environment (skS.0 1 a) (skS.0 2 a a_1))) % 41.08/41.33 (greater_or_equal (skS.0 2 a a_1) (appear efficient_producers (skS.0 1 a))) → % 41.08/41.33 greater (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero)) % 41.08/41.33 True % 41.08/41.33 Clause #48 (by clausification #[47]): ∀ (a a_1 : Iota), % 41.08/41.33 Eq % 41.08/41.33 (And (And (environment (skS.0 1 a)) (in_environment (skS.0 1 a) (skS.0 2 a a_1))) % 41.08/41.33 (greater_or_equal (skS.0 2 a a_1) (appear efficient_producers (skS.0 1 a))) → % 41.08/41.33 greater (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) % 41.08/41.33 False % 41.08/41.33 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), % 41.08/41.33 Eq % 41.08/41.33 (And (And (environment (skS.0 1 a)) (in_environment (skS.0 1 a) (skS.0 2 a a_1))) % 41.08/41.33 (greater_or_equal (skS.0 2 a a_1) (appear efficient_producers (skS.0 1 a)))) % 41.08/41.33 True % 41.08/41.33 Clause #50 (by clausification #[48]): ∀ (a a_1 : Iota), Eq (greater (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) False % 41.08/41.33 Clause #51 (by clausification #[49]): ∀ (a a_1 : Iota), Eq (greater_or_equal (skS.0 2 a a_1) (appear efficient_producers (skS.0 1 a))) True % 41.08/41.33 Clause #52 (by clausification #[49]): ∀ (a a_1 : Iota), Eq (And (environment (skS.0 1 a)) (in_environment (skS.0 1 a) (skS.0 2 a a_1))) True % 41.08/41.33 Clause #53 (by clausification #[3]): ∀ (a : Iota), % 41.08/41.33 Eq % 41.08/41.33 (∀ (T X : Iota), % 41.08/41.33 And (And (And (environment a) (in_environment a T)) (Eq (number_of_organizations a T) zero)) % 41.08/41.33 (subpopulation X a T) → % 41.08/41.33 Eq (cardinality_at_time X T) zero) % 41.08/41.33 True % 41.08/41.33 Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota), % 41.08/41.33 Eq % 41.08/41.33 (∀ (X : Iota), % 41.08/41.33 And (And (And (environment a) (in_environment a a_1)) (Eq (number_of_organizations a a_1) zero)) % 41.08/41.33 (subpopulation X a a_1) → % 41.08/41.33 Eq (cardinality_at_time X a_1) zero) % 41.08/41.33 True % 41.08/41.33 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 : Iota), % 41.08/41.33 Eq % 41.08/41.33 (And (And (And (environment a) (in_environment a a_1)) (Eq (number_of_organizations a a_1) zero)) % 41.08/41.33 (subpopulation a_2 a a_1) → % 41.08/41.33 Eq (cardinality_at_time a_2 a_1) zero) % 41.08/41.33 True % 41.08/41.33 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 : Iota), % 41.08/41.33 Or % 41.08/41.33 (Eq % 41.08/41.33 (And (And (And (environment a) (in_environment a a_1)) (Eq (number_of_organizations a a_1) zero)) % 41.08/41.33 (subpopulation a_2 a a_1)) % 41.08/41.33 False) % 41.08/41.33 (Eq (Eq (cardinality_at_time a_2 a_1) zero) True) % 41.08/41.33 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 : Iota), % 41.08/41.33 Or (Eq (Eq (cardinality_at_time a a_1) zero) True) % 41.08/41.33 (Or (Eq (And (And (environment a_2) (in_environment a_2 a_1)) (Eq (number_of_organizations a_2 a_1) zero)) False) % 41.08/41.33 (Eq (subpopulation a a_2 a_1) False)) % 41.08/41.33 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 : Iota), % 41.08/41.33 Or (Eq (And (And (environment a) (in_environment a a_1)) (Eq (number_of_organizations a a_1) zero)) False) % 41.08/41.33 (Or (Eq (subpopulation a_2 a a_1) False) (Eq (cardinality_at_time a_2 a_1) zero)) % 41.08/41.33 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 : Iota), % 41.08/41.33 Or (Eq (subpopulation a a_1 a_2) False) % 41.08/41.33 (Or (Eq (cardinality_at_time a a_2) zero) % 41.08/41.33 (Or (Eq (And (environment a_1) (in_environment a_1 a_2)) False) % 41.08/41.33 (Eq (Eq (number_of_organizations a_1 a_2) zero) False))) % 41.08/41.33 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 : Iota), % 41.08/41.33 Or (Eq (subpopulation a a_1 a_2) False) % 41.08/41.33 (Or (Eq (cardinality_at_time a a_2) zero) % 41.08/41.33 (Or (Eq (Eq (number_of_organizations a_1 a_2) zero) False) % 41.08/41.33 (Or (Eq (environment a_1) False) (Eq (in_environment a_1 a_2) False)))) % 41.08/41.33 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 : Iota), % 41.08/41.33 Or (Eq (subpopulation a a_1 a_2) False) % 41.08/41.33 (Or (Eq (cardinality_at_time a a_2) zero) % 41.08/41.33 (Or (Eq (environment a_1) False) % 41.08/41.33 (Or (Eq (in_environment a_1 a_2) False) (Ne (number_of_organizations a_1 a_2) zero)))) % 41.08/41.33 Clause #62 (by clausification #[12]): ∀ (a : Iota), % 41.08/41.33 Eq % 41.08/41.33 (∀ (S1 S2 T : Iota), % 41.08/41.33 And (And (And (environment a) (in_environment a T)) (Not (greater zero (growth_rate S1 T)))) % 41.08/41.33 (greater (resilience S2) (resilience S1)) → % 41.18/41.42 Not (greater zero (growth_rate S2 T))) % 41.18/41.42 True % 41.18/41.42 Clause #63 (by clausification #[62]): ∀ (a a_1 : Iota), % 41.18/41.42 Eq % 41.18/41.42 (∀ (S2 T : Iota), % 41.18/41.42 And (And (And (environment a) (in_environment a T)) (Not (greater zero (growth_rate a_1 T)))) % 41.18/41.42 (greater (resilience S2) (resilience a_1)) → % 41.18/41.42 Not (greater zero (growth_rate S2 T))) % 41.18/41.42 True % 41.18/41.42 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 : Iota), % 41.18/41.42 Eq % 41.18/41.42 (∀ (T : Iota), % 41.18/41.42 And (And (And (environment a) (in_environment a T)) (Not (greater zero (growth_rate a_1 T)))) % 41.18/41.42 (greater (resilience a_2) (resilience a_1)) → % 41.18/41.42 Not (greater zero (growth_rate a_2 T))) % 41.18/41.42 True % 41.18/41.42 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 a_3 : Iota), % 41.18/41.42 Eq % 41.18/41.42 (And (And (And (environment a) (in_environment a a_1)) (Not (greater zero (growth_rate a_2 a_1)))) % 41.18/41.42 (greater (resilience a_3) (resilience a_2)) → % 41.18/41.42 Not (greater zero (growth_rate a_3 a_1))) % 41.18/41.42 True % 41.18/41.42 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 a_3 : Iota), % 41.18/41.42 Or % 41.18/41.42 (Eq % 41.18/41.42 (And (And (And (environment a) (in_environment a a_1)) (Not (greater zero (growth_rate a_2 a_1)))) % 41.18/41.42 (greater (resilience a_3) (resilience a_2))) % 41.18/41.42 False) % 41.18/41.42 (Eq (Not (greater zero (growth_rate a_3 a_1))) True) % 41.18/41.42 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 a_3 : Iota), % 41.18/41.42 Or (Eq (Not (greater zero (growth_rate a a_1))) True) % 41.18/41.42 (Or (Eq (And (And (environment a_2) (in_environment a_2 a_1)) (Not (greater zero (growth_rate a_3 a_1)))) False) % 41.18/41.42 (Eq (greater (resilience a) (resilience a_3)) False)) % 41.18/41.42 Clause #68 (by clausification #[67]): ∀ (a a_1 a_2 a_3 : Iota), % 41.18/41.42 Or (Eq (And (And (environment a) (in_environment a a_1)) (Not (greater zero (growth_rate a_2 a_1)))) False) % 41.18/41.42 (Or (Eq (greater (resilience a_3) (resilience a_2)) False) (Eq (greater zero (growth_rate a_3 a_1)) False)) % 41.18/41.42 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 a_3 : Iota), % 41.18/41.42 Or (Eq (greater (resilience a) (resilience a_1)) False) % 41.18/41.42 (Or (Eq (greater zero (growth_rate a a_2)) False) % 41.18/41.42 (Or (Eq (And (environment a_3) (in_environment a_3 a_2)) False) % 41.18/41.42 (Eq (Not (greater zero (growth_rate a_1 a_2))) False))) % 41.18/41.42 Clause #70 (by clausification #[69]): ∀ (a a_1 a_2 a_3 : Iota), % 41.18/41.42 Or (Eq (greater (resilience a) (resilience a_1)) False) % 41.18/41.42 (Or (Eq (greater zero (growth_rate a a_2)) False) % 41.18/41.42 (Or (Eq (Not (greater zero (growth_rate a_1 a_2))) False) % 41.18/41.42 (Or (Eq (environment a_3) False) (Eq (in_environment a_3 a_2) False)))) % 41.18/41.42 Clause #71 (by clausification #[70]): ∀ (a a_1 a_2 a_3 : Iota), % 41.18/41.42 Or (Eq (greater (resilience a) (resilience a_1)) False) % 41.18/41.42 (Or (Eq (greater zero (growth_rate a a_2)) False) % 41.18/41.42 (Or (Eq (environment a_3) False) % 41.18/41.42 (Or (Eq (in_environment a_3 a_2) False) (Eq (greater zero (growth_rate a_1 a_2)) True)))) % 41.18/41.42 Clause #72 (by superposition #[71, 13]): ∀ (a a_1 : Iota), % 41.18/41.42 Or (Eq (greater zero (growth_rate efficient_producers a)) False) % 41.18/41.42 (Or (Eq (environment a_1) False) % 41.18/41.42 (Or (Eq (in_environment a_1 a) False) (Or (Eq (greater zero (growth_rate first_movers a)) True) (Eq False True)))) % 41.18/41.42 Clause #73 (by clausification #[4]): ∀ (a : Iota), % 41.18/41.42 Eq % 41.18/41.42 (∀ (T : Iota), % 41.18/41.42 And (environment a) (in_environment a T) → % 41.18/41.42 And (subpopulation first_movers a T) (subpopulation efficient_producers a T)) % 41.18/41.42 True % 41.18/41.42 Clause #74 (by clausification #[73]): ∀ (a a_1 : Iota), % 41.18/41.42 Eq % 41.18/41.42 (And (environment a) (in_environment a a_1) → % 41.18/41.42 And (subpopulation first_movers a a_1) (subpopulation efficient_producers a a_1)) % 41.18/41.42 True % 41.18/41.42 Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota), % 41.18/41.42 Or (Eq (And (environment a) (in_environment a a_1)) False) % 41.18/41.42 (Eq (And (subpopulation first_movers a a_1) (subpopulation efficient_producers a a_1)) True) % 41.18/41.42 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), % 41.18/41.42 Or (Eq (And (subpopulation first_movers a a_1) (subpopulation efficient_producers a a_1)) True) % 41.18/41.42 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False)) % 41.18/41.42 Clause #78 (by clausification #[76]): ∀ (a a_1 : Iota), % 41.18/41.42 Or (Eq (environment a) False) (Or (Eq (in_environment a a_1) False) (Eq (subpopulation first_movers a a_1) True)) % 41.28/41.50 Clause #79 (by clausification #[2]): ∀ (a : Iota), % 41.28/41.50 Eq % 41.28/41.50 (∀ (T : Iota), % 41.28/41.50 And (And (environment a) (in_environment a T)) (Not (decreases (number_of_organizations a T))) → % 41.28/41.50 Exists fun X => % 41.28/41.50 And (And (subpopulation X a T) (greater (cardinality_at_time X T) zero)) % 41.28/41.50 (Not (greater zero (growth_rate X T)))) % 41.28/41.50 True % 41.28/41.50 Clause #80 (by clausification #[79]): ∀ (a a_1 : Iota), % 41.28/41.50 Eq % 41.28/41.50 (And (And (environment a) (in_environment a a_1)) (Not (decreases (number_of_organizations a a_1))) → % 41.28/41.50 Exists fun X => % 41.28/41.50 And (And (subpopulation X a a_1) (greater (cardinality_at_time X a_1) zero)) % 41.28/41.50 (Not (greater zero (growth_rate X a_1)))) % 41.28/41.50 True % 41.28/41.50 Clause #81 (by clausification #[80]): ∀ (a a_1 : Iota), % 41.28/41.50 Or (Eq (And (And (environment a) (in_environment a a_1)) (Not (decreases (number_of_organizations a a_1)))) False) % 41.28/41.50 (Eq % 41.28/41.50 (Exists fun X => % 41.28/41.50 And (And (subpopulation X a a_1) (greater (cardinality_at_time X a_1) zero)) % 41.28/41.50 (Not (greater zero (growth_rate X a_1)))) % 41.28/41.50 True) % 41.28/41.50 Clause #82 (by clausification #[81]): ∀ (a a_1 : Iota), % 41.28/41.50 Or % 41.28/41.50 (Eq % 41.28/41.50 (Exists fun X => % 41.28/41.50 And (And (subpopulation X a a_1) (greater (cardinality_at_time X a_1) zero)) % 41.28/41.50 (Not (greater zero (growth_rate X a_1)))) % 41.28/41.50 True) % 41.28/41.50 (Or (Eq (And (environment a) (in_environment a a_1)) False) % 41.28/41.50 (Eq (Not (decreases (number_of_organizations a a_1))) False)) % 41.28/41.50 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 : Iota), % 41.28/41.50 Or (Eq (And (environment a) (in_environment a a_1)) False) % 41.28/41.50 (Or (Eq (Not (decreases (number_of_organizations a a_1))) False) % 41.28/41.50 (Eq % 41.28/41.50 (And % 41.28/41.50 (And (subpopulation (skS.0 3 a a_1 a_2) a a_1) (greater (cardinality_at_time (skS.0 3 a a_1 a_2) a_1) zero)) % 41.28/41.50 (Not (greater zero (growth_rate (skS.0 3 a a_1 a_2) a_1)))) % 41.28/41.50 True)) % 41.28/41.50 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 : Iota), % 41.28/41.50 Or (Eq (Not (decreases (number_of_organizations a a_1))) False) % 41.28/41.50 (Or % 41.28/41.50 (Eq % 41.28/41.50 (And % 41.28/41.50 (And (subpopulation (skS.0 3 a a_1 a_2) a a_1) (greater (cardinality_at_time (skS.0 3 a a_1 a_2) a_1) zero)) % 41.28/41.50 (Not (greater zero (growth_rate (skS.0 3 a a_1 a_2) a_1)))) % 41.28/41.50 True) % 41.28/41.50 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False))) % 41.28/41.50 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 : Iota), % 41.28/41.50 Or % 41.28/41.50 (Eq % 41.28/41.50 (And (And (subpopulation (skS.0 3 a a_1 a_2) a a_1) (greater (cardinality_at_time (skS.0 3 a a_1 a_2) a_1) zero)) % 41.28/41.50 (Not (greater zero (growth_rate (skS.0 3 a a_1 a_2) a_1)))) % 41.28/41.50 True) % 41.28/41.50 (Or (Eq (environment a) False) % 41.28/41.50 (Or (Eq (in_environment a a_1) False) (Eq (decreases (number_of_organizations a a_1)) True))) % 41.28/41.50 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 : Iota), % 41.28/41.50 Or (Eq (environment a) False) % 41.28/41.50 (Or (Eq (in_environment a a_1) False) % 41.28/41.50 (Or (Eq (decreases (number_of_organizations a a_1)) True) % 41.28/41.50 (Eq (Not (greater zero (growth_rate (skS.0 3 a a_1 a_2) a_1))) True))) % 41.28/41.50 Clause #87 (by clausification #[85]): ∀ (a a_1 a_2 : Iota), % 41.28/41.51 Or (Eq (environment a) False) % 41.28/41.51 (Or (Eq (in_environment a a_1) False) % 41.28/41.51 (Or (Eq (decreases (number_of_organizations a a_1)) True) % 41.28/41.51 (Eq (And (subpopulation (skS.0 3 a a_1 a_2) a a_1) (greater (cardinality_at_time (skS.0 3 a a_1 a_2) a_1) zero)) % 41.28/41.51 True))) % 41.28/41.51 Clause #88 (by clausification #[86]): ∀ (a a_1 a_2 : Iota), % 41.28/41.51 Or (Eq (environment a) False) % 41.28/41.51 (Or (Eq (in_environment a a_1) False) % 41.28/41.51 (Or (Eq (decreases (number_of_organizations a a_1)) True) % 41.28/41.51 (Eq (greater zero (growth_rate (skS.0 3 a a_1 a_2) a_1)) False))) % 41.28/41.51 Clause #89 (by clausification #[14]): ∀ (a : Iota), % 41.28/41.51 Eq % 41.28/41.51 (∀ (X T : Iota), % 41.28/41.51 And (And (environment a) (subpopulation X a T)) (greater (cardinality_at_time X T) zero) → % 41.28/41.51 Or (Eq X efficient_producers) (Eq X first_movers)) % 41.28/41.51 True % 41.28/41.51 Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota), % 41.28/41.51 Eq % 41.28/41.51 (∀ (T : Iota), % 41.28/41.51 And (And (environment a) (subpopulation a_1 a T)) (greater (cardinality_at_time a_1 T) zero) → % 41.28/41.51 Or (Eq a_1 efficient_producers) (Eq a_1 first_movers)) % 41.28/41.60 True % 41.28/41.60 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), % 41.28/41.60 Eq % 41.28/41.60 (And (And (environment a) (subpopulation a_1 a a_2)) (greater (cardinality_at_time a_1 a_2) zero) → % 41.28/41.60 Or (Eq a_1 efficient_producers) (Eq a_1 first_movers)) % 41.28/41.60 True % 41.28/41.60 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), % 41.28/41.60 Or (Eq (And (And (environment a) (subpopulation a_1 a a_2)) (greater (cardinality_at_time a_1 a_2) zero)) False) % 41.28/41.60 (Eq (Or (Eq a_1 efficient_producers) (Eq a_1 first_movers)) True) % 41.28/41.60 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 : Iota), % 41.28/41.60 Or (Eq (Or (Eq a efficient_producers) (Eq a first_movers)) True) % 41.28/41.60 (Or (Eq (And (environment a_1) (subpopulation a a_1 a_2)) False) % 41.28/41.60 (Eq (greater (cardinality_at_time a a_2) zero) False)) % 41.28/41.60 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 : Iota), % 41.28/41.60 Or (Eq (And (environment a) (subpopulation a_1 a a_2)) False) % 41.28/41.60 (Or (Eq (greater (cardinality_at_time a_1 a_2) zero) False) % 41.28/41.60 (Or (Eq (Eq a_1 efficient_producers) True) (Eq (Eq a_1 first_movers) True))) % 41.28/41.60 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 : Iota), % 41.28/41.60 Or (Eq (greater (cardinality_at_time a a_1) zero) False) % 41.28/41.60 (Or (Eq (Eq a efficient_producers) True) % 41.28/41.60 (Or (Eq (Eq a first_movers) True) (Or (Eq (environment a_2) False) (Eq (subpopulation a a_2 a_1) False)))) % 41.28/41.60 Clause #96 (by clausification #[95]): ∀ (a a_1 a_2 : Iota), % 41.28/41.60 Or (Eq (greater (cardinality_at_time a a_1) zero) False) % 41.28/41.60 (Or (Eq (Eq a first_movers) True) % 41.28/41.60 (Or (Eq (environment a_2) False) (Or (Eq (subpopulation a a_2 a_1) False) (Eq a efficient_producers)))) % 41.28/41.60 Clause #97 (by clausification #[96]): ∀ (a a_1 a_2 : Iota), % 41.28/41.60 Or (Eq (greater (cardinality_at_time a a_1) zero) False) % 41.28/41.60 (Or (Eq (environment a_2) False) % 41.28/41.60 (Or (Eq (subpopulation a a_2 a_1) False) (Or (Eq a efficient_producers) (Eq a first_movers)))) % 41.28/41.60 Clause #98 (by clausification #[9]): ∀ (a : Iota), % 41.28/41.60 Eq % 41.28/41.60 (∀ (T : Iota), % 41.28/41.60 And (And (environment a) (in_environment a T)) (greater (number_of_organizations a T) zero) → % 41.28/41.60 And (greater (equilibrium a) T → decreases (resources a T)) % 41.28/41.60 (Not (greater (equilibrium a) T) → constant (resources a T))) % 41.28/41.60 True % 41.28/41.60 Clause #99 (by clausification #[98]): ∀ (a a_1 : Iota), % 41.28/41.60 Eq % 41.28/41.60 (And (And (environment a) (in_environment a a_1)) (greater (number_of_organizations a a_1) zero) → % 41.28/41.60 And (greater (equilibrium a) a_1 → decreases (resources a a_1)) % 41.28/41.60 (Not (greater (equilibrium a) a_1) → constant (resources a a_1))) % 41.28/41.60 True % 41.28/41.60 Clause #100 (by clausification #[99]): ∀ (a a_1 : Iota), % 41.28/41.60 Or (Eq (And (And (environment a) (in_environment a a_1)) (greater (number_of_organizations a a_1) zero)) False) % 41.28/41.60 (Eq % 41.28/41.60 (And (greater (equilibrium a) a_1 → decreases (resources a a_1)) % 41.28/41.60 (Not (greater (equilibrium a) a_1) → constant (resources a a_1))) % 41.28/41.60 True) % 41.28/41.60 Clause #101 (by clausification #[100]): ∀ (a a_1 : Iota), % 41.28/41.60 Or % 41.28/41.60 (Eq % 41.28/41.60 (And (greater (equilibrium a) a_1 → decreases (resources a a_1)) % 41.28/41.60 (Not (greater (equilibrium a) a_1) → constant (resources a a_1))) % 41.28/41.60 True) % 41.28/41.60 (Or (Eq (And (environment a) (in_environment a a_1)) False) % 41.28/41.60 (Eq (greater (number_of_organizations a a_1) zero) False)) % 41.28/41.60 Clause #102 (by clausification #[101]): ∀ (a a_1 : Iota), % 41.28/41.60 Or (Eq (And (environment a) (in_environment a a_1)) False) % 41.28/41.60 (Or (Eq (greater (number_of_organizations a a_1) zero) False) % 41.28/41.60 (Eq (Not (greater (equilibrium a) a_1) → constant (resources a a_1)) True)) % 41.28/41.60 Clause #103 (by clausification #[101]): ∀ (a a_1 : Iota), % 41.28/41.60 Or (Eq (And (environment a) (in_environment a a_1)) False) % 41.28/41.60 (Or (Eq (greater (number_of_organizations a a_1) zero) False) % 41.28/41.60 (Eq (greater (equilibrium a) a_1 → decreases (resources a a_1)) True)) % 41.28/41.60 Clause #104 (by clausification #[102]): ∀ (a a_1 : Iota), % 41.28/41.60 Or (Eq (greater (number_of_organizations a a_1) zero) False) % 41.28/41.60 (Or (Eq (Not (greater (equilibrium a) a_1) → constant (resources a a_1)) True) % 41.28/41.60 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False))) % 41.28/41.60 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), % 41.38/41.67 Or (Eq (greater (number_of_organizations a a_1) zero) False) % 41.38/41.67 (Or (Eq (environment a) False) % 41.38/41.67 (Or (Eq (in_environment a a_1) False) % 41.38/41.67 (Or (Eq (Not (greater (equilibrium a) a_1)) False) (Eq (constant (resources a a_1)) True)))) % 41.38/41.67 Clause #106 (by clausification #[105]): ∀ (a a_1 : Iota), % 41.38/41.67 Or (Eq (greater (number_of_organizations a a_1) zero) False) % 41.38/41.67 (Or (Eq (environment a) False) % 41.38/41.67 (Or (Eq (in_environment a a_1) False) % 41.38/41.67 (Or (Eq (constant (resources a a_1)) True) (Eq (greater (equilibrium a) a_1) True)))) % 41.38/41.67 Clause #107 (by clausification #[8]): ∀ (a : Iota), % 41.38/41.67 Eq % 41.38/41.67 (∀ (T : Iota), % 41.38/41.67 And (environment a) (in_environment a T) → % 41.38/41.67 Or (greater_or_equal T (appear an_organisation a)) (greater (appear an_organisation a) T)) % 41.38/41.67 True % 41.38/41.67 Clause #108 (by clausification #[107]): ∀ (a a_1 : Iota), % 41.38/41.67 Eq % 41.38/41.67 (And (environment a) (in_environment a a_1) → % 41.38/41.67 Or (greater_or_equal a_1 (appear an_organisation a)) (greater (appear an_organisation a) a_1)) % 41.38/41.67 True % 41.38/41.67 Clause #109 (by clausification #[108]): ∀ (a a_1 : Iota), % 41.38/41.67 Or (Eq (And (environment a) (in_environment a a_1)) False) % 41.38/41.67 (Eq (Or (greater_or_equal a_1 (appear an_organisation a)) (greater (appear an_organisation a) a_1)) True) % 41.38/41.67 Clause #110 (by clausification #[109]): ∀ (a a_1 : Iota), % 41.38/41.67 Or (Eq (Or (greater_or_equal a (appear an_organisation a_1)) (greater (appear an_organisation a_1) a)) True) % 41.38/41.67 (Or (Eq (environment a_1) False) (Eq (in_environment a_1 a) False)) % 41.38/41.67 Clause #111 (by clausification #[110]): ∀ (a a_1 : Iota), % 41.38/41.67 Or (Eq (environment a) False) % 41.38/41.67 (Or (Eq (in_environment a a_1) False) % 41.38/41.67 (Or (Eq (greater_or_equal a_1 (appear an_organisation a)) True) % 41.38/41.67 (Eq (greater (appear an_organisation a) a_1) True))) % 41.38/41.67 Clause #112 (by clausification #[11]): ∀ (a : Iota), % 41.38/41.67 Eq % 41.38/41.67 (∀ (T : Iota), % 41.38/41.67 And (environment a) (in_environment a T) → % 41.38/41.67 And (decreases (resources a T) → Not (decreases (number_of_organizations a T))) % 41.38/41.67 (constant (resources a T) → constant (number_of_organizations a T))) % 41.38/41.67 True % 41.38/41.67 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), % 41.38/41.67 Eq % 41.38/41.67 (And (environment a) (in_environment a a_1) → % 41.38/41.67 And (decreases (resources a a_1) → Not (decreases (number_of_organizations a a_1))) % 41.38/41.67 (constant (resources a a_1) → constant (number_of_organizations a a_1))) % 41.38/41.67 True % 41.38/41.67 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), % 41.38/41.67 Or (Eq (And (environment a) (in_environment a a_1)) False) % 41.38/41.67 (Eq % 41.38/41.67 (And (decreases (resources a a_1) → Not (decreases (number_of_organizations a a_1))) % 41.38/41.67 (constant (resources a a_1) → constant (number_of_organizations a a_1))) % 41.38/41.67 True) % 41.38/41.67 Clause #115 (by clausification #[114]): ∀ (a a_1 : Iota), % 41.38/41.67 Or % 41.38/41.67 (Eq % 41.38/41.67 (And (decreases (resources a a_1) → Not (decreases (number_of_organizations a a_1))) % 41.38/41.67 (constant (resources a a_1) → constant (number_of_organizations a a_1))) % 41.38/41.67 True) % 41.38/41.67 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False)) % 41.38/41.67 Clause #116 (by clausification #[115]): ∀ (a a_1 : Iota), % 41.38/41.67 Or (Eq (environment a) False) % 41.38/41.67 (Or (Eq (in_environment a a_1) False) % 41.38/41.67 (Eq (constant (resources a a_1) → constant (number_of_organizations a a_1)) True)) % 41.38/41.67 Clause #117 (by clausification #[115]): ∀ (a a_1 : Iota), % 41.38/41.67 Or (Eq (environment a) False) % 41.38/41.67 (Or (Eq (in_environment a a_1) False) % 41.38/41.67 (Eq (decreases (resources a a_1) → Not (decreases (number_of_organizations a a_1))) True)) % 41.38/41.67 Clause #118 (by clausification #[116]): ∀ (a a_1 : Iota), % 41.38/41.67 Or (Eq (environment a) False) % 41.38/41.67 (Or (Eq (in_environment a a_1) False) % 41.38/41.67 (Or (Eq (constant (resources a a_1)) False) (Eq (constant (number_of_organizations a a_1)) True))) % 41.38/41.67 Clause #119 (by clausification #[6]): ∀ (a : Iota), % 41.38/41.67 Eq % 41.38/41.67 (∀ (T : Iota), % 41.38/41.67 And (environment a) (in_environment a T) → % 41.38/41.67 Or (Eq (cardinality_at_time efficient_producers T) zero) % 41.38/41.67 (greater (cardinality_at_time efficient_producers T) zero)) % 41.38/41.67 True % 41.38/41.67 Clause #120 (by clausification #[119]): ∀ (a a_1 : Iota), % 41.38/41.67 Eq % 41.38/41.67 (And (environment a) (in_environment a a_1) → % 41.48/41.76 Or (Eq (cardinality_at_time efficient_producers a_1) zero) % 41.48/41.76 (greater (cardinality_at_time efficient_producers a_1) zero)) % 41.48/41.76 True % 41.48/41.76 Clause #121 (by clausification #[120]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq (And (environment a) (in_environment a a_1)) False) % 41.48/41.76 (Eq % 41.48/41.76 (Or (Eq (cardinality_at_time efficient_producers a_1) zero) % 41.48/41.76 (greater (cardinality_at_time efficient_producers a_1) zero)) % 41.48/41.76 True) % 41.48/41.76 Clause #122 (by clausification #[121]): ∀ (a a_1 : Iota), % 41.48/41.76 Or % 41.48/41.76 (Eq % 41.48/41.76 (Or (Eq (cardinality_at_time efficient_producers a) zero) % 41.48/41.76 (greater (cardinality_at_time efficient_producers a) zero)) % 41.48/41.76 True) % 41.48/41.76 (Or (Eq (environment a_1) False) (Eq (in_environment a_1 a) False)) % 41.48/41.76 Clause #123 (by clausification #[122]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq (environment a) False) % 41.48/41.76 (Or (Eq (in_environment a a_1) False) % 41.48/41.76 (Or (Eq (Eq (cardinality_at_time efficient_producers a_1) zero) True) % 41.48/41.76 (Eq (greater (cardinality_at_time efficient_producers a_1) zero) True))) % 41.48/41.76 Clause #124 (by clausification #[123]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq (environment a) False) % 41.48/41.76 (Or (Eq (in_environment a a_1) False) % 41.48/41.76 (Or (Eq (greater (cardinality_at_time efficient_producers a_1) zero) True) % 41.48/41.76 (Eq (cardinality_at_time efficient_producers a_1) zero))) % 41.48/41.76 Clause #125 (by clausification #[117]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq (environment a) False) % 41.48/41.76 (Or (Eq (in_environment a a_1) False) % 41.48/41.76 (Or (Eq (decreases (resources a a_1)) False) (Eq (Not (decreases (number_of_organizations a a_1))) True))) % 41.48/41.76 Clause #126 (by clausification #[125]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq (environment a) False) % 41.48/41.76 (Or (Eq (in_environment a a_1) False) % 41.48/41.76 (Or (Eq (decreases (resources a a_1)) False) (Eq (decreases (number_of_organizations a a_1)) False))) % 41.48/41.76 Clause #127 (by clausification #[103]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq (greater (number_of_organizations a a_1) zero) False) % 41.48/41.76 (Or (Eq (greater (equilibrium a) a_1 → decreases (resources a a_1)) True) % 41.48/41.76 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False))) % 41.48/41.76 Clause #128 (by clausification #[127]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq (greater (number_of_organizations a a_1) zero) False) % 41.48/41.76 (Or (Eq (environment a) False) % 41.48/41.76 (Or (Eq (in_environment a a_1) False) % 41.48/41.76 (Or (Eq (greater (equilibrium a) a_1) False) (Eq (decreases (resources a a_1)) True)))) % 41.48/41.76 Clause #129 (by clausification #[72]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq (greater zero (growth_rate efficient_producers a)) False) % 41.48/41.76 (Or (Eq (environment a_1) False) % 41.48/41.76 (Or (Eq (in_environment a_1 a) False) (Eq (greater zero (growth_rate first_movers a)) True))) % 41.48/41.76 Clause #130 (by clausification #[52]): ∀ (a a_1 : Iota), Eq (in_environment (skS.0 1 a) (skS.0 2 a a_1)) True % 41.48/41.76 Clause #131 (by clausification #[52]): ∀ (a : Iota), Eq (environment (skS.0 1 a)) True % 41.48/41.76 Clause #132 (by superposition #[131, 42]): ∀ (a a_1 a_2 : Iota), % 41.48/41.76 Or (Eq True False) % 41.48/41.76 (Or (Eq (greater_or_equal a (appear efficient_producers (skS.0 1 a_1))) False) % 41.48/41.76 (Or (Ne (cardinality_at_time efficient_producers a) zero) % 41.48/41.76 (Eq (greater zero (growth_rate efficient_producers (skS.0 0 (skS.0 1 a_1) a a_2))) True))) % 41.48/41.76 Clause #134 (by superposition #[131, 78]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq True False) % 41.48/41.76 (Or (Eq (in_environment (skS.0 1 a) a_1) False) (Eq (subpopulation first_movers (skS.0 1 a) a_1) True)) % 41.48/41.76 Clause #135 (by superposition #[131, 88]): ∀ (a a_1 a_2 : Iota), % 41.48/41.76 Or (Eq True False) % 41.48/41.76 (Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.48/41.76 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) a_1)) True) % 41.48/41.76 (Eq (greater zero (growth_rate (skS.0 3 (skS.0 1 a) a_1 a_2) a_1)) False))) % 41.48/41.76 Clause #136 (by superposition #[131, 111]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq True False) % 41.48/41.76 (Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.48/41.76 (Or (Eq (greater_or_equal a_1 (appear an_organisation (skS.0 1 a))) True) % 41.48/41.76 (Eq (greater (appear an_organisation (skS.0 1 a)) a_1) True))) % 41.48/41.76 Clause #137 (by superposition #[131, 118]): ∀ (a a_1 : Iota), % 41.48/41.76 Or (Eq True False) % 41.48/41.76 (Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.48/41.76 (Or (Eq (constant (resources (skS.0 1 a) a_1)) False) % 41.58/41.84 (Eq (constant (number_of_organizations (skS.0 1 a) a_1)) True))) % 41.58/41.84 Clause #138 (by superposition #[131, 124]): ∀ (a a_1 : Iota), % 41.58/41.84 Or (Eq True False) % 41.58/41.84 (Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.58/41.84 (Or (Eq (greater (cardinality_at_time efficient_producers a_1) zero) True) % 41.58/41.84 (Eq (cardinality_at_time efficient_producers a_1) zero))) % 41.58/41.84 Clause #139 (by superposition #[131, 126]): ∀ (a a_1 : Iota), % 41.58/41.84 Or (Eq True False) % 41.58/41.84 (Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.58/41.84 (Or (Eq (decreases (resources (skS.0 1 a) a_1)) False) % 41.58/41.84 (Eq (decreases (number_of_organizations (skS.0 1 a) a_1)) False))) % 41.58/41.84 Clause #141 (by clausification #[43]): ∀ (a a_1 a_2 : Iota), % 41.58/41.84 Or (Eq (environment a) False) % 41.58/41.84 (Or (Eq (greater_or_equal a_1 (appear efficient_producers a)) False) % 41.58/41.84 (Or (Ne (cardinality_at_time efficient_producers a_1) zero) % 41.58/41.84 (Eq (And (greater (skS.0 0 a a_1 a_2) (appear efficient_producers a)) (in_environment a (skS.0 0 a a_1 a_2))) % 41.58/41.84 True))) % 41.58/41.84 Clause #143 (by clausification #[134]): ∀ (a a_1 : Iota), Or (Eq (in_environment (skS.0 1 a) a_1) False) (Eq (subpopulation first_movers (skS.0 1 a) a_1) True) % 41.58/41.84 Clause #151 (by clausification #[138]): ∀ (a a_1 : Iota), % 41.58/41.84 Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.58/41.84 (Or (Eq (greater (cardinality_at_time efficient_producers a_1) zero) True) % 41.58/41.84 (Eq (cardinality_at_time efficient_producers a_1) zero)) % 41.58/41.84 Clause #152 (by superposition #[151, 130]): ∀ (a a_1 : Iota), % 41.58/41.84 Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) True) % 41.58/41.84 (Or (Eq (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) (Eq False True)) % 41.58/41.84 Clause #153 (by clausification #[87]): ∀ (a a_1 a_2 : Iota), % 41.58/41.84 Or (Eq (environment a) False) % 41.58/41.84 (Or (Eq (in_environment a a_1) False) % 41.58/41.84 (Or (Eq (decreases (number_of_organizations a a_1)) True) % 41.58/41.84 (Eq (greater (cardinality_at_time (skS.0 3 a a_1 a_2) a_1) zero) True))) % 41.58/41.84 Clause #154 (by clausification #[87]): ∀ (a a_1 a_2 : Iota), % 41.58/41.84 Or (Eq (environment a) False) % 41.58/41.84 (Or (Eq (in_environment a a_1) False) % 41.58/41.84 (Or (Eq (decreases (number_of_organizations a a_1)) True) (Eq (subpopulation (skS.0 3 a a_1 a_2) a a_1) True))) % 41.58/41.84 Clause #155 (by superposition #[153, 131]): ∀ (a a_1 a_2 : Iota), % 41.58/41.84 Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.58/41.84 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) a_1)) True) % 41.58/41.84 (Or (Eq (greater (cardinality_at_time (skS.0 3 (skS.0 1 a) a_1 a_2) a_1) zero) True) (Eq False True))) % 41.58/41.84 Clause #156 (by superposition #[154, 131]): ∀ (a a_1 a_2 : Iota), % 41.58/41.84 Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.58/41.84 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) a_1)) True) % 41.58/41.84 (Or (Eq (subpopulation (skS.0 3 (skS.0 1 a) a_1 a_2) (skS.0 1 a) a_1) True) (Eq False True))) % 41.58/41.84 Clause #157 (by clausification #[152]): ∀ (a a_1 : Iota), % 41.58/41.84 Or (Eq (greater (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) True) % 41.58/41.84 (Eq (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) % 41.58/41.84 Clause #158 (by superposition #[157, 50]): ∀ (a a_1 : Iota), Or (Eq (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) (Eq True False) % 41.58/41.84 Clause #159 (by clausification #[158]): ∀ (a a_1 : Iota), Eq (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero % 41.58/41.84 Clause #164 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), % 41.58/41.84 Or (Eq (greater_or_equal a (appear efficient_producers (skS.0 1 a_1))) False) % 41.58/41.84 (Or (Ne (cardinality_at_time efficient_producers a) zero) % 41.58/41.84 (Eq (greater zero (growth_rate efficient_producers (skS.0 0 (skS.0 1 a_1) a a_2))) True)) % 41.58/41.84 Clause #165 (by superposition #[164, 51]): ∀ (a a_1 a_2 : Iota), % 41.58/41.84 Or (Ne (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) % 41.58/41.84 (Or (Eq (greater zero (growth_rate efficient_producers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.58/41.84 (Eq False True)) % 41.58/41.84 Clause #167 (by clausification #[139]): ∀ (a a_1 : Iota), % 41.58/41.84 Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.58/41.84 (Or (Eq (decreases (resources (skS.0 1 a) a_1)) False) % 41.58/41.84 (Eq (decreases (number_of_organizations (skS.0 1 a) a_1)) False)) % 41.68/41.94 Clause #169 (by clausification #[137]): ∀ (a a_1 : Iota), % 41.68/41.94 Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.68/41.94 (Or (Eq (constant (resources (skS.0 1 a) a_1)) False) % 41.68/41.94 (Eq (constant (number_of_organizations (skS.0 1 a) a_1)) True)) % 41.68/41.94 Clause #171 (by clausification #[136]): ∀ (a a_1 : Iota), % 41.68/41.94 Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.68/41.94 (Or (Eq (greater_or_equal a_1 (appear an_organisation (skS.0 1 a))) True) % 41.68/41.94 (Eq (greater (appear an_organisation (skS.0 1 a)) a_1) True)) % 41.68/41.94 Clause #175 (by clausification #[135]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.68/41.94 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) a_1)) True) % 41.68/41.94 (Eq (greater zero (growth_rate (skS.0 3 (skS.0 1 a) a_1 a_2) a_1)) False)) % 41.68/41.94 Clause #181 (by clausification #[165]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Ne (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) % 41.68/41.94 (Eq (greater zero (growth_rate efficient_producers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.68/41.94 Clause #182 (by forward demodulation #[181, 159]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Ne zero zero) (Eq (greater zero (growth_rate efficient_producers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.68/41.94 Clause #183 (by eliminate resolved literals #[182]): ∀ (a a_1 a_2 : Iota), Eq (greater zero (growth_rate efficient_producers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True % 41.68/41.94 Clause #184 (by superposition #[183, 129]): ∀ (a a_1 a_2 a_3 : Iota), % 41.68/41.94 Or (Eq True False) % 41.68/41.94 (Or (Eq (environment a) False) % 41.68/41.94 (Or (Eq (in_environment a (skS.0 0 (skS.0 1 a_1) (skS.0 2 a_1 a_2) a_3)) False) % 41.68/41.94 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 1 a_1) (skS.0 2 a_1 a_2) a_3))) True))) % 41.68/41.94 Clause #185 (by clausification #[141]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Eq (environment a) False) % 41.68/41.94 (Or (Eq (greater_or_equal a_1 (appear efficient_producers a)) False) % 41.68/41.94 (Or (Ne (cardinality_at_time efficient_producers a_1) zero) (Eq (in_environment a (skS.0 0 a a_1 a_2)) True))) % 41.68/41.94 Clause #187 (by superposition #[185, 131]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Eq (greater_or_equal a (appear efficient_producers (skS.0 1 a_1))) False) % 41.68/41.94 (Or (Ne (cardinality_at_time efficient_producers a) zero) % 41.68/41.94 (Or (Eq (in_environment (skS.0 1 a_1) (skS.0 0 (skS.0 1 a_1) a a_2)) True) (Eq False True))) % 41.68/41.94 Clause #194 (by clausification #[187]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Eq (greater_or_equal a (appear efficient_producers (skS.0 1 a_1))) False) % 41.68/41.94 (Or (Ne (cardinality_at_time efficient_producers a) zero) % 41.68/41.94 (Eq (in_environment (skS.0 1 a_1) (skS.0 0 (skS.0 1 a_1) a a_2)) True)) % 41.68/41.94 Clause #195 (by superposition #[194, 51]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Ne (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) % 41.68/41.94 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) (Eq False True)) % 41.68/41.94 Clause #196 (by clausification #[155]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.68/41.94 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) a_1)) True) % 41.68/41.94 (Eq (greater (cardinality_at_time (skS.0 3 (skS.0 1 a) a_1 a_2) a_1) zero) True)) % 41.68/41.94 Clause #200 (by clausification #[195]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Ne (cardinality_at_time efficient_producers (skS.0 2 a a_1)) zero) % 41.68/41.94 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.68/41.94 Clause #201 (by forward demodulation #[200, 159]): ∀ (a a_1 a_2 : Iota), Or (Ne zero zero) (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.68/41.94 Clause #202 (by eliminate resolved literals #[201]): ∀ (a a_1 a_2 : Iota), Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True % 41.68/41.94 Clause #203 (by superposition #[202, 143]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Eq True False) (Eq (subpopulation first_movers (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.68/41.94 Clause #206 (by superposition #[202, 167]): ∀ (a a_1 a_2 : Iota), % 41.68/41.94 Or (Eq True False) % 41.68/41.94 (Or (Eq (decreases (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False) % 41.68/41.94 (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False)) % 41.68/42.04 Clause #207 (by superposition #[202, 169]): ∀ (a a_1 a_2 : Iota), % 41.68/42.04 Or (Eq True False) % 41.68/42.04 (Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False) % 41.68/42.04 (Eq (constant (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True)) % 41.68/42.04 Clause #208 (by superposition #[202, 171]): ∀ (a a_1 a_2 : Iota), % 41.68/42.04 Or (Eq True False) % 41.68/42.04 (Or (Eq (greater_or_equal (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) (appear an_organisation (skS.0 1 a))) True) % 41.68/42.04 (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True)) % 41.68/42.04 Clause #209 (by superposition #[202, 175]): ∀ (a a_1 a_2 a_3 : Iota), % 41.68/42.04 Or (Eq True False) % 41.68/42.04 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.68/42.04 (Eq % 41.68/42.04 (greater zero % 41.68/42.04 (growth_rate (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) % 41.68/42.04 (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) % 41.68/42.04 False)) % 41.68/42.04 Clause #210 (by superposition #[202, 196]): ∀ (a a_1 a_2 a_3 : Iota), % 41.68/42.04 Or (Eq True False) % 41.68/42.04 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.68/42.04 (Eq % 41.68/42.04 (greater % 41.68/42.04 (cardinality_at_time (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) % 41.68/42.04 (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) % 41.68/42.04 zero) % 41.68/42.04 True)) % 41.68/42.04 Clause #215 (by clausification #[203]): ∀ (a a_1 a_2 : Iota), Eq (subpopulation first_movers (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True % 41.68/42.04 Clause #216 (by superposition #[215, 61]): ∀ (a a_1 a_2 : Iota), % 41.68/42.04 Or (Eq True False) % 41.68/42.04 (Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 41.68/42.04 (Or (Eq (environment (skS.0 1 a)) False) % 41.68/42.04 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 41.68/42.04 (Ne (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero)))) % 41.68/42.05 Clause #217 (by clausification #[156]): ∀ (a a_1 a_2 : Iota), % 41.68/42.05 Or (Eq (in_environment (skS.0 1 a) a_1) False) % 41.68/42.05 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) a_1)) True) % 41.68/42.05 (Eq (subpopulation (skS.0 3 (skS.0 1 a) a_1 a_2) (skS.0 1 a) a_1) True)) % 41.68/42.05 Clause #219 (by superposition #[217, 202]): ∀ (a a_1 a_2 a_3 : Iota), % 41.68/42.05 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.68/42.05 (Or % 41.68/42.05 (Eq % 41.68/42.05 (subpopulation (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) (skS.0 1 a) % 41.68/42.05 (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) % 41.68/42.05 True) % 41.68/42.05 (Eq False True)) % 41.68/42.05 Clause #232 (by clausification #[184]): ∀ (a a_1 a_2 a_3 : Iota), % 41.68/42.05 Or (Eq (environment a) False) % 41.68/42.05 (Or (Eq (in_environment a (skS.0 0 (skS.0 1 a_1) (skS.0 2 a_1 a_2) a_3)) False) % 41.68/42.05 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 1 a_1) (skS.0 2 a_1 a_2) a_3))) True)) % 41.68/42.05 Clause #233 (by superposition #[232, 131]): ∀ (a a_1 a_2 a_3 : Iota), % 41.68/42.05 Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a_1) (skS.0 2 a_1 a_2) a_3)) False) % 41.68/42.05 (Or (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 1 a_1) (skS.0 2 a_1 a_2) a_3))) True) % 41.68/42.05 (Eq False True)) % 41.68/42.05 Clause #234 (by clausification #[233]): ∀ (a a_1 a_2 a_3 : Iota), % 41.68/42.05 Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a_1) (skS.0 2 a_1 a_2) a_3)) False) % 41.68/42.05 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 1 a_1) (skS.0 2 a_1 a_2) a_3))) True) % 41.68/42.05 Clause #235 (by superposition #[234, 202]): ∀ (a a_1 a_2 : Iota), % 41.68/42.05 Or (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) (Eq False True) % 41.68/42.05 Clause #243 (by clausification #[235]): ∀ (a a_1 a_2 : Iota), Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True % 41.68/42.05 Clause #245 (by clausification #[207]): ∀ (a a_1 a_2 : Iota), % 41.68/42.05 Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False) % 41.68/42.05 (Eq (constant (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.93/42.16 Clause #246 (by clausification #[206]): ∀ (a a_1 a_2 : Iota), % 41.93/42.16 Or (Eq (decreases (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False) % 41.93/42.16 (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False) % 41.93/42.16 Clause #247 (by clausification #[208]): ∀ (a a_1 a_2 : Iota), % 41.93/42.16 Or (Eq (greater_or_equal (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) (appear an_organisation (skS.0 1 a))) True) % 41.93/42.16 (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.93/42.16 Clause #248 (by superposition #[247, 23]): ∀ (a a_1 a_2 : Iota), % 41.93/42.16 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.93/42.16 (Or (Eq (greater (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) True) % 41.93/42.16 (Or (Eq True False) % 41.93/42.16 (Or (Eq (environment (skS.0 1 a)) False) % 41.93/42.16 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False)))) % 41.93/42.16 Clause #249 (by clausification #[209]): ∀ (a a_1 a_2 a_3 : Iota), % 41.93/42.16 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.93/42.16 (Eq % 41.93/42.16 (greater zero % 41.93/42.16 (growth_rate (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) % 41.93/42.16 (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) % 41.93/42.16 False) % 41.93/42.16 Clause #271 (by clausification #[210]): ∀ (a a_1 a_2 a_3 : Iota), % 41.93/42.16 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.93/42.16 (Eq % 41.93/42.16 (greater % 41.93/42.16 (cardinality_at_time (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) % 41.93/42.16 (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) % 41.93/42.16 zero) % 41.93/42.16 True) % 41.93/42.16 Clause #272 (by superposition #[271, 97]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 41.93/42.16 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.93/42.16 (Or (Eq True False) % 41.93/42.16 (Or (Eq (environment a_3) False) % 41.93/42.16 (Or % 41.93/42.16 (Eq % 41.93/42.16 (subpopulation (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_4) a_3 % 41.93/42.16 (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) % 41.93/42.16 False) % 41.93/42.16 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_4) efficient_producers) % 41.93/42.16 (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_4) first_movers))))) % 41.93/42.16 Clause #284 (by clausification #[216]): ∀ (a a_1 a_2 : Iota), % 41.93/42.16 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 41.93/42.16 (Or (Eq (environment (skS.0 1 a)) False) % 41.93/42.16 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 41.93/42.16 (Ne (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero))) % 41.93/42.16 Clause #285 (by forward demodulation #[284, 131]): ∀ (a a_1 a_2 : Iota), % 41.93/42.16 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 41.93/42.16 (Or (Eq True False) % 41.93/42.16 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 41.93/42.16 (Ne (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero))) % 41.93/42.16 Clause #286 (by clausification #[285]): ∀ (a a_1 a_2 : Iota), % 41.93/42.16 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 41.93/42.16 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 41.93/42.16 (Ne (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero)) % 41.93/42.16 Clause #287 (by forward demodulation #[286, 202]): ∀ (a a_1 a_2 : Iota), % 41.93/42.16 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 41.93/42.16 (Or (Eq True False) (Ne (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero)) % 41.93/42.16 Clause #288 (by clausification #[287]): ∀ (a a_1 a_2 : Iota), % 41.93/42.16 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 41.93/42.16 (Ne (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 41.93/42.16 Clause #289 (by clausification #[219]): ∀ (a a_1 a_2 a_3 : Iota), % 41.98/42.27 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.98/42.27 (Eq % 41.98/42.27 (subpopulation (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) (skS.0 1 a) % 41.98/42.27 (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) % 41.98/42.27 True) % 41.98/42.27 Clause #310 (by clausification #[248]): ∀ (a a_1 a_2 : Iota), % 41.98/42.27 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.98/42.27 (Or (Eq (greater (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) True) % 41.98/42.27 (Or (Eq (environment (skS.0 1 a)) False) % 41.98/42.27 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False))) % 41.98/42.27 Clause #311 (by forward demodulation #[310, 131]): ∀ (a a_1 a_2 : Iota), % 41.98/42.27 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.98/42.27 (Or (Eq (greater (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) True) % 41.98/42.27 (Or (Eq True False) (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False))) % 41.98/42.27 Clause #312 (by clausification #[311]): ∀ (a a_1 a_2 : Iota), % 41.98/42.27 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.98/42.27 (Or (Eq (greater (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) True) % 41.98/42.27 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False)) % 41.98/42.27 Clause #313 (by forward demodulation #[312, 202]): ∀ (a a_1 a_2 : Iota), % 41.98/42.27 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.98/42.27 (Or (Eq (greater (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) True) % 41.98/42.27 (Eq True False)) % 41.98/42.27 Clause #314 (by clausification #[313]): ∀ (a a_1 a_2 : Iota), % 41.98/42.27 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.98/42.27 (Eq (greater (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) True) % 41.98/42.27 Clause #315 (by superposition #[314, 106]): ∀ (a a_1 a_2 : Iota), % 41.98/42.27 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.98/42.27 (Or (Eq True False) % 41.98/42.27 (Or (Eq (environment (skS.0 1 a)) False) % 41.98/42.27 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 41.98/42.27 (Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.98/42.27 (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True))))) % 41.98/42.27 Clause #316 (by superposition #[314, 128]): ∀ (a a_1 a_2 : Iota), % 41.98/42.27 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 41.98/42.27 (Or (Eq True False) % 41.98/42.27 (Or (Eq (environment (skS.0 1 a)) False) % 41.98/42.27 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 41.98/42.27 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 41.98/42.27 (Eq (decreases (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True))))) % 41.98/42.27 Clause #333 (by clausification #[272]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 41.98/42.27 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.98/42.27 (Or (Eq (environment a_3) False) % 41.98/42.27 (Or % 41.98/42.27 (Eq % 41.98/42.27 (subpopulation (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_4) a_3 % 41.98/42.27 (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) % 41.98/42.27 False) % 41.98/42.27 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_4) efficient_producers) % 41.98/42.27 (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_4) first_movers)))) % 41.98/42.27 Clause #334 (by superposition #[333, 131]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 41.98/42.27 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 41.98/42.27 (Or % 41.98/42.27 (Eq % 41.98/42.27 (subpopulation (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) (skS.0 1 a_4) % 42.08/42.38 (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) % 42.08/42.38 False) % 42.08/42.38 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) efficient_producers) % 42.08/42.38 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) first_movers) (Eq False True)))) % 42.08/42.38 Clause #370 (by clausification #[315]): ∀ (a a_1 a_2 : Iota), % 42.08/42.38 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.08/42.38 (Or (Eq (environment (skS.0 1 a)) False) % 42.08/42.38 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.08/42.38 (Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.08/42.38 (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True)))) % 42.08/42.38 Clause #371 (by forward demodulation #[370, 131]): ∀ (a a_1 a_2 : Iota), % 42.08/42.38 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.08/42.38 (Or (Eq True False) % 42.08/42.39 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.08/42.39 (Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.08/42.39 (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True)))) % 42.08/42.39 Clause #372 (by clausification #[371]): ∀ (a a_1 a_2 : Iota), % 42.08/42.39 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.08/42.39 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.08/42.39 (Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.08/42.39 (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True))) % 42.08/42.39 Clause #373 (by forward demodulation #[372, 202]): ∀ (a a_1 a_2 : Iota), % 42.08/42.39 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.08/42.39 (Or (Eq True False) % 42.08/42.39 (Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.08/42.39 (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True))) % 42.08/42.39 Clause #374 (by clausification #[373]): ∀ (a a_1 a_2 : Iota), % 42.08/42.39 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.08/42.39 (Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.08/42.39 (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True)) % 42.08/42.39 Clause #375 (by superposition #[374, 29]): ∀ (a a_1 a_2 : Iota), % 42.08/42.39 Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.08/42.39 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.08/42.39 (Or (Eq True False) % 42.08/42.39 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.08/42.39 (Or (Eq (environment (skS.0 1 a)) False) % 42.08/42.39 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False))))) % 42.08/42.39 Clause #384 (by clausification #[316]): ∀ (a a_1 a_2 : Iota), % 42.08/42.39 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.08/42.39 (Or (Eq (environment (skS.0 1 a)) False) % 42.08/42.39 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.08/42.39 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.08/42.39 (Eq (decreases (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True)))) % 42.08/42.39 Clause #385 (by forward demodulation #[384, 131]): ∀ (a a_1 a_2 : Iota), % 42.08/42.39 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.08/42.39 (Or (Eq True False) % 42.08/42.39 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.08/42.39 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.08/42.39 (Eq (decreases (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True)))) % 42.08/42.39 Clause #386 (by clausification #[385]): ∀ (a a_1 a_2 : Iota), % 42.18/42.49 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.18/42.49 (Or (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.18/42.49 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.18/42.49 (Eq (decreases (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True))) % 42.18/42.49 Clause #387 (by forward demodulation #[386, 202]): ∀ (a a_1 a_2 : Iota), % 42.18/42.49 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.18/42.49 (Or (Eq True False) % 42.18/42.49 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.18/42.49 (Eq (decreases (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True))) % 42.18/42.49 Clause #388 (by clausification #[387]): ∀ (a a_1 a_2 : Iota), % 42.18/42.49 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.18/42.49 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.18/42.49 (Eq (decreases (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True)) % 42.18/42.49 Clause #408 (by clausification #[375]): ∀ (a a_1 a_2 : Iota), % 42.18/42.49 Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.18/42.49 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.18/42.49 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.18/42.49 (Or (Eq (environment (skS.0 1 a)) False) % 42.18/42.49 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False)))) % 42.18/42.49 Clause #409 (by forward demodulation #[408, 131]): ∀ (a a_1 a_2 : Iota), % 42.18/42.49 Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.18/42.49 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.18/42.49 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.18/42.49 (Or (Eq True False) (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False)))) % 42.18/42.49 Clause #410 (by clausification #[409]): ∀ (a a_1 a_2 : Iota), % 42.18/42.49 Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.18/42.49 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.18/42.49 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.18/42.49 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False))) % 42.18/42.49 Clause #411 (by forward demodulation #[410, 202]): ∀ (a a_1 a_2 : Iota), % 42.18/42.49 Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.18/42.49 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.18/42.49 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) (Eq True False))) % 42.18/42.49 Clause #412 (by clausification #[411]): ∀ (a a_1 a_2 : Iota), % 42.18/42.49 Or (Eq (constant (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.18/42.49 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.18/42.49 (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero)) % 42.18/42.49 Clause #413 (by superposition #[412, 245]): ∀ (a a_1 a_2 : Iota), % 42.18/42.49 Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.18/42.49 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.18/42.49 (Or (Eq True False) % 42.18/42.49 (Eq (constant (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True))) % 42.18/42.49 Clause #416 (by clausification #[334]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 42.18/42.49 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.18/42.49 (Or % 42.18/42.49 (Eq % 42.18/42.49 (subpopulation (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) (skS.0 1 a_4) % 42.18/42.49 (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) % 42.18/42.49 False) % 42.38/42.60 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) efficient_producers) % 42.38/42.60 (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) first_movers))) % 42.38/42.60 Clause #417 (by superposition #[416, 289]): ∀ (a a_1 a_2 a_3 : Iota), % 42.38/42.60 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.38/42.60 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) efficient_producers) % 42.38/42.60 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) first_movers) % 42.38/42.60 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.38/42.60 (Eq False True)))) % 42.38/42.60 Clause #418 (by clausification #[413]): ∀ (a a_1 a_2 : Iota), % 42.38/42.60 Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.38/42.60 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.38/42.60 (Eq (constant (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True)) % 42.38/42.60 Clause #419 (by superposition #[418, 18]): ∀ (a a_1 a_2 : Iota), % 42.38/42.60 Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.38/42.60 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.38/42.60 (Or (Eq True False) % 42.38/42.60 (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False))) % 42.38/42.60 Clause #420 (by clausification #[419]): ∀ (a a_1 a_2 : Iota), % 42.38/42.60 Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.38/42.60 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.38/42.60 (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False)) % 42.38/42.60 Clause #421 (by clausification #[417]): ∀ (a a_1 a_2 a_3 : Iota), % 42.38/42.60 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.38/42.60 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) efficient_producers) % 42.38/42.60 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) first_movers) % 42.38/42.60 (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True))) % 42.38/42.60 Clause #422 (by eliminate duplicate literals #[421]): ∀ (a a_1 a_2 a_3 : Iota), % 42.38/42.60 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.38/42.60 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) efficient_producers) % 42.38/42.60 (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) first_movers)) % 42.38/42.60 Clause #423 (by superposition #[422, 249]): ∀ (a a_1 a_2 a_3 : Iota), % 42.38/42.60 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.38/42.60 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) efficient_producers) % 42.38/42.60 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.38/42.60 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False))) % 42.38/42.60 Clause #431 (by eliminate duplicate literals #[423]): ∀ (a a_1 a_2 a_3 : Iota), % 42.38/42.60 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.38/42.60 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) efficient_producers) % 42.38/42.60 (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False)) % 42.38/42.60 Clause #432 (by forward demodulation #[431, 243]): ∀ (a a_1 a_2 a_3 : Iota), % 42.38/42.60 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.38/42.60 (Or (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) efficient_producers) (Eq True False)) % 42.38/42.60 Clause #433 (by clausification #[432]): ∀ (a a_1 a_2 a_3 : Iota), % 42.38/42.60 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.38/42.60 (Eq (skS.0 3 (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2) a_3) efficient_producers) % 42.48/42.71 Clause #434 (by superposition #[433, 249]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.48/42.71 (Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.48/42.71 (Eq (greater zero (growth_rate efficient_producers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False)) % 42.48/42.71 Clause #439 (by eliminate duplicate literals #[434]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.48/42.71 (Eq (greater zero (growth_rate efficient_producers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False) % 42.48/42.71 Clause #440 (by forward demodulation #[439, 183]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True) % 42.48/42.71 (Eq True False) % 42.48/42.71 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Eq (decreases (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) True % 42.48/42.71 Clause #442 (by backward demodulation #[441, 246]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (decreases (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False) (Eq True False) % 42.48/42.71 Clause #448 (by superposition #[441, 420]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.48/42.71 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) (Eq True False)) % 42.48/42.71 Clause #449 (by clausification #[442]): ∀ (a a_1 a_2 : Iota), Eq (decreases (resources (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False % 42.48/42.71 Clause #450 (by backward demodulation #[449, 388]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.48/42.71 (Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) (Eq False True)) % 42.48/42.71 Clause #451 (by clausification #[448]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.48/42.71 (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.71 Clause #453 (by superposition #[451, 288]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.48/42.71 (Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) (Ne zero zero)) % 42.48/42.71 Clause #461 (by eliminate resolved literals #[453]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.48/42.71 (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.71 Clause #465 (by clausification #[450]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.48/42.71 (Eq (greater (equilibrium (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False) % 42.48/42.71 Clause #468 (by superposition #[465, 461]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.48/42.71 (Or (Eq False True) (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero)) % 42.48/42.71 Clause #471 (by clausification #[468]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (greater (appear an_organisation (skS.0 1 a)) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) True) % 42.48/42.71 (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.71 Clause #472 (by superposition #[471, 29]): ∀ (a a_1 a_2 : Iota), % 42.48/42.71 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.71 (Or (Eq True False) % 42.48/42.71 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.71 (Or (Eq (environment (skS.0 1 a)) False) % 42.48/42.71 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False)))) % 42.48/42.71 Clause #505 (by clausification #[472]): ∀ (a a_1 a_2 : Iota), % 42.48/42.76 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.76 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.76 (Or (Eq (environment (skS.0 1 a)) False) % 42.48/42.76 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False))) % 42.48/42.76 Clause #506 (by forward demodulation #[505, 131]): ∀ (a a_1 a_2 : Iota), % 42.48/42.76 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.76 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.76 (Or (Eq True False) (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False))) % 42.48/42.76 Clause #507 (by clausification #[506]): ∀ (a a_1 a_2 : Iota), % 42.48/42.76 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.76 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.76 (Eq (in_environment (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) False)) % 42.48/42.76 Clause #508 (by forward demodulation #[507, 202]): ∀ (a a_1 a_2 : Iota), % 42.48/42.76 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.76 (Or (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) (Eq True False)) % 42.48/42.76 Clause #509 (by clausification #[508]): ∀ (a a_1 a_2 : Iota), % 42.48/42.76 Or (Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.76 (Eq (number_of_organizations (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero) % 42.48/42.76 Clause #510 (by forward contextual literal cutting #[509, 288]): ∀ (a a_1 a_2 : Iota), Eq (cardinality_at_time first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2)) zero % 42.48/42.76 Clause #514 (by superposition #[510, 34]): ∀ (a a_1 a_2 : Iota), % 42.48/42.76 Or (Ne zero zero) (Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False) % 42.48/42.76 Clause #515 (by eliminate resolved literals #[514]): ∀ (a a_1 a_2 : Iota), Eq (greater zero (growth_rate first_movers (skS.0 0 (skS.0 1 a) (skS.0 2 a a_1) a_2))) False % 42.48/42.76 Clause #516 (by superposition #[515, 243]): Eq False True % 42.48/42.76 Clause #517 (by clausification #[516]): False % 42.48/42.76 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------