type expr =
        Implication of (expr * expr) |
        Conjunction of (expr * expr) |
        Disjunction of (expr * expr) |
        Negation of expr |
        Forall of (string * expr) |
        Exists of (string * expr) |
        Predicate of (string * term list) |
        Equals of (term * term)
and term =
        Add of (term * term) |
        Multiply of (term * term) |
        Var of string |
        Increment of term |
        Zero |
        Function of (string * term list)
and document = Document of (expr list * expr * expr list);;

let take s ind = if String.length s <= ind || ind < 0 then None else Some (String.get s ind);;

let rec trim s =
        match take s 0 with
        | Some ' ' -> trim (String.sub s 1 (String.length s - 1))
        | _ -> s;;

let rec trim_end s =
        match take s (String.length s - 1) with
        | Some ' ' | Some '\n' | Some '\t' -> trim_end (String.sub s 0 (String.length s - 1))
        | _ -> s;;

let rec printTerm term =
        match term with
        | Add (a, b) -> "(" ^ (printTerm a) ^ "+" ^ (printTerm b) ^ ")"
        | Multiply (a, b) -> "(" ^ (printTerm a) ^ "*" ^ (printTerm b) ^ ")"
        | Var name -> name
        | Increment a -> (printTerm a) ^ "'"
        | Zero -> "0"
        | Function (name, terms) -> name ^ "(" ^ (String.concat "," (List.map printTerm terms)) ^ ")";;

let rec printExpr expr =
        match expr with
        | Implication (a, b) -> "(" ^ (printExpr a) ^ "->" ^ (printExpr b) ^ ")"
        | Conjunction (a, b) -> "(" ^ (printExpr a) ^ "&" ^ (printExpr b) ^ ")"
        | Disjunction (a, b) -> "(" ^ (printExpr a) ^ "|" ^ (printExpr b) ^ ")"
        | Negation a -> "!" ^ (printExpr a)
        | Forall (name, e) -> "(@" ^ name ^ "." ^ (printExpr e) ^ ")"
        | Exists (name, e) -> "(?" ^ name ^ "." ^ (printExpr e) ^ ")"
        | Predicate (name, es) -> name ^ "(" ^ (String.concat "," (List.map printTerm es)) ^ ")"
        | Equals (a, b) -> (printTerm a) ^ "=" ^ (printTerm b);;

let rec parseImplication s =
        match parseDisjunction s with
        | Some (dis, s) ->
                let s = trim s in
                (match (take s 0, take s 1) with
                | (Some '-', Some '>') ->
                        let s = String.sub s 2 (String.length s - 2) in
                        (match parseImplication s with
                        | Some (impl, s) -> Some (Implication (dis, impl), s)
                        | None -> None)
                | _ -> Some (dis, s))
        | None -> None
and parseDisjunction s =
        match parseConjunction s with
        | Some (conj, s) ->
                let rec func prev s =
                        let s = trim s in
                        match take s 0 with
                        | Some '|' ->
                                let s = String.sub s 1 (String.length s - 1) in
                                (match parseConjunction s with
                                | Some (conj, s) -> func (Disjunction (prev, conj)) s
                                | None -> None)
                        | _ -> Some (prev, s) in
                func conj s
        | None -> None
and parseConjunction s =
        match parseUnary s with
        | Some (unary, s) ->
                let rec func prev s =
                        let s = trim s in
                        match take s 0 with
                        | Some '&' ->
                                let s = String.sub s 1 (String.length s - 1) in
                                (match parseUnary s with
                                | Some (unary, s) -> func (Conjunction (prev, unary)) s
                                | None -> None)
                        | _ -> Some (prev, s) in
                func unary s
        | None -> None
and parseUnary s =
        let s = trim s in
        match take s 0 with
        | Some '(' ->
                (match parseImplication (String.sub s 1 (String.length s - 1)) with
                | Some (impl, s) ->
                        let s = trim s in
                        (match take s 0 with
                        | Some ')' -> Some (impl, String.sub s 1 (String.length s - 1))
                        | _ -> None)
                | None -> parsePredicate s)
        | Some '!' -> (match parseUnary (String.sub s 1 (String.length s - 1)) with
                | Some (unary, s) -> Some (Negation unary, s)
                | None -> None)
        | Some '@' | Some '?' ->
                let construct var expr = if take s 0 = Some '@' then Forall (var, expr) else Exists (var, expr) in
                (match parseVar (String.sub s 1 (String.length s - 1)) with
                | Some (Var var, s) ->
                        let s = trim s in
                        (match take s 0 with
                        | Some '.' ->
                                (match parseUnary (String.sub s 1 (String.length s - 1)) with
                                | Some (impl, s) -> Some (construct var impl, s)
                                | None -> None)
                        | _ -> None)
                | _ -> None)

        | _ ->
                parsePredicate s
