#!/usr/bin/python


log_indent = 0

def log(*s):
  global log_indent
  print "c " + (" " * log_indent) + " ".join(map(str, s))
  log_indent += 2

def log_out():
  global log_indent
  log_indent -= 2



class Formula(object):
  def __init__(self):
    self.nvars = 2  # Variables 1 & 2 are used as placeholders. They are == 0.
    self.clauses = []

  def allocate(self, n = 1):
    curn = self.nvars
    self.nvars += n
    return curn

  def add_triplet(self, a, b, c, truth_table):
    assert a < self.nvars
    assert b < self.nvars
    assert c < self.nvars

    for av in xrange(2):
      for bv in xrange(2):
        for cv in xrange(2):
          if (av, bv, cv) not in truth_table:
            self.clauses.append((-(a+1) if av else a+1,
                                 -(b+1) if bv else b+1,
                                 -(c+1) if cv else c+1))

  def print_cnf(self):
    print "p cnf %d %d" % (self.nvars, len(self.clauses))

    for a, b, c in self.clauses:
      print a, b, c, 0

  def check(self, x):
    for a, b, c in self.clauses:
      v = False
      if a < 0:
        v = v or not x[-a - 1]
      else:
        v = v or x[a - 1]

      if b < 0:
        v = v or not x[-b - 1]
      else:
        v = v or x[b - 1]

      if c < 0:
        v = v or not x[-c - 1]
      else:
        v = v or x[c - 1]

      if not v:
        print "Wrong clause:", a, b, c


  def set_const1(self, a, v):
    log("x" + str(a), "=", v)
    self.add_triplet(a, 0, 1, [(v, 0, 0)])
    log_out()

  def set_const2(self, a, b, va, vb):
    log("x" + str(a), "x" + str(b), "=", va, vb)
    self.add_triplet(a, b, 0, [(va, vb, 0)])
    log_out()

  def set_const3(self, a, b, c, va, vb, vc):
    log("x" + str(a), "x" + str(b), "x" + str(c), "=", va, vb, vc)
    self.add_triplet(a, b, c, [(va, vb, vc)])
    log_out()

  def set_long_constant(self, a, n, v):
    log("x" + str(a) + "..x" + str(a + n - 1), "=", v)
    for i in xrange(0, n - 2, 3):
      b1 = v % 2
      v //= 2
      b2 = v % 2
      v //= 2
      b3 = v % 2
      v //= 2
      self.set_const3(a + i, a + i + 1, a + i + 2, b1, b2, b3)
    if n % 3 == 1:
      self.set_const1(a + n - 1, v)
    elif n % 3 == 2:
      self.set_const2(a + n - 2, a + n - 1, v % 2, v // 2)
    log_out()

  def new_long_constant(self, n, v):
    a = self.allocate(n)
    self.set_long_constant(a, n, v)
    return a

  def or2(self, a, b):
    log("x%d | x%d" % (a, b))
    self.add_triplet(a, b, 0, [(0, 1, 0), (1, 0, 0), (1, 1, 0)])
    log_out()

  def or3(self, a, b, c):
    log("x%d | x%d | x%d" % (a, b, c))
    self.add_triplet(a, b, c, [(0, 0, 1), (0, 1, 0), (0, 1, 1), (1, 0, 0), (1, 0, 1), (1, 1, 0), (1, 1, 1)])
    log_out()

  def eq_or(self, a, b, c):
    log("x%d = x%d | x%d" % (a, b, c))
    self.add_triplet(a, b, c, [(0, 0, 0), (1, 0, 1), (1, 1, 0), (1, 1, 1)])
    log_out()

  def new_or(self, a, b):
    x = self.allocate()
    self.eq_or(x, a, b)
    return x

  def or_mult(self, a, n):
    if n == 1:
      formula.set_const1(a, 1)
    elif n == 2:
      formula.or2(a, a + 1)
    elif n == 3:
      formula.or3(a, a + 1, a + 2)
    else:
      log(" | ".join("x%d" % i for i in range(a, a + n)))
      c = self.new_or(a, a + 1)
      for i in xrange(a + 2, a + n - 2):
        c = self.new_or(c, i)
      self.or3(c, a + n - 2, a + n - 1)
      log_out()

  def eq_and(self, a, b, c):
    log("x%d = x%d & x%d" % (a, b, c))
    self.add_triplet(a, b, c, [(0, 0, 0), (0, 0, 1), (0, 1, 0), (1, 1, 1)])
    log_out()

  def new_and(self, a, b):
    x = self.allocate()
    self.eq_and(x, a, b)
    return x

  def eq_xor(self, a, b, c):
    log("x%d = x%d xor x%d" % (a, b, c))
    self.add_triplet(a, b, c, [(0, 0, 0), (1, 0, 1), (1, 1, 0), (0, 1, 1)])
    log_out()

  def new_xor(self, a, b):
    x = self.allocate()
    self.eq_xor(x, a, b)
    return x

  def eq(self, a, b):
    log("x%d = x%d" % (a, b))
    self.add_triplet(a, b, 0, [(0, 0, 0), (1, 1, 0)])
    log_out()


def greater_than_1(formula, a, n):
  assert n > 1
  log("x%d..x%d > 1" % (a, a + n - 1))
  formula.or_mult(a + 1, n - 1)
  log_out()


def multiply1(formula, res, a, n, bit):
  log("x%d..x%d = x%d..x%d * x%d" % (res, res + n - 1, a, a + n - 1, bit))
  for i in range(n):
    formula.eq_and(res + i, a + i, bit)
  log_out()


def new_multiply1(formula, a, n, bit):
  res = formula.allocate(n)
  multiply1(formula, res, a, n, bit)
  return res


def add(formula, res, a, b, n):
  log("x%d..x%d = x%d..x%d + x%d..x%d" % (res, res + n, a, a + n - 1, b, b + n - 1))

  formula.eq_xor(res, a, b)
  c = formula.new_and(a, b)

  for i in range(1, n):
    # res[i] = c xor a[i] xor b[i]

    d = formula.new_xor(a + i, b + i)
    formula.eq_xor(res + i, c, d)

    # c = c & (a[i] xor b[i]) || a[i] & b[i]

    e = formula.new_and(a + i, b + i)
    f = formula.new_and(c, d)
    c = formula.new_or(e, f)

  formula.eq(res + n, c)

  log_out()


def new_add(formula, a, b, n):
  res = formula.allocate(n + 1)
  add(formula, res, a, b, n)
  return res


def multiply(formula, res, y, z, n):
  log("x%d..x%d = x%d..x%d * x%d..x%d" % (res, res + 2*n - 1, y, y + n - 1, z, z + n - 1))

  psum = formula.allocate(n + 1)
  formula.set_const1(psum + n, 0)

  multiply1(formula, psum, y, n, z)

  formula.eq(res, psum)

  for i in range(1, n):
    # psum = y * z[i] + (psum >> 1)
    d = new_multiply1(formula, y, n, z + i)
    psum = new_add(formula, d, psum + 1, n)

    formula.eq(res + i, psum)

  for i in range(1, n + 1):
    formula.eq(res + n + i - 1, psum + i)

  log_out()


formula = Formula()

# bits
n = 7

# x = y * z
x = formula.new_long_constant(2*n, 239)
y = formula.allocate(n)
z = formula.allocate(n)

greater_than_1(formula, y, n)
greater_than_1(formula, z, n)

multiply(formula, x, y, z, n)

formula.print_cnf()

# For n = 2, x = 6:
#
#formula.check([False, False,
#               False, True, True, False,  # x = 6
#               False, True,               # y = 2
#               True, True,                # z = 3
#               False, True, False,        # x10..x12 = y = 2
#               False, True,               # x13..x14 = y = 2
#               True, True, False,         # x15..x17 = x13..x14 + x11..x12
#               False, True,               # x18 - x19
#               False, False, False])