; TeX output 2001.11.29:0946x=lFDtqGcmr17ScuNhubert'sBSteamrollery?!",ff cmsy10#􍍍XQ ff cmr12Selmer/Bringsjord&a@NovembdCer/29,2001Q΍'NG cmbx121D(EnglishzVaGersion- 'W_olvuNes,foxes,birds,caterpillars,and 0snailsare'animals,and\4therearesomeofeacuNhofthem.'Also, therearesomegrains,andgrainsareplanuNts.'EvuNeryanimaleitherlikestoeatallplantsorall'animals qmuNuchsmallerthanitselfthatliketoeat'some=planuNts. sCaterpillarsandsnailsaremuch'smallerothanbirds,whicuNharemuchsmallerthan'fouNxes, whichinturnaremuNuchsmallerthanwuNolves.'W_olvuNesxdonotliketoeatfoxesorgrains,lwhile'birdslikuNetoeatcaterpillarsbutnotsmails.Cater-'pillarsBandsnailslikuNetoeatsomeplants.' ffd g^ O!cmsy7K`y cmr10NamedafterLenSchubGert.KSeePelletier,_F.J.(1986)\Seventy- veProblemsforT*est- ing9AutomaticTheoremProvers,"9': cmti10Journal*ofAutomate}'dReasoning9"V cmbx102:191-216.tSeealsotheUUerratainthesameauthor's(1988)JournalofAutomate}'dReasoningUU4:q235-236.XQ cmr121*x='Therefore,@thereǙisananimalthatlikuNestoeata'grain-eatingBanimal.5?֍'2D(FuOLzVaGersion& 'Nff cmbx122.1KcKey&dD\П-gq cmmi12Pj0Ǽx:mxBںisananimalBffffKPj5Ǽx:mxBںisasnail-Pj1Ǽx:mxBںisawuNolf8!ffffKQj0Ǽx:mxBںisaplanuNt-Pj2Ǽx:mxBںisafouNxA_ffffKQj1Ǽx:mxBںisagrain-Pj3Ǽx:mxBںisabird8!ffffKS5xy:mxBںismuNuchBsmallerthany-Pj4Ǽx:mxBںisacaterpillar͟ffffKR+xy:mxBںlikuNestoeaty2Wx='2.2KcSymbs3olization&d/x1.D_!",q cmsy108x(Pj1Ǽxؿ!Pj0x)^9xPj1x! ^/x2.D_8x(Pj2Ǽxؿ!Pj0x)^9xPj2x/x3.D_8x(Pj3Ǽxؿ!Pj0x)^9xPj3x/x4.D_8x(Pj4Ǽxؿ!Pj0x)^9xPj4x/x5.D_8x(Pj5Ǽxؿ!Pj0x)^9xPj5x/x6.D_9xQj1Ǽx^8x(Qj1xؿ!Qj0x)/x7.D_8x(Pj0Ǽx8!(8y(Qj0y?!R+xy)1p_8y((Pj0Ǽy^D_S5yx^9z엺(Qj0Ǽzw^R+yz엺))ؿ!R+xy)))/x8.D_8x8y((Pj3ǼyZ`^(Pj5 (_Pj4x))ؿ!S5xy)/x9.D_8x8y((Pj3Ǽx^Pj2y)ؿ!S5xy)&Lw10.D_8x8y((Pj2Ǽx^Pj1y)ؿ!S5xy)&Lw11.D_8x8y((Pj1Ǽx^(Pj2yZ`_Qj1y))ؿ!:R+xy)&Lw12.D_8x8y((Pj3Ǽx^Pj4y)ؿ!R+xy)&Lw13.D_8x8y((Pj3Ǽx^Pj5y)ؿ!:R+xy)&Lw14.D_8x((Pj4Ǽx_Pj5x)ؿ!9y(Qj0yZ`^R+xy))&Lw15.D_9x9y(Pj0Ǽx^Pj0yZ`^9z엺(Qj1zw^R+yz^R+xy))3 ;xNff cmbx12NG cmbx12"V cmbx10': cmti10!",ff cmsy10!",q cmsy10gq cmmi12XQ ff cmr12DtqGcmr17XQ cmr12 O!cmsy7K`y cmr10