(i a1 b2c2)/\(i b1 a2c2)/\(i c1 a2b2) (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 c1 c1) (p a2 a2) (p b2 b2) (p c2 c2) (p o o) (p bc bc) (p ac ac) (p ab ab) (l b2c2 b2c2) (l a2c2 a2c2) (l a2b2 a2b2) (l a1b1 a1b1) (l a1c1 a1c1) (l b1c1 b1c1) (l oa oa) (l ob ob) (l oc oc) line(ac, b2) (i ac C0)/\(i b2 C0) (l C0 C0) point(par(0), oa) (i C1 C0)/\(i C1 oa) (p C1 C1) point(par(0), oc) (i C2 C0)/\(i C2 oc) (p C2 C2) pappus(c2, ab, par(1)) stack pushed, stack: (l oc a2c2) \/ (l a2b2 a1b1) \/ (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (l oc a2c2) (l a2c2 oc) (i b1 oc) (i a2 oc) (i o a2c2) (i c1 a2c2) (i ac oc) (i C2 a2c2) stack pushed, stack: (p b1 c1) \/ (l a2c2 b1c1) :: (l a2b2 a1b1) \/ (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p b1 c1) (p c1 b1) (i b1 a2b2) (i b1 a1c1) false falid, stack: (l a2c2 b1c1) :: (l a2b2 a1b1) \/ (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l a2c2 b1c1) (l b1c1 a2c2) (l oc b1c1) (l b1c1 oc) (i a2 b1c1) (i c2 b1c1) (i o b1c1) (i bc a2c2) (i bc oc) (i ac b1c1) (i C2 b1c1) stack pushed, stack: (p b1 o) \/ (l a2c2 ob) :: (l a2b2 a1b1) \/ (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p b1 o) (p o b1) (i b1 oa) (i o a1b1) stack pushed, stack: (p b1 a2) \/ (l a2c2 oa) :: (l a2c2 ob) :: (l a2b2 a1b1) \/ (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p b1 a2) (p a2 b1) (p o a2) (p a2 o) (i b1 a2b2) (i o a2b2) (i a2 a1b1) (i a2 ob) stack pushed, stack: (p b1 c1) \/ (l a2c2 a2b2) :: (l a2c2 oa) :: (l a2c2 ob) :: (l a2b2 a1b1) \/ (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p b1 c1) (p c1 b1) (p o c1) (p c1 o) (p a2 c1) (p c1 a2) (i b1 a1c1) false falid, stack: (l a2c2 a2b2) :: (l a2c2 oa) :: (l a2c2 ob) :: (l a2b2 a1b1) \/ (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l a2c2 a2b2) (l a2b2 a2c2) (l oc a2b2) (l a2b2 oc) (l b1c1 a2b2) (l a2b2 b1c1) (i b2 a2c2) false falid, stack: (l a2c2 oa) :: (l a2c2 ob) :: (l a2b2 a1b1) \/ (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l a2c2 oa) (l oa a2c2) (l oc oa) (l oa oc) (l b1c1 oa) (l oa b1c1) (i c2 oa) (i c1 oa) false falid, stack: (l a2c2 ob) :: (l a2b2 a1b1) \/ (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l a2c2 ob) (l ob a2c2) (l oc ob) (l ob oc) (l b1c1 ob) (l ob b1c1) (i a2 ob) (i c2 ob) false falid, stack: (l a2b2 a1b1) \/ (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (l a2b2 a1b1) (l a1b1 a2b2) false falid, stack: (l C0 oa) \/ (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (l C0 oa) (l oa C0) (i o C0) (i a1 C0) (i a2 C0) (i ac oa) (i b2 oa) (i C2 oa) stack pushed, stack: (p a1 b2) \/ (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p a1 b2) (p b2 a1) (i a1 a2b2) (i a1 ob) (i b2 a1b1) (i b2 a1c1) stack pushed, stack: (p c1 b2) \/ (l a2b2 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p c1 b2) (p b2 c1) (p a1 c1) (p c1 a1) (i c1 b2c2) (i c1 ob) false falid, stack: (l a2b2 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l a2b2 a1c1) (l a1c1 a2b2) (i a2 a1c1) (i ac a2b2) (i ab a1c1) stack pushed, stack: (p a1 ab) \/ (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p a1 ab) (p ab a1) (p b2 ab) (p ab b2) (i ab b2c2) (i ab oa) (i ab C0) (i ab ob) stack pushed, stack: (p a1 b1) \/ (l a1b1 ob) :: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p a1 b1) (p b1 a1) (p b2 b1) false falid, stack: (l a1b1 ob) :: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l a1b1 ob) (l ob a1b1) (i o a1b1) stack pushed, stack: (p a1 o) \/ (l a1b1 oa) :: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p a1 o) (p o a1) (p b2 o) (p o b2) (p ab o) (p o ab) (i a1 oc) (i b2 oc) (i ab oc) (i o b2c2) (i o a1c1) (i o a2b2) stack pushed, stack: (p a1 c2) \/ (l b2c2 oc) :: (l a1b1 oa) :: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p a1 c2) (p c2 a1) (p b2 c2) (p c2 b2) (p ab c2) (p c2 ab) (p o c2) (p c2 o) (i a1 a2c2) (i b2 a2c2) false falid, stack: (l b2c2 oc) :: (l a1b1 oa) :: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l b2c2 oc) (l oc b2c2) (i c1 b2c2) (i bc oc) (i C2 b2c2) stack pushed, stack: (p a1 c1) \/ (l b2c2 a1c1) :: (l a1b1 oa) :: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p a1 c1) (p c1 a1) (p b2 c1) (p c1 b2) (p ab c1) (p c1 ab) (p o c1) (p c1 o) (i a1 b1c1) false falid, stack: (l b2c2 a1c1) :: (l a1b1 oa) :: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l b2c2 a1c1) (l a1c1 b2c2) (l a2b2 b2c2) (l b2c2 a2b2) (l oc a1c1) (l a1c1 oc) (l a2b2 oc) (l oc a2b2) (i a2 b2c2) false falid, stack: (l a1b1 oa) :: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l a1b1 oa) (l oa a1b1) (l C0 a1b1) (l a1b1 C0) (l ob oa) (l oa ob) (l C0 ob) (l ob C0) (i b1 oa) (i b1 C0) (i a2 a1b1) (i a2 ob) (i ac a1b1) (i ac ob) (i C1 a1b1) (i C1 ob) (i C2 a1b1) (i C2 ob) stack pushed, stack: (p b1 a2) \/ (l a2c2 a1b1) :: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack top tailed: (p b1 a2) (p a2 b1) (i b1 a2b2) false falid, stack: (l a2c2 a1b1) :: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l a2c2 a1b1) (l a1b1 a2c2) (l ob a2c2) (l a2c2 ob) (l oa a2c2) (l a2c2 oa) (l C0 a2c2) (l a2c2 C0) (i a1 a2c2) (i b2 a2c2) false falid, stack: (l a1b1 a1c1) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l a1b1 a1c1) (l a1c1 a1b1) (l a2b2 a1b1) (l a1b1 a2b2) false falid, stack: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l b2c2 oa) (l oa b2c2) (l C0 b2c2) (l b2c2 C0) (i c2 oa) false falid, stack: (exists A:dom,(l A A)/\(i c2 A)/\(i ab A)/\(i C1 A)) :: nil stack popped: (l C3 C3)/\(i c2 C3)/\(i ab C3)/\(i C1 C3) pappus(a2, bc, par(2)) stack pushed, stack: (l oa a2c2) \/ (l b2c2 b1c1) \/ (l C0 oc) \/ (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (l oa a2c2) (l a2c2 oa) (i b1 oa) (i c2 oa) (i o a2c2) (i a1 a2c2) (i ac oa) (i C1 a2c2) stack pushed, stack: (p a1 c2) \/ (l b2c2 oa) :: (l b2c2 b1c1) \/ (l C0 oc) \/ (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (p a1 c2) (p c2 a1) (i a1 oc) (i a1 C3) (i c2 a1b1) (i c2 a1c1) stack pushed, stack: (p b1 c2) \/ (l a2c2 a1b1) :: (l b2c2 oa) :: (l b2c2 b1c1) \/ (l C0 oc) \/ (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (p b1 c2) (p c2 b1) (p a1 b1) (p b1 a1) (i b1 b2c2) (i b1 oc) false falid, stack: (l a2c2 a1b1) :: (l b2c2 oa) :: (l b2c2 b1c1) \/ (l C0 oc) \/ (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack popped: (l a2c2 a1b1) (l a1b1 a2c2) (l oa a1b1) (l a1b1 oa) (i a2 a1b1) (i o a1b1) (i ac a1b1) (i ab a2c2) (i ab oa) (i C1 a1b1) stack pushed, stack: (p b1 o) \/ (l a2c2 ob) :: (l b2c2 oa) :: (l b2c2 b1c1) \/ (l C0 oc) \/ (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (p b1 o) (p o b1) (i b1 oc) false falid, stack: (l a2c2 ob) :: (l b2c2 oa) :: (l b2c2 b1c1) \/ (l C0 oc) \/ (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack popped: (l a2c2 ob) (l ob a2c2) (l oa ob) (l ob oa) (l a1b1 ob) (l ob a1b1) (i a1 ob) (i c2 ob) (i a2 ob) false falid, stack: (l b2c2 oa) :: (l b2c2 b1c1) \/ (l C0 oc) \/ (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack popped: (l b2c2 oa) (l oa b2c2) (l a2c2 b2c2) (l b2c2 a2c2) (i b1 b2c2) (i a2 b2c2) false falid, stack: (l b2c2 b1c1) \/ (l C0 oc) \/ (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (l b2c2 b1c1) (l b1c1 b2c2) false falid, stack: (l C0 oc) \/ (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (l C0 oc) (l oc C0) (i o C0) (i c1 C0) (i c2 C0) (i ac oc) (i b2 oc) (i C1 oc) stack pushed, stack: (p c1 b2) \/ (l a2b2 oc) :: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (p c1 b2) (p b2 c1) (i c1 b2c2) (i c1 ob) (i b2 a1c1) (i b2 b1c1) stack pushed, stack: (p a1 b2) \/ (l b2c2 a1c1) :: (l a2b2 oc) :: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (p a1 b2) (p b2 a1) (p c1 a1) (p a1 c1) (i a1 a2b2) (i a1 ob) false falid, stack: (l b2c2 a1c1) :: (l a2b2 oc) :: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack popped: (l b2c2 a1c1) (l a1c1 b2c2) (i c2 a1c1) (i bc a1c1) (i ac b2c2) stack pushed, stack: (p c1 bc) \/ (l a1c1 b1c1) :: (l a2b2 oc) :: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (p c1 bc) (p bc c1) (p b2 bc) (p bc b2) (i bc a2b2) (i bc oc) (i bc C0) (i bc ob) stack pushed, stack: (p c1 ac) \/ (l a1c1 oc) :: (l a1c1 b1c1) :: (l a2b2 oc) :: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (p c1 ac) (p ac c1) (p b2 ac) (p ac b2) (p bc ac) (p ac bc) (i c1 a2c2) (i b2 a2c2) false falid, stack: (l a1c1 oc) :: (l a1c1 b1c1) :: (l a2b2 oc) :: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack popped: (l a1c1 oc) (l oc a1c1) (l C0 a1c1) (l a1c1 C0) (l b2c2 oc) (l oc b2c2) (l C0 b2c2) (l b2c2 C0) (i a1 oc) (i a1 C0) (i o a1c1) (i o b2c2) (i C1 a1c1) (i C1 b2c2) (i C2 a1c1) (i C2 b2c2) stack pushed, stack: (p a1 o) \/ (l b2c2 oa) :: (l a1c1 b1c1) :: (l a2b2 oc) :: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack top tailed: (p a1 o) (p o a1) (i a1 ob) false falid, stack: (l b2c2 oa) :: (l a1c1 b1c1) :: (l a2b2 oc) :: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack popped: (l b2c2 oa) (l oa b2c2) (l a1c1 oa) (l oa a1c1) (l oc oa) (l oa oc) (l C0 oa) (l oa C0) (i c1 oa) (i b2 oa) (i bc oa) (i c2 oa) false falid, stack: (l a1c1 b1c1) :: (l a2b2 oc) :: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack popped: (l a1c1 b1c1) (l b1c1 a1c1) (l b2c2 b1c1) (l b1c1 b2c2) false falid, stack: (l a2b2 oc) :: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack popped: (l a2b2 oc) (l oc a2b2) (l C0 a2b2) (l a2b2 C0) (i a2 oc) false falid, stack: (exists A:dom,(l A A)/\(i a2 A)/\(i bc A)/\(i C2 A)) :: nil stack popped: (l C4 C4)/\(i a2 C4)/\(i bc C4)/\(i C2 C4) pappus(ab, bc, ac) stack pushed, stack: (l a2b2 C3) \/ (l C4 b2c2) \/ (l C0 a1c1) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (l a2b2 C3) (l C3 a2b2) (i c1 C3) (i a2 C3) (i b2 C3) false falid, stack: (l C4 b2c2) \/ (l C0 a1c1) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (l C4 b2c2) (l b2c2 C4) (i a1 C4) (i c2 C4) (i b2 C4) false falid, stack: (l C0 a1c1) \/ (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (l C0 a1c1) (l a1c1 C0) (i a1 C0) (i c1 C0) (i b2 a1c1) (i C1 a1c1) (i C2 a1c1) stack pushed, stack: (p a1 b2) \/ (l b2c2 a1c1) :: (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) (i a1 a2b2) (i a1 ob) (i b2 a1b1) (i b2 oa) stack pushed, stack: (p c1 b2) \/ (l a2b2 a1c1) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c1 b2) (p b2 c1) (p a1 c1) (p c1 a1) (i c1 b2c2) (i c1 ob) false falid, stack: (l a2b2 a1c1) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2b2 a1c1) (l a1c1 a2b2) (l C0 a2b2) (l a2b2 C0) (i a2 a1c1) (i a2 C0) (i ac a2b2) (i ab a1c1) (i ab C0) (i C1 a2b2) (i C2 a2b2) stack pushed, stack: (p c1 C2) \/ (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c1 C2) (p C2 c1) (i c1 C4) (i C2 b1c1) stack pushed, stack: (p c1 a2) \/ (l a2b2 C4) :: (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c1 a2) (p a2 c1) (p C2 a2) (p a2 C2) (i c1 a2c2) (i C2 a2c2) (i c1 oa) (i C2 oa) (i a2 b1c1) (i a2 oc) stack pushed, stack: (p b1 a2) \/ (l a2c2 b1c1) :: (l a2b2 C4) :: (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p b1 a2) (p a2 b1) (p c1 b1) (p b1 c1) (p C2 b1) (p b1 C2) (i b1 a2b2) false falid, stack: (l a2c2 b1c1) :: (l a2b2 C4) :: (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2c2 b1c1) (l b1c1 a2c2) (i c2 b1c1) (i bc a2c2) (i ac b1c1) stack pushed, stack: (p c1 ac) \/ (l a2b2 b1c1) :: (l a2b2 C4) :: (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c1 ac) (p ac c1) (p C2 ac) (p ac C2) (p a2 ac) (p ac a2) (i ac oc) (i ac C4) (i ac oa) stack pushed, stack: (p c1 b2) \/ (l a2b2 oa) :: (l a2b2 b1c1) :: (l a2b2 C4) :: (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c1 b2) (p b2 c1) (p a1 c1) (p c1 a1) (p C2 b2) (p b2 C2) (p a1 C2) (p C2 a1) (p a2 b2) (p b2 a2) (p a1 a2) (p a2 a1) false falid, stack: (l a2b2 oa) :: (l a2b2 b1c1) :: (l a2b2 C4) :: (l a2b2 oc) :: (l b2c2 a1c1) :: (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 oa) (l oa a1c1) (l C0 oa) (l oa C0) (i o a2b2) (i o a1c1) (i o C0) (i ab oa) stack pushed, stack: (p c1 o) \/ (l a2b2 oc) :: (l a2b2 b1c1) :: (l a2b2 C4) :: (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p c1 o) (p o c1) (p C2 o) (p o C2) (p a2 o) (p o a2) (p ac o) (p o ac) (i c1 ob) false falid, stack: (l a2b2 oc) :: (l a2b2 b1c1) :: (l a2b2 C4) :: (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2b2 oc) (l oc a2b2) (l a1c1 oc) (l oc a1c1) (l C0 oc) (l oc C0) (l oa oc) (l oc oa) (i b2 oc) false falid, stack: (l a2b2 b1c1) :: (l a2b2 C4) :: (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2b2 b1c1) (l b1c1 a2b2) (l a1c1 b1c1) (l b1c1 a1c1) (l C0 b1c1) (l b1c1 C0) (l a2c2 a2b2) (l a2b2 a2c2) (l a1c1 a2c2) false falid, stack: (l a2b2 C4) :: (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2b2 C4) (l C4 a2b2) (l a1c1 C4) (l C4 a1c1) (l C0 C4) (l C4 C0) (i b2 C4) (i a1 C4) (i ac C4) (i ab C4) valid, stack: (l a2b2 oc) :: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l a2b2 oc) (l oc a2b2) (l a1c1 oc) (l oc a1c1) (l C0 oc) (l oc C0) (i a2 oc) (i b2 oc) false falid, stack: (l b2c2 a1c1) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l b2c2 a1c1) (l a1c1 b2c2) (l C0 b2c2) (l b2c2 C0) (i c1 b2c2) (i c2 a1c1) (i c2 C0) (i bc a1c1) (i bc C0) (i ac b2c2) (i C1 b2c2) (i C2 b2c2) stack pushed, stack: (p a1 C1) \/ (l b2c2 oa) :: (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 C3) (i C1 a1b1) stack pushed, stack: (p a1 c2) \/ (l b2c2 C3) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack top tailed: (p a1 c2) (p c2 a1) (p C1 c2) (p c2 C1) (i a1 a2c2) (i C1 a2c2) (i a1 oc) (i C1 oc) (i c2 a1b1) (i c2 oa) stack pushed, stack: (p a1 ac) \/ (l b2c2 a2c2) :: (l b2c2 C3) :: (l b2c2 oa) :: (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 C1 ac) (p ac C1) (p c2 ac) (p ac c2) (i ac a1b1) (i ac oa) (i ac C3) (i ac oc) stack pushed, stack: (p a1 c1) \/ (l b2c2 oc) :: (l b2c2 a2c2) :: (l b2c2 C3) :: (l b2c2 oa) :: (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 c2 c1) false falid, stack: (l b2c2 oc) :: (l b2c2 a2c2) :: (l b2c2 C3) :: (l b2c2 oa) :: (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 a1c1 oc) (l oc a1c1) (l C0 oc) (l oc C0) (i b2 oc) (i o b2c2) (i o a1c1) (i o C0) (i bc oc) stack pushed, stack: (p a1 o) \/ (l b2c2 oa) :: (l b2c2 a2c2) :: (l b2c2 C3) :: (l b2c2 oa) :: (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 c2 o) (p o c2) (p ac o) (p o ac) (i a1 ob) (i C1 ob) (i c2 ob) (i ac ob) (i o a1b1) (i o C3) (i o a2c2) stack pushed, stack: (p a1 b2) \/ (l b2c2 ob) :: (l b2c2 oa) :: (l b2c2 a2c2) :: (l b2c2 C3) :: (l b2c2 oa) :: (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 c2 b2) (p b2 c2) (p ac b2) (p b2 ac) (p o b2) (p b2 o) (i a1 a2b2) (i C1 a2b2) (i c2 a2b2) false falid, stack: (l b2c2 ob) :: (l b2c2 oa) :: (l b2c2 a2c2) :: (l b2c2 C3) :: (l b2c2 oa) :: (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 a1c1 ob) (l ob a1c1) (l C0 ob) (l ob C0) (l oc ob) (l ob oc) (i c1 ob) false falid, stack: (l b2c2 oa) :: (l b2c2 a2c2) :: (l b2c2 C3) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l b2c2 oa) (l oa b2c2) (l a1c1 oa) (l oa a1c1) (l C0 oa) (l oa C0) (l oc oa) (l oa oc) (i c1 oa) (i b2 oa) false falid, stack: (l b2c2 a2c2) :: (l b2c2 C3) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l b2c2 a2c2) (l a2c2 b2c2) (l a1c1 a2c2) false falid, stack: (l b2c2 C3) :: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l b2c2 C3) (l C3 b2c2) (l a1c1 C3) (l C3 a1c1) (l C0 C3) (l C3 C0) (i c1 C3) (i b2 C3) (i bc C3) (i ac C3) valid, stack: (l b2c2 oa) :: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l b2c2 oa) (l oa b2c2) (l a1c1 oa) (l oa a1c1) (l C0 oa) (l oa C0) (i c1 oa) (i c2 oa) (i b2 oa) false falid, stack: (exists A:dom,(l A A)/\(i ab A)/\(i bc A)/\(i ac A)) :: nil stack popped: (l C5 C5)/\(i ab C5)/\(i bc C5)/\(i ac C5) valid, stack: nil