:- use_module('EQUILIBRIUM_POLICIES', [equilibrium_policies/3]).
:- set_prolog_flag(debugger_write_options,  [ quoted(true), portray(true),  max_depth(100), spacing(next_argument)]).
:- op(700, xfy, '=>').


%% ICLP / Example 6
:- equilibrium_policies(((z => x) * ((-z) + z)), [e(x),e(z)], (M,C)),
   M = [ne(x, 0, ne(z, 0, lambda)), ne(x, 1, ne(z, 1, lambda))],
   C = [([], [x])].

:- equilibrium_policies(((z => x) * ((-z) + z)), [e(z),e(x)], (M,C)),
   M = [ne(z, 0, ne(x, 0, lambda)), ne(z, 1, ne(x, 1, lambda))],
   C = [([], [x])].


%% ICLP / Example 7
:- equilibrium_policies(((z => x) * ((-z) + z)), [u(x),e(z)], (M,C)),
   M = [nu(x, (ne(z, 0, lambda), ne(z, 1, lambda)))],
   C = [([], [x])].

:- equilibrium_policies(((z => x) * ((-z) + z)), [u(z),e(x)], (M,C)),
   M = [nu(z, (ne(x, 0, lambda), ne(x, 1, lambda)))],
   C = [([], [x])].

:- equilibrium_policies(((z => x) * ((-z) + z)), [e(x),u(z)], (M,C)),
   M = [],
   C = [([], [x])].

:- equilibrium_policies(((z => x) * ((-z) + z)), [e(z),u(x)], (M,C)),
   M = [],
   C = [([], [x])].

:- equilibrium_policies(((z => x) * ((-z) + z)), [u(x),u(z)], (M,C)),
   M = [],
   C = [([], [x])].

:- equilibrium_policies(((z => x) * ((-z) + z)), [u(z),u(x)], (M,C)),
   M = [],
   C = [([], [x])].

% Answer: 1
% c g f e
?- equilibrium_policies((((e * f * g * (-c) * (-d)) => a) * c * e * f *g),[e(a),e(c),e(d),e(e),e(f),e(g)], (M, _C)), M = [ne(a, 0, ne(c, 1, ne(d, 0, ne(e, 1, ne(f, 1, ne(g, 1, lambda))))))].

% Answer: 1
% g f e a
?- equilibrium_policies((((e * f * g * (-c) * (-d)) => a) * e * f *g),[e(a),e(c),e(d),e(e),e(f),e(g)], (M, _C)),  M = [ne(a, 1, ne(c, 0, ne(d, 0, ne(e, 1, ne(f, 1, ne(g, 1, lambda))))))].

% UNSATISFIABLE
?- equilibrium_policies((((e * f * g * (-c) * (-d)) => a) * e * f * g * (a=>c)),[e(a),e(c),e(d),e(e),e(f),e(g)],(M,_C)), M = [].

% Answer: 1
% g f e a
?- equilibrium_policies((((e * f * g * (-c) * (-d)) => a) * e * f * g * ((a * (-a))=>c)),[e(a),e(c),e(d),e(e),e(f),e(g)],(M,_C)), M = [ne(a, 1, ne(c, 0, ne(d, 0, ne(e, 1, ne(f, 1, ne(g, 1, lambda))))))].

% Answer: 1
?- equilibrium_policies(((a=>b) * (b=>a)),[e(a),e(b)], (M,_C)), M = [ne(a, 0, ne(b, 0, lambda))].

% Answer: 1
% a
% Answer: 2
% b
?- equilibrium_policies((((-a)=>b) * ((-b)=>a)),[e(a),e(b)], (M,_C)), M = [ne(a, 0, ne(b, 1, lambda)), ne(a, 1, ne(b, 0, lambda))].

% Answer: 1
% a
?- equilibrium_policies((((-a) => a) * ((-a)=>b) * ((-b)=>a)),[e(a),e(b)], (M,_C)), M = [ne(a, 1, ne(b, 0, lambda))].

