%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NLP001+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 : n016.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:02 EDT 2022 % Result : Theorem 0.12s 0.41s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NLP001+1 : TPTP v8.1.0. Released v2.4.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n016.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 00:22:26 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.41 % SZS status Theorem % 0.12/0.41 (* PROOF-FOUND *) % 0.12/0.41 (* BEGIN-PROOF *) % 0.12/0.41 % SZS output start Proof % 0.12/0.41 1. (hollywood T_0) (-. (hollywood T_0)) ### Axiom % 0.12/0.41 2. (city T_0) (-. (city T_0)) ### Axiom % 0.12/0.41 3. (event T_1) (-. (event T_1)) ### Axiom % 0.12/0.41 4. (chevy T_2) (-. (chevy T_2)) ### Axiom % 0.12/0.41 5. (car T_2) (-. (car T_2)) ### Axiom % 0.12/0.41 6. (white T_2) (-. (white T_2)) ### Axiom % 0.12/0.41 7. (dirty T_2) (-. (dirty T_2)) ### Axiom % 0.12/0.41 8. (old T_2) (-. (old T_2)) ### Axiom % 0.12/0.41 9. (street T_3) (-. (street T_3)) ### Axiom % 0.12/0.41 10. (way T_3) (-. (way T_3)) ### Axiom % 0.12/0.41 11. (lonely T_3) (-. (lonely T_3)) ### Axiom % 0.12/0.41 12. (barrel T_1 T_2) (-. (barrel T_1 T_2)) ### Axiom % 0.12/0.41 13. (down T_1 T_3) (-. (down T_1 T_3)) ### Axiom % 0.12/0.41 14. (in T_1 T_0) (-. (in T_1 T_0)) ### Axiom % 0.12/0.41 15. (-. ((hollywood T_0) /\ ((city T_0) /\ ((event T_1) /\ ((chevy T_2) /\ ((car T_2) /\ ((white T_2) /\ ((dirty T_2) /\ ((old T_2) /\ ((street T_3) /\ ((way T_3) /\ ((lonely T_3) /\ ((barrel T_1 T_2) /\ ((down T_1 T_3) /\ (in T_1 T_0))))))))))))))) (in T_1 T_0) (down T_1 T_3) (barrel T_1 T_2) (lonely T_3) (way T_3) (street T_3) (old T_2) (dirty T_2) (white T_2) (car T_2) (chevy T_2) (event T_1) (city T_0) (hollywood T_0) ### DisjTree 1 2 3 4 5 6 7 8 9 10 11 12 13 14 % 0.12/0.41 16. (-. (Ex X2, ((hollywood T_0) /\ ((city T_0) /\ ((event T_1) /\ ((chevy T_2) /\ ((car T_2) /\ ((white T_2) /\ ((dirty T_2) /\ ((old T_2) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel T_1 T_2) /\ ((down T_1 X2) /\ (in T_1 T_0)))))))))))))))) (hollywood T_0) (city T_0) (event T_1) (chevy T_2) (car T_2) (white T_2) (dirty T_2) (old T_2) (street T_3) (way T_3) (lonely T_3) (barrel T_1 T_2) (down T_1 T_3) (in T_1 T_0) ### NotExists 15 % 0.12/0.41 17. (-. (Ex X1, (Ex X2, ((hollywood T_0) /\ ((city T_0) /\ ((event T_1) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel T_1 X1) /\ ((down T_1 X2) /\ (in T_1 T_0))))))))))))))))) (in T_1 T_0) (down T_1 T_3) (barrel T_1 T_2) (lonely T_3) (way T_3) (street T_3) (old T_2) (dirty T_2) (white T_2) (car T_2) (chevy T_2) (event T_1) (city T_0) (hollywood T_0) ### NotExists 16 % 0.12/0.41 18. (-. (Ex Z, (Ex X1, (Ex X2, ((hollywood T_0) /\ ((city T_0) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z T_0)))))))))))))))))) (hollywood T_0) (city T_0) (event T_1) (chevy T_2) (car T_2) (white T_2) (dirty T_2) (old T_2) (street T_3) (way T_3) (lonely T_3) (barrel T_1 T_2) (down T_1 T_3) (in T_1 T_0) ### NotExists 17 % 0.12/0.41 19. (-. (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y))))))))))))))))))) (in T_1 T_0) (down T_1 T_3) (barrel T_1 T_2) (lonely T_3) (way T_3) (street T_3) (old T_2) (dirty T_2) (white T_2) (car T_2) (chevy T_2) (event T_1) (city T_0) (hollywood T_0) ### NotExists 18 % 0.12/0.41 20. ((hollywood T_0) /\ ((city T_0) /\ ((event T_1) /\ ((street T_3) /\ ((way T_3) /\ ((lonely T_3) /\ ((chevy T_2) /\ ((car T_2) /\ ((white T_2) /\ ((dirty T_2) /\ ((old T_2) /\ ((barrel T_1 T_2) /\ ((down T_1 T_3) /\ (in T_1 T_0)))))))))))))) (-. (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y))))))))))))))))))) ### ConjTree 19 % 0.12/0.41 21. (Ex X, ((hollywood T_0) /\ ((city T_0) /\ ((event T_1) /\ ((street T_3) /\ ((way T_3) /\ ((lonely T_3) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel T_1 X) /\ ((down T_1 T_3) /\ (in T_1 T_0))))))))))))))) (-. (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y))))))))))))))))))) ### Exists 20 % 0.12/0.41 22. (Ex W, (Ex X, ((hollywood T_0) /\ ((city T_0) /\ ((event T_1) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel T_1 X) /\ ((down T_1 W) /\ (in T_1 T_0)))))))))))))))) (-. (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y))))))))))))))))))) ### Exists 21 % 0.12/0.41 23. (Ex V, (Ex W, (Ex X, ((hollywood T_0) /\ ((city T_0) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V T_0))))))))))))))))) (-. (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y))))))))))))))))))) ### Exists 22 % 0.12/0.41 24. (Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U)))))))))))))))))) (-. (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y))))))))))))))))))) ### Exists 23 % 0.12/0.41 25. (-. ((Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U)))))))))))))))))) => (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y)))))))))))))))))))) ### NotImply 24 % 0.12/0.41 26. (hollywood T_4) (-. (hollywood T_4)) ### Axiom % 0.12/0.41 27. (city T_4) (-. (city T_4)) ### Axiom % 0.12/0.41 28. (event T_5) (-. (event T_5)) ### Axiom % 0.12/0.41 29. (street T_6) (-. (street T_6)) ### Axiom % 0.12/0.41 30. (way T_6) (-. (way T_6)) ### Axiom % 0.12/0.41 31. (lonely T_6) (-. (lonely T_6)) ### Axiom % 0.12/0.41 32. (chevy T_7) (-. (chevy T_7)) ### Axiom % 0.12/0.41 33. (car T_7) (-. (car T_7)) ### Axiom % 0.12/0.41 34. (white T_7) (-. (white T_7)) ### Axiom % 0.12/0.41 35. (dirty T_7) (-. (dirty T_7)) ### Axiom % 0.12/0.41 36. (old T_7) (-. (old T_7)) ### Axiom % 0.12/0.41 37. (barrel T_5 T_7) (-. (barrel T_5 T_7)) ### Axiom % 0.12/0.41 38. (down T_5 T_6) (-. (down T_5 T_6)) ### Axiom % 0.12/0.41 39. (in T_5 T_4) (-. (in T_5 T_4)) ### Axiom % 0.12/0.41 40. (-. ((hollywood T_4) /\ ((city T_4) /\ ((event T_5) /\ ((street T_6) /\ ((way T_6) /\ ((lonely T_6) /\ ((chevy T_7) /\ ((car T_7) /\ ((white T_7) /\ ((dirty T_7) /\ ((old T_7) /\ ((barrel T_5 T_7) /\ ((down T_5 T_6) /\ (in T_5 T_4))))))))))))))) (in T_5 T_4) (down T_5 T_6) (barrel T_5 T_7) (old T_7) (dirty T_7) (white T_7) (car T_7) (chevy T_7) (lonely T_6) (way T_6) (street T_6) (event T_5) (city T_4) (hollywood T_4) ### DisjTree 26 27 28 29 30 31 32 33 34 35 36 37 38 39 % 0.12/0.41 41. (-. (Ex X, ((hollywood T_4) /\ ((city T_4) /\ ((event T_5) /\ ((street T_6) /\ ((way T_6) /\ ((lonely T_6) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel T_5 X) /\ ((down T_5 T_6) /\ (in T_5 T_4)))))))))))))))) (hollywood T_4) (city T_4) (event T_5) (street T_6) (way T_6) (lonely T_6) (chevy T_7) (car T_7) (white T_7) (dirty T_7) (old T_7) (barrel T_5 T_7) (down T_5 T_6) (in T_5 T_4) ### NotExists 40 % 0.12/0.41 42. (-. (Ex W, (Ex X, ((hollywood T_4) /\ ((city T_4) /\ ((event T_5) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel T_5 X) /\ ((down T_5 W) /\ (in T_5 T_4))))))))))))))))) (in T_5 T_4) (down T_5 T_6) (barrel T_5 T_7) (old T_7) (dirty T_7) (white T_7) (car T_7) (chevy T_7) (lonely T_6) (way T_6) (street T_6) (event T_5) (city T_4) (hollywood T_4) ### NotExists 41 % 0.12/0.41 43. (-. (Ex V, (Ex W, (Ex X, ((hollywood T_4) /\ ((city T_4) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V T_4)))))))))))))))))) (hollywood T_4) (city T_4) (event T_5) (street T_6) (way T_6) (lonely T_6) (chevy T_7) (car T_7) (white T_7) (dirty T_7) (old T_7) (barrel T_5 T_7) (down T_5 T_6) (in T_5 T_4) ### NotExists 42 % 0.18/0.41 44. (-. (Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U))))))))))))))))))) (in T_5 T_4) (down T_5 T_6) (barrel T_5 T_7) (old T_7) (dirty T_7) (white T_7) (car T_7) (chevy T_7) (lonely T_6) (way T_6) (street T_6) (event T_5) (city T_4) (hollywood T_4) ### NotExists 43 % 0.18/0.41 45. ((hollywood T_4) /\ ((city T_4) /\ ((event T_5) /\ ((chevy T_7) /\ ((car T_7) /\ ((white T_7) /\ ((dirty T_7) /\ ((old T_7) /\ ((street T_6) /\ ((way T_6) /\ ((lonely T_6) /\ ((barrel T_5 T_7) /\ ((down T_5 T_6) /\ (in T_5 T_4)))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U))))))))))))))))))) ### ConjTree 44 % 0.18/0.41 46. (Ex X2, ((hollywood T_4) /\ ((city T_4) /\ ((event T_5) /\ ((chevy T_7) /\ ((car T_7) /\ ((white T_7) /\ ((dirty T_7) /\ ((old T_7) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel T_5 T_7) /\ ((down T_5 X2) /\ (in T_5 T_4))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U))))))))))))))))))) ### Exists 45 % 0.18/0.41 47. (Ex X1, (Ex X2, ((hollywood T_4) /\ ((city T_4) /\ ((event T_5) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel T_5 X1) /\ ((down T_5 X2) /\ (in T_5 T_4)))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U))))))))))))))))))) ### Exists 46 % 0.18/0.41 48. (Ex Z, (Ex X1, (Ex X2, ((hollywood T_4) /\ ((city T_4) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z T_4))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U))))))))))))))))))) ### Exists 47 % 0.18/0.41 49. (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y)))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U))))))))))))))))))) ### Exists 48 % 0.18/0.41 50. (-. ((Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y)))))))))))))))))) => (Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U)))))))))))))))))))) ### NotImply 49 % 0.18/0.41 51. (-. (((Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U)))))))))))))))))) => (Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y))))))))))))))))))) /\ ((Ex Y, (Ex Z, (Ex X1, (Ex X2, ((hollywood Y) /\ ((city Y) /\ ((event Z) /\ ((chevy X1) /\ ((car X1) /\ ((white X1) /\ ((dirty X1) /\ ((old X1) /\ ((street X2) /\ ((way X2) /\ ((lonely X2) /\ ((barrel Z X1) /\ ((down Z X2) /\ (in Z Y)))))))))))))))))) => (Ex U, (Ex V, (Ex W, (Ex X, ((hollywood U) /\ ((city U) /\ ((event V) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel V X) /\ ((down V W) /\ (in V U))))))))))))))))))))) ### NotAnd 25 50 % 0.18/0.41 % SZS output end Proof % 0.18/0.41 (* END-PROOF *) %------------------------------------------------------------------------------