学步园

WFF 'N PROOF is a logic game played with dice. Each die has six faces representing some subset of the possible symbols K, A, N, C, E, p, q, r, s, t. A Well-formed formula (WFF) is any string of these symbols obeying the following rules:

• p, q, r, s, and t are WFFs
• if w is a WFF, Nw is a WFF
• if w and x are WFFs, Kwx, Awx, Cwx, and Ewx are WFFs.

The meaning of a WFF is defined as follows:

• p, q, r, s, and t are logical variables that may take on the value 0 (false) or 1 (true).
• K, A, N, C, E mean and, or, not, implies, and equals as defined in the truth table below.

A tautology is a WFF that has value 1 (true) regardless of the values of its variables. For example, ApNp is a tautology because it is true regardless of the value of p. On the other hand, ApNq is not, because it has the
value 0 for p=0, q=1.

You must determine whether or not a WFF is a tautology.

Input consists of several test cases. Each test case is a single line containing a WFF with no more than 100 symbols. A line containing 0 follows the last case.

For each test case, output a line containing tautology or not as appropriate.

#include <stdio.h>
#include <string.h>
#include <algorithm>
#include <math.h>
#include <sstream>
#include <vector>
#include <stack>
#include <map>
#include <queue>
#include <set>
#include <iostream>
#include <stdlib.h>
#include <cctype>
#define rep(i,s,e) for(int i = (s);i<(e);++i)
#define maxn 200
#define INF 1000000000
using namespace std;
char in[210];
int len;
stack<int> S;
int solve(int p,int q,int r,int s,int t)
{
     for(int i = len-1;i>=0;--i)
        {
            if(in[i]=='p')
            {
              S.push(p);
            }
            if(in[i]=='q')
            {
               S.push(q);
            }
            if(in[i]=='r')
            {
               S.push(r);
            }
            if(in[i]=='s')
            {
               S.push(s);
            }
            if(in[i]=='t')
            {
               S.push(t);
            }
            if(in[i]=='A')
            {
              int a,b;
              if(!S.empty())
              {
                 a = S.top();
                 S.pop();
              }
              if(!S.empty())
              {
                 b = S.top();
                 S.pop();
              }
              S.push(a|b);
            }
            if(in[i]=='K')
            {
              int a,b;
              if(!S.empty())
              {
                 a = S.top();
                 S.pop();
              }
              if(!S.empty())
              {
                 b = S.top();
                 S.pop();
              }
              S.push(a&b);
            }
            if(in[i]=='E')
            {
              int a,b;
              if(!S.empty())
              {
                 a = S.top();
                 S.pop();
              }
              if(!S.empty())
              {
                 b = S.top();
                 S.pop();
              }
              if(a==b)
              S.push(1);
              else
              S.push(0);
            }
            if(in[i]=='N')
            {
              int a;
              if(!S.empty())
              {
                 a = S.top();
                 S.pop();
              }
              if(a==0)
              S.push(1);
              if(a==1)
              S.push(0);
            }
            if(in[i]=='C')
            {
              int a,b;
              if(!S.empty())
              {
                 a = S.top();
                 S.pop();
              }
              if(!S.empty())
              {
                 b = S.top();
                 S.pop();
              }
              if(a==1&&b==0)
              S.push(0);
              else
              S.push(1);
            }
        }
    if(!S.empty())
    {
        int a = S.top();
        S.pop();
        return a;
    }
}
int main()
{
    //freopen("in.txt","r",stdin);
    while(scanf("%s",in)==1)
    {
        if(in[0]=='0')
        break;

        len = strlen(in);

        int flag = 1;

        rep(i,0,2)
        rep(j,0,2)
        rep(k,0,2)
        rep(a,0,2)
        rep(b,0,2)
        {
          while(!S.empty())
          S.pop();
           if(solve(i,j,k,a,b)==0)
           {
            flag = 0;
            goto here;
           }
        }
        here:
        if(!flag)
        cout<<"not"<<endl;
        else
        cout<<"tautology"<<endl;

    }
    return 0;
}