%-------------------------------------------------------------------------------
% File     : alice.p
% Domain   : PointsTo analysis
% Problem  : Performs pointer analysis
% Version  : 
% English  :     
%-------------------------------------------------------------------------------


% Function = bBN_hex2bn
% Params :
%   cipher : int 
%   temp : int 
% Return = int
% Je renomme cipher par bBN_hex2bn_1
% Je renomme temp par bBN_hex2bn_2

input_clause(clauses_1, axiom,
          [
          --values( bBN_hex2bn_1 , address( X ) ) ,
          --values( bBN_hex2bn_2 , address( T ) ) ,
          --values( T , Z ),
          ++values( X , Z )
          ]).


% Function = close
% Params :
%   fd : int 
% Return = int
% Je renomme fd par close_1


% Function = atoi
% Params :
%   nptr : int 
% Return = int
% Je renomme nptr par atoi_1

input_clause(clauses_2, axiom,
          [
          --values( atoi_1 , Z ),
          ++values( atoi_return , Z )
          ]).


% Function = rRAND_bytes
% Params :
%   nonce : int 
%   size : int 
% Return = int
% Je renomme nonce par rRAND_bytes_1
% Je renomme size par rRAND_bytes_2

input_clause(clauses_3, axiom,
          [
          --values( rRAND_bytes_1 , address( A ) ),
          ++values( A , A )
          ]).


% Function = time
% Params :
%   t : int 
% Return = int
% Je renomme t par time_1


% Function = bBN_new
% Params :
%   void : int 
% Return = int
% Je renomme void par bBN_new_1

input_clause(clauses_4, axiom,
          [
          ++values( cipher_1 , cipher_1 )
          ]).

input_clause(clauses_5, axiom,
          [
          ++values( cipher_2 , cipher_2 )
          ]).

input_clause(clauses_6, axiom,
          [
          ++values( cipher_3 , cipher_3 )
          ]).


% Function = srandom
% Params :
%   seed : int 
% Return = int
% Je renomme seed par srandom_1


% Function = bBN_bn2hex
% Params :
%   cipher : int 
% Return = int
% Je renomme cipher par bBN_bn2hex_1

input_clause(clauses_7, axiom,
          [
          ++values( bBN_bn2hex_return , bBN_bn2hex_1 )
          ]).


% Function = read
% Params :
%   fd : int 
%   buff : int 
%   size : int 
% Return = int
% Je renomme fd par read_1
% Je renomme buff par read_2
% Je renomme size par read_3

input_clause(clauses_8, axiom,
          [
          --values( read_2 , address( B ) ) ,
          --knows( X ),
          ++values( B , X )
          ]).


% Function = memcpy
% Params :
%   dest : int 
%   src : int 
%   size : int 
% Return = int
% Je renomme dest par memcpy_1
% Je renomme src par memcpy_2
% Je renomme size par memcpy_3

input_clause(clauses_9, axiom,
          [
          --values( memcpy_1 , address( X ) ) ,
          --values( memcpy_2 , address( Z ) ),
          ++values( X , Z )
          ]).


% Function = write
% Params :
%   fd : int 
%   buff : int 
%   size : int 
% Return = int
% Je renomme fd par write_1
% Je renomme buff par write_2
% Je renomme size par write_3

input_clause(clauses_10, axiom,
          [
          --values( write_2 , X ) ,
          --values( X , Y ) ,
          --fun_write( nil ),
          ++knows( Y )
          ]).


% Function = strcpy
% Params :
%   dest : int 
%   src : int 
% Return = int
% Je renomme dest par strcpy_1
% Je renomme src par strcpy_2

input_clause(clauses_11, axiom,
          [
          --values( strcpy_1 , address( X ) ) ,
          --values( strcpy_2 , address( Z ) ),
          ++values( X , Z )
          ]).


% Function = key_gen
% Params :
%   nskey : int 
%   pub_key : int 
% Return = int
% Je renomme nskey par key_gen_1
% Je renomme pub_key par key_gen_2
% Je renomme ctx par key_gen_3
% Je renomme res par key_gen_4
% Je renomme n par key_gen_5
% Je renomme p par key_gen_6
% Je renomme q par key_gen_7
% Je renomme phi_n par key_gen_8


% Function = printf_keys
% Params :
%   nskey : int 
% Return = int
% Je renomme nskey par printf_keys_1


% Function = my_decypher
% Params :
%   cipher : int 
%   priv_key : int 
%   plain : int 
% Return = int
% Je renomme cipher par my_decypher_1
% Je renomme priv_key par my_decypher_2
% Je renomme plain par my_decypher_3
% Je renomme msg_len par my_decypher_4
% Je renomme bn_plain par my_decypher_5
% Je renomme ctx par my_decypher_6

input_clause(clauses_12, axiom,
          [
          --fun_my_decypher( nil ) ,
          --values( my_decypher_1 , crypt( X , pub( alice ) ) ) ,
          --values( my_decypher_3 , address( Y ) ),
          ++values( Y , X )
          ]).


% Function = create_bind_socket
% Params :
%   port : int 
% Return = int
% Je renomme port par create_bind_socket_1
% Je renomme opt par create_bind_socket_2
% Je renomme listen_fd par create_bind_socket_3


% Function = printf_message
% Params :
%   msg : int 
% Return = int
% Je renomme msg par printf_message_1


% Function = print_connect_error
% Params :
%   err : int 
% Return = int
% Je renomme err par print_connect_error_1


% Function = connect_socket
% Params :
%   addr : int 
%   port : int 
% Return = int
% Je renomme addr par connect_socket_1
% Je renomme port par connect_socket_2
% Je renomme sock_fd par connect_socket_3
% Je renomme err par connect_socket_4


% Function = key_of_string
% Params :
%   kpub : int 
%   kpriv : int 
%   kmod : int 
%   nskey : int 
% Return = int
% Je renomme kpub par key_of_string_1
% Je renomme kpriv par key_of_string_2
% Je renomme kmod par key_of_string_3
% Je renomme nskey par key_of_string_4


% Function = main
% Params :
%   argc : int 
%   argv : char **
% Return = int

input_clause(clauses_13, axiom,
          [
          --fun_main( nil ),
          ++values( x21 , 12 )
          ]).

input_clause(clauses_14, axiom,
          [
          --fun_main( nil ) ,
          --values( x21 , Z ),
          ++values( x20 , Z )
          ]).

input_clause(clauses_15, axiom,
          [
          --fun_main( nil ),
          ++values( malloc_1 , x20 )
          ]).

input_clause(clauses_16, axiom,
          [
          --fun_main( nil ),
          ++fun_malloc( nil )
          ]).

input_clause(clauses_17, axiom,
          [
          --fun_main( nil ) ,
          --values( malloc_return , Z ),
          ++values( x19 , Z )
          ]).

input_clause(clauses_18, axiom,
          [
          --fun_main( nil ) ,
          --values( x19 , Z ),
          ++values( alice_key , Z )
          ]).

input_clause(clauses_19, axiom,
          [
          --fun_main( nil ) ,
          --values( alice_key , Z ),
          ++values( x18 , Z )
          ]).

input_clause(clauses_20, axiom,
          [
          --fun_main( nil ),
          ++values( x25 , 12 )
          ]).

input_clause(clauses_21, axiom,
          [
          --fun_main( nil ) ,
          --values( x25 , Z ),
          ++values( x24 , Z )
          ]).

input_clause(clauses_22, axiom,
          [
          --fun_main( nil ),
          ++values( malloc_1 , x24 )
          ]).

input_clause(clauses_23, axiom,
          [
          --fun_main( nil ),
          ++fun_malloc( nil )
          ]).

input_clause(clauses_24, axiom,
          [
          --fun_main( nil ) ,
          --values( malloc_return , Z ),
          ++values( x23 , Z )
          ]).

input_clause(clauses_25, axiom,
          [
          --fun_main( nil ) ,
          --values( x23 , Z ),
          ++values( bob_key , Z )
          ]).

input_clause(clauses_26, axiom,
          [
          --fun_main( nil ) ,
          --values( bob_key , Z ),
          ++values( x22 , Z )
          ]).

input_clause(clauses_27, axiom,
          [
          --fun_main( nil ),
          ++values( x29 , string )
          ]).

input_clause(clauses_28, axiom,
          [
          --fun_main( nil ) ,
          --values( x29 , Z ),
          ++values( x28 , Z )
          ]).

input_clause(clauses_29, axiom,
          [
          --fun_main( nil ) ,
          --values( x28 , Z ),
          ++values( x27 , Z )
          ]).