and parseVar s =
        let s = trim s in
        match take s 0 with
        | Some a ->
                (match a with
                | 'a'..'z' ->
                        let rec func have s =
                                match take s 0 with
                                | Some a ->
                                        (match a with
                                        | '0'..'9' ->
                                                func (have ^ (Char.escaped a)) (String.sub s 1 (String.length s - 1))
                                        | _ -> (have, s))
                                | None -> (have, s) in
                        let (name, s) = func (Char.escaped a) (String.sub s 1 (String.length s - 1)) in
                        Some (Var name, s)
                | _ -> None)
        | None -> None
and parsePredicate s =
        let s = trim s in
        match take s 0 with
        | Some a ->
                (match a with
                | 'A'..'Z' ->
                        let rec func have s =
                                match take s 0 with
                                | Some a ->
                                        (match a with
                                        | '0'..'9' -> func (have ^ Char.escaped a) (String.sub s 1 (String.length s - 1))
                                        | _ -> (have, s))
                                | None -> (have, s) in
                        let (name, s) = func (Char.escaped a) (String.sub s 1 (String.length s - 1)) in
                        (match take s 0 with
                        | Some '(' ->
                                let s = String.sub s 1 (String.length s - 1) in
                                (match parseTerm s with
                                | Some (term, s) ->
                                        let rec func s =
                                                let s = trim s in
                                                match take s 0 with
                                                | Some ',' ->
                                                        (match parseTerm (String.sub s 1 (String.length s - 1)) with
                                                        | Some (term, s) ->
                                                                (match func s with
                                                                | Some (terms, s) ->
                                                                        Some (term :: terms, s)
                                                                | None -> None)
                                                        | None -> None)
                                                | _ -> Some ([], s) in
                                        (match func s with
                                        | Some (terms, s) ->
                                                let s = trim s in
                                                (match take s 0 with
                                                | Some ')' ->
                                                        Some (Predicate (name, term :: terms), String.sub s 1 (String.length s - 1))
                                                | _ -> None)
                                        | None -> None)
                                | None -> None)
                        | _ -> None)
                | _ ->
                        (match parseTerm s with
                        | Some (term, s) ->
                                let s = trim s in
                                (match take s 0 with
                                | Some '=' ->
                                        (match parseTerm (String.sub s 1 (String.length s - 1)) with
                                        | Some (term1, s) ->
                                                Some (Equals (term, term1), s)
                                        | None -> None)
                                | _ -> None)
                        | None -> None))
        | None -> None
and parseTerm s =
        match parseSummand s with
        | Some (summand, s) ->
                let rec func have s =
                        let s = trim s in
                        match take s 0 with
                        | Some '+' ->
                                let s = String.sub s 1 (String.length s - 1) in
                                (match parseSummand s with
                                | Some (summand, s) ->
                                        func (Add (have, summand)) s
                                | None -> None)
                        | _ -> Some (have, s) in
                func summand s
        | None -> None
and parseSummand s =
        match parseInc s with
        | Some (mul, s) ->
                let rec func have s =
                        let s = trim s in
                        match take s 0 with
                        | Some '*' ->
                                let s = String.sub s 1 (String.length s - 1) in
                                (match parseInc s with
                                | Some (mul, s) ->
                                        func (Multiply (have, mul)) s
                                | None -> None)
                        | _ -> Some (have, s) in
                func mul s
        | None -> None
and parseInc s =
        match parseMultiplying s with
        | Some (now, s) ->
                let rec func have s =
                        let s = trim s in
                        match take s 0 with
                        | Some '\'' ->
                                func (Increment have) (String.sub s 1 (String.length s - 1))
                        | _ -> (have, s) in
                let (now, s) = func now s in
                Some (now, s)
        | None -> None
