Proof summary for theory my_list_induction
    less_wf...............................proved - complete   [shostak](0.04 s)
    list_length_induction.................proved - complete   [shostak](0.00 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.05 s)

 Proof summary for theory my_list_props
    occ_TCC1..............................proved - complete   [shostak](0.01 s)
    occ_TCC2..............................proved - complete   [shostak](0.03 s)
    occ_nth...............................proved - complete   [shostak](0.11 s)
    nth_occ...............................proved - complete   [shostak](0.10 s)
    perm_null.............................proved - complete   [shostak](0.03 s)
    perm_commutative......................proved - complete   [shostak](0.01 s)
    append_occ............................proved - complete   [shostak](0.07 s)
    length_append.........................proved - complete   [shostak](0.11 s)
    nth_append_TCC1.......................proved - complete   [shostak](0.04 s)
    nth_append_TCC2.......................proved - complete   [shostak](0.05 s)
    nth_append............................proved - complete   [shostak](0.30 s)
    Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.86 s)

 Proof summary for theory SPLIT
    split_TCC1............................proved - complete   [shostak](0.04 s)
    split_length..........................proved - complete   [shostak](0.13 s)
    split_occ.............................proved - complete   [shostak](0.14 s)
    split_lwb_upb.........................proved - complete   [shostak](0.18 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.50 s)

 Proof summary for theory QS
    qs_TCC1...............................proved - complete   [shostak](0.07 s)
    qs_TCC2...............................proved - complete   [shostak](0.06 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.12 s)

 Proof summary for theory SORTED
    sorted?_TCC1..........................proved - complete   [shostak](0.03 s)
    sorted_append.........................proved - complete   [shostak](0.53 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.56 s)

 Proof summary for theory QS_props
    qs_perm...............................proved - complete   [shostak](1.35 s)
    occ_upb...............................proved - complete   [shostak](0.12 s)
    occ_lwb...............................proved - complete   [shostak](0.10 s)
    upb_perm..............................proved - complete   [shostak](0.08 s)
    lwb_perm..............................proved - complete   [shostak](0.08 s)
    qs_sorted.............................proved - complete   [shostak](0.74 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (2.48 s)

Grand Totals: 27 proofs, 27 attempted, 27 succeeded (4.56 s)