input_clause(clauses_30, axiom,
          [
          --fun_main( nil ),
          ++values( x32 , string )
          ]).

input_clause(clauses_31, axiom,
          [
          --fun_main( nil ) ,
          --values( x32 , Z ),
          ++values( x31 , Z )
          ]).

input_clause(clauses_32, axiom,
          [
          --fun_main( nil ) ,
          --values( x31 , Z ),
          ++values( x30 , Z )
          ]).

input_clause(clauses_33, axiom,
          [
          --fun_main( nil ),
          ++values( x35 , string )
          ]).

input_clause(clauses_34, axiom,
          [
          --fun_main( nil ) ,
          --values( x35 , Z ),
          ++values( x34 , Z )
          ]).

input_clause(clauses_35, axiom,
          [
          --fun_main( nil ) ,
          --values( x34 , Z ),
          ++values( x33 , Z )
          ]).

input_clause(clauses_36, axiom,
          [
          --fun_main( nil ),
          ++values( key_of_string_1 , x27 )
          ]).

input_clause(clauses_37, axiom,
          [
          --fun_main( nil ),
          ++values( key_of_string_2 , x30 )
          ]).

input_clause(clauses_38, axiom,
          [
          --fun_main( nil ),
          ++values( key_of_string_3 , x33 )
          ]).

input_clause(clauses_39, axiom,
          [
          --fun_main( nil ),
          ++values( key_of_string_4 , alice_key )
          ]).

input_clause(clauses_40, axiom,
          [
          --fun_main( nil ),
          ++fun_key_of_string( nil )
          ]).

input_clause(clauses_41, axiom,
          [
          --fun_main( nil ) ,
          --values( key_of_string_return , Z ),
          ++values( x26 , Z )
          ]).

input_clause(clauses_42, axiom,
          [
          --fun_main( nil ),
          ++values( x39 , string )
          ]).

input_clause(clauses_43, axiom,
          [
          --fun_main( nil ) ,
          --values( x39 , Z ),
          ++values( x38 , Z )
          ]).

input_clause(clauses_44, axiom,
          [
          --fun_main( nil ) ,
          --values( x38 , Z ),
          ++values( x37 , Z )
          ]).

input_clause(clauses_45, axiom,
          [
          --fun_main( nil ),
          ++values( x42 , string )
          ]).

input_clause(clauses_46, axiom,
          [
          --fun_main( nil ) ,
          --values( x42 , Z ),
          ++values( x41 , Z )
          ]).

input_clause(clauses_47, axiom,
          [
          --fun_main( nil ) ,
          --values( x41 , Z ),
          ++values( x40 , Z )
          ]).

input_clause(clauses_48, axiom,
          [
          --fun_main( nil ),
          ++values( x45 , string )
          ]).

input_clause(clauses_49, axiom,
          [
          --fun_main( nil ) ,
          --values( x45 , Z ),
          ++values( x44 , Z )
          ]).

input_clause(clauses_50, axiom,
          [
          --fun_main( nil ) ,
          --values( x44 , Z ),
          ++values( x43 , Z )
          ]).

input_clause(clauses_51, axiom,
          [
          --fun_main( nil ),
          ++values( key_of_string_1 , x37 )
          ]).

input_clause(clauses_52, axiom,
          [
          --fun_main( nil ),
          ++values( key_of_string_2 , x40 )
          ]).

input_clause(clauses_53, axiom,
          [
          --fun_main( nil ),
          ++values( key_of_string_3 , x43 )
          ]).

input_clause(clauses_54, axiom,
          [
          --fun_main( nil ),
          ++values( key_of_string_4 , bob_key )
          ]).

input_clause(clauses_55, axiom,
          [
          --fun_main( nil ),
          ++fun_key_of_string( nil )
          ]).

input_clause(clauses_56, axiom,
          [
          --fun_main( nil ) ,
          --values( key_of_string_return , Z ),
          ++values( x36 , Z )
          ]).

input_clause(clauses_57, axiom,
          [
          --fun_main( nil ),
          ++values( x49 , string )
          ]).

input_clause(clauses_58, axiom,
          [
          --fun_main( nil ) ,
          --values( x49 , Z ),
          ++values( x48 , Z )
          ]).

input_clause(clauses_59, axiom,
          [
          --fun_main( nil ) ,
          --values( x48 , Z ),
          ++values( x47 , Z )
          ]).

input_clause(clauses_60, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x47 )
          ]).

input_clause(clauses_61, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_62, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x46 , Z )
          ]).

input_clause(clauses_63, axiom,
          [
          --fun_main( nil ),
          ++values( printf_keys_1 , alice_key )
          ]).

input_clause(clauses_64, axiom,
          [
          --fun_main( nil ),
          ++fun_printf_keys( nil )
          ]).

input_clause(clauses_65, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_keys_return , Z ),
          ++values( x50 , Z )
          ]).

input_clause(clauses_66, axiom,
          [
          --fun_main( nil ),
          ++values( x54 , string )
          ]).

input_clause(clauses_67, axiom,
          [
          --fun_main( nil ) ,
          --values( x54 , Z ),
          ++values( x53 , Z )
          ]).

input_clause(clauses_68, axiom,
          [
          --fun_main( nil ) ,
          --values( x53 , Z ),
          ++values( x52 , Z )
          ]).

input_clause(clauses_69, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x52 )
          ]).

input_clause(clauses_70, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_71, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x51 , Z )
          ]).

input_clause(clauses_72, axiom,
          [
          --fun_main( nil ),
          ++values( printf_keys_1 , bob_key )
          ]).

input_clause(clauses_73, axiom,
          [
          --fun_main( nil ),
          ++fun_printf_keys( nil )
          ]).

input_clause(clauses_74, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_keys_return , Z ),
          ++values( x55 , Z )
          ]).

input_clause(clauses_75, axiom,
          [
          --fun_main( nil ),
          ++values( alice_port , 12344 )
          ]).

input_clause(clauses_76, axiom,
          [
          --fun_main( nil ) ,
          --values( alice_port , Z ),
          ++values( x56 , Z )
          ]).

input_clause(clauses_77, axiom,
          [
          --fun_main( nil ),
          ++values( x60 , address( alice ) )
          ]).

input_clause(clauses_78, axiom,
          [
          --fun_main( nil ) ,
          --values( x60 , Z ),
          ++values( x59 , Z )
          ]).

input_clause(clauses_79, axiom,
          [
          --fun_main( nil ) ,
          --values( x59 , Z ),
          ++values( x58 , Z )
          ]).

input_clause(clauses_80, axiom,
          [
          --fun_main( nil ),
          ++values( x63 , string )
          ]).

input_clause(clauses_81, axiom,
          [
          --fun_main( nil ) ,
          --values( x63 , Z ),
          ++values( x62 , Z )
          ]).

input_clause(clauses_82, axiom,
          [
          --fun_main( nil ) ,
          --values( x62 , Z ),
          ++values( x61 , Z )
          ]).

input_clause(clauses_83, axiom,
          [
          --fun_main( nil ),
          ++values( strcpy_1 , x58 )
          ]).

input_clause(clauses_84, axiom,
          [
          --fun_main( nil ),
          ++values( strcpy_2 , x61 )
          ]).

input_clause(clauses_85, axiom,
          [
          --fun_main( nil ),
          ++fun_strcpy( nil )
          ]).

input_clause(clauses_86, axiom,
          [
          --fun_main( nil ) ,
          --values( strcpy_return , Z ),
          ++values( x57 , Z )
          ]).

input_clause(clauses_87, axiom,
          [
          --fun_main( nil ),
          ++values( bob_port , 12345 )
          ]).

input_clause(clauses_88, axiom,
          [
          --fun_main( nil ) ,
          --values( bob_port , Z ),
          ++values( x64 , Z )
          ]).

input_clause(clauses_89, axiom,
          [
          --fun_main( nil ),
          ++values( x68 , address( bob ) )
          ]).

input_clause(clauses_90, axiom,
          [
          --fun_main( nil ) ,
          --values( x68 , Z ),
          ++values( x67 , Z )
          ]).

input_clause(clauses_91, axiom,
          [
          --fun_main( nil ) ,
          --values( x67 , Z ),
          ++values( x66 , Z )
          ]).

input_clause(clauses_92, axiom,
          [
          --fun_main( nil ),
          ++values( x71 , string )
          ]).

input_clause(clauses_93, axiom,
          [
          --fun_main( nil ) ,
          --values( x71 , Z ),
          ++values( x70 , Z )
          ]).

