%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : CSR034+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n026.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 : Fri Jul 15 23:29:08 EDT 2022 % Result : Theorem 4.93s 5.21s % Output : Proof 4.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.13 % Problem : CSR034+1 : TPTP v8.1.0. Released v3.4.0. % 0.09/0.14 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.35 % Computer : n026.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sat Jun 11 19:23:04 EDT 2022 % 0.13/0.35 % CPUTime : % 4.93/5.21 % SZS status Theorem % 4.93/5.21 (* PROOF-FOUND *) % 4.93/5.21 (* BEGIN-PROOF *) % 4.93/5.21 % SZS output start Proof % 4.93/5.21 1. (mtvisible (c_tptp_member3515_mt)) (-. (mtvisible (c_tptp_member3515_mt))) ### Axiom % 4.93/5.21 2. (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (-. (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt))) ### Axiom % 4.93/5.21 3. ((c_cyclistsmt) != (c_cyclistsmt)) ### NotEqual % 4.93/5.21 4. (-. (genlmt (c_tptp_member3515_mt) (c_cyclistsmt))) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) ### Trans 2 3 % 4.93/5.21 5. ((c_keinteractionresourcetestmt) != (c_keinteractionresourcetestmt)) ### NotEqual % 4.93/5.21 6. (-. (genlmt (c_tptp_member3515_mt) (c_keinteractionresourcetestmt))) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) ### Trans 4 5 % 4.93/5.21 7. ((c_testvocabularymt) != (c_testvocabularymt)) ### NotEqual % 4.93/5.21 8. (-. (genlmt (c_tptp_member3515_mt) (c_testvocabularymt))) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) ### Trans 6 7 % 4.93/5.21 9. ((c_nooescapearchitecturemt) != (c_nooescapearchitecturemt)) ### NotEqual % 4.93/5.21 10. (-. (genlmt (c_tptp_member3515_mt) (c_nooescapearchitecturemt))) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) ### Trans 8 9 % 4.93/5.21 11. ((c_organizationdatamt) != (c_organizationdatamt)) ### NotEqual % 4.93/5.21 12. (-. (genlmt (c_tptp_member3515_mt) (c_organizationdatamt))) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) ### Trans 10 11 % 4.93/5.21 13. ((f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) != (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) ### Refl(=) % 4.93/5.21 14. (-. (genlmt (c_tptp_member3515_mt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)))) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) ### Trans 12 13 % 4.93/5.21 15. ((c_massmediadatamt) != (c_massmediadatamt)) ### NotEqual % 4.93/5.21 16. (-. (genlmt (c_tptp_member3515_mt) (c_massmediadatamt))) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) ### Trans 14 15 % 4.93/5.21 17. ((c_ethnicgroupsmt) != (c_ethnicgroupsmt)) ### NotEqual % 4.93/5.21 18. (-. (genlmt (c_tptp_member3515_mt) (c_ethnicgroupsmt))) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) ### Trans 16 17 % 4.93/5.21 19. ((c_ethnicgroupsvocabularymt) != (c_ethnicgroupsvocabularymt)) ### NotEqual % 4.93/5.21 20. (-. (genlmt (c_tptp_member3515_mt) (c_ethnicgroupsvocabularymt))) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) ### Trans 18 19 % 4.93/5.21 21. ((c_worldcompletedualistgeographymt) != (c_worldcompletedualistgeographymt)) ### NotEqual % 4.93/5.21 22. (-. (genlmt (c_tptp_member3515_mt) (c_worldcompletedualistgeographymt))) (genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) ### Trans 20 21 % 4.93/5.21 23. ((c_unitedstatesgeographydualistmt) != (c_unitedstatesgeographydualistmt)) ### NotEqual % 4.93/5.21 24. (-. (genlmt (c_tptp_member3515_mt) (c_unitedstatesgeographydualistmt))) (genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) ### Trans 22 23 % 4.93/5.21 25. ((c_worldgeographydualistmt) != (c_worldgeographydualistmt)) ### NotEqual % 4.93/5.21 26. (-. (genlmt (c_tptp_member3515_mt) (c_worldgeographydualistmt))) (genlmt (c_unitedstatesgeographydualistmt) (c_worldgeographydualistmt)) (genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) (genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) ### Trans 24 25 % 4.93/5.21 27. ((c_worldgeographymt) != (c_worldgeographymt)) ### NotEqual % 4.93/5.21 28. (-. (genlmt (c_tptp_member3515_mt) (c_worldgeographymt))) (genlmt (c_worldgeographydualistmt) (c_worldgeographymt)) (genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) (genlmt (c_unitedstatesgeographydualistmt) (c_worldgeographydualistmt)) ### Trans 26 27 % 4.93/5.21 29. (-. (mtvisible (c_worldgeographymt))) (mtvisible (c_worldgeographymt)) ### Axiom % 4.93/5.21 30. (((mtvisible (c_tptp_member3515_mt)) /\ (genlmt (c_tptp_member3515_mt) (c_worldgeographymt))) => (mtvisible (c_worldgeographymt))) (-. (mtvisible (c_worldgeographymt))) (genlmt (c_unitedstatesgeographydualistmt) (c_worldgeographydualistmt)) (genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) (genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) (genlmt (c_worldgeographydualistmt) (c_worldgeographymt)) (mtvisible (c_tptp_member3515_mt)) ### DisjTree 1 28 29 % 4.93/5.21 31. (All GENLMT, (((mtvisible (c_tptp_member3515_mt)) /\ (genlmt (c_tptp_member3515_mt) GENLMT)) => (mtvisible GENLMT))) (mtvisible (c_tptp_member3515_mt)) (genlmt (c_worldgeographydualistmt) (c_worldgeographymt)) (genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) (genlmt (c_unitedstatesgeographydualistmt) (c_worldgeographydualistmt)) (-. (mtvisible (c_worldgeographymt))) ### All 30 % 4.93/5.21 32. (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) (-. (mtvisible (c_worldgeographymt))) (genlmt (c_unitedstatesgeographydualistmt) (c_worldgeographydualistmt)) (genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) (genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) (genlmt (c_worldgeographydualistmt) (c_worldgeographymt)) (mtvisible (c_tptp_member3515_mt)) ### All 31 % 4.93/5.21 33. (-. ((mtvisible (c_tptp_member3515_mt)) => (isa (c_wanica_districtsuriname) zenon_X0))) (genlmt (c_worldgeographydualistmt) (c_worldgeographymt)) (genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) (genlmt (c_unitedstatesgeographydualistmt) (c_worldgeographydualistmt)) (-. (mtvisible (c_worldgeographymt))) (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) ### NotImply 32 % 4.93/5.21 34. (-. (Ex COL, ((mtvisible (c_tptp_member3515_mt)) => (isa (c_wanica_districtsuriname) COL)))) (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) (-. (mtvisible (c_worldgeographymt))) (genlmt (c_unitedstatesgeographydualistmt) (c_worldgeographydualistmt)) (genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) (genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) (genlmt (c_worldgeographydualistmt) (c_worldgeographymt)) ### NotExists 33 % 4.93/5.21 35. (state_geopolitical (c_wanica_districtsuriname)) (-. (state_geopolitical (c_wanica_districtsuriname))) ### Axiom % 4.93/5.21 36. (-. (isa (c_wanica_districtsuriname) (c_state_geopolitical))) (isa (c_wanica_districtsuriname) (c_state_geopolitical)) ### Axiom % 4.93/5.21 37. ((state_geopolitical (c_wanica_districtsuriname)) => (isa (c_wanica_districtsuriname) (c_state_geopolitical))) (-. (isa (c_wanica_districtsuriname) (c_state_geopolitical))) (state_geopolitical (c_wanica_districtsuriname)) ### Imply 35 36 % 4.93/5.21 38. (All X, ((state_geopolitical X) => (isa X (c_state_geopolitical)))) (state_geopolitical (c_wanica_districtsuriname)) (-. (isa (c_wanica_districtsuriname) (c_state_geopolitical))) ### All 37 % 4.93/5.21 39. (-. ((mtvisible (c_tptp_member3515_mt)) => (isa (c_wanica_districtsuriname) (c_state_geopolitical)))) (state_geopolitical (c_wanica_districtsuriname)) (All X, ((state_geopolitical X) => (isa X (c_state_geopolitical)))) ### NotImply 38 % 4.93/5.21 40. (-. (Ex COL, ((mtvisible (c_tptp_member3515_mt)) => (isa (c_wanica_districtsuriname) COL)))) (All X, ((state_geopolitical X) => (isa X (c_state_geopolitical)))) (state_geopolitical (c_wanica_districtsuriname)) ### NotExists 39 % 4.93/5.21 41. ((mtvisible (c_worldgeographymt)) => (state_geopolitical (c_wanica_districtsuriname))) (All X, ((state_geopolitical X) => (isa X (c_state_geopolitical)))) (genlmt (c_worldgeographydualistmt) (c_worldgeographymt)) (genlmt (c_worldcompletedualistgeographymt) (c_unitedstatesgeographydualistmt)) (genlmt (c_ethnicgroupsmt) (c_ethnicgroupsvocabularymt)) (genlmt (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman)) (c_massmediadatamt)) (genlmt (c_nooescapearchitecturemt) (c_organizationdatamt)) (genlmt (c_keinteractionresourcetestmt) (c_testvocabularymt)) (genlmt (c_tptp_spindleheadmt) (c_cyclistsmt)) (genlmt (c_tptp_member3515_mt) (c_tptp_spindleheadmt)) (genlmt (c_cyclistsmt) (c_keinteractionresourcetestmt)) (genlmt (c_testvocabularymt) (c_nooescapearchitecturemt)) (genlmt (c_organizationdatamt) (f_contextofpcwfn (c_ap_martha_stewart_omnimedia_names_chairman))) (genlmt (c_massmediadatamt) (c_ethnicgroupsmt)) (genlmt (c_ethnicgroupsvocabularymt) (c_worldcompletedualistgeographymt)) (genlmt (c_unitedstatesgeographydualistmt) (c_worldgeographydualistmt)) (All SPECMT, (All GENLMT, (((mtvisible SPECMT) /\ (genlmt SPECMT GENLMT)) => (mtvisible GENLMT)))) (-. (Ex COL, ((mtvisible (c_tptp_member3515_mt)) => (isa (c_wanica_districtsuriname) COL)))) ### Imply 34 40 % 4.93/5.21 % SZS output end Proof % 4.93/5.21 (* END-PROOF *) %------------------------------------------------------------------------------