----- MACE 2.2, August 2003 ----- The process was started by mccune on gyro.thornwood, Fri Oct 17 13:41:57 2003 The command was "mace2 -N6 -p". op(400,infix,^). op(400,infix,v). list(sos). 1 [] x v (y v z)=y v (x v z). 2 [] x v (x^y)=x. 3 [] x^y=c(c(x) v c(y)). 4 [] c(c(x))=x. 5 [] x v c(x)=y v c(y). 6 [] x v c(x)=1. 7 [] c(1)=0. 8 [] A v (B^ (A v C))!=A v (C^ (A v B)). end_of_list. list(flattened_and_parted_clauses). 1 [] x v y!=z|u v z!=v|$Connect1(x,y,u,v). 1 [] x v y!=z|u v z=v| -$Connect1(u,y,x,v). 2 [] x^y!=z|x v z=x. 3 [] c(x)!=y|z v y!=u|$Connect3(x,z,u). 3 [] c(x)!=y|$Connect2(z,x,u)| -$Connect3(z,y,u). 3 [] c(x)!=y|z^u=y| -$Connect2(u,z,x). 4 [] c(x)!=y|c(y)=x. 5 [] c(x)!=y|x v y!=z|$Connect4(z). 5 [] c(x)!=y|x v y=z| -$Connect4(z). 6 [] c(x)!=y|x v y=1. 7 [] c(1)=0. 8 [] x v y!=z|u^z!=v|C!=u|B!=y|A!=x| -$Connect6(x,y,u,v). 8 [] x v y!=z| -$Connect5(x,u,v,z)|$Connect6(x,u,v,y). 8 [] x v y!=z|u^z!=v|$Connect7(x,y,u,v). 8 [] x v y!=z|$Connect5(x,u,v,z)| -$Connect7(x,v,u,y). end_of_list. --- Starting search for models of size 2 --- Applying isomorphism constraints to constants: C B A. 303 clauses were generated; 280 of those survived the first stage of unit preprocessing; there are 112 atoms. After all unit preprocessing, 26 atoms are still unassigned; 22 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 280 Literal occurrences input 866 Greatest atom 112 Unit preprocess: Preprocess unit assignments 86 Clauses after subsumption 22 Literal occ. after subsump. 84 Selectable clauses 3 Decide: Splits 3 Unit assignments 10 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 B A. 1906 clauses were generated; 1826 of those survived the first stage of unit preprocessing; there are 462 atoms. After all unit preprocessing, 363 atoms are still unassigned; 806 clauses remain; 14 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 1826 Literal occurrences input 6030 Greatest atom 462 Unit preprocess: Preprocess unit assignments 99 Clauses after subsumption 806 Literal occ. after subsump. 2665 Selectable clauses 14 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 B A. 7433 clauses were generated; 7241 of those survived the first stage of unit preprocessing; there are 1328 atoms. After all unit preprocessing, 1182 atoms are still unassigned; 4800 clauses remain; 36 of those are non-Horn (selectable); 4919 K allocated; cpu time so far for this domain size: 0.01 sec. ----- statistics for domain size 4 ---- Input: Clauses input 7241 Literal occurrences input 24411 Greatest atom 1328 Unit preprocess: Preprocess unit assignments 146 Clauses after subsumption 4800 Literal occ. after subsump. 16111 Selectable clauses 36 Decide: Splits 10 Unit assignments 775 Failed paths 11 Memory: Memory malloced 37 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.01 DPLL 0.00 --- Starting search for models of size 5 --- Applying isomorphism constraints to constants: C B A. 21727 clauses were generated; 21350 of those survived the first stage of unit preprocessing; there are 3070 atoms. After all unit preprocessing, 2891 atoms are still unassigned; 16355 clauses remain; 61 of those are non-Horn (selectable); 4969 K allocated; cpu time so far for this domain size: 0.00 sec. ----- statistics for domain size 5 ---- Input: Clauses input 21350 Literal occurrences input 72656 Greatest atom 3070 Unit preprocess: Preprocess unit assignments 179 Clauses after subsumption 16355 Literal occ. after subsump. 55437 Selectable clauses 61 Decide: Splits 20 Unit assignments 3655 Failed paths 21 Memory: Memory malloced 87 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.00 DPLL 0.00 --- Starting search for models of size 6 --- Applying isomorphism constraints to constants: C B A. 52611 clauses were generated; 51958 of those survived the first stage of unit preprocessing; there are 6144 atoms. After all unit preprocessing, 5930 atoms are still unassigned; 43050 clauses remain; 85 of those are non-Horn (selectable); 5056 K allocated; cpu time so far for this domain size: 0.05 sec. ======================= Model #1 at 0.21 seconds: 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 5 3 | 3 1 1 3 3 1 4 | 4 1 1 3 4 1 5 | 5 1 5 1 1 5 ^ : | 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 2 3 | 0 3 0 3 4 0 4 | 0 4 0 4 4 0 5 | 0 5 2 0 0 5 c : 0 1 2 3 4 5 --------------- 1 0 3 2 5 4 C: 2 B: 3 A: 4 end_of_model ----- statistics for domain size 6 ---- Input: Clauses input 51958 Literal occurrences input 177751 Greatest atom 6144 Unit preprocess: Preprocess unit assignments 214 Clauses after subsumption 43050 Literal occ. after subsump. 146805 Selectable clauses 85 Decide: Splits 132 Unit assignments 72674 Failed paths 130 Memory: Memory malloced 174 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.04 DPLL 0.16 ======================================= Total times for run (seconds): user CPU time 0.21 (0 hr, 0 min, 0 sec) system CPU time 0.02 (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 Fri Oct 17 13:41:57 2003