%--------------------------------------------------------------------------
% File     : PUZ016-1 : TPTP v9.0.0. Released v1.0.0.
% Domain   : Puzzles
% Problem  : Checkerboard and Dominoes : Row 1, columns 2 and 3 removed
% Version  : Especial.
% English  : There is a checker board whose second and third squares from
%            the first row have been removed. There is a box of dominoes
%            that are one square by two squares in size. Can you exactly
%            cover the checker board with dominoes?

% Refs     :
% Source   : [ANL]
% Names    : chekndom.ver2.in [ANL]

% Status   : Unsatisfiable
% Rating   : 0.08 v9.0.0, 0.06 v8.2.0, 0.08 v8.1.0, 0.00 v7.0.0, 0.14 v6.3.0, 0.17 v6.2.0, 0.00 v6.0.0, 0.11 v5.5.0, 0.31 v5.4.0, 0.27 v5.3.0, 0.33 v5.2.0, 0.00 v5.0.0, 0.29 v4.1.0, 0.22 v4.0.1, 0.00 v3.1.0, 0.22 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.17 v2.3.0, 0.00 v2.2.1, 0.56 v2.2.0, 0.57 v2.1.0, 0.60 v2.0.0
% Syntax   : Number of clauses     :   21 (  13 unt;   0 nHn;  21 RR)
%            Number of literals    :   29 (  11 equ;   9 neg)
%            Maximal clause size   :    2 (   1 avg)
%            Maximal term depth    :    3 (   1 avg)
%            Number of predicates  :    2 (   1 usr;   0 prp; 2-2 aty)
%            Number of functors    :   16 (  16 usr;  12 con; 0-8 aty)
%            Number of variables   :   58 (   0 sgn)
% SPC      : CNF_UNS_RFO_SEQ_HRN

% Comments :
%--------------------------------------------------------------------------
cnf(cover_columns_1_and_2,axiom,
    ( ~ achievable(row(X),squares(not_covered,not_covered,Y3,Y4,Y5,Y6,Y7,Y8))
    | achievable(row(X),squares(covered,covered,Y3,Y4,Y5,Y6,Y7,Y8)) ) ).

cnf(cover_columns_2_and_3,axiom,
    ( ~ achievable(row(X),squares(Y1,not_covered,not_covered,Y4,Y5,Y6,Y7,Y8))
    | achievable(row(X),squares(Y1,covered,covered,Y4,Y5,Y6,Y7,Y8)) ) ).

cnf(cover_columns_3_and_4,axiom,
    ( ~ achievable(row(X),squares(Y1,Y2,not_covered,not_covered,Y5,Y6,Y7,Y8))
    | achievable(row(X),squares(Y1,Y2,covered,covered,Y5,Y6,Y7,Y8)) ) ).

cnf(cover_columns_4_and_5,axiom,
    ( ~ achievable(row(X),squares(Y1,Y2,Y3,not_covered,not_covered,Y6,Y7,Y8))
    | achievable(row(X),squares(Y1,Y2,Y3,covered,covered,Y6,Y7,Y8)) ) ).

cnf(cover_columns_5_and_6,axiom,
    ( ~ achievable(row(X),squares(Y1,Y2,Y3,Y4,not_covered,not_covered,Y7,Y8))
    | achievable(row(X),squares(Y1,Y2,Y3,Y4,covered,covered,Y7,Y8)) ) ).

cnf(cover_columns_6_and_7,axiom,
    ( ~ achievable(row(X),squares(Y1,Y2,Y3,Y4,Y5,not_covered,not_covered,Y8))
    | achievable(row(X),squares(Y1,Y2,Y3,Y4,Y5,covered,covered,Y8)) ) ).

cnf(cover_columns_7_and_8,axiom,
    ( ~ achievable(row(X),squares(Y1,Y2,Y3,Y4,Y5,Y6,not_covered,not_covered))
    | achievable(row(X),squares(Y1,Y2,Y3,Y4,Y5,Y6,covered,covered)) ) ).

cnf(place_vertical_pieces,axiom,
    ( ~ achievable(row(X),squares(Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8))
    | achievable(row(successor(X)),squares(complement(Y1),complement(Y2),complement(Y3),complement(Y4),complement(Y5),complement(Y6),complement(Y7),complement(Y8))) ) ).

cnf(successor_of_1_is_2,axiom,
    successor(n1) = n2 ).

cnf(successor_of_2_is_3,axiom,
    successor(n2) = n3 ).

cnf(successor_of_3_is_4,axiom,
    successor(n3) = n4 ).

cnf(successor_of_4_is_5,axiom,
    successor(n4) = n5 ).

cnf(successor_of_5_is_6,axiom,
    successor(n5) = n6 ).

cnf(successor_of_6_is_7,axiom,
    successor(n6) = n7 ).

cnf(successor_of_7_is_8,axiom,
    successor(n7) = n8 ).

cnf(successor_of_8_is_9,axiom,
    successor(n8) = n9 ).

cnf(complement_of_covered_is_not_covered,axiom,
    complement(covered) = not_covered ).

cnf(complement_of_not_covered_is_covered,axiom,
    complement(not_covered) = covered ).

cnf(complement_of_removed_is_not_covered,axiom,
    complement(removed) = not_covered ).

%----This clause is in the original, but it not sensible or needed
% input_clause(can_do_anything_to_row_9,hypothesis,
%     [++achievable(row(9),squares(Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8))]).

cnf(first_row_initially,hypothesis,
    achievable(row(n1),squares(not_covered,removed,removed,not_covered,not_covered,not_covered,not_covered,not_covered)) ).

cnf(prove_row_8_can_be_covered,negated_conjecture,
    ~ achievable(row(n8),squares(covered,covered,covered,covered,covered,covered,covered,covered)) ).

%--------------------------------------------------------------------------