(i a1 a1b1) (i b1 a1b1) (i a2 a2b2) (i b2 a2b2) (i a1 a1c1) (i c1 a1c1) (i a2 a2c2) (i c2 a2c2) (i c1 b1c1) (i b1 b1c1) (i c2 b2c2) (i b2 b2c2) (i o oa) (i o ob) (i o oc) (i a1 oa) (i a2 oa) (i b1 ob) (i b2 ob) (i c1 oc) (i c2 oc) (i bc b1c1) (i bc b2c2) (i ac a1c1) (i ac a2c2) (i ab a1b1) (i ab a2b2) (p a1 a1) (p b1 b1) (p a2 a2) (p b2 b2) (p c1 c1) (p c2 c2) (p o o) (p bc bc) (p ac ac) (p ab ab) (l a1b1 a1b1) (l a2b2 a2b2) (l a1c1 a1c1) (l a2c2 a2c2) (l b1c1 b1c1) (l b2c2 b2c2) (l oa oa) (l ob ob) (l oc oc) line(a1, b2) (i a1 C0)/\(i b2 C0) (l C0 C0) point(par(0), oc) (i C1 C0)/\(i C1 oc) (p C1 C1) line(par(1), ac) (i C1 C2)/\(i ac C2) (l C2 C2) point(par(2), a2b2) (i C3 C2)/\(i C3 a2b2) (p C3 C3) line(par(3), o) (i C3 C4)/\(i o C4) (l C4 C4) point(par(4), a1c1) (i C5 C4)/\(i C5 a1c1) (p C5 C5) pappus(b2, c2, par(5)) stack pushed, stack: (l a2b2 C0) \/ (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (l a2b2 C0) (l C0 a2b2) (i a2 C0) (i ab C0) (i a1 a2b2) (i C1 a2b2) (i C3 C0) stack pushed, stack: (p a1 ab) \/ (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 ab) (p ab a1) (i ab a1c1) (i ab oa) stack pushed, stack: (p a2 ab) \/ (l a2b2 oa) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a2 ab) (p ab a2) (p a1 a2) (p a2 a1) false falid, stack: (l a2b2 oa) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2b2 oa) (l oa a2b2) (l C0 oa) (l oa C0) (i b2 oa) (i o a2b2) (i o C0) (i C1 oa) (i C3 oa) stack pushed, stack: (p b2 o) \/ (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p b2 o) (p o b2) (i b2 oc) (i b2 C4) (i o b2c2) stack pushed, stack: (p b2 C1) \/ (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p b2 C1) (p C1 b2) (p o C1) (p C1 o) (i b2 C2) (i o C2) (i C1 b2c2) (i C1 ob) (i C1 C4) stack pushed, stack: (p b2 C3) \/ (l a2b2 C4) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p b2 C3) (p C3 b2) (p o C3) (p C3 o) (p C1 C3) (p C3 C1) (i C3 b2c2) (i C3 ob) (i C3 oc) stack pushed, stack: (p c2 b2) \/ (l b2c2 oc) :: (l a2b2 C4) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p c2 b2) (p b2 c2) (p o c2) (p c2 o) (p C1 c2) (p c2 C1) (p C3 c2) (p c2 C3) (i c2 a2b2) false falid, stack: (l b2c2 oc) :: (l a2b2 C4) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l b2c2 oc) (l oc b2c2) (i c1 b2c2) (i bc oc) stack pushed, stack: (p c1 bc) \/ (l b1c1 oc) :: (l a2b2 C4) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p c1 bc) (p bc c1) (i bc a1c1) valid, stack: (l b1c1 oc) :: (l a2b2 C4) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l b1c1 oc) (l oc b1c1) (l b2c2 b1c1) (l b1c1 b2c2) false falid, stack: (l a2b2 C4) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2b2 C4) (l C4 a2b2) (l C0 C4) (l C4 C0) (l oa C4) (l C4 oa) (i a2 C4) (i a1 C4) (i ab C4) (i C5 a2b2) (i C5 C0) (i C5 oa) stack pushed, stack: (p b2 C3) \/ (l a2b2 C2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p b2 C3) (p C3 b2) (p o C3) (p C3 o) (p C1 C3) (p C3 C1) (i C3 b2c2) (i C3 ob) (i C3 oc) stack pushed, stack: (p a1 C5) \/ (l a1c1 oa) :: (l a2b2 C2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 C5) (p C5 a1) (p ab C5) (p C5 ab) (i C5 a1b1) stack pushed, stack: (p c2 b2) \/ (l b2c2 oc) :: (l a1c1 oa) :: (l a2b2 C2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p c2 b2) (p b2 c2) (p o c2) (p c2 o) (p C1 c2) (p c2 C1) (p C3 c2) (p c2 C3) (i c2 a2b2) false falid, stack: (l b2c2 oc) :: (l a1c1 oa) :: (l a2b2 C2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l b2c2 oc) (l oc b2c2) (i c1 b2c2) (i bc oc) stack pushed, stack: (p c1 bc) \/ (l b1c1 oc) :: (l a1c1 oa) :: (l a2b2 C2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p c1 bc) (p bc c1) (i bc a1c1) valid, stack: (l b1c1 oc) :: (l a1c1 oa) :: (l a2b2 C2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l b1c1 oc) (l oc b1c1) (l b2c2 b1c1) (l b1c1 b2c2) false falid, stack: (l a1c1 oa) :: (l a2b2 C2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 oa) (l oa a1c1) (l a2b2 a1c1) (l a1c1 a2b2) (l C0 a1c1) (l a1c1 C0) (l C4 a1c1) (l a1c1 C4) (i a2 a1c1) (i b2 a1c1) valid, stack: (l a2b2 C2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2b2 C2) (l C2 a2b2) (l C0 C2) (l C2 C0) (l oa C2) (l C2 oa) (l C4 C2) (l C2 C4) (i a2 C2) (i a1 C2) (i ab C2) (i ac a2b2) (i ac C0) (i ac oa) (i ac C4) (i C5 C2) stack pushed, stack: (p a2 ac) \/ (l a2b2 a2c2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a2 ac) (p ac a2) (i a2 a1c1) stack pushed, stack: (p a2 ab) \/ (l a2b2 a1c1) :: (l a2b2 a2c2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a2 ab) (p ab a2) (p a1 a2) (p a2 a1) false falid, stack: (l a2b2 a1c1) :: (l a2b2 a2c2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2b2 a1c1) (l a1c1 a2b2) (l C0 a1c1) (l a1c1 C0) (l oa a1c1) (l a1c1 oa) (l C4 a1c1) (l a1c1 C4) (l C2 a1c1) (l a1c1 C2) (i b2 a1c1) valid, stack: (l a2b2 a2c2) :: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2b2 a2c2) (l a2c2 a2b2) (l C0 a2c2) (l a2c2 C0) (l oa a2c2) (l a2c2 oa) (l C4 a2c2) (l a2c2 C4) (l C2 a2c2) (l a2c2 C2) (i b2 a2c2) false falid, stack: (l a2b2 oc) :: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2b2 oc) (l oc a2b2) (l C0 oc) (l oc C0) (l oa oc) (l oc oa) (i a2 oc) false falid, stack: (l a2b2 ob) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2b2 ob) (l ob a2b2) (l C0 ob) (l ob C0) (l oa ob) (l ob oa) (i a2 ob) (i a1 ob) (i ab ob) (i b1 a2b2) (i b1 C0) (i b1 oa) (i C1 ob) (i C3 ob) stack pushed, stack: (p a1 b1) \/ (l a1b1 oa) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 b1) (p b1 a1) (p ab b1) (p b1 ab) (i a1 b1c1) false falid, stack: (l a1b1 oa) :: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1b1 oa) (l oa a1b1) (l a2b2 a1b1) (l a1b1 a2b2) false falid, stack: (l a1b1 C0) :: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1b1 C0) (l C0 a1b1) (l a2b2 a1b1) (l a1b1 a2b2) false falid, stack: (l a2c2 oc) \/ (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (l a2c2 oc) (l oc a2c2) (i a2 oc) (i o a2c2) (i c1 a2c2) (i ac oc) (i C1 a2c2) stack pushed, stack: (p c1 ac) \/ (l a1c1 oc) :: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p c1 ac) (p ac c1) (i c1 C2) (i ac b1c1) stack pushed, stack: (p a2 o) \/ (l a2c2 oa) :: (l a1c1 oc) :: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a2 o) (p o a2) (i a2 ob) (i a2 C4) (i o a2b2) stack pushed, stack: (p a2 b2) \/ (l a2b2 ob) :: (l a2c2 oa) :: (l a1c1 oc) :: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a2 b2) (p b2 a2) (p o b2) (p b2 o) (i a2 b2c2) false falid, stack: (l a2b2 ob) :: (l a2c2 oa) :: (l a1c1 oc) :: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2b2 ob) (l ob a2b2) (i b1 a2b2) (i ab ob) (i C3 ob) stack pushed, stack: (p b1 ab) \/ (l a1b1 ob) :: (l a2c2 oa) :: (l a1c1 oc) :: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p b1 ab) (p ab b1) (i ab b1c1) valid, stack: (l a1b1 ob) :: (l a2c2 oa) :: (l a1c1 oc) :: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1b1 ob) (l ob a1b1) (l a2b2 a1b1) (l a1b1 a2b2) false falid, stack: (l a2c2 oa) :: (l a1c1 oc) :: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2c2 oa) (l oa a2c2) (l oc oa) (l oa oc) (i c2 oa) (i a1 a2c2) (i a1 oc) (i c1 oa) (i ac oa) (i C1 oa) stack pushed, stack: (p a1 c1) \/ (l a1c1 oa) :: (l a1c1 oc) :: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 c1) (p c1 a1) (p ac a1) (p a1 ac) (i a1 b1c1) false falid, stack: (l a1c1 oa) :: (l a1c1 oc) :: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 oa) (l oa a1c1) (l a2c2 a1c1) (l a1c1 a2c2) false falid, stack: (l a1c1 oc) :: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 oc) (l oc a1c1) (l a2c2 a1c1) (l a1c1 a2c2) false falid, stack: (l a1c1 C4) \/ (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (l a1c1 C4) (l C4 a1c1) (i a1 C4) (i c1 C4) (i ac C4) (i C3 a1c1) (i o a1c1) stack pushed, stack: (p a1 o) \/ (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 o) (p o a1) (i a1 ob) (i a1 oc) (i o a1b1) (i o C0) stack pushed, stack: (p a1 b1) \/ (l a1b1 ob) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 b1) (p b1 a1) (p o b1) (p b1 o) (i a1 b1c1) false falid, stack: (l a1b1 ob) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1b1 ob) (l ob a1b1) (i b2 a1b1) (i ab ob) stack pushed, stack: (p a1 b2) \/ (l a1b1 C0) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 b2) (p b2 a1) (p o b2) (p b2 o) (i a1 a2b2) (i o a2b2) (i a1 b2c2) valid, stack: (l a1b1 C0) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1b1 C0) (l C0 a1b1) (l ob C0) (l C0 ob) (i b1 C0) (i ab C0) (i C1 a1b1) (i C1 ob) stack pushed, stack: (p a1 C1) \/ (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 C1) (p C1 a1) (p o C1) (p C1 o) (i a1 C2) (i o C2) (i C1 a1c1) (i C1 oa) (i C1 C4) stack pushed, stack: (p b2 ab) \/ (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p b2 ab) (p ab b2) (i ab b2c2) stack pushed, stack: (p a1 c1) \/ (l a1c1 oc) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 c1) (p c1 a1) (p o c1) (p c1 o) (p C1 c1) (p c1 C1) (i a1 b1c1) false falid, stack: (l a1c1 oc) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 oc) (l oc a1c1) (l C4 oc) (l oc C4) (i c2 a1c1) (i c2 C4) (i ac oc) (i C3 oc) (i C5 oc) stack pushed, stack: (p a1 ac) \/ (l a1c1 C2) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 ac) (p ac a1) (p o ac) (p ac o) (p C1 ac) (p ac C1) (i a1 a2c2) (i o a2c2) (i C1 a2c2) (i ac a1b1) (i ac oa) (i ac C0) (i ac ob) stack pushed, stack: (p a1 C3) \/ (l a1c1 C2) :: (l a1c1 C2) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 C3) (p C3 a1) (p o C3) (p C3 o) (p C1 C3) (p C3 C1) (p ac C3) (p C3 ac) (i a1 a2b2) (i o a2b2) (i C1 a2b2) (i ac a2b2) (i C3 a1b1) (i C3 oa) (i C3 C0) (i C3 ob) (i C3 a2c2) stack pushed, stack: (p a1 ab) \/ (l a1b1 a2b2) :: (l a1c1 C2) :: (l a1c1 C2) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 ab) (p ab a1) (p o ab) (p ab o) (p C1 ab) (p ab C1) (p b2 a1) (p a1 b2) (p o b2) (p b2 o) (p C1 b2) (p b2 C1) (p ac ab) (p ab ac) (p b2 ac) (p ac b2) (p C3 ab) (p ab C3) (p b2 C3) (p C3 b2) (i a1 b2c2) valid, stack: (l a1b1 a2b2) :: (l a1c1 C2) :: (l a1c1 C2) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1b1 a2b2) false falid, stack: (l a1c1 C2) :: (l a1c1 C2) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 C2) (l C2 a1c1) (l C4 C2) (l C2 C4) (l oc C2) (l C2 oc) (i c1 C2) (i c2 C2) (i C5 C2) stack pushed, stack: (p a1 c2) \/ (l a1c1 a2c2) :: (l a1c1 C2) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 c2) (p c2 a1) (p o c2) (p c2 o) (p C1 c2) (p c2 C1) (p ac c2) (p c2 ac) (i a1 b2c2) valid, stack: (l a1c1 a2c2) :: (l a1c1 C2) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 a2c2) false falid, stack: (l a1c1 C2) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 C2) (l C2 a1c1) (l C4 C2) (l C2 C4) (l oc C2) (l C2 oc) (i c1 C2) (i c2 C2) (i C5 C2) stack pushed, stack: (p c2 ac) \/ (l a2c2 oc) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p c2 ac) (p ac c2) (i ac b2c2) valid, stack: (l a2c2 oc) :: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2c2 oc) (l oc a2c2) (l a1c1 a2c2) false falid, stack: (l a2b2 ob) :: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2b2 ob) (l ob a2b2) (l a1b1 a2b2) false falid, stack: (l a1b1 oc) :: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1b1 oc) (l oc a1b1) (l ob oc) (l oc ob) (l C0 oc) (l oc C0) (i b1 oc) false falid, stack: (l a1c1 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 oa) (l oa a1c1) (l C4 oa) (l oa C4) (i c1 oa) (i a2 a1c1) (i a2 C4) (i ac oa) (i C3 oa) (i C5 oa) stack pushed, stack: (p a2 C3) \/ (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a2 C3) (p C3 a2) (i a2 C2) (i C3 a2c2) stack pushed, stack: (p c1 o) \/ (l a1c1 oc) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p c1 o) (p o c1) (i c1 ob) (i o b1c1) stack pushed, stack: (p a2 ac) \/ (l a2c2 oa) :: (l a1c1 oc) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a2 ac) (p ac a2) (p C3 ac) (p ac C3) (i ac a2b2) stack pushed, stack: (p c1 b1) \/ (l b1c1 ob) :: (l a2c2 oa) :: (l a1c1 oc) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p c1 b1) (p b1 c1) (p o b1) (p b1 o) (i c1 a1b1) false falid, stack: (l b1c1 ob) :: (l a2c2 oa) :: (l a1c1 oc) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l b1c1 ob) (l ob b1c1) (i b2 b1c1) (i bc ob) stack pushed, stack: (p b2 bc) \/ (l b2c2 ob) :: (l a2c2 oa) :: (l a1c1 oc) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p b2 bc) (p bc b2) (i bc a2b2) valid, stack: (l b2c2 ob) :: (l a2c2 oa) :: (l a1c1 oc) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l b2c2 ob) (l ob b2c2) (l b1c1 b2c2) false falid, stack: (l a2c2 oa) :: (l a1c1 oc) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2c2 oa) (l oa a2c2) (l a1c1 a2c2) false falid, stack: (l a1c1 oc) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 oc) (l oc a1c1) (l C4 oc) (l oc C4) (l oa oc) (l oc oa) (i a1 oc) (i a2 oc) (i C3 oc) (i c2 a1c1) (i c2 C4) (i c2 oa) (i ac oc) (i C1 a1c1) (i C1 C4) (i C1 oa) (i C5 oc) stack pushed, stack: (p a1 C1) \/ (l a1c1 C0) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 C1) (p C1 a1) (i a1 C2) (i C1 a1b1) stack pushed, stack: (p a1 ac) \/ (l a1c1 C2) :: (l a1c1 C0) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 ac) (p ac a1) (p C1 ac) (p ac C1) (i a1 a2c2) (i C1 a2c2) (i ac a1b1) (i ac C0) stack pushed, stack: (p a1 C3) \/ (l a1c1 C2) :: (l a1c1 C2) :: (l a1c1 C0) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 C3) (p C3 a1) (p a2 a1) false falid, stack: (l a1c1 C2) :: (l a1c1 C2) :: (l a1c1 C0) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 C2) (l C2 a1c1) (l C4 C2) (l C2 C4) (l oa C2) (l C2 oa) (l oc C2) (l C2 oc) (i c1 C2) (i o C2) (i c2 C2) (i C5 C2) stack pushed, stack: (p a1 C3) \/ (l a1c1 a2c2) :: (l a1c1 C2) :: (l a1c1 C0) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a1 C3) (p C3 a1) (p a2 a1) false falid, stack: (l a1c1 a2c2) :: (l a1c1 C2) :: (l a1c1 C0) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 a2c2) false falid, stack: (l a1c1 C2) :: (l a1c1 C0) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 C2) (l C2 a1c1) (l C4 C2) (l C2 C4) (l oa C2) (l C2 oa) (l oc C2) (l C2 oc) (i c1 C2) (i o C2) (i c2 C2) (i C5 C2) stack pushed, stack: (p a2 c2) \/ (l a2c2 oa) :: (l a1c1 C0) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack top tailed: (p a2 c2) (p c2 a2) (p C3 c2) (p c2 C3) (i a2 b2c2) false falid, stack: (l a2c2 oa) :: (l a1c1 C0) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2c2 oa) (l oa a2c2) (l a1c1 a2c2) false falid, stack: (l a1c1 C0) :: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a1c1 C0) (l C0 a1c1) (l C4 C0) (l C0 C4) (l oa C0) (l C0 oa) (l oc C0) (l C0 oc) (i c1 C0) (i o C0) (i a2 C0) (i C3 C0) (i c2 C0) false falid, stack: (l a2b2 oa) :: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l a2b2 oa) (l oa a2b2) (l a1c1 a2b2) (l a2b2 a1c1) (l C4 a2b2) (l a2b2 C4) (i b2 oa) (i b2 a1c1) valid, stack: (exists A:dom,(l A A)/\(i b2 A)/\(i c2 A)/\(i C5 A)) :: nil stack popped: (l C6 C6)/\(i b2 C6)/\(i c2 C6)/\(i C5 C6) stack pushed, stack: (p c2 b2) \/ (l b2c2 C6) :: nil stack top tailed: (p c2 b2) (p b2 c2) (i c2 a2b2) false falid, stack: (l b2c2 C6) :: nil stack popped: (l b2c2 C6) (l C6 b2c2) (i bc C6) (i C5 b2c2) point(par(4), a1b1) (i C7 C4)/\(i C7 a1b1) (p C7 C7) pappus(par(1), par(7), bc) stack pushed, stack: (l oc C0) \/ (l C4 a1b1) \/ (l b2c2 b1c1) \/ (exists A:dom,(l A A)/\(i C1 A)/\(i C7 A)/\(i bc A)) :: nil stack top tailed: (l oc C0) (l C0 oc) (i o C0) (i c1 C0) (i c2 C0) (i a1 oc) (i b2 oc) stack pushed, stack: (p a1 c1) \/ (l a1c1 C0) :: (l C4 a1b1) \/ (l b2c2 b1c1) \/ (exists A:dom,(l A A)/\(i C1 A)/\(i C7 A)/\(i bc A)) :: nil stack top tailed: (p a1 c1) (p c1 a1) (i a1 b1c1) false falid, stack: (l a1c1 C0) :: (l C4 a1b1) \/ (l b2c2 b1c1) \/ (exists A:dom,(l A A)/\(i C1 A)/\(i C7 A)/\(i bc A)) :: nil stack popped: (l a1c1 C0) (l C0 a1c1) (l oc a1c1) (l a1c1 oc) (i o a1c1) (i c2 a1c1) (i ac C0) (i ac oc) (i b2 a1c1) valid, stack: (l C4 a1b1) \/ (l b2c2 b1c1) \/ (exists A:dom,(l A A)/\(i C1 A)/\(i C7 A)/\(i bc A)) :: nil stack top tailed: (l C4 a1b1) (l a1b1 C4) (i a1 C4) (i b1 C4) (i ab C4) (i C3 a1b1) (i o a1b1) (i C5 a1b1) stack pushed, stack: (p a1 C5) \/ (l a1b1 a1c1) :: (l b2c2 b1c1) \/ (exists A:dom,(l A A)/\(i C1 A)/\(i C7 A)/\(i bc A)) :: nil stack top tailed: (p a1 C5) (p C5 a1) (i a1 C6) (i a1 b2c2) valid, stack: (l a1b1 a1c1) :: (l b2c2 b1c1) \/ (exists A:dom,(l A A)/\(i C1 A)/\(i C7 A)/\(i bc A)) :: nil stack popped: (l a1b1 a1c1) (l a1c1 a1b1) (l C4 a1c1) (l a1c1 C4) (i b1 a1c1) false falid, stack: (l b2c2 b1c1) \/ (exists A:dom,(l A A)/\(i C1 A)/\(i C7 A)/\(i bc A)) :: nil stack top tailed: (l b2c2 b1c1) (l b1c1 b2c2) false falid, stack: (exists A:dom,(l A A)/\(i C1 A)/\(i C7 A)/\(i bc A)) :: nil stack popped: (l C8 C8)/\(i C1 C8)/\(i C7 C8)/\(i bc C8) pappus(ab, bc, ac) stack pushed, stack: (l a2b2 a1b1) \/ (l b2c2 C8) \/ (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (l a2b2 a1b1) (l a1b1 a2b2) false falid, stack: (l b2c2 C8) \/ (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (l b2c2 C8) (l C8 b2c2) (l C6 C8) (l C8 C6) (i c2 C8) (i b2 C8) (i C5 C8) (i C1 b2c2) (i C1 C6) (i C7 b2c2) (i C7 C6) stack pushed, stack: (p c2 C1) \/ (l b2c2 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c2 C1) (p C1 c2) (i c2 C0) (i c2 C2) (i C1 a2c2) stack pushed, stack: (p c2 ac) \/ (l a2c2 C2) :: (l b2c2 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c2 ac) (p ac c2) (p C1 ac) (p ac C1) (i c2 a1c1) (i C1 a1c1) (i ac b2c2) (i ac oc) (i ac C6) (i ac C8) (i ac C0) stack pushed, stack: (p a1 ac) \/ (l a1c1 C0) :: (l a2c2 C2) :: (l b2c2 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 ac) (p ac a1) (p c2 a1) (p a1 c2) (p C1 a1) (p a1 C1) (i a1 a2c2) (i a1 C2) (i a1 b2c2) valid, stack: (l a1c1 C0) :: (l a2c2 C2) :: (l b2c2 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1c1 C0) (l C0 a1c1) (i c1 C0) (i b2 a1c1) valid, stack: (l a2c2 C2) :: (l b2c2 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2c2 C2) (l C2 a2c2) (i a2 C2) (i C3 a2c2) stack pushed, stack: (p a2 C3) \/ (l a2b2 a2c2) :: (l b2c2 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a2 C3) (p C3 a2) (i a2 C4) (i C3 oa) stack pushed, stack: (p c2 b2) \/ (l b2c2 C0) :: (l a2b2 a2c2) :: (l b2c2 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c2 b2) (p b2 c2) (p C1 b2) (p b2 C1) (i c2 a2b2) false falid, stack: (l b2c2 C0) :: (l a2b2 a2c2) :: (l b2c2 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l b2c2 C0) (l C0 b2c2) (l C6 C0) (l C0 C6) (l C8 C0) (l C0 C8) (i bc C0) (i a1 b2c2) valid, stack: (l a2b2 a2c2) :: (l b2c2 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2b2 a2c2) (l a2c2 a2b2) (l C2 a2b2) (l a2b2 C2) (i b2 a2c2) false falid, stack: (l b2c2 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l b2c2 oc) (l oc b2c2) (l C6 oc) (l oc C6) (l C8 oc) (l oc C8) (i b2 oc) (i o b2c2) (i o C6) (i o C8) (i c1 b2c2) (i c1 C6) (i c1 C8) (i bc oc) (i C5 oc) (i C7 oc) stack pushed, stack: (p c1 C5) \/ (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c1 C5) (p C5 c1) (i c1 C4) (i C5 b1c1) stack pushed, stack: (p c1 bc) \/ (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c1 bc) (p bc c1) (p C5 bc) (p bc C5) (i bc a1c1) (i bc C4) stack pushed, stack: (p b2 o) \/ (l b2c2 ob) :: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p b2 o) (p o b2) (i b2 oa) (i b2 C4) (i o a2b2) (i o C0) stack pushed, stack: (p a2 b2) \/ (l a2b2 oa) :: (l b2c2 ob) :: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a2 b2) (p b2 a2) (p o a2) (p a2 o) (i a2 b2c2) false falid, stack: (l a2b2 oa) :: (l b2c2 ob) :: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2b2 oa) (l oa a2b2) (i a1 a2b2) (i ab oa) (i C3 oa) stack pushed, stack: (p a1 ab) \/ (l a1b1 oa) :: (l b2c2 ob) :: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 ab) (p ab a1) (i ab a1c1) valid, stack: (l a1b1 oa) :: (l b2c2 ob) :: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 oa) (l oa a1b1) (l a2b2 a1b1) (l a1b1 a2b2) false falid, stack: (l b2c2 ob) :: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l b2c2 ob) (l ob b2c2) (l C6 ob) (l ob C6) (l C8 ob) (l ob C8) (l oc ob) (l ob oc) (i c2 ob) (i b1 b2c2) (i b1 C6) (i b1 C8) (i b1 oc) (i c1 ob) (i C5 ob) (i bc ob) (i C1 ob) (i C7 ob) stack pushed, stack: (p b1 C7) \/ (l a1b1 ob) :: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p b1 C7) (p C7 b1) (i b1 C4) (i C7 b1c1) stack pushed, stack: (p c1 b1) \/ (l b1c1 oc) :: (l a1b1 ob) :: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c1 b1) (p b1 c1) (p C5 b1) (p b1 C5) (p bc b1) (p b1 bc) (p C7 c1) (p c1 C7) (p C5 C7) (p C7 C5) (p bc C7) (p C7 bc) (i c1 a1b1) false falid, stack: (l b1c1 oc) :: (l a1b1 ob) :: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l b1c1 oc) (l oc b1c1) (l b2c2 b1c1) (l b1c1 b2c2) false falid, stack: (l a1b1 ob) :: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 ob) (l ob a1b1) (l b2c2 a1b1) (l a1b1 b2c2) (l C6 a1b1) (l a1b1 C6) (l C8 a1b1) (l a1b1 C8) (l oc a1b1) (l a1b1 oc) (i a1 ob) false falid, stack: (l b1c1 oc) :: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l b1c1 oc) (l oc b1c1) (l b2c2 b1c1) (l b1c1 b2c2) false falid, stack: (l a1c1 oc) :: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1c1 oc) (l oc a1c1) (l b2c2 a1c1) (l a1c1 b2c2) (l C6 a1c1) (l a1c1 C6) (l C8 a1c1) (l a1c1 C8) (i a1 oc) (i a1 b2c2) valid, stack: (l a1c1 C2) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (l a1c1 C2) (l C2 a1c1) (i a1 C2) (i c1 C2) (i C1 a1c1) (i C3 a1c1) (i C5 C2) stack pushed, stack: (p a1 C1) \/ (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 C1) (p C1 a1) (i a1 oc) (i a1 C8) (i C1 a1b1) (i C1 oa) stack pushed, stack: (p a1 C7) \/ (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 C7) (p C7 a1) (p C1 C7) (p C7 C1) (i a1 C4) (i C1 C4) (i C7 a1c1) (i C7 oa) (i C7 C0) (i C7 C2) (i C7 oc) stack pushed, stack: (p a1 c1) \/ (l a1c1 oc) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 c1) (p c1 a1) (p C1 c1) (p c1 C1) (p C7 c1) (p c1 C7) (i a1 b1c1) false falid, stack: (l a1c1 oc) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1c1 oc) (l oc a1c1) (l C2 oc) (l oc C2) (i o a1c1) (i o C2) (i c2 a1c1) (i c2 C2) (i ac oc) (i C3 oc) (i C5 oc) stack pushed, stack: (p a1 o) \/ (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 o) (p o a1) (p C1 o) (p o C1) (p C7 o) (p o C7) (i a1 ob) (i C1 ob) (i C7 ob) (i o a1b1) (i o C0) (i o C8) stack pushed, stack: (p a1 b1) \/ (l a1b1 ob) :: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 b1) (p b1 a1) (p C1 b1) (p b1 C1) (p C7 b1) (p b1 C7) (p o b1) (p b1 o) (i a1 b1c1) false falid, stack: (l a1b1 ob) :: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 ob) (l ob a1b1) (i b2 a1b1) (i ab ob) stack pushed, stack: (p a1 b2) \/ (l a1b1 C0) :: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 b2) (p b2 a1) (p C1 b2) (p b2 C1) (p C7 b2) (p b2 C7) (p o b2) (p b2 o) (i a1 a2b2) (i C1 a2b2) (i C7 a2b2) (i o a2b2) (i a1 b2c2) valid, stack: (l a1b1 C0) :: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 C0) (l C0 a1b1) (l ob C0) (l C0 ob) (i b1 C0) (i ab C0) stack pushed, stack: (p b2 ab) \/ (l a2b2 ob) :: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p b2 ab) (p ab b2) (i ab b2c2) (i ab C6) stack pushed, stack: (p a1 C5) \/ (l a1c1 C4) :: (l a2b2 ob) :: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 C5) (p C5 a1) (p C1 C5) (p C5 C1) (p C7 C5) (p C5 C7) (p o C5) (p C5 o) (i a1 C6) (i C1 C6) (i C7 C6) (i o C6) (i a1 b2c2) valid, stack: (l a1c1 C4) :: (l a2b2 ob) :: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1c1 C4) (l C4 a1c1) (l C2 C4) (l C4 C2) (l oc C4) (l C4 oc) (i c1 C4) (i c2 C4) (i ac C4) stack pushed, stack: (p c2 ac) \/ (l a2c2 oc) :: (l a2b2 ob) :: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c2 ac) (p ac c2) (i ac b2c2) valid, stack: (l a2c2 oc) :: (l a2b2 ob) :: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2c2 oc) (l oc a2c2) (l a1c1 a2c2) false falid, stack: (l a2b2 ob) :: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2b2 ob) (l ob a2b2) (l a1b1 a2b2) false falid, stack: (l a1c1 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1c1 oa) (l oa a1c1) (l C2 oa) (l oa C2) (l oc oa) (l oa oc) (i c1 oa) (i a2 a1c1) (i a2 C2) (i a2 oc) (i c2 oa) (i ac oa) (i C3 oa) (i C5 oa) stack pushed, stack: (p a2 C3) \/ (l a2b2 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a2 C3) (p C3 a2) (i a2 C4) (i C3 a2c2) stack pushed, stack: (p a1 C5) \/ (l a1c1 C4) :: (l a2b2 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 C5) (p C5 a1) (p C1 C5) (p C5 C1) (p C7 C5) (p C5 C7) (i a1 C6) (i C1 C6) (i C7 C6) (i a1 b2c2) valid, stack: (l a1c1 C4) :: (l a2b2 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1c1 C4) (l C4 a1c1) (l C2 C4) (l C4 C2) (l oc C4) (l C4 oc) (l oa C4) (l C4 oa) (i c1 C4) (i c2 C4) (i ac C4) stack pushed, stack: (p a2 c2) \/ (l a2c2 oa) :: (l a2b2 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a2 c2) (p c2 a2) (p C3 c2) (p c2 C3) (i a2 b2c2) false falid, stack: (l a2c2 oa) :: (l a2b2 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2c2 oa) (l oa a2c2) (l a1c1 a2c2) false falid, stack: (l a2b2 oa) :: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2b2 oa) (l oa a2b2) (l a1c1 a2b2) (l a2b2 a1c1) (l C2 a2b2) (l a2b2 C2) (l oc a2b2) (l a2b2 oc) (i b2 oa) false falid, stack: (l a1b1 C8) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 C8) (l C8 a1b1) (i b1 C8) (i ab C8) (i bc a1b1) stack pushed, stack: (p b1 bc) \/ (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p b1 bc) (p bc b1) (i b1 b2c2) (i b1 C6) (i bc ob) stack pushed, stack: (p a1 c1) \/ (l a1c1 oc) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 c1) (p c1 a1) (p C1 c1) (p c1 C1) (i a1 b1c1) false falid, stack: (l a1c1 oc) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1c1 oc) (l oc a1c1) (l C2 oc) (l oc C2) (i o a1c1) (i o C2) (i c2 a1c1) (i c2 C2) (i ac oc) (i C3 oc) (i C5 oc) stack pushed, stack: (p a1 o) \/ (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 o) (p o a1) (p C1 o) (p o C1) (i a1 ob) (i C1 ob) (i a1 C4) (i C1 C4) (i o a1b1) (i o C0) (i o C8) stack pushed, stack: (p a1 b1) \/ (l a1b1 ob) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 b1) (p b1 a1) (p C1 b1) (p b1 C1) (p bc a1) (p a1 bc) (p C1 bc) (p bc C1) (p o b1) (p b1 o) (p bc o) (p o bc) (i a1 b1c1) false falid, stack: (l a1b1 ob) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 ob) (l ob a1b1) (l C8 ob) (l ob C8) (i b2 a1b1) (i b2 C8) (i ab ob) (i C7 ob) stack pushed, stack: (p a1 b2) \/ (l a1b1 C0) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 b2) (p b2 a1) (p C1 b2) (p b2 C1) (p o b2) (p b2 o) (i a1 a2b2) (i C1 a2b2) (i o a2b2) (i a1 b2c2) valid, stack: (l a1b1 C0) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 C0) (l C0 a1b1) (l C8 C0) (l C0 C8) (l ob C0) (l C0 ob) (i b1 C0) (i bc C0) (i ab C0) (i C7 C0) stack pushed, stack: (p a1 C7) \/ (l a1b1 C4) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 C7) (p C7 a1) (p C1 C7) (p C7 C1) (p o C7) (p C7 o) (i C7 a1c1) (i C7 oa) (i C7 C2) (i C7 oc) stack pushed, stack: (p b1 b2) \/ (l a1b1 b2c2) :: (l a1b1 C4) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p b1 b2) (p b2 b1) false falid, stack: (l a1b1 b2c2) :: (l a1b1 C4) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 b2c2) (l b2c2 a1b1) (l C6 a1b1) (l a1b1 C6) (l C8 b2c2) (l b2c2 C8) (l C6 C8) (l C8 C6) (l ob b2c2) (l b2c2 ob) (l C6 ob) (l ob C6) (l C0 b2c2) (l b2c2 C0) (l C6 C0) (l C0 C6) (i a1 b2c2) valid, stack: (l a1b1 C4) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 C4) (l C4 a1b1) (l C8 C4) (l C4 C8) (l ob C4) (l C4 ob) (l C0 C4) (l C4 C0) (i b1 C4) (i bc C4) (i b2 C4) (i ab C4) (i C3 a1b1) (i C3 C8) (i C3 ob) (i C3 C0) (i C5 a1b1) (i C5 C8) (i C5 ob) (i C5 C0) stack pushed, stack: (p a1 C3) \/ (l a1b1 a1c1) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 C3) (p C3 a1) (p C1 C3) (p C3 C1) (p o C3) (p C3 o) (i a1 a2b2) (i C1 a2b2) (i o a2b2) (i C3 oa) stack pushed, stack: (p a1 C5) \/ (l a1b1 a1c1) :: (l a1b1 a1c1) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 C5) (p C5 a1) (p C1 C5) (p C5 C1) (p o C5) (p C5 o) (p C3 C5) (p C5 C3) (i a1 C6) (i C1 C6) (i o C6) (i C3 C6) (i a1 b2c2) valid, stack: (l a1b1 a1c1) :: (l a1b1 a1c1) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 a1c1) (l a1c1 a1b1) (l C2 a1b1) (l a1b1 C2) (l C8 a1c1) (l a1c1 C8) (l C2 C8) (l C8 C2) (l oc a1b1) (l a1b1 oc) (l C8 oc) (l oc C8) (l ob a1c1) (l a1c1 ob) (l C2 ob) (l ob C2) (l oc ob) (l ob oc) (l C0 a1c1) (l a1c1 C0) (l C2 C0) (l C0 C2) (l oc C0) (l C0 oc) (l C4 a1c1) (l a1c1 C4) (l C2 C4) (l C4 C2) (l oc C4) (l C4 oc) (i b1 a1c1) false falid, stack: (l a1b1 a1c1) :: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 a1c1) (l a1c1 a1b1) (l C2 a1b1) (l a1b1 C2) (l C8 a1c1) (l a1c1 C8) (l C2 C8) (l C8 C2) (l oc a1b1) (l a1b1 oc) (l C8 oc) (l oc C8) (l ob a1c1) (l a1c1 ob) (l C2 ob) (l ob C2) (l oc ob) (l ob oc) (l C0 a1c1) (l a1c1 C0) (l C2 C0) (l C0 C2) (l oc C0) (l C0 oc) (l C4 a1c1) (l a1c1 C4) (l C2 C4) (l C4 C2) (l oc C4) (l C4 oc) (i b1 a1c1) false falid, stack: (l a1c1 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1c1 oa) (l oa a1c1) (l C2 oa) (l oa C2) (l oc oa) (l oa oc) (i c1 oa) (i a2 a1c1) (i a2 C2) (i a2 oc) (i c2 oa) (i ac oa) (i C3 oa) (i C5 oa) stack pushed, stack: (p a2 C3) \/ (l a2b2 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a2 C3) (p C3 a2) (i a2 C4) (i C3 a2c2) stack pushed, stack: (p a2 c2) \/ (l a2c2 oa) :: (l a2b2 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a2 c2) (p c2 a2) (p C3 c2) (p c2 C3) (i a2 b2c2) false falid, stack: (l a2c2 oa) :: (l a2b2 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2c2 oa) (l oa a2c2) (l a1c1 a2c2) false falid, stack: (l a2b2 oa) :: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2b2 oa) (l oa a2b2) (l a1c1 a2b2) (l a2b2 a1c1) (l C2 a2b2) (l a2b2 C2) (l oc a2b2) (l a2b2 oc) (i b2 oa) false falid, stack: (l a1b1 b1c1) :: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1b1 b1c1) (l b1c1 a1b1) (l C8 b1c1) (l b1c1 C8) (i a1 b1c1) false falid, stack: (l a1c1 C0) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a1c1 C0) (l C0 a1c1) (l C2 C0) (l C0 C2) (i c1 C0) (i ac C0) (i b2 a1c1) valid, stack: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l C9 C9)/\(i ab C9)/\(i bc C9)/\(i ac C9) valid, stack: nil