% Clauses for the ISpi program nspriv.spi, automatically generated by ispi.

input_clause(case_cons_diff_crypt,axiom,
  [--to(E,q104), --eq_____Var__16 crypt(X1,X2), ++to(q104,q106)]).
input_clause(case_cons_diff_acrypt,axiom,
  [--to(E,q104), --eq_____Var__16 acrypt(X1,X2), ++to(q104,q106)]).
input_clause(case_cons_diff___nu,axiom,
  [--to(E,q104), --eq_____Var__16 __nu(X1,X2), ++to(q104,q106)]).
input_clause(case_cons_diff_pub,axiom,
  [--to(E,q104), --eq_____Var__16 pub(X1), ++to(q104,q106)]).
input_clause(case_cons_diff_prv,axiom,
  [--to(E,q104), --eq_____Var__16 prv(X1), ++to(q104,q106)]).
input_clause(case_cons_diff___eq,axiom,
  [--to(E,q104), --eq_____Var__16 __eq(X1), ++to(q104,q106)]).
input_clause(case_cons_diff_0,axiom,
  [--to(E,q104), --eq_____Var__16 0, ++to(q104,q106)]).
input_clause(case_cons_diff_kxs,axiom,
  [--to(E,q104), --eq_____Var__16 kxs(X1), ++to(q104,q106)]).
input_clause(case_cons_diff_nil,axiom,
  [--to(E,q104), --eq_____Var__16 nil, ++to(q104,q106)]).
input_clause(case_cons_diff_s,axiom,
  [--to(E,q104), --eq_____Var__16 s(X1), ++to(q104,q106)]).
input_clause(case_cons_diff_crypt,axiom,
  [--to(E,q105), --eq_____Var__17 crypt(X1,X2), ++to(q105,q106)]).
input_clause(case_cons_diff_acrypt,axiom,
  [--to(E,q105), --eq_____Var__17 acrypt(X1,X2), ++to(q105,q106)]).
input_clause(case_cons_diff___nu,axiom,
  [--to(E,q105), --eq_____Var__17 __nu(X1,X2), ++to(q105,q106)]).
input_clause(case_cons_diff_pub,axiom,
  [--to(E,q105), --eq_____Var__17 pub(X1), ++to(q105,q106)]).
input_clause(case_cons_diff_prv,axiom,
  [--to(E,q105), --eq_____Var__17 prv(X1), ++to(q105,q106)]).
input_clause(case_cons_diff___eq,axiom,
  [--to(E,q105), --eq_____Var__17 __eq(X1), ++to(q105,q106)]).
input_clause(case_cons_diff_0,axiom,
  [--to(E,q105), --eq_____Var__17 0, ++to(q105,q106)]).
input_clause(case_cons_diff_kxs,axiom,
  [--to(E,q105), --eq_____Var__17 kxs(X1), ++to(q105,q106)]).
input_clause(case_cons_diff_nil,axiom,
  [--to(E,q105), --eq_____Var__17 nil, ++to(q105,q106)]).
input_clause(case_cons_diff_s,axiom,
  [--to(E,q105), --eq_____Var__17 s(X1), ++to(q105,q106)]).
input_clause(case_cons_diff_crypt,axiom,
  [--to(E,q107), --eq_____Var__18 crypt(X1,X2), ++to(q107,q106)]).
input_clause(case_cons_diff_acrypt,axiom,
  [--to(E,q107), --eq_____Var__18 acrypt(X1,X2), ++to(q107,q106)]).
input_clause(case_cons_diff___nu,axiom,
  [--to(E,q107), --eq_____Var__18 __nu(X1,X2), ++to(q107,q106)]).
input_clause(case_cons_diff_pub,axiom,
  [--to(E,q107), --eq_____Var__18 pub(X1), ++to(q107,q106)]).
input_clause(case_cons_diff_prv,axiom,
  [--to(E,q107), --eq_____Var__18 prv(X1), ++to(q107,q106)]).
input_clause(case_cons_diff___eq,axiom,
  [--to(E,q107), --eq_____Var__18 __eq(X1), ++to(q107,q106)]).
input_clause(case_cons_diff_0,axiom,
  [--to(E,q107), --eq_____Var__18 0, ++to(q107,q106)]).
input_clause(case_cons_diff_kxs,axiom,
  [--to(E,q107), --eq_____Var__18 kxs(X1), ++to(q107,q106)]).
input_clause(case_cons_diff_nil,axiom,
  [--to(E,q107), --eq_____Var__18 nil, ++to(q107,q106)]).
input_clause(case_cons_diff_s,axiom,
  [--to(E,q107), --eq_____Var__18 s(X1), ++to(q107,q106)]).
input_clause(case_nil_diff_crypt,axiom,
  [--to(E,q108), --eq_____Var__19 crypt(X1,X2), ++to(q108,q106)]).
input_clause(case_nil_diff_acrypt,axiom,
  [--to(E,q108), --eq_____Var__19 acrypt(X1,X2), ++to(q108,q106)]).
input_clause(case_nil_diff___nu,axiom,
  [--to(E,q108), --eq_____Var__19 __nu(X1,X2), ++to(q108,q106)]).
input_clause(case_nil_diff_cons,axiom,
  [--to(E,q108), --eq_____Var__19 cons(X1,X2), ++to(q108,q106)]).
input_clause(case_nil_diff_pub,axiom,
  [--to(E,q108), --eq_____Var__19 pub(X1), ++to(q108,q106)]).
input_clause(case_nil_diff_prv,axiom,
  [--to(E,q108), --eq_____Var__19 prv(X1), ++to(q108,q106)]).
input_clause(case_nil_diff___eq,axiom,
  [--to(E,q108), --eq_____Var__19 __eq(X1), ++to(q108,q106)]).
input_clause(case_nil_diff_0,axiom,
  [--to(E,q108), --eq_____Var__19 0, ++to(q108,q106)]).
input_clause(case_nil_diff_kxs,axiom,
  [--to(E,q108), --eq_____Var__19 kxs(X1), ++to(q108,q106)]).
input_clause(case_nil_diff_s,axiom,
  [--to(E,q108), --eq_____Var__19 s(X1), ++to(q108,q106)]).
input_clause(out,axiom,
  [--to(E,q110), --eq_to__a X, --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, ++to(q110,q111)]).
input_clause(out_send,axiom,
  [--to(E,q110), --eq_to__a X, --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, ++send(q110,X,Y)]).
input_clause(fun_cons_eq,axiom,
  [--eq_A X1, --eq_nil_of__end X2, ++eq_cons_of_A_and_nil_of__end_end cons(X1,X2)]).
input_clause(fun_cons_eq,axiom,
  [--eq_Kab X1, --eq_cons_of_A_and_nil_of__end_end X2, ++eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end cons(X1,X2)]).
input_clause(fun_crypt_eq,axiom,
  [--eq_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end X1, --eq_kxs_of_B_end X2, ++eq__oc_cons_of_Kab_and_cons_of_A_and_nil_of__end_end_end_cc_kxs_of_B_end crypt(X1,X2)]).
input_clause(fun_cons_eq,axiom,
  [--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, ++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)]).
input_clause(fun_cons_eq,axiom,
  [--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, ++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)]).
input_clause(fun_cons_eq,axiom,
  [--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, ++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)]).
input_clause(fun_cons_eq,axiom,
  [--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, ++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)]).
input_clause(fun_crypt_eq,axiom,
  [--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__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)]).
input_clause(new,axiom,
  [--to(E,q109), ++to(q109,q110)]).
input_clause(new_eq,axiom,
  [--to(E,q109), --eq_Na X1, --eq_____Var__19 X2, --eq_B X3, --eq_____Var__18 X4, --eq_A X5, --eq_____Var__17 X6, --eq_____Var__16 X7, --eq_from__a X8, --eq_to__a X9, ++eq_Kab __nu(q109,__c_of_Na_and_____Var__19_and_B_and_____Var__18_and_A_and_____Var__17_and_____Var__16_and_from__a_and_to__a_end(X1,X2,X3,X4,X5,X6,X7,X8,X9))]).
