fof(clause1,conjecture,~ ssSkC10 ).
fof(clause2,conjecture,~ ssSkC9 ).
fof(clause3,conjecture,~ ssSkC8 ).
fof(clause4,conjecture,~ ssSkC7 ).
fof(clause5,conjecture,~ ssSkC6 ).
fof(clause6,conjecture,~ ssSkC5 ).
fof(clause7,conjecture,~ ssSkC4 ).
fof(clause8,conjecture,~ ssSkC3 ).
fof(clause9,conjecture,~ ssSkC2 ).
fof(clause10,conjecture,~ ssSkC1 ).
fof(clause11,conjecture,~ ssSkC0 ).
fof(clause12,conjecture,ssSkP678(skc21) | ssSkC10 ).
fof(clause13,conjecture,ssSkP515(skc20) | ssSkC9 ).
fof(clause14,conjecture,ssSkP455(skc19) | ssSkC8 ).
fof(clause15,conjecture,ssSkP401(skc18) | ssSkC7 ).
fof(clause16,conjecture,ssSkP347(skc17) | ssSkC6 ).
fof(clause17,conjecture,ssSkP287(skc16) | ssSkC5 ).
fof(clause18,conjecture,ssSkP236(skc15) | ssSkC4 ).
fof(clause19,conjecture,ssSkP190(skc14) | ssSkC3 ).
fof(clause20,conjecture,ssSkP148(skc13) | ssSkC2 ).
fof(clause21,conjecture,ssSkP100(skc12) | ssSkC1 ).
fof(clause22,conjecture,ssSkP59(skc11) | ssSkC0 ).
fof(clause23,conjecture,! [U] : ( ~ ssSkP545(U) | ssSkP532(U) ) ).
fof(clause24,conjecture,! [U] : ( ~ ssSkP545(U) | ssPv48(U) ) ).
fof(clause25,conjecture,! [U] : ( ~ ssSkP546(U) | ssSkP533(U) ) ).
fof(clause26,conjecture,! [U] : ( ~ ssSkP546(U) | ssPv25(U) ) ).
fof(clause27,conjecture,! [U] : ( ~ ssSkP547(U) | ssSkP535(U) ) ).
fof(clause28,conjecture,! [U] : ( ~ ssSkP547(U) | ssPv47(U) ) ).
fof(clause29,conjecture,! [U] : ( ~ ssSkP548(U) | ssSkP542(U) ) ).
fof(clause30,conjecture,! [U] : ( ~ ssSkP548(U) | ssPv9(U) ) ).
fof(clause31,conjecture,! [U] : ( ~ ssSkP549(U) | ssSkP538(U) ) ).
fof(clause32,conjecture,! [U] : ( ~ ssSkP549(U) | ssPv46(U) ) ).
fof(clause33,conjecture,! [U] : ( ~ ssSkP550(U) | ssSkP539(U) ) ).
fof(clause34,conjecture,! [U] : ( ~ ssSkP550(U) | ssPv16(U) ) ).
fof(clause35,conjecture,! [U] : ( ~ ssSkP551(U) | ssSkP541(U) ) ).
fof(clause36,conjecture,! [U] : ( ~ ssSkP551(U) | ssPv41(U) ) ).
fof(clause37,conjecture,! [U] : ( ~ ssSkP552(U) | ssSkP537(U) ) ).
fof(clause38,conjecture,! [U] : ( ~ ssSkP552(U) | ssPv11(U) ) ).
fof(clause39,conjecture,! [U] : ( ~ ssSkP553(U) | ssSkP544(U) ) ).
fof(clause40,conjecture,! [U] : ( ~ ssSkP553(U) | ssPv30(U) ) ).
fof(clause41,conjecture,! [U] : ( ~ ssSkP554(U) | ssSkP534(U) ) ).
fof(clause42,conjecture,! [U] : ( ~ ssSkP554(U) | ssPv14(U) ) ).
fof(clause43,conjecture,! [U] : ( ~ ssSkP555(U) | ssSkP536(U) ) ).
fof(clause44,conjecture,! [U] : ( ~ ssSkP555(U) | ssPv29(U) ) ).
fof(clause45,conjecture,! [U] : ( ~ ssSkP557(U) | ssSkP540(U) ) ).
fof(clause46,conjecture,! [U] : ( ~ ssSkP557(U) | ssPv28(U) ) ).
fof(clause47,conjecture,! [U] : ( ~ ssSkP558(U) | ssSkP543(U) ) ).
fof(clause48,conjecture,! [U] : ( ~ ssSkP558(U) | ssPv12(U) ) ).
fof(clause49,conjecture,! [U] : ( ~ ssSkP559(U) | ssSkP516(U) ) ).
fof(clause50,conjecture,! [U] : ( ~ ssSkP559(U) | ssSkP556(U) ) ).
fof(clause51,conjecture,! [U] : ( ~ ssSkP574(U) | ssSkP573(U) ) ).
fof(clause52,conjecture,! [U] : ( ~ ssSkP576(U) | ssSkP575(U) ) ).
fof(clause53,conjecture,! [U] : ( ~ ssSkP578(U) | ssSkP577(U) ) ).
fof(clause54,conjecture,! [U] : ( ~ ssSkP580(U) | ssSkP579(U) ) ).
fof(clause55,conjecture,! [U] : ( ~ ssSkP582(U) | ssSkP581(U) ) ).
fof(clause56,conjecture,! [U] : ( ~ ssSkP584(U) | ssSkP572(U) ) ).
fof(clause57,conjecture,! [U] : ( ~ ssSkP584(U) | ssSkP583(U) ) ).
fof(clause58,conjecture,! [U] : ( ~ ssSkP586(U) | ssSkP585(U) ) ).
fof(clause59,conjecture,! [U] : ( ~ ssSkP588(U) | ssSkP571(U) ) ).
fof(clause60,conjecture,! [U] : ( ~ ssSkP588(U) | ssSkP587(U) ) ).
fof(clause61,conjecture,! [U] : ( ~ ssSkP590(U) | ssSkP570(U) ) ).
fof(clause62,conjecture,! [U] : ( ~ ssSkP590(U) | ssSkP589(U) ) ).
fof(clause63,conjecture,! [U] : ( ~ ssSkP592(U) | ssSkP591(U) ) ).
fof(clause64,conjecture,! [U] : ( ~ ssSkP594(U) | ssSkP569(U) ) ).
fof(clause65,conjecture,! [U] : ( ~ ssSkP594(U) | ssSkP593(U) ) ).
fof(clause66,conjecture,! [U] : ( ~ ssSkP596(U) | ssSkP595(U) ) ).
fof(clause67,conjecture,! [U] : ( ~ ssSkP598(U) | ssSkP568(U) ) ).
fof(clause68,conjecture,! [U] : ( ~ ssSkP598(U) | ssSkP597(U) ) ).
fof(clause69,conjecture,! [U] : ( ~ ssSkP600(U) | ssSkP599(U) ) ).
fof(clause70,conjecture,! [U] : ( ~ ssSkP602(U) | ssSkP601(U) ) ).
fof(clause71,conjecture,! [U] : ( ~ ssSkP604(U) | ssSkP603(U) ) ).
fof(clause72,conjecture,! [U] : ( ~ ssSkP606(U) | ssSkP605(U) ) ).
fof(clause73,conjecture,! [U] : ( ~ ssSkP608(U) | ssSkP607(U) ) ).
fof(clause74,conjecture,! [U] : ( ~ ssSkP610(U) | ssSkP609(U) ) ).
fof(clause75,conjecture,! [U] : ( ~ ssSkP612(U) | ssSkP611(U) ) ).
fof(clause76,conjecture,! [U] : ( ~ ssSkP614(U) | ssSkP613(U) ) ).
fof(clause77,conjecture,! [U] : ( ~ ssSkP616(U) | ssSkP567(U) ) ).
fof(clause78,conjecture,! [U] : ( ~ ssSkP616(U) | ssSkP615(U) ) ).
fof(clause79,conjecture,! [U] : ( ~ ssSkP618(U) | ssSkP617(U) ) ).
fof(clause80,conjecture,! [U] : ( ~ ssSkP620(U) | ssSkP619(U) ) ).
fof(clause81,conjecture,! [U] : ( ~ ssSkP622(U) | ssSkP566(U) ) ).
fof(clause82,conjecture,! [U] : ( ~ ssSkP622(U) | ssSkP621(U) ) ).
fof(clause83,conjecture,! [U] : ( ~ ssSkP624(U) | ssSkP565(U) ) ).
fof(clause84,conjecture,! [U] : ( ~ ssSkP624(U) | ssSkP623(U) ) ).
fof(clause85,conjecture,! [U] : ( ~ ssSkP626(U) | ssSkP564(U) ) ).
fof(clause86,conjecture,! [U] : ( ~ ssSkP626(U) | ssSkP625(U) ) ).
fof(clause87,conjecture,! [U] : ( ~ ssSkP628(U) | ssSkP627(U) ) ).
fof(clause88,conjecture,! [U] : ( ~ ssSkP630(U) | ssSkP629(U) ) ).
fof(clause89,conjecture,! [U] : ( ~ ssSkP632(U) | ssSkP631(U) ) ).
fof(clause90,conjecture,! [U] : ( ~ ssSkP634(U) | ssSkP633(U) ) ).
fof(clause91,conjecture,! [U] : ( ~ ssSkP636(U) | ssSkP635(U) ) ).
fof(clause92,conjecture,! [U] : ( ~ ssSkP638(U) | ssSkP637(U) ) ).
fof(clause93,conjecture,! [U] : ( ~ ssSkP640(U) | ssSkP639(U) ) ).
fof(clause94,conjecture,! [U] : ( ~ ssSkP642(U) | ssSkP641(U) ) ).
fof(clause95,conjecture,! [U] : ( ~ ssSkP644(U) | ssSkP643(U) ) ).
fof(clause96,conjecture,! [U] : ( ~ ssSkP646(U) | ssSkP645(U) ) ).
fof(clause97,conjecture,! [U] : ( ~ ssSkP648(U) | ssSkP563(U) ) ).
fof(clause98,conjecture,! [U] : ( ~ ssSkP648(U) | ssSkP647(U) ) ).
fof(clause99,conjecture,! [U] : ( ~ ssSkP650(U) | ssSkP649(U) ) ).
fof(clause100,conjecture,! [U] : ( ~ ssSkP652(U) | ssSkP651(U) ) ).
fof(clause101,conjecture,! [U] : ( ~ ssSkP654(U) | ssSkP653(U) ) ).
fof(clause102,conjecture,! [U] : ( ~ ssSkP656(U) | ssSkP655(U) ) ).
fof(clause103,conjecture,! [U] : ( ~ ssSkP658(U) | ssSkP562(U) ) ).
fof(clause104,conjecture,! [U] : ( ~ ssSkP658(U) | ssSkP657(U) ) ).
fof(clause105,conjecture,! [U] : ( ~ ssSkP660(U) | ssSkP561(U) ) ).
fof(clause106,conjecture,! [U] : ( ~ ssSkP660(U) | ssSkP659(U) ) ).
fof(clause107,conjecture,! [U] : ( ~ ssSkP662(U) | ssSkP560(U) ) ).
fof(clause108,conjecture,! [U] : ( ~ ssSkP662(U) | ssSkP661(U) ) ).
fof(clause109,conjecture,! [U] : ( ~ ssSkP664(U) | ssSkP663(U) ) ).
fof(clause110,conjecture,! [U] : ( ~ ssSkP666(U) | ssSkP665(U) ) ).
fof(clause111,conjecture,! [U] : ( ~ ssSkP668(U) | ssSkP667(U) ) ).
fof(clause112,conjecture,! [U] : ( ~ ssSkP670(U) | ssSkP669(U) ) ).
fof(clause113,conjecture,! [U] : ( ~ ssSkP672(U) | ssSkP671(U) ) ).
fof(clause114,conjecture,! [U] : ( ~ ssSkP674(U) | ssSkP673(U) ) ).
fof(clause115,conjecture,! [U] : ( ~ ssSkP676(U) | ssSkP675(U) ) ).
fof(clause116,conjecture,! [U] : ( ~ ssSkP678(U) | ssSkP677(U) ) ).
fof(clause117,conjecture,! [U] : ( ~ ssSkP532(U) | ssSkP518(skf94(U)) ) ).
fof(clause118,conjecture,! [U] : ( ~ ssSkP533(U) | ssSkP529(skf95(U)) ) ).
fof(clause119,conjecture,! [U] : ( ~ ssSkP534(U) | ssSkP524(skf96(U)) ) ).
fof(clause120,conjecture,! [U] : ( ~ ssSkP535(U) | ssSkP522(skf97(U)) ) ).
fof(clause121,conjecture,! [U] : ( ~ ssSkP536(U) | ssSkP528(skf98(U)) ) ).
fof(clause122,conjecture,! [U] : ( ~ ssSkP537(U) | ssSkP520(skf99(U)) ) ).
fof(clause123,conjecture,! [U] : ( ~ ssSkP538(U) | ssSkP526(skf100(U)) ) ).
fof(clause124,conjecture,! [U] : ( ~ ssSkP539(U) | ssSkP525(skf101(U)) ) ).
fof(clause125,conjecture,! [U] : ( ~ ssSkP540(U) | ssSkP521(skf102(U)) ) ).
fof(clause126,conjecture,! [U] : ( ~ ssSkP541(U) | ssSkP530(skf103(U)) ) ).
fof(clause127,conjecture,! [U] : ( ~ ssSkP542(U) | ssSkP519(skf104(U)) ) ).
fof(clause128,conjecture,! [U] : ( ~ ssSkP543(U) | ssSkP527(skf105(U)) ) ).
fof(clause129,conjecture,! [U] : ( ~ ssSkP544(U) | ssSkP523(skf106(U)) ) ).
fof(clause130,conjecture,! [U] : ( ~ ssSkP560(U) | ssSkP545(skf107(U)) ) ).
fof(clause131,conjecture,! [U] : ( ~ ssSkP561(U) | ssSkP547(skf108(U)) ) ).
fof(clause132,conjecture,! [U] : ( ~ ssSkP562(U) | ssSkP549(skf109(U)) ) ).
fof(clause133,conjecture,! [U] : ( ~ ssSkP563(U) | ssSkP551(skf110(U)) ) ).
fof(clause134,conjecture,! [U] : ( ~ ssSkP564(U) | ssSkP553(skf111(U)) ) ).
fof(clause135,conjecture,! [U] : ( ~ ssSkP565(U) | ssSkP555(skf112(U)) ) ).
fof(clause136,conjecture,! [U] : ( ~ ssSkP566(U) | ssSkP557(skf113(U)) ) ).
fof(clause137,conjecture,! [U] : ( ~ ssSkP567(U) | ssSkP546(skf114(U)) ) ).
fof(clause138,conjecture,! [U] : ( ~ ssSkP568(U) | ssSkP550(skf115(U)) ) ).
fof(clause139,conjecture,! [U] : ( ~ ssSkP569(U) | ssSkP554(skf116(U)) ) ).
fof(clause140,conjecture,! [U] : ( ~ ssSkP570(U) | ssSkP558(skf117(U)) ) ).
fof(clause141,conjecture,! [U] : ( ~ ssSkP571(U) | ssSkP552(skf118(U)) ) ).
fof(clause142,conjecture,! [U] : ( ~ ssSkP572(U) | ssSkP548(skf119(U)) ) ).
fof(clause143,conjecture,! [U] : ( ~ ssSkP516(U) | ssRr(U,skf80(U)) ) ).
fof(clause144,conjecture,! [U] : ( ~ ssPv48(skf81(U)) | ~ ssSkP518(U) ) ).
fof(clause145,conjecture,! [U] : ( ~ ssSkP518(U) | ssRr(U,skf81(U)) ) ).
fof(clause146,conjecture,! [U] : ( ~ ssPv9(skf82(U)) | ~ ssSkP519(U) ) ).
fof(clause147,conjecture,! [U] : ( ~ ssSkP519(U) | ssRr(U,skf82(U)) ) ).
fof(clause148,conjecture,! [U] : ( ~ ssPv11(skf83(U)) | ~ ssSkP520(U) ) ).
fof(clause149,conjecture,! [U] : ( ~ ssSkP520(U) | ssRr(U,skf83(U)) ) ).
fof(clause150,conjecture,! [U] : ( ~ ssPv28(skf84(U)) | ~ ssSkP521(U) ) ).
fof(clause151,conjecture,! [U] : ( ~ ssSkP521(U) | ssRr(U,skf84(U)) ) ).
fof(clause152,conjecture,! [U] : ( ~ ssPv47(skf85(U)) | ~ ssSkP522(U) ) ).
fof(clause153,conjecture,! [U] : ( ~ ssSkP522(U) | ssRr(U,skf85(U)) ) ).
fof(clause154,conjecture,! [U] : ( ~ ssPv30(skf86(U)) | ~ ssSkP523(U) ) ).
fof(clause155,conjecture,! [U] : ( ~ ssSkP523(U) | ssRr(U,skf86(U)) ) ).
fof(clause156,conjecture,! [U] : ( ~ ssPv14(skf87(U)) | ~ ssSkP524(U) ) ).
fof(clause157,conjecture,! [U] : ( ~ ssSkP524(U) | ssRr(U,skf87(U)) ) ).
fof(clause158,conjecture,! [U] : ( ~ ssPv16(skf88(U)) | ~ ssSkP525(U) ) ).
fof(clause159,conjecture,! [U] : ( ~ ssSkP525(U) | ssRr(U,skf88(U)) ) ).
fof(clause160,conjecture,! [U] : ( ~ ssPv46(skf89(U)) | ~ ssSkP526(U) ) ).
fof(clause161,conjecture,! [U] : ( ~ ssSkP526(U) | ssRr(U,skf89(U)) ) ).
fof(clause162,conjecture,! [U] : ( ~ ssPv12(skf90(U)) | ~ ssSkP527(U) ) ).
fof(clause163,conjecture,! [U] : ( ~ ssSkP527(U) | ssRr(U,skf90(U)) ) ).
fof(clause164,conjecture,! [U] : ( ~ ssPv29(skf91(U)) | ~ ssSkP528(U) ) ).
fof(clause165,conjecture,! [U] : ( ~ ssSkP528(U) | ssRr(U,skf91(U)) ) ).
fof(clause166,conjecture,! [U] : ( ~ ssPv25(skf92(U)) | ~ ssSkP529(U) ) ).
fof(clause167,conjecture,! [U] : ( ~ ssSkP529(U) | ssRr(U,skf92(U)) ) ).
fof(clause168,conjecture,! [U] : ( ~ ssPv41(skf93(U)) | ~ ssSkP530(U) ) ).
fof(clause169,conjecture,! [U] : ( ~ ssSkP530(U) | ssRr(U,skf93(U)) ) ).
fof(clause170,conjecture,! [U] : ( ~ ssSkP532(U) | ssRr(skf94(U),U) ) ).
fof(clause171,conjecture,! [U] : ( ~ ssSkP533(U) | ssRr(skf95(U),U) ) ).
fof(clause172,conjecture,! [U] : ( ~ ssSkP534(U) | ssRr(skf96(U),U) ) ).
fof(clause173,conjecture,! [U] : ( ~ ssSkP535(U) | ssRr(skf97(U),U) ) ).
fof(clause174,conjecture,! [U] : ( ~ ssSkP536(U) | ssRr(skf98(U),U) ) ).
fof(clause175,conjecture,! [U] : ( ~ ssSkP537(U) | ssRr(skf99(U),U) ) ).
fof(clause176,conjecture,! [U] : ( ~ ssSkP538(U) | ssRr(skf100(U),U) ) ).
fof(clause177,conjecture,! [U] : ( ~ ssSkP539(U) | ssRr(skf101(U),U) ) ).
fof(clause178,conjecture,! [U] : ( ~ ssSkP540(U) | ssRr(skf102(U),U) ) ).
fof(clause179,conjecture,! [U] : ( ~ ssSkP541(U) | ssRr(skf103(U),U) ) ).
fof(clause180,conjecture,! [U] : ( ~ ssSkP542(U) | ssRr(skf104(U),U) ) ).
fof(clause181,conjecture,! [U] : ( ~ ssSkP543(U) | ssRr(skf105(U),U) ) ).
fof(clause182,conjecture,! [U] : ( ~ ssSkP544(U) | ssRr(skf106(U),U) ) ).
fof(clause183,conjecture,! [U] : ( ~ ssSkP560(U) | ssRr(U,skf107(U)) ) ).
fof(clause184,conjecture,! [U] : ( ~ ssSkP561(U) | ssRr(U,skf108(U)) ) ).
fof(clause185,conjecture,! [U] : ( ~ ssSkP562(U) | ssRr(U,skf109(U)) ) ).
fof(clause186,conjecture,! [U] : ( ~ ssSkP563(U) | ssRr(U,skf110(U)) ) ).
fof(clause187,conjecture,! [U] : ( ~ ssSkP564(U) | ssRr(U,skf111(U)) ) ).
fof(clause188,conjecture,! [U] : ( ~ ssSkP565(U) | ssRr(U,skf112(U)) ) ).
fof(clause189,conjecture,! [U] : ( ~ ssSkP566(U) | ssRr(U,skf113(U)) ) ).
fof(clause190,conjecture,! [U] : ( ~ ssSkP567(U) | ssRr(U,skf114(U)) ) ).
fof(clause191,conjecture,! [U] : ( ~ ssSkP568(U) | ssRr(U,skf115(U)) ) ).
fof(clause192,conjecture,! [U] : ( ~ ssSkP569(U) | ssRr(U,skf116(U)) ) ).
fof(clause193,conjecture,! [U] : ( ~ ssSkP570(U) | ssRr(U,skf117(U)) ) ).
fof(clause194,conjecture,! [U] : ( ~ ssSkP571(U) | ssRr(U,skf118(U)) ) ).
fof(clause195,conjecture,! [U] : ( ~ ssSkP572(U) | ssRr(U,skf119(U)) ) ).
fof(clause196,conjecture,! [U] : ( ~ ssSkP574(U) | ssRr(U,skf120(U)) ) ).
fof(clause197,conjecture,! [U] : ( ~ ssSkP576(U) | ssRr(U,skf121(U)) ) ).
fof(clause198,conjecture,! [U] : ( ~ ssSkP578(U) | ssRr(U,skf122(U)) ) ).
fof(clause199,conjecture,! [U] : ( ~ ssSkP580(U) | ssRr(U,skf123(U)) ) ).
fof(clause200,conjecture,! [U] : ( ~ ssSkP582(U) | ssRr(U,skf124(U)) ) ).
fof(clause201,conjecture,! [U] : ( ~ ssSkP586(U) | ssRr(U,skf125(U)) ) ).
fof(clause202,conjecture,! [U] : ( ~ ssSkP592(U) | ssRr(U,skf126(U)) ) ).
fof(clause203,conjecture,! [U] : ( ~ ssSkP596(U) | ssRr(U,skf127(U)) ) ).
fof(clause204,conjecture,! [U] : ( ~ ssSkP600(U) | ssRr(U,skf128(U)) ) ).
fof(clause205,conjecture,! [U] : ( ~ ssSkP602(U) | ssRr(U,skf129(U)) ) ).
fof(clause206,conjecture,! [U] : ( ~ ssSkP604(U) | ssRr(U,skf130(U)) ) ).
fof(clause207,conjecture,! [U] : ( ~ ssSkP606(U) | ssRr(U,skf131(U)) ) ).
fof(clause208,conjecture,! [U] : ( ~ ssSkP608(U) | ssRr(U,skf132(U)) ) ).
fof(clause209,conjecture,! [U] : ( ~ ssSkP610(U) | ssRr(U,skf133(U)) ) ).
fof(clause210,conjecture,! [U] : ( ~ ssSkP612(U) | ssRr(U,skf134(U)) ) ).
fof(clause211,conjecture,! [U] : ( ~ ssSkP614(U) | ssRr(U,skf135(U)) ) ).
fof(clause212,conjecture,! [U] : ( ~ ssSkP618(U) | ssRr(U,skf136(U)) ) ).
fof(clause213,conjecture,! [U] : ( ~ ssSkP620(U) | ssRr(U,skf137(U)) ) ).
fof(clause214,conjecture,! [U] : ( ~ ssSkP628(U) | ssRr(U,skf138(U)) ) ).
fof(clause215,conjecture,! [U] : ( ~ ssSkP630(U) | ssRr(U,skf139(U)) ) ).
fof(clause216,conjecture,! [U] : ( ~ ssSkP632(U) | ssRr(U,skf140(U)) ) ).
fof(clause217,conjecture,! [U] : ( ~ ssSkP634(U) | ssRr(U,skf141(U)) ) ).
fof(clause218,conjecture,! [U] : ( ~ ssSkP636(U) | ssRr(U,skf142(U)) ) ).
fof(clause219,conjecture,! [U] : ( ~ ssSkP638(U) | ssRr(U,skf143(U)) ) ).
fof(clause220,conjecture,! [U] : ( ~ ssSkP640(U) | ssRr(U,skf144(U)) ) ).
fof(clause221,conjecture,! [U] : ( ~ ssSkP642(U) | ssRr(U,skf145(U)) ) ).
fof(clause222,conjecture,! [U] : ( ~ ssSkP644(U) | ssRr(U,skf146(U)) ) ).
fof(clause223,conjecture,! [U] : ( ~ ssSkP646(U) | ssRr(U,skf147(U)) ) ).
fof(clause224,conjecture,! [U] : ( ~ ssSkP650(U) | ssRr(U,skf148(U)) ) ).
fof(clause225,conjecture,! [U] : ( ~ ssSkP652(U) | ssRr(U,skf149(U)) ) ).
fof(clause226,conjecture,! [U] : ( ~ ssSkP654(U) | ssRr(U,skf150(U)) ) ).
fof(clause227,conjecture,! [U] : ( ~ ssSkP656(U) | ssRr(U,skf151(U)) ) ).
fof(clause228,conjecture,! [U] : ( ~ ssSkP664(U) | ssRr(U,skf152(U)) ) ).
fof(clause229,conjecture,! [U] : ( ~ ssSkP666(U) | ssRr(U,skf153(U)) ) ).
fof(clause230,conjecture,! [U] : ( ~ ssSkP668(U) | ssRr(U,skf154(U)) ) ).
fof(clause231,conjecture,! [U] : ( ~ ssSkP670(U) | ssRr(U,skf155(U)) ) ).
fof(clause232,conjecture,! [U] : ( ~ ssSkP672(U) | ssRr(U,skf156(U)) ) ).
fof(clause233,conjecture,! [U] : ( ~ ssSkP674(U) | ssRr(U,skf157(U)) ) ).
fof(clause234,conjecture,! [U] : ( ~ ssSkP676(U) | ssRr(U,skf158(U)) ) ).
fof(clause235,conjecture,! [U] : ( ~ ssSkP678(U) | ssRr(U,skf159(U)) ) ).
fof(clause236,conjecture,! [U] : ( ~ ssSkP426(U) | ssPv28(U) | ssSkP425(U) ) ).
fof(clause237,conjecture,! [U] : ( ~ ssSkP417(U) | ssPv20(U) | ssSkP416(U) ) ).
fof(clause238,conjecture,! [U] : ( ~ ssSkP405(U) | ssPv9(U) | ssSkP404(U) ) ).
fof(clause239,conjecture,! [U] : ( ~ ssSkP378(U) | ssPv34(U) | ssSkP377(U) ) ).
fof(clause240,conjecture,! [U] : ( ~ ssSkP372(U) | ssPv29(U) | ssSkP371(U) ) ).
fof(clause241,conjecture,! [U] : ( ~ ssSkP319(U) | ssPv30(U) | ssSkP318(U) ) ).
fof(clause242,conjecture,! [U] : ( ~ ssSkP271(U) | ssPv41(U) | ssSkP270(U) ) ).
fof(clause243,conjecture,! [U] : ( ~ ssSkP252(U) | ssPv24(U) | ssSkP251(U) ) ).
fof(clause244,conjecture,! [U] : ( ~ ssSkP194(U) | ssPv17(U) | ssSkP193(U) ) ).
fof(clause245,conjecture,! [U] : ( ~ ssSkP178(U) | ssPv46(U) | ssSkP177(U) ) ).
fof(clause246,conjecture,! [U] : ( ~ ssSkP167(U) | ssPv36(U) | ssSkP166(U) ) ).
fof(clause247,conjecture,! [U] : ( ~ ssSkP119(U) | ssPv30(U) | ssSkP118(U) ) ).
fof(clause248,conjecture,! [U] : ( ~ ssSkP83(U) | ssPv41(U) | ssSkP82(U) ) ).
fof(clause249,conjecture,! [U] : ( ~ ssSkP55(U) | ssPv53(U) | ssSkP54(U) ) ).
fof(clause250,conjecture,! [U] : ( ~ ssSkP25(U) | ssPv25(U) | ssSkP24(U) ) ).
fof(clause251,conjecture,! [U] : ( ~ ssSkP486(U) | ~ ssPv28(U) | ssSkP485(U) ) ).
fof(clause252,conjecture,! [U] : ( ~ ssSkP479(U) | ~ ssPv22(U) | ssSkP478(U) ) ).
fof(clause253,conjecture,! [U] : ( ~ ssSkP468(U) | ~ ssPv12(U) | ssSkP467(U) ) ).
fof(clause254,conjecture,! [U] : ( ~ ssSkP358(U) | ~ ssPv16(U) | ssSkP357(U) ) ).
fof(clause255,conjecture,! [U] : ( ~ ssSkP329(U) | ~ ssPv39(U) | ssSkP328(U) ) ).
fof(clause256,conjecture,! [U] : ( ~ ssSkP316(U) | ~ ssPv28(U) | ssSkP315(U) ) ).
fof(clause257,conjecture,! [U] : ( ~ ssSkP268(U) | ~ ssPv39(U) | ssSkP267(U) ) ).
fof(clause258,conjecture,! [U] : ( ~ ssSkP226(U) | ~ ssPv47(U) | ssSkP225(U) ) ).
fof(clause259,conjecture,! [U] : ( ~ ssSkP200(U) | ~ ssPv22(U) | ssSkP199(U) ) ).
fof(clause260,conjecture,! [U] : ( ~ ssSkP181(U) | ~ ssPv48(U) | ssSkP180(U) ) ).
fof(clause261,conjecture,! [U] : ( ~ ssSkP141(U) | ~ ssPv50(U) | ssSkP140(U) ) ).
fof(clause262,conjecture,! [U] : ( ~ ssSkP126(U) | ~ ssPv36(U) | ssSkP125(U) ) ).
fof(clause263,conjecture,! [U] : ( ~ ssSkP95(U) | ~ ssPv52(U) | ssSkP94(U) ) ).
fof(clause264,conjecture,! [U] : ( ~ ssSkP69(U) | ~ ssPv28(U) | ssSkP68(U) ) ).
fof(clause265,conjecture,! [U] : ( ~ ssSkP49(U) | ~ ssPv48(U) | ssSkP48(U) ) ).
fof(clause266,conjecture,! [U] : ! [V] : ( ~ ssSkP531(U,V) | ~ ssSkP677(V) | ssSkP676(U) ) ).
fof(clause267,conjecture,! [U] : ! [V] : ( ~ ssSkP531(U,V) | ~ ssSkP675(V) | ssSkP674(U) ) ).
fof(clause268,conjecture,! [U] : ! [V] : ( ~ ssSkP457(U,V) | ~ ssSkP515(V) | ssSkP514(U) ) ).
fof(clause269,conjecture,! [U] : ! [V] : ( ~ ssSkP457(U,V) | ~ ssSkP514(V) | ssSkP513(U) ) ).
fof(clause270,conjecture,! [U] : ! [V] : ( ~ ssSkP403(U,V) | ~ ssSkP455(V) | ssSkP454(U) ) ).
fof(clause271,conjecture,! [U] : ! [V] : ( ~ ssSkP403(U,V) | ~ ssSkP454(V) | ssSkP453(U) ) ).
fof(clause272,conjecture,! [U] : ! [V] : ( ~ ssSkP349(U,V) | ~ ssSkP401(V) | ssSkP400(U) ) ).
fof(clause273,conjecture,! [U] : ! [V] : ( ~ ssSkP349(U,V) | ~ ssSkP400(V) | ssSkP399(U) ) ).
fof(clause274,conjecture,! [U] : ! [V] : ( ~ ssSkP289(U,V) | ~ ssSkP347(V) | ssSkP346(U) ) ).
fof(clause275,conjecture,! [U] : ! [V] : ( ~ ssSkP289(U,V) | ~ ssSkP346(V) | ssSkP345(U) ) ).
fof(clause276,conjecture,! [U] : ! [V] : ( ~ ssSkP238(U,V) | ~ ssSkP287(V) | ssSkP286(U) ) ).
fof(clause277,conjecture,! [U] : ! [V] : ( ~ ssSkP238(U,V) | ~ ssSkP286(V) | ssSkP285(U) ) ).
fof(clause278,conjecture,! [U] : ! [V] : ( ~ ssSkP192(U,V) | ~ ssSkP236(V) | ssSkP235(U) ) ).
fof(clause279,conjecture,! [U] : ! [V] : ( ~ ssSkP192(U,V) | ~ ssSkP235(V) | ssSkP234(U) ) ).
fof(clause280,conjecture,! [U] : ! [V] : ( ~ ssSkP150(U,V) | ~ ssSkP190(V) | ssSkP189(U) ) ).
fof(clause281,conjecture,! [U] : ! [V] : ( ~ ssSkP150(U,V) | ~ ssSkP189(V) | ssSkP188(U) ) ).
fof(clause282,conjecture,! [U] : ! [V] : ( ~ ssSkP102(U,V) | ~ ssSkP148(V) | ssSkP147(U) ) ).
fof(clause283,conjecture,! [U] : ! [V] : ( ~ ssSkP102(U,V) | ~ ssSkP147(V) | ssSkP146(U) ) ).
fof(clause284,conjecture,! [U] : ! [V] : ( ~ ssSkP61(U,V) | ~ ssSkP100(V) | ssSkP99(U) ) ).
fof(clause285,conjecture,! [U] : ! [V] : ( ~ ssSkP61(U,V) | ~ ssSkP99(V) | ssSkP98(U) ) ).
fof(clause286,conjecture,! [U] : ! [V] : ( ~ ssSkP1(U,V) | ~ ssSkP59(V) | ssSkP58(U) ) ).
fof(clause287,conjecture,! [U] : ! [V] : ( ~ ssSkP1(U,V) | ~ ssSkP58(V) | ssSkP57(U) ) ).
fof(clause288,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP517(W,V) | ssSkP531(W,U) ) ).
fof(clause289,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP517(W,V) ) ).
fof(clause290,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP456(W,V) | ssSkP457(W,U) ) ).
fof(clause291,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP456(W,V) ) ).
fof(clause292,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP402(W,V) | ssSkP403(W,U) ) ).
fof(clause293,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP402(W,V) ) ).
fof(clause294,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP348(W,V) | ssSkP349(W,U) ) ).
fof(clause295,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP348(W,V) ) ).
fof(clause296,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP288(W,V) | ssSkP289(W,U) ) ).
fof(clause297,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP288(W,V) ) ).
fof(clause298,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP237(W,V) | ssSkP238(W,U) ) ).
fof(clause299,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP237(W,V) ) ).
fof(clause300,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP191(W,V) | ssSkP192(W,U) ) ).
fof(clause301,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP191(W,V) ) ).
fof(clause302,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP149(W,V) | ssSkP150(W,U) ) ).
fof(clause303,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP149(W,V) ) ).
fof(clause304,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP101(W,V) | ssSkP102(W,U) ) ).
fof(clause305,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP101(W,V) ) ).
fof(clause306,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP60(W,V) | ssSkP61(W,U) ) ).
fof(clause307,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP60(W,V) ) ).
fof(clause308,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssSkP0(W,V) | ssSkP1(W,U) ) ).
fof(clause309,conjecture,! [U] : ! [V] : ! [W] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ssSkP0(W,V) ) ).
fof(clause310,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP673(X) | ssSkP672(W) ) ).
fof(clause311,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP671(X) | ssSkP670(W) ) ).
fof(clause312,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP669(X) | ssSkP668(W) ) ).
fof(clause313,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP667(X) | ssSkP666(W) ) ).
fof(clause314,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP665(X) | ssSkP664(W) ) ).
fof(clause315,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP663(X) | ssSkP662(W) ) ).
fof(clause316,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP661(X) | ssSkP660(W) ) ).
fof(clause317,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP659(X) | ssSkP658(W) ) ).
fof(clause318,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP657(X) | ssSkP656(W) ) ).
fof(clause319,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP655(X) | ssSkP654(W) ) ).
fof(clause320,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP653(X) | ssSkP652(W) ) ).
fof(clause321,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP651(X) | ssSkP650(W) ) ).
fof(clause322,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP649(X) | ssSkP648(W) ) ).
fof(clause323,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP647(X) | ssSkP646(W) ) ).
fof(clause324,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP645(X) | ssSkP644(W) ) ).
fof(clause325,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP643(X) | ssSkP642(W) ) ).
fof(clause326,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP641(X) | ssSkP640(W) ) ).
fof(clause327,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP639(X) | ssSkP638(W) ) ).
fof(clause328,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP637(X) | ssSkP636(W) ) ).
fof(clause329,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP635(X) | ssSkP634(W) ) ).
fof(clause330,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP633(X) | ssSkP632(W) ) ).
fof(clause331,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP631(X) | ssSkP630(W) ) ).
fof(clause332,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP629(X) | ssSkP628(W) ) ).
fof(clause333,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP627(X) | ssSkP626(W) ) ).
fof(clause334,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP625(X) | ssSkP624(W) ) ).
fof(clause335,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP623(X) | ssSkP622(W) ) ).
fof(clause336,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP621(X) | ssSkP620(W) ) ).
fof(clause337,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP619(X) | ssSkP618(W) ) ).
fof(clause338,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP617(X) | ssSkP616(W) ) ).
fof(clause339,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP615(X) | ssSkP614(W) ) ).
fof(clause340,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP613(X) | ssSkP612(W) ) ).
fof(clause341,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP611(X) | ssSkP610(W) ) ).
fof(clause342,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP609(X) | ssSkP608(W) ) ).
fof(clause343,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP607(X) | ssSkP606(W) ) ).
fof(clause344,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP605(X) | ssSkP604(W) ) ).
fof(clause345,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP603(X) | ssSkP602(W) ) ).
fof(clause346,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP601(X) | ssSkP600(W) ) ).
fof(clause347,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP599(X) | ssSkP598(W) ) ).
fof(clause348,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP597(X) | ssSkP596(W) ) ).
fof(clause349,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP595(X) | ssSkP594(W) ) ).
fof(clause350,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP593(X) | ssSkP592(W) ) ).
fof(clause351,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP591(X) | ssSkP590(W) ) ).
fof(clause352,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP589(X) | ssSkP588(W) ) ).
fof(clause353,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP587(X) | ssSkP586(W) ) ).
fof(clause354,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP585(X) | ssSkP584(W) ) ).
fof(clause355,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP583(X) | ssSkP582(W) ) ).
fof(clause356,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP581(X) | ssSkP580(W) ) ).
fof(clause357,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP579(X) | ssSkP578(W) ) ).
fof(clause358,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP577(X) | ssSkP576(W) ) ).
fof(clause359,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP575(X) | ssSkP574(W) ) ).
fof(clause360,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP573(X) | ssSkP559(W) ) ).
fof(clause361,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP556(X) | ssSkP516(W) ) ).
fof(clause362,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP513(X) | ssSkP512(W) ) ).
fof(clause363,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP512(X) | ssSkP511(W) ) ).
fof(clause364,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP511(X) | ssSkP510(W) ) ).
fof(clause365,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP510(X) | ssSkP509(W) ) ).
fof(clause366,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP509(X) | ssSkP508(W) ) ).
fof(clause367,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP508(X) | ssSkP507(W) ) ).
fof(clause368,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP507(X) | ssSkP506(W) ) ).
fof(clause369,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP506(X) | ssSkP505(W) ) ).
fof(clause370,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP505(X) | ssSkP504(W) ) ).
fof(clause371,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP504(X) | ssSkP503(W) ) ).
fof(clause372,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP503(X) | ssSkP502(W) ) ).
fof(clause373,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP502(X) | ssSkP501(W) ) ).
fof(clause374,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP501(X) | ssSkP500(W) ) ).
fof(clause375,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP500(X) | ssSkP499(W) ) ).
fof(clause376,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP499(X) | ssSkP498(W) ) ).
fof(clause377,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP498(X) | ssSkP497(W) ) ).
fof(clause378,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP497(X) | ssSkP496(W) ) ).
fof(clause379,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP496(X) | ssSkP495(W) ) ).
fof(clause380,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP495(X) | ssSkP494(W) ) ).
fof(clause381,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP494(X) | ssSkP493(W) ) ).
fof(clause382,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP493(X) | ssSkP492(W) ) ).
fof(clause383,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP492(X) | ssSkP491(W) ) ).
fof(clause384,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP491(X) | ssSkP490(W) ) ).
fof(clause385,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP490(X) | ssSkP489(W) ) ).
fof(clause386,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP489(X) | ssSkP488(W) ) ).
fof(clause387,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP488(X) | ssSkP487(W) ) ).
fof(clause388,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP487(X) | ssSkP486(W) ) ).
fof(clause389,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP485(X) | ssSkP484(W) ) ).
fof(clause390,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP484(X) | ssSkP483(W) ) ).
fof(clause391,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP483(X) | ssSkP482(W) ) ).
fof(clause392,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP482(X) | ssSkP481(W) ) ).
fof(clause393,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP481(X) | ssSkP480(W) ) ).
fof(clause394,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP480(X) | ssSkP479(W) ) ).
fof(clause395,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP478(X) | ssSkP477(W) ) ).
fof(clause396,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP477(X) | ssSkP476(W) ) ).
fof(clause397,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP476(X) | ssSkP475(W) ) ).
fof(clause398,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP475(X) | ssSkP474(W) ) ).
fof(clause399,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP474(X) | ssSkP473(W) ) ).
fof(clause400,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP473(X) | ssSkP472(W) ) ).
fof(clause401,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP472(X) | ssSkP471(W) ) ).
fof(clause402,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP471(X) | ssSkP470(W) ) ).
fof(clause403,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP470(X) | ssSkP469(W) ) ).
fof(clause404,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP469(X) | ssSkP468(W) ) ).
fof(clause405,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP467(X) | ssSkP466(W) ) ).
fof(clause406,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP466(X) | ssSkP465(W) ) ).
fof(clause407,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP465(X) | ssSkP464(W) ) ).
fof(clause408,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP464(X) | ssSkP463(W) ) ).
fof(clause409,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP463(X) | ssSkP462(W) ) ).
fof(clause410,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP462(X) | ssSkP461(W) ) ).
fof(clause411,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP461(X) | ssSkP460(W) ) ).
fof(clause412,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP460(X) | ssSkP459(W) ) ).
fof(clause413,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP459(X) | ssSkP458(W) ) ).
fof(clause414,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP458(X) | ssPv2(W) ) ).
fof(clause415,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP453(X) | ssSkP452(W) ) ).
fof(clause416,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP452(X) | ssSkP451(W) ) ).
fof(clause417,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP451(X) | ssSkP450(W) ) ).
fof(clause418,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP450(X) | ssSkP449(W) ) ).
fof(clause419,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP449(X) | ssSkP448(W) ) ).
fof(clause420,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP448(X) | ssSkP447(W) ) ).
fof(clause421,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP447(X) | ssSkP446(W) ) ).
fof(clause422,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP446(X) | ssSkP445(W) ) ).
fof(clause423,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP445(X) | ssSkP444(W) ) ).
fof(clause424,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP444(X) | ssSkP443(W) ) ).
fof(clause425,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP443(X) | ssSkP442(W) ) ).
fof(clause426,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP442(X) | ssSkP441(W) ) ).
fof(clause427,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP441(X) | ssSkP440(W) ) ).
fof(clause428,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP440(X) | ssSkP439(W) ) ).
fof(clause429,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP439(X) | ssSkP438(W) ) ).
fof(clause430,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP438(X) | ssSkP437(W) ) ).
fof(clause431,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP437(X) | ssSkP436(W) ) ).
fof(clause432,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP436(X) | ssSkP435(W) ) ).
fof(clause433,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP435(X) | ssSkP434(W) ) ).
fof(clause434,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP434(X) | ssSkP433(W) ) ).
fof(clause435,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP433(X) | ssSkP432(W) ) ).
fof(clause436,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP432(X) | ssSkP431(W) ) ).
fof(clause437,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP431(X) | ssSkP430(W) ) ).
fof(clause438,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP430(X) | ssSkP429(W) ) ).
fof(clause439,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP429(X) | ssSkP428(W) ) ).
fof(clause440,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP428(X) | ssSkP427(W) ) ).
fof(clause441,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP427(X) | ssSkP426(W) ) ).
fof(clause442,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP425(X) | ssSkP424(W) ) ).
fof(clause443,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP424(X) | ssSkP423(W) ) ).
fof(clause444,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP423(X) | ssSkP422(W) ) ).
fof(clause445,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP422(X) | ssSkP421(W) ) ).
fof(clause446,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP421(X) | ssSkP420(W) ) ).
fof(clause447,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP420(X) | ssSkP419(W) ) ).
fof(clause448,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP419(X) | ssSkP418(W) ) ).
fof(clause449,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP418(X) | ssSkP417(W) ) ).
fof(clause450,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP416(X) | ssSkP415(W) ) ).
fof(clause451,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP415(X) | ssSkP414(W) ) ).
fof(clause452,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP414(X) | ssSkP413(W) ) ).
fof(clause453,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP413(X) | ssSkP412(W) ) ).
fof(clause454,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP412(X) | ssSkP411(W) ) ).
fof(clause455,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP411(X) | ssSkP410(W) ) ).
fof(clause456,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP410(X) | ssSkP409(W) ) ).
fof(clause457,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP409(X) | ssSkP408(W) ) ).
fof(clause458,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP408(X) | ssSkP407(W) ) ).
fof(clause459,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP407(X) | ssSkP406(W) ) ).
fof(clause460,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP406(X) | ssSkP405(W) ) ).
fof(clause461,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP399(X) | ssSkP398(W) ) ).
fof(clause462,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP398(X) | ssSkP397(W) ) ).
fof(clause463,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP397(X) | ssSkP396(W) ) ).
fof(clause464,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP396(X) | ssSkP395(W) ) ).
fof(clause465,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP395(X) | ssSkP394(W) ) ).
fof(clause466,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP394(X) | ssSkP393(W) ) ).
fof(clause467,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP393(X) | ssSkP392(W) ) ).
fof(clause468,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP392(X) | ssSkP391(W) ) ).
fof(clause469,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP391(X) | ssSkP390(W) ) ).
fof(clause470,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP390(X) | ssSkP389(W) ) ).
fof(clause471,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP389(X) | ssSkP388(W) ) ).
fof(clause472,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP388(X) | ssSkP387(W) ) ).
fof(clause473,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP387(X) | ssSkP386(W) ) ).
fof(clause474,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP386(X) | ssSkP385(W) ) ).
fof(clause475,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP385(X) | ssSkP384(W) ) ).
fof(clause476,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP384(X) | ssSkP383(W) ) ).
fof(clause477,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP383(X) | ssSkP382(W) ) ).
fof(clause478,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP382(X) | ssSkP381(W) ) ).
fof(clause479,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP381(X) | ssSkP380(W) ) ).
fof(clause480,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP380(X) | ssSkP379(W) ) ).
fof(clause481,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP379(X) | ssSkP378(W) ) ).
fof(clause482,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP377(X) | ssSkP376(W) ) ).
fof(clause483,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP376(X) | ssSkP375(W) ) ).
fof(clause484,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP375(X) | ssSkP374(W) ) ).
fof(clause485,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP374(X) | ssSkP373(W) ) ).
fof(clause486,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP373(X) | ssSkP372(W) ) ).
fof(clause487,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP371(X) | ssSkP370(W) ) ).
fof(clause488,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP370(X) | ssSkP369(W) ) ).
fof(clause489,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP369(X) | ssSkP368(W) ) ).
fof(clause490,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP368(X) | ssSkP367(W) ) ).
fof(clause491,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP367(X) | ssSkP366(W) ) ).
fof(clause492,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP366(X) | ssSkP365(W) ) ).
fof(clause493,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP365(X) | ssSkP364(W) ) ).
fof(clause494,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP364(X) | ssSkP363(W) ) ).
fof(clause495,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP363(X) | ssSkP362(W) ) ).
fof(clause496,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP362(X) | ssSkP361(W) ) ).
fof(clause497,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP361(X) | ssSkP360(W) ) ).
fof(clause498,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP360(X) | ssSkP359(W) ) ).
fof(clause499,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP359(X) | ssSkP358(W) ) ).
fof(clause500,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP357(X) | ssSkP356(W) ) ).
fof(clause501,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP356(X) | ssSkP355(W) ) ).
fof(clause502,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP355(X) | ssSkP354(W) ) ).
fof(clause503,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP354(X) | ssSkP353(W) ) ).
fof(clause504,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP353(X) | ssSkP352(W) ) ).
fof(clause505,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP352(X) | ssSkP351(W) ) ).
fof(clause506,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP351(X) | ssSkP350(W) ) ).
fof(clause507,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP345(X) | ssSkP344(W) ) ).
fof(clause508,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP344(X) | ssSkP343(W) ) ).
fof(clause509,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP343(X) | ssSkP342(W) ) ).
fof(clause510,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP342(X) | ssSkP341(W) ) ).
fof(clause511,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP341(X) | ssSkP340(W) ) ).
fof(clause512,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP340(X) | ssSkP339(W) ) ).
fof(clause513,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP339(X) | ssSkP338(W) ) ).
fof(clause514,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP338(X) | ssSkP337(W) ) ).
fof(clause515,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP337(X) | ssSkP336(W) ) ).
fof(clause516,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP336(X) | ssSkP335(W) ) ).
fof(clause517,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP335(X) | ssSkP334(W) ) ).
fof(clause518,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP334(X) | ssSkP333(W) ) ).
fof(clause519,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP333(X) | ssSkP332(W) ) ).
fof(clause520,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP332(X) | ssSkP331(W) ) ).
fof(clause521,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP331(X) | ssSkP330(W) ) ).
fof(clause522,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP330(X) | ssSkP329(W) ) ).
fof(clause523,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP328(X) | ssSkP327(W) ) ).
fof(clause524,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP327(X) | ssSkP326(W) ) ).
fof(clause525,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP326(X) | ssSkP325(W) ) ).
fof(clause526,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP325(X) | ssSkP324(W) ) ).
fof(clause527,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP324(X) | ssSkP323(W) ) ).
fof(clause528,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP323(X) | ssSkP322(W) ) ).
fof(clause529,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP322(X) | ssSkP321(W) ) ).
fof(clause530,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP321(X) | ssSkP320(W) ) ).
fof(clause531,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP320(X) | ssSkP319(W) ) ).
fof(clause532,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP318(X) | ssSkP317(W) ) ).
fof(clause533,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP317(X) | ssSkP316(W) ) ).
fof(clause534,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP315(X) | ssSkP314(W) ) ).
fof(clause535,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP314(X) | ssSkP313(W) ) ).
fof(clause536,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP313(X) | ssSkP312(W) ) ).
fof(clause537,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP312(X) | ssSkP311(W) ) ).
fof(clause538,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP311(X) | ssSkP310(W) ) ).
fof(clause539,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP310(X) | ssSkP309(W) ) ).
fof(clause540,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP309(X) | ssSkP308(W) ) ).
fof(clause541,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP308(X) | ssSkP307(W) ) ).
fof(clause542,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP307(X) | ssSkP306(W) ) ).
fof(clause543,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP306(X) | ssSkP305(W) ) ).
fof(clause544,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP305(X) | ssSkP304(W) ) ).
fof(clause545,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP304(X) | ssSkP303(W) ) ).
fof(clause546,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP303(X) | ssSkP302(W) ) ).
fof(clause547,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP302(X) | ssSkP301(W) ) ).
fof(clause548,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP301(X) | ssSkP300(W) ) ).
fof(clause549,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP300(X) | ssSkP299(W) ) ).
fof(clause550,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP299(X) | ssSkP298(W) ) ).
fof(clause551,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP298(X) | ssSkP297(W) ) ).
fof(clause552,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP297(X) | ssSkP296(W) ) ).
fof(clause553,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP296(X) | ssSkP295(W) ) ).
fof(clause554,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP295(X) | ssSkP294(W) ) ).
fof(clause555,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP294(X) | ssSkP293(W) ) ).
fof(clause556,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP293(X) | ssSkP292(W) ) ).
fof(clause557,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP292(X) | ssSkP291(W) ) ).
fof(clause558,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP291(X) | ssSkP290(W) ) ).
fof(clause559,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP285(X) | ssSkP284(W) ) ).
fof(clause560,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP284(X) | ssSkP283(W) ) ).
fof(clause561,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP283(X) | ssSkP282(W) ) ).
fof(clause562,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP282(X) | ssSkP281(W) ) ).
fof(clause563,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP281(X) | ssSkP280(W) ) ).
fof(clause564,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP280(X) | ssSkP279(W) ) ).
fof(clause565,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP279(X) | ssSkP278(W) ) ).
fof(clause566,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP278(X) | ssSkP277(W) ) ).
fof(clause567,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP277(X) | ssSkP276(W) ) ).
fof(clause568,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP276(X) | ssSkP275(W) ) ).
fof(clause569,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP275(X) | ssSkP274(W) ) ).
fof(clause570,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP274(X) | ssSkP273(W) ) ).
fof(clause571,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP273(X) | ssSkP272(W) ) ).
fof(clause572,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP272(X) | ssSkP271(W) ) ).
fof(clause573,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP270(X) | ssSkP269(W) ) ).
fof(clause574,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP269(X) | ssSkP268(W) ) ).
fof(clause575,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP267(X) | ssSkP266(W) ) ).
fof(clause576,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP266(X) | ssSkP265(W) ) ).
fof(clause577,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP265(X) | ssSkP264(W) ) ).
fof(clause578,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP264(X) | ssSkP263(W) ) ).
fof(clause579,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP263(X) | ssSkP262(W) ) ).
fof(clause580,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP262(X) | ssSkP261(W) ) ).
fof(clause581,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP261(X) | ssSkP260(W) ) ).
fof(clause582,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP260(X) | ssSkP259(W) ) ).
fof(clause583,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP259(X) | ssSkP258(W) ) ).
fof(clause584,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP258(X) | ssSkP257(W) ) ).
fof(clause585,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP257(X) | ssSkP256(W) ) ).
fof(clause586,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP256(X) | ssSkP255(W) ) ).
fof(clause587,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP255(X) | ssSkP254(W) ) ).
fof(clause588,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP254(X) | ssSkP253(W) ) ).
fof(clause589,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP253(X) | ssSkP252(W) ) ).
fof(clause590,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP251(X) | ssSkP250(W) ) ).
fof(clause591,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP250(X) | ssSkP249(W) ) ).
fof(clause592,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP249(X) | ssSkP248(W) ) ).
fof(clause593,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP248(X) | ssSkP247(W) ) ).
fof(clause594,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP247(X) | ssSkP246(W) ) ).
fof(clause595,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP246(X) | ssSkP245(W) ) ).
fof(clause596,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP245(X) | ssSkP244(W) ) ).
fof(clause597,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP244(X) | ssSkP243(W) ) ).
fof(clause598,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP243(X) | ssSkP242(W) ) ).
fof(clause599,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP242(X) | ssSkP241(W) ) ).
fof(clause600,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP241(X) | ssSkP240(W) ) ).
fof(clause601,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP240(X) | ssSkP239(W) ) ).
fof(clause602,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP239(X) | ssPv11(W) ) ).
fof(clause603,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP234(X) | ssSkP233(W) ) ).
fof(clause604,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP233(X) | ssSkP232(W) ) ).
fof(clause605,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP232(X) | ssSkP231(W) ) ).
fof(clause606,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP231(X) | ssSkP230(W) ) ).
fof(clause607,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP230(X) | ssSkP229(W) ) ).
fof(clause608,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP229(X) | ssSkP228(W) ) ).
fof(clause609,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP228(X) | ssSkP227(W) ) ).
fof(clause610,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP227(X) | ssSkP226(W) ) ).
fof(clause611,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP225(X) | ssSkP224(W) ) ).
fof(clause612,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP224(X) | ssSkP223(W) ) ).
fof(clause613,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP223(X) | ssSkP222(W) ) ).
fof(clause614,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP222(X) | ssSkP221(W) ) ).
fof(clause615,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP221(X) | ssSkP220(W) ) ).
fof(clause616,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP220(X) | ssSkP219(W) ) ).
fof(clause617,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP219(X) | ssSkP218(W) ) ).
fof(clause618,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP218(X) | ssSkP217(W) ) ).
fof(clause619,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP217(X) | ssSkP216(W) ) ).
fof(clause620,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP216(X) | ssSkP215(W) ) ).
fof(clause621,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP215(X) | ssSkP214(W) ) ).
fof(clause622,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP214(X) | ssSkP213(W) ) ).
fof(clause623,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP213(X) | ssSkP212(W) ) ).
fof(clause624,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP212(X) | ssSkP211(W) ) ).
fof(clause625,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP211(X) | ssSkP210(W) ) ).
fof(clause626,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP210(X) | ssSkP209(W) ) ).
fof(clause627,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP209(X) | ssSkP208(W) ) ).
fof(clause628,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP208(X) | ssSkP207(W) ) ).
fof(clause629,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP207(X) | ssSkP206(W) ) ).
fof(clause630,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP206(X) | ssSkP205(W) ) ).
fof(clause631,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP205(X) | ssSkP204(W) ) ).
fof(clause632,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP204(X) | ssSkP203(W) ) ).
fof(clause633,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP203(X) | ssSkP202(W) ) ).
fof(clause634,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP202(X) | ssSkP201(W) ) ).
fof(clause635,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP201(X) | ssSkP200(W) ) ).
fof(clause636,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP199(X) | ssSkP198(W) ) ).
fof(clause637,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP198(X) | ssSkP197(W) ) ).
fof(clause638,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP197(X) | ssSkP196(W) ) ).
fof(clause639,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP196(X) | ssSkP195(W) ) ).
fof(clause640,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP195(X) | ssSkP194(W) ) ).
fof(clause641,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP193(X) | ssPv16(W) ) ).
fof(clause642,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP188(X) | ssSkP187(W) ) ).
fof(clause643,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP187(X) | ssSkP186(W) ) ).
fof(clause644,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP186(X) | ssSkP185(W) ) ).
fof(clause645,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP185(X) | ssSkP184(W) ) ).
fof(clause646,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP184(X) | ssSkP183(W) ) ).
fof(clause647,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP183(X) | ssSkP182(W) ) ).
fof(clause648,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP182(X) | ssSkP181(W) ) ).
fof(clause649,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP180(X) | ssSkP179(W) ) ).
fof(clause650,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP179(X) | ssSkP178(W) ) ).
fof(clause651,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP177(X) | ssSkP176(W) ) ).
fof(clause652,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP176(X) | ssSkP175(W) ) ).
fof(clause653,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP175(X) | ssSkP174(W) ) ).
fof(clause654,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP174(X) | ssSkP173(W) ) ).
fof(clause655,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP173(X) | ssSkP172(W) ) ).
fof(clause656,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP172(X) | ssSkP171(W) ) ).
fof(clause657,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP171(X) | ssSkP170(W) ) ).
fof(clause658,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP170(X) | ssSkP169(W) ) ).
fof(clause659,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP169(X) | ssSkP168(W) ) ).
fof(clause660,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP168(X) | ssSkP167(W) ) ).
fof(clause661,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP166(X) | ssSkP165(W) ) ).
fof(clause662,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP165(X) | ssSkP164(W) ) ).
fof(clause663,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP164(X) | ssSkP163(W) ) ).
fof(clause664,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP163(X) | ssSkP162(W) ) ).
fof(clause665,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP162(X) | ssSkP161(W) ) ).
fof(clause666,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP161(X) | ssSkP160(W) ) ).
fof(clause667,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP160(X) | ssSkP159(W) ) ).
fof(clause668,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP159(X) | ssSkP158(W) ) ).
fof(clause669,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP158(X) | ssSkP157(W) ) ).
fof(clause670,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP157(X) | ssSkP156(W) ) ).
fof(clause671,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP156(X) | ssSkP155(W) ) ).
fof(clause672,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP155(X) | ssSkP154(W) ) ).
fof(clause673,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP154(X) | ssSkP153(W) ) ).
fof(clause674,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP153(X) | ssSkP152(W) ) ).
fof(clause675,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP152(X) | ssSkP151(W) ) ).
fof(clause676,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP151(X) | ssPv20(W) ) ).
fof(clause677,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP146(X) | ssSkP145(W) ) ).
fof(clause678,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP145(X) | ssSkP144(W) ) ).
fof(clause679,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP144(X) | ssSkP143(W) ) ).
fof(clause680,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP143(X) | ssSkP142(W) ) ).
fof(clause681,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP142(X) | ssSkP141(W) ) ).
fof(clause682,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP140(X) | ssSkP139(W) ) ).
fof(clause683,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP139(X) | ssSkP138(W) ) ).
fof(clause684,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP138(X) | ssSkP137(W) ) ).
fof(clause685,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP137(X) | ssSkP136(W) ) ).
fof(clause686,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP136(X) | ssSkP135(W) ) ).
fof(clause687,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP135(X) | ssSkP134(W) ) ).
fof(clause688,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP134(X) | ssSkP133(W) ) ).
fof(clause689,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP133(X) | ssSkP132(W) ) ).
fof(clause690,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP132(X) | ssSkP131(W) ) ).
fof(clause691,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP131(X) | ssSkP130(W) ) ).
fof(clause692,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP130(X) | ssSkP129(W) ) ).
fof(clause693,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP129(X) | ssSkP128(W) ) ).
fof(clause694,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP128(X) | ssSkP127(W) ) ).
fof(clause695,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP127(X) | ssSkP126(W) ) ).
fof(clause696,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP125(X) | ssSkP124(W) ) ).
fof(clause697,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP124(X) | ssSkP123(W) ) ).
fof(clause698,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP123(X) | ssSkP122(W) ) ).
fof(clause699,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP122(X) | ssSkP121(W) ) ).
fof(clause700,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP121(X) | ssSkP120(W) ) ).
fof(clause701,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP120(X) | ssSkP119(W) ) ).
fof(clause702,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP118(X) | ssSkP117(W) ) ).
fof(clause703,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP117(X) | ssSkP116(W) ) ).
fof(clause704,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP116(X) | ssSkP115(W) ) ).
fof(clause705,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP115(X) | ssSkP114(W) ) ).
fof(clause706,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP114(X) | ssSkP113(W) ) ).
fof(clause707,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP113(X) | ssSkP112(W) ) ).
fof(clause708,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP112(X) | ssSkP111(W) ) ).
fof(clause709,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP111(X) | ssSkP110(W) ) ).
fof(clause710,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP110(X) | ssSkP109(W) ) ).
fof(clause711,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP109(X) | ssSkP108(W) ) ).
fof(clause712,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP108(X) | ssSkP107(W) ) ).
fof(clause713,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP107(X) | ssSkP106(W) ) ).
fof(clause714,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP106(X) | ssSkP105(W) ) ).
fof(clause715,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP105(X) | ssSkP104(W) ) ).
fof(clause716,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP104(X) | ssSkP103(W) ) ).
fof(clause717,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP98(X) | ssSkP97(W) ) ).
fof(clause718,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP97(X) | ssSkP96(W) ) ).
fof(clause719,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP96(X) | ssSkP95(W) ) ).
fof(clause720,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP94(X) | ssSkP93(W) ) ).
fof(clause721,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP93(X) | ssSkP92(W) ) ).
fof(clause722,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP92(X) | ssSkP91(W) ) ).
fof(clause723,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP91(X) | ssSkP90(W) ) ).
fof(clause724,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP90(X) | ssSkP89(W) ) ).
fof(clause725,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP89(X) | ssSkP88(W) ) ).
fof(clause726,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP88(X) | ssSkP87(W) ) ).
fof(clause727,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP87(X) | ssSkP86(W) ) ).
fof(clause728,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP86(X) | ssSkP85(W) ) ).
fof(clause729,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP85(X) | ssSkP84(W) ) ).
fof(clause730,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP84(X) | ssSkP83(W) ) ).
fof(clause731,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP82(X) | ssSkP81(W) ) ).
fof(clause732,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP81(X) | ssSkP80(W) ) ).
fof(clause733,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP80(X) | ssSkP79(W) ) ).
fof(clause734,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP79(X) | ssSkP78(W) ) ).
fof(clause735,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP78(X) | ssSkP77(W) ) ).
fof(clause736,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP77(X) | ssSkP76(W) ) ).
fof(clause737,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP76(X) | ssSkP75(W) ) ).
fof(clause738,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP75(X) | ssSkP74(W) ) ).
fof(clause739,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP74(X) | ssSkP73(W) ) ).
fof(clause740,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP73(X) | ssSkP72(W) ) ).
fof(clause741,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP72(X) | ssSkP71(W) ) ).
fof(clause742,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP71(X) | ssSkP70(W) ) ).
fof(clause743,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP70(X) | ssSkP69(W) ) ).
fof(clause744,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP68(X) | ssSkP67(W) ) ).
fof(clause745,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP67(X) | ssSkP66(W) ) ).
fof(clause746,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP66(X) | ssSkP65(W) ) ).
fof(clause747,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP65(X) | ssSkP64(W) ) ).
fof(clause748,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP64(X) | ssSkP63(W) ) ).
fof(clause749,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP63(X) | ssSkP62(W) ) ).
fof(clause750,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP57(X) | ssSkP56(W) ) ).
fof(clause751,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP56(X) | ssSkP55(W) ) ).
fof(clause752,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP54(X) | ssSkP53(W) ) ).
fof(clause753,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP53(X) | ssSkP52(W) ) ).
fof(clause754,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP52(X) | ssSkP51(W) ) ).
fof(clause755,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP51(X) | ssSkP50(W) ) ).
fof(clause756,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP50(X) | ssSkP49(W) ) ).
fof(clause757,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP48(X) | ssSkP47(W) ) ).
fof(clause758,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP47(X) | ssSkP46(W) ) ).
fof(clause759,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP46(X) | ssSkP45(W) ) ).
fof(clause760,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP45(X) | ssSkP44(W) ) ).
fof(clause761,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP44(X) | ssSkP43(W) ) ).
fof(clause762,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP43(X) | ssSkP42(W) ) ).
fof(clause763,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP42(X) | ssSkP41(W) ) ).
fof(clause764,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP41(X) | ssSkP40(W) ) ).
fof(clause765,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP40(X) | ssSkP39(W) ) ).
fof(clause766,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP39(X) | ssSkP38(W) ) ).
fof(clause767,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP38(X) | ssSkP37(W) ) ).
fof(clause768,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP37(X) | ssSkP36(W) ) ).
fof(clause769,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP36(X) | ssSkP35(W) ) ).
fof(clause770,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP35(X) | ssSkP34(W) ) ).
fof(clause771,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP34(X) | ssSkP33(W) ) ).
fof(clause772,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP33(X) | ssSkP32(W) ) ).
fof(clause773,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP32(X) | ssSkP31(W) ) ).
fof(clause774,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP31(X) | ssSkP30(W) ) ).
fof(clause775,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP30(X) | ssSkP29(W) ) ).
fof(clause776,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP29(X) | ssSkP28(W) ) ).
fof(clause777,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP28(X) | ssSkP27(W) ) ).
fof(clause778,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP27(X) | ssSkP26(W) ) ).
fof(clause779,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP26(X) | ssSkP25(W) ) ).
fof(clause780,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP24(X) | ssSkP23(W) ) ).
fof(clause781,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP23(X) | ssSkP22(W) ) ).
fof(clause782,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP22(X) | ssSkP21(W) ) ).
fof(clause783,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP21(X) | ssSkP20(W) ) ).
fof(clause784,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP20(X) | ssSkP19(W) ) ).
fof(clause785,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP19(X) | ssSkP18(W) ) ).
fof(clause786,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP18(X) | ssSkP17(W) ) ).
fof(clause787,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP17(X) | ssSkP16(W) ) ).
fof(clause788,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP16(X) | ssSkP15(W) ) ).
fof(clause789,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP15(X) | ssSkP14(W) ) ).
fof(clause790,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP14(X) | ssSkP13(W) ) ).
fof(clause791,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP13(X) | ssSkP12(W) ) ).
fof(clause792,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP12(X) | ssSkP11(W) ) ).
fof(clause793,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP11(X) | ssSkP10(W) ) ).
fof(clause794,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP10(X) | ssSkP9(W) ) ).
fof(clause795,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP9(X) | ssSkP8(W) ) ).
fof(clause796,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP8(X) | ssSkP7(W) ) ).
fof(clause797,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP7(X) | ssSkP6(W) ) ).
fof(clause798,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP6(X) | ssSkP5(W) ) ).
fof(clause799,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP5(X) | ssSkP4(W) ) ).
fof(clause800,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP4(X) | ssSkP3(W) ) ).
fof(clause801,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP3(X) | ssSkP2(W) ) ).
fof(clause802,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssSkP2(X) | ssPv2(W) ) ).
fof(clause803,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssPv8(W) | ~ ssSkP404(X) ) ).
fof(clause804,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssPv8(W) | ~ ssSkP350(X) ) ).
fof(clause805,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssPv2(W) | ~ ssSkP290(X) ) ).
fof(clause806,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssPv14(W) | ~ ssSkP103(X) ) ).
fof(clause807,conjecture,! [U] : ! [V] : ! [W] : ! [X] : ( ~ ssRr(U,V) | ~ ssRr(U,W) | ~ ssRr(X,V) | ~ ssPv21(W) | ~ ssSkP62(X) ) ).
