%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT032+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:06:17 AM UTC 2026 % Result : Theorem 9.06s 9.36s % Output : Proof 9.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT032+2 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.05 % Command : duper %s % 0.12/0.38 % Computer : n014.cluster.edu % 0.12/0.38 % Model : x86_64 x86_64 % 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.38 % Memory : 8046.5625MB % 0.12/0.38 % OS : Linux 6.8.0-71-generic % 0.12/0.38 % CPULimit : 300 % 0.12/0.38 % WCLimit : 300 % 0.12/0.38 % DateTime : Mon Sep 7 12:22:26 UTC 2026 % 0.12/0.38 % CPUTime : % 9.06/9.36 SZS status Theorem for theBenchmark.p % 9.06/9.36 SZS output start Proof for theBenchmark.p % 9.06/9.36 Clause #0 (by assumption #[]): Eq % 9.06/9.36 (∀ (E S1 S2 T : Iota), % 9.06/9.36 And (And (environment E) (subpopulations S1 S2 E T)) (greater (growth_rate S2 T) (growth_rate S1 T)) → % 9.06/9.36 selection_favors S2 S1 T) % 9.06/9.36 True % 9.06/9.36 Clause #1 (by assumption #[]): Eq % 9.06/9.36 (∀ (E : Iota), % 9.06/9.36 And (environment E) (stable E) → % 9.06/9.36 Exists fun To => % 9.06/9.36 And (in_environment E To) % 9.06/9.36 (∀ (T : Iota), % 9.06/9.36 And (subpopulations first_movers efficient_producers E T) (greater_or_equal T To) → % 9.06/9.36 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 9.06/9.36 True % 9.06/9.36 Clause #2 (by assumption #[]): Eq % 9.06/9.36 (Not % 9.06/9.36 (∀ (E : Iota), % 9.06/9.36 And (environment E) (stable E) → % 9.06/9.36 Exists fun To => % 9.06/9.36 And (in_environment E To) % 9.06/9.36 (∀ (T : Iota), % 9.06/9.36 And (subpopulations first_movers efficient_producers E T) (greater_or_equal T To) → % 9.06/9.36 selection_favors efficient_producers first_movers T))) % 9.06/9.36 True % 9.06/9.36 Clause #3 (by clausification #[0]): ∀ (a : Iota), % 9.06/9.36 Eq % 9.06/9.36 (∀ (S1 S2 T : Iota), % 9.06/9.36 And (And (environment a) (subpopulations S1 S2 a T)) (greater (growth_rate S2 T) (growth_rate S1 T)) → % 9.06/9.36 selection_favors S2 S1 T) % 9.06/9.36 True % 9.06/9.36 Clause #4 (by clausification #[3]): ∀ (a a_1 : Iota), % 9.06/9.36 Eq % 9.06/9.36 (∀ (S2 T : Iota), % 9.06/9.36 And (And (environment a) (subpopulations a_1 S2 a T)) (greater (growth_rate S2 T) (growth_rate a_1 T)) → % 9.06/9.36 selection_favors S2 a_1 T) % 9.06/9.36 True % 9.06/9.36 Clause #5 (by clausification #[4]): ∀ (a a_1 a_2 : Iota), % 9.06/9.36 Eq % 9.06/9.36 (∀ (T : Iota), % 9.06/9.36 And (And (environment a) (subpopulations a_1 a_2 a T)) (greater (growth_rate a_2 T) (growth_rate a_1 T)) → % 9.06/9.36 selection_favors a_2 a_1 T) % 9.06/9.36 True % 9.06/9.36 Clause #6 (by clausification #[5]): ∀ (a a_1 a_2 a_3 : Iota), % 9.06/9.36 Eq % 9.06/9.36 (And (And (environment a) (subpopulations a_1 a_2 a a_3)) (greater (growth_rate a_2 a_3) (growth_rate a_1 a_3)) → % 9.06/9.36 selection_favors a_2 a_1 a_3) % 9.06/9.36 True % 9.06/9.36 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 a_3 : Iota), % 9.06/9.36 Or % 9.06/9.36 (Eq (And (And (environment a) (subpopulations a_1 a_2 a a_3)) (greater (growth_rate a_2 a_3) (growth_rate a_1 a_3))) % 9.06/9.36 False) % 9.06/9.36 (Eq (selection_favors a_2 a_1 a_3) True) % 9.06/9.36 Clause #8 (by clausification #[7]): ∀ (a a_1 a_2 a_3 : Iota), % 9.06/9.36 Or (Eq (selection_favors a a_1 a_2) True) % 9.06/9.36 (Or (Eq (And (environment a_3) (subpopulations a_1 a a_3 a_2)) False) % 9.06/9.36 (Eq (greater (growth_rate a a_2) (growth_rate a_1 a_2)) False)) % 9.06/9.36 Clause #9 (by clausification #[8]): ∀ (a a_1 a_2 a_3 : Iota), % 9.06/9.36 Or (Eq (selection_favors a a_1 a_2) True) % 9.06/9.36 (Or (Eq (greater (growth_rate a a_2) (growth_rate a_1 a_2)) False) % 9.06/9.36 (Or (Eq (environment a_3) False) (Eq (subpopulations a_1 a a_3 a_2) False))) % 9.06/9.36 Clause #10 (by clausification #[2]): Eq % 9.06/9.36 (∀ (E : Iota), % 9.06/9.36 And (environment E) (stable E) → % 9.06/9.36 Exists fun To => % 9.06/9.36 And (in_environment E To) % 9.06/9.36 (∀ (T : Iota), % 9.06/9.36 And (subpopulations first_movers efficient_producers E T) (greater_or_equal T To) → % 9.06/9.36 selection_favors efficient_producers first_movers T)) % 9.06/9.36 False % 9.06/9.36 Clause #11 (by clausification #[10]): ∀ (a : Iota), % 9.06/9.36 Eq % 9.06/9.36 (Not % 9.06/9.36 (And (environment (skS.0 0 a)) (stable (skS.0 0 a)) → % 9.06/9.36 Exists fun To => % 9.06/9.36 And (in_environment (skS.0 0 a) To) % 9.06/9.36 (∀ (T : Iota), % 9.06/9.36 And (subpopulations first_movers efficient_producers (skS.0 0 a) T) (greater_or_equal T To) → % 9.06/9.36 selection_favors efficient_producers first_movers T))) % 9.06/9.36 True % 9.06/9.36 Clause #12 (by clausification #[11]): ∀ (a : Iota), % 9.06/9.36 Eq % 9.06/9.36 (And (environment (skS.0 0 a)) (stable (skS.0 0 a)) → % 9.06/9.36 Exists fun To => % 9.06/9.36 And (in_environment (skS.0 0 a) To) % 9.06/9.36 (∀ (T : Iota), % 9.06/9.36 And (subpopulations first_movers efficient_producers (skS.0 0 a) T) (greater_or_equal T To) → % 9.06/9.36 selection_favors efficient_producers first_movers T)) % 9.06/9.36 False % 9.06/9.36 Clause #13 (by clausification #[12]): ∀ (a : Iota), Eq (And (environment (skS.0 0 a)) (stable (skS.0 0 a))) True % 9.06/9.36 Clause #14 (by clausification #[12]): ∀ (a : Iota), % 9.16/9.40 Eq % 9.16/9.40 (Exists fun To => % 9.16/9.40 And (in_environment (skS.0 0 a) To) % 9.16/9.40 (∀ (T : Iota), % 9.16/9.40 And (subpopulations first_movers efficient_producers (skS.0 0 a) T) (greater_or_equal T To) → % 9.16/9.40 selection_favors efficient_producers first_movers T)) % 9.16/9.40 False % 9.16/9.40 Clause #15 (by clausification #[13]): ∀ (a : Iota), Eq (stable (skS.0 0 a)) True % 9.16/9.40 Clause #16 (by clausification #[13]): ∀ (a : Iota), Eq (environment (skS.0 0 a)) True % 9.16/9.40 Clause #17 (by clausification #[1]): ∀ (a : Iota), % 9.16/9.40 Eq % 9.16/9.40 (And (environment a) (stable a) → % 9.16/9.40 Exists fun To => % 9.16/9.40 And (in_environment a To) % 9.16/9.40 (∀ (T : Iota), % 9.16/9.40 And (subpopulations first_movers efficient_producers a T) (greater_or_equal T To) → % 9.16/9.40 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 9.16/9.40 True % 9.16/9.40 Clause #18 (by clausification #[17]): ∀ (a : Iota), % 9.16/9.40 Or (Eq (And (environment a) (stable a)) False) % 9.16/9.40 (Eq % 9.16/9.40 (Exists fun To => % 9.16/9.40 And (in_environment a To) % 9.16/9.40 (∀ (T : Iota), % 9.16/9.40 And (subpopulations first_movers efficient_producers a T) (greater_or_equal T To) → % 9.16/9.40 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 9.16/9.40 True) % 9.16/9.40 Clause #19 (by clausification #[18]): ∀ (a : Iota), % 9.16/9.40 Or % 9.16/9.40 (Eq % 9.16/9.40 (Exists fun To => % 9.16/9.40 And (in_environment a To) % 9.16/9.40 (∀ (T : Iota), % 9.16/9.40 And (subpopulations first_movers efficient_producers a T) (greater_or_equal T To) → % 9.16/9.40 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 9.16/9.40 True) % 9.16/9.40 (Or (Eq (environment a) False) (Eq (stable a) False)) % 9.16/9.40 Clause #20 (by clausification #[19]): ∀ (a a_1 : Iota), % 9.16/9.40 Or (Eq (environment a) False) % 9.16/9.40 (Or (Eq (stable a) False) % 9.16/9.40 (Eq % 9.16/9.40 (And (in_environment a (skS.0 1 a a_1)) % 9.16/9.40 (∀ (T : Iota), % 9.16/9.40 And (subpopulations first_movers efficient_producers a T) (greater_or_equal T (skS.0 1 a a_1)) → % 9.16/9.40 greater (growth_rate efficient_producers T) (growth_rate first_movers T))) % 9.16/9.40 True)) % 9.16/9.40 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), % 9.16/9.40 Or (Eq (environment a) False) % 9.16/9.40 (Or (Eq (stable a) False) % 9.16/9.40 (Eq % 9.16/9.40 (∀ (T : Iota), % 9.16/9.40 And (subpopulations first_movers efficient_producers a T) (greater_or_equal T (skS.0 1 a a_1)) → % 9.16/9.40 greater (growth_rate efficient_producers T) (growth_rate first_movers T)) % 9.16/9.40 True)) % 9.16/9.40 Clause #22 (by clausification #[20]): ∀ (a a_1 : Iota), Or (Eq (environment a) False) (Or (Eq (stable a) False) (Eq (in_environment a (skS.0 1 a a_1)) True)) % 9.16/9.40 Clause #23 (by clausification #[21]): ∀ (a a_1 a_2 : Iota), % 9.16/9.40 Or (Eq (environment a) False) % 9.16/9.40 (Or (Eq (stable a) False) % 9.16/9.40 (Eq % 9.16/9.40 (And (subpopulations first_movers efficient_producers a a_1) (greater_or_equal a_1 (skS.0 1 a a_2)) → % 9.16/9.40 greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1)) % 9.16/9.40 True)) % 9.16/9.40 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 : Iota), % 9.16/9.40 Or (Eq (environment a) False) % 9.16/9.40 (Or (Eq (stable a) False) % 9.16/9.40 (Or % 9.16/9.40 (Eq (And (subpopulations first_movers efficient_producers a a_1) (greater_or_equal a_1 (skS.0 1 a a_2))) False) % 9.16/9.40 (Eq (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1)) True))) % 9.16/9.40 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 : Iota), % 9.16/9.40 Or (Eq (environment a) False) % 9.16/9.40 (Or (Eq (stable a) False) % 9.16/9.40 (Or (Eq (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1)) True) % 9.16/9.40 (Or (Eq (subpopulations first_movers efficient_producers a a_1) False) % 9.16/9.40 (Eq (greater_or_equal a_1 (skS.0 1 a a_2)) False)))) % 9.16/9.40 Clause #26 (by superposition #[25, 16]): ∀ (a a_1 a_2 : Iota), % 9.16/9.40 Or (Eq (stable (skS.0 0 a)) False) % 9.16/9.40 (Or (Eq (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1)) True) % 9.16/9.40 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 9.16/9.40 (Or (Eq (greater_or_equal a_1 (skS.0 1 (skS.0 0 a) a_2)) False) (Eq False True)))) % 9.16/9.40 Clause #27 (by superposition #[22, 16]): ∀ (a a_1 : Iota), % 9.16/9.40 Or (Eq (stable (skS.0 0 a)) False) % 9.16/9.45 (Or (Eq (in_environment (skS.0 0 a) (skS.0 1 (skS.0 0 a) a_1)) True) (Eq False True)) % 9.16/9.45 Clause #28 (by clausification #[14]): ∀ (a a_1 : Iota), % 9.16/9.45 Eq % 9.16/9.45 (And (in_environment (skS.0 0 a) a_1) % 9.16/9.45 (∀ (T : Iota), % 9.16/9.45 And (subpopulations first_movers efficient_producers (skS.0 0 a) T) (greater_or_equal T a_1) → % 9.16/9.45 selection_favors efficient_producers first_movers T)) % 9.16/9.45 False % 9.16/9.45 Clause #29 (by clausification #[28]): ∀ (a a_1 : Iota), % 9.16/9.45 Or (Eq (in_environment (skS.0 0 a) a_1) False) % 9.16/9.45 (Eq % 9.16/9.45 (∀ (T : Iota), % 9.16/9.45 And (subpopulations first_movers efficient_producers (skS.0 0 a) T) (greater_or_equal T a_1) → % 9.16/9.45 selection_favors efficient_producers first_movers T) % 9.16/9.45 False) % 9.16/9.45 Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 : Iota), % 9.16/9.45 Or (Eq (in_environment (skS.0 0 a) a_1) False) % 9.16/9.45 (Eq % 9.16/9.45 (Not % 9.16/9.45 (And (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 9.16/9.45 (greater_or_equal (skS.0 2 a a_1 a_2) a_1) → % 9.16/9.45 selection_favors efficient_producers first_movers (skS.0 2 a a_1 a_2))) % 9.16/9.45 True) % 9.16/9.45 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 : Iota), % 9.16/9.45 Or (Eq (in_environment (skS.0 0 a) a_1) False) % 9.16/9.45 (Eq % 9.16/9.45 (And (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 9.16/9.45 (greater_or_equal (skS.0 2 a a_1 a_2) a_1) → % 9.16/9.45 selection_favors efficient_producers first_movers (skS.0 2 a a_1 a_2)) % 9.16/9.45 False) % 9.16/9.45 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), % 9.16/9.45 Or (Eq (in_environment (skS.0 0 a) a_1) False) % 9.16/9.45 (Eq % 9.16/9.45 (And (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 9.16/9.45 (greater_or_equal (skS.0 2 a a_1 a_2) a_1)) % 9.16/9.45 True) % 9.16/9.45 Clause #33 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), % 9.16/9.45 Or (Eq (in_environment (skS.0 0 a) a_1) False) % 9.16/9.45 (Eq (selection_favors efficient_producers first_movers (skS.0 2 a a_1 a_2)) False) % 9.16/9.45 Clause #34 (by clausification #[32]): ∀ (a a_1 a_2 : Iota), % 9.16/9.45 Or (Eq (in_environment (skS.0 0 a) a_1) False) (Eq (greater_or_equal (skS.0 2 a a_1 a_2) a_1) True) % 9.16/9.46 Clause #35 (by clausification #[32]): ∀ (a a_1 a_2 : Iota), % 9.16/9.46 Or (Eq (in_environment (skS.0 0 a) a_1) False) % 9.16/9.46 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 2 a a_1 a_2)) True) % 9.16/9.46 Clause #36 (by clausification #[27]): ∀ (a a_1 : Iota), Or (Eq (stable (skS.0 0 a)) False) (Eq (in_environment (skS.0 0 a) (skS.0 1 (skS.0 0 a) a_1)) True) % 9.16/9.46 Clause #37 (by forward demodulation #[36, 15]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (in_environment (skS.0 0 a) (skS.0 1 (skS.0 0 a) a_1)) True) % 9.16/9.46 Clause #38 (by clausification #[37]): ∀ (a a_1 : Iota), Eq (in_environment (skS.0 0 a) (skS.0 1 (skS.0 0 a) a_1)) True % 9.16/9.46 Clause #39 (by superposition #[38, 34]): ∀ (a a_1 a_2 : Iota), % 9.16/9.46 Or (Eq True False) (Eq (greater_or_equal (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2) (skS.0 1 (skS.0 0 a) a_1)) True) % 9.16/9.46 Clause #40 (by superposition #[38, 33]): ∀ (a a_1 a_2 : Iota), % 9.16/9.46 Or (Eq True False) % 9.16/9.46 (Eq (selection_favors efficient_producers first_movers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) False) % 9.16/9.46 Clause #41 (by superposition #[38, 35]): ∀ (a a_1 a_2 : Iota), % 9.16/9.46 Or (Eq True False) % 9.16/9.46 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) True) % 9.16/9.46 Clause #42 (by clausification #[40]): ∀ (a a_1 a_2 : Iota), % 9.16/9.46 Eq (selection_favors efficient_producers first_movers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) False % 9.16/9.46 Clause #43 (by clausification #[41]): ∀ (a a_1 a_2 : Iota), % 9.16/9.46 Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) True % 9.16/9.46 Clause #44 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), % 9.16/9.46 Or (Eq (stable (skS.0 0 a)) False) % 9.16/9.46 (Or (Eq (greater (growth_rate efficient_producers a_1) (growth_rate first_movers a_1)) True) % 9.16/9.46 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 9.16/9.46 (Eq (greater_or_equal a_1 (skS.0 1 (skS.0 0 a) a_2)) False))) % 9.16/9.46 Clause #45 (by forward demodulation #[44, 15]): ∀ (a a_1 a_2 : Iota), % 9.26/9.50 Or (Eq True False) % 9.26/9.50 (Or (Eq (greater (growth_rate efficient_producers a) (growth_rate first_movers a)) True) % 9.26/9.50 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) a) False) % 9.26/9.50 (Eq (greater_or_equal a (skS.0 1 (skS.0 0 a_1) a_2)) False))) % 9.26/9.50 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 : Iota), % 9.26/9.50 Or (Eq (greater (growth_rate efficient_producers a) (growth_rate first_movers a)) True) % 9.26/9.50 (Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a_1) a) False) % 9.26/9.50 (Eq (greater_or_equal a (skS.0 1 (skS.0 0 a_1) a_2)) False)) % 9.26/9.50 Clause #47 (by superposition #[46, 43]): ∀ (a a_1 a_2 a_3 : Iota), % 9.26/9.50 Or % 9.26/9.50 (Eq % 9.26/9.50 (greater (growth_rate efficient_producers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) % 9.26/9.50 (growth_rate first_movers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2))) % 9.26/9.50 True) % 9.26/9.50 (Or (Eq (greater_or_equal (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2) (skS.0 1 (skS.0 0 a) a_3)) False) % 9.26/9.50 (Eq False True)) % 9.26/9.50 Clause #48 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), Eq (greater_or_equal (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2) (skS.0 1 (skS.0 0 a) a_1)) True % 9.26/9.50 Clause #49 (by clausification #[47]): ∀ (a a_1 a_2 a_3 : Iota), % 9.26/9.50 Or % 9.26/9.50 (Eq % 9.26/9.50 (greater (growth_rate efficient_producers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) % 9.26/9.50 (growth_rate first_movers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2))) % 9.26/9.50 True) % 9.26/9.50 (Eq (greater_or_equal (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2) (skS.0 1 (skS.0 0 a) a_3)) False) % 9.26/9.50 Clause #50 (by superposition #[49, 48]): ∀ (a a_1 a_2 : Iota), % 9.26/9.50 Or % 9.26/9.50 (Eq % 9.26/9.50 (greater (growth_rate efficient_producers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) % 9.26/9.50 (growth_rate first_movers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2))) % 9.26/9.50 True) % 9.26/9.50 (Eq False True) % 9.26/9.50 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 : Iota), % 9.26/9.50 Eq % 9.26/9.50 (greater (growth_rate efficient_producers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) % 9.26/9.50 (growth_rate first_movers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2))) % 9.26/9.50 True % 9.26/9.50 Clause #52 (by superposition #[51, 9]): ∀ (a a_1 a_2 a_3 : Iota), % 9.26/9.50 Or (Eq (selection_favors efficient_producers first_movers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) True) % 9.26/9.50 (Or (Eq True False) % 9.26/9.50 (Or (Eq (environment a_3) False) % 9.26/9.50 (Eq (subpopulations first_movers efficient_producers a_3 (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) False))) % 9.26/9.50 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 : Iota), % 9.26/9.50 Or (Eq (selection_favors efficient_producers first_movers (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) True) % 9.26/9.50 (Or (Eq (environment a_3) False) % 9.26/9.50 (Eq (subpopulations first_movers efficient_producers a_3 (skS.0 2 a (skS.0 1 (skS.0 0 a) a_1) a_2)) False)) % 9.26/9.50 Clause #54 (by forward demodulation #[53, 42]): ∀ (a a_1 a_2 a_3 : Iota), % 9.26/9.50 Or (Eq False True) % 9.26/9.50 (Or (Eq (environment a) False) % 9.26/9.50 (Eq (subpopulations first_movers efficient_producers a (skS.0 2 a_1 (skS.0 1 (skS.0 0 a_1) a_2) a_3)) False)) % 9.26/9.50 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 a_3 : Iota), % 9.26/9.50 Or (Eq (environment a) False) % 9.26/9.50 (Eq (subpopulations first_movers efficient_producers a (skS.0 2 a_1 (skS.0 1 (skS.0 0 a_1) a_2) a_3)) False) % 9.26/9.50 Clause #56 (by superposition #[55, 16]): ∀ (a a_1 a_2 a_3 : Iota), % 9.26/9.50 Or % 9.26/9.50 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 2 a_1 (skS.0 1 (skS.0 0 a_1) a_2) a_3)) % 9.26/9.50 False) % 9.26/9.50 (Eq False True) % 9.26/9.50 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 : Iota), % 9.26/9.50 Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 2 a_1 (skS.0 1 (skS.0 0 a_1) a_2) a_3)) False % 9.26/9.50 Clause #58 (by superposition #[57, 43]): Eq False True % 9.26/9.50 Clause #59 (by clausification #[58]): False % 9.26/9.50 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------