/
output_Course
3709 lines (3708 loc) · 449 KB
/
output_Course
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
[ tableau proof ]
[fof(degree,axiom,(((((((composition & humanities) & science) & math) & social_science) & language) & writing) => degree)).,
fof(composition,axiom,((eng105 & eng106) => composition)).,
fof(composition_courses,axiom,(eng105 & eng106)).,
fof(humanities,axiom,((((art & literature) & religion) & phi115) => humanities)).,
fof(art,axiom,(((((artXXX | arhXXX) | danXXX) | mcyXXX) | thaXXX) => art)).,
fof(artXXX,axiom,artXXX).,
fof(literature,axiom,(eng2XX => literature)).,
fof(literature_courses,axiom,eng2XX).,
fof(religion,axiom,(relXXX => religion)).,
fof(religion_courses,axiom,relXXX).,
fof(phi115,axiom,phi115).,
fof(science,axiom,((((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX) | phyXXX) => science)).,
fof(phyXXX,axiom,phyXXX).,
fof(math,axiom,((mth162 & (cscXXX | staXXX)) => math)).,
fof(mth162,axiom,mth162).,
fof(cscXXX,axiom,cscXXX).,
fof(social_science,axiom,((((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX) | socXXX) => social_science)).,
fof(ecoXXX,axiom,ecoXXX).,
fof(language,axiom,(((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX) | spa2XX) => language)).,
fof(arbXXX,axiom,arb2XX).,
fof(wwwXXX_writing,axiom,(wwwXXX => writing)).,
fof(wwwXXX,axiom,wwwXXX).,
fof(hisXXX_writing,axiom,(hisXXX => writing)).,
fof(eng2XX_writing,axiom,(eng2XX => writing)).,
fof(phi115_writing,axiom,(phi115 => writing)).,
fof(not_get_degree,Theorem,~ (degree),negConjunction(get_degree)).]
[fof(genFunction_2_1,theorem,~ (((((((composition & humanities) & science) & math) & social_science) & language) & writing)),beta1(degree)).]
[fof(genFunction_4_1,theorem,~ ((eng105 & eng106)),beta1(composition)).,
fof(contradict_4_1,theorem,((eng105 & eng106) & ~ ((eng105 & eng106))),contraction(composition_courses,genFunction_4_1)).]
[fof(genFunction_5_1,theorem,composition,beta2(composition)).,
fof(genFunction_5_1,theorem,eng105,alpha1(composition_courses)).,
fof(genFunction_5_2,theorem,eng106,alpha2(composition_courses)).]
[fof(genFunction_10_1,theorem,~ ((((art & literature) & religion) & phi115)),beta1(humanities)).]
[fof(genFunction_20_1,theorem,~ (((((artXXX | arhXXX) | danXXX) | mcyXXX) | thaXXX)),beta1(art)).]
[fof(genFunction_40_1,theorem,~ (eng2XX),beta1(literature)).,
fof(contradict_40_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_40_1)).]
[fof(genFunction_41_1,theorem,literature,beta2(literature)).]
[fof(genFunction_82_1,theorem,~ (relXXX),beta1(religion)).,
fof(contradict_82_1,theorem,(relXXX & ~ (relXXX)),contraction(religion_courses,genFunction_82_1)).]
[fof(genFunction_83_1,theorem,religion,beta2(religion)).]
[fof(genFunction_166_1,theorem,~ ((((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX) | phyXXX)),beta1(science)).]
[fof(genFunction_332_1,theorem,~ ((mth162 & (cscXXX | staXXX))),beta1(math)).]
[fof(genFunction_664_1,theorem,~ ((((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX) | socXXX)),beta1(social_science)).]
[fof(genFunction_1328_1,theorem,~ (((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX) | spa2XX)),beta1(language)).]
[fof(genFunction_2656_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2656_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2656_1)).]
[fof(genFunction_2657_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5314_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10628_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10628_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10628_1)).]
[fof(genFunction_10629_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21258_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21258_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21258_1)).]
[fof(genFunction_21259_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42518_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85036_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85036_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85036_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85036_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85036_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85036_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85036_4)).]
[fof(genFunction_85037_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85037_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85037_1)).]
[fof(genFunction_42519_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42519_1,theorem,(writing & ~ (writing)),contraction(genFunction_10629_1,genFunction_42519_1)).]
[fof(genFunction_5315_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10630_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10630_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10630_1)).]
[fof(genFunction_10631_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21262_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21262_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21262_1)).]
[fof(genFunction_21263_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42526_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85052_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85052_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85052_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85052_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85052_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85052_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85052_4)).]
[fof(genFunction_85053_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85053_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85053_1)).]
[fof(genFunction_42527_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42527_1,theorem,(writing & ~ (writing)),contraction(genFunction_10631_1,genFunction_42527_1)).]
[fof(genFunction_1329_1,theorem,language,beta2(language)).]
[fof(genFunction_2658_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2658_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2658_1)).]
[fof(genFunction_2659_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5318_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10636_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10636_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10636_1)).]
[fof(genFunction_10637_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21274_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21274_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21274_1)).]
[fof(genFunction_21275_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42550_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85100_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85100_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85100_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85100_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85100_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85100_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85100_4)).]
[fof(genFunction_85101_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85101_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85101_1)).]
[fof(genFunction_42551_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42551_1,theorem,(writing & ~ (writing)),contraction(genFunction_10637_1,genFunction_42551_1)).]
[fof(genFunction_5319_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10638_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10638_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10638_1)).]
[fof(genFunction_10639_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21278_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21278_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21278_1)).]
[fof(genFunction_21279_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42558_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85116_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85116_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85116_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85116_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85116_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85116_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85116_4)).]
[fof(genFunction_85117_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85117_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85117_1)).]
[fof(genFunction_42559_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42559_1,theorem,(writing & ~ (writing)),contraction(genFunction_10639_1,genFunction_42559_1)).]
[fof(genFunction_665_1,theorem,social_science,beta2(social_science)).]
[fof(genFunction_1330_1,theorem,~ (((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX) | spa2XX)),beta1(language)).]
[fof(genFunction_2660_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2660_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2660_1)).]
[fof(genFunction_2661_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5322_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10644_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10644_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10644_1)).]
[fof(genFunction_10645_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21290_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21290_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21290_1)).]
[fof(genFunction_21291_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42582_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85164_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85164_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85164_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85164_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85164_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85164_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85164_4)).]
[fof(genFunction_85165_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85165_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85165_1)).]
[fof(genFunction_42583_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42583_1,theorem,(writing & ~ (writing)),contraction(genFunction_10645_1,genFunction_42583_1)).]
[fof(genFunction_5323_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10646_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10646_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10646_1)).]
[fof(genFunction_10647_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21294_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21294_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21294_1)).]
[fof(genFunction_21295_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42590_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85180_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85180_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85180_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85180_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85180_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85180_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85180_4)).]
[fof(genFunction_85181_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85181_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85181_1)).]
[fof(genFunction_42591_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42591_1,theorem,(writing & ~ (writing)),contraction(genFunction_10647_1,genFunction_42591_1)).]
[fof(genFunction_1331_1,theorem,language,beta2(language)).]
[fof(genFunction_2662_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2662_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2662_1)).]
[fof(genFunction_2663_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5326_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10652_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10652_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10652_1)).]
[fof(genFunction_10653_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21306_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21306_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21306_1)).]
[fof(genFunction_21307_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42614_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85228_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85228_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85228_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85228_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85228_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85228_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85228_4)).]
[fof(genFunction_85229_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85229_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85229_1)).]
[fof(genFunction_42615_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42615_1,theorem,(writing & ~ (writing)),contraction(genFunction_10653_1,genFunction_42615_1)).]
[fof(genFunction_5327_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10654_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10654_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10654_1)).]
[fof(genFunction_10655_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21310_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21310_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21310_1)).]
[fof(genFunction_21311_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42622_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85244_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85244_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85244_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85244_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85244_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85244_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85244_4)).]
[fof(genFunction_85245_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85245_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85245_1)).]
[fof(genFunction_42623_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42623_1,theorem,(writing & ~ (writing)),contraction(genFunction_10655_1,genFunction_42623_1)).]
[fof(genFunction_333_1,theorem,math,beta2(math)).]
[fof(genFunction_666_1,theorem,~ ((((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX) | socXXX)),beta1(social_science)).]
[fof(genFunction_1332_1,theorem,~ (((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX) | spa2XX)),beta1(language)).]
[fof(genFunction_2664_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2664_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2664_1)).]
[fof(genFunction_2665_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5330_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10660_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10660_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10660_1)).]
[fof(genFunction_10661_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21322_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21322_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21322_1)).]
[fof(genFunction_21323_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42646_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85292_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85292_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85292_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85292_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85292_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85292_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85292_4)).]
[fof(genFunction_85293_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85293_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85293_1)).]
[fof(genFunction_42647_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42647_1,theorem,(writing & ~ (writing)),contraction(genFunction_10661_1,genFunction_42647_1)).]
[fof(genFunction_5331_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10662_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10662_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10662_1)).]
[fof(genFunction_10663_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21326_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21326_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21326_1)).]
[fof(genFunction_21327_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42654_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85308_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85308_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85308_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85308_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85308_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85308_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85308_4)).]
[fof(genFunction_85309_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85309_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85309_1)).]
[fof(genFunction_42655_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42655_1,theorem,(writing & ~ (writing)),contraction(genFunction_10663_1,genFunction_42655_1)).]
[fof(genFunction_1333_1,theorem,language,beta2(language)).]
[fof(genFunction_2666_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2666_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2666_1)).]
[fof(genFunction_2667_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5334_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10668_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10668_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10668_1)).]
[fof(genFunction_10669_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21338_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21338_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21338_1)).]
[fof(genFunction_21339_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42678_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85356_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85356_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85356_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85356_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85356_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85356_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85356_4)).]
[fof(genFunction_85357_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85357_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85357_1)).]
[fof(genFunction_42679_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42679_1,theorem,(writing & ~ (writing)),contraction(genFunction_10669_1,genFunction_42679_1)).]
[fof(genFunction_5335_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10670_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10670_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10670_1)).]
[fof(genFunction_10671_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21342_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21342_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21342_1)).]
[fof(genFunction_21343_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42686_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85372_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85372_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85372_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85372_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85372_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85372_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85372_4)).]
[fof(genFunction_85373_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85373_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85373_1)).]
[fof(genFunction_42687_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42687_1,theorem,(writing & ~ (writing)),contraction(genFunction_10671_1,genFunction_42687_1)).]
[fof(genFunction_667_1,theorem,social_science,beta2(social_science)).]
[fof(genFunction_1334_1,theorem,~ (((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX) | spa2XX)),beta1(language)).]
[fof(genFunction_2668_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2668_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2668_1)).]
[fof(genFunction_2669_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5338_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10676_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10676_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10676_1)).]
[fof(genFunction_10677_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21354_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21354_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21354_1)).]
[fof(genFunction_21355_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42710_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85420_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85420_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85420_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85420_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85420_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85420_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85420_4)).]
[fof(genFunction_85421_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85421_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85421_1)).]
[fof(genFunction_42711_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42711_1,theorem,(writing & ~ (writing)),contraction(genFunction_10677_1,genFunction_42711_1)).]
[fof(genFunction_5339_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10678_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10678_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10678_1)).]
[fof(genFunction_10679_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21358_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21358_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21358_1)).]
[fof(genFunction_21359_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42718_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85436_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85436_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85436_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85436_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85436_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85436_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85436_4)).]
[fof(genFunction_85437_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85437_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85437_1)).]
[fof(genFunction_42719_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42719_1,theorem,(writing & ~ (writing)),contraction(genFunction_10679_1,genFunction_42719_1)).]
[fof(genFunction_1335_1,theorem,language,beta2(language)).]
[fof(genFunction_2670_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2670_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2670_1)).]
[fof(genFunction_2671_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5342_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10684_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10684_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10684_1)).]
[fof(genFunction_10685_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21370_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21370_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21370_1)).]
[fof(genFunction_21371_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42742_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85484_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85484_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85484_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85484_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85484_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85484_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85484_4)).]
[fof(genFunction_85485_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85485_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85485_1)).]
[fof(genFunction_42743_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42743_1,theorem,(writing & ~ (writing)),contraction(genFunction_10685_1,genFunction_42743_1)).]
[fof(genFunction_5343_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10686_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10686_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10686_1)).]
[fof(genFunction_10687_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21374_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21374_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21374_1)).]
[fof(genFunction_21375_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42750_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85500_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85500_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85500_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85500_3,theorem,~ (((((bilXXX | chmXXX) | ecsXXX) | geoXXX) | mscXXX)),alpha1(genFunction_166_1)).,
fof(genFunction_85500_4,theorem,~ (phyXXX),alpha2(genFunction_166_1)).,
fof(contradict_85500_4,theorem,(phyXXX & ~ (phyXXX)),contraction(phyXXX,genFunction_85500_4)).]
[fof(genFunction_85501_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85501_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85501_1)).]
[fof(genFunction_42751_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42751_1,theorem,(writing & ~ (writing)),contraction(genFunction_10687_1,genFunction_42751_1)).]
[fof(genFunction_167_1,theorem,science,beta2(science)).]
[fof(genFunction_334_1,theorem,~ ((mth162 & (cscXXX | staXXX))),beta1(math)).]
[fof(genFunction_668_1,theorem,~ ((((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX) | socXXX)),beta1(social_science)).]
[fof(genFunction_1336_1,theorem,~ (((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX) | spa2XX)),beta1(language)).]
[fof(genFunction_2672_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2672_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2672_1)).]
[fof(genFunction_2673_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5346_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10692_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10692_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10692_1)).]
[fof(genFunction_10693_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21386_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21386_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21386_1)).]
[fof(genFunction_21387_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42774_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85548_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85548_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85548_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).]
[fof(genFunction_171096_1,theorem,~ (mth162),beta1(genFunction_334_1)).,
fof(contradict_171096_1,theorem,(mth162 & ~ (mth162)),contraction(mth162,genFunction_171096_1)).]
[fof(genFunction_171097_1,theorem,~ ((cscXXX | staXXX)),beta2(genFunction_334_1)).,
fof(genFunction_171097_1,theorem,~ (((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX)),alpha1(genFunction_668_1)).,
fof(genFunction_171097_2,theorem,~ (socXXX),alpha2(genFunction_668_1)).,
fof(genFunction_171097_3,theorem,~ ((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX)),alpha1(genFunction_1336_1)).,
fof(genFunction_171097_4,theorem,~ (spa2XX),alpha2(genFunction_1336_1)).]
[fof(genFunction_342194_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42774_1)).]
[fof(genFunction_684388_1,theorem,~ ((art & literature)),beta1(genFunction_85548_1)).,
fof(genFunction_684388_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85548_1)).,
fof(genFunction_684388_2,theorem,~ (mcyXXX),alpha2(genFunction_85548_1)).,
fof(genFunction_684388_3,theorem,~ (cscXXX),alpha1(genFunction_171097_1)).,
fof(contradict_684388_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_684388_3)).]
[fof(genFunction_684389_1,theorem,~ (religion),beta2(genFunction_85548_1)).,
fof(contradict_684389_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_684389_1)).]
[fof(genFunction_342195_1,theorem,~ (language),beta2(genFunction_42774_1)).]
[fof(genFunction_684390_1,theorem,~ ((art & literature)),beta1(genFunction_85548_1)).,
fof(genFunction_684390_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85548_1)).,
fof(genFunction_684390_2,theorem,~ (mcyXXX),alpha2(genFunction_85548_1)).,
fof(genFunction_684390_3,theorem,~ (cscXXX),alpha1(genFunction_171097_1)).,
fof(contradict_684390_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_684390_3)).]
[fof(genFunction_684391_1,theorem,~ (religion),beta2(genFunction_85548_1)).,
fof(contradict_684391_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_684391_1)).]
[fof(genFunction_85549_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85549_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85549_1)).]
[fof(genFunction_42775_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42775_1,theorem,(writing & ~ (writing)),contraction(genFunction_10693_1,genFunction_42775_1)).]
[fof(genFunction_5347_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10694_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10694_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10694_1)).]
[fof(genFunction_10695_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21390_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21390_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21390_1)).]
[fof(genFunction_21391_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42782_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85564_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85564_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85564_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).]
[fof(genFunction_171128_1,theorem,~ (mth162),beta1(genFunction_334_1)).,
fof(contradict_171128_1,theorem,(mth162 & ~ (mth162)),contraction(mth162,genFunction_171128_1)).]
[fof(genFunction_171129_1,theorem,~ ((cscXXX | staXXX)),beta2(genFunction_334_1)).,
fof(genFunction_171129_1,theorem,~ (((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX)),alpha1(genFunction_668_1)).,
fof(genFunction_171129_2,theorem,~ (socXXX),alpha2(genFunction_668_1)).,
fof(genFunction_171129_3,theorem,~ ((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX)),alpha1(genFunction_1336_1)).,
fof(genFunction_171129_4,theorem,~ (spa2XX),alpha2(genFunction_1336_1)).]
[fof(genFunction_342258_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42782_1)).]
[fof(genFunction_684516_1,theorem,~ ((art & literature)),beta1(genFunction_85564_1)).,
fof(genFunction_684516_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85564_1)).,
fof(genFunction_684516_2,theorem,~ (mcyXXX),alpha2(genFunction_85564_1)).,
fof(genFunction_684516_3,theorem,~ (cscXXX),alpha1(genFunction_171129_1)).,
fof(contradict_684516_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_684516_3)).]
[fof(genFunction_684517_1,theorem,~ (religion),beta2(genFunction_85564_1)).,
fof(contradict_684517_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_684517_1)).]
[fof(genFunction_342259_1,theorem,~ (language),beta2(genFunction_42782_1)).]
[fof(genFunction_684518_1,theorem,~ ((art & literature)),beta1(genFunction_85564_1)).,
fof(genFunction_684518_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85564_1)).,
fof(genFunction_684518_2,theorem,~ (mcyXXX),alpha2(genFunction_85564_1)).,
fof(genFunction_684518_3,theorem,~ (cscXXX),alpha1(genFunction_171129_1)).,
fof(contradict_684518_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_684518_3)).]
[fof(genFunction_684519_1,theorem,~ (religion),beta2(genFunction_85564_1)).,
fof(contradict_684519_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_684519_1)).]
[fof(genFunction_85565_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85565_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85565_1)).]
[fof(genFunction_42783_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42783_1,theorem,(writing & ~ (writing)),contraction(genFunction_10695_1,genFunction_42783_1)).]
[fof(genFunction_1337_1,theorem,language,beta2(language)).]
[fof(genFunction_2674_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2674_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2674_1)).]
[fof(genFunction_2675_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5350_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10700_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10700_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10700_1)).]
[fof(genFunction_10701_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21402_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21402_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21402_1)).]
[fof(genFunction_21403_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42806_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85612_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85612_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85612_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).]
[fof(genFunction_171224_1,theorem,~ (mth162),beta1(genFunction_334_1)).,
fof(contradict_171224_1,theorem,(mth162 & ~ (mth162)),contraction(mth162,genFunction_171224_1)).]
[fof(genFunction_171225_1,theorem,~ ((cscXXX | staXXX)),beta2(genFunction_334_1)).,
fof(genFunction_171225_1,theorem,~ (((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX)),alpha1(genFunction_668_1)).,
fof(genFunction_171225_2,theorem,~ (socXXX),alpha2(genFunction_668_1)).]
[fof(genFunction_342450_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42806_1)).]
[fof(genFunction_684900_1,theorem,~ ((art & literature)),beta1(genFunction_85612_1)).,
fof(genFunction_684900_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85612_1)).,
fof(genFunction_684900_2,theorem,~ (mcyXXX),alpha2(genFunction_85612_1)).,
fof(genFunction_684900_3,theorem,~ (cscXXX),alpha1(genFunction_171225_1)).,
fof(contradict_684900_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_684900_3)).]
[fof(genFunction_684901_1,theorem,~ (religion),beta2(genFunction_85612_1)).,
fof(contradict_684901_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_684901_1)).]
[fof(genFunction_342451_1,theorem,~ (language),beta2(genFunction_42806_1)).,
fof(contradict_342451_1,theorem,(language & ~ (language)),contraction(genFunction_1337_1,genFunction_342451_1)).]
[fof(genFunction_85613_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85613_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85613_1)).]
[fof(genFunction_42807_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42807_1,theorem,(writing & ~ (writing)),contraction(genFunction_10701_1,genFunction_42807_1)).]
[fof(genFunction_5351_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10702_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10702_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10702_1)).]
[fof(genFunction_10703_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21406_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21406_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21406_1)).]
[fof(genFunction_21407_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42814_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85628_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85628_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85628_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).]
[fof(genFunction_171256_1,theorem,~ (mth162),beta1(genFunction_334_1)).,
fof(contradict_171256_1,theorem,(mth162 & ~ (mth162)),contraction(mth162,genFunction_171256_1)).]
[fof(genFunction_171257_1,theorem,~ ((cscXXX | staXXX)),beta2(genFunction_334_1)).,
fof(genFunction_171257_1,theorem,~ (((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX)),alpha1(genFunction_668_1)).,
fof(genFunction_171257_2,theorem,~ (socXXX),alpha2(genFunction_668_1)).]
[fof(genFunction_342514_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42814_1)).]
[fof(genFunction_685028_1,theorem,~ ((art & literature)),beta1(genFunction_85628_1)).,
fof(genFunction_685028_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85628_1)).,
fof(genFunction_685028_2,theorem,~ (mcyXXX),alpha2(genFunction_85628_1)).,
fof(genFunction_685028_3,theorem,~ (cscXXX),alpha1(genFunction_171257_1)).,
fof(contradict_685028_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_685028_3)).]
[fof(genFunction_685029_1,theorem,~ (religion),beta2(genFunction_85628_1)).,
fof(contradict_685029_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_685029_1)).]
[fof(genFunction_342515_1,theorem,~ (language),beta2(genFunction_42814_1)).,
fof(contradict_342515_1,theorem,(language & ~ (language)),contraction(genFunction_1337_1,genFunction_342515_1)).]
[fof(genFunction_85629_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85629_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85629_1)).]
[fof(genFunction_42815_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42815_1,theorem,(writing & ~ (writing)),contraction(genFunction_10703_1,genFunction_42815_1)).]
[fof(genFunction_669_1,theorem,social_science,beta2(social_science)).]
[fof(genFunction_1338_1,theorem,~ (((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX) | spa2XX)),beta1(language)).]
[fof(genFunction_2676_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2676_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2676_1)).]
[fof(genFunction_2677_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5354_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10708_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10708_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10708_1)).]
[fof(genFunction_10709_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21418_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21418_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21418_1)).]
[fof(genFunction_21419_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42838_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85676_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85676_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85676_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).]
[fof(genFunction_171352_1,theorem,~ (mth162),beta1(genFunction_334_1)).,
fof(contradict_171352_1,theorem,(mth162 & ~ (mth162)),contraction(mth162,genFunction_171352_1)).]
[fof(genFunction_171353_1,theorem,~ ((cscXXX | staXXX)),beta2(genFunction_334_1)).,
fof(genFunction_171353_1,theorem,~ ((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX)),alpha1(genFunction_1338_1)).,
fof(genFunction_171353_2,theorem,~ (spa2XX),alpha2(genFunction_1338_1)).]
[fof(genFunction_342706_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42838_1)).]
[fof(genFunction_685412_1,theorem,~ ((art & literature)),beta1(genFunction_85676_1)).,
fof(genFunction_685412_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85676_1)).,
fof(genFunction_685412_2,theorem,~ (mcyXXX),alpha2(genFunction_85676_1)).,
fof(genFunction_685412_3,theorem,~ (cscXXX),alpha1(genFunction_171353_1)).,
fof(contradict_685412_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_685412_3)).]
[fof(genFunction_685413_1,theorem,~ (religion),beta2(genFunction_85676_1)).,
fof(contradict_685413_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_685413_1)).]
[fof(genFunction_342707_1,theorem,~ (language),beta2(genFunction_42838_1)).]
[fof(genFunction_685414_1,theorem,~ ((art & literature)),beta1(genFunction_85676_1)).,
fof(genFunction_685414_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85676_1)).,
fof(genFunction_685414_2,theorem,~ (mcyXXX),alpha2(genFunction_85676_1)).,
fof(genFunction_685414_3,theorem,~ (cscXXX),alpha1(genFunction_171353_1)).,
fof(contradict_685414_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_685414_3)).]
[fof(genFunction_685415_1,theorem,~ (religion),beta2(genFunction_85676_1)).,
fof(contradict_685415_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_685415_1)).]
[fof(genFunction_85677_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85677_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85677_1)).]
[fof(genFunction_42839_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42839_1,theorem,(writing & ~ (writing)),contraction(genFunction_10709_1,genFunction_42839_1)).]
[fof(genFunction_5355_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10710_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10710_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10710_1)).]
[fof(genFunction_10711_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21422_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21422_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21422_1)).]
[fof(genFunction_21423_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42846_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85692_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85692_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85692_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).]
[fof(genFunction_171384_1,theorem,~ (mth162),beta1(genFunction_334_1)).,
fof(contradict_171384_1,theorem,(mth162 & ~ (mth162)),contraction(mth162,genFunction_171384_1)).]
[fof(genFunction_171385_1,theorem,~ ((cscXXX | staXXX)),beta2(genFunction_334_1)).,
fof(genFunction_171385_1,theorem,~ ((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX)),alpha1(genFunction_1338_1)).,
fof(genFunction_171385_2,theorem,~ (spa2XX),alpha2(genFunction_1338_1)).]
[fof(genFunction_342770_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42846_1)).]
[fof(genFunction_685540_1,theorem,~ ((art & literature)),beta1(genFunction_85692_1)).,
fof(genFunction_685540_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85692_1)).,
fof(genFunction_685540_2,theorem,~ (mcyXXX),alpha2(genFunction_85692_1)).,
fof(genFunction_685540_3,theorem,~ (cscXXX),alpha1(genFunction_171385_1)).,
fof(contradict_685540_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_685540_3)).]
[fof(genFunction_685541_1,theorem,~ (religion),beta2(genFunction_85692_1)).,
fof(contradict_685541_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_685541_1)).]
[fof(genFunction_342771_1,theorem,~ (language),beta2(genFunction_42846_1)).]
[fof(genFunction_685542_1,theorem,~ ((art & literature)),beta1(genFunction_85692_1)).,
fof(genFunction_685542_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85692_1)).,
fof(genFunction_685542_2,theorem,~ (mcyXXX),alpha2(genFunction_85692_1)).,
fof(genFunction_685542_3,theorem,~ (cscXXX),alpha1(genFunction_171385_1)).,
fof(contradict_685542_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_685542_3)).]
[fof(genFunction_685543_1,theorem,~ (religion),beta2(genFunction_85692_1)).,
fof(contradict_685543_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_685543_1)).]
[fof(genFunction_85693_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85693_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85693_1)).]
[fof(genFunction_42847_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42847_1,theorem,(writing & ~ (writing)),contraction(genFunction_10711_1,genFunction_42847_1)).]
[fof(genFunction_1339_1,theorem,language,beta2(language)).]
[fof(genFunction_2678_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2678_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2678_1)).]
[fof(genFunction_2679_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5358_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10716_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10716_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10716_1)).]
[fof(genFunction_10717_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21434_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21434_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21434_1)).]
[fof(genFunction_21435_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42870_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85740_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85740_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85740_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).]
[fof(genFunction_171480_1,theorem,~ (mth162),beta1(genFunction_334_1)).,
fof(contradict_171480_1,theorem,(mth162 & ~ (mth162)),contraction(mth162,genFunction_171480_1)).]
[fof(genFunction_171481_1,theorem,~ ((cscXXX | staXXX)),beta2(genFunction_334_1)).]
[fof(genFunction_342962_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42870_1)).]
[fof(genFunction_685924_1,theorem,~ ((art & literature)),beta1(genFunction_85740_1)).,
fof(genFunction_685924_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85740_1)).,
fof(genFunction_685924_2,theorem,~ (mcyXXX),alpha2(genFunction_85740_1)).,
fof(genFunction_685924_3,theorem,~ (cscXXX),alpha1(genFunction_171481_1)).,
fof(contradict_685924_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_685924_3)).]
[fof(genFunction_685925_1,theorem,~ (religion),beta2(genFunction_85740_1)).,
fof(contradict_685925_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_685925_1)).]
[fof(genFunction_342963_1,theorem,~ (language),beta2(genFunction_42870_1)).,
fof(contradict_342963_1,theorem,(language & ~ (language)),contraction(genFunction_1339_1,genFunction_342963_1)).]
[fof(genFunction_85741_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85741_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85741_1)).]
[fof(genFunction_42871_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42871_1,theorem,(writing & ~ (writing)),contraction(genFunction_10717_1,genFunction_42871_1)).]
[fof(genFunction_5359_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10718_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10718_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10718_1)).]
[fof(genFunction_10719_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21438_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21438_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21438_1)).]
[fof(genFunction_21439_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42878_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85756_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85756_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85756_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).]
[fof(genFunction_171512_1,theorem,~ (mth162),beta1(genFunction_334_1)).,
fof(contradict_171512_1,theorem,(mth162 & ~ (mth162)),contraction(mth162,genFunction_171512_1)).]
[fof(genFunction_171513_1,theorem,~ ((cscXXX | staXXX)),beta2(genFunction_334_1)).]
[fof(genFunction_343026_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42878_1)).]
[fof(genFunction_686052_1,theorem,~ ((art & literature)),beta1(genFunction_85756_1)).,
fof(genFunction_686052_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85756_1)).,
fof(genFunction_686052_2,theorem,~ (mcyXXX),alpha2(genFunction_85756_1)).,
fof(genFunction_686052_3,theorem,~ (cscXXX),alpha1(genFunction_171513_1)).,
fof(contradict_686052_3,theorem,(cscXXX & ~ (cscXXX)),contraction(cscXXX,genFunction_686052_3)).]
[fof(genFunction_686053_1,theorem,~ (religion),beta2(genFunction_85756_1)).,
fof(contradict_686053_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_686053_1)).]
[fof(genFunction_343027_1,theorem,~ (language),beta2(genFunction_42878_1)).,
fof(contradict_343027_1,theorem,(language & ~ (language)),contraction(genFunction_1339_1,genFunction_343027_1)).]
[fof(genFunction_85757_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85757_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85757_1)).]
[fof(genFunction_42879_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42879_1,theorem,(writing & ~ (writing)),contraction(genFunction_10719_1,genFunction_42879_1)).]
[fof(genFunction_335_1,theorem,math,beta2(math)).]
[fof(genFunction_670_1,theorem,~ ((((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX) | socXXX)),beta1(social_science)).]
[fof(genFunction_1340_1,theorem,~ (((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX) | spa2XX)),beta1(language)).]
[fof(genFunction_2680_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2680_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2680_1)).]
[fof(genFunction_2681_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5362_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10724_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10724_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10724_1)).]
[fof(genFunction_10725_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21450_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21450_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21450_1)).]
[fof(genFunction_21451_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42902_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85804_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85804_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85804_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85804_3,theorem,~ (((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX)),alpha1(genFunction_670_1)).,
fof(genFunction_85804_4,theorem,~ (socXXX),alpha2(genFunction_670_1)).,
fof(genFunction_85804_5,theorem,~ ((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX)),alpha1(genFunction_1340_1)).,
fof(genFunction_85804_6,theorem,~ (spa2XX),alpha2(genFunction_1340_1)).]
[fof(genFunction_171608_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42902_1)).]
[fof(genFunction_343216_1,theorem,~ ((art & literature)),beta1(genFunction_85804_1)).,
fof(genFunction_343216_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85804_1)).,
fof(genFunction_343216_2,theorem,~ (mcyXXX),alpha2(genFunction_85804_1)).,
fof(genFunction_343216_3,theorem,~ ((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX)),alpha1(genFunction_85804_3)).,
fof(genFunction_343216_4,theorem,~ (psyXXX),alpha2(genFunction_85804_3)).,
fof(genFunction_343216_5,theorem,~ (((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX)),alpha1(genFunction_85804_5)).,
fof(genFunction_343216_6,theorem,~ (por2XX),alpha2(genFunction_85804_5)).]
[fof(genFunction_686432_1,theorem,~ ((((composition & humanities) & science) & math)),beta1(genFunction_171608_1)).]
[fof(genFunction_1372864_1,theorem,~ (art),beta1(genFunction_343216_1)).,
fof(genFunction_1372864_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343216_1)).,
fof(genFunction_1372864_2,theorem,~ (danXXX),alpha2(genFunction_343216_1)).,
fof(genFunction_1372864_3,theorem,~ (((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX)),alpha1(genFunction_343216_3)).,
fof(genFunction_1372864_4,theorem,~ (polXXX),alpha2(genFunction_343216_3)).,
fof(genFunction_1372864_5,theorem,~ ((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX)),alpha1(genFunction_343216_5)).,
fof(genFunction_1372864_6,theorem,~ (lat2XX),alpha2(genFunction_343216_5)).]
[fof(genFunction_2745728_1,theorem,~ (((composition & humanities) & science)),beta1(genFunction_686432_1)).,
fof(genFunction_2745728_1,theorem,~ (artXXX),alpha1(genFunction_1372864_1)).,
fof(contradict_2745728_1,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_2745728_1)).]
[fof(genFunction_2745729_1,theorem,~ (math),beta2(genFunction_686432_1)).,
fof(contradict_2745729_1,theorem,(math & ~ (math)),contraction(genFunction_335_1,genFunction_2745729_1)).]
[fof(genFunction_1372865_1,theorem,~ (literature),beta2(genFunction_343216_1)).,
fof(contradict_1372865_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_1372865_1)).]
[fof(genFunction_686433_1,theorem,~ (social_science),beta2(genFunction_171608_1)).]
[fof(genFunction_1372866_1,theorem,~ (art),beta1(genFunction_343216_1)).,
fof(genFunction_1372866_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343216_1)).,
fof(genFunction_1372866_2,theorem,~ (danXXX),alpha2(genFunction_343216_1)).,
fof(genFunction_1372866_3,theorem,~ (((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX)),alpha1(genFunction_343216_3)).,
fof(genFunction_1372866_4,theorem,~ (polXXX),alpha2(genFunction_343216_3)).,
fof(genFunction_1372866_5,theorem,~ ((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX)),alpha1(genFunction_343216_5)).,
fof(genFunction_1372866_6,theorem,~ (lat2XX),alpha2(genFunction_343216_5)).,
fof(genFunction_1372866_7,theorem,~ (artXXX),alpha1(genFunction_1372866_1)).,
fof(contradict_1372866_7,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_1372866_7)).]
[fof(genFunction_1372867_1,theorem,~ (literature),beta2(genFunction_343216_1)).,
fof(contradict_1372867_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_1372867_1)).]
[fof(genFunction_343217_1,theorem,~ (religion),beta2(genFunction_85804_1)).,
fof(contradict_343217_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_343217_1)).]
[fof(genFunction_171609_1,theorem,~ (language),beta2(genFunction_42902_1)).]
[fof(genFunction_343218_1,theorem,~ ((art & literature)),beta1(genFunction_85804_1)).,
fof(genFunction_343218_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85804_1)).,
fof(genFunction_343218_2,theorem,~ (mcyXXX),alpha2(genFunction_85804_1)).,
fof(genFunction_343218_3,theorem,~ ((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX)),alpha1(genFunction_85804_3)).,
fof(genFunction_343218_4,theorem,~ (psyXXX),alpha2(genFunction_85804_3)).,
fof(genFunction_343218_5,theorem,~ (((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX)),alpha1(genFunction_85804_5)).,
fof(genFunction_343218_6,theorem,~ (por2XX),alpha2(genFunction_85804_5)).]
[fof(genFunction_686436_1,theorem,~ (art),beta1(genFunction_343218_1)).,
fof(genFunction_686436_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343218_1)).,
fof(genFunction_686436_2,theorem,~ (danXXX),alpha2(genFunction_343218_1)).,
fof(genFunction_686436_3,theorem,~ (((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX)),alpha1(genFunction_343218_3)).,
fof(genFunction_686436_4,theorem,~ (polXXX),alpha2(genFunction_343218_3)).,
fof(genFunction_686436_5,theorem,~ ((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX)),alpha1(genFunction_343218_5)).,
fof(genFunction_686436_6,theorem,~ (lat2XX),alpha2(genFunction_343218_5)).,
fof(genFunction_686436_7,theorem,~ (artXXX),alpha1(genFunction_686436_1)).,
fof(contradict_686436_7,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_686436_7)).]
[fof(genFunction_686437_1,theorem,~ (literature),beta2(genFunction_343218_1)).,
fof(contradict_686437_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_686437_1)).]
[fof(genFunction_343219_1,theorem,~ (religion),beta2(genFunction_85804_1)).,
fof(contradict_343219_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_343219_1)).]
[fof(genFunction_85805_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85805_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85805_1)).]
[fof(genFunction_42903_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42903_1,theorem,(writing & ~ (writing)),contraction(genFunction_10725_1,genFunction_42903_1)).]
[fof(genFunction_5363_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10726_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10726_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10726_1)).]
[fof(genFunction_10727_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21454_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21454_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21454_1)).]
[fof(genFunction_21455_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42910_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85820_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85820_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85820_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85820_3,theorem,~ (((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX)),alpha1(genFunction_670_1)).,
fof(genFunction_85820_4,theorem,~ (socXXX),alpha2(genFunction_670_1)).,
fof(genFunction_85820_5,theorem,~ ((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX)),alpha1(genFunction_1340_1)).,
fof(genFunction_85820_6,theorem,~ (spa2XX),alpha2(genFunction_1340_1)).]
[fof(genFunction_171640_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42910_1)).]
[fof(genFunction_343280_1,theorem,~ ((art & literature)),beta1(genFunction_85820_1)).,
fof(genFunction_343280_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85820_1)).,
fof(genFunction_343280_2,theorem,~ (mcyXXX),alpha2(genFunction_85820_1)).,
fof(genFunction_343280_3,theorem,~ ((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX)),alpha1(genFunction_85820_3)).,
fof(genFunction_343280_4,theorem,~ (psyXXX),alpha2(genFunction_85820_3)).,
fof(genFunction_343280_5,theorem,~ (((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX)),alpha1(genFunction_85820_5)).,
fof(genFunction_343280_6,theorem,~ (por2XX),alpha2(genFunction_85820_5)).]
[fof(genFunction_686560_1,theorem,~ ((((composition & humanities) & science) & math)),beta1(genFunction_171640_1)).]
[fof(genFunction_1373120_1,theorem,~ (art),beta1(genFunction_343280_1)).,
fof(genFunction_1373120_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343280_1)).,
fof(genFunction_1373120_2,theorem,~ (danXXX),alpha2(genFunction_343280_1)).,
fof(genFunction_1373120_3,theorem,~ (((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX)),alpha1(genFunction_343280_3)).,
fof(genFunction_1373120_4,theorem,~ (polXXX),alpha2(genFunction_343280_3)).,
fof(genFunction_1373120_5,theorem,~ ((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX)),alpha1(genFunction_343280_5)).,
fof(genFunction_1373120_6,theorem,~ (lat2XX),alpha2(genFunction_343280_5)).]
[fof(genFunction_2746240_1,theorem,~ (((composition & humanities) & science)),beta1(genFunction_686560_1)).,
fof(genFunction_2746240_1,theorem,~ (artXXX),alpha1(genFunction_1373120_1)).,
fof(contradict_2746240_1,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_2746240_1)).]
[fof(genFunction_2746241_1,theorem,~ (math),beta2(genFunction_686560_1)).,
fof(contradict_2746241_1,theorem,(math & ~ (math)),contraction(genFunction_335_1,genFunction_2746241_1)).]
[fof(genFunction_1373121_1,theorem,~ (literature),beta2(genFunction_343280_1)).,
fof(contradict_1373121_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_1373121_1)).]
[fof(genFunction_686561_1,theorem,~ (social_science),beta2(genFunction_171640_1)).]
[fof(genFunction_1373122_1,theorem,~ (art),beta1(genFunction_343280_1)).,
fof(genFunction_1373122_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343280_1)).,
fof(genFunction_1373122_2,theorem,~ (danXXX),alpha2(genFunction_343280_1)).,
fof(genFunction_1373122_3,theorem,~ (((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX)),alpha1(genFunction_343280_3)).,
fof(genFunction_1373122_4,theorem,~ (polXXX),alpha2(genFunction_343280_3)).,
fof(genFunction_1373122_5,theorem,~ ((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX)),alpha1(genFunction_343280_5)).,
fof(genFunction_1373122_6,theorem,~ (lat2XX),alpha2(genFunction_343280_5)).,
fof(genFunction_1373122_7,theorem,~ (artXXX),alpha1(genFunction_1373122_1)).,
fof(contradict_1373122_7,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_1373122_7)).]
[fof(genFunction_1373123_1,theorem,~ (literature),beta2(genFunction_343280_1)).,
fof(contradict_1373123_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_1373123_1)).]
[fof(genFunction_343281_1,theorem,~ (religion),beta2(genFunction_85820_1)).,
fof(contradict_343281_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_343281_1)).]
[fof(genFunction_171641_1,theorem,~ (language),beta2(genFunction_42910_1)).]
[fof(genFunction_343282_1,theorem,~ ((art & literature)),beta1(genFunction_85820_1)).,
fof(genFunction_343282_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85820_1)).,
fof(genFunction_343282_2,theorem,~ (mcyXXX),alpha2(genFunction_85820_1)).,
fof(genFunction_343282_3,theorem,~ ((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX)),alpha1(genFunction_85820_3)).,
fof(genFunction_343282_4,theorem,~ (psyXXX),alpha2(genFunction_85820_3)).,
fof(genFunction_343282_5,theorem,~ (((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX)),alpha1(genFunction_85820_5)).,
fof(genFunction_343282_6,theorem,~ (por2XX),alpha2(genFunction_85820_5)).]
[fof(genFunction_686564_1,theorem,~ (art),beta1(genFunction_343282_1)).,
fof(genFunction_686564_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343282_1)).,
fof(genFunction_686564_2,theorem,~ (danXXX),alpha2(genFunction_343282_1)).,
fof(genFunction_686564_3,theorem,~ (((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX)),alpha1(genFunction_343282_3)).,
fof(genFunction_686564_4,theorem,~ (polXXX),alpha2(genFunction_343282_3)).,
fof(genFunction_686564_5,theorem,~ ((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX)),alpha1(genFunction_343282_5)).,
fof(genFunction_686564_6,theorem,~ (lat2XX),alpha2(genFunction_343282_5)).,
fof(genFunction_686564_7,theorem,~ (artXXX),alpha1(genFunction_686564_1)).,
fof(contradict_686564_7,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_686564_7)).]
[fof(genFunction_686565_1,theorem,~ (literature),beta2(genFunction_343282_1)).,
fof(contradict_686565_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_686565_1)).]
[fof(genFunction_343283_1,theorem,~ (religion),beta2(genFunction_85820_1)).,
fof(contradict_343283_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_343283_1)).]
[fof(genFunction_85821_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85821_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85821_1)).]
[fof(genFunction_42911_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42911_1,theorem,(writing & ~ (writing)),contraction(genFunction_10727_1,genFunction_42911_1)).]
[fof(genFunction_1341_1,theorem,language,beta2(language)).]
[fof(genFunction_2682_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2682_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2682_1)).]
[fof(genFunction_2683_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5366_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10732_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10732_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10732_1)).]
[fof(genFunction_10733_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21466_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21466_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21466_1)).]
[fof(genFunction_21467_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42934_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85868_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85868_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85868_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85868_3,theorem,~ (((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX)),alpha1(genFunction_670_1)).,
fof(genFunction_85868_4,theorem,~ (socXXX),alpha2(genFunction_670_1)).]
[fof(genFunction_171736_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42934_1)).]
[fof(genFunction_343472_1,theorem,~ ((art & literature)),beta1(genFunction_85868_1)).,
fof(genFunction_343472_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85868_1)).,
fof(genFunction_343472_2,theorem,~ (mcyXXX),alpha2(genFunction_85868_1)).,
fof(genFunction_343472_3,theorem,~ ((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX)),alpha1(genFunction_85868_3)).,
fof(genFunction_343472_4,theorem,~ (psyXXX),alpha2(genFunction_85868_3)).]
[fof(genFunction_686944_1,theorem,~ ((((composition & humanities) & science) & math)),beta1(genFunction_171736_1)).]
[fof(genFunction_1373888_1,theorem,~ (art),beta1(genFunction_343472_1)).,
fof(genFunction_1373888_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343472_1)).,
fof(genFunction_1373888_2,theorem,~ (danXXX),alpha2(genFunction_343472_1)).,
fof(genFunction_1373888_3,theorem,~ (((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX)),alpha1(genFunction_343472_3)).,
fof(genFunction_1373888_4,theorem,~ (polXXX),alpha2(genFunction_343472_3)).]
[fof(genFunction_2747776_1,theorem,~ (((composition & humanities) & science)),beta1(genFunction_686944_1)).,
fof(genFunction_2747776_1,theorem,~ (artXXX),alpha1(genFunction_1373888_1)).,
fof(contradict_2747776_1,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_2747776_1)).]
[fof(genFunction_2747777_1,theorem,~ (math),beta2(genFunction_686944_1)).,
fof(contradict_2747777_1,theorem,(math & ~ (math)),contraction(genFunction_335_1,genFunction_2747777_1)).]
[fof(genFunction_1373889_1,theorem,~ (literature),beta2(genFunction_343472_1)).,
fof(contradict_1373889_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_1373889_1)).]
[fof(genFunction_686945_1,theorem,~ (social_science),beta2(genFunction_171736_1)).]
[fof(genFunction_1373890_1,theorem,~ (art),beta1(genFunction_343472_1)).,
fof(genFunction_1373890_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343472_1)).,
fof(genFunction_1373890_2,theorem,~ (danXXX),alpha2(genFunction_343472_1)).,
fof(genFunction_1373890_3,theorem,~ (((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX)),alpha1(genFunction_343472_3)).,
fof(genFunction_1373890_4,theorem,~ (polXXX),alpha2(genFunction_343472_3)).,
fof(genFunction_1373890_5,theorem,~ (artXXX),alpha1(genFunction_1373890_1)).,
fof(contradict_1373890_5,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_1373890_5)).]
[fof(genFunction_1373891_1,theorem,~ (literature),beta2(genFunction_343472_1)).,
fof(contradict_1373891_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_1373891_1)).]
[fof(genFunction_343473_1,theorem,~ (religion),beta2(genFunction_85868_1)).,
fof(contradict_343473_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_343473_1)).]
[fof(genFunction_171737_1,theorem,~ (language),beta2(genFunction_42934_1)).,
fof(contradict_171737_1,theorem,(language & ~ (language)),contraction(genFunction_1341_1,genFunction_171737_1)).]
[fof(genFunction_85869_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85869_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85869_1)).]
[fof(genFunction_42935_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42935_1,theorem,(writing & ~ (writing)),contraction(genFunction_10733_1,genFunction_42935_1)).]
[fof(genFunction_5367_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10734_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10734_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10734_1)).]
[fof(genFunction_10735_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21470_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21470_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21470_1)).]
[fof(genFunction_21471_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42942_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85884_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85884_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85884_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85884_3,theorem,~ (((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX) | psyXXX)),alpha1(genFunction_670_1)).,
fof(genFunction_85884_4,theorem,~ (socXXX),alpha2(genFunction_670_1)).]
[fof(genFunction_171768_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42942_1)).]
[fof(genFunction_343536_1,theorem,~ ((art & literature)),beta1(genFunction_85884_1)).,
fof(genFunction_343536_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85884_1)).,
fof(genFunction_343536_2,theorem,~ (mcyXXX),alpha2(genFunction_85884_1)).,
fof(genFunction_343536_3,theorem,~ ((((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX) | polXXX)),alpha1(genFunction_85884_3)).,
fof(genFunction_343536_4,theorem,~ (psyXXX),alpha2(genFunction_85884_3)).]
[fof(genFunction_687072_1,theorem,~ ((((composition & humanities) & science) & math)),beta1(genFunction_171768_1)).]
[fof(genFunction_1374144_1,theorem,~ (art),beta1(genFunction_343536_1)).,
fof(genFunction_1374144_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343536_1)).,
fof(genFunction_1374144_2,theorem,~ (danXXX),alpha2(genFunction_343536_1)).,
fof(genFunction_1374144_3,theorem,~ (((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX)),alpha1(genFunction_343536_3)).,
fof(genFunction_1374144_4,theorem,~ (polXXX),alpha2(genFunction_343536_3)).]
[fof(genFunction_2748288_1,theorem,~ (((composition & humanities) & science)),beta1(genFunction_687072_1)).,
fof(genFunction_2748288_1,theorem,~ (artXXX),alpha1(genFunction_1374144_1)).,
fof(contradict_2748288_1,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_2748288_1)).]
[fof(genFunction_2748289_1,theorem,~ (math),beta2(genFunction_687072_1)).,
fof(contradict_2748289_1,theorem,(math & ~ (math)),contraction(genFunction_335_1,genFunction_2748289_1)).]
[fof(genFunction_1374145_1,theorem,~ (literature),beta2(genFunction_343536_1)).,
fof(contradict_1374145_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_1374145_1)).]
[fof(genFunction_687073_1,theorem,~ (social_science),beta2(genFunction_171768_1)).]
[fof(genFunction_1374146_1,theorem,~ (art),beta1(genFunction_343536_1)).,
fof(genFunction_1374146_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343536_1)).,
fof(genFunction_1374146_2,theorem,~ (danXXX),alpha2(genFunction_343536_1)).,
fof(genFunction_1374146_3,theorem,~ (((((apyXXX | ecoXXX) | gegXXX) | hisXXX) | intXXX)),alpha1(genFunction_343536_3)).,
fof(genFunction_1374146_4,theorem,~ (polXXX),alpha2(genFunction_343536_3)).,
fof(genFunction_1374146_5,theorem,~ (artXXX),alpha1(genFunction_1374146_1)).,
fof(contradict_1374146_5,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_1374146_5)).]
[fof(genFunction_1374147_1,theorem,~ (literature),beta2(genFunction_343536_1)).,
fof(contradict_1374147_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_1374147_1)).]
[fof(genFunction_343537_1,theorem,~ (religion),beta2(genFunction_85884_1)).,
fof(contradict_343537_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_343537_1)).]
[fof(genFunction_171769_1,theorem,~ (language),beta2(genFunction_42942_1)).,
fof(contradict_171769_1,theorem,(language & ~ (language)),contraction(genFunction_1341_1,genFunction_171769_1)).]
[fof(genFunction_85885_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85885_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85885_1)).]
[fof(genFunction_42943_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42943_1,theorem,(writing & ~ (writing)),contraction(genFunction_10735_1,genFunction_42943_1)).]
[fof(genFunction_671_1,theorem,social_science,beta2(social_science)).]
[fof(genFunction_1342_1,theorem,~ (((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX) | spa2XX)),beta1(language)).]
[fof(genFunction_2684_1,theorem,~ (wwwXXX),beta1(wwwXXX_writing)).,
fof(contradict_2684_1,theorem,(wwwXXX & ~ (wwwXXX)),contraction(wwwXXX,genFunction_2684_1)).]
[fof(genFunction_2685_1,theorem,writing,beta2(wwwXXX_writing)).]
[fof(genFunction_5370_1,theorem,~ (hisXXX),beta1(hisXXX_writing)).]
[fof(genFunction_10740_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10740_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10740_1)).]
[fof(genFunction_10741_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21482_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21482_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21482_1)).]
[fof(genFunction_21483_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42966_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85932_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85932_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85932_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85932_3,theorem,~ ((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX)),alpha1(genFunction_1342_1)).,
fof(genFunction_85932_4,theorem,~ (spa2XX),alpha2(genFunction_1342_1)).]
[fof(genFunction_171864_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42966_1)).]
[fof(genFunction_343728_1,theorem,~ ((art & literature)),beta1(genFunction_85932_1)).,
fof(genFunction_343728_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85932_1)).,
fof(genFunction_343728_2,theorem,~ (mcyXXX),alpha2(genFunction_85932_1)).,
fof(genFunction_343728_3,theorem,~ (((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX)),alpha1(genFunction_85932_3)).,
fof(genFunction_343728_4,theorem,~ (por2XX),alpha2(genFunction_85932_3)).]
[fof(genFunction_687456_1,theorem,~ ((((composition & humanities) & science) & math)),beta1(genFunction_171864_1)).]
[fof(genFunction_1374912_1,theorem,~ (art),beta1(genFunction_343728_1)).,
fof(genFunction_1374912_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343728_1)).,
fof(genFunction_1374912_2,theorem,~ (danXXX),alpha2(genFunction_343728_1)).,
fof(genFunction_1374912_3,theorem,~ ((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX)),alpha1(genFunction_343728_3)).,
fof(genFunction_1374912_4,theorem,~ (lat2XX),alpha2(genFunction_343728_3)).]
[fof(genFunction_2749824_1,theorem,~ (((composition & humanities) & science)),beta1(genFunction_687456_1)).,
fof(genFunction_2749824_1,theorem,~ (artXXX),alpha1(genFunction_1374912_1)).,
fof(contradict_2749824_1,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_2749824_1)).]
[fof(genFunction_2749825_1,theorem,~ (math),beta2(genFunction_687456_1)).,
fof(contradict_2749825_1,theorem,(math & ~ (math)),contraction(genFunction_335_1,genFunction_2749825_1)).]
[fof(genFunction_1374913_1,theorem,~ (literature),beta2(genFunction_343728_1)).,
fof(contradict_1374913_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_1374913_1)).]
[fof(genFunction_687457_1,theorem,~ (social_science),beta2(genFunction_171864_1)).,
fof(contradict_687457_1,theorem,(social_science & ~ (social_science)),contraction(genFunction_671_1,genFunction_687457_1)).]
[fof(genFunction_343729_1,theorem,~ (religion),beta2(genFunction_85932_1)).,
fof(contradict_343729_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_343729_1)).]
[fof(genFunction_171865_1,theorem,~ (language),beta2(genFunction_42966_1)).]
[fof(genFunction_343730_1,theorem,~ ((art & literature)),beta1(genFunction_85932_1)).,
fof(genFunction_343730_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85932_1)).,
fof(genFunction_343730_2,theorem,~ (mcyXXX),alpha2(genFunction_85932_1)).,
fof(genFunction_343730_3,theorem,~ (((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX)),alpha1(genFunction_85932_3)).,
fof(genFunction_343730_4,theorem,~ (por2XX),alpha2(genFunction_85932_3)).]
[fof(genFunction_687460_1,theorem,~ (art),beta1(genFunction_343730_1)).,
fof(genFunction_687460_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343730_1)).,
fof(genFunction_687460_2,theorem,~ (danXXX),alpha2(genFunction_343730_1)).,
fof(genFunction_687460_3,theorem,~ ((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX)),alpha1(genFunction_343730_3)).,
fof(genFunction_687460_4,theorem,~ (lat2XX),alpha2(genFunction_343730_3)).,
fof(genFunction_687460_5,theorem,~ (artXXX),alpha1(genFunction_687460_1)).,
fof(contradict_687460_5,theorem,(artXXX & ~ (artXXX)),contraction(artXXX,genFunction_687460_5)).]
[fof(genFunction_687461_1,theorem,~ (literature),beta2(genFunction_343730_1)).,
fof(contradict_687461_1,theorem,(literature & ~ (literature)),contraction(genFunction_41_1,genFunction_687461_1)).]
[fof(genFunction_343731_1,theorem,~ (religion),beta2(genFunction_85932_1)).,
fof(contradict_343731_1,theorem,(religion & ~ (religion)),contraction(genFunction_83_1,genFunction_343731_1)).]
[fof(genFunction_85933_1,theorem,~ (phi115),beta2(genFunction_10_1)).,
fof(contradict_85933_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_85933_1)).]
[fof(genFunction_42967_1,theorem,~ (writing),beta2(genFunction_2_1)).,
fof(contradict_42967_1,theorem,(writing & ~ (writing)),contraction(genFunction_10741_1,genFunction_42967_1)).]
[fof(genFunction_5371_1,theorem,writing,beta2(hisXXX_writing)).]
[fof(genFunction_10742_1,theorem,~ (eng2XX),beta1(eng2XX_writing)).,
fof(contradict_10742_1,theorem,(eng2XX & ~ (eng2XX)),contraction(literature_courses,genFunction_10742_1)).]
[fof(genFunction_10743_1,theorem,writing,beta2(eng2XX_writing)).]
[fof(genFunction_21486_1,theorem,~ (phi115),beta1(phi115_writing)).,
fof(contradict_21486_1,theorem,(phi115 & ~ (phi115)),contraction(phi115,genFunction_21486_1)).]
[fof(genFunction_21487_1,theorem,writing,beta2(phi115_writing)).]
[fof(genFunction_42974_1,theorem,~ ((((((composition & humanities) & science) & math) & social_science) & language)),beta1(genFunction_2_1)).]
[fof(genFunction_85948_1,theorem,~ (((art & literature) & religion)),beta1(genFunction_10_1)).,
fof(genFunction_85948_1,theorem,~ ((((artXXX | arhXXX) | danXXX) | mcyXXX)),alpha1(genFunction_20_1)).,
fof(genFunction_85948_2,theorem,~ (thaXXX),alpha2(genFunction_20_1)).,
fof(genFunction_85948_3,theorem,~ ((((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX) | por2XX)),alpha1(genFunction_1342_1)).,
fof(genFunction_85948_4,theorem,~ (spa2XX),alpha2(genFunction_1342_1)).]
[fof(genFunction_171896_1,theorem,~ (((((composition & humanities) & science) & math) & social_science)),beta1(genFunction_42974_1)).]
[fof(genFunction_343792_1,theorem,~ ((art & literature)),beta1(genFunction_85948_1)).,
fof(genFunction_343792_1,theorem,~ (((artXXX | arhXXX) | danXXX)),alpha1(genFunction_85948_1)).,
fof(genFunction_343792_2,theorem,~ (mcyXXX),alpha2(genFunction_85948_1)).,
fof(genFunction_343792_3,theorem,~ (((((((((arb2XX | chi2XX) | fre2XX) | ger2XX) | gre2XX) | heb2XX) | ita2XX) | jap2XX) | lat2XX)),alpha1(genFunction_85948_3)).,
fof(genFunction_343792_4,theorem,~ (por2XX),alpha2(genFunction_85948_3)).]
[fof(genFunction_687584_1,theorem,~ ((((composition & humanities) & science) & math)),beta1(genFunction_171896_1)).]
[fof(genFunction_1375168_1,theorem,~ (art),beta1(genFunction_343792_1)).,
fof(genFunction_1375168_1,theorem,~ ((artXXX | arhXXX)),alpha1(genFunction_343792_1)).,