You are not logged in. login register
Game 3qbf-5cnf-20var-40cl.2.qdimacs.SAT
name 3qbf-5cnf-20var-40cl.2.qdimacs.SAT
creator hannes
number of roles 2
stylesheet sat/sat.xsl
GDL v1
enabled
matches show matches
statistics show game statistics
description

Game Description

(contains 1 (neg 35))
(contains 1 (neg 40))
(contains 1 (neg 19))
(contains 1 57)
(contains 1 10)
(contains 2 (neg 35))
(contains 2 9)
(contains 2 60)
(contains 2 30)
(contains 2 (neg 29))
(contains 3 (neg 6))
(contains 3 (neg 30))
(contains 3 54)
(contains 3 (neg 22))
(contains 3 48)
(contains 4 34)
(contains 4 (neg 28))
(contains 4 32)
(contains 4 2)
(contains 4 (neg 55))
(contains 5 44)
(contains 5 (neg 53))
(contains 5 (neg 3))
(contains 5 54)
(contains 5 55)
(contains 6 40)
(contains 6 53)
(contains 6 50)
(contains 6 2)
(contains 6 27)
(contains 7 (neg 11))
(contains 7 27)
(contains 7 (neg 22))
(contains 7 (neg 37))
(contains 7 43)
(contains 8 (neg 41))
(contains 8 25)
(contains 8 (neg 30))
(contains 8 16)
(contains 8 (neg 27))
(contains 9 (neg 20))
(contains 9 46)
(contains 9 35)
(contains 9 26)
(contains 9 (neg 34))
(contains 10 (neg 47))
(contains 10 50)
(contains 10 (neg 60))
(contains 10 (neg 53))
(contains 10 (neg 59))
(contains 11 47)
(contains 11 8)
(contains 11 55)
(contains 11 (neg 21))
(contains 11 1)
(contains 12 7)
(contains 12 (neg 16))
(contains 12 (neg 54))
(contains 12 28)
(contains 12 (neg 19))
(contains 13 (neg 17))
(contains 13 (neg 4))
(contains 13 9)
(contains 13 38)
(contains 13 24)
(contains 14 24)
(contains 14 7)
(contains 14 (neg 40))
(contains 14 31)
(contains 14 18)
(contains 15 56)
(contains 15 40)
(contains 15 (neg 35))
(contains 15 (neg 28))
(contains 15 14)
(contains 16 (neg 13))
(contains 16 57)
(contains 16 47)
(contains 16 40)
(contains 16 (neg 58))
(contains 17 50)
(contains 17 (neg 8))
(contains 17 (neg 29))
(contains 17 (neg 57))
(contains 17 (neg 31))
(contains 18 (neg 20))
(contains 18 (neg 37))
(contains 18 (neg 6))
(contains 18 13)
(contains 18 (neg 32))
(contains 19 48)
(contains 19 33)
(contains 19 (neg 60))
(contains 19 25)
(contains 19 (neg 51))
(contains 20 (neg 6))
(contains 20 (neg 55))
(contains 20 46)
(contains 20 30)
(contains 20 (neg 29))
(contains 21 51)
(contains 21 50)
(contains 21 (neg 36))
(contains 21 (neg 57))
(contains 21 (neg 7))
(contains 22 21)
(contains 22 14)
(contains 22 33)
(contains 22 52)
(contains 22 (neg 10))
(contains 23 (neg 6))
(contains 23 9)
(contains 23 (neg 17))
(contains 23 (neg 46))
(contains 23 1)
(contains 24 31)
(contains 24 (neg 10))
(contains 24 (neg 36))
(contains 24 (neg 55))
(contains 24 9)
(contains 25 (neg 47))
(contains 25 43)
(contains 25 (neg 21))
(contains 25 52)
(contains 25 (neg 50))
(contains 26 (neg 17))
(contains 26 (neg 24))
(contains 26 44)
(contains 26 (neg 33))
(contains 26 (neg 3))
(contains 27 2)
(contains 27 (neg 38))
(contains 27 35)
(contains 27 (neg 48))
(contains 27 (neg 11))
(contains 28 26)
(contains 28 (neg 51))
(contains 28 (neg 42))
(contains 28 (neg 6))
(contains 28 (neg 56))
(contains 29 12)
(contains 29 (neg 59))
(contains 29 (neg 36))
(contains 29 (neg 6))
(contains 29 26)
(contains 30 (neg 13))
(contains 30 2)
(contains 30 30)
(contains 30 26)
(contains 30 (neg 14))
(contains 31 (neg 24))
(contains 31 (neg 36))
(contains 31 41)
(contains 31 (neg 13))
(contains 31 4)
(contains 32 (neg 3))
(contains 32 8)
(contains 32 16)
(contains 32 1)
(contains 32 (neg 2))
(contains 33 39)
(contains 33 (neg 46))
(contains 33 15)
(contains 33 (neg 51))
(contains 33 49)
(contains 34 (neg 49))
(contains 34 23)
(contains 34 (neg 53))
(contains 34 (neg 55))
(contains 34 30)
(contains 35 25)
(contains 35 6)
(contains 35 44)
(contains 35 19)
(contains 35 39)
(contains 36 12)
(contains 36 (neg 39))
(contains 36 (neg 56))
(contains 36 11)
(contains 36 55)
(contains 37 21)
(contains 37 (neg 55))
(contains 37 (neg 57))
(contains 37 26)
(contains 37 (neg 53))
(contains 38 (neg 42))
(contains 38 (neg 20))
(contains 38 37)
(contains 38 (neg 27))
(contains 38 (neg 8))
(contains 39 (neg 53))
(contains 39 60)
(contains 39 3)
(contains 39 (neg 1))
(contains 39 (neg 29))
(contains 40 (neg 59))
(contains 40 20)
(contains 40 24)
(contains 40 18)
(contains 40 47)
(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)
(prop_var 21)
(prop_var 22)
(prop_var 23)
(prop_var 24)
(prop_var 25)
(prop_var 26)
(prop_var 27)
(prop_var 28)
(prop_var 29)
(prop_var 30)
(prop_var 31)
(prop_var 32)
(prop_var 33)
(prop_var 34)
(prop_var 35)
(prop_var 36)
(prop_var 37)
(prop_var 38)
(prop_var 39)
(prop_var 40)
(prop_var 41)
(prop_var 42)
(prop_var 43)
(prop_var 44)
(prop_var 45)
(prop_var 46)
(prop_var 47)
(prop_var 48)
(prop_var 49)
(prop_var 50)
(prop_var 51)
(prop_var 52)
(prop_var 53)
(prop_var 54)
(prop_var 55)
(prop_var 56)
(prop_var 57)
(prop_var 58)
(prop_var 59)
(prop_var 60)
(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)
(role exists)
(role forall)
(truth_value t)
(truth_value f)
(init (control exists 1))
(<= (legal ?v74761 (assign ?v74766 ?v74767)) (true (control ?v74761 ?v74766)) (role ?v74761) (prop_var ?v74766) (truth_value ?v74767))
(<= (legal exists noop) (true (control forall ?v74829)) (prop_var ?v74829))
(<= (legal forall noop) (true (control exists ?v74829)) (prop_var ?v74829))
(<= (next (sat ?v74853)) (true (sat ?v74853)) (clause ?v74853))
(<= (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 forall 21)) (true (control exists 20)))
(<= (next (control forall 22)) (true (control forall 21)))
(<= (next (control forall 23)) (true (control forall 22)))
(<= (next (control forall 24)) (true (control forall 23)))
(<= (next (control forall 25)) (true (control forall 24)))
(<= (next (control forall 26)) (true (control forall 25)))
(<= (next (control forall 27)) (true (control forall 26)))
(<= (next (control forall 28)) (true (control forall 27)))
(<= (next (control forall 29)) (true (control forall 28)))
(<= (next (control forall 30)) (true (control forall 29)))
(<= (next (control forall 31)) (true (control forall 30)))
(<= (next (control forall 32)) (true (control forall 31)))
(<= (next (control forall 33)) (true (control forall 32)))
(<= (next (control forall 34)) (true (control forall 33)))
(<= (next (control forall 35)) (true (control forall 34)))
(<= (next (control forall 36)) (true (control forall 35)))
(<= (next (control forall 37)) (true (control forall 36)))
(<= (next (control forall 38)) (true (control forall 37)))
(<= (next (control forall 39)) (true (control forall 38)))
(<= (next (control forall 40)) (true (control forall 39)))
(<= (next (control exists 41)) (true (control forall 40)))
(<= (next (control exists 42)) (true (control exists 41)))
(<= (next (control exists 43)) (true (control exists 42)))
(<= (next (control exists 44)) (true (control exists 43)))
(<= (next (control exists 45)) (true (control exists 44)))
(<= (next (control exists 46)) (true (control exists 45)))
(<= (next (control exists 47)) (true (control exists 46)))
(<= (next (control exists 48)) (true (control exists 47)))
(<= (next (control exists 49)) (true (control exists 48)))
(<= (next (control exists 50)) (true (control exists 49)))
(<= (next (control exists 51)) (true (control exists 50)))
(<= (next (control exists 52)) (true (control exists 51)))
(<= (next (control exists 53)) (true (control exists 52)))
(<= (next (control exists 54)) (true (control exists 53)))
(<= (next (control exists 55)) (true (control exists 54)))
(<= (next (control exists 56)) (true (control exists 55)))
(<= (next (control exists 57)) (true (control exists 56)))
(<= (next (control exists 58)) (true (control exists 57)))
(<= (next (control exists 59)) (true (control exists 58)))
(<= (next (control exists 60)) (true (control exists 59)))
(<= (next (control the end)) (true (control exists 60)))
(<= (next (sat 1)) (does ?v79631 (assign 35 f)) (role ?v79631))
(<= (next (sat 1)) (does ?v79652 (assign 40 f)) (role ?v79652))
(<= (next (sat 1)) (does ?v79673 (assign 19 f)) (role ?v79673))
(<= (next (sat 1)) (does ?v79694 (assign 57 t)) (role ?v79694))
(<= (next (sat 1)) (does ?v79715 (assign 10 t)) (role ?v79715))
(<= (next (sat 2)) (does ?v79738 (assign 35 f)) (role ?v79738))
(<= (next (sat 2)) (does ?v79759 (assign 9 t)) (role ?v79759))
(<= (next (sat 2)) (does ?v79780 (assign 60 t)) (role ?v79780))
(<= (next (sat 2)) (does ?v79801 (assign 30 t)) (role ?v79801))
(<= (next (sat 2)) (does ?v79822 (assign 29 f)) (role ?v79822))
(<= (next (sat 3)) (does ?v79845 (assign 6 f)) (role ?v79845))
(<= (next (sat 3)) (does ?v79866 (assign 30 f)) (role ?v79866))
(<= (next (sat 3)) (does ?v79887 (assign 54 t)) (role ?v79887))
(<= (next (sat 3)) (does ?v79908 (assign 22 f)) (role ?v79908))
(<= (next (sat 3)) (does ?v79929 (assign 48 t)) (role ?v79929))
(<= (next (sat 4)) (does ?v79952 (assign 34 t)) (role ?v79952))
(<= (next (sat 4)) (does ?v79973 (assign 28 f)) (role ?v79973))
(<= (next (sat 4)) (does ?v79994 (assign 32 t)) (role ?v79994))
(<= (next (sat 4)) (does ?v80015 (assign 2 t)) (role ?v80015))
(<= (next (sat 4)) (does ?v80036 (assign 55 f)) (role ?v80036))
(<= (next (sat 5)) (does ?v80059 (assign 44 t)) (role ?v80059))
(<= (next (sat 5)) (does ?v80080 (assign 53 f)) (role ?v80080))
(<= (next (sat 5)) (does ?v80101 (assign 3 f)) (role ?v80101))
(<= (next (sat 5)) (does ?v80122 (assign 54 t)) (role ?v80122))
(<= (next (sat 5)) (does ?v80143 (assign 55 t)) (role ?v80143))
(<= (next (sat 6)) (does ?v80166 (assign 40 t)) (role ?v80166))
(<= (next (sat 6)) (does ?v80187 (assign 53 t)) (role ?v80187))
(<= (next (sat 6)) (does ?v80208 (assign 50 t)) (role ?v80208))
(<= (next (sat 6)) (does ?v80229 (assign 2 t)) (role ?v80229))
(<= (next (sat 6)) (does ?v80250 (assign 27 t)) (role ?v80250))
(<= (next (sat 7)) (does ?v80273 (assign 11 f)) (role ?v80273))
(<= (next (sat 7)) (does ?v80294 (assign 27 t)) (role ?v80294))
(<= (next (sat 7)) (does ?v80315 (assign 22 f)) (role ?v80315))
(<= (next (sat 7)) (does ?v80336 (assign 37 f)) (role ?v80336))
(<= (next (sat 7)) (does ?v80357 (assign 43 t)) (role ?v80357))
(<= (next (sat 8)) (does ?v80380 (assign 41 f)) (role ?v80380))
(<= (next (sat 8)) (does ?v80401 (assign 25 t)) (role ?v80401))
(<= (next (sat 8)) (does ?v80422 (assign 30 f)) (role ?v80422))
(<= (next (sat 8)) (does ?v80443 (assign 16 t)) (role ?v80443))
(<= (next (sat 8)) (does ?v80464 (assign 27 f)) (role ?v80464))
(<= (next (sat 9)) (does ?v80487 (assign 20 f)) (role ?v80487))
(<= (next (sat 9)) (does ?v80508 (assign 46 t)) (role ?v80508))
(<= (next (sat 9)) (does ?v80529 (assign 35 t)) (role ?v80529))
(<= (next (sat 9)) (does ?v80550 (assign 26 t)) (role ?v80550))
(<= (next (sat 9)) (does ?v80571 (assign 34 f)) (role ?v80571))
(<= (next (sat 10)) (does ?v80594 (assign 47 f)) (role ?v80594))
(<= (next (sat 10)) (does ?v80615 (assign 50 t)) (role ?v80615))
(<= (next (sat 10)) (does ?v80636 (assign 60 f)) (role ?v80636))
(<= (next (sat 10)) (does ?v80657 (assign 53 f)) (role ?v80657))
(<= (next (sat 10)) (does ?v80678 (assign 59 f)) (role ?v80678))
(<= (next (sat 11)) (does ?v80701 (assign 47 t)) (role ?v80701))
(<= (next (sat 11)) (does ?v80722 (assign 8 t)) (role ?v80722))
(<= (next (sat 11)) (does ?v80743 (assign 55 t)) (role ?v80743))
(<= (next (sat 11)) (does ?v80764 (assign 21 f)) (role ?v80764))
(<= (next (sat 11)) (does ?v80785 (assign 1 t)) (role ?v80785))
(<= (next (sat 12)) (does ?v80808 (assign 7 t)) (role ?v80808))
(<= (next (sat 12)) (does ?v80829 (assign 16 f)) (role ?v80829))
(<= (next (sat 12)) (does ?v80850 (assign 54 f)) (role ?v80850))
(<= (next (sat 12)) (does ?v80871 (assign 28 t)) (role ?v80871))
(<= (next (sat 12)) (does ?v80892 (assign 19 f)) (role ?v80892))
(<= (next (sat 13)) (does ?v80915 (assign 17 f)) (role ?v80915))
(<= (next (sat 13)) (does ?v80936 (assign 4 f)) (role ?v80936))
(<= (next (sat 13)) (does ?v80957 (assign 9 t)) (role ?v80957))
(<= (next (sat 13)) (does ?v80978 (assign 38 t)) (role ?v80978))
(<= (next (sat 13)) (does ?v80999 (assign 24 t)) (role ?v80999))
(<= (next (sat 14)) (does ?v81022 (assign 24 t)) (role ?v81022))
(<= (next (sat 14)) (does ?v81043 (assign 7 t)) (role ?v81043))
(<= (next (sat 14)) (does ?v81064 (assign 40 f)) (role ?v81064))
(<= (next (sat 14)) (does ?v81085 (assign 31 t)) (role ?v81085))
(<= (next (sat 14)) (does ?v81106 (assign 18 t)) (role ?v81106))
(<= (next (sat 15)) (does ?v81129 (assign 56 t)) (role ?v81129))
(<= (next (sat 15)) (does ?v81150 (assign 40 t)) (role ?v81150))
(<= (next (sat 15)) (does ?v81171 (assign 35 f)) (role ?v81171))
(<= (next (sat 15)) (does ?v81192 (assign 28 f)) (role ?v81192))
(<= (next (sat 15)) (does ?v81213 (assign 14 t)) (role ?v81213))
(<= (next (sat 16)) (does ?v81236 (assign 13 f)) (role ?v81236))
(<= (next (sat 16)) (does ?v81257 (assign 57 t)) (role ?v81257))
(<= (next (sat 16)) (does ?v81278 (assign 47 t)) (role ?v81278))
(<= (next (sat 16)) (does ?v81299 (assign 40 t)) (role ?v81299))
(<= (next (sat 16)) (does ?v81320 (assign 58 f)) (role ?v81320))
(<= (next (sat 17)) (does ?v81343 (assign 50 t)) (role ?v81343))
(<= (next (sat 17)) (does ?v81364 (assign 8 f)) (role ?v81364))
(<= (next (sat 17)) (does ?v81385 (assign 29 f)) (role ?v81385))
(<= (next (sat 17)) (does ?v81406 (assign 57 f)) (role ?v81406))
(<= (next (sat 17)) (does ?v81427 (assign 31 f)) (role ?v81427))
(<= (next (sat 18)) (does ?v81450 (assign 20 f)) (role ?v81450))
(<= (next (sat 18)) (does ?v81471 (assign 37 f)) (role ?v81471))
(<= (next (sat 18)) (does ?v81492 (assign 6 f)) (role ?v81492))
(<= (next (sat 18)) (does ?v81513 (assign 13 t)) (role ?v81513))
(<= (next (sat 18)) (does ?v81534 (assign 32 f)) (role ?v81534))
(<= (next (sat 19)) (does ?v81557 (assign 48 t)) (role ?v81557))
(<= (next (sat 19)) (does ?v81578 (assign 33 t)) (role ?v81578))
(<= (next (sat 19)) (does ?v81599 (assign 60 f)) (role ?v81599))
(<= (next (sat 19)) (does ?v81620 (assign 25 t)) (role ?v81620))
(<= (next (sat 19)) (does ?v81641 (assign 51 f)) (role ?v81641))
(<= (next (sat 20)) (does ?v81664 (assign 6 f)) (role ?v81664))
(<= (next (sat 20)) (does ?v81685 (assign 55 f)) (role ?v81685))
(<= (next (sat 20)) (does ?v81706 (assign 46 t)) (role ?v81706))
(<= (next (sat 20)) (does ?v81727 (assign 30 t)) (role ?v81727))
(<= (next (sat 20)) (does ?v81748 (assign 29 f)) (role ?v81748))
(<= (next (sat 21)) (does ?v81771 (assign 51 t)) (role ?v81771))
(<= (next (sat 21)) (does ?v81792 (assign 50 t)) (role ?v81792))
(<= (next (sat 21)) (does ?v81813 (assign 36 f)) (role ?v81813))
(<= (next (sat 21)) (does ?v81834 (assign 57 f)) (role ?v81834))
(<= (next (sat 21)) (does ?v81855 (assign 7 f)) (role ?v81855))
(<= (next (sat 22)) (does ?v81878 (assign 21 t)) (role ?v81878))
(<= (next (sat 22)) (does ?v81899 (assign 14 t)) (role ?v81899))
(<= (next (sat 22)) (does ?v81920 (assign 33 t)) (role ?v81920))
(<= (next (sat 22)) (does ?v81941 (assign 52 t)) (role ?v81941))
(<= (next (sat 22)) (does ?v81962 (assign 10 f)) (role ?v81962))
(<= (next (sat 23)) (does ?v81985 (assign 6 f)) (role ?v81985))
(<= (next (sat 23)) (does ?v82006 (assign 9 t)) (role ?v82006))
(<= (next (sat 23)) (does ?v82027 (assign 17 f)) (role ?v82027))
(<= (next (sat 23)) (does ?v82048 (assign 46 f)) (role ?v82048))
(<= (next (sat 23)) (does ?v82069 (assign 1 t)) (role ?v82069))
(<= (next (sat 24)) (does ?v82092 (assign 31 t)) (role ?v82092))
(<= (next (sat 24)) (does ?v82113 (assign 10 f)) (role ?v82113))
(<= (next (sat 24)) (does ?v82134 (assign 36 f)) (role ?v82134))
(<= (next (sat 24)) (does ?v82155 (assign 55 f)) (role ?v82155))
(<= (next (sat 24)) (does ?v82176 (assign 9 t)) (role ?v82176))
(<= (next (sat 25)) (does ?v82199 (assign 47 f)) (role ?v82199))
(<= (next (sat 25)) (does ?v82220 (assign 43 t)) (role ?v82220))
(<= (next (sat 25)) (does ?v82241 (assign 21 f)) (role ?v82241))
(<= (next (sat 25)) (does ?v82262 (assign 52 t)) (role ?v82262))
(<= (next (sat 25)) (does ?v82283 (assign 50 f)) (role ?v82283))
(<= (next (sat 26)) (does ?v82306 (assign 17 f)) (role ?v82306))
(<= (next (sat 26)) (does ?v82327 (assign 24 f)) (role ?v82327))
(<= (next (sat 26)) (does ?v82348 (assign 44 t)) (role ?v82348))
(<= (next (sat 26)) (does ?v82369 (assign 33 f)) (role ?v82369))
(<= (next (sat 26)) (does ?v82390 (assign 3 f)) (role ?v82390))
(<= (next (sat 27)) (does ?v82413 (assign 2 t)) (role ?v82413))
(<= (next (sat 27)) (does ?v82434 (assign 38 f)) (role ?v82434))
(<= (next (sat 27)) (does ?v82455 (assign 35 t)) (role ?v82455))
(<= (next (sat 27)) (does ?v82476 (assign 48 f)) (role ?v82476))
(<= (next (sat 27)) (does ?v82497 (assign 11 f)) (role ?v82497))
(<= (next (sat 28)) (does ?v82520 (assign 26 t)) (role ?v82520))
(<= (next (sat 28)) (does ?v82541 (assign 51 f)) (role ?v82541))
(<= (next (sat 28)) (does ?v82562 (assign 42 f)) (role ?v82562))
(<= (next (sat 28)) (does ?v82583 (assign 6 f)) (role ?v82583))
(<= (next (sat 28)) (does ?v82604 (assign 56 f)) (role ?v82604))
(<= (next (sat 29)) (does ?v82627 (assign 12 t)) (role ?v82627))
(<= (next (sat 29)) (does ?v82648 (assign 59 f)) (role ?v82648))
(<= (next (sat 29)) (does ?v82669 (assign 36 f)) (role ?v82669))
(<= (next (sat 29)) (does ?v82690 (assign 6 f)) (role ?v82690))
(<= (next (sat 29)) (does ?v82711 (assign 26 t)) (role ?v82711))
(<= (next (sat 30)) (does ?v82734 (assign 13 f)) (role ?v82734))
(<= (next (sat 30)) (does ?v82755 (assign 2 t)) (role ?v82755))
(<= (next (sat 30)) (does ?v82776 (assign 30 t)) (role ?v82776))
(<= (next (sat 30)) (does ?v82797 (assign 26 t)) (role ?v82797))
(<= (next (sat 30)) (does ?v82818 (assign 14 f)) (role ?v82818))
(<= (next (sat 31)) (does ?v82841 (assign 24 f)) (role ?v82841))
(<= (next (sat 31)) (does ?v82862 (assign 36 f)) (role ?v82862))
(<= (next (sat 31)) (does ?v82883 (assign 41 t)) (role ?v82883))
(<= (next (sat 31)) (does ?v82904 (assign 13 f)) (role ?v82904))
(<= (next (sat 31)) (does ?v82925 (assign 4 t)) (role ?v82925))
(<= (next (sat 32)) (does ?v82948 (assign 3 f)) (role ?v82948))
(<= (next (sat 32)) (does ?v82969 (assign 8 t)) (role ?v82969))
(<= (next (sat 32)) (does ?v82990 (assign 16 t)) (role ?v82990))
(<= (next (sat 32)) (does ?v83011 (assign 1 t)) (role ?v83011))
(<= (next (sat 32)) (does ?v83032 (assign 2 f)) (role ?v83032))
(<= (next (sat 33)) (does ?v83055 (assign 39 t)) (role ?v83055))
(<= (next (sat 33)) (does ?v83076 (assign 46 f)) (role ?v83076))
(<= (next (sat 33)) (does ?v83097 (assign 15 t)) (role ?v83097))
(<= (next (sat 33)) (does ?v83118 (assign 51 f)) (role ?v83118))
(<= (next (sat 33)) (does ?v83139 (assign 49 t)) (role ?v83139))
(<= (next (sat 34)) (does ?v83162 (assign 49 f)) (role ?v83162))
(<= (next (sat 34)) (does ?v83183 (assign 23 t)) (role ?v83183))
(<= (next (sat 34)) (does ?v83204 (assign 53 f)) (role ?v83204))
(<= (next (sat 34)) (does ?v83225 (assign 55 f)) (role ?v83225))
(<= (next (sat 34)) (does ?v83246 (assign 30 t)) (role ?v83246))
(<= (next (sat 35)) (does ?v83269 (assign 25 t)) (role ?v83269))
(<= (next (sat 35)) (does ?v83290 (assign 6 t)) (role ?v83290))
(<= (next (sat 35)) (does ?v83311 (assign 44 t)) (role ?v83311))
(<= (next (sat 35)) (does ?v83332 (assign 19 t)) (role ?v83332))
(<= (next (sat 35)) (does ?v83353 (assign 39 t)) (role ?v83353))
(<= (next (sat 36)) (does ?v83376 (assign 12 t)) (role ?v83376))
(<= (next (sat 36)) (does ?v83397 (assign 39 f)) (role ?v83397))
(<= (next (sat 36)) (does ?v83418 (assign 56 f)) (role ?v83418))
(<= (next (sat 36)) (does ?v83439 (assign 11 t)) (role ?v83439))
(<= (next (sat 36)) (does ?v83460 (assign 55 t)) (role ?v83460))
(<= (next (sat 37)) (does ?v83483 (assign 21 t)) (role ?v83483))
(<= (next (sat 37)) (does ?v83504 (assign 55 f)) (role ?v83504))
(<= (next (sat 37)) (does ?v83525 (assign 57 f)) (role ?v83525))
(<= (next (sat 37)) (does ?v83546 (assign 26 t)) (role ?v83546))
(<= (next (sat 37)) (does ?v83567 (assign 53 f)) (role ?v83567))
(<= (next (sat 38)) (does ?v83590 (assign 42 f)) (role ?v83590))
(<= (next (sat 38)) (does ?v83611 (assign 20 f)) (role ?v83611))
(<= (next (sat 38)) (does ?v83632 (assign 37 t)) (role ?v83632))
(<= (next (sat 38)) (does ?v83653 (assign 27 f)) (role ?v83653))
(<= (next (sat 38)) (does ?v83674 (assign 8 f)) (role ?v83674))
(<= (next (sat 39)) (does ?v83697 (assign 53 f)) (role ?v83697))
(<= (next (sat 39)) (does ?v83718 (assign 60 t)) (role ?v83718))
(<= (next (sat 39)) (does ?v83739 (assign 3 t)) (role ?v83739))
(<= (next (sat 39)) (does ?v83760 (assign 1 f)) (role ?v83760))
(<= (next (sat 39)) (does ?v83781 (assign 29 f)) (role ?v83781))
(<= (next (sat 40)) (does ?v83804 (assign 59 f)) (role ?v83804))
(<= (next (sat 40)) (does ?v83825 (assign 20 t)) (role ?v83825))
(<= (next (sat 40)) (does ?v83846 (assign 24 t)) (role ?v83846))
(<= (next (sat 40)) (does ?v83867 (assign 18 t)) (role ?v83867))
(<= (next (sat 40)) (does ?v83888 (assign 47 t)) (role ?v83888))
(<= 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)))
(<= terminal all_sat)
(<= terminal (true (control the end)))
(<= (goal exists 100) all_sat)
(<= (goal exists 0) (not all_sat))
(<= (goal forall 100) (not all_sat))
(<= (goal forall 0) 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))