Input || R0 || (EXISTS p_CallSupport_1: CallSupport. (p_CallSupport_1_presence & EXISTS p_Measure_41: Measure. (p_Measure_41_presence & (p_CallSupport_1_time = p_Measure_41_time))) & ((EXISTS p_PatientFallen_14: PatientFallen. (p_PatientFallen_14_presence & ((p_PatientFallen_14_time = 0) & (p_PatientFallen_14_presence <-> PatientFallen_4_presence))) & EXISTS p_ProvideCompanionship_26: ProvideCompanionship. (p_ProvideCompanionship_26_presence & ((p_ProvideCompanionship_26_time = 1) & (p_ProvideCompanionship_26_presence <-> ProvideCompanionship_1_presence))) & EXISTS p_CallSupport_19: CallSupport. (p_CallSupport_19_presence & ((p_CallSupport_19_time = 0) & (p_CallSupport_19_presence <-> CallSupport_2_presence))) & EXISTS p_Measure_39: Measure. (p_Measure_39_presence & ((p_Measure_39_time = 0) & (p_Measure_39_underDressed <-> True) & (p_Measure_39_patientNotDeaf <-> False) & (p_Measure_39_presence <-> Measure_8_presence))) & EXISTS p_Measure_40: Measure. (p_Measure_40_presence & ((p_Measure_40_time = 600) & (p_Measure_40_underDressed <-> False) & (p_Measure_40_patientNotDeaf <-> True) & (p_Measure_40_presence <-> Measure_8_presence))) & EXISTS p_blocked_not_ProvideCompanionship_4: blocked_not_ProvideCompanionship. (p_blocked_not_ProvideCompanionship_4_presence & ((p_blocked_not_ProvideCompanionship_4_time = 0) & (p_blocked_not_ProvideCompanionship_4_end = 600) & (p_blocked_not_ProvideCompanionship_4_presence <-> blocked_not_ProvideCompanionship_1_presence)))) & Forall p_Measure_0: Measure. ( (! p_Measure_0_presence) | Forall p_Measure_42: Measure. ( (! p_Measure_42_presence) | ((! (p_Measure_0_time = p_Measure_42_time)) | ((p_Measure_0_time = p_Measure_42_time) & (p_Measure_0_underDressed <-> p_Measure_42_underDressed) & (p_Measure_0_patientNotDeaf <-> p_Measure_42_patientNotDeaf) & (p_Measure_0_presence <-> p_Measure_42_presence)))))))
Def || L1 || c0 <-> (EXISTS p_CallSupport_1: CallSupport. (p_CallSupport_1_presence & EXISTS p_Measure_41: Measure. (p_Measure_41_presence & (p_CallSupport_1_time = p_Measure_41_time))) & ((EXISTS p_PatientFallen_14: PatientFallen. (p_PatientFallen_14_presence & ((p_PatientFallen_14_time = 0) & (p_PatientFallen_14_presence <-> PatientFallen_4_presence))) & EXISTS p_ProvideCompanionship_26: ProvideCompanionship. (p_ProvideCompanionship_26_presence & ((p_ProvideCompanionship_26_time = 1) & (p_ProvideCompanionship_26_presence <-> ProvideCompanionship_1_presence))) & EXISTS p_CallSupport_19: CallSupport. (p_CallSupport_19_presence & ((p_CallSupport_19_time = 0) & (p_CallSupport_19_presence <-> CallSupport_2_presence))) & EXISTS p_Measure_39: Measure. (p_Measure_39_presence & ((p_Measure_39_time = 0) & (p_Measure_39_underDressed <-> True) & (p_Measure_39_patientNotDeaf <-> False) & (p_Measure_39_presence <-> Measure_8_presence))) & EXISTS p_Measure_40: Measure. (p_Measure_40_presence & ((p_Measure_40_time = 600) & (p_Measure_40_underDressed <-> False) & (p_Measure_40_patientNotDeaf <-> True) & (p_Measure_40_presence <-> Measure_8_presence))) & EXISTS p_blocked_not_ProvideCompanionship_4: blocked_not_ProvideCompanionship. (p_blocked_not_ProvideCompanionship_4_presence & ((p_blocked_not_ProvideCompanionship_4_time = 0) & (p_blocked_not_ProvideCompanionship_4_end = 600) & (p_blocked_not_ProvideCompanionship_4_presence <-> blocked_not_ProvideCompanionship_1_presence)))) & Forall p_Measure_0: Measure. ( (! p_Measure_0_presence) | Forall p_Measure_42: Measure. ( (! p_Measure_42_presence) | ((! (p_Measure_0_time = p_Measure_42_time)) | ((p_Measure_0_time = p_Measure_42_time) & (p_Measure_0_underDressed <-> p_Measure_42_underDressed) & (p_Measure_0_patientNotDeaf <-> p_Measure_42_patientNotDeaf) & (p_Measure_0_presence <-> p_Measure_42_presence)))))))
DeriveFact || F0 || c0 || L1 R0
Input || R3 || Forall p_CallSupport_0: CallSupport. ( (! p_CallSupport_0_presence) | EXISTS p_Measure_45: Measure. (p_Measure_45_presence & ((p_CallSupport_0_time = p_Measure_45_time) & (! EXISTS p_ProvideCompanionship_28: ProvideCompanionship. (p_ProvideCompanionship_28_presence & ((p_ProvideCompanionship_28_time <= (p_CallSupport_0_time + 600)) & ((p_CallSupport_0_time + 0) <= p_ProvideCompanionship_28_time)))))))
Def || L7 || c3 <-> Forall p_CallSupport_0: CallSupport. ( (! p_CallSupport_0_presence) | EXISTS p_Measure_45: Measure. (p_Measure_45_presence & ((p_CallSupport_0_time = p_Measure_45_time) & (! EXISTS p_ProvideCompanionship_28: ProvideCompanionship. (p_ProvideCompanionship_28_presence & ((p_ProvideCompanionship_28_time <= (p_CallSupport_0_time + 600)) & ((p_CallSupport_0_time + 0) <= p_ProvideCompanionship_28_time)))))))
DeriveFact || F3 || c3 || L7 R3
Def || L9 || c5 <-> ((EXISTS p_PatientFallen_14: PatientFallen. (p_PatientFallen_14_presence & ((p_PatientFallen_14_time = 0) & (p_PatientFallen_14_presence <-> PatientFallen_4_presence))) & EXISTS p_ProvideCompanionship_26: ProvideCompanionship. (p_ProvideCompanionship_26_presence & ((p_ProvideCompanionship_26_time = 1) & (p_ProvideCompanionship_26_presence <-> ProvideCompanionship_1_presence))) & EXISTS p_CallSupport_19: CallSupport. (p_CallSupport_19_presence & ((p_CallSupport_19_time = 0) & (p_CallSupport_19_presence <-> CallSupport_2_presence))) & EXISTS p_Measure_39: Measure. (p_Measure_39_presence & ((p_Measure_39_time = 0) & (p_Measure_39_underDressed <-> True) & (p_Measure_39_patientNotDeaf <-> False) & (p_Measure_39_presence <-> Measure_8_presence))) & EXISTS p_Measure_40: Measure. (p_Measure_40_presence & ((p_Measure_40_time = 600) & (p_Measure_40_underDressed <-> False) & (p_Measure_40_patientNotDeaf <-> True) & (p_Measure_40_presence <-> Measure_8_presence))) & EXISTS p_blocked_not_ProvideCompanionship_4: blocked_not_ProvideCompanionship. (p_blocked_not_ProvideCompanionship_4_presence & ((p_blocked_not_ProvideCompanionship_4_time = 0) & (p_blocked_not_ProvideCompanionship_4_end = 600) & (p_blocked_not_ProvideCompanionship_4_presence <-> blocked_not_ProvideCompanionship_1_presence)))) & Forall p_Measure_0: Measure. ( (! p_Measure_0_presence) | Forall p_Measure_42: Measure. ( (! p_Measure_42_presence) | ((! (p_Measure_0_time = p_Measure_42_time)) | ((p_Measure_0_time = p_Measure_42_time) & (p_Measure_0_underDressed <-> p_Measure_42_underDressed) & (p_Measure_0_patientNotDeaf <-> p_Measure_42_patientNotDeaf) & (p_Measure_0_presence <-> p_Measure_42_presence))))))
DeriveFact || F5 || c0 -> (c5) || L9 L1
Def || L14 || c10 <-> (EXISTS p_PatientFallen_14: PatientFallen. (p_PatientFallen_14_presence & ((p_PatientFallen_14_time = 0) & (p_PatientFallen_14_presence <-> PatientFallen_4_presence))) & EXISTS p_ProvideCompanionship_26: ProvideCompanionship. (p_ProvideCompanionship_26_presence & ((p_ProvideCompanionship_26_time = 1) & (p_ProvideCompanionship_26_presence <-> ProvideCompanionship_1_presence))) & EXISTS p_CallSupport_19: CallSupport. (p_CallSupport_19_presence & ((p_CallSupport_19_time = 0) & (p_CallSupport_19_presence <-> CallSupport_2_presence))) & EXISTS p_Measure_39: Measure. (p_Measure_39_presence & ((p_Measure_39_time = 0) & (p_Measure_39_underDressed <-> True) & (p_Measure_39_patientNotDeaf <-> False) & (p_Measure_39_presence <-> Measure_8_presence))) & EXISTS p_Measure_40: Measure. (p_Measure_40_presence & ((p_Measure_40_time = 600) & (p_Measure_40_underDressed <-> False) & (p_Measure_40_patientNotDeaf <-> True) & (p_Measure_40_presence <-> Measure_8_presence))) & EXISTS p_blocked_not_ProvideCompanionship_4: blocked_not_ProvideCompanionship. (p_blocked_not_ProvideCompanionship_4_presence & ((p_blocked_not_ProvideCompanionship_4_time = 0) & (p_blocked_not_ProvideCompanionship_4_end = 600) & (p_blocked_not_ProvideCompanionship_4_presence <-> blocked_not_ProvideCompanionship_1_presence))))
DeriveFact || F12 || c5 -> (c10) || L14 L9
Def || L17 || c13 <-> EXISTS p_ProvideCompanionship_26: ProvideCompanionship. (p_ProvideCompanionship_26_presence & ((p_ProvideCompanionship_26_time = 1) & (p_ProvideCompanionship_26_presence <-> ProvideCompanionship_1_presence)))
Def || L18 || c14 <-> EXISTS p_CallSupport_19: CallSupport. (p_CallSupport_19_presence & ((p_CallSupport_19_time = 0) & (p_CallSupport_19_presence <-> CallSupport_2_presence)))
DeriveFact || F15 || c10 -> (c13) || L17 L14
DeriveFact || F16 || c10 -> (c14) || L18 L14
DeriveLemma || EI L17  [p_ProvideCompanionship_26:ProvideCompanionship<-ProvideCompanionship_1] || L23 || c13 -> (ProvideCompanionship_1_presence & ((ProvideCompanionship_1_time = 1) & (ProvideCompanionship_1_presence <-> ProvideCompanionship_1_presence))) || L17
AddFact || F22 || c19 <-> (ProvideCompanionship_1_presence & ((ProvideCompanionship_1_time = 1) & (ProvideCompanionship_1_presence <-> ProvideCompanionship_1_presence)))
DeriveFact || F23 || c13 -> c19 || F22 L23
DeriveLemma || EI L18  [p_CallSupport_19:CallSupport<-CallSupport_3] || L24 || c14 -> (CallSupport_3_presence & ((CallSupport_3_time = 0) & (CallSupport_3_presence <-> CallSupport_2_presence))) || L18
AddFact || F24 || c20 <-> (CallSupport_3_presence & ((CallSupport_3_time = 0) & (CallSupport_3_presence <-> CallSupport_2_presence)))
DeriveFact || F25 || c14 -> c20 || F24 L24
AddFact || F90 || c68 <-> (! ((CallSupport_3_time + 0) <= ProvideCompanionship_1_time))
UNSAT || F16 F15 F0 F22 F25 F3 F95 F90 F23 F24 F12 F5
Vars || c3:Bool ProvideCompanionship_1_time:Int c19:Bool CallSupport_3_presence:Bool CallSupport_2_presence:Bool c14:Bool c10:Bool c13:Bool ProvideCompanionship_1_presence:Bool c5:Bool c0:Bool c68:Bool CallSupport_3_time:Int c20:Bool
