import java.io.*;
import java.util.ArrayList;
import java.util.Scanner;



public class Gerador {

    public static void main(String[] args) throws IOException {
        Scanner scanner= new Scanner(System.in);
        FileWriter saida = new FileWriter("Expressoes.txt");
        int numTab=0;
        try {
            scanner = new Scanner(new FileReader("EntradaTabela.in")).useDelimiter("\\n");
        } catch (FileNotFoundException e) {
            e.printStackTrace();
        }
        String numTest = scanner.nextLine();
        while(scanner.hasNext()){
            numTab++;
            numTest="Tabela #"+numTab;
            saida.write(numTest);
            saida.append(System.getProperty("line.separator"));
            Expre test = new Expre(scanner.nextLine());
            test.Final(saida);
        }
        scanner.close();
        saida.close();
    }
    static class Expre {
        private String expre;//expressão principal
        private boolean xe,ye,ze,te,satisfativel,refutavel;// armazena se as variáveis estão na expressão
        private int numVar,xv,yv,zv,tv;//numero de variáveis utilizadas
        private ArrayList <String> Subexps = new ArrayList<>();//armazena as subexpressões
        private ArrayList <Integer> Valores = new ArrayList<>();//armazena as valorções-verdade

        public Expre(String nome){
            this.expre=nome;
        }
        public int getNumVar(){//determina quantas variáveis estão sendo usadas
            Nvariaveis();
            numVar=0;
            if(xe==true){
                numVar++;
            }
            if(ye==true){
                numVar++;
            }
            if(ze==true){
                numVar++;
            }
            if(te==true){
                numVar++;
            }
            return  numVar;
        }
        private void Nvariaveis(){
            for (int i = 0; i < expre.length(); i++){//checa se cada uma das variáveis está na expressão
                if (expre.charAt(i) == 'x') {
                    xe=true;
                }
                if (expre.charAt(i) == 'y') {
                    ye=true;
                }
                if (expre.charAt(i) == 'z') {
                    ze=true;
                }
                if (expre.charAt(i) == 't') {
                    te=true;
                }
            }
        }
        private void gerSub(String ex){//encontra as sub-expressões de 'primeira ordem'
            int ini=0,fim=0,cont=0;
            for(int i=0;i < ex.length();i++){
                if (ex.charAt(i) == '(') {
                    if(cont==0){
                        ini=i;
                    }
                    cont++;
                }
                if (ex.charAt(i) == ')') {
                    cont--;
                    if(cont==0){
                        fim=i;
                        String sub= ex.substring(ini, fim+1);
                        Subexps.add(sub);
                    }
                }
            }
        }
        protected void gerAllSub(){//gera todas as sub-expressões, das maiores para as menore
            gerSub(expre);
            getNumVar();
            for(int i=0; i< Subexps.size();i++){
                String t=Subexps.get(i);
                if(t.length()>3){
                    t=t.substring(1,t.length());
                    gerSub(t);
                }
            }
            for(int i=0; i< Subexps.size();i++){

                for(int j=0; j< Subexps.size();j++){
                    if (Subexps.get(i).equals(Subexps.get(j)) && i!=j){
                        Subexps.remove(j);
                        j--;
                    }
                }
            }
            if(xe){
                Subexps.add("x");
            }
            if(ye){
                Subexps.add("y");
            }
            if(ze){
                Subexps.add("z");
            }
            if(te){
                Subexps.add("t");
            }
            sort();
        }
        public void printAllSub(FileWriter saida) throws IOException {//
            gerAllSub();
            for(int i=0;i<Subexps.size();i++){
                saida.write("-");
                for(int j=0;j<Subexps.get(i).length();j++){
                    saida.write("-");
                }
            }
            saida.write("-");
            saida.append(System.getProperty("line.separator"));
            for(int i=0;i<Subexps.size();i++){
                saida.write("|");
                saida.write(Subexps.get(i));
            }
            saida.write("|");
            saida.append(System.getProperty("line.separator"));
            for(int i=0;i<Subexps.size();i++){
                saida.write("-");
                for(int j=0;j<Subexps.get(i).length();j++){
                    saida.write("-");
                }
            }
            saida.write("-");
            saida.append(System.getProperty("line.separator"));
        }
        protected void inverteArrList(){
            ArrayList <String> te=new ArrayList();
            for(int i=Subexps.size()-1;i>=0;i--){
                te.add(Subexps.get(i));
            }
            Subexps.clear();
            Subexps=te;
        }
        public void printSatERef(FileWriter saida) throws IOException {
            if(satisfativel){
                saida.write("satisfativel");
            }
            else {
                saida.write("insatisfativel");
            }
            saida.write(" e ");
            if(refutavel){
                saida.write("refutavel");
                saida.append(System.getProperty("line.separator"));
            }
            else{
                saida.write("tautologia");
                saida.append(System.getProperty("line.separator"));
            }
            saida.write("");
            saida.append(System.getProperty("line.separator"));
        }
        protected int calculaValor(String exp){
            int cont=0,ini=0,fim=0;
            String sub1=null,sub2=null;
            if(exp.length()==1){
                if(exp.equals("x")){
                    return xv;
                }
                if(exp.equals("y")){
                    return yv;
                }
                if(exp.equals("z")){
                    return zv;
                }
                if(exp.equals("t")){
                    return tv;
                }
            }
            if(exp.charAt(1)=='-'){
                return not(calculaValor(exp.substring(2, exp.length()-1)));
            }
            if(exp.length()==5){
                String s=""+exp.charAt(1),r=""+exp.charAt(3);
                if(exp.charAt(2)=='.'){
                    return and(calculaValor(s),calculaValor(r));
                }
                if(exp.charAt(2)=='+'){
                    return or(calculaValor(s),calculaValor(r));
                }
                if(exp.charAt(2)=='>'){
                    return implica(calculaValor(s),calculaValor(r));
                }
            }
            if (exp.charAt(1) != '(') {
                String s=""+exp.charAt(1),r=exp.substring(3,exp.length()-1);
                if(exp.charAt(2)=='.'){
                    return and(calculaValor(s),calculaValor(r));
                }
                if(exp.charAt(2)=='+'){
                    return or(calculaValor(s),calculaValor(r));
                }
                if(exp.charAt(2)=='>'){
                    return implica(calculaValor(s),calculaValor(r));
                }
            }
            for(int i=1;i < exp.length()-1;i++){
                if (exp.charAt(i) == '(') {
                    if(cont==0){
                        ini=i;
                    }
                    cont++;
                }
                if (exp.charAt(i) == ')') {
                    cont--;
                    if(cont==0){
                        fim=i;
                        sub1= exp.substring(ini, fim+1);
                        break;
                    }
                }

            }
            char operador=exp.charAt(fim+1);
            int operadorIdx=fim+1;
            boolean sub22=false;
            for(int i=fim+2;i<exp.length();i++){
                if (exp.charAt(i) == '(') {
                    if(cont==0){
                        ini=i;
                        sub22=true;
                    }
                    cont++;
                }
                if (exp.charAt(i) == ')' && cont>0) {
                    cont--;
                    if(cont==0){
                        fim=i;
                        sub2= exp.substring(ini,fim+1);
                        break;
                    }
                }
            }
            if(!sub22){
                operadorIdx=exp.length()-3;
                operador=exp.charAt(operadorIdx);
                sub2=""+exp.charAt(exp.length()-2);
            }
            if (operador == '.') {
                return and(calculaValor(sub1),calculaValor(sub2));
            }
            if (operador == '+') {
                return or(calculaValor(sub1),calculaValor(sub2));
            }
            return implica(calculaValor(sub1),calculaValor(sub2));
        }

