%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NLP009+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 : n018.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:10 EDT 2022 % Result : Theorem 11.81s 11.99s % Output : Proof 11.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : NLP009+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.11/0.33 % Computer : n018.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Fri Jul 1 00:43:32 EDT 2022 % 0.11/0.33 % CPUTime : % 11.81/11.99 % SZS status Theorem % 11.81/11.99 (* PROOF-FOUND *) % 11.81/11.99 (* BEGIN-PROOF *) % 11.81/11.99 % SZS output start Proof % 11.81/11.99 1. (hollywood T_0) (-. (hollywood T_0)) ### Axiom % 11.81/11.99 2. (city T_0) (-. (city T_0)) ### Axiom % 11.81/11.99 3. (event T_1) (-. (event T_1)) ### Axiom % 11.81/11.99 4. (chevy T_2) (-. (chevy T_2)) ### Axiom % 11.81/11.99 5. (car T_2) (-. (car T_2)) ### Axiom % 11.81/11.99 6. (white T_2) (-. (white T_2)) ### Axiom % 11.81/11.99 7. (dirty T_2) (-. (dirty T_2)) ### Axiom % 11.81/11.99 8. (old T_2) (-. (old T_2)) ### Axiom % 11.81/11.99 9. (street T_3) (-. (street T_3)) ### Axiom % 11.81/11.99 10. (way T_3) (-. (way T_3)) ### Axiom % 11.81/11.99 11. (lonely T_3) (-. (lonely T_3)) ### Axiom % 11.81/11.99 12. (barrel T_1 T_2) (-. (barrel T_1 T_2)) ### Axiom % 11.81/11.99 13. (down T_1 T_3) (-. (down T_1 T_3)) ### Axiom % 11.81/11.99 14. (in T_1 T_0) (-. (in T_1 T_0)) ### Axiom % 11.81/11.99 15. (seat T_4) (-. (seat T_4)) ### Axiom % 11.81/11.99 16. (furniture T_4) (-. (furniture T_4)) ### Axiom % 11.81/11.99 17. (front T_4) (-. (front T_4)) ### Axiom % 11.81/11.99 18. (T_5 != T_6) (T_6 = T_5) ### Sym(=) % 11.81/11.99 19. (fellow T_6) (-. (fellow T_6)) ### Axiom % 11.81/11.99 20. (man T_6) (-. (man T_6)) ### Axiom % 11.81/11.99 21. (young T_6) (-. (young T_6)) ### Axiom % 11.81/11.99 22. (fellow T_5) (-. (fellow T_5)) ### Axiom % 11.81/11.99 23. (man T_5) (-. (man T_5)) ### Axiom % 11.81/11.99 24. (young T_5) (-. (young T_5)) ### Axiom % 11.81/11.99 25. (T_6 = T_7) (T_6 != T_7) ### Axiom % 11.81/11.99 26. (in T_7 T_4) (-. (in T_7 T_4)) ### Axiom % 11.81/11.99 27. (T_5 = T_8) (T_5 != T_8) ### Axiom % 11.81/11.99 28. (in T_8 T_4) (-. (in T_8 T_4)) ### Axiom % 11.81/11.99 29. (-. ((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) /\ ((seat T_4) /\ ((furniture T_4) /\ ((front T_4) /\ ((T_6 != T_5) /\ ((fellow T_6) /\ ((man T_6) /\ ((young T_6) /\ ((fellow T_5) /\ ((man T_5) /\ ((young T_5) /\ ((T_6 = T_7) /\ ((in T_7 T_4) /\ ((T_5 = T_8) /\ (in T_8 T_4))))))))))))))))))))))))))))) (in T_8 T_4) (T_5 = T_8) (in T_7 T_4) (T_6 = T_7) (young T_5) (man T_5) (fellow T_5) (young T_6) (man T_6) (fellow T_6) (T_5 != T_6) (front T_4) (furniture T_4) (seat T_4) (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 15 16 17 18 19 20 21 22 23 24 25 26 27 28 % 11.81/11.99 30. (-. (Ex X12, ((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) /\ ((seat T_4) /\ ((furniture T_4) /\ ((front T_4) /\ ((T_6 != T_5) /\ ((fellow T_6) /\ ((man T_6) /\ ((young T_6) /\ ((fellow T_5) /\ ((man T_5) /\ ((young T_5) /\ ((T_6 = T_7) /\ ((in T_7 T_4) /\ ((T_5 = X12) /\ (in X12 T_4)))))))))))))))))))))))))))))) (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) (seat T_4) (furniture T_4) (front T_4) (T_5 != T_6) (fellow T_6) (man T_6) (young T_6) (fellow T_5) (man T_5) (young T_5) (T_6 = T_7) (in T_7 T_4) (T_5 = T_8) (in T_8 T_4) ### NotExists 29 % 11.81/11.99 31. (-. (Ex X11, (Ex X12, ((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) /\ ((seat T_4) /\ ((furniture T_4) /\ ((front T_4) /\ ((T_6 != T_5) /\ ((fellow T_6) /\ ((man T_6) /\ ((young T_6) /\ ((fellow T_5) /\ ((man T_5) /\ ((young T_5) /\ ((T_6 = X11) /\ ((in X11 T_4) /\ ((T_5 = X12) /\ (in X12 T_4))))))))))))))))))))))))))))))) (in T_8 T_4) (T_5 = T_8) (in T_7 T_4) (T_6 = T_7) (young T_5) (man T_5) (fellow T_5) (young T_6) (man T_6) (fellow T_6) (T_5 != T_6) (front T_4) (furniture T_4) (seat T_4) (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 30 % 11.81/11.99 32. (-. (Ex X10, (Ex X11, (Ex X12, ((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) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((T_6 != T_5) /\ ((fellow T_6) /\ ((man T_6) /\ ((young T_6) /\ ((fellow T_5) /\ ((man T_5) /\ ((young T_5) /\ ((T_6 = X11) /\ ((in X11 X10) /\ ((T_5 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))) (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) (seat T_4) (furniture T_4) (front T_4) (T_5 != T_6) (fellow T_6) (man T_6) (young T_6) (fellow T_5) (man T_5) (young T_5) (T_6 = T_7) (in T_7 T_4) (T_5 = T_8) (in T_8 T_4) ### NotExists 31 % 11.81/11.99 33. (-. (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((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) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((T_6 != X9) /\ ((fellow T_6) /\ ((man T_6) /\ ((young T_6) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((T_6 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10))))))))))))))))))))))))))))))))) (in T_8 T_4) (T_5 = T_8) (in T_7 T_4) (T_6 = T_7) (young T_5) (man T_5) (fellow T_5) (young T_6) (man T_6) (fellow T_6) (T_5 != T_6) (front T_4) (furniture T_4) (seat T_4) (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 32 % 11.81/11.99 34. (-. (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((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) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))) (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) (seat T_4) (furniture T_4) (front T_4) (T_5 != T_6) (fellow T_6) (man T_6) (young T_6) (fellow T_5) (man T_5) (young T_5) (T_6 = T_7) (in T_7 T_4) (T_5 = T_8) (in T_8 T_4) ### NotExists 33 % 11.81/11.99 35. (-. (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((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 X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel T_1 T_2) /\ ((down T_1 X7) /\ ((in T_1 T_0) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10))))))))))))))))))))))))))))))))))) (in T_8 T_4) (T_5 = T_8) (in T_7 T_4) (T_6 = T_7) (young T_5) (man T_5) (fellow T_5) (young T_6) (man T_6) (fellow T_6) (T_5 != T_6) (front T_4) (furniture T_4) (seat T_4) (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 34 % 11.81/11.99 36. (-. (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood T_0) /\ ((city T_0) /\ ((event T_1) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel T_1 X6) /\ ((down T_1 X7) /\ ((in T_1 T_0) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))) (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) (seat T_4) (furniture T_4) (front T_4) (T_5 != T_6) (fellow T_6) (man T_6) (young T_6) (fellow T_5) (man T_5) (young T_5) (T_6 = T_7) (in T_7 T_4) (T_5 = T_8) (in T_8 T_4) ### NotExists 35 % 11.81/12.00 37. (-. (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood T_0) /\ ((city T_0) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 T_0) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10))))))))))))))))))))))))))))))))))))) (in T_8 T_4) (T_5 = T_8) (in T_7 T_4) (T_6 = T_7) (young T_5) (man T_5) (fellow T_5) (young T_6) (man T_6) (fellow T_6) (T_5 != T_6) (front T_4) (furniture T_4) (seat T_4) (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 36 % 11.81/12.00 38. (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) (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) (seat T_4) (furniture T_4) (front T_4) (T_5 != T_6) (fellow T_6) (man T_6) (young T_6) (fellow T_5) (man T_5) (young T_5) (T_6 = T_7) (in T_7 T_4) (T_5 = T_8) (in T_8 T_4) ### NotExists 37 % 11.81/12.00 39. ((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) /\ ((seat T_4) /\ ((furniture T_4) /\ ((front T_4) /\ ((T_5 != T_6) /\ ((fellow T_5) /\ ((man T_5) /\ ((young T_5) /\ ((fellow T_6) /\ ((man T_6) /\ ((young T_6) /\ ((T_5 = T_8) /\ ((in T_8 T_4) /\ ((T_6 = T_7) /\ (in T_7 T_4)))))))))))))))))))))))))))) (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) ### ConjTree 38 % 11.81/12.00 40. (Ex X3, ((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) /\ ((seat T_4) /\ ((furniture T_4) /\ ((front T_4) /\ ((T_5 != T_6) /\ ((fellow T_5) /\ ((man T_5) /\ ((young T_5) /\ ((fellow T_6) /\ ((man T_6) /\ ((young T_6) /\ ((T_5 = T_8) /\ ((in T_8 T_4) /\ ((T_6 = X3) /\ (in X3 T_4))))))))))))))))))))))))))))) (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) ### Exists 39 % 11.81/12.00 41. (Ex X2, (Ex X3, ((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) /\ ((seat T_4) /\ ((furniture T_4) /\ ((front T_4) /\ ((T_5 != T_6) /\ ((fellow T_5) /\ ((man T_5) /\ ((young T_5) /\ ((fellow T_6) /\ ((man T_6) /\ ((young T_6) /\ ((T_5 = X2) /\ ((in X2 T_4) /\ ((T_6 = X3) /\ (in X3 T_4)))))))))))))))))))))))))))))) (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) ### Exists 40 % 11.81/12.00 42. (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((T_5 != T_6) /\ ((fellow T_5) /\ ((man T_5) /\ ((young T_5) /\ ((fellow T_6) /\ ((man T_6) /\ ((young T_6) /\ ((T_5 = X2) /\ ((in X2 X1) /\ ((T_6 = X3) /\ (in X3 X1))))))))))))))))))))))))))))))) (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) ### Exists 41 % 11.81/12.00 43. (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((T_5 != Z) /\ ((fellow T_5) /\ ((man T_5) /\ ((young T_5) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((T_5 = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))) (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) ### Exists 42 % 11.81/12.00 44. (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1))))))))))))))))))))))))))))))))) (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) ### Exists 43 % 11.81/12.00 45. (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))) (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) ### Exists 44 % 11.81/12.00 46. (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1))))))))))))))))))))))))))))))))))) (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) ### Exists 45 % 11.81/12.00 47. (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))) (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) ### Exists 46 % 11.81/12.00 48. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1))))))))))))))))))))))))))))))))))))) (-. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) ### Exists 47 % 11.81/12.00 49. (-. ((Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1))))))))))))))))))))))))))))))))))))) => (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10))))))))))))))))))))))))))))))))))))))) ### NotImply 48 % 11.81/12.00 50. (hollywood T_9) (-. (hollywood T_9)) ### Axiom % 11.81/12.00 51. (city T_9) (-. (city T_9)) ### Axiom % 11.81/12.00 52. (event T_10) (-. (event T_10)) ### Axiom % 11.81/12.00 53. (street T_11) (-. (street T_11)) ### Axiom % 11.81/12.00 54. (way T_11) (-. (way T_11)) ### Axiom % 11.81/12.00 55. (lonely T_11) (-. (lonely T_11)) ### Axiom % 11.81/12.00 56. (chevy T_12) (-. (chevy T_12)) ### Axiom % 11.81/12.00 57. (car T_12) (-. (car T_12)) ### Axiom % 11.81/12.00 58. (white T_12) (-. (white T_12)) ### Axiom % 11.81/12.00 59. (dirty T_12) (-. (dirty T_12)) ### Axiom % 11.81/12.00 60. (old T_12) (-. (old T_12)) ### Axiom % 11.81/12.00 61. (barrel T_10 T_12) (-. (barrel T_10 T_12)) ### Axiom % 11.81/12.00 62. (down T_10 T_11) (-. (down T_10 T_11)) ### Axiom % 11.81/12.00 63. (in T_10 T_9) (-. (in T_10 T_9)) ### Axiom % 11.81/12.00 64. (seat T_13) (-. (seat T_13)) ### Axiom % 11.81/12.00 65. (furniture T_13) (-. (furniture T_13)) ### Axiom % 11.81/12.00 66. (front T_13) (-. (front T_13)) ### Axiom % 11.81/12.00 67. (T_14 != T_15) (T_15 = T_14) ### Sym(=) % 11.81/12.00 68. (fellow T_15) (-. (fellow T_15)) ### Axiom % 11.81/12.00 69. (man T_15) (-. (man T_15)) ### Axiom % 11.81/12.00 70. (young T_15) (-. (young T_15)) ### Axiom % 11.81/12.00 71. (fellow T_14) (-. (fellow T_14)) ### Axiom % 11.81/12.00 72. (man T_14) (-. (man T_14)) ### Axiom % 11.81/12.00 73. (young T_14) (-. (young T_14)) ### Axiom % 11.81/12.00 74. (T_15 = T_16) (T_15 != T_16) ### Axiom % 11.81/12.00 75. (in T_16 T_13) (-. (in T_16 T_13)) ### Axiom % 11.81/12.00 76. (T_14 = T_17) (T_14 != T_17) ### Axiom % 11.81/12.00 77. (in T_17 T_13) (-. (in T_17 T_13)) ### Axiom % 11.81/12.00 78. (-. ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat T_13) /\ ((furniture T_13) /\ ((front T_13) /\ ((T_15 != T_14) /\ ((fellow T_15) /\ ((man T_15) /\ ((young T_15) /\ ((fellow T_14) /\ ((man T_14) /\ ((young T_14) /\ ((T_15 = T_16) /\ ((in T_16 T_13) /\ ((T_14 = T_17) /\ (in T_17 T_13))))))))))))))))))))))))))))) (in T_17 T_13) (T_14 = T_17) (in T_16 T_13) (T_15 = T_16) (young T_14) (man T_14) (fellow T_14) (young T_15) (man T_15) (fellow T_15) (T_14 != T_15) (front T_13) (furniture T_13) (seat T_13) (in T_10 T_9) (down T_10 T_11) (barrel T_10 T_12) (old T_12) (dirty T_12) (white T_12) (car T_12) (chevy T_12) (lonely T_11) (way T_11) (street T_11) (event T_10) (city T_9) (hollywood T_9) ### DisjTree 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 % 11.81/12.00 79. (-. (Ex X3, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat T_13) /\ ((furniture T_13) /\ ((front T_13) /\ ((T_15 != T_14) /\ ((fellow T_15) /\ ((man T_15) /\ ((young T_15) /\ ((fellow T_14) /\ ((man T_14) /\ ((young T_14) /\ ((T_15 = T_16) /\ ((in T_16 T_13) /\ ((T_14 = X3) /\ (in X3 T_13)))))))))))))))))))))))))))))) (hollywood T_9) (city T_9) (event T_10) (street T_11) (way T_11) (lonely T_11) (chevy T_12) (car T_12) (white T_12) (dirty T_12) (old T_12) (barrel T_10 T_12) (down T_10 T_11) (in T_10 T_9) (seat T_13) (furniture T_13) (front T_13) (T_14 != T_15) (fellow T_15) (man T_15) (young T_15) (fellow T_14) (man T_14) (young T_14) (T_15 = T_16) (in T_16 T_13) (T_14 = T_17) (in T_17 T_13) ### NotExists 78 % 11.84/12.01 80. (-. (Ex X2, (Ex X3, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat T_13) /\ ((furniture T_13) /\ ((front T_13) /\ ((T_15 != T_14) /\ ((fellow T_15) /\ ((man T_15) /\ ((young T_15) /\ ((fellow T_14) /\ ((man T_14) /\ ((young T_14) /\ ((T_15 = X2) /\ ((in X2 T_13) /\ ((T_14 = X3) /\ (in X3 T_13))))))))))))))))))))))))))))))) (in T_17 T_13) (T_14 = T_17) (in T_16 T_13) (T_15 = T_16) (young T_14) (man T_14) (fellow T_14) (young T_15) (man T_15) (fellow T_15) (T_14 != T_15) (front T_13) (furniture T_13) (seat T_13) (in T_10 T_9) (down T_10 T_11) (barrel T_10 T_12) (old T_12) (dirty T_12) (white T_12) (car T_12) (chevy T_12) (lonely T_11) (way T_11) (street T_11) (event T_10) (city T_9) (hollywood T_9) ### NotExists 79 % 11.84/12.01 81. (-. (Ex X1, (Ex X2, (Ex X3, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((T_15 != T_14) /\ ((fellow T_15) /\ ((man T_15) /\ ((young T_15) /\ ((fellow T_14) /\ ((man T_14) /\ ((young T_14) /\ ((T_15 = X2) /\ ((in X2 X1) /\ ((T_14 = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))) (hollywood T_9) (city T_9) (event T_10) (street T_11) (way T_11) (lonely T_11) (chevy T_12) (car T_12) (white T_12) (dirty T_12) (old T_12) (barrel T_10 T_12) (down T_10 T_11) (in T_10 T_9) (seat T_13) (furniture T_13) (front T_13) (T_14 != T_15) (fellow T_15) (man T_15) (young T_15) (fellow T_14) (man T_14) (young T_14) (T_15 = T_16) (in T_16 T_13) (T_14 = T_17) (in T_17 T_13) ### NotExists 80 % 11.84/12.01 82. (-. (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((T_15 != Z) /\ ((fellow T_15) /\ ((man T_15) /\ ((young T_15) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((T_15 = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1))))))))))))))))))))))))))))))))) (in T_17 T_13) (T_14 = T_17) (in T_16 T_13) (T_15 = T_16) (young T_14) (man T_14) (fellow T_14) (young T_15) (man T_15) (fellow T_15) (T_14 != T_15) (front T_13) (furniture T_13) (seat T_13) (in T_10 T_9) (down T_10 T_11) (barrel T_10 T_12) (old T_12) (dirty T_12) (white T_12) (car T_12) (chevy T_12) (lonely T_11) (way T_11) (street T_11) (event T_10) (city T_9) (hollywood T_9) ### NotExists 81 % 11.84/12.01 83. (-. (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))) (hollywood T_9) (city T_9) (event T_10) (street T_11) (way T_11) (lonely T_11) (chevy T_12) (car T_12) (white T_12) (dirty T_12) (old T_12) (barrel T_10 T_12) (down T_10 T_11) (in T_10 T_9) (seat T_13) (furniture T_13) (front T_13) (T_14 != T_15) (fellow T_15) (man T_15) (young T_15) (fellow T_14) (man T_14) (young T_14) (T_15 = T_16) (in T_16 T_13) (T_14 = T_17) (in T_17 T_13) ### NotExists 82 % 11.84/12.01 84. (-. (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel T_10 X) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1))))))))))))))))))))))))))))))))))) (in T_17 T_13) (T_14 = T_17) (in T_16 T_13) (T_15 = T_16) (young T_14) (man T_14) (fellow T_14) (young T_15) (man T_15) (fellow T_15) (T_14 != T_15) (front T_13) (furniture T_13) (seat T_13) (in T_10 T_9) (down T_10 T_11) (barrel T_10 T_12) (old T_12) (dirty T_12) (white T_12) (car T_12) (chevy T_12) (lonely T_11) (way T_11) (street T_11) (event T_10) (city T_9) (hollywood T_9) ### NotExists 83 % 11.84/12.01 85. (-. (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((street W) /\ ((way W) /\ ((lonely W) /\ ((chevy X) /\ ((car X) /\ ((white X) /\ ((dirty X) /\ ((old X) /\ ((barrel T_10 X) /\ ((down T_10 W) /\ ((in T_10 T_9) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))) (hollywood T_9) (city T_9) (event T_10) (street T_11) (way T_11) (lonely T_11) (chevy T_12) (car T_12) (white T_12) (dirty T_12) (old T_12) (barrel T_10 T_12) (down T_10 T_11) (in T_10 T_9) (seat T_13) (furniture T_13) (front T_13) (T_14 != T_15) (fellow T_15) (man T_15) (young T_15) (fellow T_14) (man T_14) (young T_14) (T_15 = T_16) (in T_16 T_13) (T_14 = T_17) (in T_17 T_13) ### NotExists 84 % 11.84/12.01 86. (-. (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((hollywood T_9) /\ ((city T_9) /\ ((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_9) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1))))))))))))))))))))))))))))))))))))) (in T_17 T_13) (T_14 = T_17) (in T_16 T_13) (T_15 = T_16) (young T_14) (man T_14) (fellow T_14) (young T_15) (man T_15) (fellow T_15) (T_14 != T_15) (front T_13) (furniture T_13) (seat T_13) (in T_10 T_9) (down T_10 T_11) (barrel T_10 T_12) (old T_12) (dirty T_12) (white T_12) (car T_12) (chevy T_12) (lonely T_11) (way T_11) (street T_11) (event T_10) (city T_9) (hollywood T_9) ### NotExists 85 % 11.84/12.01 87. (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) (hollywood T_9) (city T_9) (event T_10) (street T_11) (way T_11) (lonely T_11) (chevy T_12) (car T_12) (white T_12) (dirty T_12) (old T_12) (barrel T_10 T_12) (down T_10 T_11) (in T_10 T_9) (seat T_13) (furniture T_13) (front T_13) (T_14 != T_15) (fellow T_15) (man T_15) (young T_15) (fellow T_14) (man T_14) (young T_14) (T_15 = T_16) (in T_16 T_13) (T_14 = T_17) (in T_17 T_13) ### NotExists 86 % 11.84/12.01 88. ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat T_13) /\ ((furniture T_13) /\ ((front T_13) /\ ((T_14 != T_15) /\ ((fellow T_14) /\ ((man T_14) /\ ((young T_14) /\ ((fellow T_15) /\ ((man T_15) /\ ((young T_15) /\ ((T_14 = T_17) /\ ((in T_17 T_13) /\ ((T_15 = T_16) /\ (in T_16 T_13)))))))))))))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) ### ConjTree 87 % 11.84/12.01 89. (Ex X12, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat T_13) /\ ((furniture T_13) /\ ((front T_13) /\ ((T_14 != T_15) /\ ((fellow T_14) /\ ((man T_14) /\ ((young T_14) /\ ((fellow T_15) /\ ((man T_15) /\ ((young T_15) /\ ((T_14 = T_17) /\ ((in T_17 T_13) /\ ((T_15 = X12) /\ (in X12 T_13))))))))))))))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) ### Exists 88 % 11.84/12.01 90. (Ex X11, (Ex X12, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat T_13) /\ ((furniture T_13) /\ ((front T_13) /\ ((T_14 != T_15) /\ ((fellow T_14) /\ ((man T_14) /\ ((young T_14) /\ ((fellow T_15) /\ ((man T_15) /\ ((young T_15) /\ ((T_14 = X11) /\ ((in X11 T_13) /\ ((T_15 = X12) /\ (in X12 T_13)))))))))))))))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) ### Exists 89 % 11.84/12.01 91. (Ex X10, (Ex X11, (Ex X12, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((T_14 != T_15) /\ ((fellow T_14) /\ ((man T_14) /\ ((young T_14) /\ ((fellow T_15) /\ ((man T_15) /\ ((young T_15) /\ ((T_14 = X11) /\ ((in X11 X10) /\ ((T_15 = X12) /\ (in X12 X10))))))))))))))))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) ### Exists 90 % 11.84/12.01 92. (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((T_14 != X9) /\ ((fellow T_14) /\ ((man T_14) /\ ((young T_14) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((T_14 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) ### Exists 91 % 11.84/12.01 93. (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((street T_11) /\ ((way T_11) /\ ((lonely T_11) /\ ((barrel T_10 T_12) /\ ((down T_10 T_11) /\ ((in T_10 T_9) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10))))))))))))))))))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) ### Exists 92 % 11.84/12.01 94. (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((chevy T_12) /\ ((car T_12) /\ ((white T_12) /\ ((dirty T_12) /\ ((old T_12) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel T_10 T_12) /\ ((down T_10 X7) /\ ((in T_10 T_9) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) ### Exists 93 % 11.84/12.01 95. (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood T_9) /\ ((city T_9) /\ ((event T_10) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel T_10 X6) /\ ((down T_10 X7) /\ ((in T_10 T_9) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10))))))))))))))))))))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) ### Exists 94 % 11.84/12.01 96. (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood T_9) /\ ((city T_9) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 T_9) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) ### Exists 95 % 11.84/12.01 97. (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10))))))))))))))))))))))))))))))))))))) (-. (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))) ### Exists 96 % 11.84/12.01 98. (-. ((Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10))))))))))))))))))))))))))))))))))))) => (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1))))))))))))))))))))))))))))))))))))))) ### NotImply 97 % 11.84/12.01 99. (-. (((Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1))))))))))))))))))))))))))))))))))))) => (Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10)))))))))))))))))))))))))))))))))))))) /\ ((Ex X4, (Ex X5, (Ex X6, (Ex X7, (Ex X8, (Ex X9, (Ex X10, (Ex X11, (Ex X12, ((hollywood X4) /\ ((city X4) /\ ((event X5) /\ ((chevy X6) /\ ((car X6) /\ ((white X6) /\ ((dirty X6) /\ ((old X6) /\ ((street X7) /\ ((way X7) /\ ((lonely X7) /\ ((barrel X5 X6) /\ ((down X5 X7) /\ ((in X5 X4) /\ ((seat X10) /\ ((furniture X10) /\ ((front X10) /\ ((X8 != X9) /\ ((fellow X8) /\ ((man X8) /\ ((young X8) /\ ((fellow X9) /\ ((man X9) /\ ((young X9) /\ ((X8 = X11) /\ ((in X11 X10) /\ ((X9 = X12) /\ (in X12 X10))))))))))))))))))))))))))))))))))))) => (Ex U, (Ex V, (Ex W, (Ex X, (Ex Y, (Ex Z, (Ex X1, (Ex X2, (Ex X3, ((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) /\ ((seat X1) /\ ((furniture X1) /\ ((front X1) /\ ((Y != Z) /\ ((fellow Y) /\ ((man Y) /\ ((young Y) /\ ((fellow Z) /\ ((man Z) /\ ((young Z) /\ ((Y = X2) /\ ((in X2 X1) /\ ((Z = X3) /\ (in X3 X1)))))))))))))))))))))))))))))))))))))))) ### NotAnd 49 98 % 11.84/12.01 % SZS output end Proof % 11.84/12.01 (* END-PROOF *) %------------------------------------------------------------------------------