{
    "info": {
        "author": "Tobias Glei\u00dfner",
        "author_email": "tobias.gleissner@fu-berlin.de",
        "bugtrack_url": null,
        "classifiers": [
            "Development Status :: 2 - Pre-Alpha",
            "Environment :: Console",
            "Environment :: Web Environment",
            "Intended Audience :: Developers",
            "Intended Audience :: Education",
            "Intended Audience :: Information Technology",
            "Intended Audience :: Legal Industry",
            "Intended Audience :: Science/Research",
            "Programming Language :: Python :: 3.5",
            "Programming Language :: Python :: 3.6",
            "Programming Language :: Python :: 3.7",
            "Programming Language :: Python :: 3.8",
            "Programming Language :: Python :: 3.9",
            "Topic :: Scientific/Engineering :: Artificial Intelligence"
        ],
        "description": "# A TPTP python package\n\n## Installation\n* install python >= 3.5\n* clone this repository\n\n## Usage\n\n### Run locally:\nList all solvers\n```\npython3 -m tptp local list-solvers\n```\n\nRun Leo III.\n```\n$ python3 -m tptp local run --solver-name leo3 --problem problems/SYN001+1.p --timeout 60\n```\n\nRun cvc4\n```\n$ python3 -m tptp local run --solver-name cvc4 --problem problems/SYN001+1.p --timeout 60\n```\n\n### Run System-on-TPTP:\n\nList all solvers\n```\n$ python3 -m tptp system-on-tptp list-solvers\n```\n\nRun Leo III.\n```\n$ python3 -m tptp system-on-tptp request --solver-name \"Leo-III---1.4\" --solver-command \"run_Leo-III %s %d\" --problem \"problems/SYN001+1.p\" \n```\n\n### Test the competition mode\n```\n$ python3 -m tptp competition competition-test/definition.py\n```\n\nRun with more output. Good for error tracking.\n```\n$ python3 -m tptp competition competition-test/definition.py --verbose\n```\n\n## Making a solver TPTP ready\n### SZS Status, SZS Ontology\nA solver can be used by this libary if it supports the SZS Ontology as its result on the ```stdout```.\n\nThe solution status should be reported exactly once, in a line starting ```% SZS status\"``` (the leading '%' makes the line into a TPTP language comment). \n\nFor instance, a SAT-solver started for problem ```SYN001+1``` should output the line\n```\n% SZS status Satisfiable for SYN001+1\n```\nas part of its output if it proves the problem is ```satisfiable```.\n\nConsequently:\n* if your solver proves the problem is ```unsatisfiable```, the line ```% SZS status Unsatisfiable for SYN001+1```.\n* if your solver ```gaves up``` the prove, the line ```% SZS status GaveUp for SYN001+1```.\n* a full list of possible values for the SZS Status can be found at the [SZS Ontology](http://www.tptp.org/cgi-bin/SeeTPTP?Category=Documents&File=SZSOntology) definition.\n\nAny prove or prove-model should additionally be printed on the stdout in the following form.\n```\n% SZS output start CNFRefutation for SYN001+1\n  ...\n% SZS output end CNFRefutation for SYN001+1\n```\n\n### Test your solver\nTo test your solve add it to our test competition, which can be found at\n```\ncompetition-test/definition.py\n```\n\nHere you add your solver to the ```SOLVERS``` constant\n```python\nSOLVERS = (\n    ...\n    {\n        'type': 'local',\n        'name': 'my-solver',\n        'pretty-name': 'MySolver'\n        'command': 'my-solver-binary-or-shell-script %s -t %d',\n    },\n    ...\n)\n```\n\nThis will ensure that your solver\n* is called ```my-solver``` and is pretty printed ```MySolver```\n* when invoked to solve the problem ```absolute/path/SYN001+1.p``` within a timeout of ```60``` seconds the\n  program/shellscript ```my-solver-binary-or-shell-script \"absolute/path/SYN001+1.p\" -t 60``` is called\n* your problem should output an SZS Status from the SZS Ontology (see above)\n\nRunning our test competition should now list your solver.\n```\n$ python3 -m tptp competition competition-test/definition.py\n...\n% Satisfiable for Sat1.cnf expecting Satisfiable with MySolver -t 60s which is correct\n...\n```\n\n\n",
        "description_content_type": "text/markdown",
        "docs_url": null,
        "download_url": "",
        "downloads": {
            "last_day": -1,
            "last_month": -1,
            "last_week": -1
        },
        "home_page": "https://github.com/leoprover/tptp",
        "keywords": "",
        "license": "BSD3",
        "maintainer": "",
        "maintainer_email": "",
        "name": "tptp",
        "package_url": "https://pypi.org/project/tptp/",
        "platform": "",
        "project_url": "https://pypi.org/project/tptp/",
        "project_urls": {
            "Homepage": "https://github.com/leoprover/tptp"
        },
        "release_url": "https://pypi.org/project/tptp/0.0.3.dev2/",
        "requires_dist": [
            "pathlib",
            "lxml",
            "requests",
            "colorama"
        ],
        "requires_python": ">=3.5",
        "summary": "A library for handling TPTP related input and systems",
        "version": "0.0.3.dev2"
    },
    "last_serial": 5878414,
    "releases": {
        "0.0.3.dev2": [
            {
                "comment_text": "",
                "digests": {
                    "md5": "e3dbd48fddb775b0683bd56132dbe9fb",
                    "sha256": "e282aad090f0f2c0e7288dfdb92cfd0d85b71032fa34fe8845f7dcfbc3c232da"
                },
                "downloads": -1,
                "filename": "tptp-0.0.3.dev2-py3-none-any.whl",
                "has_sig": false,
                "md5_digest": "e3dbd48fddb775b0683bd56132dbe9fb",
                "packagetype": "bdist_wheel",
                "python_version": "py3",
                "requires_python": ">=3.5",
                "size": 45233,
                "upload_time": "2019-09-24T08:50:39",
                "url": "https://files.pythonhosted.org/packages/bd/47/aa5fb605fdf261c7f1096b4ed3526b1d9052712ecebb34d67809adddfba7/tptp-0.0.3.dev2-py3-none-any.whl"
            },
            {
                "comment_text": "",
                "digests": {
                    "md5": "167dd84cea33cc7edcf20fef6284c0f7",
                    "sha256": "d462d7dc40118f1bfb0d63b663d467b495bd10c6a76da49e986648e78b4bd755"
                },
                "downloads": -1,
                "filename": "tptp-0.0.3.dev2.tar.gz",
                "has_sig": false,
                "md5_digest": "167dd84cea33cc7edcf20fef6284c0f7",
                "packagetype": "sdist",
                "python_version": "source",
                "requires_python": ">=3.5",
                "size": 31291,
                "upload_time": "2019-09-24T08:50:42",
                "url": "https://files.pythonhosted.org/packages/46/3e/87eda2aa3a485297769487586f6ac7b7195f95e51c358402190c86ce3d54/tptp-0.0.3.dev2.tar.gz"
            }
        ]
    },
    "urls": [
        {
            "comment_text": "",
            "digests": {
                "md5": "e3dbd48fddb775b0683bd56132dbe9fb",
                "sha256": "e282aad090f0f2c0e7288dfdb92cfd0d85b71032fa34fe8845f7dcfbc3c232da"
            },
            "downloads": -1,
            "filename": "tptp-0.0.3.dev2-py3-none-any.whl",
            "has_sig": false,
            "md5_digest": "e3dbd48fddb775b0683bd56132dbe9fb",
            "packagetype": "bdist_wheel",
            "python_version": "py3",
            "requires_python": ">=3.5",
            "size": 45233,
            "upload_time": "2019-09-24T08:50:39",
            "url": "https://files.pythonhosted.org/packages/bd/47/aa5fb605fdf261c7f1096b4ed3526b1d9052712ecebb34d67809adddfba7/tptp-0.0.3.dev2-py3-none-any.whl"
        },
        {
            "comment_text": "",
            "digests": {
                "md5": "167dd84cea33cc7edcf20fef6284c0f7",
                "sha256": "d462d7dc40118f1bfb0d63b663d467b495bd10c6a76da49e986648e78b4bd755"
            },
            "downloads": -1,
            "filename": "tptp-0.0.3.dev2.tar.gz",
            "has_sig": false,
            "md5_digest": "167dd84cea33cc7edcf20fef6284c0f7",
            "packagetype": "sdist",
            "python_version": "source",
            "requires_python": ">=3.5",
            "size": 31291,
            "upload_time": "2019-09-24T08:50:42",
            "url": "https://files.pythonhosted.org/packages/46/3e/87eda2aa3a485297769487586f6ac7b7195f95e51c358402190c86ce3d54/tptp-0.0.3.dev2.tar.gz"
        }
    ]
}