import java.io.PrintWriter
import scala.io.Source._
import scala.Some
import scala.collection.{mutable => m}

/**
 * @author sugak andrey
 */
object Task1 {
  val parser = new ExprParser()
  //  var data = new m.HashMap[Expr, m.Set[(Implication, Int)]]() with m.MultiMap[Expr, (Implication, Int)]
  var ctx = m.HashMap[Expr, (Implication, Int)]()
  var stored = m.HashMap[Expr, (Expr, Int)]()

  def isAxiom(expr: Expr): Option[Axiom] = expr match {
    case Implication(a, Implication(_, b)) if a == b => Some(Axiom(1))
    case Implication(Implication(a, b), Implication(Implication(c, Implication(d, e)), Implication(f, g)))
      if (a, b, e) == (c, d, g) && a == f => Some(Axiom(2))
    case Implication(a, Implication(b, Conj(c, d))) if (a, b) ==(c, d) => Some(Axiom(3))
    case Implication(Conj(a, _), c) if a == c => Some(Axiom(4))
    case Implication(Conj(_, b), c) if b == c => Some(Axiom(5))
    case Implication(a, Disj(b, c)) if a == b => Some(Axiom(6))
    case Implication(a, Disj(b, c)) if a == c => Some(Axiom(7))
    case Implication(Implication(a, b), Implication(Implication(c, d), Implication(Disj(e, f), g)))
      if (a, b, c) == (e, g, f) && b == d => Some(Axiom(8))
    case Implication(Implication(a, b), Implication(Implication(c, Negation(d)), Negation(e)))
      if (a, b) == (c, d) && a == e => Some(Axiom(9))
    case Implication(Negation(Negation(a)), b) if a == b => Some(Axiom(10))
    case _ => None
  }

  def MP(e: Expr): Reason = {
    ctx.get(e) match {
      case Some((impl: Implication, i: Int)) => stored.get(impl.lhs) match {
        case Some((x: Expr, j: Int)) => ModusPonens(j + 1, i + 1)
        case _ => Mistake()
      }
      case _ => Mistake()
    }
  }

  def showReason(e: Expr): String = isAxiom(e) match {
    case Some(axiom) => axiom.toString
    case _ => MP(e).toString
  }

  def saveEntries(entry: (Expr, Int)): Unit = {
    stored += (entry._1 -> entry)
    entry._1 match {
      case i@Implication(_, second) => ctx += (second -> (i, entry._2 ))
      case _ => None
    }
  }

  def process(s: (String, Int)): String = {
    val e = parser.parse(s._1).get
    saveEntries(e, s._2)
    s"${s._1} ${showReason(e)}"
  }

  def main(args: Array[String]) {
    val out = new PrintWriter("out1.txt")
    fromFile("in.txt").getLines().zipWithIndex.map(process).foreach(s => out.write(s + "\n"))
    out.close()
  }

}