% Answer: 1
% b
% Answer: 2
% a
?- equilibrium_policies(((((-a) *(-b)) => a) * ((-a)=>b) * ((-b)=>a)),[e(a),e(b)], (M,_C)), M = [ne(a, 0, ne(b, 1, lambda)), ne(a, 1, ne(b, 0, lambda))].

?- equilibrium_policies(((((-a) *(-b)) => a) * ((-a)=>b) * ((-b)=>a)),[u(a),e(b)], (M,_C)), M = [nu(a,  (ne(b, 1, lambda), ne(b, 0, lambda)))].

% Answer: 1
% b c d
% Answer: 2
% a
?- equilibrium_policies(((b=>d) * (b=>c) * (((-a) *(-b)) => a) * ((-a)=>b) * ((-b)=>a)),[e(a),e(b),e(c),e(d)], (M,_C)), M = [ne(a, 0, ne(b, 1, ne(c, 1, ne(d, 1, lambda)))), ne(a, 1, ne(b, 0, ne(c, 0, ne(d, 0, lambda))))].

?- equilibrium_policies(((b=>d) * (b=>c) * (((-a) *(-b)) => a) * ((-a)=>b) * ((-b)=>a)),[u(a),e(b),e(c),e(d)], (M,_C)), M = [nu(a,  (ne(b, 1, ne(c, 1, ne(d, 1, lambda))), ne(b, 0, ne(c, 0, ne(d, 0, lambda)))))].

% Answer: 1
% a
?- equilibrium_policies((((-a) => 0) * (b=>d) * (b=>c) * (((-a) *(-b)) => a) * ((-a)=>b) * ((-b)=>a)),[e(a),e(b),e(c),e(d)], (M,_C)), M = [ne(a, 1, ne(b, 0, ne(c, 0, ne(d, 0, lambda))))].

% UNSATISFIABLE
?- equilibrium_policies(((-a) => a),[e(a)], (M,_C)),  M = [].

% Answer: 1
% c a
?- equilibrium_policies( (c * ((c * (-a)) => 0) * (((-a) * (-d)) => b) * (((-b) * (-d)) => a)),[e(a),e(b),e(c),e(d)], (M,_C)), M = [ne(a, 1, ne(b, 0, ne(c, 1, ne(d, 0, lambda))))].

% UNSATISFIABLE
?- equilibrium_policies( (((-a) => 0) * (((-a) * (-b)) => 0) * (((-e) * (-f)) => 0)),[e(a),e(b),e(e),e(f)], (M,_C)), M = [].

% UNSATISFIABLE
?- equilibrium_policies( (d * (((-a) * (-b)) => b) * ((d * (-a)) => c)),[e(a),e(b),e(c),e(d)], (M,_C)), M = [].

% UNSATISFIABLE
?- equilibrium_policies( ( d * (c => a) * ((d * (-a)) => c) ), [e(a),e(b),e(c),e(d)], (M,_C)), M = [].

% UNSATISFIABLE
?- equilibrium_policies( ( d * (c => a) * (a => c) * ((d * (-a)) => c) * ((d * (-c)) => a) ), [e(a),e(b),e(c),e(d)], (M,_C)), M = [].

% Answer: 1
?- equilibrium_policies( ((a * b * (-c) * (-d)) => h), [e(a),e(b),e(c),e(d),e(h)], (M,_C)), M = [ne(a, 0, ne(b, 0, ne(c, 0, ne(d, 0, ne(h, 0, lambda)))))].

% Answer: 1
?- equilibrium_policies( ((b * (-c)) => a), [e(a),e(b),e(c)], (M,_C)),  M = [ne(a, 0, ne(b, 0, ne(c, 0, lambda)))].

