============================== Mace4 =================================
Mace4 (32) version June-2007, June 2007.
Process 13278 was started by zalta on mally,
Thu Oct  9 22:17:36 2008
The command was "mace -c -N 8 -p 1".
============================== end of head ===========================

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

formulas(assumptions).
(all x (Object(x) -> -Relation1(x))).
(all x all F (Ex1(F,x) -> Relation1(F) & Object(x))).
(all x all F (Is_the(x,F) -> Relation1(F) & Object(x))).
(all x all F all y (Object(x) & Relation1(F) & Object(y) -> (Is_the(x,F) & x = y -> Ex1(F,y)))).
end_of_list.

% From the command line: assign(iterate_up_to, 8).
    % set(print_models) -> clear(print_models_portable).

% From the command line: set(print_models).

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

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

% Formulas that are not ordinary clauses:
1 (all x (Object(x) -> -Relation1(x))) # label(non_clause).  [assumption].
2 (all x all F (Ex1(F,x) -> Relation1(F) & Object(x))) # label(non_clause).  [assumption].
3 (all x all F (Is_the(x,F) -> Relation1(F) & Object(x))) # label(non_clause).  [assumption].
4 (all x all F all y (Object(x) & Relation1(F) & Object(y) -> (Is_the(x,F) & x = y -> Ex1(F,y)))) # label(non_clause).  [assumption].

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

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

formulas(mace4_clauses).
-Object(x) | -Relation1(x).
-Ex1(x,y) | Relation1(x).
-Ex1(x,y) | Object(y).
-Is_the(x,y) | Relation1(y).
-Is_the(x,y) | Object(x).
-Object(x) | -Relation1(y) | -Object(z) | -Is_the(x,y) | z != x | Ex1(y,z).
end_of_list.

============================== end of clauses for search =============

% The maximum domain element in the input is 0.

============================== DOMAIN SIZE 2 =========================

============================== MODEL =================================

% Model 1 at 0.00 seconds.

 Object :
        0 1
    -------
        0 0

 Relation1 :
        0 1
    -------
        0 0

 Ex1 :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0

 Is_the :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0

============================== end of model ==========================

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

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=26, kept=22.
Selections=4, assignments=4, propagations=8, current_models=1.
Rewrite_terms=0, rewrite_bools=30, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

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

User_CPU=0.00, System_CPU=0.00, Wall_clock=0.

Exiting with 1 model.

Process 13278 exit (max_models) Thu Oct  9 22:17:36 2008
The process finished Thu Oct  9 22:17:36 2008