----- 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:24 2005 The command was "../bin/mace4". The process ID is 8595. assign(domain_size,8). set(verbose). formulas(theory). (all x all y (G5(x,y) <-> x = 0 & y = 0 | x = 7 & y = 7)). end_of_list. clauses(theory). - G3(0,x). - G4(x,0). - G1(7,x). - G2(x,7). S(0,1). S(1,2). S(2,3). S(3,4). S(4,5). S(5,6). S(6,7). - S(x,y) | L(x,y). - L(x,y) | - L(y,z) | L(x,z). - L(x,y) | - L(y,z) | - S(x,z). - L(x,y) | x != y. G1(x,y) | G2(x,y) | G3(x,y) | G4(x,y) | G5(x,y). - G1(x,y) | - G2(x,y). - G1(x,y) | - G3(x,y). - G1(x,y) | - G4(x,y). - G1(x,y) | - G5(x,y). - G2(x,y) | - G3(x,y). - G2(x,y) | - G4(x,y). - G2(x,y) | - G5(x,y). - G3(x,y) | - G4(x,y). - G3(x,y) | - G5(x,y). - G4(x,y) | - G5(x,y). - S(x,y) | - G1(x,z) | G3(y,z). - S(x,y) | G1(x,z) | - G3(y,z). - S(x,y) | - G2(z,x) | G4(z,y). - S(x,y) | G2(z,x) | - G4(z,y). end_of_list. % Finished reading the input. % The maximum domain element in the input is 7. === Starting model search for domain size 8. === Initial partial model: G5 : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 1 0 0 0 0 0 0 0 1 | 0 0 0 0 0 0 0 0 2 | 0 0 0 0 0 0 0 0 3 | 0 0 0 0 0 0 0 0 4 | 0 0 0 0 0 0 0 0 5 | 0 0 0 0 0 0 0 0 6 | 0 0 0 0 0 0 0 0 7 | 0 0 0 0 0 0 0 1 G3 : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 0 0 0 0 0 0 0 1 | 0 - - - - - - - 2 | - - - - - - - - 3 | - - - - - - - - 4 | - - - - - - - - 5 | - - - - - - - - 6 | - - - - - - - - 7 | - - - - - - - 0 G4 : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 0 - - - - - - 1 | 0 - - - - - - - 2 | 0 - - - - - - - 3 | 0 - - - - - - - 4 | 0 - - - - - - - 5 | 0 - - - - - - - 6 | 0 - - - - - - - 7 | 0 - - - - - - 0 G1 : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 - - - - - - - 1 | - - - - - - - - 2 | - - - - - - - - 3 | - - - - - - - - 4 | - - - - - - - - 5 | - - - - - - - - 6 | - - - - - - - 0 7 | 0 0 0 0 0 0 0 0 G2 : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 - - - - - - 0 1 | - - - - - - - 0 2 | - - - - - - - 0 3 | - - - - - - - 0 4 | - - - - - - - 0 5 | - - - - - - - 0 6 | - - - - - - - 0 7 | - - - - - - 0 0 S : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 1 0 0 0 0 0 0 1 | 0 0 1 0 0 0 0 0 2 | 0 0 0 1 0 0 0 0 3 | 0 0 0 0 1 0 0 0 4 | 0 0 0 0 0 1 0 0 5 | 0 0 0 0 0 0 1 0 6 | 0 0 0 0 0 0 0 1 7 | 0 0 0 0 0 0 0 0 L : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 1 1 1 1 1 1 1 1 | 0 0 1 1 1 1 1 1 2 | 0 0 0 1 1 1 1 1 3 | 0 0 0 0 1 1 1 1 4 | 0 0 0 0 0 1 1 1 5 | 0 0 0 0 0 0 1 1 6 | 0 0 0 0 0 0 0 1 7 | 0 0 0 0 0 0 0 0 --------- statistics for domain size 8 --------- Current CPU time: 10.53 seconds (total CPU time: 10.54 seconds). Ground clauses: seen=4327, kept=1084. Selections=186339, assignments=372678, propagations=7074222, current_models=0. Rewrite_terms=0, rewrite_bools=24093354, indexes=0. Rules_from_neg_clauses=0, cross_offs=0. ------------- memory usage (for entire run) ------------------- Total malloced: 20 megabytes type (bytes each) gets frees in use bytes chunk ( 104) 445 445 0 0.0 K string_buf ( 8) 421 421 0 0.0 K token ( 20) 721 721 0 0.0 K pterm ( 16) 399 399 0 0.0 K ilist ( 8) 36 36 0 0.0 K plist ( 8) 3429 3224 205 1.6 K mlist ( 12) 43 43 0 0.0 K term ( 16) 31639 31516 123 1.9 K term arg arrays: 0.6 K literal ( 12) 77 1 76 0.9 K clause ( 32) 37 1 36 1.1 K clist_pos ( 20) 30 30 0 0.0 K clist ( 16) 1 1 0 0.0 K mclause ( 20) 1084 1084 0 0.0 K (29.5 K high) mstate ( 16) 372679 372679 0 0.0 K jnode ( 28) 7446900 7446900 0 0.0 K estack (3208) 383294 383294 0 0.0 K (avail=0, 0.0 K) Memory report, 1 @ 20 = 20 megs (0.11 megs used). List 1, length 10, 0.0 K List 2, length 1084, 8.5 K List 3, length 6, 0.1 K List 4, length 30, 0.5 K List 5, length 53, 1.0 K List 6, length 2843, 66.6 K List 7, length 842, 23.0 K List 8, length 4, 0.1 K List 9, length 24, 0.8 K List 10, length 36, 1.4 K List 26, length 65, 6.6 K User_CPU=10.54, System_CPU=0.07, Wall_clock=11. Exiting with failure. Process 8595 exit (exhausted) Tue Jul 5 21:30:35 2005 The process finished Tue Jul 5 21:30:35 2005