%set(hyper_res).
%set(neg_hyper_res).
set(binary_res).
%set(interactive_given).
%set(sos_queue).
%set(auto).
set(para_into).
%set(para_into_left).
%set(para_into_right).
%set(para_from).
%set(para_into_units_only).
%set(para_all).
%set(demod_inf).
%set(order_eq).
%set(back_unit_deletion).
%set(dynamic_demod).
%assign(max_weight, 50).
%assign(max_literals, 8).
assign(max_distinct_vars, 2).
%set(print_kept).
assign(fpa_terms, 20).
assign(stats_level,1).
%assign(max_proofs, 110).

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

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

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([x|xs], ys) = [x| app(xs, ys)]).

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

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(0)), 1) != x | $ans(x).

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

%list(passive).
%hanoi(s(0), 1) != y | y != [z] | $ans3(z).
%hanoi(s(s(0)), 1) != z | $ans4(z).
%end_of_list.

