import fr.jussieu.script.*;
import java.util.StringTokenizer;
import java.io.*;

class Affectation {

    private boolean [] var;

    Affectation () {
	var = new boolean[0];
    }

    Affectation ( int n ) { 
	var = new boolean[n+1];
	for ( int i = 0; i <= n; i++ ) var[i]=true;
    }

    public void set ( int i, boolean b ) {
	var[i] = b;
    }

    public boolean get ( int i ) {
	return var[i];
    }

    public int longueur() {
	return var.length;
    }

}


class Clause {
    
    private int [] var;
    /*************************************** 
       0 si absente
       1 si présente
       -1 si présente mais négative
       2 si présente posivite et négative
    ***************************************/

    Clause () {
	var = new int[0];
    }

    Clause ( int n ) {
	var = new int[n+1]; // la case 0 n'est pas prise en compte
	for ( int i = 0; i <= n; i++ ) var[i]=0;
    }


    public void set ( int i, int val ) {
	var[i] = val;
    }

    public int get ( int i ) {
	return var[i];
    }

    public int longueur () {
	return var.length;
    }

    public static boolean vide ( Clause c ) {
	for ( int i = 0; i < c.var.length; i++ )
	    if ( c.var[i] != 0 ) return false;
	return true;
    }

    public static boolean totologie ( Clause c ) {
	for ( int i = 0; i < c.var.length; i++ ) 
	    if ( c.var[i] == 2 ) return true;
	return false;
    }

    public static boolean unitaire ( Clause c ) {
	int compt = 0;
	for ( int i = 0; i < c.var.length; i++ ) {
	    if ( c.var[i] == 2 ) return false;
	    if ( c.var[i] == 1 || c.var[i] == -1 ) compt++;
	}
	if ( compt == 1 ) return true;
	return false;
    }

    public static boolean egalite ( Clause a, Clause b ) {
	if ( a.var.length != b.var.length ) return false;
	for ( int i = 0; i < a.var.length; i++ ) 
	    if ( a.var[i] != b.var[i] ) return false;
	return true;
    }

    public static Clause copie ( Clause c ) {
	Clause res = new Clause ( c.var.length );
	for ( int i = 0; i < c.var.length; i++ )
	    res.var[i] = c.var[i];
	return res;
    }

    public static boolean verif ( Clause c, Affectation v ) {
	if ( totologie(c) ) return true;
	for ( int i = 0; i < c.var.length; i++ ) {
	    if ( v.get(i) && c.var[i] == 1 ) return true;
	    if ( !v.get(i) && c.var[i] == -1 ) return true;
	}
	return false;
    }

}
 
class Formule {
    
    private Clause [] claus;
    
    Formule () {
	claus = new Clause[0];
    }
    
    Formule ( int n, int v ) {
	claus = new Clause[n+1]; // la case 0 n'est pas prise en compte
	for ( int i = 0; i <= n; i++ ) claus[i]= new Clause (v);
    }
    

    public void set ( int i, Clause c ) {
	claus[i] = c;
    }
    
    public Clause get ( int i ) {
	return claus[i];
    }

    public static Formule init ( String fichier ) {
	Formule F = new Formule();
	try {
	    FileReader fr = new FileReader ( fichier );
	    
	    BufferedReader br = new BufferedReader ( fr );
	    
	    try {
		String ligne = br.readLine(); //première ligne
		StringTokenizer st = new StringTokenizer ( ligne );
		String s = st.nextToken(); //premier mot ( c )
		while ( s == "c" ) {
		    ligne = br.readLine();
		    st = new StringTokenizer ( ligne );
		    s = st.nextToken();
		}
		
		/* Ligne commençant par p */
		ligne = br.readLine(); st = new StringTokenizer ( ligne ); 
		s = st.nextToken(); //premier mot ( p )
		s = st.nextToken(); // ( cnf )
		s = st.nextToken(); int x = Integer.parseInt(s); // x est le nombre de variables
		s = st.nextToken(); int y = Integer.parseInt(s); // y est le nombre de clauses
		F = new Formule(y,x);
		
		/* La formule */
		int n;
		for ( int i = 1; i <= y; i++ ) {
		    ligne = br.readLine(); st = new StringTokenizer ( ligne );
		    do {
			s = st.nextToken(); n = Integer.parseInt(s);
			if ( n > 0 ) {
			    if ( F.claus[i].get(n) == 0 ) F.claus[i].set(n,1);
			    else F.claus[i].set(n,2);
			}
			if ( n < 0 ) {
			    n = -n;
			    if ( F.claus[i].get(n) == 0 ) F.claus[i].set(n,-1);
			    else F.claus[i].set(n,2);
			}			
		    } while ( st.hasMoreTokens () );
		}
		return F;
	    }
	    catch ( IOException e ) { System.out.println("Fichier "+fichier+" incorrect"); }
	}
	catch ( FileNotFoundException e ) { System.out.println("Le fichier "+fichier+" n'existe pas"); }
	return F;
    }
     
