{res_axiomes = [(`Forall ([("x839", `Unknown);], (`Disjunction [(`Negation
  `True);(`Disjunction [`False;(`Predicate ("AOUT", [(`Unknown, (`Variable
  "x839"));]));(`Predicate ("aNullIn", [(`Unknown, (`Variable
  "x839"));]));(`Predicate ("AbWorld", [(`Unknown, (`Variable
  "x839"));]));(`Predicate ("TransferDetails", [(`Unknown, (`Variable
  "x839"));]));(`Predicate ("Purse", [(`Unknown, (`Variable
  "x839"));]));(`Predicate ("Coin", [(`Unknown, (`Variable
  "x839"));]));]);]))); 
(`Forall ([("x838", `Unknown);("x837", `Unknown);], (`Disjunction
  [(`Negation (`Predicate ("from", [(`Unknown, (`Variable
    "x838"));(`Unknown, (`Variable "x837"));])));(`Conjunction [(`Predicate
    ("Purse", [(`Unknown, (`Variable "x837"));]));(`Predicate
    ("TransferDetails", [(`Unknown, (`Variable "x838"));]));]);]))); 
(`Forall ([("x836", `Unknown);("x835", `Unknown);], (`Disjunction
  [(`Negation (`Predicate ("to", [(`Unknown, (`Variable "x836"));(`Unknown,
  (`Variable "x835"));])));(`Conjunction [(`Predicate ("Purse", [(`Unknown,
  (`Variable "x835"));]));(`Predicate ("TransferDetails", [(`Unknown,
  (`Variable "x836"));]));]);]))); 
(`Forall ([("x834", `Unknown);("x833", `Unknown);], (`Disjunction
  [(`Negation (`Predicate ("value", [(`Unknown, (`Variable
    "x834"));(`Unknown, (`Variable "x833"));])));(`Conjunction [(`Predicate
    ("Coin", [(`Unknown, (`Variable "x833"));]));(`Predicate
    ("TransferDetails", [(`Unknown, (`Variable "x834"));]));]);]))); 
(`Forall ([("x832", `Unknown);("x831", `Unknown);], (`Disjunction
  [(`Negation (`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x832"));(`Unknown, (`Variable "x831"));])));(`Conjunction [(`Predicate
    ("AbPurse", [(`Unknown, (`Variable "x831"));]));(`Predicate ("AbWorld",
  [(`Unknown, (`Variable "x832"));]));]);]))); 
(`Forall ([("x830", `Unknown);("x829", `Unknown);("x828", `Unknown);],
(`Disjunction [(`Negation (`Predicate ("abBalance", [(`Unknown, (`Variable
  "x830"));(`Unknown, (`Variable "x829"));(`Unknown, (`Variable
  "x828"));])));(`Conjunction [(`Predicate ("AbWorld", [(`Unknown,
(`Variable "x828"));]));(`Predicate ("Coin", [(`Unknown, (`Variable
  "x829"));]));(`Predicate ("AbPurse", [(`Unknown, (`Variable
  "x830"));]));]);]))); 
(`Forall ([("x827", `Unknown);("x826", `Unknown);("x825", `Unknown);],
(`Disjunction [(`Negation (`Predicate ("abLost", [(`Unknown, (`Variable
  "x827"));(`Unknown, (`Variable "x826"));(`Unknown, (`Variable
  "x825"));])));(`Conjunction [(`Predicate ("AbWorld", [(`Unknown,
(`Variable "x825"));]));(`Predicate ("Coin", [(`Unknown, (`Variable
  "x826"));]));(`Predicate ("AbPurse", [(`Unknown, (`Variable
  "x827"));]));]);]))); 
(`Negation (`Exists ([("x824", `Unknown);], (`Conjunction [(`Disjunction
  [(`Disjunction [(`Disjunction [(`Disjunction [(`Predicate ("AOUT",
  [(`Unknown, (`Variable "x824"));]));(`Predicate ("aNullIn", [(`Unknown,
  (`Variable "x824"));]));]);(`Predicate ("AbWorld", [(`Unknown, (`Variable
    "x824"));]));]);(`Predicate ("TransferDetails", [(`Unknown, (`Variable
    "x824"));]));]);(`Predicate ("Purse", [(`Unknown, (`Variable
    "x824"));]));]);(`Predicate ("Coin", [(`Unknown, (`Variable
  "x824"));]));])))); 
(`Negation (`Exists ([("x823", `Unknown);], (`Conjunction [(`Disjunction
  [(`Disjunction [(`Disjunction [(`Predicate ("AOUT", [(`Unknown,
  (`Variable "x823"));]));(`Predicate ("aNullIn", [(`Unknown, (`Variable
    "x823"));]));]);(`Predicate ("AbWorld", [(`Unknown, (`Variable
    "x823"));]));]);(`Predicate ("TransferDetails", [(`Unknown, (`Variable
    "x823"));]));]);(`Predicate ("Purse", [(`Unknown, (`Variable
  "x823"));]));])))); 
(`Negation (`Exists ([("x822", `Unknown);], (`Conjunction [(`Disjunction
  [(`Disjunction [(`Predicate ("AOUT", [(`Unknown, (`Variable
    "x822"));]));(`Predicate ("aNullIn", [(`Unknown, (`Variable
    "x822"));]));]);(`Predicate ("AbWorld", [(`Unknown, (`Variable
    "x822"));]));]);(`Predicate ("TransferDetails", [(`Unknown, (`Variable
  "x822"));]));])))); 
(`Negation (`Exists ([("x821", `Unknown);], (`Conjunction [(`Disjunction
  [(`Predicate ("AOUT", [(`Unknown, (`Variable "x821"));]));(`Predicate
    ("aNullIn", [(`Unknown, (`Variable "x821"));]));]);(`Predicate
  ("AbWorld", [(`Unknown, (`Variable "x821"));]));])))); 
(`Negation (`Exists ([("x820", `Unknown);], (`Conjunction [(`Predicate
  ("AOUT", [(`Unknown, (`Variable "x820"));]));(`Predicate ("aNullIn",
[(`Unknown, (`Variable "x820"));]));])))); 
(`Forall ([("x819", `Unknown);], (`Disjunction [(`Negation (`Predicate
  ("AOUT", [(`Unknown, (`Variable "x819"));])));(`Disjunction
  [`False;(`Predicate ("aNullOut", [(`Unknown, (`Variable
    "x819"));]));]);]))); 
(`Conjunction [(`Conjunction [(`Exists ([("x21", `Unknown);], (`Predicate
  ("aNullOut", [(`Unknown, (`Variable "x21"));]))));(`Forall ([("x19",
`Unknown);("x20", `Unknown);], (`Disjunction [(`Negation (`Conjunction
  [(`Predicate ("aNullOut", [(`Unknown, (`Variable "x19"));]));(`Predicate
    ("aNullOut", [(`Unknown, (`Variable "x20"));]));]));(`Conjunction
  [(`Equality ((`Unknown, (`Variable "x19")), (`Unknown, (`Variable
    "x20"))));]);])));]);]); 
(`Forall ([("x18", `Unknown);], (`Disjunction [(`Negation (`Predicate
  ("aNullOut", [(`Unknown, (`Variable "x18"));])));(`Predicate ("AOUT",
[(`Unknown, (`Variable "x18"));]));]))); 
(`Conjunction [(`Conjunction [(`Exists ([("x17", `Unknown);], (`Predicate
  ("aNullIn", [(`Unknown, (`Variable "x17"));]))));(`Forall ([("x15",
`Unknown);("x16", `Unknown);], (`Disjunction [(`Negation (`Conjunction
  [(`Predicate ("aNullIn", [(`Unknown, (`Variable "x15"));]));(`Predicate
    ("aNullIn", [(`Unknown, (`Variable "x16"));]));]));(`Conjunction
  [(`Equality ((`Unknown, (`Variable "x15")), (`Unknown, (`Variable
    "x16"))));]);])));]);(`Conjunction [(`Forall ([("x14", `Unknown);],
(`Disjunction [(`Negation (`Predicate ("AIN", [(`Unknown, (`Variable
  "x14"));])));(`Disjunction [(`Predicate ("aNullIn", [(`Unknown,
(`Variable "x14"));]));(`Predicate ("TransferDetails", [(`Unknown,
(`Variable "x14"));]));]);])));(`Forall ([("x13", `Unknown);],
(`Disjunction [(`Negation (`Disjunction [(`Predicate ("aNullIn",
[(`Unknown, (`Variable "x13"));]));(`Predicate ("TransferDetails",
[(`Unknown, (`Variable "x13"));]));]));(`Predicate ("AIN", [(`Unknown,
(`Variable "x13"));]));])));]);]); 
(`Forall ([("x12", `Unknown);], (`Disjunction [(`Negation (`Predicate
  ("AIN", [(`Unknown, (`Variable "x12"));])));(`Disjunction [(`Predicate
  ("aNullIn", [(`Unknown, (`Variable "x12"));]));(`Predicate
  ("TransferDetails", [(`Unknown, (`Variable "x12"));]));]);]))); 
(`Forall ([("x11", `Unknown);], (`Disjunction [(`Negation (`Predicate
  ("AbPurse", [(`Unknown, (`Variable "x11"));])));(`Predicate ("Purse",
[(`Unknown, (`Variable "x11"));]));]))); 
(`Conjunction [(`Forall ([("x8", `Unknown);], (`Disjunction [(`Negation
  (`Predicate ("TransferDetails", [(`Unknown, (`Variable
    "x8"));])));(`Forall ([("x9", `Unknown);("x10", `Unknown);],
(`Disjunction [(`Negation (`Conjunction [(`Predicate ("to", [(`Unknown,
(`Variable "x8"));(`Unknown, (`Variable "x9"));]));(`Predicate ("to",
[(`Unknown, (`Variable "x8"));(`Unknown, (`Variable
  "x10"));]));]));(`Conjunction [(`Equality ((`Unknown, (`Variable "x9")),
(`Unknown, (`Variable "x10"))));]);])));])));(`Forall ([("x6", `Unknown);],
(`Disjunction [(`Negation (`Predicate ("TransferDetails", [(`Unknown,
(`Variable "x6"));])));(`Exists ([("x7", `Unknown);], (`Predicate ("to",
[(`Unknown, (`Variable "x6"));(`Unknown, (`Variable "x7"));]))));])));]); 
(`Conjunction [(`Forall ([("x3", `Unknown);], (`Disjunction [(`Negation
  (`Predicate ("TransferDetails", [(`Unknown, (`Variable
    "x3"));])));(`Forall ([("x4", `Unknown);("x5", `Unknown);], 
(`Disjunction [(`Negation (`Conjunction [(`Predicate ("from", [(`Unknown,
(`Variable "x3"));(`Unknown, (`Variable "x4"));]));(`Predicate ("from",
[(`Unknown, (`Variable "x3"));(`Unknown, (`Variable
  "x5"));]));]));(`Conjunction [(`Equality ((`Unknown, (`Variable "x4")),
(`Unknown, (`Variable "x5"))));]);])));])));(`Forall ([("x1", `Unknown);],
(`Disjunction [(`Negation (`Predicate ("TransferDetails", [(`Unknown,
(`Variable "x1"));])));(`Exists ([("x2", `Unknown);], (`Predicate ("from",
[(`Unknown, (`Variable "x1"));(`Unknown, (`Variable "x2"));]))));])));]); 
];

