{"entities":{"Q5210762":{"pageid":7240333,"ns":120,"title":"Item:Q5210762","lastrevid":53639177,"modified":"2026-01-25T11:42:25Z","type":"item","id":"Q5210762","labels":{"en":{"language":"en","value":"The search efficiency of theorem proving strategies"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7154538"}},"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":"Q5210762$39B5E8A1-3558-490B-A072-63AF4B2B20E2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fdee2a77c676e29252bb3575c7d1398d93fad0d4","datavalue":{"value":{"text":"The search efficiency of theorem proving strategies","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5210762$E1EBF694-AB86-486E-95D8-7877773E2B54","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3253e9c32ee410be6d1e59ea1b79500a28d84640","datavalue":{"value":"1433.68561","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5210762$86D3A8BE-CA78-4B29-90E8-53945894D74F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bf595227c4fb8a36adc200e1013ac9a359061aa7","datavalue":{"value":"10.1007/3-540-58156-1_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5210762$9DB2C68D-7B69-49AF-B6BC-FE5DABFC0473","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"5ce55bffd503afc59f0668cb8e4536460b24d029","datavalue":{"value":{"entity-type":"item","numeric-id":5210757,"id":"Q5210757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$057E67ED-BB4C-4929-AEB7-167D4D6D1A24","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3a33e9289a41a440ea82601c0f5c7fc7756e3797","datavalue":{"value":{"time":"+2020-01-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5210762$C85DFC33-D149-4DC5-B4E6-18EB20FAEBE8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5210762$636C9B36-ED2B-4393-BC44-9D1F0F6A5F04","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"122a6746b5d90db7bf7b18ebed2cbf08c578921e","datavalue":{"value":"7154538","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5210762$06508E9E-1B82-4919-B6B7-20E957E4C0EF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"34f99c9947f4d98af9da609b6496b55645bbe075","datavalue":{"value":{"entity-type":"item","numeric-id":1238600,"id":"Q1238600"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$928552F8-BC15-4A2A-9FAF-9D4034E40732","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":"Q5210762$8B04A904-2015-4ED0-AAC0-9F1096BD21EC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d7b1c4b335c77e12001aeb6140c556f5e046ab52","datavalue":{"value":"https://doi.org/10.1007/3-540-58156-1_5","type":"string"},"datatype":"url"},"type":"statement","id":"Q5210762$731253FE-CA97-4E95-9ED1-94F0AED2C437","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8e8469cb1d158956b8da73dc89f870e064deab48","datavalue":{"value":"W1520527482","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5210762$D8F637D9-B5AA-49B7-BC13-81D371C643D1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbb4aa8dad638334a86cbf0de6c1439e4250b0ce","datavalue":{"value":{"entity-type":"item","numeric-id":4692618,"id":"Q4692618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$7CB59000-DF4E-410A-963B-5A6907729BF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6821d8bf92570a1265d30079b71046c8a303a664","datavalue":{"value":{"entity-type":"item","numeric-id":3327746,"id":"Q3327746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$8BA84477-A262-4271-9D0B-F62624B709B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$910507D1-22C2-4152-A3C1-211EC48703F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bea75da9fa67a5f77faa9362cd4aa6c737c792a","datavalue":{"value":{"entity-type":"item","numeric-id":4194955,"id":"Q4194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$56D0CA29-F86C-4F43-A2DF-31D4ECA282C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$BA369991-1B49-4A3C-9ADC-104BCCAE6462","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91b17ca5304b07e27db69bbaad41f776f31427c7","datavalue":{"value":{"entity-type":"item","numeric-id":3997615,"id":"Q3997615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$B7816FE7-20A6-4B13-A843-0ED58C72FEEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2fa04d400281f100817ce7e13bdaafd2683670","datavalue":{"value":{"entity-type":"item","numeric-id":1071750,"id":"Q1071750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$6C7F7873-8561-4AAB-99E7-27F95E6C368B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bc614fe187bd0295ec729cf32cb3675e34b7b37","datavalue":{"value":{"entity-type":"item","numeric-id":4302847,"id":"Q4302847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$7CAFCF14-A33B-4FFD-A8EA-A2B3B402B275","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1f0b5c5d1ef7da893967c1b74defc4984f71dee","datavalue":{"value":{"entity-type":"item","numeric-id":1062761,"id":"Q1062761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$42D0AFF1-A75D-4996-98B2-B829ACF25339","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"606b55142cd4468a9a74e0ea3982d2b3991333cb","datavalue":{"value":{"entity-type":"item","numeric-id":3992908,"id":"Q3992908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$2C6D6643-A6DA-4F64-A2CD-BF6E1CA09DE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8586c92c4d90a06cb521bef03111f958a597fe2e","datavalue":{"value":{"entity-type":"item","numeric-id":5574714,"id":"Q5574714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$CB1C1809-0C27-4502-B801-DE6494C06B6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$2C1EFD81-AC7C-4CD8-B8BD-92C16195E766","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88fba5a1fdfac74b8e0dcefe0e56f5b10792486d","datavalue":{"value":{"entity-type":"item","numeric-id":688547,"id":"Q688547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$61169F7F-F92B-483D-9BEA-798AF88BA4AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0001ddf29143e230db9061e7c9cfd72aed8db985","datavalue":{"value":{"entity-type":"item","numeric-id":1170894,"id":"Q1170894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$BAC03163-5754-4872-B2B8-BB71568CBFE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d43919d1f4da3b9a07eea3d230b3f18d880d5940","datavalue":{"value":{"entity-type":"item","numeric-id":1116717,"id":"Q1116717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$1AE1769C-55C3-466D-86C0-B3F2AA2F922E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db1af0fa3ab79d3aca7d0c2eb038f3a2d86af567","datavalue":{"value":{"entity-type":"item","numeric-id":5541351,"id":"Q5541351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$C9FDF1FC-A084-4FED-B835-A60EE3040459","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f771f551f48b2f2d21f6f2011008cb21eb26e492","datavalue":{"value":{"entity-type":"item","numeric-id":5538933,"id":"Q5538933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$A219279B-ABFD-4DBF-8ECB-06FDC60C9DA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"017c184c3277fb681aa54b180b0d3db5f9e6933c","datavalue":{"value":{"entity-type":"item","numeric-id":3348885,"id":"Q3348885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$9D7E0449-8E96-4133-AD4A-A46A9CD076A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd379cd3bdf04144236b4ba7f69e8c77bec3c700","datavalue":{"value":{"entity-type":"item","numeric-id":4560350,"id":"Q4560350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$E02091A9-E708-4A04-A719-323B635D6784","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"728810277830424bd131e6e77eef399df584ccea","datavalue":{"value":{"entity-type":"item","numeric-id":3780485,"id":"Q3780485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$ABAB3516-F14C-4D1F-A573-C62DFBCA9592","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ef75b4b5ae4f1119c1ac9bfdcf91039dbf37c93","datavalue":{"value":{"entity-type":"item","numeric-id":3829089,"id":"Q3829089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$C2A532F2-9773-435A-B8AB-57ACCCAEA311","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47bab4f7d1b2661e9a9ca3ddc35e5a57311ad582","datavalue":{"value":{"entity-type":"item","numeric-id":5507985,"id":"Q5507985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$8AECD85F-9C87-46E5-87C9-CBED619963E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e963915702637e6f873c32169203d8b91d5f54c","datavalue":{"value":{"entity-type":"item","numeric-id":1217465,"id":"Q1217465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$E63A9B90-317A-4052-84CA-1E5DAB7C4394","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"24e4d5d206133d3398c50fe5451aaece0e817a40","datavalue":{"value":{"entity-type":"item","numeric-id":6488549,"id":"Q6488549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5210762$0A0D8ECD-CBC1-4779-9556-F443BD573F7B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c365ae4452123ae097251f5b3c1589e5b0b2b3dd","datavalue":{"value":{"entity-type":"item","numeric-id":4375764,"id":"Q4375764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c169c38edcdf836efb0914925c5e0b5cee4676a7","datavalue":{"value":{"amount":"+0.9229767322540284","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":"Q5210762$01CF18DA-7561-47AA-A53F-034F0E868E15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1977ce75e4c66a6e986ece8bd137815f9305537","datavalue":{"value":{"entity-type":"item","numeric-id":4345253,"id":"Q4345253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8f6ac436436a13b12d2ea0953315daaa8fcedbc5","datavalue":{"value":{"amount":"+0.8985784649848938","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":"Q5210762$2C14FD2E-DEE5-4D51-B3CB-0DB834EB3DFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9e6901df0d59a017c054fa969f1e65edc3a3eb1c","datavalue":{"value":{"entity-type":"item","numeric-id":688547,"id":"Q688547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8f6ac436436a13b12d2ea0953315daaa8fcedbc5","datavalue":{"value":{"amount":"+0.8985784649848938","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":"Q5210762$5D26AE79-76D1-47F0-9546-9D9D35D9ECC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb959f515fd7c7236525feea8dded276d4ea8598","datavalue":{"value":{"entity-type":"item","numeric-id":1281504,"id":"Q1281504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3514f0f6417839765d745cda3a283376cff4399a","datavalue":{"value":{"amount":"+0.8231169581413269","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":"Q5210762$F4127C3C-4982-4E65-8022-EAA6B86D74C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11f1c47359185fdc2628bfaf46602cd68016e4ee","datavalue":{"value":{"entity-type":"item","numeric-id":2456542,"id":"Q2456542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85d1f809c922ca1ffcc9bcb310bb89d68578d808","datavalue":{"value":{"amount":"+0.8171282410621643","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":"Q5210762$745AC458-7337-425F-93B3-85FD3CE683DB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5210762","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5210762"}}}}}