% Simple illustration of the technique of generalised
%       closed-world specialisation within Aleph
/** <examples>
?- rdhyp,sphyp,show(gcws),addgcws.
% input
% |: normal(A).
*/

:-use_module(library(aleph)).
:- if(current_predicate(use_rendering/1)).
:- use_rendering(prolog).
:- endif.
:-aleph.

:- mode(*,normal(+year)).
:- mode(*,div4(+year)).
:- mode(*,div100(+year)).
:- mode(*,div400(+year)).

:- determination(normal/1,div4/1).
:- determination(normal/1,div100/1).
:- determination(normal/1,div400/1).
:- determination(normal/1,year/1).

:- begin_bg.
div4(4).
div4(8).
div4(12).
div4(16).
div4(20).
div4(24).
div4(28).
div4(32).
div4(36).
div4(40).
div4(44).
div4(48).
div4(52).
div4(56).
div4(60).
div4(64).
div4(68).
div4(72).
div4(76).
div4(80).
div4(84).
div4(88).
div4(92).
div4(96).
div4(100).
div4(104).
div4(108).
div4(112).
div4(116).
div4(120).
div4(124).
div4(128).
div4(132).
div4(136).
div4(140).
div4(144).
div4(148).
div4(152).
div4(156).
div4(160).
div4(164).
div4(168).
div4(172).
div4(176).
div4(180).
div4(184).
div4(188).
div4(192).
div4(196).
div4(200).
div4(204).
div4(208).
div4(212).
div4(216).
div4(220).
div4(224).
div4(228).
div4(232).
div4(236).
div4(240).
div4(244).
div4(248).
div4(252).
div4(256).
div4(260).
div4(264).
div4(268).
div4(272).
div4(276).
div4(280).
div4(284).
div4(288).
div4(292).
div4(296).
div4(300).
div4(304).
div4(308).
div4(312).
div4(316).
div4(320).
div4(324).
div4(328).
div4(332).
div4(336).
div4(340).
div4(344).
div4(348).
div4(352).
div4(356).
div4(360).
div4(364).
div4(368).
div4(372).
div4(376).
div4(380).
div4(384).
div4(388).
div4(392).
div4(396).
div4(400).
div4(404).
div4(408).
div4(412).
div4(416).
div4(420).
div4(424).
div4(428).
div4(432).
div4(436).
div4(440).
div4(444).
div4(448).
div4(452).
div4(456).
div4(460).
div4(464).
div4(468).
div4(472).
div4(476).
div4(480).
div4(484).
div4(488).
div4(492).
div4(496).
div4(500).
div4(504).
div4(508).
div4(512).
div4(516).
div4(520).
div4(524).
div4(528).
div4(532).
div4(536).
div4(540).
div4(544).
div4(548).
div4(552).
div4(556).
div4(560).
div4(564).
div4(568).
div4(572).
div4(576).
div4(580).
div4(584).
div4(588).
div4(592).
div4(596).
div4(600).
div4(604).
div4(608).
div4(612).
div4(616).
div4(620).
div4(624).
div4(628).
div4(632).
div4(636).
div4(640).
div4(644).
div4(648).
div4(652).
div4(656).
div4(660).
div4(664).
div4(668).
div4(672).
div4(676).
div4(680).
div4(684).
div4(688).
div4(692).
div4(696).
div4(700).
div4(704).
div4(708).
div4(712).
div4(716).
div4(720).
div4(724).
div4(728).
div4(732).
div4(736).
div4(740).
div4(744).
div4(748).
div4(752).
div4(756).
div4(760).
div4(764).
div4(768).
div4(772).
div4(776).
div4(780).
div4(784).
div4(788).
div4(792).
div4(796).
div4(800).
div4(804).
div4(808).
div4(812).
div4(816).
div4(820).
div4(824).
div4(828).
div4(832).
div4(836).
div4(840).
div4(844).
div4(848).
div4(852).
div4(856).
div4(860).
div4(864).
div4(868).
div4(872).
div4(876).
div4(880).
div4(884).
div4(888).
div4(892).
div4(896).
div4(900).
div4(904).
div4(908).
div4(912).
div4(916).
div4(920).
div4(924).
div4(928).
div4(932).
div4(936).
div4(940).
div4(944).
div4(948).
div4(952).
div4(956).
div4(960).
div4(964).
div4(968).
div4(972).
div4(976).
div4(980).
div4(984).
div4(988).
div4(992).
div4(996).
div4(1000).
div4(1004).
div4(1008).
div4(1012).
div4(1016).
div4(1020).
div4(1024).
div4(1028).
div4(1032).
div4(1036).
div4(1040).
div4(1044).
div4(1048).
div4(1052).
div4(1056).
div4(1060).
div4(1064).
div4(1068).
div4(1072).
div4(1076).
div4(1080).
div4(1084).
div4(1088).
div4(1092).
div4(1096).
div4(1100).
div4(1104).
div4(1108).
div4(1112).
div4(1116).
div4(1120).
div4(1124).
div4(1128).
div4(1132).
div4(1136).
div4(1140).
div4(1144).
div4(1148).
div4(1152).
div4(1156).
div4(1160).
div4(1164).
div4(1168).
div4(1172).
div4(1176).
div4(1180).
div4(1184).
div4(1188).
div4(1192).
div4(1196).
div4(1200).
div4(1204).
div4(1208).
div4(1212).
div4(1216).
div4(1220).
div4(1224).
div4(1228).
div4(1232).
div4(1236).
div4(1240).
div4(1244).
div4(1248).
div4(1252).
div4(1256).
div4(1260).
div4(1264).
div4(1268).
div4(1272).
div4(1276).
div4(1280).
div4(1284).
div4(1288).
div4(1292).
div4(1296).
div4(1300).
div4(1304).
div4(1308).
div4(1312).
div4(1316).
div4(1320).
div4(1324).
div4(1328).
div4(1332).
div4(1336).
div4(1340).
div4(1344).
div4(1348).
div4(1352).
div4(1356).
div4(1360).
div4(1364).
div4(1368).
div4(1372).
div4(1376).
div4(1380).
div4(1384).
div4(1388).
div4(1392).
div4(1396).
div4(1400).
div4(1404).
div4(1408).
div4(1412).
div4(1416).
div4(1420).
div4(1424).
div4(1428).
div4(1432).
div4(1436).
div4(1440).
div4(1444).
div4(1448).
div4(1452).
div4(1456).
div4(1460).
div4(1464).
div4(1468).
div4(1472).
div4(1476).
div4(1480).
div4(1484).
div4(1488).
div4(1492).
div4(1496).
div4(1500).
div4(1504).
div4(1508).
div4(1512).
div4(1516).
div4(1520).
div4(1524).
div4(1528).
div4(1532).
div4(1536).
div4(1540).
div4(1544).
div4(1548).
div4(1552).
div4(1556).
div4(1560).
div4(1564).
div4(1568).
div4(1572).
div4(1576).
div4(1580).
div4(1584).
div4(1588).
div4(1592).
div4(1596).
div4(1600).

