----- 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(f(x,x),f(x,y))=x. 0 [] f(x,f(x,x))=f(y,f(y,y)). 0 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C))). end_of_list. list(clauses). 1 [] x=x. 2 [] f(f(x,x),f(x,y))=x. 3 [] f(x,f(x,x))=f(y,f(y,y)). 4 [] f(A,f(f(B,C),f(B,C)))!=f(B,f(f(A,C),f(A,C))). end_of_list. list(flattened_and_parted_clauses). 1 [] x=x. 2 [] f(x,y)!=z|$Connect1(x,z). 2 [] f(x,x)!=y|f(y,z)=x| -$Connect1(x,z). 3 [] f(x,x)!=y|f(x,y)!=z|$Connect2(z). 3 [] f(x,x)!=y|f(x,y)=z| -$Connect2(z). 4 [] f(x,y)!=z|f(z,z)!=u|C!=y|A!=x| -$Connect4(x,y,u). 4 [] f(x,y)!=z|B!=x| -$Connect3(u,v,x,z)|$Connect4(u,v,y). 4 [] f(x,y)!=z|f(z,z)!=u|$Connect5(x,y,u). 4 [] f(x,y)!=z|$Connect3(x,u,v,z)| -$Connect5(v,u,y). end_of_list. --- Starting search for models of size 2 --- Applying isomorphism constraints to constants: C A B. 149 clauses were generated; 134 of those survived the first stage of unit preprocessing; there are 56 atoms. After all unit preprocessing, 50 atoms are still unassigned; 128 clauses remain; 6 of those are non-Horn (selectable); 4883 K allocated; cpu time so far for this domain size: 0.00 sec. ----- statistics for domain size 2 ---- Input: Clauses input 134 Literal occurrences input 405 Greatest atom 56 Unit preprocess: Preprocess unit assignments 6 Clauses after subsumption 128 Literal occ. after subsump. 399 Selectable clauses 6 Decide: Splits 4 Unit assignments 59 Failed paths 5 Memory: Memory malloced 1 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. 819 clauses were generated; 754 of those survived the first stage of unit preprocessing; there are 192 atoms. After all unit preprocessing, 180 atoms are still unassigned; 742 clauses remain; 13 of those are non-Horn (selectable); 4887 K allocated; cpu time so far for this domain size: 0.00 sec. ======================= Model #1 at 0.00 seconds: interpretation( 3, [ function(f(_,_), [ 0, 0, 0, 2, 2, 0, 1, 0, 1 ]), function(C, [0]), function(A, [0]), function(B, [1]) ]). end_of_model ----- statistics for domain size 3 ---- Input: Clauses input 754 Literal occurrences input 2440 Greatest atom 192 Unit preprocess: Preprocess unit assignments 12 Clauses after subsumption 742 Literal occ. after subsump. 2428 Selectable clauses 13 Decide: Splits 8 Unit assignments 110 Failed paths 4 Memory: Memory malloced 5 K Memory MACE_tp_alloced 4882 K Time (seconds): Generate ground clauses 0.00 DPLL 0.00 ======================================= Total times for run (seconds): user CPU time 0.00 (0 hr, 0 min, 0 sec) system CPU time 0.00 (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:48 2003