{"entities":{"Q2456542":{"pageid":2467285,"ns":120,"title":"Item:Q2456542","lastrevid":78701897,"modified":"2026-05-06T12:14:08Z","type":"item","id":"Q2456542","labels":{"en":{"language":"en","value":"Towards a unified model of search in theorem-proving: subgoal-reduction strategies"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5202014"}},"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":"Q2456542$10368BB8-E121-42D9-B2CC-64E57953386A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"51771ef054f0e18cb2ccf317cd2621fc99c4538b","datavalue":{"value":{"text":"Towards a unified model of search in theorem-proving: subgoal-reduction strategies","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2456542$A375D84F-7501-4151-B8F7-66316FF6E3C7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e81b59e7bb097d852dccd32ad4601193aefdff07","datavalue":{"value":"1126.68071","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2456542$26FE141E-9899-4959-A290-51C96998BBAD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b455290f5b835c3773a6eb2262897ac70e7a163b","datavalue":{"value":{"entity-type":"item","numeric-id":287273,"id":"Q287273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$5C1F6D9F-0130-4273-84F7-A7051A9B6578","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$5D251BEC-0A64-455A-B634-1489F9CE029E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8b5dd9e0f7e970fb181073844a7c8c2ebc2be921","datavalue":{"value":{"time":"+2007-10-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2456542$27094AC8-4EB5-491A-B84A-1522C1647DA9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2456542$DDE84512-C811-480F-BFDA-F84A6326516C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"02fb829824e9bbe309a545a4bca73485916f0bd3","datavalue":{"value":"5202014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2456542$B216F761-19F7-441A-82C3-D2C183F6A8DF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc0a06ffadbc917396a626e33a9a5489bfbfb917","datavalue":{"value":"automated theorem-proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2456542$803F485E-862F-4C03-9D03-176B6629DC58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3b18127eee2dd8296e45e0992306dfdc5dba741a","datavalue":{"value":"subgoal-reduction strategies","type":"string"},"datatype":"string"},"type":"statement","id":"Q2456542$798A2A62-FDAF-4C2A-A511-3A2186B26397","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2a887ad794ee3d51d4cac03a6e52ac80fc001b58","datavalue":{"value":"tableau-based strategies","type":"string"},"datatype":"string"},"type":"statement","id":"Q2456542$13F6FC84-AFF6-414F-B6FF-5C42B6FD2565","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36ce822d3ae04a15556acf2516173f10e16a01ad","datavalue":{"value":"strategy analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q2456542$AEA3EDD9-6C17-40D0-96F1-3C0C02702E15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1b680266e97fe9a73158022e37cf94aeceb6971e","datavalue":{"value":"search model","type":"string"},"datatype":"string"},"type":"statement","id":"Q2456542$BB52BB01-5375-4DB2-9FFD-A625D2A898C3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$27B72A78-573B-4092-B2B2-1BA307C57B76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c845b927c7c8299e3e10848fbe9373f51ae3559b","datavalue":{"value":{"entity-type":"item","numeric-id":13461,"id":"Q13461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$0E200C01-766F-4AD0-AA7C-02A89FA98DCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1eaabc0e561dc484a85bd72ad458c9fb5f2683d3","datavalue":{"value":{"entity-type":"item","numeric-id":15174,"id":"Q15174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$9ABB67EF-9A11-4F60-BCF4-12C82716D096","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7b91ac32942574114e615de5dd586d7306b3c5b6","datavalue":{"value":{"entity-type":"item","numeric-id":18709,"id":"Q18709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$4DA8B25E-C1F1-47DC-90D7-BA9E5618625E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5834864074172f90c0db592b61fbce75f9303a03","datavalue":{"value":{"entity-type":"item","numeric-id":16627,"id":"Q16627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$95B55D69-EC61-423B-B32A-A6C78D7D52A4","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":"Q2456542$22A7C672-769E-401B-9D0C-C1AACCAB4DF5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"41b8fca2730259e1902b722bd8dc76a40f1627b4","datavalue":{"value":"https://doi.org/10.1016/j.jsc.2004.11.001","type":"string"},"datatype":"url"},"type":"statement","id":"Q2456542$53378A62-A364-44F1-A650-F788E875FFFF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"edc424257af6c89e2f03cebeb1a3e19bb90f0143","datavalue":{"value":"W2132979526","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2456542$7C6E6BA8-52B3-4972-B27E-371EB6AF20D8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ed4e2b73edd0e2661ebb75822eda29ecb9eb63a","datavalue":{"value":{"entity-type":"item","numeric-id":3906484,"id":"Q3906484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$4E9FB0E0-4232-4588-BCB1-1D9BFF2FB2F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"103360585a9bffb1c1cc70bf60b5d74438ed3255","datavalue":{"value":{"entity-type":"item","numeric-id":1401930,"id":"Q1401930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$0C928445-FC9E-4813-8B84-40FBBB92D98B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58c3a9e4976685d7e1f5e42b0c7df8599a954d3c","datavalue":{"value":{"entity-type":"item","numeric-id":1367083,"id":"Q1367083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$B052166B-B617-4671-841D-4D7929D13418","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57f7fa6caa55b91028ff32d7dc4d210dfa455de8","datavalue":{"value":{"entity-type":"item","numeric-id":3838803,"id":"Q3838803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$7298E174-D608-4660-814C-F53D1BC6820E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d50f7c606a252a2bb504f7358999ab7b1ba3c57d","datavalue":{"value":{"entity-type":"item","numeric-id":1369080,"id":"Q1369080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$11CA8D98-4492-4220-8E60-E68048F65026","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e3a15edbbace0d07f7ac24c32c80a198d5e25a0","datavalue":{"value":{"entity-type":"item","numeric-id":4263168,"id":"Q4263168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$E9AE6761-190B-4CD5-B44E-99D777327A34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6259d6bc26c195111d912bf0a83b34c83a8105b0","datavalue":{"value":{"entity-type":"item","numeric-id":1322772,"id":"Q1322772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$3DF5E79B-8360-47E4-BCEB-A9AADD53086E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3f5430ecc848a50171080eba0177650e4c8ef9d","datavalue":{"value":{"entity-type":"item","numeric-id":4524784,"id":"Q4524784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$2EBEFE98-6D79-43B3-A91C-D1A5C72E1E0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b0b5570cb99f8777c021532085aa4af0816281a","datavalue":{"value":{"entity-type":"item","numeric-id":1404980,"id":"Q1404980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$8AA19883-914F-4391-B18C-20F7A92114AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82285947ecd1d65d80e17696025cdf5ddb799be6","datavalue":{"value":{"entity-type":"item","numeric-id":3922205,"id":"Q3922205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$A91EBBBB-8BF1-4ED3-BCDF-FCF53EDC72BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2aad2916b073577856c022bdffa0d3b878301ba","datavalue":{"value":{"entity-type":"item","numeric-id":4645231,"id":"Q4645231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$DC3D41BE-2961-4A8F-AD1A-F7F3DA41E8DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8d3b6375caf4d4ee88902cd25cc18b6e96451d1","datavalue":{"value":{"entity-type":"item","numeric-id":1978033,"id":"Q1978033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$B150FAB5-6DF3-4554-BF3F-4C4E7AFD2FE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2eaf1c8e5e649a3c59e663efd73652b24868feb","datavalue":{"value":{"entity-type":"item","numeric-id":4941840,"id":"Q4941840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$6808622B-7B27-4C40-860E-E69D31D36C32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d47d7f807ff440d37ec1151957e0741b3996e143","datavalue":{"value":{"entity-type":"item","numeric-id":5277771,"id":"Q5277771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$161FEF85-E1AA-4438-BDD4-55C8FEF804F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67be0822f2ea25493074f855c573aed35f47e829","datavalue":{"value":{"entity-type":"item","numeric-id":673134,"id":"Q673134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$D05AB9DF-C73D-4E7F-BB97-F17A23EAB52F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f64546dea5edcb439503d41ef37e4c3a53136602","datavalue":{"value":{"entity-type":"item","numeric-id":1281504,"id":"Q1281504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$92C01351-008F-42F2-9BD1-60E62EE9854C","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":"Q2456542$32F5FC2E-089B-4A03-9238-898834F4B314","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ff8a97b4b9412cf94d02fb85f3195ed2195f2be","datavalue":{"value":{"entity-type":"item","numeric-id":4447230,"id":"Q4447230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$8F592054-AB6D-4481-A4AB-FC9200D47555","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e47a0cdfbf49c2c2a42fab05844da554fa0d9630","datavalue":{"value":{"entity-type":"item","numeric-id":2721183,"id":"Q2721183"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$3A80BF30-BA7F-4EAC-B16D-EE9E63A5CE77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c1aa73dfe0d0c7090d64e64b87f9b4f3015ccdf6","datavalue":{"value":{"entity-type":"item","numeric-id":1589576,"id":"Q1589576"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$B39E63DC-05DC-40DC-AF08-8C1281228E55","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":"Q2456542$96629D33-1A65-4F5F-88AC-F9861263FCF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a37da6481d3393a5a430cfe31bbfd3e1bb865a00","datavalue":{"value":{"entity-type":"item","numeric-id":4380444,"id":"Q4380444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$06844837-EA13-4F40-93FC-15A8F868A8C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ebba25ec6e30e98195fd89fc28af9b9ec829611","datavalue":{"value":{"entity-type":"item","numeric-id":2751377,"id":"Q2751377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$71F2E656-900C-42E2-81E5-E9810D7F2A4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"315e95e4ad8a1c26487d3ff7728ab264483e45ea","datavalue":{"value":{"entity-type":"item","numeric-id":1310269,"id":"Q1310269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$FD2D2EE6-758E-4599-A706-1CAC0141A4B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a80969bb580420f8ecd201d1cbd7dbd33d4faa0","datavalue":{"value":{"entity-type":"item","numeric-id":4770008,"id":"Q4770008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$C342DB24-2C50-4517-BA85-984AC4AA2040","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e22ba87969e65ae8e3ab31f9554443a9bbb69d7c","datavalue":{"value":{"entity-type":"item","numeric-id":5927985,"id":"Q5927985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$D53C4D45-6A19-4FC3-B191-1C25A073418F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f33c7e2fc71303fd900c50bc37fd6728d3f12f3","datavalue":{"value":{"entity-type":"item","numeric-id":4539640,"id":"Q4539640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$014C543C-D564-4DF9-9718-472CAA6FD228","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17e9e44d7ffa3e35b73497e32253991279784e6a","datavalue":{"value":{"entity-type":"item","numeric-id":2751354,"id":"Q2751354"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$8130B86D-55E6-4A70-923F-976851FF49AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d47137c7bb75820cd97b048bcb493883638963b4","datavalue":{"value":{"entity-type":"item","numeric-id":2751547,"id":"Q2751547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$F42CA3DE-70B7-49FD-99AD-CE89B4AC46D9","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":"Q2456542$0CC6BDAC-4FF5-4F42-B5DF-11174C69D772","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22d3f29968c996bb68da1f8ea593f2a057ca04cb","datavalue":{"value":{"entity-type":"item","numeric-id":5623241,"id":"Q5623241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$449733F9-6029-4A16-AE4D-03707CC38ABF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dbf5d4c6cedd5848e03816494729378cde53a8e","datavalue":{"value":{"entity-type":"item","numeric-id":2551698,"id":"Q2551698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$B5C054EC-D6A3-45CC-A5CA-C6B5BE789BA2","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":"Q2456542$6F86D9C8-18D2-4CA1-9042-C92D1BFD1736","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8755fff25bcbf365d5dd2dfde2f78f833a2371b","datavalue":{"value":{"entity-type":"item","numeric-id":4331764,"id":"Q4331764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$BF5DD1E3-58C8-466E-8A34-A71C45D15517","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e877970458b5c16302ee283d5bedf9c4963fdd7f","datavalue":{"value":{"entity-type":"item","numeric-id":4524783,"id":"Q4524783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$4FA92E8E-834E-4FE5-AB43-A790E3B2EBC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"158bb2233935470152d2dc667c5dec4b7a43c81a","datavalue":{"value":{"entity-type":"item","numeric-id":1344875,"id":"Q1344875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$FD3B7C11-0B20-4DDD-AD28-A65D6F650978","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07bde1b1ec996aeb071ba3c817fedaeed25122f5","datavalue":{"value":{"entity-type":"item","numeric-id":1189726,"id":"Q1189726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$78575EF4-4FBB-4E21-A949-258A02E48FB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21fbc83071ad5f20d8b4483227b1c409325b374f","datavalue":{"value":{"entity-type":"item","numeric-id":4539623,"id":"Q4539623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$86E5A257-8E64-451A-81BB-57687A883619","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd41301b78a03236dc27ccdfce83b246065d0cdc","datavalue":{"value":{"entity-type":"item","numeric-id":2751380,"id":"Q2751380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$582353F2-3D1E-41B0-8A50-AE713D68BCE0","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":"Q2456542$79103620-4038-40B0-BD0F-410FE14B1011","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"639ca075c3c5996188ecb0577ad81a4f9c56d3a2","datavalue":{"value":{"entity-type":"item","numeric-id":5655006,"id":"Q5655006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$D5814263-744D-495A-B28C-005379B04E6B","rank":"normal"},{"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":"Q2456542$D390C1B5-7761-4C43-BC6E-4C5C808B44FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0e6b99241bd5405a7d704114ed85dbdcd125acd","datavalue":{"value":{"entity-type":"item","numeric-id":2639044,"id":"Q2639044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$41BC9698-BE25-4DAA-A71E-82C5E817995F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc3878f9df5b6107a28c21f85873329086200c14","datavalue":{"value":{"entity-type":"item","numeric-id":4345253,"id":"Q4345253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$F254A581-3F4A-4C90-885B-EDC476BF2D4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f00589542fdb6ec4fc401e47318165d5bad4f817","datavalue":{"value":{"entity-type":"item","numeric-id":1581853,"id":"Q1581853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$BB57543F-C033-4DF2-8C69-3C5DAD671AF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5bd4f24e8eb1a084ca4ac4963d45f487b7e5bb4","datavalue":{"value":{"entity-type":"item","numeric-id":1226867,"id":"Q1226867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$B7877D62-1F1D-4D8C-970D-4EF6CEE5281A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febba330446bda559f2952d624c63d67c91597ef","datavalue":{"value":{"entity-type":"item","numeric-id":5560258,"id":"Q5560258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$23D31C77-3953-4BE2-A3F5-32EE9E006FF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9808046a6f8fa62d1a453b12f211b7893e78bc6","datavalue":{"value":{"entity-type":"item","numeric-id":1199932,"id":"Q1199932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$40D9CFA5-66FA-4F73-AC84-953BA5948D99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"444a343bef962528ebcdff413e879ec868b1e36f","datavalue":{"value":{"entity-type":"item","numeric-id":4520770,"id":"Q4520770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$63E2B4EC-6435-4618-A27E-4AB36510E6CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"760df30ca41971176d129aff49dfb79a744d4ceb","datavalue":{"value":{"entity-type":"item","numeric-id":4860660,"id":"Q4860660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$EF15B1CB-FAC9-44D6-9569-C1516923AD1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ad5589e53c0d66e13265564721ea82e85f30cc3","datavalue":{"value":{"entity-type":"item","numeric-id":4318862,"id":"Q4318862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$16BD5200-B425-4C02-89B4-FE270AE0E783","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5aeafb9ac2f2609d33e0e02fb8c95752a23334d9","datavalue":{"value":{"entity-type":"item","numeric-id":2365127,"id":"Q2365127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2456542$530D68E4-7DD7-4463-8714-83AC7584CDC4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"72ccff1ed25bd6553482bbba8b3a11311bda09b7","datavalue":{"value":"10.1016/J.JSC.2004.11.001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2456542$C3EF0052-61E0-41F6-A083-E4975C4E8C1F","rank":"normal"}],"P1643":[{"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":"5d3b84a2235b840e6f896a41c1b1c1ef1facc853","datavalue":{"value":{"amount":"+0.8369700312614441","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":"Q2456542$BFB68F61-B3A5-4926-AA12-3F190CD3AA75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0de3569d2e6f3b3616c98dcaea44ecb60d53f09a","datavalue":{"value":{"entity-type":"item","numeric-id":1369080,"id":"Q1369080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"889ea7f68eed82025c6612c50f703f9ab377be88","datavalue":{"value":{"amount":"+0.8273248672485352","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":"Q2456542$642E43B3-874F-4ED1-93D5-6EC7E7FF9206","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c93ae142d165f90d61d468b1b58b365ef92147b","datavalue":{"value":{"entity-type":"item","numeric-id":1978033,"id":"Q1978033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b1feadb89182a988b7bdc1259a1727a1c9465af","datavalue":{"value":{"amount":"+0.8271915912628174","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":"Q2456542$FE666ADD-5FEE-4D69-849A-3F4895EB46E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3328acb14c381645dbb1f9eb31b744a4a34bbbc0","datavalue":{"value":{"entity-type":"item","numeric-id":5210762,"id":"Q5210762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d179774c17a32c4100712f102edd650c0cac9e3","datavalue":{"value":{"amount":"+0.8018497228622437","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":"Q2456542$FDD7AD96-F84A-4D54-8014-C90776748616","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":"a8aeec4d37f65be9274e885f57390aba18c685ec","datavalue":{"value":{"amount":"+0.7865636348724365","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":"Q2456542$706776EB-38B8-4772-8702-883507C1667E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Towards a unified model of search in theorem-proving: subgoal-reduction strategies","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Towards_a_unified_model_of_search_in_theorem-proving:_subgoal-reduction_strategies"}}}}}