%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] Gamma_1: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] Gamma_2: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] Gamma_3: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] Gamma_4: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] Gamma_5: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) Gamma_6: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [patricide( thersandros)], ~(patricide(polyneikes)) Gamma_7: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [patricide( thersandros)], ~(patricide(polyneikes)) 7: [~(patricide(thersandros))] Gamma_8: (move) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 6: [~(patricide(thersandros))] 7: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [patricide( thersandros)], ~(patricide(polyneikes)) Gamma_9: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 6: [~(patricide(thersandros))] 7: [~(parent_of(polyneikes,thersandros))], ~(parent_of(iokaste,polyneikes)), ~( patricide(polyneikes)) Gamma_10: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 6: [~(patricide(thersandros))] 7: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] Gamma_11: (move) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 7: [~(patricide(thersandros))] Gamma_12: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)), ~(patricide(oedipus)) 7: [~(patricide(thersandros))] Gamma_13: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [~(patricide(oedipus))] 7: [~(patricide(thersandros))] Gamma_14: (move) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [~(patricide(oedipus))] 5: [patricide(oedipus)] 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 7: [~(patricide(thersandros))] Gamma_15: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [~(patricide(oedipus))] 5: [~(parent_of(polyneikes,thersandros))], ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)) 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 7: [~(patricide(thersandros))] Gamma_16: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [~(patricide(oedipus))] 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)) 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 7: [~(patricide(thersandros))] Gamma_17: (move) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)) 4: [parent_of(iokaste,oedipus)] 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [~(patricide(oedipus))] 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 7: [~(patricide(thersandros))] Gamma_18: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)) 4: [~(parent_of(polyneikes,thersandros))], ~(parent_of(iokaste,polyneikes)), ~( parent_of(oedipus,polyneikes)) 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: [~(patricide(thersandros))] Gamma_19: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)) 4: ~(parent_of(polyneikes,thersandros)), [~(parent_of(iokaste,polyneikes))], ~( parent_of(oedipus,polyneikes)) 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: [~(patricide(thersandros))] Gamma_20: (move) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: ~(parent_of(polyneikes,thersandros)), [~(parent_of(iokaste,polyneikes))], ~( parent_of(oedipus,polyneikes)) 3: [parent_of(iokaste,polyneikes)] 4: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)) 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: [~(patricide(thersandros))] Gamma_21: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: ~(parent_of(polyneikes,thersandros)), [~(parent_of(iokaste,polyneikes))], ~( parent_of(oedipus,polyneikes)) 3: [~(parent_of(polyneikes,thersandros))], ~(parent_of(oedipus,polyneikes)) 4: [~(patricide(thersandros))] Gamma_22: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: ~(parent_of(polyneikes,thersandros)), [~(parent_of(iokaste,polyneikes))], ~( parent_of(oedipus,polyneikes)) 3: ~(parent_of(polyneikes,thersandros)), [~(parent_of(oedipus,polyneikes))] 4: [~(patricide(thersandros))] Gamma_23: (move) 0: [parent_of(polyneikes,thersandros)] 1: ~(parent_of(polyneikes,thersandros)), [~(parent_of(oedipus,polyneikes))] 2: [parent_of(oedipus,polyneikes)] 3: ~(parent_of(polyneikes,thersandros)), [~(parent_of(iokaste,polyneikes))], ~( parent_of(oedipus,polyneikes)) 4: [~(patricide(thersandros))] Gamma_24: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: ~(parent_of(polyneikes,thersandros)), [~(parent_of(oedipus,polyneikes))] 2: [~(parent_of(polyneikes,thersandros))] 3: [~(patricide(thersandros))] Gamma_25: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: ~(parent_of(polyneikes,thersandros)), [~(parent_of(oedipus,polyneikes))] 2: [~(parent_of(polyneikes,thersandros))] 3: [~(patricide(thersandros))] Gamma_26: (move) 0: [~(parent_of(polyneikes,thersandros))] 1: [parent_of(polyneikes,thersandros)] 2: ~(parent_of(polyneikes,thersandros)), [~(parent_of(oedipus,polyneikes))] 3: [~(patricide(thersandros))] Gamma_27: (resolve) 0: [~(parent_of(polyneikes,thersandros))] 1: [] 2: [~(patricide(thersandros))] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] Gamma_1: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] Gamma_2: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] Gamma_3: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] Gamma_4: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] Gamma_5: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) Gamma_6: (extend-no-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [patricide( thersandros)], ~(patricide(polyneikes)) Gamma_7: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [patricide( thersandros)], ~(patricide(polyneikes)) 7: [~(patricide(thersandros))] Gamma_8: (move) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 6: [~(patricide(thersandros))] 7: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [patricide( thersandros)], ~(patricide(polyneikes)) Gamma_9: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 6: [~(patricide(thersandros))] 7: [~(parent_of(polyneikes,thersandros))], ~(parent_of(iokaste,polyneikes)), ~( patricide(polyneikes)) Gamma_10: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 6: [~(patricide(thersandros))] 7: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] Gamma_11: (move) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: ~(parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [patricide( polyneikes)], ~(patricide(oedipus)) 7: [~(patricide(thersandros))] Gamma_12: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)), ~(patricide(oedipus)) 7: [~(patricide(thersandros))] Gamma_13: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: [patricide(oedipus)] 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [~(patricide(oedipus))] 7: [~(patricide(thersandros))] Gamma_14: (move) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [~(patricide(oedipus))] 5: [patricide(oedipus)] 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 7: [~(patricide(thersandros))] Gamma_15: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [~(patricide(oedipus))] 5: [~(parent_of(polyneikes,thersandros))], ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)) 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 7: [~(patricide(thersandros))] Gamma_16: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: [parent_of(iokaste,oedipus)] 4: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [~(patricide(oedipus))] 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)) 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 7: [~(patricide(thersandros))] Gamma_17: (move) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)) 4: [parent_of(iokaste,oedipus)] 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), ~( parent_of(iokaste,oedipus)), ~(parent_of(oedipus,polyneikes)), [~(patricide(oedipus))] 6: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 7: [~(patricide(thersandros))] Gamma_18: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)) 4: [~(parent_of(polyneikes,thersandros))], ~(parent_of(iokaste,polyneikes)), ~( parent_of(oedipus,polyneikes)) 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: [~(patricide(thersandros))] Gamma_19: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: [parent_of(iokaste,polyneikes)] 3: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)) 4: ~(parent_of(polyneikes,thersandros)), [~(parent_of(iokaste,polyneikes))], ~( parent_of(oedipus,polyneikes)) 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: [~(patricide(thersandros))] Gamma_20: (move) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: ~(parent_of(polyneikes,thersandros)), [~(parent_of(iokaste,polyneikes))], ~( parent_of(oedipus,polyneikes)) 3: [parent_of(iokaste,polyneikes)] 4: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( parent_of(iokaste,oedipus))], ~(parent_of(oedipus,polyneikes)) 5: ~(parent_of(polyneikes,thersandros)), ~(parent_of(iokaste,polyneikes)), [~( patricide(polyneikes))] 6: [~(patricide(thersandros))] Gamma_21: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: ~(parent_of(polyneikes,thersandros)), [~(parent_of(iokaste,polyneikes))], ~( parent_of(oedipus,polyneikes)) 3: [~(parent_of(polyneikes,thersandros))], ~(parent_of(oedipus,polyneikes)) 4: [~(patricide(thersandros))] Gamma_22: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: [parent_of(oedipus,polyneikes)] 2: ~(parent_of(polyneikes,thersandros)), [~(parent_of(iokaste,polyneikes))], ~( parent_of(oedipus,polyneikes)) 3: ~(parent_of(polyneikes,thersandros)), [~(parent_of(oedipus,polyneikes))] 4: [~(patricide(thersandros))] Gamma_23: (move) 0: [parent_of(polyneikes,thersandros)] 1: ~(parent_of(polyneikes,thersandros)), [~(parent_of(oedipus,polyneikes))] 2: [parent_of(oedipus,polyneikes)] 3: ~(parent_of(polyneikes,thersandros)), [~(parent_of(iokaste,polyneikes))], ~( parent_of(oedipus,polyneikes)) 4: [~(patricide(thersandros))] Gamma_24: (resolve) 0: [parent_of(polyneikes,thersandros)] 1: ~(parent_of(polyneikes,thersandros)), [~(parent_of(oedipus,polyneikes))] 2: [~(parent_of(polyneikes,thersandros))] 3: [~(patricide(thersandros))] Gamma_25: (extend-conflict) 0: [parent_of(polyneikes,thersandros)] 1: ~(parent_of(polyneikes,thersandros)), [~(parent_of(oedipus,polyneikes))] 2: [~(parent_of(polyneikes,thersandros))] 3: [~(patricide(thersandros))] Gamma_26: (move) 0: [~(parent_of(polyneikes,thersandros))] 1: [parent_of(polyneikes,thersandros)] 2: ~(parent_of(polyneikes,thersandros)), [~(parent_of(oedipus,polyneikes))] 3: [~(patricide(thersandros))] Gamma_27: (resolve) 0: [~(parent_of(polyneikes,thersandros))] 1: [] 2: [~(patricide(thersandros))] SZS status Unsatisfiable