%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT039+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:06:19 AM UTC 2026 % Result : Theorem 13.79s 14.12s % Output : Proof 14.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT039+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.05 % Command : duper %s % 0.13/0.39 % Computer : n016.cluster.edu % 0.13/0.39 % Model : x86_64 x86_64 % 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.39 % Memory : 8046.5625MB % 0.13/0.39 % OS : Linux 6.8.0-71-generic % 0.13/0.39 % CPULimit : 300 % 0.13/0.39 % WCLimit : 300 % 0.13/0.39 % DateTime : Mon Sep 7 12:58:17 UTC 2026 % 0.13/0.39 % CPUTime : % 13.79/14.12 SZS status Theorem for theBenchmark.p % 13.79/14.12 SZS output start Proof for theBenchmark.p % 13.79/14.12 Clause #0 (by assumption #[]): Eq % 13.79/14.12 (∀ (P : Iota), % 13.79/14.12 And % 13.79/14.12 (And (And (observational_period P) (propagation_strategy first_movers)) % 13.79/14.12 (propagation_strategy efficient_producers)) % 13.79/14.12 (∀ (E : Iota), % 13.79/14.12 And (environment E) (in_environment P E) → selection_favors efficient_producers first_movers (end_time E)) → % 13.79/14.12 selection_favors efficient_producers first_movers P) % 13.79/14.12 True % 13.79/14.12 Clause #1 (by assumption #[]): Eq % 13.79/14.12 (∀ (P : Iota), % 13.79/14.12 And (observational_period P) (slow_change P) → % 13.79/14.12 ∀ (E : Iota), % 13.79/14.12 And (environment E) (in_environment P E) → % 13.79/14.12 Exists fun T => And (in_environment E T) (greater T (critical_point E))) % 13.79/14.12 True % 13.79/14.12 Clause #2 (by assumption #[]): Eq (propagation_strategy first_movers) True % 13.79/14.12 Clause #3 (by assumption #[]): Eq (propagation_strategy efficient_producers) True % 13.79/14.12 Clause #4 (by assumption #[]): Eq % 13.79/14.12 (∀ (E T : Iota), % 13.79/14.12 And (And (environment E) (greater_or_equal T (start_time E))) (greater_or_equal (end_time E) T) → % 13.79/14.12 in_environment E T) % 13.79/14.12 True % 13.79/14.12 Clause #5 (by assumption #[]): Eq (∀ (E T : Iota), And (environment E) (in_environment E T) → greater_or_equal (end_time E) T) True % 13.79/14.12 Clause #6 (by assumption #[]): Eq (∀ (E : Iota), environment E → greater_or_equal (critical_point E) (start_time E)) True % 13.79/14.12 Clause #7 (by assumption #[]): Eq (∀ (X Y Z : Iota), And (greater X Y) (greater Y Z) → greater X Z) True % 13.79/14.12 Clause #8 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (greater_or_equal X Y) (Or (greater X Y) (Eq X Y))) True % 13.79/14.12 Clause #10 (by assumption #[]): Eq % 13.79/14.12 (∀ (E T : Iota), % 13.79/14.12 And (And (environment E) (in_environment E T)) (greater T (critical_point E)) → % 13.79/14.12 selection_favors efficient_producers first_movers T) % 13.79/14.12 True % 13.79/14.12 Clause #11 (by assumption #[]): Eq % 13.79/14.12 (Not % 13.79/14.12 (∀ (P : Iota), And (observational_period P) (slow_change P) → selection_favors efficient_producers first_movers P)) % 13.79/14.12 True % 13.79/14.12 Clause #12 (by clausification #[0]): ∀ (a : Iota), % 13.79/14.12 Eq % 13.79/14.12 (And % 13.79/14.12 (And (And (observational_period a) (propagation_strategy first_movers)) % 13.79/14.12 (propagation_strategy efficient_producers)) % 13.79/14.12 (∀ (E : Iota), % 13.79/14.12 And (environment E) (in_environment a E) → selection_favors efficient_producers first_movers (end_time E)) → % 13.79/14.12 selection_favors efficient_producers first_movers a) % 13.79/14.12 True % 13.79/14.12 Clause #13 (by clausification #[12]): ∀ (a : Iota), % 13.79/14.12 Or % 13.79/14.12 (Eq % 13.79/14.12 (And % 13.79/14.12 (And (And (observational_period a) (propagation_strategy first_movers)) % 13.79/14.12 (propagation_strategy efficient_producers)) % 13.79/14.12 (∀ (E : Iota), % 13.79/14.12 And (environment E) (in_environment a E) → selection_favors efficient_producers first_movers (end_time E))) % 13.79/14.12 False) % 13.79/14.12 (Eq (selection_favors efficient_producers first_movers a) True) % 13.79/14.12 Clause #14 (by clausification #[13]): ∀ (a : Iota), % 13.79/14.12 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.79/14.12 (Or % 13.79/14.12 (Eq % 13.79/14.12 (And (And (observational_period a) (propagation_strategy first_movers)) % 13.79/14.12 (propagation_strategy efficient_producers)) % 13.79/14.12 False) % 13.79/14.12 (Eq % 13.79/14.12 (∀ (E : Iota), % 13.79/14.12 And (environment E) (in_environment a E) → selection_favors efficient_producers first_movers (end_time E)) % 13.79/14.12 False)) % 13.79/14.12 Clause #15 (by clausification #[14]): ∀ (a : Iota), % 13.79/14.12 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.79/14.12 (Or % 13.79/14.12 (Eq % 13.79/14.12 (∀ (E : Iota), % 13.79/14.12 And (environment E) (in_environment a E) → selection_favors efficient_producers first_movers (end_time E)) % 13.79/14.12 False) % 13.79/14.12 (Or (Eq (And (observational_period a) (propagation_strategy first_movers)) False) % 13.79/14.12 (Eq (propagation_strategy efficient_producers) False))) % 13.79/14.12 Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota), % 13.79/14.12 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.79/14.12 (Or (Eq (And (observational_period a) (propagation_strategy first_movers)) False) % 13.79/14.12 (Or (Eq (propagation_strategy efficient_producers) False) % 13.79/14.12 (Eq % 13.79/14.12 (Not % 13.79/14.12 (And (environment (skS.0 0 a a_1)) (in_environment a (skS.0 0 a a_1)) → % 13.89/14.16 selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1)))) % 13.89/14.16 True))) % 13.89/14.16 Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota), % 13.89/14.16 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.89/14.16 (Or (Eq (propagation_strategy efficient_producers) False) % 13.89/14.16 (Or % 13.89/14.16 (Eq % 13.89/14.16 (Not % 13.89/14.16 (And (environment (skS.0 0 a a_1)) (in_environment a (skS.0 0 a a_1)) → % 13.89/14.16 selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1)))) % 13.89/14.16 True) % 13.89/14.16 (Or (Eq (observational_period a) False) (Eq (propagation_strategy first_movers) False)))) % 13.89/14.16 Clause #18 (by clausification #[17]): ∀ (a a_1 : Iota), % 13.89/14.16 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.89/14.16 (Or (Eq (propagation_strategy efficient_producers) False) % 13.89/14.16 (Or (Eq (observational_period a) False) % 13.89/14.16 (Or (Eq (propagation_strategy first_movers) False) % 13.89/14.16 (Eq % 13.89/14.16 (And (environment (skS.0 0 a a_1)) (in_environment a (skS.0 0 a a_1)) → % 13.89/14.16 selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) % 13.89/14.16 False)))) % 13.89/14.16 Clause #19 (by clausification #[18]): ∀ (a a_1 : Iota), % 13.89/14.16 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.89/14.16 (Or (Eq (propagation_strategy efficient_producers) False) % 13.89/14.16 (Or (Eq (observational_period a) False) % 13.89/14.16 (Or (Eq (propagation_strategy first_movers) False) % 13.89/14.16 (Eq (And (environment (skS.0 0 a a_1)) (in_environment a (skS.0 0 a a_1))) True)))) % 13.89/14.16 Clause #20 (by clausification #[18]): ∀ (a a_1 : Iota), % 13.89/14.16 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.89/14.16 (Or (Eq (propagation_strategy efficient_producers) False) % 13.89/14.16 (Or (Eq (observational_period a) False) % 13.89/14.16 (Or (Eq (propagation_strategy first_movers) False) % 13.89/14.16 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) False)))) % 13.89/14.16 Clause #21 (by clausification #[19]): ∀ (a a_1 : Iota), % 13.89/14.16 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.89/14.16 (Or (Eq (propagation_strategy efficient_producers) False) % 13.89/14.16 (Or (Eq (observational_period a) False) % 13.89/14.16 (Or (Eq (propagation_strategy first_movers) False) (Eq (in_environment a (skS.0 0 a a_1)) True)))) % 13.89/14.16 Clause #22 (by clausification #[19]): ∀ (a a_1 : Iota), % 13.89/14.16 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.89/14.16 (Or (Eq (propagation_strategy efficient_producers) False) % 13.89/14.16 (Or (Eq (observational_period a) False) % 13.89/14.16 (Or (Eq (propagation_strategy first_movers) False) (Eq (environment (skS.0 0 a a_1)) True)))) % 13.89/14.16 Clause #23 (by forward demodulation #[21, 3]): ∀ (a a_1 : Iota), % 13.89/14.16 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.89/14.16 (Or (Eq True False) % 13.89/14.16 (Or (Eq (observational_period a) False) % 13.89/14.16 (Or (Eq (propagation_strategy first_movers) False) (Eq (in_environment a (skS.0 0 a a_1)) True)))) % 13.89/14.16 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), % 13.89/14.16 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.89/14.16 (Or (Eq (observational_period a) False) % 13.89/14.16 (Or (Eq (propagation_strategy first_movers) False) (Eq (in_environment a (skS.0 0 a a_1)) True))) % 13.89/14.16 Clause #25 (by forward demodulation #[24, 2]): ∀ (a a_1 : Iota), % 13.89/14.16 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.89/14.16 (Or (Eq (observational_period a) False) (Or (Eq True False) (Eq (in_environment a (skS.0 0 a a_1)) True))) % 13.89/14.16 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), % 13.89/14.16 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.89/14.16 (Or (Eq (observational_period a) False) (Eq (in_environment a (skS.0 0 a a_1)) True)) % 13.89/14.16 Clause #27 (by clausification #[4]): ∀ (a : Iota), % 13.89/14.16 Eq % 13.89/14.16 (∀ (T : Iota), % 13.89/14.16 And (And (environment a) (greater_or_equal T (start_time a))) (greater_or_equal (end_time a) T) → % 13.89/14.16 in_environment a T) % 13.89/14.16 True % 13.89/14.16 Clause #28 (by clausification #[27]): ∀ (a a_1 : Iota), % 13.89/14.16 Eq % 13.89/14.16 (And (And (environment a) (greater_or_equal a_1 (start_time a))) (greater_or_equal (end_time a) a_1) → % 13.89/14.16 in_environment a a_1) % 13.96/14.21 True % 13.96/14.21 Clause #29 (by clausification #[28]): ∀ (a a_1 : Iota), % 13.96/14.21 Or (Eq (And (And (environment a) (greater_or_equal a_1 (start_time a))) (greater_or_equal (end_time a) a_1)) False) % 13.96/14.21 (Eq (in_environment a a_1) True) % 13.96/14.21 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), % 13.96/14.21 Or (Eq (in_environment a a_1) True) % 13.96/14.21 (Or (Eq (And (environment a) (greater_or_equal a_1 (start_time a))) False) % 13.96/14.21 (Eq (greater_or_equal (end_time a) a_1) False)) % 13.96/14.21 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), % 13.96/14.21 Or (Eq (in_environment a a_1) True) % 13.96/14.21 (Or (Eq (greater_or_equal (end_time a) a_1) False) % 13.96/14.21 (Or (Eq (environment a) False) (Eq (greater_or_equal a_1 (start_time a)) False))) % 13.96/14.21 Clause #32 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (T : Iota), And (environment a) (in_environment a T) → greater_or_equal (end_time a) T) True % 13.96/14.21 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), Eq (And (environment a) (in_environment a a_1) → greater_or_equal (end_time a) a_1) True % 13.96/14.21 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), % 13.96/14.21 Or (Eq (And (environment a) (in_environment a a_1)) False) (Eq (greater_or_equal (end_time a) a_1) True) % 13.96/14.21 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), % 13.96/14.21 Or (Eq (greater_or_equal (end_time a) a_1) True) (Or (Eq (environment a) False) (Eq (in_environment a a_1) False)) % 13.96/14.21 Clause #36 (by clausification #[1]): ∀ (a : Iota), % 13.96/14.21 Eq % 13.96/14.21 (And (observational_period a) (slow_change a) → % 13.96/14.21 ∀ (E : Iota), % 13.96/14.21 And (environment E) (in_environment a E) → % 13.96/14.21 Exists fun T => And (in_environment E T) (greater T (critical_point E))) % 13.96/14.21 True % 13.96/14.21 Clause #37 (by clausification #[36]): ∀ (a : Iota), % 13.96/14.21 Or (Eq (And (observational_period a) (slow_change a)) False) % 13.96/14.21 (Eq % 13.96/14.21 (∀ (E : Iota), % 13.96/14.21 And (environment E) (in_environment a E) → % 13.96/14.21 Exists fun T => And (in_environment E T) (greater T (critical_point E))) % 13.96/14.21 True) % 13.96/14.21 Clause #38 (by clausification #[37]): ∀ (a : Iota), % 13.96/14.21 Or % 13.96/14.21 (Eq % 13.96/14.21 (∀ (E : Iota), % 13.96/14.21 And (environment E) (in_environment a E) → % 13.96/14.21 Exists fun T => And (in_environment E T) (greater T (critical_point E))) % 13.96/14.21 True) % 13.96/14.21 (Or (Eq (observational_period a) False) (Eq (slow_change a) False)) % 13.96/14.21 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), % 13.96/14.21 Or (Eq (observational_period a) False) % 13.96/14.21 (Or (Eq (slow_change a) False) % 13.96/14.21 (Eq % 13.96/14.21 (And (environment a_1) (in_environment a a_1) → % 13.96/14.21 Exists fun T => And (in_environment a_1 T) (greater T (critical_point a_1))) % 13.96/14.21 True)) % 13.96/14.21 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), % 13.96/14.21 Or (Eq (observational_period a) False) % 13.96/14.21 (Or (Eq (slow_change a) False) % 13.96/14.21 (Or (Eq (And (environment a_1) (in_environment a a_1)) False) % 13.96/14.21 (Eq (Exists fun T => And (in_environment a_1 T) (greater T (critical_point a_1))) True))) % 13.96/14.21 Clause #41 (by clausification #[40]): ∀ (a a_1 : Iota), % 13.96/14.21 Or (Eq (observational_period a) False) % 13.96/14.21 (Or (Eq (slow_change a) False) % 13.96/14.21 (Or (Eq (Exists fun T => And (in_environment a_1 T) (greater T (critical_point a_1))) True) % 13.96/14.21 (Or (Eq (environment a_1) False) (Eq (in_environment a a_1) False)))) % 13.96/14.21 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 : Iota), % 13.96/14.21 Or (Eq (observational_period a) False) % 13.96/14.21 (Or (Eq (slow_change a) False) % 13.96/14.21 (Or (Eq (environment a_1) False) % 13.96/14.21 (Or (Eq (in_environment a a_1) False) % 13.96/14.21 (Eq (And (in_environment a_1 (skS.0 1 a_1 a_2)) (greater (skS.0 1 a_1 a_2) (critical_point a_1))) True)))) % 13.96/14.21 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 : Iota), % 13.96/14.21 Or (Eq (observational_period a) False) % 13.96/14.21 (Or (Eq (slow_change a) False) % 13.96/14.21 (Or (Eq (environment a_1) False) % 13.96/14.21 (Or (Eq (in_environment a a_1) False) (Eq (greater (skS.0 1 a_1 a_2) (critical_point a_1)) True)))) % 13.96/14.21 Clause #44 (by clausification #[42]): ∀ (a a_1 a_2 : Iota), % 13.96/14.21 Or (Eq (observational_period a) False) % 13.96/14.21 (Or (Eq (slow_change a) False) % 13.96/14.21 (Or (Eq (environment a_1) False) % 13.96/14.21 (Or (Eq (in_environment a a_1) False) (Eq (in_environment a_1 (skS.0 1 a_1 a_2)) True)))) % 13.96/14.21 Clause #45 (by clausification #[11]): Eq (∀ (P : Iota), And (observational_period P) (slow_change P) → selection_favors efficient_producers first_movers P) % 13.96/14.26 False % 13.96/14.26 Clause #46 (by clausification #[45]): ∀ (a : Iota), % 13.96/14.26 Eq % 13.96/14.26 (Not % 13.96/14.26 (And (observational_period (skS.0 2 a)) (slow_change (skS.0 2 a)) → % 13.96/14.26 selection_favors efficient_producers first_movers (skS.0 2 a))) % 13.96/14.26 True % 13.96/14.26 Clause #47 (by clausification #[46]): ∀ (a : Iota), % 13.96/14.26 Eq % 13.96/14.26 (And (observational_period (skS.0 2 a)) (slow_change (skS.0 2 a)) → % 13.96/14.26 selection_favors efficient_producers first_movers (skS.0 2 a)) % 13.96/14.26 False % 13.96/14.26 Clause #48 (by clausification #[47]): ∀ (a : Iota), Eq (And (observational_period (skS.0 2 a)) (slow_change (skS.0 2 a))) True % 13.96/14.26 Clause #49 (by clausification #[47]): ∀ (a : Iota), Eq (selection_favors efficient_producers first_movers (skS.0 2 a)) False % 13.96/14.26 Clause #50 (by clausification #[48]): ∀ (a : Iota), Eq (slow_change (skS.0 2 a)) True % 13.96/14.26 Clause #51 (by clausification #[48]): ∀ (a : Iota), Eq (observational_period (skS.0 2 a)) True % 13.96/14.26 Clause #52 (by superposition #[51, 26]): ∀ (a a_1 : Iota), % 13.96/14.26 Or (Eq (selection_favors efficient_producers first_movers (skS.0 2 a)) True) % 13.96/14.26 (Or (Eq True False) (Eq (in_environment (skS.0 2 a) (skS.0 0 (skS.0 2 a) a_1)) True)) % 13.96/14.26 Clause #53 (by superposition #[51, 43]): ∀ (a a_1 a_2 : Iota), % 13.96/14.26 Or (Eq True False) % 13.96/14.26 (Or (Eq (slow_change (skS.0 2 a)) False) % 13.96/14.26 (Or (Eq (environment a_1) False) % 13.96/14.26 (Or (Eq (in_environment (skS.0 2 a) a_1) False) (Eq (greater (skS.0 1 a_1 a_2) (critical_point a_1)) True)))) % 13.96/14.26 Clause #60 (by clausification #[10]): ∀ (a : Iota), % 13.96/14.26 Eq % 13.96/14.26 (∀ (T : Iota), % 13.96/14.26 And (And (environment a) (in_environment a T)) (greater T (critical_point a)) → % 13.96/14.26 selection_favors efficient_producers first_movers T) % 13.96/14.26 True % 13.96/14.26 Clause #61 (by clausification #[60]): ∀ (a a_1 : Iota), % 13.96/14.26 Eq % 13.96/14.26 (And (And (environment a) (in_environment a a_1)) (greater a_1 (critical_point a)) → % 13.96/14.26 selection_favors efficient_producers first_movers a_1) % 13.96/14.26 True % 13.96/14.26 Clause #62 (by clausification #[61]): ∀ (a a_1 : Iota), % 13.96/14.26 Or (Eq (And (And (environment a) (in_environment a a_1)) (greater a_1 (critical_point a))) False) % 13.96/14.26 (Eq (selection_favors efficient_producers first_movers a_1) True) % 13.96/14.26 Clause #63 (by clausification #[62]): ∀ (a a_1 : Iota), % 13.96/14.26 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.96/14.26 (Or (Eq (And (environment a_1) (in_environment a_1 a)) False) (Eq (greater a (critical_point a_1)) False)) % 13.96/14.26 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), % 13.96/14.26 Or (Eq (selection_favors efficient_producers first_movers a) True) % 13.96/14.26 (Or (Eq (greater a (critical_point a_1)) False) (Or (Eq (environment a_1) False) (Eq (in_environment a_1 a) False))) % 13.96/14.26 Clause #65 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (Y Z : Iota), And (greater a Y) (greater Y Z) → greater a Z) True % 13.96/14.26 Clause #66 (by clausification #[65]): ∀ (a a_1 : Iota), Eq (∀ (Z : Iota), And (greater a a_1) (greater a_1 Z) → greater a Z) True % 13.96/14.26 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 : Iota), Eq (And (greater a a_1) (greater a_1 a_2) → greater a a_2) True % 13.96/14.26 Clause #68 (by clausification #[67]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (greater a a_1) (greater a_1 a_2)) False) (Eq (greater a a_2) True) % 13.96/14.26 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 : Iota), Or (Eq (greater a a_1) True) (Or (Eq (greater a a_2) False) (Eq (greater a_2 a_1) False)) % 13.96/14.26 Clause #70 (by clausification #[6]): ∀ (a : Iota), Eq (environment a → greater_or_equal (critical_point a) (start_time a)) True % 13.96/14.26 Clause #71 (by clausification #[70]): ∀ (a : Iota), Or (Eq (environment a) False) (Eq (greater_or_equal (critical_point a) (start_time a)) True) % 13.96/14.26 Clause #72 (by clausification #[8]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (greater_or_equal a Y) (Or (greater a Y) (Eq a Y))) True % 13.96/14.26 Clause #73 (by clausification #[72]): ∀ (a a_1 : Iota), Eq (Iff (greater_or_equal a a_1) (Or (greater a a_1) (Eq a a_1))) True % 13.96/14.26 Clause #74 (by clausification #[73]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (Or (greater a a_1) (Eq a a_1)) False) % 13.96/14.26 Clause #75 (by clausification #[73]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Eq (Or (greater a a_1) (Eq a a_1)) True) % 14.06/14.31 Clause #76 (by clausification #[74]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (Eq a a_1) False) % 14.06/14.31 Clause #77 (by clausification #[74]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Eq (greater a a_1) False) % 14.06/14.31 Clause #78 (by clausification #[76]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) True) (Ne a a_1) % 14.06/14.31 Clause #79 (by destructive equality resolution #[78]): ∀ (a : Iota), Eq (greater_or_equal a a) True % 14.06/14.31 Clause #80 (by superposition #[79, 31]): ∀ (a : Iota), % 14.06/14.31 Or (Eq (in_environment a (end_time a)) True) % 14.06/14.31 (Or (Eq True False) (Or (Eq (environment a) False) (Eq (greater_or_equal (end_time a) (start_time a)) False))) % 14.06/14.31 Clause #81 (by clausification #[75]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Or (Eq (greater a a_1) True) (Eq (Eq a a_1) True)) % 14.06/14.31 Clause #82 (by clausification #[81]): ∀ (a a_1 : Iota), Or (Eq (greater_or_equal a a_1) False) (Or (Eq (greater a a_1) True) (Eq a a_1)) % 14.06/14.31 Clause #85 (by forward demodulation #[20, 3]): ∀ (a a_1 : Iota), % 14.06/14.31 Or (Eq (selection_favors efficient_producers first_movers a) True) % 14.06/14.31 (Or (Eq True False) % 14.06/14.31 (Or (Eq (observational_period a) False) % 14.06/14.31 (Or (Eq (propagation_strategy first_movers) False) % 14.06/14.31 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) False)))) % 14.06/14.31 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), % 14.06/14.31 Or (Eq (selection_favors efficient_producers first_movers a) True) % 14.06/14.31 (Or (Eq (observational_period a) False) % 14.06/14.31 (Or (Eq (propagation_strategy first_movers) False) % 14.06/14.31 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) False))) % 14.06/14.31 Clause #87 (by forward demodulation #[86, 2]): ∀ (a a_1 : Iota), % 14.06/14.31 Or (Eq (selection_favors efficient_producers first_movers a) True) % 14.06/14.31 (Or (Eq (observational_period a) False) % 14.06/14.31 (Or (Eq True False) (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) False))) % 14.06/14.31 Clause #88 (by clausification #[87]): ∀ (a a_1 : Iota), % 14.06/14.31 Or (Eq (selection_favors efficient_producers first_movers a) True) % 14.06/14.31 (Or (Eq (observational_period a) False) % 14.06/14.31 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 a a_1))) False)) % 14.06/14.31 Clause #89 (by superposition #[88, 51]): ∀ (a a_1 : Iota), % 14.06/14.31 Or (Eq (selection_favors efficient_producers first_movers (skS.0 2 a)) True) % 14.06/14.31 (Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 2 a) a_1))) False) % 14.06/14.31 (Eq False True)) % 14.06/14.31 Clause #90 (by clausification #[80]): ∀ (a : Iota), % 14.06/14.31 Or (Eq (in_environment a (end_time a)) True) % 14.06/14.31 (Or (Eq (environment a) False) (Eq (greater_or_equal (end_time a) (start_time a)) False)) % 14.06/14.31 Clause #91 (by superposition #[44, 51]): ∀ (a a_1 a_2 : Iota), % 14.06/14.31 Or (Eq True False) % 14.06/14.31 (Or (Eq (slow_change (skS.0 2 a)) False) % 14.06/14.31 (Or (Eq (environment a_1) False) % 14.06/14.31 (Or (Eq (in_environment (skS.0 2 a) a_1) False) (Eq (in_environment a_1 (skS.0 1 a_1 a_2)) True)))) % 14.06/14.31 Clause #92 (by forward demodulation #[22, 3]): ∀ (a a_1 : Iota), % 14.06/14.31 Or (Eq (selection_favors efficient_producers first_movers a) True) % 14.06/14.31 (Or (Eq True False) % 14.06/14.31 (Or (Eq (observational_period a) False) % 14.06/14.31 (Or (Eq (propagation_strategy first_movers) False) (Eq (environment (skS.0 0 a a_1)) True)))) % 14.06/14.31 Clause #93 (by clausification #[92]): ∀ (a a_1 : Iota), % 14.06/14.31 Or (Eq (selection_favors efficient_producers first_movers a) True) % 14.06/14.31 (Or (Eq (observational_period a) False) % 14.06/14.31 (Or (Eq (propagation_strategy first_movers) False) (Eq (environment (skS.0 0 a a_1)) True))) % 14.06/14.31 Clause #94 (by forward demodulation #[93, 2]): ∀ (a a_1 : Iota), % 14.06/14.31 Or (Eq (selection_favors efficient_producers first_movers a) True) % 14.06/14.31 (Or (Eq (observational_period a) False) (Or (Eq True False) (Eq (environment (skS.0 0 a a_1)) True))) % 14.06/14.31 Clause #95 (by clausification #[94]): ∀ (a a_1 : Iota), % 14.06/14.31 Or (Eq (selection_favors efficient_producers first_movers a) True) % 14.06/14.31 (Or (Eq (observational_period a) False) (Eq (environment (skS.0 0 a a_1)) True)) % 14.06/14.37 Clause #96 (by superposition #[95, 51]): ∀ (a a_1 : Iota), % 14.06/14.37 Or (Eq (selection_favors efficient_producers first_movers (skS.0 2 a)) True) % 14.06/14.37 (Or (Eq (environment (skS.0 0 (skS.0 2 a) a_1)) True) (Eq False True)) % 14.06/14.37 Clause #97 (by clausification #[96]): ∀ (a a_1 : Iota), % 14.06/14.37 Or (Eq (selection_favors efficient_producers first_movers (skS.0 2 a)) True) % 14.06/14.37 (Eq (environment (skS.0 0 (skS.0 2 a) a_1)) True) % 14.06/14.37 Clause #98 (by forward demodulation #[97, 49]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (environment (skS.0 0 (skS.0 2 a) a_1)) True) % 14.06/14.37 Clause #99 (by clausification #[98]): ∀ (a a_1 : Iota), Eq (environment (skS.0 0 (skS.0 2 a) a_1)) True % 14.06/14.37 Clause #100 (by superposition #[99, 35]): ∀ (a a_1 a_2 : Iota), % 14.06/14.37 Or (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) a_2) True) % 14.06/14.37 (Or (Eq True False) (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) a_2) False)) % 14.06/14.37 Clause #102 (by superposition #[99, 71]): ∀ (a a_1 : Iota), % 14.06/14.37 Or (Eq True False) % 14.06/14.37 (Eq (greater_or_equal (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.06/14.37 Clause #103 (by superposition #[99, 90]): ∀ (a a_1 : Iota), % 14.06/14.37 Or (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (end_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.06/14.37 (Or (Eq True False) % 14.06/14.37 (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) False)) % 14.06/14.37 Clause #104 (by clausification #[89]): ∀ (a a_1 : Iota), % 14.06/14.37 Or (Eq (selection_favors efficient_producers first_movers (skS.0 2 a)) True) % 14.06/14.37 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 2 a) a_1))) False) % 14.06/14.37 Clause #105 (by forward demodulation #[104, 49]): ∀ (a a_1 : Iota), % 14.06/14.37 Or (Eq False True) (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 2 a) a_1))) False) % 14.06/14.37 Clause #106 (by clausification #[105]): ∀ (a a_1 : Iota), Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 2 a) a_1))) False % 14.06/14.37 Clause #107 (by clausification #[52]): ∀ (a a_1 : Iota), % 14.06/14.37 Or (Eq (selection_favors efficient_producers first_movers (skS.0 2 a)) True) % 14.06/14.37 (Eq (in_environment (skS.0 2 a) (skS.0 0 (skS.0 2 a) a_1)) True) % 14.06/14.37 Clause #108 (by forward demodulation #[107, 49]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (in_environment (skS.0 2 a) (skS.0 0 (skS.0 2 a) a_1)) True) % 14.06/14.37 Clause #109 (by clausification #[108]): ∀ (a a_1 : Iota), Eq (in_environment (skS.0 2 a) (skS.0 0 (skS.0 2 a) a_1)) True % 14.06/14.37 Clause #110 (by clausification #[102]): ∀ (a a_1 : Iota), % 14.06/14.37 Eq (greater_or_equal (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) True % 14.06/14.37 Clause #111 (by superposition #[110, 82]): ∀ (a a_1 : Iota), % 14.06/14.37 Or (Eq True False) % 14.06/14.37 (Or (Eq (greater (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.06/14.37 (Eq (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1)))) % 14.06/14.37 Clause #112 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), % 14.06/14.37 Or (Eq (slow_change (skS.0 2 a)) False) % 14.06/14.37 (Or (Eq (environment a_1) False) % 14.06/14.37 (Or (Eq (in_environment (skS.0 2 a) a_1) False) (Eq (in_environment a_1 (skS.0 1 a_1 a_2)) True))) % 14.06/14.37 Clause #113 (by forward demodulation #[112, 50]): ∀ (a a_1 a_2 : Iota), % 14.06/14.37 Or (Eq True False) % 14.06/14.37 (Or (Eq (environment a) False) % 14.06/14.37 (Or (Eq (in_environment (skS.0 2 a_1) a) False) (Eq (in_environment a (skS.0 1 a a_2)) True))) % 14.06/14.37 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 : Iota), % 14.06/14.37 Or (Eq (environment a) False) % 14.06/14.37 (Or (Eq (in_environment (skS.0 2 a_1) a) False) (Eq (in_environment a (skS.0 1 a a_2)) True)) % 14.06/14.37 Clause #115 (by superposition #[114, 99]): ∀ (a a_1 a_2 a_3 : Iota), % 14.06/14.37 Or (Eq (in_environment (skS.0 2 a) (skS.0 0 (skS.0 2 a_1) a_2)) False) % 14.06/14.37 (Or (Eq (in_environment (skS.0 0 (skS.0 2 a_1) a_2) (skS.0 1 (skS.0 0 (skS.0 2 a_1) a_2) a_3)) True) % 14.06/14.37 (Eq False True)) % 14.06/14.37 Clause #116 (by clausification #[53]): ∀ (a a_1 a_2 : Iota), % 14.06/14.37 Or (Eq (slow_change (skS.0 2 a)) False) % 14.06/14.37 (Or (Eq (environment a_1) False) % 14.06/14.37 (Or (Eq (in_environment (skS.0 2 a) a_1) False) (Eq (greater (skS.0 1 a_1 a_2) (critical_point a_1)) True))) % 14.16/14.43 Clause #117 (by forward demodulation #[116, 50]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Or (Eq True False) % 14.16/14.43 (Or (Eq (environment a) False) % 14.16/14.43 (Or (Eq (in_environment (skS.0 2 a_1) a) False) (Eq (greater (skS.0 1 a a_2) (critical_point a)) True))) % 14.16/14.43 Clause #118 (by clausification #[117]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Or (Eq (environment a) False) % 14.16/14.43 (Or (Eq (in_environment (skS.0 2 a_1) a) False) (Eq (greater (skS.0 1 a a_2) (critical_point a)) True)) % 14.16/14.43 Clause #119 (by superposition #[118, 99]): ∀ (a a_1 a_2 a_3 : Iota), % 14.16/14.43 Or (Eq (in_environment (skS.0 2 a) (skS.0 0 (skS.0 2 a_1) a_2)) False) % 14.16/14.43 (Or (Eq (greater (skS.0 1 (skS.0 0 (skS.0 2 a_1) a_2) a_3) (critical_point (skS.0 0 (skS.0 2 a_1) a_2))) True) % 14.16/14.43 (Eq False True)) % 14.16/14.43 Clause #120 (by clausification #[100]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Or (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) a_2) True) % 14.16/14.43 (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) a_2) False) % 14.16/14.43 Clause #122 (by clausification #[103]): ∀ (a a_1 : Iota), % 14.16/14.43 Or (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (end_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.16/14.43 (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) False) % 14.16/14.43 Clause #123 (by clausification #[115]): ∀ (a a_1 a_2 a_3 : Iota), % 14.16/14.43 Or (Eq (in_environment (skS.0 2 a) (skS.0 0 (skS.0 2 a_1) a_2)) False) % 14.16/14.43 (Eq (in_environment (skS.0 0 (skS.0 2 a_1) a_2) (skS.0 1 (skS.0 0 (skS.0 2 a_1) a_2) a_3)) True) % 14.16/14.43 Clause #124 (by superposition #[123, 109]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Or (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True) (Eq False True) % 14.16/14.43 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True % 14.16/14.43 Clause #126 (by superposition #[125, 120]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Or (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True) % 14.16/14.43 (Eq True False) % 14.16/14.43 Clause #127 (by clausification #[126]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True % 14.16/14.43 Clause #129 (by superposition #[127, 82]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Or (Eq True False) % 14.16/14.43 (Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True) % 14.16/14.43 (Eq (end_time (skS.0 0 (skS.0 2 a) a_1)) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2))) % 14.16/14.43 Clause #130 (by clausification #[119]): ∀ (a a_1 a_2 a_3 : Iota), % 14.16/14.43 Or (Eq (in_environment (skS.0 2 a) (skS.0 0 (skS.0 2 a_1) a_2)) False) % 14.16/14.43 (Eq (greater (skS.0 1 (skS.0 0 (skS.0 2 a_1) a_2) a_3) (critical_point (skS.0 0 (skS.0 2 a_1) a_2))) True) % 14.16/14.43 Clause #131 (by superposition #[130, 109]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Or (Eq (greater (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2) (critical_point (skS.0 0 (skS.0 2 a) a_1))) True) % 14.16/14.43 (Eq False True) % 14.16/14.43 Clause #132 (by clausification #[131]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Eq (greater (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2) (critical_point (skS.0 0 (skS.0 2 a) a_1))) True % 14.16/14.43 Clause #133 (by superposition #[132, 64]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True) % 14.16/14.43 (Or (Eq True False) % 14.16/14.43 (Or (Eq (environment (skS.0 0 (skS.0 2 a) a_1)) False) % 14.16/14.43 (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) False))) % 14.16/14.43 Clause #136 (by clausification #[111]): ∀ (a a_1 : Iota), % 14.16/14.43 Or (Eq (greater (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.16/14.43 (Eq (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) % 14.16/14.43 Clause #156 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), % 14.16/14.43 Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True) % 14.16/14.43 (Eq (end_time (skS.0 0 (skS.0 2 a) a_1)) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) % 14.16/14.43 Clause #157 (by superposition #[156, 69]): ∀ (a a_1 a_2 a_3 : Iota), % 14.16/14.43 Or (Eq (end_time (skS.0 0 (skS.0 2 a) a_1)) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) % 14.16/14.43 (Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) a_3) True) % 14.16/14.49 (Or (Eq True False) (Eq (greater (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2) a_3) False))) % 14.16/14.49 Clause #160 (by clausification #[133]): ∀ (a a_1 a_2 : Iota), % 14.16/14.49 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True) % 14.16/14.49 (Or (Eq (environment (skS.0 0 (skS.0 2 a) a_1)) False) % 14.16/14.49 (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) False)) % 14.16/14.49 Clause #161 (by forward demodulation #[160, 99]): ∀ (a a_1 a_2 : Iota), % 14.16/14.49 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True) % 14.16/14.49 (Or (Eq True False) (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) False)) % 14.16/14.49 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 : Iota), % 14.16/14.49 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True) % 14.16/14.49 (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) False) % 14.16/14.49 Clause #163 (by superposition #[162, 125]): ∀ (a a_1 a_2 : Iota), % 14.16/14.49 Or (Eq (selection_favors efficient_producers first_movers (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True) % 14.16/14.49 (Eq False True) % 14.16/14.49 Clause #164 (by clausification #[163]): ∀ (a a_1 a_2 : Iota), % 14.16/14.49 Eq (selection_favors efficient_producers first_movers (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) True % 14.16/14.49 Clause #166 (by clausification #[157]): ∀ (a a_1 a_2 a_3 : Iota), % 14.16/14.49 Or (Eq (end_time (skS.0 0 (skS.0 2 a) a_1)) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) % 14.16/14.49 (Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) a_3) True) % 14.16/14.49 (Eq (greater (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2) a_3) False)) % 14.16/14.49 Clause #167 (by superposition #[166, 132]): ∀ (a a_1 a_2 : Iota), % 14.16/14.49 Or (Eq (end_time (skS.0 0 (skS.0 2 a) a_1)) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) % 14.16/14.49 (Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) (critical_point (skS.0 0 (skS.0 2 a) a_1))) True) % 14.16/14.49 (Eq False True)) % 14.16/14.49 Clause #169 (by clausification #[167]): ∀ (a a_1 a_2 : Iota), % 14.16/14.49 Or (Eq (end_time (skS.0 0 (skS.0 2 a) a_1)) (skS.0 1 (skS.0 0 (skS.0 2 a) a_1) a_2)) % 14.16/14.49 (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) (critical_point (skS.0 0 (skS.0 2 a) a_1))) True) % 14.16/14.49 Clause #176 (by superposition #[169, 164]): ∀ (a a_1 : Iota), % 14.16/14.49 Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) (critical_point (skS.0 0 (skS.0 2 a) a_1))) True) % 14.16/14.49 (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.16/14.49 Clause #180 (by forward demodulation #[176, 106]): ∀ (a a_1 : Iota), % 14.16/14.49 Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) (critical_point (skS.0 0 (skS.0 2 a) a_1))) True) (Eq False True) % 14.16/14.49 Clause #181 (by clausification #[180]): ∀ (a a_1 : Iota), Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) (critical_point (skS.0 0 (skS.0 2 a) a_1))) True % 14.16/14.49 Clause #182 (by superposition #[181, 64]): ∀ (a a_1 : Iota), % 14.16/14.49 Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.16/14.49 (Or (Eq True False) % 14.16/14.49 (Or (Eq (environment (skS.0 0 (skS.0 2 a) a_1)) False) % 14.16/14.49 (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (end_time (skS.0 0 (skS.0 2 a) a_1))) False))) % 14.16/14.49 Clause #183 (by superposition #[181, 69]): ∀ (a a_1 a_2 : Iota), % 14.16/14.49 Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) a_2) True) % 14.16/14.49 (Or (Eq True False) (Eq (greater (critical_point (skS.0 0 (skS.0 2 a) a_1)) a_2) False)) % 14.16/14.49 Clause #184 (by superposition #[181, 77]): ∀ (a a_1 : Iota), % 14.16/14.49 Or (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (critical_point (skS.0 0 (skS.0 2 a) a_1))) True) % 14.16/14.49 (Eq True False) % 14.16/14.49 Clause #188 (by clausification #[184]): ∀ (a a_1 : Iota), % 14.16/14.49 Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (critical_point (skS.0 0 (skS.0 2 a) a_1))) True % 14.16/14.49 Clause #191 (by clausification #[183]): ∀ (a a_1 a_2 : Iota), % 14.16/14.49 Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) a_2) True) % 14.16/14.49 (Eq (greater (critical_point (skS.0 0 (skS.0 2 a) a_1)) a_2) False) % 14.16/14.49 Clause #192 (by superposition #[191, 136]): ∀ (a a_1 : Iota), % 14.16/14.49 Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.26/14.54 (Or (Eq False True) (Eq (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1)))) % 14.26/14.54 Clause #197 (by clausification #[192]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq (greater (end_time (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.26/14.54 (Eq (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) % 14.26/14.54 Clause #200 (by superposition #[197, 77]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) % 14.26/14.54 (Or (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.26/14.54 (Eq True False)) % 14.26/14.54 Clause #201 (by clausification #[200]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) % 14.26/14.54 (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.26/14.54 Clause #202 (by superposition #[201, 122]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) % 14.26/14.54 (Or (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (end_time (skS.0 0 (skS.0 2 a) a_1))) True) (Eq True False)) % 14.26/14.54 Clause #205 (by clausification #[202]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) % 14.26/14.54 (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (end_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.26/14.54 Clause #209 (by clausification #[182]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq (selection_favors efficient_producers first_movers (end_time (skS.0 0 (skS.0 2 a) a_1))) True) % 14.26/14.54 (Or (Eq (environment (skS.0 0 (skS.0 2 a) a_1)) False) % 14.26/14.54 (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (end_time (skS.0 0 (skS.0 2 a) a_1))) False)) % 14.26/14.54 Clause #210 (by forward demodulation #[209, 106]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq False True) % 14.26/14.54 (Or (Eq (environment (skS.0 0 (skS.0 2 a) a_1)) False) % 14.26/14.54 (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (end_time (skS.0 0 (skS.0 2 a) a_1))) False)) % 14.26/14.54 Clause #211 (by clausification #[210]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq (environment (skS.0 0 (skS.0 2 a) a_1)) False) % 14.26/14.54 (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (end_time (skS.0 0 (skS.0 2 a) a_1))) False) % 14.26/14.54 Clause #212 (by forward demodulation #[211, 99]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq True False) (Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (end_time (skS.0 0 (skS.0 2 a) a_1))) False) % 14.26/14.54 Clause #213 (by clausification #[212]): ∀ (a a_1 : Iota), Eq (in_environment (skS.0 0 (skS.0 2 a) a_1) (end_time (skS.0 0 (skS.0 2 a) a_1))) False % 14.26/14.54 Clause #214 (by backward demodulation #[213, 122]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq False True) % 14.26/14.54 (Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) False) % 14.26/14.54 Clause #215 (by superposition #[213, 205]): ∀ (a a_1 : Iota), % 14.26/14.54 Or (Eq (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) (Eq False True) % 14.26/14.54 Clause #216 (by clausification #[215]): ∀ (a a_1 : Iota), Eq (critical_point (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1)) % 14.26/14.54 Clause #227 (by backward demodulation #[216, 188]): ∀ (a a_1 : Iota), Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) True % 14.26/14.54 Clause #240 (by clausification #[214]): ∀ (a a_1 : Iota), % 14.26/14.54 Eq (greater_or_equal (end_time (skS.0 0 (skS.0 2 a) a_1)) (start_time (skS.0 0 (skS.0 2 a) a_1))) False % 14.26/14.54 Clause #241 (by superposition #[240, 227]): Eq False True % 14.26/14.54 Clause #242 (by clausification #[241]): False % 14.26/14.54 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------