// main.c
// Copyright (C) 2023 Mark Bowron

// Verify Table 12 characterizations.

// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.

// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.


#include    <stdio.h>
#include    <stdlib.h>
#include    <inttypes.h>
#include    <stdbool.h>
#include    <string.h>
#include    "set_operators.h"
#include    "set_families.h"
#include    "set_relations.h"
#include    "collapses.h"


int main(int argc, const char * argv[])
{
    FILE       *input;
    uint32_t   *point_closures, set;
    int       **check_phi, phi;
    int       **check_psi, psi;
    int         j, k, spacesize = 8, max_spacesize = 11, space = 0;

// These structs store KZ(A) and KFZ(A) for all A in X.

    KZ         *kz = CreateKZ(max_spacesize);
    KF         *kf = CreateKF(max_spacesize);
    KFZ        *kfz = CreateKFZ(max_spacesize);

// Sets are represented by unsigned 32-bit integers with leading zeros.

    point_closures = (uint32_t *)malloc(max_spacesize * sizeof(uint32_t));
    if (point_closures==0)
    {
        printf("\nCould not allocate space for point_closures.\n");
        exit(0);
    }

    for (j=0; j<max_spacesize; j++) point_closures[j] = 0;

    check_phi = (int **)malloc(31 * sizeof(int *));
    if (check_phi==0)
    {
        printf("\nCould not allocate space for check_phi.\n");
        exit(0);
    }

    for (j=0; j<31; j++)
    {
        check_phi[j] = (int *)malloc(31 * sizeof(int));
        if (check_phi[j]==0)
        {
            printf("\nCould not allocate space for check_phi[%d].\n", j);
            exit(0);
        }
        for (k=0; k<31; k++) check_phi[j][k] = 1;
    }

    check_psi = (int **)malloc(71 * sizeof(int *));
    if (check_psi==0)
    {
        printf("\nCould not allocate space for check_psi.\n");
        exit(0);
    }

    for (j=0; j<71; j++)
    {
        check_psi[j] = (int *)malloc(71 * sizeof(int));
        if (check_psi[j]==0)
        {
            printf("\nCould not allocate space for check_psi[%d].\n", j);
            exit(0);
        }
        for (k=0; k<71; k++) check_psi[j][k] = 1;
    }

// The input file contains all 8-spaces up to homeomorphism.

    input = fopen("8-spaces.txt", "r");
    if (input==0)
    {
        printf("\nCould not open file 8-spaces.txt.\n");
        exit(0);
    }

    while (space < spaces[spacesize])
    {

// This program interprets each line of input as closures of singletons.
// Alternatively, we could interpret each line as smallest open neighborhoods.
// Either interpretation yields all nonhomeomorphic 8-spaces, but any given line
// does not in general produce homeomorphic spaces under the two interpretations.

// Read the current line of input into the point_closures array.

        for (j=0; j<spacesize; j++) fscanf(input, "%" PRIu32, &point_closures[j]);

// Compute and store KFZ(A) in kf then copy KZ(A) to kz.

        ComputeKF(kf,spacesize,point_closures);
        CopyKZfromKF(kz,kf,spacesize);
        CopyKFZfromKF(kfz,kf,spacesize);

        for (set=0; set<(one<<spacesize); set++)
        {
            phi = Phi(set,kz);
            psi = Psi(set,spacesize,kfz);

// Once a set with a given phi- or psi-number fails to satisfy a given characterization,
// we know EVERY such set fails to, so we only verify it once.
// For simplicity however, we repeatedly verify that every set satisfies its own phi- and
// psi-number characterizations.

            if (check_phi[1][phi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_phi[1][phi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_phi[1][phi] = 0;
                if (kf->_bib[set] == kf->_bi[set]) check_phi[1][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[1][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[1][phi] = 0;
            }

            if (check_phi[2][phi])
            {
                if (kf->_bib[set] != kf->_b[set]) check_phi[2][phi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_phi[2][phi] = 0;
                if (kf->_bib[set] == kf->_bi[set]) check_phi[2][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[2][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[2][phi] = 0;
            }

            if (check_phi[3][phi])
            {
                if (kf->_ibi[set] != kf->_i[set]) check_phi[3][phi] = 0;
                if (kf->_bib[set] == kf->_b[set]) check_phi[3][phi] = 0;
                if (kf->_ibi[set] == kf->_ib[set]) check_phi[3][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[3][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[3][phi] = 0;
            }

            if (check_phi[4][phi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_phi[4][phi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_phi[4][phi] = 0;
                if (kf->_bib[set] != kf->_ib[set]) check_phi[4][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[4][phi] = 0;
            }

            if (check_phi[5][phi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_phi[5][phi] = 0;
                if (kf->_bib[set] == kf->_b[set]) check_phi[5][phi] = 0;
                if (kf->_ibi[set] != kf->_bi[set]) check_phi[5][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[5][phi] = 0;
            }

            if (check_phi[6][phi])
            {
                if (kf->_bib[set] != kf->_b[set]) check_phi[6][phi] = 0;
                if (kf->_ibi[set] != kf->_i[set]) check_phi[6][phi] = 0;
                if (kf->_bib[set] == kf->_bi[set]) check_phi[6][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[6][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[6][phi] = 0;
            }

            if (check_phi[7][phi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_phi[7][phi] = 0;
                if (kf->_ibi[set] != kf->_i[set]) check_phi[7][phi] = 0;
                if (kf->_bib[set] != kf->_ib[set]) check_phi[7][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[7][phi] = 0;
            }

            if (check_phi[8][phi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_phi[8][phi] = 0;
                if (kf->_bib[set] != kf->_b[set]) check_phi[8][phi] = 0;
                if (kf->_ibi[set] != kf->_bi[set]) check_phi[8][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[8][phi] = 0;
            }

            if (check_phi[9][phi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_phi[9][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[9][phi] = 0;
                if (kf->_ib[set] != kf->_b[set]) check_phi[9][phi] = 0;
            }

            if (check_phi[10][phi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_phi[10][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[10][phi] = 0;
                if (kf->_bi[set] != kf->_i[set]) check_phi[10][phi] = 0;
            }

            if (check_phi[11][phi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_phi[11][phi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_phi[11][phi] = 0;
                if (kf->_bib[set] == kf->_bi[set]) check_phi[11][phi] = 0;
                if (kf->_bib[set] != kf->_ib[set]) check_phi[11][phi] = 0;
                if (kf->_ibi[set] != kf->_bi[set]) check_phi[11][phi] = 0;
            }

            if (check_phi[12][phi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_phi[12][phi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_phi[12][phi] = 0;
                if (kf->_bib[set] != kf->_bi[set]) check_phi[12][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[12][phi] = 0;
            }

            if (check_phi[13][phi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_phi[13][phi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_phi[13][phi] = 0;
                if (kf->_bi[set] != kf->_ib[set]) check_phi[13][phi] = 0;
            }

            if (check_phi[14][phi])
            {
                if (kf->_ibi[set] != kf->_i[set]) check_phi[14][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[14][phi] = 0;
                if (kf->_ib[set] != kf->_b[set]) check_phi[14][phi] = 0;
            }

            if (check_phi[15][phi])
            {
                if (kf->_bib[set] != kf->_b[set]) check_phi[15][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[15][phi] = 0;
                if (kf->_bi[set] != kf->_i[set]) check_phi[15][phi] = 0;
            }

            if (check_phi[16][phi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_phi[16][phi] = 0;
                if (kf->_ibi[set] != kf->_bi[set]) check_phi[16][phi] = 0;
                if (kf->_bib[set] == kf->_bi[set]) check_phi[16][phi] = 0;
                if (kf->_ib[set] != kf->_b[set]) check_phi[16][phi] = 0;
            }

            if (check_phi[17][phi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_phi[17][phi] = 0;
                if (kf->_bib[set] != kf->_ib[set]) check_phi[17][phi] = 0;
                if (kf->_ibi[set] == kf->_ib[set]) check_phi[17][phi] = 0;
                if (kf->_bi[set] != kf->_i[set]) check_phi[17][phi] = 0;
            }

            if (check_phi[18][phi])
            {
                if (set == kf->_i[set]) check_phi[18][phi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_phi[18][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[18][phi] = 0;
                if (kf->_bi[set] != kf->_b[set]) check_phi[18][phi] = 0;
            }

            if (check_phi[19][phi])
            {
                if (set == kf->_b[set]) check_phi[19][phi] = 0;
                if (kf->_bib[set] == kf->_b[set]) check_phi[19][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[19][phi] = 0;
                if (kf->_ib[set] != kf->_i[set]) check_phi[19][phi] = 0;
            }

            if (check_phi[20][phi])
            {
                if (set != kf->_i[set]) check_phi[20][phi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_phi[20][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[20][phi] = 0;
            }

            if (check_phi[21][phi])
            {
                if (set != kf->_b[set]) check_phi[21][phi] = 0;
                if (kf->_bib[set] == kf->_b[set]) check_phi[21][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[21][phi] = 0;
            }

            if (check_phi[22][phi])
            {
                if (set == kf->_i[set]) check_phi[22][phi] = 0;
                if (kf->_ibi[set] != kf->_b[set]) check_phi[22][phi] = 0;
            }

            if (check_phi[23][phi])
            {
                if (set == kf->_b[set]) check_phi[23][phi] = 0;
                if (kf->_bib[set] != kf->_i[set]) check_phi[23][phi] = 0;
            }

            if (check_phi[24][phi])
            {
                if (set == kf->_b[set]) check_phi[24][phi] = 0;
                if (set == kf->_i[set]) check_phi[24][phi] = 0;
                if (kf->_f[set] != kf->_fbi[set]) check_phi[24][phi] = 0;
            }

            if (check_phi[25][phi])
            {
                if (kf->_bib[set] == kf->_bi[set]) check_phi[25][phi] = 0;
                if (kf->_f[set] != kf->_if[set]) check_phi[25][phi] = 0;
            }

            if (check_phi[26][phi])
            {
                if (set != kf->_bi[set]) check_phi[26][phi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_phi[26][phi] = 0;
            }

            if (check_phi[27][phi])
            {
                if (set != kf->_ib[set]) check_phi[27][phi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_phi[27][phi] = 0;
            }

            if (check_phi[28][phi])
            {
                if (set != kf->_i[set]) check_phi[28][phi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_phi[28][phi] = 0;
                if (kf->_bib[set] != kf->_ib[set]) check_phi[28][phi] = 0;
            }

            if (check_phi[29][phi])
            {
                if (set != kf->_b[set]) check_phi[29][phi] = 0;
                if (kf->_bib[set] == kf->_b[set]) check_phi[29][phi] = 0;
                if (kf->_ibi[set] != kf->_bi[set]) check_phi[29][phi] = 0;
            }

            if (check_phi[30][phi])
            {
                if (kf->_b[set] != kf->_i[set]) check_phi[30][phi] = 0;
            }

            if (check_psi[1][psi])
            {
                if (kf->_bib[set] == kf->_b[set])  check_psi[1][psi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_psi[1][psi] = 0;
                if (kf->_fib[set] == kf->_fbi[set]) check_psi[1][psi] = 0;
                if (kf->_fib[set] == kf->_fif[set]) check_psi[1][psi] = 0;
                if (kf->_fbi[set] == kf->_fif[set]) check_psi[1][psi] = 0;
            }

            if (check_psi[2][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[2][psi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_psi[2][psi] = 0;
                if (kf->_fib[set] != kf->_fbi[set]) check_psi[2][psi] = 0;
                if (kf->_fib[set] == kf->_fif[set]) check_psi[2][psi] = 0;
                if (kf->_bif[set] == kf->_if[set]) check_psi[2][psi] = 0;
            }

            if (check_psi[3][psi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_psi[3][psi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_psi[3][psi] = 0;
                if (kf->_bib[set] == kf->_b[set]) check_psi[3][psi] = 0;
                if (kf->_fib[set] == kf->_fbi[set]) check_psi[3][psi] = 0;
                if (kf->_fib[set] != kf->_fif[set]) check_psi[3][psi] = 0;
            }

            if (check_psi[4][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[4][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[4][psi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_psi[4][psi] = 0;
                if (kf->_fib[set] == kf->_fbi[set]) check_psi[4][psi] = 0;
                if (kf->_fbi[set] != kf->_fif[set]) check_psi[4][psi] = 0;
            }

            if (check_psi[5][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[5][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[5][psi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_psi[5][psi] = 0;
                if (kf->_fib[set] != kf->_fbi[set]) check_psi[5][psi] = 0;
                if (kf->_fbi[set] != kf->_fif[set]) check_psi[5][psi] = 0;
            }

            if (check_psi[6][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[6][psi] = 0;
                if (kf->_bib[set] == kf->_bi[set]) check_psi[6][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[6][psi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_psi[6][psi] = 0;
                if (kf->_bif[set] != kf->_if[set]) check_psi[6][psi] = 0;
            }

            if (check_psi[7][psi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_psi[7][psi] = 0;
                if (kf->_bib[set] != kf->_b[set]) check_psi[7][psi] = 0;
                if (kf->_fib[set] == kf->_fif[set]) check_psi[7][psi] = 0;
                if (kf->_ff[set] == kf->_fi[set]) check_psi[7][psi] = 0;
            }

            if (check_psi[8][psi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_psi[8][psi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_psi[8][psi] = 0;
                if (kf->_fib[set] == kf->_fbi[set]) check_psi[8][psi] = 0;
                if (kf->_fb[set] != kf->_fif[set]) check_psi[8][psi] = 0;
            }

            if (check_psi[9][psi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_psi[9][psi] = 0;
                if (kf->_ff[set] != kf->_fi[set]) check_psi[9][psi] = 0;
                if (kf->_fib[set] == kf->_fbi[set]) check_psi[9][psi] = 0;
                if (kf->_fbi[set] == kf->_fif[set]) check_psi[9][psi] = 0;
            }

            if (check_psi[10][psi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_psi[10][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[10][psi] = 0;
                if (kf->_bib[set] != kf->_b[set]) check_psi[10][psi] = 0;
                if (kf->_fbi[set] != kf->_fif[set]) check_psi[10][psi] = 0;
                if (kf->_fib[set] == kf->_fif[set]) check_psi[10][psi] = 0;
            }

            if (check_psi[11][psi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_psi[11][psi] = 0;
                if (kf->_fib[set] == kf->_fif[set]) check_psi[11][psi] = 0;
                if (kf->_fb[set] != kf->_fbi[set]) check_psi[11][psi] = 0;
                if (kf->_bif[set] == kf->_if[set]) check_psi[11][psi] = 0;
            }

            if (check_psi[12][psi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_psi[12][psi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_psi[12][psi] = 0;
                if (kf->_fib[set] != kf->_fif[set]) check_psi[12][psi] = 0;
                if (kf->_ff[set] != kf->_fi[set]) check_psi[12][psi] = 0;
            }

            if (check_psi[13][psi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_psi[13][psi] = 0;
                if (kf->_ibi[set] == kf->_ib[set]) check_psi[13][psi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_psi[13][psi] = 0;
                if (kf->_bib[set] != kf->_b[set]) check_psi[13][psi] = 0;
                if (kf->_bif[set] != kf->_if[set]) check_psi[13][psi] = 0;
            }

            if (check_psi[14][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[14][psi] = 0;
                if (kf->_ibi[set] != kf->_i[set]) check_psi[14][psi] = 0;
                if (kf->_fbi[set] == kf->_fif[set]) check_psi[14][psi] = 0;
                if (kf->_ff[set] == kf->_fb[set]) check_psi[14][psi] = 0;
            }

            if (check_psi[15][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[15][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[15][psi] = 0;
                if (kf->_fib[set] == kf->_fbi[set]) check_psi[15][psi] = 0;
                if (kf->_fi[set] != kf->_fif[set]) check_psi[15][psi] = 0;
            }

            if (check_psi[16][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[16][psi] = 0;
                if (kf->_ff[set] != kf->_fb[set]) check_psi[16][psi] = 0;
                if (kf->_fib[set] == kf->_fbi[set]) check_psi[16][psi] = 0;
                if (kf->_fib[set] == kf->_fif[set]) check_psi[16][psi] = 0;
            }

            if (check_psi[17][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[17][psi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_psi[17][psi] = 0;
                if (kf->_ibi[set] != kf->_i[set]) check_psi[17][psi] = 0;
                if (kf->_fib[set] != kf->_fif[set]) check_psi[17][psi] = 0;
                if (kf->_fbi[set] == kf->_fif[set]) check_psi[17][psi] = 0;
            }

            if (check_psi[18][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[18][psi] = 0;
                if (kf->_fbi[set] == kf->_fif[set]) check_psi[18][psi] = 0;
                if (kf->_fi[set] != kf->_fib[set]) check_psi[18][psi] = 0;
                if (kf->_bif[set] == kf->_if[set]) check_psi[18][psi] = 0;
            }

            if (check_psi[19][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[19][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[19][psi] = 0;
                if (kf->_fbi[set] != kf->_fif[set]) check_psi[19][psi] = 0;
                if (kf->_ff[set] != kf->_fb[set]) check_psi[19][psi] = 0;
            }

            if (check_psi[20][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[20][psi] = 0;
                if (kf->_bib[set] == kf->_bi[set]) check_psi[20][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[20][psi] = 0;
                if (kf->_ibi[set] != kf->_i[set]) check_psi[20][psi] = 0;
                if (kf->_bif[set] != kf->_if[set]) check_psi[20][psi] = 0;
            }

            // Psi-numbers 21-22 are identical to phi-numbers 4-5.

            if (check_psi[23][psi])
            {
                if (kf->_bib[set] != kf->_b[set]) check_psi[23][psi] = 0;
                if (kf->_ibi[set] != kf->_i[set]) check_psi[23][psi] = 0;
                if (kf->_ff[set] == kf->_fb[set]) check_psi[23][psi] = 0;
                if (kf->_ff[set] == kf->_fi[set]) check_psi[23][psi] = 0;
                if (kf->_f[set] == kf->_bif[set]) check_psi[23][psi] = 0;
            }

            if (check_psi[24][psi])
            {
                if (kf->_fb[set] == kf->_fi[set]) check_psi[24][psi] = 0;
                if (kf->_ff[set] != kf->_fib[set]) check_psi[24][psi] = 0;
                if (kf->_f[set] == kf->_bif[set]) check_psi[24][psi] = 0;
            }

            if (check_psi[25][psi])
            {
                if (kf->_fb[set] == kf->_fi[set]) check_psi[25][psi] = 0;
                if (kf->_ff[set] != kf->_fbi[set]) check_psi[25][psi] = 0;
                if (kf->_f[set] == kf->_bif[set]) check_psi[25][psi] = 0;
            }

            if (check_psi[26][psi])
            {
                if (kf->_fb[set] != kf->_fi[set]) check_psi[26][psi] = 0;
                if (kf->_bif[set] == kf->_if[set]) check_psi[26][psi] = 0;
                if (kf->_f[set] == kf->_bif[set]) check_psi[26][psi] = 0;
            }

            if (check_psi[27][psi])
            {
                if (kf->_ff[set] == kf->_fb[set]) check_psi[27][psi] = 0;
                if (kf->_ff[set] == kf->_fi[set]) check_psi[27][psi] = 0;
                if (kf->_f[set] != kf->_bif[set]) check_psi[27][psi] = 0;
            }

            if (check_psi[28][psi])
            {
                if (kf->_ibi[set] != kf->_i[set]) check_psi[28][psi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_psi[28][psi] = 0;
                if (kf->_fib[set] == kf->_fbi[set]) check_psi[28][psi] = 0;
                if (kf->_fb[set] != kf->_fif[set]) check_psi[28][psi] = 0;
            }

            if (check_psi[29][psi])
            {
                if (kf->_bib[set] != kf->_b[set]) check_psi[29][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[29][psi] = 0;
                if (kf->_fib[set] == kf->_fbi[set]) check_psi[29][psi] = 0;
                if (kf->_fi[set] != kf->_fif[set]) check_psi[29][psi] = 0;
            }

            if (check_psi[30][psi])
            {
                if (kf->_fib[set] != kf->_fbi[set]) check_psi[30][psi] = 0;
                if (kf->_bif[set] == kf->_if[set]) check_psi[30][psi] = 0;
                if (kf->_f[set] != kf->_bif[set]) check_psi[30][psi] = 0;
            }

            if (check_psi[31][psi])
            {
                if (kf->_bi[set] == kf->_b[set]) check_psi[31][psi] = 0;
                if (kf->_ib[set] == kf->_b[set]) check_psi[31][psi] = 0;
                if (kf->_fb[set] != kf->_fi[set]) check_psi[31][psi] = 0;
                if (kf->_bif[set] != kf->_if[set]) check_psi[31][psi] = 0;
            }

            // Psi-numbers 32-33 are identical to phi-numbers 7-8.

            if (check_psi[34][psi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_psi[34][psi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_psi[34][psi] = 0;
                if (kf->_ib[set] != kf->_b[set]) check_psi[34][psi] = 0;
                if (kf->_b[set] == kf->_one[set]) check_psi[34][psi] = 0;
            }

            if (check_psi[35][psi])
            {
                if (kf->_ibi[set] == kf->_i[set]) check_psi[35][psi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_psi[35][psi] = 0;
                if (kf->_b[set] != kf->_one[set]) check_psi[35][psi] = 0;
            }

            if (check_psi[36][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[36][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[36][psi] = 0;
                if (kf->_bi[set] != kf->_i[set]) check_psi[36][psi] = 0;
                if (kf->_i[set] == kf->_zero[set]) check_psi[36][psi] = 0;
            }

            if (check_psi[37][psi])
            {
                if (kf->_bib[set] == kf->_b[set]) check_psi[37][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[37][psi] = 0;
                if (kf->_i[set] != kf->_zero[set]) check_psi[37][psi] = 0;
            }

            // Psi-numbers 38-40 are identical to phi-numbers 11-13.

            if (check_psi[41][psi])
            {
                if (kf->_ibi[set] != kf->_i[set]) check_psi[41][psi] = 0;
                if (kf->_ibi[set] == kf->_bi[set]) check_psi[41][psi] = 0;
                if (kf->_ib[set] != kf->_b[set]) check_psi[41][psi] = 0;
                if (kf->_b[set] == kf->_one[set]) check_psi[41][psi] = 0;
            }

            if (check_psi[42][psi])
            {
                if (kf->_bi[set] == kf->_i[set]) check_psi[42][psi] = 0;
                if (kf->_ibi[set] != kf->_af[set]) check_psi[42][psi] = 0;
            }

            if (check_psi[43][psi])
            {
                if (kf->_bib[set] != kf->_b[set]) check_psi[43][psi] = 0;
                if (kf->_bib[set] == kf->_ib[set]) check_psi[43][psi] = 0;
                if (kf->_bi[set] != kf->_i[set]) check_psi[43][psi] = 0;
                if (kf->_i[set] == kf->_zero[set]) check_psi[43][psi] = 0;
            }

            if (check_psi[44][psi])
            {
                if (kf->_ib[set] == kf->_b[set]) check_psi[44][psi] = 0;
                if (kf->_bib[set] != kf->_f[set]) check_psi[44][psi] = 0;
            }

            if (check_psi[45][psi])
            {
                if (kf->_ibi[set] != kf->_bi[set]) check_psi[45][psi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_psi[45][psi] = 0;
                if (kf->_ibi[set] == kf->_ib[set]) check_psi[45][psi] = 0;
                if (kf->_ib[set] != kf->_b[set]) check_psi[45][psi] = 0;
                if (kf->_b[set] == kf->_one[set]) check_psi[45][psi] = 0;
            }

            if (check_psi[46][psi])
            {
                if (kf->_bi[set] == kf->_ib[set]) check_psi[46][psi] = 0;
                if (kf->_ibi[set] == kf->_i[set]) check_psi[46][psi] = 0;
                if (kf->_ibi[set] != kf->_aif[set]) check_psi[46][psi] = 0;
            }

            if (check_psi[47][psi])
            {
                if (kf->_bib[set] != kf->_ib[set]) check_psi[47][psi] = 0;
                if (kf->_bib[set] == kf->_b[set]) check_psi[47][psi] = 0;
                if (kf->_bib[set] == kf->_bi[set]) check_psi[47][psi] = 0;
                if (kf->_bi[set] != kf->_i[set]) check_psi[47][psi] = 0;
                if (kf->_i[set] == kf->_zero[set]) check_psi[47][psi] = 0;
            }

            if (check_psi[48][psi])
            {
                if (kf->_bi[set] == kf->_ib[set]) check_psi[48][psi] = 0;
                if (kf->_bib[set] == kf->_b[set]) check_psi[48][psi] = 0;
                if (kf->_bib[set] != kf->_if[set]) check_psi[48][psi] = 0;
            }

            // Psi-numbers 49-52 are identical to phi-numbers 18-21.

            if (check_psi[53][psi])
            {
                if (set == kf->_i[set]) check_psi[53][psi] = 0;
                if (kf->_ibi[set] != kf->_b[set]) check_psi[53][psi] = 0;
                if (kf->_b[set] == kf->_one[set]) check_psi[53][psi] = 0;
            }

            if (check_psi[54][psi])
            {
                if (set == kf->_i[set]) check_psi[54][psi] = 0;
                if (kf->_bi[set] != kf->_one[set]) check_psi[54][psi] = 0;
            }

            if (check_psi[55][psi])
            {
                if (set == kf->_b[set]) check_psi[55][psi] = 0;
                if (kf->_bib[set] != kf->_i[set]) check_psi[55][psi] = 0;
                if (kf->_i[set] == kf->_zero[set]) check_psi[55][psi] = 0;
            }

            if (check_psi[56][psi])
            {
                if (set == kf->_b[set]) check_psi[56][psi] = 0;
                if (kf->_ib[set] != kf->_zero[set]) check_psi[56][psi] = 0;
            }

            // Psi-number 57 is identical to phi-number 24.

            if (check_psi[58][psi])
            {
                if (kf->_bi[set] == kf->_ib[set]) check_psi[58][psi] = 0;
                if (kf->_b[set] == kf->_one[set]) check_psi[58][psi] = 0;
                if (kf->_i[set] == kf->_zero[set]) check_psi[58][psi] = 0;
                if (kf->_f[set] != kf->_if[set]) check_psi[58][psi] = 0;
            }

            if (check_psi[59][psi])
            {
                if (set == kf->_i[set]) check_psi[59][psi] = 0;
                if (kf->_bi[set] != kf->_af[set]) check_psi[59][psi] = 0;
                if (kf->_i[set] == kf->_zero[set]) check_psi[59][psi] = 0;
            }

            if (check_psi[60][psi])
            {
                if (set == kf->_b[set]) check_psi[60][psi] = 0;
                if (kf->_ib[set] != kf->_f[set]) check_psi[60][psi] = 0;
                if (kf->_b[set] == kf->_one[set]) check_psi[60][psi] = 0;
            }

            if (check_psi[61][psi])
            {
                if (kf->_f[set] != kf->_one[set]) check_psi[61][psi] = 0;
            }

            // Psi-numbers 62-63 are identical to phi-numbers 26-27.

            if (check_psi[64][psi])
            {
                if (set != kf->_i[set]) check_psi[64][psi] = 0;
                if (set == kf->_b[set]) check_psi[64][psi] = 0;
                if (kf->_ibi[set] != kf->_bi[set]) check_psi[64][psi] = 0;
                if (kf->_b[set] == kf->_one[set]) check_psi[64][psi] = 0;
            }

            if (check_psi[65][psi])
            {
                if (set != kf->_af[set]) check_psi[65][psi] = 0;
                if (set == kf->_one[set]) check_psi[65][psi] = 0;
            }

            if (check_psi[66][psi])
            {
                if (set != kf->_b[set]) check_psi[66][psi] = 0;
                if (set == kf->_i[set]) check_psi[66][psi] = 0;
                if (kf->_bib[set] != kf->_ib[set]) check_psi[66][psi] = 0;
                if (kf->_i[set] == kf->_zero[set]) check_psi[66][psi] = 0;
            }

            if (check_psi[67][psi])
            {
                if (set != kf->_f[set]) check_psi[67][psi] = 0;
                if (set == kf->_zero[set]) check_psi[67][psi] = 0;
            }

            if (check_psi[68][psi])
            {
                if (set == kf->_zero[set]) check_psi[68][psi] = 0;
                if (set == kf->_one[set]) check_psi[68][psi] = 0;
                if (kf->_b[set] != kf->_i[set]) check_psi[68][psi] = 0;
            }

            if (check_psi[69][psi])
            {
                if (set != kf->_one[set]) check_psi[69][psi] = 0;
            }

            if (check_psi[70][psi])
            {
                if (set != kf->_zero[set]) check_psi[70][psi] = 0;
            }
        }
        space++;
    }

// Table 12 is valid if check_phi[j][k] = 0 and check_psi[j][k] = 0 each hold iff j != k.

    for (j=1; j<31; j++)
        for (k=1; k<31; k++)
        {
            if ((j != k && check_phi[j][k]) || (j == k && !check_phi[j][k]))
            {
                printf("\nError: execution aborted.\n\n");
                exit(0);
            }
        }

    for (j=1; j<71; j++)
    {

// Skip psi-numbers that are equivalent to phi-numbers.

        if (j > 20 && j < 23) continue;
        if (j > 31 && j < 34) continue;
        if (j > 37 && j < 41) continue;
        if (j > 48 && j < 53) continue;
        if (j == 57) continue;
        if (j > 61 && j < 64) continue;

// No such skipping is needed for the second coordinate.

        for (k=1; k<71; k++)
        {
            if ((j != k && check_psi[j][k]) || (j == k && !check_psi[j][k]))
            {
                printf("\nError: execution aborted.\n\n");
                exit(0);
            }
        }
    }

    printf("\nTable 12 is valid.");

    fclose(input);
    for (j=0; j<31; j++) free(check_phi[j]);
    free(check_phi);
    for (j=0; j<71; j++) free(check_psi[j]);
    free(check_psi);
    free(point_closures);
    FreeKZ(kz);
    FreeKF(kf);
    FreeKFZ(kfz);
    printf("\n\n");
    return EXIT_SUCCESS;
}