-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathGithubPL.pl
More file actions
404 lines (349 loc) · 47.8 KB
/
GithubPL.pl
File metadata and controls
404 lines (349 loc) · 47.8 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
/* <Username: jg495 Name: GuanJun>
The program not produce multiple answers.
1. <Number of elements in the list binding Q after executing s1(Q,100) is 1747>
<The main idea for s1:
step 1: using Sieve of Eratosthenes method to get prime number list which is less than 100
step 2: geting composite number list according to prime number list which is less than 100
step 3: combining the prime number list with prime list[P,C,P+C,P*C] and combining the composite number list with
composite number list[C1,C2,C1+C2,C1*C2]. In this step,firstly I am going to get rid of the pairs which its sum
more than 100. Secondly, after adding the first filter, I am using mergesort
to order the list by it's product,afterthen,I will move out the list which it's product is single(compare the product of
the list and it's next list, if they are equal, then save all the list which have the same product with the first list.
Otherwise, delete that list).
step 4: mergesort the list by it's sum
>
I have not used built-ins.
2. <Number of elements in the list binding Q after executing s2(Q,100) is 145 >
<step 1: using Sieve of Eratosthenes method to get prime number list which is less than 55(53+2,the minimum prime number which is greater than 50 +2)
step 2: geting composite number list according to prime number list which is less than 55
step 3: combining the prime number list with prime list[P,C,P+C,P*C] and combining the composite number list with
composite number list[C1,C2,C1+C2,C1*C2]. In this step,firstly I will get rid of some pairs if its value of sum more than 55
and is an even number. Secondly, after adding the first filter,I am going to delete the list which their sum-2 is prime number or their sum divede 3 is a prime number.
step 4: mergesort the list by it's product >
I have not used built-ins.
3. <Number of elements in the list binding Q after executing s3(Q,100) is 86>
<select the list which their product is unit>
I have not used built-ins.
4.
<select the list which their Sum is unit>
I have not used built-ins.
5. <Number of elements in the list binding Q after executing s4(Q,500) is 1>
s4(Q,500) uses <1,109,560> inferences. */
%--------------------------------------------------------------------------------------------
s4(Q,Max):-
s3(S3Result,Max),
findTheFinalAnswer(S3Result,S4Result),
app([S4Result],[],Q).
findTheFinalAnswer([[_,_,S,_],[_,_,S,_]|T],L):-
deleteDuplicateSum(S,T,Tnew),
findTheFinalAnswer(Tnew,L).
findTheFinalAnswer([[A1,B1,S1,P1],[_,_,S2,_]|_],[A1,B1,S1,P1]):-
S1=\=S2.
deleteDuplicateSum(S,[[_,_,S,_]|T],L):-
deleteDuplicateSum(S,T,L).
deleteDuplicateSum(N,[[A,B,S,P]|T],[[A,B,S,P]|T]):-
N=\=S.
%--------------------------------------------------------------------------------------------
s3(Q,Max):-
s2(S2Result,Max),
getSingleProduct(S2Result,[],Result),
merge_sort2(Result,Q).
getSingleProduct([[_,_,_,P],[_,_,_,P]|T],L,R):-
deleteDuplicateNum(P,T,Tnew),
getSingleProduct(Tnew,L,R).
getSingleProduct([[A1,B1,C1,D1],[A2,B2,C2,D2]|T],L,R):-
D1=\=D2,
app([[A1,B1,C1,D1]],L,Lnew),
getSingleProduct([[A2,B2,C2,D2]|T],Lnew,R).
getSingleProduct([],Ls,Ls).
getSingleProduct([H|T],L,R):-
T = [],
app([H],L,R).
deleteDuplicateNum(P,[[_,_,_,P]|T],R):-
deleteDuplicateNum(P,T,R).
deleteDuplicateNum(N,[[A,B,C,D]|T],[[A,B,C,D]|T]):-
N=\=D.
deleteDuplicateNum(_,[],[]).
%--------------------------------------------------------------------------------------------
s2(Q,Max):-
Maxnew2 is Max/2,
getMaxPrime(Maxnew2,MaxPrime),
BigestSum is MaxPrime+2,
getPrimeList(BigestSum,LPrime), %get Prime number list < 55
setTheNum(2,BigestSum,LPrime,[],L1), %get composite number list <55
rev(L1,L1new),
toGetPLS2(BigestSum,LPrime,L1new,PLList), %get p*p
toGetLLS2(BigestSum,L1new,LLList), %get c*c
app(PLList,LLList,TList),
delete2AddPSumS2(TList,LPrime,[],Result), %move out if (sum-2) is prime
deleteDivideBy3(Result,[],Result2), %move out if (sum mod 3 =0)and(sum/3) is prime
merge_sort(Result2,Q).
deleteDivideBy3([[A,B,S,P]|T],L,R):-
S mod 3 =\=0,
deleteDivideBy3(T,[[A,B,S,P]|L],R).
deleteDivideBy3([[A,B,S,P]|T],L,R):-
S mod 3 =:=0,
Test is S/3,
isNot(isPrime(Test,2)),
deleteDivideBy3(T,[[A,B,S,P]|L],R).
deleteDivideBy3([[_,_,S,_]|T],L,R):-
S mod 3 =:=0,
Test is S/3,
isPrime(Test,2),
deleteDivideBy3(T,L,R).
deleteDivideBy3([],L,L).
delete2AddPSumS2([[A,B,S,P]|T],LPrime,L,R):-
TestNumber is S-2,
isNot(isTheMember(TestNumber,LPrime)),
delete2AddPSumS2(T,LPrime,[[A,B,S,P]|L],R).
delete2AddPSumS2([[_,_,S,_]|T],LPrime,L,R):-
TestNumber is S-2,
isTheMember(TestNumber,LPrime),
delete2AddPSumS2(T,LPrime,L,R).
delete2AddPSumS2([],_,L,L).
getMaxPrime(N,R):-
isNot(isPrime(N,2)),
Nnew is N+1,
getMaxPrime(Nnew,R).
getMaxPrime(R,R):-
isPrime(R,2).
toGetPLS2(Max,L1,L2,R):-
getPLListS2(Max,L1,L2,[],R).
getPLListS2(_,[],_,Ls,Ls).
getPLListS2(Max,[H|T],L,Ls,R):-
getEachPLS2(Max,H,L,[],PLnew),
app(PLnew,Ls,Lsnew),
getPLListS2(Max,T,L,Lsnew,R).
getEachPLS2(_,_,[],L,L).
getEachPLS2(Max,E,[H|T],L,R):-
E+H<Max,
Sum is E+H,
Sum mod 2 =\=0,
E<H,
Product is E*H,
app([[E,H,Sum,Product]],L,Lnew),
getEachPLS2(Max,E,T,Lnew,R).
getEachPLS2(Max,E,[H|T],L,R):-
E+H<Max,
Sum is E+H,
Sum mod 2 =\=0,
E>H,
Product is E*H,
app([[H,E,Sum,Product]],L,Lnew),
getEachPLS2(Max,E,T,Lnew,R).
getEachPLS2(Max,E,[H|T],L,R):-
E+H<Max,
Sum is E+H,
Sum mod 2 =:=0,
getEachPLS2(Max,E,T,L,R).
getEachPLS2(Max,E,[H|_],L,L):-
E+H>=Max.
toGetLLS2(Max,L,R):-
getLLListS2(Max,L,[],R).
getLLListS2(_,[],L1,L1).
getLLListS2(Max,[H|T],L1,R):-
getEachLS2(Max,H,T,[],Lnew),
app(Lnew,L1,L1new),
getLLListS2(Max,T,L1new,R).
getEachLS2(_,_,[],L,L).
getEachLS2(Max,E,[H|T],L,R):-
E+H<Max,
Sum is E+H,
Sum mod 2 =\=0,
Product is E*H,
app([[E,H,Sum,Product]],L,Lnew),
getEachLS2(Max,E,T,Lnew,R).
getEachLS2(Max,E,[H|T],L,R):-
E+H<Max,
Sum is E+H,
Sum mod 2 =:=0,
getEachLS2(Max,E,T,L,R).
getEachLS2(Max,E,[H|_],L,L):-
E+H>=Max.
%--------------------------------------------------------------------------------------------
s1(Q,Max):-
Maxnew is Max-1,
getPrimeList(Maxnew,LPrime),
Maxnew2 is Max/2,
getPrimeList(Maxnew2,LPrimeS), %get Prime number List
setTheNum(2,Maxnew,LPrime,[],L1), %get composite number List
toGetPL(Max,LPrimeS,L1,PLList), %prime list * composit list
toGetLL(Max,L1,LLList), %composit list * composit list
app(PLList,LLList,Result),
merge_sort(Result,Result2),
getFinalAns(Result2,[],Result3), %delete unit product
merge_sort2(Result3,Q).
getFinalAns([[A1,B1,S1,P1],[A2,B2,S2,P2]|T],L,R):-
P1=:=P2,
doMore(P1,[[A1,B1,S1,P1],[A2,B2,S2,P2]|T],[],NewList,NewT),
app(NewList,L,Lnew),
getFinalAns(NewT,Lnew,R).
getFinalAns([[_,_,_,P1],[A,B,S,P2]|T],L,R):-
P1=\=P2,
getFinalAns([[A,B,S,P2]|T],L,R).
getFinalAns([_|T],R,R):-
T=[].
getFinalAns([],R,R).
doMore(N,[[A,B,S,P]|T],Ls,R,NewT):-
N=:=P,
doMore(N,T,[[A,B,S,P]|Ls],R,NewT).
doMore(N,[[A,B,S,P]|T],R,R,[[A,B,S,P]|T]):-
N=\=P.
doMore(_,[],R,R,[]).
toGetPL(Max,L1,L2,R):-
getPLList(Max,L1,L2,[],R).
getPLList(_,[],_,Ls,Ls).
getPLList(Max,[H|T],L,Ls,R):-
getEachPL(Max,H,L,[],PLnew),
app(PLnew,Ls,Lsnew),
getPLList(Max,T,L,Lsnew,R).
getEachPL(_,_,[],L,L).
getEachPL(Max,E,[H|T],L,R):-
E+H=<Max,
E<H,
Sum is E+H,
Product is E*H,
app([[E,H,Sum,Product]],L,Lnew),
getEachPL(Max,E,T,Lnew,R).
getEachPL(Max,E,[H|T],L,R):-
E+H=<Max,
E>H,
Sum is E+H,
Product is E*H,
app([[H,E,Sum,Product]],L,Lnew),
getEachPL(Max,E,T,Lnew,R).
getEachPL(Max,E,[H|T],L,R):-
E+H>Max,
getEachPL(Max,E,T,L,R).
toGetLL(Max,L,R):-
rev(L,Lnew),
getLLList(Max,Lnew,Lnew,[],R).
getLLList(_,[],_,L2,L2).
getLLList(Max,[H|T],L1,L2,R):-
getEachL(Max,H,L1,[],Lnew),
app(Lnew,L2,L2new),
getLLList(Max,T,L1,L2new,R).
getEachL(_,_,[],L,L).
getEachL(Max,E,[H|T],L,R):-
E<H,
E+H=<Max,
Sum is E+H,
Product is E*H,
app([[E,H,Sum,Product]],L,Lnew),
getEachL(Max,E,T,Lnew,R).
getEachL(Max,E,[H|T],L,R):-
E>=H,
E+H=<Max,
getEachL(Max,E,T,L,R).
getEachL(Max,E,[H|_],L,L):-
E+H>Max.
setTheNum(Max,Max,_,L,L).
setTheNum(N,Max,[],L,R):-
N<Max,
Nnew is N+1,
setTheNum(Nnew,Max,[],[N|L],R).
setTheNum(N,Max,[H|T],L,R):-
N<Max,
N=\=H,
Nnew is N+1,
setTheNum(Nnew,Max,[H|T],[N|L],R).
setTheNum(N,Max,[H|T],L,R):-
N<Max,
N=:=H,
Nnew is N+1,
setTheNum(Nnew,Max,T,L,R).
getPrimeList(Max,R):-setList(Max,[],R,Max).
setList(1,L,R,Max):-setPrimeNumber(2,L,R,Max).
setList(N,L,R,Max):-
N>1,
Nnew is N-1,
setList(Nnew,[N|L],R,Max).
setPrimeNumber(Prime,L,R,Max):-
Prime=<sqrt(Max),
isPrime(Prime,2),
deleteNum(Prime,L,Lnew),
PrimeNew is Prime+1,
setPrimeNumber(PrimeNew,Lnew,R,Max).
setPrimeNumber(Prime,L,R,Max):-
Prime=<sqrt(Max),
isNot(isPrime(Prime,2)),
PrimeNew is Prime+1,
setPrimeNumber(PrimeNew,L,R,Max).
setPrimeNumber(Prime,L,L,Max):-
Prime>sqrt(Max).
deleteNum(Prime,L,R):- deleteisNotPrime(Prime,L,[],R).
deleteisNotPrime(Prime,[H|T],L,R):-
H =\= Prime,
H mod Prime =:= 0,
deleteisNotPrime(Prime,T,L,R).
deleteisNotPrime(H,[H|T],L,R):-
deleteisNotPrime(H,T,[H|L],R).
deleteisNotPrime(Prime,[H|T],L,R):-
H mod Prime =\= 0,
deleteisNotPrime(Prime,T,[H|L],R).
deleteisNotPrime(_,[],L,R):-
rev(L,R).
rev(L,R):- theRev(L,[],R).
theRev([],A,A).
theRev([H|T],A,R):- theRev(T,[H|A],R).
%test the number if is prime number
isPrime(X,X).
isPrime(X,Y):-
Y<X,
0 =\= X mod Y,
Ynew is Y+1,
isPrime(X,Ynew).
isNot(Function):-
Function,
!,
fail.
isNot(_).
app([],L,L).
app([E|T],L,[E|M]) :- app(T,L,M).
merge_sort2([],[]).
merge_sort2([X],[X]).
merge_sort2(List,Sorted):-
List=[_,_|_],divide(List,L1,L2),
merge_sort2(L1,Sorted1),merge_sort2(L2,Sorted2),
merge2(Sorted1,Sorted2,Sorted).
merge2([],L,L).
merge2(L,[],L):-L\=[].
merge2([[A1,B1,S1,P1]|T1],[[A2,B2,S2,P2]|T2],[[A1,B1,S1,P1]|T]):-S1=<S2,merge2(T1,[[A2,B2,S2,P2]|T2],T).
merge2([[A1,B1,S1,P1]|T1],[[A2,B2,S2,P2]|T2],[[A2,B2,S2,P2]|T]):-S1>S2,merge2([[A1,B1,S1,P1]|T1],T2,T).
merge_sort([],[]).
merge_sort([X],[X]).
merge_sort(List,Sorted):-
List=[_,_|_],divide(List,L1,L2),
merge_sort(L1,Sorted1),merge_sort(L2,Sorted2),
merge(Sorted1,Sorted2,Sorted).
merge([],L,L).
merge(L,[],L):-L\=[].
merge([[A1,B1,S1,P1]|T1],[[A2,B2,S2,P2]|T2],[[A1,B1,S1,P1]|T]):-P1=<P2,merge(T1,[[A2,B2,S2,P2]|T2],T).
merge([[A1,B1,S1,P1]|T1],[[A2,B2,S2,P2]|T2],[[A2,B2,S2,P2]|T]):-P1>P2,merge([[A1,B1,S1,P1]|T1],T2,T).
divide(L,L1,L2):-halve(L,L1,L2).
halve(L,A,B):-hv(L,L,A,B).
hv([],R,[],R).
hv([_],R,[],R).
hv([_,_|T],[X|L],[X|L1],R):-hv(T,L,L1,R).
isTheMember(E,[E|_]):-!.
isTheMember(E,[_|R]) :- isTheMember(E,R).
/*
?- consult(<jg495>).
% jg495 compiled 0.01 sec, 1 clauses
true.
?- time(s1(Q,100)).
% 161,966 inferences, 0.076 CPU in 0.083 seconds (91% CPU, 2124116 Lips)
Q = [[3, 4, 7, 12], [2, 6, 8, 12], [4, 5, 9, 20], [3, 6, 9, 18], [4, 6, 10, 24], [5, 6, 11, 30], [4, 7, 11, 28], [3, 8, 11, 24], [2, 9, 11, 18], [4, 8, 12, 32], [2, 10, 12, 20], [6, 7, 13, 42], [5, 8, 13, 40], [4, 9, 13, 36], [3, 10, 13, 30], [6, 8, 14, 48], [5, 9, 14, 45], [4, 10, 14, 40], [2, 12, 14, 24], [7, 8, 15, 56], [6, 9, 15, 54], [5, 10, 15, 50], [4, 11, 15, 44], [3, 12, 15, 36], [7, 9, 16, 63], [6, 10, 16, 60], [4, 12, 16, 48], [2, 14, 16, 28], [8, 9, 17, 72], [7, 10, 17, 70], [6, 11, 17, 66], [5, 12, 17, 60], [4, 13, 17, 52], [3, 14, 17, 42], [2, 15, 17, 30], [8, 10, 18, 80], [6, 12, 18, 72], [4, 14, 18, 56], [3, 15, 18, 45], [2, 16, 18, 32], [9, 10, 19, 90], [8, 11, 19, 88], [7, 12, 19, 84], [6, 13, 19, 78], [5, 14, 19, 70], [4, 15, 19, 60], [3, 16, 19, 48], [9, 11, 20, 99], [8, 12, 20, 96], [6, 14, 20, 84], [5, 15, 20, 75], [4, 16, 20, 64], [2, 18, 20, 36], [10, 11, 21, 110], [9, 12, 21, 108], [8, 13, 21, 104], [7, 14, 21, 98], [6, 15, 21, 90], [5, 16, 21, 80], [4, 17, 21, 68], [3, 18, 21, 54], [10, 12, 22, 120], [9, 13, 22, 117], [8, 14, 22, 112], [7, 15, 22, 105], [6, 16, 22, 96], [4, 18, 22, 72], [2, 20, 22, 40], [11, 12, 23, 132], [10, 13, 23, 130], [9, 14, 23, 126], [8, 15, 23, 120], [7, 16, 23, 112], [6, 17, 23, 102], [5, 18, 23, 90], [4, 19, 23, 76], [3, 20, 23, 60], [2, 21, 23, 42], [10, 14, 24, 140], [9, 15, 24, 135], [8, 16, 24, 128], [6, 18, 24, 108], [4, 20, 24, 80], [3, 21, 24, 63], [2, 22, 24, 44], [12, 13, 25, 156], [11, 14, 25, 154], [10, 15, 25, 150], [9, 16, 25, 144], [8, 17, 25, 136], [7, 18, 25, 126], [6, 19, 25, 114], [5, 20, 25, 100], [4, 21, 25, 84], [3, 22, 25, 66], [12, 14, 26, 168], [11, 15, 26, 165], [10, 16, 26, 160], [9, 17, 26, 153], [8, 18, 26, 144], [6, 20, 26, 120], [5, 21, 26, 105], [4, 22, 26, 88], [2, 24, 26, 48], [13, 14, 27, 182], [12, 15, 27, 180], [11, 16, 27, 176], [10, 17, 27, 170], [9, 18, 27, 162], [8, 19, 27, 152], [7, 20, 27, 140], [6, 21, 27, 126], [5, 22, 27, 110], [4, 23, 27, 92], [3, 24, 27, 72], [2, 25, 27, 50], [13, 15, 28, 195], [12, 16, 28, 192], [10, 18, 28, 180], [9, 19, 28, 171], [8, 20, 28, 160], [7, 21, 28, 147], [6, 22, 28, 132], [4, 24, 28, 96], [3, 25, 28, 75], [2, 26, 28, 52], [14, 15, 29, 210], [13, 16, 29, 208], [12, 17, 29, 204], [11, 18, 29, 198], [10, 19, 29, 190], [9, 20, 29, 180], [8, 21, 29, 168], [7, 22, 29, 154], [6, 23, 29, 138], [5, 24, 29, 120], [4, 25, 29, 100], [3, 26, 29, 78], [2, 27, 29, 54], [14, 16, 30, 224], [12, 18, 30, 216], [10, 20, 30, 200], [9, 21, 30, 189], [8, 22, 30, 176], [6, 24, 30, 144], [4, 26, 30, 104], [2, 28, 30, 56], [15, 16, 31, 240], [14, 17, 31, 238], [13, 18, 31, 234], [12, 19, 31, 228], [11, 20, 31, 220], [10, 21, 31, 210], [9, 22, 31, 198], [8, 23, 31, 184], [7, 24, 31, 168], [6, 25, 31, 150], [5, 26, 31, 130], [4, 27, 31, 108], [3, 28, 31, 84], [15, 17, 32, 255], [14, 18, 32, 252], [12, 20, 32, 240], [11, 21, 32, 231], [10, 22, 32, 220], [9, 23, 32, 207], [8, 24, 32, 192], [7, 25, 32, 175], [6, 26, 32, 156], [5, 27, 32, 135], [4, 28, 32, 112], [2, 30, 32, 60], [16, 17, 33, 272], [15, 18, 33, 270], [14, 19, 33, 266], [13, 20, 33, 260], [12, 21, 33, 252], [10, 23, 33, 230], [9, 24, 33, 216], [8, 25, 33, 200], [7, 26, 33, 182], [6, 27, 33, 162], [5, 28, 33, 140], [4, 29, 33, 116], [3, 30, 33, 90], [16, 18, 34, 288], [15, 19, 34, 285], [14, 20, 34, 280], [13, 21, 34, 273], [12, 22, 34, 264], [10, 24, 34, 240], [9, 25, 34, 225], [8, 26, 34, 208], [7, 27, 34, 189], [6, 28, 34, 168], [4, 30, 34, 120], [2, 32, 34, 64], [17, 18, 35, 306], [16, 19, 35, 304], [15, 20, 35, 300], [14, 21, 35, 294], [13, 22, 35, 286], [12, 23, 35, 276], [11, 24, 35, 264], [10, 25, 35, 250], [9, 26, 35, 234], [8, 27, 35, 216], [7, 28, 35, 196], [6, 29, 35, 174], [5, 30, 35, 150], [4, 31, 35, 124], [3, 32, 35, 96], [2, 33, 35, 66], [16, 20, 36, 320], [15, 21, 36, 315], [14, 22, 36, 308], [12, 24, 36, 288], [11, 25, 36, 275], [10, 26, 36, 260], [9, 27, 36, 243], [8, 28, 36, 224], [6, 30, 36, 180], [4, 32, 36, 128], [3, 33, 36, 99], [2, 34, 36, 68], [18, 19, 37, 342], [17, 20, 37, 340], [16, 21, 37, 336], [15, 22, 37, 330], [14, 23, 37, 322], [13, 24, 37, 312], [12, 25, 37, 300], [11, 26, 37, 286], [10, 27, 37, 270], [9, 28, 37, 252], [8, 29, 37, 232], [7, 30, 37, 210], [6, 31, 37, 186], [5, 32, 37, 160], [4, 33, 37, 132], [3, 34, 37, 102], [2, 35, 37, 70], [18, 20, 38, 360], [17, 21, 38, 357], [16, 22, 38, 352], [15, 23, 38, 345], [14, 24, 38, 336], [13, 25, 38, 325], [12, 26, 38, 312], [11, 27, 38, 297], [10, 28, 38, 280], [9, 29, 38, 261], [8, 30, 38, 240], [6, 32, 38, 192], [5, 33, 38, 165], [4, 34, 38, 136], [3, 35, 38, 105], [2, 36, 38, 72], [19, 20, 39, 380], [18, 21, 39, 378], [17, 22, 39, 374], [16, 23, 39, 368], [15, 24, 39, 360], [14, 25, 39, 350], [12, 27, 39, 324], [11, 28, 39, 308], [10, 29, 39, 290], [9, 30, 39, 270], [8, 31, 39, 248], [7, 32, 39, 224], [6, 33, 39, 198], [5, 34, 39, 170], [4, 35, 39, 140], [3, 36, 39, 108], [19, 21, 40, 399], [18, 22, 40, 396], [16, 24, 40, 384], [15, 25, 40, 375], [14, 26, 40, 364], [13, 27, 40, 351], [12, 28, 40, 336], [10, 30, 40, 300], [9, 31, 40, 279], [8, 32, 40, 256], [7, 33, 40, 231], [6, 34, 40, 204], [5, 35, 40, 175], [4, 36, 40, 144], [2, 38, 40, 76], [20, 21, 41, 420], [19, 22, 41, 418], [18, 23, 41, 414], [17, 24, 41, 408], [16, 25, 41, 400], [15, 26, 41, 390], [14, 27, 41, 378], [13, 28, 41, 364], [12, 29, 41, 348], [11, 30, 41, 330], [10, 31, 41, 310], [9, 32, 41, 288], [8, 33, 41, 264], [7, 34, 41, 238], [6, 35, 41, 210], [5, 36, 41, 180], [4, 37, 41, 148], [3, 38, 41, 114], [2, 39, 41, 78], [20, 22, 42, 440], [18, 24, 42, 432], [17, 25, 42, 425], [16, 26, 42, 416], [15, 27, 42, 405], [14, 28, 42, 392], [12, 30, 42, 360], [10, 32, 42, 320], [9, 33, 42, 297], [8, 34, 42, 272], [7, 35, 42, 245], [6, 36, 42, 216], [4, 38, 42, 152], [3, 39, 42, 117], [2, 40, 42, 80], [21, 22, 43, 462], [20, 23, 43, 460], [19, 24, 43, 456], [18, 25, 43, 450], [17, 26, 43, 442], [16, 27, 43, 432], [15, 28, 43, 420], [14, 29, 43, 406], [13, 30, 43, 390], [12, 31, 43, 372], [11, 32, 43, 352], [10, 33, 43, 330], [9, 34, 43, 306], [8, 35, 43, 280], [7, 36, 43, 252], [6, 37, 43, 222], [5, 38, 43, 190], [4, 39, 43, 156], [3, 40, 43, 120], [21, 23, 44, 483], [20, 24, 44, 480], [19, 25, 44, 475], [18, 26, 44, 468], [17, 27, 44, 459], [16, 28, 44, 448], [15, 29, 44, 435], [14, 30, 44, 420], [12, 32, 44, 384], [10, 34, 44, 340], [9, 35, 44, 315], [8, 36, 44, 288], [6, 38, 44, 228], [5, 39, 44, 195], [4, 40, 44, 160], [2, 42, 44, 84], [22, 23, 45, 506], [21, 24, 45, 504], [20, 25, 45, 500], [19, 26, 45, 494], [18, 27, 45, 486], [17, 28, 45, 476], [16, 29, 45, 464], [15, 30, 45, 450], [14, 31, 45, 434], [13, 32, 45, 416], [12, 33, 45, 396], [11, 34, 45, 374], [10, 35, 45, 350], [9, 36, 45, 324], [8, 37, 45, 296], [7, 38, 45, 266], [6, 39, 45, 234], [5, 40, 45, 200], [4, 41, 45, 164], [3, 42, 45, 126], [22, 24, 46, 528], [21, 25, 46, 525], [20, 26, 46, 520], [19, 27, 46, 513], [18, 28, 46, 504], [16, 30, 46, 480], [15, 31, 46, 465], [14, 32, 46, 448], [13, 33, 46, 429], [12, 34, 46, 408], [11, 35, 46, 385], [10, 36, 46, 360], [8, 38, 46, 304], [7, 39, 46, 273], [6, 40, 46, 240], [4, 42, 46, 168], [2, 44, 46, 88], [23, 24, 47, 552], [22, 25, 47, 550], [21, 26, 47, 546], [20, 27, 47, 540], [19, 28, 47, 532], [18, 29, 47, 522], [17, 30, 47, 510], [16, 31, 47, 496], [15, 32, 47, 480], [14, 33, 47, 462], [13, 34, 47, 442], [12, 35, 47, 420], [11, 36, 47, 396], [10, 37, 47, 370], [9, 38, 47, 342], [8, 39, 47, 312], [7, 40, 47, 280], [6, 41, 47, 246], [5, 42, 47, 210], [4, 43, 47, 172], [3, 44, 47, 132], [2, 45, 47, 90], [22, 26, 48, 572], [21, 27, 48, 567], [20, 28, 48, 560], [18, 30, 48, 540], [16, 32, 48, 512], [15, 33, 48, 495], [14, 34, 48, 476], [13, 35, 48, 455], [12, 36, 48, 432], [10, 38, 48, 380], [9, 39, 48, 351], [8, 40, 48, 320], [6, 42, 48, 252], [4, 44, 48, 176], [3, 45, 48, 135], [2, 46, 48, 92], [24, 25, 49, 600], [23, 26, 49, 598], [22, 27, 49, 594], [21, 28, 49, 588], [20, 29, 49, 580], [19, 30, 49, 570], [18, 31, 49, 558], [17, 32, 49, 544], [16, 33, 49, 528], [15, 34, 49, 510], [14, 35, 49, 490], [13, 36, 49, 468], [12, 37, 49, 444], [11, 38, 49, 418], [10, 39, 49, 390], [9, 40, 49, 360], [8, 41, 49, 328], [7, 42, 49, 294], [6, 43, 49, 258], [5, 44, 49, 220], [4, 45, 49, 180], [3, 46, 49, 138], [24, 26, 50, 624], [23, 27, 50, 621], [22, 28, 50, 616], [21, 29, 50, 609], [20, 30, 50, 600], [18, 32, 50, 576], [17, 33, 50, 561], [16, 34, 50, 544], [15, 35, 50, 525], [14, 36, 50, 504], [12, 38, 50, 456], [11, 39, 50, 429], [10, 40, 50, 400], [8, 42, 50, 336], [6, 44, 50, 264], [5, 45, 50, 225], [4, 46, 50, 184], [2, 48, 50, 96], [25, 26, 51, 650], [24, 27, 51, 648], [23, 28, 51, 644], [22, 29, 51, 638], [21, 30, 51, 630], [20, 31, 51, 620], [19, 32, 51, 608], [18, 33, 51, 594], [16, 35, 51, 560], [15, 36, 51, 540], [14, 37, 51, 518], [13, 38, 51, 494], [12, 39, 51, 468], [11, 40, 51, 440], [10, 41, 51, 410], [9, 42, 51, 378], [8, 43, 51, 344], [7, 44, 51, 308], [6, 45, 51, 270], [5, 46, 51, 230], [4, 47, 51, 188], [3, 48, 51, 144], [2, 49, 51, 98], [25, 27, 52, 675], [24, 28, 52, 672], [22, 30, 52, 660], [21, 31, 52, 651], [20, 32, 52, 640], [19, 33, 52, 627], [18, 34, 52, 612], [17, 35, 52, 595], [16, 36, 52, 576], [14, 38, 52, 532], [12, 40, 52, 480], [10, 42, 52, 420], [8, 44, 52, 352], [7, 45, 52, 315], [6, 46, 52, 276], [4, 48, 52, 192], [3, 49, 52, 147], [2, 50, 52, 100], [26, 27, 53, 702], [25, 28, 53, 700], [24, 29, 53, 696], [23, 30, 53, 690], [22, 31, 53, 682], [21, 32, 53, 672], [20, 33, 53, 660], [19, 34, 53, 646], [18, 35, 53, 630], [17, 36, 53, 612], [16, 37, 53, 592], [15, 38, 53, 570], [14, 39, 53, 546], [13, 40, 53, 520], [12, 41, 53, 492], [11, 42, 53, 462], [10, 43, 53, 430], [9, 44, 53, 396], [8, 45, 53, 360], [7, 46, 53, 322], [6, 47, 53, 282], [5, 48, 53, 240], [4, 49, 53, 196], [3, 50, 53, 150], [2, 51, 53, 102], [26, 28, 54, 728], [24, 30, 54, 720], [22, 32, 54, 704], [21, 33, 54, 693], [20, 34, 54, 680], [18, 36, 54, 648], [16, 38, 54, 608], [15, 39, 54, 585], [14, 40, 54, 560], [12, 42, 54, 504], [10, 44, 54, 440], [9, 45, 54, 405], [8, 46, 54, 368], [6, 48, 54, 288], [5, 49, 54, 245], [4, 50, 54, 200], [3, 51, 54, 153], [2, 52, 54, 104], [27, 28, 55, 756], [26, 29, 55, 754], [25, 30, 55, 750], [24, 31, 55, 744], [23, 32, 55, 736], [22, 33, 55, 726], [21, 34, 55, 714], [20, 35, 55, 700], [19, 36, 55, 684], [18, 37, 55, 666], [17, 38, 55, 646], [16, 39, 55, 624], [15, 40, 55, 600], [14, 41, 55, 574], [13, 42, 55, 546], [12, 43, 55, 516], [10, 45, 55, 450], [9, 46, 55, 414], [8, 47, 55, 376], [7, 48, 55, 336], [6, 49, 55, 294], [5, 50, 55, 250], [4, 51, 55, 204], [3, 52, 55, 156], [27, 29, 56, 783], [26, 30, 56, 780], [24, 32, 56, 768], [23, 33, 56, 759], [22, 34, 56, 748], [21, 35, 56, 735], [20, 36, 56, 720], [18, 38, 56, 684], [17, 39, 56, 663], [16, 40, 56, 640], [14, 42, 56, 588], [12, 44, 56, 528], [11, 45, 56, 495], [10, 46, 56, 460], [8, 48, 56, 384], [6, 50, 56, 300], [5, 51, 56, 255], [4, 52, 56, 208], [2, 54, 56, 108], [28, 29, 57, 812], [27, 30, 57, 810], [26, 31, 57, 806], [25, 32, 57, 800], [24, 33, 57, 792], [23, 34, 57, 782], [22, 35, 57, 770], [21, 36, 57, 756], [20, 37, 57, 740], [18, 39, 57, 702], [17, 40, 57, 680], [16, 41, 57, 656], [15, 42, 57, 630], [14, 43, 57, 602], [13, 44, 57, 572], [12, 45, 57, 540], [11, 46, 57, 506], [10, 47, 57, 470], [9, 48, 57, 432], [8, 49, 57, 392], [7, 50, 57, 350], [6, 51, 57, 306], [5, 52, 57, 260], [3, 54, 57, 162], [2, 55, 57, 110], [28, 30, 58, 840], [26, 32, 58, 832], [25, 33, 58, 825], [24, 34, 58, 816], [22, 36, 58, 792], [20, 38, 58, 760], [19, 39, 58, 741], [18, 40, 58, 720], [16, 42, 58, 672], [14, 44, 58, 616], [13, 45, 58, 585], [12, 46, 58, 552], [10, 48, 58, 480], [9, 49, 58, 441], [8, 50, 58, 400], [7, 51, 58, 357], [6, 52, 58, 312], [4, 54, 58, 216], [3, 55, 58, 165], [2, 56, 58, 112], [29, 30, 59, 870], [28, 31, 59, 868], [27, 32, 59, 864], [26, 33, 59, 858], [25, 34, 59, 850], [24, 35, 59, 840], [23, 36, 59, 828], [22, 37, 59, 814], [21, 38, 59, 798], [20, 39, 59, 780], [19, 40, 59, 760], [18, 41, 59, 738], [17, 42, 59, 714], [16, 43, 59, 688], [15, 44, 59, 660], [14, 45, 59, 630], [13, 46, 59, 598], [12, 47, 59, 564], [11, 48, 59, 528], [10, 49, 59, 490], [9, 50, 59, 450], [8, 51, 59, 408], [7, 52, 59, 364], [5, 54, 59, 270], [4, 55, 59, 220], [3, 56, 59, 168], [2, 57, 59, 114], [28, 32, 60, 896], [27, 33, 60, 891], [26, 34, 60, 884], [24, 36, 60, 864], [22, 38, 60, 836], [21, 39, 60, 819], [20, 40, 60, 800], [18, 42, 60, 756], [16, 44, 60, 704], [15, 45, 60, 675], [14, 46, 60, 644], [12, 48, 60, 576], [11, 49, 60, 539], [10, 50, 60, 500], [9, 51, 60, 459], [8, 52, 60, 416], [6, 54, 60, 324], [5, 55, 60, 275], [4, 56, 60, 224], [3, 57, 60, 171], [2, 58, 60, 116], [30, 31, 61, 930], [29, 32, 61, 928], [28, 33, 61, 924], [27, 34, 61, 918], [26, 35, 61, 910], [25, 36, 61, 900], [24, 37, 61, 888], [23, 38, 61, 874], [22, 39, 61, 858], [21, 40, 61, 840], [20, 41, 61, 820], [19, 42, 61, 798], [18, 43, 61, 774], [17, 44, 61, 748], [16, 45, 61, 720], [15, 46, 61, 690], [13, 48, 61, 624], [12, 49, 61, 588], [11, 50, 61, 550], [10, 51, 61, 510], [9, 52, 61, 468], [7, 54, 61, 378], [6, 55, 61, 330], [5, 56, 61, 280], [4, 57, 61, 228], [3, 58, 61, 174], [30, 32, 62, 960], [29, 33, 62, 957], [28, 34, 62, 952], [27, 35, 62, 945], [26, 36, 62, 936], [24, 38, 62, 912], [23, 39, 62, 897], [22, 40, 62, 880], [20, 42, 62, 840], [18, 44, 62, 792], [17, 45, 62, 765], [16, 46, 62, 736], [14, 48, 62, 672], [13, 49, 62, 637], [12, 50, 62, 600], [11, 51, 62, 561], [10, 52, 62, 520], [8, 54, 62, 432], [7, 55, 62, 385], [6, 56, 62, 336], [5, 57, 62, 285], [4, 58, 62, 232], [2, 60, 62, 120], [31, 32, 63, 992], [30, 33, 63, 990], [29, 34, 63, 986], [28, 35, 63, 980], [27, 36, 63, 972], [26, 37, 63, 962], [25, 38, 63, 950], [24, 39, 63, 936], [23, 40, 63, 920], [22, 41, 63, 902], [21, 42, 63, 882], [20, 43, 63, 860], [19, 44, 63, 836], [18, 45, 63, 810], [17, 46, 63, 782], [15, 48, 63, 720], [13, 50, 63, 650], [12, 51, 63, 612], [11, 52, 63, 572], [9, 54, 63, 486], [8, 55, 63, 440], [7, 56, 63, 392], [6, 57, 63, 342], [5, 58, 63, 290], [3, 60, 63, 180], [30, 34, 64, 1020], [28, 36, 64, 1008], [26, 38, 64, 988], [25, 39, 64, 975], [24, 40, 64, 960], [22, 42, 64, 924], [20, 44, 64, 880], [19, 45, 64, 855], [18, 46, 64, 828], [16, 48, 64, 768], [15, 49, 64, 735], [14, 50, 64, 700], [13, 51, 64, 663], [12, 52, 64, 624], [10, 54, 64, 540], [9, 55, 64, 495], [8, 56, 64, 448], [7, 57, 64, 399], [6, 58, 64, 348], [4, 60, 64, 240], [2, 62, 64, 124], [32, 33, 65, 1056], [31, 34, 65, 1054], [30, 35, 65, 1050], [29, 36, 65, 1044], [28, 37, 65, 1036], [27, 38, 65, 1026], [26, 39, 65, 1014], [25, 40, 65, 1000], [24, 41, 65, 984], [23, 42, 65, 966], [22, 43, 65, 946], [21, 44, 65, 924], [20, 45, 65, 900], [19, 46, 65, 874], [17, 48, 65, 816], [16, 49, 65, 784], [15, 50, 65, 750], [14, 51, 65, 714], [11, 54, 65, 594], [10, 55, 65, 550], [9, 56, 65, 504], [8, 57, 65, 456], [7, 58, 65, 406], [5, 60, 65, 300], [3, 62, 65, 186], [2, 63, 65, 126], [32, 34, 66, 1088], [30, 36, 66, 1080], [28, 38, 66, 1064], [27, 39, 66, 1053], [26, 40, 66, 1040], [24, 42, 66, 1008], [22, 44, 66, 968], [21, 45, 66, 945], [20, 46, 66, 920], [18, 48, 66, 864], [16, 50, 66, 800], [15, 51, 66, 765], [14, 52, 66, 728], [12, 54, 66, 648], [10, 56, 66, 560], [9, 57, 66, 513], [8, 58, 66, 464], [6, 60, 66, 360], [4, 62, 66, 248], [3, 63, 66, 189], [2, 64, 66, 128], [33, 34, 67, 1122], [32, 35, 67, 1120], [31, 36, 67, 1116], [30, 37, 67, 1110], [29, 38, 67, 1102], [28, 39, 67, 1092], [27, 40, 67, 1080], [26, 41, 67, 1066], [25, 42, 67, 1050], [24, 43, 67, 1032], [23, 44, 67, 1012], [22, 45, 67, 990], [21, 46, 67, 966], [19, 48, 67, 912], [18, 49, 67, 882], [17, 50, 67, 850], [16, 51, 67, 816], [15, 52, 67, 780], [13, 54, 67, 702], [12, 55, 67, 660], [11, 56, 67, 616], [10, 57, 67, 570], [9, 58, 67, 522], [7, 60, 67, 420], [5, 62, 67, 310], [4, 63, 67, 252], [3, 64, 67, 192], [2, 65, 67, 130], [33, 35, 68, 1155], [32, 36, 68, 1152], [30, 38, 68, 1140], [29, 39, 68, 1131], [28, 40, 68, 1120], [26, 42, 68, 1092], [24, 44, 68, 1056], [23, 45, 68, 1035], [22, 46, 68, 1012], [20, 48, 68, 960], [18, 50, 68, 900], [16, 52, 68, 832], [14, 54, 68, 756], [13, 55, 68, 715], [12, 56, 68, 672], [11, 57, 68, 627], [10, 58, 68, 580], [8, 60, 68, 480], [6, 62, 68, 372], [5, 63, 68, 315], [4, 64, 68, 256], [3, 65, 68, 195], [2, 66, 68, 132], [34, 35, 69, 1190], [33, 36, 69, 1188], [32, 37, 69, 1184], [31, 38, 69, 1178], [30, 39, 69, 1170], [29, 40, 69, 1160], [28, 41, 69, 1148], [27, 42, 69, 1134], [26, 43, 69, 1118], [25, 44, 69, 1100], [24, 45, 69, 1080], [21, 48, 69, 1008], [20, 49, 69, 980], [19, 50, 69, 950], [18, 51, 69, 918], [17, 52, 69, 884], [15, 54, 69, 810], [14, 55, 69, 770], [13, 56, 69, 728], [12, 57, 69, 684], [11, 58, 69, 638], [9, 60, 69, 540], [7, 62, 69, 434], [6, 63, 69, 378], [5, 64, 69, 320], [4, 65, 69, 260], [3, 66, 69, 198], [34, 36, 70, 1224], [32, 38, 70, 1216], [30, 40, 70, 1200], [28, 42, 70, 1176], [26, 44, 70, 1144], [25, 45, 70, 1125], [24, 46, 70, 1104], [22, 48, 70, 1056], [20, 50, 70, 1000], [19, 51, 70, 969], [18, 52, 70, 936], [16, 54, 70, 864], [15, 55, 70, 825], [14, 56, 70, 784], [13, 57, 70, 741], [12, 58, 70, 696], [10, 60, 70, 600], [8, 62, 70, 496], [7, 63, 70, 441], [6, 64, 70, 384], [5, 65, 70, 325], [4, 66, 70, 264], [2, 68, 70, 136], [35, 36, 71, 1260], [34, 37, 71, 1258], [33, 38, 71, 1254], [32, 39, 71, 1248], [31, 40, 71, 1240], [30, 41, 71, 1230], [29, 42, 71, 1218], [28, 43, 71, 1204], [27, 44, 71, 1188], [26, 45, 71, 1170], [25, 46, 71, 1150], [23, 48, 71, 1104], [22, 49, 71, 1078], [21, 50, 71, 1050], [20, 51, 71, 1020], [19, 52, 71, 988], [17, 54, 71, 918], [16, 55, 71, 880], [15, 56, 71, 840], [14, 57, 71, 798], [13, 58, 71, 754], [11, 60, 71, 660], [9, 62, 71, 558], [8, 63, 71, 504], [7, 64, 71, 448], [6, 65, 71, 390], [5, 66, 71, 330], [3, 68, 71, 204], [2, 69, 71, 138], [34, 38, 72, 1292], [32, 40, 72, 1280], [30, 42, 72, 1260], [28, 44, 72, 1232], [27, 45, 72, 1215], [26, 46, 72, 1196], [24, 48, 72, 1152], [22, 50, 72, 1100], [21, 51, 72, 1071], [20, 52, 72, 1040], [18, 54, 72, 972], [17, 55, 72, 935], [16, 56, 72, 896], [15, 57, 72, 855], [14, 58, 72, 812], [12, 60, 72, 720], [10, 62, 72, 620], [9, 63, 72, 567], [8, 64, 72, 512], [7, 65, 72, 455], [6, 66, 72, 396], [4, 68, 72, 272], [3, 69, 72, 207], [2, 70, 72, 140], [36, 37, 73, 1332], [35, 38, 73, 1330], [34, 39, 73, 1326], [33, 40, 73, 1320], [32, 41, 73, 1312], [31, 42, 73, 1302], [29, 44, 73, 1276], [28, 45, 73, 1260], [27, 46, 73, 1242], [25, 48, 73, 1200], [24, 49, 73, 1176], [23, 50, 73, 1150], [22, 51, 73, 1122], [21, 52, 73, 1092], [19, 54, 73, 1026], [18, 55, 73, 990], [17, 56, 73, 952], [16, 57, 73, 912], [15, 58, 73, 870], [13, 60, 73, 780], [11, 62, 73, 682], [10, 63, 73, 630], [9, 64, 73, 576], [8, 65, 73, 520], [7, 66, 73, 462], [5, 68, 73, 340], [4, 69, 73, 276], [3, 70, 73, 210], [36, 38, 74, 1368], [35, 39, 74, 1365], [34, 40, 74, 1360], [32, 42, 74, 1344], [30, 44, 74, 1320], [28, 46, 74, 1288], [26, 48, 74, 1248], [24, 50, 74, 1200], [23, 51, 74, 1173], [22, 52, 74, 1144], [20, 54, 74, 1080], [18, 56, 74, 1008], [17, 57, 74, 969], [16, 58, 74, 928], [14, 60, 74, 840], [12, 62, 74, 744], [11, 63, 74, 693], [10, 64, 74, 640], [9, 65, 74, 585], [8, 66, 74, 528], [6, 68, 74, 408], [5, 69, 74, 345], [4, 70, 74, 280], [2, 72, 74, 144], [37, 38, 75, 1406], [36, 39, 75, 1404], [35, 40, 75, 1400], [34, 41, 75, 1394], [33, 42, 75, 1386], [31, 44, 75, 1364], [30, 45, 75, 1350], [29, 46, 75, 1334], [27, 48, 75, 1296], [24, 51, 75, 1224], [23, 52, 75, 1196], [21, 54, 75, 1134], [20, 55, 75, 1100], [19, 56, 75, 1064], [18, 57, 75, 1026], [17, 58, 75, 986], [15, 60, 75, 900], [13, 62, 75, 806], [12, 63, 75, 756], [11, 64, 75, 704], [10, 65, 75, 650], [9, 66, 75, 594], [7, 68, 75, 476], [6, 69, 75, 414], [5, 70, 75, 350], [3, 72, 75, 216], [36, 40, 76, 1440], [34, 42, 76, 1428], [32, 44, 76, 1408], [30, 46, 76, 1380], [28, 48, 76, 1344], [27, 49, 76, 1323], [26, 50, 76, 1300], [25, 51, 76, 1275], [24, 52, 76, 1248], [22, 54, 76, 1188], [21, 55, 76, 1155], [20, 56, 76, 1120], [18, 58, 76, 1044], [16, 60, 76, 960], [14, 62, 76, 868], [13, 63, 76, 819], [12, 64, 76, 768], [11, 65, 76, 715], [10, 66, 76, 660], [8, 68, 76, 544], [7, 69, 76, 483], [6, 70, 76, 420], [4, 72, 76, 288], [2, 74, 76, 148], [38, 39, 77, 1482], [37, 40, 77, 1480], [36, 41, 77, 1476], [35, 42, 77, 1470], [33, 44, 77, 1452], [32, 45, 77, 1440], [31, 46, 77, 1426], [29, 48, 77, 1392], [27, 50, 77, 1350], [26, 51, 77, 1326], [25, 52, 77, 1300], [23, 54, 77, 1242], [21, 56, 77, 1176], [20, 57, 77, 1140], [19, 58, 77, 1102], [17, 60, 77, 1020], [15, 62, 77, 930], [14, 63, 77, 882], [13, 64, 77, 832], [12, 65, 77, 780], [11, 66, 77, 726], [9, 68, 77, 612], [8, 69, 77, 552], [7, 70, 77, 490], [5, 72, 77, 360], [3, 74, 77, 222], [2, 75, 77, 150], [38, 40, 78, 1520], [36, 42, 78, 1512], [34, 44, 78, 1496], [33, 45, 78, 1485], [32, 46, 78, 1472], [30, 48, 78, 1440], [28, 50, 78, 1400], [27, 51, 78, 1377], [24, 54, 78, 1296], [22, 56, 78, 1232], [21, 57, 78, 1197], [20, 58, 78, 1160], [18, 60, 78, 1080], [16, 62, 78, 992], [15, 63, 78, 945], [14, 64, 78, 896], [12, 66, 78, 792], [10, 68, 78, 680], [9, 69, 78, 621], [8, 70, 78, 560], [6, 72, 78, 432], [4, 74, 78, 296], [3, 75, 78, 225], [2, 76, 78, 152], [39, 40, 79, 1560], [37, 42, 79, 1554], [35, 44, 79, 1540], [34, 45, 79, 1530], [33, 46, 79, 1518], [31, 48, 79, 1488], [30, 49, 79, 1470], [29, 50, 79, 1450], [28, 51, 79, 1428], [27, 52, 79, 1404], [25, 54, 79, 1350], [24, 55, 79, 1320], [23, 56, 79, 1288], [22, 57, 79, 1254], [21, 58, 79, 1218], [19, 60, 79, 1140], [17, 62, 79, 1054], [16, 63, 79, 1008], [15, 64, 79, 960], [14, 65, 79, 910], [13, 66, 79, 858], [11, 68, 79, 748], [10, 69, 79, 690], [9, 70, 79, 630], [7, 72, 79, 504], [5, 74, 79, 370], [4, 75, 79, 300], [3, 76, 79, 228], [2, 77, 79, 154], [38, 42, 80, 1596], [36, 44, 80, 1584], [35, 45, 80, 1575], [34, 46, 80, 1564], [32, 48, 80, 1536], [30, 50, 80, 1500], [28, 52, 80, 1456], [26, 54, 80, 1404], [24, 56, 80, 1344], [23, 57, 80, 1311], [22, 58, 80, 1276], [20, 60, 80, 1200], [18, 62, 80, 1116], [17, 63, 80, 1071], [15, 65, 80, 975], [14, 66, 80, 924], [12, 68, 80, 816], [11, 69, 80, 759], [10, 70, 80, 700], [8, 72, 80, 576], [6, 74, 80, 444], [5, 75, 80, 375], [4, 76, 80, 304], [3, 77, 80, 231], [2, 78, 80, 156], [39, 42, 81, 1638], [37, 44, 81, 1628], [36, 45, 81, 1620], [35, 46, 81, 1610], [33, 48, 81, 1584], [32, 49, 81, 1568], [31, 50, 81, 1550], [30, 51, 81, 1530], [29, 52, 81, 1508], [27, 54, 81, 1458], [26, 55, 81, 1430], [25, 56, 81, 1400], [24, 57, 81, 1368], [23, 58, 81, 1334], [21, 60, 81, 1260], [19, 62, 81, 1178], [18, 63, 81, 1134], [17, 64, 81, 1088], [16, 65, 81, 1040], [15, 66, 81, 990], [13, 68, 81, 884], [12, 69, 81, 828], [11, 70, 81, 770], [9, 72, 81, 648], [7, 74, 81, 518], [6, 75, 81, 450], [5, 76, 81, 380], [4, 77, 81, 308], [3, 78, 81, 234], [40, 42, 82, 1680], [38, 44, 82, 1672], [36, 46, 82, 1656], [34, 48, 82, 1632], [33, 49, 82, 1617], [32, 50, 82, 1600], [30, 52, 82, 1560], [28, 54, 82, 1512], [27, 55, 82, 1485], [26, 56, 82, 1456], [25, 57, 82, 1425], [24, 58, 82, 1392], [22, 60, 82, 1320], [20, 62, 82, 1240], [19, 63, 82, 1197], [18, 64, 82, 1152], [17, 65, 82, 1105], [16, 66, 82, 1056], [14, 68, 82, 952], [13, 69, 82, 897], [12, 70, 82, 840], [10, 72, 82, 720], [8, 74, 82, 592], [7, 75, 82, 525], [6, 76, 82, 456], [5, 77, 82, 385], [4, 78, 82, 312], [2, 80, 82, 160], [39, 44, 83, 1716], [38, 45, 83, 1710], [37, 46, 83, 1702], [35, 48, 83, 1680], [33, 50, 83, 1650], [32, 51, 83, 1632], [31, 52, 83, 1612], [29, 54, 83, 1566], [28, 55, 83, 1540], [27, 56, 83, 1512], [26, 57, 83, 1482], [25, 58, 83, 1450], [23, 60, 83, 1380], [21, 62, 83, 1302], [20, 63, 83, 1260], [19, 64, 83, 1216], [18, 65, 83, 1170], [17, 66, 83, 1122], [15, 68, 83, 1020], [14, 69, 83, 966], [13, 70, 83, 910], [11, 72, 83, 792], [9, 74, 83, 666], [8, 75, 83, 600], [7, 76, 83, 532], [6, 77, 83, 462], [5, 78, 83, 390], [3, 80, 83, 240], [2, 81, 83, 162], [40, 44, 84, 1760], [39, 45, 84, 1755], [38, 46, 84, 1748], [36, 48, 84, 1728], [34, 50, 84, 1700], [32, 52, 84, 1664], [30, 54, 84, 1620], [28, 56, 84, 1568], [27, 57, 84, 1539], [26, 58, 84, 1508], [24, 60, 84, 1440], [22, 62, 84, 1364], [21, 63, 84, 1323], [20, 64, 84, 1280], [18, 66, 84, 1188], [16, 68, 84, 1088], [15, 69, 84, 1035], [14, 70, 84, 980], [12, 72, 84, 864], [10, 74, 84, 740], [9, 75, 84, 675], [8, 76, 84, 608], [7, 77, 84, 539], [6, 78, 84, 468], [4, 80, 84, 320], [3, 81, 84, 243], [2, 82, 84, 164], [40, 45, 85, 1800], [39, 46, 85, 1794], [37, 48, 85, 1776], [36, 49, 85, 1764], [35, 50, 85, 1750], [33, 52, 85, 1716], [31, 54, 85, 1674], [30, 55, 85, 1650], [29, 56, 85, 1624], [28, 57, 85, 1596], [27, 58, 85, 1566], [25, 60, 85, 1500], [23, 62, 85, 1426], [22, 63, 85, 1386], [21, 64, 85, 1344], [20, 65, 85, 1300], [19, 66, 85, 1254], [16, 69, 85, 1104], [15, 70, 85, 1050], [13, 72, 85, 936], [11, 74, 85, 814], [10, 75, 85, 750], [9, 76, 85, 684], [8, 77, 85, 616], [7, 78, 85, 546], [5, 80, 85, 400], [4, 81, 85, 324], [3, 82, 85, 246], [42, 44, 86, 1848], [38, 48, 86, 1824], [36, 50, 86, 1800], [34, 52, 86, 1768], [32, 54, 86, 1728], [30, 56, 86, 1680], [28, 58, 86, 1624], [26, 60, 86, 1560], [24, 62, 86, 1488], [23, 63, 86, 1449], [22, 64, 86, 1408], [21, 65, 86, 1365], [20, 66, 86, 1320], [18, 68, 86, 1224], [17, 69, 86, 1173], [16, 70, 86, 1120], [14, 72, 86, 1008], [12, 74, 86, 888], [11, 75, 86, 825], [10, 76, 86, 760], [9, 77, 86, 693], [8, 78, 86, 624], [6, 80, 86, 480], [5, 81, 86, 405], [4, 82, 86, 328], [2, 84, 86, 168], [42, 45, 87, 1890], [39, 48, 87, 1872], [37, 50, 87, 1850], [36, 51, 87, 1836], [35, 52, 87, 1820], [33, 54, 87, 1782], [32, 55, 87, 1760], [31, 56, 87, 1736], [30, 57, 87, 1710], [27, 60, 87, 1620], [25, 62, 87, 1550], [24, 63, 87, 1512], [23, 64, 87, 1472], [22, 65, 87, 1430], [21, 66, 87, 1386], [19, 68, 87, 1292], [18, 69, 87, 1242], [17, 70, 87, 1190], [15, 72, 87, 1080], [13, 74, 87, 962], [12, 75, 87, 900], [11, 76, 87, 836], [10, 77, 87, 770], [9, 78, 87, 702], [7, 80, 87, 560], [6, 81, 87, 486], [5, 82, 87, 410], [3, 84, 87, 252], [2, 85, 87, 170], [42, 46, 88, 1932], [40, 48, 88, 1920], [36, 52, 88, 1872], [34, 54, 88, 1836], [32, 56, 88, 1792], [30, 58, 88, 1740], [28, 60, 88, 1680], [26, 62, 88, 1612], [25, 63, 88, 1575], [24, 64, 88, 1536], [22, 66, 88, 1452], [20, 68, 88, 1360], [19, 69, 88, 1311], [18, 70, 88, 1260], [16, 72, 88, 1152], [14, 74, 88, 1036], [13, 75, 88, 975], [12, 76, 88, 912], [10, 78, 88, 780], [8, 80, 88, 640], [7, 81, 88, 567], [6, 82, 88, 492], [4, 84, 88, 336], [3, 85, 88, 255], [2, 86, 88, 172], [44, 45, 89, 1980], [40, 49, 89, 1960], [39, 50, 89, 1950], [38, 51, 89, 1938], [37, 52, 89, 1924], [35, 54, 89, 1890], [33, 56, 89, 1848], [32, 57, 89, 1824], [31, 58, 89, 1798], [29, 60, 89, 1740], [27, 62, 89, 1674], [26, 63, 89, 1638], [25, 64, 89, 1600], [24, 65, 89, 1560], [23, 66, 89, 1518], [21, 68, 89, 1428], [20, 69, 89, 1380], [19, 70, 89, 1330], [17, 72, 89, 1224], [15, 74, 89, 1110], [14, 75, 89, 1050], [13, 76, 89, 988], [12, 77, 89, 924], [11, 78, 89, 858], [9, 80, 89, 720], [8, 81, 89, 648], [7, 82, 89, 574], [5, 84, 89, 420], [4, 85, 89, 340], [3, 86, 89, 258], [2, 87, 89, 174], [42, 48, 90, 2016], [36, 54, 90, 1944], [34, 56, 90, 1904], [32, 58, 90, 1856], [30, 60, 90, 1800], [28, 62, 90, 1736], [26, 64, 90, 1664], [24, 66, 90, 1584], [22, 68, 90, 1496], [21, 69, 90, 1449], [20, 70, 90, 1400], [18, 72, 90, 1296], [16, 74, 90, 1184], [15, 75, 90, 1125], [14, 76, 90, 1064], [12, 78, 90, 936], [10, 80, 90, 800], [8, 82, 90, 656], [6, 84, 90, 504], [5, 85, 90, 425], [4, 86, 90, 344], [3, 87, 90, 261], [2, 88, 90, 176], [45, 46, 91, 2070], [40, 51, 91, 2040], [36, 55, 91, 1980], [35, 56, 91, 1960], [34, 57, 91, 1938], [33, 58, 91, 1914], [31, 60, 91, 1860], [29, 62, 91, 1798], [28, 63, 91, 1764], [27, 64, 91, 1728], [25, 66, 91, 1650], [23, 68, 91, 1564], [22, 69, 91, 1518], [21, 70, 91, 1470], [19, 72, 91, 1368], [17, 74, 91, 1258], [16, 75, 91, 1200], [15, 76, 91, 1140], [14, 77, 91, 1078], [13, 78, 91, 1014], [11, 80, 91, 880], [10, 81, 91, 810], [9, 82, 91, 738], [7, 84, 91, 588], [6, 85, 91, 510], [5, 86, 91, 430], [4, 87, 91, 348], [3, 88, 91, 264], [44, 48, 92, 2112], [42, 50, 92, 2100], [40, 52, 92, 2080], [38, 54, 92, 2052], [36, 56, 92, 2016], [34, 58, 92, 1972], [32, 60, 92, 1920], [30, 62, 92, 1860], [28, 64, 92, 1792], [27, 65, 92, 1755], [26, 66, 92, 1716], [24, 68, 92, 1632], [22, 70, 92, 1540], [20, 72, 92, 1440], [18, 74, 92, 1332], [17, 75, 92, 1275], [16, 76, 92, 1216], [15, 77, 92, 1155], [14, 78, 92, 1092], [12, 80, 92, 960], [11, 81, 92, 891], [10, 82, 92, 820], [8, 84, 92, 672], [7, 85, 92, 595], [6, 86, 92, 516], [5, 87, 92, 435], [4, 88, 92, 352], [2, 90, 92, 180], [45, 48, 93, 2160], [42, 51, 93, 2142], [36, 57, 93, 2052], [35, 58, 93, 2030], [33, 60, 93, 1980], [30, 63, 93, 1890], [29, 64, 93, 1856], [28, 65, 93, 1820], [27, 66, 93, 1782], [25, 68, 93, 1700], [24, 69, 93, 1656], [23, 70, 93, 1610], [21, 72, 93, 1512], [19, 74, 93, 1406], [18, 75, 93, 1350], [17, 76, 93, 1292], [16, 77, 93, 1232], [15, 78, 93, 1170], [13, 80, 93, 1040], [12, 81, 93, 972], [11, 82, 93, 902], [9, 84, 93, 756], [8, 85, 93, 680], [7, 86, 93, 602], [6, 87, 93, 522], [5, 88, 93, 440], [3, 90, 93, 270], [2, 91, 93, 182], [45, 49, 94, 2205], [44, 50, 94, 2200], [42, 52, 94, 2184], [40, 54, 94, 2160], [39, 55, 94, 2145], [34, 60, 94, 2040], [32, 62, 94, 1984], [30, 64, 94, 1920], [28, 66, 94, 1848], [26, 68, 94, 1768], [25, 69, 94, 1725], [24, 70, 94, 1680], [22, 72, 94, 1584], [20, 74, 94, 1480], [19, 75, 94, 1425], [18, 76, 94, 1368], [16, 78, 94, 1248], [14, 80, 94, 1120], [13, 81, 94, 1053], [12, 82, 94, 984], [10, 84, 94, 840], [9, 85, 94, 765], [8, 86, 94, 688], [7, 87, 94, 609], [6, 88, 94, 528], [4, 90, 94, 360], [3, 91, 94, 273], [2, 92, 94, 184], [44, 51, 95, 2244], [40, 55, 95, 2200], [39, 56, 95, 2184], [35, 60, 95, 2100], [33, 62, 95, 2046], [32, 63, 95, 2016], [31, 64, 95, 1984], [30, 65, 95, 1950], [29, 66, 95, 1914], [27, 68, 95, 1836], [26, 69, 95, 1794], [25, 70, 95, 1750], [23, 72, 95, 1656], [21, 74, 95, 1554], [20, 75, 95, 1500], [18, 77, 95, 1386], [17, 78, 95, 1326], [15, 80, 95, 1200], [14, 81, 95, 1134], [13, 82, 95, 1066], [11, 84, 95, 924], [10, 85, 95, 850], [9, 86, 95, 774], [8, 87, 95, 696], [7, 88, 95, 616], [5, 90, 95, 450], [4, 91, 95, 364], [3, 92, 95, 276], [2, 93, 95, 186], [42, 54, 96, 2268], [40, 56, 96, 2240], [36, 60, 96, 2160], [34, 62, 96, 2108], [30, 66, 96, 1980], [28, 68, 96, 1904], [26, 70, 96, 1820], [24, 72, 96, 1728], [22, 74, 96, 1628], [21, 75, 96, 1575], [20, 76, 96, 1520], [18, 78, 96, 1404], [16, 80, 96, 1280], [15, 81, 96, 1215], [14, 82, 96, 1148], [12, 84, 96, 1008], [11, 85, 96, 935], [10, 86, 96, 860], [9, 87, 96, 783], [8, 88, 96, 704], [6, 90, 96, 540], [5, 91, 96, 455], [4, 92, 96, 368], [3, 93, 96, 279], [2, 94, 96, 188], [48, 49, 97, 2352], [45, 52, 97, 2340], [40, 57, 97, 2280], [34, 63, 97, 2142], [33, 64, 97, 2112], [32, 65, 97, 2080], [31, 66, 97, 2046], [29, 68, 97, 1972], [28, 69, 97, 1932], [27, 70, 97, 1890], [25, 72, 97, 1800], [23, 74, 97, 1702], [22, 75, 97, 1650], [21, 76, 97, 1596], [20, 77, 97, 1540], [19, 78, 97, 1482], [17, 80, 97, 1360], [16, 81, 97, 1296], [15, 82, 97, 1230], [13, 84, 97, 1092], [12, 85, 97, 1020], [11, 86, 97, 946], [10, 87, 97, 870], [9, 88, 97, 792], [7, 90, 97, 630], [6, 91, 97, 546], [5, 92, 97, 460], [4, 93, 97, 372], [3, 94, 97, 282], [2, 95, 97, 190], [48, 50, 98, 2400], [42, 56, 98, 2352], [38, 60, 98, 2280], [35, 63, 98, 2205], [34, 64, 98, 2176], [33, 65, 98, 2145], [32, 66, 98, 2112], [30, 68, 98, 2040], [28, 70, 98, 1960], [26, 72, 98, 1872], [24, 74, 98, 1776], [23, 75, 98, 1725], [22, 76, 98, 1672], [21, 77, 98, 1617], [20, 78, 98, 1560], [18, 80, 98, 1440], [17, 81, 98, 1377], [16, 82, 98, 1312], [14, 84, 98, 1176], [13, 85, 98, 1105], [12, 86, 98, 1032], [11, 87, 98, 957], [10, 88, 98, 880], [8, 90, 98, 720], [7, 91, 98, 637], [6, 92, 98, 552], [5, 93, 98, 465], [4, 94, 98, 376], [3, 95, 98, 285], [2, 96, 98, 192], [39, 60, 99, 2340], [36, 63, 99, 2268], [35, 64, 99, 2240], [31, 68, 99, 2108], [30, 69, 99, 2070], [29, 70, 99, 2030], [27, 72, 99, 1944], [25, 74, 99, 1850], [24, 75, 99, 1800], [23, 76, 99, 1748], [21, 78, 99, 1638], [19, 80, 99, 1520], [18, 81, 99, 1458], [17, 82, 99, 1394], [15, 84, 99, 1260], [14, 85, 99, 1190], [13, 86, 99, 1118], [12, 87, 99, 1044], [11, 88, 99, 968], [9, 90, 99, 810], [8, 91, 99, 728], [7, 92, 99, 644], [6, 93, 99, 558], [5, 94, 99, 470], [4, 95, 99, 380], [3, 96, 99, 288], [40, 60, 100, 2400], [34, 66, 100, 2244], [32, 68, 100, 2176], [30, 70, 100, 2100], [28, 72, 100, 2016], [26, 74, 100, 1924], [24, 76, 100, 1824], [22, 78, 100, 1716], [20, 80, 100, 1600], [19, 81, 100, 1539], [18, 82, 100, 1476], [16, 84, 100, 1344], [15, 85, 100, 1275], [14, 86, 100, 1204], [13, 87, 100, 1131], [12, 88, 100, 1056], [10, 90, 100, 900], [9, 91, 100, 819], [8, 92, 100, 736], [7, 93, 100, 651], [6, 94, 100, 564], [5, 95, 100, 475], [4, 96, 100, 384], [2, 98, 100, 196]]
?- time(s2(Q,100)).
% 19,968 inferences, 0.004 CPU in 0.005 seconds (95% CPU, 4437333 Lips)
Q = [[2, 9, 11, 18], [3, 8, 11, 24], [4, 7, 11, 28], [5, 6, 11, 30], [2, 15, 17, 30], [3, 14, 17, 42], [2, 21, 23, 42], [2, 25, 27, 50], [4, 13, 17, 52], [2, 27, 29, 54], [5, 12, 17, 60], [3, 20, 23, 60], [6, 11, 17, 66], [2, 33, 35, 66], [7, 10, 17, 70], [2, 35, 37, 70], [3, 24, 27, 72], [8, 9, 17, 72], [4, 19, 23, 76], [3, 26, 29, 78], [2, 39, 41, 78], [5, 18, 23, 90], [2, 45, 47, 90], [4, 23, 27, 92], [3, 32, 35, 96], [4, 25, 29, 100], [6, 17, 23, 102], [3, 34, 37, 102], [2, 51, 53, 102], [5, 22, 27, 110], [7, 16, 23, 112], [3, 38, 41, 114], [5, 24, 29, 120], [8, 15, 23, 120], [4, 31, 35, 124], [9, 14, 23, 126], [6, 21, 27, 126], [10, 13, 23, 130], [11, 12, 23, 132], [3, 44, 47, 132], [4, 33, 37, 132], [6, 23, 29, 138], [7, 20, 27, 140], [4, 37, 41, 148], [5, 30, 35, 150], [3, 50, 53, 150], [8, 19, 27, 152], [7, 22, 29, 154], [5, 32, 37, 160], [9, 18, 27, 162], [8, 21, 29, 168], [10, 17, 27, 170], [4, 43, 47, 172], [6, 29, 35, 174], [11, 16, 27, 176], [5, 36, 41, 180], [12, 15, 27, 180], [9, 20, 29, 180], [13, 14, 27, 182], [6, 31, 37, 186], [10, 19, 29, 190], [7, 28, 35, 196], [4, 49, 53, 196], [11, 18, 29, 198], [12, 17, 29, 204], [13, 16, 29, 208], [7, 30, 37, 210], [5, 42, 47, 210], [14, 15, 29, 210], [6, 35, 41, 210], [8, 27, 35, 216], [8, 29, 37, 232], [9, 26, 35, 234], [7, 34, 41, 238], [5, 48, 53, 240], [6, 41, 47, 246], [10, 25, 35, 250], [9, 28, 37, 252], [11, 24, 35, 264], [8, 33, 41, 264], [10, 27, 37, 270], [12, 23, 35, 276], [7, 40, 47, 280], [6, 47, 53, 282], [13, 22, 35, 286], [11, 26, 37, 286], [9, 32, 41, 288], [14, 21, 35, 294], [15, 20, 35, 300], [12, 25, 37, 300], [16, 19, 35, 304], [17, 18, 35, 306], [10, 31, 41, 310], [13, 24, 37, 312], [8, 39, 47, 312], [14, 23, 37, 322], [7, 46, 53, 322], [11, 30, 41, 330], [15, 22, 37, 330], [16, 21, 37, 336], [17, 20, 37, 340], [18, 19, 37, 342], [9, 38, 47, 342], [12, 29, 41, 348], [8, 45, 53, 360], [13, 28, 41, 364], [10, 37, 47, 370], [14, 27, 41, 378], [15, 26, 41, 390], [11, 36, 47, 396], [9, 44, 53, 396], [16, 25, 41, 400], [17, 24, 41, 408], [18, 23, 41, 414], [19, 22, 41, 418], [20, 21, 41, 420], [12, 35, 47, 420], [10, 43, 53, 430], [13, 34, 47, 442], [11, 42, 53, 462], [14, 33, 47, 462], [15, 32, 47, 480], [12, 41, 53, 492], [16, 31, 47, 496], [17, 30, 47, 510], [13, 40, 53, 520], [18, 29, 47, 522], [19, 28, 47, 532], [20, 27, 47, 540], [21, 26, 47, 546], [14, 39, 53, 546], [22, 25, 47, 550], [23, 24, 47, 552], [15, 38, 53, 570], [16, 37, 53, 592], [17, 36, 53, 612], [18, 35, 53, 630], [19, 34, 53, 646], [20, 33, 53, 660], [21, 32, 53, 672], [22, 31, 53, 682], [23, 30, 53, 690], [24, 29, 53, 696], [25, 28, 53, 700], [26, 27, 53, 702]]
?- time(s3(Q,100)).
% 22,249 inferences, 0.005 CPU in 0.005 seconds (93% CPU, 4343811 Lips)
Q = [[4, 7, 11, 28], [3, 8, 11, 24], [2, 9, 11, 18], [4, 13, 17, 52], [10, 13, 23, 130], [7, 16, 23, 112], [4, 19, 23, 76], [13, 14, 27, 182], [11, 16, 27, 176], [10, 17, 27, 170], [9, 18, 27, 162], [8, 19, 27, 152], [7, 20, 27, 140], [5, 22, 27, 110], [4, 23, 27, 92], [2, 25, 27, 50], [13, 16, 29, 208], [12, 17, 29, 204], [11, 18, 29, 198], [10, 19, 29, 190], [8, 21, 29, 168], [7, 22, 29, 154], [6, 23, 29, 138], [4, 25, 29, 100], [2, 27, 29, 54], [17, 18, 35, 306], [16, 19, 35, 304], [14, 21, 35, 294], [12, 23, 35, 276], [10, 25, 35, 250], [9, 26, 35, 234], [8, 27, 35, 216], [6, 29, 35, 174], [4, 31, 35, 124], [3, 32, 35, 96], [17, 20, 37, 340], [16, 21, 37, 336], [10, 27, 37, 270], [9, 28, 37, 252], [8, 29, 37, 232], [6, 31, 37, 186], [5, 32, 37, 160], [19, 22, 41, 418], [18, 23, 41, 414], [17, 24, 41, 408], [16, 25, 41, 400], [15, 26, 41, 390], [14, 27, 41, 378], [13, 28, 41, 364], [12, 29, 41, 348], [10, 31, 41, 310], [9, 32, 41, 288], [7, 34, 41, 238], [4, 37, 41, 148], [3, 38, 41, 114], [23, 24, 47, 552], [22, 25, 47, 550], [20, 27, 47, 540], [19, 28, 47, 532], [18, 29, 47, 522], [17, 30, 47, 510], [16, 31, 47, 496], [15, 32, 47, 480], [13, 34, 47, 442], [10, 37, 47, 370], [7, 40, 47, 280], [6, 41, 47, 246], [4, 43, 47, 172], [26, 27, 53, 702], [25, 28, 53, 700], [24, 29, 53, 696], [23, 30, 53, 690], [22, 31, 53, 682], [21, 32, 53, 672], [20, 33, 53, 660], [19, 34, 53, 646], [18, 35, 53, 630], [17, 36, 53, 612], [16, 37, 53, 592], [15, 38, 53, 570], [13, 40, 53, 520], [12, 41, 53, 492], [10, 43, 53, 430], [8, 45, 53, 360], [6, 47, 53, 282], [5, 48, 53, 240]]
?- time(s4(Q,100)).
% 22,258 inferences, 0.005 CPU in 0.005 seconds (99% CPU, 4362603 Lips)
Q = [[4, 13, 17, 52]]
12 ?- time(s4(Q,500)).
% 1,104,872 inferences, 0.296 CPU in 0.307 seconds (96% CPU, 3737221 Lips)
Q = [[4, 13, 17, 52]]
*/