acts2cnf

acts2cnf/Banking1.acts

@@ -0,0 +1,123 @@
+[System]
+ss
+
+[Parameter]
+p1 (enum): v1, v2, v3
+p2 (enum): v1, v2, v3, v4
+p3 (enum): v1, v2, v3
+p4 (enum): v1, v2, v3
+p5 (enum): v1, v2, v3
+
+[Constraint]
+C1: (p5 != "v1" || p2 != "v4" || p3 != "v2" || p4 != "v3" || p1 != "v1")
+C2: (p1 != "v3" || p5 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3")
+C3: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v1")
+C4: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v1" || p2 != "v2")
+C5: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v3")
+C6: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p2 != "v4" || p4 != "v2")
+C7: (p5 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3" || p1 != "v1")
+C8: (p4 != "v2" || p3 != "v1" || p2 != "v3" || p5 != "v3" || p1 != "v1")
+C9: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p2 != "v4" || p3 != "v1")
+C10: (p5 != "v1" || p1 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1")
+C11: (p5 != "v1" || p2 != "v4" || p4 != "v2" || p3 != "v1" || p1 != "v1")
+C12: (p1 != "v3" || p5 != "v1" || p2 != "v4" || p3 != "v2" || p4 != "v3")
+C13: (p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v1" || p5 != "v3")
+C14: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v1" || p2 != "v3")
+C15: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v1")
+C16: (p1 != "v3" || p5 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1")
+C17: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v3")
+C18: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v3" || p2 != "v2")
+C19: (p5 != "v1" || p1 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1")
+C20: (p5 != "v1" || p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v4")
+C21: (p4 != "v1" || p3 != "v3" || p5 != "v3" || p1 != "v1" || p2 != "v2")
+C22: (p5 != "v1" || p4 != "v1" || p2 != "v4" || p3 != "v2" || p1 != "v1")
+C23: (p1 != "v3" || p2 != "v4" || p3 != "v2" || p4 != "v3" || p5 != "v3")
+C24: (p5 != "v1" || p4 != "v1" || p1 != "v2" || p3 != "v1" || p2 != "v3")
+C25: (p1 != "v3" || p4 != "v1" || p3 != "v2" || p2 != "v3" || p5 != "v3")
+C26: (p5 != "v1" || p4 != "v1" || p3 != "v1" || p1 != "v1" || p2 != "v2")
+C27: (p1 != "v3" || p2 != "v4" || p4 != "v2" || p3 != "v1" || p5 != "v3")
+C28: (p1 != "v3" || p3 != "v3" || p4 != "v2" || p2 != "v1" || p5 != "v3")
+C29: (p5 != "v1" || p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v1")
+C30: (p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v3" || p1 != "v1")
+C31: (p5 != "v1" || p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v3")
+C32: (p5 != "v2" || p3 != "v3" || p2 != "v4" || p4 != "v3" || p1 != "v1")
+C33: (p1 != "v3" || p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v3")
+C34: (p4 != "v1" || p1 != "v2" || p2 != "v4" || p3 != "v1" || p5 != "v3")
+C35: (p1 != "v3" || p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v1")
+C36: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v1")
+C37: (p1 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1" || p5 != "v3")
+C38: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v3")
+C39: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v4")
+C40: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p3 != "v1" || p2 != "v2")
+C41: (p1 != "v3" || p5 != "v2" || p3 != "v3" || p2 != "v4" || p4 != "v3")
+C42: (p1 != "v3" || p5 != "v1" || p4 != "v2" || p3 != "v1" || p2 != "v3")
+C43: (p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v1" || p1 != "v1")
+C44: (p1 != "v3" || p5 != "v1" || p4 != "v3" || p3 != "v1" || p2 != "v2")
+C45: (p1 != "v3" || p5 != "v1" || p2 != "v4" || p4 != "v2" || p3 != "v1")
+C46: (p1 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1" || p5 != "v3")
+C47: (p4 != "v3" || p3 != "v1" || p5 != "v3" || p1 != "v1" || p2 != "v2")
+C48: (p5 != "v1" || p4 != "v1" || p1 != "v2" || p2 != "v1" || p3 != "v1")
+C49: (p3 != "v3" || p2 != "v4" || p4 != "v2" || p5 != "v3" || p1 != "v1")
+C50: (p5 != "v1" || p3 != "v3" || p2 != "v4" || p4 != "v2" || p1 != "v1")
+C51: (p1 != "v3" || p5 != "v1" || p4 != "v2" || p2 != "v1" || p3 != "v1")
+C52: (p1 != "v3" || p4 != "v1" || p3 != "v2" || p2 != "v1" || p5 != "v3")
+C53: (p1 != "v3" || p3 != "v3" || p4 != "v3" || p5 != "v3" || p2 != "v2")
+C54: (p1 != "v3" || p3 != "v2" || p4 != "v3" || p2 != "v1" || p5 != "v3")
+C55: (p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v4" || p5 != "v3")
+C56: (p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v1" || p1 != "v1")
+C57: (p1 != "v3" || p5 != "v1" || p4 != "v1" || p2 != "v4" || p3 != "v2")
+C58: (p1 != "v3" || p4 != "v1" || p2 != "v4" || p3 != "v2" || p5 != "v3")
+C59: (p4 != "v1" || p1 != "v2" || p3 != "v1" || p2 != "v3" || p5 != "v3")
+C60: (p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v1" || p1 != "v1")
+C61: (p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v3" || p1 != "v1")
+C62: (p4 != "v2" || p2 != "v1" || p3 != "v1" || p5 != "v3" || p1 != "v1")
+C63: (p5 != "v2" || p4 != "v1" || p2 != "v1" || p3 != "v1" || p1 != "v1")
+C64: (p5 != "v1" || p4 != "v2" || p3 != "v1" || p2 != "v3" || p1 != "v1")
+C65: (p4 != "v1" || p2 != "v4" || p3 != "v2" || p5 != "v3" || p1 != "v1")
+C66: (p1 != "v3" || p4 != "v1" || p3 != "v3" || p5 != "v3" || p2 != "v2")
+C67: (p1 != "v3" || p4 != "v1" || p3 != "v1" || p5 != "v3" || p2 != "v2")
+C68: (p4 != "v1" || p1 != "v2" || p2 != "v1" || p3 != "v1" || p5 != "v3")
+C69: (p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v3" || p5 != "v3")
+C70: (p1 != "v3" || p5 != "v2" || p4 != "v1" || p2 != "v1" || p3 != "v1")
+C71: (p5 != "v1" || p4 != "v2" || p2 != "v1" || p3 != "v1" || p1 != "v1")
+C72: (p5 != "v2" || p4 != "v1" || p3 != "v1" || p2 != "v3" || p1 != "v1")
+C73: (p4 != "v1" || p3 != "v1" || p5 != "v3" || p1 != "v1" || p2 != "v2")
+C74: (p5 != "v2" || p4 != "v1" || p2 != "v4" || p3 != "v1" || p1 != "v1")
+C75: (p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v3" || p1 != "v1")
+C76: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v3")
+C77: (p1 != "v3" || p4 != "v3" || p3 != "v1" || p5 != "v3" || p2 != "v2")
+C78: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p4 != "v2" || p2 != "v1")
+C79: (p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v3" || p1 != "v1")
+C80: (p1 != "v3" || p3 != "v3" || p4 != "v2" || p2 != "v3" || p5 != "v3")
+C81: (p1 != "v3" || p5 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1")
+C82: (p1 != "v3" || p3 != "v2" || p4 != "v3" || p2 != "v3" || p5 != "v3")
+C83: (p1 != "v3" || p4 != "v2" || p3 != "v1" || p2 != "v3" || p5 != "v3")
+C84: (p5 != "v1" || p1 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3")
+C85: (p3 != "v3" || p4 != "v2" || p2 != "v3" || p5 != "v3" || p1 != "v1")
+C86: (p5 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v4" || p4 != "v3")
+C87: (p4 != "v1" || p3 != "v2" || p2 != "v1" || p5 != "v3" || p1 != "v1")
+C88: (p5 != "v1" || p3 != "v2" || p4 != "v3" || p2 != "v3" || p1 != "v1")
+C89: (p2 != "v4" || p4 != "v2" || p3 != "v1" || p5 != "v3" || p1 != "v1")
+C90: (p1 != "v3" || p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v3")
+C91: (p5 != "v1" || p4 != "v1" || p1 != "v2" || p2 != "v4" || p3 != "v1")
+C92: (p3 != "v3" || p1 != "v2" || p4 != "v3" || p2 != "v3" || p5 != "v3")
+C93: (p1 != "v3" || p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v1")
+C94: (p1 != "v3" || p5 != "v1" || p3 != "v3" || p4 != "v3" || p2 != "v2")
+C95: (p4 != "v1" || p3 != "v3" || p1 != "v2" || p2 != "v1" || p5 != "v3")
+C96: (p2 != "v4" || p3 != "v2" || p4 != "v3" || p5 != "v3" || p1 != "v1")
+C97: (p4 != "v1" || p3 != "v2" || p2 != "v3" || p5 != "v3" || p1 != "v1")
+C98: (p3 != "v2" || p4 != "v3" || p2 != "v1" || p5 != "v3" || p1 != "v1")
+C99: (p3 != "v3" || p1 != "v2" || p2 != "v4" || p4 != "v3" || p5 != "v3")
+C100: (p1 != "v2" || p4 != "v3" || p3 != "v1" || p2 != "v3" || p5 != "v3")
+C101: (p5 != "v2" || p4 != "v3" || p2 != "v1" || p3 != "v1" || p1 != "v1")
+C102: (p1 != "v3" || p4 != "v2" || p2 != "v1" || p3 != "v1" || p5 != "v3")
+C103: (p3 != "v3" || p4 != "v3" || p5 != "v3" || p1 != "v1" || p2 != "v2")
+C104: (p5 != "v1" || p3 != "v3" || p4 != "v3" || p1 != "v1" || p2 != "v2")
+C105: (p3 != "v2" || p4 != "v3" || p2 != "v3" || p5 != "v3" || p1 != "v1")
+C106: (p5 != "v2" || p2 != "v4" || p4 != "v3" || p3 != "v1" || p1 != "v1")
+C107: (p1 != "v3" || p3 != "v3" || p2 != "v4" || p4 != "v2" || p5 != "v3")
+C108: (p5 != "v1" || p4 != "v3" || p3 != "v1" || p1 != "v1" || p2 != "v2")
+C109: (p5 != "v1" || p4 != "v1" || p3 != "v2" || p2 != "v1" || p1 != "v1")
+C110: (p5 != "v2" || p4 != "v1" || p3 != "v3" || p2 != "v4" || p1 != "v1")
+C111: (p3 != "v3" || p4 != "v2" || p2 != "v1" || p5 != "v3" || p1 != "v1")
+C112: (p5 != "v2" || p3 != "v3" || p4 != "v3" || p2 != "v1" || p1 != "v1")

acts2cnf/tran.cc

@@ -0,0 +1,163 @@
+// =====================================================================================
+//
+//       Filename:  tran.cc
+//
+//    Description:  transform input of acts to cnf
+//
+//        Version:  1.0
+//        Created:  2019年 01月 05日 星期六 07:43:30 CST
+//       Revision:  none
+//       Compiler:  g++
+//
+//         Author:  Jinkun Lin, jkunlin@gmail.com
+//   Organization:  School of EECS, Peking University
+//
+// =====================================================================================
+#include <fstream>
+#include <iostream>
+#include <map>
+#include <sstream>
+#include <string>
+#include <vector>
+using namespace std;
+
+struct Literal {
+  char sign;
+  int value;
+  Literal(char s, int v) : sign(s), value(v) {}
+};
+
+struct Clause {
+  vector<Literal> lits;
+};
+
+int main(int argc, char const *argv[]) {
+  if (argc != 2) {
+    cout << "usage: " << endl;
+    return 1;
+  }
+  ifstream infile(argv[1]);
+  if (!infile) {
+    cout << "infile error" << endl;
+    return 1;
+  }
+
+  string line;
+  while (getline(infile, line)) {
+    if (line.find("Parameter") != line.npos) {
+      break;
+    }
+  }
+
+  map<string, int> parameter;
+  vector<map<string, int>> value;
+  int cur_pid = 0;
+  int cur_vid = 0;
+  string tmp_str;
+  while (getline(infile, line)) {
+    if (line.find("Constraint") != line.npos) {
+      break;
+    }
+    istringstream is(line);
+
+    string p;
+    is >> p >> tmp_str;
+    if (!is) {
+      if (line.size() != 1) {
+        abort();
+      }
+      continue;
+    }
+    parameter.insert(make_pair(p, cur_pid++));
+    value.push_back(map<string, int>());
+
+    string v;
+    while (is >> v) {
+      if (v[v.size() - 1] == ',') {
+        v.pop_back();
+      }
+      value[parameter[p]].insert(make_pair(v, cur_vid++));
+    }
+  }
+
+#ifndef NDEBUG
+  // for (auto p_pair : parameter) {
+  //   cout << p_pair.first << ": ";
+  //   for (auto v_pair : value[p_pair.second]) {
+  //     cout << v_pair.first << ", ";
+  //   }
+  //   cout << endl;
+  // }
+  //
+  // for (auto p_pair : parameter) {
+  //   cout << p_pair.second << ": ";
+  //   for (auto v_pair : value[p_pair.second]) {
+  //     cout << v_pair.second << ", ";
+  //   }
+  //   cout << endl;
+  // }
+  cout << 2 << endl;
+  cout << parameter.size() << endl;
+  auto iter = parameter.begin();
+  cout << value[iter->second].size();
+  for (++iter; iter != parameter.end(); ++iter) {
+    cout << ' ' << value[iter->second].size();
+  }
+  cout << endl;
+#endif
+
+  vector<Clause> formular;
+  char tmp_ch;
+  while (getline(infile, line)) {
+    istringstream is(line);
+    is >> tmp_str >> tmp_ch;
+
+    string p, v;
+    char sign;
+    Clause c;
+    do {
+      is >> p >> tmp_str >> tmp_ch;
+
+      // sign
+      if (tmp_str == "!=") {
+        sign = '-';
+      } else if (tmp_str == "=") {
+        sign = '+';
+      } else {
+        cout << "error operator" << endl;
+        return 1;
+      }
+
+      // value
+      is >> v;
+      if (v[v.size() - 1] == '"') {
+        v.pop_back();
+      } else if (v[v.size() - 1] == ')' && v[v.size() - 2] == '"') {
+        v.pop_back();
+        v.pop_back();
+      } else {
+        cout << "format error: " << v << endl;
+        return 1;
+      }
+
+      c.lits.push_back(Literal(sign, value[parameter[p]][v]));
+
+      // operator
+      is >> tmp_str;
+    } while (tmp_str == "||");
+    formular.push_back(c);
+  }
+
+#ifndef NDEBUG
+  cout << formular.size() << endl;
+  for (auto c : formular) {
+    cout << c.lits.size() << endl;
+    cout << c.lits[0].sign << ' ' << c.lits[0].value;
+    for (int i = 1; i < (int)c.lits.size(); ++i) {
+      cout << ' ' << c.lits[i].sign << ' ' << c.lits[i].value;
+    }
+    cout << endl;
+  }
+#endif
+  return 0;
+}

acts2cnf/x

@@ -0,0 +1,228 @@
+2
+5
+3 4 3 3 3
+112
+5
+- 13 - 6 - 8 - 12 - 0
+5
+- 2 - 14 - 12 - 7 - 5
+5
+- 2 - 13 - 10 - 8 - 3
+5
+- 13 - 10 - 9 - 0 - 4
+5
+- 2 - 13 - 10 - 8 - 5
+5
+- 2 - 13 - 9 - 6 - 11
+5
+- 14 - 12 - 7 - 5 - 0
+5
+- 11 - 7 - 5 - 15 - 0
+5
+- 2 - 14 - 10 - 6 - 7
+5
+- 13 - 1 - 6 - 12 - 7
+5
+- 13 - 6 - 11 - 7 - 0
+5
+- 2 - 13 - 6 - 8 - 12
+5
+- 9 - 1 - 12 - 3 - 15
+5
+- 2 - 14 - 10 - 7 - 5
+5
+- 13 - 10 - 9 - 1 - 3
+5
+- 2 - 14 - 6 - 12 - 7
+5
+- 13 - 10 - 9 - 1 - 5
+5
+- 2 - 13 - 10 - 9 - 4
+5
+- 13 - 1 - 12 - 3 - 7
+5
+- 13 - 10 - 9 - 1 - 6
+5
+- 10 - 9 - 15 - 0 - 4
+5
+- 13 - 10 - 6 - 8 - 0
+5
+- 2 - 6 - 8 - 12 - 15
+5
+- 13 - 10 - 1 - 7 - 5
+5
+- 2 - 10 - 8 - 5 - 15
+5
+- 13 - 10 - 7 - 0 - 4
+5
+- 2 - 6 - 11 - 7 - 15
+5
+- 2 - 9 - 11 - 3 - 15
+5
+- 13 - 9 - 1 - 12 - 3
+5
+- 13 - 9 - 11 - 5 - 0
+5
+- 13 - 9 - 1 - 12 - 5
+5
+- 14 - 9 - 6 - 12 - 0
+5
+- 2 - 13 - 8 - 12 - 5
+5
+- 10 - 1 - 6 - 7 - 15
+5
+- 2 - 13 - 8 - 12 - 3
+5
+- 2 - 14 - 10 - 9 - 3
+5
+- 1 - 6 - 12 - 7 - 15
+5
+- 2 - 14 - 10 - 9 - 5
+5
+- 2 - 14 - 10 - 9 - 6
+5
+- 2 - 13 - 10 - 7 - 4
+5
+- 2 - 14 - 9 - 6 - 12
+5
+- 2 - 13 - 11 - 7 - 5
+5
+- 14 - 10 - 9 - 3 - 0
+5
+- 2 - 13 - 12 - 7 - 4
+5
+- 2 - 13 - 6 - 11 - 7
+5
+- 1 - 12 - 3 - 7 - 15
+5
+- 12 - 7 - 15 - 0 - 4
+5
+- 13 - 10 - 1 - 3 - 7
+5
+- 9 - 6 - 11 - 15 - 0
+5
+- 13 - 9 - 6 - 11 - 0
+5
+- 2 - 13 - 11 - 3 - 7
+5
+- 2 - 10 - 8 - 3 - 15
+5
+- 2 - 9 - 12 - 15 - 4
+5
+- 2 - 8 - 12 - 3 - 15
+5
+- 10 - 9 - 1 - 6 - 15
+5
+- 13 - 9 - 11 - 3 - 0
+5
+- 2 - 13 - 10 - 6 - 8
+5
+- 2 - 10 - 6 - 8 - 15
+5
+- 10 - 1 - 7 - 5 - 15
+5
+- 13 - 8 - 12 - 3 - 0
+5
+- 14 - 10 - 9 - 5 - 0
+5
+- 11 - 3 - 7 - 15 - 0
+5
+- 14 - 10 - 3 - 7 - 0
+5
+- 13 - 11 - 7 - 5 - 0
+5
+- 10 - 6 - 8 - 15 - 0
+5
+- 2 - 10 - 9 - 15 - 4
+5
+- 2 - 10 - 7 - 15 - 4
+5
+- 10 - 1 - 3 - 7 - 15
+5
+- 10 - 9 - 1 - 5 - 15
+5
+- 2 - 14 - 10 - 3 - 7
+5
+- 13 - 11 - 3 - 7 - 0
+5
+- 14 - 10 - 7 - 5 - 0
+5
+- 10 - 7 - 15 - 0 - 4
+5
+- 14 - 10 - 6 - 7 - 0
+5
+- 13 - 10 - 8 - 5 - 0
+5
+- 2 - 13 - 9 - 11 - 5
+5
+- 2 - 12 - 7 - 15 - 4
+5
+- 2 - 13 - 9 - 11 - 3
+5
+- 14 - 9 - 12 - 5 - 0
+5
+- 2 - 9 - 11 - 5 - 15
+5
+- 2 - 14 - 12 - 3 - 7
+5
+- 2 - 8 - 12 - 5 - 15
+5
+- 2 - 11 - 7 - 5 - 15
+5
+- 13 - 1 - 12 - 7 - 5
+5
+- 9 - 11 - 5 - 15 - 0
+5
+- 13 - 9 - 1 - 6 - 12
+5
+- 10 - 8 - 3 - 15 - 0
+5
+- 13 - 8 - 12 - 5 - 0
+5
+- 6 - 11 - 7 - 15 - 0
+5
+- 2 - 14 - 9 - 12 - 5
+5
+- 13 - 10 - 1 - 6 - 7
+5
+- 9 - 1 - 12 - 5 - 15
+5
+- 2 - 14 - 9 - 12 - 3
+5
+- 2 - 13 - 9 - 12 - 4
+5
+- 10 - 9 - 1 - 3 - 15
+5
+- 6 - 8 - 12 - 15 - 0
+5
+- 10 - 8 - 5 - 15 - 0
+5
+- 8 - 12 - 3 - 15 - 0
+5
+- 9 - 1 - 6 - 12 - 15
+5
+- 1 - 12 - 7 - 5 - 15
+5
+- 14 - 12 - 3 - 7 - 0
+5
+- 2 - 11 - 3 - 7 - 15
+5
+- 9 - 12 - 15 - 0 - 4
+5
+- 13 - 9 - 12 - 0 - 4
+5
+- 8 - 12 - 5 - 15 - 0
+5
+- 14 - 6 - 12 - 7 - 0
+5
+- 2 - 9 - 6 - 11 - 15
+5
+- 13 - 12 - 7 - 0 - 4
+5
+- 13 - 10 - 8 - 3 - 0
+5
+- 14 - 10 - 9 - 6 - 0
+5
+- 9 - 11 - 3 - 15 - 0
+5
+- 14 - 9 - 12 - 3 - 0