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

============================== INPUT =================================
op(300,prefix,~).

formulas(sos).
(all x all d (Object(x) & Point(d) -> (ActualAt(x,d) <-> SituationAt(x,d) & (all p (Proposition(p) -> (TrueInAt(p,x,d) -> True(p,d))))))).
(all p (Proposition(p) -> Proposition(~ p))).
(all d all p (Point(d) & Proposition(p) -> (True(~ p,d) <-> - True(p,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 x (Object(x) -> ((exists d (Point(d) & WorldAt(x,d))) -> (all d (Point(d) -> WorldAt(x,d)))))).
(all x all p (Object(x) & Proposition(p) -> ((exists d (Point(d) & EncpAt(x,p,d))) -> (all d (Point(d) -> EncpAt(x,p,d)))))).
(all p all x all d (Object(x) & Proposition(p) & Point(d) -> (TrueInAt(p,x,d) <-> EncpAt(x,p,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.

 ~ :
        0 1
    -------
        0 0

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

 f2 :
      | 0 1
    --+----
    0 | 0 0
    1 | 0 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.

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

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

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

 ActualAt :
      | 0 1
    --+----
    0 | 0 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
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.
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=122, kept=122.
Selections=55, assignments=55, propagations=1, current_models=1.
Rewrite_terms=98, rewrite_bools=127, indexes=65.
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 30284 exit (max_models) Fri Sep 11 16:54:07 2009
The process finished Fri Sep 11 16:54:07 2009