fof(sos_01,conjecture,! [X0] : ( k04_buttercup10049(X0) => k04_buttercup10048(X0) ) ).
fof(sos_02,conjecture,! [X1] : ( k04_buttercup10051(X1) => k04_buttercup10048(X1) ) ).
fof(sos_03,conjecture,! [X2] : ( k04_buttercup10096(X2) => k04_buttercup10095(X2) ) ).
fof(sos_04,conjecture,! [X3] : ( k04_buttercup10097(X3) => k04_buttercup10095(X3) ) ).
fof(sos_05,conjecture,! [X4] : ( k04_buttercup10342(X4) => k04_buttercup10337(X4) ) ).
fof(sos_06,conjecture,! [X5] : ( k04_buttercup10347(X5) => k04_buttercup10337(X5) ) ).
fof(sos_07,conjecture,! [X6] : ( k04_buttercup10351(X6) => k04_buttercup10337(X6) ) ).
fof(sos_08,conjecture,! [X7] : ( k04_buttercup10453(X7) => k04_buttercup10449(X7) ) ).
fof(sos_09,conjecture,! [X8] : ( k04_buttercup10462(X8) => k04_buttercup10449(X8) ) ).
fof(sos_10,conjecture,! [X9] : ( k04_buttercup10464(X9) => k04_buttercup10449(X9) ) ).
fof(sos_11,conjecture,! [X10] : ( k04_buttercup10482(X10) => k04_buttercup10477(X10) ) ).
fof(sos_12,conjecture,! [X11] : ( k04_buttercup10486(X11) => k04_buttercup10477(X11) ) ).
fof(sos_13,conjecture,! [X12] : ( k04_buttercup10546(X12) => k04_buttercup10544(X12) ) ).
fof(sos_14,conjecture,! [X13] : ( k04_buttercup10547(X13) => k04_buttercup10544(X13) ) ).
fof(sos_15,conjecture,! [X14] : ( k04_buttercup10406(X14) => k04_buttercup10404(X14) ) ).
fof(sos_16,conjecture,! [X15] : ( k04_buttercup10408(X15) => k04_buttercup10404(X15) ) ).
fof(sos_17,conjecture,! [X16] : ( k04_buttercup10599(X16) => k04_buttercup10593(X16) ) ).
fof(sos_18,conjecture,! [X17] : ( k04_buttercup10602(X17) => k04_buttercup10593(X17) ) ).
fof(sos_19,conjecture,! [X18] : ( k04_buttercup10236(X18) => k04_buttercup10234(X18) ) ).
fof(sos_20,conjecture,! [X19] : ( k04_buttercup10238(X19) => k04_buttercup10234(X19) ) ).
fof(sos_21,conjecture,! [X20] : ( k04_buttercup10371(X20) => k04_buttercup10369(X20) ) ).
fof(sos_22,conjecture,! [X21] : ( k04_buttercup10373(X21) => k04_buttercup10369(X21) ) ).
fof(sos_23,conjecture,! [X22] : ( k04_buttercup10376(X22) => k04_buttercup10369(X22) ) ).
fof(sos_24,conjecture,! [X23] : ( k04_buttercup10296(X23) => k04_buttercup10293(X23) ) ).
fof(sos_25,conjecture,! [X24] : ( k04_buttercup10298(X24) => k04_buttercup10293(X24) ) ).
fof(sos_26,conjecture,! [X25] : ( k04_buttercup10637(X25) => k04_buttercup10635(X25) ) ).
fof(sos_27,conjecture,! [X26] : ( k04_buttercup10639(X26) => k04_buttercup10635(X26) ) ).
fof(sos_28,conjecture,! [X27] : ( k04_buttercup10641(X27) => k04_buttercup10635(X27) ) ).
fof(sos_29,conjecture,! [X28] : ( k04_buttercup10028(X28) => k04_buttercup10026(X28) ) ).
fof(sos_30,conjecture,! [X29] : ( k04_buttercup10033(X29) => k04_buttercup10026(X29) ) ).
fof(sos_31,conjecture,! [X30] : ( k04_buttercup10425(X30) => k04_buttercup10424(X30) ) ).
fof(sos_32,conjecture,! [X31] : ( k04_buttercup10206(X31) => k04_buttercup10204(X31) ) ).
fof(sos_33,conjecture,! [X32] : ( k04_buttercup10213(X32) => k04_buttercup10204(X32) ) ).
fof(sos_34,conjecture,! [X33] : ( k04_buttercup10219(X33) => k04_buttercup10204(X33) ) ).
fof(sos_35,conjecture,! [X34] : ( k04_buttercup10061(X34) => k04_buttercup10057(X34) ) ).
fof(sos_36,conjecture,! [X35] : ( k04_buttercup10064(X35) => k04_buttercup10057(X35) ) ).
fof(sos_37,conjecture,! [X36] : ( k04_buttercup10067(X36) => k04_buttercup10057(X36) ) ).
fof(sos_38,conjecture,! [X37] : ( k04_buttercup10074(X37) => k04_buttercup10057(X37) ) ).
fof(sos_39,conjecture,! [X38] : ( k04_buttercup10559(X38) => k04_buttercup10555(X38) ) ).
fof(sos_40,conjecture,! [X39] : ( k04_buttercup10620(X39) => k04_buttercup10619(X39) ) ).
fof(sos_41,conjecture,! [X40] : ( k04_buttercup10622(X40) => k04_buttercup10619(X40) ) ).
fof(sos_42,conjecture,! [X41] : ( k04_buttercup10506(X41) => k04_buttercup10504(X41) ) ).
fof(sos_43,conjecture,! [X42] : ( k04_buttercup10142(X42) => k04_buttercup10139(X42) ) ).
fof(sos_44,conjecture,! [X43] : ( k04_buttercup10517(X43) => k04_buttercup10516(X43) ) ).
fof(sos_45,conjecture,! [X44] : ( k04_buttercup10184(X44) => k04_buttercup10012(X44) ) ).
fof(sos_46,conjecture,! [X45] : ( k04_buttercup10190(X45) => k04_buttercup10012(X45) ) ).
fof(sos_47,conjecture,! [X46] : ( k04_buttercup10200(X46) => k04_buttercup10012(X46) ) ).
fof(sos_48,conjecture,! [X47] : ( k04_buttercup10204(X47) => k04_buttercup10012(X47) ) ).
fof(sos_49,conjecture,! [X48] : ( k04_buttercup10221(X48) => k04_buttercup10012(X48) ) ).
fof(sos_50,conjecture,! [X49] : ( k04_buttercup10225(X49) => k04_buttercup10012(X49) ) ).
fof(sos_51,conjecture,! [X50] : ( k04_buttercup10234(X50) => k04_buttercup10012(X50) ) ).
fof(sos_52,conjecture,! [X51] : ( k04_buttercup10244(X51) => k04_buttercup10012(X51) ) ).
fof(sos_53,conjecture,! [X52] : ( k04_buttercup10252(X52) => k04_buttercup10012(X52) ) ).
fof(sos_54,conjecture,! [X53] : ( k04_buttercup10282(X53) => k04_buttercup10012(X53) ) ).
fof(sos_55,conjecture,! [X54] : ( k04_buttercup10293(X54) => k04_buttercup10012(X54) ) ).
fof(sos_56,conjecture,! [X55] : ( k04_buttercup10303(X55) => k04_buttercup10012(X55) ) ).
fof(sos_57,conjecture,! [X56] : ( k04_buttercup10312(X56) => k04_buttercup10012(X56) ) ).
fof(sos_58,conjecture,! [X57] : ( k04_buttercup10316(X57) => k04_buttercup10012(X57) ) ).
fof(sos_59,conjecture,! [X58] : ( k04_buttercup10325(X58) => k04_buttercup10012(X58) ) ).
fof(sos_60,conjecture,! [X59] : ( k04_buttercup10329(X59) => k04_buttercup10012(X59) ) ).
fof(sos_61,conjecture,! [X60] : ( k04_buttercup10333(X60) => k04_buttercup10012(X60) ) ).
fof(sos_62,conjecture,! [X61] : ( k04_buttercup10337(X61) => k04_buttercup10012(X61) ) ).
fof(sos_63,conjecture,! [X62] : ( k04_buttercup10356(X62) => k04_buttercup10012(X62) ) ).
fof(sos_64,conjecture,! [X63] : ( k04_buttercup10016(X63) => k04_buttercup10012(X63) ) ).
fof(sos_65,conjecture,! [X64] : ( k04_buttercup10026(X64) => k04_buttercup10012(X64) ) ).
fof(sos_66,conjecture,! [X65] : ( k04_buttercup10039(X65) => k04_buttercup10012(X65) ) ).
fof(sos_67,conjecture,! [X66] : ( k04_buttercup10048(X66) => k04_buttercup10012(X66) ) ).
fof(sos_68,conjecture,! [X67] : ( k04_buttercup10053(X67) => k04_buttercup10012(X67) ) ).
fof(sos_69,conjecture,! [X68] : ( k04_buttercup10057(X68) => k04_buttercup10012(X68) ) ).
fof(sos_70,conjecture,! [X69] : ( k04_buttercup10079(X69) => k04_buttercup10012(X69) ) ).
fof(sos_71,conjecture,! [X70] : ( k04_buttercup10084(X70) => k04_buttercup10012(X70) ) ).
fof(sos_72,conjecture,! [X71] : ( k04_buttercup10089(X71) => k04_buttercup10012(X71) ) ).
fof(sos_73,conjecture,! [X72] : ( k04_buttercup10095(X72) => k04_buttercup10012(X72) ) ).
fof(sos_74,conjecture,! [X73] : ( k04_buttercup10100(X73) => k04_buttercup10012(X73) ) ).
fof(sos_75,conjecture,! [X74] : ( k04_buttercup10117(X74) => k04_buttercup10012(X74) ) ).
fof(sos_76,conjecture,! [X75] : ( k04_buttercup10125(X75) => k04_buttercup10012(X75) ) ).
fof(sos_77,conjecture,! [X76] : ( k04_buttercup10132(X76) => k04_buttercup10012(X76) ) ).
fof(sos_78,conjecture,! [X77] : ( k04_buttercup10135(X77) => k04_buttercup10012(X77) ) ).
fof(sos_79,conjecture,! [X78] : ( k04_buttercup10139(X78) => k04_buttercup10012(X78) ) ).
fof(sos_80,conjecture,! [X79] : ( k04_buttercup10147(X79) => k04_buttercup10012(X79) ) ).
fof(sos_81,conjecture,! [X80] : ( k04_buttercup10153(X80) => k04_buttercup10012(X80) ) ).
fof(sos_82,conjecture,! [X81] : ( k04_buttercup10164(X81) => k04_buttercup10012(X81) ) ).
fof(sos_83,conjecture,! [X82] : ( k04_buttercup10172(X82) => k04_buttercup10012(X82) ) ).
fof(sos_84,conjecture,! [X83] : ( k04_buttercup10181(X83) => k04_buttercup10012(X83) ) ).
fof(sos_85,conjecture,! [X84] : ( k04_buttercup10364(X84) => k04_buttercup10012(X84) ) ).
fof(sos_86,conjecture,! [X85] : ( k04_buttercup10369(X85) => k04_buttercup10012(X85) ) ).
fof(sos_87,conjecture,! [X86] : ( k04_buttercup10380(X86) => k04_buttercup10012(X86) ) ).
fof(sos_88,conjecture,! [X87] : ( k04_buttercup10382(X87) => k04_buttercup10012(X87) ) ).
fof(sos_89,conjecture,! [X88] : ( k04_buttercup10385(X88) => k04_buttercup10012(X88) ) ).
fof(sos_90,conjecture,! [X89] : ( k04_buttercup10389(X89) => k04_buttercup10012(X89) ) ).
fof(sos_91,conjecture,! [X90] : ( k04_buttercup10391(X90) => k04_buttercup10012(X90) ) ).
fof(sos_92,conjecture,! [X91] : ( k04_buttercup10397(X91) => k04_buttercup10012(X91) ) ).
fof(sos_93,conjecture,! [X92] : ( k04_buttercup10400(X92) => k04_buttercup10012(X92) ) ).
fof(sos_94,conjecture,! [X93] : ( k04_buttercup10404(X93) => k04_buttercup10012(X93) ) ).
fof(sos_95,conjecture,! [X94] : ( k04_buttercup10415(X94) => k04_buttercup10012(X94) ) ).
fof(sos_96,conjecture,! [X95] : ( k04_buttercup10419(X95) => k04_buttercup10012(X95) ) ).
fof(sos_97,conjecture,! [X96] : ( k04_buttercup10424(X96) => k04_buttercup10012(X96) ) ).
fof(sos_98,conjecture,! [X97] : ( k04_buttercup10430(X97) => k04_buttercup10012(X97) ) ).
fof(sos_99,conjecture,! [X98] : ( k04_buttercup10437(X98) => k04_buttercup10012(X98) ) ).
fof(sos_100,conjecture,! [X99] : ( k04_buttercup10445(X99) => k04_buttercup10012(X99) ) ).
fof(sos_101,conjecture,! [X100] : ( k04_buttercup10449(X100) => k04_buttercup10012(X100) ) ).
fof(sos_102,conjecture,! [X101] : ( k04_buttercup10470(X101) => k04_buttercup10012(X101) ) ).
fof(sos_103,conjecture,! [X102] : ( k04_buttercup10473(X102) => k04_buttercup10012(X102) ) ).
fof(sos_104,conjecture,! [X103] : ( k04_buttercup10477(X103) => k04_buttercup10012(X103) ) ).
fof(sos_105,conjecture,! [X104] : ( k04_buttercup10492(X104) => k04_buttercup10012(X104) ) ).
fof(sos_106,conjecture,! [X105] : ( k04_buttercup10495(X105) => k04_buttercup10012(X105) ) ).
fof(sos_107,conjecture,! [X106] : ( k04_buttercup10499(X106) => k04_buttercup10012(X106) ) ).
fof(sos_108,conjecture,! [X107] : ( k04_buttercup10504(X107) => k04_buttercup10012(X107) ) ).
fof(sos_109,conjecture,! [X108] : ( k04_buttercup10510(X108) => k04_buttercup10012(X108) ) ).
fof(sos_110,conjecture,! [X109] : ( k04_buttercup10516(X109) => k04_buttercup10012(X109) ) ).
fof(sos_111,conjecture,! [X110] : ( k04_buttercup10524(X110) => k04_buttercup10012(X110) ) ).
fof(sos_112,conjecture,! [X111] : ( k04_buttercup10529(X111) => k04_buttercup10012(X111) ) ).
fof(sos_113,conjecture,! [X112] : ( k04_buttercup10535(X112) => k04_buttercup10012(X112) ) ).
fof(sos_114,conjecture,! [X113] : ( k04_buttercup10544(X113) => k04_buttercup10012(X113) ) ).
fof(sos_115,conjecture,! [X114] : ( k04_buttercup10551(X114) => k04_buttercup10012(X114) ) ).
fof(sos_116,conjecture,! [X115] : ( k04_buttercup10555(X115) => k04_buttercup10012(X115) ) ).
fof(sos_117,conjecture,! [X116] : ( k04_buttercup10567(X116) => k04_buttercup10012(X116) ) ).
fof(sos_118,conjecture,! [X117] : ( k04_buttercup10578(X117) => k04_buttercup10012(X117) ) ).
fof(sos_119,conjecture,! [X118] : ( k04_buttercup10581(X118) => k04_buttercup10012(X118) ) ).
fof(sos_120,conjecture,! [X119] : ( k04_buttercup10586(X119) => k04_buttercup10012(X119) ) ).
fof(sos_121,conjecture,! [X120] : ( k04_buttercup10593(X120) => k04_buttercup10012(X120) ) ).
fof(sos_122,conjecture,! [X121] : ( k04_buttercup10608(X121) => k04_buttercup10012(X121) ) ).
fof(sos_123,conjecture,! [X122] : ( k04_buttercup10611(X122) => k04_buttercup10012(X122) ) ).
fof(sos_124,conjecture,! [X123] : ( k04_buttercup10619(X123) => k04_buttercup10012(X123) ) ).
fof(sos_125,conjecture,! [X124] : ( k04_buttercup10626(X124) => k04_buttercup10012(X124) ) ).
fof(sos_126,conjecture,! [X125] : ( k04_buttercup10628(X125) => k04_buttercup10012(X125) ) ).
fof(sos_127,conjecture,! [X126] : ( k04_buttercup10631(X126) => k04_buttercup10012(X126) ) ).
fof(sos_128,conjecture,! [X127] : ( k04_buttercup10635(X127) => k04_buttercup10012(X127) ) ).
fof(sos_129,conjecture,! [X128] : ( k04_buttercup10643(X128) => k04_buttercup10012(X128) ) ).
fof(sos_130,conjecture,! [X129] : ( b48_buttercup10050(X129) => b48_buttercup10046(X129) ) ).
fof(sos_131,conjecture,! [X130] : ( b48_buttercup10052(X130) => b48_buttercup10046(X130) ) ).
fof(sos_132,conjecture,! [X131] : ( b48_buttercup10305(X131) => b48_buttercup10300(X131) ) ).
fof(sos_133,conjecture,! [X132] : ( b48_buttercup10307(X132) => b48_buttercup10300(X132) ) ).
fof(sos_134,conjecture,! [X133] : ( b48_buttercup10308(X133) => b48_buttercup10300(X133) ) ).
fof(sos_135,conjecture,! [X134] : ( b48_buttercup10227(X134) => b48_buttercup10222(X134) ) ).
fof(sos_136,conjecture,! [X135] : ( b48_buttercup10228(X135) => b48_buttercup10222(X135) ) ).
fof(sos_137,conjecture,! [X136] : ( b48_buttercup10229(X136) => b48_buttercup10222(X136) ) ).
fof(sos_138,conjecture,! [X137] : ( b48_buttercup10191(X137) => b48_buttercup10186(X137) ) ).
fof(sos_139,conjecture,! [X138] : ( b48_buttercup10193(X138) => b48_buttercup10186(X138) ) ).
fof(sos_140,conjecture,! [X139] : ( b48_buttercup10195(X139) => b48_buttercup10186(X139) ) ).
fof(sos_141,conjecture,! [X140] : ( b48_buttercup10133(X140) => b48_buttercup10130(X140) ) ).
fof(sos_142,conjecture,! [X141] : ( b48_buttercup10134(X141) => b48_buttercup10130(X141) ) ).
fof(sos_143,conjecture,! [X142] : ( b48_buttercup10343(X142) => b48_buttercup10334(X142) ) ).
fof(sos_144,conjecture,! [X143] : ( b48_buttercup10344(X143) => b48_buttercup10334(X143) ) ).
fof(sos_145,conjecture,! [X144] : ( b48_buttercup10348(X144) => b48_buttercup10334(X144) ) ).
fof(sos_146,conjecture,! [X145] : ( b48_buttercup10352(X145) => b48_buttercup10334(X145) ) ).
fof(sos_147,conjecture,! [X146] : ( b48_buttercup10267(X146) => b48_buttercup10266(X146) ) ).
fof(sos_148,conjecture,! [X147] : ( b48_buttercup10268(X147) => b48_buttercup10266(X147) ) ).
fof(sos_149,conjecture,! [X148] : ( b48_buttercup10102(X148) => b48_buttercup10098(X148) ) ).
fof(sos_150,conjecture,! [X149] : ( b48_buttercup10104(X149) => b48_buttercup10098(X149) ) ).
fof(sos_151,conjecture,! [X150] : ( b48_buttercup10107(X150) => b48_buttercup10098(X150) ) ).
fof(sos_152,conjecture,! [X151] : ( b48_buttercup10108(X151) => b48_buttercup10098(X151) ) ).
fof(sos_153,conjecture,! [X152] : ( b48_buttercup10109(X152) => b48_buttercup10098(X152) ) ).
fof(sos_154,conjecture,! [X153] : ( b48_buttercup10110(X153) => b48_buttercup10098(X153) ) ).
fof(sos_155,conjecture,! [X154] : ( b48_buttercup10111(X154) => b48_buttercup10098(X154) ) ).
fof(sos_156,conjecture,! [X155] : ( b48_buttercup10441(X155) => b48_buttercup10440(X155) ) ).
fof(sos_157,conjecture,! [X156] : ( b48_buttercup10442(X156) => b48_buttercup10440(X156) ) ).
fof(sos_158,conjecture,! [X157] : ( b48_buttercup10478(X157) => b48_buttercup10474(X157) ) ).
fof(sos_159,conjecture,! [X158] : ( b48_buttercup10479(X158) => b48_buttercup10474(X158) ) ).
fof(sos_160,conjecture,! [X159] : ( b48_buttercup10483(X159) => b48_buttercup10474(X159) ) ).
fof(sos_161,conjecture,! [X160] : ( b48_buttercup10487(X160) => b48_buttercup10474(X160) ) ).
fof(sos_162,conjecture,! [X161] : ( b48_buttercup10489(X161) => b48_buttercup10474(X161) ) ).
fof(sos_163,conjecture,! [X162] : ( b48_buttercup10545(X162) => b48_buttercup10542(X162) ) ).
fof(sos_164,conjecture,! [X163] : ( b48_buttercup10548(X163) => b48_buttercup10542(X163) ) ).
fof(sos_165,conjecture,! [X164] : ( b48_buttercup10275(X164) => b48_buttercup10274(X164) ) ).
fof(sos_166,conjecture,! [X165] : ( b48_buttercup10276(X165) => b48_buttercup10274(X165) ) ).
fof(sos_167,conjecture,! [X166] : ( b48_buttercup10277(X166) => b48_buttercup10274(X166) ) ).
fof(sos_168,conjecture,! [X167] : ( b48_buttercup10278(X167) => b48_buttercup10274(X167) ) ).
fof(sos_169,conjecture,! [X168] : ( b48_buttercup10405(X168) => b48_buttercup10402(X168) ) ).
fof(sos_170,conjecture,! [X169] : ( b48_buttercup10410(X169) => b48_buttercup10402(X169) ) ).
fof(sos_171,conjecture,! [X170] : ( b48_buttercup10166(X170) => b48_buttercup10161(X170) ) ).
fof(sos_172,conjecture,! [X171] : ( b48_buttercup10167(X171) => b48_buttercup10161(X171) ) ).
fof(sos_173,conjecture,! [X172] : ( b48_buttercup10169(X172) => b48_buttercup10161(X172) ) ).
fof(sos_174,conjecture,! [X173] : ( b48_buttercup10119(X173) => b48_buttercup10115(X173) ) ).
fof(sos_175,conjecture,! [X174] : ( b48_buttercup10120(X174) => b48_buttercup10115(X174) ) ).
fof(sos_176,conjecture,! [X175] : ( b48_buttercup10596(X175) => b48_buttercup10589(X175) ) ).
fof(sos_177,conjecture,! [X176] : ( b48_buttercup10604(X176) => b48_buttercup10589(X176) ) ).
fof(sos_178,conjecture,! [X177] : ( b48_buttercup10370(X177) => b48_buttercup10367(X177) ) ).
fof(sos_179,conjecture,! [X178] : ( b48_buttercup10374(X178) => b48_buttercup10367(X178) ) ).
fof(sos_180,conjecture,! [X179] : ( b48_buttercup10377(X179) => b48_buttercup10367(X179) ) ).
fof(sos_181,conjecture,! [X180] : ( b48_buttercup10294(X180) => b48_buttercup10291(X180) ) ).
fof(sos_182,conjecture,! [X181] : ( b48_buttercup10299(X181) => b48_buttercup10291(X181) ) ).
fof(sos_183,conjecture,! [X182] : ( b48_buttercup10318(X182) => b48_buttercup10313(X182) ) ).
fof(sos_184,conjecture,! [X183] : ( b48_buttercup10320(X183) => b48_buttercup10313(X183) ) ).
fof(sos_185,conjecture,! [X184] : ( b48_buttercup10173(X184) => b48_buttercup10170(X184) ) ).
fof(sos_186,conjecture,! [X185] : ( b48_buttercup10174(X185) => b48_buttercup10170(X185) ) ).
fof(sos_187,conjecture,! [X186] : ( b48_buttercup10636(X186) => b48_buttercup10632(X186) ) ).
fof(sos_188,conjecture,! [X187] : ( b48_buttercup10638(X187) => b48_buttercup10632(X187) ) ).
fof(sos_189,conjecture,! [X188] : ( b48_buttercup10640(X188) => b48_buttercup10632(X188) ) ).
fof(sos_190,conjecture,! [X189] : ( b48_buttercup10029(X189) => b48_buttercup10024(X189) ) ).
fof(sos_191,conjecture,! [X190] : ( b48_buttercup10031(X190) => b48_buttercup10024(X190) ) ).
fof(sos_192,conjecture,! [X191] : ( b48_buttercup10034(X191) => b48_buttercup10024(X191) ) ).
fof(sos_193,conjecture,! [X192] : ( b48_buttercup10574(X192) => b48_buttercup10563(X192) ) ).
fof(sos_194,conjecture,! [X193] : ( b48_buttercup10154(X193) => b48_buttercup10150(X193) ) ).
fof(sos_195,conjecture,! [X194] : ( b48_buttercup10156(X194) => b48_buttercup10150(X194) ) ).
fof(sos_196,conjecture,! [X195] : ( b48_buttercup10158(X195) => b48_buttercup10150(X195) ) ).
fof(sos_197,conjecture,! [X196] : ( b48_buttercup10159(X196) => b48_buttercup10150(X196) ) ).
fof(sos_198,conjecture,! [X197] : ( b48_buttercup10160(X197) => b48_buttercup10150(X197) ) ).
fof(sos_199,conjecture,! [X198] : ( b48_buttercup10208(X198) => b48_buttercup10201(X198) ) ).
fof(sos_200,conjecture,! [X199] : ( b48_buttercup10210(X199) => b48_buttercup10201(X199) ) ).
fof(sos_201,conjecture,! [X200] : ( b48_buttercup10214(X200) => b48_buttercup10201(X200) ) ).
fof(sos_202,conjecture,! [X201] : ( b48_buttercup10217(X201) => b48_buttercup10201(X201) ) ).
fof(sos_203,conjecture,! [X202] : ( b48_buttercup10220(X202) => b48_buttercup10201(X202) ) ).
fof(sos_204,conjecture,! [X203] : ( b48_buttercup10513(X203) => b48_buttercup10512(X203) ) ).
fof(sos_205,conjecture,! [X204] : ( b48_buttercup10514(X204) => b48_buttercup10512(X204) ) ).
fof(sos_206,conjecture,! [X205] : ( b48_buttercup10058(X205) => b48_buttercup10054(X205) ) ).
fof(sos_207,conjecture,! [X206] : ( b48_buttercup10065(X206) => b48_buttercup10054(X206) ) ).
fof(sos_208,conjecture,! [X207] : ( b48_buttercup10068(X207) => b48_buttercup10054(X207) ) ).
fof(sos_209,conjecture,! [X208] : ( b48_buttercup10070(X208) => b48_buttercup10054(X208) ) ).
fof(sos_210,conjecture,! [X209] : ( b48_buttercup10072(X209) => b48_buttercup10054(X209) ) ).
fof(sos_211,conjecture,! [X210] : ( b48_buttercup10075(X210) => b48_buttercup10054(X210) ) ).
fof(sos_212,conjecture,! [X211] : ( b48_buttercup10561(X211) => b48_buttercup10552(X211) ) ).
fof(sos_213,conjecture,! [X212] : ( b48_buttercup10562(X212) => b48_buttercup10552(X212) ) ).
fof(sos_214,conjecture,! [X213] : ( b48_buttercup10518(X213) => b48_buttercup10515(X213) ) ).
fof(sos_215,conjecture,! [X214] : ( b48_buttercup10519(X214) => b48_buttercup10515(X214) ) ).
fof(sos_216,conjecture,! [X215] : ( b48_buttercup10520(X215) => b48_buttercup10515(X215) ) ).
fof(sos_217,conjecture,! [X216] : ( b48_buttercup10521(X216) => b48_buttercup10515(X216) ) ).
fof(sos_218,conjecture,! [X217] : ( b48_buttercup10273(X217) => b48_buttercup10271(X217) ) ).
fof(sos_219,conjecture,! [X218] : ( b48_buttercup10186(X218) => b48_buttercup10007(X218) ) ).
fof(sos_220,conjecture,! [X219] : ( b48_buttercup10196(X219) => b48_buttercup10007(X219) ) ).
fof(sos_221,conjecture,! [X220] : ( b48_buttercup10197(X220) => b48_buttercup10007(X220) ) ).
fof(sos_222,conjecture,! [X221] : ( b48_buttercup10198(X221) => b48_buttercup10007(X221) ) ).
fof(sos_223,conjecture,! [X222] : ( b48_buttercup10199(X222) => b48_buttercup10007(X222) ) ).
fof(sos_224,conjecture,! [X223] : ( b48_buttercup10201(X223) => b48_buttercup10007(X223) ) ).
fof(sos_225,conjecture,! [X224] : ( b48_buttercup10222(X224) => b48_buttercup10007(X224) ) ).
fof(sos_226,conjecture,! [X225] : ( b48_buttercup10231(X225) => b48_buttercup10007(X225) ) ).
fof(sos_227,conjecture,! [X226] : ( b48_buttercup10240(X226) => b48_buttercup10007(X226) ) ).
fof(sos_228,conjecture,! [X227] : ( b48_buttercup10247(X227) => b48_buttercup10007(X227) ) ).
fof(sos_229,conjecture,! [X228] : ( b48_buttercup10248(X228) => b48_buttercup10007(X228) ) ).
fof(sos_230,conjecture,! [X229] : ( b48_buttercup10266(X229) => b48_buttercup10007(X229) ) ).
fof(sos_231,conjecture,! [X230] : ( b48_buttercup10269(X230) => b48_buttercup10007(X230) ) ).
fof(sos_232,conjecture,! [X231] : ( b48_buttercup10271(X231) => b48_buttercup10007(X231) ) ).
fof(sos_233,conjecture,! [X232] : ( b48_buttercup10272(X232) => b48_buttercup10007(X232) ) ).
fof(sos_234,conjecture,! [X233] : ( b48_buttercup10274(X233) => b48_buttercup10007(X233) ) ).
fof(sos_235,conjecture,! [X234] : ( b48_buttercup10279(X234) => b48_buttercup10007(X234) ) ).
fof(sos_236,conjecture,! [X235] : ( b48_buttercup10291(X235) => b48_buttercup10007(X235) ) ).
fof(sos_237,conjecture,! [X236] : ( b48_buttercup10300(X236) => b48_buttercup10007(X236) ) ).
fof(sos_238,conjecture,! [X237] : ( b48_buttercup10309(X237) => b48_buttercup10007(X237) ) ).
fof(sos_239,conjecture,! [X238] : ( b48_buttercup10313(X238) => b48_buttercup10007(X238) ) ).
fof(sos_240,conjecture,! [X239] : ( b48_buttercup10322(X239) => b48_buttercup10007(X239) ) ).
fof(sos_241,conjecture,! [X240] : ( b48_buttercup10326(X240) => b48_buttercup10007(X240) ) ).
fof(sos_242,conjecture,! [X241] : ( b48_buttercup10332(X241) => b48_buttercup10007(X241) ) ).
fof(sos_243,conjecture,! [X242] : ( b48_buttercup10334(X242) => b48_buttercup10007(X242) ) ).
fof(sos_244,conjecture,! [X243] : ( b48_buttercup10353(X243) => b48_buttercup10007(X243) ) ).
fof(sos_245,conjecture,! [X244] : ( b48_buttercup10362(X244) => b48_buttercup10007(X244) ) ).
fof(sos_246,conjecture,! [X245] : ( b48_buttercup10013(X245) => b48_buttercup10007(X245) ) ).
fof(sos_247,conjecture,! [X246] : ( b48_buttercup10024(X246) => b48_buttercup10007(X246) ) ).
fof(sos_248,conjecture,! [X247] : ( b48_buttercup10035(X247) => b48_buttercup10007(X247) ) ).
fof(sos_249,conjecture,! [X248] : ( b48_buttercup10046(X248) => b48_buttercup10007(X248) ) ).
fof(sos_250,conjecture,! [X249] : ( b48_buttercup10054(X249) => b48_buttercup10007(X249) ) ).
fof(sos_251,conjecture,! [X250] : ( b48_buttercup10076(X250) => b48_buttercup10007(X250) ) ).
fof(sos_252,conjecture,! [X251] : ( b48_buttercup10082(X251) => b48_buttercup10007(X251) ) ).
fof(sos_253,conjecture,! [X252] : ( b48_buttercup10085(X252) => b48_buttercup10007(X252) ) ).
fof(sos_254,conjecture,! [X253] : ( b48_buttercup10086(X253) => b48_buttercup10007(X253) ) ).
fof(sos_255,conjecture,! [X254] : ( b48_buttercup10092(X254) => b48_buttercup10007(X254) ) ).
fof(sos_256,conjecture,! [X255] : ( b48_buttercup10098(X255) => b48_buttercup10007(X255) ) ).
fof(sos_257,conjecture,! [X256] : ( b48_buttercup10115(X256) => b48_buttercup10007(X256) ) ).
fof(sos_258,conjecture,! [X257] : ( b48_buttercup10121(X257) => b48_buttercup10007(X257) ) ).
fof(sos_259,conjecture,! [X258] : ( b48_buttercup10130(X258) => b48_buttercup10007(X258) ) ).
fof(sos_260,conjecture,! [X259] : ( b48_buttercup10143(X259) => b48_buttercup10007(X259) ) ).
fof(sos_261,conjecture,! [X260] : ( b48_buttercup10150(X260) => b48_buttercup10007(X260) ) ).
fof(sos_262,conjecture,! [X261] : ( b48_buttercup10161(X261) => b48_buttercup10007(X261) ) ).
fof(sos_263,conjecture,! [X262] : ( b48_buttercup10170(X262) => b48_buttercup10007(X262) ) ).
fof(sos_264,conjecture,! [X263] : ( b48_buttercup10176(X263) => b48_buttercup10007(X263) ) ).
fof(sos_265,conjecture,! [X264] : ( b48_buttercup10180(X264) => b48_buttercup10007(X264) ) ).
fof(sos_266,conjecture,! [X265] : ( b48_buttercup10182(X265) => b48_buttercup10007(X265) ) ).
fof(sos_267,conjecture,! [X266] : ( b48_buttercup10365(X266) => b48_buttercup10007(X266) ) ).
fof(sos_268,conjecture,! [X267] : ( b48_buttercup10367(X267) => b48_buttercup10007(X267) ) ).
fof(sos_269,conjecture,! [X268] : ( b48_buttercup10378(X268) => b48_buttercup10007(X268) ) ).
fof(sos_270,conjecture,! [X269] : ( b48_buttercup10381(X269) => b48_buttercup10007(X269) ) ).
fof(sos_271,conjecture,! [X270] : ( b48_buttercup10383(X270) => b48_buttercup10007(X270) ) ).
fof(sos_272,conjecture,! [X271] : ( b48_buttercup10386(X271) => b48_buttercup10007(X271) ) ).
fof(sos_273,conjecture,! [X272] : ( b48_buttercup10394(X272) => b48_buttercup10007(X272) ) ).
fof(sos_274,conjecture,! [X273] : ( b48_buttercup10398(X273) => b48_buttercup10007(X273) ) ).
fof(sos_275,conjecture,! [X274] : ( b48_buttercup10402(X274) => b48_buttercup10007(X274) ) ).
fof(sos_276,conjecture,! [X275] : ( b48_buttercup10411(X275) => b48_buttercup10007(X275) ) ).
fof(sos_277,conjecture,! [X276] : ( b48_buttercup10417(X276) => b48_buttercup10007(X276) ) ).
fof(sos_278,conjecture,! [X277] : ( b48_buttercup10420(X277) => b48_buttercup10007(X277) ) ).
fof(sos_279,conjecture,! [X278] : ( b48_buttercup10427(X278) => b48_buttercup10007(X278) ) ).
fof(sos_280,conjecture,! [X279] : ( b48_buttercup10433(X279) => b48_buttercup10007(X279) ) ).
fof(sos_281,conjecture,! [X280] : ( b48_buttercup10434(X280) => b48_buttercup10007(X280) ) ).
fof(sos_282,conjecture,! [X281] : ( b48_buttercup10440(X281) => b48_buttercup10007(X281) ) ).
fof(sos_283,conjecture,! [X282] : ( b48_buttercup10443(X282) => b48_buttercup10007(X282) ) ).
fof(sos_284,conjecture,! [X283] : ( b48_buttercup10446(X283) => b48_buttercup10007(X283) ) ).
fof(sos_285,conjecture,! [X284] : ( b48_buttercup10450(X284) => b48_buttercup10007(X284) ) ).
fof(sos_286,conjecture,! [X285] : ( b48_buttercup10469(X285) => b48_buttercup10007(X285) ) ).
fof(sos_287,conjecture,! [X286] : ( b48_buttercup10471(X286) => b48_buttercup10007(X286) ) ).
fof(sos_288,conjecture,! [X287] : ( b48_buttercup10474(X287) => b48_buttercup10007(X287) ) ).
fof(sos_289,conjecture,! [X288] : ( b48_buttercup10490(X288) => b48_buttercup10007(X288) ) ).
fof(sos_290,conjecture,! [X289] : ( b48_buttercup10493(X289) => b48_buttercup10007(X289) ) ).
fof(sos_291,conjecture,! [X290] : ( b48_buttercup10496(X290) => b48_buttercup10007(X290) ) ).
fof(sos_292,conjecture,! [X291] : ( b48_buttercup10502(X291) => b48_buttercup10007(X291) ) ).
fof(sos_293,conjecture,! [X292] : ( b48_buttercup10507(X292) => b48_buttercup10007(X292) ) ).
fof(sos_294,conjecture,! [X293] : ( b48_buttercup10512(X293) => b48_buttercup10007(X293) ) ).
fof(sos_295,conjecture,! [X294] : ( b48_buttercup10515(X294) => b48_buttercup10007(X294) ) ).
fof(sos_296,conjecture,! [X295] : ( b48_buttercup10522(X295) => b48_buttercup10007(X295) ) ).
fof(sos_297,conjecture,! [X296] : ( b48_buttercup10526(X296) => b48_buttercup10007(X296) ) ).
fof(sos_298,conjecture,! [X297] : ( b48_buttercup10530(X297) => b48_buttercup10007(X297) ) ).
fof(sos_299,conjecture,! [X298] : ( b48_buttercup10531(X298) => b48_buttercup10007(X298) ) ).
fof(sos_300,conjecture,! [X299] : ( b48_buttercup10542(X299) => b48_buttercup10007(X299) ) ).
fof(sos_301,conjecture,! [X300] : ( b48_buttercup10549(X300) => b48_buttercup10007(X300) ) ).
fof(sos_302,conjecture,! [X301] : ( b48_buttercup10552(X301) => b48_buttercup10007(X301) ) ).
fof(sos_303,conjecture,! [X302] : ( b48_buttercup10563(X302) => b48_buttercup10007(X302) ) ).
fof(sos_304,conjecture,! [X303] : ( b48_buttercup10570(X303) => b48_buttercup10007(X303) ) ).
fof(sos_305,conjecture,! [X304] : ( b48_buttercup10572(X304) => b48_buttercup10007(X304) ) ).
fof(sos_306,conjecture,! [X305] : ( b48_buttercup10575(X305) => b48_buttercup10007(X305) ) ).
fof(sos_307,conjecture,! [X306] : ( b48_buttercup10579(X306) => b48_buttercup10007(X306) ) ).
fof(sos_308,conjecture,! [X307] : ( b48_buttercup10582(X307) => b48_buttercup10007(X307) ) ).
fof(sos_309,conjecture,! [X308] : ( b48_buttercup10589(X308) => b48_buttercup10007(X308) ) ).
fof(sos_310,conjecture,! [X309] : ( b48_buttercup10605(X309) => b48_buttercup10007(X309) ) ).
fof(sos_311,conjecture,! [X310] : ( b48_buttercup10606(X310) => b48_buttercup10007(X310) ) ).
fof(sos_312,conjecture,! [X311] : ( b48_buttercup10609(X311) => b48_buttercup10007(X311) ) ).
fof(sos_313,conjecture,! [X312] : ( b48_buttercup10612(X312) => b48_buttercup10007(X312) ) ).
fof(sos_314,conjecture,! [X313] : ( b48_buttercup10616(X313) => b48_buttercup10007(X313) ) ).
fof(sos_315,conjecture,! [X314] : ( b48_buttercup10624(X314) => b48_buttercup10007(X314) ) ).
fof(sos_316,conjecture,! [X315] : ( b48_buttercup10629(X315) => b48_buttercup10007(X315) ) ).
fof(sos_317,conjecture,! [X316] : ( b48_buttercup10632(X316) => b48_buttercup10007(X316) ) ).
fof(sos_318,conjecture,! [X317] : ( b48_buttercup10642(X317) => b48_buttercup10007(X317) ) ).
fof(sos_319,conjecture,! [X318] : ( b48_buttercup10646(X318) => b48_buttercup10007(X318) ) ).
fof(sos_320,conjecture,! [X319] : ( b48_buttercup10305(X319) => k04_buttercup10303(X319) ) & ? [X320] : ( k04_buttercup10303(X320) & ~ b48_buttercup10305(X320) ) ).
fof(sos_321,conjecture,! [X321] : ( k04_buttercup10298(X321) <=> b48_buttercup10299(X321) ) ).
fof(sos_322,conjecture,! [X322] : ( k04_buttercup10303(X322) <=> b48_buttercup10300(X322) ) ).
fof(sos_323,conjecture,! [X323] : ( b48_buttercup10307(X323) => k04_buttercup10303(X323) ) & ? [X324] : ( k04_buttercup10303(X324) & ~ b48_buttercup10307(X324) ) ).
fof(sos_324,conjecture,! [X325] : ( k04_buttercup10643(X325) <=> b48_buttercup10642(X325) ) ).
fof(sos_325,conjecture,! [X326] : ( k04_buttercup10641(X326) <=> b48_buttercup10640(X326) ) ).
fof(sos_326,conjecture,! [X327] : ( k04_buttercup10639(X327) <=> b48_buttercup10638(X327) ) ).
fof(sos_327,conjecture,! [X328] : ( k04_buttercup10637(X328) <=> b48_buttercup10636(X328) ) ).
fof(sos_328,conjecture,! [X329] : ( k04_buttercup10252(X329) <=> b48_buttercup10248(X329) ) ).
fof(sos_329,conjecture,! [X330] : ( k04_buttercup10535(X330) <=> b48_buttercup10531(X330) ) ).
fof(sos_330,conjecture,! [X331] : ( b48_buttercup10156(X331) => k04_buttercup10153(X331) ) & ? [X332] : ( k04_buttercup10153(X332) & ~ b48_buttercup10156(X332) ) ).
fof(sos_331,conjecture,! [X333] : ( b48_buttercup10154(X333) => k04_buttercup10153(X333) ) & ? [X334] : ( k04_buttercup10153(X334) & ~ b48_buttercup10154(X334) ) ).
fof(sos_332,conjecture,! [X335] : ( k04_buttercup10153(X335) <=> b48_buttercup10150(X335) ) ).
fof(sos_333,conjecture,! [X336] : ( b48_buttercup10227(X336) => k04_buttercup10225(X336) ) & ? [X337] : ( k04_buttercup10225(X337) & ~ b48_buttercup10227(X337) ) ).
fof(sos_334,conjecture,! [X338] : ( b48_buttercup10229(X338) => k04_buttercup10225(X338) ) & ? [X339] : ( k04_buttercup10225(X339) & ~ b48_buttercup10229(X339) ) ).
fof(sos_335,conjecture,! [X340] : ( k04_buttercup10234(X340) <=> b48_buttercup10231(X340) ) ).
fof(sos_336,conjecture,! [X341] : ( b48_buttercup10465(X341) => k04_buttercup10464(X341) ) & ? [X342] : ( k04_buttercup10464(X342) & ~ b48_buttercup10465(X342) ) ).
fof(sos_337,conjecture,! [X343] : ( b48_buttercup10466(X343) => k04_buttercup10464(X343) ) & ? [X344] : ( k04_buttercup10464(X344) & ~ b48_buttercup10466(X344) ) ).
fof(sos_338,conjecture,! [X345] : ( b48_buttercup10467(X345) => k04_buttercup10464(X345) ) & ? [X346] : ( k04_buttercup10464(X346) & ~ b48_buttercup10467(X346) ) ).
fof(sos_339,conjecture,! [X347] : ( b48_buttercup10456(X347) => k04_buttercup10464(X347) ) & ? [X348] : ( k04_buttercup10464(X348) & ~ b48_buttercup10456(X348) ) ).
fof(sos_340,conjecture,? [X349] : ? [X350] : ? [X351] : ( k04_buttercup10464(X349) & b48_buttercup10458(X349) & k04_buttercup10464(X350) & ~ b48_buttercup10458(X350) & ~ k04_buttercup10464(X351) & b48_buttercup10458(X351) ) ).
fof(sos_341,conjecture,! [X352] : ( k04_buttercup10397(X352) <=> b48_buttercup10394(X352) ) ).
fof(sos_342,conjecture,! [X353] : ( k04_buttercup10391(X353) <=> b48_buttercup10616(X353) ) ).
fof(sos_343,conjecture,! [X354] : ( k04_buttercup10089(X354) <=> b48_buttercup10086(X354) ) ).
fof(sos_344,conjecture,! [X355] : ( k04_buttercup10079(X355) <=> b48_buttercup10076(X355) ) ).
fof(sos_345,conjecture,! [X356] : ( k04_buttercup10084(X356) <=> b48_buttercup10082(X356) ) ).
fof(sos_346,conjecture,? [X357] : ? [X358] : ? [X359] : ( k04_buttercup10026(X357) & b48_buttercup10029(X357) & k04_buttercup10026(X358) & ~ b48_buttercup10029(X358) & ~ k04_buttercup10026(X359) & b48_buttercup10029(X359) ) | ( ! [X360] : ( b48_buttercup10029(X360) => k04_buttercup10026(X360) ) & ? [X361] : ( k04_buttercup10026(X361) & ~ b48_buttercup10029(X361) ) ) | ( ! [X362] : ( k04_buttercup10026(X362) => b48_buttercup10029(X362) ) & ? [X363] : ( b48_buttercup10029(X363) & ~ k04_buttercup10026(X363) ) ) | ! [X364] : ( k04_buttercup10026(X364) => ~ b48_buttercup10029(X364) ) ).
fof(sos_347,conjecture,! [X365] : ( b48_buttercup10022(X365) => k04_buttercup10016(X365) ) & ? [X366] : ( k04_buttercup10016(X366) & ~ b48_buttercup10022(X366) ) ).
fof(sos_348,conjecture,! [X367] : ( b48_buttercup10021(X367) => k04_buttercup10016(X367) ) & ? [X368] : ( k04_buttercup10016(X368) & ~ b48_buttercup10021(X368) ) ).
fof(sos_349,conjecture,! [X369] : ( b48_buttercup10019(X369) => k04_buttercup10016(X369) ) & ? [X370] : ( k04_buttercup10016(X370) & ~ b48_buttercup10019(X370) ) ).
fof(sos_350,conjecture,! [X371] : ( k04_buttercup10026(X371) => b48_buttercup10024(X371) ) & ? [X372] : ( b48_buttercup10024(X372) & ~ k04_buttercup10026(X372) ) ).
fof(sos_351,conjecture,! [X373] : ( k04_buttercup10581(X373) <=> b48_buttercup10579(X373) ) ).
fof(sos_352,conjecture,! [X374] : ( k04_buttercup10586(X374) <=> b48_buttercup10582(X374) ) ).
fof(sos_353,conjecture,! [X375] : ( k04_buttercup10389(X375) <=> b48_buttercup10386(X375) ) ).
fof(sos_354,conjecture,! [X376] : ( k04_buttercup10385(X376) <=> b48_buttercup10269(X376) ) ).
fof(sos_355,conjecture,! [X377] : ( k04_buttercup10382(X377) <=> b48_buttercup10383(X377) ) ).
fof(sos_356,conjecture,! [X378] : ( k04_buttercup10296(X378) <=> b48_buttercup10294(X378) ) ).
fof(sos_357,conjecture,! [X379] : ( k04_buttercup10293(X379) <=> b48_buttercup10291(X379) ) ).
fof(sos_358,conjecture,! [X380] : ( k04_buttercup10288(X380) <=> b48_buttercup10290(X380) ) ).
fof(sos_359,conjecture,! [X381] : ( k04_buttercup10067(X381) <=> b48_buttercup10065(X381) ) ).
fof(sos_360,conjecture,! [X382] : ( k04_buttercup10074(X382) <=> b48_buttercup10072(X382) ) ).
fof(sos_361,conjecture,! [X383] : ( k04_buttercup10495(X383) <=> b48_buttercup10493(X383) ) ).
fof(sos_362,conjecture,! [X384] : ( k04_buttercup10492(X384) <=> b48_buttercup10490(X384) ) ).
fof(sos_363,conjecture,! [X385] : ( b48_buttercup10487(X385) => k04_buttercup10486(X385) ) & ? [X386] : ( k04_buttercup10486(X386) & ~ b48_buttercup10487(X386) ) ).
fof(sos_364,conjecture,! [X387] : ( b48_buttercup10489(X387) => k04_buttercup10486(X387) ) & ? [X388] : ( k04_buttercup10486(X388) & ~ b48_buttercup10489(X388) ) ).
fof(sos_365,conjecture,! [X389] : ( k04_buttercup10200(X389) <=> b48_buttercup10199(X389) ) ).
fof(sos_366,conjecture,! [X390] : ( k04_buttercup10204(X390) => b48_buttercup10201(X390) ) & ? [X391] : ( b48_buttercup10201(X391) & ~ k04_buttercup10204(X391) ) ).
fof(sos_367,conjecture,! [X392] : ( b48_buttercup10193(X392) => k04_buttercup10190(X392) ) & ? [X393] : ( k04_buttercup10190(X393) & ~ b48_buttercup10193(X393) ) ).
fof(sos_368,conjecture,! [X394] : ( b48_buttercup10195(X394) => k04_buttercup10190(X394) ) & ? [X395] : ( k04_buttercup10190(X395) & ~ b48_buttercup10195(X395) ) ).
fof(sos_369,conjecture,! [X396] : ( k04_buttercup10551(X396) <=> b48_buttercup10549(X396) ) ).
fof(sos_370,conjecture,! [X397] : ( k04_buttercup10546(X397) <=> b48_buttercup10545(X397) ) ).
fof(sos_371,conjecture,! [X398] : ( k04_buttercup10547(X398) <=> b48_buttercup10548(X398) ) ).
fof(sos_372,conjecture,! [X399] : ( b48_buttercup10102(X399) => k04_buttercup10622(X399) ) & ? [X400] : ( k04_buttercup10622(X400) & ~ b48_buttercup10102(X400) ) ).
fof(sos_373,conjecture,? [X401] : ? [X402] : ? [X403] : ( k04_buttercup10619(X401) & b48_buttercup10111(X401) & k04_buttercup10619(X402) & ~ b48_buttercup10111(X402) & ~ k04_buttercup10619(X403) & b48_buttercup10111(X403) ) | ( ! [X404] : ( b48_buttercup10111(X404) => k04_buttercup10619(X404) ) & ? [X405] : ( k04_buttercup10619(X405) & ~ b48_buttercup10111(X405) ) ) | ( ! [X406] : ( k04_buttercup10619(X406) => b48_buttercup10111(X406) ) & ? [X407] : ( b48_buttercup10111(X407) & ~ k04_buttercup10619(X407) ) ) | ! [X408] : ( k04_buttercup10619(X408) => ~ b48_buttercup10111(X408) ) ).
fof(sos_374,conjecture,? [X409] : ? [X410] : ? [X411] : ( k04_buttercup10619(X409) & b48_buttercup10109(X409) & k04_buttercup10619(X410) & ~ b48_buttercup10109(X410) & ~ k04_buttercup10619(X411) & b48_buttercup10109(X411) ) | ( ! [X412] : ( b48_buttercup10109(X412) => k04_buttercup10619(X412) ) & ? [X413] : ( k04_buttercup10619(X413) & ~ b48_buttercup10109(X413) ) ) | ( ! [X414] : ( k04_buttercup10619(X414) => b48_buttercup10109(X414) ) & ? [X415] : ( b48_buttercup10109(X415) & ~ k04_buttercup10619(X415) ) ) | ! [X416] : ( k04_buttercup10619(X416) => ~ b48_buttercup10109(X416) ) ).
fof(sos_375,conjecture,! [X417] : ( k04_buttercup10620(X417) <=> b48_buttercup10107(X417) ) ).
fof(sos_376,conjecture,! [X418] : ( k04_buttercup10619(X418) => b48_buttercup10098(X418) ) & ? [X419] : ( b48_buttercup10098(X419) & ~ k04_buttercup10619(X419) ) ).
fof(sos_377,conjecture,? [X420] : ? [X421] : ? [X422] : ( k04_buttercup10100(X420) & b48_buttercup10108(X420) & k04_buttercup10100(X421) & ~ b48_buttercup10108(X421) & ~ k04_buttercup10100(X422) & b48_buttercup10108(X422) ) | ( ! [X423] : ( b48_buttercup10108(X423) => k04_buttercup10100(X423) ) & ? [X424] : ( k04_buttercup10100(X424) & ~ b48_buttercup10108(X424) ) ) | ( ! [X425] : ( k04_buttercup10100(X425) => b48_buttercup10108(X425) ) & ? [X426] : ( b48_buttercup10108(X426) & ~ k04_buttercup10100(X426) ) ) | ! [X427] : ( k04_buttercup10100(X427) => ~ b48_buttercup10108(X427) ) ).
fof(sos_378,conjecture,? [X428] : ? [X429] : ? [X430] : ( k04_buttercup10100(X428) & b48_buttercup10107(X428) & k04_buttercup10100(X429) & ~ b48_buttercup10107(X429) & ~ k04_buttercup10100(X430) & b48_buttercup10107(X430) ) | ( ! [X431] : ( b48_buttercup10107(X431) => k04_buttercup10100(X431) ) & ? [X432] : ( k04_buttercup10100(X432) & ~ b48_buttercup10107(X432) ) ) | ( ! [X433] : ( k04_buttercup10100(X433) => b48_buttercup10107(X433) ) & ? [X434] : ( b48_buttercup10107(X434) & ~ k04_buttercup10100(X434) ) ) | ! [X435] : ( k04_buttercup10100(X435) => ~ b48_buttercup10107(X435) ) ).
fof(sos_379,conjecture,? [X436] : ? [X437] : ? [X438] : ( k04_buttercup10100(X436) & b48_buttercup10104(X436) & k04_buttercup10100(X437) & ~ b48_buttercup10104(X437) & ~ k04_buttercup10100(X438) & b48_buttercup10104(X438) ) | ( ! [X439] : ( b48_buttercup10104(X439) => k04_buttercup10100(X439) ) & ? [X440] : ( k04_buttercup10100(X440) & ~ b48_buttercup10104(X440) ) ) | ( ! [X441] : ( k04_buttercup10100(X441) => b48_buttercup10104(X441) ) & ? [X442] : ( b48_buttercup10104(X442) & ~ k04_buttercup10100(X442) ) ) | ! [X443] : ( k04_buttercup10100(X443) => ~ b48_buttercup10104(X443) ) ).
fof(sos_380,conjecture,! [X444] : ( b48_buttercup10111(X444) => k04_buttercup10100(X444) ) & ? [X445] : ( k04_buttercup10100(X445) & ~ b48_buttercup10111(X445) ) ).
fof(sos_381,conjecture,? [X446] : ? [X447] : ? [X448] : ( k04_buttercup10100(X446) & b48_buttercup10110(X446) & k04_buttercup10100(X447) & ~ b48_buttercup10110(X447) & ~ k04_buttercup10100(X448) & b48_buttercup10110(X448) ) | ( ! [X449] : ( b48_buttercup10110(X449) => k04_buttercup10100(X449) ) & ? [X450] : ( k04_buttercup10100(X450) & ~ b48_buttercup10110(X450) ) ) | ( ! [X451] : ( k04_buttercup10100(X451) => b48_buttercup10110(X451) ) & ? [X452] : ( b48_buttercup10110(X452) & ~ k04_buttercup10100(X452) ) ) | ! [X453] : ( k04_buttercup10100(X453) => ~ b48_buttercup10110(X453) ) ).
fof(sos_382,conjecture,! [X454] : ( b48_buttercup10109(X454) => k04_buttercup10100(X454) ) & ? [X455] : ( k04_buttercup10100(X455) & ~ b48_buttercup10109(X455) ) ).
fof(sos_383,conjecture,! [X456] : ( k04_buttercup10437(X456) <=> b48_buttercup10434(X456) ) ).
fof(sos_384,conjecture,! [X457] : ( k04_buttercup10016(X457) <=> b48_buttercup10013(X457) ) ).
fof(sos_385,conjecture,! [X458] : ( k04_buttercup10356(X458) <=> b48_buttercup10353(X458) ) ).
fof(sos_386,conjecture,! [X459] : ( k04_buttercup10357(X459) <=> b48_buttercup10361(X459) ) ).
fof(sos_387,conjecture,! [X460] : ( b48_buttercup10334(X460) => k04_buttercup10337(X460) ) & ? [X461] : ( k04_buttercup10337(X461) & ~ b48_buttercup10334(X461) ) ).
fof(sos_388,conjecture,! [X462] : ( k04_buttercup10333(X462) <=> b48_buttercup10332(X462) ) ).
fof(sos_389,conjecture,! [X463] : ( k04_buttercup10635(X463) <=> b48_buttercup10632(X463) ) ).
fof(sos_390,conjecture,! [X464] : ( k04_buttercup10628(X464) <=> b48_buttercup10289(X464) ) ).
fof(sos_391,conjecture,! [X465] : ( k04_buttercup10631(X465) <=> b48_buttercup10629(X465) ) ).
fof(sos_392,conjecture,! [X466] : ( b48_buttercup10075(X466) => k04_buttercup10064(X466) ) & ? [X467] : ( k04_buttercup10064(X467) & ~ b48_buttercup10075(X467) ) ).
fof(sos_393,conjecture,! [X468] : ( k04_buttercup10351(X468) <=> b48_buttercup10176(X468) ) ).
fof(sos_394,conjecture,! [X469] : ( b48_buttercup10352(X469) => k04_buttercup10347(X469) ) & ? [X470] : ( k04_buttercup10347(X470) & ~ b48_buttercup10352(X470) ) ).
fof(sos_395,conjecture,! [X471] : ( b48_buttercup10348(X471) => k04_buttercup10347(X471) ) & ? [X472] : ( k04_buttercup10347(X472) & ~ b48_buttercup10348(X472) ) ).
fof(sos_396,conjecture,! [X473] : ( b48_buttercup10070(X473) => k04_buttercup10064(X473) ) & ? [X474] : ( k04_buttercup10064(X474) & ~ b48_buttercup10070(X474) ) ).
fof(sos_397,conjecture,! [X475] : ( b48_buttercup10068(X475) => k04_buttercup10064(X475) ) & ? [X476] : ( k04_buttercup10064(X476) & ~ b48_buttercup10068(X476) ) ).
fof(sos_398,conjecture,! [X477] : ( k04_buttercup10517(X477) <=> b48_buttercup10421(X477) ) ).
fof(sos_399,conjecture,! [X478] : ( b48_buttercup10515(X478) => k04_buttercup10516(X478) ) & ? [X479] : ( k04_buttercup10516(X479) & ~ b48_buttercup10515(X479) ) ).
fof(sos_400,conjecture,! [X480] : ( k04_buttercup10516(X480) => b48_buttercup10417(X480) ) & ? [X481] : ( b48_buttercup10417(X481) & ~ k04_buttercup10516(X481) ) ).
fof(sos_401,conjecture,! [X482] : ( k04_buttercup10529(X482) <=> b48_buttercup10526(X482) ) ).
fof(sos_402,conjecture,? [X483] : ? [X484] : ? [X485] : ( k04_buttercup10204(X483) & b48_buttercup10214(X483) & k04_buttercup10204(X484) & ~ b48_buttercup10214(X484) & ~ k04_buttercup10204(X485) & b48_buttercup10214(X485) ) | ( ! [X486] : ( b48_buttercup10214(X486) => k04_buttercup10204(X486) ) & ? [X487] : ( k04_buttercup10204(X487) & ~ b48_buttercup10214(X487) ) ) | ( ! [X488] : ( k04_buttercup10204(X488) => b48_buttercup10214(X488) ) & ? [X489] : ( b48_buttercup10214(X489) & ~ k04_buttercup10204(X489) ) ) | ! [X490] : ( k04_buttercup10204(X490) => ~ b48_buttercup10214(X490) ) ).
fof(sos_403,conjecture,? [X491] : ? [X492] : ? [X493] : ( k04_buttercup10204(X491) & b48_buttercup10208(X491) & k04_buttercup10204(X492) & ~ b48_buttercup10208(X492) & ~ k04_buttercup10204(X493) & b48_buttercup10208(X493) ) | ( ! [X494] : ( b48_buttercup10208(X494) => k04_buttercup10204(X494) ) & ? [X495] : ( k04_buttercup10204(X495) & ~ b48_buttercup10208(X495) ) ) | ( ! [X496] : ( k04_buttercup10204(X496) => b48_buttercup10208(X496) ) & ? [X497] : ( b48_buttercup10208(X497) & ~ k04_buttercup10204(X497) ) ) | ! [X498] : ( k04_buttercup10204(X498) => ~ b48_buttercup10208(X498) ) ).
fof(sos_404,conjecture,! [X499] : ( k04_buttercup10555(X499) <=> b48_buttercup10552(X499) ) ).
fof(sos_405,conjecture,! [X500] : ( b48_buttercup10454(X500) => k04_buttercup10464(X500) ) & ? [X501] : ( k04_buttercup10464(X501) & ~ b48_buttercup10454(X501) ) ).
fof(sos_406,conjecture,! [X502] : ( k04_buttercup10462(X502) <=> b48_buttercup10460(X502) ) ).
fof(sos_407,conjecture,! [X503] : ( k04_buttercup10567(X503) <=> b48_buttercup10563(X503) ) ).
fof(sos_408,conjecture,! [X504] : ( k04_buttercup10559(X504) <=> b48_buttercup10562(X504) ) ).
fof(sos_409,conjecture,! [X505] : ( b48_buttercup10179(X505) => k04_buttercup10400(X505) ) & ? [X506] : ( k04_buttercup10400(X506) & ~ b48_buttercup10179(X506) ) ).
fof(sos_410,conjecture,! [X507] : ( b48_buttercup10398(X507) => k04_buttercup10400(X507) ) & ? [X508] : ( k04_buttercup10400(X508) & ~ b48_buttercup10398(X508) ) ).
fof(sos_411,conjecture,! [X509] : ( k04_buttercup10142(X509) <=> b48_buttercup10085(X509) ) ).
fof(sos_412,conjecture,! [X510] : ( b48_buttercup10085(X510) => k04_buttercup10139(X510) ) & ? [X511] : ( k04_buttercup10139(X511) & ~ b48_buttercup10085(X511) ) ).
fof(sos_413,conjecture,! [X512] : ( k04_buttercup10135(X512) => b48_buttercup10458(X512) ) & ? [X513] : ( b48_buttercup10458(X513) & ~ k04_buttercup10135(X513) ) ).
fof(sos_414,conjecture,! [X514] : ( k04_buttercup10135(X514) => b48_buttercup10446(X514) ) & ? [X515] : ( b48_buttercup10446(X515) & ~ k04_buttercup10135(X515) ) ).
fof(sos_415,conjecture,! [X516] : ( k04_buttercup10206(X516) <=> b48_buttercup10220(X516) ) ).
fof(sos_416,conjecture,! [X517] : ( k04_buttercup10147(X517) <=> b48_buttercup10143(X517) ) ).
fof(sos_417,conjecture,! [X518] : ( k04_buttercup10593(X518) <=> b48_buttercup10589(X518) ) ).
fof(sos_418,conjecture,! [X519] : ( k04_buttercup10004(X519) => b48_buttercup10007(X519) ) & ? [X520] : ( b48_buttercup10007(X520) & ~ k04_buttercup10004(X520) ) ).
fof(sos_419,conjecture,! [X521] : ( k04_buttercup10012(X521) => b48_buttercup10007(X521) ) & ? [X522] : ( b48_buttercup10007(X522) & ~ k04_buttercup10012(X522) ) ).
fof(sos_420,conjecture,? [X523] : ? [X524] : ? [X525] : ( k04_buttercup10282(X523) & b48_buttercup10289(X523) & k04_buttercup10282(X524) & ~ b48_buttercup10289(X524) & ~ k04_buttercup10282(X525) & b48_buttercup10289(X525) ) | ( ! [X526] : ( b48_buttercup10289(X526) => k04_buttercup10282(X526) ) & ? [X527] : ( k04_buttercup10282(X527) & ~ b48_buttercup10289(X527) ) ) | ( ! [X528] : ( k04_buttercup10282(X528) => b48_buttercup10289(X528) ) & ? [X529] : ( b48_buttercup10289(X529) & ~ k04_buttercup10282(X529) ) ) | ! [X530] : ( k04_buttercup10282(X530) => ~ b48_buttercup10289(X530) ) ).
fof(sos_421,conjecture,! [X531] : ( k04_buttercup10286(X531) <=> b48_buttercup10283(X531) ) ).
fof(sos_422,conjecture,! [X532] : ( b48_buttercup10158(X532) => k04_buttercup10153(X532) ) & ? [X533] : ( k04_buttercup10153(X533) & ~ b48_buttercup10158(X533) ) ).
fof(sos_423,conjecture,! [X534] : ( b48_buttercup10160(X534) => k04_buttercup10153(X534) ) & ? [X535] : ( k04_buttercup10153(X535) & ~ b48_buttercup10160(X535) ) ).
fof(sos_424,conjecture,! [X536] : ( b48_buttercup10159(X536) => k04_buttercup10153(X536) ) & ? [X537] : ( k04_buttercup10153(X537) & ~ b48_buttercup10159(X537) ) ).
fof(sos_425,conjecture,! [X538] : ( k04_buttercup10164(X538) <=> b48_buttercup10161(X538) ) ).
fof(sos_426,conjecture,! [X539] : ( k04_buttercup10061(X539) <=> b48_buttercup10058(X539) ) ).
fof(sos_427,conjecture,! [X540] : ( k04_buttercup10057(X540) <=> b48_buttercup10054(X540) ) ).
fof(sos_428,conjecture,! [X541] : ( k04_buttercup10000(X541) => b48_buttercup10007(X541) ) & ? [X542] : ( b48_buttercup10007(X542) & ~ k04_buttercup10000(X542) ) ).
fof(sos_429,conjecture,! [X543] : ( k04_buttercup10602(X543) <=> b48_buttercup10604(X543) ) ).
fof(sos_430,conjecture,! [X544] : ( k04_buttercup10599(X544) <=> b48_buttercup10596(X544) ) ).
fof(sos_431,conjecture,! [X545] : ( b48_buttercup10108(X545) => k04_buttercup10622(X545) ) & ? [X546] : ( k04_buttercup10622(X546) & ~ b48_buttercup10108(X546) ) ).
fof(sos_432,conjecture,! [X547] : ( b48_buttercup10104(X547) => k04_buttercup10622(X547) ) & ? [X548] : ( k04_buttercup10622(X548) & ~ b48_buttercup10104(X548) ) ).
fof(sos_433,conjecture,! [X549] : ( k04_buttercup10626(X549) <=> b48_buttercup10624(X549) ) ).
fof(sos_434,conjecture,! [X550] : ( b48_buttercup10110(X550) => k04_buttercup10622(X550) ) & ? [X551] : ( k04_buttercup10622(X551) & ~ b48_buttercup10110(X551) ) ).
fof(sos_435,conjecture,! [X552] : ( k04_buttercup10482(X552) <=> b48_buttercup10479(X552) ) ).
fof(sos_436,conjecture,! [X553] : ( b48_buttercup10483(X553) => k04_buttercup10486(X553) ) & ? [X554] : ( k04_buttercup10486(X554) & ~ b48_buttercup10483(X554) ) ).
fof(sos_437,conjecture,! [X555] : ( b48_buttercup10478(X555) => k04_buttercup10486(X555) ) & ? [X556] : ( k04_buttercup10486(X556) & ~ b48_buttercup10478(X556) ) ).
fof(sos_438,conjecture,! [X557] : ( b48_buttercup10381(X557) => k04_buttercup10095(X557) ) & ? [X558] : ( k04_buttercup10095(X558) & ~ b48_buttercup10381(X558) ) ).
fof(sos_439,conjecture,! [X559] : ( k04_buttercup10096(X559) <=> b48_buttercup10092(X559) ) ).
fof(sos_440,conjecture,! [X560] : ( k04_buttercup10097(X560) <=> b48_buttercup10381(X560) ) ).
fof(sos_441,conjecture,! [X561] : ( k04_buttercup10100(X561) => b48_buttercup10098(X561) ) & ? [X562] : ( b48_buttercup10098(X562) & ~ k04_buttercup10100(X562) ) ).
fof(sos_442,conjecture,? [X563] : ? [X564] : ? [X565] : ( k04_buttercup10100(X563) & b48_buttercup10102(X563) & k04_buttercup10100(X564) & ~ b48_buttercup10102(X564) & ~ k04_buttercup10100(X565) & b48_buttercup10102(X565) ) | ( ! [X566] : ( b48_buttercup10102(X566) => k04_buttercup10100(X566) ) & ? [X567] : ( k04_buttercup10100(X567) & ~ b48_buttercup10102(X567) ) ) | ( ! [X568] : ( k04_buttercup10100(X568) => b48_buttercup10102(X568) ) & ? [X569] : ( b48_buttercup10102(X569) & ~ k04_buttercup10100(X569) ) ) | ! [X570] : ( k04_buttercup10100(X570) => ~ b48_buttercup10102(X570) ) ).
fof(sos_443,conjecture,? [X571] : ? [X572] : ? [X573] : ( k04_buttercup10364(X571) & b48_buttercup10440(X571) & k04_buttercup10364(X572) & ~ b48_buttercup10440(X572) & ~ k04_buttercup10364(X573) & b48_buttercup10440(X573) ) ).
fof(sos_444,conjecture,! [X574] : ( b48_buttercup10441(X574) => k04_buttercup10364(X574) ) & ? [X575] : ( k04_buttercup10364(X575) & ~ b48_buttercup10441(X575) ) ).
fof(sos_445,conjecture,! [X576] : ( k04_buttercup10369(X576) <=> b48_buttercup10367(X576) ) ).
fof(sos_446,conjecture,! [X577] : ( k04_buttercup10360(X577) <=> b48_buttercup10359(X577) ) ).
fof(sos_447,conjecture,! [X578] : ( b48_buttercup10362(X578) => k04_buttercup10364(X578) ) & ? [X579] : ( k04_buttercup10364(X579) & ~ b48_buttercup10362(X579) ) ).
fof(sos_448,conjecture,! [X580] : ( k04_buttercup10282(X580) => b48_buttercup10279(X580) ) & ? [X581] : ( b48_buttercup10279(X581) & ~ k04_buttercup10282(X581) ) ).
fof(sos_449,conjecture,! [X582] : ( k04_buttercup10329(X582) <=> b48_buttercup10326(X582) ) ).
fof(sos_450,conjecture,! [X583] : ( k04_buttercup10325(X583) <=> b48_buttercup10322(X583) ) ).
fof(sos_451,conjecture,! [X584] : ( b48_buttercup10320(X584) => k04_buttercup10316(X584) ) & ? [X585] : ( k04_buttercup10316(X585) & ~ b48_buttercup10320(X585) ) ).
fof(sos_452,conjecture,! [X586] : ( k04_buttercup10342(X586) <=> b48_buttercup10605(X586) ) ).
fof(sos_453,conjecture,! [X587] : ( b48_buttercup10343(X587) => k04_buttercup10347(X587) ) & ? [X588] : ( k04_buttercup10347(X588) & ~ b48_buttercup10343(X588) ) ).
fof(sos_454,conjecture,! [X589] : ( k04_buttercup10544(X589) <=> b48_buttercup10542(X589) ) ).
fof(sos_455,conjecture,! [X590] : ( k04_buttercup10540(X590) <=> b48_buttercup10541(X590) ) ).
fof(sos_456,conjecture,! [X591] : ( k04_buttercup10506(X591) <=> b48_buttercup10502(X591) ) ).
fof(sos_457,conjecture,! [X592] : ( k04_buttercup10510(X592) <=> b48_buttercup10507(X592) ) ).
fof(sos_458,conjecture,! [X593] : ( k04_buttercup10048(X593) <=> b48_buttercup10046(X593) ) ).
fof(sos_459,conjecture,! [X594] : ( k04_buttercup10049(X594) <=> b48_buttercup10052(X594) ) ).
fof(sos_460,conjecture,! [X595] : ( k04_buttercup10051(X595) <=> b48_buttercup10050(X595) ) ).
fof(sos_461,conjecture,! [X596] : ( k04_buttercup10053(X596) => b48_buttercup10024(X596) ) & ? [X597] : ( b48_buttercup10024(X597) & ~ k04_buttercup10053(X597) ) ).
fof(sos_462,conjecture,! [X598] : ( k04_buttercup10053(X598) <=> b48_buttercup10029(X598) ) ).
fof(sos_463,conjecture,! [X599] : ( k04_buttercup10213(X599) <=> b48_buttercup10210(X599) ) ).
fof(sos_464,conjecture,! [X600] : ( k04_buttercup10539(X600) <=> b48_buttercup10538(X600) ) ).
fof(sos_465,conjecture,! [X601] : ( k04_buttercup10453(X601) <=> b48_buttercup10451(X601) ) ).
fof(sos_466,conjecture,! [X602] : ( k04_buttercup10449(X602) <=> b48_buttercup10446(X602) ) ).
fof(sos_467,conjecture,! [X603] : ( k04_buttercup10445(X603) <=> b48_buttercup10443(X603) ) ).
fof(sos_468,conjecture,! [X604] : ( b48_buttercup10570(X604) => k04_buttercup10567(X604) ) & ? [X605] : ( k04_buttercup10567(X605) & ~ b48_buttercup10570(X605) ) ).
fof(sos_469,conjecture,! [X606] : ( k04_buttercup10415(X606) <=> b48_buttercup10411(X606) ) ).
fof(sos_470,conjecture,! [X607] : ( k04_buttercup10408(X607) <=> b48_buttercup10410(X607) ) ).
fof(sos_471,conjecture,! [X608] : ( b48_buttercup10574(X608) => k04_buttercup10567(X608) ) & ? [X609] : ( k04_buttercup10567(X609) & ~ b48_buttercup10574(X609) ) ).
fof(sos_472,conjecture,! [X610] : ( k04_buttercup10404(X610) <=> b48_buttercup10402(X610) ) ).
fof(sos_473,conjecture,! [X611] : ( k04_buttercup10406(X611) <=> b48_buttercup10405(X611) ) ).
fof(sos_474,conjecture,! [X612] : ( b48_buttercup10133(X612) => k04_buttercup10132(X612) ) & ? [X613] : ( k04_buttercup10132(X613) & ~ b48_buttercup10133(X613) ) ).
fof(sos_475,conjecture,! [X614] : ( b48_buttercup10134(X614) => k04_buttercup10132(X614) ) & ? [X615] : ( k04_buttercup10132(X615) & ~ b48_buttercup10134(X615) ) ).
fof(sos_476,conjecture,! [X616] : ( k04_buttercup10132(X616) <=> b48_buttercup10130(X616) ) ).
fof(sos_477,conjecture,! [X617] : ( k04_buttercup10316(X617) <=> b48_buttercup10313(X617) ) ).
fof(sos_478,conjecture,! [X618] : ( k04_buttercup10312(X618) <=> b48_buttercup10309(X618) ) ).
fof(sos_479,conjecture,! [X619] : ( b48_buttercup10308(X619) => k04_buttercup10303(X619) ) & ? [X620] : ( k04_buttercup10303(X620) & ~ b48_buttercup10308(X620) ) ).
fof(sos_480,conjecture,! [X621] : ( b48_buttercup10173(X621) => k04_buttercup10172(X621) ) & ? [X622] : ( k04_buttercup10172(X622) & ~ b48_buttercup10173(X622) ) ).
fof(sos_481,conjecture,! [X623] : ( k04_buttercup10172(X623) <=> b48_buttercup10170(X623) ) ).
fof(sos_482,conjecture,! [X624] : ( b48_buttercup10169(X624) => k04_buttercup10164(X624) ) & ? [X625] : ( k04_buttercup10164(X625) & ~ b48_buttercup10169(X625) ) ).
fof(sos_483,conjecture,! [X626] : ( b48_buttercup10166(X626) => k04_buttercup10164(X626) ) & ? [X627] : ( k04_buttercup10164(X627) & ~ b48_buttercup10166(X627) ) ).
fof(sos_484,conjecture,! [X628] : ( b48_buttercup10167(X628) => k04_buttercup10164(X628) ) & ? [X629] : ( k04_buttercup10164(X629) & ~ b48_buttercup10167(X629) ) ).
fof(sos_485,conjecture,! [X630] : ( b48_buttercup10174(X630) => k04_buttercup10172(X630) ) & ? [X631] : ( k04_buttercup10172(X631) & ~ b48_buttercup10174(X631) ) ).
fof(sos_486,conjecture,! [X632] : ( k04_buttercup10181(X632) <=> b48_buttercup10180(X632) ) ).
fof(sos_487,conjecture,! [X633] : ( k04_buttercup10244(X633) <=> b48_buttercup10240(X633) ) ).
fof(sos_488,conjecture,! [X634] : ( k04_buttercup10611(X634) <=> b48_buttercup10609(X634) ) ).
fof(sos_489,conjecture,! [X635] : ( k04_buttercup10608(X635) => b48_buttercup10201(X635) ) & ? [X636] : ( b48_buttercup10201(X636) & ~ k04_buttercup10608(X636) ) ).
fof(sos_490,conjecture,! [X637] : ( k04_buttercup10608(X637) <=> b48_buttercup10214(X637) ) ).
fof(sos_491,conjecture,! [X638] : ( k04_buttercup10219(X638) <=> b48_buttercup10217(X638) ) ).
fof(sos_492,conjecture,! [X639] : ( k04_buttercup10221(X639) <=> b48_buttercup10208(X639) ) ).
fof(sos_493,conjecture,! [X640] : ( k04_buttercup10221(X640) => b48_buttercup10201(X640) ) & ? [X641] : ( b48_buttercup10201(X641) & ~ k04_buttercup10221(X641) ) ).
fof(sos_494,conjecture,! [X642] : ( k04_buttercup10225(X642) => b48_buttercup10222(X642) ) & ? [X643] : ( b48_buttercup10222(X643) & ~ k04_buttercup10225(X643) ) ).
fof(sos_495,conjecture,! [X644] : ( k04_buttercup10044(X644) <=> b48_buttercup10043(X644) ) ).
fof(sos_496,conjecture,! [X645] : ( k04_buttercup10042(X645) <=> b48_buttercup10045(X645) ) ).
fof(sos_497,conjecture,! [X646] : ( k04_buttercup10477(X646) <=> b48_buttercup10474(X646) ) ).
fof(sos_498,conjecture,! [X647] : ( k04_buttercup10473(X647) <=> b48_buttercup10471(X647) ) ).
fof(sos_499,conjecture,! [X648] : ( k04_buttercup10470(X648) <=> b48_buttercup10469(X648) ) ).
fof(sos_500,conjecture,! [X649] : ( b48_buttercup10092(X649) => k04_buttercup10095(X649) ) & ? [X650] : ( k04_buttercup10095(X650) & ~ b48_buttercup10092(X650) ) ).
fof(sos_501,conjecture,! [X651] : ( k04_buttercup10380(X651) <=> b48_buttercup10378(X651) ) ).
fof(sos_502,conjecture,! [X652] : ( k04_buttercup10371(X652) <=> b48_buttercup10370(X652) ) ).
fof(sos_503,conjecture,! [X653] : ( k04_buttercup10373(X653) <=> b48_buttercup10377(X653) ) ).
fof(sos_504,conjecture,! [X654] : ( k04_buttercup10376(X654) <=> b48_buttercup10374(X654) ) ).
fof(sos_505,conjecture,! [X655] : ( b48_buttercup10261(X655) => k04_buttercup10259(X655) ) & ? [X656] : ( k04_buttercup10259(X656) & ~ b48_buttercup10261(X656) ) ).
fof(sos_506,conjecture,! [X657] : ( k04_buttercup10255(X657) <=> b48_buttercup10253(X657) ) ).
fof(sos_507,conjecture,! [X658] : ( b48_buttercup10260(X658) => k04_buttercup10259(X658) ) & ? [X659] : ( k04_buttercup10259(X659) & ~ b48_buttercup10260(X659) ) ).
fof(sos_508,conjecture,! [X660] : ( k04_buttercup10499(X660) <=> b48_buttercup10496(X660) ) ).
fof(sos_509,conjecture,! [X661] : ( b48_buttercup10191(X661) => k04_buttercup10190(X661) ) & ? [X662] : ( k04_buttercup10190(X662) & ~ b48_buttercup10191(X662) ) ).
fof(sos_510,conjecture,! [X663] : ( k04_buttercup10190(X663) <=> b48_buttercup10186(X663) ) ).
fof(sos_511,conjecture,! [X664] : ( b48_buttercup10344(X664) => k04_buttercup10347(X664) ) & ? [X665] : ( k04_buttercup10347(X665) & ~ b48_buttercup10344(X665) ) ).
fof(sos_512,conjecture,! [X666] : ( k04_buttercup10117(X666) <=> b48_buttercup10115(X666) ) ).
fof(sos_513,conjecture,! [X667] : ( k04_buttercup10125(X667) <=> b48_buttercup10121(X667) ) ).
fof(sos_514,conjecture,! [X668] : ( b48_buttercup10120(X668) => k04_buttercup10117(X668) ) & ? [X669] : ( k04_buttercup10117(X669) & ~ b48_buttercup10120(X669) ) ).
fof(sos_515,conjecture,! [X670] : ( b48_buttercup10572(X670) => k04_buttercup10567(X670) ) & ? [X671] : ( k04_buttercup10567(X671) & ~ b48_buttercup10572(X671) ) ).
fof(sos_516,conjecture,! [X672] : ( k04_buttercup10039(X672) <=> b48_buttercup10035(X672) ) ).
fof(sos_517,conjecture,! [X673] : ( k04_buttercup10033(X673) <=> b48_buttercup10031(X673) ) ).
fof(sos_518,conjecture,! [X674] : ( k04_buttercup10028(X674) <=> b48_buttercup10034(X674) ) ).
fof(sos_519,conjecture,! [X675] : ( k04_buttercup10578(X675) <=> b48_buttercup10575(X675) ) ).
fof(sos_520,conjecture,! [X676] : ( k04_buttercup10430(X676) <=> b48_buttercup10427(X676) ) ).
fof(sos_521,conjecture,! [X677] : ( b48_buttercup10422(X677) => k04_buttercup10419(X677) ) & ? [X678] : ( k04_buttercup10419(X678) & ~ b48_buttercup10422(X678) ) ).
fof(sos_522,conjecture,? [X679] : ? [X680] : ? [X681] : ( k04_buttercup10419(X679) & b48_buttercup10421(X679) & k04_buttercup10419(X680) & ~ b48_buttercup10421(X680) & ~ k04_buttercup10419(X681) & b48_buttercup10421(X681) ) | ( ! [X682] : ( b48_buttercup10421(X682) => k04_buttercup10419(X682) ) & ? [X683] : ( k04_buttercup10419(X683) & ~ b48_buttercup10421(X683) ) ) | ( ! [X684] : ( k04_buttercup10419(X684) => b48_buttercup10421(X684) ) & ? [X685] : ( b48_buttercup10421(X685) & ~ k04_buttercup10419(X685) ) ) | ! [X686] : ( k04_buttercup10419(X686) => ~ b48_buttercup10421(X686) ) ).
fof(sos_523,conjecture,? [X687] : ? [X688] : ? [X689] : ( k04_buttercup10419(X687) & b48_buttercup10222(X687) & k04_buttercup10419(X688) & ~ b48_buttercup10222(X688) & ~ k04_buttercup10419(X689) & b48_buttercup10222(X689) ) ).
fof(sos_524,conjecture,! [X690] : ( b48_buttercup10228(X690) => k04_buttercup10419(X690) ) & ? [X691] : ( k04_buttercup10419(X691) & ~ b48_buttercup10228(X691) ) ).
fof(sos_525,conjecture,? [X692] : ? [X693] : ? [X694] : ( k04_buttercup10419(X692) & b48_buttercup10417(X692) & k04_buttercup10419(X693) & ~ b48_buttercup10417(X693) & ~ k04_buttercup10419(X694) & b48_buttercup10417(X694) ) ).
fof(sos_526,conjecture,? [X695] : k04_buttercup10282(X695) ).
fof(sos_527,conjecture,? [X696] : k04_buttercup10286(X696) ).
fof(sos_528,conjecture,? [X697] : k04_buttercup10184(X697) ).
fof(sos_529,conjecture,? [X698] : k04_buttercup10288(X698) ).
fof(sos_530,conjecture,? [X699] : k04_buttercup10164(X699) ).
fof(sos_531,conjecture,? [X700] : k04_buttercup10539(X700) ).
fof(sos_532,conjecture,? [X701] : k04_buttercup10044(X701) ).
fof(sos_533,conjecture,? [X702] : k04_buttercup10084(X702) ).
fof(sos_534,conjecture,? [X703] : k04_buttercup10042(X703) ).
fof(sos_535,conjecture,? [X704] : k04_buttercup10200(X704) ).
fof(sos_536,conjecture,? [X705] : k04_buttercup10049(X705) ).
fof(sos_537,conjecture,? [X706] : k04_buttercup10048(X706) ).
fof(sos_538,conjecture,? [X707] : k04_buttercup10535(X707) ).
fof(sos_539,conjecture,? [X708] : k04_buttercup10204(X708) ).
fof(sos_540,conjecture,? [X709] : k04_buttercup10369(X709) ).
fof(sos_541,conjecture,? [X710] : k04_buttercup10635(X710) ).
fof(sos_542,conjecture,? [X711] : k04_buttercup10445(X711) ).
fof(sos_543,conjecture,? [X712] : k04_buttercup10631(X712) ).
fof(sos_544,conjecture,? [X713] : k04_buttercup10360(X713) ).
fof(sos_545,conjecture,? [X714] : k04_buttercup10139(X714) ).
fof(sos_546,conjecture,? [X715] : k04_buttercup10364(X715) ).
fof(sos_547,conjecture,? [X716] : k04_buttercup10639(X716) ).
fof(sos_548,conjecture,? [X717] : k04_buttercup10079(X717) ).
fof(sos_549,conjecture,? [X718] : k04_buttercup10172(X718) ).
fof(sos_550,conjecture,? [X719] : k04_buttercup10504(X719) ).
fof(sos_551,conjecture,? [X720] : k04_buttercup10506(X720) ).
fof(sos_552,conjecture,? [X721] : k04_buttercup10074(X721) ).
fof(sos_553,conjecture,? [X722] : k04_buttercup10236(X722) ).
fof(sos_554,conjecture,? [X723] : k04_buttercup10477(X723) ).
fof(sos_555,conjecture,? [X724] : k04_buttercup10470(X724) ).
fof(sos_556,conjecture,? [X725] : k04_buttercup10473(X725) ).
fof(sos_557,conjecture,? [X726] : k04_buttercup10376(X726) ).
fof(sos_558,conjecture,? [X727] : k04_buttercup10626(X727) ).
fof(sos_559,conjecture,? [X728] : k04_buttercup10373(X728) ).
fof(sos_560,conjecture,? [X729] : k04_buttercup10234(X729) ).
fof(sos_561,conjecture,? [X730] : k04_buttercup10371(X730) ).
fof(sos_562,conjecture,? [X731] : k04_buttercup10622(X731) ).
fof(sos_563,conjecture,? [X732] : k04_buttercup10586(X732) ).
fof(sos_564,conjecture,? [X733] : k04_buttercup10628(X733) ).
fof(sos_565,conjecture,? [X734] : k04_buttercup10486(X734) ).
fof(sos_566,conjecture,? [X735] : k04_buttercup10389(X735) ).
fof(sos_567,conjecture,? [X736] : k04_buttercup10142(X736) ).
fof(sos_568,conjecture,? [X737] : k04_buttercup10382(X737) ).
fof(sos_569,conjecture,? [X738] : k04_buttercup10380(X738) ).
fof(sos_570,conjecture,? [X739] : k04_buttercup10064(X739) ).
fof(sos_571,conjecture,? [X740] : k04_buttercup10061(X740) ).
fof(sos_572,conjecture,? [X741] : k04_buttercup10385(X741) ).
fof(sos_573,conjecture,? [X742] : k04_buttercup10510(X742) ).
fof(sos_574,conjecture,? [X743] : k04_buttercup10517(X743) ).
fof(sos_575,conjecture,? [X744] : k04_buttercup10516(X744) ).
fof(sos_576,conjecture,? [X745] : k04_buttercup10462(X745) ).
fof(sos_577,conjecture,? [X746] : k04_buttercup10464(X746) ).
fof(sos_578,conjecture,? [X747] : k04_buttercup10303(X747) ).
fof(sos_579,conjecture,? [X748] : k04_buttercup10599(X748) ).
fof(sos_580,conjecture,? [X749] : k04_buttercup10593(X749) ).
fof(sos_581,conjecture,? [X750] : k04_buttercup10619(X750) ).
fof(sos_582,conjecture,? [X751] : k04_buttercup10206(X751) ).
fof(sos_583,conjecture,? [X752] : k04_buttercup10391(X752) ).
fof(sos_584,conjecture,? [X753] : k04_buttercup10153(X753) ).
fof(sos_585,conjecture,? [X754] : k04_buttercup10637(X754) ).
fof(sos_586,conjecture,? [X755] : k04_buttercup10012(X755) ).
fof(sos_587,conjecture,? [X756] : k04_buttercup10611(X756) ).
fof(sos_588,conjecture,? [X757] : k04_buttercup10016(X757) ).
fof(sos_589,conjecture,? [X758] : k04_buttercup10397(X758) ).
fof(sos_590,conjecture,? [X759] : k04_buttercup10495(X759) ).
fof(sos_591,conjecture,? [X760] : k04_buttercup10492(X760) ).
fof(sos_592,conjecture,? [X761] : k04_buttercup10608(X761) ).
fof(sos_593,conjecture,? [X762] : k04_buttercup10567(X762) ).
fof(sos_594,conjecture,? [X763] : k04_buttercup10602(X763) ).
fof(sos_595,conjecture,? [X764] : k04_buttercup10499(X764) ).
fof(sos_596,conjecture,? [X765] : k04_buttercup10259(X765) ).
fof(sos_597,conjecture,? [X766] : k04_buttercup10312(X766) ).
fof(sos_598,conjecture,? [X767] : k04_buttercup10096(X767) ).
fof(sos_599,conjecture,? [X768] : k04_buttercup10097(X768) ).
fof(sos_600,conjecture,? [X769] : k04_buttercup10419(X769) ).
fof(sos_601,conjecture,? [X770] : k04_buttercup10252(X770) ).
fof(sos_602,conjecture,? [X771] : k04_buttercup10415(X771) ).
fof(sos_603,conjecture,? [X772] : k04_buttercup10255(X772) ).
fof(sos_604,conjecture,? [X773] : k04_buttercup10449(X773) ).
fof(sos_605,conjecture,? [X774] : k04_buttercup10053(X774) ).
fof(sos_606,conjecture,? [X775] : k04_buttercup10147(X775) ).
fof(sos_607,conjecture,? [X776] : k04_buttercup10000(X776) ).
fof(sos_608,conjecture,? [X777] : k04_buttercup10004(X777) ).
fof(sos_609,conjecture,? [X778] : k04_buttercup10400(X778) ).
fof(sos_610,conjecture,? [X779] : k04_buttercup10125(X779) ).
fof(sos_611,conjecture,? [X780] : k04_buttercup10329(X780) ).
fof(sos_612,conjecture,? [X781] : k04_buttercup10482(X781) ).
fof(sos_613,conjecture,? [X782] : k04_buttercup10325(X782) ).
fof(sos_614,conjecture,? [X783] : k04_buttercup10581(X783) ).
fof(sos_615,conjecture,? [X784] : k04_buttercup10244(X784) ).
fof(sos_616,conjecture,? [X785] : k04_buttercup10408(X785) ).
fof(sos_617,conjecture,? [X786] : k04_buttercup10089(X786) ).
fof(sos_618,conjecture,? [X787] : k04_buttercup10404(X787) ).
fof(sos_619,conjecture,? [X788] : k04_buttercup10406(X788) ).
fof(sos_620,conjecture,? [X789] : k04_buttercup10578(X789) ).
fof(sos_621,conjecture,? [X790] : k04_buttercup10067(X790) ).
fof(sos_622,conjecture,? [X791] : k04_buttercup10033(X791) ).
fof(sos_623,conjecture,? [X792] : k04_buttercup10039(X792) ).
fof(sos_624,conjecture,? [X793] : k04_buttercup10135(X793) ).
fof(sos_625,conjecture,? [X794] : k04_buttercup10132(X794) ).
fof(sos_626,conjecture,? [X795] : k04_buttercup10333(X795) ).
fof(sos_627,conjecture,? [X796] : k04_buttercup10337(X796) ).
fof(sos_628,conjecture,? [X797] : k04_buttercup10540(X797) ).
fof(sos_629,conjecture,? [X798] : k04_buttercup10544(X798) ).
fof(sos_630,conjecture,? [X799] : k04_buttercup10546(X799) ).
fof(sos_631,conjecture,? [X800] : k04_buttercup10547(X800) ).
fof(sos_632,conjecture,? [X801] : k04_buttercup10430(X801) ).
fof(sos_633,conjecture,? [X802] : k04_buttercup10238(X802) ).
fof(sos_634,conjecture,? [X803] : k04_buttercup10095(X803) ).
fof(sos_635,conjecture,? [X804] : k04_buttercup10437(X804) ).
fof(sos_636,conjecture,? [X805] : k04_buttercup10026(X805) ).
fof(sos_637,conjecture,? [X806] : k04_buttercup10028(X806) ).
fof(sos_638,conjecture,? [X807] : k04_buttercup10100(X807) ).
fof(sos_639,conjecture,? [X808] : k04_buttercup10559(X808) ).
fof(sos_640,conjecture,? [X809] : k04_buttercup10555(X809) ).
fof(sos_641,conjecture,? [X810] : k04_buttercup10551(X810) ).
fof(sos_642,conjecture,? [X811] : k04_buttercup10221(X811) ).
fof(sos_643,conjecture,? [X812] : k04_buttercup10425(X812) ).
fof(sos_644,conjecture,? [X813] : k04_buttercup10424(X813) ).
fof(sos_645,conjecture,? [X814] : k04_buttercup10225(X814) ).
fof(sos_646,conjecture,? [X815] : k04_buttercup10181(X815) ).
fof(sos_647,conjecture,? [X816] : k04_buttercup10342(X816) ).
fof(sos_648,conjecture,? [X817] : k04_buttercup10620(X817) ).
fof(sos_649,conjecture,? [X818] : k04_buttercup10296(X818) ).
fof(sos_650,conjecture,? [X819] : k04_buttercup10293(X819) ).
fof(sos_651,conjecture,? [X820] : k04_buttercup10117(X820) ).
fof(sos_652,conjecture,? [X821] : k04_buttercup10298(X821) ).
fof(sos_653,conjecture,? [X822] : k04_buttercup10643(X822) ).
fof(sos_654,conjecture,? [X823] : k04_buttercup10057(X823) ).
fof(sos_655,conjecture,? [X824] : k04_buttercup10641(X824) ).
fof(sos_656,conjecture,? [X825] : k04_buttercup10529(X825) ).
fof(sos_657,conjecture,? [X826] : k04_buttercup10219(X826) ).
fof(sos_658,conjecture,? [X827] : k04_buttercup10051(X827) ).
fof(sos_659,conjecture,? [X828] : k04_buttercup10316(X828) ).
fof(sos_660,conjecture,? [X829] : k04_buttercup10524(X829) ).
fof(sos_661,conjecture,? [X830] : k04_buttercup10213(X830) ).
fof(sos_662,conjecture,? [X831] : k04_buttercup10453(X831) ).
fof(sos_663,conjecture,? [X832] : k04_buttercup10190(X832) ).
fof(sos_664,conjecture,? [X833] : k04_buttercup10357(X833) ).
fof(sos_665,conjecture,? [X834] : k04_buttercup10356(X834) ).
fof(sos_666,conjecture,? [X835] : k04_buttercup10351(X835) ).
fof(sos_667,conjecture,? [X836] : k04_buttercup10347(X836) ).
fof(sos_668,conjecture,? [X837] : b48_buttercup10283(X837) ).
fof(sos_669,conjecture,? [X838] : b48_buttercup10169(X838) ).
fof(sos_670,conjecture,? [X839] : b48_buttercup10502(X839) ).
fof(sos_671,conjecture,? [X840] : b48_buttercup10289(X840) ).
fof(sos_672,conjecture,? [X841] : b48_buttercup10161(X841) ).
fof(sos_673,conjecture,? [X842] : b48_buttercup10166(X842) ).
fof(sos_674,conjecture,? [X843] : b48_buttercup10167(X843) ).
fof(sos_675,conjecture,? [X844] : b48_buttercup10260(X844) ).
fof(sos_676,conjecture,? [X845] : b48_buttercup10045(X845) ).
fof(sos_677,conjecture,? [X846] : b48_buttercup10538(X846) ).
fof(sos_678,conjecture,? [X847] : b48_buttercup10046(X847) ).
fof(sos_679,conjecture,? [X848] : b48_buttercup10043(X848) ).
fof(sos_680,conjecture,? [X849] : b48_buttercup10332(X849) ).
fof(sos_681,conjecture,? [X850] : b48_buttercup10531(X850) ).
fof(sos_682,conjecture,? [X851] : b48_buttercup10530(X851) ).
fof(sos_683,conjecture,? [X852] : b48_buttercup10201(X852) ).
fof(sos_684,conjecture,? [X853] : b48_buttercup10441(X853) ).
fof(sos_685,conjecture,? [X854] : b48_buttercup10440(X854) ).
fof(sos_686,conjecture,? [X855] : b48_buttercup10443(X855) ).
fof(sos_687,conjecture,? [X856] : b48_buttercup10442(X856) ).
fof(sos_688,conjecture,? [X857] : b48_buttercup10632(X857) ).
fof(sos_689,conjecture,? [X858] : b48_buttercup10446(X858) ).
fof(sos_690,conjecture,? [X859] : b48_buttercup10361(X859) ).
fof(sos_691,conjecture,? [X860] : b48_buttercup10362(X860) ).
fof(sos_692,conjecture,? [X861] : b48_buttercup10358(X861) ).
fof(sos_693,conjecture,? [X862] : b48_buttercup10365(X862) ).
fof(sos_694,conjecture,? [X863] : b48_buttercup10638(X863) ).
fof(sos_695,conjecture,? [X864] : b48_buttercup10367(X864) ).
fof(sos_696,conjecture,? [X865] : b48_buttercup10421(X865) ).
fof(sos_697,conjecture,? [X866] : b48_buttercup10160(X866) ).
fof(sos_698,conjecture,? [X867] : b48_buttercup10179(X867) ).
fof(sos_699,conjecture,? [X868] : b48_buttercup10279(X868) ).
fof(sos_700,conjecture,? [X869] : b48_buttercup10170(X869) ).
fof(sos_701,conjecture,? [X870] : b48_buttercup10173(X870) ).
fof(sos_702,conjecture,? [X871] : b48_buttercup10174(X871) ).
fof(sos_703,conjecture,? [X872] : b48_buttercup10176(X872) ).
fof(sos_704,conjecture,? [X873] : b48_buttercup10070(X873) ).
fof(sos_705,conjecture,? [X874] : b48_buttercup10072(X874) ).
fof(sos_706,conjecture,? [X875] : b48_buttercup10507(X875) ).
fof(sos_707,conjecture,? [X876] : b48_buttercup10478(X876) ).
fof(sos_708,conjecture,? [X877] : b48_buttercup10075(X877) ).
fof(sos_709,conjecture,? [X878] : b48_buttercup10076(X878) ).
fof(sos_710,conjecture,? [X879] : b48_buttercup10474(X879) ).
fof(sos_711,conjecture,? [X880] : b48_buttercup10471(X880) ).
fof(sos_712,conjecture,? [X881] : b48_buttercup10377(X881) ).
fof(sos_713,conjecture,? [X882] : b48_buttercup10624(X882) ).
fof(sos_714,conjecture,? [X883] : b48_buttercup10374(X883) ).
fof(sos_715,conjecture,? [X884] : b48_buttercup10589(X884) ).
fof(sos_716,conjecture,? [X885] : b48_buttercup10278(X885) ).
fof(sos_717,conjecture,? [X886] : b48_buttercup10370(X886) ).
fof(sos_718,conjecture,? [X887] : b48_buttercup10276(X887) ).
fof(sos_719,conjecture,? [X888] : b48_buttercup10277(X888) ).
fof(sos_720,conjecture,? [X889] : b48_buttercup10274(X889) ).
fof(sos_721,conjecture,? [X890] : b48_buttercup10275(X890) ).
fof(sos_722,conjecture,? [X891] : b48_buttercup10629(X891) ).
fof(sos_723,conjecture,? [X892] : b48_buttercup10273(X892) ).
fof(sos_724,conjecture,? [X893] : b48_buttercup10582(X893) ).
fof(sos_725,conjecture,? [X894] : b48_buttercup10378(X894) ).
fof(sos_726,conjecture,? [X895] : b48_buttercup10208(X895) ).
fof(sos_727,conjecture,? [X896] : b48_buttercup10483(X896) ).
fof(sos_728,conjecture,? [X897] : b48_buttercup10068(X897) ).
fof(sos_729,conjecture,? [X898] : b48_buttercup10383(X898) ).
fof(sos_730,conjecture,? [X899] : b48_buttercup10065(X899) ).
fof(sos_731,conjecture,? [X900] : b48_buttercup10381(X900) ).
fof(sos_732,conjecture,? [X901] : b48_buttercup10386(X901) ).
fof(sos_733,conjecture,? [X902] : b48_buttercup10513(X902) ).
fof(sos_734,conjecture,? [X903] : b48_buttercup10512(X903) ).
fof(sos_735,conjecture,? [X904] : b48_buttercup10469(X904) ).
fof(sos_736,conjecture,? [X905] : b48_buttercup10019(X905) ).
fof(sos_737,conjecture,? [X906] : b48_buttercup10515(X906) ).
fof(sos_738,conjecture,? [X907] : b48_buttercup10514(X907) ).
fof(sos_739,conjecture,? [X908] : b48_buttercup10519(X908) ).
fof(sos_740,conjecture,? [X909] : b48_buttercup10460(X909) ).
fof(sos_741,conjecture,? [X910] : b48_buttercup10467(X910) ).
fof(sos_742,conjecture,? [X911] : b48_buttercup10466(X911) ).
fof(sos_743,conjecture,? [X912] : b48_buttercup10465(X912) ).
fof(sos_744,conjecture,? [X913] : b48_buttercup10272(X913) ).
fof(sos_745,conjecture,? [X914] : b48_buttercup10612(X914) ).
fof(sos_746,conjecture,? [X915] : b48_buttercup10269(X915) ).
fof(sos_747,conjecture,? [X916] : b48_buttercup10307(X916) ).
fof(sos_748,conjecture,? [X917] : b48_buttercup10616(X917) ).
fof(sos_749,conjecture,? [X918] : b48_buttercup10305(X918) ).
fof(sos_750,conjecture,? [X919] : b48_buttercup10489(X919) ).
fof(sos_751,conjecture,? [X920] : b48_buttercup10267(X920) ).
fof(sos_752,conjecture,? [X921] : b48_buttercup10266(X921) ).
fof(sos_753,conjecture,? [X922] : b48_buttercup10261(X922) ).
fof(sos_754,conjecture,? [X923] : b48_buttercup10596(X923) ).
fof(sos_755,conjecture,? [X924] : b48_buttercup10182(X924) ).
fof(sos_756,conjecture,? [X925] : b48_buttercup10575(X925) ).
fof(sos_757,conjecture,? [X926] : b48_buttercup10150(X926) ).
fof(sos_758,conjecture,? [X927] : b48_buttercup10156(X927) ).
fof(sos_759,conjecture,? [X928] : b48_buttercup10154(X928) ).
fof(sos_760,conjecture,? [X929] : b48_buttercup10013(X929) ).
fof(sos_761,conjecture,? [X930] : b48_buttercup10159(X930) ).
fof(sos_762,conjecture,? [X931] : b48_buttercup10158(X931) ).
fof(sos_763,conjecture,? [X932] : b48_buttercup10398(X932) ).
fof(sos_764,conjecture,? [X933] : b48_buttercup10394(X933) ).
fof(sos_765,conjecture,? [X934] : b48_buttercup10299(X934) ).
fof(sos_766,conjecture,? [X935] : b48_buttercup10496(X935) ).
fof(sos_767,conjecture,? [X936] : b48_buttercup10082(X936) ).
fof(sos_768,conjecture,? [X937] : b48_buttercup10493(X937) ).
fof(sos_769,conjecture,? [X938] : b48_buttercup10490(X938) ).
fof(sos_770,conjecture,? [X939] : b48_buttercup10606(X939) ).
fof(sos_771,conjecture,? [X940] : b48_buttercup10605(X940) ).
fof(sos_772,conjecture,? [X941] : b48_buttercup10604(X941) ).
fof(sos_773,conjecture,? [X942] : b48_buttercup10092(X942) ).
fof(sos_774,conjecture,? [X943] : b48_buttercup10313(X943) ).
fof(sos_775,conjecture,? [X944] : b48_buttercup10562(X944) ).
fof(sos_776,conjecture,? [X945] : b48_buttercup10563(X945) ).
fof(sos_777,conjecture,? [X946] : b48_buttercup10561(X946) ).
fof(sos_778,conjecture,? [X947] : b48_buttercup10318(X947) ).
fof(sos_779,conjecture,? [X948] : b48_buttercup10098(X948) ).
fof(sos_780,conjecture,? [X949] : b48_buttercup10086(X949) ).
fof(sos_781,conjecture,? [X950] : b48_buttercup10410(X950) ).
fof(sos_782,conjecture,? [X951] : b48_buttercup10411(X951) ).
fof(sos_783,conjecture,? [X952] : b48_buttercup10271(X952) ).
fof(sos_784,conjecture,? [X953] : b48_buttercup10609(X953) ).
fof(sos_785,conjecture,? [X954] : b48_buttercup10007(X954) ).
fof(sos_786,conjecture,? [X955] : b48_buttercup10214(X955) ).
fof(sos_787,conjecture,? [X956] : b48_buttercup10487(X956) ).
fof(sos_788,conjecture,? [X957] : b48_buttercup10120(X957) ).
fof(sos_789,conjecture,? [X958] : b48_buttercup10121(X958) ).
fof(sos_790,conjecture,? [X959] : b48_buttercup10326(X959) ).
fof(sos_791,conjecture,? [X960] : b48_buttercup10248(X960) ).
fof(sos_792,conjecture,? [X961] : b48_buttercup10320(X961) ).
fof(sos_793,conjecture,? [X962] : b48_buttercup10322(X962) ).
fof(sos_794,conjecture,? [X963] : b48_buttercup10247(X963) ).
fof(sos_795,conjecture,? [X964] : b48_buttercup10574(X964) ).
fof(sos_796,conjecture,? [X965] : b48_buttercup10521(X965) ).
fof(sos_797,conjecture,? [X966] : b48_buttercup10085(X966) ).
fof(sos_798,conjecture,? [X967] : b48_buttercup10570(X967) ).
fof(sos_799,conjecture,? [X968] : b48_buttercup10240(X968) ).
fof(sos_800,conjecture,? [X969] : b48_buttercup10405(X969) ).
fof(sos_801,conjecture,? [X970] : b48_buttercup10526(X970) ).
fof(sos_802,conjecture,? [X971] : b48_buttercup10024(X971) ).
fof(sos_803,conjecture,? [X972] : b48_buttercup10579(X972) ).
fof(sos_804,conjecture,? [X973] : b48_buttercup10402(X973) ).
fof(sos_805,conjecture,? [X974] : b48_buttercup10353(X974) ).
fof(sos_806,conjecture,? [X975] : b48_buttercup10034(X975) ).
fof(sos_807,conjecture,? [X976] : b48_buttercup10035(X976) ).
fof(sos_808,conjecture,? [X977] : b48_buttercup10031(X977) ).
fof(sos_809,conjecture,? [X978] : b48_buttercup10450(X978) ).
fof(sos_810,conjecture,? [X979] : b48_buttercup10134(X979) ).
fof(sos_811,conjecture,? [X980] : b48_buttercup10130(X980) ).
fof(sos_812,conjecture,? [X981] : b48_buttercup10133(X981) ).
fof(sos_813,conjecture,? [X982] : b48_buttercup10359(X982) ).
fof(sos_814,conjecture,? [X983] : b48_buttercup10334(X983) ).
fof(sos_815,conjecture,? [X984] : b48_buttercup10541(X984) ).
fof(sos_816,conjecture,? [X985] : b48_buttercup10542(X985) ).
fof(sos_817,conjecture,? [X986] : b48_buttercup10231(X986) ).
fof(sos_818,conjecture,? [X987] : b48_buttercup10545(X987) ).
fof(sos_819,conjecture,? [X988] : b48_buttercup10548(X988) ).
fof(sos_820,conjecture,? [X989] : b48_buttercup10549(X989) ).
fof(sos_821,conjecture,? [X990] : b48_buttercup10433(X990) ).
fof(sos_822,conjecture,? [X991] : b48_buttercup10434(X991) ).
fof(sos_823,conjecture,? [X992] : b48_buttercup10417(X992) ).
fof(sos_824,conjecture,? [X993] : b48_buttercup10143(X993) ).
fof(sos_825,conjecture,? [X994] : b48_buttercup10022(X994) ).
fof(sos_826,conjecture,? [X995] : b48_buttercup10021(X995) ).
fof(sos_827,conjecture,? [X996] : b48_buttercup10253(X996) ).
fof(sos_828,conjecture,? [X997] : b48_buttercup10636(X997) ).
fof(sos_829,conjecture,? [X998] : b48_buttercup10029(X998) ).
fof(sos_830,conjecture,? [X999] : b48_buttercup10456(X999) ).
fof(sos_831,conjecture,? [X1000] : b48_buttercup10102(X1000) ).
fof(sos_832,conjecture,? [X1001] : b48_buttercup10104(X1001) ).
fof(sos_833,conjecture,? [X1002] : b48_buttercup10309(X1002) ).
fof(sos_834,conjecture,? [X1003] : b48_buttercup10107(X1003) ).
fof(sos_835,conjecture,? [X1004] : b48_buttercup10108(X1004) ).
fof(sos_836,conjecture,? [X1005] : b48_buttercup10109(X1005) ).
fof(sos_837,conjecture,? [X1006] : b48_buttercup10198(X1006) ).
fof(sos_838,conjecture,? [X1007] : b48_buttercup10518(X1007) ).
fof(sos_839,conjecture,? [X1008] : b48_buttercup10552(X1008) ).
fof(sos_840,conjecture,? [X1009] : b48_buttercup10427(X1009) ).
fof(sos_841,conjecture,? [X1010] : b48_buttercup10220(X1010) ).
fof(sos_842,conjecture,? [X1011] : b48_buttercup10222(X1011) ).
fof(sos_843,conjecture,? [X1012] : b48_buttercup10422(X1012) ).
fof(sos_844,conjecture,? [X1013] : b48_buttercup10348(X1013) ).
fof(sos_845,conjecture,? [X1014] : b48_buttercup10420(X1014) ).
fof(sos_846,conjecture,? [X1015] : b48_buttercup10229(X1015) ).
fof(sos_847,conjecture,? [X1016] : b48_buttercup10228(X1016) ).
fof(sos_848,conjecture,? [X1017] : b48_buttercup10344(X1017) ).
fof(sos_849,conjecture,? [X1018] : b48_buttercup10343(X1018) ).
fof(sos_850,conjecture,? [X1019] : b48_buttercup10186(X1019) ).
fof(sos_851,conjecture,? [X1020] : b48_buttercup10294(X1020) ).
fof(sos_852,conjecture,? [X1021] : b48_buttercup10290(X1021) ).
fof(sos_853,conjecture,? [X1022] : b48_buttercup10291(X1022) ).
fof(sos_854,conjecture,? [X1023] : b48_buttercup10119(X1023) ).
fof(sos_855,conjecture,? [X1024] : b48_buttercup10454(X1024) ).
fof(sos_856,conjecture,? [X1025] : b48_buttercup10115(X1025) ).
fof(sos_857,conjecture,? [X1026] : b48_buttercup10300(X1026) ).
fof(sos_858,conjecture,? [X1027] : b48_buttercup10111(X1027) ).
fof(sos_859,conjecture,? [X1028] : b48_buttercup10110(X1028) ).
fof(sos_860,conjecture,? [X1029] : b48_buttercup10642(X1029) ).
fof(sos_861,conjecture,? [X1030] : b48_buttercup10054(X1030) ).
fof(sos_862,conjecture,? [X1031] : b48_buttercup10640(X1031) ).
fof(sos_863,conjecture,? [X1032] : b48_buttercup10052(X1032) ).
fof(sos_864,conjecture,? [X1033] : b48_buttercup10646(X1033) ).
fof(sos_865,conjecture,? [X1034] : b48_buttercup10050(X1034) ).
fof(sos_866,conjecture,? [X1035] : b48_buttercup10522(X1035) ).
fof(sos_867,conjecture,? [X1036] : b48_buttercup10520(X1036) ).
fof(sos_868,conjecture,? [X1037] : b48_buttercup10217(X1037) ).
fof(sos_869,conjecture,? [X1038] : b48_buttercup10210(X1038) ).
fof(sos_870,conjecture,? [X1039] : b48_buttercup10058(X1039) ).
fof(sos_871,conjecture,? [X1040] : b48_buttercup10268(X1040) ).
fof(sos_872,conjecture,? [X1041] : b48_buttercup10197(X1041) ).
fof(sos_873,conjecture,? [X1042] : b48_buttercup10196(X1042) ).
fof(sos_874,conjecture,? [X1043] : b48_buttercup10195(X1043) ).
fof(sos_875,conjecture,? [X1044] : b48_buttercup10451(X1044) ).
fof(sos_876,conjecture,? [X1045] : b48_buttercup10193(X1045) ).
fof(sos_877,conjecture,? [X1046] : b48_buttercup10227(X1046) ).
fof(sos_878,conjecture,? [X1047] : b48_buttercup10191(X1047) ).
fof(sos_879,conjecture,? [X1048] : b48_buttercup10458(X1048) ).
fof(sos_880,conjecture,? [X1049] : b48_buttercup10199(X1049) ).
fof(sos_881,conjecture,? [X1050] : b48_buttercup10352(X1050) ).
fof(sos_882,conjecture,? [X1051] : b48_buttercup10180(X1051) ).
fof(sos_883,conjecture,? [X1052] : b48_buttercup10572(X1052) ).
fof(sos_884,conjecture,? [X1053] : b48_buttercup10308(X1053) ).
fof(sos_885,conjecture,? [X1054] : b48_buttercup10479(X1054) ).
fof(goals_886,conjecture,~(! [X1055] : ( b48_buttercup10305(X1055) <=> k04_buttercup10303(X1055) ) | ( ! [X1056] : ( k04_buttercup10303(X1056) => b48_buttercup10305(X1056) ) & ? [X1057] : ( b48_buttercup10305(X1057) & ~ k04_buttercup10303(X1057) ) ) | ? [X1058] : ? [X1059] : ? [X1060] : ( b48_buttercup10305(X1058) & k04_buttercup10303(X1058) & b48_buttercup10305(X1059) & ~ k04_buttercup10303(X1059) & ~ b48_buttercup10305(X1060) & k04_buttercup10303(X1060) ) | ! [X1061] : ( b48_buttercup10305(X1061) => ~ k04_buttercup10303(X1061) ) )).
