# Constant formulas and knowledge
e 0 c e
e 1 c g
e 2 c i
k 0 d 0 d1

# Horn Formula

e 3 h p cnf 6 1 -1 0 ;
e 4 h p cnf 6 2 -4 -2 0 -5 0 ;
e 5 h p cnf 6 2 1 0 6 0 ;
e 6 h p cnf 6 2 4 0 2 0 ;
e 7 h p cnf 6 1 6 0 ;
e 8 h p cnf 6 1 -4 -2 0 ;

e 9 n 3
e 10 n 4
e 11 n 5
e 12 n 6
e 13 n 7
e 14 n 8
e 15 p 3
e 16 p 4
e 17 r 6
e 18 r 7
e 19 n 0
k 1 s 5 7 b1
k 2 s 3 11 b1
k 3 s 14 6 b1
k 4 s 13 11 b1
e 20 u 5 3
k 5 s 7 20 b2
e 21 i 9 1
k 6 s 21 5 b3
e 22 i 8 1
k 7 s 22 9 b3
e 23 i 12 1
k 8 s 23 19 b3
e 24 u 3 0
k 9 s 15 24 b4
e 25 i 3 1
k 10 s 25 0 b3
k 11 d 25 d3 10 0
k 12 d 3 d6 9 0 11
e 26 u 4 3
k 13 s 16 26 b4
k 14 s 2 4 b1
k 15 d 10 d7 13 12 14
k 16 s 1 10 b1
k 17 d 1 d3 16 15
k 18 u d5 17
e 27 u 4 11
k 19 s 16 27 b4
e 28 u 6 0
k 20 s 17 28 b5
k 21 s 2 12 b1
k 22 d 6 d9 20 0 21
e 29 u 7 6
k 23 s 18 29 b5
e 30 i 13 1
k 24 s 30 0 b3
k 25 d 30 d3 24 0
k 26 d 13 d8 23 22 25
k 27 s 2 13 b1
k 28 d 2 d3 27 26
k 29 u d4 28
e 31 u 7 14
k 30 s 18 31 b5


# BDD

e 32 b testbdds.bdd 0 ;
e 33 b testbdds.bdd 1 ;
e 34 b testbdds.bdd 2 ;
e 35 b testbdds.bdd 3 ;
e 36 b testbdds.bdd 4 ;
e 37 b testbdds.bdd 5 ;

e 38 n 32
e 39 n 33
e 40 n 34
e 41 n 35
e 42 n 36
e 43 n 37
e 44 p 32
e 45 p 33
e 46 r 35
e 47 r 36
e 48 n 0
k 31 s 34 36 b1
k 32 s 32 40 b1
k 33 s 43 35 b1
k 34 s 42 40 b1
e 49 u 34 32
k 35 s 36 49 b2
e 50 i 38 1
k 36 s 50 34 b3
e 51 i 37 1
k 37 s 51 38 b3
e 52 i 41 1
k 38 s 52 48 b3
e 53 u 32 0
k 39 s 44 53 b4
e 54 i 32 1
k 40 s 54 0 b3
k 41 d 54 d3 40 0
k 42 d 32 d6 39 0 41
e 55 u 33 32
k 43 s 45 55 b4
k 44 s 2 33 b1
k 45 d 39 d7 43 42 44
k 46 s 1 39 b1
k 47 d 1 d3 46 45
k 48 u d5 47
e 56 u 33 40
k 49 s 45 56 b4
e 57 u 35 0
k 50 s 46 57 b5
k 51 s 2 41 b1
k 52 d 35 d9 50 0 51
e 58 u 36 35
k 53 s 47 58 b5
e 59 i 42 1
k 54 s 59 0 b3
k 55 d 59 d3 54 0
k 56 d 42 d8 53 52 55
k 57 s 2 42 b1
k 58 d 2 d3 57 56
k 59 u d4 58
e 60 u 36 43
k 60 s 47 60 b5

# Explicit set

e 61 e 00 04 08 0c 10 14 18 1c 20 24 28 2c 30 34 38 3c 40 44 48 4c 50 54 58 5c 60 64 68 6c 70 74 78 7c ;
e 62 e 00 04 10 14 20 24 30 34 40 44 60 64 80 84 90 94 a0 a4 b0 b4 c0 c4 e0 e4 ;
e 63 e 84 8c 94 9c a4 ac b4 bc c4 cc d4 dc e4 ec f4 fc ;
e 64 e 50 54 58 5c 70 74 78 7c d0 d4 d8 dc f0 f4 f8 fc ;
e 65 e 04 14 24 34 44 54 64 74 84 94 a4 b4 c4 d4 e4 f4 0c 1c 2c 3c 4c 5c 6c 7c 8c 9c ac bc cc dc ec fc ;
e 66 e 00 04 08 0c 10 14 18 1c 20 24 28 2c 30 34 38 3c 40 44 48 4c 60 64 68 6c 80 84 88 8c 90 94 98 9c a0 a4 a8 ac b0 b4 b8 bc c0 c4 c8 cc e0 e4 e8 ec ;

e 67 n 61
e 68 n 62
e 69 n 63
e 70 n 64
e 71 n 65
e 72 n 66
e 73 p 61
e 74 p 62
e 75 r 64
e 76 r 65
e 77 n 0
k 62 s 63 65 b1
k 63 s 61 69 b1
k 64 s 72 64 b1
k 65 s 71 69 b1
e 78 u 63 61
k 66 s 65 78 b2
e 79 i 67 1
k 67 s 79 63 b3
e 80 i 66 1
k 68 s 80 67 b3
e 81 i 70 1
k 69 s 81 77 b3
e 82 u 61 0
k 70 s 73 82 b4
e 83 i 61 1
k 71 s 83 0 b3
k 72 d 83 d3 71 0
k 73 d 61 d6 70 0 72
e 84 u 62 61
k 74 s 74 84 b4
k 75 s 2 62 b1
k 76 d 68 d7 74 73 75
k 77 s 1 68 b1
k 78 d 1 d3 77 76
k 79 u d5 78
e 85 u 62 69
k 80 s 74 85 b4
e 86 u 64 0
k 81 s 75 86 b5
k 82 s 2 70 b1
k 83 d 64 d9 81 0 82
e 87 u 65 64
k 84 s 76 87 b5
e 88 i 71 1
k 85 s 88 0 b3
k 86 d 88 d3 85 0
k 87 d 71 d8 84 83 86
k 88 s 2 71 b1
k 89 d 2 d3 88 87
k 90 u d4 89
e 89 u 65 72
k 91 s 76 89 b5
