set(sos_stack).
%set(sos_queue).
%set(binary_res).
set(neg_hyper_res).
%set(print_proof_as_hints).
%clear(factor).
%set(print_kept).
%set(sos_queue).
assign(max_weight,95).
assign(max_distinct_vars,15).
assign(max_literals,11).
set(prolog_style_variables).
formula_list(usable).
all d (hanoi(0, d, [])).
all d (hanoi(s(0),d,[d])).
all n d ad x y z xyz ((antimv(d,ad) &
		    hanoi(n, ad, x) & 
                    mv(d, y) & 
                    hanoi(n, ad, z) & 
                    app3(x, y, z, xyz))
                   -> hanoi(s(n), d, xyz)).

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)).

mv(cw,[cw]).
mv(ac,[ac]).
antimv(cw,ac).
antimv(ac,cw).

%hanoi(s(s(s(s(0)))), ac, [cw,ac,cw,cw,cw,ac,cw,ac,cw,ac,cw,cw,cw,ac,cw]).
end_of_list.


list(sos).
%-hanoi(s(0), cw, x) | $ans(x).
%-hanoi(s(s(0)), cw, X) | $ans(X).
%-hanoi(s(s(s(0))), cw, X) | $ans(X).
% -hanoi(s(s(s(s(0)))), cw, X) | $ans(X).
 -hanoi(s(s(s(s(0)))), ac, X) | $ans(X).
%-hanoi(s(s(s(s(s(0))))), cw, X) | $ans(X).
end_of_list.


