%---------------- 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(sk2)))], big_p(f(f(sk1)))

Gamma_1: (extend-no-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)

Gamma_2: (extend-no-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)

Gamma_3: (extend-no-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)

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

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

Gamma_6: (extend-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(sk2))), ~(big_p(f(sk1))), [big_p(sk2)], big_p(sk1)
  5: ~(big_p(f(f(sk2)))), ~(big_p(sk2)), [big_p(a)]
  6: [~(big_p(a))]

Gamma_7: (move)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(sk2))), ~(big_p(f(sk1))), [big_p(sk2)], big_p(sk1)
  5: [~(big_p(a))]
  6: ~(big_p(f(f(sk2)))), ~(big_p(sk2)), [big_p(a)]

Gamma_8: (resolve)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(sk2))), ~(big_p(f(sk1))), [big_p(sk2)], big_p(sk1)
  5: [~(big_p(a))]
  6: [~(big_p(f(f(sk2))))], ~(big_p(sk2))

Gamma_9: (extend-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(sk2))), ~(big_p(f(sk1))), [big_p(sk2)], big_p(sk1)
  5: [~(big_p(a))]
  6: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]

Gamma_10: (move)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  5: ~(big_p(f(sk2))), ~(big_p(f(sk1))), [big_p(sk2)], big_p(sk1)
  6: [~(big_p(a))]

Gamma_11: (resolve)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  5: ~(big_p(f(f(sk2)))), [~(big_p(f(sk2)))], ~(big_p(f(sk1))), big_p(
sk1)
  6: [~(big_p(a))]

Gamma_12: (extend-no-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  5: ~(big_p(f(f(sk2)))), ~(big_p(f(sk2))), ~(big_p(f(sk1))), [big_p(
sk1)]
  6: [~(big_p(a))]

Gamma_13: (extend-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  5: ~(big_p(f(f(sk2)))), ~(big_p(f(sk2))), ~(big_p(f(sk1))), [big_p(
sk1)]
  6: [~(big_p(a))]
  7: ~(big_p(f(f(sk1)))), ~(big_p(sk1)), [big_p(a)]

Gamma_14: (resolve)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  5: ~(big_p(f(f(sk2)))), ~(big_p(f(sk2))), ~(big_p(f(sk1))), [big_p(
sk1)]
  6: [~(big_p(a))]
  7: [~(big_p(f(f(sk1))))], ~(big_p(sk1))

Gamma_15: (extend-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  5: ~(big_p(f(f(sk2)))), ~(big_p(f(sk2))), ~(big_p(f(sk1))), [big_p(
sk1)]
  6: [~(big_p(a))]
  7: ~(big_p(f(f(sk1)))), [~(big_p(sk1))]

Gamma_16: (move)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  5: ~(big_p(f(f(sk1)))), [~(big_p(sk1))]
  6: ~(big_p(f(f(sk2)))), ~(big_p(f(sk2))), ~(big_p(f(sk1))), [big_p(
sk1)]
  7: [~(big_p(a))]

Gamma_17: (resolve)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  5: ~(big_p(f(f(sk1)))), [~(big_p(sk1))]
  6: [~(big_p(f(f(sk2))))], ~(big_p(f(f(sk1)))), ~(big_p(f(sk2))), ~(
big_p(f(sk1)))
  7: [~(big_p(a))]

Gamma_18: (extend-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  5: ~(big_p(f(f(sk1)))), [~(big_p(sk1))]
  6: ~(big_p(f(f(sk2)))), ~(big_p(f(f(sk1)))), ~(big_p(f(sk2))), [~(big_p(f(sk1)))]
  7: [~(big_p(a))]

Gamma_19: (move)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk2)))), ~(big_p(f(f(sk1)))), ~(big_p(f(sk2))), [~(big_p(f(sk1)))]
  4: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  5: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  6: ~(big_p(f(f(sk1)))), [~(big_p(sk1))]
  7: [~(big_p(a))]

Gamma_20: (resolve)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk2)))), ~(big_p(f(f(sk1)))), ~(big_p(f(sk2))), [~(big_p(f(sk1)))]
  4: ~(big_p(f(f(sk2)))), [~(big_p(f(f(sk1))))], ~(big_p(f(sk2))), big_p(
a)
  5: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  6: ~(big_p(f(f(sk1)))), [~(big_p(sk1))]
  7: [~(big_p(a))]

