x8ACOe.in

assign(max_weight, 30).
set(raw).
%clear(auto_inference).


assign(max_given, 180).
assign(order, kbo).
set(raw).
set(ordered_res).
set(breadth_first).
assign(max_literals, 5).
assign(max_depth, 5).
clear(back_subsume).
%assign(max_megs, 1).
set(binary_resolution).
%set(paramodulation).
%clear(pos_hyper_resolution).
%clear(neg_hyper_resolution). 
%clear(hyper_resolution). 
assign(literal_selection, none).
%predicate_order([N,e,p,q]).
set(predicate_elim).
list(kbo_weights).
  s = 25.
  e = 2.
  p = 3.
  q = 4.
end_of_list.
%list(actions).

 % given=50        -> set(random_given).
%  given=50       -> set(print_gen).
 

%end_of_list.
formulas(sos).


N(x) | -p(x,u) | -q(x,v) | -e(u,v).

p(s(x),a(x)*y) | -p(x,y).
q(s(x),y*a(x)) | -q(x,y).

e(x*y,u*v) | -e(x,u) | -e(y,v).
e(x*y,u*v) | -e(x,v) | -e(y,u).
p(0,1).
q(0,1).
e(x,x).
e(x*1,x).
e(x,x*1).
end_of_list.