-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathformulae_exp_unsat.txt
39 lines (20 loc) · 76.1 KB
/
formulae_exp_unsat.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
~p0 & [a0*](<a0>True & (~p0 & [a0]p0 | p0 & [a0]~p0) & ~p0)
~p0 & ~p1 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) | p0 & [a0]~p0 & ~p1 & [a0]p1 | p0 & [a0]~p0 & p1 & [a0]~p1) & (~p0 | ~p1))
~p0 & ~p1 & ~p2 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2) & (~p0 | ~p1 | ~p2))
~p0 & ~p1 & ~p2 & ~p3 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3) & (~p0 | ~p1 | ~p2 | ~p3))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & ~p10 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 & (~p10 | [a0]p10) & (p10 | [a0]~p10) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & ~p10 & [a0]p10 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9 | ~p10))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & ~p10 & ~p11 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & ~p10 & [a0]p10 & (~p11 | [a0]p11) & (p11 | [a0]~p11) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & ~p11 & [a0]p11 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9 | ~p10 | ~p11))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & ~p10 & ~p11 & ~p12 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & ~p10 & [a0]p10 & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & ~p11 & [a0]p11 & (~p12 | [a0]p12) & (p12 | [a0]~p12) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & ~p12 & [a0]p12 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9 | ~p10 | ~p11 | ~p12))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & ~p10 & ~p11 & ~p12 & ~p13 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & ~p10 & [a0]p10 & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & ~p11 & [a0]p11 & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & ~p12 & [a0]p12 & (~p13 | [a0]p13) & (p13 | [a0]~p13) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & ~p13 & [a0]p13 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9 | ~p10 | ~p11 | ~p12 | ~p13))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & ~p10 & ~p11 & ~p12 & ~p13 & ~p14 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & ~p10 & [a0]p10 & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & ~p11 & [a0]p11 & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & ~p12 & [a0]p12 & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & ~p13 & [a0]p13 & (~p14 | [a0]p14) & (p14 | [a0]~p14) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & ~p14 & [a0]p14 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9 | ~p10 | ~p11 | ~p12 | ~p13 | ~p14))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & ~p10 & ~p11 & ~p12 & ~p13 & ~p14 & ~p15 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & ~p10 & [a0]p10 & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & ~p11 & [a0]p11 & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & ~p12 & [a0]p12 & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & ~p13 & [a0]p13 & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & ~p14 & [a0]p14 & (~p15 | [a0]p15) & (p15 | [a0]~p15) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & ~p15 & [a0]p15 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9 | ~p10 | ~p11 | ~p12 | ~p13 | ~p14 | ~p15))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & ~p10 & ~p11 & ~p12 & ~p13 & ~p14 & ~p15 & ~p16 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & ~p10 & [a0]p10 & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & ~p11 & [a0]p11 & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & ~p12 & [a0]p12 & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & ~p13 & [a0]p13 & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & ~p14 & [a0]p14 & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & ~p15 & [a0]p15 & (~p16 | [a0]p16) & (p16 | [a0]~p16) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & ~p16 & [a0]p16 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & p16 & [a0]~p16) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9 | ~p10 | ~p11 | ~p12 | ~p13 | ~p14 | ~p15 | ~p16))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & ~p10 & ~p11 & ~p12 & ~p13 & ~p14 & ~p15 & ~p16 & ~p17 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & ~p10 & [a0]p10 & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & ~p11 & [a0]p11 & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & ~p12 & [a0]p12 & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & ~p13 & [a0]p13 & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & ~p14 & [a0]p14 & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & ~p15 & [a0]p15 & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & ~p16 & [a0]p16 & (~p17 | [a0]p17) & (p17 | [a0]~p17) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & p16 & [a0]~p16 & ~p17 & [a0]p17 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & p16 & [a0]~p16 & p17 & [a0]~p17) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9 | ~p10 | ~p11 | ~p12 | ~p13 | ~p14 | ~p15 | ~p16 | ~p17))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & ~p10 & ~p11 & ~p12 & ~p13 & ~p14 & ~p15 & ~p16 & ~p17 & ~p18 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & ~p10 & [a0]p10 & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & ~p11 & [a0]p11 & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & ~p12 & [a0]p12 & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & ~p13 & [a0]p13 & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & ~p14 & [a0]p14 & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & ~p15 & [a0]p15 & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & ~p16 & [a0]p16 & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & p16 & [a0]~p16 & ~p17 & [a0]p17 & (~p18 | [a0]p18) & (p18 | [a0]~p18) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & p16 & [a0]~p16 & p17 & [a0]~p17 & ~p18 & [a0]p18 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & p16 & [a0]~p16 & p17 & [a0]~p17 & p18 & [a0]~p18) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9 | ~p10 | ~p11 | ~p12 | ~p13 | ~p14 | ~p15 | ~p16 | ~p17 | ~p18))
~p0 & ~p1 & ~p2 & ~p3 & ~p4 & ~p5 & ~p6 & ~p7 & ~p8 & ~p9 & ~p10 & ~p11 & ~p12 & ~p13 & ~p14 & ~p15 & ~p16 & ~p17 & ~p18 & ~p19 & [a0*](<a0>True & (~p0 & [a0]p0 & (~p1 | [a0]p1) & (p1 | [a0]~p1) & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & ~p1 & [a0]p1 & (~p2 | [a0]p2) & (p2 | [a0]~p2) & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & ~p2 & [a0]p2 & (~p3 | [a0]p3) & (p3 | [a0]~p3) & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & ~p3 & [a0]p3 & (~p4 | [a0]p4) & (p4 | [a0]~p4) & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & ~p4 & [a0]p4 & (~p5 | [a0]p5) & (p5 | [a0]~p5) & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & ~p5 & [a0]p5 & (~p6 | [a0]p6) & (p6 | [a0]~p6) & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & ~p6 & [a0]p6 & (~p7 | [a0]p7) & (p7 | [a0]~p7) & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & ~p7 & [a0]p7 & (~p8 | [a0]p8) & (p8 | [a0]~p8) & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & ~p8 & [a0]p8 & (~p9 | [a0]p9) & (p9 | [a0]~p9) & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & ~p9 & [a0]p9 & (~p10 | [a0]p10) & (p10 | [a0]~p10) & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & ~p10 & [a0]p10 & (~p11 | [a0]p11) & (p11 | [a0]~p11) & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & ~p11 & [a0]p11 & (~p12 | [a0]p12) & (p12 | [a0]~p12) & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & ~p12 & [a0]p12 & (~p13 | [a0]p13) & (p13 | [a0]~p13) & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & ~p13 & [a0]p13 & (~p14 | [a0]p14) & (p14 | [a0]~p14) & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & ~p14 & [a0]p14 & (~p15 | [a0]p15) & (p15 | [a0]~p15) & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & ~p15 & [a0]p15 & (~p16 | [a0]p16) & (p16 | [a0]~p16) & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & ~p16 & [a0]p16 & (~p17 | [a0]p17) & (p17 | [a0]~p17) & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & p16 & [a0]~p16 & ~p17 & [a0]p17 & (~p18 | [a0]p18) & (p18 | [a0]~p18) & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & p16 & [a0]~p16 & p17 & [a0]~p17 & ~p18 & [a0]p18 & (~p19 | [a0]p19) & (p19 | [a0]~p19) | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & p16 & [a0]~p16 & p17 & [a0]~p17 & p18 & [a0]~p18 & ~p19 & [a0]p19 | p0 & [a0]~p0 & p1 & [a0]~p1 & p2 & [a0]~p2 & p3 & [a0]~p3 & p4 & [a0]~p4 & p5 & [a0]~p5 & p6 & [a0]~p6 & p7 & [a0]~p7 & p8 & [a0]~p8 & p9 & [a0]~p9 & p10 & [a0]~p10 & p11 & [a0]~p11 & p12 & [a0]~p12 & p13 & [a0]~p13 & p14 & [a0]~p14 & p15 & [a0]~p15 & p16 & [a0]~p16 & p17 & [a0]~p17 & p18 & [a0]~p18 & p19 & [a0]~p19) & (~p0 | ~p1 | ~p2 | ~p3 | ~p4 | ~p5 | ~p6 | ~p7 | ~p8 | ~p9 | ~p10 | ~p11 | ~p12 | ~p13 | ~p14 | ~p15 | ~p16 | ~p17 | ~p18 | ~p19))