============================== Mace4 =================================
Mace4 (32) version June-2006B, June 2006.
Process 30324 was started by zalta on mally,
Fri Sep 11 16:58:18 2009
The command was "mace.orig -c -N 8 -p 1".
============================== end of head ===========================

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

formulas(sos).
(all x (Object(x) -> ((exists d (Point(d) & Ex1At(A,x,d))) -> (all d (Point(d) -> Ex1At(A,x,d)))))).
(all x all F (Object(x) & Property(F) -> ((exists d (Point(d) & EncAt(x,F,d))) -> (all d (Point(d) -> EncAt(x,F,d)))))).
(all x all d (Object(x) & Point(d) -> (WorldAt(x,d) <-> SituationAt(x,d) & (exists d2 (Point(d2) & (all p (Proposition(p) -> (TrueInAt(p,x,d2) <-> True(p,d2))))))))).
(all p all x all d (Object(x) & Proposition(p) & Point(d) -> (TrueInAt(p,x,d) <-> EncpAt(x,p,d)))).
(all x all d (Object(x) & Point(d) -> (SituationAt(x,d) <-> Ex1At(A,x,d) & (all F (Property(F) -> (EncAt(x,F,d) -> (exists p (Proposition(p) & F = VAC(p))))))))).
(all x all p all d (Object(x) & Proposition(p) & Point(d) -> (EncpAt(x,p,d) <-> (exists F (Property(F) & F = VAC(p) & EncAt(x,F,d)))))).
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

 VAC :
        0 1
    -------
        0 0

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

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

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

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

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

 Proposition :
        0 1
    -------
        0 0

 SituationAt :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0

 True :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0

 WorldAt :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 0
EncAt(0,0,0) = 0.
EncAt(0,0,1) = 0.
EncAt(0,1,0) = 0.
EncAt(0,1,1) = 0.
EncAt(1,0,0) = 0.
EncAt(1,0,1) = 0.
EncAt(1,1,0) = 0.
EncAt(1,1,1) = 0.
EncpAt(0,0,0) = 0.
EncpAt(0,0,1) = 0.
EncpAt(0,1,0) = 0.
EncpAt(0,1,1) = 0.
EncpAt(1,0,0) = 0.
EncpAt(1,0,1) = 0.
EncpAt(1,1,0) = 0.
EncpAt(1,1,1) = 0.
Ex1At(0,0,0) = 0.
Ex1At(0,0,1) = 0.
Ex1At(0,1,0) = 0.
Ex1At(0,1,1) = 0.
Ex1At(1,0,0) = 0.
Ex1At(1,0,1) = 0.
Ex1At(1,1,0) = 0.
Ex1At(1,1,1) = 0.
TrueInAt(0,0,0) = 0.
TrueInAt(0,0,1) = 0.
TrueInAt(0,1,0) = 0.
TrueInAt(0,1,1) = 0.
TrueInAt(1,0,0) = 0.
TrueInAt(1,0,1) = 0.
TrueInAt(1,1,0) = 0.
TrueInAt(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=164, kept=164.
Selections=87, assignments=87, propagations=0, current_models=1.
Rewrite_terms=208, rewrite_bools=176, indexes=100.
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 30324 exit (max_models) Fri Sep 11 16:58:18 2009
The process finished Fri Sep 11 16:58:18 2009