%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] Gamma_1: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] Gamma_2: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] Gamma_3: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] Gamma_4: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] Gamma_5: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] Gamma_6: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] Gamma_7: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] Gamma_8: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] Gamma_9: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] Gamma_10: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: ~(r1(esk1_0,esk4_0)), [p2(esk4_0)] Gamma_11: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: ~(r1(esk1_0,esk4_0)), [p2(esk4_0)] 11: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] Gamma_12: (extend-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: ~(r1(esk1_0,esk4_0)), [p2(esk4_0)] 11: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] 12: [~(p2(esk4_0))] Gamma_13: (move) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: [~(p2(esk4_0))] 11: ~(r1(esk1_0,esk4_0)), [p2(esk4_0)] 12: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] Gamma_14: (resolve) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: [~(p2(esk4_0))] 11: [~(r1(esk1_0,esk4_0))] 12: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] Gamma_15: (extend-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: [~(p2(esk4_0))] 11: [~(r1(esk1_0,esk4_0))] 12: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] Gamma_16: (move) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [~(r1(esk1_0,esk4_0))] 9: [r1(esk1_0,esk4_0)] 10: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 11: [~(p2(esk4_0))] 12: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] Gamma_17: (resolve) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [~(r1(esk1_0,esk4_0))] 9: [] 10: [~(p2(esk4_0))] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] Gamma_1: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] Gamma_2: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] Gamma_3: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] Gamma_4: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] Gamma_5: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] Gamma_6: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] Gamma_7: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] Gamma_8: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] Gamma_9: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] Gamma_10: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: ~(r1(esk1_0,esk4_0)), [p2(esk4_0)] Gamma_11: (extend-no-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: ~(r1(esk1_0,esk4_0)), [p2(esk4_0)] 11: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] Gamma_12: (extend-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: ~(r1(esk1_0,esk4_0)), [p2(esk4_0)] 11: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] 12: [~(p2(esk4_0))] Gamma_13: (move) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: [~(p2(esk4_0))] 11: ~(r1(esk1_0,esk4_0)), [p2(esk4_0)] 12: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] Gamma_14: (resolve) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: [~(p2(esk4_0))] 11: [~(r1(esk1_0,esk4_0))] 12: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] Gamma_15: (extend-conflict) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [r1(esk1_0,esk4_0)] 9: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 10: [~(p2(esk4_0))] 11: [~(r1(esk1_0,esk4_0))] 12: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] Gamma_16: (move) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [~(r1(esk1_0,esk4_0))] 9: [r1(esk1_0,esk4_0)] 10: ~(r1(esk1_0,esk4_0)), [p6(esk4_0)] 11: [~(p2(esk4_0))] 12: ~(r1(esk1_0,esk4_0)), [p4(esk4_0)] Gamma_17: (resolve) 0: [r1(esk1_0,esk2_0)] 1: ~(r1(esk1_0,esk2_0)), [p6(esk2_0)] 2: ~(r1(esk1_0,esk2_0)), [p2(esk2_0)] 3: ~(r1(esk1_0,esk2_0)), [p4(esk2_0)] 4: [r1(esk1_0,esk3_0)] 5: ~(r1(esk1_0,esk3_0)), [p6(esk3_0)] 6: ~(r1(esk1_0,esk3_0)), [p2(esk3_0)] 7: ~(r1(esk1_0,esk3_0)), [p4(esk3_0)] 8: [~(r1(esk1_0,esk4_0))] 9: [] 10: [~(p2(esk4_0))] SZS status Unsatisfiable