--------------------------------------- Model 5_0: 0 4 3 2 1 3 1 4 0 2 1 0 2 4 3 4 2 1 3 0 2 3 0 1 4 -- cycle notation: 0: (0) (1 4) (2 3) 1: (1) (2 4) (3 0) 2: (2) (3 4) (0 1) 3: (3) (4 0) (1 2) 4: (4) (0 2) (1 3) -- autom facts: AUTOM: (0) (1 2 4 3) (0 2 1 4 3) Equational facts: X = (f X X) X = (f Y (f Y X)) X = (f (f Y X) (f X Y)) X = (f (f (f X Y) X) Y) X = (f (f (f Y X) Y) Y) (f X Y) = (f (f Y X) X) 2 = (f X (f X 2)) X = (g X X) X = (f 2 (f 2 X)) 0 = (f X (f X 0)) X = (f (f X Y) (f (f X Y) X)) (f (f X Y) X) = (f (f Y X) Y) (f X Y) = (f Y (f (f X Y) X)) X = (f (f X Y) (f (f Y X) Y)) X = (f 3 (f 3 X)) X = (f 1 (f 1 X)) (f X Y) = (f (f X Y) (f X Y)) (f (f X Y) X) = (f Y (f X Y)) 3 = (f X (f X 3)) (f (f X Y) X) = (f X (f Y X)) --------------------------------------- Model 7_0: 5 6 3 1 0 2 4 3 0 6 4 2 1 5 2 4 1 6 5 3 0 4 3 5 2 6 0 1 1 5 4 0 3 6 2 6 2 0 5 1 4 3 0 1 2 3 4 5 6 -- cycle notation: 0: (0 5 2 3 1 6 4) 1: (1 0 3 4 2 6 5) 2: (2 1 4 5 3 6 0) 3: (3 2 5 0 4 6 1) 4: (4 3 0 1 5 6 2) 5: (5 4 1 2 0 6 3) 6: (6) (0) (1) (2) (3) (4) (5) -- autom facts: AUTOM: (0 5 4 3 2 1) (6) Equational facts: X = (f 6 X) X = (f X (f X 6)) 6 = (f (f X X) X) X = (f (f (f X Y) Y) Y) X = (f (f Y X) (f Y (f X Y))) (f X Y) = (f 6 (f X Y)) (f X (f Y X)) = (f Y (f X X)) X = (f 1 (f 4 X)) X = (f 0 (f 3 X)) X = (f (f Y Y) (f X (f X Y))) X = (f (f X (f X X)) 6) (f X (f X Y)) = (f Y (f Y X)) X = (f (f X X) (f X (f X X))) X = (f 2 (f 5 X)) X = (f 3 (f 0 X)) X = (f Y (f (f Y X) (f X Y))) X = (f (f Y X) (f X (f Y Y))) X = (f 5 (f 2 X)) (f X X) = (f 6 (f X X)) (f X (f Y Y)) = (f Y (f X Y)) --------------------------------------- Model 7_1: 6 3 0 4 2 5 1 5 6 2 0 1 4 3 2 0 6 3 5 1 4 1 2 5 6 4 3 0 0 4 3 1 6 2 5 3 1 4 5 0 6 2 4 5 1 2 3 0 6 -- cycle notation: 0: (0 6 1 3 4 2) (5) 1: (1 6 3 0 5 4) (2) 2: (2 6 4 5 1 0) (3) 3: (3 6 0 1 2 5) (4) 4: (4 6 5 2 3 1) (0) 5: (5 6 2 4 0 3) (1) 6: (6) (0 4 3 2 1 5) -- autom facts: AUTOM: (0 4 3 2 1 5) (6) Equational facts: 6 = (f X X) X = (f (f (f X Y) Y) Y) X = (f (f 6 X) X) X = (f Y (f X (f (f X Y) X))) (f X Y) = (f (f X Y) (f Y X)) X = (f X (f X (f 6 X))) (f X (f X Y)) = (f Y (f Y X)) X = (f Y (f X (f (f Y X) Y))) (f (f X Y) X) = (f (f Y X) Y) 6 = (f (f X Y) (f X Y)) 1 = (f X (f (f 4 X) X)) 4 = (f (f (f 4 X) X) X) 2 = (f (f (f 2 X) X) X) 5 = (f X (f (f 3 X) X)) (f X Y) = (f (f (f (f Y X) Y) X) X) (f X Y) = (f (f (f (f X Y) X) X) X) 3 = (f X (f (f 5 X) X)) 3 = (f (f (f 3 X) X) X) 5 = (f (f (f 5 X) X) X) (f X Y) = (f Y (f (f (f Y X) Y) Y)) --------------------------------------- Model 9_0: 1 5 2 6 7 4 8 3 0 6 3 8 0 5 2 4 7 1 8 1 7 4 0 3 5 6 2 7 2 6 5 4 1 0 8 3 2 0 3 8 6 5 7 1 4 3 4 1 7 8 0 6 2 5 0 7 4 1 3 8 2 5 6 5 8 0 3 2 6 1 4 7 4 6 5 2 1 7 3 0 8 -- cycle notation: 0: (0 1 5 4 7 3 6 8) (2) 1: (1 3 0 6 4 5 2 8) (7) 2: (2 7 6 5 3 4 0 8) (1) 3: (3 5 1 2 6 0 7 8) (4) 4: (4 6 7 1 0 2 3 8) (5) 5: (5 0 3 7 2 1 4 8) (6) 6: (6 2 4 3 1 7 5 8) (0) 7: (7 4 2 0 5 6 1 8) (3) 8: (8) (0 4 1 6 3 2 5 7) -- autom facts: AUTOM: (0 2 1 7 3 4 5 6) (8) Equational facts: X = (f X 8) X = (f (f (f X X) X) X) X = (f (f (f X Y) Y) Y) X = (f (f X 7) 6) X = (f (f X 0) 3) X = (f (f X 3) 0) (f (f X X) Y) = (f (f X Y) X) (f X Y) = (f (f X Y) 8) (f X X) = (f (f X X) 8) X = (f Y (f X (f (f Y Y) X))) 8 = (f X (f (f X X) X)) X = (f (f X 6) 7) X = (f (f 8 X) (f X X)) X = (f (f X 2) 4) X = (f Y (f X (f (f Y X) Y))) X = (f (f X 1) 5) (f X (f X Y)) = (f Y (f Y X)) (f (f X Y) X) = (f (f X X) Y) X = (f (f X 4) 2) X = (f (f X 5) 1) --------------------------------------- Model 11_0: 0 10 9 7 8 4 5 2 1 6 3 10 1 6 8 5 9 3 4 7 0 2 9 6 2 10 1 3 7 5 0 4 8 7 8 10 3 2 0 4 6 5 1 9 8 5 1 2 4 10 9 0 3 7 6 4 9 3 0 10 5 1 8 6 2 7 5 3 7 4 9 1 6 10 2 8 0 2 4 5 6 0 8 10 7 9 3 1 1 7 0 5 3 6 2 9 8 10 4 6 0 4 1 7 2 8 3 10 9 5 3 2 8 9 6 7 0 1 4 5 10 -- cycle notation: 0: (0) (1 10 3 7 2 9 6 5 4 8) 1: (1) (2 6 3 8 7 4 5 9 0 10) 2: (2) (3 10 8 0 9 4 1 6 7 5) 3: (3) (4 2 10 9 1 8 5 0 7 6) 4: (4) (5 10 6 9 7 0 8 3 2 1) 5: (5) (6 1 9 2 3 0 4 10 7 8) 6: (6) (7 10 0 5 1 3 4 9 8 2) 7: (7) (8 9 3 6 10 1 4 0 2 5) 8: (8) (9 10 4 3 5 6 2 0 1 7) 9: (9) (10 5 2 4 7 3 1 0 6 8) 10: (10) (0 3 9 5 7 1 2 8 4 6) -- autom facts: AUTOM: (0) (1 8 4 5 6 9 2 7 3 10) (0 10 1 7 8 5 3 2 4 9 6) Equational facts: X = (f X X) (f X Y) = (f Y X) (f 6 X) = (f X 6) (f 4 X) = (f X 4) (f 0 X) = (f X 0) X = (f (f X (f (f X Y) Y)) Y) (f (f X Y) X) = (f X (f X Y)) (f (f X Y) Y) = (f Y (f X Y)) (f X 1) = (f 1 X) (f 10 X) = (f X 10) (f 9 X) = (f X 9) (f 5 X) = (f X 5) (f 8 X) = (f X 8) X = (g X X) (f 2 X) = (f X 2) X = (f Y (f (f (f Y X) Y) X)) (f X 10) = (f 10 X) (f 3 X) = (f X 3) (f 7 X) = (f X 7) (f 1 X) = (f X 1) --------------------------------------- Model 11_1: 0 2 10 5 7 9 1 8 6 4 3 10 1 9 6 0 4 7 5 3 8 2 3 8 2 10 6 1 5 0 9 7 4 9 7 4 3 10 8 0 6 2 5 1 8 10 5 1 4 6 9 2 7 3 0 4 0 8 2 9 5 10 3 1 6 7 2 5 1 9 3 7 6 10 4 0 8 6 4 3 0 5 2 8 7 10 1 9 1 6 7 4 2 0 3 9 8 10 5 7 3 0 8 1 10 2 4 5 9 6 5 9 6 7 8 3 4 1 0 2 10 -- cycle notation: 0: (0) (1 2 10 3 5 9 4 7 8 6) 1: (1) (2 9 8 3 6 7 5 4 0 10) 2: (2) (3 10 4 6 5 1 8 9 7 0) 3: (3) (4 10 1 7 6 0 9 5 8 2) 4: (4) (5 6 9 3 1 10 0 8 7 2) 5: (5) (6 10 7 3 2 8 1 0 4 9) 6: (6) (7 10 8 4 3 9 0 2 1 5) 7: (7) (8 10 9 1 4 5 2 3 0 6) 8: (8) (9 10 5 0 1 6 3 4 2 7) 9: (9) (10 6 2 0 7 4 1 3 8 5) 10: (10) (0 5 3 7 1 9 2 6 4 8) -- autom facts: AUTOM: (0) (1 7 5 2 8 9 10 6 4 3) (0 5 7 8 1 4 2 9 3 10 6) Equational facts: X = (f X X) X = (f (f (f Y X) X) Y) (f X Y) = (f Y (f Y X)) (f X (f Y X)) = (f (f X Y) X) X = (f (f Y (f X Y)) (f X Y)) X = (f (f (f Y X) Y) (f X Y)) X = (g X X) X = (f Y (f (f X Y) (f Y X))) (f (f X Y) X) = (f X (f Y X)) (f X Y) = (f (f X Y) (f X Y)) X = (f (f Y X) (f (f X Y) Y)) (f 3 X) = (f X (f X 3)) (f X Y) = (f (f (f Y X) (f X Y)) X) (f 7 X) = (f X (f X 7)) (f 10 X) = (f X (f X 10)) (f 4 X) = (f X (f X 4)) (f 2 X) = (f X (f X 2)) (f 5 X) = (f X (f X 5)) (f (f X Y) X) = (f Y (f (f X Y) Y)) (f X (f Y X)) = (f Y (f (f X Y) Y)) --------------------------------------- Model 11_2: 0 10 6 9 1 7 4 8 3 2 5 3 1 10 7 0 2 8 5 9 4 6 5 4 2 10 8 1 3 9 6 0 7 1 6 5 3 10 9 2 4 0 7 8 8 2 7 6 4 10 0 3 5 1 9 2 9 3 8 7 5 10 1 4 6 0 7 3 0 4 9 8 6 10 2 5 1 6 8 4 1 5 0 9 7 10 3 2 4 7 9 5 2 6 1 0 8 10 3 10 5 8 0 6 3 7 2 1 9 4 9 0 1 2 3 4 5 6 7 8 10 -- cycle notation: 0: (0) (1 10 5 7 8 3 9 2 6 4) 1: (1) (2 10 6 8 9 4 0 3 7 5) 2: (2) (3 10 7 9 0 5 1 4 8 6) 3: (3) (4 10 8 0 1 6 2 5 9 7) 4: (4) (5 10 9 1 2 7 3 6 0 8) 5: (5) (6 10 0 2 3 8 4 7 1 9) 6: (6) (7 10 1 3 4 9 5 8 2 0) 7: (7) (8 10 2 4 5 0 6 9 3 1) 8: (8) (9 10 3 5 6 1 7 0 4 2) 9: (9) (10 4 6 7 2 8 1 5 3 0) 10: (10) (0 9 8 7 6 5 4 3 2 1) -- autom facts: AUTOM: (0) (1 4 6 2 9 3 8 7 5 10) (0 6 4 9 1 5 2 3 10 8 7) Equational facts: X = (f X X) X = (f (f X Y) Y) (f (f X Y) X) = (f X (f Y X)) 3 = (f (f 3 X) X) X = (f (f X (f X Y)) (f X Y)) X = (f Y (f Y (f X (f Y X)))) X = (g X X) X = (f (f (f X Y) X) (f Y X)) X = (f Y (f X (f Y (f X Y)))) 4 = (f (f 4 X) X) X = (f (f X 8) 8) X = (f (f X 2) 2) X = (f (f X 7) 7) 9 = (f (f 9 X) X) 5 = (f (f 5 X) X) 6 = (f (f 6 X) X) 1 = (f (f 1 X) X) X = (f (f X 4) 4) X = (f (f X 0) 0) 7 = (f (f 7 X) X) --------------------------------------- Model 11_3: 0 8 10 9 3 7 2 1 6 5 4 10 1 8 2 7 0 4 5 9 6 3 9 4 2 10 5 6 8 3 0 7 1 1 6 5 3 10 8 7 9 4 2 0 7 10 0 6 4 3 9 8 5 1 2 6 2 9 0 1 5 10 4 7 3 8 3 0 7 5 2 4 6 10 1 8 9 2 3 4 8 6 9 1 7 10 0 5 4 7 3 1 9 2 5 0 8 10 6 8 5 1 4 0 10 3 6 2 9 7 5 9 6 7 8 1 0 2 3 4 10 -- cycle notation: 0: (0) (1 8 6 2 10 4 3 9 5 7) 1: (1) (2 8 9 6 4 7 5 0 10 3) 2: (2) (3 10 1 4 5 6 8 0 9 7) 3: (3) (4 10 0 1 6 7 9 2 5 8) 4: (4) (5 3 6 9 1 10 2 0 7 8) 5: (5) (6 10 8 7 4 1 2 9 3 0) 6: (6) (7 10 9 8 1 0 3 5 4 2) 7: (7) (8 10 5 9 0 2 4 6 1 3) 8: (8) (9 10 6 5 2 3 1 7 0 4) 9: (9) (10 7 6 3 4 0 8 2 1 5) 10: (10) (0 5 1 9 4 8 3 7 2 6) -- autom facts: AUTOM: (0) (1 8 6 2 10 4 3 9 5 7) (0 7 3 4 2 9 6 5 1 8 10) Equational facts: X = (f X X) X = (f Y (f (f Y X) X)) X = (f (f X (f X Y)) Y) (f X (f Y X)) = (f (f X Y) X) (f X Y) = (f (f Y (f X Y)) X) X = (f (f Y (f Y X)) (f Y X)) X = (f (f Y X) (f X (f X Y))) (f X Y) = (f (f (f Y X) Y) X) (f (f X Y) X) = (f X (f Y X)) (f X Y) = (f (f X Y) (f X Y)) X = (f (f X Y) (f (f X Y) Y)) X = (g X X) (f X (f X Y)) = (f (f X Y) (f Y X)) (f (f X Y) X) = (f Y (f X (f X Y))) (f X (f X Y)) = (f (f (f Y X) X) X) (f (f X Y) Y) = (f (f X (f Y X)) X) (f (f X Y) Y) = (f Y (f (f X Y) X)) (f X (f X Y)) = (f Y (f Y (f X Y))) (f X (f Y X)) = (f Y (f X (f X Y))) (f X (f X Y)) = (f (f Y (f Y X)) Y) --------------------------------------- Model 13_0: 9 6 2 7 11 8 4 0 12 10 1 5 3 12 2 3 6 8 7 10 9 1 0 5 11 4 5 4 10 3 6 2 9 1 11 12 8 7 0 0 7 6 8 5 11 3 10 9 4 12 1 2 2 1 5 12 0 9 8 6 3 7 4 10 11 4 11 8 5 12 1 6 3 10 2 0 9 7 6 12 1 9 10 0 11 7 2 8 3 4 5 10 8 7 11 1 5 2 4 0 3 9 12 6 1 3 4 2 7 6 0 12 5 9 11 8 10 3 5 11 1 9 12 7 2 4 6 10 0 8 11 10 0 4 2 3 12 5 8 1 7 6 9 7 9 12 0 4 10 5 8 6 11 2 3 1 8 0 9 10 3 4 1 11 7 5 6 2 12 -- cycle notation: 0: (0 9 10 1 6 4 11 5 8 12 3 7) (2) 1: (1 2 3 6 10 5 7 9 0 12 4 8) (11) 2: (2 10 8 11 7 1 4 6 9 12 0 5) (3) 3: (3 8 9 4 5 11 1 7 10 12 2 6) (0) 4: (4 0 2 5 9 7 6 8 3 12 11 10) (1) 5: (5 1 11 9 2 8 10 0 4 12 7 3) (6) 6: (6 11 4 10 3 9 8 2 1 12 5 0) (7) 7: (7 4 1 8 0 10 9 3 11 12 6 2) (5) 8: (8 5 6 0 1 3 2 4 7 12 10 11) (9) 9: (9 6 7 2 11 0 3 1 5 12 8 4) (10) 10: (10 7 5 3 4 2 0 11 6 12 9 1) (8) 11: (11 3 0 7 8 6 5 10 2 12 1 9) (4) 12: (12) (0 8 7 11 2 9 5 4 3 10 6 1) -- autom facts: AUTOM: (0 1 6 10 3 4 5 9 2 11 7 8) (12) Equational facts: X = (f (f (f X Y) Y) Y) X = (f (f X 12) X) (f X (f X Y)) = (f Y (f Y X)) 3 = (f X (f 1 X)) (f X (f Y X)) = (f Y (f Y Y)) 1 = (f X (f 7 X)) 11 = (f X (f 5 X)) 2 = (f X (f 4 X)) 6 = (f X (f 8 X)) 8 = (f X (f 2 X)) 10 = (f X (f 0 X)) X = (f Y (f X (f (f Y X) Y))) 7 = (f X (f 9 X)) (f X (f X X)) = (f Y (f X Y)) 4 = (f X (f 6 X)) (f (f X X) Y) = (f (f Y Y) X) 9 = (f X (f 3 X)) (f X 12) = (f (f X X) X) X = (f X (f X (f X 12))) 0 = (f X (f 11 X)) --------------------------------------- Model 16_0: 0 15 1 13 8 7 14 12 2 10 6 9 3 5 11 4 12 1 15 2 14 9 8 0 13 3 11 7 10 4 6 5 7 13 2 15 3 0 10 9 1 14 4 12 8 11 5 6 6 8 14 3 15 4 1 11 10 2 0 5 13 9 12 7 13 7 9 0 4 15 5 2 12 11 3 1 6 14 10 8 11 14 8 10 1 5 15 6 3 13 12 4 2 7 0 9 1 12 0 9 11 2 6 15 7 4 14 13 5 3 8 10 9 2 13 1 10 12 3 7 15 8 5 0 14 6 4 11 5 10 3 14 2 11 13 4 8 15 9 6 1 0 7 12 8 6 11 4 0 3 12 14 5 9 15 10 7 2 1 13 2 9 7 12 5 1 4 13 0 6 10 15 11 8 3 14 4 3 10 8 13 6 2 5 14 1 7 11 15 12 9 0 10 5 4 11 9 14 7 3 6 0 2 8 12 15 13 1 14 11 6 5 12 10 0 8 4 7 1 3 9 13 15 2 15 0 12 7 6 13 11 1 9 5 8 2 4 10 14 3 3 4 5 6 7 8 9 10 11 12 13 14 0 1 2 15 -- cycle notation: 0: (0) (1 15 4 8 2) (3 13 5 7 12) (6 14 11 9 10) 1: (1) (2 15 5 9 3) (4 14 6 8 13) (7 0 12 10 11) 2: (2) (3 15 6 10 4) (5 0 7 9 14) (8 1 13 11 12) 3: (3) (4 15 7 11 5) (6 1 8 10 0) (9 2 14 12 13) 4: (4) (5 15 8 12 6) (7 2 9 11 1) (10 3 0 13 14) 5: (5) (6 15 9 13 7) (8 3 10 12 2) (11 4 1 14 0) 6: (6) (7 15 10 14 8) (9 4 11 13 3) (12 5 2 0 1) 7: (7) (8 15 11 0 9) (10 5 12 14 4) (13 6 3 1 2) 8: (8) (9 15 12 1 10) (11 6 13 0 5) (14 7 4 2 3) 9: (9) (10 15 13 2 11) (12 7 14 1 6) (0 8 5 3 4) 10: (10) (11 15 14 3 12) (13 8 0 2 7) (1 9 6 4 5) 11: (11) (12 15 0 4 13) (14 9 1 3 8) (2 10 7 5 6) 12: (12) (13 15 1 5 14) (0 10 2 4 9) (3 11 8 6 7) 13: (13) (14 15 2 6 0) (1 11 3 5 10) (4 12 9 7 8) 14: (14) (15 3 7 1 0) (2 12 4 6 11) (5 13 10 8 9) 15: (15) (0 3 6 9 12) (1 4 7 10 13) (2 5 8 11 14) -- autom facts: AUTOM: (0) (1 3 14 4 5 9 2 12 6 15 13 11 8 7 10) (0 6) (1 14) (2 10) (3 13) (4 7) (5 9) (8 15) (11 12) Equational facts: X = (f X X) X = (f (f X Y) (f Y X)) X = (f (f (f (f Y X) Y) Y) Y) X = (g X X) (f (f X Y) Y) = (f X (f X Y)) X = (f Y (f X (f (f Y X) Y))) (f X Y) = (f (f X Y) (f X Y)) (f (f X Y) X) = (f X (f Y X)) (f X Y) = (f (f (f (f Y X) Y) Y) X) (f X Y) = (f Y (f Y (f (f X Y) X))) (f X (f 14 X)) = (f (f X 14) X) (f X (f 6 X)) = (f (f X 6) X) (f (f X 8) X) = (f X (f 8 X)) (f (f X 6) X) = (f X (f 6 X)) (f X (f 4 X)) = (f (f X 4) X) (f X (f (f Y X) Y)) = (f (f (f X Y) Y) Y) (f (f X 13) X) = (f X (f 13 X)) (f (f X 12) X) = (f X (f 12 X)) (f (f X 10) X) = (f X (f 10 X)) (f (f (f X Y) X) X) = (f X (f (f Y X) X)) --------------------------------------- Model 16_1: 10 13 2 6 0 11 7 1 4 14 15 9 5 8 3 12 11 7 5 4 12 10 13 15 6 3 1 8 2 9 14 0 5 12 11 3 7 2 0 8 14 4 9 15 10 1 6 13 9 3 1 12 4 8 14 2 0 7 5 10 15 11 13 6 2 0 10 14 13 5 12 9 3 6 8 1 11 15 4 7 4 1 3 11 9 6 15 13 10 5 7 0 14 12 2 8 6 15 14 10 8 4 1 7 11 2 13 12 3 0 5 9 12 5 7 9 11 0 2 14 8 1 3 6 13 4 15 10 0 2 13 8 10 12 5 3 9 15 14 4 7 6 1 11 15 6 8 13 14 1 4 11 7 0 10 5 9 2 12 3 8 14 15 0 6 9 3 5 12 13 2 11 1 10 7 4 13 10 0 15 2 7 11 4 1 8 6 3 12 14 9 5 14 8 6 2 15 3 9 12 5 10 0 7 4 13 11 1 1 4 9 7 3 15 6 10 13 12 11 2 8 5 0 14 7 11 12 1 5 13 10 6 15 9 4 14 0 3 8 2 3 9 4 5 1 14 8 0 2 11 12 13 6 7 10 15 -- cycle notation: 0: (0 10 15 12 5 11 9 14 3 6 7 1 13 8 4) (2) 1: (1 7 15 0 11 8 6 13 9 3 4 12 2 5 10) (14) 2: (2 11 15 13 1 12 10 9 4 7 8 14 6 0 5) (3) 3: (3 12 15 6 14 13 11 10 5 8 0 9 7 2 1) (4) 4: (4 13 15 7 9 6 12 11 1 0 2 10 8 3 14) (5) 5: (5 6 15 8 10 7 13 12 14 2 3 11 0 4 9) (1) 6: (6 1 15 9 2 14 5 4 8 11 12 3 10 13 0) (7) 7: (7 14 15 10 3 9 1 5 0 12 13 4 11 6 2) (8) 8: (8 9 15 11 4 10 14 1 2 13 6 5 12 7 3) (0) 9: (9 0 15 3 13 2 8 7 11 5 1 6 4 14 12) (10) 10: (10 2 15 4 6 3 0 8 12 1 14 7 5 9 13) (11) 11: (11 3 15 5 7 4 2 0 13 14 9 8 1 10 6) (12) 12: (12 4 15 1 8 5 3 2 6 9 10 0 14 11 7) (13) 13: (13 5 15 14 0 1 4 3 7 10 11 2 9 12 8) (6) 14: (14 8 15 2 12 0 7 6 10 4 5 13 3 1 11) (9) 15: (15) (0 3 5 14 10 12 6 8 2 4 1 9 11 13 7) -- autom facts: AUTOM: (0 10 2 11 3 12 4 13 5 6 1 7 14 8 9) (15) Equational facts: 15 = (f X (f X X)) X = (f (f (f X X) X) X) X = (f (f (f X Y) Y) Y) X = (f (f X 15) (f X X)) (f X (f Y X)) = (f Y (f X Y)) X = (f (f X X) (f 15 X)) X = (f X (f (f X X) 15)) (f X (f X Y)) = (f Y (f Y X)) (f X (f Y Y)) = (f Y (f X X)) X = (f Y (f X (f (f Y X) Y))) 1 = (f (f (f 1 X) X) X) (f X 1) = (f 6 (f X X)) (f X 6) = (f 5 (f X X)) 12 = (f (f (f 12 X) X) X) 7 = (f (f (f 7 X) X) X) (f X 10) = (f 0 (f X X)) 4 = (f (f (f 4 X) X) X) (f X 14) = (f 7 (f X X)) (f X Y) = (f (f (f (f X X) Y) Y) X) (f X 3) = (f 11 (f X X)) --------------------------------------- Model 19_0: 17 16 2 15 3 7 10 13 11 18 1 5 8 0 12 6 9 14 4 5 3 12 10 15 9 11 6 13 1 8 4 14 16 18 2 0 17 7 14 0 6 3 16 4 15 11 10 12 18 17 1 9 2 13 7 8 5 12 5 15 7 4 8 9 16 0 11 13 18 6 17 10 3 14 2 1 8 9 13 16 0 5 3 10 15 2 12 14 18 7 6 11 4 1 17 11 1 9 14 8 2 17 4 5 16 3 13 15 18 0 7 12 10 6 13 8 0 17 14 12 5 7 4 3 15 6 10 1 16 9 18 11 2 0 13 14 2 6 15 12 1 18 5 4 16 7 11 17 8 10 9 3 15 12 4 1 18 13 8 17 14 9 0 10 16 2 7 5 6 3 11 6 14 16 5 17 18 4 9 7 15 10 2 11 8 3 0 1 13 12 10 18 7 8 1 6 14 5 17 0 16 11 3 12 9 4 2 15 13 1 7 11 0 9 17 16 15 3 6 2 8 12 4 13 10 5 18 14 16 6 17 12 2 10 18 8 1 4 7 3 9 13 5 14 11 0 15 9 11 8 6 13 3 2 18 12 17 5 0 4 10 14 1 15 7 16 18 4 10 9 7 14 0 3 16 13 6 1 2 5 11 15 17 12 8 4 15 18 11 10 0 13 2 6 8 14 7 17 3 1 12 16 5 9 3 2 5 18 12 11 1 14 8 7 9 15 0 6 4 17 13 16 10 7 10 1 13 11 16 6 12 2 14 17 9 5 15 8 18 3 4 0 2 17 3 4 5 1 7 0 9 10 11 12 13 14 15 16 8 6 18 -- cycle notation: 0: (0 17 14 12 8 11 5 7 13) (1 16 9 18 4 3 15 6 10) (2) 1: (1 3 10 8 13 16 0 5 9) (2 12 14 18 7 6 11 4 15) (17) 2: (2 6 15 13 9 12 1 0 14) (3) (4 16 7 11 17 8 10 18 5) 3: (3 7 16 14 10 13 17 2 15) (4) (5 8 0 12 6 9 11 18 1) 4: (4 0 8 15 11 14 6 3 16) (5) (7 10 12 18 17 1 9 2 13) 5: (5 2 9 16 12 15 7 4 8) (6 17 10 3 14 0 11 13 18) (1) 6: (6 5 12 10 15 9 3 17 11) (7) (8 4 14 16 18 2 0 13 1) 7: (7 1 13 11 16 10 4 6 12) (8 18 3 2 14 17 9 5 15) (0) 8: (8 14 7 17 3 1 12 16 6) (9) (10 0 15 5 13 2 4 18 11) 9: (9 15 0 6 4 17 13 8 7) (10) (11 2 16 1 14 3 5 18 12) 10: (10 16 2 7 5 6 14 9 0) (11) (12 3 8 17 15 4 1 18 13) 11: (11 8 3 0 1 7 15 10 2) (12) (13 4 9 6 16 5 17 18 14) 12: (12 9 4 2 17 0 16 11 3) (13) (14 5 10 7 8 1 6 18 15) 13: (13 10 5 3 6 2 8 12 4) (14) (15 1 11 0 9 17 7 18 16) 14: (14 11 1 4 7 3 9 13 5) (15) (16 17 12 2 10 6 0 18 8) 15: (15 12 17 5 0 4 10 14 1) (16) (18 9 8 6 13 3 11 7 2) 16: (16 13 6 1 2 5 11 15 17) (18 10 9 7 14 4 12 0 3) (8) 17: (17 4 11 9 14 8 2 1 10) (18 0 7 12 5 16 3 13 15) (6) 18: (18) (0 2 3 4 5 1 17 6 7) (8 9 10 11 12 13 14 15 16) -- autom facts: AUTOM: (0 12 2 13 3 14 4 15 5 16 1 8 17 9 6 10 7 11) (18) Equational facts: X = (f (f (f X X) X) X) X = (f (f (f X Y) Y) Y) X = (f (f X X) 18) X = (f Y (f X (f (f Y X) Y))) X = (f X (f X (f (f X X) X))) (f X (f X Y)) = (f Y (f Y X)) X = (f 18 (f (f X X) X)) 18 = (f (f X (f X X)) X) (f 15 X) = (f X (f 14 X)) 4 = (f (f (f 4 X) X) X) (f X X) = (f (f X 6) 8) (f 2 X) = (f X (f 0 X)) (f 1 X) = (f X (f 5 X)) 11 = (f (f (f 11 X) X) X) (f X X) = (f (f X 18) 18) (f X X) = (f (f (f (f X X) Y) Y) Y) (f X X) = (f (f X 10) 17) (f X X) = (f (f X 1) 15) (f 5 X) = (f X (f 4 X)) (f X X) = (f (f X 17) 16) --------------------------------------- Model 19_1: 7 17 2 14 5 15 3 9 1 13 6 10 16 18 8 11 4 0 12 0 6 1 4 14 11 8 16 12 5 9 13 18 7 10 3 2 15 17 12 5 8 11 15 6 16 4 10 0 14 7 2 1 18 9 3 17 13 15 9 12 2 4 3 10 18 17 14 16 5 7 0 13 8 1 11 6 10 0 16 6 17 5 4 11 18 12 15 1 3 8 2 14 9 13 7 2 10 11 0 7 12 6 5 3 18 13 16 14 4 9 17 15 1 8 11 16 17 1 2 8 13 7 6 4 18 14 0 15 5 10 12 3 9 1 13 3 15 0 17 9 14 8 7 5 18 4 2 16 6 11 12 10 14 3 0 18 16 2 12 10 15 9 8 6 13 5 17 1 7 4 11 4 8 15 7 18 1 17 13 11 16 10 9 5 14 6 12 0 2 3 9 2 5 10 8 18 0 12 14 3 1 11 17 6 15 7 13 16 4 17 14 10 3 11 9 18 2 13 15 4 0 1 12 7 16 8 6 5 5 11 7 16 9 4 1 8 0 6 3 17 10 13 12 2 18 14 15 3 18 6 12 1 10 5 0 9 2 7 4 15 11 14 13 17 8 16 18 12 4 5 13 0 11 6 2 10 17 8 9 16 3 15 14 7 1 13 15 18 9 6 14 2 3 7 17 11 12 8 10 1 4 16 5 0 16 1 14 13 10 7 15 17 4 8 12 3 6 9 11 0 5 18 2 6 4 13 8 3 16 7 1 5 11 2 15 12 17 0 18 10 9 14 8 7 9 17 12 13 14 15 16 1 0 2 11 3 4 5 6 10 18 -- cycle notation: 0: (0 7 9 13 18 12 16 4 5 15 11 10 6 3 14 8 1 17) (2) 1: (1 6 8 12 18 17 15 3 4 14 10 9 5 11 13 7 16 2) (0) 2: (2 8 10 14 18 13 1 5 6 16 3 11 7 4 15 9 0 12) (17) 3: (3 2 12 7 18 6 10 16 1 9 14 13 0 15 8 17 11 5) (4) 4: (4 17 13 8 18 7 11 1 0 10 15 14 2 16 9 12 3 6) (5) 5: (5 12 14 9 18 8 3 0 2 11 16 15 17 1 10 13 4 7) (6) 6: (6 13 15 10 18 9 4 2 17 3 1 16 12 0 11 14 5 8) (7) 7: (7 14 16 11 18 10 5 17 12 4 0 1 13 2 3 15 6 9) (8) 8: (8 15 1 3 18 11 6 12 13 5 2 0 14 17 4 16 7 10) (9) 9: (9 16 0 4 18 3 7 13 14 6 17 2 15 12 5 1 8 11) (10) 10: (10 1 2 5 18 4 8 14 15 7 12 17 16 13 6 0 9 3) (11) 11: (11 0 17 6 18 5 9 15 16 8 13 12 1 14 7 2 10 4) (3) 12: (12 10 3 16 18 15 2 7 8 0 5 4 9 6 1 11 17 14) (13) 13: (13 11 4 1 18 16 17 8 9 2 6 5 10 7 0 3 12 15) (14) 14: (14 3 5 0 18 1 12 9 10 17 7 6 11 8 2 4 13 16) (15) 15: (15 4 6 2 18 0 13 10 11 12 8 7 3 9 17 5 14 1) (16) 16: (16 5 7 17 18 2 14 11 3 13 9 8 4 10 12 6 15 0) (1) 17: (17 9 11 15 18 14 0 6 7 1 4 3 8 5 16 10 2 13) (12) 18: (18) (0 8 16 6 14 4 12 11 2 9 1 7 15 5 13 3 17 10) -- autom facts: AUTOM: (0 8 16 6 14 4 12 11 2 9 1 7 15 5 13 3 17 10) (18) Equational facts: X = (f (f (f X X) X) X) X = (f (f (f X Y) Y) Y) X = (f X (f X (f (f X X) X))) (f X (f X Y)) = (f Y (f Y X)) X = (f Y (f X (f (f Y X) Y))) 13 = (f (f (f 13 X) X) X) 11 = (f (f (f 11 X) X) X) 18 = (f X (f X (f X (f X X)))) 10 = (f (f (f 10 X) X) X) 6 = (f (f (f 6 X) X) X) 17 = (f (f (f 17 X) X) X) 5 = (f (f (f 5 X) X) X) 8 = (f (f (f 8 X) X) X) 3 = (f (f (f 3 X) X) X) (f (f X X) X) = (f X (f 18 X)) 12 = (f (f (f 12 X) X) X) (f X X) = (f 18 (f (f X X) X)) 1 = (f (f (f 1 X) X) X) (f X X) = (f Y (f (f (f Y X) X) Y)) 14 = (f (f (f 14 X) X) X) --------------------------------------- Model 21_0: 0 3 20 1 19 14 17 15 18 16 12 13 10 11 5 7 9 6 8 4 2 20 1 3 2 17 11 14 16 19 15 13 5 18 10 6 9 7 4 12 8 0 1 0 2 20 8 19 9 11 4 6 15 7 16 18 17 10 12 14 13 5 3 2 20 0 3 14 17 16 19 13 12 18 15 9 8 4 11 6 5 10 7 1 11 15 16 10 4 20 7 6 12 17 3 0 8 19 18 1 2 9 14 13 5 16 12 15 8 7 5 20 4 3 14 19 18 1 17 9 2 0 13 11 10 6 10 8 13 11 5 4 6 20 1 18 0 3 17 2 19 16 15 12 9 14 7 18 10 17 9 20 6 5 7 15 3 1 14 19 16 11 8 13 2 0 12 4 7 14 12 17 16 13 19 0 8 20 11 10 2 5 1 18 4 3 15 6 9 5 4 18 19 1 0 13 12 11 9 20 8 7 6 16 17 14 15 2 3 10 17 16 5 14 18 2 12 13 9 8 10 20 6 7 3 19 1 0 4 15 11 19 18 14 16 13 12 15 17 20 10 9 11 5 4 2 6 3 7 1 0 8 6 11 4 7 2 18 0 3 16 19 17 1 12 20 15 14 8 10 5 9 13 4 7 9 5 0 3 18 1 17 2 16 19 15 13 20 12 10 8 6 11 14 9 19 7 18 10 16 8 2 6 0 4 17 13 12 14 20 5 11 3 1 15 8 17 19 6 9 10 3 18 0 4 5 16 20 14 13 15 11 1 7 2 12 14 13 8 15 12 9 11 10 2 5 7 6 4 1 0 3 16 20 19 18 17 12 9 11 13 15 8 10 14 5 1 6 2 0 3 7 4 19 17 20 16 18 15 5 6 4 3 1 2 8 7 13 14 12 11 9 10 0 17 16 18 20 19 13 6 10 12 11 15 1 9 14 7 2 4 3 0 8 5 20 18 17 19 16 3 2 1 0 6 7 4 5 10 11 8 9 14 15 12 13 18 19 16 17 20 -- cycle notation: 0: (0) (1 3) (2 20) (4 19) (5 14) (6 17) (7 15) (8 18) (9 16) (10 12) (11 13) 1: (1) (2 3) (4 17) (5 11) (6 14) (7 16) (8 19) (9 15) (10 13) (12 18) (20 0) 2: (2) (3 20) (4 8) (5 19) (6 9) (7 11) (10 15) (12 16) (13 18) (14 17) (0 1) 3: (3) (4 14) (5 17) (6 16) (7 19) (8 13) (9 12) (10 18) (11 15) (20 1) (0 2) 4: (4) (5 20) (6 7) (8 12) (9 17) (10 3) (11 0) (13 19) (14 18) (15 1) (16 2) 5: (5) (6 20) (7 4) (8 3) (9 14) (10 19) (11 18) (12 1) (13 17) (15 2) (16 0) 6: (6) (7 20) (8 1) (9 18) (10 0) (11 3) (12 17) (13 2) (14 19) (15 16) (4 5) 7: (7) (8 15) (9 3) (10 1) (11 14) (12 19) (13 16) (17 2) (18 0) (20 4) (5 6) 8: (8) (9 20) (10 11) (12 2) (13 5) (14 1) (15 18) (16 4) (17 3) (19 6) (0 7) 9: (9) (10 20) (11 8) (12 7) (13 6) (14 16) (15 17) (18 2) (19 3) (0 5) (1 4) 10: (10) (11 20) (12 6) (13 7) (14 3) (15 19) (16 1) (17 0) (18 4) (2 5) (8 9) 11: (11) (12 5) (13 4) (14 2) (15 6) (16 3) (17 7) (18 1) (19 0) (20 8) (9 10) 12: (12) (13 20) (14 15) (16 8) (17 10) (18 5) (19 9) (0 6) (1 11) (2 4) (3 7) 13: (13) (14 20) (15 12) (16 10) (17 8) (18 6) (19 11) (0 4) (1 7) (2 9) (3 5) 14: (14) (15 20) (16 5) (17 11) (18 3) (19 1) (0 9) (2 7) (4 10) (6 8) (12 13) 15: (15) (16 11) (17 1) (18 7) (19 2) (20 12) (0 8) (3 6) (4 9) (5 10) (13 14) 16: (16) (17 20) (18 19) (0 14) (1 13) (2 8) (3 15) (4 12) (5 9) (6 11) (7 10) 17: (17) (18 20) (19 16) (0 12) (1 9) (2 11) (3 13) (4 15) (5 8) (6 10) (7 14) 18: (18) (19 20) (0 15) (1 5) (2 6) (3 4) (7 8) (9 13) (10 14) (11 12) (16 17) 19: (19) (20 16) (0 13) (1 6) (2 10) (3 12) (4 11) (5 15) (7 9) (8 14) (17 18) 20: (20) (0 3) (1 2) (4 6) (5 7) (8 10) (9 11) (12 14) (13 15) (16 18) (17 19) -- autom facts: AUTOM: (0 10 20 18 15 5 6 9 17 8 19 7 2 4 13 1 3 14 12 11 16) Equational facts: X = (f X X) X = (f Y (f Y X)) X = (f (f (f Y X) Y) Y) (f X Y) = (f (f Y X) X) X = (f (f Y X) (f X Y)) X = (f (f (f X Y) X) Y) X = (f 11 (f 11 X)) X = (f 16 (f 16 X)) 20 = (f X (f X 20)) 17 = (f X (f X 17)) 9 = (f X (f X 9)) (f X Y) = (f Y (f (f X Y) X)) X = (f 1 (f 1 X)) 10 = (f X (f X 10)) X = (f 10 (f 10 X)) 0 = (f X (f X 0)) (f (f X Y) X) = (f X (f Y X)) 1 = (f X (f X 1)) X = (f 3 (f 3 X)) X = (f 2 (f 2 X)) --------------------------------------- Model 25_0: 0 3 24 1 21 17 20 19 22 18 14 15 16 23 10 11 12 5 9 7 6 4 8 13 2 24 1 3 2 15 20 23 14 18 21 16 17 22 19 7 4 10 11 8 13 5 9 12 6 0 1 0 2 24 9 8 22 16 5 4 15 13 23 11 18 10 7 20 14 21 17 19 6 12 3 2 24 0 3 13 18 9 23 14 6 22 21 19 4 8 17 20 15 5 12 16 11 10 7 1 16 8 17 10 4 24 7 6 1 20 3 19 21 22 23 18 0 2 15 11 9 12 13 14 5 14 19 23 11 7 5 24 4 12 16 17 3 8 20 0 22 9 10 21 1 13 18 15 2 6 15 10 18 19 5 4 6 24 13 12 1 20 9 8 22 0 23 21 2 3 11 17 14 16 7 22 21 11 17 24 6 5 7 19 14 12 2 10 16 9 23 13 3 20 8 18 1 0 15 4 7 15 12 20 18 23 17 0 8 24 11 10 2 21 16 1 14 6 4 22 3 13 19 5 9 13 7 20 12 17 15 19 1 11 9 24 8 3 0 21 5 22 4 23 6 2 14 16 18 10 5 23 19 13 22 0 16 20 9 8 10 24 18 3 17 21 6 14 12 2 7 15 4 1 11 6 22 16 18 23 21 0 13 24 10 9 11 17 7 19 20 2 12 3 14 15 5 1 4 8 4 11 5 6 0 2 3 18 23 19 20 1 12 24 15 14 21 22 7 9 10 16 17 8 13 18 5 7 22 10 1 21 2 17 23 4 16 15 13 24 12 11 8 0 20 19 6 3 9 14 17 9 6 16 11 10 2 21 20 1 5 4 13 12 14 24 3 0 22 23 8 7 18 19 15 20 18 21 7 8 16 11 3 4 22 19 6 24 14 13 15 5 23 1 10 0 2 9 17 12 21 6 13 8 12 22 1 11 3 15 23 7 4 2 20 9 16 24 19 18 14 0 5 10 17 10 12 9 23 20 14 13 15 21 2 0 22 1 6 5 7 19 17 24 16 4 8 11 3 18 23 4 22 21 1 11 14 10 15 13 7 5 20 9 6 8 17 16 18 24 12 3 2 0 19 8 20 15 9 14 13 12 22 0 3 21 23 6 5 4 2 24 18 17 19 1 10 7 11 16 11 13 4 14 2 19 15 12 16 17 18 0 7 1 3 6 8 9 10 5 20 24 23 22 21 12 14 10 5 16 3 8 9 6 7 2 18 0 17 1 19 4 13 11 15 23 21 24 20 22 19 17 14 4 3 9 18 8 7 5 13 12 11 10 2 16 15 1 6 0 21 20 22 24 23 9 16 8 15 19 12 10 17 2 0 6 14 5 18 11 3 1 7 13 4 24 22 21 23 20 3 2 1 0 6 7 4 5 10 11 8 9 14 15 12 13 18 19 16 17 22 23 20 21 24 -- cycle notation: 0: (0) (1 3) (2 24) (4 21) (5 17) (6 20) (7 19) (8 22) (9 18) (10 14) (11 15) (12 16) (13 23) 1: (1) (2 3) (4 15) (5 20) (6 23) (7 14) (8 18) (9 21) (10 16) (11 17) (12 22) (13 19) (24 0) 2: (2) (3 24) (4 9) (5 8) (6 22) (7 16) (10 15) (11 13) (12 23) (14 18) (17 20) (19 21) (0 1) 3: (3) (4 13) (5 18) (6 9) (7 23) (8 14) (10 22) (11 21) (12 19) (15 17) (16 20) (24 1) (0 2) 4: (4) (5 24) (6 7) (8 1) (9 20) (10 3) (11 19) (12 21) (13 22) (14 23) (15 18) (16 0) (17 2) 5: (5) (6 24) (7 4) (8 12) (9 16) (10 17) (11 3) (13 20) (14 0) (15 22) (18 21) (19 1) (23 2) 6: (6) (7 24) (8 13) (9 12) (10 1) (11 20) (14 22) (15 0) (16 23) (17 21) (18 2) (19 3) (4 5) 7: (7) (8 19) (9 14) (10 12) (11 2) (13 16) (15 23) (17 3) (18 20) (21 1) (22 0) (24 4) (5 6) 8: (8) (9 24) (10 11) (12 2) (13 21) (14 16) (15 1) (17 6) (18 4) (19 22) (20 3) (23 5) (0 7) 9: (9) (10 24) (11 8) (12 3) (13 0) (14 21) (15 5) (16 22) (17 4) (18 23) (19 6) (20 2) (1 7) 10: (10) (11 24) (12 18) (13 3) (14 17) (15 21) (16 6) (19 2) (20 7) (22 4) (23 1) (0 5) (8 9) 11: (11) (12 17) (13 7) (14 19) (15 20) (16 2) (18 3) (21 5) (22 1) (23 4) (24 8) (0 6) (9 10) 12: (12) (13 24) (14 15) (16 21) (17 22) (18 7) (19 9) (20 10) (23 8) (0 4) (1 11) (2 5) (3 6) 13: (13) (14 24) (15 12) (16 11) (17 8) (18 0) (19 20) (21 6) (22 3) (23 9) (1 5) (2 7) (4 10) 14: (14) (15 24) (16 3) (17 0) (18 22) (19 23) (20 8) (21 7) (1 9) (2 6) (4 11) (5 10) (12 13) 15: (15) (16 5) (17 23) (18 1) (19 10) (20 0) (21 2) (22 9) (24 12) (3 7) (4 8) (6 11) (13 14) 16: (16) (17 24) (18 19) (20 14) (21 0) (22 5) (23 10) (1 6) (2 13) (3 8) (4 12) (7 11) (9 15) 17: (17) (18 24) (19 16) (20 4) (21 8) (22 11) (23 3) (0 10) (1 12) (2 9) (5 14) (6 13) (7 15) 18: (18) (19 24) (20 12) (21 3) (22 2) (23 0) (1 4) (5 11) (6 14) (7 10) (8 15) (9 13) (16 17) 19: (19) (20 1) (21 10) (22 7) (23 11) (24 16) (0 8) (2 15) (3 9) (4 14) (5 13) (6 12) (17 18) 20: (20) (21 24) (22 23) (0 11) (1 13) (2 4) (3 14) (5 19) (6 15) (7 12) (8 16) (9 17) (10 18) 21: (21) (22 24) (23 20) (0 12) (1 14) (2 10) (3 5) (4 16) (6 8) (7 9) (11 18) (13 17) (15 19) 22: (22) (23 24) (0 19) (1 17) (2 14) (3 4) (5 9) (6 18) (7 8) (10 13) (11 12) (15 16) (20 21) 23: (23) (24 20) (0 9) (1 16) (2 8) (3 15) (4 19) (5 12) (6 10) (7 17) (11 14) (13 18) (21 22) 24: (24) (0 3) (1 2) (4 6) (5 7) (8 10) (9 11) (12 14) (13 15) (16 18) (17 19) (20 22) (21 23) -- autom facts: AUTOM: (0) (1 14) (2 5) (3 10) (4) (6 20) (7 9) (8 23) (11 15) (12) (13 22) (16) (17 24) (18 19) (21) (0 1 9 19 2 14 12 10 22 24 7 3 21 6 15 18 13 20 4 23 5 17 11 8) (16) Equational facts: X = (f X X) X = (f Y (f Y X)) X = (f (f (f X Y) X) Y) X = (f (f Y X) (f X Y)) (f X Y) = (f (f Y X) X) X = (f (f (f Y X) Y) Y) X = (f 12 (f 12 X)) X = (f 18 (f 18 X)) X = (g X X) 10 = (f X (f X 10)) (f (f X Y) X) = (f X (f Y X)) 12 = (f X (f X 12)) X = (f 6 (f 6 X)) X = (f 21 (f 21 X)) X = (f 14 (f 14 X)) X = (f 10 (f 10 X)) (f X Y) = (f Y (f (f Y X) Y)) X = (f 17 (f 17 X)) X = (f 16 (f 16 X)) X = (f 3 (f 3 X)) --------------------------------------- Model 25_1: 0 3 24 1 23 20 13 22 19 14 17 16 21 6 9 18 11 10 15 8 5 12 7 4 2 24 1 3 2 19 16 22 11 13 12 23 7 9 8 17 21 5 14 20 4 18 15 6 10 0 1 0 2 24 11 21 8 18 6 16 14 4 23 19 10 22 9 20 7 13 17 5 15 12 3 2 24 0 3 13 15 9 12 17 6 22 23 7 4 19 5 20 8 21 14 16 18 10 11 1 18 9 20 10 4 24 7 6 16 1 3 17 19 22 21 23 8 11 0 12 2 14 13 15 5 9 23 19 8 7 5 24 4 3 0 16 18 22 21 20 17 10 15 11 2 14 13 12 1 6 16 17 12 18 5 4 6 24 23 21 15 13 2 11 22 10 0 1 3 20 19 9 14 8 7 8 21 14 16 24 6 5 7 0 23 18 15 20 17 2 11 3 13 10 22 12 1 19 9 4 22 20 23 15 14 17 12 19 8 24 11 10 6 18 4 3 21 5 13 7 1 16 0 2 9 20 19 15 21 12 14 18 13 11 9 24 8 4 7 5 2 22 23 6 1 0 3 16 17 10 21 5 7 13 22 1 20 2 9 8 10 24 17 3 18 19 23 12 14 15 6 0 4 16 11 6 15 17 14 20 22 0 21 24 10 9 11 18 16 3 1 13 2 12 23 4 7 5 19 8 10 4 8 20 1 11 23 16 2 19 0 5 12 24 15 14 7 21 22 9 3 17 18 6 13 11 18 5 22 10 2 16 23 20 17 4 0 15 13 24 12 6 9 1 21 8 19 3 7 14 5 6 18 23 16 0 1 10 21 20 7 19 13 12 14 24 4 22 2 11 9 8 17 3 15 4 7 16 17 0 8 19 1 5 22 20 21 24 14 13 15 2 3 23 6 10 11 9 18 12 13 10 22 12 21 23 11 20 14 15 1 6 3 0 8 9 16 24 19 18 7 4 2 5 17 12 22 4 5 2 3 14 9 15 7 21 20 0 23 6 8 19 17 24 16 11 10 1 13 18 23 8 10 9 15 12 21 14 1 3 2 22 5 20 7 4 17 16 18 24 13 6 11 0 19 7 12 21 11 9 13 10 0 22 4 6 3 1 5 23 20 24 18 17 19 15 2 8 14 16 14 13 11 7 17 9 15 3 18 5 19 2 16 1 0 6 12 4 8 10 20 24 23 22 21 17 11 13 6 8 19 3 15 4 18 12 1 10 2 16 7 14 0 9 5 23 21 24 20 22 19 14 9 4 3 18 17 8 7 2 13 12 11 10 1 16 15 6 5 0 21 20 22 24 23 15 16 6 19 18 10 2 17 12 13 5 14 8 9 11 0 1 7 4 3 24 22 21 23 20 3 2 1 0 6 7 4 5 10 11 8 9 14 15 12 13 18 19 16 17 22 23 20 21 24 -- cycle notation: 0: (0) (1 3) (2 24) (4 23) (5 20) (6 13) (7 22) (8 19) (9 14) (10 17) (11 16) (12 21) (15 18) 1: (1) (2 3) (4 19) (5 16) (6 22) (7 11) (8 13) (9 12) (10 23) (14 17) (15 21) (18 20) (24 0) 2: (2) (3 24) (4 11) (5 21) (6 8) (7 18) (9 16) (10 14) (12 23) (13 19) (15 22) (17 20) (0 1) 3: (3) (4 13) (5 15) (6 9) (7 12) (8 17) (10 22) (11 23) (14 19) (16 20) (18 21) (24 1) (0 2) 4: (4) (5 24) (6 7) (8 16) (9 1) (10 3) (11 17) (12 19) (13 22) (14 21) (15 23) (18 0) (20 2) 5: (5) (6 24) (7 4) (8 3) (9 0) (10 16) (11 18) (12 22) (13 21) (14 20) (15 17) (19 2) (23 1) 6: (6) (7 24) (8 23) (9 21) (10 15) (11 13) (12 2) (14 22) (16 0) (17 1) (18 3) (19 20) (4 5) 7: (7) (8 0) (9 23) (10 18) (11 15) (12 20) (13 17) (14 2) (16 3) (19 22) (21 1) (24 4) (5 6) 8: (8) (9 24) (10 11) (12 6) (13 18) (14 4) (15 3) (16 21) (17 5) (19 7) (20 1) (22 0) (23 2) 9: (9) (10 24) (11 8) (12 4) (13 7) (14 5) (15 2) (16 22) (17 23) (18 6) (19 1) (20 0) (21 3) 10: (10) (11 24) (12 17) (13 3) (14 18) (15 19) (16 23) (20 6) (21 0) (22 4) (1 5) (2 7) (8 9) 11: (11) (12 18) (13 16) (14 3) (15 1) (17 2) (19 23) (20 4) (21 7) (22 5) (24 8) (0 6) (9 10) 12: (12) (13 24) (14 15) (16 7) (17 21) (18 22) (19 9) (20 3) (23 6) (0 10) (1 4) (2 8) (5 11) 13: (13) (14 24) (15 12) (16 6) (17 9) (18 1) (19 21) (20 8) (22 3) (23 7) (0 11) (2 5) (4 10) 14: (14) (15 24) (16 4) (17 22) (18 2) (19 11) (20 9) (21 8) (23 3) (0 5) (1 6) (7 10) (12 13) 15: (15) (16 2) (17 3) (18 23) (19 6) (20 10) (21 11) (22 9) (24 12) (0 4) (1 7) (5 8) (13 14) 16: (16) (17 24) (18 19) (20 7) (21 4) (22 2) (23 5) (0 13) (1 10) (3 12) (6 11) (8 14) (9 15) 17: (17) (18 24) (19 16) (20 11) (21 10) (22 1) (23 13) (0 12) (2 4) (3 5) (6 14) (7 9) (8 15) 18: (18) (19 24) (20 13) (21 6) (22 11) (23 0) (1 8) (2 10) (3 9) (4 15) (5 12) (7 14) (16 17) 19: (19) (20 15) (21 2) (22 8) (23 14) (24 16) (0 7) (1 12) (3 11) (4 9) (5 13) (6 10) (17 18) 20: (20) (21 24) (22 23) (0 14) (1 13) (2 11) (3 7) (4 17) (5 9) (6 15) (8 18) (10 19) (12 16) 21: (21) (22 24) (23 20) (0 17) (1 11) (2 13) (3 6) (4 8) (5 19) (7 15) (9 18) (10 12) (14 16) 22: (22) (23 24) (0 19) (1 14) (2 9) (3 4) (5 18) (6 17) (7 8) (10 13) (11 12) (15 16) (20 21) 23: (23) (24 20) (0 15) (1 16) (2 6) (3 19) (4 18) (5 10) (7 17) (8 12) (9 13) (11 14) (21 22) 24: (24) (0 3) (1 2) (4 6) (5 7) (8 10) (9 11) (12 14) (13 15) (16 18) (17 19) (20 22) (21 23) -- autom facts: AUTOM: (0) (1 3) (2 24) (4 14) (5 18) (6 10) (7) (8) (9 23) (11 12) (13 17) (15 20) (16 21) (19) (22) (0 16 14 23 6 21 19 12 18 13 4 11 8 3 2 9 5 1 22 20 10 17 24 15) (7) Equational facts: X = (f X X) X = (f Y (f Y X)) X = (f (f Y X) (f X Y)) (f X Y) = (f (f Y X) X) X = (f (f (f X Y) X) Y) X = (f (f (f Y X) Y) Y) X = (f 13 (f 13 X)) X = (g X X) X = (f 22 (f 22 X)) X = (f 2 (f 2 X)) X = (f 12 (f 12 X)) X = (f 16 (f 16 X)) X = (f 17 (f 17 X)) (f X Y) = (f Y (f (f Y X) Y)) 18 = (f X (f X 18)) X = (f 11 (f 11 X)) 13 = (f X (f X 13)) 10 = (f X (f X 10)) X = (f 3 (f 3 X)) X = (f 1 (f 1 X)) --------------------------------------- Model 25_2: 0 3 24 1 14 20 16 9 23 7 12 17 10 19 4 22 6 11 21 13 5 18 15 8 2 24 1 3 2 18 11 12 22 14 19 21 5 6 20 8 17 23 15 4 9 13 10 7 16 0 1 0 2 24 23 19 8 13 6 15 16 22 18 7 21 9 10 20 12 5 17 14 11 4 3 2 24 0 3 10 15 21 17 18 20 4 13 23 11 16 5 14 7 8 22 9 6 19 12 1 17 13 9 19 4 24 7 6 21 2 22 14 16 1 11 23 12 0 20 3 18 8 10 15 5 10 23 14 8 7 5 24 4 3 22 0 16 20 17 2 18 11 13 15 21 12 19 9 1 6 15 19 20 13 5 4 6 24 17 12 23 21 9 3 18 0 22 8 14 1 2 11 16 10 7 21 8 16 23 24 6 5 7 1 18 13 20 17 10 22 19 2 12 9 15 11 0 14 3 4 13 22 17 15 16 18 20 14 8 24 11 10 21 0 7 3 4 2 5 23 6 12 1 19 9 18 6 23 16 15 17 1 21 11 9 24 8 19 22 20 4 3 5 0 12 14 7 13 2 10 20 15 7 22 19 12 18 2 9 8 10 24 5 16 23 1 13 21 6 4 0 17 3 14 11 4 16 12 6 0 23 3 19 24 10 9 11 2 21 17 20 1 14 22 7 15 13 18 5 8 5 9 22 7 8 0 19 3 4 1 20 18 12 24 15 14 21 23 11 6 10 16 2 17 13 23 18 10 21 20 9 11 16 19 5 2 6 15 13 24 12 7 22 1 8 4 3 17 0 14 11 7 19 9 17 21 10 1 22 3 6 0 13 12 14 24 20 4 23 2 16 5 8 18 15 16 21 4 18 2 8 22 11 5 23 17 7 24 14 13 15 0 10 3 20 19 1 6 9 12 22 5 13 20 21 1 15 10 12 14 7 23 8 2 9 6 16 24 19 18 3 4 0 11 17 14 10 6 12 11 22 2 23 20 13 1 4 3 9 0 21 19 17 24 16 8 15 5 7 18 7 20 11 5 13 3 23 0 15 21 14 2 22 4 10 8 17 16 18 24 1 9 12 6 19 8 12 21 10 22 14 9 20 0 6 3 15 1 23 5 11 24 18 17 19 7 2 4 13 16 12 4 8 14 1 10 17 15 2 16 5 19 0 18 3 7 9 6 13 11 20 24 23 22 21 9 17 5 11 12 2 13 18 16 0 15 3 4 6 19 10 8 1 7 14 23 21 24 20 22 6 14 18 4 3 13 0 8 7 17 19 12 11 5 1 16 15 9 2 10 21 20 22 24 23 19 11 15 17 9 16 14 12 13 4 18 1 7 8 6 2 5 3 10 0 24 22 21 23 20 3 2 1 0 6 7 4 5 10 11 8 9 14 15 12 13 18 19 16 17 22 23 20 21 24 -- cycle notation: 0: (0) (1 3) (2 24) (4 14) (5 20) (6 16) (7 9) (8 23) (10 12) (11 17) (13 19) (15 22) (18 21) 1: (1) (2 3) (4 18) (5 11) (6 12) (7 22) (8 14) (9 19) (10 21) (13 20) (15 17) (16 23) (24 0) 2: (2) (3 24) (4 23) (5 19) (6 8) (7 13) (9 15) (10 16) (11 22) (12 18) (14 21) (17 20) (0 1) 3: (3) (4 10) (5 15) (6 21) (7 17) (8 18) (9 20) (11 13) (12 23) (14 16) (19 22) (24 1) (0 2) 4: (4) (5 24) (6 7) (8 21) (9 2) (10 22) (11 14) (12 16) (13 1) (15 23) (17 0) (18 20) (19 3) 5: (5) (6 24) (7 4) (8 3) (9 22) (10 0) (11 16) (12 20) (13 17) (14 2) (15 18) (19 21) (23 1) 6: (6) (7 24) (8 17) (9 12) (10 23) (11 21) (13 3) (14 18) (15 0) (16 22) (19 1) (20 2) (4 5) 7: (7) (8 1) (9 18) (10 13) (11 20) (12 17) (14 22) (15 19) (16 2) (21 0) (23 3) (24 4) (5 6) 8: (8) (9 24) (10 11) (12 21) (13 0) (14 7) (15 3) (16 4) (17 2) (18 5) (19 23) (20 6) (22 1) 9: (9) (10 24) (11 8) (12 19) (13 22) (14 20) (15 4) (16 3) (17 5) (18 0) (21 7) (23 2) (1 6) 10: (10) (11 24) (12 5) (13 16) (14 23) (15 1) (17 21) (18 6) (19 4) (20 0) (22 3) (2 7) (8 9) 11: (11) (12 2) (13 21) (14 17) (15 20) (16 1) (18 22) (19 7) (23 5) (24 8) (0 4) (3 6) (9 10) 12: (12) (13 24) (14 15) (16 21) (17 23) (18 11) (19 6) (20 10) (22 2) (0 5) (1 9) (3 7) (4 8) 13: (13) (14 24) (15 12) (16 7) (17 22) (18 1) (19 8) (20 4) (21 3) (23 0) (2 10) (5 9) (6 11) 14: (14) (15 24) (16 20) (17 4) (18 23) (19 2) (21 5) (22 8) (0 11) (1 7) (3 9) (6 10) (12 13) 15: (15) (16 0) (17 10) (18 3) (19 20) (21 1) (22 6) (23 9) (24 12) (2 4) (5 8) (7 11) (13 14) 16: (16) (17 24) (18 19) (20 3) (21 4) (22 0) (23 11) (1 5) (2 13) (6 15) (7 10) (8 12) (9 14) 17: (17) (18 24) (19 16) (20 8) (21 15) (22 5) (23 7) (0 14) (1 10) (2 6) (3 12) (4 11) (9 13) 18: (18) (19 24) (20 1) (21 9) (22 12) (23 6) (0 7) (2 11) (3 5) (4 13) (8 15) (10 14) (16 17) 19: (19) (20 7) (21 2) (22 4) (23 13) (24 16) (0 8) (1 12) (3 10) (5 14) (6 9) (11 15) (17 18) 20: (20) (21 24) (22 23) (0 12) (1 4) (2 8) (3 14) (5 10) (6 17) (7 15) (9 16) (11 19) (13 18) 21: (21) (22 24) (23 20) (0 9) (1 17) (2 5) (3 11) (4 12) (6 13) (7 18) (8 16) (10 15) (14 19) 22: (22) (23 24) (0 6) (1 14) (2 18) (3 4) (5 13) (7 8) (9 17) (10 19) (11 12) (15 16) (20 21) 23: (23) (24 20) (0 19) (1 11) (2 15) (3 17) (4 9) (5 16) (6 14) (7 12) (8 13) (10 18) (21 22) 24: (24) (0 3) (1 2) (4 6) (5 7) (8 10) (9 11) (12 14) (13 15) (16 18) (17 19) (20 22) (21 23) -- autom facts: AUTOM: (0 16 21 10 5 23 24 9 13 19 18 7 2 14 6 4 15 12 1 20 11 22 8 17) (3) (0 20 10 12) (1 14 22 7) (2 9 4 23) (3) (5) (6 11 21 13) (8) (15) (16 19 17 24) (18) Equational facts: X = (f X X) X = (f Y (f Y X)) (f X Y) = (f (f Y X) X) X = (f (f (f X Y) X) Y) X = (f (f (f Y X) Y) Y) X = (f (f Y X) (f X Y)) 0 = (f X (f X 0)) 8 = (f X (f X 8)) 18 = (f X (f X 18)) X = (f 17 (f 17 X)) 14 = (f X (f X 14)) 19 = (f X (f X 19)) X = (f 2 (f 2 X)) (f X Y) = (f Y (f (f Y X) Y)) 16 = (f X (f X 16)) (f (f X Y) X) = (f (f Y X) Y) X = (f 13 (f 13 X)) 9 = (f X (f X 9)) X = (g X X) X = (f 21 (f 21 X)) --------------------------------------- Model 25_3: 0 3 24 1 10 15 21 17 18 20 4 13 23 11 16 5 14 7 8 22 9 6 19 12 2 24 1 3 2 14 20 16 9 23 7 12 17 10 19 4 22 6 11 21 13 5 18 15 8 0 1 0 2 24 18 11 12 22 14 19 21 5 6 20 8 17 23 15 4 9 13 10 7 16 3 2 24 0 3 23 19 8 13 6 15 16 22 18 7 21 9 10 20 12 5 17 14 11 4 1 22 17 13 9 4 24 7 6 21 3 19 14 16 2 11 23 12 1 20 10 18 8 0 15 5 18 10 23 14 7 5 24 4 15 22 1 16 20 17 3 8 11 13 0 21 12 19 9 2 6 11 15 19 20 5 4 6 24 17 12 23 0 9 21 18 1 22 8 14 2 3 13 16 10 7 12 21 8 16 24 6 5 7 2 18 13 20 0 10 22 19 3 23 9 15 11 1 14 17 4 5 13 22 17 16 0 20 14 8 24 11 10 21 1 7 18 4 3 15 23 6 12 2 19 9 14 18 6 23 15 17 2 21 11 9 24 8 19 22 0 4 20 5 1 12 16 7 13 3 10 19 20 15 7 22 12 18 3 9 8 10 24 5 16 23 2 13 21 6 0 1 17 4 14 11 21 4 16 12 1 23 13 19 24 10 9 11 3 6 17 20 2 14 22 7 15 0 18 5 8 17 5 9 22 8 1 19 23 4 2 20 18 12 24 15 14 21 0 11 6 10 16 3 7 13 6 23 18 10 20 9 0 16 19 5 3 21 15 13 24 12 7 22 2 8 4 11 17 1 14 20 11 7 19 17 21 10 2 22 16 6 1 13 12 14 24 9 4 23 3 0 5 8 18 15 8 16 21 4 3 18 22 11 0 23 17 7 24 14 13 15 1 10 5 20 19 2 6 9 12 9 22 5 13 21 2 15 10 12 0 7 23 8 3 20 6 16 24 19 18 14 4 1 11 17 23 14 10 6 11 22 3 12 20 13 2 4 7 9 1 21 19 17 24 16 8 15 5 0 18 15 7 20 11 13 8 23 1 5 21 14 3 22 4 10 0 17 16 18 24 2 9 12 6 19 4 8 12 21 0 14 9 20 1 6 22 15 2 23 5 11 24 18 17 19 7 3 10 13 16 16 12 4 8 2 10 17 15 3 14 5 19 1 18 9 7 0 6 13 11 20 24 23 22 21 13 9 17 5 12 3 11 18 16 1 15 6 4 0 19 10 8 2 7 14 23 21 24 20 22 10 6 14 18 19 13 1 8 7 17 0 12 11 5 2 16 15 9 3 4 21 20 22 24 23 7 19 11 15 9 16 14 0 13 4 18 2 17 8 6 3 5 12 10 1 24 22 21 23 20 3 2 1 0 6 7 4 5 10 11 8 9 14 15 12 13 18 19 16 17 22 23 20 21 24 -- cycle notation: 0: (0) (1 3) (2 24) (4 10) (5 15) (6 21) (7 17) (8 18) (9 20) (11 13) (12 23) (14 16) (19 22) 1: (1) (2 3) (4 14) (5 20) (6 16) (7 9) (8 23) (10 12) (11 17) (13 19) (15 22) (18 21) (24 0) 2: (2) (3 24) (4 18) (5 11) (6 12) (7 22) (8 14) (9 19) (10 21) (13 20) (15 17) (16 23) (0 1) 3: (3) (4 23) (5 19) (6 8) (7 13) (9 15) (10 16) (11 22) (12 18) (14 21) (17 20) (24 1) (0 2) 4: (4) (5 24) (6 7) (8 21) (9 3) (10 19) (11 14) (12 16) (13 2) (15 23) (17 1) (18 20) (22 0) 5: (5) (6 24) (7 4) (8 15) (9 22) (10 1) (11 16) (12 20) (13 17) (14 3) (18 0) (19 21) (23 2) 6: (6) (7 24) (8 17) (9 12) (10 23) (11 0) (13 21) (14 18) (15 1) (16 22) (19 2) (20 3) (4 5) 7: (7) (8 2) (9 18) (10 13) (11 20) (12 0) (14 22) (15 19) (16 3) (17 23) (21 1) (24 4) (5 6) 8: (8) (9 24) (10 11) (12 21) (13 1) (14 7) (15 18) (16 4) (17 3) (19 23) (20 6) (22 2) (0 5) 9: (9) (10 24) (11 8) (12 19) (13 22) (14 0) (15 4) (16 20) (17 5) (18 1) (21 7) (23 3) (2 6) 10: (10) (11 24) (12 5) (13 16) (14 23) (15 2) (17 21) (18 6) (19 0) (20 1) (22 4) (3 7) (8 9) 11: (11) (12 3) (13 6) (14 17) (15 20) (16 2) (18 22) (19 7) (21 0) (23 5) (24 8) (1 4) (9 10) 12: (12) (13 24) (14 15) (16 21) (17 0) (18 11) (19 6) (20 10) (22 3) (23 7) (1 5) (2 9) (4 8) 13: (13) (14 24) (15 12) (16 7) (17 22) (18 2) (19 8) (20 4) (21 11) (23 1) (0 6) (3 10) (5 9) 14: (14) (15 24) (16 9) (17 4) (18 23) (19 3) (20 0) (21 5) (22 8) (1 11) (2 7) (6 10) (12 13) 15: (15) (16 1) (17 10) (18 5) (19 20) (21 2) (22 6) (23 9) (24 12) (0 8) (3 4) (7 11) (13 14) 16: (16) (17 24) (18 19) (20 14) (21 4) (22 1) (23 11) (0 9) (2 5) (3 13) (6 15) (7 10) (8 12) 17: (17) (18 24) (19 16) (20 8) (21 15) (22 5) (23 0) (1 14) (2 10) (3 6) (4 11) (7 12) (9 13) 18: (18) (19 24) (20 2) (21 9) (22 12) (23 6) (0 15) (1 7) (3 11) (4 13) (5 8) (10 14) (16 17) 19: (19) (20 7) (21 3) (22 10) (23 13) (24 16) (0 4) (1 8) (2 12) (5 14) (6 9) (11 15) (17 18) 20: (20) (21 24) (22 23) (0 16) (1 12) (2 4) (3 8) (5 10) (6 17) (7 15) (9 14) (11 19) (13 18) 21: (21) (22 24) (23 20) (0 13) (1 9) (2 17) (3 5) (4 12) (6 11) (7 18) (8 16) (10 15) (14 19) 22: (22) (23 24) (0 10) (1 6) (2 14) (3 18) (4 19) (5 13) (7 8) (9 17) (11 12) (15 16) (20 21) 23: (23) (24 20) (0 7) (1 19) (2 11) (3 15) (4 9) (5 16) (6 14) (8 13) (10 18) (12 17) (21 22) 24: (24) (0 3) (1 2) (4 6) (5 7) (8 10) (9 11) (12 14) (13 15) (16 18) (17 19) (20 22) (21 23) -- autom facts: AUTOM: (0 22 21 10 24 17 8 18 3 5 12 14 1 13 4 23 2 9 16 6) (7) (11 19 20 15) (0 3 5 16) (1 19 11 9) (2 14) (4 12 17 6) (7 8) (10 18 13 15) (20 24 21 23) (22) Equational facts: X = (f X X) X = (f Y (f Y X)) X = (f (f (f X Y) X) Y) X = (f (f Y X) (f X Y)) X = (f (f (f Y X) Y) Y) (f X Y) = (f (f Y X) X) 15 = (f X (f X 15)) 4 = (f X (f X 4)) 10 = (f X (f X 10)) X = (f 13 (f 13 X)) X = (g X X) X = (f (f X Y) (f (f X Y) X)) 12 = (f X (f X 12)) 6 = (f X (f X 6)) X = (f 1 (f 1 X)) 1 = (f X (f X 1)) 20 = (f X (f X 20)) X = (f 8 (f 8 X)) 5 = (f X (f X 5)) 11 = (f X (f X 11)) --------------------------------------- Model 25_4: 0 3 24 1 13 23 8 18 6 15 19 16 20 4 22 9 11 21 7 10 12 17 14 5 2 24 1 3 2 19 10 12 17 13 14 5 22 6 8 9 21 20 7 23 4 16 15 11 18 0 1 0 2 24 8 17 10 19 4 16 6 23 21 22 20 18 9 5 15 7 14 12 13 11 3 2 24 0 3 18 12 16 13 19 22 21 20 5 7 23 17 6 15 4 8 11 10 9 14 1 11 15 14 9 4 24 7 6 20 3 17 0 23 16 2 1 13 10 22 21 8 19 18 12 5 15 16 13 19 7 5 24 4 12 23 20 21 8 2 18 0 1 22 14 3 10 11 17 9 6 21 11 18 14 5 4 6 24 17 19 15 1 22 20 3 10 23 8 2 9 13 0 12 16 7 12 9 23 21 24 6 5 7 15 1 13 19 0 10 17 8 22 14 20 11 18 3 16 2 4 17 23 20 5 14 3 21 16 8 24 11 10 19 18 4 22 7 0 13 12 2 6 15 1 9 5 17 12 18 22 0 13 14 11 9 24 8 2 6 7 23 21 1 3 20 19 16 4 15 10 22 20 15 7 23 16 18 3 9 8 10 24 17 21 19 2 5 12 6 14 1 13 0 4 11 13 12 7 15 16 18 22 2 24 10 9 11 1 0 21 3 4 20 5 23 17 14 6 19 8 18 22 16 8 10 19 11 20 3 21 4 6 12 24 15 14 2 23 0 5 7 9 1 17 13 16 18 17 10 11 22 19 21 23 20 3 4 15 13 24 12 0 2 1 6 9 7 5 8 14 10 7 8 16 20 11 23 1 2 17 0 5 13 12 14 24 3 9 21 22 4 18 19 6 15 23 19 6 20 21 9 2 22 16 5 18 17 24 14 13 15 8 11 10 1 3 4 7 0 12 4 10 21 23 0 20 14 15 22 12 1 13 9 11 6 7 16 24 19 18 5 2 8 3 17 6 14 22 11 12 13 0 9 21 7 23 3 4 5 1 20 19 17 24 16 15 8 2 10 18 20 8 10 22 9 21 15 12 1 4 2 14 7 23 11 6 17 16 18 24 0 5 3 13 19 14 21 11 12 15 8 20 23 5 13 22 2 3 9 0 4 24 18 17 19 6 1 10 7 16 7 5 4 17 2 1 9 0 14 6 16 15 18 19 8 11 10 3 12 13 20 24 23 22 21 8 4 9 13 1 14 17 10 0 2 7 18 16 3 5 19 12 6 11 15 23 21 24 20 22 19 6 5 4 3 2 1 8 7 18 14 12 11 17 10 16 15 13 9 0 21 20 22 24 23 9 13 19 6 17 15 3 11 18 0 12 7 10 1 16 5 14 4 8 2 24 22 21 23 20 3 2 1 0 6 7 4 5 10 11 8 9 14 15 12 13 18 19 16 17 22 23 20 21 24 -- cycle notation: 0: (0) (1 3) (2 24) (4 13) (5 23) (6 8) (7 18) (9 15) (10 19) (11 16) (12 20) (14 22) (17 21) 1: (1) (2 3) (4 19) (5 10) (6 12) (7 17) (8 13) (9 14) (11 22) (15 21) (16 20) (18 23) (24 0) 2: (2) (3 24) (4 8) (5 17) (6 10) (7 19) (9 16) (11 23) (12 21) (13 22) (14 20) (15 18) (0 1) 3: (3) (4 18) (5 12) (6 16) (7 13) (8 19) (9 22) (10 21) (11 20) (14 23) (15 17) (24 1) (0 2) 4: (4) (5 24) (6 7) (8 20) (9 3) (10 17) (11 0) (12 23) (13 16) (14 2) (15 1) (18 22) (19 21) 5: (5) (6 24) (7 4) (8 12) (9 23) (10 20) (11 21) (13 2) (14 18) (15 0) (16 1) (17 22) (19 3) 6: (6) (7 24) (8 17) (9 19) (10 15) (11 1) (12 22) (13 20) (14 3) (16 23) (18 2) (21 0) (4 5) 7: (7) (8 15) (9 1) (10 13) (11 19) (12 0) (14 17) (16 22) (18 20) (21 3) (23 2) (24 4) (5 6) 8: (8) (9 24) (10 11) (12 19) (13 18) (14 4) (15 22) (16 7) (17 0) (20 2) (21 6) (23 1) (3 5) 9: (9) (10 24) (11 8) (12 2) (13 6) (14 7) (15 23) (16 21) (17 1) (18 3) (19 20) (22 4) (0 5) 10: (10) (11 24) (12 17) (13 21) (14 19) (15 2) (16 5) (18 6) (20 1) (22 0) (23 4) (3 7) (8 9) 11: (11) (12 1) (13 0) (14 21) (15 3) (16 4) (17 20) (18 5) (19 23) (22 6) (24 8) (2 7) (9 10) 12: (12) (13 24) (14 15) (16 2) (17 23) (18 0) (19 5) (20 7) (21 9) (22 1) (3 8) (4 10) (6 11) 13: (13) (14 24) (15 12) (16 0) (17 2) (18 1) (19 6) (20 9) (21 7) (22 5) (23 8) (3 10) (4 11) 14: (14) (15 24) (16 3) (17 9) (18 21) (19 22) (20 4) (23 6) (0 10) (1 7) (2 8) (5 11) (12 13) 15: (15) (16 8) (17 11) (18 10) (19 1) (20 3) (21 4) (22 7) (23 0) (24 12) (2 6) (5 9) (13 14) 16: (16) (17 24) (18 19) (20 5) (21 2) (22 8) (23 3) (0 4) (1 10) (6 14) (7 15) (9 12) (11 13) 17: (17) (18 24) (19 16) (20 15) (21 8) (22 2) (23 10) (0 6) (1 14) (3 11) (4 12) (5 13) (7 9) 18: (18) (19 24) (20 0) (21 5) (22 3) (23 13) (1 8) (2 10) (4 9) (6 15) (7 12) (11 14) (16 17) 19: (19) (20 6) (21 1) (22 10) (23 7) (24 16) (0 14) (2 11) (3 12) (4 15) (5 8) (9 13) (17 18) 20: (20) (21 24) (22 23) (0 7) (1 5) (2 4) (3 17) (6 9) (8 14) (10 16) (11 15) (12 18) (13 19) 21: (21) (22 24) (23 20) (0 8) (1 4) (2 9) (3 13) (5 14) (6 17) (7 10) (11 18) (12 16) (15 19) 22: (22) (23 24) (0 19) (1 6) (2 5) (3 4) (7 8) (9 18) (10 14) (11 12) (13 17) (15 16) (20 21) 23: (23) (24 20) (0 9) (1 13) (2 19) (3 6) (4 17) (5 15) (7 11) (8 18) (10 12) (14 16) (21 22) 24: (24) (0 3) (1 2) (4 6) (5 7) (8 10) (9 11) (12 14) (13 15) (16 18) (17 19) (20 22) (21 23) -- autom facts: AUTOM: (0 22 12 3 2 13 15 20 4 16 7 18 9 21 10 6 19 1 5 24 17 14 11 8) (23) Equational facts: X = (f X X) X = (f Y (f Y X)) X = (f (f Y X) (f X Y)) X = (f (f (f Y X) Y) Y) (f X Y) = (f (f Y X) X) X = (f (f (f X Y) X) Y) 8 = (f X (f X 8)) X = (f 9 (f 9 X)) 2 = (f X (f X 2)) X = (f 24 (f 24 X)) X = (f 3 (f 3 X)) 0 = (f X (f X 0)) X = (f 2 (f 2 X)) X = (f 21 (f 21 X)) 4 = (f X (f X 4)) 5 = (f X (f X 5)) 3 = (f X (f X 3)) X = (f 0 (f 0 X)) 9 = (f X (f X 9)) X = (f 11 (f 11 X)) --------------------------------------- Model 25_5: 0 3 24 1 10 18 8 9 6 7 4 19 22 23 21 17 20 15 5 11 16 14 12 13 2 24 1 3 2 18 22 11 13 12 16 17 6 8 7 23 21 9 10 4 20 19 15 5 14 0 1 0 2 24 19 13 17 22 14 21 20 16 23 5 8 18 11 6 15 4 10 9 7 12 3 2 24 0 3 15 12 10 11 21 20 6 7 5 17 19 4 22 13 23 14 9 8 16 18 1 13 8 9 16 4 24 7 6 1 2 23 20 18 0 17 22 3 14 12 21 11 19 15 10 5 14 10 11 20 7 5 24 4 19 12 1 2 9 16 0 23 13 22 21 8 3 18 17 15 6 20 21 23 19 5 4 6 24 16 22 14 15 17 18 10 11 8 12 13 3 0 1 9 2 7 15 20 8 18 24 6 5 7 2 17 21 23 16 19 22 0 12 9 3 13 1 10 14 11 4 16 18 22 17 12 15 20 14 8 24 11 10 4 21 7 5 0 3 1 23 6 13 2 19 9 17 14 19 5 21 3 18 15 11 9 24 8 20 22 1 7 23 0 6 2 12 4 13 16 10 23 22 15 14 13 17 19 16 9 8 10 24 21 4 3 2 7 5 20 6 18 12 1 0 11 22 15 13 23 17 16 21 18 24 10 9 11 19 2 20 1 5 4 7 12 14 6 0 3 8 11 4 6 9 1 20 2 10 18 3 7 0 12 24 15 14 21 23 8 22 5 16 19 17 13 10 19 16 8 23 11 9 20 3 6 0 5 15 13 24 12 2 21 22 1 7 17 18 4 14 18 16 7 6 11 21 3 2 22 23 19 4 13 12 14 24 1 20 0 10 17 5 8 9 15 9 6 20 22 16 19 1 17 23 0 18 21 24 14 13 15 4 7 10 5 2 11 3 8 12 6 23 5 15 22 2 0 21 20 14 12 13 10 11 9 3 16 24 19 18 8 7 4 1 17 7 5 12 21 20 1 23 0 13 15 22 14 2 8 11 9 19 17 24 16 4 3 10 6 18 21 12 10 11 8 14 22 23 4 13 2 3 1 9 5 20 17 16 18 24 15 0 6 7 19 12 7 21 10 9 23 14 1 15 4 3 22 0 20 6 8 24 18 17 19 13 2 11 5 16 8 13 18 12 14 9 16 19 0 5 15 17 3 1 4 10 6 11 2 7 20 24 23 22 21 5 11 4 13 2 0 15 12 17 19 16 1 7 3 18 6 10 8 14 9 23 21 24 20 22 19 17 14 4 3 10 13 8 7 18 5 12 11 6 2 16 15 1 9 0 21 20 22 24 23 4 9 17 7 0 8 12 3 5 1 13 18 6 10 16 19 14 2 11 15 24 22 21 23 20 3 2 1 0 6 7 4 5 10 11 8 9 14 15 12 13 18 19 16 17 22 23 20 21 24 -- cycle notation: 0: (0) (1 3) (2 24) (4 10) (5 18) (6 8) (7 9) (11 19) (12 22) (13 23) (14 21) (15 17) (16 20) 1: (1) (2 3) (4 18) (5 22) (6 11) (7 13) (8 12) (9 16) (10 17) (14 23) (15 21) (19 20) (24 0) 2: (2) (3 24) (4 19) (5 13) (6 17) (7 22) (8 14) (9 21) (10 20) (11 16) (12 23) (15 18) (0 1) 3: (3) (4 15) (5 12) (6 10) (7 11) (8 21) (9 20) (13 17) (14 19) (16 22) (18 23) (24 1) (0 2) 4: (4) (5 24) (6 7) (8 1) (9 2) (10 23) (11 20) (12 18) (13 0) (14 17) (15 22) (16 3) (19 21) 5: (5) (6 24) (7 4) (8 19) (9 12) (10 1) (11 2) (13 16) (14 0) (15 23) (17 22) (18 21) (20 3) 6: (6) (7 24) (8 16) (9 22) (10 14) (11 15) (12 17) (13 18) (19 3) (20 0) (21 1) (23 2) (4 5) 7: (7) (8 2) (9 17) (10 21) (11 23) (12 16) (13 19) (14 22) (15 0) (18 3) (20 1) (24 4) (5 6) 8: (8) (9 24) (10 11) (12 4) (13 21) (14 7) (15 5) (16 0) (17 3) (18 1) (19 23) (20 6) (22 2) 9: (9) (10 24) (11 8) (12 20) (13 22) (14 1) (15 7) (16 23) (17 0) (18 6) (19 2) (21 4) (3 5) 10: (10) (11 24) (12 21) (13 4) (14 3) (15 2) (16 7) (17 5) (18 20) (19 6) (22 1) (23 0) (8 9) 11: (11) (12 19) (13 2) (14 20) (15 1) (16 5) (17 4) (18 7) (21 6) (22 0) (23 3) (24 8) (9 10) 12: (12) (13 24) (14 15) (16 21) (17 23) (18 8) (19 22) (20 5) (0 11) (1 4) (2 6) (3 9) (7 10) 13: (13) (14 24) (15 12) (16 2) (17 21) (18 22) (19 1) (20 7) (23 4) (0 10) (3 8) (5 11) (6 9) 14: (14) (15 24) (16 1) (17 20) (18 0) (19 10) (21 5) (22 8) (23 9) (2 7) (3 6) (4 11) (12 13) 15: (15) (16 4) (17 7) (18 10) (19 5) (20 2) (21 11) (22 3) (23 8) (24 12) (0 9) (1 6) (13 14) 16: (16) (17 24) (18 19) (20 8) (21 7) (22 4) (23 1) (0 6) (2 5) (3 15) (9 14) (10 12) (11 13) 17: (17) (18 24) (19 16) (20 4) (21 3) (22 10) (23 6) (0 7) (1 5) (2 12) (8 13) (9 15) (11 14) 18: (18) (19 24) (20 15) (21 0) (22 6) (23 7) (1 12) (2 10) (3 11) (4 8) (5 14) (9 13) (16 17) 19: (19) (20 13) (21 2) (22 11) (23 5) (24 16) (0 12) (1 7) (3 10) (4 9) (6 14) (8 15) (17 18) 20: (20) (21 24) (22 23) (0 8) (1 13) (2 18) (3 12) (4 14) (5 9) (6 16) (7 19) (10 15) (11 17) 21: (21) (22 24) (23 20) (0 5) (1 11) (2 4) (3 13) (6 15) (7 12) (8 17) (9 19) (10 16) (14 18) 22: (22) (23 24) (0 19) (1 17) (2 14) (3 4) (5 10) (6 13) (7 8) (9 18) (11 12) (15 16) (20 21) 23: (23) (24 20) (0 4) (1 9) (2 17) (3 7) (5 8) (6 12) (10 13) (11 18) (14 16) (15 19) (21 22) 24: (24) (0 3) (1 2) (4 6) (5 7) (8 10) (9 11) (12 14) (13 15) (16 18) (17 19) (20 22) (21 23) -- autom facts: AUTOM: (0 2 10 17 7 8 11 4 6 16 13 23 12 21 3 18 1 15 22 9 14 24 20 5) (19) Equational facts: X = (f X X) X = (f Y (f Y X)) X = (f (f (f X Y) X) Y) (f X Y) = (f (f Y X) X) X = (f (f (f Y X) Y) Y) X = (f (f Y X) (f X Y)) X = (f 23 (f 23 X)) 7 = (f X (f X 7)) 11 = (f X (f X 11)) 2 = (f X (f X 2)) X = (f 12 (f 12 X)) (f X Y) = (f Y (f (f Y X) Y)) 3 = (f X (f X 3)) X = (f 15 (f 15 X)) (f (f X Y) X) = (f X (f Y X)) X = (f 14 (f 14 X)) 21 = (f X (f X 21)) 5 = (f X (f X 5)) 15 = (f X (f X 15)) X = (f 24 (f 24 X)) --------------------------------------- Model 25_6: 0 3 24 1 8 19 9 18 4 6 20 14 16 22 11 23 12 21 7 5 10 17 13 15 2 24 1 3 2 15 11 12 13 19 14 21 5 6 7 9 4 23 22 20 8 18 10 17 16 0 1 0 2 24 16 20 22 17 14 13 18 19 23 9 8 21 4 7 10 11 5 15 6 12 3 2 24 0 3 12 10 14 9 18 7 5 22 4 23 6 17 21 15 8 20 19 16 11 13 1 21 18 13 11 4 24 7 6 17 16 19 3 22 2 23 20 9 8 1 10 15 0 12 14 5 22 23 14 17 7 5 24 4 20 12 15 16 9 19 2 10 11 3 21 13 8 18 0 1 6 23 19 18 21 5 4 6 24 12 15 22 20 8 17 16 9 14 13 2 1 11 3 10 0 7 11 21 12 20 24 6 5 7 15 19 13 0 2 10 18 8 22 23 14 9 3 1 16 17 4 17 6 5 23 21 2 1 16 8 24 11 10 19 18 20 22 7 0 13 12 14 4 15 3 9 15 22 4 19 2 21 23 20 11 9 24 8 18 16 17 0 13 14 12 3 7 5 1 6 10 12 7 6 15 23 17 2 1 9 8 10 24 0 21 19 3 20 5 22 14 16 13 18 4 11 18 16 15 12 22 23 13 14 24 10 9 11 3 6 7 2 1 20 0 21 17 19 4 5 8 20 8 17 22 11 18 19 23 1 21 16 4 12 24 15 14 10 2 5 6 0 9 3 7 13 5 10 16 8 9 0 20 21 3 4 1 17 15 13 24 12 2 11 23 22 6 7 19 18 14 7 17 20 16 10 8 21 0 5 22 4 18 13 12 14 24 3 1 11 23 2 6 9 19 15 6 20 19 5 18 3 0 22 16 23 17 21 24 14 13 15 8 10 4 2 1 11 7 9 12 10 5 9 6 13 1 3 15 22 2 0 23 20 4 21 7 16 24 19 18 12 14 8 11 17 4 9 23 10 0 15 11 12 21 1 3 6 7 20 22 5 19 17 24 16 13 8 14 2 18 14 15 22 13 20 9 10 11 23 5 6 7 21 3 0 1 17 16 18 24 4 12 2 8 19 13 12 21 7 14 22 8 3 6 20 23 15 1 0 4 11 24 18 17 19 9 2 5 10 16 16 4 8 9 1 14 17 19 2 3 12 13 10 11 5 18 0 6 15 7 20 24 23 22 21 8 13 11 14 17 12 16 10 0 18 7 2 5 1 3 19 6 4 9 15 23 21 24 20 22 19 14 10 4 3 13 18 8 7 17 2 12 11 5 1 16 15 9 6 0 21 20 22 24 23 9 11 7 18 19 16 15 2 13 0 14 1 17 8 10 6 5 12 3 4 24 22 21 23 20 3 2 1 0 6 7 4 5 10 11 8 9 14 15 12 13 18 19 16 17 22 23 20 21 24 -- cycle notation: 0: (0) (1 3) (2 24) (4 8) (5 19) (6 9) (7 18) (10 20) (11 14) (12 16) (13 22) (15 23) (17 21) 1: (1) (2 3) (4 15) (5 11) (6 12) (7 13) (8 19) (9 14) (10 21) (16 23) (17 22) (18 20) (24 0) 2: (2) (3 24) (4 16) (5 20) (6 22) (7 17) (8 14) (9 13) (10 18) (11 19) (12 23) (15 21) (0 1) 3: (3) (4 12) (5 10) (6 14) (7 9) (8 18) (11 22) (13 23) (15 17) (16 21) (19 20) (24 1) (0 2) 4: (4) (5 24) (6 7) (8 17) (9 16) (10 19) (11 3) (12 22) (13 2) (14 23) (15 20) (18 1) (21 0) 5: (5) (6 24) (7 4) (8 20) (9 12) (10 15) (11 16) (13 19) (14 2) (17 3) (18 21) (22 0) (23 1) 6: (6) (7 24) (8 12) (9 15) (10 22) (11 20) (13 17) (14 16) (18 2) (19 1) (21 3) (23 0) (4 5) 7: (7) (8 15) (9 19) (10 13) (11 0) (12 2) (14 18) (16 22) (17 23) (20 3) (21 1) (24 4) (5 6) 8: (8) (9 24) (10 11) (12 19) (13 18) (14 20) (15 22) (16 7) (17 0) (21 4) (23 3) (1 6) (2 5) 9: (9) (10 24) (11 8) (12 18) (13 16) (14 17) (15 0) (19 3) (20 7) (21 5) (22 1) (23 6) (2 4) 10: (10) (11 24) (12 0) (13 21) (14 19) (15 3) (16 20) (17 5) (18 22) (23 4) (1 7) (2 6) (8 9) 11: (11) (12 3) (13 6) (14 7) (15 2) (16 1) (17 20) (18 0) (19 21) (22 4) (23 5) (24 8) (9 10) 12: (12) (13 24) (14 15) (16 10) (17 2) (18 5) (19 6) (20 0) (21 9) (22 3) (23 7) (1 8) (4 11) 13: (13) (14 24) (15 12) (16 2) (17 11) (18 23) (19 22) (20 6) (21 7) (0 5) (1 10) (3 8) (4 9) 14: (14) (15 24) (16 3) (17 1) (18 11) (19 23) (20 2) (21 6) (22 9) (0 7) (4 10) (5 8) (12 13) 15: (15) (16 8) (17 10) (18 4) (19 2) (20 1) (21 11) (22 7) (23 9) (24 12) (0 6) (3 5) (13 14) 16: (16) (17 24) (18 19) (20 12) (21 14) (22 8) (23 11) (0 10) (1 5) (2 9) (3 6) (4 13) (7 15) 17: (17) (18 24) (19 16) (20 13) (21 8) (22 14) (23 2) (0 4) (1 9) (3 10) (5 15) (6 11) (7 12) 18: (18) (19 24) (20 4) (21 12) (22 2) (23 8) (0 14) (1 15) (3 13) (5 9) (6 10) (7 11) (16 17) 19: (19) (20 9) (21 2) (22 5) (23 10) (24 16) (0 13) (1 12) (3 7) (4 14) (6 8) (11 15) (17 18) 20: (20) (21 24) (22 23) (0 16) (1 4) (2 8) (3 9) (5 14) (6 17) (7 19) (10 12) (11 13) (15 18) 21: (21) (22 24) (23 20) (0 8) (1 13) (2 11) (3 14) (4 17) (5 12) (6 16) (7 10) (9 18) (15 19) 22: (22) (23 24) (0 19) (1 14) (2 10) (3 4) (5 13) (6 18) (7 8) (9 17) (11 12) (15 16) (20 21) 23: (23) (24 20) (0 9) (1 11) (2 7) (3 18) (4 19) (5 16) (6 15) (8 13) (10 14) (12 17) (21 22) 24: (24) (0 3) (1 2) (4 6) (5 7) (8 10) (9 11) (12 14) (13 15) (16 18) (17 19) (20 22) (21 23) -- autom facts: AUTOM: (0 2 23 11 14 8 13 6 21 4 9 15 19 10 24 12 1 7 5 18 20 3 17 16) (22) Equational facts: X = (f X X) X = (f Y (f Y X)) (f X Y) = (f (f Y X) X) X = (f (f Y X) (f X Y)) X = (f (f (f X Y) X) Y) X = (f (f (f Y X) Y) Y) 11 = (f X (f X 11)) 4 = (f X (f X 4)) 1 = (f X (f X 1)) 3 = (f X (f X 3)) X = (g X X) X = (f 5 (f 5 X)) X = (f 18 (f 18 X)) X = (f 20 (f 20 X)) X = (f 22 (f 22 X)) 14 = (f X (f X 14)) 7 = (f X (f X 7)) X = (f 9 (f 9 X)) X = (f 3 (f 3 X)) (f X Y) = (f Y (f (f X Y) X)) --------------------------------------- Model 25_7: 0 3 24 1 8 15 16 21 4 22 20 14 17 19 11 5 6 12 23 13 10 7 9 18 2 24 1 3 2 12 16 20 22 14 21 19 15 4 18 8 11 5 23 13 10 6 9 7 17 0 1 0 2 24 11 19 10 15 16 18 6 4 20 21 23 7 8 22 9 5 12 13 17 14 3 2 24 0 3 15 17 23 20 13 12 18 19 9 8 21 4 22 5 10 11 7 14 16 6 1 23 19 13 16 4 24 7 6 18 20 12 21 10 2 17 22 3 14 8 1 9 11 15 0 5 20 21 14 13 7 5 24 4 17 16 15 22 18 3 2 10 9 8 12 23 0 1 11 19 6 11 13 17 12 5 4 6 24 21 23 22 0 3 1 16 19 14 2 20 15 18 8 10 9 7 17 8 9 11 24 6 5 7 1 2 23 3 21 16 22 18 13 0 15 20 19 12 14 10 4 18 22 12 5 23 3 15 14 8 24 11 10 2 17 7 6 20 13 0 21 16 19 1 4 9 13 5 15 6 14 1 3 18 11 9 24 8 23 0 4 2 21 20 7 22 17 16 19 12 10 5 4 22 21 1 0 17 13 9 8 10 24 19 7 18 20 23 6 14 12 15 3 2 16 11 16 17 21 20 13 12 14 19 24 10 9 11 5 4 6 23 0 1 22 7 3 2 18 15 8 7 10 16 23 19 22 9 0 20 6 1 18 12 24 15 14 2 21 11 4 8 17 5 3 13 22 20 11 17 21 8 18 23 5 19 16 2 15 13 24 12 10 3 6 9 1 4 0 7 14 6 7 19 10 20 23 0 1 22 17 3 16 13 12 14 24 11 9 21 2 4 18 8 5 15 10 23 18 22 16 20 21 9 19 7 0 17 24 14 13 15 4 11 2 8 5 6 3 1 12 14 9 20 15 22 21 11 10 12 1 7 6 8 23 0 3 16 24 19 18 2 5 4 13 17 21 15 10 8 9 13 22 12 3 4 2 23 7 5 20 1 19 17 24 16 14 0 6 11 18 4 6 7 14 0 11 1 2 23 15 21 5 22 20 3 9 17 16 18 24 13 10 12 8 19 9 12 23 7 10 14 8 3 6 0 4 20 1 22 5 21 24 18 17 19 11 15 13 2 16 15 18 8 19 17 10 13 11 2 14 5 7 16 6 9 0 12 4 1 3 20 24 23 22 21 12 16 4 18 2 9 19 17 15 5 14 13 0 11 10 8 1 7 3 6 23 21 24 20 22 19 14 6 4 3 18 2 8 7 13 17 12 11 9 1 16 15 10 5 0 21 20 22 24 23 8 11 5 9 18 2 12 16 0 3 13 1 6 10 19 17 7 15 4 14 24 22 21 23 20 3 2 1 0 6 7 4 5 10 11 8 9 14 15 12 13 18 19 16 17 22 23 20 21 24 -- cycle notation: 0: (0) (1 3) (2 24) (4 8) (5 15) (6 16) (7 21) (9 22) (10 20) (11 14) (12 17) (13 19) (18 23) 1: (1) (2 3) (4 12) (5 16) (6 20) (7 22) (8 14) (9 21) (10 19) (11 15) (13 18) (17 23) (24 0) 2: (2) (3 24) (4 11) (5 19) (6 10) (7 15) (8 16) (9 18) (12 20) (13 21) (14 23) (17 22) (0 1) 3: (3) (4 15) (5 17) (6 23) (7 20) (8 13) (9 12) (10 18) (11 19) (14 21) (16 22) (24 1) (0 2) 4: (4) (5 24) (6 7) (8 18) (9 20) (10 12) (11 21) (13 2) (14 17) (15 22) (16 3) (19 1) (23 0) 5: (5) (6 24) (7 4) (8 17) (9 16) (10 15) (11 22) (12 18) (13 3) (14 2) (19 23) (20 0) (21 1) 6: (6) (7 24) (8 21) (9 23) (10 22) (11 0) (12 3) (13 1) (14 16) (15 19) (17 2) (18 20) (4 5) 7: (7) (8 1) (9 2) (10 23) (11 3) (12 21) (13 16) (14 22) (15 18) (17 0) (19 20) (24 4) (5 6) 8: (8) (9 24) (10 11) (12 2) (13 17) (14 7) (15 6) (16 20) (18 0) (19 21) (22 1) (23 4) (3 5) 9: (9) (10 24) (11 8) (12 23) (13 0) (14 4) (15 2) (16 21) (17 20) (18 7) (19 22) (1 5) (3 6) 10: (10) (11 24) (12 19) (13 7) (14 18) (15 20) (16 23) (17 6) (21 3) (22 2) (0 5) (1 4) (8 9) 11: (11) (12 5) (13 4) (14 6) (15 23) (16 0) (17 1) (18 22) (19 7) (20 3) (21 2) (24 8) (9 10) 12: (12) (13 24) (14 15) (16 2) (17 21) (18 11) (19 4) (20 8) (22 5) (23 3) (0 7) (1 10) (6 9) 13: (13) (14 24) (15 12) (16 10) (17 3) (18 6) (19 9) (20 1) (21 4) (22 0) (23 7) (2 11) (5 8) 14: (14) (15 24) (16 11) (17 9) (18 21) (19 2) (20 4) (22 8) (23 5) (0 6) (1 7) (3 10) (12 13) 15: (15) (16 4) (17 11) (18 2) (19 8) (20 5) (21 6) (22 3) (23 1) (24 12) (0 10) (7 9) (13 14) 16: (16) (17 24) (18 19) (20 2) (21 5) (22 4) (23 13) (0 14) (1 9) (3 15) (6 11) (7 10) (8 12) 17: (17) (18 24) (19 16) (20 14) (21 0) (22 6) (23 11) (1 15) (2 10) (3 8) (4 9) (5 13) (7 12) 18: (18) (19 24) (20 13) (21 10) (22 12) (23 8) (0 4) (1 6) (2 7) (3 14) (5 11) (9 15) (16 17) 19: (19) (20 11) (21 15) (22 13) (23 2) (24 16) (0 9) (1 12) (3 7) (4 10) (5 14) (6 8) (17 18) 20: (20) (21 24) (22 23) (0 15) (1 18) (2 8) (3 19) (4 17) (5 10) (6 13) (7 11) (9 14) (12 16) 21: (21) (22 24) (23 20) (0 12) (1 16) (2 4) (3 18) (5 9) (6 19) (7 17) (8 15) (10 14) (11 13) 22: (22) (23 24) (0 19) (1 14) (2 6) (3 4) (5 18) (7 8) (9 13) (10 17) (11 12) (15 16) (20 21) 23: (23) (24 20) (0 8) (1 11) (2 5) (3 9) (4 18) (6 12) (7 16) (10 13) (14 19) (15 17) (21 22) 24: (24) (0 3) (1 2) (4 6) (5 7) (8 10) (9 11) (12 14) (13 15) (16 18) (17 19) (20 22) (21 23) -- autom facts: AUTOM: (0 23 13 5 4 16 17 6 15 18 10 8 7 3 24 22 19 2 21 9 14 11 1 20) (12) Equational facts: X = (f X X) X = (f Y (f Y X)) X = (f (f (f X Y) X) Y) (f X Y) = (f (f Y X) X) X = (f (f (f Y X) Y) Y) X = (f (f Y X) (f X Y)) X = (f 22 (f 22 X)) 3 = (f X (f X 3)) X = (f 10 (f 10 X)) X = (f (f X Y) (f (f X Y) X)) 5 = (f X (f X 5)) 15 = (f X (f X 15)) X = (f 12 (f 12 X)) 9 = (f X (f X 9)) (f (f X Y) X) = (f X (f Y X)) X = (f 6 (f 6 X)) X = (f 17 (f 17 X)) 22 = (f X (f X 22)) 12 = (f X (f X 12)) X = (f 20 (f 20 X)) --------------------------------------- Model 29_0: 0 28 15 21 17 13 26 9 12 8 25 2 1 27 4 16 10 23 7 14 3 5 19 11 18 6 22 24 20 25 1 28 14 27 16 7 26 10 13 9 24 3 2 15 11 22 8 20 4 5 18 12 17 0 21 23 6 19 8 24 2 28 20 26 15 3 25 11 7 10 23 4 12 21 9 19 5 6 14 13 16 1 27 22 0 17 18 14 9 23 3 28 19 25 5 4 24 12 8 11 22 27 10 18 6 0 20 13 15 2 26 21 1 16 7 17 24 20 10 22 4 28 18 21 6 5 23 13 9 12 11 17 0 1 19 7 26 3 25 27 2 15 8 14 16 17 23 19 11 21 5 28 13 27 0 6 22 7 10 16 1 2 18 8 25 12 24 26 3 14 9 20 4 15 28 16 22 18 12 27 6 11 7 26 1 0 21 8 2 3 17 9 24 13 15 25 4 20 10 19 5 23 14 2 5 1 15 9 8 17 7 28 25 18 27 6 16 21 13 19 14 12 22 4 0 24 10 11 26 3 20 23 16 3 6 2 14 10 9 15 8 28 24 17 26 0 7 18 20 13 21 5 27 23 11 12 25 4 19 1 22 10 15 4 0 3 20 11 1 14 9 28 23 16 25 17 19 7 27 6 26 8 12 13 24 5 18 2 22 21 12 11 14 5 1 4 19 24 2 20 10 28 22 15 18 8 26 0 25 9 16 7 23 6 17 3 21 13 27 18 13 12 20 6 2 5 14 23 3 19 11 28 21 9 25 1 24 10 15 17 22 0 16 4 27 7 8 26 6 17 7 13 19 0 3 27 20 22 4 18 12 28 24 2 23 11 14 16 10 1 15 5 26 8 9 21 25 4 0 16 8 7 18 1 28 26 19 21 5 17 13 3 22 12 20 15 11 23 14 6 25 9 10 27 2 24 5 10 3 24 18 11 27 20 22 16 0 25 8 6 14 28 13 2 9 23 1 26 21 7 19 17 15 12 4 9 2 25 19 10 21 4 23 17 6 26 7 5 14 0 15 28 12 1 8 24 11 27 22 13 20 18 16 3 1 26 20 9 22 3 8 18 5 27 13 4 15 24 25 6 16 28 11 0 7 17 10 21 23 12 14 19 2 27 14 8 23 2 7 0 4 21 12 3 16 25 19 13 26 5 17 28 10 6 20 18 9 22 24 11 15 1 15 7 24 1 13 6 21 22 11 2 17 26 20 3 5 12 27 4 18 28 9 16 14 19 8 23 25 10 0 13 25 0 12 5 22 16 10 1 18 27 14 2 23 8 4 11 21 3 19 28 9 17 15 20 7 24 26 6 26 6 11 4 23 17 12 0 19 21 15 1 24 9 28 7 3 10 22 2 20 27 8 18 16 14 13 25 5 19 4 9 27 16 23 10 25 0 14 8 6 13 18 1 20 15 3 26 24 22 21 28 2 12 5 17 11 7 3 8 21 17 24 9 20 6 15 7 5 12 19 26 23 0 14 16 2 27 25 10 22 28 1 11 4 18 13 7 22 18 25 8 14 2 16 13 4 11 20 27 5 26 24 6 15 17 1 21 19 9 23 28 0 10 3 12 23 19 26 7 15 1 13 12 3 10 14 21 4 17 22 27 25 5 16 18 0 2 20 8 24 28 6 9 11 20 27 13 16 0 12 24 2 9 15 22 3 18 11 6 23 21 26 4 17 19 8 1 14 7 25 28 5 10 21 12 17 6 11 25 14 8 16 23 2 19 10 1 20 5 24 22 27 3 18 4 7 0 15 13 26 28 9 11 18 5 10 26 15 22 17 24 1 20 9 0 7 19 14 4 25 23 21 2 28 3 13 6 16 12 27 8 22 21 27 26 25 24 23 19 18 17 16 15 14 20 10 9 8 7 13 12 11 6 5 4 3 2 1 0 28 -- cycle notation: 0: (0) (1 28 20 3 21 5 13 27 24 18 7 9 8 12) (2 15 16 10 25 6 26 22 19 14 4 17 23 11) 1: (1) (2 28 19 4 27 6 7 26 23 17 8 10 9 13) (3 14 15 11 24 0 25 21 18 20 5 16 22 12) 2: (2) (3 28 18 5 26 0 8 25 22 16 9 11 10 7) (4 20 14 12 23 1 24 27 17 19 6 15 21 13) 3: (3) (4 28 17 6 25 1 9 24 21 15 10 12 11 8) (5 19 20 13 22 2 23 26 16 18 0 14 27 7) 4: (4) (5 28 16 0 24 2 10 23 27 14 11 13 12 9) (6 18 19 7 21 3 22 25 15 17 1 20 26 8) 5: (5) (6 28 15 1 23 3 11 22 26 20 12 7 13 10) (8 27 4 21 24 14 16 2 19 25 9 0 17 18) 6: (6) (7 11 0 28 14 2 22 4 12 21 25 19 13 8) (9 26 5 27 23 20 15 3 18 24 10 1 16 17) 7: (7) (8 28 23 10 18 12 6 17 14 21 0 2 1 5) (9 25 26 3 15 13 16 19 22 24 11 27 20 4) 8: (8) (9 28 22 11 17 13 0 16 20 27 1 3 2 6) (10 24 25 4 14 7 15 18 21 23 12 26 19 5) 9: (9) (10 28 21 12 16 7 1 15 19 26 2 4 3 0) (11 23 24 5 20 8 14 17 27 22 13 25 18 6) 10: (10) (11 28 27 13 15 8 2 14 18 25 3 5 4 1) (12 22 23 6 19 9 20 16 26 21 7 24 17 0) 11: (11) (12 28 26 7 14 9 3 20 17 24 4 6 5 2) (13 21 22 0 18 10 19 15 25 27 8 23 16 1) 12: (12) (13 28 25 8 20 10 4 19 16 23 5 0 6 3) (14 24 26 9 22 15 2 7 27 21 1 17 11 18) 13: (13) (14 3 8 26 27 2 16 12 17 20 23 25 10 21) (15 22 6 1 0 4 7 28 24 9 19 11 5 18) 14: (14) (15 28 4 18 9 16 13 6 27 12 8 22 21 26) (17 2 3 24 19 23 7 20 1 10 0 5 11 25) 15: (15) (16 28 3 19 8 17 12 5 21 11 7 23 22 27) (18 1 2 25 20 24 13 14 0 9 6 4 10 26) 16: (16) (17 28 2 20 7 18 11 4 22 10 13 24 23 21) (19 0 1 26 14 25 12 15 6 8 5 3 9 27) 17: (17) (18 28 1 14 13 19 10 3 23 9 12 25 24 22) (20 6 0 27 15 26 11 16 5 7 4 2 8 21) 18: (18) (19 28 0 15 12 20 9 2 24 8 11 26 25 23) (21 16 27 10 17 4 13 3 1 7 22 14 5 6) 19: (19) (20 28 6 16 11 14 8 1 25 7 10 27 26 24) (21 9 18 3 12 2 0 13 23 15 4 5 22 17) 20: (20) (21 27 25 14 28 5 17 10 15 7 0 26 13 9) (22 8 19 2 11 1 6 12 24 16 3 4 23 18) 21: (21) (22 28 7 25 5 23 2 9 14 1 4 16 15 20) (24 12 13 18 26 17 3 27 11 6 10 8 0 19) 22: (22) (23 28 13 26 4 24 1 8 15 0 3 17 16 14) (25 11 12 19 27 18 2 21 10 5 9 7 6 20) 23: (23) (24 28 12 27 3 25 0 7 16 6 2 18 17 15) (26 10 11 20 21 19 1 22 9 4 8 13 5 14) 24: (24) (25 28 11 21 2 26 6 13 17 5 1 19 18 16) (27 9 10 14 22 20 0 23 8 3 7 12 4 15) 25: (25) (26 28 10 22 1 27 5 12 18 4 0 20 19 17) (2 13 11 3 16 21 8 9 15 23 14 6 24 7) 26: (26) (27 28 9 23 0 21 4 11 19 3 6 14 20 18) (1 12 10 2 17 22 7 8 16 24 15 5 25 13) 27: (27) (28 8 24 6 22 3 10 20 2 5 15 14 19 21) (0 11 9 1 18 23 13 7 17 25 16 4 26 12) 28: (28) (0 22 5 24 3 26 1 21 6 23 4 25 2 27) (7 19 12 14 10 16 8 18 13 20 11 15 9 17) -- autom facts: AUTOM: (0) (1 11 21 10 24 22 8 17 20 15 13 6 7 14) (2 5 25 18 19 12 23 3 16 27 26 9 4 28) (0 16 17 10 28 3 27 26 7 12 8 6 20 9 15 21 19 11 24 14 4 22 18 25 2 23 13 1 5) Equational facts: X = (f X X) X = (f Y (f X (f (f Y X) Y))) (f X Y) = (f (f X Y) (f X Y)) (f X (f X Y)) = (f (f Y X) X) X = (g X X) (f (f X Y) Y) = (f Y (f Y X)) X = (f (f (f Y (f X Y)) X) Y) (f (f 8 X) X) = (f X (f X 8)) (f X (f X 10)) = (f (f 10 X) X) (f X (f X 18)) = (f (f 18 X) X) (f X (f X 5)) = (f (f 5 X) X) (f (f 0 X) X) = (f X (f X 0)) (f X (f X 19)) = (f (f 19 X) X) (f X (f X 11)) = (f (f 11 X) X) (f X (f X 1)) = (f (f 1 X) X) (f (f 25 X) X) = (f X (f X 25)) (f X (f X 2)) = (f (f 2 X) X) (f X (f X 20)) = (f (f 20 X) X) (f X (f X 27)) = (f (f 27 X) X) (f (f X Y) Y) = (f (f (f X (f X Y)) X) X) --------------------------------------- Model 31_0: 28 9 6 2 21 17 13 8 27 0 4 23 19 15 11 7 26 1 3 22 18 14 10 29 25 5 24 20 16 12 30 0 27 24 20 16 12 8 26 1 3 22 18 14 10 29 25 6 2 21 17 13 9 28 30 5 23 19 15 11 7 4 29 10 1 3 22 18 14 9 28 30 5 24 20 16 12 8 27 0 4 23 19 15 11 7 26 6 2 21 17 13 25 11 15 27 0 4 23 19 14 10 29 25 6 2 21 17 13 9 28 30 5 24 20 16 12 8 26 1 3 22 18 7 16 20 9 28 30 5 24 19 15 11 7 26 1 3 22 18 14 10 29 25 6 2 21 17 13 8 27 0 4 23 12 21 2 14 10 29 25 6 24 20 16 12 8 27 0 4 23 19 15 11 7 26 1 3 22 18 13 9 28 30 5 17 3 1 19 15 11 7 26 6 2 21 17 13 9 28 30 5 24 20 16 12 8 27 0 4 23 18 14 10 29 25 22 9 13 25 6 2 21 17 12 8 27 0 4 23 19 15 11 7 26 1 3 22 18 14 10 29 30 5 24 20 16 28 14 18 7 26 1 3 22 17 13 9 28 30 5 24 20 16 12 8 27 0 4 23 19 15 11 29 25 6 2 21 10 19 23 12 8 27 0 4 22 18 14 10 29 25 6 2 21 17 13 9 28 30 5 24 20 16 11 7 26 1 3 15 24 5 17 13 9 28 30 4 23 19 15 11 7 26 1 3 22 18 14 10 29 25 6 2 21 16 12 8 27 0 20 6 25 22 18 14 10 29 30 5 24 20 16 12 8 27 0 4 23 19 15 11 7 26 1 3 21 17 13 9 28 2 26 7 4 23 19 15 11 29 25 6 2 21 17 13 9 28 30 5 24 20 16 12 8 27 0 3 22 18 14 10 1 8 12 30 5 24 20 16 11 7 26 1 3 22 18 14 10 29 25 6 2 21 17 13 9 28 0 4 23 19 15 27 13 17 29 25 6 2 21 16 12 8 27 0 4 23 19 15 11 7 26 1 3 22 18 14 10 28 30 5 24 20 9 18 22 11 7 26 1 3 21 17 13 9 28 30 5 24 20 16 12 8 27 0 4 23 19 15 10 29 25 6 2 14 23 4 16 12 8 27 0 3 22 18 14 10 29 25 6 2 21 17 13 9 28 30 5 24 20 15 11 7 26 1 19 5 30 21 17 13 9 28 0 4 23 19 15 11 7 26 1 3 22 18 14 10 29 25 6 2 20 16 12 8 27 24 25 29 3 22 18 14 10 28 30 5 24 20 16 12 8 27 0 4 23 19 15 11 7 26 1 2 21 17 13 9 6 7 11 0 4 23 19 15 10 29 25 6 2 21 17 13 9 28 30 5 24 20 16 12 8 27 1 3 22 18 14 26 12 16 28 30 5 24 20 15 11 7 26 1 3 22 18 14 10 29 25 6 2 21 17 13 9 27 0 4 23 19 8 17 21 10 29 25 6 2 20 16 12 8 27 0 4 23 19 15 11 7 26 1 3 22 18 14 9 28 30 5 24 13 22 3 15 11 7 26 1 2 21 17 13 9 28 30 5 24 20 16 12 8 27 0 4 23 19 14 10 29 25 6 18 4 0 20 16 12 8 27 1 3 22 18 14 10 29 25 6 2 21 17 13 9 28 30 5 24 19 15 11 7 26 23 30 28 2 21 17 13 9 27 0 4 23 19 15 11 7 26 1 3 22 18 14 10 29 25 6 24 20 16 12 8 5 15 19 8 27 0 4 23 18 14 10 29 25 6 2 21 17 13 9 28 30 5 24 20 16 12 7 26 1 3 22 11 20 24 13 9 28 30 5 23 19 15 11 7 26 1 3 22 18 14 10 29 25 6 2 21 17 12 8 27 0 4 16 2 6 18 14 10 29 25 5 24 20 16 12 8 27 0 4 23 19 15 11 7 26 1 3 22 17 13 9 28 30 21 1 26 23 19 15 11 7 25 6 2 21 17 13 9 28 30 5 24 20 16 12 8 27 0 4 22 18 14 10 29 3 27 8 5 24 20 16 12 7 26 1 3 22 18 14 10 29 25 6 2 21 17 13 9 28 30 4 23 19 15 11 0 10 14 26 1 3 22 18 13 9 28 30 5 24 20 16 12 8 27 0 4 23 19 15 11 7 25 6 2 21 17 29 -- cycle notation: 0: (0 28 16 26 24 25 5 17 1 9) (2 6 13 15 7 8 27 20 18 3) (4 21 14 11 23 29 12 19 22 10) (30) 1: (1 27 15 25 23 30 4 16 6 8) (2 24 5 12 14 29 7 26 19 17) (3 20 13 10 22 28 11 18 21 9) (0) 2: (2 1 10 5 18 4 22 11 24 26) (3) (6 14 12 20 19 23 7 9 30 25) (8 28 17 0 29 13 16 27 21 15) 3: (3 0 11 6 19 5 23 12 2 27) (4) (7 14 17 28 22 16 9 29 18 30) (8 10 25 26 1 15 13 21 20 24) 4: (4 30 12 1 20 6 24 13 3 28) (5) (7 19 25 8 15 18 29 23 17 10) (9 11 26 27 0 16 14 22 21 2) 5: (5 25 13 0 21 1 2 14 4 29) (6) (7 24 18 11 8 20 26 9 16 19) (10 12 27 28 30 17 15 23 22 3) 6: (6 26 14 30 22 0 3 15 5 7) (8 2 19 12 9 21 27 10 17 20) (11 13 28 29 25 18 16 24 23 4) (1) 7: (7 12 23 10 0 9 27 24 29 16) (8) (11 4 2 25 30 28 20 22 14 15) (13 19 3 6 17 26 5 21 18 1) 8: (8 13 24 11 30 10 28 2 7 17) (9) (12 5 3 26 25 29 21 23 15 16) (14 20 4 1 18 27 6 22 19 0) 9: (9 14 2 12 25 11 29 3 8 18) (10) (13 6 4 27 26 7 22 24 16 17) (15 21 5 0 19 28 1 23 20 30) 10: (10 15 3 13 26 12 7 4 9 19) (11) (14 1 5 28 27 8 23 2 17 18) (16 22 6 30 20 29 0 24 21 25) 11: (11 16 4 14 27 13 8 5 10 20) (12) (15 0 6 29 28 9 24 3 18 19) (17 23 1 25 21 7 30 2 22 26) 12: (12 17 5 15 28 14 9 6 11 21) (13) (16 30 1 7 29 10 2 4 19 20) (18 24 0 26 22 8 25 3 23 27) 13: (13 18 6 16 29 15 10 1 12 22) (14) (17 25 0 8 7 11 3 5 20 21) (19 2 30 27 23 9 26 4 24 28) 14: (14 19 1 17 7 16 11 0 13 23) (15) (18 26 30 9 8 12 4 6 21 22) (20 3 25 28 24 10 27 5 2 29) 15: (15 20 0 18 8 17 12 30 14 24) (16) (19 27 25 10 9 13 5 1 22 23) (21 4 26 29 2 11 28 6 3 7) 16: (16 21 30 19 9 18 13 25 15 2) (17) (20 28 26 11 10 14 6 0 23 24) (22 5 27 7 3 12 29 1 4 8) 17: (17 22 25 20 10 19 14 26 16 3) (18) (21 29 27 12 11 15 1 30 24 2) (23 6 28 8 4 13 7 0 5 9) 18: (18 23 26 21 11 20 15 27 17 4) (19) (22 7 28 13 12 16 0 25 2 3) (24 1 29 9 5 14 8 30 6 10) 19: (19 24 27 22 12 21 16 28 18 5) (20) (23 8 29 14 13 17 30 26 3 4) (25 1 11 2 0 7 10 6 15 9) 20: (20 2 28 23 13 22 17 29 19 6) (21) (24 9 7 15 14 18 25 27 4 5) (26 0 12 3 30 8 11 1 16 10) 21: (21 3 29 24 14 23 18 7 20 1) (22) (25 9 12 0 17 11 27 30 13 4) (26 28 5 6 2 10 8 16 15 19) 22: (22 4 7 2 15 24 19 8 21 0) (23) (25 14 5 26 10 13 30 18 12 28) (27 29 6 1 3 11 9 17 16 20) 23: (23 5 8 3 16 2 20 9 22 30) (24) (25 19 13 29 26 15 6 27 11 14) (28 7 1 0 4 12 10 18 17 21) 24: (24 6 9 4 17 3 21 10 23 25) (26 20 14 7 27 16 1 28 12 15) (29 8 0 30 5 13 11 19 18 22) (2) 25: (25 7 18 28 3 27 1 19 30 11) (26) (29 22 20 5 4 0 15 17 9 10) (2 8 14 21 24 12 6 23 16 13) 26: (26 8 19 29 4 28 0 20 25 12) (27) (30 16 18 10 11 7 23 21 6 5) (1 24 17 14 3 9 15 22 2 13) 27: (27 9 20 7 5 29 30 21 26 13) (28) (0 2 18 15 4 10 16 23 3 14) (1 6 25 17 19 11 12 8 24 22) 28: (28 10 21 8 6 7 25 22 27 14) (29) (30 3 19 16 5 11 17 24 4 15) (0 1 26 18 20 12 13 9 2 23) 29: (29 11 22 9 1 8 26 23 28 15) (30 0 27 19 21 13 14 10 3 24) (2 5 16 25 4 20 17 6 12 18) (7) 30: (30 29 17 27 2 26 6 18 0 10) (1 14 16 8 9 28 21 19 4 3) (5 22 15 12 24 7 13 20 23 11) (25) -- autom facts: AUTOM: (0 1 6 5 4 3 2 24 23 22 21 20 19 18 17 16 15 14 13 12 11 10 9 8 7 29 28 27 26 25 30) Equational facts: X = (f (f (f X X) X) X) X = (f (f (f X Y) Y) Y) X = (f Y (f X (f (f Y X) Y))) (f X (f X Y)) = (f Y (f Y X)) X = (f X (f X (f (f X X) X))) (f X 29) = (f (f X X) 20) 17 = (f (f (f 17 X) X) X) (f 19 X) = (f 23 (f X X)) 11 = (f (f (f 11 X) X) X) (f 11 X) = (f 15 (f X X)) 16 = (f (f (f 16 X) X) X) 29 = (f (f (f 29 X) X) X) (f X 26) = (f (f X X) 17) (f X X) = (f (f (f (f X X) Y) Y) Y) (f X 21) = (f (f X X) 27) 6 = (f (f (f 6 X) X) X) (f X 1) = (f (f X X) 13) (f X 13) = (f (f X X) 4) (f 22 X) = (f 3 (f X X)) 26 = (f (f (f 26 X) X) X) --------------------------------------- Model 31_1: 0 30 16 4 27 18 2 13 28 26 8 5 11 20 19 24 1 25 21 23 15 10 14 3 6 22 12 29 9 17 7 18 1 30 17 5 28 19 3 14 29 27 9 6 12 21 20 25 2 26 22 24 16 11 15 4 7 23 13 0 10 8 11 19 2 30 18 6 29 20 4 15 0 28 10 7 13 22 21 26 3 27 23 25 17 12 16 5 8 24 14 1 9 2 12 20 3 30 19 7 0 21 5 16 1 29 11 8 14 23 22 27 4 28 24 26 18 13 17 6 9 25 15 10 16 3 13 21 4 30 20 8 1 22 6 17 2 0 12 9 15 24 23 28 5 29 25 27 19 14 18 7 10 26 11 27 17 4 14 22 5 30 21 9 2 23 7 18 3 1 13 10 16 25 24 29 6 0 26 28 20 15 19 8 11 12 12 28 18 5 15 23 6 30 22 10 3 24 8 19 4 2 14 11 17 26 25 0 7 1 27 29 21 16 20 9 13 10 13 29 19 6 16 24 7 30 23 11 4 25 9 20 5 3 15 12 18 27 26 1 8 2 28 0 22 17 21 14 22 11 14 0 20 7 17 25 8 30 24 12 5 26 10 21 6 4 16 13 19 28 27 2 9 3 29 1 23 18 15 19 23 12 15 1 21 8 18 26 9 30 25 13 6 27 11 22 7 5 17 14 20 29 28 3 10 4 0 2 24 16 25 20 24 13 16 2 22 9 19 27 10 30 26 14 7 28 12 23 8 6 18 15 21 0 29 4 11 5 1 3 17 4 26 21 25 14 17 3 23 10 20 28 11 30 27 15 8 29 13 24 9 7 19 16 22 1 0 5 12 6 2 18 3 5 27 22 26 15 18 4 24 11 21 29 12 30 28 16 9 0 14 25 10 8 20 17 23 2 1 6 13 7 19 8 4 6 28 23 27 16 19 5 25 12 22 0 13 30 29 17 10 1 15 26 11 9 21 18 24 3 2 7 14 20 15 9 5 7 29 24 28 17 20 6 26 13 23 1 14 30 0 18 11 2 16 27 12 10 22 19 25 4 3 8 21 9 16 10 6 8 0 25 29 18 21 7 27 14 24 2 15 30 1 19 12 3 17 28 13 11 23 20 26 5 4 22 5 10 17 11 7 9 1 26 0 19 22 8 28 15 25 3 16 30 2 20 13 4 18 29 14 12 24 21 27 6 23 7 6 11 18 12 8 10 2 27 1 20 23 9 29 16 26 4 17 30 3 21 14 5 19 0 15 13 25 22 28 24 29 8 7 12 19 13 9 11 3 28 2 21 24 10 0 17 27 5 18 30 4 22 15 6 20 1 16 14 26 23 25 24 0 9 8 13 20 14 10 12 4 29 3 22 25 11 1 18 28 6 19 30 5 23 16 7 21 2 17 15 27 26 28 25 1 10 9 14 21 15 11 13 5 0 4 23 26 12 2 19 29 7 20 30 6 24 17 8 22 3 18 16 27 17 29 26 2 11 10 15 22 16 12 14 6 1 5 24 27 13 3 20 0 8 21 30 7 25 18 9 23 4 19 28 20 18 0 27 3 12 11 16 23 17 13 15 7 2 6 25 28 14 4 21 1 9 22 30 8 26 19 10 24 5 29 6 21 19 1 28 4 13 12 17 24 18 14 16 8 3 7 26 29 15 5 22 2 10 23 30 9 27 20 11 25 0 26 7 22 20 2 29 5 14 13 18 25 19 15 17 9 4 8 27 0 16 6 23 3 11 24 30 10 28 21 12 1 13 27 8 23 21 3 0 6 15 14 19 26 20 16 18 10 5 9 28 1 17 7 24 4 12 25 30 11 29 22 2 23 14 28 9 24 22 4 1 7 16 15 20 27 21 17 19 11 6 10 29 2 18 8 25 5 13 26 30 12 0 3 1 24 15 29 10 25 23 5 2 8 17 16 21 28 22 18 20 12 7 11 0 3 19 9 26 6 14 27 30 13 4 14 2 25 16 0 11 26 24 6 3 9 18 17 22 29 23 19 21 13 8 12 1 4 20 10 27 7 15 28 30 5 30 15 3 26 17 1 12 27 25 7 4 10 19 18 23 0 24 20 22 14 9 13 2 5 21 11 28 8 16 29 6 21 22 23 24 25 26 27 28 29 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 30 -- cycle notation: 0: (0) (1 30 7 13 20 15 24 6 2 16) (3 4 27 29 17 25 22 14 19 23) (5 18 21 10 8 28 9 26 12 11) 1: (1) (2 30 8 14 21 16 25 7 3 17) (4 5 28 0 18 26 23 15 20 24) (6 19 22 11 9 29 10 27 13 12) 2: (2) (3 30 9 15 22 17 26 8 4 18) (5 6 29 1 19 27 24 16 21 25) (7 20 23 12 10 0 11 28 14 13) 3: (3) (4 30 10 16 23 18 27 9 5 19) (6 7 0 2 20 28 25 17 22 26) (8 21 24 13 11 1 12 29 15 14) 4: (4) (5 30 11 17 24 19 28 10 6 20) (7 8 1 3 21 29 26 18 23 27) (9 22 25 14 12 2 13 0 16 15) 5: (5) (6 30 12 18 25 20 29 11 7 21) (8 9 2 4 22 0 27 19 24 28) (10 23 26 15 13 3 14 1 17 16) 6: (6) (7 30 13 19 26 21 0 12 8 22) (9 10 3 5 23 1 28 20 25 29) (11 24 27 16 14 4 15 2 18 17) 7: (7) (8 30 14 20 27 22 1 13 9 23) (10 11 4 6 24 2 29 21 26 0) (12 25 28 17 15 5 16 3 19 18) 8: (8) (9 30 15 21 28 23 2 14 10 24) (11 12 5 7 25 3 0 22 27 1) (13 26 29 18 16 6 17 4 20 19) 9: (9) (10 30 16 22 29 24 3 15 11 25) (12 13 6 8 26 4 1 23 28 2) (14 27 0 19 17 7 18 5 21 20) 10: (10) (11 30 17 23 0 25 4 16 12 26) (13 14 7 9 27 5 2 24 29 3) (15 28 1 20 18 8 19 6 22 21) 11: (11) (12 30 18 24 1 26 5 17 13 27) (14 15 8 10 28 6 3 25 0 4) (16 29 2 21 19 9 20 7 23 22) 12: (12) (13 30 19 25 2 27 6 18 14 28) (15 16 9 11 29 7 4 26 1 5) (17 0 3 22 20 10 21 8 24 23) 13: (13) (14 30 20 26 3 28 7 19 15 29) (16 17 10 12 0 8 5 27 2 6) (18 1 4 23 21 11 22 9 25 24) 14: (14) (15 30 21 27 4 29 8 20 16 0) (17 18 11 13 1 9 6 28 3 7) (19 2 5 24 22 12 23 10 26 25) 15: (15) (16 30 22 28 5 0 9 21 17 1) (18 19 12 14 2 10 7 29 4 8) (20 3 6 25 23 13 24 11 27 26) 16: (16) (17 30 23 29 6 1 10 22 18 2) (19 20 13 15 3 11 8 0 5 9) (21 4 7 26 24 14 25 12 28 27) 17: (17) (18 30 24 0 7 2 11 23 19 3) (20 21 14 16 4 12 9 1 6 10) (22 5 8 27 25 15 26 13 29 28) 18: (18) (19 30 25 1 8 3 12 24 20 4) (21 22 15 17 5 13 10 2 7 11) (23 6 9 28 26 16 27 14 0 29) 19: (19) (20 30 26 2 9 4 13 25 21 5) (22 23 16 18 6 14 11 3 8 12) (24 7 10 29 27 17 28 15 1 0) 20: (20) (21 30 27 3 10 5 14 26 22 6) (23 24 17 19 7 15 12 4 9 13) (25 8 11 0 28 18 29 16 2 1) 21: (21) (22 30 28 4 11 6 15 27 23 7) (24 25 18 20 8 16 13 5 10 14) (26 9 12 1 29 19 0 17 3 2) 22: (22) (23 30 29 5 12 7 16 28 24 8) (25 26 19 21 9 17 14 6 11 15) (27 10 13 2 0 20 1 18 4 3) 23: (23) (24 30 0 6 13 8 17 29 25 9) (26 27 20 22 10 18 15 7 12 16) (28 11 14 3 1 21 2 19 5 4) 24: (24) (25 30 1 7 14 9 18 0 26 10) (27 28 21 23 11 19 16 8 13 17) (29 12 15 4 2 22 3 20 6 5) 25: (25) (26 30 2 8 15 10 19 1 27 11) (28 29 22 24 12 20 17 9 14 18) (0 13 16 5 3 23 4 21 7 6) 26: (26) (27 30 3 9 16 11 20 2 28 12) (29 0 23 25 13 21 18 10 15 19) (1 14 17 6 4 24 5 22 8 7) 27: (27) (28 30 4 10 17 12 21 3 29 13) (0 1 24 26 14 22 19 11 16 20) (2 15 18 7 5 25 6 23 9 8) 28: (28) (29 30 5 11 18 13 22 4 0 14) (1 2 25 27 15 23 20 12 17 21) (3 16 19 8 6 26 7 24 10 9) 29: (29) (30 6 12 19 14 23 5 1 15 0) (2 3 26 28 16 24 21 13 18 22) (4 17 20 9 7 27 8 25 11 10) 30: (30) (0 21 12 3 24 15 6 27 18 9) (1 22 13 4 25 16 7 28 19 10) (2 23 14 5 26 17 8 29 20 11) -- autom facts: AUTOM: (0) (1 26 25 16 9 17 2 28 29 6 8 27 24 10 4 15 21 3 20 18 23 13 5 19 7 11 14 30 12 22) (0 8 12 3 21 1 17 14 9 7 20 13 19 30 4 28 5 22 24 29 2 16 6 18 27 23 15 26 25 10 11) Equational facts: X = (f X X) (f X Y) = (f (f (f Y X) X) X) (f X Y) = (f (f X Y) (f X Y)) X = (f Y (f X (f Y (f X Y)))) (f X (f Y X)) = (f (f X Y) X) X = (g X X) (f (f X Y) Y) = (f (f Y (f X Y)) X) (f X 11) = (f (f (f 11 X) X) X) (f (f X 23) X) = (f X (f 23 X)) (f X 30) = (f (f (f 30 X) X) X) (f (f X 28) X) = (f X (f 28 X)) (f X (f 27 X)) = (f (f X 27) X) (f X (f 17 X)) = (f (f X 17) X) (f X (f 4 X)) = (f (f X 4) X) (f (f X 3) X) = (f X (f 3 X)) (f X 26) = (f (f (f 26 X) X) X) (f X 2) = (f (f (f 2 X) X) X) (f X (f 15 X)) = (f (f X 15) X) (f X 4) = (f (f (f 4 X) X) X) (f (f X 6) X) = (f X (f 6 X)) --------------------------------------- Model 31_2: 0 30 26 18 13 22 9 19 21 4 3 29 8 20 6 27 15 11 24 17 5 25 23 28 12 1 7 2 14 16 10 7 1 30 27 19 14 23 10 20 22 5 4 15 9 21 17 28 16 12 25 18 6 26 24 29 13 2 8 3 0 11 22 8 2 30 28 20 0 24 11 21 23 6 5 16 10 1 18 29 17 13 26 19 7 27 25 15 14 3 9 4 12 11 23 9 3 30 29 21 1 25 12 22 24 7 6 17 5 2 19 15 18 14 27 20 8 28 26 16 0 4 10 13 18 12 24 10 4 30 15 22 2 26 13 23 25 8 7 11 6 3 20 16 19 0 28 21 9 29 27 17 1 5 14 8 19 13 25 11 5 30 16 23 3 27 14 24 26 9 6 12 7 4 21 17 20 1 29 22 10 15 28 18 2 0 10 9 20 14 26 12 6 30 17 24 4 28 0 25 27 3 7 13 8 5 22 18 21 2 15 23 11 16 29 19 1 28 11 10 21 0 27 13 7 30 18 25 5 29 1 26 20 4 8 14 9 6 23 19 22 3 16 24 12 17 15 2 27 29 12 11 22 1 28 14 8 30 19 26 6 15 2 16 21 5 9 0 10 7 24 20 23 4 17 25 13 18 3 3 28 15 13 12 23 2 29 0 9 30 20 27 7 16 19 17 22 6 10 1 11 8 25 21 24 5 18 26 14 4 17 4 29 16 14 13 24 3 15 1 10 30 21 28 8 0 20 18 23 7 11 2 12 9 26 22 25 6 19 27 5 9 18 5 15 17 0 14 25 4 16 2 11 30 22 29 28 1 21 19 24 8 12 3 13 10 27 23 26 7 20 6 15 10 19 6 16 18 1 0 26 5 17 3 12 30 23 21 29 2 22 20 25 9 13 4 14 11 28 24 27 8 7 24 16 11 20 7 17 19 2 1 27 6 18 4 13 30 9 22 15 3 23 21 26 10 14 5 0 12 29 25 28 8 30 25 17 12 21 8 18 20 3 2 28 7 19 5 14 29 10 23 16 4 24 22 27 11 0 6 1 13 15 26 9 20 5 3 8 27 16 22 17 29 11 7 10 26 4 12 15 30 6 13 28 2 24 14 1 19 18 9 23 0 21 25 13 21 6 4 9 28 17 23 18 15 12 8 11 27 5 22 16 30 7 14 29 3 25 0 2 20 19 10 24 1 26 6 14 22 7 5 10 29 18 24 19 16 13 9 12 28 2 23 17 30 8 0 15 4 26 1 3 21 20 11 25 27 29 7 0 23 8 6 11 15 19 25 20 17 14 10 13 26 3 24 18 30 9 1 16 5 27 2 4 22 21 12 28 14 15 8 1 24 9 7 12 16 20 26 21 18 0 11 13 27 4 25 19 30 10 2 17 6 28 3 5 23 22 29 12 0 16 9 2 25 10 8 13 17 21 27 22 19 1 23 14 28 5 26 20 30 11 3 18 7 29 4 6 24 15 2 13 1 17 10 3 26 11 9 14 18 22 28 23 20 25 24 0 29 6 27 21 30 12 4 19 8 15 5 7 16 21 3 14 2 18 11 4 27 12 10 0 19 23 29 24 8 26 25 1 15 7 28 22 30 13 5 20 9 16 6 17 25 22 4 0 3 19 12 5 28 13 11 1 20 24 15 7 9 27 26 2 16 8 29 23 30 14 6 21 10 17 18 16 26 23 5 1 4 20 13 6 29 14 12 2 21 25 18 8 10 28 27 3 17 9 15 24 30 0 7 22 11 19 26 17 27 24 6 2 5 21 14 7 15 0 13 3 22 12 19 9 11 29 28 4 18 10 16 25 30 1 8 23 20 23 27 18 28 25 7 3 6 22 0 8 16 1 14 4 24 13 20 10 12 15 29 5 19 11 17 26 30 2 9 21 5 24 28 19 29 26 8 4 7 23 1 9 17 2 0 10 25 14 21 11 13 16 15 6 20 12 18 27 30 3 22 1 6 25 29 20 15 27 9 5 8 24 2 10 18 3 4 11 26 0 22 12 14 17 16 7 21 13 19 28 30 23 4 2 7 26 15 21 16 28 10 6 9 25 3 11 19 30 5 12 27 1 23 13 0 18 17 8 22 14 20 29 24 19 20 21 22 23 24 25 26 27 28 29 15 16 17 18 14 0 1 2 3 4 5 6 7 8 9 10 11 12 13 30 -- cycle notation: 0: (0) (1 30 10 3 18 24 12 8 21 25) (2 26 7 19 17 11 29 16 15 27) (4 13 20 5 22 23 28 14 6 9) 1: (1) (2 30 11 4 19 25 13 9 22 26) (3 27 8 20 18 12 15 17 16 28) (5 14 21 6 23 24 29 0 7 10) 2: (2) (3 30 12 5 20 26 14 10 23 27) (4 28 9 21 19 13 16 18 17 29) (6 0 22 7 24 25 15 1 8 11) 3: (3) (4 30 13 6 21 27 0 11 24 28) (5 29 10 22 20 14 17 19 18 15) (7 1 23 8 25 26 16 2 9 12) 4: (4) (5 30 14 7 22 28 1 12 25 29) (6 15 11 23 21 0 18 20 19 16) (8 2 24 9 26 27 17 3 10 13) 5: (5) (6 30 0 8 23 29 2 13 26 15) (7 16 12 24 22 1 19 21 20 17) (9 3 25 10 27 28 18 4 11 14) 6: (6) (7 30 1 9 24 15 3 14 27 16) (8 17 13 25 23 2 20 22 21 18) (10 4 26 11 28 29 19 5 12 0) 7: (7) (8 30 2 10 25 16 4 0 28 17) (9 18 14 26 24 3 21 23 22 19) (11 5 27 12 29 15 20 6 13 1) 8: (8) (9 30 3 11 26 17 5 1 29 18) (10 19 0 27 25 4 22 24 23 20) (12 6 28 13 15 16 21 7 14 2) 9: (9) (10 30 4 12 27 18 6 2 15 19) (11 20 1 28 26 5 23 25 24 21) (13 7 29 14 16 17 22 8 0 3) 10: (10) (11 30 5 13 28 19 7 3 16 20) (12 21 2 29 27 6 24 26 25 22) (14 8 15 0 17 18 23 9 1 4) 11: (11) (12 30 6 14 29 20 8 4 17 21) (13 22 3 15 28 7 25 27 26 23) (16 1 18 19 24 10 2 5 0 9) 12: (12) (13 30 7 0 15 21 9 5 18 22) (14 23 4 16 29 8 26 28 27 24) (17 2 19 20 25 11 3 6 1 10) 13: (13) (14 30 8 1 16 22 10 6 19 23) (15 9 27 29 28 25 0 24 5 17) (18 3 20 21 26 12 4 7 2 11) 14: (14) (15 29 26 1 25 6 18 16 10 28) (17 23 11 7 20 24 0 30 9 2) (19 4 21 22 27 13 5 8 3 12) 15: (15) (16 30 25 18 13 4 27 23 1 5) (17 6 22 14 12 26 9 11 10 7) (19 28 0 20 2 3 8 29 21 24) 16: (16) (17 30 26 19 14 5 28 24 2 6) (18 7 23 0 13 27 10 12 11 8) (20 29 1 21 3 4 9 15 22 25) 17: (17) (18 30 27 20 0 6 29 25 3 7) (19 8 24 1 14 28 11 13 12 9) (21 15 2 22 4 5 10 16 23 26) 18: (18) (19 30 28 21 1 7 15 26 4 8) (20 9 25 2 0 29 12 14 13 10) (22 16 3 23 5 6 11 17 24 27) 19: (19) (20 30 29 22 2 8 16 27 5 9) (21 10 26 3 1 15 13 0 14 11) (23 17 4 24 6 7 12 18 25 28) 20: (20) (21 30 15 23 3 9 17 28 6 10) (22 11 27 4 2 16 14 1 0 12) (24 18 5 25 7 8 13 19 26 29) 21: (21) (22 30 16 24 4 10 18 29 7 11) (23 12 28 5 3 17 0 2 1 13) (25 19 6 26 8 9 14 20 27 15) 22: (22) (23 30 17 25 5 11 19 15 8 12) (24 13 29 6 4 18 1 3 2 14) (26 20 7 27 9 10 0 21 28 16) 23: (23) (24 30 18 26 6 12 20 16 9 13) (25 14 15 7 5 19 2 4 3 0) (27 21 8 28 10 11 1 22 29 17) 24: (24) (25 30 19 27 7 13 21 17 10 14) (26 0 16 8 6 20 3 5 4 1) (28 22 9 29 11 12 2 23 15 18) 25: (25) (26 30 20 28 8 14 22 18 11 0) (27 1 17 9 7 21 4 6 5 2) (29 23 10 15 12 13 3 24 16 19) 26: (26) (27 30 21 29 9 0 23 19 12 1) (28 2 18 10 8 22 5 7 6 3) (4 25 17 20 15 24 11 16 13 14) 27: (27) (28 30 22 15 10 1 24 20 13 2) (29 3 19 11 9 23 6 8 7 4) (0 5 26 18 21 16 25 12 17 14) 28: (28) (29 30 23 16 11 2 25 21 14 3) (0 1 6 27 19 22 17 26 13 18) (4 20 12 10 24 7 9 8 5 15) 29: (29) (30 24 17 12 3 26 22 0 4 15) (1 2 7 28 20 23 18 27 14 19) (5 21 13 11 25 8 10 9 6 16) 30: (30) (0 19 3 22 6 25 9 28 12 16) (1 20 4 23 7 26 10 29 13 17) (2 21 5 24 8 27 11 15 14 18) -- autom facts: AUTOM: (0) (1 26 22 8 15 13 18 11 6 30 7 23 21 27 20 24 29 9 10 19 28 25 2 5 12 16 4 3 17 14) (0 23 5 15 13 25 29 16 9 3 8 1 17 12 11 20 14 2 30 27 24 10 21 22 7 26 18 28 19 6 4) Equational facts: X = (f X X) X = (f (f (f X Y) Y) Y) (f (f X Y) X) = (f X (f Y X)) (f X (f X Y)) = (f Y (f Y X)) X = (g X X) (f X Y) = (f (f X Y) (f X Y)) X = (f Y (f X (f (f Y X) Y))) 11 = (f (f (f 11 X) X) X) 18 = (f (f (f 18 X) X) X) 22 = (f (f (f 22 X) X) X) 0 = (f (f (f 0 X) X) X) 27 = (f (f (f 27 X) X) X) 24 = (f (f (f 24 X) X) X) 28 = (f (f (f 28 X) X) X) 10 = (f (f (f 10 X) X) X) (f X Y) = (f (f (f (f X Y) X) X) X) (f X Y) = (f Y (f (f Y X) (f X Y))) 17 = (f (f (f 17 X) X) X) 4 = (f (f (f 4 X) X) X) 30 = (f (f (f 30 X) X) X) --------------------------------------- Model 31_3: 0 24 30 1 12 25 19 29 13 10 3 27 18 15 11 4 23 26 6 5 14 16 21 9 28 8 7 2 22 20 17 30 1 26 14 24 2 28 12 18 5 29 9 17 10 20 22 25 3 4 13 8 23 11 15 7 6 27 21 19 0 16 25 30 2 26 0 13 14 20 27 28 11 4 9 19 16 24 5 21 12 7 3 10 17 22 8 29 6 18 1 23 15 2 26 21 3 30 18 8 0 9 7 20 22 15 28 23 1 13 11 24 27 29 5 16 19 6 12 4 17 14 25 10 24 22 1 19 4 30 10 6 2 23 8 18 21 16 29 9 0 14 27 25 28 20 3 17 5 7 13 26 15 12 11 23 0 25 30 20 5 1 11 7 19 21 6 27 22 17 12 10 2 29 28 26 15 18 4 14 3 8 13 24 16 9 21 3 11 29 26 17 6 30 15 27 0 19 10 7 25 14 18 20 1 9 12 13 23 28 4 24 22 16 8 2 5 4 9 22 15 27 24 16 7 30 20 28 2 26 11 8 18 12 19 13 0 10 29 14 21 23 5 25 1 17 6 3 10 23 5 25 16 28 30 17 8 1 18 29 6 24 9 20 19 13 11 14 2 22 27 12 26 21 3 7 0 15 4 11 29 20 12 3 16 4 26 10 9 30 28 5 27 2 8 17 0 14 15 24 18 25 7 22 1 19 23 6 21 13 27 18 9 17 13 4 11 5 24 29 10 30 1 3 28 2 6 15 25 12 16 8 19 26 20 23 0 22 21 7 14 19 10 28 5 15 14 25 9 3 30 27 11 29 0 4 16 1 7 17 26 13 24 6 20 2 18 21 8 23 22 12 28 5 7 13 10 8 2 15 29 26 9 20 12 30 22 23 14 27 16 3 18 1 4 0 21 17 11 6 25 19 24 3 8 29 6 14 11 27 1 16 18 24 10 23 13 30 28 21 12 19 17 4 2 0 5 9 22 15 20 7 26 25 6 27 4 9 7 12 17 28 0 11 19 25 30 21 14 13 29 22 5 20 15 3 1 2 16 10 23 24 18 8 26 1 19 14 28 22 26 5 4 21 25 6 17 11 23 12 15 30 8 9 2 7 0 29 16 13 27 18 3 10 24 20 20 12 0 24 29 23 22 3 5 15 26 7 13 9 21 6 16 30 8 10 1 17 2 27 19 14 28 25 4 11 18 13 2 18 21 25 27 3 23 4 8 16 24 22 14 10 30 7 17 0 6 11 28 15 1 29 20 12 9 26 5 19 22 15 19 10 9 1 23 27 26 0 7 21 3 20 6 17 24 28 18 30 5 12 8 11 25 13 2 14 16 4 29 16 20 23 0 11 10 24 21 28 22 2 8 7 4 18 29 15 25 3 19 30 9 13 6 1 26 14 5 12 17 27 18 21 17 11 2 9 29 25 22 6 23 1 19 8 5 26 27 16 30 4 20 7 10 14 12 0 24 15 3 13 28 29 6 12 4 8 20 9 14 23 17 1 5 25 18 26 7 11 24 28 16 22 21 30 13 15 19 10 0 27 3 2 7 13 27 18 5 6 21 10 12 3 15 0 24 26 19 25 8 9 23 29 17 14 22 30 11 16 20 4 2 28 1 14 28 8 7 19 3 13 22 11 2 4 16 20 25 24 10 26 6 15 21 27 30 12 23 18 9 17 29 5 1 0 17 11 16 20 21 15 12 2 19 4 25 14 28 6 13 3 9 23 26 22 0 27 5 8 24 30 1 10 29 18 7 9 17 15 16 18 22 20 13 1 12 5 26 14 29 7 21 4 10 2 24 23 6 28 3 0 25 30 19 11 27 8 15 16 10 23 17 19 0 18 14 24 13 3 8 12 27 11 22 5 21 1 25 4 7 29 30 2 26 28 20 9 6 5 25 13 2 23 7 26 16 6 14 17 12 4 1 15 0 28 18 20 8 21 19 9 24 3 11 29 27 30 10 22 26 14 3 8 1 21 7 24 17 13 12 15 16 5 0 19 2 29 22 18 6 25 20 10 27 4 9 11 28 30 23 12 4 24 22 6 0 15 8 25 16 14 13 2 17 3 27 20 1 7 23 19 11 26 18 10 28 5 30 9 29 21 8 7 6 27 28 29 18 19 20 21 22 23 0 2 1 5 3 4 10 11 9 26 24 25 17 15 16 12 13 14 30 -- cycle notation: 0: (0) (1 24 28 22 21 16 23 9 10 3) (2 30 17 26 7 29 20 14 11 27) (4 12 18 6 19 5 25 8 13 15) 1: (1) (2 26 27 21 23 15 22 11 9 5) (3 14 20 8 18 4 24 7 12 17) (6 28 19 13 10 29 0 30 16 25) 2: (2) (3 26 6 14 16 5 13 19 7 20) (4 0 25 29 23 22 17 21 10 11) (8 27 18 12 9 28 1 30 15 24) 3: (3) (4 30 10 20 29 25 12 15 1 26) (5 18 24 6 8 9 7 0 2 21) (11 22 16 13 28 14 23 19 27 17) 4: (4) (5 30 11 18 27 26 13 16 0 24) (6 10 8 2 1 22 3 19 25 7) (9 23 17 14 29 12 21 20 28 15) 5: (5) (6 1 0 23 4 20 26 8 7 11) (9 19 28 24 14 17 2 25 3 30) (10 21 15 12 27 13 22 18 29 16) 6: (6) (7 30 5 17 20 12 10 0 21 13) (8 15 14 25 24 4 26 22 23 28) (9 27 16 18 1 3 29 2 11 19) 7: (7) (8 30 3 15 18 13 11 2 22 14) (9 20 10 28 17 19 0 4 27 1) (12 26 25 5 24 23 21 29 6 16) 8: (8) (9 1 23 12 6 30 4 16 19 14) (10 18 11 29 15 20 2 5 28 0) (13 24 26 3 25 21 22 27 7 17) 9: (9) (10 30 13 27 23 7 26 19 15 8) (11 28 6 4 3 12 5 16 17 0) (14 2 20 24 22 25 1 29 21 18) 10: (10) (11 30 14 28 21 8 24 20 16 6) (12 1 18 25 23 26 0 27 22 19) (13 3 17 15 2 9 29 7 5 4) 11: (11) (12 29 22 6 25 18 17 7 9 30) (13 0 19 26 21 24 2 28 23 20) (14 4 15 16 1 10 27 8 3 5) 12: (12) (13 30 24 21 1 5 8 29 19 3) (14 22 4 10 9 26 11 20 18 16) (15 23 0 28 25 17 27 6 2 7) 13: (13) (14 30 25 22 0 3 6 27 20 4) (15 28 7 1 8 16 21 2 29 26) (17 12 23 5 11 10 24 9 18 19) 14: (14) (15 13 21 3 9 11 25 10 19 20) (16 29 8 0 6 17 22 1 27 24) (18 5 12 30 26 23 2 4 7 28) 15: (15) (16 30 20 7 4 22 29 24 13 23) (17 8 21 0 1 19 2 14 12 11) (18 9 25 27 3 28 10 6 5 26) 16: (16) (17 30 18 8 5 23 27 25 14 21) (19 10 26 28 4 29 11 7 3 24) (20 1 12 13 9 15 6 22 2 0) 17: (17) (18 0 13 14 10 16 7 23 1 2) (19 6 3 21 28 26 12 22 15 30) (20 11 24 29 5 27 9 8 4 25) 18: (18) (19 30 29 4 9 0 22 8 26 2) (20 5 1 15 17 28 16 24 25 13) (21 12 3 10 7 27 14 6 23 11) 19: (19) (20 30 27 5 10 2 23 6 24 1) (21 9 22 13 4 11 8 28 12 7) (25 26 14 18 3 0 16 15 29 17) 20: (20) (21 7 25 0 18 30 28 3 11 1) (22 10 23 14 5 9 6 29 13 8) (24 12 19 4 2 17 16 27 15 26) 21: (21) (22 30 2 12 25 19 16 11 5 20) (23 13 18 28 27 0 29 3 4 8) (24 15 7 14 26 10 1 6 9 17) 22: (22) (23 30 1 13 26 20 17 9 3 18) (24 11 0 7 10 15 25 16 8 12) (27 4 5 6 21 14 19 29 28 2) 23: (23) (24 18 15 10 4 19 21 30 0 14) (25 9 2 8 11 16 26 17 6 13) (27 29 1 28 5 3 7 22 12 20) 24: (24) (25 30 7 2 16 9 4 21 27 10) (26 1 11 14 13 6 12 28 29 18) (0 17 23 8 19 22 5 15 3 20) 25: (25) (26 30 8 1 17 10 5 22 28 11) (27 19 24 0 9 12 14 7 13 29) (2 15 21 6 20 23 3 16 4 18) 26: (26) (27 28 20 25 2 10 13 12 8 14) (29 9 24 30 6 0 15 11 3 23) (1 16 22 7 18 21 4 17 5 19) 27: (27) (28 30 22 9 14 15 0 5 7 16) (29 10 17 18 20 21 19 8 6 26) (1 25 11 12 4 23 24 3 2 13) 28: (28) (29 30 23 10 12 16 2 3 8 17) (0 26 9 13 5 21 25 4 1 14) (6 7 24 27 11 15 19 18 22 20) 29: (29) (30 21 11 13 17 1 4 6 15 27) (0 12 2 24 10 14 3 22 26 5) (7 8 25 28 9 16 20 19 23 18) 30: (30) (0 8 20 9 21 26 16 3 27 12) (1 7 19 11 23 25 15 5 29 14) (2 6 18 10 22 24 17 4 28 13) -- autom facts: AUTOM: (0) (1 13 30 3 8 2 10 25 27 9 5 11 23 19 14 16 6 20 21 18 29 22 12 7 28 4 26 24 15 17) (0 8 15 2 12 28 17 30 6 10 21 24 7 16 26 4 5 11 1 27 23 3 22 13 20 14 9 25 29 19 18) Equational facts: X = (f X X) (f X (f Y X)) = (f (f X Y) X) X = (g X X) (f X Y) = (f (f X Y) (f X Y)) (f (f X Y) X) = (f X (f Y X)) X = (f Y (f X (f Y (f X Y)))) X = (f Y (f X (f (f Y X) Y))) (f X (f Y X)) = (f (f Y X) (f X Y)) (f X Y) = (f (f (f Y (f X Y)) X) X) (f X Y) = (f Y (f (f (f Y X) Y) X)) (f (f X Y) X) = (f (f Y X) (f X Y)) (f X Y) = (f (f (f (f Y X) Y) X) X) (f X Y) = (f Y (f (f Y (f X Y)) X)) (f (f X 26) X) = (f X (f 26 X)) (f X (f Y (f Y X))) = (f (f (f Y X) X) Y) (f (f X 16) X) = (f X (f 16 X)) (f X (f 17 X)) = (f (f X 17) X) (f (f X 18) X) = (f X (f 18 X)) (f (f (f X Y) X) X) = (f X (f (f Y X) X)) (f (f X 3) X) = (f X (f 3 X)) --------------------------------------- Model 31_4: 0 30 16 24 14 23 8 2 27 29 3 17 15 28 10 20 25 21 12 1 19 22 9 6 5 11 18 4 26 7 13 8 1 30 17 25 15 24 9 3 28 0 4 18 16 29 11 21 26 22 13 2 20 23 10 7 6 12 19 5 27 14 28 9 2 30 18 26 16 25 10 4 29 1 5 19 17 0 12 22 27 23 14 3 21 24 11 8 7 13 20 6 15 7 29 10 3 30 19 27 17 26 11 5 0 2 6 20 18 1 13 23 28 24 15 4 22 25 12 9 8 14 21 16 22 8 0 11 4 30 20 28 18 27 12 6 1 3 7 21 19 2 14 24 29 25 16 5 23 26 13 10 9 15 17 16 23 9 1 12 5 30 21 29 19 28 13 7 2 4 8 22 20 3 15 25 0 26 17 6 24 27 14 11 10 18 11 17 24 10 2 13 6 30 22 0 20 29 14 8 3 5 9 23 21 4 16 26 1 27 18 7 25 28 15 12 19 13 12 18 25 11 3 14 7 30 23 1 21 0 15 9 4 6 10 24 22 5 17 27 2 28 19 8 26 29 16 20 17 14 13 19 26 12 4 15 8 30 24 2 22 1 16 10 5 7 11 25 23 6 18 28 3 29 20 9 27 0 21 1 18 15 14 20 27 13 5 16 9 30 25 3 23 2 17 11 6 8 12 26 24 7 19 29 4 0 21 10 28 22 29 2 19 16 15 21 28 14 6 17 10 30 26 4 24 3 18 12 7 9 13 27 25 8 20 0 5 1 22 11 23 12 0 3 20 17 16 22 29 15 7 18 11 30 27 5 25 4 19 13 8 10 14 28 26 9 21 1 6 2 23 24 24 13 1 4 21 18 17 23 0 16 8 19 12 30 28 6 26 5 20 14 9 11 15 29 27 10 22 2 7 3 25 4 25 14 2 5 22 19 18 24 1 17 9 20 13 30 29 7 27 6 21 15 10 12 16 0 28 11 23 3 8 26 9 5 26 15 3 6 23 20 19 25 2 18 10 21 14 30 0 8 28 7 22 16 11 13 17 1 29 12 24 4 27 5 10 6 27 16 4 7 24 21 20 26 3 19 11 22 15 30 1 9 29 8 23 17 12 14 18 2 0 13 25 28 26 6 11 7 28 17 5 8 25 22 21 27 4 20 12 23 16 30 2 10 0 9 24 18 13 15 19 3 1 14 29 15 27 7 12 8 29 18 6 9 26 23 22 28 5 21 13 24 17 30 3 11 1 10 25 19 14 16 20 4 2 0 3 16 28 8 13 9 0 19 7 10 27 24 23 29 6 22 14 25 18 30 4 12 2 11 26 20 15 17 21 5 1 6 4 17 29 9 14 10 1 20 8 11 28 25 24 0 7 23 15 26 19 30 5 13 3 12 27 21 16 18 22 2 23 7 5 18 0 10 15 11 2 21 9 12 29 26 25 1 8 24 16 27 20 30 6 14 4 13 28 22 17 19 3 20 24 8 6 19 1 11 16 12 3 22 10 13 0 27 26 2 9 25 17 28 21 30 7 15 5 14 29 23 18 4 19 21 25 9 7 20 2 12 17 13 4 23 11 14 1 28 27 3 10 26 18 29 22 30 8 16 6 15 0 24 5 25 20 22 26 10 8 21 3 13 18 14 5 24 12 15 2 29 28 4 11 27 19 0 23 30 9 17 7 16 1 6 2 26 21 23 27 11 9 22 4 14 19 15 6 25 13 16 3 0 29 5 12 28 20 1 24 30 10 18 8 17 7 18 3 27 22 24 28 12 10 23 5 15 20 16 7 26 14 17 4 1 0 6 13 29 21 2 25 30 11 19 9 8 10 19 4 28 23 25 29 13 11 24 6 16 21 17 8 27 15 18 5 2 1 7 14 0 22 3 26 30 12 20 9 21 11 20 5 29 24 26 0 14 12 25 7 17 22 18 9 28 16 19 6 3 2 8 15 1 23 4 27 30 13 10 14 22 12 21 6 0 25 27 1 15 13 26 8 18 23 19 10 29 17 20 7 4 3 9 16 2 24 5 28 30 11 30 15 23 13 22 7 1 26 28 2 16 14 27 9 19 24 20 11 0 18 21 8 5 4 10 17 3 25 6 29 12 27 28 29 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 30 -- cycle notation: 0: (0) (1 30 13 28 26 18 12 15 20 19) (2 16 25 11 17 21 22 9 29 7) (3 24 5 23 6 8 27 4 14 10) 1: (1) (2 30 14 29 27 19 13 16 21 20) (3 17 26 12 18 22 23 10 0 8) (4 25 6 24 7 9 28 5 15 11) 2: (2) (3 30 15 0 28 20 14 17 22 21) (4 18 27 13 19 23 24 11 1 9) (5 26 7 25 8 10 29 6 16 12) 3: (3) (4 30 16 1 29 21 15 18 23 22) (5 19 28 14 20 24 25 12 2 10) (6 27 8 26 9 11 0 7 17 13) 4: (4) (5 30 17 2 0 22 16 19 24 23) (6 20 29 15 21 25 26 13 3 11) (7 28 9 27 10 12 1 8 18 14) 5: (5) (6 30 18 3 1 23 17 20 25 24) (7 21 0 16 22 26 27 14 4 12) (8 29 10 28 11 13 2 9 19 15) 6: (6) (7 30 19 4 2 24 18 21 26 25) (8 22 1 17 23 27 28 15 5 13) (9 0 11 29 12 14 3 10 20 16) 7: (7) (8 30 20 5 3 25 19 22 27 26) (9 23 2 18 24 28 29 16 6 14) (10 1 12 0 13 15 4 11 21 17) 8: (8) (9 30 21 6 4 26 20 23 28 27) (10 24 3 19 25 29 0 17 7 15) (11 2 13 1 14 16 5 12 22 18) 9: (9) (10 30 22 7 5 27 21 24 29 28) (11 25 4 20 26 0 1 18 8 16) (12 3 14 2 15 17 6 13 23 19) 10: (10) (11 30 23 8 6 28 22 25 0 29) (12 26 5 21 27 1 2 19 9 17) (13 4 15 3 16 18 7 14 24 20) 11: (11) (12 30 24 9 7 29 23 26 1 0) (13 27 6 22 28 2 3 20 10 18) (14 5 16 4 17 19 8 15 25 21) 12: (12) (13 30 25 10 8 0 24 27 2 1) (14 28 7 23 29 3 4 21 11 19) (15 6 17 5 18 20 9 16 26 22) 13: (13) (14 30 26 11 9 1 25 28 3 2) (15 29 8 24 0 4 5 22 12 20) (16 7 18 6 19 21 10 17 27 23) 14: (14) (15 30 27 12 10 2 26 29 4 3) (16 0 9 25 1 5 6 23 13 21) (17 8 19 7 20 22 11 18 28 24) 15: (15) (16 30 28 13 11 3 27 0 5 4) (17 1 10 26 2 6 7 24 14 22) (18 9 20 8 21 23 12 19 29 25) 16: (16) (17 30 29 14 12 4 28 1 6 5) (18 2 11 27 3 7 8 25 15 23) (19 10 21 9 22 24 13 20 0 26) 17: (17) (18 30 0 15 13 5 29 2 7 6) (19 3 12 28 4 8 9 26 16 24) (20 11 22 10 23 25 14 21 1 27) 18: (18) (19 30 1 16 14 6 0 3 8 7) (20 4 13 29 5 9 10 27 17 25) (21 12 23 11 24 26 15 22 2 28) 19: (19) (20 30 2 17 15 7 1 4 9 8) (21 5 14 0 6 10 11 28 18 26) (22 13 24 12 25 27 16 23 3 29) 20: (20) (21 30 3 18 16 8 2 5 10 9) (22 6 15 1 7 11 12 29 19 27) (23 14 25 13 26 28 17 24 4 0) 21: (21) (22 30 4 19 17 9 3 6 11 10) (23 7 16 2 8 12 13 0 20 28) (24 15 26 14 27 29 18 25 5 1) 22: (22) (23 30 5 20 18 10 4 7 12 11) (24 8 17 3 9 13 14 1 21 29) (25 16 27 15 28 0 19 26 6 2) 23: (23) (24 30 6 21 19 11 5 8 13 12) (25 9 18 4 10 14 15 2 22 0) (26 17 28 16 29 1 20 27 7 3) 24: (24) (25 30 7 22 20 12 6 9 14 13) (26 10 19 5 11 15 16 3 23 1) (27 18 29 17 0 2 21 28 8 4) 25: (25) (26 30 8 23 21 13 7 10 15 14) (27 11 20 6 12 16 17 4 24 2) (28 19 0 18 1 3 22 29 9 5) 26: (26) (27 30 9 24 22 14 8 11 16 15) (28 12 21 7 13 17 18 5 25 3) (29 20 1 19 2 4 23 0 10 6) 27: (27) (28 30 10 25 23 15 9 12 17 16) (29 13 22 8 14 18 19 6 26 4) (0 21 2 20 3 5 24 1 11 7) 28: (28) (29 30 11 26 24 16 10 13 18 17) (0 14 23 9 15 19 20 7 27 5) (1 22 3 21 4 6 25 2 12 8) 29: (29) (30 12 27 25 17 11 14 19 18 0) (1 15 24 10 16 20 21 8 28 6) (2 23 4 22 5 7 26 3 13 9) 30: (30) (0 27 24 21 18 15 12 9 6 3) (1 28 25 22 19 16 13 10 7 4) (2 29 26 23 20 17 14 11 8 5) -- autom facts: AUTOM: (0) (1 11 3 30 17 24 13 21 5 28 22 23 26 9 6 18 29 8 12 7 27 15 2 4 20 16 14 19 25 10) (0 27 5 21 14 1 16 29 6 20 12 15 9 19 17 8 3 7 26 25 13 30 28 10 11 22 18 23 2 4 24) Equational facts: X = (f X X) X = (f (f (f Y X) X) (f X Y)) X = (g X X) X = (f (f X Y) (f Y (f Y X))) X = (f Y (f X (f (f Y X) Y))) X = (f (f (f (f X Y) X) Y) Y) (f X Y) = (f (f X Y) (f X Y)) (f (f X Y) X) = (f X (f Y X)) (f X Y) = (f (f (f Y (f Y X)) Y) X) (f (f X Y) Y) = (f X (f X (f X Y))) (f (f X Y) X) = (f (f (f Y X) X) Y) (f X Y) = (f (f Y (f (f Y X) Y)) X) (f X (f 3 X)) = (f (f X 3) X) (f (f X 7) X) = (f X (f 7 X)) (f X (f 6 X)) = (f (f X 6) X) (f (f X Y) X) = (f Y (f Y (f (f Y X) Y))) (f (f X 20) X) = (f X (f 20 X)) (f (f X 29) X) = (f X (f 29 X)) (f X (f 27 X)) = (f (f X 27) X) (f (f X 10) X) = (f X (f 10 X)) --------------------------------------- Model 31_5: 13 3 21 10 1 27 2 12 24 7 5 19 23 25 20 14 0 8 28 6 30 22 15 26 18 4 11 17 16 29 9 19 15 2 5 23 12 3 0 4 14 26 9 7 21 25 27 22 16 1 10 29 8 30 24 17 28 20 6 13 18 11 14 19 16 3 6 24 13 4 29 5 15 27 10 8 22 26 28 23 17 2 11 1 9 30 25 18 0 21 7 20 12 8 21 20 17 4 7 25 14 5 1 6 16 28 11 9 23 27 0 24 18 3 12 2 10 30 26 19 29 22 15 13 23 16 22 21 18 5 8 26 15 6 2 7 17 0 12 10 24 28 29 25 19 4 13 3 11 30 27 20 1 9 14 2 10 17 23 22 19 6 9 27 16 7 3 8 18 29 13 11 25 0 1 26 20 5 14 4 12 30 28 21 24 15 22 25 11 18 24 23 20 7 10 28 17 8 4 9 19 1 14 12 26 29 2 27 21 6 15 5 13 30 0 3 16 29 4 26 12 19 25 24 21 8 11 0 18 9 5 10 20 2 15 13 27 1 3 28 22 7 16 6 14 30 23 17 30 24 5 27 13 20 26 25 22 9 12 29 19 10 6 11 21 3 16 14 28 2 4 0 23 8 17 7 15 1 18 16 2 25 6 28 14 21 27 26 23 10 13 1 20 11 7 12 22 4 17 15 0 3 5 29 24 9 18 8 30 19 9 30 3 26 7 0 15 22 28 27 24 11 14 2 21 12 8 13 23 5 18 16 29 4 6 1 25 10 19 17 20 20 18 30 4 27 8 29 16 23 0 28 25 12 15 3 22 13 9 14 24 6 19 17 1 5 7 2 26 11 10 21 12 11 19 30 5 28 9 1 17 24 29 0 26 13 16 4 23 14 10 15 25 7 20 18 2 6 8 3 27 21 22 28 22 12 20 30 6 0 10 2 18 25 1 29 27 14 17 5 24 15 11 16 26 8 21 19 3 7 9 4 13 23 5 14 23 13 21 30 7 29 11 3 19 26 2 1 28 15 18 6 25 16 12 17 27 9 22 20 4 8 10 0 24 11 29 15 24 14 22 30 8 1 12 4 20 27 3 2 0 16 19 7 26 17 13 18 28 10 23 21 5 9 6 25 10 7 1 16 25 15 23 30 9 2 13 5 21 28 4 3 29 17 20 8 27 18 14 19 0 11 24 22 6 12 26 7 13 8 2 17 26 16 24 30 10 3 14 6 22 0 5 4 1 18 21 9 28 19 15 20 29 12 25 23 11 27 24 12 14 9 3 18 27 17 25 30 11 4 15 7 23 29 6 5 2 19 22 10 0 20 16 21 1 13 26 8 28 27 9 13 15 10 4 19 28 18 26 30 12 5 16 8 24 1 7 6 3 20 23 11 29 21 17 22 2 14 25 0 15 26 10 14 16 11 5 20 0 19 27 30 13 6 17 9 25 2 8 7 4 21 24 12 1 22 18 23 3 28 29 4 0 27 11 15 17 12 6 21 29 20 28 30 14 7 18 10 26 3 9 8 5 22 25 13 2 23 19 24 16 1 25 17 29 28 12 16 18 13 7 22 1 21 0 30 15 8 19 11 27 4 10 9 6 23 26 14 3 24 20 5 2 21 6 18 1 0 13 17 19 14 8 23 2 22 29 30 16 9 20 12 28 5 11 10 7 24 27 15 4 25 26 3 26 27 7 19 2 29 14 18 20 15 9 24 3 23 1 30 17 10 21 13 0 6 12 11 8 25 28 16 5 22 4 6 23 28 8 20 3 1 15 19 21 16 10 25 4 24 2 30 18 11 22 14 29 7 13 12 9 26 0 17 27 5 18 28 24 0 9 21 4 2 16 20 22 17 11 26 5 25 3 30 19 12 23 15 1 8 14 13 10 27 29 7 6 1 8 0 25 29 10 22 5 3 17 21 23 18 12 27 6 26 4 30 20 13 24 16 2 9 15 14 11 28 19 7 0 20 9 29 26 1 11 23 6 4 18 22 24 19 13 28 7 27 5 30 21 14 25 17 3 10 16 15 12 2 8 17 1 4 22 11 2 28 3 13 25 8 6 20 24 26 21 15 29 9 0 7 30 23 16 27 19 5 12 18 14 10 3 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 0 29 1 2 4 30 -- cycle notation: 0: (0 13 25 4 1 3 10 5 27 17 8 24 18 28 16) (2 21 22 15 14 20 30 9 7 12 23 26 11 19 6) (29) 1: (1 15 27 6 3 5 12 7 0 19 10 26 20 29 18) (2) (4 23 24 17 16 22 30 11 9 14 25 28 13 21 8) 2: (2 16 28 7 4 6 13 8 29 20 11 27 21 1 19) (3) (5 24 25 18 17 23 30 12 10 15 26 0 14 22 9) 3: (3 17 0 8 5 7 14 9 1 21 12 28 22 2 20) (4) (6 25 26 19 18 24 30 13 11 16 27 29 15 23 10) 4: (4 18 29 9 6 8 15 10 2 22 13 0 23 3 21) (5) (7 26 27 20 19 25 30 14 12 17 28 1 16 24 11) 5: (5 19 1 10 7 9 16 11 3 23 14 29 24 4 22) (6) (8 27 28 21 20 26 30 15 13 18 0 2 17 25 12) 6: (6 20 2 11 8 10 17 12 4 24 15 1 25 5 23) (7) (9 28 0 22 21 27 30 16 14 19 29 3 18 26 13) 7: (7 21 3 12 9 11 18 13 5 25 16 2 26 6 24) (8) (10 0 29 23 22 28 30 17 15 20 1 4 19 27 14) 8: (8 22 4 13 10 12 19 14 6 26 17 3 27 7 25) (9) (11 29 1 24 23 0 30 18 16 21 2 5 20 28 15) 9: (9 23 5 14 11 13 20 15 7 27 18 4 28 8 26) (10) (12 1 2 25 24 29 30 19 17 22 3 6 21 0 16) 10: (10 24 6 15 12 14 21 16 8 28 19 5 0 9 27) (11) (13 2 3 26 25 1 30 20 18 23 4 7 22 29 17) 11: (11 25 7 16 13 15 22 17 9 0 20 6 29 10 28) (12) (14 3 4 27 26 2 30 21 19 24 5 8 23 1 18) 12: (12 26 8 17 14 16 23 18 10 29 21 7 1 11 0) (13) (15 4 5 28 27 3 30 22 20 25 6 9 24 2 19) 13: (13 27 9 18 15 17 24 19 11 1 22 8 2 12 29) (14) (16 5 6 0 28 4 30 23 21 26 7 10 25 3 20) 14: (14 28 10 19 16 18 25 20 12 2 23 9 3 13 1) (15) (17 6 7 29 0 5 30 24 22 27 8 11 26 4 21) 15: (15 0 11 20 17 19 26 21 13 3 24 10 4 14 2) (16) (18 7 8 1 29 6 30 25 23 28 9 12 27 5 22) 16: (16 29 12 21 18 20 27 22 14 4 25 11 5 15 3) (17) (19 8 9 2 1 7 30 26 24 0 10 13 28 6 23) 17: (17 1 13 22 19 21 28 23 15 5 26 12 6 16 4) (18) (20 9 10 3 2 8 30 27 25 29 11 14 0 7 24) 18: (18 2 14 23 20 22 0 24 16 6 27 13 7 17 5) (19) (21 10 11 4 3 9 30 28 26 1 12 15 29 8 25) 19: (19 3 15 24 21 23 29 25 17 7 28 14 8 18 6) (20) (22 11 12 5 4 10 30 0 27 2 13 16 1 9 26) 20: (20 4 16 25 22 24 1 26 18 8 0 15 9 19 7) (21) (23 12 13 6 5 11 30 29 28 3 14 17 2 10 27) 21: (21 5 17 26 23 25 2 27 19 9 29 16 10 20 8) (22) (24 13 14 7 6 12 30 1 0 4 15 18 3 11 28) 22: (22 6 18 27 24 26 3 28 20 10 1 17 11 21 9) (23) (25 14 15 8 7 13 30 2 29 5 16 19 4 12 0) 23: (23 7 19 28 25 27 4 0 21 11 2 18 12 22 10) (24) (26 15 16 9 8 14 30 3 1 6 17 20 5 13 29) 24: (24 8 20 0 26 28 5 29 22 12 3 19 13 23 11) (25) (27 16 17 10 9 15 30 4 2 7 18 21 6 14 1) 25: (25 9 21 29 27 0 6 1 23 13 4 20 14 24 12) (26) (28 17 18 11 10 16 30 5 3 8 19 22 7 15 2) 26: (26 10 22 1 28 29 7 2 24 14 5 21 15 25 13) (27) (30 6 4 9 20 23 8 16 3 0 18 19 12 11 17) 27: (27 11 23 2 0 1 8 3 25 15 6 22 16 26 14) (28) (29 19 20 13 12 18 30 7 5 10 21 24 9 17 4) 28: (28 12 24 3 29 2 9 4 26 16 7 23 17 27 15) (30 8 6 11 22 25 10 18 5 1 20 21 14 13 19) (0) 29: (29 14 26 5 2 4 11 6 28 18 9 25 19 0 17) (30 10 8 13 24 27 12 20 7 3 22 23 16 15 21) (1) 30: (30) (0 3 7 11 15 19 23 27 1 5 9 13 17 21 25) (2 6 10 14 18 22 26 29 4 8 12 16 20 24 28) -- autom facts: AUTOM: (0 10 21 2 13 24 5 16 27 8 19 29 11 22 3 14 25 6 17 28 9 20 1 12 23 4 15 26 7 18) (30) Equational facts: X = (f (f (f X X) X) X) X = (f (f (f X Y) Y) Y) X = (f Y (f X (f (f Y X) Y))) X = (f 30 (f X (f X X))) X = (f X (f (f X 30) X)) (f X (f X Y)) = (f Y (f Y X)) (f X X) = (f 23 (f X 10)) (f X X) = (f 26 (f X 13)) 14 = (f (f (f 14 X) X) X) 15 = (f (f (f 15 X) X) X) (f X X) = (f (f (f (f X X) Y) Y) Y) (f X X) = (f 15 (f X 2)) 3 = (f (f (f 3 X) X) X) 6 = (f (f (f 6 X) X) X) (f X X) = (f 29 (f X 17)) 21 = (f (f (f 21 X) X) X) 16 = (f (f (f 16 X) X) X) (f X X) = (f (f 2 X) 3) (f X X) = (f (f 25 X) 26) 5 = (f (f (f 5 X) X) X) --------------------------------------- Model 41_0: 0 3 40 1 18 28 34 26 12 21 17 30 8 19 35 27 39 10 4 13 37 9 31 33 32 36 7 15 5 38 11 22 24 23 6 14 25 20 29 16 2 40 1 3 2 16 21 11 33 36 13 19 6 28 9 27 17 4 15 26 10 32 5 37 38 30 31 18 14 12 34 24 25 20 7 29 39 8 22 23 35 0 1 0 2 40 20 18 15 10 25 30 7 13 17 11 39 6 33 12 5 24 4 34 38 36 19 8 32 31 35 37 9 27 26 16 21 28 23 29 22 14 3 2 40 0 3 32 9 20 36 19 5 26 34 30 24 17 22 37 14 23 8 6 29 15 18 13 39 10 35 33 21 12 38 4 28 11 27 7 16 31 25 1 8 29 9 31 4 40 7 6 0 2 27 14 18 26 11 21 34 35 12 25 30 15 36 37 28 19 13 10 24 1 20 3 38 39 16 17 22 23 32 33 5 19 14 38 25 7 5 40 4 37 39 31 17 16 28 1 35 12 11 22 0 29 27 18 32 34 3 33 21 13 20 36 10 23 26 24 15 30 8 2 9 6 25 18 19 33 5 4 6 40 31 22 21 26 39 38 23 24 35 32 1 2 28 10 9 14 15 0 11 29 20 27 37 8 17 3 36 16 34 30 13 12 7 31 13 37 14 40 6 5 7 16 33 29 32 24 1 3 38 8 36 30 27 35 25 26 28 12 21 22 19 23 10 18 0 11 9 39 20 17 2 15 34 4 18 20 28 29 12 26 23 15 8 40 11 10 4 30 31 7 38 24 0 21 1 19 39 6 17 35 5 34 2 3 13 14 36 37 27 25 32 33 16 22 9 32 7 20 39 30 25 16 1 11 9 40 8 36 33 37 26 6 28 34 31 2 24 35 29 21 5 15 38 17 23 4 19 0 13 18 22 12 14 27 3 10 33 35 29 30 22 24 38 37 9 8 10 40 26 21 20 28 25 23 32 39 14 13 4 17 5 16 12 36 15 2 3 34 18 0 31 1 27 7 6 19 11 16 26 36 15 24 29 18 19 40 10 9 11 33 23 28 3 0 20 6 7 17 35 34 13 4 38 1 32 14 5 39 37 27 12 22 21 2 31 25 30 8 4 37 21 10 0 23 27 20 18 31 3 25 12 40 15 14 32 34 8 36 7 2 28 5 35 11 30 6 22 39 26 9 16 38 17 24 19 1 33 29 13 5 33 23 37 17 0 10 9 34 7 6 36 15 13 40 12 24 4 31 28 39 38 32 2 16 29 35 30 19 25 27 18 22 1 8 26 11 3 21 20 14 29 21 26 36 28 27 8 17 6 34 25 24 13 12 14 40 20 7 37 22 16 1 19 31 11 10 2 5 4 0 33 23 39 30 9 38 3 18 35 32 15 37 25 24 34 39 36 19 16 38 29 32 22 40 14 13 15 7 31 28 6 27 33 11 26 2 1 23 20 18 9 35 17 10 21 3 30 5 0 8 4 12 30 34 27 13 29 32 22 38 15 35 14 39 23 3 10 8 16 40 19 18 25 36 6 12 37 20 28 2 26 4 0 33 5 31 1 9 21 24 7 11 17 23 31 34 7 26 20 30 3 22 27 33 29 21 35 36 25 19 17 40 16 5 12 8 0 39 15 4 9 38 11 6 1 37 10 2 13 14 32 28 24 18 12 11 22 35 8 38 26 21 4 14 15 1 0 20 9 10 17 16 18 40 13 7 2 27 36 30 6 23 32 33 25 39 28 29 37 3 24 34 5 31 19 28 39 15 21 37 13 24 32 29 12 35 27 9 5 33 2 40 18 17 19 34 3 30 25 6 23 38 11 0 8 22 36 7 14 20 10 31 4 26 1 16 15 36 30 28 9 11 33 24 32 4 16 5 35 31 25 0 10 29 39 26 20 40 23 22 7 14 19 37 3 17 2 13 8 6 38 12 1 27 34 18 21 24 27 17 8 33 14 13 30 3 32 38 37 34 6 5 39 26 2 25 29 23 21 40 20 0 18 16 1 36 19 7 35 9 4 12 31 28 11 10 15 22 7 12 5 11 27 2 35 0 24 16 36 3 1 29 30 34 9 39 38 33 21 20 22 40 8 32 31 4 37 13 14 26 25 19 15 6 10 28 18 17 23 10 24 11 27 19 16 31 39 14 15 0 2 32 36 8 9 5 33 35 4 40 22 21 23 1 37 29 3 34 26 38 6 12 17 28 18 13 25 30 7 20 9 38 6 16 14 31 2 35 39 0 34 28 20 37 4 19 3 22 33 15 12 32 17 30 24 40 27 26 11 36 23 5 21 18 10 7 29 13 1 8 25 34 17 35 9 23 39 36 18 28 3 20 33 38 22 16 31 14 1 7 37 10 30 13 4 27 25 40 24 8 32 21 15 29 11 0 2 6 19 12 5 26 22 6 39 12 35 37 1 31 33 23 30 18 3 17 32 29 36 13 11 34 38 28 0 9 25 24 26 40 21 15 10 7 14 8 19 4 16 5 20 2 27 20 5 33 18 36 1 39 11 13 28 22 7 29 8 21 37 31 38 3 32 0 14 10 35 40 26 25 27 9 12 34 16 19 2 30 23 4 15 17 6 24 13 22 25 6 11 19 3 34 35 38 18 4 37 0 24 32 21 27 10 5 33 16 1 39 14 2 36 17 28 40 31 30 15 20 7 8 26 12 9 23 29 35 16 7 19 34 17 12 2 21 26 37 20 6 32 38 23 1 5 24 3 11 8 25 15 18 22 9 39 31 29 40 28 13 36 4 0 33 10 14 27 30 39 23 4 26 2 15 32 25 27 20 12 16 10 34 19 5 11 37 21 14 9 18 33 1 38 7 3 8 29 28 30 40 6 22 13 36 35 17 24 0 31 26 15 16 32 38 34 14 22 23 36 24 21 19 39 6 1 2 25 20 12 18 11 7 8 10 17 0 33 40 30 29 31 3 27 5 37 9 35 4 13 28 21 8 14 38 31 12 37 27 1 24 28 19 5 25 2 18 23 30 15 11 36 0 29 16 9 13 39 7 10 22 17 4 32 40 35 34 20 6 3 26 33 17 9 31 20 15 8 28 13 5 1 23 38 25 7 22 4 27 0 36 30 3 39 14 10 29 12 37 16 6 24 19 2 35 33 40 32 18 26 11 21 34 36 4 12 22 1 10 25 23 30 37 5 15 2 27 18 11 29 21 14 38 26 17 3 7 31 6 20 13 39 16 8 24 33 32 34 40 0 9 19 28 35 38 19 8 23 13 30 9 12 2 6 39 31 7 4 29 36 22 26 27 1 24 37 16 3 20 28 17 18 25 14 5 11 40 34 33 35 15 21 0 10 32 6 32 13 17 10 35 0 14 20 19 4 23 31 2 7 30 28 3 29 9 8 26 27 11 33 34 21 22 16 18 15 12 1 24 25 5 36 40 39 38 37 27 28 10 24 25 33 17 29 26 18 2 35 22 16 34 20 13 6 9 23 15 31 12 19 3 4 8 0 1 7 32 21 30 5 14 11 39 37 40 36 38 14 30 18 4 3 22 21 8 7 17 13 12 11 10 0 16 15 9 2 20 19 6 5 24 23 33 34 28 27 35 1 32 31 25 26 29 37 36 38 40 39 11 10 32 5 21 3 29 28 17 25 1 0 27 18 26 33 30 8 13 35 31 4 24 34 22 9 14 12 7 6 16 20 2 15 23 19 40 38 37 39 36 3 2 1 0 6 7 4 5 10 11 8 9 14 15 12 13 18 19 16 17 22 23 20 21 26 27 24 25 30 31 28 29 34 35 32 33 38 39 36 37 40 -- cycle notation: 0: (0) (1 3) (2 40) (4 18) (5 28) (6 34) (7 26) (8 12) (9 21) (10 17) (11 30) (13 19) (14 35) (15 27) (16 39) (20 37) (22 31) (23 33) (24 32) (25 36) (29 38) 1: (1) (2 3) (4 16) (5 21) (6 11) (7 33) (8 36) (9 13) (10 19) (12 28) (14 27) (15 17) (18 26) (20 32) (22 37) (23 38) (24 30) (25 31) (29 34) (35 39) (40 0) 2: (2) (3 40) (4 20) (5 18) (6 15) (7 10) (8 25) (9 30) (11 13) (12 17) (14 39) (16 33) (19 24) (21 34) (22 38) (23 36) (26 32) (27 31) (28 35) (29 37) (0 1) 3: (3) (4 32) (5 9) (6 20) (7 36) (8 19) (10 26) (11 34) (12 30) (13 24) (14 17) (15 22) (16 37) (18 23) (21 29) (25 39) (27 35) (28 33) (31 38) (40 1) (0 2) 4: (4) (5 40) (6 7) (8 0) (9 2) (10 27) (11 14) (12 18) (13 26) (15 21) (16 34) (17 35) (19 25) (20 30) (22 36) (23 37) (24 28) (29 1) (31 3) (32 38) (33 39) 5: (5) (6 40) (7 4) (8 37) (9 39) (10 31) (11 17) (12 16) (13 28) (14 1) (15 35) (18 22) (19 0) (20 29) (21 27) (23 32) (24 34) (25 3) (26 33) (30 36) (38 2) 6: (6) (7 40) (8 31) (9 22) (10 21) (11 26) (12 39) (13 38) (14 23) (15 24) (16 35) (17 32) (18 1) (19 2) (20 28) (25 0) (27 29) (30 37) (33 3) (34 36) (4 5) 7: (7) (8 16) (9 33) (10 29) (11 32) (12 24) (13 1) (14 3) (15 38) (17 36) (18 30) (19 27) (20 35) (21 25) (22 26) (23 28) (31 0) (34 39) (37 2) (40 4) (5 6) 8: (8) (9 40) (10 11) (12 4) (13 30) (14 31) (15 7) (16 38) (17 24) (18 0) (19 21) (20 1) (22 39) (23 6) (25 35) (26 5) (27 34) (28 2) (29 3) (32 36) (33 37) 9: (9) (10 40) (11 8) (12 36) (13 33) (14 37) (15 26) (16 6) (17 28) (18 34) (19 31) (20 2) (21 24) (22 35) (23 29) (25 5) (27 38) (30 4) (32 0) (39 3) (1 7) 10: (10) (11 40) (12 26) (13 21) (14 20) (15 28) (16 25) (17 23) (18 32) (19 39) (22 4) (24 5) (27 36) (29 2) (30 3) (31 34) (33 0) (35 1) (37 7) (38 6) (8 9) 11: (11) (12 33) (13 23) (14 28) (15 3) (16 0) (17 20) (18 6) (19 7) (21 35) (22 34) (24 4) (25 38) (26 1) (27 32) (29 5) (30 39) (31 37) (36 2) (40 8) (9 10) 12: (12) (13 40) (14 15) (16 32) (17 34) (18 8) (19 36) (20 7) (21 2) (22 28) (23 5) (24 35) (25 11) (26 30) (27 6) (29 39) (31 9) (33 38) (37 1) (0 4) (3 10) 13: (13) (14 40) (15 12) (16 24) (17 4) (18 31) (19 28) (20 39) (21 38) (22 32) (23 2) (25 29) (26 35) (27 30) (33 1) (34 8) (36 11) (37 3) (0 5) (6 10) (7 9) 14: (14) (15 40) (16 20) (17 7) (18 37) (19 22) (21 1) (23 31) (24 11) (25 10) (26 2) (27 5) (28 4) (29 0) (30 33) (32 39) (34 9) (35 38) (36 3) (6 8) (12 13) 15: (15) (16 7) (17 31) (18 28) (19 6) (20 27) (21 33) (22 11) (23 26) (24 2) (25 1) (29 9) (30 35) (32 10) (34 3) (36 5) (37 0) (38 8) (39 4) (40 12) (13 14) 16: (16) (17 40) (18 19) (20 25) (21 36) (22 6) (23 12) (24 37) (26 28) (27 2) (29 4) (30 0) (31 33) (32 5) (34 1) (35 9) (38 7) (39 11) (3 13) (8 15) (10 14) 17: (17) (18 40) (19 16) (20 5) (21 12) (22 8) (23 0) (24 39) (25 15) (26 4) (27 9) (28 38) (29 11) (30 6) (31 1) (32 37) (33 10) (34 2) (35 13) (36 14) (3 7) 18: (18) (19 40) (20 13) (21 7) (22 2) (23 27) (24 36) (25 30) (26 6) (28 32) (29 33) (31 39) (34 37) (35 3) (38 5) (0 12) (1 11) (4 8) (9 14) (10 15) (16 17) 19: (19) (20 34) (21 3) (22 30) (23 25) (24 6) (26 38) (27 11) (28 0) (29 8) (31 36) (32 7) (33 14) (35 10) (37 4) (39 1) (40 16) (2 15) (5 13) (9 12) (17 18) 20: (20) (21 40) (22 23) (24 7) (25 14) (26 19) (27 37) (28 3) (29 17) (30 2) (31 13) (32 8) (33 6) (34 38) (35 12) (36 1) (39 18) (0 15) (4 9) (5 11) (10 16) 21: (21) (22 40) (23 20) (24 0) (25 18) (26 16) (27 1) (28 36) (29 19) (30 7) (31 35) (32 9) (33 4) (34 12) (37 11) (38 10) (39 15) (2 17) (3 8) (5 14) (6 13) 22: (22) (23 40) (24 8) (25 32) (26 31) (27 4) (28 37) (29 13) (30 14) (33 19) (34 15) (35 6) (36 10) (38 18) (39 17) (0 7) (1 12) (2 5) (3 11) (9 16) (20 21) 23: (23) (24 1) (25 37) (26 29) (27 3) (28 34) (30 38) (31 6) (32 12) (33 17) (35 18) (36 13) (39 7) (40 20) (0 10) (2 11) (4 19) (5 16) (8 14) (9 15) (21 22) 24: (24) (25 40) (26 27) (28 11) (29 36) (30 23) (31 5) (32 21) (33 18) (34 10) (35 7) (37 13) (38 1) (39 8) (0 9) (2 6) (3 16) (4 14) (12 20) (15 19) (17 22) 25: (25) (26 40) (27 24) (28 8) (29 32) (30 21) (31 15) (33 11) (34 0) (35 2) (36 6) (37 19) (38 12) (39 5) (1 17) (3 9) (4 23) (7 18) (10 20) (13 22) (14 16) 26: (26) (27 40) (28 21) (29 15) (30 10) (31 7) (32 14) (33 8) (34 19) (35 4) (36 16) (37 5) (38 20) (39 2) (0 22) (1 6) (3 12) (9 23) (11 18) (13 17) (24 25) 27: (27) (28 9) (29 12) (30 34) (31 16) (32 19) (33 2) (35 23) (36 4) (37 15) (38 17) (39 6) (40 24) (0 20) (1 5) (3 18) (7 11) (8 13) (10 22) (14 21) (25 26) 28: (28) (29 40) (30 31) (32 15) (33 20) (34 7) (35 8) (36 26) (37 12) (38 9) (39 23) (0 13) (1 22) (2 25) (3 6) (4 11) (5 19) (10 18) (14 24) (16 21) (17 27) 29: (29) (30 40) (31 28) (32 13) (33 36) (34 4) (35 0) (37 10) (38 14) (39 27) (1 16) (2 7) (3 19) (5 17) (6 12) (8 21) (9 26) (11 20) (15 23) (18 24) (22 25) 30: (30) (31 40) (32 6) (33 22) (34 13) (35 36) (37 17) (38 24) (39 0) (1 23) (2 4) (3 26) (5 15) (7 25) (8 27) (9 20) (10 12) (11 16) (14 19) (18 21) (28 29) 31: (31) (32 3) (33 27) (34 5) (35 37) (36 9) (38 4) (39 13) (40 28) (0 26) (1 15) (2 16) (6 14) (7 22) (8 23) (10 24) (11 21) (12 19) (17 25) (18 20) (29 30) 32: (32) (33 40) (34 35) (36 20) (37 6) (38 3) (39 26) (0 21) (1 8) (2 14) (4 31) (5 12) (7 27) (9 24) (10 28) (11 19) (13 25) (15 18) (16 23) (17 30) (22 29) 33: (33) (34 40) (35 32) (36 18) (37 26) (38 11) (39 21) (0 17) (1 9) (2 31) (3 20) (4 15) (5 8) (6 28) (7 13) (10 23) (12 25) (14 22) (16 27) (19 30) (24 29) 34: (34) (35 40) (36 0) (37 9) (38 19) (39 28) (1 4) (2 12) (3 22) (5 10) (6 25) (7 23) (8 30) (11 15) (13 27) (14 18) (16 29) (17 21) (20 26) (24 31) (32 33) 35: (35) (36 15) (37 21) (38 0) (39 10) (40 32) (1 19) (2 8) (3 23) (4 13) (5 30) (6 9) (7 12) (11 31) (14 29) (16 22) (17 26) (18 27) (20 24) (25 28) (33 34) 36: (36) (37 40) (38 39) (0 6) (1 32) (2 13) (3 17) (4 10) (5 35) (7 14) (8 20) (9 19) (11 23) (12 31) (15 30) (16 28) (18 29) (21 26) (22 27) (24 33) (25 34) 37: (37) (38 40) (39 36) (0 27) (1 28) (2 10) (3 24) (4 25) (5 33) (6 17) (7 29) (8 26) (9 18) (11 35) (12 22) (13 16) (14 34) (15 20) (19 23) (21 31) (30 32) 38: (38) (39 40) (0 14) (1 30) (2 18) (3 4) (5 22) (6 21) (7 8) (9 17) (10 13) (11 12) (15 16) (19 20) (23 24) (25 33) (26 34) (27 28) (29 35) (31 32) (36 37) 39: (39) (40 36) (0 11) (1 10) (2 32) (3 5) (4 21) (6 29) (7 28) (8 17) (9 25) (12 27) (13 18) (14 26) (15 33) (16 30) (19 35) (20 31) (22 24) (23 34) (37 38) 40: (40) (0 3) (1 2) (4 6) (5 7) (8 10) (9 11) (12 14) (13 15) (16 18) (17 19) (20 22) (21 23) (24 26) (25 27) (28 30) (29 31) (32 34) (33 35) (36 38) (37 39) -- autom facts: AUTOM: (0) (1 6 18 26 11) (2 36 8 31 39) (3 34 4 7 30) (5 21 10 15 29) (9 17 27 38 28) (12 22 16 40 25) (13 32 23 20 14) (19 24 33 37 35) (0 23 16 26 19 39 29 18 2 8 13 7 4 11 15 17 32 21 20 10 12 36 38 35 27 33 5 28 34 1 6 24 22 25 30 9 40 14 3 31 37) Equational facts: