Browse Source

first commit

memomess
zapashcanon 1 year ago
commit
120be7d7aa
Signed by: zapashcanon GPG Key ID: 8981C3C62D1D28F1
28 changed files with 1600 additions and 0 deletions
  1. +2
    -0
      .gitignore
  2. +14
    -0
      CHANGELOG.md
  3. +8
    -0
      LICENSE.md
  4. +57
    -0
      README.md
  5. +3
    -0
      dune-project
  6. +9
    -0
      scripts/bench.sh
  7. +7
    -0
      scripts/build.sh
  8. +7
    -0
      scripts/clean.sh
  9. +8
    -0
      scripts/install.sh
  10. +8
    -0
      scripts/test.sh
  11. +6
    -0
      scripts/todo.sh
  12. +46
    -0
      src/bdd.ml
  13. +91
    -0
      src/bdd_hashcons.ml
  14. +38
    -0
      src/bdd_hashcons_common.ml
  15. +106
    -0
      src/bdd_hashcons_memo.ml
  16. +90
    -0
      src/bdd_naive.ml
  17. +53
    -0
      src/bench.ml
  18. +21
    -0
      src/dune
  19. +11
    -0
      src/expr.ml
  20. +67
    -0
      src/expr_lexer.mll
  21. +38
    -0
      src/expr_parser.mly
  22. +26
    -0
      src/expr_utils.ml
  23. +51
    -0
      src/hashcons.ml
  24. +35
    -0
      src/memo.ml
  25. +92
    -0
      src/test.ml
  26. +3
    -0
      src/utils.ml
  27. +667
    -0
      tests/test.txt
  28. +36
    -0
      tests/test2.txt

+ 2
- 0
.gitignore View File

@ -0,0 +1,2 @@
_build/
*.merlin

+ 14
- 0
CHANGELOG.md View File

