----- MACE 2.2, August 2003 -----
The process was started by mccune on gyro.thornwood,
Tue Sep 16 15:18:50 2003
The command was "mace2 -N6 -P".
include("ortholattice-header").
------- start included file ortholattice-header-------
op(400,infix,^).
op(400,infix,v).

lex([A,B,C,D,0,1,x v x,c(x),x^x,f(x,x)]).
set(anl_eq).
   dependent: set(para_from).
   dependent: set(para_into).
   dependent: clear(para_from_right).
   dependent: clear(para_into_right).
   dependent: set(para_from_vars).
   dependent: set(eq_units_both_ways).
   dependent: set(dynamic_demod_all).
   dependent: set(dynamic_demod).
   dependent: set(order_eq).
   dependent: set(back_demod).
   dependent: set(process_input).
   dependent: set(lrpo).
assign(pick_given_ratio,3).
assign(max_weight,25).
clear(detailed_history).
assign(max_seconds,60).
assign(max_mem,100000).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).
clear(print_kept).
assign(stats_level,1).

list(usable).
0 [] x=x.
end_of_list.
------- end included file ortholattice-header-------

list(usable).
0 [] x v (x^y)=x.
0 [] x^y=c(c(x) v c(y)).
0 [] c(c(x))=x.
0 [] x v c(x)=y v c(y).
0 [] A v (B v C)!=B v (A v C).
end_of_list.

list(clauses).
1 [] x=x.
2 [] x v (x^y)=x.
3 [] x^y=c(c(x) v c(y)).
4 [] c(c(x))=x.
5 [] x v c(x)=y v c(y).
6 [] A v (B v C)!=B v (A v C).
end_of_list.

list(flattened_and_parted_clauses).
1 [] x=x.
2 [] x^y!=z|x v z=x.
3 [] c(x)!=y|z v y!=u|$Connect2(x,z,u).
3 [] c(x)!=y|$Connect1(z,x,u)| -$Connect2(z,y,u).
3 [] c(x)!=y|z^u=y| -$Connect1(u,z,x).
4 [] c(x)!=y|c(y)=x.
5 [] c(x)!=y|x v y!=z|$Connect3(z).
5 [] c(x)!=y|x v y=z| -$Connect3(z).
6 [] x v y!=z|u v z!=v|C!=y|B!=u|A!=x| -$Connect4(x,y,u,v).
6 [] x v y!=z|u v z!=v|$Connect4(u,y,x,v).
end_of_list.

--- Starting search for models of size 2 ---

Applying isomorphism constraints to constants: C B A.

173 clauses were generated; 152 of those survived the first stage
of unit preprocessing; there are 64 atoms.

After all unit preprocessing, 58 atoms are still unassigned;
146 clauses remain; 12 of those are non-Horn (selectable);
4883 K allocated; cpu time so far for this domain size: 0.01 sec.

----- statistics for domain size 2 ----
Input:
    Clauses input                   152
    Literal occurrences input       436
    Greatest atom                    64
Unit preprocess:
    Preprocess unit assignments       6
    Clauses after subsumption       146
    Literal occ. after subsump.     430
    Selectable clauses               12
Decide:
    Splits                           73
    Unit assignments                652
    Failed paths                     74
Memory:
    Memory malloced                 1 K
    Memory MACE_tp_alloced       4882 K
Time (seconds):
    Generate ground clauses        0.01
    DPLL                           0.00

--- Starting search for models of size 3 ---

Applying isomorphism constraints to constants: C B A.

930 clauses were generated; 760 of those survived the first stage
of unit preprocessing; there are 219 atoms.

After all unit preprocessing, 207 atoms are still unassigned;
748 clauses remain; 25 of those are non-Horn (selectable);
4888 K allocated; cpu time so far for this domain size: 0.00 sec.

======================= Model #1 at 0.39 seconds:
interpretation( 3, [

        function(^(_,_), [
                0, 0, 0,
                1, 1, 0,
                2, 0, 2    ]),

        function(v(_,_), [
                0, 0, 0,
                1, 1, 0,
                2, 0, 2    ]),

        function(c(_), [0, 2, 1]),

        function(C, [0]),

        function(B, [0]),

        function(A, [1])
]).
end_of_model

----- statistics for domain size 3 ----
Input:
    Clauses input                   760
    Literal occurrences input      2303
    Greatest atom                   219
Unit preprocess:
    Preprocess unit assignments      12
    Clauses after subsumption       748
    Literal occ. after subsump.    2291
    Selectable clauses               25
Decide:
    Splits                        78488
    Unit assignments             681082
    Failed paths                  78475
Memory:
    Memory malloced                 6 K
    Memory MACE_tp_alloced       4882 K
Time (seconds):
    Generate ground clauses        0.00
    DPLL                           0.38

=======================================
Total times for run (seconds):
    user CPU time                  0.39   (0 hr, 0 min, 0 sec)
    system CPU time                0.00   (0 hr, 0 min, 0 sec)
    wall-clock time                0      (0 hr, 0 min, 0 sec)

Exit by max_models parameter.  The set is satisfiable (1 model(s) found).

The job finished Tue Sep 16 15:18:50 2003