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

:- flag(minsize, _, 1000000).

cdex_options([once=false,
	      gen=Gen,
	      max_level=10000,
	      test=[lt_fh(truncate(input*Factor)+1),
		    lt_ft(truncate(input*Factor)+1),
		    lt_fv(truncate(input*Factor)+1),
		    lt_dup,
		    lt_subs],
	      process_news=reg([],[],
			       [an_sort([kp_f_ht]),
				an_trim(Trim)]),
	      pre_add_max=PreAddMax
	     ]) :-
	Gen = inc_height1,
	Factor = 5,
	PreAddMax = 1,
	Trim = 1000.

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