----- 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-------
op(400,infix,^).
op(400,infix,v).

list(sos).
0 [] x v (y v z)=y v (x v z).
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 [] x v c(x)=1.
0 [] c(1)=0.
0 [] A v (B^ (A v C))!=A v (C^ (A v B)).
end_of_list.

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

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

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

Applying isomorphism constraints to constants: C B A.

305 clauses were generated; 280 of those survived the first stage
of unit preprocessing; there are 112 atoms.

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

----- statistics for domain size 2 ----
Input:
    Clauses input                   280
    Literal occurrences input       866
    Greatest atom                   112
Unit preprocess:
    Preprocess unit assignments      86
    Clauses after subsumption        22
    Literal occ. after subsump.      84
    Selectable clauses                3
Decide:
    Splits                            3
    Unit assignments                 10
    Failed paths                      4
Memory:
    Memory malloced                 3 K
    Memory MACE_tp_alloced       4882 K
Time (seconds):
    Generate ground clauses        0.00
    DPLL                           0.00

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

Applying isomorphism constraints to constants: C B A.

1909 clauses were generated; 1826 of those survived the first stage
of unit preprocessing; there are 462 atoms.

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

----- statistics for domain size 3 ----
Input:
    Clauses input                  1826
    Literal occurrences input      6030
    Greatest atom                   462
Unit preprocess:
    Preprocess unit assignments      99
    Clauses after subsumption       806
    Literal occ. after subsump.    2665
    Selectable clauses               14
Decide:
    Splits                            0
    Unit assignments                  0
    Failed paths                      1
Memory:
    Memory malloced                13 K
    Memory MACE_tp_alloced       4882 K
Time (seconds):
    Generate ground clauses        0.00
    DPLL                           0.00

--- Starting search for models of size 4 ---

Applying isomorphism constraints to constants: C B A.

7437 clauses were generated; 7241 of those survived the first stage
of unit preprocessing; there are 1328 atoms.

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

----- statistics for domain size 4 ----
Input:
    Clauses input                  7241
    Literal occurrences input     24411
    Greatest atom                  1328
Unit preprocess:
    Preprocess unit assignments     146
    Clauses after subsumption      4800
    Literal occ. after subsump.   16111
    Selectable clauses               36
Decide:
    Splits                           10
    Unit assignments                775
    Failed paths                     11
Memory:
    Memory malloced                37 K
    Memory MACE_tp_alloced       4882 K
Time (seconds):
    Generate ground clauses        0.00
    DPLL                           0.00

--- Starting search for models of size 5 ---

Applying isomorphism constraints to constants: C B A.

21732 clauses were generated; 21350 of those survived the first stage
of unit preprocessing; there are 3070 atoms.

After all unit preprocessing, 2891 atoms are still unassigned;
16355 clauses remain; 61 of those are non-Horn (selectable);
4969 K allocated; cpu time so far for this domain size: 0.02 sec.

----- statistics for domain size 5 ----
Input:
    Clauses input                 21350
    Literal occurrences input     72656
    Greatest atom                  3070
Unit preprocess:
    Preprocess unit assignments     179
    Clauses after subsumption     16355
    Literal occ. after subsump.   55437
    Selectable clauses               61
Decide:
    Splits                           20
    Unit assignments               3655
    Failed paths                     21
Memory:
    Memory malloced                87 K
    Memory MACE_tp_alloced       4882 K
Time (seconds):
    Generate ground clauses        0.02
    DPLL                           0.00

--- Starting search for models of size 6 ---

Applying isomorphism constraints to constants: C B A.

52617 clauses were generated; 51958 of those survived the first stage
of unit preprocessing; there are 6144 atoms.

After all unit preprocessing, 5930 atoms are still unassigned;
43050 clauses remain; 85 of those are non-Horn (selectable);
5056 K allocated; cpu time so far for this domain size: 0.04 sec.

======================= Model #1 at 0.20 seconds:
interpretation( 6, [

        function(v(_,_), [
                0, 1, 2, 3, 4, 5,
                1, 1, 1, 1, 1, 1,
                2, 1, 2, 1, 1, 5,
                3, 1, 1, 3, 3, 1,
                4, 1, 1, 3, 4, 1,
                5, 1, 5, 1, 1, 5    ]),

        function(^(_,_), [
                0, 0, 0, 0, 0, 0,
                0, 1, 2, 3, 4, 5,
                0, 2, 2, 0, 0, 2,
                0, 3, 0, 3, 4, 0,
                0, 4, 0, 4, 4, 0,
                0, 5, 2, 0, 0, 5    ]),

        function(c(_), [1, 0, 3, 2, 5, 4]),

        function(C, [2]),

        function(B, [3]),

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

----- statistics for domain size 6 ----
Input:
    Clauses input                 51958
    Literal occurrences input    177751
    Greatest atom                  6144
Unit preprocess:
    Preprocess unit assignments     214
    Clauses after subsumption     43050
    Literal occ. after subsump.  146805
    Selectable clauses               85
Decide:
    Splits                          132
    Unit assignments              72674
    Failed paths                    130
Memory:
    Memory malloced               174 K
    Memory MACE_tp_alloced       4882 K
Time (seconds):
    Generate ground clauses        0.03
    DPLL                           0.15

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

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

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