input_clause(case_nil,axiom,
  [--to(E,q108), --eq_____Var__19 nil, ++to(q108,q109)]).
input_clause(case_cons,axiom,
  [--to(E,q107), --eq_____Var__18 cons(X1,X2), ++to(q107,q108)]).
input_clause(case_cons_eq,axiom,
  [--to(E,q107), --eq_____Var__18 cons(X1,X2), ++eq_Na X1]).
input_clause(case_cons_eq,axiom,
  [--to(E,q107), --eq_____Var__18 cons(X1,X2), ++eq_____Var__19 X2]).
input_clause(case_cons,axiom,
  [--to(E,q105), --eq_____Var__17 cons(X1,X2), ++to(q105,q107)]).
input_clause(case_cons_eq,axiom,
  [--to(E,q105), --eq_____Var__17 cons(X1,X2), ++eq_B X1]).
input_clause(case_cons_eq,axiom,
  [--to(E,q105), --eq_____Var__17 cons(X1,X2), ++eq_____Var__18 X2]).
input_clause(case_cons,axiom,
  [--to(E,q104), --eq_____Var__16 cons(X1,X2), ++to(q104,q105)]).
input_clause(case_cons_eq,axiom,
  [--to(E,q104), --eq_____Var__16 cons(X1,X2), ++eq_A X1]).
input_clause(case_cons_eq,axiom,
  [--to(E,q104), --eq_____Var__16 cons(X1,X2), ++eq_____Var__17 X2]).
input_clause(in,axiom,
  [--to(E,q103), --send(P,X,Y), --eq_from__a X, ++to(q103,q104)]).
input_clause(in_eq,axiom,
  [--to(E,q103), --send(P,X,Y), --eq_from__a X, ++eq_____Var__16 Y]).
input_clause(in_recv,axiom,
  [--to(E,q103), --send(P,X,Y), --eq_from__a X, ++recv(P,X,Y,q104)]).
input_clause(call,axiom,
  [--to(E,q102), --eq_c__pub X1, --eq_c__pub X2, ++to(q102,q103)]).
input_clause(call_eq,axiom,
  [--to(E,q102), --eq_c__pub X1, --eq_c__pub X2, ++eq_from__a X1]).
input_clause(call_eq,axiom,
  [--to(E,q102), --eq_c__pub X1, --eq_c__pub X2, ++eq_to__a X2]).
input_clause(bang,axiom,
  [--to(E,q101), ++to(q101,q102)]).
input_clause(bang_eq,axiom,
  [--to(E,q101), --nat X, ++eq_Pid X]).
input_clause(par,axiom,
  [--to(E,q8), ++to(q8,q101)]).
input_clause(case_crypt_diff,axiom,
  [--to(E,q89), --eq_____Var__12 X, ++to(q89,q91)]).
input_clause(case_cons_diff_crypt,axiom,
  [--to(E,q90), --eq_____Var__13 crypt(X1,X2), ++to(q90,q91)]).
input_clause(case_cons_diff_acrypt,axiom,
  [--to(E,q90), --eq_____Var__13 acrypt(X1,X2), ++to(q90,q91)]).
input_clause(case_cons_diff___nu,axiom,
  [--to(E,q90), --eq_____Var__13 __nu(X1,X2), ++to(q90,q91)]).
input_clause(case_cons_diff_pub,axiom,
  [--to(E,q90), --eq_____Var__13 pub(X1), ++to(q90,q91)]).
input_clause(case_cons_diff_prv,axiom,
  [--to(E,q90), --eq_____Var__13 prv(X1), ++to(q90,q91)]).
input_clause(case_cons_diff___eq,axiom,
  [--to(E,q90), --eq_____Var__13 __eq(X1), ++to(q90,q91)]).
input_clause(case_cons_diff_0,axiom,
  [--to(E,q90), --eq_____Var__13 0, ++to(q90,q91)]).
input_clause(case_cons_diff_kxs,axiom,
  [--to(E,q90), --eq_____Var__13 kxs(X1), ++to(q90,q91)]).
input_clause(case_cons_diff_nil,axiom,
  [--to(E,q90), --eq_____Var__13 nil, ++to(q90,q91)]).
input_clause(case_cons_diff_s,axiom,
  [--to(E,q90), --eq_____Var__13 s(X1), ++to(q90,q91)]).
input_clause(case_cons_diff_crypt,axiom,
  [--to(E,q92), --eq_____Var__14 crypt(X1,X2), ++to(q92,q91)]).
input_clause(case_cons_diff_acrypt,axiom,
  [--to(E,q92), --eq_____Var__14 acrypt(X1,X2), ++to(q92,q91)]).
input_clause(case_cons_diff___nu,axiom,
  [--to(E,q92), --eq_____Var__14 __nu(X1,X2), ++to(q92,q91)]).
input_clause(case_cons_diff_pub,axiom,
  [--to(E,q92), --eq_____Var__14 pub(X1), ++to(q92,q91)]).
input_clause(case_cons_diff_prv,axiom,
  [--to(E,q92), --eq_____Var__14 prv(X1), ++to(q92,q91)]).
input_clause(case_cons_diff___eq,axiom,
  [--to(E,q92), --eq_____Var__14 __eq(X1), ++to(q92,q91)]).
input_clause(case_cons_diff_0,axiom,
  [--to(E,q92), --eq_____Var__14 0, ++to(q92,q91)]).
input_clause(case_cons_diff_kxs,axiom,
  [--to(E,q92), --eq_____Var__14 kxs(X1), ++to(q92,q91)]).
input_clause(case_cons_diff_nil,axiom,
  [--to(E,q92), --eq_____Var__14 nil, ++to(q92,q91)]).
input_clause(case_cons_diff_s,axiom,
  [--to(E,q92), --eq_____Var__14 s(X1), ++to(q92,q91)]).
input_clause(case_nil_diff_crypt,axiom,
  [--to(E,q93), --eq_____Var__15 crypt(X1,X2), ++to(q93,q91)]).
input_clause(case_nil_diff_acrypt,axiom,
  [--to(E,q93), --eq_____Var__15 acrypt(X1,X2), ++to(q93,q91)]).
input_clause(case_nil_diff___nu,axiom,
  [--to(E,q93), --eq_____Var__15 __nu(X1,X2), ++to(q93,q91)]).
input_clause(case_nil_diff_cons,axiom,
  [--to(E,q93), --eq_____Var__15 cons(X1,X2), ++to(q93,q91)]).
input_clause(case_nil_diff_pub,axiom,
  [--to(E,q93), --eq_____Var__15 pub(X1), ++to(q93,q91)]).
input_clause(case_nil_diff_prv,axiom,
  [--to(E,q93), --eq_____Var__15 prv(X1), ++to(q93,q91)]).
input_clause(case_nil_diff___eq,axiom,
  [--to(E,q93), --eq_____Var__15 __eq(X1), ++to(q93,q91)]).
input_clause(case_nil_diff_0,axiom,
  [--to(E,q93), --eq_____Var__15 0, ++to(q93,q91)]).
input_clause(case_nil_diff_kxs,axiom,
  [--to(E,q93), --eq_____Var__15 kxs(X1), ++to(q93,q91)]).
input_clause(case_nil_diff_s,axiom,
  [--to(E,q93), --eq_____Var__15 s(X1), ++to(q93,q91)]).
input_clause(case_crypt_diff,axiom,
  [--to(E,q97), --eq_____Var__10 X, ++to(q97,q99)]).
input_clause(if_diff,axiom,
  [--to(E,q98), --eq_s_of_Nb_end X, --eq_____Var__11 Y, ++to(q98,q99)]).
input_clause(if_eq,axiom,
  [--to(E,q98), --eq_s_of_Nb_end X, --eq_____Var__11 X, ++to(q98,q100)]).
input_clause(case_crypt,axiom,
  [--to(E,q97), --eq_____Var__10 crypt(X,Y), --eq_Kab Y, ++to(q97,q98)]).
input_clause(case_crypt_eq,axiom,
  [--to(E,q97), --eq_____Var__10 crypt(X,Y), --eq_Kab Y, ++eq_____Var__11 X]).