input_clause(clauses_94, axiom,
          [
          --fun_main( nil ) ,
          --values( x70 , Z ),
          ++values( x69 , Z )
          ]).

input_clause(clauses_95, axiom,
          [
          --fun_main( nil ),
          ++values( strcpy_1 , x66 )
          ]).

input_clause(clauses_96, axiom,
          [
          --fun_main( nil ),
          ++values( strcpy_2 , x69 )
          ]).

input_clause(clauses_97, axiom,
          [
          --fun_main( nil ),
          ++fun_strcpy( nil )
          ]).

input_clause(clauses_98, axiom,
          [
          --fun_main( nil ) ,
          --values( strcpy_return , Z ),
          ++values( x65 , Z )
          ]).

input_clause(clauses_99, axiom,
          [
          --fun_main( nil ),
          ++values( x73 , 3 )
          ]).

input_clause(clauses_100, axiom,
          [
          --fun_main( nil ),
          ++values( x72 , 1 )
          ]).

input_clause(clauses_101, axiom,
          [
          --fun_main( nil ),
          ++values( x72 , 0 )
          ]).

input_clause(clauses_102, axiom,
          [
          --fun_main( nil ),
          ++values( x77 , address( bob ) )
          ]).

input_clause(clauses_103, axiom,
          [
          --fun_main( nil ) ,
          --values( x77 , Z ),
          ++values( x76 , Z )
          ]).

input_clause(clauses_104, axiom,
          [
          --fun_main( nil ) ,
          --values( x76 , Z ),
          ++values( x75 , Z )
          ]).

input_clause(clauses_105, axiom,
          [
          --fun_main( nil ),
          ++values( x82 , 1 )
          ]).

input_clause(clauses_106, axiom,
          [
          --fun_main( nil ) ,
          --values( x82 , Z ),
          ++values( x81 , Z )
          ]).

input_clause(clauses_107, axiom,
          [
          --fun_main( nil ),
          ++values( x80 , address( offset( argv , x81 ) ) )
          ]).

input_clause(clauses_108, axiom,
          [
          --fun_main( nil ) ,
          --values( x80 , address( Y ) ) ,
          --values( Y , Z ),
          ++values( x79 , Z )
          ]).

input_clause(clauses_109, axiom,
          [
          --fun_main( nil ) ,
          --values( x79 , Z ),
          ++values( x78 , Z )
          ]).

input_clause(clauses_110, axiom,
          [
          --fun_main( nil ),
          ++values( strcpy_1 , x75 )
          ]).

input_clause(clauses_111, axiom,
          [
          --fun_main( nil ),
          ++values( strcpy_2 , x78 )
          ]).

input_clause(clauses_112, axiom,
          [
          --fun_main( nil ),
          ++fun_strcpy( nil )
          ]).

input_clause(clauses_113, axiom,
          [
          --fun_main( nil ) ,
          --values( strcpy_return , Z ),
          ++values( x74 , Z )
          ]).

input_clause(clauses_114, axiom,
          [
          --fun_main( nil ),
          ++values( x88 , 2 )
          ]).

input_clause(clauses_115, axiom,
          [
          --fun_main( nil ) ,
          --values( x88 , Z ),
          ++values( x87 , Z )
          ]).

input_clause(clauses_116, axiom,
          [
          --fun_main( nil ),
          ++values( x86 , address( offset( argv , x87 ) ) )
          ]).

input_clause(clauses_117, axiom,
          [
          --fun_main( nil ) ,
          --values( x86 , address( Y ) ) ,
          --values( Y , Z ),
          ++values( x85 , Z )
          ]).

input_clause(clauses_118, axiom,
          [
          --fun_main( nil ) ,
          --values( x85 , Z ),
          ++values( x84 , Z )
          ]).

input_clause(clauses_119, axiom,
          [
          --fun_main( nil ),
          ++values( atoi_1 , x84 )
          ]).

input_clause(clauses_120, axiom,
          [
          --fun_main( nil ),
          ++fun_atoi( nil )
          ]).

input_clause(clauses_121, axiom,
          [
          --fun_main( nil ) ,
          --values( atoi_return , Z ),
          ++values( bob_port , Z )
          ]).

input_clause(clauses_122, axiom,
          [
          --fun_main( nil ) ,
          --values( bob_port , Z ),
          ++values( x83 , Z )
          ]).

input_clause(clauses_123, axiom,
          [
          --fun_main( nil ),
          ++values( x90 , 3 )
          ]).

input_clause(clauses_124, axiom,
          [
          --fun_main( nil ),
          ++values( x89 , 1 )
          ]).

input_clause(clauses_125, axiom,
          [
          --fun_main( nil ),
          ++values( x89 , 0 )
          ]).

input_clause(clauses_126, axiom,
          [
          --fun_main( nil ),
          ++values( x92 , 1 )
          ]).

input_clause(clauses_127, axiom,
          [
          --fun_main( nil ),
          ++values( exit_1 , x92 )
          ]).

input_clause(clauses_128, axiom,
          [
          --fun_main( nil ),
          ++fun_exit( nil )
          ]).

input_clause(clauses_129, axiom,
          [
          --fun_main( nil ) ,
          --values( exit_return , Z ),
          ++values( x91 , Z )
          ]).

input_clause(clauses_130, axiom,
          [
          --fun_main( nil ),
          ++values( x96 , string )
          ]).

input_clause(clauses_131, axiom,
          [
          --fun_main( nil ) ,
          --values( x96 , Z ),
          ++values( x95 , Z )
          ]).

input_clause(clauses_132, axiom,
          [
          --fun_main( nil ) ,
          --values( x95 , Z ),
          ++values( x94 , Z )
          ]).

input_clause(clauses_133, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x94 )
          ]).

input_clause(clauses_134, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_135, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x93 , Z )
          ]).

input_clause(clauses_136, axiom,
          [
          --fun_main( nil ),
          ++values( x100 , string )
          ]).

input_clause(clauses_137, axiom,
          [
          --fun_main( nil ) ,
          --values( x100 , Z ),
          ++values( x99 , Z )
          ]).

input_clause(clauses_138, axiom,
          [
          --fun_main( nil ) ,
          --values( x99 , Z ),
          ++values( x98 , Z )
          ]).

input_clause(clauses_139, axiom,
          [
          --fun_main( nil ),
          ++values( x101 , address( alice ) )
          ]).

input_clause(clauses_140, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x98 )
          ]).

input_clause(clauses_141, axiom,
          [
          --fun_main( nil ),
          ++values( printf_2 , x101 )
          ]).

input_clause(clauses_142, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_143, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x97 , Z )
          ]).

input_clause(clauses_144, axiom,
          [
          --fun_main( nil ),
          ++values( x105 , string )
          ]).

input_clause(clauses_145, axiom,
          [
          --fun_main( nil ) ,
          --values( x105 , Z ),
          ++values( x104 , Z )
          ]).

input_clause(clauses_146, axiom,
          [
          --fun_main( nil ) ,
          --values( x104 , Z ),
          ++values( x103 , Z )
          ]).

input_clause(clauses_147, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x103 )
          ]).

input_clause(clauses_148, axiom,
          [
          --fun_main( nil ),
          ++values( printf_2 , alice_port )
          ]).

input_clause(clauses_149, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_150, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x102 , Z )
          ]).

input_clause(clauses_151, axiom,
          [
          --fun_main( nil ),
          ++values( x109 , string )
          ]).

input_clause(clauses_152, axiom,
          [
          --fun_main( nil ) ,
          --values( x109 , Z ),
          ++values( x108 , Z )
          ]).

input_clause(clauses_153, axiom,
          [
          --fun_main( nil ) ,
          --values( x108 , Z ),
          ++values( x107 , Z )
          ]).

input_clause(clauses_154, axiom,
          [
          --fun_main( nil ),
          ++values( x110 , address( bob ) )
          ]).

input_clause(clauses_155, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x107 )
          ]).

input_clause(clauses_156, axiom,
          [
          --fun_main( nil ),
          ++values( printf_2 , x110 )
          ]).

input_clause(clauses_157, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_158, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x106 , Z )
          ]).

input_clause(clauses_159, axiom,
          [
          --fun_main( nil ),
          ++values( x114 , string )
          ]).

input_clause(clauses_160, axiom,
          [
          --fun_main( nil ) ,
          --values( x114 , Z ),
          ++values( x113 , Z )
          ]).

