#include <iostream>
#include <vector>

using namespace std;

typedef vector<vector<int>> form;

bool contains(vector<int> & v, int n)
{ for (int i = 0; i < v.size(); i += 1)
    if (v[i] == n || v[i] == - n)
      return true;
  return false; }

void make(form & f, int vs, int ts)
{ f.clear();
  for (int i = 0; i < ts; i += 1)
  { vector<int> t;
    while (t.size() < 3)
    { int v = random() % vs + 1;
      if (contains(t, v))
        continue;
      if (random() % 2 == 0)
        t.push_back(v);
      else
        t.push_back(- v); }
    f.push_back(t); } }

void print(form & f, vector<bool> & knowns)
{ bool first = true;
  int numkn = knowns.size();
  for (int i = 0; i < f.size(); i += 1)
  { vector<int> & t = f[i];
    bool elim = false;
    for (int j = 0; j < t.size(); j += 1)
    { int v = t[j];
      int pos = v >= 0 ? v : - v;
      if (pos < numkn)
        if (v < 0 && knowns[- v] == false ||
            v >= 0 && knowns[v] == true)
        { elim = true;
          break; } } 
    if (elim)
      continue;
    if (first)
    { first = false;
      cout << "     ("; }
    else
      cout << "  && (";
    bool fint = true;
    for (int j = 0; j < t.size(); j += 1)
    { int v = t[j];
      int pos = v >= 0 ? v : - v;
      if (pos < numkn)
        if (v < 0 && knowns[- v] == true ||
            v >= 0 && knowns[v] == false)
          continue;
      if (fint)
        fint = false;
      else
        cout << " || ";
      if (t[j] < 0)
        cout << "! " << (char)('@' - t[j]);
      else
        cout << (char)('@' + t[j]); }
    cout << ")\n"; } }

bool eval(form & f, vector<bool> & vs)
{ for (int i = 0; i < f.size(); i += 1)
  { vector<int> & t = f[i];
    bool yes = false;
    for (int j = 0; j < t.size(); j += 1)
    { int v = t[j];
      if (v < 0)
      { if (! vs[- v])
        { yes = true;
          break; } }
      else if (vs[v])
      { yes = true;
        break; } }
    if (! yes)
      return false; }
  return true; }

void print(vector<bool> & v, string pre = "", string post = "")
{ cout << pre;
  for (int i = 1; i < v.size(); i += 1)
    if (v[i])
      cout << " T";
    else
      cout << " F";
    cout << post; }

bool solve(form & f, int vs, vector<bool> & knowns)
{ bool answer = false;
  int numkn = knowns.size();
  vector<bool> var;
  var.push_back(true);
  for (int i = 1; i < numkn; i += 1)
    var.push_back(knowns[i]);
  for (int i = numkn; i <= vs; i += 1)
    var.push_back(true);
  while (true)
  { bool result = eval(f, var);
    if (result)
    { answer = true;
      print(var, "    ", "\n"); }
    bool cont = false;
    for (int i = vs; i >= numkn && i > 0; i -= 1)
    { var[i] = ! var[i];
      if (! var[i])
      { cont = true;
        break; } }
    if (! cont)
      break; }
  return answer; }

int main(int argc, char * argv[])
{ int sd, vars = atol(argv[1]), terms = atol(argv[2]);
  if (argc >= 4)
    sd = atol(argv[3]);
  else
    sd = time(NULL);
  srandom(sd);
  cout << "seed is " << sd << "\n";
  form f;
  make(f, vars, terms);
  vector<bool> knowns;
  print(f, knowns);
  knowns.push_back(true);
  cout << "\nCan it be solved?\n";
  bool ok = solve(f, vars, knowns);
  if (! ok)
  { cout << "No, it can't be solved\n";
    exit(0); }
  cout << "Yes, it can be solved\n";
  for (int v = 1; v <= vars; v += 1)
  { cout << "\nCan it be solved with " << (char)('@' + v) << " set to true?\n";
    knowns.push_back(true);
    ok = solve(f, vars, knowns);
    if (ok)
      cout << "Yes it can, so set " << (char)('@' + v) << " to true\n";
    else
    { cout << "No it can't, so set " << (char)('@' + v) << " to false\n";
      knowns.back() = false; }
    print(f, knowns); } }