@ -0,0 +1,14 @@
# Change Log
All notable changes to this project will be documented in this file.
The format is based on [Keep a Changelog](http://keepachangelog.com/).
## [Unreleased]
### Added
- initial release
[Unreleased]: https://git.zapashcanon.fr/zapashcanon/bdd/src/branch/master

+ 8
- 0
LICENSE.md View File

@ -0,0 +1,8 @@
The ISC License (ISC)
=====================
Copyright © 2019, Léo Andrès and Jean-Christophe Filliâtre
Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above copyright notice and this permission notice appear in all copies.
THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.

+ 57
- 0
README.md View File

@ -0,0 +1,57 @@
# Binary Decision Diagram library in OCaml
This library provides many implementations of BDD with the same interface. We provide the same set of tests and benchmarks for all of them.
- `src/bdd_naive.ml`: naïve implementation
- `src/bdd_hashcons.ml`: hash-consing implementation
- `src/bdd_hashcons_memo.ml`: hash-consing plus memoïzation implementation
They all have the same functorial interface, that you can find in `src/bdd.ml`.
We have our own implementation of boolean expression:
- `src/expr_lexer.mll`: the lexer
- `src/expr_parser.mly`: the parser
- `src/expr.ml`: the abstract syntax
- `src/expr_utils.ml`: high-level functions to get an AST from a file or a string containing an expression written in the concrete syntax
Here's what an expression in the concrete-syntax looks like: `((0 || 1) && z => 1) <=> !(x && y || z)`.
## Build
You need to have `dune` on your system. Then:
```sh
scripts/build.sh
```
## Test
```sh
scripts/test.sh
```
## Bench
An expression written in the concrete syntax - don't forget to put double quotes around it:
```sh
scripts/bench.sh -e <expression>
```
A file containing an expression:
```sh
scripts/bench.sh -f <file>
```
## Change Log
See [CHANGELOG].
## License
See [LICENSE].
[CHANGELOG]: ./CHANGELOG.md
[LICENSE]: ./LICENSE.md

+ 3
- 0
dune-project View File

@ -0,0 +1,3 @@
(lang dune 1.6)
(name bdd)
(using menhir 2.0)

+ 9
- 0
scripts/bench.sh View File

@ -0,0 +1,9 @@
#!/bin/sh
set -eu
( cd "$(dirname "$0")/../"
eval "$(opam env)"
dune exec src/bench.exe -- "$@"
)

+ 7
- 0
scripts/build.sh View File

@ -0,0 +1,7 @@
#!/bin/sh
set -eu
( cd "$(dirname "$0")/../"
eval "$(opam env)"
dune build @all )

+ 7
- 0
scripts/clean.sh View File

@ -0,0 +1,7 @@
#!/bin/sh
set -eu
( cd "$(dirname "$0")/../"
eval "$(opam env)"
dune clean )

+ 8
- 0
scripts/install.sh View File

@ -0,0 +1,8 @@
#!/bin/sh
set -eu
( cd "$(dirname "$0")/../"
eval "$(opam env)"
dune build @install
dune install bdd )

+ 8
- 0
scripts/test.sh View File

@ -0,0 +1,8 @@
#!/bin/sh
set -eu
( cd "$(dirname "$0")/../"
eval "$(opam env)"
dune exec src/test.exe )

+ 6
- 0
scripts/todo.sh View File

@ -0,0 +1,6 @@
#!/bin/sh
set -eu
( cd "$(dirname "$0")/../"
( find . -type f -print0 | xargs -0 cat) | grep -r TODO )

+ 46
- 0
src/bdd.ml View File

@ -0,0 +1,46 @@
module type S = sig
type expr
type var
type t
val var_bdd: var -> t
val true_bdd: t
val false_bdd: t
val ite: t -> t -> t -> t
val conj: t -> t -> t
val disj: t -> t -> t
val neg: t -> t
val imp: t -> t -> t
val eq: t -> t -> t
val of_expr: expr -> t
val to_expr: t -> expr
val to_string: t -> string
val compute: (var, bool) Hashtbl.t -> t -> t
val of_string: string -> t
val var_of_string: string -> var
end
(* TODO: currently this is useless, but may be useful later *)
module Make (M : S) : (S with type var = M.var and type expr = M.expr) = struct
type t = M.t
type var = M.var
type expr = M.expr
let var_bdd = M.var_bdd
let true_bdd = M.true_bdd
let false_bdd = M.false_bdd
let ite = M.ite
let conj = M.conj
let disj = M.disj
let neg = M.neg
let imp = M.imp
let eq = M.eq
let of_expr = M.of_expr
let to_expr = M.to_expr
let to_string = M.to_string
let compute = M.compute
let of_string = M.of_string
let var_of_string = M.var_of_string
end

+ 91
- 0
src/bdd_hashcons.ml View File

@ -0,0 +1,91 @@
module C = Bdd_hashcons_common
type t = C.t
type expr = C.expr
type var = C.var
let ite = C.ite
let false_bdd = C.false_bdd
let true_bdd = C.true_bdd
let var_bdd = C.var_bdd
open Bdd_hashcons_common
open Hashcons
let rec to_string x = match x.node with
| True -> "true"
| False -> "false"
| Node (v, l, h) ->
v ^ " ? "
^ "(" ^ (to_string l) ^ ")"
^ ": (" ^ (to_string h) ^ ")"
let rec neg x = match x.node with
| True -> false_bdd
| False -> true_bdd
| Node (v, l, h) -> node v (neg l) (neg h)
let comb n1 n2 op = match n1.node, n2.node with
| Node (v1, l1, h1), Node (v2, l2, h2) ->
node v1
(node v2 (op l1 l2) (op l1 h2))
(node v2 (op h1 l2) (op h1 h2))
| _ -> failwith "hashcons blah"
let rec conj n1 n2 = match n1.node, n2.node with
| True, True -> true_bdd
| False, _ | _, False -> false_bdd
| True, _ -> n2
| _, True -> n1
| _ -> comb n1 n2 conj
let rec disj n1 n2 = match n1.node, n2.node with
| True, _ | _, True -> true_bdd
| False, False -> false_bdd
| False, _ -> n2
| _, False -> n1
| _ -> comb n1 n2 disj
let rec imp n1 n2 = match n1.node, n2.node with
| False, _ | True, True -> true_bdd
| True, False -> false_bdd
| True, _ -> n2
| _ -> comb n1 n2 imp
let rec eq n1 n2 = match n1.node, n2.node with
| False, False | True, True -> true_bdd
| True, False | False, True -> false_bdd
| _, _ -> comb n1 n2 eq
let rec of_expr = function
| Expr.True -> true_bdd
| Expr.False -> false_bdd
| Expr.Var v -> var_bdd v
| Expr.Neg e -> neg (of_expr e)
| Expr.And (e1, e2) -> conj (of_expr e1) (of_expr e2)
| Expr.Or (e1, e2) -> disj (of_expr e1) (of_expr e2)
| Expr.Imp (e1, e2) -> imp (of_expr e1) (of_expr e2)
| Expr.Eq (e1, e2) -> eq (of_expr e1) (of_expr e2)
let compute tbl =
let rec compute_aux n = match n.node with
| False -> false_bdd
| True -> true_bdd
| Node (v, l, h) -> ( match Hashtbl.find tbl v with
| exception Not_found ->
failwith ("truth value of " ^ v ^ " is missing")
| true -> compute_aux l
| false -> compute_aux h )
in compute_aux
let rec to_expr n = match n.node with
| False -> Expr.False
| True -> Expr.True
| Node (v, l, h) ->
Expr.Or (
Expr.And (Expr.Var v, (to_expr l)),
Expr.And (Expr.Neg (Expr.Var v), (to_expr h)))
let of_string s = of_expr (Expr_utils.from_string s)
let var_of_string s = s

+ 38
- 0
src/bdd_hashcons_common.ml View File

@ -0,0 +1,38 @@
type var = string
type expr = Expr.t
type t = bdd Hashcons.hash_consed
and bdd =
| True
| False
| Node of var * t * t (* x ? true : false *)
module Bdd_node = struct
type t = bdd
let equal x y = match x, y with
| True, True -> true
| False, False -> true
| Node (v1, l1, r1), Node (v2, l2, r2) ->
v1 == v2 && l1 == l2 && r1 == r2
| _ -> false
let hash = function
| True -> 1
| False -> 0
| Node (_, l, r) ->
(* TODO: add v here *)
(19 * l.hkey + r.hkey)
end
module Hbdd = Hashcons.Make(Bdd_node)
let node, false_bdd, true_bdd, var_bdd(*, ite*) =
let hc = Hbdd.hashcons (Hbdd.create 256) in
let true_bdd = hc True in
let false_bdd = hc False in
(fun v l h -> if l == h then l else hc (Node (v, l, h))),
(false_bdd),
(true_bdd),
(fun v -> hc (Node (v, true_bdd, false_bdd)))(*,
(fun _if _then _else -> false_bdd) TODO *)
let ite _ _ _ = false_bdd (* TODO *)

+ 106
- 0
src/bdd_hashcons_memo.ml View File

@ -0,0 +1,106 @@
module C = Bdd_hashcons_common
type t = C.t
type expr = C.expr
type var = C.var
let ite = C.ite
let false_bdd = C.false_bdd
let true_bdd = C.true_bdd
let var_bdd = C.var_bdd
open Bdd_hashcons_common
open Hashcons
let to_string = Hbdd.memo (fun to_string x ->
match x.node with
| True -> "true"
| False -> "false"
| Node (v, l, h) ->
v ^ " ? "
^ "(" ^ (to_string l) ^ ")"
^ ": (" ^ (to_string h) ^ ")")
let neg = Hbdd.memo (fun neg x ->
match x.node with
| True -> false_bdd
| False -> true_bdd
| Node (v, l, h) -> node v (neg l) (neg h))
let comb op = Hbdd.memo2 (fun _ n1 n2 ->
match n1.node, n2.node with
| Node (v1, l1, h1), Node (v2, l2, h2) ->
node v1
(node v2 (op l1 l2) (op l1 h2))
(node v2 (op h1 l2) (op h1 h2))
| _ -> failwith "hashcons-memo blah")
let conj = Hbdd.memo2 (fun conj n1 n2 ->
match n1.node, n2.node with
| True, True -> true_bdd
| False, _ | _, False -> false_bdd
| True, _ -> n2
| _, True -> n1
| _ -> (comb conj) n1 n2)
let disj = Hbdd.memo2 (fun disj n1 n2 ->
match n1.node, n2.node with
| True, _ | _, True -> true_bdd
| False, False -> false_bdd
| False, _ -> n2
| _, False -> n1
| _ -> (comb disj) n1 n2)
let imp = Hbdd.memo2 (fun imp n1 n2 ->
match n1.node, n2.node with
| False, _ | True, True -> true_bdd
| True, False -> false_bdd
| True, _ -> n2
| _ -> (comb imp) n1 n2)
let eq = Hbdd.memo2 (fun eq n1 n2 ->
match n1.node, n2.node with
| False, False | True, True -> true_bdd
| True, False | False, True -> false_bdd
| _, _ -> (comb eq) n1 n2)
module MemoExpr = Memo.Make(struct
type t = Expr.t
let equal = (=)
let hash b = Hashtbl.hash b
end)
let of_expr = MemoExpr.memo (fun of_expr -> function
| Expr.True -> true_bdd
| Expr.False -> false_bdd
| Expr.Var v -> var_bdd v
| Expr.Neg e -> neg (of_expr e)
| Expr.And (e1, e2) -> conj (of_expr e1) (of_expr e2)
| Expr.Or (e1, e2) -> disj (of_expr e1) (of_expr e2)
| Expr.Imp (e1, e2) -> imp (of_expr e1) (of_expr e2)
| Expr.Eq (e1, e2) -> eq (of_expr e1) (of_expr e2))
let compute tbl =
let compute_aux = Hbdd.memo (fun compute_aux n ->
match n.node with
| False -> false_bdd
| True -> true_bdd
| Node (v, l, h) -> ( match Hashtbl.find tbl v with
| exception Not_found ->
failwith ("truth value of " ^ v ^ " is missing")
| true -> compute_aux l
| false -> compute_aux h ))
in compute_aux
let to_expr = Hbdd.memo (fun to_expr n ->
match n.node with
| False -> Expr.False
| True -> Expr.True
| Node (v, l, h) ->
Expr.Or (
Expr.And (Expr.Var v, (to_expr l)),
Expr.And (Expr.Neg (Expr.Var v), (to_expr h))))
let of_string s = of_expr (Expr_utils.from_string s)
let var_of_string s = s

+ 90
- 0
src/bdd_naive.ml View File

@ -0,0 +1,90 @@
type var = string
type expr = Expr.t
type t =
| True
| False
| Node of var * t * t (* x ? true : false *)
let var_bdd x = Node (x, True, False)
let true_bdd = True
let false_bdd = False
let rec to_string = function
| True -> "true"
| False -> "false"
| Node (var, low, high) ->
var ^ " ? "
^ "(" ^ (to_string low) ^ ")"
^ ": (" ^ (to_string high) ^ ")"
let ite _ _ _ = False (* TODO *)
let rec neg = function
| True -> False
| False -> True
| Node (var, low, high) -> Node (var, neg low, neg high)
let comb n1 n2 op = match n1, n2 with
| Node (v1, l1, h1), Node (v2, l2, h2) ->
Node (v1,
Node (v2, op l1 l2, op l1 h2),
Node (v2, op h1 l2, op h1 h2))
| _ -> failwith "naive blah"
(*
| Node (v, l, h), _ -> Node (v, op l n2, op h n2)
| _, Node (v, l, h) -> Node (v, op n1 l, op n1 h)
| _, _ -> op n1 n2*)
let rec conj n1 n2 = match n1, n2 with
| True, True -> True
| False, _ | _, False -> False
| True, x | x, True -> x
| _ -> comb n1 n2 conj
let rec disj n1 n2 = match n1, n2 with
| True, _ | _, True -> True
| False, False -> False
| False, x | x, False -> x
| _ -> comb n1 n2 disj
let rec imp n1 n2 = match n1, n2 with
| False, _ | True, True -> True
| True, False -> False
| True, _ -> n2
| _ -> comb n1 n2 imp
let rec eq n1 n2 = match n1, n2 with
| False, False | True, True -> True
| True, False | False, True -> False
| n1, n2 -> comb n1 n2 eq
let rec of_expr = function
| Expr.True -> True
| Expr.False -> False
| Expr.Var v -> Node (v, True, False)
| Expr.Neg e -> neg (of_expr e)
| Expr.And (e1, e2) -> conj (of_expr e1) (of_expr e2)
| Expr.Or (e1, e2) -> disj (of_expr e1) (of_expr e2)
| Expr.Imp (e1, e2) -> imp (of_expr e1) (of_expr e2)
| Expr.Eq (e1, e2) -> eq (of_expr e1) (of_expr e2)
let compute tbl =
let rec compute_aux = function
| False -> False
| True -> True
| Node (v, l, h) -> ( match Hashtbl.find tbl v with
| exception Not_found ->
failwith ("truth value of " ^ v ^ " is missing")
| true -> compute_aux l
| false -> compute_aux h
)
in compute_aux
let to_expr = function
| False -> Expr.False
| _ -> failwith "TODO"
let of_string s = of_expr (Expr_utils.from_string s)
let var_of_string s = s

+ 53
- 0
src/bench.ml View File

@ -0,0 +1,53 @@
module Make (M: Bdd.S) = struct
module M = Bdd.Make(M)
let bench_one tbl expr =
let start = Unix.gettimeofday () in
let bdd = M.of_expr expr in
ignore (M.compute tbl bdd);
let stop = Unix.gettimeofday () in
stop -. start
let bench_n n tbl expr =
let sum = ref 0. in
for _ = 0 to n do
sum := !sum +. (bench_one tbl expr)
done;
!sum
let bench_n_print n s tbl expr =
Printf.printf "bench %s %.2f\n" s (bench_n n tbl expr)
end
let _ =
let f = ref None in
let e = ref None in
Arg.parse [
("-f", Arg.String (fun s -> f := Some s), "file");
("-e", Arg.String (fun s -> e := Some s), "expression");
] (fun _ -> ()) "Bdd test";
let expr = match !e, !f with
| Some _, Some _ -> raise (Arg.Bad "file or expression, not both...")
| Some e, _ -> Expr_utils.from_string e
| _, Some f -> Expr_utils.from_file f
| None, None -> raise (Arg.Bad "file or expression needed")
in
let tbl = Hashtbl.create 512 in
Hashtbl.add tbl "x" false;
Hashtbl.add tbl "y" true;
let n = 5 in
let module B1 = Make(Bdd_naive) in
let module B2 = Make(Bdd_hashcons) in
let module B3 = Make(Bdd_hashcons_memo) in
B3.bench_n_print n "hashcons + memo:" tbl expr;
B2.bench_n_print n "hashcons: " tbl expr;
B1.bench_n_print n "naïve: " tbl expr;

+ 21
- 0
src/dune View File

@ -0,0 +1,21 @@
(executable
(name bench)
(libraries unix bdd)
(modules bench))
(executable
(name test)
(modules test)
(libraries bdd))
(library
(name bdd)
(modules bdd bdd_naive bdd_hashcons_common bdd_hashcons bdd_hashcons_memo expr expr_utils expr_parser expr_lexer hashcons utils memo)
(wrapped false))
(ocamllex
(modules expr_lexer))
(menhir
(modules expr_parser)
(flags ("--explain" "--dump")))

+ 11
- 0
src/expr.ml View File

@ -0,0 +1,11 @@
type var = string
type t =
| True
| False
| Var of var
| Neg of t
| And of t * t
| Or of t * t
| Imp of t * t
| Eq of t * t

+ 67
- 0
src/expr_lexer.mll View File

@ -0,0 +1,67 @@
{
open Expr_parser
exception Error of string
let current_line = ref 1
let current_offset = ref 1
let total_offset = ref 1
let mem_new_line = ref []
(* TODO: add something that remembers at which offset each new_line_met () occured, so we will be able to find the line of a syntax error (and typecheck error) without having to change a lot our AST *)
let get_mem_new_line () = List.rev (!mem_new_line)
let new_line_met () =
total_offset := !total_offset + 1;
mem_new_line := (!total_offset)::(!mem_new_line);
current_line := !current_line + 1;
current_offset := 0
let incr_offset x =
total_offset := !total_offset + x;
current_offset := !current_offset + x
}
let alpha = ['a'-'z' 'A'-'Z']
let newline = ['\n' '\r']
let blank = [' ' '\t']
let digit = ['0'-'9']
let int = digit+
let ident = alpha (alpha|digit|'_')*
rule token = parse
| newline { new_line_met (); token lexbuf }
| blank { incr_offset 1; token lexbuf }
| "/*" { comment lexbuf; token lexbuf }
| '0' { incr_offset 1; FALSE }
| '1' { incr_offset 1; TRUE }
| '(' { incr_offset 1; LPAR }
| ')' { incr_offset 1; RPAR }
| '!' { incr_offset 1; NOT }
| "&&" { incr_offset 2; AND }
| "||" { incr_offset 2; OR }
| "=>" { incr_offset 2; IMP }
| "<=>" { incr_offset 3; EQ }
| ident as i {
incr_offset (String.length i);
VAR i
}
| eof { EOF }
| _ { raise (Error (Printf.sprintf "Line %d, at offset %d: unexpected character." (!current_line) (!current_offset))) }
and comment = parse
| "*/" { incr_offset 2; () }
| newline { new_line_met (); comment lexbuf }
| _ { incr_offset 1; comment lexbuf }
| eof { failwith ("Unterminated comment at line " ^ (string_of_int (!current_line)) ^ " at offset " ^ (string_of_int (!current_offset)) ^ ".") }

+ 38
- 0
src/expr_parser.mly View File

@ -0,0 +1,38 @@
%{
open Expr
%}
%token EOF
%token TRUE FALSE
%token <string> VAR
%token NOT
%token AND OR
%token IMP EQ
%token LPAR RPAR
%left EQ
%left IMP
%left OR
%left AND
%left NOT
%start <Expr.t> expr_final
%%
expr_final:
| e = expr EOF { e }
expr:
| e = par(expr) { e }
| TRUE { True }
| FALSE { False }
| id = VAR { Var id }
| NOT e = expr { Neg e }
| e1 = expr AND e2 = expr { And (e1, e2) }
| e1 = expr OR e2 = expr { Or (e1, e2) }
| e1 = expr IMP e2 = expr { Imp (e1, e2) }
| e1 = expr EQ e2 = expr { Eq (e1, e2) }
par(X):
| x = delimited(LPAR, X, RPAR) { x }

+ 26
- 0
src/expr_utils.ml View File

@ -0,0 +1,26 @@
exception Stop
let from_lexing buf =
match Expr_parser.expr_final Expr_lexer.token buf with
| exception Expr_lexer.Error msg -> failwith ("lexer: " ^ msg)
| exception _ ->
let err_pos = Lexing.lexeme_start buf in
let err_line, line_offset = ref 1, ref 0 in
( try List.iter (fun x -> if x > err_pos then raise Stop; incr err_line; line_offset := x) (Expr_lexer.get_mem_new_line ())
with | Stop -> ());
failwith (Printf.sprintf "parser: On line %d, at offset %d, syntax error." (!err_line) (err_pos - !line_offset))
| res -> res
let from_file f =
let chan = open_in f in
let buf = Lexing.from_channel chan in
let res = from_lexing buf in
close_in chan;
res
let from_string s =
let buf = Lexing.from_string s in
from_lexing buf

+ 51
- 0
src/hashcons.ml View File

@ -0,0 +1,51 @@
type 'a hash_consed = {
node: 'a;
tag: int;
hkey: int;
}
module type S = sig
type key
type t
val create: int -> t
val clear: t -> unit
val hashcons: t -> key -> key hash_consed
val memo: ((key hash_consed -> 'a) -> key hash_consed -> 'a) -> key hash_consed -> 'a
val memo2: ((key hash_consed -> key hash_consed -> 'a) -> key hash_consed -> key hash_consed -> 'a) -> key hash_consed -> key hash_consed -> 'a
end
module Make(H : Hashtbl.HashedType) : (S with type key = H.t) = struct
type key = H.t
type data = key hash_consed
module E = Ephemeron.K1.Make(struct
type t = data
let equal = (=)
let hash = Hashtbl.hash
end)
type t = data E.t
let create = E.create
let clear = E.clear
let hashcons t d =
let hkey = H.hash d in
let hnode = {
hkey = hkey;
tag = Utils.gen_tag ();
node = d
} in
E.add t hnode hnode;
hnode
module M = Memo.Make(struct
type t = H.t hash_consed
let equal = (==)
let hash b = b.tag
end)
let memo = M.memo
let memo2 = M.memo2
end

+ 35
- 0
src/memo.ml View File

@ -0,0 +1,35 @@
module type S = sig
type t
val memo: ((t -> 'a) -> t -> 'a) -> t -> 'a
val memo2: ((t -> t -> 'a) -> t -> t -> 'a) -> t -> t -> 'a
end
module Make (H: Hashtbl.HashedType): (S with type t = H.t) = struct
type t = H.t
module Hash = Hashtbl.Make(H)
let memo ff =
let tbl = Hash.create 512 in
let rec f k = match Hash.find tbl k with
| exception Not_found ->
let v = ff f k in
Hash.add tbl k v;
v
| v -> v
in
f
module Hash2 = Hashtbl.Make(struct
type t = H.t * H.t
let equal (x1, y1) (x2, y2) = H.equal x1 x2 && H.equal y1 y2
let hash (x, y) = 19 * (H.hash x) + (H.hash y)
end)
let memo2 ff =
let tbl = Hash2.create 512 in
let rec f k1 k2 = match Hash2.find tbl (k1, k2) with
| exception Not_found ->
let v = ff f k1 k2 in
Hash2.add tbl (k1, k2) v;
v
| v -> v
in
f
end

+ 92
- 0
src/test.ml View File

@ -0,0 +1,92 @@
module Make (M: Bdd.S) = struct
module M = Bdd.Make(M)
let test () =
let tbl = Hashtbl.create 32 in
Hashtbl.add tbl (M.var_of_string "t") true;
Hashtbl.add tbl (M.var_of_string "f") false;
let compute x = M.compute tbl (M.of_string x) in
let check =
let count = ref 0 in
fun expected res ->
incr count;
if (M.to_string res) <> expected then
failwith ("got: " ^ (M.to_string res) ^
", expected: " ^ expected)
else Printf.printf "test %d OK\n" (!count)
in
let check_true x = check "true" (compute x) in
let check_false x = check "false" (compute x) in
let f = [
"0";
"!1";
"0 && 0";
"0 && 1";
"1 && 0";
"0 || 0";
"f";
"f && f";
"f && t";
"f || f";
"1 => 0";
"t => f";
" 0 <=> 1";
" 1 <=> 0";
" f <=> t";
" t <=> f";
] in
let t = [
"1";
"!0";
"1 && 1";
"1 || 0";
"0 || 1";
"1 || 1";
"t";
"t && t";
"t || f";
"f || t";
"t || t";
"0 => 1";
"0 => 1";
"1 => 1";
"f => f";
"f => t";
"t => t";
"0 <=> 0";
"1 <=> 1";
"f <=> f";
"t <=> t";
] in
List.iter check_false f;
List.iter check_true t;
List.iter (fun el -> check_true ("!(" ^ el ^ ")")) f;
List.iter (fun el -> check_false ("!(" ^ el ^ ")")) t;
List.iter (fun el -> check_false ("!!(" ^ el ^ ")")) f;
List.iter (fun el -> check_true ("!!(" ^ el ^ ")")) t;
List.iter (fun f ->
List.iter (fun t ->
check_true ("(" ^ f ^ ") || (" ^ t ^ ")");
check_false ("(" ^ f ^ ") && (" ^ t ^ ")");
) t
) f;
()
end
let _ =
let module T1 = Make(Bdd_naive) in
let module T2 = Make(Bdd_hashcons) in
let module T3 = Make(Bdd_hashcons_memo) in
T1.test ();
T2.test ();
T3.test ()

+ 3
- 0
src/utils.ml View File

@ -0,0 +1,3 @@
let gen_tag =
let count = ref (-1) in
fun () -> (incr count; !count)

+ 667
- 0
tests/test.txt View File

@ -0,0 +1,667 @@
(0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))
&& (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1
&& (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x
&& y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y))) && (0 || (x && y) || (1 && (x || y)))