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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [less_or_equal(q,n)]

Gamma_1: (extend-no-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]

Gamma_2: (extend-no-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]

Gamma_3: (extend-no-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [less_or_equal(a(p),a(q))], ~(less_or_equal(q,n)), ~(less_or_equal(m,p)), less(
p,i), less(j,q)

Gamma_4: (extend-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [less_or_equal(a(p),a(q))], ~(less_or_equal(q,n)), ~(less_or_equal(m,p)), less(
p,i), less(j,q)
  4: [~(less_or_equal(a(p),a(q)))]

Gamma_5: (move)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: [less_or_equal(a(p),a(q))], ~(less_or_equal(q,n)), ~(less_or_equal(m,p)), less(
p,i), less(j,q)

Gamma_6: (resolve)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: [~(less_or_equal(q,n))], ~(less_or_equal(m,p)), less(p,i), less(
j,q)

Gamma_7: (extend-no-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: ~(less_or_equal(q,n)), ~(less_or_equal(m,p)), [less(p,i)], less(
j,q)

Gamma_8: (extend-no-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: ~(less_or_equal(q,n)), ~(less_or_equal(m,p)), [less(p,i)], less(
j,q)
  5: [less_or_equal(i,p)], ~(less(p,i))

Gamma_9: (extend-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: ~(less_or_equal(q,n)), ~(less_or_equal(m,p)), [less(p,i)], less(
j,q)
  5: [less_or_equal(i,p)], ~(less(p,i))
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]

Gamma_10: (move)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: ~(less_or_equal(q,n)), ~(less_or_equal(m,p)), [less(p,i)], less(
j,q)
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  6: [less_or_equal(i,p)], ~(less(p,i))

Gamma_11: (resolve)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: ~(less_or_equal(q,n)), ~(less_or_equal(m,p)), [less(p,i)], less(
j,q)
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]

Gamma_12: (extend-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: ~(less_or_equal(q,n)), ~(less_or_equal(m,p)), [less(p,i)], less(
j,q)
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]

Gamma_13: (move)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: ~(less_or_equal(q,n)), ~(less_or_equal(m,p)), [less(p,i)], less(
j,q)
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]

Gamma_14: (resolve)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), [~(less_or_equal(q,n))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p)), less(j,q)
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]

Gamma_15: (extend-no-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), ~(
less_or_equal(m,p)), [less(j,q)]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]

Gamma_16: (extend-no-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), ~(
less_or_equal(m,p)), [less(j,q)]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  7: [less_or_equal(q,j)], ~(less(j,q))

Gamma_17: (extend-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), ~(
less_or_equal(m,p)), [less(j,q)]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  7: [less_or_equal(q,j)], ~(less(j,q))
  8: less_or_equal(a(p),a(q)), [~(less_or_equal(q,j))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))

Gamma_18: (move)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), ~(
less_or_equal(m,p)), [less(j,q)]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  7: less_or_equal(a(p),a(q)), [~(less_or_equal(q,j))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))
  8: [less_or_equal(q,j)], ~(less(j,q))

Gamma_19: (resolve)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), ~(
less_or_equal(m,p)), [less(j,q)]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  7: less_or_equal(a(p),a(q)), [~(less_or_equal(q,j))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))
  8: less_or_equal(a(p),a(q)), ~(less_or_equal(p,q)), ~(less_or_equal(m,p)), [~(
less(j,q))]

Gamma_20: (extend-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), ~(
less_or_equal(m,p)), [less(j,q)]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  7: less_or_equal(a(p),a(q)), [~(less_or_equal(q,j))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))
  8: less_or_equal(a(p),a(q)), ~(less_or_equal(p,q)), ~(less_or_equal(m,p)), [~(
less(j,q))]

Gamma_21: (move)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(p,q)), ~(less_or_equal(m,p)), [~(
less(j,q))]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), ~(
less_or_equal(m,p)), [less(j,q)]
  7: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  8: less_or_equal(a(p),a(q)), [~(less_or_equal(q,j))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))

Gamma_22: (resolve)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(p,q)), ~(less_or_equal(m,p)), [~(
less(j,q))]
  6: [less_or_equal(a(p),a(q))], ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))
  7: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  8: less_or_equal(a(p),a(q)), [~(less_or_equal(q,j))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))

Gamma_23: (extend-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(p,q)), ~(less_or_equal(m,p)), [~(
less(j,q))]
  6: [less_or_equal(a(p),a(q))], ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))
  7: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  8: less_or_equal(a(p),a(q)), [~(less_or_equal(q,j))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))

Gamma_24: (resolve)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(p,q)), ~(less_or_equal(m,p)), [~(
less(j,q))]
  6: [~(less_or_equal(q,n))], ~(less_or_equal(p,q)), ~(less_or_equal(m,p))
  7: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  8: less_or_equal(a(p),a(q)), [~(less_or_equal(q,j))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))

Gamma_25: (extend-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: [less_or_equal(m,p)]
  3: [~(less_or_equal(a(p),a(q)))]
  4: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(p,q)), ~(less_or_equal(m,p)), [~(
less(j,q))]
  6: ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(less_or_equal(m,p))]
  7: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  8: less_or_equal(a(p),a(q)), [~(less_or_equal(q,j))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))

Gamma_26: (move)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(less_or_equal(m,p))]
  3: [less_or_equal(m,p)]
  4: [~(less_or_equal(a(p),a(q)))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(p,q)), ~(less_or_equal(m,p)), [~(
less(j,q))]
  7: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]
  8: less_or_equal(a(p),a(q)), [~(less_or_equal(q,j))], ~(less_or_equal(p,q)), ~(
less_or_equal(m,p))

Gamma_27: (resolve)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(less_or_equal(m,p))]
  3: [~(less_or_equal(q,n))], ~(less_or_equal(p,q))
  4: [~(less_or_equal(a(p),a(q)))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]

Gamma_28: (extend-conflict)
  0: [less_or_equal(q,n)]
  1: [less_or_equal(p,q)]
  2: ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(less_or_equal(m,p))]
  3: ~(less_or_equal(q,n)), [~(less_or_equal(p,q))]
  4: [~(less_or_equal(a(p),a(q)))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]

Gamma_29: (move)
  0: [less_or_equal(q,n)]
  1: ~(less_or_equal(q,n)), [~(less_or_equal(p,q))]
  2: [less_or_equal(p,q)]
  3: ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(less_or_equal(m,p))]
  4: [~(less_or_equal(a(p),a(q)))]
  5: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less(p,i))]
  6: less_or_equal(a(p),a(q)), ~(less_or_equal(q,n)), ~(less_or_equal(p,q)), [~(
less_or_equal(i,p))]

Gamma_30: (resolve)
  0: [less_or_equal(q,n)]
  1: ~(less_or_equal(q,n)), [~(less_or_equal(p,q))]
  2: [~(less_or_equal(q,n))]
  3: [~(less_or_equal(a(p),a(q)))]

Gamma_31: (extend-conflict)
  0: [less_or_equal(q,n)]
  1: ~(less_or_equal(q,n)), [~(less_or_equal(p,q))]
  2: [~(less_or_equal(q,n))]
  3: [~(less_or_equal(a(p),a(q)))]

Gamma_32: (move)
  0: [~(less_or_equal(q,n))]
  1: [less_or_equal(q,n)]
  2: ~(less_or_equal(q,n)), [~(less_or_equal(p,q))]
  3: [~(less_or_equal(a(p),a(q)))]

Gamma_33: (resolve)
  0: [~(less_or_equal(q,n))]
  1: []
  2: [~(less_or_equal(a(p),a(q)))]

SZS status Unsatisfiable