-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathLadder.tptp
4632 lines (4630 loc) · 551 KB
/
Ladder.tptp
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
fof(ax,axiom, vIL822__EN_JS_1 <=> (~ vIL822__EN_CAN_0 & (~ vIL822__EN_JR_0 & (~ vIL822_ENABLED_0 & (vIL822__EN_SEL_0 | vIL822__EN_JS_0))))).
fof(ax,axiom, vIL822__EN_AK_1 <=> vIL822__EN_JS_1).
fof(ax,axiom, vIL822__EN_SET_1 <=> (vIL822__EN_EXE_0 & vIL822__EN_AK_1)).
fof(ax,axiom, vIL822__XEN_JS_1 <=> (~ vIL822__XEN_CAN_0 & (~ vIL822__XEN_JR_0 & (vIL822_ENABLED_0 & (vIL822__XEN_SEL_0 | vIL822__XEN_JS_0))))).
fof(ax,axiom, vIL822__XEN_AK_1 <=> vIL822__XEN_JS_1).
fof(ax,axiom, vIL822__EN_RESET_1 <=> (vIL822__XEN_EXE_0 & vIL822__XEN_AK_1)).
fof(ax,axiom, vS100_OIE_1 <=> vSOM_3_2_OIE_0).
fof(ax,axiom, vS102_OIE_1 <=> vSOM_5_2_OIE_0).
fof(ax,axiom, vS104_OIE_1 <=> vSOM_7_2_OIE_0).
fof(ax,axiom, vS106_OIE_1 <=> vSOM_9_2_OIE_0).
fof(ax,axiom, vS110_OIE_1 <=> vSOM_19_2_OIE_0).
fof(ax,axiom, vMSDP6_SGRC_1 <=> (vMSDP6_QSGRC_0 | (vMSDP6_SGRC_0 & (~ vMSDP6_QXSGRC_0 | (~ vIL822_ENABLED_0 | vMSDP6__SGRC_RD_0))))).
fof(ax,axiom, vMSDP6__SGRC_RD_1 <=> ((vIL822_ENABLED_0 & vMSDP6__SGRC_QRD_0) | (vMSDP6__SGRC_RD_0 & (~ vMSDP6__SGRC_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS100_AM___U_JS_1 <=> (~ vS100_AM___U_CAN_0 & (~ vS100_AM___U_JR_0 & (~ vS100_AM___U_INHIBIT_0 & (vS100_AM___U_SEL_0 | vS100_AM___U_JS_0))))).
fof(ax,axiom, vS100_AM___U_AK_1 <=> vS100_AM___U_JS_1).
fof(ax,axiom, vS100_AM___U_SET_1 <=> (vS100_AM___U_EXE_0 & vS100_AM___U_AK_1)).
fof(ax,axiom, vS100_AM___XU_JS_1 <=> (~ vS100_AM___XU_CAN_0 & (~ vS100_AM___XU_JR_0 & (vS100_AM___U_INHIBIT_0 & (vS100_AM___XU_SEL_0 | vS100_AM___XU_JS_0))))).
fof(ax,axiom, vS100_AM___XU_AK_1 <=> vS100_AM___XU_JS_1).
fof(ax,axiom, vS100_AM___U_RESET_1 <=> (vS100_AM___XU_EXE_0 & vS100_AM___XU_AK_1)).
fof(ax,axiom, vS106_AM___U_JS_1 <=> (~ vS106_AM___U_CAN_0 & (~ vS106_AM___U_JR_0 & (~ vS106_AM___U_INHIBIT_0 & (vS106_AM___U_SEL_0 | vS106_AM___U_JS_0))))).
fof(ax,axiom, vS106_AM___U_AK_1 <=> vS106_AM___U_JS_1).
fof(ax,axiom, vS106_AM___U_SET_1 <=> (vS106_AM___U_EXE_0 & vS106_AM___U_AK_1)).
fof(ax,axiom, vS106_AM___XU_JS_1 <=> (~ vS106_AM___XU_CAN_0 & (~ vS106_AM___XU_JR_0 & (vS106_AM___U_INHIBIT_0 & (vS106_AM___XU_SEL_0 | vS106_AM___XU_JS_0))))).
fof(ax,axiom, vS106_AM___XU_AK_1 <=> vS106_AM___XU_JS_1).
fof(ax,axiom, vS106_AM___U_RESET_1 <=> (vS106_AM___XU_EXE_0 & vS106_AM___XU_AK_1)).
fof(ax,axiom, vS106_AC___U_JS_1 <=> (~ vS106_AC___U_CAN_0 & (~ vS106_AC___U_JR_0 & (~ vS106_AC___U_INHIBIT_0 & (vS106_AC___U_SEL_0 | vS106_AC___U_JS_0))))).
fof(ax,axiom, vS106_AC___U_AK_1 <=> vS106_AC___U_JS_1).
fof(ax,axiom, vS106_AC___U_SET_1 <=> (vS106_AC___U_EXE_0 & vS106_AC___U_AK_1)).
fof(ax,axiom, vS106_AC___XU_JS_1 <=> (~ vS106_AC___XU_CAN_0 & (~ vS106_AC___XU_JR_0 & (vS106_AC___U_INHIBIT_0 & (vS106_AC___XU_SEL_0 | vS106_AC___XU_JS_0))))).
fof(ax,axiom, vS106_AC___XU_AK_1 <=> vS106_AC___XU_JS_1).
fof(ax,axiom, vS106_AC___U_RESET_1 <=> (vS106_AC___XU_EXE_0 & vS106_AC___XU_AK_1)).
fof(ax,axiom, vS106_BS_NP____U_JS_1 <=> (~ vS106_BS_NP____U_CAN_0 & (~ vS106_BS_NP____U_JR_0 & (~ vS106_BS_NP____U_INHIBIT_0 & (vS106_BS_NP____U_SEL_0 | vS106_BS_NP____U_JS_0))))).
fof(ax,axiom, vS106_BS_NP____U_AK_1 <=> vS106_BS_NP____U_JS_1).
fof(ax,axiom, vS106_BS_NP____U_SET_1 <=> (vS106_BS_NP____U_EXE_0 & vS106_BS_NP____U_AK_1)).
fof(ax,axiom, vS106_BS_NP____XU_JS_1 <=> (~ vS106_BS_NP____XU_CAN_0 & (~ vS106_BS_NP____XU_JR_0 & (vS106_BS_NP____U_INHIBIT_0 & (vS106_BS_NP____XU_SEL_0 | vS106_BS_NP____XU_JS_0))))).
fof(ax,axiom, vS106_BS_NP____XU_AK_1 <=> vS106_BS_NP____XU_JS_1).
fof(ax,axiom, vS106_BS_NP____U_RESET_1 <=> (vS106_BS_NP____XU_EXE_0 & vS106_BS_NP____XU_AK_1)).
fof(ax,axiom, vS106_BS_P____U_JS_1 <=> (~ vS106_BS_P____U_CAN_0 & (~ vS106_BS_P____U_JR_0 & (~ vS106_BS_P____U_INHIBIT_0 & (vS106_BS_P____U_SEL_0 | vS106_BS_P____U_JS_0))))).
fof(ax,axiom, vS106_BS_P____U_AK_1 <=> vS106_BS_P____U_JS_1).
fof(ax,axiom, vS106_BS_P____U_SET_1 <=> (vS106_BS_P____U_EXE_0 & vS106_BS_P____U_AK_1)).
fof(ax,axiom, vS106_BS_P____XU_JS_1 <=> (~ vS106_BS_P____XU_CAN_0 & (~ vS106_BS_P____XU_JR_0 & (vS106_BS_P____U_INHIBIT_0 & (vS106_BS_P____XU_SEL_0 | vS106_BS_P____XU_JS_0))))).
fof(ax,axiom, vS106_BS_P____XU_AK_1 <=> vS106_BS_P____XU_JS_1).
fof(ax,axiom, vS106_BS_P____U_RESET_1 <=> (vS106_BS_P____XU_EXE_0 & vS106_BS_P____XU_AK_1)).
fof(ax,axiom, vS106_CM___U_JS_1 <=> (~ vS106_CM___U_CAN_0 & (~ vS106_CM___U_JR_0 & (~ vS106_CM___U_INHIBIT_0 & (vS106_CM___U_SEL_0 | vS106_CM___U_JS_0))))).
fof(ax,axiom, vS106_CM___U_AK_1 <=> vS106_CM___U_JS_1).
fof(ax,axiom, vS106_CM___U_SET_1 <=> (vS106_CM___U_EXE_0 & vS106_CM___U_AK_1)).
fof(ax,axiom, vS106_CM___XU_JS_1 <=> (~ vS106_CM___XU_CAN_0 & (~ vS106_CM___XU_JR_0 & (vS106_CM___U_INHIBIT_0 & (vS106_CM___XU_SEL_0 | vS106_CM___XU_JS_0))))).
fof(ax,axiom, vS106_CM___XU_AK_1 <=> vS106_CM___XU_JS_1).
fof(ax,axiom, vS106_CM___U_RESET_1 <=> (vS106_CM___XU_EXE_0 & vS106_CM___XU_AK_1)).
fof(ax,axiom, vS106_DS_NP____U_JS_1 <=> (~ vS106_DS_NP____U_CAN_0 & (~ vS106_DS_NP____U_JR_0 & (~ vS106_DS_NP____U_INHIBIT_0 & (vS106_DS_NP____U_SEL_0 | vS106_DS_NP____U_JS_0))))).
fof(ax,axiom, vS106_DS_NP____U_AK_1 <=> vS106_DS_NP____U_JS_1).
fof(ax,axiom, vS106_DS_NP____U_SET_1 <=> (vS106_DS_NP____U_EXE_0 & vS106_DS_NP____U_AK_1)).
fof(ax,axiom, vS106_DS_NP____XU_JS_1 <=> (~ vS106_DS_NP____XU_CAN_0 & (~ vS106_DS_NP____XU_JR_0 & (vS106_DS_NP____U_INHIBIT_0 & (vS106_DS_NP____XU_SEL_0 | vS106_DS_NP____XU_JS_0))))).
fof(ax,axiom, vS106_DS_NP____XU_AK_1 <=> vS106_DS_NP____XU_JS_1).
fof(ax,axiom, vS106_DS_NP____U_RESET_1 <=> (vS106_DS_NP____XU_EXE_0 & vS106_DS_NP____XU_AK_1)).
fof(ax,axiom, vS106_EM___U_JS_1 <=> (~ vS106_EM___U_CAN_0 & (~ vS106_EM___U_JR_0 & (~ vS106_EM___U_INHIBIT_0 & (vS106_EM___U_SEL_0 | vS106_EM___U_JS_0))))).
fof(ax,axiom, vS106_EM___U_AK_1 <=> vS106_EM___U_JS_1).
fof(ax,axiom, vS106_EM___U_SET_1 <=> (vS106_EM___U_EXE_0 & vS106_EM___U_AK_1)).
fof(ax,axiom, vS106_EM___XU_JS_1 <=> (~ vS106_EM___XU_CAN_0 & (~ vS106_EM___XU_JR_0 & (vS106_EM___U_INHIBIT_0 & (vS106_EM___XU_SEL_0 | vS106_EM___XU_JS_0))))).
fof(ax,axiom, vS106_EM___XU_AK_1 <=> vS106_EM___XU_JS_1).
fof(ax,axiom, vS106_EM___U_RESET_1 <=> (vS106_EM___XU_EXE_0 & vS106_EM___XU_AK_1)).
fof(ax,axiom, vS106_FS_P____U_JS_1 <=> (~ vS106_FS_P____U_CAN_0 & (~ vS106_FS_P____U_JR_0 & (~ vS106_FS_P____U_INHIBIT_0 & (vS106_FS_P____U_SEL_0 | vS106_FS_P____U_JS_0))))).
fof(ax,axiom, vS106_FS_P____U_AK_1 <=> vS106_FS_P____U_JS_1).
fof(ax,axiom, vS106_FS_P____U_SET_1 <=> (vS106_FS_P____U_EXE_0 & vS106_FS_P____U_AK_1)).
fof(ax,axiom, vS106_FS_P____XU_JS_1 <=> (~ vS106_FS_P____XU_CAN_0 & (~ vS106_FS_P____XU_JR_0 & (vS106_FS_P____U_INHIBIT_0 & (vS106_FS_P____XU_SEL_0 | vS106_FS_P____XU_JS_0))))).
fof(ax,axiom, vS106_FS_P____XU_AK_1 <=> vS106_FS_P____XU_JS_1).
fof(ax,axiom, vS106_FS_P____U_RESET_1 <=> (vS106_FS_P____XU_EXE_0 & vS106_FS_P____XU_AK_1)).
fof(ax,axiom, vS106_GM___U_JS_1 <=> (~ vS106_GM___U_CAN_0 & (~ vS106_GM___U_JR_0 & (~ vS106_GM___U_INHIBIT_0 & (vS106_GM___U_SEL_0 | vS106_GM___U_JS_0))))).
fof(ax,axiom, vS106_GM___U_AK_1 <=> vS106_GM___U_JS_1).
fof(ax,axiom, vS106_GM___U_SET_1 <=> (vS106_GM___U_EXE_0 & vS106_GM___U_AK_1)).
fof(ax,axiom, vS106_GM___XU_JS_1 <=> (~ vS106_GM___XU_CAN_0 & (~ vS106_GM___XU_JR_0 & (vS106_GM___U_INHIBIT_0 & (vS106_GM___XU_SEL_0 | vS106_GM___XU_JS_0))))).
fof(ax,axiom, vS106_GM___XU_AK_1 <=> vS106_GM___XU_JS_1).
fof(ax,axiom, vS106_GM___U_RESET_1 <=> (vS106_GM___XU_EXE_0 & vS106_GM___XU_AK_1)).
fof(ax,axiom, vS106_GC___U_JS_1 <=> (~ vS106_GC___U_CAN_0 & (~ vS106_GC___U_JR_0 & (~ vS106_GC___U_INHIBIT_0 & (vS106_GC___U_SEL_0 | vS106_GC___U_JS_0))))).
fof(ax,axiom, vS106_GC___U_AK_1 <=> vS106_GC___U_JS_1).
fof(ax,axiom, vS106_GC___U_SET_1 <=> (vS106_GC___U_EXE_0 & vS106_GC___U_AK_1)).
fof(ax,axiom, vS106_GC___XU_JS_1 <=> (~ vS106_GC___XU_CAN_0 & (~ vS106_GC___XU_JR_0 & (vS106_GC___U_INHIBIT_0 & (vS106_GC___XU_SEL_0 | vS106_GC___XU_JS_0))))).
fof(ax,axiom, vS106_GC___XU_AK_1 <=> vS106_GC___XU_JS_1).
fof(ax,axiom, vS106_GC___U_RESET_1 <=> (vS106_GC___XU_EXE_0 & vS106_GC___XU_AK_1)).
fof(ax,axiom, vS106_HM___U_JS_1 <=> (~ vS106_HM___U_CAN_0 & (~ vS106_HM___U_JR_0 & (~ vS106_HM___U_INHIBIT_0 & (vS106_HM___U_SEL_0 | vS106_HM___U_JS_0))))).
fof(ax,axiom, vS106_HM___U_AK_1 <=> vS106_HM___U_JS_1).
fof(ax,axiom, vS106_HM___U_SET_1 <=> (vS106_HM___U_EXE_0 & vS106_HM___U_AK_1)).
fof(ax,axiom, vS106_HM___XU_JS_1 <=> (~ vS106_HM___XU_CAN_0 & (~ vS106_HM___XU_JR_0 & (vS106_HM___U_INHIBIT_0 & (vS106_HM___XU_SEL_0 | vS106_HM___XU_JS_0))))).
fof(ax,axiom, vS106_HM___XU_AK_1 <=> vS106_HM___XU_JS_1).
fof(ax,axiom, vS106_HM___U_RESET_1 <=> (vS106_HM___XU_EXE_0 & vS106_HM___XU_AK_1)).
fof(ax,axiom, vS106_HC___U_JS_1 <=> (~ vS106_HC___U_CAN_0 & (~ vS106_HC___U_JR_0 & (~ vS106_HC___U_INHIBIT_0 & (vS106_HC___U_SEL_0 | vS106_HC___U_JS_0))))).
fof(ax,axiom, vS106_HC___U_AK_1 <=> vS106_HC___U_JS_1).
fof(ax,axiom, vS106_HC___U_SET_1 <=> (vS106_HC___U_EXE_0 & vS106_HC___U_AK_1)).
fof(ax,axiom, vS106_HC___XU_JS_1 <=> (~ vS106_HC___XU_CAN_0 & (~ vS106_HC___XU_JR_0 & (vS106_HC___U_INHIBIT_0 & (vS106_HC___XU_SEL_0 | vS106_HC___XU_JS_0))))).
fof(ax,axiom, vS106_HC___XU_AK_1 <=> vS106_HC___XU_JS_1).
fof(ax,axiom, vS106_HC___U_RESET_1 <=> (vS106_HC___XU_EXE_0 & vS106_HC___XU_AK_1)).
fof(ax,axiom, vS110_AM___U_JS_1 <=> (~ vS110_AM___U_CAN_0 & (~ vS110_AM___U_JR_0 & (~ vS110_AM___U_INHIBIT_0 & (vS110_AM___U_SEL_0 | vS110_AM___U_JS_0))))).
fof(ax,axiom, vS110_AM___U_AK_1 <=> vS110_AM___U_JS_1).
fof(ax,axiom, vS110_AM___U_SET_1 <=> (vS110_AM___U_EXE_0 & vS110_AM___U_AK_1)).
fof(ax,axiom, vS110_AM___XU_JS_1 <=> (~ vS110_AM___XU_CAN_0 & (~ vS110_AM___XU_JR_0 & (vS110_AM___U_INHIBIT_0 & (vS110_AM___XU_SEL_0 | vS110_AM___XU_JS_0))))).
fof(ax,axiom, vS110_AM___XU_AK_1 <=> vS110_AM___XU_JS_1).
fof(ax,axiom, vS110_AM___U_RESET_1 <=> (vS110_AM___XU_EXE_0 & vS110_AM___XU_AK_1)).
fof(ax,axiom, vP1602__NWD_JS_1 <=> (~ vP1602__NWD_CAN_0 & (~ vP1602__NWD_JR_0 & (~ vP1602__NW_INHIBIT_0 & (vP1602__NWD_SEL_0 | vP1602__NWD_JS_0))))).
fof(ax,axiom, vP1602__NWD_AK_1 <=> vP1602__NWD_JS_1).
fof(ax,axiom, vP1602__NWD_SET_1 <=> (vP1602__NWD_EXE_0 & vP1602__NWD_AK_1)).
fof(ax,axiom, vP1602__XNWD_JS_1 <=> (~ vP1602__XNWD_CAN_0 & (~ vP1602__XNWD_JR_0 & (vP1602__NW_INHIBIT_0 & (vP1602__XNWD_SEL_0 | vP1602__XNWD_JS_0))))).
fof(ax,axiom, vP1602__XNWD_AK_1 <=> vP1602__XNWD_JS_1).
fof(ax,axiom, vP1602__NWD_RESET_1 <=> (vP1602__XNWD_EXE_0 & vP1602__XNWD_AK_1)).
fof(ax,axiom, vP1602__RWD_JS_1 <=> (~ vP1602__RWD_CAN_0 & (~ vP1602__RWD_JR_0 & (~ vP1602__RW_INHIBIT_0 & (vP1602__RWD_SEL_0 | vP1602__RWD_JS_0))))).
fof(ax,axiom, vP1602__RWD_AK_1 <=> vP1602__RWD_JS_1).
fof(ax,axiom, vP1602__RWD_SET_1 <=> (vP1602__RWD_EXE_0 & vP1602__RWD_AK_1)).
fof(ax,axiom, vP1602__XRWD_JS_1 <=> (~ vP1602__XRWD_CAN_0 & (~ vP1602__XRWD_JR_0 & (vP1602__RW_INHIBIT_0 & (vP1602__XRWD_SEL_0 | vP1602__XRWD_JS_0))))).
fof(ax,axiom, vP1602__XRWD_AK_1 <=> vP1602__XRWD_JS_1).
fof(ax,axiom, vP1602__RWD_RESET_1 <=> (vP1602__XRWD_EXE_0 & vP1602__XRWD_AK_1)).
fof(ax,axiom, vP1604__NWD_JS_1 <=> (~ vP1604__NWD_CAN_0 & (~ vP1604__NWD_JR_0 & (~ vP1604__NW_INHIBIT_0 & (vP1604__NWD_SEL_0 | vP1604__NWD_JS_0))))).
fof(ax,axiom, vP1604__NWD_AK_1 <=> vP1604__NWD_JS_1).
fof(ax,axiom, vP1604__NWD_SET_1 <=> (vP1604__NWD_EXE_0 & vP1604__NWD_AK_1)).
fof(ax,axiom, vP1604__XNWD_JS_1 <=> (~ vP1604__XNWD_CAN_0 & (~ vP1604__XNWD_JR_0 & (vP1604__NW_INHIBIT_0 & (vP1604__XNWD_SEL_0 | vP1604__XNWD_JS_0))))).
fof(ax,axiom, vP1604__XNWD_AK_1 <=> vP1604__XNWD_JS_1).
fof(ax,axiom, vP1604__NWD_RESET_1 <=> (vP1604__XNWD_EXE_0 & vP1604__XNWD_AK_1)).
fof(ax,axiom, vP1604__RWD_JS_1 <=> (~ vP1604__RWD_CAN_0 & (~ vP1604__RWD_JR_0 & (~ vP1604__RW_INHIBIT_0 & (vP1604__RWD_SEL_0 | vP1604__RWD_JS_0))))).
fof(ax,axiom, vP1604__RWD_AK_1 <=> vP1604__RWD_JS_1).
fof(ax,axiom, vP1604__RWD_SET_1 <=> (vP1604__RWD_EXE_0 & vP1604__RWD_AK_1)).
fof(ax,axiom, vP1604__XRWD_JS_1 <=> (~ vP1604__XRWD_CAN_0 & (~ vP1604__XRWD_JR_0 & (vP1604__RW_INHIBIT_0 & (vP1604__XRWD_SEL_0 | vP1604__XRWD_JS_0))))).
fof(ax,axiom, vP1604__XRWD_AK_1 <=> vP1604__XRWD_JS_1).
fof(ax,axiom, vP1604__RWD_RESET_1 <=> (vP1604__XRWD_EXE_0 & vP1604__XRWD_AK_1)).
fof(ax,axiom, vP1606__NWD_JS_1 <=> (~ vP1606__NWD_CAN_0 & (~ vP1606__NWD_JR_0 & (~ vP1606__NW_INHIBIT_0 & (vP1606__NWD_SEL_0 | vP1606__NWD_JS_0))))).
fof(ax,axiom, vP1606__NWD_AK_1 <=> vP1606__NWD_JS_1).
fof(ax,axiom, vP1606__NWD_SET_1 <=> (vP1606__NWD_EXE_0 & vP1606__NWD_AK_1)).
fof(ax,axiom, vP1606__XNWD_JS_1 <=> (~ vP1606__XNWD_CAN_0 & (~ vP1606__XNWD_JR_0 & (vP1606__NW_INHIBIT_0 & (vP1606__XNWD_SEL_0 | vP1606__XNWD_JS_0))))).
fof(ax,axiom, vP1606__XNWD_AK_1 <=> vP1606__XNWD_JS_1).
fof(ax,axiom, vP1606__NWD_RESET_1 <=> (vP1606__XNWD_EXE_0 & vP1606__XNWD_AK_1)).
fof(ax,axiom, vP1606__RWD_JS_1 <=> (~ vP1606__RWD_CAN_0 & (~ vP1606__RWD_JR_0 & (~ vP1606__RW_INHIBIT_0 & (vP1606__RWD_SEL_0 | vP1606__RWD_JS_0))))).
fof(ax,axiom, vP1606__RWD_AK_1 <=> vP1606__RWD_JS_1).
fof(ax,axiom, vP1606__RWD_SET_1 <=> (vP1606__RWD_EXE_0 & vP1606__RWD_AK_1)).
fof(ax,axiom, vP1606__XRWD_JS_1 <=> (~ vP1606__XRWD_CAN_0 & (~ vP1606__XRWD_JR_0 & (vP1606__RW_INHIBIT_0 & (vP1606__XRWD_SEL_0 | vP1606__XRWD_JS_0))))).
fof(ax,axiom, vP1606__XRWD_AK_1 <=> vP1606__XRWD_JS_1).
fof(ax,axiom, vP1606__RWD_RESET_1 <=> (vP1606__XRWD_EXE_0 & vP1606__XRWD_AK_1)).
fof(ax,axiom, vP1608__NWD_JS_1 <=> (~ vP1608__NWD_CAN_0 & (~ vP1608__NWD_JR_0 & (~ vP1608__NW_INHIBIT_0 & (vP1608__NWD_SEL_0 | vP1608__NWD_JS_0))))).
fof(ax,axiom, vP1608__NWD_AK_1 <=> vP1608__NWD_JS_1).
fof(ax,axiom, vP1608__NWD_SET_1 <=> (vP1608__NWD_EXE_0 & vP1608__NWD_AK_1)).
fof(ax,axiom, vP1608__XNWD_JS_1 <=> (~ vP1608__XNWD_CAN_0 & (~ vP1608__XNWD_JR_0 & (vP1608__NW_INHIBIT_0 & (vP1608__XNWD_SEL_0 | vP1608__XNWD_JS_0))))).
fof(ax,axiom, vP1608__XNWD_AK_1 <=> vP1608__XNWD_JS_1).
fof(ax,axiom, vP1608__NWD_RESET_1 <=> (vP1608__XNWD_EXE_0 & vP1608__XNWD_AK_1)).
fof(ax,axiom, vP1608__RWD_JS_1 <=> (~ vP1608__RWD_CAN_0 & (~ vP1608__RWD_JR_0 & (~ vP1608__RW_INHIBIT_0 & (vP1608__RWD_SEL_0 | vP1608__RWD_JS_0))))).
fof(ax,axiom, vP1608__RWD_AK_1 <=> vP1608__RWD_JS_1).
fof(ax,axiom, vP1608__RWD_SET_1 <=> (vP1608__RWD_EXE_0 & vP1608__RWD_AK_1)).
fof(ax,axiom, vP1608__XRWD_JS_1 <=> (~ vP1608__XRWD_CAN_0 & (~ vP1608__XRWD_JR_0 & (vP1608__RW_INHIBIT_0 & (vP1608__XRWD_SEL_0 | vP1608__XRWD_JS_0))))).
fof(ax,axiom, vP1608__XRWD_AK_1 <=> vP1608__XRWD_JS_1).
fof(ax,axiom, vP1608__RWD_RESET_1 <=> (vP1608__XRWD_EXE_0 & vP1608__XRWD_AK_1)).
fof(ax,axiom, vP1620__NWD_JS_1 <=> (~ vP1620__NWD_CAN_0 & (~ vP1620__NWD_JR_0 & (~ vP1620__NW_INHIBIT_0 & (vP1620__NWD_SEL_0 | vP1620__NWD_JS_0))))).
fof(ax,axiom, vP1620__NWD_AK_1 <=> vP1620__NWD_JS_1).
fof(ax,axiom, vP1620__NWD_SET_1 <=> (vP1620__NWD_EXE_0 & vP1620__NWD_AK_1)).
fof(ax,axiom, vP1620__XNWD_JS_1 <=> (~ vP1620__XNWD_CAN_0 & (~ vP1620__XNWD_JR_0 & (vP1620__NW_INHIBIT_0 & (vP1620__XNWD_SEL_0 | vP1620__XNWD_JS_0))))).
fof(ax,axiom, vP1620__XNWD_AK_1 <=> vP1620__XNWD_JS_1).
fof(ax,axiom, vP1620__NWD_RESET_1 <=> (vP1620__XNWD_EXE_0 & vP1620__XNWD_AK_1)).
fof(ax,axiom, vP1620__RWD_JS_1 <=> (~ vP1620__RWD_CAN_0 & (~ vP1620__RWD_JR_0 & (~ vP1620__RW_INHIBIT_0 & (vP1620__RWD_SEL_0 | vP1620__RWD_JS_0))))).
fof(ax,axiom, vP1620__RWD_AK_1 <=> vP1620__RWD_JS_1).
fof(ax,axiom, vP1620__RWD_SET_1 <=> (vP1620__RWD_EXE_0 & vP1620__RWD_AK_1)).
fof(ax,axiom, vP1620__XRWD_JS_1 <=> (~ vP1620__XRWD_CAN_0 & (~ vP1620__XRWD_JR_0 & (vP1620__RW_INHIBIT_0 & (vP1620__XRWD_SEL_0 | vP1620__XRWD_JS_0))))).
fof(ax,axiom, vP1620__XRWD_AK_1 <=> vP1620__XRWD_JS_1).
fof(ax,axiom, vP1620__RWD_RESET_1 <=> (vP1620__XRWD_EXE_0 & vP1620__XRWD_AK_1)).
fof(ax,axiom, vP1622__NWD_JS_1 <=> (~ vP1622__NWD_CAN_0 & (~ vP1622__NWD_JR_0 & (~ vP1622__NW_INHIBIT_0 & (vP1622__NWD_SEL_0 | vP1622__NWD_JS_0))))).
fof(ax,axiom, vP1622__NWD_AK_1 <=> vP1622__NWD_JS_1).
fof(ax,axiom, vP1622__NWD_SET_1 <=> (vP1622__NWD_EXE_0 & vP1622__NWD_AK_1)).
fof(ax,axiom, vP1622__XNWD_JS_1 <=> (~ vP1622__XNWD_CAN_0 & (~ vP1622__XNWD_JR_0 & (vP1622__NW_INHIBIT_0 & (vP1622__XNWD_SEL_0 | vP1622__XNWD_JS_0))))).
fof(ax,axiom, vP1622__XNWD_AK_1 <=> vP1622__XNWD_JS_1).
fof(ax,axiom, vP1622__NWD_RESET_1 <=> (vP1622__XNWD_EXE_0 & vP1622__XNWD_AK_1)).
fof(ax,axiom, vP1622__RWD_JS_1 <=> (~ vP1622__RWD_CAN_0 & (~ vP1622__RWD_JR_0 & (~ vP1622__RW_INHIBIT_0 & (vP1622__RWD_SEL_0 | vP1622__RWD_JS_0))))).
fof(ax,axiom, vP1622__RWD_AK_1 <=> vP1622__RWD_JS_1).
fof(ax,axiom, vP1622__RWD_SET_1 <=> (vP1622__RWD_EXE_0 & vP1622__RWD_AK_1)).
fof(ax,axiom, vP1622__XRWD_JS_1 <=> (~ vP1622__XRWD_CAN_0 & (~ vP1622__XRWD_JR_0 & (vP1622__RW_INHIBIT_0 & (vP1622__XRWD_SEL_0 | vP1622__XRWD_JS_0))))).
fof(ax,axiom, vP1622__XRWD_AK_1 <=> vP1622__XRWD_JS_1).
fof(ax,axiom, vP1622__RWD_RESET_1 <=> (vP1622__XRWD_EXE_0 & vP1622__XRWD_AK_1)).
fof(ax,axiom, vP1624__NWD_JS_1 <=> (~ vP1624__NWD_CAN_0 & (~ vP1624__NWD_JR_0 & (~ vP1624__NW_INHIBIT_0 & (vP1624__NWD_SEL_0 | vP1624__NWD_JS_0))))).
fof(ax,axiom, vP1624__NWD_AK_1 <=> vP1624__NWD_JS_1).
fof(ax,axiom, vP1624__NWD_SET_1 <=> (vP1624__NWD_EXE_0 & vP1624__NWD_AK_1)).
fof(ax,axiom, vP1624__XNWD_JS_1 <=> (~ vP1624__XNWD_CAN_0 & (~ vP1624__XNWD_JR_0 & (vP1624__NW_INHIBIT_0 & (vP1624__XNWD_SEL_0 | vP1624__XNWD_JS_0))))).
fof(ax,axiom, vP1624__XNWD_AK_1 <=> vP1624__XNWD_JS_1).
fof(ax,axiom, vP1624__NWD_RESET_1 <=> (vP1624__XNWD_EXE_0 & vP1624__XNWD_AK_1)).
fof(ax,axiom, vP1624__RWD_JS_1 <=> (~ vP1624__RWD_CAN_0 & (~ vP1624__RWD_JR_0 & (~ vP1624__RW_INHIBIT_0 & (vP1624__RWD_SEL_0 | vP1624__RWD_JS_0))))).
fof(ax,axiom, vP1624__RWD_AK_1 <=> vP1624__RWD_JS_1).
fof(ax,axiom, vP1624__RWD_SET_1 <=> (vP1624__RWD_EXE_0 & vP1624__RWD_AK_1)).
fof(ax,axiom, vP1624__XRWD_JS_1 <=> (~ vP1624__XRWD_CAN_0 & (~ vP1624__XRWD_JR_0 & (vP1624__RW_INHIBIT_0 & (vP1624__XRWD_SEL_0 | vP1624__XRWD_JS_0))))).
fof(ax,axiom, vP1624__XRWD_AK_1 <=> vP1624__XRWD_JS_1).
fof(ax,axiom, vP1624__RWD_RESET_1 <=> (vP1624__XRWD_EXE_0 & vP1624__XRWD_AK_1)).
fof(ax,axiom, vS100__ASP_JS_1 <=> (~ vS100__ASP_CAN_0 & (~ vS100__ASP_JR_0 & (~ vS100__ASP_INHIBIT_0 & (vS100__ASP_SEL_0 | vS100__ASP_JS_0))))).
fof(ax,axiom, vS100__ASP_AK_1 <=> vS100__ASP_JS_1).
fof(ax,axiom, vS100__ASP_SET_1 <=> (vS100__ASP_EXE_0 & vS100__ASP_AK_1)).
fof(ax,axiom, vS100__XASP_JS_1 <=> (~ vS100__XASP_CAN_0 & (~ vS100__XASP_JR_0 & (vS100__ASP_INHIBIT_0 & (vS100__XASP_SEL_0 | vS100__XASP_JS_0))))).
fof(ax,axiom, vS100__XASP_AK_1 <=> vS100__XASP_JS_1).
fof(ax,axiom, vS100__ASP_RESET_1 <=> (vS100__XASP_EXE_0 & vS100__XASP_AK_1)).
fof(ax,axiom, vS102__ASP_JS_1 <=> (~ vS102__ASP_CAN_0 & (~ vS102__ASP_JR_0 & (~ vS102__ASP_INHIBIT_0 & (vS102__ASP_SEL_0 | vS102__ASP_JS_0))))).
fof(ax,axiom, vS102__ASP_AK_1 <=> vS102__ASP_JS_1).
fof(ax,axiom, vS102__ASP_SET_1 <=> (vS102__ASP_EXE_0 & vS102__ASP_AK_1)).
fof(ax,axiom, vS102__XASP_JS_1 <=> (~ vS102__XASP_CAN_0 & (~ vS102__XASP_JR_0 & (vS102__ASP_INHIBIT_0 & (vS102__XASP_SEL_0 | vS102__XASP_JS_0))))).
fof(ax,axiom, vS102__XASP_AK_1 <=> vS102__XASP_JS_1).
fof(ax,axiom, vS102__ASP_RESET_1 <=> (vS102__XASP_EXE_0 & vS102__XASP_AK_1)).
fof(ax,axiom, vS104__ASP_JS_1 <=> (~ vS104__ASP_CAN_0 & (~ vS104__ASP_JR_0 & (~ vS104__ASP_INHIBIT_0 & (vS104__ASP_SEL_0 | vS104__ASP_JS_0))))).
fof(ax,axiom, vS104__ASP_AK_1 <=> vS104__ASP_JS_1).
fof(ax,axiom, vS104__ASP_SET_1 <=> (vS104__ASP_EXE_0 & vS104__ASP_AK_1)).
fof(ax,axiom, vS104__XASP_JS_1 <=> (~ vS104__XASP_CAN_0 & (~ vS104__XASP_JR_0 & (vS104__ASP_INHIBIT_0 & (vS104__XASP_SEL_0 | vS104__XASP_JS_0))))).
fof(ax,axiom, vS104__XASP_AK_1 <=> vS104__XASP_JS_1).
fof(ax,axiom, vS104__ASP_RESET_1 <=> (vS104__XASP_EXE_0 & vS104__XASP_AK_1)).
fof(ax,axiom, vS106__ASP_JS_1 <=> (~ vS106__ASP_CAN_0 & (~ vS106__ASP_JR_0 & (~ vS106__ASP_INHIBIT_0 & (vS106__ASP_SEL_0 | vS106__ASP_JS_0))))).
fof(ax,axiom, vS106__ASP_AK_1 <=> vS106__ASP_JS_1).
fof(ax,axiom, vS106__ASP_SET_1 <=> (vS106__ASP_EXE_0 & vS106__ASP_AK_1)).
fof(ax,axiom, vS106__XASP_JS_1 <=> (~ vS106__XASP_CAN_0 & (~ vS106__XASP_JR_0 & (vS106__ASP_INHIBIT_0 & (vS106__XASP_SEL_0 | vS106__XASP_JS_0))))).
fof(ax,axiom, vS106__XASP_AK_1 <=> vS106__XASP_JS_1).
fof(ax,axiom, vS106__ASP_RESET_1 <=> (vS106__XASP_EXE_0 & vS106__XASP_AK_1)).
fof(ax,axiom, vS110__ASP_JS_1 <=> (~ vS110__ASP_CAN_0 & (~ vS110__ASP_JR_0 & (~ vS110__ASP_INHIBIT_0 & (vS110__ASP_SEL_0 | vS110__ASP_JS_0))))).
fof(ax,axiom, vS110__ASP_AK_1 <=> vS110__ASP_JS_1).
fof(ax,axiom, vS110__ASP_SET_1 <=> (vS110__ASP_EXE_0 & vS110__ASP_AK_1)).
fof(ax,axiom, vS110__XASP_JS_1 <=> (~ vS110__XASP_CAN_0 & (~ vS110__XASP_JR_0 & (vS110__ASP_INHIBIT_0 & (vS110__XASP_SEL_0 | vS110__XASP_JS_0))))).
fof(ax,axiom, vS110__XASP_AK_1 <=> vS110__XASP_JS_1).
fof(ax,axiom, vS110__ASP_RESET_1 <=> (vS110__XASP_EXE_0 & vS110__XASP_AK_1)).
fof(ax,axiom, vTAA__OCC_JS_1 <=> (~ vTAA__OCC_CAN_0 & (~ vTAA__OCC_JR_0 & (~ vTAA_OCC_TF__0 & (vTAA__OCC_SEL_0 | vTAA__OCC_JS_0))))).
fof(ax,axiom, vTAA__OCC_AK_1 <=> vTAA__OCC_JS_1).
fof(ax,axiom, vTAA__OCC_SET_1 <=> (vTAA__OCC_EXE_0 & vTAA__OCC_AK_1)).
fof(ax,axiom, vTAA__XOCC_JS_1 <=> (~ vTAA__XOCC_CAN_0 & (~ vTAA__XOCC_JR_0 & (vTAA_OCC_TF__0 & (vTAA__XOCC_SEL_0 | vTAA__XOCC_JS_0))))).
fof(ax,axiom, vTAA__XOCC_AK_1 <=> vTAA__XOCC_JS_1).
fof(ax,axiom, vTAA__OCC_RESET_1 <=> (vTAA__XOCC_EXE_0 & vTAA__XOCC_AK_1)).
fof(ax,axiom, vTAB__OCC_JS_1 <=> (~ vTAB__OCC_CAN_0 & (~ vTAB__OCC_JR_0 & (~ vTAB_OCC_TF__0 & (vTAB__OCC_SEL_0 | vTAB__OCC_JS_0))))).
fof(ax,axiom, vTAB__OCC_AK_1 <=> vTAB__OCC_JS_1).
fof(ax,axiom, vTAB__OCC_SET_1 <=> (vTAB__OCC_EXE_0 & vTAB__OCC_AK_1)).
fof(ax,axiom, vTAB__XOCC_JS_1 <=> (~ vTAB__XOCC_CAN_0 & (~ vTAB__XOCC_JR_0 & (vTAB_OCC_TF__0 & (vTAB__XOCC_SEL_0 | vTAB__XOCC_JS_0))))).
fof(ax,axiom, vTAB__XOCC_AK_1 <=> vTAB__XOCC_JS_1).
fof(ax,axiom, vTAB__OCC_RESET_1 <=> (vTAB__XOCC_EXE_0 & vTAB__XOCC_AK_1)).
fof(ax,axiom, vTAC__OCC_JS_1 <=> (~ vTAC__OCC_CAN_0 & (~ vTAC__OCC_JR_0 & (~ vTAC_OCC_TF__0 & (vTAC__OCC_SEL_0 | vTAC__OCC_JS_0))))).
fof(ax,axiom, vTAC__OCC_AK_1 <=> vTAC__OCC_JS_1).
fof(ax,axiom, vTAC__OCC_SET_1 <=> (vTAC__OCC_EXE_0 & vTAC__OCC_AK_1)).
fof(ax,axiom, vTAC__XOCC_JS_1 <=> (~ vTAC__XOCC_CAN_0 & (~ vTAC__XOCC_JR_0 & (vTAC_OCC_TF__0 & (vTAC__XOCC_SEL_0 | vTAC__XOCC_JS_0))))).
fof(ax,axiom, vTAC__XOCC_AK_1 <=> vTAC__XOCC_JS_1).
fof(ax,axiom, vTAC__OCC_RESET_1 <=> (vTAC__XOCC_EXE_0 & vTAC__XOCC_AK_1)).
fof(ax,axiom, vTAD__OCC_JS_1 <=> (~ vTAD__OCC_CAN_0 & (~ vTAD__OCC_JR_0 & (~ vTAD_OCC_TF__0 & (vTAD__OCC_SEL_0 | vTAD__OCC_JS_0))))).
fof(ax,axiom, vTAD__OCC_AK_1 <=> vTAD__OCC_JS_1).
fof(ax,axiom, vTAD__OCC_SET_1 <=> (vTAD__OCC_EXE_0 & vTAD__OCC_AK_1)).
fof(ax,axiom, vTAD__XOCC_JS_1 <=> (~ vTAD__XOCC_CAN_0 & (~ vTAD__XOCC_JR_0 & (vTAD_OCC_TF__0 & (vTAD__XOCC_SEL_0 | vTAD__XOCC_JS_0))))).
fof(ax,axiom, vTAD__XOCC_AK_1 <=> vTAD__XOCC_JS_1).
fof(ax,axiom, vTAD__OCC_RESET_1 <=> (vTAD__XOCC_EXE_0 & vTAD__XOCC_AK_1)).
fof(ax,axiom, vTAE__OCC_JS_1 <=> (~ vTAE__OCC_CAN_0 & (~ vTAE__OCC_JR_0 & (~ vTAE_OCC_TF__0 & (vTAE__OCC_SEL_0 | vTAE__OCC_JS_0))))).
fof(ax,axiom, vTAE__OCC_AK_1 <=> vTAE__OCC_JS_1).
fof(ax,axiom, vTAE__OCC_SET_1 <=> (vTAE__OCC_EXE_0 & vTAE__OCC_AK_1)).
fof(ax,axiom, vTAE__XOCC_JS_1 <=> (~ vTAE__XOCC_CAN_0 & (~ vTAE__XOCC_JR_0 & (vTAE_OCC_TF__0 & (vTAE__XOCC_SEL_0 | vTAE__XOCC_JS_0))))).
fof(ax,axiom, vTAE__XOCC_AK_1 <=> vTAE__XOCC_JS_1).
fof(ax,axiom, vTAE__OCC_RESET_1 <=> (vTAE__XOCC_EXE_0 & vTAE__XOCC_AK_1)).
fof(ax,axiom, vTAF__OCC_JS_1 <=> (~ vTAF__OCC_CAN_0 & (~ vTAF__OCC_JR_0 & (~ vTAF_OCC_TF__0 & (vTAF__OCC_SEL_0 | vTAF__OCC_JS_0))))).
fof(ax,axiom, vTAF__OCC_AK_1 <=> vTAF__OCC_JS_1).
fof(ax,axiom, vTAF__OCC_SET_1 <=> (vTAF__OCC_EXE_0 & vTAF__OCC_AK_1)).
fof(ax,axiom, vTAF__XOCC_JS_1 <=> (~ vTAF__XOCC_CAN_0 & (~ vTAF__XOCC_JR_0 & (vTAF_OCC_TF__0 & (vTAF__XOCC_SEL_0 | vTAF__XOCC_JS_0))))).
fof(ax,axiom, vTAF__XOCC_AK_1 <=> vTAF__XOCC_JS_1).
fof(ax,axiom, vTAF__OCC_RESET_1 <=> (vTAF__XOCC_EXE_0 & vTAF__XOCC_AK_1)).
fof(ax,axiom, vTAG__OCC_JS_1 <=> (~ vTAG__OCC_CAN_0 & (~ vTAG__OCC_JR_0 & (~ vTAG_OCC_TF__0 & (vTAG__OCC_SEL_0 | vTAG__OCC_JS_0))))).
fof(ax,axiom, vTAG__OCC_AK_1 <=> vTAG__OCC_JS_1).
fof(ax,axiom, vTAG__OCC_SET_1 <=> (vTAG__OCC_EXE_0 & vTAG__OCC_AK_1)).
fof(ax,axiom, vTAG__XOCC_JS_1 <=> (~ vTAG__XOCC_CAN_0 & (~ vTAG__XOCC_JR_0 & (vTAG_OCC_TF__0 & (vTAG__XOCC_SEL_0 | vTAG__XOCC_JS_0))))).
fof(ax,axiom, vTAG__XOCC_AK_1 <=> vTAG__XOCC_JS_1).
fof(ax,axiom, vTAG__OCC_RESET_1 <=> (vTAG__XOCC_EXE_0 & vTAG__XOCC_AK_1)).
fof(ax,axiom, vTBA__OCC_JS_1 <=> (~ vTBA__OCC_CAN_0 & (~ vTBA__OCC_JR_0 & (~ vTBA_OCC_TF__0 & (vTBA__OCC_SEL_0 | vTBA__OCC_JS_0))))).
fof(ax,axiom, vTBA__OCC_AK_1 <=> vTBA__OCC_JS_1).
fof(ax,axiom, vTBA__OCC_SET_1 <=> (vTBA__OCC_EXE_0 & vTBA__OCC_AK_1)).
fof(ax,axiom, vTBA__XOCC_JS_1 <=> (~ vTBA__XOCC_CAN_0 & (~ vTBA__XOCC_JR_0 & (vTBA_OCC_TF__0 & (vTBA__XOCC_SEL_0 | vTBA__XOCC_JS_0))))).
fof(ax,axiom, vTBA__XOCC_AK_1 <=> vTBA__XOCC_JS_1).
fof(ax,axiom, vTBA__OCC_RESET_1 <=> (vTBA__XOCC_EXE_0 & vTBA__XOCC_AK_1)).
fof(ax,axiom, vTCA__OCC_JS_1 <=> (~ vTCA__OCC_CAN_0 & (~ vTCA__OCC_JR_0 & (~ vTCA_OCC_TF__0 & (vTCA__OCC_SEL_0 | vTCA__OCC_JS_0))))).
fof(ax,axiom, vTCA__OCC_AK_1 <=> vTCA__OCC_JS_1).
fof(ax,axiom, vTCA__OCC_SET_1 <=> (vTCA__OCC_EXE_0 & vTCA__OCC_AK_1)).
fof(ax,axiom, vTCA__XOCC_JS_1 <=> (~ vTCA__XOCC_CAN_0 & (~ vTCA__XOCC_JR_0 & (vTCA_OCC_TF__0 & (vTCA__XOCC_SEL_0 | vTCA__XOCC_JS_0))))).
fof(ax,axiom, vTCA__XOCC_AK_1 <=> vTCA__XOCC_JS_1).
fof(ax,axiom, vTCA__OCC_RESET_1 <=> (vTCA__XOCC_EXE_0 & vTCA__XOCC_AK_1)).
fof(ax,axiom, vTDA__OCC_JS_1 <=> (~ vTDA__OCC_CAN_0 & (~ vTDA__OCC_JR_0 & (~ vTDA_OCC_TF__0 & (vTDA__OCC_SEL_0 | vTDA__OCC_JS_0))))).
fof(ax,axiom, vTDA__OCC_AK_1 <=> vTDA__OCC_JS_1).
fof(ax,axiom, vTDA__OCC_SET_1 <=> (vTDA__OCC_EXE_0 & vTDA__OCC_AK_1)).
fof(ax,axiom, vTDA__XOCC_JS_1 <=> (~ vTDA__XOCC_CAN_0 & (~ vTDA__XOCC_JR_0 & (vTDA_OCC_TF__0 & (vTDA__XOCC_SEL_0 | vTDA__XOCC_JS_0))))).
fof(ax,axiom, vTDA__XOCC_AK_1 <=> vTDA__XOCC_JS_1).
fof(ax,axiom, vTDA__OCC_RESET_1 <=> (vTDA__XOCC_EXE_0 & vTDA__XOCC_AK_1)).
fof(ax,axiom, vTEA__OCC_JS_1 <=> (~ vTEA__OCC_CAN_0 & (~ vTEA__OCC_JR_0 & (~ vTEA_OCC_TF__0 & (vTEA__OCC_SEL_0 | vTEA__OCC_JS_0))))).
fof(ax,axiom, vTEA__OCC_AK_1 <=> vTEA__OCC_JS_1).
fof(ax,axiom, vTEA__OCC_SET_1 <=> (vTEA__OCC_EXE_0 & vTEA__OCC_AK_1)).
fof(ax,axiom, vTEA__XOCC_JS_1 <=> (~ vTEA__XOCC_CAN_0 & (~ vTEA__XOCC_JR_0 & (vTEA_OCC_TF__0 & (vTEA__XOCC_SEL_0 | vTEA__XOCC_JS_0))))).
fof(ax,axiom, vTEA__XOCC_AK_1 <=> vTEA__XOCC_JS_1).
fof(ax,axiom, vTEA__OCC_RESET_1 <=> (vTEA__XOCC_EXE_0 & vTEA__XOCC_AK_1)).
fof(ax,axiom, vTFA__OCC_JS_1 <=> (~ vTFA__OCC_CAN_0 & (~ vTFA__OCC_JR_0 & (~ vTFA_OCC_TF__0 & (vTFA__OCC_SEL_0 | vTFA__OCC_JS_0))))).
fof(ax,axiom, vTFA__OCC_AK_1 <=> vTFA__OCC_JS_1).
fof(ax,axiom, vTFA__OCC_SET_1 <=> (vTFA__OCC_EXE_0 & vTFA__OCC_AK_1)).
fof(ax,axiom, vTFA__XOCC_JS_1 <=> (~ vTFA__XOCC_CAN_0 & (~ vTFA__XOCC_JR_0 & (vTFA_OCC_TF__0 & (vTFA__XOCC_SEL_0 | vTFA__XOCC_JS_0))))).
fof(ax,axiom, vTFA__XOCC_AK_1 <=> vTFA__XOCC_JS_1).
fof(ax,axiom, vTFA__OCC_RESET_1 <=> (vTFA__XOCC_EXE_0 & vTFA__XOCC_AK_1)).
fof(ax,axiom, vTGA__OCC_JS_1 <=> (~ vTGA__OCC_CAN_0 & (~ vTGA__OCC_JR_0 & (~ vTGA_OCC_TF__0 & (vTGA__OCC_SEL_0 | vTGA__OCC_JS_0))))).
fof(ax,axiom, vTGA__OCC_AK_1 <=> vTGA__OCC_JS_1).
fof(ax,axiom, vTGA__OCC_SET_1 <=> (vTGA__OCC_EXE_0 & vTGA__OCC_AK_1)).
fof(ax,axiom, vTGA__XOCC_JS_1 <=> (~ vTGA__XOCC_CAN_0 & (~ vTGA__XOCC_JR_0 & (vTGA_OCC_TF__0 & (vTGA__XOCC_SEL_0 | vTGA__XOCC_JS_0))))).
fof(ax,axiom, vTGA__XOCC_AK_1 <=> vTGA__XOCC_JS_1).
fof(ax,axiom, vTGA__OCC_RESET_1 <=> (vTGA__XOCC_EXE_0 & vTGA__XOCC_AK_1)).
fof(ax,axiom, vTHA__OCC_JS_1 <=> (~ vTHA__OCC_CAN_0 & (~ vTHA__OCC_JR_0 & (~ vTHA_OCC_TF__0 & (vTHA__OCC_SEL_0 | vTHA__OCC_JS_0))))).
fof(ax,axiom, vTHA__OCC_AK_1 <=> vTHA__OCC_JS_1).
fof(ax,axiom, vTHA__OCC_SET_1 <=> (vTHA__OCC_EXE_0 & vTHA__OCC_AK_1)).
fof(ax,axiom, vTHA__XOCC_JS_1 <=> (~ vTHA__XOCC_CAN_0 & (~ vTHA__XOCC_JR_0 & (vTHA_OCC_TF__0 & (vTHA__XOCC_SEL_0 | vTHA__XOCC_JS_0))))).
fof(ax,axiom, vTHA__XOCC_AK_1 <=> vTHA__XOCC_JS_1).
fof(ax,axiom, vTHA__OCC_RESET_1 <=> (vTHA__XOCC_EXE_0 & vTHA__XOCC_AK_1)).
fof(ax,axiom, vTAA__ISOL_JS_1 <=> (~ vTAA__ISOL_CAN_0 & (~ vTAA__ISOL_JR_0 & (~ vTAA_ISOL_0 & (vTAA__ISOL_SEL_0 | vTAA__ISOL_JS_0))))).
fof(ax,axiom, vTAA__ISOL_AK_1 <=> vTAA__ISOL_JS_1).
fof(ax,axiom, vTAA__ISOL_SET_1 <=> (vTAA__ISOL_EXE_0 & vTAA__ISOL_AK_1)).
fof(ax,axiom, vTAA__XISOL_JS_1 <=> (~ vTAA__XISOL_CAN_0 & (~ vTAA__XISOL_JR_0 & (vTAA_ISOL_0 & (vTAA__XISOL_SEL_0 | vTAA__XISOL_JS_0))))).
fof(ax,axiom, vTAA__XISOL_AK_1 <=> vTAA__XISOL_JS_1).
fof(ax,axiom, vTAA__ISOL_RESET_1 <=> (vTAA__XISOL_EXE_0 & vTAA__XISOL_AK_1)).
fof(ax,axiom, vTAB__ISOL_JS_1 <=> (~ vTAB__ISOL_CAN_0 & (~ vTAB__ISOL_JR_0 & (~ vTAB_ISOL_0 & (vTAB__ISOL_SEL_0 | vTAB__ISOL_JS_0))))).
fof(ax,axiom, vTAB__ISOL_AK_1 <=> vTAB__ISOL_JS_1).
fof(ax,axiom, vTAB__ISOL_SET_1 <=> (vTAB__ISOL_EXE_0 & vTAB__ISOL_AK_1)).
fof(ax,axiom, vTAB__XISOL_JS_1 <=> (~ vTAB__XISOL_CAN_0 & (~ vTAB__XISOL_JR_0 & (vTAB_ISOL_0 & (vTAB__XISOL_SEL_0 | vTAB__XISOL_JS_0))))).
fof(ax,axiom, vTAB__XISOL_AK_1 <=> vTAB__XISOL_JS_1).
fof(ax,axiom, vTAB__ISOL_RESET_1 <=> (vTAB__XISOL_EXE_0 & vTAB__XISOL_AK_1)).
fof(ax,axiom, vTAC__ISOL_JS_1 <=> (~ vTAC__ISOL_CAN_0 & (~ vTAC__ISOL_JR_0 & (~ vTAC_ISOL_0 & (vTAC__ISOL_SEL_0 | vTAC__ISOL_JS_0))))).
fof(ax,axiom, vTAC__ISOL_AK_1 <=> vTAC__ISOL_JS_1).
fof(ax,axiom, vTAC__ISOL_SET_1 <=> (vTAC__ISOL_EXE_0 & vTAC__ISOL_AK_1)).
fof(ax,axiom, vTAC__XISOL_JS_1 <=> (~ vTAC__XISOL_CAN_0 & (~ vTAC__XISOL_JR_0 & (vTAC_ISOL_0 & (vTAC__XISOL_SEL_0 | vTAC__XISOL_JS_0))))).
fof(ax,axiom, vTAC__XISOL_AK_1 <=> vTAC__XISOL_JS_1).
fof(ax,axiom, vTAC__ISOL_RESET_1 <=> (vTAC__XISOL_EXE_0 & vTAC__XISOL_AK_1)).
fof(ax,axiom, vTAD__ISOL_JS_1 <=> (~ vTAD__ISOL_CAN_0 & (~ vTAD__ISOL_JR_0 & (~ vTAD_ISOL_0 & (vTAD__ISOL_SEL_0 | vTAD__ISOL_JS_0))))).
fof(ax,axiom, vTAD__ISOL_AK_1 <=> vTAD__ISOL_JS_1).
fof(ax,axiom, vTAD__ISOL_SET_1 <=> (vTAD__ISOL_EXE_0 & vTAD__ISOL_AK_1)).
fof(ax,axiom, vTAD__XISOL_JS_1 <=> (~ vTAD__XISOL_CAN_0 & (~ vTAD__XISOL_JR_0 & (vTAD_ISOL_0 & (vTAD__XISOL_SEL_0 | vTAD__XISOL_JS_0))))).
fof(ax,axiom, vTAD__XISOL_AK_1 <=> vTAD__XISOL_JS_1).
fof(ax,axiom, vTAD__ISOL_RESET_1 <=> (vTAD__XISOL_EXE_0 & vTAD__XISOL_AK_1)).
fof(ax,axiom, vTAE__ISOL_JS_1 <=> (~ vTAE__ISOL_CAN_0 & (~ vTAE__ISOL_JR_0 & (~ vTAE_ISOL_0 & (vTAE__ISOL_SEL_0 | vTAE__ISOL_JS_0))))).
fof(ax,axiom, vTAE__ISOL_AK_1 <=> vTAE__ISOL_JS_1).
fof(ax,axiom, vTAE__ISOL_SET_1 <=> (vTAE__ISOL_EXE_0 & vTAE__ISOL_AK_1)).
fof(ax,axiom, vTAE__XISOL_JS_1 <=> (~ vTAE__XISOL_CAN_0 & (~ vTAE__XISOL_JR_0 & (vTAE_ISOL_0 & (vTAE__XISOL_SEL_0 | vTAE__XISOL_JS_0))))).
fof(ax,axiom, vTAE__XISOL_AK_1 <=> vTAE__XISOL_JS_1).
fof(ax,axiom, vTAE__ISOL_RESET_1 <=> (vTAE__XISOL_EXE_0 & vTAE__XISOL_AK_1)).
fof(ax,axiom, vTAF__ISOL_JS_1 <=> (~ vTAF__ISOL_CAN_0 & (~ vTAF__ISOL_JR_0 & (~ vTAF_ISOL_0 & (vTAF__ISOL_SEL_0 | vTAF__ISOL_JS_0))))).
fof(ax,axiom, vTAF__ISOL_AK_1 <=> vTAF__ISOL_JS_1).
fof(ax,axiom, vTAF__ISOL_SET_1 <=> (vTAF__ISOL_EXE_0 & vTAF__ISOL_AK_1)).
fof(ax,axiom, vTAF__XISOL_JS_1 <=> (~ vTAF__XISOL_CAN_0 & (~ vTAF__XISOL_JR_0 & (vTAF_ISOL_0 & (vTAF__XISOL_SEL_0 | vTAF__XISOL_JS_0))))).
fof(ax,axiom, vTAF__XISOL_AK_1 <=> vTAF__XISOL_JS_1).
fof(ax,axiom, vTAF__ISOL_RESET_1 <=> (vTAF__XISOL_EXE_0 & vTAF__XISOL_AK_1)).
fof(ax,axiom, vTAG__ISOL_JS_1 <=> (~ vTAG__ISOL_CAN_0 & (~ vTAG__ISOL_JR_0 & (~ vTAG_ISOL_0 & (vTAG__ISOL_SEL_0 | vTAG__ISOL_JS_0))))).
fof(ax,axiom, vTAG__ISOL_AK_1 <=> vTAG__ISOL_JS_1).
fof(ax,axiom, vTAG__ISOL_SET_1 <=> (vTAG__ISOL_EXE_0 & vTAG__ISOL_AK_1)).
fof(ax,axiom, vTAG__XISOL_JS_1 <=> (~ vTAG__XISOL_CAN_0 & (~ vTAG__XISOL_JR_0 & (vTAG_ISOL_0 & (vTAG__XISOL_SEL_0 | vTAG__XISOL_JS_0))))).
fof(ax,axiom, vTAG__XISOL_AK_1 <=> vTAG__XISOL_JS_1).
fof(ax,axiom, vTAG__ISOL_RESET_1 <=> (vTAG__XISOL_EXE_0 & vTAG__XISOL_AK_1)).
fof(ax,axiom, vTBA__ISOL_JS_1 <=> (~ vTBA__ISOL_CAN_0 & (~ vTBA__ISOL_JR_0 & (~ vTBA_ISOL_0 & (vTBA__ISOL_SEL_0 | vTBA__ISOL_JS_0))))).
fof(ax,axiom, vTBA__ISOL_AK_1 <=> vTBA__ISOL_JS_1).
fof(ax,axiom, vTBA__ISOL_SET_1 <=> (vTBA__ISOL_EXE_0 & vTBA__ISOL_AK_1)).
fof(ax,axiom, vTBA__XISOL_JS_1 <=> (~ vTBA__XISOL_CAN_0 & (~ vTBA__XISOL_JR_0 & (vTBA_ISOL_0 & (vTBA__XISOL_SEL_0 | vTBA__XISOL_JS_0))))).
fof(ax,axiom, vTBA__XISOL_AK_1 <=> vTBA__XISOL_JS_1).
fof(ax,axiom, vTBA__ISOL_RESET_1 <=> (vTBA__XISOL_EXE_0 & vTBA__XISOL_AK_1)).
fof(ax,axiom, vTCA__ISOL_JS_1 <=> (~ vTCA__ISOL_CAN_0 & (~ vTCA__ISOL_JR_0 & (~ vTCA_ISOL_0 & (vTCA__ISOL_SEL_0 | vTCA__ISOL_JS_0))))).
fof(ax,axiom, vTCA__ISOL_AK_1 <=> vTCA__ISOL_JS_1).
fof(ax,axiom, vTCA__ISOL_SET_1 <=> (vTCA__ISOL_EXE_0 & vTCA__ISOL_AK_1)).
fof(ax,axiom, vTCA__XISOL_JS_1 <=> (~ vTCA__XISOL_CAN_0 & (~ vTCA__XISOL_JR_0 & (vTCA_ISOL_0 & (vTCA__XISOL_SEL_0 | vTCA__XISOL_JS_0))))).
fof(ax,axiom, vTCA__XISOL_AK_1 <=> vTCA__XISOL_JS_1).
fof(ax,axiom, vTCA__ISOL_RESET_1 <=> (vTCA__XISOL_EXE_0 & vTCA__XISOL_AK_1)).
fof(ax,axiom, vTDA__ISOL_JS_1 <=> (~ vTDA__ISOL_CAN_0 & (~ vTDA__ISOL_JR_0 & (~ vTDA_ISOL_0 & (vTDA__ISOL_SEL_0 | vTDA__ISOL_JS_0))))).
fof(ax,axiom, vTDA__ISOL_AK_1 <=> vTDA__ISOL_JS_1).
fof(ax,axiom, vTDA__ISOL_SET_1 <=> (vTDA__ISOL_EXE_0 & vTDA__ISOL_AK_1)).
fof(ax,axiom, vTDA__XISOL_JS_1 <=> (~ vTDA__XISOL_CAN_0 & (~ vTDA__XISOL_JR_0 & (vTDA_ISOL_0 & (vTDA__XISOL_SEL_0 | vTDA__XISOL_JS_0))))).
fof(ax,axiom, vTDA__XISOL_AK_1 <=> vTDA__XISOL_JS_1).
fof(ax,axiom, vTDA__ISOL_RESET_1 <=> (vTDA__XISOL_EXE_0 & vTDA__XISOL_AK_1)).
fof(ax,axiom, vTEA__ISOL_JS_1 <=> (~ vTEA__ISOL_CAN_0 & (~ vTEA__ISOL_JR_0 & (~ vTEA_ISOL_0 & (vTEA__ISOL_SEL_0 | vTEA__ISOL_JS_0))))).
fof(ax,axiom, vTEA__ISOL_AK_1 <=> vTEA__ISOL_JS_1).
fof(ax,axiom, vTEA__ISOL_SET_1 <=> (vTEA__ISOL_EXE_0 & vTEA__ISOL_AK_1)).
fof(ax,axiom, vTEA__XISOL_JS_1 <=> (~ vTEA__XISOL_CAN_0 & (~ vTEA__XISOL_JR_0 & (vTEA_ISOL_0 & (vTEA__XISOL_SEL_0 | vTEA__XISOL_JS_0))))).
fof(ax,axiom, vTEA__XISOL_AK_1 <=> vTEA__XISOL_JS_1).
fof(ax,axiom, vTEA__ISOL_RESET_1 <=> (vTEA__XISOL_EXE_0 & vTEA__XISOL_AK_1)).
fof(ax,axiom, vTFA__ISOL_JS_1 <=> (~ vTFA__ISOL_CAN_0 & (~ vTFA__ISOL_JR_0 & (~ vTFA_ISOL_0 & (vTFA__ISOL_SEL_0 | vTFA__ISOL_JS_0))))).
fof(ax,axiom, vTFA__ISOL_AK_1 <=> vTFA__ISOL_JS_1).
fof(ax,axiom, vTFA__ISOL_SET_1 <=> (vTFA__ISOL_EXE_0 & vTFA__ISOL_AK_1)).
fof(ax,axiom, vTFA__XISOL_JS_1 <=> (~ vTFA__XISOL_CAN_0 & (~ vTFA__XISOL_JR_0 & (vTFA_ISOL_0 & (vTFA__XISOL_SEL_0 | vTFA__XISOL_JS_0))))).
fof(ax,axiom, vTFA__XISOL_AK_1 <=> vTFA__XISOL_JS_1).
fof(ax,axiom, vTFA__ISOL_RESET_1 <=> (vTFA__XISOL_EXE_0 & vTFA__XISOL_AK_1)).
fof(ax,axiom, vTGA__ISOL_JS_1 <=> (~ vTGA__ISOL_CAN_0 & (~ vTGA__ISOL_JR_0 & (~ vTGA_ISOL_0 & (vTGA__ISOL_SEL_0 | vTGA__ISOL_JS_0))))).
fof(ax,axiom, vTGA__ISOL_AK_1 <=> vTGA__ISOL_JS_1).
fof(ax,axiom, vTGA__ISOL_SET_1 <=> (vTGA__ISOL_EXE_0 & vTGA__ISOL_AK_1)).
fof(ax,axiom, vTGA__XISOL_JS_1 <=> (~ vTGA__XISOL_CAN_0 & (~ vTGA__XISOL_JR_0 & (vTGA_ISOL_0 & (vTGA__XISOL_SEL_0 | vTGA__XISOL_JS_0))))).
fof(ax,axiom, vTGA__XISOL_AK_1 <=> vTGA__XISOL_JS_1).
fof(ax,axiom, vTGA__ISOL_RESET_1 <=> (vTGA__XISOL_EXE_0 & vTGA__XISOL_AK_1)).
fof(ax,axiom, vTHA__ISOL_JS_1 <=> (~ vTHA__ISOL_CAN_0 & (~ vTHA__ISOL_JR_0 & (~ vTHA_ISOL_0 & (vTHA__ISOL_SEL_0 | vTHA__ISOL_JS_0))))).
fof(ax,axiom, vTHA__ISOL_AK_1 <=> vTHA__ISOL_JS_1).
fof(ax,axiom, vTHA__ISOL_SET_1 <=> (vTHA__ISOL_EXE_0 & vTHA__ISOL_AK_1)).
fof(ax,axiom, vTHA__XISOL_JS_1 <=> (~ vTHA__XISOL_CAN_0 & (~ vTHA__XISOL_JR_0 & (vTHA_ISOL_0 & (vTHA__XISOL_SEL_0 | vTHA__XISOL_JS_0))))).
fof(ax,axiom, vTHA__XISOL_AK_1 <=> vTHA__XISOL_JS_1).
fof(ax,axiom, vTHA__ISOL_RESET_1 <=> (vTHA__XISOL_EXE_0 & vTHA__XISOL_AK_1)).
fof(ax,axiom, vTAA__LCI_JS_1 <=> (~ vTAA__LCI_CAN_0 & (~ vTAA__LCI_JR_0 & ((~ vTAA__RSET_INUSE_0 & (~ vTAA_CE_0 & (~ vTAA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAA_LCO_0 & (~ vTAA__LCI_OVERRIDE_0 & (vTAA__LCI_SEL_0 | vTAA__LCI_JS_0))))))) | (vTAA__RSET_FAILED_0 & (~ vTAA_CE_0 & (~ vTAA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAA_LCO_0 & (~ vTAA__LCI_OVERRIDE_0 & (vTAA__LCI_SEL_0 | vTAA__LCI_JS_0))))))))))).
fof(ax,axiom, vTAA__LCI_AK_1 <=> vTAA__LCI_JS_1).
fof(ax,axiom, vTAA__LCI_OVERRIDE_IL__1 <=> (~ vTAA__RSET_A_0 & (vTAA__LCI_EXE_0 & vTAA__LCI_AK_1))).
fof(ax,axiom, vTAA__LCI_OVERRIDE_1 <=> (~ vTAA__LCI_OVERRIDEJR_0 & (vTAA__LCI_OVERRIDE_IL__1 | vTAA__LCI_OVERRIDE_0))).
fof(ax,axiom, vTAA__LCI_OVERRIDEJS_1 <=> vTAA__LCI_OVERRIDE_1).
fof(ax,axiom, vTAB__LCI_JS_1 <=> (~ vTAB__LCI_CAN_0 & (~ vTAB__LCI_JR_0 & ((~ vTAB__RSET_INUSE_0 & (~ vTAB_CE_0 & (~ vTAB_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAB_LCO_0 & (~ vTAB__LCI_OVERRIDE_0 & (vTAB__LCI_SEL_0 | vTAB__LCI_JS_0))))))) | (vTAB__RSET_FAILED_0 & (~ vTAB_CE_0 & (~ vTAB_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAB_LCO_0 & (~ vTAB__LCI_OVERRIDE_0 & (vTAB__LCI_SEL_0 | vTAB__LCI_JS_0))))))))))).
fof(ax,axiom, vTAB__LCI_AK_1 <=> vTAB__LCI_JS_1).
fof(ax,axiom, vTAB__LCI_OVERRIDE_IL__1 <=> (~ vTAB__RSET_A_0 & (vTAB__LCI_EXE_0 & vTAB__LCI_AK_1))).
fof(ax,axiom, vTAB__LCI_OVERRIDE_1 <=> (~ vTAB__LCI_OVERRIDEJR_0 & (vTAB__LCI_OVERRIDE_IL__1 | vTAB__LCI_OVERRIDE_0))).
fof(ax,axiom, vTAB__LCI_OVERRIDEJS_1 <=> vTAB__LCI_OVERRIDE_1).
fof(ax,axiom, vTAC__LCI_JS_1 <=> (~ vTAC__LCI_CAN_0 & (~ vTAC__LCI_JR_0 & ((~ vTAC__RSET_INUSE_0 & (~ vTAC_CE_0 & (~ vTAC_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAC_LCO_0 & (~ vTAC__LCI_OVERRIDE_0 & (vTAC__LCI_SEL_0 | vTAC__LCI_JS_0))))))) | (vTAC__RSET_FAILED_0 & (~ vTAC_CE_0 & (~ vTAC_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAC_LCO_0 & (~ vTAC__LCI_OVERRIDE_0 & (vTAC__LCI_SEL_0 | vTAC__LCI_JS_0))))))))))).
fof(ax,axiom, vTAC__LCI_AK_1 <=> vTAC__LCI_JS_1).
fof(ax,axiom, vTAC__LCI_OVERRIDE_IL__1 <=> (~ vTAC__RSET_A_0 & (vTAC__LCI_EXE_0 & vTAC__LCI_AK_1))).
fof(ax,axiom, vTAC__LCI_OVERRIDE_1 <=> (~ vTAC__LCI_OVERRIDEJR_0 & (vTAC__LCI_OVERRIDE_IL__1 | vTAC__LCI_OVERRIDE_0))).
fof(ax,axiom, vTAC__LCI_OVERRIDEJS_1 <=> vTAC__LCI_OVERRIDE_1).
fof(ax,axiom, vTAD__LCI_JS_1 <=> (~ vTAD__LCI_CAN_0 & (~ vTAD__LCI_JR_0 & ((~ vTAD__RSET_INUSE_0 & (~ vTAD_CE_0 & (~ vTAD_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAD_LCO_0 & (~ vTAD__LCI_OVERRIDE_0 & (vTAD__LCI_SEL_0 | vTAD__LCI_JS_0))))))) | (vTAD__RSET_FAILED_0 & (~ vTAD_CE_0 & (~ vTAD_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAD_LCO_0 & (~ vTAD__LCI_OVERRIDE_0 & (vTAD__LCI_SEL_0 | vTAD__LCI_JS_0))))))))))).
fof(ax,axiom, vTAD__LCI_AK_1 <=> vTAD__LCI_JS_1).
fof(ax,axiom, vTAD__LCI_OVERRIDE_IL__1 <=> (~ vTAD__RSET_A_0 & (vTAD__LCI_EXE_0 & vTAD__LCI_AK_1))).
fof(ax,axiom, vTAD__LCI_OVERRIDE_1 <=> (~ vTAD__LCI_OVERRIDEJR_0 & (vTAD__LCI_OVERRIDE_IL__1 | vTAD__LCI_OVERRIDE_0))).
fof(ax,axiom, vTAD__LCI_OVERRIDEJS_1 <=> vTAD__LCI_OVERRIDE_1).
fof(ax,axiom, vTAE__LCI_JS_1 <=> (~ vTAE__LCI_CAN_0 & (~ vTAE__LCI_JR_0 & ((~ vTAE__RSET_INUSE_0 & (~ vTAE_CE_0 & (~ vTAE_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAE_LCO_0 & (~ vTAE__LCI_OVERRIDE_0 & (vTAE__LCI_SEL_0 | vTAE__LCI_JS_0))))))) | (vTAE__RSET_FAILED_0 & (~ vTAE_CE_0 & (~ vTAE_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAE_LCO_0 & (~ vTAE__LCI_OVERRIDE_0 & (vTAE__LCI_SEL_0 | vTAE__LCI_JS_0))))))))))).
fof(ax,axiom, vTAE__LCI_AK_1 <=> vTAE__LCI_JS_1).
fof(ax,axiom, vTAE__LCI_OVERRIDE_IL__1 <=> (~ vTAE__RSET_A_0 & (vTAE__LCI_EXE_0 & vTAE__LCI_AK_1))).
fof(ax,axiom, vTAE__LCI_OVERRIDE_1 <=> (~ vTAE__LCI_OVERRIDEJR_0 & (vTAE__LCI_OVERRIDE_IL__1 | vTAE__LCI_OVERRIDE_0))).
fof(ax,axiom, vTAE__LCI_OVERRIDEJS_1 <=> vTAE__LCI_OVERRIDE_1).
fof(ax,axiom, vTAF__LCI_JS_1 <=> (~ vTAF__LCI_CAN_0 & (~ vTAF__LCI_JR_0 & ((~ vTAF__RSET_INUSE_0 & (~ vTAF_CE_0 & (~ vTAF_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAF_LCO_0 & (~ vTAF__LCI_OVERRIDE_0 & (vTAF__LCI_SEL_0 | vTAF__LCI_JS_0))))))) | (vTAF__RSET_FAILED_0 & (~ vTAF_CE_0 & (~ vTAF_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAF_LCO_0 & (~ vTAF__LCI_OVERRIDE_0 & (vTAF__LCI_SEL_0 | vTAF__LCI_JS_0))))))))))).
fof(ax,axiom, vTAF__LCI_AK_1 <=> vTAF__LCI_JS_1).
fof(ax,axiom, vTAF__LCI_OVERRIDE_IL__1 <=> (~ vTAF__RSET_A_0 & (vTAF__LCI_EXE_0 & vTAF__LCI_AK_1))).
fof(ax,axiom, vTAF__LCI_OVERRIDE_1 <=> (~ vTAF__LCI_OVERRIDEJR_0 & (vTAF__LCI_OVERRIDE_IL__1 | vTAF__LCI_OVERRIDE_0))).
fof(ax,axiom, vTAF__LCI_OVERRIDEJS_1 <=> vTAF__LCI_OVERRIDE_1).
fof(ax,axiom, vTAG__LCI_JS_1 <=> (~ vTAG__LCI_CAN_0 & (~ vTAG__LCI_JR_0 & ((~ vTAG__RSET_INUSE_0 & (~ vTAG_CE_0 & (~ vTAG_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAG_LCO_0 & (~ vTAG__LCI_OVERRIDE_0 & (vTAG__LCI_SEL_0 | vTAG__LCI_JS_0))))))) | (vTAG__RSET_FAILED_0 & (~ vTAG_CE_0 & (~ vTAG_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTAG_LCO_0 & (~ vTAG__LCI_OVERRIDE_0 & (vTAG__LCI_SEL_0 | vTAG__LCI_JS_0))))))))))).
fof(ax,axiom, vTAG__LCI_AK_1 <=> vTAG__LCI_JS_1).
fof(ax,axiom, vTAG__LCI_OVERRIDE_IL__1 <=> (~ vTAG__RSET_A_0 & (vTAG__LCI_EXE_0 & vTAG__LCI_AK_1))).
fof(ax,axiom, vTAG__LCI_OVERRIDE_1 <=> (~ vTAG__LCI_OVERRIDEJR_0 & (vTAG__LCI_OVERRIDE_IL__1 | vTAG__LCI_OVERRIDE_0))).
fof(ax,axiom, vTAG__LCI_OVERRIDEJS_1 <=> vTAG__LCI_OVERRIDE_1).
fof(ax,axiom, vTBA__LCI_JS_1 <=> (~ vTBA__LCI_CAN_0 & (~ vTBA__LCI_JR_0 & ((~ vTBA__RSET_INUSE_0 & (~ vTBA_CE_0 & (~ vTBA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTBA_LCO_0 & (~ vTBA__LCI_OVERRIDE_0 & (vTBA__LCI_SEL_0 | vTBA__LCI_JS_0))))))) | (vTBA__RSET_FAILED_0 & (~ vTBA_CE_0 & (~ vTBA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTBA_LCO_0 & (~ vTBA__LCI_OVERRIDE_0 & (vTBA__LCI_SEL_0 | vTBA__LCI_JS_0))))))))))).
fof(ax,axiom, vTBA__LCI_AK_1 <=> vTBA__LCI_JS_1).
fof(ax,axiom, vTBA__LCI_OVERRIDE_IL__1 <=> (~ vTBA__RSET_A_0 & (vTBA__LCI_EXE_0 & vTBA__LCI_AK_1))).
fof(ax,axiom, vTBA__LCI_OVERRIDE_1 <=> (~ vTBA__LCI_OVERRIDEJR_0 & (vTBA__LCI_OVERRIDE_IL__1 | vTBA__LCI_OVERRIDE_0))).
fof(ax,axiom, vTBA__LCI_OVERRIDEJS_1 <=> vTBA__LCI_OVERRIDE_1).
fof(ax,axiom, vTCA__LCI_JS_1 <=> (~ vTCA__LCI_CAN_0 & (~ vTCA__LCI_JR_0 & ((~ vTCA__RSET_INUSE_0 & (~ vTCA_CE_0 & (~ vTCA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTCA_LCO_0 & (~ vTCA__LCI_OVERRIDE_0 & (vTCA__LCI_SEL_0 | vTCA__LCI_JS_0))))))) | (vTCA__RSET_FAILED_0 & (~ vTCA_CE_0 & (~ vTCA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTCA_LCO_0 & (~ vTCA__LCI_OVERRIDE_0 & (vTCA__LCI_SEL_0 | vTCA__LCI_JS_0))))))))))).
fof(ax,axiom, vTCA__LCI_AK_1 <=> vTCA__LCI_JS_1).
fof(ax,axiom, vTCA__LCI_OVERRIDE_IL__1 <=> (~ vTCA__RSET_A_0 & (vTCA__LCI_EXE_0 & vTCA__LCI_AK_1))).
fof(ax,axiom, vTCA__LCI_OVERRIDE_1 <=> (~ vTCA__LCI_OVERRIDEJR_0 & (vTCA__LCI_OVERRIDE_IL__1 | vTCA__LCI_OVERRIDE_0))).
fof(ax,axiom, vTCA__LCI_OVERRIDEJS_1 <=> vTCA__LCI_OVERRIDE_1).
fof(ax,axiom, vTDA__LCI_JS_1 <=> (~ vTDA__LCI_CAN_0 & (~ vTDA__LCI_JR_0 & ((~ vTDA__RSET_INUSE_0 & (~ vTDA_CE_0 & (~ vTDA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTDA_LCO_0 & (~ vTDA__LCI_OVERRIDE_0 & (vTDA__LCI_SEL_0 | vTDA__LCI_JS_0))))))) | (vTDA__RSET_FAILED_0 & (~ vTDA_CE_0 & (~ vTDA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTDA_LCO_0 & (~ vTDA__LCI_OVERRIDE_0 & (vTDA__LCI_SEL_0 | vTDA__LCI_JS_0))))))))))).
fof(ax,axiom, vTDA__LCI_AK_1 <=> vTDA__LCI_JS_1).
fof(ax,axiom, vTDA__LCI_OVERRIDE_IL__1 <=> (~ vTDA__RSET_A_0 & (vTDA__LCI_EXE_0 & vTDA__LCI_AK_1))).
fof(ax,axiom, vTDA__LCI_OVERRIDE_1 <=> (~ vTDA__LCI_OVERRIDEJR_0 & (vTDA__LCI_OVERRIDE_IL__1 | vTDA__LCI_OVERRIDE_0))).
fof(ax,axiom, vTDA__LCI_OVERRIDEJS_1 <=> vTDA__LCI_OVERRIDE_1).
fof(ax,axiom, vTEA__LCI_JS_1 <=> (~ vTEA__LCI_CAN_0 & (~ vTEA__LCI_JR_0 & ((~ vTEA__RSET_INUSE_0 & (~ vTEA_CE_0 & (~ vTEA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTEA_LCO_0 & (~ vTEA__LCI_OVERRIDE_0 & (vTEA__LCI_SEL_0 | vTEA__LCI_JS_0))))))) | (vTEA__RSET_FAILED_0 & (~ vTEA_CE_0 & (~ vTEA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTEA_LCO_0 & (~ vTEA__LCI_OVERRIDE_0 & (vTEA__LCI_SEL_0 | vTEA__LCI_JS_0))))))))))).
fof(ax,axiom, vTEA__LCI_AK_1 <=> vTEA__LCI_JS_1).
fof(ax,axiom, vTEA__LCI_OVERRIDE_IL__1 <=> (~ vTEA__RSET_A_0 & (vTEA__LCI_EXE_0 & vTEA__LCI_AK_1))).
fof(ax,axiom, vTEA__LCI_OVERRIDE_1 <=> (~ vTEA__LCI_OVERRIDEJR_0 & (vTEA__LCI_OVERRIDE_IL__1 | vTEA__LCI_OVERRIDE_0))).
fof(ax,axiom, vTEA__LCI_OVERRIDEJS_1 <=> vTEA__LCI_OVERRIDE_1).
fof(ax,axiom, vTFA__LCI_JS_1 <=> (~ vTFA__LCI_CAN_0 & (~ vTFA__LCI_JR_0 & ((~ vTFA__RSET_INUSE_0 & (~ vTFA_CE_0 & (~ vTFA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTFA_LCO_0 & (~ vTFA__LCI_OVERRIDE_0 & (vTFA__LCI_SEL_0 | vTFA__LCI_JS_0))))))) | (vTFA__RSET_FAILED_0 & (~ vTFA_CE_0 & (~ vTFA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTFA_LCO_0 & (~ vTFA__LCI_OVERRIDE_0 & (vTFA__LCI_SEL_0 | vTFA__LCI_JS_0))))))))))).
fof(ax,axiom, vTFA__LCI_AK_1 <=> vTFA__LCI_JS_1).
fof(ax,axiom, vTFA__LCI_OVERRIDE_IL__1 <=> (~ vTFA__RSET_A_0 & (vTFA__LCI_EXE_0 & vTFA__LCI_AK_1))).
fof(ax,axiom, vTFA__LCI_OVERRIDE_1 <=> (~ vTFA__LCI_OVERRIDEJR_0 & (vTFA__LCI_OVERRIDE_IL__1 | vTFA__LCI_OVERRIDE_0))).
fof(ax,axiom, vTFA__LCI_OVERRIDEJS_1 <=> vTFA__LCI_OVERRIDE_1).
fof(ax,axiom, vTGA__LCI_JS_1 <=> (~ vTGA__LCI_CAN_0 & (~ vTGA__LCI_JR_0 & ((~ vTGA__RSET_INUSE_0 & (~ vTGA_CE_0 & (~ vTGA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTGA_LCO_0 & (~ vTGA__LCI_OVERRIDE_0 & (vTGA__LCI_SEL_0 | vTGA__LCI_JS_0))))))) | (vTGA__RSET_FAILED_0 & (~ vTGA_CE_0 & (~ vTGA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTGA_LCO_0 & (~ vTGA__LCI_OVERRIDE_0 & (vTGA__LCI_SEL_0 | vTGA__LCI_JS_0))))))))))).
fof(ax,axiom, vTGA__LCI_AK_1 <=> vTGA__LCI_JS_1).
fof(ax,axiom, vTGA__LCI_OVERRIDE_IL__1 <=> (~ vTGA__RSET_A_0 & (vTGA__LCI_EXE_0 & vTGA__LCI_AK_1))).
fof(ax,axiom, vTGA__LCI_OVERRIDE_1 <=> (~ vTGA__LCI_OVERRIDEJR_0 & (vTGA__LCI_OVERRIDE_IL__1 | vTGA__LCI_OVERRIDE_0))).
fof(ax,axiom, vTGA__LCI_OVERRIDEJS_1 <=> vTGA__LCI_OVERRIDE_1).
fof(ax,axiom, vTHA__LCI_JS_1 <=> (~ vTHA__LCI_CAN_0 & (~ vTHA__LCI_JR_0 & ((~ vTHA__RSET_INUSE_0 & (~ vTHA_CE_0 & (~ vTHA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTHA_LCO_0 & (~ vTHA__LCI_OVERRIDE_0 & (vTHA__LCI_SEL_0 | vTHA__LCI_JS_0))))))) | (vTHA__RSET_FAILED_0 & (~ vTHA_CE_0 & (~ vTHA_CLR_0 & (~ vIL822__LCI_OVERRIDE_0 & (~ vTHA_LCO_0 & (~ vTHA__LCI_OVERRIDE_0 & (vTHA__LCI_SEL_0 | vTHA__LCI_JS_0))))))))))).
fof(ax,axiom, vTHA__LCI_AK_1 <=> vTHA__LCI_JS_1).
fof(ax,axiom, vTHA__LCI_OVERRIDE_IL__1 <=> (~ vTHA__RSET_A_0 & (vTHA__LCI_EXE_0 & vTHA__LCI_AK_1))).
fof(ax,axiom, vTHA__LCI_OVERRIDE_1 <=> (~ vTHA__LCI_OVERRIDEJR_0 & (vTHA__LCI_OVERRIDE_IL__1 | vTHA__LCI_OVERRIDE_0))).
fof(ax,axiom, vTHA__LCI_OVERRIDEJS_1 <=> vTHA__LCI_OVERRIDE_1).
fof(ax,axiom, vLOS2_JS_1 <=> ~ vLOS2_0).
fof(ax,axiom, vTAA__OCCEXT_JS_1 <=> (~ vTAA_OCC_0 & vTAA_CLR_0)).
fof(ax,axiom, vTAB__OCCEXT_JS_1 <=> (~ vTAB_OCC_0 & vTAB_CLR_0)).
fof(ax,axiom, vTAC__OCCEXT_JS_1 <=> (~ vTAC_OCC_0 & vTAC_CLR_0)).
fof(ax,axiom, vTAD__OCCEXT_JS_1 <=> (~ vTAD_OCC_0 & vTAD_CLR_0)).
fof(ax,axiom, vTAE__OCCEXT_JS_1 <=> (~ vTAE_OCC_0 & vTAE_CLR_0)).
fof(ax,axiom, vTAF__OCCEXT_JS_1 <=> (~ vTAF_OCC_0 & vTAF_CLR_0)).
fof(ax,axiom, vTAG__OCCEXT_JS_1 <=> (~ vTAG_OCC_0 & vTAG_CLR_0)).
fof(ax,axiom, vTBA__OCCEXT_JS_1 <=> (~ vTBA_OCC_0 & vTBA_CLR_0)).
fof(ax,axiom, vTCA__OCCEXT_JS_1 <=> (~ vTCA_OCC_0 & vTCA_CLR_0)).
fof(ax,axiom, vTDA__OCCEXT_JS_1 <=> (~ vTDA_OCC_0 & vTDA_CLR_0)).
fof(ax,axiom, vTEA__OCCEXT_JS_1 <=> (~ vTEA_OCC_0 & vTEA_CLR_0)).
fof(ax,axiom, vTFA__OCCEXT_JS_1 <=> (~ vTFA_OCC_0 & vTFA_CLR_0)).
fof(ax,axiom, vTGA__OCCEXT_JS_1 <=> (~ vTGA_OCC_0 & vTGA_CLR_0)).
fof(ax,axiom, vTHA__OCCEXT_JS_1 <=> (~ vTHA_OCC_0 & vTHA_CLR_0)).
fof(ax,axiom, vTAA_CLR_IL__1 <=> (~ vTAA_ISOL_0 & (~ vTAA_OCC_TF__0 & (vTAA__OCCEXT_JR_0 & vTAA__OCCEXT_JS_1)))).
fof(ax,axiom, vTAA_OCC_IL__1 <=> (~ vTAA_ISOL_0 & (((vTAA_OCC_0 & ~ vTAA_CLR_0) | vTAA_OCC_TF__0) | (vTAA_OCC_IL__0 & (~ vTAA__OCCEXT_JR_0 & vTAA__OCCEXT_JS_1))))).
fof(ax,axiom, vTAB_CLR_IL__1 <=> (~ vTAB_ISOL_0 & (~ vTAB_OCC_TF__0 & (vTAB__OCCEXT_JR_0 & vTAB__OCCEXT_JS_1)))).
fof(ax,axiom, vTAB_OCC_IL__1 <=> (~ vTAB_ISOL_0 & (((vTAB_OCC_0 & ~ vTAB_CLR_0) | vTAB_OCC_TF__0) | (vTAB_OCC_IL__0 & (~ vTAB__OCCEXT_JR_0 & vTAB__OCCEXT_JS_1))))).
fof(ax,axiom, vTAC_CLR_IL__1 <=> (~ vTAC_ISOL_0 & (~ vTAC_OCC_TF__0 & (vTAC__OCCEXT_JR_0 & vTAC__OCCEXT_JS_1)))).
fof(ax,axiom, vTAC_OCC_IL__1 <=> (~ vTAC_ISOL_0 & (((vTAC_OCC_0 & ~ vTAC_CLR_0) | vTAC_OCC_TF__0) | (vTAC_OCC_IL__0 & (~ vTAC__OCCEXT_JR_0 & vTAC__OCCEXT_JS_1))))).
fof(ax,axiom, vTAD_CLR_IL__1 <=> (~ vTAD_ISOL_0 & (~ vTAD_OCC_TF__0 & (vTAD__OCCEXT_JR_0 & vTAD__OCCEXT_JS_1)))).
fof(ax,axiom, vTAD_OCC_IL__1 <=> (~ vTAD_ISOL_0 & (((vTAD_OCC_0 & ~ vTAD_CLR_0) | vTAD_OCC_TF__0) | (vTAD_OCC_IL__0 & (~ vTAD__OCCEXT_JR_0 & vTAD__OCCEXT_JS_1))))).
fof(ax,axiom, vTAE_CLR_IL__1 <=> (~ vTAE_ISOL_0 & (~ vTAE_OCC_TF__0 & (vTAE__OCCEXT_JR_0 & vTAE__OCCEXT_JS_1)))).
fof(ax,axiom, vTAE_OCC_IL__1 <=> (~ vTAE_ISOL_0 & (((vTAE_OCC_0 & ~ vTAE_CLR_0) | vTAE_OCC_TF__0) | (vTAE_OCC_IL__0 & (~ vTAE__OCCEXT_JR_0 & vTAE__OCCEXT_JS_1))))).
fof(ax,axiom, vTAF_CLR_IL__1 <=> (~ vTAF_ISOL_0 & (~ vTAF_OCC_TF__0 & (vTAF__OCCEXT_JR_0 & vTAF__OCCEXT_JS_1)))).
fof(ax,axiom, vTAF_OCC_IL__1 <=> (~ vTAF_ISOL_0 & (((vTAF_OCC_0 & ~ vTAF_CLR_0) | vTAF_OCC_TF__0) | (vTAF_OCC_IL__0 & (~ vTAF__OCCEXT_JR_0 & vTAF__OCCEXT_JS_1))))).
fof(ax,axiom, vTAG_CLR_IL__1 <=> (~ vTAG_ISOL_0 & (~ vTAG_OCC_TF__0 & (vTAG__OCCEXT_JR_0 & vTAG__OCCEXT_JS_1)))).
fof(ax,axiom, vTAG_OCC_IL__1 <=> (~ vTAG_ISOL_0 & (((vTAG_OCC_0 & ~ vTAG_CLR_0) | vTAG_OCC_TF__0) | (vTAG_OCC_IL__0 & (~ vTAG__OCCEXT_JR_0 & vTAG__OCCEXT_JS_1))))).
fof(ax,axiom, vTBA_CLR_IL__1 <=> (~ vTBA_ISOL_0 & (~ vTBA_OCC_TF__0 & (vTBA__OCCEXT_JR_0 & vTBA__OCCEXT_JS_1)))).
fof(ax,axiom, vTBA_OCC_IL__1 <=> (~ vTBA_ISOL_0 & (((vTBA_OCC_0 & ~ vTBA_CLR_0) | vTBA_OCC_TF__0) | (vTBA_OCC_IL__0 & (~ vTBA__OCCEXT_JR_0 & vTBA__OCCEXT_JS_1))))).
fof(ax,axiom, vTCA_CLR_IL__1 <=> (~ vTCA_ISOL_0 & (~ vTCA_OCC_TF__0 & (vTCA__OCCEXT_JR_0 & vTCA__OCCEXT_JS_1)))).
fof(ax,axiom, vTCA_OCC_IL__1 <=> (~ vTCA_ISOL_0 & (((vTCA_OCC_0 & ~ vTCA_CLR_0) | vTCA_OCC_TF__0) | (vTCA_OCC_IL__0 & (~ vTCA__OCCEXT_JR_0 & vTCA__OCCEXT_JS_1))))).
fof(ax,axiom, vTDA_CLR_IL__1 <=> (~ vTDA_ISOL_0 & (~ vTDA_OCC_TF__0 & (vTDA__OCCEXT_JR_0 & vTDA__OCCEXT_JS_1)))).
fof(ax,axiom, vTDA_OCC_IL__1 <=> (~ vTDA_ISOL_0 & (((vTDA_OCC_0 & ~ vTDA_CLR_0) | vTDA_OCC_TF__0) | (vTDA_OCC_IL__0 & (~ vTDA__OCCEXT_JR_0 & vTDA__OCCEXT_JS_1))))).
fof(ax,axiom, vTEA_CLR_IL__1 <=> (~ vTEA_ISOL_0 & (~ vTEA_OCC_TF__0 & (vTEA__OCCEXT_JR_0 & vTEA__OCCEXT_JS_1)))).
fof(ax,axiom, vTEA_OCC_IL__1 <=> (~ vTEA_ISOL_0 & (((vTEA_OCC_0 & ~ vTEA_CLR_0) | vTEA_OCC_TF__0) | (vTEA_OCC_IL__0 & (~ vTEA__OCCEXT_JR_0 & vTEA__OCCEXT_JS_1))))).
fof(ax,axiom, vTFA_CLR_IL__1 <=> (~ vTFA_ISOL_0 & (~ vTFA_OCC_TF__0 & (vTFA__OCCEXT_JR_0 & vTFA__OCCEXT_JS_1)))).
fof(ax,axiom, vTFA_OCC_IL__1 <=> (~ vTFA_ISOL_0 & (((vTFA_OCC_0 & ~ vTFA_CLR_0) | vTFA_OCC_TF__0) | (vTFA_OCC_IL__0 & (~ vTFA__OCCEXT_JR_0 & vTFA__OCCEXT_JS_1))))).
fof(ax,axiom, vTGA_CLR_IL__1 <=> (~ vTGA_ISOL_0 & (~ vTGA_OCC_TF__0 & (vTGA__OCCEXT_JR_0 & vTGA__OCCEXT_JS_1)))).
fof(ax,axiom, vTGA_OCC_IL__1 <=> (~ vTGA_ISOL_0 & (((vTGA_OCC_0 & ~ vTGA_CLR_0) | vTGA_OCC_TF__0) | (vTGA_OCC_IL__0 & (~ vTGA__OCCEXT_JR_0 & vTGA__OCCEXT_JS_1))))).
fof(ax,axiom, vTHA_CLR_IL__1 <=> (~ vTHA_ISOL_0 & (~ vTHA_OCC_TF__0 & (vTHA__OCCEXT_JR_0 & vTHA__OCCEXT_JS_1)))).
fof(ax,axiom, vTHA_OCC_IL__1 <=> (~ vTHA_ISOL_0 & (((vTHA_OCC_0 & ~ vTHA_CLR_0) | vTHA_OCC_TF__0) | (vTHA_OCC_IL__0 & (~ vTHA__OCCEXT_JR_0 & vTHA__OCCEXT_JS_1))))).
fof(ax,axiom, vS400__STAPP_JS_1 <=> (vTAD_CLR_IL__1 | vP1608_RL_0)).
fof(ax,axiom, vS410__STAPP_JS_1 <=> (vTAD_CLR_IL__1 | vP1608_NL_0)).
fof(ax,axiom, vS400__TAPP_JS_1 <=> vTBA_OCC_IL__1).
fof(ax,axiom, vS410__TAPP_JS_1 <=> vTCA_OCC_IL__1).
fof(ax,axiom, vS450__STAPP_JS_1 <=> (vTAE_CLR_IL__1 | vP1622_NL_0)).
fof(ax,axiom, vS450__TAPP_JS_1 <=> vTFA_OCC_IL__1).
fof(ax,axiom, vS470__STAPP_JS_1 <=> (vTAE_CLR_IL__1 | vP1624_RL_0)).
fof(ax,axiom, vS460__STAPP_JS_1 <=> (vTAE_CLR_IL__1 | vP1624_NL_0)).
fof(ax,axiom, vS460__TAPP_JS_1 <=> vTGA_OCC_IL__1).
fof(ax,axiom, vS470__TAPP_JS_1 <=> vTHA_OCC_IL__1).
fof(ax,axiom, vP1602_WZ_1 <=> (vIL822_ENABLED_0 & (vTAD_CLR_IL__1 & vP1602_C_0))).
fof(ax,axiom, vP1604_WZ_1 <=> (vIL822_ENABLED_0 & (vTAD_CLR_IL__1 & vP1604_C_0))).
fof(ax,axiom, vP1606_WZ_1 <=> (vIL822_ENABLED_0 & (vTAD_CLR_IL__1 & vP1606_C_0))).
fof(ax,axiom, vP1608_WZ_1 <=> (vIL822_ENABLED_0 & (vTAD_CLR_IL__1 & vP1608_C_0))).
fof(ax,axiom, vP1620_WZ_1 <=> (vIL822_ENABLED_0 & (vTAE_CLR_IL__1 & vP1620_C_0))).
fof(ax,axiom, vP1622_WZ_1 <=> (vIL822_ENABLED_0 & (vTAE_CLR_IL__1 & vP1622_C_0))).
fof(ax,axiom, vP1624_WZ_1 <=> (vIL822_ENABLED_0 & (vTAE_CLR_IL__1 & vP1624_C_0))).
fof(ax,axiom, vP1602_NWZ_1 <=> ((~ vP1602__RW_INHIBIT_0 & (vP1602R_UL_0 & (~ vP1602R__CALL_P_0 & vP1602_WZ_1))) | vP1602_NL_0)).
fof(ax,axiom, vP1602_RWZ_1 <=> ((~ vP1602__NW_INHIBIT_0 & (vP1602N_UL_0 & (~ vP1602N__CALL_P_0 & vP1602_WZ_1))) | vP1602_RL_0)).
fof(ax,axiom, vP1602_KN_1 <=> ((~ vP1602_QC_0 & ((vP1602_APZ_0 & (~ vP1602_RD_0 & vP1602_QN_0)) | vP1602_KN_0)) | (vP1602_RD_0 & (vP1602_KN_0 | (vP1602_APZ_0 & (~ vP1602_RD_0 & vP1602_QN_0)))))).
fof(ax,axiom, vP1602_KR_1 <=> ((~ vP1602_QC_0 & ((vP1602_APZ_0 & (~ vP1602_RD_0 & vP1602_QR_0)) | vP1602_KR_0)) | (vP1602_RD_0 & (vP1602_KR_0 | (vP1602_APZ_0 & (~ vP1602_RD_0 & vP1602_QR_0)))))).
fof(ax,axiom, vP1602_N_1 <=> (~ vP1602_R_0 & (vP1602_KN_1 & ((vP1602_APZ_0 & (vP1602_NWZ_1 & vP1602_C_0)) | ((vP1602_NL_0 & (vP1602_NWZ_1 & vP1602_C_0)) | vP1602_N_0))))).
fof(ax,axiom, vP1602_R_1 <=> (~ vP1602_N_1 & (vP1602_KR_1 & ((vP1602_APZ_0 & (vP1602_RWZ_1 & vP1602_C_0)) | ((vP1602_RL_0 & (vP1602_RWZ_1 & vP1602_C_0)) | vP1602_R_0))))).
fof(ax,axiom, vP1602_C_1 <=> (~ vP1602_R_1 & (~ vP1602_N_1 & (vP1602_QC_0 | (~ vAPPDEL1_0 | vP1602_C_0))))).
fof(ax,axiom, vP1602_APZ_1 <=> (~ vP1602_QR_0 & (~ vP1602_QN_0 & (~ vP1602_KR_1 & ~ vP1602_KN_1)))).
fof(ax,axiom, vP1602_NLZ_1 <=> (vP1602_NWZ_1 & ~ vP1602_R_1)).
fof(ax,axiom, vP1602_RLZ_1 <=> (vP1602_RWZ_1 & ~ vP1602_N_1)).
fof(ax,axiom, vP1604_NWZ_1 <=> ((~ vP1604__RW_INHIBIT_0 & (vP1604R_UL_0 & (~ vP1604R__CALL_P_0 & vP1604_WZ_1))) | vP1604_NL_0)).
fof(ax,axiom, vP1604_RWZ_1 <=> ((~ vP1604__NW_INHIBIT_0 & (vP1604N_UL_0 & (~ vP1604N__CALL_P_0 & vP1604_WZ_1))) | vP1604_RL_0)).
fof(ax,axiom, vP1604_KN_1 <=> ((~ vP1604_QC_0 & ((vP1604_APZ_0 & (~ vP1604_RD_0 & vP1604_QN_0)) | vP1604_KN_0)) | (vP1604_RD_0 & (vP1604_KN_0 | (vP1604_APZ_0 & (~ vP1604_RD_0 & vP1604_QN_0)))))).
fof(ax,axiom, vP1604_KR_1 <=> ((~ vP1604_QC_0 & ((vP1604_APZ_0 & (~ vP1604_RD_0 & vP1604_QR_0)) | vP1604_KR_0)) | (vP1604_RD_0 & (vP1604_KR_0 | (vP1604_APZ_0 & (~ vP1604_RD_0 & vP1604_QR_0)))))).
fof(ax,axiom, vP1604_N_1 <=> (~ vP1604_R_0 & (vP1604_KN_1 & ((vP1604_APZ_0 & (vP1604_NWZ_1 & vP1604_C_0)) | ((vP1604_NL_0 & (vP1604_NWZ_1 & vP1604_C_0)) | vP1604_N_0))))).
fof(ax,axiom, vP1604_R_1 <=> (~ vP1604_N_1 & (vP1604_KR_1 & ((vP1604_APZ_0 & (vP1604_RWZ_1 & vP1604_C_0)) | ((vP1604_RL_0 & (vP1604_RWZ_1 & vP1604_C_0)) | vP1604_R_0))))).
fof(ax,axiom, vP1604_C_1 <=> (~ vP1604_R_1 & (~ vP1604_N_1 & (vP1604_QC_0 | (~ vAPPDEL1_0 | vP1604_C_0))))).
fof(ax,axiom, vP1604_APZ_1 <=> (~ vP1604_QR_0 & (~ vP1604_QN_0 & (~ vP1604_KR_1 & ~ vP1604_KN_1)))).
fof(ax,axiom, vP1604_NLZ_1 <=> (vP1604_NWZ_1 & ~ vP1604_R_1)).
fof(ax,axiom, vP1604_RLZ_1 <=> (vP1604_RWZ_1 & ~ vP1604_N_1)).
fof(ax,axiom, vP1606_NWZ_1 <=> ((~ vP1606__RW_INHIBIT_0 & (vP1606R_UL_0 & (~ vP1606R__CALL_P_0 & vP1606_WZ_1))) | vP1606_NL_0)).
fof(ax,axiom, vP1606_RWZ_1 <=> ((~ vP1606__NW_INHIBIT_0 & (vP1606N_UL_0 & (~ vP1606N__CALL_P_0 & vP1606_WZ_1))) | vP1606_RL_0)).
fof(ax,axiom, vP1606_KN_1 <=> ((~ vP1606_QC_0 & ((vP1606_APZ_0 & (~ vP1606_RD_0 & vP1606_QN_0)) | vP1606_KN_0)) | (vP1606_RD_0 & (vP1606_KN_0 | (vP1606_APZ_0 & (~ vP1606_RD_0 & vP1606_QN_0)))))).
fof(ax,axiom, vP1606_KR_1 <=> ((~ vP1606_QC_0 & ((vP1606_APZ_0 & (~ vP1606_RD_0 & vP1606_QR_0)) | vP1606_KR_0)) | (vP1606_RD_0 & (vP1606_KR_0 | (vP1606_APZ_0 & (~ vP1606_RD_0 & vP1606_QR_0)))))).
fof(ax,axiom, vP1606_N_1 <=> (~ vP1606_R_0 & (vP1606_KN_1 & ((vP1606_APZ_0 & (vP1606_NWZ_1 & vP1606_C_0)) | ((vP1606_NL_0 & (vP1606_NWZ_1 & vP1606_C_0)) | vP1606_N_0))))).
fof(ax,axiom, vP1606_R_1 <=> (~ vP1606_N_1 & (vP1606_KR_1 & ((vP1606_APZ_0 & (vP1606_RWZ_1 & vP1606_C_0)) | ((vP1606_RL_0 & (vP1606_RWZ_1 & vP1606_C_0)) | vP1606_R_0))))).
fof(ax,axiom, vP1606_C_1 <=> (~ vP1606_R_1 & (~ vP1606_N_1 & (vP1606_QC_0 | (~ vAPPDEL1_0 | vP1606_C_0))))).
fof(ax,axiom, vP1606_APZ_1 <=> (~ vP1606_QR_0 & (~ vP1606_QN_0 & (~ vP1606_KR_1 & ~ vP1606_KN_1)))).
fof(ax,axiom, vP1606_NLZ_1 <=> (vP1606_NWZ_1 & ~ vP1606_R_1)).
fof(ax,axiom, vP1606_RLZ_1 <=> (vP1606_RWZ_1 & ~ vP1606_N_1)).
fof(ax,axiom, vP1608_NWZ_1 <=> ((~ vP1608__RW_INHIBIT_0 & (vP1608R_UL_0 & (~ vP1608R__CALL_P_0 & vP1608_WZ_1))) | vP1608_NL_0)).
fof(ax,axiom, vP1608_RWZ_1 <=> ((~ vP1608__NW_INHIBIT_0 & (vP1608N_UL_0 & (~ vP1608N__CALL_P_0 & vP1608_WZ_1))) | vP1608_RL_0)).
fof(ax,axiom, vP1608_KN_1 <=> ((~ vP1608_QC_0 & ((vP1608_APZ_0 & (~ vP1608_RD_0 & vP1608_QN_0)) | vP1608_KN_0)) | (vP1608_RD_0 & (vP1608_KN_0 | (vP1608_APZ_0 & (~ vP1608_RD_0 & vP1608_QN_0)))))).
fof(ax,axiom, vP1608_KR_1 <=> ((~ vP1608_QC_0 & ((vP1608_APZ_0 & (~ vP1608_RD_0 & vP1608_QR_0)) | vP1608_KR_0)) | (vP1608_RD_0 & (vP1608_KR_0 | (vP1608_APZ_0 & (~ vP1608_RD_0 & vP1608_QR_0)))))).
fof(ax,axiom, vP1608_N_1 <=> (~ vP1608_R_0 & (vP1608_KN_1 & ((vP1608_APZ_0 & (vP1608_NWZ_1 & vP1608_C_0)) | ((vP1608_NL_0 & (vP1608_NWZ_1 & vP1608_C_0)) | vP1608_N_0))))).
fof(ax,axiom, vP1608_R_1 <=> (~ vP1608_N_1 & (vP1608_KR_1 & ((vP1608_APZ_0 & (vP1608_RWZ_1 & vP1608_C_0)) | ((vP1608_RL_0 & (vP1608_RWZ_1 & vP1608_C_0)) | vP1608_R_0))))).
fof(ax,axiom, vP1608_C_1 <=> (~ vP1608_R_1 & (~ vP1608_N_1 & (vP1608_QC_0 | (~ vAPPDEL1_0 | vP1608_C_0))))).
fof(ax,axiom, vP1608_APZ_1 <=> (~ vP1608_QR_0 & (~ vP1608_QN_0 & (~ vP1608_KR_1 & ~ vP1608_KN_1)))).
fof(ax,axiom, vP1608_NLZ_1 <=> (vP1608_NWZ_1 & ~ vP1608_R_1)).
fof(ax,axiom, vP1608_RLZ_1 <=> (vP1608_RWZ_1 & ~ vP1608_N_1)).
fof(ax,axiom, vP1620_NWZ_1 <=> ((~ vP1620__RW_INHIBIT_0 & (vP1620R_UL_0 & (~ vP1620R__CALL_P_0 & vP1620_WZ_1))) | vP1620_NL_0)).
fof(ax,axiom, vP1620_RWZ_1 <=> ((~ vP1620__NW_INHIBIT_0 & (vP1620N_UL_0 & (~ vP1620N__CALL_P_0 & vP1620_WZ_1))) | vP1620_RL_0)).
fof(ax,axiom, vP1620_KN_1 <=> ((~ vP1620_QC_0 & ((vP1620_APZ_0 & (~ vP1620_RD_0 & vP1620_QN_0)) | vP1620_KN_0)) | (vP1620_RD_0 & (vP1620_KN_0 | (vP1620_APZ_0 & (~ vP1620_RD_0 & vP1620_QN_0)))))).
fof(ax,axiom, vP1620_KR_1 <=> ((~ vP1620_QC_0 & ((vP1620_APZ_0 & (~ vP1620_RD_0 & vP1620_QR_0)) | vP1620_KR_0)) | (vP1620_RD_0 & (vP1620_KR_0 | (vP1620_APZ_0 & (~ vP1620_RD_0 & vP1620_QR_0)))))).
fof(ax,axiom, vP1620_N_1 <=> (~ vP1620_R_0 & (vP1620_KN_1 & ((vP1620_APZ_0 & (vP1620_NWZ_1 & vP1620_C_0)) | ((vP1620_NL_0 & (vP1620_NWZ_1 & vP1620_C_0)) | vP1620_N_0))))).
fof(ax,axiom, vP1620_R_1 <=> (~ vP1620_N_1 & (vP1620_KR_1 & ((vP1620_APZ_0 & (vP1620_RWZ_1 & vP1620_C_0)) | ((vP1620_RL_0 & (vP1620_RWZ_1 & vP1620_C_0)) | vP1620_R_0))))).
fof(ax,axiom, vP1620_C_1 <=> (~ vP1620_R_1 & (~ vP1620_N_1 & (vP1620_QC_0 | (~ vAPPDEL1_0 | vP1620_C_0))))).
fof(ax,axiom, vP1620_APZ_1 <=> (~ vP1620_QR_0 & (~ vP1620_QN_0 & (~ vP1620_KR_1 & ~ vP1620_KN_1)))).
fof(ax,axiom, vP1620_NLZ_1 <=> (vP1620_NWZ_1 & ~ vP1620_R_1)).
fof(ax,axiom, vP1620_RLZ_1 <=> (vP1620_RWZ_1 & ~ vP1620_N_1)).
fof(ax,axiom, vP1622_NWZ_1 <=> ((~ vP1622__RW_INHIBIT_0 & (vP1622R_UL_0 & (~ vP1622R__CALL_P_0 & vP1622_WZ_1))) | vP1622_NL_0)).
fof(ax,axiom, vP1622_RWZ_1 <=> ((~ vP1622__NW_INHIBIT_0 & (vP1622N_UL_0 & (~ vP1622N__CALL_P_0 & vP1622_WZ_1))) | vP1622_RL_0)).
fof(ax,axiom, vP1622_KN_1 <=> ((~ vP1622_QC_0 & ((vP1622_APZ_0 & (~ vP1622_RD_0 & vP1622_QN_0)) | vP1622_KN_0)) | (vP1622_RD_0 & (vP1622_KN_0 | (vP1622_APZ_0 & (~ vP1622_RD_0 & vP1622_QN_0)))))).
fof(ax,axiom, vP1622_KR_1 <=> ((~ vP1622_QC_0 & ((vP1622_APZ_0 & (~ vP1622_RD_0 & vP1622_QR_0)) | vP1622_KR_0)) | (vP1622_RD_0 & (vP1622_KR_0 | (vP1622_APZ_0 & (~ vP1622_RD_0 & vP1622_QR_0)))))).
fof(ax,axiom, vP1622_N_1 <=> (~ vP1622_R_0 & (vP1622_KN_1 & ((vP1622_APZ_0 & (vP1622_NWZ_1 & vP1622_C_0)) | ((vP1622_NL_0 & (vP1622_NWZ_1 & vP1622_C_0)) | vP1622_N_0))))).
fof(ax,axiom, vP1622_R_1 <=> (~ vP1622_N_1 & (vP1622_KR_1 & ((vP1622_APZ_0 & (vP1622_RWZ_1 & vP1622_C_0)) | ((vP1622_RL_0 & (vP1622_RWZ_1 & vP1622_C_0)) | vP1622_R_0))))).
fof(ax,axiom, vP1622_C_1 <=> (~ vP1622_R_1 & (~ vP1622_N_1 & (vP1622_QC_0 | (~ vAPPDEL1_0 | vP1622_C_0))))).
fof(ax,axiom, vP1622_APZ_1 <=> (~ vP1622_QR_0 & (~ vP1622_QN_0 & (~ vP1622_KR_1 & ~ vP1622_KN_1)))).
fof(ax,axiom, vP1622_NLZ_1 <=> (vP1622_NWZ_1 & ~ vP1622_R_1)).
fof(ax,axiom, vP1622_RLZ_1 <=> (vP1622_RWZ_1 & ~ vP1622_N_1)).
fof(ax,axiom, vP1624_NWZ_1 <=> ((~ vP1624__RW_INHIBIT_0 & (vP1624R_UL_0 & (~ vP1624R__CALL_P_0 & vP1624_WZ_1))) | vP1624_NL_0)).
fof(ax,axiom, vP1624_RWZ_1 <=> ((~ vP1624__NW_INHIBIT_0 & (vP1624N_UL_0 & (~ vP1624N__CALL_P_0 & vP1624_WZ_1))) | vP1624_RL_0)).
fof(ax,axiom, vP1624_KN_1 <=> ((~ vP1624_QC_0 & ((vP1624_APZ_0 & (~ vP1624_RD_0 & vP1624_QN_0)) | vP1624_KN_0)) | (vP1624_RD_0 & (vP1624_KN_0 | (vP1624_APZ_0 & (~ vP1624_RD_0 & vP1624_QN_0)))))).
fof(ax,axiom, vP1624_KR_1 <=> ((~ vP1624_QC_0 & ((vP1624_APZ_0 & (~ vP1624_RD_0 & vP1624_QR_0)) | vP1624_KR_0)) | (vP1624_RD_0 & (vP1624_KR_0 | (vP1624_APZ_0 & (~ vP1624_RD_0 & vP1624_QR_0)))))).
fof(ax,axiom, vP1624_N_1 <=> (~ vP1624_R_0 & (vP1624_KN_1 & ((vP1624_APZ_0 & (vP1624_NWZ_1 & vP1624_C_0)) | ((vP1624_NL_0 & (vP1624_NWZ_1 & vP1624_C_0)) | vP1624_N_0))))).
fof(ax,axiom, vP1624_R_1 <=> (~ vP1624_N_1 & (vP1624_KR_1 & ((vP1624_APZ_0 & (vP1624_RWZ_1 & vP1624_C_0)) | ((vP1624_RL_0 & (vP1624_RWZ_1 & vP1624_C_0)) | vP1624_R_0))))).
fof(ax,axiom, vP1624_C_1 <=> (~ vP1624_R_1 & (~ vP1624_N_1 & (vP1624_QC_0 | (~ vAPPDEL1_0 | vP1624_C_0))))).
fof(ax,axiom, vP1624_APZ_1 <=> (~ vP1624_QR_0 & (~ vP1624_QN_0 & (~ vP1624_KR_1 & ~ vP1624_KN_1)))).
fof(ax,axiom, vP1624_NLZ_1 <=> (vP1624_NWZ_1 & ~ vP1624_R_1)).
fof(ax,axiom, vP1624_RLZ_1 <=> (vP1624_RWZ_1 & ~ vP1624_N_1)).
fof(ax,axiom, vS400_RD_1 <=> ((vIL822_ENABLED_0 & vS400_QRD_0) | (vS400_RD_0 & (~ vS400_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS400_P__RD_1 <=> ((vIL822_ENABLED_0 & vS400_P__QRD_0) | (vS400_P__RD_0 & (~ vS400_P__QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS410_RD_1 <=> ((vIL822_ENABLED_0 & vS410_QRD_0) | (vS410_RD_0 & (~ vS410_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS410_P__RD_1 <=> ((vIL822_ENABLED_0 & vS410_P__QRD_0) | (vS410_P__RD_0 & (~ vS410_P__QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS420_RD_1 <=> ((vIL822_ENABLED_0 & vS420_QRD_0) | (vS420_RD_0 & (~ vS420_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS430_RD_1 <=> ((vIL822_ENABLED_0 & vS430_QRD_0) | (vS430_RD_0 & (~ vS430_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS440_RD_1 <=> ((vIL822_ENABLED_0 & vS440_QRD_0) | (vS440_RD_0 & (~ vS440_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS450_P__RD_1 <=> ((vIL822_ENABLED_0 & vS450_P__QRD_0) | (vS450_P__RD_0 & (~ vS450_P__QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS460_RD_1 <=> ((vIL822_ENABLED_0 & vS460_QRD_0) | (vS460_RD_0 & (~ vS460_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS460_P__RD_1 <=> ((vIL822_ENABLED_0 & vS460_P__QRD_0) | (vS460_P__RD_0 & (~ vS460_P__QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS470_RD_1 <=> ((vIL822_ENABLED_0 & vS470_QRD_0) | (vS470_RD_0 & (~ vS470_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS470_P__RD_1 <=> ((vIL822_ENABLED_0 & vS470_P__QRD_0) | (vS470_P__RD_0 & (~ vS470_P__QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTAA_RD_1 <=> ((vIL822_ENABLED_0 & vTAA_QRD_0) | (vTAA_RD_0 & (~ vTAA_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTAB_RD_1 <=> ((vIL822_ENABLED_0 & vTAB_QRD_0) | (vTAB_RD_0 & (~ vTAB_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTAC_RD_1 <=> ((vIL822_ENABLED_0 & vTAC_QRD_0) | (vTAC_RD_0 & (~ vTAC_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTAD_RD_1 <=> ((vIL822_ENABLED_0 & vTAD_QRD_0) | (vTAD_RD_0 & (~ vTAD_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTAE_RD_1 <=> ((vIL822_ENABLED_0 & vTAE_QRD_0) | (vTAE_RD_0 & (~ vTAE_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTAF_RD_1 <=> ((vIL822_ENABLED_0 & vTAF_QRD_0) | (vTAF_RD_0 & (~ vTAF_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTAG_RD_1 <=> ((vIL822_ENABLED_0 & vTAG_QRD_0) | (vTAG_RD_0 & (~ vTAG_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTBA_RD_1 <=> ((vIL822_ENABLED_0 & vTBA_QRD_0) | (vTBA_RD_0 & (~ vTBA_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTCA_RD_1 <=> ((vIL822_ENABLED_0 & vTCA_QRD_0) | (vTCA_RD_0 & (~ vTCA_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTDA_RD_1 <=> ((vIL822_ENABLED_0 & vTDA_QRD_0) | (vTDA_RD_0 & (~ vTDA_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTEA_RD_1 <=> ((vIL822_ENABLED_0 & vTEA_QRD_0) | (vTEA_RD_0 & (~ vTEA_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTFA_RD_1 <=> ((vIL822_ENABLED_0 & vTFA_QRD_0) | (vTFA_RD_0 & (~ vTFA_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTGA_RD_1 <=> ((vIL822_ENABLED_0 & vTGA_QRD_0) | (vTGA_RD_0 & (~ vTGA_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vTHA_RD_1 <=> ((vIL822_ENABLED_0 & vTHA_QRD_0) | (vTHA_RD_0 & (~ vTHA_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vP1602_RD_1 <=> ((vP1602_KN_1 & (vIL822_ENABLED_0 & vP1602_QRD_0)) | ((vP1602_KR_1 & (vIL822_ENABLED_0 & vP1602_QRD_0)) | (vP1602_RD_0 & (~ vP1602_QXRD_0 | ~ vIL822_ENABLED_0))))).
fof(ax,axiom, vP1604_RD_1 <=> ((vP1604_KN_1 & (vIL822_ENABLED_0 & vP1604_QRD_0)) | ((vP1604_KR_1 & (vIL822_ENABLED_0 & vP1604_QRD_0)) | (vP1604_RD_0 & (~ vP1604_QXRD_0 | ~ vIL822_ENABLED_0))))).
fof(ax,axiom, vP1606_RD_1 <=> ((vP1606_KN_1 & (vIL822_ENABLED_0 & vP1606_QRD_0)) | ((vP1606_KR_1 & (vIL822_ENABLED_0 & vP1606_QRD_0)) | (vP1606_RD_0 & (~ vP1606_QXRD_0 | ~ vIL822_ENABLED_0))))).
fof(ax,axiom, vP1608_RD_1 <=> ((vP1608_KN_1 & (vIL822_ENABLED_0 & vP1608_QRD_0)) | ((vP1608_KR_1 & (vIL822_ENABLED_0 & vP1608_QRD_0)) | (vP1608_RD_0 & (~ vP1608_QXRD_0 | ~ vIL822_ENABLED_0))))).
fof(ax,axiom, vP1620_RD_1 <=> ((vP1620_KN_1 & (vIL822_ENABLED_0 & vP1620_QRD_0)) | ((vP1620_KR_1 & (vIL822_ENABLED_0 & vP1620_QRD_0)) | (vP1620_RD_0 & (~ vP1620_QXRD_0 | ~ vIL822_ENABLED_0))))).
fof(ax,axiom, vP1622_RD_1 <=> ((vP1622_KN_1 & (vIL822_ENABLED_0 & vP1622_QRD_0)) | ((vP1622_KR_1 & (vIL822_ENABLED_0 & vP1622_QRD_0)) | (vP1622_RD_0 & (~ vP1622_QXRD_0 | ~ vIL822_ENABLED_0))))).
fof(ax,axiom, vP1624_RD_1 <=> ((vP1624_KN_1 & (vIL822_ENABLED_0 & vP1624_QRD_0)) | ((vP1624_KR_1 & (vIL822_ENABLED_0 & vP1624_QRD_0)) | (vP1624_RD_0 & (~ vP1624_QXRD_0 | ~ vIL822_ENABLED_0))))).
fof(ax,axiom, vS100_RD_1 <=> ((vIL822_ENABLED_0 & vS100_QRD_0) | (vS100_RD_0 & (~ vS100_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS104_RD_1 <=> ((vIL822_ENABLED_0 & vS104_QRD_0) | (vS104_RD_0 & (~ vS104_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS104__R_RD_1 <=> ((vIL822_ENABLED_0 & vS104__R_QRD_0) | (vS104__R_RD_0 & (~ vS104__R_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS106_RD_1 <=> ((vIL822_ENABLED_0 & vS106_QRD_0) | (vS106_RD_0 & (~ vS106_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS106__AUTO_RD_1 <=> ((vIL822_ENABLED_0 & vS106__AUTO_QRD_0) | (vS106__AUTO_RD_0 & (~ vS106__AUTO_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS110_RD_1 <=> ((vIL822_ENABLED_0 & vS110_QRD_0) | (vS110_RD_0 & (~ vS110_QXRD_0 | ~ vIL822_ENABLED_0)))).
fof(ax,axiom, vS400_DREQ_1 <=> (~ vNCALL__S_S400_0 & ((vIL822_PBC_0 & (~ vS400_P__QD_0 & (vIL822_ENABLED_0 & vS400_QD_0))) | (vS400_DREQ_0 & (vIL822_ENABLED_0 & vS400_QD_0))))).
fof(ax,axiom, vS400_P__DREQ_1 <=> (~ vNCALL__S_S400_0 & ((vIL822_PBC_0 & (~ vS400_QD_0 & (vTBA_OCC_IL__1 & (vIL822_ENABLED_0 & vS400_P__QD_0)))) | (vS400_P__DREQ_0 & (vTBA_OCC_IL__1 & (vIL822_ENABLED_0 & vS400_P__QD_0)))))).
fof(ax,axiom, vS410_DREQ_1 <=> (~ vNCALL__S_S410_0 & ((vIL822_PBC_0 & (~ vS410_P__QD_0 & (vIL822_ENABLED_0 & vS410_QD_0))) | (vS410_DREQ_0 & (vIL822_ENABLED_0 & vS410_QD_0))))).
fof(ax,axiom, vS410_P__DREQ_1 <=> (~ vNCALL__S_S410_0 & ((vIL822_PBC_0 & (~ vS410_QD_0 & (vTCA_OCC_IL__1 & (vIL822_ENABLED_0 & vS410_P__QD_0)))) | (vS410_P__DREQ_0 & (vTCA_OCC_IL__1 & (vIL822_ENABLED_0 & vS410_P__QD_0)))))).
fof(ax,axiom, vS420_DREQ_1 <=> (~ vNCALL__S_S420_0 & ((vIL822_PBC_0 & (vIL822_ENABLED_0 & vS420_QD_0)) | (vS420_DREQ_0 & (vIL822_ENABLED_0 & vS420_QD_0))))).
fof(ax,axiom, vS430_DREQ_1 <=> (~ vNCALL__S_S430_0 & ((vIL822_PBC_0 & (vIL822_ENABLED_0 & vS430_QD_0)) | (vS430_DREQ_0 & (vIL822_ENABLED_0 & vS430_QD_0))))).
fof(ax,axiom, vS440_DREQ_1 <=> (~ vNCALL__S_S440_0 & ((vIL822_PBC_0 & (vIL822_ENABLED_0 & vS440_QD_0)) | (vS440_DREQ_0 & (vIL822_ENABLED_0 & vS440_QD_0))))).
fof(ax,axiom, vS450_P__DREQ_1 <=> (~ vNCALL__S_S450_0 & ((vIL822_PBC_0 & (vTFA_OCC_IL__1 & (vIL822_ENABLED_0 & vS450_P__QD_0))) | (vS450_P__DREQ_0 & (vTFA_OCC_IL__1 & (vIL822_ENABLED_0 & vS450_P__QD_0)))))).
fof(ax,axiom, vS460_DREQ_1 <=> (~ vNCALL__S_S460_0 & ((vIL822_PBC_0 & (~ vS460_P__QD_0 & (vIL822_ENABLED_0 & vS460_QD_0))) | (vS460_DREQ_0 & (vIL822_ENABLED_0 & vS460_QD_0))))).
fof(ax,axiom, vS460_P__DREQ_1 <=> (~ vNCALL__S_S460_0 & ((vIL822_PBC_0 & (~ vS460_QD_0 & (vTGA_OCC_IL__1 & (vIL822_ENABLED_0 & vS460_P__QD_0)))) | (vS460_P__DREQ_0 & (vTGA_OCC_IL__1 & (vIL822_ENABLED_0 & vS460_P__QD_0)))))).
fof(ax,axiom, vS470_DREQ_1 <=> (~ vNCALL__S_S470_0 & ((vIL822_PBC_0 & (~ vS470_P__QD_0 & (vIL822_ENABLED_0 & vS470_QD_0))) | (vS470_DREQ_0 & (vIL822_ENABLED_0 & vS470_QD_0))))).
fof(ax,axiom, vS470_P__DREQ_1 <=> (~ vNCALL__S_S470_0 & ((vIL822_PBC_0 & (~ vS470_QD_0 & (vTHA_OCC_IL__1 & (vIL822_ENABLED_0 & vS470_P__QD_0)))) | (vS470_P__DREQ_0 & (vTHA_OCC_IL__1 & (vIL822_ENABLED_0 & vS470_P__QD_0)))))).
fof(ax,axiom, vS100_AM__UREQ_1 <=> (~ vS100_QXR_0 & (~ vS100_AM___U_INHIBIT_0 & (~ vS100_RU_0 & (vIL822_ENABLED_0 & (~ vS100_UREQ_0 & (vIL822_PBC_0 & ((~ vS104_RD_1 & (vS104_QD_0 & vS100_QS_0)) | (vS104_QRDZ_0 & (vS104_QD_0 & vS100_QS_0)))))))))).
fof(ax,axiom, vS106_AM__PBP_1 <=> (~ vS470_P__QD_0 & (~ vS460_P__QD_0 & (~ vS450_P__QD_0 & (~ vS410_P__QD_0 & (~ vS470_QD_0 & (~ vS460_QD_0 & (~ vS110_QD_0 & (~ vS430_QD_0 & (~ vS420_QD_0 & (~ vS410_QD_0 & vS400_QD_0))))))))))).
fof(ax,axiom, vS106_AM__UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_AM___U_INHIBIT_0 & (vS106_AC__N_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_AM__PBP_1 & ((~ vS400_RD_1 & (vS400_QD_0 & vS106_QS_0)) | (vS400_QRDZ_0 & (vS400_QD_0 & vS106_QS_0)))))))))))).
fof(ax,axiom, vS106_AC__PBP_1 <=> (~ vS470_P__QD_0 & (~ vS460_P__QD_0 & (~ vS450_P__QD_0 & (~ vS410_P__QD_0 & (~ vS470_QD_0 & (~ vS460_QD_0 & (~ vS110_QD_0 & (~ vS430_QD_0 & (~ vS420_QD_0 & (~ vS410_QD_0 & (vS400_P__QD_0 & ~ vS400_QD_0)))))))))))).
fof(ax,axiom, vS106_AC__UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_AC___U_INHIBIT_0 & (vS106_AM__N_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_AC__PBP_1 & ((~ vS400_P__RD_1 & (vS400_P__QD_0 & vS106_QS_0)) | (vS400_P__QRDZ_0 & (vS400_P__QD_0 & vS106_QS_0)))))))))))).
fof(ax,axiom, vS106_BS_NP___PBP_1 <=> (~ vS470_P__QD_0 & (~ vS460_P__QD_0 & (~ vS450_P__QD_0 & (~ vS400_P__QD_0 & (~ vS470_QD_0 & (~ vS460_QD_0 & (~ vS110_QD_0 & (~ vS430_QD_0 & (~ vS420_QD_0 & (~ vS400_QD_0 & (~ vS410_P__QD_0 & vS410_QD_0)))))))))))).
fof(ax,axiom, vS106_BS_NP___UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_BS_NP____U_INHIBIT_0 & (vS106_BS_P___N_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_BS_NP___PBP_1 & ((~ vS410_RD_1 & (vS410_QD_0 & vS106_QS_0)) | (vS410_QRDZ_0 & (vS410_QD_0 & vS106_QS_0)))))))))))).
fof(ax,axiom, vS106_BS_P___PBP_1 <=> (~ vS470_P__QD_0 & (~ vS460_P__QD_0 & (~ vS450_P__QD_0 & (~ vS400_P__QD_0 & (~ vS470_QD_0 & (~ vS460_QD_0 & (~ vS110_QD_0 & (~ vS430_QD_0 & (~ vS420_QD_0 & (~ vS400_QD_0 & (vS410_P__QD_0 & ~ vS410_QD_0)))))))))))).
fof(ax,axiom, vS106_BS_P___UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_BS_P____U_INHIBIT_0 & (vS106_BS_NP___N_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_BS_P___PBP_1 & ((~ vS410_P__RD_1 & (vS410_P__QD_0 & vS106_QS_0)) | (vS410_P__QRDZ_0 & (vS410_P__QD_0 & vS106_QS_0)))))))))))).
fof(ax,axiom, vS106_CM__PBP_1 <=> (~ vS470_P__QD_0 & (~ vS460_P__QD_0 & (~ vS450_P__QD_0 & (~ vS410_P__QD_0 & (~ vS400_P__QD_0 & (~ vS470_QD_0 & (~ vS460_QD_0 & (~ vS110_QD_0 & (~ vS430_QD_0 & (~ vS410_QD_0 & (~ vS400_QD_0 & vS420_QD_0)))))))))))).
fof(ax,axiom, vS106_CM__UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_CM___U_INHIBIT_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_CM__PBP_1 & ((~ vS420_RD_1 & (vS420_QD_0 & vS106_QS_0)) | (vS420_QRDZ_0 & (vS420_QD_0 & vS106_QS_0))))))))))).
fof(ax,axiom, vS106_DS_NP___PBP_1 <=> (~ vS470_P__QD_0 & (~ vS460_P__QD_0 & (~ vS450_P__QD_0 & (~ vS410_P__QD_0 & (~ vS400_P__QD_0 & (~ vS470_QD_0 & (~ vS460_QD_0 & (~ vS110_QD_0 & (~ vS420_QD_0 & (~ vS410_QD_0 & (~ vS400_QD_0 & vS430_QD_0)))))))))))).
fof(ax,axiom, vS106_DS_NP___UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_DS_NP____U_INHIBIT_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_DS_NP___PBP_1 & ((~ vS430_RD_1 & (vS430_QD_0 & vS106_QS_0)) | (vS430_QRDZ_0 & (vS430_QD_0 & vS106_QS_0))))))))))).
fof(ax,axiom, vS106_EM__PBP_1 <=> (~ vS470_P__QD_0 & (~ vS460_P__QD_0 & (~ vS450_P__QD_0 & (~ vS410_P__QD_0 & (~ vS400_P__QD_0 & (~ vS470_QD_0 & (~ vS460_QD_0 & (~ vS430_QD_0 & (~ vS420_QD_0 & (~ vS410_QD_0 & (~ vS400_QD_0 & vS110_QD_0)))))))))))).
fof(ax,axiom, vS106_EM__UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_EM___U_INHIBIT_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_EM__PBP_1 & ((~ vS110_RD_1 & (vS110_QD_0 & vS106_QS_0)) | (vS110_QRDZ_0 & (vS110_QD_0 & vS106_QS_0))))))))))).
fof(ax,axiom, vS106_FS_P___PBP_1 <=> (~ vS470_P__QD_0 & (~ vS460_P__QD_0 & (~ vS410_P__QD_0 & (~ vS400_P__QD_0 & (~ vS470_QD_0 & (~ vS460_QD_0 & (~ vS110_QD_0 & (~ vS430_QD_0 & (~ vS420_QD_0 & (~ vS410_QD_0 & (~ vS400_QD_0 & vS450_P__QD_0)))))))))))).
fof(ax,axiom, vS106_FS_P___UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_FS_P____U_INHIBIT_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_FS_P___PBP_1 & ((~ vS450_P__RD_1 & (vS450_P__QD_0 & vS106_QS_0)) | (vS450_P__QRDZ_0 & (vS450_P__QD_0 & vS106_QS_0))))))))))).
fof(ax,axiom, vS106_GM__PBP_1 <=> (~ vS470_P__QD_0 & (~ vS450_P__QD_0 & (~ vS410_P__QD_0 & (~ vS400_P__QD_0 & (~ vS470_QD_0 & (~ vS110_QD_0 & (~ vS430_QD_0 & (~ vS420_QD_0 & (~ vS410_QD_0 & (~ vS400_QD_0 & vS460_QD_0))))))))))).
fof(ax,axiom, vS106_GM__UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_GM___U_INHIBIT_0 & (vS106_GC__N_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_GM__PBP_1 & ((~ vS460_RD_1 & (vS460_QD_0 & vS106_QS_0)) | (vS460_QRDZ_0 & (vS460_QD_0 & vS106_QS_0)))))))))))).
fof(ax,axiom, vS106_GC__PBP_1 <=> (~ vS470_P__QD_0 & (~ vS450_P__QD_0 & (~ vS410_P__QD_0 & (~ vS400_P__QD_0 & (~ vS470_QD_0 & (~ vS110_QD_0 & (~ vS430_QD_0 & (~ vS420_QD_0 & (~ vS410_QD_0 & (~ vS400_QD_0 & (vS460_P__QD_0 & ~ vS460_QD_0)))))))))))).
fof(ax,axiom, vS106_GC__UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_GC___U_INHIBIT_0 & (vS106_GM__N_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_GC__PBP_1 & ((~ vS460_P__RD_1 & (vS460_P__QD_0 & vS106_QS_0)) | (vS460_P__QRDZ_0 & (vS460_P__QD_0 & vS106_QS_0)))))))))))).
fof(ax,axiom, vS106_HM__PBP_1 <=> (~ vS460_P__QD_0 & (~ vS450_P__QD_0 & (~ vS410_P__QD_0 & (~ vS400_P__QD_0 & (~ vS460_QD_0 & (~ vS110_QD_0 & (~ vS430_QD_0 & (~ vS420_QD_0 & (~ vS410_QD_0 & (~ vS400_QD_0 & vS470_QD_0))))))))))).
fof(ax,axiom, vS106_HM__UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_HM___U_INHIBIT_0 & (vS106_HC__N_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_HM__PBP_1 & ((~ vS470_RD_1 & (vS470_QD_0 & vS106_QS_0)) | (vS470_QRDZ_0 & (vS470_QD_0 & vS106_QS_0)))))))))))).
fof(ax,axiom, vS106_HC__PBP_1 <=> (~ vS460_P__QD_0 & (~ vS450_P__QD_0 & (~ vS410_P__QD_0 & (~ vS400_P__QD_0 & (~ vS460_QD_0 & (~ vS110_QD_0 & (~ vS430_QD_0 & (~ vS420_QD_0 & (~ vS410_QD_0 & (~ vS400_QD_0 & (vS470_P__QD_0 & ~ vS470_QD_0)))))))))))).
fof(ax,axiom, vS106_HC__UREQ_1 <=> (~ vS106_QXR_0 & (~ vS106_HC___U_INHIBIT_0 & (vS106_HM__N_0 & (~ vS106_RU_0 & (vIL822_ENABLED_0 & (~ vS106_UREQ_0 & (vIL822_PBC_0 & (vS106_HC__PBP_1 & ((~ vS470_P__RD_1 & (vS470_P__QD_0 & vS106_QS_0)) | (vS470_P__QRDZ_0 & (vS470_P__QD_0 & vS106_QS_0)))))))))))).
fof(ax,axiom, vS110_AM__UREQ_1 <=> (~ vS110_QXR_0 & (~ vS110_AM___U_INHIBIT_0 & (~ vS110_RU_0 & (vIL822_ENABLED_0 & (~ vS110_UREQ_0 & (vIL822_PBC_0 & ((~ vS440_RD_1 & (vS440_QD_0 & vS110_QS_0)) | (vS440_QRDZ_0 & (vS440_QD_0 & vS110_QS_0)))))))))).
fof(ax,axiom, vS100_UREQ_1 <=> (~ vMSDP6_SGRC_1 & ((~ vS100_RD_1 & vS100_AM__UREQ_1) | (vS100_QRDZ_0 & vS100_AM__UREQ_1)))).
fof(ax,axiom, vS104__AUTO_REQ_1 <=> (~ vS104_QXA_0 & (~ vS104__AUTO_CAN_0 & (~ vMSDP6_SGRC_1 & (~ vS104__R_RD_1 & vS104_QA_0))))).
fof(ax,axiom, vS104__DEST_REQ_1 <=> vS104_QD_0).
fof(ax,axiom, vS104_DREQ_1 <=> (~ vS104__DEST_CALL_0 & ((vIL822_PBC_0 & (vIL822_ENABLED_0 & vS104__DEST_REQ_1)) | (vS104_DREQ_0 & (vIL822_ENABLED_0 & vS104__DEST_REQ_1))))).
fof(ax,axiom, vS106_UREQ_1 <=> (~ vMSDP6_SGRC_1 & ((~ vS106_RD_1 & (vS106_AM__UREQ_1 | (vS106_CM__UREQ_1 | (vS106_EM__UREQ_1 | (vS106_GM__UREQ_1 | (vS106_HM__UREQ_1 | (vS106_AC__UREQ_1 | (vS106_GC__UREQ_1 | (vS106_HC__UREQ_1 | (vS106_BS_NP___UREQ_1 | (vS106_DS_NP___UREQ_1 | (vS106_BS_P___UREQ_1 | vS106_FS_P___UREQ_1)))))))))))) | (vS106_QRDZ_0 & (vS106_CM__UREQ_1 | ((vS106_EM__UREQ_1 | (vS106_GM__UREQ_1 | (vS106_HM__UREQ_1 | (vS106_AC__UREQ_1 | (vS106_GC__UREQ_1 | (vS106_HC__UREQ_1 | (vS106_BS_NP___UREQ_1 | (vS106_DS_NP___UREQ_1 | (vS106_BS_P___UREQ_1 | vS106_FS_P___UREQ_1))))))))) | vS106_AM__UREQ_1)))))).
fof(ax,axiom, vS110_UREQ_1 <=> (~ vMSDP6_SGRC_1 & ((~ vS110_RD_1 & vS110_AM__UREQ_1) | (vS110_QRDZ_0 & vS110_AM__UREQ_1)))).
fof(ax,axiom, vS110__DEST_REQ_1 <=> vS110_QD_0).
fof(ax,axiom, vS110_DREQ_1 <=> (~ vS110__DEST_CALL_0 & ((vIL822_PBC_0 & (vIL822_ENABLED_0 & vS110__DEST_REQ_1)) | (vS110_DREQ_0 & (vIL822_ENABLED_0 & vS110__DEST_REQ_1))))).
fof(ax,axiom, vS400_PBC_1 <=> (~ vS400_P__QD_0 & ~ vS400_QD_0)).
fof(ax,axiom, vS410_PBC_1 <=> (~ vS410_P__QD_0 & ~ vS410_QD_0)).
fof(ax,axiom, vS420_PBC_1 <=> ~ vS420_QD_0).
fof(ax,axiom, vS430_PBC_1 <=> ~ vS430_QD_0).
fof(ax,axiom, vS440_PBC_1 <=> ~ vS440_QD_0).
fof(ax,axiom, vS450_PBC_1 <=> ~ vS450_P__QD_0).
fof(ax,axiom, vS460_PBC_1 <=> (~ vS460_P__QD_0 & ~ vS460_QD_0)).
fof(ax,axiom, vS470_PBC_1 <=> (~ vS470_P__QD_0 & ~ vS470_QD_0)).
fof(ax,axiom, vS100_PBC_1 <=> ~ vS100_QS_0).
fof(ax,axiom, vS104_PBC_1 <=> ~ vS104_QD_0).
fof(ax,axiom, vS106_PBC_1 <=> ~ vS106_QS_0).
fof(ax,axiom, vS110_PBC_1 <=> (~ vS110_QD_0 & ~ vS110_QS_0)).
fof(ax,axiom, vIL822__ND_PBC_1 <=> (vS110_PBC_1 & (vS460_PBC_1 & (vS450_PBC_1 & (vS440_PBC_1 & (vS430_PBC_1 & (vS420_PBC_1 & (vS410_PBC_1 & (vS400_PBC_1 & (vS106_PBC_1 & (vS104_PBC_1 & vS100_PBC_1))))))))))).
fof(ax,axiom, vIL822__OD_PBC_1 <=> vS470_PBC_1).
fof(ax,axiom, vIL822_PBC_1 <=> (vIL822__OD_PBC_1 & vIL822__ND_PBC_1)).
fof(ax,axiom, vS100_TORR_1 <=> (~ vS100_QXR_0 & (~ vS100_GS_0 & (vS100_ALS_0 & vS100_AM__TORR2_0)))).
fof(ax,axiom, vS106_TORR_1 <=> (~ vS106_QXR_0 & (~ vS106_GS_0 & (vS106_ALS_0 & (vS106_AM__TORR2_0 | (vS106_CM__TORR2_0 | (vS106_EM__TORR2_0 | (vS106_GM__TORR2_0 | (vS106_HM__TORR2_0 | (vS106_AC__TORR2_0 | (vS106_GC__TORR2_0 | (vS106_HC__TORR2_0 | (vS106_BS_NP___TORR2_0 | (vS106_DS_NP___TORR2_0 | (vS106_BS_P___TORR2_0 | vS106_FS_P___TORR2_0))))))))))))))).
fof(ax,axiom, vS110_TORR_1 <=> (~ vS110_QXR_0 & (~ vS110_GS_0 & (vS110_ALS_0 & vS110_AM__TORR2_0)))).
fof(ax,axiom, vS100_AM__TORR2_1 <=> (~ vS100_TORR_1 & (vS100_AM__U_0 & (vS100_AM__TORR1_0 | vS100_AM__TORR2_0)))).
fof(ax,axiom, vS100_AM__TORR1_1 <=> (vS100__ASP_CON_0 & (vS100_AM__U_0 & vS100_OIE_1))).
fof(ax,axiom, vS106_AM__TORR2_1 <=> (~ vS106_TORR_1 & (vS106_AM__U_0 & (vTAD_OCC_IL__1 & (vS106_AM__TORR1_0 | vS106_AM__TORR2_0))))).
fof(ax,axiom, vS106_AM__TORR1_1 <=> ((vS106__ASP_CON_0 & (vS106_AM__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_AM__TORR1_0 & (vS106_AM__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_AC__TORR2_1 <=> (~ vS106_TORR_1 & (vS106_AC__U_0 & (vTAD_OCC_IL__1 & (vS106_AC__TORR1_0 | vS106_AC__TORR2_0))))).
fof(ax,axiom, vS106_AC__TORR1_1 <=> ((vS106__SUB_GE_0 & (vS106_AC__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_AC__TORR1_0 & (vS106_AC__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_BS_NP___TORR2_1 <=> (~ vS106_TORR_1 & (vS106_BS_NP___U_0 & (vTAD_OCC_IL__1 & (vS106_BS_NP___TORR1_0 | vS106_BS_NP___TORR2_0))))).
fof(ax,axiom, vS106_BS_NP___TORR1_1 <=> ((vS106__SUB_GE_0 & (vS106_BS_NP___U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_BS_NP___TORR1_0 & (vS106_BS_NP___U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_BS_P___TORR2_1 <=> (~ vS106_TORR_1 & (vS106_BS_P___U_0 & (vTAD_OCC_IL__1 & (vS106_BS_P___TORR1_0 | vS106_BS_P___TORR2_0))))).
fof(ax,axiom, vS106_BS_P___TORR1_1 <=> ((vS106__SUB_GE_0 & (vS106_BS_P___U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_BS_P___TORR1_0 & (vS106_BS_P___U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_CM__TORR2_1 <=> (~ vS106_TORR_1 & (vS106_CM__U_0 & (vTAD_OCC_IL__1 & (vS106_CM__TORR1_0 | vS106_CM__TORR2_0))))).
fof(ax,axiom, vS106_CM__TORR1_1 <=> ((vS106__ASP_CON_0 & (vS106_CM__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_CM__TORR1_0 & (vS106_CM__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_DS_NP___TORR2_1 <=> (~ vS106_TORR_1 & (vS106_DS_NP___U_0 & (vTAD_OCC_IL__1 & (vS106_DS_NP___TORR1_0 | vS106_DS_NP___TORR2_0))))).
fof(ax,axiom, vS106_DS_NP___TORR1_1 <=> ((vS106__SUB_GE_0 & (vS106_DS_NP___U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_DS_NP___TORR1_0 & (vS106_DS_NP___U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_EM__TORR2_1 <=> (~ vS106_TORR_1 & (vS106_EM__U_0 & (vTAD_OCC_IL__1 & (vS106_EM__TORR1_0 | vS106_EM__TORR2_0))))).
fof(ax,axiom, vS106_EM__TORR1_1 <=> ((vS106__ASP_CON_0 & (vS106_EM__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_EM__TORR1_0 & (vS106_EM__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_FS_P___TORR2_1 <=> (~ vS106_TORR_1 & (vS106_FS_P___U_0 & (vTAD_OCC_IL__1 & (vS106_FS_P___TORR1_0 | vS106_FS_P___TORR2_0))))).
fof(ax,axiom, vS106_FS_P___TORR1_1 <=> ((vS106__SUB_GE_0 & (vS106_FS_P___U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_FS_P___TORR1_0 & (vS106_FS_P___U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_GM__TORR2_1 <=> (~ vS106_TORR_1 & (vS106_GM__U_0 & (vTAD_OCC_IL__1 & (vS106_GM__TORR1_0 | vS106_GM__TORR2_0))))).
fof(ax,axiom, vS106_GM__TORR1_1 <=> ((vS106__ASP_CON_0 & (vS106_GM__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_GM__TORR1_0 & (vS106_GM__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_GC__TORR2_1 <=> (~ vS106_TORR_1 & (vS106_GC__U_0 & (vTAD_OCC_IL__1 & (vS106_GC__TORR1_0 | vS106_GC__TORR2_0))))).
fof(ax,axiom, vS106_GC__TORR1_1 <=> ((vS106__SUB_GE_0 & (vS106_GC__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_GC__TORR1_0 & (vS106_GC__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_HM__TORR2_1 <=> (~ vS106_TORR_1 & (vS106_HM__U_0 & (vTAD_OCC_IL__1 & (vS106_HM__TORR1_0 | vS106_HM__TORR2_0))))).
fof(ax,axiom, vS106_HM__TORR1_1 <=> ((vS106__ASP_CON_0 & (vS106_HM__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_HM__TORR1_0 & (vS106_HM__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS106_HC__TORR2_1 <=> (~ vS106_TORR_1 & (vS106_HC__U_0 & (vTAD_OCC_IL__1 & (vS106_HC__TORR1_0 | vS106_HC__TORR2_0))))).
fof(ax,axiom, vS106_HC__TORR1_1 <=> ((vS106__SUB_GE_0 & (vS106_HC__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))) | (vS106_HC__TORR1_0 & (vS106_HC__U_0 & (vTAD_CLR_IL__1 & (vTAC_OCC_IL__1 & vS106_OIE_1)))))).
fof(ax,axiom, vS110_AM__TORR2_1 <=> (~ vS110_TORR_1 & (vS110_AM__U_0 & ((vTAG_OCC_IL__1 & (vS110_AM__TORR1_0 | vS110_AM__TORR2_0)) | (vS110_AM__TISP_0 & (vS110_AM__TORR2_0 | vS110_AM__TORR1_0)))))).
fof(ax,axiom, vS110_AM__TORR1_1 <=> (vS110__ASP_CON_0 & (vS110_AM__U_0 & (vS110_GS_0 & (vTAG_CLR_IL__1 & (vTAF_OCC_IL__1 & vS110_OIE_1)))))).
fof(ax,axiom, vS100_CAN_1 <=> (vS100_RU_0 & (vS100_QXR_0 | (vS100_TORR_1 | (vMSDP6_SGRC_1 | (vLOS2_JR_0 & (vLOS2_JS_1 & vAPPDEL1_0))))))).
fof(ax,axiom, vS104__AUTO_CAN_1 <=> (vS104__AUTO_SET_0 & (vS104_QXA_0 | (vMSDP6_SGRC_1 | (vLOS2_JR_0 & (vLOS2_JS_1 & vAPPDEL1_0)))))).
fof(ax,axiom, vS106_CAN_1 <=> (vS106_RU_0 & (vS106_QXR_0 | (vS106_TORR_1 | (vMSDP6_SGRC_1 | (vLOS2_JR_0 & (vLOS2_JS_1 & vAPPDEL1_0))))))).
fof(ax,axiom, vS110_CAN_1 <=> (vS110_RU_0 & (vS110_QXR_0 | (vS110_TORR_1 | (vMSDP6_SGRC_1 | (vLOS2_JR_0 & (vLOS2_JS_1 & vAPPDEL1_0))))))).
fof(ax,axiom, vNUA__C_S100_1 <=> (vS100_UREQ_1 | (vS100_RU_0 & (vNUA__C_S100_0 & ~ vS100_CAN_1)))).
fof(ax,axiom, vS100_UAZ_1 <=> vNUA__C_S100_1).
fof(ax,axiom, vNUA_TAA_1 <=> vNUA__C_S100_1).
fof(ax,axiom, vNUA__C_S102_1 <=> vNUA_TAA_1).
fof(ax,axiom, vS104_UAD_1 <=> vNUA__C_S102_1).
fof(ax,axiom, vNUA__C_S106_1 <=> (vS106_UREQ_1 | (vS106_RU_0 & (vNUA__C_S106_0 & ~ vS106_CAN_1)))).
fof(ax,axiom, vS106_UAZ_1 <=> vNUA__C_S106_1).
fof(ax,axiom, vNUA_TAC_1 <=> vNUA__C_S106_1).
fof(ax,axiom, vNUA__N_P1602_1 <=> (vP1602_NLZ_1 & vNUA_TAC_1)).
fof(ax,axiom, vNUA__R_P1602_1 <=> (vP1602_RLZ_1 & vNUA_TAC_1)).
fof(ax,axiom, vNUA__N_P1604_1 <=> (vP1604_NLZ_1 & vNUA__R_P1602_1)).
fof(ax,axiom, vNUA__R_P1604_1 <=> (vP1604_RLZ_1 & vNUA__R_P1602_1)).
fof(ax,axiom, vNUA__N_P1606_1 <=> (vP1606_NLZ_1 & vNUA__N_P1604_1)).
fof(ax,axiom, vNUA__R_P1606_1 <=> (vP1606_RLZ_1 & vNUA__N_P1604_1)).
fof(ax,axiom, vNUA__N_P1608_1 <=> (vP1608_NLZ_1 & vNUA__N_P1606_1)).
fof(ax,axiom, vNUA__R_P1608_1 <=> (vP1608_RLZ_1 & vNUA__N_P1606_1)).
fof(ax,axiom, vNUA_TBA_1 <=> vNUA__N_P1608_1).
fof(ax,axiom, vNUA_P__TBA_1 <=> vNUA__N_P1608_1).
fof(ax,axiom, vS400_UAD_1 <=> vNUA_TBA_1).
fof(ax,axiom, vS400_P__UAD_1 <=> vNUA_P__TBA_1).
fof(ax,axiom, vNUA_TCA_1 <=> vNUA__R_P1608_1).
fof(ax,axiom, vNUA_P__TCA_1 <=> vNUA__R_P1608_1).
fof(ax,axiom, vS410_UAD_1 <=> vNUA_TCA_1).
fof(ax,axiom, vS410_P__UAD_1 <=> vNUA_P__TCA_1).
fof(ax,axiom, vNUA_TDA_1 <=> vNUA__R_P1606_1).
fof(ax,axiom, vS420_UAD_1 <=> vNUA_TDA_1).
fof(ax,axiom, vNUA_TEA_1 <=> vNUA__R_P1604_1).
fof(ax,axiom, vS430_UAD_1 <=> vNUA_TEA_1).
fof(ax,axiom, vNUA__N_P1620_1 <=> (vP1620_NLZ_1 & vNUA__N_P1602_1)).
fof(ax,axiom, vNUA__R_P1620_1 <=> (vP1620_RLZ_1 & vNUA__N_P1602_1)).
fof(ax,axiom, vNUA_TAF_1 <=> vNUA__N_P1620_1).
fof(ax,axiom, vS110_UAD_1 <=> vNUA_TAF_1).
fof(ax,axiom, vNUA__C_S110_1 <=> (vS110_UREQ_1 | (vS110_RU_0 & (vNUA__C_S110_0 & ~ vS110_CAN_1)))).
fof(ax,axiom, vS110_UAZ_1 <=> vNUA__C_S110_1).
fof(ax,axiom, vNUA_TAG_1 <=> vNUA__C_S110_1).
fof(ax,axiom, vS440_UAD_1 <=> vNUA_TAG_1).
fof(ax,axiom, vNUA__N_P1622_1 <=> (vP1622_NLZ_1 & vNUA__R_P1620_1)).
fof(ax,axiom, vNUA__R_P1622_1 <=> (vP1622_RLZ_1 & vNUA__R_P1620_1)).
fof(ax,axiom, vNUA_P__TFA_1 <=> vNUA__R_P1622_1).
fof(ax,axiom, vS450_P__UAD_1 <=> vNUA_P__TFA_1).
fof(ax,axiom, vNUA__N_P1624_1 <=> (vP1624_NLZ_1 & vNUA__N_P1622_1)).
fof(ax,axiom, vNUA__R_P1624_1 <=> (vP1624_RLZ_1 & vNUA__N_P1622_1)).
fof(ax,axiom, vNUA_TGA_1 <=> vNUA__R_P1624_1).
fof(ax,axiom, vNUA_P__TGA_1 <=> vNUA__R_P1624_1).
fof(ax,axiom, vS460_UAD_1 <=> vNUA_TGA_1).
fof(ax,axiom, vS460_P__UAD_1 <=> vNUA_P__TGA_1).
fof(ax,axiom, vNUA_THA_1 <=> vNUA__N_P1624_1).
fof(ax,axiom, vNUA_P__THA_1 <=> vNUA__N_P1624_1).
fof(ax,axiom, vS470_UAD_1 <=> vNUA_THA_1).
fof(ax,axiom, vS470_P__UAD_1 <=> vNUA_P__THA_1).
fof(ax,axiom, vNUAOL__C_S110_1 <=> (vS110_UAD_1 & (vS110_DREQ_1 | vNUAOL__C_S110_0))).
fof(ax,axiom, vNUAOL_TAG_1 <=> vNUAOL__C_S110_1).
fof(ax,axiom, vNCALLOL_TAG_1 <=> vNUAOL_TAG_1).
fof(ax,axiom, vNCALL__S_S470_1 <=> ((vS470_UAD_1 & (vS470_DREQ_1 | vNCALL__S_S470_0)) | (vS470_P__UAD_1 & (vS470_P__DREQ_1 | vNCALL__S_S470_0)))).
fof(ax,axiom, vNCALL_THA_1 <=> ((vNUA_THA_1 & vNCALL__S_S470_1) | (vNUA_P__THA_1 & vNCALL__S_S470_1))).
fof(ax,axiom, vNCALL__S_S460_1 <=> ((vS460_UAD_1 & (vS460_DREQ_1 | vNCALL__S_S460_0)) | (vS460_P__UAD_1 & (vS460_P__DREQ_1 | vNCALL__S_S460_0)))).
fof(ax,axiom, vNCALL_TGA_1 <=> ((vNUA_TGA_1 & vNCALL__S_S460_1) | (vNUA_P__TGA_1 & vNCALL__S_S460_1))).
fof(ax,axiom, vNCALL__N_P1624_1 <=> (vNUA__N_P1624_1 & vNCALL_THA_1)).
fof(ax,axiom, vNCALL__R_P1624_1 <=> (vNUA__R_P1624_1 & vNCALL_TGA_1)).
fof(ax,axiom, vNCALL__C_P1624_1 <=> ((~ vNCALL__R_P1624_1 & vNCALL__N_P1624_1) | (~ vNCALL__N_P1624_1 & vNCALL__R_P1624_1))).
fof(ax,axiom, vNCALL__S_S450_1 <=> (vS450_P__UAD_1 & (vS450_P__DREQ_1 | vNCALL__S_S450_0))).
fof(ax,axiom, vNCALL_TFA_1 <=> (vNUA_P__TFA_1 & vNCALL__S_S450_1)).
fof(ax,axiom, vNCALL__N_P1622_1 <=> (vNUA__N_P1622_1 & vNCALL__C_P1624_1)).
fof(ax,axiom, vNCALL__R_P1622_1 <=> (vNUA__R_P1622_1 & vNCALL_TFA_1)).
fof(ax,axiom, vNCALL__C_P1622_1 <=> ((~ vNCALL__R_P1622_1 & vNCALL__N_P1622_1) | (~ vNCALL__N_P1622_1 & vNCALL__R_P1622_1))).
fof(ax,axiom, vNCALL__S_S440_1 <=> (vS440_UAD_1 & (vS440_DREQ_1 | vNCALL__S_S440_0))).
fof(ax,axiom, vNCALL_TAG_1 <=> (vNUA_TAG_1 & vNCALL__S_S440_1)).
fof(ax,axiom, vNCALL__S_S110_1 <=> (vS110_UAD_1 & ((vNUAOL__C_S110_1 & (vNCALLOL_TAG_1 & vS110_DREQ_1)) | vNCALL__S_S110_0))).
fof(ax,axiom, vNCALL_TAF_1 <=> (vNUA_TAF_1 & vNCALL__S_S110_1)).
fof(ax,axiom, vNCALL__N_P1620_1 <=> (vNUA__N_P1620_1 & vNCALL_TAF_1)).
fof(ax,axiom, vNCALL__R_P1620_1 <=> (vNUA__R_P1620_1 & vNCALL__C_P1622_1)).
fof(ax,axiom, vNCALL__C_P1620_1 <=> ((~ vNCALL__R_P1620_1 & vNCALL__N_P1620_1) | (~ vNCALL__N_P1620_1 & vNCALL__R_P1620_1))).
fof(ax,axiom, vNCALL__S_S430_1 <=> (vS430_UAD_1 & (vS430_DREQ_1 | vNCALL__S_S430_0))).
fof(ax,axiom, vNCALL_TEA_1 <=> (vNUA_TEA_1 & vNCALL__S_S430_1)).
fof(ax,axiom, vNCALL__S_S420_1 <=> (vS420_UAD_1 & (vS420_DREQ_1 | vNCALL__S_S420_0))).
fof(ax,axiom, vNCALL_TDA_1 <=> (vNUA_TDA_1 & vNCALL__S_S420_1)).
fof(ax,axiom, vNCALL__S_S410_1 <=> ((vS410_UAD_1 & (vS410_DREQ_1 | vNCALL__S_S410_0)) | (vS410_P__UAD_1 & (vS410_P__DREQ_1 | vNCALL__S_S410_0)))).
fof(ax,axiom, vNCALL_TCA_1 <=> ((vNUA_TCA_1 & vNCALL__S_S410_1) | (vNUA_P__TCA_1 & vNCALL__S_S410_1))).
fof(ax,axiom, vNCALL__S_S400_1 <=> ((vS400_UAD_1 & (vS400_DREQ_1 | vNCALL__S_S400_0)) | (vS400_P__UAD_1 & (vS400_P__DREQ_1 | vNCALL__S_S400_0)))).
fof(ax,axiom, vNCALL_TBA_1 <=> ((vNUA_TBA_1 & vNCALL__S_S400_1) | (vNUA_P__TBA_1 & vNCALL__S_S400_1))).
fof(ax,axiom, vNCALL__N_P1608_1 <=> (vNUA__N_P1608_1 & vNCALL_TBA_1)).
fof(ax,axiom, vNCALL__R_P1608_1 <=> (vNUA__R_P1608_1 & vNCALL_TCA_1)).
fof(ax,axiom, vNCALL__C_P1608_1 <=> ((~ vNCALL__R_P1608_1 & vNCALL__N_P1608_1) | (~ vNCALL__N_P1608_1 & vNCALL__R_P1608_1))).
fof(ax,axiom, vNCALL__N_P1606_1 <=> (vNUA__N_P1606_1 & vNCALL__C_P1608_1)).
fof(ax,axiom, vNCALL__R_P1606_1 <=> (vNUA__R_P1606_1 & vNCALL_TDA_1)).
fof(ax,axiom, vNCALL__C_P1606_1 <=> ((~ vNCALL__R_P1606_1 & vNCALL__N_P1606_1) | (~ vNCALL__N_P1606_1 & vNCALL__R_P1606_1))).
fof(ax,axiom, vNCALL__N_P1604_1 <=> (vNUA__N_P1604_1 & vNCALL__C_P1606_1)).
fof(ax,axiom, vNCALL__R_P1604_1 <=> (vNUA__R_P1604_1 & vNCALL_TEA_1)).
fof(ax,axiom, vNCALL__C_P1604_1 <=> ((~ vNCALL__R_P1604_1 & vNCALL__N_P1604_1) | (~ vNCALL__N_P1604_1 & vNCALL__R_P1604_1))).
fof(ax,axiom, vNCALL__N_P1602_1 <=> (vNUA__N_P1602_1 & vNCALL__C_P1620_1)).
fof(ax,axiom, vNCALL__R_P1602_1 <=> (vNUA__R_P1602_1 & vNCALL__C_P1604_1)).
fof(ax,axiom, vNCALL__C_P1602_1 <=> ((~ vNCALL__R_P1602_1 & vNCALL__N_P1602_1) | (~ vNCALL__N_P1602_1 & vNCALL__R_P1602_1))).
fof(ax,axiom, vNCALL_TAC_1 <=> (vNUA_TAC_1 & vNCALL__C_P1602_1)).
fof(ax,axiom, vNCALL__S_S104_1 <=> (vS104_UAD_1 & (vS104_DREQ_1 | vNCALL__S_S104_0))).
fof(ax,axiom, vNCALL__S_S102_1 <=> (vNUA__C_S102_1 & vNCALL__S_S104_1)).
fof(ax,axiom, vNCALL_TAA_1 <=> (vNUA_TAA_1 & vNCALL__S_S102_1)).
fof(ax,axiom, vS104__DEST_CALL_1 <=> vNCALL__S_S104_1).
fof(ax,axiom, vS110__DEST_CALL_1 <=> vNCALL__S_S110_1).
fof(ax,axiom, vS100_CALL_1 <=> vNCALL_TAA_1).
fof(ax,axiom, vS106_CALL_1 <=> vNCALL_TAC_1).
fof(ax,axiom, vS110_CALL_1 <=> vNCALL_TAG_1).
fof(ax,axiom, vP1602N_CALL_1 <=> (vNCALL__C_P1602_1 & vNCALL__N_P1602_1)).
fof(ax,axiom, vP1602R_CALL_1 <=> (vNCALL__C_P1602_1 & vNCALL__R_P1602_1)).
fof(ax,axiom, vP1604N_CALL_1 <=> (vNCALL__C_P1604_1 & vNCALL__N_P1604_1)).
fof(ax,axiom, vP1604R_CALL_1 <=> (vNCALL__C_P1604_1 & vNCALL__R_P1604_1)).
fof(ax,axiom, vP1606N_CALL_1 <=> (vNCALL__C_P1606_1 & vNCALL__N_P1606_1)).
fof(ax,axiom, vP1606R_CALL_1 <=> (vNCALL__C_P1606_1 & vNCALL__R_P1606_1)).
fof(ax,axiom, vP1608N_CALL_1 <=> (vNCALL__C_P1608_1 & vNCALL__N_P1608_1)).
fof(ax,axiom, vP1608R_CALL_1 <=> (vNCALL__C_P1608_1 & vNCALL__R_P1608_1)).
fof(ax,axiom, vP1620N_CALL_1 <=> (vNCALL__C_P1620_1 & vNCALL__N_P1620_1)).
fof(ax,axiom, vP1620R_CALL_1 <=> (vNCALL__C_P1620_1 & vNCALL__R_P1620_1)).
fof(ax,axiom, vP1622N_CALL_1 <=> (vNCALL__C_P1622_1 & vNCALL__N_P1622_1)).
fof(ax,axiom, vP1622R_CALL_1 <=> (vNCALL__C_P1622_1 & vNCALL__R_P1622_1)).
fof(ax,axiom, vP1624N_CALL_1 <=> (vNCALL__C_P1624_1 & vNCALL__N_P1624_1)).
fof(ax,axiom, vP1624R_CALL_1 <=> (vNCALL__C_P1624_1 & vNCALL__R_P1624_1)).
fof(ax,axiom, vS400_P__DSET_1 <=> (~ vS400_DREQ_1 & ((vNCALL__S_S400_1 & vS400_P__DREQ_1) | vS400_P__DSET_0))).
fof(ax,axiom, vS410_P__DSET_1 <=> (~ vS410_DREQ_1 & ((vNCALL__S_S410_1 & vS410_P__DREQ_1) | vS410_P__DSET_0))).
fof(ax,axiom, vS450_P__DSET_1 <=> ((vNCALL__S_S450_1 & vS450_P__DREQ_1) | vS450_P__DSET_0)).
fof(ax,axiom, vS460_P__DSET_1 <=> (~ vS460_DREQ_1 & ((vNCALL__S_S460_1 & vS460_P__DREQ_1) | vS460_P__DSET_0))).
fof(ax,axiom, vS470_P__DSET_1 <=> (~ vS470_DREQ_1 & ((vNCALL__S_S470_1 & vS470_P__DREQ_1) | vS470_P__DSET_0))).
fof(ax,axiom, vS100_RU_1 <=> (~ vS100_CAN_1 & ((vS100_UAZ_1 & vS100_CALL_1) | vS100_RU_0))).
fof(ax,axiom, vS106_RU_1 <=> (~ vS106_CAN_1 & ((vS106_UAZ_1 & vS106_CALL_1) | vS106_RU_0))).
fof(ax,axiom, vS110_RU_1 <=> (~ vS110_CAN_1 & ((vS110_UAZ_1 & vS110_CALL_1) | vS110_RU_0))).
fof(ax,axiom, vS100_AM__U_1 <=> (vS100_RU_1 & (vS100_AM__UREQ_1 | vS100_AM__U_0))).
fof(ax,axiom, vS106_AM__U_1 <=> (vS106_RU_1 & (vS106_AM__UREQ_1 | vS106_AM__U_0))).
fof(ax,axiom, vS106_AC__U_1 <=> (vS106_RU_1 & (vS106_AC__UREQ_1 | vS106_AC__U_0))).
fof(ax,axiom, vS106_BS_NP___U_1 <=> (vS106_RU_1 & (vS106_BS_NP___UREQ_1 | vS106_BS_NP___U_0))).
fof(ax,axiom, vS106_BS_P___U_1 <=> (vS106_RU_1 & (vS106_BS_P___UREQ_1 | vS106_BS_P___U_0))).
fof(ax,axiom, vS106_CM__U_1 <=> (vS106_RU_1 & (vS106_CM__UREQ_1 | vS106_CM__U_0))).
fof(ax,axiom, vS106_DS_NP___U_1 <=> (vS106_RU_1 & (vS106_DS_NP___UREQ_1 | vS106_DS_NP___U_0))).
fof(ax,axiom, vS106_EM__U_1 <=> (vS106_RU_1 & (vS106_EM__UREQ_1 | vS106_EM__U_0))).
fof(ax,axiom, vS106_FS_P___U_1 <=> (vS106_RU_1 & (vS106_FS_P___UREQ_1 | vS106_FS_P___U_0))).
fof(ax,axiom, vS106_GM__U_1 <=> (vS106_RU_1 & (vS106_GM__UREQ_1 | vS106_GM__U_0))).
fof(ax,axiom, vS106_GC__U_1 <=> (vS106_RU_1 & (vS106_GC__UREQ_1 | vS106_GC__U_0))).
fof(ax,axiom, vS106_HM__U_1 <=> (vS106_RU_1 & (vS106_HM__UREQ_1 | vS106_HM__U_0))).
fof(ax,axiom, vS106_HC__U_1 <=> (vS106_RU_1 & (vS106_HC__UREQ_1 | vS106_HC__U_0))).
fof(ax,axiom, vS110_AM__U_1 <=> (vS110_RU_1 & (vS110_AM__UREQ_1 | vS110_AM__U_0))).
fof(ax,axiom, vS100_AM__N_1 <=> (~ vS100_AM__U_1 & ((vS100_ALS_0 & ~ vS100_RU_1) | vS100_AM__N_0))).
fof(ax,axiom, vS106_AM__N_1 <=> (~ vS106_AM__U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_AM__N_0))).
fof(ax,axiom, vS106_AC__N_1 <=> (~ vS106_AC__U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_AC__N_0))).
fof(ax,axiom, vS106_BS_NP___N_1 <=> (~ vS106_BS_NP___U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_BS_NP___N_0))).
fof(ax,axiom, vS106_BS_P___N_1 <=> (~ vS106_BS_P___U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_BS_P___N_0))).
fof(ax,axiom, vS106_CM__N_1 <=> (~ vS106_CM__U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_CM__N_0))).
fof(ax,axiom, vS106_DS_NP___N_1 <=> (~ vS106_DS_NP___U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_DS_NP___N_0))).
fof(ax,axiom, vS106_EM__N_1 <=> (~ vS106_EM__U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_EM__N_0))).
fof(ax,axiom, vS106_FS_P___N_1 <=> (~ vS106_FS_P___U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_FS_P___N_0))).
fof(ax,axiom, vS106_GM__N_1 <=> (~ vS106_GM__U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_GM__N_0))).
fof(ax,axiom, vS106_GC__N_1 <=> (~ vS106_GC__U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_GC__N_0))).
fof(ax,axiom, vS106_HM__N_1 <=> (~ vS106_HM__U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_HM__N_0))).
fof(ax,axiom, vS106_HC__N_1 <=> (~ vS106_HC__U_1 & ((vS106_ALS_0 & ~ vS106_RU_1) | vS106_HC__N_0))).
fof(ax,axiom, vS110_AM__N_1 <=> (~ vS110_AM__U_1 & ((vS110_ALS_0 & ~ vS110_RU_1) | vS110_AM__N_0))).
fof(ax,axiom, vS100_N_1 <=> vS100_AM__N_1).
fof(ax,axiom, vS106_N_1 <=> (vS106_FS_P___N_1 & (vS106_BS_P___N_1 & (vS106_DS_NP___N_1 & (vS106_BS_NP___N_1 & (vS106_HC__N_1 & (vS106_GC__N_1 & (vS106_AC__N_1 & (vS106_HM__N_1 & (vS106_GM__N_1 & (vS106_EM__N_1 & (vS106_CM__N_1 & vS106_AM__N_1)))))))))))).
fof(ax,axiom, vS110_N_1 <=> vS110_AM__N_1).
fof(ax,axiom, vS104__AUTO_SET_1 <=> (~ vS104__AUTO_CAN_1 & (vS104__AUTO_REQ_1 | vS104__AUTO_SET_0))).
fof(ax,axiom, vS104__R_K_1 <=> ~ vS104__AUTO_SET_1).
fof(ax,axiom, vS106_AUTO_1 <=> (vS106__AR__0 & (vS106_EM__U_1 & ((~ vS110_RD_1 & (~ vS106_RD_1 & (vS106_GS_0 & (~ vS106_RR_0 & (vIL822_ENABLED_0 & (~ vS106__AUTO_RD_1 & vS106_QAUTO_0)))))) | (~ vS106_QXAUTO_0 & vS106_AUTO_0))))).
fof(ax,axiom, vP1602N__CALL_P_1 <=> vP1602N_CALL_1).
fof(ax,axiom, vP1602R__CALL_P_1 <=> vP1602R_CALL_1).
fof(ax,axiom, vP1602__AUTOR_JS_1 <=> ((vP1602_RL_0 & (~ vP1602R__CALL_P_1 & (vP1602_NLZ_1 & (~ vP1602_KR_1 & ~ vP1602_KN_1)))) | (~ vP1602_NL_0 & (~ vP1602_RL_0 & (~ vP1602R__CALL_P_1 & (vP1602_NLZ_1 & (~ vP1602_KR_1 & ~ vP1602_KN_1))))))).
fof(ax,axiom, vP1602_AUTOR_1 <=> (vP1602__AUTOR_JR_0 & vP1602__AUTOR_JS_1)).
fof(ax,axiom, vP1602__AUTOR_K_1 <=> (~ vP1602_NWK_0 & (~ vP1602R__CALL_P_1 & (vP1602_AUTOR_1 | vP1602__AUTOR_K_0)))).
fof(ax,axiom, vP1602__AUTOR_ACK_1 <=> ((vP1602__AUTOR_XJR_0 & (vIL822_Q_AUTOR_ACK_0 & vP1602__AUTOR_K_1)) | (vP1602__AUTOR_ACK_0 & vP1602__AUTOR_K_1))).
fof(ax,axiom, vP1602__AUTOR_XJS_1 <=> (~ vP1602__AUTOR_ACK_1 & vP1602__AUTOR_K_1)).
fof(ax,axiom, vP1602_NL_1 <=> (vP1602_NLZ_1 & ((vP1602_N_1 | (vP1602N__CALL_P_1 | vP1602_AUTOR_1)) | (vP1602_NL_0 & ~ vP1602R__CALL_P_1)))).
fof(ax,axiom, vP1602_RL_1 <=> (vP1602_RLZ_1 & ((vP1602_R_1 | vP1602R__CALL_P_1) | (vP1602_RL_0 & (~ vP1602_AUTOR_1 & ~ vP1602N__CALL_P_1))))).
fof(ax,axiom, vP1602_LHL_1 <=> vP1602_NL_1).
fof(ax,axiom, vP1602_RHL_1 <=> vP1602_RL_1).
fof(ax,axiom, vP1602_DUM_1 <=> (vP1602_DUM_0 & (vP1602_RHL_1 & vP1602_LHL_1))).
fof(ax,axiom, vP1602_LHK_1 <=> (~ vP1602_RHK_0 & vP1602_LHK_M__0)).
fof(ax,axiom, vP1602_RHK_1 <=> (~ vP1602_LHK_1 & vP1602_RHK_M__0)).
fof(ax,axiom, vP1602_NWC_1 <=> (vP1602_LHK_1 & vP1602_NL_1)).
fof(ax,axiom, vP1602_RWC_1 <=> (vP1602_RHK_1 & vP1602_RL_1)).
fof(ax,axiom, vP1602_NWK_1 <=> (vP1602_WMC_0 & vP1602_NWC_1)).
fof(ax,axiom, vP1602_RWK_1 <=> (vP1602_WMC_0 & vP1602_RWC_1)).
fof(ax,axiom, vP1602_NKL_1 <=> (vP1602_NWK_1 & ~ vP1602_RWZ_1)).
fof(ax,axiom, vP1602_RKL_1 <=> (vP1602_RWK_1 & ~ vP1602_NWZ_1)).
fof(ax,axiom, vP1602_N__WJS_1 <=> (vP1602_NL_1 & ~ vP1602_NWC_1)).
fof(ax,axiom, vP1602_R__WJS_1 <=> (vP1602_RL_1 & ~ vP1602_RWC_1)).
fof(ax,axiom, vP1602_NWR_1 <=> (vP1602_NL_1 & (~ vP1602_N__WJR_0 & vP1602_N__WJS_1))).
fof(ax,axiom, vP1602_RWR_1 <=> (vP1602_RL_1 & (~ vP1602_R__WJR_0 & vP1602_R__WJS_1))).
fof(ax,axiom, vP1602_LHWMR_1 <=> vP1602_NWR_1).
fof(ax,axiom, vP1602_RHWMR_1 <=> vP1602_RWR_1).
fof(ax,axiom, vP1604N__CALL_P_1 <=> vP1604N_CALL_1).
fof(ax,axiom, vP1604R__CALL_P_1 <=> vP1604R_CALL_1).
fof(ax,axiom, vP1604__AUTOR_JS_1 <=> ((vP1604_RL_0 & (~ vP1604R__CALL_P_1 & (vP1604_NLZ_1 & (~ vP1604_KR_1 & ~ vP1604_KN_1)))) | (~ vP1604_NL_0 & (~ vP1604_RL_0 & (~ vP1604R__CALL_P_1 & (vP1604_NLZ_1 & (~ vP1604_KR_1 & ~ vP1604_KN_1))))))).
fof(ax,axiom, vP1604_AUTOR_1 <=> (vP1604__AUTOR_JR_0 & vP1604__AUTOR_JS_1)).
fof(ax,axiom, vP1604__AUTOR_K_1 <=> (~ vP1604_NWK_0 & (~ vP1604R__CALL_P_1 & (vP1604_AUTOR_1 | vP1604__AUTOR_K_0)))).
fof(ax,axiom, vP1604__AUTOR_ACK_1 <=> ((vP1604__AUTOR_XJR_0 & (vIL822_Q_AUTOR_ACK_0 & vP1604__AUTOR_K_1)) | (vP1604__AUTOR_ACK_0 & vP1604__AUTOR_K_1))).
fof(ax,axiom, vP1604__AUTOR_XJS_1 <=> (~ vP1604__AUTOR_ACK_1 & vP1604__AUTOR_K_1)).
fof(ax,axiom, vP1604_NL_1 <=> (vP1604_NLZ_1 & ((vP1604_N_1 | (vP1604N__CALL_P_1 | vP1604_AUTOR_1)) | (vP1604_NL_0 & ~ vP1604R__CALL_P_1)))).
fof(ax,axiom, vP1604_RL_1 <=> (vP1604_RLZ_1 & ((vP1604_R_1 | vP1604R__CALL_P_1) | (vP1604_RL_0 & (~ vP1604_AUTOR_1 & ~ vP1604N__CALL_P_1))))).
fof(ax,axiom, vP1604_LHL_1 <=> vP1604_RL_1).
fof(ax,axiom, vP1604_RHL_1 <=> vP1604_NL_1).
fof(ax,axiom, vP1604_DUM_1 <=> (vP1604_DUM_0 & (vP1604_RHL_1 & vP1604_LHL_1))).
fof(ax,axiom, vP1604_LHK_1 <=> (~ vP1604_RHK_0 & vP1604_LHK_M__0)).
fof(ax,axiom, vP1604_RHK_1 <=> (~ vP1604_LHK_1 & vP1604_RHK_M__0)).
fof(ax,axiom, vP1604_NWC_1 <=> (vP1604_RHK_1 & vP1604_NL_1)).
fof(ax,axiom, vP1604_RWC_1 <=> (vP1604_LHK_1 & vP1604_RL_1)).
fof(ax,axiom, vP1604_NWK_1 <=> (vP1604_WMC_0 & vP1604_NWC_1)).
fof(ax,axiom, vP1604_RWK_1 <=> (vP1604_WMC_0 & vP1604_RWC_1)).
fof(ax,axiom, vP1604_NKL_1 <=> (vP1604_NWK_1 & ~ vP1604_RWZ_1)).
fof(ax,axiom, vP1604_RKL_1 <=> (vP1604_RWK_1 & ~ vP1604_NWZ_1)).
fof(ax,axiom, vP1604_N__WJS_1 <=> (vP1604_NL_1 & ~ vP1604_NWC_1)).
fof(ax,axiom, vP1604_R__WJS_1 <=> (vP1604_RL_1 & ~ vP1604_RWC_1)).
fof(ax,axiom, vP1604_NWR_1 <=> (vP1604_NL_1 & (~ vP1604_N__WJR_0 & vP1604_N__WJS_1))).
fof(ax,axiom, vP1604_RWR_1 <=> (vP1604_RL_1 & (~ vP1604_R__WJR_0 & vP1604_R__WJS_1))).
fof(ax,axiom, vP1604_LHWMR_1 <=> vP1604_RWR_1).
fof(ax,axiom, vP1604_RHWMR_1 <=> vP1604_NWR_1).
fof(ax,axiom, vP1606N__CALL_P_1 <=> vP1606N_CALL_1).
fof(ax,axiom, vP1606R__CALL_P_1 <=> vP1606R_CALL_1).
fof(ax,axiom, vP1606__AUTOR_JS_1 <=> ((vP1606_RL_0 & (~ vP1606R__CALL_P_1 & (vP1606_NLZ_1 & (~ vP1606_KR_1 & ~ vP1606_KN_1)))) | (~ vP1606_NL_0 & (~ vP1606_RL_0 & (~ vP1606R__CALL_P_1 & (vP1606_NLZ_1 & (~ vP1606_KR_1 & ~ vP1606_KN_1))))))).
fof(ax,axiom, vP1606_AUTOR_1 <=> (vP1606__AUTOR_JR_0 & vP1606__AUTOR_JS_1)).
fof(ax,axiom, vP1606__AUTOR_K_1 <=> (~ vP1606_NWK_0 & (~ vP1606R__CALL_P_1 & (vP1606_AUTOR_1 | vP1606__AUTOR_K_0)))).
fof(ax,axiom, vP1606__AUTOR_ACK_1 <=> ((vP1606__AUTOR_XJR_0 & (vIL822_Q_AUTOR_ACK_0 & vP1606__AUTOR_K_1)) | (vP1606__AUTOR_ACK_0 & vP1606__AUTOR_K_1))).
fof(ax,axiom, vP1606__AUTOR_XJS_1 <=> (~ vP1606__AUTOR_ACK_1 & vP1606__AUTOR_K_1)).
fof(ax,axiom, vP1606_NL_1 <=> (vP1606_NLZ_1 & ((vP1606_N_1 | (vP1606N__CALL_P_1 | vP1606_AUTOR_1)) | (vP1606_NL_0 & ~ vP1606R__CALL_P_1)))).
fof(ax,axiom, vP1606_RL_1 <=> (vP1606_RLZ_1 & ((vP1606_R_1 | vP1606R__CALL_P_1) | (vP1606_RL_0 & (~ vP1606_AUTOR_1 & ~ vP1606N__CALL_P_1))))).
fof(ax,axiom, vP1606_LHL_1 <=> vP1606_RL_1).
fof(ax,axiom, vP1606_RHL_1 <=> vP1606_NL_1).
fof(ax,axiom, vP1606_DUM_1 <=> (vP1606_DUM_0 & (vP1606_RHL_1 & vP1606_LHL_1))).
fof(ax,axiom, vP1606_LHK_1 <=> (~ vP1606_RHK_0 & vP1606_LHK_M__0)).
fof(ax,axiom, vP1606_RHK_1 <=> (~ vP1606_LHK_1 & vP1606_RHK_M__0)).
fof(ax,axiom, vP1606_NWC_1 <=> (vP1606_RHK_1 & vP1606_NL_1)).
fof(ax,axiom, vP1606_RWC_1 <=> (vP1606_LHK_1 & vP1606_RL_1)).
fof(ax,axiom, vP1606_NWK_1 <=> (vP1606_WMC_0 & vP1606_NWC_1)).
fof(ax,axiom, vP1606_RWK_1 <=> (vP1606_WMC_0 & vP1606_RWC_1)).
fof(ax,axiom, vP1606_NKL_1 <=> (vP1606_NWK_1 & ~ vP1606_RWZ_1)).
fof(ax,axiom, vP1606_RKL_1 <=> (vP1606_RWK_1 & ~ vP1606_NWZ_1)).
fof(ax,axiom, vP1606_N__WJS_1 <=> (vP1606_NL_1 & ~ vP1606_NWC_1)).
fof(ax,axiom, vP1606_R__WJS_1 <=> (vP1606_RL_1 & ~ vP1606_RWC_1)).
fof(ax,axiom, vP1606_NWR_1 <=> (vP1606_NL_1 & (~ vP1606_N__WJR_0 & vP1606_N__WJS_1))).
fof(ax,axiom, vP1606_RWR_1 <=> (vP1606_RL_1 & (~ vP1606_R__WJR_0 & vP1606_R__WJS_1))).
fof(ax,axiom, vP1606_LHWMR_1 <=> vP1606_RWR_1).
fof(ax,axiom, vP1606_RHWMR_1 <=> vP1606_NWR_1).
fof(ax,axiom, vP1608N__CALL_P_1 <=> vP1608N_CALL_1).
fof(ax,axiom, vP1608R__CALL_P_1 <=> vP1608R_CALL_1).
fof(ax,axiom, vP1608__AUTOR_JS_1 <=> ((vP1608_RL_0 & (~ vP1608R__CALL_P_1 & (vP1608_NLZ_1 & (~ vP1608_KR_1 & ~ vP1608_KN_1)))) | (~ vP1608_NL_0 & (~ vP1608_RL_0 & (~ vP1608R__CALL_P_1 & (vP1608_NLZ_1 & (~ vP1608_KR_1 & ~ vP1608_KN_1))))))).
fof(ax,axiom, vP1608_AUTOR_1 <=> (vP1608__AUTOR_JR_0 & vP1608__AUTOR_JS_1)).
fof(ax,axiom, vP1608__AUTOR_K_1 <=> (~ vP1608_NWK_0 & (~ vP1608R__CALL_P_1 & (vP1608_AUTOR_1 | vP1608__AUTOR_K_0)))).
fof(ax,axiom, vP1608__AUTOR_ACK_1 <=> ((vP1608__AUTOR_XJR_0 & (vIL822_Q_AUTOR_ACK_0 & vP1608__AUTOR_K_1)) | (vP1608__AUTOR_ACK_0 & vP1608__AUTOR_K_1))).
fof(ax,axiom, vP1608__AUTOR_XJS_1 <=> (~ vP1608__AUTOR_ACK_1 & vP1608__AUTOR_K_1)).
fof(ax,axiom, vP1608_NL_1 <=> (vP1608_NLZ_1 & ((vP1608_N_1 | (vP1608N__CALL_P_1 | vP1608_AUTOR_1)) | (vP1608_NL_0 & ~ vP1608R__CALL_P_1)))).
fof(ax,axiom, vP1608_RL_1 <=> (vP1608_RLZ_1 & ((vP1608_R_1 | vP1608R__CALL_P_1) | (vP1608_RL_0 & (~ vP1608_AUTOR_1 & ~ vP1608N__CALL_P_1))))).
fof(ax,axiom, vP1608_LHL_1 <=> vP1608_RL_1).
fof(ax,axiom, vP1608_RHL_1 <=> vP1608_NL_1).
fof(ax,axiom, vP1608_DUM_1 <=> (vP1608_DUM_0 & (vP1608_RHL_1 & vP1608_LHL_1))).
fof(ax,axiom, vP1608_LHK_1 <=> (~ vP1608_RHK_0 & vP1608_LHK_M__0)).
fof(ax,axiom, vP1608_RHK_1 <=> (~ vP1608_LHK_1 & vP1608_RHK_M__0)).
fof(ax,axiom, vP1608_NWC_1 <=> (vP1608_RHK_1 & vP1608_NL_1)).
fof(ax,axiom, vP1608_RWC_1 <=> (vP1608_LHK_1 & vP1608_RL_1)).
fof(ax,axiom, vP1608_NWK_1 <=> (vP1608_WMC_0 & vP1608_NWC_1)).
fof(ax,axiom, vP1608_RWK_1 <=> (vP1608_WMC_0 & vP1608_RWC_1)).
fof(ax,axiom, vP1608_NKL_1 <=> (vP1608_NWK_1 & ~ vP1608_RWZ_1)).
fof(ax,axiom, vP1608_RKL_1 <=> (vP1608_RWK_1 & ~ vP1608_NWZ_1)).
fof(ax,axiom, vP1608_N__WJS_1 <=> (vP1608_NL_1 & ~ vP1608_NWC_1)).
fof(ax,axiom, vP1608_R__WJS_1 <=> (vP1608_RL_1 & ~ vP1608_RWC_1)).
fof(ax,axiom, vP1608_NWR_1 <=> (vP1608_NL_1 & (~ vP1608_N__WJR_0 & vP1608_N__WJS_1))).
fof(ax,axiom, vP1608_RWR_1 <=> (vP1608_RL_1 & (~ vP1608_R__WJR_0 & vP1608_R__WJS_1))).
fof(ax,axiom, vP1608_LHWMR_1 <=> vP1608_RWR_1).
fof(ax,axiom, vP1608_RHWMR_1 <=> vP1608_NWR_1).
fof(ax,axiom, vP1620N__CALL_P_1 <=> vP1620N_CALL_1).
fof(ax,axiom, vP1620R__CALL_P_1 <=> vP1620R_CALL_1).
fof(ax,axiom, vP1620__AUTOR_JS_1 <=> ((vP1620_RL_0 & (~ vP1620R__CALL_P_1 & (vP1620_NLZ_1 & (~ vP1620_KR_1 & ~ vP1620_KN_1)))) | (~ vP1620_NL_0 & (~ vP1620_RL_0 & (~ vP1620R__CALL_P_1 & (vP1620_NLZ_1 & (~ vP1620_KR_1 & ~ vP1620_KN_1))))))).
fof(ax,axiom, vP1620_AUTOR_1 <=> (vP1620__AUTOR_JR_0 & vP1620__AUTOR_JS_1)).
fof(ax,axiom, vP1620__AUTOR_K_1 <=> (~ vP1620_NWK_0 & (~ vP1620R__CALL_P_1 & (vP1620_AUTOR_1 | vP1620__AUTOR_K_0)))).
fof(ax,axiom, vP1620__AUTOR_ACK_1 <=> ((vP1620__AUTOR_XJR_0 & (vIL822_Q_AUTOR_ACK_0 & vP1620__AUTOR_K_1)) | (vP1620__AUTOR_ACK_0 & vP1620__AUTOR_K_1))).
fof(ax,axiom, vP1620__AUTOR_XJS_1 <=> (~ vP1620__AUTOR_ACK_1 & vP1620__AUTOR_K_1)).
fof(ax,axiom, vP1620_NL_1 <=> (vP1620_NLZ_1 & ((vP1620_N_1 | (vP1620N__CALL_P_1 | vP1620_AUTOR_1)) | (vP1620_NL_0 & ~ vP1620R__CALL_P_1)))).
fof(ax,axiom, vP1620_RL_1 <=> (vP1620_RLZ_1 & ((vP1620_R_1 | vP1620R__CALL_P_1) | (vP1620_RL_0 & (~ vP1620_AUTOR_1 & ~ vP1620N__CALL_P_1))))).
fof(ax,axiom, vP1620_LHL_1 <=> vP1620_RL_1).
fof(ax,axiom, vP1620_RHL_1 <=> vP1620_NL_1).
fof(ax,axiom, vP1620_DUM_1 <=> (vP1620_DUM_0 & (vP1620_RHL_1 & vP1620_LHL_1))).
fof(ax,axiom, vP1620_LHK_1 <=> (~ vP1620_RHK_0 & vP1620_LHK_M__0)).
fof(ax,axiom, vP1620_RHK_1 <=> (~ vP1620_LHK_1 & vP1620_RHK_M__0)).
fof(ax,axiom, vP1620_NWC_1 <=> (vP1620_RHK_1 & vP1620_NL_1)).
fof(ax,axiom, vP1620_RWC_1 <=> (vP1620_LHK_1 & vP1620_RL_1)).
fof(ax,axiom, vP1620_NWK_1 <=> (vP1620_WMC_0 & vP1620_NWC_1)).
fof(ax,axiom, vP1620_RWK_1 <=> (vP1620_WMC_0 & vP1620_RWC_1)).
fof(ax,axiom, vP1620_NKL_1 <=> (vP1620_NWK_1 & ~ vP1620_RWZ_1)).
fof(ax,axiom, vP1620_RKL_1 <=> (vP1620_RWK_1 & ~ vP1620_NWZ_1)).
fof(ax,axiom, vP1620_N__WJS_1 <=> (vP1620_NL_1 & ~ vP1620_NWC_1)).
fof(ax,axiom, vP1620_R__WJS_1 <=> (vP1620_RL_1 & ~ vP1620_RWC_1)).
fof(ax,axiom, vP1620_NWR_1 <=> (vP1620_NL_1 & (~ vP1620_N__WJR_0 & vP1620_N__WJS_1))).
fof(ax,axiom, vP1620_RWR_1 <=> (vP1620_RL_1 & (~ vP1620_R__WJR_0 & vP1620_R__WJS_1))).
fof(ax,axiom, vP1620_LHWMR_1 <=> vP1620_RWR_1).