/
role_domino_planning_0.05_2.pddl
16751 lines (16751 loc) · 636 KB
/
role_domino_planning_0.05_2.pddl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(define (problem problemToSolve)
(:domain rbac)
(:objects
user0 user1 user2 user3 user4 user5 user6 user7 user8 user9 user10 user11 user12 user13 user14 user15 user16 user17 user18 user19 user20 user21 user22 user23 user24 user25 user26 user27 user28 user29 user30 user31 user32 user33 user34 user35 user36 user37 user38 user39 user40 user41 user42 user43 user44 user45 user46 user47 user48 user49 user50 user51 user52 user53 user54 user55 user56 user57 user58 user59 user60 user61 user62 user63 user64 user65 user66 user67 user68 user69 user70 user71 user72 user73 user74 user75 user76 user77 user78 - user
permission0 permission1 permission2 permission3 permission4 permission5 permission6 permission7 permission8 permission9 permission10 permission11 permission12 permission13 permission14 permission15 permission16 permission17 permission18 permission19 permission20 permission21 permission22 permission23 permission24 permission25 permission26 permission27 permission28 permission29 permission30 permission31 permission32 permission33 permission34 permission35 permission36 permission37 permission38 permission39 permission40 permission41 permission42 permission43 permission44 permission45 permission46 permission47 permission48 permission49 permission50 permission51 permission52 permission53 permission54 permission55 permission56 permission57 permission58 permission59 permission60 permission61 permission62 permission63 permission64 permission65 permission66 permission67 permission68 permission69 permission70 permission71 permission72 permission73 permission74 permission75 permission76 permission77 permission78 permission79 permission80 permission81 permission82 permission83 permission84 permission85 permission86 permission87 permission88 permission89 permission90 permission91 permission92 permission93 permission94 permission95 permission96 permission97 permission98 permission99 permission100 permission101 permission102 permission103 permission104 permission105 permission106 permission107 permission108 permission109 permission110 permission111 permission112 permission113 permission114 permission115 permission116 permission117 permission118 permission119 permission120 permission121 permission122 permission123 permission124 permission125 permission126 permission127 permission128 permission129 permission130 permission131 permission132 permission133 permission134 permission135 permission136 permission137 permission138 permission139 permission140 permission141 permission142 permission143 permission144 permission145 permission146 permission147 permission148 permission149 permission150 permission151 permission152 permission153 permission154 permission155 permission156 permission157 permission158 permission159 permission160 permission161 permission162 permission163 permission164 permission165 permission166 permission167 permission168 permission169 permission170 permission171 permission172 permission173 permission174 permission175 permission176 permission177 permission178 permission179 permission180 permission181 permission182 permission183 permission184 permission185 permission186 permission187 permission188 permission189 permission190 permission191 permission192 permission193 permission194 permission195 permission196 permission197 permission198 permission199 permission200 permission201 permission202 permission203 permission204 permission205 permission206 permission207 permission208 permission209 permission210 permission211 permission212 permission213 permission214 permission215 permission216 permission217 permission218 permission219 permission220 permission221 permission222 permission223 permission224 permission225 permission226 permission227 permission228 permission229 permission230 - permission
role0 role1 role2 role3 role4 role5 role6 role7 role8 role9 role10 role11 role12 role13 role14 role15 role16 role17 role18 role19 role20 role21 role22 role23 role24 role25 role26 - role)
(:init
(not(userRole user0 role0))
(not(userRole user0 role1))
(not(userRole user0 role2))
(not(userRole user0 role3))
(not(userRole user0 role4))
(not(userRole user0 role5))
(not(userRole user0 role6))
(not(userRole user0 role7))
(not(userRole user0 role8))
(not(userRole user0 role9))
(not(userRole user0 role10))
(not(userRole user0 role11))
(not(userRole user0 role12))
(not(userRole user0 role13))
(not(userRole user0 role14))
(not(userRole user0 role15))
(not(userRole user0 role16))
(not(userRole user0 role17))
(not(userRole user0 role18))
(not(userRole user0 role19))
(not(userRole user0 role20))
(not(userRole user0 role21))
(userRole user0 role22)
(not(userRole user0 role23))
(not(userRole user0 role24))
(not(userRole user0 role25))
(not(userRole user0 role26))
(not(userRole user1 role0))
(not(userRole user1 role1))
(not(userRole user1 role2))
(not(userRole user1 role3))
(userRole user1 role4)
(not(userRole user1 role5))
(not(userRole user1 role6))
(not(userRole user1 role7))
(not(userRole user1 role8))
(not(userRole user1 role9))
(userRole user1 role10)
(not(userRole user1 role11))
(not(userRole user1 role12))
(not(userRole user1 role13))
(not(userRole user1 role14))
(not(userRole user1 role15))
(not(userRole user1 role16))
(not(userRole user1 role17))
(not(userRole user1 role18))
(not(userRole user1 role19))
(not(userRole user1 role20))
(not(userRole user1 role21))
(not(userRole user1 role22))
(not(userRole user1 role23))
(not(userRole user1 role24))
(not(userRole user1 role25))
(not(userRole user1 role26))
(not(userRole user2 role0))
(not(userRole user2 role1))
(userRole user2 role2)
(not(userRole user2 role3))
(not(userRole user2 role4))
(not(userRole user2 role5))
(not(userRole user2 role6))
(not(userRole user2 role7))
(not(userRole user2 role8))
(not(userRole user2 role9))
(not(userRole user2 role10))
(not(userRole user2 role11))
(userRole user2 role12)
(not(userRole user2 role13))
(not(userRole user2 role14))
(not(userRole user2 role15))
(not(userRole user2 role16))
(not(userRole user2 role17))
(not(userRole user2 role18))
(not(userRole user2 role19))
(not(userRole user2 role20))
(not(userRole user2 role21))
(not(userRole user2 role22))
(not(userRole user2 role23))
(not(userRole user2 role24))
(not(userRole user2 role25))
(not(userRole user2 role26))
(not(userRole user3 role0))
(not(userRole user3 role1))
(not(userRole user3 role2))
(not(userRole user3 role3))
(not(userRole user3 role4))
(not(userRole user3 role5))
(not(userRole user3 role6))
(not(userRole user3 role7))
(not(userRole user3 role8))
(not(userRole user3 role9))
(not(userRole user3 role10))
(not(userRole user3 role11))
(not(userRole user3 role12))
(not(userRole user3 role13))
(not(userRole user3 role14))
(not(userRole user3 role15))
(not(userRole user3 role16))
(not(userRole user3 role17))
(not(userRole user3 role18))
(not(userRole user3 role19))
(not(userRole user3 role20))
(not(userRole user3 role21))
(userRole user3 role22)
(not(userRole user3 role23))
(not(userRole user3 role24))
(not(userRole user3 role25))
(not(userRole user3 role26))
(not(userRole user4 role0))
(not(userRole user4 role1))
(userRole user4 role2)
(not(userRole user4 role3))
(not(userRole user4 role4))
(not(userRole user4 role5))
(not(userRole user4 role6))
(not(userRole user4 role7))
(not(userRole user4 role8))
(not(userRole user4 role9))
(not(userRole user4 role10))
(not(userRole user4 role11))
(not(userRole user4 role12))
(not(userRole user4 role13))
(not(userRole user4 role14))
(not(userRole user4 role15))
(not(userRole user4 role16))
(not(userRole user4 role17))
(not(userRole user4 role18))
(not(userRole user4 role19))
(not(userRole user4 role20))
(not(userRole user4 role21))
(not(userRole user4 role22))
(not(userRole user4 role23))
(not(userRole user4 role24))
(not(userRole user4 role25))
(not(userRole user4 role26))
(not(userRole user5 role0))
(not(userRole user5 role1))
(not(userRole user5 role2))
(not(userRole user5 role3))
(not(userRole user5 role4))
(not(userRole user5 role5))
(not(userRole user5 role6))
(not(userRole user5 role7))
(not(userRole user5 role8))
(not(userRole user5 role9))
(not(userRole user5 role10))
(not(userRole user5 role11))
(not(userRole user5 role12))
(not(userRole user5 role13))
(not(userRole user5 role14))
(not(userRole user5 role15))
(not(userRole user5 role16))
(not(userRole user5 role17))
(not(userRole user5 role18))
(not(userRole user5 role19))
(not(userRole user5 role20))
(not(userRole user5 role21))
(userRole user5 role22)
(not(userRole user5 role23))
(not(userRole user5 role24))
(not(userRole user5 role25))
(not(userRole user5 role26))
(not(userRole user6 role0))
(not(userRole user6 role1))
(not(userRole user6 role2))
(not(userRole user6 role3))
(not(userRole user6 role4))
(not(userRole user6 role5))
(not(userRole user6 role6))
(not(userRole user6 role7))
(not(userRole user6 role8))
(not(userRole user6 role9))
(not(userRole user6 role10))
(not(userRole user6 role11))
(userRole user6 role12)
(not(userRole user6 role13))
(not(userRole user6 role14))
(not(userRole user6 role15))
(not(userRole user6 role16))
(not(userRole user6 role17))
(not(userRole user6 role18))
(not(userRole user6 role19))
(not(userRole user6 role20))
(not(userRole user6 role21))
(not(userRole user6 role22))
(not(userRole user6 role23))
(not(userRole user6 role24))
(not(userRole user6 role25))
(not(userRole user6 role26))
(not(userRole user7 role0))
(not(userRole user7 role1))
(not(userRole user7 role2))
(not(userRole user7 role3))
(not(userRole user7 role4))
(not(userRole user7 role5))
(not(userRole user7 role6))
(not(userRole user7 role7))
(not(userRole user7 role8))
(userRole user7 role9)
(userRole user7 role10)
(not(userRole user7 role11))
(not(userRole user7 role12))
(not(userRole user7 role13))
(not(userRole user7 role14))
(not(userRole user7 role15))
(not(userRole user7 role16))
(not(userRole user7 role17))
(userRole user7 role18)
(not(userRole user7 role19))
(not(userRole user7 role20))
(not(userRole user7 role21))
(not(userRole user7 role22))
(not(userRole user7 role23))
(not(userRole user7 role24))
(not(userRole user7 role25))
(not(userRole user7 role26))
(not(userRole user8 role0))
(not(userRole user8 role1))
(not(userRole user8 role2))
(not(userRole user8 role3))
(not(userRole user8 role4))
(not(userRole user8 role5))
(not(userRole user8 role6))
(not(userRole user8 role7))
(not(userRole user8 role8))
(not(userRole user8 role9))
(not(userRole user8 role10))
(not(userRole user8 role11))
(not(userRole user8 role12))
(not(userRole user8 role13))
(userRole user8 role14)
(not(userRole user8 role15))
(not(userRole user8 role16))
(userRole user8 role17)
(not(userRole user8 role18))
(not(userRole user8 role19))
(not(userRole user8 role20))
(not(userRole user8 role21))
(not(userRole user8 role22))
(not(userRole user8 role23))
(not(userRole user8 role24))
(not(userRole user8 role25))
(not(userRole user8 role26))
(not(userRole user9 role0))
(not(userRole user9 role1))
(not(userRole user9 role2))
(not(userRole user9 role3))
(not(userRole user9 role4))
(not(userRole user9 role5))
(not(userRole user9 role6))
(not(userRole user9 role7))
(not(userRole user9 role8))
(not(userRole user9 role9))
(not(userRole user9 role10))
(not(userRole user9 role11))
(userRole user9 role12)
(not(userRole user9 role13))
(not(userRole user9 role14))
(not(userRole user9 role15))
(not(userRole user9 role16))
(not(userRole user9 role17))
(not(userRole user9 role18))
(not(userRole user9 role19))
(not(userRole user9 role20))
(not(userRole user9 role21))
(not(userRole user9 role22))
(not(userRole user9 role23))
(not(userRole user9 role24))
(userRole user9 role25)
(not(userRole user9 role26))
(not(userRole user10 role0))
(not(userRole user10 role1))
(not(userRole user10 role2))
(not(userRole user10 role3))
(not(userRole user10 role4))
(not(userRole user10 role5))
(not(userRole user10 role6))
(not(userRole user10 role7))
(not(userRole user10 role8))
(not(userRole user10 role9))
(not(userRole user10 role10))
(userRole user10 role11)
(not(userRole user10 role12))
(not(userRole user10 role13))
(not(userRole user10 role14))
(not(userRole user10 role15))
(not(userRole user10 role16))
(not(userRole user10 role17))
(not(userRole user10 role18))
(not(userRole user10 role19))
(not(userRole user10 role20))
(not(userRole user10 role21))
(userRole user10 role22)
(not(userRole user10 role23))
(not(userRole user10 role24))
(not(userRole user10 role25))
(not(userRole user10 role26))
(not(userRole user11 role0))
(not(userRole user11 role1))
(userRole user11 role2)
(not(userRole user11 role3))
(not(userRole user11 role4))
(not(userRole user11 role5))
(not(userRole user11 role6))
(not(userRole user11 role7))
(userRole user11 role8)
(not(userRole user11 role9))
(not(userRole user11 role10))
(not(userRole user11 role11))
(not(userRole user11 role12))
(not(userRole user11 role13))
(not(userRole user11 role14))
(userRole user11 role15)
(not(userRole user11 role16))
(not(userRole user11 role17))
(not(userRole user11 role18))
(not(userRole user11 role19))
(not(userRole user11 role20))
(not(userRole user11 role21))
(not(userRole user11 role22))
(not(userRole user11 role23))
(not(userRole user11 role24))
(not(userRole user11 role25))
(not(userRole user11 role26))
(not(userRole user12 role0))
(not(userRole user12 role1))
(not(userRole user12 role2))
(not(userRole user12 role3))
(not(userRole user12 role4))
(not(userRole user12 role5))
(not(userRole user12 role6))
(not(userRole user12 role7))
(not(userRole user12 role8))
(not(userRole user12 role9))
(not(userRole user12 role10))
(not(userRole user12 role11))
(userRole user12 role12)
(not(userRole user12 role13))
(not(userRole user12 role14))
(not(userRole user12 role15))
(not(userRole user12 role16))
(not(userRole user12 role17))
(not(userRole user12 role18))
(not(userRole user12 role19))
(not(userRole user12 role20))
(not(userRole user12 role21))
(not(userRole user12 role22))
(not(userRole user12 role23))
(not(userRole user12 role24))
(not(userRole user12 role25))
(not(userRole user12 role26))
(not(userRole user13 role0))
(not(userRole user13 role1))
(userRole user13 role2)
(not(userRole user13 role3))
(not(userRole user13 role4))
(not(userRole user13 role5))
(not(userRole user13 role6))
(not(userRole user13 role7))
(not(userRole user13 role8))
(not(userRole user13 role9))
(not(userRole user13 role10))
(not(userRole user13 role11))
(userRole user13 role12)
(not(userRole user13 role13))
(not(userRole user13 role14))
(not(userRole user13 role15))
(not(userRole user13 role16))
(not(userRole user13 role17))
(not(userRole user13 role18))
(not(userRole user13 role19))
(not(userRole user13 role20))
(not(userRole user13 role21))
(not(userRole user13 role22))
(not(userRole user13 role23))
(not(userRole user13 role24))
(not(userRole user13 role25))
(not(userRole user13 role26))
(not(userRole user14 role0))
(not(userRole user14 role1))
(userRole user14 role2)
(not(userRole user14 role3))
(not(userRole user14 role4))
(not(userRole user14 role5))
(not(userRole user14 role6))
(not(userRole user14 role7))
(not(userRole user14 role8))
(not(userRole user14 role9))
(not(userRole user14 role10))
(not(userRole user14 role11))
(not(userRole user14 role12))
(not(userRole user14 role13))
(not(userRole user14 role14))
(not(userRole user14 role15))
(not(userRole user14 role16))
(not(userRole user14 role17))
(not(userRole user14 role18))
(not(userRole user14 role19))
(not(userRole user14 role20))
(not(userRole user14 role21))
(not(userRole user14 role22))
(not(userRole user14 role23))
(not(userRole user14 role24))
(not(userRole user14 role25))
(not(userRole user14 role26))
(not(userRole user15 role0))
(not(userRole user15 role1))
(not(userRole user15 role2))
(not(userRole user15 role3))
(not(userRole user15 role4))
(not(userRole user15 role5))
(not(userRole user15 role6))
(userRole user15 role7)
(not(userRole user15 role8))
(userRole user15 role9)
(not(userRole user15 role10))
(not(userRole user15 role11))
(userRole user15 role12)
(not(userRole user15 role13))
(userRole user15 role14)
(not(userRole user15 role15))
(not(userRole user15 role16))
(not(userRole user15 role17))
(not(userRole user15 role18))
(not(userRole user15 role19))
(not(userRole user15 role20))
(userRole user15 role21)
(userRole user15 role22)
(not(userRole user15 role23))
(not(userRole user15 role24))
(not(userRole user15 role25))
(not(userRole user15 role26))
(not(userRole user16 role0))
(not(userRole user16 role1))
(not(userRole user16 role2))
(not(userRole user16 role3))
(not(userRole user16 role4))
(not(userRole user16 role5))
(not(userRole user16 role6))
(not(userRole user16 role7))
(not(userRole user16 role8))
(not(userRole user16 role9))
(not(userRole user16 role10))
(not(userRole user16 role11))
(not(userRole user16 role12))
(not(userRole user16 role13))
(not(userRole user16 role14))
(not(userRole user16 role15))
(not(userRole user16 role16))
(not(userRole user16 role17))
(not(userRole user16 role18))
(not(userRole user16 role19))
(not(userRole user16 role20))
(not(userRole user16 role21))
(not(userRole user16 role22))
(not(userRole user16 role23))
(not(userRole user16 role24))
(not(userRole user16 role25))
(not(userRole user16 role26))
(not(userRole user17 role0))
(not(userRole user17 role1))
(not(userRole user17 role2))
(not(userRole user17 role3))
(not(userRole user17 role4))
(not(userRole user17 role5))
(not(userRole user17 role6))
(not(userRole user17 role7))
(not(userRole user17 role8))
(not(userRole user17 role9))
(not(userRole user17 role10))
(not(userRole user17 role11))
(userRole user17 role12)
(not(userRole user17 role13))
(not(userRole user17 role14))
(not(userRole user17 role15))
(not(userRole user17 role16))
(not(userRole user17 role17))
(not(userRole user17 role18))
(not(userRole user17 role19))
(not(userRole user17 role20))
(not(userRole user17 role21))
(not(userRole user17 role22))
(not(userRole user17 role23))
(not(userRole user17 role24))
(not(userRole user17 role25))
(not(userRole user17 role26))
(not(userRole user18 role0))
(not(userRole user18 role1))
(not(userRole user18 role2))
(not(userRole user18 role3))
(not(userRole user18 role4))
(not(userRole user18 role5))
(not(userRole user18 role6))
(not(userRole user18 role7))
(not(userRole user18 role8))
(not(userRole user18 role9))
(not(userRole user18 role10))
(not(userRole user18 role11))
(userRole user18 role12)
(not(userRole user18 role13))
(not(userRole user18 role14))
(not(userRole user18 role15))
(not(userRole user18 role16))
(not(userRole user18 role17))
(not(userRole user18 role18))
(not(userRole user18 role19))
(not(userRole user18 role20))
(not(userRole user18 role21))
(not(userRole user18 role22))
(not(userRole user18 role23))
(not(userRole user18 role24))
(not(userRole user18 role25))
(not(userRole user18 role26))
(not(userRole user19 role0))
(not(userRole user19 role1))
(userRole user19 role2)
(not(userRole user19 role3))
(not(userRole user19 role4))
(not(userRole user19 role5))
(not(userRole user19 role6))
(not(userRole user19 role7))
(not(userRole user19 role8))
(not(userRole user19 role9))
(not(userRole user19 role10))
(not(userRole user19 role11))
(userRole user19 role12)
(not(userRole user19 role13))
(not(userRole user19 role14))
(not(userRole user19 role15))
(not(userRole user19 role16))
(not(userRole user19 role17))
(not(userRole user19 role18))
(not(userRole user19 role19))
(not(userRole user19 role20))
(not(userRole user19 role21))
(not(userRole user19 role22))
(not(userRole user19 role23))
(not(userRole user19 role24))
(not(userRole user19 role25))
(not(userRole user19 role26))
(not(userRole user20 role0))
(not(userRole user20 role1))
(not(userRole user20 role2))
(not(userRole user20 role3))
(not(userRole user20 role4))
(not(userRole user20 role5))
(not(userRole user20 role6))
(not(userRole user20 role7))
(not(userRole user20 role8))
(not(userRole user20 role9))
(not(userRole user20 role10))
(not(userRole user20 role11))
(userRole user20 role12)
(not(userRole user20 role13))
(not(userRole user20 role14))
(not(userRole user20 role15))
(not(userRole user20 role16))
(not(userRole user20 role17))
(not(userRole user20 role18))
(not(userRole user20 role19))
(not(userRole user20 role20))
(not(userRole user20 role21))
(not(userRole user20 role22))
(not(userRole user20 role23))
(not(userRole user20 role24))
(not(userRole user20 role25))
(not(userRole user20 role26))
(not(userRole user21 role0))
(not(userRole user21 role1))
(userRole user21 role2)
(not(userRole user21 role3))
(not(userRole user21 role4))
(not(userRole user21 role5))
(not(userRole user21 role6))
(not(userRole user21 role7))
(not(userRole user21 role8))
(not(userRole user21 role9))
(not(userRole user21 role10))
(not(userRole user21 role11))
(userRole user21 role12)
(not(userRole user21 role13))
(not(userRole user21 role14))
(not(userRole user21 role15))
(not(userRole user21 role16))
(not(userRole user21 role17))
(not(userRole user21 role18))
(not(userRole user21 role19))
(not(userRole user21 role20))
(not(userRole user21 role21))
(not(userRole user21 role22))
(not(userRole user21 role23))
(not(userRole user21 role24))
(not(userRole user21 role25))
(not(userRole user21 role26))
(not(userRole user22 role0))
(not(userRole user22 role1))
(not(userRole user22 role2))
(not(userRole user22 role3))
(not(userRole user22 role4))
(not(userRole user22 role5))
(not(userRole user22 role6))
(not(userRole user22 role7))
(not(userRole user22 role8))
(not(userRole user22 role9))
(not(userRole user22 role10))
(not(userRole user22 role11))
(not(userRole user22 role12))
(not(userRole user22 role13))
(not(userRole user22 role14))
(not(userRole user22 role15))
(not(userRole user22 role16))
(not(userRole user22 role17))
(not(userRole user22 role18))
(not(userRole user22 role19))
(not(userRole user22 role20))
(not(userRole user22 role21))
(userRole user22 role22)
(not(userRole user22 role23))
(not(userRole user22 role24))
(not(userRole user22 role25))
(not(userRole user22 role26))
(not(userRole user23 role0))
(not(userRole user23 role1))
(userRole user23 role2)
(not(userRole user23 role3))
(not(userRole user23 role4))
(not(userRole user23 role5))
(not(userRole user23 role6))
(not(userRole user23 role7))
(not(userRole user23 role8))
(not(userRole user23 role9))
(not(userRole user23 role10))
(not(userRole user23 role11))
(userRole user23 role12)
(not(userRole user23 role13))
(not(userRole user23 role14))
(not(userRole user23 role15))
(not(userRole user23 role16))
(not(userRole user23 role17))
(not(userRole user23 role18))
(not(userRole user23 role19))
(not(userRole user23 role20))
(not(userRole user23 role21))
(not(userRole user23 role22))
(not(userRole user23 role23))
(not(userRole user23 role24))
(not(userRole user23 role25))
(not(userRole user23 role26))
(not(userRole user24 role0))
(not(userRole user24 role1))
(not(userRole user24 role2))
(userRole user24 role3)
(not(userRole user24 role4))
(not(userRole user24 role5))
(not(userRole user24 role6))
(not(userRole user24 role7))
(not(userRole user24 role8))
(not(userRole user24 role9))
(not(userRole user24 role10))
(not(userRole user24 role11))
(not(userRole user24 role12))
(not(userRole user24 role13))
(userRole user24 role14)
(not(userRole user24 role15))
(not(userRole user24 role16))
(not(userRole user24 role17))
(not(userRole user24 role18))
(not(userRole user24 role19))
(userRole user24 role20)
(not(userRole user24 role21))
(not(userRole user24 role22))
(not(userRole user24 role23))
(not(userRole user24 role24))
(not(userRole user24 role25))
(not(userRole user24 role26))
(not(userRole user25 role0))
(not(userRole user25 role1))
(not(userRole user25 role2))
(not(userRole user25 role3))
(not(userRole user25 role4))
(not(userRole user25 role5))
(not(userRole user25 role6))
(not(userRole user25 role7))
(not(userRole user25 role8))
(not(userRole user25 role9))
(not(userRole user25 role10))
(not(userRole user25 role11))
(not(userRole user25 role12))
(not(userRole user25 role13))
(userRole user25 role14)
(not(userRole user25 role15))
(not(userRole user25 role16))
(not(userRole user25 role17))
(not(userRole user25 role18))
(not(userRole user25 role19))
(not(userRole user25 role20))
(not(userRole user25 role21))
(not(userRole user25 role22))
(not(userRole user25 role23))
(userRole user25 role24)
(not(userRole user25 role25))
(not(userRole user25 role26))
(not(userRole user26 role0))
(not(userRole user26 role1))
(not(userRole user26 role2))
(not(userRole user26 role3))
(not(userRole user26 role4))
(not(userRole user26 role5))
(not(userRole user26 role6))
(not(userRole user26 role7))
(not(userRole user26 role8))
(not(userRole user26 role9))
(not(userRole user26 role10))
(not(userRole user26 role11))
(not(userRole user26 role12))
(not(userRole user26 role13))
(not(userRole user26 role14))
(not(userRole user26 role15))
(not(userRole user26 role16))
(not(userRole user26 role17))
(not(userRole user26 role18))
(not(userRole user26 role19))
(not(userRole user26 role20))
(not(userRole user26 role21))
(not(userRole user26 role22))
(not(userRole user26 role23))
(not(userRole user26 role24))
(not(userRole user26 role25))
(not(userRole user26 role26))
(not(userRole user27 role0))
(not(userRole user27 role1))
(not(userRole user27 role2))
(not(userRole user27 role3))
(not(userRole user27 role4))
(not(userRole user27 role5))
(not(userRole user27 role6))
(not(userRole user27 role7))
(not(userRole user27 role8))
(not(userRole user27 role9))
(not(userRole user27 role10))
(not(userRole user27 role11))
(userRole user27 role12)
(not(userRole user27 role13))
(not(userRole user27 role14))
(not(userRole user27 role15))
(not(userRole user27 role16))
(not(userRole user27 role17))
(not(userRole user27 role18))
(not(userRole user27 role19))
(not(userRole user27 role20))
(not(userRole user27 role21))
(not(userRole user27 role22))
(not(userRole user27 role23))
(not(userRole user27 role24))
(not(userRole user27 role25))
(not(userRole user27 role26))
(not(userRole user28 role0))
(not(userRole user28 role1))
(not(userRole user28 role2))
(not(userRole user28 role3))
(not(userRole user28 role4))
(not(userRole user28 role5))
(not(userRole user28 role6))
(not(userRole user28 role7))
(not(userRole user28 role8))
(not(userRole user28 role9))
(not(userRole user28 role10))
(not(userRole user28 role11))
(userRole user28 role12)
(not(userRole user28 role13))
(not(userRole user28 role14))
(not(userRole user28 role15))
(not(userRole user28 role16))
(not(userRole user28 role17))
(not(userRole user28 role18))
(not(userRole user28 role19))
(not(userRole user28 role20))
(not(userRole user28 role21))
(not(userRole user28 role22))
(not(userRole user28 role23))
(not(userRole user28 role24))
(not(userRole user28 role25))
(not(userRole user28 role26))
(not(userRole user29 role0))
(not(userRole user29 role1))
(userRole user29 role2)
(not(userRole user29 role3))
(not(userRole user29 role4))
(not(userRole user29 role5))
(not(userRole user29 role6))
(not(userRole user29 role7))
(not(userRole user29 role8))
(not(userRole user29 role9))
(not(userRole user29 role10))
(not(userRole user29 role11))
(userRole user29 role12)
(not(userRole user29 role13))
(not(userRole user29 role14))
(not(userRole user29 role15))
(not(userRole user29 role16))
(not(userRole user29 role17))
(not(userRole user29 role18))
(not(userRole user29 role19))
(not(userRole user29 role20))
(not(userRole user29 role21))
(not(userRole user29 role22))
(not(userRole user29 role23))
(not(userRole user29 role24))
(not(userRole user29 role25))
(not(userRole user29 role26))
(not(userRole user30 role0))
(not(userRole user30 role1))
(userRole user30 role2)
(not(userRole user30 role3))
(not(userRole user30 role4))
(not(userRole user30 role5))
(not(userRole user30 role6))
(not(userRole user30 role7))
(not(userRole user30 role8))
(not(userRole user30 role9))
(not(userRole user30 role10))
(not(userRole user30 role11))
(userRole user30 role12)
(not(userRole user30 role13))
(not(userRole user30 role14))
(not(userRole user30 role15))
(not(userRole user30 role16))
(not(userRole user30 role17))
(not(userRole user30 role18))
(not(userRole user30 role19))
(not(userRole user30 role20))
(not(userRole user30 role21))
(not(userRole user30 role22))
(not(userRole user30 role23))
(not(userRole user30 role24))
(not(userRole user30 role25))
(not(userRole user30 role26))
(not(userRole user31 role0))
(not(userRole user31 role1))
(not(userRole user31 role2))
(not(userRole user31 role3))
(not(userRole user31 role4))
(not(userRole user31 role5))
(not(userRole user31 role6))
(not(userRole user31 role7))
(not(userRole user31 role8))
(not(userRole user31 role9))
(not(userRole user31 role10))
(not(userRole user31 role11))
(not(userRole user31 role12))
(not(userRole user31 role13))
(not(userRole user31 role14))
(not(userRole user31 role15))
(userRole user31 role16)
(not(userRole user31 role17))
(not(userRole user31 role18))
(not(userRole user31 role19))
(not(userRole user31 role20))
(not(userRole user31 role21))
(not(userRole user31 role22))
(not(userRole user31 role23))
(not(userRole user31 role24))
(not(userRole user31 role25))
(not(userRole user31 role26))
(not(userRole user32 role0))
(not(userRole user32 role1))
(not(userRole user32 role2))
(not(userRole user32 role3))
(not(userRole user32 role4))
(not(userRole user32 role5))
(not(userRole user32 role6))
(not(userRole user32 role7))
(not(userRole user32 role8))
(not(userRole user32 role9))
(not(userRole user32 role10))
(not(userRole user32 role11))
(userRole user32 role12)
(not(userRole user32 role13))
(not(userRole user32 role14))
(not(userRole user32 role15))
(not(userRole user32 role16))
(not(userRole user32 role17))
(not(userRole user32 role18))
(not(userRole user32 role19))
(not(userRole user32 role20))
(not(userRole user32 role21))
(not(userRole user32 role22))
(not(userRole user32 role23))
(not(userRole user32 role24))
(not(userRole user32 role25))
(not(userRole user32 role26))
(not(userRole user33 role0))
(not(userRole user33 role1))
(userRole user33 role2)
(not(userRole user33 role3))
(not(userRole user33 role4))
(not(userRole user33 role5))
(not(userRole user33 role6))
(not(userRole user33 role7))
(not(userRole user33 role8))
(not(userRole user33 role9))
(not(userRole user33 role10))
(not(userRole user33 role11))
(not(userRole user33 role12))
(not(userRole user33 role13))
(not(userRole user33 role14))
(not(userRole user33 role15))
(not(userRole user33 role16))
(not(userRole user33 role17))
(not(userRole user33 role18))
(not(userRole user33 role19))
(not(userRole user33 role20))
(not(userRole user33 role21))
(not(userRole user33 role22))
(not(userRole user33 role23))
(not(userRole user33 role24))
(not(userRole user33 role25))
(not(userRole user33 role26))
(not(userRole user34 role0))
(not(userRole user34 role1))
(not(userRole user34 role2))
(not(userRole user34 role3))
(not(userRole user34 role4))
(not(userRole user34 role5))
(not(userRole user34 role6))
(not(userRole user34 role7))
(not(userRole user34 role8))
(not(userRole user34 role9))
(not(userRole user34 role10))
(not(userRole user34 role11))
(userRole user34 role12)
(not(userRole user34 role13))
(not(userRole user34 role14))
(not(userRole user34 role15))
(not(userRole user34 role16))
(not(userRole user34 role17))
(not(userRole user34 role18))
(not(userRole user34 role19))
(not(userRole user34 role20))
(not(userRole user34 role21))
(not(userRole user34 role22))
(not(userRole user34 role23))
(not(userRole user34 role24))
(not(userRole user34 role25))
(not(userRole user34 role26))
(not(userRole user35 role0))
(not(userRole user35 role1))
(not(userRole user35 role2))
(not(userRole user35 role3))
(not(userRole user35 role4))
(not(userRole user35 role5))
(not(userRole user35 role6))
(not(userRole user35 role7))
(not(userRole user35 role8))
(not(userRole user35 role9))
(not(userRole user35 role10))
(not(userRole user35 role11))
(userRole user35 role12)
(not(userRole user35 role13))
(not(userRole user35 role14))
(not(userRole user35 role15))
(not(userRole user35 role16))
(not(userRole user35 role17))
(not(userRole user35 role18))
(not(userRole user35 role19))
(not(userRole user35 role20))
(not(userRole user35 role21))
(not(userRole user35 role22))
(not(userRole user35 role23))
(not(userRole user35 role24))
(not(userRole user35 role25))
(not(userRole user35 role26))
(not(userRole user36 role0))
(not(userRole user36 role1))
(not(userRole user36 role2))
(not(userRole user36 role3))
(not(userRole user36 role4))
(not(userRole user36 role5))
(not(userRole user36 role6))
(not(userRole user36 role7))
(not(userRole user36 role8))
(not(userRole user36 role9))
(not(userRole user36 role10))
(not(userRole user36 role11))
(userRole user36 role12)
(not(userRole user36 role13))
(not(userRole user36 role14))
(not(userRole user36 role15))
(not(userRole user36 role16))
(not(userRole user36 role17))
(not(userRole user36 role18))
(not(userRole user36 role19))
(not(userRole user36 role20))