(PROVE '(ALL
	      ((?receivingR :SORT Action)
	       (?sendingC :SORT Action)
	       (?m :SORT Term)
	       (?agentB :SORT Agent)
	       (?n :SORT Term))
	      (IMPLIES (AND (nonce? ?n)
			    (nonce? ?m))
		       (IMPLIES (AND
				 (NOT
				  (EXISTS
				   ((?sillysending
				     :SORT
				     Action))
				   (sendIn
				    ?sillysending
				    (creator ?m)
				    (hashResponse
				     (creator ?m)
				     ?agentB
				     ?m))))
				 (AND
				  (minSendIn
				   ?sendingC
				   (creator ?m)
				   (identityChallenge
				    (creator ?m)
				    ?agentB
				    ?m))
				  (AND
				   (receiveIn
				    ?receivingR
				    (creator ?m)
				    (hashResponse
				     (creator ?m)
				     ?agentB
				     ?m))
				   (AND
				    (precedes
				     ?sendingC
				     ?receivingR)
				    (NOT
				     (=
				      ?agentB
				      (creator
				       ?m)))))))
				(EXISTS
				 ((?receivingC
				   :SORT
				   Action)
				  (?sendingR
				   :SORT
				   Action))
				 (AND
				  (receiveIn
				   ?receivingC
				   ?agentB
				   (identityChallenge
				    (creator ?m)
				    ?agentB
				    ?m))
				  (AND
				   (minSendIn
				    ?sendingR
				    ?agentB
				    (hashResponse
				     (creator ?m)
				     ?agentB
				     ?m))
				   (AND
				    (precedes
				     ?sendingC
				     ?receivingC)
				    (AND
				     (precedes
				      ?receivingC
				      ?sendingR)
				     (precedes
				      ?sendingR
				      ?receivingR)))))))))
	    :NAME :ChallengeResponse)