div100(100).
div100(200).
div100(300).
div100(400).
div100(500).
div100(600).
div100(700).
div100(800).
div100(900).
div100(1000).
div100(1100).
div100(1200).
div100(1300).
div100(1400).
div100(1500).
div100(1600).

div400(400).
div400(800).
div400(1200).
div400(1600).

year(1).
year(2).
year(3).
year(4).
year(5).
year(6).
year(7).
year(8).
year(9).
year(10).
year(11).
year(12).
year(13).
year(14).
year(15).
year(16).
year(17).
year(18).
year(19).
year(20).
year(21).
year(22).
year(23).
year(24).
year(25).
year(26).
year(27).
year(28).
year(29).
year(30).
year(31).
year(32).
year(33).
year(34).
year(35).
year(36).
year(37).
year(38).
year(39).
year(40).
year(41).
year(42).
year(43).
year(44).
year(45).
year(46).
year(47).
year(48).
year(49).
year(50).
year(51).
year(52).
year(53).
year(54).
year(55).
year(56).
year(57).
year(58).
year(59).
year(60).
year(61).
year(62).
year(63).
year(64).
year(65).
year(66).
year(67).
year(68).
year(69).
year(70).
year(71).
year(72).
year(73).
year(74).
year(75).
year(76).
year(77).
year(78).
year(79).
year(80).
year(81).
year(82).
year(83).
year(84).
year(85).
year(86).
year(87).
year(88).
year(89).
year(90).
year(91).
year(92).
year(93).
year(94).
year(95).
year(96).
year(97).
year(98).
year(99).
year(100).
year(101).
year(102).
year(103).
year(104).
year(105).
year(106).
year(107).
year(108).
year(109).
year(110).
year(111).
year(112).
year(113).
year(114).
year(115).
year(116).
year(117).
year(118).
year(119).
year(120).
year(121).
year(122).
year(123).
year(124).
year(125).
year(126).
year(127).
year(128).
year(129).
year(130).
year(131).
year(132).
year(133).
year(134).
year(135).
year(136).
year(137).
year(138).
year(139).
year(140).
year(141).
year(142).
year(143).
year(144).
year(145).
year(146).
year(147).
year(148).
year(149).
year(150).
year(151).
year(152).
year(153).
year(154).
year(155).
year(156).
year(157).
year(158).
year(159).
year(160).
year(161).
year(162).
year(163).
year(164).
year(165).
year(166).
year(167).
year(168).
year(169).
year(170).
year(171).
year(172).
year(173).
year(174).
year(175).
year(176).
year(177).
year(178).
year(179).
year(180).
year(181).
year(182).
year(183).
year(184).
year(185).
year(186).
year(187).
year(188).
year(189).
year(190).
year(191).
year(192).
year(193).
year(194).
year(195).
year(196).
year(197).
year(198).
year(199).
year(200).
year(201).
year(202).
year(203).
year(204).
year(205).
year(206).
year(207).
year(208).
year(209).
year(210).
year(211).
year(212).
year(213).
year(214).
year(215).
year(216).
year(217).
year(218).
year(219).
year(220).
year(221).
year(222).
year(223).
year(224).
year(225).
year(226).
year(227).
year(228).
year(229).
year(230).
year(231).
year(232).
year(233).
year(234).
year(235).
year(236).
year(237).
year(238).
year(239).
year(240).
year(241).
year(242).
year(243).
year(244).
year(245).
year(246).
year(247).
year(248).
year(249).
year(250).
year(251).
year(252).
year(253).
year(254).
year(255).
year(256).
year(257).
year(258).
year(259).
year(260).
year(261).
year(262).
year(263).
year(264).
year(265).
year(266).
year(267).
year(268).
year(269).
year(270).
year(271).
year(272).
year(273).
year(274).
year(275).
year(276).
year(277).
year(278).
year(279).
year(280).
year(281).
year(282).
year(283).
year(284).
year(285).
year(286).
year(287).
year(288).
year(289).
year(290).
year(291).
year(292).
year(293).
year(294).
year(295).
year(296).
year(297).
year(298).
year(299).
year(300).
year(301).
year(302).
year(303).
year(304).
year(305).
year(306).
year(307).
year(308).
year(309).
year(310).
year(311).
year(312).
year(313).
year(314).
year(315).
year(316).
year(317).
year(318).
year(319).
year(320).
year(321).
year(322).
year(323).
year(324).
year(325).
year(326).
year(327).
year(328).
year(329).
year(330).
year(331).
year(332).
year(333).
year(334).
year(335).
year(336).
year(337).
year(338).
year(339).
year(340).
year(341).
year(342).
year(343).
year(344).
year(345).
year(346).
year(347).
year(348).
year(349).
year(350).
year(351).
year(352).
year(353).
year(354).
year(355).
year(356).
year(357).
year(358).
year(359).
year(360).
year(361).
year(362).
year(363).
year(364).
year(365).
year(366).
year(367).
year(368).
year(369).
year(370).
year(371).
year(372).
year(373).
year(374).
year(375).
year(376).
year(377).
year(378).
year(379).
year(380).
year(381).
year(382).
year(383).
year(384).
year(385).
year(386).
year(387).
year(388).
year(389).
year(390).
year(391).
year(392).
year(393).
year(394).
year(395).
year(396).
year(397).
year(398).
year(399).
year(400).
year(401).
year(402).
year(403).
year(404).
year(405).
year(406).
year(407).
year(408).
year(409).
year(410).
year(411).
year(412).
year(413).
year(414).
year(415).
year(416).
year(417).
year(418).
year(419).
year(420).
year(421).
year(422).
year(423).
year(424).
year(425).
year(426).
year(427).
year(428).
year(429).
year(430).
year(431).
year(432).
year(433).
year(434).
year(435).
year(436).
year(437).
year(438).
year(439).
year(440).
year(441).
year(442).
year(443).
year(444).
year(445).
year(446).
year(447).
year(448).
year(449).
year(450).
year(451).
year(452).
year(453).
year(454).
year(455).
year(456).
year(457).
year(458).
year(459).
year(460).
year(461).
year(462).
year(463).
year(464).
year(465).
year(466).
year(467).
year(468).
year(469).
year(470).
year(471).
year(472).
year(473).
year(474).
year(475).
year(476).
year(477).
year(478).
year(479).
year(480).
year(481).
year(482).
year(483).
year(484).
year(485).
year(486).
year(487).
year(488).
year(489).
year(490).
year(491).
year(492).
year(493).
year(494).
year(495).
year(496).
year(497).
year(498).
year(499).
year(500).
year(501).
year(502).
year(503).
year(504).
year(505).
year(506).
year(507).
year(508).
year(509).
year(510).
year(511).
year(512).
year(513).
year(514).
year(515).
year(516).
year(517).
year(518).
year(519).
year(520).
year(521).
year(522).
year(523).
year(524).
year(525).
year(526).
year(527).
year(528).
year(529).
year(530).
year(531).
year(532).
year(533).
year(534).
year(535).
year(536).
year(537).
year(538).
year(539).
year(540).
year(541).
year(542).
year(543).
year(544).
year(545).
year(546).
year(547).
year(548).
year(549).
year(550).
year(551).
year(552).
year(553).
year(554).
year(555).
year(556).
year(557).
year(558).
year(559).
year(560).
year(561).
year(562).
year(563).
year(564).
year(565).
year(566).
year(567).
year(568).
year(569).
year(570).
year(571).
year(572).
year(573).
year(574).
year(575).
year(576).
year(577).
year(578).
year(579).
year(580).
year(581).
year(582).
year(583).
year(584).
year(585).
year(586).
year(587).
year(588).
year(589).
year(590).
year(591).
year(592).
year(593).
year(594).
year(595).
year(596).
year(597).
year(598).
year(599).
year(600).
year(601).
year(602).
year(603).
year(604).
year(605).
year(606).
year(607).
year(608).
year(609).
year(610).
year(611).
year(612).
year(613).
year(614).
year(615).
year(616).
year(617).
year(618).
year(619).
year(620).
year(621).
year(622).
year(623).
year(624).
year(625).
year(626).
year(627).
year(628).
year(629).
year(630).
year(631).
year(632).
year(633).
year(634).
year(635).
year(636).
year(637).
year(638).
year(639).
year(640).
year(641).
year(642).
year(643).
year(644).
year(645).
year(646).
year(647).
year(648).
year(649).
year(650).
year(651).
year(652).
year(653).
year(654).
year(655).
year(656).
year(657).
year(658).
year(659).
year(660).
year(661).
year(662).
year(663).
year(664).
year(665).
year(666).
year(667).
year(668).
year(669).
year(670).
year(671).
year(672).
year(673).
year(674).
year(675).
year(676).
year(677).
year(678).
year(679).
year(680).
year(681).
year(682).
year(683).
year(684).
year(685).
year(686).
year(687).
year(688).
year(689).
year(690).
year(691).
year(692).
year(693).
year(694).
year(695).
year(696).
year(697).
year(698).
year(699).
year(700).
year(701).
year(702).
year(703).
year(704).
year(705).
year(706).
year(707).
year(708).
year(709).
year(710).
year(711).
year(712).
year(713).
year(714).
year(715).
year(716).
year(717).
year(718).
year(719).
year(720).
year(721).
year(722).
year(723).
year(724).
year(725).
year(726).
year(727).
year(728).
year(729).
year(730).
year(731).
year(732).
year(733).
year(734).
year(735).
year(736).
year(737).
year(738).
year(739).
year(740).
year(741).
year(742).
year(743).
year(744).
year(745).
year(746).
year(747).
year(748).
year(749).
year(750).
year(751).
year(752).
year(753).
year(754).
year(755).
year(756).
year(757).
year(758).
year(759).
year(760).
year(761).
year(762).
year(763).
year(764).
year(765).
year(766).
year(767).
year(768).
year(769).
year(770).
year(771).
year(772).
year(773).
year(774).
year(775).
year(776).
year(777).
year(778).
year(779).
year(780).
year(781).
year(782).
year(783).
year(784).
year(785).
year(786).
year(787).
year(788).
year(789).
year(790).
year(791).
year(792).
year(793).
year(794).
year(795).
year(796).
year(797).
year(798).
year(799).
year(800).
year(801).
year(802).
year(803).
year(804).
year(805).
year(806).
year(807).
year(808).
year(809).
year(810).
year(811).
year(812).
year(813).
year(814).
year(815).
year(816).
year(817).
year(818).
year(819).
year(820).
year(821).
year(822).
year(823).
year(824).
year(825).
year(826).
year(827).
year(828).
year(829).
year(830).
year(831).
year(832).
year(833).
year(834).
year(835).
year(836).
year(837).
year(838).
year(839).
year(840).
year(841).
year(842).
year(843).
year(844).
year(845).
year(846).
year(847).
year(848).
year(849).
year(850).
year(851).
year(852).
year(853).
year(854).
year(855).
year(856).
year(857).
year(858).
year(859).
year(860).
year(861).
year(862).
year(863).
year(864).
year(865).
year(866).
year(867).
year(868).
year(869).
year(870).
year(871).
year(872).
year(873).
year(874).
year(875).
year(876).
year(877).
year(878).
year(879).
year(880).
year(881).
year(882).
year(883).
year(884).
year(885).
year(886).
year(887).
year(888).
year(889).
year(890).
year(891).
year(892).
year(893).
year(894).
year(895).
year(896).
year(897).
year(898).
year(899).
year(900).
year(901).
year(902).
year(903).
year(904).
year(905).
year(906).
year(907).
year(908).
year(909).
year(910).
year(911).
year(912).
year(913).
year(914).
year(915).
year(916).
year(917).
year(918).
year(919).
year(920).
year(921).
year(922).
year(923).
year(924).
year(925).
year(926).
year(927).
year(928).
year(929).
year(930).
year(931).
year(932).
year(933).
year(934).
year(935).
year(936).
year(937).
year(938).
year(939).
year(940).
year(941).
year(942).
year(943).
year(944).
year(945).
year(946).
year(947).
year(948).
year(949).
year(950).
year(951).
year(952).
year(953).
year(954).
year(955).
year(956).
year(957).
year(958).
year(959).
year(960).
year(961).
year(962).
year(963).
year(964).
year(965).
year(966).
year(967).
year(968).
year(969).
year(970).
year(971).
year(972).
year(973).
year(974).
year(975).
year(976).
year(977).
year(978).
year(979).
year(980).
year(981).
year(982).
year(983).
year(984).
year(985).
year(986).
year(987).
year(988).
year(989).
year(990).
year(991).
year(992).
year(993).
year(994).
year(995).
year(996).
year(997).
year(998).
year(999).
year(1000).
year(1001).
year(1002).
year(1003).
year(1004).
year(1005).
year(1006).
year(1007).
year(1008).
year(1009).
year(1010).
year(1011).
year(1012).
year(1013).
year(1014).
year(1015).
year(1016).
year(1017).
year(1018).
year(1019).
year(1020).
year(1021).
year(1022).
year(1023).
year(1024).
year(1025).
year(1026).
year(1027).
year(1028).
year(1029).
year(1030).
year(1031).
year(1032).
year(1033).
year(1034).
year(1035).
year(1036).
year(1037).
year(1038).
year(1039).
year(1040).
year(1041).
year(1042).
year(1043).
year(1044).
year(1045).
year(1046).
year(1047).
year(1048).
year(1049).
year(1050).
year(1051).
year(1052).
year(1053).
year(1054).
year(1055).
year(1056).
year(1057).
year(1058).
year(1059).
year(1060).
year(1061).
year(1062).
year(1063).
year(1064).
year(1065).
year(1066).
year(1067).
year(1068).
year(1069).
year(1070).
year(1071).
year(1072).
year(1073).
year(1074).
year(1075).
year(1076).
year(1077).
year(1078).
year(1079).
year(1080).
year(1081).
year(1082).
year(1083).
year(1084).
year(1085).
year(1086).
year(1087).
year(1088).
year(1089).
year(1090).
year(1091).
year(1092).
year(1093).
year(1094).
year(1095).
year(1096).
year(1097).
year(1098).
year(1099).
year(1100).
year(1101).
year(1102).
year(1103).
year(1104).
year(1105).
year(1106).
year(1107).
year(1108).
year(1109).
year(1110).
year(1111).
year(1112).
year(1113).
year(1114).
year(1115).
year(1116).
year(1117).
year(1118).
year(1119).
year(1120).
year(1121).
year(1122).
year(1123).
year(1124).
year(1125).
year(1126).
year(1127).
year(1128).
year(1129).
year(1130).
year(1131).
year(1132).
year(1133).
year(1134).
year(1135).
year(1136).
year(1137).
year(1138).
year(1139).
year(1140).
year(1141).
year(1142).
year(1143).
year(1144).
year(1145).
year(1146).
year(1147).
year(1148).
year(1149).
year(1150).
year(1151).
year(1152).
year(1153).
year(1154).
year(1155).
year(1156).
year(1157).
year(1158).
year(1159).
year(1160).
year(1161).
year(1162).
year(1163).
year(1164).
year(1165).
year(1166).
year(1167).
year(1168).
year(1169).
year(1170).
year(1171).
year(1172).
year(1173).
year(1174).
year(1175).
year(1176).
year(1177).
year(1178).
year(1179).
year(1180).
year(1181).
year(1182).
year(1183).
year(1184).
year(1185).
year(1186).
year(1187).
year(1188).
year(1189).
year(1190).
year(1191).
year(1192).
year(1193).
year(1194).
year(1195).
year(1196).
year(1197).
year(1198).
year(1199).
year(1200).
year(1201).
year(1202).
year(1203).
year(1204).
year(1205).
year(1206).
year(1207).
year(1208).
year(1209).
year(1210).
year(1211).
year(1212).
year(1213).
year(1214).
year(1215).
year(1216).
year(1217).
year(1218).
year(1219).
year(1220).
year(1221).
year(1222).
year(1223).
year(1224).
year(1225).
year(1226).
year(1227).
year(1228).
year(1229).
year(1230).
year(1231).
year(1232).
year(1233).
year(1234).
year(1235).
year(1236).
year(1237).
year(1238).
year(1239).
year(1240).
year(1241).
year(1242).
year(1243).
year(1244).
year(1245).
year(1246).
year(1247).
year(1248).
year(1249).
year(1250).
year(1251).
year(1252).
year(1253).
year(1254).
year(1255).
year(1256).
year(1257).
year(1258).
year(1259).
year(1260).
year(1261).
year(1262).
year(1263).
year(1264).
year(1265).
year(1266).
year(1267).
year(1268).
year(1269).
year(1270).
year(1271).
year(1272).
year(1273).
year(1274).
year(1275).
year(1276).
year(1277).
year(1278).
year(1279).
year(1280).
year(1281).
year(1282).
year(1283).
year(1284).
year(1285).
year(1286).
year(1287).
year(1288).
year(1289).
year(1290).
year(1291).
year(1292).
year(1293).
year(1294).
year(1295).
year(1296).
year(1297).
year(1298).
year(1299).
year(1300).
year(1301).
year(1302).
year(1303).
year(1304).
year(1305).
year(1306).
year(1307).
year(1308).
year(1309).
year(1310).
year(1311).
year(1312).
year(1313).
year(1314).
year(1315).
year(1316).
year(1317).
year(1318).
year(1319).
year(1320).
year(1321).
year(1322).
year(1323).
year(1324).
year(1325).
year(1326).
year(1327).
year(1328).
year(1329).
year(1330).
year(1331).
year(1332).
year(1333).
year(1334).
year(1335).
year(1336).
year(1337).
year(1338).
year(1339).
year(1340).
year(1341).
year(1342).
year(1343).
year(1344).
year(1345).
year(1346).
year(1347).
year(1348).
year(1349).
year(1350).
year(1351).
year(1352).
year(1353).
year(1354).
year(1355).
year(1356).
year(1357).
year(1358).
year(1359).
year(1360).
year(1361).
year(1362).
year(1363).
year(1364).
year(1365).
year(1366).
year(1367).
year(1368).
year(1369).
year(1370).
year(1371).
year(1372).
year(1373).
year(1374).
year(1375).
year(1376).
year(1377).
year(1378).
year(1379).
year(1380).
year(1381).
year(1382).
year(1383).
year(1384).
year(1385).
year(1386).
year(1387).
year(1388).
year(1389).
year(1390).
year(1391).
year(1392).
year(1393).
year(1394).
year(1395).
year(1396).
year(1397).
year(1398).
year(1399).
year(1400).
year(1401).
year(1402).
year(1403).
year(1404).
year(1405).
year(1406).
year(1407).
year(1408).
year(1409).
year(1410).
year(1411).
year(1412).
year(1413).
year(1414).
year(1415).
year(1416).
year(1417).
year(1418).
year(1419).
year(1420).
year(1421).
year(1422).
year(1423).
year(1424).
year(1425).
year(1426).
year(1427).
year(1428).
year(1429).
year(1430).
year(1431).
year(1432).
year(1433).
year(1434).
year(1435).
year(1436).
year(1437).
year(1438).
year(1439).
year(1440).
year(1441).
year(1442).
year(1443).
year(1444).
year(1445).
year(1446).
year(1447).
year(1448).
year(1449).
year(1450).
year(1451).
year(1452).
year(1453).
year(1454).
year(1455).
year(1456).
year(1457).
year(1458).
year(1459).
year(1460).
year(1461).
year(1462).
year(1463).
year(1464).
year(1465).
year(1466).
year(1467).
year(1468).
year(1469).
year(1470).
year(1471).
year(1472).
year(1473).
year(1474).
year(1475).
year(1476).
year(1477).
year(1478).
year(1479).
year(1480).
year(1481).
year(1482).
year(1483).
year(1484).
year(1485).
year(1486).
year(1487).
year(1488).
year(1489).
year(1490).
year(1491).
year(1492).
year(1493).
year(1494).
year(1495).
year(1496).
year(1497).
year(1498).
year(1499).
year(1500).
year(1501).
year(1502).
year(1503).
year(1504).
year(1505).
year(1506).
year(1507).
year(1508).
year(1509).
year(1510).
year(1511).
year(1512).
year(1513).
year(1514).
year(1515).
year(1516).
year(1517).
year(1518).
year(1519).
year(1520).
year(1521).
year(1522).
year(1523).
year(1524).
year(1525).
year(1526).
year(1527).
year(1528).
year(1529).
year(1530).
year(1531).
year(1532).
year(1533).
year(1534).
year(1535).
year(1536).
year(1537).
year(1538).
year(1539).
year(1540).
year(1541).
year(1542).
year(1543).
year(1544).
year(1545).
year(1546).
year(1547).
year(1548).
year(1549).
year(1550).
year(1551).
year(1552).
year(1553).
year(1554).
year(1555).
year(1556).
year(1557).
year(1558).
year(1559).
year(1560).
year(1561).
year(1562).
year(1563).
year(1564).
year(1565).
year(1566).
year(1567).
year(1568).
year(1569).
year(1570).
year(1571).
year(1572).
year(1573).
year(1574).
year(1575).
year(1576).
year(1577).
year(1578).
year(1579).
year(1580).
year(1581).

