// This proof script verifies that every natural number // of length n, for n >= 6 and even, is the sum of exactly // 6 generalized antipalindromes of length n-2. NestedWordAutomaton antipalCheckerSIX = ( callAlphabet = { a b }, internalAlphabet = { c d }, returnAlphabet = { e f }, states = { f_0_ZERO f_0_ONE f_0_TWO f_0_THREE f_0_FOUR f_0_FIVE f_0_SIX f_1_ZERO f_1_ONE f_1_TWO f_1_THREE f_1_FOUR f_1_FIVE f_1_SIX f_2_ZERO f_2_ONE f_2_TWO f_2_THREE f_2_FOUR f_2_FIVE f_2_SIX f_3_ZERO f_3_ONE f_3_TWO f_3_THREE f_3_FOUR f_3_FIVE f_3_SIX f_4_ZERO f_4_ONE f_4_TWO f_4_THREE f_4_FOUR f_4_FIVE f_4_SIX f_5_ZERO f_5_ONE f_5_TWO f_5_THREE f_5_FOUR f_5_FIVE f_5_SIX s0 s1 s2 s3 s4 s5 q acc}, initialStates = {f_0_ZERO f_0_ONE f_0_TWO f_0_THREE f_0_FOUR f_0_FIVE f_0_SIX }, finalStates = {acc}, callTransitions = { (f_0_ZERO a f_0_ZERO) (f_0_ZERO a f_0_ONE) (f_0_ZERO a f_0_TWO) (f_0_ZERO a f_0_THREE) (f_0_ZERO a f_0_FOUR) (f_0_ZERO a f_0_FIVE) (f_0_ZERO a f_0_SIX) (f_0_ONE b f_0_ZERO) (f_0_ONE b f_0_ONE) (f_0_ONE b f_0_TWO) (f_0_ONE b f_0_THREE) (f_0_ONE b f_0_FOUR) (f_0_ONE b f_0_FIVE) (f_0_ONE b f_0_SIX) (f_0_TWO a f_1_ZERO) (f_0_TWO a f_1_ONE) (f_0_TWO a f_1_TWO) (f_0_TWO a f_1_THREE) (f_0_TWO a f_1_FOUR) (f_0_TWO a f_1_FIVE) (f_0_TWO a f_1_SIX) (f_0_THREE b f_1_ZERO) (f_0_THREE b f_1_ONE) (f_0_THREE b f_1_TWO) (f_0_THREE b f_1_THREE) (f_0_THREE b f_1_FOUR) (f_0_THREE b f_1_FIVE) (f_0_THREE b f_1_SIX) (f_0_FOUR a f_2_ZERO) (f_0_FOUR a f_2_ONE) (f_0_FOUR a f_2_TWO) (f_0_FOUR a f_2_THREE) (f_0_FOUR a f_2_FOUR) (f_0_FOUR a f_2_FIVE) (f_0_FOUR a f_2_SIX) (f_0_FIVE b f_2_ZERO) (f_0_FIVE b f_2_ONE) (f_0_FIVE b f_2_TWO) (f_0_FIVE b f_2_THREE) (f_0_FIVE b f_2_FOUR) (f_0_FIVE b f_2_FIVE) (f_0_FIVE b f_2_SIX) (f_0_SIX a f_3_ZERO) (f_0_SIX a f_3_ONE) (f_0_SIX a f_3_TWO) (f_0_SIX a f_3_THREE) (f_0_SIX a f_3_FOUR) (f_0_SIX a f_3_FIVE) (f_0_SIX a f_3_SIX) (f_1_ZERO b f_0_ZERO) (f_1_ZERO b f_0_ONE) (f_1_ZERO b f_0_TWO) (f_1_ZERO b f_0_THREE) (f_1_ZERO b f_0_FOUR) (f_1_ZERO b f_0_FIVE) (f_1_ZERO b f_0_SIX) (f_1_ONE a f_1_ZERO) (f_1_ONE a f_1_ONE) (f_1_ONE a f_1_TWO) (f_1_ONE a f_1_THREE) (f_1_ONE a f_1_FOUR) (f_1_ONE a f_1_FIVE) (f_1_ONE a f_1_SIX) (f_1_TWO b f_1_ZERO) (f_1_TWO b f_1_ONE) (f_1_TWO b f_1_TWO) (f_1_TWO b f_1_THREE) (f_1_TWO b f_1_FOUR) (f_1_TWO b f_1_FIVE) (f_1_TWO b f_1_SIX) (f_1_THREE a f_2_ZERO) (f_1_THREE a f_2_ONE) (f_1_THREE a f_2_TWO) (f_1_THREE a f_2_THREE) (f_1_THREE a f_2_FOUR) (f_1_THREE a f_2_FIVE) (f_1_THREE a f_2_SIX) (f_1_FOUR b f_2_ZERO) (f_1_FOUR b f_2_ONE) (f_1_FOUR b f_2_TWO) (f_1_FOUR b f_2_THREE) (f_1_FOUR b f_2_FOUR) (f_1_FOUR b f_2_FIVE) (f_1_FOUR b f_2_SIX) (f_1_FIVE a f_3_ZERO) (f_1_FIVE a f_3_ONE) (f_1_FIVE a f_3_TWO) (f_1_FIVE a f_3_THREE) (f_1_FIVE a f_3_FOUR) (f_1_FIVE a f_3_FIVE) (f_1_FIVE a f_3_SIX) (f_1_SIX b f_3_ZERO) (f_1_SIX b f_3_ONE) (f_1_SIX b f_3_TWO) (f_1_SIX b f_3_THREE) (f_1_SIX b f_3_FOUR) (f_1_SIX b f_3_FIVE) (f_1_SIX b f_3_SIX) (f_2_ZERO a f_1_ZERO) (f_2_ZERO a f_1_ONE) (f_2_ZERO a f_1_TWO) (f_2_ZERO a f_1_THREE) (f_2_ZERO a f_1_FOUR) (f_2_ZERO a f_1_FIVE) (f_2_ZERO a f_1_SIX) (f_2_ONE b f_1_ZERO) (f_2_ONE b f_1_ONE) (f_2_ONE b f_1_TWO) (f_2_ONE b f_1_THREE) (f_2_ONE b f_1_FOUR) (f_2_ONE b f_1_FIVE) (f_2_ONE b f_1_SIX) (f_2_TWO a f_2_ZERO) (f_2_TWO a f_2_ONE) (f_2_TWO a f_2_TWO) (f_2_TWO a f_2_THREE) (f_2_TWO a f_2_FOUR) (f_2_TWO a f_2_FIVE) (f_2_TWO a f_2_SIX) (f_2_THREE b f_2_ZERO) (f_2_THREE b f_2_ONE) (f_2_THREE b f_2_TWO) (f_2_THREE b f_2_THREE) (f_2_THREE b f_2_FOUR) (f_2_THREE b f_2_FIVE) (f_2_THREE b f_2_SIX) (f_2_FOUR a f_3_ZERO) (f_2_FOUR a f_3_ONE) (f_2_FOUR a f_3_TWO) (f_2_FOUR a f_3_THREE) (f_2_FOUR a f_3_FOUR) (f_2_FOUR a f_3_FIVE) (f_2_FOUR a f_3_SIX) (f_2_FIVE b f_3_ZERO) (f_2_FIVE b f_3_ONE) (f_2_FIVE b f_3_TWO) (f_2_FIVE b f_3_THREE) (f_2_FIVE b f_3_FOUR) (f_2_FIVE b f_3_FIVE) (f_2_FIVE b f_3_SIX) (f_2_SIX a f_4_ZERO) (f_2_SIX a f_4_ONE) (f_2_SIX a f_4_TWO) (f_2_SIX a f_4_THREE) (f_2_SIX a f_4_FOUR) (f_2_SIX a f_4_FIVE) (f_2_SIX a f_4_SIX) (f_3_ZERO b f_1_ZERO) (f_3_ZERO b f_1_ONE) (f_3_ZERO b f_1_TWO) (f_3_ZERO b f_1_THREE) (f_3_ZERO b f_1_FOUR) (f_3_ZERO b f_1_FIVE) (f_3_ZERO b f_1_SIX) (f_3_ONE a f_2_ZERO) (f_3_ONE a f_2_ONE) (f_3_ONE a f_2_TWO) (f_3_ONE a f_2_THREE) (f_3_ONE a f_2_FOUR) (f_3_ONE a f_2_FIVE) (f_3_ONE a f_2_SIX) (f_3_TWO b f_2_ZERO) (f_3_TWO b f_2_ONE) (f_3_TWO b f_2_TWO) (f_3_TWO b f_2_THREE) (f_3_TWO b f_2_FOUR) (f_3_TWO b f_2_FIVE) (f_3_TWO b f_2_SIX) (f_3_THREE a f_3_ZERO) (f_3_THREE a f_3_ONE) (f_3_THREE a f_3_TWO) (f_3_THREE a f_3_THREE) (f_3_THREE a f_3_FOUR) (f_3_THREE a f_3_FIVE) (f_3_THREE a f_3_SIX) (f_3_FOUR b f_3_ZERO) (f_3_FOUR b f_3_ONE) (f_3_FOUR b f_3_TWO) (f_3_FOUR b f_3_THREE) (f_3_FOUR b f_3_FOUR) (f_3_FOUR b f_3_FIVE) (f_3_FOUR b f_3_SIX) (f_3_FIVE a f_4_ZERO) (f_3_FIVE a f_4_ONE) (f_3_FIVE a f_4_TWO) (f_3_FIVE a f_4_THREE) (f_3_FIVE a f_4_FOUR) (f_3_FIVE a f_4_FIVE) (f_3_FIVE a f_4_SIX) (f_3_SIX b f_4_ZERO) (f_3_SIX b f_4_ONE) (f_3_SIX b f_4_TWO) (f_3_SIX b f_4_THREE) (f_3_SIX b f_4_FOUR) (f_3_SIX b f_4_FIVE) (f_3_SIX b f_4_SIX) (f_4_ZERO a f_2_ZERO) (f_4_ZERO a f_2_ONE) (f_4_ZERO a f_2_TWO) (f_4_ZERO a f_2_THREE) (f_4_ZERO a f_2_FOUR) (f_4_ZERO a f_2_FIVE) (f_4_ZERO a f_2_SIX) (f_4_ONE b f_2_ZERO) (f_4_ONE b f_2_ONE) (f_4_ONE b f_2_TWO) (f_4_ONE b f_2_THREE) (f_4_ONE b f_2_FOUR) (f_4_ONE b f_2_FIVE) (f_4_ONE b f_2_SIX) (f_4_TWO a f_3_ZERO) (f_4_TWO a f_3_ONE) (f_4_TWO a f_3_TWO) (f_4_TWO a f_3_THREE) (f_4_TWO a f_3_FOUR) (f_4_TWO a f_3_FIVE) (f_4_TWO a f_3_SIX) (f_4_THREE b f_3_ZERO) (f_4_THREE b f_3_ONE) (f_4_THREE b f_3_TWO) (f_4_THREE b f_3_THREE) (f_4_THREE b f_3_FOUR) (f_4_THREE b f_3_FIVE) (f_4_THREE b f_3_SIX) (f_4_FOUR a f_4_ZERO) (f_4_FOUR a f_4_ONE) (f_4_FOUR a f_4_TWO) (f_4_FOUR a f_4_THREE) (f_4_FOUR a f_4_FOUR) (f_4_FOUR a f_4_FIVE) (f_4_FOUR a f_4_SIX) (f_4_FIVE b f_4_ZERO) (f_4_FIVE b f_4_ONE) (f_4_FIVE b f_4_TWO) (f_4_FIVE b f_4_THREE) (f_4_FIVE b f_4_FOUR) (f_4_FIVE b f_4_FIVE) (f_4_FIVE b f_4_SIX) (f_4_SIX a f_5_ZERO) (f_4_SIX a f_5_ONE) (f_4_SIX a f_5_TWO) (f_4_SIX a f_5_THREE) (f_4_SIX a f_5_FOUR) (f_4_SIX a f_5_FIVE) (f_4_SIX a f_5_SIX) (f_5_ZERO b f_2_ZERO) (f_5_ZERO b f_2_ONE) (f_5_ZERO b f_2_TWO) (f_5_ZERO b f_2_THREE) (f_5_ZERO b f_2_FOUR) (f_5_ZERO b f_2_FIVE) (f_5_ZERO b f_2_SIX) (f_5_ONE a f_3_ZERO) (f_5_ONE a f_3_ONE) (f_5_ONE a f_3_TWO) (f_5_ONE a f_3_THREE) (f_5_ONE a f_3_FOUR) (f_5_ONE a f_3_FIVE) (f_5_ONE a f_3_SIX) (f_5_TWO b f_3_ZERO) (f_5_TWO b f_3_ONE) (f_5_TWO b f_3_TWO) (f_5_TWO b f_3_THREE) (f_5_TWO b f_3_FOUR) (f_5_TWO b f_3_FIVE) (f_5_TWO b f_3_SIX) (f_5_THREE a f_4_ZERO) (f_5_THREE a f_4_ONE) (f_5_THREE a f_4_TWO) (f_5_THREE a f_4_THREE) (f_5_THREE a f_4_FOUR) (f_5_THREE a f_4_FIVE) (f_5_THREE a f_4_SIX) (f_5_FOUR b f_4_ZERO) (f_5_FOUR b f_4_ONE) (f_5_FOUR b f_4_TWO) (f_5_FOUR b f_4_THREE) (f_5_FOUR b f_4_FOUR) (f_5_FOUR b f_4_FIVE) (f_5_FOUR b f_4_SIX) (f_5_FIVE a f_5_ZERO) (f_5_FIVE a f_5_ONE) (f_5_FIVE a f_5_TWO) (f_5_FIVE a f_5_THREE) (f_5_FIVE a f_5_FOUR) (f_5_FIVE a f_5_FIVE) (f_5_FIVE a f_5_SIX) (f_5_SIX b f_5_ZERO) (f_5_SIX b f_5_ONE) (f_5_SIX b f_5_TWO) (f_5_SIX b f_5_THREE) (f_5_SIX b f_5_FOUR) (f_5_SIX b f_5_FIVE) (f_5_SIX b f_5_SIX) }, internalTransitions = { (f_0_ZERO c s0) (f_0_ONE c s0) (f_0_TWO c s0) (f_0_THREE c s0) (f_0_FOUR c s0) (f_0_FIVE c s0) (f_0_SIX c s0) (f_0_ZERO d s0) (f_0_ONE d s0) (f_0_TWO d s0) (f_0_THREE d s0) (f_0_FOUR d s0) (f_0_FIVE d s0) (f_0_SIX d s0) (f_0_ZERO c s1) (f_0_ONE c s1) (f_0_TWO c s1) (f_0_THREE c s1) (f_0_FOUR c s1) (f_0_FIVE c s1) (f_0_SIX c s1) (f_0_ZERO d s1) (f_0_ONE d s1) (f_0_TWO d s1) (f_0_THREE d s1) (f_0_FOUR d s1) (f_0_FIVE d s1) (f_0_SIX d s1) (f_0_ZERO c s2) (f_0_ONE c s2) (f_0_TWO c s2) (f_0_THREE c s2) (f_0_FOUR c s2) (f_0_FIVE c s2) (f_0_SIX c s2) (f_0_ZERO d s2) (f_0_ONE d s2) (f_0_TWO d s2) (f_0_THREE d s2) (f_0_FOUR d s2) (f_0_FIVE d s2) (f_0_SIX d s2) (f_0_ZERO c s3) (f_0_ONE c s3) (f_0_TWO c s3) (f_0_THREE c s3) (f_0_FOUR c s3) (f_0_FIVE c s3) (f_0_SIX c s3) (f_1_ZERO d s0) (f_1_ONE d s0) (f_1_TWO d s0) (f_1_THREE d s0) (f_1_FOUR d s0) (f_1_FIVE d s0) (f_1_SIX d s0) (f_1_ZERO c s1) (f_1_ONE c s1) (f_1_TWO c s1) (f_1_THREE c s1) (f_1_FOUR c s1) (f_1_FIVE c s1) (f_1_SIX c s1) (f_1_ZERO d s1) (f_1_ONE d s1) (f_1_TWO d s1) (f_1_THREE d s1) (f_1_FOUR d s1) (f_1_FIVE d s1) (f_1_SIX d s1) (f_1_ZERO c s2) (f_1_ONE c s2) (f_1_TWO c s2) (f_1_THREE c s2) (f_1_FOUR c s2) (f_1_FIVE c s2) (f_1_SIX c s2) (f_1_ZERO d s2) (f_1_ONE d s2) (f_1_TWO d s2) (f_1_THREE d s2) (f_1_FOUR d s2) (f_1_FIVE d s2) (f_1_SIX d s2) (f_1_ZERO c s3) (f_1_ONE c s3) (f_1_TWO c s3) (f_1_THREE c s3) (f_1_FOUR c s3) (f_1_FIVE c s3) (f_1_SIX c s3) (f_1_ZERO d s3) (f_1_ONE d s3) (f_1_TWO d s3) (f_1_THREE d s3) (f_1_FOUR d s3) (f_1_FIVE d s3) (f_1_SIX d s3) (f_2_ZERO c s1) (f_2_ONE c s1) (f_2_TWO c s1) (f_2_THREE c s1) (f_2_FOUR c s1) (f_2_FIVE c s1) (f_2_SIX c s1) (f_2_ZERO d s1) (f_2_ONE d s1) (f_2_TWO d s1) (f_2_THREE d s1) (f_2_FOUR d s1) (f_2_FIVE d s1) (f_2_SIX d s1) (f_2_ZERO c s2) (f_2_ONE c s2) (f_2_TWO c s2) (f_2_THREE c s2) (f_2_FOUR c s2) (f_2_FIVE c s2) (f_2_SIX c s2) (f_2_ZERO d s2) (f_2_ONE d s2) (f_2_TWO d s2) (f_2_THREE d s2) (f_2_FOUR d s2) (f_2_FIVE d s2) (f_2_SIX d s2) (f_2_ZERO c s3) (f_2_ONE c s3) (f_2_TWO c s3) (f_2_THREE c s3) (f_2_FOUR c s3) (f_2_FIVE c s3) (f_2_SIX c s3) (f_2_ZERO d s3) (f_2_ONE d s3) (f_2_TWO d s3) (f_2_THREE d s3) (f_2_FOUR d s3) (f_2_FIVE d s3) (f_2_SIX d s3) (f_2_ZERO c s4) (f_2_ONE c s4) (f_2_TWO c s4) (f_2_THREE c s4) (f_2_FOUR c s4) (f_2_FIVE c s4) (f_2_SIX c s4) (f_3_ZERO d s1) (f_3_ONE d s1) (f_3_TWO d s1) (f_3_THREE d s1) (f_3_FOUR d s1) (f_3_FIVE d s1) (f_3_SIX d s1) (f_3_ZERO c s2) (f_3_ONE c s2) (f_3_TWO c s2) (f_3_THREE c s2) (f_3_FOUR c s2) (f_3_FIVE c s2) (f_3_SIX c s2) (f_3_ZERO d s2) (f_3_ONE d s2) (f_3_TWO d s2) (f_3_THREE d s2) (f_3_FOUR d s2) (f_3_FIVE d s2) (f_3_SIX d s2) (f_3_ZERO c s3) (f_3_ONE c s3) (f_3_TWO c s3) (f_3_THREE c s3) (f_3_FOUR c s3) (f_3_FIVE c s3) (f_3_SIX c s3) (f_3_ZERO d s3) (f_3_ONE d s3) (f_3_TWO d s3) (f_3_THREE d s3) (f_3_FOUR d s3) (f_3_FIVE d s3) (f_3_SIX d s3) (f_3_ZERO c s4) (f_3_ONE c s4) (f_3_TWO c s4) (f_3_THREE c s4) (f_3_FOUR c s4) (f_3_FIVE c s4) (f_3_SIX c s4) (f_3_ZERO d s4) (f_3_ONE d s4) (f_3_TWO d s4) (f_3_THREE d s4) (f_3_FOUR d s4) (f_3_FIVE d s4) (f_3_SIX d s4) (f_4_ZERO c s2) (f_4_ONE c s2) (f_4_TWO c s2) (f_4_THREE c s2) (f_4_FOUR c s2) (f_4_FIVE c s2) (f_4_SIX c s2) (f_4_ZERO d s2) (f_4_ONE d s2) (f_4_TWO d s2) (f_4_THREE d s2) (f_4_FOUR d s2) (f_4_FIVE d s2) (f_4_SIX d s2) (f_4_ZERO c s3) (f_4_ONE c s3) (f_4_TWO c s3) (f_4_THREE c s3) (f_4_FOUR c s3) (f_4_FIVE c s3) (f_4_SIX c s3) (f_4_ZERO d s3) (f_4_ONE d s3) (f_4_TWO d s3) (f_4_THREE d s3) (f_4_FOUR d s3) (f_4_FIVE d s3) (f_4_SIX d s3) (f_4_ZERO c s4) (f_4_ONE c s4) (f_4_TWO c s4) (f_4_THREE c s4) (f_4_FOUR c s4) (f_4_FIVE c s4) (f_4_SIX c s4) (f_4_ZERO d s4) (f_4_ONE d s4) (f_4_TWO d s4) (f_4_THREE d s4) (f_4_FOUR d s4) (f_4_FIVE d s4) (f_4_SIX d s4) (f_4_ZERO c s5) (f_4_ONE c s5) (f_4_TWO c s5) (f_4_THREE c s5) (f_4_FOUR c s5) (f_4_FIVE c s5) (f_4_SIX c s5) (f_5_ZERO d s2) (f_5_ONE d s2) (f_5_TWO d s2) (f_5_THREE d s2) (f_5_FOUR d s2) (f_5_FIVE d s2) (f_5_SIX d s2) (f_5_ZERO c s3) (f_5_ONE c s3) (f_5_TWO c s3) (f_5_THREE c s3) (f_5_FOUR c s3) (f_5_FIVE c s3) (f_5_SIX c s3) (f_5_ZERO d s3) (f_5_ONE d s3) (f_5_TWO d s3) (f_5_THREE d s3) (f_5_FOUR d s3) (f_5_FIVE d s3) (f_5_SIX d s3) (f_5_ZERO c s4) (f_5_ONE c s4) (f_5_TWO c s4) (f_5_THREE c s4) (f_5_FOUR c s4) (f_5_FIVE c s4) (f_5_SIX c s4) (f_5_ZERO d s4) (f_5_ONE d s4) (f_5_TWO d s4) (f_5_THREE d s4) (f_5_FOUR d s4) (f_5_FIVE d s4) (f_5_SIX d s4) (f_5_ZERO c s5) (f_5_ONE c s5) (f_5_TWO c s5) (f_5_THREE c s5) (f_5_FOUR c s5) (f_5_FIVE c s5) (f_5_SIX c s5) (f_5_ZERO d s5) (f_5_ONE d s5) (f_5_TWO d s5) (f_5_THREE d s5) (f_5_FOUR d s5) (f_5_FIVE d s5) (f_5_SIX d s5) (s2 c q) (s3 d q) (q d acc) }, returnTransitions = { (f_0_ZERO f_0_ZERO e s3) (f_0_ZERO f_1_ZERO e s3) (f_0_ZERO f_2_ZERO e s3) (f_0_ZERO f_3_ZERO e s3) (f_0_ZERO f_4_ZERO e s3) (f_0_ZERO f_5_ZERO e s3) (f_0_ZERO f_0_TWO e s2) (f_0_ZERO f_1_TWO e s2) (f_0_ZERO f_2_TWO e s2) (f_0_ZERO f_3_TWO e s2) (f_0_ZERO f_4_TWO e s2) (f_0_ZERO f_5_TWO e s2) (f_0_ZERO f_0_FOUR e s1) (f_0_ZERO f_1_FOUR e s1) (f_0_ZERO f_2_FOUR e s1) (f_0_ZERO f_3_FOUR e s1) (f_0_ZERO f_4_FOUR e s1) (f_0_ZERO f_5_FOUR e s1) (f_0_ZERO f_0_SIX e s0) (f_0_ZERO f_1_SIX e s0) (f_0_ZERO f_2_SIX e s0) (f_0_ZERO f_3_SIX e s0) (f_0_ZERO f_4_SIX e s0) (f_0_ZERO f_5_SIX e s0) (f_0_ONE f_0_ZERO e s3) (f_0_ONE f_1_ZERO e s3) (f_0_ONE f_2_ZERO e s3) (f_0_ONE f_3_ZERO e s3) (f_0_ONE f_4_ZERO e s3) (f_0_ONE f_5_ZERO e s3) (f_0_ONE f_0_TWO e s2) (f_0_ONE f_1_TWO e s2) (f_0_ONE f_2_TWO e s2) (f_0_ONE f_3_TWO e s2) (f_0_ONE f_4_TWO e s2) (f_0_ONE f_5_TWO e s2) (f_0_ONE f_0_FOUR e s1) (f_0_ONE f_1_FOUR e s1) (f_0_ONE f_2_FOUR e s1) (f_0_ONE f_3_FOUR e s1) (f_0_ONE f_4_FOUR e s1) (f_0_ONE f_5_FOUR e s1) (f_0_ONE f_0_SIX e s0) (f_0_ONE f_1_SIX e s0) (f_0_ONE f_2_SIX e s0) (f_0_ONE f_3_SIX e s0) (f_0_ONE f_4_SIX e s0) (f_0_ONE f_5_SIX e s0) (f_0_TWO f_0_ZERO e s3) (f_0_TWO f_1_ZERO e s3) (f_0_TWO f_2_ZERO e s3) (f_0_TWO f_3_ZERO e s3) (f_0_TWO f_4_ZERO e s3) (f_0_TWO f_5_ZERO e s3) (f_0_TWO f_0_TWO e s2) (f_0_TWO f_1_TWO e s2) (f_0_TWO f_2_TWO e s2) (f_0_TWO f_3_TWO e s2) (f_0_TWO f_4_TWO e s2) (f_0_TWO f_5_TWO e s2) (f_0_TWO f_0_FOUR e s1) (f_0_TWO f_1_FOUR e s1) (f_0_TWO f_2_FOUR e s1) (f_0_TWO f_3_FOUR e s1) (f_0_TWO f_4_FOUR e s1) (f_0_TWO f_5_FOUR e s1) (f_0_TWO f_0_SIX e s0) (f_0_TWO f_1_SIX e s0) (f_0_TWO f_2_SIX e s0) (f_0_TWO f_3_SIX e s0) (f_0_TWO f_4_SIX e s0) (f_0_TWO f_5_SIX e s0) (f_0_THREE f_0_ZERO e s3) (f_0_THREE f_1_ZERO e s3) (f_0_THREE f_2_ZERO e s3) (f_0_THREE f_3_ZERO e s3) (f_0_THREE f_4_ZERO e s3) (f_0_THREE f_5_ZERO e s3) (f_0_THREE f_0_TWO e s2) (f_0_THREE f_1_TWO e s2) (f_0_THREE f_2_TWO e s2) (f_0_THREE f_3_TWO e s2) (f_0_THREE f_4_TWO e s2) (f_0_THREE f_5_TWO e s2) (f_0_THREE f_0_FOUR e s1) (f_0_THREE f_1_FOUR e s1) (f_0_THREE f_2_FOUR e s1) (f_0_THREE f_3_FOUR e s1) (f_0_THREE f_4_FOUR e s1) (f_0_THREE f_5_FOUR e s1) (f_0_THREE f_0_SIX e s0) (f_0_THREE f_1_SIX e s0) (f_0_THREE f_2_SIX e s0) (f_0_THREE f_3_SIX e s0) (f_0_THREE f_4_SIX e s0) (f_0_THREE f_5_SIX e s0) (f_0_FOUR f_0_ZERO e s3) (f_0_FOUR f_1_ZERO e s3) (f_0_FOUR f_2_ZERO e s3) (f_0_FOUR f_3_ZERO e s3) (f_0_FOUR f_4_ZERO e s3) (f_0_FOUR f_5_ZERO e s3) (f_0_FOUR f_0_TWO e s2) (f_0_FOUR f_1_TWO e s2) (f_0_FOUR f_2_TWO e s2) (f_0_FOUR f_3_TWO e s2) (f_0_FOUR f_4_TWO e s2) (f_0_FOUR f_5_TWO e s2) (f_0_FOUR f_0_FOUR e s1) (f_0_FOUR f_1_FOUR e s1) (f_0_FOUR f_2_FOUR e s1) (f_0_FOUR f_3_FOUR e s1) (f_0_FOUR f_4_FOUR e s1) (f_0_FOUR f_5_FOUR e s1) (f_0_FOUR f_0_SIX e s0) (f_0_FOUR f_1_SIX e s0) (f_0_FOUR f_2_SIX e s0) (f_0_FOUR f_3_SIX e s0) (f_0_FOUR f_4_SIX e s0) (f_0_FOUR f_5_SIX e s0) (f_0_FIVE f_0_ZERO e s3) (f_0_FIVE f_1_ZERO e s3) (f_0_FIVE f_2_ZERO e s3) (f_0_FIVE f_3_ZERO e s3) (f_0_FIVE f_4_ZERO e s3) (f_0_FIVE f_5_ZERO e s3) (f_0_FIVE f_0_TWO e s2) (f_0_FIVE f_1_TWO e s2) (f_0_FIVE f_2_TWO e s2) (f_0_FIVE f_3_TWO e s2) (f_0_FIVE f_4_TWO e s2) (f_0_FIVE f_5_TWO e s2) (f_0_FIVE f_0_FOUR e s1) (f_0_FIVE f_1_FOUR e s1) (f_0_FIVE f_2_FOUR e s1) (f_0_FIVE f_3_FOUR e s1) (f_0_FIVE f_4_FOUR e s1) (f_0_FIVE f_5_FOUR e s1) (f_0_FIVE f_0_SIX e s0) (f_0_FIVE f_1_SIX e s0) (f_0_FIVE f_2_SIX e s0) (f_0_FIVE f_3_SIX e s0) (f_0_FIVE f_4_SIX e s0) (f_0_FIVE f_5_SIX e s0) (f_0_SIX f_0_ZERO e s3) (f_0_SIX f_1_ZERO e s3) (f_0_SIX f_2_ZERO e s3) (f_0_SIX f_3_ZERO e s3) (f_0_SIX f_4_ZERO e s3) (f_0_SIX f_5_ZERO e s3) (f_0_SIX f_0_TWO e s2) (f_0_SIX f_1_TWO e s2) (f_0_SIX f_2_TWO e s2) (f_0_SIX f_3_TWO e s2) (f_0_SIX f_4_TWO e s2) (f_0_SIX f_5_TWO e s2) (f_0_SIX f_0_FOUR e s1) (f_0_SIX f_1_FOUR e s1) (f_0_SIX f_2_FOUR e s1) (f_0_SIX f_3_FOUR e s1) (f_0_SIX f_4_FOUR e s1) (f_0_SIX f_5_FOUR e s1) (f_0_SIX f_0_SIX e s0) (f_0_SIX f_1_SIX e s0) (f_0_SIX f_2_SIX e s0) (f_0_SIX f_3_SIX e s0) (f_0_SIX f_4_SIX e s0) (f_0_SIX f_5_SIX e s0) (f_0_ZERO f_0_ONE f s2) (f_0_ZERO f_1_ONE f s2) (f_0_ZERO f_2_ONE f s2) (f_0_ZERO f_3_ONE f s2) (f_0_ZERO f_4_ONE f s2) (f_0_ZERO f_5_ONE f s2) (f_0_ZERO f_0_THREE f s1) (f_0_ZERO f_1_THREE f s1) (f_0_ZERO f_2_THREE f s1) (f_0_ZERO f_3_THREE f s1) (f_0_ZERO f_4_THREE f s1) (f_0_ZERO f_5_THREE f s1) (f_0_ZERO f_0_FIVE f s0) (f_0_ZERO f_1_FIVE f s0) (f_0_ZERO f_2_FIVE f s0) (f_0_ZERO f_3_FIVE f s0) (f_0_ZERO f_4_FIVE f s0) (f_0_ZERO f_5_FIVE f s0) (f_0_ONE f_0_ONE f s2) (f_0_ONE f_1_ONE f s2) (f_0_ONE f_2_ONE f s2) (f_0_ONE f_3_ONE f s2) (f_0_ONE f_4_ONE f s2) (f_0_ONE f_5_ONE f s2) (f_0_ONE f_0_THREE f s1) (f_0_ONE f_1_THREE f s1) (f_0_ONE f_2_THREE f s1) (f_0_ONE f_3_THREE f s1) (f_0_ONE f_4_THREE f s1) (f_0_ONE f_5_THREE f s1) (f_0_ONE f_0_FIVE f s0) (f_0_ONE f_1_FIVE f s0) (f_0_ONE f_2_FIVE f s0) (f_0_ONE f_3_FIVE f s0) (f_0_ONE f_4_FIVE f s0) (f_0_ONE f_5_FIVE f s0) (f_0_TWO f_0_ONE f s2) (f_0_TWO f_1_ONE f s2) (f_0_TWO f_2_ONE f s2) (f_0_TWO f_3_ONE f s2) (f_0_TWO f_4_ONE f s2) (f_0_TWO f_5_ONE f s2) (f_0_TWO f_0_THREE f s1) (f_0_TWO f_1_THREE f s1) (f_0_TWO f_2_THREE f s1) (f_0_TWO f_3_THREE f s1) (f_0_TWO f_4_THREE f s1) (f_0_TWO f_5_THREE f s1) (f_0_TWO f_0_FIVE f s0) (f_0_TWO f_1_FIVE f s0) (f_0_TWO f_2_FIVE f s0) (f_0_TWO f_3_FIVE f s0) (f_0_TWO f_4_FIVE f s0) (f_0_TWO f_5_FIVE f s0) (f_0_THREE f_0_ONE f s2) (f_0_THREE f_1_ONE f s2) (f_0_THREE f_2_ONE f s2) (f_0_THREE f_3_ONE f s2) (f_0_THREE f_4_ONE f s2) (f_0_THREE f_5_ONE f s2) (f_0_THREE f_0_THREE f s1) (f_0_THREE f_1_THREE f s1) (f_0_THREE f_2_THREE f s1) (f_0_THREE f_3_THREE f s1) (f_0_THREE f_4_THREE f s1) (f_0_THREE f_5_THREE f s1) (f_0_THREE f_0_FIVE f s0) (f_0_THREE f_1_FIVE f s0) (f_0_THREE f_2_FIVE f s0) (f_0_THREE f_3_FIVE f s0) (f_0_THREE f_4_FIVE f s0) (f_0_THREE f_5_FIVE f s0) (f_0_FOUR f_0_ONE f s2) (f_0_FOUR f_1_ONE f s2) (f_0_FOUR f_2_ONE f s2) (f_0_FOUR f_3_ONE f s2) (f_0_FOUR f_4_ONE f s2) (f_0_FOUR f_5_ONE f s2) (f_0_FOUR f_0_THREE f s1) (f_0_FOUR f_1_THREE f s1) (f_0_FOUR f_2_THREE f s1) (f_0_FOUR f_3_THREE f s1) (f_0_FOUR f_4_THREE f s1) (f_0_FOUR f_5_THREE f s1) (f_0_FOUR f_0_FIVE f s0) (f_0_FOUR f_1_FIVE f s0) (f_0_FOUR f_2_FIVE f s0) (f_0_FOUR f_3_FIVE f s0) (f_0_FOUR f_4_FIVE f s0) (f_0_FOUR f_5_FIVE f s0) (f_0_FIVE f_0_ONE f s2) (f_0_FIVE f_1_ONE f s2) (f_0_FIVE f_2_ONE f s2) (f_0_FIVE f_3_ONE f s2) (f_0_FIVE f_4_ONE f s2) (f_0_FIVE f_5_ONE f s2) (f_0_FIVE f_0_THREE f s1) (f_0_FIVE f_1_THREE f s1) (f_0_FIVE f_2_THREE f s1) (f_0_FIVE f_3_THREE f s1) (f_0_FIVE f_4_THREE f s1) (f_0_FIVE f_5_THREE f s1) (f_0_FIVE f_0_FIVE f s0) (f_0_FIVE f_1_FIVE f s0) (f_0_FIVE f_2_FIVE f s0) (f_0_FIVE f_3_FIVE f s0) (f_0_FIVE f_4_FIVE f s0) (f_0_FIVE f_5_FIVE f s0) (f_0_SIX f_0_ONE f s2) (f_0_SIX f_1_ONE f s2) (f_0_SIX f_2_ONE f s2) (f_0_SIX f_3_ONE f s2) (f_0_SIX f_4_ONE f s2) (f_0_SIX f_5_ONE f s2) (f_0_SIX f_0_THREE f s1) (f_0_SIX f_1_THREE f s1) (f_0_SIX f_2_THREE f s1) (f_0_SIX f_3_THREE f s1) (f_0_SIX f_4_THREE f s1) (f_0_SIX f_5_THREE f s1) (f_0_SIX f_0_FIVE f s0) (f_0_SIX f_1_FIVE f s0) (f_0_SIX f_2_FIVE f s0) (f_0_SIX f_3_FIVE f s0) (f_0_SIX f_4_FIVE f s0) (f_0_SIX f_5_FIVE f s0) (s0 f_0_ZERO e s3) (s0 f_1_ZERO e s3) (s0 f_2_ZERO e s3) (s0 f_3_ZERO e s3) (s0 f_4_ZERO e s3) (s0 f_5_ZERO e s3) (s0 f_0_TWO e s2) (s0 f_1_TWO e s2) (s0 f_2_TWO e s2) (s0 f_3_TWO e s2) (s0 f_4_TWO e s2) (s0 f_5_TWO e s2) (s0 f_0_FOUR e s1) (s0 f_1_FOUR e s1) (s0 f_2_FOUR e s1) (s0 f_3_FOUR e s1) (s0 f_4_FOUR e s1) (s0 f_5_FOUR e s1) (s0 f_0_SIX e s0) (s0 f_1_SIX e s0) (s0 f_2_SIX e s0) (s0 f_3_SIX e s0) (s0 f_4_SIX e s0) (s0 f_5_SIX e s0) (s0 f_0_ONE f s2) (s0 f_1_ONE f s2) (s0 f_2_ONE f s2) (s0 f_3_ONE f s2) (s0 f_4_ONE f s2) (s0 f_5_ONE f s2) (s0 f_0_THREE f s1) (s0 f_1_THREE f s1) (s0 f_2_THREE f s1) (s0 f_3_THREE f s1) (s0 f_4_THREE f s1) (s0 f_5_THREE f s1) (s0 f_0_FIVE f s0) (s0 f_1_FIVE f s0) (s0 f_2_FIVE f s0) (s0 f_3_FIVE f s0) (s0 f_4_FIVE f s0) (s0 f_5_FIVE f s0) (f_1_ZERO f_0_ZERO f s3) (f_1_ZERO f_1_ZERO f s3) (f_1_ZERO f_2_ZERO f s3) (f_1_ZERO f_3_ZERO f s3) (f_1_ZERO f_4_ZERO f s3) (f_1_ZERO f_5_ZERO f s3) (f_1_ZERO f_0_TWO f s2) (f_1_ZERO f_1_TWO f s2) (f_1_ZERO f_2_TWO f s2) (f_1_ZERO f_3_TWO f s2) (f_1_ZERO f_4_TWO f s2) (f_1_ZERO f_5_TWO f s2) (f_1_ZERO f_0_FOUR f s1) (f_1_ZERO f_1_FOUR f s1) (f_1_ZERO f_2_FOUR f s1) (f_1_ZERO f_3_FOUR f s1) (f_1_ZERO f_4_FOUR f s1) (f_1_ZERO f_5_FOUR f s1) (f_1_ZERO f_0_SIX f s0) (f_1_ZERO f_1_SIX f s0) (f_1_ZERO f_2_SIX f s0) (f_1_ZERO f_3_SIX f s0) (f_1_ZERO f_4_SIX f s0) (f_1_ZERO f_5_SIX f s0) (f_1_ONE f_0_ZERO f s3) (f_1_ONE f_1_ZERO f s3) (f_1_ONE f_2_ZERO f s3) (f_1_ONE f_3_ZERO f s3) (f_1_ONE f_4_ZERO f s3) (f_1_ONE f_5_ZERO f s3) (f_1_ONE f_0_TWO f s2) (f_1_ONE f_1_TWO f s2) (f_1_ONE f_2_TWO f s2) (f_1_ONE f_3_TWO f s2) (f_1_ONE f_4_TWO f s2) (f_1_ONE f_5_TWO f s2) (f_1_ONE f_0_FOUR f s1) (f_1_ONE f_1_FOUR f s1) (f_1_ONE f_2_FOUR f s1) (f_1_ONE f_3_FOUR f s1) (f_1_ONE f_4_FOUR f s1) (f_1_ONE f_5_FOUR f s1) (f_1_ONE f_0_SIX f s0) (f_1_ONE f_1_SIX f s0) (f_1_ONE f_2_SIX f s0) (f_1_ONE f_3_SIX f s0) (f_1_ONE f_4_SIX f s0) (f_1_ONE f_5_SIX f s0) (f_1_TWO f_0_ZERO f s3) (f_1_TWO f_1_ZERO f s3) (f_1_TWO f_2_ZERO f s3) (f_1_TWO f_3_ZERO f s3) (f_1_TWO f_4_ZERO f s3) (f_1_TWO f_5_ZERO f s3) (f_1_TWO f_0_TWO f s2) (f_1_TWO f_1_TWO f s2) (f_1_TWO f_2_TWO f s2) (f_1_TWO f_3_TWO f s2) (f_1_TWO f_4_TWO f s2) (f_1_TWO f_5_TWO f s2) (f_1_TWO f_0_FOUR f s1) (f_1_TWO f_1_FOUR f s1) (f_1_TWO f_2_FOUR f s1) (f_1_TWO f_3_FOUR f s1) (f_1_TWO f_4_FOUR f s1) (f_1_TWO f_5_FOUR f s1) (f_1_TWO f_0_SIX f s0) (f_1_TWO f_1_SIX f s0) (f_1_TWO f_2_SIX f s0) (f_1_TWO f_3_SIX f s0) (f_1_TWO f_4_SIX f s0) (f_1_TWO f_5_SIX f s0) (f_1_THREE f_0_ZERO f s3) (f_1_THREE f_1_ZERO f s3) (f_1_THREE f_2_ZERO f s3) (f_1_THREE f_3_ZERO f s3) (f_1_THREE f_4_ZERO f s3) (f_1_THREE f_5_ZERO f s3) (f_1_THREE f_0_TWO f s2) (f_1_THREE f_1_TWO f s2) (f_1_THREE f_2_TWO f s2) (f_1_THREE f_3_TWO f s2) (f_1_THREE f_4_TWO f s2) (f_1_THREE f_5_TWO f s2) (f_1_THREE f_0_FOUR f s1) (f_1_THREE f_1_FOUR f s1) (f_1_THREE f_2_FOUR f s1) (f_1_THREE f_3_FOUR f s1) (f_1_THREE f_4_FOUR f s1) (f_1_THREE f_5_FOUR f s1) (f_1_THREE f_0_SIX f s0) (f_1_THREE f_1_SIX f s0) (f_1_THREE f_2_SIX f s0) (f_1_THREE f_3_SIX f s0) (f_1_THREE f_4_SIX f s0) (f_1_THREE f_5_SIX f s0) (f_1_FOUR f_0_ZERO f s3) (f_1_FOUR f_1_ZERO f s3) (f_1_FOUR f_2_ZERO f s3) (f_1_FOUR f_3_ZERO f s3) (f_1_FOUR f_4_ZERO f s3) (f_1_FOUR f_5_ZERO f s3) (f_1_FOUR f_0_TWO f s2) (f_1_FOUR f_1_TWO f s2) (f_1_FOUR f_2_TWO f s2) (f_1_FOUR f_3_TWO f s2) (f_1_FOUR f_4_TWO f s2) (f_1_FOUR f_5_TWO f s2) (f_1_FOUR f_0_FOUR f s1) (f_1_FOUR f_1_FOUR f s1) (f_1_FOUR f_2_FOUR f s1) (f_1_FOUR f_3_FOUR f s1) (f_1_FOUR f_4_FOUR f s1) (f_1_FOUR f_5_FOUR f s1) (f_1_FOUR f_0_SIX f s0) (f_1_FOUR f_1_SIX f s0) (f_1_FOUR f_2_SIX f s0) (f_1_FOUR f_3_SIX f s0) (f_1_FOUR f_4_SIX f s0) (f_1_FOUR f_5_SIX f s0) (f_1_FIVE f_0_ZERO f s3) (f_1_FIVE f_1_ZERO f s3) (f_1_FIVE f_2_ZERO f s3) (f_1_FIVE f_3_ZERO f s3) (f_1_FIVE f_4_ZERO f s3) (f_1_FIVE f_5_ZERO f s3) (f_1_FIVE f_0_TWO f s2) (f_1_FIVE f_1_TWO f s2) (f_1_FIVE f_2_TWO f s2) (f_1_FIVE f_3_TWO f s2) (f_1_FIVE f_4_TWO f s2) (f_1_FIVE f_5_TWO f s2) (f_1_FIVE f_0_FOUR f s1) (f_1_FIVE f_1_FOUR f s1) (f_1_FIVE f_2_FOUR f s1) (f_1_FIVE f_3_FOUR f s1) (f_1_FIVE f_4_FOUR f s1) (f_1_FIVE f_5_FOUR f s1) (f_1_FIVE f_0_SIX f s0) (f_1_FIVE f_1_SIX f s0) (f_1_FIVE f_2_SIX f s0) (f_1_FIVE f_3_SIX f s0) (f_1_FIVE f_4_SIX f s0) (f_1_FIVE f_5_SIX f s0) (f_1_SIX f_0_ZERO f s3) (f_1_SIX f_1_ZERO f s3) (f_1_SIX f_2_ZERO f s3) (f_1_SIX f_3_ZERO f s3) (f_1_SIX f_4_ZERO f s3) (f_1_SIX f_5_ZERO f s3) (f_1_SIX f_0_TWO f s2) (f_1_SIX f_1_TWO f s2) (f_1_SIX f_2_TWO f s2) (f_1_SIX f_3_TWO f s2) (f_1_SIX f_4_TWO f s2) (f_1_SIX f_5_TWO f s2) (f_1_SIX f_0_FOUR f s1) (f_1_SIX f_1_FOUR f s1) (f_1_SIX f_2_FOUR f s1) (f_1_SIX f_3_FOUR f s1) (f_1_SIX f_4_FOUR f s1) (f_1_SIX f_5_FOUR f s1) (f_1_SIX f_0_SIX f s0) (f_1_SIX f_1_SIX f s0) (f_1_SIX f_2_SIX f s0) (f_1_SIX f_3_SIX f s0) (f_1_SIX f_4_SIX f s0) (f_1_SIX f_5_SIX f s0) (f_1_ZERO f_0_ONE e s3) (f_1_ZERO f_1_ONE e s3) (f_1_ZERO f_2_ONE e s3) (f_1_ZERO f_3_ONE e s3) (f_1_ZERO f_4_ONE e s3) (f_1_ZERO f_5_ONE e s3) (f_1_ZERO f_0_THREE e s2) (f_1_ZERO f_1_THREE e s2) (f_1_ZERO f_2_THREE e s2) (f_1_ZERO f_3_THREE e s2) (f_1_ZERO f_4_THREE e s2) (f_1_ZERO f_5_THREE e s2) (f_1_ZERO f_0_FIVE e s1) (f_1_ZERO f_1_FIVE e s1) (f_1_ZERO f_2_FIVE e s1) (f_1_ZERO f_3_FIVE e s1) (f_1_ZERO f_4_FIVE e s1) (f_1_ZERO f_5_FIVE e s1) (f_1_ONE f_0_ONE e s3) (f_1_ONE f_1_ONE e s3) (f_1_ONE f_2_ONE e s3) (f_1_ONE f_3_ONE e s3) (f_1_ONE f_4_ONE e s3) (f_1_ONE f_5_ONE e s3) (f_1_ONE f_0_THREE e s2) (f_1_ONE f_1_THREE e s2) (f_1_ONE f_2_THREE e s2) (f_1_ONE f_3_THREE e s2) (f_1_ONE f_4_THREE e s2) (f_1_ONE f_5_THREE e s2) (f_1_ONE f_0_FIVE e s1) (f_1_ONE f_1_FIVE e s1) (f_1_ONE f_2_FIVE e s1) (f_1_ONE f_3_FIVE e s1) (f_1_ONE f_4_FIVE e s1) (f_1_ONE f_5_FIVE e s1) (f_1_TWO f_0_ONE e s3) (f_1_TWO f_1_ONE e s3) (f_1_TWO f_2_ONE e s3) (f_1_TWO f_3_ONE e s3) (f_1_TWO f_4_ONE e s3) (f_1_TWO f_5_ONE e s3) (f_1_TWO f_0_THREE e s2) (f_1_TWO f_1_THREE e s2) (f_1_TWO f_2_THREE e s2) (f_1_TWO f_3_THREE e s2) (f_1_TWO f_4_THREE e s2) (f_1_TWO f_5_THREE e s2) (f_1_TWO f_0_FIVE e s1) (f_1_TWO f_1_FIVE e s1) (f_1_TWO f_2_FIVE e s1) (f_1_TWO f_3_FIVE e s1) (f_1_TWO f_4_FIVE e s1) (f_1_TWO f_5_FIVE e s1) (f_1_THREE f_0_ONE e s3) (f_1_THREE f_1_ONE e s3) (f_1_THREE f_2_ONE e s3) (f_1_THREE f_3_ONE e s3) (f_1_THREE f_4_ONE e s3) (f_1_THREE f_5_ONE e s3) (f_1_THREE f_0_THREE e s2) (f_1_THREE f_1_THREE e s2) (f_1_THREE f_2_THREE e s2) (f_1_THREE f_3_THREE e s2) (f_1_THREE f_4_THREE e s2) (f_1_THREE f_5_THREE e s2) (f_1_THREE f_0_FIVE e s1) (f_1_THREE f_1_FIVE e s1) (f_1_THREE f_2_FIVE e s1) (f_1_THREE f_3_FIVE e s1) (f_1_THREE f_4_FIVE e s1) (f_1_THREE f_5_FIVE e s1) (f_1_FOUR f_0_ONE e s3) (f_1_FOUR f_1_ONE e s3) (f_1_FOUR f_2_ONE e s3) (f_1_FOUR f_3_ONE e s3) (f_1_FOUR f_4_ONE e s3) (f_1_FOUR f_5_ONE e s3) (f_1_FOUR f_0_THREE e s2) (f_1_FOUR f_1_THREE e s2) (f_1_FOUR f_2_THREE e s2) (f_1_FOUR f_3_THREE e s2) (f_1_FOUR f_4_THREE e s2) (f_1_FOUR f_5_THREE e s2) (f_1_FOUR f_0_FIVE e s1) (f_1_FOUR f_1_FIVE e s1) (f_1_FOUR f_2_FIVE e s1) (f_1_FOUR f_3_FIVE e s1) (f_1_FOUR f_4_FIVE e s1) (f_1_FOUR f_5_FIVE e s1) (f_1_FIVE f_0_ONE e s3) (f_1_FIVE f_1_ONE e s3) (f_1_FIVE f_2_ONE e s3) (f_1_FIVE f_3_ONE e s3) (f_1_FIVE f_4_ONE e s3) (f_1_FIVE f_5_ONE e s3) (f_1_FIVE f_0_THREE e s2) (f_1_FIVE f_1_THREE e s2) (f_1_FIVE f_2_THREE e s2) (f_1_FIVE f_3_THREE e s2) (f_1_FIVE f_4_THREE e s2) (f_1_FIVE f_5_THREE e s2) (f_1_FIVE f_0_FIVE e s1) (f_1_FIVE f_1_FIVE e s1) (f_1_FIVE f_2_FIVE e s1) (f_1_FIVE f_3_FIVE e s1) (f_1_FIVE f_4_FIVE e s1) (f_1_FIVE f_5_FIVE e s1) (f_1_SIX f_0_ONE e s3) (f_1_SIX f_1_ONE e s3) (f_1_SIX f_2_ONE e s3) (f_1_SIX f_3_ONE e s3) (f_1_SIX f_4_ONE e s3) (f_1_SIX f_5_ONE e s3) (f_1_SIX f_0_THREE e s2) (f_1_SIX f_1_THREE e s2) (f_1_SIX f_2_THREE e s2) (f_1_SIX f_3_THREE e s2) (f_1_SIX f_4_THREE e s2) (f_1_SIX f_5_THREE e s2) (f_1_SIX f_0_FIVE e s1) (f_1_SIX f_1_FIVE e s1) (f_1_SIX f_2_FIVE e s1) (f_1_SIX f_3_FIVE e s1) (f_1_SIX f_4_FIVE e s1) (f_1_SIX f_5_FIVE e s1) (s1 f_0_ZERO f s3) (s1 f_1_ZERO f s3) (s1 f_2_ZERO f s3) (s1 f_3_ZERO f s3) (s1 f_4_ZERO f s3) (s1 f_5_ZERO f s3) (s1 f_0_TWO f s2) (s1 f_1_TWO f s2) (s1 f_2_TWO f s2) (s1 f_3_TWO f s2) (s1 f_4_TWO f s2) (s1 f_5_TWO f s2) (s1 f_0_FOUR f s1) (s1 f_1_FOUR f s1) (s1 f_2_FOUR f s1) (s1 f_3_FOUR f s1) (s1 f_4_FOUR f s1) (s1 f_5_FOUR f s1) (s1 f_0_SIX f s0) (s1 f_1_SIX f s0) (s1 f_2_SIX f s0) (s1 f_3_SIX f s0) (s1 f_4_SIX f s0) (s1 f_5_SIX f s0) (s1 f_0_ONE e s3) (s1 f_1_ONE e s3) (s1 f_2_ONE e s3) (s1 f_3_ONE e s3) (s1 f_4_ONE e s3) (s1 f_5_ONE e s3) (s1 f_0_THREE e s2) (s1 f_1_THREE e s2) (s1 f_2_THREE e s2) (s1 f_3_THREE e s2) (s1 f_4_THREE e s2) (s1 f_5_THREE e s2) (s1 f_0_FIVE e s1) (s1 f_1_FIVE e s1) (s1 f_2_FIVE e s1) (s1 f_3_FIVE e s1) (s1 f_4_FIVE e s1) (s1 f_5_FIVE e s1) (f_2_ZERO f_0_ZERO e s4) (f_2_ZERO f_1_ZERO e s4) (f_2_ZERO f_2_ZERO e s4) (f_2_ZERO f_3_ZERO e s4) (f_2_ZERO f_4_ZERO e s4) (f_2_ZERO f_5_ZERO e s4) (f_2_ZERO f_0_TWO e s3) (f_2_ZERO f_1_TWO e s3) (f_2_ZERO f_2_TWO e s3) (f_2_ZERO f_3_TWO e s3) (f_2_ZERO f_4_TWO e s3) (f_2_ZERO f_5_TWO e s3) (f_2_ZERO f_0_FOUR e s2) (f_2_ZERO f_1_FOUR e s2) (f_2_ZERO f_2_FOUR e s2) (f_2_ZERO f_3_FOUR e s2) (f_2_ZERO f_4_FOUR e s2) (f_2_ZERO f_5_FOUR e s2) (f_2_ZERO f_0_SIX e s1) (f_2_ZERO f_1_SIX e s1) (f_2_ZERO f_2_SIX e s1) (f_2_ZERO f_3_SIX e s1) (f_2_ZERO f_4_SIX e s1) (f_2_ZERO f_5_SIX e s1) (f_2_ONE f_0_ZERO e s4) (f_2_ONE f_1_ZERO e s4) (f_2_ONE f_2_ZERO e s4) (f_2_ONE f_3_ZERO e s4) (f_2_ONE f_4_ZERO e s4) (f_2_ONE f_5_ZERO e s4) (f_2_ONE f_0_TWO e s3) (f_2_ONE f_1_TWO e s3) (f_2_ONE f_2_TWO e s3) (f_2_ONE f_3_TWO e s3) (f_2_ONE f_4_TWO e s3) (f_2_ONE f_5_TWO e s3) (f_2_ONE f_0_FOUR e s2) (f_2_ONE f_1_FOUR e s2) (f_2_ONE f_2_FOUR e s2) (f_2_ONE f_3_FOUR e s2) (f_2_ONE f_4_FOUR e s2) (f_2_ONE f_5_FOUR e s2) (f_2_ONE f_0_SIX e s1) (f_2_ONE f_1_SIX e s1) (f_2_ONE f_2_SIX e s1) (f_2_ONE f_3_SIX e s1) (f_2_ONE f_4_SIX e s1) (f_2_ONE f_5_SIX e s1) (f_2_TWO f_0_ZERO e s4) (f_2_TWO f_1_ZERO e s4) (f_2_TWO f_2_ZERO e s4) (f_2_TWO f_3_ZERO e s4) (f_2_TWO f_4_ZERO e s4) (f_2_TWO f_5_ZERO e s4) (f_2_TWO f_0_TWO e s3) (f_2_TWO f_1_TWO e s3) (f_2_TWO f_2_TWO e s3) (f_2_TWO f_3_TWO e s3) (f_2_TWO f_4_TWO e s3) (f_2_TWO f_5_TWO e s3) (f_2_TWO f_0_FOUR e s2) (f_2_TWO f_1_FOUR e s2) (f_2_TWO f_2_FOUR e s2) (f_2_TWO f_3_FOUR e s2) (f_2_TWO f_4_FOUR e s2) (f_2_TWO f_5_FOUR e s2) (f_2_TWO f_0_SIX e s1) (f_2_TWO f_1_SIX e s1) (f_2_TWO f_2_SIX e s1) (f_2_TWO f_3_SIX e s1) (f_2_TWO f_4_SIX e s1) (f_2_TWO f_5_SIX e s1) (f_2_THREE f_0_ZERO e s4) (f_2_THREE f_1_ZERO e s4) (f_2_THREE f_2_ZERO e s4) (f_2_THREE f_3_ZERO e s4) (f_2_THREE f_4_ZERO e s4) (f_2_THREE f_5_ZERO e s4) (f_2_THREE f_0_TWO e s3) (f_2_THREE f_1_TWO e s3) (f_2_THREE f_2_TWO e s3) (f_2_THREE f_3_TWO e s3) (f_2_THREE f_4_TWO e s3) (f_2_THREE f_5_TWO e s3) (f_2_THREE f_0_FOUR e s2) (f_2_THREE f_1_FOUR e s2) (f_2_THREE f_2_FOUR e s2) (f_2_THREE f_3_FOUR e s2) (f_2_THREE f_4_FOUR e s2) (f_2_THREE f_5_FOUR e s2) (f_2_THREE f_0_SIX e s1) (f_2_THREE f_1_SIX e s1) (f_2_THREE f_2_SIX e s1) (f_2_THREE f_3_SIX e s1) (f_2_THREE f_4_SIX e s1) (f_2_THREE f_5_SIX e s1) (f_2_FOUR f_0_ZERO e s4) (f_2_FOUR f_1_ZERO e s4) (f_2_FOUR f_2_ZERO e s4) (f_2_FOUR f_3_ZERO e s4) (f_2_FOUR f_4_ZERO e s4) (f_2_FOUR f_5_ZERO e s4) (f_2_FOUR f_0_TWO e s3) (f_2_FOUR f_1_TWO e s3) (f_2_FOUR f_2_TWO e s3) (f_2_FOUR f_3_TWO e s3) (f_2_FOUR f_4_TWO e s3) (f_2_FOUR f_5_TWO e s3) (f_2_FOUR f_0_FOUR e s2) (f_2_FOUR f_1_FOUR e s2) (f_2_FOUR f_2_FOUR e s2) (f_2_FOUR f_3_FOUR e s2) (f_2_FOUR f_4_FOUR e s2) (f_2_FOUR f_5_FOUR e s2) (f_2_FOUR f_0_SIX e s1) (f_2_FOUR f_1_SIX e s1) (f_2_FOUR f_2_SIX e s1) (f_2_FOUR f_3_SIX e s1) (f_2_FOUR f_4_SIX e s1) (f_2_FOUR f_5_SIX e s1) (f_2_FIVE f_0_ZERO e s4) (f_2_FIVE f_1_ZERO e s4) (f_2_FIVE f_2_ZERO e s4) (f_2_FIVE f_3_ZERO e s4) (f_2_FIVE f_4_ZERO e s4) (f_2_FIVE f_5_ZERO e s4) (f_2_FIVE f_0_TWO e s3) (f_2_FIVE f_1_TWO e s3) (f_2_FIVE f_2_TWO e s3) (f_2_FIVE f_3_TWO e s3) (f_2_FIVE f_4_TWO e s3) (f_2_FIVE f_5_TWO e s3) (f_2_FIVE f_0_FOUR e s2) (f_2_FIVE f_1_FOUR e s2) (f_2_FIVE f_2_FOUR e s2) (f_2_FIVE f_3_FOUR e s2) (f_2_FIVE f_4_FOUR e s2) (f_2_FIVE f_5_FOUR e s2) (f_2_FIVE f_0_SIX e s1) (f_2_FIVE f_1_SIX e s1) (f_2_FIVE f_2_SIX e s1) (f_2_FIVE f_3_SIX e s1) (f_2_FIVE f_4_SIX e s1) (f_2_FIVE f_5_SIX e s1) (f_2_SIX f_0_ZERO e s4) (f_2_SIX f_1_ZERO e s4) (f_2_SIX f_2_ZERO e s4) (f_2_SIX f_3_ZERO e s4) (f_2_SIX f_4_ZERO e s4) (f_2_SIX f_5_ZERO e s4) (f_2_SIX f_0_TWO e s3) (f_2_SIX f_1_TWO e s3) (f_2_SIX f_2_TWO e s3) (f_2_SIX f_3_TWO e s3) (f_2_SIX f_4_TWO e s3) (f_2_SIX f_5_TWO e s3) (f_2_SIX f_0_FOUR e s2) (f_2_SIX f_1_FOUR e s2) (f_2_SIX f_2_FOUR e s2) (f_2_SIX f_3_FOUR e s2) (f_2_SIX f_4_FOUR e s2) (f_2_SIX f_5_FOUR e s2) (f_2_SIX f_0_SIX e s1) (f_2_SIX f_1_SIX e s1) (f_2_SIX f_2_SIX e s1) (f_2_SIX f_3_SIX e s1) (f_2_SIX f_4_SIX e s1) (f_2_SIX f_5_SIX e s1) (f_2_ZERO f_0_ONE f s3) (f_2_ZERO f_1_ONE f s3) (f_2_ZERO f_2_ONE f s3) (f_2_ZERO f_3_ONE f s3) (f_2_ZERO f_4_ONE f s3) (f_2_ZERO f_5_ONE f s3) (f_2_ZERO f_0_THREE f s2) (f_2_ZERO f_1_THREE f s2) (f_2_ZERO f_2_THREE f s2) (f_2_ZERO f_3_THREE f s2) (f_2_ZERO f_4_THREE f s2) (f_2_ZERO f_5_THREE f s2) (f_2_ZERO f_0_FIVE f s1) (f_2_ZERO f_1_FIVE f s1) (f_2_ZERO f_2_FIVE f s1) (f_2_ZERO f_3_FIVE f s1) (f_2_ZERO f_4_FIVE f s1) (f_2_ZERO f_5_FIVE f s1) (f_2_ONE f_0_ONE f s3) (f_2_ONE f_1_ONE f s3) (f_2_ONE f_2_ONE f s3) (f_2_ONE f_3_ONE f s3) (f_2_ONE f_4_ONE f s3) (f_2_ONE f_5_ONE f s3) (f_2_ONE f_0_THREE f s2) (f_2_ONE f_1_THREE f s2) (f_2_ONE f_2_THREE f s2) (f_2_ONE f_3_THREE f s2) (f_2_ONE f_4_THREE f s2) (f_2_ONE f_5_THREE f s2) (f_2_ONE f_0_FIVE f s1) (f_2_ONE f_1_FIVE f s1) (f_2_ONE f_2_FIVE f s1) (f_2_ONE f_3_FIVE f s1) (f_2_ONE f_4_FIVE f s1) (f_2_ONE f_5_FIVE f s1) (f_2_TWO f_0_ONE f s3) (f_2_TWO f_1_ONE f s3) (f_2_TWO f_2_ONE f s3) (f_2_TWO f_3_ONE f s3) (f_2_TWO f_4_ONE f s3) (f_2_TWO f_5_ONE f s3) (f_2_TWO f_0_THREE f s2) (f_2_TWO f_1_THREE f s2) (f_2_TWO f_2_THREE f s2) (f_2_TWO f_3_THREE f s2) (f_2_TWO f_4_THREE f s2) (f_2_TWO f_5_THREE f s2) (f_2_TWO f_0_FIVE f s1) (f_2_TWO f_1_FIVE f s1) (f_2_TWO f_2_FIVE f s1) (f_2_TWO f_3_FIVE f s1) (f_2_TWO f_4_FIVE f s1) (f_2_TWO f_5_FIVE f s1) (f_2_THREE f_0_ONE f s3) (f_2_THREE f_1_ONE f s3) (f_2_THREE f_2_ONE f s3) (f_2_THREE f_3_ONE f s3) (f_2_THREE f_4_ONE f s3) (f_2_THREE f_5_ONE f s3) (f_2_THREE f_0_THREE f s2) (f_2_THREE f_1_THREE f s2) (f_2_THREE f_2_THREE f s2) (f_2_THREE f_3_THREE f s2) (f_2_THREE f_4_THREE f s2) (f_2_THREE f_5_THREE f s2) (f_2_THREE f_0_FIVE f s1) (f_2_THREE f_1_FIVE f s1) (f_2_THREE f_2_FIVE f s1) (f_2_THREE f_3_FIVE f s1) (f_2_THREE f_4_FIVE f s1) (f_2_THREE f_5_FIVE f s1) (f_2_FOUR f_0_ONE f s3) (f_2_FOUR f_1_ONE f s3) (f_2_FOUR f_2_ONE f s3) (f_2_FOUR f_3_ONE f s3) (f_2_FOUR f_4_ONE f s3) (f_2_FOUR f_5_ONE f s3) (f_2_FOUR f_0_THREE f s2) (f_2_FOUR f_1_THREE f s2) (f_2_FOUR f_2_THREE f s2) (f_2_FOUR f_3_THREE f s2) (f_2_FOUR f_4_THREE f s2) (f_2_FOUR f_5_THREE f s2) (f_2_FOUR f_0_FIVE f s1) (f_2_FOUR f_1_FIVE f s1) (f_2_FOUR f_2_FIVE f s1) (f_2_FOUR f_3_FIVE f s1) (f_2_FOUR f_4_FIVE f s1) (f_2_FOUR f_5_FIVE f s1) (f_2_FIVE f_0_ONE f s3) (f_2_FIVE f_1_ONE f s3) (f_2_FIVE f_2_ONE f s3) (f_2_FIVE f_3_ONE f s3) (f_2_FIVE f_4_ONE f s3) (f_2_FIVE f_5_ONE f s3) (f_2_FIVE f_0_THREE f s2) (f_2_FIVE f_1_THREE f s2) (f_2_FIVE f_2_THREE f s2) (f_2_FIVE f_3_THREE f s2) (f_2_FIVE f_4_THREE f s2) (f_2_FIVE f_5_THREE f s2) (f_2_FIVE f_0_FIVE f s1) (f_2_FIVE f_1_FIVE f s1) (f_2_FIVE f_2_FIVE f s1) (f_2_FIVE f_3_FIVE f s1) (f_2_FIVE f_4_FIVE f s1) (f_2_FIVE f_5_FIVE f s1) (f_2_SIX f_0_ONE f s3) (f_2_SIX f_1_ONE f s3) (f_2_SIX f_2_ONE f s3) (f_2_SIX f_3_ONE f s3) (f_2_SIX f_4_ONE f s3) (f_2_SIX f_5_ONE f s3) (f_2_SIX f_0_THREE f s2) (f_2_SIX f_1_THREE f s2) (f_2_SIX f_2_THREE f s2) (f_2_SIX f_3_THREE f s2) (f_2_SIX f_4_THREE f s2) (f_2_SIX f_5_THREE f s2) (f_2_SIX f_0_FIVE f s1) (f_2_SIX f_1_FIVE f s1) (f_2_SIX f_2_FIVE f s1) (f_2_SIX f_3_FIVE f s1) (f_2_SIX f_4_FIVE f s1) (f_2_SIX f_5_FIVE f s1) (s2 f_0_ZERO e s4) (s2 f_1_ZERO e s4) (s2 f_2_ZERO e s4) (s2 f_3_ZERO e s4) (s2 f_4_ZERO e s4) (s2 f_5_ZERO e s4) (s2 f_0_TWO e s3) (s2 f_1_TWO e s3) (s2 f_2_TWO e s3) (s2 f_3_TWO e s3) (s2 f_4_TWO e s3) (s2 f_5_TWO e s3) (s2 f_0_FOUR e s2) (s2 f_1_FOUR e s2) (s2 f_2_FOUR e s2) (s2 f_3_FOUR e s2) (s2 f_4_FOUR e s2) (s2 f_5_FOUR e s2) (s2 f_0_SIX e s1) (s2 f_1_SIX e s1) (s2 f_2_SIX e s1) (s2 f_3_SIX e s1) (s2 f_4_SIX e s1) (s2 f_5_SIX e s1) (s2 f_0_ONE f s3) (s2 f_1_ONE f s3) (s2 f_2_ONE f s3) (s2 f_3_ONE f s3) (s2 f_4_ONE f s3) (s2 f_5_ONE f s3) (s2 f_0_THREE f s2) (s2 f_1_THREE f s2) (s2 f_2_THREE f s2) (s2 f_3_THREE f s2) (s2 f_4_THREE f s2) (s2 f_5_THREE f s2) (s2 f_0_FIVE f s1) (s2 f_1_FIVE f s1) (s2 f_2_FIVE f s1) (s2 f_3_FIVE f s1) (s2 f_4_FIVE f s1) (s2 f_5_FIVE f s1) (f_3_ZERO f_0_ZERO f s4) (f_3_ZERO f_1_ZERO f s4) (f_3_ZERO f_2_ZERO f s4) (f_3_ZERO f_3_ZERO f s4) (f_3_ZERO f_4_ZERO f s4) (f_3_ZERO f_5_ZERO f s4) (f_3_ZERO f_0_TWO f s3) (f_3_ZERO f_1_TWO f s3) (f_3_ZERO f_2_TWO f s3) (f_3_ZERO f_3_TWO f s3) (f_3_ZERO f_4_TWO f s3) (f_3_ZERO f_5_TWO f s3) (f_3_ZERO f_0_FOUR f s2) (f_3_ZERO f_1_FOUR f s2) (f_3_ZERO f_2_FOUR f s2) (f_3_ZERO f_3_FOUR f s2) (f_3_ZERO f_4_FOUR f s2) (f_3_ZERO f_5_FOUR f s2) (f_3_ZERO f_0_SIX f s1) (f_3_ZERO f_1_SIX f s1) (f_3_ZERO f_2_SIX f s1) (f_3_ZERO f_3_SIX f s1) (f_3_ZERO f_4_SIX f s1) (f_3_ZERO f_5_SIX f s1) (f_3_ONE f_0_ZERO f s4) (f_3_ONE f_1_ZERO f s4) (f_3_ONE f_2_ZERO f s4) (f_3_ONE f_3_ZERO f s4) (f_3_ONE f_4_ZERO f s4) (f_3_ONE f_5_ZERO f s4) (f_3_ONE f_0_TWO f s3) (f_3_ONE f_1_TWO f s3) (f_3_ONE f_2_TWO f s3) (f_3_ONE f_3_TWO f s3) (f_3_ONE f_4_TWO f s3) (f_3_ONE f_5_TWO f s3) (f_3_ONE f_0_FOUR f s2) (f_3_ONE f_1_FOUR f s2) (f_3_ONE f_2_FOUR f s2) (f_3_ONE f_3_FOUR f s2) (f_3_ONE f_4_FOUR f s2) (f_3_ONE f_5_FOUR f s2) (f_3_ONE f_0_SIX f s1) (f_3_ONE f_1_SIX f s1) (f_3_ONE f_2_SIX f s1) (f_3_ONE f_3_SIX f s1) (f_3_ONE f_4_SIX f s1) (f_3_ONE f_5_SIX f s1) (f_3_TWO f_0_ZERO f s4) (f_3_TWO f_1_ZERO f s4) (f_3_TWO f_2_ZERO f s4) (f_3_TWO f_3_ZERO f s4) (f_3_TWO f_4_ZERO f s4) (f_3_TWO f_5_ZERO f s4) (f_3_TWO f_0_TWO f s3) (f_3_TWO f_1_TWO f s3) (f_3_TWO f_2_TWO f s3) (f_3_TWO f_3_TWO f s3) (f_3_TWO f_4_TWO f s3) (f_3_TWO f_5_TWO f s3) (f_3_TWO f_0_FOUR f s2) (f_3_TWO f_1_FOUR f s2) (f_3_TWO f_2_FOUR f s2) (f_3_TWO f_3_FOUR f s2) (f_3_TWO f_4_FOUR f s2) (f_3_TWO f_5_FOUR f s2) (f_3_TWO f_0_SIX f s1) (f_3_TWO f_1_SIX f s1) (f_3_TWO f_2_SIX f s1) (f_3_TWO f_3_SIX f s1) (f_3_TWO f_4_SIX f s1) (f_3_TWO f_5_SIX f s1) (f_3_THREE f_0_ZERO f s4) (f_3_THREE f_1_ZERO f s4) (f_3_THREE f_2_ZERO f s4) (f_3_THREE f_3_ZERO f s4) (f_3_THREE f_4_ZERO f s4) (f_3_THREE f_5_ZERO f s4) (f_3_THREE f_0_TWO f s3) (f_3_THREE f_1_TWO f s3) (f_3_THREE f_2_TWO f s3) (f_3_THREE f_3_TWO f s3) (f_3_THREE f_4_TWO f s3) (f_3_THREE f_5_TWO f s3) (f_3_THREE f_0_FOUR f s2) (f_3_THREE f_1_FOUR f s2) (f_3_THREE f_2_FOUR f s2) (f_3_THREE f_3_FOUR f s2) (f_3_THREE f_4_FOUR f s2) (f_3_THREE f_5_FOUR f s2) (f_3_THREE f_0_SIX f s1) (f_3_THREE f_1_SIX f s1) (f_3_THREE f_2_SIX f s1) (f_3_THREE f_3_SIX f s1) (f_3_THREE f_4_SIX f s1) (f_3_THREE f_5_SIX f s1) (f_3_FOUR f_0_ZERO f s4) (f_3_FOUR f_1_ZERO f s4) (f_3_FOUR f_2_ZERO f s4) (f_3_FOUR f_3_ZERO f s4) (f_3_FOUR f_4_ZERO f s4) (f_3_FOUR f_5_ZERO f s4) (f_3_FOUR f_0_TWO f s3) (f_3_FOUR f_1_TWO f s3) (f_3_FOUR f_2_TWO f s3) (f_3_FOUR f_3_TWO f s3) (f_3_FOUR f_4_TWO f s3) (f_3_FOUR f_5_TWO f s3) (f_3_FOUR f_0_FOUR f s2) (f_3_FOUR f_1_FOUR f s2) (f_3_FOUR f_2_FOUR f s2) (f_3_FOUR f_3_FOUR f s2) (f_3_FOUR f_4_FOUR f s2) (f_3_FOUR f_5_FOUR f s2) (f_3_FOUR f_0_SIX f s1) (f_3_FOUR f_1_SIX f s1) (f_3_FOUR f_2_SIX f s1) (f_3_FOUR f_3_SIX f s1) (f_3_FOUR f_4_SIX f s1) (f_3_FOUR f_5_SIX f s1) (f_3_FIVE f_0_ZERO f s4) (f_3_FIVE f_1_ZERO f s4) (f_3_FIVE f_2_ZERO f s4) (f_3_FIVE f_3_ZERO f s4) (f_3_FIVE f_4_ZERO f s4) (f_3_FIVE f_5_ZERO f s4) (f_3_FIVE f_0_TWO f s3) (f_3_FIVE f_1_TWO f s3) (f_3_FIVE f_2_TWO f s3) (f_3_FIVE f_3_TWO f s3) (f_3_FIVE f_4_TWO f s3) (f_3_FIVE f_5_TWO f s3) (f_3_FIVE f_0_FOUR f s2) (f_3_FIVE f_1_FOUR f s2) (f_3_FIVE f_2_FOUR f s2) (f_3_FIVE f_3_FOUR f s2) (f_3_FIVE f_4_FOUR f s2) (f_3_FIVE f_5_FOUR f s2) (f_3_FIVE f_0_SIX f s1) (f_3_FIVE f_1_SIX f s1) (f_3_FIVE f_2_SIX f s1) (f_3_FIVE f_3_SIX f s1) (f_3_FIVE f_4_SIX f s1) (f_3_FIVE f_5_SIX f s1) (f_3_SIX f_0_ZERO f s4) (f_3_SIX f_1_ZERO f s4) (f_3_SIX f_2_ZERO f s4) (f_3_SIX f_3_ZERO f s4) (f_3_SIX f_4_ZERO f s4) (f_3_SIX f_5_ZERO f s4) (f_3_SIX f_0_TWO f s3) (f_3_SIX f_1_TWO f s3) (f_3_SIX f_2_TWO f s3) (f_3_SIX f_3_TWO f s3) (f_3_SIX f_4_TWO f s3) (f_3_SIX f_5_TWO f s3) (f_3_SIX f_0_FOUR f s2) (f_3_SIX f_1_FOUR f s2) (f_3_SIX f_2_FOUR f s2) (f_3_SIX f_3_FOUR f s2) (f_3_SIX f_4_FOUR f s2) (f_3_SIX f_5_FOUR f s2) (f_3_SIX f_0_SIX f s1) (f_3_SIX f_1_SIX f s1) (f_3_SIX f_2_SIX f s1) (f_3_SIX f_3_SIX f s1) (f_3_SIX f_4_SIX f s1) (f_3_SIX f_5_SIX f s1) (f_3_ZERO f_0_ONE e s4) (f_3_ZERO f_1_ONE e s4) (f_3_ZERO f_2_ONE e s4) (f_3_ZERO f_3_ONE e s4) (f_3_ZERO f_4_ONE e s4) (f_3_ZERO f_5_ONE e s4) (f_3_ZERO f_0_THREE e s3) (f_3_ZERO f_1_THREE e s3) (f_3_ZERO f_2_THREE e s3) (f_3_ZERO f_3_THREE e s3) (f_3_ZERO f_4_THREE e s3) (f_3_ZERO f_5_THREE e s3) (f_3_ZERO f_0_FIVE e s2) (f_3_ZERO f_1_FIVE e s2) (f_3_ZERO f_2_FIVE e s2) (f_3_ZERO f_3_FIVE e s2) (f_3_ZERO f_4_FIVE e s2) (f_3_ZERO f_5_FIVE e s2) (f_3_ONE f_0_ONE e s4) (f_3_ONE f_1_ONE e s4) (f_3_ONE f_2_ONE e s4) (f_3_ONE f_3_ONE e s4) (f_3_ONE f_4_ONE e s4) (f_3_ONE f_5_ONE e s4) (f_3_ONE f_0_THREE e s3) (f_3_ONE f_1_THREE e s3) (f_3_ONE f_2_THREE e s3) (f_3_ONE f_3_THREE e s3) (f_3_ONE f_4_THREE e s3) (f_3_ONE f_5_THREE e s3) (f_3_ONE f_0_FIVE e s2) (f_3_ONE f_1_FIVE e s2) (f_3_ONE f_2_FIVE e s2) (f_3_ONE f_3_FIVE e s2) (f_3_ONE f_4_FIVE e s2) (f_3_ONE f_5_FIVE e s2) (f_3_TWO f_0_ONE e s4) (f_3_TWO f_1_ONE e s4) (f_3_TWO f_2_ONE e s4) (f_3_TWO f_3_ONE e s4) (f_3_TWO f_4_ONE e s4) (f_3_TWO f_5_ONE e s4) (f_3_TWO f_0_THREE e s3) (f_3_TWO f_1_THREE e s3) (f_3_TWO f_2_THREE e s3) (f_3_TWO f_3_THREE e s3) (f_3_TWO f_4_THREE e s3) (f_3_TWO f_5_THREE e s3) (f_3_TWO f_0_FIVE e s2) (f_3_TWO f_1_FIVE e s2) (f_3_TWO f_2_FIVE e s2) (f_3_TWO f_3_FIVE e s2) (f_3_TWO f_4_FIVE e s2) (f_3_TWO f_5_FIVE e s2) (f_3_THREE f_0_ONE e s4) (f_3_THREE f_1_ONE e s4) (f_3_THREE f_2_ONE e s4) (f_3_THREE f_3_ONE e s4) (f_3_THREE f_4_ONE e s4) (f_3_THREE f_5_ONE e s4) (f_3_THREE f_0_THREE e s3) (f_3_THREE f_1_THREE e s3) (f_3_THREE f_2_THREE e s3) (f_3_THREE f_3_THREE e s3) (f_3_THREE f_4_THREE e s3) (f_3_THREE f_5_THREE e s3) (f_3_THREE f_0_FIVE e s2) (f_3_THREE f_1_FIVE e s2) (f_3_THREE f_2_FIVE e s2) (f_3_THREE f_3_FIVE e s2) (f_3_THREE f_4_FIVE e s2) (f_3_THREE f_5_FIVE e s2) (f_3_FOUR f_0_ONE e s4) (f_3_FOUR f_1_ONE e s4) (f_3_FOUR f_2_ONE e s4) (f_3_FOUR f_3_ONE e s4) (f_3_FOUR f_4_ONE e s4) (f_3_FOUR f_5_ONE e s4) (f_3_FOUR f_0_THREE e s3) (f_3_FOUR f_1_THREE e s3) (f_3_FOUR f_2_THREE e s3) (f_3_FOUR f_3_THREE e s3) (f_3_FOUR f_4_THREE e s3) (f_3_FOUR f_5_THREE e s3) (f_3_FOUR f_0_FIVE e s2) (f_3_FOUR f_1_FIVE e s2) (f_3_FOUR f_2_FIVE e s2) (f_3_FOUR f_3_FIVE e s2) (f_3_FOUR f_4_FIVE e s2) (f_3_FOUR f_5_FIVE e s2) (f_3_FIVE f_0_ONE e s4) (f_3_FIVE f_1_ONE e s4) (f_3_FIVE f_2_ONE e s4) (f_3_FIVE f_3_ONE e s4) (f_3_FIVE f_4_ONE e s4) (f_3_FIVE f_5_ONE e s4) (f_3_FIVE f_0_THREE e s3) (f_3_FIVE f_1_THREE e s3) (f_3_FIVE f_2_THREE e s3) (f_3_FIVE f_3_THREE e s3) (f_3_FIVE f_4_THREE e s3) (f_3_FIVE f_5_THREE e s3) (f_3_FIVE f_0_FIVE e s2) (f_3_FIVE f_1_FIVE e s2) (f_3_FIVE f_2_FIVE e s2) (f_3_FIVE f_3_FIVE e s2) (f_3_FIVE f_4_FIVE e s2) (f_3_FIVE f_5_FIVE e s2) (f_3_SIX f_0_ONE e s4) (f_3_SIX f_1_ONE e s4) (f_3_SIX f_2_ONE e s4) (f_3_SIX f_3_ONE e s4) (f_3_SIX f_4_ONE e s4) (f_3_SIX f_5_ONE e s4) (f_3_SIX f_0_THREE e s3) (f_3_SIX f_1_THREE e s3) (f_3_SIX f_2_THREE e s3) (f_3_SIX f_3_THREE e s3) (f_3_SIX f_4_THREE e s3) (f_3_SIX f_5_THREE e s3) (f_3_SIX f_0_FIVE e s2) (f_3_SIX f_1_FIVE e s2) (f_3_SIX f_2_FIVE e s2) (f_3_SIX f_3_FIVE e s2) (f_3_SIX f_4_FIVE e s2) (f_3_SIX f_5_FIVE e s2) (s3 f_0_ZERO f s4) (s3 f_1_ZERO f s4) (s3 f_2_ZERO f s4) (s3 f_3_ZERO f s4) (s3 f_4_ZERO f s4) (s3 f_5_ZERO f s4) (s3 f_0_TWO f s3) (s3 f_1_TWO f s3) (s3 f_2_TWO f s3) (s3 f_3_TWO f s3) (s3 f_4_TWO f s3) (s3 f_5_TWO f s3) (s3 f_0_FOUR f s2) (s3 f_1_FOUR f s2) (s3 f_2_FOUR f s2) (s3 f_3_FOUR f s2) (s3 f_4_FOUR f s2) (s3 f_5_FOUR f s2) (s3 f_0_SIX f s1) (s3 f_1_SIX f s1) (s3 f_2_SIX f s1) (s3 f_3_SIX f s1) (s3 f_4_SIX f s1) (s3 f_5_SIX f s1) (s3 f_0_ONE e s4) (s3 f_1_ONE e s4) (s3 f_2_ONE e s4) (s3 f_3_ONE e s4) (s3 f_4_ONE e s4) (s3 f_5_ONE e s4) (s3 f_0_THREE e s3) (s3 f_1_THREE e s3) (s3 f_2_THREE e s3) (s3 f_3_THREE e s3) (s3 f_4_THREE e s3) (s3 f_5_THREE e s3) (s3 f_0_FIVE e s2) (s3 f_1_FIVE e s2) (s3 f_2_FIVE e s2) (s3 f_3_FIVE e s2) (s3 f_4_FIVE e s2) (s3 f_5_FIVE e s2) (f_4_ZERO f_0_ZERO e s5) (f_4_ZERO f_1_ZERO e s5) (f_4_ZERO f_2_ZERO e s5) (f_4_ZERO f_3_ZERO e s5) (f_4_ZERO f_4_ZERO e s5) (f_4_ZERO f_5_ZERO e s5) (f_4_ZERO f_0_TWO e s4) (f_4_ZERO f_1_TWO e s4) (f_4_ZERO f_2_TWO e s4) (f_4_ZERO f_3_TWO e s4) (f_4_ZERO f_4_TWO e s4) (f_4_ZERO f_5_TWO e s4) (f_4_ZERO f_0_FOUR e s3) (f_4_ZERO f_1_FOUR e s3) (f_4_ZERO f_2_FOUR e s3) (f_4_ZERO f_3_FOUR e s3) (f_4_ZERO f_4_FOUR e s3) (f_4_ZERO f_5_FOUR e s3) (f_4_ZERO f_0_SIX e s2) (f_4_ZERO f_1_SIX e s2) (f_4_ZERO f_2_SIX e s2) (f_4_ZERO f_3_SIX e s2) (f_4_ZERO f_4_SIX e s2) (f_4_ZERO f_5_SIX e s2) (f_4_ONE f_0_ZERO e s5) (f_4_ONE f_1_ZERO e s5) (f_4_ONE f_2_ZERO e s5) (f_4_ONE f_3_ZERO e s5) (f_4_ONE f_4_ZERO e s5) (f_4_ONE f_5_ZERO e s5) (f_4_ONE f_0_TWO e s4) (f_4_ONE f_1_TWO e s4) (f_4_ONE f_2_TWO e s4) (f_4_ONE f_3_TWO e s4) (f_4_ONE f_4_TWO e s4) (f_4_ONE f_5_TWO e s4) (f_4_ONE f_0_FOUR e s3) (f_4_ONE f_1_FOUR e s3) (f_4_ONE f_2_FOUR e s3) (f_4_ONE f_3_FOUR e s3) (f_4_ONE f_4_FOUR e s3) (f_4_ONE f_5_FOUR e s3) (f_4_ONE f_0_SIX e s2) (f_4_ONE f_1_SIX e s2) (f_4_ONE f_2_SIX e s2) (f_4_ONE f_3_SIX e s2) (f_4_ONE f_4_SIX e s2) (f_4_ONE f_5_SIX e s2) (f_4_TWO f_0_ZERO e s5) (f_4_TWO f_1_ZERO e s5) (f_4_TWO f_2_ZERO e s5) (f_4_TWO f_3_ZERO e s5) (f_4_TWO f_4_ZERO e s5) (f_4_TWO f_5_ZERO e s5) (f_4_TWO f_0_TWO e s4) (f_4_TWO f_1_TWO e s4) (f_4_TWO f_2_TWO e s4) (f_4_TWO f_3_TWO e s4) (f_4_TWO f_4_TWO e s4) (f_4_TWO f_5_TWO e s4) (f_4_TWO f_0_FOUR e s3) (f_4_TWO f_1_FOUR e s3) (f_4_TWO f_2_FOUR e s3) (f_4_TWO f_3_FOUR e s3) (f_4_TWO f_4_FOUR e s3) (f_4_TWO f_5_FOUR e s3) (f_4_TWO f_0_SIX e s2) (f_4_TWO f_1_SIX e s2) (f_4_TWO f_2_SIX e s2) (f_4_TWO f_3_SIX e s2) (f_4_TWO f_4_SIX e s2) (f_4_TWO f_5_SIX e s2) (f_4_THREE f_0_ZERO e s5) (f_4_THREE f_1_ZERO e s5) (f_4_THREE f_2_ZERO e s5) (f_4_THREE f_3_ZERO e s5) (f_4_THREE f_4_ZERO e s5) (f_4_THREE f_5_ZERO e s5) (f_4_THREE f_0_TWO e s4) (f_4_THREE f_1_TWO e s4) (f_4_THREE f_2_TWO e s4) (f_4_THREE f_3_TWO e s4) (f_4_THREE f_4_TWO e s4) (f_4_THREE f_5_TWO e s4) (f_4_THREE f_0_FOUR e s3) (f_4_THREE f_1_FOUR e s3) (f_4_THREE f_2_FOUR e s3) (f_4_THREE f_3_FOUR e s3) (f_4_THREE f_4_FOUR e s3) (f_4_THREE f_5_FOUR e s3) (f_4_THREE f_0_SIX e s2) (f_4_THREE f_1_SIX e s2) (f_4_THREE f_2_SIX e s2) (f_4_THREE f_3_SIX e s2) (f_4_THREE f_4_SIX e s2) (f_4_THREE f_5_SIX e s2) (f_4_FOUR f_0_ZERO e s5) (f_4_FOUR f_1_ZERO e s5) (f_4_FOUR f_2_ZERO e s5) (f_4_FOUR f_3_ZERO e s5) (f_4_FOUR f_4_ZERO e s5) (f_4_FOUR f_5_ZERO e s5) (f_4_FOUR f_0_TWO e s4) (f_4_FOUR f_1_TWO e s4) (f_4_FOUR f_2_TWO e s4) (f_4_FOUR f_3_TWO e s4) (f_4_FOUR f_4_TWO e s4) (f_4_FOUR f_5_TWO e s4) (f_4_FOUR f_0_FOUR e s3) (f_4_FOUR f_1_FOUR e s3) (f_4_FOUR f_2_FOUR e s3) (f_4_FOUR f_3_FOUR e s3) (f_4_FOUR f_4_FOUR e s3) (f_4_FOUR f_5_FOUR e s3) (f_4_FOUR f_0_SIX e s2) (f_4_FOUR f_1_SIX e s2) (f_4_FOUR f_2_SIX e s2) (f_4_FOUR f_3_SIX e s2) (f_4_FOUR f_4_SIX e s2) (f_4_FOUR f_5_SIX e s2) (f_4_FIVE f_0_ZERO e s5) (f_4_FIVE f_1_ZERO e s5) (f_4_FIVE f_2_ZERO e s5) (f_4_FIVE f_3_ZERO e s5) (f_4_FIVE f_4_ZERO e s5) (f_4_FIVE f_5_ZERO e s5) (f_4_FIVE f_0_TWO e s4) (f_4_FIVE f_1_TWO e s4) (f_4_FIVE f_2_TWO e s4) (f_4_FIVE f_3_TWO e s4) (f_4_FIVE f_4_TWO e s4) (f_4_FIVE f_5_TWO e s4) (f_4_FIVE f_0_FOUR e s3) (f_4_FIVE f_1_FOUR e s3) (f_4_FIVE f_2_FOUR e s3) (f_4_FIVE f_3_FOUR e s3) (f_4_FIVE f_4_FOUR e s3) (f_4_FIVE f_5_FOUR e s3) (f_4_FIVE f_0_SIX e s2) (f_4_FIVE f_1_SIX e s2) (f_4_FIVE f_2_SIX e s2) (f_4_FIVE f_3_SIX e s2) (f_4_FIVE f_4_SIX e s2) (f_4_FIVE f_5_SIX e s2) (f_4_SIX f_0_ZERO e s5) (f_4_SIX f_1_ZERO e s5) (f_4_SIX f_2_ZERO e s5) (f_4_SIX f_3_ZERO e s5) (f_4_SIX f_4_ZERO e s5) (f_4_SIX f_5_ZERO e s5) (f_4_SIX f_0_TWO e s4) (f_4_SIX f_1_TWO e s4) (f_4_SIX f_2_TWO e s4) (f_4_SIX f_3_TWO e s4) (f_4_SIX f_4_TWO e s4) (f_4_SIX f_5_TWO e s4) (f_4_SIX f_0_FOUR e s3) (f_4_SIX f_1_FOUR e s3) (f_4_SIX f_2_FOUR e s3) (f_4_SIX f_3_FOUR e s3) (f_4_SIX f_4_FOUR e s3) (f_4_SIX f_5_FOUR e s3) (f_4_SIX f_0_SIX e s2) (f_4_SIX f_1_SIX e s2) (f_4_SIX f_2_SIX e s2) (f_4_SIX f_3_SIX e s2) (f_4_SIX f_4_SIX e s2) (f_4_SIX f_5_SIX e s2) (f_4_ZERO f_0_ONE f s4) (f_4_ZERO f_1_ONE f s4) (f_4_ZERO f_2_ONE f s4) (f_4_ZERO f_3_ONE f s4) (f_4_ZERO f_4_ONE f s4) (f_4_ZERO f_5_ONE f s4) (f_4_ZERO f_0_THREE f s3) (f_4_ZERO f_1_THREE f s3) (f_4_ZERO f_2_THREE f s3) (f_4_ZERO f_3_THREE f s3) (f_4_ZERO f_4_THREE f s3) (f_4_ZERO f_5_THREE f s3) (f_4_ZERO f_0_FIVE f s2) (f_4_ZERO f_1_FIVE f s2) (f_4_ZERO f_2_FIVE f s2) (f_4_ZERO f_3_FIVE f s2) (f_4_ZERO f_4_FIVE f s2) (f_4_ZERO f_5_FIVE f s2) (f_4_ONE f_0_ONE f s4) (f_4_ONE f_1_ONE f s4) (f_4_ONE f_2_ONE f s4) (f_4_ONE f_3_ONE f s4) (f_4_ONE f_4_ONE f s4) (f_4_ONE f_5_ONE f s4) (f_4_ONE f_0_THREE f s3) (f_4_ONE f_1_THREE f s3) (f_4_ONE f_2_THREE f s3) (f_4_ONE f_3_THREE f s3) (f_4_ONE f_4_THREE f s3) (f_4_ONE f_5_THREE f s3) (f_4_ONE f_0_FIVE f s2) (f_4_ONE f_1_FIVE f s2) (f_4_ONE f_2_FIVE f s2) (f_4_ONE f_3_FIVE f s2) (f_4_ONE f_4_FIVE f s2) (f_4_ONE f_5_FIVE f s2) (f_4_TWO f_0_ONE f s4) (f_4_TWO f_1_ONE f s4) (f_4_TWO f_2_ONE f s4) (f_4_TWO f_3_ONE f s4) (f_4_TWO f_4_ONE f s4) (f_4_TWO f_5_ONE f s4) (f_4_TWO f_0_THREE f s3) (f_4_TWO f_1_THREE f s3) (f_4_TWO f_2_THREE f s3) (f_4_TWO f_3_THREE f s3) (f_4_TWO f_4_THREE f s3) (f_4_TWO f_5_THREE f s3) (f_4_TWO f_0_FIVE f s2) (f_4_TWO f_1_FIVE f s2) (f_4_TWO f_2_FIVE f s2) (f_4_TWO f_3_FIVE f s2) (f_4_TWO f_4_FIVE f s2) (f_4_TWO f_5_FIVE f s2) (f_4_THREE f_0_ONE f s4) (f_4_THREE f_1_ONE f s4) (f_4_THREE f_2_ONE f s4) (f_4_THREE f_3_ONE f s4) (f_4_THREE f_4_ONE f s4) (f_4_THREE f_5_ONE f s4) (f_4_THREE f_0_THREE f s3) (f_4_THREE f_1_THREE f s3) (f_4_THREE f_2_THREE f s3) (f_4_THREE f_3_THREE f s3) (f_4_THREE f_4_THREE f s3) (f_4_THREE f_5_THREE f s3) (f_4_THREE f_0_FIVE f s2) (f_4_THREE f_1_FIVE f s2) (f_4_THREE f_2_FIVE f s2) (f_4_THREE f_3_FIVE f s2) (f_4_THREE f_4_FIVE f s2) (f_4_THREE f_5_FIVE f s2) (f_4_FOUR f_0_ONE f s4) (f_4_FOUR f_1_ONE f s4) (f_4_FOUR f_2_ONE f s4) (f_4_FOUR f_3_ONE f s4) (f_4_FOUR f_4_ONE f s4) (f_4_FOUR f_5_ONE f s4) (f_4_FOUR f_0_THREE f s3) (f_4_FOUR f_1_THREE f s3) (f_4_FOUR f_2_THREE f s3) (f_4_FOUR f_3_THREE f s3) (f_4_FOUR f_4_THREE f s3) (f_4_FOUR f_5_THREE f s3) (f_4_FOUR f_0_FIVE f s2) (f_4_FOUR f_1_FIVE f s2) (f_4_FOUR f_2_FIVE f s2) (f_4_FOUR f_3_FIVE f s2) (f_4_FOUR f_4_FIVE f s2) (f_4_FOUR f_5_FIVE f s2) (f_4_FIVE f_0_ONE f s4) (f_4_FIVE f_1_ONE f s4) (f_4_FIVE f_2_ONE f s4) (f_4_FIVE f_3_ONE f s4) (f_4_FIVE f_4_ONE f s4) (f_4_FIVE f_5_ONE f s4) (f_4_FIVE f_0_THREE f s3) (f_4_FIVE f_1_THREE f s3) (f_4_FIVE f_2_THREE f s3) (f_4_FIVE f_3_THREE f s3) (f_4_FIVE f_4_THREE f s3) (f_4_FIVE f_5_THREE f s3) (f_4_FIVE f_0_FIVE f s2) (f_4_FIVE f_1_FIVE f s2) (f_4_FIVE f_2_FIVE f s2) (f_4_FIVE f_3_FIVE f s2) (f_4_FIVE f_4_FIVE f s2) (f_4_FIVE f_5_FIVE f s2) (f_4_SIX f_0_ONE f s4) (f_4_SIX f_1_ONE f s4) (f_4_SIX f_2_ONE f s4) (f_4_SIX f_3_ONE f s4) (f_4_SIX f_4_ONE f s4) (f_4_SIX f_5_ONE f s4) (f_4_SIX f_0_THREE f s3) (f_4_SIX f_1_THREE f s3) (f_4_SIX f_2_THREE f s3) (f_4_SIX f_3_THREE f s3) (f_4_SIX f_4_THREE f s3) (f_4_SIX f_5_THREE f s3) (f_4_SIX f_0_FIVE f s2) (f_4_SIX f_1_FIVE f s2) (f_4_SIX f_2_FIVE f s2) (f_4_SIX f_3_FIVE f s2) (f_4_SIX f_4_FIVE f s2) (f_4_SIX f_5_FIVE f s2) (s4 f_0_ZERO e s5) (s4 f_1_ZERO e s5) (s4 f_2_ZERO e s5) (s4 f_3_ZERO e s5) (s4 f_4_ZERO e s5) (s4 f_5_ZERO e s5) (s4 f_0_TWO e s4) (s4 f_1_TWO e s4) (s4 f_2_TWO e s4) (s4 f_3_TWO e s4) (s4 f_4_TWO e s4) (s4 f_5_TWO e s4) (s4 f_0_FOUR e s3) (s4 f_1_FOUR e s3) (s4 f_2_FOUR e s3) (s4 f_3_FOUR e s3) (s4 f_4_FOUR e s3) (s4 f_5_FOUR e s3) (s4 f_0_SIX e s2) (s4 f_1_SIX e s2) (s4 f_2_SIX e s2) (s4 f_3_SIX e s2) (s4 f_4_SIX e s2) (s4 f_5_SIX e s2) (s4 f_0_ONE f s4) (s4 f_1_ONE f s4) (s4 f_2_ONE f s4) (s4 f_3_ONE f s4) (s4 f_4_ONE f s4) (s4 f_5_ONE f s4) (s4 f_0_THREE f s3) (s4 f_1_THREE f s3) (s4 f_2_THREE f s3) (s4 f_3_THREE f s3) (s4 f_4_THREE f s3) (s4 f_5_THREE f s3) (s4 f_0_FIVE f s2) (s4 f_1_FIVE f s2) (s4 f_2_FIVE f s2) (s4 f_3_FIVE f s2) (s4 f_4_FIVE f s2) (s4 f_5_FIVE f s2) (f_5_ZERO f_0_ZERO f s5) (f_5_ZERO f_1_ZERO f s5) (f_5_ZERO f_2_ZERO f s5) (f_5_ZERO f_3_ZERO f s5) (f_5_ZERO f_4_ZERO f s5) (f_5_ZERO f_5_ZERO f s5) (f_5_ZERO f_0_TWO f s4) (f_5_ZERO f_1_TWO f s4) (f_5_ZERO f_2_TWO f s4) (f_5_ZERO f_3_TWO f s4) (f_5_ZERO f_4_TWO f s4) (f_5_ZERO f_5_TWO f s4) (f_5_ZERO f_0_FOUR f s3) (f_5_ZERO f_1_FOUR f s3) (f_5_ZERO f_2_FOUR f s3) (f_5_ZERO f_3_FOUR f s3) (f_5_ZERO f_4_FOUR f s3) (f_5_ZERO f_5_FOUR f s3) (f_5_ZERO f_0_SIX f s2) (f_5_ZERO f_1_SIX f s2) (f_5_ZERO f_2_SIX f s2) (f_5_ZERO f_3_SIX f s2) (f_5_ZERO f_4_SIX f s2) (f_5_ZERO f_5_SIX f s2) (f_5_ONE f_0_ZERO f s5) (f_5_ONE f_1_ZERO f s5) (f_5_ONE f_2_ZERO f s5) (f_5_ONE f_3_ZERO f s5) (f_5_ONE f_4_ZERO f s5) (f_5_ONE f_5_ZERO f s5) (f_5_ONE f_0_TWO f s4) (f_5_ONE f_1_TWO f s4) (f_5_ONE f_2_TWO f s4) (f_5_ONE f_3_TWO f s4) (f_5_ONE f_4_TWO f s4) (f_5_ONE f_5_TWO f s4) (f_5_ONE f_0_FOUR f s3) (f_5_ONE f_1_FOUR f s3) (f_5_ONE f_2_FOUR f s3) (f_5_ONE f_3_FOUR f s3) (f_5_ONE f_4_FOUR f s3) (f_5_ONE f_5_FOUR f s3) (f_5_ONE f_0_SIX f s2) (f_5_ONE f_1_SIX f s2) (f_5_ONE f_2_SIX f s2) (f_5_ONE f_3_SIX f s2) (f_5_ONE f_4_SIX f s2) (f_5_ONE f_5_SIX f s2) (f_5_TWO f_0_ZERO f s5) (f_5_TWO f_1_ZERO f s5) (f_5_TWO f_2_ZERO f s5) (f_5_TWO f_3_ZERO f s5) (f_5_TWO f_4_ZERO f s5) (f_5_TWO f_5_ZERO f s5) (f_5_TWO f_0_TWO f s4) (f_5_TWO f_1_TWO f s4) (f_5_TWO f_2_TWO f s4) (f_5_TWO f_3_TWO f s4) (f_5_TWO f_4_TWO f s4) (f_5_TWO f_5_TWO f s4) (f_5_TWO f_0_FOUR f s3) (f_5_TWO f_1_FOUR f s3) (f_5_TWO f_2_FOUR f s3) (f_5_TWO f_3_FOUR f s3) (f_5_TWO f_4_FOUR f s3) (f_5_TWO f_5_FOUR f s3) (f_5_TWO f_0_SIX f s2) (f_5_TWO f_1_SIX f s2) (f_5_TWO f_2_SIX f s2) (f_5_TWO f_3_SIX f s2) (f_5_TWO f_4_SIX f s2) (f_5_TWO f_5_SIX f s2) (f_5_THREE f_0_ZERO f s5) (f_5_THREE f_1_ZERO f s5) (f_5_THREE f_2_ZERO f s5) (f_5_THREE f_3_ZERO f s5) (f_5_THREE f_4_ZERO f s5) (f_5_THREE f_5_ZERO f s5) (f_5_THREE f_0_TWO f s4) (f_5_THREE f_1_TWO f s4) (f_5_THREE f_2_TWO f s4) (f_5_THREE f_3_TWO f s4) (f_5_THREE f_4_TWO f s4) (f_5_THREE f_5_TWO f s4) (f_5_THREE f_0_FOUR f s3) (f_5_THREE f_1_FOUR f s3) (f_5_THREE f_2_FOUR f s3) (f_5_THREE f_3_FOUR f s3) (f_5_THREE f_4_FOUR f s3) (f_5_THREE f_5_FOUR f s3) (f_5_THREE f_0_SIX f s2) (f_5_THREE f_1_SIX f s2) (f_5_THREE f_2_SIX f s2) (f_5_THREE f_3_SIX f s2) (f_5_THREE f_4_SIX f s2) (f_5_THREE f_5_SIX f s2) (f_5_FOUR f_0_ZERO f s5) (f_5_FOUR f_1_ZERO f s5) (f_5_FOUR f_2_ZERO f s5) (f_5_FOUR f_3_ZERO f s5) (f_5_FOUR f_4_ZERO f s5) (f_5_FOUR f_5_ZERO f s5) (f_5_FOUR f_0_TWO f s4) (f_5_FOUR f_1_TWO f s4) (f_5_FOUR f_2_TWO f s4) (f_5_FOUR f_3_TWO f s4) (f_5_FOUR f_4_TWO f s4) (f_5_FOUR f_5_TWO f s4) (f_5_FOUR f_0_FOUR f s3) (f_5_FOUR f_1_FOUR f s3) (f_5_FOUR f_2_FOUR f s3) (f_5_FOUR f_3_FOUR f s3) (f_5_FOUR f_4_FOUR f s3) (f_5_FOUR f_5_FOUR f s3) (f_5_FOUR f_0_SIX f s2) (f_5_FOUR f_1_SIX f s2) (f_5_FOUR f_2_SIX f s2) (f_5_FOUR f_3_SIX f s2) (f_5_FOUR f_4_SIX f s2) (f_5_FOUR f_5_SIX f s2) (f_5_FIVE f_0_ZERO f s5) (f_5_FIVE f_1_ZERO f s5) (f_5_FIVE f_2_ZERO f s5) (f_5_FIVE f_3_ZERO f s5) (f_5_FIVE f_4_ZERO f s5) (f_5_FIVE f_5_ZERO f s5) (f_5_FIVE f_0_TWO f s4) (f_5_FIVE f_1_TWO f s4) (f_5_FIVE f_2_TWO f s4) (f_5_FIVE f_3_TWO f s4) (f_5_FIVE f_4_TWO f s4) (f_5_FIVE f_5_TWO f s4) (f_5_FIVE f_0_FOUR f s3) (f_5_FIVE f_1_FOUR f s3) (f_5_FIVE f_2_FOUR f s3) (f_5_FIVE f_3_FOUR f s3) (f_5_FIVE f_4_FOUR f s3) (f_5_FIVE f_5_FOUR f s3) (f_5_FIVE f_0_SIX f s2) (f_5_FIVE f_1_SIX f s2) (f_5_FIVE f_2_SIX f s2) (f_5_FIVE f_3_SIX f s2) (f_5_FIVE f_4_SIX f s2) (f_5_FIVE f_5_SIX f s2) (f_5_SIX f_0_ZERO f s5) (f_5_SIX f_1_ZERO f s5) (f_5_SIX f_2_ZERO f s5) (f_5_SIX f_3_ZERO f s5) (f_5_SIX f_4_ZERO f s5) (f_5_SIX f_5_ZERO f s5) (f_5_SIX f_0_TWO f s4) (f_5_SIX f_1_TWO f s4) (f_5_SIX f_2_TWO f s4) (f_5_SIX f_3_TWO f s4) (f_5_SIX f_4_TWO f s4) (f_5_SIX f_5_TWO f s4) (f_5_SIX f_0_FOUR f s3) (f_5_SIX f_1_FOUR f s3) (f_5_SIX f_2_FOUR f s3) (f_5_SIX f_3_FOUR f s3) (f_5_SIX f_4_FOUR f s3) (f_5_SIX f_5_FOUR f s3) (f_5_SIX f_0_SIX f s2) (f_5_SIX f_1_SIX f s2) (f_5_SIX f_2_SIX f s2) (f_5_SIX f_3_SIX f s2) (f_5_SIX f_4_SIX f s2) (f_5_SIX f_5_SIX f s2) (f_5_ZERO f_0_ONE e s5) (f_5_ZERO f_1_ONE e s5) (f_5_ZERO f_2_ONE e s5) (f_5_ZERO f_3_ONE e s5) (f_5_ZERO f_4_ONE e s5) (f_5_ZERO f_5_ONE e s5) (f_5_ZERO f_0_THREE e s4) (f_5_ZERO f_1_THREE e s4) (f_5_ZERO f_2_THREE e s4) (f_5_ZERO f_3_THREE e s4) (f_5_ZERO f_4_THREE e s4) (f_5_ZERO f_5_THREE e s4) (f_5_ZERO f_0_FIVE e s3) (f_5_ZERO f_1_FIVE e s3) (f_5_ZERO f_2_FIVE e s3) (f_5_ZERO f_3_FIVE e s3) (f_5_ZERO f_4_FIVE e s3) (f_5_ZERO f_5_FIVE e s3) (f_5_ONE f_0_ONE e s5) (f_5_ONE f_1_ONE e s5) (f_5_ONE f_2_ONE e s5) (f_5_ONE f_3_ONE e s5) (f_5_ONE f_4_ONE e s5) (f_5_ONE f_5_ONE e s5) (f_5_ONE f_0_THREE e s4) (f_5_ONE f_1_THREE e s4) (f_5_ONE f_2_THREE e s4) (f_5_ONE f_3_THREE e s4) (f_5_ONE f_4_THREE e s4) (f_5_ONE f_5_THREE e s4) (f_5_ONE f_0_FIVE e s3) (f_5_ONE f_1_FIVE e s3) (f_5_ONE f_2_FIVE e s3) (f_5_ONE f_3_FIVE e s3) (f_5_ONE f_4_FIVE e s3) (f_5_ONE f_5_FIVE e s3) (f_5_TWO f_0_ONE e s5) (f_5_TWO f_1_ONE e s5) (f_5_TWO f_2_ONE e s5) (f_5_TWO f_3_ONE e s5) (f_5_TWO f_4_ONE e s5) (f_5_TWO f_5_ONE e s5) (f_5_TWO f_0_THREE e s4) (f_5_TWO f_1_THREE e s4) (f_5_TWO f_2_THREE e s4) (f_5_TWO f_3_THREE e s4) (f_5_TWO f_4_THREE e s4) (f_5_TWO f_5_THREE e s4) (f_5_TWO f_0_FIVE e s3) (f_5_TWO f_1_FIVE e s3) (f_5_TWO f_2_FIVE e s3) (f_5_TWO f_3_FIVE e s3) (f_5_TWO f_4_FIVE e s3) (f_5_TWO f_5_FIVE e s3) (f_5_THREE f_0_ONE e s5) (f_5_THREE f_1_ONE e s5) (f_5_THREE f_2_ONE e s5) (f_5_THREE f_3_ONE e s5) (f_5_THREE f_4_ONE e s5) (f_5_THREE f_5_ONE e s5) (f_5_THREE f_0_THREE e s4) (f_5_THREE f_1_THREE e s4) (f_5_THREE f_2_THREE e s4) (f_5_THREE f_3_THREE e s4) (f_5_THREE f_4_THREE e s4) (f_5_THREE f_5_THREE e s4) (f_5_THREE f_0_FIVE e s3) (f_5_THREE f_1_FIVE e s3) (f_5_THREE f_2_FIVE e s3) (f_5_THREE f_3_FIVE e s3) (f_5_THREE f_4_FIVE e s3) (f_5_THREE f_5_FIVE e s3) (f_5_FOUR f_0_ONE e s5) (f_5_FOUR f_1_ONE e s5) (f_5_FOUR f_2_ONE e s5) (f_5_FOUR f_3_ONE e s5) (f_5_FOUR f_4_ONE e s5) (f_5_FOUR f_5_ONE e s5) (f_5_FOUR f_0_THREE e s4) (f_5_FOUR f_1_THREE e s4) (f_5_FOUR f_2_THREE e s4) (f_5_FOUR f_3_THREE e s4) (f_5_FOUR f_4_THREE e s4) (f_5_FOUR f_5_THREE e s4) (f_5_FOUR f_0_FIVE e s3) (f_5_FOUR f_1_FIVE e s3) (f_5_FOUR f_2_FIVE e s3) (f_5_FOUR f_3_FIVE e s3) (f_5_FOUR f_4_FIVE e s3) (f_5_FOUR f_5_FIVE e s3) (f_5_FIVE f_0_ONE e s5) (f_5_FIVE f_1_ONE e s5) (f_5_FIVE f_2_ONE e s5) (f_5_FIVE f_3_ONE e s5) (f_5_FIVE f_4_ONE e s5) (f_5_FIVE f_5_ONE e s5) (f_5_FIVE f_0_THREE e s4) (f_5_FIVE f_1_THREE e s4) (f_5_FIVE f_2_THREE e s4) (f_5_FIVE f_3_THREE e s4) (f_5_FIVE f_4_THREE e s4) (f_5_FIVE f_5_THREE e s4) (f_5_FIVE f_0_FIVE e s3) (f_5_FIVE f_1_FIVE e s3) (f_5_FIVE f_2_FIVE e s3) (f_5_FIVE f_3_FIVE e s3) (f_5_FIVE f_4_FIVE e s3) (f_5_FIVE f_5_FIVE e s3) (f_5_SIX f_0_ONE e s5) (f_5_SIX f_1_ONE e s5) (f_5_SIX f_2_ONE e s5) (f_5_SIX f_3_ONE e s5) (f_5_SIX f_4_ONE e s5) (f_5_SIX f_5_ONE e s5) (f_5_SIX f_0_THREE e s4) (f_5_SIX f_1_THREE e s4) (f_5_SIX f_2_THREE e s4) (f_5_SIX f_3_THREE e s4) (f_5_SIX f_4_THREE e s4) (f_5_SIX f_5_THREE e s4) (f_5_SIX f_0_FIVE e s3) (f_5_SIX f_1_FIVE e s3) (f_5_SIX f_2_FIVE e s3) (f_5_SIX f_3_FIVE e s3) (f_5_SIX f_4_FIVE e s3) (f_5_SIX f_5_FIVE e s3) (s5 f_0_ZERO f s5) (s5 f_1_ZERO f s5) (s5 f_2_ZERO f s5) (s5 f_3_ZERO f s5) (s5 f_4_ZERO f s5) (s5 f_5_ZERO f s5) (s5 f_0_TWO f s4) (s5 f_1_TWO f s4) (s5 f_2_TWO f s4) (s5 f_3_TWO f s4) (s5 f_4_TWO f s4) (s5 f_5_TWO f s4) (s5 f_0_FOUR f s3) (s5 f_1_FOUR f s3) (s5 f_2_FOUR f s3) (s5 f_3_FOUR f s3) (s5 f_4_FOUR f s3) (s5 f_5_FOUR f s3) (s5 f_0_SIX f s2) (s5 f_1_SIX f s2) (s5 f_2_SIX f s2) (s5 f_3_SIX f s2) (s5 f_4_SIX f s2) (s5 f_5_SIX f s2) (s5 f_0_ONE e s5) (s5 f_1_ONE e s5) (s5 f_2_ONE e s5) (s5 f_3_ONE e s5) (s5 f_4_ONE e s5) (s5 f_5_ONE e s5) (s5 f_0_THREE e s4) (s5 f_1_THREE e s4) (s5 f_2_THREE e s4) (s5 f_3_THREE e s4) (s5 f_4_THREE e s4) (s5 f_5_THREE e s4) (s5 f_0_FIVE e s3) (s5 f_1_FIVE e s3) (s5 f_2_FIVE e s3) (s5 f_3_FIVE e s3) (s5 f_4_FIVE e s3) (s5 f_5_FIVE e s3) } ); NestedWordAutomaton syntaxChecker = ( callAlphabet = { a b }, internalAlphabet = { c d }, returnAlphabet = { e f }, states = {q1 q2 q3 q4 q5 acc}, initialStates = {q1}, finalStates = {acc}, callTransitions = { (q1 a q2) (q1 b q2) (q2 a q2) (q2 b q2) }, internalTransitions = { (q4 c q5) (q4 d q5) (q5 d acc) }, returnTransitions = { (q2 q2 e q3) (q2 q2 f q3) (q3 q2 e q3) (q3 q2 f q3) (q3 q1 e q4) (q3 q1 f q4) } ); //print(getAcceptedWord(Difference(syntaxChecker, antipalCheckerSIX))); assert(IsIncluded(syntaxChecker, antipalCheckerSIX));