----- MACE 2.2f, August 2004 ----- The process was started by mccune on cleo.thornwood, Mon Nov 14 15:26:22 2005 The command was "mace2 -n3 -p". op(400,xfx,[*,+,^,v,/,\,#]). op(300,yf,@). clear(print_kept). clear(print_new_demod). clear(print_back_demod). assign(pick_given_ratio,4). assign(max_mem,20000). set(geometric_rule). set(geometric_rewrite_before). set(para_from). set(para_into). set(para_from_vars). set(para_into_vars). set(order_eq). set(back_demod). dependent: set(dynamic_demod). set(process_input). set(lrpo). clear(process_input). assign(max_weight,15). lex([A,e,_*_,_+_]). list(usable). 1 [] x=x. 2 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. end_of_list. list(sos). 3 [] x+e=x. 4 [] e+x=x. 5 [] x* (y*x)=y. 6 [] x*y=y*x. 7 [] A+B!=e* (A*B). end_of_list. list(flattened_and_parted_clauses). 1 [] x=x. 2 [] x*y!=z|z*u!=v|$Connect3(x,y,u,v). 2 [] -$Connect1(x,y,z,u)|$Connect2(v,w,z,u)| -$Connect3(v,x,y,w). 2 [] x*y!=z|z*u=v| -$Connect2(x,v,y,u). 2 [] x*y!=z|z*u!=v|$Connect5(x,y,u,v). 2 [] $Connect1(x,y,z,u)| -$Connect4(v,w,z,u)| -$Connect5(v,x,y,w). 2 [] x*y!=z|z*u!=v|$Connect4(x,v,y,u). 3 [] e!=x|y+x=y. 4 [] e!=x|x+y=y. 5 [] x*y!=z|y*z=x. 6 [] x*y!=z|y*x=z. 7 [] x*y!=z|B!=y|A!=x|x+y!=u| -$Connect6(z,u). 7 [] e!=x|x*y!=z|$Connect6(y,z). end_of_list. --- Starting search for models of size 3 --- Applying isomorphism constraints to constants: e B A. 2709 clauses were generated; 2626 of those survived the first stage of unit preprocessing; there are 486 atoms. After all unit preprocessing, 459 atoms are still unassigned; 2585 clauses remain; 17 of those are non-Horn (selectable); 4895 K allocated; cpu time so far for this domain size: 0.00 sec. ======================= Model #1 at 0.00 seconds: * : | 0 1 2 --+------ 0 | 0 2 1 1 | 2 1 0 2 | 1 0 2 e: 0 + : | 0 1 2 --+------ 0 | 0 1 2 1 | 1 0 0 2 | 2 0 0 B: 1 A: 1 end_of_model ----- statistics for domain size 3 ---- Input: Clauses input 2626 Literal occurrences input 7773 Greatest atom 486 Unit preprocess: Preprocess unit assignments 27 Clauses after subsumption 2585 Literal occ. after subsump. 7718 Selectable clauses 17 Decide: Splits 14 Unit assignments 704 Failed paths 8 Memory: Memory malloced 13 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 Mon Nov 14 15:26:22 2005