%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT021+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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:15 AM UTC 2026 % Result : Theorem 9.15s 9.42s % Output : Proof 9.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT021+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : duper %s % 0.10/0.37 % Computer : n020.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Mon Sep 7 12:03:28 UTC 2026 % 0.10/0.37 % CPUTime : % 9.15/9.42 SZS status Theorem for theBenchmark.p % 9.15/9.42 SZS output start Proof for theBenchmark.p % 9.15/9.42 Clause #0 (by assumption #[]): Eq (∀ (E T : Iota), And (environment E) (subpopulations first_movers efficient_producers E T) → in_environment E T) True % 9.15/9.42 Clause #1 (by assumption #[]): Eq % 9.15/9.42 (∀ (E T : Iota), % 9.15/9.42 And (environment E) (subpopulations first_movers efficient_producers E T) → % 9.15/9.42 greater (number_of_organizations E T) zero) % 9.15/9.42 True % 9.15/9.42 Clause #2 (by assumption #[]): Eq (∀ (X : Iota), increases X → Not (decreases X)) True % 9.15/9.42 Clause #4 (by assumption #[]): Eq % 9.15/9.42 (∀ (E T : Iota), % 9.15/9.42 And (And (environment E) (in_environment E T)) (greater (number_of_organizations E T) zero) → % 9.15/9.42 And (greater (equilibrium E) T → decreases (resources E T)) % 9.15/9.42 (Not (greater (equilibrium E) T) → constant (resources E T))) % 9.15/9.42 True % 9.15/9.42 Clause #5 (by assumption #[]): Eq % 9.15/9.42 (∀ (E T : Iota), % 9.15/9.42 And (environment E) (subpopulations first_movers efficient_producers E T) → % 9.15/9.42 And % 9.15/9.42 (decreases (resources E T) → % 9.15/9.42 increases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T))) % 9.15/9.42 (constant (resources E T) → % 9.15/9.42 Not (decreases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T))))) % 9.15/9.42 True % 9.15/9.42 Clause #6 (by assumption #[]): Eq % 9.15/9.42 (Not % 9.15/9.42 (∀ (E T : Iota), % 9.15/9.42 And (environment E) (subpopulations first_movers efficient_producers E T) → % 9.15/9.42 Not (decreases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T))))) % 9.15/9.42 True % 9.15/9.42 Clause #7 (by clausification #[2]): ∀ (a : Iota), Eq (increases a → Not (decreases a)) True % 9.15/9.42 Clause #8 (by clausification #[7]): ∀ (a : Iota), Or (Eq (increases a) False) (Eq (Not (decreases a)) True) % 9.15/9.42 Clause #9 (by clausification #[8]): ∀ (a : Iota), Or (Eq (increases a) False) (Eq (decreases a) False) % 9.15/9.42 Clause #10 (by clausification #[0]): ∀ (a : Iota), % 9.15/9.42 Eq (∀ (T : Iota), And (environment a) (subpopulations first_movers efficient_producers a T) → in_environment a T) True % 9.15/9.42 Clause #11 (by clausification #[10]): ∀ (a a_1 : Iota), % 9.15/9.42 Eq (And (environment a) (subpopulations first_movers efficient_producers a a_1) → in_environment a a_1) True % 9.15/9.42 Clause #12 (by clausification #[11]): ∀ (a a_1 : Iota), % 9.15/9.42 Or (Eq (And (environment a) (subpopulations first_movers efficient_producers a a_1)) False) % 9.15/9.42 (Eq (in_environment a a_1) True) % 9.15/9.42 Clause #13 (by clausification #[12]): ∀ (a a_1 : Iota), % 9.15/9.42 Or (Eq (in_environment a a_1) True) % 9.15/9.42 (Or (Eq (environment a) False) (Eq (subpopulations first_movers efficient_producers a a_1) False)) % 9.15/9.42 Clause #14 (by clausification #[1]): ∀ (a : Iota), % 9.15/9.42 Eq % 9.15/9.42 (∀ (T : Iota), % 9.15/9.42 And (environment a) (subpopulations first_movers efficient_producers a T) → % 9.15/9.42 greater (number_of_organizations a T) zero) % 9.15/9.42 True % 9.15/9.42 Clause #15 (by clausification #[14]): ∀ (a a_1 : Iota), % 9.15/9.42 Eq % 9.15/9.42 (And (environment a) (subpopulations first_movers efficient_producers a a_1) → % 9.15/9.42 greater (number_of_organizations a a_1) zero) % 9.15/9.42 True % 9.15/9.42 Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota), % 9.15/9.42 Or (Eq (And (environment a) (subpopulations first_movers efficient_producers a a_1)) False) % 9.15/9.42 (Eq (greater (number_of_organizations a a_1) zero) True) % 9.15/9.42 Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota), % 9.15/9.42 Or (Eq (greater (number_of_organizations a a_1) zero) True) % 9.15/9.42 (Or (Eq (environment a) False) (Eq (subpopulations first_movers efficient_producers a a_1) False)) % 9.15/9.42 Clause #23 (by clausification #[6]): Eq % 9.15/9.42 (∀ (E T : Iota), % 9.15/9.42 And (environment E) (subpopulations first_movers efficient_producers E T) → % 9.15/9.42 Not (decreases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T)))) % 9.15/9.42 False % 9.15/9.42 Clause #24 (by clausification #[23]): ∀ (a : Iota), % 9.15/9.42 Eq % 9.15/9.42 (Not % 9.15/9.42 (∀ (T : Iota), % 9.15/9.42 And (environment (skS.0 0 a)) (subpopulations first_movers efficient_producers (skS.0 0 a) T) → % 9.15/9.42 Not (decreases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T))))) % 9.15/9.42 True % 9.15/9.42 Clause #25 (by clausification #[24]): ∀ (a : Iota), % 9.15/9.42 Eq % 9.15/9.46 (∀ (T : Iota), % 9.15/9.46 And (environment (skS.0 0 a)) (subpopulations first_movers efficient_producers (skS.0 0 a) T) → % 9.15/9.46 Not (decreases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T)))) % 9.15/9.46 False % 9.15/9.46 Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota), % 9.15/9.46 Eq % 9.15/9.46 (Not % 9.15/9.46 (And (environment (skS.0 0 a)) (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) → % 9.15/9.46 Not % 9.15/9.46 (decreases % 9.15/9.46 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.15/9.46 (disbanding_rate efficient_producers (skS.0 1 a a_1)))))) % 9.15/9.46 True % 9.15/9.46 Clause #27 (by clausification #[26]): ∀ (a a_1 : Iota), % 9.15/9.46 Eq % 9.15/9.46 (And (environment (skS.0 0 a)) (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) → % 9.15/9.46 Not % 9.15/9.46 (decreases % 9.15/9.46 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.15/9.46 (disbanding_rate efficient_producers (skS.0 1 a a_1))))) % 9.15/9.46 False % 9.15/9.46 Clause #28 (by clausification #[27]): ∀ (a a_1 : Iota), % 9.15/9.46 Eq (And (environment (skS.0 0 a)) (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1))) True % 9.15/9.46 Clause #29 (by clausification #[27]): ∀ (a a_1 : Iota), % 9.15/9.46 Eq % 9.15/9.46 (Not % 9.15/9.46 (decreases % 9.15/9.46 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.15/9.46 (disbanding_rate efficient_producers (skS.0 1 a a_1))))) % 9.15/9.46 False % 9.15/9.46 Clause #30 (by clausification #[28]): ∀ (a a_1 : Iota), Eq (subpopulations first_movers efficient_producers (skS.0 0 a) (skS.0 1 a a_1)) True % 9.15/9.46 Clause #31 (by clausification #[28]): ∀ (a : Iota), Eq (environment (skS.0 0 a)) True % 9.15/9.46 Clause #32 (by clausification #[4]): ∀ (a : Iota), % 9.15/9.46 Eq % 9.15/9.46 (∀ (T : Iota), % 9.15/9.46 And (And (environment a) (in_environment a T)) (greater (number_of_organizations a T) zero) → % 9.15/9.46 And (greater (equilibrium a) T → decreases (resources a T)) % 9.15/9.46 (Not (greater (equilibrium a) T) → constant (resources a T))) % 9.15/9.46 True % 9.15/9.46 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), % 9.15/9.46 Eq % 9.15/9.46 (And (And (environment a) (in_environment a a_1)) (greater (number_of_organizations a a_1) zero) → % 9.15/9.46 And (greater (equilibrium a) a_1 → decreases (resources a a_1)) % 9.15/9.46 (Not (greater (equilibrium a) a_1) → constant (resources a a_1))) % 9.15/9.46 True % 9.15/9.46 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), % 9.15/9.46 Or (Eq (And (And (environment a) (in_environment a a_1)) (greater (number_of_organizations a a_1) zero)) False) % 9.15/9.46 (Eq % 9.15/9.46 (And (greater (equilibrium a) a_1 → decreases (resources a a_1)) % 9.15/9.46 (Not (greater (equilibrium a) a_1) → constant (resources a a_1))) % 9.15/9.46 True) % 9.15/9.46 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), % 9.15/9.46 Or % 9.15/9.46 (Eq % 9.15/9.46 (And (greater (equilibrium a) a_1 → decreases (resources a a_1)) % 9.15/9.46 (Not (greater (equilibrium a) a_1) → constant (resources a a_1))) % 9.15/9.46 True) % 9.15/9.46 (Or (Eq (And (environment a) (in_environment a a_1)) False) % 9.15/9.46 (Eq (greater (number_of_organizations a a_1) zero) False)) % 9.15/9.46 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), % 9.15/9.46 Or (Eq (And (environment a) (in_environment a a_1)) False) % 9.15/9.46 (Or (Eq (greater (number_of_organizations a a_1) zero) False) % 9.15/9.46 (Eq (Not (greater (equilibrium a) a_1) → constant (resources a a_1)) True)) % 9.15/9.46 Clause #37 (by clausification #[35]): ∀ (a a_1 : Iota), % 9.15/9.46 Or (Eq (And (environment a) (in_environment a a_1)) False) % 9.15/9.46 (Or (Eq (greater (number_of_organizations a a_1) zero) False) % 9.15/9.46 (Eq (greater (equilibrium a) a_1 → decreases (resources a a_1)) True)) % 9.15/9.46 Clause #38 (by clausification #[36]): ∀ (a a_1 : Iota), % 9.15/9.46 Or (Eq (greater (number_of_organizations a a_1) zero) False) % 9.15/9.46 (Or (Eq (Not (greater (equilibrium a) a_1) → constant (resources a a_1)) True) % 9.15/9.46 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False))) % 9.15/9.46 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), % 9.15/9.46 Or (Eq (greater (number_of_organizations a a_1) zero) False) % 9.15/9.46 (Or (Eq (environment a) False) % 9.15/9.46 (Or (Eq (in_environment a a_1) False) % 9.15/9.46 (Or (Eq (Not (greater (equilibrium a) a_1)) False) (Eq (constant (resources a a_1)) True)))) % 9.25/9.51 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), % 9.25/9.51 Or (Eq (greater (number_of_organizations a a_1) zero) False) % 9.25/9.51 (Or (Eq (environment a) False) % 9.25/9.51 (Or (Eq (in_environment a a_1) False) % 9.25/9.51 (Or (Eq (constant (resources a a_1)) True) (Eq (greater (equilibrium a) a_1) True)))) % 9.25/9.51 Clause #41 (by superposition #[31, 13]): ∀ (a a_1 : Iota), % 9.25/9.51 Or (Eq (in_environment (skS.0 0 a) a_1) True) % 9.25/9.51 (Or (Eq True False) (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False)) % 9.25/9.51 Clause #42 (by superposition #[31, 17]): ∀ (a a_1 : Iota), % 9.25/9.51 Or (Eq (greater (number_of_organizations (skS.0 0 a) a_1) zero) True) % 9.25/9.51 (Or (Eq True False) (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False)) % 9.25/9.51 Clause #43 (by clausification #[37]): ∀ (a a_1 : Iota), % 9.25/9.51 Or (Eq (greater (number_of_organizations a a_1) zero) False) % 9.25/9.51 (Or (Eq (greater (equilibrium a) a_1 → decreases (resources a a_1)) True) % 9.25/9.51 (Or (Eq (environment a) False) (Eq (in_environment a a_1) False))) % 9.25/9.51 Clause #44 (by clausification #[43]): ∀ (a a_1 : Iota), % 9.25/9.51 Or (Eq (greater (number_of_organizations a a_1) zero) False) % 9.25/9.51 (Or (Eq (environment a) False) % 9.25/9.51 (Or (Eq (in_environment a a_1) False) % 9.25/9.51 (Or (Eq (greater (equilibrium a) a_1) False) (Eq (decreases (resources a a_1)) True)))) % 9.25/9.51 Clause #45 (by clausification #[41]): ∀ (a a_1 : Iota), % 9.25/9.51 Or (Eq (in_environment (skS.0 0 a) a_1) True) % 9.25/9.51 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 9.25/9.51 Clause #46 (by superposition #[45, 30]): ∀ (a a_1 : Iota), Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq False True) % 9.25/9.51 Clause #47 (by clausification #[46]): ∀ (a a_1 : Iota), Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) True % 9.25/9.51 Clause #48 (by clausification #[42]): ∀ (a a_1 : Iota), % 9.25/9.51 Or (Eq (greater (number_of_organizations (skS.0 0 a) a_1) zero) True) % 9.25/9.51 (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 9.25/9.51 Clause #49 (by superposition #[48, 30]): ∀ (a a_1 : Iota), Or (Eq (greater (number_of_organizations (skS.0 0 a) (skS.0 1 a a_1)) zero) True) (Eq False True) % 9.25/9.51 Clause #50 (by clausification #[5]): ∀ (a : Iota), % 9.25/9.51 Eq % 9.25/9.51 (∀ (T : Iota), % 9.25/9.51 And (environment a) (subpopulations first_movers efficient_producers a T) → % 9.25/9.51 And % 9.25/9.51 (decreases (resources a T) → % 9.25/9.51 increases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T))) % 9.25/9.51 (constant (resources a T) → % 9.25/9.51 Not (decreases (difference (disbanding_rate first_movers T) (disbanding_rate efficient_producers T))))) % 9.25/9.51 True % 9.25/9.51 Clause #51 (by clausification #[50]): ∀ (a a_1 : Iota), % 9.25/9.51 Eq % 9.25/9.51 (And (environment a) (subpopulations first_movers efficient_producers a a_1) → % 9.25/9.51 And % 9.25/9.51 (decreases (resources a a_1) → % 9.25/9.51 increases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) % 9.25/9.51 (constant (resources a a_1) → % 9.25/9.51 Not (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))))) % 9.25/9.51 True % 9.25/9.51 Clause #52 (by clausification #[51]): ∀ (a a_1 : Iota), % 9.25/9.51 Or (Eq (And (environment a) (subpopulations first_movers efficient_producers a a_1)) False) % 9.25/9.51 (Eq % 9.25/9.51 (And % 9.25/9.51 (decreases (resources a a_1) → % 9.25/9.51 increases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) % 9.25/9.51 (constant (resources a a_1) → % 9.25/9.51 Not (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))))) % 9.25/9.51 True) % 9.25/9.51 Clause #53 (by clausification #[52]): ∀ (a a_1 : Iota), % 9.25/9.51 Or % 9.25/9.51 (Eq % 9.25/9.51 (And % 9.25/9.51 (decreases (resources a a_1) → % 9.25/9.51 increases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) % 9.25/9.51 (constant (resources a a_1) → % 9.25/9.51 Not (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))))) % 9.25/9.51 True) % 9.25/9.51 (Or (Eq (environment a) False) (Eq (subpopulations first_movers efficient_producers a a_1) False)) % 9.25/9.51 Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq (environment a) False) % 9.25/9.55 (Or (Eq (subpopulations first_movers efficient_producers a a_1) False) % 9.25/9.55 (Eq % 9.25/9.55 (constant (resources a a_1) → % 9.25/9.55 Not (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1)))) % 9.25/9.55 True)) % 9.25/9.55 Clause #55 (by clausification #[53]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq (environment a) False) % 9.25/9.55 (Or (Eq (subpopulations first_movers efficient_producers a a_1) False) % 9.25/9.55 (Eq % 9.25/9.55 (decreases (resources a a_1) → % 9.25/9.55 increases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) % 9.25/9.55 True)) % 9.25/9.55 Clause #56 (by clausification #[54]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq (environment a) False) % 9.25/9.55 (Or (Eq (subpopulations first_movers efficient_producers a a_1) False) % 9.25/9.55 (Or (Eq (constant (resources a a_1)) False) % 9.25/9.55 (Eq (Not (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1)))) % 9.25/9.55 True))) % 9.25/9.55 Clause #57 (by clausification #[56]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq (environment a) False) % 9.25/9.55 (Or (Eq (subpopulations first_movers efficient_producers a a_1) False) % 9.25/9.55 (Or (Eq (constant (resources a a_1)) False) % 9.25/9.55 (Eq (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) % 9.25/9.55 False))) % 9.25/9.55 Clause #58 (by superposition #[57, 31]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 9.25/9.55 (Or (Eq (constant (resources (skS.0 0 a) a_1)) False) % 9.25/9.55 (Or % 9.25/9.55 (Eq (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) False) % 9.25/9.55 (Eq False True))) % 9.25/9.55 Clause #59 (by clausification #[55]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq (environment a) False) % 9.25/9.55 (Or (Eq (subpopulations first_movers efficient_producers a a_1) False) % 9.25/9.55 (Or (Eq (decreases (resources a a_1)) False) % 9.25/9.55 (Eq (increases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) % 9.25/9.55 True))) % 9.25/9.55 Clause #60 (by superposition #[59, 31]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 9.25/9.55 (Or (Eq (decreases (resources (skS.0 0 a) a_1)) False) % 9.25/9.55 (Or % 9.25/9.55 (Eq (increases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) True) % 9.25/9.55 (Eq False True))) % 9.25/9.55 Clause #61 (by clausification #[49]): ∀ (a a_1 : Iota), Eq (greater (number_of_organizations (skS.0 0 a) (skS.0 1 a a_1)) zero) True % 9.25/9.55 Clause #62 (by superposition #[61, 40]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq True False) % 9.25/9.55 (Or (Eq (environment (skS.0 0 a)) False) % 9.25/9.55 (Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False) % 9.25/9.55 (Or (Eq (constant (resources (skS.0 0 a) (skS.0 1 a a_1))) True) % 9.25/9.55 (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) True)))) % 9.25/9.55 Clause #63 (by superposition #[61, 44]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq True False) % 9.25/9.55 (Or (Eq (environment (skS.0 0 a)) False) % 9.25/9.55 (Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False) % 9.25/9.55 (Or (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) False) % 9.25/9.55 (Eq (decreases (resources (skS.0 0 a) (skS.0 1 a a_1))) True)))) % 9.25/9.55 Clause #64 (by clausification #[29]): ∀ (a a_1 : Iota), % 9.25/9.55 Eq % 9.25/9.55 (decreases % 9.25/9.55 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.25/9.55 True % 9.25/9.55 Clause #65 (by clausification #[58]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 9.25/9.55 (Or (Eq (constant (resources (skS.0 0 a) a_1)) False) % 9.25/9.55 (Eq (decreases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) False)) % 9.25/9.55 Clause #66 (by superposition #[65, 30]): ∀ (a a_1 : Iota), % 9.25/9.55 Or (Eq (constant (resources (skS.0 0 a) (skS.0 1 a a_1))) False) % 9.25/9.55 (Or % 9.25/9.55 (Eq % 9.25/9.55 (decreases % 9.25/9.55 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.25/9.55 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.25/9.55 False) % 9.35/9.61 (Eq False True)) % 9.35/9.61 Clause #67 (by clausification #[60]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq (subpopulations first_movers efficient_producers (skS.0 0 a) a_1) False) % 9.35/9.61 (Or (Eq (decreases (resources (skS.0 0 a) a_1)) False) % 9.35/9.61 (Eq (increases (difference (disbanding_rate first_movers a_1) (disbanding_rate efficient_producers a_1))) True)) % 9.35/9.61 Clause #68 (by superposition #[67, 30]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq (decreases (resources (skS.0 0 a) (skS.0 1 a a_1))) False) % 9.35/9.61 (Or % 9.35/9.61 (Eq % 9.35/9.61 (increases % 9.35/9.61 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.35/9.61 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.35/9.61 True) % 9.35/9.61 (Eq False True)) % 9.35/9.61 Clause #69 (by clausification #[62]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq (environment (skS.0 0 a)) False) % 9.35/9.61 (Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False) % 9.35/9.61 (Or (Eq (constant (resources (skS.0 0 a) (skS.0 1 a a_1))) True) % 9.35/9.61 (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) True))) % 9.35/9.61 Clause #70 (by forward demodulation #[69, 31]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq True False) % 9.35/9.61 (Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False) % 9.35/9.61 (Or (Eq (constant (resources (skS.0 0 a) (skS.0 1 a a_1))) True) % 9.35/9.61 (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) True))) % 9.35/9.61 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False) % 9.35/9.61 (Or (Eq (constant (resources (skS.0 0 a) (skS.0 1 a a_1))) True) % 9.35/9.61 (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) True)) % 9.35/9.61 Clause #72 (by forward demodulation #[71, 47]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq True False) % 9.35/9.61 (Or (Eq (constant (resources (skS.0 0 a) (skS.0 1 a a_1))) True) % 9.35/9.61 (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) True)) % 9.35/9.61 Clause #73 (by clausification #[72]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq (constant (resources (skS.0 0 a) (skS.0 1 a a_1))) True) % 9.35/9.61 (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) True) % 9.35/9.61 Clause #74 (by clausification #[66]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq (constant (resources (skS.0 0 a) (skS.0 1 a a_1))) False) % 9.35/9.61 (Eq % 9.35/9.61 (decreases % 9.35/9.61 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.35/9.61 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.35/9.61 False) % 9.35/9.61 Clause #75 (by superposition #[74, 73]): ∀ (a a_1 : Iota), % 9.35/9.61 Or % 9.35/9.61 (Eq % 9.35/9.61 (decreases % 9.35/9.61 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.35/9.61 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.35/9.61 False) % 9.35/9.61 (Or (Eq False True) (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) True)) % 9.35/9.61 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), % 9.35/9.61 Or % 9.35/9.61 (Eq % 9.35/9.61 (decreases % 9.35/9.61 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.35/9.61 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.35/9.61 False) % 9.35/9.61 (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) True) % 9.35/9.61 Clause #77 (by superposition #[76, 64]): ∀ (a a_1 : Iota), Or (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) True) (Eq False True) % 9.35/9.61 Clause #78 (by clausification #[77]): ∀ (a a_1 : Iota), Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) True % 9.35/9.61 Clause #81 (by clausification #[63]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq (environment (skS.0 0 a)) False) % 9.35/9.61 (Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False) % 9.35/9.61 (Or (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) False) % 9.35/9.61 (Eq (decreases (resources (skS.0 0 a) (skS.0 1 a a_1))) True))) % 9.35/9.61 Clause #82 (by forward demodulation #[81, 31]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq True False) % 9.35/9.61 (Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False) % 9.35/9.61 (Or (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) False) % 9.35/9.61 (Eq (decreases (resources (skS.0 0 a) (skS.0 1 a a_1))) True))) % 9.35/9.61 Clause #83 (by clausification #[82]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq (in_environment (skS.0 0 a) (skS.0 1 a a_1)) False) % 9.35/9.61 (Or (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) False) % 9.35/9.61 (Eq (decreases (resources (skS.0 0 a) (skS.0 1 a a_1))) True)) % 9.35/9.61 Clause #84 (by forward demodulation #[83, 47]): ∀ (a a_1 : Iota), % 9.35/9.61 Or (Eq True False) % 9.35/9.63 (Or (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) False) % 9.35/9.63 (Eq (decreases (resources (skS.0 0 a) (skS.0 1 a a_1))) True)) % 9.35/9.63 Clause #85 (by clausification #[84]): ∀ (a a_1 : Iota), % 9.35/9.63 Or (Eq (greater (equilibrium (skS.0 0 a)) (skS.0 1 a a_1)) False) % 9.35/9.63 (Eq (decreases (resources (skS.0 0 a) (skS.0 1 a a_1))) True) % 9.35/9.63 Clause #86 (by forward demodulation #[85, 78]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (decreases (resources (skS.0 0 a) (skS.0 1 a a_1))) True) % 9.35/9.63 Clause #87 (by clausification #[86]): ∀ (a a_1 : Iota), Eq (decreases (resources (skS.0 0 a) (skS.0 1 a a_1))) True % 9.35/9.63 Clause #88 (by clausification #[68]): ∀ (a a_1 : Iota), % 9.35/9.63 Or (Eq (decreases (resources (skS.0 0 a) (skS.0 1 a a_1))) False) % 9.35/9.63 (Eq % 9.35/9.63 (increases % 9.35/9.63 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.35/9.63 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.35/9.63 True) % 9.35/9.63 Clause #89 (by forward demodulation #[88, 87]): ∀ (a a_1 : Iota), % 9.35/9.63 Or (Eq True False) % 9.35/9.63 (Eq % 9.35/9.63 (increases % 9.35/9.63 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.35/9.63 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.35/9.63 True) % 9.35/9.63 Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota), % 9.35/9.63 Eq % 9.35/9.63 (increases % 9.35/9.63 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.35/9.63 True % 9.35/9.63 Clause #91 (by superposition #[90, 9]): ∀ (a a_1 : Iota), % 9.35/9.63 Or (Eq True False) % 9.35/9.63 (Eq % 9.35/9.63 (decreases % 9.35/9.63 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) % 9.35/9.63 (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.35/9.63 False) % 9.35/9.63 Clause #92 (by clausification #[91]): ∀ (a a_1 : Iota), % 9.35/9.63 Eq % 9.35/9.63 (decreases % 9.35/9.63 (difference (disbanding_rate first_movers (skS.0 1 a a_1)) (disbanding_rate efficient_producers (skS.0 1 a a_1)))) % 9.35/9.63 False % 9.35/9.63 Clause #93 (by superposition #[92, 64]): Eq False True % 9.35/9.63 Clause #94 (by clausification #[93]): False % 9.35/9.63 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------