input_clause(in,axiom,
  [--to(E,q96), --send(P,X,Y), --eq_from__a X, ++to(q96,q97)]).
input_clause(in_eq,axiom,
  [--to(E,q96), --send(P,X,Y), --eq_from__a X, ++eq_____Var__10 Y]).
input_clause(in_recv,axiom,
  [--to(E,q96), --send(P,X,Y), --eq_from__a X, ++recv(P,X,Y,q97)]).
input_clause(out,axiom,
  [--to(E,q95), --eq_to__a X, --eq__oc_Nb_cc_Kab Y, ++to(q95,q96)]).
input_clause(out_send,axiom,
  [--to(E,q95), --eq_to__a X, --eq__oc_Nb_cc_Kab Y, ++send(q95,X,Y)]).
input_clause(fun_crypt_eq,axiom,
  [--eq_Nb X1, --eq_Kab X2, ++eq__oc_Nb_cc_Kab crypt(X1,X2)]).
input_clause(new,axiom,
  [--to(E,q94), ++to(q94,q95)]).
input_clause(new_eq,axiom,
  [--to(E,q94), --eq_A X1, --eq_____Var__15 X2, --eq_Kab X3, --eq_____Var__14 X4, --eq_____Var__13 X5, --eq_____Var__12 X6, --eq_to__a X7, --eq_from__a X8, --eq_Kbs X9, ++eq_Nb __nu(q94,__c_of_A_and_____Var__15_and_Kab_and_____Var__14_and_____Var__13_and_____Var__12_and_to__a_and_from__a_and_Kbs_end(X1,X2,X3,X4,X5,X6,X7,X8,X9))]).
input_clause(case_nil,axiom,
  [--to(E,q93), --eq_____Var__15 nil, ++to(q93,q94)]).
input_clause(case_cons,axiom,
  [--to(E,q92), --eq_____Var__14 cons(X1,X2), ++to(q92,q93)]).
input_clause(case_cons_eq,axiom,
  [--to(E,q92), --eq_____Var__14 cons(X1,X2), ++eq_A X1]).
input_clause(case_cons_eq,axiom,
  [--to(E,q92), --eq_____Var__14 cons(X1,X2), ++eq_____Var__15 X2]).
input_clause(case_cons,axiom,
  [--to(E,q90), --eq_____Var__13 cons(X1,X2), ++to(q90,q92)]).
input_clause(case_cons_eq,axiom,
  [--to(E,q90), --eq_____Var__13 cons(X1,X2), ++eq_Kab X1]).
input_clause(case_cons_eq,axiom,
  [--to(E,q90), --eq_____Var__13 cons(X1,X2), ++eq_____Var__14 X2]).
input_clause(case_crypt,axiom,
  [--to(E,q89), --eq_____Var__12 crypt(X,Y), --eq_Kbs Y, ++to(q89,q90)]).
input_clause(case_crypt_eq,axiom,
  [--to(E,q89), --eq_____Var__12 crypt(X,Y), --eq_Kbs Y, ++eq_____Var__13 X]).
input_clause(in,axiom,
  [--to(E,q88), --send(P,X,Y), --eq_from__a X, ++to(q88,q89)]).
input_clause(in_eq,axiom,
  [--to(E,q88), --send(P,X,Y), --eq_from__a X, ++eq_____Var__12 Y]).
input_clause(in_recv,axiom,
  [--to(E,q88), --send(P,X,Y), --eq_from__a X, ++recv(P,X,Y,q89)]).
input_clause(call,axiom,
  [--to(E,q87), --eq_c__pub X1, --eq_c__pub X2, --eq_kxs_of_B_end X3, ++to(q87,q88)]).
input_clause(call_eq,axiom,
  [--to(E,q87), --eq_c__pub X1, --eq_c__pub X2, --eq_kxs_of_B_end X3, ++eq_to__a X1]).
input_clause(call_eq,axiom,
  [--to(E,q87), --eq_c__pub X1, --eq_c__pub X2, --eq_kxs_of_B_end X3, ++eq_from__a X2]).
input_clause(call_eq,axiom,
  [--to(E,q87), --eq_c__pub X1, --eq_c__pub X2, --eq_kxs_of_B_end X3, ++eq_Kbs X3]).
input_clause(fun_kxs_eq,axiom,
  [--eq_B X1, ++eq_kxs_of_B_end kxs(X1)]).
input_clause(par,axiom,
  [--to(E,q67), ++to(q67,q87)]).
input_clause(case_crypt_diff,axiom,
  [--to(E,q72), --eq_____Var__2 X, ++to(q72,q74)]).
input_clause(case_cons_diff_crypt,axiom,
  [--to(E,q73), --eq_____Var__3 crypt(X1,X2), ++to(q73,q74)]).
input_clause(case_cons_diff_acrypt,axiom,
  [--to(E,q73), --eq_____Var__3 acrypt(X1,X2), ++to(q73,q74)]).
input_clause(case_cons_diff___nu,axiom,
  [--to(E,q73), --eq_____Var__3 __nu(X1,X2), ++to(q73,q74)]).
input_clause(case_cons_diff_pub,axiom,
  [--to(E,q73), --eq_____Var__3 pub(X1), ++to(q73,q74)]).
input_clause(case_cons_diff_prv,axiom,
  [--to(E,q73), --eq_____Var__3 prv(X1), ++to(q73,q74)]).
input_clause(case_cons_diff___eq,axiom,
  [--to(E,q73), --eq_____Var__3 __eq(X1), ++to(q73,q74)]).
input_clause(case_cons_diff_0,axiom,
  [--to(E,q73), --eq_____Var__3 0, ++to(q73,q74)]).
input_clause(case_cons_diff_kxs,axiom,
  [--to(E,q73), --eq_____Var__3 kxs(X1), ++to(q73,q74)]).
input_clause(case_cons_diff_nil,axiom,
  [--to(E,q73), --eq_____Var__3 nil, ++to(q73,q74)]).
input_clause(case_cons_diff_s,axiom,
  [--to(E,q73), --eq_____Var__3 s(X1), ++to(q73,q74)]).
input_clause(if_diff,axiom,
  [--to(E,q75), --eq_Na X, --eq_____Var__4 Y, ++to(q75,q74)]).
input_clause(case_cons_diff_crypt,axiom,
  [--to(E,q76), --eq_____Var__5 crypt(X1,X2), ++to(q76,q74)]).
input_clause(case_cons_diff_acrypt,axiom,
  [--to(E,q76), --eq_____Var__5 acrypt(X1,X2), ++to(q76,q74)]).
input_clause(case_cons_diff___nu,axiom,
  [--to(E,q76), --eq_____Var__5 __nu(X1,X2), ++to(q76,q74)]).
input_clause(case_cons_diff_pub,axiom,
  [--to(E,q76), --eq_____Var__5 pub(X1), ++to(q76,q74)]).
input_clause(case_cons_diff_prv,axiom,
  [--to(E,q76), --eq_____Var__5 prv(X1), ++to(q76,q74)]).
input_clause(case_cons_diff___eq,axiom,
  [--to(E,q76), --eq_____Var__5 __eq(X1), ++to(q76,q74)]).
input_clause(case_cons_diff_0,axiom,
  [--to(E,q76), --eq_____Var__5 0, ++to(q76,q74)]).
input_clause(case_cons_diff_kxs,axiom,
  [--to(E,q76), --eq_____Var__5 kxs(X1), ++to(q76,q74)]).
input_clause(case_cons_diff_nil,axiom,
  [--to(E,q76), --eq_____Var__5 nil, ++to(q76,q74)]).
input_clause(case_cons_diff_s,axiom,
  [--to(E,q76), --eq_____Var__5 s(X1), ++to(q76,q74)]).
input_clause(if_diff,axiom,
  [--to(E,q77), --eq_B X, --eq_____Var__6 Y, ++to(q77,q74)]).
input_clause(case_cons_diff_crypt,axiom,
  [--to(E,q78), --eq_____Var__7 crypt(X1,X2), ++to(q78,q74)]).
