-
Notifications
You must be signed in to change notification settings - Fork 0
/
tlg_formulas_full.pl
861 lines (861 loc) · 44.3 KB
/
tlg_formulas_full.pl
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
% -*- Mode: Prolog -*-
formula(n, 121627).
formula(dr(0,np,n), 76363).
formula(let, 37678).
formula(dl(0,n,n), 30899).
formula(dr(0,dl(0,n,n),n), 28693).
formula(np, 27896).
formula(dr(0,dl(0,n,n),np), 20425).
formula(dl(0,s,txt), 19394).
formula(dr(0,n,n), 11783).
formula(dr(0,dl(0,np,s),np), 9301).
formula(dr(0,dl(0,np,np),np), 8748).
formula(dr(0,dl(1,s,s),np), 8034).
formula(dr(0,np,np), 6296).
formula(dl(1,s,s), 6204).
formula(dr(0,dl(0,np,s),dl(0,np,s_ppart)), 5671).
formula(dr(0,dl(0,np,s),dl(0,np,s)), 5611).
formula(dr(0,dl(0,np,s_inf),np), 5350).
formula(dr(0,dl(1,s,s),n), 4936).
formula(cl_r, 4559).
formula(dr(0,dl(0,n,n),dl(0,n,n)), 4202).
formula(dr(0,dl(0,np,s_inf),dl(0,np,s_inf)), 4079).
formula(dr(0,dl(0,np,s),dl(0,np,s_inf)), 3951).
formula(dr(0,dl(0,s,s),s), 3800).
formula(dr(0,pp_a,np), 3683).
formula(dr(0,dl(0,dl(0,n,n),dl(0,n,n)),dl(0,n,n)), 3677).
formula(dr(0,pp_de,np), 3577).
formula(dr(0,dl(0,n,n),dl(0,np,s)), 3250).
formula(dr(0,s_q,s), 3045).
formula(dr(0,dr(0,s,s),np), 2989).
formula(dr(0,pp,np), 2915).
formula(dr(0,pp_de,n), 2701).
formula(dr(0,dl(0,np,s_ppart),np), 2586).
formula(dr(0,s,s), 2559).
formula(dr(0,pp_a,n), 2305).
formula(dr(0,dl(0,np,np),n), 2216).
formula(dr(0,dl(0,dl(0,np,s),dl(0,np,s)),dl(0,np,s)), 2204).
formula(dr(0,pp_par,np), 2176).
formula(dr(0,dl(0,np,s),dl(0,n,n)), 2008).
formula(dr(0,dr(0,s,s),n), 1898).
formula(dr(0,dl(0,n,n),dl(0,np,s_inf)), 1610).
formula(dr(0,dl(0,np,s),dr(0,dl(0,np,s),dia(1,box(1,np)))), 1577).
formula(dr(0,dl(0,np,s),dl(0,np,s_pass)), 1570).
formula(dl(0,np,s), 1551).
formula(dl(0,np,s_pass), 1393).
formula(dr(0,dl(1,s,s),dl(1,s,s)), 1294).
formula(dr(0,dl(0,np,s),pp), 1280).
formula(dl(0,np,s_inf), 1229).
formula(dr(0,dl(0,np,s),dr(0,dl(0,np,s),dia(1,box(1,pp_a)))), 1078).
formula(dr(0,dl(1,s,s),dl(0,np,s_inf)), 1045).
formula(dr(0,dl(0,n,n),pp), 1045).
formula(dl(0,cl_r,dl(0,np,s)), 1004).
formula(dr(0,dl(0,n,n),pp_par), 977).
formula(dr(0,dl(0,n,n),pp_de), 922).
formula(dr(0,dl(0,n,n),s), 920).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),np), 895).
formula(dr(0,dl(0,n,n),pp_a), 890).
formula(dr(0,pp,n), 875).
formula(dr(0,dl(0,n,n),dr(0,s,dia(1,box(1,np)))), 846).
formula(dr(0,np,pp_de), 839).
formula(dr(0,dl(0,pp,pp),pp), 830).
formula(dr(0,dl(0,np,s),s_q), 773).
formula(dr(0,dl(0,np,s_ppart),dl(0,np,s_pass)), 718).
formula(dr(0,dl(0,np,s_ppres),np), 706).
formula(dr(0,dl(0,np,np),dl(0,n,n)), 688).
formula(dl(0,np,txt), 687).
formula(dr(0,dl(0,np,s),pp_a), 672).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),dl(0,cl_r,dl(0,np,s_ppart))), 664).
formula(dr(0,dl(0,np,s_ppart),dl(0,np,s_inf)), 661).
formula(dr(0,dl(0,np,s_pass),pp_par), 625).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),n), 604).
formula(dr(0,dl(0,np,np),dl(0,np,s)), 593).
formula(dl(0,np,np), 573).
formula(dr(0,dr(0,s,s),s), 570).
formula(dl(0,np,s_ppart), 569).
formula(dr(0,dr(0,dl(0,np,s),pp_a),np), 562).
formula(dr(0,dl(0,np,s),pp_de), 558).
formula(dr(0,dl(1,s,s),s), 532).
formula(dr(0,dl(1,s,s),s_q), 518).
formula(dr(0,s,np), 472).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),pp), 468).
formula(dr(0,n,pp_de), 467).
formula(cl_y, 463).
formula(dr(0,dl(0,dl(0,np,s),dl(0,np,s)),dl(0,np,s_ppres)), 426).
formula(dr(0,s_q,np), 417).
formula(dr(0,dl(0,dl(1,s,s),dl(1,s,s)),dl(1,s,s)), 409).
formula(dr(0,dl(0,np,s_inf),pp), 398).
formula(dl(0,cl_r,dl(0,np,s_inf)), 395).
formula(dr(0,dl(0,np,s_inf),pp_a), 393).
formula(dr(0,dr(0,dl(0,n,n),dl(0,np,s)),np), 385).
formula(dr(0,dl(0,np,s_inf),dl(0,np,s_pass)), 383).
formula(dr(0,dl(0,dl(0,np,s),np),np), 358).
formula(dr(0,dr(0,n,n),dr(0,n,n)), 356).
formula(dr(0,dl(0,np,s_inf),pp_de), 346).
formula(dr(0,pp,pp), 343).
formula(dr(0,dl(0,s,s),np), 343).
formula(dr(0,dl(0,np,s_pass),pp_a), 334).
formula(dl(0,n,txt), 332).
formula(dr(0,dr(0,s,s),dr(0,s,s)), 327).
formula(dr(0,dr(0,dl(0,n,n),s_q),dl(0,n,n)), 326).
formula(dr(0,dr(0,dl(0,np,s_inf),pp_a),np), 318).
formula(dr(0,dl(0,np,s_ppart),pp), 312).
formula(dr(0,dr(0,s,np),np), 311).
formula(dl(0,cl_r,dl(0,np,s_ppart)), 311).
formula(dr(0,dl(0,dl(0,np,s),dl(0,np,s)),dl(0,np,s_inf)), 304).
formula(dr(0,dl(1,s,s),pp_de), 303).
formula(dr(0,dl(0,np,s_pass),pp), 290).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),pp_a), 277).
formula(dr(0,dl(0,np,s_inf),dl(0,np,s_ppart)), 276).
formula(dr(0,dr(0,s,s),dl(0,np,s_inf)), 274).
formula(dr(0,dl(0,np,s_ppart),pp_de), 261).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),pp_de), 259).
formula(dr(0,dl(0,cl_y,dl(0,np,s)),np), 253).
formula(dr(0,dl(0,np,np),dr(0,s,dia(1,box(1,np)))), 246).
formula(dr(0,dl(0,np,s_inf),s_q), 242).
formula(dr(0,dl(0,np,s_ppart),s_q), 240).
formula(dr(0,dl(0,dr(0,np,n),dr(0,np,n)),dr(0,np,n)), 231).
formula(dr(0,dl(0,np,s_pass),pp_de), 225).
formula(dr(0,dr(0,np,np),n), 224).
formula(dr(0,dl(1,s,s),pp), 223).
formula(dr(0,dl(0,np,s_ppart),pp_a), 217).
formula(dr(0,dl(0,dr(0,pp,np),dl(0,n,n)),s), 210).
formula(dl(1,dl(0,n,n),dl(0,n,n)), 207).
formula(dr(0,dr(0,dl(0,n,n),dl(0,n,n)),n), 201).
formula(dr(0,s_whq,s), 199).
formula(dr(0,dr(0,dl(0,np,s_ppart),pp_a),np), 197).
formula(dr(0,dl(0,np,s),s), 197).
formula(dl(0,dr(0,s,s),txt), 195).
formula(dr(0,dr(0,s,np),dl(0,np,s_ppart)), 193).
formula(dr(0,dl(0,np,np),s), 189).
formula(dr(0,dl(0,np,s_ppart),dl(0,n,n)), 182).
formula(dr(0,dl(0,np,s),dr(0,dl(0,np,s),dia(1,box(1,pp_de)))), 177).
formula(dr(0,dr(0,dl(0,np,s),pp_de),np), 176).
formula(dr(0,s_q,pp), 171).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),dl(0,np,s_inf)), 167).
formula(dl(1,s,dl(0,np,s_ppart)), 167).
formula(dr(0,dl(0,dr(0,n,n),dr(0,n,n)),dr(0,n,n)), 165).
formula(dr(0,dr(0,dl(0,np,s_inf),pp),np), 162).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),dl(0,cl_r,dl(0,np,s))), 162).
formula(dr(0,dr(0,s,s),pp_a), 157).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s_inf)),np), 157).
formula(dr(0,np,dl(0,n,n)), 156).
formula(dr(0,dr(0,s,s),s_q), 150).
formula(dr(0,dl(0,np,s_inf),dl(0,n,n)), 149).
formula(dr(0,n,pp_a), 144).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),pp_a), 143).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),pp), 141).
formula(dr(0,dl(0,n,s),s), 140).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s_inf)),pp_a), 126).
formula(dr(0,dr(0,dl(1,s,s),dl(1,s,s)),n), 120).
formula(dr(0,dl(0,np,s_pass),dl(0,np,s_inf)), 119).
formula(dr(0,dr(0,dl(0,np,s),np),pp_a), 116).
formula(dr(0,dl(1,s,s),pp_a), 116).
formula(dr(0,dl(0,n,n),s_q), 116).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),dl(0,n,n)), 113).
formula(dr(0,dl(0,dr(0,s,s),dr(0,s,s)),dr(0,s,s)), 108).
formula(s, 103).
formula(dr(0,dr(0,dl(0,np,s),pp),np), 102).
formula(dr(0,dr(0,dl(0,np,s_inf),pp_de),np), 101).
formula(dr(0,dr(0,dl(0,np,s_ppart),dl(0,np,s_inf)),np), 100).
formula(dr(0,dr(0,s,s),pp_de), 99).
formula(dr(0,dl(0,pp_de,pp_a),np), 98).
formula(dr(0,dl(0,np,s_ppres),dl(0,np,s_inf)), 98).
formula(dr(0,dl(0,n,n),dr(0,s,dia(1,box(1,pp_de)))), 98).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),np), 96).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),dr(0,dl(0,cl_r,dl(0,np,s)),dia(1,box(1,pp_de)))), 95).
formula(dr(0,dr(0,dl(0,np,s_inf),np),pp), 94).
formula(dr(0,s,dr(0,s,dia(1,box(1,np)))), 93).
formula(dr(0,dr(0,dl(0,np,s),np),pp), 93).
formula(dl(0,np,s_ppres), 92).
formula(dr(0,dr(0,dl(0,np,s_inf),np),dl(0,np,s_inf)), 91).
formula(dr(0,dr(0,np,np),np), 89).
formula(dr(0,dr(0,s,dl(0,np,s_inf)),np), 88).
formula(dr(0,dr(0,dl(0,np,s_inf),dl(0,np,s_inf)),np), 88).
formula(dr(0,dr(0,dl(0,np,s),s_q),dl(0,n,n)), 87).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),pp_de), 86).
formula(dr(0,dl(0,np,s_ppres),s_q), 85).
formula(dr(0,dl(0,np,np),dl(0,np,s_inf)), 85).
formula(dr(0,dr(0,dl(0,np,s),s_q),pp), 84).
formula(dr(0,dl(0,n,n),dr(0,s,dia(1,box(1,pp_a)))), 84).
formula(dr(0,dr(0,n,s_q),n), 83).
formula(dr(0,dl(0,dl(0,n,n),np),np), 82).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppart)),pp), 81).
formula(dr(0,np,s_q), 79).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppart)),pp_a), 77).
formula(dr(0,dl(0,np,s_ppres),pp), 76).
formula(dr(0,dl(0,cl_r,s),np), 76).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s_inf)),dl(0,n,n)), 74).
formula(dr(0,dl(0,np,s_ppres),dl(0,np,s_ppart)), 74).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),dr(0,dl(0,cl_r,dl(0,np,s)),dia(1,box(1,pp_a)))), 74).
formula(dr(0,dr(0,dr(0,s,dl(0,np,s)),np),dl(0,np,s_inf)), 73).
formula(dr(0,dr(0,dr(0,s,s),dr(0,s,s)),n), 72).
formula(dr(0,pp_a,pp_de), 71).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),np), 71).
formula(dr(0,dr(0,dl(0,np,s_inf),np),pp_a), 70).
formula(dr(0,s_q,dl(0,n,n)), 69).
formula(dr(0,dl(0,dr(0,pp,np),dl(0,n,n)),dr(0,s,dia(1,box(1,pp)))), 69).
formula(dr(0,dr(0,dl(0,np,s_ppres),pp_a),np), 67).
formula(dr(0,dl(0,np,s_ppres),pp_de), 67).
formula(dr(0,dr(0,dl(0,np,s_ppart),pp_de),np), 63).
formula(dr(0,dr(0,dl(0,n,n),pp_de),dl(0,n,n)), 63).
formula(dr(0,s_whq,dr(0,s,dia(1,box(1,np)))), 62).
formula(dr(0,dl(0,np,s_pass),dl(0,n,n)), 60).
formula(dr(0,dr(0,s,dl(0,np,s_ppart)),np), 59).
formula(dr(0,dr(0,dr(0,s,dl(0,np,s)),np),dl(0,np,s_ppres)), 59).
formula(dr(0,dl(0,pp_de,dl(0,n,n)),dl(0,n,n)), 59).
formula(dr(0,dl(0,np,np),s_q), 59).
formula(dr(0,dl(0,dr(0,dl(0,np,s),np),dr(0,dl(0,np,s),np)),dr(0,dl(0,np,s),np)), 59).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppart)),pp_de), 59).
formula(dl(0,dl(0,np,s),txt), 59).
formula(dr(0,dr(0,dl(1,s,s),s_q),dl(1,s,s)), 58).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppres)),pp_a), 58).
formula(dr(0,dr(0,s,s),pp), 57).
formula(dr(0,dl(0,np,s_ppres),pp_a), 56).
formula(dr(0,dl(0,np,s),s_whq), 56).
formula(dr(0,dl(0,cl_y,dl(0,np,dl(1,s,s))),np), 56).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppres)),pp_de), 56).
formula(dr(0,dl(0,s,s),n), 55).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppart)),dl(0,np,s_inf)), 55).
formula(dr(0,dr(0,s,s),dl(0,np,s_ppres)), 54).
formula(dl(0,np,dl(1,s,s)), 54).
formula(dr(0,dr(0,s,np),dl(0,np,s_inf)), 53).
formula(dr(0,dr(0,dl(0,np,s_ppart),pp),np), 52).
formula(dr(0,dl(0,s,s),dl(0,s,s)), 52).
formula(dr(0,dr(0,s,dl(0,n,n)),np), 50).
formula(dr(0,dr(0,dl(0,np,s),np),dl(0,np,s_inf)), 50).
formula(dr(0,s_whq,dl(0,np,s_inf)), 49).
formula(dr(0,dr(0,s,np),dl(0,np,s_pass)), 49).
formula(dr(0,dr(0,dl(0,n,n),dl(0,n,n)),np), 49).
formula(dr(0,s_q,dl(0,np,s)), 48).
formula(dr(0,dr(0,dl(0,np,s),dl(0,n,n)),np), 48).
formula(dr(0,dl(0,np,s_inf),s_whq), 48).
formula(dr(0,dr(0,dl(0,np,s_ppart),dl(0,np,s_inf)),pp_a), 46).
formula(dr(0,dr(0,dl(0,np,s),np),dl(0,n,n)), 46).
formula(dr(0,s,s_q), 44).
formula(dr(0,dr(0,dl(0,np,s_inf),dl(0,np,s_inf)),pp_a), 44).
formula(dr(0,dr(0,s,pp),np), 43).
formula(dr(0,dl(0,dl(0,np,s),dl(0,np,s)),dl(0,dl(0,np,s),dl(0,np,s))), 43).
formula(dr(0,dl(0,dl(0,np,np),dl(0,np,np)),dl(0,n,n)), 43).
formula(dr(0,dr(0,np,np),dr(0,np,np)), 42).
formula(dr(0,dl(0,np,s),dr(0,dl(0,np,s),np)), 42).
formula(dr(0,dl(0,np,np),pp), 42).
formula(dr(0,n,s_q), 41).
formula(dr(0,dr(0,dl(0,np,s),s_q),pp_a), 41).
formula(dr(0,dl(0,np,s_ppres),dl(0,np,s_pass)), 39).
formula(dl(0,dl(0,n,n),txt), 39).
formula(dr(0,dr(0,dl(0,np,s_ppart),np),dl(0,np,s_inf)), 36).
formula(dl(0,cl_r,dl(0,np,s_ppres)), 36).
formula(dr(0,dl(1,s,s),dl(0,np,s)), 35).
formula(dr(0,dl(0,np,s_pass),np), 35).
formula(dr(0,pp,pp_de), 34).
formula(dr(0,dr(0,s,pp_de),np), 34).
formula(dr(0,dr(0,dl(0,n,n),dl(0,np,s_inf)),dl(0,n,n)), 34).
formula(dr(0,dl(0,np,s_ppres),dl(0,n,n)), 34).
formula(dr(0,dl(0,dl(0,n,n),s),np), 34).
formula(dr(0,dl(0,cl_y,dl(0,np,dl(1,dl(0,n,n),dl(0,n,n)))),np), 34).
formula(dr(0,dr(0,dl(1,s,s),np),n), 33).
formula(dr(0,dr(0,dl(0,np,s_ppart),np),pp), 33).
formula(dr(0,dr(0,dl(0,np,s),pp_a),dl(0,np,s_inf)), 33).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),dl(0,np,s_inf)), 33).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppart)),dl(0,n,n)), 33).
formula(dr(0,s_q,dl(1,s,s)), 32).
formula(dr(0,dr(0,dl(0,np,s_inf),dl(0,n,n)),np), 32).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),pp_de), 32).
formula(dr(0,dr(0,dl(0,np,s_inf),np),pp_de), 31).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),pp_par), 31).
formula(dr(0,dr(0,pp,pp),n), 30).
formula(dr(0,dr(0,dl(0,np,s_ppart),np),pp_a), 30).
formula(dr(0,dl(0,dr(0,pp,np),s_whq),dr(0,s,dia(1,box(1,pp)))), 30).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),dl(0,np,s_inf)), 30).
formula(dr(0,dr(0,dl(0,np,s),np),pp_de), 29).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s)),n), 27).
formula(dr(0,dl(1,s,s),dl(0,n,n)), 27).
formula(dr(0,dl(0,dr(0,s,dia(1,box(1,dr(0,dl(0,np,s),pp)))),dr(0,s,box(1,dia(1,dr(0,dl(0,np,s),pp))))),dr(0,s,dia(1,box(1,dr(0,dl(0,np,s),pp))))), 27).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppart)),np), 27).
formula(dr(0,s,dr(0,s,dia(1,box(1,pp_a)))), 26).
formula(dr(0,dl(0,s,s),dl(0,n,n)), 26).
formula(dr(0,dl(0,pp_de,dl(1,s,s)),dl(1,s,s)), 26).
formula(dr(0,dl(0,np,dl(0,np,np)),np), 26).
formula(dr(0,dl(0,n,dl(1,s,s)),n), 26).
formula(dr(0,dl(0,dr(0,pp,np),dl(0,n,n)),np), 26).
formula(dr(0,dl(0,cl_y,dl(0,np,dr(0,s,s))),np), 26).
formula(dr(0,pp_par,n), 25).
formula(dr(0,dr(0,s,s_q),np), 25).
formula(dr(0,s,dl(0,np,s_inf)), 24).
formula(dr(0,n,dl(0,np,s_inf)), 24).
formula(dr(0,dr(0,dl(0,np,s),pp_a),dl(0,n,n)), 24).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),s_q), 24).
formula(dr(0,dl(0,pp_de,dl(1,s,s)),np), 24).
formula(dr(0,dl(0,dr(0,s,dia(1,box(1,dr(0,dl(0,np,s),np)))),dr(0,s,box(1,dia(1,dr(0,dl(0,np,s),np))))),dr(0,s,dia(1,box(1,dr(0,dl(0,np,s),np))))), 24).
formula(dr(0,s_whq,dl(0,np,s)), 23).
formula(dr(0,dr(0,dl(0,np,s),s_q),np), 23).
formula(dr(0,dl(0,dl(0,np,s_inf),s),np), 23).
formula(dr(0,dl(0,cl_y,dl(0,np,s_ppart)),np), 23).
formula(dr(0,dl(0,cl_y,dl(0,np,s)),dl(0,cl_y,dl(0,np,s_ppart))), 23).
formula(dl(0,cl_r,dl(1,s,dr(0,s,np))), 23).
formula(dr(0,dl(0,cl_y,dl(0,np,s)),dl(0,cl_y,dl(0,np,s))), 22).
formula(dr(0,dr(0,dl(0,np,s_ppres),pp),np), 21).
formula(dr(0,dr(0,dl(0,cl_r,s),pp_a),np), 21).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),s), 21).
formula(dr(0,dl(0,s,s),dl(0,np,s)), 21).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),s_q), 21).
formula(dr(0,dr(0,dl(0,np,s),np),np), 20).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s)),dr(0,dl(0,np,s),dl(0,np,s))), 20).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s)),dl(0,np,s_ppres)), 20).
formula(dr(0,dl(0,dr(0,dl(0,n,n),dl(0,n,n)),dr(0,dl(0,n,n),dl(0,n,n))),dr(0,dl(0,n,n),dl(0,n,n))), 20).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppart)),pp_par), 20).
formula(dr(0,dr(0,np,s_q),np), 19).
formula(dr(0,dr(0,dl(0,np,s),s_q),dl(0,np,s)), 19).
formula(dr(0,dl(0,n,n),dl(0,np,s_ppart)), 19).
formula(dr(0,dl(0,dl(1,dl(0,n,n),dl(0,n,n)),dl(1,dl(0,n,n),dl(0,n,n))),dl(1,dl(0,n,n),dl(0,n,n))), 19).
formula(dr(0,dl(0,dl(0,dl(0,np,s),dl(0,np,s)),dl(0,dl(0,np,s),dl(0,np,s))),dl(0,dl(0,np,s),dl(0,np,s))), 19).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),dl(0,cl_r,dl(0,np,s_ppart))), 19).
formula(dr(0,np,pp), 18).
formula(dr(0,dr(0,dl(1,s,s),dl(1,s,s)),np), 18).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s_inf)),pp), 18).
formula(dr(0,dl(1,s,s),dl(0,np,s_ppres)), 18).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),pp), 18).
formula(dr(0,dl(0,np,dl(1,s,s)),pp_de), 18).
formula(dr(0,dr(0,s,dr(0,s,dia(1,box(1,pp_a)))),np), 17).
formula(dr(0,dr(0,dl(0,np,s_ppres),pp_de),np), 17).
formula(dr(0,dr(0,dl(0,np,s_ppres),dl(0,np,s_inf)),np), 17).
formula(dr(0,dr(0,dl(0,np,s_ppart),dl(0,n,n)),np), 17).
formula(dr(0,dr(0,dl(0,np,s_inf),np),dl(0,n,n)), 17).
formula(dr(0,dr(0,dl(0,dr(0,pp,np),s_whq),s),n), 17).
formula(dr(0,dl(0,np,s),pp_par), 17).
formula(dr(0,dl(0,np,dl(0,dr(0,s,np),s)),dl(0,np,s_ppres)), 17).
formula(dr(0,dl(0,n,n),dl(0,np,s_ppres)), 17).
formula(dr(0,dl(0,dr(0,np,n),dl(0,dr(0,pp_de,np),dr(0,pp_a,n))),dr(0,np,n)), 17).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),dl(0,n,n)), 17).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),dr(0,dl(0,np,s_inf),dia(1,box(1,np)))), 17).
formula(dr(0,dr(0,dl(0,np,s_inf),s_q),pp_a), 16).
formula(dr(0,dl(0,dr(0,pp,np),np),dl(0,np,s_inf)), 16).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),dr(0,dl(0,np,s_inf),dia(1,box(1,np)))), 16).
formula(dr(0,s_q,n), 15).
formula(dr(0,s,dr(0,s,dia(1,box(1,pp_de)))), 15).
formula(dr(0,dr(0,dl(0,np,s_ppres),dl(0,np,s_inf)),pp_a), 15).
formula(dr(0,dr(0,dl(0,np,s_ppart),np),pp_de), 15).
formula(dr(0,dr(0,dl(0,n,n),pp_a),np), 15).
formula(dr(0,dl(0,dr(0,s,dia(1,box(1,dr(0,dl(0,np,s),dl(0,n,n))))),dr(0,s,box(1,dia(1,dr(0,dl(0,np,s),dl(0,n,n)))))),dr(0,s,dia(1,box(1,dr(0,dl(0,np,s),dl(0,n,n)))))), 15).
formula(dr(0,dl(0,dr(0,dl(0,np,s),dia(0,box(0,np))),dr(0,dl(0,np,s),np)),dr(0,dl(0,np,s),dia(0,box(0,np)))), 15).
formula(dr(0,dl(0,dl(0,np,s),s),s), 15).
formula(dl(1,s,dr(0,s,np)), 15).
formula(dr(0,dr(0,pp,pp),np), 14).
formula(dr(0,dr(0,np,s_q),pp_de), 14).
formula(dr(0,dr(0,dl(0,np,s_ppart),s_q),pp_a), 14).
formula(dr(0,dr(0,dl(0,np,s_pass),pp_par),dl(0,n,n)), 14).
formula(dr(0,dr(0,dl(0,n,n),pp_par),pp), 14).
formula(dr(0,dl(1,dl(0,np,s),dl(0,np,s)),dl(0,np,s_inf)), 14).
formula(dr(0,dl(1,dl(0,np,np),dl(0,np,np)),np), 14).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),dl(1,dl(0,n,n),dl(0,n,n))), 14).
formula(dr(0,dl(0,cl_r,dr(0,s,np)),dl(0,cl_r,dl(0,np,s_ppart))), 14).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppart)),dr(0,dl(0,np,s_inf),dia(1,box(1,np)))), 14).
formula(pp, 13).
formula(dr(0,dr(0,dl(0,np,s_ppres),np),pp), 13).
formula(dr(0,dr(0,dl(0,np,s_ppres),np),dl(0,np,s_inf)), 13).
formula(dr(0,dr(0,dl(0,np,s_pass),pp_par),pp_a), 13).
formula(dr(0,dr(0,dl(0,np,s_pass),pp_par),pp), 13).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s)),dl(0,np,s_inf)), 13).
formula(dr(0,dl(0,dl(0,np,s),dl(0,np,s)),np), 13).
formula(dl(0,dl(1,s,s),dl(1,s,s)), 13).
formula(dr(0,dr(0,s,pp_a),np), 12).
formula(dr(0,dl(0,np,s_ppres),pp_par), 12).
formula(dr(0,dl(0,np,s_inf),pp_par), 12).
formula(dr(0,dl(0,np,dl(1,s,s)),np), 12).
formula(dr(0,pp_de,dl(0,n,n)), 11).
formula(dr(0,dr(0,pp,s_q),pp), 11).
formula(dr(0,dr(0,dl(0,n,n),pp_par),pp_a), 11).
formula(dr(0,dl(0,np,np),pp_de), 11).
formula(dr(0,dl(0,np,dl(1,s,s)),s), 11).
formula(dr(0,dl(0,dl(0,np,s_inf),s),dl(0,np,s_inf)), 11).
formula(dr(0,dr(0,dl(0,np,s),pp_par),np), 10).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s)),np), 10).
formula(dr(0,dr(0,dl(0,n,n),pp_par),dl(0,n,n)), 10).
formula(dr(0,dr(0,dl(0,n,n),dl(0,n,n)),dr(0,dl(0,n,n),dl(0,n,n))), 10).
formula(dr(0,dl(1,dl(0,np,np),dl(0,np,np)),n), 10).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),pp_a), 10).
formula(dr(0,dl(0,p(0,np,pp),p(0,np,dia(0,box(0,pp)))),p(0,np,pp)), 10).
formula(dr(0,dl(0,n,n),dr(0,s,dia(1,box(1,pp)))), 10).
formula(dr(0,dl(0,dr(0,s,dia(1,box(1,dr(0,dl(0,np,s),dl(0,np,s))))),dr(0,s,box(1,dia(1,dr(0,dl(0,np,s),dl(0,np,s)))))),dr(0,s,dia(1,box(1,dr(0,dl(0,np,s),dl(0,np,s)))))), 10).
formula(dr(0,dl(0,cl_y,dl(1,s,s)),dl(1,s,s)), 10).
formula(dl(1,dl(0,np,s),dl(0,np,s)), 10).
formula(dr(0,s_whq,dr(0,s,dia(1,box(1,dl(0,n,n))))), 9).
formula(dr(0,s_whq,dr(0,dl(0,np,s),dia(1,box(1,np)))), 9).
formula(dr(0,dr(0,dr(0,s,s),s_q),dr(0,s,s)), 9).
formula(dr(0,dr(0,dl(0,np,s_pass),pp_par),pp_de), 9).
formula(dr(0,dr(0,dl(0,np,s_inf),pp_par),np), 9).
formula(dr(0,dr(0,dl(0,np,s),s_q),dl(1,s,s)), 9).
formula(dr(0,dr(0,dl(0,n,n),pp_a),pp_par), 9).
formula(dr(0,dr(0,dl(0,n,n),dl(0,np,s_inf)),pp_a), 9).
formula(dr(0,dr(0,dl(0,cl_r,s),np),np), 9).
formula(dr(0,dl(0,pp,pp),s_q), 9).
formula(dr(0,dl(0,dr(0,dl(0,np,s),pp),dr(0,dl(0,np,s),pp)),dr(0,dl(0,np,s),pp)), 9).
formula(dr(0,dl(0,dl(0,n,n),s),s), 9).
formula(dr(0,dl(0,cl_y,dl(0,np,np)),np), 9).
formula(dr(0,dl(0,cl_y,dl(0,np,dl(0,n,n))),np), 9).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppres)),pp), 9).
formula(dl(1,s,dl(0,np,s_inf)), 9).
formula(dr(0,dr(0,s,dr(0,s,dia(1,box(1,pp_a)))),n), 8).
formula(dr(0,dr(0,dl(0,np,s_inf),pp_a),dl(0,np,s_inf)), 8).
formula(dr(0,dr(0,dl(0,np,s),s_q),pp_de), 8).
formula(dr(0,dl(1,dl(0,np,s),dl(0,np,s)),dl(0,np,s_ppres)), 8).
formula(dr(0,dl(0,np,s_pass),s_q), 8).
formula(dr(0,dl(0,np,np),pp_par), 8).
formula(dr(0,dl(0,np,dr(0,s,s)),pp_de), 8).
formula(dr(0,dl(0,dl(0,np,s),s),dl(0,dl(0,np,s),s)), 8).
formula(dr(0,dl(0,dl(0,n,n),dr(0,s,s)),dr(0,s,dia(1,box(1,dl(0,n,n))))), 8).
formula(dr(0,dl(0,dl(0,dia(0,box(0,n)),n),dl(0,n,n)),dl(0,dia(0,box(0,n)),n)), 8).
formula(dr(0,s,pp), 7).
formula(dr(0,pp_a,dl(0,n,n)), 7).
formula(dr(0,np,s), 7).
formula(dr(0,np,dl(0,np,s)), 7).
formula(dr(0,dr(0,dl(0,np,s_ppres),np),pp_de), 7).
formula(dr(0,dr(0,dl(0,np,s_ppres),dl(0,n,n)),np), 7).
formula(dr(0,dr(0,dl(0,n,n),np),pp), 7).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),dl(0,np,s_ppres)), 7).
formula(dr(0,dl(0,p(0,dl(1,s,s),np),p(0,dl(1,s,s),dia(0,box(0,np)))),p(0,dl(1,s,s),np)), 7).
formula(dr(0,dl(0,np,np),pp_a), 7).
formula(dr(0,dl(0,dr(0,np,n),dl(0,dr(0,pp_de,np),dr(0,np,n))),dr(0,np,n)), 7).
formula(dr(0,dl(0,dl(0,np,s_inf),s),dl(0,n,n)), 7).
formula(dr(0,dl(0,cl_y,dl(0,np,pp)),np), 7).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppres)),dl(0,np,s_inf)), 7).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),s_whq), 7).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),s_q), 7).
formula(dr(0,dl(0,cl_r,dl(0,n,n)),pp_a), 7).
formula(dl(0,dr(0,s,s),dr(0,s,s)), 7).
formula(dr(0,s_whq,dr(0,s,dia(1,box(1,pp)))), 6).
formula(dr(0,pp_de,pp), 6).
formula(dr(0,dr(0,s,s),dl(0,n,n)), 6).
formula(dr(0,dr(0,s,pp),cl_r), 6).
formula(dr(0,dr(0,s,np),pp), 6).
formula(dr(0,dr(0,pp,pp),dr(0,pp,pp)), 6).
formula(dr(0,dr(0,np,np),dl(0,np,s_inf)), 6).
formula(dr(0,dr(0,dr(0,s,s),np),n), 6).
formula(dr(0,dr(0,dr(0,dl(0,np,s),dl(0,np,s_inf)),pp_a),dl(0,n,n)), 6).
formula(dr(0,dr(0,dl(0,np,s_ppres),np),dl(0,n,n)), 6).
formula(dr(0,dr(0,dl(0,np,s_inf),s_q),pp_de), 6).
formula(dr(0,dr(0,dl(0,n,n),pp_de),np), 6).
formula(dr(0,dl(1,s,dl(0,np,s_ppart)),pp_a), 6).
formula(dr(0,dl(0,pp_de,pp_a),n), 6).
formula(dr(0,dl(0,pp_de,dl(1,s,s)),n), 6).
formula(dr(0,dl(0,pp,dl(0,n,n)),s), 6).
formula(dr(0,dl(0,np,s_ppart),s_whq), 6).
formula(dr(0,dl(0,np,np),dr(0,s,dia(1,box(1,pp_de)))), 6).
formula(dr(0,dl(0,dr(0,dl(0,np,s),dl(0,np,s)),dr(0,dl(0,np,s),dl(0,np,s))),dr(0,dl(0,np,s),dl(0,np,s))), 6).
formula(dr(0,dl(0,dr(0,dl(0,n,n),dia(0,box(0,n))),dr(0,dl(0,n,n),n)),dr(0,dl(0,n,n),dia(0,box(0,n)))), 6).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppart)),dr(0,dl(0,np,s_inf),dia(1,box(1,pp_a)))), 6).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),s_whq), 6).
formula(dr(0,dr(0,s_whq,dl(0,np,s)),pp_de), 5).
formula(dr(0,dr(0,dr(0,s,pp_a),np),np), 5).
formula(dr(0,dr(0,dr(0,s,np),pp_a),np), 5).
formula(dr(0,dr(0,dr(0,s,dl(0,np,s_inf)),dl(0,n,n)),np), 5).
formula(dr(0,dr(0,dr(0,dr(0,s,dl(0,np,s)),np),dr(0,dr(0,s,dl(0,np,s)),np)),n), 5).
formula(dr(0,dr(0,dl(0,np,s_pass),dl(0,np,s_inf)),pp_par), 5).
formula(dr(0,dr(0,dl(0,np,s_inf),np),np), 5).
formula(dr(0,dr(0,dl(0,cl_r,s),pp),np), 5).
formula(dr(0,dl(1,dl(0,np,s),dl(0,np,s)),np), 5).
formula(dr(0,dl(0,pp_de,np),np), 5).
formula(dr(0,dl(0,pp_de,dl(0,n,n)),np), 5).
formula(dr(0,dl(0,np,np),dl(0,np,np)), 5).
formula(dr(0,dl(0,np,dl(0,dl(0,n,n),dl(0,n,n))),dl(0,n,n)), 5).
formula(dr(0,dl(0,n,n),dr(0,dl(0,n,n),dia(1,box(1,pp_a)))), 5).
formula(dr(0,dl(0,dr(0,pp,np),s_whq),s), 5).
formula(dr(0,dl(0,dr(0,pp,np),dl(0,np,np)),dr(0,s,dia(1,box(1,pp)))), 5).
formula(dr(0,dl(0,dr(0,pp,dia(0,box(0,n))),dl(0,n,n)),s), 5).
formula(dr(0,dl(0,dr(0,np,dia(0,box(0,n))),dr(0,np,n)),dr(0,np,dia(0,box(0,n)))), 5).
formula(dr(0,dl(0,dr(0,dl(1,s,s),dia(0,box(0,n))),dr(0,dl(1,s,s),n)),dr(0,dl(1,s,s),dia(0,box(0,n)))), 5).
formula(dr(0,dl(0,dr(0,dl(0,n,n),np),dr(0,dl(0,n,n),np)),dr(0,dl(0,n,n),np)), 5).
formula(dr(0,dl(0,dl(0,n,n),dl(0,n,n)),np), 5).
formula(dr(0,dl(0,dl(0,cl_r,dl(0,np,s)),dl(0,cl_r,dl(0,np,s))),dl(0,cl_r,dl(0,np,s))), 5).
formula(dr(0,dl(0,cl_y,dl(0,n,n)),dl(0,n,n)), 5).
formula(dl(0,np,dr(0,s,s)), 5).
formula(s_whq, 4).
formula(dr(0,s_whq,np), 4).
formula(dr(0,dr(0,s,s),dl(0,np,s_ppart)), 4).
formula(dr(0,dr(0,n,n),n), 4).
formula(dr(0,dr(0,dr(0,s,pp_de),np),np), 4).
formula(dr(0,dr(0,dl(1,s,s),pp_a),np), 4).
formula(dr(0,dr(0,dl(0,np,s_ppart),s_q),np), 4).
formula(dr(0,dr(0,dl(0,np,s_pass),pp_a),np), 4).
formula(dr(0,dr(0,dl(0,np,s_inf),s_q),np), 4).
formula(dr(0,dr(0,dl(0,n,n),pp),dl(0,n,n)), 4).
formula(dr(0,dl(0,pp_de,dr(0,s,s)),np), 4).
formula(dr(0,dl(0,pp,s_q),dr(0,s,dia(1,box(1,pp)))), 4).
formula(dr(0,dl(0,np,dl(0,pp,pp)),pp), 4).
formula(dr(0,dl(0,np,dl(0,n,n)),dl(0,n,n)), 4).
formula(dr(0,dl(0,np,dl(0,dl(1,s,s),dl(1,s,s))),dl(1,s,s)), 4).
formula(dr(0,dl(0,np,dl(0,dl(0,np,s),dl(0,np,s))),dl(0,np,s)), 4).
formula(dr(0,dl(0,n,n),dr(0,dl(0,n,n),dia(1,box(1,np)))), 4).
formula(dr(0,dl(0,n,n),dl(0,np,s_pass)), 4).
formula(dr(0,dl(0,dr(0,pp,np),s_whq),n), 4).
formula(dr(0,dl(0,dr(0,pp,np),dl(0,np,np)),s), 4).
formula(dr(0,dl(0,dr(0,dl(0,n,n),n),dr(0,dl(0,n,n),n)),dr(0,dl(0,n,n),n)), 4).
formula(dr(0,dl(0,dl(0,n,n),dl(1,s,s)),dr(0,s,dia(1,box(1,dl(0,n,n))))), 4).
formula(dr(0,dl(0,cl_y,dl(1,s,s)),np), 4).
formula(dr(0,dl(0,cl_r,s),dr(0,dl(0,cl_r,s),dia(1,box(1,pp_a)))), 4).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppres)),dl(0,n,n)), 4).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppart)),s_q), 4).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),pp_par), 4).
formula(pp_a, 3).
formula(dr(0,s,s_whq), 3).
formula(dr(0,s,cl_r), 3).
formula(dr(0,pp_a,dl(0,np,s_inf)), 3).
formula(dr(0,dr(0,s,np),pp_a), 3).
formula(dr(0,dr(0,s,np),dl(0,n,n)), 3).
formula(dr(0,dr(0,s,dr(0,s,dia(1,box(1,pp_de)))),np), 3).
formula(dr(0,dr(0,s,dl(0,np,s_pass)),np), 3).
formula(dr(0,dr(0,dr(0,s,s),dr(0,s,s)),pp_de), 3).
formula(dr(0,dr(0,dl(1,s,s),dl(1,s,s)),dl(0,n,n)), 3).
formula(dr(0,dr(0,dl(1,dl(0,n,n),dl(0,n,n)),dl(1,dl(0,n,n),dl(0,n,n))),n), 3).
formula(dr(0,dr(0,dl(0,np,s_ppart),pp_par),np), 3).
formula(dr(0,dr(0,dl(0,np,s_ppart),np),dl(0,n,n)), 3).
formula(dr(0,dr(0,dl(0,np,s_ppart),dl(0,np,s_inf)),pp), 3).
formula(dr(0,dr(0,dl(0,np,s_pass),pp_a),pp_par), 3).
formula(dr(0,dr(0,dl(0,np,s_pass),dl(0,n,n)),pp_par), 3).
formula(dr(0,dr(0,dl(0,np,s_inf),np),pp_par), 3).
formula(dr(0,dr(0,dl(0,np,s_inf),dl(0,np,s_inf)),dl(0,n,n)), 3).
formula(dr(0,dr(0,dl(0,np,s),s_q),dl(0,np,s_inf)), 3).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s_ppart)),np), 3).
formula(dr(0,dr(0,dl(0,n,n),np),pp_a), 3).
formula(dr(0,dr(0,dl(0,n,n),np),n), 3).
formula(dr(0,dr(0,dl(0,n,n),dl(0,np,s_inf)),np), 3).
formula(dr(0,dr(0,dl(0,n,n),dl(0,n,n)),pp), 3).
formula(dr(0,dr(0,dl(0,dr(0,pp,np),s_whq),dr(0,s,dia(1,box(1,pp)))),n), 3).
formula(dr(0,dr(0,dl(0,dl(0,np,s),dl(0,np,s)),dl(0,dl(0,np,s),dl(0,np,s))),n), 3).
formula(dr(0,dl(1,s,s),dr(0,dl(1,s,s),dia(1,box(1,pp_a)))), 3).
formula(dr(0,dl(1,dl(0,np,s),dl(0,np,s)),dl(1,dl(0,np,s),dl(0,np,s))), 3).
formula(dr(0,dl(0,pp_de,pp),pp), 3).
formula(dr(0,dl(0,p(0,pp,np),p(0,pp,dia(0,box(0,np)))),p(0,pp,np)), 3).
formula(dr(0,dl(0,p(0,np,dl(0,np,s)),p(0,np,dia(0,box(0,dl(0,np,s))))),p(0,np,dl(0,np,s))), 3).
formula(dr(0,dl(0,np,np),dr(0,s,s)), 3).
formula(dr(0,dl(0,np,np),dr(0,s,dia(1,box(1,pp_a)))), 3).
formula(dr(0,dl(0,np,dl(0,n,n)),pp_de), 3).
formula(dr(0,dl(0,dr(0,s,np),dr(0,s,np)),dl(0,np,s_ppres)), 3).
formula(dr(0,dl(0,dr(0,s,dia(0,box(0,np))),dr(0,s,np)),dr(0,s,dia(0,box(0,np)))), 3).
formula(dr(0,dl(0,dr(0,np,np),dr(0,np,np)),dr(0,np,np)), 3).
formula(dr(0,dl(0,dr(0,dr(0,s,dl(0,np,s)),np),dr(0,dr(0,s,dl(0,np,s)),np)),dr(0,dr(0,s,dl(0,np,s)),np)), 3).
formula(dr(0,dl(0,dr(0,dr(0,dr(0,s,s),s_q),dr(0,s,s)),dr(0,dr(0,dr(0,s,s),s_q),dr(0,s,s))),dr(0,dr(0,dr(0,s,s),s_q),dr(0,s,s))), 3).
formula(dr(0,dl(0,dr(0,dr(0,dl(0,n,n),dl(0,n,n)),n),dr(0,dr(0,dl(0,n,n),dl(0,n,n)),n)),dr(0,dr(0,dl(0,n,n),dl(0,n,n)),n)), 3).
formula(dr(0,dl(0,dr(0,dl(0,n,n),pp),dr(0,dl(0,n,n),pp)),dr(0,dl(0,n,n),pp)), 3).
formula(dr(0,dl(0,dl(0,n,n),n),n), 3).
formula(dr(0,dl(0,dl(0,n,n),dl(0,n,n)),dr(0,s,dia(1,box(1,dl(0,n,n))))), 3).
formula(dr(0,dl(0,cl_y,dl(0,np,s_inf)),np), 3).
formula(dr(0,dl(0,cl_y,dl(0,np,s)),pp), 3).
formula(dr(0,dl(0,cl_y,dl(0,np,s)),dl(0,np,s_inf)), 3).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),dr(0,dl(0,cl_r,dl(0,np,s)),dia(1,box(1,np)))), 3).
formula(dl(0,np,dl(1,dl(0,n,n),dl(0,n,n))), 3).
formula(dr(0,s_whq,pp_de), 2).
formula(dr(0,s_whq,n), 2).
formula(dr(0,s,pp_a), 2).
formula(dr(0,s,dl(0,n,n)), 2).
formula(dr(0,pp,s_q), 2).
formula(dr(0,pp,pp_a), 2).
formula(dr(0,dr(0,s_whq,dr(0,s,dia(1,box(1,np)))),pp_de), 2).
formula(dr(0,dr(0,s_whq,dr(0,s,dia(1,box(1,np)))),n), 2).
formula(dr(0,dr(0,s_whq,dl(0,np,s)),n), 2).
formula(dr(0,dr(0,s,s),dl(0,np,s)), 2).
formula(dr(0,dr(0,s,np),s), 2).
formula(dr(0,dr(0,s,dr(0,s,dia(1,box(1,pp_de)))),n), 2).
formula(dr(0,dr(0,s,dl(0,np,s_inf)),pp_a), 2).
formula(dr(0,dr(0,np,np),s), 2).
formula(dr(0,dr(0,n,n),np), 2).
formula(dr(0,dr(0,dr(0,s,s_q),pp),np), 2).
formula(dr(0,dr(0,dr(0,s,s),np),pp), 2).
formula(dr(0,dr(0,dr(0,s,s),dr(0,s,s)),np), 2).
formula(dr(0,dr(0,dr(0,s,np),np),dl(0,np,s_inf)), 2).
formula(dr(0,dr(0,dr(0,dl(0,np,s),dl(0,np,s_inf)),pp_a),np), 2).
formula(dr(0,dr(0,dr(0,dl(0,np,s),dl(0,np,s)),dr(0,dl(0,np,s),dl(0,np,s))),n), 2).
formula(dr(0,dr(0,dl(1,s,s),np),pp), 2).
formula(dr(0,dr(0,dl(1,s,s),dl(1,s,s)),pp_de), 2).
formula(dr(0,dr(0,dl(0,np,s_ppart),s_q),pp_de), 2).
formula(dr(0,dr(0,dl(0,np,s_ppart),pp_a),dl(0,n,n)), 2).
formula(dr(0,dr(0,dl(0,np,s_ppart),dl(0,np,s_inf)),dl(0,n,n)), 2).
formula(dr(0,dr(0,dl(0,np,s_pass),pp_par),np), 2).
formula(dr(0,dr(0,dl(0,np,s_pass),dl(0,np,s_inf)),pp_a), 2).
formula(dr(0,dr(0,dl(0,np,s_inf),s_whq),pp_a), 2).
formula(dr(0,dr(0,dl(0,np,s_inf),s_q),pp), 2).
formula(dr(0,dr(0,dl(0,np,s),s_whq),pp_a), 2).
formula(dr(0,dr(0,dl(0,np,s),s),s), 2).
formula(dr(0,dr(0,dl(0,np,s),pp_de),pp_a), 2).
formula(dr(0,dr(0,dl(0,np,s),pp_a),pp_de), 2).
formula(dr(0,dr(0,dl(0,np,s),pp_a),pp_a), 2).
formula(dr(0,dr(0,dl(0,np,np),s_q),dl(0,n,n)), 2).
formula(dr(0,dr(0,dl(0,n,s),s),n), 2).
formula(dr(0,dr(0,dl(0,n,n),pp_par),np), 2).
formula(dr(0,dr(0,dl(0,n,n),pp),pp_par), 2).
formula(dr(0,dr(0,dl(0,n,n),dl(0,np,s_inf)),pp_par), 2).
formula(dr(0,dr(0,dl(0,n,n),dl(0,np,s)),dr(0,dl(0,n,n),dl(0,np,s))), 2).
formula(dr(0,dr(0,dl(0,n,n),dl(0,n,n)),s), 2).
formula(dr(0,dr(0,dl(0,cl_y,s),np),np), 2).
formula(dr(0,dr(0,dl(0,cl_y,dl(0,np,s)),s_q),np), 2).
formula(dr(0,dr(0,dl(0,cl_y,dl(0,np,s)),dl(0,np,s_inf)),np), 2).
formula(dr(0,dr(0,dl(0,cl_r,s),dl(0,np,s_inf)),np), 2).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s_ppart)),s_q),np), 2).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s_ppart)),pp_a),np), 2).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s_inf)),pp_de),np), 2).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s)),s_q),dl(0,cl_r,dl(0,np,s))), 2).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s)),pp_de),np), 2).
formula(dr(0,dl(1,np,np),np), 2).
formula(dr(0,dl(0,pp_de,dl(0,n,n)),n), 2).
formula(dr(0,dl(0,pp,dl(0,n,n)),np), 2).
formula(dr(0,dl(0,pp,dl(0,n,n)),dr(0,s,dia(1,box(1,pp)))), 2).
formula(dr(0,dl(0,p(0,pp,dl(1,s,s)),p(0,pp,dl(1,s,s))),p(0,pp,dl(1,s,s))), 2).
formula(dr(0,dl(0,p(0,np,dl(0,n,n)),p(0,np,dia(0,box(0,dl(0,n,n))))),p(0,np,dl(0,n,n))), 2).
formula(dr(0,dl(0,p(0,dl(1,s,s),pp),p(0,dl(1,s,s),dia(0,box(0,pp)))),p(0,dl(1,s,s),pp)), 2).
formula(dr(0,dl(0,p(0,dl(0,n,n),pp),p(0,dl(0,n,n),dia(0,box(0,pp)))),p(0,dl(0,n,n),pp)), 2).
formula(dr(0,dl(0,np,s_ppart),pp_par), 2).
formula(dr(0,dl(0,np,dl(1,dl(0,n,n),dl(0,n,n))),np), 2).
formula(dr(0,dl(0,np,dl(0,n,n)),np), 2).
formula(dr(0,dl(0,np,dl(0,dr(0,s,np),s)),dl(0,np,dl(0,dr(0,s,np),s))), 2).
formula(dr(0,dl(0,n,n),dr(0,s_q,dia(1,box(1,pp)))), 2).
formula(dr(0,dl(0,dr(0,s,dia(0,box(0,s_q))),dr(0,s,s_q)),dr(0,s,dia(0,box(0,s_q)))), 2).
formula(dr(0,dl(0,dr(0,s,dia(0,box(0,s))),dr(0,s,s)),dr(0,s,dia(0,box(0,s)))), 2).
formula(dr(0,dl(0,dr(0,s,dia(0,box(0,dl(0,np,s)))),dr(0,s,dl(0,np,s))),dr(0,s,dia(0,box(0,dl(0,np,s))))), 2).
formula(dr(0,dl(0,dr(0,np,pp),dr(0,np,pp)),dr(0,np,pp)), 2).
formula(dr(0,dl(0,dr(0,np,n),dl(0,dr(0,pp_de,np),dr(0,dl(1,s,s),n))),dr(0,np,n)), 2).
formula(dr(0,dl(0,dr(0,n,dia(0,box(0,n))),dr(0,n,n)),dr(0,n,dia(0,box(0,n)))), 2).
formula(dr(0,dl(0,dr(0,dr(0,s,s),dia(0,box(0,np))),dr(0,dr(0,s,s),np)),dr(0,dr(0,s,s),dia(0,box(0,np)))), 2).
formula(dr(0,dl(0,dr(0,dl(1,s,s),n),dr(0,dl(1,s,s),n)),dr(0,dl(1,s,s),n)), 2).
formula(dr(0,dl(0,dr(0,dl(1,s,s),dl(1,s,s)),dr(0,dl(1,s,s),dl(1,s,s))),dr(0,dl(1,s,s),dl(1,s,s))), 2).
formula(dr(0,dl(0,dr(0,dl(0,np,s),dia(0,box(0,s_q))),dr(0,dl(0,np,s),s_q)),dr(0,dl(0,np,s),dia(0,box(0,s_q)))), 2).
formula(dr(0,dl(0,dr(0,dl(0,np,s),dia(0,box(0,pp))),dr(0,dl(0,np,s),pp)),dr(0,dl(0,np,s),dia(0,box(0,pp)))), 2).
formula(dr(0,dl(0,dr(0,dl(0,np,s),dia(0,box(0,dl(0,np,s)))),dr(0,dl(0,np,s),dl(0,np,s))),dr(0,dl(0,np,s),dia(0,box(0,dl(0,np,s))))), 2).
formula(dr(0,dl(0,dr(0,dl(0,n,n),s_q),dr(0,dl(0,n,n),s_q)),dr(0,dl(0,n,n),s_q)), 2).
formula(dr(0,dl(0,dr(0,dl(0,n,n),dia(0,box(0,pp))),dr(0,dl(0,n,n),pp)),dr(0,dl(0,n,n),dia(0,box(0,pp)))), 2).
formula(dr(0,dl(0,dr(0,dl(0,n,n),dia(0,box(0,dl(0,np,s)))),dr(0,dl(0,n,n),dl(0,np,s))),dr(0,dl(0,n,n),dia(0,box(0,dl(0,np,s))))), 2).
formula(dr(0,dl(0,dl(1,s,s),dl(1,s,s)),s_q), 2).
formula(dr(0,dl(0,dl(1,s,s),dl(1,s,s)),s), 2).
formula(dr(0,dl(0,dl(1,dl(0,np,s),dl(0,np,s)),dl(1,dl(0,np,s),dl(0,np,s))),dl(1,dl(0,np,s),dl(0,np,s))), 2).
formula(dr(0,dl(0,dl(0,np,s_inf),s),pp_a), 2).
formula(dr(0,dl(0,dl(0,np,s),dl(1,s,s)),dl(0,np,s)), 2).
formula(dr(0,dl(0,dl(0,np,s),dl(0,np,s)),s), 2).
formula(dr(0,dl(0,dl(0,n,n),s),dr(0,s,dia(1,box(1,dl(0,n,n))))), 2).
formula(dr(0,dl(0,cl_y,dl(0,np,s)),dr(0,dl(0,cl_y,dl(0,np,s)),dia(1,box(1,np)))), 2).
formula(dr(0,dl(0,cl_r,dr(0,s,np)),dl(0,np,s_inf)), 2).
formula(dr(0,dl(0,cl_r,dl(1,s,s)),np), 2).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppres)),pp_par), 2).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppres)),dl(0,cl_r,dl(0,np,s_ppart))), 2).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),dr(0,dl(0,np,s_inf),dia(1,box(1,pp_a)))), 2).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),dl(1,s,s)), 2).
formula(dr(0,dl(0,cl_r,dl(0,n,n)),pp), 2).
formula(dl(1,s,dl(0,cl_r,dl(0,np,s_ppart))), 2).
formula(dl(0,n,dl(1,s,s)), 2).
formula(dl(0,dr(0,s,s),s), 2).
formula(dl(0,dl(0,n,n),dl(0,np,s_inf)), 2).
formula(dl(0,dl(0,n,n),dl(0,n,n)), 2).
formula(dl(0,cl_r,dl(0,n,n)), 2).
formula(pp_de, 1).
formula(dr(0,s,pp_de), 1).
formula(dr(0,s,n), 1).
formula(dr(0,s,dl(0,np,s_ppart)), 1).
formula(dr(0,pp,dr(0,s,dia(1,box(1,pp)))), 1).
formula(dr(0,pp,dl(0,np,s)), 1).
formula(dr(0,pp,dl(0,n,n)), 1).
formula(dr(0,np,pp_a), 1).
formula(dr(0,np,dr(0,n,n)), 1).
formula(dr(0,n,dl(0,n,n)), 1).
formula(dr(0,dr(0,s_whq,dr(0,s,dia(1,box(1,pp_a)))),pp_de), 1).
formula(dr(0,dr(0,s_whq,dl(0,np,s_inf)),n), 1).
formula(dr(0,dr(0,s_ppres,dl(0,np,s_inf)),np), 1).
formula(dr(0,dr(0,s,s_whq),np), 1).
formula(dr(0,dr(0,s,s),pp_par), 1).
formula(dr(0,dr(0,s,pp),clr), 1).
formula(dr(0,dr(0,s,dr(0,s,dia(1,box(1,pp)))),np), 1).
formula(dr(0,dr(0,s,dl(1,s,s)),np), 1).
formula(dr(0,dr(0,s,dl(0,np,s_inf)),dl(0,np,s_ppart)), 1).
formula(dr(0,dr(0,s,dl(0,np,s_inf)),cl_r), 1).
formula(dr(0,dr(0,pp_a,np),n), 1).
formula(dr(0,dr(0,pp,pp),dl(1,s,s)), 1).
formula(dr(0,dr(0,p(0,dl(0,n,n),dia(0,box(0,np))),s_q),p(0,dl(0,n,n),np)), 1).
formula(dr(0,dr(0,np,s_q),pp), 1).
formula(dr(0,dr(0,np,s_q),n), 1).
formula(dr(0,dr(0,np,np),pp_de), 1).
formula(dr(0,dr(0,np,np),pp), 1).
formula(dr(0,dr(0,np,np),dl(1,s,s)), 1).
formula(dr(0,dr(0,np,np),dl(0,np,s_ppres)), 1).
formula(dr(0,dr(0,np,n),np), 1).
formula(dr(0,dr(0,np,n),dr(0,np,n)), 1).
formula(dr(0,dr(0,n,s_q),pp), 1).
formula(dr(0,dr(0,dr(0,s,s_q),s),n), 1).
formula(dr(0,dr(0,dr(0,s,s_q),dl(0,np,s_inf)),np), 1).
formula(dr(0,dr(0,dr(0,s,s_q),dl(0,n,n)),np), 1).
formula(dr(0,dr(0,dr(0,s,s),pp_par),np), 1).
formula(dr(0,dr(0,dr(0,s,pp_a),dl(0,np,s_inf)),pp_a), 1).
formula(dr(0,dr(0,dr(0,s,dl(0,np,s)),np),np), 1).
formula(dr(0,dr(0,dr(0,s,dl(0,np,s)),np),dr(0,dr(0,s,dl(0,np,s)),np)), 1).
formula(dr(0,dr(0,dr(0,np,s_q),np),dl(1,s,s)), 1).
formula(dr(0,dr(0,dr(0,n,n),dr(0,n,n)),n), 1).
formula(dr(0,dr(0,dr(0,dl(0,np,s_ppres),dl(0,np,s_inf)),pp_a),np), 1).
formula(dr(0,dr(0,dr(0,dl(0,np,s_ppart),np),pp_a),dl(0,np,s_inf)), 1).
formula(dr(0,dr(0,dr(0,dl(0,np,s_ppart),dl(0,np,s_inf)),pp_a),dl(0,n,n)), 1).
formula(dr(0,dr(0,dr(0,dl(0,np,s_inf),pp_par),pp_de),np), 1).
formula(dr(0,dr(0,dr(0,dl(0,np,s_inf),pp_a),np),pp), 1).
formula(dr(0,dr(0,dr(0,dl(0,np,s_inf),pp_a),dl(0,n,n)),np), 1).
formula(dr(0,dr(0,dr(0,dl(0,np,s_inf),dl(0,np,s_inf)),pp_par),np), 1).
formula(dr(0,dr(0,dr(0,dl(0,np,s),s_q),pp_a),np), 1).
formula(dr(0,dr(0,dr(0,dl(0,np,s),pp),s_q),dr(0,dl(0,np,s),pp)), 1).
formula(dr(0,dr(0,dl(1,s,s),dl(1,s,s)),s_q), 1).
formula(dr(0,dr(0,dl(1,s,s),dl(1,s,s)),s), 1).
formula(dr(0,dr(0,dl(1,s,s),dl(1,s,s)),dr(0,dl(1,s,s),dl(1,s,s))), 1).
formula(dr(0,dr(0,dl(1,s,s),dl(1,s,s)),dl(0,np,s_inf)), 1).
formula(dr(0,dr(0,dl(1,dl(0,n,n),dl(0,n,n)),dl(0,n,n)),np), 1).
formula(dr(0,dr(0,dl(0,np,s_ppres),pp_a),dl(0,np,s_inf)), 1).
formula(dr(0,dr(0,dl(0,np,s_ppres),pp_a),dl(0,n,n)), 1).
formula(dr(0,dr(0,dl(0,np,s_ppres),np),pp_a), 1).
formula(dr(0,dr(0,dl(0,np,s_ppres),np),np), 1).
formula(dr(0,dr(0,dl(0,np,s_ppres),dl(0,np,s_ppart)),np), 1).
formula(dr(0,dr(0,dl(0,np,s_ppart),s_whq),pp_a), 1).
formula(dr(0,dr(0,dl(0,np,s_ppart),pp_par),dl(0,n,n)), 1).
formula(dr(0,dr(0,dl(0,np,s_ppart),pp_a),pp_de), 1).
formula(dr(0,dr(0,dl(0,np,s_ppart),pp_a),dl(0,np,s_inf)), 1).
formula(dr(0,dr(0,dl(0,np,s_ppart),pp),pp_de), 1).
formula(dr(0,dr(0,dl(0,np,s_ppart),np),pp_par), 1).
formula(dr(0,dr(0,dl(0,np,s_ppart),dl(0,np,s_inf)),pp_de), 1).
formula(dr(0,dr(0,dl(0,np,s_pass),pp_de),pp_par), 1).
formula(dr(0,dr(0,dl(0,np,s_pass),np),pp_par), 1).
formula(dr(0,dr(0,dl(0,np,s_inf),pp_de),pp_a), 1).
formula(dr(0,dr(0,dl(0,np,s_inf),pp_a),pp_de), 1).
formula(dr(0,dr(0,dl(0,np,s_inf),pp_a),pp), 1).
formula(dr(0,dr(0,dl(0,np,s_inf),pp_a),dl(0,n,n)), 1).
formula(dr(0,dr(0,dl(0,np,s_inf),pp),pp), 1).
formula(dr(0,dr(0,dl(0,np,s_inf),dl(0,np,s_inf)),pp), 1).
formula(dr(0,dr(0,dl(0,np,s),pp_par),pp_de), 1).
formula(dr(0,dr(0,dl(0,np,s),pp_de),dl(0,n,n)), 1).
formula(dr(0,dr(0,dl(0,np,s),pp_a),s_q), 1).
formula(dr(0,dr(0,dl(0,np,s),dl(0,np,s_inf)),dl(0,np,s)), 1).
formula(dr(0,dr(0,dl(0,np,s),dl(0,n,n)),pp_a), 1).
formula(dr(0,dr(0,dl(0,np,np),pp_par),np), 1).
formula(dr(0,dr(0,dl(0,np,np),dl(0,np,s)),np), 1).
formula(dr(0,dr(0,dl(0,np,np),dl(0,np,np)),n), 1).
formula(dr(0,dr(0,dl(0,np,dr(0,s,s)),pp_a),pp_par), 1).
formula(dr(0,dr(0,dl(0,n,n),s_q),pp_de), 1).
formula(dr(0,dr(0,dl(0,n,n),s_q),pp_a), 1).
formula(dr(0,dr(0,dl(0,n,n),s_q),np), 1).
formula(dr(0,dr(0,dl(0,n,n),pp),np), 1).
formula(dr(0,dr(0,dl(0,n,n),np),dl(0,np,s_inf)), 1).
formula(dr(0,dr(0,dl(0,n,n),dl(0,n,n)),pp_par), 1).
formula(dr(0,dr(0,dl(0,n,n),dl(0,n,n)),pp_de), 1).
formula(dr(0,dr(0,dl(0,n,n),dl(0,n,n)),dl(0,np,s_inf)), 1).
formula(dr(0,dr(0,dl(0,n,n),dl(0,n,n)),dl(0,n,n)), 1).
formula(dr(0,dr(0,dl(0,dr(0,pp,dia(0,box(0,n))),s_whq),s),n), 1).
formula(dr(0,dr(0,dl(0,dl(0,np,s_inf),s),pp_a),np), 1).
formula(dr(0,dr(0,dl(0,dl(0,np,s_inf),s),pp_a),dl(0,n,n)), 1).
formula(dr(0,dr(0,dl(0,cl_y,dl(0,np,s)),dl(0,np,s_inf)),dl(0,n,n)), 1).
formula(dr(0,dr(0,dl(0,cl_r,s),pp_de),np), 1).
formula(dr(0,dr(0,dl(0,cl_r,s),pp_a),s_q), 1).
formula(dr(0,dr(0,dl(0,cl_r,s),dl(0,cl_r,dl(0,np,s_ppart))),np), 1).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s_ppres)),s_q),np), 1).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s_ppart)),pp_par),dl(0,np,s_inf)), 1).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s_ppart)),pp_de),np), 1).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s_inf)),s_q),np), 1).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s)),dl(0,np,s_inf)),np), 1).
formula(dr(0,dr(0,dl(0,cl_r,dl(0,np,s)),dl(0,cl_r,dl(0,np,s))),n), 1).
formula(dr(0,dl(1,s,s),dr(0,n,n)), 1).
formula(dr(0,dl(1,s,s),dl(0,np,s_ppart)), 1).
formula(dr(0,dl(1,dl(0,np,s),dl(0,np,s)),pp_a), 1).
formula(dr(0,dl(1,dl(0,np,s),dl(0,np,s)),n), 1).
formula(dr(0,dl(1,dl(0,np,s),dl(0,np,s)),dl(0,np,s)), 1).
formula(dr(0,dl(1,dl(0,np,np),dl(0,np,np)),dl(0,np,s_inf)), 1).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),dl(0,np,s_pass)), 1).
formula(dr(0,dl(1,dl(0,n,n),dl(0,n,n)),dl(0,n,n)), 1).
formula(dr(0,dl(0,s,s),pp), 1).
formula(dr(0,dl(0,pp_de,dr(0,s,s)),n), 1).
formula(dr(0,dl(0,pp,dr(0,s,dr(0,s,dia(1,box(1,pp))))),pp), 1).
formula(dr(0,dl(0,pp,dl(1,s,s)),pp), 1).
formula(dr(0,dl(0,pp,dl(1,s,s)),dr(0,s,dia(1,box(1,pp)))), 1).
formula(dr(0,dl(0,p(0,pp,dl(1,dl(0,n,n),dl(0,n,n))),p(0,pp,dl(1,dl(0,n,n),dl(0,n,n)))),p(0,pp,dl(1,dl(0,n,n),dl(0,n,n)))), 1).
formula(dr(0,dl(0,p(0,p(0,pp,np),dl(1,s,s)),p(0,p(0,pp,dia(0,box(0,np))),dl(1,s,s))),p(0,pp,dl(1,s,s))), 1).
formula(dr(0,dl(0,p(0,n,pp),p(0,n,dia(0,box(0,pp)))),p(0,n,pp)), 1).
formula(dr(0,dl(0,p(0,dl(0,np,s),np),p(0,dl(0,np,s),dia(0,box(0,np)))),p(0,dl(0,np,s),np)), 1).
formula(dr(0,dl(0,np,pp_de),np), 1).
formula(dr(0,dl(0,np,dr(0,s,s)),dl(0,np,dr(0,s,s))), 1).
formula(dr(0,dl(0,np,dl(1,s,s)),dl(0,np,dl(1,s,s))), 1).
formula(dr(0,dl(0,np,dl(1,s,s)),dl(0,n,n)), 1).
formula(dr(0,dl(0,np,dl(0,np,np)),pp), 1).
formula(dr(0,dl(0,np,dl(0,np,np)),dl(0,np,s)), 1).
formula(dr(0,dl(0,np,dl(0,n,n)),pp), 1).
formula(dr(0,dl(0,np,dl(0,n,n)),dl(0,np,dl(0,n,n))), 1).
formula(dr(0,dl(0,np,dl(0,dr(0,s,s),dr(0,s,s))),dr(0,s,s)), 1).
formula(dr(0,dl(0,n,pp_a),n), 1).
formula(dr(0,dl(0,n,n),dr(0,s,s)), 1).
formula(dr(0,dl(0,n,n),dl(0,s,s)), 1).
formula(dr(0,dl(0,n,dr(0,s,s)),n), 1).
formula(dr(0,dl(0,n,dl(0,n,n)),n), 1).
formula(dr(0,dl(0,dr(0,s,s),np),np), 1).
formula(dr(0,dl(0,dr(0,s,s),dr(0,s,s)),s), 1).
formula(dr(0,dl(0,dr(0,s,s),dr(0,s,s)),dr(0,dr(0,s,dl(0,np,s)),np)), 1).
formula(dr(0,dl(0,dr(0,s,np),dr(0,s,np)),dl(0,np,s_inf)), 1).
formula(dr(0,dl(0,dr(0,s,dr(0,s,dia(1,box(1,pp_a)))),dr(0,s,dr(0,s,dia(1,box(1,pp_a))))),dr(0,s,dr(0,s,dia(1,box(1,pp_a))))), 1).
formula(dr(0,dl(0,dr(0,s,dl(0,np,s)),dr(0,s,dl(0,np,s))),dr(0,s,dl(0,np,s))), 1).
formula(dr(0,dl(0,dr(0,s,dia(1,box(1,dr(0,s,np)))),dr(0,s,box(1,dia(1,dr(0,s,np))))),dr(0,s,dia(1,box(1,dr(0,s,np))))), 1).
formula(dr(0,dl(0,dr(0,s,dia(1,box(1,dl(0,np,s)))),dr(0,s,box(1,dia(1,dl(0,np,s))))),dr(0,s,dia(1,box(1,dl(0,np,s))))), 1).
formula(dr(0,dl(0,dr(0,s,dia(0,box(0,np))),np),n), 1).
formula(dr(0,dl(0,dr(0,pp,pp_de),dl(0,n,n)),s), 1).
formula(dr(0,dl(0,dr(0,pp,pp_de),dl(0,n,n)),dr(0,s,dia(1,box(1,pp)))), 1).
formula(dr(0,dl(0,dr(0,pp,np),s_whq),pp_de), 1).
formula(dr(0,dl(0,dr(0,pp,np),s_whq),dl(0,np,s_inf)), 1).
formula(dr(0,dl(0,dr(0,pp,np),dr(0,pp,np)),dr(0,pp,np)), 1).
formula(dr(0,dl(0,dr(0,pp,np),dl(1,s,s)),dl(1,s,s)), 1).
formula(dr(0,dl(0,dr(0,pp,np),dl(0,np,np)),np), 1).
formula(dr(0,dl(0,dr(0,pp,dia(0,box(0,n))),s_whq),s), 1).
formula(dr(0,dl(0,dr(0,pp,dia(0,box(0,n))),s),s), 1).
formula(dr(0,dl(0,dr(0,pp,dia(0,box(0,n))),dr(0,pp,n)),dr(0,pp,dia(0,box(0,n)))), 1).
formula(dr(0,dl(0,dr(0,n,n),n),n), 1).
formula(dr(0,dl(0,dr(0,dr(0,np,np),n),dr(0,dr(0,np,np),n)),dr(0,dr(0,np,np),n)), 1).
formula(dr(0,dl(0,dr(0,dr(0,dr(0,s,s),dr(0,s,s)),n),dr(0,dr(0,dr(0,s,s),dr(0,s,s)),n)),dr(0,dr(0,dr(0,s,s),dr(0,s,s)),n)), 1).
formula(dr(0,dl(0,dr(0,dr(0,dl(1,s,s),s_q),dl(1,s,s)),dr(0,dr(0,dl(1,s,s),s_q),dl(1,s,s))),dr(0,dr(0,dl(1,s,s),s_q),dl(1,s,s))), 1).
formula(dr(0,dl(0,dr(0,dr(0,dl(0,np,s),dl(0,np,s)),dia(0,box(0,np))),dr(0,dr(0,dl(0,np,s),dl(0,np,s)),np)),dr(0,dr(0,dl(0,np,s),dl(0,np,s)),dia(0,box(0,np)))), 1).
formula(dr(0,dl(0,dr(0,dl(1,s,s),s_q),dr(0,dl(1,s,s),s_q)),dr(0,dl(1,s,s),s_q)), 1).
formula(dr(0,dl(0,dr(0,dl(1,s,s),np),dr(0,dl(1,s,s),np)),dr(0,dl(1,s,s),np)), 1).
formula(dr(0,dl(0,dr(0,dl(1,s,s),dia(0,box(0,np))),dr(0,dl(1,s,s),np)),dr(0,dl(1,s,s),dia(0,box(0,np)))), 1).
formula(dr(0,dl(0,dr(0,dl(1,s,s),dia(0,box(0,n))),dl(0,n,n)),s), 1).
formula(dr(0,dl(0,dr(0,dl(0,n,n),dl(0,np,s)),dr(0,dl(0,n,n),dl(0,np,s))),dr(0,dl(0,n,n),dl(0,np,s))), 1).
formula(dr(0,dl(0,dr(0,dl(0,n,n),dia(0,box(0,np))),dr(0,dl(0,n,n),np)),dr(0,dl(0,n,n),dia(0,box(0,np)))), 1).
formula(dr(0,dl(0,dr(0,dl(0,dl(1,s,s),dl(1,s,s)),dl(1,s,s)),dr(0,dl(0,dl(1,s,s),dl(1,s,s)),dl(1,s,s))),dr(0,dl(0,dl(1,s,s),dl(1,s,s)),dl(1,s,s))), 1).
formula(dr(0,dl(0,dl(1,s,s),dl(1,s,s)),np), 1).
formula(dr(0,dl(0,dl(1,s,s),dl(1,s,s)),n), 1).
formula(dr(0,dl(0,dl(1,s,s),dl(1,s,s)),dl(0,np,s)), 1).
formula(dr(0,dl(0,dl(1,s,s),dl(1,s,s)),dl(0,dl(0,np,s),dl(0,np,s))), 1).
formula(dr(0,dl(0,dl(0,np,s_inf),s),pp_de), 1).
formula(dr(0,dl(0,dl(0,np,s_inf),s),dl(0,np,s_ppart)), 1).
formula(dr(0,dl(0,dl(0,np,s),s),dr(0,dl(0,dl(0,np,s),s),dia(1,box(1,pp_a)))), 1).
formula(dr(0,dl(0,dl(0,np,s),np),n), 1).
formula(dr(0,dl(0,dl(0,np,s),dl(0,np,s)),dl(0,n,n)), 1).
formula(dr(0,dl(0,dl(0,n,n),s_q),dr(0,s,dia(1,box(1,dl(0,n,n))))), 1).
formula(dr(0,dl(0,dl(0,n,n),dl(0,np,np)),dr(0,s,dia(1,box(1,pp)))), 1).
formula(dr(0,dl(0,dl(0,n,n),dl(0,np,np)),dr(0,s,dia(1,box(1,dl(0,n,n))))), 1).
formula(dr(0,dl(0,dl(0,n,n),dl(0,n,n)),s), 1).
formula(dr(0,dl(0,dl(0,n,n),dl(0,n,n)),n), 1).
formula(dr(0,dl(0,dl(0,n,n),dl(0,n,n)),dl(0,np,s)), 1).
formula(dr(0,dl(0,dl(0,dl(0,np,s),s),dl(0,dl(0,np,s),s)),dl(0,dl(0,np,s),s)), 1).
formula(dr(0,dl(0,dl(0,dia(0,box(0,n)),n),np),np), 1).
formula(dr(0,dl(0,cl_y,s),dr(0,s,s)), 1).
formula(dr(0,dl(0,cl_y,dl(0,np,s)),dl(0,n,n)), 1).
formula(dr(0,dl(0,cl_y,dl(0,np,dl(1,dl(0,np,np),dl(0,np,np)))),np), 1).
formula(dr(0,dl(0,cl_y,dl(0,n,n)),np), 1).
formula(dr(0,dl(0,cl_r,s),dr(0,dl(0,cl_r,s),dia(1,box(1,pp_de)))), 1).
formula(dr(0,dl(0,cl_r,s),dl(0,cl_r,s)), 1).
formula(dr(0,dl(0,cl_r,s),dl(0,cl_r,dl(0,np,s_ppart))), 1).
formula(dr(0,dl(0,cl_r,dr(0,s,s)),pp_de), 1).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppres)),s_q), 1).
formula(dr(0,dl(0,cl_r,dl(0,np,s_ppres)),np), 1).
formula(dr(0,dl(0,cl_r,dl(0,np,s_inf)),dr(0,dl(0,np,s_inf),dia(1,box(1,pp_de)))), 1).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),s), 1).
formula(dr(0,dl(0,cl_r,dl(0,np,s)),dl(0,cl_r,dl(0,np,s_inf))), 1).
formula(dr(0,dl(0,cl_r,dl(0,n,n)),pp_de), 1).
formula(dr(0,dl(0,cl_r,dl(0,dl(0,np,s_inf),s)),dl(0,np,s_inf)), 1).
formula(dr(0,dl(0,cl_r,dl(0,dl(0,n,n),dl(0,n,n))),pp_de), 1).
formula(dl(0,np,dl(0,np,s_inf)), 1).
formula(dl(0,np,dl(0,np,s)), 1).
formula(dl(0,np,dl(0,np,np)), 1).
formula(dl(0,dr(0,pp,np),s_whq), 1).
formula(dl(0,dr(0,pp,np),np), 1).
formula(dl(0,dr(0,pp,dia(0,box(0,n))),s_whq), 1).
formula(dl(0,dr(0,n,n),dr(0,n,n)), 1).
formula(dl(0,dr(0,dl(0,np,s),np),s_whq), 1).
formula(dl(0,dl(0,np,s_inf),s), 1).
formula(dl(0,dl(0,np,s),np), 1).
formula(dl(0,dl(0,np,s),dl(1,s,s)), 1).
formula(dl(0,cl_r,dl(1,s,s)), 1).
formula(dl(0,cl_r,dl(0,np,dr(0,n,n))), 1).