type tree = Conj of tree * tree | Disj of tree * tree | Neg of tree | Var of int;;
type oper = And | Or

let inp = open_in "formula.in";;
let s = Scanf.fscanf inp "%[^\n]" (fun s -> s^";");;
close_in inp;;

let n = ref 0;;
let next () = n := !n + 1;;
let rec curr () = if s.[!n] = ' ' then (next(); curr()) else s.[!n];;
let eat c = if curr() <> c then failwith ((String.make 1 c) ^ " expected"); next();;

let rec parse_disj () = 
  let a = parse_conj () in
  if curr() = '|' then (next(); Disj (a, parse_disj())) else a

and parse_conj () =
  let a = parse_neg () in
  if curr() = '&' then (next(); Conj (a, parse_conj())) else a

and parse_neg () =
  if curr() = '~' then (next(); Neg (parse_neg())) else parse_expr()

and parse_expr () =
  match curr() with
    '('           -> next(); let r = parse_disj () in eat (')'); r
  | 'a'..'k' as c -> next(); Var (int_of_char c - int_of_char 'a')
  | _ -> failwith "parse?";;

let compute tree vars =
  let rec c' tree = 
    match tree with
      Conj (a,b) -> (c' a) && (c' b)
    | Disj (a,b) -> (c' a) || (c' b)
    | Neg a      -> not (c' a)
    | Var n      -> (vars land (1 lsl n)) <> 0
  in c' tree;;

let formula = parse_disj ();; eat ';';;
let table = Array.init 2048 (compute formula);;

let rec gen lst a = 
  match lst with [] -> [a]
  | l1::ls -> gen ls a @ gen ls (l1 lor a);;

let unique_map f = List.fold_left (fun res n -> 
    let (lst,plus) = f n in
    if List.mem_assoc lst res then res else (lst,plus)::res
  ) [];;

let check_subset table a_index b_index plus = 
  let la = gen a_index plus in
  let lb = gen b_index plus in
  match unique_map (fun a -> List.map (fun v -> (table.(a lor v), v)) lb, a) la with
    [x;y] -> 
      let ((minl,minplus),(maxl,maxplus)) = if x < y then (x,y) else (y,x) in
      if not (List.mem_assoc true minl) then Some (And,maxplus,List.assoc true maxl)
      else if not (List.mem_assoc false maxl) then Some (Or,minplus,List.assoc false minl)
      else None
  | [x] -> failwith ("All vars should be used: "^string_of_int plus)
  | _ -> None;;

exception Found;;
let used table v =
  try 
    Array.iteri (fun i a -> 
      if a <> table.(i lxor v) then raise Found) table;
    false
  with Found -> true;;

let rec log2 n = if n > 1 then 1 + log2 (n/2) else 0;;

let rec sfilter i v =
  match v with
    [] -> []
  | l1::ls -> if ((1 lsl (List.length ls)) land i) <> 0 then l1::(sfilter i ls)
    else sfilter i ls;;

exception SFound of string;;
let rec build table v plus =
  match v with
    [] ->  None
  | [l] -> Some ((if (table.(l lor plus)) then "" else "~") ^
                 (String.make 1 "abcdefghijk".[log2 l]))
  | v ->   
      try  
        for i = 1 to (1 lsl List.length v) - 2 do
          let a = sfilter i v in
          let b = sfilter (lnot i) v in
          match check_subset table a b plus with
            None -> ()
          | Some (r, plusa, plusb) ->
            (match (build table a plusb, build table b plusa) with
              (Some ea, Some eb) -> raise (SFound (
                 "(" ^ ea ^ (match r with And -> "&" | Or -> "|") ^ eb ^ ")"))
            | _ -> ())
        done;
        None
      with SFound s -> Some s;;

let v = List.filter (used table) [1;2;4;8;16;32;64;128;256;512;1024] in 
let out = open_out "formula.out" in
match build table v 0 with
  Some s -> Printf.fprintf out "Yes\n%s\n" s
| None -> Printf.fprintf out "No\n";
close_out out;;
