test/regress/regress0/tptp_parser7.p


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

% EXPECT: unknown
% EXIT: 0

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

cnf(query_1,axiom, p( A, d ) | b ).

cnf(query_1,axiom, b | c ).

cnf(query_1,axiom, ~p(A, axiom) ).

cnf(query_1,axiom, axiom != d ).

cnf(query_1,negated_conjecture, ~ b ).

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