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

Relation Ackermann

Relation *succ

----------
Ackermann:

State (51/9261, 511.6 bits available)

Determinate literals
	succ(A,D)
	succ(B,D) ->succ(B,E)
	succ(D,C) ->succ(F,C)

State (51/8000, 511.6 bits available)

	Save D=1 (20,400 value 64.4)
	Save B=F (20,400 value 64.4)
	Save C=E (20,400 value 64.4)
	Save succ(B,C) (20,400 value 64.4)

Best literal A=0 (6.6 bits)

State (20/400, 230.6 bits available)

	Save clause ending with B=F (cover 20, accuracy 100%)

	Save C=E (20,20 value 149.5)

Best literal B=F (6.9 bits)

Clause 0: Ackermann(A,B,C) :- A=0, succ(B,C).

State (31/9241, 339.8 bits available)

Determinate literals
	succ(A,D)
	succ(B,D) ->succ(B,E)
	succ(D,A) ->succ(F,A)
	succ(D,C) ->succ(G,C)

State (31/7600, 339.8 bits available)

Determinate literals
	Ackermann(F,B,H)
	Ackermann(F,E,H) ->Ackermann(F,E,I)

State (31/920, 339.8 bits available)

Determinate literals
	succ(H,J)
	succ(J,H) ->succ(K,H)
	succ(J,I) ->succ(L,I)

State (31/920, 339.8 bits available)

	Save G=L (22,46 value 157.1)
	Save Ackermann(F,E,C) (22,46 value 157.1)
	Save succ(G,I) (22,46 value 157.1)
	Save succ(L,C) (22,46 value 157.1)

Best literal C=I (9.0 bits)

State (22/46, 247.4 bits available)

	Save clause ending with A=1 (cover 19, accuracy 100%)

	Save F=0 (19,19 value 155.3)
	Save B=K (19,19 value 155.3)
	Save E=G (19,19 value 155.3)
	Save E=H (19,19 value 155.3)

Best literal A=1 (7.3 bits)

[Regrow clause] Ackermann(A,B,C) :- A=1.

State (19/441, 220.1 bits available)

Determinate literals
	succ(B,D)
	succ(D,C) ->succ(E,C) E=D (no new vars)

State (19/420, 220.1 bits available)

Best literal succ(D,C) (6.9 bits)

Clause 1: Ackermann(A,B,C) :- A=1, succ(B,D), succ(D,C).

State (12/9222, 156.7 bits available)

Determinate literals
	succ(A,D)
	succ(B,D) ->succ(B,E)
	succ(C,D) ->succ(C,F)
	succ(D,A) ->succ(G,A)
	succ(D,C) ->succ(H,C)

State (12/7202, 156.7 bits available)

Determinate literals
	Ackermann(G,B,I)
	Ackermann(G,E,I) ->Ackermann(G,E,J)

State (12/856, 156.7 bits available)

Determinate literals
	succ(I,K)
	succ(J,K) ->succ(J,L)
	succ(K,I) ->succ(M,I)
	succ(K,J) ->succ(N,J)

State (12/818, 156.7 bits available)

	Save F=L (3,26 value 20.1)
	Save H=N (3,26 value 20.1)
	Save Ackermann(G,E,C) (3,26 value 20.1)
	Save succ(C,L) (3,26 value 20.1)

Best literal C=J (9.5 bits)

State (3/26, 45.6 bits available)

	Save clause ending with B=0 (cover 3, accuracy 100%)

	Save E=1 (3,3 value 28.4)

Best literal B=0 (7.5 bits)

[Regrow clause] Ackermann(A,B,C) :- B=0.

State (3/439, 47.7 bits available)

Determinate literals
	succ(A,D)
	succ(C,D) ->succ(C,E)
	succ(D,A) ->succ(F,A)
	succ(D,C) ->succ(G,C)

State (3/360, 47.7 bits available)

Determinate literals
	Ackermann(B,D,H)
	Ackermann(B,E,H) ->Ackermann(B,E,I)
	Ackermann(F,B,H) ->Ackermann(F,B,J)

State (3/89, 47.7 bits available)

Determinate literals
	Ackermann(B,H,K)
	Ackermann(B,I,K) ->Ackermann(B,I,L)
	Ackermann(B,J,K) ->Ackermann(B,J,M)
	succ(H,K) ->succ(H,N) N=K (no new vars)
	succ(I,K) ->succ(I,N) N=L (no new vars)
	succ(J,K) ->succ(J,N) N=M (no new vars)
	succ(K,J) ->succ(N,J)

State (3/84, 47.7 bits available)

Determinate literals
	Ackermann(B,K,O)
	Ackermann(B,L,O) ->Ackermann(B,L,P)
	Ackermann(B,M,O) ->Ackermann(B,M,Q)
	succ(K,O) ->succ(K,R) R=O (no new vars)
	succ(L,O) ->succ(L,R) R=P (no new vars)
	succ(M,O) ->succ(M,R) R=Q (no new vars)

State (3/79, 47.7 bits available)

	Save Ackermann(F,J,P) (1,1 value 9.5)
	Save Ackermann(F,C,K) (1,2 value 8.9)
	Save Ackermann(F,F,I) (1,2 value 8.9)
	Save Ackermann(F,N,I) (1,2 value 8.9)

Best literal Ackermann(F,A,P) (12.2 bits)

[Replace by saved clause]

Clause 2: Ackermann(A,B,C) :- B=0, succ(B,D), succ(E,A), Ackermann(E,D,C).

State (9/9219, 124.6 bits available)

Determinate literals
	succ(A,D)
	succ(B,D) ->succ(B,E)
	succ(C,D) ->succ(C,F)
	succ(D,A) ->succ(G,A)
	succ(D,B) ->succ(H,B)
	succ(D,C) ->succ(I,C)

State (9/6842, 124.6 bits available)

Determinate literals
	Ackermann(A,H,J)
	Ackermann(G,A,J) ->Ackermann(G,A,K)
	Ackermann(G,B,J) ->Ackermann(G,B,L)
	Ackermann(G,D,J) ->Ackermann(G,D,M)
	Ackermann(G,E,J) ->Ackermann(G,E,N)
	Ackermann(G,G,J) ->Ackermann(G,G,O)
	Ackermann(G,H,J) ->Ackermann(G,H,P)

State (9/534, 124.6 bits available)

	Save clause ending with Ackermann(G,J,C) (cover 9, accuracy 100%)

Best literal Ackermann(G,J,C) (11.0 bits)

Clause 3: Ackermann(A,B,C) :- succ(D,A), succ(E,B), Ackermann(A,E,F), Ackermann(D,F,C).

Delete clause
	Ackermann(A,B,C) :- A=1, succ(B,D), succ(D,C).

Ackermann(0,B,C) :- succ(B,C).
Ackermann(A,0,C) :- succ(0,D), succ(E,A), Ackermann(E,D,C).
Ackermann(A,B,C) :- succ(D,A), succ(E,B), Ackermann(A,E,F), Ackermann(D,F,C).

Time 7.7 secs