% Answer: 1
% a
?- equilibrium_policies( (((-b)=>a) *(c=>b) * (b=>c)) ,[e(a),e(b),e(c)], (M,_C)), M = [ne(a, 1, ne(b, 0, ne(c, 0, lambda)))].

% Answer: 1
% b c d
?- equilibrium_policies( (((-b)=>a) *(c=>b) * (b=>c) * (d=>c) *d) ,[e(a),e(b),e(c),e(d)], (M,_C)), M = [ne(a, 0, ne(b, 1, ne(c, 1, ne(d, 1, lambda))))].

% UNSATISFIABLE
?- equilibrium_policies( (((-b)=>a) *(a=>d) * (c=>b) * (b=>c) * (d=>c)) ,[e(a),e(b),e(c),e(d)], (M,_C)), M = [].

% Answer: 1
% b
?- equilibrium_policies( (((-b)=>a) *(a=>d) * (c=>b) * (d=>c) * ((-c)=>b)) ,[e(a),e(b),e(c),e(d)], (M,_C)), M = [ne(a, 0, ne(b, 1, ne(c, 0, ne(d, 0, lambda))))].

% UNSATISFIABLE
?- equilibrium_policies( (((-b)=>a) *(a=>d) * (c=>b) * (d=>c) * ((-c)=>e) * (b => e)) ,[e(a),e(b),e(c),e(d),e(e)], (M,_C)), M = [].

% Answer: 1
% b e
?- equilibrium_policies( (((-b)=>a) *(a=>d) * (c=>b) * (d=>c) * ((-c)=>e) * (e => b)) ,[e(a),e(b),e(c),e(d),e(e)], (M,_C)), M = [ne(a, 0, ne(b, 1, ne(c, 0, ne(d, 0, ne(e, 1, lambda)))))].

% Answer: 1
% b e c
% Answer: 2
% b e d
% Answer: 3
% b f c
% Answer: 4
% b f d
?- equilibrium_policies( (((-b)=>a) * ((-a)=>b) * ((-f)=>e) * ((-e)=>f) * ((-c)=>d) * ((-d)=>c) * ((a * e) => 0) * ((a * f) => 0)) ,[e(a),e(b),e(c),e(d),e(e),e(f)], (M,_C)), M = [ne(a, 0, ne(b, 1, ne(c, 0, ne(d, 1, ne(e, 0, ne(f, 1, lambda)))))), ne(a, 0, ne(b, 1, ne(c, 0, ne(d, 1, ne(e, 1, ne(f, 0, lambda)))))), ne(a, 0, ne(b, 1, ne(c, 1, ne(d, 0, ne(e, 0, ne(f, 1, lambda)))))), ne(a, 0, ne(b, 1, ne(c, 1, ne(d, 0, ne(e, 1, ne(f, 0, lambda))))))].


?- equilibrium_policies( (((-b)=>a) * ((-a)=>b) * ((-f)=>e) * ((-e)=>f) * ((-c)=>d) * ((-d)=>c) * ((a * e) => 0) * ((a * f) => 0)) ,[e(b),e(a),u(c),e(d),e(e),e(f)], (M,_C)), M = [ne(b, 1, ne(a, 0, nu(c,  (ne(d, 1, ne(e, 0, ne(f, 1, lambda))), ne(d, 0, ne(e, 0, ne(f, 1, lambda))))))), ne(b, 1, ne(a, 0, nu(c,  (ne(d, 1, ne(e, 0, ne(f, 1, lambda))), ne(d, 0, ne(e, 1, ne(f, 0, lambda))))))), ne(b, 1, ne(a, 0, nu(c,  (ne(d, 1, ne(e, 1, ne(f, 0, lambda))), ne(d, 0, ne(e, 0, ne(f, 1, lambda))))))), ne(b, 1, ne(a, 0, nu(c,  (ne(d, 1, ne(e, 1, ne(f, 0, lambda))), ne(d, 0, ne(e, 1, ne(f, 0, lambda)))))))].

