%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] Gamma_1: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] Gamma_2: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] Gamma_3: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] Gamma_4: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) Gamma_5: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 5: ~(subpopulations(efficient_producers,first_movers,sk1,sk2)), [outcompetes( first_movers,efficient_producers,sk2)], ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) Gamma_6: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 5: ~(subpopulations(efficient_producers,first_movers,sk1,sk2)), [outcompetes( first_movers,efficient_producers,sk2)], ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) 6: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) Gamma_7: (move) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 5: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) 6: ~(subpopulations(efficient_producers,first_movers,sk1,sk2)), [outcompetes( first_movers,efficient_producers,sk2)], ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) Gamma_8: (resolve) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 5: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) 6: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) Gamma_9: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 5: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) 6: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) Gamma_10: (move) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) 5: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 6: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) Gamma_11: (resolve) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) 5: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))], ~( greater(zero,growth_rate(efficient_producers,sk2))), ~(greater_or_equal(growth_rate(first_movers,sk2),zero)), ~( environment(sk1)) 6: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) Gamma_12: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) 5: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), [~(environment(sk1))] 6: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) Gamma_13: (move) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), [~(environment(sk1))] 4: [environment(sk1)] 5: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) 6: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) Gamma_14: (resolve) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), [~(environment(sk1))] 4: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))], ~( greater(zero,growth_rate(efficient_producers,sk2))), ~(greater_or_equal(growth_rate(first_movers,sk2),zero)) Gamma_15: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), [~(environment(sk1))] 4: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), [~( greater_or_equal(growth_rate(first_movers,sk2),zero))] Gamma_16: (move) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), [~( greater_or_equal(growth_rate(first_movers,sk2),zero))] 3: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 4: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), [~(environment(sk1))] Gamma_17: (resolve) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), [~( greater_or_equal(growth_rate(first_movers,sk2),zero))] 3: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))], ~( greater(zero,growth_rate(efficient_producers,sk2))) Gamma_18: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), [~( greater_or_equal(growth_rate(first_movers,sk2),zero))] 3: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( greater(zero,growth_rate(efficient_producers,sk2)))] Gamma_19: (move) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( greater(zero,growth_rate(efficient_producers,sk2)))] 2: [greater(zero,growth_rate(efficient_producers,sk2))] 3: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), [~( greater_or_equal(growth_rate(first_movers,sk2),zero))] Gamma_20: (resolve) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( greater(zero,growth_rate(efficient_producers,sk2)))] 2: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))] Gamma_21: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( greater(zero,growth_rate(efficient_producers,sk2)))] 2: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))] Gamma_22: (move) 0: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))] 1: [subpopulations(first_movers,efficient_producers,sk1,sk2)] 2: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( greater(zero,growth_rate(efficient_producers,sk2)))] Gamma_23: (resolve) 0: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))] 1: [] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] Gamma_1: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] Gamma_2: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] Gamma_3: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] Gamma_4: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) Gamma_5: (extend-no-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 5: ~(subpopulations(efficient_producers,first_movers,sk1,sk2)), [outcompetes( first_movers,efficient_producers,sk2)], ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) Gamma_6: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 5: ~(subpopulations(efficient_producers,first_movers,sk1,sk2)), [outcompetes( first_movers,efficient_producers,sk2)], ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) 6: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) Gamma_7: (move) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 5: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) 6: ~(subpopulations(efficient_producers,first_movers,sk1,sk2)), [outcompetes( first_movers,efficient_producers,sk2)], ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) Gamma_8: (resolve) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 5: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) 6: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) Gamma_9: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 5: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) 6: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) Gamma_10: (move) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) 5: [subpopulations(efficient_producers,first_movers,sk1,sk2)], ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~( environment(sk1)) 6: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) Gamma_11: (resolve) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) 5: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))], ~( greater(zero,growth_rate(efficient_producers,sk2))), ~(greater_or_equal(growth_rate(first_movers,sk2),zero)), ~( environment(sk1)) 6: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) Gamma_12: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: [environment(sk1)] 4: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) 5: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), [~(environment(sk1))] 6: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) Gamma_13: (move) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), [~(environment(sk1))] 4: [environment(sk1)] 5: [~(subpopulations(efficient_producers,first_movers,sk1,sk2))], ~( subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), ~(environment(sk1)) 6: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( outcompetes(first_movers,efficient_producers,sk2))], ~(environment(sk1)) Gamma_14: (resolve) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), [~(environment(sk1))] 4: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))], ~( greater(zero,growth_rate(efficient_producers,sk2))), ~(greater_or_equal(growth_rate(first_movers,sk2),zero)) Gamma_15: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 3: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), [~(environment(sk1))] 4: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), [~( greater_or_equal(growth_rate(first_movers,sk2),zero))] Gamma_16: (move) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), [~( greater_or_equal(growth_rate(first_movers,sk2),zero))] 3: [greater_or_equal(growth_rate(first_movers,sk2),zero)] 4: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), ~( greater_or_equal(growth_rate(first_movers,sk2),zero)), [~(environment(sk1))] Gamma_17: (resolve) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), [~( greater_or_equal(growth_rate(first_movers,sk2),zero))] 3: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))], ~( greater(zero,growth_rate(efficient_producers,sk2))) Gamma_18: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: [greater(zero,growth_rate(efficient_producers,sk2))] 2: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), [~( greater_or_equal(growth_rate(first_movers,sk2),zero))] 3: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( greater(zero,growth_rate(efficient_producers,sk2)))] Gamma_19: (move) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( greater(zero,growth_rate(efficient_producers,sk2)))] 2: [greater(zero,growth_rate(efficient_producers,sk2))] 3: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), ~(greater(zero,growth_rate(efficient_producers,sk2))), [~( greater_or_equal(growth_rate(first_movers,sk2),zero))] Gamma_20: (resolve) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( greater(zero,growth_rate(efficient_producers,sk2)))] 2: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))] Gamma_21: (extend-conflict) 0: [subpopulations(first_movers,efficient_producers, sk1,sk2)] 1: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( greater(zero,growth_rate(efficient_producers,sk2)))] 2: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))] Gamma_22: (move) 0: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))] 1: [subpopulations(first_movers,efficient_producers,sk1,sk2)] 2: ~(subpopulations(first_movers,efficient_producers,sk1,sk2)), [~( greater(zero,growth_rate(efficient_producers,sk2)))] Gamma_23: (resolve) 0: [~(subpopulations(first_movers,efficient_producers,sk1,sk2))] 1: [] SZS status Unsatisfiable