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

Game Description

(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 ?v488920 (assign ?v488930 ?v488931)) (true (control ?v488920 ?v488930)) (role ?v488920) (prop_var ?v488930) (truth_value ?v488931))
(<= (legal exists noop) (true (control forall ?v488966)) (prop_var ?v488966))
(<= (legal forall noop) (true (control exists ?v488966)) (prop_var ?v488966))
(<= (next (sat ?v488990)) (true (sat ?v488990)) (clause ?v488990))
(<= (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 ?v493768 (assign 56 f)) (role ?v493768))
(<= (next (sat 1)) (does ?v493789 (assign 52 f)) (role ?v493789))
(<= (next (sat 1)) (does ?v493810 (assign 55 f)) (role ?v493810))
(<= (next (sat 1)) (does ?v493831 (assign 27 f)) (role ?v493831))
(<= (next (sat 1)) (does ?v493852 (assign 18 t)) (role ?v493852))
(<= (next (sat 2)) (does ?v493875 (assign 4 f)) (role ?v493875))
(<= (next (sat 2)) (does ?v493896 (assign 29 t)) (role ?v493896))
(<= (next (sat 2)) (does ?v493917 (assign 23 f)) (role ?v493917))
(<= (next (sat 2)) (does ?v493938 (assign 58 f)) (role ?v493938))
(<= (next (sat 2)) (does ?v493959 (assign 5 t)) (role ?v493959))
(<= (next (sat 3)) (does ?v493982 (assign 29 t)) (role ?v493982))
(<= (next (sat 3)) (does ?v494003 (assign 8 t)) (role ?v494003))
(<= (next (sat 3)) (does ?v494024 (assign 7 f)) (role ?v494024))
(<= (next (sat 3)) (does ?v494045 (assign 25 t)) (role ?v494045))
(<= (next (sat 3)) (does ?v494066 (assign 24 t)) (role ?v494066))
(<= (next (sat 4)) (does ?v494089 (assign 15 f)) (role ?v494089))
(<= (next (sat 4)) (does ?v494110 (assign 11 t)) (role ?v494110))
(<= (next (sat 4)) (does ?v494131 (assign 58 t)) (role ?v494131))
(<= (next (sat 4)) (does ?v494152 (assign 19 t)) (role ?v494152))
(<= (next (sat 4)) (does ?v494173 (assign 9 t)) (role ?v494173))
(<= (next (sat 5)) (does ?v494196 (assign 1 f)) (role ?v494196))
(<= (next (sat 5)) (does ?v494217 (assign 42 f)) (role ?v494217))
(<= (next (sat 5)) (does ?v494238 (assign 30 f)) (role ?v494238))
(<= (next (sat 5)) (does ?v494259 (assign 58 t)) (role ?v494259))
(<= (next (sat 5)) (does ?v494280 (assign 21 t)) (role ?v494280))
(<= (next (sat 6)) (does ?v494303 (assign 33 f)) (role ?v494303))
(<= (next (sat 6)) (does ?v494324 (assign 39 t)) (role ?v494324))
(<= (next (sat 6)) (does ?v494345 (assign 59 t)) (role ?v494345))
(<= (next (sat 6)) (does ?v494366 (assign 60 t)) (role ?v494366))
(<= (next (sat 6)) (does ?v494387 (assign 29 f)) (role ?v494387))
(<= (next (sat 7)) (does ?v494410 (assign 9 f)) (role ?v494410))
(<= (next (sat 7)) (does ?v494431 (assign 20 t)) (role ?v494431))
(<= (next (sat 7)) (does ?v494452 (assign 34 f)) (role ?v494452))
(<= (next (sat 7)) (does ?v494473 (assign 29 t)) (role ?v494473))
(<= (next (sat 7)) (does ?v494494 (assign 3 t)) (role ?v494494))
(<= (next (sat 8)) (does ?v494517 (assign 56 f)) (role ?v494517))
(<= (next (sat 8)) (does ?v494538 (assign 28 f)) (role ?v494538))
(<= (next (sat 8)) (does ?v494559 (assign 17 t)) (role ?v494559))
(<= (next (sat 8)) (does ?v494580 (assign 1 t)) (role ?v494580))
(<= (next (sat 8)) (does ?v494601 (assign 51 f)) (role ?v494601))
(<= (next (sat 9)) (does ?v494624 (assign 17 t)) (role ?v494624))
(<= (next (sat 9)) (does ?v494645 (assign 49 f)) (role ?v494645))
(<= (next (sat 9)) (does ?v494666 (assign 27 t)) (role ?v494666))
(<= (next (sat 9)) (does ?v494687 (assign 24 f)) (role ?v494687))
(<= (next (sat 9)) (does ?v494708 (assign 56 t)) (role ?v494708))
(<= (next (sat 10)) (does ?v494731 (assign 47 f)) (role ?v494731))
(<= (next (sat 10)) (does ?v494752 (assign 34 f)) (role ?v494752))
(<= (next (sat 10)) (does ?v494773 (assign 26 f)) (role ?v494773))
(<= (next (sat 10)) (does ?v494794 (assign 20 f)) (role ?v494794))
(<= (next (sat 10)) (does ?v494815 (assign 39 t)) (role ?v494815))
(<= (next (sat 11)) (does ?v494838 (assign 17 f)) (role ?v494838))
(<= (next (sat 11)) (does ?v494859 (assign 20 f)) (role ?v494859))
(<= (next (sat 11)) (does ?v494880 (assign 48 t)) (role ?v494880))
(<= (next (sat 11)) (does ?v494901 (assign 10 f)) (role ?v494901))
(<= (next (sat 11)) (does ?v494922 (assign 8 t)) (role ?v494922))
(<= (next (sat 12)) (does ?v494945 (assign 24 f)) (role ?v494945))
(<= (next (sat 12)) (does ?v494966 (assign 52 f)) (role ?v494966))
(<= (next (sat 12)) (does ?v494987 (assign 13 t)) (role ?v494987))
(<= (next (sat 12)) (does ?v495008 (assign 20 t)) (role ?v495008))
(<= (next (sat 12)) (does ?v495029 (assign 26 f)) (role ?v495029))
(<= (next (sat 13)) (does ?v495052 (assign 57 f)) (role ?v495052))
(<= (next (sat 13)) (does ?v495073 (assign 30 t)) (role ?v495073))
(<= (next (sat 13)) (does ?v495094 (assign 36 t)) (role ?v495094))
(<= (next (sat 13)) (does ?v495115 (assign 46 f)) (role ?v495115))
(<= (next (sat 13)) (does ?v495136 (assign 43 t)) (role ?v495136))
(<= (next (sat 14)) (does ?v495159 (assign 1 t)) (role ?v495159))
(<= (next (sat 14)) (does ?v495180 (assign 28 t)) (role ?v495180))
(<= (next (sat 14)) (does ?v495201 (assign 21 f)) (role ?v495201))
(<= (next (sat 14)) (does ?v495222 (assign 2 t)) (role ?v495222))
(<= (next (sat 14)) (does ?v495243 (assign 23 f)) (role ?v495243))
(<= (next (sat 15)) (does ?v495266 (assign 33 f)) (role ?v495266))
(<= (next (sat 15)) (does ?v495287 (assign 30 f)) (role ?v495287))
(<= (next (sat 15)) (does ?v495308 (assign 3 f)) (role ?v495308))
(<= (next (sat 15)) (does ?v495329 (assign 41 t)) (role ?v495329))
(<= (next (sat 15)) (does ?v495350 (assign 32 f)) (role ?v495350))
(<= (next (sat 16)) (does ?v495373 (assign 52 t)) (role ?v495373))
(<= (next (sat 16)) (does ?v495394 (assign 41 f)) (role ?v495394))
(<= (next (sat 16)) (does ?v495415 (assign 49 t)) (role ?v495415))
(<= (next (sat 16)) (does ?v495436 (assign 60 t)) (role ?v495436))
(<= (next (sat 16)) (does ?v495457 (assign 34 t)) (role ?v495457))
(<= (next (sat 17)) (does ?v495480 (assign 57 f)) (role ?v495480))
(<= (next (sat 17)) (does ?v495501 (assign 28 t)) (role ?v495501))
(<= (next (sat 17)) (does ?v495522 (assign 23 t)) (role ?v495522))
(<= (next (sat 17)) (does ?v495543 (assign 50 f)) (role ?v495543))
(<= (next (sat 17)) (does ?v495564 (assign 59 t)) (role ?v495564))
(<= (next (sat 18)) (does ?v495587 (assign 41 t)) (role ?v495587))
(<= (next (sat 18)) (does ?v495608 (assign 38 f)) (role ?v495608))
(<= (next (sat 18)) (does ?v495629 (assign 5 t)) (role ?v495629))
(<= (next (sat 18)) (does ?v495650 (assign 35 f)) (role ?v495650))
(<= (next (sat 18)) (does ?v495671 (assign 11 t)) (role ?v495671))
(<= (next (sat 19)) (does ?v495694 (assign 45 f)) (role ?v495694))
(<= (next (sat 19)) (does ?v495715 (assign 53 t)) (role ?v495715))
(<= (next (sat 19)) (does ?v495736 (assign 33 t)) (role ?v495736))
(<= (next (sat 19)) (does ?v495757 (assign 52 t)) (role ?v495757))
(<= (next (sat 19)) (does ?v495778 (assign 8 t)) (role ?v495778))
(<= (next (sat 20)) (does ?v495801 (assign 19 f)) (role ?v495801))
(<= (next (sat 20)) (does ?v495822 (assign 3 f)) (role ?v495822))
(<= (next (sat 20)) (does ?v495843 (assign 49 f)) (role ?v495843))
(<= (next (sat 20)) (does ?v495864 (assign 23 f)) (role ?v495864))
(<= (next (sat 20)) (does ?v495885 (assign 40 t)) (role ?v495885))
(<= (next (sat 21)) (does ?v495908 (assign 29 t)) (role ?v495908))
(<= (next (sat 21)) (does ?v495929 (assign 9 f)) (role ?v495929))
(<= (next (sat 21)) (does ?v495950 (assign 25 t)) (role ?v495950))
(<= (next (sat 21)) (does ?v495971 (assign 45 t)) (role ?v495971))
(<= (next (sat 21)) (does ?v495992 (assign 24 f)) (role ?v495992))
(<= (next (sat 22)) (does ?v496015 (assign 33 f)) (role ?v496015))
(<= (next (sat 22)) (does ?v496036 (assign 36 t)) (role ?v496036))
(<= (next (sat 22)) (does ?v496057 (assign 51 f)) (role ?v496057))
(<= (next (sat 22)) (does ?v496078 (assign 34 t)) (role ?v496078))
(<= (next (sat 22)) (does ?v496099 (assign 46 t)) (role ?v496099))
(<= (next (sat 23)) (does ?v496122 (assign 22 t)) (role ?v496122))
(<= (next (sat 23)) (does ?v496143 (assign 55 t)) (role ?v496143))
(<= (next (sat 23)) (does ?v496164 (assign 51 t)) (role ?v496164))
(<= (next (sat 23)) (does ?v496185 (assign 20 f)) (role ?v496185))
(<= (next (sat 23)) (does ?v496206 (assign 47 f)) (role ?v496206))
(<= (next (sat 24)) (does ?v496229 (assign 6 f)) (role ?v496229))
(<= (next (sat 24)) (does ?v496250 (assign 58 f)) (role ?v496250))
(<= (next (sat 24)) (does ?v496271 (assign 26 f)) (role ?v496271))
(<= (next (sat 24)) (does ?v496292 (assign 38 f)) (role ?v496292))
(<= (next (sat 24)) (does ?v496313 (assign 31 f)) (role ?v496313))
(<= (next (sat 25)) (does ?v496336 (assign 5 f)) (role ?v496336))
(<= (next (sat 25)) (does ?v496357 (assign 29 t)) (role ?v496357))
(<= (next (sat 25)) (does ?v496378 (assign 59 f)) (role ?v496378))
(<= (next (sat 25)) (does ?v496399 (assign 53 t)) (role ?v496399))
(<= (next (sat 25)) (does ?v496420 (assign 25 t)) (role ?v496420))
(<= (next (sat 26)) (does ?v496443 (assign 19 f)) (role ?v496443))
(<= (next (sat 26)) (does ?v496464 (assign 2 f)) (role ?v496464))
(<= (next (sat 26)) (does ?v496485 (assign 42 t)) (role ?v496485))
(<= (next (sat 26)) (does ?v496506 (assign 23 f)) (role ?v496506))
(<= (next (sat 26)) (does ?v496527 (assign 22 f)) (role ?v496527))
(<= (next (sat 27)) (does ?v496550 (assign 41 t)) (role ?v496550))
(<= (next (sat 27)) (does ?v496571 (assign 29 f)) (role ?v496571))
(<= (next (sat 27)) (does ?v496592 (assign 56 f)) (role ?v496592))
(<= (next (sat 27)) (does ?v496613 (assign 11 t)) (role ?v496613))
(<= (next (sat 27)) (does ?v496634 (assign 52 f)) (role ?v496634))
(<= (next (sat 28)) (does ?v496657 (assign 41 f)) (role ?v496657))
(<= (next (sat 28)) (does ?v496678 (assign 13 t)) (role ?v496678))
(<= (next (sat 28)) (does ?v496699 (assign 51 f)) (role ?v496699))
(<= (next (sat 28)) (does ?v496720 (assign 47 f)) (role ?v496720))
(<= (next (sat 28)) (does ?v496741 (assign 14 f)) (role ?v496741))
(<= (next (sat 29)) (does ?v496764 (assign 51 f)) (role ?v496764))
(<= (next (sat 29)) (does ?v496785 (assign 24 f)) (role ?v496785))
(<= (next (sat 29)) (does ?v496806 (assign 60 f)) (role ?v496806))
(<= (next (sat 29)) (does ?v496827 (assign 53 f)) (role ?v496827))
(<= (next (sat 29)) (does ?v496848 (assign 25 t)) (role ?v496848))
(<= (next (sat 30)) (does ?v496871 (assign 16 f)) (role ?v496871))
(<= (next (sat 30)) (does ?v496892 (assign 39 f)) (role ?v496892))
(<= (next (sat 30)) (does ?v496913 (assign 49 f)) (role ?v496913))
(<= (next (sat 30)) (does ?v496934 (assign 51 t)) (role ?v496934))
(<= (next (sat 30)) (does ?v496955 (assign 40 f)) (role ?v496955))
(<= (next (sat 31)) (does ?v496978 (assign 33 f)) (role ?v496978))
(<= (next (sat 31)) (does ?v496999 (assign 15 t)) (role ?v496999))
(<= (next (sat 31)) (does ?v497020 (assign 36 t)) (role ?v497020))
(<= (next (sat 31)) (does ?v497041 (assign 44 t)) (role ?v497041))
(<= (next (sat 31)) (does ?v497062 (assign 60 t)) (role ?v497062))
(<= (next (sat 32)) (does ?v497085 (assign 60 f)) (role ?v497085))
(<= (next (sat 32)) (does ?v497106 (assign 25 f)) (role ?v497106))
(<= (next (sat 32)) (does ?v497127 (assign 57 t)) (role ?v497127))
(<= (next (sat 32)) (does ?v497148 (assign 24 t)) (role ?v497148))
(<= (next (sat 32)) (does ?v497169 (assign 14 t)) (role ?v497169))
(<= (next (sat 33)) (does ?v497192 (assign 26 t)) (role ?v497192))
(<= (next (sat 33)) (does ?v497213 (assign 49 f)) (role ?v497213))
(<= (next (sat 33)) (does ?v497234 (assign 55 t)) (role ?v497234))
(<= (next (sat 33)) (does ?v497255 (assign 52 t)) (role ?v497255))
(<= (next (sat 33)) (does ?v497276 (assign 42 t)) (role ?v497276))
(<= (next (sat 34)) (does ?v497299 (assign 36 t)) (role ?v497299))
(<= (next (sat 34)) (does ?v497320 (assign 6 f)) (role ?v497320))
(<= (next (sat 34)) (does ?v497341 (assign 51 t)) (role ?v497341))
(<= (next (sat 34)) (does ?v497362 (assign 56 t)) (role ?v497362))
(<= (next (sat 34)) (does ?v497383 (assign 24 t)) (role ?v497383))
(<= (next (sat 35)) (does ?v497406 (assign 6 f)) (role ?v497406))
(<= (next (sat 35)) (does ?v497427 (assign 31 t)) (role ?v497427))
(<= (next (sat 35)) (does ?v497448 (assign 18 t)) (role ?v497448))
(<= (next (sat 35)) (does ?v497469 (assign 36 f)) (role ?v497469))
(<= (next (sat 35)) (does ?v497490 (assign 37 t)) (role ?v497490))
(<= (next (sat 36)) (does ?v497513 (assign 33 t)) (role ?v497513))
(<= (next (sat 36)) (does ?v497534 (assign 46 f)) (role ?v497534))
(<= (next (sat 36)) (does ?v497555 (assign 5 t)) (role ?v497555))
(<= (next (sat 36)) (does ?v497576 (assign 20 f)) (role ?v497576))
(<= (next (sat 36)) (does ?v497597 (assign 22 f)) (role ?v497597))
(<= (next (sat 37)) (does ?v497620 (assign 47 f)) (role ?v497620))
(<= (next (sat 37)) (does ?v497641 (assign 27 t)) (role ?v497641))
(<= (next (sat 37)) (does ?v497662 (assign 32 t)) (role ?v497662))
(<= (next (sat 37)) (does ?v497683 (assign 14 f)) (role ?v497683))
(<= (next (sat 37)) (does ?v497704 (assign 52 t)) (role ?v497704))
(<= (next (sat 38)) (does ?v497727 (assign 53 t)) (role ?v497727))
(<= (next (sat 38)) (does ?v497748 (assign 43 t)) (role ?v497748))
(<= (next (sat 38)) (does ?v497769 (assign 58 f)) (role ?v497769))
(<= (next (sat 38)) (does ?v497790 (assign 50 t)) (role ?v497790))
(<= (next (sat 38)) (does ?v497811 (assign 42 f)) (role ?v497811))
(<= (next (sat 39)) (does ?v497834 (assign 6 f)) (role ?v497834))
(<= (next (sat 39)) (does ?v497855 (assign 13 t)) (role ?v497855))
(<= (next (sat 39)) (does ?v497876 (assign 43 t)) (role ?v497876))
(<= (next (sat 39)) (does ?v497897 (assign 31 t)) (role ?v497897))
(<= (next (sat 39)) (does ?v497918 (assign 22 f)) (role ?v497918))
(<= (next (sat 40)) (does ?v497941 (assign 38 t)) (role ?v497941))
(<= (next (sat 40)) (does ?v497962 (assign 2 t)) (role ?v497962))
(<= (next (sat 40)) (does ?v497983 (assign 16 t)) (role ?v497983))
(<= (next (sat 40)) (does ?v498004 (assign 51 t)) (role ?v498004))
(<= (next (sat 40)) (does ?v498025 (assign 26 f)) (role ?v498025))
(<= 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))