module RUS where import DEMO -- This is an implementation of Russian Cards problem in DEMO -- By using this, we can check whether some communications are effective and safe. -- Three agens Anne/Bill/Cath are represented by a/b/c. -- Proposional letter "pi" is True iff Anne holds card i. (p <= p0) -- Proposional letter "qi" is True iff Bill holds card i. -- Proposional letter "ri" is True iff Cath holds card i. --The action model for: Anne says "My hand is one of 012,034,056,135,246" a_announce=public( K a (Disj[Conj[p,p1,p2],Conj[p,p3,p4],Conj[p,p5,p6],Conj[p1,p3,p5],Conj[p2,p4,p6]])) --The action model for: Bill says "Cath holds card 6" b_announce = public (K b r6) -- Formulas to present agents' knowledge. -- Anne knows Bill's cards a_knows_bs = Conj[ Disj[K a q, K a (Neg q) ], Disj[K a q1, K a (Neg q1) ], Disj[K a q2, K a (Neg q2) ], Disj[K a q3, K a (Neg q3) ], Disj[K a q4, K a (Neg q4) ], Disj[K a q5, K a (Neg q5) ], Disj[K a q6, K a (Neg q6) ] ] -- Bill knows Anne's cards b_knows_as = Conj[ Disj[K b p, K b (Neg p) ], Disj[K b p1, K b (Neg p1) ], Disj[K b p2, K b (Neg p2) ], Disj[K b p3, K b (Neg p3) ], Disj[K b p4, K b (Neg p4) ], Disj[K b p5, K b (Neg p5) ], Disj[K b p6, K b (Neg p6) ] ] -- Cath is ignorant. --If C does not hold i, then C does not know whether i belongs to A or B. c_ignorant=Conj[ Disj[r, Conj[ Neg (K c p), Neg (K c q)]], Disj[r1,Conj[ Neg (K c p1), Neg (K c q1)]], Disj[r2,Conj[ Neg (K c p2), Neg (K c q2)]], Disj[r3,Conj[ Neg (K c p3), Neg (K c q3)]], Disj[r4,Conj[ Neg (K c p4), Neg (K c q4)]], Disj[r5,Conj[ Neg (K c p5), Neg (K c q5)]], Disj[r6,Conj[ Neg (K c p6), Neg (K c q6)]] ] -- Checking for knowledge during the communication: --Step 1 -- After Anne announces five hands, Bill knows Anne's card. And this is commonly known by a,b. check1 = isTrue ( upd rus a_announce ) b_knows_as check2 = isTrue ( upd rus a_announce ) (CK [a,b] b_knows_as) -- And Bill knows Cath's card. (This is entailed by the fact that Bill knows Anne's cards.) check3 = isTrue ( upd rus a_announce ) (K b r6) -- Cath remains ignorant of anne's and Bill's cards, and this is common knowledge. check4 = isTrue ( upd rus a_announce ) (CK [a,b,c] c_ignorant) --Step 2 -- After Bill announces Cath's card, Anne knows Bill's cards, with Cath remains ignorant. check5 = isTrue ( upd ( upd rus a_announce ) b_announce) (CK [a,b] a_knows_bs) check6 = isTrue ( upd ( upd rus a_announce ) b_announce) (CK [a,b] b_knows_as) check7 = isTrue ( upd ( upd rus a_announce ) b_announce) (CK [a,b,c] c_ignorant) rus :: EpistM rus = (Pmod [0..139] val acc [0]) where val = [ ( 0,[P 0,P 1,P 2,Q 3,Q 4,Q 5,R 6]),( 1,[P 0,P 1,P 2,Q 3,Q 4,Q 6,R 5]), ( 2,[P 0,P 1,P 2,Q 3,Q 5,Q 6,R 4]),( 3,[P 0,P 1,P 2,Q 4,Q 5,Q 6,R 3]), ( 4,[P 0,P 1,P 3,Q 2,Q 4,Q 5,R 6]),( 5,[P 0,P 1,P 3,Q 2,Q 4,Q 6,R 5]), ( 6,[P 0,P 1,P 3,Q 2,Q 5,Q 6,R 4]),( 7,[P 0,P 1,P 3,Q 4,Q 5,Q 6,R 2]), ( 8,[P 0,P 1,P 4,Q 2,Q 3,Q 5,R 6]),( 9,[P 0,P 1,P 4,Q 2,Q 3,Q 6,R 5]), ( 10,[P 0,P 1,P 4,Q 2,Q 5,Q 6,R 3]),( 11,[P 0,P 1,P 4,Q 3,Q 5,Q 6,R 2]), ( 12,[P 0,P 1,P 5,Q 2,Q 3,Q 4,R 6]),( 13,[P 0,P 1,P 5,Q 2,Q 3,Q 6,R 4]), ( 14,[P 0,P 1,P 5,Q 2,Q 4,Q 6,R 3]),( 15,[P 0,P 1,P 5,Q 3,Q 4,Q 6,R 2]), ( 16,[P 0,P 1,P 6,Q 2,Q 3,Q 4,R 5]),( 17,[P 0,P 1,P 6,Q 2,Q 3,Q 5,R 4]), ( 18,[P 0,P 1,P 6,Q 2,Q 4,Q 5,R 3]),( 19,[P 0,P 1,P 6,Q 3,Q 4,Q 5,R 2]), ( 20,[P 0,P 2,P 3,Q 1,Q 4,Q 5,R 6]),( 21,[P 0,P 2,P 3,Q 1,Q 4,Q 6,R 5]), ( 22,[P 0,P 2,P 3,Q 1,Q 5,Q 6,R 4]),( 23,[P 0,P 2,P 3,Q 4,Q 5,Q 6,R 1]), ( 24,[P 0,P 2,P 4,Q 1,Q 3,Q 5,R 6]),( 25,[P 0,P 2,P 4,Q 1,Q 3,Q 6,R 5]), ( 26,[P 0,P 2,P 4,Q 1,Q 5,Q 6,R 3]),( 27,[P 0,P 2,P 4,Q 3,Q 5,Q 6,R 1]), ( 28,[P 0,P 2,P 5,Q 1,Q 3,Q 4,R 6]),( 29,[P 0,P 2,P 5,Q 1,Q 3,Q 6,R 4]), ( 30,[P 0,P 2,P 5,Q 1,Q 4,Q 6,R 3]),( 31,[P 0,P 2,P 5,Q 3,Q 4,Q 6,R 1]), ( 32,[P 0,P 2,P 6,Q 1,Q 3,Q 4,R 5]),( 33,[P 0,P 2,P 6,Q 1,Q 3,Q 5,R 4]), ( 34,[P 0,P 2,P 6,Q 1,Q 4,Q 5,R 3]),( 35,[P 0,P 2,P 6,Q 3,Q 4,Q 5,R 1]), ( 36,[P 0,P 3,P 4,Q 1,Q 2,Q 5,R 6]),( 37,[P 0,P 3,P 4,Q 1,Q 2,Q 6,R 5]), ( 38,[P 0,P 3,P 4,Q 1,Q 5,Q 6,R 2]),( 39,[P 0,P 3,P 4,Q 2,Q 5,Q 6,R 1]), ( 40,[P 0,P 3,P 5,Q 1,Q 2,Q 4,R 6]),( 41,[P 0,P 3,P 5,Q 1,Q 2,Q 6,R 4]), ( 42,[P 0,P 3,P 5,Q 1,Q 4,Q 6,R 2]),( 43,[P 0,P 3,P 5,Q 2,Q 4,Q 6,R 1]), ( 44,[P 0,P 3,P 6,Q 1,Q 2,Q 4,R 5]),( 45,[P 0,P 3,P 6,Q 1,Q 2,Q 5,R 4]), ( 46,[P 0,P 3,P 6,Q 1,Q 4,Q 5,R 2]),( 47,[P 0,P 3,P 6,Q 2,Q 4,Q 5,R 1]), ( 48,[P 0,P 4,P 5,Q 1,Q 2,Q 3,R 6]),( 49,[P 0,P 4,P 5,Q 1,Q 2,Q 6,R 3]), ( 50,[P 0,P 4,P 5,Q 1,Q 3,Q 6,R 2]),( 51,[P 0,P 4,P 5,Q 2,Q 3,Q 6,R 1]), ( 52,[P 0,P 4,P 6,Q 1,Q 2,Q 3,R 5]),( 53,[P 0,P 4,P 6,Q 1,Q 2,Q 5,R 3]), ( 54,[P 0,P 4,P 6,Q 1,Q 3,Q 5,R 2]),( 55,[P 0,P 4,P 6,Q 2,Q 3,Q 5,R 1]), ( 56,[P 0,P 5,P 6,Q 1,Q 2,Q 3,R 4]),( 57,[P 0,P 5,P 6,Q 1,Q 2,Q 4,R 3]), ( 58,[P 0,P 5,P 6,Q 1,Q 3,Q 4,R 2]),( 59,[P 0,P 5,P 6,Q 2,Q 3,Q 4,R 1]), ( 60,[P 1,P 2,P 3,Q 0,Q 4,Q 5,R 6]),( 61,[P 1,P 2,P 3,Q 0,Q 4,Q 6,R 5]), ( 62,[P 1,P 2,P 3,Q 0,Q 5,Q 6,R 4]),( 63,[P 1,P 2,P 3,Q 4,Q 5,Q 6,R 0]), ( 64,[P 1,P 2,P 4,Q 0,Q 3,Q 5,R 6]),( 65,[P 1,P 2,P 4,Q 0,Q 3,Q 6,R 5]), ( 66,[P 1,P 2,P 4,Q 0,Q 5,Q 6,R 3]),( 67,[P 1,P 2,P 4,Q 3,Q 5,Q 6,R 0]), ( 68,[P 1,P 2,P 5,Q 0,Q 3,Q 4,R 6]),( 69,[P 1,P 2,P 5,Q 0,Q 3,Q 6,R 4]), ( 70,[P 1,P 2,P 5,Q 0,Q 4,Q 6,R 3]),( 71,[P 1,P 2,P 5,Q 3,Q 4,Q 6,R 0]), ( 72,[P 1,P 2,P 6,Q 0,Q 3,Q 4,R 5]),( 73,[P 1,P 2,P 6,Q 0,Q 3,Q 5,R 4]), ( 74,[P 1,P 2,P 6,Q 0,Q 4,Q 5,R 3]),( 75,[P 1,P 2,P 6,Q 3,Q 4,Q 5,R 0]), ( 76,[P 1,P 3,P 4,Q 0,Q 2,Q 5,R 6]),( 77,[P 1,P 3,P 4,Q 0,Q 2,Q 6,R 5]), ( 78,[P 1,P 3,P 4,Q 0,Q 5,Q 6,R 2]),( 79,[P 1,P 3,P 4,Q 2,Q 5,Q 6,R 0]), ( 80,[P 1,P 3,P 5,Q 0,Q 2,Q 4,R 6]),( 81,[P 1,P 3,P 5,Q 0,Q 2,Q 6,R 4]), ( 82,[P 1,P 3,P 5,Q 0,Q 4,Q 6,R 2]),( 83,[P 1,P 3,P 5,Q 2,Q 4,Q 6,R 0]), ( 84,[P 1,P 3,P 6,Q 0,Q 2,Q 4,R 5]),( 85,[P 1,P 3,P 6,Q 0,Q 2,Q 5,R 4]), ( 86,[P 1,P 3,P 6,Q 0,Q 4,Q 5,R 2]),( 87,[P 1,P 3,P 6,Q 2,Q 4,Q 5,R 0]), ( 88,[P 1,P 4,P 5,Q 0,Q 2,Q 3,R 6]),( 89,[P 1,P 4,P 5,Q 0,Q 2,Q 6,R 3]), ( 90,[P 1,P 4,P 5,Q 0,Q 3,Q 6,R 2]),( 91,[P 1,P 4,P 5,Q 2,Q 3,Q 6,R 0]), ( 92,[P 1,P 4,P 6,Q 0,Q 2,Q 3,R 5]),( 93,[P 1,P 4,P 6,Q 0,Q 2,Q 5,R 3]), ( 94,[P 1,P 4,P 6,Q 0,Q 3,Q 5,R 2]),( 95,[P 1,P 4,P 6,Q 2,Q 3,Q 5,R 0]), ( 96,[P 1,P 5,P 6,Q 0,Q 2,Q 3,R 4]),( 97,[P 1,P 5,P 6,Q 0,Q 2,Q 4,R 3]), ( 98,[P 1,P 5,P 6,Q 0,Q 3,Q 4,R 2]),( 99,[P 1,P 5,P 6,Q 2,Q 3,Q 4,R 0]), (100,[P 2,P 3,P 4,Q 0,Q 1,Q 5,R 6]),(101,[P 2,P 3,P 4,Q 0,Q 1,Q 6,R 5]), (102,[P 2,P 3,P 4,Q 0,Q 5,Q 6,R 1]),(103,[P 2,P 3,P 4,Q 1,Q 5,Q 6,R 0]), (104,[P 2,P 3,P 5,Q 0,Q 1,Q 4,R 6]),(105,[P 2,P 3,P 5,Q 0,Q 1,Q 6,R 4]), (106,[P 2,P 3,P 5,Q 0,Q 4,Q 6,R 1]),(107,[P 2,P 3,P 5,Q 1,Q 4,Q 6,R 0]), (108,[P 2,P 3,P 6,Q 0,Q 1,Q 4,R 5]),(109,[P 2,P 3,P 6,Q 0,Q 1,Q 5,R 4]), (110,[P 2,P 3,P 6,Q 0,Q 4,Q 5,R 1]),(111,[P 2,P 3,P 6,Q 1,Q 4,Q 5,R 0]), (112,[P 2,P 4,P 5,Q 0,Q 1,Q 3,R 6]),(113,[P 2,P 4,P 5,Q 0,Q 1,Q 6,R 3]), (114,[P 2,P 4,P 5,Q 0,Q 3,Q 6,R 1]),(115,[P 2,P 4,P 5,Q 1,Q 3,Q 6,R 0]), (116,[P 2,P 4,P 6,Q 0,Q 1,Q 3,R 5]),(117,[P 2,P 4,P 6,Q 0,Q 1,Q 5,R 3]), (118,[P 2,P 4,P 6,Q 0,Q 3,Q 5,R 1]),(119,[P 2,P 4,P 6,Q 1,Q 3,Q 5,R 0]), (120,[P 2,P 5,P 6,Q 0,Q 1,Q 3,R 4]),(121,[P 2,P 5,P 6,Q 0,Q 1,Q 4,R 3]), (122,[P 2,P 5,P 6,Q 0,Q 3,Q 4,R 1]),(123,[P 2,P 5,P 6,Q 1,Q 3,Q 4,R 0]), (124,[P 3,P 4,P 5,Q 0,Q 1,Q 2,R 6]),(125,[P 3,P 4,P 5,Q 0,Q 1,Q 6,R 2]), (126,[P 3,P 4,P 5,Q 0,Q 2,Q 6,R 1]),(127,[P 3,P 4,P 5,Q 1,Q 2,Q 6,R 0]), (128,[P 3,P 4,P 6,Q 0,Q 1,Q 2,R 5]),(129,[P 3,P 4,P 6,Q 0,Q 1,Q 5,R 2]), (130,[P 3,P 4,P 6,Q 0,Q 2,Q 5,R 1]),(131,[P 3,P 4,P 6,Q 1,Q 2,Q 5,R 0]), (132,[P 3,P 5,P 6,Q 0,Q 1,Q 2,R 4]),(133,[P 3,P 5,P 6,Q 0,Q 1,Q 4,R 2]), (134,[P 3,P 5,P 6,Q 0,Q 2,Q 4,R 1]),(135,[P 3,P 5,P 6,Q 1,Q 2,Q 4,R 0]), (136,[P 4,P 5,P 6,Q 0,Q 1,Q 2,R 3]),(137,[P 4,P 5,P 6,Q 0,Q 1,Q 3,R 2]), (138,[P 4,P 5,P 6,Q 0,Q 2,Q 3,R 1]),(139,[P 4,P 5,P 6,Q 1,Q 2,Q 3,R 0])] acc = [ (a,0,0),(a,0,1),(a,0,2),(a,0,3),(a,1,0),(a,1,1), (a,1,2),(a,1,3),(a,2,0),(a,2,1),(a,2,2),(a,2,3), (a,3,0),(a,3,1),(a,3,2),(a,3,3),(a,4,4),(a,4,5), (a,4,6),(a,4,7),(a,5,4),(a,5,5),(a,5,6),(a,5,7), (a,6,4),(a,6,5),(a,6,6),(a,6,7),(a,7,4),(a,7,5), (a,7,6),(a,7,7),(a,8,8),(a,8,9),(a,8,10),(a,8,11), (a,9,8),(a,9,9),(a,9,10),(a,9,11),(a,10,8),(a,10,9), (a,10,10),(a,10,11),(a,11,8),(a,11,9),(a,11,10),(a,11,11), (a,12,12),(a,12,13),(a,12,14),(a,12,15),(a,13,12),(a,13,13), (a,13,14),(a,13,15),(a,14,12),(a,14,13),(a,14,14),(a,14,15), (a,15,12),(a,15,13),(a,15,14),(a,15,15),(a,16,16),(a,16,17), (a,16,18),(a,16,19),(a,17,16),(a,17,17),(a,17,18),(a,17,19), (a,18,16),(a,18,17),(a,18,18),(a,18,19),(a,19,16),(a,19,17), (a,19,18),(a,19,19),(a,20,20),(a,20,21),(a,20,22),(a,20,23), (a,21,20),(a,21,21),(a,21,22),(a,21,23),(a,22,20),(a,22,21), (a,22,22),(a,22,23),(a,23,20),(a,23,21),(a,23,22),(a,23,23), (a,24,24),(a,24,25),(a,24,26),(a,24,27),(a,25,24),(a,25,25), (a,25,26),(a,25,27),(a,26,24),(a,26,25),(a,26,26),(a,26,27), (a,27,24),(a,27,25),(a,27,26),(a,27,27),(a,28,28),(a,28,29), (a,28,30),(a,28,31),(a,29,28),(a,29,29),(a,29,30),(a,29,31), (a,30,28),(a,30,29),(a,30,30),(a,30,31),(a,31,28),(a,31,29), (a,31,30),(a,31,31),(a,32,32),(a,32,33),(a,32,34),(a,32,35), (a,33,32),(a,33,33),(a,33,34),(a,33,35),(a,34,32),(a,34,33), (a,34,34),(a,34,35),(a,35,32),(a,35,33),(a,35,34),(a,35,35), (a,36,36),(a,36,37),(a,36,38),(a,36,39),(a,37,36),(a,37,37), (a,37,38),(a,37,39),(a,38,36),(a,38,37),(a,38,38),(a,38,39), (a,39,36),(a,39,37),(a,39,38),(a,39,39),(a,40,40),(a,40,41), (a,40,42),(a,40,43),(a,41,40),(a,41,41),(a,41,42),(a,41,43), (a,42,40),(a,42,41),(a,42,42),(a,42,43),(a,43,40),(a,43,41), (a,43,42),(a,43,43),(a,44,44),(a,44,45),(a,44,46),(a,44,47), (a,45,44),(a,45,45),(a,45,46),(a,45,47),(a,46,44),(a,46,45), (a,46,46),(a,46,47),(a,47,44),(a,47,45),(a,47,46),(a,47,47), (a,48,48),(a,48,49),(a,48,50),(a,48,51),(a,49,48),(a,49,49), (a,49,50),(a,49,51),(a,50,48),(a,50,49),(a,50,50),(a,50,51), (a,51,48),(a,51,49),(a,51,50),(a,51,51),(a,52,52),(a,52,53), (a,52,54),(a,52,55),(a,53,52),(a,53,53),(a,53,54),(a,53,55), (a,54,52),(a,54,53),(a,54,54),(a,54,55),(a,55,52),(a,55,53), (a,55,54),(a,55,55),(a,56,56),(a,56,57),(a,56,58),(a,56,59), (a,57,56),(a,57,57),(a,57,58),(a,57,59),(a,58,56),(a,58,57), (a,58,58),(a,58,59),(a,59,56),(a,59,57),(a,59,58),(a,59,59), (a,60,60),(a,60,61),(a,60,62),(a,60,63),(a,61,60),(a,61,61), (a,61,62),(a,61,63),(a,62,60),(a,62,61),(a,62,62),(a,62,63), (a,63,60),(a,63,61),(a,63,62),(a,63,63),(a,64,64),(a,64,65), (a,64,66),(a,64,67),(a,65,64),(a,65,65),(a,65,66),(a,65,67), (a,66,64),(a,66,65),(a,66,66),(a,66,67),(a,67,64),(a,67,65), (a,67,66),(a,67,67),(a,68,68),(a,68,69),(a,68,70),(a,68,71), (a,69,68),(a,69,69),(a,69,70),(a,69,71),(a,70,68),(a,70,69), (a,70,70),(a,70,71),(a,71,68),(a,71,69),(a,71,70),(a,71,71), (a,72,72),(a,72,73),(a,72,74),(a,72,75),(a,73,72),(a,73,73), (a,73,74),(a,73,75),(a,74,72),(a,74,73),(a,74,74),(a,74,75), (a,75,72),(a,75,73),(a,75,74),(a,75,75),(a,76,76),(a,76,77), (a,76,78),(a,76,79),(a,77,76),(a,77,77),(a,77,78),(a,77,79), (a,78,76),(a,78,77),(a,78,78),(a,78,79),(a,79,76),(a,79,77), (a,79,78),(a,79,79),(a,80,80),(a,80,81),(a,80,82),(a,80,83), (a,81,80),(a,81,81),(a,81,82),(a,81,83),(a,82,80),(a,82,81), (a,82,82),(a,82,83),(a,83,80),(a,83,81),(a,83,82),(a,83,83), (a,84,84),(a,84,85),(a,84,86),(a,84,87),(a,85,84),(a,85,85), (a,85,86),(a,85,87),(a,86,84),(a,86,85),(a,86,86),(a,86,87), (a,87,84),(a,87,85),(a,87,86),(a,87,87),(a,88,88),(a,88,89), (a,88,90),(a,88,91),(a,89,88),(a,89,89),(a,89,90),(a,89,91), (a,90,88),(a,90,89),(a,90,90),(a,90,91),(a,91,88),(a,91,89), (a,91,90),(a,91,91),(a,92,92),(a,92,93),(a,92,94),(a,92,95), (a,93,92),(a,93,93),(a,93,94),(a,93,95),(a,94,92),(a,94,93), (a,94,94),(a,94,95),(a,95,92),(a,95,93),(a,95,94),(a,95,95), (a,96,96),(a,96,97),(a,96,98),(a,96,99),(a,97,96),(a,97,97), (a,97,98),(a,97,99),(a,98,96),(a,98,97),(a,98,98),(a,98,99), (a,99,96),(a,99,97),(a,99,98),(a,99,99),(a,100,100),(a,100,101), (a,100,102),(a,100,103),(a,101,100),(a,101,101),(a,101,102),(a,101,103), (a,102,100),(a,102,101),(a,102,102),(a,102,103),(a,103,100),(a,103,101), (a,103,102),(a,103,103),(a,104,104),(a,104,105),(a,104,106),(a,104,107), (a,105,104),(a,105,105),(a,105,106),(a,105,107),(a,106,104),(a,106,105), (a,106,106),(a,106,107),(a,107,104),(a,107,105),(a,107,106),(a,107,107), (a,108,108),(a,108,109),(a,108,110),(a,108,111),(a,109,108),(a,109,109), (a,109,110),(a,109,111),(a,110,108),(a,110,109),(a,110,110),(a,110,111), (a,111,108),(a,111,109),(a,111,110),(a,111,111),(a,112,112),(a,112,113), (a,112,114),(a,112,115),(a,113,112),(a,113,113),(a,113,114),(a,113,115), (a,114,112),(a,114,113),(a,114,114),(a,114,115),(a,115,112),(a,115,113), (a,115,114),(a,115,115),(a,116,116),(a,116,117),(a,116,118),(a,116,119), (a,117,116),(a,117,117),(a,117,118),(a,117,119),(a,118,116),(a,118,117), (a,118,118),(a,118,119),(a,119,116),(a,119,117),(a,119,118),(a,119,119), (a,120,120),(a,120,121),(a,120,122),(a,120,123),(a,121,120),(a,121,121), (a,121,122),(a,121,123),(a,122,120),(a,122,121),(a,122,122),(a,122,123), (a,123,120),(a,123,121),(a,123,122),(a,123,123),(a,124,124),(a,124,125), (a,124,126),(a,124,127),(a,125,124),(a,125,125),(a,125,126),(a,125,127), (a,126,124),(a,126,125),(a,126,126),(a,126,127),(a,127,124),(a,127,125), (a,127,126),(a,127,127),(a,128,128),(a,128,129),(a,128,130),(a,128,131), (a,129,128),(a,129,129),(a,129,130),(a,129,131),(a,130,128),(a,130,129), (a,130,130),(a,130,131),(a,131,128),(a,131,129),(a,131,130),(a,131,131), (a,132,132),(a,132,133),(a,132,134),(a,132,135),(a,133,132),(a,133,133), (a,133,134),(a,133,135),(a,134,132),(a,134,133),(a,134,134),(a,134,135), (a,135,132),(a,135,133),(a,135,134),(a,135,135),(a,136,136),(a,136,137), (a,136,138),(a,136,139),(a,137,136),(a,137,137),(a,137,138),(a,137,139), (a,138,136),(a,138,137),(a,138,138),(a,138,139),(a,139,136),(a,139,137), (a,139,138),(a,139,139),(b,0,0),(b,0,19),(b,0,35),(b,0,75), (b,1,1),(b,1,15),(b,1,31),(b,1,71),(b,2,2),(b,2,11), (b,2,27),(b,2,67),(b,3,3),(b,3,7),(b,3,23),(b,3,63), (b,4,4),(b,4,18),(b,4,47),(b,4,87),(b,5,5),(b,5,14), (b,5,43),(b,5,83),(b,6,6),(b,6,10),(b,6,39),(b,6,79), (b,7,3),(b,7,7),(b,7,23),(b,7,63),(b,8,8),(b,8,17), (b,8,55),(b,8,95),(b,9,9),(b,9,13),(b,9,51),(b,9,91), (b,10,6),(b,10,10),(b,10,39),(b,10,79),(b,11,2),(b,11,11), (b,11,27),(b,11,67),(b,12,12),(b,12,16),(b,12,59),(b,12,99), (b,13,9),(b,13,13),(b,13,51),(b,13,91),(b,14,5),(b,14,14), (b,14,43),(b,14,83),(b,15,1),(b,15,15),(b,15,31),(b,15,71), (b,16,12),(b,16,16),(b,16,59),(b,16,99),(b,17,8),(b,17,17), (b,17,55),(b,17,95),(b,18,4),(b,18,18),(b,18,47),(b,18,87), (b,19,0),(b,19,19),(b,19,35),(b,19,75),(b,20,20),(b,20,34), (b,20,46),(b,20,111),(b,21,21),(b,21,30),(b,21,42),(b,21,107), (b,22,22),(b,22,26),(b,22,38),(b,22,103),(b,23,3),(b,23,7), (b,23,23),(b,23,63),(b,24,24),(b,24,33),(b,24,54),(b,24,119), (b,25,25),(b,25,29),(b,25,50),(b,25,115),(b,26,22),(b,26,26), (b,26,38),(b,26,103),(b,27,2),(b,27,11),(b,27,27),(b,27,67), (b,28,28),(b,28,32),(b,28,58),(b,28,123),(b,29,25),(b,29,29), (b,29,50),(b,29,115),(b,30,21),(b,30,30),(b,30,42),(b,30,107), (b,31,1),(b,31,15),(b,31,31),(b,31,71),(b,32,28),(b,32,32), (b,32,58),(b,32,123),(b,33,24),(b,33,33),(b,33,54),(b,33,119), (b,34,20),(b,34,34),(b,34,46),(b,34,111),(b,35,0),(b,35,19), (b,35,35),(b,35,75),(b,36,36),(b,36,45),(b,36,53),(b,36,131), (b,37,37),(b,37,41),(b,37,49),(b,37,127),(b,38,22),(b,38,26), (b,38,38),(b,38,103),(b,39,6),(b,39,10),(b,39,39),(b,39,79), (b,40,40),(b,40,44),(b,40,57),(b,40,135),(b,41,37),(b,41,41), (b,41,49),(b,41,127),(b,42,21),(b,42,30),(b,42,42),(b,42,107), (b,43,5),(b,43,14),(b,43,43),(b,43,83),(b,44,40),(b,44,44), (b,44,57),(b,44,135),(b,45,36),(b,45,45),(b,45,53),(b,45,131), (b,46,20),(b,46,34),(b,46,46),(b,46,111),(b,47,4),(b,47,18), (b,47,47),(b,47,87),(b,48,48),(b,48,52),(b,48,56),(b,48,139), (b,49,37),(b,49,41),(b,49,49),(b,49,127),(b,50,25),(b,50,29), (b,50,50),(b,50,115),(b,51,9),(b,51,13),(b,51,51),(b,51,91), (b,52,48),(b,52,52),(b,52,56),(b,52,139),(b,53,36),(b,53,45), (b,53,53),(b,53,131),(b,54,24),(b,54,33),(b,54,54),(b,54,119), (b,55,8),(b,55,17),(b,55,55),(b,55,95),(b,56,48),(b,56,52), (b,56,56),(b,56,139),(b,57,40),(b,57,44),(b,57,57),(b,57,135), (b,58,28),(b,58,32),(b,58,58),(b,58,123),(b,59,12),(b,59,16), (b,59,59),(b,59,99),(b,60,60),(b,60,74),(b,60,86),(b,60,110), (b,61,61),(b,61,70),(b,61,82),(b,61,106),(b,62,62),(b,62,66), (b,62,78),(b,62,102),(b,63,3),(b,63,7),(b,63,23),(b,63,63), (b,64,64),(b,64,73),(b,64,94),(b,64,118),(b,65,65),(b,65,69), (b,65,90),(b,65,114),(b,66,62),(b,66,66),(b,66,78),(b,66,102), (b,67,2),(b,67,11),(b,67,27),(b,67,67),(b,68,68),(b,68,72), (b,68,98),(b,68,122),(b,69,65),(b,69,69),(b,69,90),(b,69,114), (b,70,61),(b,70,70),(b,70,82),(b,70,106),(b,71,1),(b,71,15), (b,71,31),(b,71,71),(b,72,68),(b,72,72),(b,72,98),(b,72,122), (b,73,64),(b,73,73),(b,73,94),(b,73,118),(b,74,60),(b,74,74), (b,74,86),(b,74,110),(b,75,0),(b,75,19),(b,75,35),(b,75,75), (b,76,76),(b,76,85),(b,76,93),(b,76,130),(b,77,77),(b,77,81), (b,77,89),(b,77,126),(b,78,62),(b,78,66),(b,78,78),(b,78,102), (b,79,6),(b,79,10),(b,79,39),(b,79,79),(b,80,80),(b,80,84), (b,80,97),(b,80,134),(b,81,77),(b,81,81),(b,81,89),(b,81,126), (b,82,61),(b,82,70),(b,82,82),(b,82,106),(b,83,5),(b,83,14), (b,83,43),(b,83,83),(b,84,80),(b,84,84),(b,84,97),(b,84,134), (b,85,76),(b,85,85),(b,85,93),(b,85,130),(b,86,60),(b,86,74), (b,86,86),(b,86,110),(b,87,4),(b,87,18),(b,87,47),(b,87,87), (b,88,88),(b,88,92),(b,88,96),(b,88,138),(b,89,77),(b,89,81), (b,89,89),(b,89,126),(b,90,65),(b,90,69),(b,90,90),(b,90,114), (b,91,9),(b,91,13),(b,91,51),(b,91,91),(b,92,88),(b,92,92), (b,92,96),(b,92,138),(b,93,76),(b,93,85),(b,93,93),(b,93,130), (b,94,64),(b,94,73),(b,94,94),(b,94,118),(b,95,8),(b,95,17), (b,95,55),(b,95,95),(b,96,88),(b,96,92),(b,96,96),(b,96,138), (b,97,80),(b,97,84),(b,97,97),(b,97,134),(b,98,68),(b,98,72), (b,98,98),(b,98,122),(b,99,12),(b,99,16),(b,99,59),(b,99,99), (b,100,100),(b,100,109),(b,100,117),(b,100,129),(b,101,101),(b,101,105), (b,101,113),(b,101,125),(b,102,62),(b,102,66),(b,102,78),(b,102,102), (b,103,22),(b,103,26),(b,103,38),(b,103,103),(b,104,104),(b,104,108), (b,104,121),(b,104,133),(b,105,101),(b,105,105),(b,105,113),(b,105,125), (b,106,61),(b,106,70),(b,106,82),(b,106,106),(b,107,21),(b,107,30), (b,107,42),(b,107,107),(b,108,104),(b,108,108),(b,108,121),(b,108,133), (b,109,100),(b,109,109),(b,109,117),(b,109,129),(b,110,60),(b,110,74), (b,110,86),(b,110,110),(b,111,20),(b,111,34),(b,111,46),(b,111,111), (b,112,112),(b,112,116),(b,112,120),(b,112,137),(b,113,101),(b,113,105), (b,113,113),(b,113,125),(b,114,65),(b,114,69),(b,114,90),(b,114,114), (b,115,25),(b,115,29),(b,115,50),(b,115,115),(b,116,112),(b,116,116), (b,116,120),(b,116,137),(b,117,100),(b,117,109),(b,117,117),(b,117,129), (b,118,64),(b,118,73),(b,118,94),(b,118,118),(b,119,24),(b,119,33), (b,119,54),(b,119,119),(b,120,112),(b,120,116),(b,120,120),(b,120,137), (b,121,104),(b,121,108),(b,121,121),(b,121,133),(b,122,68),(b,122,72), (b,122,98),(b,122,122),(b,123,28),(b,123,32),(b,123,58),(b,123,123), (b,124,124),(b,124,128),(b,124,132),(b,124,136),(b,125,101),(b,125,105), (b,125,113),(b,125,125),(b,126,77),(b,126,81),(b,126,89),(b,126,126), (b,127,37),(b,127,41),(b,127,49),(b,127,127),(b,128,124),(b,128,128), (b,128,132),(b,128,136),(b,129,100),(b,129,109),(b,129,117),(b,129,129), (b,130,76),(b,130,85),(b,130,93),(b,130,130),(b,131,36),(b,131,45), (b,131,53),(b,131,131),(b,132,124),(b,132,128),(b,132,132),(b,132,136), (b,133,104),(b,133,108),(b,133,121),(b,133,133),(b,134,80),(b,134,84), (b,134,97),(b,134,134),(b,135,40),(b,135,44),(b,135,57),(b,135,135), (b,136,124),(b,136,128),(b,136,132),(b,136,136),(b,137,112),(b,137,116), (b,137,120),(b,137,137),(b,138,88),(b,138,92),(b,138,96),(b,138,138), (b,139,48),(b,139,52),(b,139,56),(b,139,139),(c,0,0),(c,0,4), (c,0,8),(c,0,12),(c,0,20),(c,0,24),(c,0,28),(c,0,36), (c,0,40),(c,0,48),(c,0,60),(c,0,64),(c,0,68),(c,0,76), (c,0,80),(c,0,88),(c,0,100),(c,0,104),(c,0,112),(c,0,124), (c,1,1),(c,1,5),(c,1,9),(c,1,16),(c,1,21),(c,1,25), (c,1,32),(c,1,37),(c,1,44),(c,1,52),(c,1,61),(c,1,65), (c,1,72),(c,1,77),(c,1,84),(c,1,92),(c,1,101),(c,1,108), (c,1,116),(c,1,128),(c,2,2),(c,2,6),(c,2,13),(c,2,17), (c,2,22),(c,2,29),(c,2,33),(c,2,41),(c,2,45),(c,2,56), (c,2,62),(c,2,69),(c,2,73),(c,2,81),(c,2,85),(c,2,96), (c,2,105),(c,2,109),(c,2,120),(c,2,132),(c,3,3),(c,3,10), (c,3,14),(c,3,18),(c,3,26),(c,3,30),(c,3,34),(c,3,49), (c,3,53),(c,3,57),(c,3,66),(c,3,70),(c,3,74),(c,3,89), (c,3,93),(c,3,97),(c,3,113),(c,3,117),(c,3,121),(c,3,136), (c,4,0),(c,4,4),(c,4,8),(c,4,12),(c,4,20),(c,4,24), (c,4,28),(c,4,36),(c,4,40),(c,4,48),(c,4,60),(c,4,64), (c,4,68),(c,4,76),(c,4,80),(c,4,88),(c,4,100),(c,4,104), (c,4,112),(c,4,124),(c,5,1),(c,5,5),(c,5,9),(c,5,16), (c,5,21),(c,5,25),(c,5,32),(c,5,37),(c,5,44),(c,5,52), (c,5,61),(c,5,65),(c,5,72),(c,5,77),(c,5,84),(c,5,92), (c,5,101),(c,5,108),(c,5,116),(c,5,128),(c,6,2),(c,6,6), (c,6,13),(c,6,17),(c,6,22),(c,6,29),(c,6,33),(c,6,41), (c,6,45),(c,6,56),(c,6,62),(c,6,69),(c,6,73),(c,6,81), (c,6,85),(c,6,96),(c,6,105),(c,6,109),(c,6,120),(c,6,132), (c,7,7),(c,7,11),(c,7,15),(c,7,19),(c,7,38),(c,7,42), (c,7,46),(c,7,50),(c,7,54),(c,7,58),(c,7,78),(c,7,82), (c,7,86),(c,7,90),(c,7,94),(c,7,98),(c,7,125),(c,7,129), (c,7,133),(c,7,137),(c,8,0),(c,8,4),(c,8,8),(c,8,12), (c,8,20),(c,8,24),(c,8,28),(c,8,36),(c,8,40),(c,8,48), (c,8,60),(c,8,64),(c,8,68),(c,8,76),(c,8,80),(c,8,88), (c,8,100),(c,8,104),(c,8,112),(c,8,124),(c,9,1),(c,9,5), (c,9,9),(c,9,16),(c,9,21),(c,9,25),(c,9,32),(c,9,37), (c,9,44),(c,9,52),(c,9,61),(c,9,65),(c,9,72),(c,9,77), (c,9,84),(c,9,92),(c,9,101),(c,9,108),(c,9,116),(c,9,128), (c,10,3),(c,10,10),(c,10,14),(c,10,18),(c,10,26),(c,10,30), (c,10,34),(c,10,49),(c,10,53),(c,10,57),(c,10,66),(c,10,70), (c,10,74),(c,10,89),(c,10,93),(c,10,97),(c,10,113),(c,10,117), (c,10,121),(c,10,136),(c,11,7),(c,11,11),(c,11,15),(c,11,19), (c,11,38),(c,11,42),(c,11,46),(c,11,50),(c,11,54),(c,11,58), (c,11,78),(c,11,82),(c,11,86),(c,11,90),(c,11,94),(c,11,98), (c,11,125),(c,11,129),(c,11,133),(c,11,137),(c,12,0),(c,12,4), (c,12,8),(c,12,12),(c,12,20),(c,12,24),(c,12,28),(c,12,36), (c,12,40),(c,12,48),(c,12,60),(c,12,64),(c,12,68),(c,12,76), (c,12,80),(c,12,88),(c,12,100),(c,12,104),(c,12,112),(c,12,124), (c,13,2),(c,13,6),(c,13,13),(c,13,17),(c,13,22),(c,13,29), (c,13,33),(c,13,41),(c,13,45),(c,13,56),(c,13,62),(c,13,69), (c,13,73),(c,13,81),(c,13,85),(c,13,96),(c,13,105),(c,13,109), (c,13,120),(c,13,132),(c,14,3),(c,14,10),(c,14,14),(c,14,18), (c,14,26),(c,14,30),(c,14,34),(c,14,49),(c,14,53),(c,14,57), (c,14,66),(c,14,70),(c,14,74),(c,14,89),(c,14,93),(c,14,97), (c,14,113),(c,14,117),(c,14,121),(c,14,136),(c,15,7),(c,15,11), (c,15,15),(c,15,19),(c,15,38),(c,15,42),(c,15,46),(c,15,50), (c,15,54),(c,15,58),(c,15,78),(c,15,82),(c,15,86),(c,15,90), (c,15,94),(c,15,98),(c,15,125),(c,15,129),(c,15,133),(c,15,137), (c,16,1),(c,16,5),(c,16,9),(c,16,16),(c,16,21),(c,16,25), (c,16,32),(c,16,37),(c,16,44),(c,16,52),(c,16,61),(c,16,65), (c,16,72),(c,16,77),(c,16,84),(c,16,92),(c,16,101),(c,16,108), (c,16,116),(c,16,128),(c,17,2),(c,17,6),(c,17,13),(c,17,17), (c,17,22),(c,17,29),(c,17,33),(c,17,41),(c,17,45),(c,17,56), (c,17,62),(c,17,69),(c,17,73),(c,17,81),(c,17,85),(c,17,96), (c,17,105),(c,17,109),(c,17,120),(c,17,132),(c,18,3),(c,18,10), (c,18,14),(c,18,18),(c,18,26),(c,18,30),(c,18,34),(c,18,49), (c,18,53),(c,18,57),(c,18,66),(c,18,70),(c,18,74),(c,18,89), (c,18,93),(c,18,97),(c,18,113),(c,18,117),(c,18,121),(c,18,136), (c,19,7),(c,19,11),(c,19,15),(c,19,19),(c,19,38),(c,19,42), (c,19,46),(c,19,50),(c,19,54),(c,19,58),(c,19,78),(c,19,82), (c,19,86),(c,19,90),(c,19,94),(c,19,98),(c,19,125),(c,19,129), (c,19,133),(c,19,137),(c,20,0),(c,20,4),(c,20,8),(c,20,12), (c,20,20),(c,20,24),(c,20,28),(c,20,36),(c,20,40),(c,20,48), (c,20,60),(c,20,64),(c,20,68),(c,20,76),(c,20,80),(c,20,88), (c,20,100),(c,20,104),(c,20,112),(c,20,124),(c,21,1),(c,21,5), (c,21,9),(c,21,16),(c,21,21),(c,21,25),(c,21,32),(c,21,37), (c,21,44),(c,21,52),(c,21,61),(c,21,65),(c,21,72),(c,21,77), (c,21,84),(c,21,92),(c,21,101),(c,21,108),(c,21,116),(c,21,128), (c,22,2),(c,22,6),(c,22,13),(c,22,17),(c,22,22),(c,22,29), (c,22,33),(c,22,41),(c,22,45),(c,22,56),(c,22,62),(c,22,69), (c,22,73),(c,22,81),(c,22,85),(c,22,96),(c,22,105),(c,22,109), (c,22,120),(c,22,132),(c,23,23),(c,23,27),(c,23,31),(c,23,35), (c,23,39),(c,23,43),(c,23,47),(c,23,51),(c,23,55),(c,23,59), (c,23,102),(c,23,106),(c,23,110),(c,23,114),(c,23,118),(c,23,122), (c,23,126),(c,23,130),(c,23,134),(c,23,138),(c,24,0),(c,24,4), (c,24,8),(c,24,12),(c,24,20),(c,24,24),(c,24,28),(c,24,36), (c,24,40),(c,24,48),(c,24,60),(c,24,64),(c,24,68),(c,24,76), (c,24,80),(c,24,88),(c,24,100),(c,24,104),(c,24,112),(c,24,124), (c,25,1),(c,25,5),(c,25,9),(c,25,16),(c,25,21),(c,25,25), (c,25,32),(c,25,37),(c,25,44),(c,25,52),(c,25,61),(c,25,65), (c,25,72),(c,25,77),(c,25,84),(c,25,92),(c,25,101),(c,25,108), (c,25,116),(c,25,128),(c,26,3),(c,26,10),(c,26,14),(c,26,18), (c,26,26),(c,26,30),(c,26,34),(c,26,49),(c,26,53),(c,26,57), (c,26,66),(c,26,70),(c,26,74),(c,26,89),(c,26,93),(c,26,97), (c,26,113),(c,26,117),(c,26,121),(c,26,136),(c,27,23),(c,27,27), (c,27,31),(c,27,35),(c,27,39),(c,27,43),(c,27,47),(c,27,51), (c,27,55),(c,27,59),(c,27,102),(c,27,106),(c,27,110),(c,27,114), (c,27,118),(c,27,122),(c,27,126),(c,27,130),(c,27,134),(c,27,138), (c,28,0),(c,28,4),(c,28,8),(c,28,12),(c,28,20),(c,28,24), (c,28,28),(c,28,36),(c,28,40),(c,28,48),(c,28,60),(c,28,64), (c,28,68),(c,28,76),(c,28,80),(c,28,88),(c,28,100),(c,28,104), (c,28,112),(c,28,124),(c,29,2),(c,29,6),(c,29,13),(c,29,17), (c,29,22),(c,29,29),(c,29,33),(c,29,41),(c,29,45),(c,29,56), (c,29,62),(c,29,69),(c,29,73),(c,29,81),(c,29,85),(c,29,96), (c,29,105),(c,29,109),(c,29,120),(c,29,132),(c,30,3),(c,30,10), (c,30,14),(c,30,18),(c,30,26),(c,30,30),(c,30,34),(c,30,49), (c,30,53),(c,30,57),(c,30,66),(c,30,70),(c,30,74),(c,30,89), (c,30,93),(c,30,97),(c,30,113),(c,30,117),(c,30,121),(c,30,136), (c,31,23),(c,31,27),(c,31,31),(c,31,35),(c,31,39),(c,31,43), (c,31,47),(c,31,51),(c,31,55),(c,31,59),(c,31,102),(c,31,106), (c,31,110),(c,31,114),(c,31,118),(c,31,122),(c,31,126),(c,31,130), (c,31,134),(c,31,138),(c,32,1),(c,32,5),(c,32,9),(c,32,16), (c,32,21),(c,32,25),(c,32,32),(c,32,37),(c,32,44),(c,32,52), (c,32,61),(c,32,65),(c,32,72),(c,32,77),(c,32,84),(c,32,92), (c,32,101),(c,32,108),(c,32,116),(c,32,128),(c,33,2),(c,33,6), (c,33,13),(c,33,17),(c,33,22),(c,33,29),(c,33,33),(c,33,41), (c,33,45),(c,33,56),(c,33,62),(c,33,69),(c,33,73),(c,33,81), (c,33,85),(c,33,96),(c,33,105),(c,33,109),(c,33,120),(c,33,132), (c,34,3),(c,34,10),(c,34,14),(c,34,18),(c,34,26),(c,34,30), (c,34,34),(c,34,49),(c,34,53),(c,34,57),(c,34,66),(c,34,70), (c,34,74),(c,34,89),(c,34,93),(c,34,97),(c,34,113),(c,34,117), (c,34,121),(c,34,136),(c,35,23),(c,35,27),(c,35,31),(c,35,35), (c,35,39),(c,35,43),(c,35,47),(c,35,51),(c,35,55),(c,35,59), (c,35,102),(c,35,106),(c,35,110),(c,35,114),(c,35,118),(c,35,122), (c,35,126),(c,35,130),(c,35,134),(c,35,138),(c,36,0),(c,36,4), (c,36,8),(c,36,12),(c,36,20),(c,36,24),(c,36,28),(c,36,36), (c,36,40),(c,36,48),(c,36,60),(c,36,64),(c,36,68),(c,36,76), (c,36,80),(c,36,88),(c,36,100),(c,36,104),(c,36,112),(c,36,124), (c,37,1),(c,37,5),(c,37,9),(c,37,16),(c,37,21),(c,37,25), (c,37,32),(c,37,37),(c,37,44),(c,37,52),(c,37,61),(c,37,65), (c,37,72),(c,37,77),(c,37,84),(c,37,92),(c,37,101),(c,37,108), (c,37,116),(c,37,128),(c,38,7),(c,38,11),(c,38,15),(c,38,19), (c,38,38),(c,38,42),(c,38,46),(c,38,50),(c,38,54),(c,38,58), (c,38,78),(c,38,82),(c,38,86),(c,38,90),(c,38,94),(c,38,98), (c,38,125),(c,38,129),(c,38,133),(c,38,137),(c,39,23),(c,39,27), (c,39,31),(c,39,35),(c,39,39),(c,39,43),(c,39,47),(c,39,51), (c,39,55),(c,39,59),(c,39,102),(c,39,106),(c,39,110),(c,39,114), (c,39,118),(c,39,122),(c,39,126),(c,39,130),(c,39,134),(c,39,138), (c,40,0),(c,40,4),(c,40,8),(c,40,12),(c,40,20),(c,40,24), (c,40,28),(c,40,36),(c,40,40),(c,40,48),(c,40,60),(c,40,64), (c,40,68),(c,40,76),(c,40,80),(c,40,88),(c,40,100),(c,40,104), (c,40,112),(c,40,124),(c,41,2),(c,41,6),(c,41,13),(c,41,17), (c,41,22),(c,41,29),(c,41,33),(c,41,41),(c,41,45),(c,41,56), (c,41,62),(c,41,69),(c,41,73),(c,41,81),(c,41,85),(c,41,96), (c,41,105),(c,41,109),(c,41,120),(c,41,132),(c,42,7),(c,42,11), (c,42,15),(c,42,19),(c,42,38),(c,42,42),(c,42,46),(c,42,50), (c,42,54),(c,42,58),(c,42,78),(c,42,82),(c,42,86),(c,42,90), (c,42,94),(c,42,98),(c,42,125),(c,42,129),(c,42,133),(c,42,137), (c,43,23),(c,43,27),(c,43,31),(c,43,35),(c,43,39),(c,43,43), (c,43,47),(c,43,51),(c,43,55),(c,43,59),(c,43,102),(c,43,106), (c,43,110),(c,43,114),(c,43,118),(c,43,122),(c,43,126),(c,43,130), (c,43,134),(c,43,138),(c,44,1),(c,44,5),(c,44,9),(c,44,16), (c,44,21),(c,44,25),(c,44,32),(c,44,37),(c,44,44),(c,44,52), (c,44,61),(c,44,65),(c,44,72),(c,44,77),(c,44,84),(c,44,92), (c,44,101),(c,44,108),(c,44,116),(c,44,128),(c,45,2),(c,45,6), (c,45,13),(c,45,17),(c,45,22),(c,45,29),(c,45,33),(c,45,41), (c,45,45),(c,45,56),(c,45,62),(c,45,69),(c,45,73),(c,45,81), (c,45,85),(c,45,96),(c,45,105),(c,45,109),(c,45,120),(c,45,132), (c,46,7),(c,46,11),(c,46,15),(c,46,19),(c,46,38),(c,46,42), (c,46,46),(c,46,50),(c,46,54),(c,46,58),(c,46,78),(c,46,82), (c,46,86),(c,46,90),(c,46,94),(c,46,98),(c,46,125),(c,46,129), (c,46,133),(c,46,137),(c,47,23),(c,47,27),(c,47,31),(c,47,35), (c,47,39),(c,47,43),(c,47,47),(c,47,51),(c,47,55),(c,47,59), (c,47,102),(c,47,106),(c,47,110),(c,47,114),(c,47,118),(c,47,122), (c,47,126),(c,47,130),(c,47,134),(c,47,138),(c,48,0),(c,48,4), (c,48,8),(c,48,12),(c,48,20),(c,48,24),(c,48,28),(c,48,36), (c,48,40),(c,48,48),(c,48,60),(c,48,64),(c,48,68),(c,48,76), (c,48,80),(c,48,88),(c,48,100),(c,48,104),(c,48,112),(c,48,124), (c,49,3),(c,49,10),(c,49,14),(c,49,18),(c,49,26),(c,49,30), (c,49,34),(c,49,49),(c,49,53),(c,49,57),(c,49,66),(c,49,70), (c,49,74),(c,49,89),(c,49,93),(c,49,97),(c,49,113),(c,49,117), (c,49,121),(c,49,136),(c,50,7),(c,50,11),(c,50,15),(c,50,19), (c,50,38),(c,50,42),(c,50,46),(c,50,50),(c,50,54),(c,50,58), (c,50,78),(c,50,82),(c,50,86),(c,50,90),(c,50,94),(c,50,98), (c,50,125),(c,50,129),(c,50,133),(c,50,137),(c,51,23),(c,51,27), (c,51,31),(c,51,35),(c,51,39),(c,51,43),(c,51,47),(c,51,51), (c,51,55),(c,51,59),(c,51,102),(c,51,106),(c,51,110),(c,51,114), (c,51,118),(c,51,122),(c,51,126),(c,51,130),(c,51,134),(c,51,138), (c,52,1),(c,52,5),(c,52,9),(c,52,16),(c,52,21),(c,52,25), (c,52,32),(c,52,37),(c,52,44),(c,52,52),(c,52,61),(c,52,65), (c,52,72),(c,52,77),(c,52,84),(c,52,92),(c,52,101),(c,52,108), (c,52,116),(c,52,128),(c,53,3),(c,53,10),(c,53,14),(c,53,18), (c,53,26),(c,53,30),(c,53,34),(c,53,49),(c,53,53),(c,53,57), (c,53,66),(c,53,70),(c,53,74),(c,53,89),(c,53,93),(c,53,97), (c,53,113),(c,53,117),(c,53,121),(c,53,136),(c,54,7),(c,54,11), (c,54,15),(c,54,19),(c,54,38),(c,54,42),(c,54,46),(c,54,50), (c,54,54),(c,54,58),(c,54,78),(c,54,82),(c,54,86),(c,54,90), (c,54,94),(c,54,98),(c,54,125),(c,54,129),(c,54,133),(c,54,137), (c,55,23),(c,55,27),(c,55,31),(c,55,35),(c,55,39),(c,55,43), (c,55,47),(c,55,51),(c,55,55),(c,55,59),(c,55,102),(c,55,106), (c,55,110),(c,55,114),(c,55,118),(c,55,122),(c,55,126),(c,55,130), (c,55,134),(c,55,138),(c,56,2),(c,56,6),(c,56,13),(c,56,17), (c,56,22),(c,56,29),(c,56,33),(c,56,41),(c,56,45),(c,56,56), (c,56,62),(c,56,69),(c,56,73),(c,56,81),(c,56,85),(c,56,96), (c,56,105),(c,56,109),(c,56,120),(c,56,132),(c,57,3),(c,57,10), (c,57,14),(c,57,18),(c,57,26),(c,57,30),(c,57,34),(c,57,49), (c,57,53),(c,57,57),(c,57,66),(c,57,70),(c,57,74),(c,57,89), (c,57,93),(c,57,97),(c,57,113),(c,57,117),(c,57,121),(c,57,136), (c,58,7),(c,58,11),(c,58,15),(c,58,19),(c,58,38),(c,58,42), (c,58,46),(c,58,50),(c,58,54),(c,58,58),(c,58,78),(c,58,82), (c,58,86),(c,58,90),(c,58,94),(c,58,98),(c,58,125),(c,58,129), (c,58,133),(c,58,137),(c,59,23),(c,59,27),(c,59,31),(c,59,35), (c,59,39),(c,59,43),(c,59,47),(c,59,51),(c,59,55),(c,59,59), (c,59,102),(c,59,106),(c,59,110),(c,59,114),(c,59,118),(c,59,122), (c,59,126),(c,59,130),(c,59,134),(c,59,138),(c,60,0),(c,60,4), (c,60,8),(c,60,12),(c,60,20),(c,60,24),(c,60,28),(c,60,36), (c,60,40),(c,60,48),(c,60,60),(c,60,64),(c,60,68),(c,60,76), (c,60,80),(c,60,88),(c,60,100),(c,60,104),(c,60,112),(c,60,124), (c,61,1),(c,61,5),(c,61,9),(c,61,16),(c,61,21),(c,61,25), (c,61,32),(c,61,37),(c,61,44),(c,61,52),(c,61,61),(c,61,65), (c,61,72),(c,61,77),(c,61,84),(c,61,92),(c,61,101),(c,61,108), (c,61,116),(c,61,128),(c,62,2),(c,62,6),(c,62,13),(c,62,17), (c,62,22),(c,62,29),(c,62,33),(c,62,41),(c,62,45),(c,62,56), (c,62,62),(c,62,69),(c,62,73),(c,62,81),(c,62,85),(c,62,96), (c,62,105),(c,62,109),(c,62,120),(c,62,132),(c,63,63),(c,63,67), (c,63,71),(c,63,75),(c,63,79),(c,63,83),(c,63,87),(c,63,91), (c,63,95),(c,63,99),(c,63,103),(c,63,107),(c,63,111),(c,63,115), (c,63,119),(c,63,123),(c,63,127),(c,63,131),(c,63,135),(c,63,139), (c,64,0),(c,64,4),(c,64,8),(c,64,12),(c,64,20),(c,64,24), (c,64,28),(c,64,36),(c,64,40),(c,64,48),(c,64,60),(c,64,64), (c,64,68),(c,64,76),(c,64,80),(c,64,88),(c,64,100),(c,64,104), (c,64,112),(c,64,124),(c,65,1),(c,65,5),(c,65,9),(c,65,16), (c,65,21),(c,65,25),(c,65,32),(c,65,37),(c,65,44),(c,65,52), (c,65,61),(c,65,65),(c,65,72),(c,65,77),(c,65,84),(c,65,92), (c,65,101),(c,65,108),(c,65,116),(c,65,128),(c,66,3),(c,66,10), (c,66,14),(c,66,18),(c,66,26),(c,66,30),(c,66,34),(c,66,49), (c,66,53),(c,66,57),(c,66,66),(c,66,70),(c,66,74),(c,66,89), (c,66,93),(c,66,97),(c,66,113),(c,66,117),(c,66,121),(c,66,136), (c,67,63),(c,67,67),(c,67,71),(c,67,75),(c,67,79),(c,67,83), (c,67,87),(c,67,91),(c,67,95),(c,67,99),(c,67,103),(c,67,107), (c,67,111),(c,67,115),(c,67,119),(c,67,123),(c,67,127),(c,67,131), (c,67,135),(c,67,139),(c,68,0),(c,68,4),(c,68,8),(c,68,12), (c,68,20),(c,68,24),(c,68,28),(c,68,36),(c,68,40),(c,68,48), (c,68,60),(c,68,64),(c,68,68),(c,68,76),(c,68,80),(c,68,88), (c,68,100),(c,68,104),(c,68,112),(c,68,124),(c,69,2),(c,69,6), (c,69,13),(c,69,17),(c,69,22),(c,69,29),(c,69,33),(c,69,41), (c,69,45),(c,69,56),(c,69,62),(c,69,69),(c,69,73),(c,69,81), (c,69,85),(c,69,96),(c,69,105),(c,69,109),(c,69,120),(c,69,132), (c,70,3),(c,70,10),(c,70,14),(c,70,18),(c,70,26),(c,70,30), (c,70,34),(c,70,49),(c,70,53),(c,70,57),(c,70,66),(c,70,70), (c,70,74),(c,70,89),(c,70,93),(c,70,97),(c,70,113),(c,70,117), (c,70,121),(c,70,136),(c,71,63),(c,71,67),(c,71,71),(c,71,75), (c,71,79),(c,71,83),(c,71,87),(c,71,91),(c,71,95),(c,71,99), (c,71,103),(c,71,107),(c,71,111),(c,71,115),(c,71,119),(c,71,123), (c,71,127),(c,71,131),(c,71,135),(c,71,139),(c,72,1),(c,72,5), (c,72,9),(c,72,16),(c,72,21),(c,72,25),(c,72,32),(c,72,37), (c,72,44),(c,72,52),(c,72,61),(c,72,65),(c,72,72),(c,72,77), (c,72,84),(c,72,92),(c,72,101),(c,72,108),(c,72,116),(c,72,128), (c,73,2),(c,73,6),(c,73,13),(c,73,17),(c,73,22),(c,73,29), (c,73,33),(c,73,41),(c,73,45),(c,73,56),(c,73,62),(c,73,69), (c,73,73),(c,73,81),(c,73,85),(c,73,96),(c,73,105),(c,73,109), (c,73,120),(c,73,132),(c,74,3),(c,74,10),(c,74,14),(c,74,18), (c,74,26),(c,74,30),(c,74,34),(c,74,49),(c,74,53),(c,74,57), (c,74,66),(c,74,70),(c,74,74),(c,74,89),(c,74,93),(c,74,97), (c,74,113),(c,74,117),(c,74,121),(c,74,136),(c,75,63),(c,75,67), (c,75,71),(c,75,75),(c,75,79),(c,75,83),(c,75,87),(c,75,91), (c,75,95),(c,75,99),(c,75,103),(c,75,107),(c,75,111),(c,75,115), (c,75,119),(c,75,123),(c,75,127),(c,75,131),(c,75,135),(c,75,139), (c,76,0),(c,76,4),(c,76,8),(c,76,12),(c,76,20),(c,76,24), (c,76,28),(c,76,36),(c,76,40),(c,76,48),(c,76,60),(c,76,64), (c,76,68),(c,76,76),(c,76,80),(c,76,88),(c,76,100),(c,76,104), (c,76,112),(c,76,124),(c,77,1),(c,77,5),(c,77,9),(c,77,16), (c,77,21),(c,77,25),(c,77,32),(c,77,37),(c,77,44),(c,77,52), (c,77,61),(c,77,65),(c,77,72),(c,77,77),(c,77,84),(c,77,92), (c,77,101),(c,77,108),(c,77,116),(c,77,128),(c,78,7),(c,78,11), (c,78,15),(c,78,19),(c,78,38),(c,78,42),(c,78,46),(c,78,50), (c,78,54),(c,78,58),(c,78,78),(c,78,82),(c,78,86),(c,78,90), (c,78,94),(c,78,98),(c,78,125),(c,78,129),(c,78,133),(c,78,137), (c,79,63),(c,79,67),(c,79,71),(c,79,75),(c,79,79),(c,79,83), (c,79,87),(c,79,91),(c,79,95),(c,79,99),(c,79,103),(c,79,107), (c,79,111),(c,79,115),(c,79,119),(c,79,123),(c,79,127),(c,79,131), (c,79,135),(c,79,139),(c,80,0),(c,80,4),(c,80,8),(c,80,12), (c,80,20),(c,80,24),(c,80,28),(c,80,36),(c,80,40),(c,80,48), (c,80,60),(c,80,64),(c,80,68),(c,80,76),(c,80,80),(c,80,88), (c,80,100),(c,80,104),(c,80,112),(c,80,124),(c,81,2),(c,81,6), (c,81,13),(c,81,17),(c,81,22),(c,81,29),(c,81,33),(c,81,41), (c,81,45),(c,81,56),(c,81,62),(c,81,69),(c,81,73),(c,81,81), (c,81,85),(c,81,96),(c,81,105),(c,81,109),(c,81,120),(c,81,132), (c,82,7),(c,82,11),(c,82,15),(c,82,19),(c,82,38),(c,82,42), (c,82,46),(c,82,50),(c,82,54),(c,82,58),(c,82,78),(c,82,82), (c,82,86),(c,82,90),(c,82,94),(c,82,98),(c,82,125),(c,82,129), (c,82,133),(c,82,137),(c,83,63),(c,83,67),(c,83,71),(c,83,75), (c,83,79),(c,83,83),(c,83,87),(c,83,91),(c,83,95),(c,83,99), (c,83,103),(c,83,107),(c,83,111),(c,83,115),(c,83,119),(c,83,123), (c,83,127),(c,83,131),(c,83,135),(c,83,139),(c,84,1),(c,84,5), (c,84,9),(c,84,16),(c,84,21),(c,84,25),(c,84,32),(c,84,37), (c,84,44),(c,84,52),(c,84,61),(c,84,65),(c,84,72),(c,84,77), (c,84,84),(c,84,92),(c,84,101),(c,84,108),(c,84,116),(c,84,128), (c,85,2),(c,85,6),(c,85,13),(c,85,17),(c,85,22),(c,85,29), (c,85,33),(c,85,41),(c,85,45),(c,85,56),(c,85,62),(c,85,69), (c,85,73),(c,85,81),(c,85,85),(c,85,96),(c,85,105),(c,85,109), (c,85,120),(c,85,132),(c,86,7),(c,86,11),(c,86,15),(c,86,19), (c,86,38),(c,86,42),(c,86,46),(c,86,50),(c,86,54),(c,86,58), (c,86,78),(c,86,82),(c,86,86),(c,86,90),(c,86,94),(c,86,98), (c,86,125),(c,86,129),(c,86,133),(c,86,137),(c,87,63),(c,87,67), (c,87,71),(c,87,75),(c,87,79),(c,87,83),(c,87,87),(c,87,91), (c,87,95),(c,87,99),(c,87,103),(c,87,107),(c,87,111),(c,87,115), (c,87,119),(c,87,123),(c,87,127),(c,87,131),(c,87,135),(c,87,139), (c,88,0),(c,88,4),(c,88,8),(c,88,12),(c,88,20),(c,88,24), (c,88,28),(c,88,36),(c,88,40),(c,88,48),(c,88,60),(c,88,64), (c,88,68),(c,88,76),(c,88,80),(c,88,88),(c,88,100),(c,88,104), (c,88,112),(c,88,124),(c,89,3),(c,89,10),(c,89,14),(c,89,18), (c,89,26),(c,89,30),(c,89,34),(c,89,49),(c,89,53),(c,89,57), (c,89,66),(c,89,70),(c,89,74),(c,89,89),(c,89,93),(c,89,97), (c,89,113),(c,89,117),(c,89,121),(c,89,136),(c,90,7),(c,90,11), (c,90,15),(c,90,19),(c,90,38),(c,90,42),(c,90,46),(c,90,50), (c,90,54),(c,90,58),(c,90,78),(c,90,82),(c,90,86),(c,90,90), (c,90,94),(c,90,98),(c,90,125),(c,90,129),(c,90,133),(c,90,137), (c,91,63),(c,91,67),(c,91,71),(c,91,75),(c,91,79),(c,91,83), (c,91,87),(c,91,91),(c,91,95),(c,91,99),(c,91,103),(c,91,107), (c,91,111),(c,91,115),(c,91,119),(c,91,123),(c,91,127),(c,91,131), (c,91,135),(c,91,139),(c,92,1),(c,92,5),(c,92,9),(c,92,16), (c,92,21),(c,92,25),(c,92,32),(c,92,37),(c,92,44),(c,92,52), (c,92,61),(c,92,65),(c,92,72),(c,92,77),(c,92,84),(c,92,92), (c,92,101),(c,92,108),(c,92,116),(c,92,128),(c,93,3),(c,93,10), (c,93,14),(c,93,18),(c,93,26),(c,93,30),(c,93,34),(c,93,49), (c,93,53),(c,93,57),(c,93,66),(c,93,70),(c,93,74),(c,93,89), (c,93,93),(c,93,97),(c,93,113),(c,93,117),(c,93,121),(c,93,136), (c,94,7),(c,94,11),(c,94,15),(c,94,19),(c,94,38),(c,94,42), (c,94,46),(c,94,50),(c,94,54),(c,94,58),(c,94,78),(c,94,82), (c,94,86),(c,94,90),(c,94,94),(c,94,98),(c,94,125),(c,94,129), (c,94,133),(c,94,137),(c,95,63),(c,95,67),(c,95,71),(c,95,75), (c,95,79),(c,95,83),(c,95,87),(c,95,91),(c,95,95),(c,95,99), (c,95,103),(c,95,107),(c,95,111),(c,95,115),(c,95,119),(c,95,123), (c,95,127),(c,95,131),(c,95,135),(c,95,139),(c,96,2),(c,96,6), (c,96,13),(c,96,17),(c,96,22),(c,96,29),(c,96,33),(c,96,41), (c,96,45),(c,96,56),(c,96,62),(c,96,69),(c,96,73),(c,96,81), (c,96,85),(c,96,96),(c,96,105),(c,96,109),(c,96,120),(c,96,132), (c,97,3),(c,97,10),(c,97,14),(c,97,18),(c,97,26),(c,97,30), (c,97,34),(c,97,49),(c,97,53),(c,97,57),(c,97,66),(c,97,70), (c,97,74),(c,97,89),(c,97,93),(c,97,97),(c,97,113),(c,97,117), (c,97,121),(c,97,136),(c,98,7),(c,98,11),(c,98,15),(c,98,19), (c,98,38),(c,98,42),(c,98,46),(c,98,50),(c,98,54),(c,98,58), (c,98,78),(c,98,82),(c,98,86),(c,98,90),(c,98,94),(c,98,98), (c,98,125),(c,98,129),(c,98,133),(c,98,137),(c,99,63),(c,99,67), (c,99,71),(c,99,75),(c,99,79),(c,99,83),(c,99,87),(c,99,91), (c,99,95),(c,99,99),(c,99,103),(c,99,107),(c,99,111),(c,99,115), (c,99,119),(c,99,123),(c,99,127),(c,99,131),(c,99,135),(c,99,139), (c,100,0),(c,100,4),(c,100,8),(c,100,12),(c,100,20),(c,100,24), (c,100,28),(c,100,36),(c,100,40),(c,100,48),(c,100,60),(c,100,64), (c,100,68),(c,100,76),(c,100,80),(c,100,88),(c,100,100),(c,100,104), (c,100,112),(c,100,124),(c,101,1),(c,101,5),(c,101,9),(c,101,16), (c,101,21),(c,101,25),(c,101,32),(c,101,37),(c,101,44),(c,101,52), (c,101,61),(c,101,65),(c,101,72),(c,101,77),(c,101,84),(c,101,92), (c,101,101),(c,101,108),(c,101,116),(c,101,128),(c,102,23),(c,102,27), (c,102,31),(c,102,35),(c,102,39),(c,102,43),(c,102,47),(c,102,51), (c,102,55),(c,102,59),(c,102,102),(c,102,106),(c,102,110),(c,102,114), (c,102,118),(c,102,122),(c,102,126),(c,102,130),(c,102,134),(c,102,138), (c,103,63),(c,103,67),(c,103,71),(c,103,75),(c,103,79),(c,103,83), (c,103,87),(c,103,91),(c,103,95),(c,103,99),(c,103,103),(c,103,107), (c,103,111),(c,103,115),(c,103,119),(c,103,123),(c,103,127),(c,103,131), (c,103,135),(c,103,139),(c,104,0),(c,104,4),(c,104,8),(c,104,12), (c,104,20),(c,104,24),(c,104,28),(c,104,36),(c,104,40),(c,104,48), (c,104,60),(c,104,64),(c,104,68),(c,104,76),(c,104,80),(c,104,88), (c,104,100),(c,104,104),(c,104,112),(c,104,124),(c,105,2),(c,105,6), (c,105,13),(c,105,17),(c,105,22),(c,105,29),(c,105,33),(c,105,41), (c,105,45),(c,105,56),(c,105,62),(c,105,69),(c,105,73),(c,105,81), (c,105,85),(c,105,96),(c,105,105),(c,105,109),(c,105,120),(c,105,132), (c,106,23),(c,106,27),(c,106,31),(c,106,35),(c,106,39),(c,106,43), (c,106,47),(c,106,51),(c,106,55),(c,106,59),(c,106,102),(c,106,106), (c,106,110),(c,106,114),(c,106,118),(c,106,122),(c,106,126),(c,106,130), (c,106,134),(c,106,138),(c,107,63),(c,107,67),(c,107,71),(c,107,75), (c,107,79),(c,107,83),(c,107,87),(c,107,91),(c,107,95),(c,107,99), (c,107,103),(c,107,107),(c,107,111),(c,107,115),(c,107,119),(c,107,123), (c,107,127),(c,107,131),(c,107,135),(c,107,139),(c,108,1),(c,108,5), (c,108,9),(c,108,16),(c,108,21),(c,108,25),(c,108,32),(c,108,37), (c,108,44),(c,108,52),(c,108,61),(c,108,65),(c,108,72),(c,108,77), (c,108,84),(c,108,92),(c,108,101),(c,108,108),(c,108,116),(c,108,128), (c,109,2),(c,109,6),(c,109,13),(c,109,17),(c,109,22),(c,109,29), (c,109,33),(c,109,41),(c,109,45),(c,109,56),(c,109,62),(c,109,69), (c,109,73),(c,109,81),(c,109,85),(c,109,96),(c,109,105),(c,109,109), (c,109,120),(c,109,132),(c,110,23),(c,110,27),(c,110,31),(c,110,35), (c,110,39),(c,110,43),(c,110,47),(c,110,51),(c,110,55),(c,110,59), (c,110,102),(c,110,106),(c,110,110),(c,110,114),(c,110,118),(c,110,122), (c,110,126),(c,110,130),(c,110,134),(c,110,138),(c,111,63),(c,111,67), (c,111,71),(c,111,75),(c,111,79),(c,111,83),(c,111,87),(c,111,91), (c,111,95),(c,111,99),(c,111,103),(c,111,107),(c,111,111),(c,111,115), (c,111,119),(c,111,123),(c,111,127),(c,111,131),(c,111,135),(c,111,139), (c,112,0),(c,112,4),(c,112,8),(c,112,12),(c,112,20),(c,112,24), (c,112,28),(c,112,36),(c,112,40),(c,112,48),(c,112,60),(c,112,64), (c,112,68),(c,112,76),(c,112,80),(c,112,88),(c,112,100),(c,112,104), (c,112,112),(c,112,124),(c,113,3),(c,113,10),(c,113,14),(c,113,18), (c,113,26),(c,113,30),(c,113,34),(c,113,49),(c,113,53),(c,113,57), (c,113,66),(c,113,70),(c,113,74),(c,113,89),(c,113,93),(c,113,97), (c,113,113),(c,113,117),(c,113,121),(c,113,136),(c,114,23),(c,114,27), (c,114,31),(c,114,35),(c,114,39),(c,114,43),(c,114,47),(c,114,51), (c,114,55),(c,114,59),(c,114,102),(c,114,106),(c,114,110),(c,114,114), (c,114,118),(c,114,122),(c,114,126),(c,114,130),(c,114,134),(c,114,138), (c,115,63),(c,115,67),(c,115,71),(c,115,75),(c,115,79),(c,115,83), (c,115,87),(c,115,91),(c,115,95),(c,115,99),(c,115,103),(c,115,107), (c,115,111),(c,115,115),(c,115,119),(c,115,123),(c,115,127),(c,115,131), (c,115,135),(c,115,139),(c,116,1),(c,116,5),(c,116,9),(c,116,16), (c,116,21),(c,116,25),(c,116,32),(c,116,37),(c,116,44),(c,116,52), (c,116,61),(c,116,65),(c,116,72),(c,116,77),(c,116,84),(c,116,92), (c,116,101),(c,116,108),(c,116,116),(c,116,128),(c,117,3),(c,117,10), (c,117,14),(c,117,18),(c,117,26),(c,117,30),(c,117,34),(c,117,49), (c,117,53),(c,117,57),(c,117,66),(c,117,70),(c,117,74),(c,117,89), (c,117,93),(c,117,97),(c,117,113),(c,117,117),(c,117,121),(c,117,136), (c,118,23),(c,118,27),(c,118,31),(c,118,35),(c,118,39),(c,118,43), (c,118,47),(c,118,51),(c,118,55),(c,118,59),(c,118,102),(c,118,106), (c,118,110),(c,118,114),(c,118,118),(c,118,122),(c,118,126),(c,118,130), (c,118,134),(c,118,138),(c,119,63),(c,119,67),(c,119,71),(c,119,75), (c,119,79),(c,119,83),(c,119,87),(c,119,91),(c,119,95),(c,119,99), (c,119,103),(c,119,107),(c,119,111),(c,119,115),(c,119,119),(c,119,123), (c,119,127),(c,119,131),(c,119,135),(c,119,139),(c,120,2),(c,120,6), (c,120,13),(c,120,17),(c,120,22),(c,120,29),(c,120,33),(c,120,41), (c,120,45),(c,120,56),(c,120,62),(c,120,69),(c,120,73),(c,120,81), (c,120,85),(c,120,96),(c,120,105),(c,120,109),(c,120,120),(c,120,132), (c,121,3),(c,121,10),(c,121,14),(c,121,18),(c,121,26),(c,121,30), (c,121,34),(c,121,49),(c,121,53),(c,121,57),(c,121,66),(c,121,70), (c,121,74),(c,121,89),(c,121,93),(c,121,97),(c,121,113),(c,121,117), (c,121,121),(c,121,136),(c,122,23),(c,122,27),(c,122,31),(c,122,35), (c,122,39),(c,122,43),(c,122,47),(c,122,51),(c,122,55),(c,122,59), (c,122,102),(c,122,106),(c,122,110),(c,122,114),(c,122,118),(c,122,122), (c,122,126),(c,122,130),(c,122,134),(c,122,138),(c,123,63),(c,123,67), (c,123,71),(c,123,75),(c,123,79),(c,123,83),(c,123,87),(c,123,91), (c,123,95),(c,123,99),(c,123,103),(c,123,107),(c,123,111),(c,123,115), (c,123,119),(c,123,123),(c,123,127),(c,123,131),(c,123,135),(c,123,139), (c,124,0),(c,124,4),(c,124,8),(c,124,12),(c,124,20),(c,124,24), (c,124,28),(c,124,36),(c,124,40),(c,124,48),(c,124,60),(c,124,64), (c,124,68),(c,124,76),(c,124,80),(c,124,88),(c,124,100),(c,124,104), (c,124,112),(c,124,124),(c,125,7),(c,125,11),(c,125,15),(c,125,19), (c,125,38),(c,125,42),(c,125,46),(c,125,50),(c,125,54),(c,125,58), (c,125,78),(c,125,82),(c,125,86),(c,125,90),(c,125,94),(c,125,98), (c,125,125),(c,125,129),(c,125,133),(c,125,137),(c,126,23),(c,126,27), (c,126,31),(c,126,35),(c,126,39),(c,126,43),(c,126,47),(c,126,51), (c,126,55),(c,126,59),(c,126,102),(c,126,106),(c,126,110),(c,126,114), (c,126,118),(c,126,122),(c,126,126),(c,126,130),(c,126,134),(c,126,138), (c,127,63),(c,127,67),(c,127,71),(c,127,75),(c,127,79),(c,127,83), (c,127,87),(c,127,91),(c,127,95),(c,127,99),(c,127,103),(c,127,107), (c,127,111),(c,127,115),(c,127,119),(c,127,123),(c,127,127),(c,127,131), (c,127,135),(c,127,139),(c,128,1),(c,128,5),(c,128,9),(c,128,16), (c,128,21),(c,128,25),(c,128,32),(c,128,37),(c,128,44),(c,128,52), (c,128,61),(c,128,65),(c,128,72),(c,128,77),(c,128,84),(c,128,92), (c,128,101),(c,128,108),(c,128,116),(c,128,128),(c,129,7),(c,129,11), (c,129,15),(c,129,19),(c,129,38),(c,129,42),(c,129,46),(c,129,50), (c,129,54),(c,129,58),(c,129,78),(c,129,82),(c,129,86),(c,129,90), (c,129,94),(c,129,98),(c,129,125),(c,129,129),(c,129,133),(c,129,137), (c,130,23),(c,130,27),(c,130,31),(c,130,35),(c,130,39),(c,130,43), (c,130,47),(c,130,51),(c,130,55),(c,130,59),(c,130,102),(c,130,106), (c,130,110),(c,130,114),(c,130,118),(c,130,122),(c,130,126),(c,130,130), (c,130,134),(c,130,138),(c,131,63),(c,131,67),(c,131,71),(c,131,75), (c,131,79),(c,131,83),(c,131,87),(c,131,91),(c,131,95),(c,131,99), (c,131,103),(c,131,107),(c,131,111),(c,131,115),(c,131,119),(c,131,123), (c,131,127),(c,131,131),(c,131,135),(c,131,139),(c,132,2),(c,132,6), (c,132,13),(c,132,17),(c,132,22),(c,132,29),(c,132,33),(c,132,41), (c,132,45),(c,132,56),(c,132,62),(c,132,69),(c,132,73),(c,132,81), (c,132,85),(c,132,96),(c,132,105),(c,132,109),(c,132,120),(c,132,132), (c,133,7),(c,133,11),(c,133,15),(c,133,19),(c,133,38),(c,133,42), (c,133,46),(c,133,50),(c,133,54),(c,133,58),(c,133,78),(c,133,82), (c,133,86),(c,133,90),(c,133,94),(c,133,98),(c,133,125),(c,133,129), (c,133,133),(c,133,137),(c,134,23),(c,134,27),(c,134,31),(c,134,35), (c,134,39),(c,134,43),(c,134,47),(c,134,51),(c,134,55),(c,134,59), (c,134,102),(c,134,106),(c,134,110),(c,134,114),(c,134,118),(c,134,122), (c,134,126),(c,134,130),(c,134,134),(c,134,138),(c,135,63),(c,135,67), (c,135,71),(c,135,75),(c,135,79),(c,135,83),(c,135,87),(c,135,91), (c,135,95),(c,135,99),(c,135,103),(c,135,107),(c,135,111),(c,135,115), (c,135,119),(c,135,123),(c,135,127),(c,135,131),(c,135,135),(c,135,139), (c,136,3),(c,136,10),(c,136,14),(c,136,18),(c,136,26),(c,136,30), (c,136,34),(c,136,49),(c,136,53),(c,136,57),(c,136,66),(c,136,70), (c,136,74),(c,136,89),(c,136,93),(c,136,97),(c,136,113),(c,136,117), (c,136,121),(c,136,136),(c,137,7),(c,137,11),(c,137,15),(c,137,19), (c,137,38),(c,137,42),(c,137,46),(c,137,50),(c,137,54),(c,137,58), (c,137,78),(c,137,82),(c,137,86),(c,137,90),(c,137,94),(c,137,98), (c,137,125),(c,137,129),(c,137,133),(c,137,137),(c,138,23),(c,138,27), (c,138,31),(c,138,35),(c,138,39),(c,138,43),(c,138,47),(c,138,51), (c,138,55),(c,138,59),(c,138,102),(c,138,106),(c,138,110),(c,138,114), (c,138,118),(c,138,122),(c,138,126),(c,138,130),(c,138,134),(c,138,138), (c,139,63),(c,139,67),(c,139,71),(c,139,75),(c,139,79),(c,139,83), (c,139,87),(c,139,91),(c,139,95),(c,139,99),(c,139,103),(c,139,107), (c,139,111),(c,139,115),(c,139,119),(c,139,123),(c,139,127),(c,139,131), (c,139,135),(c,139,139)] p4, p5, p6, q4, q5, q6, r4, r5, r6:: Form p4 = Prop (P 4); p5 = Prop (P 5); p6 = Prop (P 6) q4 = Prop (Q 4); q5 = Prop (Q 5); q6 = Prop (Q 6) r4 = Prop (R 4); r5 = Prop (R 5); r6 = Prop (R 6)