res_theoremes = [("AbTransfer_inv",(`Conjunction [(`Forall ([("a",
`Unknown);("a'", `Unknown);("a_in", `Unknown);("a_out", `Unknown);],
(`Disjunction [(`Negation (`Conjunction [(`Predicate ("AbWorld",
[(`Unknown, (`Variable "a"));]));(`Predicate ("AbWorld", [(`Unknown,
(`Variable "a'"));]));(`Predicate ("AIN", [(`Unknown, (`Variable
  "a_in"));]));(`Predicate ("AOUT", [(`Unknown, (`Variable
  "a_out"));]));]));(`Disjunction [(`Negation (`Conjunction [(`Conjunction
  [(`Negation (`Exists ([("x818", `Unknown);], (`Conjunction [(`Exists
    ([("x817", `Unknown);], (`Conjunction [(`Exists ([("x816", `Unknown);],
    (`Conjunction [(`Exists ([("x815", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x815")), (`Unknown, (`Variable
        "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x815"));(`Unknown, (`Variable "x816"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x816"));(`Unknown, (`Variable
        "x818"));(`Unknown, (`Variable "x817"));]));])));(`Equality
      ((`Unknown, (`Variable "x817")), (`Unknown, (`Variable
        "a"))));])));(`Exists ([("x814", `Unknown);], (`Conjunction
    [(`Exists ([("x813", `Unknown);], (`Conjunction [(`Exists ([("x812",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x812")),
    (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x812"));(`Unknown, (`Variable "x813"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x813"));(`Unknown, (`Variable
        "x818"));(`Unknown, (`Variable "x814"));]));])));(`Equality
      ((`Unknown, (`Variable "x814")), (`Unknown, (`Variable
        "a"))));])));]))));(`Forall ([("c", `Unknown);], (`Disjunction
    [(`Negation (`Conjunction [(`Predicate ("Coin", [(`Unknown, (`Variable
      "c"));]));]));(`Forall ([("x808", `Unknown);("x809", `Unknown);],
    (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
      ([("x807", `Unknown);], (`Conjunction [(`Exists ([("x811",
      `Unknown);], (`Conjunction [(`Disjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x808"));(`Unknown, (`Variable
        "x807"));(`Unknown, (`Variable "x811"));]));(`Predicate ("abLost",
      [(`Unknown, (`Variable "x808"));(`Unknown, (`Variable
        "x807"));(`Unknown, (`Variable "x811"));]));]);(`Equality
        ((`Unknown, (`Variable "x811")), (`Unknown, (`Variable
          "a"))));])));(`Equality ((`Unknown, (`Variable "x807")),
      (`Unknown, (`Variable "c"))));])));(`Exists ([("x805", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x805")), (`Unknown,
    (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x805"));(`Unknown, (`Variable "x808"));]));])));]);(`Conjunction
      [(`Exists ([("x807", `Unknown);], (`Conjunction [(`Exists ([("x810",
      `Unknown);], (`Conjunction [(`Disjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x809"));(`Unknown, (`Variable
        "x807"));(`Unknown, (`Variable "x810"));]));(`Predicate ("abLost",
      [(`Unknown, (`Variable "x809"));(`Unknown, (`Variable
        "x807"));(`Unknown, (`Variable "x810"));]));]);(`Equality
        ((`Unknown, (`Variable "x810")), (`Unknown, (`Variable
          "a"))));])));(`Equality ((`Unknown, (`Variable "x807")),
      (`Unknown, (`Variable "c"))));])));(`Exists ([("x805", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x805")), (`Unknown,
      (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x805"));(`Unknown, (`Variable
        "x809"));]));])));]);]));(`Conjunction [(`Equality ((`Unknown,
    (`Variable "x808")), (`Unknown, (`Variable
      "x809"))));]);])));])));]);(`Conjunction [(`Disjunction
  [(`Conjunction [(`Conjunction [(`Conjunction [(`Conjunction [(`Forall
    ([("x804", `Unknown);], (`Disjunction [(`Negation (`Equality
      ((`Unknown, (`Variable "x804")), (`Unknown, (`Variable
        "a_out")))));(`Predicate ("aNullOut", [(`Unknown, (`Variable
      "x804"));]));])));(`Forall ([("x803", `Unknown);], (`Disjunction
    [(`Negation (`Predicate ("aNullOut", [(`Unknown, (`Variable
      "x803"));])));(`Equality ((`Unknown, (`Variable "x803")), (`Unknown,
    (`Variable "a_out"))));])));]);]);(`Forall ([("x802", `Unknown);],
  (`Disjunction [(`Negation (`Equality ((`Unknown, (`Variable "x802")),
  (`Unknown, (`Variable "a_in")))));(`Predicate ("TransferDetails",
  [(`Unknown, (`Variable "x802"));]));])));(`Conjunction [(`Forall
    ([("x801", `Unknown);], (`Disjunction [(`Negation (`Conjunction
      [(`Conjunction [(`Exists ([("x799", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x799")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x799"));(`Unknown, (`Variable "x801"));]));])));(`Negation
        (`Exists ([("x798", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x798")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x798"));(`Unknown, (`Variable "x801"));]));]))));]);(`Negation
        (`Exists ([("x797", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x797")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x797"));(`Unknown, (`Variable
          "x801"));]));]))));]));(`Conjunction [(`Conjunction [(`Exists
      ([("x796", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x796")), (`Unknown, (`Variable "a'"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x796"));(`Unknown,
        (`Variable "x801"));]));])));(`Negation (`Exists ([("x795",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x795")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x795"));(`Unknown, (`Variable
      "x801"));]));]))));]);(`Negation (`Exists ([("x794", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x794")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x794"));(`Unknown, (`Variable "x801"));]));]))));]);])));(`Forall
    ([("x800", `Unknown);], (`Disjunction [(`Negation (`Conjunction
      [(`Conjunction [(`Exists ([("x796", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x796")), (`Unknown, (`Variable
          "a'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x796"));(`Unknown, (`Variable "x800"));]));])));(`Negation
        (`Exists ([("x795", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x795")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x795"));(`Unknown, (`Variable "x800"));]));]))));]);(`Negation
        (`Exists ([("x794", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x794")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x794"));(`Unknown, (`Variable
          "x800"));]));]))));]));(`Conjunction [(`Conjunction [(`Exists
      ([("x799", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x799")), (`Unknown, (`Variable "a"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x799"));(`Unknown,
        (`Variable "x800"));]));])));(`Negation (`Exists ([("x798",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x798")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x798"));(`Unknown, (`Variable
      "x800"));]));]))));]);(`Negation (`Exists ([("x797", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x797")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x797"));(`Unknown, (`Variable
      "x800"));]));]))));]);])));]);(`Conjunction [(`Conjunction [(`Forall
    ([("x793", `Unknown);("x790", `Unknown);], (`Disjunction [(`Negation
      (`Conjunction [(`Conjunction [(`Conjunction [(`Exists ([("x773",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x773")), (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse",
      [(`Unknown, (`Variable "x773"));(`Unknown, (`Variable
        "x790"));]));])));(`Negation (`Exists ([("x772", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x772")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x772"));(`Unknown, (`Variable "x790"));]));]))));]);(`Negation
        (`Exists ([("x771", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x771")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x771"));(`Unknown, (`Variable "x790"));]));]))));]);(`Exists
        ([("x792", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
        [(`Unknown, (`Variable "x790"));(`Unknown, (`Variable
          "x793"));(`Unknown, (`Variable "x792"));]));(`Equality
          ((`Unknown, (`Variable "x792")), (`Unknown, (`Variable
            "a"))));])));]));(`Conjunction [(`Conjunction [(`Conjunction
      [(`Exists ([("x773", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x773")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x773"));(`Unknown, (`Variable "x790"));]));])));(`Negation
        (`Exists ([("x772", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x772")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x772"));(`Unknown, (`Variable "x790"));]));]))));]);(`Negation
      (`Exists ([("x771", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x771")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x771"));(`Unknown, (`Variable "x790"));]));]))));]);(`Exists
      ([("x791", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x790"));(`Unknown, (`Variable
        "x793"));(`Unknown, (`Variable "x791"));]));(`Equality ((`Unknown,
      (`Variable "x791")), (`Unknown, (`Variable
        "a'"))));])));]);])));(`Forall ([("x789", `Unknown);("x786",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Conjunction
    [(`Conjunction [(`Exists ([("x773", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x773")), (`Unknown, (`Variable
        "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x773"));(`Unknown, (`Variable "x786"));]));])));(`Negation
      (`Exists ([("x772", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x772")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x772"));(`Unknown, (`Variable "x786"));]));]))));]);(`Negation
      (`Exists ([("x771", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x771")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x771"));(`Unknown, (`Variable "x786"));]));]))));]);(`Exists
    ([("x788", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
    [(`Unknown, (`Variable "x786"));(`Unknown, (`Variable
      "x789"));(`Unknown, (`Variable "x788"));]));(`Equality ((`Unknown,
    (`Variable "x788")), (`Unknown, (`Variable
      "a'"))));])));]));(`Conjunction [(`Conjunction [(`Conjunction
    [(`Exists ([("x773", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x773")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x773"));(`Unknown, (`Variable
        "x786"));]));])));(`Negation (`Exists ([("x772", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x772")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
      "x772"));(`Unknown, (`Variable "x786"));]));]))));]);(`Negation
    (`Exists ([("x771", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x771")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x771"));(`Unknown, (`Variable
        "x786"));]));]))));]);(`Exists ([("x787", `Unknown);],
  (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x786"));(`Unknown, (`Variable "x789"));(`Unknown, (`Variable
    "x787"));]));(`Equality ((`Unknown, (`Variable "x787")), (`Unknown,
  (`Variable "a"))));])));]);])));]);(`Conjunction [(`Forall ([("x783",
  `Unknown);("x780", `Unknown);], (`Disjunction [(`Negation (`Conjunction
    [(`Conjunction [(`Conjunction [(`Exists ([("x773", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x773")), (`Unknown,
    (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x773"));(`Unknown, (`Variable "x780"));]));])));(`Negation (`Exists
      ([("x772", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x772")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("from", [(`Unknown, (`Variable "x772"));(`Unknown, (`Variable
          "x780"));]));]))));]);(`Negation (`Exists ([("x771", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x771")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x771"));(`Unknown, (`Variable "x780"));]));]))));]);(`Exists
      ([("x782", `Unknown);], (`Conjunction [(`Predicate ("abLost",
      [(`Unknown, (`Variable "x780"));(`Unknown, (`Variable
        "x783"));(`Unknown, (`Variable "x782"));]));(`Equality ((`Unknown,
      (`Variable "x782")), (`Unknown, (`Variable
        "a"))));])));]));(`Conjunction [(`Conjunction [(`Conjunction
    [(`Exists ([("x773", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x773")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x773"));(`Unknown, (`Variable
        "x780"));]));])));(`Negation (`Exists ([("x772", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x772")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
      "x772"));(`Unknown, (`Variable "x780"));]));]))));]);(`Negation
    (`Exists ([("x771", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x771")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x771"));(`Unknown, (`Variable
        "x780"));]));]))));]);(`Exists ([("x781", `Unknown);],
  (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x780"));(`Unknown, (`Variable "x783"));(`Unknown, (`Variable
    "x781"));]));(`Equality ((`Unknown, (`Variable "x781")), (`Unknown,
  (`Variable "a'"))));])));]);])));(`Forall ([("x779", `Unknown);("x776",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Conjunction
    [(`Conjunction [(`Exists ([("x773", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x773")), (`Unknown, (`Variable
        "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x773"));(`Unknown, (`Variable "x776"));]));])));(`Negation
      (`Exists ([("x772", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x772")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x772"));(`Unknown, (`Variable "x776"));]));]))));]);(`Negation
      (`Exists ([("x771", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x771")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x771"));(`Unknown, (`Variable "x776"));]));]))));]);(`Exists
    ([("x778", `Unknown);], (`Conjunction [(`Predicate ("abLost",
    [(`Unknown, (`Variable "x776"));(`Unknown, (`Variable
      "x779"));(`Unknown, (`Variable "x778"));]));(`Equality ((`Unknown,
    (`Variable "x778")), (`Unknown, (`Variable
      "a'"))));])));]));(`Conjunction [(`Conjunction [(`Conjunction
    [(`Exists ([("x773", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x773")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x773"));(`Unknown, (`Variable
        "x776"));]));])));(`Negation (`Exists ([("x772", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x772")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
      "x772"));(`Unknown, (`Variable "x776"));]));]))));]);(`Negation
    (`Exists ([("x771", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x771")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x771"));(`Unknown, (`Variable
        "x776"));]));]))));]);(`Exists ([("x777", `Unknown);],
  (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x776"));(`Unknown, (`Variable "x779"));(`Unknown, (`Variable
    "x777"));]));(`Equality ((`Unknown, (`Variable "x777")), (`Unknown,
  (`Variable "a"))));])));]);])));]);]);]);(`Conjunction [(`Forall
    ([("x770", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x768",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x768")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x768"));(`Unknown, (`Variable "x770"));]));]))));(`Exists
      ([("x769", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x769")), (`Unknown, (`Variable "a"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x769"));(`Unknown,
        (`Variable "x770"));]));])));])));]);(`Conjunction [(`Forall
    ([("x767", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x765",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x765")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
    (`Variable "x765"));(`Unknown, (`Variable "x767"));]));]))));(`Exists
      ([("x766", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x766")), (`Unknown, (`Variable "a"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x766"));(`Unknown,
        (`Variable "x767"));]));])));])));]);(`Conjunction [(`Forall
    ([("x764", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x763",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x763")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
    (`Variable "x763"));(`Unknown, (`Variable "x764"));]));]))));(`Exists
      ([("x762", `Unknown);], (`Conjunction [(`Exists ([("x761",
      `Unknown);], (`Conjunction [(`Exists ([("x760", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x760")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x760"));(`Unknown, (`Variable "x761"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x761"));(`Unknown, (`Variable
          "x764"));(`Unknown, (`Variable "x762"));]));])));(`Equality
        ((`Unknown, (`Variable "x762")), (`Unknown, (`Variable
          "a"))));])));])));]);(`Negation (`Exists ([("x759", `Unknown);],
  (`Conjunction [(`Exists ([("x758", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x758")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x758"));(`Unknown, (`Variable "x759"));]));])));(`Exists ([("x757",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x757")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
  (`Variable "x757"));(`Unknown, (`Variable
    "x759"));]));])));]))));(`Conjunction [(`Forall ([("x756", `Unknown);],
  (`Disjunction [(`Negation (`Exists ([("x754", `Unknown);], (`Conjunction
    [(`Exists ([("x753", `Unknown);], (`Conjunction [(`Exists ([("x752",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x752")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x752"));(`Unknown, (`Variable "x753"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x753"));(`Unknown, (`Variable
        "x756"));(`Unknown, (`Variable "x754"));]));])));(`Equality
      ((`Unknown, (`Variable "x754")), (`Unknown, (`Variable
        "a'"))));]))));(`Conjunction [(`Exists ([("x751", `Unknown);],
  (`Conjunction [(`Exists ([("x750", `Unknown);], (`Conjunction [(`Exists
    ([("x749", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x749")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x749"));(`Unknown, (`Variable
        "x750"));]));])));(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x750"));(`Unknown, (`Variable "x756"));(`Unknown, (`Variable
    "x751"));]));])));(`Equality ((`Unknown, (`Variable "x751")),
  (`Unknown, (`Variable "a"))));])));(`Negation (`Exists ([("x748",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x748")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
  (`Variable "x748"));(`Unknown, (`Variable
    "x756"));]));]))));]);])));(`Forall ([("x755", `Unknown);],
  (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x751", `Unknown);],
  (`Conjunction [(`Exists ([("x750", `Unknown);], (`Conjunction [(`Exists
    ([("x749", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x749")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x749"));(`Unknown, (`Variable
        "x750"));]));])));(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x750"));(`Unknown, (`Variable "x755"));(`Unknown, (`Variable
    "x751"));]));])));(`Equality ((`Unknown, (`Variable "x751")),
  (`Unknown, (`Variable "a"))));])));(`Negation (`Exists ([("x748",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x748")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
  (`Variable "x748"));(`Unknown, (`Variable "x755"));]));]))));]));(`Exists
    ([("x754", `Unknown);], (`Conjunction [(`Exists ([("x753", `Unknown);],
    (`Conjunction [(`Exists ([("x752", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x752")), (`Unknown, (`Variable
        "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x752"));(`Unknown, (`Variable "x753"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x753"));(`Unknown, (`Variable
        "x755"));(`Unknown, (`Variable "x754"));]));])));(`Equality
      ((`Unknown, (`Variable "x754")), (`Unknown, (`Variable
        "a'"))));])));])));]);(`Conjunction [(`Forall ([("x747",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x745", `Unknown);],
  (`Conjunction [(`Exists ([("x744", `Unknown);], (`Conjunction [(`Exists
    ([("x743", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x743")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x743"));(`Unknown, (`Variable
        "x744"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
    "x744"));(`Unknown, (`Variable "x747"));(`Unknown, (`Variable
    "x745"));]));])));(`Equality ((`Unknown, (`Variable "x745")),
  (`Unknown, (`Variable "a'"))));]))));(`Exists ([("x742", `Unknown);],
  (`Conjunction [(`Exists ([("x741", `Unknown);], (`Conjunction [(`Exists
    ([("x740", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x740")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x740"));(`Unknown, (`Variable
        "x741"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
    "x741"));(`Unknown, (`Variable "x747"));(`Unknown, (`Variable
    "x742"));]));])));(`Equality ((`Unknown, (`Variable "x742")),
  (`Unknown, (`Variable "a"))));])));])));(`Forall ([("x746", `Unknown);],
  (`Disjunction [(`Negation (`Exists ([("x742", `Unknown);], (`Conjunction
    [(`Exists ([("x741", `Unknown);], (`Conjunction [(`Exists ([("x740",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x740")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x740"));(`Unknown, (`Variable "x741"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x741"));(`Unknown, (`Variable
        "x746"));(`Unknown, (`Variable "x742"));]));])));(`Equality
      ((`Unknown, (`Variable "x742")), (`Unknown, (`Variable
        "a"))));]))));(`Exists ([("x745", `Unknown);], (`Conjunction
    [(`Exists ([("x744", `Unknown);], (`Conjunction [(`Exists ([("x743",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x743")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x743"));(`Unknown, (`Variable "x744"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x744"));(`Unknown, (`Variable
        "x746"));(`Unknown, (`Variable "x745"));]));])));(`Equality
      ((`Unknown, (`Variable "x745")), (`Unknown, (`Variable
        "a'"))));])));])));]);(`Conjunction [(`Forall ([("x739",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x737", `Unknown);],
  (`Conjunction [(`Exists ([("x736", `Unknown);], (`Conjunction [(`Exists
    ([("x735", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x735")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x735"));(`Unknown, (`Variable
        "x736"));]));])));(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x736"));(`Unknown, (`Variable "x739"));(`Unknown, (`Variable
    "x737"));]));])));(`Equality ((`Unknown, (`Variable "x737")),
  (`Unknown, (`Variable "a'"))));]))));(`Disjunction [(`Exists ([("x734",
  `Unknown);], (`Conjunction [(`Exists ([("x733", `Unknown);],
  (`Conjunction [(`Exists ([("x732", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x732")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x732"));(`Unknown, (`Variable "x733"));]));])));(`Predicate
    ("abBalance", [(`Unknown, (`Variable "x733"));(`Unknown, (`Variable
      "x739"));(`Unknown, (`Variable "x734"));]));])));(`Equality
    ((`Unknown, (`Variable "x734")), (`Unknown, (`Variable
      "a"))));])));(`Exists ([("x731", `Unknown);], (`Conjunction
    [(`Equality ((`Unknown, (`Variable "x731")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
      "x731"));(`Unknown, (`Variable "x739"));]));])));]);])));(`Forall
    ([("x738", `Unknown);], (`Disjunction [(`Negation (`Disjunction
      [(`Exists ([("x734", `Unknown);], (`Conjunction [(`Exists ([("x733",
      `Unknown);], (`Conjunction [(`Exists ([("x732", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x732")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x732"));(`Unknown, (`Variable "x733"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x733"));(`Unknown, (`Variable
          "x738"));(`Unknown, (`Variable "x734"));]));])));(`Equality
        ((`Unknown, (`Variable "x734")), (`Unknown, (`Variable
          "a"))));])));(`Exists ([("x731", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x731")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
          "x731"));(`Unknown, (`Variable "x738"));]));])));]));(`Exists
      ([("x737", `Unknown);], (`Conjunction [(`Exists ([("x736",
      `Unknown);], (`Conjunction [(`Exists ([("x735", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x735")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x735"));(`Unknown, (`Variable "x736"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x736"));(`Unknown, (`Variable
          "x738"));(`Unknown, (`Variable "x737"));]));])));(`Equality
        ((`Unknown, (`Variable "x737")), (`Unknown, (`Variable
          "a'"))));])));])));]);(`Conjunction [(`Forall ([("x730",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x728", `Unknown);],
  (`Conjunction [(`Exists ([("x727", `Unknown);], (`Conjunction [(`Exists
    ([("x726", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x726")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x726"));(`Unknown, (`Variable
        "x727"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
    "x727"));(`Unknown, (`Variable "x730"));(`Unknown, (`Variable
    "x728"));]));])));(`Equality ((`Unknown, (`Variable "x728")),
  (`Unknown, (`Variable "a'"))));]))));(`Exists ([("x725", `Unknown);],
  (`Conjunction [(`Exists ([("x724", `Unknown);], (`Conjunction [(`Exists
    ([("x723", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x723")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x723"));(`Unknown, (`Variable
        "x724"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
    "x724"));(`Unknown, (`Variable "x730"));(`Unknown, (`Variable
    "x725"));]));])));(`Equality ((`Unknown, (`Variable "x725")),
  (`Unknown, (`Variable "a"))));])));])));(`Forall ([("x729", `Unknown);],
  (`Disjunction [(`Negation (`Exists ([("x725", `Unknown);], (`Conjunction
    [(`Exists ([("x724", `Unknown);], (`Conjunction [(`Exists ([("x723",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x723")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
    (`Variable "x723"));(`Unknown, (`Variable "x724"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x724"));(`Unknown, (`Variable
        "x729"));(`Unknown, (`Variable "x725"));]));])));(`Equality
      ((`Unknown, (`Variable "x725")), (`Unknown, (`Variable
        "a"))));]))));(`Exists ([("x728", `Unknown);], (`Conjunction
    [(`Exists ([("x727", `Unknown);], (`Conjunction [(`Exists ([("x726",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x726")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
    (`Variable "x726"));(`Unknown, (`Variable "x727"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x727"));(`Unknown, (`Variable
        "x729"));(`Unknown, (`Variable "x728"));]));])));(`Equality
      ((`Unknown, (`Variable "x728")), (`Unknown, (`Variable
        "a'"))));])));])));]);(`Conjunction [(`Forall ([("x722",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x720", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x720")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x720"));(`Unknown, (`Variable "x722"));]));]))));(`Exists ([("x721",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x721")),
  (`Unknown, (`Variable "a'"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x721"));(`Unknown, (`Variable
    "x722"));]));])));])));]);(`Conjunction [(`Forall ([("x719",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x717", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x717")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x717"));(`Unknown, (`Variable "x719"));]));]))));(`Exists ([("x718",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x718")),
  (`Unknown, (`Variable "a'"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x718"));(`Unknown, (`Variable
    "x719"));]));])));])));]);]);(`Conjunction [(`Conjunction
    [(`Conjunction [(`Conjunction [(`Forall ([("x716", `Unknown);],
    (`Disjunction [(`Negation (`Equality ((`Unknown, (`Variable "x716")),
    (`Unknown, (`Variable "a_out")))));(`Predicate ("aNullOut", [(`Unknown,
    (`Variable "x716"));]));])));(`Forall ([("x715", `Unknown);],
    (`Disjunction [(`Negation (`Predicate ("aNullOut", [(`Unknown,
    (`Variable "x715"));])));(`Equality ((`Unknown, (`Variable "x715")),
    (`Unknown, (`Variable "a_out"))));])));]);]);(`Forall ([("x714",
    `Unknown);], (`Disjunction [(`Negation (`Equality ((`Unknown,
    (`Variable "x714")), (`Unknown, (`Variable "a_in")))));(`Predicate
      ("TransferDetails", [(`Unknown, (`Variable
        "x714"));]));])));(`Conjunction [(`Forall ([("x713", `Unknown);],
    (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
      ([("x711", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x711")), (`Unknown, (`Variable "a"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x711"));(`Unknown,
        (`Variable "x713"));]));])));(`Negation (`Exists ([("x710",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x710")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x710"));(`Unknown, (`Variable
      "x713"));]));]))));]);(`Negation (`Exists ([("x709", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x709")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x709"));(`Unknown, (`Variable "x713"));]));]))));]));(`Conjunction
      [(`Conjunction [(`Exists ([("x708", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x708")), (`Unknown, (`Variable
          "a'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x708"));(`Unknown, (`Variable "x713"));]));])));(`Negation
        (`Exists ([("x707", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x707")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x707"));(`Unknown, (`Variable "x713"));]));]))));]);(`Negation
        (`Exists ([("x706", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x706")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x706"));(`Unknown, (`Variable
          "x713"));]));]))));]);])));(`Forall ([("x712", `Unknown);],
    (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
      ([("x708", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x708")), (`Unknown, (`Variable "a'"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x708"));(`Unknown,
        (`Variable "x712"));]));])));(`Negation (`Exists ([("x707",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x707")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x707"));(`Unknown, (`Variable
      "x712"));]));]))));]);(`Negation (`Exists ([("x706", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x706")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x706"));(`Unknown, (`Variable "x712"));]));]))));]));(`Conjunction
      [(`Conjunction [(`Exists ([("x711", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x711")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x711"));(`Unknown, (`Variable "x712"));]));])));(`Negation
        (`Exists ([("x710", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x710")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x710"));(`Unknown, (`Variable "x712"));]));]))));]);(`Negation
        (`Exists ([("x709", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x709")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x709"));(`Unknown, (`Variable
          "x712"));]));]))));]);])));]);(`Conjunction [(`Conjunction
      [(`Forall ([("x705", `Unknown);("x702", `Unknown);], (`Disjunction
        [(`Negation (`Conjunction [(`Conjunction [(`Conjunction [(`Exists
          ([("x685", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x685")), (`Unknown, (`Variable "a"))));(`Predicate
            ("abAuthPurse", [(`Unknown, (`Variable "x685"));(`Unknown,
            (`Variable "x702"));]));])));(`Negation (`Exists ([("x684",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x684")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x684"));(`Unknown, (`Variable
          "x702"));]));]))));]);(`Negation (`Exists ([("x683", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x683")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x683"));(`Unknown, (`Variable
          "x702"));]));]))));]);(`Exists ([("x704", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x702"));(`Unknown, (`Variable "x705"));(`Unknown, (`Variable
          "x704"));]));(`Equality ((`Unknown, (`Variable "x704")),
        (`Unknown, (`Variable "a"))));])));]));(`Conjunction [(`Conjunction
          [(`Conjunction [(`Exists ([("x685", `Unknown);], (`Conjunction
            [(`Equality ((`Unknown, (`Variable "x685")), (`Unknown,
            (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
            (`Variable "x685"));(`Unknown, (`Variable
              "x702"));]));])));(`Negation (`Exists ([("x684", `Unknown);],
          (`Conjunction [(`Equality ((`Unknown, (`Variable "x684")),
          (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
          (`Variable "x684"));(`Unknown, (`Variable
            "x702"));]));]))));]);(`Negation (`Exists ([("x683",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x683")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x683"));(`Unknown, (`Variable
            "x702"));]));]))));]);(`Exists ([("x703", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x702"));(`Unknown, (`Variable "x705"));(`Unknown, (`Variable
          "x703"));]));(`Equality ((`Unknown, (`Variable "x703")),
        (`Unknown, (`Variable "a'"))));])));]);])));(`Forall ([("x701",
      `Unknown);("x698", `Unknown);], (`Disjunction [(`Negation
        (`Conjunction [(`Conjunction [(`Conjunction [(`Exists ([("x685",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x685")), (`Unknown, (`Variable "a"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x685"));(`Unknown,
          (`Variable "x698"));]));])));(`Negation (`Exists ([("x684",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x684")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x684"));(`Unknown, (`Variable
          "x698"));]));]))));]);(`Negation (`Exists ([("x683", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x683")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x683"));(`Unknown, (`Variable
          "x698"));]));]))));]);(`Exists ([("x700", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x698"));(`Unknown, (`Variable "x701"));(`Unknown, (`Variable
          "x700"));]));(`Equality ((`Unknown, (`Variable "x700")),
        (`Unknown, (`Variable "a'"))));])));]));(`Conjunction
        [(`Conjunction [(`Conjunction [(`Exists ([("x685", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x685")),
        (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse",
        [(`Unknown, (`Variable "x685"));(`Unknown, (`Variable
          "x698"));]));])));(`Negation (`Exists ([("x684", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x684")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
        (`Variable "x684"));(`Unknown, (`Variable
          "x698"));]));]))));]);(`Negation (`Exists ([("x683", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x683")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x683"));(`Unknown, (`Variable
          "x698"));]));]))));]);(`Exists ([("x699", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x698"));(`Unknown, (`Variable "x701"));(`Unknown, (`Variable
          "x699"));]));(`Equality ((`Unknown, (`Variable "x699")),
        (`Unknown, (`Variable "a"))));])));]);])));]);(`Conjunction
      [(`Forall ([("x695", `Unknown);("x692", `Unknown);], (`Disjunction
        [(`Negation (`Conjunction [(`Conjunction [(`Conjunction [(`Exists
          ([("x685", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x685")), (`Unknown, (`Variable "a"))));(`Predicate
            ("abAuthPurse", [(`Unknown, (`Variable "x685"));(`Unknown,
            (`Variable "x692"));]));])));(`Negation (`Exists ([("x684",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x684")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x684"));(`Unknown, (`Variable
          "x692"));]));]))));]);(`Negation (`Exists ([("x683", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x683")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x683"));(`Unknown, (`Variable
          "x692"));]));]))));]);(`Exists ([("x694", `Unknown);],
        (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
          "x692"));(`Unknown, (`Variable "x695"));(`Unknown, (`Variable
          "x694"));]));(`Equality ((`Unknown, (`Variable "x694")),
        (`Unknown, (`Variable "a"))));])));]));(`Conjunction [(`Conjunction
          [(`Conjunction [(`Exists ([("x685", `Unknown);], (`Conjunction
            [(`Equality ((`Unknown, (`Variable "x685")), (`Unknown,
            (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
            (`Variable "x685"));(`Unknown, (`Variable
              "x692"));]));])));(`Negation (`Exists ([("x684", `Unknown);],
          (`Conjunction [(`Equality ((`Unknown, (`Variable "x684")),
          (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
          (`Variable "x684"));(`Unknown, (`Variable
            "x692"));]));]))));]);(`Negation (`Exists ([("x683",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x683")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x683"));(`Unknown, (`Variable
            "x692"));]));]))));]);(`Exists ([("x693", `Unknown);],
        (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
          "x692"));(`Unknown, (`Variable "x695"));(`Unknown, (`Variable
          "x693"));]));(`Equality ((`Unknown, (`Variable "x693")),
        (`Unknown, (`Variable "a'"))));])));]);])));(`Forall ([("x691",
      `Unknown);("x688", `Unknown);], (`Disjunction [(`Negation
        (`Conjunction [(`Conjunction [(`Conjunction [(`Exists ([("x685",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x685")), (`Unknown, (`Variable "a"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x685"));(`Unknown,
          (`Variable "x688"));]));])));(`Negation (`Exists ([("x684",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x684")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x684"));(`Unknown, (`Variable
          "x688"));]));]))));]);(`Negation (`Exists ([("x683", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x683")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x683"));(`Unknown, (`Variable
          "x688"));]));]))));]);(`Exists ([("x690", `Unknown);],
        (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
          "x688"));(`Unknown, (`Variable "x691"));(`Unknown, (`Variable
          "x690"));]));(`Equality ((`Unknown, (`Variable "x690")),
        (`Unknown, (`Variable "a'"))));])));]));(`Conjunction
        [(`Conjunction [(`Conjunction [(`Exists ([("x685", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x685")),
        (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse",
        [(`Unknown, (`Variable "x685"));(`Unknown, (`Variable
          "x688"));]));])));(`Negation (`Exists ([("x684", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x684")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
        (`Variable "x684"));(`Unknown, (`Variable
          "x688"));]));]))));]);(`Negation (`Exists ([("x683", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x683")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x683"));(`Unknown, (`Variable
          "x688"));]));]))));]);(`Exists ([("x689", `Unknown);],
        (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
          "x688"));(`Unknown, (`Variable "x691"));(`Unknown, (`Variable
          "x689"));]));(`Equality ((`Unknown, (`Variable "x689")),
        (`Unknown, (`Variable "a"))));])));]);])));]);]);]);(`Conjunction
    [(`Forall ([("x682", `Unknown);], (`Disjunction [(`Negation (`Exists
      ([("x680", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x680")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("from", [(`Unknown, (`Variable "x680"));(`Unknown, (`Variable
          "x682"));]));]))));(`Exists ([("x681", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x681")), (`Unknown, (`Variable
        "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x681"));(`Unknown, (`Variable
        "x682"));]));])));])));]);(`Conjunction [(`Forall ([("x679",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x677", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x677")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x677"));(`Unknown, (`Variable "x679"));]));]))));(`Exists ([("x678",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x678")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x678"));(`Unknown, (`Variable
    "x679"));]));])));])));]);(`Conjunction [(`Forall ([("x676",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x675", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x675")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
    "x675"));(`Unknown, (`Variable "x676"));]));]))));(`Exists ([("x674",
  `Unknown);], (`Conjunction [(`Exists ([("x673", `Unknown);],
  (`Conjunction [(`Exists ([("x672", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x672")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x672"));(`Unknown, (`Variable "x673"));]));])));(`Predicate
    ("abBalance", [(`Unknown, (`Variable "x673"));(`Unknown, (`Variable
      "x676"));(`Unknown, (`Variable "x674"));]));])));(`Equality
    ((`Unknown, (`Variable "x674")), (`Unknown, (`Variable
      "a"))));])));])));]);(`Negation (`Exists ([("x671", `Unknown);],
  (`Conjunction [(`Exists ([("x670", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x670")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x670"));(`Unknown, (`Variable "x671"));]));])));(`Exists ([("x669",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x669")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
  (`Variable "x669"));(`Unknown, (`Variable
    "x671"));]));])));]))));(`Conjunction [(`Forall ([("x668", `Unknown);],
  (`Disjunction [(`Negation (`Exists ([("x666", `Unknown);], (`Conjunction
    [(`Exists ([("x665", `Unknown);], (`Conjunction [(`Exists ([("x664",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x664")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x664"));(`Unknown, (`Variable "x665"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x665"));(`Unknown, (`Variable
        "x668"));(`Unknown, (`Variable "x666"));]));])));(`Equality
      ((`Unknown, (`Variable "x666")), (`Unknown, (`Variable
        "a'"))));]))));(`Conjunction [(`Exists ([("x663", `Unknown);],
  (`Conjunction [(`Exists ([("x662", `Unknown);], (`Conjunction [(`Exists
    ([("x661", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x661")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x661"));(`Unknown, (`Variable
        "x662"));]));])));(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x662"));(`Unknown, (`Variable "x668"));(`Unknown, (`Variable
    "x663"));]));])));(`Equality ((`Unknown, (`Variable "x663")),
  (`Unknown, (`Variable "a"))));])));(`Negation (`Exists ([("x660",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x660")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
  (`Variable "x660"));(`Unknown, (`Variable
    "x668"));]));]))));]);])));(`Forall ([("x667", `Unknown);],
  (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x663", `Unknown);],
  (`Conjunction [(`Exists ([("x662", `Unknown);], (`Conjunction [(`Exists
    ([("x661", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x661")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x661"));(`Unknown, (`Variable
        "x662"));]));])));(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x662"));(`Unknown, (`Variable "x667"));(`Unknown, (`Variable
    "x663"));]));])));(`Equality ((`Unknown, (`Variable "x663")),
  (`Unknown, (`Variable "a"))));])));(`Negation (`Exists ([("x660",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x660")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
  (`Variable "x660"));(`Unknown, (`Variable "x667"));]));]))));]));(`Exists
    ([("x666", `Unknown);], (`Conjunction [(`Exists ([("x665", `Unknown);],
    (`Conjunction [(`Exists ([("x664", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x664")), (`Unknown, (`Variable
        "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x664"));(`Unknown, (`Variable "x665"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x665"));(`Unknown, (`Variable
        "x667"));(`Unknown, (`Variable "x666"));]));])));(`Equality
      ((`Unknown, (`Variable "x666")), (`Unknown, (`Variable
        "a'"))));])));])));]);(`Conjunction [(`Forall ([("x659",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x657", `Unknown);],
  (`Conjunction [(`Exists ([("x656", `Unknown);], (`Conjunction [(`Exists
    ([("x655", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x655")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x655"));(`Unknown, (`Variable
        "x656"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
    "x656"));(`Unknown, (`Variable "x659"));(`Unknown, (`Variable
    "x657"));]));])));(`Equality ((`Unknown, (`Variable "x657")),
  (`Unknown, (`Variable "a'"))));]))));(`Disjunction [(`Exists ([("x654",
  `Unknown);], (`Conjunction [(`Exists ([("x653", `Unknown);],
  (`Conjunction [(`Exists ([("x652", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x652")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x652"));(`Unknown, (`Variable "x653"));]));])));(`Predicate ("abLost",
  [(`Unknown, (`Variable "x653"));(`Unknown, (`Variable "x659"));(`Unknown,
  (`Variable "x654"));]));])));(`Equality ((`Unknown, (`Variable "x654")),
  (`Unknown, (`Variable "a"))));])));(`Exists ([("x651", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x651")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
    "x651"));(`Unknown, (`Variable "x659"));]));])));]);])));(`Forall
    ([("x658", `Unknown);], (`Disjunction [(`Negation (`Disjunction
      [(`Exists ([("x654", `Unknown);], (`Conjunction [(`Exists ([("x653",
      `Unknown);], (`Conjunction [(`Exists ([("x652", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x652")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x652"));(`Unknown, (`Variable "x653"));]));])));(`Predicate
        ("abLost", [(`Unknown, (`Variable "x653"));(`Unknown, (`Variable
          "x658"));(`Unknown, (`Variable "x654"));]));])));(`Equality
        ((`Unknown, (`Variable "x654")), (`Unknown, (`Variable
          "a"))));])));(`Exists ([("x651", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x651")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
          "x651"));(`Unknown, (`Variable "x658"));]));])));]));(`Exists
      ([("x657", `Unknown);], (`Conjunction [(`Exists ([("x656",
      `Unknown);], (`Conjunction [(`Exists ([("x655", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x655")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x655"));(`Unknown, (`Variable "x656"));]));])));(`Predicate
        ("abLost", [(`Unknown, (`Variable "x656"));(`Unknown, (`Variable
          "x658"));(`Unknown, (`Variable "x657"));]));])));(`Equality
        ((`Unknown, (`Variable "x657")), (`Unknown, (`Variable
          "a'"))));])));])));]);(`Conjunction [(`Conjunction [(`Forall
    ([("x650", `Unknown);("x647", `Unknown);], (`Disjunction [(`Negation
      (`Conjunction [(`Exists ([("x630", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x630")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x630"));(`Unknown, (`Variable "x647"));]));])));(`Exists
        ([("x649", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
        [(`Unknown, (`Variable "x647"));(`Unknown, (`Variable
          "x650"));(`Unknown, (`Variable "x649"));]));(`Equality
          ((`Unknown, (`Variable "x649")), (`Unknown, (`Variable
            "a"))));])));]));(`Conjunction [(`Exists ([("x630",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x630")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
    (`Variable "x630"));(`Unknown, (`Variable "x647"));]));])));(`Exists
      ([("x648", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x647"));(`Unknown, (`Variable
        "x650"));(`Unknown, (`Variable "x648"));]));(`Equality ((`Unknown,
      (`Variable "x648")), (`Unknown, (`Variable
        "a'"))));])));]);])));(`Forall ([("x646", `Unknown);("x643",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x630",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x630")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
  (`Variable "x630"));(`Unknown, (`Variable "x643"));]));])));(`Exists
    ([("x645", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
    [(`Unknown, (`Variable "x643"));(`Unknown, (`Variable
      "x646"));(`Unknown, (`Variable "x645"));]));(`Equality ((`Unknown,
    (`Variable "x645")), (`Unknown, (`Variable
      "a'"))));])));]));(`Conjunction [(`Exists ([("x630", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x630")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x630"));(`Unknown, (`Variable "x643"));]));])));(`Exists ([("x644",
  `Unknown);], (`Conjunction [(`Predicate ("abBalance", [(`Unknown,
  (`Variable "x643"));(`Unknown, (`Variable "x646"));(`Unknown, (`Variable
    "x644"));]));(`Equality ((`Unknown, (`Variable "x644")), (`Unknown,
  (`Variable "a"))));])));]);])));]);(`Conjunction [(`Forall ([("x640",
  `Unknown);("x637", `Unknown);], (`Disjunction [(`Negation (`Conjunction
    [(`Exists ([("x630", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x630")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x630"));(`Unknown, (`Variable
        "x637"));]));])));(`Exists ([("x639", `Unknown);], (`Conjunction
      [(`Predicate ("abLost", [(`Unknown, (`Variable "x637"));(`Unknown,
      (`Variable "x640"));(`Unknown, (`Variable "x639"));]));(`Equality
        ((`Unknown, (`Variable "x639")), (`Unknown, (`Variable
          "a"))));])));]));(`Conjunction [(`Exists ([("x630", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x630")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x630"));(`Unknown, (`Variable "x637"));]));])));(`Exists ([("x638",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x637"));(`Unknown, (`Variable "x640"));(`Unknown, (`Variable
    "x638"));]));(`Equality ((`Unknown, (`Variable "x638")), (`Unknown,
  (`Variable "a'"))));])));]);])));(`Forall ([("x636", `Unknown);("x633",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x630",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x630")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
  (`Variable "x630"));(`Unknown, (`Variable "x633"));]));])));(`Exists
    ([("x635", `Unknown);], (`Conjunction [(`Predicate ("abLost",
    [(`Unknown, (`Variable "x633"));(`Unknown, (`Variable
      "x636"));(`Unknown, (`Variable "x635"));]));(`Equality ((`Unknown,
    (`Variable "x635")), (`Unknown, (`Variable
      "a'"))));])));]));(`Conjunction [(`Exists ([("x630", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x630")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x630"));(`Unknown, (`Variable "x633"));]));])));(`Exists ([("x634",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x633"));(`Unknown, (`Variable "x636"));(`Unknown, (`Variable
    "x634"));]));(`Equality ((`Unknown, (`Variable "x634")), (`Unknown,
  (`Variable "a"))));])));]);])));]);]);(`Conjunction [(`Forall ([("x629",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x627", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x627")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x627"));(`Unknown, (`Variable "x629"));]));]))));(`Exists ([("x628",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x628")),
  (`Unknown, (`Variable "a'"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x628"));(`Unknown, (`Variable
    "x629"));]));])));])));]);(`Conjunction [(`Forall ([("x626",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x624", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x624")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x624"));(`Unknown, (`Variable "x626"));]));]))));(`Exists ([("x625",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x625")),
  (`Unknown, (`Variable "a'"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x625"));(`Unknown, (`Variable
    "x626"));]));])));])));]);]);(`Conjunction [(`Conjunction
    [(`Conjunction [(`Forall ([("x623", `Unknown);], (`Disjunction
      [(`Negation (`Equality ((`Unknown, (`Variable "x623")), (`Unknown,
      (`Variable "a_out")))));(`Predicate ("aNullOut", [(`Unknown,
      (`Variable "x623"));]));])));(`Forall ([("x622", `Unknown);],
    (`Disjunction [(`Negation (`Predicate ("aNullOut", [(`Unknown,
    (`Variable "x622"));])));(`Equality ((`Unknown, (`Variable "x622")),
    (`Unknown, (`Variable "a_out"))));])));]);]);(`Conjunction [(`Forall
    ([("x621", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x619",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x619")),
    (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x619"));(`Unknown, (`Variable "x621"));]));]))));(`Exists
      ([("x618", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x618")), (`Unknown, (`Variable "a'"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x618"));(`Unknown,
        (`Variable "x621"));]));])));])));(`Forall ([("x620", `Unknown);],
  (`Disjunction [(`Negation (`Exists ([("x618", `Unknown);], (`Conjunction
    [(`Equality ((`Unknown, (`Variable "x618")), (`Unknown, (`Variable
      "a'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x618"));(`Unknown, (`Variable "x620"));]));]))));(`Exists ([("x619",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x619")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x619"));(`Unknown, (`Variable
    "x620"));]));])));])));]);(`Conjunction [(`Conjunction [(`Forall
    ([("x617", `Unknown);("x614", `Unknown);], (`Disjunction [(`Negation
      (`Conjunction [(`Exists ([("x597", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x597")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x597"));(`Unknown, (`Variable "x614"));]));])));(`Exists
        ([("x616", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
        [(`Unknown, (`Variable "x614"));(`Unknown, (`Variable
          "x617"));(`Unknown, (`Variable "x616"));]));(`Equality
          ((`Unknown, (`Variable "x616")), (`Unknown, (`Variable
            "a"))));])));]));(`Conjunction [(`Exists ([("x597",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x597")),
    (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x597"));(`Unknown, (`Variable "x614"));]));])));(`Exists
      ([("x615", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x614"));(`Unknown, (`Variable
        "x617"));(`Unknown, (`Variable "x615"));]));(`Equality ((`Unknown,
      (`Variable "x615")), (`Unknown, (`Variable
        "a'"))));])));]);])));(`Forall ([("x613", `Unknown);("x610",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x597",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x597")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x597"));(`Unknown, (`Variable "x610"));]));])));(`Exists
    ([("x612", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
    [(`Unknown, (`Variable "x610"));(`Unknown, (`Variable
      "x613"));(`Unknown, (`Variable "x612"));]));(`Equality ((`Unknown,
    (`Variable "x612")), (`Unknown, (`Variable
      "a'"))));])));]));(`Conjunction [(`Exists ([("x597", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x597")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x597"));(`Unknown, (`Variable "x610"));]));])));(`Exists ([("x611",
  `Unknown);], (`Conjunction [(`Predicate ("abBalance", [(`Unknown,
  (`Variable "x610"));(`Unknown, (`Variable "x613"));(`Unknown, (`Variable
    "x611"));]));(`Equality ((`Unknown, (`Variable "x611")), (`Unknown,
  (`Variable "a"))));])));]);])));]);(`Conjunction [(`Forall ([("x607",
  `Unknown);("x604", `Unknown);], (`Disjunction [(`Negation (`Conjunction
    [(`Exists ([("x597", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x597")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x597"));(`Unknown, (`Variable
        "x604"));]));])));(`Exists ([("x606", `Unknown);], (`Conjunction
      [(`Predicate ("abLost", [(`Unknown, (`Variable "x604"));(`Unknown,
      (`Variable "x607"));(`Unknown, (`Variable "x606"));]));(`Equality
        ((`Unknown, (`Variable "x606")), (`Unknown, (`Variable
          "a"))));])));]));(`Conjunction [(`Exists ([("x597", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x597")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x597"));(`Unknown, (`Variable "x604"));]));])));(`Exists ([("x605",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x604"));(`Unknown, (`Variable "x607"));(`Unknown, (`Variable
    "x605"));]));(`Equality ((`Unknown, (`Variable "x605")), (`Unknown,
  (`Variable "a'"))));])));]);])));(`Forall ([("x603", `Unknown);("x600",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x597",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x597")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x597"));(`Unknown, (`Variable "x600"));]));])));(`Exists
    ([("x602", `Unknown);], (`Conjunction [(`Predicate ("abLost",
    [(`Unknown, (`Variable "x600"));(`Unknown, (`Variable
      "x603"));(`Unknown, (`Variable "x602"));]));(`Equality ((`Unknown,
    (`Variable "x602")), (`Unknown, (`Variable
      "a'"))));])));]));(`Conjunction [(`Exists ([("x597", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x597")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x597"));(`Unknown, (`Variable "x600"));]));])));(`Exists ([("x601",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x600"));(`Unknown, (`Variable "x603"));(`Unknown, (`Variable
    "x601"));]));(`Equality ((`Unknown, (`Variable "x601")), (`Unknown,
  (`Variable "a"))));])));]);])));]);]);]);]);]);]));(`Conjunction
  [(`Negation (`Exists ([("x596", `Unknown);], (`Conjunction [(`Exists
    ([("x595", `Unknown);], (`Conjunction [(`Exists ([("x594", `Unknown);],
    (`Conjunction [(`Exists ([("x593", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x593")), (`Unknown, (`Variable
        "a'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x593"));(`Unknown, (`Variable "x594"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x594"));(`Unknown, (`Variable
        "x596"));(`Unknown, (`Variable "x595"));]));])));(`Equality
      ((`Unknown, (`Variable "x595")), (`Unknown, (`Variable
        "a'"))));])));(`Exists ([("x592", `Unknown);], (`Conjunction
    [(`Exists ([("x591", `Unknown);], (`Conjunction [(`Exists ([("x590",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x590")),
    (`Unknown, (`Variable "a'"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x590"));(`Unknown, (`Variable "x591"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x591"));(`Unknown, (`Variable
        "x596"));(`Unknown, (`Variable "x592"));]));])));(`Equality
      ((`Unknown, (`Variable "x592")), (`Unknown, (`Variable
        "a'"))));])));]))));(`Forall ([("c", `Unknown);], (`Disjunction
    [(`Negation (`Conjunction [(`Predicate ("Coin", [(`Unknown, (`Variable
      "c"));]));]));(`Forall ([("x586", `Unknown);("x587", `Unknown);],
    (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
      ([("x585", `Unknown);], (`Conjunction [(`Exists ([("x589",
      `Unknown);], (`Conjunction [(`Disjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x586"));(`Unknown, (`Variable
        "x585"));(`Unknown, (`Variable "x589"));]));(`Predicate ("abLost",
      [(`Unknown, (`Variable "x586"));(`Unknown, (`Variable
        "x585"));(`Unknown, (`Variable "x589"));]));]);(`Equality
        ((`Unknown, (`Variable "x589")), (`Unknown, (`Variable
          "a'"))));])));(`Equality ((`Unknown, (`Variable "x585")),
      (`Unknown, (`Variable "c"))));])));(`Exists ([("x583", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x583")), (`Unknown,
    (`Variable "a'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x583"));(`Unknown, (`Variable "x586"));]));])));]);(`Conjunction
      [(`Exists ([("x585", `Unknown);], (`Conjunction [(`Exists ([("x588",
      `Unknown);], (`Conjunction [(`Disjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x587"));(`Unknown, (`Variable
        "x585"));(`Unknown, (`Variable "x588"));]));(`Predicate ("abLost",
      [(`Unknown, (`Variable "x587"));(`Unknown, (`Variable
        "x585"));(`Unknown, (`Variable "x588"));]));]);(`Equality
        ((`Unknown, (`Variable "x588")), (`Unknown, (`Variable
          "a'"))));])));(`Equality ((`Unknown, (`Variable "x585")),
      (`Unknown, (`Variable "c"))));])));(`Exists ([("x583", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x583")), (`Unknown,
      (`Variable "a'"))));(`Predicate ("abAuthPurse", [(`Unknown,
      (`Variable "x583"));(`Unknown, (`Variable
        "x587"));]));])));]);]));(`Conjunction [(`Equality ((`Unknown,
    (`Variable "x586")), (`Unknown, (`Variable
      "x587"))));]);])));])));]);]);])));])); 
