% |X| = 496   |Y| = 498
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).
Exists(x151).
Exists(x152).
Exists(x153).
Exists(x154).
Exists(x155).
Exists(x156).
Exists(x157).
Exists(x158).
Exists(x159).
Exists(x160).
Exists(x161).
Exists(x162).
Exists(x163).
Exists(x164).
Exists(x165).
Exists(x166).
Exists(x167).
Exists(x168).
Exists(x169).
Exists(x170).
Exists(x171).
Exists(x172).
Exists(x173).
Exists(x174).
Exists(x175).
Exists(x176).
Exists(x177).
Exists(x178).
Exists(x179).
Exists(x180).
Exists(x181).
Exists(x182).
Exists(x183).
Exists(x184).
Exists(x185).
Exists(x186).
Exists(x187).
Exists(x188).
Exists(x189).
Exists(x190).
Exists(x191).
Exists(x192).
Exists(x193).
Exists(x194).
Exists(x195).
Exists(x196).
Exists(x197).
Exists(x198).
Exists(x199).
Exists(x200).
Exists(x201).
Exists(x202).
Exists(x203).
Exists(x204).
Exists(x205).
Exists(x206).
Exists(x207).
Exists(x208).
Exists(x209).
Exists(x210).
Exists(x211).
Exists(x212).
Exists(x213).
Exists(x214).
Exists(x215).
Exists(x216).
Exists(x217).
Exists(x218).
Exists(x219).
Exists(x220).
Exists(x221).
Exists(x222).
Exists(x223).
Exists(x224).
Exists(x225).
Exists(x226).
Exists(x227).
Exists(x228).
Exists(x229).
Exists(x230).
Exists(x231).
Exists(x232).
Exists(x233).
Exists(x234).
Exists(x235).
Exists(x236).
Exists(x237).
Exists(x238).
Exists(x239).
Exists(x240).
Exists(x241).
Exists(x242).
Exists(x243).
Exists(x244).
Exists(x245).
Exists(x246).
Exists(x247).
Exists(x248).
Exists(x249).
Exists(x250).
Exists(x251).
Exists(x252).
Exists(x253).
Exists(x254).
Exists(x255).
Exists(x256).
Exists(x257).
Exists(x258).
Exists(x259).
Exists(x260).
Exists(x261).
Exists(x262).
Exists(x263).
Exists(x264).
Exists(x265).
Exists(x266).
Exists(x267).
Exists(x268).
Exists(x269).
Exists(x270).
Exists(x271).
Exists(x272).
Exists(x273).
Exists(x274).
Exists(x275).
Exists(x276).
Exists(x277).
Exists(x278).
Exists(x279).
Exists(x280).
Exists(x281).
Exists(x282).
Exists(x283).
Exists(x284).
Exists(x285).
Exists(x286).
Exists(x287).
Exists(x288).
Exists(x289).
Exists(x290).
Exists(x291).
Exists(x292).
Exists(x293).
Exists(x294).
Exists(x295).
Exists(x296).
Exists(x297).
Exists(x298).
Exists(x299).
Exists(x300).
Exists(x301).
Exists(x302).
Exists(x303).
Exists(x304).
Exists(x305).
Exists(x306).
Exists(x307).
Exists(x308).
Exists(x309).
Exists(x310).
Exists(x311).
Exists(x312).
Exists(x313).
Exists(x314).
Exists(x315).
Exists(x316).
Exists(x317).
Exists(x318).
Exists(x319).
Exists(x320).
Exists(x321).
Exists(x322).
Exists(x323).
Exists(x324).
Exists(x325).
Exists(x326).
Exists(x327).
Exists(x328).
Exists(x329).
Exists(x330).
Exists(x331).
Exists(x332).
Exists(x333).
Exists(x334).
Exists(x335).
Exists(x336).
Exists(x337).
Exists(x338).
Exists(x339).
Exists(x340).
Exists(x341).
Exists(x342).
Exists(x343).
Exists(x344).
Exists(x345).
Exists(x346).
Exists(x347).
Exists(x348).
Exists(x349).
Exists(x350).
Exists(x351).
Exists(x352).
Exists(x353).
Exists(x354).
Exists(x355).
Exists(x356).
Exists(x357).
Exists(x358).
Exists(x359).
Exists(x360).
Exists(x361).
Exists(x362).
Exists(x363).
Exists(x364).
Exists(x365).
Exists(x366).
Exists(x367).
Exists(x368).
Exists(x369).
Exists(x370).
Exists(x371).
Exists(x372).
Exists(x373).
Exists(x374).
Exists(x375).
Exists(x376).
Exists(x377).
Exists(x378).
Exists(x379).
Exists(x380).
Exists(x381).
Exists(x382).
Exists(x383).
Exists(x384).
Exists(x385).
Exists(x386).
Exists(x387).
Exists(x388).
Exists(x389).
Exists(x390).
Exists(x391).
Exists(x392).
Exists(x393).
Exists(x394).
Exists(x395).
Exists(x396).
Exists(x397).
Exists(x398).
Exists(x399).
Exists(x400).
Exists(x401).
Exists(x402).
Exists(x403).
Exists(x404).
Exists(x405).
Exists(x406).
Exists(x407).
Exists(x408).
Exists(x409).
Exists(x410).
Exists(x411).
Exists(x412).
Exists(x413).
Exists(x414).
Exists(x415).
Exists(x416).
Exists(x417).
Exists(x418).
Exists(x419).
Exists(x420).
Exists(x421).
Exists(x422).
Exists(x423).
Exists(x424).
Exists(x425).
Exists(x426).
Exists(x427).
Exists(x428).
Exists(x429).
Exists(x430).
Exists(x431).
Exists(x432).
Exists(x433).
Exists(x434).
Exists(x435).
Exists(x436).
Exists(x437).
Exists(x438).
Exists(x439).
Exists(x440).
Exists(x441).
Exists(x442).
Exists(x443).
Exists(x444).
Exists(x445).
Exists(x446).
Exists(x447).
Exists(x448).
Exists(x449).
Exists(x450).
Exists(x451).
Exists(x452).
Exists(x453).
Exists(x454).
Exists(x455).
Exists(x456).
Exists(x457).
Exists(x458).
Exists(x459).
Exists(x460).
Exists(x461).
Exists(x462).
Exists(x463).
Exists(x464).
Exists(x465).
Exists(x466).
Exists(x467).
Exists(x468).
Exists(x469).
Exists(x470).
Exists(x471).
Exists(x472).
Exists(x473).
Exists(x474).
Exists(x475).
Exists(x476).
Exists(x477).
Exists(x478).
Exists(x479).
Exists(x480).
Exists(x481).
Exists(x482).
Exists(x483).
Exists(x484).
Exists(x485).
Exists(x486).
Exists(x487).
Exists(x488).
Exists(x489).
Exists(x490).
Exists(x491).
Exists(x492).
Exists(x493).
Exists(x494).
Exists(x495).
Exists(x496).
Forall(y501).
Forall(y502).
Forall(y503).
Forall(y504).
Forall(y505).
Forall(y506).
Forall(y507).
Forall(y508).
Forall(y509).
Forall(y510).
Forall(y511).
Forall(y512).
Forall(y513).
Forall(y514).
Forall(y515).
Forall(y516).
Forall(y517).
Forall(y518).
Forall(y519).
Forall(y520).
Forall(y521).
Forall(y522).
Forall(y523).
Forall(y524).
Forall(y525).
Forall(y526).
Forall(y527).
Forall(y528).
Forall(y529).
Forall(y530).
Forall(y531).
Forall(y532).
Forall(y533).
Forall(y534).
Forall(y535).
Forall(y536).
Forall(y537).
Forall(y538).
Forall(y539).
Forall(y540).
Forall(y541).
Forall(y542).
Forall(y543).
Forall(y544).
Forall(y545).
Forall(y546).
Forall(y547).
Forall(y548).
Forall(y549).
Forall(y550).
Forall(y551).
Forall(y552).
Forall(y553).
Forall(y554).
Forall(y555).
Forall(y556).
Forall(y557).
Forall(y558).
Forall(y559).
Forall(y560).
Forall(y561).
Forall(y562).
Forall(y563).
Forall(y564).
Forall(y565).
Forall(y566).
Forall(y567).
Forall(y568).
Forall(y569).
Forall(y570).
Forall(y571).
Forall(y572).
Forall(y573).
Forall(y574).
Forall(y575).
Forall(y576).
Forall(y577).
Forall(y578).
Forall(y579).
Forall(y580).
Forall(y581).
Forall(y582).
Forall(y583).
Forall(y584).
Forall(y585).
Forall(y586).
Forall(y587).
Forall(y588).
Forall(y589).
Forall(y590).
Forall(y591).
Forall(y592).
Forall(y593).
Forall(y594).
Forall(y595).
Forall(y596).
Forall(y597).
Forall(y598).
Forall(y599).
Forall(y600).
Forall(y601).
Forall(y602).
Forall(y603).
Forall(y604).
Forall(y605).
Forall(y606).
Forall(y607).
Forall(y608).
Forall(y609).
Forall(y610).
Forall(y611).
Forall(y612).
Forall(y613).
Forall(y614).
Forall(y615).
Forall(y616).
Forall(y617).
Forall(y618).
Forall(y619).
Forall(y620).
Forall(y621).
Forall(y622).
Forall(y623).
Forall(y624).
Forall(y625).
Forall(y626).
Forall(y627).
Forall(y628).
Forall(y629).
Forall(y630).
Forall(y631).
Forall(y632).
Forall(y633).
Forall(y634).
Forall(y635).
Forall(y636).
Forall(y637).
Forall(y638).
Forall(y639).
Forall(y640).
Forall(y641).
Forall(y642).
Forall(y643).
Forall(y644).
Forall(y645).
Forall(y646).
Forall(y647).
Forall(y648).
Forall(y649).
Forall(y650).
Forall(y651).
Forall(y652).
Forall(y653).
Forall(y654).
Forall(y655).
Forall(y656).
Forall(y657).
Forall(y658).
Forall(y659).
Forall(y660).
Forall(y661).
Forall(y662).
Forall(y663).
Forall(y664).
Forall(y665).
Forall(y666).
Forall(y667).
Forall(y668).
Forall(y669).
Forall(y670).
Forall(y671).
Forall(y672).
Forall(y673).
Forall(y674).
Forall(y675).
Forall(y676).
Forall(y677).
Forall(y678).
Forall(y679).
Forall(y680).
Forall(y681).
Forall(y682).
Forall(y683).
Forall(y684).
Forall(y685).
Forall(y686).
Forall(y687).
Forall(y688).
Forall(y689).
Forall(y690).
Forall(y691).
Forall(y692).
Forall(y693).
Forall(y694).
Forall(y695).
Forall(y696).
Forall(y697).
Forall(y698).
Forall(y699).
Forall(y700).
Forall(y701).
Forall(y702).
Forall(y703).
Forall(y704).
Forall(y705).
Forall(y706).
Forall(y707).
Forall(y708).
Forall(y709).
Forall(y710).
Forall(y711).
Forall(y712).
Forall(y713).
Forall(y714).
Forall(y715).
Forall(y716).
Forall(y717).
Forall(y718).
Forall(y719).
Forall(y720).
Forall(y721).
Forall(y722).
Forall(y723).
Forall(y724).
Forall(y725).
Forall(y726).
Forall(y727).
Forall(y728).
Forall(y729).
Forall(y730).
Forall(y731).
Forall(y732).
Forall(y733).
Forall(y734).
Forall(y735).
Forall(y736).
Forall(y737).
Forall(y738).
Forall(y739).
Forall(y740).
Forall(y741).
Forall(y742).
Forall(y743).
Forall(y744).
Forall(y745).
Forall(y746).
Forall(y747).
Forall(y748).
Forall(y749).
Forall(y750).
Forall(y751).
Forall(y752).
Forall(y753).
Forall(y754).
Forall(y755).
Forall(y756).
Forall(y757).
Forall(y758).
Forall(y759).
Forall(y760).
Forall(y761).
Forall(y762).
Forall(y763).
Forall(y764).
Forall(y765).
Forall(y766).
Forall(y767).
Forall(y768).
Forall(y769).
Forall(y770).
Forall(y771).
Forall(y772).
Forall(y773).
Forall(y774).
Forall(y775).
Forall(y776).
Forall(y777).
Forall(y778).
Forall(y779).
Forall(y780).
Forall(y781).
Forall(y782).
Forall(y783).
Forall(y784).
Forall(y785).
Forall(y786).
Forall(y787).
Forall(y788).
Forall(y789).
Forall(y790).
Forall(y791).
Forall(y792).
Forall(y793).
Forall(y794).
Forall(y795).
Forall(y796).
Forall(y797).
Forall(y798).
Forall(y799).
Forall(y800).
Forall(y801).
Forall(y802).
Forall(y803).
Forall(y804).
Forall(y805).
Forall(y806).
Forall(y807).
Forall(y808).
Forall(y809).
Forall(y810).
Forall(y811).
Forall(y812).
Forall(y813).
Forall(y814).
Forall(y815).
Forall(y816).
Forall(y817).
Forall(y818).
Forall(y819).
Forall(y820).
Forall(y821).
Forall(y822).
Forall(y823).
Forall(y824).
Forall(y825).
Forall(y826).
Forall(y827).
Forall(y828).
Forall(y829).
Forall(y830).
Forall(y831).
Forall(y832).
Forall(y833).
Forall(y834).
Forall(y835).
Forall(y836).
Forall(y837).
Forall(y838).
Forall(y839).
Forall(y840).
Forall(y841).
Forall(y842).
Forall(y843).
Forall(y844).
Forall(y845).
Forall(y846).
Forall(y847).
Forall(y848).
Forall(y849).
Forall(y850).
Forall(y851).
Forall(y852).
Forall(y853).
Forall(y854).
Forall(y855).
Forall(y856).
Forall(y857).
Forall(y858).
Forall(y859).
Forall(y860).
Forall(y861).
Forall(y862).
Forall(y863).
Forall(y864).
Forall(y865).
Forall(y866).
Forall(y867).
Forall(y868).
Forall(y869).
Forall(y870).
Forall(y871).
Forall(y872).
Forall(y873).
Forall(y874).
Forall(y875).
Forall(y876).
Forall(y877).
Forall(y878).
Forall(y879).
Forall(y880).
Forall(y881).
Forall(y882).
Forall(y883).
Forall(y884).
Forall(y885).
Forall(y886).
Forall(y887).
Forall(y888).
Forall(y889).
Forall(y890).
Forall(y891).
Forall(y892).
Forall(y893).
Forall(y894).
Forall(y895).
Forall(y896).
Forall(y897).
Forall(y898).
Forall(y899).
Forall(y900).
Forall(y901).
Forall(y902).
Forall(y903).
Forall(y904).
Forall(y905).
Forall(y906).
Forall(y907).
Forall(y908).
Forall(y909).
Forall(y910).
Forall(y911).
Forall(y912).
Forall(y913).
Forall(y914).
Forall(y915).
Forall(y916).
Forall(y917).
Forall(y918).
Forall(y919).
Forall(y920).
Forall(y921).
Forall(y922).
Forall(y923).
Forall(y924).
Forall(y925).
Forall(y926).
Forall(y927).
Forall(y928).
Forall(y929).
Forall(y930).
Forall(y931).
Forall(y932).
Forall(y933).
Forall(y934).
Forall(y935).
Forall(y936).
Forall(y937).
Forall(y938).
Forall(y939).
Forall(y940).
Forall(y941).
Forall(y942).
Forall(y943).
Forall(y944).
Forall(y945).
Forall(y946).
Forall(y947).
Forall(y948).
Forall(y949).
Forall(y950).
Forall(y951).
Forall(y952).
Forall(y953).
Forall(y954).
Forall(y955).
Forall(y956).
Forall(y957).
Forall(y958).
Forall(y959).
Forall(y960).
Forall(y961).
Forall(y962).
Forall(y963).
Forall(y964).
Forall(y965).
Forall(y966).
Forall(y967).
Forall(y968).
Forall(y969).
Forall(y970).
Forall(y971).
Forall(y972).
Forall(y973).
Forall(y974).
Forall(y975).
Forall(y976).
Forall(y977).
Forall(y978).
Forall(y979).
Forall(y980).
Forall(y981).
Forall(y982).
Forall(y983).
Forall(y984).
Forall(y985).
Forall(y986).
Forall(y987).
Forall(y988).
Forall(y989).
Forall(y990).
Forall(y991).
Forall(y992).
Forall(y993).
Forall(y994).
Forall(y995).
Forall(y996).
Forall(y997).
Forall(y998).
Conjunct(true, true, x251, y543, y879, false).
Conjunct(x127, true, x157, false, y731, false).
Conjunct(x220, true, x71, false, y642, false).
Conjunct(x20, x176, y721, false, false, false).
Conjunct(true, y984, true, x386, false, y946).
Conjunct(true, true, x286, y794, x260, false).
Conjunct(y697, true, true, false, y869, x333).
Conjunct(x398, y971, true, false, false, y685).
Conjunct(true, true, y660, y735, x147, false).
Conjunct(true, true, true, y882, y885, x218).
Conjunct(x333, x111, y918, false, false, false).
Conjunct(true, x276, y667, x123, false, false).
Conjunct(x378, true, y968, false, y892, false).
Conjunct(true, true, true, y643, y982, y648).
Conjunct(true, true, true, y730, x11, y788).
Conjunct(x308, true, y876, false, x194, false).
Conjunct(y663, x225, true, false, false, y790).
Conjunct(true, x475, true, x495, false, y654).
Conjunct(x155, y696, true, false, false, y861).
Conjunct(y678, true, true, false, x136, x229).
Conjunct(true, x404, y916, y830, false, false).
Conjunct(true, x186, true, y805, false, x360).
Conjunct(true, x321, y536, x32, false, false).
Conjunct(x326, x350, true, false, false, y598).
Conjunct(x329, y771, y998, false, false, false).
Conjunct(true, x141, true, y541, false, x136).
Conjunct(true, true, x128, y691, y578, false).
Conjunct(x302, true, true, false, x47, y514).
Conjunct(y793, y856, x367, false, false, false).
Conjunct(true, true, true, x495, y857, x439).
Conjunct(y860, y647, true, false, false, x215).
Conjunct(x144, true, true, false, x212, y851).
Conjunct(y626, y957, y852, false, false, false).
Conjunct(true, true, true, x347, x463, y717).
Conjunct(true, x407, y552, x23, false, false).
Conjunct(true, y787, x226, x254, false, false).
Conjunct(x274, true, y684, false, x319, false).
Conjunct(x274, y707, x282, false, false, false).
Conjunct(true, x287, y673, x326, false, false).
Conjunct(true, y933, true, y911, false, y592).
Conjunct(y607, y738, x236, false, false, false).
Conjunct(true, true, true, x366, y617, x68).
Conjunct(true, true, true, x289, x38, y830).
Conjunct(x457, x37, true, false, false, y633).
Conjunct(y771, y693, y647, false, false, false).
Conjunct(y698, y968, true, false, false, x263).
Conjunct(x196, y634, y564, false, false, false).
Conjunct(true, true, true, y612, x416, x86).
Conjunct(true, true, true, x392, x72, y714).
Conjunct(y537, y967, true, false, false, y592).
Conjunct(true, true, x401, y779, x340, false).
Conjunct(x108, x409, y901, false, false, false).
Conjunct(true, true, true, y733, y808, y676).
Conjunct(true, true, y695, y721, x141, false).
Conjunct(x89, y668, y664, false, false, false).
Conjunct(x406, y908, x260, false, false, false).
Conjunct(true, true, true, x344, y598, x318).
Conjunct(true, true, y686, y555, x231, false).
Conjunct(true, x118, true, x306, false, y604).
Conjunct(true, x116, true, y699, false, x376).
Conjunct(x179, x423, true, false, false, y659).
Conjunct(x50, true, x316, false, y621, false).
Conjunct(true, y906, x229, y975, false, false).
Conjunct(true, true, y533, x145, x341, false).
Conjunct(x122, y833, x127, false, false, false).
Conjunct(true, y773, true, x372, false, x469).
Conjunct(y973, true, true, false, y702, x244).
Conjunct(y967, x405, y828, false, false, false).
Conjunct(true, x319, true, y949, false, x467).
Conjunct(x155, x302, true, false, false, y932).
Conjunct(x471, true, true, false, x401, y639).
Conjunct(y918, true, x422, false, x456, false).
Conjunct(true, true, x229, x410, y553, false).
Conjunct(x46, y607, y540, false, false, false).
Conjunct(true, y770, x364, y690, false, false).
Conjunct(y908, y847, x57, false, false, false).
Conjunct(true, true, y983, y654, x323, false).
Conjunct(y798, y833, true, false, false, y523).
Conjunct(y660, x493, true, false, false, y824).
Conjunct(x192, true, true, false, y506, y967).
Conjunct(y501, true, x486, false, y792, false).
Conjunct(true, true, true, y917, y641, x245).
Conjunct(true, true, y650, x33, x36, false).
Conjunct(true, y955, true, y926, false, x492).
Conjunct(x326, y718, true, false, false, x47).
Conjunct(true, true, true, x445, y604, x218).
Conjunct(x162, true, true, false, y673, y766).
Conjunct(y635, x328, x296, false, false, false).
Conjunct(true, true, true, x163, x94, y558).
Conjunct(y558, y948, true, false, false, x305).
Conjunct(y679, x96, true, false, false, x204).
Conjunct(y586, x73, true, false, false, y711).
Conjunct(true, true, y854, x93, y766, false).
Conjunct(x444, y521, x181, false, false, false).
Conjunct(x445, y978, true, false, false, x260).
Conjunct(true, true, x464, x393, y903, false).
Conjunct(true, y786, y921, y939, false, false).
Conjunct(true, y833, true, y771, false, x35).
Conjunct(x100, true, true, false, y902, y774).
Conjunct(y889, true, y776, false, y592, false).
Conjunct(x36, true, y694, false, x261, false).
Conjunct(x105, true, x72, false, y545, false).
Conjunct(true, true, true, y502, y579, x248).
Conjunct(true, true, x81, y832, x204, false).
Conjunct(y984, true, true, false, x419, x124).
Conjunct(true, true, true, x154, y712, x35).
Conjunct(x85, x430, true, false, false, y789).
Conjunct(x218, true, y603, false, x242, false).
Conjunct(true, true, x154, y900, y773, false).
Conjunct(true, y968, x62, y557, false, false).
Conjunct(true, x480, x291, y593, false, false).
Conjunct(x100, true, y577, false, x342, false).
Conjunct(y700, x55, x85, false, false, false).
Conjunct(true, y870, x90, x108, false, false).
Conjunct(true, true, true, y729, y685, y587).
Conjunct(y699, true, true, false, y727, y662).
Conjunct(y935, true, x123, false, x126, false).
Conjunct(y980, y866, y957, false, false, false).
Conjunct(true, true, x136, y523, x293, false).
Conjunct(x492, y725, true, false, false, y721).
Conjunct(x62, true, true, false, y977, x222).
Conjunct(true, true, true, x86, x69, y960).
Conjunct(true, true, y938, y515, x203, false).
Conjunct(x379, true, true, false, y733, y744).
Conjunct(true, true, y784, x246, y557, false).
Conjunct(y855, y646, true, false, false, x462).
Conjunct(true, y844, true, y876, false, y522).
Conjunct(y567, y922, y781, false, false, false).
Conjunct(y554, y655, true, false, false, x206).
Conjunct(true, x458, true, x413, false, y997).
Conjunct(y628, true, true, false, y692, x347).
Conjunct(y754, true, true, false, x486, y514).
Conjunct(true, true, x280, x438, y950, false).
Conjunct(true, true, true, y762, x312, y856).
Conjunct(true, true, true, x493, x244, y828).
Conjunct(true, true, y558, y616, x328, false).
Conjunct(y860, y902, true, false, false, y569).
Conjunct(true, true, y678, y734, y579, false).
Conjunct(true, y533, true, y744, false, y792).
Conjunct(y534, true, y710, false, x165, false).
Conjunct(true, y904, true, y846, false, x120).
Conjunct(x476, y655, y848, false, false, false).
Conjunct(x186, true, true, false, x394, y892).
Conjunct(true, true, true, y510, x169, y525).
Conjunct(true, true, true, x256, x353, y660).
Conjunct(true, true, true, x490, x107, y807).
Conjunct(x180, true, true, false, y628, x179).
Conjunct(true, y973, y865, y978, false, false).
Conjunct(true, true, y628, y792, y698, false).
Conjunct(y778, y611, true, false, false, y657).
Conjunct(true, y943, true, x224, false, y735).
Conjunct(x308, x93, true, false, false, y669).
Conjunct(x91, x86, true, false, false, y780).
Conjunct(y997, true, x57, false, y892, false).
Conjunct(true, true, true, y910, x237, y987).
Conjunct(true, true, true, y783, x355, y588).
Conjunct(true, true, true, y684, x326, y592).
Conjunct(y597, y714, true, false, false, y537).
Conjunct(x334, true, true, false, y563, y524).
Conjunct(y782, x414, true, false, false, x75).
Conjunct(x8, y692, x214, false, false, false).
Conjunct(x347, y912, x156, false, false, false).
Conjunct(true, true, true, x241, x98, y953).
Conjunct(x164, true, y591, false, x490, false).
Conjunct(true, true, y829, x145, x169, false).
Conjunct(true, true, y732, x405, x114, false).
Conjunct(true, true, true, y744, y789, y624).
Conjunct(true, y666, true, y960, false, y881).
Conjunct(true, true, y918, x304, x56, false).
Conjunct(y844, x267, true, false, false, x443).
Conjunct(y937, x69, true, false, false, y599).
Conjunct(y767, y755, y765, false, false, false).
Conjunct(y994, x274, true, false, false, x452).
Conjunct(x107, y915, x327, false, false, false).
Conjunct(x62, true, y835, false, x27, false).
Conjunct(y760, true, x376, false, y709, false).
Conjunct(y566, true, true, false, y530, y892).
Conjunct(true, true, true, x209, y930, y725).
Conjunct(true, true, y713, x142, x48, false).
Conjunct(y543, y776, true, false, false, x465).
Conjunct(true, x316, y956, x391, false, false).
Conjunct(true, y581, true, y827, false, x179).
Conjunct(true, true, true, y781, y541, y701).
Conjunct(true, y623, y656, x488, false, false).
Conjunct(y796, true, x439, false, y560, false).
Conjunct(x154, y998, true, false, false, y856).
Conjunct(true, true, y604, x254, y783, false).
Conjunct(true, true, true, x166, y562, y761).
Conjunct(x220, true, true, false, y928, y844).
Conjunct(x216, y958, true, false, false, x245).
Conjunct(true, true, x139, y924, y689, false).
Conjunct(y709, x394, true, false, false, y547).
Conjunct(true, true, y815, x485, y617, false).
Conjunct(true, true, true, y654, x258, y683).
Conjunct(y908, true, true, false, x146, x323).
Conjunct(true, true, y641, y830, x479, false).
Conjunct(y741, true, true, false, y838, y713).
Conjunct(x425, true, true, false, x168, y950).
Conjunct(x366, true, true, false, x214, y602).
Conjunct(y927, true, y845, false, x307, false).
Conjunct(true, true, y916, y707, y682, false).
Conjunct(true, x466, true, x63, false, y789).
Conjunct(y515, true, true, false, x291, x6).
Conjunct(true, x30, true, y679, false, y706).
Conjunct(true, x193, x274, y910, false, false).
Conjunct(true, x424, true, x80, false, y752).
Conjunct(true, x78, y912, x483, false, false).
Conjunct(true, true, true, x437, x152, y894).
Conjunct(x145, x123, y661, false, false, false).
Conjunct(x21, true, y821, false, x183, false).
Conjunct(y780, y694, true, false, false, x346).
Conjunct(true, x223, true, x313, false, y669).
Conjunct(true, true, true, y599, x425, x115).
Conjunct(x414, x340, true, false, false, y900).
Conjunct(true, y968, x8, x410, false, false).
Conjunct(true, x68, true, x67, false, y725).
Conjunct(true, x297, y547, y577, false, false).
Conjunct(x201, x361, true, false, false, y672).
Conjunct(y947, x130, x482, false, false, false).
Conjunct(true, x135, y901, y862, false, false).
Conjunct(true, y755, x210, y778, false, false).
Conjunct(y767, y689, true, false, false, x299).
Conjunct(true, true, y945, x104, x24, false).
Conjunct(x97, y941, x303, false, false, false).
Conjunct(x156, y547, x371, false, false, false).
Conjunct(true, true, y585, y658, y565, false).
Conjunct(y770, y737, x53, false, false, false).
Conjunct(true, x496, true, x75, false, y523).
Conjunct(y678, y944, y748, false, false, false).
Conjunct(x72, true, true, false, y752, x80).
Conjunct(x195, true, y842, false, y970, false).
Conjunct(x309, x335, true, false, false, y558).
Conjunct(true, y513, x282, y779, false, false).
Conjunct(true, x193, true, y779, false, y881).
Conjunct(true, y753, x116, y768, false, false).
Conjunct(true, true, y733, x159, x476, false).
Conjunct(true, true, x335, y620, x133, false).
Conjunct(x12, y673, y542, false, false, false).
Conjunct(y907, true, y974, false, y575, false).
Conjunct(true, y963, x9, x171, false, false).
Conjunct(true, y709, true, x97, false, y845).
Conjunct(true, true, true, y616, x67, x337).
Conjunct(true, y658, x420, x292, false, false).
Conjunct(y822, true, true, false, x120, y824).
Conjunct(true, true, x231, y797, y818, false).
Conjunct(true, y560, x467, x264, false, false).
Conjunct(true, true, y902, x199, x34, false).
Conjunct(x117, x301, y737, false, false, false).
Conjunct(x140, true, y589, false, x144, false).
Conjunct(true, true, true, y552, y681, y607).
Conjunct(y892, y675, x83, false, false, false).
Conjunct(y916, y578, x159, false, false, false).
Conjunct(y771, x264, x243, false, false, false).
Conjunct(true, true, y955, x424, x462, false).
Conjunct(y605, x442, true, false, false, y893).
Conjunct(true, x158, true, y857, false, y860).
Conjunct(x334, x460, true, false, false, y847).
Conjunct(true, true, y655, x417, x360, false).
Conjunct(x404, y772, true, false, false, x425).
Conjunct(x413, true, x201, false, y748, false).
Conjunct(true, true, true, y776, x186, x480).
Conjunct(x211, y833, true, false, false, y664).
Conjunct(y966, x175, y909, false, false, false).
Conjunct(x361, true, y920, false, x209, false).
Conjunct(y508, x163, true, false, false, y644).
Conjunct(true, y912, y724, y591, false, false).
Conjunct(y769, x288, x72, false, false, false).
Conjunct(x330, true, true, false, y706, x373).
Conjunct(true, true, true, x45, x268, y711).
Conjunct(true, y649, true, y886, false, x241).
Conjunct(true, y797, true, x158, false, x451).
Conjunct(y676, y978, y849, false, false, false).
Conjunct(y564, x289, true, false, false, y655).
Conjunct(true, x114, true, x217, false, y880).
Conjunct(x371, true, y702, false, y690, false).
Conjunct(true, x378, true, y838, false, y602).
Conjunct(x235, y889, x496, false, false, false).
Conjunct(true, y902, true, y885, false, y752).
Conjunct(x268, true, y888, false, x348, false).
Conjunct(x187, y926, true, false, false, x34).