(* Entry point for this web application *)

(* open Chadprover.Types *)
open Chadprover.To_string
(* open Chadprover.Lib_utils *)
open Chadprover.Lexing.Lexer
open Chadprover.Parsing.Parser
(* open Chadprover.Satisfiability.Satisfiable *)

let () =
  let lex_result = lex "(p > (q > (p > p)))" in (* "a & b & c = z > x & y | c" *)
  let parse_result = parse lex_result in
  let proof = Chadprover.Sequent_calculus.Sequent_proof.prove_sequent (Seq([], [parse_result])) in
  print string_of_stree proof

let () = Api.Startapp.startapp ()