?- equilibrium_policies( (((-b)=>a) * ((-a)=>b) * ((-f)=>e) * ((-e)=>f) * ((-c)=>d) * ((-d)=>c) * ((a * e) => 0) * ((a * f) => 0)) ,[e(b),e(a),u(c),e(d),u(e),e(f)], (M,_C)), M = [ne(b, 1, ne(a, 0, nu(c,  (ne(d, 1, nu(e,  (ne(f, 1, lambda), ne(f, 0, lambda)))), ne(d, 0, nu(e,  (ne(f, 1, lambda), ne(f, 0, lambda))))))))].

% Answer: 1
% a d
% Answer: 2
% b e
?- equilibrium_policies( (((-b)=>a) * ((a*(-c))=>d) * ((-d)=>e) * ((-a)=>b) * ((a*(-d))=>c) * ((a * e) => 0)) ,[e(a),e(b),e(c),e(d),e(e)], (M,_C)), M = [ne(a, 0, ne(b, 1, ne(c, 0, ne(d, 0, ne(e, 1, lambda))))), ne(a, 1, ne(b, 0, ne(c, 0, ne(d, 1, ne(e, 0, lambda)))))].

?- equilibrium_policies( (((-b)=>a) * ((a*(-c))=>d) * ((-d)=>e) * ((-a)=>b) * ((a*(-d))=>c) * ((a * e) => 0)) ,[u(a),e(b),e(c),e(d),e(e)], (M,_C)), M = [nu(a,  (ne(b, 1, ne(c, 0, ne(d, 0, ne(e, 1, lambda)))), ne(b, 0, ne(c, 0, ne(d, 1, ne(e, 0, lambda))))))].

?- equilibrium_policies( (((-b)=>a) * ((a*(-c))=>d) * ((-d)=>e) * ((-a)=>b) * ((a*(-d))=>c) * ((a * e) => 0)) ,[e(b),u(a),e(c),e(d),e(e)], (M,_C)), M = [].

% Answer: 1
% b a d c f e
?- equilibrium_policies( (a * d * f *(b=>a) * (a=>b) * (f=>e) * ((b*d)=>c) * ((e*f)=>c)) ,[e(a),e(b),e(c),e(d),e(e),e(f)], (M,_C)), M = [ne(a, 1, ne(b, 1, ne(c, 1, ne(d, 1, ne(e, 1, ne(f, 1, lambda))))))].

% Answer: 1
?- equilibrium_policies( ((b=>a) * ((a*c)=>b) * (d=>b)) ,[e(a),e(b),e(c),e(d)], (M,_C)), M = [ne(a, 0, ne(b, 0, ne(c, 0, ne(d, 0, lambda))))].

% UNSATISFIABLE
?- equilibrium_policies( (((b*(-a))=>a) * ((-c)=>b)) ,[e(a),e(b),e(c)], (M,_C)), M = [].

% Answer: 1
% c a
% Answer: 2
% c b
?- equilibrium_policies( (((c*(-b))=>a) * ((-a)=>b) * (((-c)*(-d))=>d) * c) ,[e(a),e(b),e(c),e(d)], (M,_C)), M = [ne(a, 0, ne(b, 1, ne(c, 1, ne(d, 0, lambda)))), ne(a, 1, ne(b, 0, ne(c, 1, ne(d, 0, lambda))))].

?- equilibrium_policies( (((c*(-b))=>a) * ((-a)=>b) * (((-c)*(-d))=>d) * c) ,[e(c),e(d),u(b),e(a)], (M,_C)), M = [ne(c, 1, ne(d, 0, nu(b,  (ne(a, 1, lambda), ne(a, 0, lambda)))))].

?- equilibrium_policies( (((c*(-b))=>a) * ((-a)=>b) * (((-c)*(-d))=>d) * c) ,[e(c),e(d),u(a),e(b)], (M,_C)), M = [ne(c, 1, ne(d, 0, nu(a,  (ne(b, 1, lambda), ne(b, 0, lambda)))))].

