{"entities":{"Q5747649":{"pageid":7777200,"ns":120,"title":"Item:Q5747649","lastrevid":41573006,"modified":"2025-05-06T00:12:49Z","type":"item","id":"Q5747649","labels":{"en":{"language":"en","value":"Fast LCF-Style Proof Reconstruction for Z3"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5785342"}},"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":"Q5747649$D373360B-A603-422D-B4CB-322464838419","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f0ff89ebc1313ae804a8775ff921cdbb94c6c91b","datavalue":{"value":{"text":"Fast LCF-Style Proof Reconstruction for Z3","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5747649$F82D5938-CE2A-4409-8F5E-F7237078E4AD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c41b546cc0b09bcc7244287b58365ac4f7072842","datavalue":{"value":"1291.68328","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747649$91879B2E-D6E2-417E-9449-EA8AB443A716","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"483d751b63fffc2ff3779dca384d6909a9e6e15a","datavalue":{"value":"10.1007/978-3-642-14052-5_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747649$B04E3542-0255-4B0C-860A-F8C1A219CF42","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e52ea9fecc32655489a0560f1f3a2c96d34140f0","datavalue":{"value":{"entity-type":"item","numeric-id":287336,"id":"Q287336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747649$101DE6EF-4124-446A-A037-7E2F8C95CC43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d1f8cd3b806fd78547b3f4844ba487e41a5ec455","datavalue":{"value":{"entity-type":"item","numeric-id":286783,"id":"Q286783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747649$6D7C9E7B-1D62-4226-8B97-9556EF776067","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747649$41E7EF6A-A564-4D80-9DD4-35B150E99ED3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5f7d3744053f89b932df935693d4d726597e5f91","datavalue":{"value":{"time":"+2010-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5747649$FEBAA3C8-4C8B-48C8-9729-82EF44A56131","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747649$8762A163-F234-4683-8093-12AAEBE58469","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0ff93327130a9fc69c5c773f243f0ba387d1338c","datavalue":{"value":"5785342","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747649$376C2518-1F3C-41EA-AF7A-39F7A05C1E63","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cd543fd49199b1838ba332ea5e7b335fbe6c5a58","datavalue":{"value":{"entity-type":"item","numeric-id":19608,"id":"Q19608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747649$6E6A9BFF-96EC-4726-BCDB-0189CD831A5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"43f7c4ee5068daf82f8bffbb0f7510a5f16faf63","datavalue":{"value":{"entity-type":"item","numeric-id":16615,"id":"Q16615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747649$153D4E7D-FF0B-4A62-A68D-268180D5E32C","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":"Q5747649$2D135099-F9B9-4309-80FF-11F1644105B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747649$6AB1732B-3CB8-4C40-B1C0-4BD2BF27B1ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747649$B9F35B16-32BB-4F99-A429-D590F85E821B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747649$FC28F7AF-642A-4932-9FCE-3EBA724A8A61","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":"Q5747649$CFC81718-A6BE-4B1B-B7EE-47C770E39C6F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"16a54de3fb2031c9507c8f7c392ae3296d9f453a","datavalue":{"value":"https://doi.org/10.1007/978-3-642-14052-5_14","type":"string"},"datatype":"url"},"type":"statement","id":"Q5747649$23116DAC-AA61-4021-B17C-AA71B443A79A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9d49c16833c41e7adb04e8f24ecc94b1a04399d5","datavalue":{"value":"W1552715853","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747649$E642B3FF-AC1A-405B-875B-4FD0DEBD10FD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba3d44bbd36b0708161e2ec3ff7b4197443a7cb0","datavalue":{"value":{"entity-type":"item","numeric-id":3100212,"id":"Q3100212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4bb70d2e214c1e033d7a3e774fb828d9f76e0adf","datavalue":{"value":{"amount":"+0.8603772","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5747649$E751575C-1CF4-4134-BBC5-2E003CB4AD13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3c96f31c21c599df4912deaf373beaff916e5fa6","datavalue":{"value":{"entity-type":"item","numeric-id":5743488,"id":"Q5743488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a8d1aeacc98132667ee4949ee48c707f395846a","datavalue":{"value":{"amount":"+0.82848287","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5747649$0D19ED62-DA21-475E-BD4E-35515097E2CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3887436224fbac122f76103186469b3b0ecfe68c","datavalue":{"value":{"entity-type":"item","numeric-id":4962203,"id":"Q4962203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a8d1aeacc98132667ee4949ee48c707f395846a","datavalue":{"value":{"amount":"+0.82848287","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5747649$9B11159D-5680-490A-A29F-AB1CAD066339","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30337d26ba6b5d33cb4176f2a080ff9d9c543f8f","datavalue":{"value":{"entity-type":"item","numeric-id":876046,"id":"Q876046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3c0feb541c9c9beb43d27ad4f710ee4b07d81727","datavalue":{"value":{"amount":"+0.8208203","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5747649$5E1784D1-3B46-4BD3-8BAC-2BD07DF09D46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43c75afe9048b90d96d419aafcc8f618e7a8d0d9","datavalue":{"value":{"entity-type":"item","numeric-id":1334905,"id":"Q1334905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0359cba6044319ceaeee42a57a2a3f427d2e7fef","datavalue":{"value":{"amount":"+0.8111561","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5747649$122B65A7-3968-4C85-AC61-1FC10F689DD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"886821d968a74ddfc204486ec05d48aba98cd2f7","datavalue":{"value":{"entity-type":"item","numeric-id":832321,"id":"Q832321"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8ec252cdd68bb691d7b43b7bab0fa1d4cfec3052","datavalue":{"value":{"amount":"+0.8104347","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5747649$CC1FF0D1-6F08-4EAB-92DC-7AEFDFBA27DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3301eaabd8b9cecc3120b315096a41a88aa00005","datavalue":{"value":{"entity-type":"item","numeric-id":5327336,"id":"Q5327336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45b6ef0c273655cb3f4591c995386fc832a64c69","datavalue":{"value":{"amount":"+0.8096859","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5747649$05C5C050-BA1C-4B3C-BAC3-CBBEF2D6CB7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26f14e4aeab67c72b756c0ccbc192de1aea09f40","datavalue":{"value":{"entity-type":"item","numeric-id":2868803,"id":"Q2868803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d2de4f51ed82cfde6dff6efbe023405140adcb05","datavalue":{"value":{"amount":"+0.80793923","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5747649$95A0538C-DABB-469B-A5E6-D091E93F1720","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5b89d9c65c96bcb4fc81fea1c97b652c1967661","datavalue":{"value":{"entity-type":"item","numeric-id":3608434,"id":"Q3608434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53f151d55c7de33221e0a4232298d7c3b9f8c105","datavalue":{"value":{"amount":"+0.8076569","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5747649$A405608D-1E5E-4CF1-8DED-4DF1DAB3575F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5747649","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5747649"}}}}}