input_clause(clauses_161, axiom,
          [
          --fun_main( nil ) ,
          --values( x113 , Z ),
          ++values( x112 , Z )
          ]).

input_clause(clauses_162, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x112 )
          ]).

input_clause(clauses_163, axiom,
          [
          --fun_main( nil ),
          ++values( printf_2 , bob_port )
          ]).

input_clause(clauses_164, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_165, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x111 , Z )
          ]).

input_clause(clauses_166, axiom,
          [
          --fun_main( nil ),
          ++values( x118 , string )
          ]).

input_clause(clauses_167, axiom,
          [
          --fun_main( nil ) ,
          --values( x118 , Z ),
          ++values( x117 , Z )
          ]).

input_clause(clauses_168, axiom,
          [
          --fun_main( nil ) ,
          --values( x117 , Z ),
          ++values( x116 , Z )
          ]).

input_clause(clauses_169, axiom,
          [
          --fun_main( nil ),
          ++values( x119 , address( bob ) )
          ]).

input_clause(clauses_170, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x116 )
          ]).

input_clause(clauses_171, axiom,
          [
          --fun_main( nil ),
          ++values( printf_2 , x119 )
          ]).

input_clause(clauses_172, axiom,
          [
          --fun_main( nil ),
          ++values( printf_3 , bob_port )
          ]).

input_clause(clauses_173, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_174, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x115 , Z )
          ]).

input_clause(clauses_175, axiom,
          [
          --fun_main( nil ),
          ++values( x123 , address( bob ) )
          ]).

input_clause(clauses_176, axiom,
          [
          --fun_main( nil ) ,
          --values( x123 , Z ),
          ++values( x122 , Z )
          ]).

input_clause(clauses_177, axiom,
          [
          --fun_main( nil ) ,
          --values( x122 , Z ),
          ++values( x121 , Z )
          ]).

input_clause(clauses_178, axiom,
          [
          --fun_main( nil ),
          ++values( connect_socket_1 , x121 )
          ]).

input_clause(clauses_179, axiom,
          [
          --fun_main( nil ),
          ++values( connect_socket_2 , bob_port )
          ]).

input_clause(clauses_180, axiom,
          [
          --fun_main( nil ),
          ++fun_connect_socket( nil )
          ]).

input_clause(clauses_181, axiom,
          [
          --fun_main( nil ) ,
          --values( connect_socket_return , Z ),
          ++values( conn_fd , Z )
          ]).

input_clause(clauses_182, axiom,
          [
          --fun_main( nil ) ,
          --values( conn_fd , Z ),
          ++values( x120 , Z )
          ]).

input_clause(clauses_183, axiom,
          [
          --fun_main( nil ),
          ++values( x127 , string )
          ]).

input_clause(clauses_184, axiom,
          [
          --fun_main( nil ) ,
          --values( x127 , Z ),
          ++values( x126 , Z )
          ]).

input_clause(clauses_185, axiom,
          [
          --fun_main( nil ) ,
          --values( x126 , Z ),
          ++values( x125 , Z )
          ]).

input_clause(clauses_186, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x125 )
          ]).

input_clause(clauses_187, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_188, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x124 , Z )
          ]).

input_clause(clauses_189, axiom,
          [
          --fun_main( nil ),
          ++values( x131 , address( nonceA ) )
          ]).

input_clause(clauses_190, axiom,
          [
          --fun_main( nil ) ,
          --values( x131 , Z ),
          ++values( x130 , Z )
          ]).

input_clause(clauses_191, axiom,
          [
          --fun_main( nil ) ,
          --values( x130 , Z ),
          ++values( x129 , Z )
          ]).

input_clause(clauses_192, axiom,
          [
          --fun_main( nil ),
          ++values( x132 , 16 )
          ]).

input_clause(clauses_193, axiom,
          [
          --fun_main( nil ),
          ++values( rRAND_bytes_1 , x129 )
          ]).

input_clause(clauses_194, axiom,
          [
          --fun_main( nil ),
          ++values( rRAND_bytes_2 , x132 )
          ]).

input_clause(clauses_195, axiom,
          [
          --fun_main( nil ),
          ++fun_rRAND_bytes( nil )
          ]).

input_clause(clauses_196, axiom,
          [
          --fun_main( nil ) ,
          --values( rRAND_bytes_return , Z ),
          ++values( x128 , Z )
          ]).

input_clause(clauses_197, axiom,
          [
          --fun_main( nil ),
          ++values( x135 , address( alice_mess_1 ) )
          ]).

input_clause(clauses_198, axiom,
          [
          --fun_main( nil ),
          ++values( x134 , address( field( x135 , msg_type ) ) )
          ]).

input_clause(clauses_199, axiom,
          [
          --fun_main( nil ),
          ++values( x133 , 1 )
          ]).

input_clause(clauses_200, axiom,
          [
          --fun_main( nil ) ,
          --values( x134 , address( Z ) ) ,
          --values( x133 , Y ),
          ++values( Z , Y )
          ]).

input_clause(clauses_201, axiom,
          [
          --fun_main( nil ),
          ++values( x140 , address( alice_mess_1 ) )
          ]).

input_clause(clauses_202, axiom,
          [
          --fun_main( nil ),
          ++values( x139 , address( field( x140 , msg ) ) )
          ]).

input_clause(clauses_203, axiom,
          [
          --fun_main( nil ),
          ++values( x138 , address( field( x139 , msg1 ) ) )
          ]).

input_clause(clauses_204, axiom,
          [
          --fun_main( nil ),
          ++values( x137 , address( field( x138 , id ) ) )
          ]).

input_clause(clauses_205, axiom,
          [
          --fun_main( nil ),
          ++values( x141 , 0 )
          ]).

input_clause(clauses_206, axiom,
          [
          --fun_main( nil ) ,
          --values( x141 , Z ),
          ++values( x136 , Z )
          ]).

input_clause(clauses_207, axiom,
          [
          --fun_main( nil ) ,
          --values( x137 , address( Z ) ) ,
          --values( x136 , Y ),
          ++values( Z , Y )
          ]).

input_clause(clauses_208, axiom,
          [
          --fun_main( nil ),
          ++values( x148 , address( alice_mess_1 ) )
          ]).

input_clause(clauses_209, axiom,
          [
          --fun_main( nil ),
          ++values( x147 , address( field( x148 , msg ) ) )
          ]).

input_clause(clauses_210, axiom,
          [
          --fun_main( nil ),
          ++values( x146 , address( field( x147 , msg1 ) ) )
          ]).

input_clause(clauses_211, axiom,
          [
          --fun_main( nil ),
          ++values( x145 , address( field( x146 , nonce ) ) )
          ]).

input_clause(clauses_212, axiom,
          [
          --fun_main( nil ) ,
          --values( x145 , Z ),
          ++values( x144 , Z )
          ]).

input_clause(clauses_213, axiom,
          [
          --fun_main( nil ) ,
          --values( x144 , Z ),
          ++values( x143 , Z )
          ]).

input_clause(clauses_214, axiom,
          [
          --fun_main( nil ),
          ++values( x150 , address( nonceA ) )
          ]).

input_clause(clauses_215, axiom,
          [
          --fun_main( nil ) ,
          --values( x150 , Z ),
          ++values( x149 , Z )
          ]).

input_clause(clauses_216, axiom,
          [
          --fun_main( nil ),
          ++values( x152 , 16 )
          ]).

input_clause(clauses_217, axiom,
          [
          --fun_main( nil ) ,
          --values( x152 , Z ),
          ++values( x151 , Z )
          ]).

input_clause(clauses_218, axiom,
          [
          --fun_main( nil ),
          ++values( memcpy_1 , x143 )
          ]).

input_clause(clauses_219, axiom,
          [
          --fun_main( nil ),
          ++values( memcpy_2 , x149 )
          ]).

input_clause(clauses_220, axiom,
          [
          --fun_main( nil ),
          ++values( memcpy_3 , x151 )
          ]).

input_clause(clauses_221, axiom,
          [
          --fun_main( nil ),
          ++fun_memcpy( nil )
          ]).

input_clause(clauses_222, axiom,
          [
          --fun_main( nil ) ,
          --values( memcpy_return , Z ),
          ++values( x142 , Z )
          ]).

input_clause(clauses_223, axiom,
          [
          --fun_main( nil ),
          ++fun_bBN_new( nil )
          ]).

input_clause(clauses_224, axiom,
          [
          --fun_main( nil ) ,
          --values( bBN_new_return , Z ),
          ++values( cipher_1 , Z )
          ]).