("AbIgnore_inv",(`Conjunction [(`Forall ([("a", `Unknown);("a'",
`Unknown);("a_out", `Unknown);], (`Disjunction [(`Negation (`Conjunction
  [(`Predicate ("AbWorld", [(`Unknown, (`Variable "a"));]));(`Predicate
    ("AbWorld", [(`Unknown, (`Variable "a'"));]));(`Predicate ("AOUT",
  [(`Unknown, (`Variable "a_out"));]));]));(`Disjunction [(`Negation
  (`Conjunction [(`Conjunction [(`Negation (`Exists ([("x582", `Unknown);],
  (`Conjunction [(`Exists ([("x581", `Unknown);], (`Conjunction [(`Exists
    ([("x580", `Unknown);], (`Conjunction [(`Exists ([("x579", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x579")), (`Unknown,
    (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x579"));(`Unknown, (`Variable "x580"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x580"));(`Unknown, (`Variable
        "x582"));(`Unknown, (`Variable "x581"));]));])));(`Equality
    ((`Unknown, (`Variable "x581")), (`Unknown, (`Variable
      "a"))));])));(`Exists ([("x578", `Unknown);], (`Conjunction [(`Exists
    ([("x577", `Unknown);], (`Conjunction [(`Exists ([("x576", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x576")), (`Unknown,
    (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x576"));(`Unknown, (`Variable "x577"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x577"));(`Unknown, (`Variable
        "x582"));(`Unknown, (`Variable "x578"));]));])));(`Equality
    ((`Unknown, (`Variable "x578")), (`Unknown, (`Variable
      "a"))));])));]))));(`Forall ([("c", `Unknown);], (`Disjunction
    [(`Negation (`Conjunction [(`Predicate ("Coin", [(`Unknown, (`Variable
      "c"));]));]));(`Forall ([("x572", `Unknown);("x573", `Unknown);],
    (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
      ([("x571", `Unknown);], (`Conjunction [(`Exists ([("x575",
      `Unknown);], (`Conjunction [(`Disjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x572"));(`Unknown, (`Variable
        "x571"));(`Unknown, (`Variable "x575"));]));(`Predicate ("abLost",
      [(`Unknown, (`Variable "x572"));(`Unknown, (`Variable
        "x571"));(`Unknown, (`Variable "x575"));]));]);(`Equality
        ((`Unknown, (`Variable "x575")), (`Unknown, (`Variable
          "a"))));])));(`Equality ((`Unknown, (`Variable "x571")),
      (`Unknown, (`Variable "c"))));])));(`Exists ([("x569", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x569")), (`Unknown,
    (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x569"));(`Unknown, (`Variable "x572"));]));])));]);(`Conjunction
      [(`Exists ([("x571", `Unknown);], (`Conjunction [(`Exists ([("x574",
      `Unknown);], (`Conjunction [(`Disjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x573"));(`Unknown, (`Variable
        "x571"));(`Unknown, (`Variable "x574"));]));(`Predicate ("abLost",
      [(`Unknown, (`Variable "x573"));(`Unknown, (`Variable
        "x571"));(`Unknown, (`Variable "x574"));]));]);(`Equality
        ((`Unknown, (`Variable "x574")), (`Unknown, (`Variable
          "a"))));])));(`Equality ((`Unknown, (`Variable "x571")),
      (`Unknown, (`Variable "c"))));])));(`Exists ([("x569", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x569")), (`Unknown,
      (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x569"));(`Unknown, (`Variable
        "x573"));]));])));]);]));(`Conjunction [(`Equality ((`Unknown,
    (`Variable "x572")), (`Unknown, (`Variable
      "x573"))));]);])));])));]);(`Conjunction [(`Conjunction
    [(`Conjunction [(`Forall ([("x568", `Unknown);], (`Disjunction
      [(`Negation (`Equality ((`Unknown, (`Variable "x568")), (`Unknown,
      (`Variable "a_out")))));(`Predicate ("aNullOut", [(`Unknown,
      (`Variable "x568"));]));])));(`Forall ([("x567", `Unknown);],
    (`Disjunction [(`Negation (`Predicate ("aNullOut", [(`Unknown,
    (`Variable "x567"));])));(`Equality ((`Unknown, (`Variable "x567")),
    (`Unknown, (`Variable "a_out"))));])));]);]);(`Conjunction [(`Forall
    ([("x566", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x564",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x564")),
    (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x564"));(`Unknown, (`Variable "x566"));]));]))));(`Exists
      ([("x563", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x563")), (`Unknown, (`Variable "a'"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x563"));(`Unknown,
        (`Variable "x566"));]));])));])));(`Forall ([("x565", `Unknown);],
  (`Disjunction [(`Negation (`Exists ([("x563", `Unknown);], (`Conjunction
    [(`Equality ((`Unknown, (`Variable "x563")), (`Unknown, (`Variable
      "a'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x563"));(`Unknown, (`Variable "x565"));]));]))));(`Exists ([("x564",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x564")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x564"));(`Unknown, (`Variable
    "x565"));]));])));])));]);(`Conjunction [(`Conjunction [(`Forall
    ([("x562", `Unknown);("x559", `Unknown);], (`Disjunction [(`Negation
      (`Conjunction [(`Exists ([("x542", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x542")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x542"));(`Unknown, (`Variable "x559"));]));])));(`Exists
        ([("x561", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
        [(`Unknown, (`Variable "x559"));(`Unknown, (`Variable
          "x562"));(`Unknown, (`Variable "x561"));]));(`Equality
          ((`Unknown, (`Variable "x561")), (`Unknown, (`Variable
            "a"))));])));]));(`Conjunction [(`Exists ([("x542",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x542")),
    (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x542"));(`Unknown, (`Variable "x559"));]));])));(`Exists
      ([("x560", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x559"));(`Unknown, (`Variable
        "x562"));(`Unknown, (`Variable "x560"));]));(`Equality ((`Unknown,
      (`Variable "x560")), (`Unknown, (`Variable
        "a'"))));])));]);])));(`Forall ([("x558", `Unknown);("x555",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x542",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x542")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x542"));(`Unknown, (`Variable "x555"));]));])));(`Exists
    ([("x557", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
    [(`Unknown, (`Variable "x555"));(`Unknown, (`Variable
      "x558"));(`Unknown, (`Variable "x557"));]));(`Equality ((`Unknown,
    (`Variable "x557")), (`Unknown, (`Variable
      "a'"))));])));]));(`Conjunction [(`Exists ([("x542", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x542")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x542"));(`Unknown, (`Variable "x555"));]));])));(`Exists ([("x556",
  `Unknown);], (`Conjunction [(`Predicate ("abBalance", [(`Unknown,
  (`Variable "x555"));(`Unknown, (`Variable "x558"));(`Unknown, (`Variable
    "x556"));]));(`Equality ((`Unknown, (`Variable "x556")), (`Unknown,
  (`Variable "a"))));])));]);])));]);(`Conjunction [(`Forall ([("x552",
  `Unknown);("x549", `Unknown);], (`Disjunction [(`Negation (`Conjunction
    [(`Exists ([("x542", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x542")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x542"));(`Unknown, (`Variable
        "x549"));]));])));(`Exists ([("x551", `Unknown);], (`Conjunction
      [(`Predicate ("abLost", [(`Unknown, (`Variable "x549"));(`Unknown,
      (`Variable "x552"));(`Unknown, (`Variable "x551"));]));(`Equality
        ((`Unknown, (`Variable "x551")), (`Unknown, (`Variable
          "a"))));])));]));(`Conjunction [(`Exists ([("x542", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x542")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x542"));(`Unknown, (`Variable "x549"));]));])));(`Exists ([("x550",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x549"));(`Unknown, (`Variable "x552"));(`Unknown, (`Variable
    "x550"));]));(`Equality ((`Unknown, (`Variable "x550")), (`Unknown,
  (`Variable "a'"))));])));]);])));(`Forall ([("x548", `Unknown);("x545",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x542",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x542")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x542"));(`Unknown, (`Variable "x545"));]));])));(`Exists
    ([("x547", `Unknown);], (`Conjunction [(`Predicate ("abLost",
    [(`Unknown, (`Variable "x545"));(`Unknown, (`Variable
      "x548"));(`Unknown, (`Variable "x547"));]));(`Equality ((`Unknown,
    (`Variable "x547")), (`Unknown, (`Variable
      "a'"))));])));]));(`Conjunction [(`Exists ([("x542", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x542")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x542"));(`Unknown, (`Variable "x545"));]));])));(`Exists ([("x546",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x545"));(`Unknown, (`Variable "x548"));(`Unknown, (`Variable
    "x546"));]));(`Equality ((`Unknown, (`Variable "x546")), (`Unknown,
  (`Variable "a"))));])));]);])));]);]);]);]));(`Conjunction [(`Negation
  (`Exists ([("x541", `Unknown);], (`Conjunction [(`Exists ([("x540",
  `Unknown);], (`Conjunction [(`Exists ([("x539", `Unknown);],
  (`Conjunction [(`Exists ([("x538", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x538")), (`Unknown, (`Variable
      "a'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x538"));(`Unknown, (`Variable "x539"));]));])));(`Predicate
    ("abBalance", [(`Unknown, (`Variable "x539"));(`Unknown, (`Variable
      "x541"));(`Unknown, (`Variable "x540"));]));])));(`Equality
    ((`Unknown, (`Variable "x540")), (`Unknown, (`Variable
      "a'"))));])));(`Exists ([("x537", `Unknown);], (`Conjunction
    [(`Exists ([("x536", `Unknown);], (`Conjunction [(`Exists ([("x535",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x535")),
    (`Unknown, (`Variable "a'"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x535"));(`Unknown, (`Variable "x536"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x536"));(`Unknown, (`Variable
        "x541"));(`Unknown, (`Variable "x537"));]));])));(`Equality
      ((`Unknown, (`Variable "x537")), (`Unknown, (`Variable
        "a'"))));])));]))));(`Forall ([("c", `Unknown);], (`Disjunction
  [(`Negation (`Conjunction [(`Predicate ("Coin", [(`Unknown, (`Variable
    "c"));]));]));(`Forall ([("x531", `Unknown);("x532", `Unknown);],
  (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
    ([("x530", `Unknown);], (`Conjunction [(`Exists ([("x534", `Unknown);],
    (`Conjunction [(`Disjunction [(`Predicate ("abBalance", [(`Unknown,
    (`Variable "x531"));(`Unknown, (`Variable "x530"));(`Unknown,
    (`Variable "x534"));]));(`Predicate ("abLost", [(`Unknown, (`Variable
      "x531"));(`Unknown, (`Variable "x530"));(`Unknown, (`Variable
      "x534"));]));]);(`Equality ((`Unknown, (`Variable "x534")),
    (`Unknown, (`Variable "a'"))));])));(`Equality ((`Unknown, (`Variable
      "x530")), (`Unknown, (`Variable "c"))));])));(`Exists ([("x528",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x528")),
  (`Unknown, (`Variable "a'"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x528"));(`Unknown, (`Variable
    "x531"));]));])));]);(`Conjunction [(`Exists ([("x530", `Unknown);],
  (`Conjunction [(`Exists ([("x533", `Unknown);], (`Conjunction
    [(`Disjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
      "x532"));(`Unknown, (`Variable "x530"));(`Unknown, (`Variable
      "x533"));]));(`Predicate ("abLost", [(`Unknown, (`Variable
      "x532"));(`Unknown, (`Variable "x530"));(`Unknown, (`Variable
      "x533"));]));]);(`Equality ((`Unknown, (`Variable "x533")),
    (`Unknown, (`Variable "a'"))));])));(`Equality ((`Unknown, (`Variable
    "x530")), (`Unknown, (`Variable "c"))));])));(`Exists ([("x528",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x528")),
  (`Unknown, (`Variable "a'"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x528"));(`Unknown, (`Variable
    "x532"));]));])));]);]));(`Conjunction [(`Equality ((`Unknown,
  (`Variable "x531")), (`Unknown, (`Variable
    "x532"))));]);])));])));]);]);])));])); 