(Refutation
 (Row :ThmSendInIsMonotonic
      (or (not (sendIn ?Action ?Agent ?Term))
	  (not (inside ?Term1 ?Term))
	  (sendIn ?Action ?Agent ?Term1))
      assertion)
 (Row :ThmReceiveInIsMonotonic
      (or (not (receiveIn ?Action ?Agent ?Term))
	  (not (inside ?Term1 ?Term))
	  (receiveIn ?Action ?Agent ?Term1))
      assertion)
 (Row :DefinitionOfMinSendIn
      (or (not (minSendIn ?Action ?Agent ?Term))
	  (sendIn ?Action ?Agent ?Term))
      assertion)
 (Row :DefinitionOfMinSendIn
      (or (not (minSendIn ?Action ?Agent ?Term))
	  (not (sendIn ?Action1 ?Agent1 ?Term))
	  (not (precedes ?Action1 ?Action)))
      assertion)
 (Row :ThmReceivingPrecededByMinimalSending
      (or (not (receiveIn ?Action ?Agent ?Term))
	  (minSendIn
	   (sending-7 ?Term ?Action)
	   (sender-8 ?Term ?Action) ?Term))
      assertion)
 (Row :ThmReceivingPrecededByMinimalSending
      (or (not (receiveIn ?Action ?Agent ?Term))
	  (precedes
	   (sending-7 ?Term ?Action) ?Action))
      assertion)
 (Row :DefinitionOfFirstSendIn
      (or (not (firstSendIn ?Action ?Agent ?Term))
	  (sendIn ?Action ?Agent ?Term))
      assertion)
 (Row :DefinitionOfFirstSendIn
      (or (not (firstSendIn ?Action ?Agent ?Term))
	  (not (sendIn ?Action1 ?Agent1 ?Term))
	  (precedes ?Action ?Action1) (= ?Action ?Action1))
      assertion)
 (Row :ThmFirstSendInPrecedesReceiveIn
      (or (not (firstSendIn ?Action ?Agent ?Term))
	  (not (receiveIn ?Action1 ?Agent1 ?Term))
	  (precedes ?Action ?Action1))
      assertion)
 (Row :NonceOtherSending
      (or (not (nonce? ?Term)) (= ?Agent (creator ?Term))
	  (not (sendIn ?Action ?Agent ?Term))
	  (receiveIn
	   (receiving-11 ?Agent ?Term ?Action)
	   ?Agent ?Term))
      assertion)
 (Row :NonceOtherSending
      (or (not (nonce? ?Term)) (= ?Agent (creator ?Term))
	  (not (sendIn ?Action ?Agent ?Term))
	  (precedes
	   (receiving-11 ?Agent ?Term ?Action)
	   ?Action))
      assertion)
 (Row :ThmNonceFirstSendPrecedesReceiving
      (or (not (nonce? ?Term))
	  (not (receiveIn ?Action ?Agent ?Term))
	  (firstSendIn
	   (sending-12 ?Term ?Action)
	   (creator ?Term) ?Term))
      assertion)
 (Row :SenderOfHash
      (or (not (minSendIn ?Action ?Agent
			  (hash ?Agent1 ?Agent2 ?Term)))
	  (= ?Agent ?Agent1) (= ?Agent ?Agent2))
      assertion)
 (Row :HashContainsTerm
      (inside ?Term (hash ?Agent ?Agent1 ?Term))
      assertion)
 (Row :DefinitionOfIdentityChallenge
      (= (identityChallenge ?Agent ?Agent1 ?Term) ?Term)
      assertion)
 (Row :DefinitionOfHashResponse
      (= (hashResponse ?Agent ?Agent1 ?Term)
	 (hash ?Agent1 ?Agent ?Term))
      assertion)
 (Row :ChallengeResponse
      (nonce? m)
      ~conclusion)
 (Row :ChallengeResponse
      (not (sendIn ?Action
		   (creator m)
		   (hash agentB
			 (creator m)
			 m)))
      (rewrite ~conclusion :DefinitionOfHashResponse))
 (Row :ChallengeResponse
      (minSendIn sendingC
		 (creator m)
		 m)
      (rewrite ~conclusion :DefinitionOfIdentityChallenge))
 (Row :ChallengeResponse
      (receiveIn receivingR
		 (creator m)
		 (hash agentB
		       (creator m)
		       m))
      (rewrite ~conclusion :DefinitionOfHashResponse))
 (Row :ChallengeResponse
      (not (= agentB
	      (creator m)))
      ~conclusion)
 (Row :ChallengeResponse
      (or (not (receiveIn ?Action agentB
			  m))
	  (not (minSendIn ?Action1 agentB
			  (hash agentB
				(creator m)
				m)))
	  (not (precedes sendingC ?Action))
	  (not (precedes ?Action ?Action1))
	  (not (precedes ?Action1
			 receivingR)))
      (rewrite ~conclusion :DefinitionOfIdentityChallenge :DefinitionOfHashResponse))
 (Row 90
      (sendIn sendingC
	      (creator m)
	      m)
      (hyperresolve :DefinitionOfMinSendIn :ChallengeResponse))
 (Row 94
      (precedes
       (sending-7
	(hash agentB
	      (creator m)
	      m)
	receivingR)
       receivingR)
      (hyperresolve :ThmReceivingPrecededByMinimalSending :ChallengeResponse))
 (Row 101
      (receiveIn receivingR
		 (creator m)
		 m)
      (hyperresolve :ThmReceiveInIsMonotonic :ChallengeResponse :HashContainsTerm))
 (Row 104
      (minSendIn
       (sending-7
	(hash agentB
	      (creator m)
	      m)
	receivingR)
       (sender-8
	(hash agentB
	      (creator m)
	      m)
	receivingR)
       (hash agentB
	     (creator m)
	     m))
      (hyperresolve :ThmReceivingPrecededByMinimalSending :ChallengeResponse))
 (Row 130
      (firstSendIn
       (sending-12 m
		   receivingR)
       (creator m)
       m)
      (hyperresolve :ThmNonceFirstSendPrecedesReceiving 101 :ChallengeResponse))
 (Row 148
      (sendIn
       (sending-12 m
		   receivingR)
       (creator m)
       m)
      (hyperresolve :DefinitionOfFirstSendIn 130))
 (Row 149
      (or (precedes
	   (sending-12 m
		       receivingR)
	   sendingC)
	  (= (sending-12
	      m
	      receivingR)
	     sendingC))
      (hyperresolve :DefinitionOfFirstSendIn 130 90))
 (Row 257
      (= (sending-12 m
		     receivingR)
	 sendingC)
      (hyperresolve :DefinitionOfMinSendIn 149 :ChallengeResponse 148))
 (Row 258
      (firstSendIn sendingC
		   (creator m)
		   m)
      (rewrite 130 257))
 (Row 813
      (sendIn
       (sending-7
	(hash agentB
	      (creator m)
	      m)
	receivingR)
       (sender-8
	(hash agentB
	      (creator m)
	      m)
	receivingR)
       (hash agentB
	     (creator m)
	     m))
      (hyperresolve :DefinitionOfMinSendIn 104))
 (Row 814
      (or (= (sender-8
	      (hash agentB
		    (creator m)
		    m)
	      receivingR)
	     agentB)
	  (= (sender-8
	      (hash agentB
		    (creator m)
		    m)
	      receivingR)
	     (creator m)))
      (hyperresolve :SenderOfHash 104))
 (Row 925
      (sendIn
       (sending-7
	(hash agentB
	      (creator m)
	      m)
	receivingR)
       (sender-8
	(hash agentB
	      (creator m)
	      m)
	receivingR)
       m)
      (hyperresolve :ThmSendInIsMonotonic 813 :HashContainsTerm))
 (Row 939
      (or (= (sender-8
	      (hash agentB
		    (creator m)
		    m)
	      receivingR)
	     (creator m))
	  (precedes
	   (receiving-11
	    (sender-8
	     (hash agentB
		   (creator m)
		   m)
	     receivingR)
	    m
	    (sending-7
	     (hash agentB
		   (creator m)
		   m)
	     receivingR))
	   (sending-7
	    (hash agentB
		  (creator m)
		  m)
	    receivingR)))
      (hyperresolve :NonceOtherSending 925 :ChallengeResponse))
 (Row 940
      (or (= (sender-8
	      (hash agentB
		    (creator m)
		    m)
	      receivingR)
	     (creator m))
	  (receiveIn
	   (receiving-11
	    (sender-8
	     (hash agentB
		   (creator m)
		   m)
	     receivingR)
	    m
	    (sending-7
	     (hash agentB
		   (creator m)
		   m)
	     receivingR))
	   (sender-8
	    (hash agentB
		  (creator m)
		  m)
	    receivingR)
	   m))
      (hyperresolve :NonceOtherSending 925 :ChallengeResponse))
 (Row 1732
      (= (sender-8
	  (hash agentB
		(creator m)
		m)
	  receivingR)
	 agentB)
      (rewrite (paramodulate 813 814) :ChallengeResponse))
 (Row 1733
      (minSendIn
       (sending-7
	(hash agentB
	      (creator m)
	      m)
	receivingR)
       agentB
       (hash agentB
	     (creator m)
	     m))
      (rewrite 104 1732))
 (Row 1747
      (precedes
       (receiving-11 agentB
		     m
		     (sending-7
		      (hash agentB
			    (creator m)
			    m)
		      receivingR))
       (sending-7
	(hash agentB
	      (creator m)
	      m)
	receivingR))
      (rewrite 939 1732 :ChallengeResponse))
 (Row 1748
      (receiveIn
       (receiving-11 agentB
		     m
		     (sending-7
		      (hash agentB
			    (creator m)
			    m)
		      receivingR))
       agentB m)
      (rewrite 940 1732 :ChallengeResponse))
 (Row 1807
      (precedes sendingC
		(receiving-11 agentB
			      m
			      (sending-7
			       (hash agentB
				     (creator m)
				     m)
			       receivingR)))
      (hyperresolve :ThmFirstSendInPrecedesReceiveIn 1748 258))
 (Row 1891
      false
      (hyperresolve :ChallengeResponse 1747 1748 1733 1807 94))
 )