%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... flip all literals with predicate richer use I- Gamma_0: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) Gamma_1: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) Gamma_2: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] Gamma_3: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] Gamma_4: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_5: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [hates(agatha,agatha)] Gamma_6: (extend-conflict) 0: [killed(charles,agatha)], killed(butler, agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [hates(agatha,agatha)] 6: ~(hates(charles,agatha)), [~(hates(agatha,agatha))] Gamma_7: (move) 0: [killed(charles,agatha)], killed(butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: ~(hates(charles,agatha)), [~(hates(agatha,agatha))] 6: [hates(agatha,agatha)] Gamma_8: (resolve) 0: [killed(charles,agatha)], killed(butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: ~(hates(charles,agatha)), [~(hates(agatha,agatha))] 6: [~(hates(charles,agatha))] Gamma_9: (extend-conflict) 0: [killed(charles,agatha)], killed(butler, agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: ~(hates(charles,agatha)), [~(hates(agatha,agatha))] 6: [~(hates(charles,agatha))] Gamma_10: (move) 0: [killed(charles,agatha)], killed(butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: [~(hates(charles,agatha))] 3: ~(killed(charles,agatha)), [hates(charles,agatha)] 4: [hates(agatha,charles)] 5: [hates(butler,charles)], ~(hates(agatha,charles)) 6: ~(hates(charles,agatha)), [~(hates(agatha,agatha))] Gamma_11: (resolve) 0: [killed(charles,agatha)], killed(butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: [~(hates(charles,agatha))] 3: [~(killed(charles,agatha))] 4: [hates(agatha,charles)] 5: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_12: (extend-conflict) 0: [killed(charles,agatha)], killed(butler, agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: [~(hates(charles,agatha))] 3: [~(killed(charles,agatha))] 4: [hates(agatha,charles)] 5: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_13: (move) 0: [~(killed(charles,agatha))] 1: [killed(charles,agatha)], killed(butler,agatha) 2: [richer(charles,agatha)], ~(killed(charles,agatha)) 3: [~(hates(charles,agatha))] 4: [hates(agatha,charles)] 5: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_14: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_15: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_16: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) Gamma_17: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] Gamma_18: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] Gamma_19: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] Gamma_20: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] Gamma_21: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] 10: ~(richer(butler,agatha)), [hates(butler,butler)], ~(lives(butler)) Gamma_22: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] 10: ~(richer(butler,agatha)), [hates(butler,butler)], ~(lives(butler)) 11: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) Gamma_23: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] 10: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) 11: ~(richer(butler,agatha)), [hates(butler,butler)], ~(lives(butler)) Gamma_24: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] 10: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) 11: [~(richer(butler,agatha))], ~(hates(butler,charles)), ~(hates(butler,agatha)), ~( lives(butler)) Gamma_25: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] 10: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) 11: ~(richer(butler,agatha)), ~(hates(butler,charles)), ~(hates(butler,agatha)), [~( lives(butler))] Gamma_26: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: ~(richer(butler,agatha)), ~(hates(butler,charles)), ~(hates(butler,agatha)), [~( lives(butler))] 10: [lives(butler)] 11: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) Gamma_27: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: ~(richer(butler,agatha)), ~(hates(butler,charles)), ~(hates(butler,agatha)), [~( lives(butler))] 10: [~(richer(butler,agatha))], ~(hates(butler,charles)), ~(hates(butler,agatha)) 11: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) Gamma_28: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: ~(richer(butler,agatha)), ~(hates(butler,charles)), ~(hates(butler,agatha)), [~( lives(butler))] 10: ~(richer(butler,agatha)), ~(hates(butler,charles)), [~(hates(butler,agatha))] 11: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) Gamma_29: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(richer(butler,agatha)), ~(hates(butler,charles)), [~(hates(butler,agatha))] 7: ~(killed(butler,agatha)), [hates(butler,agatha)] 8: [hates(agatha,agatha)] 9: [lives(charles)] 10: ~(richer(butler,agatha)), ~(hates(butler,charles)), ~(hates(butler,agatha)), [~( lives(butler))] 11: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) Gamma_30: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(richer(butler,agatha)), ~(hates(butler,charles)), [~(hates(butler,agatha))] 7: ~(richer(butler,agatha)), [~(killed(butler,agatha))], ~(hates(butler,charles)) 8: [hates(agatha,agatha)] 9: [lives(charles)] Gamma_31: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(richer(butler,agatha)), ~(hates(butler,charles)), [~(hates(butler,agatha))] 7: [~(richer(butler,agatha))], ~(killed(butler,agatha)), ~(hates(butler,charles)) 8: [hates(agatha,agatha)] 9: [lives(charles)] Gamma_32: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [~(richer(butler,agatha))], ~(killed(butler,agatha)), ~(hates(butler,charles)) 6: [richer(butler,agatha)], ~(killed(butler,agatha)) 7: ~(richer(butler,agatha)), ~(hates(butler,charles)), [~(hates(butler,agatha))] 8: [hates(agatha,agatha)] 9: [lives(charles)] Gamma_33: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [~(richer(butler,agatha))], ~(killed(butler,agatha)), ~(hates(butler,charles)) 6: [~(killed(butler,agatha))], ~(hates(butler,charles)) 7: [hates(agatha,agatha)] 8: [lives(charles)] Gamma_34: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [~(richer(butler,agatha))], ~(killed(butler,agatha)), ~(hates(butler,charles)) 6: ~(killed(butler,agatha)), [~(hates(butler,charles))] 7: [hates(agatha,agatha)] 8: [lives(charles)] Gamma_35: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: ~(killed(butler,agatha)), [~(hates(butler,charles))] 5: [hates(butler,charles)], ~(hates(agatha,charles)) 6: [~(richer(butler,agatha))], ~(killed(butler,agatha)), ~(hates(butler,charles)) 7: [hates(agatha,agatha)] 8: [lives(charles)] Gamma_36: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: ~(killed(butler,agatha)), [~(hates(butler,charles))] 5: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_37: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: ~(killed(butler,agatha)), [~(hates(butler,charles))] 5: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_38: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 4: [hates(agatha,charles)] 5: ~(killed(butler,agatha)), [~(hates(butler,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_39: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 4: [~(killed(butler,agatha))] 5: ~(killed(butler,agatha)), [~(hates(butler,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_40: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 4: [~(killed(butler,agatha))] 5: ~(killed(butler,agatha)), [~(hates(butler,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_41: (move) 0: [~(killed(charles,agatha))] 1: [~(killed(butler,agatha))] 2: [killed(butler,agatha)] 3: [~(hates(charles,agatha))] 4: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 5: ~(killed(butler,agatha)), [~(hates(butler,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_42: (resolve) 0: [~(killed(charles,agatha))] 1: [~(killed(butler,agatha))] 2: [] 3: [~(hates(charles,agatha))] 4: [hates(agatha,agatha)] 5: [lives(charles)] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... flip all literals with predicate richer use I- Gamma_0: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) Gamma_1: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) Gamma_2: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] Gamma_3: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] Gamma_4: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_5: (extend-no-conflict) 0: [killed(charles,agatha)], killed( butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [hates(agatha,agatha)] Gamma_6: (extend-conflict) 0: [killed(charles,agatha)], killed(butler, agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [hates(agatha,agatha)] 6: ~(hates(charles,agatha)), [~(hates(agatha,agatha))] Gamma_7: (move) 0: [killed(charles,agatha)], killed(butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: ~(hates(charles,agatha)), [~(hates(agatha,agatha))] 6: [hates(agatha,agatha)] Gamma_8: (resolve) 0: [killed(charles,agatha)], killed(butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: ~(hates(charles,agatha)), [~(hates(agatha,agatha))] 6: [~(hates(charles,agatha))] Gamma_9: (extend-conflict) 0: [killed(charles,agatha)], killed(butler, agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: ~(killed(charles,agatha)), [hates(charles,agatha)] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: ~(hates(charles,agatha)), [~(hates(agatha,agatha))] 6: [~(hates(charles,agatha))] Gamma_10: (move) 0: [killed(charles,agatha)], killed(butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: [~(hates(charles,agatha))] 3: ~(killed(charles,agatha)), [hates(charles,agatha)] 4: [hates(agatha,charles)] 5: [hates(butler,charles)], ~(hates(agatha,charles)) 6: ~(hates(charles,agatha)), [~(hates(agatha,agatha))] Gamma_11: (resolve) 0: [killed(charles,agatha)], killed(butler,agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: [~(hates(charles,agatha))] 3: [~(killed(charles,agatha))] 4: [hates(agatha,charles)] 5: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_12: (extend-conflict) 0: [killed(charles,agatha)], killed(butler, agatha) 1: [richer(charles,agatha)], ~(killed(charles,agatha)) 2: [~(hates(charles,agatha))] 3: [~(killed(charles,agatha))] 4: [hates(agatha,charles)] 5: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_13: (move) 0: [~(killed(charles,agatha))] 1: [killed(charles,agatha)], killed(butler,agatha) 2: [richer(charles,agatha)], ~(killed(charles,agatha)) 3: [~(hates(charles,agatha))] 4: [hates(agatha,charles)] 5: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_14: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_15: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) Gamma_16: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) Gamma_17: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] Gamma_18: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] Gamma_19: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] Gamma_20: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] Gamma_21: (extend-no-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] 10: ~(richer(butler,agatha)), [hates(butler,butler)], ~(lives(butler)) Gamma_22: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] 10: ~(richer(butler,agatha)), [hates(butler,butler)], ~(lives(butler)) 11: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) Gamma_23: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] 10: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) 11: ~(richer(butler,agatha)), [hates(butler,butler)], ~(lives(butler)) Gamma_24: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] 10: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) 11: [~(richer(butler,agatha))], ~(hates(butler,charles)), ~(hates(butler,agatha)), ~( lives(butler)) Gamma_25: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: [lives(butler)] 10: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) 11: ~(richer(butler,agatha)), ~(hates(butler,charles)), ~(hates(butler,agatha)), [~( lives(butler))] Gamma_26: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: ~(richer(butler,agatha)), ~(hates(butler,charles)), ~(hates(butler,agatha)), [~( lives(butler))] 10: [lives(butler)] 11: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) Gamma_27: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: ~(richer(butler,agatha)), ~(hates(butler,charles)), ~(hates(butler,agatha)), [~( lives(butler))] 10: [~(richer(butler,agatha))], ~(hates(butler,charles)), ~(hates(butler,agatha)) 11: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) Gamma_28: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(killed(butler,agatha)), [hates(butler,agatha)] 7: [hates(agatha,agatha)] 8: [lives(charles)] 9: ~(richer(butler,agatha)), ~(hates(butler,charles)), ~(hates(butler,agatha)), [~( lives(butler))] 10: ~(richer(butler,agatha)), ~(hates(butler,charles)), [~(hates(butler,agatha))] 11: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) Gamma_29: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(richer(butler,agatha)), ~(hates(butler,charles)), [~(hates(butler,agatha))] 7: ~(killed(butler,agatha)), [hates(butler,agatha)] 8: [hates(agatha,agatha)] 9: [lives(charles)] 10: ~(richer(butler,agatha)), ~(hates(butler,charles)), ~(hates(butler,agatha)), [~( lives(butler))] 11: ~(hates(butler,charles)), [~(hates(butler,butler))], ~(hates(butler,agatha)) Gamma_30: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(richer(butler,agatha)), ~(hates(butler,charles)), [~(hates(butler,agatha))] 7: ~(richer(butler,agatha)), [~(killed(butler,agatha))], ~(hates(butler,charles)) 8: [hates(agatha,agatha)] 9: [lives(charles)] Gamma_31: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [richer(butler,agatha)], ~(killed(butler,agatha)) 6: ~(richer(butler,agatha)), ~(hates(butler,charles)), [~(hates(butler,agatha))] 7: [~(richer(butler,agatha))], ~(killed(butler,agatha)), ~(hates(butler,charles)) 8: [hates(agatha,agatha)] 9: [lives(charles)] Gamma_32: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [~(richer(butler,agatha))], ~(killed(butler,agatha)), ~(hates(butler,charles)) 6: [richer(butler,agatha)], ~(killed(butler,agatha)) 7: ~(richer(butler,agatha)), ~(hates(butler,charles)), [~(hates(butler,agatha))] 8: [hates(agatha,agatha)] 9: [lives(charles)] Gamma_33: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [~(richer(butler,agatha))], ~(killed(butler,agatha)), ~(hates(butler,charles)) 6: [~(killed(butler,agatha))], ~(hates(butler,charles)) 7: [hates(agatha,agatha)] 8: [lives(charles)] Gamma_34: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: [hates(butler,charles)], ~(hates(agatha,charles)) 5: [~(richer(butler,agatha))], ~(killed(butler,agatha)), ~(hates(butler,charles)) 6: ~(killed(butler,agatha)), [~(hates(butler,charles))] 7: [hates(agatha,agatha)] 8: [lives(charles)] Gamma_35: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: ~(killed(butler,agatha)), [~(hates(butler,charles))] 5: [hates(butler,charles)], ~(hates(agatha,charles)) 6: [~(richer(butler,agatha))], ~(killed(butler,agatha)), ~(hates(butler,charles)) 7: [hates(agatha,agatha)] 8: [lives(charles)] Gamma_36: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: ~(killed(butler,agatha)), [~(hates(butler,charles))] 5: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_37: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: [hates(agatha,charles)] 4: ~(killed(butler,agatha)), [~(hates(butler,charles))] 5: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_38: (move) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 4: [hates(agatha,charles)] 5: ~(killed(butler,agatha)), [~(hates(butler,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_39: (resolve) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 4: [~(killed(butler,agatha))] 5: ~(killed(butler,agatha)), [~(hates(butler,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_40: (extend-conflict) 0: [~(killed(charles,agatha))] 1: [killed(butler,agatha)] 2: [~(hates(charles,agatha))] 3: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 4: [~(killed(butler,agatha))] 5: ~(killed(butler,agatha)), [~(hates(butler,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_41: (move) 0: [~(killed(charles,agatha))] 1: [~(killed(butler,agatha))] 2: [killed(butler,agatha)] 3: [~(hates(charles,agatha))] 4: ~(killed(butler,agatha)), [~(hates(agatha,charles))] 5: ~(killed(butler,agatha)), [~(hates(butler,charles))] 6: [hates(agatha,agatha)] 7: [lives(charles)] Gamma_42: (resolve) 0: [~(killed(charles,agatha))] 1: [~(killed(butler,agatha))] 2: [] 3: [~(hates(charles,agatha))] 4: [hates(agatha,agatha)] 5: [lives(charles)] SZS status Unsatisfiable