set(auto).
assign(pick_given_ratio, 2).

assign(max_weight, 48).

terms(weights).
e(x,x) = 1000.
end_of_list.

clauses(usable).
-P(e(x,y)) | -P(x) | P(y).
end_of_list.
  
clauses(sos).
P(e(x,e(e(e(x,y),e(z,y)),z))) # label(XCB).
end_of_list.
  
clauses(denials).
-P(e(e(e(a,b),c),e(b,e(c,a)))) # answer(UM).
-P(e(e(a,b),e(e(c,b),e(a,c)))) # answer(YQL).
-P(e(e(a,b),e(e(a,c),e(c,b)))) # answer(YQF).
-P(e(e(a,b),e(e(c,a),e(b,c)))) # answer(YQJ).
-P(e(a,e(e(b,e(a,c)),e(c,b)))) # answer(XGF).
-P(e(e(a,e(b,c)),e(c,e(a,b)))) # answer(WN).
-P(e(e(a,b),e(c,e(e(b,c),a)))) # answer(YRM).
-P(e(e(a,b),e(c,e(e(c,b),a)))) # answer(YRO).
-P(e(e(e(a,e(b,c)),c),e(b,a))) # answer(PYO).
-P(e(e(e(a,e(b,c)),b),e(c,a))) # answer(PYM).
-P(e(a,e(e(b,e(c,a)),e(c,b)))) # answer(XGK).
-P(e(a,e(e(b,c),e(e(a,c),b)))) # answer(XHK).
-P(e(a,e(e(b,c),e(e(c,a),b)))) # answer(XHN).
end_of_list.