% more examples

year(1582).
year(1583).
year(1584).
year(1585).
year(1586).
year(1587).
year(1588).
year(1589).
year(1590).
year(1591).
year(1592).
year(1593).
year(1594).
year(1595).
year(1596).
year(1597).
year(1598).
year(1599).
year(1600).
:-end_bg.
:-begin_in_pos.
normal(1).
normal(2).
normal(3).
normal(5).
normal(6).
normal(7).
normal(9).
normal(10).
normal(11).
normal(13).
normal(14).
normal(15).
normal(17).
normal(18).
normal(19).
normal(21).
normal(22).
normal(23).
normal(25).
normal(26).
normal(27).
normal(29).
normal(30).
normal(31).
normal(33).
normal(34).
normal(35).
normal(37).
normal(38).
normal(39).
normal(41).
normal(42).
normal(43).
normal(45).
normal(46).
normal(47).
normal(49).
normal(50).
normal(51).
normal(53).
normal(54).
normal(55).
normal(57).
normal(58).
normal(59).
normal(61).
normal(62).
normal(63).
normal(65).
normal(66).
normal(67).
normal(69).
normal(70).
normal(71).
normal(73).
normal(74).
normal(75).
normal(77).
normal(78).
normal(79).
normal(81).
normal(82).
normal(83).
normal(85).
normal(86).
normal(87).
normal(89).
normal(90).
normal(91).
normal(93).
normal(94).
normal(95).
normal(97).
normal(98).
normal(99).
normal(100).
normal(101).
normal(102).
normal(103).
normal(105).
normal(106).
normal(107).
normal(109).
normal(110).
normal(111).
normal(113).
normal(114).
normal(115).
normal(117).
normal(118).
normal(119).
normal(121).
normal(122).
normal(123).
normal(125).
normal(126).
normal(127).
normal(129).
normal(130).
normal(131).
normal(133).
normal(134).
normal(135).
normal(137).
normal(138).
normal(139).
normal(141).
normal(142).
normal(143).
normal(145).
normal(146).
normal(147).
normal(149).
normal(150).
normal(151).
normal(153).
normal(154).
normal(155).
normal(157).
normal(158).
normal(159).
normal(161).
normal(162).
normal(163).
normal(165).
normal(166).
normal(167).
normal(169).
normal(170).
normal(171).
normal(173).
normal(174).
normal(175).
normal(177).
normal(178).
normal(179).
normal(181).
normal(182).
normal(183).
normal(185).
normal(186).
normal(187).
normal(189).
normal(190).
normal(191).
normal(193).
normal(194).
normal(195).
normal(197).
normal(198).
normal(199).
normal(200).
normal(201).
normal(202).
normal(203).
normal(205).
normal(206).
normal(207).
normal(209).
normal(210).
normal(211).
normal(213).
normal(214).
normal(215).
normal(217).
normal(218).
normal(219).
normal(221).
normal(222).
normal(223).
normal(225).
normal(226).
normal(227).
normal(229).
normal(230).
normal(231).
normal(233).
normal(234).
normal(235).
normal(237).
normal(238).
normal(239).
normal(241).
normal(242).
normal(243).
normal(245).
normal(246).
normal(247).
normal(249).
normal(250).
normal(251).
normal(253).
normal(254).
normal(255).
normal(257).
normal(258).
normal(259).
normal(261).
normal(262).
normal(263).
normal(265).
normal(266).
normal(267).
normal(269).
normal(270).
normal(271).
normal(273).
normal(274).
normal(275).
normal(277).
normal(278).
normal(279).
normal(281).
normal(282).
normal(283).
normal(285).
normal(286).
normal(287).
normal(289).
normal(290).
normal(291).
normal(293).
normal(294).
normal(295).
normal(297).
normal(298).
normal(299).
normal(300).
normal(301).
normal(302).
normal(303).
normal(305).
normal(306).
normal(307).
normal(309).
normal(310).
normal(311).
normal(313).
normal(314).
normal(315).
normal(317).
normal(318).
normal(319).
normal(321).
normal(322).
normal(323).
normal(325).
normal(326).
normal(327).
normal(329).
normal(330).
normal(331).
normal(333).
normal(334).
normal(335).
normal(337).
normal(338).
normal(339).
normal(341).
normal(342).
normal(343).
normal(345).
normal(346).
normal(347).
normal(349).
normal(350).
normal(351).
normal(353).
normal(354).
normal(355).
normal(357).
normal(358).
normal(359).
normal(361).
normal(362).
normal(363).
normal(365).
normal(366).
normal(367).
normal(369).
normal(370).
normal(371).
normal(373).
normal(374).
normal(375).
normal(377).
normal(378).
normal(379).
normal(381).
normal(382).
normal(383).
normal(385).
normal(386).
normal(387).
normal(389).
normal(390).
normal(391).
normal(393).
normal(394).
normal(395).
normal(397).
normal(398).
normal(399).
normal(401).
normal(402).
normal(403).
normal(405).
normal(406).
normal(407).
normal(409).
normal(410).
normal(411).
normal(413).
normal(414).
normal(415).
normal(417).
normal(418).
normal(419).
normal(421).
normal(422).
normal(423).
normal(425).
normal(426).
normal(427).
normal(429).
normal(430).
normal(431).
normal(433).
normal(434).
normal(435).
normal(437).
normal(438).
normal(439).
normal(441).
normal(442).
normal(443).
normal(445).
normal(446).
normal(447).
normal(449).
normal(450).
normal(451).
normal(453).
normal(454).
normal(455).
normal(457).
normal(458).
normal(459).
normal(461).
normal(462).
normal(463).
normal(465).
normal(466).
normal(467).
normal(469).
normal(470).
normal(471).
normal(473).
normal(474).
normal(475).
normal(477).
normal(478).
normal(479).
normal(481).
normal(482).
normal(483).
normal(485).
normal(486).
normal(487).
normal(489).
normal(490).
normal(491).
normal(493).
normal(494).
normal(495).
normal(497).
normal(498).
normal(499).
normal(500).
normal(501).
normal(502).
normal(503).
normal(505).
normal(506).
normal(507).
normal(509).
normal(510).
normal(511).
normal(513).
normal(514).
normal(515).
normal(517).
normal(518).
normal(519).
normal(521).
normal(522).
normal(523).
normal(525).
normal(526).
normal(527).
normal(529).
normal(530).
normal(531).
normal(533).
normal(534).
normal(535).
normal(537).
normal(538).
normal(539).
normal(541).
normal(542).
normal(543).
normal(545).
normal(546).
normal(547).
normal(549).
normal(550).
normal(551).
normal(553).
normal(554).
normal(555).
normal(557).
normal(558).
normal(559).
normal(561).
normal(562).
normal(563).
normal(565).
normal(566).
normal(567).
normal(569).
normal(570).
normal(571).
normal(573).
normal(574).
normal(575).
normal(577).
normal(578).
normal(579).
normal(581).
normal(582).
normal(583).
normal(585).
normal(586).
normal(587).
normal(589).
normal(590).
normal(591).
normal(593).
normal(594).
normal(595).
normal(597).
normal(598).
normal(599).
normal(600).
normal(601).
normal(602).
normal(603).
normal(605).
normal(606).
normal(607).
normal(609).
normal(610).
normal(611).
normal(613).
normal(614).
normal(615).
normal(617).
normal(618).
normal(619).
normal(621).
normal(622).
normal(623).
normal(625).
normal(626).
normal(627).
normal(629).
normal(630).
normal(631).
normal(633).
normal(634).
normal(635).
normal(637).
normal(638).
normal(639).
normal(641).
normal(642).
normal(643).
normal(645).
normal(646).
normal(647).
normal(649).
normal(650).
normal(651).
normal(653).
normal(654).
normal(655).
normal(657).
normal(658).
normal(659).
normal(661).
normal(662).
normal(663).
normal(665).
normal(666).
normal(667).
normal(669).
normal(670).
normal(671).
normal(673).
normal(674).
normal(675).
normal(677).
normal(678).
normal(679).
normal(681).
normal(682).
normal(683).
normal(685).
normal(686).
normal(687).
normal(689).
normal(690).
normal(691).
normal(693).
normal(694).
normal(695).
normal(697).
normal(698).
normal(699).
normal(700).
normal(701).
normal(702).
normal(703).
normal(705).
normal(706).
normal(707).
normal(709).
normal(710).
normal(711).
normal(713).
normal(714).
normal(715).
normal(717).
normal(718).
normal(719).
normal(721).
normal(722).
normal(723).
normal(725).
normal(726).
normal(727).
normal(729).
normal(730).
normal(731).
normal(733).
normal(734).
normal(735).
normal(737).
normal(738).
normal(739).
normal(741).
normal(742).
normal(743).
normal(745).
normal(746).
normal(747).
normal(749).
normal(750).
normal(751).
normal(753).
normal(754).
normal(755).
normal(757).
normal(758).
normal(759).
normal(761).
normal(762).
normal(763).
normal(765).
normal(766).
normal(767).
normal(769).
normal(770).
normal(771).
normal(773).
normal(774).
normal(775).
normal(777).
normal(778).
normal(779).
normal(781).
normal(782).
normal(783).
normal(785).
normal(786).
normal(787).
normal(789).
normal(790).
normal(791).
normal(793).
normal(794).
normal(795).
normal(797).
normal(798).
normal(799).
normal(801).
normal(802).
normal(803).
normal(805).
normal(806).
normal(807).
normal(809).
normal(810).
normal(811).
normal(813).
normal(814).
normal(815).
normal(817).
normal(818).
normal(819).
normal(821).
normal(822).
normal(823).
normal(825).
normal(826).
normal(827).
normal(829).
normal(830).
normal(831).
normal(833).
normal(834).
normal(835).
normal(837).
normal(838).
normal(839).
normal(841).
normal(842).
normal(843).
normal(845).
normal(846).
normal(847).
normal(849).
normal(850).
normal(851).
normal(853).
normal(854).
normal(855).
normal(857).
normal(858).
normal(859).
normal(861).
normal(862).
normal(863).
normal(865).
normal(866).
normal(867).
normal(869).
normal(870).
normal(871).
normal(873).
normal(874).
normal(875).
normal(877).
normal(878).
normal(879).
normal(881).
normal(882).
normal(883).
normal(885).
normal(886).
normal(887).
normal(889).
normal(890).
normal(891).
normal(893).
normal(894).
normal(895).
normal(897).
normal(898).
normal(899).
normal(900).
normal(901).
normal(902).
normal(903).
normal(905).
normal(906).
normal(907).
normal(909).
normal(910).
normal(911).
normal(913).
normal(914).
normal(915).
normal(917).
normal(918).
normal(919).
normal(921).
normal(922).
normal(923).
normal(925).
normal(926).
normal(927).
normal(929).
normal(930).
normal(931).
normal(933).
normal(934).
normal(935).
normal(937).
normal(938).
normal(939).
normal(941).
normal(942).
normal(943).
normal(945).
normal(946).
normal(947).
normal(949).
normal(950).
normal(951).
normal(953).
normal(954).
normal(955).
normal(957).
normal(958).
normal(959).
normal(961).
normal(962).
normal(963).
normal(965).
normal(966).
normal(967).
normal(969).
normal(970).
normal(971).
normal(973).
normal(974).
normal(975).
normal(977).
normal(978).
normal(979).
normal(981).
normal(982).
normal(983).
normal(985).
normal(986).
normal(987).
normal(989).
normal(990).
normal(991).
normal(993).
normal(994).
normal(995).
normal(997).
normal(998).
normal(999).
normal(1000).
normal(1001).
normal(1002).
normal(1003).
normal(1005).
normal(1006).
normal(1007).
normal(1009).
normal(1010).
normal(1011).
normal(1013).
normal(1014).
normal(1015).
normal(1017).
normal(1018).
normal(1019).
normal(1021).
normal(1022).
normal(1023).
normal(1025).
normal(1026).
normal(1027).
normal(1029).
normal(1030).
normal(1031).
normal(1033).
normal(1034).
normal(1035).
normal(1037).
normal(1038).
normal(1039).
normal(1041).
normal(1042).
normal(1043).
normal(1045).
normal(1046).
normal(1047).
normal(1049).
normal(1050).
normal(1051).
normal(1053).
normal(1054).
normal(1055).
normal(1057).
normal(1058).
normal(1059).
normal(1061).
normal(1062).
normal(1063).
normal(1065).
normal(1066).
normal(1067).
normal(1069).
normal(1070).
normal(1071).
normal(1073).
normal(1074).
normal(1075).
normal(1077).
normal(1078).
normal(1079).
normal(1081).
normal(1082).
normal(1083).
normal(1085).
normal(1086).
normal(1087).
normal(1089).
normal(1090).
normal(1091).
normal(1093).
normal(1094).
normal(1095).
normal(1097).
normal(1098).
normal(1099).
normal(1100).
normal(1101).
normal(1102).
normal(1103).
normal(1105).
normal(1106).
normal(1107).
normal(1109).
normal(1110).
normal(1111).
normal(1113).
normal(1114).
normal(1115).
normal(1117).
normal(1118).
normal(1119).
normal(1121).
normal(1122).
normal(1123).
normal(1125).
normal(1126).
normal(1127).
normal(1129).
normal(1130).
normal(1131).
normal(1133).
normal(1134).
normal(1135).
normal(1137).
normal(1138).
normal(1139).
normal(1141).
normal(1142).
normal(1143).
normal(1145).
normal(1146).
normal(1147).
normal(1149).
normal(1150).
normal(1151).
normal(1153).
normal(1154).
normal(1155).
normal(1157).
normal(1158).
normal(1159).
normal(1161).
normal(1162).
normal(1163).
normal(1165).
normal(1166).
normal(1167).
normal(1169).
normal(1170).
normal(1171).
normal(1173).
normal(1174).
normal(1175).
normal(1177).
normal(1178).
normal(1179).
normal(1181).
normal(1182).
normal(1183).
normal(1185).
normal(1186).
normal(1187).
normal(1189).
normal(1190).
normal(1191).
normal(1193).
normal(1194).
normal(1195).
normal(1197).
normal(1198).
normal(1199).
normal(1201).
normal(1202).
normal(1203).
normal(1205).
normal(1206).
normal(1207).
normal(1209).
normal(1210).
normal(1211).
normal(1213).
normal(1214).
normal(1215).
normal(1217).
normal(1218).
normal(1219).
normal(1221).
normal(1222).
normal(1223).
normal(1225).
normal(1226).
normal(1227).
normal(1229).
normal(1230).
normal(1231).
normal(1233).
normal(1234).
normal(1235).
normal(1237).
normal(1238).
normal(1239).
normal(1241).
normal(1242).
normal(1243).
normal(1245).
normal(1246).
normal(1247).
normal(1249).
normal(1250).
normal(1251).
normal(1253).
normal(1254).
normal(1255).
normal(1257).
normal(1258).
normal(1259).
normal(1261).
normal(1262).
normal(1263).
normal(1265).
normal(1266).
normal(1267).
normal(1269).
normal(1270).
normal(1271).
normal(1273).
normal(1274).
normal(1275).
normal(1277).
normal(1278).
normal(1279).
normal(1281).
normal(1282).
normal(1283).
normal(1285).
normal(1286).
normal(1287).
normal(1289).
normal(1290).
normal(1291).
normal(1293).
normal(1294).
normal(1295).
normal(1297).
normal(1298).
normal(1299).
normal(1300).
normal(1301).
normal(1302).
normal(1303).
normal(1305).
normal(1306).
normal(1307).
normal(1309).
normal(1310).
normal(1311).
normal(1313).
normal(1314).
normal(1315).
normal(1317).
normal(1318).
normal(1319).
normal(1321).
normal(1322).
normal(1323).
normal(1325).
normal(1326).
normal(1327).
normal(1329).
normal(1330).
normal(1331).
normal(1333).
normal(1334).
normal(1335).
normal(1337).
normal(1338).
normal(1339).
normal(1341).
normal(1342).
normal(1343).
normal(1345).
normal(1346).
normal(1347).
normal(1349).
normal(1350).
normal(1351).
normal(1353).
normal(1354).
normal(1355).
normal(1357).
normal(1358).
normal(1359).
normal(1361).
normal(1362).
normal(1363).
normal(1365).
normal(1366).
normal(1367).
normal(1369).
normal(1370).
normal(1371).
normal(1373).
normal(1374).
normal(1375).
normal(1377).
normal(1378).
normal(1379).
normal(1381).
normal(1382).
normal(1383).
normal(1385).
normal(1386).
normal(1387).
normal(1389).
normal(1390).
normal(1391).
normal(1393).
normal(1394).
normal(1395).
normal(1397).
normal(1398).
normal(1399).
normal(1400).
normal(1401).
normal(1402).
normal(1403).
normal(1405).
normal(1406).
normal(1407).
normal(1409).
normal(1410).
normal(1411).
normal(1413).
normal(1414).
normal(1415).
normal(1417).
normal(1418).
normal(1419).
normal(1421).
normal(1422).
normal(1423).
normal(1425).
normal(1426).
normal(1427).
normal(1429).
normal(1430).
normal(1431).
normal(1433).
normal(1434).
normal(1435).
normal(1437).
normal(1438).
normal(1439).
normal(1441).
normal(1442).
normal(1443).
normal(1445).
normal(1446).
normal(1447).
normal(1449).
normal(1450).
normal(1451).
normal(1453).
normal(1454).
normal(1455).
normal(1457).
normal(1458).
normal(1459).
normal(1461).
normal(1462).
normal(1463).
normal(1465).
normal(1466).
normal(1467).
normal(1469).
normal(1470).
normal(1471).
normal(1473).
normal(1474).
normal(1475).
normal(1477).
normal(1478).
normal(1479).
normal(1481).
normal(1482).
normal(1483).
normal(1485).
normal(1486).
normal(1487).
normal(1489).
normal(1490).
normal(1491).
normal(1493).
normal(1494).
normal(1495).
normal(1497).
normal(1498).
normal(1499).
normal(1500).
normal(1501).
normal(1502).
normal(1503).
normal(1505).
normal(1506).
normal(1507).
normal(1509).
normal(1510).
normal(1511).
normal(1513).
normal(1514).
normal(1515).
normal(1517).
normal(1518).
normal(1519).
normal(1521).
normal(1522).
normal(1523).
normal(1525).
normal(1526).
normal(1527).
normal(1529).
normal(1530).
normal(1531).
normal(1533).
normal(1534).
normal(1535).
normal(1537).
normal(1538).
normal(1539).
normal(1541).
normal(1542).
normal(1543).
normal(1545).
normal(1546).
normal(1547).
normal(1549).
normal(1550).
normal(1551).
normal(1553).
normal(1554).
normal(1555).
normal(1557).
normal(1558).
normal(1559).
normal(1561).
normal(1562).
normal(1563).
normal(1565).
normal(1566).
normal(1567).
normal(1569).
normal(1570).
normal(1571).
normal(1573).
normal(1574).
normal(1575).
normal(1577).
normal(1578).
normal(1579).
normal(1581).