("AbOp_total",(`Conjunction [(`Forall ([("a", `Unknown);("a_in",
`Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Predicate
  ("AbWorld", [(`Unknown, (`Variable "a"));]));(`Predicate ("AIN",
[(`Unknown, (`Variable "a_in"));]));]));(`Disjunction [(`Negation
  (`Conjunction [(`Negation (`Exists ([("x527", `Unknown);], (`Conjunction
    [(`Exists ([("x526", `Unknown);], (`Conjunction [(`Exists ([("x525",
    `Unknown);], (`Conjunction [(`Exists ([("x524", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x524")), (`Unknown,
    (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x524"));(`Unknown, (`Variable "x525"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x525"));(`Unknown, (`Variable
        "x527"));(`Unknown, (`Variable "x526"));]));])));(`Equality
      ((`Unknown, (`Variable "x526")), (`Unknown, (`Variable
        "a"))));])));(`Exists ([("x523", `Unknown);], (`Conjunction
      [(`Exists ([("x522", `Unknown);], (`Conjunction [(`Exists ([("x521",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x521")), (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse",
      [(`Unknown, (`Variable "x521"));(`Unknown, (`Variable
        "x522"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
        "x522"));(`Unknown, (`Variable "x527"));(`Unknown, (`Variable
        "x523"));]));])));(`Equality ((`Unknown, (`Variable "x523")),
      (`Unknown, (`Variable "a"))));])));]))));(`Forall ([("c",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Predicate
    ("Coin", [(`Unknown, (`Variable "c"));]));]));(`Forall ([("x517",
  `Unknown);("x518", `Unknown);], (`Disjunction [(`Negation (`Conjunction
    [(`Conjunction [(`Exists ([("x516", `Unknown);], (`Conjunction
      [(`Exists ([("x520", `Unknown);], (`Conjunction [(`Disjunction
        [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x517"));(`Unknown, (`Variable "x516"));(`Unknown, (`Variable
          "x520"));]));(`Predicate ("abLost", [(`Unknown, (`Variable
          "x517"));(`Unknown, (`Variable "x516"));(`Unknown, (`Variable
          "x520"));]));]);(`Equality ((`Unknown, (`Variable "x520")),
      (`Unknown, (`Variable "a"))));])));(`Equality ((`Unknown, (`Variable
        "x516")), (`Unknown, (`Variable "c"))));])));(`Exists ([("x514",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x514")),
    (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x514"));(`Unknown, (`Variable
      "x517"));]));])));]);(`Conjunction [(`Exists ([("x516", `Unknown);],
    (`Conjunction [(`Exists ([("x519", `Unknown);], (`Conjunction
      [(`Disjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
        "x518"));(`Unknown, (`Variable "x516"));(`Unknown, (`Variable
        "x519"));]));(`Predicate ("abLost", [(`Unknown, (`Variable
        "x518"));(`Unknown, (`Variable "x516"));(`Unknown, (`Variable
        "x519"));]));]);(`Equality ((`Unknown, (`Variable "x519")),
      (`Unknown, (`Variable "a"))));])));(`Equality ((`Unknown, (`Variable
      "x516")), (`Unknown, (`Variable "c"))));])));(`Exists ([("x514",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x514")),
    (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x514"));(`Unknown, (`Variable
      "x518"));]));])));]);]));(`Conjunction [(`Equality ((`Unknown,
  (`Variable "x517")), (`Unknown, (`Variable
    "x518"))));]);])));])));]));(`Conjunction [(`Conjunction [(`Conjunction
  [(`Conjunction [(`Forall ([("x513", `Unknown);], (`Disjunction
    [(`Negation (`Predicate ("aNullOut", [(`Unknown, (`Variable
      "x513"));])));(`Predicate ("aNullOut", [(`Unknown, (`Variable
      "x513"));]));])));(`Forall ([("x512", `Unknown);], (`Disjunction
    [(`Negation (`Predicate ("aNullOut", [(`Unknown, (`Variable
      "x512"));])));(`Predicate ("aNullOut", [(`Unknown, (`Variable
      "x512"));]));])));]);]);(`Conjunction [(`Forall ([("x511",
`Unknown);], (`Disjunction [(`Negation (`Exists ([("x509", `Unknown);],
(`Conjunction [(`Equality ((`Unknown, (`Variable "x509")), (`Unknown,
(`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
  "x509"));(`Unknown, (`Variable "x511"));]));]))));(`Exists ([("x508",
`Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x508")),
(`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
(`Variable "x508"));(`Unknown, (`Variable "x511"));]));])));])));(`Forall
  ([("x510", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x508",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x508")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x508"));(`Unknown, (`Variable "x510"));]));]))));(`Exists
    ([("x509", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x509")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x509"));(`Unknown, (`Variable
        "x510"));]));])));])));]);(`Conjunction [(`Conjunction [(`Forall
  ([("x507", `Unknown);("x504", `Unknown);], (`Disjunction [(`Negation
    (`Conjunction [(`Exists ([("x487", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x487")), (`Unknown, (`Variable
        "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x487"));(`Unknown, (`Variable "x504"));]));])));(`Exists
      ([("x506", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x504"));(`Unknown, (`Variable
        "x507"));(`Unknown, (`Variable "x506"));]));(`Equality ((`Unknown,
      (`Variable "x506")), (`Unknown, (`Variable
        "a"))));])));]));(`Conjunction [(`Exists ([("x487", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x487")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x487"));(`Unknown, (`Variable "x504"));]));])));(`Exists ([("x505",
  `Unknown);], (`Conjunction [(`Predicate ("abBalance", [(`Unknown,
  (`Variable "x504"));(`Unknown, (`Variable "x507"));(`Unknown, (`Variable
    "x505"));]));(`Equality ((`Unknown, (`Variable "x505")), (`Unknown,
  (`Variable "a"))));])));]);])));(`Forall ([("x503", `Unknown);("x500",
`Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x487",
`Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x487")),
(`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
(`Variable "x487"));(`Unknown, (`Variable "x500"));]));])));(`Exists
  ([("x502", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
  [(`Unknown, (`Variable "x500"));(`Unknown, (`Variable "x503"));(`Unknown,
  (`Variable "x502"));]));(`Equality ((`Unknown, (`Variable "x502")),
  (`Unknown, (`Variable "a"))));])));]));(`Conjunction [(`Exists ([("x487",
`Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x487")),
(`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
(`Variable "x487"));(`Unknown, (`Variable "x500"));]));])));(`Exists
  ([("x501", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
  [(`Unknown, (`Variable "x500"));(`Unknown, (`Variable "x503"));(`Unknown,
  (`Variable "x501"));]));(`Equality ((`Unknown, (`Variable "x501")),
  (`Unknown, (`Variable "a"))));])));]);])));]);(`Conjunction [(`Forall
  ([("x497", `Unknown);("x494", `Unknown);], (`Disjunction [(`Negation
    (`Conjunction [(`Exists ([("x487", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x487")), (`Unknown, (`Variable
        "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x487"));(`Unknown, (`Variable "x494"));]));])));(`Exists
      ([("x496", `Unknown);], (`Conjunction [(`Predicate ("abLost",
      [(`Unknown, (`Variable "x494"));(`Unknown, (`Variable
        "x497"));(`Unknown, (`Variable "x496"));]));(`Equality ((`Unknown,
      (`Variable "x496")), (`Unknown, (`Variable
        "a"))));])));]));(`Conjunction [(`Exists ([("x487", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x487")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x487"));(`Unknown, (`Variable "x494"));]));])));(`Exists ([("x495",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x494"));(`Unknown, (`Variable "x497"));(`Unknown, (`Variable
    "x495"));]));(`Equality ((`Unknown, (`Variable "x495")), (`Unknown,
  (`Variable "a"))));])));]);])));(`Forall ([("x493", `Unknown);("x490",
`Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x487",
`Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x487")),
(`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
(`Variable "x487"));(`Unknown, (`Variable "x490"));]));])));(`Exists
  ([("x492", `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown,
  (`Variable "x490"));(`Unknown, (`Variable "x493"));(`Unknown, (`Variable
    "x492"));]));(`Equality ((`Unknown, (`Variable "x492")), (`Unknown,
  (`Variable "a"))));])));]));(`Conjunction [(`Exists ([("x487",
`Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x487")),
(`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
(`Variable "x487"));(`Unknown, (`Variable "x490"));]));])));(`Exists
  ([("x491", `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown,
  (`Variable "x490"));(`Unknown, (`Variable "x493"));(`Unknown, (`Variable
    "x491"));]));(`Equality ((`Unknown, (`Variable "x491")), (`Unknown,
  (`Variable "a"))));])));]);])));]);]);]);(`Conjunction [(`Disjunction
  [(`Conjunction [(`Conjunction [(`Conjunction [(`Conjunction [(`Forall
    ([("x486", `Unknown);], (`Disjunction [(`Negation (`Predicate
      ("aNullOut", [(`Unknown, (`Variable "x486"));])));(`Predicate
      ("aNullOut", [(`Unknown, (`Variable "x486"));]));])));(`Forall
    ([("x485", `Unknown);], (`Disjunction [(`Negation (`Predicate
      ("aNullOut", [(`Unknown, (`Variable "x485"));])));(`Predicate
      ("aNullOut", [(`Unknown, (`Variable "x485"));]));])));]);]);(`Forall
    ([("x484", `Unknown);], (`Disjunction [(`Negation (`Equality
      ((`Unknown, (`Variable "x484")), (`Unknown, (`Variable
        "a_in")))));(`Predicate ("TransferDetails", [(`Unknown, (`Variable
      "x484"));]));])));(`Conjunction [(`Forall ([("x483", `Unknown);],
  (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
    ([("x481", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x481")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x481"));(`Unknown, (`Variable
        "x483"));]));])));(`Negation (`Exists ([("x480", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x480")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x480"));(`Unknown, (`Variable "x483"));]));]))));]);(`Negation
    (`Exists ([("x479", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x479")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x479"));(`Unknown, (`Variable
        "x483"));]));]))));]));(`Conjunction [(`Conjunction [(`Exists
    ([("x478", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x478")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x478"));(`Unknown, (`Variable
        "x483"));]));])));(`Negation (`Exists ([("x477", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x477")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x477"));(`Unknown, (`Variable "x483"));]));]))));]);(`Negation
    (`Exists ([("x476", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x476")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x476"));(`Unknown, (`Variable
        "x483"));]));]))));]);])));(`Forall ([("x482", `Unknown);],
  (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
    ([("x478", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x478")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x478"));(`Unknown, (`Variable
        "x482"));]));])));(`Negation (`Exists ([("x477", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x477")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x477"));(`Unknown, (`Variable "x482"));]));]))));]);(`Negation
    (`Exists ([("x476", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x476")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x476"));(`Unknown, (`Variable
        "x482"));]));]))));]));(`Conjunction [(`Conjunction [(`Exists
    ([("x481", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x481")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x481"));(`Unknown, (`Variable
        "x482"));]));])));(`Negation (`Exists ([("x480", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x480")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x480"));(`Unknown, (`Variable "x482"));]));]))));]);(`Negation
    (`Exists ([("x479", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x479")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x479"));(`Unknown, (`Variable
        "x482"));]));]))));]);])));]);(`Conjunction [(`Conjunction
    [(`Forall ([("x475", `Unknown);("x472", `Unknown);], (`Disjunction
      [(`Negation (`Conjunction [(`Conjunction [(`Conjunction [(`Exists
        ([("x455", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
        (`Variable "x455")), (`Unknown, (`Variable "a"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x455"));(`Unknown,
          (`Variable "x472"));]));])));(`Negation (`Exists ([("x454",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x454")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
      [(`Unknown, (`Variable "x454"));(`Unknown, (`Variable
        "x472"));]));]))));]);(`Negation (`Exists ([("x453", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x453")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x453"));(`Unknown, (`Variable "x472"));]));]))));]);(`Exists
        ([("x474", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
        [(`Unknown, (`Variable "x472"));(`Unknown, (`Variable
          "x475"));(`Unknown, (`Variable "x474"));]));(`Equality
          ((`Unknown, (`Variable "x474")), (`Unknown, (`Variable
            "a"))));])));]));(`Conjunction [(`Conjunction [(`Conjunction
        [(`Exists ([("x455", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x455")), (`Unknown, (`Variable
            "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x455"));(`Unknown, (`Variable "x472"));]));])));(`Negation
          (`Exists ([("x454", `Unknown);], (`Conjunction [(`Equality
            ((`Unknown, (`Variable "x454")), (`Unknown, (`Variable
              "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
            "x454"));(`Unknown, (`Variable "x472"));]));]))));]);(`Negation
        (`Exists ([("x453", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x453")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x453"));(`Unknown, (`Variable "x472"));]));]))));]);(`Exists
        ([("x473", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
        [(`Unknown, (`Variable "x472"));(`Unknown, (`Variable
          "x475"));(`Unknown, (`Variable "x473"));]));(`Equality
          ((`Unknown, (`Variable "x473")), (`Unknown, (`Variable
            "a"))));])));]);])));(`Forall ([("x471", `Unknown);("x468",
    `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Conjunction
      [(`Conjunction [(`Exists ([("x455", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x455")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x455"));(`Unknown, (`Variable "x468"));]));])));(`Negation
        (`Exists ([("x454", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x454")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x454"));(`Unknown, (`Variable "x468"));]));]))));]);(`Negation
        (`Exists ([("x453", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x453")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x453"));(`Unknown, (`Variable "x468"));]));]))));]);(`Exists
      ([("x470", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x468"));(`Unknown, (`Variable
        "x471"));(`Unknown, (`Variable "x470"));]));(`Equality ((`Unknown,
      (`Variable "x470")), (`Unknown, (`Variable
        "a"))));])));]));(`Conjunction [(`Conjunction [(`Conjunction
      [(`Exists ([("x455", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x455")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x455"));(`Unknown, (`Variable "x468"));]));])));(`Negation
        (`Exists ([("x454", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x454")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x454"));(`Unknown, (`Variable "x468"));]));]))));]);(`Negation
      (`Exists ([("x453", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x453")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x453"));(`Unknown, (`Variable "x468"));]));]))));]);(`Exists
      ([("x469", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x468"));(`Unknown, (`Variable
        "x471"));(`Unknown, (`Variable "x469"));]));(`Equality ((`Unknown,
      (`Variable "x469")), (`Unknown, (`Variable
        "a"))));])));]);])));]);(`Conjunction [(`Forall ([("x465",
  `Unknown);("x462", `Unknown);], (`Disjunction [(`Negation (`Conjunction
    [(`Conjunction [(`Conjunction [(`Exists ([("x455", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x455")), (`Unknown,
    (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x455"));(`Unknown, (`Variable "x462"));]));])));(`Negation (`Exists
      ([("x454", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x454")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("from", [(`Unknown, (`Variable "x454"));(`Unknown, (`Variable
          "x462"));]));]))));]);(`Negation (`Exists ([("x453", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x453")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x453"));(`Unknown, (`Variable "x462"));]));]))));]);(`Exists
      ([("x464", `Unknown);], (`Conjunction [(`Predicate ("abLost",
      [(`Unknown, (`Variable "x462"));(`Unknown, (`Variable
        "x465"));(`Unknown, (`Variable "x464"));]));(`Equality ((`Unknown,
      (`Variable "x464")), (`Unknown, (`Variable
        "a"))));])));]));(`Conjunction [(`Conjunction [(`Conjunction
    [(`Exists ([("x455", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x455")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x455"));(`Unknown, (`Variable
        "x462"));]));])));(`Negation (`Exists ([("x454", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x454")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
      "x454"));(`Unknown, (`Variable "x462"));]));]))));]);(`Negation
    (`Exists ([("x453", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x453")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x453"));(`Unknown, (`Variable
        "x462"));]));]))));]);(`Exists ([("x463", `Unknown);],
  (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x462"));(`Unknown, (`Variable "x465"));(`Unknown, (`Variable
    "x463"));]));(`Equality ((`Unknown, (`Variable "x463")), (`Unknown,
  (`Variable "a"))));])));]);])));(`Forall ([("x461", `Unknown);("x458",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Conjunction
    [(`Conjunction [(`Exists ([("x455", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x455")), (`Unknown, (`Variable
        "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x455"));(`Unknown, (`Variable "x458"));]));])));(`Negation
      (`Exists ([("x454", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x454")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x454"));(`Unknown, (`Variable "x458"));]));]))));]);(`Negation
      (`Exists ([("x453", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x453")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x453"));(`Unknown, (`Variable "x458"));]));]))));]);(`Exists
    ([("x460", `Unknown);], (`Conjunction [(`Predicate ("abLost",
    [(`Unknown, (`Variable "x458"));(`Unknown, (`Variable
      "x461"));(`Unknown, (`Variable "x460"));]));(`Equality ((`Unknown,
    (`Variable "x460")), (`Unknown, (`Variable
      "a"))));])));]));(`Conjunction [(`Conjunction [(`Conjunction
    [(`Exists ([("x455", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x455")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x455"));(`Unknown, (`Variable
        "x458"));]));])));(`Negation (`Exists ([("x454", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x454")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
      "x454"));(`Unknown, (`Variable "x458"));]));]))));]);(`Negation
    (`Exists ([("x453", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x453")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x453"));(`Unknown, (`Variable
        "x458"));]));]))));]);(`Exists ([("x459", `Unknown);],
  (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x458"));(`Unknown, (`Variable "x461"));(`Unknown, (`Variable
    "x459"));]));(`Equality ((`Unknown, (`Variable "x459")), (`Unknown,
  (`Variable "a"))));])));]);])));]);]);]);(`Conjunction [(`Forall
    ([("x452", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x450",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x450")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x450"));(`Unknown, (`Variable "x452"));]));]))));(`Exists
      ([("x451", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x451")), (`Unknown, (`Variable "a"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x451"));(`Unknown,
        (`Variable "x452"));]));])));])));]);(`Conjunction [(`Forall
    ([("x449", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x447",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x447")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
    (`Variable "x447"));(`Unknown, (`Variable "x449"));]));]))));(`Exists
      ([("x448", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x448")), (`Unknown, (`Variable "a"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x448"));(`Unknown,
        (`Variable "x449"));]));])));])));]);(`Conjunction [(`Forall
    ([("x446", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x445",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x445")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
    (`Variable "x445"));(`Unknown, (`Variable "x446"));]));]))));(`Exists
      ([("x444", `Unknown);], (`Conjunction [(`Exists ([("x443",
      `Unknown);], (`Conjunction [(`Exists ([("x442", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x442")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x442"));(`Unknown, (`Variable "x443"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x443"));(`Unknown, (`Variable
          "x446"));(`Unknown, (`Variable "x444"));]));])));(`Equality
        ((`Unknown, (`Variable "x444")), (`Unknown, (`Variable
          "a"))));])));])));]);(`Negation (`Exists ([("x441", `Unknown);],
  (`Conjunction [(`Exists ([("x440", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x440")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x440"));(`Unknown, (`Variable "x441"));]));])));(`Exists ([("x439",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x439")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
  (`Variable "x439"));(`Unknown, (`Variable
    "x441"));]));])));]))));(`Conjunction [(`Forall ([("x438", `Unknown);],
  (`Disjunction [(`Negation (`Exists ([("x436", `Unknown);], (`Conjunction
    [(`Exists ([("x435", `Unknown);], (`Conjunction [(`Exists ([("x434",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x434")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x434"));(`Unknown, (`Variable "x435"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x435"));(`Unknown, (`Variable
        "x438"));(`Unknown, (`Variable "x436"));]));])));(`Equality
      ((`Unknown, (`Variable "x436")), (`Unknown, (`Variable
        "a"))));]))));(`Conjunction [(`Exists ([("x433", `Unknown);],
  (`Conjunction [(`Exists ([("x432", `Unknown);], (`Conjunction [(`Exists
    ([("x431", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x431")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x431"));(`Unknown, (`Variable
        "x432"));]));])));(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x432"));(`Unknown, (`Variable "x438"));(`Unknown, (`Variable
    "x433"));]));])));(`Equality ((`Unknown, (`Variable "x433")),
  (`Unknown, (`Variable "a"))));])));(`Negation (`Exists ([("x430",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x430")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
  (`Variable "x430"));(`Unknown, (`Variable
    "x438"));]));]))));]);])));(`Forall ([("x437", `Unknown);],
  (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x433", `Unknown);],
  (`Conjunction [(`Exists ([("x432", `Unknown);], (`Conjunction [(`Exists
    ([("x431", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x431")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x431"));(`Unknown, (`Variable
        "x432"));]));])));(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x432"));(`Unknown, (`Variable "x437"));(`Unknown, (`Variable
    "x433"));]));])));(`Equality ((`Unknown, (`Variable "x433")),
  (`Unknown, (`Variable "a"))));])));(`Negation (`Exists ([("x430",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x430")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
  (`Variable "x430"));(`Unknown, (`Variable "x437"));]));]))));]));(`Exists
    ([("x436", `Unknown);], (`Conjunction [(`Exists ([("x435", `Unknown);],
    (`Conjunction [(`Exists ([("x434", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x434")), (`Unknown, (`Variable
        "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x434"));(`Unknown, (`Variable "x435"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x435"));(`Unknown, (`Variable
        "x437"));(`Unknown, (`Variable "x436"));]));])));(`Equality
      ((`Unknown, (`Variable "x436")), (`Unknown, (`Variable
        "a"))));])));])));]);(`Conjunction [(`Forall ([("x429",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x427", `Unknown);],
  (`Conjunction [(`Exists ([("x426", `Unknown);], (`Conjunction [(`Exists
    ([("x425", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x425")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x425"));(`Unknown, (`Variable
        "x426"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
    "x426"));(`Unknown, (`Variable "x429"));(`Unknown, (`Variable
    "x427"));]));])));(`Equality ((`Unknown, (`Variable "x427")),
  (`Unknown, (`Variable "a"))));]))));(`Exists ([("x424", `Unknown);],
  (`Conjunction [(`Exists ([("x423", `Unknown);], (`Conjunction [(`Exists
    ([("x422", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x422")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x422"));(`Unknown, (`Variable
        "x423"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
    "x423"));(`Unknown, (`Variable "x429"));(`Unknown, (`Variable
    "x424"));]));])));(`Equality ((`Unknown, (`Variable "x424")),
  (`Unknown, (`Variable "a"))));])));])));(`Forall ([("x428", `Unknown);],
  (`Disjunction [(`Negation (`Exists ([("x424", `Unknown);], (`Conjunction
    [(`Exists ([("x423", `Unknown);], (`Conjunction [(`Exists ([("x422",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x422")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x422"));(`Unknown, (`Variable "x423"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x423"));(`Unknown, (`Variable
        "x428"));(`Unknown, (`Variable "x424"));]));])));(`Equality
      ((`Unknown, (`Variable "x424")), (`Unknown, (`Variable
        "a"))));]))));(`Exists ([("x427", `Unknown);], (`Conjunction
    [(`Exists ([("x426", `Unknown);], (`Conjunction [(`Exists ([("x425",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x425")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x425"));(`Unknown, (`Variable "x426"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x426"));(`Unknown, (`Variable
        "x428"));(`Unknown, (`Variable "x427"));]));])));(`Equality
      ((`Unknown, (`Variable "x427")), (`Unknown, (`Variable
        "a"))));])));])));]);(`Conjunction [(`Forall ([("x421",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x419", `Unknown);],
  (`Conjunction [(`Exists ([("x418", `Unknown);], (`Conjunction [(`Exists
    ([("x417", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x417")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x417"));(`Unknown, (`Variable
        "x418"));]));])));(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x418"));(`Unknown, (`Variable "x421"));(`Unknown, (`Variable
    "x419"));]));])));(`Equality ((`Unknown, (`Variable "x419")),
  (`Unknown, (`Variable "a"))));]))));(`Disjunction [(`Exists ([("x416",
  `Unknown);], (`Conjunction [(`Exists ([("x415", `Unknown);],
  (`Conjunction [(`Exists ([("x414", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x414")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x414"));(`Unknown, (`Variable "x415"));]));])));(`Predicate
    ("abBalance", [(`Unknown, (`Variable "x415"));(`Unknown, (`Variable
      "x421"));(`Unknown, (`Variable "x416"));]));])));(`Equality
    ((`Unknown, (`Variable "x416")), (`Unknown, (`Variable
      "a"))));])));(`Exists ([("x413", `Unknown);], (`Conjunction
    [(`Equality ((`Unknown, (`Variable "x413")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
      "x413"));(`Unknown, (`Variable "x421"));]));])));]);])));(`Forall
    ([("x420", `Unknown);], (`Disjunction [(`Negation (`Disjunction
      [(`Exists ([("x416", `Unknown);], (`Conjunction [(`Exists ([("x415",
      `Unknown);], (`Conjunction [(`Exists ([("x414", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x414")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x414"));(`Unknown, (`Variable "x415"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x415"));(`Unknown, (`Variable
          "x420"));(`Unknown, (`Variable "x416"));]));])));(`Equality
        ((`Unknown, (`Variable "x416")), (`Unknown, (`Variable
          "a"))));])));(`Exists ([("x413", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x413")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
          "x413"));(`Unknown, (`Variable "x420"));]));])));]));(`Exists
      ([("x419", `Unknown);], (`Conjunction [(`Exists ([("x418",
      `Unknown);], (`Conjunction [(`Exists ([("x417", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x417")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x417"));(`Unknown, (`Variable "x418"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x418"));(`Unknown, (`Variable
          "x420"));(`Unknown, (`Variable "x419"));]));])));(`Equality
        ((`Unknown, (`Variable "x419")), (`Unknown, (`Variable
          "a"))));])));])));]);(`Conjunction [(`Forall ([("x412",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x410", `Unknown);],
  (`Conjunction [(`Exists ([("x409", `Unknown);], (`Conjunction [(`Exists
    ([("x408", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x408")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x408"));(`Unknown, (`Variable
        "x409"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
    "x409"));(`Unknown, (`Variable "x412"));(`Unknown, (`Variable
    "x410"));]));])));(`Equality ((`Unknown, (`Variable "x410")),
  (`Unknown, (`Variable "a"))));]))));(`Exists ([("x407", `Unknown);],
  (`Conjunction [(`Exists ([("x406", `Unknown);], (`Conjunction [(`Exists
    ([("x405", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x405")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x405"));(`Unknown, (`Variable
        "x406"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
    "x406"));(`Unknown, (`Variable "x412"));(`Unknown, (`Variable
    "x407"));]));])));(`Equality ((`Unknown, (`Variable "x407")),
  (`Unknown, (`Variable "a"))));])));])));(`Forall ([("x411", `Unknown);],
  (`Disjunction [(`Negation (`Exists ([("x407", `Unknown);], (`Conjunction
    [(`Exists ([("x406", `Unknown);], (`Conjunction [(`Exists ([("x405",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x405")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
    (`Variable "x405"));(`Unknown, (`Variable "x406"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x406"));(`Unknown, (`Variable
        "x411"));(`Unknown, (`Variable "x407"));]));])));(`Equality
      ((`Unknown, (`Variable "x407")), (`Unknown, (`Variable
        "a"))));]))));(`Exists ([("x410", `Unknown);], (`Conjunction
    [(`Exists ([("x409", `Unknown);], (`Conjunction [(`Exists ([("x408",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x408")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
    (`Variable "x408"));(`Unknown, (`Variable "x409"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x409"));(`Unknown, (`Variable
        "x411"));(`Unknown, (`Variable "x410"));]));])));(`Equality
      ((`Unknown, (`Variable "x410")), (`Unknown, (`Variable
        "a"))));])));])));]);(`Conjunction [(`Forall ([("x404",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x402", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x402")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x402"));(`Unknown, (`Variable "x404"));]));]))));(`Exists ([("x403",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x403")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x403"));(`Unknown, (`Variable
    "x404"));]));])));])));]);(`Conjunction [(`Forall ([("x401",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x399", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x399")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x399"));(`Unknown, (`Variable "x401"));]));]))));(`Exists ([("x400",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x400")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x400"));(`Unknown, (`Variable
    "x401"));]));])));])));]);]);(`Conjunction [(`Conjunction
    [(`Conjunction [(`Conjunction [(`Forall ([("x398", `Unknown);],
    (`Disjunction [(`Negation (`Predicate ("aNullOut", [(`Unknown,
    (`Variable "x398"));])));(`Predicate ("aNullOut", [(`Unknown,
    (`Variable "x398"));]));])));(`Forall ([("x397", `Unknown);],
    (`Disjunction [(`Negation (`Predicate ("aNullOut", [(`Unknown,
    (`Variable "x397"));])));(`Predicate ("aNullOut", [(`Unknown,
    (`Variable "x397"));]));])));]);]);(`Forall ([("x396", `Unknown);],
    (`Disjunction [(`Negation (`Equality ((`Unknown, (`Variable "x396")),
    (`Unknown, (`Variable "a_in")))));(`Predicate ("TransferDetails",
    [(`Unknown, (`Variable "x396"));]));])));(`Conjunction [(`Forall
      ([("x395", `Unknown);], (`Disjunction [(`Negation (`Conjunction
        [(`Conjunction [(`Exists ([("x393", `Unknown);], (`Conjunction
          [(`Equality ((`Unknown, (`Variable "x393")), (`Unknown,
          (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
          (`Variable "x393"));(`Unknown, (`Variable
            "x395"));]));])));(`Negation (`Exists ([("x392", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x392")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
        (`Variable "x392"));(`Unknown, (`Variable
          "x395"));]));]))));]);(`Negation (`Exists ([("x391", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x391")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x391"));(`Unknown, (`Variable
          "x395"));]));]))));]));(`Conjunction [(`Conjunction [(`Exists
        ([("x390", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
        (`Variable "x390")), (`Unknown, (`Variable "a"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x390"));(`Unknown,
          (`Variable "x395"));]));])));(`Negation (`Exists ([("x389",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x389")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
      [(`Unknown, (`Variable "x389"));(`Unknown, (`Variable
        "x395"));]));]))));]);(`Negation (`Exists ([("x388", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x388")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x388"));(`Unknown, (`Variable "x395"));]));]))));]);])));(`Forall
      ([("x394", `Unknown);], (`Disjunction [(`Negation (`Conjunction
        [(`Conjunction [(`Exists ([("x390", `Unknown);], (`Conjunction
          [(`Equality ((`Unknown, (`Variable "x390")), (`Unknown,
          (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
          (`Variable "x390"));(`Unknown, (`Variable
            "x394"));]));])));(`Negation (`Exists ([("x389", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x389")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
        (`Variable "x389"));(`Unknown, (`Variable
          "x394"));]));]))));]);(`Negation (`Exists ([("x388", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x388")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x388"));(`Unknown, (`Variable
          "x394"));]));]))));]));(`Conjunction [(`Conjunction [(`Exists
        ([("x393", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
        (`Variable "x393")), (`Unknown, (`Variable "a"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x393"));(`Unknown,
          (`Variable "x394"));]));])));(`Negation (`Exists ([("x392",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x392")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
      [(`Unknown, (`Variable "x392"));(`Unknown, (`Variable
        "x394"));]));]))));]);(`Negation (`Exists ([("x391", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x391")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x391"));(`Unknown, (`Variable
        "x394"));]));]))));]);])));]);(`Conjunction [(`Conjunction
      [(`Forall ([("x387", `Unknown);("x384", `Unknown);], (`Disjunction
        [(`Negation (`Conjunction [(`Conjunction [(`Conjunction [(`Exists
          ([("x367", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x367")), (`Unknown, (`Variable "a"))));(`Predicate
            ("abAuthPurse", [(`Unknown, (`Variable "x367"));(`Unknown,
            (`Variable "x384"));]));])));(`Negation (`Exists ([("x366",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x366")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x366"));(`Unknown, (`Variable
          "x384"));]));]))));]);(`Negation (`Exists ([("x365", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x365")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x365"));(`Unknown, (`Variable
          "x384"));]));]))));]);(`Exists ([("x386", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x384"));(`Unknown, (`Variable "x387"));(`Unknown, (`Variable
          "x386"));]));(`Equality ((`Unknown, (`Variable "x386")),
        (`Unknown, (`Variable "a"))));])));]));(`Conjunction [(`Conjunction
          [(`Conjunction [(`Exists ([("x367", `Unknown);], (`Conjunction
            [(`Equality ((`Unknown, (`Variable "x367")), (`Unknown,
            (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
            (`Variable "x367"));(`Unknown, (`Variable
              "x384"));]));])));(`Negation (`Exists ([("x366", `Unknown);],
          (`Conjunction [(`Equality ((`Unknown, (`Variable "x366")),
          (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
          (`Variable "x366"));(`Unknown, (`Variable
            "x384"));]));]))));]);(`Negation (`Exists ([("x365",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x365")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x365"));(`Unknown, (`Variable
            "x384"));]));]))));]);(`Exists ([("x385", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x384"));(`Unknown, (`Variable "x387"));(`Unknown, (`Variable
          "x385"));]));(`Equality ((`Unknown, (`Variable "x385")),
        (`Unknown, (`Variable "a"))));])));]);])));(`Forall ([("x383",
      `Unknown);("x380", `Unknown);], (`Disjunction [(`Negation
        (`Conjunction [(`Conjunction [(`Conjunction [(`Exists ([("x367",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x367")), (`Unknown, (`Variable "a"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x367"));(`Unknown,
          (`Variable "x380"));]));])));(`Negation (`Exists ([("x366",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x366")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x366"));(`Unknown, (`Variable
          "x380"));]));]))));]);(`Negation (`Exists ([("x365", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x365")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x365"));(`Unknown, (`Variable
          "x380"));]));]))));]);(`Exists ([("x382", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x380"));(`Unknown, (`Variable "x383"));(`Unknown, (`Variable
          "x382"));]));(`Equality ((`Unknown, (`Variable "x382")),
        (`Unknown, (`Variable "a"))));])));]));(`Conjunction [(`Conjunction
        [(`Conjunction [(`Exists ([("x367", `Unknown);], (`Conjunction
          [(`Equality ((`Unknown, (`Variable "x367")), (`Unknown,
          (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
          (`Variable "x367"));(`Unknown, (`Variable
            "x380"));]));])));(`Negation (`Exists ([("x366", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x366")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
        (`Variable "x366"));(`Unknown, (`Variable
          "x380"));]));]))));]);(`Negation (`Exists ([("x365", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x365")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x365"));(`Unknown, (`Variable
          "x380"));]));]))));]);(`Exists ([("x381", `Unknown);],
      (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
        "x380"));(`Unknown, (`Variable "x383"));(`Unknown, (`Variable
        "x381"));]));(`Equality ((`Unknown, (`Variable "x381")), (`Unknown,
      (`Variable "a"))));])));]);])));]);(`Conjunction [(`Forall ([("x377",
    `Unknown);("x374", `Unknown);], (`Disjunction [(`Negation (`Conjunction
      [(`Conjunction [(`Conjunction [(`Exists ([("x367", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x367")), (`Unknown,
      (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x367"));(`Unknown, (`Variable "x374"));]));])));(`Negation
        (`Exists ([("x366", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x366")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x366"));(`Unknown, (`Variable "x374"));]));]))));]);(`Negation
        (`Exists ([("x365", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x365")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x365"));(`Unknown, (`Variable "x374"));]));]))));]);(`Exists
        ([("x376", `Unknown);], (`Conjunction [(`Predicate ("abLost",
        [(`Unknown, (`Variable "x374"));(`Unknown, (`Variable
          "x377"));(`Unknown, (`Variable "x376"));]));(`Equality
          ((`Unknown, (`Variable "x376")), (`Unknown, (`Variable
            "a"))));])));]));(`Conjunction [(`Conjunction [(`Conjunction
      [(`Exists ([("x367", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x367")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x367"));(`Unknown, (`Variable "x374"));]));])));(`Negation
        (`Exists ([("x366", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x366")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x366"));(`Unknown, (`Variable "x374"));]));]))));]);(`Negation
      (`Exists ([("x365", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x365")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x365"));(`Unknown, (`Variable "x374"));]));]))));]);(`Exists
      ([("x375", `Unknown);], (`Conjunction [(`Predicate ("abLost",
      [(`Unknown, (`Variable "x374"));(`Unknown, (`Variable
        "x377"));(`Unknown, (`Variable "x375"));]));(`Equality ((`Unknown,
      (`Variable "x375")), (`Unknown, (`Variable
        "a"))));])));]);])));(`Forall ([("x373", `Unknown);("x370",
    `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Conjunction
      [(`Conjunction [(`Exists ([("x367", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x367")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x367"));(`Unknown, (`Variable "x370"));]));])));(`Negation
        (`Exists ([("x366", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x366")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x366"));(`Unknown, (`Variable "x370"));]));]))));]);(`Negation
        (`Exists ([("x365", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x365")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x365"));(`Unknown, (`Variable "x370"));]));]))));]);(`Exists
      ([("x372", `Unknown);], (`Conjunction [(`Predicate ("abLost",
      [(`Unknown, (`Variable "x370"));(`Unknown, (`Variable
        "x373"));(`Unknown, (`Variable "x372"));]));(`Equality ((`Unknown,
      (`Variable "x372")), (`Unknown, (`Variable
        "a"))));])));]));(`Conjunction [(`Conjunction [(`Conjunction
      [(`Exists ([("x367", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x367")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x367"));(`Unknown, (`Variable "x370"));]));])));(`Negation
        (`Exists ([("x366", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x366")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x366"));(`Unknown, (`Variable "x370"));]));]))));]);(`Negation
      (`Exists ([("x365", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x365")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x365"));(`Unknown, (`Variable "x370"));]));]))));]);(`Exists
      ([("x371", `Unknown);], (`Conjunction [(`Predicate ("abLost",
      [(`Unknown, (`Variable "x370"));(`Unknown, (`Variable
        "x373"));(`Unknown, (`Variable "x371"));]));(`Equality ((`Unknown,
      (`Variable "x371")), (`Unknown, (`Variable
        "a"))));])));]);])));]);]);]);(`Conjunction [(`Forall ([("x364",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x362", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x362")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x362"));(`Unknown, (`Variable "x364"));]));]))));(`Exists ([("x363",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x363")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x363"));(`Unknown, (`Variable
    "x364"));]));])));])));]);(`Conjunction [(`Forall ([("x361",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x359", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x359")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x359"));(`Unknown, (`Variable "x361"));]));]))));(`Exists ([("x360",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x360")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x360"));(`Unknown, (`Variable
    "x361"));]));])));])));]);(`Conjunction [(`Forall ([("x358",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x357", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x357")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
    "x357"));(`Unknown, (`Variable "x358"));]));]))));(`Exists ([("x356",
  `Unknown);], (`Conjunction [(`Exists ([("x355", `Unknown);],
  (`Conjunction [(`Exists ([("x354", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x354")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x354"));(`Unknown, (`Variable "x355"));]));])));(`Predicate
    ("abBalance", [(`Unknown, (`Variable "x355"));(`Unknown, (`Variable
      "x358"));(`Unknown, (`Variable "x356"));]));])));(`Equality
    ((`Unknown, (`Variable "x356")), (`Unknown, (`Variable
      "a"))));])));])));]);(`Negation (`Exists ([("x353", `Unknown);],
  (`Conjunction [(`Exists ([("x352", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x352")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x352"));(`Unknown, (`Variable "x353"));]));])));(`Exists ([("x351",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x351")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
  (`Variable "x351"));(`Unknown, (`Variable
    "x353"));]));])));]))));(`Conjunction [(`Forall ([("x350", `Unknown);],
  (`Disjunction [(`Negation (`Exists ([("x348", `Unknown);], (`Conjunction
    [(`Exists ([("x347", `Unknown);], (`Conjunction [(`Exists ([("x346",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x346")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x346"));(`Unknown, (`Variable "x347"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x347"));(`Unknown, (`Variable
        "x350"));(`Unknown, (`Variable "x348"));]));])));(`Equality
      ((`Unknown, (`Variable "x348")), (`Unknown, (`Variable
        "a"))));]))));(`Conjunction [(`Exists ([("x345", `Unknown);],
  (`Conjunction [(`Exists ([("x344", `Unknown);], (`Conjunction [(`Exists
    ([("x343", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x343")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x343"));(`Unknown, (`Variable
        "x344"));]));])));(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x344"));(`Unknown, (`Variable "x350"));(`Unknown, (`Variable
    "x345"));]));])));(`Equality ((`Unknown, (`Variable "x345")),
  (`Unknown, (`Variable "a"))));])));(`Negation (`Exists ([("x342",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x342")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
  (`Variable "x342"));(`Unknown, (`Variable
    "x350"));]));]))));]);])));(`Forall ([("x349", `Unknown);],
  (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x345", `Unknown);],
  (`Conjunction [(`Exists ([("x344", `Unknown);], (`Conjunction [(`Exists
    ([("x343", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x343")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x343"));(`Unknown, (`Variable
        "x344"));]));])));(`Predicate ("abBalance", [(`Unknown, (`Variable
    "x344"));(`Unknown, (`Variable "x349"));(`Unknown, (`Variable
    "x345"));]));])));(`Equality ((`Unknown, (`Variable "x345")),
  (`Unknown, (`Variable "a"))));])));(`Negation (`Exists ([("x342",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x342")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
  (`Variable "x342"));(`Unknown, (`Variable "x349"));]));]))));]));(`Exists
    ([("x348", `Unknown);], (`Conjunction [(`Exists ([("x347", `Unknown);],
    (`Conjunction [(`Exists ([("x346", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x346")), (`Unknown, (`Variable
        "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x346"));(`Unknown, (`Variable "x347"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x347"));(`Unknown, (`Variable
        "x349"));(`Unknown, (`Variable "x348"));]));])));(`Equality
      ((`Unknown, (`Variable "x348")), (`Unknown, (`Variable
        "a"))));])));])));]);(`Conjunction [(`Forall ([("x341",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x339", `Unknown);],
  (`Conjunction [(`Exists ([("x338", `Unknown);], (`Conjunction [(`Exists
    ([("x337", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x337")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("from", [(`Unknown, (`Variable "x337"));(`Unknown, (`Variable
        "x338"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
    "x338"));(`Unknown, (`Variable "x341"));(`Unknown, (`Variable
    "x339"));]));])));(`Equality ((`Unknown, (`Variable "x339")),
  (`Unknown, (`Variable "a"))));]))));(`Disjunction [(`Exists ([("x336",
  `Unknown);], (`Conjunction [(`Exists ([("x335", `Unknown);],
  (`Conjunction [(`Exists ([("x334", `Unknown);], (`Conjunction [(`Equality
    ((`Unknown, (`Variable "x334")), (`Unknown, (`Variable
      "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x334"));(`Unknown, (`Variable "x335"));]));])));(`Predicate ("abLost",
  [(`Unknown, (`Variable "x335"));(`Unknown, (`Variable "x341"));(`Unknown,
  (`Variable "x336"));]));])));(`Equality ((`Unknown, (`Variable "x336")),
  (`Unknown, (`Variable "a"))));])));(`Exists ([("x333", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x333")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
    "x333"));(`Unknown, (`Variable "x341"));]));])));]);])));(`Forall
    ([("x340", `Unknown);], (`Disjunction [(`Negation (`Disjunction
      [(`Exists ([("x336", `Unknown);], (`Conjunction [(`Exists ([("x335",
      `Unknown);], (`Conjunction [(`Exists ([("x334", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x334")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x334"));(`Unknown, (`Variable "x335"));]));])));(`Predicate
        ("abLost", [(`Unknown, (`Variable "x335"));(`Unknown, (`Variable
          "x340"));(`Unknown, (`Variable "x336"));]));])));(`Equality
        ((`Unknown, (`Variable "x336")), (`Unknown, (`Variable
          "a"))));])));(`Exists ([("x333", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x333")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
          "x333"));(`Unknown, (`Variable "x340"));]));])));]));(`Exists
      ([("x339", `Unknown);], (`Conjunction [(`Exists ([("x338",
      `Unknown);], (`Conjunction [(`Exists ([("x337", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x337")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x337"));(`Unknown, (`Variable "x338"));]));])));(`Predicate
        ("abLost", [(`Unknown, (`Variable "x338"));(`Unknown, (`Variable
          "x340"));(`Unknown, (`Variable "x339"));]));])));(`Equality
        ((`Unknown, (`Variable "x339")), (`Unknown, (`Variable
          "a"))));])));])));]);(`Conjunction [(`Conjunction [(`Forall
    ([("x332", `Unknown);("x329", `Unknown);], (`Disjunction [(`Negation
      (`Conjunction [(`Exists ([("x312", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x312")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x312"));(`Unknown, (`Variable "x329"));]));])));(`Exists
        ([("x331", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
        [(`Unknown, (`Variable "x329"));(`Unknown, (`Variable
          "x332"));(`Unknown, (`Variable "x331"));]));(`Equality
          ((`Unknown, (`Variable "x331")), (`Unknown, (`Variable
            "a"))));])));]));(`Conjunction [(`Exists ([("x312",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x312")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
    (`Variable "x312"));(`Unknown, (`Variable "x329"));]));])));(`Exists
      ([("x330", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x329"));(`Unknown, (`Variable
        "x332"));(`Unknown, (`Variable "x330"));]));(`Equality ((`Unknown,
      (`Variable "x330")), (`Unknown, (`Variable
        "a"))));])));]);])));(`Forall ([("x328", `Unknown);("x325",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x312",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x312")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
  (`Variable "x312"));(`Unknown, (`Variable "x325"));]));])));(`Exists
    ([("x327", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
    [(`Unknown, (`Variable "x325"));(`Unknown, (`Variable
      "x328"));(`Unknown, (`Variable "x327"));]));(`Equality ((`Unknown,
    (`Variable "x327")), (`Unknown, (`Variable
      "a"))));])));]));(`Conjunction [(`Exists ([("x312", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x312")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x312"));(`Unknown, (`Variable "x325"));]));])));(`Exists ([("x326",
  `Unknown);], (`Conjunction [(`Predicate ("abBalance", [(`Unknown,
  (`Variable "x325"));(`Unknown, (`Variable "x328"));(`Unknown, (`Variable
    "x326"));]));(`Equality ((`Unknown, (`Variable "x326")), (`Unknown,
  (`Variable "a"))));])));]);])));]);(`Conjunction [(`Forall ([("x322",
  `Unknown);("x319", `Unknown);], (`Disjunction [(`Negation (`Conjunction
    [(`Exists ([("x312", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x312")), (`Unknown, (`Variable "a_in"))));(`Predicate
      ("to", [(`Unknown, (`Variable "x312"));(`Unknown, (`Variable
        "x319"));]));])));(`Exists ([("x321", `Unknown);], (`Conjunction
      [(`Predicate ("abLost", [(`Unknown, (`Variable "x319"));(`Unknown,
      (`Variable "x322"));(`Unknown, (`Variable "x321"));]));(`Equality
        ((`Unknown, (`Variable "x321")), (`Unknown, (`Variable
          "a"))));])));]));(`Conjunction [(`Exists ([("x312", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x312")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x312"));(`Unknown, (`Variable "x319"));]));])));(`Exists ([("x320",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x319"));(`Unknown, (`Variable "x322"));(`Unknown, (`Variable
    "x320"));]));(`Equality ((`Unknown, (`Variable "x320")), (`Unknown,
  (`Variable "a"))));])));]);])));(`Forall ([("x318", `Unknown);("x315",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x312",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x312")),
  (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
  (`Variable "x312"));(`Unknown, (`Variable "x315"));]));])));(`Exists
    ([("x317", `Unknown);], (`Conjunction [(`Predicate ("abLost",
    [(`Unknown, (`Variable "x315"));(`Unknown, (`Variable
      "x318"));(`Unknown, (`Variable "x317"));]));(`Equality ((`Unknown,
    (`Variable "x317")), (`Unknown, (`Variable
      "a"))));])));]));(`Conjunction [(`Exists ([("x312", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x312")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x312"));(`Unknown, (`Variable "x315"));]));])));(`Exists ([("x316",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x315"));(`Unknown, (`Variable "x318"));(`Unknown, (`Variable
    "x316"));]));(`Equality ((`Unknown, (`Variable "x316")), (`Unknown,
  (`Variable "a"))));])));]);])));]);]);(`Conjunction [(`Forall ([("x311",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x309", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x309")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
    "x309"));(`Unknown, (`Variable "x311"));]));]))));(`Exists ([("x310",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x310")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x310"));(`Unknown, (`Variable
    "x311"));]));])));])));]);(`Conjunction [(`Forall ([("x308",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x306", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x306")), (`Unknown,
  (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
    "x306"));(`Unknown, (`Variable "x308"));]));]))));(`Exists ([("x307",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x307")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x307"));(`Unknown, (`Variable
    "x308"));]));])));])));]);]);(`Conjunction [(`Conjunction
    [(`Conjunction [(`Forall ([("x305", `Unknown);], (`Disjunction
      [(`Negation (`Predicate ("aNullOut", [(`Unknown, (`Variable
        "x305"));])));(`Predicate ("aNullOut", [(`Unknown, (`Variable
        "x305"));]));])));(`Forall ([("x304", `Unknown);], (`Disjunction
      [(`Negation (`Predicate ("aNullOut", [(`Unknown, (`Variable
        "x304"));])));(`Predicate ("aNullOut", [(`Unknown, (`Variable
        "x304"));]));])));]);]);(`Conjunction [(`Forall ([("x303",
  `Unknown);], (`Disjunction [(`Negation (`Exists ([("x301", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x301")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x301"));(`Unknown, (`Variable "x303"));]));]))));(`Exists ([("x300",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x300")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x300"));(`Unknown, (`Variable "x303"));]));])));])));(`Forall
    ([("x302", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x300",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x300")),
    (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x300"));(`Unknown, (`Variable "x302"));]));]))));(`Exists
      ([("x301", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x301")), (`Unknown, (`Variable "a"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x301"));(`Unknown,
        (`Variable "x302"));]));])));])));]);(`Conjunction [(`Conjunction
    [(`Forall ([("x299", `Unknown);("x296", `Unknown);], (`Disjunction
      [(`Negation (`Conjunction [(`Exists ([("x279", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x279")), (`Unknown,
      (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x279"));(`Unknown, (`Variable "x296"));]));])));(`Exists
        ([("x298", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
        [(`Unknown, (`Variable "x296"));(`Unknown, (`Variable
          "x299"));(`Unknown, (`Variable "x298"));]));(`Equality
          ((`Unknown, (`Variable "x298")), (`Unknown, (`Variable
            "a"))));])));]));(`Conjunction [(`Exists ([("x279",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x279")), (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse",
      [(`Unknown, (`Variable "x279"));(`Unknown, (`Variable
        "x296"));]));])));(`Exists ([("x297", `Unknown);], (`Conjunction
        [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x296"));(`Unknown, (`Variable "x299"));(`Unknown, (`Variable
          "x297"));]));(`Equality ((`Unknown, (`Variable "x297")),
        (`Unknown, (`Variable "a"))));])));]);])));(`Forall ([("x295",
    `Unknown);("x292", `Unknown);], (`Disjunction [(`Negation (`Conjunction
      [(`Exists ([("x279", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x279")), (`Unknown, (`Variable
          "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x279"));(`Unknown, (`Variable "x292"));]));])));(`Exists
        ([("x294", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
        [(`Unknown, (`Variable "x292"));(`Unknown, (`Variable
          "x295"));(`Unknown, (`Variable "x294"));]));(`Equality
          ((`Unknown, (`Variable "x294")), (`Unknown, (`Variable
            "a"))));])));]));(`Conjunction [(`Exists ([("x279",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x279")),
    (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x279"));(`Unknown, (`Variable "x292"));]));])));(`Exists
      ([("x293", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x292"));(`Unknown, (`Variable
        "x295"));(`Unknown, (`Variable "x293"));]));(`Equality ((`Unknown,
      (`Variable "x293")), (`Unknown, (`Variable
        "a"))));])));]);])));]);(`Conjunction [(`Forall ([("x289",
  `Unknown);("x286", `Unknown);], (`Disjunction [(`Negation (`Conjunction
    [(`Exists ([("x279", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
    (`Variable "x279")), (`Unknown, (`Variable "a"))));(`Predicate
      ("abAuthPurse", [(`Unknown, (`Variable "x279"));(`Unknown, (`Variable
        "x286"));]));])));(`Exists ([("x288", `Unknown);], (`Conjunction
      [(`Predicate ("abLost", [(`Unknown, (`Variable "x286"));(`Unknown,
      (`Variable "x289"));(`Unknown, (`Variable "x288"));]));(`Equality
        ((`Unknown, (`Variable "x288")), (`Unknown, (`Variable
          "a"))));])));]));(`Conjunction [(`Exists ([("x279", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x279")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x279"));(`Unknown, (`Variable "x286"));]));])));(`Exists ([("x287",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x286"));(`Unknown, (`Variable "x289"));(`Unknown, (`Variable
    "x287"));]));(`Equality ((`Unknown, (`Variable "x287")), (`Unknown,
  (`Variable "a"))));])));]);])));(`Forall ([("x285", `Unknown);("x282",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists ([("x279",
  `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x279")),
  (`Unknown, (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown,
  (`Variable "x279"));(`Unknown, (`Variable "x282"));]));])));(`Exists
    ([("x284", `Unknown);], (`Conjunction [(`Predicate ("abLost",
    [(`Unknown, (`Variable "x282"));(`Unknown, (`Variable
      "x285"));(`Unknown, (`Variable "x284"));]));(`Equality ((`Unknown,
    (`Variable "x284")), (`Unknown, (`Variable
      "a"))));])));]));(`Conjunction [(`Exists ([("x279", `Unknown);],
  (`Conjunction [(`Equality ((`Unknown, (`Variable "x279")), (`Unknown,
  (`Variable "a"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
    "x279"));(`Unknown, (`Variable "x282"));]));])));(`Exists ([("x283",
  `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
    "x282"));(`Unknown, (`Variable "x285"));(`Unknown, (`Variable
    "x283"));]));(`Equality ((`Unknown, (`Variable "x283")), (`Unknown,
  (`Variable "a"))));])));]);])));]);]);]);]);]);]);]);])));])); 
