#include <iostream>
#include <sstream>
#include <string>
#include <regex>
#include <fstream>

std::string text = R"#((a\/b\/c\/d\/f\/g\/h\/i)(a\/b\/c\/d\/f\/g\/h\/¬i)(a\/b\/c\/d\/f\/g\/¬h\/i)(a\/b\/c\/d\/f\/¬g\/h\/i)(a\/b\/c\/d\/¬f\/g\/h\/i)(a\/b\/c\/d\/¬f\/¬g\/¬h\/¬i)(a\/b\/c\/¬d\/f\/g\/h\/i)(a\/b\/c\/¬d\/f\/¬g\/¬h\/¬i)(a\/b\/c\/¬d\/¬f\/g\/¬h\/¬i)(a\/b\/c\/¬d\/¬f\/¬g\/h\/¬i)(a\/b\/c\/¬d\/¬f\/¬g\/¬h\/i)(a\/b\/c\/¬d\/¬f\/¬g\/¬h\/¬i)(a\/b\/¬c\/d\/f\/g\/h\/i)(a\/b\/¬c\/d\/f\/¬g\/¬h\/¬i)(a\/b\/¬c\/d\/¬f\/g\/¬h\/¬i)(a\/b\/¬c\/d\/¬f\/¬g\/h\/¬i)(a\/b\/¬c\/d\/¬f\/¬g\/¬h\/i)(a\/b\/¬c\/d\/¬f\/¬g\/¬h\/¬i)(a\/b\/¬c\/¬d\/f\/g\/¬h\/¬i)(a\/b\/¬c\/¬d\/f\/¬g\/h\/¬i)(a\/b\/¬c\/¬d\/f\/¬g\/¬h\/i)(a\/b\/¬c\/¬d\/f\/¬g\/¬h\/¬i)(a\/b\/¬c\/¬d\/¬f\/g\/h\/¬i)(a\/b\/¬c\/¬d\/¬f\/g\/¬h\/i)(a\/b\/¬c\/¬d\/¬f\/g\/¬h\/¬i)(a\/b\/¬c\/¬d\/¬f\/¬g\/h\/i)(a\/b\/¬c\/¬d\/¬f\/¬g\/h\/¬i)(a\/b\/¬c\/¬d\/¬f\/¬g\/¬h\/i)(a\/b\/¬c\/¬d\/¬f\/¬g\/¬h\/¬i)(a\/¬b\/c\/d\/f\/g\/h\/i)(a\/¬b\/c\/d\/f\/¬g\/¬h\/¬i)(a\/¬b\/c\/d\/¬f\/g\/¬h\/¬i)(a\/¬b\/c\/d\/¬f\/¬g\/h\/¬i)(a\/¬b\/c\/d\/¬f\/¬g\/¬h\/i)(a\/¬b\/c\/d\/¬f\/¬g\/¬h\/¬i)(a\/¬b\/c\/¬d\/f\/g\/¬h\/¬i)(a\/¬b\/c\/¬d\/f\/¬g\/h\/¬i)(a\/¬b\/c\/¬d\/f\/¬g\/¬h\/i)(a\/¬b\/c\/¬d\/f\/¬g\/¬h\/¬i)(a\/¬b\/c\/¬d\/¬f\/g\/h\/¬i)(a\/¬b\/c\/¬d\/¬f\/g\/¬h\/i)(a\/¬b\/c\/¬d\/¬f\/g\/¬h\/¬i)(a\/¬b\/c\/¬d\/¬f\/¬g\/h\/i)(a\/¬b\/c\/¬d\/¬f\/¬g\/h\/¬i)(a\/¬b\/c\/¬d\/¬f\/¬g\/¬h\/i)(a\/¬b\/c\/¬d\/¬f\/¬g\/¬h\/¬i)(a\/¬b\/¬c\/d\/f\/g\/¬h\/¬i)(a\/¬b\/¬c\/d\/f\/¬g\/h\/¬i)(a\/¬b\/¬c\/d\/f\/¬g\/¬h\/i)(a\/¬b\/¬c\/d\/f\/¬g\/¬h\/¬i)(a\/¬b\/¬c\/d\/¬f\/g\/h\/¬i)(a\/¬b\/¬c\/d\/¬f\/g\/¬h\/i)(a\/¬b\/¬c\/d\/¬f\/g\/¬h\/¬i)(a\/¬b\/¬c\/d\/¬f\/¬g\/h\/i)(a\/¬b\/¬c\/d\/¬f\/¬g\/h\/¬i)(a\/¬b\/¬c\/d\/¬f\/¬g\/¬h\/i)(a\/¬b\/¬c\/d\/¬f\/¬g\/¬h\/¬i)(a\/¬b\/¬c\/¬d\/f\/g\/h\/¬i)(a\/¬b\/¬c\/¬d\/f\/g\/¬h\/i)(a\/¬b\/¬c\/¬d\/f\/g\/¬h\/¬i)(a\/¬b\/¬c\/¬d\/f\/¬g\/h\/i)(a\/¬b\/¬c\/¬d\/f\/¬g\/h\/¬i)(a\/¬b\/¬c\/¬d\/f\/¬g\/¬h\/i)(a\/¬b\/¬c\/¬d\/f\/¬g\/¬h\/¬i)(a\/¬b\/¬c\/¬d\/¬f\/g\/h\/i)(a\/¬b\/¬c\/¬d\/¬f\/g\/h\/¬i)(a\/¬b\/¬c\/¬d\/¬f\/g\/¬h\/i)(a\/¬b\/¬c\/¬d\/¬f\/g\/¬h\/¬i)(a\/¬b\/¬c\/¬d\/¬f\/¬g\/h\/i)(a\/¬b\/¬c\/¬d\/¬f\/¬g\/h\/¬i)(a\/¬b\/¬c\/¬d\/¬f\/¬g\/¬h\/i)(a\/¬b\/¬c\/¬d\/¬f\/¬g\/¬h\/¬i)(¬a\/b\/c\/d\/f\/g\/h\/i)(¬a\/b\/c\/d\/f\/¬g\/¬h\/¬i)(¬a\/b\/c\/d\/¬f\/g\/¬h\/¬i)(¬a\/b\/c\/d\/¬f\/¬g\/h\/¬i)(¬a\/b\/c\/d\/¬f\/¬g\/¬h\/i)(¬a\/b\/c\/d\/¬f\/¬g\/¬h\/¬i)(¬a\/b\/c\/¬d\/f\/g\/¬h\/¬i)(¬a\/b\/c\/¬d\/f\/¬g\/h\/¬i)(¬a\/b\/c\/¬d\/f\/¬g\/¬h\/i)(¬a\/b\/c\/¬d\/f\/¬g\/¬h\/¬i)(¬a\/b\/c\/¬d\/¬f\/g\/h\/¬i)(¬a\/b\/c\/¬d\/¬f\/g\/¬h\/i)(¬a\/b\/c\/¬d\/¬f\/g\/¬h\/¬i)(¬a\/b\/c\/¬d\/¬f\/¬g\/h\/i)(¬a\/b\/c\/¬d\/¬f\/¬g\/h\/¬i)(¬a\/b\/c\/¬d\/¬f\/¬g\/¬h\/i)(¬a\/b\/c\/¬d\/¬f\/¬g\/¬h\/¬i)(¬a\/b\/¬c\/d\/f\/g\/¬h\/¬i)(¬a\/b\/¬c\/d\/f\/¬g\/h\/¬i)(¬a\/b\/¬c\/d\/f\/¬g\/¬h\/i)(¬a\/b\/¬c\/d\/f\/¬g\/¬h\/¬i)(¬a\/b\/¬c\/d\/¬f\/g\/h\/¬i)(¬a\/b\/¬c\/d\/¬f\/g\/¬h\/i)(¬a\/b\/¬c\/d\/¬f\/g\/¬h\/¬i)(¬a\/b\/¬c\/d\/¬f\/¬g\/h\/i)(¬a\/b\/¬c\/d\/¬f\/¬g\/h\/¬i)(¬a\/b\/¬c\/d\/¬f\/¬g\/¬h\/i)(¬a\/b\/¬c\/d\/¬f\/¬g\/¬h\/¬i)(¬a\/b\/¬c\/¬d\/f\/g\/h\/¬i)(¬a\/b\/¬c\/¬d\/f\/g\/¬h\/i)(¬a\/b\/¬c\/¬d\/f\/g\/¬h\/¬i)(¬a\/b\/¬c\/¬d\/f\/¬g\/h\/i)(¬a\/b\/¬c\/¬d\/f\/¬g\/h\/¬i)(¬a\/b\/¬c\/¬d\/f\/¬g\/¬h\/i)(¬a\/b\/¬c\/¬d\/f\/¬g\/¬h\/¬i)(¬a\/b\/¬c\/¬d\/¬f\/g\/h\/i)(¬a\/b\/¬c\/¬d\/¬f\/g\/h\/¬i)(¬a\/b\/¬c\/¬d\/¬f\/g\/¬h\/i)(¬a\/b\/¬c\/¬d\/¬f\/g\/¬h\/¬i)(¬a\/b\/¬c\/¬d\/¬f\/¬g\/h\/i)(¬a\/b\/¬c\/¬d\/¬f\/¬g\/h\/¬i)(¬a\/b\/¬c\/¬d\/¬f\/¬g\/¬h\/i)(¬a\/b\/¬c\/¬d\/¬f\/¬g\/¬h\/¬i)(¬a\/¬b\/c\/d\/f\/g\/¬h\/¬i)(¬a\/¬b\/c\/d\/f\/¬g\/h\/¬i)(¬a\/¬b\/c\/d\/f\/¬g\/¬h\/i)(¬a\/¬b\/c\/d\/f\/¬g\/¬h\/¬i)(¬a\/¬b\/c\/d\/¬f\/g\/h\/¬i)(¬a\/¬b\/c\/d\/¬f\/g\/¬h\/i)(¬a\/¬b\/c\/d\/¬f\/g\/¬h\/¬i)(¬a\/¬b\/c\/d\/¬f\/¬g\/h\/i)(¬a\/¬b\/c\/d\/¬f\/¬g\/h\/¬i)(¬a\/¬b\/c\/d\/¬f\/¬g\/¬h\/i)(¬a\/¬b\/c\/d\/¬f\/¬g\/¬h\/¬i)(¬a\/¬b\/c\/¬d\/f\/g\/h\/¬i)(¬a\/¬b\/c\/¬d\/f\/g\/¬h\/i)(¬a\/¬b\/c\/¬d\/f\/g\/¬h\/¬i)(¬a\/¬b\/c\/¬d\/f\/¬g\/h\/i)(¬a\/¬b\/c\/¬d\/f\/¬g\/h\/¬i)(¬a\/¬b\/c\/¬d\/f\/¬g\/¬h\/i)(¬a\/¬b\/c\/¬d\/f\/¬g\/¬h\/¬i)(¬a\/¬b\/c\/¬d\/¬f\/g\/h\/i)(¬a\/¬b\/c\/¬d\/¬f\/g\/h\/¬i)(¬a\/¬b\/c\/¬d\/¬f\/g\/¬h\/i)(¬a\/¬b\/c\/¬d\/¬f\/g\/¬h\/¬i)(¬a\/¬b\/c\/¬d\/¬f\/¬g\/h\/i)(¬a\/¬b\/c\/¬d\/¬f\/¬g\/h\/¬i)(¬a\/¬b\/c\/¬d\/¬f\/¬g\/¬h\/i)(¬a\/¬b\/c\/¬d\/¬f\/¬g\/¬h\/¬i)(¬a\/¬b\/¬c\/d\/f\/g\/h\/¬i)(¬a\/¬b\/¬c\/d\/f\/g\/¬h\/i)(¬a\/¬b\/¬c\/d\/f\/g\/¬h\/¬i)(¬a\/¬b\/¬c\/d\/f\/¬g\/h\/i)(¬a\/¬b\/¬c\/d\/f\/¬g\/h\/¬i)(¬a\/¬b\/¬c\/d\/f\/¬g\/¬h\/i)(¬a\/¬b\/¬c\/d\/f\/¬g\/¬h\/¬i)(¬a\/¬b\/¬c\/d\/¬f\/g\/h\/i)(¬a\/¬b\/¬c\/d\/¬f\/g\/h\/¬i)(¬a\/¬b\/¬c\/d\/¬f\/g\/¬h\/i)(¬a\/¬b\/¬c\/d\/¬f\/g\/¬h\/¬i)(¬a\/¬b\/¬c\/d\/¬f\/¬g\/h\/i)(¬a\/¬b\/¬c\/d\/¬f\/¬g\/h\/¬i)(¬a\/¬b\/¬c\/d\/¬f\/¬g\/¬h\/i)(¬a\/¬b\/¬c\/d\/¬f\/¬g\/¬h\/¬i)(¬a\/¬b\/¬c\/¬d\/f\/g\/h\/i)(¬a\/¬b\/¬c\/¬d\/f\/g\/h\/¬i)(¬a\/¬b\/¬c\/¬d\/f\/g\/¬h\/i)(¬a\/¬b\/¬c\/¬d\/f\/g\/¬h\/¬i)(¬a\/¬b\/¬c\/¬d\/f\/¬g\/h\/i)(¬a\/¬b\/¬c\/¬d\/f\/¬g\/h\/¬i)(¬a\/¬b\/¬c\/¬d\/f\/¬g\/¬h\/i)(¬a\/¬b\/¬c\/¬d\/f\/¬g\/¬h\/¬i)(¬a\/¬b\/¬c\/¬d\/¬f\/g\/h\/i)(¬a\/¬b\/¬c\/¬d\/¬f\/g\/h\/¬i)(¬a\/¬b\/¬c\/¬d\/¬f\/g\/¬h\/i)(¬a\/¬b\/¬c\/¬d\/¬f\/g\/¬h\/¬i)(¬a\/¬b\/¬c\/¬d\/¬f\/¬g\/h\/i)(¬a\/¬b\/¬c\/¬d\/¬f\/¬g\/h\/¬i)(¬a\/¬b\/¬c\/¬d\/¬f\/¬g\/¬h\/i)(¬a\/¬b\/¬c\/¬d\/¬f\/¬g\/¬h\/¬i))#";

int main()
{
    std::ofstream out("output.txt");
    auto x = -1;

    std::regex regex("(¬?[a-z])");
    //auto count = 0;
    for (auto it = std::sregex_iterator(text.begin(), text.end(), regex); it != std::sregex_iterator(); ++it, x++) {
        out << "(¬x" + std::to_string(x) + "v" + it->str() + "vx" + std::to_string(x + 1) + ")&";
    //  if (++count % 8 == 0)
    //      out << "\n";
    }
}