{"entities":{"Q3454101":{"pageid":5233501,"ns":120,"title":"Item:Q3454101","lastrevid":52405955,"modified":"2026-01-22T14:06:11Z","type":"item","id":"Q3454101","labels":{"en":{"language":"en","value":"SMTtoTPTP -- a converter for theorem proving formats"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6515513"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454101$0DC48221-D510-4E29-9B56-06E4560764BD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7275a996824339da27de4d35c28509f9435565d6","datavalue":{"value":{"text":"SMTtoTPTP \u2013 A Converter for Theorem Proving Formats","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3454101$D022490E-7860-4D4B-BD30-499F229737A8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"72c71a90fb82c33ad406d55e984af74cd03a3ae8","datavalue":{"value":"1465.68276","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454101$9903213E-9E99-460F-A3BE-A00799F91544","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5f8dffaf155c422f4d4a7048e07a566e5544758c","datavalue":{"value":"10.1007/978-3-319-21401-6_19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454101$306B089D-A04C-4AF7-920E-11497F95467C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"63095d86c000f08026b5823fdf1f8a25bfef2e00","datavalue":{"value":{"entity-type":"item","numeric-id":167057,"id":"Q167057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454101$AB0474F8-117C-4403-AE30-2905F22F19E8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3cc4c7edeb37e5e3024aeff0de74501df6e066e3","datavalue":{"value":{"entity-type":"item","numeric-id":3454078,"id":"Q3454078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454101$4A147AB5-1616-4555-949F-75CB4FB98C51","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f34c33daac76be2878f4eb0eeca7aa927e679a8","datavalue":{"value":{"time":"+2015-12-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3454101$191E5C43-98F7-437B-BCAE-D60AF617454E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454101$CAC9FCCC-7AE3-4BBC-9B3D-AC6C6DE60308","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c90cc862797b61aee67bab3ee24897a1c44a3773","datavalue":{"value":"6515513","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454101$AC656509-935D-4C0B-B8BC-9BF9E33997EC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454101$D0ADDB4D-5B76-4BF7-9494-E1BB4E120BDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454101$BAA1F469-9DA8-4CF7-AC84-862423861BEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454101$D77B76A2-0EE8-431B-BFCD-1EAD3B8E1C44","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454101$9D8A4B92-CEC1-4995-B089-085D77F2D17B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b72650ecbb1c1bd06dd1ca7ab6e45b3496360733","datavalue":{"value":"https://doi.org/10.1007/978-3-319-21401-6_19","type":"string"},"datatype":"url"},"type":"statement","id":"Q3454101$E5382D04-427E-4F58-846B-9FB36262C03C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5f17a934495d47560dfffadf822cead346308530","datavalue":{"value":"W1604495270","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454101$75CE690A-8B2B-4EC8-B46C-4DD7DC0369A2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c4669aa80f1b8115df57035710adf683c0764c3","datavalue":{"value":{"entity-type":"item","numeric-id":4928456,"id":"Q4928456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454101$64B7EEDC-4F3B-42B3-9FBC-807834C00CD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454101$46B01DEC-32C9-4F3F-A3A3-4C1909CDB213","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a4e0edf0e28b481677ec6286aff34ea615b8e86","datavalue":{"value":{"entity-type":"item","numeric-id":2891471,"id":"Q2891471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454101$F96219EA-851B-457E-9A70-A742F6672E32","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af82521c3a0087569af5fb986fd5dc32a05cff95","datavalue":{"value":{"entity-type":"item","numeric-id":1694574,"id":"Q1694574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25cbd622ff74dde7c4ace5fe21bdaee959127e2c","datavalue":{"value":{"amount":"+0.7512365579605103","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3454101$37E218D5-2DA4-4FA3-B8D6-E7F744D80C12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13f103237e1b4889a22b078c6687a2ac0c70875b","datavalue":{"value":{"entity-type":"item","numeric-id":5210777,"id":"Q5210777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"14e6ce0806e7bc0edaa2991d3764e5b8fec429d7","datavalue":{"value":{"amount":"+0.7435253262519836","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3454101$358AE569-E671-4758-B5E7-DFBA26A1D3BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"113e2d1d879d9c142457b829e6b1af5a24f50a97","datavalue":{"value":{"entity-type":"item","numeric-id":4928456,"id":"Q4928456"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f554115fb0afacd3aeba27880e0627f1b88bc7ec","datavalue":{"value":{"amount":"+0.7360513806343079","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3454101$1E5C96A0-20AD-4DCE-B878-513F8FD8BA08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d2c14ed20a48c3aab929077d06fb2b3dc501071a","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f3fe069b6bceee91973394293c3c68ef130ddd0","datavalue":{"value":{"amount":"+0.7294303774833679","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3454101$124CE4E0-5FFC-489A-BB27-931BBCEFD2FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"833679bd5dba8272dd461558b8d437f3c0e999af","datavalue":{"value":{"entity-type":"item","numeric-id":4916228,"id":"Q4916228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f123d8754b79c7fa078b472f3ee5729f2d4a0de0","datavalue":{"value":{"amount":"+0.7157616019248962","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3454101$E03D1BCF-11A6-416E-8FE7-ED4F47F41D1A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3454101","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3454101"}}}}}