1 2 3 4 5 6 7 8 9 10 11 12 13 14
% COMMAND-LINE: --finite-model-find % Status: Unsatisfiable %-------------------------------------------------------------------------- cnf(query_1,axiom, p( A, d ) | b ). cnf(query_1,axiom, b | c ). cnf(query_1,axiom, ~p(A, d) | ~ 'c' ). cnf(query_1,negated_conjecture, ~ b ). %--------------------------------------------------------------------------