Euler Problem 67 - Maximum Path Sum II: Difference between revisions

(Created page with 'From [https://projecteuler.net/problem=67 Euler Problem 67]: By starting at the top of the triangle below and moving to adjacent numbers on the row below, the maximum total from…')
 
No edit summary
 
(10 intermediate revisions by the same user not shown)
Line 1: Line 1:
From [https://projecteuler.net/problem=67 Euler Problem 67]:
Here we give a solution to the [https://projecteuler.net/problem=67 Euler Problem 67].
The purpose is to show:
* that the encoding in B is compact and hopefully readable
* that by using ProB we get dynamic programming automatically.
 
=== The Euler Problem 67 Description ===
 
For convenience,here is the description from the official site of the  [https://projecteuler.net/problem=67 Euler Problem 67]:


By starting at the top of the triangle below and moving to adjacent numbers on the row below, the maximum total from top to bottom is 23.
By starting at the top of the triangle below and moving to adjacent numbers on the row below, the maximum total from top to bottom is 23.
Line 14: Line 21:
NOTE: This is a much more difficult version of Problem 18. It is not possible to try every route to solve this problem, as there are 299 altogether! If you could check one trillion (1012) routes every second it would take over twenty billion years to check them all. There is an efficient algorithm to solve it. ;o)
NOTE: This is a much more difficult version of Problem 18. It is not possible to try every route to solve this problem, as there are 299 altogether! If you could check one trillion (1012) routes every second it would take over twenty billion years to check them all. There is an efficient algorithm to solve it. ;o)


Solution in B, where data is held in file triangle_Euler67.def:
=== The solution in B ===
 
A solution in B is as follows, where the data for the triangle is held in the file <tt>triangle_Euler67.def</tt>:


<pre>
<pre>
Line 40: Line 49:
</pre>
</pre>


Solved on a MacBook Air 1.7 GHz using ProB 1.4.0rc2 in 2.4 seconds.
This problem was solved on a MacBook Air 1.7 GHz using ProB 1.4.0rc2 in under 2.5 seconds:
<pre>
$ probcli Euler_Problem_067.mch -init
% set_pref(TIME_OUT,time_out,5000)
% found_enumeration_of_constants(1990,2260)
% backtrack(found_enumeration_of_constants(1990,2260))
</pre>
 
You can also check the assertions using the command <tt>probcli Euler_Problem_067.mch -init -assertions</tt> in the same time:


Interesting fact: dynamic programming done automatically by ProB's constraint solving.
<pre>
Time could be improved by enforcing proper order (e.g., by putting the computation of rows into B operations and use model checking or animation to solve the problem).
$ probcliEuler_Problem_067.mch -init -assertions
% set_pref(TIME_OUT,time_out,5000)
% found_enumeration_of_constants(2060,2350)
% backtrack(found_enumeration_of_constants(2060,2350))
% Checking ASSERTIONS:
Checking Static Assertions
 
==> OptimalSolution = 7273
TRUE
TRUE  (0 ms + 0 ms = 0 ms)
 
==> n = 100
TRUE
TRUE  (0 ms + 0 ms = 0 ms)
=======
SUMMARY
=======
2 predicates: 2 TRUE, 0 FALSE, 0 UNKNOWN (0 timeouts)
0 ms to analyse
Checking Dynamic Assertions
=======
SUMMARY
=======
0 predicates: 0 TRUE, 0 FALSE, 0 UNKNOWN (0 timeouts)
0 ms to analyse
[total/2,total_after_expansion/2,true/2,true_after_expansion/2,false/0,false_after_expansion/0,unknown/0,unknown_after_expansion/0,timeout/0,runtime/0,enum_warning/0]
% Finished checking ASSERTIONS
</pre>
 
 
An interesting fact is the that [https://en.wikipedia.org/wiki/Dynamic_programming dynamic programming] is done automatically by ProB's constraint solving. In the [[Fibonacci Numbers with Automatic Dynamic Programming]] page we explain this fact on a simpler example.
 
A [http://picat-lang.org/euler/p67.pi picat solution is also available].
Compared to our solution, in the Picat solution the order of computation is directly encoded in the Picat program. Here, ProB has to infer the order of computation itself; this obviously comes at a performance price compared to a more imperative encoding of the problem.
 
The runtimes could be improved by enforcing the proper order of computation explicitly inside the model (e.g., by putting the computation of rows into B operations and use model checking or animation to solve the problem).
 
=== The data file for the Euler Problem 67 ===
Contents of the definition file <tt>triangle_Euler67.def</tt> are:
 
<pre>
DEFINITIONS
Triangle == [
[59],
[73, 41],
[52, 40, 09],
[26, 53, 06, 34],
[10, 51, 87, 86, 81],
[61, 95, 66, 57, 25, 68],
[90, 81, 80, 38, 92, 67, 73],
[30, 28, 51, 76, 81, 18, 75, 44],
[84, 14, 95, 87, 62, 81, 17, 78, 58],
[21, 46, 71, 58, 02, 79, 62, 39, 31, 09],
[56, 34, 35, 53, 78, 31, 81, 18, 90, 93, 15],
[78, 53, 04, 21, 84, 93, 32, 13, 97, 11, 37, 51],
[45, 03, 81, 79, 05, 18, 78, 86, 13, 30, 63, 99, 95],
[39, 87, 96, 28, 03, 38, 42, 17, 82, 87, 58, 07, 22, 57],
[06, 17, 51, 17, 07, 93, 09, 07, 75, 97, 95, 78, 87, 08, 53],
[67, 66, 59, 60, 88, 99, 94, 65, 55, 77, 55, 34, 27, 53, 78, 28],
[76, 40, 41, 04, 87, 16, 09, 42, 75, 69, 23, 97, 30, 60, 10, 79, 87],
[12, 10, 44, 26, 21, 36, 32, 84, 98, 60, 13, 12, 36, 16, 63, 31, 91, 35],
[70, 39, 06, 05, 55, 27, 38, 48, 28, 22, 34, 35, 62, 62, 15, 14, 94, 89, 86],
[66, 56, 68, 84, 96, 21, 34, 34, 34, 81, 62, 40, 65, 54, 62, 05, 98, 03, 02, 60],
[38, 89, 46, 37, 99, 54, 34, 53, 36, 14, 70, 26, 02, 90, 45, 13, 31, 61, 83, 73, 47],
[36, 10, 63, 96, 60, 49, 41, 05, 37, 42, 14, 58, 84, 93, 96, 17, 09, 43, 05, 43, 06, 59],
[66, 57, 87, 57, 61, 28, 37, 51, 84, 73, 79, 15, 39, 95, 88, 87, 43, 39, 11, 86, 77, 74, 18],
[54, 42, 05, 79, 30, 49, 99, 73, 46, 37, 50, 02, 45, 09, 54, 52, 27, 95, 27, 65, 19, 45, 26, 45],
[71, 39, 17, 78, 76, 29, 52, 90, 18, 99, 78, 19, 35, 62, 71, 19, 23, 65, 93, 85, 49, 33, 75, 09, 02],
[33, 24, 47, 61, 60, 55, 32, 88, 57, 55, 91, 54, 46, 57, 07, 77, 98, 52, 80, 99, 24, 25, 46, 78, 79, 05],
[92, 09, 13, 55, 10, 67, 26, 78, 76, 82, 63, 49, 51, 31, 24, 68, 05, 57, 07, 54, 69, 21, 67, 43, 17, 63, 12],
[24, 59, 06, 08, 98, 74, 66, 26, 61, 60, 13, 03, 09, 09, 24, 30, 71, 08, 88, 70, 72, 70, 29, 90, 11, 82, 41, 34],
[66, 82, 67, 04, 36, 60, 92, 77, 91, 85, 62, 49, 59, 61, 30, 90, 29, 94, 26, 41, 89, 04, 53, 22, 83, 41, 09, 74, 90],
[48, 28, 26, 37, 28, 52, 77, 26, 51, 32, 18, 98, 79, 36, 62, 13, 17, 08, 19, 54, 89, 29, 73, 68, 42, 14, 08, 16, 70, 37],
[37, 60, 69, 70, 72, 71, 09, 59, 13, 60, 38, 13, 57, 36, 09, 30, 43, 89, 30, 39, 15, 02, 44, 73, 05, 73, 26, 63, 56, 86, 12],
[55, 55, 85, 50, 62, 99, 84, 77, 28, 85, 03, 21, 27, 22, 19, 26, 82, 69, 54, 04, 13, 07, 85, 14, 01, 15, 70, 59, 89, 95, 10, 19],
[04, 09, 31, 92, 91, 38, 92, 86, 98, 75, 21, 05, 64, 42, 62, 84, 36, 20, 73, 42, 21, 23, 22, 51, 51, 79, 25, 45, 85, 53, 03, 43, 22],
[75, 63, 02, 49, 14, 12, 89, 14, 60, 78, 92, 16, 44, 82, 38, 30, 72, 11, 46, 52, 90, 27, 08, 65, 78, 03, 85, 41, 57, 79, 39, 52, 33, 48],
[78, 27, 56, 56, 39, 13, 19, 43, 86, 72, 58, 95, 39, 07, 04, 34, 21, 98, 39, 15, 39, 84, 89, 69, 84, 46, 37, 57, 59, 35, 59, 50, 26, 15, 93],
[42, 89, 36, 27, 78, 91, 24, 11, 17, 41, 05, 94, 07, 69, 51, 96, 03, 96, 47, 90, 90, 45, 91, 20, 50, 56, 10, 32, 36, 49, 04, 53, 85, 92, 25, 65],
[52, 09, 61, 30, 61, 97, 66, 21, 96, 92, 98, 90, 06, 34, 96, 60, 32, 69, 68, 33, 75, 84, 18, 31, 71, 50, 84, 63, 03, 03, 19, 11, 28, 42, 75, 45, 45],
[61, 31, 61, 68, 96, 34, 49, 39, 05, 71, 76, 59, 62, 67, 06, 47, 96, 99, 34, 21, 32, 47, 52, 07, 71, 60, 42, 72, 94, 56, 82, 83, 84, 40, 94, 87, 82, 46],
[01, 20, 60, 14, 17, 38, 26, 78, 66, 81, 45, 95, 18, 51, 98, 81, 48, 16, 53, 88, 37, 52, 69, 95, 72, 93, 22, 34, 98, 20, 54, 27, 73, 61, 56, 63, 60, 34, 63],
[93, 42, 94, 83, 47, 61, 27, 51, 79, 79, 45, 01, 44, 73, 31, 70, 83, 42, 88, 25, 53, 51, 30, 15, 65, 94, 80, 44, 61, 84, 12, 77, 02, 62, 02, 65, 94, 42, 14, 94],
[32, 73, 09, 67, 68, 29, 74, 98, 10, 19, 85, 48, 38, 31, 85, 67, 53, 93, 93, 77, 47, 67, 39, 72, 94, 53, 18, 43, 77, 40, 78, 32, 29, 59, 24, 06, 02, 83, 50, 60, 66],
[32, 01, 44, 30, 16, 51, 15, 81, 98, 15, 10, 62, 86, 79, 50, 62, 45, 60, 70, 38, 31, 85, 65, 61, 64, 06, 69, 84, 14, 22, 56, 43, 09, 48, 66, 69, 83, 91, 60, 40, 36, 61],
[92, 48, 22, 99, 15, 95, 64, 43, 01, 16, 94, 02, 99, 19, 17, 69, 11, 58, 97, 56, 89, 31, 77, 45, 67, 96, 12, 73, 08, 20, 36, 47, 81, 44, 50, 64, 68, 85, 40, 81, 85, 52, 09],
[91, 35, 92, 45, 32, 84, 62, 15, 19, 64, 21, 66, 06, 01, 52, 80, 62, 59, 12, 25, 88, 28, 91, 50, 40, 16, 22, 99, 92, 79, 87, 51, 21, 77, 74, 77, 07, 42, 38, 42, 74, 83, 02, 05],
[46, 19, 77, 66, 24, 18, 05, 32, 02, 84, 31, 99, 92, 58, 96, 72, 91, 36, 62, 99, 55, 29, 53, 42, 12, 37, 26, 58, 89, 50, 66, 19, 82, 75, 12, 48, 24, 87, 91, 85, 02, 07, 03, 76, 86],
[99, 98, 84, 93, 07, 17, 33, 61, 92, 20, 66, 60, 24, 66, 40, 30, 67, 05, 37, 29, 24, 96, 03, 27, 70, 62, 13, 04, 45, 47, 59, 88, 43, 20, 66, 15, 46, 92, 30, 04, 71, 66, 78, 70, 53, 99],
[67, 60, 38, 06, 88, 04, 17, 72, 10, 99, 71, 07, 42, 25, 54, 05, 26, 64, 91, 50, 45, 71, 06, 30, 67, 48, 69, 82, 08, 56, 80, 67, 18, 46, 66, 63, 01, 20, 08, 80, 47, 07, 91, 16, 03, 79, 87],
[18, 54, 78, 49, 80, 48, 77, 40, 68, 23, 60, 88, 58, 80, 33, 57, 11, 69, 55, 53, 64, 02, 94, 49, 60, 92, 16, 35, 81, 21, 82, 96, 25, 24, 96, 18, 02, 05, 49, 03, 50, 77, 06, 32, 84, 27, 18, 38],
[68, 01, 50, 04, 03, 21, 42, 94, 53, 24, 89, 05, 92, 26, 52, 36, 68, 11, 85, 01, 04, 42, 02, 45, 15, 06, 50, 04, 53, 73, 25, 74, 81, 88, 98, 21, 67, 84, 79, 97, 99, 20, 95, 04, 40, 46, 02, 58, 87],
[94, 10, 02, 78, 88, 52, 21, 03, 88, 60, 06, 53, 49, 71, 20, 91, 12, 65, 07, 49, 21, 22, 11, 41, 58, 99, 36, 16, 09, 48, 17, 24, 52, 36, 23, 15, 72, 16, 84, 56, 02, 99, 43, 76, 81, 71, 29, 39, 49, 17],
[64, 39, 59, 84, 86, 16, 17, 66, 03, 09, 43, 06, 64, 18, 63, 29, 68, 06, 23, 07, 87, 14, 26, 35, 17, 12, 98, 41, 53, 64, 78, 18, 98, 27, 28, 84, 80, 67, 75, 62, 10, 11, 76, 90, 54, 10, 05, 54, 41, 39, 66],
[43, 83, 18, 37, 32, 31, 52, 29, 95, 47, 08, 76, 35, 11, 04, 53, 35, 43, 34, 10, 52, 57, 12, 36, 20, 39, 40, 55, 78, 44, 07, 31, 38, 26, 08, 15, 56, 88, 86, 01, 52, 62, 10, 24, 32, 05, 60, 65, 53, 28, 57, 99],
[03, 50, 03, 52, 07, 73, 49, 92, 66, 80, 01, 46, 08, 67, 25, 36, 73, 93, 07, 42, 25, 53, 13, 96, 76, 83, 87, 90, 54, 89, 78, 22, 78, 91, 73, 51, 69, 09, 79, 94, 83, 53, 09, 40, 69, 62, 10, 79, 49, 47, 03, 81, 30],
[71, 54, 73, 33, 51, 76, 59, 54, 79, 37, 56, 45, 84, 17, 62, 21, 98, 69, 41, 95, 65, 24, 39, 37, 62, 03, 24, 48, 54, 64, 46, 82, 71, 78, 33, 67, 09, 16, 96, 68, 52, 74, 79, 68, 32, 21, 13, 78, 96, 60, 09, 69, 20, 36],
[73, 26, 21, 44, 46, 38, 17, 83, 65, 98, 07, 23, 52, 46, 61, 97, 33, 13, 60, 31, 70, 15, 36, 77, 31, 58, 56, 93, 75, 68, 21, 36, 69, 53, 90, 75, 25, 82, 39, 50, 65, 94, 29, 30, 11, 33, 11, 13, 96, 02, 56, 47, 07, 49, 02],
[76, 46, 73, 30, 10, 20, 60, 70, 14, 56, 34, 26, 37, 39, 48, 24, 55, 76, 84, 91, 39, 86, 95, 61, 50, 14, 53, 93, 64, 67, 37, 31, 10, 84, 42, 70, 48, 20, 10, 72, 60, 61, 84, 79, 69, 65, 99, 73, 89, 25, 85, 48, 92, 56, 97, 16],
[03, 14, 80, 27, 22, 30, 44, 27, 67, 75, 79, 32, 51, 54, 81, 29, 65, 14, 19, 04, 13, 82, 04, 91, 43, 40, 12, 52, 29, 99, 07, 76, 60, 25, 01, 07, 61, 71, 37, 92, 40, 47, 99, 66, 57, 01, 43, 44, 22, 40, 53, 53, 09, 69, 26, 81, 07],
[49, 80, 56, 90, 93, 87, 47, 13, 75, 28, 87, 23, 72, 79, 32, 18, 27, 20, 28, 10, 37, 59, 21, 18, 70, 04, 79, 96, 03, 31, 45, 71, 81, 06, 14, 18, 17, 05, 31, 50, 92, 79, 23, 47, 09, 39, 47, 91, 43, 54, 69, 47, 42, 95, 62, 46, 32, 85],
[37, 18, 62, 85, 87, 28, 64, 05, 77, 51, 47, 26, 30, 65, 05, 70, 65, 75, 59, 80, 42, 52, 25, 20, 44, 10, 92, 17, 71, 95, 52, 14, 77, 13, 24, 55, 11, 65, 26, 91, 01, 30, 63, 15, 49, 48, 41, 17, 67, 47, 03, 68, 20, 90, 98, 32, 04, 40, 68],
[90, 51, 58, 60, 06, 55, 23, 68, 05, 19, 76, 94, 82, 36, 96, 43, 38, 90, 87, 28, 33, 83, 05, 17, 70, 83, 96, 93, 06, 04, 78, 47, 80, 06, 23, 84, 75, 23, 87, 72, 99, 14, 50, 98, 92, 38, 90, 64, 61, 58, 76, 94, 36, 66, 87, 80, 51, 35, 61, 38],
[57, 95, 64, 06, 53, 36, 82, 51, 40, 33, 47, 14, 07, 98, 78, 65, 39, 58, 53, 06, 50, 53, 04, 69, 40, 68, 36, 69, 75, 78, 75, 60, 03, 32, 39, 24, 74, 47, 26, 90, 13, 40, 44, 71, 90, 76, 51, 24, 36, 50, 25, 45, 70, 80, 61, 80, 61, 43, 90, 64, 11],
[18, 29, 86, 56, 68, 42, 79, 10, 42, 44, 30, 12, 96, 18, 23, 18, 52, 59, 02, 99, 67, 46, 60, 86, 43, 38, 55, 17, 44, 93, 42, 21, 55, 14, 47, 34, 55, 16, 49, 24, 23, 29, 96, 51, 55, 10, 46, 53, 27, 92, 27, 46, 63, 57, 30, 65, 43, 27, 21, 20, 24, 83],
[81, 72, 93, 19, 69, 52, 48, 01, 13, 83, 92, 69, 20, 48, 69, 59, 20, 62, 05, 42, 28, 89, 90, 99, 32, 72, 84, 17, 08, 87, 36, 03, 60, 31, 36, 36, 81, 26, 97, 36, 48, 54, 56, 56, 27, 16, 91, 08, 23, 11, 87, 99, 33, 47, 02, 14, 44, 73, 70, 99, 43, 35, 33],
[90, 56, 61, 86, 56, 12, 70, 59, 63, 32, 01, 15, 81, 47, 71, 76, 95, 32, 65, 80, 54, 70, 34, 51, 40, 45, 33, 04, 64, 55, 78, 68, 88, 47, 31, 47, 68, 87, 03, 84, 23, 44, 89, 72, 35, 08, 31, 76, 63, 26, 90, 85, 96, 67, 65, 91, 19, 14, 17, 86, 04, 71, 32, 95],
[37, 13, 04, 22, 64, 37, 37, 28, 56, 62, 86, 33, 07, 37, 10, 44, 52, 82, 52, 06, 19, 52, 57, 75, 90, 26, 91, 24, 06, 21, 14, 67, 76, 30, 46, 14, 35, 89, 89, 41, 03, 64, 56, 97, 87, 63, 22, 34, 03, 79, 17, 45, 11, 53, 25, 56, 96, 61, 23, 18, 63, 31, 37, 37, 47],
[77, 23, 26, 70, 72, 76, 77, 04, 28, 64, 71, 69, 14, 85, 96, 54, 95, 48, 06, 62, 99, 83, 86, 77, 97, 75, 71, 66, 30, 19, 57, 90, 33, 01, 60, 61, 14, 12, 90, 99, 32, 77, 56, 41, 18, 14, 87, 49, 10, 14, 90, 64, 18, 50, 21, 74, 14, 16, 88, 05, 45, 73, 82, 47, 74, 44],
[22, 97, 41, 13, 34, 31, 54, 61, 56, 94, 03, 24, 59, 27, 98, 77, 04, 09, 37, 40, 12, 26, 87, 09, 71, 70, 07, 18, 64, 57, 80, 21, 12, 71, 83, 94, 60, 39, 73, 79, 73, 19, 97, 32, 64, 29, 41, 07, 48, 84, 85, 67, 12, 74, 95, 20, 24, 52, 41, 67, 56, 61, 29, 93, 35, 72, 69],
[72, 23, 63, 66, 01, 11, 07, 30, 52, 56, 95, 16, 65, 26, 83, 90, 50, 74, 60, 18, 16, 48, 43, 77, 37, 11, 99, 98, 30, 94, 91, 26, 62, 73, 45, 12, 87, 73, 47, 27, 01, 88, 66, 99, 21, 41, 95, 80, 02, 53, 23, 32, 61, 48, 32, 43, 43, 83, 14, 66, 95, 91, 19, 81, 80, 67, 25, 88],
[08, 62, 32, 18, 92, 14, 83, 71, 37, 96, 11, 83, 39, 99, 05, 16, 23, 27, 10, 67, 02, 25, 44, 11, 55, 31, 46, 64, 41, 56, 44, 74, 26, 81, 51, 31, 45, 85, 87, 09, 81, 95, 22, 28, 76, 69, 46, 48, 64, 87, 67, 76, 27, 89, 31, 11, 74, 16, 62, 03, 60, 94, 42, 47, 09, 34, 94, 93, 72],
[56, 18, 90, 18, 42, 17, 42, 32, 14, 86, 06, 53, 33, 95, 99, 35, 29, 15, 44, 20, 49, 59, 25, 54, 34, 59, 84, 21, 23, 54, 35, 90, 78, 16, 93, 13, 37, 88, 54, 19, 86, 67, 68, 55, 66, 84, 65, 42, 98, 37, 87, 56, 33, 28, 58, 38, 28, 38, 66, 27, 52, 21, 81, 15, 08, 22, 97, 32, 85, 27],
[91, 53, 40, 28, 13, 34, 91, 25, 01, 63, 50, 37, 22, 49, 71, 58, 32, 28, 30, 18, 68, 94, 23, 83, 63, 62, 94, 76, 80, 41, 90, 22, 82, 52, 29, 12, 18, 56, 10, 08, 35, 14, 37, 57, 23, 65, 67, 40, 72, 39, 93, 39, 70, 89, 40, 34, 07, 46, 94, 22, 20, 05, 53, 64, 56, 30, 05, 56, 61, 88, 27],
[23, 95, 11, 12, 37, 69, 68, 24, 66, 10, 87, 70, 43, 50, 75, 07, 62, 41, 83, 58, 95, 93, 89, 79, 45, 39, 02, 22, 05, 22, 95, 43, 62, 11, 68, 29, 17, 40, 26, 44, 25, 71, 87, 16, 70, 85, 19, 25, 59, 94, 90, 41, 41, 80, 61, 70, 55, 60, 84, 33, 95, 76, 42, 63, 15, 09, 03, 40, 38, 12, 03, 32],
[09, 84, 56, 80, 61, 55, 85, 97, 16, 94, 82, 94, 98, 57, 84, 30, 84, 48, 93, 90, 71, 05, 95, 90, 73, 17, 30, 98, 40, 64, 65, 89, 07, 79, 09, 19, 56, 36, 42, 30, 23, 69, 73, 72, 07, 05, 27, 61, 24, 31, 43, 48, 71, 84, 21, 28, 26, 65, 65, 59, 65, 74, 77, 20, 10, 81, 61, 84, 95, 08, 52, 23, 70],
[47, 81, 28, 09, 98, 51, 67, 64, 35, 51, 59, 36, 92, 82, 77, 65, 80, 24, 72, 53, 22, 07, 27, 10, 21, 28, 30, 22, 48, 82, 80, 48, 56, 20, 14, 43, 18, 25, 50, 95, 90, 31, 77, 08, 09, 48, 44, 80, 90, 22, 93, 45, 82, 17, 13, 96, 25, 26, 08, 73, 34, 99, 06, 49, 24, 06, 83, 51, 40, 14, 15, 10, 25, 01],
[54, 25, 10, 81, 30, 64, 24, 74, 75, 80, 36, 75, 82, 60, 22, 69, 72, 91, 45, 67, 03, 62, 79, 54, 89, 74, 44, 83, 64, 96, 66, 73, 44, 30, 74, 50, 37, 05, 09, 97, 70, 01, 60, 46, 37, 91, 39, 75, 75, 18, 58, 52, 72, 78, 51, 81, 86, 52, 08, 97, 01, 46, 43, 66, 98, 62, 81, 18, 70, 93, 73, 08, 32, 46, 34],
[96, 80, 82, 07, 59, 71, 92, 53, 19, 20, 88, 66, 03, 26, 26, 10, 24, 27, 50, 82, 94, 73, 63, 08, 51, 33, 22, 45, 19, 13, 58, 33, 90, 15, 22, 50, 36, 13, 55, 06, 35, 47, 82, 52, 33, 61, 36, 27, 28, 46, 98, 14, 73, 20, 73, 32, 16, 26, 80, 53, 47, 66, 76, 38, 94, 45, 02, 01, 22, 52, 47, 96, 64, 58, 52, 39],
[88, 46, 23, 39, 74, 63, 81, 64, 20, 90, 33, 33, 76, 55, 58, 26, 10, 46, 42, 26, 74, 74, 12, 83, 32, 43, 09, 02, 73, 55, 86, 54, 85, 34, 28, 23, 29, 79, 91, 62, 47, 41, 82, 87, 99, 22, 48, 90, 20, 05, 96, 75, 95, 04, 43, 28, 81, 39, 81, 01, 28, 42, 78, 25, 39, 77, 90, 57, 58, 98, 17, 36, 73, 22, 63, 74, 51],
[29, 39, 74, 94, 95, 78, 64, 24, 38, 86, 63, 87, 93, 06, 70, 92, 22, 16, 80, 64, 29, 52, 20, 27, 23, 50, 14, 13, 87, 15, 72, 96, 81, 22, 08, 49, 72, 30, 70, 24, 79, 31, 16, 64, 59, 21, 89, 34, 96, 91, 48, 76, 43, 53, 88, 01, 57, 80, 23, 81, 90, 79, 58, 01, 80, 87, 17, 99, 86, 90, 72, 63, 32, 69, 14, 28, 88, 69],
[37, 17, 71, 95, 56, 93, 71, 35, 43, 45, 04, 98, 92, 94, 84, 96, 11, 30, 31, 27, 31, 60, 92, 03, 48, 05, 98, 91, 86, 94, 35, 90, 90, 08, 48, 19, 33, 28, 68, 37, 59, 26, 65, 96, 50, 68, 22, 07, 09, 49, 34, 31, 77, 49, 43, 06, 75, 17, 81, 87, 61, 79, 52, 26, 27, 72, 29, 50, 07, 98, 86, 01, 17, 10, 46, 64, 24, 18, 56],
[51, 30, 25, 94, 88, 85, 79, 91, 40, 33, 63, 84, 49, 67, 98, 92, 15, 26, 75, 19, 82, 05, 18, 78, 65, 93, 61, 48, 91, 43, 59, 41, 70, 51, 22, 15, 92, 81, 67, 91, 46, 98, 11, 11, 65, 31, 66, 10, 98, 65, 83, 21, 05, 56, 05, 98, 73, 67, 46, 74, 69, 34, 08, 30, 05, 52, 07, 98, 32, 95, 30, 94, 65, 50, 24, 63, 28, 81, 99, 57],
[19, 23, 61, 36, 09, 89, 71, 98, 65, 17, 30, 29, 89, 26, 79, 74, 94, 11, 44, 48, 97, 54, 81, 55, 39, 66, 69, 45, 28, 47, 13, 86, 15, 76, 74, 70, 84, 32, 36, 33, 79, 20, 78, 14, 41, 47, 89, 28, 81, 05, 99, 66, 81, 86, 38, 26, 06, 25, 13, 60, 54, 55, 23, 53, 27, 05, 89, 25, 23, 11, 13, 54, 59, 54, 56, 34, 16, 24, 53, 44, 06],
[13, 40, 57, 72, 21, 15, 60, 08, 04, 19, 11, 98, 34, 45, 09, 97, 86, 71, 03, 15, 56, 19, 15, 44, 97, 31, 90, 04, 87, 87, 76, 08, 12, 30, 24, 62, 84, 28, 12, 85, 82, 53, 99, 52, 13, 94, 06, 65, 97, 86, 09, 50, 94, 68, 69, 74, 30, 67, 87, 94, 63, 07, 78, 27, 80, 36, 69, 41, 06, 92, 32, 78, 37, 82, 30, 05, 18, 87, 99, 72, 19, 99],
[44, 20, 55, 77, 69, 91, 27, 31, 28, 81, 80, 27, 02, 07, 97, 23, 95, 98, 12, 25, 75, 29, 47, 71, 07, 47, 78, 39, 41, 59, 27, 76, 13, 15, 66, 61, 68, 35, 69, 86, 16, 53, 67, 63, 99, 85, 41, 56, 08, 28, 33, 40, 94, 76, 90, 85, 31, 70, 24, 65, 84, 65, 99, 82, 19, 25, 54, 37, 21, 46, 33, 02, 52, 99, 51, 33, 26, 04, 87, 02, 08, 18, 96],
[54, 42, 61, 45, 91, 06, 64, 79, 80, 82, 32, 16, 83, 63, 42, 49, 19, 78, 65, 97, 40, 42, 14, 61, 49, 34, 04, 18, 25, 98, 59, 30, 82, 72, 26, 88, 54, 36, 21, 75, 03, 88, 99, 53, 46, 51, 55, 78, 22, 94, 34, 40, 68, 87, 84, 25, 30, 76, 25, 08, 92, 84, 42, 61, 40, 38, 09, 99, 40, 23, 29, 39, 46, 55, 10, 90, 35, 84, 56, 70, 63, 23, 91, 39],
[52, 92, 03, 71, 89, 07, 09, 37, 68, 66, 58, 20, 44, 92, 51, 56, 13, 71, 79, 99, 26, 37, 02, 06, 16, 67, 36, 52, 58, 16, 79, 73, 56, 60, 59, 27, 44, 77, 94, 82, 20, 50, 98, 33, 09, 87, 94, 37, 40, 83, 64, 83, 58, 85, 17, 76, 53, 02, 83, 52, 22, 27, 39, 20, 48, 92, 45, 21, 09, 42, 24, 23, 12, 37, 52, 28, 50, 78, 79, 20, 86, 62, 73, 20, 59],
[54, 96, 80, 15, 91, 90, 99, 70, 10, 09, 58, 90, 93, 50, 81, 99, 54, 38, 36, 10, 30, 11, 35, 84, 16, 45, 82, 18, 11, 97, 36, 43, 96, 79, 97, 65, 40, 48, 23, 19, 17, 31, 64, 52, 65, 65, 37, 32, 65, 76, 99, 79, 34, 65, 79, 27, 55, 33, 03, 01, 33, 27, 61, 28, 66, 08, 04, 70, 49, 46, 48, 83, 01, 45, 19, 96, 13, 81, 14, 21, 31, 79, 93, 85, 50, 05],
[92, 92, 48, 84, 59, 98, 31, 53, 23, 27, 15, 22, 79, 95, 24, 76, 05, 79, 16, 93, 97, 89, 38, 89, 42, 83, 02, 88, 94, 95, 82, 21, 01, 97, 48, 39, 31, 78, 09, 65, 50, 56, 97, 61, 01, 07, 65, 27, 21, 23, 14, 15, 80, 97, 44, 78, 49, 35, 33, 45, 81, 74, 34, 05, 31, 57, 09, 38, 94, 07, 69, 54, 69, 32, 65, 68, 46, 68, 78, 90, 24, 28, 49, 51, 45, 86, 35],
[41, 63, 89, 76, 87, 31, 86, 09, 46, 14, 87, 82, 22, 29, 47, 16, 13, 10, 70, 72, 82, 95, 48, 64, 58, 43, 13, 75, 42, 69, 21, 12, 67, 13, 64, 85, 58, 23, 98, 09, 37, 76, 05, 22, 31, 12, 66, 50, 29, 99, 86, 72, 45, 25, 10, 28, 19, 06, 90, 43, 29, 31, 67, 79, 46, 25, 74, 14, 97, 35, 76, 37, 65, 46, 23, 82, 06, 22, 30, 76, 93, 66, 94, 17, 96, 13, 20, 72],
[63, 40, 78, 08, 52, 09, 90, 41, 70, 28, 36, 14, 46, 44, 85, 96, 24, 52, 58, 15, 87, 37, 05, 98, 99, 39, 13, 61, 76, 38, 44, 99, 83, 74, 90, 22, 53, 80, 56, 98, 30, 51, 63, 39, 44, 30, 91, 91, 04, 22, 27, 73, 17, 35, 53, 18, 35, 45, 54, 56, 27, 78, 48, 13, 69, 36, 44, 38, 71, 25, 30, 56, 15, 22, 73, 43, 32, 69, 59, 25, 93, 83, 45, 11, 34, 94, 44, 39, 92],
[12, 36, 56, 88, 13, 96, 16, 12, 55, 54, 11, 47, 19, 78, 17, 17, 68, 81, 77, 51, 42, 55, 99, 85, 66, 27, 81, 79, 93, 42, 65, 61, 69, 74, 14, 01, 18, 56, 12, 01, 58, 37, 91, 22, 42, 66, 83, 25, 19, 04, 96, 41, 25, 45, 18, 69, 96, 88, 36, 93, 10, 12, 98, 32, 44, 83, 83, 04, 72, 91, 04, 27, 73, 07, 34, 37, 71, 60, 59, 31, 01, 54, 54, 44, 96, 93, 83, 36, 04, 45],
[30, 18, 22, 20, 42, 96, 65, 79, 17, 41, 55, 69, 94, 81, 29, 80, 91, 31, 85, 25, 47, 26, 43, 49, 02, 99, 34, 67, 99, 76, 16, 14, 15, 93, 08, 32, 99, 44, 61, 77, 67, 50, 43, 55, 87, 55, 53, 72, 17, 46, 62, 25, 50, 99, 73, 05, 93, 48, 17, 31, 70, 80, 59, 09, 44, 59, 45, 13, 74, 66, 58, 94, 87, 73, 16, 14, 85, 38, 74, 99, 64, 23, 79, 28, 71, 42, 20, 37, 82, 31, 23],
[51, 96, 39, 65, 46, 71, 56, 13, 29, 68, 53, 86, 45, 33, 51, 49, 12, 91, 21, 21, 76, 85, 02, 17, 98, 15, 46, 12, 60, 21, 88, 30, 92, 83, 44, 59, 42, 50, 27, 88, 46, 86, 94, 73, 45, 54, 23, 24, 14, 10, 94, 21, 20, 34, 23, 51, 04, 83, 99, 75, 90, 63, 60, 16, 22, 33, 83, 70, 11, 32, 10, 50, 29, 30, 83, 46, 11, 05, 31, 17, 86, 42, 49, 01, 44, 63, 28, 60, 07, 78, 95, 40],
[44, 61, 89, 59, 04, 49, 51, 27, 69, 71, 46, 76, 44, 04, 09, 34, 56, 39, 15, 06, 94, 91, 75, 90, 65, 27, 56, 23, 74, 06, 23, 33, 36, 69, 14, 39, 05, 34, 35, 57, 33, 22, 76, 46, 56, 10, 61, 65, 98, 09, 16, 69, 04, 62, 65, 18, 99, 76, 49, 18, 72, 66, 73, 83, 82, 40, 76, 31, 89, 91, 27, 88, 17, 35, 41, 35, 32, 51, 32, 67, 52, 68, 74, 85, 80, 57, 07, 11, 62, 66, 47, 22, 67],
[65, 37, 19, 97, 26, 17, 16, 24, 24, 17, 50, 37, 64, 82, 24, 36, 32, 11, 68, 34, 69, 31, 32, 89, 79, 93, 96, 68, 49, 90, 14, 23, 04, 04, 67, 99, 81, 74, 70, 74, 36, 96, 68, 09, 64, 39, 88, 35, 54, 89, 96, 58, 66, 27, 88, 97, 32, 14, 06, 35, 78, 20, 71, 06, 85, 66, 57, 02, 58, 91, 72, 05, 29, 56, 73, 48, 86, 52, 09, 93, 22, 57, 79, 42, 12, 01, 31, 68, 17, 59, 63, 76, 07, 77],
[73, 81, 14, 13, 17, 20, 11, 09, 01, 83, 08, 85, 91, 70, 84, 63, 62, 77, 37, 07, 47, 01, 59, 95, 39, 69, 39, 21, 99, 09, 87, 02, 97, 16, 92, 36, 74, 71, 90, 66, 33, 73, 73, 75, 52, 91, 11, 12, 26, 53, 05, 26, 26, 48, 61, 50, 90, 65, 01, 87, 42, 47, 74, 35, 22, 73, 24, 26, 56, 70, 52, 05, 48, 41, 31, 18, 83, 27, 21, 39, 80, 85, 26, 08, 44, 02, 71, 07, 63, 22, 05, 52, 19, 08, 20],
[17, 25, 21, 11, 72, 93, 33, 49, 64, 23, 53, 82, 03, 13, 91, 65, 85, 02, 40, 05, 42, 31, 77, 42, 05, 36, 06, 54, 04, 58, 07, 76, 87, 83, 25, 57, 66, 12, 74, 33, 85, 37, 74, 32, 20, 69, 03, 97, 91, 68, 82, 44, 19, 14, 89, 28, 85, 85, 80, 53, 34, 87, 58, 98, 88, 78, 48, 65, 98, 40, 11, 57, 10, 67, 70, 81, 60, 79, 74, 72, 97, 59, 79, 47, 30, 20, 54, 80, 89, 91, 14, 05, 33, 36, 79, 39],
[60, 85, 59, 39, 60, 07, 57, 76, 77, 92, 06, 35, 15, 72, 23, 41, 45, 52, 95, 18, 64, 79, 86, 53, 56, 31, 69, 11, 91, 31, 84, 50, 44, 82, 22, 81, 41, 40, 30, 42, 30, 91, 48, 94, 74, 76, 64, 58, 74, 25, 96, 57, 14, 19, 03, 99, 28, 83, 15, 75, 99, 01, 89, 85, 79, 50, 03, 95, 32, 67, 44, 08, 07, 41, 62, 64, 29, 20, 14, 76, 26, 55, 48, 71, 69, 66, 19, 72, 44, 25, 14, 01, 48, 74, 12, 98, 07],
[64, 66, 84, 24, 18, 16, 27, 48, 20, 14, 47, 69, 30, 86, 48, 40, 23, 16, 61, 21, 51, 50, 26, 47, 35, 33, 91, 28, 78, 64, 43, 68, 04, 79, 51, 08, 19, 60, 52, 95, 06, 68, 46, 86, 35, 97, 27, 58, 04, 65, 30, 58, 99, 12, 12, 75, 91, 39, 50, 31, 42, 64, 70, 04, 46, 07, 98, 73, 98, 93, 37, 89, 77, 91, 64, 71, 64, 65, 66, 21, 78, 62, 81, 74, 42, 20, 83, 70, 73, 95, 78, 45, 92, 27, 34, 53, 71, 15],
[30, 11, 85, 31, 34, 71, 13, 48, 05, 14, 44, 03, 19, 67, 23, 73, 19, 57, 06, 90, 94, 72, 57, 69, 81, 62, 59, 68, 88, 57, 55, 69, 49, 13, 07, 87, 97, 80, 89, 05, 71, 05, 05, 26, 38, 40, 16, 62, 45, 99, 18, 38, 98, 24, 21, 26, 62, 74, 69, 04, 85, 57, 77, 35, 58, 67, 91, 79, 79, 57, 86, 28, 66, 34, 72, 51, 76, 78, 36, 95, 63, 90, 08, 78, 47, 63, 45, 31, 22, 70, 52, 48, 79, 94, 15, 77, 61, 67, 68],
[23, 33, 44, 81, 80, 92, 93, 75, 94, 88, 23, 61, 39, 76, 22, 03, 28, 94, 32, 06, 49, 65, 41, 34, 18, 23, 08, 47, 62, 60, 03, 63, 33, 13, 80, 52, 31, 54, 73, 43, 70, 26, 16, 69, 57, 87, 83, 31, 03, 93, 70, 81, 47, 95, 77, 44, 29, 68, 39, 51, 56, 59, 63, 07, 25, 70, 07, 77, 43, 53, 64, 03, 94, 42, 95, 39, 18, 01, 66, 21, 16, 97, 20, 50, 90, 16, 70, 10, 95, 69, 29, 06, 25, 61, 41, 26, 15, 59, 63, 35]
]
</pre>

Latest revision as of 17:07, 27 January 2021

Here we give a solution to the Euler Problem 67. The purpose is to show:

  • that the encoding in B is compact and hopefully readable
  • that by using ProB we get dynamic programming automatically.

The Euler Problem 67 Description

For convenience,here is the description from the official site of the Euler Problem 67:

By starting at the top of the triangle below and moving to adjacent numbers on the row below, the maximum total from top to bottom is 23.

3
7 4
2 4 6
8 5 9 3

That is, 3 + 7 + 4 + 9 = 23.

Find the maximum total from top to bottom in triangle.txt (right click and 'Save Link/Target As...'), a 15K text file containing a triangle with one-hundred rows.

NOTE: This is a much more difficult version of Problem 18. It is not possible to try every route to solve this problem, as there are 299 altogether! If you could check one trillion (1012) routes every second it would take over twenty billion years to check them all. There is an efficient algorithm to solve it. ;o)

The solution in B

A solution in B is as follows, where the data for the triangle is held in the file triangle_Euler67.def:

MACHINE Euler_Problem_067
DEFINITIONS
 "triangle_Euler67.def";
 SET_PREF_TIME_OUT == 5000
CONSTANTS  n, Sol, OptimalSolution, TriangleC
PROPERTIES TriangleC = Triangle &
n = size (TriangleC) &

Sol : 1..n --> seq(INTEGER) &
Sol(n) = TriangleC(n) /* Initialisation */
&
! i. (i:1..(n-1) =>
  (size(Sol(i)) = size(TriangleC(i))
   & !j.(j: 1..size(TriangleC(i)) => Sol(i)(j) = TriangleC(i)(j)+max({Sol(i+1)(j),Sol(i+1)(j+1)}))
  )
  )
 & OptimalSolution = Sol(1)(1)
ASSERTIONS
 OptimalSolution = 7273;
 n = 100
END

This problem was solved on a MacBook Air 1.7 GHz using ProB 1.4.0rc2 in under 2.5 seconds:

$ probcli Euler_Problem_067.mch -init
% set_pref(TIME_OUT,time_out,5000)
% found_enumeration_of_constants(1990,2260)
% backtrack(found_enumeration_of_constants(1990,2260))

You can also check the assertions using the command probcli Euler_Problem_067.mch -init -assertions in the same time:

$ probcliEuler_Problem_067.mch -init -assertions
% set_pref(TIME_OUT,time_out,5000)
% found_enumeration_of_constants(2060,2350)
% backtrack(found_enumeration_of_constants(2060,2350))
% Checking ASSERTIONS: 
Checking Static Assertions

==> OptimalSolution = 7273
TRUE
TRUE  (0 ms + 0 ms = 0 ms)

==> n = 100
TRUE
TRUE  (0 ms + 0 ms = 0 ms)
=======
SUMMARY
=======
2 predicates: 2 TRUE, 0 FALSE, 0 UNKNOWN (0 timeouts)
0 ms to analyse
Checking Dynamic Assertions
=======
SUMMARY
=======
0 predicates: 0 TRUE, 0 FALSE, 0 UNKNOWN (0 timeouts)
0 ms to analyse
[total/2,total_after_expansion/2,true/2,true_after_expansion/2,false/0,false_after_expansion/0,unknown/0,unknown_after_expansion/0,timeout/0,runtime/0,enum_warning/0]
% Finished checking ASSERTIONS


An interesting fact is the that dynamic programming is done automatically by ProB's constraint solving. In the Fibonacci Numbers with Automatic Dynamic Programming page we explain this fact on a simpler example.

A picat solution is also available. Compared to our solution, in the Picat solution the order of computation is directly encoded in the Picat program. Here, ProB has to infer the order of computation itself; this obviously comes at a performance price compared to a more imperative encoding of the problem.

The runtimes could be improved by enforcing the proper order of computation explicitly inside the model (e.g., by putting the computation of rows into B operations and use model checking or animation to solve the problem).

The data file for the Euler Problem 67

Contents of the definition file triangle_Euler67.def are:

DEFINITIONS
Triangle == [
[59],
[73, 41],
[52, 40, 09],
[26, 53, 06, 34],
[10, 51, 87, 86, 81],
[61, 95, 66, 57, 25, 68],
[90, 81, 80, 38, 92, 67, 73],
[30, 28, 51, 76, 81, 18, 75, 44],
[84, 14, 95, 87, 62, 81, 17, 78, 58],
[21, 46, 71, 58, 02, 79, 62, 39, 31, 09],
[56, 34, 35, 53, 78, 31, 81, 18, 90, 93, 15],
[78, 53, 04, 21, 84, 93, 32, 13, 97, 11, 37, 51],
[45, 03, 81, 79, 05, 18, 78, 86, 13, 30, 63, 99, 95],
[39, 87, 96, 28, 03, 38, 42, 17, 82, 87, 58, 07, 22, 57],
[06, 17, 51, 17, 07, 93, 09, 07, 75, 97, 95, 78, 87, 08, 53],
[67, 66, 59, 60, 88, 99, 94, 65, 55, 77, 55, 34, 27, 53, 78, 28],
[76, 40, 41, 04, 87, 16, 09, 42, 75, 69, 23, 97, 30, 60, 10, 79, 87],
[12, 10, 44, 26, 21, 36, 32, 84, 98, 60, 13, 12, 36, 16, 63, 31, 91, 35],
[70, 39, 06, 05, 55, 27, 38, 48, 28, 22, 34, 35, 62, 62, 15, 14, 94, 89, 86],
[66, 56, 68, 84, 96, 21, 34, 34, 34, 81, 62, 40, 65, 54, 62, 05, 98, 03, 02, 60],
[38, 89, 46, 37, 99, 54, 34, 53, 36, 14, 70, 26, 02, 90, 45, 13, 31, 61, 83, 73, 47],
[36, 10, 63, 96, 60, 49, 41, 05, 37, 42, 14, 58, 84, 93, 96, 17, 09, 43, 05, 43, 06, 59],
[66, 57, 87, 57, 61, 28, 37, 51, 84, 73, 79, 15, 39, 95, 88, 87, 43, 39, 11, 86, 77, 74, 18],
[54, 42, 05, 79, 30, 49, 99, 73, 46, 37, 50, 02, 45, 09, 54, 52, 27, 95, 27, 65, 19, 45, 26, 45],
[71, 39, 17, 78, 76, 29, 52, 90, 18, 99, 78, 19, 35, 62, 71, 19, 23, 65, 93, 85, 49, 33, 75, 09, 02],
[33, 24, 47, 61, 60, 55, 32, 88, 57, 55, 91, 54, 46, 57, 07, 77, 98, 52, 80, 99, 24, 25, 46, 78, 79, 05],
[92, 09, 13, 55, 10, 67, 26, 78, 76, 82, 63, 49, 51, 31, 24, 68, 05, 57, 07, 54, 69, 21, 67, 43, 17, 63, 12],
[24, 59, 06, 08, 98, 74, 66, 26, 61, 60, 13, 03, 09, 09, 24, 30, 71, 08, 88, 70, 72, 70, 29, 90, 11, 82, 41, 34],
[66, 82, 67, 04, 36, 60, 92, 77, 91, 85, 62, 49, 59, 61, 30, 90, 29, 94, 26, 41, 89, 04, 53, 22, 83, 41, 09, 74, 90],
[48, 28, 26, 37, 28, 52, 77, 26, 51, 32, 18, 98, 79, 36, 62, 13, 17, 08, 19, 54, 89, 29, 73, 68, 42, 14, 08, 16, 70, 37],
[37, 60, 69, 70, 72, 71, 09, 59, 13, 60, 38, 13, 57, 36, 09, 30, 43, 89, 30, 39, 15, 02, 44, 73, 05, 73, 26, 63, 56, 86, 12],
[55, 55, 85, 50, 62, 99, 84, 77, 28, 85, 03, 21, 27, 22, 19, 26, 82, 69, 54, 04, 13, 07, 85, 14, 01, 15, 70, 59, 89, 95, 10, 19],
[04, 09, 31, 92, 91, 38, 92, 86, 98, 75, 21, 05, 64, 42, 62, 84, 36, 20, 73, 42, 21, 23, 22, 51, 51, 79, 25, 45, 85, 53, 03, 43, 22],
[75, 63, 02, 49, 14, 12, 89, 14, 60, 78, 92, 16, 44, 82, 38, 30, 72, 11, 46, 52, 90, 27, 08, 65, 78, 03, 85, 41, 57, 79, 39, 52, 33, 48],
[78, 27, 56, 56, 39, 13, 19, 43, 86, 72, 58, 95, 39, 07, 04, 34, 21, 98, 39, 15, 39, 84, 89, 69, 84, 46, 37, 57, 59, 35, 59, 50, 26, 15, 93],
[42, 89, 36, 27, 78, 91, 24, 11, 17, 41, 05, 94, 07, 69, 51, 96, 03, 96, 47, 90, 90, 45, 91, 20, 50, 56, 10, 32, 36, 49, 04, 53, 85, 92, 25, 65],
[52, 09, 61, 30, 61, 97, 66, 21, 96, 92, 98, 90, 06, 34, 96, 60, 32, 69, 68, 33, 75, 84, 18, 31, 71, 50, 84, 63, 03, 03, 19, 11, 28, 42, 75, 45, 45],
[61, 31, 61, 68, 96, 34, 49, 39, 05, 71, 76, 59, 62, 67, 06, 47, 96, 99, 34, 21, 32, 47, 52, 07, 71, 60, 42, 72, 94, 56, 82, 83, 84, 40, 94, 87, 82, 46],
[01, 20, 60, 14, 17, 38, 26, 78, 66, 81, 45, 95, 18, 51, 98, 81, 48, 16, 53, 88, 37, 52, 69, 95, 72, 93, 22, 34, 98, 20, 54, 27, 73, 61, 56, 63, 60, 34, 63],
[93, 42, 94, 83, 47, 61, 27, 51, 79, 79, 45, 01, 44, 73, 31, 70, 83, 42, 88, 25, 53, 51, 30, 15, 65, 94, 80, 44, 61, 84, 12, 77, 02, 62, 02, 65, 94, 42, 14, 94],
[32, 73, 09, 67, 68, 29, 74, 98, 10, 19, 85, 48, 38, 31, 85, 67, 53, 93, 93, 77, 47, 67, 39, 72, 94, 53, 18, 43, 77, 40, 78, 32, 29, 59, 24, 06, 02, 83, 50, 60, 66],
[32, 01, 44, 30, 16, 51, 15, 81, 98, 15, 10, 62, 86, 79, 50, 62, 45, 60, 70, 38, 31, 85, 65, 61, 64, 06, 69, 84, 14, 22, 56, 43, 09, 48, 66, 69, 83, 91, 60, 40, 36, 61],
[92, 48, 22, 99, 15, 95, 64, 43, 01, 16, 94, 02, 99, 19, 17, 69, 11, 58, 97, 56, 89, 31, 77, 45, 67, 96, 12, 73, 08, 20, 36, 47, 81, 44, 50, 64, 68, 85, 40, 81, 85, 52, 09],
[91, 35, 92, 45, 32, 84, 62, 15, 19, 64, 21, 66, 06, 01, 52, 80, 62, 59, 12, 25, 88, 28, 91, 50, 40, 16, 22, 99, 92, 79, 87, 51, 21, 77, 74, 77, 07, 42, 38, 42, 74, 83, 02, 05],
[46, 19, 77, 66, 24, 18, 05, 32, 02, 84, 31, 99, 92, 58, 96, 72, 91, 36, 62, 99, 55, 29, 53, 42, 12, 37, 26, 58, 89, 50, 66, 19, 82, 75, 12, 48, 24, 87, 91, 85, 02, 07, 03, 76, 86],
[99, 98, 84, 93, 07, 17, 33, 61, 92, 20, 66, 60, 24, 66, 40, 30, 67, 05, 37, 29, 24, 96, 03, 27, 70, 62, 13, 04, 45, 47, 59, 88, 43, 20, 66, 15, 46, 92, 30, 04, 71, 66, 78, 70, 53, 99],
[67, 60, 38, 06, 88, 04, 17, 72, 10, 99, 71, 07, 42, 25, 54, 05, 26, 64, 91, 50, 45, 71, 06, 30, 67, 48, 69, 82, 08, 56, 80, 67, 18, 46, 66, 63, 01, 20, 08, 80, 47, 07, 91, 16, 03, 79, 87],
[18, 54, 78, 49, 80, 48, 77, 40, 68, 23, 60, 88, 58, 80, 33, 57, 11, 69, 55, 53, 64, 02, 94, 49, 60, 92, 16, 35, 81, 21, 82, 96, 25, 24, 96, 18, 02, 05, 49, 03, 50, 77, 06, 32, 84, 27, 18, 38],
[68, 01, 50, 04, 03, 21, 42, 94, 53, 24, 89, 05, 92, 26, 52, 36, 68, 11, 85, 01, 04, 42, 02, 45, 15, 06, 50, 04, 53, 73, 25, 74, 81, 88, 98, 21, 67, 84, 79, 97, 99, 20, 95, 04, 40, 46, 02, 58, 87],
[94, 10, 02, 78, 88, 52, 21, 03, 88, 60, 06, 53, 49, 71, 20, 91, 12, 65, 07, 49, 21, 22, 11, 41, 58, 99, 36, 16, 09, 48, 17, 24, 52, 36, 23, 15, 72, 16, 84, 56, 02, 99, 43, 76, 81, 71, 29, 39, 49, 17],
[64, 39, 59, 84, 86, 16, 17, 66, 03, 09, 43, 06, 64, 18, 63, 29, 68, 06, 23, 07, 87, 14, 26, 35, 17, 12, 98, 41, 53, 64, 78, 18, 98, 27, 28, 84, 80, 67, 75, 62, 10, 11, 76, 90, 54, 10, 05, 54, 41, 39, 66],
[43, 83, 18, 37, 32, 31, 52, 29, 95, 47, 08, 76, 35, 11, 04, 53, 35, 43, 34, 10, 52, 57, 12, 36, 20, 39, 40, 55, 78, 44, 07, 31, 38, 26, 08, 15, 56, 88, 86, 01, 52, 62, 10, 24, 32, 05, 60, 65, 53, 28, 57, 99],
[03, 50, 03, 52, 07, 73, 49, 92, 66, 80, 01, 46, 08, 67, 25, 36, 73, 93, 07, 42, 25, 53, 13, 96, 76, 83, 87, 90, 54, 89, 78, 22, 78, 91, 73, 51, 69, 09, 79, 94, 83, 53, 09, 40, 69, 62, 10, 79, 49, 47, 03, 81, 30],
[71, 54, 73, 33, 51, 76, 59, 54, 79, 37, 56, 45, 84, 17, 62, 21, 98, 69, 41, 95, 65, 24, 39, 37, 62, 03, 24, 48, 54, 64, 46, 82, 71, 78, 33, 67, 09, 16, 96, 68, 52, 74, 79, 68, 32, 21, 13, 78, 96, 60, 09, 69, 20, 36],
[73, 26, 21, 44, 46, 38, 17, 83, 65, 98, 07, 23, 52, 46, 61, 97, 33, 13, 60, 31, 70, 15, 36, 77, 31, 58, 56, 93, 75, 68, 21, 36, 69, 53, 90, 75, 25, 82, 39, 50, 65, 94, 29, 30, 11, 33, 11, 13, 96, 02, 56, 47, 07, 49, 02],
[76, 46, 73, 30, 10, 20, 60, 70, 14, 56, 34, 26, 37, 39, 48, 24, 55, 76, 84, 91, 39, 86, 95, 61, 50, 14, 53, 93, 64, 67, 37, 31, 10, 84, 42, 70, 48, 20, 10, 72, 60, 61, 84, 79, 69, 65, 99, 73, 89, 25, 85, 48, 92, 56, 97, 16],
[03, 14, 80, 27, 22, 30, 44, 27, 67, 75, 79, 32, 51, 54, 81, 29, 65, 14, 19, 04, 13, 82, 04, 91, 43, 40, 12, 52, 29, 99, 07, 76, 60, 25, 01, 07, 61, 71, 37, 92, 40, 47, 99, 66, 57, 01, 43, 44, 22, 40, 53, 53, 09, 69, 26, 81, 07],
[49, 80, 56, 90, 93, 87, 47, 13, 75, 28, 87, 23, 72, 79, 32, 18, 27, 20, 28, 10, 37, 59, 21, 18, 70, 04, 79, 96, 03, 31, 45, 71, 81, 06, 14, 18, 17, 05, 31, 50, 92, 79, 23, 47, 09, 39, 47, 91, 43, 54, 69, 47, 42, 95, 62, 46, 32, 85],
[37, 18, 62, 85, 87, 28, 64, 05, 77, 51, 47, 26, 30, 65, 05, 70, 65, 75, 59, 80, 42, 52, 25, 20, 44, 10, 92, 17, 71, 95, 52, 14, 77, 13, 24, 55, 11, 65, 26, 91, 01, 30, 63, 15, 49, 48, 41, 17, 67, 47, 03, 68, 20, 90, 98, 32, 04, 40, 68],
[90, 51, 58, 60, 06, 55, 23, 68, 05, 19, 76, 94, 82, 36, 96, 43, 38, 90, 87, 28, 33, 83, 05, 17, 70, 83, 96, 93, 06, 04, 78, 47, 80, 06, 23, 84, 75, 23, 87, 72, 99, 14, 50, 98, 92, 38, 90, 64, 61, 58, 76, 94, 36, 66, 87, 80, 51, 35, 61, 38],
[57, 95, 64, 06, 53, 36, 82, 51, 40, 33, 47, 14, 07, 98, 78, 65, 39, 58, 53, 06, 50, 53, 04, 69, 40, 68, 36, 69, 75, 78, 75, 60, 03, 32, 39, 24, 74, 47, 26, 90, 13, 40, 44, 71, 90, 76, 51, 24, 36, 50, 25, 45, 70, 80, 61, 80, 61, 43, 90, 64, 11],
[18, 29, 86, 56, 68, 42, 79, 10, 42, 44, 30, 12, 96, 18, 23, 18, 52, 59, 02, 99, 67, 46, 60, 86, 43, 38, 55, 17, 44, 93, 42, 21, 55, 14, 47, 34, 55, 16, 49, 24, 23, 29, 96, 51, 55, 10, 46, 53, 27, 92, 27, 46, 63, 57, 30, 65, 43, 27, 21, 20, 24, 83],
[81, 72, 93, 19, 69, 52, 48, 01, 13, 83, 92, 69, 20, 48, 69, 59, 20, 62, 05, 42, 28, 89, 90, 99, 32, 72, 84, 17, 08, 87, 36, 03, 60, 31, 36, 36, 81, 26, 97, 36, 48, 54, 56, 56, 27, 16, 91, 08, 23, 11, 87, 99, 33, 47, 02, 14, 44, 73, 70, 99, 43, 35, 33],
[90, 56, 61, 86, 56, 12, 70, 59, 63, 32, 01, 15, 81, 47, 71, 76, 95, 32, 65, 80, 54, 70, 34, 51, 40, 45, 33, 04, 64, 55, 78, 68, 88, 47, 31, 47, 68, 87, 03, 84, 23, 44, 89, 72, 35, 08, 31, 76, 63, 26, 90, 85, 96, 67, 65, 91, 19, 14, 17, 86, 04, 71, 32, 95],
[37, 13, 04, 22, 64, 37, 37, 28, 56, 62, 86, 33, 07, 37, 10, 44, 52, 82, 52, 06, 19, 52, 57, 75, 90, 26, 91, 24, 06, 21, 14, 67, 76, 30, 46, 14, 35, 89, 89, 41, 03, 64, 56, 97, 87, 63, 22, 34, 03, 79, 17, 45, 11, 53, 25, 56, 96, 61, 23, 18, 63, 31, 37, 37, 47],
[77, 23, 26, 70, 72, 76, 77, 04, 28, 64, 71, 69, 14, 85, 96, 54, 95, 48, 06, 62, 99, 83, 86, 77, 97, 75, 71, 66, 30, 19, 57, 90, 33, 01, 60, 61, 14, 12, 90, 99, 32, 77, 56, 41, 18, 14, 87, 49, 10, 14, 90, 64, 18, 50, 21, 74, 14, 16, 88, 05, 45, 73, 82, 47, 74, 44],
[22, 97, 41, 13, 34, 31, 54, 61, 56, 94, 03, 24, 59, 27, 98, 77, 04, 09, 37, 40, 12, 26, 87, 09, 71, 70, 07, 18, 64, 57, 80, 21, 12, 71, 83, 94, 60, 39, 73, 79, 73, 19, 97, 32, 64, 29, 41, 07, 48, 84, 85, 67, 12, 74, 95, 20, 24, 52, 41, 67, 56, 61, 29, 93, 35, 72, 69],
[72, 23, 63, 66, 01, 11, 07, 30, 52, 56, 95, 16, 65, 26, 83, 90, 50, 74, 60, 18, 16, 48, 43, 77, 37, 11, 99, 98, 30, 94, 91, 26, 62, 73, 45, 12, 87, 73, 47, 27, 01, 88, 66, 99, 21, 41, 95, 80, 02, 53, 23, 32, 61, 48, 32, 43, 43, 83, 14, 66, 95, 91, 19, 81, 80, 67, 25, 88],
[08, 62, 32, 18, 92, 14, 83, 71, 37, 96, 11, 83, 39, 99, 05, 16, 23, 27, 10, 67, 02, 25, 44, 11, 55, 31, 46, 64, 41, 56, 44, 74, 26, 81, 51, 31, 45, 85, 87, 09, 81, 95, 22, 28, 76, 69, 46, 48, 64, 87, 67, 76, 27, 89, 31, 11, 74, 16, 62, 03, 60, 94, 42, 47, 09, 34, 94, 93, 72],
[56, 18, 90, 18, 42, 17, 42, 32, 14, 86, 06, 53, 33, 95, 99, 35, 29, 15, 44, 20, 49, 59, 25, 54, 34, 59, 84, 21, 23, 54, 35, 90, 78, 16, 93, 13, 37, 88, 54, 19, 86, 67, 68, 55, 66, 84, 65, 42, 98, 37, 87, 56, 33, 28, 58, 38, 28, 38, 66, 27, 52, 21, 81, 15, 08, 22, 97, 32, 85, 27],
[91, 53, 40, 28, 13, 34, 91, 25, 01, 63, 50, 37, 22, 49, 71, 58, 32, 28, 30, 18, 68, 94, 23, 83, 63, 62, 94, 76, 80, 41, 90, 22, 82, 52, 29, 12, 18, 56, 10, 08, 35, 14, 37, 57, 23, 65, 67, 40, 72, 39, 93, 39, 70, 89, 40, 34, 07, 46, 94, 22, 20, 05, 53, 64, 56, 30, 05, 56, 61, 88, 27],
[23, 95, 11, 12, 37, 69, 68, 24, 66, 10, 87, 70, 43, 50, 75, 07, 62, 41, 83, 58, 95, 93, 89, 79, 45, 39, 02, 22, 05, 22, 95, 43, 62, 11, 68, 29, 17, 40, 26, 44, 25, 71, 87, 16, 70, 85, 19, 25, 59, 94, 90, 41, 41, 80, 61, 70, 55, 60, 84, 33, 95, 76, 42, 63, 15, 09, 03, 40, 38, 12, 03, 32],
[09, 84, 56, 80, 61, 55, 85, 97, 16, 94, 82, 94, 98, 57, 84, 30, 84, 48, 93, 90, 71, 05, 95, 90, 73, 17, 30, 98, 40, 64, 65, 89, 07, 79, 09, 19, 56, 36, 42, 30, 23, 69, 73, 72, 07, 05, 27, 61, 24, 31, 43, 48, 71, 84, 21, 28, 26, 65, 65, 59, 65, 74, 77, 20, 10, 81, 61, 84, 95, 08, 52, 23, 70],
[47, 81, 28, 09, 98, 51, 67, 64, 35, 51, 59, 36, 92, 82, 77, 65, 80, 24, 72, 53, 22, 07, 27, 10, 21, 28, 30, 22, 48, 82, 80, 48, 56, 20, 14, 43, 18, 25, 50, 95, 90, 31, 77, 08, 09, 48, 44, 80, 90, 22, 93, 45, 82, 17, 13, 96, 25, 26, 08, 73, 34, 99, 06, 49, 24, 06, 83, 51, 40, 14, 15, 10, 25, 01],
[54, 25, 10, 81, 30, 64, 24, 74, 75, 80, 36, 75, 82, 60, 22, 69, 72, 91, 45, 67, 03, 62, 79, 54, 89, 74, 44, 83, 64, 96, 66, 73, 44, 30, 74, 50, 37, 05, 09, 97, 70, 01, 60, 46, 37, 91, 39, 75, 75, 18, 58, 52, 72, 78, 51, 81, 86, 52, 08, 97, 01, 46, 43, 66, 98, 62, 81, 18, 70, 93, 73, 08, 32, 46, 34],
[96, 80, 82, 07, 59, 71, 92, 53, 19, 20, 88, 66, 03, 26, 26, 10, 24, 27, 50, 82, 94, 73, 63, 08, 51, 33, 22, 45, 19, 13, 58, 33, 90, 15, 22, 50, 36, 13, 55, 06, 35, 47, 82, 52, 33, 61, 36, 27, 28, 46, 98, 14, 73, 20, 73, 32, 16, 26, 80, 53, 47, 66, 76, 38, 94, 45, 02, 01, 22, 52, 47, 96, 64, 58, 52, 39],
[88, 46, 23, 39, 74, 63, 81, 64, 20, 90, 33, 33, 76, 55, 58, 26, 10, 46, 42, 26, 74, 74, 12, 83, 32, 43, 09, 02, 73, 55, 86, 54, 85, 34, 28, 23, 29, 79, 91, 62, 47, 41, 82, 87, 99, 22, 48, 90, 20, 05, 96, 75, 95, 04, 43, 28, 81, 39, 81, 01, 28, 42, 78, 25, 39, 77, 90, 57, 58, 98, 17, 36, 73, 22, 63, 74, 51],
[29, 39, 74, 94, 95, 78, 64, 24, 38, 86, 63, 87, 93, 06, 70, 92, 22, 16, 80, 64, 29, 52, 20, 27, 23, 50, 14, 13, 87, 15, 72, 96, 81, 22, 08, 49, 72, 30, 70, 24, 79, 31, 16, 64, 59, 21, 89, 34, 96, 91, 48, 76, 43, 53, 88, 01, 57, 80, 23, 81, 90, 79, 58, 01, 80, 87, 17, 99, 86, 90, 72, 63, 32, 69, 14, 28, 88, 69],
[37, 17, 71, 95, 56, 93, 71, 35, 43, 45, 04, 98, 92, 94, 84, 96, 11, 30, 31, 27, 31, 60, 92, 03, 48, 05, 98, 91, 86, 94, 35, 90, 90, 08, 48, 19, 33, 28, 68, 37, 59, 26, 65, 96, 50, 68, 22, 07, 09, 49, 34, 31, 77, 49, 43, 06, 75, 17, 81, 87, 61, 79, 52, 26, 27, 72, 29, 50, 07, 98, 86, 01, 17, 10, 46, 64, 24, 18, 56],
[51, 30, 25, 94, 88, 85, 79, 91, 40, 33, 63, 84, 49, 67, 98, 92, 15, 26, 75, 19, 82, 05, 18, 78, 65, 93, 61, 48, 91, 43, 59, 41, 70, 51, 22, 15, 92, 81, 67, 91, 46, 98, 11, 11, 65, 31, 66, 10, 98, 65, 83, 21, 05, 56, 05, 98, 73, 67, 46, 74, 69, 34, 08, 30, 05, 52, 07, 98, 32, 95, 30, 94, 65, 50, 24, 63, 28, 81, 99, 57],
[19, 23, 61, 36, 09, 89, 71, 98, 65, 17, 30, 29, 89, 26, 79, 74, 94, 11, 44, 48, 97, 54, 81, 55, 39, 66, 69, 45, 28, 47, 13, 86, 15, 76, 74, 70, 84, 32, 36, 33, 79, 20, 78, 14, 41, 47, 89, 28, 81, 05, 99, 66, 81, 86, 38, 26, 06, 25, 13, 60, 54, 55, 23, 53, 27, 05, 89, 25, 23, 11, 13, 54, 59, 54, 56, 34, 16, 24, 53, 44, 06],
[13, 40, 57, 72, 21, 15, 60, 08, 04, 19, 11, 98, 34, 45, 09, 97, 86, 71, 03, 15, 56, 19, 15, 44, 97, 31, 90, 04, 87, 87, 76, 08, 12, 30, 24, 62, 84, 28, 12, 85, 82, 53, 99, 52, 13, 94, 06, 65, 97, 86, 09, 50, 94, 68, 69, 74, 30, 67, 87, 94, 63, 07, 78, 27, 80, 36, 69, 41, 06, 92, 32, 78, 37, 82, 30, 05, 18, 87, 99, 72, 19, 99],
[44, 20, 55, 77, 69, 91, 27, 31, 28, 81, 80, 27, 02, 07, 97, 23, 95, 98, 12, 25, 75, 29, 47, 71, 07, 47, 78, 39, 41, 59, 27, 76, 13, 15, 66, 61, 68, 35, 69, 86, 16, 53, 67, 63, 99, 85, 41, 56, 08, 28, 33, 40, 94, 76, 90, 85, 31, 70, 24, 65, 84, 65, 99, 82, 19, 25, 54, 37, 21, 46, 33, 02, 52, 99, 51, 33, 26, 04, 87, 02, 08, 18, 96],
[54, 42, 61, 45, 91, 06, 64, 79, 80, 82, 32, 16, 83, 63, 42, 49, 19, 78, 65, 97, 40, 42, 14, 61, 49, 34, 04, 18, 25, 98, 59, 30, 82, 72, 26, 88, 54, 36, 21, 75, 03, 88, 99, 53, 46, 51, 55, 78, 22, 94, 34, 40, 68, 87, 84, 25, 30, 76, 25, 08, 92, 84, 42, 61, 40, 38, 09, 99, 40, 23, 29, 39, 46, 55, 10, 90, 35, 84, 56, 70, 63, 23, 91, 39],
[52, 92, 03, 71, 89, 07, 09, 37, 68, 66, 58, 20, 44, 92, 51, 56, 13, 71, 79, 99, 26, 37, 02, 06, 16, 67, 36, 52, 58, 16, 79, 73, 56, 60, 59, 27, 44, 77, 94, 82, 20, 50, 98, 33, 09, 87, 94, 37, 40, 83, 64, 83, 58, 85, 17, 76, 53, 02, 83, 52, 22, 27, 39, 20, 48, 92, 45, 21, 09, 42, 24, 23, 12, 37, 52, 28, 50, 78, 79, 20, 86, 62, 73, 20, 59],
[54, 96, 80, 15, 91, 90, 99, 70, 10, 09, 58, 90, 93, 50, 81, 99, 54, 38, 36, 10, 30, 11, 35, 84, 16, 45, 82, 18, 11, 97, 36, 43, 96, 79, 97, 65, 40, 48, 23, 19, 17, 31, 64, 52, 65, 65, 37, 32, 65, 76, 99, 79, 34, 65, 79, 27, 55, 33, 03, 01, 33, 27, 61, 28, 66, 08, 04, 70, 49, 46, 48, 83, 01, 45, 19, 96, 13, 81, 14, 21, 31, 79, 93, 85, 50, 05],
[92, 92, 48, 84, 59, 98, 31, 53, 23, 27, 15, 22, 79, 95, 24, 76, 05, 79, 16, 93, 97, 89, 38, 89, 42, 83, 02, 88, 94, 95, 82, 21, 01, 97, 48, 39, 31, 78, 09, 65, 50, 56, 97, 61, 01, 07, 65, 27, 21, 23, 14, 15, 80, 97, 44, 78, 49, 35, 33, 45, 81, 74, 34, 05, 31, 57, 09, 38, 94, 07, 69, 54, 69, 32, 65, 68, 46, 68, 78, 90, 24, 28, 49, 51, 45, 86, 35],
[41, 63, 89, 76, 87, 31, 86, 09, 46, 14, 87, 82, 22, 29, 47, 16, 13, 10, 70, 72, 82, 95, 48, 64, 58, 43, 13, 75, 42, 69, 21, 12, 67, 13, 64, 85, 58, 23, 98, 09, 37, 76, 05, 22, 31, 12, 66, 50, 29, 99, 86, 72, 45, 25, 10, 28, 19, 06, 90, 43, 29, 31, 67, 79, 46, 25, 74, 14, 97, 35, 76, 37, 65, 46, 23, 82, 06, 22, 30, 76, 93, 66, 94, 17, 96, 13, 20, 72],
[63, 40, 78, 08, 52, 09, 90, 41, 70, 28, 36, 14, 46, 44, 85, 96, 24, 52, 58, 15, 87, 37, 05, 98, 99, 39, 13, 61, 76, 38, 44, 99, 83, 74, 90, 22, 53, 80, 56, 98, 30, 51, 63, 39, 44, 30, 91, 91, 04, 22, 27, 73, 17, 35, 53, 18, 35, 45, 54, 56, 27, 78, 48, 13, 69, 36, 44, 38, 71, 25, 30, 56, 15, 22, 73, 43, 32, 69, 59, 25, 93, 83, 45, 11, 34, 94, 44, 39, 92],
[12, 36, 56, 88, 13, 96, 16, 12, 55, 54, 11, 47, 19, 78, 17, 17, 68, 81, 77, 51, 42, 55, 99, 85, 66, 27, 81, 79, 93, 42, 65, 61, 69, 74, 14, 01, 18, 56, 12, 01, 58, 37, 91, 22, 42, 66, 83, 25, 19, 04, 96, 41, 25, 45, 18, 69, 96, 88, 36, 93, 10, 12, 98, 32, 44, 83, 83, 04, 72, 91, 04, 27, 73, 07, 34, 37, 71, 60, 59, 31, 01, 54, 54, 44, 96, 93, 83, 36, 04, 45],
[30, 18, 22, 20, 42, 96, 65, 79, 17, 41, 55, 69, 94, 81, 29, 80, 91, 31, 85, 25, 47, 26, 43, 49, 02, 99, 34, 67, 99, 76, 16, 14, 15, 93, 08, 32, 99, 44, 61, 77, 67, 50, 43, 55, 87, 55, 53, 72, 17, 46, 62, 25, 50, 99, 73, 05, 93, 48, 17, 31, 70, 80, 59, 09, 44, 59, 45, 13, 74, 66, 58, 94, 87, 73, 16, 14, 85, 38, 74, 99, 64, 23, 79, 28, 71, 42, 20, 37, 82, 31, 23],
[51, 96, 39, 65, 46, 71, 56, 13, 29, 68, 53, 86, 45, 33, 51, 49, 12, 91, 21, 21, 76, 85, 02, 17, 98, 15, 46, 12, 60, 21, 88, 30, 92, 83, 44, 59, 42, 50, 27, 88, 46, 86, 94, 73, 45, 54, 23, 24, 14, 10, 94, 21, 20, 34, 23, 51, 04, 83, 99, 75, 90, 63, 60, 16, 22, 33, 83, 70, 11, 32, 10, 50, 29, 30, 83, 46, 11, 05, 31, 17, 86, 42, 49, 01, 44, 63, 28, 60, 07, 78, 95, 40],
[44, 61, 89, 59, 04, 49, 51, 27, 69, 71, 46, 76, 44, 04, 09, 34, 56, 39, 15, 06, 94, 91, 75, 90, 65, 27, 56, 23, 74, 06, 23, 33, 36, 69, 14, 39, 05, 34, 35, 57, 33, 22, 76, 46, 56, 10, 61, 65, 98, 09, 16, 69, 04, 62, 65, 18, 99, 76, 49, 18, 72, 66, 73, 83, 82, 40, 76, 31, 89, 91, 27, 88, 17, 35, 41, 35, 32, 51, 32, 67, 52, 68, 74, 85, 80, 57, 07, 11, 62, 66, 47, 22, 67],
[65, 37, 19, 97, 26, 17, 16, 24, 24, 17, 50, 37, 64, 82, 24, 36, 32, 11, 68, 34, 69, 31, 32, 89, 79, 93, 96, 68, 49, 90, 14, 23, 04, 04, 67, 99, 81, 74, 70, 74, 36, 96, 68, 09, 64, 39, 88, 35, 54, 89, 96, 58, 66, 27, 88, 97, 32, 14, 06, 35, 78, 20, 71, 06, 85, 66, 57, 02, 58, 91, 72, 05, 29, 56, 73, 48, 86, 52, 09, 93, 22, 57, 79, 42, 12, 01, 31, 68, 17, 59, 63, 76, 07, 77],
[73, 81, 14, 13, 17, 20, 11, 09, 01, 83, 08, 85, 91, 70, 84, 63, 62, 77, 37, 07, 47, 01, 59, 95, 39, 69, 39, 21, 99, 09, 87, 02, 97, 16, 92, 36, 74, 71, 90, 66, 33, 73, 73, 75, 52, 91, 11, 12, 26, 53, 05, 26, 26, 48, 61, 50, 90, 65, 01, 87, 42, 47, 74, 35, 22, 73, 24, 26, 56, 70, 52, 05, 48, 41, 31, 18, 83, 27, 21, 39, 80, 85, 26, 08, 44, 02, 71, 07, 63, 22, 05, 52, 19, 08, 20],
[17, 25, 21, 11, 72, 93, 33, 49, 64, 23, 53, 82, 03, 13, 91, 65, 85, 02, 40, 05, 42, 31, 77, 42, 05, 36, 06, 54, 04, 58, 07, 76, 87, 83, 25, 57, 66, 12, 74, 33, 85, 37, 74, 32, 20, 69, 03, 97, 91, 68, 82, 44, 19, 14, 89, 28, 85, 85, 80, 53, 34, 87, 58, 98, 88, 78, 48, 65, 98, 40, 11, 57, 10, 67, 70, 81, 60, 79, 74, 72, 97, 59, 79, 47, 30, 20, 54, 80, 89, 91, 14, 05, 33, 36, 79, 39],
[60, 85, 59, 39, 60, 07, 57, 76, 77, 92, 06, 35, 15, 72, 23, 41, 45, 52, 95, 18, 64, 79, 86, 53, 56, 31, 69, 11, 91, 31, 84, 50, 44, 82, 22, 81, 41, 40, 30, 42, 30, 91, 48, 94, 74, 76, 64, 58, 74, 25, 96, 57, 14, 19, 03, 99, 28, 83, 15, 75, 99, 01, 89, 85, 79, 50, 03, 95, 32, 67, 44, 08, 07, 41, 62, 64, 29, 20, 14, 76, 26, 55, 48, 71, 69, 66, 19, 72, 44, 25, 14, 01, 48, 74, 12, 98, 07],
[64, 66, 84, 24, 18, 16, 27, 48, 20, 14, 47, 69, 30, 86, 48, 40, 23, 16, 61, 21, 51, 50, 26, 47, 35, 33, 91, 28, 78, 64, 43, 68, 04, 79, 51, 08, 19, 60, 52, 95, 06, 68, 46, 86, 35, 97, 27, 58, 04, 65, 30, 58, 99, 12, 12, 75, 91, 39, 50, 31, 42, 64, 70, 04, 46, 07, 98, 73, 98, 93, 37, 89, 77, 91, 64, 71, 64, 65, 66, 21, 78, 62, 81, 74, 42, 20, 83, 70, 73, 95, 78, 45, 92, 27, 34, 53, 71, 15],
[30, 11, 85, 31, 34, 71, 13, 48, 05, 14, 44, 03, 19, 67, 23, 73, 19, 57, 06, 90, 94, 72, 57, 69, 81, 62, 59, 68, 88, 57, 55, 69, 49, 13, 07, 87, 97, 80, 89, 05, 71, 05, 05, 26, 38, 40, 16, 62, 45, 99, 18, 38, 98, 24, 21, 26, 62, 74, 69, 04, 85, 57, 77, 35, 58, 67, 91, 79, 79, 57, 86, 28, 66, 34, 72, 51, 76, 78, 36, 95, 63, 90, 08, 78, 47, 63, 45, 31, 22, 70, 52, 48, 79, 94, 15, 77, 61, 67, 68],
[23, 33, 44, 81, 80, 92, 93, 75, 94, 88, 23, 61, 39, 76, 22, 03, 28, 94, 32, 06, 49, 65, 41, 34, 18, 23, 08, 47, 62, 60, 03, 63, 33, 13, 80, 52, 31, 54, 73, 43, 70, 26, 16, 69, 57, 87, 83, 31, 03, 93, 70, 81, 47, 95, 77, 44, 29, 68, 39, 51, 56, 59, 63, 07, 25, 70, 07, 77, 43, 53, 64, 03, 94, 42, 95, 39, 18, 01, 66, 21, 16, 97, 20, 50, 90, 16, 70, 10, 95, 69, 29, 06, 25, 61, 41, 26, 15, 59, 63, 35]
]