TPTP Problem File: NLP002^7.p

View Solutions - Solve Problem

```%------------------------------------------------------------------------------
% File     : NLP002^7 : TPTP v7.1.0. Released v5.5.0.
% Domain   : Natural Language Processing
% Problem  : "The old dirty white Chevy" problem 2
% Version  : [Ben12] axioms.
% English  :

% Refs     : [Bos00] Bos (2000), DORIS: Discourse Oriented Representation an
%          : [Ben12] Benzmueller (2012), Email to Geoff Sutcliffe
% Source   : [Ben12]
% Names    : s4-cumul-NLP002+1 [Ben12]

% Status   : CounterSatisfiable
% Rating   : 0.67 v5.5.0
% Syntax   : Number of formulae    :  188 (   0 unit;  72 type;  32 defn)
%            Number of atoms       : 1179 (  36 equality; 464 variable)
%            Maximal formula depth :   27 (   8 average)
%            Number of connectives :  996 (   5   ~;   5   |;   9   &; 967   @)
%                                         (   0 <=>;  10  =>;   0  <=;   0 <~>)
%                                         (   0  ~|;   0  ~&)
%            Number of type conns  :  259 ( 259   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   76 (  72   :;   0   =)
%            Number of variables   :  245 (   2 sgn;  34   !;   7   ?; 204   ^)
%                                         ( 245   :;   0  !>;   0  ?*)
%                                         (   0  @-;   0  @+)
% SPC      : TH0_CSA_EQU_NAR

%------------------------------------------------------------------------------
%----Include axioms for Modal logic S4 under cumulative domains
include('Axioms/LCL015^0.ax').
include('Axioms/LCL013^5.ax').
include('Axioms/LCL015^1.ax').
%------------------------------------------------------------------------------
thf(vehicle_type,type,(
vehicle: mu > \$i > \$o )).

thf(transport_type,type,(
transport: mu > \$i > \$o )).

thf(instrumentality_type,type,(
instrumentality: mu > \$i > \$o )).

thf(artifact_type,type,(
artifact: mu > \$i > \$o )).

thf(location_type,type,(
location: mu > \$i > \$o )).

thf(object_type,type,(
object: mu > \$i > \$o )).

thf(new_type,type,(
new: mu > \$i > \$o )).

thf(eventuality_type,type,(
eventuality: mu > \$i > \$o )).

thf(abstraction_type,type,(
abstraction: mu > \$i > \$o )).

thf(man_type,type,(
man: mu > \$i > \$o )).

thf(male_type,type,(
male: mu > \$i > \$o )).

thf(female_type,type,(
female: mu > \$i > \$o )).

thf(woman_type,type,(
woman: mu > \$i > \$o )).

thf(proposition_type,type,(
proposition: mu > \$i > \$o )).

thf(drs_type,type,(
drs: mu > \$i > \$o )).

thf(entity_type,type,(
entity: mu > \$i > \$o )).

thf(owner_type,type,(
owner: mu > \$i > \$o )).

thf(human_type,type,(
human: mu > \$i > \$o )).

thf(nonhuman_type,type,(
nonhuman: mu > \$i > \$o )).

thf(have_type,type,(
have: mu > mu > mu > \$i > \$o )).

thf(of_type,type,(
of: mu > mu > \$i > \$o )).

thf(partof_type,type,(
partof: mu > mu > \$i > \$o )).

thf(in_type,type,(
in: mu > mu > \$i > \$o )).

thf(down_type,type,(
down: mu > mu > \$i > \$o )).

thf(barrel_type,type,(
barrel: mu > mu > \$i > \$o )).

thf(old_type,type,(
old: mu > \$i > \$o )).

thf(dirty_type,type,(
dirty: mu > \$i > \$o )).

thf(white_type,type,(
white: mu > \$i > \$o )).

thf(car_type,type,(
car: mu > \$i > \$o )).

thf(chevy_type,type,(
chevy: mu > \$i > \$o )).

thf(lonely_type,type,(
lonely: mu > \$i > \$o )).

thf(way_type,type,(
way: mu > \$i > \$o )).

thf(street_type,type,(
street: mu > \$i > \$o )).

thf(event_type,type,(
event: mu > \$i > \$o )).

thf(city_type,type,(
city: mu > \$i > \$o )).

thf(hollywood_type,type,(
hollywood: mu > \$i > \$o )).

thf(reflexivity,axiom,
( mvalid
@ ( mforall_ind
@ ^ [X: mu] :
( qmltpeq @ X @ X ) ) )).

thf(symmetry,axiom,
( mvalid
@ ( mforall_ind
@ ^ [X: mu] :
( mforall_ind
@ ^ [Y: mu] :
( mimplies @ ( qmltpeq @ X @ Y ) @ ( qmltpeq @ Y @ X ) ) ) ) )).

thf(transitivity,axiom,
( mvalid
@ ( mforall_ind
@ ^ [X: mu] :
( mforall_ind
@ ^ [Y: mu] :
( mforall_ind
@ ^ [Z: mu] :
( mimplies @ ( mand @ ( qmltpeq @ X @ Y ) @ ( qmltpeq @ Y @ Z ) ) @ ( qmltpeq @ X @ Z ) ) ) ) ) )).

thf(abstraction_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( abstraction @ A ) ) @ ( abstraction @ B ) ) ) ) )).

thf(artifact_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( artifact @ A ) ) @ ( artifact @ B ) ) ) ) )).

thf(barrel_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( barrel @ A @ C ) ) @ ( barrel @ B @ C ) ) ) ) ) )).

thf(barrel_substitution_2,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( barrel @ C @ A ) ) @ ( barrel @ C @ B ) ) ) ) ) )).

thf(car_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( car @ A ) ) @ ( car @ B ) ) ) ) )).

thf(chevy_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( chevy @ A ) ) @ ( chevy @ B ) ) ) ) )).

thf(city_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( city @ A ) ) @ ( city @ B ) ) ) ) )).

thf(dirty_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( dirty @ A ) ) @ ( dirty @ B ) ) ) ) )).

thf(down_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( down @ A @ C ) ) @ ( down @ B @ C ) ) ) ) ) )).

thf(down_substitution_2,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( down @ C @ A ) ) @ ( down @ C @ B ) ) ) ) ) )).

thf(drs_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( drs @ A ) ) @ ( drs @ B ) ) ) ) )).

thf(entity_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( entity @ A ) ) @ ( entity @ B ) ) ) ) )).

thf(event_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( event @ A ) ) @ ( event @ B ) ) ) ) )).

thf(eventuality_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( eventuality @ A ) ) @ ( eventuality @ B ) ) ) ) )).

thf(female_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( female @ A ) ) @ ( female @ B ) ) ) ) )).

thf(have_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mforall_ind
@ ^ [D: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( have @ A @ C @ D ) ) @ ( have @ B @ C @ D ) ) ) ) ) ) )).

thf(have_substitution_2,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mforall_ind
@ ^ [D: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( have @ C @ A @ D ) ) @ ( have @ C @ B @ D ) ) ) ) ) ) )).

thf(have_substitution_3,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mforall_ind
@ ^ [D: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( have @ C @ D @ A ) ) @ ( have @ C @ D @ B ) ) ) ) ) ) )).

thf(hollywood_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( hollywood @ A ) ) @ ( hollywood @ B ) ) ) ) )).

thf(human_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( human @ A ) ) @ ( human @ B ) ) ) ) )).

thf(in_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( in @ A @ C ) ) @ ( in @ B @ C ) ) ) ) ) )).

thf(in_substitution_2,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( in @ C @ A ) ) @ ( in @ C @ B ) ) ) ) ) )).

thf(instrumentality_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( instrumentality @ A ) ) @ ( instrumentality @ B ) ) ) ) )).

thf(location_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( location @ A ) ) @ ( location @ B ) ) ) ) )).

thf(lonely_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( lonely @ A ) ) @ ( lonely @ B ) ) ) ) )).

thf(male_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( male @ A ) ) @ ( male @ B ) ) ) ) )).

thf(man_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( man @ A ) ) @ ( man @ B ) ) ) ) )).

thf(new_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( new @ A ) ) @ ( new @ B ) ) ) ) )).

thf(nonhuman_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( nonhuman @ A ) ) @ ( nonhuman @ B ) ) ) ) )).

thf(object_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( object @ A ) ) @ ( object @ B ) ) ) ) )).

thf(of_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( of @ A @ C ) ) @ ( of @ B @ C ) ) ) ) ) )).

thf(of_substitution_2,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( of @ C @ A ) ) @ ( of @ C @ B ) ) ) ) ) )).

thf(old_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( old @ A ) ) @ ( old @ B ) ) ) ) )).

thf(owner_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( owner @ A ) ) @ ( owner @ B ) ) ) ) )).

thf(partof_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( partof @ A @ C ) ) @ ( partof @ B @ C ) ) ) ) ) )).

thf(partof_substitution_2,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mforall_ind
@ ^ [C: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( partof @ C @ A ) ) @ ( partof @ C @ B ) ) ) ) ) )).

thf(proposition_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( proposition @ A ) ) @ ( proposition @ B ) ) ) ) )).

thf(street_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( street @ A ) ) @ ( street @ B ) ) ) ) )).

thf(transport_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( transport @ A ) ) @ ( transport @ B ) ) ) ) )).

thf(vehicle_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( vehicle @ A ) ) @ ( vehicle @ B ) ) ) ) )).

thf(way_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( way @ A ) ) @ ( way @ B ) ) ) ) )).

thf(white_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( white @ A ) ) @ ( white @ B ) ) ) ) )).

thf(woman_substitution_1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [A: mu] :
( mforall_ind
@ ^ [B: mu] :
( mimplies @ ( mand @ ( qmltpeq @ A @ B ) @ ( woman @ A ) ) @ ( woman @ B ) ) ) ) )).

thf(ax1,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( chevy @ U ) @ ( car @ U ) ) ) )).

thf(ax2,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( car @ U ) @ ( vehicle @ U ) ) ) )).

thf(ax3,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( vehicle @ U ) @ ( transport @ U ) ) ) )).

thf(ax4,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( transport @ U ) @ ( instrumentality @ U ) ) ) )).

thf(ax5,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( instrumentality @ U ) @ ( artifact @ U ) ) ) )).

thf(ax6,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( instrumentality @ U ) @ ( mnot @ ( way @ U ) ) ) ) )).

thf(ax7,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( street @ U ) @ ( way @ U ) ) ) )).

thf(ax8,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( way @ U ) @ ( artifact @ U ) ) ) )).

thf(ax9,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( artifact @ U ) @ ( object @ U ) ) ) )).

thf(ax10,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( artifact @ U ) @ ( mnot @ ( location @ U ) ) ) ) )).

thf(ax11,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( event @ U ) @ ( eventuality @ U ) ) ) )).

thf(ax12,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( hollywood @ U ) @ ( city @ U ) ) ) )).

thf(ax13,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( city @ U ) @ ( location @ U ) ) ) )).

thf(ax14,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( location @ U ) @ ( object @ U ) ) ) )).

thf(ax15,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( object @ U ) @ ( entity @ U ) ) ) )).

thf(ax16,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( old @ U ) @ ( mnot @ ( new @ U ) ) ) ) )).

thf(ax17,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( eventuality @ U ) @ ( mnot @ ( entity @ U ) ) ) ) )).

thf(ax18,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( abstraction @ U ) @ ( mnot @ ( entity @ U ) ) ) ) )).

thf(ax19,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( abstraction @ U ) @ ( mnot @ ( eventuality @ U ) ) ) ) )).

thf(ax20,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( male @ U ) @ ( mnot @ ( female @ U ) ) ) ) )).

thf(ax21,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( man @ U ) @ ( mnot @ ( woman @ U ) ) ) ) )).

thf(ax22,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( man @ U ) @ ( male @ U ) ) ) )).

thf(ax23,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( male @ U ) @ ( human @ U ) ) ) )).

thf(ax24,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( female @ U ) @ ( human @ U ) ) ) )).

thf(ax25,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( woman @ U ) @ ( female @ U ) ) ) )).

thf(ax26,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mequiv @ ( drs @ U ) @ ( proposition @ U ) ) ) )).

thf(ax27,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( nonhuman @ U ) @ ( entity @ U ) ) ) )).

thf(ax28,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mimplies @ ( human @ U ) @ ( mnot @ ( nonhuman @ U ) ) ) ) )).

thf(ax29,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mforall_ind
@ ^ [V: mu] :
( mforall_ind
@ ^ [W: mu] :
( mequiv @ ( mand @ ( have @ U @ V @ W ) @ ( human @ V ) ) @ ( mand @ ( owner @ V ) @ ( of @ V @ W ) ) ) ) ) ) )).

thf(ax30,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mforall_ind
@ ^ [V: mu] :
( mforall_ind
@ ^ [W: mu] :
( mimplies @ ( mand @ ( have @ U @ V @ W ) @ ( mand @ ( nonhuman @ V ) @ ( nonhuman @ W ) ) ) @ ( partof @ W @ V ) ) ) ) ) )).

thf(ax31,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mforall_ind
@ ^ [V: mu] :
( mforall_ind
@ ^ [W: mu] :
( mimplies @ ( mand @ ( event @ U ) @ ( have @ U @ V @ W ) ) @ ( of @ V @ W ) ) ) ) ) )).

thf(ax32,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mforall_ind
@ ^ [V: mu] :
( mimplies @ ( of @ V @ U )
@ ( mexists_ind
@ ^ [W: mu] :
( mand @ ( event @ W ) @ ( have @ W @ U @ V ) ) ) ) ) ) )).

thf(ax33,axiom,
( mvalid
@ ( mforall_ind
@ ^ [U: mu] :
( mforall_ind
@ ^ [V: mu] :
( mforall_ind
@ ^ [W: mu] :
( mimplies @ ( mand @ ( partof @ U @ V ) @ ( partof @ U @ W ) ) @ ( qmltpeq @ V @ W ) ) ) ) ) )).

thf(co1,conjecture,
( mvalid
@ ( mnot
@ ( mexists_ind
@ ^ [U: mu] :
( mexists_ind
@ ^ [V: mu] :
( mexists_ind
@ ^ [W: mu] :
( mexists_ind
@ ^ [X: mu] :
( mand @ ( hollywood @ U ) @ ( mand @ ( city @ U ) @ ( mand @ ( event @ V ) @ ( mand @ ( street @ W ) @ ( mand @ ( way @ W ) @ ( mand @ ( lonely @ W ) @ ( mand @ ( chevy @ X ) @ ( mand @ ( car @ X ) @ ( mand @ ( white @ X ) @ ( mand @ ( dirty @ X ) @ ( mand @ ( old @ X ) @ ( mand @ ( barrel @ V @ X ) @ ( mand @ ( down @ V @ W ) @ ( in @ V @ U ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )).

%------------------------------------------------------------------------------
```