import choco.Problem;
import choco.Constraint;
import choco.Solver;
import choco.Solution;
import choco.ContradictionException;
import choco.integer.IntVar;
//import choco.search.AssignVar;
import choco.search.AbstractGlobalSearchSolver;
import choco.search.AbstractGlobalSearchLimit;
import choco.integer.search.*;
import java.io.*;
import java.lang.*;
import java.util.*;

public class Necessity {	
   

    public static void main(String[] args) throws Exception,ContradictionException,FileNotFoundException,IOException {
	long ms1 = System.currentTimeMillis();
	Dict d = new Dict();
	MyIo fin = new MyIo(args[0]);
	int n = fin.getNextInt();
	Tree t[] = new Tree[n+1];
	for (int i=0;i<n;i++) t[i] = new Tree(fin.getNextString(),d);	
	fin.close();

	t[n] = new Tree(args[1],d);

	Problem pb = new Problem();
	int m = d.size();

	UMatrix um = new UMatrix(m-1,pb,d,false);	
	
	for (int i=0;i<=n;i++) t[i].breakUp(um);

	long ms2 = System.currentTimeMillis();

	for (int i=0;i<n;i++){
	    ArrayList S = um.getTriples(t[i]);
	    for (int j=0;j<S.size();j++){
		Triple T = (Triple)S.get(j);
		System.out.println(T);
		T.post();
	    }
	}
	
	boolean necessary = false;
	ArrayList S = um.getTriples(t[n]);
	for (int i=0;i<S.size();i++){
	    Triple T = (Triple)S.get(i);
	    if (T.isPosted()) necessary = true;
	    else T.retract();
	    System.out.println(T + " " + T.isPosted());	  
	}

	try {pb.propagate();}
	catch (Exception e) {necessary = true;}

	long ms3 = System.currentTimeMillis();

	System.out.println(necessary);

	System.out.println("model: " + (ms2-ms1) + "ms   " + "solve: " + (ms3-ms2) + "ms" );
    }
}