:- use_module(cdtools(working_cd)).
:- use_module(cdtools(ccs_main_cd)).

:- flag(minsize, _, 1000000).

cdex_options([]).

solve(P, D) :-
	flag(minsize, _, 1000000),
	between(0, 100000, I),
	try_with_time_limit(-1,
			    (ccs(P, [once=multi,
				     format=cd,
				     gen=[d(_,_)],
				     min_level=I,
				     max_level=I,
				     proof=D,
				     proof_level=J]),
			     d_to_gr(D, G),
			     gr_to_fsk(G, S,[lambda_optim=2,simp=red]),
			     sk_ocsize(S, X),
			     flag(minsize, M, M),
			     d_to_dc(D, D1),
			     ( M > X ->
			       \+ \+ ( numbervars(D1, 0, _), writeq(compression(P, X, J, D1)) ),
			       writeln('.'),
			       M1 is min(M,X),
			      flag(minsize, _, M1),
			       fail
			     ; fail
			     ))).