begin_problem(Unknown).

list_of_descriptions.
name({*some theory*}).
author({*Saturate*}).
status(satisfiable).
description({*type theory of some logic program*}).
end_of_list.

list_of_symbols.
functions[(goal__dnf,2),(dnf_,2),(a,2),(o,2),(goal__norm,2),(norm,2),(n,1),(z9,0),(z8,0),(z7,0),(z6,0),(z5,0),(z4,0),(z3,0),(z2,0),(z1,0),(z0,0)].
predicates[(tt__73_1,1),(tt__73_2,1),(tt__72_4,1),(tt__o_72_1_1,1),(tt__a_72_1_1_1,1),(tt__72_2,1),(tt__a_72_1_1_2,1),(tt__72_1,1),(tt__72_3,1),(tt__71_1,1),(tt__o_71_1_2,1),(tt__71_2,1),(tt__71_3,1),(tt__70_1,1),(tt__70_2,1),(tt__69_3,1),(tt__a_69_1_1,1),(tt__69_1,1),(tt__69_2,1),(tt__68_4,1),(tt__o_68_1_1,1),(tt__a_68_1_1_1,1),(tt__68_1,1),(tt__a_68_1_1_2,1),(tt__68_3,1),(tt__68_2,1),(tt__67_1,1),(tt__67_2,1),(tt__66_1,1),(tt__o_66_1_2,1),(tt__66_2,1),(tt__66_3,1),(tt__65_3,1),(tt__a_65_1_1,1),(tt__65_1,1),(tt__65_2,1),(tt__64_5,1),(tt__a_64_1_1,1),(tt__a_64_1_1_1,1),(tt__64_1,1),(tt__64_2,1),(tt__a_64_1_1_2,1),(tt__64_3,1),(tt__64_4,1),(tt__63_1,1),(tt__a_63_1_2,1),(tt__63_2,1),(tt__63_3,1),(tt__62_1,1),(tt__a_62_1_2,1),(tt__62_2,1),(tt__62_3,1),(tt__61_3,1),(tt__a_61_1_1,1),(tt__61_1,1),(tt__61_2,1),(tt__60_1,1),(tt__a_60_1_2,1),(tt__60_2,1),(tt__60_3,1),(goal__literal_59_1,1),(tt__a_58_1_1,1),(tt__58_2,1),(tt__a_58_1_2,1),(tt__58_1,1),(tt__a_58_1_2_1,1),(tt__58_3,1),(tt__58_4,1),(tt__57_1,1),(tt__a_57_1_2,1),(tt__57_2,1),(tt__57_3,1),(goal__literal_56_1,1),(tt__a_55_1_1,1),(tt__55_1,1),(tt__a_55_1_2,1),(tt__55_2,1),(tt__a_55_1_2_1,1),(tt__55_3,1),(tt__55_4,1),(tt__54_3,1),(tt__o_54_1_1,1),(tt__54_1,1),(tt__54_2,1),(tt__53_1,1),(tt__53_2,1),(tt__52_1,1),(tt__52_2,1),(tt__51_3,1),(tt__o_51_1_1,1),(tt__51_1,1),(tt__51_2,1),(tt__50_3,1),(tt__o_50_1_1,1),(tt__n_50_1_1_1,1),(tt__50_1,1),(tt__n_50_1_1_2,1),(tt__50_2,1),(tt__49_3,1),(tt__n_49_1_1,1),(tt__a_49_1_1_1,1),(tt__49_1,1),(tt__49_2,1),(tt__48_3,1),(tt__a_48_1_1,1),(tt__n_48_1_1_1,1),(tt__48_1,1),(tt__n_48_1_1_2,1),(tt__48_2,1),(tt__47_3,1),(tt__n_47_1_1,1),(tt__o_47_1_1_1,1),(tt__47_1,1),(tt__47_2,1),(tt__46_1,1),(tt__46_2,1),(tt__45_2,1),(tt__n_45_1_1,1),(tt__n_45_1_1_1,1),(tt__45_1,1),(goal__literal_44_1,1),(goal__literal_43_1,1),(tt__a_42_1_1,1),(tt__a_42_1_2,1),(tt__42_1,1),(tt__42_2,1),(goal__literal_41_1,1),(goal__literal_40_1,1),(tt__o_39_1_1,1),(tt__o_39_1_2,1),(tt__39_1,1),(tt__39_2,1),(goal__literal_38_1,1),(tt__37_1,1),(tt__36_3,1),(tt__o_36_1_1,1),(tt__36_1,1),(tt__36_2,1),(tt__35_1,1),(tt__35_2,1),(tt__a_34_1_1,1),(tt__34_1,1),(tt__o_34_1_1_2,1),(tt__34_2,1),(tt__34_3,1),(tt__a_34_1_2,1),(tt__34_4,1),(tt__34_5,1),(tt__33_4,1),(tt__a_33_1_1,1),(tt__33_3,1),(tt__a_33_1_1_1,1),(tt__33_1,1),(tt__33_2,1),(tt__32_4,1),(tt__a_32_1_1,1),(tt__32_1,1),(tt__a_32_1_1_2,1),(tt__32_2,1),(tt__32_3,1),(tt__31_1,1),(tt__31_2,1),(goal__literal_30_1,1),(tt__a_29_1_1,1),(tt__29_1,1),(tt__a_29_1_2,1),(tt__29_3,1),(tt__29_2,1),(tt__28_3,1),(tt__a_28_1_1,1),(tt__28_1,1),(tt__28_2,1),(tt__27_1,1),(tt__27_2,1),(tt__o_26_1_1,1),(tt__26_1,1),(tt__a_26_1_1_2,1),(tt__26_2,1),(tt__26_3,1),(tt__o_26_1_2,1),(tt__26_4,1),(tt__26_5,1),(tt__25_4,1),(tt__o_25_1_1,1),(tt__25_3,1),(tt__o_25_1_1_1,1),(tt__25_1,1),(tt__25_2,1),(tt__24_4,1),(tt__o_24_1_1,1),(tt__24_1,1),(tt__o_24_1_1_2,1),(tt__24_2,1),(tt__24_3,1),(tt__23_1,1),(tt__23_2,1),(goal__literal_22_1,1),(tt__o_21_1_1,1),(tt__21_1,1),(tt__o_21_1_2,1),(tt__21_3,1),(tt__21_2,1),(goal__literal_20_1,1),(goal__literal_19_1,1),(tt__a_18_1_1,1),(tt__a_18_1_2,1),(tt__18_1,1),(tt__18_2,1),(goal__literal_17_1,1),(goal__literal_16_1,1),(tt__o_15_1_1,1),(tt__o_15_1_2,1),(tt__15_1,1),(tt__15_2,1),(goal__literal_14_1,1),(tt_,1),(tt__13_1,1),(goal__literal_12_1,1),(goal__literal,1),(literal_11_1,1),(literal,1)].
end_of_list.

