----- MACE 2.2f, August 2004 ----- The process was started by mccune on gyro.thornwood, Mon Aug 2 15:44:39 2004 The command was "../../bin/mace2 -N6 -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 (y^ (x v z))= (x v y)^ (x v z). 20 [] A^ (B v C)!= (A^B) v (A^C). 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|z^u!=v| -$Connect4(x,u)|$Connect5(x,y,u,v). 19 [] x^y!=z|u v z=v| -$Connect5(u,x,y,v). 19 [] x v y!=z|$Connect4(x,z). 20 [] x^y!=z|u v z!=v|C!=y|A!=x| -$Connect7(x,y,u,v). 20 [] x^y!=z|B!=y| -$Connect6(x,u,y,v)|$Connect7(x,u,z,v). 20 [] x v y!=z|u^z!=v|$Connect6(u,y,x,v). end_of_list. --- Starting search for models of size 2 --- Applying isomorphism constraints to constants: C A B. 366 clauses were generated; 156 of those survived the first stage of unit preprocessing; there are 114 atoms. After all unit preprocessing, 32 atoms are still unassigned; 30 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 156 Literal occurrences input 291 Greatest atom 114 Unit preprocess: Preprocess unit assignments 82 Clauses after subsumption 30 Literal occ. after subsump. 84 Selectable clauses 3 Decide: Splits 3 Unit assignments 18 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 A B. 2214 clauses were generated; 656 of those survived the first stage of unit preprocessing; there are 468 atoms. After all unit preprocessing, 215 atoms are still unassigned; 228 clauses remain; 6 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 656 Literal occurrences input 1258 Greatest atom 468 Unit preprocess: Preprocess unit assignments 253 Clauses after subsumption 228 Literal occ. after subsump. 615 Selectable clauses 6 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 A B. 8576 clauses were generated; 2397 of those survived the first stage of unit preprocessing; there are 1340 atoms. After all unit preprocessing, 488 atoms are still unassigned; 348 clauses remain; 10 of those are non-Horn (selectable); 4920 K allocated; cpu time so far for this domain size: 0.00 sec. ----- statistics for domain size 4 ---- Input: Clauses input 2397 Literal occurrences input 5382 Greatest atom 1340 Unit preprocess: Preprocess unit assignments 852 Clauses after subsumption 348 Literal occ. after subsump. 1085 Selectable clauses 10 Decide: Splits 9 Unit assignments 94 Failed paths 10 Memory: Memory malloced 38 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 A B. 25051 clauses were generated; 7522 of those survived the first stage of unit preprocessing; there are 3090 atoms. After all unit preprocessing, 1916 atoms are still unassigned; 4117 clauses remain; 31 of those are non-Horn (selectable); 4969 K allocated; cpu time so far for this domain size: 0.01 sec. ----- statistics for domain size 5 ---- Input: Clauses input 7522 Literal occurrences input 19164 Greatest atom 3090 Unit preprocess: Preprocess unit assignments 1174 Clauses after subsumption 4117 Literal occ. after subsump. 12045 Selectable clauses 31 Decide: Splits 1 Unit assignments 135 Failed paths 2 Memory: Memory malloced 87 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: C A B. 60698 clauses were generated; 20314 of those survived the first stage of unit preprocessing; there are 6174 atoms. After all unit preprocessing, 4276 atoms are still unassigned; 13462 clauses remain; 45 of those are non-Horn (selectable); 5057 K allocated; cpu time so far for this domain size: 0.03 sec. ======================= Model #1 at 0.06 seconds: ^ : | 0 1 2 3 4 5 --+------------ 0 | 0 0 0 0 0 0 1 | 0 1 2 3 4 5 2 | 0 2 2 0 0 0 3 | 0 3 0 3 0 0 4 | 0 4 0 0 4 0 5 | 0 5 0 0 0 5 v : | 0 1 2 3 4 5 --+------------ 0 | 0 1 2 3 4 5 1 | 1 1 1 1 1 1 2 | 2 1 2 1 1 1 3 | 3 1 1 3 1 1 4 | 4 1 1 1 4 1 5 | 5 1 1 1 1 5 c : 0 1 2 3 4 5 --------------- 1 0 3 2 5 4 C: 2 A: 3 B: 4 end_of_model  Exit by max_models parameter. The set is satisfiable (1 model(s) found). ----- statistics for domain size 6 ---- Input: Clauses input 20314 Literal occurrences input 56300 Greatest atom 6174 Unit preprocess: Preprocess unit assignments 1898 Clauses after subsumption 13462 Literal occ. after subsump. 40753 Selectable clauses 45 Decide: Splits 18 Unit assignments 6193 Failed paths 16 Memory: Memory malloced 175 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.03 DPLL 0.01 ======================================= Total times for run (seconds): user CPU time 0.06 (0 hr, 0 min, 0 sec) system CPU time 0.01 (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 Mon Aug 2 15:44:39 2004