Gamma_21: (extend-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk2)))), ~(big_p(f(f(sk1)))), ~(big_p(f(sk2))), [~(big_p(f(sk1)))]
  4: ~(big_p(f(f(sk2)))), ~(big_p(f(f(sk1)))), ~(big_p(f(sk2))), [big_p(
a)]
  5: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  6: ~(big_p(f(f(sk1)))), [~(big_p(sk1))]
  7: [~(big_p(a))]

Gamma_22: (move)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: [big_p(f(f(sk1)))], ~(big_p(f(sk2))), big_p(sk2)
  3: ~(big_p(f(f(sk2)))), ~(big_p(f(f(sk1)))), ~(big_p(f(sk2))), [~(big_p(f(sk1)))]
  4: [~(big_p(a))]
  5: ~(big_p(f(f(sk2)))), ~(big_p(f(f(sk1)))), ~(big_p(f(sk2))), [big_p(
a)]
  6: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  7: ~(big_p(f(f(sk1)))), [~(big_p(sk1))]

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

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

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

Gamma_26: (resolve)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: ~(big_p(f(f(sk2)))), [~(big_p(f(f(sk1))))], ~(big_p(f(sk2)))
  3: ~(big_p(f(f(sk2)))), [~(big_p(f(sk2)))], big_p(sk2)
  4: [~(big_p(a))]
  5: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]

Gamma_27: (extend-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: ~(big_p(f(f(sk2)))), [~(big_p(f(f(sk1))))], ~(big_p(f(sk2)))
  3: ~(big_p(f(f(sk2)))), ~(big_p(f(sk2))), [big_p(sk2)]
  4: [~(big_p(a))]
  5: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]

Gamma_28: (move)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: ~(big_p(f(f(sk2)))), [~(big_p(f(f(sk1))))], ~(big_p(f(sk2)))
  3: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  4: ~(big_p(f(f(sk2)))), ~(big_p(f(sk2))), [big_p(sk2)]
  5: [~(big_p(a))]

Gamma_29: (resolve)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: ~(big_p(f(f(sk2)))), [~(big_p(f(f(sk1))))], ~(big_p(f(sk2)))
  3: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  4: [~(big_p(f(f(sk2))))], ~(big_p(f(sk2)))
  5: [~(big_p(a))]

Gamma_30: (extend-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  2: ~(big_p(f(f(sk2)))), [~(big_p(f(f(sk1))))], ~(big_p(f(sk2)))
  3: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  4: ~(big_p(f(f(sk2)))), [~(big_p(f(sk2)))]
  5: [~(big_p(a))]

Gamma_31: (move)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [~(big_p(f(sk2)))]
  2: ~(big_p(f(f(sk2)))), [big_p(f(sk2))], big_p(a)
  3: ~(big_p(f(f(sk2)))), [~(big_p(f(f(sk1))))], ~(big_p(f(sk2)))
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  5: [~(big_p(a))]

Gamma_32: (resolve)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [~(big_p(f(sk2)))]
  2: [~(big_p(f(f(sk2))))], big_p(a)
  3: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  4: [~(big_p(a))]

Gamma_33: (extend-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [~(big_p(f(sk2)))]
  2: ~(big_p(f(f(sk2)))), [big_p(a)]
  3: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]
  4: [~(big_p(a))]

Gamma_34: (move)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [~(big_p(f(sk2)))]
  2: [~(big_p(a))]
  3: ~(big_p(f(f(sk2)))), [big_p(a)]
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]

Gamma_35: (resolve)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [~(big_p(f(sk2)))]
  2: [~(big_p(a))]
  3: [~(big_p(f(f(sk2))))]
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]

Gamma_36: (extend-conflict)
  0: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  1: ~(big_p(f(f(sk2)))), [~(big_p(f(sk2)))]
  2: [~(big_p(a))]
  3: [~(big_p(f(f(sk2))))]
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]

Gamma_37: (move)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk2)))], big_p(f(f(sk1)))
  2: ~(big_p(f(f(sk2)))), [~(big_p(f(sk2)))]
  3: [~(big_p(a))]
  4: ~(big_p(f(f(sk2)))), [~(big_p(sk2))]

Gamma_38: (resolve)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]

Gamma_39: (extend-no-conflict)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]

Gamma_40: (extend-no-conflict)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)