list_of_formulae(axioms).
formula(or(literal(z0))).
formula(or(literal(z1))).
formula(or(literal(z2))).
formula(or(literal(z3))).
formula(or(literal(z4))).
formula(or(literal(z5))).
formula(or(literal(z6))).
formula(or(literal(z7))).
formula(or(literal(z8))).
formula(or(literal(z9))).
formula(forall([_41079],or(not(literal_11_1(_41079)),literal(n(_41079))))).
formula(forall([_40998],or(not(goal__literal(n(_40998))),not(literal(_40998)),literal_11_1(_40998)))).
formula(forall([_40898],or(not(goal__literal_12_1(_40898)),goal__literal(_40898)))).
formula(forall([_40819],or(not(goal__literal(n(_40819))),goal__literal_12_1(_40819)))).
formula(forall([_40719,_40731],or(not(tt__13_1(_40731)),not(tt__13_1(_40719)),tt_(norm(_40719,_40731))))).
formula(forall([_40637],or(not(tt_(goal__norm(_40637,_40637))),not(literal(_40637)),tt__13_1(_40637)))).
formula(forall([_40547],or(not(goal__literal_14_1(_40547)),goal__literal(_40547)))).
formula(forall([_40468],or(not(tt_(goal__norm(_40468,_40468))),goal__literal_14_1(_40468)))).
formula(forall([_40378,_40390],or(not(tt__15_2(_40390)),not(tt__15_1(_40378)),tt__o_15_1_2(o(_40378,_40390))))).
formula(forall([_40286,_40298],or(not(tt__15_2(_40298)),not(tt__15_1(_40286)),tt__o_15_1_1(o(_40286,_40298))))).
formula(forall([_40146,_40158,_40170,_40182,_40194,_40206],or(not(tt__o_15_1_1(_40206)),not(tt__o_15_1_2(_40194)),not(tt__15_2(_40182)),not(tt__15_1(_40170)),not(tt__15_2(_40158)),not(tt__15_1(_40146)),tt_(norm(_40206,_40194))))).
formula(forall([_40060,_40061],or(not(tt_(goal__norm(o(_40060,_40061),o(_40060,_40061)))),not(literal(_40060)),not(literal(_40061)),tt__15_2(_40061)))).
formula(forall([_39950,_39951],or(not(tt_(goal__norm(o(_39950,_39951),o(_39950,_39951)))),not(literal(_39950)),not(literal(_39951)),tt__15_1(_39950)))).
formula(forall([_39846],or(not(goal__literal_16_1(_39846)),goal__literal(_39846)))).
formula(forall([_39763,_39764],or(not(tt_(goal__norm(o(_39763,_39764),o(_39763,_39764)))),goal__literal_16_1(_39763)))).
formula(forall([_39683],or(not(goal__literal_17_1(_39683)),goal__literal(_39683)))).
formula(forall([_39600,_39601],or(not(tt_(goal__norm(o(_39600,_39601),o(_39600,_39601)))),not(literal(_39600)),goal__literal_17_1(_39601)))).
formula(forall([_39496,_39508],or(not(tt__18_2(_39508)),not(tt__18_1(_39496)),tt__a_18_1_2(a(_39496,_39508))))).
formula(forall([_39404,_39416],or(not(tt__18_2(_39416)),not(tt__18_1(_39404)),tt__a_18_1_1(a(_39404,_39416))))).
formula(forall([_39264,_39276,_39288,_39300,_39312,_39324],or(not(tt__a_18_1_1(_39324)),not(tt__a_18_1_2(_39312)),not(tt__18_2(_39300)),not(tt__18_1(_39288)),not(tt__18_2(_39276)),not(tt__18_1(_39264)),tt_(norm(_39324,_39312))))).
formula(forall([_39178,_39179],or(not(tt_(goal__norm(a(_39178,_39179),a(_39178,_39179)))),not(literal(_39178)),not(literal(_39179)),tt__18_2(_39179)))).
formula(forall([_39068,_39069],or(not(tt_(goal__norm(a(_39068,_39069),a(_39068,_39069)))),not(literal(_39068)),not(literal(_39069)),tt__18_1(_39068)))).
formula(forall([_38964],or(not(goal__literal_19_1(_38964)),goal__literal(_38964)))).
formula(forall([_38881,_38882],or(not(tt_(goal__norm(a(_38881,_38882),a(_38881,_38882)))),goal__literal_19_1(_38881)))).
formula(forall([_38801],or(not(goal__literal_20_1(_38801)),goal__literal(_38801)))).
formula(forall([_38718,_38719],or(not(tt_(goal__norm(a(_38718,_38719),a(_38718,_38719)))),not(literal(_38718)),goal__literal_20_1(_38719)))).
formula(forall([_38614,_38626],or(not(tt__21_2(_38626)),not(tt__21_3(_38614)),tt__o_21_1_2(o(_38614,_38626))))).
formula(forall([_38522,_38534],or(not(tt__21_2(_38534)),not(tt__21_1(_38522)),tt__o_21_1_1(o(_38522,_38534))))).
formula(forall([_38382,_38394,_38406,_38418,_38430,_38442],or(not(tt__o_21_1_1(_38442)),not(tt__o_21_1_2(_38430)),not(tt__21_2(_38418)),not(tt__21_3(_38406)),not(tt__21_2(_38394)),not(tt__21_1(_38382)),tt_(norm(_38442,_38430))))).
formula(forall([_38293,_38296,_38297],or(not(tt_(goal__norm(o(_38296,_38297),o(_38293,_38297)))),not(literal(_38297)),not(tt_(norm(_38296,_38293))),tt__21_3(_38293)))).
formula(forall([_38180,_38183,_38184],or(not(tt_(goal__norm(o(_38183,_38184),o(_38180,_38184)))),not(literal(_38184)),not(tt_(norm(_38183,_38180))),tt__21_2(_38184)))).
formula(forall([_38067,_38070,_38071],or(not(tt_(goal__norm(o(_38070,_38071),o(_38067,_38071)))),not(literal(_38071)),not(tt_(norm(_38070,_38067))),tt__21_1(_38070)))).
formula(forall([_37963],or(not(goal__literal_22_1(_37963)),goal__literal(_37963)))).
formula(forall([_37877,_37880,_37881],or(not(tt_(goal__norm(o(_37880,_37881),o(_37877,_37881)))),goal__literal_22_1(_37881)))).
formula(forall([_37788,_37800],or(not(tt__23_2(_37800)),not(tt__23_1(_37788)),tt_(goal__norm(_37788,_37800))))).
formula(forall([_37699,_37702,_37703],or(not(tt_(goal__norm(o(_37702,_37703),o(_37699,_37703)))),not(literal(_37703)),tt__23_2(_37699)))).
formula(forall([_37601,_37604,_37605],or(not(tt_(goal__norm(o(_37604,_37605),o(_37601,_37605)))),not(literal(_37605)),tt__23_1(_37604)))).
formula(forall([_37500,_37512],or(not(tt__24_3(_37512)),not(tt__24_2(_37500)),tt__o_24_1_1_2(o(_37500,_37512))))).
formula(forall([_37408,_37420],or(not(tt__o_24_1_1_2(_37420)),not(tt__24_1(_37408)),tt__o_24_1_1(o(_37408,_37420))))).
formula(forall([_37268,_37280,_37292,_37304,_37316,_37328],or(not(tt__o_24_1_1(_37328)),not(tt__o_24_1_1_2(_37316)),not(tt__24_4(_37304)),not(tt__24_3(_37292)),not(tt__24_2(_37280)),not(tt__24_1(_37268)),tt_(norm(_37328,_37304))))).
formula(forall([_37179,_37180,_37182,_37186],or(not(tt_(goal__norm(o(_37182,o(_37179,_37180)),_37186))),not(tt_(norm(o(o(_37182,_37179),_37180),_37186))),tt__24_4(_37186)))).
formula(forall([_37072,_37073,_37075,_37079],or(not(tt_(goal__norm(o(_37075,o(_37072,_37073)),_37079))),not(tt_(norm(o(o(_37075,_37072),_37073),_37079))),tt__24_3(_37073)))).
formula(forall([_36965,_36966,_36968,_36972],or(not(tt_(goal__norm(o(_36968,o(_36965,_36966)),_36972))),not(tt_(norm(o(o(_36968,_36965),_36966),_36972))),tt__24_2(_36965)))).
formula(forall([_36858,_36859,_36861,_36865],or(not(tt_(goal__norm(o(_36861,o(_36858,_36859)),_36865))),not(tt_(norm(o(o(_36861,_36858),_36859),_36865))),tt__24_1(_36861)))).
formula(forall([_36748,_36760],or(not(tt__25_2(_36760)),not(tt__25_1(_36748)),tt__o_25_1_1_1(o(_36748,_36760))))).
formula(forall([_36656,_36668],or(not(tt__o_25_1_1_1(_36668)),not(tt__25_3(_36656)),tt__o_25_1_1(o(_36668,_36656))))).
formula(forall([_36516,_36528,_36540,_36552,_36564,_36576],or(not(tt__o_25_1_1(_36576)),not(tt__o_25_1_1_1(_36564)),not(tt__25_4(_36552)),not(tt__25_3(_36540)),not(tt__25_2(_36528)),not(tt__25_1(_36516)),tt_(goal__norm(_36576,_36552))))).
formula(forall([_36427,_36428,_36430,_36434],or(not(tt_(goal__norm(o(_36430,o(_36427,_36428)),_36434))),tt__25_4(_36434)))).
formula(forall([_36341,_36342,_36344,_36348],or(not(tt_(goal__norm(o(_36344,o(_36341,_36342)),_36348))),tt__25_3(_36342)))).
formula(forall([_36255,_36256,_36258,_36262],or(not(tt_(goal__norm(o(_36258,o(_36255,_36256)),_36262))),tt__25_2(_36255)))).
formula(forall([_36169,_36170,_36172,_36176],or(not(tt_(goal__norm(o(_36172,o(_36169,_36170)),_36176))),tt__25_1(_36172)))).
formula(forall([_36080,_36092],or(not(tt__26_5(_36092)),not(tt__26_4(_36080)),tt__o_26_1_2(o(_36080,_36092))))).
formula(forall([_35988,_36000],or(not(tt__26_3(_36000)),not(tt__26_2(_35988)),tt__a_26_1_1_2(a(_35988,_36000))))).
formula(forall([_35896,_35908],or(not(tt__a_26_1_1_2(_35908)),not(tt__26_1(_35896)),tt__o_26_1_1(o(_35896,_35908))))).
formula(forall([_35732,_35744,_35756,_35768,_35780,_35792,_35804,_35816],or(not(tt__o_26_1_1(_35816)),not(tt__a_26_1_1_2(_35804)),not(tt__o_26_1_2(_35792)),not(tt__26_5(_35780)),not(tt__26_4(_35768)),not(tt__26_3(_35756)),not(tt__26_2(_35744)),not(tt__26_1(_35732)),tt_(norm(_35816,_35792))))).
formula(forall([_35640,_35641,_35643,_35644,_35646],or(not(tt_(goal__norm(o(_35646,a(_35643,_35644)),o(_35640,_35641)))),not(tt_(norm(_35646,_35640))),not(tt_(norm(a(_35643,_35644),_35641))),tt__26_5(_35641)))).
formula(forall([_35518,_35519,_35521,_35522,_35524],or(not(tt_(goal__norm(o(_35524,a(_35521,_35522)),o(_35518,_35519)))),not(tt_(norm(_35524,_35518))),not(tt_(norm(a(_35521,_35522),_35519))),tt__26_4(_35518)))).
formula(forall([_35396,_35397,_35399,_35400,_35402],or(not(tt_(goal__norm(o(_35402,a(_35399,_35400)),o(_35396,_35397)))),not(tt_(norm(_35402,_35396))),not(tt_(norm(a(_35399,_35400),_35397))),tt__26_3(_35400)))).
formula(forall([_35274,_35275,_35277,_35278,_35280],or(not(tt_(goal__norm(o(_35280,a(_35277,_35278)),o(_35274,_35275)))),not(tt_(norm(_35280,_35274))),not(tt_(norm(a(_35277,_35278),_35275))),tt__26_2(_35277)))).
formula(forall([_35152,_35153,_35155,_35156,_35158],or(not(tt_(goal__norm(o(_35158,a(_35155,_35156)),o(_35152,_35153)))),not(tt_(norm(_35158,_35152))),not(tt_(norm(a(_35155,_35156),_35153))),tt__26_1(_35158)))).
formula(forall([_35030,_35042],or(not(tt__27_2(_35042)),not(tt__27_1(_35030)),tt_(goal__norm(_35030,_35042))))).
formula(forall([_34938,_34939,_34941,_34942,_34944],or(not(tt_(goal__norm(o(_34944,a(_34941,_34942)),o(_34938,_34939)))),tt__27_2(_34938)))).
formula(forall([_34849,_34850,_34852,_34853,_34855],or(not(tt_(goal__norm(o(_34855,a(_34852,_34853)),o(_34849,_34850)))),tt__27_1(_34855)))).
formula(forall([_34760,_34772],or(not(tt__28_2(_34772)),not(tt__28_1(_34760)),tt__a_28_1_1(a(_34760,_34772))))).
formula(forall([_34644,_34656,_34668,_34680],or(not(tt__a_28_1_1(_34680)),not(tt__28_3(_34668)),not(tt__28_2(_34656)),not(tt__28_1(_34644)),tt_(goal__norm(_34680,_34668))))).
formula(forall([_34552,_34553,_34555,_34556,_34558],or(not(tt_(goal__norm(o(_34558,a(_34555,_34556)),o(_34552,_34553)))),not(tt_(norm(_34558,_34552))),tt__28_3(_34553)))).
formula(forall([_34448,_34449,_34451,_34452,_34454],or(not(tt_(goal__norm(o(_34454,a(_34451,_34452)),o(_34448,_34449)))),not(tt_(norm(_34454,_34448))),tt__28_2(_34452)))).
formula(forall([_34344,_34345,_34347,_34348,_34350],or(not(tt_(goal__norm(o(_34350,a(_34347,_34348)),o(_34344,_34345)))),not(tt_(norm(_34350,_34344))),tt__28_1(_34347)))).
formula(forall([_34240,_34252],or(not(tt__29_2(_34252)),not(tt__29_3(_34240)),tt__a_29_1_2(a(_34240,_34252))))).
formula(forall([_34148,_34160],or(not(tt__29_2(_34160)),not(tt__29_1(_34148)),tt__a_29_1_1(a(_34148,_34160))))).
formula(forall([_34008,_34020,_34032,_34044,_34056,_34068],or(not(tt__a_29_1_1(_34068)),not(tt__a_29_1_2(_34056)),not(tt__29_2(_34044)),not(tt__29_3(_34032)),not(tt__29_2(_34020)),not(tt__29_1(_34008)),tt_(norm(_34068,_34056))))).
formula(forall([_33919,_33922,_33923],or(not(tt_(goal__norm(a(_33922,_33923),a(_33919,_33923)))),not(literal(_33923)),not(tt_(norm(_33922,_33919))),tt__29_3(_33919)))).
formula(forall([_33806,_33809,_33810],or(not(tt_(goal__norm(a(_33809,_33810),a(_33806,_33810)))),not(literal(_33810)),not(tt_(norm(_33809,_33806))),tt__29_2(_33810)))).
formula(forall([_33693,_33696,_33697],or(not(tt_(goal__norm(a(_33696,_33697),a(_33693,_33697)))),not(literal(_33697)),not(tt_(norm(_33696,_33693))),tt__29_1(_33696)))).
formula(forall([_33589],or(not(goal__literal_30_1(_33589)),goal__literal(_33589)))).
formula(forall([_33503,_33506,_33507],or(not(tt_(goal__norm(a(_33506,_33507),a(_33503,_33507)))),goal__literal_30_1(_33507)))).
formula(forall([_33414,_33426],or(not(tt__31_2(_33426)),not(tt__31_1(_33414)),tt_(goal__norm(_33414,_33426))))).
formula(forall([_33325,_33328,_33329],or(not(tt_(goal__norm(a(_33328,_33329),a(_33325,_33329)))),not(literal(_33329)),tt__31_2(_33325)))).
formula(forall([_33227,_33230,_33231],or(not(tt_(goal__norm(a(_33230,_33231),a(_33227,_33231)))),not(literal(_33231)),tt__31_1(_33230)))).
formula(forall([_33126,_33138],or(not(tt__32_3(_33138)),not(tt__32_2(_33126)),tt__a_32_1_1_2(a(_33126,_33138))))).
formula(forall([_33034,_33046],or(not(tt__a_32_1_1_2(_33046)),not(tt__32_1(_33034)),tt__a_32_1_1(a(_33034,_33046))))).
formula(forall([_32894,_32906,_32918,_32930,_32942,_32954],or(not(tt__a_32_1_1(_32954)),not(tt__a_32_1_1_2(_32942)),not(tt__32_4(_32930)),not(tt__32_3(_32918)),not(tt__32_2(_32906)),not(tt__32_1(_32894)),tt_(norm(_32954,_32930))))).
formula(forall([_32805,_32806,_32808,_32812],or(not(tt_(goal__norm(a(_32808,a(_32805,_32806)),_32812))),not(tt_(norm(a(a(_32808,_32805),_32806),_32812))),tt__32_4(_32812)))).
formula(forall([_32698,_32699,_32701,_32705],or(not(tt_(goal__norm(a(_32701,a(_32698,_32699)),_32705))),not(tt_(norm(a(a(_32701,_32698),_32699),_32705))),tt__32_3(_32699)))).
formula(forall([_32591,_32592,_32594,_32598],or(not(tt_(goal__norm(a(_32594,a(_32591,_32592)),_32598))),not(tt_(norm(a(a(_32594,_32591),_32592),_32598))),tt__32_2(_32591)))).
formula(forall([_32484,_32485,_32487,_32491],or(not(tt_(goal__norm(a(_32487,a(_32484,_32485)),_32491))),not(tt_(norm(a(a(_32487,_32484),_32485),_32491))),tt__32_1(_32487)))).
formula(forall([_32374,_32386],or(not(tt__33_2(_32386)),not(tt__33_1(_32374)),tt__a_33_1_1_1(a(_32374,_32386))))).
formula(forall([_32282,_32294],or(not(tt__a_33_1_1_1(_32294)),not(tt__33_3(_32282)),tt__a_33_1_1(a(_32294,_32282))))).
formula(forall([_32142,_32154,_32166,_32178,_32190,_32202],or(not(tt__a_33_1_1(_32202)),not(tt__a_33_1_1_1(_32190)),not(tt__33_4(_32178)),not(tt__33_3(_32166)),not(tt__33_2(_32154)),not(tt__33_1(_32142)),tt_(goal__norm(_32202,_32178))))).
formula(forall([_32053,_32054,_32056,_32060],or(not(tt_(goal__norm(a(_32056,a(_32053,_32054)),_32060))),tt__33_4(_32060)))).
formula(forall([_31967,_31968,_31970,_31974],or(not(tt_(goal__norm(a(_31970,a(_31967,_31968)),_31974))),tt__33_3(_31968)))).
formula(forall([_31881,_31882,_31884,_31888],or(not(tt_(goal__norm(a(_31884,a(_31881,_31882)),_31888))),tt__33_2(_31881)))).
formula(forall([_31795,_31796,_31798,_31802],or(not(tt_(goal__norm(a(_31798,a(_31795,_31796)),_31802))),tt__33_1(_31798)))).
formula(forall([_31706,_31718],or(not(tt__34_5(_31718)),not(tt__34_4(_31706)),tt__a_34_1_2(a(_31706,_31718))))).
formula(forall([_31614,_31626],or(not(tt__34_3(_31626)),not(tt__34_2(_31614)),tt__o_34_1_1_2(o(_31614,_31626))))).
formula(forall([_31522,_31534],or(not(tt__o_34_1_1_2(_31534)),not(tt__34_1(_31522)),tt__a_34_1_1(a(_31522,_31534))))).
formula(forall([_31358,_31370,_31382,_31394,_31406,_31418,_31430,_31442],or(not(tt__a_34_1_1(_31442)),not(tt__o_34_1_1_2(_31430)),not(tt__a_34_1_2(_31418)),not(tt__34_5(_31406)),not(tt__34_4(_31394)),not(tt__34_3(_31382)),not(tt__34_2(_31370)),not(tt__34_1(_31358)),tt_(norm(_31442,_31418))))).
formula(forall([_31266,_31267,_31269,_31270,_31272],or(not(tt_(goal__norm(a(_31272,o(_31269,_31270)),a(_31266,_31267)))),not(tt_(norm(_31272,_31266))),not(tt_(norm(o(_31269,_31270),_31267))),tt__34_5(_31267)))).
formula(forall([_31144,_31145,_31147,_31148,_31150],or(not(tt_(goal__norm(a(_31150,o(_31147,_31148)),a(_31144,_31145)))),not(tt_(norm(_31150,_31144))),not(tt_(norm(o(_31147,_31148),_31145))),tt__34_4(_31144)))).
formula(forall([_31022,_31023,_31025,_31026,_31028],or(not(tt_(goal__norm(a(_31028,o(_31025,_31026)),a(_31022,_31023)))),not(tt_(norm(_31028,_31022))),not(tt_(norm(o(_31025,_31026),_31023))),tt__34_3(_31026)))).
formula(forall([_30900,_30901,_30903,_30904,_30906],or(not(tt_(goal__norm(a(_30906,o(_30903,_30904)),a(_30900,_30901)))),not(tt_(norm(_30906,_30900))),not(tt_(norm(o(_30903,_30904),_30901))),tt__34_2(_30903)))).
formula(forall([_30778,_30779,_30781,_30782,_30784],or(not(tt_(goal__norm(a(_30784,o(_30781,_30782)),a(_30778,_30779)))),not(tt_(norm(_30784,_30778))),not(tt_(norm(o(_30781,_30782),_30779))),tt__34_1(_30784)))).
formula(forall([_30656,_30668],or(not(tt__35_2(_30668)),not(tt__35_1(_30656)),tt_(goal__norm(_30656,_30668))))).
formula(forall([_30564,_30565,_30567,_30568,_30570],or(not(tt_(goal__norm(a(_30570,o(_30567,_30568)),a(_30564,_30565)))),tt__35_2(_30564)))).
formula(forall([_30475,_30476,_30478,_30479,_30481],or(not(tt_(goal__norm(a(_30481,o(_30478,_30479)),a(_30475,_30476)))),tt__35_1(_30481)))).
formula(forall([_30386,_30398],or(not(tt__36_2(_30398)),not(tt__36_1(_30386)),tt__o_36_1_1(o(_30386,_30398))))).
formula(forall([_30270,_30282,_30294,_30306],or(not(tt__o_36_1_1(_30306)),not(tt__36_3(_30294)),not(tt__36_2(_30282)),not(tt__36_1(_30270)),tt_(goal__norm(_30306,_30294))))).
formula(forall([_30178,_30179,_30181,_30182,_30184],or(not(tt_(goal__norm(a(_30184,o(_30181,_30182)),a(_30178,_30179)))),not(tt_(norm(_30184,_30178))),tt__36_3(_30179)))).
formula(forall([_30074,_30075,_30077,_30078,_30080],or(not(tt_(goal__norm(a(_30080,o(_30077,_30078)),a(_30074,_30075)))),not(tt_(norm(_30080,_30074))),tt__36_2(_30078)))).
formula(forall([_29970,_29971,_29973,_29974,_29976],or(not(tt_(goal__norm(a(_29976,o(_29973,_29974)),a(_29970,_29971)))),not(tt_(norm(_29976,_29970))),tt__36_1(_29973)))).
formula(forall([_29866,_29878],or(not(tt__37_1(_29878)),not(tt__37_1(_29866)),tt_(dnf_(_29866,_29878))))).
formula(forall([_29784],or(not(tt_(goal__dnf(_29784,_29784))),not(literal(_29784)),tt__37_1(_29784)))).
formula(forall([_29694],or(not(goal__literal_38_1(_29694)),goal__literal(_29694)))).
formula(forall([_29615],or(not(tt_(goal__dnf(_29615,_29615))),goal__literal_38_1(_29615)))).
formula(forall([_29525,_29537],or(not(tt__39_2(_29537)),not(tt__39_1(_29525)),tt__o_39_1_2(o(_29525,_29537))))).
formula(forall([_29433,_29445],or(not(tt__39_2(_29445)),not(tt__39_1(_29433)),tt__o_39_1_1(o(_29433,_29445))))).
formula(forall([_29293,_29305,_29317,_29329,_29341,_29353],or(not(tt__o_39_1_1(_29353)),not(tt__o_39_1_2(_29341)),not(tt__39_2(_29329)),not(tt__39_1(_29317)),not(tt__39_2(_29305)),not(tt__39_1(_29293)),tt_(dnf_(_29353,_29341))))).
formula(forall([_29207,_29208],or(not(tt_(goal__dnf(o(_29207,_29208),o(_29207,_29208)))),not(literal(_29207)),not(literal(_29208)),tt__39_2(_29208)))).
formula(forall([_29097,_29098],or(not(tt_(goal__dnf(o(_29097,_29098),o(_29097,_29098)))),not(literal(_29097)),not(literal(_29098)),tt__39_1(_29097)))).
formula(forall([_28993],or(not(goal__literal_40_1(_28993)),goal__literal(_28993)))).
formula(forall([_28910,_28911],or(not(tt_(goal__dnf(o(_28910,_28911),o(_28910,_28911)))),goal__literal_40_1(_28910)))).
formula(forall([_28830],or(not(goal__literal_41_1(_28830)),goal__literal(_28830)))).
formula(forall([_28747,_28748],or(not(tt_(goal__dnf(o(_28747,_28748),o(_28747,_28748)))),not(literal(_28747)),goal__literal_41_1(_28748)))).
formula(forall([_28643,_28655],or(not(tt__42_2(_28655)),not(tt__42_1(_28643)),tt__a_42_1_2(a(_28643,_28655))))).
formula(forall([_28551,_28563],or(not(tt__42_2(_28563)),not(tt__42_1(_28551)),tt__a_42_1_1(a(_28551,_28563))))).
formula(forall([_28411,_28423,_28435,_28447,_28459,_28471],or(not(tt__a_42_1_1(_28471)),not(tt__a_42_1_2(_28459)),not(tt__42_2(_28447)),not(tt__42_1(_28435)),not(tt__42_2(_28423)),not(tt__42_1(_28411)),tt_(dnf_(_28471,_28459))))).
formula(forall([_28325,_28326],or(not(tt_(goal__dnf(a(_28325,_28326),a(_28325,_28326)))),not(literal(_28325)),not(literal(_28326)),tt__42_2(_28326)))).
formula(forall([_28215,_28216],or(not(tt_(goal__dnf(a(_28215,_28216),a(_28215,_28216)))),not(literal(_28215)),not(literal(_28216)),tt__42_1(_28215)))).
formula(forall([_28111],or(not(goal__literal_43_1(_28111)),goal__literal(_28111)))).
formula(forall([_28028,_28029],or(not(tt_(goal__dnf(a(_28028,_28029),a(_28028,_28029)))),goal__literal_43_1(_28028)))).
formula(forall([_27948],or(not(goal__literal_44_1(_27948)),goal__literal(_27948)))).
formula(forall([_27865,_27866],or(not(tt_(goal__dnf(a(_27865,_27866),a(_27865,_27866)))),not(literal(_27865)),goal__literal_44_1(_27866)))).
formula(forall([_27773],or(not(tt__45_1(_27773)),tt__n_45_1_1_1(n(_27773))))).
formula(forall([_27694],or(not(tt__n_45_1_1_1(_27694)),tt__n_45_1_1(n(_27694))))).
formula(forall([_27579,_27591,_27603,_27615],or(not(tt__n_45_1_1(_27615)),not(tt__n_45_1_1_1(_27603)),not(tt__45_2(_27591)),not(tt__45_1(_27579)),tt_(dnf_(_27615,_27591))))).
formula(forall([_27492,_27497],or(not(tt_(goal__dnf(n(n(_27492)),_27497))),not(tt_(dnf_(_27492,_27497))),tt__45_2(_27497)))).
formula(forall([_27393,_27398],or(not(tt_(goal__dnf(n(n(_27393)),_27398))),not(tt_(dnf_(_27393,_27398))),tt__45_1(_27393)))).
formula(forall([_27289,_27301],or(not(tt__46_2(_27301)),not(tt__46_1(_27289)),tt_(goal__dnf(_27289,_27301))))).
formula(forall([_27202,_27207],or(not(tt_(goal__dnf(n(n(_27202)),_27207))),tt__46_2(_27207)))).
formula(forall([_27118,_27123],or(not(tt_(goal__dnf(n(n(_27118)),_27123))),tt__46_1(_27118)))).
formula(forall([_27029,_27041],or(not(tt__47_2(_27041)),not(tt__47_1(_27029)),tt__o_47_1_1_1(o(_27029,_27041))))).
formula(forall([_26949],or(not(tt__o_47_1_1_1(_26949)),tt__n_47_1_1(n(_26949))))).
formula(forall([_26822,_26834,_26846,_26858,_26870],or(not(tt__n_47_1_1(_26870)),not(tt__o_47_1_1_1(_26858)),not(tt__47_3(_26846)),not(tt__47_2(_26834)),not(tt__47_1(_26822)),tt_(dnf_(_26870,_26846))))).
formula(forall([_26734,_26735,_26740],or(not(tt_(goal__dnf(n(o(_26734,_26735)),_26740))),not(tt_(dnf_(a(n(_26734),n(_26735)),_26740))),tt__47_3(_26740)))).
formula(forall([_26627,_26628,_26633],or(not(tt_(goal__dnf(n(o(_26627,_26628)),_26633))),not(tt_(dnf_(a(n(_26627),n(_26628)),_26633))),tt__47_2(_26628)))).
formula(forall([_26520,_26521,_26526],or(not(tt_(goal__dnf(n(o(_26520,_26521)),_26526))),not(tt_(dnf_(a(n(_26520),n(_26521)),_26526))),tt__47_1(_26520)))).
formula(forall([_26421],or(not(tt__48_2(_26421)),tt__n_48_1_1_2(n(_26421))))).
formula(forall([_26342],or(not(tt__48_1(_26342)),tt__n_48_1_1_1(n(_26342))))).
formula(forall([_26251,_26263],or(not(tt__n_48_1_1_1(_26263)),not(tt__n_48_1_1_2(_26251)),tt__a_48_1_1(a(_26263,_26251))))).
formula(forall([_26111,_26123,_26135,_26147,_26159,_26171],or(not(tt__a_48_1_1(_26171)),not(tt__n_48_1_1_1(_26159)),not(tt__n_48_1_1_2(_26147)),not(tt__48_3(_26135)),not(tt__48_2(_26123)),not(tt__48_1(_26111)),tt_(goal__dnf(_26171,_26135))))).
formula(forall([_26023,_26024,_26029],or(not(tt_(goal__dnf(n(o(_26023,_26024)),_26029))),tt__48_3(_26029)))).
formula(forall([_25938,_25939,_25944],or(not(tt_(goal__dnf(n(o(_25938,_25939)),_25944))),tt__48_2(_25939)))).
formula(forall([_25853,_25854,_25859],or(not(tt_(goal__dnf(n(o(_25853,_25854)),_25859))),tt__48_1(_25853)))).
formula(forall([_25764,_25776],or(not(tt__49_2(_25776)),not(tt__49_1(_25764)),tt__a_49_1_1_1(a(_25764,_25776))))).
formula(forall([_25684],or(not(tt__a_49_1_1_1(_25684)),tt__n_49_1_1(n(_25684))))).
formula(forall([_25557,_25569,_25581,_25593,_25605],or(not(tt__n_49_1_1(_25605)),not(tt__a_49_1_1_1(_25593)),not(tt__49_3(_25581)),not(tt__49_2(_25569)),not(tt__49_1(_25557)),tt_(dnf_(_25605,_25581))))).
formula(forall([_25469,_25470,_25475],or(not(tt_(goal__dnf(n(a(_25469,_25470)),_25475))),not(tt_(dnf_(o(n(_25469),n(_25470)),_25475))),tt__49_3(_25475)))).
formula(forall([_25362,_25363,_25368],or(not(tt_(goal__dnf(n(a(_25362,_25363)),_25368))),not(tt_(dnf_(o(n(_25362),n(_25363)),_25368))),tt__49_2(_25363)))).
formula(forall([_25255,_25256,_25261],or(not(tt_(goal__dnf(n(a(_25255,_25256)),_25261))),not(tt_(dnf_(o(n(_25255),n(_25256)),_25261))),tt__49_1(_25255)))).
formula(forall([_25156],or(not(tt__50_2(_25156)),tt__n_50_1_1_2(n(_25156))))).
formula(forall([_25077],or(not(tt__50_1(_25077)),tt__n_50_1_1_1(n(_25077))))).
formula(forall([_24986,_24998],or(not(tt__n_50_1_1_1(_24998)),not(tt__n_50_1_1_2(_24986)),tt__o_50_1_1(o(_24998,_24986))))).
formula(forall([_24846,_24858,_24870,_24882,_24894,_24906],or(not(tt__o_50_1_1(_24906)),not(tt__n_50_1_1_1(_24894)),not(tt__n_50_1_1_2(_24882)),not(tt__50_3(_24870)),not(tt__50_2(_24858)),not(tt__50_1(_24846)),tt_(goal__dnf(_24906,_24870))))).
formula(forall([_24758,_24759,_24764],or(not(tt_(goal__dnf(n(a(_24758,_24759)),_24764))),tt__50_3(_24764)))).
formula(forall([_24673,_24674,_24679],or(not(tt_(goal__dnf(n(a(_24673,_24674)),_24679))),tt__50_2(_24674)))).
formula(forall([_24588,_24589,_24594],or(not(tt_(goal__dnf(n(a(_24588,_24589)),_24594))),tt__50_1(_24588)))).
formula(forall([_24499,_24511],or(not(tt__51_2(_24511)),not(tt__51_1(_24499)),tt__o_51_1_1(o(_24499,_24511))))).
formula(forall([_24383,_24395,_24407,_24419],or(not(tt__o_51_1_1(_24419)),not(tt__51_3(_24407)),not(tt__51_2(_24395)),not(tt__51_1(_24383)),tt_(dnf_(_24419,_24407))))).
formula(forall([_24268,_24283,_24297,_24298,_24301],or(not(tt_(goal__dnf(o(_24297,_24298),_24301))),not(tt_(dnf_(_24297,_24283))),not(tt_(dnf_(_24298,_24268))),not(tt_(norm(o(_24283,_24268),_24301))),tt__51_3(_24301)))).
formula(forall([_24137,_24152,_24166,_24167,_24170],or(not(tt_(goal__dnf(o(_24166,_24167),_24170))),not(tt_(dnf_(_24166,_24152))),not(tt_(dnf_(_24167,_24137))),not(tt_(norm(o(_24152,_24137),_24170))),tt__51_2(_24167)))).
formula(forall([_24006,_24021,_24035,_24036,_24039],or(not(tt_(goal__dnf(o(_24035,_24036),_24039))),not(tt_(dnf_(_24035,_24021))),not(tt_(dnf_(_24036,_24006))),not(tt_(norm(o(_24021,_24006),_24039))),tt__51_1(_24035)))).
formula(forall([_23898,_23910],or(not(tt__52_2(_23910)),not(tt__52_1(_23898)),tt_(goal__dnf(_23898,_23910))))).
formula(forall([_23798,_23812,_23813,_23816],or(not(tt_(goal__dnf(o(_23812,_23813),_23816))),tt__52_2(_23798)))).
formula(forall([_23729,_23730,_23733],or(not(tt_(goal__dnf(o(_23729,_23730),_23733))),tt__52_1(_23729)))).
formula(forall([_23640,_23652],or(not(tt__53_2(_23652)),not(tt__53_1(_23640)),tt_(goal__dnf(_23640,_23652))))).
formula(forall([_23525,_23540,_23554,_23555,_23558],or(not(tt_(goal__dnf(o(_23554,_23555),_23558))),not(tt_(dnf_(_23554,_23540))),tt__53_2(_23525)))).
formula(forall([_23442,_23456,_23457,_23460],or(not(tt_(goal__dnf(o(_23456,_23457),_23460))),not(tt_(dnf_(_23456,_23442))),tt__53_1(_23457)))).
formula(forall([_23352,_23364],or(not(tt__54_2(_23364)),not(tt__54_1(_23352)),tt__o_54_1_1(o(_23352,_23364))))).
formula(forall([_23236,_23248,_23260,_23272],or(not(tt__o_54_1_1(_23272)),not(tt__54_3(_23260)),not(tt__54_2(_23248)),not(tt__54_1(_23236)),tt_(goal__norm(_23272,_23260))))).
formula(forall([_23121,_23136,_23150,_23151,_23154],or(not(tt_(goal__dnf(o(_23150,_23151),_23154))),not(tt_(dnf_(_23151,_23136))),not(tt_(dnf_(_23150,_23121))),tt__54_3(_23154)))).
formula(forall([_23008,_23023,_23037,_23038,_23041],or(not(tt_(goal__dnf(o(_23037,_23038),_23041))),not(tt_(dnf_(_23038,_23023))),not(tt_(dnf_(_23037,_23008))),tt__54_2(_23023)))).
formula(forall([_22895,_22910,_22924,_22925,_22928],or(not(tt_(goal__dnf(o(_22924,_22925),_22928))),not(tt_(dnf_(_22925,_22910))),not(tt_(dnf_(_22924,_22895))),tt__54_1(_22895)))).
formula(forall([_22805,_22817],or(not(tt__55_4(_22817)),not(tt__55_3(_22805)),tt__a_55_1_2_1(a(_22805,_22817))))).
formula(forall([_22713,_22725],or(not(tt__a_55_1_2_1(_22725)),not(tt__55_2(_22713)),tt__a_55_1_2(a(_22725,_22713))))).
formula(forall([_22621,_22633],or(not(tt__55_2(_22633)),not(tt__55_1(_22621)),tt__a_55_1_1(a(_22621,_22633))))).
formula(forall([_22457,_22469,_22481,_22493,_22505,_22517,_22529,_22541],or(not(tt__a_55_1_1(_22541)),not(tt__a_55_1_2(_22529)),not(tt__a_55_1_2_1(_22517)),not(tt__55_2(_22505)),not(tt__55_4(_22493)),not(tt__55_3(_22481)),not(tt__55_2(_22469)),not(tt__55_1(_22457)),tt_(dnf_(_22541,_22529))))).
formula(forall([_22365,_22366,_22371,_22372],or(not(tt_(goal__dnf(a(_22371,_22372),a(a(_22365,_22366),_22372)))),not(literal(_22372)),not(tt_(dnf_(_22371,a(_22365,_22366)))),tt__55_4(_22366)))).
formula(forall([_22246,_22247,_22252,_22253],or(not(tt_(goal__dnf(a(_22252,_22253),a(a(_22246,_22247),_22253)))),not(literal(_22253)),not(tt_(dnf_(_22252,a(_22246,_22247)))),tt__55_3(_22246)))).
formula(forall([_22127,_22128,_22133,_22134],or(not(tt_(goal__dnf(a(_22133,_22134),a(a(_22127,_22128),_22134)))),not(literal(_22134)),not(tt_(dnf_(_22133,a(_22127,_22128)))),tt__55_2(_22134)))).
formula(forall([_22008,_22009,_22014,_22015],or(not(tt_(goal__dnf(a(_22014,_22015),a(a(_22008,_22009),_22015)))),not(literal(_22015)),not(tt_(dnf_(_22014,a(_22008,_22009)))),tt__55_1(_22014)))).
formula(forall([_21901],or(not(goal__literal_56_1(_21901)),goal__literal(_21901)))).
formula(forall([_21812,_21813,_21818,_21819],or(not(tt_(goal__dnf(a(_21818,_21819),a(a(_21812,_21813),_21819)))),goal__literal_56_1(_21819)))).
formula(forall([_21723,_21735],or(not(tt__57_3(_21735)),not(tt__57_2(_21723)),tt__a_57_1_2(a(_21723,_21735))))).
formula(forall([_21607,_21619,_21631,_21643],or(not(tt__a_57_1_2(_21643)),not(tt__57_3(_21631)),not(tt__57_2(_21619)),not(tt__57_1(_21607)),tt_(goal__dnf(_21607,_21643))))).
formula(forall([_21515,_21516,_21521,_21522],or(not(tt_(goal__dnf(a(_21521,_21522),a(a(_21515,_21516),_21522)))),not(literal(_21522)),tt__57_3(_21516)))).
formula(forall([_21414,_21415,_21420,_21421],or(not(tt_(goal__dnf(a(_21420,_21421),a(a(_21414,_21415),_21421)))),not(literal(_21421)),tt__57_2(_21414)))).
formula(forall([_21313,_21314,_21319,_21320],or(not(tt_(goal__dnf(a(_21319,_21320),a(a(_21313,_21314),_21320)))),not(literal(_21320)),tt__57_1(_21319)))).
formula(forall([_21212,_21224],or(not(tt__58_4(_21224)),not(tt__58_3(_21212)),tt__a_58_1_2_1(a(_21212,_21224))))).
formula(forall([_21120,_21132],or(not(tt__a_58_1_2_1(_21132)),not(tt__58_1(_21120)),tt__a_58_1_2(a(_21132,_21120))))).
formula(forall([_21028,_21040],or(not(tt__58_2(_21040)),not(tt__58_1(_21028)),tt__a_58_1_1(a(_21028,_21040))))).
formula(forall([_20864,_20876,_20888,_20900,_20912,_20924,_20936,_20948],or(not(tt__a_58_1_1(_20948)),not(tt__a_58_1_2(_20936)),not(tt__a_58_1_2_1(_20924)),not(tt__58_1(_20912)),not(tt__58_4(_20900)),not(tt__58_3(_20888)),not(tt__58_2(_20876)),not(tt__58_1(_20864)),tt_(dnf_(_20948,_20936))))).
formula(forall([_20772,_20773,_20778,_20779],or(not(tt_(goal__dnf(a(_20778,_20779),a(a(_20772,_20773),_20778)))),not(literal(_20778)),not(tt_(dnf_(_20779,a(_20772,_20773)))),tt__58_4(_20773)))).
formula(forall([_20653,_20654,_20659,_20660],or(not(tt_(goal__dnf(a(_20659,_20660),a(a(_20653,_20654),_20659)))),not(literal(_20659)),not(tt_(dnf_(_20660,a(_20653,_20654)))),tt__58_3(_20653)))).
formula(forall([_20534,_20535,_20540,_20541],or(not(tt_(goal__dnf(a(_20540,_20541),a(a(_20534,_20535),_20540)))),not(literal(_20540)),not(tt_(dnf_(_20541,a(_20534,_20535)))),tt__58_2(_20541)))).
formula(forall([_20415,_20416,_20421,_20422],or(not(tt_(goal__dnf(a(_20421,_20422),a(a(_20415,_20416),_20421)))),not(literal(_20421)),not(tt_(dnf_(_20422,a(_20415,_20416)))),tt__58_1(_20421)))).
formula(forall([_20308],or(not(goal__literal_59_1(_20308)),goal__literal(_20308)))).
formula(forall([_20219,_20220,_20225,_20226],or(not(tt_(goal__dnf(a(_20225,_20226),a(a(_20219,_20220),_20225)))),goal__literal_59_1(_20225)))).
formula(forall([_20130,_20142],or(not(tt__60_3(_20142)),not(tt__60_2(_20130)),tt__a_60_1_2(a(_20130,_20142))))).
formula(forall([_20014,_20026,_20038,_20050],or(not(tt__a_60_1_2(_20050)),not(tt__60_3(_20038)),not(tt__60_2(_20026)),not(tt__60_1(_20014)),tt_(goal__dnf(_20014,_20050))))).
formula(forall([_19922,_19923,_19928,_19929],or(not(tt_(goal__dnf(a(_19928,_19929),a(a(_19922,_19923),_19928)))),not(literal(_19928)),tt__60_3(_19923)))).
formula(forall([_19821,_19822,_19827,_19828],or(not(tt_(goal__dnf(a(_19827,_19828),a(a(_19821,_19822),_19827)))),not(literal(_19827)),tt__60_2(_19821)))).
formula(forall([_19720,_19721,_19726,_19727],or(not(tt_(goal__dnf(a(_19726,_19727),a(a(_19720,_19721),_19726)))),not(literal(_19726)),tt__60_1(_19727)))).
formula(forall([_19619,_19631],or(not(tt__61_2(_19631)),not(tt__61_1(_19619)),tt__a_61_1_1(a(_19619,_19631))))).
formula(forall([_19503,_19515,_19527,_19539],or(not(tt__a_61_1_1(_19539)),not(tt__61_3(_19527)),not(tt__61_2(_19515)),not(tt__61_1(_19503)),tt_(dnf_(_19539,_19527))))).
formula(forall([_19381,_19382,_19399,_19400,_19417,_19418,_19421],or(not(tt_(goal__dnf(a(_19417,_19418),_19421))),not(tt_(dnf_(_19417,a(_19399,_19400)))),not(tt_(dnf_(_19418,a(_19381,_19382)))),not(tt_(norm(a(a(_19399,_19400),a(_19381,_19382)),_19421))),tt__61_3(_19421)))).
formula(forall([_19238,_19239,_19256,_19257,_19274,_19275,_19278],or(not(tt_(goal__dnf(a(_19274,_19275),_19278))),not(tt_(dnf_(_19274,a(_19256,_19257)))),not(tt_(dnf_(_19275,a(_19238,_19239)))),not(tt_(norm(a(a(_19256,_19257),a(_19238,_19239)),_19278))),tt__61_2(_19275)))).
formula(forall([_19095,_19096,_19113,_19114,_19131,_19132,_19135],or(not(tt_(goal__dnf(a(_19131,_19132),_19135))),not(tt_(dnf_(_19131,a(_19113,_19114)))),not(tt_(dnf_(_19132,a(_19095,_19096)))),not(tt_(norm(a(a(_19113,_19114),a(_19095,_19096)),_19135))),tt__61_1(_19131)))).
formula(forall([_18982,_18994],or(not(tt__62_3(_18994)),not(tt__62_2(_18982)),tt__a_62_1_2(a(_18982,_18994))))).
formula(forall([_18866,_18878,_18890,_18902],or(not(tt__a_62_1_2(_18902)),not(tt__62_3(_18890)),not(tt__62_2(_18878)),not(tt__62_1(_18866)),tt_(goal__dnf(_18866,_18902))))).
formula(forall([_18766,_18780,_18781,_18784],or(not(tt_(goal__dnf(a(_18780,_18781),_18784))),tt__62_3(_18766)))).
formula(forall([_18683,_18697,_18698,_18701],or(not(tt_(goal__dnf(a(_18697,_18698),_18701))),tt__62_2(_18683)))).
formula(forall([_18614,_18615,_18618],or(not(tt_(goal__dnf(a(_18614,_18615),_18618))),tt__62_1(_18614)))).
formula(forall([_18525,_18537],or(not(tt__63_3(_18537)),not(tt__63_2(_18525)),tt__a_63_1_2(a(_18525,_18537))))).
formula(forall([_18409,_18421,_18433,_18445],or(not(tt__a_63_1_2(_18445)),not(tt__63_3(_18433)),not(tt__63_2(_18421)),not(tt__63_1(_18409)),tt_(goal__dnf(_18409,_18445))))).
formula(forall([_18291,_18305,_18306,_18323,_18324,_18327],or(not(tt_(goal__dnf(a(_18323,_18324),_18327))),not(tt_(dnf_(_18323,a(_18305,_18306)))),tt__63_3(_18291)))).
formula(forall([_18190,_18204,_18205,_18222,_18223,_18226],or(not(tt_(goal__dnf(a(_18222,_18223),_18226))),not(tt_(dnf_(_18222,a(_18204,_18205)))),tt__63_2(_18190)))).
formula(forall([_18103,_18104,_18121,_18122,_18125],or(not(tt_(goal__dnf(a(_18121,_18122),_18125))),not(tt_(dnf_(_18121,a(_18103,_18104)))),tt__63_1(_18122)))).
formula(forall([_18014,_18026],or(not(tt__64_4(_18026)),not(tt__64_3(_18014)),tt__a_64_1_1_2(a(_18014,_18026))))).
formula(forall([_17922,_17934],or(not(tt__64_2(_17934)),not(tt__64_1(_17922)),tt__a_64_1_1_1(a(_17922,_17934))))).
formula(forall([_17830,_17842],or(not(tt__a_64_1_1_1(_17842)),not(tt__a_64_1_1_2(_17830)),tt__a_64_1_1(a(_17842,_17830))))).
formula(forall([_17666,_17678,_17690,_17702,_17714,_17726,_17738,_17750],or(not(tt__a_64_1_1(_17750)),not(tt__a_64_1_1_1(_17738)),not(tt__a_64_1_1_2(_17726)),not(tt__64_5(_17714)),not(tt__64_4(_17702)),not(tt__64_3(_17690)),not(tt__64_2(_17678)),not(tt__64_1(_17666)),tt_(goal__norm(_17750,_17714))))).
formula(forall([_17544,_17545,_17562,_17563,_17580,_17581,_17584],or(not(tt_(goal__dnf(a(_17580,_17581),_17584))),not(tt_(dnf_(_17581,a(_17562,_17563)))),not(tt_(dnf_(_17580,a(_17544,_17545)))),tt__64_5(_17584)))).
formula(forall([_17425,_17426,_17443,_17444,_17461,_17462,_17465],or(not(tt_(goal__dnf(a(_17461,_17462),_17465))),not(tt_(dnf_(_17462,a(_17443,_17444)))),not(tt_(dnf_(_17461,a(_17425,_17426)))),tt__64_4(_17444)))).
formula(forall([_17306,_17307,_17324,_17325,_17342,_17343,_17346],or(not(tt_(goal__dnf(a(_17342,_17343),_17346))),not(tt_(dnf_(_17343,a(_17324,_17325)))),not(tt_(dnf_(_17342,a(_17306,_17307)))),tt__64_3(_17324)))).
formula(forall([_17187,_17188,_17205,_17206,_17223,_17224,_17227],or(not(tt_(goal__dnf(a(_17223,_17224),_17227))),not(tt_(dnf_(_17224,a(_17205,_17206)))),not(tt_(dnf_(_17223,a(_17187,_17188)))),tt__64_2(_17188)))).
formula(forall([_17068,_17069,_17086,_17087,_17104,_17105,_17108],or(not(tt_(goal__dnf(a(_17104,_17105),_17108))),not(tt_(dnf_(_17105,a(_17086,_17087)))),not(tt_(dnf_(_17104,a(_17068,_17069)))),tt__64_1(_17068)))).
formula(forall([_16979,_16991],or(not(tt__65_2(_16991)),not(tt__65_1(_16979)),tt__a_65_1_1(a(_16979,_16991))))).
formula(forall([_16863,_16875,_16887,_16899],or(not(tt__a_65_1_1(_16899)),not(tt__65_3(_16887)),not(tt__65_2(_16875)),not(tt__65_1(_16863)),tt_(dnf_(_16899,_16887))))).
formula(forall([_16745,_16759,_16760,_16777,_16778,_16781],or(not(tt_(goal__dnf(a(_16777,_16778),_16781))),not(tt_(dnf_(_16777,o(_16759,_16760)))),not(tt_(dnf_(_16778,_16745))),not(tt_(dnf_(o(a(_16759,_16745),a(_16760,_16745)),_16781))),tt__65_3(_16781)))).
formula(forall([_16605,_16619,_16620,_16637,_16638,_16641],or(not(tt_(goal__dnf(a(_16637,_16638),_16641))),not(tt_(dnf_(_16637,o(_16619,_16620)))),not(tt_(dnf_(_16638,_16605))),not(tt_(dnf_(o(a(_16619,_16605),a(_16620,_16605)),_16641))),tt__65_2(_16638)))).
formula(forall([_16465,_16479,_16480,_16497,_16498,_16501],or(not(tt_(goal__dnf(a(_16497,_16498),_16501))),not(tt_(dnf_(_16497,o(_16479,_16480)))),not(tt_(dnf_(_16498,_16465))),not(tt_(dnf_(o(a(_16479,_16465),a(_16480,_16465)),_16501))),tt__65_1(_16497)))).
formula(forall([_16351,_16363],or(not(tt__66_3(_16363)),not(tt__66_2(_16351)),tt__o_66_1_2(o(_16351,_16363))))).
formula(forall([_16235,_16247,_16259,_16271],or(not(tt__o_66_1_2(_16271)),not(tt__66_3(_16259)),not(tt__66_2(_16247)),not(tt__66_1(_16235)),tt_(goal__dnf(_16235,_16271))))).
formula(forall([_16135,_16149,_16150,_16153],or(not(tt_(goal__dnf(a(_16149,_16150),_16153))),tt__66_3(_16135)))).
formula(forall([_16052,_16066,_16067,_16070],or(not(tt_(goal__dnf(a(_16066,_16067),_16070))),tt__66_2(_16052)))).
formula(forall([_15983,_15984,_15987],or(not(tt_(goal__dnf(a(_15983,_15984),_15987))),tt__66_1(_15983)))).
formula(forall([_15894,_15906],or(not(tt__67_2(_15906)),not(tt__67_1(_15894)),tt_(goal__dnf(_15894,_15906))))).
formula(forall([_15776,_15790,_15791,_15808,_15809,_15812],or(not(tt_(goal__dnf(a(_15808,_15809),_15812))),not(tt_(dnf_(_15808,o(_15790,_15791)))),tt__67_2(_15776)))).
formula(forall([_15689,_15690,_15707,_15708,_15711],or(not(tt_(goal__dnf(a(_15707,_15708),_15711))),not(tt_(dnf_(_15707,o(_15689,_15690)))),tt__67_1(_15708)))).
formula(forall([_15600,_15612],or(not(tt__68_2(_15612)),not(tt__68_3(_15600)),tt__a_68_1_1_2(a(_15600,_15612))))).
formula(forall([_15508,_15520],or(not(tt__68_2(_15520)),not(tt__68_1(_15508)),tt__a_68_1_1_1(a(_15508,_15520))))).
formula(forall([_15416,_15428],or(not(tt__a_68_1_1_1(_15428)),not(tt__a_68_1_1_2(_15416)),tt__o_68_1_1(o(_15428,_15416))))).
formula(forall([_15252,_15264,_15276,_15288,_15300,_15312,_15324,_15336],or(not(tt__o_68_1_1(_15336)),not(tt__a_68_1_1_1(_15324)),not(tt__a_68_1_1_2(_15312)),not(tt__68_4(_15300)),not(tt__68_2(_15288)),not(tt__68_3(_15276)),not(tt__68_2(_15264)),not(tt__68_1(_15252)),tt_(goal__dnf(_15336,_15300))))).
formula(forall([_15133,_15134,_15152,_15166,_15167,_15170],or(not(tt_(goal__dnf(a(_15166,_15167),_15170))),not(tt_(dnf_(_15167,_15152))),not(tt_(dnf_(_15166,o(_15133,_15134)))),tt__68_4(_15170)))).
formula(forall([_15017,_15018,_15036,_15050,_15051,_15054],or(not(tt_(goal__dnf(a(_15050,_15051),_15054))),not(tt_(dnf_(_15051,_15036))),not(tt_(dnf_(_15050,o(_15017,_15018)))),tt__68_3(_15018)))).
formula(forall([_14901,_14902,_14920,_14934,_14935,_14938],or(not(tt_(goal__dnf(a(_14934,_14935),_14938))),not(tt_(dnf_(_14935,_14920))),not(tt_(dnf_(_14934,o(_14901,_14902)))),tt__68_2(_14920)))).
formula(forall([_14785,_14786,_14804,_14818,_14819,_14822],or(not(tt_(goal__dnf(a(_14818,_14819),_14822))),not(tt_(dnf_(_14819,_14804))),not(tt_(dnf_(_14818,o(_14785,_14786)))),tt__68_1(_14785)))).
formula(forall([_14696,_14708],or(not(tt__69_2(_14708)),not(tt__69_1(_14696)),tt__a_69_1_1(a(_14696,_14708))))).
formula(forall([_14580,_14592,_14604,_14616],or(not(tt__a_69_1_1(_14616)),not(tt__69_3(_14604)),not(tt__69_2(_14592)),not(tt__69_1(_14580)),tt_(dnf_(_14616,_14604))))).
formula(forall([_14461,_14462,_14480,_14494,_14495,_14498],or(not(tt_(goal__dnf(a(_14494,_14495),_14498))),not(tt_(dnf_(_14494,_14480))),not(tt_(dnf_(_14495,o(_14461,_14462)))),not(tt_(dnf_(o(a(_14480,_14461),a(_14480,_14462)),_14498))),tt__69_3(_14498)))).
formula(forall([_14321,_14322,_14340,_14354,_14355,_14358],or(not(tt_(goal__dnf(a(_14354,_14355),_14358))),not(tt_(dnf_(_14354,_14340))),not(tt_(dnf_(_14355,o(_14321,_14322)))),not(tt_(dnf_(o(a(_14340,_14321),a(_14340,_14322)),_14358))),tt__69_2(_14355)))).
formula(forall([_14181,_14182,_14200,_14214,_14215,_14218],or(not(tt_(goal__dnf(a(_14214,_14215),_14218))),not(tt_(dnf_(_14214,_14200))),not(tt_(dnf_(_14215,o(_14181,_14182)))),not(tt_(dnf_(o(a(_14200,_14181),a(_14200,_14182)),_14218))),tt__69_1(_14214)))).
formula(forall([_14068,_14080],or(not(tt__70_2(_14080)),not(tt__70_1(_14068)),tt_(goal__dnf(_14068,_14080))))).
formula(forall([_13968,_13982,_13983,_13986],or(not(tt_(goal__dnf(a(_13982,_13983),_13986))),tt__70_2(_13968)))).
formula(forall([_13899,_13900,_13903],or(not(tt_(goal__dnf(a(_13899,_13900),_13903))),tt__70_1(_13899)))).
formula(forall([_13810,_13822],or(not(tt__71_3(_13822)),not(tt__71_2(_13810)),tt__o_71_1_2(o(_13810,_13822))))).
formula(forall([_13694,_13706,_13718,_13730],or(not(tt__o_71_1_2(_13730)),not(tt__71_3(_13718)),not(tt__71_2(_13706)),not(tt__71_1(_13694)),tt_(goal__dnf(_13694,_13730))))).
formula(forall([_13579,_13594,_13608,_13609,_13612],or(not(tt_(goal__dnf(a(_13608,_13609),_13612))),not(tt_(dnf_(_13608,_13594))),tt__71_3(_13579)))).
formula(forall([_13481,_13496,_13510,_13511,_13514],or(not(tt_(goal__dnf(a(_13510,_13511),_13514))),not(tt_(dnf_(_13510,_13496))),tt__71_2(_13481)))).
formula(forall([_13398,_13412,_13413,_13416],or(not(tt_(goal__dnf(a(_13412,_13413),_13416))),not(tt_(dnf_(_13412,_13398))),tt__71_1(_13413)))).
formula(forall([_13308,_13320],or(not(tt__72_3(_13320)),not(tt__72_1(_13308)),tt__a_72_1_1_2(a(_13308,_13320))))).
formula(forall([_13216,_13228],or(not(tt__72_2(_13228)),not(tt__72_1(_13216)),tt__a_72_1_1_1(a(_13216,_13228))))).
formula(forall([_13124,_13136],or(not(tt__a_72_1_1_1(_13136)),not(tt__a_72_1_1_2(_13124)),tt__o_72_1_1(o(_13136,_13124))))).
formula(forall([_12960,_12972,_12984,_12996,_13008,_13020,_13032,_13044],or(not(tt__o_72_1_1(_13044)),not(tt__a_72_1_1_1(_13032)),not(tt__a_72_1_1_2(_13020)),not(tt__72_4(_13008)),not(tt__72_3(_12996)),not(tt__72_1(_12984)),not(tt__72_2(_12972)),not(tt__72_1(_12960)),tt_(goal__dnf(_13044,_13008))))).
formula(forall([_12842,_12856,_12857,_12874,_12875,_12878],or(not(tt_(goal__dnf(a(_12874,_12875),_12878))),not(tt_(dnf_(_12875,o(_12856,_12857)))),not(tt_(dnf_(_12874,_12842))),tt__72_4(_12878)))).
formula(forall([_12726,_12740,_12741,_12758,_12759,_12762],or(not(tt_(goal__dnf(a(_12758,_12759),_12762))),not(tt_(dnf_(_12759,o(_12740,_12741)))),not(tt_(dnf_(_12758,_12726))),tt__72_3(_12741)))).
formula(forall([_12610,_12624,_12625,_12642,_12643,_12646],or(not(tt_(goal__dnf(a(_12642,_12643),_12646))),not(tt_(dnf_(_12643,o(_12624,_12625)))),not(tt_(dnf_(_12642,_12610))),tt__72_2(_12624)))).
formula(forall([_12494,_12508,_12509,_12526,_12527,_12530],or(not(tt_(goal__dnf(a(_12526,_12527),_12530))),not(tt_(dnf_(_12527,o(_12508,_12509)))),not(tt_(dnf_(_12526,_12494))),tt__72_1(_12494)))).
formula(forall([_12404,_12416],or(not(tt__73_2(_12416)),not(tt__73_1(_12404)),tt_(goal__dnf(_12404,_12416))))).
formula(forall([_12322],or(tt__73_2(_12322)))).
formula(forall([_12248],or(tt__73_1(_12248)))).
end_of_list.

