test/regress/regress0/tptp_parser.p


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

% EXPECT: unsat
% EXIT: 20

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

/*
cnf(query_1,axiom,
    $false | $false /* | $false).
*/

cnf(query_1,axiom,
    $false | $false | $false).

cnf(query_1,negated_conjecture, ~
    $false | $false | $false).

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