Tbox:  ( F  ( !C27 /\ H >= 5.G26 )  /\ F O >= 1.L29 )  <<  ( C13 /\ O  ( O H C3 /\  ( >= 1.L22 /\ >= 4.G14 )  )  ) 
Tbox:  (  ( G H >= 3.L3 /\ G C5 )  /\  ( C17 /\ C10 )  )  <<  ( O !C24 /\ O O  ( >= 5.L17 /\ !C24 )  ) 
Tbox: G O O G  ( >= 2.L5 /\ O  ( C18 /\ C3 )  )  <<  ( G !>= 5.G10 /\  ( !>= 4.L0 /\ O O C23 )  ) 
Tbox:  ( H C3 /\ F F O  ( C4 /\ !C26 )  )  << O  ( !C9 /\ O  ( C19 /\ H !C27 )  ) 
Tbox: H G F H F F  ( >= 1.L29 /\ O C1 )  <<  (  ( >= 3.L3 /\ H G C23 )  /\ H  ( >= 4.L17 /\ >= 4.L28 )  ) 
Tbox: F  ( O !C26 /\  ( F >= 3.G12 /\ O C25 )  )  <<  ( F O F C10 /\  ( G >= 4.L20 /\ !C20 )  ) 
Tbox: G  ( >= 2.L19 /\  ( !C14 /\  ( C11 /\ O >= 3.L0 )  )  )  << F O  (  ( !C17 /\ !>= 1.G2 )  /\ !>= 5.G10 ) 
Tbox:  ( F !>= 3.L0 /\  ( >= 4.L11 /\  ( C23 /\ O C25 )  )  )  << H O  ( H O G >= 4.L21 /\  ( C8 /\ C20 )  ) 
Tbox:  (  ( !C6 /\ !>= 3.G14 )  /\ F  ( C25 /\ >= 3.L21 )  )  <<  (  ( !>= 5.G27 /\ G C6 )  /\  ( >= 3.L24 /\ H >= 2.G20 )  ) 
Tbox: G O  ( O !C10 /\  ( >= 3.G23 /\ G >= 4.G18 )  )  << G G  ( !C2 /\  ( G C8 /\ !>= 2.G28 )  ) 
Tbox: G O G H  ( H C18 /\  ( C3 /\ >= 2.G11 )  )  <<  (  ( C19 /\ !>= 2.G11 )  /\ H H  ( C10 /\ C19 )  ) 
Tbox: G F F  ( C28 /\  ( H >= 4.G13 /\ O >= 3.L28 )  )  <<  (  ( !>= 5.G25 /\  ( >= 4.L26 /\ >= 2.L8 )  )  /\ G G C22 ) 
Tbox: G  (  ( C16 /\ C14 )  /\ O O H !C24 )  <<  (  ( C15 /\ >= 1.G4 )  /\  ( O F >= 1.G26 /\ F >= 5.L28 )  ) 
Tbox:  ( F !C28 /\ F H  ( >= 4.G1 /\ !>= 4.L25 )  )  << F G F  (  ( C28 /\ >= 1.G9 )  /\  ( >= 5.G7 /\ C0 )  ) 
Tbox:  ( H F F G !C20 /\ O F >= 2.L23 )  << O  (  ( >= 1.L13 /\ >= 1.G5 )  /\ O O H G C4 ) 
Tbox: G  ( H >= 2.L2 /\ F H O G O C15 )  << H H  (  ( C20 /\ C20 )  /\ O O G >= 1.G14 ) 
Tbox: G F  ( !C16 /\  ( C12 /\ H G C15 )  )  << H  ( F O O  ( C18 /\ C3 )  /\ !C27 ) 
Tbox: H G  ( !C10 /\  ( F C1 /\ !C2 )  )  <<  ( F H  ( >= 1.L9 /\ C12 )  /\  ( >= 3.G19 /\ !>= 5.G28 )  ) 
Tbox: O  (  ( C3 /\ G !C0 )  /\ O !C8 )  << G  ( G H !>= 2.L3 /\ O  ( >= 1.G26 /\ C22 )  ) 
Tbox:  (  ( H F !>= 3.G13 /\ !>= 2.G0 )  /\ H >= 2.L6 )  << F  ( G H G >= 3.L5 /\  ( >= 2.G0 /\ O >= 2.L27 )  ) 
Tbox:  ( G H H O !>= 2.L2 /\ F !C26 )  <<  ( F C15 /\ O  ( F C28 /\  ( >= 1.G18 /\ C6 )  )  ) 
Tbox: H  ( H C22 /\  ( O C25 /\  ( >= 1.L3 /\ C21 )  )  )  <<  ( F  ( C26 /\ >= 1.G9 )  /\ H  ( >= 3.G5 /\ H C8 )  ) 
Tbox: H G  ( F  ( C20 /\ G >= 2.L23 )  /\ O >= 4.L3 )  << H  ( >= 3.G15 /\ H  ( F H C20 /\ !C17 )  ) 
Tbox: G  ( !C5 /\  ( C6 /\ F  ( >= 3.L9 /\ >= 3.G25 )  )  )  <<  (  ( F !>= 4.G28 /\ !C2 )  /\ F !>= 5.G18 ) 
Tbox:  ( C1 /\  ( !>= 1.G18 /\  ( !C1 /\ !C21 )  )  )  << H  ( H O H H >= 3.L20 /\  ( C23 /\ C20 )  ) 
Tbox:  ( C23 /\  ( >= 5.G2 /\  ( H G C3 /\ H >= 2.G14 )  )  )  << F  ( G O H !>= 1.L23 /\  ( C2 /\ C7 )  ) 
Tbox: H H  ( H O C6 /\ F  ( >= 1.G19 /\ >= 4.G12 )  )  << H  ( G G G O >= 4.L19 /\  ( >= 2.L0 /\ C8 )  ) 
Tbox: F  ( G H O !C9 /\ F F >= 3.G10 )  << G  ( C24 /\ H H  ( C3 /\ G O >= 3.G14 )  ) 
Tbox:  (  ( O C3 /\  ( >= 4.L9 /\ C28 )  )  /\  ( C16 /\ >= 1.G16 )  )  << O G H  ( !>= 3.G2 /\ G G !>= 1.L22 ) 
Tbox:  ( H  ( !>= 5.L9 /\ O >= 3.L18 )  /\ F !>= 2.L12 )  <<  (  ( >= 5.L19 /\ >= 1.G6 )  /\ O F  ( C3 /\ F >= 3.G24 )  ) 
Tbox: F F  ( H O >= 3.L7 /\ O F O >= 2.L20 )  <<  ( G G F  ( >= 5.L8 /\ >= 4.G0 )  /\ G H >= 5.G9 ) 
Tbox:  (  ( F F C7 /\ !C18 )  /\ O O C8 )  << F G H F  (  ( C24 /\ >= 1.L26 )  /\ !>= 2.L14 ) 
Tbox: O F  ( >= 3.L19 /\  ( !C20 /\ H !>= 4.G11 )  )  <<  ( H  ( >= 1.G26 /\ H G >= 5.L14 )  /\ O !>= 2.G21 ) 
Tbox: G O F O  ( !>= 5.L15 /\ G F C13 )  << G  ( >= 3.G15 /\ F  ( C20 /\  ( C15 /\ O >= 5.L18 )  )  ) 
Tbox:  ( G  ( H C9 /\ O >= 5.L2 )  /\  ( >= 4.L10 /\ C2 )  )  <<  ( F >= 4.G22 /\ O H O  ( C1 /\ !C26 )  ) 
Generating model LTL file...
Num of Propositions: 179988
Solver...NuSMV
SolverAalta
Solverpltl
SolverTRP++UC
Generating FO file...
Done! Total time:12676ms