2 module type Dodec_ineq_names =
5 val dodec_ineqs : (string * term) list
9 module Dodec_ineq_names : Dodec_ineq_names =
14 "D_232427898",D_232427898;
15 "D_501745932",D_501745932;
16 "D_454413312",D_454413312;
17 "D_484548925",D_484548925;
18 "D_140432082",D_140432082;
19 "D_211431164",D_211431164;
20 "D_120383233",D_120383233;
21 "D_950195574",D_950195574;
22 "D_411439162",D_411439162;
23 "D_930476095",D_930476095;
24 "D_504216105",D_504216105;
25 "D_303447655",D_303447655;
26 "D_999530305",D_999530305;
27 "D_774222998",D_774222998;
28 "D_583790155",D_583790155;
29 "D_954638763",D_954638763;
30 "D_836501282",D_836501282;
31 "D_815857122",D_815857122;
32 "D_143442051",D_143442051;
33 "D_616037833",D_616037833;
34 "D_943639543",D_943639543;
35 "D_348573741",D_348573741;
36 "D_887895540",D_887895540;
37 "D_292050936",D_292050936;
38 "D_747114280",D_747114280;
39 "D_407035272",D_407035272;
40 "D_746762527",D_746762527;
41 "D_908135697",D_908135697;
42 "D_852700722",D_852700722;
43 "D_187794654",D_187794654;
44 "D_241250402",D_241250402;
45 "D_614375500",D_614375500;
46 "D_392850749",D_392850749;
47 "D_324682944",D_324682944;
48 "D_102919537",D_102919537;
49 "D_756454529",D_756454529;
50 "D_563250599",D_563250599;
51 "D_439521695",D_439521695;
52 "D_805633512",D_805633512;
53 "D_892141600",D_892141600;
54 "D_224306197",D_224306197;
55 "D_120210454",D_120210454;
56 "D_479875130",D_479875130;
57 "D_629548058",D_629548058;
58 "D_469668150",D_469668150;
59 "D_218128189",D_218128189;
60 "D_169113912",D_169113912;
61 "D_143105921",D_143105921;
62 "D_421739939",D_421739939;
63 "D_595203705",D_595203705;
64 "D_943490566",D_943490566;
65 "D_797136399",D_797136399;
66 "D_603733089",D_603733089;
67 "D_459264712",D_459264712;
68 "D_557495949",D_557495949;
69 "D_171329882",D_171329882;
70 "D_720788076",D_720788076;
71 "D_554235027",D_554235027;
72 "D_569393441",D_569393441;
73 "D_992963254",D_992963254;
74 "D_157321192",D_157321192;
75 "D_954705068",D_954705068;
76 "D_607292193",D_607292193;
77 "D_852636576",D_852636576;
78 "D_981457443",D_981457443;
79 "D_400655725",D_400655725;
80 "D_552790530",D_552790530;
81 "D_339650543",D_339650543;
82 "D_195763418",D_195763418;
83 "D_346647038",D_346647038;
84 "D_542422328",D_542422328;
85 "D_958501031",D_958501031;
86 "D_977882706",D_977882706;
87 "D_817699709",D_817699709;
88 "D_221335081",D_221335081;
89 "D_380511524",D_380511524;
90 "D_534704091",D_534704091;
91 "D_510654661",D_510654661;
92 "D_296038926",D_296038926;
93 "D_725284239",D_725284239;
94 "D_508592316",D_508592316;
95 "D_780228595",D_780228595;
96 "D_129176394",D_129176394;
97 "D_794503453",D_794503453;
98 "D_820371697",D_820371697;
99 "D_993947481",D_993947481;
100 "D_888634003",D_888634003;
101 "D_985594975",D_985594975;
102 "D_278856582",D_278856582;
103 "D_309781213",D_309781213;
104 "D_546070702",D_546070702;
105 "D_273299220",D_273299220;
106 "D_420356876",D_420356876;
107 "D_168730298",D_168730298;
108 "D_563211815",D_563211815;
109 "D_923665644",D_923665644;
110 "D_131907821",D_131907821;
111 "D_632783039",D_632783039;
112 "D_997560269",D_997560269;
113 "D_849090707",D_849090707;
114 "D_741613981",D_741613981;