//[def] __aux_520  :- eq_from__b X,send (P,X,Y),to (E,q82).
//[def] __aux_29 q104.
//[def] __aux_187  :- eq_____Var__13 kxs(X1),to (E,q90).
//[def] __aux_119 q108.
//[def] __aux_222 q91.
//[def] __aux_621  :- eq_M prv(X1),to (E,q60).
//[def] __aux_866 X :- __aux_864 (Y,X,P).
//[def] __aux_872 E :- to (E,q41).
//[def] __aux_171 q104.
//[def] __aux_484 q74.
//[def] __aux_1060 q6.
//[def] __aux_331 E :- to (E,q90).
//[def] __aux_530 q81.
//[def] __aux_308 X3 :- eq_Kab X3.
//[def] __aux_854 q44.
//[def] __aux_612  :- eq_M kxs(X1),to (E,q60).
//[def] __aux_895  :- eq_c__in X,send (P,X,Y),to (E,q38).
//[def] __aux_598 q67.
//[def] __aux_585 X4 :- eq_from__b X4.
//[def] __aux_76  :- eq_____Var__18 __nu(X1,X2),to (E,q107).
//[def] __aux_497  :- eq_____Var__9 __nu(X1,X2),to (E,q80).
//[def] __aux_65 q107.
//[def] __aux_1032 E :- to (E,q13).
//[def] __aux_732 q56.
//[def] __aux_486 q80.
//[def] __aux_447 q78.
//[def] __aux_638 q27.
//[def] __aux_850 q44.
//[def] __aux_355 q74.
//[def] __aux_801 q51.
//[def] __aux_591 nil.
//[def] __aux_852 E :- to (E,q12).
//[def] __aux_778  :- eq_M s(X1),to (E,q54).
//[def] __aux_657 P :- __aux_656 (Y,X,P).
//[def] __aux_847 q47.
//[def] __aux_986 E :- to (E,q24).
//[def] __aux_556 E :- to (E,q73).
//[def] __aux_858 X :- eq_c__out X.
//[def] __aux_1043 q11.
//[def] __aux_1001 cons(X2,cons(X3,nil)) :- eq_initial__knowledge X3,eq_pub__channel X2.
//[def] __aux_238  :- eq_____Var__14 s(X1),to (E,q92).
//[def] __aux_224 q92.
//[def] __aux_913 E :- to (E,q36).
//[def] __aux_572 X :- eq_to__s X.
//[def] __aux_278 q98.
//[def] __aux_969 Y :- eq_s_of_M1_end Y.
//[def] __aux_988 q25.
//[def] __aux_920 E :- to (E,q35).
//[def] __aux_709 q27.
//[def] __aux_179 q8.
//[def] __aux_586 cons(X5,cons(X6,cons(X7,nil))) :- eq_B X6,eq_Kas X7,eq_A X5.
//[def] __aux_814 P :- __aux_813 (Y,X,P).
//[def] __aux_1003 cons(X2,nil) :- eq_initial__knowledge X2.
//[def] __aux_959 E :- to (E,q30).
//[def] __aux_531 q82.
//[def] __aux_143 X7 :- eq_____Var__16 X7.
//[def] __aux_772  :- eq_M pub(X1),to (E,q54).
//[def] __aux_614 q27.
//[def] __aux_843 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q46).
//[def] __aux_906 q37.
//[def] __aux_140 cons(X6,cons(X7,cons(X8,cons(X9,nil)))) :- eq_to__a X9,eq_____Var__17 X6,eq_from__a X8,eq_____Var__16 X7.
//[def] __aux_443  :- eq_____Var__7 s(X1),to (E,q78).
//[def] __aux_186 q91.
//[def] __aux_477 q79.
//[def] __aux_432 q78.
//[def] __aux_18 q106.
//[def] __aux_348 q67.
//[def] __aux_594 q69.
//[def] __aux_917 Y :- __aux_914 (Y,X,P).
//[def] __aux_517  :- eq_Kab Y,eq_____Var__1 crypt(X,Y),to (E,q83).
//[def] __aux_242 q92.
//[def] __aux_314 X6 :- eq_____Var__12 X6.
//[def] __aux_840 q46.
//[def] __aux_925  :- eq_c__in X,send (P,X,Y),to (E,q34).
//[def] __aux_588 cons(X6,cons(X7,nil)) :- eq_Kas X7,eq_B X6.
//[def] __aux_19  :- eq_____Var__16 pub(X1),to (E,q104).
//[def] __aux_748 Y :- __aux_745 (Y,X,P).
//[def] __aux_357 q73.
//[def] __aux_961 q27.
//[def] __aux_1012 q18.
//[def] __aux_956 Y :- __aux_953 (Y,X,P).
//[def] __aux_578 cons(X1,cons(X2,cons(X3,cons(X4,cons(X5,cons(X6,cons(X7,nil))))))) :- eq_from__s X2,eq_from__b X4,eq_B X6,eq_Kas X7,eq_A X5,eq_to__b X3,eq_to__s X1.
//[def] __aux_476  :- eq_____Var__8 nil,to (E,q79).
//[def] __aux_965 E :- to (E,q29).
//[def] __aux_527 Y :- __aux_524 (Y,X,P).
//[def] __aux_400 q74.
//[def] __aux_239 q92.
//[def] __aux_431  :- eq_____Var__7 prv(X1),to (E,q78).
//[def] __aux_294 E :- to (E,q95).
//[def] __aux_312 X5 :- eq_____Var__13 X5.
//[def] __aux_973 E :- to (E,q28).
//[def] __aux_85  :- eq_____Var__18 s(X1),to (E,q107).
//[def] __aux_345 q87.
//[def] __aux_565 P :- __aux_564 (Y,X,P).
//[def] __aux_1035 X :- eq_pub__channel X.
//[def] __aux_77 q107.
//[def] __aux_241  :- eq_____Var__14 nil,to (E,q92).
//[def] __aux_746 P :- __aux_745 (Y,X,P).
//[def] __aux_349 q87.
//[def] __aux_1010 Y :- eq_M Y.
//[def] __aux_125 Y :- eq__oc_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end_cc_kxs_of_A_end Y.
//[def] __aux_976 X :- __aux_974 (Y,X,P).
//[def] __aux_902 Y :- __aux_899 (Y,X,P).
//[def] __aux_696 q27.
//[def] __aux_869  :- eq_c__in X,send (P,X,Y),to (E,q41).
//[def] __aux_356  :- eq_____Var__3 kxs(X1),to (E,q73).
//[def] __aux_286 q96.
//[def] __aux_596 E :- to (E,q66).
//[def] __aux_63 q106.
//[def] __aux_289 (Y,X,P) :- eq_from__a X,send (P,X,Y),to (E,q96).
//[def] __aux_704 Y :- __aux_701 (Y,X,P).
//[def] __aux_742 q55.
//[def] __aux_234 q91.
//[def] __aux_806 X :- __aux_804 (Y,X,P).
//[def] __aux_188 q90.
//[def] __aux_639 E :- to (E,q62).
//[def] __aux_974 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q28).
//[def] __aux_1016  :- eq_pub__channel X,send (P,X,Y),to (E,q17).
//[def] __aux_237 q91.
//[def] __aux_782 q54.
//[def] __aux_275 q97.
//[def] __aux_905 E :- to (E,q37).
//[def] __aux_395  :- eq_____Var__5 acrypt(X1,X2),to (E,q76).
//[def] __aux_970  :- eq_c__in X,send (P,X,Y),to (E,q28).
//[def] __aux_496 q74.
//[def] __aux_928 E :- to (E,q34).
//[def] __aux_75 q106.
//[def] __aux_562 q72.
//[def] __aux_743 q56.
//[def] __aux_924 Y :- eq_cons_of_M1_and_M2_end Y.
//[def] __aux_768 q27.
//[def] __aux_518 q83.
//[def] __aux_700 E :- to (E,q57).
//[def] __aux_20 q104.
//[def] __aux_172 E :- to (E,q102).
//[def] __aux_442 q74.
//[def] __aux_780 q27.
//[def] __aux_333 q89.
//[def] __aux_118  :- eq_____Var__19 s(X1),to (E,q108).
//[def] __aux_834 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q47).
//[def] __aux_181 E :- to (E,q89).
//[def] __aux_130 cons(X1,cons(X2,cons(X3,cons(X4,cons(X5,cons(X6,cons(X7,cons(X8,cons(X9,nil))))))))) :- eq_____Var__19 X2,eq_____Var__18 X4,eq_____Var__17 X6,eq_from__a X8,eq_to__a X9,eq_____Var__16 X7,eq_A X5,eq_B X3,eq_Na X1.
//[def] __aux_93 q106.
//[def] __aux_1004 nil.
//[def] __aux_28  :- eq_____Var__16 nil,to (E,q104).
//[def] __aux_446  :- eq_____Var__7 nil,to (E,q78).
//[def] __aux_898 E :- to (E,q38).
//[def] __aux_388 q74.
//[def] __aux_134 cons(X3,cons(X4,cons(X5,cons(X6,cons(X7,cons(X8,cons(X9,nil))))))) :- eq_to__a X9,eq_from__a X8,eq_B X3,eq_____Var__16 X7,eq_____Var__18 X4,eq_____Var__17 X6,eq_A X5.
//[def] __aux_336 q88.
//[def] __aux_341 X :- __aux_339 (Y,X,P).
//[def] __aux_481 q74.
//[def] __aux_293 q97.
//[def] __aux_223  :- eq_____Var__14 acrypt(X1,X2),to (E,q92).
//[def] __aux_809  :- eq_c__in X,send (P,X,Y),to (E,q50).
//[def] __aux_64  :- eq_____Var__18 kxs(X1),to (E,q107).
//[def] __aux_342 Y :- __aux_339 (Y,X,P).
//[def] __aux_523 E :- to (E,q82).
//[def] __aux_908 X :- eq_c__out X.
//[def] __aux_932 Y :- __aux_929 (Y,X,P).
//[def] __aux_656 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q59).
//[def] __aux_651 E :- to (E,q60).
//[def] __aux_817 q51.
//[def] __aux_444 q78.
//[def] __aux_95 q108.
//[def] __aux_386  :- eq_____Var__5 crypt(X1,X2),to (E,q76).
//[def] __aux_340 P :- __aux_339 (Y,X,P).
//[def] __aux_347 E :- to (E,q67).
//[def] __aux_141 X6 :- eq_____Var__17 X6.
//[def] __aux_645 q61.
//[def] __aux_576 q70.
//[def] __aux_32 q105.
//[def] __aux_328  :- eq_____Var__13 cons(X1,X2),to (E,q90).
//[def] __aux_401  :- eq_____Var__5 __nu(X1,X2),to (E,q76).
//[def] __aux_1058 E :- to (E,q5).
//[def] __aux_667  :- eq_M kxs(X1),to (E,q58).
//[def] __aux_485  :- eq_____Var__9 __eq(X1),to (E,q80).
//[def] __aux_284 q98.
//[def] __aux_1034 q14.
//[def] __aux_930 P :- __aux_929 (Y,X,P).
//[def] __aux_804 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q51).
//[def] __aux_650 q61.
//[def] __aux_641 q27.
//[def] __aux_557  :- eq_Kas Y,eq_____Var__2 crypt(X,Y),to (E,q72).
//[def] __aux_90 q106.
//[def] __aux_593 q68.
//[def] __aux_927 q35.
//[def] __aux_313 cons(X6,cons(X7,cons(X8,cons(X9,nil)))) :- eq_Kbs X9,eq_____Var__12 X6,eq_from__a X8,eq_to__a X7.
//[def] __aux_60 q106.
//[def] __aux_92 q108.
//[def] __aux_450 q79.
//[def] __aux_665 q58.
//[def] __aux_178 E :- to (E,q8).
//[def] __aux_304 X1 :- eq_A X1.
//[def] __aux_731  :- eq_M 0,to (E,q56).
//[def] __aux_1013 q19.
//[def] __aux_741  :- eq_c__in X,send (P,X,Y),to (E,q55).
//[def] __aux_643 Y :- eq_M2 Y.
//[def] __aux_590 cons(X7,nil) :- eq_Kas X7.
//[def] __aux_490 q74.
//[def] __aux_174 q103.
//[def] __aux_69 q106.
//[def] __aux_608 q63.
//[def] __aux_911 q36.
//[def] __aux_736 q27.
//[def] __aux_900 P :- __aux_899 (Y,X,P).
//[def] __aux_114 q106.
//[def] __aux_131 X1 :- eq_Na X1.
//[def] __aux_653 q59.
//[def] __aux_26 q104.
//[def] __aux_658 X :- __aux_656 (Y,X,P).
//[def] __aux_228 q91.
//[def] __aux_1002 X1 :- eq_pub__channel X1.
//[def] __aux_856 q43.
//[def] __aux_145 X8 :- eq_from__a X8.
//[def] __aux_1061 nil.
//[def] __aux_525 P :- __aux_524 (Y,X,P).
//[def] __aux_812 E :- to (E,q50).
//[def] __aux_522 q83.
//[def] __aux_845 X :- __aux_843 (Y,X,P).
//[def] __aux_390 q76.
//[def] __aux_230 q92.
//[def] __aux_14 q104.
//[def] __aux_560  :- eq_from__s X,send (P,X,Y),to (E,q71).
//[def] __aux_848 q46.
//[def] __aux_1015 Y :- eq_M Y.
//[def] __aux_492 q80.
//[def] __aux_71 q107.
//[def] __aux_276 q99.
//[def] __aux_922 q27.
//[def] __aux_480 q80.
//[def] __aux_738 q56.
//[def] __aux_245 q93.
//[def] __aux_897 q39.
//[def] __aux_438 q78.
//[def] __aux_389  :- eq_____Var__5 kxs(X1),to (E,q76).
//[def] __aux_229  :- eq_____Var__14 __nu(X1,X2),to (E,q92).
//[def] __aux_291 X :- __aux_289 (Y,X,P).
//[def] __aux_13  :- eq_____Var__16 prv(X1),to (E,q104).
//[def] __aux_343 q89.
//[def] __aux_1011 E :- to (E,q18).
//[def] __aux_963 Y :- eq_0_of__end Y.
//[def] __aux_1057 nil.
//[def] __aux_491  :- eq_____Var__9 prv(X1),to (E,q80).
//[def] __aux_70  :- eq_____Var__18 acrypt(X1,X2),to (E,q107).
//[def] __aux_558 q72.
//[def] __aux_91  :- eq_____Var__19 crypt(X1,X2),to (E,q108).
//[def] __aux_737  :- eq_M s(X1),to (E,q56).
//[def] __aux_430 q74.
//[def] __aux_691  :- eq_M nil,to (E,q58).
//[def] __aux_353  :- eq_____Var__3 crypt(X1,X2),to (E,q73).
//[def] __aux_563 E :- to (E,q71).
//[def] __aux_394 q74.
//[def] __aux_609  :- eq_M crypt(X1,X2),to (E,q60).
//[def] __aux_384 q75.
//[def] __aux_868 q43.
//[def] __aux_967 q27.
//[def] __aux_402 q76.
//[def] __aux_1008 q20.
//[def] __aux_774 q27.
//[def] __aux_907 q27.
//[def] __aux_315 cons(X7,cons(X8,cons(X9,nil))) :- eq_from__a X8,eq_Kbs X9,eq_to__a X7.
//[def] __aux_344 E :- to (E,q87).
//[def] __aux_192 q91.
//[def] __aux_697  :- eq_c__in X,send (P,X,Y),to (E,q57).
//[def] __aux_117 q106.
//[def] __aux_597 q66.
//[def] __aux_339 (Y,X,P) :- eq_from__a X,send (P,X,Y),to (E,q88).
//[def] __aux_1007 q19.
//[def] __aux_989 q24.
//[def] __aux_177 q102.
//[def] __aux_972 q29.
//[def] __aux_12 q106.
//[def] __aux_406 q74.
//[def] __aux_999 cons(X1,cons(X2,cons(X3,nil))) :- eq_pub__channel X2,eq_initial__knowledge X3,eq_Pid X1.
//[def] __aux_316 X7 :- eq_to__a X7.
//[def] __aux_707  :- eq_M crypt(X1,X2),to (E,q56).
//[def] __aux_864 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q42).
//[def] __aux_94  :- eq_____Var__19 kxs(X1),to (E,q108).
//[def] __aux_915 P :- __aux_914 (Y,X,P).
//[def] __aux_84 q106.
//[def] __aux_770 q54.
//[def] __aux_620 q27.
//[def] __aux_81 q106.
//[def] __aux_616 q60.
//[def] __aux_567 Y :- __aux_564 (Y,X,P).
//[def] __aux_836 X :- __aux_834 (Y,X,P).
//[def] __aux_987 q24.
//[def] __aux_861 q42.
//[def] __aux_350 E :- to (E,q72).
//[def] __aux_570 q70.
//[def] __aux_871 q42.
//[def] __aux_1018 q18.
//[def] __aux_516 Y :- eq__oc_s_of_Nb_end_cc_Kab Y.
//[def] __aux_1050 E :- to (E,q7).
//[def] __aux_184  :- eq_____Var__13 crypt(X1,X2),to (E,q90).
//[def] __aux_445 q74.
//[def] __aux_648  :- eq_M cons(X1,X2),to (E,q60).
//[def] __aux_957 q32.
//[def] __aux_749 q56.
//[def] __aux_142 cons(X7,cons(X8,cons(X9,nil))) :- eq_from__a X8,eq_to__a X9,eq_____Var__16 X7.
//[def] __aux_771 q27.
//[def] __aux_918 q37.
//[def] __aux_1052 q8.
//[def] __aux_1000 X1 :- eq_Pid X1.
//[def] __aux_1036 Y :- eq_initial__knowledge Y.
//[def] __aux_11 q104.
//[def] __aux_337 q89.
//[def] __aux_305 cons(X2,cons(X3,cons(X4,cons(X5,cons(X6,cons(X7,cons(X8,cons(X9,nil)))))))) :- eq_Kab X3,eq_to__a X7,eq_from__a X8,eq_____Var__14 X4,eq_____Var__15 X2,eq_____Var__12 X6,eq_Kbs X9,eq_____Var__13 X5.
//[def] __aux_437  :- eq_____Var__7 pub(X1),to (E,q78).
//[def] __aux_807 Y :- __aux_804 (Y,X,P).
//[def] __aux_1051 q7.
//[def] __aux_783 q27.
//[def] __aux_429 q78.
//[def] __aux_699 q58.
//[def] __aux_306 X2 :- eq_____Var__15 X2.
//[def] __aux_226  :- eq_____Var__14 prv(X1),to (E,q92).
//[def] __aux_23 q104.
//[def] __aux_393 q76.
//[def] __aux_519 q84.
//[def] __aux_566 X :- __aux_564 (Y,X,P).
//[def] __aux_21 q106.
//[def] __aux_835 P :- __aux_834 (Y,X,P).
//[def] __aux_695 q58.
//[def] __aux_1014 X :- eq_pub__channel X.
//[def] __aux_966 q29.
//[def] __aux_334 q90.
//[def] __aux_773 q54.
//[def] __aux_67  :- eq_____Var__18 __eq(X1),to (E,q107).
//[def] __aux_734  :- eq_M nil,to (E,q56).
//[def] __aux_784  :- eq_c__in X,send (P,X,Y),to (E,q53).
//[def] __aux_810 q50.
//[def] __aux_338 E :- to (E,q88).
//[def] __aux_240 q91.
//[def] __aux_191 q90.
//[def] __aux_282  :- eq_Kab Y,eq_____Var__10 crypt(X,Y),to (E,q97).
//[def] __aux_346 q88.
//[def] __aux_280 q98.
//[def] __aux_909 Y :- eq_prv_of_M1_end Y.
//[def] __aux_146 cons(X9,nil) :- eq_to__a X9.
//[def] __aux_176 q101.
//[def] __aux_971 q28.
//[def] __aux_1053 nil.
//[def] __aux_78 q106.
//[def] __aux_873 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q41).
//[def] __aux_776 q54.
//[def] __aux_860  :- eq_c__in X,send (P,X,Y),to (E,q42).
//[def] __aux_1039 q11.
//[def] __aux_89 q107.
//[def] __aux_642 X :- eq_c__out X.
//[def] __aux_808 q52.
//[def] __aux_121 E :- to (E,q110).
//[def] __aux_287 q97.
//[def] __aux_573 Y :- eq_cons_of_A_and_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end_end Y.
//[def] __aux_83 q107.
//[def] __aux_189 q91.
//[def] __aux_80 q107.
//[def] __aux_803 E :- to (E,q51).
//[def] __aux_404  :- eq_____Var__5 pub(X1),to (E,q76).
//[def] __aux_277 E :- to (E,q98).
//[def] __aux_183 q91.
//[def] __aux_745 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q55).
//[def] __aux_290 P :- __aux_289 (Y,X,P).
//[def] __aux_767 q54.
//[def] __aux_962 X :- eq_c__out X.
//[def] __aux_58  :- eq_____Var__17 nil,to (E,q105).
//[def] __aux_870 q41.
//[def] __aux_1017 q17.
//[def] __aux_968 X :- eq_c__out X.
//[def] __aux_838 q48.
//[def] __aux_914 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q36).
//[def] __aux_647 q49.
//[def] __aux_489 q80.
//[def] __aux_173 q102.
//[def] __aux_68 q107.
//[def] __aux_82  :- eq_____Var__18 0,to (E,q107).
//[def] __aux_30 q106.
//[def] __aux_735 q56.
//[def] __aux_479  :- eq_____Var__9 crypt(X1,X2),to (E,q80).
//[def] __aux_113 q108.
//[def] __aux_79  :- eq_____Var__18 pub(X1),to (E,q107).
//[def] __aux_120 q106.
//[def] __aux_524 (Y,X,P) :- eq_from__b X,send (P,X,Y),to (E,q82).
//[def] __aux_933 q35.
//[def] __aux_644 E :- to (E,q61).
//[def] __aux_899 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q38).
//[def] __aux_227 q92.
//[def] __aux_122 q110.
//[def] __aux_396 q76.
//[def] __aux_61  :- eq_____Var__18 crypt(X1,X2),to (E,q107).
//[def] __aux_574 E :- to (E,q69).
//[def] __aux_244  :- eq_____Var__15 crypt(X1,X2),to (E,q93).
//[def] __aux_863 E :- to (E,q42).
//[def] __aux_351 q72.
//[def] __aux_521 q82.
//[def] __aux_66 q106.
//[def] __aux_815 X :- __aux_813 (Y,X,P).
//[def] __aux_1041 E :- to (E,q10).
//[def] __aux_88  :- eq_____Var__18 nil,to (E,q107).
//[def] __aux_733 q27.
//[def] __aux_487 q74.
//[def] __aux_610 q60.
//[def] __aux_448 q74.
//[def] __aux_851 q45.
//[def] __aux_529 E :- to (E,q81).
//[def] __aux_652  :- eq_c__in X,send (P,X,Y),to (E,q59).
//[def] __aux_802 q52.
//[def] __aux_859 Y :- eq__oc_M1_cc_M2 Y.
//[def] __aux_921 q35.
//[def] __aux_190  :- eq_____Var__13 __eq(X1),to (E,q90).
//[def] __aux_115  :- eq_____Var__19 0,to (E,q108).
//[def] __aux_910  :- eq_c__in X,send (P,X,Y),to (E,q36).
//[def] __aux_1037 q13.
//[def] __aux_225 q91.
//[def] __aux_896 q38.
//[def] __aux_528 q83.
//[def] __aux_10  :- eq_____Var__16 acrypt(X1,X2),to (E,q104).
//[def] __aux_279 q99.
//[def] __aux_587 X5 :- eq_A X5.
//[def] __aux_148  :- eq_____Var__19 nil,to (E,q108).
//[def] __aux_844 P :- __aux_843 (Y,X,P).
//[def] __aux_180 q101.
//[def] __aux_926 q34.
//[def] __aux_397 q74.
//[def] __aux_59 q105.
//[def] __aux_649 q60.
//[def] __aux_867 Y :- __aux_864 (Y,X,P).
//[def] __aux_31  :- eq_____Var__17 crypt(X1,X2),to (E,q105).
//[def] __aux_640 q62.
//[def] __aux_903 q39.
//[def] __aux_405 q76.
//[def] __aux_589 X6 :- eq_B X6.
//[def] __aux_660 q60.
//[def] __aux_478 q74.
//[def] __aux_661 E :- to (E,q45).
//[def] __aux_705 q58.
//[def] __aux_433 q74.
//[def] __aux_740 E :- to (E,q56).
//[def] __aux_133 X2 :- eq_____Var__19 X2.
//[def] __aux_283 q97.
//[def] __aux_449  :- eq_____Var__8 crypt(X1,X2),to (E,q79).
//[def] __aux_664  :- eq_M crypt(X1,X2),to (E,q58).
//[def] __aux_243 q91.
//[def] __aux_841 q47.
//[def] __aux_575 q69.
//[def] __aux_978 q29.
//[def] __aux_392  :- eq_____Var__5 __eq(X1),to (E,q76).
//[def] __aux_358 q74.
//[def] __aux_577 q69.
//[def] __aux_929 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q34).
//[def] __aux_22  :- eq_____Var__16 0,to (E,q104).
//[def] __aux_923 X :- eq_c__out X.
//[def] __aux_1056 q7.
//[def] __aux_708 q56.
//[def] __aux_124 X :- eq_to__a X.
//[def] __aux_309 cons(X4,cons(X5,cons(X6,cons(X7,cons(X8,cons(X9,nil)))))) :- eq_____Var__12 X6,eq_to__a X7,eq_from__a X8,eq_Kbs X9,eq_____Var__14 X4,eq_____Var__13 X5.
//[def] __aux_1055 q6.
//[def] __aux_862 q43.
//[def] __aux_571 q71.
//[def] __aux_1006 E :- to (E,q19).
//[def] __aux_839  :- eq_c__in X,send (P,X,Y),to (E,q46).
//[def] __aux_698 q57.
//[def] __aux_579 X1 :- eq_to__s X1.
//[def] __aux_992 q23.
//[def] __aux_833 E :- to (E,q47).
//[def] __aux_332  :- eq_Kbs Y,eq_____Var__12 crypt(X,Y),to (E,q89).
//[def] __aux_617 q27.
//[def] __aux_659 Y :- __aux_656 (Y,X,P).
//[def] __aux_24 q106.
//[def] __aux_185 q90.
//[def] __aux_865 P :- __aux_864 (Y,X,P).
//[def] __aux_17 q104.
//[def] __aux_292 Y :- __aux_289 (Y,X,P).
//[def] __aux_592 E :- to (E,q68).
//[def] __aux_182 q89.
//[def] __aux_662 q45.
//[def] __aux_175 E :- to (E,q101).
//[def] __aux_985 q26.
//[def] __aux_440  :- eq_____Var__7 0,to (E,q78).
//[def] __aux_655 E :- to (E,q59).
//[def] __aux_960 q30.
//[def] __aux_307 cons(X3,cons(X4,cons(X5,cons(X6,cons(X7,cons(X8,cons(X9,nil))))))) :- eq_Kbs X9,eq_from__a X8,eq_Kab X3,eq_to__a X7,eq_____Var__14 X4,eq_____Var__12 X6,eq_____Var__13 X5.
//[def] __aux_288 E :- to (E,q96).
//[def] __aux_439 q74.
//[def] __aux_694  :- eq_M 0,to (E,q58).
//[def] __aux_706 q57.
//[def] __aux_975 P :- __aux_974 (Y,X,P).
//[def] __aux_692 q58.
//[def] __aux_354 q73.
//[def] __aux_916 X :- __aux_914 (Y,X,P).
//[def] __aux_958 q31.
//[def] __aux_123 q111.
//[def] __aux_559 q73.
//[def] __aux_747 X :- __aux_745 (Y,X,P).
//[def] __aux_919 q36.
//[def] __aux_1042 q10.
//[def] __aux_1049 q9.
//[def] __aux_955 X :- __aux_953 (Y,X,P).
//[def] __aux_398  :- eq_____Var__5 prv(X1),to (E,q76).
//[def] __aux_837 Y :- __aux_834 (Y,X,P).
//[def] __aux_352 q74.
//[def] __aux_619 q60.
//[def] __aux_775  :- eq_M 0,to (E,q54).
//[def] __aux_800  :- eq_c__in X,send (P,X,Y),to (E,q51).
//[def] __aux_744 E :- to (E,q55).
//[def] __aux_816 Y :- __aux_813 (Y,X,P).
//[def] __aux_483 q80.
//[def] __aux_407  :- eq_____Var__5 0,to (E,q76).
//[def] __aux_1059 q5.
//[def] __aux_494  :- eq_____Var__9 cons(X1,X2),to (E,q80).
//[def] __aux_73  :- eq_____Var__18 prv(X1),to (E,q107).
//[def] __aux_853 q12.
//[def] __aux_132 cons(X2,cons(X3,cons(X4,cons(X5,cons(X6,cons(X7,cons(X8,cons(X9,nil)))))))) :- eq_B X3,eq_____Var__16 X7,eq_from__a X8,eq_____Var__18 X4,eq_____Var__19 X2,eq_____Var__17 X6,eq_to__a X9,eq_A X5.
//[def] __aux_611 q27.
//[def] __aux_385 q74.
//[def] __aux_403 q74.
//[def] __aux_434  :- eq_____Var__7 __nu(X1,X2),to (E,q78).
//[def] __aux_235  :- eq_____Var__14 0,to (E,q92).
//[def] __aux_221 q92.
//[def] __aux_584 cons(X4,cons(X5,cons(X6,cons(X7,nil)))) :- eq_Kas X7,eq_from__b X4,eq_B X6,eq_A X5.
//[def] __aux_1033 q13.
//[def] __aux_232  :- eq_____Var__14 pub(X1),to (E,q92).
//[def] __aux_990 E :- to (E,q22).
//[def] __aux_96 q106.
//[def] __aux_769  :- eq_M __nu(X1,X2),to (E,q54).
//[def] __aux_335  :- eq_from__a X,send (P,X,Y),to (E,q88).
//[def] __aux_703 X :- __aux_701 (Y,X,P).
//[def] __aux_482  :- eq_____Var__9 kxs(X1),to (E,q80).
//[def] __aux_86 q107.
//[def] __aux_805 P :- __aux_804 (Y,X,P).
//[def] __aux_646 q62.
//[def] __aux_33 q106.
//[def] __aux_441 q78.
//[def] __aux_87 q106.
//[def] __aux_220  :- eq_____Var__14 __eq(X1),to (E,q92).
//[def] __aux_702 P :- __aux_701 (Y,X,P).
//[def] __aux_991 q22.
//[def] __aux_846 Y :- __aux_843 (Y,X,P).
//[def] __aux_62 q107.
//[def] __aux_568 q72.
//[def] __aux_964 q30.
//[def] __aux_25  :- eq_____Var__16 s(X1),to (E,q104).
//[def] __aux_701 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q57).
//[def] __aux_387 q76.
//[def] __aux_811 q51.
//[def] __aux_904 q38.
//[def] __aux_1009 X :- eq_pub__channel X.
//[def] __aux_901 X :- __aux_899 (Y,X,P).
//[def] __aux_488  :- eq_____Var__9 acrypt(X1,X2),to (E,q80).
//[def] __aux_116 q108.
//[def] __aux_329 q90.
//[def] __aux_618  :- eq_M acrypt(X1,X2),to (E,q60).
//[def] __aux_451 q74.
//[def] __aux_666 q27.
//[def] __aux_813 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q50).
//[def] __aux_144 cons(X8,cons(X9,nil)) :- eq_to__a X9,eq_from__a X8.
//[def] __aux_777 q27.
//[def] __aux_595 q68.
//[def] __aux_526 X :- __aux_524 (Y,X,P).
//[def] __aux_615  :- eq_M __eq(X1),to (E,q60).
//[def] __aux_849 E :- to (E,q44).
//[def] __aux_1038 E :- to (E,q11).
//[def] __aux_1054 E :- to (E,q6).
//[def] __aux_233 q92.
//[def] __aux_1005 q21.
//[def] __aux_912 q37.
//[def] __aux_569 E :- to (E,q70).
//[def] __aux_654 q60.
//[def] __aux_281 q100.
//[def] __aux_27 q106.
//[def] __aux_435 q78.
//[def] __aux_663 q59.
//[def] __aux_236 q92.
//[def] __aux_285  :- eq_from__a X,send (P,X,Y),to (E,q96).
//[def] __aux_613 q60.
//[def] __aux_693 q27.
//[def] __aux_781  :- eq_M nil,to (E,q54).
//[def] __aux_857 q27.
//[def] __aux_1040 q12.
//[def] __aux_436 q74.
//[def] __aux_931 X :- __aux_929 (Y,X,P).
//[def] __aux_147 nil.
//[def] __aux_495 q80.
//[def] __aux_74 q107.
//[def] __aux_561 q71.
//[def] __aux_564 (Y,X,P) :- eq_from__s X,send (P,X,Y),to (E,q71).
//[def] __aux_359  :- eq_____Var__3 __eq(X1),to (E,q73).
//[def] __aux_391 q74.
//[def] __aux_231 q91.
//[def] __aux_15 q106.
//[def] __aux_842 E :- to (E,q46).
//[def] __aux_515 X :- eq_to__b X.
//[def] __aux_493 q74.
//[def] __aux_72 q106.
//[def] __aux_977 Y :- __aux_974 (Y,X,P).
//[def] __aux_739 q49.
//[def] __aux_330 q92.
//[def] __aux_16  :- eq_____Var__16 __nu(X1,X2),to (E,q104).
//[def] __aux_246 q91.
//[def] __aux_855 E :- to (E,q43).
//[def] __aux_399 q76.
//[def] __aux_779 q54.
//[def] __aux_555 q75.
//[def] __aux_298 Y :- eq__oc_Nb_cc_Kab Y.
//[def] __aux_467  :- eq_____Var__8 pub(X1),to (E,q79).
//[def] __aux_549 q77.
//[def] __aux_1031 q15.
//[def] __aux_456 q79.
//[def] __aux_413  :- eq_____Var__5 nil,to (E,q76).
//[def] __aux_470  :- eq_____Var__8 0,to (E,q79).
//[def] __aux_791 Y :- __aux_788 (Y,X,P).
//[def] __aux_6 q106.
//[def] __aux_207 q91.
//[def] __aux_581 X2 :- eq_from__s X2.
//[def] __aux_138 cons(X5,cons(X6,cons(X7,cons(X8,cons(X9,nil))))) :- eq_from__a X8,eq_____Var__17 X6,eq_____Var__16 X7,eq_to__a X9,eq_A X5.
//[def] __aux_600 q65.
//[def] __aux_469 q74.
//[def] __aux_682  :- eq_M __nu(X1,X2),to (E,q58).
//[def] __aux_152 q107.
//[def] __aux_629 q27.
//[def] __aux_204 q91.
//[def] __aux_382 q74.
//[def] __aux_894 q40.
//[def] __aux_454 q74.
//[def] __aux_995 E :- to (E,q21).
//[def] __aux_209 q90.
//[def] __aux_43  :- eq_____Var__17 prv(X1),to (E,q105).
//[def] __aux_167 (Y,X,P) :- eq_from__a X,send (P,X,Y),to (E,q103).
//[def] __aux_366 q73.
//[def] __aux_156 q105.
//[def] __aux_510 q83.
//[def] __aux_211  :- eq_____Var__13 nil,to (E,q90).
//[def] __aux_370 q74.
//[def] __aux_326 q93.
//[def] __aux_532 X :- eq_to__b X.
//[def] __aux_1021 P :- __aux_1020 (Y,X,P).
//[def] __aux_890 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q39).
//[def] __aux_193  :- eq_____Var__13 acrypt(X1,X2),to (E,q90).
//[def] __aux_943 q33.
//[def] __aux_57 q106.
//[def] __aux_711 q56.
//[def] __aux_677 q58.
//[def] __aux_630  :- eq_M 0,to (E,q60).
//[def] __aux_255 q91.
//[def] __aux_320 nil.
//[def] __aux_940 X :- __aux_938 (Y,X,P).
//[def] __aux_993 X :- eq_pub__channel X.
//[def] __aux_795 q52.
//[def] __aux_550 E :- to (E,q76).
//[def] __aux_887 q39.
//[def] __aux_419  :- eq_____Var__7 crypt(X1,X2),to (E,q78).
//[def] __aux_271  :- eq_____Var__15 s(X1),to (E,q93).
//[def] __aux_257 q93.
//[def] __aux_1029 X :- eq_pub__channel X.
//[def] __aux_668 q58.
//[def] __aux_712 q27.
//[def] __aux_98 q108.
//[def] __aux_325 q92.
//[def] __aux_383 E :- to (E,q75).
//[def] __aux_882 q40.
//[def] __aux_818 q50.
//[def] __aux_165 q104.
//[def] __aux_212 q90.
//[def] __aux_418 q74.
//[def] __aux_44 q105.
//[def] __aux_256  :- eq_____Var__15 prv(X1),to (E,q93).
//[def] __aux_110 q108.
//[def] __aux_150 q109.
//[def] __aux_97  :- eq_____Var__19 __eq(X1),to (E,q108).
//[def] __aux_1067 q3.
//[def] __aux_828 q48.
//[def] __aux_721 q27.
//[def] __aux_627  :- eq_M pub(X1),to (E,q60).
//[def] __aux_466 q74.
//[def] __aux_1026 E :- to (E,q15).
//[def] __aux_168 P :- __aux_167 (Y,X,P).
//[def] __aux_42 q106.
//[def] __aux_676  :- eq_M prv(X1),to (E,q58).
//[def] __aux_468 q79.
//[def] __aux_874 P :- __aux_873 (Y,X,P).
//[def] __aux_514 q86.
//[def] __aux_750 q55.
//[def] __aux_414 q76.
//[def] __aux_323 q94.
//[def] __aux_604 q65.
//[def] __aux_219 q91.
//[def] __aux_752 q54.
//[def] __aux_820 q48.
//[def] __aux_151  :- eq_____Var__18 cons(X1,X2),to (E,q107).
//[def] __aux_1064 q5.
//[def] __aux_687 q27.
//[def] __aux_508 q74.
//[def] __aux_540 E :- to (E,q79).
//[def] __aux_417 q77.
//[def] __aux_327 E :- to (E,q92).
//[def] __aux_455  :- eq_____Var__8 __eq(X1),to (E,q79).
//[def] __aux_710  :- eq_M kxs(X1),to (E,q56).
//[def] __aux_686 q58.
//[def] __aux_409 q74.
//[def] __aux_272 q93.
//[def] __aux_427 q74.
//[def] __aux_764 q54.
//[def] __aux_5 q104.
//[def] __aux_422  :- eq_____Var__7 kxs(X1),to (E,q78).
//[def] __aux_365  :- eq_____Var__3 prv(X1),to (E,q73).
//[def] __aux_824 q27.
//[def] __aux_194 q90.
//[def] __aux_208  :- eq_____Var__13 s(X1),to (E,q90).
//[def] __aux_270 q91.
//[def] __aux_300 q94.
//[def] __aux_762 q27.
//[def] __aux_1  :- eq_____Var__16 crypt(X1,X2),to (E,q104).
//[def] __aux_267 q91.
//[def] __aux_582 cons(X3,cons(X4,cons(X5,cons(X6,cons(X7,nil))))) :- eq_B X6,eq_from__b X4,eq_to__b X3,eq_Kas X7,eq_A X5.
//[def] __aux_689 q58.
//[def] __aux_758 q54.
//[def] __aux_499 q74.
//[def] __aux_263 q93.
//[def] __aux_310 X4 :- eq_____Var__14 X4.
//[def] __aux_681 q27.
//[def] __aux_261 q91.
//[def] __aux_371  :- eq_____Var__3 pub(X1),to (E,q73).
//[def] __aux_199  :- eq_____Var__13 __nu(X1,X2),to (E,q90).
//[def] __aux_8 q104.
//[def] __aux_756 q27.
//[def] __aux_101 q108.
//[def] __aux_2 q104.
//[def] __aux_296 q96.
//[def] __aux_136 cons(X4,cons(X5,cons(X6,cons(X7,cons(X8,cons(X9,nil)))))) :- eq_____Var__17 X6,eq_____Var__16 X7,eq_from__a X8,eq_to__a X9,eq_____Var__18 X4,eq_A X5.
//[def] __aux_501 q80.
//[def] __aux_945 q32.
//[def] __aux_421 q74.
//[def] __aux_799 q49.
//[def] __aux_1073 q1.
//[def] __aux_832 q48.
//[def] __aux_504 q80.
//[def] __aux_160 q104.
//[def] __aux_950 q31.
//[def] __aux_428  :- eq_____Var__7 acrypt(X1,X2),to (E,q78).
//[def] __aux_410  :- eq_____Var__5 s(X1),to (E,q76).
//[def] __aux_884 X :- eq_c__out X.
//[def] __aux_717 q56.
//[def] __aux_462 q79.
//[def] __aux_36 q106.
//[def] __aux_670  :- eq_M __eq(X1),to (E,q58).
//[def] __aux_4  :- eq_____Var__16 kxs(X1),to (E,q104).
//[def] __aux_302 q94.
//[def] __aux_379 q74.
//[def] __aux_163  :- eq_from__a X,send (P,X,Y),to (E,q103).
//[def] __aux_375 q73.
//[def] __aux_728  :- eq_M pub(X1),to (E,q56).
//[def] __aux_139 X5 :- eq_A X5.
//[def] __aux_605 E :- to (E,q63).
//[def] __aux_1065 nil.
//[def] __aux_49  :- eq_____Var__17 pub(X1),to (E,q105).
//[def] __aux_103  :- eq_____Var__19 prv(X1),to (E,q108).
//[def] __aux_250  :- eq_____Var__15 __eq(X1),to (E,q93).
//[def] __aux_38 q105.
//[def] __aux_1047 q9.
//[def] __aux_52  :- eq_____Var__17 0,to (E,q105).
//[def] __aux_360 q73.
//[def] __aux_714 q56.
//[def] __aux_953 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q31).
//[def] __aux_947 X :- eq_c__out X.
//[def] __aux_880 q41.
//[def] __aux_364 q74.
//[def] __aux_460 q74.
//[def] __aux_715 q27.
//[def] __aux_1074 q2.
//[def] __aux_892 X :- __aux_890 (Y,X,P).
//[def] __aux_789 P :- __aux_788 (Y,X,P).
//[def] __aux_606 q63.
//[def] __aux_935 q33.
//[def] __aux_127 q109.
//[def] __aux_37  :- eq_____Var__17 __eq(X1),to (E,q105).
//[def] __aux_821 q27.
//[def] __aux_1019 E :- to (E,q17).
//[def] __aux_215 q92.
//[def] __aux_998 q21.
//[def] __aux_372 q73.
//[def] __aux_200 q90.
//[def] __aux_299 E :- to (E,q94).
//[def] __aux_166 E :- to (E,q103).
//[def] __aux_996 q21.
//[def] __aux_1071 q2.
//[def] __aux_826 Y :- eq_M1 Y.
//[def] __aux_716  :- eq_M acrypt(X1,X2),to (E,q56).
//[def] __aux_461  :- eq_____Var__8 prv(X1),to (E,q79).
//[def] __aux_544 E :- to (E,q78).
//[def] __aux_9 q106.
//[def] __aux_374  :- eq_____Var__3 0,to (E,q73).
//[def] __aux_1072 q3.
//[def] __aux_787 E :- to (E,q53).
//[def] __aux_538 q79.
//[def] __aux_938 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q33).
//[def] __aux_511 q85.
//[def] __aux_198 q91.
//[def] __aux_317 cons(X8,cons(X9,nil)) :- eq_Kbs X9,eq_from__a X8.
//[def] __aux_583 X3 :- eq_to__b X3.
//[def] __aux_475 q74.
//[def] __aux_1023 Y :- __aux_1020 (Y,X,P).
//[def] __aux_669 q27.
//[def] __aux_509 E :- to (E,q83).
//[def] __aux_723 q56.
//[def] __aux_546 q78.
//[def] __aux_513 q84.
//[def] __aux_727 q27.
//[def] __aux_552 q76.
//[def] __aux_262  :- eq_____Var__15 __nu(X1,X2),to (E,q93).
//[def] __aux_50 q105.
//[def] __aux_104 q108.
//[def] __aux_876 Y :- __aux_873 (Y,X,P).
//[def] __aux_994 Y :- eq_N Y.
//[def] __aux_757  :- eq_M __eq(X1),to (E,q54).
//[def] __aux_251 q93.
//[def] __aux_53 q105.
//[def] __aux_108 q106.
//[def] __aux_1045 cons(X1,cons(X2,nil)) :- eq_initial__knowledge X2,eq_pub__channel X1.
//[def] __aux_411 q76.
//[def] __aux_500  :- eq_____Var__9 pub(X1),to (E,q80).
//[def] __aux_503  :- eq_____Var__9 0,to (E,q80).
//[def] __aux_249 q91.
//[def] __aux_671 q58.
//[def] __aux_48 q106.
//[def] __aux_543 q79.
//[def] __aux_169 X :- __aux_167 (Y,X,P).
//[def] __aux_129 q109.
//[def] __aux_942 q34.
//[def] __aux_690 q27.
//[def] __aux_1062 E :- to (E,q4).
//[def] __aux_1022 X :- __aux_1020 (Y,X,P).
//[def] __aux_535 q80.
//[def] __aux_722  :- eq_M cons(X1,X2),to (E,q56).
//[def] __aux_195 q91.
//[def] __aux_672 q27.
//[def] __aux_137 X4 :- eq_____Var__18 X4.
//[def] __aux_301 q95.
//[def] __aux_632 q27.
//[def] __aux_537  :- eq_____Var__8 cons(X1,X2),to (E,q79).
//[def] __aux_367 q74.
//[def] __aux_875 X :- __aux_873 (Y,X,P).
//[def] __aux_362  :- eq_____Var__3 acrypt(X1,X2),to (E,q73).
//[def] __aux_458  :- eq_____Var__8 acrypt(X1,X2),to (E,q79).
//[def] __aux_788 (Y,X,P) :- eq_c__in X,send (P,X,Y),to (E,q53).
//[def] __aux_753 q27.
//[def] __aux_823 q49.
//[def] __aux_34  :- eq_____Var__17 kxs(X1),to (E,q105).
//[def] __aux_984 Y :- eq_nil_of__end Y.
//[def] __aux_377  :- eq_____Var__3 s(X1),to (E,q73).
//[def] __aux_423 q78.
//[def] __aux_793 q53.
//[def] __aux_830  :- eq_c__in X,send (P,X,Y),to (E,q47).
//[def] __aux_162 E :- to (E,q104).
//[def] __aux_952 E :- to (E,q31).
//[def] __aux_786 q54.
//[def] __aux_983 X :- eq_c__out X.
//[def] __aux_214  :- eq_____Var__14 crypt(X1,X2),to (E,q92).
//[def] __aux_197 q90.
//[def] __aux_688  :- eq_M s(X1),to (E,q58).
//[def] __aux_934  :- eq_c__in X,send (P,X,Y),to (E,q33).
//[def] __aux_273 q91.
//[def] __aux_765 q27.
//[def] __aux_474 q79.
//[def] __aux_883 q27.
//[def] __aux_213 q91.
//[def] __aux_675 q27.
//[def] __aux_45 q106.
//[def] __aux_545 q77.
//[def] __aux_679  :- eq_M cons(X1,X2),to (E,q58).
//[def] __aux_948 Y :- eq_pub_of_M1_end Y.
//[def] __aux_726 q56.
//[def] __aux_551 q75.
//[def] __aux_982 q27.
//[def] __aux_792 q54.
//[def] __aux_624  :- eq_M __nu(X1,X2),to (E,q60).
//[def] __aux_1069 nil.
//[def] __aux_829 q49.
//[def] __aux_763  :- eq_M prv(X1),to (E,q54).
//[def] __aux_105 q106.
//[def] __aux_107 q108.
//[def] __aux_724 q27.
//[def] __aux_321  :- eq_____Var__15 nil,to (E,q93).
//[def] __aux_794 E :- to (E,q52).
//[def] __aux_825 X :- eq_c__out X.
//[def] __aux_881 E :- to (E,q40).
//[def] __aux_415 q74.
//[def] __aux_472 q74.
//[def] __aux_602 E :- to (E,q64).
//[def] __aux_754  :- eq_M kxs(X1),to (E,q54).
//[def] __aux_248 q93.
//[def] __aux_47 q105.
//[def] __aux_1068 q4.
//[def] __aux_542 q78.
//[def] __aux_259  :- eq_____Var__15 cons(X1,X2),to (E,q93).
//[def] __aux_111 q106.
//[def] __aux_622 q60.
//[def] __aux_944 E :- to (E,q32).
//[def] __aux_1025 q17.
//[def] __aux_457 q74.
//[def] __aux_318 X8 :- eq_from__a X8.
//[def] __aux_247  :- eq_____Var__15 kxs(X1),to (E,q93).
//[def] __aux_35 q105.
//[def] __aux_378 q73.
//[def] __aux_601 q66.
//[def] __aux_153 q108.
//[def] __aux_46  :- eq_____Var__17 __nu(X1,X2),to (E,q105).
//[def] __aux_541  :- eq_____Var__7 cons(X1,X2),to (E,q78).
//[def] __aux_1030 Y :- eq_id Y.
//[def] __aux_512 E :- to (E,q84).
//[def] __aux_1028 q16.
//[def] __aux_533 Y :- eq_M Y.
//[def] __aux_210 q91.
//[def] __aux_303 cons(X1,cons(X2,cons(X3,cons(X4,cons(X5,cons(X6,cons(X7,cons(X8,cons(X9,nil))))))))) :- eq_____Var__15 X2,eq_____Var__14 X4,eq_____Var__12 X6,eq_from__a X8,eq_Kbs X9,eq_to__a X7,eq_____Var__13 X5,eq_Kab X3,eq_A X1.
//[def] __aux_106  :- eq_____Var__19 cons(X1,X2),to (E,q108).
//[def] __aux_607 q64.
//[def] __aux_424 q74.
//[def] __aux_879 q25.
//[def] __aux_157 q107.
//[def] __aux_363 q73.
//[def] __aux_126 E :- to (E,q109).
//[def] __aux_459 q79.
//[def] __aux_949  :- eq_c__in X,send (P,X,Y),to (E,q31).
//[def] __aux_159  :- eq_____Var__16 cons(X1,X2),to (E,q104).
//[def] __aux_473  :- eq_____Var__8 s(X1),to (E,q79).
//[def] __aux_941 Y :- __aux_938 (Y,X,P).
//[def] __aux_311 cons(X5,cons(X6,cons(X7,cons(X8,cons(X9,nil))))) :- eq_from__a X8,eq_____Var__12 X6,eq_to__a X7,eq_Kbs X9,eq_____Var__13 X5.
//[def] __aux_260 q93.
//[def] __aux_766  :- eq_M cons(X1,X2),to (E,q54).
//[def] __aux_790 X :- __aux_788 (Y,X,P).
//[def] __aux_755 q54.
//[def] __aux_295 q95.
//[def] __aux_678 q27.
//[def] __aux_937 E :- to (E,q33).
//[def] __aux_534  :- eq_____Var__9 nil,to (E,q80).
//[def] __aux_420 q78.
//[def] __aux_109  :- eq_____Var__19 __nu(X1,X2),to (E,q108).
//[def] __aux_713  :- eq_M __eq(X1),to (E,q56).
//[def] __aux_798 q52.
//[def] __aux_831 q47.
//[def] __aux_891 P :- __aux_890 (Y,X,P).
//[def] __aux_536 q81.
//[def] __aux_796 q27.
//[def] __aux_888 q40.
//[def] __aux_196  :- eq_____Var__13 prv(X1),to (E,q90).
//[def] __aux_680 q58.
//[def] __aux_258 q91.
//[def] __aux_827  :- eq_M2 Y,eq_M crypt(X,Y),to (E,q48).
//[def] __aux_625 q60.
//[def] __aux_99 q106.
//[def] __aux_102 q106.
//[def] __aux_154 E :- to (E,q107).
//[def] __aux_498 q80.
//[def] __aux_416 E :- to (E,q77).
//[def] __aux_730 q27.
//[def] __aux_886  :- eq_c__in X,send (P,X,Y),to (E,q39).
//[def] __aux_135 X3 :- eq_B X3.
//[def] __aux_319 cons(X9,nil) :- eq_Kbs X9.
//[def] __aux_981 q26.
//[def] __aux_56 q105.
//[def] __aux_980 E :- to (E,q26).
//[def] __aux_268  :- eq_____Var__15 0,to (E,q93).
//[def] __aux_412 q74.
//[def] __aux_760  :- eq_M acrypt(X1,X2),to (E,q54).
//[def] __aux_254 q93.
//[def] __aux_265  :- eq_____Var__15 pub(X1),to (E,q93).
//[def] __aux_683 q58.
//[def] __aux_633  :- eq_M s(X1),to (E,q60).
//[def] __aux_506  :- eq_____Var__9 s(X1),to (E,q80).
//[def] __aux_274 E :- to (E,q97).
//[def] __aux_1066 E :- to (E,q3).
//[def] __aux_425  :- eq_____Var__7 __eq(X1),to (E,q78).
//[def] __aux_51 q106.
//[def] __aux_685  :- eq_M pub(X1),to (E,q58).
//[def] __aux_322 q93.
//[def] __aux_297 X :- eq_to__a X.
//[def] __aux_252 q91.
//[def] __aux_674 q58.
//[def] __aux_1044 q10.
//[def] __aux_54 q106.
//[def] __aux_217  :- eq_____Var__14 kxs(X1),to (E,q92).
//[def] __aux_453 q79.
//[def] __aux_936 q34.
//[def] __aux_112  :- eq_____Var__19 pub(X1),to (E,q108).
//[def] __aux_719  :- eq_M prv(X1),to (E,q56).
//[def] __aux_464  :- eq_____Var__8 __nu(X1,X2),to (E,q79).
//[def] __aux_1046 E :- to (E,q9).
//[def] __aux_216 q91.
//[def] __aux_373 q74.
//[def] __aux_201 q91.
//[def] __aux_997 q22.
//[def] __aux_369 q73.
//[def] __aux_636  :- eq_M nil,to (E,q60).
//[def] __aux_206 q90.
//[def] __aux_155  :- eq_____Var__17 cons(X1,X2),to (E,q105).
//[def] __aux_628 q60.
//[def] __aux_203 q90.
//[def] __aux_939 P :- __aux_938 (Y,X,P).
//[def] __aux_381 q73.
//[def] __aux_539 q80.
//[def] __aux_1070 E :- to (E,q2).
//[def] __aux_599 E :- to (E,q65).
//[def] __aux_548 q76.
//[def] __aux_40  :- eq_____Var__17 acrypt(X1,X2),to (E,q105).
//[def] __aux_554 q73.
//[def] __aux_893 Y :- __aux_890 (Y,X,P).
//[def] __aux_218 q92.
//[def] __aux_623 q27.
//[def] __aux_205  :- eq_____Var__13 0,to (E,q90).
//[def] __aux_725  :- eq_M __nu(X1,X2),to (E,q56).
//[def] __aux_759 q27.
//[def] __aux_128 q110.
//[def] __aux_264 q91.
//[def] __aux_202  :- eq_____Var__13 pub(X1),to (E,q90).
//[def] __aux_380  :- eq_____Var__3 nil,to (E,q73).
//[def] __aux_507 q80.
//[def] __aux_471 q79.
//[def] __aux_408 q76.
//[def] __aux_547  :- eq_____Var__5 cons(X1,X2),to (E,q76).
//[def] __aux_797  :- eq_inv_M2 Y,eq_M crypt(X,Y),to (E,q52).
//[def] __aux_631 q60.
//[def] __aux_822 E :- to (E,q49).
//[def] __aux_426 q78.
//[def] __aux_553  :- eq_____Var__3 cons(X1,X2),to (E,q73).
//[def] __aux_170 Y :- __aux_167 (Y,X,P).
//[def] __aux_1024 q18.
//[def] __aux_979 q28.
//[def] __aux_729 q56.
//[def] __aux_684 q27.
//[def] __aux_885 Y :- eq__ob_M1_cb_M2 Y.
//[def] __aux_368  :- eq_____Var__3 __nu(X1,X2),to (E,q73).
//[def] __aux_158 E :- to (E,q105).
//[def] __aux_3 q106.
//[def] __aux_819 E :- to (E,q48).
//[def] __aux_269 q93.
//[def] __aux_761 q54.
//[def] __aux_502 q74.
//[def] __aux_635 q27.
//[def] __aux_266 q93.
//[def] __aux_452  :- eq_____Var__8 kxs(X1),to (E,q79).
//[def] __aux_946 q27.
//[def] __aux_877 q42.
//[def] __aux_751  :- eq_M crypt(X1,X2),to (E,q54).
//[def] __aux_634 q60.
//[def] __aux_505 q74.
//[def] __aux_161 q105.
//[def] __aux_55  :- eq_____Var__17 s(X1),to (E,q105).
//[def] __aux_41 q105.
//[def] __aux_951 q32.
//[def] __aux_580 cons(X2,cons(X3,cons(X4,cons(X5,cons(X6,cons(X7,nil)))))) :- eq_to__b X3,eq_Kas X7,eq_from__b X4,eq_from__s X2,eq_B X6,eq_A X5.
//[def] __aux_253  :- eq_____Var__15 acrypt(X1,X2),to (E,q93).
//[def] __aux_1027 q15.
//[def] __aux_626 q27.
//[def] __aux_1020 (Y,X,P) :- eq_pub__channel X,send (P,X,Y),to (E,q17).
//[def] __aux_1063 q4.
//[def] __aux_718 q27.
//[def] __aux_637 q60.
//[def] __aux_463 q74.
//[def] __aux_324  :- eq_____Var__14 cons(X1,X2),to (E,q92).
//[def] __aux_785 q53.
//[def] __aux_7  :- eq_____Var__16 __eq(X1),to (E,q104).
//[def] __aux_376 q74.
//[def] __aux_603 q64.
//[def] __aux_149 q108.
//[def] __aux_878 E :- to (E,q25).
//[def] __aux_720 q56.
//[def] __aux_465 q79.
//[def] __aux_954 P :- __aux_953 (Y,X,P).
//[def] __aux_100  :- eq_____Var__19 acrypt(X1,X2),to (E,q108).
//[def] __aux_39 q106.
//[def] __aux_1048 q10.
//[def] __aux_673  :- eq_M acrypt(X1,X2),to (E,q58).
//[def] __aux_361 q74.
//[def] __aux_889 E :- to (E,q39).
//[def] __aux_164 q103.
__aux_520.
__aux_29(q104).
__aux_119(q108).
__aux_222(q91).
__aux_171(q104).
__aux_484(q74).
__aux_1060(q6).
__aux_331(q89).
__aux_530(q81).
__aux_308(__nu(X1,X2)) :- __aux_129(X1), __aux_130(X2).
__aux_854(q44).
__aux_598(q67).
__aux_585(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
eq_Kas(__nu(X1,X2)) :- __aux_1055(X1), __aux_1057(X2).
eq_Kas(kxs(X)) :- eq_A(X).
__aux_65(q107).
__aux_1032(q12).
__aux_732(q56).
__aux_486(q80).
__aux_447(q78).
__aux_638(q27).
__aux_850(q44).
__aux_355(q74).
__aux_801(q51).
__aux_591(nil).
__aux_852(q11).
eq_0_of__end(0).
__aux_847(q47).
__aux_986(q12).
__aux_556(q72).
__aux_1043(q11).
__aux_1001(cons(X1,X2)) :- __aux_1002(X1), __aux_1003(X2).
__aux_224(q92).
__aux_572(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_278(q98).
__aux_988(q25).
__aux_709(q27).
__aux_179(q8).
__aux_586(cons(X1,X2)) :- __aux_587(X1), __aux_588(X2).
__aux_1003(cons(X1,X2)) :- eq_initial__knowledge(X1), __aux_1004(X2).
__aux_531(q82).
__aux_143(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_143(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_143(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_143(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_143(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_143(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_143(0).
__aux_143(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_614(q27).
__aux_906(q37).
__aux_140(cons(X1,X2)) :- __aux_141(X1), __aux_142(X2).
__aux_186(q91).
__aux_477(q79).
__aux_432(q78).
__aux_18(q106).
__aux_348(q67).
eq_____Var__4(__nu(X1,X2)) :- __aux_577(X1), __aux_578(X2).
__aux_594(q69).
__aux_517.
__aux_242(q92).
__aux_314(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_314(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_314(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_314(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_314(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_314(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_314(0).
__aux_314(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_840(q46).
__aux_588(cons(X1,X2)) :- __aux_589(X1), __aux_590(X2).
__aux_357(q73).
__aux_961(q27).
__aux_1012(q18).
__aux_578(cons(X1,X2)) :- __aux_579(X1), __aux_580(X2).
__aux_527(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_527(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_527(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_527(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_527(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_527(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_527(0).
__aux_527(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_400(q74).
__aux_239(q92).
__aux_294(q94).
__aux_312(cons(X1,X2)) :- eq_Kab(X1), eq_cons_of_A_and_nil_of__end_end(X2).
__aux_345(q87).
__aux_565(q81).
__aux_565(q84).
__aux_565(q70).
__aux_565(q22).
__aux_565(q95).
__aux_565(q15).
__aux_565(q13).
__aux_565(q19).
__aux_565(q110).
__aux_565(q18).
__aux_1035(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_77(q107).
__aux_349(q87).
__aux_1010(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_1010(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_1010(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_1010(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_1010(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_1010(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_1010(0).
__aux_1010(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_125(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_696(q27).
__aux_286(q96).
__aux_596(q65).
__aux_63(q106).
__aux_289(X1,X2,X3) :- __aux_1010(X1), __aux_1009(X2), eq_from__a(X2), __aux_1007(X3).
__aux_289(X1,X2,X3) :- __aux_994(X1), __aux_993(X2), eq_from__a(X2), __aux_991(X3).
__aux_289(X1,X2,X3) :- __aux_573(X1), __aux_572(X2), eq_from__a(X2), __aux_570(X3).
__aux_289(X1,X2,X3) :- __aux_298(X1), eq_from__a(X2), __aux_297(X2), __aux_295(X3).
__aux_289(X1,X2,X3) :- __aux_1030(X1), __aux_1029(X2), eq_from__a(X2), __aux_1027(X3).
__aux_289(X1,X2,X3) :- __aux_1036(X1), __aux_1035(X2), eq_from__a(X2), __aux_1033(X3).
__aux_289(X1,X2,X3) :- __aux_533(X1), __aux_532(X2), eq_from__a(X2), __aux_530(X3).
__aux_289(X1,X2,X3) :- __aux_1015(X1), __aux_1014(X2), eq_from__a(X2), __aux_1012(X3).
__aux_289(X1,X2,X3) :- __aux_125(X1), __aux_124(X2), eq_from__a(X2), __aux_122(X3).
__aux_289(X1,X2,X3) :- __aux_516(X1), __aux_515(X2), eq_from__a(X2), __aux_513(X3).
eq_to__b(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_742(q55).
__aux_234(q91).
__aux_188(q90).
__aux_1016.
__aux_237(q91).
__aux_782(q54).
__aux_275(q97).
__aux_496(q74).
__aux_75(q106).
__aux_562(q72).
__aux_743(q56).
__aux_768(q27).
__aux_518(q83).
__aux_20(q104).
__aux_172(q101).
__aux_442(q74).
__aux_780(q27).
__aux_333(q89).
eq_to__s(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_181(q88).
__aux_130(cons(X1,X2)) :- __aux_131(X1), __aux_132(X2).
__aux_93(q106).
__aux_1004(nil).
__aux_388(q74).
__aux_134(cons(X1,X2)) :- __aux_135(X1), __aux_136(X2).
__aux_336(q88).
__aux_341(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_481(q74).
eq_from__s(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_293(q97).
__aux_342(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_342(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_342(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_342(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_342(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_342(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_342(0).
__aux_342(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_523(q81).
__aux_817(q51).
__aux_444(q78).
__aux_95(q108).
__aux_340(q81).
__aux_340(q84).
__aux_340(q70).
__aux_340(q22).
__aux_340(q95).
__aux_340(q15).
__aux_340(q13).
__aux_340(q19).
__aux_340(q110).
__aux_340(q18).
__aux_347(q66).
__aux_141(cons(X1,X2)) :- eq_B(X1), eq_cons_of_Na_and_nil_of__end_end(X2).
__aux_645(q61).
__aux_576(q70).
__aux_32(q105).
__aux_328.
__aux_1058(q4).
__aux_284(q98).
__aux_1034(q14).
__aux_650(q61).
__aux_641(q27).
__aux_557.
__aux_90(q106).
__aux_593(q68).
__aux_927(q35).
__aux_313(cons(X1,X2)) :- __aux_314(X1), __aux_315(X2).
__aux_60(q106).
__aux_92(q108).
__aux_450(q79).
__aux_665(q58).
__aux_178(q7).
__aux_304(cons(X1,X2)) :- eq_a(X1), eq_cons_of_a__no_and_nil_of__end_end(X2).
__aux_1013(q19).
__aux_590(cons(X1,X2)) :- eq_Kas(X1), __aux_591(X2).
__aux_490(q74).
__aux_174(q103).
__aux_69(q106).
__aux_608(q63).
__aux_911(q36).
__aux_736(q27).
__aux_114(q106).
__aux_131(__nu(X1,X2)) :- __aux_577(X1), __aux_578(X2).
__aux_653(q59).
__aux_26(q104).
__aux_228(q91).
__aux_1002(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_856(q43).
__aux_145(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_1061(nil).
__aux_525(q81).
__aux_525(q84).
__aux_525(q70).
__aux_525(q22).
__aux_525(q95).
__aux_525(q15).
__aux_525(q13).
__aux_525(q19).
__aux_525(q110).
__aux_525(q18).
__aux_522(q83).
__aux_390(q76).
__aux_230(q92).
__aux_14(q104).
__aux_560.
__aux_848(q46).
__aux_1015(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_1015(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_1015(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_1015(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_1015(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_1015(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_1015(0).
__aux_1015(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_492(q80).
__aux_71(q107).
__aux_276(q99).
__aux_922(q27).
__aux_480(q80).
__aux_738(q56).
__aux_245(q93).
__aux_897(q39).
__aux_438(q78).
__aux_291(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_343(q89).
__aux_1011(q17).
__aux_963(0).
__aux_1057(nil).
eq_____Var__2(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
eq_____Var__2(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
eq_____Var__2(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
eq_____Var__2(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
eq_____Var__2(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
eq_____Var__2(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
eq_____Var__2(0).
eq_____Var__2(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_558(q72).
__aux_430(q74).
eq__oc_s_of_Nb_end_cc_Kab(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_563(q70).
__aux_394(q74).
__aux_384(q75).
__aux_868(q43).
__aux_967(q27).
__aux_402(q76).
eq_from__b(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_1008(q20).
__aux_774(q27).
__aux_907(q27).
__aux_315(cons(X1,X2)) :- __aux_316(X1), __aux_317(X2).
__aux_344(q67).
__aux_192(q91).
__aux_117(q106).
__aux_597(q66).
__aux_339(X1,X2,X3) :- __aux_1010(X1), __aux_1009(X2), eq_from__a(X2), __aux_1007(X3).
__aux_339(X1,X2,X3) :- __aux_994(X1), __aux_993(X2), eq_from__a(X2), __aux_991(X3).
__aux_339(X1,X2,X3) :- __aux_573(X1), __aux_572(X2), eq_from__a(X2), __aux_570(X3).
__aux_339(X1,X2,X3) :- __aux_298(X1), eq_from__a(X2), __aux_297(X2), __aux_295(X3).
__aux_339(X1,X2,X3) :- __aux_1030(X1), __aux_1029(X2), eq_from__a(X2), __aux_1027(X3).
__aux_339(X1,X2,X3) :- __aux_1036(X1), __aux_1035(X2), eq_from__a(X2), __aux_1033(X3).
__aux_339(X1,X2,X3) :- __aux_533(X1), __aux_532(X2), eq_from__a(X2), __aux_530(X3).
__aux_339(X1,X2,X3) :- __aux_1015(X1), __aux_1014(X2), eq_from__a(X2), __aux_1012(X3).
__aux_339(X1,X2,X3) :- __aux_125(X1), __aux_124(X2), eq_from__a(X2), __aux_122(X3).
__aux_339(X1,X2,X3) :- __aux_516(X1), __aux_515(X2), eq_from__a(X2), __aux_513(X3).
__aux_1007(q19).
__aux_989(q24).
__aux_177(q102).
__aux_972(q29).
__aux_12(q106).
__aux_406(q74).
eq_cons_of_A_and_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end_end(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_999(cons(X1,X2)) :- __aux_1000(X1), __aux_1001(X2).
__aux_316(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_84(q106).
__aux_770(q54).
__aux_620(q27).
eq_____Var__5(cons(X1,X2)) :- eq_B(X1), eq_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end(X2).
__aux_81(q106).
__aux_616(q60).
__aux_567(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_567(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_567(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_567(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_567(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_567(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_567(0).
__aux_567(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_987(q24).
__aux_861(q42).
__aux_350(q71).
eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(cons(X1,X2)) :- eq_B(X1), eq_cons_of_Na_and_nil_of__end_end(X2).
__aux_570(q70).
__aux_871(q42).
__aux_1018(q18).
__aux_516(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_1050(q6).
__aux_445(q74).
__aux_957(q32).
__aux_749(q56).
__aux_142(cons(X1,X2)) :- __aux_143(X1), __aux_144(X2).
__aux_771(q27).
__aux_918(q37).
__aux_1052(q8).
__aux_1000(s(X)) :- nat(X).
__aux_1000(0).
__aux_1036(0).
__aux_11(q104).
__aux_337(q89).
__aux_305(cons(X1,X2)) :- __aux_306(X1), __aux_307(X2).
__aux_1051(q7).
__aux_783(q27).
__aux_429(q78).
__aux_699(q58).
__aux_306(nil).
__aux_23(q104).
__aux_393(q76).
__aux_519(q84).
__aux_566(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_21(q106).
__aux_695(q58).
__aux_1014(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_966(q29).
__aux_334(q90).
__aux_773(q54).
__aux_810(q50).
__aux_338(q87).
eq_N(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_240(q91).
__aux_191(q90).
eq_____Var__6(cons(X1,X2)) :- eq_b(X1), eq_cons_of_b__no_and_nil_of__end_end(X2).
__aux_282.
__aux_346(q88).
__aux_280(q98).
__aux_146(cons(X1,X2)) :- eq_to__a(X1), __aux_147(X2).
__aux_176(q101).
__aux_971(q28).
eq_____Var__17(cons(X1,X2)) :- eq_B(X1), eq_cons_of_Na_and_nil_of__end_end(X2).
__aux_1053(nil).
__aux_78(q106).
__aux_776(q54).
__aux_1039(q11).
__aux_89(q107).
__aux_808(q52).
__aux_121(q109).
__aux_287(q97).
__aux_573(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_83(q107).
__aux_189(q91).
__aux_80(q107).
__aux_277(q97).
__aux_183(q91).
__aux_290(q81).
__aux_290(q84).
__aux_290(q70).
__aux_290(q22).
__aux_290(q95).
__aux_290(q15).
__aux_290(q13).
__aux_290(q19).
__aux_290(q110).
__aux_290(q18).
eq_____Var__8(cons(X1,X2)) :- eq__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end(X1), eq_nil_of__end(X2).
__aux_767(q54).
eq_cons_of_Na_and_nil_of__end_end(cons(X1,X2)) :- eq_Na(X1), eq_nil_of__end(X2).
__aux_870(q41).
__aux_1017(q17).
__aux_838(q48).
__aux_647(q49).
__aux_489(q80).
__aux_173(q102).
__aux_68(q107).
__aux_30(q106).
__aux_735(q56).
__aux_113(q108).
__aux_120(q106).
__aux_524(X1,X2,X3) :- __aux_516(X1), eq_from__b(X2), __aux_515(X2), __aux_513(X3).
__aux_524(X1,X2,X3) :- __aux_573(X1), __aux_572(X2), eq_from__b(X2), __aux_570(X3).
__aux_524(X1,X2,X3) :- __aux_1030(X1), eq_from__b(X2), __aux_1029(X2), __aux_1027(X3).
__aux_524(X1,X2,X3) :- __aux_298(X1), eq_from__b(X2), __aux_297(X2), __aux_295(X3).
__aux_524(X1,X2,X3) :- __aux_1015(X1), eq_from__b(X2), __aux_1014(X2), __aux_1012(X3).
__aux_524(X1,X2,X3) :- __aux_533(X1), eq_from__b(X2), __aux_532(X2), __aux_530(X3).
__aux_524(X1,X2,X3) :- __aux_125(X1), eq_from__b(X2), __aux_124(X2), __aux_122(X3).
__aux_524(X1,X2,X3) :- __aux_994(X1), eq_from__b(X2), __aux_993(X2), __aux_991(X3).
__aux_524(X1,X2,X3) :- __aux_1036(X1), __aux_1035(X2), eq_from__b(X2), __aux_1033(X3).
__aux_524(X1,X2,X3) :- __aux_1010(X1), eq_from__b(X2), __aux_1009(X2), __aux_1007(X3).
__aux_933(q35).
__aux_227(q92).
__aux_122(q110).
__aux_396(q76).
__aux_574(q68).
__aux_351(q72).
__aux_521(q82).
__aux_66(q106).
__aux_1041(q9).
__aux_733(q27).
__aux_487(q74).
__aux_610(q60).
__aux_448(q74).
__aux_851(q45).
__aux_529(q80).
__aux_802(q52).
to(X1,X2) :- __aux_322(X1), __aux_323(X2).
to(X1,X2) :- __aux_561(X1), __aux_562(X2).
to(X1,X2) :- __aux_23(X1), __aux_24(X2).
to(X1,X2) :- __aux_179(X1), __aux_180(X2).
to(X1,X2) :- __aux_853(X1), __aux_854(X2).
to(X1,X2) :- __aux_1039(X1), __aux_1040(X2).
to(X1,X2) :- __aux_593(X1), __aux_594(X2).
to(X1,X2) :- __aux_1007(X1), __aux_1008(X2).
to(X1,X2) :- __aux_122(X1), __aux_123(X2).
to(X1,X2) :- __aux_384(X1), __aux_385(X2).
to(X1,X2) :- __aux_1012(X1), __aux_1013(X2).
to(X1,X2) :- __aux_853(X1), __aux_1025(X2).
to(X1,X2) :- __aux_149(X1), __aux_150(X2).
to(X1,X2) :- __aux_179(X1), __aux_608(X2).
to(X1,X2) :- __aux_1063(X1), __aux_1064(X2).
to(X1,X2) :- __aux_329(X1), __aux_330(X2).
to(X1,X2) :- __aux_603(X1), __aux_604(X2).
to(X1,X2) :- __aux_1071(X1), __aux_1072(X2).
to(X1,X2) :- __aux_518(X1), __aux_519(X2).
to(X1,X2) :- __aux_1055(X1), __aux_1056(X2).
to(X1,X2) :- __aux_853(X1), __aux_1037(X2).
to(X1,X2) :- __aux_542(X1), __aux_543(X2).
to(X1,X2) :- __aux_548(X1), __aux_549(X2).
to(X1,X2) :- __aux_278(X1), __aux_279(X2).
to(X1,X2) :- __aux_333(X1), __aux_334(X2).
to(X1,X2) :- __aux_348(X1), __aux_349(X2).
to(X1,X2) :- __aux_1073(X1), __aux_1074(X2).
to(X1,X2) :- __aux_530(X1), __aux_531(X2).
to(X1,X2) :- __aux_1017(X1), __aux_1018(X2).
to(X1,X2) :- __aux_521(X1), __aux_522(X2).
to(X1,X2) :- __aux_127(X1), __aux_128(X2).
to(X1,X2) :- __aux_545(X1), __aux_546(X2).
to(X1,X2) :- __aux_1047(X1), __aux_1048(X2).
to(X1,X2) :- __aux_176(X1), __aux_177(X2).
to(X1,X2) :- __aux_606(X1), __aux_607(X2).
to(X1,X2) :- __aux_510(X1), __aux_511(X2).
to(X1,X2) :- __aux_348(X1), __aux_595(X2).
to(X1,X2) :- __aux_991(X1), __aux_992(X2).
to(X1,X2) :- __aux_853(X1), __aux_1005(X2).
to(X1,X2) :- __aux_164(X1), __aux_165(X2).
to(X1,X2) :- __aux_535(X1), __aux_536(X2).
to(X1,X2) :- __aux_853(X1), __aux_1031(X2).
to(X1,X2) :- __aux_1033(X1), __aux_1034(X2).
to(X1,X2) :- __aux_1042(X1), __aux_1043(X2).
to(X1,X2) :- __aux_513(X1), __aux_514(X2).
to(X1,X2) :- __aux_182(X1), __aux_183(X2).
to(X1,X2) :- __aux_160(X1), __aux_161(X2).
to(X1,X2) :- __aux_179(X1), __aux_1049(X2).
to(X1,X2) :- __aux_600(X1), __aux_601(X2).
to(X1,X2) :- __aux_1067(X1), __aux_1068(X2).
to(X1,X2) :- __aux_996(X1), __aux_997(X2).
to(X1,X2) :- __aux_575(X1), __aux_576(X2).
to(X1,X2) :- __aux_280(X1), __aux_281(X2).
to(X1,X2) :- __aux_336(X1), __aux_337(X2).
to(X1,X2) :- __aux_1027(X1), __aux_1028(X2).
to(X1,X2) :- __aux_597(X1), __aux_598(X2).
to(X1,X2) :- __aux_295(X1), __aux_296(X2).
to(X1,X2) :- __aux_300(X1), __aux_301(X2).
to(X1,X2) :- __aux_325(X1), __aux_326(X2).
to(X1,X2) :- __aux_286(X1), __aux_287(X2).
to(X1,X2) :- __aux_351(X1), __aux_352(X2).
to(X1,X2) :- __aux_2(X1), __aux_3(X2).
to(X1,X2) :- __aux_551(X1), __aux_552(X2).
to(X1,X2) :- __aux_554(X1), __aux_555(X2).
to(X1,X2) :- __aux_152(X1), __aux_153(X2).
to(X1,X2) :- __aux_538(X1), __aux_539(X2).
to(X1,X2) :- __aux_558(X1), __aux_559(X2).
to(X1,X2) :- __aux_1059(X1), __aux_1060(X2).
to(X1,X2) :- __aux_853(X1), __aux_989(X2).
to(X1,X2) :- __aux_173(X1), __aux_174(X2).
to(X1,X2) :- __aux_570(X1), __aux_571(X2).
to(X1,X2) :- __aux_156(X1), __aux_157(X2).
to(X1,X2) :- __aux_345(X1), __aux_346(X2).
to(X1,X2) :- __aux_17(X1), __aux_18(X2).
to(X1,X2) :- __aux_283(X1), __aux_284(X2).
to(X1,X2) :- __aux_275(X1), __aux_276(X2).
to(X1,X2) :- __aux_1051(X1), __aux_1052(X2).
__aux_921(q35).
__aux_1037(q13).
__aux_225(q91).
__aux_896(q38).
__aux_528(q83).
__aux_279(q99).
eq_____Var__1(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
eq_____Var__1(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
eq_____Var__1(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
eq_____Var__1(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
eq_____Var__1(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
eq_____Var__1(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
eq_____Var__1(0).
eq_____Var__1(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_587(cons(X1,X2)) :- eq_a(X1), eq_cons_of_a__no_and_nil_of__end_end(X2).
__aux_148.
__aux_180(q101).
__aux_926(q34).
__aux_397(q74).
__aux_59(q105).
__aux_649(q60).
eq_____Var__3(cons(X1,X2)) :- eq_Na(X1), eq_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end(X2).
__aux_640(q62).
__aux_903(q39).
__aux_405(q76).
__aux_589(cons(X1,X2)) :- eq_b(X1), eq_cons_of_b__no_and_nil_of__end_end(X2).
__aux_660(q60).
__aux_478(q74).
__aux_705(q58).
__aux_433(q74).
__aux_133(nil).
__aux_283(q97).
__aux_243(q91).
__aux_841(q47).
__aux_575(q69).
__aux_978(q29).
__aux_358(q74).
__aux_577(q69).
__aux_22.
__aux_1056(q7).
__aux_708(q56).
__aux_124(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
eq_____Var__16(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
eq_____Var__16(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
eq_____Var__16(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
eq_____Var__16(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
eq_____Var__16(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
eq_____Var__16(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
eq_____Var__16(0).
eq_____Var__16(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_309(cons(X1,X2)) :- __aux_310(X1), __aux_311(X2).
__aux_1055(q6).
__aux_862(q43).
__aux_571(q71).
__aux_1006(q18).
__aux_698(q57).
__aux_579(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_992(q23).
__aux_332.
__aux_617(q27).
eq_____Var__9(nil).
__aux_24(q106).
__aux_185(q90).
__aux_17(q104).
__aux_292(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_292(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_292(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_292(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_292(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_292(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_292(0).
__aux_292(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_592(q67).
__aux_182(q89).
__aux_662(q45).
__aux_175(q8).
__aux_985(q26).
__aux_960(q30).
eq_____Var__18(cons(X1,X2)) :- eq_Na(X1), eq_nil_of__end(X2).
__aux_307(cons(X1,X2)) :- __aux_308(X1), __aux_309(X2).
__aux_288(q95).
__aux_439(q74).
__aux_706(q57).
__aux_692(q58).
__aux_354(q73).
__aux_958(q31).
__aux_123(q111).
__aux_559(q73).
__aux_919(q36).
__aux_1042(q10).
__aux_1049(q9).
__aux_352(q74).
__aux_619(q60).
__aux_483(q80).
__aux_1059(q5).
__aux_853(q12).
__aux_132(cons(X1,X2)) :- __aux_133(X1), __aux_134(X2).
__aux_611(q27).
__aux_385(q74).
__aux_403(q74).
__aux_221(q92).
__aux_584(cons(X1,X2)) :- __aux_585(X1), __aux_586(X2).
__aux_1033(q13).
__aux_990(q21).
__aux_96(q106).
__aux_335.
__aux_86(q107).
__aux_646(q62).
eq_M(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
eq_M(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
eq_M(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
eq_M(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
eq_M(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
eq_M(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
eq_M(0).
eq_M(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_33(q106).
__aux_441(q78).
__aux_87(q106).
__aux_991(q22).
__aux_62(q107).
__aux_568(q72).
__aux_964(q30).
__aux_387(q76).
__aux_811(q51).
__aux_904(q38).
__aux_1009(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_116(q108).
__aux_329(q90).
__aux_451(q74).
__aux_666(q27).
__aux_144(cons(X1,X2)) :- __aux_145(X1), __aux_146(X2).
__aux_777(q27).
__aux_595(q68).
__aux_526(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_849(q12).
eq_pub__channel(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_1038(q10).
__aux_1054(q5).
__aux_233(q92).
eq_____Var__7(cons(X1,X2)) :- eq_Kab(X1), eq_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end(X2).
__aux_1005(q21).
__aux_912(q37).
__aux_569(q69).
__aux_654(q60).
__aux_281(q100).
__aux_27(q106).
__aux_435(q78).
__aux_663(q59).
__aux_236(q92).
__aux_285.
__aux_613(q60).
__aux_693(q27).
__aux_857(q27).
__aux_1040(q12).
__aux_436(q74).
__aux_147(nil).
__aux_495(q80).
__aux_74(q107).
__aux_561(q71).
__aux_564(X1,X2,X3) :- __aux_1030(X1), eq_from__s(X2), __aux_1029(X2), __aux_1027(X3).
__aux_564(X1,X2,X3) :- __aux_573(X1), __aux_572(X2), eq_from__s(X2), __aux_570(X3).
__aux_564(X1,X2,X3) :- __aux_533(X1), eq_from__s(X2), __aux_532(X2), __aux_530(X3).
__aux_564(X1,X2,X3) :- __aux_516(X1), eq_from__s(X2), __aux_515(X2), __aux_513(X3).
__aux_564(X1,X2,X3) :- __aux_1036(X1), __aux_1035(X2), eq_from__s(X2), __aux_1033(X3).
__aux_564(X1,X2,X3) :- __aux_1010(X1), eq_from__s(X2), __aux_1009(X2), __aux_1007(X3).
__aux_564(X1,X2,X3) :- __aux_125(X1), eq_from__s(X2), __aux_124(X2), __aux_122(X3).
__aux_564(X1,X2,X3) :- __aux_994(X1), eq_from__s(X2), __aux_993(X2), __aux_991(X3).
__aux_564(X1,X2,X3) :- __aux_1015(X1), eq_from__s(X2), __aux_1014(X2), __aux_1012(X3).
__aux_564(X1,X2,X3) :- __aux_298(X1), eq_from__s(X2), __aux_297(X2), __aux_295(X3).
__aux_391(q74).
__aux_231(q91).
__aux_15(q106).
__aux_515(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_493(q74).
__aux_72(q106).
__aux_739(q49).
__aux_330(q92).
__aux_16.
__aux_246(q91).
__aux_399(q76).
__aux_779(q54).
__aux_555(q75).
__aux_298(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_549(q77).
__aux_1031(q15).
__aux_456(q79).
__aux_6(q106).
__aux_207(q91).
__aux_581(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_138(cons(X1,X2)) :- __aux_139(X1), __aux_140(X2).
__aux_600(q65).
__aux_469(q74).
__aux_152(q107).
__aux_629(q27).
__aux_204(q91).
eq_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end(cons(X1,X2)) :- eq_B(X1), eq_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end(X2).
__aux_382(q74).
__aux_894(q40).
eq_s_of_Nb_end(s(X)) :- eq_Nb(X).
__aux_454(q74).
__aux_995(q12).
__aux_209(q90).
__aux_167(X1,X2,X3) :- __aux_1010(X1), __aux_1009(X2), eq_from__a(X2), __aux_1007(X3).
__aux_167(X1,X2,X3) :- __aux_994(X1), __aux_993(X2), eq_from__a(X2), __aux_991(X3).
__aux_167(X1,X2,X3) :- __aux_573(X1), __aux_572(X2), eq_from__a(X2), __aux_570(X3).
__aux_167(X1,X2,X3) :- __aux_298(X1), eq_from__a(X2), __aux_297(X2), __aux_295(X3).
__aux_167(X1,X2,X3) :- __aux_1030(X1), __aux_1029(X2), eq_from__a(X2), __aux_1027(X3).
__aux_167(X1,X2,X3) :- __aux_1036(X1), __aux_1035(X2), eq_from__a(X2), __aux_1033(X3).
__aux_167(X1,X2,X3) :- __aux_533(X1), __aux_532(X2), eq_from__a(X2), __aux_530(X3).
__aux_167(X1,X2,X3) :- __aux_1015(X1), __aux_1014(X2), eq_from__a(X2), __aux_1012(X3).
__aux_167(X1,X2,X3) :- __aux_125(X1), __aux_124(X2), eq_from__a(X2), __aux_122(X3).
__aux_167(X1,X2,X3) :- __aux_516(X1), __aux_515(X2), eq_from__a(X2), __aux_513(X3).
__aux_366(q73).
__aux_156(q105).
__aux_510(q83).
__aux_370(q74).
__aux_326(q93).
eq_Nb(__nu(X1,X2)) :- __aux_302(X1), __aux_303(X2).
eq_Nb(s(X)) :- eq_Nb(X).
__aux_532(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_1021(q81).
__aux_1021(q84).
__aux_1021(q70).
__aux_1021(q22).
__aux_1021(q95).
__aux_1021(q15).
__aux_1021(q13).
__aux_1021(q19).
__aux_1021(q110).
__aux_1021(q18).
__aux_943(q33).
__aux_57(q106).
__aux_711(q56).
__aux_677(q58).
__aux_255(q91).
__aux_320(nil).
eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(cons(X1,X2)) :- eq_Na(X1), eq_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end(X2).
__aux_993(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_795(q52).
__aux_550(q75).
__aux_887(q39).
eq_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end(cons(X1,X2)) :- eq_Kab(X1), eq_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end(X2).
__aux_257(q93).
__aux_1029(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_668(q58).
__aux_712(q27).
__aux_98(q108).
__aux_325(q92).
__aux_383(q73).
__aux_882(q40).
__aux_818(q50).
__aux_165(q104).
__aux_212(q90).
__aux_418(q74).
__aux_44(q105).
eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(cons(X1,X2)) :- eq_Kab(X1), eq_cons_of_A_and_nil_of__end_end(X2).
__aux_110(q108).
__aux_150(q109).
eq_cons_of_b__no_and_nil_of__end_end(cons(X1,X2)) :- eq_b__no(X1), eq_nil_of__end(X2).
__aux_1067(q3).
__aux_828(q48).
__aux_721(q27).
__aux_466(q74).
__aux_1026(q12).
__aux_168(q81).
__aux_168(q84).
__aux_168(q70).
__aux_168(q22).
__aux_168(q95).
__aux_168(q15).
__aux_168(q13).
__aux_168(q19).
__aux_168(q110).
__aux_168(q18).
__aux_42(q106).
__aux_468(q79).
__aux_514(q86).
__aux_750(q55).
__aux_414(q76).
__aux_323(q94).
__aux_604(q65).
__aux_219(q91).
__aux_752(q54).
__aux_820(q48).
__aux_151.
__aux_1064(q5).
eq__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_687(q27).
__aux_508(q74).
__aux_540(q78).
__aux_417(q77).
__aux_327(q90).
__aux_686(q58).
__aux_409(q74).
__aux_272(q93).
__aux_427(q74).
__aux_764(q54).
__aux_5(q104).
__aux_824(q27).
__aux_194(q90).
eq_a(__nu(X1,X2)) :- __aux_1063(X1), __aux_1065(X2).
__aux_270(q91).
__aux_300(q94).
eq_nil_of__end(nil).
__aux_762(q27).
__aux_1.
__aux_267(q91).
__aux_582(cons(X1,X2)) :- __aux_583(X1), __aux_584(X2).
__aux_689(q58).
eq_id(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_758(q54).
__aux_499(q74).
eq_____Var__12(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
eq_____Var__12(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
eq_____Var__12(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
eq_____Var__12(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
eq_____Var__12(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
eq_____Var__12(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
eq_____Var__12(0).
eq_____Var__12(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_263(q93).
__aux_310(cons(X1,X2)) :- eq_A(X1), eq_nil_of__end(X2).
__aux_681(q27).
__aux_261(q91).
eq_____Var__11(__nu(X1,X2)) :- __aux_302(X1), __aux_303(X2).
eq_____Var__11(s(X)) :- eq_Nb(X).
__aux_8(q104).
__aux_756(q27).
recv(X1,X2,X3,X4) :- __aux_290(X1), __aux_291(X2), __aux_292(X3), __aux_293(X4).
recv(X1,X2,X3,X4) :- __aux_565(X1), __aux_566(X2), __aux_567(X3), __aux_568(X4).
recv(X1,X2,X3,X4) :- __aux_168(X1), __aux_169(X2), __aux_170(X3), __aux_171(X4).
recv(X1,X2,X3,X4) :- __aux_525(X1), __aux_526(X2), __aux_527(X3), __aux_528(X4).
recv(X1,X2,X3,X4) :- __aux_340(X1), __aux_341(X2), __aux_342(X3), __aux_343(X4).
recv(X1,X2,X3,X4) :- __aux_1021(X1), __aux_1022(X2), __aux_1023(X3), __aux_1024(X4).
__aux_101(q108).
__aux_2(q104).
__aux_296(q96).
__aux_136(cons(X1,X2)) :- __aux_137(X1), __aux_138(X2).
__aux_501(q80).
__aux_945(q32).
__aux_421(q74).
__aux_799(q49).
__aux_1073(q1).
__aux_832(q48).
__aux_504(q80).
__aux_160(q104).
__aux_950(q31).
eq_kxs_of_B_end(kxs(X)) :- eq_B(X).
__aux_717(q56).
__aux_462(q79).
__aux_36(q106).
__aux_302(q94).
__aux_379(q74).
__aux_163.
eq_____Var__19(nil).
__aux_375(q73).
__aux_139(cons(X1,X2)) :- eq_a(X1), eq_cons_of_a__no_and_nil_of__end_end(X2).
__aux_605(q8).
__aux_1065(nil).
__aux_38(q105).
__aux_1047(q9).
__aux_360(q73).
__aux_714(q56).
__aux_880(q41).
eq_A(cons(X1,X2)) :- eq_a(X1), eq_cons_of_a__no_and_nil_of__end_end(X2).
__aux_364(q74).
__aux_460(q74).
__aux_715(q27).
__aux_1074(q2).
__aux_606(q63).
__aux_935(q33).
__aux_127(q109).
__aux_821(q27).
__aux_1019(q12).
__aux_215(q92).
__aux_998(q21).
__aux_372(q73).
__aux_200(q90).
__aux_299(q93).
__aux_166(q102).
__aux_996(q21).
__aux_1071(q2).
__aux_544(q77).
__aux_9(q106).
__aux_1072(q3).
eq_a__no(s(X)) :- nat(X).
eq_a__no(0).
__aux_538(q79).
__aux_511(q85).
__aux_198(q91).
__aux_317(cons(X1,X2)) :- __aux_318(X1), __aux_319(X2).
__aux_583(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_475(q74).
__aux_1023(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_1023(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_1023(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_1023(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_1023(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_1023(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_1023(0).
__aux_1023(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_669(q27).
__aux_509(q82).
__aux_723(q56).
__aux_546(q78).
__aux_513(q84).
__aux_727(q27).
__aux_552(q76).
eq_cons_of_a_and_cons_of_a__no_and_nil_of__end_end_end(cons(X1,X2)) :- eq_a(X1), eq_cons_of_a__no_and_nil_of__end_end(X2).
__aux_50(q105).
__aux_104(q108).
__aux_994(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_251(q93).
eq_kxs_of_A_end(kxs(X)) :- eq_A(X).
__aux_53(q105).
__aux_108(q106).
__aux_1045(cons(X1,X2)) :- __aux_1002(X1), __aux_1003(X2).
__aux_411(q76).
__aux_249(q91).
__aux_671(q58).
eq_cons_of_A_and_nil_of__end_end(cons(X1,X2)) :- eq_A(X1), eq_nil_of__end(X2).
__aux_48(q106).
__aux_543(q79).
__aux_169(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_129(q109).
__aux_942(q34).
__aux_690(q27).
__aux_1062(q3).
__aux_1022(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_535(q80).
__aux_195(q91).
__aux_672(q27).
__aux_137(cons(X1,X2)) :- eq_Na(X1), eq_nil_of__end(X2).
__aux_301(q95).
eq_Kab(__nu(X1,X2)) :- __aux_129(X1), __aux_130(X2).
__aux_632(q27).
__aux_537.
__aux_367(q74).
eq_b__no(s(X)) :- nat(X).
eq_b__no(0).
__aux_753(q27).
__aux_823(q49).
__aux_984(nil).
__aux_423(q78).
__aux_793(q53).
eq_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end(cons(X1,X2)) :- eq__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end(X1), eq_nil_of__end(X2).
__aux_162(q103).
__aux_786(q54).
__aux_197(q90).
__aux_273(q91).
__aux_765(q27).
__aux_474(q79).
__aux_883(q27).
eq_from__a(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_213(q91).
eq_____Var__13(cons(X1,X2)) :- eq_Kab(X1), eq_cons_of_A_and_nil_of__end_end(X2).
__aux_675(q27).
__aux_45(q106).
__aux_545(q77).
__aux_726(q56).
__aux_551(q75).
__aux_982(q27).
__aux_792(q54).
__aux_1069(nil).
eq_to__a(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_829(q49).
__aux_105(q106).
__aux_107(q108).
__aux_724(q27).
__aux_321.
eq_c__pub(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_415(q74).
__aux_472(q74).
__aux_602(q63).
__aux_248(q93).
eq_cons_of_a__no_and_nil_of__end_end(cons(X1,X2)) :- eq_a__no(X1), eq_nil_of__end(X2).
__aux_47(q105).
__aux_1068(q4).
__aux_542(q78).
__aux_111(q106).
__aux_622(q60).
__aux_1025(q17).
__aux_457(q74).
__aux_318(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_35(q105).
__aux_378(q73).
__aux_601(q66).
__aux_153(q108).
__aux_541.
eq_Na(__nu(X1,X2)) :- __aux_577(X1), __aux_578(X2).
__aux_1030(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_512(q83).
__aux_1028(q16).
__aux_533(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_533(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_533(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_533(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_533(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_533(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_533(0).
__aux_533(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_210(q91).
__aux_303(cons(X1,X2)) :- __aux_304(X1), __aux_305(X2).
__aux_607(q64).
__aux_424(q74).
__aux_879(q25).
send(X1,X2,X3) :- __aux_1012(X1), __aux_1014(X2), __aux_1015(X3).
send(X1,X2,X3) :- __aux_295(X1), __aux_297(X2), __aux_298(X3).
send(X1,X2,X3) :- __aux_991(X1), __aux_993(X2), __aux_994(X3).
send(X1,X2,X3) :- __aux_570(X1), __aux_572(X2), __aux_573(X3).
send(X1,X2,X3) :- __aux_1007(X1), __aux_1009(X2), __aux_1010(X3).
send(X1,X2,X3) :- __aux_513(X1), __aux_515(X2), __aux_516(X3).
send(X1,X2,X3) :- __aux_1033(X1), __aux_1035(X2), __aux_1036(X3).
send(X1,X2,X3) :- __aux_530(X1), __aux_532(X2), __aux_533(X3).
send(X1,X2,X3) :- __aux_1027(X1), __aux_1029(X2), __aux_1030(X3).
send(X1,X2,X3) :- __aux_122(X1), __aux_124(X2), __aux_125(X3).
__aux_157(q107).
__aux_363(q73).
eq_initial__knowledge(0).
eq_Pid(s(X)) :- nat(X).
eq_Pid(0).
__aux_126(q108).
__aux_459(q79).
__aux_159.
__aux_311(cons(X1,X2)) :- __aux_312(X1), __aux_313(X2).
__aux_260(q93).
__aux_755(q54).
__aux_295(q95).
__aux_678(q27).
__aux_534.
__aux_420(q78).
__aux_798(q52).
__aux_831(q47).
__aux_536(q81).
__aux_796(q27).
__aux_888(q40).
__aux_680(q58).
eq_B(cons(X1,X2)) :- eq_b(X1), eq_cons_of_b__no_and_nil_of__end_end(X2).
__aux_258(q91).
eq_____Var__15(nil).
__aux_625(q60).
__aux_99(q106).
__aux_102(q106).
__aux_154(q105).
__aux_498(q80).
__aux_416(q76).
__aux_730(q27).
__aux_135(cons(X1,X2)) :- eq_b(X1), eq_cons_of_b__no_and_nil_of__end_end(X2).
__aux_319(cons(X1,X2)) :- eq_Kbs(X1), __aux_320(X2).
__aux_981(q26).
__aux_56(q105).
__aux_412(q74).
__aux_254(q93).
__aux_683(q58).
__aux_274(q96).
__aux_1066(q2).
__aux_51(q106).
eq_____Var__14(cons(X1,X2)) :- eq_A(X1), eq_nil_of__end(X2).
__aux_322(q93).
__aux_297(__nu(X1,X2)) :- __aux_1067(X1), __aux_1069(X2).
__aux_252(q91).
nat(s(X)) :- nat(X).
nat(0).
__aux_674(q58).
__aux_1044(q10).
__aux_54(q106).
__aux_453(q79).
__aux_936(q34).
__aux_1046(q8).
__aux_216(q91).
__aux_373(q74).
__aux_201(q91).
eq__oc_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end_cc_kxs_of_A_end(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_997(q22).
__aux_369(q73).
__aux_206(q90).
__aux_155.
eq_Kbs(__nu(X1,X2)) :- __aux_1051(X1), __aux_1053(X2).
eq_Kbs(kxs(X)) :- eq_B(X).
__aux_628(q60).
__aux_203(q90).
__aux_381(q73).
__aux_539(q80).
__aux_1070(q1).
__aux_599(q64).
__aux_548(q76).
__aux_554(q73).
eq_____Var__10(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
eq_____Var__10(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
eq_____Var__10(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
eq_____Var__10(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
eq_____Var__10(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
eq_____Var__10(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
eq_____Var__10(0).
eq_____Var__10(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_218(q92).
__aux_623(q27).
__aux_759(q27).
__aux_128(q110).
__aux_264(q91).
__aux_507(q80).
eq_b(__nu(X1,X2)) :- __aux_1059(X1), __aux_1061(X2).
__aux_471(q79).
__aux_408(q76).
__aux_547.
__aux_631(q60).
__aux_426(q78).
__aux_553.
__aux_170(crypt(X1,X2)) :- eq_s_of_Nb_end(X1), eq_Kab(X2).
__aux_170(crypt(X1,X2)) :- eq_cons_of_Na_and_cons_of_B_and_cons_of_Kab_and_cons_of__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end_and_nil_of__end_end_end_end_end(X1), eq_kxs_of_A_end(X2).
__aux_170(crypt(X1,X2)) :- eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end(X1), eq_kxs_of_B_end(X2).
__aux_170(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_170(__nu(X1,X2)) :- __aux_998(X1), __aux_999(X2).
__aux_170(__nu(X1,X2)) :- __aux_1044(X1), __aux_1045(X2).
__aux_170(0).
__aux_170(cons(X1,X2)) :- eq_A(X1), eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end(X2).
__aux_1024(q18).
eq_cons_of_b_and_cons_of_b__no_and_nil_of__end_end_end(cons(X1,X2)) :- eq_b(X1), eq_cons_of_b__no_and_nil_of__end_end(X2).
__aux_979(q28).
__aux_729(q56).
__aux_684(q27).
__aux_158(q104).
__aux_3(q106).
__aux_269(q93).
__aux_761(q54).
__aux_502(q74).
__aux_635(q27).
__aux_266(q93).
__aux_946(q27).
__aux_877(q42).
__aux_634(q60).
__aux_505(q74).
__aux_161(q105).
__aux_41(q105).
__aux_951(q32).
__aux_580(cons(X1,X2)) :- __aux_581(X1), __aux_582(X2).
__aux_1027(q15).
__aux_626(q27).
__aux_1020(X1,X2,X3) :- __aux_125(X1), __aux_124(X2), eq_pub__channel(X2), __aux_122(X3).
__aux_1020(X1,X2,X3) :- __aux_533(X1), eq_pub__channel(X2), __aux_532(X2), __aux_530(X3).
__aux_1020(X1,X2,X3) :- __aux_1036(X1), __aux_1035(X2), eq_pub__channel(X2), __aux_1033(X3).
__aux_1020(X1,X2,X3) :- __aux_1010(X1), __aux_1009(X2), eq_pub__channel(X2), __aux_1007(X3).
__aux_1020(X1,X2,X3) :- __aux_298(X1), eq_pub__channel(X2), __aux_297(X2), __aux_295(X3).
__aux_1020(X1,X2,X3) :- __aux_516(X1), eq_pub__channel(X2), __aux_515(X2), __aux_513(X3).
__aux_1020(X1,X2,X3) :- __aux_1030(X1), eq_pub__channel(X2), __aux_1029(X2), __aux_1027(X3).
__aux_1020(X1,X2,X3) :- __aux_573(X1), __aux_572(X2), eq_pub__channel(X2), __aux_570(X3).
__aux_1020(X1,X2,X3) :- __aux_994(X1), eq_pub__channel(X2), __aux_993(X2), __aux_991(X3).
__aux_1020(X1,X2,X3) :- __aux_1015(X1), __aux_1014(X2), eq_pub__channel(X2), __aux_1012(X3).
__aux_1063(q4).
__aux_718(q27).
__aux_637(q60).
__aux_463(q74).
__aux_324.
__aux_785(q53).
__aux_376(q74).
__aux_603(q64).
__aux_149(q108).
__aux_720(q56).
__aux_465(q79).
__aux_39(q106).
__aux_1048(q10).
eq__oc_Nb_cc_Kab(crypt(X1,X2)) :- eq_Nb(X1), eq_Kab(X2).
__aux_361(q74).
__aux_164(q103).