%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NLP122+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 : n029.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:33:15 EDT 2022 % Result : Theorem 0.20s 0.44s % Output : Proof 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NLP122+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 : n029.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 05:01:39 EDT 2022 % 0.12/0.33 % CPUTime : % 0.20/0.44 % SZS status Theorem % 0.20/0.44 (* PROOF-FOUND *) % 0.20/0.44 (* BEGIN-PROOF *) % 0.20/0.44 % SZS output start Proof % 0.20/0.44 1. (actual_world T_0) (-. (actual_world T_0)) ### Axiom % 0.20/0.44 2. (street T_0 T_1) (-. (street T_0 T_1)) ### Axiom % 0.20/0.44 3. (lonely T_0 T_1) (-. (lonely T_0 T_1)) ### Axiom % 0.20/0.44 4. (of T_0 T_2 T_3) (-. (of T_0 T_2 T_3)) ### Axiom % 0.20/0.44 5. (city T_0 T_3) (-. (city T_0 T_3)) ### Axiom % 0.20/0.44 6. (hollywood_placename T_0 T_2) (-. (hollywood_placename T_0 T_2)) ### Axiom % 0.20/0.44 7. (placename T_0 T_2) (-. (placename T_0 T_2)) ### Axiom % 0.20/0.44 8. (chevy T_0 T_3) (-. (chevy T_0 T_3)) ### Axiom % 0.20/0.44 9. (white T_0 T_3) (-. (white T_0 T_3)) ### Axiom % 0.20/0.44 10. (dirty T_0 T_3) (-. (dirty T_0 T_3)) ### Axiom % 0.20/0.44 11. (old T_0 T_3) (-. (old T_0 T_3)) ### Axiom % 0.20/0.44 12. (event T_0 T_4) (-. (event T_0 T_4)) ### Axiom % 0.20/0.44 13. (agent T_0 T_4 T_3) (-. (agent T_0 T_4 T_3)) ### Axiom % 0.20/0.44 14. (present T_0 T_4) (-. (present T_0 T_4)) ### Axiom % 0.20/0.44 15. (barrel T_0 T_4) (-. (barrel T_0 T_4)) ### Axiom % 0.20/0.44 16. (down T_0 T_4 T_1) (-. (down T_0 T_4 T_1)) ### Axiom % 0.20/0.44 17. (in T_0 T_4 T_3) (-. (in T_0 T_4 T_3)) ### Axiom % 0.20/0.44 18. (-. ((street T_0 T_1) /\ ((lonely T_0 T_1) /\ ((of T_0 T_2 T_3) /\ ((city T_0 T_3) /\ ((hollywood_placename T_0 T_2) /\ ((placename T_0 T_2) /\ ((chevy T_0 T_3) /\ ((white T_0 T_3) /\ ((dirty T_0 T_3) /\ ((old T_0 T_3) /\ ((event T_0 T_4) /\ ((agent T_0 T_4 T_3) /\ ((present T_0 T_4) /\ ((barrel T_0 T_4) /\ ((down T_0 T_4 T_1) /\ (in T_0 T_4 T_3))))))))))))))))) (in T_0 T_4 T_3) (down T_0 T_4 T_1) (barrel T_0 T_4) (present T_0 T_4) (agent T_0 T_4 T_3) (event T_0 T_4) (old T_0 T_3) (dirty T_0 T_3) (white T_0 T_3) (chevy T_0 T_3) (placename T_0 T_2) (hollywood_placename T_0 T_2) (city T_0 T_3) (of T_0 T_2 T_3) (lonely T_0 T_1) (street T_0 T_1) ### DisjTree 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 % 0.20/0.44 19. (-. (Ex X4, ((street T_0 T_1) /\ ((lonely T_0 T_1) /\ ((of T_0 T_2 T_3) /\ ((city T_0 T_3) /\ ((hollywood_placename T_0 T_2) /\ ((placename T_0 T_2) /\ ((chevy T_0 T_3) /\ ((white T_0 T_3) /\ ((dirty T_0 T_3) /\ ((old T_0 T_3) /\ ((event T_0 X4) /\ ((agent T_0 X4 T_3) /\ ((present T_0 X4) /\ ((barrel T_0 X4) /\ ((down T_0 X4 T_1) /\ (in T_0 X4 T_3)))))))))))))))))) (street T_0 T_1) (lonely T_0 T_1) (of T_0 T_2 T_3) (city T_0 T_3) (hollywood_placename T_0 T_2) (placename T_0 T_2) (chevy T_0 T_3) (white T_0 T_3) (dirty T_0 T_3) (old T_0 T_3) (event T_0 T_4) (agent T_0 T_4 T_3) (present T_0 T_4) (barrel T_0 T_4) (down T_0 T_4 T_1) (in T_0 T_4 T_3) ### NotExists 18 % 0.20/0.44 20. (-. (Ex X3, (Ex X4, ((street T_0 T_1) /\ ((lonely T_0 T_1) /\ ((of T_0 T_2 X3) /\ ((city T_0 X3) /\ ((hollywood_placename T_0 T_2) /\ ((placename T_0 T_2) /\ ((chevy T_0 X3) /\ ((white T_0 X3) /\ ((dirty T_0 X3) /\ ((old T_0 X3) /\ ((event T_0 X4) /\ ((agent T_0 X4 X3) /\ ((present T_0 X4) /\ ((barrel T_0 X4) /\ ((down T_0 X4 T_1) /\ (in T_0 X4 X3))))))))))))))))))) (in T_0 T_4 T_3) (down T_0 T_4 T_1) (barrel T_0 T_4) (present T_0 T_4) (agent T_0 T_4 T_3) (event T_0 T_4) (old T_0 T_3) (dirty T_0 T_3) (white T_0 T_3) (chevy T_0 T_3) (placename T_0 T_2) (hollywood_placename T_0 T_2) (city T_0 T_3) (of T_0 T_2 T_3) (lonely T_0 T_1) (street T_0 T_1) ### NotExists 19 % 0.20/0.44 21. (-. (Ex X2, (Ex X3, (Ex X4, ((street T_0 T_1) /\ ((lonely T_0 T_1) /\ ((of T_0 X2 X3) /\ ((city T_0 X3) /\ ((hollywood_placename T_0 X2) /\ ((placename T_0 X2) /\ ((chevy T_0 X3) /\ ((white T_0 X3) /\ ((dirty T_0 X3) /\ ((old T_0 X3) /\ ((event T_0 X4) /\ ((agent T_0 X4 X3) /\ ((present T_0 X4) /\ ((barrel T_0 X4) /\ ((down T_0 X4 T_1) /\ (in T_0 X4 X3)))))))))))))))))))) (street T_0 T_1) (lonely T_0 T_1) (of T_0 T_2 T_3) (city T_0 T_3) (hollywood_placename T_0 T_2) (placename T_0 T_2) (chevy T_0 T_3) (white T_0 T_3) (dirty T_0 T_3) (old T_0 T_3) (event T_0 T_4) (agent T_0 T_4 T_3) (present T_0 T_4) (barrel T_0 T_4) (down T_0 T_4 T_1) (in T_0 T_4 T_3) ### NotExists 20 % 0.20/0.44 22. (-. (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street T_0 X1) /\ ((lonely T_0 X1) /\ ((of T_0 X2 X3) /\ ((city T_0 X3) /\ ((hollywood_placename T_0 X2) /\ ((placename T_0 X2) /\ ((chevy T_0 X3) /\ ((white T_0 X3) /\ ((dirty T_0 X3) /\ ((old T_0 X3) /\ ((event T_0 X4) /\ ((agent T_0 X4 X3) /\ ((present T_0 X4) /\ ((barrel T_0 X4) /\ ((down T_0 X4 X1) /\ (in T_0 X4 X3))))))))))))))))))))) (in T_0 T_4 T_3) (down T_0 T_4 T_1) (barrel T_0 T_4) (present T_0 T_4) (agent T_0 T_4 T_3) (event T_0 T_4) (old T_0 T_3) (dirty T_0 T_3) (white T_0 T_3) (chevy T_0 T_3) (placename T_0 T_2) (hollywood_placename T_0 T_2) (city T_0 T_3) (of T_0 T_2 T_3) (lonely T_0 T_1) (street T_0 T_1) ### NotExists 21 % 0.20/0.44 23. (-. ((actual_world T_0) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street T_0 X1) /\ ((lonely T_0 X1) /\ ((of T_0 X2 X3) /\ ((city T_0 X3) /\ ((hollywood_placename T_0 X2) /\ ((placename T_0 X2) /\ ((chevy T_0 X3) /\ ((white T_0 X3) /\ ((dirty T_0 X3) /\ ((old T_0 X3) /\ ((event T_0 X4) /\ ((agent T_0 X4 X3) /\ ((present T_0 X4) /\ ((barrel T_0 X4) /\ ((down T_0 X4 X1) /\ (in T_0 X4 X3)))))))))))))))))))))) (street T_0 T_1) (lonely T_0 T_1) (of T_0 T_2 T_3) (city T_0 T_3) (hollywood_placename T_0 T_2) (placename T_0 T_2) (chevy T_0 T_3) (white T_0 T_3) (dirty T_0 T_3) (old T_0 T_3) (event T_0 T_4) (agent T_0 T_4 T_3) (present T_0 T_4) (barrel T_0 T_4) (down T_0 T_4 T_1) (in T_0 T_4 T_3) (actual_world T_0) ### NotAnd 1 22 % 0.20/0.44 24. (-. (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3))))))))))))))))))))))) (actual_world T_0) (in T_0 T_4 T_3) (down T_0 T_4 T_1) (barrel T_0 T_4) (present T_0 T_4) (agent T_0 T_4 T_3) (event T_0 T_4) (old T_0 T_3) (dirty T_0 T_3) (white T_0 T_3) (chevy T_0 T_3) (placename T_0 T_2) (hollywood_placename T_0 T_2) (city T_0 T_3) (of T_0 T_2 T_3) (lonely T_0 T_1) (street T_0 T_1) ### NotExists 23 % 0.20/0.44 25. ((of T_0 T_2 T_3) /\ ((city T_0 T_3) /\ ((hollywood_placename T_0 T_2) /\ ((placename T_0 T_2) /\ ((chevy T_0 T_3) /\ ((white T_0 T_3) /\ ((dirty T_0 T_3) /\ ((old T_0 T_3) /\ ((street T_0 T_1) /\ ((lonely T_0 T_1) /\ ((event T_0 T_4) /\ ((agent T_0 T_4 T_3) /\ ((present T_0 T_4) /\ ((barrel T_0 T_4) /\ ((down T_0 T_4 T_1) /\ (in T_0 T_4 T_3)))))))))))))))) (actual_world T_0) (-. (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3))))))))))))))))))))))) ### ConjTree 24 % 0.20/0.44 26. (Ex Y, ((of T_0 T_2 T_3) /\ ((city T_0 T_3) /\ ((hollywood_placename T_0 T_2) /\ ((placename T_0 T_2) /\ ((chevy T_0 T_3) /\ ((white T_0 T_3) /\ ((dirty T_0 T_3) /\ ((old T_0 T_3) /\ ((street T_0 T_1) /\ ((lonely T_0 T_1) /\ ((event T_0 Y) /\ ((agent T_0 Y T_3) /\ ((present T_0 Y) /\ ((barrel T_0 Y) /\ ((down T_0 Y T_1) /\ (in T_0 Y T_3))))))))))))))))) (-. (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3))))))))))))))))))))))) (actual_world T_0) ### Exists 25 % 0.20/0.44 27. (Ex X, (Ex Y, ((of T_0 T_2 T_3) /\ ((city T_0 T_3) /\ ((hollywood_placename T_0 T_2) /\ ((placename T_0 T_2) /\ ((chevy T_0 T_3) /\ ((white T_0 T_3) /\ ((dirty T_0 T_3) /\ ((old T_0 T_3) /\ ((street T_0 X) /\ ((lonely T_0 X) /\ ((event T_0 Y) /\ ((agent T_0 Y T_3) /\ ((present T_0 Y) /\ ((barrel T_0 Y) /\ ((down T_0 Y X) /\ (in T_0 Y T_3)))))))))))))))))) (actual_world T_0) (-. (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3))))))))))))))))))))))) ### Exists 26 % 0.20/0.46 28. (Ex W, (Ex X, (Ex Y, ((of T_0 T_2 W) /\ ((city T_0 W) /\ ((hollywood_placename T_0 T_2) /\ ((placename T_0 T_2) /\ ((chevy T_0 W) /\ ((white T_0 W) /\ ((dirty T_0 W) /\ ((old T_0 W) /\ ((street T_0 X) /\ ((lonely T_0 X) /\ ((event T_0 Y) /\ ((agent T_0 Y W) /\ ((present T_0 Y) /\ ((barrel T_0 Y) /\ ((down T_0 Y X) /\ (in T_0 Y W))))))))))))))))))) (-. (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3))))))))))))))))))))))) (actual_world T_0) ### Exists 27 % 0.20/0.46 29. (Ex V, (Ex W, (Ex X, (Ex Y, ((of T_0 V W) /\ ((city T_0 W) /\ ((hollywood_placename T_0 V) /\ ((placename T_0 V) /\ ((chevy T_0 W) /\ ((white T_0 W) /\ ((dirty T_0 W) /\ ((old T_0 W) /\ ((street T_0 X) /\ ((lonely T_0 X) /\ ((event T_0 Y) /\ ((agent T_0 Y W) /\ ((present T_0 Y) /\ ((barrel T_0 Y) /\ ((down T_0 Y X) /\ (in T_0 Y W)))))))))))))))))))) (actual_world T_0) (-. (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3))))))))))))))))))))))) ### Exists 28 % 0.20/0.46 30. ((actual_world T_0) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of T_0 V W) /\ ((city T_0 W) /\ ((hollywood_placename T_0 V) /\ ((placename T_0 V) /\ ((chevy T_0 W) /\ ((white T_0 W) /\ ((dirty T_0 W) /\ ((old T_0 W) /\ ((street T_0 X) /\ ((lonely T_0 X) /\ ((event T_0 Y) /\ ((agent T_0 Y W) /\ ((present T_0 Y) /\ ((barrel T_0 Y) /\ ((down T_0 Y X) /\ (in T_0 Y W))))))))))))))))))))) (-. (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3))))))))))))))))))))))) ### And 29 % 0.20/0.46 31. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W)))))))))))))))))))))) (-. (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3))))))))))))))))))))))) ### Exists 30 % 0.20/0.46 32. (-. ((Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W)))))))))))))))))))))) => (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3)))))))))))))))))))))))) ### NotImply 31 % 0.20/0.46 33. (actual_world T_5) (-. (actual_world T_5)) ### Axiom % 0.20/0.46 34. (of T_5 T_6 T_7) (-. (of T_5 T_6 T_7)) ### Axiom % 0.20/0.46 35. (city T_5 T_7) (-. (city T_5 T_7)) ### Axiom % 0.20/0.46 36. (hollywood_placename T_5 T_6) (-. (hollywood_placename T_5 T_6)) ### Axiom % 0.20/0.46 37. (placename T_5 T_6) (-. (placename T_5 T_6)) ### Axiom % 0.20/0.46 38. (chevy T_5 T_7) (-. (chevy T_5 T_7)) ### Axiom % 0.20/0.46 39. (white T_5 T_7) (-. (white T_5 T_7)) ### Axiom % 0.20/0.46 40. (dirty T_5 T_7) (-. (dirty T_5 T_7)) ### Axiom % 0.20/0.46 41. (old T_5 T_7) (-. (old T_5 T_7)) ### Axiom % 0.20/0.46 42. (street T_5 T_8) (-. (street T_5 T_8)) ### Axiom % 0.20/0.46 43. (lonely T_5 T_8) (-. (lonely T_5 T_8)) ### Axiom % 0.20/0.46 44. (event T_5 T_9) (-. (event T_5 T_9)) ### Axiom % 0.20/0.46 45. (agent T_5 T_9 T_7) (-. (agent T_5 T_9 T_7)) ### Axiom % 0.20/0.46 46. (present T_5 T_9) (-. (present T_5 T_9)) ### Axiom % 0.20/0.46 47. (barrel T_5 T_9) (-. (barrel T_5 T_9)) ### Axiom % 0.20/0.46 48. (down T_5 T_9 T_8) (-. (down T_5 T_9 T_8)) ### Axiom % 0.20/0.46 49. (in T_5 T_9 T_7) (-. (in T_5 T_9 T_7)) ### Axiom % 0.20/0.46 50. (-. ((of T_5 T_6 T_7) /\ ((city T_5 T_7) /\ ((hollywood_placename T_5 T_6) /\ ((placename T_5 T_6) /\ ((chevy T_5 T_7) /\ ((white T_5 T_7) /\ ((dirty T_5 T_7) /\ ((old T_5 T_7) /\ ((street T_5 T_8) /\ ((lonely T_5 T_8) /\ ((event T_5 T_9) /\ ((agent T_5 T_9 T_7) /\ ((present T_5 T_9) /\ ((barrel T_5 T_9) /\ ((down T_5 T_9 T_8) /\ (in T_5 T_9 T_7))))))))))))))))) (in T_5 T_9 T_7) (down T_5 T_9 T_8) (barrel T_5 T_9) (present T_5 T_9) (agent T_5 T_9 T_7) (event T_5 T_9) (lonely T_5 T_8) (street T_5 T_8) (old T_5 T_7) (dirty T_5 T_7) (white T_5 T_7) (chevy T_5 T_7) (placename T_5 T_6) (hollywood_placename T_5 T_6) (city T_5 T_7) (of T_5 T_6 T_7) ### DisjTree 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 % 0.20/0.46 51. (-. (Ex Y, ((of T_5 T_6 T_7) /\ ((city T_5 T_7) /\ ((hollywood_placename T_5 T_6) /\ ((placename T_5 T_6) /\ ((chevy T_5 T_7) /\ ((white T_5 T_7) /\ ((dirty T_5 T_7) /\ ((old T_5 T_7) /\ ((street T_5 T_8) /\ ((lonely T_5 T_8) /\ ((event T_5 Y) /\ ((agent T_5 Y T_7) /\ ((present T_5 Y) /\ ((barrel T_5 Y) /\ ((down T_5 Y T_8) /\ (in T_5 Y T_7)))))))))))))))))) (of T_5 T_6 T_7) (city T_5 T_7) (hollywood_placename T_5 T_6) (placename T_5 T_6) (chevy T_5 T_7) (white T_5 T_7) (dirty T_5 T_7) (old T_5 T_7) (street T_5 T_8) (lonely T_5 T_8) (event T_5 T_9) (agent T_5 T_9 T_7) (present T_5 T_9) (barrel T_5 T_9) (down T_5 T_9 T_8) (in T_5 T_9 T_7) ### NotExists 50 % 0.20/0.46 52. (-. (Ex X, (Ex Y, ((of T_5 T_6 T_7) /\ ((city T_5 T_7) /\ ((hollywood_placename T_5 T_6) /\ ((placename T_5 T_6) /\ ((chevy T_5 T_7) /\ ((white T_5 T_7) /\ ((dirty T_5 T_7) /\ ((old T_5 T_7) /\ ((street T_5 X) /\ ((lonely T_5 X) /\ ((event T_5 Y) /\ ((agent T_5 Y T_7) /\ ((present T_5 Y) /\ ((barrel T_5 Y) /\ ((down T_5 Y X) /\ (in T_5 Y T_7))))))))))))))))))) (in T_5 T_9 T_7) (down T_5 T_9 T_8) (barrel T_5 T_9) (present T_5 T_9) (agent T_5 T_9 T_7) (event T_5 T_9) (lonely T_5 T_8) (street T_5 T_8) (old T_5 T_7) (dirty T_5 T_7) (white T_5 T_7) (chevy T_5 T_7) (placename T_5 T_6) (hollywood_placename T_5 T_6) (city T_5 T_7) (of T_5 T_6 T_7) ### NotExists 51 % 0.20/0.46 53. (-. (Ex W, (Ex X, (Ex Y, ((of T_5 T_6 W) /\ ((city T_5 W) /\ ((hollywood_placename T_5 T_6) /\ ((placename T_5 T_6) /\ ((chevy T_5 W) /\ ((white T_5 W) /\ ((dirty T_5 W) /\ ((old T_5 W) /\ ((street T_5 X) /\ ((lonely T_5 X) /\ ((event T_5 Y) /\ ((agent T_5 Y W) /\ ((present T_5 Y) /\ ((barrel T_5 Y) /\ ((down T_5 Y X) /\ (in T_5 Y W)))))))))))))))))))) (of T_5 T_6 T_7) (city T_5 T_7) (hollywood_placename T_5 T_6) (placename T_5 T_6) (chevy T_5 T_7) (white T_5 T_7) (dirty T_5 T_7) (old T_5 T_7) (street T_5 T_8) (lonely T_5 T_8) (event T_5 T_9) (agent T_5 T_9 T_7) (present T_5 T_9) (barrel T_5 T_9) (down T_5 T_9 T_8) (in T_5 T_9 T_7) ### NotExists 52 % 0.20/0.46 54. (-. (Ex V, (Ex W, (Ex X, (Ex Y, ((of T_5 V W) /\ ((city T_5 W) /\ ((hollywood_placename T_5 V) /\ ((placename T_5 V) /\ ((chevy T_5 W) /\ ((white T_5 W) /\ ((dirty T_5 W) /\ ((old T_5 W) /\ ((street T_5 X) /\ ((lonely T_5 X) /\ ((event T_5 Y) /\ ((agent T_5 Y W) /\ ((present T_5 Y) /\ ((barrel T_5 Y) /\ ((down T_5 Y X) /\ (in T_5 Y W))))))))))))))))))))) (in T_5 T_9 T_7) (down T_5 T_9 T_8) (barrel T_5 T_9) (present T_5 T_9) (agent T_5 T_9 T_7) (event T_5 T_9) (lonely T_5 T_8) (street T_5 T_8) (old T_5 T_7) (dirty T_5 T_7) (white T_5 T_7) (chevy T_5 T_7) (placename T_5 T_6) (hollywood_placename T_5 T_6) (city T_5 T_7) (of T_5 T_6 T_7) ### NotExists 53 % 0.20/0.46 55. (-. ((actual_world T_5) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of T_5 V W) /\ ((city T_5 W) /\ ((hollywood_placename T_5 V) /\ ((placename T_5 V) /\ ((chevy T_5 W) /\ ((white T_5 W) /\ ((dirty T_5 W) /\ ((old T_5 W) /\ ((street T_5 X) /\ ((lonely T_5 X) /\ ((event T_5 Y) /\ ((agent T_5 Y W) /\ ((present T_5 Y) /\ ((barrel T_5 Y) /\ ((down T_5 Y X) /\ (in T_5 Y W)))))))))))))))))))))) (of T_5 T_6 T_7) (city T_5 T_7) (hollywood_placename T_5 T_6) (placename T_5 T_6) (chevy T_5 T_7) (white T_5 T_7) (dirty T_5 T_7) (old T_5 T_7) (street T_5 T_8) (lonely T_5 T_8) (event T_5 T_9) (agent T_5 T_9 T_7) (present T_5 T_9) (barrel T_5 T_9) (down T_5 T_9 T_8) (in T_5 T_9 T_7) (actual_world T_5) ### NotAnd 33 54 % 0.20/0.46 56. (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W))))))))))))))))))))))) (actual_world T_5) (in T_5 T_9 T_7) (down T_5 T_9 T_8) (barrel T_5 T_9) (present T_5 T_9) (agent T_5 T_9 T_7) (event T_5 T_9) (lonely T_5 T_8) (street T_5 T_8) (old T_5 T_7) (dirty T_5 T_7) (white T_5 T_7) (chevy T_5 T_7) (placename T_5 T_6) (hollywood_placename T_5 T_6) (city T_5 T_7) (of T_5 T_6 T_7) ### NotExists 55 % 0.20/0.46 57. ((street T_5 T_8) /\ ((lonely T_5 T_8) /\ ((of T_5 T_6 T_7) /\ ((city T_5 T_7) /\ ((hollywood_placename T_5 T_6) /\ ((placename T_5 T_6) /\ ((chevy T_5 T_7) /\ ((white T_5 T_7) /\ ((dirty T_5 T_7) /\ ((old T_5 T_7) /\ ((event T_5 T_9) /\ ((agent T_5 T_9 T_7) /\ ((present T_5 T_9) /\ ((barrel T_5 T_9) /\ ((down T_5 T_9 T_8) /\ (in T_5 T_9 T_7)))))))))))))))) (actual_world T_5) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W))))))))))))))))))))))) ### ConjTree 56 % 0.20/0.46 58. (Ex X4, ((street T_5 T_8) /\ ((lonely T_5 T_8) /\ ((of T_5 T_6 T_7) /\ ((city T_5 T_7) /\ ((hollywood_placename T_5 T_6) /\ ((placename T_5 T_6) /\ ((chevy T_5 T_7) /\ ((white T_5 T_7) /\ ((dirty T_5 T_7) /\ ((old T_5 T_7) /\ ((event T_5 X4) /\ ((agent T_5 X4 T_7) /\ ((present T_5 X4) /\ ((barrel T_5 X4) /\ ((down T_5 X4 T_8) /\ (in T_5 X4 T_7))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W))))))))))))))))))))))) (actual_world T_5) ### Exists 57 % 0.20/0.46 59. (Ex X3, (Ex X4, ((street T_5 T_8) /\ ((lonely T_5 T_8) /\ ((of T_5 T_6 X3) /\ ((city T_5 X3) /\ ((hollywood_placename T_5 T_6) /\ ((placename T_5 T_6) /\ ((chevy T_5 X3) /\ ((white T_5 X3) /\ ((dirty T_5 X3) /\ ((old T_5 X3) /\ ((event T_5 X4) /\ ((agent T_5 X4 X3) /\ ((present T_5 X4) /\ ((barrel T_5 X4) /\ ((down T_5 X4 T_8) /\ (in T_5 X4 X3)))))))))))))))))) (actual_world T_5) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W))))))))))))))))))))))) ### Exists 58 % 0.20/0.46 60. (Ex X2, (Ex X3, (Ex X4, ((street T_5 T_8) /\ ((lonely T_5 T_8) /\ ((of T_5 X2 X3) /\ ((city T_5 X3) /\ ((hollywood_placename T_5 X2) /\ ((placename T_5 X2) /\ ((chevy T_5 X3) /\ ((white T_5 X3) /\ ((dirty T_5 X3) /\ ((old T_5 X3) /\ ((event T_5 X4) /\ ((agent T_5 X4 X3) /\ ((present T_5 X4) /\ ((barrel T_5 X4) /\ ((down T_5 X4 T_8) /\ (in T_5 X4 X3))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W))))))))))))))))))))))) (actual_world T_5) ### Exists 59 % 0.20/0.46 61. (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street T_5 X1) /\ ((lonely T_5 X1) /\ ((of T_5 X2 X3) /\ ((city T_5 X3) /\ ((hollywood_placename T_5 X2) /\ ((placename T_5 X2) /\ ((chevy T_5 X3) /\ ((white T_5 X3) /\ ((dirty T_5 X3) /\ ((old T_5 X3) /\ ((event T_5 X4) /\ ((agent T_5 X4 X3) /\ ((present T_5 X4) /\ ((barrel T_5 X4) /\ ((down T_5 X4 X1) /\ (in T_5 X4 X3)))))))))))))))))))) (actual_world T_5) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W))))))))))))))))))))))) ### Exists 60 % 0.20/0.46 62. ((actual_world T_5) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street T_5 X1) /\ ((lonely T_5 X1) /\ ((of T_5 X2 X3) /\ ((city T_5 X3) /\ ((hollywood_placename T_5 X2) /\ ((placename T_5 X2) /\ ((chevy T_5 X3) /\ ((white T_5 X3) /\ ((dirty T_5 X3) /\ ((old T_5 X3) /\ ((event T_5 X4) /\ ((agent T_5 X4 X3) /\ ((present T_5 X4) /\ ((barrel T_5 X4) /\ ((down T_5 X4 X1) /\ (in T_5 X4 X3))))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W))))))))))))))))))))))) ### And 61 % 0.20/0.46 63. (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3)))))))))))))))))))))) (-. (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W))))))))))))))))))))))) ### Exists 62 % 0.20/0.46 64. (-. ((Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3)))))))))))))))))))))) => (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W)))))))))))))))))))))))) ### NotImply 63 % 0.20/0.46 65. (-. (((Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W)))))))))))))))))))))) => (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3))))))))))))))))))))))) /\ ((Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3)))))))))))))))))))))) => (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W))))))))))))))))))))))))) ### NotAnd 32 64 % 0.20/0.46 66. (-. (-. (-. (((Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W)))))))))))))))))))))) => (Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3))))))))))))))))))))))) /\ ((Ex Z, ((actual_world Z) /\ (Ex X1, (Ex X2, (Ex X3, (Ex X4, ((street Z X1) /\ ((lonely Z X1) /\ ((of Z X2 X3) /\ ((city Z X3) /\ ((hollywood_placename Z X2) /\ ((placename Z X2) /\ ((chevy Z X3) /\ ((white Z X3) /\ ((dirty Z X3) /\ ((old Z X3) /\ ((event Z X4) /\ ((agent Z X4 X3) /\ ((present Z X4) /\ ((barrel Z X4) /\ ((down Z X4 X1) /\ (in Z X4 X3)))))))))))))))))))))) => (Ex U, ((actual_world U) /\ (Ex V, (Ex W, (Ex X, (Ex Y, ((of U V W) /\ ((city U W) /\ ((hollywood_placename U V) /\ ((placename U V) /\ ((chevy U W) /\ ((white U W) /\ ((dirty U W) /\ ((old U W) /\ ((street U X) /\ ((lonely U X) /\ ((event U Y) /\ ((agent U Y W) /\ ((present U Y) /\ ((barrel U Y) /\ ((down U Y X) /\ (in U Y W))))))))))))))))))))))))))) ### NotNot 65 % 0.20/0.46 % SZS output end Proof % 0.20/0.46 (* END-PROOF *) %------------------------------------------------------------------------------