----- 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 [] f(e,x)=x. 2 [] f(g(x),x)=e. 3 [] f(f(x,y),z)=f(x,f(y,z)). 4 [] f(a,b)!=f(b,a). end_of_list. list(flattened_and_parted_clauses). 1 [] e!=x|f(x,y)=y. 2 [] e!=x|g(y)!=z|f(z,y)=x. 3 [] f(x,y)!=z|f(u,z)!=v|$Connect1(x,y,u,v). 3 [] f(x,y)!=z|f(z,u)=v| -$Connect1(y,u,x,v). 4 [] f(x,y)!=z|b!=x|a!=y|f(y,x)!=z. end_of_list. --- Starting search for models of size 2 --- Applying isomorphism constraints to constants: e b a. 107 clauses were generated; 66 of those survived the first stage of unit preprocessing; there are 38 atoms. After all unit preprocessing, 4 atoms are still unassigned; 8 clauses remain; 2 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 66 Literal occurrences input 133 Greatest atom 38 Unit preprocess: Preprocess unit assignments 34 Clauses after subsumption 8 Literal occ. after subsump. 19 Selectable clauses 2 Decide: Splits 1 Unit assignments 4 Failed paths 2 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: e b a. 621 clauses were generated; 408 of those survived the first stage of unit preprocessing; there are 135 atoms. After all unit preprocessing, 103 atoms are still unassigned; 365 clauses remain; 13 of those are non-Horn (selectable); 4885 K allocated; cpu time so far for this domain size: 0.00 sec. ----- statistics for domain size 3 ---- Input: Clauses input 408 Literal occurrences input 1022 Greatest atom 135 Unit preprocess: Preprocess unit assignments 32 Clauses after subsumption 365 Literal occ. after subsump. 968 Selectable clauses 13 Decide: Splits 5 Unit assignments 245 Failed paths 6 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 4 --- Applying isomorphism constraints to constants: e b a. 2373 clauses were generated; 1683 of those survived the first stage of unit preprocessing; there are 364 atoms. After all unit preprocessing, 309 atoms are still unassigned; 1603 clauses remain; 21 of those are non-Horn (selectable); 4892 K allocated; cpu time so far for this domain size: 0.00 sec. ----- statistics for domain size 4 ---- Input: Clauses input 1683 Literal occurrences input 4544 Greatest atom 364 Unit preprocess: Preprocess unit assignments 55 Clauses after subsumption 1603 Literal occ. after subsump. 4439 Selectable clauses 21 Decide: Splits 29 Unit assignments 1520 Failed paths 30 Memory: Memory malloced 10 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: e b a. 6917 clauses were generated; 5203 of those survived the first stage of unit preprocessing; there are 815 atoms. After all unit preprocessing, 731 atoms are still unassigned; 5073 clauses remain; 30 of those are non-Horn (selectable); 4905 K allocated; cpu time so far for this domain size: 0.01 sec. ----- statistics for domain size 5 ---- Input: Clauses input 5203 Literal occurrences input 14514 Greatest atom 815 Unit preprocess: Preprocess unit assignments 84 Clauses after subsumption 5073 Literal occ. after subsump. 14338 Selectable clauses 30 Decide: Splits 87 Unit assignments 11552 Failed paths 88 Memory: Memory malloced 23 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.01 DPLL 0.00 --- Starting search for models of size 6 --- Applying isomorphism constraints to constants: e b a. 16780 clauses were generated; 13181 of those survived the first stage of unit preprocessing; there are 1602 atoms. After all unit preprocessing, 1483 atoms are still unassigned; 12987 clauses remain; 41 of those are non-Horn (selectable); 4927 K allocated; cpu time so far for this domain size: 0.01 sec. ======================= Model #1 at 0.05 seconds: e: 0 f : | 0 1 2 3 4 5 --+------------ 0 | 0 1 2 3 4 5 1 | 1 0 3 2 5 4 2 | 2 4 0 5 1 3 3 | 3 5 1 4 0 2 4 | 4 2 5 0 3 1 5 | 5 3 4 1 2 0 g : 0 1 2 3 4 5 --------------- 0 1 2 4 3 5 b: 1 a: 2 end_of_model  Exit by max_models parameter. The set is satisfiable (1 model(s) found). ----- statistics for domain size 6 ---- Input: Clauses input 13181 Literal occurrences input 37418 Greatest atom 1602 Unit preprocess: Preprocess unit assignments 119 Clauses after subsumption 12987 Literal occ. after subsump. 37149 Selectable clauses 41 Decide: Splits 212 Unit assignments 50629 Failed paths 208 Memory: Memory malloced 45 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.01 DPLL 0.03 ======================================= Total times for run (seconds): user CPU time 0.05 (0 hr, 0 min, 0 sec) system CPU time 0.00 (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 Aug 19 14:47:16 2003