% |X| = 150   |Y| = 5
Exists(x1).
Exists(x2).
Exists(x3).
Exists(x4).
Exists(x5).
Exists(x6).
Exists(x7).
Exists(x8).
Exists(x9).
Exists(x10).
Exists(x11).
Exists(x12).
Exists(x13).
Exists(x14).
Exists(x15).
Exists(x16).
Exists(x17).
Exists(x18).
Exists(x19).
Exists(x20).
Exists(x21).
Exists(x22).
Exists(x23).
Exists(x24).
Exists(x25).
Exists(x26).
Exists(x27).
Exists(x28).
Exists(x29).
Exists(x30).
Exists(x31).
Exists(x32).
Exists(x33).
Exists(x34).
Exists(x35).
Exists(x36).
Exists(x37).
Exists(x38).
Exists(x39).
Exists(x40).
Exists(x41).
Exists(x42).
Exists(x43).
Exists(x44).
Exists(x45).
Exists(x46).
Exists(x47).
Exists(x48).
Exists(x49).
Exists(x50).
Exists(x51).
Exists(x52).
Exists(x53).
Exists(x54).
Exists(x55).
Exists(x56).
Exists(x57).
Exists(x58).
Exists(x59).
Exists(x60).
Exists(x61).
Exists(x62).
Exists(x63).
Exists(x64).
Exists(x65).
Exists(x66).
Exists(x67).
Exists(x68).
Exists(x69).
Exists(x70).
Exists(x71).
Exists(x72).
Exists(x73).
Exists(x74).
Exists(x75).
Exists(x76).
Exists(x77).
Exists(x78).
Exists(x79).
Exists(x80).
Exists(x81).
Exists(x82).
Exists(x83).
Exists(x84).
Exists(x85).
Exists(x86).
Exists(x87).
Exists(x88).
Exists(x89).
Exists(x90).
Exists(x91).
Exists(x92).
Exists(x93).
Exists(x94).
Exists(x95).
Exists(x96).
Exists(x97).
Exists(x98).
Exists(x99).
Exists(x100).
Exists(x101).
Exists(x102).
Exists(x103).
Exists(x104).
Exists(x105).
Exists(x106).
Exists(x107).
Exists(x108).
Exists(x109).
Exists(x110).
Exists(x111).
Exists(x112).
Exists(x113).
Exists(x114).
Exists(x115).
Exists(x116).
Exists(x117).
Exists(x118).
Exists(x119).
Exists(x120).
Exists(x121).
Exists(x122).
Exists(x123).
Exists(x124).
Exists(x125).
Exists(x126).
Exists(x127).
Exists(x128).
Exists(x129).
Exists(x130).
Exists(x131).
Exists(x132).
Exists(x133).
Exists(x134).
Exists(x135).
Exists(x136).
Exists(x137).
Exists(x138).
Exists(x139).
Exists(x140).
Exists(x141).
Exists(x142).
Exists(x143).
Exists(x144).
Exists(x145).
Exists(x146).
Exists(x147).
Exists(x148).
Exists(x149).
Exists(x150).
Forall(y151).
Forall(y152).
Forall(y153).
Forall(y154).
Forall(y155).
Conjunct(x51, x60, true, false, false, y151).
Conjunct(x66, true, y154, false, x30, false).
Conjunct(x15, true, y153, false, x8, false).
Conjunct(true, true, y154, x60, x74, false).
Conjunct(true, x98, y152, x81, false, false).
Conjunct(true, x144, y153, x137, false, false).
Conjunct(x45, true, y155, false, x126, false).
Conjunct(x122, x29, y155, false, false, false).
Conjunct(y154, true, true, false, y152, x117).
Conjunct(true, x142, y153, x127, false, false).
Conjunct(true, x37, y154, x145, false, false).
Conjunct(true, x64, true, x99, false, y151).
Conjunct(x13, x137, y153, false, false, false).
Conjunct(true, true, true, x147, x100, y151).
Conjunct(x10, true, y155, false, x40, false).
Conjunct(true, x50, y152, x6, false, false).
Conjunct(x149, true, y155, false, x4, false).
Conjunct(true, true, y153, x125, x42, false).
Conjunct(x133, true, y155, false, x43, false).
Conjunct(true, y153, true, x106, false, x94).
Conjunct(true, x146, true, x49, false, y151).
Conjunct(x139, x10, true, false, false, y151).
Conjunct(x17, true, y152, false, x62, false).
Conjunct(true, true, y152, x116, x57, false).
Conjunct(true, x102, true, x9, false, y151).
Conjunct(true, true, y155, x145, x144, false).
Conjunct(x110, true, y153, false, x10, false).
Conjunct(true, true, y152, x123, x67, false).
Conjunct(x50, x39, y153, false, false, false).
Conjunct(true, true, y153, x122, x59, false).
Conjunct(true, y154, true, x147, false, x72).
Conjunct(true, x147, y155, x104, false, false).
Conjunct(true, x127, y155, x80, false, false).
Conjunct(x12, true, y155, false, x149, false).
Conjunct(x74, x14, true, false, false, y151).
Conjunct(x94, true, y152, false, x73, false).
Conjunct(x38, x51, y154, false, false, false).
Conjunct(x118, x1, y152, false, false, false).
Conjunct(true, true, y154, x86, x21, false).
Conjunct(x113, x148, y154, false, false, false).
Conjunct(true, x81, y153, x110, false, false).
Conjunct(x10, true, y153, false, x29, false).
Conjunct(y153, true, true, false, x21, x24).
Conjunct(x64, x20, y152, false, false, false).
Conjunct(true, true, y152, x131, x75, false).
Conjunct(true, true, y153, x60, x34, false).
Conjunct(true, x103, y155, x57, false, false).
Conjunct(true, true, true, x145, x100, y151).
Conjunct(true, true, true, x100, x139, y151).
Conjunct(true, x89, y152, x7, false, false).
Conjunct(x130, x140, y155, false, false, false).
Conjunct(true, true, y155, x58, x95, false).
Conjunct(x140, true, y155, false, x92, false).
Conjunct(x36, true, y155, false, x81, false).
Conjunct(true, true, y154, x74, x28, false).
Conjunct(x44, true, y152, false, x150, false).
Conjunct(true, true, y152, x103, x1, false).
Conjunct(true, x64, y153, x79, false, false).
Conjunct(true, x114, y153, x120, false, false).
Conjunct(x29, x26, y154, false, false, false).
Conjunct(x45, x27, y155, false, false, false).
Conjunct(true, x46, true, x55, false, y151).
Conjunct(true, true, y152, x100, x122, false).
Conjunct(x70, x59, y152, false, false, false).
Conjunct(x119, x40, y155, false, false, false).
Conjunct(true, x84, y152, x63, false, false).
Conjunct(x14, x147, y155, false, false, false).
Conjunct(x61, true, true, false, x102, y151).
Conjunct(x101, true, y152, false, x120, false).
Conjunct(true, x136, y155, x23, false, false).
Conjunct(true, true, y153, x48, x66, false).
Conjunct(true, x35, y152, x56, false, false).
Conjunct(true, x110, y154, x7, false, false).
Conjunct(x61, true, y155, false, x42, false).
Conjunct(true, x119, true, x102, false, y151).
Conjunct(x134, true, true, false, x133, y151).
Conjunct(true, true, y154, x61, x135, false).
Conjunct(true, true, y154, x108, x18, false).
Conjunct(true, x16, true, x69, false, y151).
Conjunct(true, true, y153, x133, x41, false).
Conjunct(true, x59, y155, x53, false, false).
Conjunct(x108, true, y154, false, x128, false).
Conjunct(true, true, true, x25, x121, y151).
Conjunct(true, x80, y153, x86, false, false).
Conjunct(true, x52, y155, x35, false, false).
Conjunct(true, x96, y152, x90, false, false).
Conjunct(x103, true, y152, false, x72, false).
Conjunct(x128, true, y155, false, x14, false).
Conjunct(true, true, y152, x75, x89, false).
Conjunct(x31, true, y155, false, x96, false).
Conjunct(x53, x8, y153, false, false, false).
Conjunct(true, x11, y152, x63, false, false).
Conjunct(true, x101, true, x110, false, y151).
Conjunct(true, true, y155, x12, x51, false).
Conjunct(true, x107, y155, x37, false, false).
Conjunct(true, y154, x68, x45, false, false).
Conjunct(true, true, true, x126, x70, y151).
Conjunct(x113, x140, true, false, false, y151).
Conjunct(true, x60, true, x102, false, y151).
Conjunct(true, true, y155, x51, x105, false).
Conjunct(x84, x38, y155, false, false, false).
Conjunct(true, x103, y154, x52, false, false).
Conjunct(x87, true, y155, false, x150, false).
Conjunct(x54, true, y154, false, x14, false).
Conjunct(x132, true, y155, false, x110, false).
Conjunct(true, x72, y155, x16, false, false).
Conjunct(true, true, y153, x79, x62, false).
Conjunct(true, true, y155, x113, x83, false).
Conjunct(x57, x32, true, false, false, y151).
Conjunct(true, true, true, x92, x136, y151).
Conjunct(x80, y154, true, false, false, x107).
Conjunct(y152, true, x9, false, x150, false).
Conjunct(true, x40, y154, x132, false, false).
Conjunct(true, x53, true, x130, false, y151).
Conjunct(true, x33, y154, x36, false, false).
Conjunct(x136, true, y152, false, x129, false).
Conjunct(x90, true, y154, false, x103, false).
Conjunct(x128, true, y154, false, x96, false).
Conjunct(x119, true, true, false, x31, y151).
Conjunct(true, true, y153, x89, x58, false).
Conjunct(true, true, y153, x146, x3, false).
Conjunct(x71, x56, y154, false, false, false).
Conjunct(x67, true, x91, false, y151, false).
Conjunct(x80, x87, y155, false, false, false).
Conjunct(true, x114, y155, x99, false, false).
Conjunct(true, true, y152, x49, x36, false).
Conjunct(x147, x35, y154, false, false, false).
Conjunct(x32, true, y153, false, x113, false).
Conjunct(true, x14, true, x150, false, y151).
Conjunct(x7, x63, y154, false, false, false).
Conjunct(true, true, y155, x65, x60, false).
Conjunct(true, true, y154, x42, x3, false).
Conjunct(true, x98, y154, x42, false, false).
Conjunct(true, y154, x57, x64, false, false).
Conjunct(x70, x38, y153, false, false, false).
Conjunct(x119, x116, y152, false, false, false).
Conjunct(x110, true, y155, false, x16, false).
Conjunct(true, x11, y153, x54, false, false).
Conjunct(true, true, y154, x142, x64, false).
Conjunct(x70, true, true, false, x114, y151).
Conjunct(x29, true, y155, false, x106, false).
Conjunct(true, true, true, x41, x70, y151).
Conjunct(true, y152, true, x74, false, y155).
Conjunct(true, x14, y152, x40, false, false).
Conjunct(x18, x53, true, false, false, y151).
Conjunct(true, x3, true, x118, false, y151).
Conjunct(x70, true, y155, false, x116, false).
Conjunct(x43, true, y154, false, x90, false).
Conjunct(x43, true, y154, false, x77, false).
Conjunct(true, x126, true, x147, false, y151).
Conjunct(x62, true, y152, false, x34, false).
Conjunct(true, x133, y154, x77, false, false).
Conjunct(x14, x102, y152, false, false, false).
Conjunct(x140, true, y154, false, x87, false).
Conjunct(x148, x37, y152, false, false, false).
Conjunct(x19, true, y155, false, x117, false).
Conjunct(x137, true, y152, false, x45, false).
Conjunct(true, true, y155, x76, x68, false).
Conjunct(x27, x85, y153, false, false, false).
Conjunct(true, x93, true, x23, false, y151).
Conjunct(true, x113, y154, x123, false, false).
Conjunct(x58, true, y155, false, x78, false).
Conjunct(x97, true, true, false, x90, y151).
Conjunct(true, x15, y152, x119, false, false).
Conjunct(x95, x15, y155, false, false, false).
Conjunct(x51, x130, y154, false, false, false).
Conjunct(true, x11, y154, x3, false, false).
Conjunct(true, x14, y152, x98, false, false).
Conjunct(true, x37, y152, x90, false, false).
Conjunct(x82, x16, y154, false, false, false).
Conjunct(true, x57, y155, x50, false, false).
Conjunct(x85, x107, y155, false, false, false).
Conjunct(x70, x6, y154, false, false, false).
Conjunct(x68, x21, y152, false, false, false).
Conjunct(true, true, y154, x14, x57, false).
Conjunct(true, true, y153, x97, x34, false).
Conjunct(y155, x86, x67, false, false, false).
Conjunct(true, true, y155, x138, x13, false).
Conjunct(x69, x21, y154, false, false, false).
Conjunct(true, true, y155, x2, x82, false).
Conjunct(true, x85, true, x88, false, y151).
Conjunct(true, true, y154, x12, x83, false).
Conjunct(x29, x108, true, false, false, y151).
Conjunct(x10, x43, y153, false, false, false).
Conjunct(true, x126, y153, x138, false, false).
Conjunct(true, x66, y155, x102, false, false).
Conjunct(true, x42, y155, x142, false, false).
Conjunct(true, true, y155, x44, x100, false).
Conjunct(true, true, y154, x142, x50, false).
Conjunct(true, true, y153, x32, x88, false).
Conjunct(true, y154, x129, x12, false, false).
Conjunct(x48, x117, y154, false, false, false).
Conjunct(x29, x1, y155, false, false, false).
Conjunct(x58, true, y153, false, x56, false).
Conjunct(x105, true, y153, false, x40, false).
Conjunct(x69, x4, y153, false, false, false).
Conjunct(true, x101, y155, x79, false, false).
Conjunct(true, true, x36, y151, x144, false).
Conjunct(x22, x128, true, false, false, y151).
Conjunct(x95, true, y152, false, x6, false).
Conjunct(y153, true, x57, false, x99, false).
Conjunct(true, y153, true, x68, false, x16).
Conjunct(x68, x93, y154, false, false, false).
Conjunct(x50, true, y152, false, x116, false).
Conjunct(true, x70, y152, x51, false, false).
Conjunct(true, true, y152, x31, x100, false).
Conjunct(true, x39, y154, x91, false, false).
Conjunct(true, x134, y152, x73, false, false).
Conjunct(x14, true, y155, false, x128, false).
Conjunct(x77, true, true, false, x2, y151).
Conjunct(x63, x36, y154, false, false, false).
Conjunct(x50, true, y153, false, x92, false).
Conjunct(x1, x36, true, false, false, y151).
Conjunct(x146, x112, y155, false, false, false).
Conjunct(true, true, y152, x64, x119, false).
Conjunct(x144, true, true, false, x103, y151).
Conjunct(x62, true, y152, false, x106, false).
Conjunct(true, true, y152, x86, x24, false).
Conjunct(true, true, y153, x65, x23, false).
Conjunct(x82, x61, y152, false, false, false).
Conjunct(x101, x134, y152, false, false, false).
Conjunct(true, x72, y155, x138, false, false).
Conjunct(x145, true, true, false, x48, y151).
Conjunct(true, true, y153, x90, x115, false).
Conjunct(x93, x82, y152, false, false, false).
Conjunct(x119, x5, y154, false, false, false).
Conjunct(true, true, y154, x24, x114, false).
Conjunct(true, x3, y155, x45, false, false).
Conjunct(x44, true, y153, false, x65, false).
Conjunct(true, x35, y153, x122, false, false).
Conjunct(x61, true, y152, false, x4, false).
Conjunct(x48, x53, true, false, false, y151).
Conjunct(true, x85, y154, x134, false, false).
Conjunct(true, x2, true, x140, false, y151).
Conjunct(true, true, y153, x122, x39, false).
Conjunct(x85, x43, y155, false, false, false).
Conjunct(true, true, y153, x28, x15, false).
Conjunct(true, true, true, x150, x149, y151).
Conjunct(x111, true, y153, false, x29, false).
Conjunct(x83, true, true, false, x147, y151).
Conjunct(true, true, y155, x64, x147, false).
Conjunct(x112, true, true, false, x113, y151).
Conjunct(x1, x38, y154, false, false, false).
Conjunct(true, true, y154, x101, x88, false).
Conjunct(true, true, y154, x138, x22, false).
Conjunct(y153, x105, x44, false, false, false).
Conjunct(true, true, y153, x79, x36, false).
Conjunct(x31, y153, x66, false, false, false).
Conjunct(y155, x69, x141, false, false, false).
Conjunct(x15, true, y155, false, x44, false).
Conjunct(true, x68, y152, x24, false, false).
Conjunct(true, true, y153, x22, x31, false).
Conjunct(true, x49, y155, x59, false, false).
Conjunct(true, true, y152, x34, x87, false).
Conjunct(x90, x59, y154, false, false, false).
Conjunct(x9, x48, y153, false, false, false).
Conjunct(x110, x83, y153, false, false, false).
Conjunct(x65, x138, true, false, false, y151).
Conjunct(x111, x27, y154, false, false, false).
Conjunct(x107, true, y154, false, x50, false).
Conjunct(x40, true, y154, false, x8, false).
Conjunct(x43, x110, y155, false, false, false).
Conjunct(true, x80, y152, x18, false, false).
Conjunct(true, true, y155, x86, x145, false).
Conjunct(x74, true, y154, false, x140, false).
Conjunct(true, true, y155, x112, x88, false).
Conjunct(x77, true, true, false, x95, y151).
Conjunct(x21, x75, true, false, false, y151).
Conjunct(x106, x146, y152, false, false, false).
Conjunct(x58, y152, x141, false, false, false).
Conjunct(x86, x106, y154, false, false, false).
Conjunct(x59, x126, y155, false, false, false).
Conjunct(x13, true, y152, false, x86, false).
Conjunct(true, true, y152, x58, x136, false).
Conjunct(true, x44, y155, x42, false, false).
Conjunct(true, true, y155, x131, x95, false).
Conjunct(true, true, y154, x78, x71, false).
Conjunct(true, x30, y153, x25, false, false).
Conjunct(true, x44, y155, x134, false, false).
Conjunct(x99, x110, true, false, false, y151).
Conjunct(x79, x42, y152, false, false, false).
Conjunct(x98, x87, y154, false, false, false).
Conjunct(x71, true, y154, false, x79, false).
Conjunct(true, x64, y155, x13, false, false).
Conjunct(true, x41, y154, x25, false, false).
Conjunct(x84, true, true, false, y151, x115).
Conjunct(true, true, y152, x3, x83, false).
Conjunct(x123, x114, y152, false, false, false).
Conjunct(x101, true, y152, false, x118, false).
Conjunct(x56, true, y153, false, x54, false).
Conjunct(x35, true, y153, false, x54, false).
Conjunct(x45, x102, y152, false, false, false).
Conjunct(x42, true, y155, false, x43, false).
Conjunct(x116, x113, y153, false, false, false).
Conjunct(x33, true, y152, false, x19, false).
Conjunct(true, x119, true, y151, false, x137).
Conjunct(x72, true, y152, false, x47, false).
Conjunct(true, true, y154, x29, x72, false).
Conjunct(x10, true, y155, false, x100, false).
Conjunct(x65, true, y153, false, x85, false).