set(auto).

assign(max_weight,50).
assign(sos_limit,15000).
assign(pick_given_ratio,4).

clear(print_given).

terms(weights).

   weight(e(x,x)) = 10.

end_of_list.

clauses(usable).

   % condensed detachment
   -P(e(x,y)) | -P(x) | P(y).

end_of_list.

clauses(sos).

   % known sufficient condition
   -P(e(a,a))
      | -P(e(e(a,b),e(b,a)))
      | -P(e(e(a,b),e(e(b,c),e(a,c)))).

end_of_list.

% single axiom candidates
clauses(assumptions).

   P(e(e(x,y),e(e(z,y),e(x,z))))  # label("YQL").
   P(e(e(x,y),e(e(x,z),e(z,y))))  # label("YQF").
   P(e(e(x,y),e(e(z,x),e(y,z))))  # label("YQJ").
   P(e(e(e(x,y),z),e(y,e(z,x))))  # label("UM").
   P(e(x,e(e(y,e(x,z)),e(z,y))))  # label("XGF").
   P(e(e(x,e(y,z)),e(z,e(x,y))))  # label("WN").
   P(e(e(x,y),e(z,e(e(y,z),x))))  # label("YRM").
   P(e(e(x,y),e(z,e(e(z,y),x))))  # label("YRO").
   P(e(e(e(x,e(y,z)),z),e(y,x)))  # label("PYO").
   P(e(e(e(x,e(y,z)),y),e(z,x)))  # label("PYM").
   P(e(x,e(e(y,e(z,x)),e(z,y))))  # label("XGK").
   P(e(x,e(e(y,z),e(e(x,z),y))))  # label("XHK").
   P(e(x,e(e(y,z),e(e(z,x),y))))  # label("XHN").
   %P(e(x,e(e(e(x,y),e(z,y)),z)))  # label("XCB").

end_of_list.

clauses(hints).

   P(e(x,x)).
   P(e(e(x,y),e(y,x))).
   P(e(e(x,y),e(e(y,z),e(x,z)))).
   
   P(e(e(x,y),e(e(z,y),e(x,z))))  # label("YQL").
   P(e(e(x,y),e(e(x,z),e(z,y))))  # label("YQF").
   P(e(e(x,y),e(e(z,x),e(y,z))))  # label("YQJ").
   P(e(e(e(x,y),z),e(y,e(z,x))))  # label("UM").
   P(e(x,e(e(y,e(x,z)),e(z,y))))  # label("XGF").
   P(e(e(x,e(y,z)),e(z,e(x,y))))  # label("WN").
   P(e(e(x,y),e(z,e(e(y,z),x))))  # label("YRM").
   P(e(e(x,y),e(z,e(e(z,y),x))))  # label("YRO").
   P(e(e(e(x,e(y,z)),z),e(y,x)))  # label("PYO").
   P(e(e(e(x,e(y,z)),y),e(z,x)))  # label("PYM").
   P(e(x,e(e(y,e(z,x)),e(z,y))))  # label("XGK").
   P(e(x,e(e(y,z),e(e(x,z),y))))  # label("XHK").
   P(e(x,e(e(y,z),e(e(z,x),y))))  # label("XHN").
   P(e(x,e(e(e(x,y),e(z,y)),z)))  # label("XCB").

end_of_list.