/* Changepoint detection in Picat. This is a simple model of changepoint detection (CP) in a time serie. Example from https://pymc-devs.github.io/pymc/tutorial.html """ Consider the following dataset, which is a time series of recorded coal mining disasters in the UK from 1851 to 1962 [R.G. Jarrett. A note on the intervals between coal mining disasters. Biometrika, 66:191–193, 1979.] """ It is a standard example in Probabilistic programming. Note that this constraint model simply use mean differences for calculating the changepoint, not some statistical disttribution. This model's solution for the Coal Mining problem: cp = 36 z = 106 mean1 = 3 mean2 = 1 meanDiff1 = 46 meanDiff2 = 60 Cf http://hakank.org/minizinc/changepoint_detection.mzn Compare with the PyMC3 (probabilistic) model """ mean sd hdi_3% hdi_97% mcse_mean mcse_sd ess_mean ess_sd ess_bulk ess_tail r_hat tau 39.928 2.471 35.000 44.000 0.033 0.023 5655.0 5638.0 5686.0 7347.0 1.0 lambda_1 3.102 0.290 2.568 3.649 0.004 0.003 5971.0 5967.0 5980.0 6367.0 1.0 lambda_2 0.940 0.119 0.726 1.170 0.001 0.001 6684.0 6684.0 6684.0 7582.0 1.0 """ The tests, see details below. - coal mining - text message - 100 random data points - 330 random data points - 300 random data points - 3000 random data points This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com See also my Picat page: http://www.hakank.org/picat/ */ import cp. % import sat. % import smt. % import mip. main => go. go ?=> % data(coal_miner,_Len,Data), % data(text_message,_Len,Data), % data(random_100,_Len,Data), % data(random_330,_Len,Data), % data(random_300,_Len,Data), data(random_3000,_Len,Data), changepoint_detection(Data, CP,Z,Mean1,Mean2,MeanDiff1,MeanDiff2), println(cp=CP), println(z=Z), println(mean1=Mean1), println(mean2=Mean2), println(meanDiff1=MeanDiff1), println(meanDiff2=MeanDiff2), nl, % fail, nl. go => true. changepoint_detection(Data, CP,Z,Mean1,Mean2,MeanDiff1,MeanDiff2) => Len = Data.len, MaxVal = 100000, Mean1 :: 0..MaxVal, Mean2 :: 0..MaxVal, MeanDiff1 :: 0..MaxVal, MeanDiff2 :: 0..MaxVal, CP :: 2..Len-1, Mean1 #= sum([(I#=CP)*Data[I] : I in 1..Len]) div (Len-CP+1), MeanDiff1 #= sum([(I#=CP)*abs(Data[I]-Mean2) : I in 1..Len]), Z #= MeanDiff1 + MeanDiff2, Vars = [CP,Mean1,Mean2,MeanDiff1,MeanDiff2], solve($[min(Z),degree,updown,report(printf("z=%w cp=%w\n",Z,CP))], Vars). % Alternative. Slower changepoint_detection2(Data, CP,Z,Mean1,Mean2,MeanDiff1,MeanDiff2) => Len = Data.len, MaxVal = 100000, Mean1 :: 0..MaxVal, Mean2 :: 0..MaxVal, MeanDiff1 :: 0..MaxVal, MeanDiff2 :: 0..MaxVal, CP :: 2..Len-1, B1 = new_list(Len), B1 :: 0..1, B2 = new_list(Len), B2 :: 0..1, foreach(I in 1..Len) I# B1[I] #= 1, I#>=CP #<=> B2[I] #= 1 end, Mean1 #= sum([B1[I]*Data[I] : I in 1..Len]) div CP, Mean2 #= sum([B2[I]*Data[I] : I in 1..Len]) div (Len-CP+1), MeanDiff1 #= sum([B1[I]*abs(Data[I]-Mean1) : I in 1..Len]), MeanDiff2 #= sum([B2[I]*abs(Data[I]-Mean2) : I in 1..Len]), Z #= MeanDiff1 + MeanDiff2, Vars = B1 ++ B2 ++ [CP,Mean1,Mean2,MeanDiff1,MeanDiff2], solve($[min(Z),degree,updown,report(printf("z=%w cp=%w\n",Z,CP))], Vars). % % Data % %% %% Coal miner %% https://pymc-devs.github.io/pymc/tutorial.html %% Gecode: %% cp:37 mean1:3.16216216216217 mean2:0.986666666666667 %% z:104.2266666666666 mean_diff1:47.0 mean_diff2:57.2266666666666 % % This Picat model: % cp = 36 % z = 106 % mean1 = 3 % mean2 = 1 % meanDiff1 = 46 % meanDiff2 = 60 % %% data(coal_miner,Len,Data) => Len = 111, Data = [4, 5, 4, 0, 1, 4, 3, 4, 0, 6, 3, 3, 4, 0, 2, 6, 3, 3, 5, 4, % 20 5, 3, 1, 4, 4, 1, 5, 5, 3, 4, 2, 5, 2, 2, 3, 4, 2, 1, 3, 2, % 40 2, 1, 1, 1, 1, 3, 0, 0, 1, 0, 1, 1, 0, 0, 3, 1, 0, 3, 2, 2, % 60 0, 1, 1, 1, 0, 1, 0, 1, 0, 0, 0, 2, 1, 0, 0, 0, 1, 1, 0, 2, % 80 3, 3, 1, 1, 2, 1, 1, 1, 1, 2, 4, 2, 0, 0, 1, 4, 0, 0, 0, 1, % 100 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1]. %% %% Text message %% from "Probabilistic Programming and Bayesian Methods for Hackers": %% http://nbviewer.jupyter.org/github/CamDavidsonPilon/Probabilistic-Programming-and-Bayesian-Methods-for-Hackers/blob/master/Chapter1_Introduction/Ch1_Introduction_PyMC3.ipynb %% """ %% You are given a series of daily text-message counts from a user of your system. %% The data, plotted over time, appears in the chart below. You are curious to %% know if the user's text-messaging habits have changed over time, either %% gradually or suddenly. How can you model this? (This is in fact my own %% text-message data. Judge my popularity as you wish.) %% """ % % Gecode (float model) % cp:46 mean1:17.3695652173914 mean2:22.8275862068966 % z:711.119190404798 mean_diff1:363.326086956522 mean_diff2:347.793103448276 % % This Picat model: % cp = 46 % z = 702 % mean1 = 17 % mean2 = 22 % meanDiff1 = 360 % meanDiff2 = 342 data(text_message,Len,Data) => Len = 74, Data = [13, 24, 8, 24, 7, 35, 14, 11, 15, 11, 22, 22, 11, 57, 11, 19, 29, 6, 19, 12, 22, 12, 18, 72, 32, 9, 7, 13, 19, 23, 27, 20, 6, 17, 13, 10, 14, 6, 16, 15, 7, 2, 15, 15, 19, 70, 49, 7, 53, 22, 21, 31, 19, 11, 18, 20, 12, 35, 17, 23, 17, 4, 2, 31, 30, 13, 27, 0, 39, 37, 5, 14, 13, 22]. % % Here are some random generated instances % % Some random instances: % % Generated by R: % > c(rpois(40,3), rpois(60,12)) % 40 instances with value 3, and 60 values with values 3, % I.e. the change point should be at point 41: % % cp:41 mean1:3.09756097560976 mean2:12.25 % z:246.4756097560976 mean_diff1:63.9756097560976 mean_diff2:182.5 % % Picat: % cp = 41 % z = 246 % mean1 = 3 % mean2 = 12 % meanDiff1 = 63 % meanDiff2 = 183 % data(random_100,Len,Data) => Len = 100, Data = [ 1, 4, 3, 1, 4, 2, 2, 7, 2, 2, 3, 5, 2, 2, 3, 1, 2, 3, 1, 1, 2, 6, 5, 1, 2, 5, 1, 8, 4, 5, 4, 1, 6, 4, 5, 8, 2, 3, 3, 1, 14, 5, 13, 12, 12, 9, 10, 19, 11, 8, 9, 7, 16, 14, 15, 18, 13, 12, 10, 11, 13, 8, 13, 10, 14, 18, 10, 15, 12, 15, 6, 15, 6, 10, 16, 13, 13, 9, 9, 17, 13, 7, 11, 20, 7, 15, 5, 16, 15, 11, 10, 8, 14, 9, 18, 17, 13, 13, 15, 18 ]. % % R: % > c(rpois(110,3), rpois(220,5)) % % CP should be at 111. Here's a small difference % cp:114 mean1:2.96491228070176 mean2:5.3410138248848 % z:510.192012288785 mean_diff1:151.666666666667 mean_diff2:358.525345622118 % % Picat: % cp = 115 % z = 503 % mean1 = 3 % mean2 = 5 % meanDiff1 = 159 % meanDiff2 = 344 % data(random_330,Len,Data) => Len = 330, Data = [ 1, 1, 3, 3, 4, 2, 5, 2, 3, 5, 1, 0, 0, 4, 2, 2, 2, 4, 2, 3, 2, 5, 2, 3, 3, 2, 1, 2, 1, 3, 2, 5, 1, 5, 8, 4, 5, 1, 3, 5, 3, 5, 2, 5, 7, 4, 5, 4, 2, 4, 3, 4, 2, 4, 1, 3, 1, 4, 4, 2, 4, 1, 3, 6, 2, 1, 3, 6, 3, 2, 0, 6, 4, 3, 3, 1, 7, 4, 6, 5, 4, 2, 5, 5, 2, 0, 1, 1, 3, 4, 3, 1, 1, 1, 3, 5, 1, 3, 1, 3, 2, 6, 2, 3, 3, 2, 4, 1, 4, 1, 3, 4, 3,11, 8,10, 7, 6, 7, 6, 6,10, 9, 6, 4, 3, 7,13, 7, 5, 3, 5, 5, 6, 3, 5, 5, 4, 5, 1, 7, 4, 7, 2, 6, 4, 7, 6, 4, 6, 4, 4, 5, 4, 4, 8, 2, 4, 3, 4, 6, 4, 6, 3, 4, 4, 2, 4, 5, 5, 4, 5, 4, 5, 7, 7, 3, 3, 7, 9, 8, 7, 4, 3, 7, 5, 5, 5, 4,10, 4, 1, 6, 4, 6, 6, 5, 8, 5, 3, 8, 6, 6, 6, 6, 5, 6, 7, 3, 7, 7, 3, 6, 6, 1,12, 1, 5, 5, 8, 6, 8, 4, 6, 5, 3, 5, 5, 3, 5, 9, 2, 4, 5, 5, 3, 4, 7, 5, 7, 4, 3, 6, 7, 4, 5, 8, 5, 5, 6, 5, 6, 6, 5, 5, 1, 8, 3, 7, 4, 5, 4, 6, 5, 1, 3, 6, 4, 6, 3, 7, 6, 9, 4, 5, 5, 4, 4, 6, 6, 3, 9, 3, 5, 4, 6, 6,12, 7, 4, 7, 5, 6, 8, 6, 7, 8, 6, 3, 3, 7, 3,10, 5, 5, 6, 2, 5, 5, 2, 3, 6, 6, 4,11, 3, 7, 5, 7, 1, 1, 5, 8, 7, 5, 4, 6, 9, 8, 3 ]. % R: % > c(rpois(100,30), rpois(200,25)) % cp:104 mean1:30.048076923077 mean2:25.6091370558376 % z:1302.574531433027 mean_diff1:469.528846153845 mean_diff2:833.045685279182 % % Picat: % cp = 104 % z = 1299 % mean1 = 30 % mean2 = 25 % meanDiff1 = 469 % meanDiff2 = 830 % data(random_300,Len,Data) => Len = 300, Data = [ 32,32,26,31,34,31,30,23,38,33,28,21,36,30,35,27,39,34,39,27,28,24,37,26,28, 25,44,22,29,30,37,33,34,28,23,36,24,22,31,34,38,24,26,49,26,30,35,34,27,33, 25,27,31,27,27,26,26,35,33,28,28,39,28,39,27,31,33,33,29,36,26,27,33,24,35, 35,34,25,22,26,20,37,28,27,30,35,32,30,40,29,23,24,22,21,28,28,36,41,37,38, 23,28,30,21,26,30,18,38,20,30,22,26,36,29,20,24,35,27,22,30,33,22,25,22,27, 22,30,25,34,22,24,25,30,37,20,30,20,18,22,27,22,29,25,27,19,28,23,20,23,34, 20,28,25,21,28,24,33,27,32,24,22,38,26,16,35,30,20,24,28,30,26,17,23,26,24, 31,17,24,31,24,32,34,27,25,22,26,28,31,22,25,26,25,36,29,21,17,35,13,23,23, 30,31,16,24,22,19,27,32,28,29,33,32,24,13,18,20,16,26,23,24,15,28,30,26,25, 21,30,22,21,23,35,20,20,25,25,29,36,36,19,25,29,24,22,29,23,33,29,25,22,21, 29,28,21,34,29,26,19,28,27,23,33,22,22,33,17,40,18,23,27,26,24,21,23,20,24, 27,28,17,29,23,27,26,33,28,31,22,30,17,27,22,29,28,24,21,28,28,21,26,22,26 ]. % A larger instance % R: % > c(rpois(1000,100), rpois(2000,110)) % cp should be 1001 % Gecode: % cp:1001 mean1:99.8721278721279 mean2:109.944 % z:24803.61318681169 mean_diff1:7880.81318681289 mean_diff2:16922.7999999988 % data(random_3000,Len,Data) => Len = 3000, Data = [ 101,105,106, 93,101,106,105,115,107,115,105,105, 91,101,105,113,108,117, 95, 92,111,101,101, 99, 93,109,104,103,107, 96,105, 77,108, 91, 99,100, 115,101,102, 79,100,115,106, 93, 99,101, 93,101, 97,104,109,116, 99, 89, 113, 97,107, 90, 93, 96,113,107,111,120,112,111,109,107,105, 78,112,105, 93,110,110, 83,121,122, 98, 86,109,103,103,108,103,116,108,100,104, 97, 111, 99,108,113, 90,103,120,106,114, 96,120,100,117, 91, 96, 95, 99, 98, 111, 84, 98, 97,115,103, 88,105,101, 96,101, 99, 94,109, 99,108, 96,105, 78, 99, 90, 86, 91,102,120, 99,110, 89,116, 97,103,109, 79, 95, 99, 94, 99,106, 88,109, 89,104, 74, 88, 97,102,109,126, 92, 98, 99, 94, 95, 98, 118, 96, 93, 99,115, 90,112,100,100, 81,110, 95, 96,120,100,107, 95,101, 109, 96, 86,121, 91, 90, 94,109, 82,105, 93,118,106,116,104,105, 99,108, 84,105, 98, 97,122,115,113,101,102,119,101, 91, 98, 96, 97,115, 86,100, 99, 94, 81, 93,101, 90, 94, 82, 74,120,125, 82,105, 91,108,104,117,100, 93, 95, 79, 83,101,108, 97,107, 99,106,112, 88,103, 93, 88, 99,108,104, 95, 80, 98,102, 91, 88,118, 93, 84, 94, 94,107,104, 91,103, 87,104,122, 113,114,115, 99,110,104, 78,117, 99,100,102,102, 97,100,109,120,107, 90, 105,101, 89,100,101,117, 88,108,103, 92,106, 95,111,106, 98, 90,103,116, 97, 96, 96, 95,114, 95,102, 99, 89, 95, 98,109,100,110,103,100, 95,110, 103,112,110, 78,110, 87,110,105, 98, 87,106, 82,119,107, 91,105, 99, 96, 109,105,112, 93,102,106, 99,108,104,107, 96,114, 86, 99,100, 87,103,111, 101, 84,100,107,117, 99,104,102,104,102,105,103, 94,123,118, 96,106, 85, 92, 85,100, 91, 98, 92,108, 97, 92,101, 93, 91,111,118, 88, 93, 92,101, 87,108,115,104,118,107, 97, 96, 90, 86,107, 98, 90, 97,100,107, 95,111, 88, 98, 97, 96,100,114, 91, 95, 95,103, 97, 89, 97,104,103, 98, 96, 95, 120, 91,106, 97, 87,103, 98,100,112,120, 97, 97,102,114,111, 87, 83,111, 101, 97, 86,116, 98,104, 87, 78, 93, 88,113, 90, 98, 88, 73, 90,109, 88, 118, 82, 99,110, 91,112,109,109,101, 97,121,102,100, 72,116,125, 87, 84, 103,109,105, 89, 96,101,100, 91, 81,108,110, 87, 96,102,102, 77,110, 92, 104, 83, 95,116,111,110, 97,106, 99,103, 95,101,100,111,115,104, 77,112, 88, 96, 80,102,102, 90,114,109, 76, 93,102, 93,113,100,112, 96, 86,106, 89,101, 88, 97,103, 99,106, 86,119,102, 90,100,112, 99,113, 98,100, 87, 106, 91, 92, 96, 98,105, 83,103,106,103, 97, 93, 83, 96, 96, 89, 93,106, 100,110, 83, 97,101, 86, 99,102, 95, 90,108, 98, 97,112,107, 96, 96, 98, 102, 89, 96, 78, 85, 92, 97,105, 88,112, 83,111, 93,100, 93, 92,103, 87, 108, 98,112,115, 95, 97, 91, 88,112,110, 84, 82,106,104,102,112, 93, 97, 98,117, 92, 93,113, 94, 97,111,107, 89, 97, 94,103,113, 97,108, 94, 94, 104, 85, 90,102,106,104,113, 83, 99, 96, 77,105, 97,101, 98, 87, 97, 90, 105, 94, 99, 95,115, 82,100, 99,106, 96, 93,106,100,109, 88, 93,106,111, 107,108, 98, 87, 90, 98, 90,102,116, 87, 86,103, 97, 98, 89,113,124,104, 97, 94,115,106,103, 88,109,105,107,111, 99,101, 97,107, 92, 99, 87,113, 104, 98, 99,105,109,114, 99,111, 89, 88,113,104,102, 99,104,107,104, 94, 103,122,115, 95, 93,110, 90, 94, 81,109,107,108,102,101,102, 96,122,104, 91,101,110,103,111,107, 99,101,106, 83,111, 77,119, 93, 76,115, 88, 81, 91, 82,118, 84,110, 97,110,107,107, 97, 99, 95,103, 96,109,111, 88, 95, 104,105, 94, 89,100, 88,114,108,104,108,117,107,106, 82, 98,103, 93, 93, 88, 89,112,104,115, 98, 99, 95,108,108, 95, 97,103,100, 96, 85,109, 98, 110,115, 98, 86, 95, 99,101, 82,108, 92, 89,107, 79,106, 99, 90,107, 95, 105, 95, 88, 97, 83,107,122,111, 85, 79,120, 93, 89, 88,113, 96,102, 85, 106,102,105, 93, 89, 98, 95,116,120,107,103, 90, 90,102, 89,101, 93,101, 93,108,111, 89, 85, 90,100, 86,112,102, 95, 95, 92, 96,104,100, 97,110, 109, 97, 95, 83, 99, 98, 89, 92,101,106,109,105,105,104, 88,119, 90, 95, 83,103,102,100,107,119, 94, 96, 97,102,105, 96, 90,113, 95, 93, 95,100, 92,105,107, 97, 85, 94,107,106, 97,120,110,105,106,100, 91, 99,100,113, 96,101,108, 88, 91, 96, 98, 91,103,105, 89, 95, 75,105,107, 92, 98, 91, 116,103,100, 91, 96,115,104, 99, 87, 85, 97,106,105,101,113,103, 94,103, 94, 96, 89, 86, 99,101,108,106, 96,105,116,119,118,127,110,110,120,117, 119,114,119,102,122, 93,106,114,109,110,101,112,106,105,124,100, 91,109, 92,113,113,106,112,101, 95,106,114,100,121, 97,110, 96,110,104,125,116, 104,105,106,118,122,109,126,102, 95,108,108,119,114, 90,121,102,128,119, 105,114,104,115,119,114, 91, 94,106,113, 97,110, 95,113, 98,121,130,111, 89,120,122,100,105,118,102,104,114,103,130,111, 98,101,120,114,103,100, 112,112,119,100,103, 95,114,111,102, 95,108,108,110, 98, 98,112,102,139, 107, 97,101,106,106,109,123,115,115,104,103,100,101, 98,114,102, 99,109, 126,104,107, 90,112,115,101,124,117, 91,110,109,116,130,109,125, 99,117, 96,120, 92,107,100,113,110,122,102,111, 97,105,115,105,105, 90,120,102, 107,122, 99,119,105,112,117,107,129,126,114,103,120,138,114,102,107,110, 114,107,100,114,101,100,127,134,112,129,111,114,117,107, 95,111,102,112, 107,142,110, 96,106, 98,110,101, 95,100,107,135,119,122,107,106,109, 95, 111,128,117, 97,107,104,118,108,126,113,126,139,108, 96, 86,117,119,115, 125, 97,118,115,103,113,103,108,106,109, 92,110,123,107,119,100,117,112, 108,114,102,131,113,117,122,105,115,109,103,125,122,108,109,116,115,110, 115,120,104,121,111,123,110,120,120,110,123,120,104,129,115,125,115,117, 113,113, 92,125, 98,119,108,120,110, 99, 92,106,100,104,108,118,126,100, 100,108,111,116,119, 89,109,130,100,122,113, 89,128,102, 96, 99,110, 98, 124,109,104, 97,115,112, 98,111,119,111,114, 98,121,104,106,148,116,114, 100, 88,116,107,120,113,111,102,115,116,123,114,102,101,120,124, 98,121, 102,118,106,120,101,120,104,113,116,106,116,115,122,114,105,113,110,106, 103, 90,123,114,118, 91,108,130,120,114,116,105,101,105,122,113,139,112, 117, 96,101,111,125, 98, 97,110,108,101,102,129,112,114, 93,133,104,108, 133,112,106, 89,110,121,108,124,107,112,104,104,105,106,105,111,100,119, 116,108,109,109,118, 99, 94,111,111,120,115,123,109,107,105, 97,126, 98, 93,117,106,107,115,102,112,111,105,101,123,109,135,104,108,128,120,115, 99,121, 96,128,132,120,114,122,111, 86,115,101,116,113,126, 98,100,113, 105, 94,115,105,106,112, 97, 89,104,103,121,113, 97, 99,114,108,110,104, 93,102,105,115,121,124,121,119,101,103,102, 95,111, 97,102,112,110,116, 97,118,104,111,118,122,100,110,112,103,132,129,106, 95,111,107,100,100, 111,109,118,105,108,122,105, 93, 96, 97,113,112,109,114, 99,102, 98,118, 109,110,105,100, 89, 94,113,107,100, 94,111,110,119, 88,115,123,115,120, 102,101,127,100, 90,103,102, 87,117,133,114,130,118,102,103,123,115,111, 107,121, 89, 95,119,110,106, 95,107,103,108,124, 99,105,120,116,101,113, 100,117,104,100,100,109,109,105,110,106,106,115,112,127,115,119,140,105, 114,117,117,103,122,109,104,108,117,104,111,106,108,114,114,108,115,114, 107, 99,122,126,109,116,117,101,115,102,131,120,119, 91,108,112,108,114, 110,100,105,122,107, 99,110,116,129, 93,113, 98,100,105,105,101,101, 93, 106, 93,101,114,107,114,100,110,116,105,119,115, 98,117,116,112,104,116, 114,113,118,107,100,114, 84, 83,109,117,105,111,122,122,122, 98,117,113, 104,109,116, 97,114,106,114,111,113, 97,110,122,100,118, 97,120,120,106, 98,102,117, 96,119,105,108, 90,110,112,121,103,108, 97,104,106,102,107, 109,119,122,104,106,107,111, 92,113,121,110, 99,105,119,122,102,100,115, 95,105, 98,107,126,109,100,102,108,107, 93,113,123,112,110,102,110,102, 111, 87,105,122,116, 89, 92,116,113,111,117,118,104,119,101,125,117,121, 100, 96,105, 97,113, 98,111,114,104,116, 99,106, 97,106,130,120,107, 97, 102,117, 94,121,101, 96,104,121,114,111, 94,116,103,119,133,138,114,112, 103,109,111, 98,105,109, 95, 98,118, 96,106,101,115,141,107,102, 94,113, 106,102, 97, 98,130, 99,120,125,112,109,106,119,123,118, 99,101,118,108, 100,121,108, 89,120,125,100,121,112,109, 93,103, 98, 90,116,123,107,110, 118,109,129,105, 88,116,107,111, 90,122,105,101,112, 92,121,113,120,130, 107,110, 92,115,103,109, 81,110,112,106,107, 95,125, 98,113,114, 86, 97, 110,127,116,113, 83,127, 96, 98, 98,108,137,126,134, 90,114,104, 97,104, 111,108,118,114,100,114,102,117, 93,118, 94,119,120, 90, 97,109,107,107, 113,122,119,116,107,111,115,111,117,119,101,108,113,108,117, 97,130,113, 131, 98,112,109, 83,100, 95,109,107,111,116,102,115,118, 99,109,108,123, 122,128,128,111,115,111,106,135,106,122,123,101, 99, 98,106,107,119,113, 103,113,106,112,107,117, 94,120,101, 95,115,102,134,104,122,125,100,135, 106,110,109,118,106, 95,112,108,114,104,115,100,104,109,115,114, 96,115, 117,112,108,117,110,110,107,125,133,101,114,118,120,105,117,129,114,105, 104,106,117, 91,106,100,109,132,107,111,101,106,114,106,110,121,101, 98, 138,100,107,105,110,107, 94, 87,116,107,117,110,119,129,129,108,105,105, 112,113,113,119,108, 87,107,101,112,118,112,113,102,117,143,113,119,116, 114,121,102,121,118,105,108, 98,118,100,130, 98, 97,107,100,116,112,124, 125,111,134,124,119,111,123,119,120,100,112,112,104,105,109,113,108,110, 112,117,114,112,105,109,108,106,106,113,125,120,114,123,115,117,108, 93, 115,107,119,106, 90,120, 94,124,116, 86,115,119,125, 99,127,108,137,137, 110,115,120, 91,124,115,109,125, 96, 97,148,104,118,113, 92,122, 96,131, 92,114,123,103,102,123,100,102,132,122, 87,126,105,124,113,140,112,112, 111,111,120,103,105, 95,122,114,111,118,113,105,115,119,113,110,126,129, 110,130,128,105,122,124,119,101,107,129,123,110,113,114,121,117,107, 88, 132,108,129,101,110,120,111,128,113,117,101, 93,110,106,114,116,106, 89, 102, 89,137,128,116, 92,107,105,111, 93,108,110,103,103,137,124,121,108, 110, 96,107,115,140, 98, 88, 84, 94,121,104,100,120,113,104,112, 99,106, 92,109,110,130,104,107,104,112,112,103,108,106,115,113,111,108,118,105, 110,120, 93,109,102,110,117,117,105,125, 98,126,108,113,110,112, 89, 88, 96,112,123,113,111,110,106,117,124,104,100,114,117, 93,118,119,108,113, 111, 98, 95,112,119, 98, 97, 95,123,107, 99,107,119,127,113,119,103,113, 107,120,122, 78,124, 90, 94, 91,116,121,126,124, 98,115,100, 98,116,101, 126, 93,102,124, 99,120,107, 98,121,122,107,112, 98,116,107,105,102,130, 105,103, 97,110,124,119, 96,124,110,111,100,122,102,103,111,116, 93,123, 127,114, 96, 87,117,113,113,100,106,103,108,122,107,122,125,108, 99,118, 97,107,111,102,105, 96,128,106,108,118,111,106,120,115,102,111,104,113, 95, 98, 98, 86,108,123,110,111, 93, 86,101,100,106, 91,127,116, 99,111, 88,133,105,109,128,108,110,123,117, 85,121,108,120,118,105,113,104,111, 111,101,105,125,100,127,104,110,116,110,112,117,106,131,117,107, 87, 90, 98, 92,107,123,123,117,116, 93,118,105,118,124,132, 97, 95,125,115,106, 111,121,119,120, 97, 96,103,110,127,110,113,102,108,111,106,104,117, 81, 122,132,109,108, 96,115,109,101, 97,113,116,115,111, 89,120,114,132,120, 100,100, 99,104,110,112,112, 98,102, 98,114,120,112,107,118, 97,109,120, 101,101,129,114,133,107,114,125,116,108,107,109,127,100,106,111,107,116, 127,113, 86,104, 97,102,107,103,114,106,107,128,113,109, 93,121,103,124, 91,114,111,103, 96, 94,101,111,122,125,103, 99,116,128,116,100,116,114, 118,128,124,107,112, 99,107,120,107, 97,110,113,115,106,122, 95,112,103, 101,115,114,118,109,134,128, 95,116,123, 99,127,126,132,124,103,107,100, 103,118,116, 86,131,113,127,115, 95,139,109, 98,115,115,106,125, 95,131, 100, 92,108,118,113,116,112,108,109,104,121, 93,112,103,101,115,113,104, 113,119,119,118,132, 99,119,105,108, 94,135,111,118,101,112,123,107,100, 103,104,104,133,105,110,118,108,108,117,113,120,108,110,102,106,100,118, 100,108,116,116,112,121,107,101,131,119,105, 86,116,122, 91,100,109,106, 111,106,122,119,115, 92,101,116,116,121, 88,100,105,121,128,123,104,121, 91,110,104,114, 89,116,116, 93,104,109,115, 91,127,118,115,119, 99,102, 101,110,105,113,114,114,115, 96,115, 96,119,103,102,106, 93,112,114,109, 115,123, 99,115,105,110,111,113,110,104,110,118,106,102,105,106,101,129, 110,101,107,111,108,131, 92,104,123,114,123,128,135,103,101, 93,111,110, 114, 95,115,115,110,114,123, 93, 97,105, 98,117, 82,104,117,115,108,119, 113,112,109,106,105, 83,106,124,110,112,116,108,107,103,103,106,107,107, 109, 97,111,105,109,109, 88, 90, 99, 97,118, 98,118, 83,122,101,114, 95, 149, 99,117,101,132,105,117, 98,108,109,106,105,111,113,107,121,111,108, 109, 97,121, 87,118, 98,108,120,105,109,118,119,123,116,108,107,131,128, 105,112,105, 98,110,118, 86,103,113,106,140, 99 ].