%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO651-1 : TPTP v7.5.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n024.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 57.98s 58.03s % Output : CNFRefutation 57.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYO651-1 : TPTP v7.5.0. Released v7.3.0. % 0.11/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n024.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % RAMPerCPU : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Mar 14 13:46:18 EDT 2022 % 0.12/0.34 % 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.45 file=/export/starexec/sandbox2/benchmark/theBenchmark.p % 0.52/0.69 start to proof:theBenchmark % 57.98/58.03 % Version : CSE-F---1.0 % 57.98/58.03 % Problem : theBenchmark.p % 57.98/58.03 % Proof found % 57.98/58.03 % SZS status Theorem for theBenchmark.p % 57.98/58.03 % SZS output start Proof % 57.98/58.03 [2]~P1(f1(a4),a2) % 57.98/58.03 [1]P1(f1(x11),f3(a2)) % 57.98/58.03 [3]~P1(f1(x31),f3(a2))+P2(a2,f1(x31))+P1(f1(x31),a2) % 57.98/58.03 [4]P1(f1(x41),a2)+~P1(f1(f5(x41)),f3(a2))+P2(a2,f1(f5(x41))) % 57.98/58.03 [6]P1(f1(x61),a2)+~P1(f1(f5(f5(x61))),f3(a2))+P2(a2,f1(f5(f5(x61)))) % 57.98/58.03 [7]P1(f1(x71),a2)+~P1(f1(f5(f5(f5(x71)))),f3(a2))+P2(a2,f1(f5(f5(f5(x71))))) % 57.98/58.03 [10]P1(f1(x101),a2)+~P1(f1(f5(f5(f5(f5(x101))))),f3(a2))+P2(a2,f1(f5(f5(f5(f5(x101)))))) % 57.98/58.03 [5]P3(f5(x51),f5(x51))+~P2(a2,f1(x51))+P2(f1(x51),f1(f5(x51)))+~P2(a2,f1(f5(x51))) % 57.98/58.03 [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)))) % 57.98/58.03 [14]P3(f5(x141),f5(x141))+~P2(a2,f1(x141))+~P2(f1(x141),f1(f5(x141)))+~P2(f1(x141),f1(f5(f5(x141))))+~P2(a2,f1(f5(x141)))+P2(f1(x141),f1(f5(f5(f5(x141)))))+~P2(a2,f1(f5(f5(x141))))+~P2(a2,f1(f5(f5(f5(x141))))) % 57.98/58.03 [22]P3(f5(x221),f5(x221))+~P2(a2,f1(x221))+~P2(f1(x221),f1(f5(x221)))+~P2(f1(x221),f1(f5(f5(x221))))+~P2(a2,f1(f5(x221)))+~P2(f1(x221),f1(f5(f5(f5(x221)))))+~P2(a2,f1(f5(f5(x221))))+~P2(a2,f1(f5(f5(f5(x221)))))+~P2(a2,f1(f5(f5(f5(f5(x221)))))) % 57.98/58.03 [9]~P3(f5(x92),f5(x91))+~P3(f5(x93),f5(x92))+P2(f1(x91),f1(f5(x91)))+P2(f1(x92),f1(f5(x92)))+~P2(a2,f1(x91))+P2(f1(x93),f1(f5(x93)))+~P2(a2,f1(x92))+~P2(a2,f1(x93))+~P2(a2,f1(f5(x91)))+~P2(a2,f1(f5(x92)))+~P2(a2,f1(f5(x93))) % 57.98/58.03 [11]~P3(f5(x112),f5(x111))+~P3(f5(x113),f5(x112))+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(a2,f1(x113))+~P2(a2,f1(f5(x111)))+~P2(a2,f1(f5(x112)))+~P2(a2,f1(f5(x113)))+P2(f1(x113),f1(f5(f5(x113))))+~P2(a2,f1(f5(f5(x113)))) % 57.98/58.03 [12]~P3(f5(x122),f5(x123))+~P3(f5(x123),f5(x121))+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(a2,f1(x123))+~P2(a2,f1(f5(x121)))+~P2(a2,f1(f5(x122)))+~P2(a2,f1(f5(x123)))+P2(f1(x123),f1(f5(f5(x123))))+~P2(a2,f1(f5(f5(x123)))) % 57.98/58.03 [13]~P3(f5(x131),f5(x133))+~P3(f5(x132),f5(x131))+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(a2,f1(x133))+~P2(a2,f1(f5(x133)))+~P2(a2,f1(f5(x131)))+~P2(a2,f1(f5(x132)))+P2(f1(x133),f1(f5(f5(x133))))+~P2(a2,f1(f5(f5(x133)))) % 57.98/58.03 [15]~P3(f5(x152),f5(x153))+~P3(f5(x153),f5(x151))+P2(f1(x151),f1(f5(x151)))+~P2(a2,f1(x151))+~P2(f1(x152),f1(f5(x152)))+~P2(f1(x153),f1(f5(x153)))+~P2(a2,f1(x152))+~P2(a2,f1(x153))+~P2(a2,f1(f5(x151)))+~P2(a2,f1(f5(x152)))+~P2(a2,f1(f5(x153)))+P2(f1(x152),f1(f5(f5(x152))))+P2(f1(x153),f1(f5(f5(x153))))+~P2(a2,f1(f5(f5(x152))))+~P2(a2,f1(f5(f5(x153)))) % 57.98/58.03 [16]~P3(f5(x161),f5(x162))+~P3(f5(x163),f5(x161))+P2(f1(x161),f1(f5(x161)))+~P2(a2,f1(x161))+~P2(f1(x162),f1(f5(x162)))+~P2(f1(x163),f1(f5(x163)))+~P2(a2,f1(x162))+~P2(a2,f1(x163))+~P2(a2,f1(f5(x162)))+~P2(a2,f1(f5(x161)))+~P2(a2,f1(f5(x163)))+P2(f1(x162),f1(f5(f5(x162))))+P2(f1(x163),f1(f5(f5(x163))))+~P2(a2,f1(f5(f5(x162))))+~P2(a2,f1(f5(f5(x163)))) % 57.98/58.03 [17]~P3(f5(x171),f5(x173))+~P3(f5(x173),f5(x172))+P2(f1(x171),f1(f5(x171)))+~P2(a2,f1(x171))+~P2(f1(x172),f1(f5(x172)))+~P2(f1(x173),f1(f5(x173)))+~P2(a2,f1(x172))+~P2(a2,f1(x173))+~P2(a2,f1(f5(x172)))+~P2(a2,f1(f5(x171)))+~P2(a2,f1(f5(x173)))+P2(f1(x172),f1(f5(f5(x172))))+P2(f1(x173),f1(f5(f5(x173))))+~P2(a2,f1(f5(f5(x172))))+~P2(a2,f1(f5(f5(x173)))) % 57.98/58.03 [18]~P3(f5(x182),f5(x181))+~P3(f5(x183),f5(x182))+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(a2,f1(x183))+~P2(a2,f1(f5(x181)))+~P2(a2,f1(f5(x182)))+~P2(a2,f1(f5(x183)))+~P2(f1(x183),f1(f5(f5(x183))))+~P2(a2,f1(f5(f5(x183))))+P2(f1(x183),f1(f5(f5(f5(x183)))))+~P2(a2,f1(f5(f5(f5(x183))))) % 57.98/58.03 [19]~P3(f5(x192),f5(x193))+~P3(f5(x193),f5(x191))+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(a2,f1(x193))+~P2(a2,f1(f5(x191)))+~P2(a2,f1(f5(x192)))+~P2(a2,f1(f5(x193)))+~P2(f1(x193),f1(f5(f5(x193))))+~P2(a2,f1(f5(f5(x193))))+P2(f1(x193),f1(f5(f5(f5(x193)))))+~P2(a2,f1(f5(f5(f5(x193))))) % 57.98/58.03 [20]~P3(f5(x201),f5(x203))+~P3(f5(x202),f5(x201))+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(a2,f1(x203))+~P2(a2,f1(f5(x203)))+~P2(a2,f1(f5(x201)))+~P2(a2,f1(f5(x202)))+~P2(f1(x203),f1(f5(f5(x203))))+~P2(a2,f1(f5(f5(x203))))+P2(f1(x203),f1(f5(f5(f5(x203)))))+~P2(a2,f1(f5(f5(f5(x203))))) % 57.98/58.03 [32]~P3(f5(x322),f5(x321))+~P3(f5(x323),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(a2,f1(x322))+~P2(a2,f1(x323))+~P2(a2,f1(f5(x321)))+~P2(a2,f1(f5(x322)))+~P2(a2,f1(f5(x323)))+~P2(f1(x323),f1(f5(f5(x323))))+~P2(a2,f1(f5(f5(x323))))+~P2(f1(x323),f1(f5(f5(f5(x323)))))+~P2(a2,f1(f5(f5(f5(x323)))))+~P2(a2,f1(f5(f5(f5(f5(x323)))))) % 57.98/58.03 [33]~P3(f5(x332),f5(x333))+~P3(f5(x333),f5(x331))+P2(f1(x331),f1(f5(x331)))+P2(f1(x332),f1(f5(x332)))+~P2(a2,f1(x331))+~P2(f1(x333),f1(f5(x333)))+~P2(a2,f1(x332))+~P2(a2,f1(x333))+~P2(a2,f1(f5(x331)))+~P2(a2,f1(f5(x332)))+~P2(a2,f1(f5(x333)))+~P2(f1(x333),f1(f5(f5(x333))))+~P2(a2,f1(f5(f5(x333))))+~P2(f1(x333),f1(f5(f5(f5(x333)))))+~P2(a2,f1(f5(f5(f5(x333)))))+~P2(a2,f1(f5(f5(f5(f5(x333)))))) % 57.98/58.03 [34]~P3(f5(x341),f5(x343))+~P3(f5(x342),f5(x341))+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(a2,f1(x343))+~P2(a2,f1(f5(x343)))+~P2(a2,f1(f5(x341)))+~P2(a2,f1(f5(x342)))+~P2(f1(x343),f1(f5(f5(x343))))+~P2(a2,f1(f5(f5(x343))))+~P2(f1(x343),f1(f5(f5(f5(x343)))))+~P2(a2,f1(f5(f5(f5(x343)))))+~P2(a2,f1(f5(f5(f5(f5(x343)))))) % 57.98/58.03 [21]~P3(f5(x212),f5(x213))+~P3(f5(x213),f5(x211))+~P2(f1(x211),f1(f5(x211)))+~P2(a2,f1(x211))+~P2(f1(x212),f1(f5(x212)))+~P2(f1(x213),f1(f5(x213)))+~P2(a2,f1(x212))+~P2(a2,f1(x213))+~P2(a2,f1(f5(x211)))+~P2(a2,f1(f5(x212)))+~P2(a2,f1(f5(x213)))+P2(f1(x211),f1(f5(f5(x211))))+P2(f1(x212),f1(f5(f5(x212))))+P2(f1(x213),f1(f5(f5(x213))))+~P2(a2,f1(f5(f5(x211))))+~P2(a2,f1(f5(f5(x212))))+~P2(a2,f1(f5(f5(x213)))) % 57.98/58.03 [23]~P3(f5(x232),f5(x231))+~P3(f5(x233),f5(x232))+P2(f1(x231),f1(f5(x231)))+~P2(a2,f1(x231))+~P2(f1(x232),f1(f5(x232)))+~P2(f1(x233),f1(f5(x233)))+~P2(a2,f1(x232))+~P2(a2,f1(x233))+~P2(a2,f1(f5(x231)))+~P2(a2,f1(f5(x232)))+~P2(a2,f1(f5(x233)))+P2(f1(x232),f1(f5(f5(x232))))+~P2(f1(x233),f1(f5(f5(x233))))+~P2(a2,f1(f5(f5(x232))))+~P2(a2,f1(f5(f5(x233))))+P2(f1(x233),f1(f5(f5(f5(x233)))))+~P2(a2,f1(f5(f5(f5(x233))))) % 57.98/58.03 [24]~P3(f5(x242),f5(x243))+~P3(f5(x243),f5(x241))+P2(f1(x241),f1(f5(x241)))+~P2(a2,f1(x241))+~P2(f1(x242),f1(f5(x242)))+~P2(f1(x243),f1(f5(x243)))+~P2(a2,f1(x242))+~P2(a2,f1(x243))+~P2(a2,f1(f5(x241)))+~P2(a2,f1(f5(x242)))+~P2(a2,f1(f5(x243)))+P2(f1(x242),f1(f5(f5(x242))))+~P2(f1(x243),f1(f5(f5(x243))))+~P2(a2,f1(f5(f5(x242))))+~P2(a2,f1(f5(f5(x243))))+P2(f1(x243),f1(f5(f5(f5(x243)))))+~P2(a2,f1(f5(f5(f5(x243))))) % 57.98/58.03 [25]~P3(f5(x251),f5(x252))+~P3(f5(x253),f5(x251))+P2(f1(x251),f1(f5(x251)))+~P2(a2,f1(x251))+~P2(f1(x252),f1(f5(x252)))+~P2(f1(x253),f1(f5(x253)))+~P2(a2,f1(x252))+~P2(a2,f1(x253))+~P2(a2,f1(f5(x252)))+~P2(a2,f1(f5(x251)))+~P2(a2,f1(f5(x253)))+P2(f1(x252),f1(f5(f5(x252))))+~P2(f1(x253),f1(f5(f5(x253))))+~P2(a2,f1(f5(f5(x252))))+~P2(a2,f1(f5(f5(x253))))+P2(f1(x253),f1(f5(f5(f5(x253)))))+~P2(a2,f1(f5(f5(f5(x253))))) % 57.98/58.03 [26]~P3(f5(x261),f5(x263))+~P3(f5(x263),f5(x262))+P2(f1(x261),f1(f5(x261)))+~P2(a2,f1(x261))+~P2(f1(x262),f1(f5(x262)))+~P2(f1(x263),f1(f5(x263)))+~P2(a2,f1(x262))+~P2(a2,f1(x263))+~P2(a2,f1(f5(x262)))+~P2(a2,f1(f5(x261)))+~P2(a2,f1(f5(x263)))+P2(f1(x262),f1(f5(f5(x262))))+~P2(f1(x263),f1(f5(f5(x263))))+~P2(a2,f1(f5(f5(x262))))+~P2(a2,f1(f5(f5(x263))))+P2(f1(x263),f1(f5(f5(f5(x263)))))+~P2(a2,f1(f5(f5(f5(x263))))) % 57.98/58.03 [27]~P3(f5(x271),f5(x273))+~P3(f5(x272),f5(x271))+P2(f1(x271),f1(f5(x271)))+~P2(f1(x272),f1(f5(x272)))+~P2(a2,f1(x271))+~P2(f1(x273),f1(f5(x273)))+~P2(a2,f1(x272))+~P2(a2,f1(x273))+~P2(a2,f1(f5(x273)))+~P2(a2,f1(f5(x271)))+~P2(a2,f1(f5(x272)))+P2(f1(x272),f1(f5(f5(x272))))+~P2(f1(x273),f1(f5(f5(x273))))+~P2(a2,f1(f5(f5(x273))))+~P2(a2,f1(f5(f5(x272))))+P2(f1(x273),f1(f5(f5(f5(x273)))))+~P2(a2,f1(f5(f5(f5(x273))))) % 57.98/58.03 [28]~P3(f5(x281),f5(x282))+~P3(f5(x282),f5(x283))+P2(f1(x281),f1(f5(x281)))+~P2(f1(x282),f1(f5(x282)))+~P2(a2,f1(x281))+~P2(f1(x283),f1(f5(x283)))+~P2(a2,f1(x282))+~P2(a2,f1(x283))+~P2(a2,f1(f5(x283)))+~P2(a2,f1(f5(x281)))+~P2(a2,f1(f5(x282)))+P2(f1(x282),f1(f5(f5(x282))))+~P2(f1(x283),f1(f5(f5(x283))))+~P2(a2,f1(f5(f5(x283))))+~P2(a2,f1(f5(f5(x282))))+P2(f1(x283),f1(f5(f5(f5(x283)))))+~P2(a2,f1(f5(f5(f5(x283))))) % 57.98/58.03 [38]~P3(f5(x382),f5(x381))+~P3(f5(x383),f5(x382))+P2(f1(x381),f1(f5(x381)))+~P2(a2,f1(x381))+~P2(f1(x382),f1(f5(x382)))+~P2(f1(x383),f1(f5(x383)))+~P2(a2,f1(x382))+~P2(a2,f1(x383))+~P2(a2,f1(f5(x381)))+~P2(a2,f1(f5(x382)))+~P2(a2,f1(f5(x383)))+P2(f1(x382),f1(f5(f5(x382))))+~P2(f1(x383),f1(f5(f5(x383))))+~P2(a2,f1(f5(f5(x382))))+~P2(a2,f1(f5(f5(x383))))+~P2(f1(x383),f1(f5(f5(f5(x383)))))+~P2(a2,f1(f5(f5(f5(x383)))))+~P2(a2,f1(f5(f5(f5(f5(x383)))))) % 57.98/58.03 [39]~P3(f5(x392),f5(x393))+~P3(f5(x393),f5(x391))+P2(f1(x391),f1(f5(x391)))+~P2(a2,f1(x391))+~P2(f1(x392),f1(f5(x392)))+~P2(f1(x393),f1(f5(x393)))+~P2(a2,f1(x392))+~P2(a2,f1(x393))+~P2(a2,f1(f5(x391)))+~P2(a2,f1(f5(x392)))+~P2(a2,f1(f5(x393)))+P2(f1(x392),f1(f5(f5(x392))))+~P2(f1(x393),f1(f5(f5(x393))))+~P2(a2,f1(f5(f5(x392))))+~P2(a2,f1(f5(f5(x393))))+~P2(f1(x393),f1(f5(f5(f5(x393)))))+~P2(a2,f1(f5(f5(f5(x393)))))+~P2(a2,f1(f5(f5(f5(f5(x393)))))) % 57.98/58.03 [40]~P3(f5(x401),f5(x402))+~P3(f5(x403),f5(x401))+P2(f1(x401),f1(f5(x401)))+~P2(a2,f1(x401))+~P2(f1(x402),f1(f5(x402)))+~P2(f1(x403),f1(f5(x403)))+~P2(a2,f1(x402))+~P2(a2,f1(x403))+~P2(a2,f1(f5(x402)))+~P2(a2,f1(f5(x401)))+~P2(a2,f1(f5(x403)))+P2(f1(x402),f1(f5(f5(x402))))+~P2(f1(x403),f1(f5(f5(x403))))+~P2(a2,f1(f5(f5(x402))))+~P2(a2,f1(f5(f5(x403))))+~P2(f1(x403),f1(f5(f5(f5(x403)))))+~P2(a2,f1(f5(f5(f5(x403)))))+~P2(a2,f1(f5(f5(f5(f5(x403)))))) % 57.98/58.03 [41]~P3(f5(x411),f5(x413))+~P3(f5(x413),f5(x412))+P2(f1(x411),f1(f5(x411)))+~P2(a2,f1(x411))+~P2(f1(x412),f1(f5(x412)))+~P2(f1(x413),f1(f5(x413)))+~P2(a2,f1(x412))+~P2(a2,f1(x413))+~P2(a2,f1(f5(x412)))+~P2(a2,f1(f5(x411)))+~P2(a2,f1(f5(x413)))+P2(f1(x412),f1(f5(f5(x412))))+~P2(f1(x413),f1(f5(f5(x413))))+~P2(a2,f1(f5(f5(x412))))+~P2(a2,f1(f5(f5(x413))))+~P2(f1(x413),f1(f5(f5(f5(x413)))))+~P2(a2,f1(f5(f5(f5(x413)))))+~P2(a2,f1(f5(f5(f5(f5(x413)))))) % 57.98/58.03 [42]~P3(f5(x421),f5(x423))+~P3(f5(x422),f5(x421))+P2(f1(x421),f1(f5(x421)))+~P2(a2,f1(x421))+~P2(f1(x422),f1(f5(x422)))+~P2(f1(x423),f1(f5(x423)))+~P2(a2,f1(x422))+~P2(a2,f1(x423))+~P2(a2,f1(f5(x423)))+~P2(a2,f1(f5(x421)))+~P2(a2,f1(f5(x422)))+P2(f1(x422),f1(f5(f5(x422))))+~P2(f1(x423),f1(f5(f5(x423))))+~P2(a2,f1(f5(f5(x423))))+~P2(a2,f1(f5(f5(x422))))+~P2(f1(x423),f1(f5(f5(f5(x423)))))+~P2(a2,f1(f5(f5(f5(x423)))))+~P2(a2,f1(f5(f5(f5(f5(x423)))))) % 57.98/58.03 [43]~P3(f5(x431),f5(x432))+~P3(f5(x432),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(a2,f1(x432))+~P2(a2,f1(x433))+~P2(a2,f1(f5(x433)))+~P2(a2,f1(f5(x431)))+~P2(a2,f1(f5(x432)))+P2(f1(x432),f1(f5(f5(x432))))+~P2(f1(x433),f1(f5(f5(x433))))+~P2(a2,f1(f5(f5(x433))))+~P2(a2,f1(f5(f5(x432))))+~P2(f1(x433),f1(f5(f5(f5(x433)))))+~P2(a2,f1(f5(f5(f5(x433)))))+~P2(a2,f1(f5(f5(f5(f5(x433)))))) % 57.98/58.03 [29]~P3(f5(x292),f5(x291))+~P3(f5(x293),f5(x292))+~P2(f1(x291),f1(f5(x291)))+~P2(a2,f1(x291))+~P2(f1(x292),f1(f5(x292)))+~P2(f1(x293),f1(f5(x293)))+~P2(a2,f1(x292))+~P2(a2,f1(x293))+~P2(a2,f1(f5(x291)))+~P2(a2,f1(f5(x292)))+~P2(a2,f1(f5(x293)))+P2(f1(x291),f1(f5(f5(x291))))+P2(f1(x292),f1(f5(f5(x292))))+~P2(f1(x293),f1(f5(f5(x293))))+~P2(a2,f1(f5(f5(x291))))+~P2(a2,f1(f5(f5(x292))))+~P2(a2,f1(f5(f5(x293))))+P2(f1(x293),f1(f5(f5(f5(x293)))))+~P2(a2,f1(f5(f5(f5(x293))))) % 57.98/58.03 [30]~P3(f5(x302),f5(x303))+~P3(f5(x303),f5(x301))+~P2(f1(x301),f1(f5(x301)))+~P2(a2,f1(x301))+~P2(f1(x302),f1(f5(x302)))+~P2(f1(x303),f1(f5(x303)))+~P2(a2,f1(x302))+~P2(a2,f1(x303))+~P2(a2,f1(f5(x301)))+~P2(a2,f1(f5(x302)))+~P2(a2,f1(f5(x303)))+P2(f1(x301),f1(f5(f5(x301))))+P2(f1(x302),f1(f5(f5(x302))))+~P2(f1(x303),f1(f5(f5(x303))))+~P2(a2,f1(f5(f5(x301))))+~P2(a2,f1(f5(f5(x302))))+~P2(a2,f1(f5(f5(x303))))+P2(f1(x303),f1(f5(f5(f5(x303)))))+~P2(a2,f1(f5(f5(f5(x303))))) % 57.98/58.03 [31]~P3(f5(x311),f5(x312))+~P3(f5(x312),f5(x313))+~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(a2,f1(x313))+~P2(a2,f1(f5(x313)))+~P2(a2,f1(f5(x311)))+~P2(a2,f1(f5(x312)))+P2(f1(x311),f1(f5(f5(x311))))+P2(f1(x312),f1(f5(f5(x312))))+~P2(f1(x313),f1(f5(f5(x313))))+~P2(a2,f1(f5(f5(x313))))+~P2(a2,f1(f5(f5(x311))))+~P2(a2,f1(f5(f5(x312))))+P2(f1(x313),f1(f5(f5(f5(x313)))))+~P2(a2,f1(f5(f5(f5(x313))))) % 57.98/58.03 [35]~P3(f5(x352),f5(x351))+~P3(f5(x353),f5(x352))+P2(f1(x351),f1(f5(x351)))+~P2(a2,f1(x351))+~P2(f1(x352),f1(f5(x352)))+~P2(f1(x353),f1(f5(x353)))+~P2(a2,f1(x352))+~P2(a2,f1(x353))+~P2(a2,f1(f5(x351)))+~P2(a2,f1(f5(x352)))+~P2(a2,f1(f5(x353)))+~P2(f1(x352),f1(f5(f5(x352))))+~P2(f1(x353),f1(f5(f5(x353))))+~P2(a2,f1(f5(f5(x352))))+~P2(a2,f1(f5(f5(x353))))+P2(f1(x352),f1(f5(f5(f5(x352)))))+P2(f1(x353),f1(f5(f5(f5(x353)))))+~P2(a2,f1(f5(f5(f5(x352)))))+~P2(a2,f1(f5(f5(f5(x353))))) % 57.98/58.03 [36]~P3(f5(x361),f5(x362))+~P3(f5(x363),f5(x361))+P2(f1(x361),f1(f5(x361)))+~P2(a2,f1(x361))+~P2(f1(x362),f1(f5(x362)))+~P2(f1(x363),f1(f5(x363)))+~P2(a2,f1(x362))+~P2(a2,f1(x363))+~P2(a2,f1(f5(x362)))+~P2(a2,f1(f5(x361)))+~P2(a2,f1(f5(x363)))+~P2(f1(x362),f1(f5(f5(x362))))+~P2(f1(x363),f1(f5(f5(x363))))+~P2(a2,f1(f5(f5(x362))))+~P2(a2,f1(f5(f5(x363))))+P2(f1(x362),f1(f5(f5(f5(x362)))))+P2(f1(x363),f1(f5(f5(f5(x363)))))+~P2(a2,f1(f5(f5(f5(x362)))))+~P2(a2,f1(f5(f5(f5(x363))))) % 57.98/58.03 [37]~P3(f5(x371),f5(x373))+~P3(f5(x373),f5(x372))+P2(f1(x371),f1(f5(x371)))+~P2(a2,f1(x371))+~P2(f1(x372),f1(f5(x372)))+~P2(f1(x373),f1(f5(x373)))+~P2(a2,f1(x372))+~P2(a2,f1(x373))+~P2(a2,f1(f5(x372)))+~P2(a2,f1(f5(x371)))+~P2(a2,f1(f5(x373)))+~P2(f1(x372),f1(f5(f5(x372))))+~P2(f1(x373),f1(f5(f5(x373))))+~P2(a2,f1(f5(f5(x372))))+~P2(a2,f1(f5(f5(x373))))+P2(f1(x372),f1(f5(f5(f5(x372)))))+P2(f1(x373),f1(f5(f5(f5(x373)))))+~P2(a2,f1(f5(f5(f5(x372)))))+~P2(a2,f1(f5(f5(f5(x373))))) % 57.98/58.03 [47]~P3(f5(x472),f5(x471))+~P3(f5(x473),f5(x472))+~P2(f1(x471),f1(f5(x471)))+~P2(a2,f1(x471))+~P2(f1(x472),f1(f5(x472)))+~P2(f1(x473),f1(f5(x473)))+~P2(a2,f1(x472))+~P2(a2,f1(x473))+~P2(a2,f1(f5(x471)))+~P2(a2,f1(f5(x472)))+~P2(a2,f1(f5(x473)))+P2(f1(x471),f1(f5(f5(x471))))+P2(f1(x472),f1(f5(f5(x472))))+~P2(f1(x473),f1(f5(f5(x473))))+~P2(a2,f1(f5(f5(x471))))+~P2(a2,f1(f5(f5(x472))))+~P2(a2,f1(f5(f5(x473))))+~P2(f1(x473),f1(f5(f5(f5(x473)))))+~P2(a2,f1(f5(f5(f5(x473)))))+~P2(a2,f1(f5(f5(f5(f5(x473)))))) % 57.98/58.03 [48]~P3(f5(x482),f5(x483))+~P3(f5(x483),f5(x481))+~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(a2,f1(x483))+~P2(a2,f1(f5(x481)))+~P2(a2,f1(f5(x482)))+~P2(a2,f1(f5(x483)))+P2(f1(x481),f1(f5(f5(x481))))+P2(f1(x482),f1(f5(f5(x482))))+~P2(f1(x483),f1(f5(f5(x483))))+~P2(a2,f1(f5(f5(x481))))+~P2(a2,f1(f5(f5(x482))))+~P2(a2,f1(f5(f5(x483))))+~P2(f1(x483),f1(f5(f5(f5(x483)))))+~P2(a2,f1(f5(f5(f5(x483)))))+~P2(a2,f1(f5(f5(f5(f5(x483)))))) % 57.98/58.04 [49]~P3(f5(x491),f5(x492))+~P3(f5(x492),f5(x493))+~P2(f1(x491),f1(f5(x491)))+~P2(a2,f1(x491))+~P2(f1(x492),f1(f5(x492)))+~P2(f1(x493),f1(f5(x493)))+~P2(a2,f1(x492))+~P2(a2,f1(x493))+~P2(a2,f1(f5(x493)))+~P2(a2,f1(f5(x491)))+~P2(a2,f1(f5(x492)))+P2(f1(x491),f1(f5(f5(x491))))+P2(f1(x492),f1(f5(f5(x492))))+~P2(f1(x493),f1(f5(f5(x493))))+~P2(a2,f1(f5(f5(x493))))+~P2(a2,f1(f5(f5(x491))))+~P2(a2,f1(f5(f5(x492))))+~P2(f1(x493),f1(f5(f5(f5(x493)))))+~P2(a2,f1(f5(f5(f5(x493)))))+~P2(a2,f1(f5(f5(f5(f5(x493)))))) % 57.98/58.04 [50]~P3(f5(x502),f5(x501))+~P3(f5(x503),f5(x502))+P2(f1(x501),f1(f5(x501)))+~P2(a2,f1(x501))+~P2(f1(x502),f1(f5(x502)))+~P2(f1(x503),f1(f5(x503)))+~P2(a2,f1(x502))+~P2(a2,f1(x503))+~P2(a2,f1(f5(x501)))+~P2(a2,f1(f5(x502)))+~P2(a2,f1(f5(x503)))+~P2(f1(x502),f1(f5(f5(x502))))+~P2(f1(x503),f1(f5(f5(x503))))+~P2(a2,f1(f5(f5(x502))))+~P2(a2,f1(f5(f5(x503))))+P2(f1(x502),f1(f5(f5(f5(x502)))))+~P2(f1(x503),f1(f5(f5(f5(x503)))))+~P2(a2,f1(f5(f5(f5(x502)))))+~P2(a2,f1(f5(f5(f5(x503)))))+~P2(a2,f1(f5(f5(f5(f5(x503)))))) % 57.98/58.04 [51]~P3(f5(x513),f5(x511))+~P3(f5(x512),f5(x513))+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(a2,f1(x513))+~P2(a2,f1(f5(x511)))+~P2(a2,f1(f5(x513)))+~P2(a2,f1(f5(x512)))+~P2(f1(x512),f1(f5(f5(x512))))+~P2(f1(x513),f1(f5(f5(x513))))+~P2(a2,f1(f5(f5(x513))))+~P2(a2,f1(f5(f5(x512))))+P2(f1(x512),f1(f5(f5(f5(x512)))))+~P2(f1(x513),f1(f5(f5(f5(x513)))))+~P2(a2,f1(f5(f5(f5(x513)))))+~P2(a2,f1(f5(f5(f5(x512)))))+~P2(a2,f1(f5(f5(f5(f5(x513)))))) % 57.98/58.04 [52]~P3(f5(x521),f5(x522))+~P3(f5(x523),f5(x521))+P2(f1(x521),f1(f5(x521)))+~P2(a2,f1(x521))+~P2(f1(x522),f1(f5(x522)))+~P2(f1(x523),f1(f5(x523)))+~P2(a2,f1(x522))+~P2(a2,f1(x523))+~P2(a2,f1(f5(x522)))+~P2(a2,f1(f5(x521)))+~P2(a2,f1(f5(x523)))+~P2(f1(x522),f1(f5(f5(x522))))+~P2(f1(x523),f1(f5(f5(x523))))+~P2(a2,f1(f5(f5(x522))))+~P2(a2,f1(f5(f5(x523))))+P2(f1(x522),f1(f5(f5(f5(x522)))))+~P2(f1(x523),f1(f5(f5(f5(x523)))))+~P2(a2,f1(f5(f5(f5(x522)))))+~P2(a2,f1(f5(f5(f5(x523)))))+~P2(a2,f1(f5(f5(f5(f5(x523)))))) % 57.98/58.04 [53]~P3(f5(x531),f5(x533))+~P3(f5(x533),f5(x532))+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(a2,f1(x533))+~P2(a2,f1(f5(x532)))+~P2(a2,f1(f5(x531)))+~P2(a2,f1(f5(x533)))+~P2(f1(x532),f1(f5(f5(x532))))+~P2(f1(x533),f1(f5(f5(x533))))+~P2(a2,f1(f5(f5(x532))))+~P2(a2,f1(f5(f5(x533))))+P2(f1(x532),f1(f5(f5(f5(x532)))))+~P2(f1(x533),f1(f5(f5(f5(x533)))))+~P2(a2,f1(f5(f5(f5(x532)))))+~P2(a2,f1(f5(f5(f5(x533)))))+~P2(a2,f1(f5(f5(f5(f5(x533)))))) % 57.98/58.04 [54]~P3(f5(x541),f5(x543))+~P3(f5(x542),f5(x541))+P2(f1(x541),f1(f5(x541)))+~P2(a2,f1(x541))+~P2(f1(x542),f1(f5(x542)))+~P2(f1(x543),f1(f5(x543)))+~P2(a2,f1(x542))+~P2(a2,f1(x543))+~P2(a2,f1(f5(x543)))+~P2(a2,f1(f5(x541)))+~P2(a2,f1(f5(x542)))+~P2(f1(x542),f1(f5(f5(x542))))+~P2(f1(x543),f1(f5(f5(x543))))+~P2(a2,f1(f5(f5(x543))))+~P2(a2,f1(f5(f5(x542))))+P2(f1(x542),f1(f5(f5(f5(x542)))))+~P2(f1(x543),f1(f5(f5(f5(x543)))))+~P2(a2,f1(f5(f5(f5(x543)))))+~P2(a2,f1(f5(f5(f5(x542)))))+~P2(a2,f1(f5(f5(f5(f5(x543)))))) % 57.98/58.04 [55]~P3(f5(x551),f5(x552))+~P3(f5(x552),f5(x553))+P2(f1(x551),f1(f5(x551)))+~P2(a2,f1(x551))+~P2(f1(x552),f1(f5(x552)))+~P2(f1(x553),f1(f5(x553)))+~P2(a2,f1(x552))+~P2(a2,f1(x553))+~P2(a2,f1(f5(x553)))+~P2(a2,f1(f5(x551)))+~P2(a2,f1(f5(x552)))+~P2(f1(x552),f1(f5(f5(x552))))+~P2(f1(x553),f1(f5(f5(x553))))+~P2(a2,f1(f5(f5(x553))))+~P2(a2,f1(f5(f5(x552))))+P2(f1(x552),f1(f5(f5(f5(x552)))))+~P2(f1(x553),f1(f5(f5(f5(x553)))))+~P2(a2,f1(f5(f5(f5(x553)))))+~P2(a2,f1(f5(f5(f5(x552)))))+~P2(a2,f1(f5(f5(f5(f5(x553)))))) % 57.98/58.04 [44]~P3(f5(x442),f5(x441))+~P3(f5(x443),f5(x442))+~P2(f1(x441),f1(f5(x441)))+~P2(f1(x442),f1(f5(x442)))+~P2(a2,f1(x441))+~P2(f1(x443),f1(f5(x443)))+~P2(a2,f1(x442))+~P2(a2,f1(x443))+~P2(a2,f1(f5(x441)))+~P2(a2,f1(f5(x442)))+~P2(a2,f1(f5(x443)))+P2(f1(x441),f1(f5(f5(x441))))+~P2(f1(x442),f1(f5(f5(x442))))+~P2(f1(x443),f1(f5(f5(x443))))+~P2(a2,f1(f5(f5(x441))))+~P2(a2,f1(f5(f5(x442))))+~P2(a2,f1(f5(f5(x443))))+P2(f1(x442),f1(f5(f5(f5(x442)))))+P2(f1(x443),f1(f5(f5(f5(x443)))))+~P2(a2,f1(f5(f5(f5(x442)))))+~P2(a2,f1(f5(f5(f5(x443))))) % 57.98/58.04 [45]~P3(f5(x451),f5(x452))+~P3(f5(x453),f5(x451))+~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(a2,f1(x453))+~P2(a2,f1(f5(x452)))+~P2(a2,f1(f5(x451)))+~P2(a2,f1(f5(x453)))+P2(f1(x451),f1(f5(f5(x451))))+~P2(f1(x452),f1(f5(f5(x452))))+~P2(f1(x453),f1(f5(f5(x453))))+~P2(a2,f1(f5(f5(x452))))+~P2(a2,f1(f5(f5(x451))))+~P2(a2,f1(f5(f5(x453))))+P2(f1(x452),f1(f5(f5(f5(x452)))))+P2(f1(x453),f1(f5(f5(f5(x453)))))+~P2(a2,f1(f5(f5(f5(x452)))))+~P2(a2,f1(f5(f5(f5(x453))))) % 57.98/58.04 [46]~P3(f5(x461),f5(x463))+~P3(f5(x463),f5(x462))+~P2(f1(x461),f1(f5(x461)))+~P2(a2,f1(x461))+~P2(f1(x462),f1(f5(x462)))+~P2(f1(x463),f1(f5(x463)))+~P2(a2,f1(x462))+~P2(a2,f1(x463))+~P2(a2,f1(f5(x462)))+~P2(a2,f1(f5(x461)))+~P2(a2,f1(f5(x463)))+P2(f1(x461),f1(f5(f5(x461))))+~P2(f1(x462),f1(f5(f5(x462))))+~P2(f1(x463),f1(f5(f5(x463))))+~P2(a2,f1(f5(f5(x462))))+~P2(a2,f1(f5(f5(x461))))+~P2(a2,f1(f5(f5(x463))))+P2(f1(x462),f1(f5(f5(f5(x462)))))+P2(f1(x463),f1(f5(f5(f5(x463)))))+~P2(a2,f1(f5(f5(f5(x462)))))+~P2(a2,f1(f5(f5(f5(x463))))) % 57.98/58.04 [63]~P3(f5(x632),f5(x631))+~P3(f5(x633),f5(x632))+P2(f1(x631),f1(f5(x631)))+~P2(a2,f1(x631))+~P2(f1(x632),f1(f5(x632)))+~P2(f1(x633),f1(f5(x633)))+~P2(a2,f1(x632))+~P2(a2,f1(x633))+~P2(a2,f1(f5(x631)))+~P2(a2,f1(f5(x632)))+~P2(a2,f1(f5(x633)))+~P2(f1(x632),f1(f5(f5(x632))))+~P2(f1(x633),f1(f5(f5(x633))))+~P2(a2,f1(f5(f5(x632))))+~P2(a2,f1(f5(f5(x633))))+~P2(f1(x632),f1(f5(f5(f5(x632)))))+~P2(f1(x633),f1(f5(f5(f5(x633)))))+~P2(a2,f1(f5(f5(f5(x632)))))+~P2(a2,f1(f5(f5(f5(x633)))))+~P2(a2,f1(f5(f5(f5(f5(x632))))))+~P2(a2,f1(f5(f5(f5(f5(x633)))))) % 57.98/58.04 [64]~P3(f5(x641),f5(x642))+~P3(f5(x643),f5(x641))+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(a2,f1(x643))+~P2(a2,f1(f5(x641)))+~P2(a2,f1(f5(x643)))+~P2(a2,f1(f5(x642)))+~P2(f1(x642),f1(f5(f5(x642))))+~P2(f1(x643),f1(f5(f5(x643))))+~P2(a2,f1(f5(f5(x642))))+~P2(a2,f1(f5(f5(x643))))+~P2(f1(x642),f1(f5(f5(f5(x642)))))+~P2(f1(x643),f1(f5(f5(f5(x643)))))+~P2(a2,f1(f5(f5(f5(x642)))))+~P2(a2,f1(f5(f5(f5(x643)))))+~P2(a2,f1(f5(f5(f5(f5(x642))))))+~P2(a2,f1(f5(f5(f5(f5(x643)))))) % 57.98/58.04 [65]~P3(f5(x651),f5(x653))+~P3(f5(x653),f5(x652))+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(a2,f1(x653))+~P2(a2,f1(f5(x651)))+~P2(a2,f1(f5(x653)))+~P2(a2,f1(f5(x652)))+~P2(f1(x652),f1(f5(f5(x652))))+~P2(f1(x653),f1(f5(f5(x653))))+~P2(a2,f1(f5(f5(x652))))+~P2(a2,f1(f5(f5(x653))))+~P2(f1(x652),f1(f5(f5(f5(x652)))))+~P2(f1(x653),f1(f5(f5(f5(x653)))))+~P2(a2,f1(f5(f5(f5(x652)))))+~P2(a2,f1(f5(f5(f5(x653)))))+~P2(a2,f1(f5(f5(f5(f5(x652))))))+~P2(a2,f1(f5(f5(f5(f5(x653)))))) % 57.98/58.04 [57]~P3(f5(x572),f5(x571))+~P3(f5(x573),f5(x572))+~P2(f1(x571),f1(f5(x571)))+~P2(a2,f1(x571))+~P2(f1(x572),f1(f5(x572)))+~P2(f1(x573),f1(f5(x573)))+~P2(a2,f1(x572))+~P2(a2,f1(x573))+~P2(a2,f1(f5(x571)))+~P2(a2,f1(f5(x572)))+~P2(a2,f1(f5(x573)))+P2(f1(x571),f1(f5(f5(x571))))+~P2(f1(x572),f1(f5(f5(x572))))+~P2(f1(x573),f1(f5(f5(x573))))+~P2(a2,f1(f5(f5(x571))))+~P2(a2,f1(f5(f5(x572))))+~P2(a2,f1(f5(f5(x573))))+P2(f1(x572),f1(f5(f5(f5(x572)))))+~P2(f1(x573),f1(f5(f5(f5(x573)))))+~P2(a2,f1(f5(f5(f5(x572)))))+~P2(a2,f1(f5(f5(f5(x573)))))+~P2(a2,f1(f5(f5(f5(f5(x573)))))) % 57.98/58.04 [58]~P3(f5(x583),f5(x581))+~P3(f5(x582),f5(x583))+~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(a2,f1(x583))+~P2(a2,f1(f5(x581)))+~P2(a2,f1(f5(x583)))+~P2(a2,f1(f5(x582)))+P2(f1(x581),f1(f5(f5(x581))))+~P2(f1(x582),f1(f5(f5(x582))))+~P2(f1(x583),f1(f5(f5(x583))))+~P2(a2,f1(f5(f5(x581))))+~P2(a2,f1(f5(f5(x583))))+~P2(a2,f1(f5(f5(x582))))+P2(f1(x582),f1(f5(f5(f5(x582)))))+~P2(f1(x583),f1(f5(f5(f5(x583)))))+~P2(a2,f1(f5(f5(f5(x583)))))+~P2(a2,f1(f5(f5(f5(x582)))))+~P2(a2,f1(f5(f5(f5(f5(x583)))))) % 57.98/58.04 [59]~P3(f5(x591),f5(x592))+~P3(f5(x593),f5(x591))+~P2(f1(x591),f1(f5(x591)))+~P2(a2,f1(x591))+~P2(f1(x592),f1(f5(x592)))+~P2(f1(x593),f1(f5(x593)))+~P2(a2,f1(x592))+~P2(a2,f1(x593))+~P2(a2,f1(f5(x592)))+~P2(a2,f1(f5(x591)))+~P2(a2,f1(f5(x593)))+P2(f1(x591),f1(f5(f5(x591))))+~P2(f1(x592),f1(f5(f5(x592))))+~P2(f1(x593),f1(f5(f5(x593))))+~P2(a2,f1(f5(f5(x592))))+~P2(a2,f1(f5(f5(x591))))+~P2(a2,f1(f5(f5(x593))))+P2(f1(x592),f1(f5(f5(f5(x592)))))+~P2(f1(x593),f1(f5(f5(f5(x593)))))+~P2(a2,f1(f5(f5(f5(x592)))))+~P2(a2,f1(f5(f5(f5(x593)))))+~P2(a2,f1(f5(f5(f5(f5(x593)))))) % 57.98/58.04 [60]~P3(f5(x601),f5(x603))+~P3(f5(x603),f5(x602))+~P2(f1(x601),f1(f5(x601)))+~P2(a2,f1(x601))+~P2(f1(x602),f1(f5(x602)))+~P2(f1(x603),f1(f5(x603)))+~P2(a2,f1(x602))+~P2(a2,f1(x603))+~P2(a2,f1(f5(x602)))+~P2(a2,f1(f5(x601)))+~P2(a2,f1(f5(x603)))+P2(f1(x601),f1(f5(f5(x601))))+~P2(f1(x602),f1(f5(f5(x602))))+~P2(f1(x603),f1(f5(f5(x603))))+~P2(a2,f1(f5(f5(x602))))+~P2(a2,f1(f5(f5(x601))))+~P2(a2,f1(f5(f5(x603))))+P2(f1(x602),f1(f5(f5(f5(x602)))))+~P2(f1(x603),f1(f5(f5(f5(x603)))))+~P2(a2,f1(f5(f5(f5(x602)))))+~P2(a2,f1(f5(f5(f5(x603)))))+~P2(a2,f1(f5(f5(f5(f5(x603)))))) % 57.98/58.04 [61]~P3(f5(x611),f5(x613))+~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(a2,f1(x613))+~P2(a2,f1(f5(x613)))+~P2(a2,f1(f5(x611)))+~P2(a2,f1(f5(x612)))+P2(f1(x611),f1(f5(f5(x611))))+~P2(f1(x612),f1(f5(f5(x612))))+~P2(f1(x613),f1(f5(f5(x613))))+~P2(a2,f1(f5(f5(x613))))+~P2(a2,f1(f5(f5(x611))))+~P2(a2,f1(f5(f5(x612))))+P2(f1(x612),f1(f5(f5(f5(x612)))))+~P2(f1(x613),f1(f5(f5(f5(x613)))))+~P2(a2,f1(f5(f5(f5(x613)))))+~P2(a2,f1(f5(f5(f5(x612)))))+~P2(a2,f1(f5(f5(f5(f5(x613)))))) % 57.98/58.04 [62]~P3(f5(x621),f5(x622))+~P3(f5(x622),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(a2,f1(x622))+~P2(a2,f1(x623))+~P2(a2,f1(f5(x623)))+~P2(a2,f1(f5(x621)))+~P2(a2,f1(f5(x622)))+P2(f1(x621),f1(f5(f5(x621))))+~P2(f1(x622),f1(f5(f5(x622))))+~P2(f1(x623),f1(f5(f5(x623))))+~P2(a2,f1(f5(f5(x623))))+~P2(a2,f1(f5(f5(x621))))+~P2(a2,f1(f5(f5(x622))))+P2(f1(x622),f1(f5(f5(f5(x622)))))+~P2(f1(x623),f1(f5(f5(f5(x623)))))+~P2(a2,f1(f5(f5(f5(x623)))))+~P2(a2,f1(f5(f5(f5(x622)))))+~P2(a2,f1(f5(f5(f5(f5(x623)))))) % 57.98/58.04 [56]~P3(f5(x562),f5(x561))+~P3(f5(x563),f5(x562))+~P2(f1(x561),f1(f5(x561)))+~P2(a2,f1(x561))+~P2(f1(x562),f1(f5(x562)))+~P2(f1(x563),f1(f5(x563)))+~P2(a2,f1(x562))+~P2(a2,f1(x563))+~P2(a2,f1(f5(x561)))+~P2(a2,f1(f5(x562)))+~P2(a2,f1(f5(x563)))+~P2(f1(x561),f1(f5(f5(x561))))+~P2(f1(x562),f1(f5(f5(x562))))+~P2(f1(x563),f1(f5(f5(x563))))+~P2(a2,f1(f5(f5(x561))))+~P2(a2,f1(f5(f5(x562))))+~P2(a2,f1(f5(f5(x563))))+P2(f1(x561),f1(f5(f5(f5(x561)))))+P2(f1(x562),f1(f5(f5(f5(x562)))))+P2(f1(x563),f1(f5(f5(f5(x563)))))+~P2(a2,f1(f5(f5(f5(x561)))))+~P2(a2,f1(f5(f5(f5(x562)))))+~P2(a2,f1(f5(f5(f5(x563))))) % 57.98/58.04 [69]~P3(f5(x692),f5(x691))+~P3(f5(x693),f5(x692))+~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(a2,f1(x693))+~P2(a2,f1(f5(x692)))+~P2(a2,f1(f5(x693)))+~P2(a2,f1(f5(x691)))+P2(f1(x691),f1(f5(f5(x691))))+~P2(f1(x692),f1(f5(f5(x692))))+~P2(f1(x693),f1(f5(f5(x693))))+~P2(a2,f1(f5(f5(x693))))+~P2(a2,f1(f5(f5(x692))))+~P2(a2,f1(f5(f5(x691))))+~P2(f1(x692),f1(f5(f5(f5(x692)))))+~P2(f1(x693),f1(f5(f5(f5(x693)))))+~P2(a2,f1(f5(f5(f5(x692)))))+~P2(a2,f1(f5(f5(f5(x693)))))+~P2(a2,f1(f5(f5(f5(f5(x692))))))+~P2(a2,f1(f5(f5(f5(f5(x693)))))) % 57.98/58.04 [70]~P3(f5(x701),f5(x702))+~P3(f5(x703),f5(x701))+~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(a2,f1(x703))+~P2(a2,f1(f5(x701)))+~P2(a2,f1(f5(x703)))+~P2(a2,f1(f5(x702)))+P2(f1(x701),f1(f5(f5(x701))))+~P2(f1(x702),f1(f5(f5(x702))))+~P2(f1(x703),f1(f5(f5(x703))))+~P2(a2,f1(f5(f5(x702))))+~P2(a2,f1(f5(f5(x701))))+~P2(a2,f1(f5(f5(x703))))+~P2(f1(x702),f1(f5(f5(f5(x702)))))+~P2(f1(x703),f1(f5(f5(f5(x703)))))+~P2(a2,f1(f5(f5(f5(x702)))))+~P2(a2,f1(f5(f5(f5(x703)))))+~P2(a2,f1(f5(f5(f5(f5(x702))))))+~P2(a2,f1(f5(f5(f5(f5(x703)))))) % 57.98/58.04 [71]~P3(f5(x711),f5(x713))+~P3(f5(x713),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(a2,f1(x713))+~P2(a2,f1(f5(x711)))+~P2(a2,f1(f5(x713)))+~P2(a2,f1(f5(x712)))+P2(f1(x711),f1(f5(f5(x711))))+~P2(f1(x712),f1(f5(f5(x712))))+~P2(f1(x713),f1(f5(f5(x713))))+~P2(a2,f1(f5(f5(x712))))+~P2(a2,f1(f5(f5(x711))))+~P2(a2,f1(f5(f5(x713))))+~P2(f1(x712),f1(f5(f5(f5(x712)))))+~P2(f1(x713),f1(f5(f5(f5(x713)))))+~P2(a2,f1(f5(f5(f5(x712)))))+~P2(a2,f1(f5(f5(f5(x713)))))+~P2(a2,f1(f5(f5(f5(f5(x712))))))+~P2(a2,f1(f5(f5(f5(f5(x713)))))) % 57.98/58.04 [66]~P3(f5(x662),f5(x661))+~P3(f5(x663),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(a2,f1(x663))+~P2(a2,f1(f5(x661)))+~P2(a2,f1(f5(x662)))+~P2(a2,f1(f5(x663)))+~P2(f1(x661),f1(f5(f5(x661))))+~P2(f1(x662),f1(f5(f5(x662))))+~P2(f1(x663),f1(f5(f5(x663))))+~P2(a2,f1(f5(f5(x662))))+~P2(a2,f1(f5(f5(x663))))+~P2(a2,f1(f5(f5(x661))))+P2(f1(x661),f1(f5(f5(f5(x661)))))+P2(f1(x662),f1(f5(f5(f5(x662)))))+~P2(f1(x663),f1(f5(f5(f5(x663)))))+~P2(a2,f1(f5(f5(f5(x661)))))+~P2(a2,f1(f5(f5(f5(x662)))))+~P2(a2,f1(f5(f5(f5(x663)))))+~P2(a2,f1(f5(f5(f5(f5(x663)))))) % 57.98/58.04 [67]~P3(f5(x673),f5(x671))+~P3(f5(x672),f5(x673))+~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(a2,f1(x673))+~P2(a2,f1(f5(x671)))+~P2(a2,f1(f5(x673)))+~P2(a2,f1(f5(x672)))+~P2(f1(x671),f1(f5(f5(x671))))+~P2(f1(x672),f1(f5(f5(x672))))+~P2(f1(x673),f1(f5(f5(x673))))+~P2(a2,f1(f5(f5(x671))))+~P2(a2,f1(f5(f5(x673))))+~P2(a2,f1(f5(f5(x672))))+P2(f1(x671),f1(f5(f5(f5(x671)))))+P2(f1(x672),f1(f5(f5(f5(x672)))))+~P2(f1(x673),f1(f5(f5(f5(x673)))))+~P2(a2,f1(f5(f5(f5(x671)))))+~P2(a2,f1(f5(f5(f5(x673)))))+~P2(a2,f1(f5(f5(f5(x672)))))+~P2(a2,f1(f5(f5(f5(f5(x673)))))) % 57.98/58.04 [68]~P3(f5(x681),f5(x683))+~P3(f5(x682),f5(x681))+~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(a2,f1(x683))+~P2(a2,f1(f5(x683)))+~P2(a2,f1(f5(x681)))+~P2(a2,f1(f5(x682)))+~P2(f1(x681),f1(f5(f5(x681))))+~P2(f1(x682),f1(f5(f5(x682))))+~P2(f1(x683),f1(f5(f5(x683))))+~P2(a2,f1(f5(f5(x683))))+~P2(a2,f1(f5(f5(x681))))+~P2(a2,f1(f5(f5(x682))))+P2(f1(x681),f1(f5(f5(f5(x681)))))+P2(f1(x682),f1(f5(f5(f5(x682)))))+~P2(f1(x683),f1(f5(f5(f5(x683)))))+~P2(a2,f1(f5(f5(f5(x683)))))+~P2(a2,f1(f5(f5(f5(x681)))))+~P2(a2,f1(f5(f5(f5(x682)))))+~P2(a2,f1(f5(f5(f5(f5(x683)))))) % 57.98/58.04 [72]~P3(f5(x722),f5(x721))+~P3(f5(x723),f5(x722))+~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(a2,f1(x723))+~P2(a2,f1(f5(x721)))+~P2(a2,f1(f5(x722)))+~P2(a2,f1(f5(x723)))+~P2(f1(x721),f1(f5(f5(x721))))+~P2(f1(x722),f1(f5(f5(x722))))+~P2(f1(x723),f1(f5(f5(x723))))+~P2(a2,f1(f5(f5(x721))))+~P2(a2,f1(f5(f5(x723))))+~P2(a2,f1(f5(f5(x722))))+P2(f1(x721),f1(f5(f5(f5(x721)))))+~P2(f1(x722),f1(f5(f5(f5(x722)))))+~P2(f1(x723),f1(f5(f5(f5(x723)))))+~P2(a2,f1(f5(f5(f5(x721)))))+~P2(a2,f1(f5(f5(f5(x722)))))+~P2(a2,f1(f5(f5(f5(x723)))))+~P2(a2,f1(f5(f5(f5(f5(x722))))))+~P2(a2,f1(f5(f5(f5(f5(x723)))))) % 57.98/58.04 [73]~P3(f5(x731),f5(x732))+~P3(f5(x733),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(a2,f1(x733))+~P2(a2,f1(f5(x732)))+~P2(a2,f1(f5(x731)))+~P2(a2,f1(f5(x733)))+~P2(f1(x731),f1(f5(f5(x731))))+~P2(f1(x732),f1(f5(f5(x732))))+~P2(f1(x733),f1(f5(f5(x733))))+~P2(a2,f1(f5(f5(x732))))+~P2(a2,f1(f5(f5(x733))))+~P2(a2,f1(f5(f5(x731))))+P2(f1(x731),f1(f5(f5(f5(x731)))))+~P2(f1(x732),f1(f5(f5(f5(x732)))))+~P2(f1(x733),f1(f5(f5(f5(x733)))))+~P2(a2,f1(f5(f5(f5(x732)))))+~P2(a2,f1(f5(f5(f5(x731)))))+~P2(a2,f1(f5(f5(f5(x733)))))+~P2(a2,f1(f5(f5(f5(f5(x732))))))+~P2(a2,f1(f5(f5(f5(f5(x733)))))) % 57.98/58.04 [74]~P3(f5(x743),f5(x742))+~P3(f5(x741),f5(x743))+~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(a2,f1(x743))+~P2(a2,f1(f5(x742)))+~P2(a2,f1(f5(x743)))+~P2(a2,f1(f5(x741)))+~P2(f1(x741),f1(f5(f5(x741))))+~P2(f1(x742),f1(f5(f5(x742))))+~P2(f1(x743),f1(f5(f5(x743))))+~P2(a2,f1(f5(f5(x742))))+~P2(a2,f1(f5(f5(x741))))+~P2(a2,f1(f5(f5(x743))))+P2(f1(x741),f1(f5(f5(f5(x741)))))+~P2(f1(x742),f1(f5(f5(f5(x742)))))+~P2(f1(x743),f1(f5(f5(f5(x743)))))+~P2(a2,f1(f5(f5(f5(x742)))))+~P2(a2,f1(f5(f5(f5(x743)))))+~P2(a2,f1(f5(f5(f5(x741)))))+~P2(a2,f1(f5(f5(f5(f5(x742))))))+~P2(a2,f1(f5(f5(f5(f5(x743)))))) % 57.98/58.04 [75]~P3(f5(x752),f5(x751))+~P3(f5(x753),f5(x752))+~P2(f1(x751),f1(f5(x751)))+~P2(f1(x752),f1(f5(x752)))+~P2(a2,f1(x751))+~P2(f1(x753),f1(f5(x753)))+~P2(a2,f1(x752))+~P2(a2,f1(x753))+~P2(a2,f1(f5(x751)))+~P2(a2,f1(f5(x752)))+~P2(a2,f1(f5(x753)))+~P2(f1(x751),f1(f5(f5(x751))))+~P2(f1(x752),f1(f5(f5(x752))))+~P2(f1(x753),f1(f5(f5(x753))))+~P2(a2,f1(f5(f5(x753))))+~P2(a2,f1(f5(f5(x752))))+~P2(a2,f1(f5(f5(x751))))+~P2(f1(x751),f1(f5(f5(f5(x751)))))+~P2(f1(x752),f1(f5(f5(f5(x752)))))+~P2(f1(x753),f1(f5(f5(f5(x753)))))+~P2(a2,f1(f5(f5(f5(x751)))))+~P2(a2,f1(f5(f5(f5(x752)))))+~P2(a2,f1(f5(f5(f5(x753)))))+~P2(a2,f1(f5(f5(f5(f5(x751))))))+~P2(a2,f1(f5(f5(f5(f5(x752))))))+~P2(a2,f1(f5(f5(f5(f5(x753)))))) % 57.98/58.04 cnf(82,plain, % 57.98/58.04 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(a4)))+~P2(a2,f1(f5(a4)))), % 57.98/58.04 inference(scs_inference,[],[2,1,5,3])). % 57.98/58.04 cnf(83,plain, % 57.98/58.04 (P2(f1(a4),f1(f5(a4)))+P3(f5(a4),f5(a4))), % 57.98/58.04 inference(scs_inference,[],[1,2,82,4])). % 57.98/58.04 cnf(89,plain, % 57.98/58.04 (P2(a2,f1(a4))), % 57.98/58.04 inference(scs_inference,[],[1,2,3])). % 57.98/58.04 cnf(90,plain, % 57.98/58.04 (P1(f1(x901),f3(a2))), % 57.98/58.04 inference(rename_variables,[],[1])). % 57.98/58.04 cnf(92,plain, % 57.98/58.04 (P2(a2,f1(f5(a4)))), % 57.98/58.04 inference(scs_inference,[],[1,90,2,3,4])). % 57.98/58.04 cnf(93,plain, % 57.98/58.04 (P1(f1(x931),f3(a2))), % 57.98/58.04 inference(rename_variables,[],[1])). % 57.98/58.04 cnf(95,plain, % 57.98/58.04 (P2(a2,f1(f5(f5(a4))))), % 57.98/58.04 inference(scs_inference,[],[1,90,93,2,3,4,6])). % 57.98/58.04 cnf(96,plain, % 57.98/58.04 (P1(f1(x961),f3(a2))), % 57.98/58.04 inference(rename_variables,[],[1])). % 57.98/58.04 cnf(98,plain, % 57.98/58.04 (P2(a2,f1(f5(f5(f5(a4)))))), % 57.98/58.04 inference(scs_inference,[],[1,90,93,96,2,3,4,6,7])). % 57.98/58.04 cnf(99,plain, % 57.98/58.04 (P1(f1(x991),f3(a2))), % 57.98/58.04 inference(rename_variables,[],[1])). % 57.98/58.04 cnf(101,plain, % 57.98/58.04 (P2(a2,f1(f5(f5(f5(f5(a4))))))), % 57.98/58.04 inference(scs_inference,[],[1,90,93,96,99,2,3,4,6,7,10])). % 57.98/58.04 cnf(107,plain, % 57.98/58.04 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(a4))))+~P2(f1(a4),f1(f5(f5(f5(a4)))))), % 57.98/58.04 inference(scs_inference,[],[98,101,95,89,92,22])). % 57.98/58.04 cnf(115,plain, % 57.98/58.04 (~P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(a4)))), % 57.98/58.04 inference(scs_inference,[],[89,92,9])). % 57.98/58.04 cnf(118,plain, % 57.98/58.04 (~P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(f5(a4))))+P2(f1(a4),f1(f5(f5(f5(a4)))))), % 57.98/58.04 inference(scs_inference,[],[95,92,89,98,115,56])). % 57.98/58.04 cnf(134,plain, % 57.98/58.04 (~P2(f1(a4),f1(f5(f5(a4))))+P2(f1(a4),f1(f5(f5(f5(a4)))))+P2(f1(a4),f1(f5(a4)))), % 57.98/58.04 inference(scs_inference,[],[89,92,118,5])). % 57.98/58.04 cnf(150,plain, % 57.98/58.04 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(f5(a4))))+P2(f1(a4),f1(f5(f5(f5(a4)))))), % 57.98/58.04 inference(scs_inference,[],[92,89,95,98,134,14])). % 57.98/58.04 cnf(204,plain, % 57.98/58.04 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+P2(f1(a4),f1(f5(f5(a4))))), % 57.98/58.04 inference(scs_inference,[],[89,95,92,101,8])). % 57.98/58.04 cnf(252,plain, % 57.98/58.04 (~P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+P2(f1(a4),f1(f5(f5(a4))))), % 57.98/58.04 inference(scs_inference,[],[89,101,92,95,21])). % 57.98/58.04 cnf(298,plain, % 57.98/58.04 (~P2(f1(a4),f1(f5(a4)))+P2(f1(a4),f1(f5(f5(a4))))), % 57.98/58.04 inference(scs_inference,[],[204,252])). % 57.98/58.04 cnf(314,plain, % 57.98/58.04 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(a4))))), % 57.98/58.04 inference(scs_inference,[],[298,83])). % 57.98/58.04 cnf(330,plain, % 57.98/58.04 (P2(f1(a4),f1(f5(a4)))+P2(f1(a4),f1(f5(f5(a4))))), % 57.98/58.04 inference(scs_inference,[],[314,115])). % 57.98/58.04 cnf(346,plain, % 57.98/58.04 (P2(f1(a4),f1(f5(f5(a4))))), % 57.98/58.04 inference(scs_inference,[],[330,298])). % 57.98/58.04 cnf(347,plain, % 57.98/58.04 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))+~P2(f1(a4),f1(f5(f5(f5(a4)))))), % 57.98/58.04 inference(scs_inference,[],[346,107])). % 57.98/58.04 cnf(349,plain, % 57.98/58.04 (~P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(f5(a4)))))), % 57.98/58.04 inference(scs_inference,[],[346,118])). % 57.98/58.04 cnf(351,plain, % 57.98/58.04 (P3(f5(a4),f5(a4))+P2(f1(a4),f1(f5(f5(f5(a4)))))), % 57.98/58.04 inference(scs_inference,[],[346,150])). % 57.98/58.04 cnf(362,plain, % 57.98/58.04 (P2(f1(a4),f1(f5(f5(f5(a4)))))), % 57.98/58.04 inference(scs_inference,[],[349,351])). % 57.98/58.04 cnf(364,plain, % 57.98/58.04 (P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))), % 57.98/58.04 inference(scs_inference,[],[362,347])). % 57.98/58.04 cnf(366,plain, % 57.98/58.04 (~P3(f5(a4),f5(a4))+~P2(f1(a4),f1(f5(a4)))), % 57.98/58.04 inference(scs_inference,[],[362,346,89,101,95,92,98,75])). % 57.98/58.04 cnf(411,plain, % 57.98/58.04 (~P3(f5(a4),f5(a4))), % 57.98/58.04 inference(scs_inference,[],[366,115])). % 57.98/58.04 cnf(412,plain, % 57.98/58.04 (P2(f1(a4),f1(f5(a4)))), % 57.98/58.04 inference(scs_inference,[],[411,83])). % 57.98/58.04 cnf(413,plain, % 57.98/58.04 (~P2(f1(a4),f1(f5(a4)))), % 57.98/58.04 inference(scs_inference,[],[411,364])). % 57.98/58.04 cnf(415,plain, % 57.98/58.04 ($false), % 57.98/58.04 inference(scs_inference,[],[413,412]), % 57.98/58.04 ['proof']). % 57.98/58.04 % SZS output end Proof % 57.98/58.04 % Total time : 57.160000 s %------------------------------------------------------------------------------