%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) Gamma_1: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] Gamma_2: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] Gamma_3: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) Gamma_4: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) Gamma_5: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) Gamma_6: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) Gamma_7: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) Gamma_8: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) Gamma_9: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) Gamma_10: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] Gamma_11: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 11: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_12: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 11: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] Gamma_13: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 11: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] 12: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_14: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 11: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk4_0))], ~( big_f(esk3_0)) Gamma_15: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 11: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), [~( big_f(esk3_0))] Gamma_16: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), [~( big_f(esk3_0))] 11: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] Gamma_17: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), [~( big_f(esk3_0))] 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] Gamma_18: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), [~( big_f(esk3_0))] 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] Gamma_19: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 10: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 11: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), [~( big_f(esk3_0))] 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] Gamma_20: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 10: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) Gamma_21: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 10: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) Gamma_22: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) Gamma_23: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: [~(big_j(esk4_0))], ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), big_f( esk3_0) 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) Gamma_24: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) Gamma_25: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 11: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_26: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 11: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_27: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 11: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) 12: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_28: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 11: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) 12: ~(big_j(esk4_0)), big_g(esk6_0), [~(big_g(esk4_0))], ~(big_f(esk3_0)) Gamma_29: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 11: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) 12: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] Gamma_30: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 10: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_31: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 10: [~(big_j(esk4_0))], ~(big_h(esk5_0)), big_g(esk6_0), ~(big_g(esk4_0)), ~( big_f(esk5_0)) 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_32: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 10: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_g(esk6_0)], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_33: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 10: [~(big_j(esk4_0))], ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)) 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_34: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 10: ~(big_j(esk4_0)), [~(big_h(esk5_0))], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_35: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: ~(big_j(esk4_0)), [~(big_h(esk5_0))], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 10: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_36: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: ~(big_j(esk4_0)), [~(big_h(esk5_0))], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [~(big_g(esk4_0))], ~(big_f(esk5_0)) Gamma_37: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: ~(big_j(esk4_0)), [~(big_h(esk5_0))], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] Gamma_38: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 8: ~(big_j(esk4_0)), [~(big_h(esk5_0))], ~(big_g(esk4_0)), ~(big_f(esk5_0)) Gamma_39: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: [~(big_j(esk4_0))], ~(big_g(esk4_0)), big_f(esk3_0) Gamma_40: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] Gamma_41: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 8: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_42: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 8: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_43: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 8: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) 9: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_44: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 8: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) 9: ~(big_j(esk4_0)), [~(big_g(esk4_0))], big_f(esk5_0), ~(big_f(esk3_0)) Gamma_45: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 8: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) 9: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] Gamma_46: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 8: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_47: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 8: [~(big_j(esk4_0))], ~(big_g(esk4_0)), big_f(esk5_0) 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_48: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 8: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk5_0)] 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_49: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 8: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_50: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 8: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_51: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 5: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 8: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_52: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 5: [~(big_g(esk4_0))], ~(big_f(esk1_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) Gamma_53: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 5: ~(big_g(esk4_0)), [~(big_f(esk1_0))] 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) Gamma_54: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: ~(big_g(esk4_0)), [~(big_f(esk1_0))] 3: [big_f(esk1_0)] 4: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) Gamma_55: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: ~(big_g(esk4_0)), [~(big_f(esk1_0))] 3: [~(big_g(esk4_0))] 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) Gamma_56: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: ~(big_g(esk4_0)), [~(big_f(esk1_0))] 3: [~(big_g(esk4_0))] 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) Gamma_57: (move) 0: [~(big_g(esk4_0))] 1: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 2: [big_g(esk2_0)] 3: ~(big_g(esk4_0)), [~(big_f(esk1_0))] 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) Gamma_58: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] Gamma_59: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] Gamma_60: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) Gamma_61: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) Gamma_62: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) Gamma_63: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) Gamma_64: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] Gamma_65: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 8: [big_h(esk3_0)], ~(big_g(esk6_0)), ~(big_f(esk3_0)) Gamma_66: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 8: [big_h(esk3_0)], ~(big_g(esk6_0)), ~(big_f(esk3_0)) 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) Gamma_67: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 8: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) 9: [big_h(esk3_0)], ~(big_g(esk6_0)), ~(big_f(esk3_0)) Gamma_68: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 8: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~( big_f(esk3_0)) Gamma_69: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 8: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0), [~( big_f(esk3_0))] Gamma_70: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0), [~( big_f(esk3_0))] 8: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) Gamma_71: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0), [~( big_f(esk3_0))] 8: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) Gamma_72: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0), [~( big_f(esk3_0))] 8: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) Gamma_73: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) 7: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk6_0)), ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0), [~( big_f(esk3_0))] 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) Gamma_74: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) 7: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) Gamma_75: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) 7: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) Gamma_76: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 7: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) Gamma_77: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), [big_g(esk4_0)], ~(big_f(esk5_0)), big_f(esk3_0) Gamma_78: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] Gamma_79: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 7: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_80: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 7: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_81: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 7: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) 8: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_82: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 7: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) 8: big_g(esk6_0), big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk3_0)) Gamma_83: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 7: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) 8: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] Gamma_84: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 7: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_85: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 7: [~(big_h(esk5_0))], big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), ~( big_f(esk5_0)) 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_86: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 7: ~(big_h(esk5_0)), [big_g(esk6_0)], big_g(esk4_0), ~(big_g(esk2_0)), ~( big_f(esk5_0)) 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_87: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 7: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_88: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 7: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_89: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 7: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_90: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) Gamma_91: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) Gamma_92: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) 3: [big_g(esk2_0)] 4: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) Gamma_93: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) 3: [big_g(esk4_0)], ~(big_f(esk5_0)) Gamma_94: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) 3: big_g(esk4_0), [~(big_f(esk5_0))] Gamma_95: (move) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: [big_f(esk5_0)], big_f(esk3_0) 3: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) Gamma_96: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] Gamma_97: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] Gamma_98: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] Gamma_99: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_100: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_101: (extend-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) 6: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_102: (move) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) 5: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_103: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) 5: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_104: (extend-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) 5: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_105: (move) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 4: [big_g(esk2_0)] 5: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_106: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 4: [big_g(esk4_0)], big_f(esk5_0), ~(big_f(esk3_0)) 5: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_107: (extend-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 4: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 5: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_108: (move) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: big_g(esk4_0), [big_f(esk3_0)] 4: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 5: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_109: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: [big_g(esk4_0)], big_f(esk5_0) 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_110: (extend-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: big_g(esk4_0), [big_f(esk5_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_111: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: [big_g(esk4_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_112: (extend-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: [big_g(esk4_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_113: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: [] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) Gamma_1: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] Gamma_2: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] Gamma_3: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) Gamma_4: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) Gamma_5: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) Gamma_6: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) Gamma_7: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) Gamma_8: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) Gamma_9: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) Gamma_10: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] Gamma_11: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 11: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_12: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 11: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] Gamma_13: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 11: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] 12: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_14: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 11: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk4_0))], ~( big_f(esk3_0)) Gamma_15: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 11: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), [~( big_f(esk3_0))] Gamma_16: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), [~( big_f(esk3_0))] 11: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_f(esk3_0)] 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] Gamma_17: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), [~( big_f(esk3_0))] 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] Gamma_18: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 10: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), [~( big_f(esk3_0))] 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] Gamma_19: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 10: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 11: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), [~( big_f(esk3_0))] 12: ~(big_j(esk6_0)), ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))] Gamma_20: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 10: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) Gamma_21: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 9: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 10: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) Gamma_22: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), [big_g(esk6_0)], big_f(esk3_0) 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) Gamma_23: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: [~(big_j(esk4_0))], ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), big_f( esk3_0) 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) Gamma_24: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) Gamma_25: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 11: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_26: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 11: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_27: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 11: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) 12: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_28: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 11: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) 12: ~(big_j(esk4_0)), big_g(esk6_0), [~(big_g(esk4_0))], ~(big_f(esk3_0)) Gamma_29: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 10: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 11: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) 12: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] Gamma_30: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 10: ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)), [big_f( esk3_0)] 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_31: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 10: [~(big_j(esk4_0))], ~(big_h(esk5_0)), big_g(esk6_0), ~(big_g(esk4_0)), ~( big_f(esk5_0)) 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_32: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 10: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [big_g(esk6_0)], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_33: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 10: [~(big_j(esk4_0))], ~(big_h(esk5_0)), ~(big_g(esk4_0)), ~(big_f(esk5_0)) 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_34: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 9: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 10: ~(big_j(esk4_0)), [~(big_h(esk5_0))], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_35: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: ~(big_j(esk4_0)), [~(big_h(esk5_0))], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: [big_h(esk5_0)], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 9: ~(big_j(esk4_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], ~(big_g(esk4_0)), ~( big_f(esk5_0)) 10: ~(big_j(esk4_0)), big_g(esk6_0), ~(big_g(esk4_0)), [~(big_f(esk3_0))] 11: [~(big_j(esk6_0))], ~(big_j(esk4_0)), ~(big_h(esk5_0)), ~(big_g(esk4_0)) 12: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_g(esk6_0) Gamma_36: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: ~(big_j(esk4_0)), [~(big_h(esk5_0))], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), [~(big_g(esk4_0))], ~(big_f(esk5_0)) Gamma_37: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 7: ~(big_j(esk4_0)), [~(big_h(esk5_0))], ~(big_g(esk4_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] Gamma_38: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), [big_f(esk5_0)], big_f(esk3_0) 8: ~(big_j(esk4_0)), [~(big_h(esk5_0))], ~(big_g(esk4_0)), ~(big_f(esk5_0)) Gamma_39: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: [~(big_j(esk4_0))], ~(big_g(esk4_0)), big_f(esk3_0) Gamma_40: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] Gamma_41: (extend-no-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 8: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_42: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 8: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_43: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 8: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) 9: [big_h(esk3_0)], ~(big_g(esk4_0)), ~(big_f(esk3_0)) Gamma_44: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 8: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) 9: ~(big_j(esk4_0)), [~(big_g(esk4_0))], big_f(esk5_0), ~(big_f(esk3_0)) Gamma_45: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 8: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) 9: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] Gamma_46: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 8: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk3_0)] 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_47: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 8: [~(big_j(esk4_0))], ~(big_g(esk4_0)), big_f(esk5_0) 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_48: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 8: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [big_f(esk5_0)] 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_49: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 8: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_50: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 6: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 8: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_51: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 5: [big_j(esk4_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) 7: ~(big_j(esk4_0)), ~(big_g(esk4_0)), [~(big_f(esk5_0))] 8: ~(big_j(esk4_0)), ~(big_g(esk4_0)), big_f(esk5_0), [~(big_f(esk3_0))] 9: ~(big_j(esk4_0)), [~(big_h(esk3_0))], big_f(esk5_0) Gamma_52: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 5: [~(big_g(esk4_0))], ~(big_f(esk1_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) Gamma_53: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: [big_f(esk1_0)] 3: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 5: ~(big_g(esk4_0)), [~(big_f(esk1_0))] 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) Gamma_54: (move) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: ~(big_g(esk4_0)), [~(big_f(esk1_0))] 3: [big_f(esk1_0)] 4: [big_h(esk1_0)], ~(big_g(esk4_0)), ~(big_f(esk1_0)) 5: [~(big_j(esk4_0))], ~(big_g(esk4_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk1_0)) Gamma_55: (resolve) 0: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 1: [big_g(esk2_0)] 2: ~(big_g(esk4_0)), [~(big_f(esk1_0))] 3: [~(big_g(esk4_0))] 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) Gamma_56: (extend-conflict) 0: [big_g(esk4_0)], big_f(esk5_0), big_f( esk3_0) 1: [big_g(esk2_0)] 2: ~(big_g(esk4_0)), [~(big_f(esk1_0))] 3: [~(big_g(esk4_0))] 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) Gamma_57: (move) 0: [~(big_g(esk4_0))] 1: [big_g(esk4_0)], big_f(esk5_0), big_f(esk3_0) 2: [big_g(esk2_0)] 3: ~(big_g(esk4_0)), [~(big_f(esk1_0))] 4: [~(big_j(esk4_0))], ~(big_g(esk4_0)) Gamma_58: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] Gamma_59: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] Gamma_60: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) Gamma_61: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) Gamma_62: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) Gamma_63: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) Gamma_64: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] Gamma_65: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 8: [big_h(esk3_0)], ~(big_g(esk6_0)), ~(big_f(esk3_0)) Gamma_66: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 8: [big_h(esk3_0)], ~(big_g(esk6_0)), ~(big_f(esk3_0)) 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) Gamma_67: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 8: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) 9: [big_h(esk3_0)], ~(big_g(esk6_0)), ~(big_f(esk3_0)) Gamma_68: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 8: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~( big_f(esk3_0)) Gamma_69: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 8: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0), [~( big_f(esk3_0))] Gamma_70: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0), [~( big_f(esk3_0))] 8: ~(big_j(esk6_0)), ~(big_h(esk5_0)), big_g(esk4_0), [big_f(esk3_0)] 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) Gamma_71: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0), [~( big_f(esk3_0))] 8: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) Gamma_72: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 7: ~(big_j(esk6_0)), ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0), [~( big_f(esk3_0))] 8: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) Gamma_73: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) 7: [big_j(esk6_0)], ~(big_g(esk6_0)), ~(big_f(esk5_0)) 8: ~(big_j(esk6_0)), ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0), [~( big_f(esk3_0))] 9: ~(big_j(esk6_0)), ~(big_h(esk5_0)), [~(big_h(esk3_0))], big_g(esk4_0) Gamma_74: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) 7: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) Gamma_75: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 6: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) 7: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) Gamma_76: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: [big_g(esk6_0)], big_g(esk4_0), big_f(esk3_0) 7: [~(big_j(esk6_0))], ~(big_h(esk5_0)), ~(big_g(esk6_0)), big_g(esk4_0) Gamma_77: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), [big_g(esk4_0)], ~(big_f(esk5_0)), big_f(esk3_0) Gamma_78: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] Gamma_79: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 7: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_80: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 7: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_81: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 7: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) 8: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_82: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 7: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) 8: big_g(esk6_0), big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk3_0)) Gamma_83: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 7: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) 8: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] Gamma_84: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 7: ~(big_h(esk5_0)), big_g(esk4_0), ~(big_f(esk5_0)), [big_f(esk3_0)] 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_85: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 7: [~(big_h(esk5_0))], big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), ~( big_f(esk5_0)) 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_86: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 7: ~(big_h(esk5_0)), [big_g(esk6_0)], big_g(esk4_0), ~(big_g(esk2_0)), ~( big_f(esk5_0)) 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_87: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 7: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_88: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 6: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 7: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_89: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: [big_h(esk5_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) 6: ~(big_h(esk5_0)), [~(big_g(esk6_0))], big_g(esk4_0), ~(big_f(esk5_0)) 7: big_g(esk6_0), big_g(esk4_0), ~(big_g(esk2_0)), [~(big_f(esk3_0))] 8: [~(big_h(esk3_0))], big_g(esk6_0), big_g(esk4_0) Gamma_90: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) Gamma_91: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: [big_g(esk2_0)] 3: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 4: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) Gamma_92: (move) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) 3: [big_g(esk2_0)] 4: [~(big_h(esk5_0))], big_g(esk4_0), ~(big_g(esk2_0)), ~(big_f(esk5_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk5_0)) Gamma_93: (resolve) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) 3: [big_g(esk4_0)], ~(big_f(esk5_0)) Gamma_94: (extend-conflict) 0: [~(big_g(esk4_0))] 1: [big_f(esk5_0)], big_f(esk3_0) 2: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) 3: big_g(esk4_0), [~(big_f(esk5_0))] Gamma_95: (move) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: [big_f(esk5_0)], big_f(esk3_0) 3: big_g(esk4_0), [~(big_g(esk2_0))], ~(big_f(esk5_0)) Gamma_96: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] Gamma_97: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] Gamma_98: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] Gamma_99: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_100: (extend-no-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_101: (extend-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) 5: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) 6: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_102: (move) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) 5: [big_h(esk3_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_103: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) 5: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_104: (extend-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: [big_g(esk2_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) 5: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_105: (move) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 4: [big_g(esk2_0)] 5: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) 6: [big_j(esk2_0)], ~(big_g(esk2_0)), ~(big_f(esk3_0)) Gamma_106: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 4: [big_g(esk4_0)], big_f(esk5_0), ~(big_f(esk3_0)) 5: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_107: (extend-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), [big_f(esk3_0)] 3: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 4: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 5: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_108: (move) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: big_g(esk4_0), [big_f(esk3_0)] 4: big_g(esk4_0), [~(big_g(esk2_0))], big_f(esk5_0), ~(big_f(esk3_0)) 5: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_109: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: [big_g(esk4_0)], big_f(esk5_0) 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_110: (extend-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: big_g(esk4_0), [big_f(esk5_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_111: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: [big_g(esk4_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_112: (extend-conflict) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: [big_g(esk4_0)] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) Gamma_113: (resolve) 0: [~(big_g(esk4_0))] 1: big_g(esk4_0), [~(big_f(esk5_0))] 2: big_g(esk4_0), big_f(esk5_0), [~(big_f(esk3_0))] 3: [] 4: [~(big_h(esk3_0))], big_g(esk4_0), big_f(esk5_0) SZS status Unsatisfiable