%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO653-1 : TPTP v7.5.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Mar 29 01:05:47 EDT 2022 % Result : Unsatisfiable 56.13s 56.19s % Output : CNFRefutation 56.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYO653-1 : TPTP v7.5.0. Released v7.3.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n016.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 : Mon Mar 14 14:12:49 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.44 openjdk version "1.8.0_171" % 0.18/0.44 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.18/0.44 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.18/0.45 file=/export/starexec/sandbox/benchmark/theBenchmark.p % 0.62/0.66 start to proof:theBenchmark % 56.13/56.19 % Version : CSE-F---1.0 % 56.13/56.19 % Problem : theBenchmark.p % 56.13/56.19 % Proof found % 56.13/56.19 % SZS status Theorem for theBenchmark.p % 56.13/56.19 % SZS output start Proof % 56.13/56.19 [2]~P1(f1(a4),a2) % 56.13/56.19 [1]P1(f1(x11),f3(a2)) % 56.13/56.19 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2) % 56.13/56.19 [4]P1(f1(x41),a2)+~P1(f1(f5(x41)),f3(a2))+P2(a2,f1(f5(x41))) % 56.13/56.19 [6]P1(f1(x61),a2)+~P1(f1(f5(f5(x61))),f3(a2))+P2(a2,f1(f5(f5(x61)))) % 56.13/56.19 [7]P1(f1(x71),a2)+~P1(f1(f5(f5(f5(x71)))),f3(a2))+P2(a2,f1(f5(f5(f5(x71))))) % 56.13/56.19 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+P2(f1(x51),f1(f5(x51)))+~P2(a2,f1(f5(x51))) % 56.13/56.19 [8]P3(f5(x81),f5(x81))+~P2(a2,f1(x81))+~P2(f1(x81),f1(f5(x81)))+P2(f1(x81),f1(f5(f5(x81))))+~P2(a2,f1(f5(x81)))+~P2(a2,f1(f5(f5(x81)))) % 56.13/56.19 [9]P3(f5(x91),f5(x91))+~P2(a2,f1(x91))+~P2(f1(x91),f1(f5(x91)))+~P2(f1(x91),f1(f5(f5(x91))))+~P2(a2,f1(f5(x91)))+~P2(a2,f1(f5(f5(x91))))+~P2(a2,f1(f5(f5(f5(x91))))) % 56.13/56.19 [10]~P3(f5(x101),f5(x104))+~P3(f5(x103),f5(x102))+~P3(f5(x104),f5(x103))+P2(f1(x101),f1(f5(x101)))+P2(f1(x102),f1(f5(x102)))+~P2(a2,f1(x101))+P2(f1(x103),f1(f5(x103)))+P2(f1(x104),f1(f5(x104)))+~P2(a2,f1(x102))+~P2(a2,f1(x103))+~P2(a2,f1(x104))+~P2(a2,f1(f5(x101)))+~P2(a2,f1(f5(x102)))+~P2(a2,f1(f5(x103)))+~P2(a2,f1(f5(x104))) % 56.13/56.19 [11]~P3(f5(x114),f5(x113))+~P3(f5(x113),f5(x112))+~P3(f5(x111),f5(x114))+P2(f1(x111),f1(f5(x111)))+P2(f1(x112),f1(f5(x112)))+~P2(a2,f1(x111))+P2(f1(x113),f1(f5(x113)))+~P2(a2,f1(x112))+~P2(f1(x114),f1(f5(x114)))+~P2(a2,f1(x113))+~P2(a2,f1(x114))+~P2(a2,f1(f5(x111)))+~P2(a2,f1(f5(x112)))+~P2(a2,f1(f5(x113)))+~P2(a2,f1(f5(x114)))+P2(f1(x114),f1(f5(f5(x114))))+~P2(a2,f1(f5(f5(x114)))) % 56.13/56.19 [12]~P3(f5(x123),f5(x124))+~P3(f5(x124),f5(x122))+~P3(f5(x121),f5(x123))+P2(f1(x121),f1(f5(x121)))+P2(f1(x122),f1(f5(x122)))+~P2(a2,f1(x121))+P2(f1(x123),f1(f5(x123)))+~P2(a2,f1(x122))+~P2(f1(x124),f1(f5(x124)))+~P2(a2,f1(x123))+~P2(a2,f1(x124))+~P2(a2,f1(f5(x121)))+~P2(a2,f1(f5(x122)))+~P2(a2,f1(f5(x124)))+~P2(a2,f1(f5(x123)))+P2(f1(x124),f1(f5(f5(x124))))+~P2(a2,f1(f5(f5(x124)))) % 56.13/56.19 [13]~P3(f5(x133),f5(x132))+~P3(f5(x132),f5(x134))+~P3(f5(x131),f5(x133))+P2(f1(x131),f1(f5(x131)))+P2(f1(x132),f1(f5(x132)))+~P2(a2,f1(x131))+P2(f1(x133),f1(f5(x133)))+~P2(a2,f1(x132))+~P2(f1(x134),f1(f5(x134)))+~P2(a2,f1(x133))+~P2(a2,f1(x134))+~P2(a2,f1(f5(x131)))+~P2(a2,f1(f5(x134)))+~P2(a2,f1(f5(x132)))+~P2(a2,f1(f5(x133)))+P2(f1(x134),f1(f5(f5(x134))))+~P2(a2,f1(f5(f5(x134)))) % 56.13/56.19 [14]~P3(f5(x143),f5(x142))+~P3(f5(x142),f5(x141))+~P3(f5(x144),f5(x143))+P2(f1(x141),f1(f5(x141)))+P2(f1(x142),f1(f5(x142)))+~P2(a2,f1(x141))+P2(f1(x143),f1(f5(x143)))+~P2(a2,f1(x142))+~P2(f1(x144),f1(f5(x144)))+~P2(a2,f1(x143))+~P2(a2,f1(x144))+~P2(a2,f1(f5(x144)))+~P2(a2,f1(f5(x141)))+~P2(a2,f1(f5(x142)))+~P2(a2,f1(f5(x143)))+P2(f1(x144),f1(f5(f5(x144))))+~P2(a2,f1(f5(f5(x144)))) % 56.13/56.19 [21]~P3(f5(x214),f5(x213))+~P3(f5(x213),f5(x212))+~P3(f5(x211),f5(x214))+P2(f1(x211),f1(f5(x211)))+P2(f1(x212),f1(f5(x212)))+~P2(a2,f1(x211))+P2(f1(x213),f1(f5(x213)))+~P2(a2,f1(x212))+~P2(f1(x214),f1(f5(x214)))+~P2(a2,f1(x213))+~P2(a2,f1(x214))+~P2(a2,f1(f5(x211)))+~P2(a2,f1(f5(x212)))+~P2(a2,f1(f5(x213)))+~P2(a2,f1(f5(x214)))+~P2(f1(x214),f1(f5(f5(x214))))+~P2(a2,f1(f5(f5(x214))))+~P2(a2,f1(f5(f5(f5(x214))))) % 56.13/56.19 [22]~P3(f5(x224),f5(x223))+~P3(f5(x223),f5(x222))+~P3(f5(x222),f5(x221))+P2(f1(x221),f1(f5(x221)))+P2(f1(x222),f1(f5(x222)))+~P2(a2,f1(x221))+P2(f1(x223),f1(f5(x223)))+~P2(a2,f1(x222))+~P2(f1(x224),f1(f5(x224)))+~P2(a2,f1(x223))+~P2(a2,f1(x224))+~P2(a2,f1(f5(x221)))+~P2(a2,f1(f5(x222)))+~P2(a2,f1(f5(x223)))+~P2(a2,f1(f5(x224)))+~P2(f1(x224),f1(f5(f5(x224))))+~P2(a2,f1(f5(f5(x224))))+~P2(a2,f1(f5(f5(f5(x224))))) % 56.13/56.19 [23]~P3(f5(x233),f5(x234))+~P3(f5(x234),f5(x232))+~P3(f5(x231),f5(x233))+P2(f1(x231),f1(f5(x231)))+P2(f1(x232),f1(f5(x232)))+~P2(a2,f1(x231))+P2(f1(x233),f1(f5(x233)))+~P2(a2,f1(x232))+~P2(f1(x234),f1(f5(x234)))+~P2(a2,f1(x233))+~P2(a2,f1(x234))+~P2(a2,f1(f5(x231)))+~P2(a2,f1(f5(x232)))+~P2(a2,f1(f5(x234)))+~P2(a2,f1(f5(x233)))+~P2(f1(x234),f1(f5(f5(x234))))+~P2(a2,f1(f5(f5(x234))))+~P2(a2,f1(f5(f5(f5(x234))))) % 56.13/56.19 [24]~P3(f5(x243),f5(x242))+~P3(f5(x242),f5(x244))+~P3(f5(x241),f5(x243))+P2(f1(x241),f1(f5(x241)))+P2(f1(x242),f1(f5(x242)))+~P2(a2,f1(x241))+P2(f1(x243),f1(f5(x243)))+~P2(a2,f1(x242))+~P2(f1(x244),f1(f5(x244)))+~P2(a2,f1(x243))+~P2(a2,f1(x244))+~P2(a2,f1(f5(x241)))+~P2(a2,f1(f5(x244)))+~P2(a2,f1(f5(x242)))+~P2(a2,f1(f5(x243)))+~P2(f1(x244),f1(f5(f5(x244))))+~P2(a2,f1(f5(f5(x244))))+~P2(a2,f1(f5(f5(f5(x244))))) % 56.13/56.19 [15]~P3(f5(x154),f5(x153))+~P3(f5(x153),f5(x152))+~P3(f5(x151),f5(x154))+P2(f1(x151),f1(f5(x151)))+P2(f1(x152),f1(f5(x152)))+~P2(a2,f1(x151))+~P2(f1(x153),f1(f5(x153)))+~P2(a2,f1(x152))+~P2(f1(x154),f1(f5(x154)))+~P2(a2,f1(x153))+~P2(a2,f1(x154))+~P2(a2,f1(f5(x151)))+~P2(a2,f1(f5(x152)))+~P2(a2,f1(f5(x153)))+~P2(a2,f1(f5(x154)))+P2(f1(x153),f1(f5(f5(x153))))+P2(f1(x154),f1(f5(f5(x154))))+~P2(a2,f1(f5(f5(x153))))+~P2(a2,f1(f5(f5(x154)))) % 56.13/56.19 [16]~P3(f5(x164),f5(x162))+~P3(f5(x162),f5(x163))+~P3(f5(x161),f5(x164))+P2(f1(x161),f1(f5(x161)))+P2(f1(x162),f1(f5(x162)))+~P2(a2,f1(x161))+~P2(f1(x163),f1(f5(x163)))+~P2(a2,f1(x162))+~P2(f1(x164),f1(f5(x164)))+~P2(a2,f1(x163))+~P2(a2,f1(x164))+~P2(a2,f1(f5(x161)))+~P2(a2,f1(f5(x163)))+~P2(a2,f1(f5(x162)))+~P2(a2,f1(f5(x164)))+P2(f1(x163),f1(f5(f5(x163))))+P2(f1(x164),f1(f5(f5(x164))))+~P2(a2,f1(f5(f5(x163))))+~P2(a2,f1(f5(f5(x164)))) % 56.13/56.19 [17]~P3(f5(x172),f5(x174))+~P3(f5(x174),f5(x173))+~P3(f5(x171),f5(x172))+P2(f1(x171),f1(f5(x171)))+P2(f1(x172),f1(f5(x172)))+~P2(a2,f1(x171))+~P2(f1(x173),f1(f5(x173)))+~P2(a2,f1(x172))+~P2(f1(x174),f1(f5(x174)))+~P2(a2,f1(x173))+~P2(a2,f1(x174))+~P2(a2,f1(f5(x171)))+~P2(a2,f1(f5(x173)))+~P2(a2,f1(f5(x174)))+~P2(a2,f1(f5(x172)))+P2(f1(x173),f1(f5(f5(x173))))+P2(f1(x174),f1(f5(f5(x174))))+~P2(a2,f1(f5(f5(x173))))+~P2(a2,f1(f5(f5(x174)))) % 56.13/56.19 [18]~P3(f5(x184),f5(x182))+~P3(f5(x182),f5(x181))+~P3(f5(x183),f5(x184))+P2(f1(x181),f1(f5(x181)))+P2(f1(x182),f1(f5(x182)))+~P2(a2,f1(x181))+~P2(f1(x183),f1(f5(x183)))+~P2(a2,f1(x182))+~P2(f1(x184),f1(f5(x184)))+~P2(a2,f1(x183))+~P2(a2,f1(x184))+~P2(a2,f1(f5(x183)))+~P2(a2,f1(f5(x181)))+~P2(a2,f1(f5(x182)))+~P2(a2,f1(f5(x184)))+P2(f1(x183),f1(f5(f5(x183))))+P2(f1(x184),f1(f5(f5(x184))))+~P2(a2,f1(f5(f5(x183))))+~P2(a2,f1(f5(f5(x184)))) % 56.13/56.19 [19]~P3(f5(x192),f5(x194))+~P3(f5(x194),f5(x191))+~P3(f5(x193),f5(x192))+P2(f1(x191),f1(f5(x191)))+P2(f1(x192),f1(f5(x192)))+~P2(a2,f1(x191))+~P2(f1(x193),f1(f5(x193)))+~P2(a2,f1(x192))+~P2(f1(x194),f1(f5(x194)))+~P2(a2,f1(x193))+~P2(a2,f1(x194))+~P2(a2,f1(f5(x193)))+~P2(a2,f1(f5(x191)))+~P2(a2,f1(f5(x194)))+~P2(a2,f1(f5(x192)))+P2(f1(x193),f1(f5(f5(x193))))+P2(f1(x194),f1(f5(f5(x194))))+~P2(a2,f1(f5(f5(x193))))+~P2(a2,f1(f5(f5(x194)))) % 56.13/56.19 [20]~P3(f5(x202),f5(x201))+~P3(f5(x201),f5(x204))+~P3(f5(x203),f5(x202))+P2(f1(x201),f1(f5(x201)))+P2(f1(x202),f1(f5(x202)))+~P2(a2,f1(x201))+~P2(f1(x203),f1(f5(x203)))+~P2(a2,f1(x202))+~P2(f1(x204),f1(f5(x204)))+~P2(a2,f1(x203))+~P2(a2,f1(x204))+~P2(a2,f1(f5(x203)))+~P2(a2,f1(f5(x204)))+~P2(a2,f1(f5(x201)))+~P2(a2,f1(f5(x202)))+P2(f1(x203),f1(f5(f5(x203))))+P2(f1(x204),f1(f5(f5(x204))))+~P2(a2,f1(f5(f5(x203))))+~P2(a2,f1(f5(f5(x204)))) % 56.13/56.19 [29]~P3(f5(x291),f5(x294))+~P3(f5(x293),f5(x292))+~P3(f5(x294),f5(x293))+P2(f1(x291),f1(f5(x291)))+P2(f1(x292),f1(f5(x292)))+~P2(a2,f1(x291))+~P2(f1(x293),f1(f5(x293)))+~P2(f1(x294),f1(f5(x294)))+~P2(a2,f1(x292))+~P2(a2,f1(x293))+~P2(a2,f1(x294))+~P2(a2,f1(f5(x291)))+~P2(a2,f1(f5(x294)))+~P2(a2,f1(f5(x293)))+~P2(a2,f1(f5(x292)))+P2(f1(x293),f1(f5(f5(x293))))+~P2(f1(x294),f1(f5(f5(x294))))+~P2(a2,f1(f5(f5(x293))))+~P2(a2,f1(f5(f5(x294))))+~P2(a2,f1(f5(f5(f5(x294))))) % 56.13/56.19 [30]~P3(f5(x302),f5(x301))+~P3(f5(x303),f5(x302))+~P3(f5(x304),f5(x303))+P2(f1(x301),f1(f5(x301)))+P2(f1(x302),f1(f5(x302)))+~P2(a2,f1(x301))+~P2(f1(x303),f1(f5(x303)))+~P2(f1(x304),f1(f5(x304)))+~P2(a2,f1(x302))+~P2(a2,f1(x303))+~P2(a2,f1(x304))+~P2(a2,f1(f5(x301)))+~P2(a2,f1(f5(x304)))+~P2(a2,f1(f5(x303)))+~P2(a2,f1(f5(x302)))+P2(f1(x303),f1(f5(f5(x303))))+~P2(f1(x304),f1(f5(f5(x304))))+~P2(a2,f1(f5(f5(x303))))+~P2(a2,f1(f5(f5(x304))))+~P2(a2,f1(f5(f5(f5(x304))))) % 56.13/56.19 [31]~P3(f5(x311),f5(x313))+~P3(f5(x314),f5(x312))+~P3(f5(x313),f5(x314))+P2(f1(x311),f1(f5(x311)))+P2(f1(x312),f1(f5(x312)))+~P2(a2,f1(x311))+~P2(f1(x313),f1(f5(x313)))+~P2(a2,f1(x312))+~P2(f1(x314),f1(f5(x314)))+~P2(a2,f1(x313))+~P2(a2,f1(x314))+~P2(a2,f1(f5(x311)))+~P2(a2,f1(f5(x313)))+~P2(a2,f1(f5(x314)))+~P2(a2,f1(f5(x312)))+P2(f1(x313),f1(f5(f5(x313))))+~P2(f1(x314),f1(f5(f5(x314))))+~P2(a2,f1(f5(f5(x314))))+~P2(a2,f1(f5(f5(x313))))+~P2(a2,f1(f5(f5(f5(x314))))) % 56.13/56.19 [32]~P3(f5(x321),f5(x324))+~P3(f5(x322),f5(x323))+~P3(f5(x324),f5(x322))+P2(f1(x321),f1(f5(x321)))+P2(f1(x322),f1(f5(x322)))+~P2(a2,f1(x321))+~P2(f1(x323),f1(f5(x323)))+~P2(f1(x324),f1(f5(x324)))+~P2(a2,f1(x322))+~P2(a2,f1(x323))+~P2(a2,f1(x324))+~P2(a2,f1(f5(x321)))+~P2(a2,f1(f5(x324)))+~P2(a2,f1(f5(x322)))+~P2(a2,f1(f5(x323)))+P2(f1(x323),f1(f5(f5(x323))))+~P2(f1(x324),f1(f5(f5(x324))))+~P2(a2,f1(f5(f5(x323))))+~P2(a2,f1(f5(f5(x324))))+~P2(a2,f1(f5(f5(f5(x324))))) % 56.13/56.19 [33]~P3(f5(x333),f5(x331))+~P3(f5(x332),f5(x333))+~P3(f5(x334),f5(x332))+P2(f1(x331),f1(f5(x331)))+P2(f1(x332),f1(f5(x332)))+~P2(a2,f1(x331))+~P2(f1(x333),f1(f5(x333)))+~P2(f1(x334),f1(f5(x334)))+~P2(a2,f1(x332))+~P2(a2,f1(x333))+~P2(a2,f1(x334))+~P2(a2,f1(f5(x331)))+~P2(a2,f1(f5(x334)))+~P2(a2,f1(f5(x332)))+~P2(a2,f1(f5(x333)))+P2(f1(x333),f1(f5(f5(x333))))+~P2(f1(x334),f1(f5(f5(x334))))+~P2(a2,f1(f5(f5(x333))))+~P2(a2,f1(f5(f5(x334))))+~P2(a2,f1(f5(f5(f5(x334))))) % 56.13/56.19 [34]~P3(f5(x341),f5(x343))+~P3(f5(x342),f5(x344))+~P3(f5(x343),f5(x342))+P2(f1(x341),f1(f5(x341)))+P2(f1(x342),f1(f5(x342)))+~P2(a2,f1(x341))+~P2(f1(x343),f1(f5(x343)))+~P2(a2,f1(x342))+~P2(f1(x344),f1(f5(x344)))+~P2(a2,f1(x343))+~P2(a2,f1(x344))+~P2(a2,f1(f5(x341)))+~P2(a2,f1(f5(x343)))+~P2(a2,f1(f5(x342)))+~P2(a2,f1(f5(x344)))+P2(f1(x343),f1(f5(f5(x343))))+~P2(f1(x344),f1(f5(f5(x344))))+~P2(a2,f1(f5(f5(x344))))+~P2(a2,f1(f5(f5(x343))))+~P2(a2,f1(f5(f5(f5(x344))))) % 56.13/56.19 [35]~P3(f5(x351),f5(x352))+~P3(f5(x354),f5(x353))+~P3(f5(x352),f5(x354))+P2(f1(x351),f1(f5(x351)))+P2(f1(x352),f1(f5(x352)))+~P2(a2,f1(x351))+~P2(f1(x353),f1(f5(x353)))+~P2(f1(x354),f1(f5(x354)))+~P2(a2,f1(x352))+~P2(a2,f1(x353))+~P2(a2,f1(x354))+~P2(a2,f1(f5(x351)))+~P2(a2,f1(f5(x352)))+~P2(a2,f1(f5(x354)))+~P2(a2,f1(f5(x353)))+P2(f1(x353),f1(f5(f5(x353))))+~P2(f1(x354),f1(f5(f5(x354))))+~P2(a2,f1(f5(f5(x353))))+~P2(a2,f1(f5(f5(x354))))+~P2(a2,f1(f5(f5(f5(x354))))) % 56.17/56.19 [36]~P3(f5(x361),f5(x362))+~P3(f5(x363),f5(x364))+~P3(f5(x362),f5(x363))+P2(f1(x361),f1(f5(x361)))+P2(f1(x362),f1(f5(x362)))+~P2(a2,f1(x361))+~P2(f1(x363),f1(f5(x363)))+~P2(a2,f1(x362))+~P2(f1(x364),f1(f5(x364)))+~P2(a2,f1(x363))+~P2(a2,f1(x364))+~P2(a2,f1(f5(x361)))+~P2(a2,f1(f5(x362)))+~P2(a2,f1(f5(x363)))+~P2(a2,f1(f5(x364)))+P2(f1(x363),f1(f5(f5(x363))))+~P2(f1(x364),f1(f5(f5(x364))))+~P2(a2,f1(f5(f5(x364))))+~P2(a2,f1(f5(f5(x363))))+~P2(a2,f1(f5(f5(f5(x364))))) % 56.17/56.19 [37]~P3(f5(x373),f5(x374))+~P3(f5(x372),f5(x371))+~P3(f5(x374),f5(x372))+P2(f1(x371),f1(f5(x371)))+P2(f1(x372),f1(f5(x372)))+~P2(a2,f1(x371))+~P2(f1(x373),f1(f5(x373)))+~P2(f1(x374),f1(f5(x374)))+~P2(a2,f1(x372))+~P2(a2,f1(x373))+~P2(a2,f1(x374))+~P2(a2,f1(f5(x373)))+~P2(a2,f1(f5(x374)))+~P2(a2,f1(f5(x372)))+~P2(a2,f1(f5(x371)))+P2(f1(x373),f1(f5(f5(x373))))+~P2(f1(x374),f1(f5(f5(x374))))+~P2(a2,f1(f5(f5(x373))))+~P2(a2,f1(f5(f5(x374))))+~P2(a2,f1(f5(f5(f5(x374))))) % 56.17/56.19 [38]~P3(f5(x381),f5(x383))+~P3(f5(x382),f5(x381))+~P3(f5(x384),f5(x382))+P2(f1(x381),f1(f5(x381)))+P2(f1(x382),f1(f5(x382)))+~P2(a2,f1(x381))+~P2(f1(x383),f1(f5(x383)))+~P2(f1(x384),f1(f5(x384)))+~P2(a2,f1(x382))+~P2(a2,f1(x383))+~P2(a2,f1(x384))+~P2(a2,f1(f5(x383)))+~P2(a2,f1(f5(x384)))+~P2(a2,f1(f5(x382)))+~P2(a2,f1(f5(x381)))+P2(f1(x383),f1(f5(f5(x383))))+~P2(f1(x384),f1(f5(f5(x384))))+~P2(a2,f1(f5(f5(x383))))+~P2(a2,f1(f5(f5(x384))))+~P2(a2,f1(f5(f5(f5(x384))))) % 56.17/56.19 [39]~P3(f5(x393),f5(x392))+~P3(f5(x394),f5(x391))+~P3(f5(x392),f5(x394))+P2(f1(x391),f1(f5(x391)))+P2(f1(x392),f1(f5(x392)))+~P2(a2,f1(x391))+~P2(f1(x393),f1(f5(x393)))+~P2(f1(x394),f1(f5(x394)))+~P2(a2,f1(x392))+~P2(a2,f1(x393))+~P2(a2,f1(x394))+~P2(a2,f1(f5(x393)))+~P2(a2,f1(f5(x392)))+~P2(a2,f1(f5(x394)))+~P2(a2,f1(f5(x391)))+P2(f1(x393),f1(f5(f5(x393))))+~P2(f1(x394),f1(f5(f5(x394))))+~P2(a2,f1(f5(f5(x393))))+~P2(a2,f1(f5(f5(x394))))+~P2(a2,f1(f5(f5(f5(x394))))) % 56.17/56.19 [40]~P3(f5(x403),f5(x402))+~P3(f5(x401),f5(x404))+~P3(f5(x402),f5(x401))+P2(f1(x401),f1(f5(x401)))+P2(f1(x402),f1(f5(x402)))+~P2(a2,f1(x401))+~P2(f1(x403),f1(f5(x403)))+~P2(f1(x404),f1(f5(x404)))+~P2(a2,f1(x402))+~P2(a2,f1(x403))+~P2(a2,f1(x404))+~P2(a2,f1(f5(x403)))+~P2(a2,f1(f5(x402)))+~P2(a2,f1(f5(x401)))+~P2(a2,f1(f5(x404)))+P2(f1(x403),f1(f5(f5(x403))))+~P2(f1(x404),f1(f5(f5(x404))))+~P2(a2,f1(f5(f5(x403))))+~P2(a2,f1(f5(f5(x404))))+~P2(a2,f1(f5(f5(f5(x404))))) % 56.17/56.19 [25]~P3(f5(x251),f5(x254))+~P3(f5(x253),f5(x252))+~P3(f5(x254),f5(x253))+P2(f1(x251),f1(f5(x251)))+~P2(a2,f1(x251))+~P2(f1(x252),f1(f5(x252)))+~P2(f1(x253),f1(f5(x253)))+~P2(f1(x254),f1(f5(x254)))+~P2(a2,f1(x252))+~P2(a2,f1(x253))+~P2(a2,f1(x254))+~P2(a2,f1(f5(x251)))+~P2(a2,f1(f5(x252)))+~P2(a2,f1(f5(x253)))+~P2(a2,f1(f5(x254)))+P2(f1(x252),f1(f5(f5(x252))))+P2(f1(x253),f1(f5(f5(x253))))+P2(f1(x254),f1(f5(f5(x254))))+~P2(a2,f1(f5(f5(x252))))+~P2(a2,f1(f5(f5(x253))))+~P2(a2,f1(f5(f5(x254)))) % 56.17/56.19 [26]~P3(f5(x262),f5(x264))+~P3(f5(x263),f5(x261))+~P3(f5(x264),f5(x263))+P2(f1(x261),f1(f5(x261)))+~P2(a2,f1(x261))+~P2(f1(x262),f1(f5(x262)))+~P2(f1(x263),f1(f5(x263)))+~P2(f1(x264),f1(f5(x264)))+~P2(a2,f1(x262))+~P2(a2,f1(x263))+~P2(a2,f1(x264))+~P2(a2,f1(f5(x262)))+~P2(a2,f1(f5(x261)))+~P2(a2,f1(f5(x263)))+~P2(a2,f1(f5(x264)))+P2(f1(x262),f1(f5(f5(x262))))+P2(f1(x263),f1(f5(f5(x263))))+P2(f1(x264),f1(f5(f5(x264))))+~P2(a2,f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(x263))))+~P2(a2,f1(f5(f5(x264)))) % 56.17/56.19 [27]~P3(f5(x272),f5(x274))+~P3(f5(x271),f5(x273))+~P3(f5(x274),f5(x271))+P2(f1(x271),f1(f5(x271)))+~P2(a2,f1(x271))+~P2(f1(x272),f1(f5(x272)))+~P2(f1(x273),f1(f5(x273)))+~P2(f1(x274),f1(f5(x274)))+~P2(a2,f1(x272))+~P2(a2,f1(x273))+~P2(a2,f1(x274))+~P2(a2,f1(f5(x272)))+~P2(a2,f1(f5(x273)))+~P2(a2,f1(f5(x271)))+~P2(a2,f1(f5(x274)))+P2(f1(x272),f1(f5(f5(x272))))+P2(f1(x273),f1(f5(f5(x273))))+P2(f1(x274),f1(f5(f5(x274))))+~P2(a2,f1(f5(f5(x272))))+~P2(a2,f1(f5(f5(x273))))+~P2(a2,f1(f5(f5(x274)))) % 56.17/56.19 [28]~P3(f5(x282),f5(x281))+~P3(f5(x284),f5(x283))+~P3(f5(x281),f5(x284))+P2(f1(x281),f1(f5(x281)))+~P2(a2,f1(x281))+~P2(f1(x282),f1(f5(x282)))+~P2(f1(x283),f1(f5(x283)))+~P2(f1(x284),f1(f5(x284)))+~P2(a2,f1(x282))+~P2(a2,f1(x283))+~P2(a2,f1(x284))+~P2(a2,f1(f5(x282)))+~P2(a2,f1(f5(x283)))+~P2(a2,f1(f5(x284)))+~P2(a2,f1(f5(x281)))+P2(f1(x282),f1(f5(f5(x282))))+P2(f1(x283),f1(f5(f5(x283))))+P2(f1(x284),f1(f5(f5(x284))))+~P2(a2,f1(f5(f5(x282))))+~P2(a2,f1(f5(f5(x283))))+~P2(a2,f1(f5(f5(x284)))) % 56.17/56.19 [54]~P3(f5(x541),f5(x544))+~P3(f5(x543),f5(x542))+~P3(f5(x544),f5(x543))+P2(f1(x541),f1(f5(x541)))+P2(f1(x542),f1(f5(x542)))+~P2(a2,f1(x541))+~P2(f1(x543),f1(f5(x543)))+~P2(a2,f1(x542))+~P2(f1(x544),f1(f5(x544)))+~P2(a2,f1(x543))+~P2(a2,f1(x544))+~P2(a2,f1(f5(x542)))+~P2(a2,f1(f5(x544)))+~P2(a2,f1(f5(x543)))+~P2(a2,f1(f5(x541)))+~P2(f1(x543),f1(f5(f5(x543))))+~P2(f1(x544),f1(f5(f5(x544))))+~P2(a2,f1(f5(f5(x543))))+~P2(a2,f1(f5(f5(x544))))+~P2(a2,f1(f5(f5(f5(x543)))))+~P2(a2,f1(f5(f5(f5(x544))))) % 56.17/56.19 [55]~P3(f5(x552),f5(x551))+~P3(f5(x553),f5(x552))+~P3(f5(x554),f5(x553))+P2(f1(x551),f1(f5(x551)))+P2(f1(x552),f1(f5(x552)))+~P2(a2,f1(x551))+~P2(f1(x553),f1(f5(x553)))+~P2(a2,f1(x552))+~P2(f1(x554),f1(f5(x554)))+~P2(a2,f1(x553))+~P2(a2,f1(x554))+~P2(a2,f1(f5(x552)))+~P2(a2,f1(f5(x554)))+~P2(a2,f1(f5(x553)))+~P2(a2,f1(f5(x551)))+~P2(f1(x553),f1(f5(f5(x553))))+~P2(f1(x554),f1(f5(f5(x554))))+~P2(a2,f1(f5(f5(x553))))+~P2(a2,f1(f5(f5(x554))))+~P2(a2,f1(f5(f5(f5(x553)))))+~P2(a2,f1(f5(f5(f5(x554))))) % 56.17/56.19 [56]~P3(f5(x561),f5(x564))+~P3(f5(x562),f5(x563))+~P3(f5(x564),f5(x562))+P2(f1(x561),f1(f5(x561)))+P2(f1(x562),f1(f5(x562)))+~P2(a2,f1(x561))+~P2(f1(x563),f1(f5(x563)))+~P2(a2,f1(x562))+~P2(f1(x564),f1(f5(x564)))+~P2(a2,f1(x563))+~P2(a2,f1(x564))+~P2(a2,f1(f5(x563)))+~P2(a2,f1(f5(x564)))+~P2(a2,f1(f5(x562)))+~P2(a2,f1(f5(x561)))+~P2(f1(x563),f1(f5(f5(x563))))+~P2(f1(x564),f1(f5(f5(x564))))+~P2(a2,f1(f5(f5(x563))))+~P2(a2,f1(f5(f5(x564))))+~P2(a2,f1(f5(f5(f5(x563)))))+~P2(a2,f1(f5(f5(f5(x564))))) % 56.17/56.19 [57]~P3(f5(x573),f5(x571))+~P3(f5(x572),f5(x573))+~P3(f5(x574),f5(x572))+P2(f1(x571),f1(f5(x571)))+P2(f1(x572),f1(f5(x572)))+~P2(a2,f1(x571))+~P2(f1(x573),f1(f5(x573)))+~P2(a2,f1(x572))+~P2(f1(x574),f1(f5(x574)))+~P2(a2,f1(x573))+~P2(a2,f1(x574))+~P2(a2,f1(f5(x573)))+~P2(a2,f1(f5(x574)))+~P2(a2,f1(f5(x572)))+~P2(a2,f1(f5(x571)))+~P2(f1(x573),f1(f5(f5(x573))))+~P2(f1(x574),f1(f5(f5(x574))))+~P2(a2,f1(f5(f5(x573))))+~P2(a2,f1(f5(f5(x574))))+~P2(a2,f1(f5(f5(f5(x573)))))+~P2(a2,f1(f5(f5(f5(x574))))) % 56.17/56.19 [58]~P3(f5(x581),f5(x582))+~P3(f5(x584),f5(x583))+~P3(f5(x582),f5(x584))+P2(f1(x581),f1(f5(x581)))+P2(f1(x582),f1(f5(x582)))+~P2(a2,f1(x581))+~P2(f1(x583),f1(f5(x583)))+~P2(a2,f1(x582))+~P2(f1(x584),f1(f5(x584)))+~P2(a2,f1(x583))+~P2(a2,f1(x584))+~P2(a2,f1(f5(x583)))+~P2(a2,f1(f5(x582)))+~P2(a2,f1(f5(x584)))+~P2(a2,f1(f5(x581)))+~P2(f1(x583),f1(f5(f5(x583))))+~P2(f1(x584),f1(f5(f5(x584))))+~P2(a2,f1(f5(f5(x583))))+~P2(a2,f1(f5(f5(x584))))+~P2(a2,f1(f5(f5(f5(x583)))))+~P2(a2,f1(f5(f5(f5(x584))))) % 56.17/56.19 [59]~P3(f5(x591),f5(x593))+~P3(f5(x592),f5(x591))+~P3(f5(x594),f5(x592))+P2(f1(x591),f1(f5(x591)))+P2(f1(x592),f1(f5(x592)))+~P2(a2,f1(x591))+~P2(f1(x593),f1(f5(x593)))+~P2(a2,f1(x592))+~P2(f1(x594),f1(f5(x594)))+~P2(a2,f1(x593))+~P2(a2,f1(x594))+~P2(a2,f1(f5(x591)))+~P2(a2,f1(f5(x594)))+~P2(a2,f1(f5(x592)))+~P2(a2,f1(f5(x593)))+~P2(f1(x593),f1(f5(f5(x593))))+~P2(f1(x594),f1(f5(f5(x594))))+~P2(a2,f1(f5(f5(x593))))+~P2(a2,f1(f5(f5(x594))))+~P2(a2,f1(f5(f5(f5(x593)))))+~P2(a2,f1(f5(f5(f5(x594))))) % 56.17/56.19 [42]~P3(f5(x421),f5(x424))+~P3(f5(x423),f5(x422))+~P3(f5(x424),f5(x423))+P2(f1(x421),f1(f5(x421)))+~P2(a2,f1(x421))+~P2(f1(x422),f1(f5(x422)))+~P2(f1(x423),f1(f5(x423)))+~P2(f1(x424),f1(f5(x424)))+~P2(a2,f1(x422))+~P2(a2,f1(x423))+~P2(a2,f1(x424))+~P2(a2,f1(f5(x421)))+~P2(a2,f1(f5(x422)))+~P2(a2,f1(f5(x423)))+~P2(a2,f1(f5(x424)))+P2(f1(x422),f1(f5(f5(x422))))+P2(f1(x423),f1(f5(f5(x423))))+~P2(f1(x424),f1(f5(f5(x424))))+~P2(a2,f1(f5(f5(x422))))+~P2(a2,f1(f5(f5(x423))))+~P2(a2,f1(f5(f5(x424))))+~P2(a2,f1(f5(f5(f5(x424))))) % 56.17/56.19 [43]~P3(f5(x432),f5(x431))+~P3(f5(x433),f5(x432))+~P3(f5(x434),f5(x433))+P2(f1(x431),f1(f5(x431)))+~P2(a2,f1(x431))+~P2(f1(x432),f1(f5(x432)))+~P2(f1(x433),f1(f5(x433)))+~P2(f1(x434),f1(f5(x434)))+~P2(a2,f1(x432))+~P2(a2,f1(x433))+~P2(a2,f1(x434))+~P2(a2,f1(f5(x431)))+~P2(a2,f1(f5(x432)))+~P2(a2,f1(f5(x433)))+~P2(a2,f1(f5(x434)))+P2(f1(x432),f1(f5(f5(x432))))+P2(f1(x433),f1(f5(f5(x433))))+~P2(f1(x434),f1(f5(f5(x434))))+~P2(a2,f1(f5(f5(x432))))+~P2(a2,f1(f5(f5(x433))))+~P2(a2,f1(f5(f5(x434))))+~P2(a2,f1(f5(f5(f5(x434))))) % 56.17/56.19 [44]~P3(f5(x441),f5(x443))+~P3(f5(x444),f5(x442))+~P3(f5(x443),f5(x444))+P2(f1(x441),f1(f5(x441)))+~P2(a2,f1(x441))+~P2(f1(x442),f1(f5(x442)))+~P2(f1(x443),f1(f5(x443)))+~P2(a2,f1(x442))+~P2(f1(x444),f1(f5(x444)))+~P2(a2,f1(x443))+~P2(a2,f1(x444))+~P2(a2,f1(f5(x441)))+~P2(a2,f1(f5(x442)))+~P2(a2,f1(f5(x444)))+~P2(a2,f1(f5(x443)))+P2(f1(x442),f1(f5(f5(x442))))+P2(f1(x443),f1(f5(f5(x443))))+~P2(f1(x444),f1(f5(f5(x444))))+~P2(a2,f1(f5(f5(x442))))+~P2(a2,f1(f5(f5(x444))))+~P2(a2,f1(f5(f5(x443))))+~P2(a2,f1(f5(f5(f5(x444))))) % 56.17/56.19 [45]~P3(f5(x451),f5(x453))+~P3(f5(x452),f5(x454))+~P3(f5(x453),f5(x452))+P2(f1(x451),f1(f5(x451)))+~P2(a2,f1(x451))+~P2(f1(x452),f1(f5(x452)))+~P2(f1(x453),f1(f5(x453)))+~P2(a2,f1(x452))+~P2(f1(x454),f1(f5(x454)))+~P2(a2,f1(x453))+~P2(a2,f1(x454))+~P2(a2,f1(f5(x451)))+~P2(a2,f1(f5(x454)))+~P2(a2,f1(f5(x452)))+~P2(a2,f1(f5(x453)))+P2(f1(x452),f1(f5(f5(x452))))+P2(f1(x453),f1(f5(f5(x453))))+~P2(f1(x454),f1(f5(f5(x454))))+~P2(a2,f1(f5(f5(x454))))+~P2(a2,f1(f5(f5(x452))))+~P2(a2,f1(f5(f5(x453))))+~P2(a2,f1(f5(f5(f5(x454))))) % 56.17/56.19 [46]~P3(f5(x462),f5(x464))+~P3(f5(x463),f5(x461))+~P3(f5(x464),f5(x463))+P2(f1(x461),f1(f5(x461)))+~P2(a2,f1(x461))+~P2(f1(x462),f1(f5(x462)))+~P2(f1(x463),f1(f5(x463)))+~P2(f1(x464),f1(f5(x464)))+~P2(a2,f1(x462))+~P2(a2,f1(x463))+~P2(a2,f1(x464))+~P2(a2,f1(f5(x462)))+~P2(a2,f1(f5(x461)))+~P2(a2,f1(f5(x463)))+~P2(a2,f1(f5(x464)))+P2(f1(x462),f1(f5(f5(x462))))+P2(f1(x463),f1(f5(f5(x463))))+~P2(f1(x464),f1(f5(f5(x464))))+~P2(a2,f1(f5(f5(x462))))+~P2(a2,f1(f5(f5(x463))))+~P2(a2,f1(f5(f5(x464))))+~P2(a2,f1(f5(f5(f5(x464))))) % 56.17/56.19 [47]~P3(f5(x471),f5(x472))+~P3(f5(x473),f5(x471))+~P3(f5(x474),f5(x473))+P2(f1(x471),f1(f5(x471)))+~P2(a2,f1(x471))+~P2(f1(x472),f1(f5(x472)))+~P2(f1(x473),f1(f5(x473)))+~P2(f1(x474),f1(f5(x474)))+~P2(a2,f1(x472))+~P2(a2,f1(x473))+~P2(a2,f1(x474))+~P2(a2,f1(f5(x472)))+~P2(a2,f1(f5(x471)))+~P2(a2,f1(f5(x473)))+~P2(a2,f1(f5(x474)))+P2(f1(x472),f1(f5(f5(x472))))+P2(f1(x473),f1(f5(f5(x473))))+~P2(f1(x474),f1(f5(f5(x474))))+~P2(a2,f1(f5(f5(x472))))+~P2(a2,f1(f5(f5(x473))))+~P2(a2,f1(f5(f5(x474))))+~P2(a2,f1(f5(f5(f5(x474))))) % 56.17/56.19 [48]~P3(f5(x482),f5(x483))+~P3(f5(x484),f5(x481))+~P3(f5(x483),f5(x484))+P2(f1(x481),f1(f5(x481)))+~P2(a2,f1(x481))+~P2(f1(x482),f1(f5(x482)))+~P2(f1(x483),f1(f5(x483)))+~P2(a2,f1(x482))+~P2(f1(x484),f1(f5(x484)))+~P2(a2,f1(x483))+~P2(a2,f1(x484))+~P2(a2,f1(f5(x482)))+~P2(a2,f1(f5(x481)))+~P2(a2,f1(f5(x484)))+~P2(a2,f1(f5(x483)))+P2(f1(x482),f1(f5(f5(x482))))+P2(f1(x483),f1(f5(f5(x483))))+~P2(f1(x484),f1(f5(f5(x484))))+~P2(a2,f1(f5(f5(x482))))+~P2(a2,f1(f5(f5(x484))))+~P2(a2,f1(f5(f5(x483))))+~P2(a2,f1(f5(f5(f5(x484))))) % 56.17/56.19 [49]~P3(f5(x492),f5(x494))+~P3(f5(x491),f5(x493))+~P3(f5(x494),f5(x491))+P2(f1(x491),f1(f5(x491)))+~P2(a2,f1(x491))+~P2(f1(x492),f1(f5(x492)))+~P2(f1(x493),f1(f5(x493)))+~P2(f1(x494),f1(f5(x494)))+~P2(a2,f1(x492))+~P2(a2,f1(x493))+~P2(a2,f1(x494))+~P2(a2,f1(f5(x492)))+~P2(a2,f1(f5(x493)))+~P2(a2,f1(f5(x491)))+~P2(a2,f1(f5(x494)))+P2(f1(x492),f1(f5(f5(x492))))+P2(f1(x493),f1(f5(f5(x493))))+~P2(f1(x494),f1(f5(f5(x494))))+~P2(a2,f1(f5(f5(x492))))+~P2(a2,f1(f5(f5(x493))))+~P2(a2,f1(f5(f5(x494))))+~P2(a2,f1(f5(f5(f5(x494))))) % 56.17/56.19 [50]~P3(f5(x503),f5(x502))+~P3(f5(x501),f5(x503))+~P3(f5(x504),f5(x501))+P2(f1(x501),f1(f5(x501)))+~P2(a2,f1(x501))+~P2(f1(x502),f1(f5(x502)))+~P2(f1(x503),f1(f5(x503)))+~P2(f1(x504),f1(f5(x504)))+~P2(a2,f1(x502))+~P2(a2,f1(x503))+~P2(a2,f1(x504))+~P2(a2,f1(f5(x502)))+~P2(a2,f1(f5(x503)))+~P2(a2,f1(f5(x501)))+~P2(a2,f1(f5(x504)))+P2(f1(x502),f1(f5(f5(x502))))+P2(f1(x503),f1(f5(f5(x503))))+~P2(f1(x504),f1(f5(f5(x504))))+~P2(a2,f1(f5(f5(x502))))+~P2(a2,f1(f5(f5(x503))))+~P2(a2,f1(f5(f5(x504))))+~P2(a2,f1(f5(f5(f5(x504))))) % 56.17/56.19 [51]~P3(f5(x512),f5(x513))+~P3(f5(x511),f5(x514))+~P3(f5(x513),f5(x511))+P2(f1(x511),f1(f5(x511)))+~P2(a2,f1(x511))+~P2(f1(x512),f1(f5(x512)))+~P2(f1(x513),f1(f5(x513)))+~P2(a2,f1(x512))+~P2(f1(x514),f1(f5(x514)))+~P2(a2,f1(x513))+~P2(a2,f1(x514))+~P2(a2,f1(f5(x512)))+~P2(a2,f1(f5(x514)))+~P2(a2,f1(f5(x511)))+~P2(a2,f1(f5(x513)))+P2(f1(x512),f1(f5(f5(x512))))+P2(f1(x513),f1(f5(f5(x513))))+~P2(f1(x514),f1(f5(f5(x514))))+~P2(a2,f1(f5(f5(x512))))+~P2(a2,f1(f5(f5(x514))))+~P2(a2,f1(f5(f5(x513))))+~P2(a2,f1(f5(f5(f5(x514))))) % 56.17/56.19 [52]~P3(f5(x522),f5(x521))+~P3(f5(x524),f5(x523))+~P3(f5(x521),f5(x524))+P2(f1(x521),f1(f5(x521)))+~P2(a2,f1(x521))+~P2(f1(x522),f1(f5(x522)))+~P2(f1(x523),f1(f5(x523)))+~P2(f1(x524),f1(f5(x524)))+~P2(a2,f1(x522))+~P2(a2,f1(x523))+~P2(a2,f1(x524))+~P2(a2,f1(f5(x522)))+~P2(a2,f1(f5(x523)))+~P2(a2,f1(f5(x524)))+~P2(a2,f1(f5(x521)))+P2(f1(x522),f1(f5(f5(x522))))+P2(f1(x523),f1(f5(f5(x523))))+~P2(f1(x524),f1(f5(f5(x524))))+~P2(a2,f1(f5(f5(x522))))+~P2(a2,f1(f5(f5(x523))))+~P2(a2,f1(f5(f5(x524))))+~P2(a2,f1(f5(f5(f5(x524))))) % 56.17/56.19 [53]~P3(f5(x532),f5(x531))+~P3(f5(x533),f5(x534))+~P3(f5(x531),f5(x533))+P2(f1(x531),f1(f5(x531)))+~P2(a2,f1(x531))+~P2(f1(x532),f1(f5(x532)))+~P2(f1(x533),f1(f5(x533)))+~P2(a2,f1(x532))+~P2(f1(x534),f1(f5(x534)))+~P2(a2,f1(x533))+~P2(a2,f1(x534))+~P2(a2,f1(f5(x532)))+~P2(a2,f1(f5(x534)))+~P2(a2,f1(f5(x533)))+~P2(a2,f1(f5(x531)))+P2(f1(x532),f1(f5(f5(x532))))+P2(f1(x533),f1(f5(f5(x533))))+~P2(f1(x534),f1(f5(f5(x534))))+~P2(a2,f1(f5(f5(x532))))+~P2(a2,f1(f5(f5(x534))))+~P2(a2,f1(f5(f5(x533))))+~P2(a2,f1(f5(f5(f5(x534))))) % 56.17/56.19 [41]~P3(f5(x414),f5(x413))+~P3(f5(x413),f5(x412))+~P3(f5(x411),f5(x414))+~P2(f1(x411),f1(f5(x411)))+~P2(f1(x412),f1(f5(x412)))+~P2(a2,f1(x411))+~P2(f1(x413),f1(f5(x413)))+~P2(a2,f1(x412))+~P2(f1(x414),f1(f5(x414)))+~P2(a2,f1(x413))+~P2(a2,f1(x414))+~P2(a2,f1(f5(x411)))+~P2(a2,f1(f5(x412)))+~P2(a2,f1(f5(x413)))+~P2(a2,f1(f5(x414)))+P2(f1(x411),f1(f5(f5(x411))))+P2(f1(x412),f1(f5(f5(x412))))+P2(f1(x413),f1(f5(f5(x413))))+P2(f1(x414),f1(f5(f5(x414))))+~P2(a2,f1(f5(f5(x411))))+~P2(a2,f1(f5(f5(x412))))+~P2(a2,f1(f5(f5(x413))))+~P2(a2,f1(f5(f5(x414)))) % 56.17/56.19 [64]~P3(f5(x641),f5(x644))+~P3(f5(x643),f5(x642))+~P3(f5(x644),f5(x643))+P2(f1(x641),f1(f5(x641)))+~P2(a2,f1(x641))+~P2(f1(x642),f1(f5(x642)))+~P2(f1(x643),f1(f5(x643)))+~P2(a2,f1(x642))+~P2(f1(x644),f1(f5(x644)))+~P2(a2,f1(x643))+~P2(a2,f1(x644))+~P2(a2,f1(f5(x641)))+~P2(a2,f1(f5(x642)))+~P2(a2,f1(f5(x643)))+~P2(a2,f1(f5(x644)))+P2(f1(x642),f1(f5(f5(x642))))+~P2(f1(x643),f1(f5(f5(x643))))+~P2(f1(x644),f1(f5(f5(x644))))+~P2(a2,f1(f5(f5(x642))))+~P2(a2,f1(f5(f5(x643))))+~P2(a2,f1(f5(f5(x644))))+~P2(a2,f1(f5(f5(f5(x643)))))+~P2(a2,f1(f5(f5(f5(x644))))) % 56.17/56.19 [65]~P3(f5(x652),f5(x651))+~P3(f5(x653),f5(x652))+~P3(f5(x654),f5(x653))+P2(f1(x651),f1(f5(x651)))+~P2(a2,f1(x651))+~P2(f1(x652),f1(f5(x652)))+~P2(f1(x653),f1(f5(x653)))+~P2(a2,f1(x652))+~P2(f1(x654),f1(f5(x654)))+~P2(a2,f1(x653))+~P2(a2,f1(x654))+~P2(a2,f1(f5(x651)))+~P2(a2,f1(f5(x652)))+~P2(a2,f1(f5(x653)))+~P2(a2,f1(f5(x654)))+P2(f1(x652),f1(f5(f5(x652))))+~P2(f1(x653),f1(f5(f5(x653))))+~P2(f1(x654),f1(f5(f5(x654))))+~P2(a2,f1(f5(f5(x652))))+~P2(a2,f1(f5(f5(x653))))+~P2(a2,f1(f5(f5(x654))))+~P2(a2,f1(f5(f5(f5(x653)))))+~P2(a2,f1(f5(f5(f5(x654))))) % 56.17/56.19 [66]~P3(f5(x661),f5(x664))+~P3(f5(x662),f5(x663))+~P3(f5(x664),f5(x662))+P2(f1(x661),f1(f5(x661)))+~P2(a2,f1(x661))+~P2(f1(x662),f1(f5(x662)))+~P2(f1(x663),f1(f5(x663)))+~P2(a2,f1(x662))+~P2(f1(x664),f1(f5(x664)))+~P2(a2,f1(x663))+~P2(a2,f1(x664))+~P2(a2,f1(f5(x661)))+~P2(a2,f1(f5(x663)))+~P2(a2,f1(f5(x662)))+~P2(a2,f1(f5(x664)))+P2(f1(x662),f1(f5(f5(x662))))+~P2(f1(x663),f1(f5(f5(x663))))+~P2(f1(x664),f1(f5(f5(x664))))+~P2(a2,f1(f5(f5(x663))))+~P2(a2,f1(f5(f5(x662))))+~P2(a2,f1(f5(f5(x664))))+~P2(a2,f1(f5(f5(f5(x663)))))+~P2(a2,f1(f5(f5(f5(x664))))) % 56.17/56.19 [67]~P3(f5(x673),f5(x671))+~P3(f5(x672),f5(x673))+~P3(f5(x674),f5(x672))+P2(f1(x671),f1(f5(x671)))+~P2(a2,f1(x671))+~P2(f1(x672),f1(f5(x672)))+~P2(f1(x673),f1(f5(x673)))+~P2(a2,f1(x672))+~P2(f1(x674),f1(f5(x674)))+~P2(a2,f1(x673))+~P2(a2,f1(x674))+~P2(a2,f1(f5(x671)))+~P2(a2,f1(f5(x673)))+~P2(a2,f1(f5(x672)))+~P2(a2,f1(f5(x674)))+P2(f1(x672),f1(f5(f5(x672))))+~P2(f1(x673),f1(f5(f5(x673))))+~P2(f1(x674),f1(f5(f5(x674))))+~P2(a2,f1(f5(f5(x673))))+~P2(a2,f1(f5(f5(x672))))+~P2(a2,f1(f5(f5(x674))))+~P2(a2,f1(f5(f5(f5(x673)))))+~P2(a2,f1(f5(f5(f5(x674))))) % 56.17/56.19 [68]~P3(f5(x681),f5(x682))+~P3(f5(x684),f5(x683))+~P3(f5(x682),f5(x684))+P2(f1(x681),f1(f5(x681)))+~P2(a2,f1(x681))+~P2(f1(x682),f1(f5(x682)))+~P2(f1(x683),f1(f5(x683)))+~P2(a2,f1(x682))+~P2(f1(x684),f1(f5(x684)))+~P2(a2,f1(x683))+~P2(a2,f1(x684))+~P2(a2,f1(f5(x681)))+~P2(a2,f1(f5(x683)))+~P2(a2,f1(f5(x684)))+~P2(a2,f1(f5(x682)))+P2(f1(x682),f1(f5(f5(x682))))+~P2(f1(x683),f1(f5(f5(x683))))+~P2(f1(x684),f1(f5(f5(x684))))+~P2(a2,f1(f5(f5(x683))))+~P2(a2,f1(f5(f5(x684))))+~P2(a2,f1(f5(f5(x682))))+~P2(a2,f1(f5(f5(f5(x683)))))+~P2(a2,f1(f5(f5(f5(x684))))) % 56.17/56.19 [69]~P3(f5(x692),f5(x694))+~P3(f5(x693),f5(x691))+~P3(f5(x694),f5(x693))+P2(f1(x691),f1(f5(x691)))+~P2(a2,f1(x691))+~P2(f1(x692),f1(f5(x692)))+~P2(f1(x693),f1(f5(x693)))+~P2(a2,f1(x692))+~P2(f1(x694),f1(f5(x694)))+~P2(a2,f1(x693))+~P2(a2,f1(x694))+~P2(a2,f1(f5(x692)))+~P2(a2,f1(f5(x691)))+~P2(a2,f1(f5(x693)))+~P2(a2,f1(f5(x694)))+P2(f1(x692),f1(f5(f5(x692))))+~P2(f1(x693),f1(f5(f5(x693))))+~P2(f1(x694),f1(f5(f5(x694))))+~P2(a2,f1(f5(f5(x692))))+~P2(a2,f1(f5(f5(x693))))+~P2(a2,f1(f5(f5(x694))))+~P2(a2,f1(f5(f5(f5(x693)))))+~P2(a2,f1(f5(f5(f5(x694))))) % 56.17/56.19 [70]~P3(f5(x701),f5(x702))+~P3(f5(x703),f5(x701))+~P3(f5(x704),f5(x703))+P2(f1(x701),f1(f5(x701)))+~P2(a2,f1(x701))+~P2(f1(x702),f1(f5(x702)))+~P2(f1(x703),f1(f5(x703)))+~P2(a2,f1(x702))+~P2(f1(x704),f1(f5(x704)))+~P2(a2,f1(x703))+~P2(a2,f1(x704))+~P2(a2,f1(f5(x702)))+~P2(a2,f1(f5(x701)))+~P2(a2,f1(f5(x703)))+~P2(a2,f1(f5(x704)))+P2(f1(x702),f1(f5(f5(x702))))+~P2(f1(x703),f1(f5(f5(x703))))+~P2(f1(x704),f1(f5(f5(x704))))+~P2(a2,f1(f5(f5(x702))))+~P2(a2,f1(f5(f5(x703))))+~P2(a2,f1(f5(f5(x704))))+~P2(a2,f1(f5(f5(f5(x703)))))+~P2(a2,f1(f5(f5(f5(x704))))) % 56.17/56.19 [71]~P3(f5(x711),f5(x713))+~P3(f5(x712),f5(x711))+~P3(f5(x714),f5(x712))+P2(f1(x711),f1(f5(x711)))+~P2(a2,f1(x711))+~P2(f1(x712),f1(f5(x712)))+~P2(f1(x713),f1(f5(x713)))+~P2(a2,f1(x712))+~P2(f1(x714),f1(f5(x714)))+~P2(a2,f1(x713))+~P2(a2,f1(x714))+~P2(a2,f1(f5(x713)))+~P2(a2,f1(f5(x711)))+~P2(a2,f1(f5(x712)))+~P2(a2,f1(f5(x714)))+P2(f1(x712),f1(f5(f5(x712))))+~P2(f1(x713),f1(f5(f5(x713))))+~P2(f1(x714),f1(f5(f5(x714))))+~P2(a2,f1(f5(f5(x713))))+~P2(a2,f1(f5(f5(x712))))+~P2(a2,f1(f5(f5(x714))))+~P2(a2,f1(f5(f5(f5(x713)))))+~P2(a2,f1(f5(f5(f5(x714))))) % 56.17/56.19 [72]~P3(f5(x722),f5(x724))+~P3(f5(x721),f5(x723))+~P3(f5(x724),f5(x721))+P2(f1(x721),f1(f5(x721)))+~P2(a2,f1(x721))+~P2(f1(x722),f1(f5(x722)))+~P2(f1(x723),f1(f5(x723)))+~P2(a2,f1(x722))+~P2(f1(x724),f1(f5(x724)))+~P2(a2,f1(x723))+~P2(a2,f1(x724))+~P2(a2,f1(f5(x722)))+~P2(a2,f1(f5(x723)))+~P2(a2,f1(f5(x721)))+~P2(a2,f1(f5(x724)))+P2(f1(x722),f1(f5(f5(x722))))+~P2(f1(x723),f1(f5(f5(x723))))+~P2(f1(x724),f1(f5(f5(x724))))+~P2(a2,f1(f5(f5(x722))))+~P2(a2,f1(f5(f5(x723))))+~P2(a2,f1(f5(f5(x724))))+~P2(a2,f1(f5(f5(f5(x723)))))+~P2(a2,f1(f5(f5(f5(x724))))) % 56.17/56.19 [73]~P3(f5(x733),f5(x732))+~P3(f5(x731),f5(x733))+~P3(f5(x734),f5(x731))+P2(f1(x731),f1(f5(x731)))+~P2(a2,f1(x731))+~P2(f1(x732),f1(f5(x732)))+~P2(f1(x733),f1(f5(x733)))+~P2(a2,f1(x732))+~P2(f1(x734),f1(f5(x734)))+~P2(a2,f1(x733))+~P2(a2,f1(x734))+~P2(a2,f1(f5(x732)))+~P2(a2,f1(f5(x733)))+~P2(a2,f1(f5(x731)))+~P2(a2,f1(f5(x734)))+P2(f1(x732),f1(f5(f5(x732))))+~P2(f1(x733),f1(f5(f5(x733))))+~P2(f1(x734),f1(f5(f5(x734))))+~P2(a2,f1(f5(f5(x732))))+~P2(a2,f1(f5(f5(x733))))+~P2(a2,f1(f5(f5(x734))))+~P2(a2,f1(f5(f5(f5(x733)))))+~P2(a2,f1(f5(f5(f5(x734))))) % 56.17/56.19 [74]~P3(f5(x742),f5(x743))+~P3(f5(x741),f5(x742))+~P3(f5(x744),f5(x741))+P2(f1(x741),f1(f5(x741)))+~P2(a2,f1(x741))+~P2(f1(x742),f1(f5(x742)))+~P2(f1(x743),f1(f5(x743)))+~P2(a2,f1(x742))+~P2(f1(x744),f1(f5(x744)))+~P2(a2,f1(x743))+~P2(a2,f1(x744))+~P2(a2,f1(f5(x743)))+~P2(a2,f1(f5(x742)))+~P2(a2,f1(f5(x741)))+~P2(a2,f1(f5(x744)))+P2(f1(x742),f1(f5(f5(x742))))+~P2(f1(x743),f1(f5(f5(x743))))+~P2(f1(x744),f1(f5(f5(x744))))+~P2(a2,f1(f5(f5(x743))))+~P2(a2,f1(f5(f5(x742))))+~P2(a2,f1(f5(f5(x744))))+~P2(a2,f1(f5(f5(f5(x743)))))+~P2(a2,f1(f5(f5(f5(x744))))) % 56.17/56.20 [75]~P3(f5(x752),f5(x751))+~P3(f5(x754),f5(x753))+~P3(f5(x751),f5(x754))+P2(f1(x751),f1(f5(x751)))+~P2(a2,f1(x751))+~P2(f1(x752),f1(f5(x752)))+~P2(f1(x753),f1(f5(x753)))+~P2(a2,f1(x752))+~P2(f1(x754),f1(f5(x754)))+~P2(a2,f1(x753))+~P2(a2,f1(x754))+~P2(a2,f1(f5(x752)))+~P2(a2,f1(f5(x753)))+~P2(a2,f1(f5(x754)))+~P2(a2,f1(f5(x751)))+P2(f1(x752),f1(f5(f5(x752))))+~P2(f1(x753),f1(f5(f5(x753))))+~P2(f1(x754),f1(f5(f5(x754))))+~P2(a2,f1(f5(f5(x752))))+~P2(a2,f1(f5(f5(x753))))+~P2(a2,f1(f5(f5(x754))))+~P2(a2,f1(f5(f5(f5(x753)))))+~P2(a2,f1(f5(f5(f5(x754))))) % 56.17/56.20 [60]~P3(f5(x604),f5(x603))+~P3(f5(x603),f5(x602))+~P3(f5(x601),f5(x604))+~P2(f1(x601),f1(f5(x601)))+~P2(f1(x602),f1(f5(x602)))+~P2(a2,f1(x601))+~P2(f1(x603),f1(f5(x603)))+~P2(a2,f1(x602))+~P2(f1(x604),f1(f5(x604)))+~P2(a2,f1(x603))+~P2(a2,f1(x604))+~P2(a2,f1(f5(x601)))+~P2(a2,f1(f5(x602)))+~P2(a2,f1(f5(x603)))+~P2(a2,f1(f5(x604)))+P2(f1(x601),f1(f5(f5(x601))))+P2(f1(x602),f1(f5(f5(x602))))+P2(f1(x603),f1(f5(f5(x603))))+~P2(f1(x604),f1(f5(f5(x604))))+~P2(a2,f1(f5(f5(x601))))+~P2(a2,f1(f5(f5(x602))))+~P2(a2,f1(f5(f5(x603))))+~P2(a2,f1(f5(f5(x604))))+~P2(a2,f1(f5(f5(f5(x604))))) % 56.17/56.20 [61]~P3(f5(x614),f5(x613))+~P3(f5(x613),f5(x612))+~P3(f5(x612),f5(x611))+~P2(f1(x611),f1(f5(x611)))+~P2(f1(x612),f1(f5(x612)))+~P2(a2,f1(x611))+~P2(f1(x613),f1(f5(x613)))+~P2(a2,f1(x612))+~P2(f1(x614),f1(f5(x614)))+~P2(a2,f1(x613))+~P2(a2,f1(x614))+~P2(a2,f1(f5(x611)))+~P2(a2,f1(f5(x612)))+~P2(a2,f1(f5(x613)))+~P2(a2,f1(f5(x614)))+P2(f1(x611),f1(f5(f5(x611))))+P2(f1(x612),f1(f5(f5(x612))))+P2(f1(x613),f1(f5(f5(x613))))+~P2(f1(x614),f1(f5(f5(x614))))+~P2(a2,f1(f5(f5(x611))))+~P2(a2,f1(f5(f5(x612))))+~P2(a2,f1(f5(f5(x613))))+~P2(a2,f1(f5(f5(x614))))+~P2(a2,f1(f5(f5(f5(x614))))) % 56.17/56.20 [62]~P3(f5(x623),f5(x624))+~P3(f5(x624),f5(x622))+~P3(f5(x621),f5(x623))+~P2(f1(x621),f1(f5(x621)))+~P2(f1(x622),f1(f5(x622)))+~P2(a2,f1(x621))+~P2(f1(x623),f1(f5(x623)))+~P2(f1(x624),f1(f5(x624)))+~P2(a2,f1(x622))+~P2(a2,f1(x623))+~P2(a2,f1(x624))+~P2(a2,f1(f5(x621)))+~P2(a2,f1(f5(x622)))+~P2(a2,f1(f5(x624)))+~P2(a2,f1(f5(x623)))+P2(f1(x621),f1(f5(f5(x621))))+P2(f1(x622),f1(f5(f5(x622))))+P2(f1(x623),f1(f5(f5(x623))))+~P2(f1(x624),f1(f5(f5(x624))))+~P2(a2,f1(f5(f5(x621))))+~P2(a2,f1(f5(f5(x622))))+~P2(a2,f1(f5(f5(x624))))+~P2(a2,f1(f5(f5(x623))))+~P2(a2,f1(f5(f5(f5(x624))))) % 56.17/56.20 [63]~P3(f5(x633),f5(x632))+~P3(f5(x632),f5(x634))+~P3(f5(x631),f5(x633))+~P2(f1(x631),f1(f5(x631)))+~P2(f1(x632),f1(f5(x632)))+~P2(a2,f1(x631))+~P2(f1(x633),f1(f5(x633)))+~P2(a2,f1(x632))+~P2(f1(x634),f1(f5(x634)))+~P2(a2,f1(x633))+~P2(a2,f1(x634))+~P2(a2,f1(f5(x631)))+~P2(a2,f1(f5(x634)))+~P2(a2,f1(f5(x632)))+~P2(a2,f1(f5(x633)))+P2(f1(x631),f1(f5(f5(x631))))+P2(f1(x632),f1(f5(f5(x632))))+P2(f1(x633),f1(f5(f5(x633))))+~P2(f1(x634),f1(f5(f5(x634))))+~P2(a2,f1(f5(f5(x631))))+~P2(a2,f1(f5(f5(x634))))+~P2(a2,f1(f5(f5(x632))))+~P2(a2,f1(f5(f5(x633))))+~P2(a2,f1(f5(f5(f5(x634))))) % 56.17/56.20 [82]~P3(f5(x824),f5(x823))+~P3(f5(x823),f5(x822))+~P3(f5(x821),f5(x824))+P2(f1(x821),f1(f5(x821)))+~P2(a2,f1(x821))+~P2(f1(x822),f1(f5(x822)))+~P2(f1(x823),f1(f5(x823)))+~P2(a2,f1(x822))+~P2(f1(x824),f1(f5(x824)))+~P2(a2,f1(x823))+~P2(a2,f1(x824))+~P2(a2,f1(f5(x821)))+~P2(a2,f1(f5(x822)))+~P2(a2,f1(f5(x823)))+~P2(a2,f1(f5(x824)))+~P2(f1(x822),f1(f5(f5(x822))))+~P2(f1(x823),f1(f5(f5(x823))))+~P2(f1(x824),f1(f5(f5(x824))))+~P2(a2,f1(f5(f5(x822))))+~P2(a2,f1(f5(f5(x824))))+~P2(a2,f1(f5(f5(x823))))+~P2(a2,f1(f5(f5(f5(x822)))))+~P2(a2,f1(f5(f5(f5(x823)))))+~P2(a2,f1(f5(f5(f5(x824))))) % 56.17/56.20 [83]~P3(f5(x834),f5(x833))+~P3(f5(x833),f5(x832))+~P3(f5(x832),f5(x831))+P2(f1(x831),f1(f5(x831)))+~P2(a2,f1(x831))+~P2(f1(x832),f1(f5(x832)))+~P2(f1(x833),f1(f5(x833)))+~P2(a2,f1(x832))+~P2(f1(x834),f1(f5(x834)))+~P2(a2,f1(x833))+~P2(a2,f1(x834))+~P2(a2,f1(f5(x831)))+~P2(a2,f1(f5(x832)))+~P2(a2,f1(f5(x833)))+~P2(a2,f1(f5(x834)))+~P2(f1(x832),f1(f5(f5(x832))))+~P2(f1(x833),f1(f5(f5(x833))))+~P2(f1(x834),f1(f5(f5(x834))))+~P2(a2,f1(f5(f5(x832))))+~P2(a2,f1(f5(f5(x834))))+~P2(a2,f1(f5(f5(x833))))+~P2(a2,f1(f5(f5(f5(x832)))))+~P2(a2,f1(f5(f5(f5(x833)))))+~P2(a2,f1(f5(f5(f5(x834))))) % 56.17/56.20 [84]~P3(f5(x841),f5(x842))+~P3(f5(x843),f5(x841))+~P3(f5(x844),f5(x843))+P2(f1(x841),f1(f5(x841)))+~P2(a2,f1(x841))+~P2(f1(x842),f1(f5(x842)))+~P2(f1(x843),f1(f5(x843)))+~P2(a2,f1(x842))+~P2(f1(x844),f1(f5(x844)))+~P2(a2,f1(x843))+~P2(a2,f1(x844))+~P2(a2,f1(f5(x841)))+~P2(a2,f1(f5(x843)))+~P2(a2,f1(f5(x844)))+~P2(a2,f1(f5(x842)))+~P2(f1(x842),f1(f5(f5(x842))))+~P2(f1(x843),f1(f5(f5(x843))))+~P2(f1(x844),f1(f5(f5(x844))))+~P2(a2,f1(f5(f5(x842))))+~P2(a2,f1(f5(f5(x843))))+~P2(a2,f1(f5(f5(x844))))+~P2(a2,f1(f5(f5(f5(x842)))))+~P2(a2,f1(f5(f5(f5(x843)))))+~P2(a2,f1(f5(f5(f5(x844))))) % 56.17/56.20 [85]~P3(f5(x853),f5(x852))+~P3(f5(x851),f5(x853))+~P3(f5(x854),f5(x851))+P2(f1(x851),f1(f5(x851)))+~P2(a2,f1(x851))+~P2(f1(x852),f1(f5(x852)))+~P2(f1(x853),f1(f5(x853)))+~P2(a2,f1(x852))+~P2(f1(x854),f1(f5(x854)))+~P2(a2,f1(x853))+~P2(a2,f1(x854))+~P2(a2,f1(f5(x853)))+~P2(a2,f1(f5(x851)))+~P2(a2,f1(f5(x854)))+~P2(a2,f1(f5(x852)))+~P2(f1(x852),f1(f5(f5(x852))))+~P2(f1(x853),f1(f5(f5(x853))))+~P2(f1(x854),f1(f5(f5(x854))))+~P2(a2,f1(f5(f5(x852))))+~P2(a2,f1(f5(f5(x853))))+~P2(a2,f1(f5(f5(x854))))+~P2(a2,f1(f5(f5(f5(x852)))))+~P2(a2,f1(f5(f5(f5(x853)))))+~P2(a2,f1(f5(f5(f5(x854))))) % 56.17/56.20 [76]~P3(f5(x764),f5(x763))+~P3(f5(x761),f5(x764))+~P3(f5(x763),f5(x762))+~P2(f1(x761),f1(f5(x761)))+~P2(a2,f1(x761))+~P2(f1(x762),f1(f5(x762)))+~P2(f1(x763),f1(f5(x763)))+~P2(f1(x764),f1(f5(x764)))+~P2(a2,f1(x762))+~P2(a2,f1(x763))+~P2(a2,f1(x764))+~P2(a2,f1(f5(x761)))+~P2(a2,f1(f5(x762)))+~P2(a2,f1(f5(x763)))+~P2(a2,f1(f5(x764)))+P2(f1(x761),f1(f5(f5(x761))))+P2(f1(x762),f1(f5(f5(x762))))+~P2(f1(x763),f1(f5(f5(x763))))+~P2(f1(x764),f1(f5(f5(x764))))+~P2(a2,f1(f5(f5(x761))))+~P2(a2,f1(f5(f5(x762))))+~P2(a2,f1(f5(f5(x763))))+~P2(a2,f1(f5(f5(x764))))+~P2(a2,f1(f5(f5(f5(x763)))))+~P2(a2,f1(f5(f5(f5(x764))))) % 56.17/56.20 [77]~P3(f5(x774),f5(x773))+~P3(f5(x772),f5(x771))+~P3(f5(x773),f5(x772))+~P2(f1(x771),f1(f5(x771)))+~P2(a2,f1(x771))+~P2(f1(x772),f1(f5(x772)))+~P2(f1(x773),f1(f5(x773)))+~P2(f1(x774),f1(f5(x774)))+~P2(a2,f1(x772))+~P2(a2,f1(x773))+~P2(a2,f1(x774))+~P2(a2,f1(f5(x771)))+~P2(a2,f1(f5(x772)))+~P2(a2,f1(f5(x773)))+~P2(a2,f1(f5(x774)))+P2(f1(x771),f1(f5(f5(x771))))+P2(f1(x772),f1(f5(f5(x772))))+~P2(f1(x773),f1(f5(f5(x773))))+~P2(f1(x774),f1(f5(f5(x774))))+~P2(a2,f1(f5(f5(x771))))+~P2(a2,f1(f5(f5(x772))))+~P2(a2,f1(f5(f5(x773))))+~P2(a2,f1(f5(f5(x774))))+~P2(a2,f1(f5(f5(f5(x773)))))+~P2(a2,f1(f5(f5(f5(x774))))) % 56.17/56.20 [78]~P3(f5(x784),f5(x782))+~P3(f5(x781),f5(x784))+~P3(f5(x782),f5(x783))+~P2(f1(x781),f1(f5(x781)))+~P2(f1(x782),f1(f5(x782)))+~P2(a2,f1(x781))+~P2(f1(x783),f1(f5(x783)))+~P2(f1(x784),f1(f5(x784)))+~P2(a2,f1(x782))+~P2(a2,f1(x783))+~P2(a2,f1(x784))+~P2(a2,f1(f5(x781)))+~P2(a2,f1(f5(x783)))+~P2(a2,f1(f5(x782)))+~P2(a2,f1(f5(x784)))+P2(f1(x781),f1(f5(f5(x781))))+P2(f1(x782),f1(f5(f5(x782))))+~P2(f1(x783),f1(f5(f5(x783))))+~P2(f1(x784),f1(f5(f5(x784))))+~P2(a2,f1(f5(f5(x781))))+~P2(a2,f1(f5(f5(x783))))+~P2(a2,f1(f5(f5(x782))))+~P2(a2,f1(f5(f5(x784))))+~P2(a2,f1(f5(f5(f5(x783)))))+~P2(a2,f1(f5(f5(f5(x784))))) % 56.17/56.20 [79]~P3(f5(x794),f5(x792))+~P3(f5(x793),f5(x791))+~P3(f5(x792),f5(x793))+~P2(f1(x791),f1(f5(x791)))+~P2(f1(x792),f1(f5(x792)))+~P2(a2,f1(x791))+~P2(f1(x793),f1(f5(x793)))+~P2(f1(x794),f1(f5(x794)))+~P2(a2,f1(x792))+~P2(a2,f1(x793))+~P2(a2,f1(x794))+~P2(a2,f1(f5(x791)))+~P2(a2,f1(f5(x793)))+~P2(a2,f1(f5(x792)))+~P2(a2,f1(f5(x794)))+P2(f1(x791),f1(f5(f5(x791))))+P2(f1(x792),f1(f5(f5(x792))))+~P2(f1(x793),f1(f5(f5(x793))))+~P2(f1(x794),f1(f5(f5(x794))))+~P2(a2,f1(f5(f5(x791))))+~P2(a2,f1(f5(f5(x793))))+~P2(a2,f1(f5(f5(x792))))+~P2(a2,f1(f5(f5(x794))))+~P2(a2,f1(f5(f5(f5(x793)))))+~P2(a2,f1(f5(f5(f5(x794))))) % 56.17/56.20 [80]~P3(f5(x802),f5(x804))+~P3(f5(x804),f5(x803))+~P3(f5(x801),f5(x802))+~P2(f1(x801),f1(f5(x801)))+~P2(f1(x802),f1(f5(x802)))+~P2(a2,f1(x801))+~P2(f1(x803),f1(f5(x803)))+~P2(a2,f1(x802))+~P2(f1(x804),f1(f5(x804)))+~P2(a2,f1(x803))+~P2(a2,f1(x804))+~P2(a2,f1(f5(x801)))+~P2(a2,f1(f5(x803)))+~P2(a2,f1(f5(x804)))+~P2(a2,f1(f5(x802)))+P2(f1(x801),f1(f5(f5(x801))))+P2(f1(x802),f1(f5(f5(x802))))+~P2(f1(x803),f1(f5(f5(x803))))+~P2(f1(x804),f1(f5(f5(x804))))+~P2(a2,f1(f5(f5(x801))))+~P2(a2,f1(f5(f5(x803))))+~P2(a2,f1(f5(f5(x804))))+~P2(a2,f1(f5(f5(x802))))+~P2(a2,f1(f5(f5(f5(x803)))))+~P2(a2,f1(f5(f5(f5(x804))))) % 56.17/56.20 [81]~P3(f5(x814),f5(x812))+~P3(f5(x811),f5(x813))+~P3(f5(x812),f5(x811))+~P2(f1(x811),f1(f5(x811)))+~P2(f1(x812),f1(f5(x812)))+~P2(a2,f1(x811))+~P2(f1(x813),f1(f5(x813)))+~P2(f1(x814),f1(f5(x814)))+~P2(a2,f1(x812))+~P2(a2,f1(x813))+~P2(a2,f1(x814))+~P2(a2,f1(f5(x813)))+~P2(a2,f1(f5(x811)))+~P2(a2,f1(f5(x812)))+~P2(a2,f1(f5(x814)))+P2(f1(x811),f1(f5(f5(x811))))+P2(f1(x812),f1(f5(f5(x812))))+~P2(f1(x813),f1(f5(f5(x813))))+~P2(f1(x814),f1(f5(f5(x814))))+~P2(a2,f1(f5(f5(x813))))+~P2(a2,f1(f5(f5(x811))))+~P2(a2,f1(f5(f5(x812))))+~P2(a2,f1(f5(f5(x814))))+~P2(a2,f1(f5(f5(f5(x813)))))+~P2(a2,f1(f5(f5(f5(x814))))) % 56.17/56.20 [86]~P3(f5(x864),f5(x863))+~P3(f5(x863),f5(x862))+~P3(f5(x861),f5(x864))+~P2(f1(x861),f1(f5(x861)))+~P2(a2,f1(x861))+~P2(f1(x862),f1(f5(x862)))+~P2(f1(x863),f1(f5(x863)))+~P2(a2,f1(x862))+~P2(f1(x864),f1(f5(x864)))+~P2(a2,f1(x863))+~P2(a2,f1(x864))+~P2(a2,f1(f5(x861)))+~P2(a2,f1(f5(x862)))+~P2(a2,f1(f5(x863)))+~P2(a2,f1(f5(x864)))+P2(f1(x861),f1(f5(f5(x861))))+~P2(f1(x862),f1(f5(f5(x862))))+~P2(f1(x863),f1(f5(f5(x863))))+~P2(f1(x864),f1(f5(f5(x864))))+~P2(a2,f1(f5(f5(x861))))+~P2(a2,f1(f5(f5(x864))))+~P2(a2,f1(f5(f5(x863))))+~P2(a2,f1(f5(f5(x862))))+~P2(a2,f1(f5(f5(f5(x862)))))+~P2(a2,f1(f5(f5(f5(x863)))))+~P2(a2,f1(f5(f5(f5(x864))))) % 56.17/56.20 [87]~P3(f5(x874),f5(x873))+~P3(f5(x873),f5(x872))+~P3(f5(x872),f5(x871))+~P2(f1(x871),f1(f5(x871)))+~P2(a2,f1(x871))+~P2(f1(x872),f1(f5(x872)))+~P2(f1(x873),f1(f5(x873)))+~P2(a2,f1(x872))+~P2(f1(x874),f1(f5(x874)))+~P2(a2,f1(x873))+~P2(a2,f1(x874))+~P2(a2,f1(f5(x871)))+~P2(a2,f1(f5(x872)))+~P2(a2,f1(f5(x873)))+~P2(a2,f1(f5(x874)))+P2(f1(x871),f1(f5(f5(x871))))+~P2(f1(x872),f1(f5(f5(x872))))+~P2(f1(x873),f1(f5(f5(x873))))+~P2(f1(x874),f1(f5(f5(x874))))+~P2(a2,f1(f5(f5(x871))))+~P2(a2,f1(f5(f5(x874))))+~P2(a2,f1(f5(f5(x873))))+~P2(a2,f1(f5(f5(x872))))+~P2(a2,f1(f5(f5(f5(x872)))))+~P2(a2,f1(f5(f5(f5(x873)))))+~P2(a2,f1(f5(f5(f5(x874))))) % 56.17/56.20 [88]~P3(f5(x881),f5(x882))+~P3(f5(x883),f5(x881))+~P3(f5(x884),f5(x883))+~P2(f1(x881),f1(f5(x881)))+~P2(a2,f1(x881))+~P2(f1(x882),f1(f5(x882)))+~P2(f1(x883),f1(f5(x883)))+~P2(a2,f1(x882))+~P2(f1(x884),f1(f5(x884)))+~P2(a2,f1(x883))+~P2(a2,f1(x884))+~P2(a2,f1(f5(x883)))+~P2(a2,f1(f5(x884)))+~P2(a2,f1(f5(x882)))+~P2(a2,f1(f5(x881)))+P2(f1(x881),f1(f5(f5(x881))))+~P2(f1(x882),f1(f5(f5(x882))))+~P2(f1(x883),f1(f5(f5(x883))))+~P2(f1(x884),f1(f5(f5(x884))))+~P2(a2,f1(f5(f5(x881))))+~P2(a2,f1(f5(f5(x884))))+~P2(a2,f1(f5(f5(x883))))+~P2(a2,f1(f5(f5(x882))))+~P2(a2,f1(f5(f5(f5(x882)))))+~P2(a2,f1(f5(f5(f5(x883)))))+~P2(a2,f1(f5(f5(f5(x884))))) % 56.17/56.20 [89]~P3(f5(x893),f5(x892))+~P3(f5(x891),f5(x893))+~P3(f5(x894),f5(x891))+~P2(f1(x891),f1(f5(x891)))+~P2(a2,f1(x891))+~P2(f1(x892),f1(f5(x892)))+~P2(f1(x893),f1(f5(x893)))+~P2(a2,f1(x892))+~P2(f1(x894),f1(f5(x894)))+~P2(a2,f1(x893))+~P2(a2,f1(x894))+~P2(a2,f1(f5(x891)))+~P2(a2,f1(f5(x894)))+~P2(a2,f1(f5(x892)))+~P2(a2,f1(f5(x893)))+P2(f1(x891),f1(f5(f5(x891))))+~P2(f1(x892),f1(f5(f5(x892))))+~P2(f1(x893),f1(f5(f5(x893))))+~P2(f1(x894),f1(f5(f5(x894))))+~P2(a2,f1(f5(f5(x893))))+~P2(a2,f1(f5(f5(x894))))+~P2(a2,f1(f5(f5(x891))))+~P2(a2,f1(f5(f5(x892))))+~P2(a2,f1(f5(f5(f5(x892)))))+~P2(a2,f1(f5(f5(f5(x893)))))+~P2(a2,f1(f5(f5(f5(x894))))) % 56.17/56.20 [90]~P3(f5(x902),f5(x901))+~P3(f5(x903),f5(x902))+~P3(f5(x904),f5(x903))+~P2(f1(x901),f1(f5(x901)))+~P2(a2,f1(x901))+~P2(f1(x902),f1(f5(x902)))+~P2(f1(x903),f1(f5(x903)))+~P2(a2,f1(x902))+~P2(f1(x904),f1(f5(x904)))+~P2(a2,f1(x903))+~P2(a2,f1(x904))+~P2(a2,f1(f5(x904)))+~P2(a2,f1(f5(x902)))+~P2(a2,f1(f5(x901)))+~P2(a2,f1(f5(x903)))+~P2(f1(x901),f1(f5(f5(x901))))+~P2(f1(x902),f1(f5(f5(x902))))+~P2(f1(x903),f1(f5(f5(x903))))+~P2(f1(x904),f1(f5(f5(x904))))+~P2(a2,f1(f5(f5(x904))))+~P2(a2,f1(f5(f5(x903))))+~P2(a2,f1(f5(f5(x902))))+~P2(a2,f1(f5(f5(x901))))+~P2(a2,f1(f5(f5(f5(x901)))))+~P2(a2,f1(f5(f5(f5(x902)))))+~P2(a2,f1(f5(f5(f5(x903)))))+~P2(a2,f1(f5(f5(f5(x904))))) % 56.17/56.20 cnf(97,plain, % 56.17/56.20 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(f5(a4)))), % 56.17/56.20 inference(scs_inference,[],[2,1,5,3])). % 56.17/56.20 cnf(98,plain, % 56.17/56.20 (P2(f1(a4),f1(f5(a4)))+P3(f5(a4),f5(a4))), % 56.17/56.20 inference(scs_inference,[],[1,2,97,4])). % 56.17/56.20 cnf(102,plain, % 56.17/56.20 (P2(a2,f1(a4))), % 56.17/56.20 inference(scs_inference,[],[1,2,3])). % 56.17/56.20 cnf(103,plain, % 56.17/56.20 (P1(f1(x1031),f3(a2))), % 56.17/56.20 inference(rename_variables,[],[1])). % 56.17/56.20 cnf(105,plain, % 56.17/56.20 (P2(a2,f1(f5(a4)))), % 56.17/56.20 inference(scs_inference,[],[1,103,2,3,4])). % 56.17/56.20 cnf(106,plain, % 56.17/56.20 (P1(f1(x1061),f3(a2))), % 56.17/56.20 inference(rename_variables,[],[1])). % 56.17/56.20 cnf(108,plain, % 56.17/56.20 (P2(a2,f1(f5(f5(a4))))), % 56.17/56.20 inference(scs_inference,[],[1,103,106,2,3,4,6])). % 56.17/56.20 cnf(109,plain, % 56.17/56.20 (P1(f1(x1091),f3(a2))), % 56.17/56.20 inference(rename_variables,[],[1])). % 56.17/56.20 cnf(111,plain, % 56.17/56.20 (P2(a2,f1(f5(f5(f5(a4)))))), % 56.17/56.20 inference(scs_inference,[],[1,103,106,109,2,3,4,6,7])). % 56.17/56.20 cnf(115,plain, % 56.17/56.20 (~P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(a4)))), % 56.17/56.20 inference(scs_inference,[],[102,105,10])). % 56.17/56.20 cnf(134,plain, % 56.17/56.20 (~P2(f1(a4),f1(f5(a4)))+P2(f1(a4),f1(f5(f5(a4))))), % 56.17/56.20 inference(scs_inference,[],[102,105,108,8,41])). % 56.17/56.20 cnf(148,plain, % 56.17/56.20 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(a4))))), % 56.17/56.20 inference(scs_inference,[],[134,98])). % 56.17/56.20 cnf(164,plain, % 56.17/56.20 (P2(f1(a4),f1(f5(a4)))+P2(f1(a4),f1(f5(f5(a4))))), % 56.17/56.20 inference(scs_inference,[],[148,115])). % 56.17/56.20 cnf(175,plain, % 56.17/56.20 (~P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(a4))))), % 56.17/56.20 inference(scs_inference,[],[102,105,111,108,9,90])). % 56.17/56.20 cnf(256,plain, % 56.17/56.20 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(f5(a4))))), % 56.17/56.20 inference(scs_inference,[],[98,175])). % 56.17/56.20 cnf(272,plain, % 56.17/56.20 (P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(a4))))), % 56.17/56.20 inference(scs_inference,[],[256,115])). % 56.17/56.20 cnf(288,plain, % 56.17/56.20 (~P2(f1(a4),f1(f5(f5(a4))))), % 56.17/56.20 inference(scs_inference,[],[272,175])). % 56.17/56.20 cnf(289,plain, % 56.17/56.20 (~P2(f1(a4),f1(f5(a4)))), % 56.17/56.20 inference(scs_inference,[],[288,134])). % 56.17/56.20 cnf(291,plain, % 56.17/56.20 (P2(f1(a4),f1(f5(a4)))), % 56.17/56.20 inference(scs_inference,[],[288,164])). % 56.17/56.20 cnf(293,plain, % 56.17/56.20 ($false), % 56.17/56.20 inference(scs_inference,[],[291,289]), % 56.17/56.20 ['proof']). % 56.17/56.20 % SZS output end Proof % 56.17/56.20 % Total time : 55.320000 s %------------------------------------------------------------------------------