-- LOGPROOF1


Derivation of

Any q:
(  perm([1,2,3],p)
 & append(q,[2],p))

Narrowing the preceding formula leads to the formula

Any q:
(  Any p1 q1:
   (  perm([2,3],q1)
    & insert(1,q1,p1)
    & p = p1)
 & append(q,[2],p))

Simplifying the preceding formula (4 steps) leads to the formula

  Any q1:
  (  perm([2,3],q1)
   & insert(1,q1,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any q1:
  (  Any p3 q3:
     (  perm([3],q3)
      & insert(2,q3,p3)
      & q1 = p3)
   & insert(1,q1,p))
& Any q:
  (append(q,[2],p))

Simplifying the preceding formula (2 steps) leads to the formula

  Any q1:
  (  Any q3:
     (  perm([3],q3)
      & insert(2,q3,q1))
   & insert(1,q1,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any q1:
  (  Any q3:
     (  Any p5 q5:
        (  perm([],q5)
         & insert(3,q5,p5)
         & q3 = p5)
      & insert(2,q3,q1))
   & insert(1,q1,p))
& Any q:
  (append(q,[2],p))

Simplifying the preceding formula (2 steps) leads to the formula

  Any q1:
  (  Any q3:
     (  Any q5:
        (  perm([],q5)
         & insert(3,q5,q3))
      & insert(2,q3,q1))
   & insert(1,q1,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any q1:
  (  Any q3:
     (  Any q5:
        (  q5 = []
         & insert(3,q5,q3))
      & insert(2,q3,q1))
   & insert(1,q1,p))
& Any q:
  (append(q,[2],p))

Simplifying the preceding formula (2 steps) leads to the formula

  Any q1:
  (  Any q3:
     (  insert(3,[],q3)
      & insert(2,q3,q1))
   & insert(1,q1,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any q1:
  (  Any q3:
     (  q3 = 3:[]
      & insert(2,q3,q1))
   & insert(1,q1,p))
& Any q:
  (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

  Any q1:
  (  insert(2,[3],q1)
   & insert(1,q1,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any q1:
  (  (  q1 = 2:[3]
      | Any p9:
        (  insert(2,[],p9)
         & q1 = 3:p9))
   & insert(1,q1,p))
& Any q:
  (append(q,[2],p))

Simplifying the preceding formula (6 steps) leads to the formula

    insert(1,[2,3],p)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    (  p = 1:[2,3]
     | Any p11:
       (  insert(1,[3],p11)
        & p = 2:p11))
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (5 steps) leads to the formula

    p = [1,2,3]
  & Any q:
    (append(q,[2],[1,2,3]))
|   Any p11:
    (  insert(1,[3],p11)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any q:
    (Any L6:
     (  append(L6,[2],[2,3])
      & q = 1:L6))
|   Any p11:
    (  insert(1,[3],p11)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L6:
    (append(L6,[2],[2,3]))
|   Any p11:
    (  insert(1,[3],p11)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L6:
    (Any L9:
     (  append(L9,[2],[3])
      & L6 = 2:L9))
|   Any p11:
    (  insert(1,[3],p11)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L9:
    (append(L9,[2],[3]))
|   Any p11:
    (  insert(1,[3],p11)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L9:
    (Any L12:
     (  append(L12,[2],[])
      & L9 = 3:L12))
|   Any p11:
    (  insert(1,[3],p11)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   Any p11:
    (  insert(1,[3],p11)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   Any p11:
    (  (  p11 = 1:[3]
        | Any p16:
          (  insert(1,[],p16)
           & p11 = 3:p16))
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (10 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any q:
    (append(q,[2],[2,1,3]))
|   Any p11:
    (  Any p16:
       (  insert(1,[],p16)
        & p11 = 3:p16)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any q:
    (Any L15:
     (  append(L15,[2],[1,3])
      & q = 2:L15))
|   Any p11:
    (  Any p16:
       (  insert(1,[],p16)
        & p11 = 3:p16)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L15:
    (append(L15,[2],[1,3]))
|   Any p11:
    (  Any p16:
       (  insert(1,[],p16)
        & p11 = 3:p16)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L15:
    (Any L18:
     (  append(L18,[2],[3])
      & L15 = 1:L18))
|   Any p11:
    (  Any p16:
       (  insert(1,[],p16)
        & p11 = 3:p16)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L18:
    (append(L18,[2],[3]))
|   Any p11:
    (  Any p16:
       (  insert(1,[],p16)
        & p11 = 3:p16)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L18:
    (Any L21:
     (  append(L21,[2],[])
      & L18 = 3:L21))
|   Any p11:
    (  Any p16:
       (  insert(1,[],p16)
        & p11 = 3:p16)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   Any p11:
    (  Any p16:
       (  insert(1,[],p16)
        & p11 = 3:p16)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   Any p11:
    (  Any p16:
       (  p16 = 1:[]
        & p11 = 3:p16)
     & p = 2:p11)
  & Any q:
    (append(q,[2],p))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (13 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any q:
    (append(q,[2],[2,3,1]))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any q:
    (Any L24:
     (  append(L24,[2],[3,1])
      & q = 2:L24))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L24:
    (append(L24,[2],[3,1]))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L24:
    (Any L27:
     (  append(L27,[2],[1])
      & L24 = 3:L27))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L27:
    (append(L27,[2],[1]))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L27:
    (Any L30:
     (  append(L30,[2],[])
      & L27 = 1:L30))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   Any q1:
    (  Any p9:
       (  insert(2,[],p9)
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   Any q1:
    (  Any p9:
       (  p9 = 2:[]
        & q1 = 3:p9)
     & insert(1,q1,p))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (9 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   insert(1,[3,2],p)
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   (  p = 1:[3,2]
     | Any p26:
       (  insert(1,[2],p26)
        & p = 3:p26))
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (5 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [1,3,2]
  & Any q:
    (append(q,[2],[1,3,2]))
|   Any p26:
    (  insert(1,[2],p26)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [1,3,2]
  & Any q:
    (Any L33:
     (  append(L33,[2],[3,2])
      & q = 1:L33))
|   Any p26:
    (  insert(1,[2],p26)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [1,3,2]
  & Any L33:
    (append(L33,[2],[3,2]))
|   Any p26:
    (  insert(1,[2],p26)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [1,3,2]
  & Any L33:
    (Any L36:
     (  append(L36,[2],[2])
      & L33 = 3:L36))
|   Any p26:
    (  insert(1,[2],p26)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [1,3,2]
  & Any L36:
    (append(L36,[2],[2]))
|   Any p26:
    (  insert(1,[2],p26)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [1,3,2]
  & Any L36:
    (  L36 = []
     | Any L39:
       (  append(L39,[2],[])
        & L36 = 2:L39))
|   Any p26:
    (  insert(1,[2],p26)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))

Simplifying the preceding formula (7 steps) leads to the formula

    Any p26:
    (  insert(1,[2],p26)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))

Narrowing the preceding formula leads to the formula

    Any p26:
    (  (  p26 = 1:[2]
        | Any p31:
          (  insert(1,[],p31)
           & p26 = 2:p31))
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))

Simplifying the preceding formula (10 steps) leads to the formula

    p = [3,1,2]
  & Any q:
    (append(q,[2],[3,1,2]))
|   Any p26:
    (  Any p31:
       (  insert(1,[],p31)
        & p26 = 2:p31)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))

Narrowing the preceding formula leads to the formula

    p = [3,1,2]
  & Any q:
    (Any L42:
     (  append(L42,[2],[1,2])
      & q = 3:L42))
|   Any p26:
    (  Any p31:
       (  insert(1,[],p31)
        & p26 = 2:p31)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [3,1,2]
  & Any L42:
    (append(L42,[2],[1,2]))
|   Any p26:
    (  Any p31:
       (  insert(1,[],p31)
        & p26 = 2:p31)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))

Narrowing the preceding formula leads to the formula

    p = [3,1,2]
  & Any L42:
    (Any L45:
     (  append(L45,[2],[2])
      & L42 = 1:L45))
|   Any p26:
    (  Any p31:
       (  insert(1,[],p31)
        & p26 = 2:p31)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))

Simplifying the preceding formula (3 steps) leads to the formula

    p = [3,1,2]
  & Any L45:
    (append(L45,[2],[2]))
|   Any p26:
    (  Any p31:
       (  insert(1,[],p31)
        & p26 = 2:p31)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))

Narrowing the preceding formula leads to the formula

    p = [3,1,2]
  & Any L45:
    (  L45 = []
     | Any L48:
       (  append(L48,[2],[])
        & L45 = 2:L48))
|   Any p26:
    (  Any p31:
       (  insert(1,[],p31)
        & p26 = 2:p31)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))

Simplifying the preceding formula (7 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
| p = [1,3,2]
|   Any p26:
    (  Any p31:
       (  insert(1,[],p31)
        & p26 = 2:p31)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))
| p = [3,1,2]

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
| p = [1,3,2]
|   Any p26:
    (  Any p31:
       (  p31 = 1:[]
        & p26 = 2:p31)
     & p = 3:p26)
  & Any q:
    (append(q,[2],p))
| p = [3,1,2]

Simplifying the preceding formula (13 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
| p = [1,3,2]
|   p = [3,2,1]
  & Any q:
    (append(q,[2],[3,2,1]))
| p = [3,1,2]

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
| p = [1,3,2]
|   p = [3,2,1]
  & Any q:
    (Any L51:
     (  append(L51,[2],[2,1])
      & q = 3:L51))
| p = [3,1,2]

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
| p = [1,3,2]
|   p = [3,2,1]
  & Any L51:
    (append(L51,[2],[2,1]))
| p = [3,1,2]

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
| p = [1,3,2]
|   p = [3,2,1]
  & Any L51:
    (Any L54:
     (  append(L54,[2],[1])
      & L51 = 2:L54))
| p = [3,1,2]

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
| p = [1,3,2]
|   p = [3,2,1]
  & Any L54:
    (append(L54,[2],[1]))
| p = [3,1,2]

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
| p = [1,3,2]
|   p = [3,2,1]
  & Any L54:
    (Any L57:
     (  append(L57,[2],[])
      & L54 = 1:L57))
| p = [3,1,2]

Simplifying the preceding formula (3 steps) leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
| p = [1,3,2]
|   p = [3,2,1]
  & Any L57:
    (append(L57,[2],[]))
| p = [3,1,2]

Narrowing the preceding formula (4 steps) leads to the formula

  p = [1,3,2]
| p = [3,1,2]

Number of proof steps: 63