:- source.
:- style_check(all).
:- yap_flag(unknown,error).
:- yap_flag(write_strings,on).
:- use_module(library(clpbn)).
:- set_clpbn_flag(solver, bp).
:- [-schema].

lives(_joe, nyc).

run_query(Guilty) :- 
	guilty(joe, Guilty),
	witness(nyc, t),
	runall(X, ev(X)).


runall(G, Wrapper) :-
	findall(G, Wrapper, L),
	execute_all(L).


execute_all([]).
execute_all(G.L) :-
	call(G),
	execute_all(L).


ev(descn(p2, t)).
ev(descn(p3, t)).
ev(descn(p4, t)).
ev(descn(p5, t)).
ev(descn(p6, t)).
ev(descn(p7, t)).
ev(descn(p8, t)).
ev(descn(p9, t)).
ev(descn(p10, t)).
ev(descn(p11, t)).
ev(descn(p12, t)).
ev(descn(p13, t)).
ev(descn(p14, t)).
ev(descn(p15, t)).
ev(descn(p16, t)).
ev(descn(p17, t)).
ev(descn(p18, t)).
ev(descn(p19, t)).
ev(descn(p20, t)).
ev(descn(p21, t)).
ev(descn(p22, t)).
ev(descn(p23, t)).
ev(descn(p24, t)).
ev(descn(p25, t)).
ev(descn(p26, t)).
ev(descn(p27, t)).
ev(descn(p28, t)).
ev(descn(p29, t)).
ev(descn(p30, t)).
ev(descn(p31, t)).
ev(descn(p32, t)).
ev(descn(p33, t)).
ev(descn(p34, t)).
ev(descn(p35, t)).
ev(descn(p36, t)).
ev(descn(p37, t)).
ev(descn(p38, t)).
ev(descn(p39, t)).
ev(descn(p40, t)).
ev(descn(p41, t)).
ev(descn(p42, t)).
ev(descn(p43, t)).
ev(descn(p44, t)).
ev(descn(p45, t)).
ev(descn(p46, t)).
ev(descn(p47, t)).
ev(descn(p48, t)).
ev(descn(p49, t)).
ev(descn(p50, t)).
ev(descn(p51, t)).
ev(descn(p52, t)).
ev(descn(p53, t)).
ev(descn(p54, t)).
ev(descn(p55, t)).
ev(descn(p56, t)).
ev(descn(p57, t)).
ev(descn(p58, t)).
ev(descn(p59, t)).
ev(descn(p60, t)).
ev(descn(p61, t)).
ev(descn(p62, t)).
ev(descn(p63, t)).
ev(descn(p64, t)).
ev(descn(p65, t)).
ev(descn(p66, t)).
ev(descn(p67, t)).
ev(descn(p68, t)).
ev(descn(p69, t)).
ev(descn(p70, t)).
ev(descn(p71, t)).
ev(descn(p72, t)).
ev(descn(p73, t)).
ev(descn(p74, t)).
ev(descn(p75, t)).
ev(descn(p76, t)).
ev(descn(p77, t)).
ev(descn(p78, t)).
ev(descn(p79, t)).
ev(descn(p80, t)).
ev(descn(p81, t)).
ev(descn(p82, t)).
ev(descn(p83, t)).
ev(descn(p84, t)).
ev(descn(p85, t)).
ev(descn(p86, t)).
ev(descn(p87, t)).
ev(descn(p88, t)).
ev(descn(p89, t)).
ev(descn(p90, t)).
ev(descn(p91, t)).
ev(descn(p92, t)).
ev(descn(p93, t)).
ev(descn(p94, t)).
ev(descn(p95, t)).
ev(descn(p96, t)).
ev(descn(p97, t)).
ev(descn(p98, t)).
ev(descn(p99, t)).
ev(descn(p100, t)).
ev(descn(p101, t)).
ev(descn(p102, t)).
ev(descn(p103, t)).
ev(descn(p104, t)).
ev(descn(p105, t)).
ev(descn(p106, t)).
ev(descn(p107, t)).
ev(descn(p108, t)).
ev(descn(p109, t)).
ev(descn(p110, t)).
ev(descn(p111, t)).
ev(descn(p112, t)).
ev(descn(p113, t)).
ev(descn(p114, t)).
ev(descn(p115, t)).
ev(descn(p116, t)).
ev(descn(p117, t)).
ev(descn(p118, t)).
ev(descn(p119, t)).
ev(descn(p120, t)).
ev(descn(p121, t)).
ev(descn(p122, t)).
ev(descn(p123, t)).
ev(descn(p124, t)).
ev(descn(p125, t)).
ev(descn(p126, t)).
ev(descn(p127, t)).
ev(descn(p128, t)).
ev(descn(p129, t)).
ev(descn(p130, t)).
ev(descn(p131, t)).
ev(descn(p132, t)).
ev(descn(p133, t)).
ev(descn(p134, t)).
ev(descn(p135, t)).
ev(descn(p136, t)).
ev(descn(p137, t)).
ev(descn(p138, t)).
ev(descn(p139, t)).
ev(descn(p140, t)).
ev(descn(p141, t)).
ev(descn(p142, t)).
ev(descn(p143, t)).
ev(descn(p144, t)).
ev(descn(p145, t)).
ev(descn(p146, t)).
ev(descn(p147, t)).
ev(descn(p148, t)).
ev(descn(p149, t)).
ev(descn(p150, t)).
ev(descn(p151, t)).
ev(descn(p152, t)).
ev(descn(p153, t)).
ev(descn(p154, t)).
ev(descn(p155, t)).
ev(descn(p156, t)).
ev(descn(p157, t)).
ev(descn(p158, t)).
ev(descn(p159, t)).
ev(descn(p160, t)).
ev(descn(p161, t)).
ev(descn(p162, t)).
ev(descn(p163, t)).
ev(descn(p164, t)).
ev(descn(p165, t)).
ev(descn(p166, t)).
ev(descn(p167, t)).
ev(descn(p168, t)).
ev(descn(p169, t)).
ev(descn(p170, t)).
ev(descn(p171, t)).
ev(descn(p172, t)).
ev(descn(p173, t)).
ev(descn(p174, t)).
ev(descn(p175, t)).
ev(descn(p176, t)).
ev(descn(p177, t)).
ev(descn(p178, t)).
ev(descn(p179, t)).
ev(descn(p180, t)).
ev(descn(p181, t)).
ev(descn(p182, t)).
ev(descn(p183, t)).
ev(descn(p184, t)).
ev(descn(p185, t)).
ev(descn(p186, t)).
ev(descn(p187, t)).
ev(descn(p188, t)).
ev(descn(p189, t)).
ev(descn(p190, t)).
ev(descn(p191, t)).
ev(descn(p192, t)).
ev(descn(p193, t)).
ev(descn(p194, t)).
ev(descn(p195, t)).
ev(descn(p196, t)).
ev(descn(p197, t)).
ev(descn(p198, t)).
ev(descn(p199, t)).
ev(descn(p200, t)).
ev(descn(p201, t)).
ev(descn(p202, t)).
ev(descn(p203, t)).
ev(descn(p204, t)).
ev(descn(p205, t)).
ev(descn(p206, t)).
ev(descn(p207, t)).
ev(descn(p208, t)).
ev(descn(p209, t)).
ev(descn(p210, t)).
ev(descn(p211, t)).
ev(descn(p212, t)).
ev(descn(p213, t)).
ev(descn(p214, t)).
ev(descn(p215, t)).
ev(descn(p216, t)).
ev(descn(p217, t)).
ev(descn(p218, t)).
ev(descn(p219, t)).
ev(descn(p220, t)).
ev(descn(p221, t)).
ev(descn(p222, t)).
ev(descn(p223, t)).
ev(descn(p224, t)).
ev(descn(p225, t)).
ev(descn(p226, t)).
ev(descn(p227, t)).
ev(descn(p228, t)).
ev(descn(p229, t)).
ev(descn(p230, t)).
ev(descn(p231, t)).
ev(descn(p232, t)).
ev(descn(p233, t)).
ev(descn(p234, t)).
ev(descn(p235, t)).
ev(descn(p236, t)).
ev(descn(p237, t)).
ev(descn(p238, t)).
ev(descn(p239, t)).
ev(descn(p240, t)).
ev(descn(p241, t)).
ev(descn(p242, t)).
ev(descn(p243, t)).
ev(descn(p244, t)).
ev(descn(p245, t)).
ev(descn(p246, t)).
ev(descn(p247, t)).
ev(descn(p248, t)).
ev(descn(p249, t)).
ev(descn(p250, t)).
ev(descn(p251, t)).
ev(descn(p252, t)).
ev(descn(p253, t)).
ev(descn(p254, t)).
ev(descn(p255, t)).
ev(descn(p256, t)).
ev(descn(p257, t)).
ev(descn(p258, t)).
ev(descn(p259, t)).
ev(descn(p260, t)).
ev(descn(p261, t)).
ev(descn(p262, t)).
ev(descn(p263, t)).
ev(descn(p264, t)).
ev(descn(p265, t)).
ev(descn(p266, t)).
ev(descn(p267, t)).
ev(descn(p268, t)).
ev(descn(p269, t)).
ev(descn(p270, t)).
ev(descn(p271, t)).
ev(descn(p272, t)).
ev(descn(p273, t)).
ev(descn(p274, t)).
ev(descn(p275, t)).
ev(descn(p276, t)).
ev(descn(p277, t)).
ev(descn(p278, t)).
ev(descn(p279, t)).
ev(descn(p280, t)).
ev(descn(p281, t)).
ev(descn(p282, t)).
ev(descn(p283, t)).
ev(descn(p284, t)).
ev(descn(p285, t)).
ev(descn(p286, t)).
ev(descn(p287, t)).
ev(descn(p288, t)).
ev(descn(p289, t)).
ev(descn(p290, t)).
ev(descn(p291, t)).
ev(descn(p292, t)).
ev(descn(p293, t)).
ev(descn(p294, t)).
ev(descn(p295, t)).
ev(descn(p296, t)).
ev(descn(p297, t)).
ev(descn(p298, t)).
ev(descn(p299, t)).
ev(descn(p300, t)).
ev(descn(p301, t)).
ev(descn(p302, t)).
ev(descn(p303, t)).
ev(descn(p304, t)).
ev(descn(p305, t)).
ev(descn(p306, t)).
ev(descn(p307, t)).
ev(descn(p308, t)).
ev(descn(p309, t)).
ev(descn(p310, t)).
ev(descn(p311, t)).
ev(descn(p312, t)).
ev(descn(p313, t)).
ev(descn(p314, t)).
ev(descn(p315, t)).
ev(descn(p316, t)).
ev(descn(p317, t)).
ev(descn(p318, t)).
ev(descn(p319, t)).
ev(descn(p320, t)).
ev(descn(p321, t)).
ev(descn(p322, t)).
ev(descn(p323, t)).
ev(descn(p324, t)).
ev(descn(p325, t)).
ev(descn(p326, t)).
ev(descn(p327, t)).
ev(descn(p328, t)).
ev(descn(p329, t)).
ev(descn(p330, t)).
ev(descn(p331, t)).
ev(descn(p332, t)).
ev(descn(p333, t)).
ev(descn(p334, t)).
ev(descn(p335, t)).
ev(descn(p336, t)).
ev(descn(p337, t)).
ev(descn(p338, t)).
ev(descn(p339, t)).
ev(descn(p340, t)).
ev(descn(p341, t)).
ev(descn(p342, t)).
ev(descn(p343, t)).
ev(descn(p344, t)).
ev(descn(p345, t)).
ev(descn(p346, t)).
ev(descn(p347, t)).
ev(descn(p348, t)).
ev(descn(p349, t)).
ev(descn(p350, t)).
ev(descn(p351, t)).
ev(descn(p352, t)).
ev(descn(p353, t)).
ev(descn(p354, t)).
ev(descn(p355, t)).
ev(descn(p356, t)).
ev(descn(p357, t)).
ev(descn(p358, t)).
ev(descn(p359, t)).
ev(descn(p360, t)).
ev(descn(p361, t)).
ev(descn(p362, t)).
ev(descn(p363, t)).
ev(descn(p364, t)).
ev(descn(p365, t)).
ev(descn(p366, t)).
ev(descn(p367, t)).
ev(descn(p368, t)).
ev(descn(p369, t)).
ev(descn(p370, t)).
ev(descn(p371, t)).
ev(descn(p372, t)).
ev(descn(p373, t)).
ev(descn(p374, t)).
ev(descn(p375, t)).
ev(descn(p376, t)).
ev(descn(p377, t)).
ev(descn(p378, t)).
ev(descn(p379, t)).
ev(descn(p380, t)).
ev(descn(p381, t)).
ev(descn(p382, t)).
ev(descn(p383, t)).
ev(descn(p384, t)).
ev(descn(p385, t)).
ev(descn(p386, t)).
ev(descn(p387, t)).
ev(descn(p388, t)).
ev(descn(p389, t)).
ev(descn(p390, t)).
ev(descn(p391, t)).
ev(descn(p392, t)).
ev(descn(p393, t)).
ev(descn(p394, t)).
ev(descn(p395, t)).
ev(descn(p396, t)).
ev(descn(p397, t)).
ev(descn(p398, t)).
ev(descn(p399, t)).
ev(descn(p400, t)).
ev(descn(p401, t)).
ev(descn(p402, t)).
ev(descn(p403, t)).
ev(descn(p404, t)).
ev(descn(p405, t)).
ev(descn(p406, t)).
ev(descn(p407, t)).
ev(descn(p408, t)).
ev(descn(p409, t)).
ev(descn(p410, t)).
ev(descn(p411, t)).
ev(descn(p412, t)).
ev(descn(p413, t)).
ev(descn(p414, t)).
ev(descn(p415, t)).
ev(descn(p416, t)).
ev(descn(p417, t)).
ev(descn(p418, t)).
ev(descn(p419, t)).
ev(descn(p420, t)).
ev(descn(p421, t)).
ev(descn(p422, t)).
ev(descn(p423, t)).
ev(descn(p424, t)).
ev(descn(p425, t)).
ev(descn(p426, t)).
ev(descn(p427, t)).
ev(descn(p428, t)).
ev(descn(p429, t)).
ev(descn(p430, t)).
ev(descn(p431, t)).
ev(descn(p432, t)).
ev(descn(p433, t)).
ev(descn(p434, t)).
ev(descn(p435, t)).
ev(descn(p436, t)).
ev(descn(p437, t)).
ev(descn(p438, t)).
ev(descn(p439, t)).
ev(descn(p440, t)).
ev(descn(p441, t)).
ev(descn(p442, t)).
ev(descn(p443, t)).
ev(descn(p444, t)).
ev(descn(p445, t)).
ev(descn(p446, t)).
ev(descn(p447, t)).
ev(descn(p448, t)).
ev(descn(p449, t)).
ev(descn(p450, t)).
ev(descn(p451, t)).
ev(descn(p452, t)).
ev(descn(p453, t)).
ev(descn(p454, t)).
ev(descn(p455, t)).
ev(descn(p456, t)).
ev(descn(p457, t)).
ev(descn(p458, t)).
ev(descn(p459, t)).
ev(descn(p460, t)).
ev(descn(p461, t)).
ev(descn(p462, t)).
ev(descn(p463, t)).
ev(descn(p464, t)).
ev(descn(p465, t)).
ev(descn(p466, t)).
ev(descn(p467, t)).
ev(descn(p468, t)).
ev(descn(p469, t)).
ev(descn(p470, t)).
ev(descn(p471, t)).
ev(descn(p472, t)).
ev(descn(p473, t)).
ev(descn(p474, t)).
ev(descn(p475, t)).
ev(descn(p476, t)).
ev(descn(p477, t)).
ev(descn(p478, t)).
ev(descn(p479, t)).
ev(descn(p480, t)).
ev(descn(p481, t)).
ev(descn(p482, t)).
ev(descn(p483, t)).
ev(descn(p484, t)).
ev(descn(p485, t)).
ev(descn(p486, t)).
ev(descn(p487, t)).
ev(descn(p488, t)).
ev(descn(p489, t)).
ev(descn(p490, t)).
ev(descn(p491, t)).
ev(descn(p492, t)).
ev(descn(p493, t)).
ev(descn(p494, t)).
ev(descn(p495, t)).
ev(descn(p496, t)).
ev(descn(p497, t)).
ev(descn(p498, t)).
ev(descn(p499, t)).
ev(descn(p500, t)).
ev(descn(p501, t)).
ev(descn(p502, t)).
ev(descn(p503, t)).
ev(descn(p504, t)).
ev(descn(p505, t)).
ev(descn(p506, t)).
ev(descn(p507, t)).
ev(descn(p508, t)).
ev(descn(p509, t)).
ev(descn(p510, t)).
ev(descn(p511, t)).
ev(descn(p512, t)).
ev(descn(p513, t)).
ev(descn(p514, t)).
ev(descn(p515, t)).
ev(descn(p516, t)).
ev(descn(p517, t)).
ev(descn(p518, t)).
ev(descn(p519, t)).
ev(descn(p520, t)).
ev(descn(p521, t)).
ev(descn(p522, t)).
ev(descn(p523, t)).
ev(descn(p524, t)).
ev(descn(p525, t)).
ev(descn(p526, t)).
ev(descn(p527, t)).
ev(descn(p528, t)).
ev(descn(p529, t)).
ev(descn(p530, t)).
ev(descn(p531, t)).
ev(descn(p532, t)).
ev(descn(p533, t)).
ev(descn(p534, t)).
ev(descn(p535, t)).
ev(descn(p536, t)).
ev(descn(p537, t)).
ev(descn(p538, t)).
ev(descn(p539, t)).
ev(descn(p540, t)).
ev(descn(p541, t)).
ev(descn(p542, t)).
ev(descn(p543, t)).
ev(descn(p544, t)).
ev(descn(p545, t)).
ev(descn(p546, t)).
ev(descn(p547, t)).
ev(descn(p548, t)).
ev(descn(p549, t)).
ev(descn(p550, t)).
ev(descn(p551, t)).
ev(descn(p552, t)).
ev(descn(p553, t)).
ev(descn(p554, t)).
ev(descn(p555, t)).
ev(descn(p556, t)).
ev(descn(p557, t)).
ev(descn(p558, t)).
ev(descn(p559, t)).
ev(descn(p560, t)).
ev(descn(p561, t)).
ev(descn(p562, t)).
ev(descn(p563, t)).
ev(descn(p564, t)).
ev(descn(p565, t)).
ev(descn(p566, t)).
ev(descn(p567, t)).
ev(descn(p568, t)).
ev(descn(p569, t)).
ev(descn(p570, t)).
ev(descn(p571, t)).
ev(descn(p572, t)).
ev(descn(p573, t)).
ev(descn(p574, t)).
ev(descn(p575, t)).
ev(descn(p576, t)).
ev(descn(p577, t)).
ev(descn(p578, t)).
ev(descn(p579, t)).
ev(descn(p580, t)).
ev(descn(p581, t)).
ev(descn(p582, t)).
ev(descn(p583, t)).
ev(descn(p584, t)).
ev(descn(p585, t)).
ev(descn(p586, t)).
ev(descn(p587, t)).
ev(descn(p588, t)).
ev(descn(p589, t)).
ev(descn(p590, t)).
ev(descn(p591, t)).
ev(descn(p592, t)).
ev(descn(p593, t)).
ev(descn(p594, t)).
ev(descn(p595, t)).
ev(descn(p596, t)).
ev(descn(p597, t)).
ev(descn(p598, t)).
ev(descn(p599, t)).
ev(descn(p600, t)).
ev(descn(p601, t)).
ev(descn(p602, t)).
ev(descn(p603, t)).
ev(descn(p604, t)).
ev(descn(p605, t)).
ev(descn(p606, t)).
ev(descn(p607, t)).
ev(descn(p608, t)).
ev(descn(p609, t)).
ev(descn(p610, t)).
ev(descn(p611, t)).
ev(descn(p612, t)).
ev(descn(p613, t)).
ev(descn(p614, t)).
ev(descn(p615, t)).
ev(descn(p616, t)).
ev(descn(p617, t)).
ev(descn(p618, t)).
ev(descn(p619, t)).
ev(descn(p620, t)).
ev(descn(p621, t)).
ev(descn(p622, t)).
ev(descn(p623, t)).
ev(descn(p624, t)).
ev(descn(p625, t)).
ev(descn(p626, t)).
ev(descn(p627, t)).
ev(descn(p628, t)).
ev(descn(p629, t)).
ev(descn(p630, t)).
ev(descn(p631, t)).
ev(descn(p632, t)).
ev(descn(p633, t)).
ev(descn(p634, t)).
ev(descn(p635, t)).
ev(descn(p636, t)).
ev(descn(p637, t)).
ev(descn(p638, t)).
ev(descn(p639, t)).
ev(descn(p640, t)).
ev(descn(p641, t)).
ev(descn(p642, t)).
ev(descn(p643, t)).
ev(descn(p644, t)).
ev(descn(p645, t)).
ev(descn(p646, t)).
ev(descn(p647, t)).
ev(descn(p648, t)).
ev(descn(p649, t)).
ev(descn(p650, t)).
ev(descn(p651, t)).
ev(descn(p652, t)).
ev(descn(p653, t)).
ev(descn(p654, t)).
ev(descn(p655, t)).
ev(descn(p656, t)).
ev(descn(p657, t)).
ev(descn(p658, t)).
ev(descn(p659, t)).
ev(descn(p660, t)).
ev(descn(p661, t)).
ev(descn(p662, t)).
ev(descn(p663, t)).
ev(descn(p664, t)).
ev(descn(p665, t)).
ev(descn(p666, t)).
ev(descn(p667, t)).
ev(descn(p668, t)).
ev(descn(p669, t)).
ev(descn(p670, t)).
ev(descn(p671, t)).
ev(descn(p672, t)).
ev(descn(p673, t)).
ev(descn(p674, t)).
ev(descn(p675, t)).
ev(descn(p676, t)).
ev(descn(p677, t)).
ev(descn(p678, t)).
ev(descn(p679, t)).
ev(descn(p680, t)).
ev(descn(p681, t)).
ev(descn(p682, t)).
ev(descn(p683, t)).
ev(descn(p684, t)).
ev(descn(p685, t)).
ev(descn(p686, t)).
ev(descn(p687, t)).
ev(descn(p688, t)).
ev(descn(p689, t)).
ev(descn(p690, t)).
ev(descn(p691, t)).
ev(descn(p692, t)).
ev(descn(p693, t)).
ev(descn(p694, t)).
ev(descn(p695, t)).
ev(descn(p696, t)).
ev(descn(p697, t)).
ev(descn(p698, t)).
ev(descn(p699, t)).
ev(descn(p700, t)).
ev(descn(p701, t)).
ev(descn(p702, t)).
ev(descn(p703, t)).
ev(descn(p704, t)).
ev(descn(p705, t)).
ev(descn(p706, t)).
ev(descn(p707, t)).
ev(descn(p708, t)).
ev(descn(p709, t)).
ev(descn(p710, t)).
ev(descn(p711, t)).
ev(descn(p712, t)).
ev(descn(p713, t)).
ev(descn(p714, t)).
ev(descn(p715, t)).
ev(descn(p716, t)).
ev(descn(p717, t)).
ev(descn(p718, t)).
ev(descn(p719, t)).
ev(descn(p720, t)).
ev(descn(p721, t)).
ev(descn(p722, t)).
ev(descn(p723, t)).
ev(descn(p724, t)).
ev(descn(p725, t)).
ev(descn(p726, t)).
ev(descn(p727, t)).
ev(descn(p728, t)).
ev(descn(p729, t)).
ev(descn(p730, t)).
ev(descn(p731, t)).
ev(descn(p732, t)).
ev(descn(p733, t)).
ev(descn(p734, t)).
ev(descn(p735, t)).
ev(descn(p736, t)).
ev(descn(p737, t)).
ev(descn(p738, t)).
ev(descn(p739, t)).
ev(descn(p740, t)).
ev(descn(p741, t)).
ev(descn(p742, t)).
ev(descn(p743, t)).
ev(descn(p744, t)).
ev(descn(p745, t)).
ev(descn(p746, t)).
ev(descn(p747, t)).
ev(descn(p748, t)).
ev(descn(p749, t)).
ev(descn(p750, t)).
ev(descn(p751, t)).
ev(descn(p752, t)).
ev(descn(p753, t)).
ev(descn(p754, t)).
ev(descn(p755, t)).
ev(descn(p756, t)).
ev(descn(p757, t)).
ev(descn(p758, t)).
ev(descn(p759, t)).
ev(descn(p760, t)).
ev(descn(p761, t)).
ev(descn(p762, t)).
ev(descn(p763, t)).
ev(descn(p764, t)).
ev(descn(p765, t)).
ev(descn(p766, t)).
ev(descn(p767, t)).
ev(descn(p768, t)).
ev(descn(p769, t)).
ev(descn(p770, t)).
ev(descn(p771, t)).
ev(descn(p772, t)).
ev(descn(p773, t)).
ev(descn(p774, t)).
ev(descn(p775, t)).
ev(descn(p776, t)).
ev(descn(p777, t)).
ev(descn(p778, t)).
ev(descn(p779, t)).
ev(descn(p780, t)).
ev(descn(p781, t)).
ev(descn(p782, t)).
ev(descn(p783, t)).
ev(descn(p784, t)).
ev(descn(p785, t)).
ev(descn(p786, t)).
ev(descn(p787, t)).
ev(descn(p788, t)).
ev(descn(p789, t)).
ev(descn(p790, t)).
ev(descn(p791, t)).
ev(descn(p792, t)).
ev(descn(p793, t)).
ev(descn(p794, t)).
ev(descn(p795, t)).
ev(descn(p796, t)).
ev(descn(p797, t)).
ev(descn(p798, t)).
ev(descn(p799, t)).
ev(descn(p800, t)).
ev(descn(p801, t)).
ev(descn(p802, t)).
ev(descn(p803, t)).
ev(descn(p804, t)).
ev(descn(p805, t)).
ev(descn(p806, t)).
ev(descn(p807, t)).
ev(descn(p808, t)).
ev(descn(p809, t)).
ev(descn(p810, t)).
ev(descn(p811, t)).
ev(descn(p812, t)).
ev(descn(p813, t)).
ev(descn(p814, t)).
ev(descn(p815, t)).
ev(descn(p816, t)).
ev(descn(p817, t)).
ev(descn(p818, t)).
ev(descn(p819, t)).
ev(descn(p820, t)).
ev(descn(p821, t)).
ev(descn(p822, t)).
ev(descn(p823, t)).
ev(descn(p824, t)).
ev(descn(p825, t)).
ev(descn(p826, t)).
ev(descn(p827, t)).
ev(descn(p828, t)).
ev(descn(p829, t)).
ev(descn(p830, t)).
ev(descn(p831, t)).
ev(descn(p832, t)).
ev(descn(p833, t)).
ev(descn(p834, t)).
ev(descn(p835, t)).
ev(descn(p836, t)).
ev(descn(p837, t)).
ev(descn(p838, t)).
ev(descn(p839, t)).
ev(descn(p840, t)).
ev(descn(p841, t)).
ev(descn(p842, t)).
ev(descn(p843, t)).
ev(descn(p844, t)).
ev(descn(p845, t)).
ev(descn(p846, t)).
ev(descn(p847, t)).
ev(descn(p848, t)).
ev(descn(p849, t)).
ev(descn(p850, t)).
ev(descn(p851, t)).
ev(descn(p852, t)).
ev(descn(p853, t)).
ev(descn(p854, t)).
ev(descn(p855, t)).
ev(descn(p856, t)).
ev(descn(p857, t)).
ev(descn(p858, t)).
ev(descn(p859, t)).
ev(descn(p860, t)).
ev(descn(p861, t)).
ev(descn(p862, t)).
ev(descn(p863, t)).
ev(descn(p864, t)).
ev(descn(p865, t)).
ev(descn(p866, t)).
ev(descn(p867, t)).
ev(descn(p868, t)).
ev(descn(p869, t)).
ev(descn(p870, t)).
ev(descn(p871, t)).
ev(descn(p872, t)).
ev(descn(p873, t)).
ev(descn(p874, t)).
ev(descn(p875, t)).
ev(descn(p876, t)).
ev(descn(p877, t)).
ev(descn(p878, t)).
ev(descn(p879, t)).
ev(descn(p880, t)).
ev(descn(p881, t)).
ev(descn(p882, t)).
ev(descn(p883, t)).
ev(descn(p884, t)).
ev(descn(p885, t)).
ev(descn(p886, t)).
ev(descn(p887, t)).
ev(descn(p888, t)).
ev(descn(p889, t)).
ev(descn(p890, t)).
ev(descn(p891, t)).
ev(descn(p892, t)).
ev(descn(p893, t)).
ev(descn(p894, t)).
ev(descn(p895, t)).
ev(descn(p896, t)).
ev(descn(p897, t)).
ev(descn(p898, t)).
ev(descn(p899, t)).
ev(descn(p900, t)).
ev(descn(p901, t)).
ev(descn(p902, t)).
ev(descn(p903, t)).
ev(descn(p904, t)).
ev(descn(p905, t)).
ev(descn(p906, t)).
ev(descn(p907, t)).
ev(descn(p908, t)).
ev(descn(p909, t)).
ev(descn(p910, t)).
ev(descn(p911, t)).
ev(descn(p912, t)).
ev(descn(p913, t)).
ev(descn(p914, t)).
ev(descn(p915, t)).
ev(descn(p916, t)).
ev(descn(p917, t)).
ev(descn(p918, t)).
ev(descn(p919, t)).
ev(descn(p920, t)).
ev(descn(p921, t)).
ev(descn(p922, t)).
ev(descn(p923, t)).
ev(descn(p924, t)).
ev(descn(p925, t)).
ev(descn(p926, t)).
ev(descn(p927, t)).
ev(descn(p928, t)).
ev(descn(p929, t)).
ev(descn(p930, t)).
ev(descn(p931, t)).
ev(descn(p932, t)).
ev(descn(p933, t)).
ev(descn(p934, t)).
ev(descn(p935, t)).
ev(descn(p936, t)).
ev(descn(p937, t)).
ev(descn(p938, t)).
ev(descn(p939, t)).
ev(descn(p940, t)).
ev(descn(p941, t)).
ev(descn(p942, t)).
ev(descn(p943, t)).
ev(descn(p944, t)).
ev(descn(p945, t)).
ev(descn(p946, t)).
ev(descn(p947, t)).
ev(descn(p948, t)).
ev(descn(p949, t)).
ev(descn(p950, t)).
ev(descn(p951, t)).
ev(descn(p952, t)).
ev(descn(p953, t)).
ev(descn(p954, t)).
ev(descn(p955, t)).
ev(descn(p956, t)).
ev(descn(p957, t)).
ev(descn(p958, t)).
ev(descn(p959, t)).
ev(descn(p960, t)).
ev(descn(p961, t)).
ev(descn(p962, t)).
ev(descn(p963, t)).
ev(descn(p964, t)).
ev(descn(p965, t)).
ev(descn(p966, t)).
ev(descn(p967, t)).
ev(descn(p968, t)).
ev(descn(p969, t)).
ev(descn(p970, t)).
ev(descn(p971, t)).
ev(descn(p972, t)).
ev(descn(p973, t)).
ev(descn(p974, t)).
ev(descn(p975, t)).
ev(descn(p976, t)).
ev(descn(p977, t)).
ev(descn(p978, t)).
ev(descn(p979, t)).
ev(descn(p980, t)).
ev(descn(p981, t)).
ev(descn(p982, t)).
ev(descn(p983, t)).
ev(descn(p984, t)).
ev(descn(p985, t)).
ev(descn(p986, t)).
ev(descn(p987, t)).
ev(descn(p988, t)).
ev(descn(p989, t)).
ev(descn(p990, t)).
ev(descn(p991, t)).
ev(descn(p992, t)).
ev(descn(p993, t)).
ev(descn(p994, t)).
ev(descn(p995, t)).
ev(descn(p996, t)).
ev(descn(p997, t)).
ev(descn(p998, t)).
ev(descn(p999, t)).
ev(descn(p1000, t)).