ForAll(~((x2_s_A21) ^ (empty)))
ForAll(~((tau_A27) ^ (fin)))
ForAll(~((x2_s_A0) ^ (a2_s_A0 | a2_e_A0)))
ForAll(~((l_s_A0 | new) ^ (x2_s_A0 | x2_e_A0)))
ForAll(~((tau_A7) ^ (x2_s_A5 | x2_e_A22)))
ForAll(((manual) | (code_ok)) => Exist(x2_e_A12))
ForAll(~((l_s_A3) ^ (tau_A28)))
ForAll(~((l_s_A5 | release) ^ (x2_e_A10)))
Exist(x2_s_A9)
ForAll(~((x2_s_A19) ^ (l_s_A9 | reopen)))
ForAll(((tau_A17) | (l_s_A6 | code_nok)) => Exist(x2_e_A14))
ForAll(~((x2_s_A15) ^ (tau_A19)))
ForAll(~((tau_A13) ^ (l_s_A5 | release)))
ForAll(~((l_s_A2 | join_pat) ^ (x2_e_A3)))
Exist(l_s_A3 | x3_e_A6)
ForAll((tau_A6) => Exist(join_pat))
ForAll(~((x2_s_A7 | x2_e_A8) ^ (change_end)))
Exist(l_s_A7)
ForAll(((tau_A2) | (l_s_A1 | billed)) => Exist(x2_e_A1))
Exist(x2_s_A3)
ForAll(~((a2_s_A1 | a2_e_A1) ^ (x2_s_A23 | x2_e_A23)))
ForAll((l_s_A7) => Exist(storno | x2_e_A17))
ForAll(~((empty) ^ (x2_e_A21)))
ForAll(~((tau_A9) ^ (set_status)))
ForAll((tau_A12) => Exist(code_error))
ForAll(~(((x2_s_A9 | x2_e_A9) | (x2_s_A10 | x2_e_A13)) ^ (a2_e_A2)))
ForAll(((tau_A13) | (l_s_A5 | release)) => Exist(x2_e_A10))
ForAll((x2_s_A3) => ((Exist(tau_A5) ^ ~(Exist(l_s_A2 | join_pat))) | (~(Exist(tau_A5)) ^ Exist(l_s_A2 | join_pat))))
ForAll((x2_s_A16 | x2_e_A16) => Exist(x2_s_A18 | x2_e_A18))
ForAll(~((x2_s_A9) ^ (l_s_A4 | code_error)))
ForAll(~((x2_s_A2) ^ (a2_s_A1 | x2_e_A23)))
ForAll(~((x2_s_A18) ^ (tau_A24)))
ForAll((a2_s_A1 | a2_e_A1) => Exist(x2_s_A23 | x2_e_A23))
ForAll(((tau_A16) | (a2_s_A3 | a2_e_A3)) => Exist(x2_e_A13))
ForAll(~((tau_A10) ^ (x2_e_A8)))
ForAll(((tau_A4) | (a2_s_A1 | x2_e_A23)) => Exist(x2_e_A2))
Exist(x3_s_A6)
ForAll(~((x2_s_A8) ^ (x2_e_A8)))
ForAll((x2_s_A14 | x2_e_A14) => Exist(a2_e_A3))
ForAll(~((a2_s_A1 | x2_e_A23) ^ (x2_e_A2)))
ForAll(~((tau_A1) ^ (a2_s_A0 | a2_e_A0)))
ForAll(~((l_s_A8) ^ (reject)))
ForAll(~((x2_s_A4) ^ (x2_e_A4)))
Exist(a2_s_A4)
ForAll((x2_s_A13) => ((Exist(tau_A16) ^ ~(Exist(a2_s_A3 | a2_e_A3))) | (~(Exist(tau_A16)) ^ Exist(a2_s_A3 | a2_e_A3))))
ForAll((billed) => ((Exist(tau_A3) ^ Exist(billed)) | (~(Exist(tau_A3)))))
ForAll(~((x2_s_A18) ^ (a2_s_A4 | a2_e_A4)))
ForAll((code_nok) => ((Exist(tau_A18) ^ Exist(code_nok)) | (~(Exist(tau_A18)))))
ForAll((x2_s_A5) => ((Exist(tau_A8) ^ ~(Exist(l_s_A3 | x2_e_A21))) | (~(Exist(tau_A8)) ^ Exist(l_s_A3 | x2_e_A21))))
ForAll(~((x2_s_A3) ^ (tau_A5)))
ForAll(~((tau_A13) ^ (x2_e_A10)))
ForAll(~((tau_A29) ^ (x2_e_A21)))
Exist(x2_s_A16)
ForAll(~((tau_A24) ^ (x2_e_A18)))
ForAll(~((x2_s_A5) ^ (tau_A8)))
ForAll(~((x2_s_A7) ^ (x2_e_A7)))
ForAll(~((x2_s_A7 | x2_e_A8) ^ (x3_e_A6)))
ForAll((a2_s_A3) => (Exist(x2_s_A14 | x2_e_A14) ^ Exist(x2_s_A15 | x2_e_A15)))
ForAll((x2_s_A9) => ((Exist(tau_A11) ^ ~(Exist(l_s_A4 | code_error))) | (~(Exist(tau_A11)) ^ Exist(l_s_A4 | code_error))))
ForAll(~((l_s_A8 | reject) ^ (x2_e_A17)))
ForAll(~((x2_s_A12) ^ (manual)))
ForAll(((tau_A11) | (l_s_A4 | code_error)) => Exist(x2_e_A9))
ForAll((x2_s_A20 | x2_e_A20) => Exist(a2_e_A4))
ForAll((x2_s_A11 | x2_e_A11) => Exist(x2_s_A13 | x2_e_A13))
ForAll(~((tau_A7) ^ (x2_e_A4)))
ForAll(~((x2_s_A10 | x2_e_A10) ^ (x2_s_A13 | x2_e_A13)))
ForAll(~((tau_A17) ^ (x2_e_A14)))
ForAll(~((x2_s_A16 | x2_e_A16) ^ (x2_s_A18 | x2_e_A18)))
ForAll(~((fin) ^ (x2_e_A20)))
ForAll(~((l_s_A3) ^ (x3_s_A6 | x3_e_A6)))
ForAll((x2_s_A20) => ((Exist(tau_A27) ^ ~(Exist(fin))) | (~(Exist(tau_A27)) ^ Exist(fin))))
Exist(l_s_A6)
ForAll(~((x2_s_A19) ^ (x2_e_A19)))
ForAll(~((tau_A5) ^ (x2_e_A3)))
Exist(a2_s_A0)
ForAll(~((tau_A2) ^ (x2_e_A1)))
Exist(x2_s_A11)
ForAll(((tau_A25) | (l_s_A9 | reopen)) => Exist(x2_e_A19))
ForAll((l_s_A5) => Exist(release))
Exist(x2_s_A10 | x2_e_A10)
ForAll(((tau_A32) | (zdbc_behan)) => Exist(x2_e_A23))
ForAll(~((a2_s_A2 | a2_e_A2) ^ (x2_e_A8)))
ForAll(~((tau_A8) ^ (l_s_A3 | x2_e_A21)))
ForAll((tau_A14) => Exist(release))
ForAll(~((code_nok) ^ (tau_A18)))
ForAll((x2_s_A1) => ((Exist(tau_A2) ^ ~(Exist(l_s_A1 | billed))) | (~(Exist(tau_A2)) ^ Exist(l_s_A1 | billed))))
ForAll(~((tau_A16) ^ (a2_s_A3 | a2_e_A3)))
ForAll(~((x2_s_A5 | x2_e_A22) ^ (x2_e_A4)))
Exist(x2_s_A7)
ForAll(((tau_A29) | (empty)) => Exist(x2_e_A21))
ForAll(~((l_s_A9) ^ (reopen)))
ForAll((tau_A0) => Exist(new))
ForAll(~((x2_s_A15) ^ (x2_e_A15)))
ForAll(~((tau_A19) ^ (x2_s_A16 | x2_e_A18)))
Exist(x2_s_A4)
ForAll((x2_s_A17) => ((Exist(tau_A21) ^ ~(Exist(l_s_A8 | reject))) | (~(Exist(tau_A21)) ^ Exist(l_s_A8 | reject))))
ForAll((l_s_A0 | new) => Exist(x2_s_A0 | x2_e_A0))
ForAll(~((x2_s_A21) ^ (x2_e_A21)))
Exist(a2_s_A3)
ForAll(~((x2_s_A4) ^ (tau_A7)))
ForAll(~((l_s_A7) ^ (tau_A23)))
ForAll(~((x2_s_A13) ^ (tau_A16)))
ForAll(((tau_A21) | (l_s_A8 | reject)) => Exist(x2_e_A17))
ForAll(~((x2_s_A12 | x2_e_A12) ^ (x2_e_A11)))
ForAll(~((tau_A30) ^ (x2_e_A22)))
Exist(x2_s_A13)
ForAll(~((code_error) ^ (tau_A12)))
Exist(x2_s_A14)
ForAll((x2_s_A7 | x2_e_A7) => Exist(x2_s_A8 | x2_e_A8))
Exist(x2_s_A23)
ForAll((l_s_A6) => Exist(code_nok))
ForAll(~((x2_s_A10) ^ (l_s_A5 | release)))
ForAll(~((x2_s_A23) ^ (x2_e_A23)))
ForAll(~((x2_s_A13) ^ (x2_e_A13)))
ForAll(~((zdbc_behan) ^ (x2_e_A23)))
ForAll(~((x2_s_A0) ^ (tau_A1)))
ForAll(~((x2_s_A20) ^ (fin)))
ForAll((x2_s_A5 | x2_e_A5) => Exist(x2_s_A22 | x2_e_A22))
ForAll(~((tau_A11) ^ (l_s_A4 | code_error)))
ForAll(~(((x2_s_A1 | x2_e_A1) | (x2_s_A2 | x2_e_A2)) ^ (a2_e_A0)))
ForAll(~((l_s_A0) ^ (tau_A0)))
ForAll(~((l_s_A6) ^ (tau_A18)))
ForAll((tau_A31) => Exist(delete))
Exist(l_s_A2)
ForAll(~((x2_s_A15) ^ (x2_s_A16 | x2_e_A18)))
ForAll((x2_s_A9 | x2_e_A9) => Exist(a2_e_A2))
ForAll(~(((x2_s_A3 | x2_e_A3) | (x2_s_A4 | x2_e_A4)) ^ (a2_e_A1)))
Exist(l_s_A3)
ForAll(~((x2_s_A1) ^ (l_s_A1 | billed)))
ForAll(((x2_s_A7 | x2_e_A8) | (change_end) | (change_diagn)) => Exist(x3_e_A6))
Exist(x2_s_A16 | x2_e_A16)
ForAll((x2_s_A10 | x2_e_A13) => Exist(a2_e_A2))
ForAll((x2_s_A21) => ((Exist(tau_A29) ^ ~(Exist(empty))) | (~(Exist(tau_A29)) ^ Exist(empty))))
ForAll(~((set_status) ^ (x2_e_A7)))
ForAll(~((a2_s_A4) ^ ((x2_s_A19 | x2_e_A19) | (x2_s_A20 | x2_e_A20))))
ForAll((x2_s_A2 | x2_e_A2) => Exist(a2_e_A0))
ForAll((x2_s_A19 | x2_e_A19) => Exist(a2_e_A4))
ForAll(~((x2_s_A14) ^ (tau_A17)))
ForAll((reopen) => ((Exist(tau_A26) ^ Exist(reopen)) | (~(Exist(tau_A26)))))
ForAll(~((x2_s_A12) ^ (x2_e_A12)))
ForAll((storno | x2_e_A17) => ((Exist(tau_A23) ^ Exist(storno | x2_e_A17)) | (~(Exist(tau_A23)))))
ForAll(~((x2_s_A11 | x2_e_A11) ^ (x2_s_A13 | x2_e_A13)))
ForAll((new) => ((Exist(tau_A0) ^ Exist(new)) | (~(Exist(tau_A0)))))
ForAll(((tau_A8) | (l_s_A3 | x2_e_A21)) => Exist(x2_e_A5))
ForAll((tau_A23) => Exist(storno | x2_e_A17))
ForAll((l_s_A0) => Exist(new))
ForAll(((tau_A1) | (a2_s_A0 | a2_e_A0)) => Exist(x2_e_A0))
ForAll((x2_s_A4 | x2_e_A4) => Exist(a2_e_A1))
ForAll(~((change_end) ^ (change_diagn)))
ForAll(~((l_s_A10) ^ (tau_A31)))
Exist(l_s_A5)
ForAll(~((l_s_A6) ^ (code_nok)))
ForAll((x2_s_A14) => ((Exist(tau_A17) ^ ~(Exist(l_s_A6 | code_nok))) | (~(Exist(tau_A17)) ^ Exist(l_s_A6 | code_nok))))
ForAll(~((storno | x2_e_A17) ^ (tau_A23)))
ForAll((x2_s_A22) => ((Exist(tau_A30) ^ ~(Exist(l_s_A10 | delete))) | (~(Exist(tau_A30)) ^ Exist(l_s_A10 | delete))))
Exist(x2_s_A10)
Exist(x2_s_A5)
ForAll(~((l_s_A7) ^ (storno | x2_e_A17)))
ForAll(~((a2_s_A1) ^ ((x2_s_A3 | x2_e_A3) | (x2_s_A4 | x2_e_A4))))
ForAll((x2_s_A18) => ((Exist(tau_A24) ^ ~(Exist(a2_s_A4 | a2_e_A4))) | (~(Exist(tau_A24)) ^ Exist(a2_s_A4 | a2_e_A4))))
ForAll(~((x2_s_A21) ^ (tau_A29)))
ForAll(~((change_end) ^ (x3_e_A6)))
ForAll(~((x2_s_A14) ^ (x2_e_A14)))
ForAll(~((l_s_A5) ^ (tau_A14)))
ForAll(~((tau_A2) ^ (l_s_A1 | billed)))
ForAll((tau_A22) => Exist(reject))
ForAll((a2_s_A2) => (Exist(x2_s_A9 | x2_e_A9) ^ Exist(x2_s_A10 | x2_e_A13)))
ForAll((x2_s_A7) => ((Exist(tau_A9) ^ ~(Exist(set_status))) | (~(Exist(tau_A9)) ^ Exist(set_status))))
ForAll(~((x2_s_A10) ^ (x2_e_A10)))
ForAll(~((l_s_A4 | code_error) ^ (x2_e_A9)))
ForAll(~((x2_s_A11) ^ (x2_s_A12 | x2_e_A12)))
ForAll(~((tau_A9) ^ (x2_e_A7)))
ForAll(~((x2_s_A8) ^ (a2_s_A2 | a2_e_A2)))
ForAll(~((x2_s_A3) ^ (x2_e_A3)))
Exist(x2_s_A5 | x2_e_A5)
ForAll(~((billed) ^ (tau_A3)))
ForAll(~((tau_A19) ^ (x2_e_A15)))
Exist(x2_s_A19)
ForAll(~((x2_s_A4) ^ (x2_s_A5 | x2_e_A22)))
ForAll(~((x2_s_A9) ^ (x2_e_A9)))
ForAll((reject) => ((Exist(tau_A22) ^ Exist(reject)) | (~(Exist(tau_A22)))))
ForAll(~((x2_s_A16) ^ (l_s_A7 | x2_e_A17)))
ForAll(~((tau_A29) ^ (empty)))
ForAll(~((l_s_A2) ^ (tau_A6)))
ForAll((tau_A18) => Exist(code_nok))
Exist(l_s_A0 | new)
ForAll(~((x2_s_A13) ^ (a2_s_A3 | a2_e_A3)))
ForAll(~((l_s_A5) ^ (release)))
ForAll(~((delete) ^ (tau_A31)))
ForAll(~((tau_A21) ^ (l_s_A8 | reject)))
ForAll(~((storno) ^ (x2_s_A17 | x2_e_A17)))
ForAll(~((l_s_A10) ^ (delete)))
Exist(l_s_A9)
ForAll((storno) => Exist(x2_s_A17 | x2_e_A17))
ForAll(~((x2_s_A11) ^ (tau_A15)))
ForAll((x2_s_A15) => ((Exist(tau_A19) ^ ~(Exist(x2_s_A16 | x2_e_A18))) | (~(Exist(tau_A19)) ^ Exist(x2_s_A16 | x2_e_A18))))
ForAll(~((x2_s_A12) ^ (code_ok)))
ForAll((x2_s_A2) => ((Exist(tau_A4) ^ ~(Exist(a2_s_A1 | x2_e_A23))) | (~(Exist(tau_A4)) ^ Exist(a2_s_A1 | x2_e_A23))))
ForAll(~((x2_s_A7 | x2_e_A8) ^ (change_diagn)))
ForAll(~((x2_s_A14) ^ (l_s_A6 | code_nok)))
ForAll(~((x2_s_A7 | x2_e_A7) ^ (x2_s_A8 | x2_e_A8)))
Exist(x2_s_A1)
ForAll(~((x2_s_A22) ^ (l_s_A10 | delete)))
Exist(x2_s_A2)
ForAll(~((x2_s_A3) ^ (l_s_A2 | join_pat)))
ForAll((x2_s_A8) => ((Exist(tau_A10) ^ ~(Exist(a2_s_A2 | a2_e_A2))) | (~(Exist(tau_A10)) ^ Exist(a2_s_A2 | a2_e_A2))))
ForAll(~((a2_s_A2) ^ ((x2_s_A9 | x2_e_A9) | (x2_s_A10 | x2_e_A13))))
ForAll((l_s_A2) => Exist(join_pat))
ForAll((x2_s_A19) => ((Exist(tau_A25) ^ ~(Exist(l_s_A9 | reopen))) | (~(Exist(tau_A25)) ^ Exist(l_s_A9 | reopen))))
Exist(x2_s_A22)
ForAll((code_error) => ((Exist(tau_A12) ^ Exist(code_error)) | (~(Exist(tau_A12)))))
Exist(x2_s_A20)
ForAll(~((code_ok) ^ (x2_e_A12)))
ForAll(~((x2_s_A23) ^ (zdbc_behan)))
ForAll(~((x3_s_A6) ^ (change_end)))
ForAll(((tau_A20) | (l_s_A7 | x2_e_A17)) => Exist(x2_e_A16))
ForAll(~((reopen) ^ (tau_A26)))
ForAll(~((x2_s_A9) ^ (tau_A11)))
ForAll((l_s_A9) => Exist(reopen))
ForAll(~((x2_s_A10 | x2_e_A10) ^ (x2_s_A11 | x2_e_A11)))
Exist(x2_s_A8)
ForAll((x2_s_A15 | x2_e_A15) => Exist(a2_e_A3))
ForAll(~((l_s_A4) ^ (code_error)))
ForAll(~((tau_A4) ^ (x2_e_A2)))
ForAll(~((x3_s_A6) ^ (x3_e_A6)))
ForAll(~((x2_s_A17) ^ (tau_A21)))
ForAll((x2_s_A4) => ((Exist(tau_A7) ^ ~(Exist(x2_s_A5 | x2_e_A22))) | (~(Exist(tau_A7)) ^ Exist(x2_s_A5 | x2_e_A22))))
Exist(x2_s_A18)
ForAll(~((a2_s_A4 | a2_e_A4) ^ (x2_e_A18)))
ForAll((release) => ((Exist(tau_A14) ^ Exist(release)) | (~(Exist(tau_A14)))))
ForAll(~((x2_s_A8) ^ (tau_A10)))
ForAll(((tau_A24) | (a2_s_A4 | a2_e_A4)) => Exist(x2_e_A18))
ForAll(~((tau_A32) ^ (zdbc_behan)))
ForAll(~((a2_s_A0) ^ ((x2_s_A1 | x2_e_A1) | (x2_s_A2 | x2_e_A2))))
ForAll(~((l_s_A3 | x2_e_A21) ^ (x2_e_A5)))
ForAll(~((x2_s_A18) ^ (x2_e_A18)))
ForAll(~((x2_s_A1) ^ (x2_e_A1)))
ForAll((l_s_A1) => Exist(billed))
ForAll(~((tau_A25) ^ (x2_e_A19)))
ForAll(~((tau_A30) ^ (l_s_A10 | delete)))
ForAll((join_pat) => ((Exist(tau_A6) ^ Exist(join_pat)) | (~(Exist(tau_A6)))))
ForAll(((tau_A5) | (l_s_A2 | join_pat)) => Exist(x2_e_A3))
ForAll(~((x2_s_A2) ^ (tau_A4)))
ForAll(~((x2_s_A2) ^ (x2_e_A2)))
ForAll(~((x2_s_A5 | x2_e_A5) ^ (x2_s_A22 | x2_e_A22)))
ForAll(~((tau_A17) ^ (l_s_A6 | code_nok)))
ForAll((l_s_A10) => Exist(delete))
ForAll(~((tau_A8) ^ (x2_e_A5)))
ForAll(((tau_A9) | (set_status)) => Exist(x2_e_A7))
ForAll((x3_s_A6 | x3_e_A6) => ((Exist(tau_A28) ^ Exist(x3_s_A6 | x3_e_A6)) | (~(Exist(tau_A28)))))
Exist(x2_s_A21)
ForAll(~((tau_A4) ^ (a2_s_A1 | x2_e_A23)))
ForAll(~((x3_s_A6) ^ (x2_s_A7 | x2_e_A8)))
ForAll(~((x2_s_A17) ^ (l_s_A8 | reject)))
ForAll(~((x2_s_A17) ^ (x2_e_A17)))
ForAll(~((manual) ^ (code_ok)))
ForAll(~((l_s_A2) ^ (join_pat)))
ForAll(~((l_s_A1) ^ (billed)))
ForAll(~((x2_s_A5) ^ (x2_e_A5)))
ForAll((x2_s_A1 | x2_e_A1) => Exist(a2_e_A0))
ForAll((l_s_A3) => Exist(x3_s_A6 | x3_e_A6))
ForAll((tau_A3) => Exist(billed))
Exist(x2_s_A15)
ForAll(~((tau_A16) ^ (x2_e_A13)))
ForAll(~((release) ^ (tau_A14)))
ForAll((l_s_A8) => Exist(reject))
Exist(x2_s_A12)
Exist(l_s_A4)
ForAll((a2_s_A1) => (Exist(x2_s_A3 | x2_e_A3) ^ Exist(x2_s_A4 | x2_e_A4)))
ForAll(~((x3_s_A6) ^ (change_diagn)))
ForAll(~((l_s_A10 | delete) ^ (x2_e_A22)))
ForAll(~(((x2_s_A19 | x2_e_A19) | (x2_s_A20 | x2_e_A20)) ^ (a2_e_A4)))
ForAll((x2_s_A11) => ((Exist(tau_A15) ^ ~(Exist(x2_s_A12 | x2_e_A12))) | (~(Exist(tau_A15)) ^ Exist(x2_s_A12 | x2_e_A12))))
ForAll(~((x2_s_A16) ^ (x2_e_A16)))
ForAll(~((tau_A32) ^ (x2_e_A23)))
ForAll(~((l_s_A4) ^ (tau_A12)))
ForAll((x2_s_A10 | x2_e_A10) => Exist(x2_s_A11 | x2_e_A11))
ForAll((l_s_A4) => Exist(code_error))
ForAll(~((change_diagn) ^ (x3_e_A6)))
ForAll(~((tau_A15) ^ (x2_e_A11)))
ForAll((l_s_A3 | x3_e_A6) => Exist(x2_s_A21 | x2_e_A21))
ForAll(~((x2_s_A22) ^ (tau_A30)))
ForAll(~((x2_s_A0) ^ (x2_e_A0)))
ForAll(~(((x2_s_A14 | x2_e_A14) | (x2_s_A15 | x2_e_A15)) ^ (a2_e_A3)))
Exist(x2_s_A7 | x2_e_A7)
ForAll(~((x2_s_A7) ^ (tau_A9)))
ForAll(~((tau_A24) ^ (a2_s_A4 | a2_e_A4)))
ForAll((delete) => ((Exist(tau_A31) ^ Exist(delete)) | (~(Exist(tau_A31)))))
ForAll((tau_A28) => Exist(x3_s_A6 | x3_e_A6))
ForAll(~((tau_A25) ^ (l_s_A9 | reopen)))
ForAll(~((x2_s_A16 | x2_e_A18) ^ (x2_e_A15)))
ForAll(~((a2_s_A3 | a2_e_A3) ^ (x2_e_A13)))
ForAll(~((tau_A1) ^ (x2_e_A0)))
Exist(a2_s_A1)
ForAll(~((x2_s_A16) ^ (tau_A20)))
ForAll(((tau_A30) | (l_s_A10 | delete)) => Exist(x2_e_A22))
ForAll((x2_s_A23) => ((Exist(tau_A32) ^ ~(Exist(zdbc_behan))) | (~(Exist(tau_A32)) ^ Exist(zdbc_behan))))
ForAll(((tau_A27) | (fin)) => Exist(x2_e_A20))
Exist(l_s_A1)
ForAll((x3_s_A6) => ((Exist(x2_s_A7 | x2_e_A8) ^ ~(Exist(change_end)) ^ ~(Exist(change_diagn))) | ((~(Exist(x2_s_A7 | x2_e_A8)) ^ Exist(change_end) ^ ~(Exist(change_diagn))) | (~(Exist(x2_s_A7 | x2_e_A8)) ^ ~(Exist(change_end)) ^ Exist(change_diagn)))))
Exist(l_s_A8)
Exist(a2_s_A2)
Exist(x2_s_A17)
ForAll(~((new) ^ (tau_A0)))
ForAll(~((x2_s_A1) ^ (tau_A2)))
ForAll(~((x2_s_A5) ^ (l_s_A3 | x2_e_A21)))
ForAll(((tau_A7) | (x2_s_A5 | x2_e_A22)) => Exist(x2_e_A4))
ForAll(~((x2_s_A20) ^ (x2_e_A20)))
Exist(l_s_A0)
ForAll(~((x2_s_A22) ^ (x2_e_A22)))
ForAll(~((x2_s_A11) ^ (x2_e_A11)))
ForAll((x2_s_A3 | x2_e_A3) => Exist(a2_e_A1))
ForAll(~((tau_A10) ^ (a2_s_A2 | a2_e_A2)))
ForAll((tau_A26) => Exist(reopen))
ForAll(~((l_s_A7 | x2_e_A17) ^ (x2_e_A16)))
ForAll(~((l_s_A0) ^ (new)))
ForAll(~((a2_s_A0 | a2_e_A0) ^ (x2_e_A0)))
ForAll(((tau_A19) | (x2_s_A16 | x2_e_A18)) => Exist(x2_e_A15))
ForAll(~((x2_s_A7) ^ (set_status)))
Exist(x2_s_A0)
ForAll(~((l_s_A8) ^ (tau_A22)))
ForAll(~((x2_s_A20) ^ (tau_A27)))
ForAll((x2_s_A12) => ((Exist(manual) ^ ~(Exist(code_ok))) | (~(Exist(manual)) ^ Exist(code_ok))))
ForAll(~((manual) ^ (x2_e_A12)))
ForAll(~((reject) ^ (tau_A22)))
ForAll(~((l_s_A9 | reopen) ^ (x2_e_A19)))
ForAll((x2_s_A16) => ((Exist(tau_A20) ^ ~(Exist(l_s_A7 | x2_e_A17))) | (~(Exist(tau_A20)) ^ Exist(l_s_A7 | x2_e_A17))))
ForAll(~((tau_A21) ^ (x2_e_A17)))
ForAll(~((x2_s_A19) ^ (tau_A25)))
ForAll(~((tau_A11) ^ (x2_e_A9)))
ForAll(~((l_s_A6 | code_nok) ^ (x2_e_A14)))
ForAll(~((tau_A20) ^ (l_s_A7 | x2_e_A17)))
ForAll(((tau_A15) | (x2_s_A12 | x2_e_A12)) => Exist(x2_e_A11))
Exist(l_s_A10)
ForAll((a2_s_A4) => (Exist(x2_s_A19 | x2_e_A19) ^ Exist(x2_s_A20 | x2_e_A20)))
ForAll((a2_s_A0) => (Exist(x2_s_A1 | x2_e_A1) ^ Exist(x2_s_A2 | x2_e_A2)))
ForAll(~((x2_s_A23) ^ (tau_A32)))
ForAll(~((tau_A20) ^ (x2_e_A16)))
ForAll((x2_s_A10) => ((Exist(tau_A13) ^ ~(Exist(l_s_A5 | release))) | (~(Exist(tau_A13)) ^ Exist(l_s_A5 | release))))
Exist(a2_s_A1 | a2_e_A1)
ForAll(~((l_s_A9) ^ (tau_A26)))
ForAll(~((tau_A15) ^ (x2_s_A12 | x2_e_A12)))
ForAll(~((x2_s_A10) ^ (tau_A13)))
Exist(storno)
ForAll(~((join_pat) ^ (tau_A6)))
ForAll(~((l_s_A1) ^ (tau_A3)))
ForAll(~((x3_s_A6 | x3_e_A6) ^ (tau_A28)))
ForAll(~((tau_A5) ^ (l_s_A2 | join_pat)))
ForAll(~((a2_s_A3) ^ ((x2_s_A14 | x2_e_A14) | (x2_s_A15 | x2_e_A15))))
ForAll(~((l_s_A3 | x3_e_A6) ^ (x2_s_A21 | x2_e_A21)))
ForAll((x2_s_A0) => ((Exist(tau_A1) ^ ~(Exist(a2_s_A0 | a2_e_A0))) | (~(Exist(tau_A1)) ^ Exist(a2_s_A0 | a2_e_A0))))
ForAll(((tau_A10) | (a2_s_A2 | a2_e_A2)) => Exist(x2_e_A8))
ForAll(~((tau_A27) ^ (x2_e_A20)))
ForAll(~((l_s_A1 | billed) ^ (x2_e_A1)))