test/regress/regress0/tptp/tptp_parser5.p

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