problem.qdimacs

c [(1, f.positive.literal[1,1]), (2, f.negated.literal[1,1]), (3, a.positive.literal[1,1])]
c [(4, a.negated.literal[1,1]), (5, c.positive.literal[1,1]), (6, c.negated.literal[1,1])]
c [(7, e.positive.literal[1,1]), (8, e.negated.literal[1,1]), (9, b.positive.literal[1,1])]
c [(10, b.negated.literal[1,1]), (11, constant.positive.literal[1,1]), (12, constant.negated.literal[1,1])]
c [(13, f.positive.literal[1,2]), (14, f.negated.literal[1,2]), (15, a.positive.literal[1,2])]
c [(16, a.negated.literal[1,2]), (17, c.positive.literal[1,2]), (18, c.negated.literal[1,2])]
c [(19, e.positive.literal[1,2]), (20, e.negated.literal[1,2]), (21, b.positive.literal[1,2])]
c [(22, b.negated.literal[1,2]), (23, constant.positive.literal[1,2]), (24, constant.negated.literal[1,2])]
c [(25, f.positive.literal[1,3]), (26, f.negated.literal[1,3]), (27, a.positive.literal[1,3])]
c [(28, a.negated.literal[1,3]), (29, c.positive.literal[1,3]), (30, c.negated.literal[1,3])]
c [(31, e.positive.literal[1,3]), (32, e.negated.literal[1,3]), (33, b.positive.literal[1,3])]
c [(34, b.negated.literal[1,3]), (35, constant.positive.literal[1,3]), (36, constant.negated.literal[1,3])]
c [(37, f.positive.literal[2,1]), (38, f.negated.literal[2,1]), (39, a.positive.literal[2,1])]
c [(40, a.negated.literal[2,1]), (41, c.positive.literal[2,1]), (42, c.negated.literal[2,1])]
c [(43, e.positive.literal[2,1]), (44, e.negated.literal[2,1]), (45, b.positive.literal[2,1])]
c [(46, b.negated.literal[2,1]), (47, constant.positive.literal[2,1]), (48, constant.negated.literal[2,1])]
c [(49, f.positive.literal[2,2]), (50, f.negated.literal[2,2]), (51, a.positive.literal[2,2])]
c [(52, a.negated.literal[2,2]), (53, c.positive.literal[2,2]), (54, c.negated.literal[2,2])]
c [(55, e.positive.literal[2,2]), (56, e.negated.literal[2,2]), (57, b.positive.literal[2,2])]
c [(58, b.negated.literal[2,2]), (59, constant.positive.literal[2,2]), (60, constant.negated.literal[2,2])]
c [(61, f.positive.literal[2,3]), (62, f.negated.literal[2,3]), (63, a.positive.literal[2,3])]
c [(64, a.negated.literal[2,3]), (65, c.positive.literal[2,3]), (66, c.negated.literal[2,3])]
c [(67, e.positive.literal[2,3]), (68, e.negated.literal[2,3]), (69, b.positive.literal[2,3])]
c [(70, b.negated.literal[2,3]), (71, constant.positive.literal[2,3]), (72, constant.negated.literal[2,3])]
c [(73, f.positive.literal[3,1]), (74, f.negated.literal[3,1]), (75, a.positive.literal[3,1])]
c [(76, a.negated.literal[3,1]), (77, c.positive.literal[3,1]), (78, c.negated.literal[3,1])]
c [(79, e.positive.literal[3,1]), (80, e.negated.literal[3,1]), (81, b.positive.literal[3,1])]
c [(82, b.negated.literal[3,1]), (83, constant.positive.literal[3,1]), (84, constant.negated.literal[3,1])]
c [(85, f.positive.literal[3,2]), (86, f.negated.literal[3,2]), (87, a.positive.literal[3,2])]
c [(88, a.negated.literal[3,2]), (89, c.positive.literal[3,2]), (90, c.negated.literal[3,2])]
c [(91, e.positive.literal[3,2]), (92, e.negated.literal[3,2]), (93, b.positive.literal[3,2])]
c [(94, b.negated.literal[3,2]), (95, constant.positive.literal[3,2]), (96, constant.negated.literal[3,2])]
c [(97, f.positive.literal[3,3]), (98, f.negated.literal[3,3]), (99, a.positive.literal[3,3])]
c [(100, a.negated.literal[3,3]), (101, c.positive.literal[3,3]), (102, c.negated.literal[3,3])]
c [(103, e.positive.literal[3,3]), (104, e.negated.literal[3,3]), (105, b.positive.literal[3,3])]
c [(106, b.negated.literal[3,3]), (107, constant.positive.literal[3,3]), (108, constant.negated.literal[3,3])]
c [(109, f), (110, a), (111, c)]
c [(112, e), (113, b), (114, constant)]
c [(115, sinz[1,633]), (116, sinz[11,633]), (117, sinz[2,633])]
c [(118, sinz[3,633]), (119, sinz[4,633]), (120, sinz[5,633])]
c [(121, sinz[6,633]), (122, sinz[7,633]), (123, sinz[8,633])]
c [(124, sinz[9,633]), (125, sinz[10,633]), (126, sinz[1,634])]
c [(127, sinz[11,634]), (128, sinz[2,634]), (129, sinz[3,634])]
c [(130, sinz[4,634]), (131, sinz[5,634]), (132, sinz[6,634])]
c [(133, sinz[7,634]), (134, sinz[8,634]), (135, sinz[9,634])]
c [(136, sinz[10,634]), (137, sinz[1,635]), (138, sinz[11,635])]
c [(139, sinz[2,635]), (140, sinz[3,635]), (141, sinz[4,635])]
c [(142, sinz[5,635]), (143, sinz[6,635]), (144, sinz[7,635])]
c [(145, sinz[8,635]), (146, sinz[9,635]), (147, sinz[10,635])]
c [(148, sinz[1,636]), (149, sinz[11,636]), (150, sinz[2,636])]
c [(151, sinz[3,636]), (152, sinz[4,636]), (153, sinz[5,636])]
c [(154, sinz[6,636]), (155, sinz[7,636]), (156, sinz[8,636])]
c [(157, sinz[9,636]), (158, sinz[10,636]), (159, sinz[1,637])]
c [(160, sinz[11,637]), (161, sinz[2,637]), (162, sinz[3,637])]
c [(163, sinz[4,637]), (164, sinz[5,637]), (165, sinz[6,637])]
c [(166, sinz[7,637]), (167, sinz[8,637]), (168, sinz[9,637])]
c [(169, sinz[10,637]), (170, sinz[1,638]), (171, sinz[11,638])]
c [(172, sinz[2,638]), (173, sinz[3,638]), (174, sinz[4,638])]
c [(175, sinz[5,638]), (176, sinz[6,638]), (177, sinz[7,638])]
c [(178, sinz[8,638]), (179, sinz[9,638]), (180, sinz[10,638])]
c [(181, sinz[1,639]), (182, sinz[11,639]), (183, sinz[2,639])]
c [(184, sinz[3,639]), (185, sinz[4,639]), (186, sinz[5,639])]
c [(187, sinz[6,639]), (188, sinz[7,639]), (189, sinz[8,639])]
c [(190, sinz[9,639]), (191, sinz[10,639]), (192, sinz[1,640])]
c [(193, sinz[11,640]), (194, sinz[2,640]), (195, sinz[3,640])]
c [(196, sinz[4,640]), (197, sinz[5,640]), (198, sinz[6,640])]
c [(199, sinz[7,640]), (200, sinz[8,640]), (201, sinz[9,640])]
c [(202, sinz[10,640]), (203, sinz[1,641]), (204, sinz[11,641])]
c [(205, sinz[2,641]), (206, sinz[3,641]), (207, sinz[4,641])]
c [(208, sinz[5,641]), (209, sinz[6,641]), (210, sinz[7,641])]
c [(211, sinz[8,641]), (212, sinz[9,641]), (213, sinz[10,641])]
c [(214, on_path.synth[3684]), (215, on_path.synth[3685]), (216, on_path.synth[3686])]
c [(217, on_path.synth[3687]), (218, on_path.synth[3688]), (219, on_path.synth[3689])]
c [(220, path[1,1]), (221, on_path.synth[3690]), (222, on_path.synth[3691])]
c [(223, on_path.synth[3692]), (224, on_path.synth[3693]), (225, on_path.synth[3694])]
c [(226, on_path.synth[3695]), (227, path[1,2]), (228, on_path.synth[3696])]
c [(229, on_path.synth[3697]), (230, on_path.synth[3698]), (231, on_path.synth[3699])]
c [(232, on_path.synth[3700]), (233, on_path.synth[3701]), (234, path[1,3])]
c [(235, on_path.synth[3702]), (236, on_path.synth[3703]), (237, on_path.synth[3704])]
c [(238, on_path.synth[3705]), (239, on_path.synth[3706]), (240, on_path.synth[3707])]
c [(241, path[2,1]), (242, on_path.synth[3708]), (243, on_path.synth[3709])]
c [(244, on_path.synth[3710]), (245, on_path.synth[3711]), (246, on_path.synth[3712])]
c [(247, on_path.synth[3713]), (248, path[2,2]), (249, on_path.synth[3714])]
c [(250, on_path.synth[3715]), (251, on_path.synth[3716]), (252, on_path.synth[3717])]
c [(253, on_path.synth[3718]), (254, on_path.synth[3719]), (255, path[2,3])]
c [(256, on_path.synth[3720]), (257, on_path.synth[3721]), (258, on_path.synth[3722])]
c [(259, on_path.synth[3723]), (260, on_path.synth[3724]), (261, on_path.synth[3725])]
c [(262, path[3,1]), (263, on_path.synth[3726]), (264, on_path.synth[3727])]
c [(265, on_path.synth[3728]), (266, on_path.synth[3729]), (267, on_path.synth[3730])]
c [(268, on_path.synth[3731]), (269, path[3,2]), (270, on_path.synth[3732])]
c [(271, on_path.synth[3733]), (272, on_path.synth[3734]), (273, on_path.synth[3735])]
c [(274, on_path.synth[3736]), (275, on_path.synth[3737]), (276, path[3,3])]
c [(277, sinz[1,642]), (278, sinz[2,642]), (279, sinz[1,643])]
c [(280, sinz[2,643]), (281, hm_c.cardnet[2,8894]), (282, hm_c.cardnet[1,8893])]
c [(283, a.cardnet[1,8892]), (284, hm_c.cardnet[2,8896]), (285, hm_c.cardnet[1,8895])]
c [(286, hm_c.cardnet[2,8898]), (287, hm_c.cardnet[1,8897]), (288, hm_c.cardnet[2,8900])]
c [(289, hm_c.cardnet[1,8899]), (290, hm_c.cardnet[3,8903]), (291, hm_c.cardnet[2,8902])]
c [(292, equals_two.synth[3738]), (293, hm_c.cardnet[2,8908]), (294, hm_c.cardnet[1,8907])]
c [(295, a.cardnet[1,8906]), (296, hm_c.cardnet[2,8910]), (297, hm_c.cardnet[1,8909])]
c [(298, sm_c.cardnet[1,8912]), (299, sm_c.cardnet[1,8911]), (300, sm_c.cardnet[1,8914])]
c [(301, sm_c.cardnet[1,8913]), (302, sm_c.cardnet[3,8917]), (303, sm_c.cardnet[2,8916])]
c [(304, hm_c.cardnet[2,8919]), (305, hm_c.cardnet[1,8918]), (306, hm_c.cardnet[2,8921])]
c [(307, hm_c.cardnet[1,8920]), (308, hm_c.cardnet[2,8923]), (309, hm_c.cardnet[1,8922])]
c [(310, hm_c.cardnet[2,8925]), (311, hm_c.cardnet[1,8924]), (312, hm_c.cardnet[3,8928])]
c [(313, hm_c.cardnet[2,8927]), (314, equals_two.synth[3739]), (315, hm_c.cardnet[2,8932])]
c [(316, hm_c.cardnet[1,8931]), (317, hm_c.cardnet[2,8934]), (318, hm_c.cardnet[1,8933])]
c [(319, hm_c.cardnet[2,8936]), (320, hm_c.cardnet[1,8935]), (321, hm_c.cardnet[2,8938])]
c [(322, hm_c.cardnet[1,8937]), (323, hm_c.cardnet[3,8941]), (324, hm_c.cardnet[2,8940])]
c [(325, hm_c.cardnet[2,8946]), (326, hm_c.cardnet[1,8945]), (327, a.cardnet[1,8944])]
c [(328, hm_c.cardnet[2,8948]), (329, hm_c.cardnet[1,8947]), (330, hm_c.cardnet[2,8950])]
c [(331, hm_c.cardnet[1,8949]), (332, hm_c.cardnet[2,8952]), (333, hm_c.cardnet[1,8951])]
c [(334, hm_c.cardnet[3,8955]), (335, hm_c.cardnet[2,8954]), (336, equals_two.synth[3740])]
c [(337, hm_c.cardnet[2,8960]), (338, hm_c.cardnet[1,8959]), (339, a.cardnet[1,8958])]
c [(340, hm_c.cardnet[2,8962]), (341, hm_c.cardnet[1,8961]), (342, sm_c.cardnet[1,8964])]
c [(343, sm_c.cardnet[1,8963]), (344, sm_c.cardnet[1,8966]), (345, sm_c.cardnet[1,8965])]
c [(346, sm_c.cardnet[3,8969]), (347, sm_c.cardnet[2,8968]), (348, on_neg_path.synth[3741])]
c [(349, on_neg_path.synth[3742]), (350, on_neg_path.synth[3743]), (351, on_neg_path.synth[3744])]
c [(352, on_neg_path.synth[3745]), (353, on_neg_path.synth[3746]), (354, negative.path[1,1])]
c [(355, on_neg_path.synth[3747]), (356, on_neg_path.synth[3748]), (357, on_neg_path.synth[3749])]
c [(358, on_neg_path.synth[3750]), (359, on_neg_path.synth[3751]), (360, on_neg_path.synth[3752])]
c [(361, negative.path[1,2]), (362, on_neg_path.synth[3753]), (363, on_neg_path.synth[3754])]
c [(364, on_neg_path.synth[3755]), (365, on_neg_path.synth[3756]), (366, on_neg_path.synth[3757])]
c [(367, on_neg_path.synth[3758]), (368, negative.path[1,3]), (369, on_neg_path.synth[3759])]
c [(370, on_neg_path.synth[3760]), (371, on_neg_path.synth[3761]), (372, on_neg_path.synth[3762])]
c [(373, on_neg_path.synth[3763]), (374, on_neg_path.synth[3764]), (375, negative.path[2,1])]
c [(376, on_neg_path.synth[3765]), (377, on_neg_path.synth[3766]), (378, on_neg_path.synth[3767])]
c [(379, on_neg_path.synth[3768]), (380, on_neg_path.synth[3769]), (381, on_neg_path.synth[3770])]
c [(382, negative.path[2,2]), (383, on_neg_path.synth[3771]), (384, on_neg_path.synth[3772])]
c [(385, on_neg_path.synth[3773]), (386, on_neg_path.synth[3774]), (387, on_neg_path.synth[3775])]
c [(388, on_neg_path.synth[3776]), (389, negative.path[2,3]), (390, on_neg_path.synth[3777])]
c [(391, on_neg_path.synth[3778]), (392, on_neg_path.synth[3779]), (393, on_neg_path.synth[3780])]
c [(394, on_neg_path.synth[3781]), (395, on_neg_path.synth[3782]), (396, negative.path[3,1])]
c [(397, on_neg_path.synth[3783]), (398, on_neg_path.synth[3784]), (399, on_neg_path.synth[3785])]
c [(400, on_neg_path.synth[3786]), (401, on_neg_path.synth[3787]), (402, on_neg_path.synth[3788])]
c [(403, negative.path[3,2]), (404, on_neg_path.synth[3789]), (405, on_neg_path.synth[3790])]
c [(406, on_neg_path.synth[3791]), (407, on_neg_path.synth[3792]), (408, on_neg_path.synth[3793])]
c [(409, on_neg_path.synth[3794]), (410, negative.path[3,3]), (411, sinz[1,644])]
c [(412, sinz[2,644]), (413, sinz[1,645]), (414, sinz[2,645])]
c [(415, hm_c.cardnet[2,8971]), (416, hm_c.cardnet[1,8970]), (417, equals_one.synth[3795])]
c [(418, hm_c.cardnet[2,8973]), (419, hm_c.cardnet[1,8972]), (420, hm_c.cardnet[2,8975])]
c [(421, hm_c.cardnet[1,8974]), (422, equals_one.synth[3796]), (423, hm_c.cardnet[2,8977])]
c [(424, hm_c.cardnet[1,8976]), (425, hm_c.cardnet[2,8982]), (426, hm_c.cardnet[1,8981])]
c [(427, hm_c.cardnet[2,8984]), (428, hm_c.cardnet[1,8983]), (429, hm_c.cardnet[2,8986])]
c [(430, hm_c.cardnet[1,8985]), (431, hm_c.cardnet[2,8988]), (432, hm_c.cardnet[1,8987])]
c [(433, hm_c.cardnet[3,8991]), (434, hm_c.cardnet[2,8990]), (435, a.cardnet[1,8978])]
c [(436, hm_c.cardnet[2,8995]), (437, hm_c.cardnet[1,8994]), (438, a.cardnet[2,8979])]
c [(439, a.cardnet[3,8980]), (440, hm_c.cardnet[2,8997]), (441, hm_c.cardnet[1,8996])]
c [(442, hm_c.cardnet[2,8999]), (443, hm_c.cardnet[1,8998]), (444, hm_c.cardnet[2,9001])]
c [(445, hm_c.cardnet[1,9000]), (446, hm_c.cardnet[3,9004]), (447, hm_c.cardnet[2,9003])]
c [(448, sm_c.cardnet[1,9008]), (449, sm_c.cardnet[1,9007]), (450, sm_c.cardnet[1,9010])]
c [(451, sm_c.cardnet[1,9009]), (452, sm_c.cardnet[3,9013]), (453, sm_c.cardnet[2,9012])]
c [(454, sm_c.cardnet[1,9015]), (455, sm_c.cardnet[1,9014]), (456, sm_c.cardnet[1,9017])]
c [(457, sm_c.cardnet[1,9016]), (458, sm_c.cardnet[3,9020]), (459, sm_c.cardnet[2,9019])]
c [(460, sm_c.cardnet[3,9023]), (461, sm_c.cardnet[2,9022]), (462, sm_c.cardnet[5,9025])]
c [(463, sm_c.cardnet[4,9024]), (464, equals_two.synth[3797]), (465, hm_c.cardnet[2,9030])]
c [(466, hm_c.cardnet[1,9029]), (467, hm_c.cardnet[2,9032]), (468, hm_c.cardnet[1,9031])]
c [(469, hm_c.cardnet[2,9034]), (470, hm_c.cardnet[1,9033]), (471, hm_c.cardnet[2,9036])]
c [(472, hm_c.cardnet[1,9035]), (473, hm_c.cardnet[3,9039]), (474, hm_c.cardnet[2,9038])]
c [(475, a.cardnet[1,9026]), (476, hm_c.cardnet[2,9043]), (477, hm_c.cardnet[1,9042])]
c [(478, a.cardnet[2,9027]), (479, a.cardnet[3,9028]), (480, hm_c.cardnet[2,9045])]
c [(481, hm_c.cardnet[1,9044]), (482, hm_c.cardnet[2,9047]), (483, hm_c.cardnet[1,9046])]
c [(484, hm_c.cardnet[2,9049]), (485, hm_c.cardnet[1,9048]), (486, hm_c.cardnet[3,9052])]
c [(487, hm_c.cardnet[2,9051]), (488, sm_c.cardnet[1,9056]), (489, sm_c.cardnet[1,9055])]
c [(490, sm_c.cardnet[1,9058]), (491, sm_c.cardnet[1,9057]), (492, sm_c.cardnet[3,9061])]
c [(493, sm_c.cardnet[2,9060]), (494, sm_c.cardnet[1,9063]), (495, sm_c.cardnet[1,9062])]
c [(496, sm_c.cardnet[1,9065]), (497, sm_c.cardnet[1,9064]), (498, sm_c.cardnet[3,9068])]
c [(499, sm_c.cardnet[2,9067]), (500, sm_c.cardnet[3,9071]), (501, sm_c.cardnet[2,9070])]
c [(502, sm_c.cardnet[5,9073]), (503, sm_c.cardnet[4,9072]), (504, hm_c.cardnet[2,9076])]
c [(505, hm_c.cardnet[1,9075]), (506, a.cardnet[1,9074]), (507, hm_c.cardnet[2,9078])]
c [(508, hm_c.cardnet[1,9077]), (509, sm_c.cardnet[1,9080]), (510, sm_c.cardnet[1,9079])]
c [(511, sm_c.cardnet[1,9082]), (512, sm_c.cardnet[1,9081]), (513, sm_c.cardnet[3,9085])]
c [(514, sm_c.cardnet[2,9084]), (515, equals_one.synth[3798]), (516, hm_c.cardnet[2,9088])]
c [(517, hm_c.cardnet[1,9087]), (518, a.cardnet[1,9086]), (519, hm_c.cardnet[2,9090])]
c [(520, hm_c.cardnet[1,9089]), (521, hm_c.cardnet[2,9092]), (522, hm_c.cardnet[1,9091])]
c [(523, hm_c.cardnet[2,9094]), (524, hm_c.cardnet[1,9093]), (525, hm_c.cardnet[3,9097])]
c [(526, hm_c.cardnet[2,9096]), (527, hm_c.cardnet[2,9102]), (528, hm_c.cardnet[1,9101])]
c [(529, a.cardnet[1,9100]), (530, hm_c.cardnet[2,9104]), (531, hm_c.cardnet[1,9103])]
c [(532, sm_c.cardnet[1,9106]), (533, sm_c.cardnet[1,9105]), (534, sm_c.cardnet[1,9108])]
c [(535, sm_c.cardnet[1,9107]), (536, sm_c.cardnet[3,9111]), (537, sm_c.cardnet[2,9110])]
c [(538, equals_one.synth[3799]), (539, hm_c.cardnet[2,9114]), (540, hm_c.cardnet[1,9113])]
c [(541, a.cardnet[1,9112]), (542, hm_c.cardnet[2,9116]), (543, hm_c.cardnet[1,9115])]
c [(544, hm_c.cardnet[2,9118]), (545, hm_c.cardnet[1,9117]), (546, hm_c.cardnet[2,9120])]
c [(547, hm_c.cardnet[1,9119]), (548, hm_c.cardnet[3,9123]), (549, hm_c.cardnet[2,9122])]
c [(550, hm_c.cardnet[2,9127]), (551, hm_c.cardnet[1,9126]), (552, hm_c.cardnet[2,9129])]
c [(553, hm_c.cardnet[1,9128]), (554, hm_c.cardnet[2,9131]), (555, hm_c.cardnet[1,9130])]
c [(556, hm_c.cardnet[2,9133]), (557, hm_c.cardnet[1,9132]), (558, hm_c.cardnet[3,9136])]
c [(559, hm_c.cardnet[2,9135]), (560, hm_c.cardnet[2,9140]), (561, hm_c.cardnet[1,9139])]
c [(562, hm_c.cardnet[2,9142]), (563, hm_c.cardnet[1,9141]), (564, hm_c.cardnet[2,9144])]
c [(565, hm_c.cardnet[1,9143]), (566, hm_c.cardnet[2,9146]), (567, hm_c.cardnet[1,9145])]
c [(568, hm_c.cardnet[3,9149]), (569, hm_c.cardnet[2,9148]), (570, sm_c.cardnet[1,9153])]
c [(571, sm_c.cardnet[1,9152]), (572, sm_c.cardnet[1,9155]), (573, sm_c.cardnet[1,9154])]
c [(574, sm_c.cardnet[3,9158]), (575, sm_c.cardnet[2,9157]), (576, sm_c.cardnet[1,9160])]
c [(577, sm_c.cardnet[1,9159]), (578, sm_c.cardnet[1,9162]), (579, sm_c.cardnet[1,9161])]
c [(580, sm_c.cardnet[3,9165]), (581, sm_c.cardnet[2,9164]), (582, sm_c.cardnet[3,9168])]
c [(583, sm_c.cardnet[2,9167]), (584, sm_c.cardnet[5,9170]), (585, sm_c.cardnet[4,9169])]
c [(586, equals_two.synth[3800]), (587, hm_c.cardnet[2,9172]), (588, hm_c.cardnet[1,9171])]
c [(589, hm_c.cardnet[2,9174]), (590, hm_c.cardnet[1,9173]), (591, hm_c.cardnet[2,9176])]
c [(592, hm_c.cardnet[1,9175]), (593, hm_c.cardnet[2,9178]), (594, hm_c.cardnet[1,9177])]
c [(595, hm_c.cardnet[3,9181]), (596, hm_c.cardnet[2,9180]), (597, hm_c.cardnet[2,9185])]
c [(598, hm_c.cardnet[1,9184]), (599, hm_c.cardnet[2,9187]), (600, hm_c.cardnet[1,9186])]
c [(601, hm_c.cardnet[2,9189]), (602, hm_c.cardnet[1,9188]), (603, hm_c.cardnet[2,9191])]
c [(604, hm_c.cardnet[1,9190]), (605, hm_c.cardnet[3,9194]), (606, hm_c.cardnet[2,9193])]
c [(607, hm_c.cardnet[2,9198]), (608, hm_c.cardnet[1,9197]), (609, hm_c.cardnet[2,9200])]
c [(610, hm_c.cardnet[1,9199]), (611, hm_c.cardnet[3,9203]), (612, hm_c.cardnet[2,9202])]
c [(613, hm_c.cardnet[2,9207]), (614, hm_c.cardnet[1,9206]), (615, hm_c.cardnet[2,9209])]
c [(616, hm_c.cardnet[1,9208]), (617, hm_c.cardnet[3,9212]), (618, hm_c.cardnet[2,9211])]
c [(619, hm_c.cardnet[3,9217]), (620, hm_c.cardnet[2,9216]), (621, hm_c.cardnet[5,9219])]
c [(622, hm_c.cardnet[4,9218]), (623, hm_c.cardnet[7,9221]), (624, hm_c.cardnet[6,9220])]
c [(625, hm_c.cardnet[2,9225]), (626, hm_c.cardnet[1,9224]), (627, equals_one.synth[3801])]
c [(628, hm_c.cardnet[2,9227]), (629, hm_c.cardnet[1,9226]), (630, hm_c.cardnet[2,9229])]
c [(631, hm_c.cardnet[1,9228]), (632, equals_one.synth[3802]), (633, hm_c.cardnet[2,9231])]
c [(634, hm_c.cardnet[1,9230]), (635, hm_c.cardnet[2,9236]), (636, hm_c.cardnet[1,9235])]
c [(637, hm_c.cardnet[2,9238]), (638, hm_c.cardnet[1,9237]), (639, hm_c.cardnet[2,9240])]
c [(640, hm_c.cardnet[1,9239]), (641, hm_c.cardnet[2,9242]), (642, hm_c.cardnet[1,9241])]
c [(643, hm_c.cardnet[3,9245]), (644, hm_c.cardnet[2,9244]), (645, a.cardnet[1,9232])]
c [(646, hm_c.cardnet[2,9249]), (647, hm_c.cardnet[1,9248]), (648, a.cardnet[2,9233])]
c [(649, a.cardnet[3,9234]), (650, hm_c.cardnet[2,9251]), (651, hm_c.cardnet[1,9250])]
c [(652, hm_c.cardnet[2,9253]), (653, hm_c.cardnet[1,9252]), (654, hm_c.cardnet[2,9255])]
c [(655, hm_c.cardnet[1,9254]), (656, hm_c.cardnet[3,9258]), (657, hm_c.cardnet[2,9257])]
c [(658, sm_c.cardnet[1,9262]), (659, sm_c.cardnet[1,9261]), (660, sm_c.cardnet[1,9264])]
c [(661, sm_c.cardnet[1,9263]), (662, sm_c.cardnet[3,9267]), (663, sm_c.cardnet[2,9266])]
c [(664, sm_c.cardnet[1,9269]), (665, sm_c.cardnet[1,9268]), (666, sm_c.cardnet[1,9271])]
c [(667, sm_c.cardnet[1,9270]), (668, sm_c.cardnet[3,9274]), (669, sm_c.cardnet[2,9273])]
c [(670, sm_c.cardnet[3,9277]), (671, sm_c.cardnet[2,9276]), (672, sm_c.cardnet[5,9279])]
c [(673, sm_c.cardnet[4,9278]), (674, equals_two.synth[3803]), (675, hm_c.cardnet[2,9284])]
c [(676, hm_c.cardnet[1,9283]), (677, hm_c.cardnet[2,9286]), (678, hm_c.cardnet[1,9285])]
c [(679, hm_c.cardnet[2,9288]), (680, hm_c.cardnet[1,9287]), (681, hm_c.cardnet[2,9290])]
c [(682, hm_c.cardnet[1,9289]), (683, hm_c.cardnet[3,9293]), (684, hm_c.cardnet[2,9292])]
c [(685, a.cardnet[1,9280]), (686, hm_c.cardnet[2,9297]), (687, hm_c.cardnet[1,9296])]
c [(688, a.cardnet[2,9281]), (689, a.cardnet[3,9282]), (690, hm_c.cardnet[2,9299])]
c [(691, hm_c.cardnet[1,9298]), (692, hm_c.cardnet[2,9301]), (693, hm_c.cardnet[1,9300])]
c [(694, hm_c.cardnet[2,9303]), (695, hm_c.cardnet[1,9302]), (696, hm_c.cardnet[3,9306])]
c [(697, hm_c.cardnet[2,9305]), (698, sm_c.cardnet[1,9310]), (699, sm_c.cardnet[1,9309])]
c [(700, sm_c.cardnet[1,9312]), (701, sm_c.cardnet[1,9311]), (702, sm_c.cardnet[3,9315])]
c [(703, sm_c.cardnet[2,9314]), (704, sm_c.cardnet[1,9317]), (705, sm_c.cardnet[1,9316])]
c [(706, sm_c.cardnet[1,9319]), (707, sm_c.cardnet[1,9318]), (708, sm_c.cardnet[3,9322])]
c [(709, sm_c.cardnet[2,9321]), (710, sm_c.cardnet[3,9325]), (711, sm_c.cardnet[2,9324])]
c [(712, sm_c.cardnet[5,9327]), (713, sm_c.cardnet[4,9326])]
p cnf 713 1233
e 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 0
a 109 110 111 112 113 0
e 170 571 171 570 573 172 572 173 575 574 174 577 175 576 579 176 578 177 581 178 580 590 179 583 180 582 585 181 584 587 182 588 183 184 185 186 187 133 310 464 225 419 480 134 483 418 482 226 227 313 422 135 485 312 228 421 230 484 136 420 487 235 137 316 475 424 486 229 138 423 315 231 435 139 438 489 318 232 439 140 488 317 426 491 320 233 141 425 490 319 234 237 322 428 142 493 321 427 492 242 143 506 324 430 236 495 323 144 429 494 497 238 432 145 327 496 431 239 146 499 498 240 434 147 433 244 336 148 326 501 325 500 149 329 503 243 328 502 437 150 331 515 330 436 245 333 151 188 246 461 460 189 389 247 463 462 190 249 251 479 191 256 192 250 193 252 194 220 253 195 254 196 258 466 197 478 241 263 465 198 257 468 467 199 470 259 262 469 200 472 260 471 201 261 474 403 202 473 265 203 354 204 264 477 205 476 266 481 548 625 632 357 701 267 614 376 631 700 362 613 278 630 268 551 616 356 703 615 270 634 702 272 633 358 618 689 705 617 550 645 704 359 271 648 707 553 649 706 360 552 636 273 269 555 635 709 364 620 554 638 708 274 619 557 637 369 622 556 640 275 621 363 639 711 624 559 642 710 623 558 641 713 365 277 712 644 366 626 643 279 627 367 280 561 560 371 563 292 276 382 562 647 283 565 646 282 370 564 651 281 567 650 566 653 285 372 652 284 569 373 655 568 654 287 374 629 286 657 628 656 289 399 129 288 412 130 404 131 398 291 132 290 400 128 401 295 402 406 294 396 293 297 405 115 296 116 299 407 298 117 301 408 300 118 361 409 119 303 302 120 305 121 411 122 413 123 414 124 314 304 125 307 306 417 126 309 127 416 308 415 311 368 332 375 525 152 335 529 153 676 334 154 675 678 155 339 677 680 538 156 528 679 527 682 157 338 531 681 530 158 337 533 684 341 532 683 159 340 535 160 343 534 342 161 345 537 344 536 687 162 686 347 586 691 163 346 690 348 693 355 164 692 540 695 541 165 694 539 543 166 697 542 349 696 350 545 167 544 351 547 168 546 352 169 699 353 549 698 441 440 443 442 445 248 444 447 504 446 508 507 510 509 449 512 511 448 451 514 513 450 255 518 453 452 505 517 455 454 516 520 457 519 456 522 521 524 459 523 458 526 378 589 206 592 397 383 591 207 594 377 593 208 659 410 658 379 596 209 661 595 660 380 210 663 381 211 662 674 385 598 114 212 665 597 664 390 600 213 599 667 384 602 214 666 601 386 604 216 221 603 669 387 668 215 606 688 388 605 217 671 392 670 218 673 672 219 608 391 685 607 223 610 393 609 394 612 222 611 395 224 0
114 0
-1 115 0
-12 -116 0
-2 117 0
-115 117 0
-2 -115 0
-3 118 0
-117 118 0
-3 -117 0
-4 119 0
-118 119 0
-4 -118 0
-5 120 0
-119 120 0
-5 -119 0
-6 121 0
-120 121 0
-6 -120 0
-7 122 0
-121 122 0
-7 -121 0
-8 123 0
-122 123 0
-8 -122 0
-9 124 0
-123 124 0
-9 -123 0
-10 125 0
-124 125 0
-10 -124 0
-11 116 0
116 -125 0
-11 -125 0
3 4 9 10 11 12 5 6 1 2 7 8 0
-13 126 0
-24 -127 0
-14 128 0
-126 128 0
-14 -126 0
-15 129 0
-128 129 0
-15 -128 0
-16 130 0
-129 130 0
-16 -129 0
-17 131 0
-130 131 0
-17 -130 0
-18 132 0
-131 132 0
-18 -131 0
-19 133 0
-132 133 0
-19 -132 0
-20 134 0
-133 134 0
-20 -133 0
-21 135 0
-134 135 0
-21 -134 0
-22 136 0
-135 136 0
-22 -135 0
-23 127 0
127 -136 0
-23 -136 0
13 14 17 18 15 16 21 22 23 24 19 20 0
-25 137 0
-36 -138 0
-26 139 0
-137 139 0
-26 -137 0
-27 140 0
-139 140 0
-27 -139 0
-28 141 0
-140 141 0
-28 -140 0
-29 142 0
-141 142 0
-29 -141 0
-30 143 0
-142 143 0
-30 -142 0
-31 144 0
-143 144 0
-31 -143 0
-32 145 0
-144 145 0
-32 -144 0
-33 146 0
-145 146 0
-33 -145 0
-34 147 0
-146 147 0
-34 -146 0
-35 138 0
138 -147 0
-35 -147 0
25 26 29 30 27 28 33 34 35 36 31 32 0
-37 148 0
-48 -149 0
-38 150 0
-148 150 0
-38 -148 0
-39 151 0
-150 151 0
-39 -150 0
-40 152 0
-151 152 0
-40 -151 0
-41 153 0
-152 153 0
-41 -152 0
-42 154 0
-153 154 0
-42 -153 0
-43 155 0
-154 155 0
-43 -154 0
-44 156 0
-155 156 0
-44 -155 0
-45 157 0
-156 157 0
-45 -156 0
-46 158 0
-157 158 0
-46 -157 0
-47 149 0
149 -158 0
-47 -158 0
39 40 45 46 47 48 41 42 37 38 43 44 0
-49 159 0
-60 -160 0
-50 161 0
-159 161 0
-50 -159 0
-51 162 0
-161 162 0
-51 -161 0
-52 163 0
-162 163 0
-52 -162 0
-53 164 0
-163 164 0
-53 -163 0
-54 165 0
-164 165 0
-54 -164 0
-55 166 0
-165 166 0
-55 -165 0
-56 167 0
-166 167 0
-56 -166 0
-57 168 0
-167 168 0
-57 -167 0
-58 169 0
-168 169 0
-58 -168 0
-59 160 0
160 -169 0
-59 -169 0
49 50 53 54 51 52 57 58 59 60 55 56 0
-61 170 0
-72 -171 0
-62 172 0
-170 172 0
-62 -170 0
-63 173 0
-172 173 0
-63 -172 0
-64 174 0
-173 174 0
-64 -173 0
-65 175 0
-174 175 0
-65 -174 0
-66 176 0
-175 176 0
-66 -175 0
-67 177 0
-176 177 0
-67 -176 0
-68 178 0
-177 178 0
-68 -177 0
-69 179 0
-178 179 0
-69 -178 0
-70 180 0
-179 180 0
-70 -179 0
-71 171 0
171 -180 0
-71 -180 0
61 62 65 66 63 64 69 70 71 72 67 68 0
-73 181 0
-84 -182 0
-74 183 0
-181 183 0
-74 -181 0
-75 184 0
-183 184 0
-75 -183 0
-76 185 0
-184 185 0
-76 -184 0
-77 186 0
-185 186 0
-77 -185 0
-78 187 0
-186 187 0
-78 -186 0
-79 188 0
-187 188 0
-79 -187 0
-80 189 0
-188 189 0
-80 -188 0
-81 190 0
-189 190 0
-81 -189 0
-82 191 0
-190 191 0
-82 -190 0
-83 182 0
182 -191 0
-83 -191 0
73 74 75 76 81 82 83 84 77 78 79 80 0
-85 192 0
-96 -193 0
-86 194 0
-192 194 0
-86 -192 0
-87 195 0
-194 195 0
-87 -194 0
-88 196 0
-195 196 0
-88 -195 0
-89 197 0
-196 197 0
-89 -196 0
-90 198 0
-197 198 0
-90 -197 0
-91 199 0
-198 199 0
-91 -198 0
-92 200 0
-199 200 0
-92 -199 0
-93 201 0
-200 201 0
-93 -200 0
-94 202 0
-201 202 0
-94 -201 0
-95 193 0
193 -202 0
-95 -202 0
85 86 89 90 87 88 93 94 95 96 91 92 0
-97 203 0
-108 -204 0
-98 205 0
-203 205 0
-98 -203 0
-99 206 0
-205 206 0
-99 -205 0
-100 207 0
-206 207 0
-100 -206 0
-101 208 0
-207 208 0
-101 -207 0
-102 209 0
-208 209 0
-102 -208 0
-103 210 0
-209 210 0
-103 -209 0
-104 211 0
-210 211 0
-104 -210 0
-105 212 0
-211 212 0
-105 -211 0
-106 213 0
-212 213 0
-106 -212 0
-107 204 0
204 -213 0
-107 -213 0
97 98 101 102 99 100 105 106 107 108 103 104 0
-109 1 -214 0
109 2 -214 0
1 2 -214 0
-110 3 -215 0
110 4 -215 0
3 4 -215 0
-111 5 -216 0
111 6 -216 0
5 6 -216 0
-112 7 -217 0
112 8 -217 0
7 8 -217 0
-113 9 -218 0
113 10 -218 0
9 10 -218 0
-114 11 -219 0
114 12 -219 0
11 12 -219 0
-220 214 215 216 217 218 219 0
-109 13 -221 0
109 14 -221 0
13 14 -221 0
-110 15 -222 0
110 16 -222 0
15 16 -222 0
-111 17 -223 0
111 18 -223 0
17 18 -223 0
-112 19 -224 0
112 20 -224 0
19 20 -224 0
-113 21 -225 0
113 22 -225 0
21 22 -225 0
-114 23 -226 0
114 24 -226 0
23 24 -226 0
-227 221 222 223 224 225 226 0
-109 25 -228 0
109 26 -228 0
25 26 -228 0
-110 27 -229 0
110 28 -229 0
27 28 -229 0
-111 29 -230 0
111 30 -230 0
29 30 -230 0
-112 31 -231 0
112 32 -231 0
31 32 -231 0
-113 33 -232 0
113 34 -232 0
33 34 -232 0
-114 35 -233 0
114 36 -233 0
35 36 -233 0
-234 228 229 230 231 232 233 0
-109 37 -235 0
109 38 -235 0
37 38 -235 0
-110 39 -236 0
110 40 -236 0
39 40 -236 0
-111 41 -237 0
111 42 -237 0
41 42 -237 0
-112 43 -238 0
112 44 -238 0
43 44 -238 0
-113 45 -239 0
113 46 -239 0
45 46 -239 0
-114 47 -240 0
114 48 -240 0
47 48 -240 0
-241 235 236 237 238 239 240 0
-109 49 -242 0
109 50 -242 0
49 50 -242 0
-110 51 -243 0
110 52 -243 0
51 52 -243 0
-111 53 -244 0
111 54 -244 0
53 54 -244 0
-112 55 -245 0
112 56 -245 0
55 56 -245 0
-113 57 -246 0
113 58 -246 0
57 58 -246 0
-114 59 -247 0
114 60 -247 0
59 60 -247 0
-248 242 243 244 245 246 247 0
-109 61 -249 0
109 62 -249 0
61 62 -249 0
-110 63 -250 0
110 64 -250 0
63 64 -250 0
-111 65 -251 0
111 66 -251 0
65 66 -251 0
-112 67 -252 0
112 68 -252 0
67 68 -252 0
-113 69 -253 0
113 70 -253 0
69 70 -253 0
-114 71 -254 0
114 72 -254 0
71 72 -254 0
-255 249 250 251 252 253 254 0
-109 73 -256 0
109 74 -256 0
73 74 -256 0
-110 75 -257 0
110 76 -257 0
75 76 -257 0
-111 77 -258 0
111 78 -258 0
77 78 -258 0
-112 79 -259 0
112 80 -259 0
79 80 -259 0
-113 81 -260 0
113 82 -260 0
81 82 -260 0
-114 83 -261 0
114 84 -261 0
83 84 -261 0
-262 256 257 258 259 260 261 0
-109 85 -263 0
109 86 -263 0
85 86 -263 0
-110 87 -264 0
110 88 -264 0
87 88 -264 0
-111 89 -265 0
111 90 -265 0
89 90 -265 0
-112 91 -266 0
112 92 -266 0
91 92 -266 0
-113 93 -267 0
113 94 -267 0
93 94 -267 0
-114 95 -268 0
114 96 -268 0
95 96 -268 0
-269 263 264 265 266 267 268 0
-109 97 -270 0
109 98 -270 0
97 98 -270 0
-110 99 -271 0
110 100 -271 0
99 100 -271 0
-111 101 -272 0
111 102 -272 0
101 102 -272 0
-112 103 -273 0
112 104 -273 0
103 104 -273 0
-113 105 -274 0
113 106 -274 0
105 106 -274 0
-114 107 -275 0
114 108 -275 0
107 108 -275 0
-276 270 271 272 273 274 275 0
-220 277 0
-234 -278 0
-227 278 0
-277 278 0
-227 -277 0
-262 279 0
-276 -280 0
-269 280 0
-279 280 0
-269 -279 0
-220 241 0
241 -262 0
-227 248 0
248 -269 0
-234 255 0
255 -276 0
-220 -248 281 0
-220 282 0
-248 282 0
-262 -283 284 0
-262 285 0
-283 285 0
-282 -285 286 0
-282 287 0
-285 287 0
-281 -284 288 0
-281 289 0
-284 289 0
-286 -289 290 0
-286 291 0
-289 291 0
-292 -290 0
292 290 0
220 248 293 0
220 294 0
248 294 0
262 -295 296 0
262 297 0
-295 297 0
-294 -297 298 0
-294 299 0
-297 299 0
-293 -296 300 0
-293 301 0
-296 301 0
-298 -301 302 0
-298 303 0
-301 303 0
-292 -303 0
292 303 0
-241 292 0
-241 -227 304 0
-227 305 0
-241 305 0
-255 -269 306 0
-255 307 0
-269 307 0
-305 -307 308 0
-305 309 0
-307 309 0
-304 -306 310 0
-304 311 0
-306 311 0
-308 -311 312 0
-308 313 0
-311 313 0
-314 -312 0
314 312 0
241 227 315 0
227 316 0
241 316 0
255 269 317 0
255 318 0
269 318 0
-316 -318 319 0
-316 320 0
-318 320 0
-315 -317 321 0
-315 322 0
-317 322 0
-319 -322 323 0
-319 324 0
-322 324 0
-314 -323 0
314 323 0
-248 314 0
-234 -248 325 0
-234 326 0
-248 326 0
-276 -327 328 0
-276 329 0
-327 329 0
-326 -329 330 0
-326 331 0
-329 331 0
-325 -328 332 0
-325 333 0
-328 333 0
-330 -333 334 0
-330 335 0
-333 335 0
-336 -334 0
336 334 0
234 248 337 0
234 338 0
248 338 0
276 -339 340 0
276 341 0
-339 341 0
-338 -341 342 0
-338 343 0
-341 343 0
-337 -340 344 0
-337 345 0
-340 345 0
-342 -345 346 0
-342 347 0
-345 347 0
-336 -347 0
336 347 0
-255 336 0
-110 -113 -109 262 269 276 0
-110 -111 -109 262 269 276 0
-110 -112 -109 262 269 276 0
109 1 -348 0
-109 2 -348 0
1 2 -348 0
110 3 -349 0
-110 4 -349 0
3 4 -349 0
111 5 -350 0
-111 6 -350 0
5 6 -350 0
112 7 -351 0
-112 8 -351 0
7 8 -351 0
113 9 -352 0
-113 10 -352 0
9 10 -352 0
114 11 -353 0
-114 12 -353 0
11 12 -353 0
-354 348 349 350 351 352 353 0
109 13 -355 0
-109 14 -355 0
13 14 -355 0
110 15 -356 0
-110 16 -356 0
15 16 -356 0
111 17 -357 0
-111 18 -357 0
17 18 -357 0
112 19 -358 0
-112 20 -358 0
19 20 -358 0
113 21 -359 0
-113 22 -359 0
21 22 -359 0
114 23 -360 0
-114 24 -360 0
23 24 -360 0
-361 355 356 357 358 359 360 0
109 25 -362 0
-109 26 -362 0
25 26 -362 0
110 27 -363 0
-110 28 -363 0
27 28 -363 0
111 29 -364 0
-111 30 -364 0
29 30 -364 0
112 31 -365 0
-112 32 -365 0
31 32 -365 0
113 33 -366 0
-113 34 -366 0
33 34 -366 0
114 35 -367 0
-114 36 -367 0
35 36 -367 0
-368 362 363 364 365 366 367 0
109 37 -369 0
-109 38 -369 0
37 38 -369 0
110 39 -370 0
-110 40 -370 0
39 40 -370 0
111 41 -371 0
-111 42 -371 0
41 42 -371 0
112 43 -372 0
-112 44 -372 0
43 44 -372 0
113 45 -373 0
-113 46 -373 0
45 46 -373 0
114 47 -374 0
-114 48 -374 0
47 48 -374 0
-375 369 370 371 372 373 374 0
109 49 -376 0
-109 50 -376 0
49 50 -376 0
110 51 -377 0
-110 52 -377 0
51 52 -377 0
111 53 -378 0
-111 54 -378 0
53 54 -378 0
112 55 -379 0
-112 56 -379 0
55 56 -379 0
113 57 -380 0
-113 58 -380 0
57 58 -380 0
114 59 -381 0
-114 60 -381 0
59 60 -381 0
-382 376 377 378 379 380 381 0
109 61 -383 0
-109 62 -383 0
61 62 -383 0
110 63 -384 0
-110 64 -384 0
63 64 -384 0
111 65 -385 0
-111 66 -385 0
65 66 -385 0
112 67 -386 0
-112 68 -386 0
67 68 -386 0
113 69 -387 0
-113 70 -387 0
69 70 -387 0
114 71 -388 0
-114 72 -388 0
71 72 -388 0
-389 383 384 385 386 387 388 0
109 73 -390 0
-109 74 -390 0
73 74 -390 0
110 75 -391 0
-110 76 -391 0
75 76 -391 0
111 77 -392 0
-111 78 -392 0
77 78 -392 0
112 79 -393 0
-112 80 -393 0
79 80 -393 0
113 81 -394 0
-113 82 -394 0
81 82 -394 0
114 83 -395 0
-114 84 -395 0
83 84 -395 0
-396 390 391 392 393 394 395 0
109 85 -397 0
-109 86 -397 0
85 86 -397 0
110 87 -398 0
-110 88 -398 0
87 88 -398 0
111 89 -399 0
-111 90 -399 0
89 90 -399 0
112 91 -400 0
-112 92 -400 0
91 92 -400 0
113 93 -401 0
-113 94 -401 0
93 94 -401 0
114 95 -402 0
-114 96 -402 0
95 96 -402 0
-403 397 398 399 400 401 402 0
109 97 -404 0
-109 98 -404 0
97 98 -404 0
110 99 -405 0
-110 100 -405 0
99 100 -405 0
111 101 -406 0
-111 102 -406 0
101 102 -406 0
112 103 -407 0
-112 104 -407 0
103 104 -407 0
113 105 -408 0
-113 106 -408 0
105 106 -408 0
114 107 -409 0
-114 108 -409 0
107 108 -409 0
-410 404 405 406 407 408 409 0
-354 411 0
-396 -412 0
-375 412 0
-411 412 0
-375 -411 0
-368 413 0
-410 -414 0
-389 414 0
-413 414 0
-389 -413 0
-361 -382 415 0
-361 416 0
-382 416 0
-417 -415 0
417 415 0
361 382 418 0
361 419 0
382 419 0
-417 -418 0
417 418 0
-354 417 0
-361 -382 420 0
-361 421 0
-382 421 0
-422 -420 0
422 420 0
361 382 423 0
361 424 0
382 424 0
-422 -423 0
422 423 0
-368 422 0
-354 -368 425 0
-354 426 0
-368 426 0
-375 -382 427 0
-375 428 0
-382 428 0
-426 -428 429 0
-426 430 0
-428 430 0
-425 -427 431 0
-425 432 0
-427 432 0
-429 -432 433 0
-429 434 0
-432 434 0
-389 -435 436 0
-389 437 0
-435 437 0
-438 -439 440 0
-438 441 0
-439 441 0
-437 -441 442 0
-437 443 0
-441 443 0
-436 -440 444 0
-436 445 0
-440 445 0
-442 -445 446 0
-442 447 0
-445 447 0
-430 -443 448 0
-430 449 0
-443 449 0
-433 -446 450 0
-433 451 0
-446 451 0
-448 -451 452 0
-448 453 0
-451 453 0
-434 -447 454 0
-434 455 0
-447 455 0
-431 -444 456 0
-431 457 0
-444 457 0
-454 -457 458 0
-454 459 0
-457 459 0
-453 -455 460 0
-453 461 0
-455 461 0
-452 -459 462 0
-452 463 0
-459 463 0
-464 -460 0
464 460 0
354 368 465 0
354 466 0
368 466 0
375 382 467 0
375 468 0
382 468 0
-466 -468 469 0
-466 470 0
-468 470 0
-465 -467 471 0
-465 472 0
-467 472 0
-469 -472 473 0
-469 474 0
-472 474 0
389 -475 476 0
389 477 0
-475 477 0
-478 -479 480 0
-478 481 0
-479 481 0
-477 -481 482 0
-477 483 0
-481 483 0
-476 -480 484 0
-476 485 0
-480 485 0
-482 -485 486 0
-482 487 0
-485 487 0
-470 -483 488 0
-470 489 0
-483 489 0
-473 -486 490 0
-473 491 0
-486 491 0
-488 -491 492 0
-488 493 0
-491 493 0
-474 -487 494 0
-474 495 0
-487 495 0
-471 -484 496 0
-471 497 0
-484 497 0
-494 -497 498 0
-494 499 0
-497 499 0
-493 -495 500 0
-493 501 0
-495 501 0
-492 -499 502 0
-492 503 0
-499 503 0
-464 -503 0
464 503 0
-361 464 0
-361 -382 504 0
-361 505 0
-382 505 0
-403 -506 507 0
-403 508 0
-506 508 0
-505 -508 509 0
-505 510 0
-508 510 0
-504 -507 511 0
-504 512 0
-507 512 0
-509 -512 513 0
-509 514 0
-512 514 0
-515 -514 0
515 514 0
361 382 516 0
361 517 0
382 517 0
403 -518 519 0
403 520 0
-518 520 0
-517 -520 521 0
-517 522 0
-520 522 0
-516 -519 523 0
-516 524 0
-519 524 0
-521 -524 525 0
-521 526 0
-524 526 0
-515 -525 0
515 525 0
-375 515 0
-361 -382 527 0
-361 528 0
-382 528 0
-403 -529 530 0
-403 531 0
-529 531 0
-528 -531 532 0
-528 533 0
-531 533 0
-527 -530 534 0
-527 535 0
-530 535 0
-532 -535 536 0
-532 537 0
-535 537 0
-538 -537 0
538 537 0
361 382 539 0
361 540 0
382 540 0
403 -541 542 0
403 543 0
-541 543 0
-540 -543 544 0
-540 545 0
-543 545 0
-539 -542 546 0
-539 547 0
-542 547 0
-544 -547 548 0
-544 549 0
-547 549 0
-538 -548 0
538 548 0
-389 538 0
-354 -361 550 0
-354 551 0
-361 551 0
-375 -368 552 0
-368 553 0
-375 553 0
-551 -553 554 0
-551 555 0
-553 555 0
-550 -552 556 0
-550 557 0
-552 557 0
-554 -557 558 0
-554 559 0
-557 559 0
-396 -389 560 0
-389 561 0
-396 561 0
-403 -410 562 0
-403 563 0
-410 563 0
-561 -563 564 0
-561 565 0
-563 565 0
-560 -562 566 0
-560 567 0
-562 567 0
-564 -567 568 0
-564 569 0
-567 569 0
-555 -565 570 0
-555 571 0
-565 571 0
-558 -568 572 0
-558 573 0
-568 573 0
-570 -573 574 0
-570 575 0
-573 575 0
-559 -569 576 0
-559 577 0
-569 577 0
-556 -566 578 0
-556 579 0
-566 579 0
-576 -579 580 0
-576 581 0
-579 581 0
-575 -577 582 0
-575 583 0
-577 583 0
-574 -581 584 0
-574 585 0
-581 585 0
-586 -582 0
586 582 0
354 361 587 0
354 588 0
361 588 0
375 368 589 0
368 590 0
375 590 0
-588 -590 591 0
-588 592 0
-590 592 0
-587 -589 593 0
-587 594 0
-589 594 0
-591 -594 595 0
-591 596 0
-594 596 0
396 389 597 0
389 598 0
396 598 0
403 410 599 0
403 600 0
410 600 0
-598 -600 601 0
-598 602 0
-600 602 0
-597 -599 603 0
-597 604 0
-599 604 0
-601 -604 605 0
-601 606 0
-604 606 0
-592 -602 607 0
-592 608 0
-602 608 0
-595 -605 609 0
-595 610 0
-605 610 0
-607 -610 611 0
-607 612 0
-610 612 0
-596 -606 613 0
-596 614 0
-606 614 0
-593 -603 615 0
-593 616 0
-603 616 0
-613 -616 617 0
-613 618 0
-616 618 0
-612 -614 619 0
-612 620 0
-614 620 0
-611 -618 621 0
-611 622 0
-618 622 0
-609 -617 623 0
-609 624 0
-617 624 0
-586 -623 0
586 623 0
-382 586 0
-382 -403 625 0
-382 626 0
-403 626 0
-627 -625 0
627 625 0
382 403 628 0
382 629 0
403 629 0
-627 -628 0
627 628 0
-396 627 0
-382 -403 630 0
-382 631 0
-403 631 0
-632 -630 0
632 630 0
382 403 633 0
382 634 0
403 634 0
-632 -633 0
632 633 0
-410 632 0
-375 -382 635 0
-375 636 0
-382 636 0
-396 -389 637 0
-389 638 0
-396 638 0
-636 -638 639 0
-636 640 0
-638 640 0
-635 -637 641 0
-635 642 0
-637 642 0
-639 -642 643 0
-639 644 0
-642 644 0
-410 -645 646 0
-410 647 0
-645 647 0
-648 -649 650 0
-648 651 0
-649 651 0
-647 -651 652 0
-647 653 0
-651 653 0
-646 -650 654 0
-646 655 0
-650 655 0
-652 -655 656 0
-652 657 0
-655 657 0
-640 -653 658 0
-640 659 0
-653 659 0
-643 -656 660 0
-643 661 0
-656 661 0
-658 -661 662 0
-658 663 0
-661 663 0
-644 -657 664 0
-644 665 0
-657 665 0
-641 -654 666 0
-641 667 0
-654 667 0
-664 -667 668 0
-664 669 0
-667 669 0
-663 -665 670 0
-663 671 0
-665 671 0
-662 -669 672 0
-662 673 0
-669 673 0
-674 -670 0
674 670 0
375 382 675 0
375 676 0
382 676 0
396 389 677 0
389 678 0
396 678 0
-676 -678 679 0
-676 680 0
-678 680 0
-675 -677 681 0
-675 682 0
-677 682 0
-679 -682 683 0
-679 684 0
-682 684 0
410 -685 686 0
410 687 0
-685 687 0
-688 -689 690 0
-688 691 0
-689 691 0
-687 -691 692 0
-687 693 0
-691 693 0
-686 -690 694 0
-686 695 0
-690 695 0
-692 -695 696 0
-692 697 0
-695 697 0
-680 -693 698 0
-680 699 0
-693 699 0
-683 -696 700 0
-683 701 0
-696 701 0
-698 -701 702 0
-698 703 0
-701 703 0
-684 -697 704 0
-684 705 0
-697 705 0
-681 -694 706 0
-681 707 0
-694 707 0
-704 -707 708 0
-704 709 0
-707 709 0
-703 -705 710 0
-703 711 0
-705 711 0
-702 -709 712 0
-702 713 0
-709 713 0
-674 -713 0
674 713 0
-403 674 0
110 368 389 410 0
109 368 389 410 0
113 111 112 368 389 410 0