input_clause(case_cons_diff_acrypt,axiom,
  [--to(E,q78), --eq_____Var__7 acrypt(X1,X2), ++to(q78,q74)]).
input_clause(case_cons_diff___nu,axiom,
  [--to(E,q78), --eq_____Var__7 __nu(X1,X2), ++to(q78,q74)]).
input_clause(case_cons_diff_pub,axiom,
  [--to(E,q78), --eq_____Var__7 pub(X1), ++to(q78,q74)]).
input_clause(case_cons_diff_prv,axiom,
  [--to(E,q78), --eq_____Var__7 prv(X1), ++to(q78,q74)]).
input_clause(case_cons_diff___eq,axiom,
  [--to(E,q78), --eq_____Var__7 __eq(X1), ++to(q78,q74)]).
input_clause(case_cons_diff_0,axiom,
  [--to(E,q78), --eq_____Var__7 0, ++to(q78,q74)]).
input_clause(case_cons_diff_kxs,axiom,
  [--to(E,q78), --eq_____Var__7 kxs(X1), ++to(q78,q74)]).
input_clause(case_cons_diff_nil,axiom,
  [--to(E,q78), --eq_____Var__7 nil, ++to(q78,q74)]).
input_clause(case_cons_diff_s,axiom,
  [--to(E,q78), --eq_____Var__7 s(X1), ++to(q78,q74)]).
input_clause(case_cons_diff_crypt,axiom,
  [--to(E,q79), --eq_____Var__8 crypt(X1,X2), ++to(q79,q74)]).
input_clause(case_cons_diff_acrypt,axiom,
  [--to(E,q79), --eq_____Var__8 acrypt(X1,X2), ++to(q79,q74)]).
input_clause(case_cons_diff___nu,axiom,
  [--to(E,q79), --eq_____Var__8 __nu(X1,X2), ++to(q79,q74)]).
input_clause(case_cons_diff_pub,axiom,
  [--to(E,q79), --eq_____Var__8 pub(X1), ++to(q79,q74)]).
input_clause(case_cons_diff_prv,axiom,
  [--to(E,q79), --eq_____Var__8 prv(X1), ++to(q79,q74)]).
input_clause(case_cons_diff___eq,axiom,
  [--to(E,q79), --eq_____Var__8 __eq(X1), ++to(q79,q74)]).
input_clause(case_cons_diff_0,axiom,
  [--to(E,q79), --eq_____Var__8 0, ++to(q79,q74)]).
input_clause(case_cons_diff_kxs,axiom,
  [--to(E,q79), --eq_____Var__8 kxs(X1), ++to(q79,q74)]).
input_clause(case_cons_diff_nil,axiom,
  [--to(E,q79), --eq_____Var__8 nil, ++to(q79,q74)]).
input_clause(case_cons_diff_s,axiom,
  [--to(E,q79), --eq_____Var__8 s(X1), ++to(q79,q74)]).
input_clause(case_nil_diff_crypt,axiom,
  [--to(E,q80), --eq_____Var__9 crypt(X1,X2), ++to(q80,q74)]).
input_clause(case_nil_diff_acrypt,axiom,
  [--to(E,q80), --eq_____Var__9 acrypt(X1,X2), ++to(q80,q74)]).
input_clause(case_nil_diff___nu,axiom,
  [--to(E,q80), --eq_____Var__9 __nu(X1,X2), ++to(q80,q74)]).
input_clause(case_nil_diff_cons,axiom,
  [--to(E,q80), --eq_____Var__9 cons(X1,X2), ++to(q80,q74)]).
input_clause(case_nil_diff_pub,axiom,
  [--to(E,q80), --eq_____Var__9 pub(X1), ++to(q80,q74)]).
input_clause(case_nil_diff_prv,axiom,
  [--to(E,q80), --eq_____Var__9 prv(X1), ++to(q80,q74)]).
input_clause(case_nil_diff___eq,axiom,
  [--to(E,q80), --eq_____Var__9 __eq(X1), ++to(q80,q74)]).
input_clause(case_nil_diff_0,axiom,
  [--to(E,q80), --eq_____Var__9 0, ++to(q80,q74)]).
input_clause(case_nil_diff_kxs,axiom,
  [--to(E,q80), --eq_____Var__9 kxs(X1), ++to(q80,q74)]).
input_clause(case_nil_diff_s,axiom,
  [--to(E,q80), --eq_____Var__9 s(X1), ++to(q80,q74)]).
input_clause(case_crypt_diff,axiom,
  [--to(E,q83), --eq_____Var__1 X, ++to(q83,q85)]).
input_clause(out,axiom,
  [--to(E,q84), --eq_to__b X, --eq__oc_s_of_Nb_end_cc_Kab Y, ++to(q84,q86)]).
input_clause(out_send,axiom,
  [--to(E,q84), --eq_to__b X, --eq__oc_s_of_Nb_end_cc_Kab Y, ++send(q84,X,Y)]).
input_clause(fun_s_eq,axiom,
  [--eq_Nb X1, ++eq_s_of_Nb_end s(X1)]).
input_clause(fun_crypt_eq,axiom,
  [--eq_s_of_Nb_end X1, --eq_Kab X2, ++eq__oc_s_of_Nb_end_cc_Kab crypt(X1,X2)]).
input_clause(case_crypt,axiom,
  [--to(E,q83), --eq_____Var__1 crypt(X,Y), --eq_Kab Y, ++to(q83,q84)]).
input_clause(case_crypt_eq,axiom,
  [--to(E,q83), --eq_____Var__1 crypt(X,Y), --eq_Kab Y, ++eq_Nb X]).
input_clause(in,axiom,
  [--to(E,q82), --send(P,X,Y), --eq_from__b X, ++to(q82,q83)]).
input_clause(in_eq,axiom,
  [--to(E,q82), --send(P,X,Y), --eq_from__b X, ++eq_____Var__1 Y]).
input_clause(in_recv,axiom,
  [--to(E,q82), --send(P,X,Y), --eq_from__b X, ++recv(P,X,Y,q83)]).
input_clause(out,axiom,
  [--to(E,q81), --eq_to__b X, --eq_M Y, ++to(q81,q82)]).
input_clause(out_send,axiom,
  [--to(E,q81), --eq_to__b X, --eq_M Y, ++send(q81,X,Y)]).
input_clause(case_nil,axiom,
  [--to(E,q80), --eq_____Var__9 nil, ++to(q80,q81)]).
input_clause(case_cons,axiom,
  [--to(E,q79), --eq_____Var__8 cons(X1,X2), ++to(q79,q80)]).
input_clause(case_cons_eq,axiom,
  [--to(E,q79), --eq_____Var__8 cons(X1,X2), ++eq_M X1]).
input_clause(case_cons_eq,axiom,
  [--to(E,q79), --eq_____Var__8 cons(X1,X2), ++eq_____Var__9 X2]).
input_clause(case_cons,axiom,
  [--to(E,q78), --eq_____Var__7 cons(X1,X2), ++to(q78,q79)]).
input_clause(case_cons_eq,axiom,
  [--to(E,q78), --eq_____Var__7 cons(X1,X2), ++eq_Kab X1]).
input_clause(case_cons_eq,axiom,
  [--to(E,q78), --eq_____Var__7 cons(X1,X2), ++eq_____Var__8 X2]).
input_clause(if_eq,axiom,
  [--to(E,q77), --eq_B X, --eq_____Var__6 X, ++to(q77,q78)]).
input_clause(case_cons,axiom,
  [--to(E,q76), --eq_____Var__5 cons(X1,X2), ++to(q76,q77)]).
input_clause(case_cons_eq,axiom,
  [--to(E,q76), --eq_____Var__5 cons(X1,X2), ++eq_____Var__6 X1]).
input_clause(case_cons_eq,axiom,
  [--to(E,q76), --eq_____Var__5 cons(X1,X2), ++eq_____Var__7 X2]).
input_clause(if_eq,axiom,
  [--to(E,q75), --eq_Na X, --eq_____Var__4 X, ++to(q75,q76)]).
input_clause(case_cons,axiom,
  [--to(E,q73), --eq_____Var__3 cons(X1,X2), ++to(q73,q75)]).
