cnf(clause_1,axiom,
    ( ~ big_p(X)
    | big_q(a) )).

cnf(clause_2,axiom,
    ( ~ big_q(X)
    | big_p(b) )).

cnf(clause_3,axiom,
    ( ~ big_p(X)
    | ~ big_q(Y)
    | ~ big_r(X)
    | big_s(Y) )).

cnf(clause_4,axiom,
    ( ~ big_p(X)
    | ~ big_q(Y)
    | ~ big_s(Y)
    | big_r(X) )).

cnf(clause_6,negated_conjecture,
    ( ~ big_p(X)
    | big_p(c)
    | big_r(X) )).

cnf(clause_10,negated_conjecture,
    ( big_p(c)
    | big_q(d) )).

cnf(clause_11,negated_conjecture,
    ( ~ big_r(c)
    | big_q(d) )).

cnf(clause_13,negated_conjecture,
    ( ~ big_r(c)
    | ~ big_s(d) )).

%cnf(clause_5,axiom,
%    ( ~ big_p(X)
%    | ~ big_q(X)
%    | big_r(X)
%    | big_s(X) )).

%cnf(clause_7,negated_conjecture,
%    ( ~ big_p(X)
%    | ~ big_r(c)
%    | big_r(X) )).

%cnf(clause_8,negated_conjecture,
%    ( ~ big_q(X)
%    | big_q(d)
%    | big_s(X) )).

%cnf(clause_9,negated_conjecture,
%    ( ~ big_q(X)
%    | ~ big_s(d)
%    | big_s(X) )).

%cnf(clause_12,negated_conjecture,
%    ( ~ big_s(d)
%    | big_p(c) )).