and parseMultiplying s =
        let s = trim s in
        match take s 0 with
        | Some a ->
                (match a with
                | '0' -> Some (Zero, String.sub s 1 (String.length s - 1))
                | '(' ->
                        let s = String.sub s 1 (String.length s - 1) in
                        (match parseTerm s with
                        | Some (term, s) ->
                                let s = trim s in
                                (match take s 0 with
                                | Some ')' ->
                                        Some (term, String.sub s 1 (String.length s - 1))
                                | _ -> None)
                        | None -> None)
                | _ ->
                        (match parseVar s with
                        | Some (Var name, s) ->
                                (match take s 0 with
                                | Some '(' ->
                                        let s = String.sub s 1 (String.length s - 1) in
                                        (match parseTerm s with
                                        | Some (term, s) ->
                                                let rec func s =
                                                        let s = trim s in
                                                        match take s 0 with
                                                        | Some ',' ->
                                                                (match parseTerm (String.sub s 1 (String.length s - 1)) with
                                                                | Some (term, s) ->
                                                                        (match func s with
                                                                        | Some (terms, s) ->
                                                                                Some (term :: terms, s)
                                                                        | None -> None)
                                                                | None -> None)
                                                        | _ -> Some ([], s) in
                                                (match func s with
                                                | Some (terms, s) ->
                                                        let s = trim s in
                                                        (match take s 0 with
                                                        | Some ')' ->
                                                                Some (Function (name, term :: terms), String.sub s 1 (String.length s - 1))
                                                        | _ -> None)
                                                | None -> None)
                                        | None -> None)
                                | _ -> Some (Var name, s))
                        | _ -> None))
        | None -> None;;

let parse s =
        match parseImplication s with
        | Some (expr, s) ->
                let s = trim s in
                if String.length s = 0 then Some expr else None
        | None -> None;;

let find_barrier s =
        let rec find_barrier_int s ind =
                match take s 0 with
                | Some '|' ->
                        (match take s 1 with
                        | Some '-' ->
                                Some ind
                        | _ ->
                                find_barrier_int (String.sub s 1 (String.length s - 1)) (ind + 1))
                | Some a ->
                        find_barrier_int (String.sub s 1 (String.length s - 1)) (ind + 1)
                | None -> None in
        find_barrier_int s 0;;

let parseDocument s =
        let rec func c s =
                match parseImplication s with
                | Some (impl, s) ->
                        let s = trim s in
                        if take s 0 = Some c then
                                (match func c (String.sub s 1 (String.length s - 1)) with
                                | Some (last, s) ->
                                        Some (impl :: last, s)
                                | None -> None)
                        else if take s 0 = None then
                                Some (impl :: [], s)
                        else None
                | None -> None in
        match find_barrier s with
        | Some ind ->
                let s1 = trim (String.sub s 0 ind) in
                let s = trim_end (trim (String.sub s (ind + 2) (String.length s - ind - 2))) in
                (match ((if String.length s1 = 0 then Some ([], "") else func ',' s1), func '\n' s) with
                | (Some (d1, _) , Some (d2 :: d3, _)) ->
                        Some (Document (d1, d2, d3))
                | _ -> None)
        | None -> None;;

let printDocument (Document (d1, d2, d3)) = (String.concat "," (List.map printExpr d1)) ^ "|-" ^ (printExpr d2) ^ "\n" ^ (String.concat "\n" (List.map printExpr d3));;

let parse_bad s =
        match parse s with
        | Some x -> x
        | None -> failwith "Bad expression"
and parseDocument_bad s =
        match parseDocument s with
        | Some x -> x
        | None -> failwith "Bad document";;

let rawSchemes =
        ["A(0) -> B(0) -> A(0)";
        "(A(0) -> B(0)) -> (A(0) -> B(0) -> C(0)) -> (A(0) -> C(0))";
        "A(0) -> B(0) -> A(0) & B(0)";
        "A(0) & B(0) -> A(0)";
        "A(0) & B(0) -> B(0)";
        "A(0) -> A(0) | B(0)";
        "B(0) -> A(0) | B(0)";
        "(A(0) -> C(0)) -> (B(0) -> C(0)) -> (A(0) | B(0) -> C(0))";
        "(A(0) -> B(0)) -> (A(0) -> !B(0)) -> !A(0)";
        "!!A(0) -> A(0)"];;

let schemes = List.map parse_bad rawSchemes;;

let rawAxioms =
        ["a = b -> a' = b'";
        "a = b -> a = c -> b = c";
        "a' = b' -> a = b";
        "!a' = 0";
        "a + b' = (a + b)'";
        "a + 0 = a";
        "a * 0 = 0";
        "a * b' = a * b + a"];;

