%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYN890-1 : TPTP v7.5.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n017.cluster.edu---x86_64 x86_64--- ------Linux 3.10.0-693.el7.x86_64 % Model : Unavailable % CPU : Unavailable % Memory : Unavailable % OS : Unavailable % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Mar 28 15:04:29 EDT 2022 % Result : Unsatisfiable 7.50s 7.59s % Output : CNFRefutation 7.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN890-1 : TPTP v7.5.0. Released v2.5.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % RAMPerCPU : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Mar 10 10:44:36 EST 2022 % 0.12/0.33 % CPUTime : % 0.19/0.44 openjdk version "1.8.0_171" % 0.19/0.44 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.19/0.44 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.19/0.44 file=/export/starexec/sandbox/benchmark/theBenchmark.p % 0.59/0.67 start to proof:theBenchmark % 7.50/7.59 % Version : CSE-F---1.0 % 7.50/7.59 % Problem : theBenchmark.p % 7.50/7.59 % Proof found % 7.50/7.59 % SZS status Theorem for theBenchmark.p % 7.50/7.59 % SZS output start Proof % 7.50/7.59 [1]P1(a5000) % 7.50/7.59 [2]P2(x21)+~P1(a5000) % 7.50/7.59 [3]~P2(x31)+P13(x31,x32)+~P1(a5000) % 7.50/7.59 [4]~P2(x41)+~P13(x41,x42)+P14(x41,x42,x43)+~P1(a5000) % 7.50/7.59 [5]~P2(x51)+~P13(x51,x52)+~P14(x51,x52,x53)+P15(x51,x52,x53,x54)+~P1(a5000) % 7.50/7.59 [6]~P2(x61)+~P13(x61,x62)+~P14(x61,x62,x63)+P16(x61,x62,x63,x64,a1)+~P1(a5000) % 7.50/7.59 [8]~P2(x81)+~P13(x81,x82)+~P14(x81,x82,x83)+~P16(x81,x82,x83,x84,a16)+~P1(a5000) % 7.50/7.59 [7]~P2(x71)+~P13(x71,x72)+~P14(x71,x72,x73)+~P15(x71,x72,x73,x74)+P17(x71,x72,x73,x74,x75)+~P1(a5000) % 7.50/7.59 [9]~P2(x91)+~P13(x91,x92)+~P14(x91,x92,x93)+~P15(x91,x92,x93,x94)+P18(x91,x92,x93,x94,x95,a2)+~P1(a5000) % 7.50/7.59 [11]~P2(x111)+~P13(x111,x112)+~P14(x111,x112,x113)+~P15(x111,x112,x113,x114)+~P18(x111,x112,x113,x114,x115,a15)+~P1(a5000) % 7.50/7.59 [10]~P2(x101)+~P13(x101,x102)+~P14(x101,x102,x103)+~P15(x101,x102,x103,x104)+~P17(x101,x102,x103,x104,x105)+P19(x101,x102,x103,x104,x105,x106)+~P1(a5000) % 7.50/7.59 [12]~P2(x121)+~P13(x121,x122)+~P14(x121,x122,x123)+~P15(x121,x122,x123,x124)+~P17(x121,x122,x123,x124,x125)+P20(x121,x122,x123,x124,x125,x126,a3)+~P1(a5000) % 7.50/7.59 [14]~P2(x141)+~P13(x141,x142)+~P14(x141,x142,x143)+~P15(x141,x142,x143,x144)+~P17(x141,x142,x143,x144,x145)+~P20(x141,x142,x143,x144,x145,x146,a14)+~P1(a5000) % 7.50/7.59 [13]~P2(x131)+~P13(x131,x132)+~P14(x131,x132,x133)+~P15(x131,x132,x133,x134)+~P17(x131,x132,x133,x134,x135)+~P19(x131,x132,x133,x134,x135,x136)+P21(x131,x132,x133,x134,x135,x136,x137)+~P1(a5000) % 7.50/7.59 [16]~P2(x161)+~P13(x161,x162)+~P14(x161,x162,x163)+~P15(x161,x162,x163,x164)+~P17(x161,x162,x163,x164,x165)+~P19(x161,x162,x163,x164,x165,x166)+P22(x161,x162,x163,x164,x165,x166,x167,a4)+~P1(a5000) % 7.50/7.59 [18]~P2(x181)+~P13(x181,x182)+~P14(x181,x182,x183)+~P15(x181,x182,x183,x184)+~P17(x181,x182,x183,x184,x185)+~P19(x181,x182,x183,x184,x185,x186)+~P22(x181,x182,x183,x184,x185,x186,x187,a13)+~P1(a5000) % 7.50/7.59 [17]~P2(x171)+~P13(x171,x172)+~P14(x171,x172,x173)+~P15(x171,x172,x173,x174)+~P17(x171,x172,x173,x174,x175)+~P19(x171,x172,x173,x174,x175,x176)+~P21(x171,x172,x173,x174,x175,x176,x177)+P23(x171,x172,x173,x174,x175,x176,x177,x178)+~P1(a5000) % 7.50/7.59 [20]~P2(x201)+~P13(x201,x202)+~P14(x201,x202,x203)+~P15(x201,x202,x203,x204)+~P17(x201,x202,x203,x204,x205)+~P19(x201,x202,x203,x204,x205,x206)+~P21(x201,x202,x203,x204,x205,x206,x207)+~P23(x201,x202,x203,x204,x205,x206,x207,x208)+P24(x201,x202,x203,x204,x205,x206,x207,x208,x209)+~P1(a5000) % 7.50/7.59 [15]~P2(x151)+~P13(x151,x152)+~P29(x151,x152)+~P14(x151,x152,x153)+~P15(x151,x152,x153,x154)+~P17(x151,x152,x153,x154,x155)+P28(x151,x152,x153,x154)+P16(x151,x152,x153,x154,x155)+~P19(x151,x152,x153,x154,x155,x156)+~P20(x151,x152,x153,x154,x155,x156,x157)+~P1(a5000) % 7.50/7.59 [23]~P2(x231)+~P13(x231,x232)+~P14(x231,x232,x233)+~P15(x231,x232,x233,x234)+~P17(x231,x232,x233,x234,x235)+~P19(x231,x232,x233,x234,x235,x236)+~P21(x231,x232,x233,x234,x235,x236,x237)+~P23(x231,x232,x233,x234,x235,x236,x237,x238)+~P24(x231,x232,x233,x234,x235,x236,x237,x238,x239)+P3(x231,x232,x233,x234,x235,x236,x237,x238,x239,x2310)+~P1(a5000) % 7.50/7.59 [19]~P2(x191)+~P13(x191,x192)+~P14(x191,x192,x193)+~P15(x191,x192,x193,x194)+~P17(x191,x192,x193,x194,x195)+P31(x191)+P29(x191,x192)+P16(x191,x192,x193,x194,x195)+~P19(x191,x192,x193,x194,x195,x196)+~P21(x191,x192,x193,x194,x195,x196,x197)+~P22(x191,x192,x193,x194,x195,x196,x197,x198)+~P1(a5000) % 7.50/7.59 [26]~P2(x261)+~P13(x261,x262)+~P14(x261,x262,x263)+~P15(x261,x262,x263,x264)+~P17(x261,x262,x263,x264,x265)+~P19(x261,x262,x263,x264,x265,x266)+~P21(x261,x262,x263,x264,x265,x266,x267)+~P23(x261,x262,x263,x264,x265,x266,x267,x268)+~P24(x261,x262,x263,x264,x265,x266,x267,x268,x269)+~P3(x261,x262,x263,x264,x265,x266,x267,x268,x269,x2610)+P4(x261,x262,x263,x264,x265,x266,x267,x268,x269,x2610,x2611)+~P1(a5000) % 7.50/7.59 [21]~P2(x211)+~P13(x211,x212)+~P14(x211,x212,x213)+~P15(x211,x212,x213,x214)+~P16(x211,x212,x213,x214,x215)+~P17(x211,x212,x213,x214,x215)+~P19(x211,x212,x213,x214,x215,x216)+~P21(x211,x212,x213,x214,x215,x216,x217)+~P23(x211,x212,x213,x214,x215,x216,x217,x218)+P28(x211,x212,x213,x214)+P18(x211,x212,x213,x214,x215,x216)+P25(x211,x212,x213,x214,x215,x216,x217,x218,x219)+~P1(a5000) % 7.50/7.59 [22]~P31(x221)+~P17(x221,x222,x223,x224,x225)+~P19(x221,x222,x223,x224,x225,x226)+~P2(x221)+~P13(x221,x222)+~P14(x221,x222,x223)+~P15(x221,x222,x223,x224)+~P16(x221,x222,x223,x224,x225)+~P18(x221,x222,x223,x224,x225,x226)+~P21(x221,x222,x223,x224,x225,x226,x227)+~P23(x221,x222,x223,x224,x225,x226,x227,x228)+~P25(x221,x222,x223,x224,x225,x226,x227,x228,x229)+~P1(a5000) % 7.50/7.59 [28]~P2(x281)+~P13(x281,x282)+~P14(x281,x282,x283)+~P15(x281,x282,x283,x284)+~P17(x281,x282,x283,x284,x285)+~P19(x281,x282,x283,x284,x285,x286)+~P21(x281,x282,x283,x284,x285,x286,x287)+~P23(x281,x282,x283,x284,x285,x286,x287,x288)+~P24(x281,x282,x283,x284,x285,x286,x287,x288,x289)+~P3(x281,x282,x283,x284,x285,x286,x287,x288,x289,x2810)+~P4(x281,x282,x283,x284,x285,x286,x287,x288,x289,x2810,x2811)+P5(x281,x282,x283,x284,x285,x286,x287,x288,x289,x2810,x2811,x2812)+~P1(a5000) % 7.50/7.60 [31]~P2(x311)+~P13(x311,x312)+~P14(x311,x312,x313)+~P15(x311,x312,x313,x314)+~P17(x311,x312,x313,x314,x315)+~P19(x311,x312,x313,x314,x315,x316)+~P21(x311,x312,x313,x314,x315,x316,x317)+~P23(x311,x312,x313,x314,x315,x316,x317,x318)+~P24(x311,x312,x313,x314,x315,x316,x317,x318,x319)+~P3(x311,x312,x313,x314,x315,x316,x317,x318,x319,x3110)+~P4(x311,x312,x313,x314,x315,x316,x317,x318,x319,x3110,x3111)+P34(x311,x312,x313,x314,x315,x316,x317,x318,x319,x3110,x3111,x3112,a5)+~P1(a5000) % 7.50/7.60 [34]~P2(x341)+~P13(x341,x342)+~P14(x341,x342,x343)+~P15(x341,x342,x343,x344)+~P17(x341,x342,x343,x344,x345)+~P19(x341,x342,x343,x344,x345,x346)+~P21(x341,x342,x343,x344,x345,x346,x347)+~P23(x341,x342,x343,x344,x345,x346,x347,x348)+~P24(x341,x342,x343,x344,x345,x346,x347,x348,x349)+~P3(x341,x342,x343,x344,x345,x346,x347,x348,x349,x3410)+~P4(x341,x342,x343,x344,x345,x346,x347,x348,x349,x3410,x3411)+~P34(x341,x342,x343,x344,x345,x346,x347,x348,x349,x3410,x3411,x3412,a12)+~P1(a5000) % 7.50/7.60 [24]~P2(x241)+~P31(x241)+~P13(x241,x242)+~P14(x241,x242,x243)+~P15(x241,x242,x243,x244)+~P17(x241,x242,x243,x244,x245)+~P19(x241,x242,x243,x244,x245,x246)+~P21(x241,x242,x243,x244,x245,x246,x247)+P18(x241,x242,x243,x244,x245,x246)+P20(x241,x242,x243,x244,x245,x246,x247)+~P23(x241,x242,x243,x244,x245,x246,x247,x248)+~P24(x241,x242,x243,x244,x245,x246,x247,x248,x249)+~P26(x241,x242,x243,x244,x245,x246,x247,x248,x249,x2410)+~P1(a5000) % 7.50/7.60 [25]~P2(x251)+~P13(x251,x252)+~P14(x251,x252,x253)+~P15(x251,x252,x253,x254)+~P17(x251,x252,x253,x254,x255)+~P23(x251,x252,x253,x254,x255,x256,x257,x258)+P30(x251,x252,x253)+P16(x251,x252,x253,x254,x255)+~P19(x251,x252,x253,x254,x255,x256)+~P21(x251,x252,x253,x254,x255,x256,x257)+~P22(x251,x252,x253,x254,x255,x256,x257,x258)+~P24(x251,x252,x253,x254,x255,x256,x257,x258,x259)+~P26(x251,x252,x253,x254,x255,x256,x257,x258,x259,x2510)+~P1(a5000) % 7.50/7.60 [32]~P2(x321)+~P13(x321,x322)+~P14(x321,x322,x323)+~P15(x321,x322,x323,x324)+~P17(x321,x322,x323,x324,x325)+~P19(x321,x322,x323,x324,x325,x326)+~P21(x321,x322,x323,x324,x325,x326,x327)+~P23(x321,x322,x323,x324,x325,x326,x327,x328)+~P24(x321,x322,x323,x324,x325,x326,x327,x328,x329)+~P3(x321,x322,x323,x324,x325,x326,x327,x328,x329,x3210)+~P4(x321,x322,x323,x324,x325,x326,x327,x328,x329,x3210,x3211)+~P5(x321,x322,x323,x324,x325,x326,x327,x328,x329,x3210,x3211,x3212)+P6(x321,x322,x323,x324,x325,x326,x327,x328,x329,x3210,x3211,x3212,x3213)+~P1(a5000) % 7.50/7.60 [38]~P2(x381)+~P13(x381,x382)+~P14(x381,x382,x383)+~P15(x381,x382,x383,x384)+~P17(x381,x382,x383,x384,x385)+~P19(x381,x382,x383,x384,x385,x386)+~P21(x381,x382,x383,x384,x385,x386,x387)+~P23(x381,x382,x383,x384,x385,x386,x387,x388)+~P24(x381,x382,x383,x384,x385,x386,x387,x388,x389)+~P3(x381,x382,x383,x384,x385,x386,x387,x388,x389,x3810)+~P4(x381,x382,x383,x384,x385,x386,x387,x388,x389,x3810,x3811)+~P5(x381,x382,x383,x384,x385,x386,x387,x388,x389,x3810,x3811,x3812)+P35(x381,x382,x383,x384,x385,x386,x387,x388,x389,x3810,x3811,x3812,x3813,a6)+~P1(a5000) % 7.50/7.60 [40]~P2(x401)+~P13(x401,x402)+~P14(x401,x402,x403)+~P15(x401,x402,x403,x404)+~P17(x401,x402,x403,x404,x405)+~P19(x401,x402,x403,x404,x405,x406)+~P21(x401,x402,x403,x404,x405,x406,x407)+~P23(x401,x402,x403,x404,x405,x406,x407,x408)+~P24(x401,x402,x403,x404,x405,x406,x407,x408,x409)+~P3(x401,x402,x403,x404,x405,x406,x407,x408,x409,x4010)+~P4(x401,x402,x403,x404,x405,x406,x407,x408,x409,x4010,x4011)+~P5(x401,x402,x403,x404,x405,x406,x407,x408,x409,x4010,x4011,x4012)+~P35(x401,x402,x403,x404,x405,x406,x407,x408,x409,x4010,x4011,x4012,x4013,a11)+~P1(a5000) % 7.50/7.60 [27]~P2(x271)+~P31(x271)+~P13(x271,x272)+~P14(x271,x272,x273)+~P15(x271,x272,x273,x274)+~P17(x271,x272,x273,x274,x275)+~P19(x271,x272,x273,x274,x275,x276)+~P21(x271,x272,x273,x274,x275,x276,x277)+~P22(x271,x272,x273,x274,x275,x276,x277,x278)+~P23(x271,x272,x273,x274,x275,x276,x277,x278)+~P24(x271,x272,x273,x274,x275,x276,x277,x278,x279)+~P3(x271,x272,x273,x274,x275,x276,x277,x278,x279,x2710)+P16(x271,x272,x273,x274,x275)+P27(x271,x272,x273,x274,x275,x276,x277,x278,x279,x2710,x2711)+~P1(a5000) % 7.50/7.60 [39]~P2(x391)+~P13(x391,x392)+~P14(x391,x392,x393)+~P15(x391,x392,x393,x394)+~P17(x391,x392,x393,x394,x395)+~P19(x391,x392,x393,x394,x395,x396)+~P21(x391,x392,x393,x394,x395,x396,x397)+~P23(x391,x392,x393,x394,x395,x396,x397,x398)+~P24(x391,x392,x393,x394,x395,x396,x397,x398,x399)+~P3(x391,x392,x393,x394,x395,x396,x397,x398,x399,x3910)+~P4(x391,x392,x393,x394,x395,x396,x397,x398,x399,x3910,x3911)+~P5(x391,x392,x393,x394,x395,x396,x397,x398,x399,x3910,x3911,x3912)+~P6(x391,x392,x393,x394,x395,x396,x397,x398,x399,x3910,x3911,x3912,x3913)+P7(x391,x392,x393,x394,x395,x396,x397,x398,x399,x3910,x3911,x3912,x3913,x3914)+~P1(a5000) % 7.50/7.60 [42]~P2(x421)+~P13(x421,x422)+~P14(x421,x422,x423)+~P15(x421,x422,x423,x424)+~P17(x421,x422,x423,x424,x425)+~P19(x421,x422,x423,x424,x425,x426)+~P21(x421,x422,x423,x424,x425,x426,x427)+~P23(x421,x422,x423,x424,x425,x426,x427,x428)+~P24(x421,x422,x423,x424,x425,x426,x427,x428,x429)+~P3(x421,x422,x423,x424,x425,x426,x427,x428,x429,x4210)+~P4(x421,x422,x423,x424,x425,x426,x427,x428,x429,x4210,x4211)+~P5(x421,x422,x423,x424,x425,x426,x427,x428,x429,x4210,x4211,x4212)+~P6(x421,x422,x423,x424,x425,x426,x427,x428,x429,x4210,x4211,x4212,x4213)+P36(x421,x422,x423,x424,x425,x426,x427,x428,x429,x4210,x4211,x4212,x4213,x4214,a7)+~P1(a5000) % 7.50/7.60 [46]~P6(x461,x462,x463,x464,x465,x466,x467,x468,x469,x4610,x4611,x4612,x4613)+~P2(x461)+~P13(x461,x462)+~P14(x461,x462,x463)+~P15(x461,x462,x463,x464)+~P17(x461,x462,x463,x464,x465)+~P19(x461,x462,x463,x464,x465,x466)+~P21(x461,x462,x463,x464,x465,x466,x467)+~P23(x461,x462,x463,x464,x465,x466,x467,x468)+~P24(x461,x462,x463,x464,x465,x466,x467,x468,x469)+~P3(x461,x462,x463,x464,x465,x466,x467,x468,x469,x4610)+~P4(x461,x462,x463,x464,x465,x466,x467,x468,x469,x4610,x4611)+~P5(x461,x462,x463,x464,x465,x466,x467,x468,x469,x4610,x4611,x4612)+~P36(x461,x462,x463,x464,x465,x466,x467,x468,x469,x4610,x4611,x4612,x4613,x4614,a10)+~P1(a5000) % 7.50/7.60 [29]~P2(x291)+~P17(x291,x292,x293,x294,x295)+~P21(x291,x292,x293,x294,x295,x296,x297)+P31(x291)+~P13(x291,x292)+~P14(x291,x292,x293)+~P15(x291,x292,x293,x294)+~P16(x291,x292,x293,x294,x295)+~P19(x291,x292,x293,x294,x295,x296)+~P20(x291,x292,x293,x294,x295,x296,x297)+~P23(x291,x292,x293,x294,x295,x296,x297,x298)+~P24(x291,x292,x293,x294,x295,x296,x297,x298,x299)+~P3(x291,x292,x293,x294,x295,x296,x297,x298,x299,x2910)+~P4(x291,x292,x293,x294,x295,x296,x297,x298,x299,x2910,x2911)+~P33(x291,x292,x293,x294,x295,x296,x297,x298,x299,x2910,x2911,x2912)+~P1(a5000) % 7.50/7.60 [30]~P2(x301)+~P21(x301,x302,x303,x304,x305,x306,x307)+~P23(x301,x302,x303,x304,x305,x306,x307,x308)+P31(x301)+~P13(x301,x302)+~P14(x301,x302,x303)+~P15(x301,x302,x303,x304)+~P17(x301,x302,x303,x304,x305)+~P19(x301,x302,x303,x304,x305,x306)+~P20(x301,x302,x303,x304,x305,x306,x307)+~P22(x301,x302,x303,x304,x305,x306,x307,x308)+~P24(x301,x302,x303,x304,x305,x306,x307,x308,x309)+~P3(x301,x302,x303,x304,x305,x306,x307,x308,x309,x3010)+~P4(x301,x302,x303,x304,x305,x306,x307,x308,x309,x3010,x3011)+~P33(x301,x302,x303,x304,x305,x306,x307,x308,x309,x3010,x3011,x3012)+~P1(a5000) % 7.50/7.60 [43]~P2(x431)+~P13(x431,x432)+~P14(x431,x432,x433)+~P15(x431,x432,x433,x434)+~P17(x431,x432,x433,x434,x435)+~P19(x431,x432,x433,x434,x435,x436)+~P21(x431,x432,x433,x434,x435,x436,x437)+~P23(x431,x432,x433,x434,x435,x436,x437,x438)+~P24(x431,x432,x433,x434,x435,x436,x437,x438,x439)+~P3(x431,x432,x433,x434,x435,x436,x437,x438,x439,x4310)+~P4(x431,x432,x433,x434,x435,x436,x437,x438,x439,x4310,x4311)+~P5(x431,x432,x433,x434,x435,x436,x437,x438,x439,x4310,x4311,x4312)+~P6(x431,x432,x433,x434,x435,x436,x437,x438,x439,x4310,x4311,x4312,x4313)+~P7(x431,x432,x433,x434,x435,x436,x437,x438,x439,x4310,x4311,x4312,x4313,x4314)+P8(x431,x432,x433,x434,x435,x436,x437,x438,x439,x4310,x4311,x4312,x4313,x4314,x4315)+~P1(a5000) % 7.50/7.60 [48]~P2(x481)+~P13(x481,x482)+~P14(x481,x482,x483)+~P15(x481,x482,x483,x484)+~P17(x481,x482,x483,x484,x485)+~P19(x481,x482,x483,x484,x485,x486)+~P21(x481,x482,x483,x484,x485,x486,x487)+~P23(x481,x482,x483,x484,x485,x486,x487,x488)+~P24(x481,x482,x483,x484,x485,x486,x487,x488,x489)+~P3(x481,x482,x483,x484,x485,x486,x487,x488,x489,x4810)+~P4(x481,x482,x483,x484,x485,x486,x487,x488,x489,x4810,x4811)+~P5(x481,x482,x483,x484,x485,x486,x487,x488,x489,x4810,x4811,x4812)+~P6(x481,x482,x483,x484,x485,x486,x487,x488,x489,x4810,x4811,x4812,x4813)+~P7(x481,x482,x483,x484,x485,x486,x487,x488,x489,x4810,x4811,x4812,x4813,x4814)+P37(x481,x482,x483,x484,x485,x486,x487,x488,x489,x4810,x4811,x4812,x4813,x4814,x4815,a8)+~P1(a5000) % 7.50/7.60 [54]~P6(x541,x542,x543,x544,x545,x546,x547,x548,x549,x5410,x5411,x5412,x5413)+~P2(x541)+~P13(x541,x542)+~P14(x541,x542,x543)+~P15(x541,x542,x543,x544)+~P17(x541,x542,x543,x544,x545)+~P19(x541,x542,x543,x544,x545,x546)+~P21(x541,x542,x543,x544,x545,x546,x547)+~P23(x541,x542,x543,x544,x545,x546,x547,x548)+~P24(x541,x542,x543,x544,x545,x546,x547,x548,x549)+~P3(x541,x542,x543,x544,x545,x546,x547,x548,x549,x5410)+~P4(x541,x542,x543,x544,x545,x546,x547,x548,x549,x5410,x5411)+~P5(x541,x542,x543,x544,x545,x546,x547,x548,x549,x5410,x5411,x5412)+~P7(x541,x542,x543,x544,x545,x546,x547,x548,x549,x5410,x5411,x5412,x5413,x5414)+~P37(x541,x542,x543,x544,x545,x546,x547,x548,x549,x5410,x5411,x5412,x5413,x5414,x5415,a9)+~P1(a5000) % 7.50/7.60 [33]~P17(x331,x332,x333,x334,x335)+~P5(x331,x332,x333,x334,x335,x336,x337,x338,x339,x3310,x3311,x3312)+~P27(x331,x332,x333,x334,x335,x336,x337,x338,x339,x3310,x3311)+~P4(x331,x332,x333,x334,x335,x336,x337,x338,x339,x3310,x3311)+~P3(x331,x332,x333,x334,x335,x336,x337,x338,x339,x3310)+~P24(x331,x332,x333,x334,x335,x336,x337,x338,x339)+~P23(x331,x332,x333,x334,x335,x336,x337,x338)+~P21(x331,x332,x333,x334,x335,x336,x337)+~P19(x331,x332,x333,x334,x335,x336)+~P15(x331,x332,x333,x334)+~P14(x331,x332,x333)+~P13(x331,x332)+~P2(x331)+P34(x331,x332,x333,x334,x335,x336,x337,x338,x339,x3310,x3311,x3312,x3313)+P20(x331,x332,x333,x334,x335,x336,x337)+P26(x331,x332,x333,x334,x335,x336,x337,x338,x339,x3310)+~P1(a5000) % 7.50/7.60 [35]~P31(x351)+~P29(x351,x352)+~P21(x351,x352,x353,x354,x355,x356,x357)+~P34(x351,x352,x353,x354,x355,x356,x357,x358,x359,x3510,x3511,x3512,x3513)+~P19(x351,x352,x353,x354,x355,x356)+~P5(x351,x352,x353,x354,x355,x356,x357,x358,x359,x3510,x3511,x3512)+~P4(x351,x352,x353,x354,x355,x356,x357,x358,x359,x3510,x3511)+~P3(x351,x352,x353,x354,x355,x356,x357,x358,x359,x3510)+~P24(x351,x352,x353,x354,x355,x356,x357,x358,x359)+~P23(x351,x352,x353,x354,x355,x356,x357,x358)+~P20(x351,x352,x353,x354,x355,x356,x357)+~P17(x351,x352,x353,x354,x355)+~P15(x351,x352,x353,x354)+~P14(x351,x352,x353)+~P13(x351,x352)+~P2(x351)+~P1(a5000) % 7.50/7.60 [36]~P24(x361,x362,x363,x364,x365,x366,x367,x368,x369)+~P23(x361,x362,x363,x364,x365,x366,x367,x368)+~P2(x361)+~P31(x361)+~P13(x361,x362)+~P14(x361,x362,x363)+~P15(x361,x362,x363,x364)+~P17(x361,x362,x363,x364,x365)+~P19(x361,x362,x363,x364,x365,x366)+~P21(x361,x362,x363,x364,x365,x366,x367)+~P34(x361,x362,x363,x364,x365,x366,x367,x368,x369,x3610,x3611,x3612,x3613)+P25(x361,x362,x363,x364,x365,x366,x367,x368,x369)+~P3(x361,x362,x363,x364,x365,x366,x367,x368,x369,x3610)+~P4(x361,x362,x363,x364,x365,x366,x367,x368,x369,x3610,x3611)+~P5(x361,x362,x363,x364,x365,x366,x367,x368,x369,x3610,x3611,x3612)+P18(x361,x362,x363,x364,x365,x366)+~P1(a5000) % 7.50/7.60 [37]~P29(x371,x372)+~P27(x371,x372,x373,x374,x375,x376,x377,x378,x379,x3710,x3711)+~P21(x371,x372,x373,x374,x375,x376,x377)+~P34(x371,x372,x373,x374,x375,x376,x377,x378,x379,x3710,x3711,x3712,x3713)+~P20(x371,x372,x373,x374,x375,x376,x377)+~P5(x371,x372,x373,x374,x375,x376,x377,x378,x379,x3710,x3711,x3712)+~P4(x371,x372,x373,x374,x375,x376,x377,x378,x379,x3710,x3711)+~P3(x371,x372,x373,x374,x375,x376,x377,x378,x379,x3710)+~P24(x371,x372,x373,x374,x375,x376,x377,x378,x379)+~P23(x371,x372,x373,x374,x375,x376,x377,x378)+~P19(x371,x372,x373,x374,x375,x376)+~P17(x371,x372,x373,x374,x375)+~P15(x371,x372,x373,x374)+~P14(x371,x372,x373)+~P13(x371,x372)+~P2(x371)+~P1(a5000) % 7.50/7.60 [49]~P21(x491,x492,x493,x494,x495,x496,x497)+~P8(x491,x492,x493,x494,x495,x496,x497,x498,x499,x4910,x4911,x4912,x4913,x4914,x4915)+~P7(x491,x492,x493,x494,x495,x496,x497,x498,x499,x4910,x4911,x4912,x4913,x4914)+~P6(x491,x492,x493,x494,x495,x496,x497,x498,x499,x4910,x4911,x4912,x4913)+~P5(x491,x492,x493,x494,x495,x496,x497,x498,x499,x4910,x4911,x4912)+~P4(x491,x492,x493,x494,x495,x496,x497,x498,x499,x4910,x4911)+~P3(x491,x492,x493,x494,x495,x496,x497,x498,x499,x4910)+~P24(x491,x492,x493,x494,x495,x496,x497,x498,x499)+~P23(x491,x492,x493,x494,x495,x496,x497,x498)+~P19(x491,x492,x493,x494,x495,x496)+~P17(x491,x492,x493,x494,x495)+~P15(x491,x492,x493,x494)+~P14(x491,x492,x493)+~P13(x491,x492)+~P2(x491)+P9(x491,x492,x493,x494,x495,x496,x497,x498,x499,x4910,x4911,x4912,x4913,x4914,x4915,x4916)+~P1(a5000) % 7.50/7.60 [41]~P2(x411)+~P13(x411,x412)+~P29(x411,x412)+~P14(x411,x412,x413)+~P15(x411,x412,x413,x414)+~P17(x411,x412,x413,x414,x415)+~P19(x411,x412,x413,x414,x415,x416)+~P21(x411,x412,x413,x414,x415,x416,x417)+~P25(x411,x412,x413,x414,x415,x416,x417,x418,x419)+~P6(x411,x412,x413,x414,x415,x416,x417,x418,x419,x4110,x4111,x4112,x4113)+~P35(x411,x412,x413,x414,x415,x416,x417,x418,x419,x4110,x4111,x4112,x4113,x4114)+P20(x411,x412,x413,x414,x415,x416,x417)+~P5(x411,x412,x413,x414,x415,x416,x417,x418,x419,x4110,x4111,x4112)+~P4(x411,x412,x413,x414,x415,x416,x417,x418,x419,x4110,x4111)+~P3(x411,x412,x413,x414,x415,x416,x417,x418,x419,x4110)+~P24(x411,x412,x413,x414,x415,x416,x417,x418,x419)+~P23(x411,x412,x413,x414,x415,x416,x417,x418)+~P1(a5000) % 7.50/7.60 [55]~P23(x551,x552,x553,x554,x555,x556,x557,x558)+~P9(x551,x552,x553,x554,x555,x556,x557,x558,x559,x5510,x5511,x5512,x5513,x5514,x5515,x5516)+~P8(x551,x552,x553,x554,x555,x556,x557,x558,x559,x5510,x5511,x5512,x5513,x5514,x5515)+~P7(x551,x552,x553,x554,x555,x556,x557,x558,x559,x5510,x5511,x5512,x5513,x5514)+~P6(x551,x552,x553,x554,x555,x556,x557,x558,x559,x5510,x5511,x5512,x5513)+~P5(x551,x552,x553,x554,x555,x556,x557,x558,x559,x5510,x5511,x5512)+~P4(x551,x552,x553,x554,x555,x556,x557,x558,x559,x5510,x5511)+~P3(x551,x552,x553,x554,x555,x556,x557,x558,x559,x5510)+~P24(x551,x552,x553,x554,x555,x556,x557,x558,x559)+~P21(x551,x552,x553,x554,x555,x556,x557)+~P19(x551,x552,x553,x554,x555,x556)+~P17(x551,x552,x553,x554,x555)+~P15(x551,x552,x553,x554)+~P14(x551,x552,x553)+~P13(x551,x552)+~P2(x551)+P10(x551,x552,x553,x554,x555,x556,x557,x558,x559,x5510,x5511,x5512,x5513,x5514,x5515,x5516,x5517)+~P1(a5000) % 7.50/7.60 [44]~P17(x441,x442,x443,x444,x445)+~P7(x441,x442,x443,x444,x445,x446,x447,x448,x449,x4410,x4411,x4412,x4413,x4414)+~P6(x441,x442,x443,x444,x445,x446,x447,x448,x449,x4410,x4411,x4412,x4413)+~P5(x441,x442,x443,x444,x445,x446,x447,x448,x449,x4410,x4411,x4412)+~P4(x441,x442,x443,x444,x445,x446,x447,x448,x449,x4410,x4411)+~P3(x441,x442,x443,x444,x445,x446,x447,x448,x449,x4410)+~P24(x441,x442,x443,x444,x445,x446,x447,x448,x449)+~P23(x441,x442,x443,x444,x445,x446,x447,x448)+~P21(x441,x442,x443,x444,x445,x446,x447)+~P19(x441,x442,x443,x444,x445,x446)+~P16(x441,x442,x443,x444,x445)+~P15(x441,x442,x443,x444)+~P14(x441,x442,x443)+~P13(x441,x442)+~P2(x441)+P29(x441,x442)+P36(x441,x442,x443,x444,x445,x446,x447,x448,x449,x4410,x4411,x4412,x4413,x4414,x4415)+P30(x441,x442,x443)+~P1(a5000) % 7.50/7.60 [45]~P19(x451,x452,x453,x454,x455,x456)+~P7(x451,x452,x453,x454,x455,x456,x457,x458,x459,x4510,x4511,x4512,x4513,x4514)+~P6(x451,x452,x453,x454,x455,x456,x457,x458,x459,x4510,x4511,x4512,x4513)+~P5(x451,x452,x453,x454,x455,x456,x457,x458,x459,x4510,x4511,x4512)+~P27(x451,x452,x453,x454,x455,x456,x457,x458,x459,x4510,x4511)+~P4(x451,x452,x453,x454,x455,x456,x457,x458,x459,x4510,x4511)+~P3(x451,x452,x453,x454,x455,x456,x457,x458,x459,x4510)+~P24(x451,x452,x453,x454,x455,x456,x457,x458,x459)+~P23(x451,x452,x453,x454,x455,x456,x457,x458)+~P21(x451,x452,x453,x454,x455,x456,x457)+~P17(x451,x452,x453,x454,x455)+~P15(x451,x452,x453,x454)+~P14(x451,x452,x453)+~P13(x451,x452)+~P2(x451)+P29(x451,x452)+P36(x451,x452,x453,x454,x455,x456,x457,x458,x459,x4510,x4511,x4512,x4513,x4514,x4515)+P16(x451,x452,x453,x454,x455)+~P1(a5000) % 7.50/7.60 [47]~P2(x471)+~P13(x471,x472)+~P29(x471,x472)+~P14(x471,x472,x473)+~P15(x471,x472,x473,x474)+~P17(x471,x472,x473,x474,x475)+~P19(x471,x472,x473,x474,x475,x476)+~P21(x471,x472,x473,x474,x475,x476,x477)+~P23(x471,x472,x473,x474,x475,x476,x477,x478)+~P24(x471,x472,x473,x474,x475,x476,x477,x478,x479)+~P6(x471,x472,x473,x474,x475,x476,x477,x478,x479,x4710,x4711,x4712,x4713)+~P36(x471,x472,x473,x474,x475,x476,x477,x478,x479,x4710,x4711,x4712,x4713,x4714,x4715)+P22(x471,x472,x473,x474,x475,x476,x477,x478)+~P7(x471,x472,x473,x474,x475,x476,x477,x478,x479,x4710,x4711,x4712,x4713,x4714)+~P5(x471,x472,x473,x474,x475,x476,x477,x478,x479,x4710,x4711,x4712)+~P4(x471,x472,x473,x474,x475,x476,x477,x478,x479,x4710,x4711)+~P3(x471,x472,x473,x474,x475,x476,x477,x478,x479,x4710)+P25(x471,x472,x473,x474,x475,x476,x477,x478,x479)+~P1(a5000) % 7.50/7.60 [64]~P23(x641,x642,x643,x644,x645,x646,x647,x648)+~P10(x641,x642,x643,x644,x645,x646,x647,x648,x649,x6410,x6411,x6412,x6413,x6414,x6415,x6416,x6417)+~P9(x641,x642,x643,x644,x645,x646,x647,x648,x649,x6410,x6411,x6412,x6413,x6414,x6415,x6416)+~P8(x641,x642,x643,x644,x645,x646,x647,x648,x649,x6410,x6411,x6412,x6413,x6414,x6415)+~P7(x641,x642,x643,x644,x645,x646,x647,x648,x649,x6410,x6411,x6412,x6413,x6414)+~P6(x641,x642,x643,x644,x645,x646,x647,x648,x649,x6410,x6411,x6412,x6413)+~P5(x641,x642,x643,x644,x645,x646,x647,x648,x649,x6410,x6411,x6412)+~P4(x641,x642,x643,x644,x645,x646,x647,x648,x649,x6410,x6411)+~P3(x641,x642,x643,x644,x645,x646,x647,x648,x649,x6410)+~P24(x641,x642,x643,x644,x645,x646,x647,x648,x649)+~P21(x641,x642,x643,x644,x645,x646,x647)+~P19(x641,x642,x643,x644,x645,x646)+~P17(x641,x642,x643,x644,x645)+~P15(x641,x642,x643,x644)+~P14(x641,x642,x643)+~P13(x641,x642)+~P2(x641)+P11(x641,x642,x643,x644,x645,x646,x647,x648,x649,x6410,x6411,x6412,x6413,x6414,x6415,x6416,x6417,x6418)+~P1(a5000) % 7.50/7.60 [50]~P19(x501,x502,x503,x504,x505,x506)+~P8(x501,x502,x503,x504,x505,x506,x507,x508,x509,x5010,x5011,x5012,x5013,x5014,x5015)+~P7(x501,x502,x503,x504,x505,x506,x507,x508,x509,x5010,x5011,x5012,x5013,x5014)+~P6(x501,x502,x503,x504,x505,x506,x507,x508,x509,x5010,x5011,x5012,x5013)+~P5(x501,x502,x503,x504,x505,x506,x507,x508,x509,x5010,x5011,x5012)+~P4(x501,x502,x503,x504,x505,x506,x507,x508,x509,x5010,x5011)+~P3(x501,x502,x503,x504,x505,x506,x507,x508,x509,x5010)+~P24(x501,x502,x503,x504,x505,x506,x507,x508,x509)+~P23(x501,x502,x503,x504,x505,x506,x507,x508)+~P21(x501,x502,x503,x504,x505,x506,x507)+~P18(x501,x502,x503,x504,x505,x506)+~P17(x501,x502,x503,x504,x505)+~P15(x501,x502,x503,x504)+~P14(x501,x502,x503)+~P13(x501,x502)+~P31(x501)+~P2(x501)+P33(x501,x502,x503,x504,x505,x506,x507,x508,x509,x5010,x5011,x5012)+P37(x501,x502,x503,x504,x505,x506,x507,x508,x509,x5010,x5011,x5012,x5013,x5014,x5015,x5016)+~P1(a5000) % 7.50/7.60 [51]~P21(x511,x512,x513,x514,x515,x516,x517)+~P8(x511,x512,x513,x514,x515,x516,x517,x518,x519,x5110,x5111,x5112,x5113,x5114,x5115)+~P7(x511,x512,x513,x514,x515,x516,x517,x518,x519,x5110,x5111,x5112,x5113,x5114)+~P6(x511,x512,x513,x514,x515,x516,x517,x518,x519,x5110,x5111,x5112,x5113)+~P5(x511,x512,x513,x514,x515,x516,x517,x518,x519,x5110,x5111,x5112)+~P4(x511,x512,x513,x514,x515,x516,x517,x518,x519,x5110,x5111)+~P26(x511,x512,x513,x514,x515,x516,x517,x518,x519,x5110)+~P3(x511,x512,x513,x514,x515,x516,x517,x518,x519,x5110)+~P24(x511,x512,x513,x514,x515,x516,x517,x518,x519)+~P23(x511,x512,x513,x514,x515,x516,x517,x518)+~P19(x511,x512,x513,x514,x515,x516)+~P17(x511,x512,x513,x514,x515)+~P15(x511,x512,x513,x514)+~P14(x511,x512,x513)+~P13(x511,x512)+~P2(x511)+P31(x511)+P37(x511,x512,x513,x514,x515,x516,x517,x518,x519,x5110,x5111,x5112,x5113,x5114,x5115,x5116)+P35(x511,x512,x513,x514,x515,x516,x517,x518,x519,x5110,x5111,x5112,x5113,x5114)+~P1(a5000) % 7.50/7.60 [52]~P21(x521,x522,x523,x524,x525,x526,x527)+~P8(x521,x522,x523,x524,x525,x526,x527,x528,x529,x5210,x5211,x5212,x5213,x5214,x5215)+~P7(x521,x522,x523,x524,x525,x526,x527,x528,x529,x5210,x5211,x5212,x5213,x5214)+~P35(x521,x522,x523,x524,x525,x526,x527,x528,x529,x5210,x5211,x5212,x5213,x5214)+~P6(x521,x522,x523,x524,x525,x526,x527,x528,x529,x5210,x5211,x5212,x5213)+~P5(x521,x522,x523,x524,x525,x526,x527,x528,x529,x5210,x5211,x5212)+~P4(x521,x522,x523,x524,x525,x526,x527,x528,x529,x5210,x5211)+~P3(x521,x522,x523,x524,x525,x526,x527,x528,x529,x5210)+~P24(x521,x522,x523,x524,x525,x526,x527,x528,x529)+~P23(x521,x522,x523,x524,x525,x526,x527,x528)+~P19(x521,x522,x523,x524,x525,x526)+~P17(x521,x522,x523,x524,x525)+~P15(x521,x522,x523,x524)+~P30(x521,x522,x523)+~P14(x521,x522,x523)+~P13(x521,x522)+~P2(x521)+P26(x521,x522,x523,x524,x525,x526,x527,x528,x529,x5210)+P37(x521,x522,x523,x524,x525,x526,x527,x528,x529,x5210,x5211,x5212,x5213,x5214,x5215,x5216)+~P1(a5000) % 7.50/7.60 [53]~P24(x531,x532,x533,x534,x535,x536,x537,x538,x539)+~P8(x531,x532,x533,x534,x535,x536,x537,x538,x539,x5310,x5311,x5312,x5313,x5314,x5315)+~P7(x531,x532,x533,x534,x535,x536,x537,x538,x539,x5310,x5311,x5312,x5313,x5314)+~P35(x531,x532,x533,x534,x535,x536,x537,x538,x539,x5310,x5311,x5312,x5313,x5314)+~P6(x531,x532,x533,x534,x535,x536,x537,x538,x539,x5310,x5311,x5312,x5313)+~P5(x531,x532,x533,x534,x535,x536,x537,x538,x539,x5310,x5311,x5312)+~P27(x531,x532,x533,x534,x535,x536,x537,x538,x539,x5310,x5311)+~P4(x531,x532,x533,x534,x535,x536,x537,x538,x539,x5310,x5311)+~P26(x531,x532,x533,x534,x535,x536,x537,x538,x539,x5310)+~P3(x531,x532,x533,x534,x535,x536,x537,x538,x539,x5310)+~P23(x531,x532,x533,x534,x535,x536,x537,x538)+~P21(x531,x532,x533,x534,x535,x536,x537)+~P19(x531,x532,x533,x534,x535,x536)+~P17(x531,x532,x533,x534,x535)+~P15(x531,x532,x533,x534)+~P14(x531,x532,x533)+~P13(x531,x532)+~P2(x531)+P37(x531,x532,x533,x534,x535,x536,x537,x538,x539,x5310,x5311,x5312,x5313,x5314,x5315,x5316)+~P1(a5000) % 7.50/7.60 [72]~P24(x721,x722,x723,x724,x725,x726,x727,x728,x729)+~P11(x721,x722,x723,x724,x725,x726,x727,x728,x729,x7210,x7211,x7212,x7213,x7214,x7215,x7216,x7217,x7218)+~P10(x721,x722,x723,x724,x725,x726,x727,x728,x729,x7210,x7211,x7212,x7213,x7214,x7215,x7216,x7217)+~P9(x721,x722,x723,x724,x725,x726,x727,x728,x729,x7210,x7211,x7212,x7213,x7214,x7215,x7216)+~P8(x721,x722,x723,x724,x725,x726,x727,x728,x729,x7210,x7211,x7212,x7213,x7214,x7215)+~P7(x721,x722,x723,x724,x725,x726,x727,x728,x729,x7210,x7211,x7212,x7213,x7214)+~P6(x721,x722,x723,x724,x725,x726,x727,x728,x729,x7210,x7211,x7212,x7213)+~P5(x721,x722,x723,x724,x725,x726,x727,x728,x729,x7210,x7211,x7212)+~P4(x721,x722,x723,x724,x725,x726,x727,x728,x729,x7210,x7211)+~P3(x721,x722,x723,x724,x725,x726,x727,x728,x729,x7210)+~P23(x721,x722,x723,x724,x725,x726,x727,x728)+~P21(x721,x722,x723,x724,x725,x726,x727)+~P19(x721,x722,x723,x724,x725,x726)+~P17(x721,x722,x723,x724,x725)+~P15(x721,x722,x723,x724)+~P14(x721,x722,x723)+~P13(x721,x722)+~P2(x721)+P12(x721,x722,x723,x724,x725,x726,x727,x728,x729,x7210,x7211,x7212,x7213,x7214,x7215,x7216,x7217,x7218,x7219)+~P1(a5000) % 7.50/7.60 [56]~P21(x561,x562,x563,x564,x565,x566,x567)+~P9(x561,x562,x563,x564,x565,x566,x567,x568,x569,x5610,x5611,x5612,x5613,x5614,x5615,x5616)+~P8(x561,x562,x563,x564,x565,x566,x567,x568,x569,x5610,x5611,x5612,x5613,x5614,x5615)+~P7(x561,x562,x563,x564,x565,x566,x567,x568,x569,x5610,x5611,x5612,x5613,x5614)+~P6(x561,x562,x563,x564,x565,x566,x567,x568,x569,x5610,x5611,x5612,x5613)+~P5(x561,x562,x563,x564,x565,x566,x567,x568,x569,x5610,x5611,x5612)+~P4(x561,x562,x563,x564,x565,x566,x567,x568,x569,x5610,x5611)+~P3(x561,x562,x563,x564,x565,x566,x567,x568,x569,x5610)+~P24(x561,x562,x563,x564,x565,x566,x567,x568,x569)+~P23(x561,x562,x563,x564,x565,x566,x567,x568)+~P22(x561,x562,x563,x564,x565,x566,x567,x568)+~P19(x561,x562,x563,x564,x565,x566)+~P17(x561,x562,x563,x564,x565)+~P16(x561,x562,x563,x564,x565)+~P15(x561,x562,x563,x564)+~P14(x561,x562,x563)+~P13(x561,x562)+~P31(x561)+~P2(x561)+P38(x561,x562,x563,x564,x565,x566,x567,x568,x569,x5610,x5611,x5612,x5613,x5614,x5615,x5616,x5617)+~P1(a5000) % 7.50/7.60 [57]~P19(x571,x572,x573,x574,x575,x576)+~P9(x571,x572,x573,x574,x575,x576,x577,x578,x579,x5710,x5711,x5712,x5713,x5714,x5715,x5716)+~P8(x571,x572,x573,x574,x575,x576,x577,x578,x579,x5710,x5711,x5712,x5713,x5714,x5715)+~P7(x571,x572,x573,x574,x575,x576,x577,x578,x579,x5710,x5711,x5712,x5713,x5714)+~P6(x571,x572,x573,x574,x575,x576,x577,x578,x579,x5710,x5711,x5712,x5713)+~P5(x571,x572,x573,x574,x575,x576,x577,x578,x579,x5710,x5711,x5712)+~P4(x571,x572,x573,x574,x575,x576,x577,x578,x579,x5710,x5711)+~P3(x571,x572,x573,x574,x575,x576,x577,x578,x579,x5710)+~P24(x571,x572,x573,x574,x575,x576,x577,x578,x579)+~P23(x571,x572,x573,x574,x575,x576,x577,x578)+~P21(x571,x572,x573,x574,x575,x576,x577)+~P17(x571,x572,x573,x574,x575)+~P15(x571,x572,x573,x574)+~P14(x571,x572,x573)+~P13(x571,x572)+~P2(x571)+P34(x571,x572,x573,x574,x575,x576,x577,x578,x579,x5710,x5711,x5712,x5713)+P16(x571,x572,x573,x574,x575)+P38(x571,x572,x573,x574,x575,x576,x577,x578,x579,x5710,x5711,x5712,x5713,x5714,x5715,x5716,x5717)+P27(x571,x572,x573,x574,x575,x576,x577,x578,x579,x5710,x5711)+~P1(a5000) % 7.50/7.60 [58]~P20(x581,x582,x583,x584,x585,x586,x587)+~P9(x581,x582,x583,x584,x585,x586,x587,x588,x589,x5810,x5811,x5812,x5813,x5814,x5815,x5816)+~P8(x581,x582,x583,x584,x585,x586,x587,x588,x589,x5810,x5811,x5812,x5813,x5814,x5815)+~P7(x581,x582,x583,x584,x585,x586,x587,x588,x589,x5810,x5811,x5812,x5813,x5814)+~P6(x581,x582,x583,x584,x585,x586,x587,x588,x589,x5810,x5811,x5812,x5813)+~P5(x581,x582,x583,x584,x585,x586,x587,x588,x589,x5810,x5811,x5812)+~P4(x581,x582,x583,x584,x585,x586,x587,x588,x589,x5810,x5811)+~P3(x581,x582,x583,x584,x585,x586,x587,x588,x589,x5810)+~P24(x581,x582,x583,x584,x585,x586,x587,x588,x589)+~P23(x581,x582,x583,x584,x585,x586,x587,x588)+~P21(x581,x582,x583,x584,x585,x586,x587)+~P19(x581,x582,x583,x584,x585,x586)+~P17(x581,x582,x583,x584,x585)+~P15(x581,x582,x583,x584)+~P14(x581,x582,x583)+~P29(x581,x582)+~P13(x581,x582)+~P2(x581)+P36(x581,x582,x583,x584,x585,x586,x587,x588,x589,x5810,x5811,x5812,x5813,x5814,x5815)+P38(x581,x582,x583,x584,x585,x586,x587,x588,x589,x5810,x5811,x5812,x5813,x5814,x5815,x5816,x5817)+~P1(a5000) % 7.50/7.60 [59]~P21(x591,x592,x593,x594,x595,x596,x597)+~P9(x591,x592,x593,x594,x595,x596,x597,x598,x599,x5910,x5911,x5912,x5913,x5914,x5915,x5916)+~P8(x591,x592,x593,x594,x595,x596,x597,x598,x599,x5910,x5911,x5912,x5913,x5914,x5915)+~P7(x591,x592,x593,x594,x595,x596,x597,x598,x599,x5910,x5911,x5912,x5913,x5914)+~P6(x591,x592,x593,x594,x595,x596,x597,x598,x599,x5910,x5911,x5912,x5913)+~P5(x591,x592,x593,x594,x595,x596,x597,x598,x599,x5910,x5911,x5912)+~P4(x591,x592,x593,x594,x595,x596,x597,x598,x599,x5910,x5911)+~P3(x591,x592,x593,x594,x595,x596,x597,x598,x599,x5910)+~P24(x591,x592,x593,x594,x595,x596,x597,x598,x599)+~P23(x591,x592,x593,x594,x595,x596,x597,x598)+~P22(x591,x592,x593,x594,x595,x596,x597,x598)+~P19(x591,x592,x593,x594,x595,x596)+~P17(x591,x592,x593,x594,x595)+~P15(x591,x592,x593,x594)+~P14(x591,x592,x593)+~P13(x591,x592)+~P2(x591)+P30(x591,x592,x593)+P38(x591,x592,x593,x594,x595,x596,x597,x598,x599,x5910,x5911,x5912,x5913,x5914,x5915,x5916,x5917)+P36(x591,x592,x593,x594,x595,x596,x597,x598,x599,x5910,x5911,x5912,x5913,x5914,x5915)+~P1(a5000) % 7.50/7.60 [60]~P2(x601)+~P13(x601,x602)+~P14(x601,x602,x603)+~P15(x601,x602,x603,x604)+~P17(x601,x602,x603,x604,x605)+~P19(x601,x602,x603,x604,x605,x606)+~P21(x601,x602,x603,x604,x605,x606,x607)+~P23(x601,x602,x603,x604,x605,x606,x607,x608)+~P24(x601,x602,x603,x604,x605,x606,x607,x608,x609)+~P3(x601,x602,x603,x604,x605,x606,x607,x608,x609,x6010)+~P6(x601,x602,x603,x604,x605,x606,x607,x608,x609,x6010,x6011,x6012,x6013)+~P38(x601,x602,x603,x604,x605,x606,x607,x608,x609,x6010,x6011,x6012,x6013,x6014,x6015,x6016,x6017)+P20(x601,x602,x603,x604,x605,x606,x607)+~P9(x601,x602,x603,x604,x605,x606,x607,x608,x609,x6010,x6011,x6012,x6013,x6014,x6015,x6016)+~P8(x601,x602,x603,x604,x605,x606,x607,x608,x609,x6010,x6011,x6012,x6013,x6014,x6015)+~P7(x601,x602,x603,x604,x605,x606,x607,x608,x609,x6010,x6011,x6012,x6013,x6014)+~P5(x601,x602,x603,x604,x605,x606,x607,x608,x609,x6010,x6011,x6012)+~P4(x601,x602,x603,x604,x605,x606,x607,x608,x609,x6010,x6011)+P26(x601,x602,x603,x604,x605,x606,x607,x608,x609,x6010)+P22(x601,x602,x603,x604,x605,x606,x607,x608)+~P1(a5000) % 7.50/7.60 [61]~P21(x611,x612,x613,x614,x615,x616,x617)+~P7(x611,x612,x613,x614,x615,x616,x617,x618,x619,x6110,x6111,x6112,x6113,x6114)+~P6(x611,x612,x613,x614,x615,x616,x617,x618,x619,x6110,x6111,x6112,x6113)+~P34(x611,x612,x613,x614,x615,x616,x617,x618,x619,x6110,x6111,x6112,x6113)+~P5(x611,x612,x613,x614,x615,x616,x617,x618,x619,x6110,x6111,x6112)+~P4(x611,x612,x613,x614,x615,x616,x617,x618,x619,x6110,x6111)+~P3(x611,x612,x613,x614,x615,x616,x617,x618,x619,x6110)+~P24(x611,x612,x613,x614,x615,x616,x617,x618,x619)+~P23(x611,x612,x613,x614,x615,x616,x617,x618)+~P19(x611,x612,x613,x614,x615,x616)+~P17(x611,x612,x613,x614,x615)+~P28(x611,x612,x613,x614)+~P15(x611,x612,x613,x614)+~P14(x611,x612,x613)+~P13(x611,x612)+~P2(x611)+~P9(x611,x612,x613,x614,x615,x616,x617,x618,x619,x6110,x6111,x6112,x6113,x6114,x6115,x6116)+~P38(x611,x612,x613,x614,x615,x616,x617,x618,x619,x6110,x6111,x6112,x6113,x6114,x6115,x6116,x6117)+P35(x611,x612,x613,x614,x615,x616,x617,x618,x619,x6110,x6111,x6112,x6113,x6114)+~P8(x611,x612,x613,x614,x615,x616,x617,x618,x619,x6110,x6111,x6112,x6113,x6114,x6115)+~P1(a5000) % 7.50/7.60 [62]~P19(x621,x622,x623,x624,x625,x626)+~P8(x621,x622,x623,x624,x625,x626,x627,x628,x629,x6210,x6211,x6212,x6213,x6214,x6215)+~P5(x621,x622,x623,x624,x625,x626,x627,x628,x629,x6210,x6211,x6212)+~P4(x621,x622,x623,x624,x625,x626,x627,x628,x629,x6210,x6211)+~P3(x621,x622,x623,x624,x625,x626,x627,x628,x629,x6210)+~P24(x621,x622,x623,x624,x625,x626,x627,x628,x629)+~P23(x621,x622,x623,x624,x625,x626,x627,x628)+~P21(x621,x622,x623,x624,x625,x626,x627)+~P17(x621,x622,x623,x624,x625)+~P15(x621,x622,x623,x624)+~P14(x621,x622,x623)+~P13(x621,x622)+~P2(x621)+~P6(x621,x622,x623,x624,x625,x626,x627,x628,x629,x6210,x6211,x6212,x6213)+~P38(x621,x622,x623,x624,x625,x626,x627,x628,x629,x6210,x6211,x6212,x6213,x6214,x6215,x6216,x6217)+~P9(x621,x622,x623,x624,x625,x626,x627,x628,x629,x6210,x6211,x6212,x6213,x6214,x6215,x6216)+P22(x621,x622,x623,x624,x625,x626,x627,x628)+~P36(x621,x622,x623,x624,x625,x626,x627,x628,x629,x6210,x6211,x6212,x6213,x6214,x6215)+~P7(x621,x622,x623,x624,x625,x626,x627,x628,x629,x6210,x6211,x6212,x6213,x6214)+P33(x621,x622,x623,x624,x625,x626,x627,x628,x629,x6210,x6211,x6212)+~P1(a5000) % 7.50/7.60 [63]~P21(x631,x632,x633,x634,x635,x636,x637)+~P8(x631,x632,x633,x634,x635,x636,x637,x638,x639,x6310,x6311,x6312,x6313,x6314,x6315)+~P7(x631,x632,x633,x634,x635,x636,x637,x638,x639,x6310,x6311,x6312,x6313,x6314)+~P6(x631,x632,x633,x634,x635,x636,x637,x638,x639,x6310,x6311,x6312,x6313)+~P5(x631,x632,x633,x634,x635,x636,x637,x638,x639,x6310,x6311,x6312)+~P4(x631,x632,x633,x634,x635,x636,x637,x638,x639,x6310,x6311)+~P3(x631,x632,x633,x634,x635,x636,x637,x638,x639,x6310)+~P25(x631,x632,x633,x634,x635,x636,x637,x638,x639)+~P24(x631,x632,x633,x634,x635,x636,x637,x638,x639)+~P23(x631,x632,x633,x634,x635,x636,x637,x638)+~P19(x631,x632,x633,x634,x635,x636)+~P17(x631,x632,x633,x634,x635)+~P15(x631,x632,x633,x634)+~P14(x631,x632,x633)+~P13(x631,x632)+~P2(x631)+~P9(x631,x632,x633,x634,x635,x636,x637,x638,x639,x6310,x6311,x6312,x6313,x6314,x6315,x6316)+P34(x631,x632,x633,x634,x635,x636,x637,x638,x639,x6310,x6311,x6312,x6313)+~P38(x631,x632,x633,x634,x635,x636,x637,x638,x639,x6310,x6311,x6312,x6313,x6314,x6315,x6316,x6317)+P37(x631,x632,x633,x634,x635,x636,x637,x638,x639,x6310,x6311,x6312,x6313,x6314,x6315,x6316)+~P1(a5000) % 7.50/7.60 [65]~P23(x651,x652,x653,x654,x655,x656,x657,x658)+~P10(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510,x6511,x6512,x6513,x6514,x6515,x6516,x6517)+~P9(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510,x6511,x6512,x6513,x6514,x6515,x6516)+~P8(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510,x6511,x6512,x6513,x6514,x6515)+~P36(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510,x6511,x6512,x6513,x6514,x6515)+~P7(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510,x6511,x6512,x6513,x6514)+~P6(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510,x6511,x6512,x6513)+~P5(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510,x6511,x6512)+~P4(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510,x6511)+~P3(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510)+~P24(x651,x652,x653,x654,x655,x656,x657,x658,x659)+~P22(x651,x652,x653,x654,x655,x656,x657,x658)+~P21(x651,x652,x653,x654,x655,x656,x657)+~P19(x651,x652,x653,x654,x655,x656)+~P17(x651,x652,x653,x654,x655)+~P15(x651,x652,x653,x654)+~P14(x651,x652,x653)+~P13(x651,x652)+~P2(x651)+P33(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510,x6511,x6512)+P39(x651,x652,x653,x654,x655,x656,x657,x658,x659,x6510,x6511,x6512,x6513,x6514,x6515,x6516,x6517,x6518)+~P1(a5000) % 7.50/7.60 [66]~P2(x661)+~P13(x661,x662)+~P14(x661,x662,x663)+~P19(x661,x662,x663,x664,x665,x666)+~P23(x661,x662,x663,x664,x665,x666,x667,x668)+~P6(x661,x662,x663,x664,x665,x666,x667,x668,x669,x6610,x6611,x6612,x6613)+~P39(x661,x662,x663,x664,x665,x666,x667,x668,x669,x6610,x6611,x6612,x6613,x6614,x6615,x6616,x6617,x6618)+P30(x661,x662,x663)+~P10(x661,x662,x663,x664,x665,x666,x667,x668,x669,x6610,x6611,x6612,x6613,x6614,x6615,x6616,x6617)+~P9(x661,x662,x663,x664,x665,x666,x667,x668,x669,x6610,x6611,x6612,x6613,x6614,x6615,x6616)+~P8(x661,x662,x663,x664,x665,x666,x667,x668,x669,x6610,x6611,x6612,x6613,x6614,x6615)+~P7(x661,x662,x663,x664,x665,x666,x667,x668,x669,x6610,x6611,x6612,x6613,x6614)+~P5(x661,x662,x663,x664,x665,x666,x667,x668,x669,x6610,x6611,x6612)+~P4(x661,x662,x663,x664,x665,x666,x667,x668,x669,x6610,x6611)+~P3(x661,x662,x663,x664,x665,x666,x667,x668,x669,x6610)+~P24(x661,x662,x663,x664,x665,x666,x667,x668,x669)+~P22(x661,x662,x663,x664,x665,x666,x667,x668)+~P21(x661,x662,x663,x664,x665,x666,x667)+~P18(x661,x662,x663,x664,x665,x666)+~P17(x661,x662,x663,x664,x665)+~P15(x661,x662,x663,x664)+~P1(a5000) % 7.50/7.60 [67]~P2(x671)+~P13(x671,x672)+~P14(x671,x672,x673)+~P15(x671,x672,x673,x674)+~P17(x671,x672,x673,x674,x675)+~P7(x671,x672,x673,x674,x675,x676,x677,x678,x679,x6710,x6711,x6712,x6713,x6714)+~P6(x671,x672,x673,x674,x675,x676,x677,x678,x679,x6710,x6711,x6712,x6713)+~P24(x671,x672,x673,x674,x675,x676,x677,x678,x679)+~P39(x671,x672,x673,x674,x675,x676,x677,x678,x679,x6710,x6711,x6712,x6713,x6714,x6715,x6716,x6717,x6718)+~P10(x671,x672,x673,x674,x675,x676,x677,x678,x679,x6710,x6711,x6712,x6713,x6714,x6715,x6716,x6717)+~P9(x671,x672,x673,x674,x675,x676,x677,x678,x679,x6710,x6711,x6712,x6713,x6714,x6715,x6716)+~P8(x671,x672,x673,x674,x675,x676,x677,x678,x679,x6710,x6711,x6712,x6713,x6714,x6715)+~P35(x671,x672,x673,x674,x675,x676,x677,x678,x679,x6710,x6711,x6712,x6713,x6714)+~P5(x671,x672,x673,x674,x675,x676,x677,x678,x679,x6710,x6711,x6712)+~P4(x671,x672,x673,x674,x675,x676,x677,x678,x679,x6710,x6711)+~P3(x671,x672,x673,x674,x675,x676,x677,x678,x679,x6710)+P29(x671,x672)+~P23(x671,x672,x673,x674,x675,x676,x677,x678)+~P21(x671,x672,x673,x674,x675,x676,x677)+~P19(x671,x672,x673,x674,x675,x676)+P16(x671,x672,x673,x674,x675)+~P1(a5000) % 7.50/7.60 [68]~P19(x681,x682,x683,x684,x685,x686)+~P8(x681,x682,x683,x684,x685,x686,x687,x688,x689,x6810,x6811,x6812,x6813,x6814,x6815)+~P7(x681,x682,x683,x684,x685,x686,x687,x688,x689,x6810,x6811,x6812,x6813,x6814)+~P6(x681,x682,x683,x684,x685,x686,x687,x688,x689,x6810,x6811,x6812,x6813)+~P5(x681,x682,x683,x684,x685,x686,x687,x688,x689,x6810,x6811,x6812)+~P4(x681,x682,x683,x684,x685,x686,x687,x688,x689,x6810,x6811)+~P3(x681,x682,x683,x684,x685,x686,x687,x688,x689,x6810)+~P24(x681,x682,x683,x684,x685,x686,x687,x688,x689)+~P23(x681,x682,x683,x684,x685,x686,x687,x688)+~P21(x681,x682,x683,x684,x685,x686,x687)+~P17(x681,x682,x683,x684,x685)+~P15(x681,x682,x683,x684)+~P14(x681,x682,x683)+~P29(x681,x682)+~P13(x681,x682)+~P2(x681)+~P39(x681,x682,x683,x684,x685,x686,x687,x688,x689,x6810,x6811,x6812,x6813,x6814,x6815,x6816,x6817,x6818)+~P10(x681,x682,x683,x684,x685,x686,x687,x688,x689,x6810,x6811,x6812,x6813,x6814,x6815,x6816,x6817)+P18(x681,x682,x683,x684,x685,x686)+~P9(x681,x682,x683,x684,x685,x686,x687,x688,x689,x6810,x6811,x6812,x6813,x6814,x6815,x6816)+P36(x681,x682,x683,x684,x685,x686,x687,x688,x689,x6810,x6811,x6812,x6813,x6814,x6815)+~P1(a5000) % 7.50/7.60 [69]~P8(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910,x6911,x6912,x6913,x6914,x6915)+~P33(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910,x6911,x6912)+~P23(x691,x692,x693,x694,x695,x696,x697,x698)+~P6(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910,x6911,x6912,x6913)+~P3(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910)+~P39(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910,x6911,x6912,x6913,x6914,x6915,x6916,x6917,x6918)+~P10(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910,x6911,x6912,x6913,x6914,x6915,x6916,x6917)+~P9(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910,x6911,x6912,x6913,x6914,x6915,x6916)+~P36(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910,x6911,x6912,x6913,x6914,x6915)+~P7(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910,x6911,x6912,x6913,x6914)+~P5(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910,x6911,x6912)+~P4(x691,x692,x693,x694,x695,x696,x697,x698,x699,x6910,x6911)+~P24(x691,x692,x693,x694,x695,x696,x697,x698,x699)+~P22(x691,x692,x693,x694,x695,x696,x697,x698)+~P21(x691,x692,x693,x694,x695,x696,x697)+~P19(x691,x692,x693,x694,x695,x696)+~P17(x691,x692,x693,x694,x695)+~P15(x691,x692,x693,x694)+~P14(x691,x692,x693)+~P13(x691,x692)+~P2(x691)+~P1(a5000) % 7.50/7.60 [70]~P21(x701,x702,x703,x704,x705,x706,x707)+~P8(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010,x7011,x7012,x7013,x7014,x7015)+~P7(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010,x7011,x7012,x7013,x7014)+~P6(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010,x7011,x7012,x7013)+~P5(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010,x7011,x7012)+~P4(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010,x7011)+~P3(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010)+~P24(x701,x702,x703,x704,x705,x706,x707,x708,x709)+~P23(x701,x702,x703,x704,x705,x706,x707,x708)+~P19(x701,x702,x703,x704,x705,x706)+~P17(x701,x702,x703,x704,x705)+~P15(x701,x702,x703,x704)+~P14(x701,x702,x703)+~P13(x701,x702)+~P2(x701)+~P39(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010,x7011,x7012,x7013,x7014,x7015,x7016,x7017,x7018)+~P10(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010,x7011,x7012,x7013,x7014,x7015,x7016,x7017)+~P9(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010,x7011,x7012,x7013,x7014,x7015,x7016)+P31(x701)+~P36(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010,x7011,x7012,x7013,x7014,x7015)+P35(x701,x702,x703,x704,x705,x706,x707,x708,x709,x7010,x7011,x7012,x7013,x7014)+~P1(a5000) % 7.50/7.60 [71]~P21(x711,x712,x713,x714,x715,x716,x717)+~P9(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110,x7111,x7112,x7113,x7114,x7115,x7116)+~P8(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110,x7111,x7112,x7113,x7114,x7115)+~P7(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110,x7111,x7112,x7113,x7114)+~P6(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110,x7111,x7112,x7113)+~P5(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110,x7111,x7112)+~P4(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110,x7111)+~P3(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110)+~P24(x711,x712,x713,x714,x715,x716,x717,x718,x719)+~P23(x711,x712,x713,x714,x715,x716,x717,x718)+~P19(x711,x712,x713,x714,x715,x716)+~P17(x711,x712,x713,x714,x715)+~P15(x711,x712,x713,x714)+~P30(x711,x712,x713)+~P14(x711,x712,x713)+~P13(x711,x712)+~P2(x711)+P34(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110,x7111,x7112,x7113)+~P39(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110,x7111,x7112,x7113,x7114,x7115,x7116,x7117,x7118)+~P10(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110,x7111,x7112,x7113,x7114,x7115,x7116,x7117)+P37(x711,x712,x713,x714,x715,x716,x717,x718,x719,x7110,x7111,x7112,x7113,x7114,x7115,x7116)+~P1(a5000) % 7.50/7.60 [73]~P21(x731,x732,x733,x734,x735,x736,x737)+~P11(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310,x7311,x7312,x7313,x7314,x7315,x7316,x7317,x7318)+~P10(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310,x7311,x7312,x7313,x7314,x7315,x7316,x7317)+~P9(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310,x7311,x7312,x7313,x7314,x7315,x7316)+~P8(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310,x7311,x7312,x7313,x7314,x7315)+~P7(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310,x7311,x7312,x7313,x7314)+~P6(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310,x7311,x7312,x7313)+~P5(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310,x7311,x7312)+~P4(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310,x7311)+~P3(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310)+~P24(x731,x732,x733,x734,x735,x736,x737,x738,x739)+~P23(x731,x732,x733,x734,x735,x736,x737,x738)+~P19(x731,x732,x733,x734,x735,x736)+~P17(x731,x732,x733,x734,x735)+~P15(x731,x732,x733,x734)+~P14(x731,x732,x733)+~P29(x731,x732)+~P13(x731,x732)+~P2(x731)+P20(x731,x732,x733,x734,x735,x736,x737)+P40(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310,x7311,x7312,x7313,x7314,x7315,x7316,x7317,x7318,x7319)+P37(x731,x732,x733,x734,x735,x736,x737,x738,x739,x7310,x7311,x7312,x7313,x7314,x7315,x7316)+~P1(a5000) % 7.50/7.60 [74]~P23(x741,x742,x743,x744,x745,x746,x747,x748)+~P11(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411,x7412,x7413,x7414,x7415,x7416,x7417,x7418)+~P10(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411,x7412,x7413,x7414,x7415,x7416,x7417)+~P9(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411,x7412,x7413,x7414,x7415,x7416)+~P8(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411,x7412,x7413,x7414,x7415)+~P7(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411,x7412,x7413,x7414)+~P6(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411,x7412,x7413)+~P34(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411,x7412,x7413)+~P5(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411,x7412)+~P4(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411)+~P3(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410)+~P24(x741,x742,x743,x744,x745,x746,x747,x748,x749)+~P21(x741,x742,x743,x744,x745,x746,x747)+~P19(x741,x742,x743,x744,x745,x746)+~P17(x741,x742,x743,x744,x745)+~P15(x741,x742,x743,x744)+~P14(x741,x742,x743)+~P13(x741,x742)+~P2(x741)+P30(x741,x742,x743)+P40(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411,x7412,x7413,x7414,x7415,x7416,x7417,x7418,x7419)+P37(x741,x742,x743,x744,x745,x746,x747,x748,x749,x7410,x7411,x7412,x7413,x7414,x7415,x7416)+~P1(a5000) % 7.50/7.60 [75]~P24(x751,x752,x753,x754,x755,x756,x757,x758,x759)+~P11(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511,x7512,x7513,x7514,x7515,x7516,x7517,x7518)+~P10(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511,x7512,x7513,x7514,x7515,x7516,x7517)+~P9(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511,x7512,x7513,x7514,x7515,x7516)+~P37(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511,x7512,x7513,x7514,x7515,x7516)+~P8(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511,x7512,x7513,x7514,x7515)+~P7(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511,x7512,x7513,x7514)+~P6(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511,x7512,x7513)+~P34(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511,x7512,x7513)+~P5(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511,x7512)+~P4(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511)+~P3(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510)+~P23(x751,x752,x753,x754,x755,x756,x757,x758)+~P21(x751,x752,x753,x754,x755,x756,x757)+~P19(x751,x752,x753,x754,x755,x756)+~P17(x751,x752,x753,x754,x755)+~P15(x751,x752,x753,x754)+~P30(x751,x752,x753)+~P14(x751,x752,x753)+~P13(x751,x752)+~P2(x751)+P40(x751,x752,x753,x754,x755,x756,x757,x758,x759,x7510,x7511,x7512,x7513,x7514,x7515,x7516,x7517,x7518,x7519)+~P1(a5000) % 7.50/7.60 [76]~P24(x761,x762,x763,x764,x765,x766,x767,x768,x769)+~P11(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611,x7612,x7613,x7614,x7615,x7616,x7617,x7618)+~P10(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611,x7612,x7613,x7614,x7615,x7616,x7617)+~P9(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611,x7612,x7613,x7614,x7615,x7616)+~P37(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611,x7612,x7613,x7614,x7615,x7616)+~P8(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611,x7612,x7613,x7614,x7615)+~P36(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611,x7612,x7613,x7614,x7615)+~P7(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611,x7612,x7613,x7614)+~P6(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611,x7612,x7613)+~P5(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611,x7612)+~P4(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611)+~P3(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610)+~P23(x761,x762,x763,x764,x765,x766,x767,x768)+~P21(x761,x762,x763,x764,x765,x766,x767)+~P19(x761,x762,x763,x764,x765,x766)+~P17(x761,x762,x763,x764,x765)+~P28(x761,x762,x763,x764)+~P15(x761,x762,x763,x764)+~P14(x761,x762,x763)+~P13(x761,x762)+~P2(x761)+P40(x761,x762,x763,x764,x765,x766,x767,x768,x769,x7610,x7611,x7612,x7613,x7614,x7615,x7616,x7617,x7618,x7619)+~P1(a5000) % 7.50/7.60 [77]~P3(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710)+~P11(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712,x7713,x7714,x7715,x7716,x7717,x7718)+~P38(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712,x7713,x7714,x7715,x7716,x7717)+~P10(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712,x7713,x7714,x7715,x7716,x7717)+~P9(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712,x7713,x7714,x7715,x7716)+~P8(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712,x7713,x7714,x7715)+~P7(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712,x7713,x7714)+~P35(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712,x7713,x7714)+~P6(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712,x7713)+~P34(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712,x7713)+~P5(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712)+~P4(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711)+~P24(x771,x772,x773,x774,x775,x776,x777,x778,x779)+~P23(x771,x772,x773,x774,x775,x776,x777,x778)+~P21(x771,x772,x773,x774,x775,x776,x777)+~P19(x771,x772,x773,x774,x775,x776)+~P17(x771,x772,x773,x774,x775)+~P15(x771,x772,x773,x774)+~P14(x771,x772,x773)+~P13(x771,x772)+~P2(x771)+P40(x771,x772,x773,x774,x775,x776,x777,x778,x779,x7710,x7711,x7712,x7713,x7714,x7715,x7716,x7717,x7718,x7719)+~P1(a5000) % 7.50/7.60 [78]~P2(x781)+~P13(x781,x782)+~P14(x781,x782,x783)+~P15(x781,x782,x783,x784)+~P17(x781,x782,x783,x784,x785)+~P23(x781,x782,x783,x784,x785,x786,x787,x788)+~P25(x781,x782,x783,x784,x785,x786,x787,x788,x789)+~P6(x781,x782,x783,x784,x785,x786,x787,x788,x789,x7810,x7811,x7812,x7813)+~P24(x781,x782,x783,x784,x785,x786,x787,x788,x789)+~P40(x781,x782,x783,x784,x785,x786,x787,x788,x789,x7810,x7811,x7812,x7813,x7814,x7815,x7816,x7817,x7818,x7819)+~P11(x781,x782,x783,x784,x785,x786,x787,x788,x789,x7810,x7811,x7812,x7813,x7814,x7815,x7816,x7817,x7818)+~P10(x781,x782,x783,x784,x785,x786,x787,x788,x789,x7810,x7811,x7812,x7813,x7814,x7815,x7816,x7817)+~P9(x781,x782,x783,x784,x785,x786,x787,x788,x789,x7810,x7811,x7812,x7813,x7814,x7815,x7816)+~P8(x781,x782,x783,x784,x785,x786,x787,x788,x789,x7810,x7811,x7812,x7813,x7814,x7815)+~P7(x781,x782,x783,x784,x785,x786,x787,x788,x789,x7810,x7811,x7812,x7813,x7814)+~P5(x781,x782,x783,x784,x785,x786,x787,x788,x789,x7810,x7811,x7812)+~P4(x781,x782,x783,x784,x785,x786,x787,x788,x789,x7810,x7811)+~P3(x781,x782,x783,x784,x785,x786,x787,x788,x789,x7810)+P16(x781,x782,x783,x784,x785)+~P22(x781,x782,x783,x784,x785,x786,x787,x788)+~P21(x781,x782,x783,x784,x785,x786,x787)+~P19(x781,x782,x783,x784,x785,x786)+~P1(a5000) % 7.50/7.60 [79]~P23(x791,x792,x793,x794,x795,x796,x797,x798)+~P9(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910,x7911,x7912,x7913,x7914,x7915,x7916)+~P8(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910,x7911,x7912,x7913,x7914,x7915)+~P7(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910,x7911,x7912,x7913,x7914)+~P6(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910,x7911,x7912,x7913)+~P5(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910,x7911,x7912)+~P4(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910,x7911)+~P26(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910)+~P3(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910)+~P24(x791,x792,x793,x794,x795,x796,x797,x798,x799)+~P21(x791,x792,x793,x794,x795,x796,x797)+~P19(x791,x792,x793,x794,x795,x796)+~P17(x791,x792,x793,x794,x795)+~P15(x791,x792,x793,x794)+~P14(x791,x792,x793)+~P13(x791,x792)+~P2(x791)+~P40(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910,x7911,x7912,x7913,x7914,x7915,x7916,x7917,x7918,x7919)+~P11(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910,x7911,x7912,x7913,x7914,x7915,x7916,x7917,x7918)+P22(x791,x792,x793,x794,x795,x796,x797,x798)+~P10(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910,x7911,x7912,x7913,x7914,x7915,x7916,x7917)+P37(x791,x792,x793,x794,x795,x796,x797,x798,x799,x7910,x7911,x7912,x7913,x7914,x7915,x7916)+~P1(a5000) % 7.50/7.60 [80]~P30(x801,x802,x803)+~P9(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011,x8012,x8013,x8014,x8015,x8016)+~P7(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011,x8012,x8013,x8014)+~P6(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011,x8012,x8013)+~P3(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010)+~P40(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011,x8012,x8013,x8014,x8015,x8016,x8017,x8018,x8019)+~P11(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011,x8012,x8013,x8014,x8015,x8016,x8017,x8018)+~P10(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011,x8012,x8013,x8014,x8015,x8016,x8017)+~P37(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011,x8012,x8013,x8014,x8015,x8016)+~P8(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011,x8012,x8013,x8014,x8015)+~P35(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011,x8012,x8013,x8014)+~P5(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011,x8012)+~P4(x801,x802,x803,x804,x805,x806,x807,x808,x809,x8010,x8011)+~P24(x801,x802,x803,x804,x805,x806,x807,x808,x809)+~P23(x801,x802,x803,x804,x805,x806,x807,x808)+~P21(x801,x802,x803,x804,x805,x806,x807)+~P19(x801,x802,x803,x804,x805,x806)+~P17(x801,x802,x803,x804,x805)+~P15(x801,x802,x803,x804)+~P14(x801,x802,x803)+~P13(x801,x802)+~P2(x801)+~P1(a5000) % 7.50/7.60 [81]~P24(x811,x812,x813,x814,x815,x816,x817,x818,x819)+~P12(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111,x8112,x8113,x8114,x8115,x8116,x8117,x8118,x8119)+~P11(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111,x8112,x8113,x8114,x8115,x8116,x8117,x8118)+~P10(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111,x8112,x8113,x8114,x8115,x8116,x8117)+~P9(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111,x8112,x8113,x8114,x8115,x8116)+~P8(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111,x8112,x8113,x8114,x8115)+~P36(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111,x8112,x8113,x8114,x8115)+~P7(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111,x8112,x8113,x8114)+~P6(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111,x8112,x8113)+~P5(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111,x8112)+~P4(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111)+~P3(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110)+~P23(x811,x812,x813,x814,x815,x816,x817,x818)+~P21(x811,x812,x813,x814,x815,x816,x817)+~P19(x811,x812,x813,x814,x815,x816)+~P17(x811,x812,x813,x814,x815)+~P15(x811,x812,x813,x814)+~P14(x811,x812,x813)+~P13(x811,x812)+~P2(x811)+P29(x811,x812)+P32(x811,x812,x813,x814,x815,x816,x817,x818,x819,x8110,x8111,x8112,x8113,x8114,x8115,x8116,x8117,x8118,x8119,x8120)+P16(x811,x812,x813,x814,x815)+~P1(a5000) % 7.50/7.60 [82]~P24(x821,x822,x823,x824,x825,x826,x827,x828,x829)+~P12(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211,x8212,x8213,x8214,x8215,x8216,x8217,x8218,x8219)+~P11(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211,x8212,x8213,x8214,x8215,x8216,x8217,x8218)+~P10(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211,x8212,x8213,x8214,x8215,x8216,x8217)+~P9(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211,x8212,x8213,x8214,x8215,x8216)+~P37(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211,x8212,x8213,x8214,x8215,x8216)+~P8(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211,x8212,x8213,x8214,x8215)+~P7(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211,x8212,x8213,x8214)+~P6(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211,x8212,x8213)+~P5(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211,x8212)+~P4(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211)+~P3(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210)+~P23(x821,x822,x823,x824,x825,x826,x827,x828)+~P21(x821,x822,x823,x824,x825,x826,x827)+~P19(x821,x822,x823,x824,x825,x826)+~P17(x821,x822,x823,x824,x825)+~P15(x821,x822,x823,x824)+~P14(x821,x822,x823)+~P13(x821,x822)+~P2(x821)+P29(x821,x822)+P32(x821,x822,x823,x824,x825,x826,x827,x828,x829,x8210,x8211,x8212,x8213,x8214,x8215,x8216,x8217,x8218,x8219,x8220)+P16(x821,x822,x823,x824,x825)+~P1(a5000) % 7.50/7.60 [83]~P7(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311,x8312,x8313,x8314)+~P6(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311,x8312,x8313)+~P2(x831)+~P13(x831,x832)+~P14(x831,x832,x833)+~P15(x831,x832,x833,x834)+~P17(x831,x832,x833,x834,x835)+~P19(x831,x832,x833,x834,x835,x836)+~P21(x831,x832,x833,x834,x835,x836,x837)+~P23(x831,x832,x833,x834,x835,x836,x837,x838)+~P24(x831,x832,x833,x834,x835,x836,x837,x838,x839)+~P3(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310)+~P4(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311)+~P5(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311,x8312)+~P10(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311,x8312,x8313,x8314,x8315,x8316,x8317)+~P32(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311,x8312,x8313,x8314,x8315,x8316,x8317,x8318,x8319,x8320)+~P11(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311,x8312,x8313,x8314,x8315,x8316,x8317,x8318)+~P12(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311,x8312,x8313,x8314,x8315,x8316,x8317,x8318,x8319)+P28(x831,x832,x833,x834)+~P9(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311,x8312,x8313,x8314,x8315,x8316)+~P8(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311,x8312,x8313,x8314,x8315)+P35(x831,x832,x833,x834,x835,x836,x837,x838,x839,x8310,x8311,x8312,x8313,x8314)+P16(x831,x832,x833,x834,x835)+~P1(a5000) % 7.50/7.60 [84]~P7(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412,x8413,x8414)+~P6(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412,x8413)+~P2(x841)+~P13(x841,x842)+~P29(x841,x842)+~P14(x841,x842,x843)+~P15(x841,x842,x843,x844)+~P17(x841,x842,x843,x844,x845)+~P19(x841,x842,x843,x844,x845,x846)+~P21(x841,x842,x843,x844,x845,x846,x847)+~P23(x841,x842,x843,x844,x845,x846,x847,x848)+~P24(x841,x842,x843,x844,x845,x846,x847,x848,x849)+~P3(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410)+~P4(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411)+~P5(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412)+P34(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412,x8413)+~P12(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412,x8413,x8414,x8415,x8416,x8417,x8418,x8419)+~P32(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412,x8413,x8414,x8415,x8416,x8417,x8418,x8419,x8420)+~P11(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412,x8413,x8414,x8415,x8416,x8417,x8418)+~P10(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412,x8413,x8414,x8415,x8416,x8417)+~P9(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412,x8413,x8414,x8415,x8416)+~P8(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412,x8413,x8414,x8415)+P35(x841,x842,x843,x844,x845,x846,x847,x848,x849,x8410,x8411,x8412,x8413,x8414)+~P1(a5000) % 7.50/7.60 [85]~P21(x851,x852,x853,x854,x855,x856,x857)+~P8(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511,x8512,x8513,x8514,x8515)+~P3(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510)+~P24(x851,x852,x853,x854,x855,x856,x857,x858,x859)+~P23(x851,x852,x853,x854,x855,x856,x857,x858)+~P20(x851,x852,x853,x854,x855,x856,x857)+~P19(x851,x852,x853,x854,x855,x856)+~P17(x851,x852,x853,x854,x855)+~P15(x851,x852,x853,x854)+~P14(x851,x852,x853)+~P13(x851,x852)+~P2(x851)+~P6(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511,x8512,x8513)+~P32(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511,x8512,x8513,x8514,x8515,x8516,x8517,x8518,x8519,x8520)+~P12(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511,x8512,x8513,x8514,x8515,x8516,x8517,x8518,x8519)+~P11(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511,x8512,x8513,x8514,x8515,x8516,x8517,x8518)+~P10(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511,x8512,x8513,x8514,x8515,x8516,x8517)+~P9(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511,x8512,x8513,x8514,x8515,x8516)+P26(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510)+~P36(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511,x8512,x8513,x8514,x8515)+~P7(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511,x8512,x8513,x8514)+~P5(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511,x8512)+~P4(x851,x852,x853,x854,x855,x856,x857,x858,x859,x8510,x8511)+~P1(a5000) % 7.50/7.61 [86]~P2(x861)+~P13(x861,x862)+~P29(x861,x862)+~P14(x861,x862,x863)+~P15(x861,x862,x863,x864)+~P17(x861,x862,x863,x864,x865)+~P19(x861,x862,x863,x864,x865,x866)+~P9(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611,x8612,x8613,x8614,x8615,x8616)+~P6(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611,x8612,x8613)+~P3(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610)+~P32(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611,x8612,x8613,x8614,x8615,x8616,x8617,x8618,x8619,x8620)+~P12(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611,x8612,x8613,x8614,x8615,x8616,x8617,x8618,x8619)+~P11(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611,x8612,x8613,x8614,x8615,x8616,x8617,x8618)+~P10(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611,x8612,x8613,x8614,x8615,x8616,x8617)+~P37(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611,x8612,x8613,x8614,x8615,x8616)+~P8(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611,x8612,x8613,x8614,x8615)+~P7(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611,x8612,x8613,x8614)+~P5(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611,x8612)+~P4(x861,x862,x863,x864,x865,x866,x867,x868,x869,x8610,x8611)+P18(x861,x862,x863,x864,x865,x866)+~P24(x861,x862,x863,x864,x865,x866,x867,x868,x869)+~P23(x861,x862,x863,x864,x865,x866,x867,x868)+~P21(x861,x862,x863,x864,x865,x866,x867)+~P1(a5000) % 7.50/7.61 cnf(87,plain, % 7.50/7.61 (P2(x871)), % 7.50/7.61 inference(scs_inference,[],[1,2])). % 7.50/7.61 cnf(88,plain, % 7.50/7.61 (P13(x881,x882)), % 7.50/7.61 inference(scs_inference,[],[1,2,3])). % 7.50/7.61 cnf(90,plain, % 7.50/7.61 (P14(x901,x902,x903)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4])). % 7.50/7.61 cnf(92,plain, % 7.50/7.61 (P15(x921,x922,x923,x924)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5])). % 7.50/7.61 cnf(94,plain, % 7.50/7.61 (P16(x941,x942,x943,x944,a1)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6])). % 7.50/7.61 cnf(96,plain, % 7.50/7.61 (~P16(x961,x962,x963,x964,a16)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8])). % 7.50/7.61 cnf(98,plain, % 7.50/7.61 (P17(x981,x982,x983,x984,x985)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7])). % 7.50/7.61 cnf(100,plain, % 7.50/7.61 (P18(x1001,x1002,x1003,x1004,x1005,a2)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9])). % 7.50/7.61 cnf(102,plain, % 7.50/7.61 (~P18(x1021,x1022,x1023,x1024,x1025,a15)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11])). % 7.50/7.61 cnf(104,plain, % 7.50/7.61 (P19(x1041,x1042,x1043,x1044,x1045,x1046)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10])). % 7.50/7.61 cnf(108,plain, % 7.50/7.61 (~P20(x1081,x1082,x1083,x1084,x1085,x1086,a14)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14])). % 7.50/7.61 cnf(110,plain, % 7.50/7.61 (P21(x1101,x1102,x1103,x1104,x1105,x1106,x1107)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13])). % 7.50/7.61 cnf(112,plain, % 7.50/7.61 (P22(x1121,x1122,x1123,x1124,x1125,x1126,x1127,a4)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16])). % 7.50/7.61 cnf(116,plain, % 7.50/7.61 (P23(x1161,x1162,x1163,x1164,x1165,x1166,x1167,x1168)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17])). % 7.50/7.61 cnf(118,plain, % 7.50/7.61 (P24(x1181,x1182,x1183,x1184,x1185,x1186,x1187,x1188,x1189)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20])). % 7.50/7.61 cnf(120,plain, % 7.50/7.61 (P3(x1201,x1202,x1203,x1204,x1205,x1206,x1207,x1208,x1209,x12010)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23])). % 7.50/7.61 cnf(122,plain, % 7.50/7.61 (P4(x1221,x1222,x1223,x1224,x1225,x1226,x1227,x1228,x1229,x12210,x12211)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26])). % 7.50/7.61 cnf(124,plain, % 7.50/7.61 (P5(x1241,x1242,x1243,x1244,x1245,x1246,x1247,x1248,x1249,x12410,x12411,x12412)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28])). % 7.50/7.61 cnf(126,plain, % 7.50/7.61 (P34(x1261,x1262,x1263,x1264,x1265,x1266,x1267,x1268,x1269,x12610,x12611,x12612,a5)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31])). % 7.50/7.61 cnf(128,plain, % 7.50/7.61 (~P34(x1281,x1282,x1283,x1284,x1285,x1286,x1287,x1288,x1289,x12810,x12811,x12812,a12)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31,34])). % 7.50/7.61 cnf(130,plain, % 7.50/7.61 (P6(x1301,x1302,x1303,x1304,x1305,x1306,x1307,x1308,x1309,x13010,x13011,x13012,x13013)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31,34,32])). % 7.50/7.61 cnf(132,plain, % 7.50/7.61 (P35(x1321,x1322,x1323,x1324,x1325,x1326,x1327,x1328,x1329,x13210,x13211,x13212,x13213,a6)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31,34,32,38])). % 7.50/7.61 cnf(134,plain, % 7.50/7.61 (~P35(x1341,x1342,x1343,x1344,x1345,x1346,x1347,x1348,x1349,x13410,x13411,x13412,x13413,a11)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31,34,32,38,40])). % 7.50/7.61 cnf(136,plain, % 7.50/7.61 (P7(x1361,x1362,x1363,x1364,x1365,x1366,x1367,x1368,x1369,x13610,x13611,x13612,x13613,x13614)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31,34,32,38,40,39])). % 7.50/7.61 cnf(140,plain, % 7.50/7.61 (~P36(x1401,x1402,x1403,x1404,x1405,x1406,x1407,x1408,x1409,x14010,x14011,x14012,x14013,x14014,a10)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31,34,32,38,40,39,42,46])). % 7.50/7.61 cnf(142,plain, % 7.50/7.61 (P8(x1421,x1422,x1423,x1424,x1425,x1426,x1427,x1428,x1429,x14210,x14211,x14212,x14213,x14214,x14215)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31,34,32,38,40,39,42,46,43])). % 7.50/7.61 cnf(146,plain, % 7.50/7.61 (~P37(x1461,x1462,x1463,x1464,x1465,x1466,x1467,x1468,x1469,x14610,x14611,x14612,x14613,x14614,x14615,a9)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31,34,32,38,40,39,42,46,43,48,54])). % 7.50/7.61 cnf(148,plain, % 7.50/7.61 (P9(x1481,x1482,x1483,x1484,x1485,x1486,x1487,x1488,x1489,x14810,x14811,x14812,x14813,x14814,x14815,x14816)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31,34,32,38,40,39,42,46,43,48,54,49])). % 7.50/7.61 cnf(158,plain, % 7.50/7.61 (P31(x1581)+P28(x1581,x1582,x1583,x1584)), % 7.50/7.61 inference(scs_inference,[],[1,2,3,4,5,6,8,7,9,11,10,12,14,13,16,18,17,20,23,26,28,31,34,32,38,40,39,42,46,43,48,54,49,55,64,72,15,19])). % 7.50/7.61 cnf(177,plain, % 7.50/7.61 (~P2(x1771)+~P13(x1771,x1772)+~P14(x1771,x1772,x1773)+~P15(x1771,x1772,x1773,x1774)+~P16(x1771,x1772,x1773,x1774,x1775)+~P18(x1771,x1772,x1773,x1774,x1775,x1776)+~P31(x1771)+~P17(x1771,x1772,x1773,x1774,x1775)+~P19(x1771,x1772,x1773,x1774,x1775,x1776)+~P21(x1771,x1772,x1773,x1774,x1775,x1776,x1777)+~P23(x1771,x1772,x1773,x1774,x1775,x1776,x1777,x1778)+~P25(x1771,x1772,x1773,x1774,x1775,x1776,x1777,x1778,x1779)), % 7.50/7.61 inference(scs_inference,[],[1,22])). % 7.50/7.61 cnf(178,plain, % 7.50/7.61 (~P31(x1781)+P18(x1781,x1782,x1783,x1784,x1785,x1786)+P20(x1781,x1782,x1783,x1784,x1785,x1786,x1787)+~P2(x1781)+~P13(x1781,x1782)+~P14(x1781,x1782,x1783)+~P15(x1781,x1782,x1783,x1784)+~P17(x1781,x1782,x1783,x1784,x1785)+~P19(x1781,x1782,x1783,x1784,x1785,x1786)+~P21(x1781,x1782,x1783,x1784,x1785,x1786,x1787)+~P23(x1781,x1782,x1783,x1784,x1785,x1786,x1787,x1788)+~P24(x1781,x1782,x1783,x1784,x1785,x1786,x1787,x1788,x1789)+~P26(x1781,x1782,x1783,x1784,x1785,x1786,x1787,x1788,x1789,x17810)), % 7.50/7.61 inference(scs_inference,[],[1,24])). % 7.50/7.61 cnf(180,plain, % 7.50/7.61 (~P31(x1801)+~P23(x1801,x1802,x1803,x1804,x1805,x1806,x1807,x1808)+P16(x1801,x1802,x1803,x1804,x1805)+~P2(x1801)+~P13(x1801,x1802)+~P14(x1801,x1802,x1803)+~P15(x1801,x1802,x1803,x1804)+~P17(x1801,x1802,x1803,x1804,x1805)+~P19(x1801,x1802,x1803,x1804,x1805,x1806)+~P21(x1801,x1802,x1803,x1804,x1805,x1806,x1807)+~P22(x1801,x1802,x1803,x1804,x1805,x1806,x1807,x1808)+~P24(x1801,x1802,x1803,x1804,x1805,x1806,x1807,x1808,x1809)+~P3(x1801,x1802,x1803,x1804,x1805,x1806,x1807,x1808,x1809,x18010)+P27(x1801,x1802,x1803,x1804,x1805,x1806,x1807,x1808,x1809,x18010,x18011)), % 7.50/7.61 inference(scs_inference,[],[1,27])). % 7.50/7.61 cnf(183,plain, % 7.50/7.61 (~P27(x1831,x1832,x1833,x1834,x1835,x1836,x1837,x1838,x1839,x18310,x18311)+~P4(x1831,x1832,x1833,x1834,x1835,x1836,x1837,x1838,x1839,x18310,x18311)+~P3(x1831,x1832,x1833,x1834,x1835,x1836,x1837,x1838,x1839,x18310)+~P24(x1831,x1832,x1833,x1834,x1835,x1836,x1837,x1838,x1839)+~P23(x1831,x1832,x1833,x1834,x1835,x1836,x1837,x1838)+~P21(x1831,x1832,x1833,x1834,x1835,x1836,x1837)+~P19(x1831,x1832,x1833,x1834,x1835,x1836)+~P15(x1831,x1832,x1833,x1834)+~P14(x1831,x1832,x1833)+~P13(x1831,x1832)+~P2(x1831)+P20(x1831,x1832,x1833,x1834,x1835,x1836,x1837)+P26(x1831,x1832,x1833,x1834,x1835,x1836,x1837,x1838,x1839,x18310)+P34(x1831,x1832,x1833,x1834,x1835,x1836,x1837,x1838,x1839,x18310,x18311,x18312,x18313)+~P17(x1831,x1832,x1833,x1834,x1835)+~P5(x1831,x1832,x1833,x1834,x1835,x1836,x1837,x1838,x1839,x18310,x18311,x18312)), % 7.50/7.61 inference(scs_inference,[],[1,33])). % 7.50/7.61 cnf(192,plain, % 7.50/7.61 (~P7(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928,x1929,x19210,x19211,x19212,x19213,x19214)+~P6(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928,x1929,x19210,x19211,x19212,x19213)+~P5(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928,x1929,x19210,x19211,x19212)+~P4(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928,x1929,x19210,x19211)+~P26(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928,x1929,x19210)+~P3(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928,x1929,x19210)+~P24(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928,x1929)+~P23(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928)+~P19(x1921,x1922,x1923,x1924,x1925,x1926)+~P17(x1921,x1922,x1923,x1924,x1925)+~P15(x1921,x1922,x1923,x1924)+~P14(x1921,x1922,x1923)+~P13(x1921,x1922)+~P2(x1921)+P31(x1921)+P35(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928,x1929,x19210,x19211,x19212,x19213,x19214)+~P21(x1921,x1922,x1923,x1924,x1925,x1926,x1927)+~P8(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928,x1929,x19210,x19211,x19212,x19213,x19214,x19215)+P37(x1921,x1922,x1923,x1924,x1925,x1926,x1927,x1928,x1929,x19210,x19211,x19212,x19213,x19214,x19215,x19216)), % 7.50/7.61 inference(scs_inference,[],[1,51])). % 7.50/7.61 cnf(193,plain, % 7.50/7.61 (~P7(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938,x1939,x19310,x19311,x19312,x19313,x19314)+~P35(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938,x1939,x19310,x19311,x19312,x19313,x19314)+~P6(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938,x1939,x19310,x19311,x19312,x19313)+~P5(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938,x1939,x19310,x19311,x19312)+~P4(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938,x1939,x19310,x19311)+~P3(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938,x1939,x19310)+~P24(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938,x1939)+~P23(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938)+~P19(x1931,x1932,x1933,x1934,x1935,x1936)+~P17(x1931,x1932,x1933,x1934,x1935)+~P15(x1931,x1932,x1933,x1934)+~P30(x1931,x1932,x1933)+~P14(x1931,x1932,x1933)+~P13(x1931,x1932)+~P2(x1931)+P26(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938,x1939,x19310)+~P21(x1931,x1932,x1933,x1934,x1935,x1936,x1937)+~P8(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938,x1939,x19310,x19311,x19312,x19313,x19314,x19315)+P37(x1931,x1932,x1933,x1934,x1935,x1936,x1937,x1938,x1939,x19310,x19311,x19312,x19313,x19314,x19315,x19316)), % 7.50/7.61 inference(scs_inference,[],[1,52])). % 7.50/7.61 cnf(198,plain, % 7.50/7.61 (~P8(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988,x1989,x19810,x19811,x19812,x19813,x19814,x19815)+~P7(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988,x1989,x19810,x19811,x19812,x19813,x19814)+~P6(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988,x1989,x19810,x19811,x19812,x19813)+~P5(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988,x1989,x19810,x19811,x19812)+~P4(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988,x1989,x19810,x19811)+~P3(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988,x1989,x19810)+~P24(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988,x1989)+~P23(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988)+~P22(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988)+~P19(x1981,x1982,x1983,x1984,x1985,x1986)+~P17(x1981,x1982,x1983,x1984,x1985)+~P15(x1981,x1982,x1983,x1984)+~P14(x1981,x1982,x1983)+~P13(x1981,x1982)+~P2(x1981)+P30(x1981,x1982,x1983)+P36(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988,x1989,x19810,x19811,x19812,x19813,x19814,x19815)+~P21(x1981,x1982,x1983,x1984,x1985,x1986,x1987)+~P9(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988,x1989,x19810,x19811,x19812,x19813,x19814,x19815,x19816)+P38(x1981,x1982,x1983,x1984,x1985,x1986,x1987,x1988,x1989,x19810,x19811,x19812,x19813,x19814,x19815,x19816,x19817)), % 7.50/7.61 inference(scs_inference,[],[1,59])). % 7.50/7.61 cnf(200,plain, % 7.50/7.61 (~P6(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009,x20010,x20011,x20012,x20013)+~P34(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009,x20010,x20011,x20012,x20013)+~P5(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009,x20010,x20011,x20012)+~P4(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009,x20010,x20011)+~P3(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009,x20010)+~P24(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009)+~P23(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008)+~P19(x2001,x2002,x2003,x2004,x2005,x2006)+~P17(x2001,x2002,x2003,x2004,x2005)+~P28(x2001,x2002,x2003,x2004)+~P15(x2001,x2002,x2003,x2004)+~P14(x2001,x2002,x2003)+~P13(x2001,x2002)+~P2(x2001)+P35(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009,x20010,x20011,x20012,x20013,x20014)+~P8(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009,x20010,x20011,x20012,x20013,x20014,x20015)+~P21(x2001,x2002,x2003,x2004,x2005,x2006,x2007)+~P7(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009,x20010,x20011,x20012,x20013,x20014)+~P9(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009,x20010,x20011,x20012,x20013,x20014,x20015,x20016)+~P38(x2001,x2002,x2003,x2004,x2005,x2006,x2007,x2008,x2009,x20010,x20011,x20012,x20013,x20014,x20015,x20016,x20017)), % 7.50/7.61 inference(scs_inference,[],[1,61])). % 7.50/7.61 cnf(3768,plain, % 7.50/7.61 (P6(x37681,x37682,x37683,x37684,x37685,x37686,x37687,x37688,x37689,x376810,x376811,x376812,x376813)), % 7.50/7.61 inference(rename_variables,[],[130])). % 7.50/7.61 cnf(3769,plain, % 7.50/7.61 (P5(x37691,x37692,x37693,x37694,x37695,x37696,x37697,x37698,x37699,x376910,x376911,x376912)), % 7.50/7.61 inference(rename_variables,[],[124])). % 7.50/7.61 cnf(3770,plain, % 7.50/7.61 (P4(x37701,x37702,x37703,x37704,x37705,x37706,x37707,x37708,x37709,x377010,x377011)), % 7.50/7.61 inference(rename_variables,[],[122])). % 7.50/7.61 cnf(3771,plain, % 7.50/7.61 (P3(x37711,x37712,x37713,x37714,x37715,x37716,x37717,x37718,x37719,x377110)), % 7.50/7.61 inference(rename_variables,[],[120])). % 7.50/7.61 cnf(3772,plain, % 7.50/7.61 (P24(x37721,x37722,x37723,x37724,x37725,x37726,x37727,x37728,x37729)), % 7.50/7.61 inference(rename_variables,[],[118])). % 7.50/7.61 cnf(3773,plain, % 7.50/7.61 (P23(x37731,x37732,x37733,x37734,x37735,x37736,x37737,x37738)), % 7.50/7.61 inference(rename_variables,[],[116])). % 7.50/7.61 cnf(3774,plain, % 7.50/7.61 (P19(x37741,x37742,x37743,x37744,x37745,x37746)), % 7.50/7.61 inference(rename_variables,[],[104])). % 7.50/7.61 cnf(3775,plain, % 7.50/7.61 (P17(x37751,x37752,x37753,x37754,x37755)), % 7.50/7.61 inference(rename_variables,[],[98])). % 7.50/7.61 cnf(3776,plain, % 7.50/7.61 (P15(x37761,x37762,x37763,x37764)), % 7.50/7.61 inference(rename_variables,[],[92])). % 7.50/7.61 cnf(3777,plain, % 7.50/7.61 (P14(x37771,x37772,x37773)), % 7.50/7.61 inference(rename_variables,[],[90])). % 7.50/7.61 cnf(3778,plain, % 7.50/7.61 (P13(x37781,x37782)), % 7.50/7.61 inference(rename_variables,[],[88])). % 7.50/7.61 cnf(3779,plain, % 7.50/7.61 (P2(x37791)), % 7.50/7.61 inference(rename_variables,[],[87])). % 7.50/7.61 cnf(3780,plain, % 7.50/7.61 (~P35(x37801,x37802,x37803,x37804,x37805,x37806,x37807,x37808,x37809,x378010,x378011,x378012,x378013,a11)), % 7.50/7.61 inference(rename_variables,[],[134])). % 7.50/7.61 cnf(3781,plain, % 7.50/7.61 (P21(x37811,x37812,x37813,x37814,x37815,x37816,x37817)), % 7.50/7.61 inference(rename_variables,[],[110])). % 7.50/7.61 cnf(3782,plain, % 7.50/7.61 (P7(x37821,x37822,x37823,x37824,x37825,x37826,x37827,x37828,x37829,x378210,x378211,x378212,x378213,x378214)), % 7.50/7.61 inference(rename_variables,[],[136])). % 7.50/7.61 cnf(3783,plain, % 7.50/7.61 (P8(x37831,x37832,x37833,x37834,x37835,x37836,x37837,x37838,x37839,x378310,x378311,x378312,x378313,x378314,x378315)), % 7.50/7.61 inference(rename_variables,[],[142])). % 7.50/7.61 cnf(3784,plain, % 7.50/7.61 (~P37(x37841,x37842,x37843,x37844,x37845,x37846,x37847,x37848,x37849,x378410,x378411,x378412,x378413,x378414,x378415,a9)), % 7.50/7.61 inference(rename_variables,[],[146])). % 7.50/7.61 cnf(3788,plain, % 7.50/7.61 (P6(x37881,x37882,x37883,x37884,x37885,x37886,x37887,x37888,x37889,x378810,x378811,x378812,x378813)), % 7.50/7.61 inference(rename_variables,[],[130])). % 7.50/7.61 cnf(3789,plain, % 7.50/7.61 (P5(x37891,x37892,x37893,x37894,x37895,x37896,x37897,x37898,x37899,x378910,x378911,x378912)), % 7.50/7.61 inference(rename_variables,[],[124])). % 7.50/7.61 cnf(3790,plain, % 7.50/7.61 (P4(x37901,x37902,x37903,x37904,x37905,x37906,x37907,x37908,x37909,x379010,x379011)), % 7.50/7.61 inference(rename_variables,[],[122])). % 7.50/7.61 cnf(3791,plain, % 7.50/7.61 (P3(x37911,x37912,x37913,x37914,x37915,x37916,x37917,x37918,x37919,x379110)), % 7.50/7.61 inference(rename_variables,[],[120])). % 7.50/7.61 cnf(3792,plain, % 7.50/7.61 (P24(x37921,x37922,x37923,x37924,x37925,x37926,x37927,x37928,x37929)), % 7.50/7.61 inference(rename_variables,[],[118])). % 7.50/7.61 cnf(3793,plain, % 7.50/7.61 (P23(x37931,x37932,x37933,x37934,x37935,x37936,x37937,x37938)), % 7.50/7.61 inference(rename_variables,[],[116])). % 7.50/7.61 cnf(3794,plain, % 7.50/7.61 (P19(x37941,x37942,x37943,x37944,x37945,x37946)), % 7.50/7.61 inference(rename_variables,[],[104])). % 7.50/7.61 cnf(3795,plain, % 7.50/7.61 (P17(x37951,x37952,x37953,x37954,x37955)), % 7.50/7.61 inference(rename_variables,[],[98])). % 7.50/7.61 cnf(3796,plain, % 7.50/7.61 (P15(x37961,x37962,x37963,x37964)), % 7.50/7.61 inference(rename_variables,[],[92])). % 7.50/7.61 cnf(3797,plain, % 7.50/7.61 (P14(x37971,x37972,x37973)), % 7.50/7.61 inference(rename_variables,[],[90])). % 7.50/7.61 cnf(3798,plain, % 7.50/7.61 (P13(x37981,x37982)), % 7.50/7.61 inference(rename_variables,[],[88])). % 7.50/7.61 cnf(3799,plain, % 7.50/7.61 (P2(x37991)), % 7.50/7.61 inference(rename_variables,[],[87])). % 7.50/7.61 cnf(3800,plain, % 7.50/7.61 (P21(x38001,x38002,x38003,x38004,x38005,x38006,x38007)), % 7.50/7.61 inference(rename_variables,[],[110])). % 7.50/7.61 cnf(3801,plain, % 7.50/7.61 (P7(x38011,x38012,x38013,x38014,x38015,x38016,x38017,x38018,x38019,x380110,x380111,x380112,x380113,x380114)), % 7.50/7.61 inference(rename_variables,[],[136])). % 7.50/7.61 cnf(3802,plain, % 7.50/7.61 (P8(x38021,x38022,x38023,x38024,x38025,x38026,x38027,x38028,x38029,x380210,x380211,x380212,x380213,x380214,x380215)), % 7.50/7.61 inference(rename_variables,[],[142])). % 7.50/7.61 cnf(3806,plain, % 7.50/7.61 (P7(x38061,x38062,x38063,x38064,x38065,x38066,x38067,x38068,x38069,x380610,x380611,x380612,x380613,x380614)), % 7.50/7.61 inference(rename_variables,[],[136])). % 7.50/7.61 cnf(3807,plain, % 7.50/7.61 (P6(x38071,x38072,x38073,x38074,x38075,x38076,x38077,x38078,x38079,x380710,x380711,x380712,x380713)), % 7.50/7.61 inference(rename_variables,[],[130])). % 7.50/7.61 cnf(3808,plain, % 7.50/7.61 (P5(x38081,x38082,x38083,x38084,x38085,x38086,x38087,x38088,x38089,x380810,x380811,x380812)), % 7.50/7.61 inference(rename_variables,[],[124])). % 7.50/7.61 cnf(3809,plain, % 7.50/7.61 (P4(x38091,x38092,x38093,x38094,x38095,x38096,x38097,x38098,x38099,x380910,x380911)), % 7.50/7.61 inference(rename_variables,[],[122])). % 7.50/7.61 cnf(3810,plain, % 7.50/7.61 (P3(x38101,x38102,x38103,x38104,x38105,x38106,x38107,x38108,x38109,x381010)), % 7.50/7.61 inference(rename_variables,[],[120])). % 7.50/7.61 cnf(3811,plain, % 7.50/7.61 (P24(x38111,x38112,x38113,x38114,x38115,x38116,x38117,x38118,x38119)), % 7.50/7.61 inference(rename_variables,[],[118])). % 7.50/7.61 cnf(3812,plain, % 7.50/7.61 (P23(x38121,x38122,x38123,x38124,x38125,x38126,x38127,x38128)), % 7.50/7.61 inference(rename_variables,[],[116])). % 7.50/7.61 cnf(3814,plain, % 7.50/7.61 (P19(x38141,x38142,x38143,x38144,x38145,x38146)), % 7.50/7.61 inference(rename_variables,[],[104])). % 7.50/7.61 cnf(3815,plain, % 7.50/7.61 (P17(x38151,x38152,x38153,x38154,x38155)), % 7.50/7.61 inference(rename_variables,[],[98])). % 7.50/7.61 cnf(3816,plain, % 7.50/7.61 (P15(x38161,x38162,x38163,x38164)), % 7.50/7.61 inference(rename_variables,[],[92])). % 7.50/7.61 cnf(3817,plain, % 7.50/7.61 (P14(x38171,x38172,x38173)), % 7.50/7.61 inference(rename_variables,[],[90])). % 7.50/7.61 cnf(3818,plain, % 7.50/7.61 (P13(x38181,x38182)), % 7.50/7.61 inference(rename_variables,[],[88])). % 7.50/7.61 cnf(3819,plain, % 7.50/7.61 (P2(x38191)), % 7.50/7.61 inference(rename_variables,[],[87])). % 7.50/7.61 cnf(3821,plain, % 7.50/7.61 (P21(x38211,x38212,x38213,x38214,x38215,x38216,x38217)), % 7.50/7.61 inference(rename_variables,[],[110])). % 7.50/7.61 cnf(3822,plain, % 7.50/7.61 (P8(x38221,x38222,x38223,x38224,x38225,x38226,x38227,x38228,x38229,x382210,x382211,x382212,x382213,x382214,x382215)), % 7.50/7.61 inference(rename_variables,[],[142])). % 7.50/7.61 cnf(3823,plain, % 7.50/7.61 (P9(x38231,x38232,x38233,x38234,x38235,x38236,x38237,x38238,x38239,x382310,x382311,x382312,x382313,x382314,x382315,x382316)), % 7.50/7.61 inference(rename_variables,[],[148])). % 7.50/7.61 cnf(3825,plain, % 7.50/7.61 (~P28(x38251,x38252,x38253,x38254)+P31(x38251)), % 7.50/7.61 inference(scs_inference,[],[87,3779,3799,3819,130,3768,3788,3807,122,3770,3790,3809,132,140,148,3823,134,3780,88,3778,3798,3818,90,3777,3797,3817,92,3776,3796,3816,98,3775,3795,3815,104,3774,3794,3814,110,3781,3800,3821,116,3773,3793,3812,118,3772,3792,3811,120,3771,3791,3810,124,3769,3789,3808,136,3782,3801,3806,142,3783,3802,3822,146,3784,126,112,192,193,198,200])). % 7.50/7.61 cnf(8588,plain, % 7.50/7.61 (P31(x85881)), % 7.50/7.61 inference(scs_inference,[],[158,3825])). % 7.50/7.61 cnf(8590,plain, % 7.50/7.61 (P31(x85901)), % 7.50/7.61 inference(rename_variables,[],[8588])). % 7.50/7.61 cnf(8591,plain, % 7.50/7.61 (P17(x85911,x85912,x85913,x85914,x85915)), % 7.50/7.61 inference(rename_variables,[],[98])). % 7.50/7.61 cnf(8592,plain, % 7.50/7.61 (P19(x85921,x85922,x85923,x85924,x85925,x85926)), % 7.50/7.61 inference(rename_variables,[],[104])). % 7.50/7.61 cnf(8593,plain, % 7.50/7.61 (P2(x85931)), % 7.50/7.61 inference(rename_variables,[],[87])). % 7.50/7.61 cnf(8594,plain, % 7.50/7.61 (P13(x85941,x85942)), % 7.50/7.61 inference(rename_variables,[],[88])). % 7.50/7.61 cnf(8595,plain, % 7.50/7.61 (P14(x85951,x85952,x85953)), % 7.50/7.61 inference(rename_variables,[],[90])). % 7.50/7.61 cnf(8596,plain, % 7.50/7.61 (P15(x85961,x85962,x85963,x85964)), % 7.50/7.61 inference(rename_variables,[],[92])). % 7.50/7.61 cnf(8599,plain, % 7.50/7.61 (P21(x85991,x85992,x85993,x85994,x85995,x85996,x85997)), % 7.50/7.61 inference(rename_variables,[],[110])). % 7.50/7.61 cnf(8600,plain, % 7.50/7.61 (P23(x86001,x86002,x86003,x86004,x86005,x86006,x86007,x86008)), % 7.50/7.61 inference(rename_variables,[],[116])). % 7.50/7.61 cnf(8603,plain, % 7.50/7.61 (P2(x86031)), % 7.50/7.61 inference(rename_variables,[],[87])). % 7.50/7.61 cnf(8604,plain, % 7.50/7.61 (P13(x86041,x86042)), % 7.50/7.61 inference(rename_variables,[],[88])). % 7.50/7.61 cnf(8605,plain, % 7.50/7.61 (P14(x86051,x86052,x86053)), % 7.50/7.61 inference(rename_variables,[],[90])). % 7.50/7.61 cnf(8606,plain, % 7.50/7.61 (P15(x86061,x86062,x86063,x86064)), % 7.50/7.61 inference(rename_variables,[],[92])). % 7.50/7.61 cnf(8607,plain, % 7.50/7.61 (P17(x86071,x86072,x86073,x86074,x86075)), % 7.50/7.61 inference(rename_variables,[],[98])). % 7.50/7.62 cnf(8608,plain, % 7.50/7.62 (P19(x86081,x86082,x86083,x86084,x86085,x86086)), % 7.50/7.62 inference(rename_variables,[],[104])). % 7.50/7.62 cnf(8609,plain, % 7.50/7.62 (P21(x86091,x86092,x86093,x86094,x86095,x86096,x86097)), % 7.50/7.62 inference(rename_variables,[],[110])). % 7.50/7.62 cnf(8610,plain, % 7.50/7.62 (P31(x86101)), % 7.50/7.62 inference(rename_variables,[],[8588])). % 7.50/7.62 cnf(8612,plain, % 7.50/7.62 (~P20(x86121,x86122,x86123,x86124,x86125,x86126,a14)), % 7.50/7.62 inference(rename_variables,[],[108])). % 7.50/7.62 cnf(8613,plain, % 7.50/7.62 (P23(x86131,x86132,x86133,x86134,x86135,x86136,x86137,x86138)), % 7.50/7.62 inference(rename_variables,[],[116])). % 7.50/7.62 cnf(8614,plain, % 7.50/7.62 (P24(x86141,x86142,x86143,x86144,x86145,x86146,x86147,x86148,x86149)), % 7.50/7.62 inference(rename_variables,[],[118])). % 7.50/7.62 cnf(8618,plain, % 7.50/7.62 (P2(x86181)), % 7.50/7.62 inference(rename_variables,[],[87])). % 7.50/7.62 cnf(8619,plain, % 7.50/7.62 (P13(x86191,x86192)), % 7.50/7.62 inference(rename_variables,[],[88])). % 7.50/7.62 cnf(8620,plain, % 7.50/7.62 (P14(x86201,x86202,x86203)), % 7.50/7.62 inference(rename_variables,[],[90])). % 7.50/7.62 cnf(8621,plain, % 7.50/7.62 (P15(x86211,x86212,x86213,x86214)), % 7.50/7.62 inference(rename_variables,[],[92])). % 7.50/7.62 cnf(8622,plain, % 7.50/7.62 (P17(x86221,x86222,x86223,x86224,x86225)), % 7.50/7.62 inference(rename_variables,[],[98])). % 7.50/7.62 cnf(8623,plain, % 7.50/7.62 (P19(x86231,x86232,x86233,x86234,x86235,x86236)), % 7.50/7.62 inference(rename_variables,[],[104])). % 7.50/7.62 cnf(8624,plain, % 7.50/7.62 (P21(x86241,x86242,x86243,x86244,x86245,x86246,x86247)), % 7.50/7.62 inference(rename_variables,[],[110])). % 7.50/7.62 cnf(8627,plain, % 7.50/7.62 (P23(x86271,x86272,x86273,x86274,x86275,x86276,x86277,x86278)), % 7.50/7.62 inference(rename_variables,[],[116])). % 7.50/7.62 cnf(8628,plain, % 7.50/7.62 (P24(x86281,x86282,x86283,x86284,x86285,x86286,x86287,x86288,x86289)), % 7.50/7.62 inference(rename_variables,[],[118])). % 7.50/7.62 cnf(8629,plain, % 7.50/7.62 (P3(x86291,x86292,x86293,x86294,x86295,x86296,x86297,x86298,x86299,x862910)), % 7.50/7.62 inference(rename_variables,[],[120])). % 7.50/7.62 cnf(8631,plain, % 7.50/7.62 ($false), % 7.50/7.62 inference(scs_inference,[],[124,87,8593,8603,8618,122,96,116,8600,8613,8627,118,8614,8628,8588,8590,8610,100,102,108,8612,94,112,128,88,8594,8604,8619,90,8595,8605,8620,92,8596,8606,8621,98,8591,8607,8622,104,8592,8608,8623,110,8599,8609,8624,120,8629,177,178,180,183]), % 7.50/7.62 ['proof']). % 7.50/7.62 % SZS output end Proof % 7.50/7.62 % Total time : 6.770000 s %------------------------------------------------------------------------------