{-| Module  : FiniteCategories
Description : Examples of 'Sketch'es.
Copyright   : Guillaume Sabbagh 2023
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Examples of 'Sketch'es.
-}
module Math.FiniteCategories.FinSketch.Examples
(
    exampleSketchMagma,
    exampleSketchUnitalMagma,
    exampleSketchMorphismMagmaToUnitalMagma,
    exampleSketchGraph,
    exampleSketchPointedSet,
    exampleSketchAtomic,
    exampleDiagramOfSketches,
    exampleSketchLoop,
    exampleDiagramOfSketches2,
    exampleLantern,
    exampleSpotlight,
    exampleCrescentMoon,
    exampleColantern,
    exampleCospotlight,
    exampleCocrescentMoon,
    exampleNoCrescentMoon,
    exampleSketchToRealize,
    exampleSketchSAT1,
    exampleSketchSAT2,
    exampleSketchSAT3,
    exampleSketchSAT4,
    exampleSketchSAT5,
    exampleSketchSAT6, 
 
)
where
    import qualified Data.WeakSet as Set
    import Data.WeakSet.Safe
    import Data.WeakMap.Safe
    import Data.Simplifiable
    
    import Math.FiniteCategory
    import Math.Categories
    import Math.CocompleteCategory
    import Math.FiniteCategories
    import Math.FiniteCategories.FunctorCategory
    import Math.Categories.FinCat
    import Math.Categories.FinSketch
    
    import Data.Text (pack , Text)
    
    import System.Random
    import Numeric.Natural
    
    -- | The 'Sketch' of the magma structure.
    exampleSketchMagma :: Sketch Text Text
    exampleSketchMagma = result
        where
            Right cg = readCGString "ExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\n"
            Right indx = readCGString "A\nB\n"
            Right base = readCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\n</TGT>\nA => E\nB => E\n"
            Just c = cone (pack "ExE") (unsafeNaturalTransformation (constantDiagram indx cg (pack "ExE")) base (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p_1")), (pack "B", unsafeGetMorphismFromLabel cg (pack "p_2"))]))
            Right result = sketchText cg (set [c]) (set []) (set [])
            
    -- | The 'Sketch' of the unital magma structure. A unital magma is a magma with an identity.
    exampleSketchUnitalMagma :: Sketch Text Text
    exampleSketchUnitalMagma = simplify result
        where
            cg = unsafeReadCGString "ExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\nE -(e,_)-> ExE -p_1-> E = E -T-> 1 -e-> E\nE -(e,_)-> ExE -+-> E = <ID>\nE -(_,e)-> ExE -p_2-> E = E -T-> 1 -e-> E\nE -(_,e)-> ExE -+-> E = <ID>\n"
            indx1 = unsafeReadCGString "A\nB\n"
            base1 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\nE -(e,_)-> ExE -p_1-> E = E -T-> 1 -e-> E\nE -(e,_)-> ExE -+-> E = <ID>\nE -(_,e)-> ExE -p_2-> E = E -T-> 1 -e-> E\nE -(_,e)-> ExE -+-> E = <ID>\n</TGT>\nA => E\nB => E\n"
            c1 = unsafeCone (pack "ExE") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "ExE")) base1 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p_1")), (pack "B", unsafeGetMorphismFromLabel cg (pack "p_2"))]))
            indx2 = unsafeReadCGString ""
            base2 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\nExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\nE -(e,_)-> ExE -p_1-> E = E -T-> 1 -e-> E\nE -(e,_)-> ExE -+-> E = <ID>\nE -(_,e)-> ExE -p_2-> E = E -T-> 1 -e-> E\nE -(_,e)-> ExE -+-> E = <ID>\n</TGT>"
            c2 = unsafeCone (pack "1") (unsafeNaturalTransformation base2 base2 (weakMap []))
            result = unsafeSketch cg (set [c1,c2]) (set []) (set [])
            
    -- | The inclusion sketch morphism from the sketch of magmas to the sketch of unital magmas.
    exampleSketchMorphismMagmaToUnitalMagma :: SketchMorphism Text Text
    exampleSketchMorphismMagmaToUnitalMagma = simplify result
        where
            f = unsafeReadCGDString "<SRC>\nExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\n</SRC>\n<TGT>\nExE -p_1-> E\nExE -p_2-> E\nExE -+-> E\nE -(e,_)-> ExE -p_1-> E = E -T-> 1 -e-> E\nE -(e,_)-> ExE -+-> E = <ID>\nE -(_,e)-> ExE -p_2-> E = E -T-> 1 -e-> E\nE -(_,e)-> ExE -+-> E = <ID>\n</TGT>\nExE -p_1-> E => ExE -p_1-> E\nExE -p_2-> E => ExE -p_2-> E\nExE -+-> E => ExE -+-> E\n"
            Right result = sketchMorphism exampleSketchMagma exampleSketchUnitalMagma f
            
    -- | The sketch of graphs.
    exampleSketchGraph :: Sketch Text Text
    exampleSketchGraph = simplify result
        where
            cg = unsafeReadCGString "E -s-> V\nE -t-> V\n"
            Right result = sketchText cg (set []) (set []) (set [])
            
    -- | The sketch of pointed sets.
    exampleSketchPointedSet :: Sketch Text Text
    exampleSketchPointedSet = simplify result
        where
            cg = unsafeReadCGString "1 -p-> E\n"
            indx1 = unsafeReadCGString ""
            base1 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\n1 -p-> E\n</TGT>\n"
            c1 = unsafeCone (pack "1") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "1")) base1 (weakMap []))
            Right result = sketchText cg (set [c1]) (set []) (set [])
   
    -- |  A sketch with just one object and no (co)cone.     
    exampleSketchAtomic :: Sketch Text Text
    exampleSketchAtomic = simplify result
        where
            cg = unsafeReadCGString "E\n"
            Right result = sketchText cg (set []) (set []) (set [])
            
    -- | A diagram selecting 'exampleSketchAtomic', 'exampleSketchPointedSet' and 'exampleSketchGraph' so that its colimit is the sketch of graphs with a distinguished edge.
    exampleDiagramOfSketches :: Diagram Hat HatAr HatOb (FinSketch Text Text) (SketchMorphism Text Text) (Sketch Text Text)
    exampleDiagramOfSketches = simplify result
        where
            Right f = readCGDString "<SRC>\nE\n</SRC>\n<TGT>\n1 -p-> E\n</TGT>\nE => E\n"
            Right sm1 = sketchMorphism exampleSketchAtomic exampleSketchPointedSet f
            Right g = readCGDString "<SRC>\nE\n</SRC>\n<TGT>\nE -s-> V\nE -t-> V\n</TGT>\nE => E\n"
            Right sm2 = sketchMorphism exampleSketchAtomic exampleSketchGraph g
            result = completeDiagram Diagram{src = Hat, tgt = FinSketch, omap = weakMap [], mmap = weakMap [(HatF,sm1), (HatG, sm2)]}
    
    
    -- | A sketch with a single object and a loop. This sketch is infinite because of the loop.
    exampleSketchLoop :: Sketch Text Text
    exampleSketchLoop = simplify result
        where
            cg = unsafeReadCGString "N -s-> N\n"
            result = unsafeSketch cg (set []) (set []) (set [])
            
    -- | A diagram selecting 'exampleSketchAtomic', 'exampleSketchPointedSet' and 'exampleSketchLoop' so that its colimit is the sketch of discrete systems.
    exampleDiagramOfSketches2 :: Diagram Hat HatAr HatOb (FinSketch Text Text) (SketchMorphism Text Text) (Sketch Text Text)
    exampleDiagramOfSketches2 = simplify result
        where
            Right f = readCGDString "<SRC>\nE\n</SRC>\n<TGT>\n1 -p-> E\n</TGT>\nE => E\n"
            Right sm1 = sketchMorphism exampleSketchAtomic exampleSketchPointedSet f
            g = completeDiagram Diagram{src = underlyingCategory exampleSketchAtomic, tgt = underlyingCategory exampleSketchLoop, omap = weakMap [(pack "E",pack "N")],mmap = weakMap []}
            Right sm2 = sketchMorphism exampleSketchAtomic exampleSketchLoop g
            result = completeDiagram Diagram{src = Hat, tgt = FinSketch, omap = weakMap [(HatA, source sm1),(HatB, target sm1),(HatC, target sm2)], mmap = weakMap [(HatF,sm1), (HatG, sm2)]}
            
            
    -- | An example of 'Sketch' containing a 'Lantern'.        
    exampleLantern :: Sketch Text Text
    exampleLantern = simplify result
        where
            cg = unsafeReadCGString "C -f-> A x B -p1-> A = C -g-> A x B -p1-> A\nC -f-> A x B -p2-> B = C -g-> A x B -p2-> B\n"
            indx1 = unsafeReadCGString "A\nB\n"
            base1 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nC -f-> A x B -p1-> A = C -g-> A x B -p1-> A\nC -f-> A x B -p2-> B = C -g-> A x B -p2-> B\n</TGT>\nA => A\nB => B\n"
            c1 = unsafeCone (pack "A x B") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "A x B")) base1 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")), (pack "B", unsafeGetMorphismFromLabel cg (pack "p2"))]))
            result = unsafeSketch cg (set [c1]) (set []) (set [])
    
    -- | An example of 'Sketch' containing a 'Spotlight'.     
    exampleSpotlight :: Sketch Text Text
    exampleSpotlight = simplify result
        where
            cg = unsafeReadCGString "A -f-> B\nA -g-> B\n"
            indx1 = unsafeReadCGString "A\nB\n"
            base1 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nA -f-> B\nA -g-> B\n</TGT>\nA => B\nB => B\n"
            c1 = unsafeCone (pack "A") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "A")) base1 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "f")), (pack "B", unsafeGetMorphismFromLabel cg (pack "f"))]))
            result = unsafeSketch cg (set [c1]) (set []) (set [])
            
    -- | An example of 'Sketch' containing a 'CrescentMoon'. 
    exampleCrescentMoon :: Sketch Text Text
    exampleCrescentMoon = simplify result
        where
            cg = unsafeReadCGString "A -f-> B\nA -g-> C\nX -h-> B\nX -i-> C\nX -j-> C\n"
            indx1 = unsafeReadCGString "A\nB\n"
            base1 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nA -f-> B\nA -g-> C\nX -h-> B\nX -i-> C\nX -j-> C\n</TGT>\nA => B\nB => C\n"
            c1 = unsafeCone (pack "A") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "A")) base1 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "f")), (pack "B", unsafeGetMorphismFromLabel cg (pack "g"))]))
            indx2 = unsafeReadCGString "*\n"
            base2 = unsafeReadCGDString "<SRC>\n*\n</SRC>\n<TGT>\nA -f-> B\nA -g-> C\nX -h-> B\nX -i-> C\nX -j-> C\n</TGT>\n* => B\n"
            c2 = unsafeCone (pack "A") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "A")) base2 (weakMap [(pack "*", unsafeGetMorphismFromLabel cg (pack "f"))]))
            result = unsafeSketch cg (set [c1,c2]) (set []) (set [])
            
    -- | An example of 'Sketch' containing no 'CrescentMoon' but in a tricky way. 
    exampleNoCrescentMoon :: Sketch Text Text
    exampleNoCrescentMoon = simplify result
        where
            cg = unsafeReadCGString "D -p1-> A -f-> C = D -p3-> C\nD -p2-> B\nX -c-> A\nX -a-> C\nX -b-> C\n"
            indx1 = unsafeReadCGString "A -f-> C\nB\n"
            base1 = unsafeReadCGDString "<SRC>\nA -f-> C\nB\n</SRC>\n<TGT>\nD -p1-> A -f-> C = D -p3-> C\nD -p2-> B\nX -c-> A\nX -a-> C\nX -b-> C\n</TGT>\nA -f-> C => A -f-> C\nB => B\n"
            c1 = unsafeCone (pack "D") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "D")) base1 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")), (pack "B", unsafeGetMorphismFromLabel cg (pack "p2")), (pack "C", unsafeGetMorphismFromLabel cg (pack "p3"))]))
            indx2 = unsafeReadCGString "*\n"
            base2 = unsafeReadCGDString "<SRC>\n*\n</SRC>\n<TGT>\nD -p1-> A -f-> C = D -p3-> C\nD -p2-> B\nX -c-> A\nX -a-> C\nX -b-> C\n</TGT>\n* => A\n"
            c2 = unsafeCone (pack "D") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "D")) base2 (weakMap [(pack "*", unsafeGetMorphismFromLabel cg (pack "p1"))]))
            result = unsafeSketch cg (set [c1,c2]) (set []) (set [])
    

    -- | An example of 'Sketch' containing a 'Colantern'. 
    exampleColantern :: Sketch Text Text
    exampleColantern = simplify result
        where
            cg = unsafeReadCGString "A -q1-> A + B -f-> C = A -q1-> A + B -g-> C\nB -q2-> A + B -f-> C = B -q2-> A + B -g-> C\n"
            indx1 = unsafeReadCGString "A\nB\n"
            base1 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nA -q1-> A + B -f-> C = A -q1-> A + B -g-> C\nB -q2-> A + B -f-> C = B -q2-> A + B -g-> C\n</TGT>\nA => A\nB => B\n"
            cc1 = unsafeCocone (pack "A + B") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "A + B")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1")), (pack "B", unsafeGetMorphismFromLabel cg (pack "q2"))]))
            result = unsafeSketch cg (set []) (set [cc1]) (set [])
    
    -- | An example of 'Sketch' containing a 'Cospotlight'. 
    exampleCospotlight :: Sketch Text Text
    exampleCospotlight = simplify result
        where
            cg = unsafeReadCGString "A -f-> B\nA -g-> B\n"
            indx1 = unsafeReadCGString "A\nB\n"
            base1 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nA -f-> B\nA -g-> B\n</TGT>\nA => A\nB => A\n"
            cc1 = unsafeCocone (pack "B") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "B")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "f")), (pack "B", unsafeGetMorphismFromLabel cg (pack "f"))]))
            result = unsafeSketch cg (set []) (set [cc1]) (set [])
        
    -- | An example of 'Sketch' containing a 'CocrescentMoon'. 
    exampleCocrescentMoon :: Sketch Text Text
    exampleCocrescentMoon = simplify result
        where
            cg = unsafeReadCGString "B -f-> A\nC -g-> A\nB -h-> X\nC -i-> X\nC -j-> X\n"
            indx1 = unsafeReadCGString "A\nB\n"
            base1 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nB -f-> A\nC -g-> A\nB -h-> X\nC -i-> X\nC -j-> X\n</TGT>\nA => B\nB => C\n"
            cc1 = unsafeCocone (pack "A") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "A")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "f")), (pack "B", unsafeGetMorphismFromLabel cg (pack "g"))]))
            indx2 = unsafeReadCGString "*\n"
            base2 = unsafeReadCGDString "<SRC>\n*\n</SRC>\n<TGT>\nB -f-> A\nC -g-> A\nB -h-> X\nC -i-> X\nC -j-> X\n</TGT>\n* => B\n"
            cc2 = unsafeCocone (pack "A") (unsafeNaturalTransformation base2 (constantDiagram indx2 cg (pack "A")) (weakMap [(pack "*", unsafeGetMorphismFromLabel cg (pack "f"))]))
            result = unsafeSketch cg (set []) (set [cc1,cc2]) (set [])
            
    
    -- | An example of 'Sketch' to realize.
    exampleSketchToRealize :: Sketch Text Text
    exampleSketchToRealize = simplify result
        where
            cg = unsafeReadCGString "A -f-> B\nA -g-> C\nX -h-> B\nX -i-> C\n"
            indx1 = unsafeReadCGString "A\nB\n"
            base1 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nA -f-> B\nA -g-> C\nX -h-> B\nX -i-> C\n</TGT>\nA => B\nB => C\n"
            c1 = unsafeCone (pack "A") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "A")) base1 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "f")), (pack "B", unsafeGetMorphismFromLabel cg (pack "g"))]))
            result = unsafeSketch cg (set [c1]) (set []) (set [])
            

    exampleSketchSAT1 :: Sketch Text Text
    exampleSketchSAT1 = simplify result
        where
            cg = unsafeReadCGString "1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -et-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -et-> B = 1 -F-> B\n1 -(F,V)-> BxB -et-> B = 1 -F-> B\n1 -(V,F)-> BxB -et-> B = 1 -F-> B\n1 -(V,V)-> BxB -et-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -et-> B = 1 -V-> B\n"
            indx1 = unsafeReadCGString ""
            base1 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -et-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -et-> B = 1 -F-> B\n1 -(F,V)-> BxB -et-> B = 1 -F-> B\n1 -(V,F)-> BxB -et-> B = 1 -F-> B\n1 -(V,V)-> BxB -et-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -et-> B = 1 -V-> B\n</TGT>\n"
            c1 = unsafeCone (pack "1") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "1")) base1 (weakMap []))
            indx2 = unsafeReadCGString "A\nB\n"
            base2 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -et-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -et-> B = 1 -F-> B\n1 -(F,V)-> BxB -et-> B = 1 -F-> B\n1 -(V,F)-> BxB -et-> B = 1 -F-> B\n1 -(V,V)-> BxB -et-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -et-> B = 1 -V-> B\n</TGT>\nA => 1\nB => 1\n"
            cc2 = unsafeCocone (pack "B") (unsafeNaturalTransformation base2 (constantDiagram indx2 cg (pack "B")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "V")),(pack "B", unsafeGetMorphismFromLabel cg (pack "F"))]))
            indx3 = unsafeReadCGString "A\nB\n"
            base3 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -et-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -et-> B = 1 -F-> B\n1 -(F,V)-> BxB -et-> B = 1 -F-> B\n1 -(V,F)-> BxB -et-> B = 1 -F-> B\n1 -(V,V)-> BxB -et-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -et-> B = 1 -V-> B\n</TGT>\nA => B\nB => B\n"
            c3 = unsafeCone (pack "BxB") (unsafeNaturalTransformation (constantDiagram indx3 cg (pack "BxB")) base3 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2"))]))
            result = unsafeSketch cg (set [c1,c3]) (set [cc2]) (set [])
            
    exampleSketchSAT2 :: Sketch Text Text
    exampleSketchSAT2 = simplify result
        where
            cg = unsafeReadCGString "1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -ou-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -ou-> B = 1 -F-> B\n1 -(F,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,F)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -ou-> B = 1 -V-> B\n"
            indx1 = unsafeReadCGString ""
            base1 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -ou-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -ou-> B = 1 -F-> B\n1 -(F,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,F)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -ou-> B = 1 -V-> B\n</TGT>\n"
            c1 = unsafeCone (pack "1") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "1")) base1 (weakMap []))
            indx2 = unsafeReadCGString "A\nB\n"
            base2 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -ou-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -ou-> B = 1 -F-> B\n1 -(F,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,F)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -ou-> B = 1 -V-> B\n</TGT>\nA => 1\nB => 1\n"
            cc2 = unsafeCocone (pack "B") (unsafeNaturalTransformation base2 (constantDiagram indx2 cg (pack "B")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "V")),(pack "B", unsafeGetMorphismFromLabel cg (pack "F"))]))
            indx3 = unsafeReadCGString "A\nB\n"
            base3 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n1 -V-> B\n1 -F-> B\n1 -P-> B\n1 -Q-> B\nBxB -p1-> B\nBxB -p2-> B\nBxB -ou-> B\n1 -(F,F)-> BxB -p1-> B = 1 -F-> B\n1 -(F,F)-> BxB -p2-> B = 1 -F-> B\n1 -(F,V)-> BxB -p1-> B = 1 -F-> B\n1 -(F,V)-> BxB -p2-> B = 1 -V-> B\n1 -(V,F)-> BxB -p1-> B = 1 -V-> B\n1 -(V,F)-> BxB -p2-> B = 1 -F-> B\n1 -(V,V)-> BxB -p1-> B = 1 -V-> B\n1 -(V,V)-> BxB -p2-> B = 1 -V-> B\n1 -(F,F)-> BxB -ou-> B = 1 -F-> B\n1 -(F,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,F)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(V,V)-> BxB -ou-> B = 1 -V-> B\n1 -(P,Q)-> BxB -p1-> B = 1 -P-> B\n1 -(P,Q)-> BxB -p2-> B = 1 -Q-> B\n1 -(P,Q)-> BxB -ou-> B = 1 -V-> B\n</TGT>\nA => B\nB => B\n"
            c3 = unsafeCone (pack "BxB") (unsafeNaturalTransformation (constantDiagram indx3 cg (pack "BxB")) base3 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2"))]))
            result = unsafeSketch cg (set [c1,c3]) (set [cc2]) (set [])
            
    exampleSketchSAT3 :: Sketch Text Text
    exampleSketchSAT3 = simplify result
        where
            cg = unsafeReadCGString "P&Q -p1-> P\nP&Q -p2-> Q\nX -f-> Q\nX -g-> Q\n"
            indx1 = unsafeReadCGString ""
            base1 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\nP&Q -p1-> P\nP&Q -p2-> Q\nX -f-> Q\nX -g-> Q\n</TGT>\n"
            c1 = unsafeCone (pack "P&Q") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "P&Q")) base1 (weakMap []))
            indx2 = unsafeReadCGString "A\nB\n"
            base2 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nP&Q -p1-> P\nP&Q -p2-> Q\nX -f-> Q\nX -g-> Q\n</TGT>\nA => P\nB => Q\n"
            c2 = unsafeCone (pack "P&Q") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "P&Q")) base2 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2"))]))
            result = unsafeSketch cg (set [c1,c2]) (set []) (set [])
            
    exampleSketchSAT4 :: Sketch Text Text
    exampleSketchSAT4 = simplify result
        where
            cg = unsafeReadCGString "P -q1-> P|Q\nQ -q2-> P|Q\nQ -f-> X\nQ -g-> X\n"
            indx1 = unsafeReadCGString ""
            base1 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\nP -q1-> P|Q\nQ -q2-> P|Q\nQ -f-> X\nQ -g-> X\n</TGT>\n"
            cc1 = unsafeCocone (pack "P|Q") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "P|Q")) (weakMap []))
            indx2 = unsafeReadCGString "A\nB\n"
            base2 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nP -q1-> P|Q\nQ -q2-> P|Q\nQ -f-> X\nQ -g-> X\n</TGT>\nA => P\nB => Q\n"
            cc2 = unsafeCocone (pack "P|Q") (unsafeNaturalTransformation base2 (constantDiagram indx2 cg (pack "P|Q")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2"))]))
            result = unsafeSketch cg (set []) (set [cc1,cc2]) (set [])
            
    exampleSketchSAT5 :: Sketch Text Text
    exampleSketchSAT5 = simplify result
        where
            cg = unsafeReadCGString "A&-A -p3-> A\nA&-A -p4-> -A\nA&-A -f-> X\nA&-A -g-> X\n"
            indx1 = unsafeReadCGString ""
            base1 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\nA&-A -p3-> A\nA&-A -p4-> -A\nA&-A -f-> X\nA&-A -g-> X\n</TGT>\n"
            cc1 = unsafeCocone (pack "A&-A") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "A&-A")) (weakMap []))
            indx2 = unsafeReadCGString "A\nB\n"
            base2 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nA&-A -p3-> A\nA&-A -p4-> -A\nA&-A -f-> X\nA&-A -g-> X\n</TGT>\nA => A\nB => -A\n"
            c3 = unsafeCone (pack "A&-A") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "A&-A")) base2 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p3")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p4"))]))
            result = unsafeSketch cg (set [c3]) (set [cc1]) (set [])
            
    exampleSketchSAT6 :: Sketch Text Text
    exampleSketchSAT6 = simplify result
        where
            cg = unsafeReadCGString "0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n"
            indx1 = unsafeReadCGString ""
            base1 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\n"
            cc1 = unsafeCocone (pack "0") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "0")) (weakMap []))
            indx2 = unsafeReadCGString "A\nB\n"
            base2 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => A\nB => -A\n"
            c2 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base2 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1A")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2A"))]))
            base3 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => B\nB => -B\n"
            c3 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base3 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1B")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2B"))]))
            base4 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => C\nB => -C\n"
            c4 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base4 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1C")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2C"))]))
            base5 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -A\nB => B\n"
            cc5 = unsafeCocone (pack "-A|B") (unsafeNaturalTransformation base5 (constantDiagram indx2 cg (pack "-A|B")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2"))]))
            base6 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -B\nB => C\n"
            cc6 = unsafeCocone (pack "-B|C") (unsafeNaturalTransformation base6 (constantDiagram indx2 cg (pack "-B|C")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q3")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q4"))]))
            indx7 = unsafeReadCGString "A\nB\nC\nD\n"
            base7 = unsafeReadCGDString "<SRC>\nA\nB\nC\nD\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -A|B\nB => -B|C\nC => A\nD => -C\n"
            c7 = unsafeCone (pack "(-A|B)&(-B|C)&A&-C") (unsafeNaturalTransformation (constantDiagram indx7 cg (pack "(-A|B)&(-B|C)&A&-C")) base7 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2")),(pack "C", unsafeGetMorphismFromLabel cg (pack "p3")),(pack "D", unsafeGetMorphismFromLabel cg (pack "p4"))]))
            base8 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => A\nB => -A\n"
            cc8 = unsafeCocone (pack "1") (unsafeNaturalTransformation base8 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1A")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2A"))]))
            base9 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => B\nB => -B\n"
            cc9 = unsafeCocone (pack "1") (unsafeNaturalTransformation base9 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1B")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2B"))]))
            base10 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => C\nB => -C\n"
            cc10 = unsafeCocone (pack "1") (unsafeNaturalTransformation base10 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1C")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2C"))]))
            c11 = unsafeCone (pack "1") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "1")) base1 (weakMap []))
            result = unsafeSketch cg (set [c2,c3,c4,c7,c11]) (set [cc1,cc5,cc6,cc8,cc9,cc10]) (set [])
            
    exampleSketchSAT7 :: Sketch Text Text
    exampleSketchSAT7 = simplify result
        where
            cg = unsafeReadCGString "0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n"
            indx1 = unsafeReadCGString ""
            base1 = unsafeReadCGDString "<SRC>\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\n"
            cc1 = unsafeCocone (pack "0") (unsafeNaturalTransformation base1 (constantDiagram indx1 cg (pack "0")) (weakMap []))
            indx2 = unsafeReadCGString "A\nB\n"
            base2 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => A\nB => -A\n"
            c2 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base2 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1A")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2A"))]))
            base3 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => B\nB => -B\n"
            c3 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base3 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1B")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2B"))]))
            base4 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => C\nB => -C\n"
            c4 = unsafeCone (pack "0") (unsafeNaturalTransformation (constantDiagram indx2 cg (pack "0")) base4 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1C")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2C"))]))
            base5 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -A\nB => B\n"
            cc5 = unsafeCocone (pack "-A|B") (unsafeNaturalTransformation base5 (constantDiagram indx2 cg (pack "-A|B")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2"))]))
            base6 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -B\nB => C\n"
            cc6 = unsafeCocone (pack "-B|C") (unsafeNaturalTransformation base6 (constantDiagram indx2 cg (pack "-B|C")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q3")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q4"))]))
            indx7 = unsafeReadCGString "A\nB\nC\nD\n"
            base7 = unsafeReadCGDString "<SRC>\nA\nB\nC\nD\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => -A|B\nB => -B|C\nC => A\nD => -C\n"
            c7 = unsafeCone (pack "(-A|B)&(-B|C)&A&-C") (unsafeNaturalTransformation (constantDiagram indx7 cg (pack "(-A|B)&(-B|C)&A&-C")) base7 (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "p1")),(pack "B", unsafeGetMorphismFromLabel cg (pack "p2")),(pack "C", unsafeGetMorphismFromLabel cg (pack "p3")),(pack "D", unsafeGetMorphismFromLabel cg (pack "p4"))]))
            base8 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => A\nB => -A\n"
            cc8 = unsafeCocone (pack "1") (unsafeNaturalTransformation base8 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1A")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2A"))]))
            base9 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => B\nB => -B\n"
            cc9 = unsafeCocone (pack "1") (unsafeNaturalTransformation base9 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1B")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2B"))]))
            base10 = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -p1A-> A\nA -q1A-> 1\n0 -p2A-> -A -q2A-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1B-> B -q1B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2B-> -B -q2B-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p1C-> C -q1C-> 1 = 0 -p1A-> A -q1A-> 1\n0 -p2C-> -C -q2C-> 1 = 0 -p1A-> A -q1A-> 1\n-A -q1-> -A|B\nB -q2-> -A|B\n-B -q3-> -B|C\nC -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p1-> -A|B\n(-A|B)&(-B|C)&A&-C -p2-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A\n(-A|B)&(-B|C)&A&-C -p4-> -C\n(-A|B)&(-B|C)&A&-C -f-> X\n(-A|B)&(-B|C)&A&-C -g-> X\n0 -p2A-> -A -q1-> -A|B = 0 -p1B-> B -q2-> -A|B\n0 -p2B-> -B -q3-> -B|C = 0 -p1C-> C -q4-> -B|C\n(-A|B)&(-B|C)&A&-C -p3-> A -q1A-> 1 = (-A|B)&(-B|C)&A&-C -p4-> -C -q2C-> 1\n</TGT>\nA => C\nB => -C\n"
            cc10 = unsafeCocone (pack "1") (unsafeNaturalTransformation base10 (constantDiagram indx2 cg (pack "1")) (weakMap [(pack "A", unsafeGetMorphismFromLabel cg (pack "q1C")),(pack "B", unsafeGetMorphismFromLabel cg (pack "q2C"))]))
            c11 = unsafeCone (pack "1") (unsafeNaturalTransformation (constantDiagram indx1 cg (pack "1")) base1 (weakMap []))
            result = unsafeSketch cg (set [c2,c3,c4,c7,c11]) (set [cc1,cc5,cc6,cc8,cc9,cc10]) (set [])