Input || R0 || (! Forall p_CallSupport_0: CallSupport. ( (! p_CallSupport_0_presence) | EXISTS p_Measure_22: Measure. (p_Measure_22_presence & ((p_CallSupport_0_time = p_Measure_22_time) & (! EXISTS p_ProvideCompanionship_14: ProvideCompanionship. (p_ProvideCompanionship_14_presence & ((p_ProvideCompanionship_14_time <= (p_CallSupport_0_time + 600)) & ((p_CallSupport_0_time + 0) <= p_ProvideCompanionship_14_time))))))))
Def || L1 || c0 <-> (! Forall p_CallSupport_0: CallSupport. ( (! p_CallSupport_0_presence) | EXISTS p_Measure_22: Measure. (p_Measure_22_presence & ((p_CallSupport_0_time = p_Measure_22_time) & (! EXISTS p_ProvideCompanionship_14: ProvideCompanionship. (p_ProvideCompanionship_14_presence & ((p_ProvideCompanionship_14_time <= (p_CallSupport_0_time + 600)) & ((p_CallSupport_0_time + 0) <= p_ProvideCompanionship_14_time))))))))
DeriveFact || F0 || c0 || L1 R0
Input || R1 || Forall p_PatientFallen_0: PatientFallen. ( (! p_PatientFallen_0_presence) | EXISTS p_Measure_23: Measure. (p_Measure_23_presence & ((p_PatientFallen_0_time = p_Measure_23_time) & EXISTS p_CallSupport_12: CallSupport. (p_CallSupport_12_presence & ((p_CallSupport_12_time <= (p_PatientFallen_0_time + 0)) & ((p_PatientFallen_0_time + 0) <= p_CallSupport_12_time))))))
Def || L3 || c1 <-> Forall p_PatientFallen_0: PatientFallen. ( (! p_PatientFallen_0_presence) | EXISTS p_Measure_23: Measure. (p_Measure_23_presence & ((p_PatientFallen_0_time = p_Measure_23_time) & EXISTS p_CallSupport_12: CallSupport. (p_CallSupport_12_presence & ((p_CallSupport_12_time <= (p_PatientFallen_0_time + 0)) & ((p_PatientFallen_0_time + 0) <= p_CallSupport_12_time))))))
DeriveFact || F1 || c1 || L3 R1
Input || R2 || Forall p_PatientFallen_2: PatientFallen. ( (! p_PatientFallen_2_presence) | EXISTS p_Measure_24: Measure. (p_Measure_24_presence & ((p_PatientFallen_2_time = p_Measure_24_time) & (((! (True & p_Measure_24_patientNotDeaf)) | True) & ((! ((True & (! p_Measure_24_patientNotDeaf)) & True)) | EXISTS p_ProvideCompanionship_15: ProvideCompanionship. (p_ProvideCompanionship_15_presence & ((p_ProvideCompanionship_15_time <= (p_PatientFallen_2_time + 600)) & ((p_PatientFallen_2_time + 0) <= p_ProvideCompanionship_15_time))))))))
Def || L5 || c2 <-> Forall p_PatientFallen_2: PatientFallen. ( (! p_PatientFallen_2_presence) | EXISTS p_Measure_24: Measure. (p_Measure_24_presence & ((p_PatientFallen_2_time = p_Measure_24_time) & (((! (True & p_Measure_24_patientNotDeaf)) | True) & ((! ((True & (! p_Measure_24_patientNotDeaf)) & True)) | EXISTS p_ProvideCompanionship_15: ProvideCompanionship. (p_ProvideCompanionship_15_presence & ((p_ProvideCompanionship_15_time <= (p_PatientFallen_2_time + 600)) & ((p_PatientFallen_2_time + 0) <= p_ProvideCompanionship_15_time))))))))
DeriveFact || F2 || c2 || L5 R2
Input || R3 || Forall p_Measure_0: Measure. ( (! p_Measure_0_presence) | Forall p_Measure_25: Measure. ( (! p_Measure_25_presence) | ((! (p_Measure_0_time = p_Measure_25_time)) | ((p_Measure_0_time = p_Measure_25_time) & (p_Measure_0_underDressed <-> p_Measure_25_underDressed) & (p_Measure_0_patientNotDeaf <-> p_Measure_25_patientNotDeaf) & (p_Measure_0_presence <-> p_Measure_25_presence)))))
Def || L7 || c3 <-> Forall p_Measure_0: Measure. ( (! p_Measure_0_presence) | Forall p_Measure_25: Measure. ( (! p_Measure_25_presence) | ((! (p_Measure_0_time = p_Measure_25_time)) | ((p_Measure_0_time = p_Measure_25_time) & (p_Measure_0_underDressed <-> p_Measure_25_underDressed) & (p_Measure_0_patientNotDeaf <-> p_Measure_25_patientNotDeaf) & (p_Measure_0_presence <-> p_Measure_25_presence)))))
DeriveFact || F3 || c3 || L7 R3
DeriveLemma || NNF L1 || L8 || c0 <-> EXISTS p_CallSupport_13: CallSupport. (p_CallSupport_13_presence & Forall p_Measure_27: Measure. ( (! p_Measure_27_presence) | ((! (p_CallSupport_13_time = p_Measure_27_time)) | EXISTS p_ProvideCompanionship_16: ProvideCompanionship. (p_ProvideCompanionship_16_presence & ((p_ProvideCompanionship_16_time <= (p_CallSupport_13_time + 600)) & ((p_CallSupport_13_time + 0) <= p_ProvideCompanionship_16_time)))))) 
Def || L9 || c4 <-> EXISTS p_CallSupport_13: CallSupport. (p_CallSupport_13_presence & Forall p_Measure_27: Measure. ( (! p_Measure_27_presence) | ((! (p_CallSupport_13_time = p_Measure_27_time)) | EXISTS p_ProvideCompanionship_16: ProvideCompanionship. (p_ProvideCompanionship_16_presence & ((p_ProvideCompanionship_16_time <= (p_CallSupport_13_time + 600)) & ((p_CallSupport_13_time + 0) <= p_ProvideCompanionship_16_time))))))
DeriveFact || F4 || c0 -> c4 || L9 L8
DeriveLemma || EI L9  [p_CallSupport_13:CallSupport<-CallSupport_0] || L10 || c4 -> (CallSupport_0_presence & Forall p_Measure_29: Measure. ( (! p_Measure_29_presence) | ((! (CallSupport_0_time = p_Measure_29_time)) | EXISTS p_ProvideCompanionship_17: ProvideCompanionship. (p_ProvideCompanionship_17_presence & ((p_ProvideCompanionship_17_time <= (CallSupport_0_time + 600)) & ((CallSupport_0_time + 0) <= p_ProvideCompanionship_17_time))))))
Def || L11 || c5 <-> (CallSupport_0_presence & Forall p_Measure_29: Measure. ( (! p_Measure_29_presence) | ((! (CallSupport_0_time = p_Measure_29_time)) | EXISTS p_ProvideCompanionship_17: ProvideCompanionship. (p_ProvideCompanionship_17_presence & ((p_ProvideCompanionship_17_time <= (CallSupport_0_time + 600)) & ((CallSupport_0_time + 0) <= p_ProvideCompanionship_17_time))))))
DeriveFact || F5 || c4 -> c5 || L11 L10
AddFact || F6 || c6 <-> CallSupport_0_presence || 708 719
Def || L12 || c7 <-> Forall p_Measure_29: Measure. ( (! p_Measure_29_presence) | ((! (CallSupport_0_time = p_Measure_29_time)) | EXISTS p_ProvideCompanionship_17: ProvideCompanionship. (p_ProvideCompanionship_17_presence & ((p_ProvideCompanionship_17_time <= (CallSupport_0_time + 600)) & ((CallSupport_0_time + 0) <= p_ProvideCompanionship_17_time)))))
DeriveFact || F7 || c5 -> (c6) || F6 L11
DeriveFact || F8 || c5 -> (c7) || L12 L11
Def || L13 || c8 <-> (CallSupport_0_presence & Forall p_Measure_29: Measure. ( (! p_Measure_29_presence) | ((! (CallSupport_0_time = p_Measure_29_time)) | EXISTS p_ProvideCompanionship_17: ProvideCompanionship. (p_ProvideCompanionship_17_presence & ((p_ProvideCompanionship_17_time <= (CallSupport_0_time + 600)) & ((CallSupport_0_time + 0) <= p_ProvideCompanionship_17_time))))))
DeriveFact || F9 || c8 -> (c6) || F6 L13
DeriveFact || F10 || c8 -> (c7) || L12 L13
