FOIL 6.4   [January 1996]
--------

Relation *dec

Relation *mult

Relation choose

----------
choose:

State (21/210, 113.0 bits available)

Determinate literals
	dec(C,D)
	mult(A,A,D) ->mult(A,A,E)
	mult(A,B,D) ->mult(A,B,F)
	mult(A,C,D) ->mult(A,C,G)
	mult(B,A,D) ->mult(B,A,H) H=F (no new vars)
	mult(B,B,D) ->mult(B,B,H)
	mult(B,C,D) ->mult(B,C,I)
	mult(C,A,D) ->mult(C,A,J) J=G (no new vars)
	mult(C,B,D) ->mult(C,B,J) J=I (no new vars)
	mult(C,C,D) ->mult(C,C,J)

State (21/210, 113.0 bits available)

Determinate literals
	mult(A,D,K)
	mult(B,D,K) ->mult(B,D,L)
	mult(C,D,K) ->mult(C,D,M)
	mult(D,A,K) ->mult(D,A,N) N=K (no new vars)
	mult(D,B,K) ->mult(D,B,N) N=L (no new vars)
	mult(D,C,K) ->mult(D,C,N) N=M (no new vars)
	mult(D,D,K) ->mult(D,D,N)

State (21/210, 113.0 bits available)

	Save clause ending with F=M (cover 10, accuracy 100%)

	Save mult(A,D,M) (18,39 value 39.4)
	Save mult(C,D,K) (18,39 value 39.4)
	Save mult(D,A,M) (18,39 value 39.4)
	Save mult(D,C,K) (18,39 value 39.4)

Best literal K=M (9.8 bits)

State (18/39, 92.5 bits available)

	Save mult(I,B,F) (15,19 value 44.1)
	Save A=I (10,10 value 32.6)
	Save B=D (10,10 value 32.6)
	Save F=K (10,10 value 32.6)

Best literal mult(B,I,F) (14.5 bits)

State (15/19, 67.3 bits available)

	Save clause ending with D=L (cover 15, accuracy 100%)

	Save L=N (12,12 value 39.1)

Best literal D=L (9.6 bits)

Clause 0: choose(A,B,C) :- dec(C,D), mult(A,B,E), mult(B,C,F), mult(B,D,D), mult(B,F,E).

State (6/195, 48.8 bits available)

Determinate literals
	dec(A,D)
	dec(B,D) ->dec(B,E)
	dec(C,D) ->dec(C,F)
	mult(A,A,D) ->mult(A,A,G)
	mult(A,B,D) ->mult(A,B,H)
	mult(A,C,D) ->mult(A,C,I)
	mult(B,A,D) ->mult(B,A,J) J=H (no new vars)
	mult(B,B,D) ->mult(B,B,J)
	mult(B,C,D) ->mult(B,C,K)
	mult(C,A,D) ->mult(C,A,L) L=I (no new vars)
	mult(C,B,D) ->mult(C,B,L) L=K (no new vars)
	mult(C,C,D) ->mult(C,C,L)

State (6/141, 48.8 bits available)

Determinate literals
	choose(A,E,M)
	choose(D,B,M) ->choose(D,B,N)
	choose(D,E,M) ->choose(D,E,O)
	mult(A,D,M) ->mult(A,D,P)
	mult(A,E,M) ->mult(A,E,Q)
	mult(A,F,M) ->mult(A,F,R)
	mult(B,D,M) ->mult(B,D,S)
	mult(B,E,M) ->mult(B,E,T)
	mult(B,F,M) ->mult(B,F,U)
	mult(C,D,M) ->mult(C,D,V)
	mult(C,E,M) ->mult(C,E,W)
	mult(C,F,M) ->mult(C,F,X)
	mult(D,A,M) ->mult(D,A,Y) Y=P (no new vars)
	mult(D,B,M) ->mult(D,B,Y) Y=S (no new vars)
	mult(D,C,M) ->mult(D,C,Y) Y=V (no new vars)
	mult(D,D,M) ->mult(D,D,Y)
	mult(D,E,M) ->mult(D,E,Z)
	mult(D,F,M) ->mult(D,F,AA)
	mult(E,A,M) ->mult(E,A,AB) AB=Q (no new vars)
	mult(E,B,M) ->mult(E,B,AB) AB=T (no new vars)
	mult(E,C,M) ->mult(E,C,AB) AB=W (no new vars)
	mult(E,D,M) ->mult(E,D,AB) AB=Z (no new vars)
	mult(E,E,M) ->mult(E,E,AB)
	mult(E,F,M) ->mult(E,F,AC)
	mult(F,A,M) ->mult(F,A,AD) AD=R (no new vars)
	mult(F,B,M) ->mult(F,B,AD) AD=U (no new vars)
	mult(F,C,M) ->mult(F,C,AD) AD=X (no new vars)
	mult(F,D,M) ->mult(F,D,AD) AD=AA (no new vars)
	mult(F,E,M) ->mult(F,E,AD) AD=AC (no new vars)
	mult(F,F,M) ->mult(F,F,AD)

State (6/96, 48.8 bits available)

	Save clause ending with mult(A,O,K) (cover 6, accuracy 100%)

Best literal mult(A,O,K) (18.1 bits)

Clause 1: choose(A,B,C) :- dec(A,D), dec(B,E), mult(B,C,F), choose(D,E,G), mult(A,G,F).

choose(A,B,C) :- dec(C,D), mult(A,B,E), mult(B,C,F), mult(B,D,D), mult(B,F,E).
choose(A,B,C) :- dec(A,D), dec(B,E), mult(B,C,F), choose(D,E,G), mult(A,G,F).

Time 1.7 secs