% eliminating super-Arrovean profiles by using Prolog
% Nov 2013; originally Sep & Oct 2010; modified: 19 Nov 2013
% lastly modified: 29 Dec 2013
% created by Kenryo Indo (kindo@kanto-gakuen.ac.jp)
% URL: http://www.xkindo.net/sclp/pl/icaart2014.pl
% this source code has been developed on PC with Windows 7 (and Windows XP) OS
% using SWI-Prolog version 6.4.1 (and 5.6.52)
/* preference ordering (linear ordering) for 3-alternative case */
rc(1, [a, c, b]).
rc(2, [a, b, c]).
rc(3, [b, a, c]).
rc(4, [b, c, a]).
rc(5, [c, b, a]).
rc(6, [c, a, b]).
x( X):- member( X, [a,b,c]).
r( [X, Y], R):-
rc( _, R),
append( _, [ X | Z], R),
member( Y, [ X | Z]).
i( [X, Y], R):-
r( [X, Y], R),
r( [Y, X], R).
p( [X, Y], R):-
r( [X, Y], R),
\+ i( [X, Y], R).
/* profile of ordering */
pp( [ R, Q]):- rc( _, R), rc( _, Q).
all_profiles( U):-
findall( R, pp( R), U).
/* the super-Arrovian domain for 2-individual and 3-alternative case */
jv( 1, 5).
jv( 2, 6).
jv( 3, 1).
jv( 4, 2).
jv( 5, 3).
jv( 6, 4).
% automated proof of the super-Arrovian domain.
jv( M, K, J):- between( 1, 6, M), between( 1, 6, K), J is mod( K + M, 6) + 1.
ppc( M, [K, J], [P, Q]):- jv(M, K, J), rc( K, P), rc( J, Q).
m( M, D):- setof(PP, K^J^ ppc( M, [K, J], PP), D).
test0:- m( M, D), nl, write([M]), f(_F,D,swf_axiom), write(*), fail.
/*
% M should be either 1 or 3.
?- test0.
[1]**
[2]********************
[3]**
[4]****************************************************************
[5]*
[6]****************************************************************
false.
% What happen if M = 5.
?- M = 5, m( M, D), f( F, D, swf_axiom), fig( swf, F), fail.
123456
1:[a,c,b] 1-----
2:[a,b,c] -2----
3:[b,a,c] --3---
4:[b,c,a] ---4--
5:[c,b,a] ----5-
6:[c,a,b] -----6
--
false.
*/
ppc( [ K, J], [ R, Q]):- jv( K, J), rc( K, R), rc( J, Q).
m1(C):- findall( P, ppc( _, P), C).
m2(C):- findall( [Q, P], ppc( _, [ P, Q]), C).
m(C):- m1( A), m2( B), append( A, B, C).
/* generic function */
f( [ ], [ ], _).
f( [ X - Y | F], [X | D], Axiom):-
f( F, D, Axiom),
Goal =.. [ Axiom, X, Y, F],
Goal.
sample_axiom( _, A, _):- between( 0, 2, A).
/*
?- f( F, [ a, b], sample_axiom).
F = [a-0, b-0] ;
F = [a-1, b-0] ;
F = [a-2, b-0] ;
F = [a-0, b-1] ;
F = [a-1, b-1] ;
F = [a-2, b-1] ;
F = [a-0, b-2] ;
F = [a-1, b-2] ;
F = [a-2, b-2].
*/
/* Arrow-type preference aggregation (SWF; social welfare function) */
swf( F):-
all_profiles( U),
swf( F, U).
swf( F, D):-
f( F, D, swf_axiom),
\+ dictatorial_swf( _, F).
swf_axiom( X, Y, F):-
rc( _, Y),
pareto( X - Y),
iia( X - Y, F).
agree( +, B, [R, Q]):-
p( B, R),
p( B, Q).
agree( -, [X, Y], [R, Q]):-
p( [Y, X], R),
p( [Y, X], Q).
exactly_agree( +, B, [R, Q]):-
r( B, R),
r( B, Q).
exactly_agree( -, [X, Y], [R, Q]):-
r( [Y, X], R),
r( [Y, X], Q).
pareto( X - Y):-
\+ (
agree( +, W, X),
\+ r( W, Y)
),
\+ (
agree( -, W, X),
r( W, Y)
).
iia( [ P, Q] - S, F):-
\+ (
x( A),
x( B),
member( [ U, V] - T, F),
exactly_agree( _, [ A, B], [ P, U]),
exactly_agree( _, [ A, B], [ Q, V]),
\+ exactly_agree( _, [ A, B], [ S, T])
).
dictatorial_swf( J, F):-
nth1( J, [P, Q], R),
\+ (
member( [ P, Q] - S, F),
S \= R
).
% an automated-proof of Arrow's impossibility theorem.
/*
?- swf(F).
false.
?- all_profiles(U), f(F, U, swf_axiom), fig(swf, F), fail.
123456
1:[a,b,c] 123456
2:[a,c,b] 123456
3:[b,a,c] 123456
4:[b,c,a] 123456
5:[c,a,b] 123456
6:[c,b,a] 123456
--
123456
1:[a,b,c] 111111
2:[a,c,b] 222222
3:[b,a,c] 333333
4:[b,c,a] 444444
5:[c,a,b] 555555
6:[c,b,a] 666666
--
false.
% proving dictatorships on the super-Arrovian domain.
?- m1(U), f(F, U, swf_axiom), fig(swf, F), fail.
123456
1:[a,c,b] ----5-
2:[a,b,c] -----6
3:[b,a,c] 1-----
4:[b,c,a] -2----
5:[c,b,a] --3---
6:[c,a,b] ---4--
--
123456
1:[a,c,b] ----1-
2:[a,b,c] -----2
3:[b,a,c] 3-----
4:[b,c,a] -4----
5:[c,b,a] --5---
6:[c,a,b] ---6--
--
false.
?- findall(P,(between(1,6,K), J is mod(K -3,6) +1,ppc([K,J],P)),U),
f(F, U, swf_axiom), fig(swf, F), fail.
123456
1:[a,c,b] ----5-
2:[a,b,c] -----6
3:[b,a,c] 1-----
4:[b,c,a] -2----
5:[c,b,a] --3---
6:[c,a,b] ---4--
--
123456
1:[a,c,b] ----1-
2:[a,b,c] -----2
3:[b,a,c] 3-----
4:[b,c,a] -4----
5:[c,b,a] --5---
6:[c,a,b] ---6--
--
false.
*/
/* strategy-proof and non-imposed voting procedure (SCF; social choice function) */
scf( F):-
all_profiles( U),
scf( F, U).
scf( F, D):-
f( F, D, scf_axiom),
non_imposed( F),
\+ dictatorial_scf( _, F).
scf_axiom( X, Y, F):-
x( Y),
\+ manipulable( _, X - Y, F).
manipulable( 1, [ R, Q] - S, F):-
member( [ P, Q] - T, F),
(
p( [ T, S], R)
;
p( [ S, T], P)
).
manipulable( 2, [ R, Q] - S, F):-
member( [ R, W] - T, F),
(
p( [ T, S], Q)
;
p( [ S, T], W)
).
non_imposed(F):-
\+ (
x(X),
\+ member( _ - X, F)
).
dictatorial_scf( J, F):-
nth1( J, [ P, Q], R),
\+ (
member( [ P, Q] - X, F),
\+ best( X, R)
).
best(X,Q):-
x( X),
\+ (
x( Y),
\+ r( [X, Y], Q)
).
% an automated-proof of the Gibbard-Satterthwaite theorem.
/*
?- scf(F).
false.
?- all_profiles(U), f(F, U, scf_axiom), non_imposed( F), fig(scf, F), fail.
123456
1:[a,b,c] aabbcc
2:[a,c,b] aabbcc
3:[b,a,c] aabbcc
4:[b,c,a] aabbcc
5:[c,a,b] aabbcc
6:[c,b,a] aabbcc
--
123456
1:[a,b,c] aaaaaa
2:[a,c,b] aaaaaa
3:[b,a,c] bbbbbb
4:[b,c,a] bbbbbb
5:[c,a,b] cccccc
6:[c,b,a] cccccc
--
false.
*/
/* monotone and unanimous SCF */
mcf( F):-
all_profiles( U),
mcf( F, U).
mcf( F, D):-
f( F, D, mcf_axiom),
\+ dictatorial_scf( _, F).
% note: nondictatorship constraint is not active in the unrestricted domain.
mcf_axiom( X, Y, F):-
x( Y),
unanimity( X - Y),
\+ nonmonotonic_change( X - Y, _, F).
nonmonotonic_change( [R1, R2] - C, [S1, S2] - D, F):-
member( [S1, S2] - D, F),
C \= D,
has_no_reversal( C, R1, S1),
has_no_reversal( C, R2, S2).
nonmonotonic_change( [R1, R2] - C, [S1, S2] - D, F):-
member( [S1, S2] - D, F),
C \= D,
has_no_reversal( D, S1, R1),
has_no_reversal( D, S2, R2).
has_no_reversal( X, R, Q):-
lcc( X, R, Lr),
lcc( X, Q, Lq),
subset( Lr, Lq).
lcc( X, R, L):-
x( X),
rc( _, R),
append( _, [ X| L], R).
unanimity( [[X|_], [X|_]] - X).
unanimity( [[X|_], [Y|_]] - _):- X \= Y.
unanimity1( [R1, R2] - D):-
pp( [R1, R2] ),
x( D),
\+ (
x( C),
C \= D,
p( [ C, D], R1),
p( [ C, D], R2)
).
/*
% another automated-proof of the Gibbard-Satterthwaite theorem
% using Maskin-monotonicity (the Muller-Satterthwaite theorem).
?- all_profiles(U),f(F, U, mcf_axiom), fig(scf, F), fail.
123456
1:[a,b,c] aabbcc
2:[a,c,b] aabbcc
3:[b,a,c] aabbcc
4:[b,c,a] aabbcc
5:[c,a,b] aabbcc
6:[c,b,a] aabbcc
--
123456
1:[a,b,c] aaaaaa
2:[a,c,b] aaaaaa
3:[b,a,c] bbbbbb
4:[b,c,a] bbbbbb
5:[c,a,b] cccccc
6:[c,b,a] cccccc
--
false.
*/
% utilities
/* table display */
fig( _, _):-
nl, tab(10), rc( K, _), write( K), fail.
fig( M, F):-
rc( J, P), nl, write( J : P), tab(1),
rc( _, Q), fig_cell( M, [ P, Q], F), fail.
fig( _, _):- nl, write( '--').
fig_cell( swf, [ P, Q], F):-
member( [ P, Q] - S, F), !,
rc( I, S), write( I).
fig_cell( scf, [ P, Q], F):-
member( [ P, Q] - X, F), !, write( X).
fig_cell( _, [ P, Q], F):-
\+ member( [ P, Q] - _, F), !,
write( '-').
fig_cell( _, _, _):- nl, write( '-').
/* select n elements given a list ( to create restricted domain) */
select_n( [], [], 0).
select_n( [ R | Q], [ R | S], A):-
select_n( Q, S, B),
A is B + 1.
select_n( Q, [ _ | S], B):-
select_n( Q, S, B).
/* proving the pallarel possibility results by using profile-elimination */
% test1 to test5
% test1: the cross-elimination of paired profiles
% with adjacent-indecies in the super-Arrovian domain
test1:-
test1( swf),
test1( scf),
test1( mcf).
test1( Type ):-
member( Type, [swf, scf, mcf]),
test1_message( Type, Mes),
nl,
write( Mes),
all_profiles( L),
m1( C),
nth1( K, C, V),
nl, write( [ K]), tab( 1),
m2( D),
nth1( J, D, W),
subtract( L, [ V, W], H),
Rule =.. [ Type, _, H],
Rule,
write(J; ' '),
fail.
test1( _).
test1_message( swf, ' minimal (cross-)elimination for Arrow-type swf:').
test1_message( scf, ' minimal (cross-)elimination for strategy-proof scf:').
test1_message( mcf, ' minimal (cross-)elimination for monotonic scf:').
/*
minimal (cross-)elimination for Arrow-type swf:
[1] 1; 2; 6;
[2] 1; 2; 3;
[3] 2; 3; 4;
[4] 3; 4; 5;
[5] 4; 5; 6;
[6] 1; 5; 6;
minimal (cross-)elimination for strategy-proof scf:
[1] 1; 2; 6;
[2] 1; 2; 3;
[3] 2; 3; 4;
[4] 3; 4; 5;
[5] 4; 5; 6;
[6] 1; 5; 6;
minimal (cross-)elimination for monotonic scf:
[1] 1; 2; 6;
[2] 1; 2; 3;
[3] 2; 3; 4;
[4] 3; 4; 5;
[5] 4; 5; 6;
[6] 1; 5; 6;
true.
*/
% test2: pallarel generation of restricted SWFs and SCFs
% by eliminating profiles in the two super-Arrovian domains.
:- dynamic test2_data/4, test_2_f/3.
test2:-
retractall( test2_data(_,_,_,_)),
retractall( test2_f(_,_,_)),
all_profiles( L),
m(B),
length( [_|B], K),
between( 0, K, N),
M is N - 1,
test2_stat( swf, M),
select_n( C, B, N),
subtract( L, C, U),
% findall( 1, f( F, U, swf_axiom), H),
findall( 1, (
f( F, U, swf_axiom),
assert( test_2_f( swf(N), F, U))
), H),
length( H, I),
% findall( 1, (f( _, U, scf_axiom), non_imposed( F)), G),
findall( 1, (
f( F, U, scf_axiom),
non_imposed( F),
assert( test_2_f( scf(N), F, U))
), G),
length( G, J),
assert( test2_data( N, C, I, J)),
fail.
test2.
test2_stat( F, K):-
( var(K) -> true ; K >= 0),
nl,
write( [K]),
tab(1),
member( F, [ swf, scf]),
test2_stat( F, K, I, B),
bagof( 1, B, W),
length( W, S),
write( I - S ;' '),
fail.
test2_stat( _, _).
test2_stat( swf, K, I, C^J^test2_data( K, C, I, J)).
test2_stat( scf, K, J, C^I^test2_data( K, C, I, J)).
/*
?- test2.
[0] 2-1;
[1] 2-12;
[2] 2-48; 3-18;
[3] 2-76; 3-108; 4-36;
[4] 2-48; 3-156; 4-225; 5-60; 6-6;
[5] 2-12; 3-60; 4-228; 5-348; 6-120; 7-24;
[6] 2-2; 4-54; 5-170; 6-390; 7-252; 8-50; 9-6;
[7] 5-12; 6-60; 7-228; 8-348; 9-120; 10-24;
[8] 8-48; 9-156; 10-225; 11-60; 12-6;
[9] 11-76; 12-108; 13-36;
[10] 14-48; 15-18;
[12] 20-1;
?- between(0,12,K),test4_stat( swf, K),fail.
[0] 2-1;
[1] 2-12;
[2] 2-48; 3-18;
[3] 2-76; 3-108; 4-36;
[4] 2-48; 3-156; 4-225; 5-60; 6-6;
[5] 2-12; 3-60; 4-228; 5-348; 6-120; 7-24;
[6] 2-2; 4-54; 5-170; 6-390; 7-252; 8-50; 9-6;
[7] 5-12; 6-60; 7-228; 8-348; 9-120; 10-24;
[8] 8-48; 9-156; 10-225; 11-60; 12-6;
[9] 11-76; 12-108; 13-36;
[10] 14-48; 15-18;
[11] 17-12;
[12] 20-1;
false.
?- between(0,12,K),test2_stat( scf, K),fail.
[0] 2-1;
[1] 2-12;
[2] 2-48; 3-18;
[3] 2-64; 3-120; 4-36;
[4] 2-30; 3-114; 4-255; 5-90; 6-6;
[5] 2-12; 4-144; 5-300; 6-252; 7-72; 8-12;
[6] 2-2; 5-62; 6-150; 7-294; 8-242; 9-78; 10-72; 12-18; 13-6;
[7] 6-12; 8-120; 9-132; 10-192; 11-48; 12-108; 13-48; 14-72; 15-12; 16-24; 19-24;
[8] 10-18; 11-36; 12-57; 13-30; 14-36; 15-36; 16-69; 17-36; 18-72; 19-12; 20-12; 22-36; 25-30; 28-3; 29-6; 30-6;
[9] 14-4; 17-12; 20-36; 21-12; 22-36; 23-12; 26-12; 28-24; 31-24; 34-12; 35-12; 38-12; 40-12;
[10] 37-12; 38-6; 40-6; 41-12; 46-6; 48-12; 50-6; 74-6;
[11] 88-12;
[12] 196-1;
?- [menu].
?- tell_goal( 'test2_data.pl', forall, test2_data(_,_,_,_)).
?- tell_goal( 'test2_f.pl', forall, test2_f(_,_,_)).
*/
% test3: the cross table of test2 data.
test3:-
setof( J, K^C^I^test2_data( K, C, I, J), L),
member( J, L), nl, write( [J]),
bagof( C, K^test2_data( K, C, I, J), W),
length( W, S), tab(1), write( I - S ;' '),
fail.
test3.
/*
?- test3.
[2] 2-169;
[3] 2-24; 3-228;
[4] 2-6; 3-84; 4-345;
[5] 3-6; 4-144; 5-302;
[6] 3-24; 4-24; 5-168; 6-204;
[7] 5-36; 6-192; 7-138;
[8] 4-24; 5-36; 6-78; 7-168; 8-68;
[9] 5-12; 6-12; 7-60; 8-96; 9-30;
[10] 5-36; 6-36; 7-18; 8-120; 9-60; 10-12;
[11] 7-24; 8-12; 9-24; 10-24;
[12] 6-30; 7-36; 8-30; 9-24; 10-48; 11-12; 12-3;
[13] 4-6; 7-24; 8-24; 10-12; 11-18;
[14] 7-24; 8-48; 10-30; 11-10;
[15] 8-12; 9-24; 11-12;
[16] 6-12; 8-18; 9-48; 10-12; 12-3;
[17] 9-12; 10-24; 13-12;
[18] 10-60; 11-12;
[19] 6-12; 7-12; 10-12;
[20] 9-6; 10-6; 11-24; 12-12;
[21] 12-12;
[22] 8-12; 9-24; 12-24; 13-12;
[23] 13-12;
[25] 9-24; 10-6;
[26] 12-12;
[28] 10-3; 11-24;
[29] 9-6;
[30] 8-6;
[31] 12-24;
[34] 12-12;
[35] 12-12;
[37] 14-12;
[38] 11-12; 15-6;
[40] 11-12; 14-6;
[41] 15-12;
[46] 14-6;
[48] 14-12;
[50] 14-6;
[74] 14-6;
[88] 17-12;
[196] 20-1;
true.
*/
% test4: a variant of test3 that replaces strategy-proofness with Maskin-monotonicity.
:- dynamic test4_data/4.
test4:-
retractall( test4_data(_,_,_,_)),
all_profiles( L),
m(B),
length( [_|B], K),
between( 0, K, N),
M is N - 1,
test4_stat( swf, M),
select_n( C, B, N),
subtract( L, C, U),
findall( 1, f( _, U, swf_axiom), H),
length( H, I),
findall( 1, f( _, U, mcf_axiom), G),
length( G, J),
assert( test4_data( N, C, I, J)),
fail.
test4.
test4_stat( F, K):-
( var(K) -> true ; K >= 0),
nl,
write( [K]),
tab(1),
member( F, [ swf, mcf]),
test4_stat( F, K, I, B),
bagof( 1, B, W),
length( W, S),
write( I - S ;' '),
fail.
test4_stat( _, _).
test4_stat( swf, K, I, C^J^test4_data( K, C, I, J)).
test4_stat( mcf, K, J, C^I^test4_data( K, C, I, J)).
% test5: the cross table of test2 data.
test5:-
setof( J, K^C^I^test4_data( K, C, I, J), L),
member( J, L), nl, write( [J]),
bagof( C, K^test4_data( K, C, I, J), W),
length( W, S), tab(1), write( I - S ;' '),
fail.
test5.
/*
?- test4.
[0] 2-1;
[1] 2-12;
[2] 2-48; 3-18;
[3] 2-76; 3-108; 4-36;
[4] 2-48; 3-156; 4-225; 5-60; 6-6;
[5] 2-12; 3-60; 4-228; 5-348; 6-120; 7-24;
[6] 2-2; 4-54; 5-170; 6-390; 7-252; 8-50; 9-6;
[7] 5-12; 6-60; 7-228; 8-348; 9-120; 10-24;
[8] 8-48; 9-156; 10-225; 11-60; 12-6;
[9] 11-76; 12-108; 13-36;
[10] 14-48; 15-18;
[11] 17-12;
[12] 20-1;
true.
?- between(0,12,K),test4_stat( swf, K),fail.
[0] 2-1;
[1] 2-12;
[2] 2-48; 3-18;
[3] 2-76; 3-108; 4-36;
[4] 2-48; 3-156; 4-225; 5-60; 6-6;
[5] 2-12; 3-60; 4-228; 5-348; 6-120; 7-24;
[6] 2-2; 4-54; 5-170; 6-390; 7-252; 8-50; 9-6;
[7] 5-12; 6-60; 7-228; 8-348; 9-120; 10-24;
[8] 8-48; 9-156; 10-225; 11-60; 12-6;
[9] 11-76; 12-108; 13-36;
[10] 14-48; 15-18;
[11] 17-12;
[12] 20-1;
false.
?- between(0,12,K),test4_stat( mcf, K),fail.
[0] 2-1;
[1] 2-12;
[2] 2-48; 3-18;
[3] 2-76; 3-108; 4-36;
[4] 2-48; 3-156; 4-225; 5-60; 6-6;
[5] 2-12; 3-60; 4-228; 5-348; 6-120; 7-24;
[6] 2-2; 4-54; 5-170; 6-390; 7-252; 8-50; 9-6;
[7] 5-12; 6-60; 7-228; 8-348; 9-120; 10-24;
[8] 8-48; 9-156; 10-225; 11-60; 12-6;
[9] 11-76; 12-108; 13-36;
[10] 14-48; 15-18;
[11] 17-12;
[12] 20-1;
false.
?- test5.
[2] 2-199;
[3] 3-342;
[4] 4-543;
[5] 5-590;
[6] 6-576;
[7] 7-504;
[8] 8-446;
[9] 9-282;
[10] 10-249;
[11] 11-136;
[12] 12-114;
[13] 13-36;
[14] 14-48;
[15] 15-18;
[17] 17-12;
[20] 20-1;
true.
*/
% test6: simultaneously collects the three types of possibility results.
:- dynamic test6_data/4.
test6:-
retractall( test6_data(_,_,_,_)),
all_profiles( L),
m(B),
length( [_|B], K),
between( 0, K, N),
M is N - 1,
nl, write(['complete level':M]),
select_n( C, B, N),
subtract( L, C, U),
test6( N, C, U, _),
fail.
test6.
test6( N, C, U, swf):-
f( F, U, swf_axiom),
assert( test6_data( N, C, U, swf:F)).
test6( N, C, U, scf):-
f( F, U, scf_axiom),
non_imposed( F),
assert( test6_data( N, C, U, scf:F)).
test6( N, C, U, scf):-
f( F, U, mcf_axiom),
assert( test6_data( N, C, U, mcf:F)).
test6_stat:-
test6_stat( _, _), fail ; true.
test6_stat( F, K):-
member( F, [ swf, scf, mcf]),
nl,
write( 'number of possible domains':F),
between( 0, 12, K),
nl,
write( [K]),
tab(1),
bagof( 1, C^test6_stat_part( F, K, C, I), W),
length( W, S),
write( I - S ;' '),
fail.
test6_stat( _, _).
test6_stat_part( F, K, C, I):-
bagof( C, H^test6_data( K, C, _U, F: H), P),
length( P, I).
% test7: the cross table of test6 data.
test7:-
member( F, [ scf, mcf]),
nl,
write( 'cross table of swf and '), write( F),
setof( J, K^C^
test6_stat_part( swf, K, C, J),
L),
member( J, L), nl, write( [J]),
setof( C, K^(
test6_stat_part( swf, K, C, J),
test6_stat_part( F, K, C, I)
), W),
length( W, S), tab(1), write( I - S ;' '),
fail.
test7.
/*
?- test6.
?- test6_stat.
number of possible domains:swf
[0] 2-1;
[1] 2-12;
[2] 2-48; 3-18;
[3] 2-76; 3-108; 4-36;
[4] 2-48; 3-156; 4-225; 5-60; 6-6;
[5] 2-12; 3-60; 4-228; 5-348; 6-120; 7-24;
[6] 2-2; 4-54; 5-170; 6-390; 7-252; 8-50; 9-6;
[7] 5-12; 6-60; 7-228; 8-348; 9-120; 10-24;
[8] 8-48; 9-156; 10-225; 11-60; 12-6;
[9] 11-76; 12-108; 13-36;
[10] 14-48; 15-18;
[11] 17-12;
[12] 20-1;
number of possible domains:scf
[0] 2-1;
[1] 2-12;
[2] 2-48; 3-18;
[3] 2-64; 3-120; 4-36;
[4] 2-30; 3-114; 4-255; 5-90; 6-6;
[5] 2-12; 4-144; 5-300; 6-252; 7-72; 8-12;
[6] 2-2; 5-62; 6-150; 7-294; 8-242; 9-78; 10-72; 12-18; 13-6;
[7] 6-12; 8-120; 9-132; 10-192; 11-48; 12-108; 13-48; 14-72; 15-12; 16-24; 19-24;
[8] 10-18; 11-36; 12-57; 13-30; 14-36; 15-36; 16-69; 17-36; 18-72; 19-12; 20-12; 22-36; 25-30; 28-3; 29-6; 30-6;
[9] 14-4; 17-12; 20-36; 21-12; 22-36; 23-12; 26-12; 28-24; 31-24; 34-12; 35-12; 38-12; 40-12;
[10] 37-12; 38-6; 40-6; 41-12; 46-6; 48-12; 50-6; 74-6;
[11] 88-12;
[12] 196-1;
number of possible domains:mcf
[0] 2-1;
[1] 2-12;
[2] 2-48; 3-18;
[3] 2-76; 3-108; 4-36;
[4] 2-48; 3-156; 4-225; 5-60; 6-6;
[5] 2-12; 3-60; 4-228; 5-348; 6-120; 7-24;
[6] 2-2; 4-54; 5-170; 6-390; 7-252; 8-50; 9-6;
[7] 5-12; 6-60; 7-228; 8-348; 9-120; 10-24;
[8] 8-48; 9-156; 10-225; 11-60; 12-6;
[9] 11-76; 12-108; 13-36;
[10] 14-48; 15-18;
[11] 17-12;
[12] 20-1;
true.
?- [menu].
?- tell_goal( 'test6_data.pl', forall, test6_data(_,_,_,_)).
*/