{"entities":{"Q286784":{"pageid":288551,"ns":120,"title":"Item:Q286784","lastrevid":60662424,"modified":"2026-04-10T18:21:57Z","type":"item","id":"Q286784","labels":{"en":{"language":"en","value":"The 2013 evaluation of SMT-COMP and SMT-LIB"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6585235"}},"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":"Q286784$9D51C60A-B4CE-488D-8AD6-25462D2F0BF0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d77a78e7546628b76e2f35dbb6a19ca48317011b","datavalue":{"value":{"text":"The 2013 evaluation of SMT-COMP and SMT-LIB","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q286784$B767E7F1-FA6E-4B1D-847D-329A07D51A49","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5b113e7c3572a48225c1ef9c8701d7f4223754c8","datavalue":{"value":"1356.68185","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286784$3311B4E9-5918-4ED1-B4CB-BAB3CA7CCA5B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8fccf28e5fb59a7359b1c673c6b1ec3dedd933d1","datavalue":{"value":{"entity-type":"item","numeric-id":286781,"id":"Q286781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286784$CD568F91-C4C3-4BA9-9C5C-D7126C378B0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7daa8e19dd762c08a3fe86309cfbf3893a62423c","datavalue":{"value":{"entity-type":"item","numeric-id":286782,"id":"Q286782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286784$6A118001-D0C5-41DA-B2BF-7C46B118BFAC","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":"Q286784$1E7A1710-7742-4422-A958-74B1D05CB0D3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286784$FE933D2A-8E49-4327-99FF-3DEA974DA82A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b626bb78b3e93b3076e6958296f7f25e2e74c3ab","datavalue":{"value":{"time":"+2016-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q286784$42553BBC-ADBD-4239-8C5C-85420487089A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286784$262F1B8D-ED05-47A4-AC5C-B22A6C5D5243","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"78f250da2b1d399377355781d49528dae5851bbb","datavalue":{"value":"6585235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286784$33BA428A-B65B-4FC3-9441-CBC2D5BA19EE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae8faa50294ada0a6f21782e773c449c8b4c7854","datavalue":{"value":"SMT-COMP","type":"string"},"datatype":"string"},"type":"statement","id":"Q286784$FA5E3371-B954-4B50-B52B-A9791A412340","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"655e59b317297bd0677a1c6892ce92baa484d23f","datavalue":{"value":"competition","type":"string"},"datatype":"string"},"type":"statement","id":"Q286784$B47D6E9D-9D00-4810-B98D-3AFB72916757","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b30a9b183f2157941e9c7d9f5d96193d061890c3","datavalue":{"value":"SMT-LIB","type":"string"},"datatype":"string"},"type":"statement","id":"Q286784$421FAA5D-4A10-4FC1-8E5F-FE583CE04B43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"61439d791f6aac729372268f16b553bcf47e3b78","datavalue":{"value":"SMT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q286784$99AF7101-C0C0-4329-A361-0C782DBE91D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q286784$74276B8F-5A41-4C67-A624-8E8DCC296550","rank":"normal"}],"P1463":[{"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":"Q286784$41707D0E-7BBF-47CE-841C-82B1B9C57BBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"45fa147ad24d78ff9111165d21eddec7203c8bfd","datavalue":{"value":{"entity-type":"item","numeric-id":20838,"id":"Q20838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286784$BF80B8D4-233D-4824-9A64-7FE56AE6637E","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":"Q286784$6033581B-1EBE-4166-BBD2-1443CA04D337","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e790d8a5cf3dfafc547a4c9188c945589ab5f382","datavalue":{"value":"https://doi.org/10.1007/s10817-015-9328-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q286784$E45DDBD3-B855-47E9-8DAC-9107F612B4C2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b7b30be22f1d3a2d99741845b263c2597ad0ab4c","datavalue":{"value":"W565454175","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286784$C55C51A7-9678-4859-9C3C-8DA2667A2C5F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"661f0b9795f66b5d2362d9e2b01387b3e66c126c","datavalue":{"value":{"entity-type":"item","numeric-id":3150299,"id":"Q3150299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286784$3C64C431-BDFD-4F9E-898E-2BEEF6C2C79C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66319efa68022a17b3f0d51cba4a6a8b45923c84","datavalue":{"value":{"entity-type":"item","numeric-id":5325882,"id":"Q5325882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286784$287C89AD-FA55-47A0-A8E6-5EF91A63A8A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bccd1fbbe7b06f5a2e523bc6b279f22309b5dc96","datavalue":{"value":{"entity-type":"item","numeric-id":5307082,"id":"Q5307082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q286784$09A85EAE-D52D-4ECE-94CB-A044727AE3E3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0344408244404e13e91927148550a60eede4169e","datavalue":{"value":"10.1007/S10817-015-9328-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q286784$FAD5BC7D-DB05-4904-BC45-54D14F67A4FE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f0de31b8c633fe95660b63c7beba4568cd0ee834","datavalue":{"value":{"entity-type":"item","numeric-id":861691,"id":"Q861691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"635c51e9848886887eacbd178b7a5ca8e30298ce","datavalue":{"value":{"amount":"+0.8070741295814514","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":"Q286784$89E997CE-79FB-491E-ACF5-39EA4DE225C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2643e601498b0a07c3125e9fd426278846b0b9ba","datavalue":{"value":{"entity-type":"item","numeric-id":5325882,"id":"Q5325882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e11d3b4c856c02d519bc24aaf436c83eb8e4ac1","datavalue":{"value":{"amount":"+0.780759334564209","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":"Q286784$4B7AB0FC-3D1E-4A21-A912-DA300DB15544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5893747e6d9d5cef32be8d1b739b1ddfd532bac3","datavalue":{"value":{"entity-type":"item","numeric-id":2461559,"id":"Q2461559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8b022895c6caeb8812975d33c8c1dacc57beb41","datavalue":{"value":{"amount":"+0.7778857350349426","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":"Q286784$CBF54BC4-B916-44BD-84B7-36156AC63FB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1f943c54080b27de44312af7634875e7f707904","datavalue":{"value":{"entity-type":"item","numeric-id":5716582,"id":"Q5716582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"390b8d1389bb7b03be2431a116e982740a8b1ba0","datavalue":{"value":{"amount":"+0.7463193535804749","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":"Q286784$7A640590-B1AF-4BE3-9860-EFB3940C76C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"126d4d871d06b17e7671c4bb12e3c63983c99e44","datavalue":{"value":{"entity-type":"item","numeric-id":5714765,"id":"Q5714765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a50eabb65ede3bc3ceaec72c8c5a18e669127d62","datavalue":{"value":{"amount":"+0.7208503484725952","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":"Q286784$0537567E-591B-43CC-8C9B-A70EE06E2F03","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The 2013 evaluation of SMT-COMP and SMT-LIB","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_2013_evaluation_of_SMT-COMP_and_SMT-LIB"}}}}}