let axioms = List.map parse_bad rawAxioms;;

module StringMap = Map.Make(String);;
module ExprMap = Map.Make(struct type t = expr let compare = compare end);;
module ExprSet = Set.Make(struct type t = expr let compare = compare end);;
module StringSet = Set.Make(String);;

let rec freeVars e =
        match e with
        | Implication (a, b) | Conjunction (a, b) | Disjunction (a, b) ->
                StringSet.union (freeVars a) (freeVars b)
        | Negation a ->
                freeVars a
        | Exists (name, a) | Forall (name, a) ->
                StringSet.remove name (freeVars a)
        | Predicate (_, l) ->
                List.fold_left (fun m a -> StringSet.union m (freeVarsTerm a)) StringSet.empty l
        | Equals (a, b) ->
                StringSet.union (freeVarsTerm a) (freeVarsTerm b)
and freeVarsTerm t =
        match t with
        | Add (a, b) | Multiply (a, b) ->
                StringSet.union (freeVarsTerm a) (freeVarsTerm b)
        | Var name ->
                StringSet.singleton name
        | Increment a ->
                freeVarsTerm a
        | Zero ->
                StringSet.empty
        | Function (_, l) ->
                List.fold_left (fun m a -> StringSet.union m (freeVarsTerm a)) StringSet.empty l;;

let upperPred e name =
        let rec upperPredExpr e name =
                match e with
                | Implication (a, b) | Conjunction (a, b) | Disjunction (a, b) ->
                        (match (upperPredExpr a name, upperPredExpr b name) with
                        | (None, None) -> None
                        | (a, b) -> Some (StringSet.union (takeOr a) (takeOr b)))
                | Negation a ->
                        upperPredExpr a name
                | Exists (var, a) | Forall (var, a) ->
                        (match upperPredExpr a name with
                        | None -> None
                        | Some b -> Some (StringSet.add var b))
                | Predicate (_, l) ->
                        List.fold_left (fun m a ->
                                match m with
                                | None -> upperPredTerm a name
                                | Some b ->
                                        Some (StringSet.union b (takeOr (upperPredTerm a name)))) None l
                | Equals (a, b) ->
                        (match (upperPredTerm a name, upperPredTerm b name) with
                        | (None, None) -> None
                        | (a, b) -> Some (StringSet.union (takeOr a) (takeOr b)))
        and upperPredTerm t name =
                match t with
                | Add (a, b) | Multiply (a, b) ->
                        (match (upperPredTerm a name, upperPredTerm b name) with
                        | (None, None) -> None
                        | (a, b) -> Some (StringSet.union (takeOr a) (takeOr b)))
                | Var var ->
                        if var = name then Some StringSet.empty else None
                | Increment a ->
                        upperPredTerm a name
                | Zero ->
                        None
                | Function (_, l) ->
                        List.fold_left (fun m a ->
                                match m with
                                | None -> upperPredTerm a name
                                | Some b ->
                                        Some (StringSet.union b (takeOr (upperPredTerm a name)))) None l

        and takeOr a =
                match a with
                | Some b -> b
                | None -> StringSet.empty in
        takeOr (upperPredExpr e name);;

let println_string s = print_string (s ^ "\n");;

let rec transformTerm e was became =
        let rec transform t =
                if t = was then became else
                        match t with
                        | Add (a, b) ->
                                Add (transform a, transform b)
                        | Multiply (a, b) ->
                                Multiply (transform a, transform b)
                        | Var name ->
                                Var name
                        | Increment a ->
                                Increment (transform a)
                        | Zero ->
                                Zero
                        | Function (name, l) ->
                                Function (name, List.map transform l) in
        let rec func e =
                match e with
                | Implication (a, b) ->
                        Implication (func a, func b)
                | Conjunction (a, b) ->
                        Conjunction (func a, func b)
                | Disjunction (a, b) ->
                        Disjunction (func a, func b)
                | Negation a ->
                        Negation (func a)
                | Forall (var, a) ->
                        Forall (var, func a)
                | Exists (var, a) ->
                        Exists (var, func a)
                | Predicate (name, l) ->
                        Predicate (name, List.map (fun e -> transform e) l)
                | Equals (a, b) ->
                        Equals (transform a, transform b) in
        func e
