%set(auto).
%set(sos_stack).
%set(sos_queue).
%set(binary_res).
set(hyper_res).
%set(print_proof_as_hints).
%clear(factor).
%set(print_kept).
%set(sos_queue).
assign(max_weight,3995).
assign(max_distinct_vars,552).
assign(max_literals,310).
set(prolog_style_variables).
%set(input_sos_first).
%lex([antimv,cw,ac,s,0,hanoi,app]).
%weight_list(pick_given).
%weight(hanoi($dots(0),$dots(cw),$dots(X)),1000).
%weight(hanoi($dots(0),$dots(ac),$dots(X)),1000).
%end_of_list.

assign(stats_level, 1).
formula_list(usable).
all n d ad x y z xyz ((antimv(d,ad) &
		    hanoi(n, ad, x) & 
                    hanoi(n, ad, z) & 
                    app(x,[d | z], xyz))
                   -> hanoi(s(n), d, xyz)).

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

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

formula_list(sos).
all d (hanoi(0, d, [])).
all d (hanoi(s(0),d,[d])).
all y app([],y,y).
mv(cw,[cw]).
mv(ac,[ac]).
antimv(cw,ac).
antimv(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).
%-hanoi(s(s(s(s(s(s(0)))))), cw, X) | $ans(X).
% -hanoi(s(s(s(s(s(s(s(0))))))), cw, X) | $ans(X).
 -hanoi(s(s(s(s(s(s(s(s(0)))))))), cw, X) | $ans(X).
end_of_list.


