Tbox: F F  ( !>= 3.L84 /\ F F G !>= 1.G14 )  <<  (  ( >= 3.L67 /\ F >= 4.G51 )  /\ F  ( C6 /\ !C0 )  ) 
Tbox: F G  ( G G >= 5.L65 /\ G G G >= 5.G69 )  <<  (  ( >= 4.G25 /\ C16 )  /\  ( F >= 3.G92 /\  ( C82 /\ >= 3.L0 )  )  ) 
Tbox: F  ( C41 /\ G F F G F !>= 2.L82 )  <<  ( F G G F C51 /\ F F F C91 ) 
Tbox: F G G F G G G  ( >= 3.L28 /\ >= 5.L37 )  << F  ( >= 3.G75 /\  ( >= 1.G90 /\  ( G C30 /\ F C30 )  )  ) 
Tbox:  (  ( G >= 1.L14 /\ G G F >= 4.G50 )  /\ !>= 2.L17 )  <<  ( F G >= 2.L13 /\ F F G G F C76 ) 
Tbox:  ( F C17 /\ F  ( !>= 2.G82 /\ G !C4 )  )  << G G G G  (  ( >= 3.L67 /\ C8 )  /\ G >= 4.G32 ) 
Tbox:  ( F G  ( C70 /\  ( >= 1.L6 /\ C43 )  )  /\ G >= 3.L76 )  << G G G  ( !C92 /\  ( C7 /\ !C42 )  ) 
Tbox: F G  ( C38 /\  ( G C35 /\ F F >= 3.L56 )  )  << F  (  ( !C42 /\ G >= 1.G25 )  /\  ( C90 /\ C66 )  ) 
Tbox: G G  ( C40 /\  ( F >= 3.G72 /\ G F >= 5.L33 )  )  << G  ( F >= 3.L45 /\  (  ( C9 /\ C44 )  /\ !C16 )  ) 
Tbox:  (  ( C14 /\ F  ( >= 5.G56 /\ !>= 5.G69 )  )  /\ !C86 )  <<  ( G G  ( C19 /\ >= 2.L79 )  /\  ( >= 3.L35 /\ !C27 )  ) 
Tbox: F F  ( F G C26 /\ F  ( >= 3.G87 /\ C83 )  )  << F  (  ( >= 3.G15 /\ G F >= 5.L16 )  /\ F G >= 3.G2 ) 
Tbox: F G F  ( C56 /\ F F F F C92 )  << F  ( C28 /\  (  ( >= 3.G77 /\ >= 1.G8 )  /\  ( >= 3.G25 /\ >= 4.G40 )  )  ) 
Tbox: G  ( C55 /\  (  ( C48 /\ C41 )  /\  ( >= 1.G70 /\ >= 2.L72 )  )  )  <<  ( !C23 /\ F G F F  ( C95 /\ >= 5.L68 )  ) 
Tbox:  ( G  ( C75 /\ F  ( >= 4.L7 /\ C40 )  )  /\ !>= 5.L84 )  << F  ( F >= 3.L13 /\  (  ( >= 1.G5 /\ >= 4.L70 )  /\ F C44 )  ) 
Tbox:  (  ( C79 /\  ( C38 /\ >= 2.L29 )  )  /\  ( C59 /\ G >= 1.L82 )  )  << F  (  ( C67 /\ >= 5.G79 )  /\ F  ( C49 /\ !C1 )  ) 
Tbox:  (  ( G G C42 /\  ( C13 /\ C81 )  )  /\ F >= 2.G41 )  << G F  ( >= 5.L26 /\ F G  ( C0 /\ F C86 )  ) 
Tbox:  ( C33 /\  ( F F F >= 4.L91 /\ F G >= 5.L10 )  )  <<  ( >= 5.L31 /\  (  ( >= 2.L6 /\ >= 1.L98 )  /\  ( >= 1.G34 /\ !C38 )  )  ) 
Tbox: G G  (  ( >= 3.G91 /\ >= 5.L5 )  /\ G G !>= 4.L34 )  << G  ( !C25 /\  ( G !C19 /\ G C41 )  ) 
Tbox: F  ( G F F !C49 /\ G F >= 4.G58 )  <<  ( C70 /\ F  ( C67 /\  ( !>= 4.G87 /\ !>= 1.L88 )  )  ) 
Tbox:  ( G !C36 /\ F F  ( >= 1.L63 /\ !>= 1.L36 )  )  << G F F F  ( F !>= 3.G23 /\ !>= 1.G15 ) 
Tbox:  ( >= 1.L95 /\ F  ( G F G >= 5.G32 /\ !C41 )  )  <<  (  ( >= 3.G61 /\ >= 3.G31 )  /\  ( G !>= 4.L54 /\ F >= 4.G3 )  ) 
Tbox: F  ( !>= 5.L26 /\  (  ( C99 /\ C5 )  /\ G C30 )  )  << F  ( >= 4.G74 /\ F F  ( C38 /\  ( C32 /\ C22 )  )  ) 
Tbox: G G G F F F G F G >= 5.L27 <<  ( C68 /\  ( F F >= 4.G80 /\  ( >= 5.G45 /\ F C63 )  )  ) 
Tbox:  ( !C46 /\  ( >= 3.L93 /\ F F G F C29 )  )  <<  ( G G G  ( >= 4.L1 /\ >= 3.G1 )  /\ F F C16 ) 
Tbox:  ( F  ( >= 2.L13 /\ >= 4.L90 )  /\ G  ( C33 /\ !C82 )  )  <<  ( G !C1 /\  (  ( >= 2.L83 /\ C66 )  /\ F >= 4.G15 )  ) 
Tbox: F  (  ( C47 /\ !C25 )  /\  ( C68 /\ F >= 5.L84 )  )  << G F F  ( F  ( C55 /\ C72 )  /\ !>= 1.L4 ) 
Tbox:  ( F  ( >= 2.L31 /\  ( >= 2.L80 /\ C36 )  )  /\  ( C57 /\ C30 )  )  <<  (  ( F C93 /\ !C50 )  /\  ( >= 2.L5 /\ !>= 2.G14 )  ) 
Tbox: G F  ( F F  ( >= 2.G67 /\ C34 )  /\ G >= 1.G29 )  << F F  ( C66 /\ G F G  ( C46 /\ C46 )  ) 
Tbox:  (  ( >= 5.L55 /\ !>= 5.G78 )  /\  ( F C70 /\ !>= 5.G87 )  )  << G  ( !C25 /\ G  ( C96 /\ F G >= 1.L32 )  ) 
Tbox:  (  ( !>= 1.L97 /\ G G !C32 )  /\ G C54 )  << G G F F  ( G !C32 /\ !>= 1.G21 ) 
Tbox: F  (  ( >= 1.L51 /\  ( C57 /\ >= 1.L54 )  )  /\  ( >= 4.L41 /\ >= 1.L77 )  )  << G G G F G F G  ( >= 5.G63 /\ >= 4.L10 ) 
Tbox:  ( C4 /\  (  ( >= 5.G50 /\ >= 3.G22 )  /\  ( C27 /\ !C46 )  )  )  << G F  ( >= 4.L18 /\  ( G F >= 3.L45 /\ !C15 )  ) 
Tbox:  ( F F G C10 /\ F G F G C71 )  <<  ( F G C21 /\  ( C39 /\ G F !>= 5.G37 )  ) 
Tbox:  (  ( C61 /\ >= 4.G87 )  /\  ( !C75 /\  ( C49 /\ C26 )  )  )  << G F  (  ( >= 1.L86 /\ G !>= 1.L33 )  /\ !C89 ) 
Tbox: F  (  ( G >= 1.L84 /\ F !>= 3.G5 )  /\ !>= 5.G83 )  << F F  ( >= 3.G12 /\ F F G  ( C97 /\ >= 5.L50 )  ) 
Tbox: G  ( >= 1.L66 /\  ( G  ( C22 /\ >= 4.L56 )  /\ F >= 3.L44 )  )  << G F  (  ( >= 2.L40 /\ !C4 )  /\  ( >= 2.L4 /\ >= 5.G94 )  ) 
Tbox:  (  (  ( C56 /\ !C19 )  /\ !C74 )  /\ !>= 1.G59 )  << F  ( G F F !>= 2.L31 /\  ( C1 /\ >= 1.G43 )  ) 
Tbox:  ( !>= 1.G72 /\ F  ( G !>= 3.L64 /\ !C58 )  )  <<  (  ( F >= 3.L97 /\ F >= 5.G4 )  /\ G G F >= 1.G36 ) 
Tbox:  (  ( >= 4.G24 /\ F >= 5.L67 )  /\  ( >= 1.G60 /\ G !C11 )  )  << F G F F  ( C7 /\ F F !C1 ) 
Tbox:  ( G F F F >= 5.G70 /\  ( C1 /\ F >= 2.G12 )  )  << G F  (  ( G >= 1.L11 /\ !C47 )  /\ !C73 ) 
Tbox:  ( C20 /\ G F G G F  ( C98 /\ C53 )  )  <<  ( C29 /\ G F F F G  ( C22 /\ C4 )  ) 
Tbox:  ( F  ( C22 /\ F C66 )  /\ F G !C93 )  << F  ( F F G >= 2.L49 /\ F  ( >= 4.L85 /\ C9 )  ) 
Tbox: F G G  ( !>= 3.G96 /\ F  ( C91 /\ >= 5.L63 )  )  <<  ( F  (  ( C52 /\ C23 )  /\ F C59 )  /\ F C36 ) 
Tbox:  ( G  ( >= 4.G55 /\  ( >= 1.L2 /\ >= 2.L58 )  )  /\ F F >= 1.L91 )  << F G G F  ( C17 /\  ( C49 /\ G >= 3.L98 )  ) 
Tbox:  (  ( F >= 1.G42 /\  ( C23 /\ >= 3.G4 )  )  /\ G F >= 3.L73 )  << F F  ( C42 /\  ( >= 3.L23 /\ F  ( C91 /\ >= 5.G14 )  )  ) 
Tbox: F F  (  ( C63 /\ !>= 3.L5 )  /\  ( >= 4.L56 /\ >= 1.L55 )  )  << G G F  (  ( >= 4.G18 /\ C97 )  /\ F !>= 1.G37 ) 
Tbox: G  ( G F  ( >= 4.L79 /\ C64 )  /\ F !C96 )  <<  ( F F  ( C71 /\ !C58 )  /\ F !>= 2.G56 ) 
Tbox:  ( F >= 5.L12 /\  ( G F F >= 4.L44 /\ !>= 3.G16 )  )  << G G G G  (  ( C44 /\ C79 )  /\ F C71 ) 
Tbox: F G  ( !>= 1.G64 /\ G  ( C97 /\ !>= 2.L88 )  )  << F  ( G F C89 /\ F G G !C4 ) 
Tbox: F G G F  (  ( >= 4.L56 /\ >= 1.L56 )  /\ !>= 1.G98 )  <<  ( F C27 /\  ( F  ( >= 2.G47 /\ >= 3.L30 )  /\ !>= 3.L89 )  ) 
Tbox: G  (  ( >= 1.G40 /\ G  ( >= 1.L87 /\ >= 4.L84 )  )  /\ F >= 3.G52 )  << F G G G F F G  ( C57 /\ >= 3.L70 ) 
Tbox: F G G G F F  ( C82 /\ F C17 )  <<  (  ( C76 /\  ( C12 /\ !>= 4.G29 )  )  /\  ( C53 /\ C60 )  ) 
Tbox:  (  ( C11 /\  ( C3 /\  ( C39 /\ >= 3.G39 )  )  )  /\ !>= 4.L78 )  << F  ( >= 5.G77 /\ G  ( >= 5.L29 /\ F F !>= 1.G19 )  ) 
Tbox:  (  ( >= 2.L77 /\ !>= 3.G66 )  /\  ( >= 1.L26 /\  ( >= 4.G99 /\ C83 )  )  )  << G  ( >= 1.G17 /\ G  ( F C22 /\  ( C23 /\ C68 )  )  ) 
Tbox: F  ( >= 3.L27 /\  (  ( C97 /\ C91 )  /\ G !>= 2.G64 )  )  << G  ( G F C38 /\  ( >= 5.G27 /\  ( C44 /\ C79 )  )  ) 
Tbox: F F G  ( C86 /\  ( >= 3.G29 /\  ( C39 /\ >= 2.G19 )  )  )  <<  (  ( !C74 /\ F !C79 )  /\ G !C63 ) 
Tbox:  ( G C51 /\ F F F F  ( C91 /\ >= 5.L68 )  )  <<  ( G G G !>= 1.L25 /\ G G !C88 ) 
Tbox: F  ( F  ( >= 3.L95 /\ >= 5.G92 )  /\  ( C29 /\ !>= 5.L81 )  )  <<  ( G  ( C86 /\ C16 )  /\  ( !C35 /\ !C82 )  ) 
Tbox: F G  ( G C34 /\ G F G !C1 )  <<  ( F G  ( F C10 /\ !C95 )  /\ !>= 2.G96 ) 
Tbox:  ( F F !C74 /\  ( >= 1.G19 /\  ( C65 /\ >= 3.L57 )  )  )  << G  (  ( G F >= 4.G0 /\ !>= 5.G29 )  /\ !>= 4.L5 ) 
TBox -> Qtl1
Num of Propositions: 135000
Generating NuSMV file...
Solverpltl
Generating FO file...
Done! Total time:6087ms