%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NLP094+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 : n027.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:59 EDT 2022 % Result : Theorem 0.18s 0.47s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP094+1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n027.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 : Thu Jun 30 21:47:52 EDT 2022 % 0.12/0.34 % CPUTime : % 0.18/0.47 % SZS status Theorem % 0.18/0.47 (* PROOF-FOUND *) % 0.18/0.47 (* BEGIN-PROOF *) % 0.18/0.47 % SZS output start Proof % 0.18/0.47 1. (actual_world T_0) (-. (actual_world T_0)) ### Axiom % 0.18/0.47 2. (customer T_0 T_1) (-. (customer T_0 T_1)) ### Axiom % 0.18/0.47 3. (restaurant T_0 T_2) (-. (restaurant T_0 T_2)) ### Axiom % 0.18/0.47 4. (in T_0 T_1 T_2) (-. (in T_0 T_1 T_2)) ### Axiom % 0.18/0.47 5. (coffee T_0 T_3) (-. (coffee T_0 T_3)) ### Axiom % 0.18/0.47 6. (human_person T_0 T_4) (-. (human_person T_0 T_4)) ### Axiom % 0.18/0.47 7. (event T_0 T_5) (-. (event T_0 T_5)) ### Axiom % 0.18/0.47 8. (agent T_0 T_5 T_4) (-. (agent T_0 T_5 T_4)) ### Axiom % 0.18/0.47 9. (patient T_0 T_5 T_3) (-. (patient T_0 T_5 T_3)) ### Axiom % 0.18/0.47 10. (past T_0 T_5) (-. (past T_0 T_5)) ### Axiom % 0.18/0.47 11. (nonreflexive T_0 T_5) (-. (nonreflexive T_0 T_5)) ### Axiom % 0.18/0.47 12. (drink T_0 T_5) (-. (drink T_0 T_5)) ### Axiom % 0.18/0.47 13. (event T_0 T_6) (-. (event T_0 T_6)) ### Axiom % 0.18/0.47 14. (agent T_0 T_6 T_1) (-. (agent T_0 T_6 T_1)) ### Axiom % 0.18/0.47 15. (patient T_0 T_6 T_4) (-. (patient T_0 T_6 T_4)) ### Axiom % 0.18/0.47 16. (past T_0 T_6) (-. (past T_0 T_6)) ### Axiom % 0.18/0.47 17. (nonreflexive T_0 T_6) (-. (nonreflexive T_0 T_6)) ### Axiom % 0.18/0.47 18. (see T_0 T_6) (-. (see T_0 T_6)) ### Axiom % 0.18/0.47 19. (-. ((coffee T_0 T_3) /\ ((human_person T_0 T_4) /\ ((event T_0 T_5) /\ ((agent T_0 T_5 T_4) /\ ((patient T_0 T_5 T_3) /\ ((past T_0 T_5) /\ ((nonreflexive T_0 T_5) /\ ((drink T_0 T_5) /\ ((event T_0 T_6) /\ ((agent T_0 T_6 T_1) /\ ((patient T_0 T_6 T_4) /\ ((past T_0 T_6) /\ ((nonreflexive T_0 T_6) /\ (see T_0 T_6))))))))))))))) (see T_0 T_6) (nonreflexive T_0 T_6) (past T_0 T_6) (patient T_0 T_6 T_4) (agent T_0 T_6 T_1) (event T_0 T_6) (drink T_0 T_5) (nonreflexive T_0 T_5) (past T_0 T_5) (patient T_0 T_5 T_3) (agent T_0 T_5 T_4) (event T_0 T_5) (human_person T_0 T_4) (coffee T_0 T_3) ### DisjTree 5 6 7 8 9 10 11 12 13 14 15 16 17 18 % 0.18/0.47 20. (-. (Ex X8, ((coffee T_0 T_3) /\ ((human_person T_0 T_4) /\ ((event T_0 T_5) /\ ((agent T_0 T_5 T_4) /\ ((patient T_0 T_5 T_3) /\ ((past T_0 T_5) /\ ((nonreflexive T_0 T_5) /\ ((drink T_0 T_5) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 T_4) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8)))))))))))))))) (coffee T_0 T_3) (human_person T_0 T_4) (event T_0 T_5) (agent T_0 T_5 T_4) (patient T_0 T_5 T_3) (past T_0 T_5) (nonreflexive T_0 T_5) (drink T_0 T_5) (event T_0 T_6) (agent T_0 T_6 T_1) (patient T_0 T_6 T_4) (past T_0 T_6) (nonreflexive T_0 T_6) (see T_0 T_6) ### NotExists 19 % 0.18/0.47 21. (-. (Ex X7, (Ex X8, ((coffee T_0 T_3) /\ ((human_person T_0 T_4) /\ ((event T_0 X7) /\ ((agent T_0 X7 T_4) /\ ((patient T_0 X7 T_3) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 T_4) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))) (see T_0 T_6) (nonreflexive T_0 T_6) (past T_0 T_6) (patient T_0 T_6 T_4) (agent T_0 T_6 T_1) (event T_0 T_6) (drink T_0 T_5) (nonreflexive T_0 T_5) (past T_0 T_5) (patient T_0 T_5 T_3) (agent T_0 T_5 T_4) (event T_0 T_5) (human_person T_0 T_4) (coffee T_0 T_3) ### NotExists 20 % 0.18/0.47 22. (-. (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 T_3) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 T_3) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8)))))))))))))))))) (coffee T_0 T_3) (human_person T_0 T_4) (event T_0 T_5) (agent T_0 T_5 T_4) (patient T_0 T_5 T_3) (past T_0 T_5) (nonreflexive T_0 T_5) (drink T_0 T_5) (event T_0 T_6) (agent T_0 T_6 T_1) (patient T_0 T_6 T_4) (past T_0 T_6) (nonreflexive T_0 T_6) (see T_0 T_6) ### NotExists 21 % 0.18/0.47 23. (-. (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))) (see T_0 T_6) (nonreflexive T_0 T_6) (past T_0 T_6) (patient T_0 T_6 T_4) (agent T_0 T_6 T_1) (event T_0 T_6) (drink T_0 T_5) (nonreflexive T_0 T_5) (past T_0 T_5) (patient T_0 T_5 T_3) (agent T_0 T_5 T_4) (event T_0 T_5) (human_person T_0 T_4) (coffee T_0 T_3) ### NotExists 22 % 0.18/0.47 24. ((human_person T_0 T_4) /\ ((coffee T_0 T_3) /\ ((event T_0 T_5) /\ ((agent T_0 T_5 T_4) /\ ((patient T_0 T_5 T_3) /\ ((past T_0 T_5) /\ ((nonreflexive T_0 T_5) /\ ((drink T_0 T_5) /\ ((event T_0 T_6) /\ ((agent T_0 T_6 T_1) /\ ((patient T_0 T_6 T_4) /\ ((past T_0 T_6) /\ ((nonreflexive T_0 T_6) /\ (see T_0 T_6)))))))))))))) (-. (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))) ### ConjTree 23 % 0.18/0.47 25. (Ex X1, ((human_person T_0 T_4) /\ ((coffee T_0 T_3) /\ ((event T_0 T_5) /\ ((agent T_0 T_5 T_4) /\ ((patient T_0 T_5 T_3) /\ ((past T_0 T_5) /\ ((nonreflexive T_0 T_5) /\ ((drink T_0 T_5) /\ ((event T_0 X1) /\ ((agent T_0 X1 T_1) /\ ((patient T_0 X1 T_4) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1))))))))))))))) (-. (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))) ### Exists 24 % 0.18/0.47 26. (Ex Z, (Ex X1, ((human_person T_0 T_4) /\ ((coffee T_0 T_3) /\ ((event T_0 Z) /\ ((agent T_0 Z T_4) /\ ((patient T_0 Z T_3) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 T_1) /\ ((patient T_0 X1 T_4) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1)))))))))))))))) (-. (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))) ### Exists 25 % 0.18/0.47 27. (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 T_4) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z T_4) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 T_1) /\ ((patient T_0 X1 T_4) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1))))))))))))))))) (-. (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))) ### Exists 26 % 0.18/0.47 28. (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 X) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z X) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 T_1) /\ ((patient T_0 X1 X) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1)))))))))))))))))) (-. (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))) ### Exists 27 % 0.18/0.47 29. (((customer T_0 T_1) /\ ((restaurant T_0 T_2) /\ (in T_0 T_1 T_2))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 X) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z X) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 T_1) /\ ((patient T_0 X1 X) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1))))))))))))))))))) (-. (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))) (in T_0 T_1 T_2) (restaurant T_0 T_2) (customer T_0 T_1) ### DisjTree 2 3 4 28 % 0.18/0.49 30. (All W, (((customer T_0 T_1) /\ ((restaurant T_0 W) /\ (in T_0 T_1 W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 X) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z X) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 T_1) /\ ((patient T_0 X1 X) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1)))))))))))))))))))) (customer T_0 T_1) (restaurant T_0 T_2) (in T_0 T_1 T_2) (-. (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))) ### All 29 % 0.18/0.49 31. (All V, (All W, (((customer T_0 V) /\ ((restaurant T_0 W) /\ (in T_0 V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 X) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z X) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 V) /\ ((patient T_0 X1 X) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1))))))))))))))))))))) (-. (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))) (in T_0 T_1 T_2) (restaurant T_0 T_2) (customer T_0 T_1) ### All 30 % 0.18/0.49 32. (-. (((customer T_0 T_1) /\ ((restaurant T_0 T_2) /\ (in T_0 T_1 T_2))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8)))))))))))))))))))) (All V, (All W, (((customer T_0 V) /\ ((restaurant T_0 W) /\ (in T_0 V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 X) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z X) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 V) /\ ((patient T_0 X1 X) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1))))))))))))))))))))) ### ConjTree 31 % 0.18/0.49 33. (-. (All X4, (((customer T_0 T_1) /\ ((restaurant T_0 X4) /\ (in T_0 T_1 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 T_1) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))))) (All V, (All W, (((customer T_0 V) /\ ((restaurant T_0 W) /\ (in T_0 V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 X) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z X) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 V) /\ ((patient T_0 X1 X) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1))))))))))))))))))))) ### NotAllEx 32 % 0.18/0.49 34. (-. (All X3, (All X4, (((customer T_0 X3) /\ ((restaurant T_0 X4) /\ (in T_0 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 X3) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8)))))))))))))))))))))) (All V, (All W, (((customer T_0 V) /\ ((restaurant T_0 W) /\ (in T_0 V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 X) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z X) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 V) /\ ((patient T_0 X1 X) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1))))))))))))))))))))) ### NotAllEx 33 % 0.18/0.49 35. (-. ((actual_world T_0) /\ (All X3, (All X4, (((customer T_0 X3) /\ ((restaurant T_0 X4) /\ (in T_0 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_0 X5) /\ ((human_person T_0 X6) /\ ((event T_0 X7) /\ ((agent T_0 X7 X6) /\ ((patient T_0 X7 X5) /\ ((past T_0 X7) /\ ((nonreflexive T_0 X7) /\ ((drink T_0 X7) /\ ((event T_0 X8) /\ ((agent T_0 X8 X3) /\ ((patient T_0 X8 X6) /\ ((past T_0 X8) /\ ((nonreflexive T_0 X8) /\ (see T_0 X8))))))))))))))))))))))) (All V, (All W, (((customer T_0 V) /\ ((restaurant T_0 W) /\ (in T_0 V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 X) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z X) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 V) /\ ((patient T_0 X1 X) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1))))))))))))))))))))) (actual_world T_0) ### NotAnd 1 34 % 0.18/0.49 36. (-. (Ex X2, ((actual_world X2) /\ (All X3, (All X4, (((customer X2 X3) /\ ((restaurant X2 X4) /\ (in X2 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee X2 X5) /\ ((human_person X2 X6) /\ ((event X2 X7) /\ ((agent X2 X7 X6) /\ ((patient X2 X7 X5) /\ ((past X2 X7) /\ ((nonreflexive X2 X7) /\ ((drink X2 X7) /\ ((event X2 X8) /\ ((agent X2 X8 X3) /\ ((patient X2 X8 X6) /\ ((past X2 X8) /\ ((nonreflexive X2 X8) /\ (see X2 X8)))))))))))))))))))))))) (actual_world T_0) (All V, (All W, (((customer T_0 V) /\ ((restaurant T_0 W) /\ (in T_0 V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 X) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z X) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 V) /\ ((patient T_0 X1 X) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1))))))))))))))))))))) ### NotExists 35 % 0.18/0.49 37. ((actual_world T_0) /\ (All V, (All W, (((customer T_0 V) /\ ((restaurant T_0 W) /\ (in T_0 V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_0 X) /\ ((coffee T_0 Y) /\ ((event T_0 Z) /\ ((agent T_0 Z X) /\ ((patient T_0 Z Y) /\ ((past T_0 Z) /\ ((nonreflexive T_0 Z) /\ ((drink T_0 Z) /\ ((event T_0 X1) /\ ((agent T_0 X1 V) /\ ((patient T_0 X1 X) /\ ((past T_0 X1) /\ ((nonreflexive T_0 X1) /\ (see T_0 X1)))))))))))))))))))))) (-. (Ex X2, ((actual_world X2) /\ (All X3, (All X4, (((customer X2 X3) /\ ((restaurant X2 X4) /\ (in X2 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee X2 X5) /\ ((human_person X2 X6) /\ ((event X2 X7) /\ ((agent X2 X7 X6) /\ ((patient X2 X7 X5) /\ ((past X2 X7) /\ ((nonreflexive X2 X7) /\ ((drink X2 X7) /\ ((event X2 X8) /\ ((agent X2 X8 X3) /\ ((patient X2 X8 X6) /\ ((past X2 X8) /\ ((nonreflexive X2 X8) /\ (see X2 X8)))))))))))))))))))))))) ### And 36 % 0.18/0.49 38. (Ex U, ((actual_world U) /\ (All V, (All W, (((customer U V) /\ ((restaurant U W) /\ (in U V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person U X) /\ ((coffee U Y) /\ ((event U Z) /\ ((agent U Z X) /\ ((patient U Z Y) /\ ((past U Z) /\ ((nonreflexive U Z) /\ ((drink U Z) /\ ((event U X1) /\ ((agent U X1 V) /\ ((patient U X1 X) /\ ((past U X1) /\ ((nonreflexive U X1) /\ (see U X1))))))))))))))))))))))) (-. (Ex X2, ((actual_world X2) /\ (All X3, (All X4, (((customer X2 X3) /\ ((restaurant X2 X4) /\ (in X2 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee X2 X5) /\ ((human_person X2 X6) /\ ((event X2 X7) /\ ((agent X2 X7 X6) /\ ((patient X2 X7 X5) /\ ((past X2 X7) /\ ((nonreflexive X2 X7) /\ ((drink X2 X7) /\ ((event X2 X8) /\ ((agent X2 X8 X3) /\ ((patient X2 X8 X6) /\ ((past X2 X8) /\ ((nonreflexive X2 X8) /\ (see X2 X8)))))))))))))))))))))))) ### Exists 37 % 0.18/0.50 39. (-. ((Ex U, ((actual_world U) /\ (All V, (All W, (((customer U V) /\ ((restaurant U W) /\ (in U V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person U X) /\ ((coffee U Y) /\ ((event U Z) /\ ((agent U Z X) /\ ((patient U Z Y) /\ ((past U Z) /\ ((nonreflexive U Z) /\ ((drink U Z) /\ ((event U X1) /\ ((agent U X1 V) /\ ((patient U X1 X) /\ ((past U X1) /\ ((nonreflexive U X1) /\ (see U X1))))))))))))))))))))))) => (Ex X2, ((actual_world X2) /\ (All X3, (All X4, (((customer X2 X3) /\ ((restaurant X2 X4) /\ (in X2 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee X2 X5) /\ ((human_person X2 X6) /\ ((event X2 X7) /\ ((agent X2 X7 X6) /\ ((patient X2 X7 X5) /\ ((past X2 X7) /\ ((nonreflexive X2 X7) /\ ((drink X2 X7) /\ ((event X2 X8) /\ ((agent X2 X8 X3) /\ ((patient X2 X8 X6) /\ ((past X2 X8) /\ ((nonreflexive X2 X8) /\ (see X2 X8))))))))))))))))))))))))) ### NotImply 38 % 0.18/0.50 40. (actual_world T_7) (-. (actual_world T_7)) ### Axiom % 0.18/0.50 41. (customer T_7 T_8) (-. (customer T_7 T_8)) ### Axiom % 0.18/0.50 42. (restaurant T_7 T_9) (-. (restaurant T_7 T_9)) ### Axiom % 0.18/0.50 43. (in T_7 T_8 T_9) (-. (in T_7 T_8 T_9)) ### Axiom % 0.18/0.50 44. (human_person T_7 T_10) (-. (human_person T_7 T_10)) ### Axiom % 0.18/0.50 45. (coffee T_7 T_11) (-. (coffee T_7 T_11)) ### Axiom % 0.18/0.50 46. (event T_7 T_12) (-. (event T_7 T_12)) ### Axiom % 0.18/0.50 47. (agent T_7 T_12 T_10) (-. (agent T_7 T_12 T_10)) ### Axiom % 0.18/0.50 48. (patient T_7 T_12 T_11) (-. (patient T_7 T_12 T_11)) ### Axiom % 0.18/0.50 49. (past T_7 T_12) (-. (past T_7 T_12)) ### Axiom % 0.18/0.50 50. (nonreflexive T_7 T_12) (-. (nonreflexive T_7 T_12)) ### Axiom % 0.18/0.50 51. (drink T_7 T_12) (-. (drink T_7 T_12)) ### Axiom % 0.18/0.50 52. (event T_7 T_13) (-. (event T_7 T_13)) ### Axiom % 0.18/0.50 53. (agent T_7 T_13 T_8) (-. (agent T_7 T_13 T_8)) ### Axiom % 0.18/0.50 54. (patient T_7 T_13 T_10) (-. (patient T_7 T_13 T_10)) ### Axiom % 0.18/0.50 55. (past T_7 T_13) (-. (past T_7 T_13)) ### Axiom % 0.18/0.50 56. (nonreflexive T_7 T_13) (-. (nonreflexive T_7 T_13)) ### Axiom % 0.18/0.50 57. (see T_7 T_13) (-. (see T_7 T_13)) ### Axiom % 0.18/0.50 58. (-. ((human_person T_7 T_10) /\ ((coffee T_7 T_11) /\ ((event T_7 T_12) /\ ((agent T_7 T_12 T_10) /\ ((patient T_7 T_12 T_11) /\ ((past T_7 T_12) /\ ((nonreflexive T_7 T_12) /\ ((drink T_7 T_12) /\ ((event T_7 T_13) /\ ((agent T_7 T_13 T_8) /\ ((patient T_7 T_13 T_10) /\ ((past T_7 T_13) /\ ((nonreflexive T_7 T_13) /\ (see T_7 T_13))))))))))))))) (see T_7 T_13) (nonreflexive T_7 T_13) (past T_7 T_13) (patient T_7 T_13 T_10) (agent T_7 T_13 T_8) (event T_7 T_13) (drink T_7 T_12) (nonreflexive T_7 T_12) (past T_7 T_12) (patient T_7 T_12 T_11) (agent T_7 T_12 T_10) (event T_7 T_12) (coffee T_7 T_11) (human_person T_7 T_10) ### DisjTree 44 45 46 47 48 49 50 51 52 53 54 55 56 57 % 0.18/0.50 59. (-. (Ex X1, ((human_person T_7 T_10) /\ ((coffee T_7 T_11) /\ ((event T_7 T_12) /\ ((agent T_7 T_12 T_10) /\ ((patient T_7 T_12 T_11) /\ ((past T_7 T_12) /\ ((nonreflexive T_7 T_12) /\ ((drink T_7 T_12) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 T_10) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1)))))))))))))))) (human_person T_7 T_10) (coffee T_7 T_11) (event T_7 T_12) (agent T_7 T_12 T_10) (patient T_7 T_12 T_11) (past T_7 T_12) (nonreflexive T_7 T_12) (drink T_7 T_12) (event T_7 T_13) (agent T_7 T_13 T_8) (patient T_7 T_13 T_10) (past T_7 T_13) (nonreflexive T_7 T_13) (see T_7 T_13) ### NotExists 58 % 0.18/0.50 60. (-. (Ex Z, (Ex X1, ((human_person T_7 T_10) /\ ((coffee T_7 T_11) /\ ((event T_7 Z) /\ ((agent T_7 Z T_10) /\ ((patient T_7 Z T_11) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 T_10) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))) (see T_7 T_13) (nonreflexive T_7 T_13) (past T_7 T_13) (patient T_7 T_13 T_10) (agent T_7 T_13 T_8) (event T_7 T_13) (drink T_7 T_12) (nonreflexive T_7 T_12) (past T_7 T_12) (patient T_7 T_12 T_11) (agent T_7 T_12 T_10) (event T_7 T_12) (coffee T_7 T_11) (human_person T_7 T_10) ### NotExists 59 % 0.18/0.50 61. (-. (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 T_10) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z T_10) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 T_10) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1)))))))))))))))))) (human_person T_7 T_10) (coffee T_7 T_11) (event T_7 T_12) (agent T_7 T_12 T_10) (patient T_7 T_12 T_11) (past T_7 T_12) (nonreflexive T_7 T_12) (drink T_7 T_12) (event T_7 T_13) (agent T_7 T_13 T_8) (patient T_7 T_13 T_10) (past T_7 T_13) (nonreflexive T_7 T_13) (see T_7 T_13) ### NotExists 60 % 0.18/0.50 62. (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))) (see T_7 T_13) (nonreflexive T_7 T_13) (past T_7 T_13) (patient T_7 T_13 T_10) (agent T_7 T_13 T_8) (event T_7 T_13) (drink T_7 T_12) (nonreflexive T_7 T_12) (past T_7 T_12) (patient T_7 T_12 T_11) (agent T_7 T_12 T_10) (event T_7 T_12) (coffee T_7 T_11) (human_person T_7 T_10) ### NotExists 61 % 0.18/0.50 63. ((coffee T_7 T_11) /\ ((human_person T_7 T_10) /\ ((event T_7 T_12) /\ ((agent T_7 T_12 T_10) /\ ((patient T_7 T_12 T_11) /\ ((past T_7 T_12) /\ ((nonreflexive T_7 T_12) /\ ((drink T_7 T_12) /\ ((event T_7 T_13) /\ ((agent T_7 T_13 T_8) /\ ((patient T_7 T_13 T_10) /\ ((past T_7 T_13) /\ ((nonreflexive T_7 T_13) /\ (see T_7 T_13)))))))))))))) (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))) ### ConjTree 62 % 0.18/0.50 64. (Ex X8, ((coffee T_7 T_11) /\ ((human_person T_7 T_10) /\ ((event T_7 T_12) /\ ((agent T_7 T_12 T_10) /\ ((patient T_7 T_12 T_11) /\ ((past T_7 T_12) /\ ((nonreflexive T_7 T_12) /\ ((drink T_7 T_12) /\ ((event T_7 X8) /\ ((agent T_7 X8 T_8) /\ ((patient T_7 X8 T_10) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8))))))))))))))) (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))) ### Exists 63 % 0.18/0.50 65. (Ex X7, (Ex X8, ((coffee T_7 T_11) /\ ((human_person T_7 T_10) /\ ((event T_7 X7) /\ ((agent T_7 X7 T_10) /\ ((patient T_7 X7 T_11) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 T_8) /\ ((patient T_7 X8 T_10) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8)))))))))))))))) (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))) ### Exists 64 % 0.18/0.50 66. (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 T_11) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 T_11) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 T_8) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8))))))))))))))))) (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))) ### Exists 65 % 0.18/0.50 67. (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 X5) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 X5) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 T_8) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8)))))))))))))))))) (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))) ### Exists 66 % 0.18/0.51 68. (((customer T_7 T_8) /\ ((restaurant T_7 T_9) /\ (in T_7 T_8 T_9))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 X5) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 X5) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 T_8) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8))))))))))))))))))) (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))) (in T_7 T_8 T_9) (restaurant T_7 T_9) (customer T_7 T_8) ### DisjTree 41 42 43 67 % 0.18/0.51 69. (All X4, (((customer T_7 T_8) /\ ((restaurant T_7 X4) /\ (in T_7 T_8 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 X5) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 X5) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 T_8) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8)))))))))))))))))))) (customer T_7 T_8) (restaurant T_7 T_9) (in T_7 T_8 T_9) (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))) ### All 68 % 0.18/0.51 70. (All X3, (All X4, (((customer T_7 X3) /\ ((restaurant T_7 X4) /\ (in T_7 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 X5) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 X5) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 X3) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8))))))))))))))))))))) (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))) (in T_7 T_8 T_9) (restaurant T_7 T_9) (customer T_7 T_8) ### All 69 % 0.18/0.51 71. (-. (((customer T_7 T_8) /\ ((restaurant T_7 T_9) /\ (in T_7 T_8 T_9))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1)))))))))))))))))))) (All X3, (All X4, (((customer T_7 X3) /\ ((restaurant T_7 X4) /\ (in T_7 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 X5) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 X5) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 X3) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8))))))))))))))))))))) ### ConjTree 70 % 0.18/0.51 72. (-. (All W, (((customer T_7 T_8) /\ ((restaurant T_7 W) /\ (in T_7 T_8 W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 T_8) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))))) (All X3, (All X4, (((customer T_7 X3) /\ ((restaurant T_7 X4) /\ (in T_7 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 X5) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 X5) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 X3) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8))))))))))))))))))))) ### NotAllEx 71 % 0.18/0.51 73. (-. (All V, (All W, (((customer T_7 V) /\ ((restaurant T_7 W) /\ (in T_7 V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 V) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1)))))))))))))))))))))) (All X3, (All X4, (((customer T_7 X3) /\ ((restaurant T_7 X4) /\ (in T_7 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 X5) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 X5) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 X3) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8))))))))))))))))))))) ### NotAllEx 72 % 0.18/0.51 74. (-. ((actual_world T_7) /\ (All V, (All W, (((customer T_7 V) /\ ((restaurant T_7 W) /\ (in T_7 V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person T_7 X) /\ ((coffee T_7 Y) /\ ((event T_7 Z) /\ ((agent T_7 Z X) /\ ((patient T_7 Z Y) /\ ((past T_7 Z) /\ ((nonreflexive T_7 Z) /\ ((drink T_7 Z) /\ ((event T_7 X1) /\ ((agent T_7 X1 V) /\ ((patient T_7 X1 X) /\ ((past T_7 X1) /\ ((nonreflexive T_7 X1) /\ (see T_7 X1))))))))))))))))))))))) (All X3, (All X4, (((customer T_7 X3) /\ ((restaurant T_7 X4) /\ (in T_7 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 X5) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 X5) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 X3) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8))))))))))))))))))))) (actual_world T_7) ### NotAnd 40 73 % 0.18/0.51 75. (-. (Ex U, ((actual_world U) /\ (All V, (All W, (((customer U V) /\ ((restaurant U W) /\ (in U V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person U X) /\ ((coffee U Y) /\ ((event U Z) /\ ((agent U Z X) /\ ((patient U Z Y) /\ ((past U Z) /\ ((nonreflexive U Z) /\ ((drink U Z) /\ ((event U X1) /\ ((agent U X1 V) /\ ((patient U X1 X) /\ ((past U X1) /\ ((nonreflexive U X1) /\ (see U X1)))))))))))))))))))))))) (actual_world T_7) (All X3, (All X4, (((customer T_7 X3) /\ ((restaurant T_7 X4) /\ (in T_7 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 X5) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 X5) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 X3) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8))))))))))))))))))))) ### NotExists 74 % 0.18/0.51 76. ((actual_world T_7) /\ (All X3, (All X4, (((customer T_7 X3) /\ ((restaurant T_7 X4) /\ (in T_7 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee T_7 X5) /\ ((human_person T_7 X6) /\ ((event T_7 X7) /\ ((agent T_7 X7 X6) /\ ((patient T_7 X7 X5) /\ ((past T_7 X7) /\ ((nonreflexive T_7 X7) /\ ((drink T_7 X7) /\ ((event T_7 X8) /\ ((agent T_7 X8 X3) /\ ((patient T_7 X8 X6) /\ ((past T_7 X8) /\ ((nonreflexive T_7 X8) /\ (see T_7 X8)))))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (All V, (All W, (((customer U V) /\ ((restaurant U W) /\ (in U V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person U X) /\ ((coffee U Y) /\ ((event U Z) /\ ((agent U Z X) /\ ((patient U Z Y) /\ ((past U Z) /\ ((nonreflexive U Z) /\ ((drink U Z) /\ ((event U X1) /\ ((agent U X1 V) /\ ((patient U X1 X) /\ ((past U X1) /\ ((nonreflexive U X1) /\ (see U X1)))))))))))))))))))))))) ### And 75 % 0.18/0.51 77. (Ex X2, ((actual_world X2) /\ (All X3, (All X4, (((customer X2 X3) /\ ((restaurant X2 X4) /\ (in X2 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee X2 X5) /\ ((human_person X2 X6) /\ ((event X2 X7) /\ ((agent X2 X7 X6) /\ ((patient X2 X7 X5) /\ ((past X2 X7) /\ ((nonreflexive X2 X7) /\ ((drink X2 X7) /\ ((event X2 X8) /\ ((agent X2 X8 X3) /\ ((patient X2 X8 X6) /\ ((past X2 X8) /\ ((nonreflexive X2 X8) /\ (see X2 X8))))))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (All V, (All W, (((customer U V) /\ ((restaurant U W) /\ (in U V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person U X) /\ ((coffee U Y) /\ ((event U Z) /\ ((agent U Z X) /\ ((patient U Z Y) /\ ((past U Z) /\ ((nonreflexive U Z) /\ ((drink U Z) /\ ((event U X1) /\ ((agent U X1 V) /\ ((patient U X1 X) /\ ((past U X1) /\ ((nonreflexive U X1) /\ (see U X1)))))))))))))))))))))))) ### Exists 76 % 0.18/0.51 78. (-. ((Ex X2, ((actual_world X2) /\ (All X3, (All X4, (((customer X2 X3) /\ ((restaurant X2 X4) /\ (in X2 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee X2 X5) /\ ((human_person X2 X6) /\ ((event X2 X7) /\ ((agent X2 X7 X6) /\ ((patient X2 X7 X5) /\ ((past X2 X7) /\ ((nonreflexive X2 X7) /\ ((drink X2 X7) /\ ((event X2 X8) /\ ((agent X2 X8 X3) /\ ((patient X2 X8 X6) /\ ((past X2 X8) /\ ((nonreflexive X2 X8) /\ (see X2 X8))))))))))))))))))))))) => (Ex U, ((actual_world U) /\ (All V, (All W, (((customer U V) /\ ((restaurant U W) /\ (in U V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person U X) /\ ((coffee U Y) /\ ((event U Z) /\ ((agent U Z X) /\ ((patient U Z Y) /\ ((past U Z) /\ ((nonreflexive U Z) /\ ((drink U Z) /\ ((event U X1) /\ ((agent U X1 V) /\ ((patient U X1 X) /\ ((past U X1) /\ ((nonreflexive U X1) /\ (see U X1))))))))))))))))))))))))) ### NotImply 77 % 0.18/0.51 79. (-. (((Ex U, ((actual_world U) /\ (All V, (All W, (((customer U V) /\ ((restaurant U W) /\ (in U V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person U X) /\ ((coffee U Y) /\ ((event U Z) /\ ((agent U Z X) /\ ((patient U Z Y) /\ ((past U Z) /\ ((nonreflexive U Z) /\ ((drink U Z) /\ ((event U X1) /\ ((agent U X1 V) /\ ((patient U X1 X) /\ ((past U X1) /\ ((nonreflexive U X1) /\ (see U X1))))))))))))))))))))))) => (Ex X2, ((actual_world X2) /\ (All X3, (All X4, (((customer X2 X3) /\ ((restaurant X2 X4) /\ (in X2 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee X2 X5) /\ ((human_person X2 X6) /\ ((event X2 X7) /\ ((agent X2 X7 X6) /\ ((patient X2 X7 X5) /\ ((past X2 X7) /\ ((nonreflexive X2 X7) /\ ((drink X2 X7) /\ ((event X2 X8) /\ ((agent X2 X8 X3) /\ ((patient X2 X8 X6) /\ ((past X2 X8) /\ ((nonreflexive X2 X8) /\ (see X2 X8)))))))))))))))))))))))) /\ ((Ex X2, ((actual_world X2) /\ (All X3, (All X4, (((customer X2 X3) /\ ((restaurant X2 X4) /\ (in X2 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee X2 X5) /\ ((human_person X2 X6) /\ ((event X2 X7) /\ ((agent X2 X7 X6) /\ ((patient X2 X7 X5) /\ ((past X2 X7) /\ ((nonreflexive X2 X7) /\ ((drink X2 X7) /\ ((event X2 X8) /\ ((agent X2 X8 X3) /\ ((patient X2 X8 X6) /\ ((past X2 X8) /\ ((nonreflexive X2 X8) /\ (see X2 X8))))))))))))))))))))))) => (Ex U, ((actual_world U) /\ (All V, (All W, (((customer U V) /\ ((restaurant U W) /\ (in U V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person U X) /\ ((coffee U Y) /\ ((event U Z) /\ ((agent U Z X) /\ ((patient U Z Y) /\ ((past U Z) /\ ((nonreflexive U Z) /\ ((drink U Z) /\ ((event U X1) /\ ((agent U X1 V) /\ ((patient U X1 X) /\ ((past U X1) /\ ((nonreflexive U X1) /\ (see U X1)))))))))))))))))))))))))) ### NotAnd 39 78 % 0.18/0.51 80. (-. (-. (-. (((Ex U, ((actual_world U) /\ (All V, (All W, (((customer U V) /\ ((restaurant U W) /\ (in U V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person U X) /\ ((coffee U Y) /\ ((event U Z) /\ ((agent U Z X) /\ ((patient U Z Y) /\ ((past U Z) /\ ((nonreflexive U Z) /\ ((drink U Z) /\ ((event U X1) /\ ((agent U X1 V) /\ ((patient U X1 X) /\ ((past U X1) /\ ((nonreflexive U X1) /\ (see U X1))))))))))))))))))))))) => (Ex X2, ((actual_world X2) /\ (All X3, (All X4, (((customer X2 X3) /\ ((restaurant X2 X4) /\ (in X2 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee X2 X5) /\ ((human_person X2 X6) /\ ((event X2 X7) /\ ((agent X2 X7 X6) /\ ((patient X2 X7 X5) /\ ((past X2 X7) /\ ((nonreflexive X2 X7) /\ ((drink X2 X7) /\ ((event X2 X8) /\ ((agent X2 X8 X3) /\ ((patient X2 X8 X6) /\ ((past X2 X8) /\ ((nonreflexive X2 X8) /\ (see X2 X8)))))))))))))))))))))))) /\ ((Ex X2, ((actual_world X2) /\ (All X3, (All X4, (((customer X2 X3) /\ ((restaurant X2 X4) /\ (in X2 X3 X4))) => (Ex X5, (Ex X6, (Ex X7, (Ex X8, ((coffee X2 X5) /\ ((human_person X2 X6) /\ ((event X2 X7) /\ ((agent X2 X7 X6) /\ ((patient X2 X7 X5) /\ ((past X2 X7) /\ ((nonreflexive X2 X7) /\ ((drink X2 X7) /\ ((event X2 X8) /\ ((agent X2 X8 X3) /\ ((patient X2 X8 X6) /\ ((past X2 X8) /\ ((nonreflexive X2 X8) /\ (see X2 X8))))))))))))))))))))))) => (Ex U, ((actual_world U) /\ (All V, (All W, (((customer U V) /\ ((restaurant U W) /\ (in U V W))) => (Ex X, (Ex Y, (Ex Z, (Ex X1, ((human_person U X) /\ ((coffee U Y) /\ ((event U Z) /\ ((agent U Z X) /\ ((patient U Z Y) /\ ((past U Z) /\ ((nonreflexive U Z) /\ ((drink U Z) /\ ((event U X1) /\ ((agent U X1 V) /\ ((patient U X1 X) /\ ((past U X1) /\ ((nonreflexive U X1) /\ (see U X1)))))))))))))))))))))))))))) ### NotNot 79 % 0.18/0.51 % SZS output end Proof % 0.18/0.51 (* END-PROOF *) %------------------------------------------------------------------------------