yap-6.3/docs/index/Benchmarks/tc_r_oo_chain2000.P

abolish_table_info :- at(tc_bench/2).

time :- statistics(runtime,_), benchmark, fail;
        statistics(runtime,[_,T]), write(T).

benchmark :- tc_bench(_Out1, _Out2).

:- table tc_bench/2.

tc_bench(A, B) :- chain(A, B).
tc_bench(A, B) :- chain(A, C), tc_bench(C, B).

chain(0,1).
chain(1,2).
chain(2,3).
chain(3,4).
chain(4,5).
chain(5,6).
chain(6,7).
chain(7,8).
chain(8,9).
chain(9,10).
chain(10,11).
chain(11,12).
chain(12,13).
chain(13,14).
chain(14,15).
chain(15,16).
chain(16,17).
chain(17,18).
chain(18,19).
chain(19,20).
chain(20,21).
chain(21,22).
chain(22,23).
chain(23,24).
chain(24,25).
chain(25,26).
chain(26,27).
chain(27,28).
chain(28,29).
chain(29,30).
chain(30,31).
chain(31,32).
chain(32,33).
chain(33,34).
chain(34,35).
chain(35,36).
chain(36,37).
chain(37,38).
chain(38,39).
chain(39,40).
chain(40,41).
chain(41,42).
chain(42,43).
chain(43,44).
chain(44,45).
chain(45,46).
chain(46,47).
chain(47,48).
chain(48,49).
chain(49,50).
chain(50,51).
chain(51,52).
chain(52,53).
chain(53,54).
chain(54,55).
chain(55,56).
chain(56,57).
chain(57,58).
chain(58,59).
chain(59,60).
chain(60,61).
chain(61,62).
chain(62,63).
chain(63,64).
chain(64,65).
chain(65,66).
chain(66,67).
chain(67,68).
chain(68,69).
chain(69,70).
chain(70,71).
chain(71,72).
chain(72,73).
chain(73,74).
chain(74,75).
chain(75,76).
chain(76,77).
chain(77,78).
chain(78,79).
chain(79,80).
chain(80,81).
chain(81,82).
chain(82,83).
chain(83,84).
chain(84,85).
chain(85,86).
chain(86,87).
chain(87,88).
chain(88,89).
chain(89,90).
chain(90,91).
chain(91,92).
chain(92,93).
chain(93,94).
chain(94,95).
chain(95,96).
chain(96,97).
chain(97,98).
chain(98,99).
chain(99,100).
chain(100,101).
chain(101,102).
chain(102,103).
chain(103,104).
chain(104,105).
chain(105,106).
chain(106,107).
chain(107,108).
chain(108,109).
chain(109,110).
chain(110,111).
chain(111,112).
chain(112,113).
chain(113,114).
chain(114,115).
chain(115,116).
chain(116,117).
chain(117,118).
chain(118,119).
chain(119,120).
chain(120,121).
chain(121,122).
chain(122,123).
chain(123,124).
chain(124,125).
chain(125,126).
chain(126,127).
chain(127,128).
chain(128,129).
chain(129,130).
chain(130,131).
chain(131,132).
chain(132,133).
chain(133,134).
chain(134,135).
chain(135,136).
chain(136,137).
chain(137,138).
chain(138,139).
chain(139,140).
chain(140,141).
chain(141,142).
chain(142,143).
chain(143,144).
chain(144,145).
chain(145,146).
chain(146,147).
chain(147,148).
chain(148,149).
chain(149,150).
chain(150,151).
chain(151,152).
chain(152,153).
chain(153,154).
chain(154,155).
chain(155,156).
chain(156,157).
chain(157,158).
chain(158,159).
chain(159,160).
chain(160,161).
chain(161,162).
chain(162,163).
chain(163,164).
chain(164,165).
chain(165,166).
chain(166,167).
chain(167,168).
chain(168,169).
chain(169,170).
chain(170,171).
chain(171,172).
chain(172,173).
chain(173,174).
chain(174,175).
chain(175,176).
chain(176,177).
chain(177,178).
chain(178,179).
chain(179,180).
chain(180,181).
chain(181,182).
chain(182,183).
chain(183,184).
chain(184,185).
chain(185,186).
chain(186,187).
chain(187,188).
chain(188,189).
chain(189,190).
chain(190,191).
chain(191,192).
chain(192,193).
chain(193,194).
chain(194,195).
chain(195,196).
chain(196,197).
chain(197,198).
chain(198,199).
chain(199,200).
chain(200,201).
chain(201,202).
chain(202,203).
chain(203,204).
chain(204,205).
chain(205,206).
chain(206,207).
chain(207,208).
chain(208,209).
chain(209,210).
chain(210,211).
chain(211,212).
chain(212,213).
chain(213,214).
chain(214,215).
chain(215,216).
chain(216,217).
chain(217,218).
chain(218,219).
chain(219,220).
chain(220,221).
chain(221,222).
chain(222,223).
chain(223,224).
chain(224,225).
chain(225,226).
chain(226,227).
chain(227,228).
chain(228,229).
chain(229,230).
chain(230,231).
chain(231,232).
chain(232,233).
chain(233,234).
chain(234,235).
chain(235,236).
chain(236,237).
chain(237,238).
chain(238,239).
chain(239,240).
chain(240,241).
chain(241,242).
chain(242,243).
chain(243,244).
chain(244,245).
chain(245,246).
chain(246,247).
chain(247,248).
chain(248,249).
chain(249,250).
chain(250,251).
chain(251,252).
chain(252,253).
chain(253,254).
chain(254,255).
chain(255,256).
chain(256,257).
chain(257,258).
chain(258,259).
chain(259,260).
chain(260,261).
chain(261,262).
chain(262,263).
chain(263,264).
chain(264,265).
chain(265,266).
chain(266,267).
chain(267,268).
chain(268,269).
chain(269,270).
chain(270,271).
chain(271,272).
chain(272,273).
chain(273,274).
chain(274,275).
chain(275,276).
chain(276,277).
chain(277,278).
chain(278,279).
chain(279,280).
chain(280,281).
chain(281,282).
chain(282,283).
chain(283,284).
chain(284,285).
chain(285,286).
chain(286,287).
chain(287,288).
chain(288,289).
chain(289,290).
chain(290,291).
chain(291,292).
chain(292,293).
chain(293,294).
chain(294,295).
chain(295,296).
chain(296,297).
chain(297,298).
chain(298,299).
chain(299,300).
chain(300,301).
chain(301,302).
chain(302,303).
chain(303,304).
chain(304,305).
chain(305,306).
chain(306,307).
chain(307,308).
chain(308,309).
chain(309,310).
chain(310,311).
chain(311,312).
chain(312,313).
chain(313,314).
chain(314,315).
chain(315,316).
chain(316,317).
chain(317,318).
chain(318,319).
chain(319,320).
chain(320,321).
chain(321,322).
chain(322,323).
chain(323,324).
chain(324,325).
chain(325,326).
chain(326,327).
chain(327,328).
chain(328,329).
chain(329,330).
chain(330,331).
chain(331,332).
chain(332,333).
chain(333,334).
chain(334,335).
chain(335,336).
chain(336,337).
chain(337,338).
chain(338,339).
chain(339,340).
chain(340,341).
chain(341,342).
chain(342,343).
chain(343,344).
chain(344,345).
chain(345,346).
chain(346,347).
chain(347,348).
chain(348,349).
chain(349,350).
chain(350,351).
chain(351,352).
chain(352,353).
chain(353,354).
chain(354,355).
chain(355,356).
chain(356,357).
chain(357,358).
chain(358,359).
chain(359,360).
chain(360,361).
chain(361,362).
chain(362,363).
chain(363,364).
chain(364,365).
chain(365,366).
chain(366,367).
chain(367,368).
chain(368,369).
chain(369,370).
chain(370,371).
chain(371,372).
chain(372,373).
chain(373,374).
chain(374,375).
chain(375,376).
chain(376,377).
chain(377,378).
chain(378,379).
chain(379,380).
chain(380,381).
chain(381,382).
chain(382,383).
chain(383,384).
chain(384,385).
chain(385,386).
chain(386,387).
chain(387,388).
chain(388,389).
chain(389,390).
chain(390,391).
chain(391,392).
chain(392,393).
chain(393,394).
chain(394,395).
chain(395,396).
chain(396,397).
chain(397,398).
chain(398,399).
chain(399,400).
chain(400,401).
chain(401,402).
chain(402,403).
chain(403,404).
chain(404,405).
chain(405,406).
chain(406,407).
chain(407,408).
chain(408,409).
chain(409,410).
chain(410,411).
chain(411,412).
chain(412,413).
chain(413,414).
chain(414,415).
chain(415,416).
chain(416,417).
chain(417,418).
chain(418,419).
chain(419,420).
chain(420,421).
chain(421,422).
chain(422,423).
chain(423,424).
chain(424,425).
chain(425,426).
chain(426,427).
chain(427,428).
chain(428,429).
chain(429,430).
chain(430,431).
chain(431,432).
chain(432,433).
chain(433,434).
chain(434,435).
chain(435,436).
chain(436,437).
chain(437,438).
chain(438,439).
chain(439,440).
chain(440,441).
chain(441,442).
chain(442,443).
chain(443,444).
chain(444,445).
chain(445,446).
chain(446,447).
chain(447,448).
chain(448,449).
chain(449,450).
chain(450,451).
chain(451,452).
chain(452,453).
chain(453,454).
chain(454,455).
chain(455,456).
chain(456,457).
chain(457,458).
chain(458,459).
chain(459,460).
chain(460,461).
chain(461,462).
chain(462,463).
chain(463,464).
chain(464,465).
chain(465,466).
chain(466,467).
chain(467,468).
chain(468,469).
chain(469,470).
chain(470,471).
chain(471,472).
chain(472,473).
chain(473,474).
chain(474,475).
chain(475,476).
chain(476,477).
chain(477,478).
chain(478,479).
chain(479,480).
chain(480,481).
chain(481,482).
chain(482,483).
chain(483,484).
chain(484,485).
chain(485,486).
chain(486,487).
chain(487,488).
chain(488,489).
chain(489,490).
chain(490,491).
chain(491,492).
chain(492,493).
chain(493,494).
chain(494,495).
chain(495,496).
chain(496,497).
chain(497,498).
chain(498,499).
chain(499,500).
chain(500,501).
chain(501,502).
chain(502,503).
chain(503,504).
chain(504,505).
chain(505,506).
chain(506,507).
chain(507,508).
chain(508,509).
chain(509,510).
chain(510,511).
chain(511,512).
chain(512,513).
chain(513,514).
chain(514,515).
chain(515,516).
chain(516,517).
chain(517,518).
chain(518,519).
chain(519,520).
chain(520,521).
chain(521,522).
chain(522,523).
chain(523,524).
chain(524,525).
chain(525,526).
chain(526,527).
chain(527,528).
chain(528,529).
chain(529,530).
chain(530,531).
chain(531,532).
chain(532,533).
chain(533,534).
chain(534,535).
chain(535,536).
chain(536,537).
chain(537,538).
chain(538,539).
chain(539,540).
chain(540,541).
chain(541,542).
chain(542,543).
chain(543,544).
chain(544,545).
chain(545,546).
chain(546,547).
chain(547,548).
chain(548,549).
chain(549,550).
chain(550,551).
chain(551,552).
chain(552,553).
chain(553,554).
chain(554,555).
chain(555,556).
chain(556,557).
chain(557,558).
chain(558,559).
chain(559,560).
chain(560,561).
chain(561,562).
chain(562,563).
chain(563,564).
chain(564,565).
chain(565,566).
chain(566,567).
chain(567,568).
chain(568,569).
chain(569,570).
chain(570,571).
chain(571,572).
chain(572,573).
chain(573,574).
chain(574,575).
chain(575,576).
chain(576,577).
chain(577,578).
chain(578,579).
chain(579,580).
chain(580,581).
chain(581,582).
chain(582,583).
chain(583,584).
chain(584,585).
chain(585,586).
chain(586,587).
chain(587,588).
chain(588,589).
chain(589,590).
chain(590,591).
chain(591,592).
chain(592,593).
chain(593,594).
chain(594,595).
chain(595,596).
chain(596,597).
chain(597,598).
chain(598,599).
chain(599,600).
chain(600,601).
chain(601,602).
chain(602,603).
chain(603,604).
chain(604,605).
chain(605,606).
chain(606,607).
chain(607,608).
chain(608,609).
chain(609,610).
chain(610,611).
chain(611,612).
chain(612,613).
chain(613,614).
chain(614,615).
chain(615,616).
chain(616,617).
chain(617,618).
chain(618,619).
chain(619,620).
chain(620,621).
chain(621,622).
chain(622,623).
chain(623,624).
chain(624,625).
chain(625,626).
chain(626,627).
chain(627,628).
chain(628,629).
chain(629,630).
chain(630,631).
chain(631,632).
chain(632,633).
chain(633,634).
chain(634,635).
chain(635,636).
chain(636,637).
chain(637,638).
chain(638,639).
chain(639,640).
chain(640,641).
chain(641,642).
chain(642,643).
chain(643,644).
chain(644,645).
chain(645,646).
chain(646,647).
chain(647,648).
chain(648,649).
chain(649,650).
chain(650,651).
chain(651,652).
chain(652,653).
chain(653,654).
chain(654,655).
chain(655,656).
chain(656,657).
chain(657,658).
chain(658,659).
chain(659,660).
chain(660,661).
chain(661,662).
chain(662,663).
chain(663,664).
chain(664,665).
chain(665,666).
chain(666,667).
chain(667,668).
chain(668,669).
chain(669,670).
chain(670,671).
chain(671,672).
chain(672,673).
chain(673,674).
chain(674,675).
chain(675,676).
chain(676,677).
chain(677,678).
chain(678,679).
chain(679,680).
chain(680,681).
chain(681,682).
chain(682,683).
chain(683,684).
chain(684,685).
chain(685,686).
chain(686,687).
chain(687,688).
chain(688,689).
chain(689,690).
chain(690,691).
chain(691,692).
chain(692,693).
chain(693,694).
chain(694,695).
chain(695,696).
chain(696,697).
chain(697,698).
chain(698,699).
chain(699,700).
chain(700,701).
chain(701,702).
chain(702,703).
chain(703,704).
chain(704,705).
chain(705,706).
chain(706,707).
chain(707,708).
chain(708,709).
chain(709,710).
chain(710,711).
chain(711,712).
chain(712,713).
chain(713,714).
chain(714,715).
chain(715,716).
chain(716,717).
chain(717,718).
chain(718,719).
chain(719,720).
chain(720,721).
chain(721,722).
chain(722,723).
chain(723,724).
chain(724,725).
chain(725,726).
chain(726,727).
chain(727,728).
chain(728,729).
chain(729,730).
chain(730,731).
chain(731,732).
chain(732,733).
chain(733,734).
chain(734,735).
chain(735,736).
chain(736,737).
chain(737,738).
chain(738,739).
chain(739,740).
chain(740,741).
chain(741,742).
chain(742,743).
chain(743,744).
chain(744,745).
chain(745,746).
chain(746,747).
chain(747,748).
chain(748,749).
chain(749,750).
chain(750,751).
chain(751,752).
chain(752,753).
chain(753,754).
chain(754,755).
chain(755,756).
chain(756,757).
chain(757,758).
chain(758,759).
chain(759,760).
chain(760,761).
chain(761,762).
chain(762,763).
chain(763,764).
chain(764,765).
chain(765,766).
chain(766,767).
chain(767,768).
chain(768,769).
chain(769,770).
chain(770,771).
chain(771,772).
chain(772,773).
chain(773,774).
chain(774,775).
chain(775,776).
chain(776,777).
chain(777,778).
chain(778,779).
chain(779,780).
chain(780,781).
chain(781,782).
chain(782,783).
chain(783,784).
chain(784,785).
chain(785,786).
chain(786,787).
chain(787,788).
chain(788,789).
chain(789,790).
chain(790,791).
chain(791,792).
chain(792,793).
chain(793,794).
chain(794,795).
chain(795,796).
chain(796,797).
chain(797,798).
chain(798,799).
chain(799,800).
chain(800,801).
chain(801,802).
chain(802,803).
chain(803,804).
chain(804,805).
chain(805,806).
chain(806,807).
chain(807,808).
chain(808,809).
chain(809,810).
chain(810,811).
chain(811,812).
chain(812,813).
chain(813,814).
chain(814,815).
chain(815,816).
chain(816,817).
chain(817,818).
chain(818,819).
chain(819,820).
chain(820,821).
chain(821,822).
chain(822,823).
chain(823,824).
chain(824,825).
chain(825,826).
chain(826,827).
chain(827,828).
chain(828,829).
chain(829,830).
chain(830,831).
chain(831,832).
chain(832,833).
chain(833,834).
chain(834,835).
chain(835,836).
chain(836,837).
chain(837,838).
chain(838,839).
chain(839,840).
chain(840,841).
chain(841,842).
chain(842,843).
chain(843,844).
chain(844,845).
chain(845,846).
chain(846,847).
chain(847,848).
chain(848,849).
chain(849,850).
chain(850,851).
chain(851,852).
chain(852,853).
chain(853,854).
chain(854,855).
chain(855,856).
chain(856,857).
chain(857,858).
chain(858,859).
chain(859,860).
chain(860,861).
chain(861,862).
chain(862,863).
chain(863,864).
chain(864,865).
chain(865,866).
chain(866,867).
chain(867,868).
chain(868,869).
chain(869,870).
chain(870,871).
chain(871,872).
chain(872,873).
chain(873,874).
chain(874,875).
chain(875,876).
chain(876,877).
chain(877,878).
chain(878,879).
chain(879,880).
chain(880,881).
chain(881,882).
chain(882,883).
chain(883,884).
chain(884,885).
chain(885,886).
chain(886,887).
chain(887,888).
chain(888,889).
chain(889,890).
chain(890,891).
chain(891,892).
chain(892,893).
chain(893,894).
chain(894,895).
chain(895,896).
chain(896,897).
chain(897,898).
chain(898,899).
chain(899,900).
chain(900,901).
chain(901,902).
chain(902,903).
chain(903,904).
chain(904,905).
chain(905,906).
chain(906,907).
chain(907,908).
chain(908,909).
chain(909,910).
chain(910,911).
chain(911,912).
chain(912,913).
chain(913,914).
chain(914,915).
chain(915,916).
chain(916,917).
chain(917,918).
chain(918,919).
chain(919,920).
chain(920,921).
chain(921,922).
chain(922,923).
chain(923,924).
chain(924,925).
chain(925,926).
chain(926,927).
chain(927,928).
chain(928,929).
chain(929,930).
chain(930,931).
chain(931,932).
chain(932,933).
chain(933,934).
chain(934,935).
chain(935,936).
chain(936,937).
chain(937,938).
chain(938,939).
chain(939,940).
chain(940,941).
chain(941,942).
chain(942,943).
chain(943,944).
chain(944,945).
chain(945,946).
chain(946,947).
chain(947,948).
chain(948,949).
chain(949,950).
chain(950,951).
chain(951,952).
chain(952,953).
chain(953,954).
chain(954,955).
chain(955,956).
chain(956,957).
chain(957,958).
chain(958,959).
chain(959,960).
chain(960,961).
chain(961,962).
chain(962,963).
chain(963,964).
chain(964,965).
chain(965,966).
chain(966,967).
chain(967,968).
chain(968,969).
chain(969,970).
chain(970,971).
chain(971,972).
chain(972,973).
chain(973,974).
chain(974,975).
chain(975,976).
chain(976,977).
chain(977,978).
chain(978,979).
chain(979,980).
chain(980,981).
chain(981,982).
chain(982,983).
chain(983,984).
chain(984,985).
chain(985,986).
chain(986,987).
chain(987,988).
chain(988,989).
chain(989,990).
chain(990,991).
chain(991,992).
chain(992,993).
chain(993,994).
chain(994,995).
chain(995,996).
chain(996,997).
chain(997,998).
chain(998,999).
chain(999,1000).
chain(1000,1001).
chain(1001,1002).
chain(1002,1003).
chain(1003,1004).
chain(1004,1005).
chain(1005,1006).
chain(1006,1007).
chain(1007,1008).
chain(1008,1009).
chain(1009,1010).
chain(1010,1011).
chain(1011,1012).
chain(1012,1013).
chain(1013,1014).
chain(1014,1015).
chain(1015,1016).
chain(1016,1017).
chain(1017,1018).
chain(1018,1019).
chain(1019,1020).
chain(1020,1021).
chain(1021,1022).
chain(1022,1023).
chain(1023,1024).
chain(1024,1025).
chain(1025,1026).
chain(1026,1027).
chain(1027,1028).
chain(1028,1029).
chain(1029,1030).
chain(1030,1031).
chain(1031,1032).
chain(1032,1033).
chain(1033,1034).
chain(1034,1035).
chain(1035,1036).
chain(1036,1037).
chain(1037,1038).
chain(1038,1039).
chain(1039,1040).
chain(1040,1041).
chain(1041,1042).
chain(1042,1043).
chain(1043,1044).
chain(1044,1045).
chain(1045,1046).
chain(1046,1047).
chain(1047,1048).
chain(1048,1049).
chain(1049,1050).
chain(1050,1051).
chain(1051,1052).
chain(1052,1053).
chain(1053,1054).
chain(1054,1055).
chain(1055,1056).
chain(1056,1057).
chain(1057,1058).
chain(1058,1059).
chain(1059,1060).
chain(1060,1061).
chain(1061,1062).
chain(1062,1063).
chain(1063,1064).
chain(1064,1065).
chain(1065,1066).
chain(1066,1067).
chain(1067,1068).
chain(1068,1069).
chain(1069,1070).
chain(1070,1071).
chain(1071,1072).
chain(1072,1073).
chain(1073,1074).
chain(1074,1075).
chain(1075,1076).
chain(1076,1077).
chain(1077,1078).
chain(1078,1079).
chain(1079,1080).
chain(1080,1081).
chain(1081,1082).
chain(1082,1083).
chain(1083,1084).
chain(1084,1085).
chain(1085,1086).
chain(1086,1087).
chain(1087,1088).
chain(1088,1089).
chain(1089,1090).
chain(1090,1091).
chain(1091,1092).
chain(1092,1093).
chain(1093,1094).
chain(1094,1095).
chain(1095,1096).
chain(1096,1097).
chain(1097,1098).
chain(1098,1099).
chain(1099,1100).
chain(1100,1101).
chain(1101,1102).
chain(1102,1103).
chain(1103,1104).
chain(1104,1105).
chain(1105,1106).
chain(1106,1107).
chain(1107,1108).
chain(1108,1109).
chain(1109,1110).
chain(1110,1111).
chain(1111,1112).
chain(1112,1113).
chain(1113,1114).
chain(1114,1115).
chain(1115,1116).
chain(1116,1117).
chain(1117,1118).
chain(1118,1119).
chain(1119,1120).
chain(1120,1121).
chain(1121,1122).
chain(1122,1123).
chain(1123,1124).
chain(1124,1125).
chain(1125,1126).
chain(1126,1127).
chain(1127,1128).
chain(1128,1129).
chain(1129,1130).
chain(1130,1131).
chain(1131,1132).
chain(1132,1133).
chain(1133,1134).
chain(1134,1135).
chain(1135,1136).
chain(1136,1137).
chain(1137,1138).
chain(1138,1139).
chain(1139,1140).
chain(1140,1141).
chain(1141,1142).
chain(1142,1143).
chain(1143,1144).
chain(1144,1145).
chain(1145,1146).
chain(1146,1147).
chain(1147,1148).
chain(1148,1149).
chain(1149,1150).
chain(1150,1151).
chain(1151,1152).
chain(1152,1153).
chain(1153,1154).
chain(1154,1155).
chain(1155,1156).
chain(1156,1157).
chain(1157,1158).
chain(1158,1159).
chain(1159,1160).
chain(1160,1161).
chain(1161,1162).
chain(1162,1163).
chain(1163,1164).
chain(1164,1165).
chain(1165,1166).
chain(1166,1167).
chain(1167,1168).
chain(1168,1169).
chain(1169,1170).
chain(1170,1171).
chain(1171,1172).
chain(1172,1173).
chain(1173,1174).
chain(1174,1175).
chain(1175,1176).
chain(1176,1177).
chain(1177,1178).
chain(1178,1179).
chain(1179,1180).
chain(1180,1181).
chain(1181,1182).
chain(1182,1183).
chain(1183,1184).
chain(1184,1185).
chain(1185,1186).
chain(1186,1187).
chain(1187,1188).
chain(1188,1189).
chain(1189,1190).
chain(1190,1191).
chain(1191,1192).
chain(1192,1193).
chain(1193,1194).
chain(1194,1195).
chain(1195,1196).
chain(1196,1197).
chain(1197,1198).
chain(1198,1199).
chain(1199,1200).
chain(1200,1201).
chain(1201,1202).
chain(1202,1203).
chain(1203,1204).
chain(1204,1205).
chain(1205,1206).
chain(1206,1207).
chain(1207,1208).
chain(1208,1209).
chain(1209,1210).
chain(1210,1211).
chain(1211,1212).
chain(1212,1213).
chain(1213,1214).
chain(1214,1215).
chain(1215,1216).
chain(1216,1217).
chain(1217,1218).
chain(1218,1219).
chain(1219,1220).
chain(1220,1221).
chain(1221,1222).
chain(1222,1223).
chain(1223,1224).
chain(1224,1225).
chain(1225,1226).
chain(1226,1227).
chain(1227,1228).
chain(1228,1229).
chain(1229,1230).
chain(1230,1231).
chain(1231,1232).
chain(1232,1233).
chain(1233,1234).
chain(1234,1235).
chain(1235,1236).
chain(1236,1237).
chain(1237,1238).
chain(1238,1239).
chain(1239,1240).
chain(1240,1241).
chain(1241,1242).
chain(1242,1243).
chain(1243,1244).
chain(1244,1245).
chain(1245,1246).
chain(1246,1247).
chain(1247,1248).
chain(1248,1249).
chain(1249,1250).
chain(1250,1251).
chain(1251,1252).
chain(1252,1253).
chain(1253,1254).
chain(1254,1255).
chain(1255,1256).
chain(1256,1257).
chain(1257,1258).
chain(1258,1259).
chain(1259,1260).
chain(1260,1261).
chain(1261,1262).
chain(1262,1263).
chain(1263,1264).
chain(1264,1265).
chain(1265,1266).
chain(1266,1267).
chain(1267,1268).
chain(1268,1269).
chain(1269,1270).
chain(1270,1271).
chain(1271,1272).
chain(1272,1273).
chain(1273,1274).
chain(1274,1275).
chain(1275,1276).
chain(1276,1277).
chain(1277,1278).
chain(1278,1279).
chain(1279,1280).
chain(1280,1281).
chain(1281,1282).
chain(1282,1283).
chain(1283,1284).
chain(1284,1285).
chain(1285,1286).
chain(1286,1287).
chain(1287,1288).
chain(1288,1289).
chain(1289,1290).
chain(1290,1291).
chain(1291,1292).
chain(1292,1293).
chain(1293,1294).
chain(1294,1295).
chain(1295,1296).
chain(1296,1297).
chain(1297,1298).
chain(1298,1299).
chain(1299,1300).
chain(1300,1301).
chain(1301,1302).
chain(1302,1303).
chain(1303,1304).
chain(1304,1305).
chain(1305,1306).
chain(1306,1307).
chain(1307,1308).
chain(1308,1309).
chain(1309,1310).
chain(1310,1311).
chain(1311,1312).
chain(1312,1313).
chain(1313,1314).
chain(1314,1315).
chain(1315,1316).
chain(1316,1317).
chain(1317,1318).
chain(1318,1319).
chain(1319,1320).
chain(1320,1321).
chain(1321,1322).
chain(1322,1323).
chain(1323,1324).
chain(1324,1325).
chain(1325,1326).
chain(1326,1327).
chain(1327,1328).
chain(1328,1329).
chain(1329,1330).
chain(1330,1331).
chain(1331,1332).
chain(1332,1333).
chain(1333,1334).
chain(1334,1335).
chain(1335,1336).
chain(1336,1337).
chain(1337,1338).
chain(1338,1339).
chain(1339,1340).
chain(1340,1341).
chain(1341,1342).
chain(1342,1343).
chain(1343,1344).
chain(1344,1345).
chain(1345,1346).
chain(1346,1347).
chain(1347,1348).
chain(1348,1349).
chain(1349,1350).
chain(1350,1351).
chain(1351,1352).
chain(1352,1353).
chain(1353,1354).
chain(1354,1355).
chain(1355,1356).
chain(1356,1357).
chain(1357,1358).
chain(1358,1359).
chain(1359,1360).
chain(1360,1361).
chain(1361,1362).
chain(1362,1363).
chain(1363,1364).
chain(1364,1365).
chain(1365,1366).
chain(1366,1367).
chain(1367,1368).
chain(1368,1369).
chain(1369,1370).
chain(1370,1371).
chain(1371,1372).
chain(1372,1373).
chain(1373,1374).
chain(1374,1375).
chain(1375,1376).
chain(1376,1377).
chain(1377,1378).
chain(1378,1379).
chain(1379,1380).
chain(1380,1381).
chain(1381,1382).
chain(1382,1383).
chain(1383,1384).
chain(1384,1385).
chain(1385,1386).
chain(1386,1387).
chain(1387,1388).
chain(1388,1389).
chain(1389,1390).
chain(1390,1391).
chain(1391,1392).
chain(1392,1393).
chain(1393,1394).
chain(1394,1395).
chain(1395,1396).
chain(1396,1397).
chain(1397,1398).
chain(1398,1399).
chain(1399,1400).
chain(1400,1401).
chain(1401,1402).
chain(1402,1403).
chain(1403,1404).
chain(1404,1405).
chain(1405,1406).
chain(1406,1407).
chain(1407,1408).
chain(1408,1409).
chain(1409,1410).
chain(1410,1411).
chain(1411,1412).
chain(1412,1413).
chain(1413,1414).
chain(1414,1415).
chain(1415,1416).
chain(1416,1417).
chain(1417,1418).
chain(1418,1419).
chain(1419,1420).
chain(1420,1421).
chain(1421,1422).
chain(1422,1423).
chain(1423,1424).
chain(1424,1425).
chain(1425,1426).
chain(1426,1427).
chain(1427,1428).
chain(1428,1429).
chain(1429,1430).
chain(1430,1431).
chain(1431,1432).
chain(1432,1433).
chain(1433,1434).
chain(1434,1435).
chain(1435,1436).
chain(1436,1437).
chain(1437,1438).
chain(1438,1439).
chain(1439,1440).
chain(1440,1441).
chain(1441,1442).
chain(1442,1443).
chain(1443,1444).
chain(1444,1445).
chain(1445,1446).
chain(1446,1447).
chain(1447,1448).
chain(1448,1449).
chain(1449,1450).
chain(1450,1451).
chain(1451,1452).
chain(1452,1453).
chain(1453,1454).
chain(1454,1455).
chain(1455,1456).
chain(1456,1457).
chain(1457,1458).
chain(1458,1459).
chain(1459,1460).
chain(1460,1461).
chain(1461,1462).
chain(1462,1463).
chain(1463,1464).
chain(1464,1465).
chain(1465,1466).
chain(1466,1467).
chain(1467,1468).
chain(1468,1469).
chain(1469,1470).
chain(1470,1471).
chain(1471,1472).
chain(1472,1473).
chain(1473,1474).
chain(1474,1475).
chain(1475,1476).
chain(1476,1477).
chain(1477,1478).
chain(1478,1479).
chain(1479,1480).
chain(1480,1481).
chain(1481,1482).
chain(1482,1483).
chain(1483,1484).
chain(1484,1485).
chain(1485,1486).
chain(1486,1487).
chain(1487,1488).
chain(1488,1489).
chain(1489,1490).
chain(1490,1491).
chain(1491,1492).
chain(1492,1493).
chain(1493,1494).
chain(1494,1495).
chain(1495,1496).
chain(1496,1497).
chain(1497,1498).
chain(1498,1499).
chain(1499,1500).
chain(1500,1501).
chain(1501,1502).
chain(1502,1503).
chain(1503,1504).
chain(1504,1505).
chain(1505,1506).
chain(1506,1507).
chain(1507,1508).
chain(1508,1509).
chain(1509,1510).
chain(1510,1511).
chain(1511,1512).
chain(1512,1513).
chain(1513,1514).
chain(1514,1515).
chain(1515,1516).
chain(1516,1517).
chain(1517,1518).
chain(1518,1519).
chain(1519,1520).
chain(1520,1521).
chain(1521,1522).
chain(1522,1523).
chain(1523,1524).
chain(1524,1525).
chain(1525,1526).
chain(1526,1527).
chain(1527,1528).
chain(1528,1529).
chain(1529,1530).
chain(1530,1531).
chain(1531,1532).
chain(1532,1533).
chain(1533,1534).
chain(1534,1535).
chain(1535,1536).
chain(1536,1537).
chain(1537,1538).
chain(1538,1539).
chain(1539,1540).
chain(1540,1541).
chain(1541,1542).
chain(1542,1543).
chain(1543,1544).
chain(1544,1545).
chain(1545,1546).
chain(1546,1547).
chain(1547,1548).
chain(1548,1549).
chain(1549,1550).
chain(1550,1551).
chain(1551,1552).
chain(1552,1553).
chain(1553,1554).
chain(1554,1555).
chain(1555,1556).
chain(1556,1557).
chain(1557,1558).
chain(1558,1559).
chain(1559,1560).
chain(1560,1561).
chain(1561,1562).
chain(1562,1563).
chain(1563,1564).
chain(1564,1565).
chain(1565,1566).
chain(1566,1567).
chain(1567,1568).
chain(1568,1569).
chain(1569,1570).
chain(1570,1571).
chain(1571,1572).
chain(1572,1573).
chain(1573,1574).
chain(1574,1575).
chain(1575,1576).
chain(1576,1577).
chain(1577,1578).
chain(1578,1579).
chain(1579,1580).
chain(1580,1581).
chain(1581,1582).
chain(1582,1583).
chain(1583,1584).
chain(1584,1585).
chain(1585,1586).
chain(1586,1587).
chain(1587,1588).
chain(1588,1589).
chain(1589,1590).
chain(1590,1591).
chain(1591,1592).
chain(1592,1593).
chain(1593,1594).
chain(1594,1595).
chain(1595,1596).
chain(1596,1597).
chain(1597,1598).
chain(1598,1599).
chain(1599,1600).
chain(1600,1601).
chain(1601,1602).
chain(1602,1603).
chain(1603,1604).
chain(1604,1605).
chain(1605,1606).
chain(1606,1607).
chain(1607,1608).
chain(1608,1609).
chain(1609,1610).
chain(1610,1611).
chain(1611,1612).
chain(1612,1613).
chain(1613,1614).
chain(1614,1615).
chain(1615,1616).
chain(1616,1617).
chain(1617,1618).
chain(1618,1619).
chain(1619,1620).
chain(1620,1621).
chain(1621,1622).
chain(1622,1623).
chain(1623,1624).
chain(1624,1625).
chain(1625,1626).
chain(1626,1627).
chain(1627,1628).
chain(1628,1629).
chain(1629,1630).
chain(1630,1631).
chain(1631,1632).
chain(1632,1633).
chain(1633,1634).
chain(1634,1635).
chain(1635,1636).
chain(1636,1637).
chain(1637,1638).
chain(1638,1639).
chain(1639,1640).
chain(1640,1641).
chain(1641,1642).
chain(1642,1643).
chain(1643,1644).
chain(1644,1645).
chain(1645,1646).
chain(1646,1647).
chain(1647,1648).
chain(1648,1649).
chain(1649,1650).
chain(1650,1651).
chain(1651,1652).
chain(1652,1653).
chain(1653,1654).
chain(1654,1655).
chain(1655,1656).
chain(1656,1657).
chain(1657,1658).
chain(1658,1659).
chain(1659,1660).
chain(1660,1661).
chain(1661,1662).
chain(1662,1663).
chain(1663,1664).
chain(1664,1665).
chain(1665,1666).
chain(1666,1667).
chain(1667,1668).
chain(1668,1669).
chain(1669,1670).
chain(1670,1671).
chain(1671,1672).
chain(1672,1673).
chain(1673,1674).
chain(1674,1675).
chain(1675,1676).
chain(1676,1677).
chain(1677,1678).
chain(1678,1679).
chain(1679,1680).
chain(1680,1681).
chain(1681,1682).
chain(1682,1683).
chain(1683,1684).
chain(1684,1685).
chain(1685,1686).
chain(1686,1687).
chain(1687,1688).
chain(1688,1689).
chain(1689,1690).
chain(1690,1691).
chain(1691,1692).
chain(1692,1693).
chain(1693,1694).
chain(1694,1695).
chain(1695,1696).
chain(1696,1697).
chain(1697,1698).
chain(1698,1699).
chain(1699,1700).
chain(1700,1701).
chain(1701,1702).
chain(1702,1703).
chain(1703,1704).
chain(1704,1705).
chain(1705,1706).
chain(1706,1707).
chain(1707,1708).
chain(1708,1709).
chain(1709,1710).
chain(1710,1711).
chain(1711,1712).
chain(1712,1713).
chain(1713,1714).
chain(1714,1715).
chain(1715,1716).
chain(1716,1717).
chain(1717,1718).
chain(1718,1719).
chain(1719,1720).
chain(1720,1721).
chain(1721,1722).
chain(1722,1723).
chain(1723,1724).
chain(1724,1725).
chain(1725,1726).
chain(1726,1727).
chain(1727,1728).
chain(1728,1729).
chain(1729,1730).
chain(1730,1731).
chain(1731,1732).
chain(1732,1733).
chain(1733,1734).
chain(1734,1735).
chain(1735,1736).
chain(1736,1737).
chain(1737,1738).
chain(1738,1739).
chain(1739,1740).
chain(1740,1741).
chain(1741,1742).
chain(1742,1743).
chain(1743,1744).
chain(1744,1745).
chain(1745,1746).
chain(1746,1747).
chain(1747,1748).
chain(1748,1749).
chain(1749,1750).
chain(1750,1751).
chain(1751,1752).
chain(1752,1753).
chain(1753,1754).
chain(1754,1755).
chain(1755,1756).
chain(1756,1757).
chain(1757,1758).
chain(1758,1759).
chain(1759,1760).
chain(1760,1761).
chain(1761,1762).
chain(1762,1763).
chain(1763,1764).
chain(1764,1765).
chain(1765,1766).
chain(1766,1767).
chain(1767,1768).
chain(1768,1769).
chain(1769,1770).
chain(1770,1771).
chain(1771,1772).
chain(1772,1773).
chain(1773,1774).
chain(1774,1775).
chain(1775,1776).
chain(1776,1777).
chain(1777,1778).
chain(1778,1779).
chain(1779,1780).
chain(1780,1781).
chain(1781,1782).
chain(1782,1783).
chain(1783,1784).
chain(1784,1785).
chain(1785,1786).
chain(1786,1787).
chain(1787,1788).
chain(1788,1789).
chain(1789,1790).
chain(1790,1791).
chain(1791,1792).
chain(1792,1793).
chain(1793,1794).
chain(1794,1795).
chain(1795,1796).
chain(1796,1797).
chain(1797,1798).
chain(1798,1799).
chain(1799,1800).
chain(1800,1801).
chain(1801,1802).
chain(1802,1803).
chain(1803,1804).
chain(1804,1805).
chain(1805,1806).
chain(1806,1807).
chain(1807,1808).
chain(1808,1809).
chain(1809,1810).
chain(1810,1811).
chain(1811,1812).
chain(1812,1813).
chain(1813,1814).
chain(1814,1815).
chain(1815,1816).
chain(1816,1817).
chain(1817,1818).
chain(1818,1819).
chain(1819,1820).
chain(1820,1821).
chain(1821,1822).
chain(1822,1823).
chain(1823,1824).
chain(1824,1825).
chain(1825,1826).
chain(1826,1827).
chain(1827,1828).
chain(1828,1829).
chain(1829,1830).
chain(1830,1831).
chain(1831,1832).
chain(1832,1833).
chain(1833,1834).
chain(1834,1835).
chain(1835,1836).
chain(1836,1837).
chain(1837,1838).
chain(1838,1839).
chain(1839,1840).
chain(1840,1841).
chain(1841,1842).
chain(1842,1843).
chain(1843,1844).
chain(1844,1845).
chain(1845,1846).
chain(1846,1847).
chain(1847,1848).
chain(1848,1849).
chain(1849,1850).
chain(1850,1851).
chain(1851,1852).
chain(1852,1853).
chain(1853,1854).
chain(1854,1855).
chain(1855,1856).
chain(1856,1857).
chain(1857,1858).
chain(1858,1859).
chain(1859,1860).
chain(1860,1861).
chain(1861,1862).
chain(1862,1863).
chain(1863,1864).
chain(1864,1865).
chain(1865,1866).
chain(1866,1867).
chain(1867,1868).
chain(1868,1869).
chain(1869,1870).
chain(1870,1871).
chain(1871,1872).
chain(1872,1873).
chain(1873,1874).
chain(1874,1875).
chain(1875,1876).
chain(1876,1877).
chain(1877,1878).
chain(1878,1879).
chain(1879,1880).
chain(1880,1881).
chain(1881,1882).
chain(1882,1883).
chain(1883,1884).
chain(1884,1885).
chain(1885,1886).
chain(1886,1887).
chain(1887,1888).
chain(1888,1889).
chain(1889,1890).
chain(1890,1891).
chain(1891,1892).
chain(1892,1893).
chain(1893,1894).
chain(1894,1895).
chain(1895,1896).
chain(1896,1897).
chain(1897,1898).
chain(1898,1899).
chain(1899,1900).
chain(1900,1901).
chain(1901,1902).
chain(1902,1903).
chain(1903,1904).
chain(1904,1905).
chain(1905,1906).
chain(1906,1907).
chain(1907,1908).
chain(1908,1909).
chain(1909,1910).
chain(1910,1911).
chain(1911,1912).
chain(1912,1913).
chain(1913,1914).
chain(1914,1915).
chain(1915,1916).
chain(1916,1917).
chain(1917,1918).
chain(1918,1919).
chain(1919,1920).
chain(1920,1921).
chain(1921,1922).
chain(1922,1923).
chain(1923,1924).
chain(1924,1925).
chain(1925,1926).
chain(1926,1927).
chain(1927,1928).
chain(1928,1929).
chain(1929,1930).
chain(1930,1931).
chain(1931,1932).
chain(1932,1933).
chain(1933,1934).
chain(1934,1935).
chain(1935,1936).
chain(1936,1937).
chain(1937,1938).
chain(1938,1939).
chain(1939,1940).
chain(1940,1941).
chain(1941,1942).
chain(1942,1943).
chain(1943,1944).
chain(1944,1945).
chain(1945,1946).
chain(1946,1947).
chain(1947,1948).
chain(1948,1949).
chain(1949,1950).
chain(1950,1951).
chain(1951,1952).
chain(1952,1953).
chain(1953,1954).
chain(1954,1955).
chain(1955,1956).
chain(1956,1957).
chain(1957,1958).
chain(1958,1959).
chain(1959,1960).
chain(1960,1961).
chain(1961,1962).
chain(1962,1963).
chain(1963,1964).
chain(1964,1965).
chain(1965,1966).
chain(1966,1967).
chain(1967,1968).
chain(1968,1969).
chain(1969,1970).
chain(1970,1971).
chain(1971,1972).
chain(1972,1973).
chain(1973,1974).
chain(1974,1975).
chain(1975,1976).
chain(1976,1977).
chain(1977,1978).
chain(1978,1979).
chain(1979,1980).
chain(1980,1981).
chain(1981,1982).
chain(1982,1983).
chain(1983,1984).
chain(1984,1985).
chain(1985,1986).
chain(1986,1987).
chain(1987,1988).
chain(1988,1989).
chain(1989,1990).
chain(1990,1991).
chain(1991,1992).
chain(1992,1993).
chain(1993,1994).
chain(1994,1995).
chain(1995,1996).
chain(1996,1997).
chain(1997,1998).
chain(1998,1999).
chain(1999,2000).