%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 Gamma_1: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 Gamma_2: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 Gamma_3: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 Gamma_4: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 4: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [p_1] Gamma_5: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 4: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [p_1] 5: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [~(p_1)] Gamma_6: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 4: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [p_1] Gamma_7: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 4: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: [~(p_5)], ~(p_4), ~(p_3), ~(p_2) Gamma_8: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 4: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] Gamma_9: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 5: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [~(p_1)] Gamma_10: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: [~(p_5)], ~(p_4), ~(p_3), p_1 Gamma_11: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), [p_1] Gamma_12: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), [p_1] 5: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] Gamma_13: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] 5: ~(p_5), ~(p_4), ~(p_3), [p_1] Gamma_14: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] 5: [~(p_5)], ~(p_4), ~(p_3), p_2 Gamma_15: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] 5: ~(p_5), ~(p_4), ~(p_3), [p_2] Gamma_16: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] 5: [~(p_5)], ~(p_4), ~(p_3) Gamma_17: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] 5: ~(p_5), ~(p_4), [~(p_3)] Gamma_18: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_3], p_2, p_1 4: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 5: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] Gamma_19: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: [~(p_5)], ~(p_4), p_2, p_1 Gamma_20: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 Gamma_21: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 4: ~(p_5), ~(p_4), p_3, ~(p_2), [p_1] Gamma_22: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 4: ~(p_5), ~(p_4), p_3, ~(p_2), [p_1] 5: ~(p_5), ~(p_4), p_3, ~(p_2), [~(p_1)] Gamma_23: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 4: ~(p_5), ~(p_4), p_3, ~(p_2), [~(p_1)] 5: ~(p_5), ~(p_4), p_3, ~(p_2), [p_1] Gamma_24: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 4: ~(p_5), ~(p_4), p_3, ~(p_2), [~(p_1)] 5: [~(p_5)], ~(p_4), p_3, ~(p_2) Gamma_25: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 4: ~(p_5), ~(p_4), p_3, ~(p_2), [~(p_1)] 5: ~(p_5), ~(p_4), p_3, [~(p_2)] Gamma_26: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), [p_2], p_1 5: ~(p_5), ~(p_4), p_3, ~(p_2), [~(p_1)] Gamma_27: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: [~(p_5)], ~(p_4), p_3, p_1 Gamma_28: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, [p_1] Gamma_29: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, [p_1] 5: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] Gamma_30: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: ~(p_5), ~(p_4), p_3, [p_1] Gamma_31: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: [~(p_5)], ~(p_4), p_3, p_2 Gamma_32: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: ~(p_5), ~(p_4), p_3, [p_2] Gamma_33: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: [~(p_5)], ~(p_4), p_3 Gamma_34: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: ~(p_5), ~(p_4), [p_3] Gamma_35: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: [~(p_5)], ~(p_4) Gamma_36: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: ~(p_5), [~(p_4)] Gamma_37: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_4], p_3, p_2, p_1 3: ~(p_5), ~(p_4), [~(p_3)] 4: ~(p_5), ~(p_4), p_3, [~(p_2)] 5: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] Gamma_38: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: [~(p_5)], p_3, p_2, p_1 Gamma_39: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 Gamma_40: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 Gamma_41: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 4: ~(p_5), p_4, ~(p_3), ~(p_2), [p_1] Gamma_42: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 4: ~(p_5), p_4, ~(p_3), ~(p_2), [p_1] 5: ~(p_5), p_4, ~(p_3), ~(p_2), [~(p_1)] Gamma_43: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 4: ~(p_5), p_4, ~(p_3), ~(p_2), [~(p_1)] 5: ~(p_5), p_4, ~(p_3), ~(p_2), [p_1] Gamma_44: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 4: ~(p_5), p_4, ~(p_3), ~(p_2), [~(p_1)] 5: [~(p_5)], p_4, ~(p_3), ~(p_2) Gamma_45: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 4: ~(p_5), p_4, ~(p_3), ~(p_2), [~(p_1)] 5: ~(p_5), p_4, ~(p_3), [~(p_2)] Gamma_46: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), [p_2], p_1 5: ~(p_5), p_4, ~(p_3), ~(p_2), [~(p_1)] Gamma_47: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: [~(p_5)], p_4, ~(p_3), p_1 Gamma_48: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), [p_1] Gamma_49: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), [p_1] 5: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] Gamma_50: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] 5: ~(p_5), p_4, ~(p_3), [p_1] Gamma_51: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] 5: [~(p_5)], p_4, ~(p_3), p_2 Gamma_52: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] 5: ~(p_5), p_4, ~(p_3), [p_2] Gamma_53: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] 5: [~(p_5)], p_4, ~(p_3) Gamma_54: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] 5: ~(p_5), p_4, [~(p_3)] Gamma_55: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), [p_3], p_2, p_1 4: ~(p_5), p_4, ~(p_3), [~(p_2)] 5: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] Gamma_56: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: [~(p_5)], p_4, p_2, p_1 Gamma_57: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 Gamma_58: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 4: ~(p_5), p_4, p_3, ~(p_2), [p_1] Gamma_59: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 4: ~(p_5), p_4, p_3, ~(p_2), [p_1] 5: ~(p_5), p_4, p_3, ~(p_2), [~(p_1)] Gamma_60: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 4: ~(p_5), p_4, p_3, ~(p_2), [~(p_1)] 5: ~(p_5), p_4, p_3, ~(p_2), [p_1] Gamma_61: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 4: ~(p_5), p_4, p_3, ~(p_2), [~(p_1)] 5: [~(p_5)], p_4, p_3, ~(p_2) Gamma_62: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 4: ~(p_5), p_4, p_3, ~(p_2), [~(p_1)] 5: ~(p_5), p_4, p_3, [~(p_2)] Gamma_63: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, [p_2], p_1 5: ~(p_5), p_4, p_3, ~(p_2), [~(p_1)] Gamma_64: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: [~(p_5)], p_4, p_3, p_1 Gamma_65: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, [p_1] Gamma_66: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, [p_1] 5: ~(p_5), p_4, p_3, p_2, [~(p_1)] Gamma_67: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: ~(p_5), p_4, p_3, [p_1] Gamma_68: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: [~(p_5)], p_4, p_3, p_2 Gamma_69: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: ~(p_5), p_4, p_3, [p_2] Gamma_70: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: [~(p_5)], p_4, p_3 Gamma_71: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: ~(p_5), p_4, [p_3] Gamma_72: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: [~(p_5)], p_4 Gamma_73: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: ~(p_5), [p_4] Gamma_74: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: [~(p_5)] Gamma_75: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: [~(p_5)] Gamma_76: (move) 0: [~(p_5)] 1: [p_5], p_4, p_3, p_2, p_1 2: ~(p_5), [~(p_4)] 3: ~(p_5), p_4, [~(p_3)] 4: ~(p_5), p_4, p_3, [~(p_2)] 5: ~(p_5), p_4, p_3, p_2, [~(p_1)] Gamma_77: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 Gamma_78: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 Gamma_79: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 Gamma_80: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 Gamma_81: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 4: p_5, ~(p_4), ~(p_3), ~(p_2), [p_1] Gamma_82: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 4: p_5, ~(p_4), ~(p_3), ~(p_2), [p_1] 5: p_5, ~(p_4), ~(p_3), ~(p_2), [~(p_1)] Gamma_83: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 4: p_5, ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: p_5, ~(p_4), ~(p_3), ~(p_2), [p_1] Gamma_84: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 4: p_5, ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: [p_5], ~(p_4), ~(p_3), ~(p_2) Gamma_85: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 4: p_5, ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: p_5, ~(p_4), ~(p_3), [~(p_2)] Gamma_86: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), [p_2], p_1 5: p_5, ~(p_4), ~(p_3), ~(p_2), [~(p_1)] Gamma_87: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: [p_5], ~(p_4), ~(p_3), p_1 Gamma_88: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), [p_1] Gamma_89: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), [p_1] 5: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] Gamma_90: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] 5: p_5, ~(p_4), ~(p_3), [p_1] Gamma_91: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] 5: [p_5], ~(p_4), ~(p_3), p_2 Gamma_92: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] 5: p_5, ~(p_4), ~(p_3), [p_2] Gamma_93: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] 5: [p_5], ~(p_4), ~(p_3) Gamma_94: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] 5: p_5, ~(p_4), [~(p_3)] Gamma_95: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_3], p_2, p_1 4: p_5, ~(p_4), ~(p_3), [~(p_2)] 5: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] Gamma_96: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: [p_5], ~(p_4), p_2, p_1 Gamma_97: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 Gamma_98: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 4: p_5, ~(p_4), p_3, ~(p_2), [p_1] Gamma_99: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 4: p_5, ~(p_4), p_3, ~(p_2), [p_1] 5: p_5, ~(p_4), p_3, ~(p_2), [~(p_1)] Gamma_100: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 4: p_5, ~(p_4), p_3, ~(p_2), [~(p_1)] 5: p_5, ~(p_4), p_3, ~(p_2), [p_1] Gamma_101: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 4: p_5, ~(p_4), p_3, ~(p_2), [~(p_1)] 5: [p_5], ~(p_4), p_3, ~(p_2) Gamma_102: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 4: p_5, ~(p_4), p_3, ~(p_2), [~(p_1)] 5: p_5, ~(p_4), p_3, [~(p_2)] Gamma_103: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), [p_2], p_1 5: p_5, ~(p_4), p_3, ~(p_2), [~(p_1)] Gamma_104: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: [p_5], ~(p_4), p_3, p_1 Gamma_105: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, [p_1] Gamma_106: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, [p_1] 5: p_5, ~(p_4), p_3, p_2, [~(p_1)] Gamma_107: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: p_5, ~(p_4), p_3, [p_1] Gamma_108: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: [p_5], ~(p_4), p_3, p_2 Gamma_109: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: p_5, ~(p_4), p_3, [p_2] Gamma_110: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: [p_5], ~(p_4), p_3 Gamma_111: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: p_5, ~(p_4), [p_3] Gamma_112: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: [p_5], ~(p_4) Gamma_113: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: p_5, [~(p_4)] Gamma_114: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: [p_4], p_3, p_2, p_1 3: p_5, ~(p_4), [~(p_3)] 4: p_5, ~(p_4), p_3, [~(p_2)] 5: p_5, ~(p_4), p_3, p_2, [~(p_1)] Gamma_115: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 Gamma_116: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 Gamma_117: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 Gamma_118: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 4: p_5, p_4, ~(p_3), ~(p_2), [p_1] Gamma_119: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 4: p_5, p_4, ~(p_3), ~(p_2), [p_1] 5: p_5, p_4, ~(p_3), ~(p_2), [~(p_1)] Gamma_120: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 4: p_5, p_4, ~(p_3), ~(p_2), [~(p_1)] 5: p_5, p_4, ~(p_3), ~(p_2), [p_1] Gamma_121: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 4: p_5, p_4, ~(p_3), ~(p_2), [~(p_1)] 5: [p_5], p_4, ~(p_3), ~(p_2) Gamma_122: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 4: p_5, p_4, ~(p_3), ~(p_2), [~(p_1)] 5: p_5, p_4, ~(p_3), [~(p_2)] Gamma_123: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), [p_2], p_1 5: p_5, p_4, ~(p_3), ~(p_2), [~(p_1)] Gamma_124: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: [p_5], p_4, ~(p_3), p_1 Gamma_125: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), [p_1] Gamma_126: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), [p_1] 5: p_5, p_4, ~(p_3), p_2, [~(p_1)] Gamma_127: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), p_2, [~(p_1)] 5: p_5, p_4, ~(p_3), [p_1] Gamma_128: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), p_2, [~(p_1)] 5: [p_5], p_4, ~(p_3), p_2 Gamma_129: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), p_2, [~(p_1)] 5: p_5, p_4, ~(p_3), [p_2] Gamma_130: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), p_2, [~(p_1)] 5: [p_5], p_4, ~(p_3) Gamma_131: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), p_2, [~(p_1)] 5: p_5, p_4, [~(p_3)] Gamma_132: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, [p_3], p_2, p_1 4: p_5, p_4, ~(p_3), [~(p_2)] 5: p_5, p_4, ~(p_3), p_2, [~(p_1)] Gamma_133: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: [p_5], p_4, p_2, p_1 Gamma_134: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 Gamma_135: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 4: p_5, p_4, p_3, ~(p_2), [p_1] Gamma_136: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 4: p_5, p_4, p_3, ~(p_2), [p_1] 5: p_5, p_4, p_3, ~(p_2), [~(p_1)] Gamma_137: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 4: p_5, p_4, p_3, ~(p_2), [~(p_1)] 5: p_5, p_4, p_3, ~(p_2), [p_1] Gamma_138: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 4: p_5, p_4, p_3, ~(p_2), [~(p_1)] 5: [p_5], p_4, p_3, ~(p_2) Gamma_139: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 4: p_5, p_4, p_3, ~(p_2), [~(p_1)] 5: p_5, p_4, p_3, [~(p_2)] Gamma_140: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, [p_2], p_1 5: p_5, p_4, p_3, ~(p_2), [~(p_1)] Gamma_141: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: [p_5], p_4, p_3, p_1 Gamma_142: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, [p_1] Gamma_143: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, [p_1] 5: p_5, p_4, p_3, p_2, [~(p_1)] Gamma_144: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: p_5, p_4, p_3, [p_1] Gamma_145: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [p_5], p_4, p_3, p_2 Gamma_146: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: p_5, p_4, p_3, [p_2] Gamma_147: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [p_5], p_4, p_3 Gamma_148: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: p_5, p_4, [p_3] Gamma_149: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [p_5], p_4 Gamma_150: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: p_5, [p_4] Gamma_151: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [p_5] Gamma_152: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [p_5] Gamma_153: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 Gamma_1: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 Gamma_2: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 Gamma_3: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 Gamma_4: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 4: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [p_1] Gamma_5: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 4: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [p_1] 5: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [~(p_1)] Gamma_6: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 4: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [p_1] Gamma_7: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 4: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: [~(p_5)], ~(p_4), ~(p_3), ~(p_2) Gamma_8: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 4: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] Gamma_9: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), [p_2], p_1 5: ~(p_5), ~(p_4), ~(p_3), ~(p_2), [~(p_1)] Gamma_10: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: [~(p_5)], ~(p_4), ~(p_3), p_1 Gamma_11: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), [p_1] Gamma_12: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), [p_1] 5: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] Gamma_13: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] 5: ~(p_5), ~(p_4), ~(p_3), [p_1] Gamma_14: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] 5: [~(p_5)], ~(p_4), ~(p_3), p_2 Gamma_15: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] 5: ~(p_5), ~(p_4), ~(p_3), [p_2] Gamma_16: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] 5: [~(p_5)], ~(p_4), ~(p_3) Gamma_17: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [p_3], p_2, p_1 3: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 4: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] 5: ~(p_5), ~(p_4), [~(p_3)] Gamma_18: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_3], p_2, p_1 4: ~(p_5), ~(p_4), ~(p_3), [~(p_2)] 5: ~(p_5), ~(p_4), ~(p_3), p_2, [~(p_1)] Gamma_19: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: [~(p_5)], ~(p_4), p_2, p_1 Gamma_20: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 Gamma_21: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 4: ~(p_5), ~(p_4), p_3, ~(p_2), [p_1] Gamma_22: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 4: ~(p_5), ~(p_4), p_3, ~(p_2), [p_1] 5: ~(p_5), ~(p_4), p_3, ~(p_2), [~(p_1)] Gamma_23: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 4: ~(p_5), ~(p_4), p_3, ~(p_2), [~(p_1)] 5: ~(p_5), ~(p_4), p_3, ~(p_2), [p_1] Gamma_24: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 4: ~(p_5), ~(p_4), p_3, ~(p_2), [~(p_1)] 5: [~(p_5)], ~(p_4), p_3, ~(p_2) Gamma_25: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), [p_2], p_1 4: ~(p_5), ~(p_4), p_3, ~(p_2), [~(p_1)] 5: ~(p_5), ~(p_4), p_3, [~(p_2)] Gamma_26: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), [p_2], p_1 5: ~(p_5), ~(p_4), p_3, ~(p_2), [~(p_1)] Gamma_27: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: [~(p_5)], ~(p_4), p_3, p_1 Gamma_28: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, [p_1] Gamma_29: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, [p_1] 5: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] Gamma_30: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: ~(p_5), ~(p_4), p_3, [p_1] Gamma_31: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: [~(p_5)], ~(p_4), p_3, p_2 Gamma_32: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: ~(p_5), ~(p_4), p_3, [p_2] Gamma_33: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: [~(p_5)], ~(p_4), p_3 Gamma_34: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: ~(p_5), ~(p_4), [p_3] Gamma_35: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: [~(p_5)], ~(p_4) Gamma_36: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [p_4], p_3, p_2, p_1 2: ~(p_5), ~(p_4), [~(p_3)] 3: ~(p_5), ~(p_4), p_3, [~(p_2)] 4: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] 5: ~(p_5), [~(p_4)] Gamma_37: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_4], p_3, p_2, p_1 3: ~(p_5), ~(p_4), [~(p_3)] 4: ~(p_5), ~(p_4), p_3, [~(p_2)] 5: ~(p_5), ~(p_4), p_3, p_2, [~(p_1)] Gamma_38: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: [~(p_5)], p_3, p_2, p_1 Gamma_39: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 Gamma_40: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 Gamma_41: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 4: ~(p_5), p_4, ~(p_3), ~(p_2), [p_1] Gamma_42: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 4: ~(p_5), p_4, ~(p_3), ~(p_2), [p_1] 5: ~(p_5), p_4, ~(p_3), ~(p_2), [~(p_1)] Gamma_43: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 4: ~(p_5), p_4, ~(p_3), ~(p_2), [~(p_1)] 5: ~(p_5), p_4, ~(p_3), ~(p_2), [p_1] Gamma_44: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 4: ~(p_5), p_4, ~(p_3), ~(p_2), [~(p_1)] 5: [~(p_5)], p_4, ~(p_3), ~(p_2) Gamma_45: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [p_2], p_1 4: ~(p_5), p_4, ~(p_3), ~(p_2), [~(p_1)] 5: ~(p_5), p_4, ~(p_3), [~(p_2)] Gamma_46: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), [p_2], p_1 5: ~(p_5), p_4, ~(p_3), ~(p_2), [~(p_1)] Gamma_47: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: [~(p_5)], p_4, ~(p_3), p_1 Gamma_48: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), [p_1] Gamma_49: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), [p_1] 5: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] Gamma_50: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] 5: ~(p_5), p_4, ~(p_3), [p_1] Gamma_51: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] 5: [~(p_5)], p_4, ~(p_3), p_2 Gamma_52: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] 5: ~(p_5), p_4, ~(p_3), [p_2] Gamma_53: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] 5: [~(p_5)], p_4, ~(p_3) Gamma_54: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), [p_3], p_2, p_1 3: ~(p_5), p_4, ~(p_3), [~(p_2)] 4: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] 5: ~(p_5), p_4, [~(p_3)] Gamma_55: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), [p_3], p_2, p_1 4: ~(p_5), p_4, ~(p_3), [~(p_2)] 5: ~(p_5), p_4, ~(p_3), p_2, [~(p_1)] Gamma_56: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: [~(p_5)], p_4, p_2, p_1 Gamma_57: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 Gamma_58: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 4: ~(p_5), p_4, p_3, ~(p_2), [p_1] Gamma_59: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 4: ~(p_5), p_4, p_3, ~(p_2), [p_1] 5: ~(p_5), p_4, p_3, ~(p_2), [~(p_1)] Gamma_60: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 4: ~(p_5), p_4, p_3, ~(p_2), [~(p_1)] 5: ~(p_5), p_4, p_3, ~(p_2), [p_1] Gamma_61: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 4: ~(p_5), p_4, p_3, ~(p_2), [~(p_1)] 5: [~(p_5)], p_4, p_3, ~(p_2) Gamma_62: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, [p_2], p_1 4: ~(p_5), p_4, p_3, ~(p_2), [~(p_1)] 5: ~(p_5), p_4, p_3, [~(p_2)] Gamma_63: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, [p_2], p_1 5: ~(p_5), p_4, p_3, ~(p_2), [~(p_1)] Gamma_64: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: [~(p_5)], p_4, p_3, p_1 Gamma_65: (extend-no-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, [p_1] Gamma_66: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, [p_1] 5: ~(p_5), p_4, p_3, p_2, [~(p_1)] Gamma_67: (move) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: ~(p_5), p_4, p_3, [p_1] Gamma_68: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: [~(p_5)], p_4, p_3, p_2 Gamma_69: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: ~(p_5), p_4, p_3, [p_2] Gamma_70: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: [~(p_5)], p_4, p_3 Gamma_71: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: ~(p_5), p_4, [p_3] Gamma_72: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: [~(p_5)], p_4 Gamma_73: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: ~(p_5), [p_4] Gamma_74: (resolve) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: [~(p_5)] Gamma_75: (extend-conflict) 0: [p_5], p_4, p_3, p_2, p_1 1: ~(p_5), [~(p_4)] 2: ~(p_5), p_4, [~(p_3)] 3: ~(p_5), p_4, p_3, [~(p_2)] 4: ~(p_5), p_4, p_3, p_2, [~(p_1)] 5: [~(p_5)] Gamma_76: (move) 0: [~(p_5)] 1: [p_5], p_4, p_3, p_2, p_1 2: ~(p_5), [~(p_4)] 3: ~(p_5), p_4, [~(p_3)] 4: ~(p_5), p_4, p_3, [~(p_2)] 5: ~(p_5), p_4, p_3, p_2, [~(p_1)] Gamma_77: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 Gamma_78: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 Gamma_79: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 Gamma_80: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 Gamma_81: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 4: p_5, ~(p_4), ~(p_3), ~(p_2), [p_1] Gamma_82: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 4: p_5, ~(p_4), ~(p_3), ~(p_2), [p_1] 5: p_5, ~(p_4), ~(p_3), ~(p_2), [~(p_1)] Gamma_83: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 4: p_5, ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: p_5, ~(p_4), ~(p_3), ~(p_2), [p_1] Gamma_84: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 4: p_5, ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: [p_5], ~(p_4), ~(p_3), ~(p_2) Gamma_85: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [p_2], p_1 4: p_5, ~(p_4), ~(p_3), ~(p_2), [~(p_1)] 5: p_5, ~(p_4), ~(p_3), [~(p_2)] Gamma_86: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), [p_2], p_1 5: p_5, ~(p_4), ~(p_3), ~(p_2), [~(p_1)] Gamma_87: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: [p_5], ~(p_4), ~(p_3), p_1 Gamma_88: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), [p_1] Gamma_89: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), [p_1] 5: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] Gamma_90: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] 5: p_5, ~(p_4), ~(p_3), [p_1] Gamma_91: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] 5: [p_5], ~(p_4), ~(p_3), p_2 Gamma_92: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] 5: p_5, ~(p_4), ~(p_3), [p_2] Gamma_93: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] 5: [p_5], ~(p_4), ~(p_3) Gamma_94: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [p_3], p_2, p_1 3: p_5, ~(p_4), ~(p_3), [~(p_2)] 4: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] 5: p_5, ~(p_4), [~(p_3)] Gamma_95: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_3], p_2, p_1 4: p_5, ~(p_4), ~(p_3), [~(p_2)] 5: p_5, ~(p_4), ~(p_3), p_2, [~(p_1)] Gamma_96: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: [p_5], ~(p_4), p_2, p_1 Gamma_97: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 Gamma_98: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 4: p_5, ~(p_4), p_3, ~(p_2), [p_1] Gamma_99: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 4: p_5, ~(p_4), p_3, ~(p_2), [p_1] 5: p_5, ~(p_4), p_3, ~(p_2), [~(p_1)] Gamma_100: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 4: p_5, ~(p_4), p_3, ~(p_2), [~(p_1)] 5: p_5, ~(p_4), p_3, ~(p_2), [p_1] Gamma_101: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 4: p_5, ~(p_4), p_3, ~(p_2), [~(p_1)] 5: [p_5], ~(p_4), p_3, ~(p_2) Gamma_102: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), [p_2], p_1 4: p_5, ~(p_4), p_3, ~(p_2), [~(p_1)] 5: p_5, ~(p_4), p_3, [~(p_2)] Gamma_103: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), [p_2], p_1 5: p_5, ~(p_4), p_3, ~(p_2), [~(p_1)] Gamma_104: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: [p_5], ~(p_4), p_3, p_1 Gamma_105: (extend-no-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, [p_1] Gamma_106: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, [p_1] 5: p_5, ~(p_4), p_3, p_2, [~(p_1)] Gamma_107: (move) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: p_5, ~(p_4), p_3, [p_1] Gamma_108: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: [p_5], ~(p_4), p_3, p_2 Gamma_109: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: p_5, ~(p_4), p_3, [p_2] Gamma_110: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: [p_5], ~(p_4), p_3 Gamma_111: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: p_5, ~(p_4), [p_3] Gamma_112: (resolve) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: [p_5], ~(p_4) Gamma_113: (extend-conflict) 0: [~(p_5)] 1: [p_4], p_3, p_2, p_1 2: p_5, ~(p_4), [~(p_3)] 3: p_5, ~(p_4), p_3, [~(p_2)] 4: p_5, ~(p_4), p_3, p_2, [~(p_1)] 5: p_5, [~(p_4)] Gamma_114: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: [p_4], p_3, p_2, p_1 3: p_5, ~(p_4), [~(p_3)] 4: p_5, ~(p_4), p_3, [~(p_2)] 5: p_5, ~(p_4), p_3, p_2, [~(p_1)] Gamma_115: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 Gamma_116: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 Gamma_117: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 Gamma_118: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 4: p_5, p_4, ~(p_3), ~(p_2), [p_1] Gamma_119: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 4: p_5, p_4, ~(p_3), ~(p_2), [p_1] 5: p_5, p_4, ~(p_3), ~(p_2), [~(p_1)] Gamma_120: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 4: p_5, p_4, ~(p_3), ~(p_2), [~(p_1)] 5: p_5, p_4, ~(p_3), ~(p_2), [p_1] Gamma_121: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 4: p_5, p_4, ~(p_3), ~(p_2), [~(p_1)] 5: [p_5], p_4, ~(p_3), ~(p_2) Gamma_122: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [p_2], p_1 4: p_5, p_4, ~(p_3), ~(p_2), [~(p_1)] 5: p_5, p_4, ~(p_3), [~(p_2)] Gamma_123: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), [p_2], p_1 5: p_5, p_4, ~(p_3), ~(p_2), [~(p_1)] Gamma_124: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: [p_5], p_4, ~(p_3), p_1 Gamma_125: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), [p_1] Gamma_126: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), [p_1] 5: p_5, p_4, ~(p_3), p_2, [~(p_1)] Gamma_127: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), p_2, [~(p_1)] 5: p_5, p_4, ~(p_3), [p_1] Gamma_128: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), p_2, [~(p_1)] 5: [p_5], p_4, ~(p_3), p_2 Gamma_129: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), p_2, [~(p_1)] 5: p_5, p_4, ~(p_3), [p_2] Gamma_130: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), p_2, [~(p_1)] 5: [p_5], p_4, ~(p_3) Gamma_131: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, [p_3], p_2, p_1 3: p_5, p_4, ~(p_3), [~(p_2)] 4: p_5, p_4, ~(p_3), p_2, [~(p_1)] 5: p_5, p_4, [~(p_3)] Gamma_132: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, [p_3], p_2, p_1 4: p_5, p_4, ~(p_3), [~(p_2)] 5: p_5, p_4, ~(p_3), p_2, [~(p_1)] Gamma_133: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: [p_5], p_4, p_2, p_1 Gamma_134: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 Gamma_135: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 4: p_5, p_4, p_3, ~(p_2), [p_1] Gamma_136: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 4: p_5, p_4, p_3, ~(p_2), [p_1] 5: p_5, p_4, p_3, ~(p_2), [~(p_1)] Gamma_137: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 4: p_5, p_4, p_3, ~(p_2), [~(p_1)] 5: p_5, p_4, p_3, ~(p_2), [p_1] Gamma_138: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 4: p_5, p_4, p_3, ~(p_2), [~(p_1)] 5: [p_5], p_4, p_3, ~(p_2) Gamma_139: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, [p_2], p_1 4: p_5, p_4, p_3, ~(p_2), [~(p_1)] 5: p_5, p_4, p_3, [~(p_2)] Gamma_140: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, [p_2], p_1 5: p_5, p_4, p_3, ~(p_2), [~(p_1)] Gamma_141: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: [p_5], p_4, p_3, p_1 Gamma_142: (extend-no-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, [p_1] Gamma_143: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, [p_1] 5: p_5, p_4, p_3, p_2, [~(p_1)] Gamma_144: (move) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: p_5, p_4, p_3, [p_1] Gamma_145: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [p_5], p_4, p_3, p_2 Gamma_146: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: p_5, p_4, p_3, [p_2] Gamma_147: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [p_5], p_4, p_3 Gamma_148: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: p_5, p_4, [p_3] Gamma_149: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [p_5], p_4 Gamma_150: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: p_5, [p_4] Gamma_151: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [p_5] Gamma_152: (extend-conflict) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [p_5] Gamma_153: (resolve) 0: [~(p_5)] 1: p_5, [~(p_4)] 2: p_5, p_4, [~(p_3)] 3: p_5, p_4, p_3, [~(p_2)] 4: p_5, p_4, p_3, p_2, [~(p_1)] 5: [] SZS status Unsatisfiable