----- MACE 2.2, August 2003 ----- The process was started by mccune on gyro.thornwood, Tue Aug 19 14:47:16 2003 The command was "../../bin/mace2 -N8 -p". op(450,xfx,+). op(400,xfx,*). op(350,fy,~). list(usable). 1 [] 0+x=x. 2 [] x+0=x. 3 [] ~x+x=0. 4 [] x+ ~x=0. 5 [] (x+y)+z=x+ (y+z). 6 [] x+y=y+x. 7 [] (x*y)*z=x* (y*z). 8 [] x* (y+z)=x*y+x*z. 9 [] (y+z)*x=y*x+z*x. 10 [] ~ ~x=x. 11 [] ~0=0. 12 [] 0*x=0. 13 [] x*0=0. 14 [] 1*x=x. 15 [] x*1=x. 16 [] a*b!=b*a. end_of_list. list(flattened_and_parted_clauses). 1 [] 0+x=x. 2 [] x+0=x. 3 [] ~x!=y|y+x=0. 4 [] ~x!=y|x+y=0. 5 [] x+y!=z|u+z!=v|$Connect1(x,y,u,v). 5 [] x+y!=z|z+u=v| -$Connect1(y,u,x,v). 6 [] x+y!=z|y+x=z. 7 [] x*y!=z|u*z!=v|$Connect2(x,y,u,v). 7 [] x*y!=z|z*u=v| -$Connect2(y,u,x,v). 8 [] x*y!=z|u+z!=v|$Connect4(x,y,u,v). 8 [] x*y!=z|$Connect3(x,u,y,v)| -$Connect4(x,u,z,v). 8 [] x+y!=z|u*z=v| -$Connect3(u,y,x,v). 9 [] x*y!=z|u+z!=v|$Connect6(x,y,u,v). 9 [] x*y!=z|$Connect5(u,y,x,v)| -$Connect6(u,y,z,v). 9 [] x+y!=z|z*u=v| -$Connect5(y,u,x,v). 10 [] ~x!=y| ~y=x. 11 [] ~0=0. 12 [] 0*x=0. 13 [] x*0=0. 14 [] 1*x=x. 15 [] x*1=x. 16 [] x*y!=z|b!=x|a!=y|y*x!=z. end_of_list. --- Starting search for models of size 2 --- Applying isomorphism constraints to constants: b a. 389 clauses were generated; 153 of those survived the first stage of unit preprocessing; there are 124 atoms. After all unit preprocessing, 8 atoms are still unassigned; 8 clauses remain; 2 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 153 Literal occurrences input 224 Greatest atom 124 Unit preprocess: Preprocess unit assignments 116 Clauses after subsumption 8 Literal occ. after subsump. 16 Selectable clauses 2 Decide: Splits 1 Unit assignments 4 Failed paths 2 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: b a. 2631 clauses were generated; 986 of those survived the first stage of unit preprocessing; there are 564 atoms. After all unit preprocessing, 258 atoms are still unassigned; 618 clauses remain; 9 of those are non-Horn (selectable); 4898 K allocated; cpu time so far for this domain size: 0.00 sec. ----- statistics for domain size 3 ---- Input: Clauses input 986 Literal occurrences input 1910 Greatest atom 564 Unit preprocess: Preprocess unit assignments 306 Clauses after subsumption 618 Literal occ. after subsump. 1422 Selectable clauses 9 Decide: Splits 3 Unit assignments 299 Failed paths 4 Memory: Memory malloced 16 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: b a. 10726 clauses were generated; 4514 of those survived the first stage of unit preprocessing; there are 1704 atoms. After all unit preprocessing, 1059 atoms are still unassigned; 3667 clauses remain; 21 of those are non-Horn (selectable); 4930 K allocated; cpu time so far for this domain size: 0.00 sec. ----- statistics for domain size 4 ---- Input: Clauses input 4514 Literal occurrences input 10351 Greatest atom 1704 Unit preprocess: Preprocess unit assignments 645 Clauses after subsumption 3667 Literal occ. after subsump. 9125 Selectable clauses 21 Decide: Splits 8 Unit assignments 2162 Failed paths 9 Memory: Memory malloced 48 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: b a. 32262 clauses were generated; 15341 of those survived the first stage of unit preprocessing; there are 4060 atoms. After all unit preprocessing, 2936 atoms are still unassigned; 13733 clauses remain; 35 of those are non-Horn (selectable); 4997 K allocated; cpu time so far for this domain size: 0.01 sec. ----- statistics for domain size 5 ---- Input: Clauses input 15341 Literal occurrences input 38264 Greatest atom 4060 Unit preprocess: Preprocess unit assignments 1124 Clauses after subsumption 13733 Literal occ. after subsump. 35768 Selectable clauses 35 Decide: Splits 16 Unit assignments 9299 Failed paths 17 Memory: Memory malloced 115 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.01 DPLL 0.01 --- Starting search for models of size 6 --- Applying isomorphism constraints to constants: b a. 79657 clauses were generated; 41893 of those survived the first stage of unit preprocessing; there are 8292 atoms. After all unit preprocessing, 6537 atoms are still unassigned; 39178 clauses remain; 52 of those are non-Horn (selectable); 5117 K allocated; cpu time so far for this domain size: 0.04 sec. ----- statistics for domain size 6 ---- Input: Clauses input 41893 Literal occurrences input 109472 Greatest atom 8292 Unit preprocess: Preprocess unit assignments 1755 Clauses after subsumption 39178 Literal occ. after subsump. 105022 Selectable clauses 52 Decide: Splits 53 Unit assignments 61215 Failed paths 54 Memory: Memory malloced 235 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.04 DPLL 0.11 --- Starting search for models of size 7 --- Applying isomorphism constraints to constants: b a. 171353 clauses were generated; 97612 of those survived the first stage of unit preprocessing; there are 15204 atoms. After all unit preprocessing, 12654 atoms are still unassigned; 93380 clauses remain; 73 of those are non-Horn (selectable); 5312 K allocated; cpu time so far for this domain size: 0.06 sec. ----- statistics for domain size 7 ---- Input: Clauses input 97612 Literal occurrences input 262490 Greatest atom 15204 Unit preprocess: Preprocess unit assignments 2550 Clauses after subsumption 93380 Literal occ. after subsump. 255250 Selectable clauses 73 Decide: Splits 270 Unit assignments 805684 Failed paths 271 Memory: Memory malloced 430 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.05 DPLL 2.05 --- Starting search for models of size 8 --- Applying isomorphism constraints to constants: b a. 333015 clauses were generated; 202155 of those survived the first stage of unit preprocessing; there are 25744 atoms. After all unit preprocessing, 22223 atoms are still unassigned; 195932 clauses remain; 98 of those are non-Horn (selectable); 10494 K allocated; cpu time so far for this domain size: 0.16 sec. ======================= Model #1 at 2.53 seconds: + : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 1 2 3 4 5 6 7 1 | 1 0 4 5 2 3 7 6 2 | 2 4 0 6 1 7 3 5 3 | 3 5 6 0 7 1 2 4 4 | 4 2 1 7 0 6 5 3 5 | 5 3 7 1 6 0 4 2 6 | 6 7 3 2 5 4 0 1 7 | 7 6 5 4 3 2 1 0 ~ : 0 1 2 3 4 5 6 7 ------------------- 0 1 2 3 4 5 6 7 * : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 2 | 0 2 0 0 2 2 0 2 3 | 0 3 2 3 6 0 6 2 4 | 0 4 2 3 1 7 6 5 5 | 0 5 0 0 5 5 0 5 6 | 0 6 2 3 3 2 6 0 7 | 0 7 0 0 7 7 0 7 b: 2 a: 3 end_of_model  Exit by max_models parameter. The set is satisfiable (1 model(s) found). ----- statistics for domain size 8 ---- Input: Clauses input 202155 Literal occurrences input 554116 Greatest atom 25744 Unit preprocess: Preprocess unit assignments 3521 Clauses after subsumption 195932 Literal occ. after subsump. 543098 Selectable clauses 98 Decide: Splits 58 Unit assignments 54394 Failed paths 51 Memory: Memory malloced 729 K Memory MACE_tp_alloced 9765 K Time (seconds): Generate ground clauses 0.12 DPLL 0.14 ======================================= Total times for run (seconds): user CPU time 2.53 (0 hr, 0 min, 2 sec) system CPU time 0.08 (0 hr, 0 min, 0 sec) wall-clock time 2 (0 hr, 0 min, 2 sec) Exit by max_models parameter. The set is satisfiable (1 model(s) found). The job finished Tue Aug 19 14:47:18 2003