input_clause(case_cons_eq,axiom,
  [--to(E,q73), --eq_____Var__3 cons(X1,X2), ++eq_____Var__4 X1]).
input_clause(case_cons_eq,axiom,
  [--to(E,q73), --eq_____Var__3 cons(X1,X2), ++eq_____Var__5 X2]).
input_clause(case_crypt,axiom,
  [--to(E,q72), --eq_____Var__2 crypt(X,Y), --eq_Kas Y, ++to(q72,q73)]).
input_clause(case_crypt_eq,axiom,
  [--to(E,q72), --eq_____Var__2 crypt(X,Y), --eq_Kas Y, ++eq_____Var__3 X]).
input_clause(in,axiom,
  [--to(E,q71), --send(P,X,Y), --eq_from__s X, ++to(q71,q72)]).
input_clause(in_eq,axiom,
  [--to(E,q71), --send(P,X,Y), --eq_from__s X, ++eq_____Var__2 Y]).
input_clause(in_recv,axiom,
  [--to(E,q71), --send(P,X,Y), --eq_from__s X, ++recv(P,X,Y,q72)]).
input_clause(out,axiom,
  [--to(E,q70), --eq_to__s X, --eq_cons_of_A_and_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end_end Y, ++to(q70,q71)]).
input_clause(out_send,axiom,
  [--to(E,q70), --eq_to__s X, --eq_cons_of_A_and_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end_end Y, ++send(q70,X,Y)]).
input_clause(fun_cons_eq,axiom,
  [--eq_Na X1, --eq_nil_of__end X2, ++eq_cons_of_Na_and_nil_of__end_end cons(X1,X2)]).
input_clause(fun_cons_eq,axiom,
  [--eq_B X1, --eq_cons_of_Na_and_nil_of__end_end X2, ++eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end cons(X1,X2)]).
input_clause(fun_cons_eq,axiom,
  [--eq_A X1, --eq_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end X2, ++eq_cons_of_A_and_cons_of_B_and_cons_of_Na_and_nil_of__end_end_end_end cons(X1,X2)]).
input_clause(new,axiom,
  [--to(E,q69), ++to(q69,q70)]).
input_clause(new_eq,axiom,
  [--to(E,q69), --eq_to__s X1, --eq_from__s X2, --eq_to__b X3, --eq_from__b X4, --eq_A X5, --eq_B X6, --eq_Kas X7, ++eq_Na __nu(q69,__c_of_to__s_and_from__s_and_to__b_and_from__b_and_A_and_B_and_Kas_end(X1,X2,X3,X4,X5,X6,X7))]).
input_clause(call,axiom,
  [--to(E,q68), --eq_c__pub X1, --eq_c__pub X2, --eq_c__pub X3, --eq_c__pub X4, --eq_A X5, --eq_B X6, --eq_kxs_of_A_end X7, ++to(q68,q69)]).
input_clause(call_eq,axiom,
  [--to(E,q68), --eq_c__pub X1, --eq_c__pub X2, --eq_c__pub X3, --eq_c__pub X4, --eq_A X5, --eq_B X6, --eq_kxs_of_A_end X7, ++eq_to__s X1]).
input_clause(call_eq,axiom,
  [--to(E,q68), --eq_c__pub X1, --eq_c__pub X2, --eq_c__pub X3, --eq_c__pub X4, --eq_A X5, --eq_B X6, --eq_kxs_of_A_end X7, ++eq_from__s X2]).
input_clause(call_eq,axiom,
  [--to(E,q68), --eq_c__pub X1, --eq_c__pub X2, --eq_c__pub X3, --eq_c__pub X4, --eq_A X5, --eq_B X6, --eq_kxs_of_A_end X7, ++eq_to__b X3]).
input_clause(call_eq,axiom,
  [--to(E,q68), --eq_c__pub X1, --eq_c__pub X2, --eq_c__pub X3, --eq_c__pub X4, --eq_A X5, --eq_B X6, --eq_kxs_of_A_end X7, ++eq_from__b X4]).
input_clause(call_eq,axiom,
  [--to(E,q68), --eq_c__pub X1, --eq_c__pub X2, --eq_c__pub X3, --eq_c__pub X4, --eq_A X5, --eq_B X6, --eq_kxs_of_A_end X7, ++eq_A X5]).
input_clause(call_eq,axiom,
  [--to(E,q68), --eq_c__pub X1, --eq_c__pub X2, --eq_c__pub X3, --eq_c__pub X4, --eq_A X5, --eq_B X6, --eq_kxs_of_A_end X7, ++eq_B X6]).
input_clause(call_eq,axiom,
  [--to(E,q68), --eq_c__pub X1, --eq_c__pub X2, --eq_c__pub X3, --eq_c__pub X4, --eq_A X5, --eq_B X6, --eq_kxs_of_A_end X7, ++eq_Kas X7]).
input_clause(fun_kxs_eq,axiom,
  [--eq_A X1, ++eq_kxs_of_A_end kxs(X1)]).
input_clause(par,axiom,
  [--to(E,q67), ++to(q67,q68)]).
input_clause(let,axiom,
  [--to(E,q66), --eq_cons_of_b_and_cons_of_b__no_and_nil_of__end_end_end X, ++to(q66,q67)]).
input_clause(let_eq,axiom,
  [--to(E,q66), --eq_cons_of_b_and_cons_of_b__no_and_nil_of__end_end_end X, ++eq_B X]).
input_clause(fun_cons_eq,axiom,
  [--eq_b__no X1, --eq_nil_of__end X2, ++eq_cons_of_b__no_and_nil_of__end_end cons(X1,X2)]).
input_clause(fun_cons_eq,axiom,
  [--eq_b X1, --eq_cons_of_b__no_and_nil_of__end_end X2, ++eq_cons_of_b_and_cons_of_b__no_and_nil_of__end_end_end cons(X1,X2)]).
input_clause(let,axiom,
  [--to(E,q65), --eq_cons_of_a_and_cons_of_a__no_and_nil_of__end_end_end X, ++to(q65,q66)]).
input_clause(let_eq,axiom,
  [--to(E,q65), --eq_cons_of_a_and_cons_of_a__no_and_nil_of__end_end_end X, ++eq_A X]).
input_clause(fun_cons_eq,axiom,
  [--eq_a__no X1, --eq_nil_of__end X2, ++eq_cons_of_a__no_and_nil_of__end_end cons(X1,X2)]).
input_clause(fun_cons_eq,axiom,
  [--eq_a X1, --eq_cons_of_a__no_and_nil_of__end_end X2, ++eq_cons_of_a_and_cons_of_a__no_and_nil_of__end_end_end cons(X1,X2)]).
input_clause(bang,axiom,
  [--to(E,q64), ++to(q64,q65)]).
input_clause(bang_eq,axiom,
  [--to(E,q64), --nat X, ++eq_b__no X]).
input_clause(bang,axiom,
  [--to(E,q63), ++to(q63,q64)]).
input_clause(bang_eq,axiom,
  [--to(E,q63), --nat X, ++eq_a__no X]).
input_clause(par,axiom,
  [--to(E,q8), ++to(q8,q63)]).
input_clause(case_cons_diff_crypt,axiom,
  [--to(E,q60), --eq_M crypt(X1,X2), ++to(q60,q28)]).
input_clause(case_cons_diff_acrypt,axiom,
  [--to(E,q60), --eq_M acrypt(X1,X2), ++to(q60,q28)]).
input_clause(case_cons_diff___nu,axiom,
  [--to(E,q60), --eq_M __nu(X1,X2), ++to(q60,q28)]).
input_clause(case_cons_diff_pub,axiom,
  [--to(E,q60), --eq_M pub(X1), ++to(q60,q28)]).
input_clause(case_cons_diff_prv,axiom,
  [--to(E,q60), --eq_M prv(X1), ++to(q60,q28)]).
input_clause(case_cons_diff___eq,axiom,
  [--to(E,q60), --eq_M __eq(X1), ++to(q60,q28)]).
input_clause(case_cons_diff_0,axiom,
  [--to(E,q60), --eq_M 0, ++to(q60,q28)]).
