%------------------------------------------------------------------------------
% File     : SWV005-1 : TPTP v7.2.0. Released v3.2.0.
% Domain   : Software Verification
% Axioms   : Cryptographic protocol axioms for messages
% Version  : [Pau06] axioms.
% English  :

% Refs     : [Pau06] Paulson (2006), Email to G. Sutcliffe
% Source   : [Pau06]
% Names    : Message-simp2.ax [Pau06]

% Status   : Satisfiable
% Syntax   : Number of clauses     :   51 (   9 non-Horn;  19 unit;  30 RR)
%            Number of atoms       :   93 (  21 equality)
%            Maximal clause size   :    3 (   2 average)
%            Number of predicates  :    3 (   0 propositional; 2-3 arity)
%            Number of functors    :   18 (   3 constant; 0-3 arity)
%            Number of variables   :  112 (   6 singleton)
%            Maximal term depth    :    5 (   2 average)
% SPC      : 

% Comments : Requires MSC001-0.ax, MSC001-1.ax, SWV005-0.ax
%------------------------------------------------------------------------------
cnf(cls_Message_OAgent__synth_0,axiom,
    ( c_in(c_Message_Omsg_OAgent(V_A),c_Message_Osynth(V_H),tc_Message_Omsg) )).

cnf(cls_Message_OCrypt__synth_1,axiom,
    ( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(V_X,c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg) )).

cnf(cls_Message_OCrypt__synth__eq_0,axiom,
    ( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg)
    | c_in(c_Message_Omsg_OKey(V_K),V_H,tc_Message_Omsg) )).

cnf(cls_Message_OCrypt__synth__eq_1,axiom,
    ( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg)
    | c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(c_Message_Omsg_OKey(V_K),V_H,tc_Message_Omsg) )).