?- equilibrium_policies( (((c*(-b))=>a) * ((-a)=>b) * (((-c)*(-d))=>d) * c) ,[u(a),e(c),e(d),e(b)], (M,_C)), M = [nu(a,  (ne(c, 1, ne(d, 0, ne(b, 1, lambda))), ne(c, 1, ne(d, 0, ne(b, 0, lambda)))))].

?- equilibrium_policies( (((c*(-b))=>a) * ((-a)=>b) * (((-c)*(-d))=>d) * c) ,[e(d),u(a),e(c),e(b)], (M,_C)), M = [ne(d, 0, nu(a,  (ne(c, 1, ne(b, 1, lambda)), ne(c, 1, ne(b, 0, lambda)))))].

?- equilibrium_policies( (((c*(-b))=>a) * ((-a)=>b) * (((-c)*(-d))=>d) * c) ,[e(d),e(c),e(b),u(a)], (M,_C)), M = [].

% UNSATISFIABLE
?- equilibrium_policies( ((-a) => 0) ,[e(a)], (M,_C)), M = [].

% UNSATISFIABLE
?- equilibrium_policies( (((-a) * (-b)) => 0) ,[e(a),e(b)], (M,_C)), M = [].

% Answer: 1
?- equilibrium_policies( ( ((b * c * (-f) * (-g)) => a) * ((a * c * (-g) * (-f)) => b) * (a => c) * (b => d) * ((c * g) => f) * ((d * f) => g) ) ,[e(a),e(b),e(c),e(d),e(f),e(g)], (M,_C)), M = [ne(a, 0, ne(b, 0, ne(c, 0, ne(d, 0, ne(f, 0, ne(g, 0, lambda))))))].

% Answer: 1
% a d
% Answer: 2
% b e
?- equilibrium_policies(((((-b) * (-b)) => a) * ((a * (-c) * (-c)) => d) * (((-d) * (-d)) => e) * (((-a) * (-a)) => b) * ((a * (-d)* (-d)) => c) * ((a * e) => 0)) , [e(a),e(b),e(c),e(d),e(e)], (M,_C)), M = [ne(a, 0, ne(b, 1, ne(c, 0, ne(d, 0, ne(e, 1, lambda))))), ne(a, 1, ne(b, 0, ne(c, 0, ne(d, 1, ne(e, 0, lambda)))))].

?- equilibrium_policies(((((-b) * (-b)) => a) * ((a * (-c) * (-c)) => d) * (((-d) * (-d)) => e) * (((-a) * (-a)) => b) * ((a * (-d)* (-d)) => c) * ((a * e) => 0)) , [u(a),e(b),e(c),e(d),e(e)], (M,_C)), M = [nu(a, (ne(b, 1, ne(c, 0, ne(d, 0, ne(e, 1, lambda)))), ne(b, 0, ne(c, 0, ne(d, 1, ne(e, 0, lambda))))))].


?- equilibrium_policies(((((-b) * (-b)) => a) * ((a * (-c) * (-c)) => d) * (((-d) * (-d)) => e) * (((-a) * (-a)) => b) * ((a * (-d)* (-d)) => c) * ((a * e) => 0)) , [e(b),u(a),e(c),e(d),e(e)], (M,_C)), M = [].

% Answer: 1
% q
?- equilibrium_policies((((-q) => p) * ((-p) => q) * ((p * (-s)) => s) * q), [e(q),e(p),e(s)], (M,_C)), M = [ne(q, 1, ne(p, 0, ne(s, 0, lambda)))].

% Answer: 1
% a i
?- equilibrium_policies(( (((-c)* (-d)) => a) * ((a*(-b)) => i) * ((a*(-i)) => i)), [e(a),e(b),e(c),e(d),e(i)], (M,_C)), M = [ne(a, 1, ne(b, 0, ne(c, 0, ne(d, 0, ne(i, 1, lambda)))))].