and transformExpr e was became =
        let rec func e =
                if e = was then became else
                        match e with
                        | Implication (a, b) ->
                                Implication (func a, func b)
                        | Conjunction (a, b) ->
                                Conjunction (func a, func b)
                        | Disjunction (a, b) ->
                                Disjunction (func a, func b)
                        | Negation a ->
                                Negation (func a)
                        | Forall (var, a) ->
                                Forall (var, func a)
                        | Exists (var, a) ->
                                Exists (var, func a)
                        | Predicate (name, l) ->
                                Predicate (name, l)
                        | Equals (a, b) ->
                                Equals (a, b) in
        func e;;

let rec findTerm e1 e2 need =
        let rec find t1 t2 =
                if t1 = need then Some t2 else
                        match (t1, t2) with
                        | (Add (a1, b1), Add (a2, b2)) | (Multiply (a1, b1), Multiply (a2, b2)) ->
                                let res = find a1 a2 in
                                if res = None then find b1 b2 else res
                        | (Increment a1, Increment a2) ->
                                find a1 a2
                        | (Function (name1, l1), Function (name2, l2)) ->
                                if name1 = name2 then
                                        if List.length l1 = List.length l2 then
                                                List.fold_left (fun a (b1, b2) ->
                                                        match a with
                                                        | Some c -> Some c
                                                        | None -> find b1 b2) None (List.combine l1 l2)
                                        else None
                                else None
                        | (_, _) -> None in
        let rec func e1 e2 =
                match (e1, e2) with
                | (Implication (a1, b1), Implication (a2, b2))
                | (Conjunction (a1, b1), Conjunction (a2, b2))
                | (Disjunction (a1, b1), Disjunction (a2, b2)) ->
                        let res = func a1 a2 in
                        if res = None then func b1 b2 else res
                | (Negation a1, Negation a2) ->
                        func a1 a2
                | (Forall (var1, a1), Forall (var2, a2))
                | (Exists (var1, a1), Exists (var2, a2)) ->
                        if var1 = var2 then func a1 a2 else None
                | (Predicate (name1, l1), Predicate (name2, l2)) ->
                        if name1 = name2 then
                                if List.length l1 = List.length l2 then
                                        List.fold_left (fun a (b1, b2) ->
                                                match a with
                                                | Some c -> Some c
                                                | None -> find b1 b2) None (List.combine l1 l2)
                                else None
                        else None
                | (Equals (a1, b1), Equals (a2, b2)) ->
                        let res = find a1 a2 in
                        if res = None then find b1 b2 else res
                | (_, _) -> None in
        func e1 e2
and findExpr e1 e2 need =
        let rec func e1 e2 =
                if e1 = need then Some e2 else
                        match (e1, e2) with
                        | (Implication (a1, b1), Implication (a2, b2))
                        | (Conjunction (a1, b1), Conjunction (a2, b2))
                        | (Disjunction (a1, b1), Disjunction (a2, b2)) ->
                                let res = func a1 a2 in
                                if res = None then func b1 b2 else res
                        | (Negation a1, Negation a2) ->
                                func a1 a2
                        | (Forall (var1, a1), Forall (var2, a2))
                        | (Exists (var1, a1), Exists (var2, a2)) ->
                                if var1 = var2 then func a1 a2 else None
                        | (_, _) -> None in
        func e1 e2;;

let is_scheme_axiom e ax =
        let func e was became =
                match became with
                | None -> e
                | Some became -> transformExpr e was became in
        let a = findExpr ax e (Predicate ("A", [Zero])) in
        let b = findExpr ax e (Predicate ("B", [Zero])) in
        let c = findExpr ax e (Predicate ("C", [Zero])) in
        let za = func ax (Predicate ("A", [Zero])) a in
        let zb = func za (Predicate ("B", [Zero])) b in
        let zc = func zb (Predicate ("C", [Zero])) c in
        zc = e;;

let enumerate l =
        let rec func l a =
                match l with
                | [] -> []
                | x :: xs -> (x, a) :: (func xs (a + 1)) in
        func l 0;;

let which_scheme_axiom e =
        let eschemes = enumerate schemes in
        let axs = List.map (fun (a, num) -> if is_scheme_axiom e a then Some num else None) eschemes in
        List.fold_left (fun was now ->
                match was with
                | None -> now
                | Some a -> Some a) None axs;;

let print_scheme_number e =
        match which_scheme_axiom e with
        | None -> -1
        | Some a -> a;;

