%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------%

------ Parsing...successful


------ Proving...
flip all literals with predicate big_p
use I-

Gamma_0: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))

Gamma_1: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)

Gamma_2: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)

Gamma_3: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)

Gamma_4: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)

Gamma_5: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)

Gamma_6: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk1_0)], big_p(
esk2_0)

Gamma_7: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk1_0)], big_p(
esk2_0)
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(esk1_0)), [big_p(a)]

Gamma_8: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk1_0)], big_p(
esk2_0)
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(esk1_0)), [big_p(a)]
  8: ~(big_p(f(esk3_0))), [big_p(esk2_0)], ~(big_p(a))

Gamma_9: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk1_0)], big_p(
esk2_0)
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(esk1_0)), [big_p(a)]
  8: ~(big_p(f(esk3_0))), [big_p(esk2_0)], ~(big_p(a))
  9: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_10: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk1_0)], big_p(
esk2_0)
  7: ~(big_p(f(esk3_0))), [~(big_p(a))]
  8: ~(big_p(f(f(esk1_0)))), ~(big_p(esk1_0)), [big_p(a)]
  9: ~(big_p(f(esk3_0))), [big_p(esk2_0)], ~(big_p(a))

Gamma_11: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk1_0)], big_p(
esk2_0)
  7: ~(big_p(f(esk3_0))), [~(big_p(a))]
  8: [~(big_p(f(f(esk1_0))))], ~(big_p(f(esk3_0))), ~(big_p(esk1_0))

Gamma_12: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk1_0)], big_p(
esk2_0)
  7: ~(big_p(f(esk3_0))), [~(big_p(a))]
  8: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]

Gamma_13: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk1_0)], big_p(
esk2_0)
  8: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_14: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(f(esk1_0)))], ~(big_p(f(esk3_0))), big_p(
esk2_0)
  8: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_15: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(
esk2_0)]
  8: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_16: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(
esk2_0)]
  8: ~(big_p(f(esk3_0))), [~(big_p(a))]
  9: ~(big_p(f(f(esk2_0)))), ~(big_p(esk2_0)), [big_p(a)]

Gamma_17: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(
esk2_0)]
  8: ~(big_p(f(esk3_0))), [~(big_p(a))]
  9: [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk3_0))), ~(big_p(esk2_0))

Gamma_18: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(
esk2_0)]
  8: ~(big_p(f(esk3_0))), [~(big_p(a))]
  9: ~(big_p(f(f(esk2_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk2_0))]

Gamma_19: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(f(esk2_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk2_0))]
  8: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(
esk2_0)]
  9: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_20: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(f(esk2_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk2_0))]
  8: [~(big_p(f(f(esk1_0))))], ~(big_p(f(f(esk2_0)))), ~(big_p(f(esk1_0))), ~(
big_p(f(esk3_0)))
  9: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_21: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(f(esk2_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk2_0))]
  8: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk1_0))), ~(
big_p(f(esk3_0)))
  9: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_22: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk1_0))), ~(
big_p(f(esk3_0)))
  5: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), big_p(
esk1_0)
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  8: ~(big_p(f(f(esk2_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk2_0))]
  9: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_23: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk1_0))), ~(
big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk1_0)))), [~(big_p(f(esk1_0)))], ~(big_p(f(esk3_0))), big_p(
esk1_0)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_24: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk1_0))), ~(
big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(
esk1_0)]
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_25: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk1_0))), ~(
big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(
esk1_0)]
  7: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_26: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk1_0))), ~(
big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  6: [~(big_p(f(f(esk1_0))))], ~(big_p(f(esk1_0))), ~(big_p(f(esk3_0)))
  7: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_27: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk1_0))), ~(
big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  7: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_28: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  4: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  5: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk1_0))), ~(
big_p(f(esk3_0)))
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk3_0))), [~(big_p(esk1_0))]
  7: ~(big_p(f(esk3_0))), [~(big_p(a))]

Gamma_29: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0))), big_p(
a)

Gamma_30: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(f(esk3_0)))), ~(big_p(f(esk1_0))), [big_p(
a)]

Gamma_31: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(f(esk3_0)))), ~(big_p(f(esk1_0))), [big_p(
a)]
  5: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(esk1_0), ~(big_p(a))

Gamma_32: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(f(esk3_0)))), ~(big_p(f(esk1_0))), [big_p(
a)]
  5: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(esk1_0), ~(big_p(a))
  6: ~(big_p(f(esk1_0))), [big_p(esk1_0)], big_p(esk2_0), ~(big_p(a))

Gamma_33: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(f(esk3_0)))), ~(big_p(f(esk1_0))), [big_p(
a)]
  5: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(esk1_0), ~(big_p(a))
  6: ~(big_p(f(esk1_0))), [big_p(esk1_0)], big_p(esk2_0), ~(big_p(a))
  7: [big_p(esk2_0)], ~(big_p(a))

Gamma_34: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(f(esk3_0)))), ~(big_p(f(esk1_0))), [big_p(
a)]
  5: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(esk1_0), ~(big_p(a))
  6: ~(big_p(f(esk1_0))), [big_p(esk1_0)], big_p(esk2_0), ~(big_p(a))
  7: [big_p(esk2_0)], ~(big_p(a))
  8: [~(big_p(a))]

