----- MACE 2.2, August 2003 ----- The process was started by mccune on gyro.thornwood, Tue Aug 19 14:47:18 2003 The command was "../../bin/mace2 -n2 -N6 -p". set(prolog_style_variables). set(tptp_eq). set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). clear(print_given). list(usable). 0 [] lives(agatha). 0 [] lives(butler). 0 [] lives(charles). 0 [] -killed(X,Y)| -richer(X,Y). 0 [] -hates(agatha,X)| -hates(charles,X). 0 [] -hates(X,agatha)| -hates(X,butler)| -hates(X,charles). 0 [] hates(agatha,agatha). 0 [] hates(agatha,charles). 0 [] -killed(X,Y)|hates(X,Y). 0 [] -hates(agatha,X)|hates(butler,X). 0 [] -lives(X)|richer(X,agatha)|hates(butler,X). end_of_list. list(sos). 0 [] killed(agatha,agatha)|killed(butler,agatha)|killed(charles,agatha). end_of_list. list(clauses). 1 [] lives(agatha). 2 [] lives(butler). 3 [] lives(charles). 4 [] -killed(X,Y)| -richer(X,Y). 5 [] -hates(agatha,X)| -hates(charles,X). 6 [] -hates(X,agatha)| -hates(X,butler)| -hates(X,charles). 7 [] hates(agatha,agatha). 8 [] hates(agatha,charles). 9 [] -killed(X,Y)|hates(X,Y). 10 [] -hates(agatha,X)|hates(butler,X). 11 [] -lives(X)|richer(X,agatha)|hates(butler,X). 12 [] killed(agatha,agatha)|killed(butler,agatha)|killed(charles,agatha). end_of_list. list(flattened_and_parted_clauses). 1 [] -equal(agatha,A)|lives(A). 2 [] -equal(butler,A)|lives(A). 3 [] -equal(charles,A)|lives(A). 4 [] -killed(A,B)| -richer(A,B). 5 [] -equal(charles,A)| -hates(A,B)| -$Connect1(B). 5 [] -equal(agatha,A)| -hates(A,B)|$Connect1(B). 6 [] -equal(charles,A)| -hates(B,A)| -$Connect2(B)| -$Connect3(B). 6 [] -equal(butler,A)| -hates(B,A)|$Connect3(B). 6 [] -equal(agatha,A)| -hates(B,A)|$Connect2(B). 7 [] -equal(agatha,A)|hates(A,A). 8 [] -equal(charles,A)| -equal(agatha,B)|hates(B,A). 9 [] -killed(A,B)|hates(A,B). 10 [] -equal(butler,A)|hates(A,B)| -$Connect4(B). 10 [] -equal(agatha,A)| -hates(A,B)|$Connect4(B). 11 [] -equal(butler,A)| -lives(B)|hates(A,B)| -$Connect5(B). 11 [] -equal(agatha,A)|richer(B,A)|$Connect5(B). 12 [] -equal(charles,A)| -equal(agatha,B)|killed(B,B)|killed(A,B)| -$Connect6(B). 12 [] -equal(butler,A)|killed(A,B)|$Connect6(B). end_of_list. --- Starting search for models of size 2 --- Applying isomorphism constraints to constants: agatha butler charles. 75 clauses were generated; 56 of those survived the first stage of unit preprocessing; there are 36 atoms. After all unit preprocessing, 16 atoms are still unassigned; 14 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 56 Literal occurrences input 129 Greatest atom 36 Unit preprocess: Preprocess unit assignments 20 Clauses after subsumption 14 Literal occ. after subsump. 35 Selectable clauses 6 Decide: Splits 0 Unit assignments 0 Failed paths 1 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: agatha butler charles. 162 clauses were generated; 118 of those survived the first stage of unit preprocessing; there are 66 atoms. After all unit preprocessing, 48 atoms are still unassigned; 88 clauses remain; 18 of those are non-Horn (selectable); 4883 K allocated; cpu time so far for this domain size: 0.00 sec. ======================= Model #1 at 0.00 seconds: agatha: 0 lives : 0 1 2 --------- T T T butler: 1 charles: 2 killed : | 0 1 2 --+------ 0 | T F F 1 | F F T 2 | F F F richer : | 0 1 2 --+------ 0 | F F F 1 | T F F 2 | T F F hates : | 0 1 2 --+------ 0 | T F T 1 | T F T 2 | F F F end_of_model  Exit by max_models parameter. The set is satisfiable (1 model(s) found). ----- statistics for domain size 3 ---- Input: Clauses input 118 Literal occurrences input 291 Greatest atom 66 Unit preprocess: Preprocess unit assignments 18 Clauses after subsumption 88 Literal occ. after subsump. 240 Selectable clauses 18 Decide: Splits 3 Unit assignments 36 Failed paths 1 Memory: Memory malloced 1 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 Aug 19 14:47:18 2003