let check11 e =
        match e with
        | Implication (Forall (var, c), b) ->
                (match findTerm c b (Var var) with
                | Some expr ->
                        if StringSet.is_empty (StringSet.inter (freeVarsTerm expr) (upperPred c var)) then
                                transformTerm c (Var var) expr = b
                        else false
                | None -> false)
        | _ -> false;;

let check12 e =
        match e with
        | Implication (b, Exists (var, c)) ->
                (match findTerm c b (Var var) with
                | Some expr ->
                        if StringSet.is_empty (StringSet.inter (freeVarsTerm expr) (upperPred c var)) then
                                transformTerm c (Var var) expr = b
                        else false
                | None -> false)
        | _ -> false;;

let checkInduction e =
        match e with
        | Implication (Conjunction (s, Forall (var, bb)), res) ->
                s = (transformTerm res (Var var) Zero) && bb = (Implication (res, transformTerm res (Var var) (Increment (Var var))))
        | _ -> false;;

let checkAllAxioms e =
        match which_scheme_axiom e with
        | Some a -> Some ("Scheme " ^ (string_of_int (a + 1)))
        | None ->
                if check11 e then Some "Scheme 11" else
                if check12 e then Some "Scheme 12" else
                if checkInduction e then Some "Induction" else
                let eaxioms = enumerate axioms in
                match List.find_opt (fun (now, _) -> now = e) eaxioms with
                | Some (_, num) -> Some ("Axiom " ^ (string_of_int (num + 1)))
                | None -> None;;

let printAllAxioms e =
        match checkAllAxioms e with
        | None -> "Nothing"
        | Some a -> a;;

let rec checkProof (Document (was, need, proof)) =
        let wasExprs = List.fold_left (fun set x -> ExprSet.add x set) ExprSet.empty was in
        let func was needLeft needRight e =
                if match checkAllAxioms e with
                | Some _ -> true
                | None ->
                        match e with
                        | Implication (a, Forall (x, b)) ->
                                if (List.exists (fun v -> v = x) (StringSet.elements (freeVars a)) = false) && (ExprSet.mem (Implication (a, b)) was) then true
                                else (ExprSet.mem e wasExprs) || (ExprSet.mem e needRight)
                        | Implication (Exists (x, b), a) ->
                                if (List.exists (fun v -> v = x) (StringSet.elements (freeVars a)) = false) && (ExprSet.mem (Implication (b, a)) was) then true
                                else (ExprSet.mem e wasExprs) || (ExprSet.mem e needRight)
                        | _ ->
                                (ExprSet.mem e wasExprs) || (ExprSet.mem e needRight) then
                        let was = ExprSet.add e was in
                        let (needLeft, needRight) =
                                match ExprMap.find_opt e needLeft with
                                | Some l ->
                                        (ExprMap.remove e needLeft, List.fold_left (fun need x -> ExprSet.add x need) needRight l)
                                | None ->
                                        (needLeft, needRight) in
                        let (needLeft, needRight) =
                                match e with
                                | Implication (a, b) ->
                                        if ExprSet.mem a was then (needLeft, ExprSet.add b needRight)
                                        else (ExprMap.add a (b :: (match ExprMap.find_opt a needLeft with
                                        | Some a -> a
                                        | None -> [])) needLeft, needRight)
                                | _ ->
                                        (needLeft, needRight) in
                        Some (was, needLeft, needRight)
                else None in
        let rec repeat eproof was needLeft needRight =
                match eproof with
                | (x, num) :: xs ->
                        (match func was needLeft needRight x with
                        | Some (was, needLeft, needRight) ->
                                repeat xs was needLeft needRight
                        | None -> Some num)
                | [] -> None in
        match repeat (enumerate proof) ExprSet.empty ExprMap.empty ExprSet.empty with
        | Some num -> "Line " ^ (string_of_int (num + 1)) ^ " can't be obtained"
        | None -> if List.exists (fun v -> v = need) proof then "Proof is correct" else "Required hasn't been proven";;

let rec readDocument () =
    try let x = input_line stdin in x :: readDocument () with _ -> [];;

let rec parseL l =
        match l with
        | x :: xs ->
                (match parse x with
                | Some _ -> parseL xs
                | None -> "Error on " ^ x)
        | [] -> "No errors";;

(*print_string (parseL (List.tl (readDocument ())));;*)

print_string (checkProof (parseDocument_bad (String.concat "\n" (readDocument ()))));;