        protected int not(int x){
            if(x==1){
                return 0;
            }
            return 1;
        }
        protected int and(int x,int y){
            if(x==1 && y==1){
                return 1;
            }
            return 0;
        }
        protected int or(int x,int y){
            if(x==1 || y==1){
                return 1;
            }
            return 0;
        }
        protected int implica(int x,int y){
            if(x==1 && y==0){
                return 0;
            }
            return 1;
        }
        protected void calcula1valor(int x,int y,int z,int t){
            Valores.clear();
            int i=getNumVar();
            xv=x;
            yv=y;
            zv=z;
            tv=t;
            for(i=0;i<Subexps.size();i++){
                Valores.add(calculaValor(Subexps.get(i)));
            }
            if(Valores.get(Valores.size()-1)==1){
                satisfativel=true;
            }
            else {
                refutavel=true;
            }
        }
        protected void printvalor(FileWriter saida) throws IOException {
            int v=getNumVar();
            int xa[]={0,0,0,0,0,0,0,0,1,1,1,1,1,1,1,1};
            int ya[]={0,0,0,0,1,1,1,1,0,0,0,0,1,1,1,1};
            int za[]={0,0,1,1,0,0,1,1,0,0,1,1,0,0,1,1};
            int ta[]={0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1};
            for(int m=0;m<16;m++){
                if(!xe && xa[m]==1){
                    continue;
                }
                if(!ye && ya[m]==1){
                    continue;
                }
                if(!ze && za[m]==1){
                    continue;
                }
                if(!te && ta[m]==1){
                    continue;
                }
                calcula1valor(xa[m],ya[m],za[m],ta[m]);
                for(int i=0;i<Subexps.size();i++){
                    saida.write("|");
                    for(int j=1;j<Subexps.get(i).length();j++){
                        saida.write(" ");
                    }
                    saida.write(Valores.get(i).toString());
                }
                saida.write("|");
                saida.append(System.getProperty("line.separator"));
                for(int i=0;i<Subexps.size();i++){
                    saida.write("-");
                    for(int j=0;j<Subexps.get(i).length();j++){
                        saida.write("-");
                    }
                }
                saida.write("-");
                saida.append(System.getProperty("line.separator"));
            }
        }
        protected void sort(){
        ArrayList<String> aux=new ArrayList<>();
        while(!(Subexps.isEmpty())){
            String s=Subexps.get(0);
            int m=0;
            for(int j=1;j<Subexps.size();j++){
                if(s.length()==1){
                    continue;
                }
                String c=Subexps.get(j);
                if(s.length()==c.length()){
                    if(lexOrd(s,c)){
                        s=c;
                        m=j;
                        continue;
                    }
                    else{
                        continue;
                    }
                }
                if(s.length()>c.length()){
                    s=c;
                    m=j;
                }
            }
            aux.add(s);
            Subexps.remove(m);
        }
        Subexps=aux;
    }
    private boolean lexOrd(String s,String r){
            for(int i=0;i<s.length();i++){
                if(s.charAt(i)==r.charAt(i)){
                    continue;
                }
                else if(s.charAt(i)>r.charAt(i)){
                    return true;
                }
                else {
                    return false;
                }
            }
            return false;
    }
        public void Final(FileWriter saida) throws IOException {
            printAllSub(saida);
            printvalor(saida);
            printSatERef(saida);
        }
    }
}