input_clause(case_cons_diff_kxs,axiom,
  [--to(E,q60), --eq_M kxs(X1), ++to(q60,q28)]).
input_clause(case_cons_diff_nil,axiom,
  [--to(E,q60), --eq_M nil, ++to(q60,q28)]).
input_clause(case_cons_diff_s,axiom,
  [--to(E,q60), --eq_M s(X1), ++to(q60,q28)]).
input_clause(out,axiom,
  [--to(E,q62), --eq_c__out X, --eq_M2 Y, ++to(q62,q28)]).
input_clause(out_send,axiom,
  [--to(E,q62), --eq_c__out X, --eq_M2 Y, ++send(q62,X,Y)]).
input_clause(par,axiom,
  [--to(E,q61), ++to(q61,q62)]).
input_clause(par,axiom,
  [--to(E,q61), ++to(q61,q49)]).
input_clause(case_cons,axiom,
  [--to(E,q60), --eq_M cons(X1,X2), ++to(q60,q61)]).
input_clause(case_cons_eq,axiom,
  [--to(E,q60), --eq_M cons(X1,X2), ++eq_M1 X1]).
input_clause(case_cons_eq,axiom,
  [--to(E,q60), --eq_M cons(X1,X2), ++eq_M2 X2]).
input_clause(in,axiom,
  [--to(E,q59), --send(P,X,Y), --eq_c__in X, ++to(q59,q60)]).
input_clause(in_eq,axiom,
  [--to(E,q59), --send(P,X,Y), --eq_c__in X, ++eq_M Y]).
input_clause(in_recv,axiom,
  [--to(E,q59), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q60)]).
input_clause(par,axiom,
  [--to(E,q45), ++to(q45,q59)]).
input_clause(case_0_diff_crypt,axiom,
  [--to(E,q58), --eq_M crypt(X1,X2), ++to(q58,q28)]).
input_clause(case_0_diff_acrypt,axiom,
  [--to(E,q58), --eq_M acrypt(X1,X2), ++to(q58,q28)]).
input_clause(case_0_diff___nu,axiom,
  [--to(E,q58), --eq_M __nu(X1,X2), ++to(q58,q28)]).
input_clause(case_0_diff_cons,axiom,
  [--to(E,q58), --eq_M cons(X1,X2), ++to(q58,q28)]).
input_clause(case_0_diff_pub,axiom,
  [--to(E,q58), --eq_M pub(X1), ++to(q58,q28)]).
input_clause(case_0_diff_prv,axiom,
  [--to(E,q58), --eq_M prv(X1), ++to(q58,q28)]).
input_clause(case_0_diff___eq,axiom,
  [--to(E,q58), --eq_M __eq(X1), ++to(q58,q28)]).
input_clause(case_0_diff_kxs,axiom,
  [--to(E,q58), --eq_M kxs(X1), ++to(q58,q28)]).
input_clause(case_0_diff_nil,axiom,
  [--to(E,q58), --eq_M nil, ++to(q58,q28)]).
input_clause(case_0_diff_s,axiom,
  [--to(E,q58), --eq_M s(X1), ++to(q58,q28)]).
input_clause(case_0,axiom,
  [--to(E,q58), --eq_M 0, ++to(q58,q28)]).
input_clause(in,axiom,
  [--to(E,q57), --send(P,X,Y), --eq_c__in X, ++to(q57,q58)]).
input_clause(in_eq,axiom,
  [--to(E,q57), --send(P,X,Y), --eq_c__in X, ++eq_M Y]).
input_clause(in_recv,axiom,
  [--to(E,q57), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q58)]).
input_clause(par,axiom,
  [--to(E,q45), ++to(q45,q57)]).
input_clause(case_nil_diff_crypt,axiom,
  [--to(E,q56), --eq_M crypt(X1,X2), ++to(q56,q28)]).
input_clause(case_nil_diff_acrypt,axiom,
  [--to(E,q56), --eq_M acrypt(X1,X2), ++to(q56,q28)]).
input_clause(case_nil_diff___nu,axiom,
  [--to(E,q56), --eq_M __nu(X1,X2), ++to(q56,q28)]).
input_clause(case_nil_diff_cons,axiom,
  [--to(E,q56), --eq_M cons(X1,X2), ++to(q56,q28)]).
input_clause(case_nil_diff_pub,axiom,
  [--to(E,q56), --eq_M pub(X1), ++to(q56,q28)]).
input_clause(case_nil_diff_prv,axiom,
  [--to(E,q56), --eq_M prv(X1), ++to(q56,q28)]).
input_clause(case_nil_diff___eq,axiom,
  [--to(E,q56), --eq_M __eq(X1), ++to(q56,q28)]).
input_clause(case_nil_diff_0,axiom,
  [--to(E,q56), --eq_M 0, ++to(q56,q28)]).
input_clause(case_nil_diff_kxs,axiom,
  [--to(E,q56), --eq_M kxs(X1), ++to(q56,q28)]).
input_clause(case_nil_diff_s,axiom,
  [--to(E,q56), --eq_M s(X1), ++to(q56,q28)]).
input_clause(case_nil,axiom,
  [--to(E,q56), --eq_M nil, ++to(q56,q28)]).
input_clause(in,axiom,
  [--to(E,q55), --send(P,X,Y), --eq_c__in X, ++to(q55,q56)]).
input_clause(in_eq,axiom,
  [--to(E,q55), --send(P,X,Y), --eq_c__in X, ++eq_M Y]).
input_clause(in_recv,axiom,
  [--to(E,q55), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q56)]).
input_clause(par,axiom,
  [--to(E,q45), ++to(q45,q55)]).
input_clause(case_s_diff_crypt,axiom,
  [--to(E,q54), --eq_M crypt(X1,X2), ++to(q54,q28)]).
input_clause(case_s_diff_acrypt,axiom,
  [--to(E,q54), --eq_M acrypt(X1,X2), ++to(q54,q28)]).
input_clause(case_s_diff___nu,axiom,
  [--to(E,q54), --eq_M __nu(X1,X2), ++to(q54,q28)]).
input_clause(case_s_diff_cons,axiom,
  [--to(E,q54), --eq_M cons(X1,X2), ++to(q54,q28)]).
input_clause(case_s_diff_pub,axiom,
  [--to(E,q54), --eq_M pub(X1), ++to(q54,q28)]).
input_clause(case_s_diff_prv,axiom,
  [--to(E,q54), --eq_M prv(X1), ++to(q54,q28)]).
input_clause(case_s_diff___eq,axiom,
  [--to(E,q54), --eq_M __eq(X1), ++to(q54,q28)]).
input_clause(case_s_diff_0,axiom,
  [--to(E,q54), --eq_M 0, ++to(q54,q28)]).
input_clause(case_s_diff_kxs,axiom,
  [--to(E,q54), --eq_M kxs(X1), ++to(q54,q28)]).
input_clause(case_s_diff_nil,axiom,
  [--to(E,q54), --eq_M nil, ++to(q54,q28)]).
input_clause(case_s,axiom,
  [--to(E,q54), --eq_M s(X1), ++to(q54,q49)]).
input_clause(case_s_eq,axiom,
  [--to(E,q54), --eq_M s(X1), ++eq_M1 X1]).
input_clause(in,axiom,
  [--to(E,q53), --send(P,X,Y), --eq_c__in X, ++to(q53,q54)]).
input_clause(in_eq,axiom,
  [--to(E,q53), --send(P,X,Y), --eq_c__in X, ++eq_M Y]).
input_clause(in_recv,axiom,
  [--to(E,q53), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q54)]).
input_clause(par,axiom,
  [--to(E,q45), ++to(q45,q53)]).
input_clause(case_crypt_diff,axiom,
  [--to(E,q52), --eq_M X, ++to(q52,q28)]).
input_clause(case_crypt,axiom,
  [--to(E,q52), --eq_M crypt(X,Y), --eq_inv_M2 Y, ++to(q52,q49)]).
input_clause(case_crypt_eq,axiom,
  [--to(E,q52), --eq_M crypt(X,Y), --eq_inv_M2 Y, ++eq_M1 X]).