Gamma_35: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  4: [~(big_p(a))]
  5: ~(big_p(f(f(esk1_0)))), ~(big_p(f(f(esk3_0)))), ~(big_p(f(esk1_0))), [big_p(
a)]
  6: [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(esk1_0), ~(big_p(a))
  7: ~(big_p(f(esk1_0))), [big_p(esk1_0)], big_p(esk2_0), ~(big_p(a))
  8: [big_p(esk2_0)], ~(big_p(a))

Gamma_36: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  4: [~(big_p(a))]
  5: [~(big_p(f(f(esk1_0))))], ~(big_p(f(f(esk3_0)))), ~(big_p(f(esk1_0)))

Gamma_37: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  3: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  4: [~(big_p(a))]
  5: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))

Gamma_38: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]

Gamma_39: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]

Gamma_40: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]

Gamma_41: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)

Gamma_42: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), [big_p(esk1_0)], big_p(
esk2_0)

Gamma_43: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), [big_p(esk1_0)], big_p(
esk2_0)
  8: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)

Gamma_44: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  8: big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), [big_p(esk1_0)], big_p(
esk2_0)

Gamma_45: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  8: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk3_0)))], ~(big_p(f(esk1_0))), big_p(
esk2_0), big_p(a)

Gamma_46: (extend-no-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  8: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), [big_p(
esk2_0)], big_p(a)

Gamma_47: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  8: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), [big_p(
esk2_0)], big_p(a)
  9: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)

Gamma_48: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  8: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  9: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), [big_p(
esk2_0)], big_p(a)

Gamma_49: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  8: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  9: [~(big_p(f(f(esk1_0))))], big_p(f(f(esk3_0))), ~(big_p(f(f(esk2_0)))), ~(
big_p(f(esk1_0))), big_p(a)

Gamma_50: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  8: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  9: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), ~(big_p(f(f(esk2_0)))), ~(
big_p(f(esk1_0))), [big_p(a)]

Gamma_51: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  8: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  9: [~(big_p(f(f(esk1_0))))], big_p(f(f(esk3_0))), ~(big_p(f(f(esk2_0)))), ~(
big_p(f(esk1_0)))

Gamma_52: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  4: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  8: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  9: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))

Gamma_53: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk1_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  6: [~(big_p(a))]
  7: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  8: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  9: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)

Gamma_54: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: [~(big_p(f(f(esk1_0))))], big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), big_p(
esk1_0)
  5: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  6: [~(big_p(a))]
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)

Gamma_55: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), [big_p(
esk1_0)]
  5: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  6: [~(big_p(a))]
  7: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)

Gamma_56: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  5: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), [big_p(
esk1_0)]
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  7: [~(big_p(a))]

Gamma_57: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  5: [~(big_p(f(f(esk1_0))))], big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), big_p(
a)
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  7: [~(big_p(a))]

Gamma_58: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  5: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), [big_p(
a)]
  6: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]
  7: [~(big_p(a))]

Gamma_59: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), ~(big_p(f(esk1_0))), [big_p(
a)]
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]

Gamma_60: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  5: [~(big_p(a))]
  6: [~(big_p(f(f(esk1_0))))], big_p(f(f(esk3_0))), ~(big_p(f(esk1_0)))
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]

Gamma_61: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk1_0)))), [big_p(f(f(esk3_0)))], ~(big_p(f(esk1_0)))
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]

Gamma_62: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  5: [~(big_p(a))]
  6: [~(big_p(f(f(esk1_0))))], ~(big_p(f(esk1_0)))
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]

Gamma_63: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  3: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  5: [~(big_p(a))]
  6: ~(big_p(f(f(esk1_0)))), [~(big_p(f(esk1_0)))]
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]

Gamma_64: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [~(big_p(f(esk1_0)))]
  2: ~(big_p(f(f(esk1_0)))), [big_p(f(esk1_0))], big_p(a)
  3: ~(big_p(f(f(esk1_0)))), [~(big_p(f(f(esk3_0))))], ~(big_p(f(esk1_0)))
  4: ~(big_p(f(f(esk1_0)))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))], ~(
big_p(f(esk1_0)))
  5: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  6: [~(big_p(a))]
  7: ~(big_p(f(f(esk1_0)))), ~(big_p(f(esk1_0))), [~(big_p(f(esk3_0)))]

Gamma_65: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [~(big_p(f(esk1_0)))]
  2: [~(big_p(f(f(esk1_0))))], big_p(a)
  3: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  4: [~(big_p(a))]

Gamma_66: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [~(big_p(f(esk1_0)))]
  2: ~(big_p(f(f(esk1_0)))), [big_p(a)]
  3: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)
  4: [~(big_p(a))]

Gamma_67: (move)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [~(big_p(f(esk1_0)))]
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk1_0)))), [big_p(a)]
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)

