%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] Gamma_1: (extend-no-conflict) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] Gamma_2: (extend-no-conflict) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] 2: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [c_in( c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)], ~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))) Gamma_3: (extend-no-conflict) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] 2: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [c_in( c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)], ~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))) 3: ~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)), [c_in( c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] Gamma_4: (extend-conflict) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] 2: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [c_in( c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)], ~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))) 3: ~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)), [c_in( c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 4: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_5: (move) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] 2: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [c_in( c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)], ~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))) 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 4: ~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)), [c_in( c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] Gamma_6: (resolve) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] 2: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [c_in( c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)], ~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))) 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 4: [~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_7: (extend-conflict) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] 2: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [c_in( c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)], ~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))) 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 4: [~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_8: (move) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] 2: [~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [c_in( c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)], ~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))) 4: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_9: (resolve) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] 2: [~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: [~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent))], ~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))) 4: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_10: (extend-conflict) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] 2: [~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)))] 4: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_11: (move) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)))] 2: [c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent))] 3: [~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 4: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_12: (resolve) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)))] 2: [~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent))] 3: [~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 4: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_13: (extend-conflict) 0: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 1: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)))] 2: [~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent))] 3: [~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 4: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_14: (move) 0: [~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent))] 1: [c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))), c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)] 2: ~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent)), [~( c_in(v_evs2,c_Yahalom_Oyahalom,tc_List_Olist(tc_Event_Oevent)))] 3: [~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 4: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_15: (resolve) 0: [~(c_in(c_Event_Oevent_OGets(v_Ba,c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB))),c_List_Oset(v_evs2,tc_Event_Oevent),tc_Event_Oevent))] 1: [] 2: [~(c_in(c_Message_Omsg_OMPair(c_Message_Omsg_OAgent(v_Aa),c_Message_Omsg_ONonce(v_NB)),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] SZS status Unsatisfiable