{
    "data_id": "1475",
    "name": "first-order-theorem-proving",
    "exact_name": "first-order-theorem-proving",
    "version": 1,
    "version_label": null,
    "description": "**Author**: James P Bridge, Sean B Holden and Lawrence C Paulson \r\n  \r\n**Source**: [UCI](https:\/\/archive.ics.uci.edu\/ml\/datasets\/First-order+theorem+proving)  \r\n\r\n**Please cite**: James P Bridge, Sean B Holden and Lawrence C Paulson . Machine learning for first-order theorem proving: learning to select a good heuristic. Journal of Automated Reasoning, Springer 2012\/13. \r\n\r\nSource:\r\n\r\nJames P Bridge, Sean B Holden and Lawrence C Paulson \r\n\r\nUniversity of Cambridge \r\nComputer Laboratory \r\nWilliam Gates Building \r\n15 JJ Thomson Avenue \r\nCambridge CB3 0FD \r\nUK \r\n\r\n+44 (0)1223 763500 \r\nforename.surname '@' cl.cam.ac.uk\r\n\r\n\r\nData Set Information:\r\n\r\nSee the file dataset file.\r\n\r\n\r\nAttribute Information:\r\n\r\nThe attributes are a mixture of static and dynamic features derived from theorems to be proved. See the paper for full details.\r\n",
    "format": "ARFF",
    "uploader": "Rafael Gomes Mantovani",
    "uploader_id": 64,
    "visibility": "public",
    "creator": null,
    "contributor": null,
    "date": "2015-05-22 17:30:40",
    "update_comment": null,
    "last_update": "2015-11-09 20:36:55",
    "licence": "Public",
    "status": "active",
    "error_message": null,
    "url": "https:\/\/www.openml.org\/data\/download\/1587932\/phpPbCMyg",
    "default_target_attribute": "Class",
    "row_id_attribute": null,
    "ignore_attribute": null,
    "runs": 26642,
    "suggest": {
        "input": [
            "first-order-theorem-proving",
            "Source: James P Bridge, Sean B Holden and Lawrence C Paulson University of Cambridge Computer Laboratory William Gates Building 15 JJ Thomson Avenue Cambridge CB3 0FD UK +44 (0)1223 763500 forename.surname '@' cl.cam.ac.uk Data Set Information: See the file dataset file. Attribute Information: The attributes are a mixture of static and dynamic features derived from theorems to be proved. See the paper for full details. "
        ],
        "weight": 5
    },
    "qualities": {
        "NumberOfInstances": 6118,
        "NumberOfFeatures": 52,
        "NumberOfClasses": 6,
        "NumberOfMissingValues": 0,
        "NumberOfInstancesWithMissingValues": 0,
        "NumberOfNumericFeatures": 51,
        "NumberOfSymbolicFeatures": 1,
        "kNN1NKappa": 0.3867635866819356,
        "MajorityClassSize": 2554,
        "MinAttributeEntropy": null,
        "Quartile2KurtosisOfNumericAtts": 15.286501444565163,
        "REPTreeDepth2Kappa": 0.3022006426588284,
        "ClassEntropy": 2.3000070580673455,
        "MaxAttributeEntropy": null,
        "MinKurtosisOfNumericAtts": -0.971971602375862,
        "Quartile2MeansOfNumericAtts": -0.002469232265446736,
        "REPTreeDepth3AUC": 0.7474597786162569,
        "DecisionStumpAUC": 0.5958041430205936,
        "MaxKurtosisOfNumericAtts": 2944.6525317078385,
        "MinMeansOfNumericAtts": -0.04091056701536289,
        "Quartile2MutualInformation": null,
        "REPTreeDepth3ErrRate": 0.5052304674730304,
        "DecisionStumpErrRate": 0.582543314808761,
        "MaxMeansOfNumericAtts": 0.052954623733246275,
        "MinMutualInformation": null,
        "Quartile2SkewnessOfNumericAtts": 3.1426279908840025,
        "REPTreeDepth3Kappa": 0.3022006426588284,
        "DecisionStumpKappa": 0,
        "MaxMutualInformation": null,
        "MinNominalAttDistinctValues": 6,
        "PercentageOfBinaryFeatures": 0,
        "Quartile2StdDevOfNumericAtts": 0.99719270235299,
        "RandomTreeDepth1AUC": 0.6943273232081051,
        "Dimensionality": 0.008499509643674403,
        "MaxNominalAttDistinctValues": 6,
        "MinSkewnessOfNumericAtts": -1.875764427110436,
        "PercentageOfInstancesWithMissingValues": 0,
        "Quartile3AttributeEntropy": null,
        "RandomTreeDepth1ErrRate": 0.4870872834259562,
        "EquivalentNumberOfAtts": null,
        "MaxSkewnessOfNumericAtts": 53.784844915558836,
        "MinStdDevOfNumericAtts": 0.8394622129143448,
        "PercentageOfMissingValues": 0,
        "Quartile3KurtosisOfNumericAtts": 137.49118065052153,
        "AutoCorrelation": 0.3678273663560569,
        "RandomTreeDepth1Kappa": 0.3568830760926545,
        "J48.00001.AUC": 0.7129106639983,
        "J48.00001.ErrRate": 0.465675057208238,
        "MaxStdDevOfNumericAtts": 1.5063662920278478,
        "MinorityClassPercentage": 7.943772474664923,
        "PercentageOfNumericFeatures": 98.07692307692307,
        "Quartile3MeansOfNumericAtts": 0.002845900948022519,
        "CfsSubsetEval_DecisionStumpAUC": 0.7090827191037619,
        "RandomTreeDepth2AUC": 0.6943273232081051,
        "J48.00001.Kappa": 0.375395542857667,
        "MeanAttributeEntropy": null,
        "MinorityClassSize": 486,
        "PercentageOfSymbolicFeatures": 1.9230769230769231,
        "Quartile3MutualInformation": null,
        "CfsSubsetEval_DecisionStumpErrRate": 0.4851258581235698,
        "RandomTreeDepth2ErrRate": 0.4870872834259562,
        "J48.0001.AUC": 0.7129106639983,
        "MeanKurtosisOfNumericAtts": 228.1908672595734,
        "NaiveBayesAUC": 0.620496665896741,
        "Quartile1AttributeEntropy": null,
        "Quartile3SkewnessOfNumericAtts": 10.454373740045988,
        "CfsSubsetEval_DecisionStumpKappa": 0.346242749551416,
        "RandomTreeDepth2Kappa": 0.3568830760926545,
        "J48.0001.ErrRate": 0.465675057208238,
        "MeanMeansOfNumericAtts": -0.0005510331198841205,
        "NaiveBayesErrRate": 0.8345864661654135,
        "Quartile1KurtosisOfNumericAtts": 1.3326773975344213,
        "Quartile3StdDevOfNumericAtts": 1.0036680416341404,
        "CfsSubsetEval_NaiveBayesAUC": 0.7090827191037619,
        "RandomTreeDepth3AUC": 0.6943273232081051,
        "RandomTreeDepth3ErrRate": 0.4870872834259562,
        "J48.0001.Kappa": 0.375395542857667,
        "MeanMutualInformation": null,
        "NaiveBayesKappa": 0.05473977746349635,
        "Quartile1MeansOfNumericAtts": -0.0081597994442654,
        "REPTreeDepth1AUC": 0.7474597786162569,
        "CfsSubsetEval_NaiveBayesErrRate": 0.4851258581235698,
        "RandomTreeDepth3Kappa": 0.3568830760926545,
        "J48.001.AUC": 0.7129106639983,
        "MeanNoiseToSignalRatio": null,
        "NumberOfBinaryFeatures": 0,
        "Quartile1MutualInformation": null,
        "REPTreeDepth1ErrRate": 0.5052304674730304,
        "CfsSubsetEval_NaiveBayesKappa": 0.346242749551416,
        "StdvNominalAttDistinctValues": 0,
        "J48.001.ErrRate": 0.465675057208238,
        "MeanNominalAttDistinctValues": 6,
        "Quartile1SkewnessOfNumericAtts": 1.3330441633458074,
        "REPTreeDepth1Kappa": 0.3022006426588284,
        "CfsSubsetEval_kNN1NAUC": 0.7090827191037619,
        "kNN1NAUC": 0.716082344973639,
        "J48.001.Kappa": 0.375395542857667,
        "MeanSkewnessOfNumericAtts": 7.440976027873651,
        "Quartile1StdDevOfNumericAtts": 0.9727856745152441,
        "REPTreeDepth2AUC": 0.7474597786162569,
        "CfsSubsetEval_kNN1NErrRate": 0.4851258581235698,
        "kNN1NErrRate": 0.4635501797973194,
        "MajorityClassPercentage": 41.745668519123896,
        "MeanStdDevOfNumericAtts": 0.9916438519187979,
        "Quartile2AttributeEntropy": null,
        "REPTreeDepth2ErrRate": 0.5052304674730304,
        "CfsSubsetEval_kNN1NKappa": 0.346242749551416
    },
    "tags": [
        {
            "tag": "Chemistry",
            "uploader": "38960"
        },
        {
            "tag": "Life Science",
            "uploader": "38960"
        },
        {
            "tag": "OpenML-CC18",
            "uploader": "1"
        },
        {
            "tag": "OpenML100",
            "uploader": "348"
        },
        {
            "tag": "study_123",
            "uploader": "3886"
        },
        {
            "tag": "study_14",
            "uploader": "64"
        },
        {
            "tag": "study_34",
            "uploader": "1"
        },
        {
            "tag": "study_50",
            "uploader": "64"
        },
        {
            "tag": "study_52",
            "uploader": "64"
        },
        {
            "tag": "study_7",
            "uploader": "64"
        },
        {
            "tag": "study_98",
            "uploader": "1935"
        },
        {
            "tag": "study_99",
            "uploader": "1"
        },
        {
            "tag": "study_225",
            "uploader": "0"
        },
        {
            "tag": "study_236",
            "uploader": "0"
        },
        {
            "tag": "study_293",
            "uploader": "0"
        },
        {
            "tag": "study_270",
            "uploader": "0"
        },
        {
            "tag": "study_271",
            "uploader": "0"
        },
        {
            "tag": "study_253",
            "uploader": "0"
        },
        {
            "tag": "study_282",
            "uploader": "0"
        },
        {
            "tag": "study_275",
            "uploader": "0"
        }
    ],
    "features": [
        {
            "name": "Class",
            "index": "51",
            "type": "nominal",
            "distinct": "6",
            "missing": "0",
            "target": "1",
            "distr": [
                [
                    "1",
                    "2",
                    "3",
                    "4",
                    "5",
                    "6"
                ],
                [
                    [
                        "1089",
                        "0",
                        "0",
                        "0",
                        "0",
                        "0"
                    ],
                    [
                        "0",
                        "486",
                        "0",
                        "0",
                        "0",
                        "0"
                    ],
                    [
                        "0",
                        "0",
                        "748",
                        "0",
                        "0",
                        "0"
                    ],
                    [
                        "0",
                        "0",
                        "0",
                        "617",
                        "0",
                        "0"
                    ],
                    [
                        "0",
                        "0",
                        "0",
                        "0",
                        "624",
                        "0"
                    ],
                    [
                        "0",
                        "0",
                        "0",
                        "0",
                        "0",
                        "2554"
                    ]
                ]
            ]
        },
        {
            "name": "V1",
            "index": "0",
            "type": "numeric",
            "distinct": "1309",
            "missing": "0",
            "min": "-1",
            "max": "2",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V2",
            "index": "1",
            "type": "numeric",
            "distinct": "1194",
            "missing": "0",
            "min": "-4",
            "max": "1",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V3",
            "index": "2",
            "type": "numeric",
            "distinct": "1148",
            "missing": "0",
            "min": "-1",
            "max": "3",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V4",
            "index": "3",
            "type": "numeric",
            "distinct": "1261",
            "missing": "0",
            "min": "-1",
            "max": "3",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V5",
            "index": "4",
            "type": "numeric",
            "distinct": "1394",
            "missing": "0",
            "min": "-1",
            "max": "2",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V6",
            "index": "5",
            "type": "numeric",
            "distinct": "1030",
            "missing": "0",
            "min": "-1",
            "max": "7",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V7",
            "index": "6",
            "type": "numeric",
            "distinct": "1309",
            "missing": "0",
            "min": "-2",
            "max": "1",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V8",
            "index": "7",
            "type": "numeric",
            "distinct": "49",
            "missing": "0",
            "min": "-1",
            "max": "32",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V9",
            "index": "8",
            "type": "numeric",
            "distinct": "1883",
            "missing": "0",
            "min": "-1",
            "max": "15",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V10",
            "index": "9",
            "type": "numeric",
            "distinct": "29",
            "missing": "0",
            "min": "-1",
            "max": "11",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V11",
            "index": "10",
            "type": "numeric",
            "distinct": "2431",
            "missing": "0",
            "min": "-2",
            "max": "9",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V12",
            "index": "11",
            "type": "numeric",
            "distinct": "219",
            "missing": "0",
            "min": "0",
            "max": "42",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V13",
            "index": "12",
            "type": "numeric",
            "distinct": "3079",
            "missing": "0",
            "min": "-1",
            "max": "23",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V14",
            "index": "13",
            "type": "numeric",
            "distinct": "82",
            "missing": "0",
            "min": "-3",
            "max": "1",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V15",
            "index": "14",
            "type": "numeric",
            "distinct": "4674",
            "missing": "0",
            "min": "0",
            "max": "31",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V16",
            "index": "15",
            "type": "numeric",
            "distinct": "3095",
            "missing": "0",
            "min": "-2",
            "max": "4",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V17",
            "index": "16",
            "type": "numeric",
            "distinct": "1969",
            "missing": "0",
            "min": "0",
            "max": "18",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V18",
            "index": "17",
            "type": "numeric",
            "distinct": "134",
            "missing": "0",
            "min": "-2",
            "max": "6",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V19",
            "index": "18",
            "type": "numeric",
            "distinct": "3368",
            "missing": "0",
            "min": "-3",
            "max": "10",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V20",
            "index": "19",
            "type": "numeric",
            "distinct": "108",
            "missing": "0",
            "min": "-3",
            "max": "13",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V21",
            "index": "20",
            "type": "numeric",
            "distinct": "3841",
            "missing": "0",
            "min": "-2",
            "max": "37",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V22",
            "index": "21",
            "type": "numeric",
            "distinct": "103",
            "missing": "0",
            "min": "-2",
            "max": "14",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V23",
            "index": "22",
            "type": "numeric",
            "distinct": "4182",
            "missing": "0",
            "min": "-3",
            "max": "8",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V24",
            "index": "23",
            "type": "numeric",
            "distinct": "121",
            "missing": "0",
            "min": "-2",
            "max": "10",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V25",
            "index": "24",
            "type": "numeric",
            "distinct": "4393",
            "missing": "0",
            "min": "-2",
            "max": "9",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V26",
            "index": "25",
            "type": "numeric",
            "distinct": "803",
            "missing": "0",
            "min": "-1",
            "max": "15",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V27",
            "index": "26",
            "type": "numeric",
            "distinct": "4560",
            "missing": "0",
            "min": "-2",
            "max": "13",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V28",
            "index": "27",
            "type": "numeric",
            "distinct": "1023",
            "missing": "0",
            "min": "0",
            "max": "28",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V29",
            "index": "28",
            "type": "numeric",
            "distinct": "4709",
            "missing": "0",
            "min": "-1",
            "max": "29",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V30",
            "index": "29",
            "type": "numeric",
            "distinct": "69",
            "missing": "0",
            "min": "0",
            "max": "7",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V31",
            "index": "30",
            "type": "numeric",
            "distinct": "79",
            "missing": "0",
            "min": "-1",
            "max": "5",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V32",
            "index": "31",
            "type": "numeric",
            "distinct": "82",
            "missing": "0",
            "min": "-3",
            "max": "1",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V33",
            "index": "32",
            "type": "numeric",
            "distinct": "23",
            "missing": "0",
            "min": "0",
            "max": "55",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V34",
            "index": "33",
            "type": "numeric",
            "distinct": "31",
            "missing": "0",
            "min": "0",
            "max": "16",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V35",
            "index": "34",
            "type": "numeric",
            "distinct": "48",
            "missing": "0",
            "min": "0",
            "max": "10",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V36",
            "index": "35",
            "type": "numeric",
            "distinct": "70",
            "missing": "0",
            "min": "0",
            "max": "68",
            "mean": "0",
            "stdev": "2"
        },
        {
            "name": "V37",
            "index": "36",
            "type": "numeric",
            "distinct": "1053",
            "missing": "0",
            "min": "0",
            "max": "15",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V38",
            "index": "37",
            "type": "numeric",
            "distinct": "1569",
            "missing": "0",
            "min": "-1",
            "max": "16",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V39",
            "index": "38",
            "type": "numeric",
            "distinct": "893",
            "missing": "0",
            "min": "0",
            "max": "16",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V40",
            "index": "39",
            "type": "numeric",
            "distinct": "72",
            "missing": "0",
            "min": "0",
            "max": "29",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V41",
            "index": "40",
            "type": "numeric",
            "distinct": "1041",
            "missing": "0",
            "min": "0",
            "max": "15",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V42",
            "index": "41",
            "type": "numeric",
            "distinct": "37",
            "missing": "0",
            "min": "0",
            "max": "31",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V43",
            "index": "42",
            "type": "numeric",
            "distinct": "29",
            "missing": "0",
            "min": "0",
            "max": "54",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V44",
            "index": "43",
            "type": "numeric",
            "distinct": "1698",
            "missing": "0",
            "min": "-1",
            "max": "2",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V45",
            "index": "44",
            "type": "numeric",
            "distinct": "2246",
            "missing": "0",
            "min": "-2",
            "max": "1",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V46",
            "index": "45",
            "type": "numeric",
            "distinct": "1941",
            "missing": "0",
            "min": "-1",
            "max": "3",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V47",
            "index": "46",
            "type": "numeric",
            "distinct": "1676",
            "missing": "0",
            "min": "-1",
            "max": "2",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V48",
            "index": "47",
            "type": "numeric",
            "distinct": "1703",
            "missing": "0",
            "min": "0",
            "max": "3",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V49",
            "index": "48",
            "type": "numeric",
            "distinct": "2315",
            "missing": "0",
            "min": "-1",
            "max": "2",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V50",
            "index": "49",
            "type": "numeric",
            "distinct": "1537",
            "missing": "0",
            "min": "0",
            "max": "10",
            "mean": "0",
            "stdev": "1"
        },
        {
            "name": "V51",
            "index": "50",
            "type": "numeric",
            "distinct": "2462",
            "missing": "0",
            "min": "-2",
            "max": "1",
            "mean": "0",
            "stdev": "1"
        }
    ],
    "nr_of_issues": 0,
    "nr_of_downvotes": 0,
    "nr_of_likes": 1,
    "nr_of_downloads": 21,
    "total_downloads": 40,
    "reach": 22,
    "reuse": 45,
    "impact_of_reuse": 0,
    "reach_of_reuse": 0,
    "impact": 45
}