You are not logged in. login register
Game satlike_20v_91c
name satlike_20v_91c
creator stephan
number of roles 1
stylesheet sat/sat.xsl
GDL v1
enabled
matches show matches
statistics show game statistics
description

Game Description

(contains 1 4)
(contains 1 (not 18))
(contains 1 19)
(contains 2 3)
(contains 2 18)
(contains 2 (not 5))
(contains 3 (not 5))
(contains 3 (not 8))
(contains 3 (not 15))
(contains 4 (not 20))
(contains 4 7)
(contains 4 (not 16))
(contains 5 10)
(contains 5 (not 13))
(contains 5 (not 7))
(contains 6 (not 12))
(contains 6 (not 9))
(contains 6 17)
(contains 7 17)
(contains 7 19)
(contains 7 5)
(contains 8 (not 16))
(contains 8 9)
(contains 8 15)
(contains 9 11)
(contains 9 (not 5))
(contains 9 (not 14))
(contains 10 18)
(contains 10 (not 10))
(contains 10 13)
(contains 11 (not 3))
(contains 11 11)
(contains 11 12)
(contains 12 (not 6))
(contains 12 (not 17))
(contains 12 (not 8))
(contains 13 (not 18))
(contains 13 14)
(contains 13 1)
(contains 14 (not 19))
(contains 14 (not 15))
(contains 14 10)
(contains 15 12)
(contains 15 18)
(contains 15 (not 19))
(contains 16 (not 8))
(contains 16 4)
(contains 16 7)
(contains 17 (not 8))
(contains 17 (not 9))
(contains 17 4)
(contains 18 7)
(contains 18 17)
(contains 18 (not 15))
(contains 19 12)
(contains 19 (not 7))
(contains 19 (not 14))
(contains 20 (not 10))
(contains 20 (not 11))
(contains 20 8)
(contains 21 2)
(contains 21 (not 15))
(contains 21 (not 11))
(contains 22 9)
(contains 22 6)
(contains 22 1)
(contains 23 (not 11))
(contains 23 20)
(contains 23 (not 17))
(contains 24 9)
(contains 24 (not 15))
(contains 24 13)
(contains 25 12)
(contains 25 (not 7))
(contains 25 (not 17))
(contains 26 (not 18))
(contains 26 (not 2))
(contains 26 20)
(contains 27 20)
(contains 27 12)
(contains 27 4)
(contains 28 19)
(contains 28 11)
(contains 28 14)
(contains 29 (not 16))
(contains 29 18)
(contains 29 (not 4))
(contains 30 (not 1))
(contains 30 (not 17))
(contains 30 (not 19))
(contains 31 (not 13))
(contains 31 15)
(contains 31 10)
(contains 32 (not 12))
(contains 32 (not 14))
(contains 32 (not 13))
(contains 33 12)
(contains 33 (not 14))
(contains 33 (not 7))
(contains 34 (not 7))
(contains 34 16)
(contains 34 10)
(contains 35 6)
(contains 35 10)
(contains 35 7)
(contains 36 20)
(contains 36 14)
(contains 36 (not 16))
(contains 37 (not 19))
(contains 37 17)
(contains 37 11)
(contains 38 (not 7))
(contains 38 1)
(contains 38 (not 20))
(contains 39 (not 5))
(contains 39 12)
(contains 39 15)
(contains 40 (not 4))
(contains 40 (not 9))
(contains 40 (not 13))
(contains 41 12)
(contains 41 (not 11))
(contains 41 (not 7))
(contains 42 (not 5))
(contains 42 19)
(contains 42 (not 8))
(contains 43 1)
(contains 43 16)
(contains 43 17)
(contains 44 20)
(contains 44 (not 14))
(contains 44 (not 15))
(contains 45 13)
(contains 45 (not 4))
(contains 45 10)
(contains 46 14)
(contains 46 7)
(contains 46 10)
(contains 47 (not 5))
(contains 47 9)
(contains 47 20)
(contains 48 10)
(contains 48 1)
(contains 48 (not 19))
(contains 49 (not 16))
(contains 49 (not 15))
(contains 49 (not 1))
(contains 50 16)
(contains 50 3)
(contains 50 (not 11))
(contains 51 (not 15))
(contains 51 (not 10))
(contains 51 4)
(contains 52 4)
(contains 52 (not 15))
(contains 52 (not 3))
(contains 53 (not 10))
(contains 53 (not 16))
(contains 53 11)
(contains 54 (not 8))
(contains 54 12)
(contains 54 (not 5))
(contains 55 14)
(contains 55 (not 6))
(contains 55 12)
(contains 56 1)
(contains 56 6)
(contains 56 11)
(contains 57 (not 13))
(contains 57 (not 5))
(contains 57 (not 1))
(contains 58 (not 7))
(contains 58 (not 2))
(contains 58 12)
(contains 59 1)
(contains 59 (not 20))
(contains 59 19)
(contains 60 (not 2))
(contains 60 (not 13))
(contains 60 (not 8))
(contains 61 15)
(contains 61 18)
(contains 61 4)
(contains 62 (not 11))
(contains 62 14)
(contains 62 9)
(contains 63 (not 6))
(contains 63 (not 15))
(contains 63 (not 2))
(contains 64 5)
(contains 64 (not 12))
(contains 64 (not 15))
(contains 65 (not 6))
(contains 65 17)
(contains 65 5)
(contains 66 (not 13))
(contains 66 5)
(contains 66 (not 19))
(contains 67 20)
(contains 67 (not 1))
(contains 67 14)
(contains 68 9)
(contains 68 (not 17))
(contains 68 15)
(contains 69 (not 5))
(contains 69 19)
(contains 69 (not 18))
(contains 70 (not 12))
(contains 70 8)
(contains 70 (not 10))
(contains 71 (not 18))
(contains 71 14)
(contains 71 (not 4))
(contains 72 15)
(contains 72 (not 9))
(contains 72 13)
(contains 73 9)
(contains 73 (not 5))
(contains 73 (not 1))
(contains 74 10)
(contains 74 (not 19))
(contains 74 (not 14))
(contains 75 20)
(contains 75 9)
(contains 75 4)
(contains 76 (not 9))
(contains 76 (not 2))
(contains 76 19)
(contains 77 (not 5))
(contains 77 13)
(contains 77 (not 17))
(contains 78 2)
(contains 78 (not 10))
(contains 78 (not 18))
(contains 79 (not 18))
(contains 79 3)
(contains 79 11)
(contains 80 7)
(contains 80 (not 9))
(contains 80 17)
(contains 81 (not 15))
(contains 81 (not 6))
(contains 81 (not 3))
(contains 82 (not 2))
(contains 82 3)
(contains 82 (not 13))
(contains 83 12)
(contains 83 3)
(contains 83 (not 2))
(contains 84 (not 2))
(contains 84 (not 3))
(contains 84 17)
(contains 85 20)
(contains 85 (not 15))
(contains 85 (not 16))
(contains 86 (not 5))
(contains 86 (not 17))
(contains 86 (not 19))
(contains 87 (not 20))
(contains 87 (not 18))
(contains 87 11)
(contains 88 (not 9))
(contains 88 1)
(contains 88 (not 5))
(contains 89 (not 19))
(contains 89 9)
(contains 89 17)
(contains 90 12)
(contains 90 (not 2))
(contains 90 17)
(contains 91 4)
(contains 91 (not 16))
(contains 91 (not 5))
(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 ?v9794 (assign ?v9804 ?v9805)) (true (control ?v9794 ?v9804)) (role ?v9794) (prop_var ?v9804) (truth_value ?v9805))
(<= (next (sat ?v9864)) (true (sat ?v9864)) (clause ?v9864))
(<= (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 ?v10682 (assign 4 t)) (role ?v10682))
(<= (next (sat 1)) (does ?v10703 (assign 18 f)) (role ?v10703))
(<= (next (sat 1)) (does ?v10724 (assign 19 t)) (role ?v10724))
(<= (next (sat 2)) (does ?v10747 (assign 3 t)) (role ?v10747))
(<= (next (sat 2)) (does ?v10768 (assign 18 t)) (role ?v10768))
(<= (next (sat 2)) (does ?v10789 (assign 5 f)) (role ?v10789))
(<= (next (sat 3)) (does ?v10812 (assign 5 f)) (role ?v10812))
(<= (next (sat 3)) (does ?v10833 (assign 8 f)) (role ?v10833))
(<= (next (sat 3)) (does ?v10854 (assign 15 f)) (role ?v10854))
(<= (next (sat 4)) (does ?v10877 (assign 20 f)) (role ?v10877))
(<= (next (sat 4)) (does ?v10898 (assign 7 t)) (role ?v10898))
(<= (next (sat 4)) (does ?v10919 (assign 16 f)) (role ?v10919))
(<= (next (sat 5)) (does ?v10942 (assign 10 t)) (role ?v10942))
(<= (next (sat 5)) (does ?v10963 (assign 13 f)) (role ?v10963))
(<= (next (sat 5)) (does ?v10984 (assign 7 f)) (role ?v10984))
(<= (next (sat 6)) (does ?v11007 (assign 12 f)) (role ?v11007))
(<= (next (sat 6)) (does ?v11028 (assign 9 f)) (role ?v11028))
(<= (next (sat 6)) (does ?v11049 (assign 17 t)) (role ?v11049))
(<= (next (sat 7)) (does ?v11072 (assign 17 t)) (role ?v11072))
(<= (next (sat 7)) (does ?v11093 (assign 19 t)) (role ?v11093))
(<= (next (sat 7)) (does ?v11114 (assign 5 t)) (role ?v11114))
(<= (next (sat 8)) (does ?v11137 (assign 16 f)) (role ?v11137))
(<= (next (sat 8)) (does ?v11158 (assign 9 t)) (role ?v11158))
(<= (next (sat 8)) (does ?v11179 (assign 15 t)) (role ?v11179))
(<= (next (sat 9)) (does ?v11202 (assign 11 t)) (role ?v11202))
(<= (next (sat 9)) (does ?v11223 (assign 5 f)) (role ?v11223))
(<= (next (sat 9)) (does ?v11244 (assign 14 f)) (role ?v11244))
(<= (next (sat 10)) (does ?v11267 (assign 18 t)) (role ?v11267))
(<= (next (sat 10)) (does ?v11288 (assign 10 f)) (role ?v11288))
(<= (next (sat 10)) (does ?v11309 (assign 13 t)) (role ?v11309))
(<= (next (sat 11)) (does ?v11332 (assign 3 f)) (role ?v11332))
(<= (next (sat 11)) (does ?v11353 (assign 11 t)) (role ?v11353))
(<= (next (sat 11)) (does ?v11374 (assign 12 t)) (role ?v11374))
(<= (next (sat 12)) (does ?v11397 (assign 6 f)) (role ?v11397))
(<= (next (sat 12)) (does ?v11418 (assign 17 f)) (role ?v11418))
(<= (next (sat 12)) (does ?v11439 (assign 8 f)) (role ?v11439))
(<= (next (sat 13)) (does ?v11462 (assign 18 f)) (role ?v11462))
(<= (next (sat 13)) (does ?v11483 (assign 14 t)) (role ?v11483))
(<= (next (sat 13)) (does ?v11504 (assign 1 t)) (role ?v11504))
(<= (next (sat 14)) (does ?v11527 (assign 19 f)) (role ?v11527))
(<= (next (sat 14)) (does ?v11548 (assign 15 f)) (role ?v11548))
(<= (next (sat 14)) (does ?v11569 (assign 10 t)) (role ?v11569))
(<= (next (sat 15)) (does ?v11592 (assign 12 t)) (role ?v11592))
(<= (next (sat 15)) (does ?v11613 (assign 18 t)) (role ?v11613))
(<= (next (sat 15)) (does ?v11634 (assign 19 f)) (role ?v11634))
(<= (next (sat 16)) (does ?v11657 (assign 8 f)) (role ?v11657))
(<= (next (sat 16)) (does ?v11678 (assign 4 t)) (role ?v11678))
(<= (next (sat 16)) (does ?v11699 (assign 7 t)) (role ?v11699))
(<= (next (sat 17)) (does ?v11722 (assign 8 f)) (role ?v11722))
(<= (next (sat 17)) (does ?v11743 (assign 9 f)) (role ?v11743))
(<= (next (sat 17)) (does ?v11764 (assign 4 t)) (role ?v11764))
(<= (next (sat 18)) (does ?v11787 (assign 7 t)) (role ?v11787))
(<= (next (sat 18)) (does ?v11808 (assign 17 t)) (role ?v11808))
(<= (next (sat 18)) (does ?v11829 (assign 15 f)) (role ?v11829))
(<= (next (sat 19)) (does ?v11852 (assign 12 t)) (role ?v11852))
(<= (next (sat 19)) (does ?v11873 (assign 7 f)) (role ?v11873))
(<= (next (sat 19)) (does ?v11894 (assign 14 f)) (role ?v11894))
(<= (next (sat 20)) (does ?v11917 (assign 10 f)) (role ?v11917))
(<= (next (sat 20)) (does ?v11938 (assign 11 f)) (role ?v11938))
(<= (next (sat 20)) (does ?v11959 (assign 8 t)) (role ?v11959))
(<= (next (sat 21)) (does ?v11982 (assign 2 t)) (role ?v11982))
(<= (next (sat 21)) (does ?v12003 (assign 15 f)) (role ?v12003))
(<= (next (sat 21)) (does ?v12024 (assign 11 f)) (role ?v12024))
(<= (next (sat 22)) (does ?v12047 (assign 9 t)) (role ?v12047))
(<= (next (sat 22)) (does ?v12068 (assign 6 t)) (role ?v12068))
(<= (next (sat 22)) (does ?v12089 (assign 1 t)) (role ?v12089))
(<= (next (sat 23)) (does ?v12112 (assign 11 f)) (role ?v12112))
(<= (next (sat 23)) (does ?v12133 (assign 20 t)) (role ?v12133))
(<= (next (sat 23)) (does ?v12154 (assign 17 f)) (role ?v12154))
(<= (next (sat 24)) (does ?v12177 (assign 9 t)) (role ?v12177))
(<= (next (sat 24)) (does ?v12198 (assign 15 f)) (role ?v12198))
(<= (next (sat 24)) (does ?v12219 (assign 13 t)) (role ?v12219))
(<= (next (sat 25)) (does ?v12242 (assign 12 t)) (role ?v12242))
(<= (next (sat 25)) (does ?v12263 (assign 7 f)) (role ?v12263))
(<= (next (sat 25)) (does ?v12284 (assign 17 f)) (role ?v12284))
(<= (next (sat 26)) (does ?v12307 (assign 18 f)) (role ?v12307))
(<= (next (sat 26)) (does ?v12328 (assign 2 f)) (role ?v12328))
(<= (next (sat 26)) (does ?v12349 (assign 20 t)) (role ?v12349))
(<= (next (sat 27)) (does ?v12372 (assign 20 t)) (role ?v12372))
(<= (next (sat 27)) (does ?v12393 (assign 12 t)) (role ?v12393))
(<= (next (sat 27)) (does ?v12414 (assign 4 t)) (role ?v12414))
(<= (next (sat 28)) (does ?v12437 (assign 19 t)) (role ?v12437))
(<= (next (sat 28)) (does ?v12458 (assign 11 t)) (role ?v12458))
(<= (next (sat 28)) (does ?v12479 (assign 14 t)) (role ?v12479))
(<= (next (sat 29)) (does ?v12502 (assign 16 f)) (role ?v12502))
(<= (next (sat 29)) (does ?v12523 (assign 18 t)) (role ?v12523))
(<= (next (sat 29)) (does ?v12544 (assign 4 f)) (role ?v12544))
(<= (next (sat 30)) (does ?v12567 (assign 1 f)) (role ?v12567))
(<= (next (sat 30)) (does ?v12588 (assign 17 f)) (role ?v12588))
(<= (next (sat 30)) (does ?v12609 (assign 19 f)) (role ?v12609))
(<= (next (sat 31)) (does ?v12632 (assign 13 f)) (role ?v12632))
(<= (next (sat 31)) (does ?v12653 (assign 15 t)) (role ?v12653))
(<= (next (sat 31)) (does ?v12674 (assign 10 t)) (role ?v12674))
(<= (next (sat 32)) (does ?v12697 (assign 12 f)) (role ?v12697))
(<= (next (sat 32)) (does ?v12718 (assign 14 f)) (role ?v12718))
(<= (next (sat 32)) (does ?v12739 (assign 13 f)) (role ?v12739))
(<= (next (sat 33)) (does ?v12762 (assign 12 t)) (role ?v12762))
(<= (next (sat 33)) (does ?v12783 (assign 14 f)) (role ?v12783))
(<= (next (sat 33)) (does ?v12804 (assign 7 f)) (role ?v12804))
(<= (next (sat 34)) (does ?v12827 (assign 7 f)) (role ?v12827))
(<= (next (sat 34)) (does ?v12848 (assign 16 t)) (role ?v12848))
(<= (next (sat 34)) (does ?v12869 (assign 10 t)) (role ?v12869))
(<= (next (sat 35)) (does ?v12892 (assign 6 t)) (role ?v12892))
(<= (next (sat 35)) (does ?v12913 (assign 10 t)) (role ?v12913))
(<= (next (sat 35)) (does ?v12934 (assign 7 t)) (role ?v12934))
(<= (next (sat 36)) (does ?v12957 (assign 20 t)) (role ?v12957))
(<= (next (sat 36)) (does ?v12978 (assign 14 t)) (role ?v12978))
(<= (next (sat 36)) (does ?v12999 (assign 16 f)) (role ?v12999))
(<= (next (sat 37)) (does ?v13022 (assign 19 f)) (role ?v13022))
(<= (next (sat 37)) (does ?v13043 (assign 17 t)) (role ?v13043))
(<= (next (sat 37)) (does ?v13064 (assign 11 t)) (role ?v13064))
(<= (next (sat 38)) (does ?v13087 (assign 7 f)) (role ?v13087))
(<= (next (sat 38)) (does ?v13108 (assign 1 t)) (role ?v13108))
(<= (next (sat 38)) (does ?v13129 (assign 20 f)) (role ?v13129))
(<= (next (sat 39)) (does ?v13152 (assign 5 f)) (role ?v13152))
(<= (next (sat 39)) (does ?v13173 (assign 12 t)) (role ?v13173))
(<= (next (sat 39)) (does ?v13194 (assign 15 t)) (role ?v13194))
(<= (next (sat 40)) (does ?v13217 (assign 4 f)) (role ?v13217))
(<= (next (sat 40)) (does ?v13238 (assign 9 f)) (role ?v13238))
(<= (next (sat 40)) (does ?v13259 (assign 13 f)) (role ?v13259))
(<= (next (sat 41)) (does ?v13282 (assign 12 t)) (role ?v13282))
(<= (next (sat 41)) (does ?v13303 (assign 11 f)) (role ?v13303))
(<= (next (sat 41)) (does ?v13324 (assign 7 f)) (role ?v13324))
(<= (next (sat 42)) (does ?v13347 (assign 5 f)) (role ?v13347))
(<= (next (sat 42)) (does ?v13368 (assign 19 t)) (role ?v13368))
(<= (next (sat 42)) (does ?v13389 (assign 8 f)) (role ?v13389))
(<= (next (sat 43)) (does ?v13412 (assign 1 t)) (role ?v13412))
(<= (next (sat 43)) (does ?v13433 (assign 16 t)) (role ?v13433))
(<= (next (sat 43)) (does ?v13454 (assign 17 t)) (role ?v13454))
(<= (next (sat 44)) (does ?v13477 (assign 20 t)) (role ?v13477))
(<= (next (sat 44)) (does ?v13498 (assign 14 f)) (role ?v13498))
(<= (next (sat 44)) (does ?v13519 (assign 15 f)) (role ?v13519))
(<= (next (sat 45)) (does ?v13542 (assign 13 t)) (role ?v13542))
(<= (next (sat 45)) (does ?v13563 (assign 4 f)) (role ?v13563))
(<= (next (sat 45)) (does ?v13584 (assign 10 t)) (role ?v13584))
(<= (next (sat 46)) (does ?v13607 (assign 14 t)) (role ?v13607))
(<= (next (sat 46)) (does ?v13628 (assign 7 t)) (role ?v13628))
(<= (next (sat 46)) (does ?v13649 (assign 10 t)) (role ?v13649))
(<= (next (sat 47)) (does ?v13672 (assign 5 f)) (role ?v13672))
(<= (next (sat 47)) (does ?v13693 (assign 9 t)) (role ?v13693))
(<= (next (sat 47)) (does ?v13714 (assign 20 t)) (role ?v13714))
(<= (next (sat 48)) (does ?v13737 (assign 10 t)) (role ?v13737))
(<= (next (sat 48)) (does ?v13758 (assign 1 t)) (role ?v13758))
(<= (next (sat 48)) (does ?v13779 (assign 19 f)) (role ?v13779))
(<= (next (sat 49)) (does ?v13802 (assign 16 f)) (role ?v13802))
(<= (next (sat 49)) (does ?v13823 (assign 15 f)) (role ?v13823))
(<= (next (sat 49)) (does ?v13844 (assign 1 f)) (role ?v13844))
(<= (next (sat 50)) (does ?v13867 (assign 16 t)) (role ?v13867))
(<= (next (sat 50)) (does ?v13888 (assign 3 t)) (role ?v13888))
(<= (next (sat 50)) (does ?v13909 (assign 11 f)) (role ?v13909))
(<= (next (sat 51)) (does ?v13932 (assign 15 f)) (role ?v13932))
(<= (next (sat 51)) (does ?v13953 (assign 10 f)) (role ?v13953))
(<= (next (sat 51)) (does ?v13974 (assign 4 t)) (role ?v13974))
(<= (next (sat 52)) (does ?v13997 (assign 4 t)) (role ?v13997))
(<= (next (sat 52)) (does ?v14018 (assign 15 f)) (role ?v14018))
(<= (next (sat 52)) (does ?v14039 (assign 3 f)) (role ?v14039))
(<= (next (sat 53)) (does ?v14062 (assign 10 f)) (role ?v14062))
(<= (next (sat 53)) (does ?v14083 (assign 16 f)) (role ?v14083))
(<= (next (sat 53)) (does ?v14104 (assign 11 t)) (role ?v14104))
(<= (next (sat 54)) (does ?v14127 (assign 8 f)) (role ?v14127))
(<= (next (sat 54)) (does ?v14148 (assign 12 t)) (role ?v14148))
(<= (next (sat 54)) (does ?v14169 (assign 5 f)) (role ?v14169))
(<= (next (sat 55)) (does ?v14192 (assign 14 t)) (role ?v14192))
(<= (next (sat 55)) (does ?v14213 (assign 6 f)) (role ?v14213))
(<= (next (sat 55)) (does ?v14234 (assign 12 t)) (role ?v14234))
(<= (next (sat 56)) (does ?v14257 (assign 1 t)) (role ?v14257))
(<= (next (sat 56)) (does ?v14278 (assign 6 t)) (role ?v14278))
(<= (next (sat 56)) (does ?v14299 (assign 11 t)) (role ?v14299))
(<= (next (sat 57)) (does ?v14322 (assign 13 f)) (role ?v14322))
(<= (next (sat 57)) (does ?v14343 (assign 5 f)) (role ?v14343))
(<= (next (sat 57)) (does ?v14364 (assign 1 f)) (role ?v14364))
(<= (next (sat 58)) (does ?v14387 (assign 7 f)) (role ?v14387))
(<= (next (sat 58)) (does ?v14408 (assign 2 f)) (role ?v14408))
(<= (next (sat 58)) (does ?v14429 (assign 12 t)) (role ?v14429))
(<= (next (sat 59)) (does ?v14452 (assign 1 t)) (role ?v14452))
(<= (next (sat 59)) (does ?v14473 (assign 20 f)) (role ?v14473))
(<= (next (sat 59)) (does ?v14494 (assign 19 t)) (role ?v14494))
(<= (next (sat 60)) (does ?v14517 (assign 2 f)) (role ?v14517))
(<= (next (sat 60)) (does ?v14538 (assign 13 f)) (role ?v14538))
(<= (next (sat 60)) (does ?v14559 (assign 8 f)) (role ?v14559))
(<= (next (sat 61)) (does ?v14582 (assign 15 t)) (role ?v14582))
(<= (next (sat 61)) (does ?v14603 (assign 18 t)) (role ?v14603))
(<= (next (sat 61)) (does ?v14624 (assign 4 t)) (role ?v14624))
(<= (next (sat 62)) (does ?v14647 (assign 11 f)) (role ?v14647))
(<= (next (sat 62)) (does ?v14668 (assign 14 t)) (role ?v14668))
(<= (next (sat 62)) (does ?v14689 (assign 9 t)) (role ?v14689))
(<= (next (sat 63)) (does ?v14712 (assign 6 f)) (role ?v14712))
(<= (next (sat 63)) (does ?v14733 (assign 15 f)) (role ?v14733))
(<= (next (sat 63)) (does ?v14754 (assign 2 f)) (role ?v14754))
(<= (next (sat 64)) (does ?v14777 (assign 5 t)) (role ?v14777))
(<= (next (sat 64)) (does ?v14798 (assign 12 f)) (role ?v14798))
(<= (next (sat 64)) (does ?v14819 (assign 15 f)) (role ?v14819))
(<= (next (sat 65)) (does ?v14842 (assign 6 f)) (role ?v14842))
(<= (next (sat 65)) (does ?v14863 (assign 17 t)) (role ?v14863))
(<= (next (sat 65)) (does ?v14884 (assign 5 t)) (role ?v14884))
(<= (next (sat 66)) (does ?v14907 (assign 13 f)) (role ?v14907))
(<= (next (sat 66)) (does ?v14928 (assign 5 t)) (role ?v14928))
(<= (next (sat 66)) (does ?v14949 (assign 19 f)) (role ?v14949))
(<= (next (sat 67)) (does ?v14972 (assign 20 t)) (role ?v14972))
(<= (next (sat 67)) (does ?v14993 (assign 1 f)) (role ?v14993))
(<= (next (sat 67)) (does ?v15014 (assign 14 t)) (role ?v15014))
(<= (next (sat 68)) (does ?v15037 (assign 9 t)) (role ?v15037))
(<= (next (sat 68)) (does ?v15058 (assign 17 f)) (role ?v15058))
(<= (next (sat 68)) (does ?v15079 (assign 15 t)) (role ?v15079))
(<= (next (sat 69)) (does ?v15102 (assign 5 f)) (role ?v15102))
(<= (next (sat 69)) (does ?v15123 (assign 19 t)) (role ?v15123))
(<= (next (sat 69)) (does ?v15144 (assign 18 f)) (role ?v15144))
(<= (next (sat 70)) (does ?v15167 (assign 12 f)) (role ?v15167))
(<= (next (sat 70)) (does ?v15188 (assign 8 t)) (role ?v15188))
(<= (next (sat 70)) (does ?v15209 (assign 10 f)) (role ?v15209))
(<= (next (sat 71)) (does ?v15232 (assign 18 f)) (role ?v15232))
(<= (next (sat 71)) (does ?v15253 (assign 14 t)) (role ?v15253))
(<= (next (sat 71)) (does ?v15274 (assign 4 f)) (role ?v15274))
(<= (next (sat 72)) (does ?v15297 (assign 15 t)) (role ?v15297))
(<= (next (sat 72)) (does ?v15318 (assign 9 f)) (role ?v15318))
(<= (next (sat 72)) (does ?v15339 (assign 13 t)) (role ?v15339))
(<= (next (sat 73)) (does ?v15362 (assign 9 t)) (role ?v15362))
(<= (next (sat 73)) (does ?v15383 (assign 5 f)) (role ?v15383))
(<= (next (sat 73)) (does ?v15404 (assign 1 f)) (role ?v15404))
(<= (next (sat 74)) (does ?v15427 (assign 10 t)) (role ?v15427))
(<= (next (sat 74)) (does ?v15448 (assign 19 f)) (role ?v15448))
(<= (next (sat 74)) (does ?v15469 (assign 14 f)) (role ?v15469))
(<= (next (sat 75)) (does ?v15492 (assign 20 t)) (role ?v15492))
(<= (next (sat 75)) (does ?v15513 (assign 9 t)) (role ?v15513))
(<= (next (sat 75)) (does ?v15534 (assign 4 t)) (role ?v15534))
(<= (next (sat 76)) (does ?v15557 (assign 9 f)) (role ?v15557))
(<= (next (sat 76)) (does ?v15578 (assign 2 f)) (role ?v15578))
(<= (next (sat 76)) (does ?v15599 (assign 19 t)) (role ?v15599))
(<= (next (sat 77)) (does ?v15622 (assign 5 f)) (role ?v15622))
(<= (next (sat 77)) (does ?v15643 (assign 13 t)) (role ?v15643))
(<= (next (sat 77)) (does ?v15664 (assign 17 f)) (role ?v15664))
(<= (next (sat 78)) (does ?v15687 (assign 2 t)) (role ?v15687))
(<= (next (sat 78)) (does ?v15708 (assign 10 f)) (role ?v15708))
(<= (next (sat 78)) (does ?v15729 (assign 18 f)) (role ?v15729))
(<= (next (sat 79)) (does ?v15752 (assign 18 f)) (role ?v15752))
(<= (next (sat 79)) (does ?v15773 (assign 3 t)) (role ?v15773))
(<= (next (sat 79)) (does ?v15794 (assign 11 t)) (role ?v15794))
(<= (next (sat 80)) (does ?v15817 (assign 7 t)) (role ?v15817))
(<= (next (sat 80)) (does ?v15838 (assign 9 f)) (role ?v15838))
(<= (next (sat 80)) (does ?v15859 (assign 17 t)) (role ?v15859))
(<= (next (sat 81)) (does ?v15882 (assign 15 f)) (role ?v15882))
(<= (next (sat 81)) (does ?v15903 (assign 6 f)) (role ?v15903))
(<= (next (sat 81)) (does ?v15924 (assign 3 f)) (role ?v15924))
(<= (next (sat 82)) (does ?v15947 (assign 2 f)) (role ?v15947))
(<= (next (sat 82)) (does ?v15968 (assign 3 t)) (role ?v15968))
(<= (next (sat 82)) (does ?v15989 (assign 13 f)) (role ?v15989))
(<= (next (sat 83)) (does ?v16012 (assign 12 t)) (role ?v16012))
(<= (next (sat 83)) (does ?v16033 (assign 3 t)) (role ?v16033))
(<= (next (sat 83)) (does ?v16054 (assign 2 f)) (role ?v16054))
(<= (next (sat 84)) (does ?v16077 (assign 2 f)) (role ?v16077))
(<= (next (sat 84)) (does ?v16098 (assign 3 f)) (role ?v16098))
(<= (next (sat 84)) (does ?v16119 (assign 17 t)) (role ?v16119))
(<= (next (sat 85)) (does ?v16142 (assign 20 t)) (role ?v16142))
(<= (next (sat 85)) (does ?v16163 (assign 15 f)) (role ?v16163))
(<= (next (sat 85)) (does ?v16184 (assign 16 f)) (role ?v16184))
(<= (next (sat 86)) (does ?v16207 (assign 5 f)) (role ?v16207))
(<= (next (sat 86)) (does ?v16228 (assign 17 f)) (role ?v16228))
(<= (next (sat 86)) (does ?v16249 (assign 19 f)) (role ?v16249))
(<= (next (sat 87)) (does ?v16272 (assign 20 f)) (role ?v16272))
(<= (next (sat 87)) (does ?v16293 (assign 18 f)) (role ?v16293))
(<= (next (sat 87)) (does ?v16314 (assign 11 t)) (role ?v16314))
(<= (next (sat 88)) (does ?v16337 (assign 9 f)) (role ?v16337))
(<= (next (sat 88)) (does ?v16358 (assign 1 t)) (role ?v16358))
(<= (next (sat 88)) (does ?v16379 (assign 5 f)) (role ?v16379))
(<= (next (sat 89)) (does ?v16402 (assign 19 f)) (role ?v16402))
(<= (next (sat 89)) (does ?v16423 (assign 9 t)) (role ?v16423))
(<= (next (sat 89)) (does ?v16444 (assign 17 t)) (role ?v16444))
(<= (next (sat 90)) (does ?v16467 (assign 12 t)) (role ?v16467))
(<= (next (sat 90)) (does ?v16488 (assign 2 f)) (role ?v16488))
(<= (next (sat 90)) (does ?v16509 (assign 17 t)) (role ?v16509))
(<= (next (sat 91)) (does ?v16532 (assign 4 t)) (role ?v16532))
(<= (next (sat 91)) (does ?v16553 (assign 16 f)) (role ?v16553))
(<= (next (sat 91)) (does ?v16574 (assign 5 f)) (role ?v16574))
(<= 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 50) one_not_sat (not two_not_sat))
(<= (goal exists 25) two_not_sat (not three_not_sat))
(<= (goal exists 0) three_not_sat)

(<= one_not_sat
	(clause ?c)
	(not (true (sat ?c)))
)

(<= two_not_sat
	(clause ?c1)
	(not (true (sat ?c1)))
	(clause ?c2)
	(not (true (sat ?c2)))
	(distinct ?c1 ?c2)
)

(<= three_not_sat
	(clause ?c1)
	(not (true (sat ?c1)))
	(clause ?c2)
	(not (true (sat ?c2)))
	(distinct ?c1 ?c2)
	(clause ?c3)
	(not (true (sat ?c3)))
	(distinct ?c1 ?c3)
	(distinct ?c2 ?c3)
)

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))