Input || R0 || (EXISTS p_AskPermission_1: AskPermission. (p_AskPermission_1_presence & EXISTS p_Measure_476: Measure. (p_Measure_476_presence & (p_AskPermission_1_time = p_Measure_476_time))) & ((EXISTS p_RobotMoving_414: RobotMoving. (p_RobotMoving_414_presence & ((p_RobotMoving_414_time = 1) & (p_RobotMoving_414_presence <-> RobotMoving_15_presence))) & EXISTS p_InformHuman_149: InformHuman. (p_InformHuman_149_presence & ((p_InformHuman_149_time = 0) & (p_InformHuman_149_presence <-> InformHuman_7_presence))) & EXISTS p_AskPermission_70: AskPermission. (p_AskPermission_70_presence & ((p_AskPermission_70_time = 0) & (p_AskPermission_70_presence <-> AskPermission_2_presence))) & EXISTS p_Measure_475: Measure. (p_Measure_475_presence & ((p_Measure_475_time = 0) & (p_Measure_475_humanInRoute <-> False) & (p_Measure_475_humanInRange <-> False) & (p_Measure_475_bumpHuman <-> False) & (p_Measure_475_humanTooClose <-> False) & (p_Measure_475_routeAvailable <-> True) & (p_Measure_475_humanReEnables <-> False) & (p_Measure_475_risk = 0) & (p_Measure_475_efficiency = 0) & (p_Measure_475_isHumanTask <-> False) & (p_Measure_475_humanConsents <-> False) & (p_Measure_475_accident <-> False) & (p_Measure_475_humansPresent <-> False) & (p_Measure_475_obstaclePresent <-> False) & (p_Measure_475_presence <-> Measure_37_presence))) & EXISTS p_blocked_not_RobotMoving_32: blocked_not_RobotMoving. (p_blocked_not_RobotMoving_32_presence & ((p_blocked_not_RobotMoving_32_time = 0) & (p_blocked_not_RobotMoving_32_end = 0) & (p_blocked_not_RobotMoving_32_presence <-> blocked_not_RobotMoving_1_presence)))) & Forall p_Measure_0: Measure. ( (! p_Measure_0_presence) | Forall p_Measure_477: Measure. ( (! p_Measure_477_presence) | ((! (p_Measure_0_time = p_Measure_477_time)) | ((p_Measure_0_time = p_Measure_477_time) & (p_Measure_0_humanInRoute <-> p_Measure_477_humanInRoute) & (p_Measure_0_humanInRange <-> p_Measure_477_humanInRange) & (p_Measure_0_bumpHuman <-> p_Measure_477_bumpHuman) & (p_Measure_0_humanTooClose <-> p_Measure_477_humanTooClose) & (p_Measure_0_routeAvailable <-> p_Measure_477_routeAvailable) & (p_Measure_0_humanReEnables <-> p_Measure_477_humanReEnables) & (p_Measure_0_risk = p_Measure_477_risk) & (p_Measure_0_efficiency = p_Measure_477_efficiency) & (p_Measure_0_isHumanTask <-> p_Measure_477_isHumanTask) & (p_Measure_0_humanConsents <-> p_Measure_477_humanConsents) & (p_Measure_0_accident <-> p_Measure_477_accident) & (p_Measure_0_humansPresent <-> p_Measure_477_humansPresent) & (p_Measure_0_obstaclePresent <-> p_Measure_477_obstaclePresent) & (p_Measure_0_presence <-> p_Measure_477_presence)))))))
Def || L1 || c0 <-> (EXISTS p_AskPermission_1: AskPermission. (p_AskPermission_1_presence & EXISTS p_Measure_476: Measure. (p_Measure_476_presence & (p_AskPermission_1_time = p_Measure_476_time))) & ((EXISTS p_RobotMoving_414: RobotMoving. (p_RobotMoving_414_presence & ((p_RobotMoving_414_time = 1) & (p_RobotMoving_414_presence <-> RobotMoving_15_presence))) & EXISTS p_InformHuman_149: InformHuman. (p_InformHuman_149_presence & ((p_InformHuman_149_time = 0) & (p_InformHuman_149_presence <-> InformHuman_7_presence))) & EXISTS p_AskPermission_70: AskPermission. (p_AskPermission_70_presence & ((p_AskPermission_70_time = 0) & (p_AskPermission_70_presence <-> AskPermission_2_presence))) & EXISTS p_Measure_475: Measure. (p_Measure_475_presence & ((p_Measure_475_time = 0) & (p_Measure_475_humanInRoute <-> False) & (p_Measure_475_humanInRange <-> False) & (p_Measure_475_bumpHuman <-> False) & (p_Measure_475_humanTooClose <-> False) & (p_Measure_475_routeAvailable <-> True) & (p_Measure_475_humanReEnables <-> False) & (p_Measure_475_risk = 0) & (p_Measure_475_efficiency = 0) & (p_Measure_475_isHumanTask <-> False) & (p_Measure_475_humanConsents <-> False) & (p_Measure_475_accident <-> False) & (p_Measure_475_humansPresent <-> False) & (p_Measure_475_obstaclePresent <-> False) & (p_Measure_475_presence <-> Measure_37_presence))) & EXISTS p_blocked_not_RobotMoving_32: blocked_not_RobotMoving. (p_blocked_not_RobotMoving_32_presence & ((p_blocked_not_RobotMoving_32_time = 0) & (p_blocked_not_RobotMoving_32_end = 0) & (p_blocked_not_RobotMoving_32_presence <-> blocked_not_RobotMoving_1_presence)))) & Forall p_Measure_0: Measure. ( (! p_Measure_0_presence) | Forall p_Measure_477: Measure. ( (! p_Measure_477_presence) | ((! (p_Measure_0_time = p_Measure_477_time)) | ((p_Measure_0_time = p_Measure_477_time) & (p_Measure_0_humanInRoute <-> p_Measure_477_humanInRoute) & (p_Measure_0_humanInRange <-> p_Measure_477_humanInRange) & (p_Measure_0_bumpHuman <-> p_Measure_477_bumpHuman) & (p_Measure_0_humanTooClose <-> p_Measure_477_humanTooClose) & (p_Measure_0_routeAvailable <-> p_Measure_477_routeAvailable) & (p_Measure_0_humanReEnables <-> p_Measure_477_humanReEnables) & (p_Measure_0_risk = p_Measure_477_risk) & (p_Measure_0_efficiency = p_Measure_477_efficiency) & (p_Measure_0_isHumanTask <-> p_Measure_477_isHumanTask) & (p_Measure_0_humanConsents <-> p_Measure_477_humanConsents) & (p_Measure_0_accident <-> p_Measure_477_accident) & (p_Measure_0_humansPresent <-> p_Measure_477_humansPresent) & (p_Measure_0_obstaclePresent <-> p_Measure_477_obstaclePresent) & (p_Measure_0_presence <-> p_Measure_477_presence)))))))
DeriveFact || F0 || c0 || L1 R0
Input || R7 || Forall p_InformHuman_0: InformHuman. ( (! p_InformHuman_0_presence) | EXISTS p_Measure_484: Measure. (p_Measure_484_presence & ((p_InformHuman_0_time = p_Measure_484_time) & (((! (True & (! p_Measure_484_routeAvailable))) | EXISTS p_AskPermission_71: AskPermission. (p_AskPermission_71_presence & ((p_AskPermission_71_time <= (p_InformHuman_0_time + 0)) & ((p_InformHuman_0_time + 0) <= p_AskPermission_71_time)))) & ((! ((True & p_Measure_484_routeAvailable) & p_Measure_484_humanInRoute)) | EXISTS p_AdjustRoute_115: AdjustRoute. (p_AdjustRoute_115_presence & ((p_AdjustRoute_115_time <= (p_InformHuman_0_time + 0)) & ((p_InformHuman_0_time + 0) <= p_AdjustRoute_115_time)))) & ((! (((True & p_Measure_484_routeAvailable) & (! p_Measure_484_humanInRoute)) & True)) | EXISTS p_RobotMoving_415: RobotMoving. (p_RobotMoving_415_presence & ((p_RobotMoving_415_time <= (p_InformHuman_0_time + 0)) & ((p_InformHuman_0_time + 0) <= p_RobotMoving_415_time))))))))
Def || L15 || c7 <-> Forall p_InformHuman_0: InformHuman. ( (! p_InformHuman_0_presence) | EXISTS p_Measure_484: Measure. (p_Measure_484_presence & ((p_InformHuman_0_time = p_Measure_484_time) & (((! (True & (! p_Measure_484_routeAvailable))) | EXISTS p_AskPermission_71: AskPermission. (p_AskPermission_71_presence & ((p_AskPermission_71_time <= (p_InformHuman_0_time + 0)) & ((p_InformHuman_0_time + 0) <= p_AskPermission_71_time)))) & ((! ((True & p_Measure_484_routeAvailable) & p_Measure_484_humanInRoute)) | EXISTS p_AdjustRoute_115: AdjustRoute. (p_AdjustRoute_115_presence & ((p_AdjustRoute_115_time <= (p_InformHuman_0_time + 0)) & ((p_InformHuman_0_time + 0) <= p_AdjustRoute_115_time)))) & ((! (((True & p_Measure_484_routeAvailable) & (! p_Measure_484_humanInRoute)) & True)) | EXISTS p_RobotMoving_415: RobotMoving. (p_RobotMoving_415_presence & ((p_RobotMoving_415_time <= (p_InformHuman_0_time + 0)) & ((p_InformHuman_0_time + 0) <= p_RobotMoving_415_time))))))))
DeriveFact || F7 || c7 || L15 R7
Input || R24 || Forall p_AskPermission_0: AskPermission. ( (! p_AskPermission_0_presence) | EXISTS p_Measure_501: Measure. (p_Measure_501_presence & ((p_AskPermission_0_time = p_Measure_501_time) & (! EXISTS p_RobotMoving_416: RobotMoving. (p_RobotMoving_416_presence & ((p_RobotMoving_416_time <= (p_AskPermission_0_time + 0)) & ((p_AskPermission_0_time + 0) <= p_RobotMoving_416_time)))))))
Def || L49 || c24 <-> Forall p_AskPermission_0: AskPermission. ( (! p_AskPermission_0_presence) | EXISTS p_Measure_501: Measure. (p_Measure_501_presence & ((p_AskPermission_0_time = p_Measure_501_time) & (! EXISTS p_RobotMoving_416: RobotMoving. (p_RobotMoving_416_presence & ((p_RobotMoving_416_time <= (p_AskPermission_0_time + 0)) & ((p_AskPermission_0_time + 0) <= p_RobotMoving_416_time)))))))
DeriveFact || F24 || c24 || L49 R24
Def || L55 || c28 <-> ((EXISTS p_RobotMoving_414: RobotMoving. (p_RobotMoving_414_presence & ((p_RobotMoving_414_time = 1) & (p_RobotMoving_414_presence <-> RobotMoving_15_presence))) & EXISTS p_InformHuman_149: InformHuman. (p_InformHuman_149_presence & ((p_InformHuman_149_time = 0) & (p_InformHuman_149_presence <-> InformHuman_7_presence))) & EXISTS p_AskPermission_70: AskPermission. (p_AskPermission_70_presence & ((p_AskPermission_70_time = 0) & (p_AskPermission_70_presence <-> AskPermission_2_presence))) & EXISTS p_Measure_475: Measure. (p_Measure_475_presence & ((p_Measure_475_time = 0) & (p_Measure_475_humanInRoute <-> False) & (p_Measure_475_humanInRange <-> False) & (p_Measure_475_bumpHuman <-> False) & (p_Measure_475_humanTooClose <-> False) & (p_Measure_475_routeAvailable <-> True) & (p_Measure_475_humanReEnables <-> False) & (p_Measure_475_risk = 0) & (p_Measure_475_efficiency = 0) & (p_Measure_475_isHumanTask <-> False) & (p_Measure_475_humanConsents <-> False) & (p_Measure_475_accident <-> False) & (p_Measure_475_humansPresent <-> False) & (p_Measure_475_obstaclePresent <-> False) & (p_Measure_475_presence <-> Measure_37_presence))) & EXISTS p_blocked_not_RobotMoving_32: blocked_not_RobotMoving. (p_blocked_not_RobotMoving_32_presence & ((p_blocked_not_RobotMoving_32_time = 0) & (p_blocked_not_RobotMoving_32_end = 0) & (p_blocked_not_RobotMoving_32_presence <-> blocked_not_RobotMoving_1_presence)))) & Forall p_Measure_0: Measure. ( (! p_Measure_0_presence) | Forall p_Measure_477: Measure. ( (! p_Measure_477_presence) | ((! (p_Measure_0_time = p_Measure_477_time)) | ((p_Measure_0_time = p_Measure_477_time) & (p_Measure_0_humanInRoute <-> p_Measure_477_humanInRoute) & (p_Measure_0_humanInRange <-> p_Measure_477_humanInRange) & (p_Measure_0_bumpHuman <-> p_Measure_477_bumpHuman) & (p_Measure_0_humanTooClose <-> p_Measure_477_humanTooClose) & (p_Measure_0_routeAvailable <-> p_Measure_477_routeAvailable) & (p_Measure_0_humanReEnables <-> p_Measure_477_humanReEnables) & (p_Measure_0_risk = p_Measure_477_risk) & (p_Measure_0_efficiency = p_Measure_477_efficiency) & (p_Measure_0_isHumanTask <-> p_Measure_477_isHumanTask) & (p_Measure_0_humanConsents <-> p_Measure_477_humanConsents) & (p_Measure_0_accident <-> p_Measure_477_accident) & (p_Measure_0_humansPresent <-> p_Measure_477_humansPresent) & (p_Measure_0_obstaclePresent <-> p_Measure_477_obstaclePresent) & (p_Measure_0_presence <-> p_Measure_477_presence))))))
DeriveFact || F28 || c0 -> (c28) || L55 L1
Def || L60 || c33 <-> (EXISTS p_RobotMoving_414: RobotMoving. (p_RobotMoving_414_presence & ((p_RobotMoving_414_time = 1) & (p_RobotMoving_414_presence <-> RobotMoving_15_presence))) & EXISTS p_InformHuman_149: InformHuman. (p_InformHuman_149_presence & ((p_InformHuman_149_time = 0) & (p_InformHuman_149_presence <-> InformHuman_7_presence))) & EXISTS p_AskPermission_70: AskPermission. (p_AskPermission_70_presence & ((p_AskPermission_70_time = 0) & (p_AskPermission_70_presence <-> AskPermission_2_presence))) & EXISTS p_Measure_475: Measure. (p_Measure_475_presence & ((p_Measure_475_time = 0) & (p_Measure_475_humanInRoute <-> False) & (p_Measure_475_humanInRange <-> False) & (p_Measure_475_bumpHuman <-> False) & (p_Measure_475_humanTooClose <-> False) & (p_Measure_475_routeAvailable <-> True) & (p_Measure_475_humanReEnables <-> False) & (p_Measure_475_risk = 0) & (p_Measure_475_efficiency = 0) & (p_Measure_475_isHumanTask <-> False) & (p_Measure_475_humanConsents <-> False) & (p_Measure_475_accident <-> False) & (p_Measure_475_humansPresent <-> False) & (p_Measure_475_obstaclePresent <-> False) & (p_Measure_475_presence <-> Measure_37_presence))) & EXISTS p_blocked_not_RobotMoving_32: blocked_not_RobotMoving. (p_blocked_not_RobotMoving_32_presence & ((p_blocked_not_RobotMoving_32_time = 0) & (p_blocked_not_RobotMoving_32_end = 0) & (p_blocked_not_RobotMoving_32_presence <-> blocked_not_RobotMoving_1_presence))))
Def || L61 || c34 <-> Forall p_Measure_0: Measure. ( (! p_Measure_0_presence) | Forall p_Measure_477: Measure. ( (! p_Measure_477_presence) | ((! (p_Measure_0_time = p_Measure_477_time)) | ((p_Measure_0_time = p_Measure_477_time) & (p_Measure_0_humanInRoute <-> p_Measure_477_humanInRoute) & (p_Measure_0_humanInRange <-> p_Measure_477_humanInRange) & (p_Measure_0_bumpHuman <-> p_Measure_477_bumpHuman) & (p_Measure_0_humanTooClose <-> p_Measure_477_humanTooClose) & (p_Measure_0_routeAvailable <-> p_Measure_477_routeAvailable) & (p_Measure_0_humanReEnables <-> p_Measure_477_humanReEnables) & (p_Measure_0_risk = p_Measure_477_risk) & (p_Measure_0_efficiency = p_Measure_477_efficiency) & (p_Measure_0_isHumanTask <-> p_Measure_477_isHumanTask) & (p_Measure_0_humanConsents <-> p_Measure_477_humanConsents) & (p_Measure_0_accident <-> p_Measure_477_accident) & (p_Measure_0_humansPresent <-> p_Measure_477_humansPresent) & (p_Measure_0_obstaclePresent <-> p_Measure_477_obstaclePresent) & (p_Measure_0_presence <-> p_Measure_477_presence)))))
DeriveFact || F35 || c28 -> (c33) || L60 L55
DeriveFact || F36 || c28 -> (c34) || L61 L55
Def || L63 || c36 <-> EXISTS p_InformHuman_149: InformHuman. (p_InformHuman_149_presence & ((p_InformHuman_149_time = 0) & (p_InformHuman_149_presence <-> InformHuman_7_presence)))
Def || L64 || c37 <-> EXISTS p_AskPermission_70: AskPermission. (p_AskPermission_70_presence & ((p_AskPermission_70_time = 0) & (p_AskPermission_70_presence <-> AskPermission_2_presence)))
Def || L65 || c38 <-> EXISTS p_Measure_475: Measure. (p_Measure_475_presence & ((p_Measure_475_time = 0) & (p_Measure_475_humanInRoute <-> False) & (p_Measure_475_humanInRange <-> False) & (p_Measure_475_bumpHuman <-> False) & (p_Measure_475_humanTooClose <-> False) & (p_Measure_475_routeAvailable <-> True) & (p_Measure_475_humanReEnables <-> False) & (p_Measure_475_risk = 0) & (p_Measure_475_efficiency = 0) & (p_Measure_475_isHumanTask <-> False) & (p_Measure_475_humanConsents <-> False) & (p_Measure_475_accident <-> False) & (p_Measure_475_humansPresent <-> False) & (p_Measure_475_obstaclePresent <-> False) & (p_Measure_475_presence <-> Measure_37_presence)))
DeriveFact || F38 || c33 -> (c36) || L63 L60
DeriveFact || F39 || c33 -> (c37) || L64 L60
DeriveFact || F40 || c33 -> (c38) || L65 L60
DeriveLemma || EI L63  [p_InformHuman_149:InformHuman<-InformHuman_7] || L68 || c36 -> (InformHuman_7_presence & ((InformHuman_7_time = 0) & (InformHuman_7_presence <-> InformHuman_7_presence))) || L63
AddFact || F44 || c41 <-> (InformHuman_7_presence & ((InformHuman_7_time = 0) & (InformHuman_7_presence <-> InformHuman_7_presence)))
DeriveFact || F45 || c36 -> c41 || F44 L68
DeriveLemma || EI L64  [p_AskPermission_70:AskPermission<-AskPermission_3] || L69 || c37 -> (AskPermission_3_presence & ((AskPermission_3_time = 0) & (AskPermission_3_presence <-> AskPermission_2_presence))) || L64
AddFact || F46 || c42 <-> (AskPermission_3_presence & ((AskPermission_3_time = 0) & (AskPermission_3_presence <-> AskPermission_2_presence)))
DeriveFact || F47 || c37 -> c42 || F46 L69
DeriveLemma || EI L65  [p_Measure_475:Measure<-Measure_38] || L70 || c38 -> (Measure_38_presence & ((Measure_38_time = 0) & (Measure_38_humanInRoute <-> False) & (Measure_38_humanInRange <-> False) & (Measure_38_bumpHuman <-> False) & (Measure_38_humanTooClose <-> False) & (Measure_38_routeAvailable <-> True) & (Measure_38_humanReEnables <-> False) & (Measure_38_risk = 0) & (Measure_38_efficiency = 0) & (Measure_38_isHumanTask <-> False) & (Measure_38_humanConsents <-> False) & (Measure_38_accident <-> False) & (Measure_38_humansPresent <-> False) & (Measure_38_obstaclePresent <-> False) & (Measure_38_presence <-> Measure_37_presence))) || L65
AddFact || F48 || c43 <-> (Measure_38_presence & ((Measure_38_time = 0) & (Measure_38_humanInRoute <-> False) & (Measure_38_humanInRange <-> False) & (Measure_38_bumpHuman <-> False) & (Measure_38_humanTooClose <-> False) & (Measure_38_routeAvailable <-> True) & (Measure_38_humanReEnables <-> False) & (Measure_38_risk = 0) & (Measure_38_efficiency = 0) & (Measure_38_isHumanTask <-> False) & (Measure_38_humanConsents <-> False) & (Measure_38_accident <-> False) & (Measure_38_humansPresent <-> False) & (Measure_38_obstaclePresent <-> False) & (Measure_38_presence <-> Measure_37_presence)))
DeriveFact || F49 || c38 -> c43 || F48 L70
DeriveLemma || UI L61  [p_Measure_0:Measure<-Measure_38] || L77 || c34 -> ((! Measure_38_presence) | Forall p_Measure_506: Measure. ( (! p_Measure_506_presence) | ((! (Measure_38_time = p_Measure_506_time)) | ((Measure_38_time = p_Measure_506_time) & (Measure_38_humanInRoute <-> p_Measure_506_humanInRoute) & (Measure_38_humanInRange <-> p_Measure_506_humanInRange) & (Measure_38_bumpHuman <-> p_Measure_506_bumpHuman) & (Measure_38_humanTooClose <-> p_Measure_506_humanTooClose) & (Measure_38_routeAvailable <-> p_Measure_506_routeAvailable) & (Measure_38_humanReEnables <-> p_Measure_506_humanReEnables) & (Measure_38_risk = p_Measure_506_risk) & (Measure_38_efficiency = p_Measure_506_efficiency) & (Measure_38_isHumanTask <-> p_Measure_506_isHumanTask) & (Measure_38_humanConsents <-> p_Measure_506_humanConsents) & (Measure_38_accident <-> p_Measure_506_accident) & (Measure_38_humansPresent <-> p_Measure_506_humansPresent) & (Measure_38_obstaclePresent <-> p_Measure_506_obstaclePresent) & (Measure_38_presence <-> p_Measure_506_presence))))) || L61 L70
Def || L78 || c50 <-> ((! Measure_38_presence) | Forall p_Measure_506: Measure. ( (! p_Measure_506_presence) | ((! (Measure_38_time = p_Measure_506_time)) | ((Measure_38_time = p_Measure_506_time) & (Measure_38_humanInRoute <-> p_Measure_506_humanInRoute) & (Measure_38_humanInRange <-> p_Measure_506_humanInRange) & (Measure_38_bumpHuman <-> p_Measure_506_bumpHuman) & (Measure_38_humanTooClose <-> p_Measure_506_humanTooClose) & (Measure_38_routeAvailable <-> p_Measure_506_routeAvailable) & (Measure_38_humanReEnables <-> p_Measure_506_humanReEnables) & (Measure_38_risk = p_Measure_506_risk) & (Measure_38_efficiency = p_Measure_506_efficiency) & (Measure_38_isHumanTask <-> p_Measure_506_isHumanTask) & (Measure_38_humanConsents <-> p_Measure_506_humanConsents) & (Measure_38_accident <-> p_Measure_506_accident) & (Measure_38_humansPresent <-> p_Measure_506_humansPresent) & (Measure_38_obstaclePresent <-> p_Measure_506_obstaclePresent) & (Measure_38_presence <-> p_Measure_506_presence)))))
DeriveFact || F59 || c34 -> c50 || L78 L77
AddFact || F60 || c51 <-> (! Measure_38_presence)
Def || L79 || c52 <-> Forall p_Measure_506: Measure. ( (! p_Measure_506_presence) | ((! (Measure_38_time = p_Measure_506_time)) | ((Measure_38_time = p_Measure_506_time) & (Measure_38_humanInRoute <-> p_Measure_506_humanInRoute) & (Measure_38_humanInRange <-> p_Measure_506_humanInRange) & (Measure_38_bumpHuman <-> p_Measure_506_bumpHuman) & (Measure_38_humanTooClose <-> p_Measure_506_humanTooClose) & (Measure_38_routeAvailable <-> p_Measure_506_routeAvailable) & (Measure_38_humanReEnables <-> p_Measure_506_humanReEnables) & (Measure_38_risk = p_Measure_506_risk) & (Measure_38_efficiency = p_Measure_506_efficiency) & (Measure_38_isHumanTask <-> p_Measure_506_isHumanTask) & (Measure_38_humanConsents <-> p_Measure_506_humanConsents) & (Measure_38_accident <-> p_Measure_506_accident) & (Measure_38_humansPresent <-> p_Measure_506_humansPresent) & (Measure_38_obstaclePresent <-> p_Measure_506_obstaclePresent) & (Measure_38_presence <-> p_Measure_506_presence))))
DeriveFact || F61 || c50 -> (c51 | c52) || F60 L79 L78
AddFact || F82 || c70 <-> (! True)
DeriveLemma || UI L15  [p_InformHuman_0:InformHuman<-InformHuman_7] || L209 || c7 -> ((! InformHuman_7_presence) | EXISTS p_Measure_511: Measure. (p_Measure_511_presence & ((InformHuman_7_time = p_Measure_511_time) & (((! (True & (! p_Measure_511_routeAvailable))) | EXISTS p_AskPermission_74: AskPermission. (p_AskPermission_74_presence & ((p_AskPermission_74_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AskPermission_74_time)))) & ((! ((True & p_Measure_511_routeAvailable) & p_Measure_511_humanInRoute)) | EXISTS p_AdjustRoute_121: AdjustRoute. (p_AdjustRoute_121_presence & ((p_AdjustRoute_121_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AdjustRoute_121_time)))) & ((! (((True & p_Measure_511_routeAvailable) & (! p_Measure_511_humanInRoute)) & True)) | EXISTS p_RobotMoving_418: RobotMoving. (p_RobotMoving_418_presence & ((p_RobotMoving_418_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_RobotMoving_418_time)))))))) || L15 L68
Def || L210 || c195 <-> ((! InformHuman_7_presence) | EXISTS p_Measure_511: Measure. (p_Measure_511_presence & ((InformHuman_7_time = p_Measure_511_time) & (((! (True & (! p_Measure_511_routeAvailable))) | EXISTS p_AskPermission_74: AskPermission. (p_AskPermission_74_presence & ((p_AskPermission_74_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AskPermission_74_time)))) & ((! ((True & p_Measure_511_routeAvailable) & p_Measure_511_humanInRoute)) | EXISTS p_AdjustRoute_121: AdjustRoute. (p_AdjustRoute_121_presence & ((p_AdjustRoute_121_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AdjustRoute_121_time)))) & ((! (((True & p_Measure_511_routeAvailable) & (! p_Measure_511_humanInRoute)) & True)) | EXISTS p_RobotMoving_418: RobotMoving. (p_RobotMoving_418_presence & ((p_RobotMoving_418_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_RobotMoving_418_time))))))))
DeriveFact || F269 || c7 -> c195 || L210 L209
AddFact || F270 || c196 <-> (! InformHuman_7_presence) || (1951, 1962)
Def || L211 || c197 <-> EXISTS p_Measure_511: Measure. (p_Measure_511_presence & ((InformHuman_7_time = p_Measure_511_time) & (((! (True & (! p_Measure_511_routeAvailable))) | EXISTS p_AskPermission_74: AskPermission. (p_AskPermission_74_presence & ((p_AskPermission_74_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AskPermission_74_time)))) & ((! ((True & p_Measure_511_routeAvailable) & p_Measure_511_humanInRoute)) | EXISTS p_AdjustRoute_121: AdjustRoute. (p_AdjustRoute_121_presence & ((p_AdjustRoute_121_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AdjustRoute_121_time)))) & ((! (((True & p_Measure_511_routeAvailable) & (! p_Measure_511_humanInRoute)) & True)) | EXISTS p_RobotMoving_418: RobotMoving. (p_RobotMoving_418_presence & ((p_RobotMoving_418_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_RobotMoving_418_time)))))))
DeriveFact || F271 || c195 -> (c196 | c197) || F270 L211 L210
DeriveLemma || EI L211  [p_Measure_511:Measure<-t_Measure_343] || L212 || c197 -> (t_Measure_343_presence & ((InformHuman_7_time = t_Measure_343_time) & (((! (True & (! t_Measure_343_routeAvailable))) | EXISTS p_AskPermission_73: AskPermission. (p_AskPermission_73_presence & ((p_AskPermission_73_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AskPermission_73_time)))) & ((! ((True & t_Measure_343_routeAvailable) & t_Measure_343_humanInRoute)) | EXISTS p_AdjustRoute_120: AdjustRoute. (p_AdjustRoute_120_presence & ((p_AdjustRoute_120_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AdjustRoute_120_time)))) & ((! (((True & t_Measure_343_routeAvailable) & (! t_Measure_343_humanInRoute)) & True)) | EXISTS p_RobotMoving_417: RobotMoving. (p_RobotMoving_417_presence & ((p_RobotMoving_417_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_RobotMoving_417_time))))))) || L211
Def || L213 || c198 <-> (t_Measure_343_presence & ((InformHuman_7_time = t_Measure_343_time) & (((! (True & (! t_Measure_343_routeAvailable))) | EXISTS p_AskPermission_73: AskPermission. (p_AskPermission_73_presence & ((p_AskPermission_73_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AskPermission_73_time)))) & ((! ((True & t_Measure_343_routeAvailable) & t_Measure_343_humanInRoute)) | EXISTS p_AdjustRoute_120: AdjustRoute. (p_AdjustRoute_120_presence & ((p_AdjustRoute_120_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AdjustRoute_120_time)))) & ((! (((True & t_Measure_343_routeAvailable) & (! t_Measure_343_humanInRoute)) & True)) | EXISTS p_RobotMoving_417: RobotMoving. (p_RobotMoving_417_presence & ((p_RobotMoving_417_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_RobotMoving_417_time)))))))
DeriveFact || F272 || c197 -> c198 || L213 L212
AddFact || F273 || c199 <-> t_Measure_343_presence
Def || L214 || c200 <-> ((InformHuman_7_time = t_Measure_343_time) & (((! (True & (! t_Measure_343_routeAvailable))) | EXISTS p_AskPermission_73: AskPermission. (p_AskPermission_73_presence & ((p_AskPermission_73_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AskPermission_73_time)))) & ((! ((True & t_Measure_343_routeAvailable) & t_Measure_343_humanInRoute)) | EXISTS p_AdjustRoute_120: AdjustRoute. (p_AdjustRoute_120_presence & ((p_AdjustRoute_120_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AdjustRoute_120_time)))) & ((! (((True & t_Measure_343_routeAvailable) & (! t_Measure_343_humanInRoute)) & True)) | EXISTS p_RobotMoving_417: RobotMoving. (p_RobotMoving_417_presence & ((p_RobotMoving_417_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_RobotMoving_417_time))))))
DeriveFact || F274 || c198 -> (c199) || F273 L213
DeriveFact || F275 || c198 -> (c200) || L214 L213
AddFact || F276 || c201 <-> (InformHuman_7_time = t_Measure_343_time)
Def || L215 || c202 <-> (((! (True & (! t_Measure_343_routeAvailable))) | EXISTS p_AskPermission_73: AskPermission. (p_AskPermission_73_presence & ((p_AskPermission_73_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AskPermission_73_time)))) & ((! ((True & t_Measure_343_routeAvailable) & t_Measure_343_humanInRoute)) | EXISTS p_AdjustRoute_120: AdjustRoute. (p_AdjustRoute_120_presence & ((p_AdjustRoute_120_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_AdjustRoute_120_time)))) & ((! (((True & t_Measure_343_routeAvailable) & (! t_Measure_343_humanInRoute)) & True)) | EXISTS p_RobotMoving_417: RobotMoving. (p_RobotMoving_417_presence & ((p_RobotMoving_417_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_RobotMoving_417_time)))))
DeriveFact || F277 || c200 -> (c201) || F276 L214
DeriveFact || F278 || c200 -> (c202) || L215 L214
Def || L218 || c205 <-> ((! (((True & t_Measure_343_routeAvailable) & (! t_Measure_343_humanInRoute)) & True)) | EXISTS p_RobotMoving_417: RobotMoving. (p_RobotMoving_417_presence & ((p_RobotMoving_417_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_RobotMoving_417_time))))
DeriveFact || F281 || c202 -> (c205) || L218 L215
Def || L229 || c216 <-> ((! True) | (! t_Measure_343_routeAvailable))
AddFact || F295 || c218 <-> (! t_Measure_343_routeAvailable) || (2036, 2052)
DeriveFact || F296 || c216 -> (c70 | c218) || F82 F295 L229
Def || L232 || c222 <-> (! (((True & t_Measure_343_routeAvailable) & (! t_Measure_343_humanInRoute)) & True))
Def || L233 || c223 <-> EXISTS p_RobotMoving_417: RobotMoving. (p_RobotMoving_417_presence & ((p_RobotMoving_417_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= p_RobotMoving_417_time)))
DeriveFact || F302 || c205 -> (c222 | c223) || L232 L233 L218
DeriveLemma || NNF L232  || L234 || c222 <-> ((((! True) | (! t_Measure_343_routeAvailable)) | t_Measure_343_humanInRoute) | (! True)) || L232
Def || L235 || c224 <-> ((((! True) | (! t_Measure_343_routeAvailable)) | t_Measure_343_humanInRoute) | (! True))
DeriveFact || F303 || c222 -> c224 || L235 L234
Def || L236 || c225 <-> (((! True) | (! t_Measure_343_routeAvailable)) | t_Measure_343_humanInRoute)
DeriveFact || F304 || c224 -> (c225 | c70) || L236 F82 L235
AddFact || F305 || c226 <-> t_Measure_343_humanInRoute || (1987, 2001)
DeriveFact || F306 || c225 -> (c216 | c226) || L229 F305 L236
DeriveLemma || EI L233  [p_RobotMoving_417:RobotMoving<-t_RobotMoving_15] || L237 || c223 -> (t_RobotMoving_15_presence & ((t_RobotMoving_15_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= t_RobotMoving_15_time))) || L233
Def || L238 || c227 <-> (t_RobotMoving_15_presence & ((t_RobotMoving_15_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= t_RobotMoving_15_time)))
DeriveFact || F307 || c223 -> c227 || L238 L237
AddFact || F308 || c228 <-> t_RobotMoving_15_presence || (1968, 1979)
AddFact || F309 || c229 <-> ((t_RobotMoving_15_time <= (InformHuman_7_time + 0)) & ((InformHuman_7_time + 0) <= t_RobotMoving_15_time))
DeriveFact || F310 || c227 -> (c228) || F308 L238
DeriveFact || F311 || c227 -> (c229) || F309 L238
AddFact || F322 || c236 <-> (! t_RobotMoving_15_presence) || (1235, 1246)
DeriveLemma || UI L79  [p_Measure_506:Measure<-t_Measure_343] || L325 || c52 -> ((! t_Measure_343_presence) | ((! (Measure_38_time = t_Measure_343_time)) | ((Measure_38_time = t_Measure_343_time) & (Measure_38_humanInRoute <-> t_Measure_343_humanInRoute) & (Measure_38_humanInRange <-> t_Measure_343_humanInRange) & (Measure_38_bumpHuman <-> t_Measure_343_bumpHuman) & (Measure_38_humanTooClose <-> t_Measure_343_humanTooClose) & (Measure_38_routeAvailable <-> t_Measure_343_routeAvailable) & (Measure_38_humanReEnables <-> t_Measure_343_humanReEnables) & (Measure_38_risk = t_Measure_343_risk) & (Measure_38_efficiency = t_Measure_343_efficiency) & (Measure_38_isHumanTask <-> t_Measure_343_isHumanTask) & (Measure_38_humanConsents <-> t_Measure_343_humanConsents) & (Measure_38_accident <-> t_Measure_343_accident) & (Measure_38_humansPresent <-> t_Measure_343_humansPresent) & (Measure_38_obstaclePresent <-> t_Measure_343_obstaclePresent) & (Measure_38_presence <-> t_Measure_343_presence)))) || L79 L212
AddFact || F445 || c328 <-> ((! t_Measure_343_presence) | ((! (Measure_38_time = t_Measure_343_time)) | ((Measure_38_time = t_Measure_343_time) & (Measure_38_humanInRoute <-> t_Measure_343_humanInRoute) & (Measure_38_humanInRange <-> t_Measure_343_humanInRange) & (Measure_38_bumpHuman <-> t_Measure_343_bumpHuman) & (Measure_38_humanTooClose <-> t_Measure_343_humanTooClose) & (Measure_38_routeAvailable <-> t_Measure_343_routeAvailable) & (Measure_38_humanReEnables <-> t_Measure_343_humanReEnables) & (Measure_38_risk = t_Measure_343_risk) & (Measure_38_efficiency = t_Measure_343_efficiency) & (Measure_38_isHumanTask <-> t_Measure_343_isHumanTask) & (Measure_38_humanConsents <-> t_Measure_343_humanConsents) & (Measure_38_accident <-> t_Measure_343_accident) & (Measure_38_humansPresent <-> t_Measure_343_humansPresent) & (Measure_38_obstaclePresent <-> t_Measure_343_obstaclePresent) & (Measure_38_presence <-> t_Measure_343_presence))))
DeriveFact || F446 || c52 -> c328 || F445 L325
DeriveLemma || UI L49  [p_AskPermission_0:AskPermission<-AskPermission_3] || L671 || c24 -> ((! AskPermission_3_presence) | EXISTS p_Measure_522: Measure. (p_Measure_522_presence & ((AskPermission_3_time = p_Measure_522_time) & (! EXISTS p_RobotMoving_424: RobotMoving. (p_RobotMoving_424_presence & ((p_RobotMoving_424_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= p_RobotMoving_424_time))))))) || L49 L69
Def || L672 || c688 <-> ((! AskPermission_3_presence) | EXISTS p_Measure_522: Measure. (p_Measure_522_presence & ((AskPermission_3_time = p_Measure_522_time) & (! EXISTS p_RobotMoving_424: RobotMoving. (p_RobotMoving_424_presence & ((p_RobotMoving_424_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= p_RobotMoving_424_time)))))))
DeriveFact || F991 || c24 -> c688 || L672 L671
AddFact || F992 || c689 <-> (! AskPermission_3_presence) || (3720, 3733)
Def || L673 || c690 <-> EXISTS p_Measure_522: Measure. (p_Measure_522_presence & ((AskPermission_3_time = p_Measure_522_time) & (! EXISTS p_RobotMoving_424: RobotMoving. (p_RobotMoving_424_presence & ((p_RobotMoving_424_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= p_RobotMoving_424_time))))))
DeriveFact || F993 || c688 -> (c689 | c690) || F992 L673 L672
DeriveLemma || EI L673  [p_Measure_522:Measure<-t_Measure_353] || L674 || c690 -> (t_Measure_353_presence & ((AskPermission_3_time = t_Measure_353_time) & (! EXISTS p_RobotMoving_421: RobotMoving. (p_RobotMoving_421_presence & ((p_RobotMoving_421_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= p_RobotMoving_421_time)))))) || L673
Def || L675 || c691 <-> (t_Measure_353_presence & ((AskPermission_3_time = t_Measure_353_time) & (! EXISTS p_RobotMoving_421: RobotMoving. (p_RobotMoving_421_presence & ((p_RobotMoving_421_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= p_RobotMoving_421_time))))))
DeriveFact || F994 || c690 -> c691 || L675 L674
Def || L676 || c693 <-> ((AskPermission_3_time = t_Measure_353_time) & (! EXISTS p_RobotMoving_421: RobotMoving. (p_RobotMoving_421_presence & ((p_RobotMoving_421_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= p_RobotMoving_421_time)))))
DeriveFact || F997 || c691 -> (c693) || L676 L675
Def || L677 || c695 <-> (! EXISTS p_RobotMoving_421: RobotMoving. (p_RobotMoving_421_presence & ((p_RobotMoving_421_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= p_RobotMoving_421_time))))
DeriveFact || F1000 || c693 -> (c695) || L677 L676
DeriveLemma || NNF L677  || L678 || c695 <-> Forall p_RobotMoving_422: RobotMoving. ( (! p_RobotMoving_422_presence) | (! ((p_RobotMoving_422_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= p_RobotMoving_422_time)))) || L677
Def || L679 || c696 <-> Forall p_RobotMoving_422: RobotMoving. ( (! p_RobotMoving_422_presence) | (! ((p_RobotMoving_422_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= p_RobotMoving_422_time))))
DeriveFact || F1001 || c695 -> c696 || L679 L678
DeriveLemma || UI L679  [p_RobotMoving_422:RobotMoving<-t_RobotMoving_15] || L682 || c696 -> ((! t_RobotMoving_15_presence) | (! ((t_RobotMoving_15_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= t_RobotMoving_15_time)))) || L679 L237
Def || L683 || c699 <-> ((! t_RobotMoving_15_presence) | (! ((t_RobotMoving_15_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= t_RobotMoving_15_time))))
DeriveFact || F1005 || c696 -> c699 || L683 L682
AddFact || F1006 || c700 <-> (! ((t_RobotMoving_15_time <= (AskPermission_3_time + 0)) & ((AskPermission_3_time + 0) <= t_RobotMoving_15_time)))
DeriveFact || F1007 || c699 -> (c236 | c700) || F322 F1006 L683
UNSAT || F272 F296 F44 F992 F305 F7 F295 F269 F276 F48 F24 F306 F38 F445 F82 F271 F304 F275 F1005 F994 F1006 F1000 F1007 F302 F60 F36 F303 F46 F310 F309 F311 F273 F281 F49 F61 F308 F270 F28 F993 F1001 F991 F307 F278 F322 F47 F277 F997 F35 F59 F446 F39 F40 F0 F45 F274
Vars || Measure_37_presence:Bool c52:Bool t_Measure_343_efficiency:Int Measure_38_humanTooClose:Bool c225:Bool c690:Bool t_Measure_343_routeAvailable:Bool c50:Bool c51:Bool c201:Bool c42:Bool Measure_38_presence:Bool t_Measure_343_humanTooClose:Bool c224:Bool c700:Bool t_Measure_343_obstaclePresent:Bool c223:Bool c38:Bool t_Measure_343_humansPresent:Bool c202:Bool c227:Bool Measure_38_isHumanTask:Bool t_Measure_343_presence:Bool c34:Bool Measure_38_time:Int c70:Bool t_Measure_343_humanReEnables:Bool Measure_38_humanConsents:Bool Measure_38_obstaclePresent:Bool t_Measure_343_humanConsents:Bool Measure_38_bumpHuman:Bool c199:Bool t_RobotMoving_15_time:Int c236:Bool c200:Bool c699:Bool c693:Bool Measure_38_humanInRange:Bool c195:Bool t_Measure_343_humanInRoute:Bool c691:Bool c198:Bool AskPermission_3_presence:Bool c33:Bool c216:Bool c24:Bool t_Measure_343_risk:Int t_RobotMoving_15_presence:Bool Measure_38_humansPresent:Bool c226:Bool c218:Bool InformHuman_7_time:Int c229:Bool Measure_38_routeAvailable:Bool c43:Bool c222:Bool c196:Bool c36:Bool c328:Bool AskPermission_3_time:Int Measure_38_humanInRoute:Bool Measure_38_risk:Int c28:Bool c0:Bool Measure_38_accident:Bool InformHuman_7_presence:Bool c696:Bool t_Measure_343_accident:Bool Measure_38_humanReEnables:Bool c41:Bool Measure_38_efficiency:Int c7:Bool c689:Bool t_Measure_343_time:Int t_Measure_343_humanInRange:Bool c688:Bool c37:Bool t_Measure_343_bumpHuman:Bool t_Measure_343_isHumanTask:Bool c695:Bool AskPermission_2_presence:Bool c205:Bool c228:Bool c197:Bool
