{"entities":{"Q5370898":{"pageid":7400472,"ns":120,"title":"Item:Q5370898","lastrevid":92249411,"modified":"2026-06-05T01:14:50Z","type":"item","id":"Q5370898","labels":{"en":{"language":"en","value":"Complexity verification using guided theorem enumeration"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6794684"}},"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":"Q5370898$011F6472-EB43-4EE1-AD91-030CAB2D3DBD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bb2cb6c6ea915e0d86abfd119422533a1e86715c","datavalue":{"value":{"text":"Complexity verification using guided theorem enumeration","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5370898$0921573F-E64A-432A-A407-0AC53F81A8E2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"13d3306dd0cf60b181f223718b5ffe0cd6d5033d","datavalue":{"value":"1380.68284","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370898$B692B68D-3BCB-463F-8FAF-09A41E4B24AD","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1b821ba4e1d268c9ee20917ce7a61baf434f06d2","datavalue":{"value":"10.1145/3009837.3009864","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370898$068DE406-411A-4511-98B2-9D9CB827D477","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2245f1136ed3d9795d13ae09615b2c9fd81f7a09","datavalue":{"value":{"entity-type":"item","numeric-id":5370896,"id":"Q5370896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370898$592D9D4A-05AD-4C8E-A9EC-CF7C3B36A1F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d6e5e07a0abbe7ea1888645c300301fb82fdb43a","datavalue":{"value":{"entity-type":"item","numeric-id":5370897,"id":"Q5370897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370898$26E257AC-5C06-4797-A9AA-99DBAF2AE4EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"90445a82981b6e7b2f2657e880bf9e7e26c8ddbb","datavalue":{"value":{"entity-type":"item","numeric-id":1696588,"id":"Q1696588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370898$293C55AE-1F1F-4B19-9AD3-AAB869F4E745","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e2300a4bb532724f6695014ad32dc9335c9fdde3","datavalue":{"value":{"entity-type":"item","numeric-id":5370840,"id":"Q5370840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370898$B5FA3559-EEBD-4A6D-8BBE-0113761F7715","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c23b22abb6cd47509eac4c3e5d58b13717e9ea4","datavalue":{"value":{"time":"+2017-10-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5370898$3B956246-12C1-486B-B9BC-FC8C580D1F9F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370898$281D1EA9-C91A-44E4-A417-056FE10D88E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370898$1A5A2A9A-C6E9-4223-B82F-E194DCB35DE8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6e461aed20d2c3f82533ebddeedb1ffe24d4b716","datavalue":{"value":"6794684","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370898$24F1C73B-ED17-4C20-8AEF-FD47A279F48C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5f8382ba04f9f05f645b4d0e4b9ea28f0619583","datavalue":{"value":"complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370898$AEB409CA-9CC9-4E2B-981E-73C92C7A63D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9bc6474ad8409ef4528af84655741b6b5be3d7c","datavalue":{"value":"interpolation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370898$8BF340BE-0B74-4489-94DB-E47DA58F7CAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"934102fa9f8df2a9f8e7be5ae7fb3384fbe95989","datavalue":{"value":"theorem grounding","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370898$2780AA3A-768F-47A8-948E-CF8D79EC5022","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"544285ff7639d6e2f1833203ed056490a36c6e30","datavalue":{"value":{"entity-type":"item","numeric-id":21115,"id":"Q21115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370898$627707E4-27E4-4575-8C33-85FC6C0062CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f5d485aaf0775c43cdf0d13e0f4e6342461ec8dd","datavalue":{"value":{"entity-type":"item","numeric-id":33507,"id":"Q33507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370898$61494EF9-42B5-4973-B860-4767124A014E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"562adc39cf7a987a51555fef3f75195b4a9ddeec","datavalue":{"value":{"entity-type":"item","numeric-id":33506,"id":"Q33506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370898$45B41158-13F4-47D3-8902-F62A9C4FF692","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":"Q5370898$D203024A-6DB9-4738-BB1A-197CDC1DFF2C","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":"Q5370898$C9B70CE2-846D-42E7-98D3-59CD5584AB56","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"49d55251325376d3f77e8ef26048dfd62013447c","datavalue":{"value":"https://doi.org/10.1145/3009837.3009864","type":"string"},"datatype":"url"},"type":"statement","id":"Q5370898$7140F93E-C069-4EB2-8D7A-B0A2A41EC98E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"26a5e4a1f4555df04e96c573b049f22cafb6cb9d","datavalue":{"value":"W2565511473","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370898$812B35DE-1E50-4F32-9644-4226817A414F","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ffbdc3e193b70fb73f96f46503b68552faa3c66b","datavalue":{"value":"Q131117542","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370898$BA794CF6-4012-4717-B7E6-93ABCF1ABEC2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59bfbdc7e86cccf445f54e1e3091c5033971a071","datavalue":{"value":{"entity-type":"item","numeric-id":2323994,"id":"Q2323994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4854cdb3bebc39ebddcbc906c7e86b1ba65d478b","datavalue":{"value":{"amount":"+0.7200900316238403","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":"Q5370898$B40BB4FE-3F53-4D38-9C9B-21A15E4897F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"829403039d4597098f6869563c6c587368fb3adb","datavalue":{"value":{"entity-type":"item","numeric-id":2883083,"id":"Q2883083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c37a667b1087e54871697466b156627522dc4531","datavalue":{"value":{"amount":"+0.7109110951423645","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":"Q5370898$04A30F94-260E-4EFD-AA31-CCE1053E8AFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7d458edef0a12fe970318efe1226e2d77f71467","datavalue":{"value":{"entity-type":"item","numeric-id":5261512,"id":"Q5261512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bbc7465906b8af10aa5dae8a775df5b5dfa1da78","datavalue":{"value":{"amount":"+0.7063595056533813","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":"Q5370898$3CC0BE51-52B7-40D0-A23F-D139BC466433","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0667b953dc767cf4cd903ac17fa69f11f3b19d0d","datavalue":{"value":{"entity-type":"item","numeric-id":2164211,"id":"Q2164211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5dafbfe736ef1a849673a32ba66c8668c4042f88","datavalue":{"value":{"amount":"+0.7029646039009094","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":"Q5370898$04FA9313-952D-49EC-A3A4-DCD48059DD82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e830bddf2f5d41ef29146b9c90592c5455f9bc17","datavalue":{"value":{"entity-type":"item","numeric-id":5464660,"id":"Q5464660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a1195031d28a3e2cef85cc3bad45a5c759a85179","datavalue":{"value":{"amount":"+0.6987842917442322","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":"Q5370898$CAAB40EA-AE63-42D9-A6B3-C27B2D35D0CE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Complexity verification using guided theorem enumeration","badges":[]}}}}}