%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%% Resolution and Demodulation 
%%%%%%%%%%%%%%%%%%%%%%%%%

%set(auto).

% resolution flags

%set(hyper_res).
%set(neg_hyper_res).
set(binary_res).

% demodulation settings

set(demod_inf).
%set(demod_out_in).
%set(index_for_back_demod).
%set(lrpo).
%set(lex_order_vars).
%set(eq_units_both_ways).
%set(demod_linear).
%set(order_eq).
%assign(demod_limit,3).

% weight
set(atom_wt_max_args).
%set(term_wt_max_args).
%assign(neg_weight, 1000).

% sos ordering
%assign(max_levels, 7).
%set(interactive_given).
%set(sos_stack).
%set(sos_queue).
%assign(max_literals, 4).
assign(max_answers, 1).
%set(interactive_given).

%assign(pick_given_ratio, 150).
assign(max_distinct_vars, 18).
%set(print_kept).
%assign(fpa_literals,5).
%assign(fpa_terms, 20).
%assign(max_proofs, 110).

%lex([mv(_,_),hanoi(_,_),app(_,_),app3(_,_)]).

% output format 

assign(stats_level,1).

make_evaluable(_-_,$DIFF(_,_)).

formula_list(usable).
all d (hanoi(0, d)= []).
all n d x y z xyz (((hanoi(n, (1-d))=x) & 
                     (mv(s(n), d)= y) & 
                     (hanoi(n, (1-d))= z) & 
                     (app3(x, y, z) =  xyz))
                   -> (hanoi(s(n), d)= xyz)).

all n (mv(n, 1) = [ACW(n)]).
all n (mv(n, 0) = [CW(n)]).

all y (app([],y) = y).
all x xs ys zs ((app(xs, ys) =  zs) -> (app([x|xs], ys) = [x|zs])).

all x w xw y z (((app(x, w) = xw) & (app(xw, y) = z)) -> (app3(x, w, y) =  z)).

end_of_list.

%list(hints).
%-(hanoi(x, y) = z).
%end_of_list.

assign(fsub_hint_wt,0).

list(sos).
%hanoi(0, 1) != x | $ans(x).
%hanoi(s(0), 1) != [x|xs] | $ans([x|xs]).
%hanoi(s(s(0)), 1) != [x|xs] | $ans([x|xs]).

hanoi(s(s(s(0))), 1) != [x | xs] | $ans([x|xs]).
%hanoi(s(s(s(s(0)))), 1) != [x | xs] | $ans([x|xs]).
end_of_list.


