%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [r(sk2)], r(sk1) Gamma_1: (extend-no-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) Gamma_2: (extend-no-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] Gamma_3: (extend-no-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 3: [s(sk1)], ~(r(sk1)) Gamma_4: (extend-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 3: [s(sk1)], ~(r(sk1)) 4: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) Gamma_5: (move) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 3: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) 4: [s(sk1)], ~(r(sk1)) Gamma_6: (resolve) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 3: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) 4: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] Gamma_7: (extend-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 3: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) 4: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] Gamma_8: (move) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] 3: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 4: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) Gamma_9: (resolve) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] 3: [~(s(sk2))], ~(r(sk2)) 4: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) Gamma_10: (extend-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] 3: [~(s(sk2))], ~(r(sk2)) 4: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) Gamma_11: (move) 0: [r(sk2)], r(sk1) 1: [~(s(sk2))], ~(r(sk2)) 2: [s(sk2)], ~(r(sk2)) 3: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] 4: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) Gamma_12: (resolve) 0: [r(sk2)], r(sk1) 1: [~(s(sk2))], ~(r(sk2)) 2: [~(r(sk2))] Gamma_13: (extend-conflict) 0: [r(sk2)], r(sk1) 1: [~(s(sk2))], ~(r(sk2)) 2: [~(r(sk2))] Gamma_14: (move) 0: [~(r(sk2))] 1: [r(sk2)], r(sk1) 2: [~(s(sk2))], ~(r(sk2)) Gamma_15: (resolve) 0: [~(r(sk2))] 1: [r(sk1)] Gamma_16: (extend-no-conflict) 0: [~(r(sk2))] 1: [r(sk1)] Gamma_17: (extend-no-conflict) 0: [~(r(sk2))] 1: [r(sk1)] 2: [s(sk1)], ~(r(sk1)) Gamma_18: (extend-conflict) 0: [~(r(sk2))] 1: [r(sk1)] 2: [s(sk1)], ~(r(sk1)) 3: [~(s(sk1))], r(sk2) Gamma_19: (move) 0: [~(r(sk2))] 1: [r(sk1)] 2: [~(s(sk1))], r(sk2) 3: [s(sk1)], ~(r(sk1)) Gamma_20: (resolve) 0: [~(r(sk2))] 1: [r(sk1)] 2: [~(s(sk1))], r(sk2) 3: r(sk2), [~(r(sk1))] Gamma_21: (extend-conflict) 0: [~(r(sk2))] 1: [r(sk1)] 2: [~(s(sk1))], r(sk2) 3: r(sk2), [~(r(sk1))] Gamma_22: (move) 0: [~(r(sk2))] 1: r(sk2), [~(r(sk1))] 2: [r(sk1)] 3: [~(s(sk1))], r(sk2) Gamma_23: (resolve) 0: [~(r(sk2))] 1: r(sk2), [~(r(sk1))] 2: [r(sk2)] 3: [~(s(sk1))], r(sk2) Gamma_24: (extend-conflict) 0: [~(r(sk2))] 1: r(sk2), [~(r(sk1))] 2: [r(sk2)] 3: [~(s(sk1))], r(sk2) Gamma_25: (resolve) 0: [~(r(sk2))] 1: r(sk2), [~(r(sk1))] 2: [] 3: [~(s(sk1))], r(sk2) SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [r(sk2)], r(sk1) Gamma_1: (extend-no-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) Gamma_2: (extend-no-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] Gamma_3: (extend-no-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 3: [s(sk1)], ~(r(sk1)) Gamma_4: (extend-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 3: [s(sk1)], ~(r(sk1)) 4: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) Gamma_5: (move) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 3: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) 4: [s(sk1)], ~(r(sk1)) Gamma_6: (resolve) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 3: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) 4: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] Gamma_7: (extend-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 3: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) 4: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] Gamma_8: (move) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] 3: ~(s(sk2)), ~(r(sk2)), [r(sk1)] 4: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) Gamma_9: (resolve) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] 3: [~(s(sk2))], ~(r(sk2)) 4: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) Gamma_10: (extend-conflict) 0: [r(sk2)], r(sk1) 1: [s(sk2)], ~(r(sk2)) 2: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] 3: [~(s(sk2))], ~(r(sk2)) 4: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) Gamma_11: (move) 0: [r(sk2)], r(sk1) 1: [~(s(sk2))], ~(r(sk2)) 2: [s(sk2)], ~(r(sk2)) 3: ~(s(sk2)), ~(r(sk2)), [~(r(sk1))] 4: ~(s(sk2)), [~(s(sk1))], ~(r(sk2)) Gamma_12: (resolve) 0: [r(sk2)], r(sk1) 1: [~(s(sk2))], ~(r(sk2)) 2: [~(r(sk2))] Gamma_13: (extend-conflict) 0: [r(sk2)], r(sk1) 1: [~(s(sk2))], ~(r(sk2)) 2: [~(r(sk2))] Gamma_14: (move) 0: [~(r(sk2))] 1: [r(sk2)], r(sk1) 2: [~(s(sk2))], ~(r(sk2)) Gamma_15: (resolve) 0: [~(r(sk2))] 1: [r(sk1)] Gamma_16: (extend-no-conflict) 0: [~(r(sk2))] 1: [r(sk1)] Gamma_17: (extend-no-conflict) 0: [~(r(sk2))] 1: [r(sk1)] 2: [s(sk1)], ~(r(sk1)) Gamma_18: (extend-conflict) 0: [~(r(sk2))] 1: [r(sk1)] 2: [s(sk1)], ~(r(sk1)) 3: [~(s(sk1))], r(sk2) Gamma_19: (move) 0: [~(r(sk2))] 1: [r(sk1)] 2: [~(s(sk1))], r(sk2) 3: [s(sk1)], ~(r(sk1)) Gamma_20: (resolve) 0: [~(r(sk2))] 1: [r(sk1)] 2: [~(s(sk1))], r(sk2) 3: r(sk2), [~(r(sk1))] Gamma_21: (extend-conflict) 0: [~(r(sk2))] 1: [r(sk1)] 2: [~(s(sk1))], r(sk2) 3: r(sk2), [~(r(sk1))] Gamma_22: (move) 0: [~(r(sk2))] 1: r(sk2), [~(r(sk1))] 2: [r(sk1)] 3: [~(s(sk1))], r(sk2) Gamma_23: (resolve) 0: [~(r(sk2))] 1: r(sk2), [~(r(sk1))] 2: [r(sk2)] 3: [~(s(sk1))], r(sk2) Gamma_24: (extend-conflict) 0: [~(r(sk2))] 1: r(sk2), [~(r(sk1))] 2: [r(sk2)] 3: [~(s(sk1))], r(sk2) Gamma_25: (resolve) 0: [~(r(sk2))] 1: r(sk2), [~(r(sk1))] 2: [] 3: [~(s(sk1))], r(sk2) SZS status Unsatisfiable