Gamma_68: (resolve)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [~(big_p(f(esk1_0)))]
  2: [~(big_p(a))]
  3: [~(big_p(f(f(esk1_0))))]
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)

Gamma_69: (extend-conflict)
  0: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(
f(f(esk2_0)))
  1: ~(big_p(f(f(esk1_0)))), [~(big_p(f(esk1_0)))]
  2: [~(big_p(a))]
  3: [~(big_p(f(f(esk1_0))))]
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)

Gamma_70: (move)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), big_p(f(f(esk2_0)))
  2: ~(big_p(f(f(esk1_0)))), [~(big_p(f(esk1_0)))]
  3: [~(big_p(a))]
  4: ~(big_p(f(f(esk1_0)))), [~(big_p(esk1_0))], big_p(a)

Gamma_71: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]

Gamma_72: (extend-no-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]

Gamma_73: (extend-no-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)

Gamma_74: (extend-no-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk3_0)))

Gamma_75: (extend-no-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)

Gamma_76: (extend-no-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: big_p(f(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk2_0)]

Gamma_77: (extend-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: big_p(f(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk2_0)]
  7: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)

Gamma_78: (move)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  7: big_p(f(f(esk1_0))), ~(big_p(f(esk3_0))), [big_p(esk2_0)]

Gamma_79: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  7: [big_p(f(f(esk1_0)))], ~(big_p(f(f(esk2_0)))), ~(big_p(f(esk3_0))), big_p(
a)

Gamma_80: (extend-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk3_0)))
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  7: big_p(f(f(esk1_0))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk3_0))), big_p(
a)

Gamma_81: (move)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: big_p(f(f(esk1_0))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk3_0))), big_p(
a)
  5: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))], ~(big_p(f(esk3_0)))
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)

Gamma_82: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: big_p(f(f(esk1_0))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk3_0))), big_p(
a)
  5: [big_p(f(f(esk1_0)))], ~(big_p(f(esk3_0))), big_p(a)

Gamma_83: (extend-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  4: big_p(f(f(esk1_0))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk3_0))), big_p(
a)
  5: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)

Gamma_84: (move)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  4: ~(big_p(f(f(esk3_0)))), [big_p(f(esk3_0))], big_p(a)
  5: big_p(f(f(esk1_0))), [~(big_p(f(f(esk2_0))))], ~(big_p(f(esk3_0))), big_p(
a)

Gamma_85: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  4: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))], big_p(a)

Gamma_86: (extend-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  4: big_p(f(f(esk1_0))), ~(big_p(f(f(esk3_0)))), [big_p(a)]

Gamma_87: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  4: [big_p(f(f(esk1_0)))], ~(big_p(f(f(esk3_0))))

Gamma_88: (extend-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  2: [~(big_p(a))]
  3: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  4: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]

Gamma_89: (move)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: [big_p(f(f(esk3_0)))], big_p(f(f(esk2_0)))
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)

Gamma_90: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)

Gamma_91: (extend-no-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)

Gamma_92: (extend-no-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)

Gamma_93: (extend-no-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), [big_p(esk2_0)]

Gamma_94: (extend-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), [big_p(esk2_0)]
  7: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)

Gamma_95: (move)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  7: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), [big_p(esk2_0)]

Gamma_96: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  7: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), ~(big_p(f(f(esk2_0)))), big_p(
a)

Gamma_97: (extend-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  7: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), ~(big_p(f(f(esk2_0)))), [big_p(
a)]

Gamma_98: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  7: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0))), ~(big_p(f(f(esk2_0))))

Gamma_99: (extend-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  3: [~(big_p(a))]
  4: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  5: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  6: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)
  7: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))]

Gamma_100: (move)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))]
  3: big_p(f(f(esk1_0))), [big_p(f(f(esk2_0)))]
  4: [~(big_p(a))]
  5: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)
  6: ~(big_p(f(f(esk2_0)))), [big_p(f(esk2_0))], big_p(a)
  7: ~(big_p(f(f(esk2_0)))), [~(big_p(esk2_0))], big_p(a)

Gamma_101: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))]
  3: [big_p(f(f(esk1_0)))], big_p(f(f(esk3_0)))
  4: [~(big_p(a))]
  5: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)

Gamma_102: (extend-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))]
  3: big_p(f(f(esk1_0))), [big_p(f(f(esk3_0)))]
  4: [~(big_p(a))]
  5: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)

Gamma_103: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))]
  3: [big_p(f(f(esk1_0)))]
  4: [~(big_p(a))]
  5: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)

Gamma_104: (extend-conflict)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))]
  3: [big_p(f(f(esk1_0)))]
  4: [~(big_p(a))]
  5: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)

Gamma_105: (resolve)
  0: [~(big_p(f(f(esk1_0))))]
  1: big_p(f(f(esk1_0))), [~(big_p(f(f(esk3_0))))]
  2: big_p(f(f(esk1_0))), big_p(f(f(esk3_0))), [~(big_p(f(f(esk2_0))))]
  3: []
  4: [~(big_p(a))]
  5: big_p(f(f(esk1_0))), [~(big_p(f(esk3_0)))], big_p(a)

SZS status Unsatisfiable