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