You are not logged in. login register
Game uf20-010.cnf.SAT
name uf20-010.cnf.SAT
creator hannes
number of roles 1
stylesheet sat/sat.xsl
GDL v1
enabled
matches show matches
statistics show game statistics
description

Game Description

(contains 1 (neg 11))
(contains 1 9)
(contains 1 12)
(contains 2 (neg 7))
(contains 2 (neg 17))
(contains 2 (neg 18))
(contains 3 (neg 13))
(contains 3 (neg 17))
(contains 3 20)
(contains 4 (neg 4))
(contains 4 (neg 16))
(contains 4 12)
(contains 5 8)
(contains 5 2)
(contains 5 14)
(contains 6 (neg 9))
(contains 6 (neg 19))
(contains 6 14)
(contains 7 7)
(contains 7 4)
(contains 7 18)
(contains 8 (neg 19))
(contains 8 (neg 16))
(contains 8 5)
(contains 9 (neg 1))
(contains 9 (neg 16))
(contains 9 17)
(contains 10 (neg 2))
(contains 10 20)
(contains 10 (neg 11))
(contains 11 (neg 20))
(contains 11 9)
(contains 11 (neg 17))
(contains 12 (neg 14))
(contains 12 (neg 15))
(contains 12 (neg 17))
(contains 13 19)
(contains 13 (neg 18))
(contains 13 15)
(contains 14 6)
(contains 14 15)
(contains 14 (neg 2))
(contains 15 12)
(contains 15 8)
(contains 15 (neg 14))
(contains 16 (neg 1))
(contains 16 (neg 2))
(contains 16 (neg 3))
(contains 17 11)
(contains 17 (neg 8))
(contains 17 5)
(contains 18 6)
(contains 18 18)
(contains 18 (neg 1))
(contains 19 7)
(contains 19 (neg 11))
(contains 19 8)
(contains 20 1)
(contains 20 5)
(contains 20 15)
(contains 21 4)
(contains 21 10)
(contains 21 12)
(contains 22 11)
(contains 22 6)
(contains 22 18)
(contains 23 7)
(contains 23 10)
(contains 23 3)
(contains 24 14)
(contains 24 (neg 16))
(contains 24 (neg 17))
(contains 25 4)
(contains 25 18)
(contains 25 13)
(contains 26 (neg 11))
(contains 26 (neg 15))
(contains 26 (neg 13))
(contains 27 (neg 2))
(contains 27 (neg 9))
(contains 27 20)
(contains 28 2)
(contains 28 (neg 5))
(contains 28 19)
(contains 29 14)
(contains 29 6)
(contains 29 (neg 19))
(contains 30 (neg 8))
(contains 30 (neg 13))
(contains 30 20)
(contains 31 (neg 9))
(contains 31 8)
(contains 31 13)
(contains 32 2)
(contains 32 (neg 14))
(contains 32 (neg 7))
(contains 33 3)
(contains 33 16)
(contains 33 (neg 15))
(contains 34 (neg 2))
(contains 34 13)
(contains 34 17)
(contains 35 (neg 18))
(contains 35 (neg 13))
(contains 35 16)
(contains 36 (neg 18))
(contains 36 1)
(contains 36 (neg 16))
(contains 37 18)
(contains 37 2)
(contains 37 14)
(contains 38 (neg 20))
(contains 38 6)
(contains 38 (neg 14))
(contains 39 15)
(contains 39 (neg 19))
(contains 39 (neg 8))
(contains 40 4)
(contains 40 12)
(contains 40 (neg 11))
(contains 41 19)
(contains 41 3)
(contains 41 (neg 14))
(contains 42 6)
(contains 42 5)
(contains 42 (neg 7))
(contains 43 10)
(contains 43 13)
(contains 43 (neg 11))
(contains 44 15)
(contains 44 (neg 1))
(contains 44 (neg 3))
(contains 45 9)
(contains 45 6)
(contains 45 10)
(contains 46 (neg 11))
(contains 46 (neg 1))
(contains 46 16)
(contains 47 18)
(contains 47 (neg 1))
(contains 47 12)
(contains 48 18)
(contains 48 (neg 2))
(contains 48 (neg 4))
(contains 49 5)
(contains 49 13)
(contains 49 (neg 20))
(contains 50 19)
(contains 50 (neg 12))
(contains 50 (neg 6))
(contains 51 15)
(contains 51 11)
(contains 51 13)
(contains 52 12)
(contains 52 2)
(contains 52 (neg 7))
(contains 53 3)
(contains 53 5)
(contains 53 (neg 19))
(contains 54 3)
(contains 54 13)
(contains 54 (neg 10))
(contains 55 1)
(contains 55 8)
(contains 55 (neg 6))
(contains 56 (neg 2))
(contains 56 18)
(contains 56 (neg 11))
(contains 57 (neg 3))
(contains 57 6)
(contains 57 (neg 9))
(contains 58 (neg 18))
(contains 58 (neg 14))
(contains 58 (neg 3))
(contains 59 (neg 4))
(contains 59 (neg 19))
(contains 59 (neg 17))
(contains 60 7)
(contains 60 5)
(contains 60 (neg 14))
(contains 61 13)
(contains 61 19)
(contains 61 (neg 12))
(contains 62 (neg 12))
(contains 62 (neg 7))
(contains 62 (neg 3))
(contains 63 9)
(contains 63 7)
(contains 63 (neg 19))
(contains 64 6)
(contains 64 2)
(contains 64 10)
(contains 65 11)
(contains 65 6)
(contains 65 (neg 12))
(contains 66 15)
(contains 66 1)
(contains 66 (neg 17))
(contains 67 20)
(contains 67 (neg 1))
(contains 67 (neg 4))
(contains 68 (neg 18))
(contains 68 1)
(contains 68 5)
(contains 69 9)
(contains 69 18)
(contains 69 14)
(contains 70 15)
(contains 70 (neg 17))
(contains 70 9)
(contains 71 (neg 3))
(contains 71 11)
(contains 71 9)
(contains 72 14)
(contains 72 12)
(contains 72 9)
(contains 73 5)
(contains 73 14)
(contains 73 2)
(contains 74 17)
(contains 74 (neg 10))
(contains 74 (neg 8))
(contains 75 14)
(contains 75 (neg 15))
(contains 75 9)
(contains 76 (neg 6))
(contains 76 (neg 20))
(contains 76 13)
(contains 77 1)
(contains 77 6)
(contains 77 13)
(contains 78 (neg 16))
(contains 78 15)
(contains 78 (neg 17))
(contains 79 (neg 8))
(contains 79 19)
(contains 79 7)
(contains 80 (neg 7))
(contains 80 3)
(contains 80 (neg 1))
(contains 81 (neg 18))
(contains 81 10)
(contains 81 17)
(contains 82 12)
(contains 82 (neg 4))
(contains 82 14)
(contains 83 7)
(contains 83 10)
(contains 83 19)
(contains 84 20)
(contains 84 15)
(contains 84 19)
(contains 85 (neg 13))
(contains 85 (neg 17))
(contains 85 (neg 9))
(contains 86 10)
(contains 86 (neg 9))
(contains 86 3)
(contains 87 15)
(contains 87 (neg 11))
(contains 87 10)
(contains 88 12)
(contains 88 1)
(contains 88 (neg 13))
(contains 89 11)
(contains 89 3)
(contains 89 15)
(contains 90 16)
(contains 90 (neg 2))
(contains 90 (neg 1))
(contains 91 (neg 17))
(contains 91 (neg 5))
(contains 91 (neg 1))
(prop_var 1)
(prop_var 2)
(prop_var 3)
(prop_var 4)
(prop_var 5)
(prop_var 6)
(prop_var 7)
(prop_var 8)
(prop_var 9)
(prop_var 10)
(prop_var 11)
(prop_var 12)
(prop_var 13)
(prop_var 14)
(prop_var 15)
(prop_var 16)
(prop_var 17)
(prop_var 18)
(prop_var 19)
(prop_var 20)
(clause 1)
(clause 2)
(clause 3)
(clause 4)
(clause 5)
(clause 6)
(clause 7)
(clause 8)
(clause 9)
(clause 10)
(clause 11)
(clause 12)
(clause 13)
(clause 14)
(clause 15)
(clause 16)
(clause 17)
(clause 18)
(clause 19)
(clause 20)
(clause 21)
(clause 22)
(clause 23)
(clause 24)
(clause 25)
(clause 26)
(clause 27)
(clause 28)
(clause 29)
(clause 30)
(clause 31)
(clause 32)
(clause 33)
(clause 34)
(clause 35)
(clause 36)
(clause 37)
(clause 38)
(clause 39)
(clause 40)
(clause 41)
(clause 42)
(clause 43)
(clause 44)
(clause 45)
(clause 46)
(clause 47)
(clause 48)
(clause 49)
(clause 50)
(clause 51)
(clause 52)
(clause 53)
(clause 54)
(clause 55)
(clause 56)
(clause 57)
(clause 58)
(clause 59)
(clause 60)
(clause 61)
(clause 62)
(clause 63)
(clause 64)
(clause 65)
(clause 66)
(clause 67)
(clause 68)
(clause 69)
(clause 70)
(clause 71)
(clause 72)
(clause 73)
(clause 74)
(clause 75)
(clause 76)
(clause 77)
(clause 78)
(clause 79)
(clause 80)
(clause 81)
(clause 82)
(clause 83)
(clause 84)
(clause 85)
(clause 86)
(clause 87)
(clause 88)
(clause 89)
(clause 90)
(clause 91)
(role exists)
(truth_value t)
(truth_value f)
(init (control exists 1))
(<= (legal ?v80866 (assign ?v80871 ?v80872)) (true (control ?v80866 ?v80871)) (role ?v80866) (prop_var ?v80871) (truth_value ?v80872))
(<= (next (sat ?v80902)) (true (sat ?v80902)) (clause ?v80902))
(<= (next (control exists 2)) (true (control exists 1)))
(<= (next (control exists 3)) (true (control exists 2)))
(<= (next (control exists 4)) (true (control exists 3)))
(<= (next (control exists 5)) (true (control exists 4)))
(<= (next (control exists 6)) (true (control exists 5)))
(<= (next (control exists 7)) (true (control exists 6)))
(<= (next (control exists 8)) (true (control exists 7)))
(<= (next (control exists 9)) (true (control exists 8)))
(<= (next (control exists 10)) (true (control exists 9)))
(<= (next (control exists 11)) (true (control exists 10)))
(<= (next (control exists 12)) (true (control exists 11)))
(<= (next (control exists 13)) (true (control exists 12)))
(<= (next (control exists 14)) (true (control exists 13)))
(<= (next (control exists 15)) (true (control exists 14)))
(<= (next (control exists 16)) (true (control exists 15)))
(<= (next (control exists 17)) (true (control exists 16)))
(<= (next (control exists 18)) (true (control exists 17)))
(<= (next (control exists 19)) (true (control exists 18)))
(<= (next (control exists 20)) (true (control exists 19)))
(<= (next (control the end)) (true (control exists 20)))
(<= (next (sat 1)) (does ?v81720 (assign 11 f)) (role ?v81720))
(<= (next (sat 1)) (does ?v81741 (assign 9 t)) (role ?v81741))
(<= (next (sat 1)) (does ?v81762 (assign 12 t)) (role ?v81762))
(<= (next (sat 2)) (does ?v81785 (assign 7 f)) (role ?v81785))
(<= (next (sat 2)) (does ?v81806 (assign 17 f)) (role ?v81806))
(<= (next (sat 2)) (does ?v81827 (assign 18 f)) (role ?v81827))
(<= (next (sat 3)) (does ?v81850 (assign 13 f)) (role ?v81850))
(<= (next (sat 3)) (does ?v81871 (assign 17 f)) (role ?v81871))
(<= (next (sat 3)) (does ?v81892 (assign 20 t)) (role ?v81892))
(<= (next (sat 4)) (does ?v81915 (assign 4 f)) (role ?v81915))
(<= (next (sat 4)) (does ?v81936 (assign 16 f)) (role ?v81936))
(<= (next (sat 4)) (does ?v81957 (assign 12 t)) (role ?v81957))
(<= (next (sat 5)) (does ?v81980 (assign 8 t)) (role ?v81980))
(<= (next (sat 5)) (does ?v82001 (assign 2 t)) (role ?v82001))
(<= (next (sat 5)) (does ?v82022 (assign 14 t)) (role ?v82022))
(<= (next (sat 6)) (does ?v82045 (assign 9 f)) (role ?v82045))
(<= (next (sat 6)) (does ?v82066 (assign 19 f)) (role ?v82066))
(<= (next (sat 6)) (does ?v82087 (assign 14 t)) (role ?v82087))
(<= (next (sat 7)) (does ?v82110 (assign 7 t)) (role ?v82110))
(<= (next (sat 7)) (does ?v82131 (assign 4 t)) (role ?v82131))
(<= (next (sat 7)) (does ?v82152 (assign 18 t)) (role ?v82152))
(<= (next (sat 8)) (does ?v82175 (assign 19 f)) (role ?v82175))
(<= (next (sat 8)) (does ?v82196 (assign 16 f)) (role ?v82196))
(<= (next (sat 8)) (does ?v82217 (assign 5 t)) (role ?v82217))
(<= (next (sat 9)) (does ?v82240 (assign 1 f)) (role ?v82240))
(<= (next (sat 9)) (does ?v82261 (assign 16 f)) (role ?v82261))
(<= (next (sat 9)) (does ?v82282 (assign 17 t)) (role ?v82282))
(<= (next (sat 10)) (does ?v82305 (assign 2 f)) (role ?v82305))
(<= (next (sat 10)) (does ?v82326 (assign 20 t)) (role ?v82326))
(<= (next (sat 10)) (does ?v82347 (assign 11 f)) (role ?v82347))
(<= (next (sat 11)) (does ?v82370 (assign 20 f)) (role ?v82370))
(<= (next (sat 11)) (does ?v82391 (assign 9 t)) (role ?v82391))
(<= (next (sat 11)) (does ?v82412 (assign 17 f)) (role ?v82412))
(<= (next (sat 12)) (does ?v82435 (assign 14 f)) (role ?v82435))
(<= (next (sat 12)) (does ?v82456 (assign 15 f)) (role ?v82456))
(<= (next (sat 12)) (does ?v82477 (assign 17 f)) (role ?v82477))
(<= (next (sat 13)) (does ?v82500 (assign 19 t)) (role ?v82500))
(<= (next (sat 13)) (does ?v82521 (assign 18 f)) (role ?v82521))
(<= (next (sat 13)) (does ?v82542 (assign 15 t)) (role ?v82542))
(<= (next (sat 14)) (does ?v82565 (assign 6 t)) (role ?v82565))
(<= (next (sat 14)) (does ?v82586 (assign 15 t)) (role ?v82586))
(<= (next (sat 14)) (does ?v82607 (assign 2 f)) (role ?v82607))
(<= (next (sat 15)) (does ?v82630 (assign 12 t)) (role ?v82630))
(<= (next (sat 15)) (does ?v82651 (assign 8 t)) (role ?v82651))
(<= (next (sat 15)) (does ?v82672 (assign 14 f)) (role ?v82672))
(<= (next (sat 16)) (does ?v82695 (assign 1 f)) (role ?v82695))
(<= (next (sat 16)) (does ?v82716 (assign 2 f)) (role ?v82716))
(<= (next (sat 16)) (does ?v82737 (assign 3 f)) (role ?v82737))
(<= (next (sat 17)) (does ?v82760 (assign 11 t)) (role ?v82760))
(<= (next (sat 17)) (does ?v82781 (assign 8 f)) (role ?v82781))
(<= (next (sat 17)) (does ?v82802 (assign 5 t)) (role ?v82802))
(<= (next (sat 18)) (does ?v82825 (assign 6 t)) (role ?v82825))
(<= (next (sat 18)) (does ?v82846 (assign 18 t)) (role ?v82846))
(<= (next (sat 18)) (does ?v82867 (assign 1 f)) (role ?v82867))
(<= (next (sat 19)) (does ?v82890 (assign 7 t)) (role ?v82890))
(<= (next (sat 19)) (does ?v82911 (assign 11 f)) (role ?v82911))
(<= (next (sat 19)) (does ?v82932 (assign 8 t)) (role ?v82932))
(<= (next (sat 20)) (does ?v82955 (assign 1 t)) (role ?v82955))
(<= (next (sat 20)) (does ?v82976 (assign 5 t)) (role ?v82976))
(<= (next (sat 20)) (does ?v82997 (assign 15 t)) (role ?v82997))
(<= (next (sat 21)) (does ?v83020 (assign 4 t)) (role ?v83020))
(<= (next (sat 21)) (does ?v83041 (assign 10 t)) (role ?v83041))
(<= (next (sat 21)) (does ?v83062 (assign 12 t)) (role ?v83062))
(<= (next (sat 22)) (does ?v83085 (assign 11 t)) (role ?v83085))
(<= (next (sat 22)) (does ?v83106 (assign 6 t)) (role ?v83106))
(<= (next (sat 22)) (does ?v83127 (assign 18 t)) (role ?v83127))
(<= (next (sat 23)) (does ?v83150 (assign 7 t)) (role ?v83150))
(<= (next (sat 23)) (does ?v83171 (assign 10 t)) (role ?v83171))
(<= (next (sat 23)) (does ?v83192 (assign 3 t)) (role ?v83192))
(<= (next (sat 24)) (does ?v83215 (assign 14 t)) (role ?v83215))
(<= (next (sat 24)) (does ?v83236 (assign 16 f)) (role ?v83236))
(<= (next (sat 24)) (does ?v83257 (assign 17 f)) (role ?v83257))
(<= (next (sat 25)) (does ?v83280 (assign 4 t)) (role ?v83280))
(<= (next (sat 25)) (does ?v83301 (assign 18 t)) (role ?v83301))
(<= (next (sat 25)) (does ?v83322 (assign 13 t)) (role ?v83322))
(<= (next (sat 26)) (does ?v83345 (assign 11 f)) (role ?v83345))
(<= (next (sat 26)) (does ?v83366 (assign 15 f)) (role ?v83366))
(<= (next (sat 26)) (does ?v83387 (assign 13 f)) (role ?v83387))
(<= (next (sat 27)) (does ?v83410 (assign 2 f)) (role ?v83410))
(<= (next (sat 27)) (does ?v83431 (assign 9 f)) (role ?v83431))
(<= (next (sat 27)) (does ?v83452 (assign 20 t)) (role ?v83452))
(<= (next (sat 28)) (does ?v83475 (assign 2 t)) (role ?v83475))
(<= (next (sat 28)) (does ?v83496 (assign 5 f)) (role ?v83496))
(<= (next (sat 28)) (does ?v83517 (assign 19 t)) (role ?v83517))
(<= (next (sat 29)) (does ?v83540 (assign 14 t)) (role ?v83540))
(<= (next (sat 29)) (does ?v83561 (assign 6 t)) (role ?v83561))
(<= (next (sat 29)) (does ?v83582 (assign 19 f)) (role ?v83582))
(<= (next (sat 30)) (does ?v83605 (assign 8 f)) (role ?v83605))
(<= (next (sat 30)) (does ?v83626 (assign 13 f)) (role ?v83626))
(<= (next (sat 30)) (does ?v83647 (assign 20 t)) (role ?v83647))
(<= (next (sat 31)) (does ?v83670 (assign 9 f)) (role ?v83670))
(<= (next (sat 31)) (does ?v83691 (assign 8 t)) (role ?v83691))
(<= (next (sat 31)) (does ?v83712 (assign 13 t)) (role ?v83712))
(<= (next (sat 32)) (does ?v83735 (assign 2 t)) (role ?v83735))
(<= (next (sat 32)) (does ?v83756 (assign 14 f)) (role ?v83756))
(<= (next (sat 32)) (does ?v83777 (assign 7 f)) (role ?v83777))
(<= (next (sat 33)) (does ?v83800 (assign 3 t)) (role ?v83800))
(<= (next (sat 33)) (does ?v83821 (assign 16 t)) (role ?v83821))
(<= (next (sat 33)) (does ?v83842 (assign 15 f)) (role ?v83842))
(<= (next (sat 34)) (does ?v83865 (assign 2 f)) (role ?v83865))
(<= (next (sat 34)) (does ?v83886 (assign 13 t)) (role ?v83886))
(<= (next (sat 34)) (does ?v83907 (assign 17 t)) (role ?v83907))
(<= (next (sat 35)) (does ?v83930 (assign 18 f)) (role ?v83930))
(<= (next (sat 35)) (does ?v83951 (assign 13 f)) (role ?v83951))
(<= (next (sat 35)) (does ?v83972 (assign 16 t)) (role ?v83972))
(<= (next (sat 36)) (does ?v83995 (assign 18 f)) (role ?v83995))
(<= (next (sat 36)) (does ?v84016 (assign 1 t)) (role ?v84016))
(<= (next (sat 36)) (does ?v84037 (assign 16 f)) (role ?v84037))
(<= (next (sat 37)) (does ?v84060 (assign 18 t)) (role ?v84060))
(<= (next (sat 37)) (does ?v84081 (assign 2 t)) (role ?v84081))
(<= (next (sat 37)) (does ?v84102 (assign 14 t)) (role ?v84102))
(<= (next (sat 38)) (does ?v84125 (assign 20 f)) (role ?v84125))
(<= (next (sat 38)) (does ?v84146 (assign 6 t)) (role ?v84146))
(<= (next (sat 38)) (does ?v84167 (assign 14 f)) (role ?v84167))
(<= (next (sat 39)) (does ?v84190 (assign 15 t)) (role ?v84190))
(<= (next (sat 39)) (does ?v84211 (assign 19 f)) (role ?v84211))
(<= (next (sat 39)) (does ?v84232 (assign 8 f)) (role ?v84232))
(<= (next (sat 40)) (does ?v84255 (assign 4 t)) (role ?v84255))
(<= (next (sat 40)) (does ?v84276 (assign 12 t)) (role ?v84276))
(<= (next (sat 40)) (does ?v84297 (assign 11 f)) (role ?v84297))
(<= (next (sat 41)) (does ?v84320 (assign 19 t)) (role ?v84320))
(<= (next (sat 41)) (does ?v84341 (assign 3 t)) (role ?v84341))
(<= (next (sat 41)) (does ?v84362 (assign 14 f)) (role ?v84362))
(<= (next (sat 42)) (does ?v84385 (assign 6 t)) (role ?v84385))
(<= (next (sat 42)) (does ?v84406 (assign 5 t)) (role ?v84406))
(<= (next (sat 42)) (does ?v84427 (assign 7 f)) (role ?v84427))
(<= (next (sat 43)) (does ?v84450 (assign 10 t)) (role ?v84450))
(<= (next (sat 43)) (does ?v84471 (assign 13 t)) (role ?v84471))
(<= (next (sat 43)) (does ?v84492 (assign 11 f)) (role ?v84492))
(<= (next (sat 44)) (does ?v84515 (assign 15 t)) (role ?v84515))
(<= (next (sat 44)) (does ?v84536 (assign 1 f)) (role ?v84536))
(<= (next (sat 44)) (does ?v84557 (assign 3 f)) (role ?v84557))
(<= (next (sat 45)) (does ?v84580 (assign 9 t)) (role ?v84580))
(<= (next (sat 45)) (does ?v84601 (assign 6 t)) (role ?v84601))
(<= (next (sat 45)) (does ?v84622 (assign 10 t)) (role ?v84622))
(<= (next (sat 46)) (does ?v84645 (assign 11 f)) (role ?v84645))
(<= (next (sat 46)) (does ?v84666 (assign 1 f)) (role ?v84666))
(<= (next (sat 46)) (does ?v84687 (assign 16 t)) (role ?v84687))
(<= (next (sat 47)) (does ?v84710 (assign 18 t)) (role ?v84710))
(<= (next (sat 47)) (does ?v84731 (assign 1 f)) (role ?v84731))
(<= (next (sat 47)) (does ?v84752 (assign 12 t)) (role ?v84752))
(<= (next (sat 48)) (does ?v84775 (assign 18 t)) (role ?v84775))
(<= (next (sat 48)) (does ?v84796 (assign 2 f)) (role ?v84796))
(<= (next (sat 48)) (does ?v84817 (assign 4 f)) (role ?v84817))
(<= (next (sat 49)) (does ?v84840 (assign 5 t)) (role ?v84840))
(<= (next (sat 49)) (does ?v84861 (assign 13 t)) (role ?v84861))
(<= (next (sat 49)) (does ?v84882 (assign 20 f)) (role ?v84882))
(<= (next (sat 50)) (does ?v84905 (assign 19 t)) (role ?v84905))
(<= (next (sat 50)) (does ?v84926 (assign 12 f)) (role ?v84926))
(<= (next (sat 50)) (does ?v84947 (assign 6 f)) (role ?v84947))
(<= (next (sat 51)) (does ?v84970 (assign 15 t)) (role ?v84970))
(<= (next (sat 51)) (does ?v84991 (assign 11 t)) (role ?v84991))
(<= (next (sat 51)) (does ?v85012 (assign 13 t)) (role ?v85012))
(<= (next (sat 52)) (does ?v85035 (assign 12 t)) (role ?v85035))
(<= (next (sat 52)) (does ?v85056 (assign 2 t)) (role ?v85056))
(<= (next (sat 52)) (does ?v85077 (assign 7 f)) (role ?v85077))
(<= (next (sat 53)) (does ?v85100 (assign 3 t)) (role ?v85100))
(<= (next (sat 53)) (does ?v85121 (assign 5 t)) (role ?v85121))
(<= (next (sat 53)) (does ?v85142 (assign 19 f)) (role ?v85142))
(<= (next (sat 54)) (does ?v85165 (assign 3 t)) (role ?v85165))
(<= (next (sat 54)) (does ?v85186 (assign 13 t)) (role ?v85186))
(<= (next (sat 54)) (does ?v85207 (assign 10 f)) (role ?v85207))
(<= (next (sat 55)) (does ?v85230 (assign 1 t)) (role ?v85230))
(<= (next (sat 55)) (does ?v85251 (assign 8 t)) (role ?v85251))
(<= (next (sat 55)) (does ?v85272 (assign 6 f)) (role ?v85272))
(<= (next (sat 56)) (does ?v85295 (assign 2 f)) (role ?v85295))
(<= (next (sat 56)) (does ?v85316 (assign 18 t)) (role ?v85316))
(<= (next (sat 56)) (does ?v85337 (assign 11 f)) (role ?v85337))
(<= (next (sat 57)) (does ?v85360 (assign 3 f)) (role ?v85360))
(<= (next (sat 57)) (does ?v85381 (assign 6 t)) (role ?v85381))
(<= (next (sat 57)) (does ?v85402 (assign 9 f)) (role ?v85402))
(<= (next (sat 58)) (does ?v85425 (assign 18 f)) (role ?v85425))
(<= (next (sat 58)) (does ?v85446 (assign 14 f)) (role ?v85446))
(<= (next (sat 58)) (does ?v85467 (assign 3 f)) (role ?v85467))
(<= (next (sat 59)) (does ?v85490 (assign 4 f)) (role ?v85490))
(<= (next (sat 59)) (does ?v85511 (assign 19 f)) (role ?v85511))
(<= (next (sat 59)) (does ?v85532 (assign 17 f)) (role ?v85532))
(<= (next (sat 60)) (does ?v85555 (assign 7 t)) (role ?v85555))
(<= (next (sat 60)) (does ?v85576 (assign 5 t)) (role ?v85576))
(<= (next (sat 60)) (does ?v85597 (assign 14 f)) (role ?v85597))
(<= (next (sat 61)) (does ?v85620 (assign 13 t)) (role ?v85620))
(<= (next (sat 61)) (does ?v85641 (assign 19 t)) (role ?v85641))
(<= (next (sat 61)) (does ?v85662 (assign 12 f)) (role ?v85662))
(<= (next (sat 62)) (does ?v85685 (assign 12 f)) (role ?v85685))
(<= (next (sat 62)) (does ?v85706 (assign 7 f)) (role ?v85706))
(<= (next (sat 62)) (does ?v85727 (assign 3 f)) (role ?v85727))
(<= (next (sat 63)) (does ?v85750 (assign 9 t)) (role ?v85750))
(<= (next (sat 63)) (does ?v85771 (assign 7 t)) (role ?v85771))
(<= (next (sat 63)) (does ?v85792 (assign 19 f)) (role ?v85792))
(<= (next (sat 64)) (does ?v85815 (assign 6 t)) (role ?v85815))
(<= (next (sat 64)) (does ?v85836 (assign 2 t)) (role ?v85836))
(<= (next (sat 64)) (does ?v85857 (assign 10 t)) (role ?v85857))
(<= (next (sat 65)) (does ?v85880 (assign 11 t)) (role ?v85880))
(<= (next (sat 65)) (does ?v85901 (assign 6 t)) (role ?v85901))
(<= (next (sat 65)) (does ?v85922 (assign 12 f)) (role ?v85922))
(<= (next (sat 66)) (does ?v85945 (assign 15 t)) (role ?v85945))
(<= (next (sat 66)) (does ?v85966 (assign 1 t)) (role ?v85966))
(<= (next (sat 66)) (does ?v85987 (assign 17 f)) (role ?v85987))
(<= (next (sat 67)) (does ?v86010 (assign 20 t)) (role ?v86010))
(<= (next (sat 67)) (does ?v86031 (assign 1 f)) (role ?v86031))
(<= (next (sat 67)) (does ?v86052 (assign 4 f)) (role ?v86052))
(<= (next (sat 68)) (does ?v86075 (assign 18 f)) (role ?v86075))
(<= (next (sat 68)) (does ?v86096 (assign 1 t)) (role ?v86096))
(<= (next (sat 68)) (does ?v86117 (assign 5 t)) (role ?v86117))
(<= (next (sat 69)) (does ?v86140 (assign 9 t)) (role ?v86140))
(<= (next (sat 69)) (does ?v86161 (assign 18 t)) (role ?v86161))
(<= (next (sat 69)) (does ?v86182 (assign 14 t)) (role ?v86182))
(<= (next (sat 70)) (does ?v86205 (assign 15 t)) (role ?v86205))
(<= (next (sat 70)) (does ?v86226 (assign 17 f)) (role ?v86226))
(<= (next (sat 70)) (does ?v86247 (assign 9 t)) (role ?v86247))
(<= (next (sat 71)) (does ?v86270 (assign 3 f)) (role ?v86270))
(<= (next (sat 71)) (does ?v86291 (assign 11 t)) (role ?v86291))
(<= (next (sat 71)) (does ?v86312 (assign 9 t)) (role ?v86312))
(<= (next (sat 72)) (does ?v86335 (assign 14 t)) (role ?v86335))
(<= (next (sat 72)) (does ?v86356 (assign 12 t)) (role ?v86356))
(<= (next (sat 72)) (does ?v86377 (assign 9 t)) (role ?v86377))
(<= (next (sat 73)) (does ?v86400 (assign 5 t)) (role ?v86400))
(<= (next (sat 73)) (does ?v86421 (assign 14 t)) (role ?v86421))
(<= (next (sat 73)) (does ?v86442 (assign 2 t)) (role ?v86442))
(<= (next (sat 74)) (does ?v86465 (assign 17 t)) (role ?v86465))
(<= (next (sat 74)) (does ?v86486 (assign 10 f)) (role ?v86486))
(<= (next (sat 74)) (does ?v86507 (assign 8 f)) (role ?v86507))
(<= (next (sat 75)) (does ?v86530 (assign 14 t)) (role ?v86530))
(<= (next (sat 75)) (does ?v86551 (assign 15 f)) (role ?v86551))
(<= (next (sat 75)) (does ?v86572 (assign 9 t)) (role ?v86572))
(<= (next (sat 76)) (does ?v86595 (assign 6 f)) (role ?v86595))
(<= (next (sat 76)) (does ?v86616 (assign 20 f)) (role ?v86616))
(<= (next (sat 76)) (does ?v86637 (assign 13 t)) (role ?v86637))
(<= (next (sat 77)) (does ?v86660 (assign 1 t)) (role ?v86660))
(<= (next (sat 77)) (does ?v86681 (assign 6 t)) (role ?v86681))
(<= (next (sat 77)) (does ?v86702 (assign 13 t)) (role ?v86702))
(<= (next (sat 78)) (does ?v86725 (assign 16 f)) (role ?v86725))
(<= (next (sat 78)) (does ?v86746 (assign 15 t)) (role ?v86746))
(<= (next (sat 78)) (does ?v86767 (assign 17 f)) (role ?v86767))
(<= (next (sat 79)) (does ?v86790 (assign 8 f)) (role ?v86790))
(<= (next (sat 79)) (does ?v86811 (assign 19 t)) (role ?v86811))
(<= (next (sat 79)) (does ?v86832 (assign 7 t)) (role ?v86832))
(<= (next (sat 80)) (does ?v86855 (assign 7 f)) (role ?v86855))
(<= (next (sat 80)) (does ?v86876 (assign 3 t)) (role ?v86876))
(<= (next (sat 80)) (does ?v86897 (assign 1 f)) (role ?v86897))
(<= (next (sat 81)) (does ?v86920 (assign 18 f)) (role ?v86920))
(<= (next (sat 81)) (does ?v86941 (assign 10 t)) (role ?v86941))
(<= (next (sat 81)) (does ?v86962 (assign 17 t)) (role ?v86962))
(<= (next (sat 82)) (does ?v86985 (assign 12 t)) (role ?v86985))
(<= (next (sat 82)) (does ?v87006 (assign 4 f)) (role ?v87006))
(<= (next (sat 82)) (does ?v87027 (assign 14 t)) (role ?v87027))
(<= (next (sat 83)) (does ?v87050 (assign 7 t)) (role ?v87050))
(<= (next (sat 83)) (does ?v87071 (assign 10 t)) (role ?v87071))
(<= (next (sat 83)) (does ?v87092 (assign 19 t)) (role ?v87092))
(<= (next (sat 84)) (does ?v87115 (assign 20 t)) (role ?v87115))
(<= (next (sat 84)) (does ?v87136 (assign 15 t)) (role ?v87136))
(<= (next (sat 84)) (does ?v87157 (assign 19 t)) (role ?v87157))
(<= (next (sat 85)) (does ?v87180 (assign 13 f)) (role ?v87180))
(<= (next (sat 85)) (does ?v87201 (assign 17 f)) (role ?v87201))
(<= (next (sat 85)) (does ?v87222 (assign 9 f)) (role ?v87222))
(<= (next (sat 86)) (does ?v87245 (assign 10 t)) (role ?v87245))
(<= (next (sat 86)) (does ?v87266 (assign 9 f)) (role ?v87266))
(<= (next (sat 86)) (does ?v87287 (assign 3 t)) (role ?v87287))
(<= (next (sat 87)) (does ?v87310 (assign 15 t)) (role ?v87310))
(<= (next (sat 87)) (does ?v87331 (assign 11 f)) (role ?v87331))
(<= (next (sat 87)) (does ?v87352 (assign 10 t)) (role ?v87352))
(<= (next (sat 88)) (does ?v87375 (assign 12 t)) (role ?v87375))
(<= (next (sat 88)) (does ?v87396 (assign 1 t)) (role ?v87396))
(<= (next (sat 88)) (does ?v87417 (assign 13 f)) (role ?v87417))
(<= (next (sat 89)) (does ?v87440 (assign 11 t)) (role ?v87440))
(<= (next (sat 89)) (does ?v87461 (assign 3 t)) (role ?v87461))
(<= (next (sat 89)) (does ?v87482 (assign 15 t)) (role ?v87482))
(<= (next (sat 90)) (does ?v87505 (assign 16 t)) (role ?v87505))
(<= (next (sat 90)) (does ?v87526 (assign 2 f)) (role ?v87526))
(<= (next (sat 90)) (does ?v87547 (assign 1 f)) (role ?v87547))
(<= (next (sat 91)) (does ?v87570 (assign 17 f)) (role ?v87570))
(<= (next (sat 91)) (does ?v87591 (assign 5 f)) (role ?v87591))
(<= (next (sat 91)) (does ?v87612 (assign 1 f)) (role ?v87612))
(<= all_sat (true (sat 1)) (true (sat 2)) (true (sat 3)) (true (sat 4)) (true (sat 5)) (true (sat 6)) (true (sat 7)) (true (sat 8)) (true (sat 9)) (true (sat 10)) (true (sat 11)) (true (sat 12)) (true (sat 13)) (true (sat 14)) (true (sat 15)) (true (sat 16)) (true (sat 17)) (true (sat 18)) (true (sat 19)) (true (sat 20)) (true (sat 21)) (true (sat 22)) (true (sat 23)) (true (sat 24)) (true (sat 25)) (true (sat 26)) (true (sat 27)) (true (sat 28)) (true (sat 29)) (true (sat 30)) (true (sat 31)) (true (sat 32)) (true (sat 33)) (true (sat 34)) (true (sat 35)) (true (sat 36)) (true (sat 37)) (true (sat 38)) (true (sat 39)) (true (sat 40)) (true (sat 41)) (true (sat 42)) (true (sat 43)) (true (sat 44)) (true (sat 45)) (true (sat 46)) (true (sat 47)) (true (sat 48)) (true (sat 49)) (true (sat 50)) (true (sat 51)) (true (sat 52)) (true (sat 53)) (true (sat 54)) (true (sat 55)) (true (sat 56)) (true (sat 57)) (true (sat 58)) (true (sat 59)) (true (sat 60)) (true (sat 61)) (true (sat 62)) (true (sat 63)) (true (sat 64)) (true (sat 65)) (true (sat 66)) (true (sat 67)) (true (sat 68)) (true (sat 69)) (true (sat 70)) (true (sat 71)) (true (sat 72)) (true (sat 73)) (true (sat 74)) (true (sat 75)) (true (sat 76)) (true (sat 77)) (true (sat 78)) (true (sat 79)) (true (sat 80)) (true (sat 81)) (true (sat 82)) (true (sat 83)) (true (sat 84)) (true (sat 85)) (true (sat 86)) (true (sat 87)) (true (sat 88)) (true (sat 89)) (true (sat 90)) (true (sat 91)))
(<= terminal all_sat)
(<= terminal (true (control the end)))
(<= (goal exists 100) all_sat)
(<= (goal exists 0) (not all_sat))

sees_XML(...) rules

(<= (sees_xml random ?t) (sees_xml1 ?t))
(<= (sees_xml ?p ?t) (role ?p) (distinct ?p random) (sees_xml1 ?t))

(<= (sees_xml1 ?t) (true ?t))
(<= (sees_xml1 (contains ?clause ?literal)) (contains ?clause ?literal))