%--------------------------------------------------------------------------
% File     : NLP116-1 : TPTP v2.4.1. Released v2.4.0.
% Domain   : Natural Language Processing
% Problem  : An old dirty white Chevy, problem 3
% Version  : [Bos00b] axioms.
% English  : Eliminating logically equivalent interpretations in the statement
%            "An old dirty white chevy barrels down a lonely street in 
%            hollywood."

% Refs     : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a
%            [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language
% Source   : [TPTP]
% Names    : 

% Status   : satisfiable
% Rating   : 0.00 v2.4.0
% Syntax   : Number of clauses    :   36 (  16 non-Horn;   2 unit;  36 RR)
%            Number of literals   :  102 (   0 equality)
%            Maximal clause size  :   18 (   2 average)
%            Number of predicates :   18 (   1 propositional; 0-3 arity)
%            Number of functors   :   10 (  10 constant; 0-0 arity)
%            Number of variables  :   10 (   0 singleton)
%            Maximal term depth   :    1 (   1 average)

% Comments : Created from NLP116+1.p using FLOTTER
%          : tptp2X -f tptp NLP116-1.p 
%--------------------------------------------------------------------------
input_clause(clause1,conjecture,
    [++ actual_world(skc15)]).

input_clause(clause2,conjecture,
    [++ actual_world(skc10)]).

input_clause(clause3,conjecture,
    [++ ssSkC0,
     ++ event(skc15, skc16)]).

input_clause(clause4,conjecture,
    [++ ssSkC0,
     ++ present(skc15, skc16)]).

input_clause(clause5,conjecture,
    [++ ssSkC0,
     ++ barrel(skc15, skc16)]).

input_clause(clause6,conjecture,
    [++ ssSkC0,
     ++ lonely(skc15, skc19)]).

input_clause(clause7,conjecture,
    [++ ssSkC0,
     ++ street(skc15, skc19)]).

input_clause(clause8,conjecture,
    [++ ssSkC0,
     ++ old(skc15, skc17)]).

input_clause(clause9,conjecture,
    [++ ssSkC0,
     ++ dirty(skc15, skc17)]).

input_clause(clause10,conjecture,
    [++ ssSkC0,
     ++ white(skc15, skc17)]).

input_clause(clause11,conjecture,
    [++ ssSkC0,
     ++ chevy(skc15, skc17)]).

input_clause(clause12,conjecture,
    [++ ssSkC0,
     ++ city(skc15, skc17)]).

input_clause(clause13,conjecture,
    [++ ssSkC0,
     ++ hollywood_placename(skc15, skc18)]).

input_clause(clause14,conjecture,
    [++ ssSkC0,
     ++ placename(skc15, skc18)]).

input_clause(clause15,conjecture,
    [-- ssSkC0,
     ++ city(skc10, skc13)]).

input_clause(clause16,conjecture,
    [-- ssSkC0,
     ++ street(skc10, skc13)]).

input_clause(clause17,conjecture,
    [-- ssSkC0,
     ++ lonely(skc10, skc13)]).

input_clause(clause18,conjecture,
    [-- ssSkC0,
     ++ placename(skc10, skc14)]).

input_clause(clause19,conjecture,
    [-- ssSkC0,
     ++ hollywood_placename(skc10, skc14)]).

input_clause(clause20,conjecture,
    [-- ssSkC0,
     ++ event(skc10, skc11)]).

input_clause(clause21,conjecture,
    [-- ssSkC0,
     ++ present(skc10, skc11)]).

input_clause(clause22,conjecture,
    [-- ssSkC0,
     ++ barrel(skc10, skc11)]).

input_clause(clause23,conjecture,
    [-- ssSkC0,
     ++ old(skc10, skc12)]).

input_clause(clause24,conjecture,
    [-- ssSkC0,
     ++ dirty(skc10, skc12)]).

input_clause(clause25,conjecture,
    [-- ssSkC0,
     ++ white(skc10, skc12)]).

input_clause(clause26,conjecture,
    [-- ssSkC0,
     ++ chevy(skc10, skc12)]).

input_clause(clause27,conjecture,
    [++ ssSkC0,
     ++ down(skc15, skc16, skc19)]).

input_clause(clause28,conjecture,
    [++ ssSkC0,
     ++ in(skc15, skc16, skc17)]).

input_clause(clause29,conjecture,
    [++ ssSkC0,
     ++ agent(skc15, skc16, skc17)]).

input_clause(clause30,conjecture,
    [++ ssSkC0,
     ++ of(skc15, skc18, skc17)]).

input_clause(clause31,conjecture,
    [-- ssSkC0,
     ++ down(skc10, skc11, skc13)]).

input_clause(clause32,conjecture,
    [-- ssSkC0,
     ++ in(skc10, skc11, skc13)]).

input_clause(clause33,conjecture,
    [-- ssSkC0,
     ++ of(skc10, skc14, skc13)]).

input_clause(clause34,conjecture,
    [-- ssSkC0,
     ++ agent(skc10, skc11, skc12)]).

input_clause(clause35,conjecture,
    [-- city(U, V),
     -- street(U, V),
     -- lonely(U, V),
     -- down(U, W, V),
     -- in(U, W, V),
     -- placename(U, X),
     -- hollywood_placename(U, X),
     -- of(U, X, V),
     -- event(U, W),
     -- present(U, W),
     -- barrel(U, W),
     -- agent(U, W, Y),
     -- old(U, Y),
     -- dirty(U, Y),
     -- white(U, Y),
     -- chevy(U, Y),
     -- actual_world(U),
     ++ ssSkC0]).

input_clause(clause36,conjecture,
    [-- event(U, V),
     -- present(U, V),
     -- barrel(U, V),
     -- down(U, V, W),
     -- lonely(U, W),
     -- street(U, W),
     -- in(U, V, X),
     -- agent(U, V, X),
     -- old(U, X),
     -- dirty(U, X),
     -- white(U, X),
     -- chevy(U, X),
     -- city(U, X),
     -- of(U, Y, X),
     -- hollywood_placename(U, Y),
     -- placename(U, Y),
     -- actual_world(U),
     -- ssSkC0]).
%--------------------------------------------------------------------------