input_clause(pub_inv,axiom,
  [--eq_M2 pub(X), ++eq_inv_M2 prv(X)]).
input_clause(prv_inv,axiom,
  [--eq_M2 prv(X), ++eq_inv_M2 pub(X)]).
input_clause(in,axiom,
  [--to(E,q51), --send(P,X,Y), --eq_c__in X, ++to(q51,q52)]).
input_clause(in_eq,axiom,
  [--to(E,q51), --send(P,X,Y), --eq_c__in X, ++eq_M2 Y]).
input_clause(in_recv,axiom,
  [--to(E,q51), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q52)]).
input_clause(in,axiom,
  [--to(E,q50), --send(P,X,Y), --eq_c__in X, ++to(q50,q51)]).
input_clause(in_eq,axiom,
  [--to(E,q50), --send(P,X,Y), --eq_c__in X, ++eq_M Y]).
input_clause(in_recv,axiom,
  [--to(E,q50), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q51)]).
input_clause(par,axiom,
  [--to(E,q45), ++to(q45,q50)]).
input_clause(case_crypt_diff,axiom,
  [--to(E,q48), --eq_M X, ++to(q48,q28)]).
input_clause(out,axiom,
  [--to(E,q49), --eq_c__out X, --eq_M1 Y, ++to(q49,q28)]).
input_clause(out_send,axiom,
  [--to(E,q49), --eq_c__out X, --eq_M1 Y, ++send(q49,X,Y)]).
input_clause(case_crypt,axiom,
  [--to(E,q48), --eq_M crypt(X,Y), --eq_M2 Y, ++to(q48,q49)]).
input_clause(case_crypt_eq,axiom,
  [--to(E,q48), --eq_M crypt(X,Y), --eq_M2 Y, ++eq_M1 X]).
input_clause(in,axiom,
  [--to(E,q47), --send(P,X,Y), --eq_c__in X, ++to(q47,q48)]).
input_clause(in_eq,axiom,
  [--to(E,q47), --send(P,X,Y), --eq_c__in X, ++eq_M2 Y]).
input_clause(in_recv,axiom,
  [--to(E,q47), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q48)]).
input_clause(in,axiom,
  [--to(E,q46), --send(P,X,Y), --eq_c__in X, ++to(q46,q47)]).
input_clause(in_eq,axiom,
  [--to(E,q46), --send(P,X,Y), --eq_c__in X, ++eq_M Y]).
input_clause(in_recv,axiom,
  [--to(E,q46), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q47)]).
input_clause(par,axiom,
  [--to(E,q45), ++to(q45,q46)]).
input_clause(call,axiom,
  [--to(E,q44), --eq_pub__channel X1, --eq_pub__channel X2, ++to(q44,q45)]).
input_clause(call_eq,axiom,
  [--to(E,q44), --eq_pub__channel X1, --eq_pub__channel X2, ++eq_c__in X1]).
input_clause(call_eq,axiom,
  [--to(E,q44), --eq_pub__channel X1, --eq_pub__channel X2, ++eq_c__out X2]).
input_clause(par,axiom,
  [--to(E,q12), ++to(q12,q44)]).
input_clause(out,axiom,
  [--to(E,q43), --eq_c__out X, --eq__oc_M1_cc_M2 Y, ++to(q43,q28)]).
input_clause(out_send,axiom,
  [--to(E,q43), --eq_c__out X, --eq__oc_M1_cc_M2 Y, ++send(q43,X,Y)]).
input_clause(fun_crypt_eq,axiom,
  [--eq_M1 X1, --eq_M2 X2, ++eq__oc_M1_cc_M2 crypt(X1,X2)]).
input_clause(in,axiom,
  [--to(E,q42), --send(P,X,Y), --eq_c__in X, ++to(q42,q43)]).
input_clause(in_eq,axiom,
  [--to(E,q42), --send(P,X,Y), --eq_c__in X, ++eq_M2 Y]).
input_clause(in_recv,axiom,
  [--to(E,q42), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q43)]).
input_clause(in,axiom,
  [--to(E,q41), --send(P,X,Y), --eq_c__in X, ++to(q41,q42)]).
input_clause(in_eq,axiom,
  [--to(E,q41), --send(P,X,Y), --eq_c__in X, ++eq_M1 Y]).
input_clause(in_recv,axiom,
  [--to(E,q41), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q42)]).
input_clause(par,axiom,
  [--to(E,q25), ++to(q25,q41)]).
input_clause(out,axiom,
  [--to(E,q40), --eq_c__out X, --eq__ob_M1_cb_M2 Y, ++to(q40,q28)]).
input_clause(out_send,axiom,
  [--to(E,q40), --eq_c__out X, --eq__ob_M1_cb_M2 Y, ++send(q40,X,Y)]).
input_clause(fun_acrypt_eq,axiom,
  [--eq_M1 X1, --eq_M2 X2, ++eq__ob_M1_cb_M2 acrypt(X1,X2)]).
input_clause(in,axiom,
  [--to(E,q39), --send(P,X,Y), --eq_c__in X, ++to(q39,q40)]).
input_clause(in_eq,axiom,
  [--to(E,q39), --send(P,X,Y), --eq_c__in X, ++eq_M2 Y]).
input_clause(in_recv,axiom,
  [--to(E,q39), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q40)]).
input_clause(in,axiom,
  [--to(E,q38), --send(P,X,Y), --eq_c__in X, ++to(q38,q39)]).
input_clause(in_eq,axiom,
  [--to(E,q38), --send(P,X,Y), --eq_c__in X, ++eq_M1 Y]).
input_clause(in_recv,axiom,
  [--to(E,q38), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q39)]).
input_clause(par,axiom,
  [--to(E,q25), ++to(q25,q38)]).
input_clause(out,axiom,
  [--to(E,q37), --eq_c__out X, --eq_cons_of_M1_and_M2_end Y, ++to(q37,q28)]).
input_clause(out_send,axiom,
  [--to(E,q37), --eq_c__out X, --eq_cons_of_M1_and_M2_end Y, ++send(q37,X,Y)]).
input_clause(fun_cons_eq,axiom,
  [--eq_M1 X1, --eq_M2 X2, ++eq_cons_of_M1_and_M2_end cons(X1,X2)]).
input_clause(in,axiom,
  [--to(E,q36), --send(P,X,Y), --eq_c__in X, ++to(q36,q37)]).
input_clause(in_eq,axiom,
  [--to(E,q36), --send(P,X,Y), --eq_c__in X, ++eq_M2 Y]).
input_clause(in_recv,axiom,
  [--to(E,q36), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q37)]).
input_clause(in,axiom,
  [--to(E,q35), --send(P,X,Y), --eq_c__in X, ++to(q35,q36)]).
input_clause(in_eq,axiom,
  [--to(E,q35), --send(P,X,Y), --eq_c__in X, ++eq_M1 Y]).
input_clause(in_recv,axiom,
  [--to(E,q35), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q36)]).
input_clause(par,axiom,
  [--to(E,q25), ++to(q25,q35)]).
input_clause(out,axiom,
  [--to(E,q34), --eq_c__out X, --eq_pub_of_M1_end Y, ++to(q34,q28)]).
input_clause(out_send,axiom,
  [--to(E,q34), --eq_c__out X, --eq_pub_of_M1_end Y, ++send(q34,X,Y)]).
input_clause(fun_pub_eq,axiom,
  [--eq_M1 X1, ++eq_pub_of_M1_end pub(X1)]).
input_clause(in,axiom,
  [--to(E,q33), --send(P,X,Y), --eq_c__in X, ++to(q33,q34)]).
input_clause(in_eq,axiom,
  [--to(E,q33), --send(P,X,Y), --eq_c__in X, ++eq_M1 Y]).
input_clause(in_recv,axiom,
  [--to(E,q33), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q34)]).
input_clause(par,axiom,
  [--to(E,q25), ++to(q25,q33)]).
input_clause(out,axiom,
  [--to(E,q32), --eq_c__out X, --eq_prv_of_M1_end Y, ++to(q32,q28)]).
