You are not logged in. login register
Game 3qbf-5cnf-20var-40cl.1.qdimacs.viz.SAT
name 3qbf-5cnf-20var-40cl.1.qdimacs.viz.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 (not 1))
(contains 1 52)
(contains 1 16)
(contains 1 4)
(contains 1 (not 27))
(contains 2 (not 27))
(contains 2 (not 51))
(contains 2 19)
(contains 2 1)
(contains 2 30)
(contains 3 35)
(contains 3 52)
(contains 3 (not 41))
(contains 3 (not 18))
(contains 3 (not 59))
(contains 4 24)
(contains 4 30)
(contains 4 20)
(contains 4 (not 7))
(contains 4 (not 23))
(contains 5 (not 34))
(contains 5 (not 4))
(contains 5 13)
(contains 5 (not 49))
(contains 5 (not 17))
(contains 6 51)
(contains 6 (not 37))
(contains 6 1)
(contains 6 5)
(contains 6 (not 29))
(contains 7 (not 2))
(contains 7 (not 7))
(contains 7 (not 53))
(contains 7 (not 12))
(contains 7 (not 35))
(contains 8 (not 39))
(contains 8 (not 44))
(contains 8 28)
(contains 8 (not 2))
(contains 8 51)
(contains 9 (not 21))
(contains 9 (not 11))
(contains 9 8)
(contains 9 (not 20))
(contains 9 2)
(contains 10 (not 37))
(contains 10 (not 21))
(contains 10 58)
(contains 10 (not 59))
(contains 10 7)
(contains 11 33)
(contains 11 59)
(contains 11 (not 41))
(contains 11 52)
(contains 11 21)
(contains 12 43)
(contains 12 35)
(contains 12 (not 7))
(contains 12 33)
(contains 12 50)
(contains 13 29)
(contains 13 45)
(contains 13 (not 14))
(contains 13 25)
(contains 13 24)
(contains 14 (not 21))
(contains 14 54)
(contains 14 49)
(contains 14 2)
(contains 14 42)
(contains 15 (not 25))
(contains 15 7)
(contains 15 (not 43))
(contains 15 (not 39))
(contains 15 59)
(contains 16 32)
(contains 16 (not 30))
(contains 16 14)
(contains 16 17)
(contains 16 51)
(contains 17 (not 9))
(contains 17 44)
(contains 17 (not 3))
(contains 17 4)
(contains 17 (not 54))
(contains 18 (not 46))
(contains 18 48)
(contains 18 55)
(contains 18 (not 6))
(contains 18 59)
(contains 19 51)
(contains 19 (not 12))
(contains 19 1)
(contains 19 52)
(contains 19 58)
(contains 20 (not 8))
(contains 20 47)
(contains 20 19)
(contains 20 (not 42))
(contains 20 (not 12))
(contains 21 (not 39))
(contains 21 11)
(contains 21 1)
(contains 21 (not 41))
(contains 21 (not 31))
(contains 22 (not 26))
(contains 22 34)
(contains 22 9)
(contains 22 (not 35))
(contains 22 41)
(contains 23 54)
(contains 23 26)
(contains 23 (not 47))
(contains 23 31)
(contains 23 (not 36))
(contains 24 (not 15))
(contains 24 (not 60))
(contains 24 (not 13))
(contains 24 6)
(contains 24 47)
(contains 25 (not 21))
(contains 25 (not 10))
(contains 25 26)
(contains 25 33)
(contains 25 15)
(contains 26 (not 20))
(contains 26 11)
(contains 26 49)
(contains 26 12)
(contains 26 (not 41))
(contains 27 (not 3))
(contains 27 53)
(contains 27 15)
(contains 27 (not 23))
(contains 27 58)
(contains 28 (not 3))
(contains 28 (not 48))
(contains 28 (not 21))
(contains 28 59)
(contains 28 46)
(contains 29 28)
(contains 29 25)
(contains 29 (not 10))
(contains 29 18)
(contains 29 4)
(contains 30 (not 55))
(contains 30 7)
(contains 30 (not 44))
(contains 30 22)
(contains 30 (not 32))
(contains 31 (not 12))
(contains 31 (not 35))
(contains 31 (not 48))
(contains 31 (not 14))
(contains 31 (not 39))
(contains 32 13)
(contains 32 (not 45))
(contains 32 49)
(contains 32 (not 35))
(contains 32 60)
(contains 33 (not 60))
(contains 33 27)
(contains 33 (not 19))
(contains 33 (not 25))
(contains 33 29)
(contains 34 (not 12))
(contains 34 43)
(contains 34 3)
(contains 34 (not 5))
(contains 34 30)
(contains 35 (not 9))
(contains 35 50)
(contains 35 (not 19))
(contains 35 (not 59))
(contains 35 (not 2))
(contains 36 (not 20))
(contains 36 14)
(contains 36 (not 58))
(contains 36 (not 12))
(contains 36 (not 34))
(contains 37 22)
(contains 37 (not 16))
(contains 37 (not 4))
(contains 37 (not 14))
(contains 37 52)
(contains 38 (not 45))
(contains 38 (not 13))
(contains 38 47)
(contains 38 (not 12))
(contains 38 15)
(contains 39 (not 50))
(contains 39 60)
(contains 39 9)
(contains 39 (not 4))
(contains 39 18)
(contains 40 (not 10))
(contains 40 (not 54))
(contains 40 (not 15))
(contains 40 47)
(contains 40 (not 22))
(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 ?v5689 (assign ?v5699 ?v5700)) (true (control ?v5689 ?v5699)) (role ?v5689) (prop_var ?v5699) (truth_value ?v5700))
(<= (legal exists noop) (true (control forall ?v5735)) (prop_var ?v5735))
(<= (legal forall noop) (true (control exists ?v5735)) (prop_var ?v5735))
(<= (next (sat ?v5759)) (true (sat ?v5759)) (clause ?v5759))
(<= (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 ?v9608 (assign 1 f)) (role ?v9608))
(<= (next (sat 1)) (does ?v9629 (assign 52 t)) (role ?v9629))
(<= (next (sat 1)) (does ?v9650 (assign 16 t)) (role ?v9650))
(<= (next (sat 1)) (does ?v9671 (assign 4 t)) (role ?v9671))
(<= (next (sat 1)) (does ?v9692 (assign 27 f)) (role ?v9692))
(<= (next (sat 2)) (does ?v9715 (assign 27 f)) (role ?v9715))
(<= (next (sat 2)) (does ?v9736 (assign 51 f)) (role ?v9736))
(<= (next (sat 2)) (does ?v9757 (assign 19 t)) (role ?v9757))
(<= (next (sat 2)) (does ?v9778 (assign 1 t)) (role ?v9778))
(<= (next (sat 2)) (does ?v9799 (assign 30 t)) (role ?v9799))
(<= (next (sat 3)) (does ?v9822 (assign 35 t)) (role ?v9822))
(<= (next (sat 3)) (does ?v9843 (assign 52 t)) (role ?v9843))
(<= (next (sat 3)) (does ?v9864 (assign 41 f)) (role ?v9864))
(<= (next (sat 3)) (does ?v9885 (assign 18 f)) (role ?v9885))
(<= (next (sat 3)) (does ?v9906 (assign 59 f)) (role ?v9906))
(<= (next (sat 4)) (does ?v9929 (assign 24 t)) (role ?v9929))
(<= (next (sat 4)) (does ?v9950 (assign 30 t)) (role ?v9950))
(<= (next (sat 4)) (does ?v9971 (assign 20 t)) (role ?v9971))
(<= (next (sat 4)) (does ?v9992 (assign 7 f)) (role ?v9992))
(<= (next (sat 4)) (does ?v10013 (assign 23 f)) (role ?v10013))
(<= (next (sat 5)) (does ?v10036 (assign 34 f)) (role ?v10036))
(<= (next (sat 5)) (does ?v10057 (assign 4 f)) (role ?v10057))
(<= (next (sat 5)) (does ?v10078 (assign 13 t)) (role ?v10078))
(<= (next (sat 5)) (does ?v10099 (assign 49 f)) (role ?v10099))
(<= (next (sat 5)) (does ?v10120 (assign 17 f)) (role ?v10120))
(<= (next (sat 6)) (does ?v10143 (assign 51 t)) (role ?v10143))
(<= (next (sat 6)) (does ?v10164 (assign 37 f)) (role ?v10164))
(<= (next (sat 6)) (does ?v10185 (assign 1 t)) (role ?v10185))
(<= (next (sat 6)) (does ?v10206 (assign 5 t)) (role ?v10206))
(<= (next (sat 6)) (does ?v10227 (assign 29 f)) (role ?v10227))
(<= (next (sat 7)) (does ?v10250 (assign 2 f)) (role ?v10250))
(<= (next (sat 7)) (does ?v10271 (assign 7 f)) (role ?v10271))
(<= (next (sat 7)) (does ?v10292 (assign 53 f)) (role ?v10292))
(<= (next (sat 7)) (does ?v10313 (assign 12 f)) (role ?v10313))
(<= (next (sat 7)) (does ?v10334 (assign 35 f)) (role ?v10334))
(<= (next (sat 8)) (does ?v10357 (assign 39 f)) (role ?v10357))
(<= (next (sat 8)) (does ?v10378 (assign 44 f)) (role ?v10378))
(<= (next (sat 8)) (does ?v10399 (assign 28 t)) (role ?v10399))
(<= (next (sat 8)) (does ?v10420 (assign 2 f)) (role ?v10420))
(<= (next (sat 8)) (does ?v10441 (assign 51 t)) (role ?v10441))
(<= (next (sat 9)) (does ?v10464 (assign 21 f)) (role ?v10464))
(<= (next (sat 9)) (does ?v10485 (assign 11 f)) (role ?v10485))
(<= (next (sat 9)) (does ?v10506 (assign 8 t)) (role ?v10506))
(<= (next (sat 9)) (does ?v10527 (assign 20 f)) (role ?v10527))
(<= (next (sat 9)) (does ?v10548 (assign 2 t)) (role ?v10548))
(<= (next (sat 10)) (does ?v10571 (assign 37 f)) (role ?v10571))
(<= (next (sat 10)) (does ?v10592 (assign 21 f)) (role ?v10592))
(<= (next (sat 10)) (does ?v10613 (assign 58 t)) (role ?v10613))
(<= (next (sat 10)) (does ?v10634 (assign 59 f)) (role ?v10634))
(<= (next (sat 10)) (does ?v10655 (assign 7 t)) (role ?v10655))
(<= (next (sat 11)) (does ?v10678 (assign 33 t)) (role ?v10678))
(<= (next (sat 11)) (does ?v10699 (assign 59 t)) (role ?v10699))
(<= (next (sat 11)) (does ?v10720 (assign 41 f)) (role ?v10720))
(<= (next (sat 11)) (does ?v10741 (assign 52 t)) (role ?v10741))
(<= (next (sat 11)) (does ?v10762 (assign 21 t)) (role ?v10762))
(<= (next (sat 12)) (does ?v10785 (assign 43 t)) (role ?v10785))
(<= (next (sat 12)) (does ?v10806 (assign 35 t)) (role ?v10806))
(<= (next (sat 12)) (does ?v10827 (assign 7 f)) (role ?v10827))
(<= (next (sat 12)) (does ?v10848 (assign 33 t)) (role ?v10848))
(<= (next (sat 12)) (does ?v10869 (assign 50 t)) (role ?v10869))
(<= (next (sat 13)) (does ?v10892 (assign 29 t)) (role ?v10892))
(<= (next (sat 13)) (does ?v10913 (assign 45 t)) (role ?v10913))
(<= (next (sat 13)) (does ?v10934 (assign 14 f)) (role ?v10934))
(<= (next (sat 13)) (does ?v10955 (assign 25 t)) (role ?v10955))
(<= (next (sat 13)) (does ?v10976 (assign 24 t)) (role ?v10976))
(<= (next (sat 14)) (does ?v10999 (assign 21 f)) (role ?v10999))
(<= (next (sat 14)) (does ?v11020 (assign 54 t)) (role ?v11020))
(<= (next (sat 14)) (does ?v11041 (assign 49 t)) (role ?v11041))
(<= (next (sat 14)) (does ?v11062 (assign 2 t)) (role ?v11062))
(<= (next (sat 14)) (does ?v11083 (assign 42 t)) (role ?v11083))
(<= (next (sat 15)) (does ?v11106 (assign 25 f)) (role ?v11106))
(<= (next (sat 15)) (does ?v11127 (assign 7 t)) (role ?v11127))
(<= (next (sat 15)) (does ?v11148 (assign 43 f)) (role ?v11148))
(<= (next (sat 15)) (does ?v11169 (assign 39 f)) (role ?v11169))
(<= (next (sat 15)) (does ?v11190 (assign 59 t)) (role ?v11190))
(<= (next (sat 16)) (does ?v11213 (assign 32 t)) (role ?v11213))
(<= (next (sat 16)) (does ?v11234 (assign 30 f)) (role ?v11234))
(<= (next (sat 16)) (does ?v11255 (assign 14 t)) (role ?v11255))
(<= (next (sat 16)) (does ?v11276 (assign 17 t)) (role ?v11276))
(<= (next (sat 16)) (does ?v11297 (assign 51 t)) (role ?v11297))
(<= (next (sat 17)) (does ?v11320 (assign 9 f)) (role ?v11320))
(<= (next (sat 17)) (does ?v11341 (assign 44 t)) (role ?v11341))
(<= (next (sat 17)) (does ?v11362 (assign 3 f)) (role ?v11362))
(<= (next (sat 17)) (does ?v11383 (assign 4 t)) (role ?v11383))
(<= (next (sat 17)) (does ?v11404 (assign 54 f)) (role ?v11404))
(<= (next (sat 18)) (does ?v11427 (assign 46 f)) (role ?v11427))
(<= (next (sat 18)) (does ?v11448 (assign 48 t)) (role ?v11448))
(<= (next (sat 18)) (does ?v11469 (assign 55 t)) (role ?v11469))
(<= (next (sat 18)) (does ?v11490 (assign 6 f)) (role ?v11490))
(<= (next (sat 18)) (does ?v11511 (assign 59 t)) (role ?v11511))
(<= (next (sat 19)) (does ?v11534 (assign 51 t)) (role ?v11534))
(<= (next (sat 19)) (does ?v11555 (assign 12 f)) (role ?v11555))
(<= (next (sat 19)) (does ?v11576 (assign 1 t)) (role ?v11576))
(<= (next (sat 19)) (does ?v11597 (assign 52 t)) (role ?v11597))
(<= (next (sat 19)) (does ?v11618 (assign 58 t)) (role ?v11618))
(<= (next (sat 20)) (does ?v11641 (assign 8 f)) (role ?v11641))
(<= (next (sat 20)) (does ?v11662 (assign 47 t)) (role ?v11662))
(<= (next (sat 20)) (does ?v11683 (assign 19 t)) (role ?v11683))
(<= (next (sat 20)) (does ?v11704 (assign 42 f)) (role ?v11704))
(<= (next (sat 20)) (does ?v11725 (assign 12 f)) (role ?v11725))
(<= (next (sat 21)) (does ?v11748 (assign 39 f)) (role ?v11748))
(<= (next (sat 21)) (does ?v11769 (assign 11 t)) (role ?v11769))
(<= (next (sat 21)) (does ?v11790 (assign 1 t)) (role ?v11790))
(<= (next (sat 21)) (does ?v11811 (assign 41 f)) (role ?v11811))
(<= (next (sat 21)) (does ?v11832 (assign 31 f)) (role ?v11832))
(<= (next (sat 22)) (does ?v11855 (assign 26 f)) (role ?v11855))
(<= (next (sat 22)) (does ?v11876 (assign 34 t)) (role ?v11876))
(<= (next (sat 22)) (does ?v11897 (assign 9 t)) (role ?v11897))
(<= (next (sat 22)) (does ?v11918 (assign 35 f)) (role ?v11918))
(<= (next (sat 22)) (does ?v11939 (assign 41 t)) (role ?v11939))
(<= (next (sat 23)) (does ?v11962 (assign 54 t)) (role ?v11962))
(<= (next (sat 23)) (does ?v11983 (assign 26 t)) (role ?v11983))
(<= (next (sat 23)) (does ?v12004 (assign 47 f)) (role ?v12004))
(<= (next (sat 23)) (does ?v12025 (assign 31 t)) (role ?v12025))
(<= (next (sat 23)) (does ?v12046 (assign 36 f)) (role ?v12046))
(<= (next (sat 24)) (does ?v12069 (assign 15 f)) (role ?v12069))
(<= (next (sat 24)) (does ?v12090 (assign 60 f)) (role ?v12090))
(<= (next (sat 24)) (does ?v12111 (assign 13 f)) (role ?v12111))
(<= (next (sat 24)) (does ?v12132 (assign 6 t)) (role ?v12132))
(<= (next (sat 24)) (does ?v12153 (assign 47 t)) (role ?v12153))
(<= (next (sat 25)) (does ?v12176 (assign 21 f)) (role ?v12176))
(<= (next (sat 25)) (does ?v12197 (assign 10 f)) (role ?v12197))
(<= (next (sat 25)) (does ?v12218 (assign 26 t)) (role ?v12218))
(<= (next (sat 25)) (does ?v12239 (assign 33 t)) (role ?v12239))
(<= (next (sat 25)) (does ?v12260 (assign 15 t)) (role ?v12260))
(<= (next (sat 26)) (does ?v12283 (assign 20 f)) (role ?v12283))
(<= (next (sat 26)) (does ?v12304 (assign 11 t)) (role ?v12304))
(<= (next (sat 26)) (does ?v12325 (assign 49 t)) (role ?v12325))
(<= (next (sat 26)) (does ?v12346 (assign 12 t)) (role ?v12346))
(<= (next (sat 26)) (does ?v12367 (assign 41 f)) (role ?v12367))
(<= (next (sat 27)) (does ?v12390 (assign 3 f)) (role ?v12390))
(<= (next (sat 27)) (does ?v12411 (assign 53 t)) (role ?v12411))
(<= (next (sat 27)) (does ?v12432 (assign 15 t)) (role ?v12432))
(<= (next (sat 27)) (does ?v12453 (assign 23 f)) (role ?v12453))
(<= (next (sat 27)) (does ?v12474 (assign 58 t)) (role ?v12474))
(<= (next (sat 28)) (does ?v12497 (assign 3 f)) (role ?v12497))
(<= (next (sat 28)) (does ?v12518 (assign 48 f)) (role ?v12518))
(<= (next (sat 28)) (does ?v12539 (assign 21 f)) (role ?v12539))
(<= (next (sat 28)) (does ?v12560 (assign 59 t)) (role ?v12560))
(<= (next (sat 28)) (does ?v12581 (assign 46 t)) (role ?v12581))
(<= (next (sat 29)) (does ?v12604 (assign 28 t)) (role ?v12604))
(<= (next (sat 29)) (does ?v12625 (assign 25 t)) (role ?v12625))
(<= (next (sat 29)) (does ?v12646 (assign 10 f)) (role ?v12646))
(<= (next (sat 29)) (does ?v12667 (assign 18 t)) (role ?v12667))
(<= (next (sat 29)) (does ?v12688 (assign 4 t)) (role ?v12688))
(<= (next (sat 30)) (does ?v12711 (assign 55 f)) (role ?v12711))
(<= (next (sat 30)) (does ?v12732 (assign 7 t)) (role ?v12732))
(<= (next (sat 30)) (does ?v12753 (assign 44 f)) (role ?v12753))
(<= (next (sat 30)) (does ?v12774 (assign 22 t)) (role ?v12774))
(<= (next (sat 30)) (does ?v12795 (assign 32 f)) (role ?v12795))
(<= (next (sat 31)) (does ?v12818 (assign 12 f)) (role ?v12818))
(<= (next (sat 31)) (does ?v12839 (assign 35 f)) (role ?v12839))
(<= (next (sat 31)) (does ?v12860 (assign 48 f)) (role ?v12860))
(<= (next (sat 31)) (does ?v12881 (assign 14 f)) (role ?v12881))
(<= (next (sat 31)) (does ?v12902 (assign 39 f)) (role ?v12902))
(<= (next (sat 32)) (does ?v12925 (assign 13 t)) (role ?v12925))
(<= (next (sat 32)) (does ?v12946 (assign 45 f)) (role ?v12946))
(<= (next (sat 32)) (does ?v12967 (assign 49 t)) (role ?v12967))
(<= (next (sat 32)) (does ?v12988 (assign 35 f)) (role ?v12988))
(<= (next (sat 32)) (does ?v13009 (assign 60 t)) (role ?v13009))
(<= (next (sat 33)) (does ?v13032 (assign 60 f)) (role ?v13032))
(<= (next (sat 33)) (does ?v13053 (assign 27 t)) (role ?v13053))
(<= (next (sat 33)) (does ?v13074 (assign 19 f)) (role ?v13074))
(<= (next (sat 33)) (does ?v13095 (assign 25 f)) (role ?v13095))
(<= (next (sat 33)) (does ?v13116 (assign 29 t)) (role ?v13116))
(<= (next (sat 34)) (does ?v13139 (assign 12 f)) (role ?v13139))
(<= (next (sat 34)) (does ?v13160 (assign 43 t)) (role ?v13160))
(<= (next (sat 34)) (does ?v13181 (assign 3 t)) (role ?v13181))
(<= (next (sat 34)) (does ?v13202 (assign 5 f)) (role ?v13202))
(<= (next (sat 34)) (does ?v13223 (assign 30 t)) (role ?v13223))
(<= (next (sat 35)) (does ?v13246 (assign 9 f)) (role ?v13246))
(<= (next (sat 35)) (does ?v13267 (assign 50 t)) (role ?v13267))
(<= (next (sat 35)) (does ?v13288 (assign 19 f)) (role ?v13288))
(<= (next (sat 35)) (does ?v13309 (assign 59 f)) (role ?v13309))
(<= (next (sat 35)) (does ?v13330 (assign 2 f)) (role ?v13330))
(<= (next (sat 36)) (does ?v13353 (assign 20 f)) (role ?v13353))
(<= (next (sat 36)) (does ?v13374 (assign 14 t)) (role ?v13374))
(<= (next (sat 36)) (does ?v13395 (assign 58 f)) (role ?v13395))
(<= (next (sat 36)) (does ?v13416 (assign 12 f)) (role ?v13416))
(<= (next (sat 36)) (does ?v13437 (assign 34 f)) (role ?v13437))
(<= (next (sat 37)) (does ?v13460 (assign 22 t)) (role ?v13460))
(<= (next (sat 37)) (does ?v13481 (assign 16 f)) (role ?v13481))
(<= (next (sat 37)) (does ?v13502 (assign 4 f)) (role ?v13502))
(<= (next (sat 37)) (does ?v13523 (assign 14 f)) (role ?v13523))
(<= (next (sat 37)) (does ?v13544 (assign 52 t)) (role ?v13544))
(<= (next (sat 38)) (does ?v13567 (assign 45 f)) (role ?v13567))
(<= (next (sat 38)) (does ?v13588 (assign 13 f)) (role ?v13588))
(<= (next (sat 38)) (does ?v13609 (assign 47 t)) (role ?v13609))
(<= (next (sat 38)) (does ?v13630 (assign 12 f)) (role ?v13630))
(<= (next (sat 38)) (does ?v13651 (assign 15 t)) (role ?v13651))
(<= (next (sat 39)) (does ?v13674 (assign 50 f)) (role ?v13674))
(<= (next (sat 39)) (does ?v13695 (assign 60 t)) (role ?v13695))
(<= (next (sat 39)) (does ?v13716 (assign 9 t)) (role ?v13716))
(<= (next (sat 39)) (does ?v13737 (assign 4 f)) (role ?v13737))
(<= (next (sat 39)) (does ?v13758 (assign 18 t)) (role ?v13758))
(<= (next (sat 40)) (does ?v13781 (assign 10 f)) (role ?v13781))
(<= (next (sat 40)) (does ?v13802 (assign 54 f)) (role ?v13802))
(<= (next (sat 40)) (does ?v13823 (assign 15 f)) (role ?v13823))
(<= (next (sat 40)) (does ?v13844 (assign 47 t)) (role ?v13844))
(<= (next (sat 40)) (does ?v13865 (assign 22 f)) (role ?v13865))
(<= 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))