Tbox: F G  ( G G C76 /\ F F F C34 )  << F F G F F F  ( C52 /\ F C68 ) 
Tbox: F F F G G G G F F C91 << G F F G F G G G F >= 5.G1
Tbox: F  ( F C51 /\ G G F F G >= 1.L80 )  << G F G G G F G  ( >= 2.G95 /\ C83 ) 
Tbox: F F F G G G  ( C33 /\ G >= 5.G64 )  << F G  ( C16 /\ G G  ( >= 1.G59 /\ G >= 2.G18 )  ) 
Tbox: G F G F F F F G F C79 << F F F F  ( !>= 1.L70 /\ G F C96 ) 
Tbox:  ( F G F F F C99 /\  ( >= 3.G49 /\ C21 )  )  << G G F F G G G F F C19
Tbox: G F F F G F G F F C17 <<  ( G >= 2.G50 /\ G G F F G G >= 5.G18 ) 
Tbox:  ( G G C1 /\  (  ( C54 /\ C69 )  /\ !C30 )  )  << F F G F F G  ( C79 /\ G >= 3.G22 ) 
Tbox: G  ( G G >= 5.L82 /\ F F  ( >= 3.G12 /\ C42 )  )  << G  ( G G F G F C34 /\ !>= 1.G73 ) 
Tbox: F G G F G F  ( C65 /\ G C44 )  << G F  ( F F C60 /\ F F G C20 ) 
Tbox:  (  ( F >= 3.G66 /\ F F C90 )  /\  ( C67 /\ C63 )  )  << G G  ( F C97 /\ G G F F C31 ) 
Tbox: F F F  ( G >= 3.L15 /\  ( C57 /\ G >= 1.G78 )  )  << F G G  ( G F >= 2.G71 /\ G F C26 ) 
Tbox: F  ( G G G F C0 /\ G G >= 3.G27 )  << G G G F F G G G G >= 5.L36
Tbox: G F  (  ( C33 /\ >= 5.G43 )  /\ G F F C92 )  << G F G F F G G F F >= 5.G16
Tbox: F F G G G  ( G C37 /\ F C18 )  << G G G G F F G F G >= 4.L97
Tbox: F G  ( G C95 /\ G G G G C99 )  << G G F F  ( G C55 /\ G F >= 3.G51 ) 
Tbox: G F F G G G  ( C68 /\ G >= 5.G97 )  << G G F F G F  ( >= 3.G96 /\ G C89 ) 
Tbox: G F G G G G G F F C85 << F F G F F G  ( >= 1.G39 /\ G >= 3.G57 ) 
Tbox:  ( F G C98 /\  ( F G C38 /\ F C1 )  )  << G F G G G F G F G C37
Tbox: G G G G G  ( F C53 /\ F >= 3.G82 )  << G F F F F G F G F C58
Tbox: F G G G F F F  ( C51 /\ >= 4.G76 )  << G F F G F G G F G >= 5.G4
Tbox: G G G F G G G G G C34 << F F F G G G G G !>= 5.G26
Tbox: G G F  ( C72 /\ F G G G >= 4.L53 )  << F F G G F G F G G >= 2.G73
Tbox: F F F G G F  ( C8 /\ G C74 )  <<  ( F F >= 1.G29 /\ F G G F G C63 ) 
Tbox: F F G G F G F G !C9 << F G F G  ( G C13 /\ G G C65 ) 
Tbox: G F G F  ( G >= 2.G70 /\  ( C79 /\ C4 )  )  << G F G F F G G G F >= 4.G9
Tbox: G F F F G  ( >= 4.G33 /\ G G C14 )  << F F G G G F G G F >= 3.G44
Tbox: F G G  ( G >= 1.G30 /\ F G G >= 3.G56 )  << G G G G F G G G G C81
Tbox: F G G F  ( G !>= 1.G70 /\ F C76 )  << F F  ( F  ( >= 5.L68 /\ G >= 5.G12 )  /\ G >= 3.G71 ) 
Tbox: F G G F F F F G G >= 2.G97 << G F G F F  ( C68 /\ F F >= 5.G63 ) 
Tbox:  ( F >= 3.L69 /\ G G G G F F >= 4.G79 )  << G F G  ( >= 4.G42 /\ G F F G >= 1.L81 ) 
Tbox: G G G F G G G G F >= 1.G0 << G  ( G G >= 2.G68 /\ F G G F >= 4.G35 ) 
Tbox: F F F G G G G G G >= 2.G43 << G G G G F F F G G >= 2.G2
Tbox: G G G G  ( F G C5 /\ G C95 )  << F  ( F F F G >= 3.G58 /\ G F >= 2.G59 ) 
Tbox: F  (  ( C71 /\ G C94 )  /\ G G G C54 )  << F G F F G G F G G C57
Tbox: G F F F G G G G G >= 5.G37 << F F G F F  ( G >= 5.G67 /\ G >= 1.G99 ) 
Tbox:  ( G F F >= 1.G39 /\ G F G !>= 2.G50 )  << G  ( G F F G >= 1.L98 /\ G F C70 ) 
Tbox: G F F G F F F  ( >= 2.G53 /\ C29 )  << G G F G G F F F F C36
Tbox: G F G G G  ( >= 4.G83 /\ G !>= 3.G5 )  <<  ( F G F  ( >= 3.G51 /\ G >= 2.G79 )  /\ F >= 3.G94 ) 
Tbox: G F G G G G G G F >= 4.G70 << G F  ( F G >= 5.G59 /\ G G F >= 4.G98 ) 
Tbox: G F G  ( >= 5.G73 /\ G G  ( >= 2.G9 /\ >= 3.G12 )  )  << F  ( F G >= 4.G8 /\ F F F F >= 1.G29 ) 
Tbox: F F F G  ( F F >= 2.G36 /\ F >= 4.L17 )  << G F F F G F G F F C63
Tbox: F F G G  (  ( C67 /\ C40 )  /\ G C29 )  << F G F F F G G G !C22
Tbox: F G  ( G C8 /\ F F G G >= 4.G82 )  << F G F G F G  ( >= 3.G23 /\ F >= 1.G65 ) 
Tbox: G G G  ( !C57 /\ G F F C74 )  << G F  ( G G F G >= 1.G42 /\ F C84 ) 
Tbox: F F F F G  ( C56 /\ F F >= 2.G1 )  << F G G G G  ( F >= 4.G35 /\ !C29 ) 
Tbox: F G G F G F G G G >= 1.G15 <<  (  ( >= 3.G1 /\ C87 )  /\ G F F F F C0 ) 
Tbox: F F F G F  ( C60 /\ G G >= 3.G71 )  << F F G F F G F F F >= 2.G80
Tbox: F F F  ( G F >= 3.L76 /\  ( >= 2.L88 /\ >= 4.G54 )  )  << G G F F G G G G G >= 3.G47
Tbox: G G F F G G F G F C12 << G G F F G G G F F C56
Tbox: F  ( C7 /\ F F F G  ( C87 /\ >= 1.G81 )  )  << G F  ( C33 /\ G G G F F >= 1.G88 ) 
Tbox: F F F G G F F F !C23 << G G F F G G F F F C43
Tbox: F G G F F F  ( >= 3.G66 /\ G >= 5.G58 )  << G F G  ( >= 2.G45 /\ G G G G >= 4.G17 ) 
Tbox: G F G F F F F F F >= 5.G16 <<  ( G C1 /\ G G G F G !C72 ) 
Tbox: F F G G G G G G !>= 1.G50 << G G F G G F G  ( >= 4.G65 /\ >= 2.G86 ) 
Tbox: F G G G G G G G F >= 5.G48 << F F F F F G G G F >= 1.G32
Tbox: F G F G F F G F F >= 4.G37 << G F  ( F G >= 3.G52 /\ F G F >= 3.G50 ) 
Tbox: F F F G F F F G G C86 << G F G F G G F F G C14
Tbox:  ( G G F G C19 /\ F  ( >= 5.L50 /\ C2 )  )  << F G G  ( >= 4.G72 /\ G F F G C83 ) 
Tbox: G F G F G G G F F C30 << F F G G  ( G G >= 5.G82 /\ G >= 5.G64 ) 
TBox -> Qtl1
Qrole:>= 1.G99
Qrole1:>= 1.G99
Qrole:>= 1.G15
Qrole1:>= 1.G15
Qrole:>= 3.G23
Qrole1:>= 1.G23
Qrole:>= 5.L50
Qrole1:>= 1.L50
Qrole:>= 3.G22
Qrole1:>= 1.G22
Qrole:>= 5.G37
Qrole1:>= 1.G37
Qrole:>= 2.G50
Qrole1:>= 1.G50
Qrole:>= 3.G27
Qrole1:>= 1.G27
Qrole:>= 2.G59
Qrole1:>= 1.G59
Qrole:>= 4.G65
Qrole1:>= 1.G65
Qrole:>= 2.G53
Qrole1:>= 1.G53
Qrole:>= 3.G94
Qrole1:>= 1.G94
Qrole:>= 3.G12
Qrole1:>= 1.G12
Qrole:>= 5.G43
Qrole1:>= 1.G43
Qrole:>= 3.G96
Qrole1:>= 1.G96
Qrole:>= 5.G48
Qrole1:>= 1.G48
Qrole:>= 5.L68
Qrole1:>= 1.L68
Qrole:>= 1.G29
Qrole1:>= 1.G29
Qrole:>= 4.G9
Qrole1:>= 1.G9
Qrole:>= 4.G8
Qrole1:>= 1.G8
Qrole:>= 2.L88
Qrole1:>= 1.L88
Qrole:>= 4.G54
Qrole1:>= 1.G54
Qrole:>= 2.G68
Qrole1:>= 1.G68
Qrole:>= 3.G82
Qrole1:>= 1.G82
Qrole:>= 1.G78
Qrole1:>= 1.G78
Qrole:>= 1.L98
Qrole1:>= 1.L98
Qrole:>= 1.G70
Qrole1:>= 1.G70
Qrole:>= 1.G73
Qrole1:>= 1.G73
Qrole:>= 5.G58
Qrole1:>= 1.G58
Qrole:>= 5.G1
Qrole1:>= 1.G1
Qrole:>= 5.G59
Qrole1:>= 1.G59
Qrole:>= 5.G4
Qrole1:>= 1.G4
Qrole:>= 4.G42
Qrole1:>= 1.G42
Qrole:>= 2.G36
Qrole1:>= 1.G36
Qrole:>= 3.G71
Qrole1:>= 1.G71
Qrole:>= 1.G88
Qrole1:>= 1.G88
Qrole:>= 4.G37
Qrole1:>= 1.G37
Qrole:>= 5.G63
Qrole1:>= 1.G63
Qrole:>= 1.G81
Qrole1:>= 1.G81
Qrole:>= 5.G64
Qrole1:>= 1.G64
Qrole:>= 5.L82
Qrole1:>= 1.L82
Qrole:>= 5.G67
Qrole1:>= 1.G67
Qrole:>= 3.L15
Qrole1:>= 1.L15
Qrole:>= 2.G1
Qrole1:>= 1.G1
Qrole:>= 2.G9
Qrole1:>= 1.G9
Qrole:>= 4.G35
Qrole1:>= 1.G35
Qrole:>= 2.G2
Qrole1:>= 1.G2
Qrole:>= 4.L53
Qrole1:>= 1.L53
Qrole:>= 2.G45
Qrole1:>= 1.G45
Qrole:>= 4.G33
Qrole1:>= 1.G33
Qrole:>= 2.G43
Qrole1:>= 1.G43
Qrole:>= 1.G59
Qrole1:>= 1.G59
Qrole:>= 2.G18
Qrole1:>= 1.G18
Qrole:>= 5.G73
Qrole1:>= 1.G73
Qrole:>= 1.G50
Qrole1:>= 1.G50
Qrole:>= 1.L70
Qrole1:>= 1.L70
Qrole:>= 3.G66
Qrole1:>= 1.G66
Qrole:>= 2.G95
Qrole1:>= 1.G95
Qrole:>= 3.G1
Qrole1:>= 1.G1
Qrole:>= 2.G97
Qrole1:>= 1.G97
Qrole:>= 3.G5
Qrole1:>= 1.G5
Qrole:>= 1.G65
Qrole1:>= 1.G65
Qrole:>= 4.G17
Qrole1:>= 1.G17
Qrole:>= 3.G50
Qrole1:>= 1.G50
Qrole:>= 3.G51
Qrole1:>= 1.G51
Qrole:>= 5.G82
Qrole1:>= 1.G82
Qrole:>= 3.G56
Qrole1:>= 1.G56
Qrole:>= 3.G57
Qrole1:>= 1.G57
Qrole:>= 3.G58
Qrole1:>= 1.G58
Qrole:>= 3.L76
Qrole1:>= 1.L76
Qrole:>= 3.G52
Qrole1:>= 1.G52
Qrole:>= 1.L80
Qrole1:>= 1.L80
Qrole:>= 1.L81
Qrole1:>= 1.L81
Qrole:>= 4.G98
Qrole1:>= 1.G98
Qrole:>= 1.G32
Qrole1:>= 1.G32
Qrole:>= 1.G39
Qrole1:>= 1.G39
Qrole:>= 3.G47
Qrole1:>= 1.G47
Qrole:>= 5.G97
Qrole1:>= 1.G97
Qrole:>= 1.G30
Qrole1:>= 1.G30
Qrole:>= 5.G12
Qrole1:>= 1.G12
Qrole:>= 3.G44
Qrole1:>= 1.G44
Qrole:>= 2.G73
Qrole1:>= 1.G73
Qrole:>= 2.G71
Qrole1:>= 1.G71
Qrole:>= 5.G16
Qrole1:>= 1.G16
Qrole:>= 3.G49
Qrole1:>= 1.G49
Qrole:>= 5.G18
Qrole1:>= 1.G18
Qrole:>= 1.G0
Qrole1:>= 1.G0
Qrole:>= 4.G82
Qrole1:>= 1.G82
Qrole:>= 5.L36
Qrole1:>= 1.L36
Qrole:>= 2.G70
Qrole1:>= 1.G70
Qrole:>= 4.G83
Qrole1:>= 1.G83
Qrole:>= 3.L69
Qrole1:>= 1.L69
Qrole:>= 2.G79
Qrole1:>= 1.G79
Qrole:>= 4.L17
Qrole1:>= 1.L17
Qrole:>= 1.G42
Qrole1:>= 1.G42
Qrole:>= 5.G26
Qrole1:>= 1.G26
Qrole:>= 2.G80
Qrole1:>= 1.G80
Qrole:>= 4.G72
Qrole1:>= 1.G72
Qrole:>= 4.G70
Qrole1:>= 1.G70
Qrole:>= 4.G76
Qrole1:>= 1.G76
Qrole:>= 4.G79
Qrole1:>= 1.G79
Qrole:>= 4.L97
Qrole1:>= 1.L97
Qrole:>= 2.G86
Qrole1:>= 1.G86
Num of Propositions: 49920
Generating NuSMV file...
Solverpltl
Generating FO file...
Done! Total time:2343ms