input_clause(out_send,axiom,
  [--to(E,q32), --eq_c__out X, --eq_prv_of_M1_end Y, ++send(q32,X,Y)]).
input_clause(fun_prv_eq,axiom,
  [--eq_M1 X1, ++eq_prv_of_M1_end prv(X1)]).
input_clause(in,axiom,
  [--to(E,q31), --send(P,X,Y), --eq_c__in X, ++to(q31,q32)]).
input_clause(in_eq,axiom,
  [--to(E,q31), --send(P,X,Y), --eq_c__in X, ++eq_M1 Y]).
input_clause(in_recv,axiom,
  [--to(E,q31), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q32)]).
input_clause(par,axiom,
  [--to(E,q25), ++to(q25,q31)]).
input_clause(out,axiom,
  [--to(E,q30), --eq_c__out X, --eq_0_of__end Y, ++to(q30,q28)]).
input_clause(out_send,axiom,
  [--to(E,q30), --eq_c__out X, --eq_0_of__end Y, ++send(q30,X,Y)]).
input_clause(par,axiom,
  [--to(E,q25), ++to(q25,q30)]).
input_clause(out,axiom,
  [--to(E,q29), --eq_c__out X, --eq_nil_of__end Y, ++to(q29,q28)]).
input_clause(out_send,axiom,
  [--to(E,q29), --eq_c__out X, --eq_nil_of__end Y, ++send(q29,X,Y)]).
input_clause(fun_nil_eq,axiom,
  [++eq_nil_of__end nil]).
input_clause(par,axiom,
  [--to(E,q25), ++to(q25,q29)]).
input_clause(out,axiom,
  [--to(E,q27), --eq_c__out X, --eq_s_of_M1_end Y, ++to(q27,q28)]).
input_clause(out_send,axiom,
  [--to(E,q27), --eq_c__out X, --eq_s_of_M1_end Y, ++send(q27,X,Y)]).
input_clause(fun_s_eq,axiom,
  [--eq_M1 X1, ++eq_s_of_M1_end s(X1)]).
input_clause(in,axiom,
  [--to(E,q26), --send(P,X,Y), --eq_c__in X, ++to(q26,q27)]).
input_clause(in_eq,axiom,
  [--to(E,q26), --send(P,X,Y), --eq_c__in X, ++eq_M1 Y]).
input_clause(in_recv,axiom,
  [--to(E,q26), --send(P,X,Y), --eq_c__in X, ++recv(P,X,Y,q27)]).
input_clause(par,axiom,
  [--to(E,q25), ++to(q25,q26)]).
input_clause(call,axiom,
  [--to(E,q24), --eq_pub__channel X1, --eq_pub__channel X2, ++to(q24,q25)]).
input_clause(call_eq,axiom,
  [--to(E,q24), --eq_pub__channel X1, --eq_pub__channel X2, ++eq_c__in X1]).
input_clause(call_eq,axiom,
  [--to(E,q24), --eq_pub__channel X1, --eq_pub__channel X2, ++eq_c__out X2]).
input_clause(par,axiom,
  [--to(E,q12), ++to(q12,q24)]).
input_clause(out,axiom,
  [--to(E,q22), --eq_pub__channel X, --eq_N Y, ++to(q22,q23)]).
input_clause(out_send,axiom,
  [--to(E,q22), --eq_pub__channel X, --eq_N Y, ++send(q22,X,Y)]).
input_clause(new,axiom,
  [--to(E,q21), ++to(q21,q22)]).
input_clause(new_eq,axiom,
  [--to(E,q21), --eq_Pid X1, --eq_pub__channel X2, --eq_initial__knowledge X3, ++eq_N __nu(q21,__c_of_Pid_and_pub__channel_and_initial__knowledge_end(X1,X2,X3))]).
input_clause(par,axiom,
  [--to(E,q12), ++to(q12,q21)]).
input_clause(out,axiom,
  [--to(E,q19), --eq_pub__channel X, --eq_M Y, ++to(q19,q20)]).
input_clause(out_send,axiom,
  [--to(E,q19), --eq_pub__channel X, --eq_M Y, ++send(q19,X,Y)]).
input_clause(out,axiom,
  [--to(E,q18), --eq_pub__channel X, --eq_M Y, ++to(q18,q19)]).
input_clause(out_send,axiom,
  [--to(E,q18), --eq_pub__channel X, --eq_M Y, ++send(q18,X,Y)]).
input_clause(in,axiom,
  [--to(E,q17), --send(P,X,Y), --eq_pub__channel X, ++to(q17,q18)]).
input_clause(in_eq,axiom,
  [--to(E,q17), --send(P,X,Y), --eq_pub__channel X, ++eq_M Y]).
input_clause(in_recv,axiom,
  [--to(E,q17), --send(P,X,Y), --eq_pub__channel X, ++recv(P,X,Y,q18)]).
input_clause(par,axiom,
  [--to(E,q12), ++to(q12,q17)]).
input_clause(out,axiom,
  [--to(E,q15), --eq_pub__channel X, --eq_id Y, ++to(q15,q16)]).
input_clause(out_send,axiom,
  [--to(E,q15), --eq_pub__channel X, --eq_id Y, ++send(q15,X,Y)]).
input_clause(par,axiom,
  [--to(E,q12), ++to(q12,q15)]).
input_clause(out,axiom,
  [--to(E,q13), --eq_pub__channel X, --eq_initial__knowledge Y, ++to(q13,q14)]).
input_clause(out_send,axiom,
  [--to(E,q13), --eq_pub__channel X, --eq_initial__knowledge Y, ++send(q13,X,Y)]).
input_clause(par,axiom,
  [--to(E,q12), ++to(q12,q13)]).
input_clause(bang,axiom,
  [--to(E,q11), ++to(q11,q12)]).
input_clause(bang_eq,axiom,
  [--to(E,q11), --nat X, ++eq_Pid X]).
input_clause(new,axiom,
  [--to(E,q10), ++to(q10,q11)]).
input_clause(new_eq,axiom,
  [--to(E,q10), --eq_pub__channel X1, --eq_initial__knowledge X2, ++eq_id __nu(q10,__c_of_pub__channel_and_initial__knowledge_end(X1,X2))]).
input_clause(call,axiom,
  [--to(E,q9), --eq_c__pub X1, --eq_0_of__end X2, ++to(q9,q10)]).
input_clause(call_eq,axiom,
  [--to(E,q9), --eq_c__pub X1, --eq_0_of__end X2, ++eq_pub__channel X1]).
input_clause(call_eq,axiom,
  [--to(E,q9), --eq_c__pub X1, --eq_0_of__end X2, ++eq_initial__knowledge X2]).
input_clause(fun_0_eq,axiom,
  [++eq_0_of__end 0]).
input_clause(par,axiom,
  [--to(E,q8), ++to(q8,q9)]).
input_clause(new,axiom,
  [--to(E,q7), ++to(q7,q8)]).
input_clause(new_eq,axiom,
  [--to(E,q7), ++eq_Kbs __nu(q7,__c_of__end)]).
input_clause(new,axiom,
  [--to(E,q6), ++to(q6,q7)]).
input_clause(new_eq,axiom,
  [--to(E,q6), ++eq_Kas __nu(q6,__c_of__end)]).
input_clause(new,axiom,
  [--to(E,q5), ++to(q5,q6)]).
input_clause(new_eq,axiom,
  [--to(E,q5), ++eq_b __nu(q5,__c_of__end)]).
input_clause(new,axiom,
  [--to(E,q4), ++to(q4,q5)]).
input_clause(new_eq,axiom,
  [--to(E,q4), ++eq_a __nu(q4,__c_of__end)]).
input_clause(new,axiom,
  [--to(E,q3), ++to(q3,q4)]).
input_clause(new_eq,axiom,
  [--to(E,q3), ++eq_c__pub __nu(q3,__c_of__end)]).
input_clause(call,axiom,
  [--to(E,q2), ++to(q2,q3)]).
input_clause(start,axiom,
  [++to(q1,q2)]).
input_clause(zero,axiom,
  [++nat 0]).
input_clause(s,axiom,
  [--nat X, ++nat s(X)]).