#include <cctype>
#include <iostream>
#include <map>
#include <memory>
#include <set>
#include <string>
#include <vector>

using namespace std;

struct FormulaNode;
typedef shared_ptr<const FormulaNode> Formula;

enum FormulaType
{
FALSE,
TRUE,
LETTER,
NEGATION,
CONJUNCTION,
DISJUNCTION,
IMPLICATION,
EQUIVALENCE
};

Formula constant(bool value);
Formula letter(const string &name);
Formula negation(const Formula &formula);
Formula conjunction(const vector<Formula> &args);
Formula disjunction(const vector<Formula> &args);
Formula implication(const vector<Formula> &args);
Formula implication(const Formula &first, const Formula &second);
Formula equivalence(const vector<Formula> &args);

struct FormulaNode
{
const FormulaType type;
const vector<Formula> args;
const string name;

FormulaNode(FormulaType type, const vector<Formula> &args, const string &name) :
   type(type),
   args(args),
   name(name)
{
}

virtual ~FormulaNode()
{
}
};

int cmp(const Formula &first, const Formula &second)
{
if (first->type!=second->type) {
   return first->type < second->type ? -1 : 1;
}

if (first->args.size()!=second->args.size()) {
   return first->args.size()<second->args.size() ? -1 : 1;
}

if (first->type==LETTER) {
   if (first->name==second->name) {
         return 0;
   }

   return first->name<second->name ? -1 : 1;
}

for (size_t i = 0; i<first->args.size(); ++i) {
   int result = cmp(first->args[i], second->args[i]);

   if (result!=0) {
         return result;
   }
}

return 0;
}

struct Less
{
bool operator ()(const Formula &first, const Formula &second) const
{
   return cmp(first, second)<0;
}
};

struct ConstantNode : FormulaNode
{
ConstantNode(bool value) :
   FormulaNode(value ? TRUE : FALSE, vector<Formula>(), "")
{
}
};

Formula constant(bool value)
{
return Formula(new ConstantNode(value));
}

Formula letter(const string &name)
{
return Formula(new FormulaNode(LETTER, vector<Formula>(), name));
}

Formula negation(const Formula &formula)
{
vector<Formula> args;

args.push_back(formula);

return Formula(new FormulaNode(NEGATION, args, ""));
}

1). Show that if n is any integer, then n³ ≠2 (mod 4). Hint: use a...