app/willard/test7

   1 Input:
   2 (((not((((((((((((a and b) and c) and d) and e) and a) and b) and c) and d) and e) and(true or false)) and(a and b)) and(a or b))) and(not((a and b) and c))) and true)
   3 (((not((((((((((((a and b) and c) and d) and e) and a) and b) and c) and d) and e) and(true or false)) and(a and b)) and(a or b))) and(not((a and b) and c))) and true)
   4
   5 [Renaming phase]
   6
   7 (((not((((((((((((a and b) and c) and d) and e) and a) and b) and c) and d) and e) and(true or false)) and(a and b)) and(a or b))) and(not((a and b) and c))) and true)
   8
   9 [DNF construction and simplification phase]
  10
  11 (((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or((not a) and((not b) and(not c)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  12
  13 [Constructing the query graph]
  14
  15 [Query Graph]
  16 (((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or((not a) and((not b) and(not c)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  17
  18 [Quantifier elimination phase]
  19
  20 (((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not c) and(not a))) or(((not c) and((not c) and(not b))) or(((not c) and((not c) and(not c))) or(((not c) and((not d) and(not a))) or(((not c) and((not d) and(not b))) or(((not c) and((not d) and(not c))) or(((not c) and((not e) and(not a))) or(((not c) and((not e) and(not b))) or(((not c) and((not e) and(not c))) or(((not c) and((not a) and(not a))) or(((not c) and((not a) and(not b))) or(((not c) and((not a) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not c) and((not b) and(not a))) or(((not c) and((not b) and(not b))) or(((not c) and((not b) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not c) and(not a))) or(((not d) and((not c) and(not b))) or(((not d) and((not c) and(not c))) or(((not d) and((not d) and(not a))) or(((not d) and((not d) and(not b))) or(((not d) and((not d) and(not c))) or(((not d) and((not e) and(not a))) or(((not d) and((not e) and(not b))) or(((not d) and((not e) and(not c))) or(((not d) and((not a) and(not a))) or(((not d) and((not a) and(not b))) or(((not d) and((not a) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not d) and((not b) and(not a))) or(((not d) and((not b) and(not b))) or(((not d) and((not b) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not c) and(not a))) or(((not e) and((not c) and(not b))) or(((not e) and((not c) and(not c))) or(((not e) and((not d) and(not a))) or(((not e) and((not d) and(not b))) or(((not e) and((not d) and(not c))) or(((not e) and((not e) and(not a))) or(((not e) and((not e) and(not b))) or(((not e) and((not e) and(not c))) or(((not e) and((not a) and(not a))) or(((not e) and((not a) and(not b))) or(((not e) and((not a) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not e) and((not b) and(not a))) or(((not e) and((not b) and(not b))) or(((not e) and((not b) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not c) and(not a))) or(((not b) and((not c) and(not b))) or(((not b) and((not c) and(not c))) or(((not b) and((not d) and(not a))) or(((not b) and((not d) and(not b))) or(((not b) and((not d) and(not c))) or(((not b) and((not e) and(not a))) or(((not b) and((not e) and(not b))) or(((not b) and((not e) and(not c))) or(((not b) and((not a) and(not a))) or(((not b) and((not a) and(not b))) or(((not b) and((not a) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not b) and((not b) and(not a))) or(((not b) and((not b) and(not b))) or(((not b) and((not b) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not c) and(not a))) or(((not a) and((not c) and(not b))) or(((not a) and((not c) and(not c))) or(((not a) and((not d) and(not a))) or(((not a) and((not d) and(not b))) or(((not a) and((not d) and(not c))) or(((not a) and((not e) and(not a))) or(((not a) and((not e) and(not b))) or(((not a) and((not e) and(not c))) or(((not a) and((not a) and(not a))) or(((not a) and((not a) and(not b))) or(((not a) and((not a) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or(((not a) and((not b) and(not c))) or(((not a) and((not b) and(not a))) or(((not a) and((not b) and(not b))) or((not a) and((not b) and(not c)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  21
  22 [Disjunction removal phase]
  23
  24 or(((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not c) and(not a))),((not a) and((not c) and(not b))),((not a) and((not c) and(not c))),((not a) and((not d) and(not a))),((not a) and((not d) and(not b))),((not a) and((not d) and(not c))),((not a) and((not e) and(not a))),((not a) and((not e) and(not b))),((not a) and((not e) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not c) and(not a))),((not a) and((not c) and(not b))),((not a) and((not c) and(not c))),((not a) and((not d) and(not a))),((not a) and((not d) and(not b))),((not a) and((not d) and(not c))),((not a) and((not e) and(not a))),((not a) and((not e) and(not b))),((not a) and((not e) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not b) and((not a) and(not a))),((not b) and((not a) and(not b))),((not b) and((not a) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not b) and((not c) and(not a))),((not b) and((not c) and(not b))),((not b) and((not c) and(not c))),((not b) and((not d) and(not a))),((not b) and((not d) and(not b))),((not b) and((not d) and(not c))),((not b) and((not e) and(not a))),((not b) and((not e) and(not b))),((not b) and((not e) and(not c))),((not b) and((not a) and(not a))),((not b) and((not a) and(not b))),((not b) and((not a) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not b) and((not c) and(not a))),((not b) and((not c) and(not b))),((not b) and((not c) and(not c))),((not b) and((not d) and(not a))),((not b) and((not d) and(not b))),((not b) and((not d) and(not c))),((not b) and((not e) and(not a))),((not b) and((not e) and(not b))),((not b) and((not e) and(not c))),((not b) and((not a) and(not a))),((not b) and((not a) and(not b))),((not b) and((not a) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not c) and((not a) and(not a))),((not c) and((not a) and(not b))),((not c) and((not a) and(not c))),((not c) and((not b) and(not a))),((not c) and((not b) and(not b))),((not c) and((not b) and(not c))),((not c) and((not c) and(not a))),((not c) and((not c) and(not b))),((not c) and((not c) and(not c))),((not c) and((not d) and(not a))),((not c) and((not d) and(not b))),((not c) and((not d) and(not c))),((not c) and((not e) and(not a))),((not c) and((not e) and(not b))),((not c) and((not e) and(not c))),((not c) and((not a) and(not a))),((not c) and((not a) and(not b))),((not c) and((not a) and(not c))),((not c) and((not b) and(not a))),((not c) and((not b) and(not b))),((not c) and((not b) and(not c))),((not c) and((not c) and(not a))),((not c) and((not c) and(not b))),((not c) and((not c) and(not c))),((not c) and((not d) and(not a))),((not c) and((not d) and(not b))),((not c) and((not d) and(not c))),((not c) and((not e) and(not a))),((not c) and((not e) and(not b))),((not c) and((not e) and(not c))),((not c) and((not a) and(not a))),((not c) and((not a) and(not b))),((not c) and((not a) and(not c))),((not c) and((not b) and(not a))),((not c) and((not b) and(not b))),((not c) and((not b) and(not c))),((not c) and((not b) and(not a))),((not c) and((not b) and(not b))),((not c) and((not b) and(not c))),((not d) and((not a) and(not a))),((not d) and((not a) and(not b))),((not d) and((not a) and(not c))),((not d) and((not b) and(not a))),((not d) and((not b) and(not b))),((not d) and((not b) and(not c))),((not d) and((not c) and(not a))),((not d) and((not c) and(not b))),((not d) and((not c) and(not c))),((not d) and((not d) and(not a))),((not d) and((not d) and(not b))),((not d) and((not d) and(not c))),((not d) and((not e) and(not a))),((not d) and((not e) and(not b))),((not d) and((not e) and(not c))),((not d) and((not a) and(not a))),((not d) and((not a) and(not b))),((not d) and((not a) and(not c))),((not d) and((not b) and(not a))),((not d) and((not b) and(not b))),((not d) and((not b) and(not c))),((not d) and((not c) and(not a))),((not d) and((not c) and(not b))),((not d) and((not c) and(not c))),((not d) and((not d) and(not a))),((not d) and((not d) and(not b))),((not d) and((not d) and(not c))),((not d) and((not e) and(not a))),((not d) and((not e) and(not b))),((not d) and((not e) and(not c))),((not d) and((not a) and(not a))),((not d) and((not a) and(not b))),((not d) and((not a) and(not c))),((not d) and((not b) and(not a))),((not d) and((not b) and(not b))),((not d) and((not b) and(not c))),((not d) and((not b) and(not a))),((not d) and((not b) and(not b))),((not d) and((not b) and(not c))),((not e) and((not a) and(not a))),((not e) and((not a) and(not b))),((not e) and((not a) and(not c))),((not e) and((not b) and(not a))),((not e) and((not b) and(not b))),((not e) and((not b) and(not c))),((not e) and((not c) and(not a))),((not e) and((not c) and(not b))),((not e) and((not c) and(not c))),((not e) and((not d) and(not a))),((not e) and((not d) and(not b))),((not e) and((not d) and(not c))),((not e) and((not e) and(not a))),((not e) and((not e) and(not b))),((not e) and((not e) and(not c))),((not e) and((not a) and(not a))),((not e) and((not a) and(not b))),((not e) and((not a) and(not c))),((not e) and((not b) and(not a))),((not e) and((not b) and(not b))),((not e) and((not b) and(not c))),((not e) and((not c) and(not a))),((not e) and((not c) and(not b))),((not e) and((not c) and(not c))),((not e) and((not d) and(not a))),((not e) and((not d) and(not b))),((not e) and((not d) and(not c))),((not e) and((not e) and(not a))),((not e) and((not e) and(not b))),((not e) and((not e) and(not c))),((not e) and((not a) and(not a))),((not e) and((not a) and(not b))),((not e) and((not a) and(not c))),((not e) and((not b) and(not a))),((not e) and((not b) and(not b))),((not e) and((not b) and(not c))),((not e) and((not b) and(not a))),((not e) and((not b) and(not b))),((not e) and((not b) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not c) and(not a))),((not a) and((not c) and(not b))),((not a) and((not c) and(not c))),((not a) and((not d) and(not a))),((not a) and((not d) and(not b))),((not a) and((not d) and(not c))),((not a) and((not e) and(not a))),((not a) and((not e) and(not b))),((not a) and((not e) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not c) and(not a))),((not a) and((not c) and(not b))),((not a) and((not c) and(not c))),((not a) and((not d) and(not a))),((not a) and((not d) and(not b))),((not a) and((not d) and(not c))),((not a) and((not e) and(not a))),((not a) and((not e) and(not b))),((not a) and((not e) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not b) and((not a) and(not a))),((not b) and((not a) and(not b))),((not b) and((not a) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not b) and((not c) and(not a))),((not b) and((not c) and(not b))),((not b) and((not c) and(not c))),((not b) and((not d) and(not a))),((not b) and((not d) and(not b))),((not b) and((not d) and(not c))),((not b) and((not e) and(not a))),((not b) and((not e) and(not b))),((not b) and((not e) and(not c))),((not b) and((not a) and(not a))),((not b) and((not a) and(not b))),((not b) and((not a) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not b) and((not c) and(not a))),((not b) and((not c) and(not b))),((not b) and((not c) and(not c))),((not b) and((not d) and(not a))),((not b) and((not d) and(not b))),((not b) and((not d) and(not c))),((not b) and((not e) and(not a))),((not b) and((not e) and(not b))),((not b) and((not e) and(not c))),((not b) and((not a) and(not a))),((not b) and((not a) and(not b))),((not b) and((not a) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not c) and((not a) and(not a))),((not c) and((not a) and(not b))),((not c) and((not a) and(not c))),((not c) and((not b) and(not a))),((not c) and((not b) and(not b))),((not c) and((not b) and(not c))),((not c) and((not c) and(not a))),((not c) and((not c) and(not b))),((not c) and((not c) and(not c))),((not c) and((not d) and(not a))),((not c) and((not d) and(not b))),((not c) and((not d) and(not c))),((not c) and((not e) and(not a))),((not c) and((not e) and(not b))),((not c) and((not e) and(not c))),((not c) and((not a) and(not a))),((not c) and((not a) and(not b))),((not c) and((not a) and(not c))),((not c) and((not b) and(not a))),((not c) and((not b) and(not b))),((not c) and((not b) and(not c))),((not c) and((not c) and(not a))),((not c) and((not c) and(not b))),((not c) and((not c) and(not c))),((not c) and((not d) and(not a))),((not c) and((not d) and(not b))),((not c) and((not d) and(not c))),((not c) and((not e) and(not a))),((not c) and((not e) and(not b))),((not c) and((not e) and(not c))),((not c) and((not a) and(not a))),((not c) and((not a) and(not b))),((not c) and((not a) and(not c))),((not c) and((not b) and(not a))),((not c) and((not b) and(not b))),((not c) and((not b) and(not c))),((not c) and((not b) and(not a))),((not c) and((not b) and(not b))),((not c) and((not b) and(not c))),((not d) and((not a) and(not a))),((not d) and((not a) and(not b))),((not d) and((not a) and(not c))),((not d) and((not b) and(not a))),((not d) and((not b) and(not b))),((not d) and((not b) and(not c))),((not d) and((not c) and(not a))),((not d) and((not c) and(not b))),((not d) and((not c) and(not c))),((not d) and((not d) and(not a))),((not d) and((not d) and(not b))),((not d) and((not d) and(not c))),((not d) and((not e) and(not a))),((not d) and((not e) and(not b))),((not d) and((not e) and(not c))),((not d) and((not a) and(not a))),((not d) and((not a) and(not b))),((not d) and((not a) and(not c))),((not d) and((not b) and(not a))),((not d) and((not b) and(not b))),((not d) and((not b) and(not c))),((not d) and((not c) and(not a))),((not d) and((not c) and(not b))),((not d) and((not c) and(not c))),((not d) and((not d) and(not a))),((not d) and((not d) and(not b))),((not d) and((not d) and(not c))),((not d) and((not e) and(not a))),((not d) and((not e) and(not b))),((not d) and((not e) and(not c))),((not d) and((not a) and(not a))),((not d) and((not a) and(not b))),((not d) and((not a) and(not c))),((not d) and((not b) and(not a))),((not d) and((not b) and(not b))),((not d) and((not b) and(not c))),((not d) and((not b) and(not a))),((not d) and((not b) and(not b))),((not d) and((not b) and(not c))),((not e) and((not a) and(not a))),((not e) and((not a) and(not b))),((not e) and((not a) and(not c))),((not e) and((not b) and(not a))),((not e) and((not b) and(not b))),((not e) and((not b) and(not c))),((not e) and((not c) and(not a))),((not e) and((not c) and(not b))),((not e) and((not c) and(not c))),((not e) and((not d) and(not a))),((not e) and((not d) and(not b))),((not e) and((not d) and(not c))),((not e) and((not e) and(not a))),((not e) and((not e) and(not b))),((not e) and((not e) and(not c))),((not e) and((not a) and(not a))),((not e) and((not a) and(not b))),((not e) and((not a) and(not c))),((not e) and((not b) and(not a))),((not e) and((not b) and(not b))),((not e) and((not b) and(not c))),((not e) and((not c) and(not a))),((not e) and((not c) and(not b))),((not e) and((not c) and(not c))),((not e) and((not d) and(not a))),((not e) and((not d) and(not b))),((not e) and((not d) and(not c))),((not e) and((not e) and(not a))),((not e) and((not e) and(not b))),((not e) and((not e) and(not c))),((not e) and((not a) and(not a))),((not e) and((not a) and(not b))),((not e) and((not a) and(not c))),((not e) and((not b) and(not a))),((not e) and((not b) and(not b))),((not e) and((not b) and(not c))),((not e) and((not b) and(not a))),((not e) and((not b) and(not b))),((not e) and((not b) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not c) and(not a))),((not a) and((not c) and(not b))),((not a) and((not c) and(not c))),((not a) and((not d) and(not a))),((not a) and((not d) and(not b))),((not a) and((not d) and(not c))),((not a) and((not e) and(not a))),((not a) and((not e) and(not b))),((not a) and((not e) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not c) and(not a))),((not a) and((not c) and(not b))),((not a) and((not c) and(not c))),((not a) and((not d) and(not a))),((not a) and((not d) and(not b))),((not a) and((not d) and(not c))),((not a) and((not e) and(not a))),((not a) and((not e) and(not b))),((not a) and((not e) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not b) and((not a) and(not a))),((not b) and((not a) and(not b))),((not b) and((not a) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not b) and((not c) and(not a))),((not b) and((not c) and(not b))),((not b) and((not c) and(not c))),((not b) and((not d) and(not a))),((not b) and((not d) and(not b))),((not b) and((not d) and(not c))),((not b) and((not e) and(not a))),((not b) and((not e) and(not b))),((not b) and((not e) and(not c))),((not b) and((not a) and(not a))),((not b) and((not a) and(not b))),((not b) and((not a) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not b) and((not c) and(not a))),((not b) and((not c) and(not b))),((not b) and((not c) and(not c))),((not b) and((not d) and(not a))),((not b) and((not d) and(not b))),((not b) and((not d) and(not c))),((not b) and((not e) and(not a))),((not b) and((not e) and(not b))),((not b) and((not e) and(not c))),((not b) and((not a) and(not a))),((not b) and((not a) and(not b))),((not b) and((not a) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not b) and((not b) and(not a))),((not b) and((not b) and(not b))),((not b) and((not b) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not c) and(not a))),((not a) and((not c) and(not b))),((not a) and((not c) and(not c))),((not a) and((not d) and(not a))),((not a) and((not d) and(not b))),((not a) and((not d) and(not c))),((not a) and((not e) and(not a))),((not a) and((not e) and(not b))),((not a) and((not e) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not c) and(not a))),((not a) and((not c) and(not b))),((not a) and((not c) and(not c))),((not a) and((not d) and(not a))),((not a) and((not d) and(not b))),((not a) and((not d) and(not c))),((not a) and((not e) and(not a))),((not a) and((not e) and(not b))),((not a) and((not e) and(not c))),((not a) and((not a) and(not a))),((not a) and((not a) and(not b))),((not a) and((not a) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))),((not a) and((not b) and(not a))),((not a) and((not b) and(not b))),((not a) and((not b) and(not c))))
  25
  26 [Conjunctive query decomposition phase]
  27
  28 [Query Graph]
  29 or(and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)))
  30
  31 [Projection recognition phase]
  32
  33 or(and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)))
  34
  35 [Simple find/count query decomposition phase]
  36
  37 Output:
  38 or(and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not c),(not a)),and((not c),(not c),(not b)),and((not c),(not c),(not c)),and((not c),(not d),(not a)),and((not c),(not d),(not b)),and((not c),(not d),(not c)),and((not c),(not e),(not a)),and((not c),(not e),(not b)),and((not c),(not e),(not c)),and((not c),(not a),(not a)),and((not c),(not a),(not b)),and((not c),(not a),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not c),(not b),(not a)),and((not c),(not b),(not b)),and((not c),(not b),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not c),(not a)),and((not d),(not c),(not b)),and((not d),(not c),(not c)),and((not d),(not d),(not a)),and((not d),(not d),(not b)),and((not d),(not d),(not c)),and((not d),(not e),(not a)),and((not d),(not e),(not b)),and((not d),(not e),(not c)),and((not d),(not a),(not a)),and((not d),(not a),(not b)),and((not d),(not a),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not d),(not b),(not a)),and((not d),(not b),(not b)),and((not d),(not b),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not c),(not a)),and((not e),(not c),(not b)),and((not e),(not c),(not c)),and((not e),(not d),(not a)),and((not e),(not d),(not b)),and((not e),(not d),(not c)),and((not e),(not e),(not a)),and((not e),(not e),(not b)),and((not e),(not e),(not c)),and((not e),(not a),(not a)),and((not e),(not a),(not b)),and((not e),(not a),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not e),(not b),(not a)),and((not e),(not b),(not b)),and((not e),(not b),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not c),(not a)),and((not b),(not c),(not b)),and((not b),(not c),(not c)),and((not b),(not d),(not a)),and((not b),(not d),(not b)),and((not b),(not d),(not c)),and((not b),(not e),(not a)),and((not b),(not e),(not b)),and((not b),(not e),(not c)),and((not b),(not a),(not a)),and((not b),(not a),(not b)),and((not b),(not a),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not b),(not b),(not a)),and((not b),(not b),(not b)),and((not b),(not b),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not c),(not a)),and((not a),(not c),(not b)),and((not a),(not c),(not c)),and((not a),(not d),(not a)),and((not a),(not d),(not b)),and((not a),(not d),(not c)),and((not a),(not e),(not a)),and((not a),(not e),(not b)),and((not a),(not e),(not c)),and((not a),(not a),(not a)),and((not a),(not a),(not b)),and((not a),(not a),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)),and((not a),(not b),(not a)),and((not a),(not b),(not b)),and((not a),(not b),(not c)))