----- MACE 2.2, August 2003 ----- The process was started by mccune on gyro.thornwood, Tue Sep 16 15:18:48 2003 The command was "mace2 -N6 -P". include("ortholattice-header"). ------- start included file ortholattice-header------- op(400,infix,^). op(400,infix,v). lex([A,B,C,D,0,1,x v x,c(x),x^x,f(x,x)]). set(anl_eq). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(process_input). dependent: set(lrpo). assign(pick_given_ratio,3). assign(max_weight,25). clear(detailed_history). assign(max_seconds,60). assign(max_mem,100000). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). clear(print_kept). assign(stats_level,1). list(usable). 0 [] x=x. end_of_list. ------- end included file ortholattice-header------- list(sos). 0 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 0 [] f(f(x,x),f(x,y))=x. 0 [] f(x,f(x,x))=f(y,f(y,y)). 0 [] f(A,f(B,f(A,f(C,C))))!=f(A,f(C,f(A,f(B,B)))). end_of_list. list(clauses). 1 [] x=x. 2 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))). 3 [] f(f(x,x),f(x,y))=x. 4 [] f(x,f(x,x))=f(y,f(y,y)). 5 [] f(A,f(B,f(A,f(C,C))))!=f(A,f(C,f(A,f(B,B)))). end_of_list. list(flattened_and_parted_clauses). 1 [] x=x. 2 [] f(x,y)!=z|f(z,z)!=u|$Connect2(x,y,u). 2 [] f(x,y)!=z|$Connect1(u,v,x,z)| -$Connect2(u,v,y). 2 [] f(x,y)!=z|f(z,z)!=u|$Connect3(x,y,u). 2 [] f(x,y)=z| -$Connect1(x,u,v,z)| -$Connect3(v,u,y). 3 [] f(x,y)!=z|$Connect4(x,z). 3 [] f(x,x)!=y|f(y,z)=x| -$Connect4(x,z). 4 [] f(x,x)!=y|f(x,y)!=z|$Connect5(z). 4 [] f(x,x)!=y|f(x,y)=z| -$Connect5(z). 5 [] f(x,x)!=y|f(z,y)!=u|B!=x|A!=z| -$Connect7(x,z,u). 5 [] f(x,y)!=z|f(u,z)!=v|C!=x|$Connect8(x,y,u,v). 5 [] -$Connect6(x,y,z,u)|$Connect7(x,y,v)| -$Connect8(z,v,y,u). 5 [] f(x,x)!=y|f(z,y)!=u|$Connect9(x,z,u). 5 [] f(x,y)!=z|f(u,z)!=v|$Connect10(x,y,u,v). 5 [] $Connect6(x,y,z,u)| -$Connect9(z,y,v)| -$Connect10(x,v,y,u). end_of_list. --- Starting search for models of size 2 --- Applying isomorphism constraints to constants: B A C. 309 clauses were generated; 294 of those survived the first stage of unit preprocessing; there are 120 atoms. After all unit preprocessing, 114 atoms are still unassigned; 288 clauses remain; 6 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 294 Literal occurrences input 873 Greatest atom 120 Unit preprocess: Preprocess unit assignments 6 Clauses after subsumption 288 Literal occ. after subsump. 867 Selectable clauses 6 Decide: Splits 4 Unit assignments 142 Failed paths 5 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 C. 1953 clauses were generated; 1888 of those survived the first stage of unit preprocessing; there are 489 atoms. After all unit preprocessing, 477 atoms are still unassigned; 1876 clauses remain; 13 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 1888 Literal occurrences input 5818 Greatest atom 489 Unit preprocess: Preprocess unit assignments 12 Clauses after subsumption 1876 Literal occ. after subsump. 5806 Selectable clauses 13 Decide: Splits 46 Unit assignments 1782 Failed paths 47 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: B A C. 7581 clauses were generated; 7373 of those survived the first stage of unit preprocessing; there are 1392 atoms. After all unit preprocessing, 1372 atoms are still unassigned; 7353 clauses remain; 21 of those are non-Horn (selectable); 4921 K allocated; cpu time so far for this domain size: 0.01 sec. ----- statistics for domain size 4 ---- Input: Clauses input 7373 Literal occurrences input 22964 Greatest atom 1392 Unit preprocess: Preprocess unit assignments 20 Clauses after subsumption 7353 Literal occ. after subsump. 22944 Selectable clauses 21 Decide: Splits 508 Unit assignments 36946 Failed paths 509 Memory: Memory malloced 39 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.01 DPLL 0.02 --- Starting search for models of size 5 --- Applying isomorphism constraints to constants: B A C. 22092 clauses were generated; 21570 of those survived the first stage of unit preprocessing; there are 3195 atoms. After all unit preprocessing, 3165 atoms are still unassigned; 21540 clauses remain; 30 of those are non-Horn (selectable); 4972 K allocated; cpu time so far for this domain size: 0.02 sec. ----- statistics for domain size 5 ---- Input: Clauses input 21570 Literal occurrences input 67488 Greatest atom 3195 Unit preprocess: Preprocess unit assignments 30 Clauses after subsumption 21540 Literal occ. after subsump. 67458 Selectable clauses 30 Decide: Splits 6601 Unit assignments 453826 Failed paths 6602 Memory: Memory malloced 90 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.01 DPLL 0.65 --- Starting search for models of size 6 --- Applying isomorphism constraints to constants: B A C. 53374 clauses were generated; 52265 of those survived the first stage of unit preprocessing; there are 6360 atoms. After all unit preprocessing, 6318 atoms are still unassigned; 52223 clauses remain; 41 of those are non-Horn (selectable); 5062 K allocated; cpu time so far for this domain size: 0.04 sec. ======================= Model #1 at 1.62 seconds: interpretation( 6, [ function(f(_,_), [ 2, 3, 3, 2, 3, 1, 3, 5, 0, 5, 3, 3, 3, 0, 0, 0, 3, 3, 2, 5, 0, 4, 3, 1, 3, 3, 3, 3, 3, 3, 1, 3, 3, 1, 3, 1 ]), function(B, [0]), function(A, [0]), function(C, [1]) ]). end_of_model ----- statistics for domain size 6 ---- Input: Clauses input 52265 Literal occurrences input 163934 Greatest atom 6360 Unit preprocess: Preprocess unit assignments 42 Clauses after subsumption 52223 Literal occ. after subsump. 163892 Selectable clauses 41 Decide: Splits 4503 Unit assignments 347500 Failed paths 4493 Memory: Memory malloced 180 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.03 DPLL 0.89 ======================================= Total times for run (seconds): user CPU time 1.62 (0 hr, 0 min, 1 sec) system CPU time 0.00 (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 Sep 16 15:18:50 2003