(sbool 
    (
        (0.0 0.0 1.0) 
        (1 1) 
        (19 13 
            (TRUE)) 
        (20 13 
            (TRUE)) 
        (21 13 
            (TRUE)) 
        (22 13 
            (TRUE)) 
        (23 13 
            (TRUE)) 
        (24 13 
            (TRUE)) 
        (25 13 
            (TRUE)) 
        (7 14 
            (TRUE)) 
        (8 14 
            (TRUE)) 
        (9 14 
            (TRUE)) 
        (10 14 
            (TRUE)) 
        (11 14 
            (TRUE)) 
        (12 14 
            (TRUE)) 
        (13 14 
            (TRUE)) 
        (14 14 
            (TRUE)) 
        (15 14 
            (TRUE)) 
        (16 14 
            (TRUE)) 
        (17 14 
            (TRUE)) 
        (18 14 
            (TRUE)) 
        (26 14 
            (TRUE)) 
        (27 14 
            (TRUE)) 
        (28 14 
            (TRUE)) 
        (1 15 
            (TRUE)) 
        (2 15 
            (TRUE)) 
        (3 15 
            (TRUE)) 
        (4 15 
            (TRUE)) 
        (5 15 
            (TRUE)) 
        (6 15 
            (TRUE)) 
        (29 15 
            (TRUE)) 
        (30 15 
            (TRUE)) 
        (1 16 
            (TRUE)) 
        (2 17 
            (TRUE)) 
        (2 18 
            (TRUE)) 
        (3 19 
            (TRUE)) 
        (3 20 
            (TRUE)) 
        (4 21 
            (TRUE)) 
        (4 22 
            (TRUE)) 
        (5 23 
            (TRUE)) 
        (5 24 
            (TRUE)) 
        (6 25 
            (TRUE)) 
        (6 26 
            (TRUE)) 
        (7 27 
            (TRUE)) 
        (7 28 
            (TRUE)) 
        (8 29 
            (TRUE)) 
        (8 30 
            (TRUE)) 
        (9 31 
            (TRUE)) 
        (9 32 
            (TRUE)) 
        (10 33 
            (TRUE)) 
        (10 34 
            (TRUE)) 
        (11 35 
            (TRUE)) 
        (11 36 
            (TRUE)) 
        (12 37 
            (TRUE)) 
        (12 38 
            (TRUE)) 
        (12 39 
            (TRUE)) 
        (13 40 
            (TRUE)) 
        (13 41 
            (TRUE)) 
        (14 42 
            (TRUE)) 
        (14 43 
            (TRUE)) 
        (15 44 
            (TRUE)) 
        (15 45 
            (TRUE)) 
        (16 46 
            (TRUE)) 
        (16 47 
            (TRUE)) 
        (17 48 
            (TRUE)) 
        (17 49 
            (TRUE)) 
        (18 50 
            (TRUE)) 
        (18 51 
            (TRUE)) 
        (19 52 
            (TRUE)) 
        (19 53 
            (TRUE)) 
        (20 54 
            (TRUE)) 
        (20 55 
            (TRUE)) 
        (21 56 
            (TRUE)) 
        (21 57 
            (TRUE)) 
        (22 58 
            (TRUE)) 
        (22 59 
            (TRUE)) 
        (23 60 
            (TRUE)) 
        (23 61 
            (TRUE)) 
        (24 62 
            (TRUE)) 
        (24 63 
            (TRUE))))