input_clause(clauses_225, axiom,
          [
          --fun_main( nil ) ,
          --values( cipher_1 , Z ),
          ++values( x153 , Z )
          ]).

input_clause(clauses_226, axiom,
          [
          --fun_main( nil ),
          ++values( x155 , address( alice_mess_1 ) )
          ]).

input_clause(clauses_227, axiom,
          [
          --fun_main( nil ),
          ++values( my_cypher_1 , x155 )
          ]).

input_clause(clauses_228, axiom,
          [
          --fun_main( nil ),
          ++values( my_cypher_2 , bob_key )
          ]).

input_clause(clauses_229, axiom,
          [
          --fun_main( nil ),
          ++values( my_cypher_3 , cipher_1 )
          ]).

input_clause(clauses_230, axiom,
          [
          --fun_main( nil ),
          ++fun_my_cypher( nil )
          ]).

input_clause(clauses_231, axiom,
          [
          --fun_main( nil ) ,
          --values( my_cypher_return , Z ),
          ++values( x154 , Z )
          ]).

input_clause(clauses_232, axiom,
          [
          --fun_main( nil ),
          ++values( x159 , string )
          ]).

input_clause(clauses_233, axiom,
          [
          --fun_main( nil ) ,
          --values( x159 , Z ),
          ++values( x158 , Z )
          ]).

input_clause(clauses_234, axiom,
          [
          --fun_main( nil ) ,
          --values( x158 , Z ),
          ++values( x157 , Z )
          ]).

input_clause(clauses_235, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x157 )
          ]).

input_clause(clauses_236, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_237, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x156 , Z )
          ]).

input_clause(clauses_238, axiom,
          [
          --fun_main( nil ),
          ++values( x163 , string )
          ]).

input_clause(clauses_239, axiom,
          [
          --fun_main( nil ) ,
          --values( x163 , Z ),
          ++values( x162 , Z )
          ]).

input_clause(clauses_240, axiom,
          [
          --fun_main( nil ) ,
          --values( x162 , Z ),
          ++values( x161 , Z )
          ]).

input_clause(clauses_241, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x161 )
          ]).

input_clause(clauses_242, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_243, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x160 , Z )
          ]).

input_clause(clauses_244, axiom,
          [
          --fun_main( nil ),
          ++values( x165 , address( alice_mess_1 ) )
          ]).

input_clause(clauses_245, axiom,
          [
          --fun_main( nil ),
          ++values( printf_message_1 , x165 )
          ]).

input_clause(clauses_246, axiom,
          [
          --fun_main( nil ),
          ++fun_printf_message( nil )
          ]).

input_clause(clauses_247, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_message_return , Z ),
          ++values( x164 , Z )
          ]).

input_clause(clauses_248, axiom,
          [
          --fun_main( nil ),
          ++values( x169 , string )
          ]).

input_clause(clauses_249, axiom,
          [
          --fun_main( nil ) ,
          --values( x169 , Z ),
          ++values( x168 , Z )
          ]).

input_clause(clauses_250, axiom,
          [
          --fun_main( nil ) ,
          --values( x168 , Z ),
          ++values( x167 , Z )
          ]).

input_clause(clauses_251, axiom,
          [
          --fun_main( nil ) ,
          --values( cipher_1 , Z ),
          ++values( x171 , Z )
          ]).

input_clause(clauses_252, axiom,
          [
          --fun_main( nil ),
          ++values( bBN_bn2hex_1 , x171 )
          ]).

input_clause(clauses_253, axiom,
          [
          --fun_main( nil ),
          ++fun_bBN_bn2hex( nil )
          ]).

input_clause(clauses_254, axiom,
          [
          --fun_main( nil ) ,
          --values( bBN_bn2hex_return , Z ),
          ++values( x170 , Z )
          ]).

input_clause(clauses_255, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x167 )
          ]).

input_clause(clauses_256, axiom,
          [
          --fun_main( nil ),
          ++values( printf_2 , x170 )
          ]).

input_clause(clauses_257, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_258, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x166 , Z )
          ]).

input_clause(clauses_259, axiom,
          [
          --fun_main( nil ),
          ++values( x175 , string )
          ]).

input_clause(clauses_260, axiom,
          [
          --fun_main( nil ) ,
          --values( x175 , Z ),
          ++values( x174 , Z )
          ]).

input_clause(clauses_261, axiom,
          [
          --fun_main( nil ) ,
          --values( x174 , Z ),
          ++values( x173 , Z )
          ]).

input_clause(clauses_262, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x173 )
          ]).

input_clause(clauses_263, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_264, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x172 , Z )
          ]).

input_clause(clauses_265, axiom,
          [
          --fun_main( nil ) ,
          --values( cipher_1 , Z ),
          ++values( x179 , Z )
          ]).

input_clause(clauses_266, axiom,
          [
          --fun_main( nil ),
          ++values( bBN_bn2hex_1 , x179 )
          ]).

input_clause(clauses_267, axiom,
          [
          --fun_main( nil ),
          ++fun_bBN_bn2hex( nil )
          ]).

input_clause(clauses_268, axiom,
          [
          --fun_main( nil ) ,
          --values( bBN_bn2hex_return , Z ),
          ++values( x178 , Z )
          ]).

input_clause(clauses_269, axiom,
          [
          --fun_main( nil ) ,
          --values( x178 , Z ),
          ++values( x177 , Z )
          ]).

input_clause(clauses_270, axiom,
          [
          --fun_main( nil ),
          ++values( x181 , 128 )
          ]).

input_clause(clauses_271, axiom,
          [
          --fun_main( nil ) ,
          --values( x181 , Z ),
          ++values( x180 , Z )
          ]).

input_clause(clauses_272, axiom,
          [
          --fun_main( nil ),
          ++values( write_1 , conn_fd )
          ]).

input_clause(clauses_273, axiom,
          [
          --fun_main( nil ),
          ++values( write_2 , x177 )
          ]).

input_clause(clauses_274, axiom,
          [
          --fun_main( nil ),
          ++values( write_3 , x180 )
          ]).

input_clause(clauses_275, axiom,
          [
          --fun_main( nil ),
          ++fun_write( nil )
          ]).

input_clause(clauses_276, axiom,
          [
          --fun_main( nil ) ,
          --values( write_return , Z ),
          ++values( x176 , Z )
          ]).

input_clause(clauses_277, axiom,
          [
          --fun_main( nil ),
          ++fun_bBN_new( nil )
          ]).

input_clause(clauses_278, axiom,
          [
          --fun_main( nil ) ,
          --values( bBN_new_return , Z ),
          ++values( cipher_2 , Z )
          ]).

input_clause(clauses_279, axiom,
          [
          --fun_main( nil ) ,
          --values( cipher_2 , Z ),
          ++values( x182 , Z )
          ]).

input_clause(clauses_280, axiom,
          [
          --fun_main( nil ),
          ++values( x185 , address( temp ) )
          ]).

input_clause(clauses_281, axiom,
          [
          --fun_main( nil ) ,
          --values( x185 , Z ),
          ++values( x184 , Z )
          ]).

input_clause(clauses_282, axiom,
          [
          --fun_main( nil ),
          ++values( x187 , 128 )
          ]).

input_clause(clauses_283, axiom,
          [
          --fun_main( nil ) ,
          --values( x187 , Z ),
          ++values( x186 , Z )
          ]).

input_clause(clauses_284, axiom,
          [
          --fun_main( nil ),
          ++values( read_1 , conn_fd )
          ]).

input_clause(clauses_285, axiom,
          [
          --fun_main( nil ),
          ++values( read_2 , x184 )
          ]).

input_clause(clauses_286, axiom,
          [
          --fun_main( nil ),
          ++values( read_3 , x186 )
          ]).

input_clause(clauses_287, axiom,
          [
          --fun_main( nil ),
          ++fun_read( nil )
          ]).

input_clause(clauses_288, axiom,
          [
          --fun_main( nil ) ,
          --values( read_return , Z ),
          ++values( x183 , Z )
          ]).

input_clause(clauses_289, axiom,
          [
          --fun_main( nil ),
          ++values( x191 , string )
          ]).

input_clause(clauses_290, axiom,
          [
          --fun_main( nil ) ,
          --values( x191 , Z ),
          ++values( x190 , Z )
          ]).

input_clause(clauses_291, axiom,
          [
          --fun_main( nil ) ,
          --values( x190 , Z ),
          ++values( x189 , Z )
          ]).

input_clause(clauses_292, axiom,
          [
          --fun_main( nil ),
          ++values( x192 , address( temp ) )
          ]).

