----- MACE4 2005-A, 30 June 2005 ----- Built with library LADR July-2005, 30 June 2005. The process was started by mccune on theorem.mcs.anl.gov, Tue Jul 5 21:30:20 2005 The command was "../bin/mace4". The process ID is 8587. assign(domain_size,48). clear(negprop). set(verbose). clauses(theory). e * x = x. x ' * x = e. (x * y) * z = x * (y * z). A * B != B * A. end_of_list. % Finished reading the input. % There are no domain elements in the input. === Starting model search for domain size 48. === Initial partial model: e : - A : - B : - ' : 0 1 2 3 4 5 6 7 8 91011121314151617181920212223242526272829303132333435363738394041424344454647 --------------------------------------------------------------------------------------------------- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - * : | 0 1 2 3 4 5 6 7 8 91011121314151617181920212223242526272829303132333435363738394041424344454647 --+------------------------------------------------------------------------------------------------ 0 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 1 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 2 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 3 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 4 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 5 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 6 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 7 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 8 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 9 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 10 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 11 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 12 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 13 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 14 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 15 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 16 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 17 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 18 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 19 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 20 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 21 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 22 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 23 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 24 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 25 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 26 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 27 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 28 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 29 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 30 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 31 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 32 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 33 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 34 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 35 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 36 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 37 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 38 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 39 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 40 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 41 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 42 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 43 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 44 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 45 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 46 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 47 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -------- Model 1 at 0.40 seconds -------- e : 0 A : 1 B : 2 ' : 0 1 2 3 4 5 6 7 8 91011121314151617181920212223242526272829303132333435363738394041424344454647 --------------------------------------------------------------------------------------------------- 0 1 2 4 3 5 6 7 810 911121314161517181920222123242526282729303132343335363738403941424344464547 * : | 0 1 2 3 4 5 6 7 8 91011121314151617181920212223242526272829303132333435363738394041424344454647 --+------------------------------------------------------------------------------------------------ 0 | 0 1 2 3 4 5 6 7 8 91011121314151617181920212223242526272829303132333435363738394041424344454647 1 | 1 0 3 2 5 4 7 6 9 81110131215141716191821202322252427262928313033323534373639384140434245444746 2 | 2 4 0 5 1 3 810 611 7 9141612171315202218231921262824292527323430353133384036413739444642474345 3 | 3 5 1 4 0 2 911 710 6 8151713161214212319221820272925282426333531343032394137403638454743464244 4 | 4 2 5 0 3 110 811 6 9 7161417121513222023182119282629242725343235303331403841363937464447424543 5 | 5 3 4 1 2 011 910 7 8 6171516131412232122192018292728252624353334313230413940373836474546434442 6 | 6 7 8 91011 0 1 2 3 4 5181920212223121314151617303132333435242526272829424344454647363738394041 7 | 7 6 9 81110 1 0 3 2 5 4191821202322131215141716313033323534252427262928434245444746373639384140 8 | 810 611 7 9 2 4 0 5 1 3202218231921141612171315323430353133262824292527444642474345384036413739 9 | 911 710 6 8 3 5 1 4 0 2212319221820151713161214333531343032272925282426454743464244394137403638 10 |10 811 6 9 7 4 2 5 0 3 1222023182119161417121513343235303331282629242725464447424543403841363937 11 |11 910 7 8 6 5 3 4 1 2 0232122192018171516131412353334313230292728252624474546434442413940373836 12 |121314151617181920212223 0 1 2 3 4 5 6 7 8 91011363738394041424344454647242526272829303132333435 13 |131215141716191821202322 1 0 3 2 5 4 7 6 9 81110373639384140434245444746252427262928313033323534 14 |141612171315202218231921 2 4 0 5 1 3 810 611 7 9384036413739444642474345262824292527323430353133 15 |151713161214212319221820 3 5 1 4 0 2 911 710 6 8394137403638454743464244272925282426333531343032 16 |161417121513222023182119 4 2 5 0 3 110 811 6 9 7403841363937464447424543282629242725343235303331 17 |171516131412232122192018 5 3 4 1 2 011 910 7 8 6413940373836474546434442292728252624353334313230 18 |181920212223121314151617 6 7 8 91011 0 1 2 3 4 5424344454647363738394041303132333435242526272829 19 |191821202322131215141716 7 6 9 81110 1 0 3 2 5 4434245444746373639384140313033323534252427262928 20 |202218231921141612171315 810 611 7 9 2 4 0 5 1 3444642474345384036413739323430353133262824292527 21 |212319221820151713161214 911 710 6 8 3 5 1 4 0 2454743464244394137403638333531343032272925282426 22 |22202318211916141712151310 811 6 9 7 4 2 5 0 3 1464447424543403841363937343235303331282629242725 23 |23212219201817151613141211 910 7 8 6 5 3 4 1 2 0474546434442413940373836353334313230292728252624 24 |242526272829303132333435363738394041424344454647 0 1 2 3 4 5 6 7 8 91011121314151617181920212223 25 |252427262928313033323534373639384140434245444746 1 0 3 2 5 4 7 6 9 81110131215141716191821202322 26 |262824292527323430353133384036413739444642474345 2 4 0 5 1 3 810 611 7 9141612171315202218231921 27 |272925282426333531343032394137403638454743464244 3 5 1 4 0 2 911 710 6 8151713161214212319221820 28 |282629242725343235303331403841363937464447424543 4 2 5 0 3 110 811 6 9 7161417121513222023182119 29 |292728252624353334313230413940373836474546434442 5 3 4 1 2 011 910 7 8 6171516131412232122192018 30 |303132333435242526272829424344454647363738394041 6 7 8 91011 0 1 2 3 4 5181920212223121314151617 31 |313033323534252427262928434245444746373639384140 7 6 9 81110 1 0 3 2 5 4191821202322131215141716 32 |323430353133262824292527444642474345384036413739 810 611 7 9 2 4 0 5 1 3202218231921141612171315 33 |333531343032272925282426454743464244394137403638 911 710 6 8 3 5 1 4 0 2212319221820151713161214 34 |34323530333128262924272546444742454340384136393710 811 6 9 7 4 2 5 0 3 1222023182119161417121513 35 |35333431323029272825262447454643444241394037383611 910 7 8 6 5 3 4 1 2 0232122192018171516131412 36 |363738394041424344454647242526272829303132333435121314151617181920212223 0 1 2 3 4 5 6 7 8 91011 37 |373639384140434245444746252427262928313033323534131215141716191821202322 1 0 3 2 5 4 7 6 9 81110 38 |384036413739444642474345262824292527323430353133141612171315202218231921 2 4 0 5 1 3 810 611 7 9 39 |394137403638454743464244272925282426333531343032151713161214212319221820 3 5 1 4 0 2 911 710 6 8 40 |403841363937464447424543282629242725343235303331161417121513222023182119 4 2 5 0 3 110 811 6 9 7 41 |413940373836474546434442292728252624353334313230171516131412232122192018 5 3 4 1 2 011 910 7 8 6 42 |424344454647363738394041303132333435242526272829181920212223121314151617 6 7 8 91011 0 1 2 3 4 5 43 |434245444746373639384140313033323534252427262928191821202322131215141716 7 6 9 81110 1 0 3 2 5 4 44 |444642474345384036413739323430353133262824292527202218231921141612171315 810 611 7 9 2 4 0 5 1 3 45 |454743464244394137403638333531343032272925282426212319221820151713161214 911 710 6 8 3 5 1 4 0 2 46 |46444742454340384136393734323530333128262924272522202318211916141712151310 811 6 9 7 4 2 5 0 3 1 47 |47454643444241394037383635333431323029272825262423212219201817151613141211 910 7 8 6 5 3 4 1 2 0 -------- end of model -------- --------- statistics for domain size 48 --------- Current CPU time: 0.49 seconds (total CPU time: 0.49 seconds). Ground clauses: seen=110689, kept=110689. Selections=153, assignments=2766, propagations=31120, current_models=1. Rewrite_terms=625374, rewrite_bools=116719, indexes=168084. Rules_from_neg_clauses=0, cross_offs=7. ------------- memory usage (for entire run) ------------------- Total malloced: 20 megabytes type (bytes each) gets frees in use bytes chunk ( 104) 62 62 0 0.0 K string_buf ( 8) 60 60 0 0.0 K token ( 20) 93 93 0 0.0 K pterm ( 16) 46 46 0 0.0 K ilist ( 8) 12 12 0 0.0 K plist ( 8) 221494 221378 116 0.9 K mlist ( 12) 12 12 0 0.0 K term ( 16) 558141 558122 19 0.3 K term arg arrays: 0.1 K literal ( 12) 5 1 4 0.0 K clause ( 32) 5 1 4 0.1 K clist_pos ( 20) 4 4 0 0.0 K clist ( 16) 1 1 0 0.0 K mclause ( 20) 110689 110689 0 0.0 K (2594.3 K high) mstate ( 16) 2767 2767 0 0.0 K jnode ( 28) 33886 33886 0 0.0 K estack (3208) 5181 5181 0 0.0 K (avail=0, 0.0 K) Memory report, 1 @ 20 = 20 megs (16.15 megs used). List 2, length 110689, 864.8 K List 3, length 11, 0.1 K List 4, length 105, 1.6 K List 5, length 97, 1.9 K List 6, length 668452, 15666.8 K List 7, length 136, 3.7 K List 8, length 1, 0.0 K List 26, length 12, 1.2 K User_CPU=0.51, System_CPU=0.07, Wall_clock=1. Exiting with 1 model. Process 8587 exit (max_models) Tue Jul 5 21:30:21 2005 The process finished Tue Jul 5 21:30:21 2005