(set-logic SLIA) (synth-fun f ((name String)) String ((Start String (ntString)) (ntString String (name " " "(" ")" "-" (str.++ ntString ntString) (str.replace ntString ntString ntString) (str.at ntString ntInt) (int.to.str ntInt) (str.substr ntString ntInt ntInt))) (ntInt Int (0 1 2 3 4 5 (+ ntInt ntInt) (- ntInt ntInt) (str.len ntString) (str.to.int ntString) (str.indexof ntString ntString ntInt))) (ntBool Bool (true false (str.prefixof ntString ntString) (str.suffixof ntString ntString) (str.contains ntString ntString))))) (declare-var name String) (constraint (= (f "938-242-504") "(938) 242-504")) (constraint (= (f "938-242-504") "(938) 242-504")) (constraint (= (f "938-242-504") "(938) 242-504")) (constraint (= (f "308-916-545") "(308) 916-545")) (constraint (= (f "308-916-545") "(308) 916-545")) (constraint (= (f "308-916-545") "(308) 916-545")) (constraint (= (f "623-599-749") "(623) 599-749")) (constraint (= (f "623-599-749") "(623) 599-749")) (constraint (= (f "623-599-749") "(623) 599-749")) (constraint (= (f "981-424-843") "(981) 424-843")) (constraint (= (f "981-424-843") "(981) 424-843")) (constraint (= (f "981-424-843") "(981) 424-843")) (constraint (= (f "118-980-214") "(118) 980-214")) (constraint (= (f "118-980-214") "(118) 980-214")) (constraint (= (f "118-980-214") "(118) 980-214")) (constraint (= (f "244-655-094") "(244) 655-094")) (constraint (= (f "244-655-094") "(244) 655-094")) (constraint (= (f "244-655-094") "(244) 655-094")) (constraint (= (f "830-941-991") "(830) 941-991")) (constraint (= (f "830-941-991") "(830) 941-991")) (constraint (= (f "830-941-991") "(830) 941-991")) (constraint (= (f "911-186-562") "(911) 186-562")) (constraint (= (f "911-186-562") "(911) 186-562")) (constraint (= (f "911-186-562") "(911) 186-562")) (constraint (= (f "002-500-200") "(002) 500-200")) (constraint (= (f "002-500-200") "(002) 500-200")) (constraint (= (f "002-500-200") "(002) 500-200")) (constraint (= (f "113-860-034") "(113) 860-034")) (constraint (= (f "113-860-034") "(113) 860-034")) (constraint (= (f "113-860-034") "(113) 860-034")) (constraint (= (f "457-622-959") "(457) 622-959")) (constraint (= (f "457-622-959") "(457) 622-959")) (constraint (= (f "457-622-959") "(457) 622-959")) (constraint (= (f "986-722-311") "(986) 722-311")) (constraint (= (f "986-722-311") "(986) 722-311")) (constraint (= (f "986-722-311") "(986) 722-311")) (constraint (= (f "110-170-771") "(110) 170-771")) (constraint (= (f "110-170-771") "(110) 170-771")) (constraint (= (f "110-170-771") "(110) 170-771")) (constraint (= (f "469-610-118") "(469) 610-118")) (constraint (= (f "469-610-118") "(469) 610-118")) (constraint (= (f "469-610-118") "(469) 610-118")) (constraint (= (f "817-925-247") "(817) 925-247")) (constraint (= (f "817-925-247") "(817) 925-247")) (constraint (= (f "817-925-247") "(817) 925-247")) (constraint (= (f "256-899-439") "(256) 899-439")) (constraint (= (f "256-899-439") "(256) 899-439")) (constraint (= (f "256-899-439") "(256) 899-439")) (constraint (= (f "886-911-726") "(886) 911-726")) (constraint (= (f "886-911-726") "(886) 911-726")) (constraint (= (f "886-911-726") "(886) 911-726")) (constraint (= (f "562-950-358") "(562) 950-358")) (constraint (= (f "562-950-358") "(562) 950-358")) (constraint (= (f "562-950-358") "(562) 950-358")) (constraint (= (f "693-049-588") "(693) 049-588")) (constraint (= (f "693-049-588") "(693) 049-588")) (constraint (= (f "693-049-588") "(693) 049-588")) (constraint (= (f "840-503-234") "(840) 503-234")) (constraint (= (f "840-503-234") "(840) 503-234")) (constraint (= (f "840-503-234") "(840) 503-234")) (constraint (= (f "698-815-340") "(698) 815-340")) (constraint (= (f "698-815-340") "(698) 815-340")) (constraint (= (f "698-815-340") "(698) 815-340")) (constraint (= (f "498-808-434") "(498) 808-434")) (constraint (= (f "498-808-434") "(498) 808-434")) (constraint (= (f "498-808-434") "(498) 808-434")) (constraint (= (f "329-545-000") "(329) 545-000")) (constraint (= (f "329-545-000") "(329) 545-000")) (constraint (= (f "329-545-000") "(329) 545-000")) (constraint (= (f "380-281-597") "(380) 281-597")) (constraint (= (f "380-281-597") "(380) 281-597")) (constraint (= (f "380-281-597") "(380) 281-597")) (constraint (= (f "332-395-493") "(332) 395-493")) (constraint (= (f "332-395-493") "(332) 395-493")) (constraint (= (f "332-395-493") "(332) 395-493")) (constraint (= (f "251-903-028") "(251) 903-028")) (constraint (= (f "251-903-028") "(251) 903-028")) (constraint (= (f "251-903-028") "(251) 903-028")) (constraint (= (f "176-090-894") "(176) 090-894")) (constraint (= (f "176-090-894") "(176) 090-894")) (constraint (= (f "176-090-894") "(176) 090-894")) (constraint (= (f "336-611-100") "(336) 611-100")) (constraint (= (f "336-611-100") "(336) 611-100")) (constraint (= (f "336-611-100") "(336) 611-100")) (constraint (= (f "416-390-647") "(416) 390-647")) (constraint (= (f "416-390-647") "(416) 390-647")) (constraint (= (f "416-390-647") "(416) 390-647")) (constraint (= (f "019-430-596") "(019) 430-596")) (constraint (= (f "019-430-596") "(019) 430-596")) (constraint (= (f "019-430-596") "(019) 430-596")) (constraint (= (f "960-659-771") "(960) 659-771")) (constraint (= (f "960-659-771") "(960) 659-771")) (constraint (= (f "960-659-771") "(960) 659-771")) (constraint (= (f "475-505-007") "(475) 505-007")) (constraint (= (f "475-505-007") "(475) 505-007")) (constraint (= (f "475-505-007") "(475) 505-007")) (constraint (= (f "424-069-886") "(424) 069-886")) (constraint (= (f "424-069-886") "(424) 069-886")) (constraint (= (f "424-069-886") "(424) 069-886")) (constraint (= (f "941-102-117") "(941) 102-117")) (constraint (= (f "941-102-117") "(941) 102-117")) (constraint (= (f "941-102-117") "(941) 102-117")) (constraint (= (f "331-728-008") "(331) 728-008")) (constraint (= (f "331-728-008") "(331) 728-008")) (constraint (= (f "331-728-008") "(331) 728-008")) (constraint (= (f "487-726-198") "(487) 726-198")) (constraint (= (f "487-726-198") "(487) 726-198")) (constraint (= (f "487-726-198") "(487) 726-198")) (constraint (= (f "612-419-942") "(612) 419-942")) (constraint (= (f "612-419-942") "(612) 419-942")) (constraint (= (f "612-419-942") "(612) 419-942")) (constraint (= (f "594-741-346") "(594) 741-346")) (constraint (= (f "594-741-346") "(594) 741-346")) (constraint (= (f "594-741-346") "(594) 741-346")) (constraint (= (f "320-984-742") "(320) 984-742")) (constraint (= (f "320-984-742") "(320) 984-742")) (constraint (= (f "320-984-742") "(320) 984-742")) (constraint (= (f "060-919-361") "(060) 919-361")) (constraint (= (f "060-919-361") "(060) 919-361")) (constraint (= (f "060-919-361") "(060) 919-361")) (constraint (= (f "275-536-998") "(275) 536-998")) (constraint (= (f "275-536-998") "(275) 536-998")) (constraint (= (f "275-536-998") "(275) 536-998")) (constraint (= (f "548-835-065") "(548) 835-065")) (constraint (= (f "548-835-065") "(548) 835-065")) (constraint (= (f "548-835-065") "(548) 835-065")) (constraint (= (f "197-485-507") "(197) 485-507")) (constraint (= (f "197-485-507") "(197) 485-507")) (constraint (= (f "197-485-507") "(197) 485-507")) (constraint (= (f "455-776-949") "(455) 776-949")) (constraint (= (f "455-776-949") "(455) 776-949")) (constraint (= (f "455-776-949") "(455) 776-949")) (constraint (= (f "085-421-340") "(085) 421-340")) (constraint (= (f "085-421-340") "(085) 421-340")) (constraint (= (f "085-421-340") "(085) 421-340")) (constraint (= (f "785-713-099") "(785) 713-099")) (constraint (= (f "785-713-099") "(785) 713-099")) (constraint (= (f "785-713-099") "(785) 713-099")) (constraint (= (f "426-712-861") "(426) 712-861")) (constraint (= (f "426-712-861") "(426) 712-861")) (constraint (= (f "426-712-861") "(426) 712-861")) (constraint (= (f "386-994-906") "(386) 994-906")) (constraint (= (f "386-994-906") "(386) 994-906")) (constraint (= (f "386-994-906") "(386) 994-906")) (constraint (= (f "918-304-840") "(918) 304-840")) (constraint (= (f "918-304-840") "(918) 304-840")) (constraint (= (f "918-304-840") "(918) 304-840")) (constraint (= (f "247-153-598") "(247) 153-598")) (constraint (= (f "247-153-598") "(247) 153-598")) (constraint (= (f "247-153-598") "(247) 153-598")) (constraint (= (f "075-497-069") "(075) 497-069")) (constraint (= (f "075-497-069") "(075) 497-069")) (constraint (= (f "075-497-069") "(075) 497-069")) (constraint (= (f "140-726-583") "(140) 726-583")) (constraint (= (f "140-726-583") "(140) 726-583")) (constraint (= (f "140-726-583") "(140) 726-583")) (constraint (= (f "049-413-248") "(049) 413-248")) (constraint (= (f "049-413-248") "(049) 413-248")) (constraint (= (f "049-413-248") "(049) 413-248")) (constraint (= (f "977-386-462") "(977) 386-462")) (constraint (= (f "977-386-462") "(977) 386-462")) (constraint (= (f "977-386-462") "(977) 386-462")) (constraint (= (f "058-272-455") "(058) 272-455")) (constraint (= (f "058-272-455") "(058) 272-455")) (constraint (= (f "058-272-455") "(058) 272-455")) (constraint (= (f "428-629-927") "(428) 629-927")) (constraint (= (f "428-629-927") "(428) 629-927")) (constraint (= (f "428-629-927") "(428) 629-927")) (constraint (= (f "449-122-191") "(449) 122-191")) (constraint (= (f "449-122-191") "(449) 122-191")) (constraint (= (f "449-122-191") "(449) 122-191")) (constraint (= (f "568-759-670") "(568) 759-670")) (constraint (= (f "568-759-670") "(568) 759-670")) (constraint (= (f "568-759-670") "(568) 759-670")) (constraint (= (f "312-846-053") "(312) 846-053")) (constraint (= (f "312-846-053") "(312) 846-053")) (constraint (= (f "312-846-053") "(312) 846-053")) (constraint (= (f "943-037-297") "(943) 037-297")) (constraint (= (f "943-037-297") "(943) 037-297")) (constraint (= (f "943-037-297") "(943) 037-297")) (constraint (= (f "014-270-177") "(014) 270-177")) (constraint (= (f "014-270-177") "(014) 270-177")) (constraint (= (f "014-270-177") "(014) 270-177")) (constraint (= (f "658-877-878") "(658) 877-878")) (constraint (= (f "658-877-878") "(658) 877-878")) (constraint (= (f "658-877-878") "(658) 877-878")) (constraint (= (f "888-594-038") "(888) 594-038")) (constraint (= (f "888-594-038") "(888) 594-038")) (constraint (= (f "888-594-038") "(888) 594-038")) (constraint (= (f "232-253-254") "(232) 253-254")) (constraint (= (f "232-253-254") "(232) 253-254")) (constraint (= (f "232-253-254") "(232) 253-254")) (constraint (= (f "308-722-292") "(308) 722-292")) (constraint (= (f "308-722-292") "(308) 722-292")) (constraint (= (f "308-722-292") "(308) 722-292")) (constraint (= (f "342-145-742") "(342) 145-742")) (constraint (= (f "342-145-742") "(342) 145-742")) (constraint (= (f "342-145-742") "(342) 145-742")) (constraint (= (f "568-181-515") "(568) 181-515")) (constraint (= (f "568-181-515") "(568) 181-515")) (constraint (= (f "568-181-515") "(568) 181-515")) (constraint (= (f "300-140-756") "(300) 140-756")) (constraint (= (f "300-140-756") "(300) 140-756")) (constraint (= (f "300-140-756") "(300) 140-756")) (constraint (= (f "099-684-216") "(099) 684-216")) (constraint (= (f "099-684-216") "(099) 684-216")) (constraint (= (f "099-684-216") "(099) 684-216")) (constraint (= (f "575-296-621") "(575) 296-621")) (constraint (= (f "575-296-621") "(575) 296-621")) (constraint (= (f "575-296-621") "(575) 296-621")) (constraint (= (f "994-443-794") "(994) 443-794")) (constraint (= (f "994-443-794") "(994) 443-794")) (constraint (= (f "994-443-794") "(994) 443-794")) (constraint (= (f "400-334-692") "(400) 334-692")) (constraint (= (f "400-334-692") "(400) 334-692")) (constraint (= (f "400-334-692") "(400) 334-692")) (constraint (= (f "684-711-883") "(684) 711-883")) (constraint (= (f "684-711-883") "(684) 711-883")) (constraint (= (f "684-711-883") "(684) 711-883")) (constraint (= (f "539-636-358") "(539) 636-358")) (constraint (= (f "539-636-358") "(539) 636-358")) (constraint (= (f "539-636-358") "(539) 636-358")) (constraint (= (f "009-878-919") "(009) 878-919")) (constraint (= (f "009-878-919") "(009) 878-919")) (constraint (= (f "009-878-919") "(009) 878-919")) (constraint (= (f "919-545-701") "(919) 545-701")) (constraint (= (f "919-545-701") "(919) 545-701")) (constraint (= (f "919-545-701") "(919) 545-701")) (constraint (= (f "546-399-239") "(546) 399-239")) (constraint (= (f "546-399-239") "(546) 399-239")) (constraint (= (f "546-399-239") "(546) 399-239")) (constraint (= (f "993-608-757") "(993) 608-757")) (constraint (= (f "993-608-757") "(993) 608-757")) (constraint (= (f "993-608-757") "(993) 608-757")) (constraint (= (f "107-652-845") "(107) 652-845")) (constraint (= (f "107-652-845") "(107) 652-845")) (constraint (= (f "107-652-845") "(107) 652-845")) (constraint (= (f "206-805-793") "(206) 805-793")) (constraint (= (f "206-805-793") "(206) 805-793")) (constraint (= (f "206-805-793") "(206) 805-793")) (constraint (= (f "198-857-684") "(198) 857-684")) (constraint (= (f "198-857-684") "(198) 857-684")) (constraint (= (f "198-857-684") "(198) 857-684")) (constraint (= (f "912-827-430") "(912) 827-430")) (constraint (= (f "912-827-430") "(912) 827-430")) (constraint (= (f "912-827-430") "(912) 827-430")) (constraint (= (f "560-951-766") "(560) 951-766")) (constraint (= (f "560-951-766") "(560) 951-766")) (constraint (= (f "560-951-766") "(560) 951-766")) (constraint (= (f "142-178-290") "(142) 178-290")) (constraint (= (f "142-178-290") "(142) 178-290")) (constraint (= (f "142-178-290") "(142) 178-290")) (constraint (= (f "732-196-946") "(732) 196-946")) (constraint (= (f "732-196-946") "(732) 196-946")) (constraint (= (f "732-196-946") "(732) 196-946")) (constraint (= (f "963-875-745") "(963) 875-745")) (constraint (= (f "963-875-745") "(963) 875-745")) (constraint (= (f "963-875-745") "(963) 875-745")) (constraint (= (f "881-865-867") "(881) 865-867")) (constraint (= (f "881-865-867") "(881) 865-867")) (constraint (= (f "881-865-867") "(881) 865-867")) (constraint (= (f "234-686-715") "(234) 686-715")) (constraint (= (f "234-686-715") "(234) 686-715")) (constraint (= (f "234-686-715") "(234) 686-715")) (constraint (= (f "720-330-583") "(720) 330-583")) (constraint (= (f "720-330-583") "(720) 330-583")) (constraint (= (f "720-330-583") "(720) 330-583")) (constraint (= (f "593-065-126") "(593) 065-126")) (constraint (= (f "593-065-126") "(593) 065-126")) (constraint (= (f "593-065-126") "(593) 065-126")) (constraint (= (f "671-778-064") "(671) 778-064")) (constraint (= (f "671-778-064") "(671) 778-064")) (constraint (= (f "671-778-064") "(671) 778-064")) (constraint (= (f "252-029-036") "(252) 029-036")) (constraint (= (f "252-029-036") "(252) 029-036")) (constraint (= (f "252-029-036") "(252) 029-036")) (constraint (= (f "700-322-036") "(700) 322-036")) (constraint (= (f "700-322-036") "(700) 322-036")) (constraint (= (f "700-322-036") "(700) 322-036")) (constraint (= (f "882-587-473") "(882) 587-473")) (constraint (= (f "882-587-473") "(882) 587-473")) (constraint (= (f "882-587-473") "(882) 587-473")) (constraint (= (f "964-134-953") "(964) 134-953")) (constraint (= (f "964-134-953") "(964) 134-953")) (constraint (= (f "964-134-953") "(964) 134-953")) (constraint (= (f "038-300-876") "(038) 300-876")) (constraint (= (f "038-300-876") "(038) 300-876")) (constraint (= (f "038-300-876") "(038) 300-876")) (constraint (= (f "158-894-947") "(158) 894-947")) (constraint (= (f "158-894-947") "(158) 894-947")) (constraint (= (f "158-894-947") "(158) 894-947")) (constraint (= (f "757-454-374") "(757) 454-374")) (constraint (= (f "757-454-374") "(757) 454-374")) (constraint (= (f "757-454-374") "(757) 454-374")) (constraint (= (f "872-513-190") "(872) 513-190")) (constraint (= (f "872-513-190") "(872) 513-190")) (constraint (= (f "872-513-190") "(872) 513-190")) (constraint (= (f "566-086-726") "(566) 086-726")) (constraint (= (f "566-086-726") "(566) 086-726")) (constraint (= (f "566-086-726") "(566) 086-726")) (constraint (= (f "938-242-504") "(938) 242-504")) (constraint (= (f "308-916-545") "(308) 916-545")) (constraint (= (f "623-599-749") "(623) 599-749")) (constraint (= (f "981-424-843") "(981) 424-843")) (constraint (= (f "118-980-214") "(118) 980-214")) (constraint (= (f "244-655-094") "(244) 655-094")) (constraint (= (f "830-941-991") "(830) 941-991")) (constraint (= (f "911-186-562") "(911) 186-562")) (constraint (= (f "002-500-200") "(002) 500-200")) (constraint (= (f "113-860-034") "(113) 860-034")) (constraint (= (f "457-622-959") "(457) 622-959")) (constraint (= (f "986-722-311") "(986) 722-311")) (constraint (= (f "110-170-771") "(110) 170-771")) (constraint (= (f "469-610-118") "(469) 610-118")) (constraint (= (f "817-925-247") "(817) 925-247")) (constraint (= (f "256-899-439") "(256) 899-439")) (constraint (= (f "886-911-726") "(886) 911-726")) (constraint (= (f "562-950-358") "(562) 950-358")) (constraint (= (f "693-049-588") "(693) 049-588")) (constraint (= (f "840-503-234") "(840) 503-234")) (constraint (= (f "698-815-340") "(698) 815-340")) (constraint (= (f "498-808-434") "(498) 808-434")) (constraint (= (f "329-545-000") "(329) 545-000")) (constraint (= (f "380-281-597") "(380) 281-597")) (constraint (= (f "332-395-493") "(332) 395-493")) (constraint (= (f "251-903-028") "(251) 903-028")) (constraint (= (f "176-090-894") "(176) 090-894")) (constraint (= (f "336-611-100") "(336) 611-100")) (constraint (= (f "416-390-647") "(416) 390-647")) (constraint (= (f "019-430-596") "(019) 430-596")) (constraint (= (f "960-659-771") "(960) 659-771")) (constraint (= (f "475-505-007") "(475) 505-007")) (constraint (= (f "424-069-886") "(424) 069-886")) (constraint (= (f "941-102-117") "(941) 102-117")) (constraint (= (f "331-728-008") "(331) 728-008")) (constraint (= (f "487-726-198") "(487) 726-198")) (constraint (= (f "612-419-942") "(612) 419-942")) (constraint (= (f "594-741-346") "(594) 741-346")) (constraint (= (f "320-984-742") "(320) 984-742")) (constraint (= (f "060-919-361") "(060) 919-361")) (constraint (= (f "275-536-998") "(275) 536-998")) (constraint (= (f "548-835-065") "(548) 835-065")) (constraint (= (f "197-485-507") "(197) 485-507")) (constraint (= (f "455-776-949") "(455) 776-949")) (constraint (= (f "085-421-340") "(085) 421-340")) (constraint (= (f "785-713-099") "(785) 713-099")) (constraint (= (f "426-712-861") "(426) 712-861")) (constraint (= (f "386-994-906") "(386) 994-906")) (constraint (= (f "918-304-840") "(918) 304-840")) (constraint (= (f "247-153-598") "(247) 153-598")) (constraint (= (f "075-497-069") "(075) 497-069")) (constraint (= (f "140-726-583") "(140) 726-583")) (constraint (= (f "049-413-248") "(049) 413-248")) (constraint (= (f "977-386-462") "(977) 386-462")) (constraint (= (f "058-272-455") "(058) 272-455")) (constraint (= (f "428-629-927") "(428) 629-927")) (constraint (= (f "449-122-191") "(449) 122-191")) (constraint (= (f "568-759-670") "(568) 759-670")) (constraint (= (f "312-846-053") "(312) 846-053")) (constraint (= (f "943-037-297") "(943) 037-297")) (constraint (= (f "014-270-177") "(014) 270-177")) (constraint (= (f "658-877-878") "(658) 877-878")) (constraint (= (f "888-594-038") "(888) 594-038")) (constraint (= (f "232-253-254") "(232) 253-254")) (constraint (= (f "308-722-292") "(308) 722-292")) (constraint (= (f "342-145-742") "(342) 145-742")) (constraint (= (f "568-181-515") "(568) 181-515")) (constraint (= (f "300-140-756") "(300) 140-756")) (constraint (= (f "099-684-216") "(099) 684-216")) (constraint (= (f "575-296-621") "(575) 296-621")) (constraint (= (f "994-443-794") "(994) 443-794")) (constraint (= (f "400-334-692") "(400) 334-692")) (constraint (= (f "684-711-883") "(684) 711-883")) (constraint (= (f "539-636-358") "(539) 636-358")) (constraint (= (f "009-878-919") "(009) 878-919")) (constraint (= (f "919-545-701") "(919) 545-701")) (constraint (= (f "546-399-239") "(546) 399-239")) (constraint (= (f "993-608-757") "(993) 608-757")) (constraint (= (f "107-652-845") "(107) 652-845")) (constraint (= (f "206-805-793") "(206) 805-793")) (constraint (= (f "198-857-684") "(198) 857-684")) (constraint (= (f "912-827-430") "(912) 827-430")) (constraint (= (f "560-951-766") "(560) 951-766")) (constraint (= (f "142-178-290") "(142) 178-290")) (constraint (= (f "732-196-946") "(732) 196-946")) (constraint (= (f "963-875-745") "(963) 875-745")) (constraint (= (f "881-865-867") "(881) 865-867")) (constraint (= (f "234-686-715") "(234) 686-715")) (constraint (= (f "720-330-583") "(720) 330-583")) (constraint (= (f "593-065-126") "(593) 065-126")) (constraint (= (f "671-778-064") "(671) 778-064")) (constraint (= (f "252-029-036") "(252) 029-036")) (constraint (= (f "700-322-036") "(700) 322-036")) (constraint (= (f "882-587-473") "(882) 587-473")) (constraint (= (f "964-134-953") "(964) 134-953")) (constraint (= (f "038-300-876") "(038) 300-876")) (constraint (= (f "158-894-947") "(158) 894-947")) (constraint (= (f "757-454-374") "(757) 454-374")) (constraint (= (f "872-513-190") "(872) 513-190")) (constraint (= (f "566-086-726") "(566) 086-726")) (check-synth)