============================== Mace4 =================================
Mace4 (32) version Dec-2007, Dec 2007.
Process 20083 was started by mccune on cleo,
Sun Dec  9 21:37:57 2007
The command was "./mace4 -f t1.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file t1.in


formulas(assumptions).
p.
-p.
end_of_list.

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:

============================== end of process non-clausal formulas ===

============================== CLAUSES FOR SEARCH ====================

formulas(mace4_clauses).
p.
-p.
end_of_list.

============================== end of clauses for search =============

% There are no domain elements in the input.

============================== DOMAIN SIZE 2 =========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 2.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 3 =========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 3.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 4 =========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 4.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 5 =========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 5.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 6 =========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 6.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 7 =========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 7.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 8 =========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 9 =========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 9.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 10 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 10.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 11 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 11.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 12 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 12.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 13 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 13.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 14 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 14.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 15 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 15.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 16 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 16.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 17 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 17.

Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 18 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 18.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 19 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 19.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 20 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 20.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 21 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 21.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 22 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 22.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 23 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 23.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 24 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 24.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 25 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 25.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 26 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 26.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 27 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 27.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 28 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 28.

Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 29 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 29.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 30 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 30.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 31 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 31.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 32 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 32.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 33 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 33.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 34 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 34.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 35 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 35.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 36 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 36.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 37 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 37.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 38 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 38.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 39 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 39.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 40 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 40.

Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 41 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 41.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 42 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 42.

Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 43 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 43.

Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 44 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 44.

Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 45 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 45.

Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 46 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 46.

Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 47 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 47.

Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 48 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 48.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 49 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 49.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 50 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 50.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 51 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 51.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 52 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 52.

Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 53 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 53.

Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 54 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 54.

Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 55 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 55.

Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 56 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 56.

Current CPU time: 0.00 seconds (total CPU time: 0.07 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 57 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 57.

Current CPU time: 0.00 seconds (total CPU time: 0.07 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 58 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 58.

Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 59 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 59.

Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 60 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 60.

Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 61 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 61.

Current CPU time: 0.00 seconds (total CPU time: 0.09 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 62 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 62.

Current CPU time: 0.00 seconds (total CPU time: 0.09 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 63 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 63.

Current CPU time: 0.00 seconds (total CPU time: 0.09 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 64 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 64.

Current CPU time: 0.00 seconds (total CPU time: 0.09 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 65 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 65.

Current CPU time: 0.00 seconds (total CPU time: 0.10 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 66 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 66.

Current CPU time: 0.00 seconds (total CPU time: 0.10 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 67 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 67.

Current CPU time: 0.00 seconds (total CPU time: 0.10 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 68 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 68.

Current CPU time: 0.00 seconds (total CPU time: 0.11 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 69 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 69.

Current CPU time: 0.00 seconds (total CPU time: 0.11 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 70 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 70.

Current CPU time: 0.00 seconds (total CPU time: 0.11 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 71 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 71.

Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 72 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 72.

Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 73 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 73.

Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 74 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 74.

Current CPU time: 0.00 seconds (total CPU time: 0.13 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 75 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 75.

Current CPU time: 0.00 seconds (total CPU time: 0.13 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 76 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 76.

Current CPU time: 0.00 seconds (total CPU time: 0.14 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 77 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 77.

Current CPU time: 0.00 seconds (total CPU time: 0.14 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 78 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 78.

Current CPU time: 0.00 seconds (total CPU time: 0.15 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 79 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 79.

Current CPU time: 0.00 seconds (total CPU time: 0.15 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 80 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 80.

Current CPU time: 0.00 seconds (total CPU time: 0.16 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 81 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 81.

Current CPU time: 0.00 seconds (total CPU time: 0.16 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 82 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 82.

Current CPU time: 0.00 seconds (total CPU time: 0.17 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 83 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 83.

Current CPU time: 0.00 seconds (total CPU time: 0.17 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 84 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 84.

Current CPU time: 0.00 seconds (total CPU time: 0.18 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 85 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 85.

Current CPU time: 0.00 seconds (total CPU time: 0.18 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 86 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 86.

Current CPU time: 0.00 seconds (total CPU time: 0.19 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 87 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 87.

Current CPU time: 0.00 seconds (total CPU time: 0.20 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 88 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 88.

Current CPU time: 0.00 seconds (total CPU time: 0.20 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 89 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 89.

Current CPU time: 0.00 seconds (total CPU time: 0.21 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 90 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 90.

Current CPU time: 0.00 seconds (total CPU time: 0.22 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 91 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 91.

Current CPU time: 0.00 seconds (total CPU time: 0.22 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 92 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 92.

Current CPU time: 0.00 seconds (total CPU time: 0.23 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 93 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 93.

Current CPU time: 0.00 seconds (total CPU time: 0.24 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 94 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 94.

Current CPU time: 0.00 seconds (total CPU time: 0.24 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 95 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 95.

Current CPU time: 0.00 seconds (total CPU time: 0.25 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 96 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 96.

Current CPU time: 0.00 seconds (total CPU time: 0.26 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 97 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 97.

Current CPU time: 0.00 seconds (total CPU time: 0.26 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 98 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 98.

Current CPU time: 0.00 seconds (total CPU time: 0.27 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 99 ========================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 99.

Current CPU time: 0.00 seconds (total CPU time: 0.28 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 100 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 100.

Current CPU time: 0.00 seconds (total CPU time: 0.28 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 101 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 101.

Current CPU time: 0.00 seconds (total CPU time: 0.29 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 102 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 102.

Current CPU time: 0.00 seconds (total CPU time: 0.30 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 103 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 103.

Current CPU time: 0.00 seconds (total CPU time: 0.30 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 104 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 104.

Current CPU time: 0.00 seconds (total CPU time: 0.31 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 105 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 105.

Current CPU time: 0.00 seconds (total CPU time: 0.32 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 106 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 106.

Current CPU time: 0.00 seconds (total CPU time: 0.33 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 107 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 107.

Current CPU time: 0.00 seconds (total CPU time: 0.34 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 108 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 108.

Current CPU time: 0.00 seconds (total CPU time: 0.35 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 109 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 109.

Current CPU time: 0.00 seconds (total CPU time: 0.36 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 110 =======================

NOTE: unsatisfiability detected on input.

============================== STATISTICS ============================

For domain size 110.

Current CPU time: 0.00 seconds (total CPU time: 0.37 seconds).
Ground clauses: seen=2, kept=1.
Selections=0, assignments=0, propagations=1, current_models=0.
Rewrite_terms=0, rewrite_bools=1, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

============================== DOMAIN SIZE 111 =======================

mace4_sig_handler: condition 2
============================== STATISTICS ============================

For domain size 110.

Current CPU time: 0.00 seconds (total CPU time: 0.37 seconds).
Ground clauses: seen=0, kept=0.
Selections=0, assignments=0, propagations=0, current_models=0.
Rewrite_terms=0, rewrite_bools=0, indexes=0.
Rules_from_neg_clauses=0, cross_offs=0.

============================== end of statistics =====================

User_CPU=0.37, System_CPU=0.01, Wall_clock=1.

Exiting with failure.

Process 20083 exit (mace_sigint) Sun Dec  9 21:37:58 2007
The process finished Sun Dec  9 21:37:58 2007
