%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [p_10] Gamma_1: (extend-no-conflict) 0: [p_10] 1: [p_9] Gamma_2: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] Gamma_3: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] Gamma_4: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] Gamma_5: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] Gamma_6: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] Gamma_7: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] Gamma_8: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] Gamma_9: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] Gamma_10: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] 10: [p_0], ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~( p_3), ~(p_2), ~(p_1) Gamma_11: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] 10: [p_0], ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~( p_3), ~(p_2), ~(p_1) 11: [~(p_0)] Gamma_12: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] 10: [~(p_0)] 11: [p_0], ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~( p_3), ~(p_2), ~(p_1) Gamma_13: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] 10: [~(p_0)] 11: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), ~(p_1) Gamma_14: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] 10: [~(p_0)] 11: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), [~(p_1)] Gamma_15: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), [~(p_1)] 10: [p_1] 11: [~(p_0)] Gamma_16: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), [~(p_1)] 10: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2) 11: [~(p_0)] Gamma_17: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), [~(p_1)] 10: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), [~( p_2)] 11: [~(p_0)] Gamma_18: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), [~( p_2)] 9: [p_2] 10: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), [~(p_1)] 11: [~(p_0)] Gamma_19: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), [~( p_2)] 9: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3) 10: [~(p_0)] Gamma_20: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), [~( p_2)] 9: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), [~(p_3)] 10: [~(p_0)] Gamma_21: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), [~(p_3)] 8: [p_3] 9: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), [~( p_2)] 10: [~(p_0)] Gamma_22: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), [~(p_3)] 8: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4) 9: [~(p_0)] Gamma_23: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), [~(p_3)] 8: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), [~(p_4)] 9: [~(p_0)] Gamma_24: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), [~(p_4)] 7: [p_4] 8: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), [~(p_3)] 9: [~(p_0)] Gamma_25: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), [~(p_4)] 7: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5) 8: [~(p_0)] Gamma_26: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), [~(p_4)] 7: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), [~(p_5)] 8: [~(p_0)] Gamma_27: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), [~(p_5)] 6: [p_5] 7: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), [~(p_4)] 8: [~(p_0)] Gamma_28: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), [~(p_5)] 6: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6) 7: [~(p_0)] Gamma_29: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), [~(p_5)] 6: ~(p_10), ~(p_9), ~(p_8), ~(p_7), [~(p_6)] 7: [~(p_0)] Gamma_30: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: ~(p_10), ~(p_9), ~(p_8), ~(p_7), [~(p_6)] 5: [p_6] 6: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), [~(p_5)] 7: [~(p_0)] Gamma_31: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: ~(p_10), ~(p_9), ~(p_8), ~(p_7), [~(p_6)] 5: [~(p_10)], ~(p_9), ~(p_8), ~(p_7) 6: [~(p_0)] Gamma_32: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: ~(p_10), ~(p_9), ~(p_8), ~(p_7), [~(p_6)] 5: ~(p_10), ~(p_9), ~(p_8), [~(p_7)] 6: [~(p_0)] Gamma_33: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: ~(p_10), ~(p_9), ~(p_8), [~(p_7)] 4: [p_7] 5: ~(p_10), ~(p_9), ~(p_8), ~(p_7), [~(p_6)] 6: [~(p_0)] Gamma_34: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: ~(p_10), ~(p_9), ~(p_8), [~(p_7)] 4: [~(p_10)], ~(p_9), ~(p_8) 5: [~(p_0)] Gamma_35: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: ~(p_10), ~(p_9), ~(p_8), [~(p_7)] 4: ~(p_10), ~(p_9), [~(p_8)] 5: [~(p_0)] Gamma_36: (move) 0: [p_10] 1: [p_9] 2: ~(p_10), ~(p_9), [~(p_8)] 3: [p_8] 4: ~(p_10), ~(p_9), ~(p_8), [~(p_7)] 5: [~(p_0)] Gamma_37: (resolve) 0: [p_10] 1: [p_9] 2: ~(p_10), ~(p_9), [~(p_8)] 3: [~(p_10)], ~(p_9) 4: [~(p_0)] Gamma_38: (extend-conflict) 0: [p_10] 1: [p_9] 2: ~(p_10), ~(p_9), [~(p_8)] 3: ~(p_10), [~(p_9)] 4: [~(p_0)] Gamma_39: (move) 0: [p_10] 1: ~(p_10), [~(p_9)] 2: [p_9] 3: ~(p_10), ~(p_9), [~(p_8)] 4: [~(p_0)] Gamma_40: (resolve) 0: [p_10] 1: ~(p_10), [~(p_9)] 2: [~(p_10)] 3: [~(p_0)] Gamma_41: (extend-conflict) 0: [p_10] 1: ~(p_10), [~(p_9)] 2: [~(p_10)] 3: [~(p_0)] Gamma_42: (move) 0: [~(p_10)] 1: [p_10] 2: ~(p_10), [~(p_9)] 3: [~(p_0)] Gamma_43: (resolve) 0: [~(p_10)] 1: [] 2: [~(p_0)] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [p_10] Gamma_1: (extend-no-conflict) 0: [p_10] 1: [p_9] Gamma_2: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] Gamma_3: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] Gamma_4: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] Gamma_5: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] Gamma_6: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] Gamma_7: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] Gamma_8: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] Gamma_9: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] Gamma_10: (extend-no-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] 10: [p_0], ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~( p_3), ~(p_2), ~(p_1) Gamma_11: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] 10: [p_0], ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~( p_3), ~(p_2), ~(p_1) 11: [~(p_0)] Gamma_12: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] 10: [~(p_0)] 11: [p_0], ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~( p_3), ~(p_2), ~(p_1) Gamma_13: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] 10: [~(p_0)] 11: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), ~(p_1) Gamma_14: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: [p_1] 10: [~(p_0)] 11: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), [~(p_1)] Gamma_15: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), [~(p_1)] 10: [p_1] 11: [~(p_0)] Gamma_16: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), [~(p_1)] 10: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2) 11: [~(p_0)] Gamma_17: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: [p_2] 9: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), [~(p_1)] 10: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), [~( p_2)] 11: [~(p_0)] Gamma_18: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), [~( p_2)] 9: [p_2] 10: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), ~( p_2), [~(p_1)] 11: [~(p_0)] Gamma_19: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), [~( p_2)] 9: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3) 10: [~(p_0)] Gamma_20: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: [p_3] 8: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), [~( p_2)] 9: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), [~(p_3)] 10: [~(p_0)] Gamma_21: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), [~(p_3)] 8: [p_3] 9: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), ~(p_3), [~( p_2)] 10: [~(p_0)] Gamma_22: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), [~(p_3)] 8: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4) 9: [~(p_0)] Gamma_23: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: [p_4] 7: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), [~(p_3)] 8: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), [~(p_4)] 9: [~(p_0)] Gamma_24: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), [~(p_4)] 7: [p_4] 8: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), ~(p_4), [~(p_3)] 9: [~(p_0)] Gamma_25: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), [~(p_4)] 7: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5) 8: [~(p_0)] Gamma_26: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: [p_5] 6: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), [~(p_4)] 7: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), [~(p_5)] 8: [~(p_0)] Gamma_27: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), [~(p_5)] 6: [p_5] 7: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), ~(p_5), [~(p_4)] 8: [~(p_0)] Gamma_28: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), [~(p_5)] 6: [~(p_10)], ~(p_9), ~(p_8), ~(p_7), ~(p_6) 7: [~(p_0)] Gamma_29: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: [p_6] 5: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), [~(p_5)] 6: ~(p_10), ~(p_9), ~(p_8), ~(p_7), [~(p_6)] 7: [~(p_0)] Gamma_30: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: ~(p_10), ~(p_9), ~(p_8), ~(p_7), [~(p_6)] 5: [p_6] 6: ~(p_10), ~(p_9), ~(p_8), ~(p_7), ~(p_6), [~(p_5)] 7: [~(p_0)] Gamma_31: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: ~(p_10), ~(p_9), ~(p_8), ~(p_7), [~(p_6)] 5: [~(p_10)], ~(p_9), ~(p_8), ~(p_7) 6: [~(p_0)] Gamma_32: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: [p_7] 4: ~(p_10), ~(p_9), ~(p_8), ~(p_7), [~(p_6)] 5: ~(p_10), ~(p_9), ~(p_8), [~(p_7)] 6: [~(p_0)] Gamma_33: (move) 0: [p_10] 1: [p_9] 2: [p_8] 3: ~(p_10), ~(p_9), ~(p_8), [~(p_7)] 4: [p_7] 5: ~(p_10), ~(p_9), ~(p_8), ~(p_7), [~(p_6)] 6: [~(p_0)] Gamma_34: (resolve) 0: [p_10] 1: [p_9] 2: [p_8] 3: ~(p_10), ~(p_9), ~(p_8), [~(p_7)] 4: [~(p_10)], ~(p_9), ~(p_8) 5: [~(p_0)] Gamma_35: (extend-conflict) 0: [p_10] 1: [p_9] 2: [p_8] 3: ~(p_10), ~(p_9), ~(p_8), [~(p_7)] 4: ~(p_10), ~(p_9), [~(p_8)] 5: [~(p_0)] Gamma_36: (move) 0: [p_10] 1: [p_9] 2: ~(p_10), ~(p_9), [~(p_8)] 3: [p_8] 4: ~(p_10), ~(p_9), ~(p_8), [~(p_7)] 5: [~(p_0)] Gamma_37: (resolve) 0: [p_10] 1: [p_9] 2: ~(p_10), ~(p_9), [~(p_8)] 3: [~(p_10)], ~(p_9) 4: [~(p_0)] Gamma_38: (extend-conflict) 0: [p_10] 1: [p_9] 2: ~(p_10), ~(p_9), [~(p_8)] 3: ~(p_10), [~(p_9)] 4: [~(p_0)] Gamma_39: (move) 0: [p_10] 1: ~(p_10), [~(p_9)] 2: [p_9] 3: ~(p_10), ~(p_9), [~(p_8)] 4: [~(p_0)] Gamma_40: (resolve) 0: [p_10] 1: ~(p_10), [~(p_9)] 2: [~(p_10)] 3: [~(p_0)] Gamma_41: (extend-conflict) 0: [p_10] 1: ~(p_10), [~(p_9)] 2: [~(p_10)] 3: [~(p_0)] Gamma_42: (move) 0: [~(p_10)] 1: [p_10] 2: ~(p_10), [~(p_9)] 3: [~(p_0)] Gamma_43: (resolve) 0: [~(p_10)] 1: [] 2: [~(p_0)] SZS status Unsatisfiable