============================== Mace4 =================================
Mace4 (32) version 22-May-2007, May 2007.
Process 26980 was started by mccune on cleo,
Tue May 22 14:44:22 2007
The command was "/home/mccune/bin/mace4 -f toughnut.in".
============================== end of head ===========================

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

% Reading from file toughnut.in

assign(domain_size,8).
    % assign(domain_size, 8) -> assign(iterate_up_to, 0).

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

formulas(theory).
-G3(0,y).
-G4(x,0).
-G1(7,y).
-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(x1,x2) | -G1(x1,y) | G3(x2,y).
-S(x1,x2) | G1(x1,y) | -G3(x2,y).
-S(y1,y2) | -G2(x,y1) | G4(x,y2).
-S(y1,y2) | G2(x,y1) | -G4(x,y2).
end_of_list.

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

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 (all x all y (G5(x,y) <-> x = 0 & y = 0 | x = 7 & y = 7)) # label(non_clause).  [assumption].

============================== end of process non-clausal formulas ===

============================== CLAUSES FOR SEARCH ====================

formulas(mace4_clauses).
-G5(x,y) | 0 = x | 7 = x.
-G5(x,y) | 0 = x | 7 = y.
-G5(x,y) | 0 = y | 7 = x.
-G5(x,y) | 0 = y | 7 = y.
G5(x,y) | 0 != x | 0 != y.
G5(x,y) | 7 != x | 7 != y.
-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 clauses for search =============

% 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: 4.55 seconds).
Ground clauses: seen=4327, kept=1175.
Selections=165745, assignments=331490, propagations=7767377, current_models=0.
Rewrite_terms=0, rewrite_bools=26041281, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

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

User_CPU=4.55, System_CPU=0.03, Wall_clock=5.

Exiting with failure.

Process 26980 exit (exhausted) Tue May 22 14:44:27 2007
The process finished Tue May 22 14:44:27 2007