% UNSATISFIABLE
?- equilibrium_policies( (((-q) => p) * ((-p) => q) * ((r * (-s))=> s) * (p => r) * r), [e(p),e(q),e(r),e(s)], (M,_C)), M = [].

% UNSATISFIABLE
?- equilibrium_policies((((-q) => p) * ((-r) => q) * ((-p) => r)), [e(q),e(p),e(r)], (M,_C)), M = [].

% Answer: 1
% a
?- equilibrium_policies((a * ((-a) => a)), [e(a)], (M,_C)), M = [ne(a, 1, lambda)].

% Answer: 1
% a
?- equilibrium_policies((a * (((-a)*(-a)) => a)), [e(a)], (M,_C)), M = [ne(a, 1, lambda)].

% Answer: 1
% d
?- equilibrium_policies((((-c)=> d) * (((-d)*(-d)) => e) * ((-d) => c) * (e => 0)), [e(a),e(b),e(c),e(d),e(e)], (M,_C)), M = [ne(a, 0, ne(b, 0, ne(c, 0, ne(d, 1, ne(e, 0, lambda)))))].

% Answer: 1
% d
?- equilibrium_policies((((-c)=> d) * ((-d) => e) * ((-d) => c) * (e => 0)), [e(a),e(b),e(c),e(d),e(e)], (M,_C)), M = [ne(a, 0, ne(b, 0, ne(c, 0, ne(d, 1, ne(e, 0, lambda)))))].

% Answer: 1
% c
?- equilibrium_policies((c * (((-c) * (-d))=>e)), [e(c),e(d),e(e)], (M,_C)), M = [ne(c, 1, ne(d, 0, ne(e, 0, lambda)))].

% Answer: 1
% d
?- equilibrium_policies((d * (((-d) * (-d)) => e)), [e(e),e(d)], (M,_C)), M = [ne(e, 0, ne(d, 1, lambda))].

% UNSATISFIABLE
?- equilibrium_policies(((a => b) * (b => a) * ((-b) => 0)), [e(a),e(b)], (M,_C)), M = [].

% Answer: 1
?- equilibrium_policies(((a => b) * (b => a) * (b => 0)), [e(a),e(b)], (M,_C)), M = [ne(a, 0, ne(b, 0, lambda))].

% Answer: 1
% e b g f
% Answer: 2
% e b a
% Answer: 3
% c a
?- equilibrium_policies( ((g => f) * (e => b) * ((-a) => g) * ((-g) => a) * ((-b) => a) * ((-e) => c)  * ((-c) => e)), [e(a),e(b),e(c),e(e),e(f),e(g)], (M,_C)), M = [ne(a, 0, ne(b, 1, ne(c, 0, ne(e, 1, ne(f, 1, ne(g, 1, lambda)))))), ne(a, 1, ne(b, 0, ne(c, 1, ne(e, 0, ne(f, 0, ne(g, 0, lambda)))))), ne(a, 1, ne(b, 1, ne(c, 0, ne(e, 1, ne(f, 0, ne(g, 0, lambda))))))].

?- equilibrium_policies(((z => x) * ((-z) => y) * ((-y) => z) * ((-x) => 0) * ((-y) => 0) ), [e(x),e(y),e(z)], (M,_C)), M = [].

?- equilibrium_policies(((z => x) * ((-z) => y) * ((-y) => z)), [u(x),e(y),e(z)], (M,_C)), M = [nu(x,  (ne(y, 1, ne(z, 0, lambda)), ne(y, 0, ne(z, 1, lambda))))].

?- equilibrium_policies(((z => x) * ((-z) => y) * ((-y) => z) ), [e(x),e(y),e(z)], (M,_C)), M = [ne(x, 0, ne(y, 1, ne(z, 0, lambda))), ne(x, 1, ne(y, 0, ne(z, 1, lambda)))].