----- MACE 2.2, August 2003 ----- The process was started by mccune on gyro.thornwood, Tue Aug 19 14:48:09 2003 The command was "../../bin/mace2 -n5 -N10 -p". include("ortholattice"). ------- start included file ortholattice------- op(400,infix,[^,v]). list(usable). 1 [] x^y=y^x. 2 [] x v y=y v x. 3 [] (x v y) v z=x v (y v z). 4 [] c(c(x))=x. 5 [] x v (x^y)=x. 6 [] x^y=c(c(x) v c(y)). 7 [] x^x=x. 8 [] x v x=x. 9 [] c(x) v x=1. 10 [] c(x)^x=0. 11 [] 1 v x=1. 12 [] x v 1=1. 13 [] 1^x=x. 14 [] x^1=x. 15 [] 0^x=0. 16 [] x^0=0. 17 [] 0 v x=x. 18 [] x v 0=x. end_of_list. ------- end included file ortholattice------- list(usable). 19 [] x v (c(x)^ (x v y))=x v y. 20 [] 2 v (4^ (2 v 3))!= (2 v 4)^ (2 v 3). end_of_list. list(flattened_and_parted_clauses). 1 [] x^y!=z|y^x=z. 2 [] x v y!=z|y v x=z. 3 [] x v y!=z|u v z!=v|$Connect1(x,y,u,v). 3 [] x v y!=z|z v u=v| -$Connect1(y,u,x,v). 4 [] c(x)!=y|c(y)=x. 5 [] x^y!=z|x v z=x. 6 [] c(x)!=y|z v y!=u|$Connect3(x,z,u). 6 [] c(x)!=y|$Connect2(z,x,u)| -$Connect3(z,y,u). 6 [] c(x)!=y|z^u=y| -$Connect2(u,z,x). 7 [] x^x=x. 8 [] x v x=x. 9 [] c(x)!=y|y v x=1. 10 [] c(x)!=y|y^x=0. 11 [] 1 v x=1. 12 [] x v 1=1. 13 [] 1^x=x. 14 [] x^1=x. 15 [] 0^x=0. 16 [] x^0=0. 17 [] 0 v x=x. 18 [] x v 0=x. 19 [] x v y!=z|$Connect4(x,z). 19 [] c(x)!=y|y^z!=u|x v u=z| -$Connect4(x,z). 20 [] 2 v 4!=x|x^y!=z|2 v 3!=y| -$Connect5(y,z). 20 [] 4^x!=y|2 v y!=z|$Connect5(x,z). end_of_list. --- Starting search for models of size 5 --- 10255 clauses were generated; 4055 of those survived the first stage of unit preprocessing; there are 1225 atoms. After all unit preprocessing, 522 atoms are still unassigned; 1850 clauses remain; 15 of those are non-Horn (selectable); 4916 K allocated; cpu time so far for this domain size: 0.01 sec. ----- statistics for domain size 5 ---- Input: Clauses input 4055 Literal occurrences input 9006 Greatest atom 1225 Unit preprocess: Preprocess unit assignments 703 Clauses after subsumption 1850 Literal occ. after subsump. 4519 Selectable clauses 15 Decide: Splits 1 Unit assignments 106 Failed paths 2 Memory: Memory malloced 34 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.01 DPLL 0.00 --- Starting search for models of size 6 --- 23484 clauses were generated; 9835 of those survived the first stage of unit preprocessing; there are 2304 atoms. After all unit preprocessing, 1195 atoms are still unassigned; 5960 clauses remain; 28 of those are non-Horn (selectable); 4947 K allocated; cpu time so far for this domain size: 0.01 sec. ----- statistics for domain size 6 ---- Input: Clauses input 9835 Literal occurrences input 23223 Greatest atom 2304 Unit preprocess: Preprocess unit assignments 1109 Clauses after subsumption 5960 Literal occ. after subsump. 15030 Selectable clauses 28 Decide: Splits 6 Unit assignments 3111 Failed paths 7 Memory: Memory malloced 65 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.01 DPLL 0.01 --- Starting search for models of size 7 --- 47852 clauses were generated; 21393 of those survived the first stage of unit preprocessing; there are 3969 atoms. After all unit preprocessing, 2338 atoms are still unassigned; 15173 clauses remain; 45 of those are non-Horn (selectable); 4994 K allocated; cpu time so far for this domain size: 0.02 sec. ----- statistics for domain size 7 ---- Input: Clauses input 21393 Literal occurrences input 52792 Greatest atom 3969 Unit preprocess: Preprocess unit assignments 1631 Clauses after subsumption 15173 Literal occ. after subsump. 39247 Selectable clauses 45 Decide: Splits 7 Unit assignments 2542 Failed paths 8 Memory: Memory malloced 112 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.02 DPLL 0.00 --- Starting search for models of size 8 --- 89272 clauses were generated; 42512 of those survived the first stage of unit preprocessing; there are 6400 atoms. After all unit preprocessing, 4119 atoms are still unassigned; 33158 clauses remain; 66 of those are non-Horn (selectable); 5063 K allocated; cpu time so far for this domain size: 0.04 sec. ----- statistics for domain size 8 ---- Input: Clauses input 42512 Literal occurrences input 108327 Greatest atom 6400 Unit preprocess: Preprocess unit assignments 2281 Clauses after subsumption 33158 Literal occ. after subsump. 87478 Selectable clauses 66 Decide: Splits 128 Unit assignments 124526 Failed paths 129 Memory: Memory malloced 181 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.04 DPLL 0.19 --- Starting search for models of size 9 --- 155457 clauses were generated; 78415 of those survived the first stage of unit preprocessing; there are 9801 atoms. After all unit preprocessing, 6730 atoms are still unassigned; 65024 clauses remain; 91 of those are non-Horn (selectable); 5159 K allocated; cpu time so far for this domain size: 0.06 sec. ----- statistics for domain size 9 ---- Input: Clauses input 78415 Literal occurrences input 204642 Greatest atom 9801 Unit preprocess: Preprocess unit assignments 3071 Clauses after subsumption 65024 Literal occ. after subsump. 174231 Selectable clauses 91 Decide: Splits 47 Unit assignments 26268 Failed paths 48 Memory: Memory malloced 277 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.05 DPLL 0.07 --- Starting search for models of size 10 --- 256160 clauses were generated; 136005 of those survived the first stage of unit preprocessing; there are 14400 atoms. After all unit preprocessing, 10387 atoms are still unassigned; 117560 clauses remain; 120 of those are non-Horn (selectable); 10173 K allocated; cpu time so far for this domain size: 0.12 sec. ======================= Model #1 at 6.13 seconds: ^ : | 0 1 2 3 4 5 6 7 8 9 --+-------------------- 0 | 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 9 2 | 0 2 2 0 0 0 2 0 0 2 3 | 0 3 0 3 0 3 0 0 0 3 4 | 0 4 0 0 4 0 0 0 0 0 5 | 0 5 0 3 0 5 8 0 8 3 6 | 0 6 2 0 0 8 6 0 8 2 7 | 0 7 0 0 0 0 0 7 0 0 8 | 0 8 0 0 0 8 8 0 8 0 9 | 0 9 2 3 0 3 2 0 0 9 v : | 0 1 2 3 4 5 6 7 8 9 --+-------------------- 0 | 0 1 2 3 4 5 6 7 8 9 1 | 1 1 1 1 1 1 1 1 1 1 2 | 2 1 2 9 1 1 6 1 6 9 3 | 3 1 9 3 1 5 1 1 5 9 4 | 4 1 1 1 4 1 1 1 1 1 5 | 5 1 1 5 1 5 1 1 5 1 6 | 6 1 6 1 1 1 6 1 6 1 7 | 7 1 1 1 1 1 1 7 1 1 8 | 8 1 6 5 1 5 6 1 8 1 9 | 9 1 9 9 1 1 1 1 1 9 c : 0 1 2 3 4 5 6 7 8 9 ----------------------- 1 0 5 6 7 2 3 4 9 8 end_of_model  Exit by max_models parameter. The set is satisfiable (1 model(s) found). ----- statistics for domain size 10 ---- Input: Clauses input 136005 Literal occurrences input 361471 Greatest atom 14400 Unit preprocess: Preprocess unit assignments 4013 Clauses after subsumption 117560 Literal occ. after subsump. 318934 Selectable clauses 120 Decide: Splits 1430 Unit assignments 1915319 Failed paths 1420 Memory: Memory malloced 408 K Memory MACE_tp_alloced 9765 K Time (seconds): Generate ground clauses 0.10 DPLL 5.63 ======================================= Total times for run (seconds): user CPU time 6.13 (0 hr, 0 min, 6 sec) system CPU time 0.06 (0 hr, 0 min, 0 sec) wall-clock time 6 (0 hr, 0 min, 6 sec) Exit by max_models parameter. The set is satisfiable (1 model(s) found). The job finished Tue Aug 19 14:48:15 2003