import java.util.Scanner;
import java.util.ArrayList;

public class Logic{
	static boolean isFNC(String exp) {
		for(int i = 0; i < exp.length(); i++){
			if(exp.charAt(i) == '~' && exp.charAt(i+1) == '(') return false;
			if(exp.charAt(i) == '&' && (exp.charAt(i-1) != ')' || exp.charAt(i+1) != '(')) return false;
			if(exp.charAt(i) == '>' || exp.charAt(i) == '<') return false;
		}
		return true;
	}
	static boolean isHorn(String exp){
		int contador = 0; int aux = 0;

		for(int i = 0; i < exp.length(); i++){
			if(exp.charAt(i) == '(') contador++;
			if(contador == 1 && exp.charAt(i) == 'v' && (exp.charAt(i+1) >= 'A' && exp.charAt(i+1) <= 'Z')) aux++;
			if(aux > 1) return false;
			if(exp.charAt(i) == ')') {
				contador = 0;
				aux = 0;
			}
		}
		return true;
	}
	boolean SAT(String exp) {
		ArrayList<String> clausulas = new ArrayList<String>();
		ArrayList<String> unity = new ArrayList<String>();

		int aux1 = 0, aux2 = 0;
		String auux = " ";

		for(int i = 0; i < exp.length(); i++) {
			if(exp.charAt(i-1) == '(') aux1 = i;
			if(exp.charAt(i+1) == ')') aux2 = i;

			auux = exp.substring(aux1, aux2);

			if(auux.length() > 2) clausulas.add(auux);
			else unity.add(auux);
		}

		for(int i = 0; i < unity.size(); i++) {
			//BUSCA ENTRE AS CLAUSULAS UNITARIAS
			boolean neg = false;
			if(unity.get(i).length() > 1) neg = true;

			for(int j = 0; j < unity.size(); j++) {
				if(j != i) {
					//Positio e negativo
					if(neg == false && unity.get(j).length() == 2 && (unity.get(j).charAt(1) == unity.get(i).charAt(0)))
						return false;

					//Negativo e negativo
					else if(neg == true && unity.get(j).length() == 2 && (unity.get(j).charAt(1) == unity.get(i).charAt(1)))
						unity.remove(j);

					//Positivo e positivo
					else if(neg == false && unity.get(j).length() == 1 && (unity.get(j).charAt(0) == unity.get(i).charAt(0)))
						unity.remove(j);
				}
			}
			//BUSCA ENTRE AS CLAUSULAS
			for(int k = 0; k < clausulas.size(); k++) {
				for(int l = 0; l < clausulas.get(k).length(); l++) {
					if(neg = false && (clausulas.get(k).charAt(l) == unity.get(i).charAt(0))) {
						if(clausulas.get(k).charAt(l-1) == '~') clausulas.remove(k);
					}
				}
			}
		}
	}
	public static void main(String args[]) {
		Scanner in = new Scanner(System.in);

		int qtd_exp = in.nextInt();
		in.nextLine();

		for(int i = 0; i < qtd_exp; i++){
			String exp = in.nextLine();
			String newExp = " ";

			for(int j = 0; j < exp.length(); j++)
				if(exp.charAt(j) != ' ') newExp += exp.charAt(j);
			exp = newExp;

			if(!isFNC(exp)) {
				System.out.printf("Problema #%d\n",i+1);
				System.out.println("Não está na FNC.\n");
			}
			else if(!isHorn(exp)) {
				System.out.printf("Problema #%d\n",i+1);
				System.out.println("Nem todas as cláusulas são de Horn.\n");
			}
			else {
				if(SAT(exp)) {

				}
				else {

				}
			}
		}
	}
}