#!/usr/bin/env python
import sys, getopt


"""
Copyright (C) 2014 by Boris Konev & Liverpool University     
"""

def usage():
    print "usage: STD [-i filename] [-n number]"
    print "       specifying a number as input sets in the translation"
    print "       values of X1,..Xn to 1..n"

def main(argv):
    vars = 0
    NameToInt = dict()
    clauses = []

    try:
        opts, args = getopt.getopt(argv, "hi:n:", ["help", "input="])
    except getopt.GetoptError as err:
        print str(err)
        usage()
        sys.exit(2)
    fin = sys.stdin
    for o, a in opts:
        if o in ("-i", "--input"):
            fin = open(a, 'r') 
        if o=="-n":
            for i in range (1,int(a)+1):
                vars += 1
                id = "X"+str(i)
                NameToInt[id] = vars
                print "c ", id, "->", NameToInt[id]
        if o in ("-h", "--help"):
            usage()
            sys.exit(0)
    for line in fin.readlines():
        if (line[0:2] == "~ "):
            print "c ", line[1:],
            continue
        if (line.strip() == ""):
            continue
    
        clause = ""
        for id in line.strip().split():
            #print id
            sign = ""
            if (id[0] == '~'):
                id = id [1:]
                sign = "-"
                #print id
            if not (id in NameToInt):
                #print id,"->",NameToInt[id]
                vars += 1
                NameToInt[id] = vars
                print "c ", id,"->",NameToInt[id]
            clause += " " + sign + str(NameToInt[id])
        #print clause
        clauses.append(clause)
    
    print  "p cnf", vars, len(clauses)
    for clause in clauses:
        print clause, 0

if __name__ == "__main__":
    main(sys.argv[1:])