% more examples

normal(1582).
normal(1583).
normal(1585).
normal(1586).
normal(1587).
normal(1589).
normal(1590).
normal(1591).
normal(1593).
normal(1594).
normal(1595).
normal(1597).
normal(1598).
normal(1599).
:-end_in_pos.
:-begin_in_neg.
normal(4).
normal(8).
normal(12).
normal(16).
normal(20).
normal(24).
normal(28).
normal(32).
normal(36).
normal(40).
normal(44).
normal(48).
normal(52).
normal(56).
normal(60).
normal(64).
normal(68).
normal(72).
normal(76).
normal(80).
normal(84).
normal(88).
normal(92).
normal(96).
normal(104).
normal(108).
normal(112).
normal(116).
normal(120).
normal(124).
normal(128).
normal(132).
normal(136).
normal(140).
normal(144).
normal(148).
normal(152).
normal(156).
normal(160).
normal(164).
normal(168).
normal(172).
normal(176).
normal(180).
normal(184).
normal(188).
normal(192).
normal(196).
normal(204).
normal(208).
normal(212).
normal(216).
normal(220).
normal(224).
normal(228).
normal(232).
normal(236).
normal(240).
normal(244).
normal(248).
normal(252).
normal(256).
normal(260).
normal(264).
normal(268).
normal(272).
normal(276).
normal(280).
normal(284).
normal(288).
normal(292).
normal(296).
normal(304).
normal(308).
normal(312).
normal(316).
normal(320).
normal(324).
normal(328).
normal(332).
normal(336).
normal(340).
normal(344).
normal(348).
normal(352).
normal(356).
normal(360).
normal(364).
normal(368).
normal(372).
normal(376).
normal(380).
normal(384).
normal(388).
normal(392).
normal(396).
normal(400).
normal(404).
normal(408).
normal(412).
normal(416).
normal(420).
normal(424).
normal(428).
normal(432).
normal(436).
normal(440).
normal(444).
normal(448).
normal(452).
normal(456).
normal(460).
normal(464).
normal(468).
normal(472).
normal(476).
normal(480).
normal(484).
normal(488).
normal(492).
normal(496).
normal(504).
normal(508).
normal(512).
normal(516).
normal(520).
normal(524).
normal(528).
normal(532).
normal(536).
normal(540).
normal(544).
normal(548).
normal(552).
normal(556).
normal(560).
normal(564).
normal(568).
normal(572).
normal(576).
normal(580).
normal(584).
normal(588).
normal(592).
normal(596).
normal(604).
normal(608).
normal(612).
normal(616).
normal(620).
normal(624).
normal(628).
normal(632).
normal(636).
normal(640).
normal(644).
normal(648).
normal(652).
normal(656).
normal(660).
normal(664).
normal(668).
normal(672).
normal(676).
normal(680).
normal(684).
normal(688).
normal(692).
normal(696).
normal(704).
normal(708).
normal(712).
normal(716).
normal(720).
normal(724).
normal(728).
normal(732).
normal(736).
normal(740).
normal(744).
normal(748).
normal(752).
normal(756).
normal(760).
normal(764).
normal(768).
normal(772).
normal(776).
normal(780).
normal(784).
normal(788).
normal(792).
normal(796).
normal(800).
normal(804).
normal(808).
normal(812).
normal(816).
normal(820).
normal(824).
normal(828).
normal(832).
normal(836).
normal(840).
normal(844).
normal(848).
normal(852).
normal(856).
normal(860).
normal(864).
normal(868).
normal(872).
normal(876).
normal(880).
normal(884).
normal(888).
normal(892).
normal(896).
normal(904).
normal(908).
normal(912).
normal(916).
normal(920).
normal(924).
normal(928).
normal(932).
normal(936).
normal(940).
normal(944).
normal(948).
normal(952).
normal(956).
normal(960).
normal(964).
normal(968).
normal(972).
normal(976).
normal(980).
normal(984).
normal(988).
normal(992).
normal(996).
normal(1004).
normal(1008).
normal(1012).
normal(1016).
normal(1020).
normal(1024).
normal(1028).
normal(1032).
normal(1036).
normal(1040).
normal(1044).
normal(1048).
normal(1052).
normal(1056).
normal(1060).
normal(1064).
normal(1068).
normal(1072).
normal(1076).
normal(1080).
normal(1084).
normal(1088).
normal(1092).
normal(1096).
normal(1104).
normal(1108).
normal(1112).
normal(1116).
normal(1120).
normal(1124).
normal(1128).
normal(1132).
normal(1136).
normal(1140).
normal(1144).
normal(1148).
normal(1152).
normal(1156).
normal(1160).
normal(1164).
normal(1168).
normal(1172).
normal(1176).
normal(1180).
normal(1184).
normal(1188).
normal(1192).
normal(1196).
normal(1200).
normal(1204).
normal(1208).
normal(1212).
normal(1216).
normal(1220).
normal(1224).
normal(1228).
normal(1232).
normal(1236).
normal(1240).
normal(1244).
normal(1248).
normal(1252).
normal(1256).
normal(1260).
normal(1264).
normal(1268).
normal(1272).
normal(1276).
normal(1280).
normal(1284).
normal(1288).
normal(1292).
normal(1296).
normal(1304).
normal(1308).
normal(1312).
normal(1316).
normal(1320).
normal(1324).
normal(1328).
normal(1332).
normal(1336).
normal(1340).
normal(1344).
normal(1348).
normal(1352).
normal(1356).
normal(1360).
normal(1364).
normal(1368).
normal(1372).
normal(1376).
normal(1380).
normal(1384).
normal(1388).
normal(1392).
normal(1396).
normal(1404).
normal(1408).
normal(1412).
normal(1416).
normal(1420).
normal(1424).
normal(1428).
normal(1432).
normal(1436).
normal(1440).
normal(1444).
normal(1448).
normal(1452).
normal(1456).
normal(1460).
normal(1464).
normal(1468).
normal(1472).
normal(1476).
normal(1480).
normal(1484).
normal(1488).
normal(1492).
normal(1496).
normal(1504).
normal(1508).
normal(1512).
normal(1516).
normal(1520).
normal(1524).
normal(1528).
normal(1532).
normal(1536).
normal(1540).
normal(1544).
normal(1548).
normal(1552).
normal(1556).
normal(1560).
normal(1564).
normal(1568).
normal(1572).
normal(1576).
normal(1580).

% more examples
normal(1584).
normal(1588).
normal(1592).
normal(1596).
normal(1600).
:-end_in_neg.