============================== Mace4 =================================
Mace4 (32) version June-2006B, June 2006.
Process 3689 was started by zalta on mally,
Wed Jun 14 17:01:42 2006
The command was "mace -c -N 8 -p 1".
============================== end of head ===========================

============================== INPUT =================================
set(auto2).
WARNING, flag not recognized: set(auto2).

formulas(sos).
Point(W).
(all F all G (Property(F) & Property(G) -> (Implies(F,G) <-> (all x all w (Point(w) -> (Ex1(F,x,w) -> Ex1(G,x,w))))))).
(all x all G (Object(x) & Property(G) -> (IsAFormOf(x,G) <-> Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))).
(all x all y all w (Object(x) & Object(y) & Point(w) -> (PartPTA(x,y,w) <-> (exists F (Property(F) & IsTheFormOf(y,F) & Ex1(F,x,w)))))).
(all x all G (Object(x) & Property(G) -> (IsTheFormOf(x,G) <-> IsAFormOf(x,G) & (all y (IsAFormOf(y,G) -> y = x))))).
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 ==========================

% The maximum domain element in the input is 0.

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

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

% Model 1 at 0.00 seconds.

 A : 0

 W : 0

 f1 :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0

 f2 :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0

 f3 :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0

 f5 :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0
f4(0,0,0) = 0.
f4(0,0,1) = 0.
f4(0,1,0) = 0.
f4(0,1,1) = 0.
f4(1,0,0) = 0.
f4(1,0,1) = 0.
f4(1,1,0) = 0.
f4(1,1,1) = 0.

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

 Point :
        0 1
    -------
        1 0

 Property :
        0 1
    -------
        0 0

 Enc :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0

 Implies :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0

 IsAFormOf :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0

 IsTheFormOf :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0
Ex1(0,0,0) = 0.
Ex1(0,0,1) = 0.
Ex1(0,1,0) = 0.
Ex1(0,1,1) = 0.
Ex1(1,0,0) = 0.
Ex1(1,0,1) = 0.
Ex1(1,1,0) = 0.
Ex1(1,1,1) = 0.
PartPTA(0,0,0) = 0.
PartPTA(0,0,1) = 0.
PartPTA(0,1,0) = 0.
PartPTA(0,1,1) = 0.
PartPTA(1,0,0) = 0.
PartPTA(1,0,1) = 0.
PartPTA(1,1,0) = 0.
PartPTA(1,1,1) = 0.

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

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

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=121, kept=117.
Selections=63, assignments=63, propagations=1, current_models=1.
Rewrite_terms=105, rewrite_bools=149, indexes=52.
Rules_from_neg_clauses=0, cross_offs=0.

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

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

Exiting with 1 model.

Process 3689 exit (max_models) Wed Jun 14 17:01:42 2006
The process finished Wed Jun 14 17:01:42 2006