----- MACE 2.2, August 2003 ----- The process was started by mccune on gyro.thornwood, Tue Aug 19 14:47:15 2003 The command was "../../bin/mace2 -n2 -N6 -p". list(usable). 1 [] -P(e(x,y))| -P(x)|P(y). 2 [] P(e(e(x,y),e(e(y,z),e(z,x)))). 3 [] -P(e(a,a)). end_of_list. list(flattened_and_parted_clauses). 1 [] e(x,y)!=z| -P(z)| -P(x)|P(y). 2 [] e(x,y)!=z|e(u,x)!=v|$Connect2(y,z,u,v). 2 [] e(x,y)!=z|$Connect1(u,v,z)| -$Connect2(u,y,v,x). 2 [] e(x,y)!=z| -$Connect1(x,y,u)|$Connect3(z,u). 2 [] e(x,y)!=z|P(z)| -$Connect3(x,y). 3 [] a!=x|e(x,x)!=y| -P(y). end_of_list. --- Starting search for models of size 2 --- Applying isomorphism constraints to constants: a. 115 clauses were generated; 106 of those survived the first stage of unit preprocessing; there are 44 atoms. After all unit preprocessing, 38 atoms are still unassigned; 100 clauses remain; 4 of those are non-Horn (selectable); 4883 K allocated; cpu time so far for this domain size: 0.00 sec. ----- statistics for domain size 2 ---- Input: Clauses input 106 Literal occurrences input 292 Greatest atom 44 Unit preprocess: Preprocess unit assignments 6 Clauses after subsumption 100 Literal occ. after subsump. 286 Selectable clauses 4 Decide: Splits 3 Unit assignments 46 Failed paths 4 Memory: Memory malloced 1 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: a. 680 clauses were generated; 657 of those survived the first stage of unit preprocessing; there are 159 atoms. After all unit preprocessing, 147 atoms are still unassigned; 645 clauses remain; 9 of those are non-Horn (selectable); 4886 K allocated; cpu time so far for this domain size: 0.00 sec. ----- statistics for domain size 3 ---- Input: Clauses input 657 Literal occurrences input 1914 Greatest atom 159 Unit preprocess: Preprocess unit assignments 12 Clauses after subsumption 645 Literal occ. after subsump. 1902 Selectable clauses 9 Decide: Splits 91 Unit assignments 1982 Failed paths 92 Memory: Memory malloced 4 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: a. 2584 clauses were generated; 2540 of those survived the first stage of unit preprocessing; there are 424 atoms. After all unit preprocessing, 404 atoms are still unassigned; 2520 clauses remain; 16 of those are non-Horn (selectable); 4894 K allocated; cpu time so far for this domain size: 0.01 sec. ======================= Model #1 at 0.02 seconds: e : | 0 1 2 3 --+-------- 0 | 1 2 0 3 1 | 0 3 1 2 2 | 3 0 2 1 3 | 2 1 3 0 P : 0 1 2 3 ----------- F F T F a: 0 end_of_model  Exit by max_models parameter. The set is satisfiable (1 model(s) found). ----- statistics for domain size 4 ---- Input: Clauses input 2540 Literal occurrences input 7504 Greatest atom 424 Unit preprocess: Preprocess unit assignments 20 Clauses after subsumption 2520 Literal occ. after subsump. 7484 Selectable clauses 16 Decide: Splits 1156 Unit assignments 37799 Failed paths 1151 Memory: Memory malloced 12 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.01 DPLL 0.01 ======================================= Total times for run (seconds): user CPU time 0.02 (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 Aug 19 14:47:15 2003