cnf(cls_Message_OHash__synth_0,axiom,
    ( ~ c_in(c_Message_Omsg_OHash(V_X),c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(V_X,c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(c_Message_Omsg_OHash(V_X),V_H,tc_Message_Omsg) )).

cnf(cls_Message_OKey__synth__eq_0,axiom,
    ( ~ c_in(c_Message_Omsg_OKey(V_K),c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(c_Message_Omsg_OKey(V_K),V_H,tc_Message_Omsg) )).

cnf(cls_Message_OKey__synth__eq_1,axiom,
    ( ~ c_in(c_Message_Omsg_OKey(V_K),V_H,tc_Message_Omsg)
    | c_in(c_Message_Omsg_OKey(V_K),c_Message_Osynth(V_H),tc_Message_Omsg) )).

cnf(cls_Message_OMPair__analz_0,axiom,
    ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg)
    | c_in(V_Y,c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_OMPair__analz_1,axiom,
    ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(V_H),tc_Message_Omsg)
    | c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_OMPair__synth_0,axiom,
    ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(V_Y,c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(c_Message_Omsg_OMPair(V_X,V_Y),V_H,tc_Message_Omsg) )).

cnf(cls_Message_OMPair__synth_1,axiom,
    ( ~ c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(V_X,c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(c_Message_Omsg_OMPair(V_X,V_Y),V_H,tc_Message_Omsg) )).

cnf(cls_Message_ONonce__synth__eq_0,axiom,
    ( ~ c_in(c_Message_Omsg_ONonce(V_N),c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(c_Message_Omsg_ONonce(V_N),V_H,tc_Message_Omsg) )).

cnf(cls_Message_ONonce__synth__eq_1,axiom,
    ( ~ c_in(c_Message_Omsg_ONonce(V_N),V_H,tc_Message_Omsg)
    | c_in(c_Message_Omsg_ONonce(V_N),c_Message_Osynth(V_H),tc_Message_Omsg) )).

cnf(cls_Message_ONumber__synth_0,axiom,
    ( c_in(c_Message_Omsg_ONumber(V_n),c_Message_Osynth(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz_ODecrypt__dest_0,axiom,
    ( ~ c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oanalz(V_H),tc_Message_Omsg)
    | ~ c_in(c_Message_Omsg_OKey(c_Message_OinvKey(V_K)),c_Message_Oanalz(V_H),tc_Message_Omsg)
    | c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz_OInj_0,axiom,
    ( ~ c_in(V_X,V_H,tc_Message_Omsg)
    | c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz__Crypt__if_0,axiom,
    ( ~ c_in(c_Message_Omsg_OKey(c_Message_OinvKey(V_K)),c_Message_Oanalz(V_H),tc_Message_Omsg)
    | c_Message_Oanalz(c_insert(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oanalz(c_insert(V_X,V_H,tc_Message_Omsg)),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz__Crypt__if_1,axiom,
    ( c_in(c_Message_Omsg_OKey(c_Message_OinvKey(V_K)),c_Message_Oanalz(V_H),tc_Message_Omsg)
    | c_Message_Oanalz(c_insert(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz__analzD__dest_0,axiom,
    ( ~ c_in(V_X,c_Message_Oanalz(c_Message_Oanalz(V_H)),tc_Message_Omsg)
    | c_in(V_X,c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz__empty_0,axiom,
    ( c_Message_Oanalz(c_emptyset) = c_emptyset )).

cnf(cls_Message_Oanalz__idem_0,axiom,
    ( c_Message_Oanalz(c_Message_Oanalz(V_H)) = c_Message_Oanalz(V_H) )).

cnf(cls_Message_Oanalz__insert__Agent_0,axiom,
    ( c_Message_Oanalz(c_insert(c_Message_Omsg_OAgent(V_agt),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OAgent(V_agt),c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz__insert__Hash_0,axiom,
    ( c_Message_Oanalz(c_insert(c_Message_Omsg_OHash(V_X),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OHash(V_X),c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz__insert__Key_0,axiom,
    ( c_in(V_K,c_Message_OkeysFor(c_Message_Oanalz(V_H)),tc_nat)
    | c_Message_Oanalz(c_insert(c_Message_Omsg_OKey(V_K),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OKey(V_K),c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz__insert__MPair_0,axiom,
    ( c_Message_Oanalz(c_insert(c_Message_Omsg_OMPair(V_X,V_Y),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oanalz(c_insert(V_X,c_insert(V_Y,V_H,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz__insert__Nonce_0,axiom,
    ( c_Message_Oanalz(c_insert(c_Message_Omsg_ONonce(V_N),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_ONonce(V_N),c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz__insert__Number_0,axiom,
    ( c_Message_Oanalz(c_insert(c_Message_Omsg_ONumber(V_N),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_ONumber(V_N),c_Message_Oanalz(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oanalz__parts_0,axiom,
    ( c_Message_Oanalz(c_Message_Oparts(V_H)) = c_Message_Oparts(V_H) )).

cnf(cls_Message_Oanalz__subset__iff_0,axiom,
    ( ~ c_lessequals(c_Message_Oanalz(V_G),c_Message_Oanalz(V_H),tc_set(tc_Message_Omsg))
    | c_lessequals(V_G,c_Message_Oanalz(V_H),tc_set(tc_Message_Omsg)) )).

cnf(cls_Message_Oanalz__subset__iff_1,axiom,
    ( ~ c_lessequals(V_G,c_Message_Oanalz(V_H),tc_set(tc_Message_Omsg))
    | c_lessequals(c_Message_Oanalz(V_G),c_Message_Oanalz(V_H),tc_set(tc_Message_Omsg)) )).

cnf(cls_Message_Oin__parts__UnE_0,axiom,
    ( ~ c_in(V_c,c_Message_Oparts(c_union(V_G,V_H,tc_Message_Omsg)),tc_Message_Omsg)
    | c_in(V_c,c_Message_Oparts(V_H),tc_Message_Omsg)
    | c_in(V_c,c_Message_Oparts(V_G),tc_Message_Omsg) )).

cnf(cls_Message_Oparts__analz_0,axiom,
    ( c_Message_Oparts(c_Message_Oanalz(V_H)) = c_Message_Oparts(V_H) )).

cnf(cls_Message_Oparts__cut__eq_0,axiom,
    ( ~ c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg)
    | c_Message_Oparts(c_insert(V_X,V_H,tc_Message_Omsg)) = c_Message_Oparts(V_H) )).

cnf(cls_Message_Oparts__idem_0,axiom,
    ( c_Message_Oparts(c_Message_Oparts(V_H)) = c_Message_Oparts(V_H) )).

cnf(cls_Message_Oparts__insert__Agent_0,axiom,
    ( c_Message_Oparts(c_insert(c_Message_Omsg_OAgent(V_agt),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OAgent(V_agt),c_Message_Oparts(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oparts__insert__Crypt_0,axiom,
    ( c_Message_Oparts(c_insert(c_Message_Omsg_OCrypt(V_K,V_X),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Oparts(c_insert(V_X,V_H,tc_Message_Omsg)),tc_Message_Omsg) )).

cnf(cls_Message_Oparts__insert__Hash_0,axiom,
    ( c_Message_Oparts(c_insert(c_Message_Omsg_OHash(V_X),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OHash(V_X),c_Message_Oparts(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oparts__insert__Key_0,axiom,
    ( c_Message_Oparts(c_insert(c_Message_Omsg_OKey(V_K),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OKey(V_K),c_Message_Oparts(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oparts__insert__MPair_0,axiom,
    ( c_Message_Oparts(c_insert(c_Message_Omsg_OMPair(V_X,V_Y),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Oparts(c_insert(V_X,c_insert(V_Y,V_H,tc_Message_Omsg),tc_Message_Omsg)),tc_Message_Omsg) )).

cnf(cls_Message_Oparts__insert__Nonce_0,axiom,
    ( c_Message_Oparts(c_insert(c_Message_Omsg_ONonce(V_N),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_ONonce(V_N),c_Message_Oparts(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oparts__insert__Number_0,axiom,
    ( c_Message_Oparts(c_insert(c_Message_Omsg_ONumber(V_N),V_H,tc_Message_Omsg)) = c_insert(c_Message_Omsg_ONumber(V_N),c_Message_Oparts(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oparts__partsD__dest_0,axiom,
    ( ~ c_in(V_X,c_Message_Oparts(c_Message_Oparts(V_H)),tc_Message_Omsg)
    | c_in(V_X,c_Message_Oparts(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Oparts__subset__iff_0,axiom,
    ( ~ c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))
    | c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) )).

cnf(cls_Message_Oparts__subset__iff_1,axiom,
    ( ~ c_lessequals(V_G,c_Message_Oparts(V_H),tc_set(tc_Message_Omsg))
    | c_lessequals(c_Message_Oparts(V_G),c_Message_Oparts(V_H),tc_set(tc_Message_Omsg)) )).

cnf(cls_Message_Osynth_OCrypt_0,axiom,
    ( ~ c_in(V_X,c_Message_Osynth(V_H),tc_Message_Omsg)
    | ~ c_in(c_Message_Omsg_OKey(V_K),V_H,tc_Message_Omsg)
    | c_in(c_Message_Omsg_OCrypt(V_K,V_X),c_Message_Osynth(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Osynth_OHash_0,axiom,
    ( ~ c_in(V_X,c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(c_Message_Omsg_OHash(V_X),c_Message_Osynth(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Osynth_OInj_0,axiom,
    ( ~ c_in(V_X,V_H,tc_Message_Omsg)
    | c_in(V_X,c_Message_Osynth(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Osynth_OMPair_0,axiom,
    ( ~ c_in(V_Y,c_Message_Osynth(V_H),tc_Message_Omsg)
    | ~ c_in(V_X,c_Message_Osynth(V_H),tc_Message_Omsg)
    | c_in(c_Message_Omsg_OMPair(V_X,V_Y),c_Message_Osynth(V_H),tc_Message_Omsg) )).

cnf(cls_Message_Osynth__subset__iff_0,axiom,
    ( ~ c_lessequals(c_Message_Osynth(V_G),c_Message_Osynth(V_H),tc_set(tc_Message_Omsg))
    | c_lessequals(V_G,c_Message_Osynth(V_H),tc_set(tc_Message_Omsg)) )).

cnf(cls_Message_Osynth__subset__iff_1,axiom,
    ( ~ c_lessequals(V_G,c_Message_Osynth(V_H),tc_set(tc_Message_Omsg))
    | c_lessequals(c_Message_Osynth(V_G),c_Message_Osynth(V_H),tc_set(tc_Message_Omsg)) )).

cnf(cls_Message_Osynth__synthD__dest_0,axiom,
    ( ~ c_in(V_X,c_Message_Osynth(c_Message_Osynth(V_H)),tc_Message_Omsg)
    | c_in(V_X,c_Message_Osynth(V_H),tc_Message_Omsg) )).

%------------------------------------------------------------------------------