Problem: Hibiki and Dita are in love with each other, but belong to communities that are in a long lasting conflict. Hibiki is deeply concerned with the state of affairs, and wants to figure out if his relationship with Dita is an act of love or an act of treason.

<image>

Hibiki prepared several binary features his decision will depend on, and built a three layer logical circuit on top of them, each layer consisting of one or more [logic gates](https://en.wikipedia.org/wiki/Logic_gate). Each gate in the circuit is either "or", "and", "nor" (not or) or "nand" (not and). Each gate in the first layer is connected to exactly two features. Each gate in the second layer is connected to exactly two gates in the first layer. The third layer has only one "or" gate, which is connected to all the gates in the second layer (in other words, the entire circuit produces 1 if and only if at least one gate in the second layer produces 1).

The problem is, Hibiki knows very well that when the person is in love, his ability to think logically degrades drastically. In particular, it is well known that when a person in love evaluates a logical circuit in his mind, every gate evaluates to a value that is the opposite of what it was supposed to evaluate to. For example, "or" gates return 1 if and only if both inputs are zero, "t{nand}" gates produce 1 if and only if both inputs are one etc.

In particular, the "or" gate in the last layer also produces opposite results, and as such if Hibiki is in love, the entire circuit produces 1 if and only if all the gates on the second layer produced 0.

Hibiki can’t allow love to affect his decision. He wants to know what is the smallest number of gates that needs to be removed from the second layer so that the output of the circuit for all possible inputs doesn't depend on whether Hibiki is in love or not.

Input

The first line contains three integers n, m, k (2 ≤ n, m ≤ 50; 1 ≤ k ≤ 50) — the number of input features, the number of gates in the first layer, and the number of gates in the second layer correspondingly.

The second line contains m pairs of strings separated by spaces describing the first layer. The first string in each pair describes the gate ("and", "or", "nand" or "nor"), and the second string describes the two input features the gate is connected two as a string consisting of exactly n characters, with exactly two characters (that correspond to the input features the gate is connected to) equal to 'x' and the remaining characters equal to ".'.

The third line contains k pairs of strings separated by spaces describing the second layer in the same format, where the strings that describe the input parameters have length m and correspond to the gates of the first layer.

Output

Print the number of gates that need to be removed from the second layer so that the output of the remaining circuit doesn't depend on whether Hibiki is in love or not.

If no matter how many gates are removed the output of the circuit continues to depend on Hibiki's feelings, print -1.

Examples

Input

2 2 2
and xx nand xx
and xx or xx


Output

1


Input

3 2 2
and xx. nor .xx
and xx nor xx


Output

-1


Input

4 4 5
nor x..x and ..xx and xx.. nand xx..
nand ..xx nor ..xx and xx.. nor ..xx or ..xx


Output

2

Note

In the first example the two gates in the first layer are connected to the same inputs, but first computes "and" while second computes "nand", and as such their output is always different no matter what the input is and whether Hibiki is in love or not. The second layer has "or" and "and" gates both connected to the two gates in the first layer. If Hibiki is not in love, the "and" gate will produce 0 and the "or" gate will produce 1 no matter what input features are equal to, with the final "or" gate in the third layer always producing the final answer of 1. If Hibiki is in love, "and" gate in the second layer will produce 1 and "or" gate will produce 0 no matter what the input is, with the final "or" gate in the third layer producing the final answer of 0. Thus, if both gates in the second layer are kept, the output of the circuit does depend on whether Hibiki is in love. If any of the two gates in the second layer is dropped, the output of the circuit will no longer depend on whether Hibiki is in love or not, and hence the answer is 1.

In the second example no matter what gates are left in the second layer, the output of the circuit will depend on whether Hibiki is in love or not.

In the third example if Hibiki keeps second, third and fourth gates in the second layer, the circuit will not depend on whether Hibiki is in love or not. Alternatively, he can keep the first and the last gates. The former requires removing two gates, the latter requires removing three gates, so the former is better, and the answer is 2.

Solution (in CPP):

Solution:
#include <bits/stdc++.h>
using namespace std;
struct tarjan_t {
  int n;
  vector<vector<int>> adj;
  vector<int> preorder, inv_preorder, highest_reach;
  stack<int> active;
  vector<bool> is_active;
  vector<vector<int>> cnts;
  vector<int> cnt_of;
  tarjan_t(int _n)
      : n(_n),
        adj(n),
        inv_preorder(n, -1),
        highest_reach(n, n),
        is_active(n, false),
        cnt_of(n, -1) {}
  void dfs(int v) {
    inv_preorder[v] = preorder.size();
    preorder.push_back(v);
    highest_reach[v] = inv_preorder[v];
    active.push(v);
    is_active[v] = true;
    for (int u : adj[v]) {
      if (inv_preorder[u] == -1) {
        dfs(u);
        highest_reach[v] = min(highest_reach[v], highest_reach[u]);
      } else if (is_active[u]) {
        highest_reach[v] = min(highest_reach[v], inv_preorder[u]);
      }
    }
    if (highest_reach[v] == inv_preorder[v]) {
      vector<int> cnt;
      int u;
      do {
        u = active.top();
        active.pop();
        is_active[u] = false;
        cnt.push_back(u);
        cnt_of[u] = cnts.size();
      } while (u != v);
      cnts.push_back(move(cnt));
    }
  }
  void solve() {
    for (int v = 0; v < n; ++v)
      if (inv_preorder[v] == -1) dfs(v);
  }
};
struct twosat_t {
  int n;
  vector<vector<int>> adj;
  twosat_t() {}
  twosat_t(int _n) : n(_n), adj(2 * n) {}
  void add_implication(int a, int b) { adj[a].push_back(b); }
  bool solve() {
    tarjan_t tarjan(2 * n);
    tarjan.adj = adj;
    tarjan.solve();
    for (int i = 0; i < n; ++i)
      if (tarjan.cnt_of[2 * i] == tarjan.cnt_of[2 * i + 1]) return false;
    return true;
  }
};
enum gate_t {
  AND,
  OR,
  NAND,
  NOR,
};
gate_t mirror(gate_t g) {
  if (g == AND) return OR;
  if (g == OR) return AND;
  if (g == NAND) return NOR;
  if (g == NOR) return NAND;
  assert(false);
  return (gate_t)-1;
}
int apply_gate(gate_t g, int a, int b) {
  if (g == AND) return a & b;
  if (g == OR) return a | b;
  if (g == NAND) return !(a & b);
  if (g == NOR) return !(a | b);
  assert(false);
  return -1;
}
const char *gate_to_string(gate_t g) {
  if (g == AND) return "and";
  if (g == OR) return "or";
  if (g == NAND) return "nand";
  if (g == NOR) return "nor";
  return "";
}
struct expr_t {
  int input_id = -1;
  gate_t gate;
  expr_t *sub0 = nullptr, *sub1 = nullptr;
  int enforce_value = -1;
  expr_t() {}
  expr_t(int _id) : input_id(_id) {}
  expr_t(gate_t _gate, expr_t *_sub0, expr_t *_sub1)
      : gate(_gate), sub0(_sub0), sub1(_sub1) {}
  int compute_normal() {
    if (enforce_value != -1) return enforce_value;
    assert(input_id == -1);
    return apply_gate(gate, sub0->compute_normal(), sub1->compute_normal());
  }
  int compute_changed() {
    if (enforce_value != -1) return enforce_value;
    assert(input_id == -1);
    return apply_gate(mirror(gate), sub0->compute_normal(),
                      sub1->compute_normal());
  }
  void add_constraints(int target_value, twosat_t &twosat) {
    assert(sub0->input_id >= 0);
    assert(sub1->input_id >= 0);
    bool v0_implies_v1[2][2] = {{true, true}, {true, true}};
    bool v1_implies_v0[2][2] = {{true, true}, {true, true}};
    for (int v0 = 0; v0 < 2; ++v0)
      for (int v1 = 0; v1 < 2; ++v1) {
        int res = apply_gate(gate, v0, v1);
        if (res == target_value) {
          v0_implies_v1[v0][v1 ^ 1] = false;
          v1_implies_v0[v1][v0 ^ 1] = false;
        }
      }
    for (int v0 = 0; v0 < 2; ++v0)
      for (int v1 = 0; v1 < 2; ++v1)
        if (v0_implies_v1[v0][v1]) {
          twosat.add_implication(sub0->input_id * 2 + v0,
                                 sub1->input_id * 2 + v1);
        }
    for (int v1 = 0; v1 < 2; ++v1)
      for (int v0 = 0; v0 < 2; ++v0)
        if (v1_implies_v0[v1][v0]) {
          twosat.add_implication(sub1->input_id * 2 + v1,
                                 sub0->input_id * 2 + v0);
        }
  }
};
string read_string() {
  char *str;
  scanf("%ms", &str);
  string result(str);
  free(str);
  return result;
}
vector<int> read_gate_ids() {
  string s = read_string();
  vector<int> result;
  for (int i = 0; i < (int)s.size(); ++i)
    if (s[i] == 'x') result.push_back(i);
  assert((int)result.size() == 2);
  return result;
}
gate_t gate_from_str(const string &s) {
  if (s == "and") return AND;
  if (s == "nand") return NAND;
  if (s == "or") return OR;
  if (s == "nor") return NOR;
  assert(false);
  return (gate_t)-1;
}
void add_inputs(expr_t *expr, vector<int> &output) {
  if (expr->input_id >= 0) output.push_back(expr->input_id);
  if (expr->sub0) add_inputs(expr->sub0, output);
  if (expr->sub1) add_inputs(expr->sub1, output);
}
vector<int> get_inputs(vector<expr_t *> exprs) {
  vector<int> result;
  for (expr_t *expr : exprs) add_inputs(expr, result);
  sort(result.begin(), result.end());
  result.resize(unique(result.begin(), result.end()) - result.begin());
  return result;
}
void dfs(int v, int side, vector<bool> &mark, vector<vector<int>> &adj,
         vector<int> &side0, vector<int> &side1) {
  mark[v] = true;
  if (side == 0)
    side0.push_back(v);
  else
    side1.push_back(v);
  for (int u : adj[v])
    if (!mark[u]) dfs(u, side ^ 1, mark, adj, side0, side1);
}
int main() {
  int ni, nl1, nl2;
  scanf("%d %d %d", &ni, &nl1, &nl2);
  vector<expr_t> input_exprs(ni);
  for (int i = 0; i < ni; ++i) {
    input_exprs[i] = expr_t(i);
  }
  vector<expr_t> l1exprs(nl1);
  for (int i = 0; i < nl1; ++i) {
    string gate_str = read_string();
    vector<int> ids = read_gate_ids();
    l1exprs[i] = expr_t(gate_from_str(gate_str), &input_exprs[ids[0]],
                        &input_exprs[ids[1]]);
  }
  vector<expr_t> l2exprs(nl2);
  for (int i = 0; i < nl2; ++i) {
    string gate_str = read_string();
    vector<int> ids = read_gate_ids();
    l2exprs[i] =
        expr_t(gate_from_str(gate_str), &l1exprs[ids[0]], &l1exprs[ids[1]]);
  }
  int nalways_use = 0;
  vector<expr_t> new_l2exprs;
  for (int i = 0; i < nl2; ++i) {
    vector<int> input_ids = get_inputs({&l2exprs[i]});
    bool never_use = false, always_use = true;
    for (int s = 0; s < (1 << input_ids.size()); ++s) {
      for (int j = 0; j < (int)input_ids.size(); ++j) {
        input_exprs[input_ids[j]].enforce_value = ((s & (1 << j)) != 0);
      }
      int res_normal = l2exprs[i].compute_normal();
      int res_changed = l2exprs[i].compute_changed();
      if (res_normal && res_changed) never_use = true;
      if (res_normal || res_changed) always_use = false;
    }
    for (int j = 0; j < (int)input_ids.size(); ++j)
      input_exprs[input_ids[j]].enforce_value = -1;
    assert(!(always_use && never_use));
    if (never_use) {
    } else if (always_use) {
      ++nalways_use;
    } else {
      new_l2exprs.push_back(l2exprs[i]);
    }
  }
  l2exprs = new_l2exprs;
  int orig_nl2 = nl2;
  nl2 = l2exprs.size();
  vector<vector<int>> adj(nl2);
  for (int i = 0; i < nl2; ++i)
    for (int j = i + 1; j < nl2; ++j) {
      vector<int> input_ids = get_inputs({&l2exprs[i], &l2exprs[j]});
      bool conflict = false;
      for (int s = 0; s < (1 << input_ids.size()); ++s) {
        for (int k = 0; k < (int)input_ids.size(); ++k) {
          input_exprs[input_ids[k]].enforce_value = ((s & (1 << k)) != 0);
        }
        int res_normal =
            l2exprs[i].compute_normal() || l2exprs[j].compute_normal();
        int res_changed =
            l2exprs[i].compute_changed() || l2exprs[j].compute_changed();
        if (res_normal && res_changed) {
          conflict = true;
          break;
        }
      }
      for (int k = 0; k < (int)input_ids.size(); ++k) {
        input_exprs[input_ids[k]].enforce_value = -1;
      }
      if (conflict) {
        adj[i].push_back(j);
        adj[j].push_back(i);
      }
    }
  vector<bool> mark(nl2, false);
  vector<int> left_side, right_side;
  for (int i = 0; i < nl2; ++i)
    if (!mark[i]) {
      vector<int> side0, side1;
      dfs(i, 0, mark, adj, side0, side1);
      if (side0.size() > side1.size()) swap(side0, side1);
      left_side.insert(left_side.end(), side0.begin(), side0.end());
      right_side.insert(right_side.end(), side1.begin(), side1.end());
    }
  const int nleft = left_side.size(), nright = right_side.size();
  vector<long long> left_adj_mask(nleft);
  for (int i = 0; i < nleft; ++i) {
    left_adj_mask[i] = 0LL;
    for (int id : adj[left_side[i]]) {
      int right_pos =
          find(right_side.begin(), right_side.end(), id) - right_side.begin();
      assert(right_pos < (int)right_side.size());
      left_adj_mask[i] |= 1LL << right_pos;
    }
  }
  const int first_half = nleft / 2, second_half = (nleft + 1) / 2;
  vector<long long> first_combined(1 << first_half, 0LL);
  for (int i = 0; i < first_half; ++i)
    first_combined[1 << i] = left_adj_mask[i];
  for (int mask = 1; mask < (1 << first_half); ++mask) {
    int low_bit = mask & -mask;
    if (mask != low_bit) {
      first_combined[mask] =
          first_combined[low_bit] | first_combined[mask ^ low_bit];
    }
  }
  vector<long long> second_combined(1 << second_half, 0LL);
  for (int i = 0; i < second_half; ++i)
    second_combined[1 << i] = left_adj_mask[first_half + i];
  for (int mask = 1; mask < (1 << second_half); ++mask) {
    int low_bit = mask & -mask;
    if (mask != low_bit) {
      second_combined[mask] =
          second_combined[low_bit] | second_combined[mask ^ low_bit];
    }
  }
  const bool ensure_maximal = (nleft >= 21);
  vector<bool> seen_right_mask;
  if (ensure_maximal) seen_right_mask.resize(1 << nright, false);
  int final_result = INT_MAX;
  for (int left_mask = (1 << nleft) - 1; left_mask >= 0; --left_mask) {
    long long combined_adj =
        first_combined[left_mask & ((1 << first_half) - 1)] |
        second_combined[left_mask >> first_half];
    long long right_mask = ((1LL << nright) - 1) ^ combined_adj;
    if (ensure_maximal) {
      if (seen_right_mask[right_mask]) continue;
      seen_right_mask[right_mask] = true;
    }
    twosat_t twosat(ni);
    vector<int> candidates;
    for (int i = 0; i < nleft; ++i)
      if (left_mask & (1 << i)) candidates.push_back(left_side[i]);
    for (int i = 0; i < nright; ++i)
      if (right_mask & (1LL << i)) candidates.push_back(right_side[i]);
    for (int i = 0; i < (int)candidates.size(); ++i) {
      expr_t &expr = l2exprs[candidates[i]];
      expr_t *subs[2] = {expr.sub0, expr.sub1};
      int neutral_value_mask = -1;
      for (int value_mask = 0; value_mask < (1 << 2); ++value_mask) {
        for (int k = 0; k < 2; ++k)
          subs[k]->enforce_value = ((value_mask & (1 << k)) != 0);
        int res_normal = expr.compute_normal();
        int res_changed = expr.compute_changed();
        if (!res_normal && !res_changed) {
          neutral_value_mask = value_mask;
          break;
        }
      }
      for (int k = 0; k < 2; ++k) subs[k]->enforce_value = -1;
      assert(neutral_value_mask != -1);
      for (int k = 0; k < 2; ++k)
        subs[k]->add_constraints(((neutral_value_mask & (1 << k)) != 0),
                                 twosat);
    }
    bool ok = !twosat.solve();
    if (ok) {
      final_result =
          min(final_result, orig_nl2 - (nalways_use + (int)candidates.size()));
    }
  }
  if (final_result == INT_MAX)
    printf("-1\n");
  else
    printf("%d\n", final_result);
  return 0;
}