%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NLP079+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 05:32:50 EDT 2022 % Result : Theorem 1.65s 1.90s % Output : Proof 1.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : NLP079+1 : TPTP v8.1.0. Released v2.4.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n015.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jul 1 09:44:58 EDT 2022 % 0.12/0.33 % CPUTime : % 1.65/1.90 % SZS status Theorem % 1.65/1.90 (* PROOF-FOUND *) % 1.65/1.90 (* BEGIN-PROOF *) % 1.65/1.90 % SZS output start Proof % 1.65/1.90 1. (actual_world T_0) (-. (actual_world T_0)) ### Axiom % 1.65/1.90 2. (male T_0 T_1) (-. (male T_0 T_1)) ### Axiom % 1.65/1.90 3. (male T_0 T_2) (-. (male T_0 T_2)) ### Axiom % 1.65/1.90 4. (man T_0 T_2) (-. (man T_0 T_2)) ### Axiom % 1.65/1.90 5. (of T_0 T_3 T_2) (-. (of T_0 T_3 T_2)) ### Axiom % 1.65/1.90 6. (cannon T_0 T_3) (-. (cannon T_0 T_3)) ### Axiom % 1.65/1.90 7. (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (-. (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3))))))))))) ### Axiom % 1.65/1.90 8. (six T_0 T_4) (-. (six T_0 T_4)) ### Axiom % 1.65/1.90 9. (group T_0 T_4) (-. (group T_0 T_4)) ### Axiom % 1.65/1.90 10. (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (-. (All X5, ((member T_0 X5 T_4) => (shot T_0 X5)))) ### Axiom % 1.65/1.90 11. (cry T_0 T_5) (-. (cry T_0 T_5)) ### Axiom % 1.65/1.90 12. (revenge T_0 T_6) (-. (revenge T_0 T_6)) ### Axiom % 1.65/1.90 13. (event T_0 T_7) (-. (event T_0 T_7)) ### Axiom % 1.65/1.90 14. (agent T_0 T_7 T_1) (-. (agent T_0 T_7 T_1)) ### Axiom % 1.65/1.90 15. (patient T_0 T_7 T_5) (-. (patient T_0 T_7 T_5)) ### Axiom % 1.65/1.90 16. (present T_0 T_7) (-. (present T_0 T_7)) ### Axiom % 1.65/1.90 17. (nonreflexive T_0 T_7) (-. (nonreflexive T_0 T_7)) ### Axiom % 1.65/1.90 18. (scream T_0 T_7) (-. (scream T_0 T_7)) ### Axiom % 1.65/1.90 19. (of T_0 T_7 T_6) (-. (of T_0 T_7 T_6)) ### Axiom % 1.65/1.90 20. (-. ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 T_3 T_2) /\ ((cannon T_0 T_3) /\ ((All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) /\ ((six T_0 T_4) /\ ((group T_0 T_4) /\ ((All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) /\ ((cry T_0 T_5) /\ ((revenge T_0 T_6) /\ ((event T_0 T_7) /\ ((agent T_0 T_7 T_1) /\ ((patient T_0 T_7 T_5) /\ ((present T_0 T_7) /\ ((nonreflexive T_0 T_7) /\ ((scream T_0 T_7) /\ (of T_0 T_7 T_6))))))))))))))))))) (of T_0 T_7 T_6) (scream T_0 T_7) (nonreflexive T_0 T_7) (present T_0 T_7) (patient T_0 T_7 T_5) (agent T_0 T_7 T_1) (event T_0 T_7) (revenge T_0 T_6) (cry T_0 T_5) (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (group T_0 T_4) (six T_0 T_4) (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (cannon T_0 T_3) (of T_0 T_3 T_2) (man T_0 T_2) (male T_0 T_2) (male T_0 T_1) ### DisjTree 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 % 1.65/1.90 21. (-. (Ex X13, ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 T_3 T_2) /\ ((cannon T_0 T_3) /\ ((All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) /\ ((six T_0 T_4) /\ ((group T_0 T_4) /\ ((All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) /\ ((cry T_0 T_5) /\ ((revenge T_0 T_6) /\ ((event T_0 X13) /\ ((agent T_0 X13 T_1) /\ ((patient T_0 X13 T_5) /\ ((present T_0 X13) /\ ((nonreflexive T_0 X13) /\ ((scream T_0 X13) /\ (of T_0 X13 T_6)))))))))))))))))))) (male T_0 T_1) (male T_0 T_2) (man T_0 T_2) (of T_0 T_3 T_2) (cannon T_0 T_3) (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (six T_0 T_4) (group T_0 T_4) (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (cry T_0 T_5) (revenge T_0 T_6) (event T_0 T_7) (agent T_0 T_7 T_1) (patient T_0 T_7 T_5) (present T_0 T_7) (nonreflexive T_0 T_7) (scream T_0 T_7) (of T_0 T_7 T_6) ### NotExists 20 % 1.65/1.90 22. (-. (Ex X12, (Ex X13, ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 T_3 T_2) /\ ((cannon T_0 T_3) /\ ((All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) /\ ((six T_0 T_4) /\ ((group T_0 T_4) /\ ((All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) /\ ((cry T_0 T_5) /\ ((revenge T_0 X12) /\ ((event T_0 X13) /\ ((agent T_0 X13 T_1) /\ ((patient T_0 X13 T_5) /\ ((present T_0 X13) /\ ((nonreflexive T_0 X13) /\ ((scream T_0 X13) /\ (of T_0 X13 X12))))))))))))))))))))) (of T_0 T_7 T_6) (scream T_0 T_7) (nonreflexive T_0 T_7) (present T_0 T_7) (patient T_0 T_7 T_5) (agent T_0 T_7 T_1) (event T_0 T_7) (revenge T_0 T_6) (cry T_0 T_5) (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (group T_0 T_4) (six T_0 T_4) (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (cannon T_0 T_3) (of T_0 T_3 T_2) (man T_0 T_2) (male T_0 T_2) (male T_0 T_1) ### NotExists 21 % 1.65/1.90 23. (-. (Ex X11, (Ex X12, (Ex X13, ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 T_3 T_2) /\ ((cannon T_0 T_3) /\ ((All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) /\ ((six T_0 T_4) /\ ((group T_0 T_4) /\ ((All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) /\ ((cry T_0 X11) /\ ((revenge T_0 X12) /\ ((event T_0 X13) /\ ((agent T_0 X13 T_1) /\ ((patient T_0 X13 X11) /\ ((present T_0 X13) /\ ((nonreflexive T_0 X13) /\ ((scream T_0 X13) /\ (of T_0 X13 X12)))))))))))))))))))))) (male T_0 T_1) (male T_0 T_2) (man T_0 T_2) (of T_0 T_3 T_2) (cannon T_0 T_3) (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (six T_0 T_4) (group T_0 T_4) (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (cry T_0 T_5) (revenge T_0 T_6) (event T_0 T_7) (agent T_0 T_7 T_1) (patient T_0 T_7 T_5) (present T_0 T_7) (nonreflexive T_0 T_7) (scream T_0 T_7) (of T_0 T_7 T_6) ### NotExists 22 % 1.65/1.90 24. (-. (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 T_3 T_2) /\ ((cannon T_0 T_3) /\ ((All X14, ((member T_0 X14 X10) => (Ex X15, ((event T_0 X15) /\ ((agent T_0 X15 T_2) /\ ((patient T_0 X15 X14) /\ ((present T_0 X15) /\ ((nonreflexive T_0 X15) /\ ((fire T_0 X15) /\ (from_loc T_0 X15 T_3)))))))))) /\ ((six T_0 X10) /\ ((group T_0 X10) /\ ((All X16, ((member T_0 X16 X10) => (shot T_0 X16))) /\ ((cry T_0 X11) /\ ((revenge T_0 X12) /\ ((event T_0 X13) /\ ((agent T_0 X13 T_1) /\ ((patient T_0 X13 X11) /\ ((present T_0 X13) /\ ((nonreflexive T_0 X13) /\ ((scream T_0 X13) /\ (of T_0 X13 X12))))))))))))))))))))))) (of T_0 T_7 T_6) (scream T_0 T_7) (nonreflexive T_0 T_7) (present T_0 T_7) (patient T_0 T_7 T_5) (agent T_0 T_7 T_1) (event T_0 T_7) (revenge T_0 T_6) (cry T_0 T_5) (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (group T_0 T_4) (six T_0 T_4) (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (cannon T_0 T_3) (of T_0 T_3 T_2) (man T_0 T_2) (male T_0 T_2) (male T_0 T_1) ### NotExists 23 % 1.65/1.90 25. (-. (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 X9 T_2) /\ ((cannon T_0 X9) /\ ((All X14, ((member T_0 X14 X10) => (Ex X15, ((event T_0 X15) /\ ((agent T_0 X15 T_2) /\ ((patient T_0 X15 X14) /\ ((present T_0 X15) /\ ((nonreflexive T_0 X15) /\ ((fire T_0 X15) /\ (from_loc T_0 X15 X9)))))))))) /\ ((six T_0 X10) /\ ((group T_0 X10) /\ ((All X16, ((member T_0 X16 X10) => (shot T_0 X16))) /\ ((cry T_0 X11) /\ ((revenge T_0 X12) /\ ((event T_0 X13) /\ ((agent T_0 X13 T_1) /\ ((patient T_0 X13 X11) /\ ((present T_0 X13) /\ ((nonreflexive T_0 X13) /\ ((scream T_0 X13) /\ (of T_0 X13 X12)))))))))))))))))))))))) (male T_0 T_1) (male T_0 T_2) (man T_0 T_2) (of T_0 T_3 T_2) (cannon T_0 T_3) (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (six T_0 T_4) (group T_0 T_4) (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (cry T_0 T_5) (revenge T_0 T_6) (event T_0 T_7) (agent T_0 T_7 T_1) (patient T_0 T_7 T_5) (present T_0 T_7) (nonreflexive T_0 T_7) (scream T_0 T_7) (of T_0 T_7 T_6) ### NotExists 24 % 1.65/1.90 26. (-. (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male T_0 T_1) /\ ((male T_0 X8) /\ ((man T_0 X8) /\ ((of T_0 X9 X8) /\ ((cannon T_0 X9) /\ ((All X14, ((member T_0 X14 X10) => (Ex X15, ((event T_0 X15) /\ ((agent T_0 X15 X8) /\ ((patient T_0 X15 X14) /\ ((present T_0 X15) /\ ((nonreflexive T_0 X15) /\ ((fire T_0 X15) /\ (from_loc T_0 X15 X9)))))))))) /\ ((six T_0 X10) /\ ((group T_0 X10) /\ ((All X16, ((member T_0 X16 X10) => (shot T_0 X16))) /\ ((cry T_0 X11) /\ ((revenge T_0 X12) /\ ((event T_0 X13) /\ ((agent T_0 X13 T_1) /\ ((patient T_0 X13 X11) /\ ((present T_0 X13) /\ ((nonreflexive T_0 X13) /\ ((scream T_0 X13) /\ (of T_0 X13 X12))))))))))))))))))))))))) (of T_0 T_7 T_6) (scream T_0 T_7) (nonreflexive T_0 T_7) (present T_0 T_7) (patient T_0 T_7 T_5) (agent T_0 T_7 T_1) (event T_0 T_7) (revenge T_0 T_6) (cry T_0 T_5) (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (group T_0 T_4) (six T_0 T_4) (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (cannon T_0 T_3) (of T_0 T_3 T_2) (man T_0 T_2) (male T_0 T_2) (male T_0 T_1) ### NotExists 25 % 1.65/1.90 27. (-. (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male T_0 X7) /\ ((male T_0 X8) /\ ((man T_0 X8) /\ ((of T_0 X9 X8) /\ ((cannon T_0 X9) /\ ((All X14, ((member T_0 X14 X10) => (Ex X15, ((event T_0 X15) /\ ((agent T_0 X15 X8) /\ ((patient T_0 X15 X14) /\ ((present T_0 X15) /\ ((nonreflexive T_0 X15) /\ ((fire T_0 X15) /\ (from_loc T_0 X15 X9)))))))))) /\ ((six T_0 X10) /\ ((group T_0 X10) /\ ((All X16, ((member T_0 X16 X10) => (shot T_0 X16))) /\ ((cry T_0 X11) /\ ((revenge T_0 X12) /\ ((event T_0 X13) /\ ((agent T_0 X13 X7) /\ ((patient T_0 X13 X11) /\ ((present T_0 X13) /\ ((nonreflexive T_0 X13) /\ ((scream T_0 X13) /\ (of T_0 X13 X12)))))))))))))))))))))))))) (male T_0 T_1) (male T_0 T_2) (man T_0 T_2) (of T_0 T_3 T_2) (cannon T_0 T_3) (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (six T_0 T_4) (group T_0 T_4) (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (cry T_0 T_5) (revenge T_0 T_6) (event T_0 T_7) (agent T_0 T_7 T_1) (patient T_0 T_7 T_5) (present T_0 T_7) (nonreflexive T_0 T_7) (scream T_0 T_7) (of T_0 T_7 T_6) ### NotExists 26 % 1.65/1.90 28. (-. ((actual_world T_0) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male T_0 X7) /\ ((male T_0 X8) /\ ((man T_0 X8) /\ ((of T_0 X9 X8) /\ ((cannon T_0 X9) /\ ((All X14, ((member T_0 X14 X10) => (Ex X15, ((event T_0 X15) /\ ((agent T_0 X15 X8) /\ ((patient T_0 X15 X14) /\ ((present T_0 X15) /\ ((nonreflexive T_0 X15) /\ ((fire T_0 X15) /\ (from_loc T_0 X15 X9)))))))))) /\ ((six T_0 X10) /\ ((group T_0 X10) /\ ((All X16, ((member T_0 X16 X10) => (shot T_0 X16))) /\ ((cry T_0 X11) /\ ((revenge T_0 X12) /\ ((event T_0 X13) /\ ((agent T_0 X13 X7) /\ ((patient T_0 X13 X11) /\ ((present T_0 X13) /\ ((nonreflexive T_0 X13) /\ ((scream T_0 X13) /\ (of T_0 X13 X12))))))))))))))))))))))))))) (of T_0 T_7 T_6) (scream T_0 T_7) (nonreflexive T_0 T_7) (present T_0 T_7) (patient T_0 T_7 T_5) (agent T_0 T_7 T_1) (event T_0 T_7) (revenge T_0 T_6) (cry T_0 T_5) (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (group T_0 T_4) (six T_0 T_4) (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (cannon T_0 T_3) (of T_0 T_3 T_2) (man T_0 T_2) (male T_0 T_2) (male T_0 T_1) (actual_world T_0) ### NotAnd 1 27 % 1.65/1.90 29. (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) (actual_world T_0) (male T_0 T_1) (male T_0 T_2) (man T_0 T_2) (of T_0 T_3 T_2) (cannon T_0 T_3) (All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) (six T_0 T_4) (group T_0 T_4) (All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) (cry T_0 T_5) (revenge T_0 T_6) (event T_0 T_7) (agent T_0 T_7 T_1) (patient T_0 T_7 T_5) (present T_0 T_7) (nonreflexive T_0 T_7) (scream T_0 T_7) (of T_0 T_7 T_6) ### NotExists 28 % 1.65/1.90 30. ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 T_3 T_2) /\ ((cannon T_0 T_3) /\ ((All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) /\ ((six T_0 T_4) /\ ((group T_0 T_4) /\ ((All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) /\ ((revenge T_0 T_6) /\ ((cry T_0 T_5) /\ ((event T_0 T_7) /\ ((agent T_0 T_7 T_1) /\ ((patient T_0 T_7 T_5) /\ ((present T_0 T_7) /\ ((nonreflexive T_0 T_7) /\ ((scream T_0 T_7) /\ (of T_0 T_7 T_6)))))))))))))))))) (actual_world T_0) (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) ### ConjTree 29 % 1.65/1.90 31. (Ex X2, ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 T_3 T_2) /\ ((cannon T_0 T_3) /\ ((All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) /\ ((six T_0 T_4) /\ ((group T_0 T_4) /\ ((All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) /\ ((revenge T_0 T_6) /\ ((cry T_0 T_5) /\ ((event T_0 X2) /\ ((agent T_0 X2 T_1) /\ ((patient T_0 X2 T_5) /\ ((present T_0 X2) /\ ((nonreflexive T_0 X2) /\ ((scream T_0 X2) /\ (of T_0 X2 T_6))))))))))))))))))) (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) (actual_world T_0) ### Exists 30 % 1.73/1.91 32. (Ex X1, (Ex X2, ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 T_3 T_2) /\ ((cannon T_0 T_3) /\ ((All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) /\ ((six T_0 T_4) /\ ((group T_0 T_4) /\ ((All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) /\ ((revenge T_0 T_6) /\ ((cry T_0 X1) /\ ((event T_0 X2) /\ ((agent T_0 X2 T_1) /\ ((patient T_0 X2 X1) /\ ((present T_0 X2) /\ ((nonreflexive T_0 X2) /\ ((scream T_0 X2) /\ (of T_0 X2 T_6)))))))))))))))))))) (actual_world T_0) (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) ### Exists 31 % 1.73/1.91 33. (Ex Z, (Ex X1, (Ex X2, ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 T_3 T_2) /\ ((cannon T_0 T_3) /\ ((All X3, ((member T_0 X3 T_4) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) /\ ((six T_0 T_4) /\ ((group T_0 T_4) /\ ((All X5, ((member T_0 X5 T_4) => (shot T_0 X5))) /\ ((revenge T_0 Z) /\ ((cry T_0 X1) /\ ((event T_0 X2) /\ ((agent T_0 X2 T_1) /\ ((patient T_0 X2 X1) /\ ((present T_0 X2) /\ ((nonreflexive T_0 X2) /\ ((scream T_0 X2) /\ (of T_0 X2 Z))))))))))))))))))))) (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) (actual_world T_0) ### Exists 32 % 1.73/1.91 34. (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 T_3 T_2) /\ ((cannon T_0 T_3) /\ ((All X3, ((member T_0 X3 Y) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 T_3)))))))))) /\ ((six T_0 Y) /\ ((group T_0 Y) /\ ((All X5, ((member T_0 X5 Y) => (shot T_0 X5))) /\ ((revenge T_0 Z) /\ ((cry T_0 X1) /\ ((event T_0 X2) /\ ((agent T_0 X2 T_1) /\ ((patient T_0 X2 X1) /\ ((present T_0 X2) /\ ((nonreflexive T_0 X2) /\ ((scream T_0 X2) /\ (of T_0 X2 Z)))))))))))))))))))))) (actual_world T_0) (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) ### Exists 33 % 1.73/1.91 35. (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male T_0 T_1) /\ ((male T_0 T_2) /\ ((man T_0 T_2) /\ ((of T_0 X T_2) /\ ((cannon T_0 X) /\ ((All X3, ((member T_0 X3 Y) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 T_2) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 X)))))))))) /\ ((six T_0 Y) /\ ((group T_0 Y) /\ ((All X5, ((member T_0 X5 Y) => (shot T_0 X5))) /\ ((revenge T_0 Z) /\ ((cry T_0 X1) /\ ((event T_0 X2) /\ ((agent T_0 X2 T_1) /\ ((patient T_0 X2 X1) /\ ((present T_0 X2) /\ ((nonreflexive T_0 X2) /\ ((scream T_0 X2) /\ (of T_0 X2 Z))))))))))))))))))))))) (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) (actual_world T_0) ### Exists 34 % 1.73/1.91 36. (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male T_0 T_1) /\ ((male T_0 W) /\ ((man T_0 W) /\ ((of T_0 X W) /\ ((cannon T_0 X) /\ ((All X3, ((member T_0 X3 Y) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 W) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 X)))))))))) /\ ((six T_0 Y) /\ ((group T_0 Y) /\ ((All X5, ((member T_0 X5 Y) => (shot T_0 X5))) /\ ((revenge T_0 Z) /\ ((cry T_0 X1) /\ ((event T_0 X2) /\ ((agent T_0 X2 T_1) /\ ((patient T_0 X2 X1) /\ ((present T_0 X2) /\ ((nonreflexive T_0 X2) /\ ((scream T_0 X2) /\ (of T_0 X2 Z)))))))))))))))))))))))) (actual_world T_0) (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) ### Exists 35 % 1.73/1.91 37. (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male T_0 V) /\ ((male T_0 W) /\ ((man T_0 W) /\ ((of T_0 X W) /\ ((cannon T_0 X) /\ ((All X3, ((member T_0 X3 Y) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 W) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 X)))))))))) /\ ((six T_0 Y) /\ ((group T_0 Y) /\ ((All X5, ((member T_0 X5 Y) => (shot T_0 X5))) /\ ((revenge T_0 Z) /\ ((cry T_0 X1) /\ ((event T_0 X2) /\ ((agent T_0 X2 V) /\ ((patient T_0 X2 X1) /\ ((present T_0 X2) /\ ((nonreflexive T_0 X2) /\ ((scream T_0 X2) /\ (of T_0 X2 Z))))))))))))))))))))))))) (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) (actual_world T_0) ### Exists 36 % 1.73/1.92 38. ((actual_world T_0) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male T_0 V) /\ ((male T_0 W) /\ ((man T_0 W) /\ ((of T_0 X W) /\ ((cannon T_0 X) /\ ((All X3, ((member T_0 X3 Y) => (Ex X4, ((event T_0 X4) /\ ((agent T_0 X4 W) /\ ((patient T_0 X4 X3) /\ ((present T_0 X4) /\ ((nonreflexive T_0 X4) /\ ((fire T_0 X4) /\ (from_loc T_0 X4 X)))))))))) /\ ((six T_0 Y) /\ ((group T_0 Y) /\ ((All X5, ((member T_0 X5 Y) => (shot T_0 X5))) /\ ((revenge T_0 Z) /\ ((cry T_0 X1) /\ ((event T_0 X2) /\ ((agent T_0 X2 V) /\ ((patient T_0 X2 X1) /\ ((present T_0 X2) /\ ((nonreflexive T_0 X2) /\ ((scream T_0 X2) /\ (of T_0 X2 Z)))))))))))))))))))))))))) (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) ### And 37 % 1.73/1.92 39. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z))))))))))))))))))))))))))) (-. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) ### Exists 38 % 1.73/1.92 40. (-. ((Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z))))))))))))))))))))))))))) => (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12))))))))))))))))))))))))))))) ### NotImply 39 % 1.73/1.92 41. (actual_world T_8) (-. (actual_world T_8)) ### Axiom % 1.73/1.92 42. (male T_8 T_9) (-. (male T_8 T_9)) ### Axiom % 1.73/1.92 43. (male T_8 T_10) (-. (male T_8 T_10)) ### Axiom % 1.73/1.92 44. (man T_8 T_10) (-. (man T_8 T_10)) ### Axiom % 1.73/1.92 45. (of T_8 T_11 T_10) (-. (of T_8 T_11 T_10)) ### Axiom % 1.73/1.92 46. (cannon T_8 T_11) (-. (cannon T_8 T_11)) ### Axiom % 1.73/1.92 47. (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (-. (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11))))))))))) ### Axiom % 1.73/1.92 48. (six T_8 T_12) (-. (six T_8 T_12)) ### Axiom % 1.73/1.92 49. (group T_8 T_12) (-. (group T_8 T_12)) ### Axiom % 1.73/1.92 50. (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (-. (All X16, ((member T_8 X16 T_12) => (shot T_8 X16)))) ### Axiom % 1.73/1.92 51. (revenge T_8 T_13) (-. (revenge T_8 T_13)) ### Axiom % 1.73/1.92 52. (cry T_8 T_14) (-. (cry T_8 T_14)) ### Axiom % 1.73/1.92 53. (event T_8 T_15) (-. (event T_8 T_15)) ### Axiom % 1.73/1.92 54. (agent T_8 T_15 T_9) (-. (agent T_8 T_15 T_9)) ### Axiom % 1.73/1.92 55. (patient T_8 T_15 T_14) (-. (patient T_8 T_15 T_14)) ### Axiom % 1.73/1.92 56. (present T_8 T_15) (-. (present T_8 T_15)) ### Axiom % 1.73/1.92 57. (nonreflexive T_8 T_15) (-. (nonreflexive T_8 T_15)) ### Axiom % 1.73/1.92 58. (scream T_8 T_15) (-. (scream T_8 T_15)) ### Axiom % 1.73/1.92 59. (of T_8 T_15 T_13) (-. (of T_8 T_15 T_13)) ### Axiom % 1.73/1.92 60. (-. ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 T_11 T_10) /\ ((cannon T_8 T_11) /\ ((All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) /\ ((six T_8 T_12) /\ ((group T_8 T_12) /\ ((All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) /\ ((revenge T_8 T_13) /\ ((cry T_8 T_14) /\ ((event T_8 T_15) /\ ((agent T_8 T_15 T_9) /\ ((patient T_8 T_15 T_14) /\ ((present T_8 T_15) /\ ((nonreflexive T_8 T_15) /\ ((scream T_8 T_15) /\ (of T_8 T_15 T_13))))))))))))))))))) (of T_8 T_15 T_13) (scream T_8 T_15) (nonreflexive T_8 T_15) (present T_8 T_15) (patient T_8 T_15 T_14) (agent T_8 T_15 T_9) (event T_8 T_15) (cry T_8 T_14) (revenge T_8 T_13) (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (group T_8 T_12) (six T_8 T_12) (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (cannon T_8 T_11) (of T_8 T_11 T_10) (man T_8 T_10) (male T_8 T_10) (male T_8 T_9) ### DisjTree 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 % 1.73/1.92 61. (-. (Ex X2, ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 T_11 T_10) /\ ((cannon T_8 T_11) /\ ((All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) /\ ((six T_8 T_12) /\ ((group T_8 T_12) /\ ((All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) /\ ((revenge T_8 T_13) /\ ((cry T_8 T_14) /\ ((event T_8 X2) /\ ((agent T_8 X2 T_9) /\ ((patient T_8 X2 T_14) /\ ((present T_8 X2) /\ ((nonreflexive T_8 X2) /\ ((scream T_8 X2) /\ (of T_8 X2 T_13)))))))))))))))))))) (male T_8 T_9) (male T_8 T_10) (man T_8 T_10) (of T_8 T_11 T_10) (cannon T_8 T_11) (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (six T_8 T_12) (group T_8 T_12) (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (revenge T_8 T_13) (cry T_8 T_14) (event T_8 T_15) (agent T_8 T_15 T_9) (patient T_8 T_15 T_14) (present T_8 T_15) (nonreflexive T_8 T_15) (scream T_8 T_15) (of T_8 T_15 T_13) ### NotExists 60 % 1.73/1.92 62. (-. (Ex X1, (Ex X2, ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 T_11 T_10) /\ ((cannon T_8 T_11) /\ ((All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) /\ ((six T_8 T_12) /\ ((group T_8 T_12) /\ ((All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) /\ ((revenge T_8 T_13) /\ ((cry T_8 X1) /\ ((event T_8 X2) /\ ((agent T_8 X2 T_9) /\ ((patient T_8 X2 X1) /\ ((present T_8 X2) /\ ((nonreflexive T_8 X2) /\ ((scream T_8 X2) /\ (of T_8 X2 T_13))))))))))))))))))))) (of T_8 T_15 T_13) (scream T_8 T_15) (nonreflexive T_8 T_15) (present T_8 T_15) (patient T_8 T_15 T_14) (agent T_8 T_15 T_9) (event T_8 T_15) (cry T_8 T_14) (revenge T_8 T_13) (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (group T_8 T_12) (six T_8 T_12) (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (cannon T_8 T_11) (of T_8 T_11 T_10) (man T_8 T_10) (male T_8 T_10) (male T_8 T_9) ### NotExists 61 % 1.73/1.92 63. (-. (Ex Z, (Ex X1, (Ex X2, ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 T_11 T_10) /\ ((cannon T_8 T_11) /\ ((All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) /\ ((six T_8 T_12) /\ ((group T_8 T_12) /\ ((All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) /\ ((revenge T_8 Z) /\ ((cry T_8 X1) /\ ((event T_8 X2) /\ ((agent T_8 X2 T_9) /\ ((patient T_8 X2 X1) /\ ((present T_8 X2) /\ ((nonreflexive T_8 X2) /\ ((scream T_8 X2) /\ (of T_8 X2 Z)))))))))))))))))))))) (male T_8 T_9) (male T_8 T_10) (man T_8 T_10) (of T_8 T_11 T_10) (cannon T_8 T_11) (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (six T_8 T_12) (group T_8 T_12) (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (revenge T_8 T_13) (cry T_8 T_14) (event T_8 T_15) (agent T_8 T_15 T_9) (patient T_8 T_15 T_14) (present T_8 T_15) (nonreflexive T_8 T_15) (scream T_8 T_15) (of T_8 T_15 T_13) ### NotExists 62 % 1.73/1.92 64. (-. (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 T_11 T_10) /\ ((cannon T_8 T_11) /\ ((All X3, ((member T_8 X3 Y) => (Ex X4, ((event T_8 X4) /\ ((agent T_8 X4 T_10) /\ ((patient T_8 X4 X3) /\ ((present T_8 X4) /\ ((nonreflexive T_8 X4) /\ ((fire T_8 X4) /\ (from_loc T_8 X4 T_11)))))))))) /\ ((six T_8 Y) /\ ((group T_8 Y) /\ ((All X5, ((member T_8 X5 Y) => (shot T_8 X5))) /\ ((revenge T_8 Z) /\ ((cry T_8 X1) /\ ((event T_8 X2) /\ ((agent T_8 X2 T_9) /\ ((patient T_8 X2 X1) /\ ((present T_8 X2) /\ ((nonreflexive T_8 X2) /\ ((scream T_8 X2) /\ (of T_8 X2 Z))))))))))))))))))))))) (of T_8 T_15 T_13) (scream T_8 T_15) (nonreflexive T_8 T_15) (present T_8 T_15) (patient T_8 T_15 T_14) (agent T_8 T_15 T_9) (event T_8 T_15) (cry T_8 T_14) (revenge T_8 T_13) (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (group T_8 T_12) (six T_8 T_12) (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (cannon T_8 T_11) (of T_8 T_11 T_10) (man T_8 T_10) (male T_8 T_10) (male T_8 T_9) ### NotExists 63 % 1.73/1.92 65. (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 X T_10) /\ ((cannon T_8 X) /\ ((All X3, ((member T_8 X3 Y) => (Ex X4, ((event T_8 X4) /\ ((agent T_8 X4 T_10) /\ ((patient T_8 X4 X3) /\ ((present T_8 X4) /\ ((nonreflexive T_8 X4) /\ ((fire T_8 X4) /\ (from_loc T_8 X4 X)))))))))) /\ ((six T_8 Y) /\ ((group T_8 Y) /\ ((All X5, ((member T_8 X5 Y) => (shot T_8 X5))) /\ ((revenge T_8 Z) /\ ((cry T_8 X1) /\ ((event T_8 X2) /\ ((agent T_8 X2 T_9) /\ ((patient T_8 X2 X1) /\ ((present T_8 X2) /\ ((nonreflexive T_8 X2) /\ ((scream T_8 X2) /\ (of T_8 X2 Z)))))))))))))))))))))))) (male T_8 T_9) (male T_8 T_10) (man T_8 T_10) (of T_8 T_11 T_10) (cannon T_8 T_11) (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (six T_8 T_12) (group T_8 T_12) (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (revenge T_8 T_13) (cry T_8 T_14) (event T_8 T_15) (agent T_8 T_15 T_9) (patient T_8 T_15 T_14) (present T_8 T_15) (nonreflexive T_8 T_15) (scream T_8 T_15) (of T_8 T_15 T_13) ### NotExists 64 % 1.73/1.92 66. (-. (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male T_8 T_9) /\ ((male T_8 W) /\ ((man T_8 W) /\ ((of T_8 X W) /\ ((cannon T_8 X) /\ ((All X3, ((member T_8 X3 Y) => (Ex X4, ((event T_8 X4) /\ ((agent T_8 X4 W) /\ ((patient T_8 X4 X3) /\ ((present T_8 X4) /\ ((nonreflexive T_8 X4) /\ ((fire T_8 X4) /\ (from_loc T_8 X4 X)))))))))) /\ ((six T_8 Y) /\ ((group T_8 Y) /\ ((All X5, ((member T_8 X5 Y) => (shot T_8 X5))) /\ ((revenge T_8 Z) /\ ((cry T_8 X1) /\ ((event T_8 X2) /\ ((agent T_8 X2 T_9) /\ ((patient T_8 X2 X1) /\ ((present T_8 X2) /\ ((nonreflexive T_8 X2) /\ ((scream T_8 X2) /\ (of T_8 X2 Z))))))))))))))))))))))))) (of T_8 T_15 T_13) (scream T_8 T_15) (nonreflexive T_8 T_15) (present T_8 T_15) (patient T_8 T_15 T_14) (agent T_8 T_15 T_9) (event T_8 T_15) (cry T_8 T_14) (revenge T_8 T_13) (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (group T_8 T_12) (six T_8 T_12) (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (cannon T_8 T_11) (of T_8 T_11 T_10) (man T_8 T_10) (male T_8 T_10) (male T_8 T_9) ### NotExists 65 % 1.73/1.92 67. (-. (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male T_8 V) /\ ((male T_8 W) /\ ((man T_8 W) /\ ((of T_8 X W) /\ ((cannon T_8 X) /\ ((All X3, ((member T_8 X3 Y) => (Ex X4, ((event T_8 X4) /\ ((agent T_8 X4 W) /\ ((patient T_8 X4 X3) /\ ((present T_8 X4) /\ ((nonreflexive T_8 X4) /\ ((fire T_8 X4) /\ (from_loc T_8 X4 X)))))))))) /\ ((six T_8 Y) /\ ((group T_8 Y) /\ ((All X5, ((member T_8 X5 Y) => (shot T_8 X5))) /\ ((revenge T_8 Z) /\ ((cry T_8 X1) /\ ((event T_8 X2) /\ ((agent T_8 X2 V) /\ ((patient T_8 X2 X1) /\ ((present T_8 X2) /\ ((nonreflexive T_8 X2) /\ ((scream T_8 X2) /\ (of T_8 X2 Z)))))))))))))))))))))))))) (male T_8 T_9) (male T_8 T_10) (man T_8 T_10) (of T_8 T_11 T_10) (cannon T_8 T_11) (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (six T_8 T_12) (group T_8 T_12) (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (revenge T_8 T_13) (cry T_8 T_14) (event T_8 T_15) (agent T_8 T_15 T_9) (patient T_8 T_15 T_14) (present T_8 T_15) (nonreflexive T_8 T_15) (scream T_8 T_15) (of T_8 T_15 T_13) ### NotExists 66 % 1.73/1.92 68. (-. ((actual_world T_8) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male T_8 V) /\ ((male T_8 W) /\ ((man T_8 W) /\ ((of T_8 X W) /\ ((cannon T_8 X) /\ ((All X3, ((member T_8 X3 Y) => (Ex X4, ((event T_8 X4) /\ ((agent T_8 X4 W) /\ ((patient T_8 X4 X3) /\ ((present T_8 X4) /\ ((nonreflexive T_8 X4) /\ ((fire T_8 X4) /\ (from_loc T_8 X4 X)))))))))) /\ ((six T_8 Y) /\ ((group T_8 Y) /\ ((All X5, ((member T_8 X5 Y) => (shot T_8 X5))) /\ ((revenge T_8 Z) /\ ((cry T_8 X1) /\ ((event T_8 X2) /\ ((agent T_8 X2 V) /\ ((patient T_8 X2 X1) /\ ((present T_8 X2) /\ ((nonreflexive T_8 X2) /\ ((scream T_8 X2) /\ (of T_8 X2 Z))))))))))))))))))))))))))) (of T_8 T_15 T_13) (scream T_8 T_15) (nonreflexive T_8 T_15) (present T_8 T_15) (patient T_8 T_15 T_14) (agent T_8 T_15 T_9) (event T_8 T_15) (cry T_8 T_14) (revenge T_8 T_13) (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (group T_8 T_12) (six T_8 T_12) (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (cannon T_8 T_11) (of T_8 T_11 T_10) (man T_8 T_10) (male T_8 T_10) (male T_8 T_9) (actual_world T_8) ### NotAnd 41 67 % 1.73/1.93 69. (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) (actual_world T_8) (male T_8 T_9) (male T_8 T_10) (man T_8 T_10) (of T_8 T_11 T_10) (cannon T_8 T_11) (All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) (six T_8 T_12) (group T_8 T_12) (All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) (revenge T_8 T_13) (cry T_8 T_14) (event T_8 T_15) (agent T_8 T_15 T_9) (patient T_8 T_15 T_14) (present T_8 T_15) (nonreflexive T_8 T_15) (scream T_8 T_15) (of T_8 T_15 T_13) ### NotExists 68 % 1.73/1.93 70. ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 T_11 T_10) /\ ((cannon T_8 T_11) /\ ((All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) /\ ((six T_8 T_12) /\ ((group T_8 T_12) /\ ((All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) /\ ((cry T_8 T_14) /\ ((revenge T_8 T_13) /\ ((event T_8 T_15) /\ ((agent T_8 T_15 T_9) /\ ((patient T_8 T_15 T_14) /\ ((present T_8 T_15) /\ ((nonreflexive T_8 T_15) /\ ((scream T_8 T_15) /\ (of T_8 T_15 T_13)))))))))))))))))) (actual_world T_8) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) ### ConjTree 69 % 1.73/1.93 71. (Ex X13, ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 T_11 T_10) /\ ((cannon T_8 T_11) /\ ((All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) /\ ((six T_8 T_12) /\ ((group T_8 T_12) /\ ((All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) /\ ((cry T_8 T_14) /\ ((revenge T_8 T_13) /\ ((event T_8 X13) /\ ((agent T_8 X13 T_9) /\ ((patient T_8 X13 T_14) /\ ((present T_8 X13) /\ ((nonreflexive T_8 X13) /\ ((scream T_8 X13) /\ (of T_8 X13 T_13))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) (actual_world T_8) ### Exists 70 % 1.73/1.93 72. (Ex X12, (Ex X13, ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 T_11 T_10) /\ ((cannon T_8 T_11) /\ ((All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) /\ ((six T_8 T_12) /\ ((group T_8 T_12) /\ ((All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) /\ ((cry T_8 T_14) /\ ((revenge T_8 X12) /\ ((event T_8 X13) /\ ((agent T_8 X13 T_9) /\ ((patient T_8 X13 T_14) /\ ((present T_8 X13) /\ ((nonreflexive T_8 X13) /\ ((scream T_8 X13) /\ (of T_8 X13 X12)))))))))))))))))))) (actual_world T_8) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) ### Exists 71 % 1.73/1.93 73. (Ex X11, (Ex X12, (Ex X13, ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 T_11 T_10) /\ ((cannon T_8 T_11) /\ ((All X14, ((member T_8 X14 T_12) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) /\ ((six T_8 T_12) /\ ((group T_8 T_12) /\ ((All X16, ((member T_8 X16 T_12) => (shot T_8 X16))) /\ ((cry T_8 X11) /\ ((revenge T_8 X12) /\ ((event T_8 X13) /\ ((agent T_8 X13 T_9) /\ ((patient T_8 X13 X11) /\ ((present T_8 X13) /\ ((nonreflexive T_8 X13) /\ ((scream T_8 X13) /\ (of T_8 X13 X12))))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) (actual_world T_8) ### Exists 72 % 1.73/1.93 74. (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 T_11 T_10) /\ ((cannon T_8 T_11) /\ ((All X14, ((member T_8 X14 X10) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 T_11)))))))))) /\ ((six T_8 X10) /\ ((group T_8 X10) /\ ((All X16, ((member T_8 X16 X10) => (shot T_8 X16))) /\ ((cry T_8 X11) /\ ((revenge T_8 X12) /\ ((event T_8 X13) /\ ((agent T_8 X13 T_9) /\ ((patient T_8 X13 X11) /\ ((present T_8 X13) /\ ((nonreflexive T_8 X13) /\ ((scream T_8 X13) /\ (of T_8 X13 X12)))))))))))))))))))))) (actual_world T_8) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) ### Exists 73 % 1.73/1.93 75. (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male T_8 T_9) /\ ((male T_8 T_10) /\ ((man T_8 T_10) /\ ((of T_8 X9 T_10) /\ ((cannon T_8 X9) /\ ((All X14, ((member T_8 X14 X10) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 T_10) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 X9)))))))))) /\ ((six T_8 X10) /\ ((group T_8 X10) /\ ((All X16, ((member T_8 X16 X10) => (shot T_8 X16))) /\ ((cry T_8 X11) /\ ((revenge T_8 X12) /\ ((event T_8 X13) /\ ((agent T_8 X13 T_9) /\ ((patient T_8 X13 X11) /\ ((present T_8 X13) /\ ((nonreflexive T_8 X13) /\ ((scream T_8 X13) /\ (of T_8 X13 X12))))))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) (actual_world T_8) ### Exists 74 % 1.73/1.93 76. (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male T_8 T_9) /\ ((male T_8 X8) /\ ((man T_8 X8) /\ ((of T_8 X9 X8) /\ ((cannon T_8 X9) /\ ((All X14, ((member T_8 X14 X10) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 X8) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 X9)))))))))) /\ ((six T_8 X10) /\ ((group T_8 X10) /\ ((All X16, ((member T_8 X16 X10) => (shot T_8 X16))) /\ ((cry T_8 X11) /\ ((revenge T_8 X12) /\ ((event T_8 X13) /\ ((agent T_8 X13 T_9) /\ ((patient T_8 X13 X11) /\ ((present T_8 X13) /\ ((nonreflexive T_8 X13) /\ ((scream T_8 X13) /\ (of T_8 X13 X12)))))))))))))))))))))))) (actual_world T_8) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) ### Exists 75 % 1.73/1.93 77. (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male T_8 X7) /\ ((male T_8 X8) /\ ((man T_8 X8) /\ ((of T_8 X9 X8) /\ ((cannon T_8 X9) /\ ((All X14, ((member T_8 X14 X10) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 X8) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 X9)))))))))) /\ ((six T_8 X10) /\ ((group T_8 X10) /\ ((All X16, ((member T_8 X16 X10) => (shot T_8 X16))) /\ ((cry T_8 X11) /\ ((revenge T_8 X12) /\ ((event T_8 X13) /\ ((agent T_8 X13 X7) /\ ((patient T_8 X13 X11) /\ ((present T_8 X13) /\ ((nonreflexive T_8 X13) /\ ((scream T_8 X13) /\ (of T_8 X13 X12))))))))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) (actual_world T_8) ### Exists 76 % 1.73/1.93 78. ((actual_world T_8) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male T_8 X7) /\ ((male T_8 X8) /\ ((man T_8 X8) /\ ((of T_8 X9 X8) /\ ((cannon T_8 X9) /\ ((All X14, ((member T_8 X14 X10) => (Ex X15, ((event T_8 X15) /\ ((agent T_8 X15 X8) /\ ((patient T_8 X15 X14) /\ ((present T_8 X15) /\ ((nonreflexive T_8 X15) /\ ((fire T_8 X15) /\ (from_loc T_8 X15 X9)))))))))) /\ ((six T_8 X10) /\ ((group T_8 X10) /\ ((All X16, ((member T_8 X16 X10) => (shot T_8 X16))) /\ ((cry T_8 X11) /\ ((revenge T_8 X12) /\ ((event T_8 X13) /\ ((agent T_8 X13 X7) /\ ((patient T_8 X13 X11) /\ ((present T_8 X13) /\ ((nonreflexive T_8 X13) /\ ((scream T_8 X13) /\ (of T_8 X13 X12)))))))))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) ### And 77 % 1.73/1.93 79. (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12))))))))))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))) ### Exists 78 % 1.73/1.93 80. (-. ((Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12))))))))))))))))))))))))))) => (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z))))))))))))))))))))))))))))) ### NotImply 79 % 1.73/1.93 81. (-. (((Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z))))))))))))))))))))))))))) => (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) /\ ((Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12))))))))))))))))))))))))))) => (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))))) ### NotAnd 40 80 % 1.73/1.93 82. (-. (-. (-. (((Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z))))))))))))))))))))))))))) => (Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12)))))))))))))))))))))))))))) /\ ((Ex X6, ((actual_world X6) /\ (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, (Ex X13, ((male X6 X7) /\ ((male X6 X8) /\ ((man X6 X8) /\ ((of X6 X9 X8) /\ ((cannon X6 X9) /\ ((All X14, ((member X6 X14 X10) => (Ex X15, ((event X6 X15) /\ ((agent X6 X15 X8) /\ ((patient X6 X15 X14) /\ ((present X6 X15) /\ ((nonreflexive X6 X15) /\ ((fire X6 X15) /\ (from_loc X6 X15 X9)))))))))) /\ ((six X6 X10) /\ ((group X6 X10) /\ ((All X16, ((member X6 X16 X10) => (shot X6 X16))) /\ ((cry X6 X11) /\ ((revenge X6 X12) /\ ((event X6 X13) /\ ((agent X6 X13 X7) /\ ((patient X6 X13 X11) /\ ((present X6 X13) /\ ((nonreflexive X6 X13) /\ ((scream X6 X13) /\ (of X6 X13 X12))))))))))))))))))))))))))) => (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((male U V) /\ ((male U W) /\ ((man U W) /\ ((of U X W) /\ ((cannon U X) /\ ((All X3, ((member U X3 Y) => (Ex X4, ((event U X4) /\ ((agent U X4 W) /\ ((patient U X4 X3) /\ ((present U X4) /\ ((nonreflexive U X4) /\ ((fire U X4) /\ (from_loc U X4 X)))))))))) /\ ((six U Y) /\ ((group U Y) /\ ((All X5, ((member U X5 Y) => (shot U X5))) /\ ((revenge U Z) /\ ((cry U X1) /\ ((event U X2) /\ ((agent U X2 V) /\ ((patient U X2 X1) /\ ((present U X2) /\ ((nonreflexive U X2) /\ ((scream U X2) /\ (of U X2 Z)))))))))))))))))))))))))))))))) ### NotNot 81 % 1.73/1.93 % SZS output end Proof % 1.73/1.93 (* END-PROOF *) %------------------------------------------------------------------------------