============================== Mace4 =================================
Mace4 (32) version June-2006B, June 2006.
Process 13576 was started by zalta on mally,
Sat Jul 21 16:08:13 2007
The command was "mace.orig -c -N 8 -p 1".
============================== end of head ===========================

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

formulas(sos).
Point(W).
(all p (Proposition(p) -> Proposition(~ p))).
(all w all p (Point(w) & Proposition(p) -> (True(~ p,w) <-> - True(p,w)))).
(all x (Object(x) -> (Actual(x) <-> Situation(x) & (all p (Proposition(p) -> (TrueIn(p,x) -> True(p,W))))))).
(all x (Actual(x) -> Object(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.

 W : 0

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

 f1 :
        0 1
    -------
        0 0

 Actual :
        0 1
    -------
        0 0

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

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

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

 Situation :
        0 1
    -------
        0 0

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

 TrueIn :
      | 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=25, kept=25.
Selections=21, assignments=21, propagations=2, current_models=1.
Rewrite_terms=23, rewrite_bools=38, indexes=16.
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 13576 exit (max_models) Sat Jul 21 16:08:13 2007
The process finished Sat Jul 21 16:08:13 2007