该题是在给定一系列的计算逻辑的基础上，询问一个表达式是否恒为真的问题，由于构成的表达式是一个以运算符开始的先序遍历的式子，所以可以利用递归进行求解。

什么是构造法呢？  

　　1．对所讨论的对象能进行较为直观的描述；

　　2．实现的具体性，就是不只是判明某种解的存在性，而且要实现具体求解。

代码如下：

#include 
     
      #include 
      
       #include 
       
        using namespace std;char s[105];int K[2][2] = {
   0, 0, 0, 1}, A[2][2] = {
   0, 1, 1, 1};int N[2] = {
   1, 0}, C[2][2] = {
   1, 1, 0, 1}, E[2][2] = {
   1, 0, 0, 1};int pos;bool calc(int &x) // 引用只是为了是为了避免数据的复制 {    ++pos;    switch (s[pos]) {        // 这个括号中的运算有一个先后顺序，所以出现G++（从左至右）能多，但是C++（从右至左）不能过         case 'K': return K[calc(x)][calc(x)];        case 'A': return A[calc(x)][calc(x)];        case 'N': return N[calc(x)];        case 'C': return C[calc(x)][calc(x)];        case 'E': return E[calc(x)][calc(x)];        case 'p': return x & 1;  // 分别取到压缩后的字节中的状态即可         case 'q': return x & (1 << 1);        case 'r': return x & (1 << 2);        case 's': return x & (1 << 3);        case 't': return x & (1 << 4);    }}int main(){    bool yes;    while (scanf("%s", s), s[0] != '0') {        yes = true;        // 这里的一个for循环顶五个for循环        for(int i = 0; i < 32 && yes; ++i) {            pos = -1;            if (!calc(i)) {                yes = false;            }        }        printf(yes ? "tautology\n" : "not\n");    }    return 0;    }