input_clause(clauses_293, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x189 )
          ]).

input_clause(clauses_294, axiom,
          [
          --fun_main( nil ),
          ++values( printf_2 , x192 )
          ]).

input_clause(clauses_295, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_296, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x188 , Z )
          ]).

input_clause(clauses_297, axiom,
          [
          --fun_main( nil ),
          ++values( x196 , string )
          ]).

input_clause(clauses_298, axiom,
          [
          --fun_main( nil ) ,
          --values( x196 , Z ),
          ++values( x195 , Z )
          ]).

input_clause(clauses_299, axiom,
          [
          --fun_main( nil ) ,
          --values( x195 , Z ),
          ++values( x194 , Z )
          ]).

input_clause(clauses_300, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x194 )
          ]).

input_clause(clauses_301, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_302, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x193 , Z )
          ]).

input_clause(clauses_303, axiom,
          [
          --fun_main( nil ),
          ++values( x198 , address( cipher_2 ) )
          ]).

input_clause(clauses_304, axiom,
          [
          --fun_main( nil ),
          ++values( x201 , address( temp ) )
          ]).

input_clause(clauses_305, axiom,
          [
          --fun_main( nil ) ,
          --values( x201 , Z ),
          ++values( x200 , Z )
          ]).

input_clause(clauses_306, axiom,
          [
          --fun_main( nil ) ,
          --values( x200 , Z ),
          ++values( x199 , Z )
          ]).

input_clause(clauses_307, axiom,
          [
          --fun_main( nil ),
          ++values( bBN_hex2bn_1 , x198 )
          ]).

input_clause(clauses_308, axiom,
          [
          --fun_main( nil ),
          ++values( bBN_hex2bn_2 , x199 )
          ]).

input_clause(clauses_309, axiom,
          [
          --fun_main( nil ),
          ++fun_bBN_hex2bn( nil )
          ]).

input_clause(clauses_310, axiom,
          [
          --fun_main( nil ) ,
          --values( bBN_hex2bn_return , Z ),
          ++values( x197 , Z )
          ]).

input_clause(clauses_311, axiom,
          [
          --fun_main( nil ),
          ++values( x203 , address( alice_mess_2 ) )
          ]).

input_clause(clauses_312, axiom,
          [
          --fun_main( nil ),
          ++values( my_decypher_1 , cipher_2 )
          ]).

input_clause(clauses_313, axiom,
          [
          --fun_main( nil ),
          ++values( my_decypher_2 , alice_key )
          ]).

input_clause(clauses_314, axiom,
          [
          --fun_main( nil ),
          ++values( my_decypher_3 , x203 )
          ]).

input_clause(clauses_315, axiom,
          [
          --fun_main( nil ),
          ++fun_my_decypher( nil )
          ]).

input_clause(clauses_316, axiom,
          [
          --fun_main( nil ) ,
          --values( my_decypher_return , Z ),
          ++values( x202 , Z )
          ]).

input_clause(clauses_317, axiom,
          [
          --fun_main( nil ),
          ++values( x205 , address( alice_mess_2 ) )
          ]).

input_clause(clauses_318, axiom,
          [
          --fun_main( nil ),
          ++values( printf_message_1 , x205 )
          ]).

input_clause(clauses_319, axiom,
          [
          --fun_main( nil ),
          ++fun_printf_message( nil )
          ]).

input_clause(clauses_320, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_message_return , Z ),
          ++values( x204 , Z )
          ]).

input_clause(clauses_321, axiom,
          [
          --fun_main( nil ),
          ++values( x214 , address( alice_mess_2 ) )
          ]).

input_clause(clauses_322, axiom,
          [
          --fun_main( nil ),
          ++values( x213 , address( field( x214 , msg ) ) )
          ]).

input_clause(clauses_323, axiom,
          [
          --fun_main( nil ),
          ++values( x212 , address( field( x213 , msg2 ) ) )
          ]).

input_clause(clauses_324, axiom,
          [
          --fun_main( nil ),
          ++values( x211 , address( field( x212 , nonce1 ) ) )
          ]).

input_clause(clauses_325, axiom,
          [
          --fun_main( nil ) ,
          --values( x211 , Z ),
          ++values( x210 , Z )
          ]).

input_clause(clauses_326, axiom,
          [
          --fun_main( nil ) ,
          --values( x210 , Z ),
          ++values( x209 , Z )
          ]).

input_clause(clauses_327, axiom,
          [
          --fun_main( nil ) ,
          --values( x209 , Z ),
          ++values( x208 , Z )
          ]).

input_clause(clauses_328, axiom,
          [
          --fun_main( nil ),
          ++values( x217 , address( nonceA ) )
          ]).

input_clause(clauses_329, axiom,
          [
          --fun_main( nil ) ,
          --values( x217 , Z ),
          ++values( x216 , Z )
          ]).

input_clause(clauses_330, axiom,
          [
          --fun_main( nil ) ,
          --values( x216 , Z ),
          ++values( x215 , Z )
          ]).

input_clause(clauses_331, axiom,
          [
          --fun_main( nil ),
          ++values( x219 , 16 )
          ]).

input_clause(clauses_332, axiom,
          [
          --fun_main( nil ) ,
          --values( x219 , Z ),
          ++values( x218 , Z )
          ]).

input_clause(clauses_333, axiom,
          [
          --fun_main( nil ),
          ++values( strncmp_1 , x208 )
          ]).

input_clause(clauses_334, axiom,
          [
          --fun_main( nil ),
          ++values( strncmp_2 , x215 )
          ]).

input_clause(clauses_335, axiom,
          [
          --fun_main( nil ),
          ++values( strncmp_3 , x218 )
          ]).

input_clause(clauses_336, axiom,
          [
          --fun_main( nil ),
          ++fun_strncmp( nil )
          ]).

input_clause(clauses_337, axiom,
          [
          --fun_main( nil ) ,
          --values( strncmp_return , Z ),
          ++values( x207 , Z )
          ]).

input_clause(clauses_338, axiom,
          [
          --fun_main( nil ),
          ++values( x220 , 0 )
          ]).

input_clause(clauses_339, axiom,
          [
          --fun_main( nil ),
          ++values( x206 , 1 )
          ]).

input_clause(clauses_340, axiom,
          [
          --fun_main( nil ),
          ++values( x206 , 0 )
          ]).

input_clause(clauses_341, axiom,
          [
          --fun_main( nil ),
          ++values( x224 , string )
          ]).

input_clause(clauses_342, axiom,
          [
          --fun_main( nil ) ,
          --values( x224 , Z ),
          ++values( x223 , Z )
          ]).

input_clause(clauses_343, axiom,
          [
          --fun_main( nil ) ,
          --values( x223 , Z ),
          ++values( x222 , Z )
          ]).

input_clause(clauses_344, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x222 )
          ]).

input_clause(clauses_345, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_346, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x221 , Z )
          ]).

input_clause(clauses_347, axiom,
          [
          --fun_main( nil ),
          ++values( fflush_1 , stdout )
          ]).

input_clause(clauses_348, axiom,
          [
          --fun_main( nil ),
          ++fun_fflush( nil )
          ]).

input_clause(clauses_349, axiom,
          [
          --fun_main( nil ) ,
          --values( fflush_return , Z ),
          ++values( x225 , Z )
          ]).

input_clause(clauses_350, axiom,
          [
          --fun_main( nil ),
          ++values( x229 , string )
          ]).

input_clause(clauses_351, axiom,
          [
          --fun_main( nil ) ,
          --values( x229 , Z ),
          ++values( x228 , Z )
          ]).

input_clause(clauses_352, axiom,
          [
          --fun_main( nil ) ,
          --values( x228 , Z ),
          ++values( x227 , Z )
          ]).

input_clause(clauses_353, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x227 )
          ]).

input_clause(clauses_354, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_355, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x226 , Z )
          ]).

input_clause(clauses_356, axiom,
          [
          --fun_main( nil ),
          ++values( fflush_1 , stdout )
          ]).

input_clause(clauses_357, axiom,
          [
          --fun_main( nil ),
          ++fun_fflush( nil )
          ]).

input_clause(clauses_358, axiom,
          [
          --fun_main( nil ) ,
          --values( fflush_return , Z ),
          ++values( x230 , Z )
          ]).

input_clause(clauses_359, axiom,
          [
          --fun_main( nil ),
          ++values( x232 , 1 )
          ]).

input_clause(clauses_360, axiom,
          [
          --fun_main( nil ),
          ++values( exit_1 , x232 )
          ]).