    public void affiche () {
	int n;
	Deug.println("p cnf "+this.claus[0].longueur()+" "+this.claus.length);
	for ( int i = 1; i < this.claus.length; i++ ) {
	    for ( int j = 1; j < this.claus[i].longueur(); j++ ) {
		n = this.claus[i].get(j);
		if ( n == 1 ) Deug.print(j+" ");
		if ( n == -1 ) Deug.print("-"+j+" ");
		if ( n == 2 ) Deug.print(j+" -"+j+" ");
	    }
	    if ( i < this.claus.length-1 ) Deug.println("0");
	}
	Deug.println();
    }

    public static boolean vide ( Formule F ) {
	for ( int i = 0; i < F.claus.length; i++ )
	    if ( !Clause.vide(F.claus[i]) ) return false;
	return true;
    }

    public static boolean clausevide ( Formule F ) {
	if ( F.claus.length == 0 ) return true;
	for ( int i = 0; i < F.claus.length; i++ )
	    if ( Clause.vide(F.claus[i]) ) return true;
	return false;
    }
    
    public static int contienttotologie ( Formule F ) {
	for ( int i = 0; i < F.claus.length; i++ ) 
	    if ( Clause.totologie(F.claus[i]) ) return i;
	return -1;
    }

    public static boolean contientunitaire ( Formule F ) {
	for ( int i = 0; i < F.claus.length; i++ )
	    if ( Clause.unitaire(F.claus[i]) ) return true;
	return false;
    }
    
    public static boolean membre ( Formule F, Clause c ) {
	for ( int i = 0; i < F.claus.length; i++ )
	    if ( Clause.egalite(c, F.claus[i]) ) return true;
	return false;
    }

    public static Formule supprimeclausei ( Formule F, int j ) {
	Formule G = new Formule ( F.claus.length-1, F.claus[j].longueur() );
	for ( int i = 0; i < F.claus.length; i++ ) {
	    if ( i < j ) G.claus[i] = Clause.copie(F.claus[i]);
	    if ( i > j ) G.claus[i-1] = Clause.copie(F.claus[i]);
	}
	return G;
    }
	
    public static Formule supprimeclause ( Formule F, Clause c ) {
	Formule G = new Formule();
	for ( int i = 0; i < F.claus.length; i++ ) 
	    if ( Clause.egalite(F.claus[i],c) ) G = supprimeclause(supprimeclausei(F,i),c);
	return G;
    }

    public static boolean verif ( Formule F, Affectation v ) {
	for ( int i = 0; i < F.claus.length; i++ )
	    if ( !Clause.verif(F.claus[i],v) ) return false;
	return true;
    }

}


class dPutnam {

    public static void afficheDimacs ( String fichier ) {
	try {
	    FileReader fr = new FileReader ( fichier );
	    
	    BufferedReader br = new BufferedReader ( fr );
	    
	    try {
		String ligne = br.readLine(); //première ligne
 		StringTokenizer st = new StringTokenizer ( ligne );
		String s = st.nextToken(); //premier mot ( c )
		while ( s == "c" ) {
		    ligne = br.readLine();
		    st = new StringTokenizer ( ligne );
		    s = st.nextToken();
		}
		
		/* Ligne commençant par p */
		ligne = br.readLine(); st = new StringTokenizer ( ligne ); 
		s = st.nextToken(); //premier mot ( p )
		s = st.nextToken(); // ( cnf )
		s = st.nextToken(); Deug.println("Nombre de variables : "+s); int x = Integer.parseInt(s);
		s = st.nextToken(); Deug.println("Nombre de clauses : "+s); int y = Integer.parseInt(s);

		/* La formule */

		for ( int i = 0; i < y; i++ ) {
		ligne = br.readLine(); st = new StringTokenizer ( ligne );
		    /* Boolean pour savoir si on doit écrire \/ */
		    boolean test = false;
		    Deug.print("( ");
		    do {
			s = st.nextToken();
			if ( test && Integer.parseInt(s) != 0 ) { Deug.print(" \\/ "); }
			if ( Integer.parseInt(s) > 0 ) {
			    Deug.print("x"+s); test = true;
			}
			if ( Integer.parseInt(s) < 0 ) {
			    int a = -Integer.parseInt(s);
			    Deug.print("~x"+a); test = true;
			}			
		    } while ( st.hasMoreTokens () );
		    Deug.print(" )"); if ( i < y-1 ) Deug.print(" /\\ "); 
		}
		Deug.println();
	    }
	    catch ( IOException e ) { System.out.println("Fichier "+fichier+" incorrect"); }
	}
	catch ( FileNotFoundException e ) { System.out.println("Le fichier "+fichier+" n'existe pas"); }
    }
    
    public static void main (String[] args) {
	afficheDimacs("test.dim");
	Formule F = Formule.init("test.dim");
	F.affiche();
	//Deug.println(Formule.contientunitaire(F));
	Formule.supprimeclausei(F,2).affiche();
    }
}