("A241",(`Conjunction [(`Forall ([("s", `Unknown);("s'", `Unknown);("a_in",
`Unknown);("a_out", `Unknown);], (`Disjunction [(`Negation (`Conjunction
  [(`Predicate ("AbWorld", [(`Unknown, (`Variable "s"));]));(`Predicate
    ("AbWorld", [(`Unknown, (`Variable "s'"));]));(`Predicate ("AIN",
  [(`Unknown, (`Variable "a_in"));]));(`Predicate ("AOUT", [(`Unknown,
  (`Variable "a_out"));]));]));(`Disjunction [(`Negation (`Conjunction
  [(`Conjunction [(`Negation (`Exists ([("x278", `Unknown);], (`Conjunction
    [(`Exists ([("x277", `Unknown);], (`Conjunction [(`Exists ([("x276",
    `Unknown);], (`Conjunction [(`Exists ([("x275", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x275")), (`Unknown,
    (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x275"));(`Unknown, (`Variable "x276"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x276"));(`Unknown, (`Variable
        "x278"));(`Unknown, (`Variable "x277"));]));])));(`Equality
      ((`Unknown, (`Variable "x277")), (`Unknown, (`Variable
        "s"))));])));(`Exists ([("x274", `Unknown);], (`Conjunction
      [(`Exists ([("x273", `Unknown);], (`Conjunction [(`Exists ([("x272",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x272")), (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse",
      [(`Unknown, (`Variable "x272"));(`Unknown, (`Variable
        "x273"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
        "x273"));(`Unknown, (`Variable "x278"));(`Unknown, (`Variable
        "x274"));]));])));(`Equality ((`Unknown, (`Variable "x274")),
      (`Unknown, (`Variable "s"))));])));]))));(`Forall ([("c",
  `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Predicate
    ("Coin", [(`Unknown, (`Variable "c"));]));]));(`Forall ([("x268",
  `Unknown);("x269", `Unknown);], (`Disjunction [(`Negation (`Conjunction
    [(`Conjunction [(`Exists ([("x267", `Unknown);], (`Conjunction
      [(`Exists ([("x271", `Unknown);], (`Conjunction [(`Disjunction
        [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x268"));(`Unknown, (`Variable "x267"));(`Unknown, (`Variable
          "x271"));]));(`Predicate ("abLost", [(`Unknown, (`Variable
          "x268"));(`Unknown, (`Variable "x267"));(`Unknown, (`Variable
          "x271"));]));]);(`Equality ((`Unknown, (`Variable "x271")),
      (`Unknown, (`Variable "s"))));])));(`Equality ((`Unknown, (`Variable
        "x267")), (`Unknown, (`Variable "c"))));])));(`Exists ([("x265",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x265")),
    (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x265"));(`Unknown, (`Variable
      "x268"));]));])));]);(`Conjunction [(`Exists ([("x267", `Unknown);],
    (`Conjunction [(`Exists ([("x270", `Unknown);], (`Conjunction
      [(`Disjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
        "x269"));(`Unknown, (`Variable "x267"));(`Unknown, (`Variable
        "x270"));]));(`Predicate ("abLost", [(`Unknown, (`Variable
        "x269"));(`Unknown, (`Variable "x267"));(`Unknown, (`Variable
        "x270"));]));]);(`Equality ((`Unknown, (`Variable "x270")),
      (`Unknown, (`Variable "s"))));])));(`Equality ((`Unknown, (`Variable
      "x267")), (`Unknown, (`Variable "c"))));])));(`Exists ([("x265",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x265")),
    (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x265"));(`Unknown, (`Variable
      "x269"));]));])));]);]));(`Conjunction [(`Equality ((`Unknown,
  (`Variable "x268")), (`Unknown, (`Variable
    "x269"))));]);])));])));]);(`Conjunction [(`Negation (`Exists
    ([("x264", `Unknown);], (`Conjunction [(`Exists ([("x263", `Unknown);],
    (`Conjunction [(`Exists ([("x262", `Unknown);], (`Conjunction [(`Exists
      ([("x261", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x261")), (`Unknown, (`Variable "s'"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x261"));(`Unknown,
        (`Variable "x262"));]));])));(`Predicate ("abBalance", [(`Unknown,
    (`Variable "x262"));(`Unknown, (`Variable "x264"));(`Unknown,
    (`Variable "x263"));]));])));(`Equality ((`Unknown, (`Variable
      "x263")), (`Unknown, (`Variable "s'"))));])));(`Exists ([("x260",
    `Unknown);], (`Conjunction [(`Exists ([("x259", `Unknown);],
    (`Conjunction [(`Exists ([("x258", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x258")), (`Unknown, (`Variable
        "s'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x258"));(`Unknown, (`Variable "x259"));]));])));(`Predicate
      ("abLost", [(`Unknown, (`Variable "x259"));(`Unknown, (`Variable
        "x264"));(`Unknown, (`Variable "x260"));]));])));(`Equality
      ((`Unknown, (`Variable "x260")), (`Unknown, (`Variable
        "s'"))));])));]))));(`Forall ([("c", `Unknown);], (`Disjunction
    [(`Negation (`Conjunction [(`Predicate ("Coin", [(`Unknown, (`Variable
      "c"));]));]));(`Forall ([("x254", `Unknown);("x255", `Unknown);],
    (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
      ([("x253", `Unknown);], (`Conjunction [(`Exists ([("x257",
      `Unknown);], (`Conjunction [(`Disjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x254"));(`Unknown, (`Variable
        "x253"));(`Unknown, (`Variable "x257"));]));(`Predicate ("abLost",
      [(`Unknown, (`Variable "x254"));(`Unknown, (`Variable
        "x253"));(`Unknown, (`Variable "x257"));]));]);(`Equality
        ((`Unknown, (`Variable "x257")), (`Unknown, (`Variable
          "s'"))));])));(`Equality ((`Unknown, (`Variable "x253")),
      (`Unknown, (`Variable "c"))));])));(`Exists ([("x251", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x251")), (`Unknown,
    (`Variable "s'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x251"));(`Unknown, (`Variable "x254"));]));])));]);(`Conjunction
      [(`Exists ([("x253", `Unknown);], (`Conjunction [(`Exists ([("x256",
      `Unknown);], (`Conjunction [(`Disjunction [(`Predicate ("abBalance",
      [(`Unknown, (`Variable "x255"));(`Unknown, (`Variable
        "x253"));(`Unknown, (`Variable "x256"));]));(`Predicate ("abLost",
      [(`Unknown, (`Variable "x255"));(`Unknown, (`Variable
        "x253"));(`Unknown, (`Variable "x256"));]));]);(`Equality
        ((`Unknown, (`Variable "x256")), (`Unknown, (`Variable
          "s'"))));])));(`Equality ((`Unknown, (`Variable "x253")),
      (`Unknown, (`Variable "c"))));])));(`Exists ([("x251", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x251")), (`Unknown,
      (`Variable "s'"))));(`Predicate ("abAuthPurse", [(`Unknown,
      (`Variable "x251"));(`Unknown, (`Variable
        "x255"));]));])));]);]));(`Conjunction [(`Equality ((`Unknown,
    (`Variable "x254")), (`Unknown, (`Variable
      "x255"))));]);])));])));]);(`Conjunction [(`Disjunction
    [(`Conjunction [(`Conjunction [(`Conjunction [(`Conjunction [(`Forall
      ([("x250", `Unknown);], (`Disjunction [(`Negation (`Equality
        ((`Unknown, (`Variable "x250")), (`Unknown, (`Variable
          "a_out")))));(`Predicate ("aNullOut", [(`Unknown, (`Variable
        "x250"));]));])));(`Forall ([("x249", `Unknown);], (`Disjunction
      [(`Negation (`Predicate ("aNullOut", [(`Unknown, (`Variable
        "x249"));])));(`Equality ((`Unknown, (`Variable "x249")),
      (`Unknown, (`Variable "a_out"))));])));]);]);(`Forall ([("x248",
    `Unknown);], (`Disjunction [(`Negation (`Equality ((`Unknown,
    (`Variable "x248")), (`Unknown, (`Variable "a_in")))));(`Predicate
      ("TransferDetails", [(`Unknown, (`Variable
        "x248"));]));])));(`Conjunction [(`Forall ([("x247", `Unknown);],
    (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
      ([("x245", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x245")), (`Unknown, (`Variable "s"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x245"));(`Unknown,
        (`Variable "x247"));]));])));(`Negation (`Exists ([("x244",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x244")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x244"));(`Unknown, (`Variable
      "x247"));]));]))));]);(`Negation (`Exists ([("x243", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x243")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x243"));(`Unknown, (`Variable "x247"));]));]))));]));(`Conjunction
      [(`Conjunction [(`Exists ([("x242", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x242")), (`Unknown, (`Variable
          "s'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x242"));(`Unknown, (`Variable "x247"));]));])));(`Negation
        (`Exists ([("x241", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x241")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x241"));(`Unknown, (`Variable "x247"));]));]))));]);(`Negation
        (`Exists ([("x240", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x240")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x240"));(`Unknown, (`Variable
          "x247"));]));]))));]);])));(`Forall ([("x246", `Unknown);],
    (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
      ([("x242", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x242")), (`Unknown, (`Variable "s'"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x242"));(`Unknown,
        (`Variable "x246"));]));])));(`Negation (`Exists ([("x241",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x241")),
    (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
    (`Variable "x241"));(`Unknown, (`Variable
      "x246"));]));]))));]);(`Negation (`Exists ([("x240", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x240")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x240"));(`Unknown, (`Variable "x246"));]));]))));]));(`Conjunction
      [(`Conjunction [(`Exists ([("x245", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x245")), (`Unknown, (`Variable
          "s"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x245"));(`Unknown, (`Variable "x246"));]));])));(`Negation
        (`Exists ([("x244", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x244")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x244"));(`Unknown, (`Variable "x246"));]));]))));]);(`Negation
        (`Exists ([("x243", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x243")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x243"));(`Unknown, (`Variable
          "x246"));]));]))));]);])));]);(`Conjunction [(`Conjunction
      [(`Forall ([("x239", `Unknown);("x236", `Unknown);], (`Disjunction
        [(`Negation (`Conjunction [(`Conjunction [(`Conjunction [(`Exists
          ([("x219", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x219")), (`Unknown, (`Variable "s"))));(`Predicate
            ("abAuthPurse", [(`Unknown, (`Variable "x219"));(`Unknown,
            (`Variable "x236"));]));])));(`Negation (`Exists ([("x218",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x218")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x218"));(`Unknown, (`Variable
          "x236"));]));]))));]);(`Negation (`Exists ([("x217", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x217")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x217"));(`Unknown, (`Variable
          "x236"));]));]))));]);(`Exists ([("x238", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x236"));(`Unknown, (`Variable "x239"));(`Unknown, (`Variable
          "x238"));]));(`Equality ((`Unknown, (`Variable "x238")),
        (`Unknown, (`Variable "s"))));])));]));(`Conjunction [(`Conjunction
          [(`Conjunction [(`Exists ([("x219", `Unknown);], (`Conjunction
            [(`Equality ((`Unknown, (`Variable "x219")), (`Unknown,
            (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown,
            (`Variable "x219"));(`Unknown, (`Variable
              "x236"));]));])));(`Negation (`Exists ([("x218", `Unknown);],
          (`Conjunction [(`Equality ((`Unknown, (`Variable "x218")),
          (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
          (`Variable "x218"));(`Unknown, (`Variable
            "x236"));]));]))));]);(`Negation (`Exists ([("x217",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x217")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x217"));(`Unknown, (`Variable
            "x236"));]));]))));]);(`Exists ([("x237", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x236"));(`Unknown, (`Variable "x239"));(`Unknown, (`Variable
          "x237"));]));(`Equality ((`Unknown, (`Variable "x237")),
        (`Unknown, (`Variable "s'"))));])));]);])));(`Forall ([("x235",
      `Unknown);("x232", `Unknown);], (`Disjunction [(`Negation
        (`Conjunction [(`Conjunction [(`Conjunction [(`Exists ([("x219",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x219")), (`Unknown, (`Variable "s"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x219"));(`Unknown,
          (`Variable "x232"));]));])));(`Negation (`Exists ([("x218",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x218")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x218"));(`Unknown, (`Variable
          "x232"));]));]))));]);(`Negation (`Exists ([("x217", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x217")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x217"));(`Unknown, (`Variable
          "x232"));]));]))));]);(`Exists ([("x234", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x232"));(`Unknown, (`Variable "x235"));(`Unknown, (`Variable
          "x234"));]));(`Equality ((`Unknown, (`Variable "x234")),
        (`Unknown, (`Variable "s'"))));])));]));(`Conjunction
        [(`Conjunction [(`Conjunction [(`Exists ([("x219", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x219")),
        (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse",
        [(`Unknown, (`Variable "x219"));(`Unknown, (`Variable
          "x232"));]));])));(`Negation (`Exists ([("x218", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x218")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
        (`Variable "x218"));(`Unknown, (`Variable
          "x232"));]));]))));]);(`Negation (`Exists ([("x217", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x217")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x217"));(`Unknown, (`Variable
          "x232"));]));]))));]);(`Exists ([("x233", `Unknown);],
        (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x232"));(`Unknown, (`Variable "x235"));(`Unknown, (`Variable
          "x233"));]));(`Equality ((`Unknown, (`Variable "x233")),
        (`Unknown, (`Variable "s"))));])));]);])));]);(`Conjunction
      [(`Forall ([("x229", `Unknown);("x226", `Unknown);], (`Disjunction
        [(`Negation (`Conjunction [(`Conjunction [(`Conjunction [(`Exists
          ([("x219", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x219")), (`Unknown, (`Variable "s"))));(`Predicate
            ("abAuthPurse", [(`Unknown, (`Variable "x219"));(`Unknown,
            (`Variable "x226"));]));])));(`Negation (`Exists ([("x218",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x218")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x218"));(`Unknown, (`Variable
          "x226"));]));]))));]);(`Negation (`Exists ([("x217", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x217")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x217"));(`Unknown, (`Variable
          "x226"));]));]))));]);(`Exists ([("x228", `Unknown);],
        (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
          "x226"));(`Unknown, (`Variable "x229"));(`Unknown, (`Variable
          "x228"));]));(`Equality ((`Unknown, (`Variable "x228")),
        (`Unknown, (`Variable "s"))));])));]));(`Conjunction [(`Conjunction
          [(`Conjunction [(`Exists ([("x219", `Unknown);], (`Conjunction
            [(`Equality ((`Unknown, (`Variable "x219")), (`Unknown,
            (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown,
            (`Variable "x219"));(`Unknown, (`Variable
              "x226"));]));])));(`Negation (`Exists ([("x218", `Unknown);],
          (`Conjunction [(`Equality ((`Unknown, (`Variable "x218")),
          (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
          (`Variable "x218"));(`Unknown, (`Variable
            "x226"));]));]))));]);(`Negation (`Exists ([("x217",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x217")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x217"));(`Unknown, (`Variable
            "x226"));]));]))));]);(`Exists ([("x227", `Unknown);],
        (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
          "x226"));(`Unknown, (`Variable "x229"));(`Unknown, (`Variable
          "x227"));]));(`Equality ((`Unknown, (`Variable "x227")),
        (`Unknown, (`Variable "s'"))));])));]);])));(`Forall ([("x225",
      `Unknown);("x222", `Unknown);], (`Disjunction [(`Negation
        (`Conjunction [(`Conjunction [(`Conjunction [(`Exists ([("x219",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x219")), (`Unknown, (`Variable "s"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x219"));(`Unknown,
          (`Variable "x222"));]));])));(`Negation (`Exists ([("x218",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x218")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x218"));(`Unknown, (`Variable
          "x222"));]));]))));]);(`Negation (`Exists ([("x217", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x217")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x217"));(`Unknown, (`Variable
          "x222"));]));]))));]);(`Exists ([("x224", `Unknown);],
        (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
          "x222"));(`Unknown, (`Variable "x225"));(`Unknown, (`Variable
          "x224"));]));(`Equality ((`Unknown, (`Variable "x224")),
        (`Unknown, (`Variable "s'"))));])));]));(`Conjunction
        [(`Conjunction [(`Conjunction [(`Exists ([("x219", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x219")),
        (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse",
        [(`Unknown, (`Variable "x219"));(`Unknown, (`Variable
          "x222"));]));])));(`Negation (`Exists ([("x218", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x218")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
        (`Variable "x218"));(`Unknown, (`Variable
          "x222"));]));]))));]);(`Negation (`Exists ([("x217", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x217")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x217"));(`Unknown, (`Variable
          "x222"));]));]))));]);(`Exists ([("x223", `Unknown);],
        (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
          "x222"));(`Unknown, (`Variable "x225"));(`Unknown, (`Variable
          "x223"));]));(`Equality ((`Unknown, (`Variable "x223")),
        (`Unknown, (`Variable "s"))));])));]);])));]);]);]);(`Conjunction
      [(`Forall ([("x216", `Unknown);], (`Disjunction [(`Negation (`Exists
        ([("x214", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
        (`Variable "x214")), (`Unknown, (`Variable "a_in"))));(`Predicate
          ("from", [(`Unknown, (`Variable "x214"));(`Unknown, (`Variable
            "x216"));]));]))));(`Exists ([("x215", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x215")), (`Unknown,
      (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x215"));(`Unknown, (`Variable
        "x216"));]));])));])));]);(`Conjunction [(`Forall ([("x213",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x211", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x211")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x211"));(`Unknown, (`Variable "x213"));]));]))));(`Exists ([("x212",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x212")),
    (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x212"));(`Unknown, (`Variable
      "x213"));]));])));])));]);(`Conjunction [(`Forall ([("x210",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x209", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x209")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
      "x209"));(`Unknown, (`Variable "x210"));]));]))));(`Exists ([("x208",
    `Unknown);], (`Conjunction [(`Exists ([("x207", `Unknown);],
    (`Conjunction [(`Exists ([("x206", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x206")), (`Unknown, (`Variable
        "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x206"));(`Unknown, (`Variable "x207"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x207"));(`Unknown, (`Variable
        "x210"));(`Unknown, (`Variable "x208"));]));])));(`Equality
      ((`Unknown, (`Variable "x208")), (`Unknown, (`Variable
        "s"))));])));])));]);(`Negation (`Exists ([("x205", `Unknown);],
    (`Conjunction [(`Exists ([("x204", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x204")), (`Unknown, (`Variable
        "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x204"));(`Unknown, (`Variable "x205"));]));])));(`Exists
      ([("x203", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x203")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("to", [(`Unknown, (`Variable "x203"));(`Unknown, (`Variable
          "x205"));]));])));]))));(`Conjunction [(`Forall ([("x202",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x200", `Unknown);],
    (`Conjunction [(`Exists ([("x199", `Unknown);], (`Conjunction [(`Exists
      ([("x198", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x198")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("from", [(`Unknown, (`Variable "x198"));(`Unknown, (`Variable
          "x199"));]));])));(`Predicate ("abBalance", [(`Unknown,
    (`Variable "x199"));(`Unknown, (`Variable "x202"));(`Unknown,
    (`Variable "x200"));]));])));(`Equality ((`Unknown, (`Variable
      "x200")), (`Unknown, (`Variable "s'"))));]))));(`Conjunction
      [(`Exists ([("x197", `Unknown);], (`Conjunction [(`Exists ([("x196",
      `Unknown);], (`Conjunction [(`Exists ([("x195", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x195")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x195"));(`Unknown, (`Variable "x196"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x196"));(`Unknown, (`Variable
          "x202"));(`Unknown, (`Variable "x197"));]));])));(`Equality
        ((`Unknown, (`Variable "x197")), (`Unknown, (`Variable
          "s"))));])));(`Negation (`Exists ([("x194", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x194")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
        "x194"));(`Unknown, (`Variable "x202"));]));]))));]);])));(`Forall
      ([("x201", `Unknown);], (`Disjunction [(`Negation (`Conjunction
        [(`Exists ([("x197", `Unknown);], (`Conjunction [(`Exists
          ([("x196", `Unknown);], (`Conjunction [(`Exists ([("x195",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x195")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
          [(`Unknown, (`Variable "x195"));(`Unknown, (`Variable
            "x196"));]));])));(`Predicate ("abBalance", [(`Unknown,
          (`Variable "x196"));(`Unknown, (`Variable "x201"));(`Unknown,
          (`Variable "x197"));]));])));(`Equality ((`Unknown, (`Variable
          "x197")), (`Unknown, (`Variable "s"))));])));(`Negation (`Exists
          ([("x194", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x194")), (`Unknown, (`Variable "a_in"))));(`Predicate
            ("value", [(`Unknown, (`Variable "x194"));(`Unknown, (`Variable
              "x201"));]));]))));]));(`Exists ([("x200", `Unknown);],
      (`Conjunction [(`Exists ([("x199", `Unknown);], (`Conjunction
        [(`Exists ([("x198", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x198")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x198"));(`Unknown, (`Variable "x199"));]));])));(`Predicate
          ("abBalance", [(`Unknown, (`Variable "x199"));(`Unknown,
          (`Variable "x201"));(`Unknown, (`Variable
            "x200"));]));])));(`Equality ((`Unknown, (`Variable "x200")),
      (`Unknown, (`Variable "s'"))));])));])));]);(`Conjunction [(`Forall
      ([("x193", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x191",
      `Unknown);], (`Conjunction [(`Exists ([("x190", `Unknown);],
      (`Conjunction [(`Exists ([("x189", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x189")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x189"));(`Unknown, (`Variable "x190"));]));])));(`Predicate
        ("abLost", [(`Unknown, (`Variable "x190"));(`Unknown, (`Variable
          "x193"));(`Unknown, (`Variable "x191"));]));])));(`Equality
        ((`Unknown, (`Variable "x191")), (`Unknown, (`Variable
          "s'"))));]))));(`Exists ([("x188", `Unknown);], (`Conjunction
        [(`Exists ([("x187", `Unknown);], (`Conjunction [(`Exists
          ([("x186", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x186")), (`Unknown, (`Variable "a_in"))));(`Predicate
            ("from", [(`Unknown, (`Variable "x186"));(`Unknown, (`Variable
              "x187"));]));])));(`Predicate ("abLost", [(`Unknown,
        (`Variable "x187"));(`Unknown, (`Variable "x193"));(`Unknown,
        (`Variable "x188"));]));])));(`Equality ((`Unknown, (`Variable
          "x188")), (`Unknown, (`Variable "s"))));])));])));(`Forall
      ([("x192", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x188",
      `Unknown);], (`Conjunction [(`Exists ([("x187", `Unknown);],
      (`Conjunction [(`Exists ([("x186", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x186")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x186"));(`Unknown, (`Variable "x187"));]));])));(`Predicate
        ("abLost", [(`Unknown, (`Variable "x187"));(`Unknown, (`Variable
          "x192"));(`Unknown, (`Variable "x188"));]));])));(`Equality
        ((`Unknown, (`Variable "x188")), (`Unknown, (`Variable
          "s"))));]))));(`Exists ([("x191", `Unknown);], (`Conjunction
        [(`Exists ([("x190", `Unknown);], (`Conjunction [(`Exists
          ([("x189", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x189")), (`Unknown, (`Variable "a_in"))));(`Predicate
            ("from", [(`Unknown, (`Variable "x189"));(`Unknown, (`Variable
              "x190"));]));])));(`Predicate ("abLost", [(`Unknown,
        (`Variable "x190"));(`Unknown, (`Variable "x192"));(`Unknown,
        (`Variable "x191"));]));])));(`Equality ((`Unknown, (`Variable
          "x191")), (`Unknown, (`Variable
          "s'"))));])));])));]);(`Conjunction [(`Forall ([("x185",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x183", `Unknown);],
    (`Conjunction [(`Exists ([("x182", `Unknown);], (`Conjunction [(`Exists
      ([("x181", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x181")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("to", [(`Unknown, (`Variable "x181"));(`Unknown, (`Variable
          "x182"));]));])));(`Predicate ("abBalance", [(`Unknown,
    (`Variable "x182"));(`Unknown, (`Variable "x185"));(`Unknown,
    (`Variable "x183"));]));])));(`Equality ((`Unknown, (`Variable
      "x183")), (`Unknown, (`Variable "s'"))));]))));(`Disjunction
      [(`Exists ([("x180", `Unknown);], (`Conjunction [(`Exists ([("x179",
      `Unknown);], (`Conjunction [(`Exists ([("x178", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x178")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x178"));(`Unknown, (`Variable "x179"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x179"));(`Unknown, (`Variable
          "x185"));(`Unknown, (`Variable "x180"));]));])));(`Equality
        ((`Unknown, (`Variable "x180")), (`Unknown, (`Variable
          "s"))));])));(`Exists ([("x177", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x177")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
          "x177"));(`Unknown, (`Variable "x185"));]));])));]);])));(`Forall
      ([("x184", `Unknown);], (`Disjunction [(`Negation (`Disjunction
        [(`Exists ([("x180", `Unknown);], (`Conjunction [(`Exists
          ([("x179", `Unknown);], (`Conjunction [(`Exists ([("x178",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x178")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x178"));(`Unknown, (`Variable
            "x179"));]));])));(`Predicate ("abBalance", [(`Unknown,
          (`Variable "x179"));(`Unknown, (`Variable "x184"));(`Unknown,
          (`Variable "x180"));]));])));(`Equality ((`Unknown, (`Variable
          "x180")), (`Unknown, (`Variable "s"))));])));(`Exists ([("x177",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x177")), (`Unknown, (`Variable "a_in"))));(`Predicate ("value",
        [(`Unknown, (`Variable "x177"));(`Unknown, (`Variable
          "x184"));]));])));]));(`Exists ([("x183", `Unknown);],
      (`Conjunction [(`Exists ([("x182", `Unknown);], (`Conjunction
        [(`Exists ([("x181", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x181")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x181"));(`Unknown, (`Variable "x182"));]));])));(`Predicate
          ("abBalance", [(`Unknown, (`Variable "x182"));(`Unknown,
          (`Variable "x184"));(`Unknown, (`Variable
            "x183"));]));])));(`Equality ((`Unknown, (`Variable "x183")),
      (`Unknown, (`Variable "s'"))));])));])));]);(`Conjunction [(`Forall
      ([("x176", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x174",
      `Unknown);], (`Conjunction [(`Exists ([("x173", `Unknown);],
      (`Conjunction [(`Exists ([("x172", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x172")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x172"));(`Unknown, (`Variable "x173"));]));])));(`Predicate
        ("abLost", [(`Unknown, (`Variable "x173"));(`Unknown, (`Variable
          "x176"));(`Unknown, (`Variable "x174"));]));])));(`Equality
        ((`Unknown, (`Variable "x174")), (`Unknown, (`Variable
          "s'"))));]))));(`Exists ([("x171", `Unknown);], (`Conjunction
        [(`Exists ([("x170", `Unknown);], (`Conjunction [(`Exists
          ([("x169", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x169")), (`Unknown, (`Variable "a_in"))));(`Predicate
            ("to", [(`Unknown, (`Variable "x169"));(`Unknown, (`Variable
              "x170"));]));])));(`Predicate ("abLost", [(`Unknown,
        (`Variable "x170"));(`Unknown, (`Variable "x176"));(`Unknown,
        (`Variable "x171"));]));])));(`Equality ((`Unknown, (`Variable
          "x171")), (`Unknown, (`Variable "s"))));])));])));(`Forall
      ([("x175", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x171",
      `Unknown);], (`Conjunction [(`Exists ([("x170", `Unknown);],
      (`Conjunction [(`Exists ([("x169", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x169")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
          "x169"));(`Unknown, (`Variable "x170"));]));])));(`Predicate
        ("abLost", [(`Unknown, (`Variable "x170"));(`Unknown, (`Variable
          "x175"));(`Unknown, (`Variable "x171"));]));])));(`Equality
        ((`Unknown, (`Variable "x171")), (`Unknown, (`Variable
          "s"))));]))));(`Exists ([("x174", `Unknown);], (`Conjunction
        [(`Exists ([("x173", `Unknown);], (`Conjunction [(`Exists
          ([("x172", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x172")), (`Unknown, (`Variable "a_in"))));(`Predicate
            ("to", [(`Unknown, (`Variable "x172"));(`Unknown, (`Variable
              "x173"));]));])));(`Predicate ("abLost", [(`Unknown,
        (`Variable "x173"));(`Unknown, (`Variable "x175"));(`Unknown,
        (`Variable "x174"));]));])));(`Equality ((`Unknown, (`Variable
          "x174")), (`Unknown, (`Variable
          "s'"))));])));])));]);(`Conjunction [(`Forall ([("x168",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x166", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x166")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
      "x166"));(`Unknown, (`Variable "x168"));]));]))));(`Exists ([("x167",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x167")),
    (`Unknown, (`Variable "s'"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x167"));(`Unknown, (`Variable
      "x168"));]));])));])));]);(`Conjunction [(`Forall ([("x165",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x163", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x163")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x163"));(`Unknown, (`Variable "x165"));]));]))));(`Exists ([("x164",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x164")),
    (`Unknown, (`Variable "s'"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x164"));(`Unknown, (`Variable
      "x165"));]));])));])));]);]);(`Conjunction [(`Conjunction
      [(`Conjunction [(`Conjunction [(`Forall ([("x162", `Unknown);],
      (`Disjunction [(`Negation (`Equality ((`Unknown, (`Variable "x162")),
      (`Unknown, (`Variable "a_out")))));(`Predicate ("aNullOut",
      [(`Unknown, (`Variable "x162"));]));])));(`Forall ([("x161",
      `Unknown);], (`Disjunction [(`Negation (`Predicate ("aNullOut",
      [(`Unknown, (`Variable "x161"));])));(`Equality ((`Unknown,
      (`Variable "x161")), (`Unknown, (`Variable
        "a_out"))));])));]);]);(`Forall ([("x160", `Unknown);],
      (`Disjunction [(`Negation (`Equality ((`Unknown, (`Variable "x160")),
      (`Unknown, (`Variable "a_in")))));(`Predicate ("TransferDetails",
      [(`Unknown, (`Variable "x160"));]));])));(`Conjunction [(`Forall
        ([("x159", `Unknown);], (`Disjunction [(`Negation (`Conjunction
          [(`Conjunction [(`Exists ([("x157", `Unknown);], (`Conjunction
            [(`Equality ((`Unknown, (`Variable "x157")), (`Unknown,
            (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown,
            (`Variable "x157"));(`Unknown, (`Variable
              "x159"));]));])));(`Negation (`Exists ([("x156", `Unknown);],
          (`Conjunction [(`Equality ((`Unknown, (`Variable "x156")),
          (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
          (`Variable "x156"));(`Unknown, (`Variable
            "x159"));]));]))));]);(`Negation (`Exists ([("x155",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x155")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x155"));(`Unknown, (`Variable
            "x159"));]));]))));]));(`Conjunction [(`Conjunction [(`Exists
          ([("x154", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x154")), (`Unknown, (`Variable "s'"))));(`Predicate
            ("abAuthPurse", [(`Unknown, (`Variable "x154"));(`Unknown,
            (`Variable "x159"));]));])));(`Negation (`Exists ([("x153",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x153")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
        [(`Unknown, (`Variable "x153"));(`Unknown, (`Variable
          "x159"));]));]))));]);(`Negation (`Exists ([("x152", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x152")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x152"));(`Unknown, (`Variable
          "x159"));]));]))));]);])));(`Forall ([("x158", `Unknown);],
      (`Disjunction [(`Negation (`Conjunction [(`Conjunction [(`Exists
        ([("x154", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
        (`Variable "x154")), (`Unknown, (`Variable "s'"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x154"));(`Unknown,
          (`Variable "x158"));]));])));(`Negation (`Exists ([("x153",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x153")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
      [(`Unknown, (`Variable "x153"));(`Unknown, (`Variable
        "x158"));]));]))));]);(`Negation (`Exists ([("x152", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x152")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x152"));(`Unknown, (`Variable "x158"));]));]))));]));(`Conjunction
        [(`Conjunction [(`Exists ([("x157", `Unknown);], (`Conjunction
          [(`Equality ((`Unknown, (`Variable "x157")), (`Unknown,
          (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown,
          (`Variable "x157"));(`Unknown, (`Variable
            "x158"));]));])));(`Negation (`Exists ([("x156", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x156")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
        (`Variable "x156"));(`Unknown, (`Variable
          "x158"));]));]))));]);(`Negation (`Exists ([("x155", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x155")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("to", [(`Unknown,
        (`Variable "x155"));(`Unknown, (`Variable
          "x158"));]));]))));]);])));]);(`Conjunction [(`Conjunction
        [(`Forall ([("x151", `Unknown);("x148", `Unknown);], (`Disjunction
          [(`Negation (`Conjunction [(`Conjunction [(`Conjunction [(`Exists
            ([("x131", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
            (`Variable "x131")), (`Unknown, (`Variable "s"))));(`Predicate
              ("abAuthPurse", [(`Unknown, (`Variable "x131"));(`Unknown,
              (`Variable "x148"));]));])));(`Negation (`Exists ([("x130",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x130")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
          [(`Unknown, (`Variable "x130"));(`Unknown, (`Variable
            "x148"));]));]))));]);(`Negation (`Exists ([("x129",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x129")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x129"));(`Unknown, (`Variable
            "x148"));]));]))));]);(`Exists ([("x150", `Unknown);],
          (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
            "x148"));(`Unknown, (`Variable "x151"));(`Unknown, (`Variable
            "x150"));]));(`Equality ((`Unknown, (`Variable "x150")),
          (`Unknown, (`Variable "s"))));])));]));(`Conjunction
            [(`Conjunction [(`Conjunction [(`Exists ([("x131", `Unknown);],
            (`Conjunction [(`Equality ((`Unknown, (`Variable "x131")),
            (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse",
            [(`Unknown, (`Variable "x131"));(`Unknown, (`Variable
              "x148"));]));])));(`Negation (`Exists ([("x130", `Unknown);],
            (`Conjunction [(`Equality ((`Unknown, (`Variable "x130")),
            (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
            [(`Unknown, (`Variable "x130"));(`Unknown, (`Variable
              "x148"));]));]))));]);(`Negation (`Exists ([("x129",
            `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
              "x129")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
            [(`Unknown, (`Variable "x129"));(`Unknown, (`Variable
              "x148"));]));]))));]);(`Exists ([("x149", `Unknown);],
            (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
              "x148"));(`Unknown, (`Variable "x151"));(`Unknown, (`Variable
              "x149"));]));(`Equality ((`Unknown, (`Variable "x149")),
            (`Unknown, (`Variable "s'"))));])));]);])));(`Forall ([("x147",
        `Unknown);("x144", `Unknown);], (`Disjunction [(`Negation
          (`Conjunction [(`Conjunction [(`Conjunction [(`Exists ([("x131",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x131")), (`Unknown, (`Variable "s"))));(`Predicate
            ("abAuthPurse", [(`Unknown, (`Variable "x131"));(`Unknown,
            (`Variable "x144"));]));])));(`Negation (`Exists ([("x130",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x130")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
          [(`Unknown, (`Variable "x130"));(`Unknown, (`Variable
            "x144"));]));]))));]);(`Negation (`Exists ([("x129",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x129")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x129"));(`Unknown, (`Variable
            "x144"));]));]))));]);(`Exists ([("x146", `Unknown);],
          (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
            "x144"));(`Unknown, (`Variable "x147"));(`Unknown, (`Variable
            "x146"));]));(`Equality ((`Unknown, (`Variable "x146")),
          (`Unknown, (`Variable "s'"))));])));]));(`Conjunction
          [(`Conjunction [(`Conjunction [(`Exists ([("x131", `Unknown);],
          (`Conjunction [(`Equality ((`Unknown, (`Variable "x131")),
          (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse",
          [(`Unknown, (`Variable "x131"));(`Unknown, (`Variable
            "x144"));]));])));(`Negation (`Exists ([("x130", `Unknown);],
          (`Conjunction [(`Equality ((`Unknown, (`Variable "x130")),
          (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
          (`Variable "x130"));(`Unknown, (`Variable
            "x144"));]));]))));]);(`Negation (`Exists ([("x129",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x129")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x129"));(`Unknown, (`Variable
            "x144"));]));]))));]);(`Exists ([("x145", `Unknown);],
          (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
            "x144"));(`Unknown, (`Variable "x147"));(`Unknown, (`Variable
            "x145"));]));(`Equality ((`Unknown, (`Variable "x145")),
          (`Unknown, (`Variable "s"))));])));]);])));]);(`Conjunction
        [(`Forall ([("x141", `Unknown);("x138", `Unknown);], (`Disjunction
          [(`Negation (`Conjunction [(`Conjunction [(`Conjunction [(`Exists
            ([("x131", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
            (`Variable "x131")), (`Unknown, (`Variable "s"))));(`Predicate
              ("abAuthPurse", [(`Unknown, (`Variable "x131"));(`Unknown,
              (`Variable "x138"));]));])));(`Negation (`Exists ([("x130",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x130")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
          [(`Unknown, (`Variable "x130"));(`Unknown, (`Variable
            "x138"));]));]))));]);(`Negation (`Exists ([("x129",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x129")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x129"));(`Unknown, (`Variable
            "x138"));]));]))));]);(`Exists ([("x140", `Unknown);],
          (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
            "x138"));(`Unknown, (`Variable "x141"));(`Unknown, (`Variable
            "x140"));]));(`Equality ((`Unknown, (`Variable "x140")),
          (`Unknown, (`Variable "s"))));])));]));(`Conjunction
            [(`Conjunction [(`Conjunction [(`Exists ([("x131", `Unknown);],
            (`Conjunction [(`Equality ((`Unknown, (`Variable "x131")),
            (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse",
            [(`Unknown, (`Variable "x131"));(`Unknown, (`Variable
              "x138"));]));])));(`Negation (`Exists ([("x130", `Unknown);],
            (`Conjunction [(`Equality ((`Unknown, (`Variable "x130")),
            (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
            [(`Unknown, (`Variable "x130"));(`Unknown, (`Variable
              "x138"));]));]))));]);(`Negation (`Exists ([("x129",
            `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
              "x129")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
            [(`Unknown, (`Variable "x129"));(`Unknown, (`Variable
              "x138"));]));]))));]);(`Exists ([("x139", `Unknown);],
            (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
              "x138"));(`Unknown, (`Variable "x141"));(`Unknown, (`Variable
              "x139"));]));(`Equality ((`Unknown, (`Variable "x139")),
            (`Unknown, (`Variable "s'"))));])));]);])));(`Forall ([("x137",
        `Unknown);("x134", `Unknown);], (`Disjunction [(`Negation
          (`Conjunction [(`Conjunction [(`Conjunction [(`Exists ([("x131",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x131")), (`Unknown, (`Variable "s"))));(`Predicate
            ("abAuthPurse", [(`Unknown, (`Variable "x131"));(`Unknown,
            (`Variable "x134"));]));])));(`Negation (`Exists ([("x130",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x130")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
          [(`Unknown, (`Variable "x130"));(`Unknown, (`Variable
            "x134"));]));]))));]);(`Negation (`Exists ([("x129",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x129")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x129"));(`Unknown, (`Variable
            "x134"));]));]))));]);(`Exists ([("x136", `Unknown);],
          (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
            "x134"));(`Unknown, (`Variable "x137"));(`Unknown, (`Variable
            "x136"));]));(`Equality ((`Unknown, (`Variable "x136")),
          (`Unknown, (`Variable "s'"))));])));]));(`Conjunction
          [(`Conjunction [(`Conjunction [(`Exists ([("x131", `Unknown);],
          (`Conjunction [(`Equality ((`Unknown, (`Variable "x131")),
          (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse",
          [(`Unknown, (`Variable "x131"));(`Unknown, (`Variable
            "x134"));]));])));(`Negation (`Exists ([("x130", `Unknown);],
          (`Conjunction [(`Equality ((`Unknown, (`Variable "x130")),
          (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
          (`Variable "x130"));(`Unknown, (`Variable
            "x134"));]));]))));]);(`Negation (`Exists ([("x129",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x129")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
          [(`Unknown, (`Variable "x129"));(`Unknown, (`Variable
            "x134"));]));]))));]);(`Exists ([("x135", `Unknown);],
          (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
            "x134"));(`Unknown, (`Variable "x137"));(`Unknown, (`Variable
            "x135"));]));(`Equality ((`Unknown, (`Variable "x135")),
          (`Unknown, (`Variable "s"))));])));]);])));]);]);]);(`Conjunction
      [(`Forall ([("x128", `Unknown);], (`Disjunction [(`Negation (`Exists
        ([("x126", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
        (`Variable "x126")), (`Unknown, (`Variable "a_in"))));(`Predicate
          ("from", [(`Unknown, (`Variable "x126"));(`Unknown, (`Variable
            "x128"));]));]))));(`Exists ([("x127", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x127")), (`Unknown,
      (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x127"));(`Unknown, (`Variable
        "x128"));]));])));])));]);(`Conjunction [(`Forall ([("x125",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x123", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x123")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x123"));(`Unknown, (`Variable "x125"));]));]))));(`Exists ([("x124",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x124")),
    (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x124"));(`Unknown, (`Variable
      "x125"));]));])));])));]);(`Conjunction [(`Forall ([("x122",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x121", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x121")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
      "x121"));(`Unknown, (`Variable "x122"));]));]))));(`Exists ([("x120",
    `Unknown);], (`Conjunction [(`Exists ([("x119", `Unknown);],
    (`Conjunction [(`Exists ([("x118", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x118")), (`Unknown, (`Variable
        "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x118"));(`Unknown, (`Variable "x119"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x119"));(`Unknown, (`Variable
        "x122"));(`Unknown, (`Variable "x120"));]));])));(`Equality
      ((`Unknown, (`Variable "x120")), (`Unknown, (`Variable
        "s"))));])));])));]);(`Negation (`Exists ([("x117", `Unknown);],
    (`Conjunction [(`Exists ([("x116", `Unknown);], (`Conjunction
      [(`Equality ((`Unknown, (`Variable "x116")), (`Unknown, (`Variable
        "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x116"));(`Unknown, (`Variable "x117"));]));])));(`Exists
      ([("x115", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x115")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("to", [(`Unknown, (`Variable "x115"));(`Unknown, (`Variable
          "x117"));]));])));]))));(`Conjunction [(`Forall ([("x114",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x112", `Unknown);],
    (`Conjunction [(`Exists ([("x111", `Unknown);], (`Conjunction [(`Exists
      ([("x110", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x110")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("from", [(`Unknown, (`Variable "x110"));(`Unknown, (`Variable
          "x111"));]));])));(`Predicate ("abBalance", [(`Unknown,
    (`Variable "x111"));(`Unknown, (`Variable "x114"));(`Unknown,
    (`Variable "x112"));]));])));(`Equality ((`Unknown, (`Variable
      "x112")), (`Unknown, (`Variable "s'"))));]))));(`Conjunction
      [(`Exists ([("x109", `Unknown);], (`Conjunction [(`Exists ([("x108",
      `Unknown);], (`Conjunction [(`Exists ([("x107", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x107")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
        "x107"));(`Unknown, (`Variable "x108"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x108"));(`Unknown, (`Variable
          "x114"));(`Unknown, (`Variable "x109"));]));])));(`Equality
        ((`Unknown, (`Variable "x109")), (`Unknown, (`Variable
          "s"))));])));(`Negation (`Exists ([("x106", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x106")), (`Unknown,
      (`Variable "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
        "x106"));(`Unknown, (`Variable "x114"));]));]))));]);])));(`Forall
      ([("x113", `Unknown);], (`Disjunction [(`Negation (`Conjunction
        [(`Exists ([("x109", `Unknown);], (`Conjunction [(`Exists
          ([("x108", `Unknown);], (`Conjunction [(`Exists ([("x107",
          `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
            "x107")), (`Unknown, (`Variable "a_in"))));(`Predicate ("from",
          [(`Unknown, (`Variable "x107"));(`Unknown, (`Variable
            "x108"));]));])));(`Predicate ("abBalance", [(`Unknown,
          (`Variable "x108"));(`Unknown, (`Variable "x113"));(`Unknown,
          (`Variable "x109"));]));])));(`Equality ((`Unknown, (`Variable
          "x109")), (`Unknown, (`Variable "s"))));])));(`Negation (`Exists
          ([("x106", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
          (`Variable "x106")), (`Unknown, (`Variable "a_in"))));(`Predicate
            ("value", [(`Unknown, (`Variable "x106"));(`Unknown, (`Variable
              "x113"));]));]))));]));(`Exists ([("x112", `Unknown);],
      (`Conjunction [(`Exists ([("x111", `Unknown);], (`Conjunction
        [(`Exists ([("x110", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x110")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x110"));(`Unknown, (`Variable "x111"));]));])));(`Predicate
          ("abBalance", [(`Unknown, (`Variable "x111"));(`Unknown,
          (`Variable "x113"));(`Unknown, (`Variable
            "x112"));]));])));(`Equality ((`Unknown, (`Variable "x112")),
      (`Unknown, (`Variable "s'"))));])));])));]);(`Conjunction [(`Forall
      ([("x105", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x103",
      `Unknown);], (`Conjunction [(`Exists ([("x102", `Unknown);],
      (`Conjunction [(`Exists ([("x101", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x101")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x101"));(`Unknown, (`Variable "x102"));]));])));(`Predicate
        ("abLost", [(`Unknown, (`Variable "x102"));(`Unknown, (`Variable
          "x105"));(`Unknown, (`Variable "x103"));]));])));(`Equality
        ((`Unknown, (`Variable "x103")), (`Unknown, (`Variable
          "s'"))));]))));(`Disjunction [(`Exists ([("x100", `Unknown);],
      (`Conjunction [(`Exists ([("x99", `Unknown);], (`Conjunction
        [(`Exists ([("x98", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x98")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x98"));(`Unknown, (`Variable "x99"));]));])));(`Predicate
          ("abLost", [(`Unknown, (`Variable "x99"));(`Unknown, (`Variable
            "x105"));(`Unknown, (`Variable "x100"));]));])));(`Equality
        ((`Unknown, (`Variable "x100")), (`Unknown, (`Variable
          "s"))));])));(`Exists ([("x97", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x97")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("value", [(`Unknown, (`Variable
          "x97"));(`Unknown, (`Variable "x105"));]));])));]);])));(`Forall
      ([("x104", `Unknown);], (`Disjunction [(`Negation (`Disjunction
        [(`Exists ([("x100", `Unknown);], (`Conjunction [(`Exists ([("x99",
        `Unknown);], (`Conjunction [(`Exists ([("x98", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x98")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("from", [(`Unknown,
        (`Variable "x98"));(`Unknown, (`Variable
          "x99"));]));])));(`Predicate ("abLost", [(`Unknown, (`Variable
          "x99"));(`Unknown, (`Variable "x104"));(`Unknown, (`Variable
          "x100"));]));])));(`Equality ((`Unknown, (`Variable "x100")),
        (`Unknown, (`Variable "s"))));])));(`Exists ([("x97", `Unknown);],
        (`Conjunction [(`Equality ((`Unknown, (`Variable "x97")),
        (`Unknown, (`Variable "a_in"))));(`Predicate ("value", [(`Unknown,
        (`Variable "x97"));(`Unknown, (`Variable
          "x104"));]));])));]));(`Exists ([("x103", `Unknown);],
      (`Conjunction [(`Exists ([("x102", `Unknown);], (`Conjunction
        [(`Exists ([("x101", `Unknown);], (`Conjunction [(`Equality
          ((`Unknown, (`Variable "x101")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
          "x101"));(`Unknown, (`Variable "x102"));]));])));(`Predicate
          ("abLost", [(`Unknown, (`Variable "x102"));(`Unknown, (`Variable
            "x104"));(`Unknown, (`Variable "x103"));]));])));(`Equality
        ((`Unknown, (`Variable "x103")), (`Unknown, (`Variable
          "s'"))));])));])));]);(`Conjunction [(`Conjunction [(`Forall
      ([("x96", `Unknown);("x93", `Unknown);], (`Disjunction [(`Negation
        (`Conjunction [(`Exists ([("x76", `Unknown);], (`Conjunction
          [(`Equality ((`Unknown, (`Variable "x76")), (`Unknown, (`Variable
            "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
            "x76"));(`Unknown, (`Variable "x93"));]));])));(`Exists
          ([("x95", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
          [(`Unknown, (`Variable "x93"));(`Unknown, (`Variable
            "x96"));(`Unknown, (`Variable "x95"));]));(`Equality
            ((`Unknown, (`Variable "x95")), (`Unknown, (`Variable
              "s"))));])));]));(`Conjunction [(`Exists ([("x76",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x76")), (`Unknown, (`Variable "a_in"))));(`Predicate ("to",
      [(`Unknown, (`Variable "x76"));(`Unknown, (`Variable
        "x93"));]));])));(`Exists ([("x94", `Unknown);], (`Conjunction
        [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x93"));(`Unknown, (`Variable "x96"));(`Unknown, (`Variable
          "x94"));]));(`Equality ((`Unknown, (`Variable "x94")), (`Unknown,
        (`Variable "s'"))));])));]);])));(`Forall ([("x92",
    `Unknown);("x89", `Unknown);], (`Disjunction [(`Negation (`Conjunction
      [(`Exists ([("x76", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x76")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x76"));(`Unknown, (`Variable "x89"));]));])));(`Exists ([("x91",
      `Unknown);], (`Conjunction [(`Predicate ("abBalance", [(`Unknown,
      (`Variable "x89"));(`Unknown, (`Variable "x92"));(`Unknown,
      (`Variable "x91"));]));(`Equality ((`Unknown, (`Variable "x91")),
      (`Unknown, (`Variable "s'"))));])));]));(`Conjunction [(`Exists
      ([("x76", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x76")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("to", [(`Unknown, (`Variable "x76"));(`Unknown, (`Variable
          "x89"));]));])));(`Exists ([("x90", `Unknown);], (`Conjunction
      [(`Predicate ("abBalance", [(`Unknown, (`Variable "x89"));(`Unknown,
      (`Variable "x92"));(`Unknown, (`Variable "x90"));]));(`Equality
        ((`Unknown, (`Variable "x90")), (`Unknown, (`Variable
          "s"))));])));]);])));]);(`Conjunction [(`Forall ([("x86",
    `Unknown);("x83", `Unknown);], (`Disjunction [(`Negation (`Conjunction
      [(`Exists ([("x76", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x76")), (`Unknown, (`Variable
          "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
        "x76"));(`Unknown, (`Variable "x83"));]));])));(`Exists ([("x85",
      `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown,
      (`Variable "x83"));(`Unknown, (`Variable "x86"));(`Unknown,
      (`Variable "x85"));]));(`Equality ((`Unknown, (`Variable "x85")),
      (`Unknown, (`Variable "s"))));])));]));(`Conjunction [(`Exists
      ([("x76", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x76")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("to", [(`Unknown, (`Variable "x76"));(`Unknown, (`Variable
          "x83"));]));])));(`Exists ([("x84", `Unknown);], (`Conjunction
      [(`Predicate ("abLost", [(`Unknown, (`Variable "x83"));(`Unknown,
      (`Variable "x86"));(`Unknown, (`Variable "x84"));]));(`Equality
        ((`Unknown, (`Variable "x84")), (`Unknown, (`Variable
          "s'"))));])));]);])));(`Forall ([("x82", `Unknown);("x79",
    `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists
      ([("x76", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x76")), (`Unknown, (`Variable "a_in"))));(`Predicate
        ("to", [(`Unknown, (`Variable "x76"));(`Unknown, (`Variable
          "x79"));]));])));(`Exists ([("x81", `Unknown);], (`Conjunction
      [(`Predicate ("abLost", [(`Unknown, (`Variable "x79"));(`Unknown,
      (`Variable "x82"));(`Unknown, (`Variable "x81"));]));(`Equality
        ((`Unknown, (`Variable "x81")), (`Unknown, (`Variable
          "s'"))));])));]));(`Conjunction [(`Exists ([("x76", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x76")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x76"));(`Unknown, (`Variable "x79"));]));])));(`Exists ([("x80",
    `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown,
    (`Variable "x79"));(`Unknown, (`Variable "x82"));(`Unknown, (`Variable
      "x80"));]));(`Equality ((`Unknown, (`Variable "x80")), (`Unknown,
    (`Variable "s"))));])));]);])));]);]);(`Conjunction [(`Forall ([("x75",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x73", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x73")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("from", [(`Unknown, (`Variable
      "x73"));(`Unknown, (`Variable "x75"));]));]))));(`Exists ([("x74",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x74")),
    (`Unknown, (`Variable "s'"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x74"));(`Unknown, (`Variable
      "x75"));]));])));])));]);(`Conjunction [(`Forall ([("x72",
    `Unknown);], (`Disjunction [(`Negation (`Exists ([("x70", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x70")), (`Unknown,
    (`Variable "a_in"))));(`Predicate ("to", [(`Unknown, (`Variable
      "x70"));(`Unknown, (`Variable "x72"));]));]))));(`Exists ([("x71",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x71")),
    (`Unknown, (`Variable "s'"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x71"));(`Unknown, (`Variable
      "x72"));]));])));])));]);]);(`Conjunction [(`Conjunction
      [(`Conjunction [(`Forall ([("x69", `Unknown);], (`Disjunction
        [(`Negation (`Equality ((`Unknown, (`Variable "x69")), (`Unknown,
        (`Variable "a_out")))));(`Predicate ("aNullOut", [(`Unknown,
        (`Variable "x69"));]));])));(`Forall ([("x68", `Unknown);],
      (`Disjunction [(`Negation (`Predicate ("aNullOut", [(`Unknown,
      (`Variable "x68"));])));(`Equality ((`Unknown, (`Variable "x68")),
      (`Unknown, (`Variable "a_out"))));])));]);]);(`Conjunction [(`Forall
      ([("x67", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x65",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x65")), (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse",
      [(`Unknown, (`Variable "x65"));(`Unknown, (`Variable
        "x67"));]));]))));(`Exists ([("x64", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x64")), (`Unknown, (`Variable
          "s'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x64"));(`Unknown, (`Variable "x67"));]));])));])));(`Forall
      ([("x66", `Unknown);], (`Disjunction [(`Negation (`Exists ([("x64",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x64")), (`Unknown, (`Variable "s'"))));(`Predicate ("abAuthPurse",
      [(`Unknown, (`Variable "x64"));(`Unknown, (`Variable
        "x66"));]));]))));(`Exists ([("x65", `Unknown);], (`Conjunction
        [(`Equality ((`Unknown, (`Variable "x65")), (`Unknown, (`Variable
          "s"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
          "x65"));(`Unknown, (`Variable
          "x66"));]));])));])));]);(`Conjunction [(`Conjunction [(`Forall
      ([("x63", `Unknown);("x60", `Unknown);], (`Disjunction [(`Negation
        (`Conjunction [(`Exists ([("x43", `Unknown);], (`Conjunction
          [(`Equality ((`Unknown, (`Variable "x43")), (`Unknown, (`Variable
            "s"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
            "x43"));(`Unknown, (`Variable "x60"));]));])));(`Exists
          ([("x62", `Unknown);], (`Conjunction [(`Predicate ("abBalance",
          [(`Unknown, (`Variable "x60"));(`Unknown, (`Variable
            "x63"));(`Unknown, (`Variable "x62"));]));(`Equality
            ((`Unknown, (`Variable "x62")), (`Unknown, (`Variable
              "s"))));])));]));(`Conjunction [(`Exists ([("x43",
      `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
        "x43")), (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse",
      [(`Unknown, (`Variable "x43"));(`Unknown, (`Variable
        "x60"));]));])));(`Exists ([("x61", `Unknown);], (`Conjunction
        [(`Predicate ("abBalance", [(`Unknown, (`Variable
          "x60"));(`Unknown, (`Variable "x63"));(`Unknown, (`Variable
          "x61"));]));(`Equality ((`Unknown, (`Variable "x61")), (`Unknown,
        (`Variable "s'"))));])));]);])));(`Forall ([("x59",
    `Unknown);("x56", `Unknown);], (`Disjunction [(`Negation (`Conjunction
      [(`Exists ([("x43", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x43")), (`Unknown, (`Variable
          "s"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x43"));(`Unknown, (`Variable "x56"));]));])));(`Exists ([("x58",
      `Unknown);], (`Conjunction [(`Predicate ("abBalance", [(`Unknown,
      (`Variable "x56"));(`Unknown, (`Variable "x59"));(`Unknown,
      (`Variable "x58"));]));(`Equality ((`Unknown, (`Variable "x58")),
      (`Unknown, (`Variable "s'"))));])));]));(`Conjunction [(`Exists
      ([("x43", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x43")), (`Unknown, (`Variable "s"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x43"));(`Unknown,
        (`Variable "x56"));]));])));(`Exists ([("x57", `Unknown);],
    (`Conjunction [(`Predicate ("abBalance", [(`Unknown, (`Variable
      "x56"));(`Unknown, (`Variable "x59"));(`Unknown, (`Variable
      "x57"));]));(`Equality ((`Unknown, (`Variable "x57")), (`Unknown,
    (`Variable "s"))));])));]);])));]);(`Conjunction [(`Forall ([("x53",
    `Unknown);("x50", `Unknown);], (`Disjunction [(`Negation (`Conjunction
      [(`Exists ([("x43", `Unknown);], (`Conjunction [(`Equality
        ((`Unknown, (`Variable "x43")), (`Unknown, (`Variable
          "s"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x43"));(`Unknown, (`Variable "x50"));]));])));(`Exists ([("x52",
      `Unknown);], (`Conjunction [(`Predicate ("abLost", [(`Unknown,
      (`Variable "x50"));(`Unknown, (`Variable "x53"));(`Unknown,
      (`Variable "x52"));]));(`Equality ((`Unknown, (`Variable "x52")),
      (`Unknown, (`Variable "s"))));])));]));(`Conjunction [(`Exists
      ([("x43", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x43")), (`Unknown, (`Variable "s"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x43"));(`Unknown,
        (`Variable "x50"));]));])));(`Exists ([("x51", `Unknown);],
    (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
      "x50"));(`Unknown, (`Variable "x53"));(`Unknown, (`Variable
      "x51"));]));(`Equality ((`Unknown, (`Variable "x51")), (`Unknown,
    (`Variable "s'"))));])));]);])));(`Forall ([("x49", `Unknown);("x46",
    `Unknown);], (`Disjunction [(`Negation (`Conjunction [(`Exists
      ([("x43", `Unknown);], (`Conjunction [(`Equality ((`Unknown,
      (`Variable "x43")), (`Unknown, (`Variable "s"))));(`Predicate
        ("abAuthPurse", [(`Unknown, (`Variable "x43"));(`Unknown,
        (`Variable "x46"));]));])));(`Exists ([("x48", `Unknown);],
    (`Conjunction [(`Predicate ("abLost", [(`Unknown, (`Variable
      "x46"));(`Unknown, (`Variable "x49"));(`Unknown, (`Variable
      "x48"));]));(`Equality ((`Unknown, (`Variable "x48")), (`Unknown,
    (`Variable "s'"))));])));]));(`Conjunction [(`Exists ([("x43",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x43")),
    (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x43"));(`Unknown, (`Variable "x46"));]));])));(`Exists
      ([("x47", `Unknown);], (`Conjunction [(`Predicate ("abLost",
      [(`Unknown, (`Variable "x46"));(`Unknown, (`Variable
        "x49"));(`Unknown, (`Variable "x47"));]));(`Equality ((`Unknown,
      (`Variable "x47")), (`Unknown, (`Variable
        "s"))));])));]);])));]);]);]);]);]);]));(`Conjunction
  [(`Conjunction [(`Forall ([("x42", `Unknown);], (`Disjunction [(`Negation
    (`Exists ([("x41", `Unknown);], (`Conjunction [(`Exists ([("x40",
    `Unknown);], (`Conjunction [(`Exists ([("x39", `Unknown);],
    (`Conjunction [(`Equality ((`Unknown, (`Variable "x39")), (`Unknown,
    (`Variable "s'"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
      "x39"));(`Unknown, (`Variable "x40"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x40"));(`Unknown, (`Variable
        "x42"));(`Unknown, (`Variable "x41"));]));])));(`Equality
      ((`Unknown, (`Variable "x41")), (`Unknown, (`Variable
        "s'"))));]))));(`Exists ([("x38", `Unknown);], (`Conjunction
    [(`Exists ([("x37", `Unknown);], (`Conjunction [(`Exists ([("x36",
    `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable "x36")),
    (`Unknown, (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown,
    (`Variable "x36"));(`Unknown, (`Variable "x37"));]));])));(`Predicate
      ("abBalance", [(`Unknown, (`Variable "x37"));(`Unknown, (`Variable
        "x42"));(`Unknown, (`Variable "x38"));]));])));(`Equality
      ((`Unknown, (`Variable "x38")), (`Unknown, (`Variable
        "s"))));])));])));]);(`Conjunction [(`Conjunction [(`Forall
    ([("x35", `Unknown);], (`Disjunction [(`Negation (`Disjunction
      [(`Exists ([("x33", `Unknown);], (`Conjunction [(`Exists ([("x32",
      `Unknown);], (`Conjunction [(`Exists ([("x31", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x31")), (`Unknown,
      (`Variable "s'"))));(`Predicate ("abAuthPurse", [(`Unknown,
      (`Variable "x31"));(`Unknown, (`Variable "x32"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x32"));(`Unknown, (`Variable
          "x35"));(`Unknown, (`Variable "x33"));]));])));(`Equality
        ((`Unknown, (`Variable "x33")), (`Unknown, (`Variable
          "s'"))));])));(`Exists ([("x30", `Unknown);], (`Conjunction
        [(`Exists ([("x29", `Unknown);], (`Conjunction [(`Exists ([("x28",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x28")), (`Unknown, (`Variable "s'"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x28"));(`Unknown,
          (`Variable "x29"));]));])));(`Predicate ("abLost", [(`Unknown,
        (`Variable "x29"));(`Unknown, (`Variable "x35"));(`Unknown,
        (`Variable "x30"));]));])));(`Equality ((`Unknown, (`Variable
          "x30")), (`Unknown, (`Variable "s'"))));])));]));(`Disjunction
      [(`Exists ([("x27", `Unknown);], (`Conjunction [(`Exists ([("x26",
      `Unknown);], (`Conjunction [(`Exists ([("x25", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x25")), (`Unknown,
      (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x25"));(`Unknown, (`Variable "x26"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x26"));(`Unknown, (`Variable
          "x35"));(`Unknown, (`Variable "x27"));]));])));(`Equality
        ((`Unknown, (`Variable "x27")), (`Unknown, (`Variable
          "s"))));])));(`Exists ([("x24", `Unknown);], (`Conjunction
        [(`Exists ([("x23", `Unknown);], (`Conjunction [(`Exists ([("x22",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x22")), (`Unknown, (`Variable "s"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x22"));(`Unknown,
          (`Variable "x23"));]));])));(`Predicate ("abLost", [(`Unknown,
        (`Variable "x23"));(`Unknown, (`Variable "x35"));(`Unknown,
        (`Variable "x24"));]));])));(`Equality ((`Unknown, (`Variable
          "x24")), (`Unknown, (`Variable "s"))));])));]);])));(`Forall
    ([("x34", `Unknown);], (`Disjunction [(`Negation (`Disjunction
      [(`Exists ([("x27", `Unknown);], (`Conjunction [(`Exists ([("x26",
      `Unknown);], (`Conjunction [(`Exists ([("x25", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x25")), (`Unknown,
      (`Variable "s"))));(`Predicate ("abAuthPurse", [(`Unknown, (`Variable
        "x25"));(`Unknown, (`Variable "x26"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x26"));(`Unknown, (`Variable
          "x34"));(`Unknown, (`Variable "x27"));]));])));(`Equality
        ((`Unknown, (`Variable "x27")), (`Unknown, (`Variable
          "s"))));])));(`Exists ([("x24", `Unknown);], (`Conjunction
        [(`Exists ([("x23", `Unknown);], (`Conjunction [(`Exists ([("x22",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x22")), (`Unknown, (`Variable "s"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x22"));(`Unknown,
          (`Variable "x23"));]));])));(`Predicate ("abLost", [(`Unknown,
        (`Variable "x23"));(`Unknown, (`Variable "x34"));(`Unknown,
        (`Variable "x24"));]));])));(`Equality ((`Unknown, (`Variable
          "x24")), (`Unknown, (`Variable "s"))));])));]));(`Disjunction
      [(`Exists ([("x33", `Unknown);], (`Conjunction [(`Exists ([("x32",
      `Unknown);], (`Conjunction [(`Exists ([("x31", `Unknown);],
      (`Conjunction [(`Equality ((`Unknown, (`Variable "x31")), (`Unknown,
      (`Variable "s'"))));(`Predicate ("abAuthPurse", [(`Unknown,
      (`Variable "x31"));(`Unknown, (`Variable "x32"));]));])));(`Predicate
        ("abBalance", [(`Unknown, (`Variable "x32"));(`Unknown, (`Variable
          "x34"));(`Unknown, (`Variable "x33"));]));])));(`Equality
        ((`Unknown, (`Variable "x33")), (`Unknown, (`Variable
          "s'"))));])));(`Exists ([("x30", `Unknown);], (`Conjunction
        [(`Exists ([("x29", `Unknown);], (`Conjunction [(`Exists ([("x28",
        `Unknown);], (`Conjunction [(`Equality ((`Unknown, (`Variable
          "x28")), (`Unknown, (`Variable "s'"))));(`Predicate
          ("abAuthPurse", [(`Unknown, (`Variable "x28"));(`Unknown,
          (`Variable "x29"));]));])));(`Predicate ("abLost", [(`Unknown,
        (`Variable "x29"));(`Unknown, (`Variable "x34"));(`Unknown,
        (`Variable "x30"));]));])));(`Equality ((`Unknown, (`Variable
          "x30")), (`Unknown, (`Variable
          "s'"))));])));]);])));]);]);]);]);])));])); 
]}