input_clause(clauses_361, axiom,
          [
          --fun_main( nil ),
          ++fun_exit( nil )
          ]).

input_clause(clauses_362, axiom,
          [
          --fun_main( nil ) ,
          --values( exit_return , Z ),
          ++values( x231 , Z )
          ]).

input_clause(clauses_363, axiom,
          [
          --fun_main( nil ),
          ++values( x235 , address( alice_mess_3 ) )
          ]).

input_clause(clauses_364, axiom,
          [
          --fun_main( nil ),
          ++values( x234 , address( field( x235 , msg_type ) ) )
          ]).

input_clause(clauses_365, axiom,
          [
          --fun_main( nil ),
          ++values( x233 , 3 )
          ]).

input_clause(clauses_366, axiom,
          [
          --fun_main( nil ) ,
          --values( x234 , address( Z ) ) ,
          --values( x233 , Y ),
          ++values( Z , Y )
          ]).

input_clause(clauses_367, axiom,
          [
          --fun_main( nil ),
          ++values( x242 , address( alice_mess_3 ) )
          ]).

input_clause(clauses_368, axiom,
          [
          --fun_main( nil ),
          ++values( x241 , address( field( x242 , msg ) ) )
          ]).

input_clause(clauses_369, axiom,
          [
          --fun_main( nil ),
          ++values( x240 , address( field( x241 , msg3 ) ) )
          ]).

input_clause(clauses_370, axiom,
          [
          --fun_main( nil ),
          ++values( x239 , address( field( x240 , nonce ) ) )
          ]).

input_clause(clauses_371, axiom,
          [
          --fun_main( nil ) ,
          --values( x239 , Z ),
          ++values( x238 , Z )
          ]).

input_clause(clauses_372, axiom,
          [
          --fun_main( nil ) ,
          --values( x238 , Z ),
          ++values( x237 , Z )
          ]).

input_clause(clauses_373, axiom,
          [
          --fun_main( nil ),
          ++values( x248 , address( alice_mess_2 ) )
          ]).

input_clause(clauses_374, axiom,
          [
          --fun_main( nil ),
          ++values( x247 , address( field( x248 , msg ) ) )
          ]).

input_clause(clauses_375, axiom,
          [
          --fun_main( nil ),
          ++values( x246 , address( field( x247 , msg2 ) ) )
          ]).

input_clause(clauses_376, axiom,
          [
          --fun_main( nil ),
          ++values( x245 , address( field( x246 , nonce2 ) ) )
          ]).

input_clause(clauses_377, axiom,
          [
          --fun_main( nil ) ,
          --values( x245 , Z ),
          ++values( x244 , Z )
          ]).

input_clause(clauses_378, axiom,
          [
          --fun_main( nil ) ,
          --values( x244 , Z ),
          ++values( x243 , Z )
          ]).

input_clause(clauses_379, axiom,
          [
          --fun_main( nil ),
          ++values( x250 , 16 )
          ]).

input_clause(clauses_380, axiom,
          [
          --fun_main( nil ) ,
          --values( x250 , Z ),
          ++values( x249 , Z )
          ]).

input_clause(clauses_381, axiom,
          [
          --fun_main( nil ),
          ++values( memcpy_1 , x237 )
          ]).

input_clause(clauses_382, axiom,
          [
          --fun_main( nil ),
          ++values( memcpy_2 , x243 )
          ]).

input_clause(clauses_383, axiom,
          [
          --fun_main( nil ),
          ++values( memcpy_3 , x249 )
          ]).

input_clause(clauses_384, axiom,
          [
          --fun_main( nil ),
          ++fun_memcpy( nil )
          ]).

input_clause(clauses_385, axiom,
          [
          --fun_main( nil ) ,
          --values( memcpy_return , Z ),
          ++values( x236 , Z )
          ]).

input_clause(clauses_386, axiom,
          [
          --fun_main( nil ),
          ++fun_bBN_new( nil )
          ]).

input_clause(clauses_387, axiom,
          [
          --fun_main( nil ) ,
          --values( bBN_new_return , Z ),
          ++values( cipher_3 , Z )
          ]).

input_clause(clauses_388, axiom,
          [
          --fun_main( nil ) ,
          --values( cipher_3 , Z ),
          ++values( x251 , Z )
          ]).

input_clause(clauses_389, axiom,
          [
          --fun_main( nil ),
          ++values( x253 , address( alice_mess_3 ) )
          ]).

input_clause(clauses_390, axiom,
          [
          --fun_main( nil ),
          ++values( my_cypher_1 , x253 )
          ]).

input_clause(clauses_391, axiom,
          [
          --fun_main( nil ),
          ++values( my_cypher_2 , bob_key )
          ]).

input_clause(clauses_392, axiom,
          [
          --fun_main( nil ),
          ++values( my_cypher_3 , cipher_3 )
          ]).

input_clause(clauses_393, axiom,
          [
          --fun_main( nil ),
          ++fun_my_cypher( nil )
          ]).

input_clause(clauses_394, axiom,
          [
          --fun_main( nil ) ,
          --values( my_cypher_return , Z ),
          ++values( x252 , Z )
          ]).

input_clause(clauses_395, axiom,
          [
          --fun_main( nil ),
          ++values( x257 , string )
          ]).

input_clause(clauses_396, axiom,
          [
          --fun_main( nil ) ,
          --values( x257 , Z ),
          ++values( x256 , Z )
          ]).

input_clause(clauses_397, axiom,
          [
          --fun_main( nil ) ,
          --values( x256 , Z ),
          ++values( x255 , Z )
          ]).

input_clause(clauses_398, axiom,
          [
          --fun_main( nil ) ,
          --values( cipher_3 , Z ),
          ++values( x259 , Z )
          ]).

input_clause(clauses_399, axiom,
          [
          --fun_main( nil ),
          ++values( bBN_bn2hex_1 , x259 )
          ]).

input_clause(clauses_400, axiom,
          [
          --fun_main( nil ),
          ++fun_bBN_bn2hex( nil )
          ]).

input_clause(clauses_401, axiom,
          [
          --fun_main( nil ) ,
          --values( bBN_bn2hex_return , Z ),
          ++values( x258 , Z )
          ]).

input_clause(clauses_402, axiom,
          [
          --fun_main( nil ),
          ++values( printf_1 , x255 )
          ]).

input_clause(clauses_403, axiom,
          [
          --fun_main( nil ),
          ++values( printf_2 , x258 )
          ]).

input_clause(clauses_404, axiom,
          [
          --fun_main( nil ),
          ++fun_printf( nil )
          ]).

input_clause(clauses_405, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_return , Z ),
          ++values( x254 , Z )
          ]).

input_clause(clauses_406, axiom,
          [
          --fun_main( nil ),
          ++values( x261 , address( alice_mess_3 ) )
          ]).

input_clause(clauses_407, axiom,
          [
          --fun_main( nil ),
          ++values( printf_message_1 , x261 )
          ]).

input_clause(clauses_408, axiom,
          [
          --fun_main( nil ),
          ++fun_printf_message( nil )
          ]).

input_clause(clauses_409, axiom,
          [
          --fun_main( nil ) ,
          --values( printf_message_return , Z ),
          ++values( x260 , Z )
          ]).

input_clause(clauses_410, axiom,
          [
          --fun_main( nil ) ,
          --values( cipher_3 , Z ),
          ++values( x265 , Z )
          ]).

input_clause(clauses_411, axiom,
          [
          --fun_main( nil ),
          ++values( bBN_bn2hex_1 , x265 )
          ]).

input_clause(clauses_412, axiom,
          [
          --fun_main( nil ),
          ++fun_bBN_bn2hex( nil )
          ]).

input_clause(clauses_413, axiom,
          [
          --fun_main( nil ) ,
          --values( bBN_bn2hex_return , Z ),
          ++values( x264 , Z )
          ]).

input_clause(clauses_414, axiom,
          [
          --fun_main( nil ) ,
          --values( x264 , Z ),
          ++values( x263 , Z )
          ]).

input_clause(clauses_415, axiom,
          [
          --fun_main( nil ),
          ++values( x267 , 128 )
          ]).

input_clause(clauses_416, axiom,
          [
          --fun_main( nil ) ,
          --values( x267 , Z ),
          ++values( x266 , Z )
          ]).

input_clause(clauses_417, axiom,
          [
          --fun_main( nil ),
          ++values( write_1 , conn_fd )
          ]).

input_clause(clauses_418, axiom,
          [
          --fun_main( nil ),
          ++values( write_2 , x263 )
          ]).