list_of_settings(SPASS).
{*
set_flag(Auto,0).
set_flag(Ordering,1).
set_precedence(n,o,a,z9,z8,z7,z6,z5,z4,z3,z2,z1,z0,norm,goal__norm,goal__dnf,dnf_,tt__o_72_1_1,tt__o_71_1_2,tt__o_68_1_1,tt__o_66_1_2,tt__o_54_1_1,tt__o_51_1_1,tt__o_50_1_1,tt__o_47_1_1_1,tt__o_39_1_2,tt__o_39_1_1,tt__o_36_1_1,tt__o_34_1_1_2,tt__o_26_1_2,tt__o_26_1_1,tt__o_25_1_1_1,tt__o_25_1_1,tt__o_24_1_1_2,tt__o_24_1_1,tt__o_21_1_2,tt__o_21_1_1,tt__o_15_1_2,tt__o_15_1_1,tt__n_50_1_1_2,tt__n_50_1_1_1,tt__n_49_1_1,tt__n_48_1_1_2,tt__n_48_1_1_1,tt__n_47_1_1,tt__n_45_1_1_1,tt__n_45_1_1,tt__a_72_1_1_2,tt__a_72_1_1_1,tt__a_69_1_1,tt__a_68_1_1_2,tt__a_68_1_1_1,tt__a_65_1_1,tt__a_64_1_1_2,tt__a_64_1_1_1,tt__a_64_1_1,tt__a_63_1_2,tt__a_62_1_2,tt__a_61_1_1,tt__a_60_1_2,tt__a_58_1_2_1,tt__a_58_1_2,tt__a_58_1_1,tt__a_57_1_2,tt__a_55_1_2_1,tt__a_55_1_2,tt__a_55_1_1,tt__a_49_1_1_1,tt__a_48_1_1,tt__a_42_1_2,tt__a_42_1_1,tt__a_34_1_2,tt__a_34_1_1,tt__a_33_1_1_1,tt__a_33_1_1,tt__a_32_1_1_2,tt__a_32_1_1,tt__a_29_1_2,tt__a_29_1_1,tt__a_28_1_1,tt__a_26_1_1_2,tt__a_18_1_2,tt__a_18_1_1,tt__72_4,tt__72_3,tt__72_2,tt__72_1,tt__71_3,tt__71_2,tt__71_1,tt__70_2,tt__70_1,tt__69_3,tt__69_2,tt__69_1,tt__68_4,tt__68_3,tt__68_2,tt__68_1,tt__67_2,tt__67_1,tt__66_3,tt__66_2,tt__66_1,tt__65_3,tt__65_2,tt__65_1,tt__64_5,tt__64_4,tt__64_3,tt__64_2,tt__64_1,tt__63_3,tt__63_2,tt__63_1,tt__62_3,tt__62_2,tt__62_1,tt__61_3,tt__61_2,tt__61_1,tt__60_3,tt__60_2,tt__60_1,tt__58_4,tt__58_3,tt__58_2,tt__58_1,tt__57_3,tt__57_2,tt__57_1,tt__55_4,tt__55_3,tt__55_2,tt__55_1,tt__54_3,tt__54_2,tt__54_1,tt__53_2,tt__53_1,tt__52_2,tt__52_1,tt__51_3,tt__51_2,tt__51_1,tt__50_3,tt__50_2,tt__50_1,tt__49_3,tt__49_2,tt__49_1,tt__48_3,tt__48_2,tt__48_1,tt__47_3,tt__47_2,tt__47_1,tt__46_2,tt__46_1,tt__45_2,tt__45_1,tt__42_2,tt__42_1,tt__39_2,tt__39_1,tt__37_1,tt__36_3,tt__36_2,tt__36_1,tt__35_2,tt__35_1,tt__34_5,tt__34_4,tt__34_3,tt__34_2,tt__34_1,tt__33_4,tt__33_3,tt__33_2,tt__33_1,tt__32_4,tt__32_3,tt__32_2,tt__32_1,tt__31_2,tt__31_1,tt__29_3,tt__29_2,tt__29_1,tt__28_3,tt__28_2,tt__28_1,tt__27_2,tt__27_1,tt__26_5,tt__26_4,tt__26_3,tt__26_2,tt__26_1,tt__25_4,tt__25_3,tt__25_2,tt__25_1,tt__24_4,tt__24_3,tt__24_2,tt__24_1,tt__23_2,tt__23_1,tt__21_3,tt__21_2,tt__21_1,tt__18_2,tt__18_1,tt__15_2,tt__15_1,tt__13_1,tt_,literal_11_1,literal,goal__literal_59_1,goal__literal_56_1,goal__literal_44_1,goal__literal_43_1,goal__literal_41_1,goal__literal_40_1,goal__literal_38_1,goal__literal_30_1,goal__literal_22_1,goal__literal_20_1,goal__literal_19_1,goal__literal_17_1,goal__literal_16_1,goal__literal_14_1,goal__literal_12_1,goal__literal,tt__73_2,tt__73_1).
*}
end_of_list.
end_problem.
