----- MACE 2.2, August 2003 ----- The process was started by mccune on gyro.thornwood, Tue Sep 16 15:18:50 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 [] x v (y v z)=y v (x v z). 0 [] x v (x^y)=x. 0 [] x^y=c(c(x) v c(y)). 0 [] c(c(x))=x. 0 [] x v (y^ (x v z))=x v (z^ (x v y)). 0 [] A v c(A)!=B v c(B). end_of_list. list(clauses). 1 [] x=x. 2 [] x v (y v z)=y v (x v z). 3 [] x v (x^y)=x. 4 [] x^y=c(c(x) v c(y)). 5 [] c(c(x))=x. 6 [] x v (y^ (x v z))=x v (z^ (x v y)). 7 [] A v c(A)!=B v c(B). end_of_list. list(flattened_and_parted_clauses). 1 [] x=x. 2 [] x v y!=z|u v z!=v|$Connect1(x,y,u,v). 2 [] x v y!=z|u v z=v| -$Connect1(u,y,x,v). 3 [] x^y!=z|x v z=x. 4 [] c(x)!=y|z v y!=u|$Connect3(x,z,u). 4 [] c(x)!=y|$Connect2(z,x,u)| -$Connect3(z,y,u). 4 [] c(x)!=y|z^u=y| -$Connect2(u,z,x). 5 [] c(x)!=y|c(y)=x. 6 [] x v y!=z|u^z!=v|$Connect5(x,y,u,v). 6 [] x v y!=z|$Connect4(x,u,v,z)| -$Connect5(x,u,v,y). 6 [] x v y!=z|u^z!=v|$Connect6(x,y,u,v). 6 [] x v y=z| -$Connect4(x,u,v,z)| -$Connect6(x,v,u,y). 7 [] c(x)!=y|B!=x|x v y!=z| -$Connect7(z). 7 [] c(x)!=y|A!=x|x v y!=z|$Connect7(z). end_of_list. --- Starting search for models of size 2 --- Applying isomorphism constraints to constants: B A. 299 clauses were generated; 286 of those survived the first stage of unit preprocessing; there are 110 atoms. After all unit preprocessing, 104 atoms are still unassigned; 280 clauses remain; 11 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 286 Literal occurrences input 818 Greatest atom 110 Unit preprocess: Preprocess unit assignments 6 Clauses after subsumption 280 Literal occ. after subsump. 812 Selectable clauses 11 Decide: Splits 12 Unit assignments 378 Failed paths 13 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. 1897 clauses were generated; 1862 of those survived the first stage of unit preprocessing; there are 459 atoms. After all unit preprocessing, 447 atoms are still unassigned; 1850 clauses remain; 23 of those are non-Horn (selectable); 4895 K allocated; cpu time so far for this domain size: 0.00 sec. ======================= Model #1 at 0.01 seconds: interpretation( 3, [ function(v(_,_), [ 0, 0, 0, 0, 1, 1, 0, 1, 2 ]), function(^(_,_), [ 0, 1, 2, 1, 1, 2, 2, 2, 2 ]), function(c(_), [2, 1, 0]), function(B, [0]), function(A, [1]) ]). end_of_model ----- statistics for domain size 3 ---- Input: Clauses input 1862 Literal occurrences input 5480 Greatest atom 459 Unit preprocess: Preprocess unit assignments 12 Clauses after subsumption 1850 Literal occ. after subsump. 5468 Selectable clauses 23 Decide: Splits 761 Unit assignments 27727 Failed paths 753 Memory: Memory malloced 13 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.00 DPLL 0.01 ======================================= Total times for run (seconds): user CPU time 0.01 (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 Tue Sep 16 15:18:50 2003