input_clause(clauses_419, axiom,
          [
          --fun_main( nil ),
          ++values( write_3 , x266 )
          ]).

input_clause(clauses_420, axiom,
          [
          --fun_main( nil ),
          ++fun_write( nil )
          ]).

input_clause(clauses_421, axiom,
          [
          --fun_main( nil ) ,
          --values( write_return , Z ),
          ++values( x262 , Z )
          ]).

input_clause(clauses_422, axiom,
          [
          --fun_main( nil ),
          ++values( main_return , 0 )
          ]).


% Function = my_cypher
% Params :
%   msg : int 
%   pub_key : int 
%   cipher : int 
% Return = int
% Je renomme msg par my_cypher_1
% Je renomme pub_key par my_cypher_2
% Je renomme cipher par my_cypher_3
% Je renomme msg_len par my_cypher_4
% Je renomme plain par my_cypher_5
% Je renomme ctx par my_cypher_6

input_clause(clauses_423, axiom,
          [
          --fun_my_cypher( nil ) ,
          --values( my_cypher_3 , X ) ,
          --values( my_cypher_1 , address( Y ) ) ,
          --values( my_cypher_2 , PK ),
          ++values( X , encr( Y , PK ) )
          ]).




%
% Ajout des clauses du prototole
%
%

input_clause(protocol_1, axiom,
          [
          ++knows( nil )
          ]).

input_clause(protocol_2, axiom,
          [
          --knows( cons( M1 , M2 ) ),
          ++knows( M1 )
          ]).

input_clause(protocol_3, axiom,
          [
          --knows( cons( M1 , M2 ) ),
          ++knows( M2 )
          ]).

input_clause(protocol_4, axiom,
          [
          --knows( M1 ) ,
          --knows( M2 ),
          ++knows( cons( M1 , M2 ) )
          ]).

input_clause(protocol_5, axiom,
          [
          --knows( M ) ,
          --knows( K ),
          ++knows( crypt( M , K ) )
          ]).

input_clause(protocol_6, axiom,
          [
          --knows( crypt( M , pub( K ) ) ) ,
          --knows( prv( K ) ),
          ++knows( M )
          ]).

input_clause(protocol_7, axiom,
          [
          --knows( crypt( M , prv( K ) ) ) ,
          --knows( pub( K ) ),
          ++knows( M )
          ]).

input_clause(protocol_8, axiom,
          [
          --knows( crypt( M , symkey( A , B ) ) ) ,
          --knows( symkey( A , B ) ),
          ++knows( M )
          ]).

input_clause(protocol_9, axiom,
          [
          --knows( crypt( cons( A , cons( Na , nil ) ) , pub( B ) ) ),
          ++knows( crypt( cons( Na , cons( nonceb( cons( B , cons( A , nil ) ) ) , nil ) ) , pub( A ) ) )
          ]).

input_clause(protocol_10, axiom,
          [
          ++knows( pub( bob ) )
          ]).

input_clause(protocol_11, axiom,
          [
          ++knows( pub( alice ) )
          ]).

input_clause(protocol_12, axiom,
          [
          ++knows( pub( intrus ) )
          ]).

input_clause(protocol_13, axiom,
          [
          ++knows( prv( intrus ) )
          ]).

input_clause(protocol_14, axiom,
          [
          ++agent( alice )
          ]).

input_clause(protocol_15, axiom,
          [
          ++agent( bob )
          ]).

input_clause(protocol_16, axiom,
          [
          ++agent( intrus )
          ]).

input_clause(protocol_17, axiom,
          [
          --values( field( X , N ) , V ) ,
          --values( X , address( Y ) ),
          ++values( field( Y , N ) , V )
          ]).

input_clause(protocol_18, axiom,
          [
          --values( field( X , N ) , V ) ,
          --values( X , address( Z ) ) ,
          --values( Y , address( Z ) ),
          ++values( field( Y , N ) , V )
          ]).

input_clause(protocol_19, axiom,
          [
          --values( K , address( field( X , Y ) ) ) ,
          --values( J , address( field( K , Z ) ) ),
          ++values( J , address( field( field( X , Y ) , Z ) ) )
          ]).

input_clause(protocol_20, axiom,
          [
          --values( J , address( field( field( K , Y ) , Z ) ) ) ,
          --values( K , address( X ) ),
          ++values( J , address( field( field( X , Y ) , Z ) ) )
          ]).

input_clause(protocol_21, axiom,
          [
          --values( Pt , address( offset( Y , Z ) ) ) ,
          --values( Y , address( X ) ),
          ++values( Pt , address( offset( X , Z ) ) )
          ]).

input_clause(protocol_22, axiom,
          [
          --values( Pt , address( offset( X , Y ) ) ) ,
          --values( Y , Z ),
          ++values( Pt , address( offset( X , Z ) ) )
          ]).

input_clause(protocol_23, axiom,
          [
          --values( offset( X , Z ) , V ) ,
          --values( Z , Y ),
          ++values( offset( X , Y ) , V )
          ]).

input_clause(protocol_24, axiom,
          [
          --values( field( field( X2 , Y ) , Z ) , V ) ,
          --values( X2 , address( X1 ) ),
          ++values( field( field( X1 , Y ) , Z ) , V )
          ]).

input_clause(protocol_25, axiom,
          [
          --values( field( field( X2 , Y ) , Z ) , V ) ,
          --values( X1 , address( K ) ) ,
          --values( X2 , address( K ) ),
          ++values( field( field( X1 , Y ) , Z ) , V )
          ]).

input_clause(protocol_26, axiom,
          [
          --values( field( field( field( X2 , Y ) , Z ) , K ) , V ) ,
          --values( X2 , address( X1 ) ),
          ++values( field( field( field( X1 , Y ) , Z ) , K ) , V )
          ]).

input_clause(protocol_27, axiom,
          [
          --values( field( field( field( X2 , Y ) , Z ) , K ) , V ) ,
          --values( X1 , address( K ) ) ,
          --values( X2 , address( K ) ),
          ++values( field( field( field( X1 , Y ) , Z ) , K ) , V )
          ]).

input_clause(protocol_28, axiom,
          [
          --values( X , Z ) ,
          --values( Z , Y ),
          ++values( X , Y )
          ]).

input_clause(protocol_29, axiom,
          [
          --values( field( alice_mess_1 , msg_type ) , 1 ) ,
          --values( field( field( field( alice_mess_1 , msg ) , msg1 ) , id ) , 0 ) ,
          --values( field( field( field( alice_mess_1 , msg ) , msg1 ) , nonce ) , nonceA ),
          ++values( alice_mess_1 , cons( nonceA , cons( alice , nil ) ) )
          ]).

input_clause(protocol_30, axiom,
          [
          --values( alice_mess_1 , cons( nonceA , cons( alice , nil ) ) ) ,
          --values( X , encr( alice_mess_1 , bob_key ) ),
          ++values( X , crypt( cons( noncea( cons( alice , cons( bob , nil ) ) ) , cons( alice , nil ) ) , pub( bob ) ) )
          ]).

input_clause(protocol_31, axiom,
          [
          ++knows( crypt( cons( noncea( cons( alice , cons( bob , nil ) ) ) , cons( nonceb( cons( bob , cons( alice , nil ) ) ) , nil ) ) , pub( alice ) ) )
          ]).

input_clause(protocol_32, axiom,
          [
          --values( X , cons( Y , cons( Z , nil ) ) ),
          ++values( field( field( field( X , msg ) , msg2 ) , nonce1 ) , Y )
          ]).

input_clause(protocol_33, axiom,
          [
          --values( X , cons( Y , cons( Z , nil ) ) ),
          ++values( field( field( field( X , msg ) , msg2 ) , nonce2 ) , Z )
          ]).

input_clause(protocol_34, axiom,
          [
          --values( field( alice_mess_3 , msg_type ) , 3 ) ,
          --values( field( field( field( alice_mess_3 , msg ) , msg3 ) , nonce ) , nonceb( cons( bob , cons( alice , nil ) ) ) ) ,
          --values( X , encr( alice_mess_3 , bob_key ) ),
          ++values( X , crypt( nonceb( cons( bob , cons( alice , nil ) ) ) , pub( bob ) ) )
          ]).

input_clause(protocol_35, axiom,
          [
          ++fun_main( nil )
          ]).

input_clause(clause_conj, conjecture, 
 [
   --knows( crypt( nonceb( cons( bob , cons( alice , nil ) ) ) , pub( bob ) ) )
  ]).