Gamma_41: (extend-no-conflict)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: big_p(f(f(sk2))), ~(big_p(f(sk1))), [big_p(sk1)]

Gamma_42: (extend-conflict)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: big_p(f(f(sk2))), ~(big_p(f(sk1))), [big_p(sk1)]
  5: ~(big_p(f(f(sk1)))), [~(big_p(sk1))], big_p(a)

Gamma_43: (move)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk1)))), [~(big_p(sk1))], big_p(a)
  5: big_p(f(f(sk2))), ~(big_p(f(sk1))), [big_p(sk1)]

Gamma_44: (resolve)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk1)))), [~(big_p(sk1))], big_p(a)
  5: [big_p(f(f(sk2)))], ~(big_p(f(f(sk1)))), ~(big_p(f(sk1))), big_p(
a)

Gamma_45: (extend-conflict)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  4: ~(big_p(f(f(sk1)))), [~(big_p(sk1))], big_p(a)
  5: big_p(f(f(sk2))), ~(big_p(f(f(sk1)))), [~(big_p(f(sk1)))], big_p(
a)

Gamma_46: (move)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: big_p(f(f(sk2))), ~(big_p(f(f(sk1)))), [~(big_p(f(sk1)))], big_p(
a)
  4: ~(big_p(f(f(sk1)))), [big_p(f(sk1))], big_p(a)
  5: ~(big_p(f(f(sk1)))), [~(big_p(sk1))], big_p(a)

Gamma_47: (resolve)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: big_p(f(f(sk2))), ~(big_p(f(f(sk1)))), [~(big_p(f(sk1)))], big_p(
a)
  4: big_p(f(f(sk2))), [~(big_p(f(f(sk1))))], big_p(a)
  5: ~(big_p(f(f(sk1)))), [~(big_p(sk1))], big_p(a)

Gamma_48: (extend-conflict)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: big_p(f(f(sk2))), ~(big_p(f(f(sk1)))), [~(big_p(f(sk1)))], big_p(
a)
  4: big_p(f(f(sk2))), ~(big_p(f(f(sk1)))), [big_p(a)]
  5: ~(big_p(f(f(sk1)))), [~(big_p(sk1))], big_p(a)

Gamma_49: (resolve)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: big_p(f(f(sk2))), ~(big_p(f(f(sk1)))), [~(big_p(f(sk1)))], big_p(
a)
  4: [big_p(f(f(sk2)))], ~(big_p(f(f(sk1))))
  5: ~(big_p(f(f(sk1)))), [~(big_p(sk1))], big_p(a)

Gamma_50: (extend-conflict)
  0: [~(big_p(f(f(sk2))))]
  1: [big_p(f(f(sk1)))]
  2: [~(big_p(a))]
  3: big_p(f(f(sk2))), ~(big_p(f(f(sk1)))), [~(big_p(f(sk1)))], big_p(
a)
  4: big_p(f(f(sk2))), [~(big_p(f(f(sk1))))]
  5: ~(big_p(f(f(sk1)))), [~(big_p(sk1))], big_p(a)

Gamma_51: (move)
  0: [~(big_p(f(f(sk2))))]
  1: big_p(f(f(sk2))), [~(big_p(f(f(sk1))))]
  2: [big_p(f(f(sk1)))]
  3: [~(big_p(a))]
  4: big_p(f(f(sk2))), ~(big_p(f(f(sk1)))), [~(big_p(f(sk1)))], big_p(
a)
  5: ~(big_p(f(f(sk1)))), [~(big_p(sk1))], big_p(a)

Gamma_52: (resolve)
  0: [~(big_p(f(f(sk2))))]
  1: big_p(f(f(sk2))), [~(big_p(f(f(sk1))))]
  2: [big_p(f(f(sk2)))]
  3: [~(big_p(a))]

Gamma_53: (extend-conflict)
  0: [~(big_p(f(f(sk2))))]
  1: big_p(f(f(sk2))), [~(big_p(f(f(sk1))))]
  2: [big_p(f(f(sk2)))]
  3: [~(big_p(a))]

Gamma_54: (resolve)
  0: [~(big_p(f(f(sk2))))]
  1: big_p(f(f(sk2))), [~(big_p(f(f(sk1))))]
  2: []
  3: [~(big_p(a))]

SZS status Unsatisfiable