%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] Gamma_1: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) Gamma_2: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] Gamma_3: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] Gamma_4: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) Gamma_5: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) Gamma_6: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] Gamma_7: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] Gamma_8: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] Gamma_9: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) Gamma_10: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) Gamma_11: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 11: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)), [banks( west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast)] Gamma_12: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 11: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)), [banks( west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast)] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_13: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 11: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] 12: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)), [banks( west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast)] Gamma_14: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 11: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] 12: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] Gamma_15: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 11: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] 12: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] Gamma_16: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 11: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_17: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 11: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_18: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 11: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_19: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 10: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_20: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 10: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_21: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 10: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_22: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 9: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_23: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 9: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_24: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 9: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_25: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 8: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_26: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 8: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_27: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 8: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_28: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 7: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_29: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 7: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_30: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 7: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_31: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 6: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_32: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 6: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_33: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 6: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_34: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 5: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_35: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 5: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_36: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 5: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_37: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 4: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_38: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 4: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_39: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 4: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_40: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 3: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_41: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 3: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_42: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 3: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_43: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 2: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 3: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_44: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 2: [~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest))] 3: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_45: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 2: [~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest))] 3: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_46: (move) 0: [~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest))] 1: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 2: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 3: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_47: (resolve) 0: [~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest))] 1: [] 2: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 3: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] Gamma_1: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) Gamma_2: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] Gamma_3: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] Gamma_4: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) Gamma_5: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) Gamma_6: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] Gamma_7: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] Gamma_8: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] Gamma_9: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) Gamma_10: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) Gamma_11: (extend-no-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 11: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)), [banks( west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast)] Gamma_12: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 11: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)), [banks( west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast)] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_13: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 11: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] 12: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)), [banks( west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast)] Gamma_14: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 11: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] 12: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] Gamma_15: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 11: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] 12: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] Gamma_16: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 11: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest)], ~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)) 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_17: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 11: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_18: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 10: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 11: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_19: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 10: [banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast)], ~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)) 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_20: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 10: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_21: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 9: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 10: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_22: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 9: ~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)), [banks( west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest)] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_23: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 9: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_24: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 8: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 9: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_25: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 8: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)), [banks( west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast)] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_26: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 8: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_27: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 7: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 8: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_28: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 7: ~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)), [banks( west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest)] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_29: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 7: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_30: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 6: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 7: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_31: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 6: [banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast)], ~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)) 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_32: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 6: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_33: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 5: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 6: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_34: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 5: [banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest)], ~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)) 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_35: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 5: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_36: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 4: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 5: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_37: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 4: ~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)), [banks( west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast)] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_38: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 4: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_39: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 3: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 4: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_40: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 3: ~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)), [banks( west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest)] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_41: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 3: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_42: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 2: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 3: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_43: (move) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 1: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 2: [banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast)], ~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)) 3: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_44: (resolve) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 2: [~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest))] 3: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_45: (extend-conflict) 0: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)), boatonwest)] 1: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 2: [~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest))] 3: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_46: (move) 0: [~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest))] 1: [banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest)] 2: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 3: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] Gamma_47: (resolve) 0: [~(banks(west(m(n3),c(n3)),east(m(n0),c(n0)),boatonwest))] 1: [] 2: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatoneast))] 3: [~(banks(west(m(n3),c(n2)),east(m(n0),c(n1)),boatonwest))] 4: [~(banks(west(m(n3),c(n0)),east(m(n0),c(n3)),boatoneast))] 5: [~(banks(west(m(n3),c(n1)),east(m(n0),c(n2)),boatonwest))] 6: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatoneast))] 7: [~(banks(west(m(n2),c(n2)),east(m(n1),c(n1)),boatonwest))] 8: [~(banks(west(m(n0),c(n2)),east(m(n3),c(n1)),boatoneast))] 9: [~(banks(west(m(n0),c(n3)),east(m(n3),c(n0)),boatonwest))] 10: [~(banks(west(m(n0),c(n1)),east(m(n3),c(n2)),boatoneast))] 11: [~(banks(west(m(n1),c(n1)),east(m(n2),c(n2)),boatonwest))] 12: [~(banks(west(m(n0),c(n0)),east(m(n3),c(n3)),boatoneast))] SZS status Unsatisfiable