// Checker to be used by evaluator.
//
// Usage: [checker] [input] [official_output] [contestant_output]
//
// Score (real between 0.0 and 1.0) written on stdout.
// Textual description of the result written on stderr.

#include <algorithm>
#include <cassert>
#include <cstdlib>
#include <cstring>
#include <fstream>
#include <iostream>
#include <sstream>
#include <string>
#include <vector>
#include <functional>
#include <map>

using namespace std;

namespace TwoSat {
  // klasa testirana u TwoSat_test.cpp
  
  vector<vector<int>> E;
  vector<int> bio, val;
  int n, cookie;
  
  bool __dfs(int x, int v) {
    if (bio[x] == cookie) return val[x] == v;
    val[x] = v;
    bio[x] = cookie;
    for (int y: E[x*2+v])
      if (!__dfs(y/2, y&1)) return false;
    return true;
  }
 
  bool __solve(vector<vector<bool>>& imps, vector<bool> fixed) {
    /* Args:
            imps - implication matrix (2N x 2N)
            fixed - used to fix values of some prefix of variables
       Returns:
            true if solutions exists, false otherwise
    */
    
    int N = imps.size() / 2;
    E = vector<vector<int>>(2*N);
    val = vector<int>(N, -1);
    bio = vector<int>(N, 0);
    cookie = 0;
    
    for (int i = 0; i < 2*N; ++i) {
      for (int j = 0; j < 2*N; ++j) {
        if (imps[i][j]) E[i].push_back(j);
      }
    }

    for (int i = 0; i < (int)fixed.size(); ++i) {
      int val = fixed[i];
      E[2*i+(val^1)].push_back(2*i+val);
    }
    
    for (int i = 0; i < N; ++i) {
      cookie++;
      if (!__dfs(i, 0)) {
        for (int j = 0; j < N; ++j)
          if (bio[j] == cookie) val[j] = -1;
        cookie++;
        if (!__dfs(i, 1)) return false;
      }
    }
    return true;
  }


  bool check_solution(vector<vector<bool>>& E, vector<bool> sol) {
    /* Args:
       E - 2sat implication matrix (2N x 2N)
       sol - bit vector of size K, where K <= N. Assignments of values to first K variables.
       Returns:
       true if assignments in sol are consistent with implication matrix E
    */

    return TwoSat::__solve(E, sol);
  }

  int count_solutions(vector<vector<bool>>& E) {
    // returns min(4, C) where C is number of solutions to 2sat problem given by implication matrix E
    
    int N = E.size() / 2;
    int ans = 0;
    vector<bool> fixed;
    function<void (int)> rec = [&](int i) {
      if (ans >= 4) return;
      if (!TwoSat::__solve(E, fixed)) return;
    
      if (i == N) {
        ans++;
        return;
      }

      for (int val = 0; val < 2; ++val) {
        fixed.push_back(val);
        rec(i + 1);
        fixed.pop_back();
      }
    };

    rec(0);
    
    return ans;
  }
}

/**
 * @param p fraction of points awarded to the contestant.
 * @pararm m error message displayed to the contestant.
 */
void finish(double p, const string& m);

/**
 * The main checking function.
 * @param fin official input
 * @param foff official output
 * @param fout contestant's output
 */
void checker(ifstream& fin, ifstream& foff, ifstream& fout)
{
  const string WRONG_OUTPUT_FORMAT = "Incorrectly formatted output.";
  const string TEST_DATA_ERROR = "Error in official input or output.";
  const string WRONG = "Incorrect.";
  const string CORRECT = "Correct.";

  // Read official input
  int N;
  if (!(fin >> N)) finish(0, TEST_DATA_ERROR);

  vector<vector<bool>> sols;
  for (int i = 0; i < 3; ++i) {
    vector<bool> sol;
    for (int j = 0; j < N; ++j) {
      int x;
      if (!(fin >> x)) finish(0, TEST_DATA_ERROR);
      if (x != 0 && x != 1) finish(0, TEST_DATA_ERROR);
      sol.push_back(x);
    }
    sols.push_back(sol);
  }

  // Read first line of official output
  int M_official;
  if (!(foff >> M_official)) finish(0, TEST_DATA_ERROR);
  
  // Read contestant's output
  int M;
  if (!(fout >> M)) finish(0, WRONG_OUTPUT_FORMAT);

  if (M == -1 && M_official != -1) {
    finish(0, WRONG + " Received -1, but solution exists.");
  }
  if (M != -1 && M_official == -1) {
    finish(0, WRONG + " Solution received, but solution doesn't exist.");
  }
 
  if (M != -1) { // Solution exists, check if it's valid
    if (M <= 0) {
      finish(0, WRONG + " Invalid number of constraints: " + to_string(M) + ".");
    }
    if (M > 500) {
      finish(0, WRONG + " Too many constraints.");
    }
    
    map<string, int> literals;
    for (int i = 1; i <= N; ++i) {
      literals["x" + std::to_string(i)] = 2*(i-1) + 1;
      literals["!x" + std::to_string(i)] = 2*(i-1);
    }

    vector<vector<bool>> E(2*N, vector<bool>(2*N, false));
    // Each line consists of 3 strings
    for (int i = 0; i < M; ++i) {
      string A, B, C;
      if (!(fout >> A >> B >> C)) finish(0, WRONG_OUTPUT_FORMAT);
      if (B != "->") finish(0, WRONG_OUTPUT_FORMAT + " Invalid constraint.");

      if (!literals.count(A) || !literals.count(C)) finish(0, WRONG_OUTPUT_FORMAT + " Invalid constraint.");
      int x = literals[A];
      int y = literals[C];

      E[x][y] = true;
    }

    // Check if all three solutions from input are valid
    for (int i = 0; i < 3; ++i) {
      if (!TwoSat::check_solution(E, sols[i])) finish(0, WRONG + " Assignment no." + to_string(i+1) + " from the input does not satisfy received constraints.");
    }

    // Check if there is more solutions
    if (TwoSat::count_solutions(E) != 3) finish(0, WRONG + " More than 3 assignments satisfy received constraints.");
  }
    
  string tmp_buf;
  if (fout >> tmp_buf) finish(0, WRONG_OUTPUT_FORMAT);
  finish(1, CORRECT);
  // The function MUST terminate before this line via finish()!
}

void finish(double p, const string& m) {
  cout << p << endl;
  cout << m << endl;
  exit(0);
}

int main(int argc, char *argv[])
{
  assert(argc == 4);

  ifstream fin(argv[1]);
  ifstream foff(argv[2]);
  ifstream fout(argv[3]);

  assert(!fin.fail() && !fout.fail());
  checker(fin, foff, fout);
  assert(false); // checker must terminate via finish() before exiting!

  return 0;
}