;------------------------------------------------------------------------------
; File     : NLP059+1 : TPTP v5.3.0. Released v2.4.0.
; Domain   : Natural Language Processing
; Problem  : A man comes out of the bathroom, problem 1
; Version  : [Bos00b] axioms.
; English  : Eliminating inconsistent interpretations in the statement
;            "A man comes out of the bathroom with a magnum in his hand.
;            The man fires six shots from his canon."

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

; Status   : CounterSatisfiable
; Rating   : 0.13 v5.3.0, 0.08 v5.2.0, 0.00 v4.1.0, 0.17 v4.0.1, 0.00 v3.4.0, 0.17 v3.3.0, 0.00 v2.7.0, 0.33 v2.6.0, 0.00 v2.4.0
; Syntax   : Number of formulae    :    1 (   0 unit)
;            Number of atoms       :   68 (   0 equality)
;            Maximal formula depth :   22 (  22 average)
;            Number of connectives :   69 (   2 ~  ;   0  |;  57  &)
;                                         (   0 <=>;  10 =>;   0 <=)
;                                         (   0 <~>;   0 ~|;   0 ~&)
;            Number of predicates  :   16 (   0 propositional; 1-3 arity)
;            Number of functors    :    0 (   0 constant; --- arity)
;            Number of variables   :   28 (   0 singleton;  10 !;  18 ?)
;            Maximal term depth    :    1 (   1 average)
; SPC      : FOF_CSA_RFO_NEQ

; Comments :
;          : tptp2X -f smt2 NLP059+1.p 
;------------------------------------------------------------------------------
(set-logic UFNIRA)

(declare-sort smt_individual 0)

; actual_world_1_type
(declare-fun actual_world (smt_individual) Bool)

; agent_3_type
(declare-fun agent (smt_individual smt_individual smt_individual) Bool)

; cannon_2_type
(declare-fun cannon (smt_individual smt_individual) Bool)

; event_2_type
(declare-fun event (smt_individual smt_individual) Bool)

; fire_2_type
(declare-fun fire (smt_individual smt_individual) Bool)

; from_loc_3_type
(declare-fun from_loc (smt_individual smt_individual smt_individual) Bool)

; group_2_type
(declare-fun group (smt_individual smt_individual) Bool)

; male_2_type
(declare-fun male (smt_individual smt_individual) Bool)

; man_2_type
(declare-fun man (smt_individual smt_individual) Bool)

; member_3_type
(declare-fun member (smt_individual smt_individual smt_individual) Bool)

; nonreflexive_2_type
(declare-fun nonreflexive (smt_individual smt_individual) Bool)

; of_3_type
(declare-fun of (smt_individual smt_individual smt_individual) Bool)

; patient_3_type
(declare-fun patient (smt_individual smt_individual smt_individual) Bool)

; present_2_type
(declare-fun present (smt_individual smt_individual) Bool)

; shot_2_type
(declare-fun shot (smt_individual smt_individual) Bool)

; six_2_type
(declare-fun six (smt_individual smt_individual) Bool)


;----This is the conjecture with negated conjecture; co1
(assert 
    (or (and (exists ((?U smt_individual)) 
                          (and (actual_world ?U)
                              (exists ((?V smt_individual) (?W smt_individual)) 
                                (and (male ?U ?V)
                                    (forall ((?X smt_individual)) 
                                      (=> (and (of ?U ?X ?V)
                                              (cannon ?U ?X)
                                              (member ?U ?X ?W) )
                                          (exists ((?Y smt_individual) (?Z smt_individual)) 
                                            (and (man ?U ?Y)
                                                (event ?U ?Z)
                                                (agent ?U ?Z ?Y)
                                                (patient ?U ?Z ?X)
                                                (present ?U ?Z)
                                                (nonreflexive ?U ?Z)
                                                (fire ?U ?Z)
                                                (from_loc ?U ?Z ?X) ) ) ) )
                                    (six ?U ?W)
                                    (group ?U ?W)
                                    (forall ((?X1 smt_individual)) 
                                      (=> (member ?U ?X1 ?W)
                                          (shot ?U ?X1) ) ) ) ) ) )
                        (not (exists ((?X2 smt_individual)) 
                          (and (actual_world ?X2)
                              (exists ((?X3 smt_individual) (?X4 smt_individual)) 
                                (and (male ?X2 ?X3)
                                    (forall ((?X5 smt_individual) (?X6 smt_individual)) 
                                      (=> (and (man ?X2 ?X5)
                                              (of ?X2 ?X6 ?X3)
                                              (cannon ?X2 ?X6)
                                              (member ?X2 ?X6 ?X4) )
                                          (exists ((?X7 smt_individual)) 
                                            (and (event ?X2 ?X7)
                                                (agent ?X2 ?X7 ?X5)
                                                (patient ?X2 ?X7 ?X6)
                                                (present ?X2 ?X7)
                                                (nonreflexive ?X2 ?X7)
                                                (fire ?X2 ?X7)
                                                (from_loc ?X2 ?X7 ?X6) ) ) ) )
                                    (six ?X2 ?X4)
                                    (group ?X2 ?X4)
                                    (forall ((?X8 smt_individual)) 
                                      (=> (member ?X2 ?X8 ?X4)
                                          (shot ?X2 ?X8) ) ) ) ) ) ) ) )
                    (and (exists ((?X2 smt_individual)) 
                          (and (actual_world ?X2)
                              (exists ((?X3 smt_individual) (?X4 smt_individual)) 
                                (and (male ?X2 ?X3)
                                    (forall ((?X5 smt_individual) (?X6 smt_individual)) 
                                      (=> (and (man ?X2 ?X5)
                                              (of ?X2 ?X6 ?X3)
                                              (cannon ?X2 ?X6)
                                              (member ?X2 ?X6 ?X4) )
                                          (exists ((?X7 smt_individual)) 
                                            (and (event ?X2 ?X7)
                                                (agent ?X2 ?X7 ?X5)
                                                (patient ?X2 ?X7 ?X6)
                                                (present ?X2 ?X7)
                                                (nonreflexive ?X2 ?X7)
                                                (fire ?X2 ?X7)
                                                (from_loc ?X2 ?X7 ?X6) ) ) ) )
                                    (six ?X2 ?X4)
                                    (group ?X2 ?X4)
                                    (forall ((?X8 smt_individual)) 
                                      (=> (member ?X2 ?X8 ?X4)
                                          (shot ?X2 ?X8) ) ) ) ) ) )
                        (not (exists ((?U smt_individual)) 
                          (and (actual_world ?U)
                              (exists ((?V smt_individual) (?W smt_individual)) 
                                (and (male ?U ?V)
                                    (forall ((?X smt_individual)) 
                                      (=> (and (of ?U ?X ?V)
                                              (cannon ?U ?X)
                                              (member ?U ?X ?W) )
                                          (exists ((?Y smt_individual) (?Z smt_individual)) 
                                            (and (man ?U ?Y)
                                                (event ?U ?Z)
                                                (agent ?U ?Z ?Y)
                                                (patient ?U ?Z ?X)
                                                (present ?U ?Z)
                                                (nonreflexive ?U ?Z)
                                                (fire ?U ?Z)
                                                (from_loc ?U ?Z ?X) ) ) ) )
                                    (six ?U ?W)
                                    (group ?U ?W)
                                    (forall ((?X1 smt_individual)) 
                                      (=> (member ?U ?X1 ?W)
                                          (shot ?U ?X1) ) ) ) ) ) ) ) ) )
)

(check-sat)
;------------------------------------------------------------------------------