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

:- flag(minsize, _, 1000000).

cdex_options([once=false,
	      gen=Gen,
 	      test=[lt_fh(truncate(input*FactorH)+1),
 		    lt_ft(truncate(input*FactorT)+1),
 		    lt_subs],
	      max_level=1000000,
%	      test=[lt_fh(7),lt_ft(18),lt_subs],
	      process_news=reg_first([],[ipt_mgt,red_n],[])]) :-
	Gen = inc_psp1,
	FactorH = 2,
	FactorT = 3.

solve(P, D) :-
	flag(minsize, _, 1000000),
	tptpcd_problem_install(P, [goal=Goal]),
	cdex_options(Opts),
	( sgcd([proof=D, goal=Goal|Opts]),
	  d_csize(D, 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
	  )
	).