============================== Mace4 =================================
Mace4 (32) version June-2007, June 2007.
Process 8115 was started by zalta on mally,
Tue Jul 24 18:01:32 2007
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 (exemplifies1(F,x) -> relation1(F) & object(x))).
(all x all F (is_the(x,F) -> relation1(F) & object(x))).
(all F all x all w (relation1(F) & object(x) & object(w) -> (is_the(x,F) & x = w <-> (exists y (object(y) & exemplifies1(F,y) & (all z (object(z) -> (exemplifies1(F,z) -> z = y))) & y = w))))).
end_of_list.

formulas(goals).
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 (exemplifies1(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 F all x all w (relation1(F) & object(x) & object(w) -> (is_the(x,F) & x = w <-> (exists y (object(y) & exemplifies1(F,y) & (all z (object(z) -> (exemplifies1(F,z) -> z = y))) & y = w))))) # label(non_clause).  [assumption].

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

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

formulas(mace4_clauses).
-object(x) | -relation1(x).
-exemplifies1(x,y) | relation1(x).
-exemplifies1(x,y) | object(y).
-is_the(x,y) | relation1(y).
-is_the(x,y) | object(x).
-relation1(x) | -object(y) | -object(z) | -is_the(y,x) | z != y | object(f1(x,y,z)).
-relation1(x) | -object(y) | -object(z) | -is_the(y,x) | z != y | exemplifies1(x,f1(x,y,z)).
-relation1(x) | -object(y) | -object(z) | -is_the(y,x) | z != y | -object(u) | -exemplifies1(x,u) | u = f1(x,y,z).
-relation1(x) | -object(y) | -object(z) | -is_the(y,x) | z != y | f1(x,y,z) = z.
-relation1(x) | -object(y) | -object(z) | is_the(y,x) | -object(u) | -exemplifies1(x,u) | object(f2(x,y,z,u)) | u != z.
-relation1(x) | -object(y) | -object(z) | is_the(y,x) | -object(u) | -exemplifies1(x,u) | exemplifies1(x,f2(x,y,z,u)) | u != z.
-relation1(x) | -object(y) | -object(z) | is_the(y,x) | -object(u) | -exemplifies1(x,u) | f2(x,y,z,u) != u | u != z.
-relation1(x) | -object(y) | -object(z) | z = y | -object(u) | -exemplifies1(x,u) | object(f2(x,y,z,u)) | u != z.
-relation1(x) | -object(y) | -object(z) | z = y | -object(u) | -exemplifies1(x,u) | exemplifies1(x,f2(x,y,z,u)) | u != z.
-relation1(x) | -object(y) | -object(z) | z = y | -object(u) | -exemplifies1(x,u) | f2(x,y,z,u) != u | u != 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.
f1(0,0,0) = 0.
f1(0,0,1) = 0.
f1(0,1,0) = 0.
f1(0,1,1) = 0.
f1(1,0,0) = 0.
f1(1,0,1) = 0.
f1(1,1,0) = 0.
f1(1,1,1) = 0.
f2(0,0,0,0) = 0.
f2(0,0,0,1) = 0.
f2(0,0,1,0) = 0.
f2(0,0,1,1) = 0.
f2(0,1,0,0) = 0.
f2(0,1,0,1) = 0.
f2(0,1,1,0) = 0.
f2(0,1,1,1) = 0.
f2(1,0,0,0) = 0.
f2(1,0,0,1) = 0.
f2(1,0,1,0) = 0.
f2(1,0,1,1) = 0.
f2(1,1,0,0) = 0.
f2(1,1,0,1) = 0.
f2(1,1,1,0) = 0.
f2(1,1,1,1) = 0.

 object :
        0 1
    -------
        0 0

 relation1 :
        0 1
    -------
        0 0

 exemplifies1 :
      | 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=154, kept=74.
Selections=28, assignments=28, propagations=8, current_models=1.
Rewrite_terms=56, rewrite_bools=92, indexes=4.
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 8115 exit (max_models) Tue Jul 24 18:01:32 2007
The process finished Tue Jul 24 18:01:32 2007