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