============================== Mace4 =================================
Mace4 (32) version June-2006C, June 2006.
Process 13048 was started by mccune on cleo.thornwood,
Mon Jun 19 16:40:33 2006
The command was "/home/mccune/bin/mace4 -f toughnut.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file toughnut.in

assign(domain_size,8).

formulas(theory).
(all x all y (G5(x,y) <-> x = 0 & y = 0 | x = 7 & y = 7)).
end_of_list.

clauses(theory).
- G3(0,x).
- G4(x,0).
- G1(7,x).
- G2(x,7).
S(0,1).
S(1,2).
S(2,3).
S(3,4).
S(4,5).
S(5,6).
S(6,7).
- S(x,y) | L(x,y).
- L(x,y) | - L(y,z) | L(x,z).
- L(x,y) | - L(y,z) | - S(x,z).
- L(x,y) | x != y.
G1(x,y) | G2(x,y) | G3(x,y) | G4(x,y) | G5(x,y).
- G1(x,y) | - G2(x,y).
- G1(x,y) | - G3(x,y).
- G1(x,y) | - G4(x,y).
- G1(x,y) | - G5(x,y).
- G2(x,y) | - G3(x,y).
- G2(x,y) | - G4(x,y).
- G2(x,y) | - G5(x,y).
- G3(x,y) | - G4(x,y).
- G3(x,y) | - G5(x,y).
- G4(x,y) | - G5(x,y).
- S(x,y) | - G1(x,z) | G3(y,z).
- S(x,y) | G1(x,z) | - G3(y,z).
- S(x,y) | - G2(z,x) | G4(z,y).
- S(x,y) | G2(z,x) | - G4(z,y).
end_of_list.

============================== end of input ==========================

% The maximum domain element in the input is 7.

============================== DOMAIN SIZE 8 =========================

============================== STATISTICS ============================

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 5.06 seconds).
Ground clauses: seen=4327, kept=1084.
Selections=165745, assignments=331490, propagations=7767377, current_models=0.
Rewrite_terms=0, rewrite_bools=26041140, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

User_CPU=5.06, System_CPU=0.07, Wall_clock=5.

Exiting with failure.

Process 13048 exit (exhausted) Mon Jun 19 16:40:38 2006
The process finished Mon Jun 19 16:40:38 2006