{"entities":{"Q331617":{"pageid":333384,"ns":120,"title":"Item:Q331617","lastrevid":61109772,"modified":"2026-04-10T21:14:36Z","type":"item","id":"Q331617","labels":{"en":{"language":"en","value":"A learning-based fact selector for Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6644465"}},"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":"Q331617$6EC37951-3A03-482A-BB5D-2D11F0A5E0C5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5d2b6937c2b8833a8284b3b0ec28b3ff1b0aa468","datavalue":{"value":{"text":"A learning-based fact selector for Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q331617$21C2BD4C-8019-41B4-AFE2-39391C900324","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e97a089a9f20649bb333dfb4b59b90c63d4cce08","datavalue":{"value":"1386.68149","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q331617$67E62C77-25BA-4BD7-85EC-83C90B2AC0F2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"42c29c686dffd678d9f155b05a4a1aa93e85953c","datavalue":{"value":{"entity-type":"item","numeric-id":287335,"id":"Q287335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$9891EFCB-4C58-46B9-9C67-E15DC8B06896","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"54053fba3e8a52ba38500db64ccaef0197e5c7ca","datavalue":{"value":{"entity-type":"item","numeric-id":331616,"id":"Q331616"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$FB0583D5-8A7B-4139-B16F-AC8E14C03DDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ad6a046b48bbe4ab777309f1d5c19b5fc7dfbda","datavalue":{"value":{"entity-type":"item","numeric-id":286799,"id":"Q286799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$BB5742FA-DB9D-4A04-B8BA-CD75315A2F15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"10ac899857b53db65920b63129111456d82cf0ed","datavalue":{"value":{"entity-type":"item","numeric-id":286785,"id":"Q286785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$C4E8AA83-1794-436A-98A0-EC4136790BA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$C86E2FCC-73FD-45AC-B923-8EF129190147","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":"Q331617$BD9E1FB0-2D55-41F0-BAC4-D22DFCD77E0E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3adf6ceedb6d880e3aaf819e51e828456bb3558d","datavalue":{"value":{"time":"+2016-10-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q331617$3106079F-E998-44AF-BEFF-505CD9457C9E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8736473389963e6f7c7b3955696a05578b659cee","datavalue":{"value":"https://zenodo.org/record/1227195","type":"string"},"datatype":"url"},"type":"statement","id":"Q331617$95FEC7A0-F054-4568-B537-B95847B17554","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q331617$564EBA84-C0D7-4B7D-9749-F9FF39F8745B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cfe779e91fe9c53ee133568259955801965765ae","datavalue":{"value":"68T05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q331617$CED80C13-F3AB-44AA-A81C-47A1E703B96C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b919a7cc29dc6122b76b7ba7c5274cc28c4abb3f","datavalue":{"value":"6644465","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q331617$0C1FF306-27EA-43F9-8894-9F7B6ECFC765","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b21c1d8177ce0f6461c3bbe4e8df47538468468d","datavalue":{"value":"relevance filtering","type":"string"},"datatype":"string"},"type":"statement","id":"Q331617$5D7D607B-71D7-42C8-9B77-8A284F919C9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0afe30fcd4cd25e8e8273c02ad48a97b4a0e001","datavalue":{"value":"machine learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q331617$46A1E43E-6A26-48DC-AB77-26A2C136F254","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q331617$6D9E1ACF-6D92-4F08-972F-157825F94EC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1735a133d49ec9a3b5c084ee424340f472bf4d74","datavalue":{"value":"automatic theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q331617$EFBE8989-70F8-483E-B061-41CC53F315FA","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"607a8a6060a7bf2ca22bac44d5b54c91824aa13d","datavalue":{"value":"Q108482139","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q331617$BD2E04CF-D68F-4051-B24A-C314B6C24AF7","rank":"normal"}],"P1463":[{"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":"Q331617$8C1E68F6-979D-4F1D-A3EE-6B799DB5720C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$B66F8185-03BD-4529-A741-B5F48470C945","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":"Q331617$FF247642-FBE8-4323-8421-D94DC15764DC","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":"Q331617$923BC9D3-FB3E-4ED1-AD46-6B9E8463218A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$D9B19F03-0A5E-4894-9391-7B45C42C9DDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$D3EED954-D26C-4CA0-BF8A-DF140CE1C5B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"23f1d4970d4f2ba01b8146500b5c1a10ed17d235","datavalue":{"value":{"entity-type":"item","numeric-id":23493,"id":"Q23493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$CF5720E4-6087-4457-BE12-4AD0BB50B577","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d40b61763c81cd80c5c82e03c39b2fdb5cbb80a2","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$A0850D78-6EFA-4B57-8BEF-98BD5B14F559","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$A26BA848-91B6-4055-8CE2-B7256D376133","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"30c23680895c6c05b43b4be92074136c496750ec","datavalue":{"value":{"entity-type":"item","numeric-id":28682,"id":"Q28682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$2F5FCAC2-9111-48A0-AFA3-54FF97A16F90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"90c7c18880caa813a6bdace0f373d3dec3147690","datavalue":{"value":{"entity-type":"item","numeric-id":40350,"id":"Q40350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$B14672EF-19E1-4D24-BF94-EF6535A96DC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"484f589bd857c6ecd5604196ba88033adb11a795","datavalue":{"value":{"entity-type":"item","numeric-id":15128,"id":"Q15128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$07FEF241-5885-48F1-B237-93B66E6A3035","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":"Q331617$FE3B9C56-2AB1-4FD1-929D-3CD6A4B494B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7cccd35b34888307d4ad7b137783609eb5c56b79","datavalue":{"value":{"entity-type":"item","numeric-id":16825,"id":"Q16825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$BFB1DC8D-D265-47D0-95B8-4075C655AC10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8e7deacad56e3bf59f522de6c1fa96858f2fd494","datavalue":{"value":{"entity-type":"item","numeric-id":18676,"id":"Q18676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$F5F12B74-98A4-4849-940E-5F55C6BAE24A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5df14ee9c6f65085bdee53a419634b2235aa5c43","datavalue":{"value":{"entity-type":"item","numeric-id":19326,"id":"Q19326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$536E4BD0-70A8-4A21-94B0-8154CDD8E3C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4725be8fa705861afbab12b59e447099c9ebb4e","datavalue":{"value":{"entity-type":"item","numeric-id":20216,"id":"Q20216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$C3DBF9EE-5F93-4369-8F7C-D32971F13964","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$7BF80558-8EF3-4FC5-8ABD-DE89BCE983CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$3CE16A80-D525-46DB-8E7E-C560A01CB7D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa59c17593526f154af9ca65ff557f73aaa41e7c","datavalue":{"value":{"entity-type":"item","numeric-id":40590,"id":"Q40590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$EFD4F6B4-101B-4285-8BE0-F35AB6F2EC40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$5AF8CECA-D797-4577-AD24-0B588AF1557E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$795A54CD-8240-4859-A570-7812E0A698F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"66eb045e037081b6f6e8499f9fef44d8fbb7e0b0","datavalue":{"value":{"entity-type":"item","numeric-id":22240,"id":"Q22240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$179824ED-3E64-4BF7-B8EB-C8599C22EC0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62af2c5e450adf37bd9acb47c5a55b60b68447ea","datavalue":{"value":{"entity-type":"item","numeric-id":22241,"id":"Q22241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$AAD658BE-4F8B-4C0B-BAEB-6E8CC6A0BE3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"31d2ddeef485fccfd3a5fe32ea329d2b65b4f1b4","datavalue":{"value":{"entity-type":"item","numeric-id":35396,"id":"Q35396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$4BEA228F-851A-480C-A544-874628B7ED9C","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":"Q331617$CD7994B3-5C41-4AAD-9900-419BE8C88A68","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ea6c2fffe49efb07548aaa7e82ea04a17a0d3ccc","datavalue":{"value":"W2310495003","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q331617$AA0B2C3D-A763-44F7-A644-4AF52E4E27F8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$5A589475-7045-44F8-863B-758EC7A4FBB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b52a45de8c1208b3a6a3b50a53088ff43e0469f7","datavalue":{"value":{"entity-type":"item","numeric-id":5326348,"id":"Q5326348"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$122FA5A9-BD86-4633-B03F-E32B9EDA6571","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f6a505c48f7ed8fbc36053c87307f799e1a7f54","datavalue":{"value":{"entity-type":"item","numeric-id":2351158,"id":"Q2351158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$9A84E5C3-B82C-49C3-925B-4A75D6F190E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b19149185e72c842c12321303888117be6b4dec","datavalue":{"value":{"entity-type":"item","numeric-id":2914754,"id":"Q2914754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$B5CB3B67-F073-47A4-B72A-1C85C082C834","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa6750f3149d248c4e232f6fdbdc36d7bc86e39","datavalue":{"value":{"entity-type":"item","numeric-id":2920991,"id":"Q2920991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$323637D8-B83A-413D-B3F3-E1C0C6D6AB1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"741b1c2a1697c669d1b3bbdff87dd79f9f007366","datavalue":{"value":{"entity-type":"item","numeric-id":1006731,"id":"Q1006731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$02B9FB84-34A1-41BA-9801-2DEB1321EE7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"604f23db2dd4d34a2f60254ad57a8915830982b5","datavalue":{"value":{"entity-type":"item","numeric-id":5200114,"id":"Q5200114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$F289E567-7CDA-4AB4-AEC1-7A044A2377AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb1bab11b75e766c233c3a1b9a3682b90b0e288d","datavalue":{"value":{"entity-type":"item","numeric-id":3075247,"id":"Q3075247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$2B45B8C1-E9DB-412E-BEC2-8ACEB6D57D10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbf7b4ce3ab96d4236a4c36e2f89589530011a89","datavalue":{"value":{"entity-type":"item","numeric-id":877826,"id":"Q877826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$02A2BEAA-E9D8-44C0-BA04-C7851716E4C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"065f96a47cd2c09ae1ea2ab42886a32d0c8223cd","datavalue":{"value":{"entity-type":"item","numeric-id":2891438,"id":"Q2891438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$4F1ECFA1-5CAA-404D-8ABC-2EA0E55EBC13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9655c068a195af6d54bbb62184581b058670a2b2","datavalue":{"value":{"entity-type":"item","numeric-id":3541722,"id":"Q3541722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$F0E7BEC4-8FDF-4D4A-B97E-124C221336C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29b0802dd9ffb89108bee25aa26120dffc46ad60","datavalue":{"value":{"entity-type":"item","numeric-id":2352489,"id":"Q2352489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$11EA2510-F900-4E8C-8545-5684B44F7F0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e14549321cbae3c57ae9ce6a9266b4af3d64fd4f","datavalue":{"value":{"entity-type":"item","numeric-id":286800,"id":"Q286800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$0B7040AA-F840-4C6F-AB5C-11873D5A94BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15c58f40f8893ea08e9b168dd3629a56d2e8291d","datavalue":{"value":{"entity-type":"item","numeric-id":2908509,"id":"Q2908509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$77FD3FA9-7999-4DBF-91DF-843A9C499C80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"483d3c17c09c578723154da4261b70aeda673d47","datavalue":{"value":{"entity-type":"item","numeric-id":2351415,"id":"Q2351415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$44B9E871-ABC0-4A94-A145-AFCC98845829","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e5ef200ca0a6ffd921de7b0fd780ff05ef7a989","datavalue":{"value":{"entity-type":"item","numeric-id":5327335,"id":"Q5327335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$DADB4347-F970-4748-8A4E-A3DCCF205F56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f44b125cf3594b01960f6a5396e298346e4cfbbd","datavalue":{"value":{"entity-type":"item","numeric-id":2870167,"id":"Q2870167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$FB4B1DD3-E693-4A28-9ACE-466AEEF79E2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"961e583e188fc7cff1699f17f5a1576a96a31fd3","datavalue":{"value":{"entity-type":"item","numeric-id":287340,"id":"Q287340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$8030AA19-7852-4231-8EA4-3428DF244774","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"716d170b6d9b095492bf0c2b742ee0dbade5bbe0","datavalue":{"value":{"entity-type":"item","numeric-id":3523178,"id":"Q3523178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$39004891-1F64-406B-BDD6-17A8B7E1D47B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12e4cb046e7e6d1eac10022f3d396c57882b72a6","datavalue":{"value":{"entity-type":"item","numeric-id":2754030,"id":"Q2754030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$FED1040D-7192-4900-8041-6357EB53DBD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c50bf30b5dabdf4dda50dde9e43de872f1c8761","datavalue":{"value":{"entity-type":"item","numeric-id":5200032,"id":"Q5200032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$C0F640D8-428E-4942-9929-8E9A50B21858","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0aef60bd392ccfb5e82daa98f095917b33d1745","datavalue":{"value":{"entity-type":"item","numeric-id":3183545,"id":"Q3183545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$BC0EA9D4-5828-49BE-A03D-C5E8A43623DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20d4a2aad4cebbcfa646c9c5d2e3fb1738d09daf","datavalue":{"value":{"entity-type":"item","numeric-id":5891628,"id":"Q5891628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$F09BC337-212F-4C17-9BF2-4E02F72A7209","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34dd873a66486e9e38fc156a4b8aa6ba19960bb7","datavalue":{"value":{"entity-type":"item","numeric-id":3088003,"id":"Q3088003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$9B4C41B2-F9A2-4878-BD89-E0DD64687FB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c39b9040e3d2807bc13175b6074f0175a0a4a1c","datavalue":{"value":{"entity-type":"item","numeric-id":5747754,"id":"Q5747754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$48DAF560-63ED-44D4-8B58-C5C7B7DE224F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb6a694c413940271a785e87645155d12c05123","datavalue":{"value":{"entity-type":"item","numeric-id":2914735,"id":"Q2914735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$FF3EAE2C-3CEC-4362-884F-4B49402AB027","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93c550078709a24810b3ec6e1d82a47c85cb06a5","datavalue":{"value":{"entity-type":"item","numeric-id":2018657,"id":"Q2018657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$FA37CDE4-6B5C-4639-8AD5-7C403FB0638D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed473c6e01919b49d2a3d56d48fd6fe4dac1c845","datavalue":{"value":{"entity-type":"item","numeric-id":1945905,"id":"Q1945905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$197C7FE4-1385-4AA9-84A6-6590B717EFB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c5239edfd305efbd1c9a075b6bf62b0b4959a45","datavalue":{"value":{"entity-type":"item","numeric-id":2870142,"id":"Q2870142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$69192576-FD89-4FD1-A763-22EA5BDA78C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ca970164517030c1d68d21b85053761baf38cfb","datavalue":{"value":{"entity-type":"item","numeric-id":4913871,"id":"Q4913871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q331617$C8F9068E-4223-437A-B12F-A9424AEC89C0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"799f8938cd133dea9bba8660f221677ece6dc740","datavalue":{"value":"10.1007/S10817-016-9362-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q331617$CFF294FA-B9A6-4C00-8933-06FC145B4413","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d3472b195953f2a339aa5fcdef649bc9eac6cc9","datavalue":{"value":{"entity-type":"item","numeric-id":5327335,"id":"Q5327335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"495a1d27ea41b40b1bce929baaed018399157bf3","datavalue":{"value":{"amount":"+0.9237741827964784","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":"Q331617$912E22DC-5660-4390-8FA4-1457684C731D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80a02b86f5e7c12a000ea62837c3061ae5ebea26","datavalue":{"value":{"entity-type":"item","numeric-id":4645730,"id":"Q4645730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c7cdc9cbce3cb2b0e7ff7acec5d1dd6873b2ed69","datavalue":{"value":{"amount":"+0.7623499631881714","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":"Q331617$9433A987-A9EE-48C0-AF4B-A38F11162F56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"825181a4e60dddb2c120a0a9288fdf3e7ea44101","datavalue":{"value":{"entity-type":"item","numeric-id":5747754,"id":"Q5747754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"341eaad399d0515aa9210904349efb3847512afb","datavalue":{"value":{"amount":"+0.760026752948761","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":"Q331617$5E45280B-52B2-40E8-8AD8-13842F96E746","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eab127e20c4e479e5e30e398294a19c06fe4cca4","datavalue":{"value":{"entity-type":"item","numeric-id":2351414,"id":"Q2351414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a961a8220a55ea30503c751841c08266a671caa3","datavalue":{"value":{"amount":"+0.7544125318527222","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":"Q331617$5369F6B6-0014-4F87-8190-9448F0DA9AE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e17ad5cefe2934a9da315d890618323f9b182ae","datavalue":{"value":{"entity-type":"item","numeric-id":4982446,"id":"Q4982446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31c157c2b0234280c12d626e70028c918a195724","datavalue":{"value":{"amount":"+0.7518661618232727","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":"Q331617$AC9EDEC9-91B5-4AB6-A3E8-FE23F8F98BA8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A learning-based fact selector for Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_learning-based_fact_selector_for_Isabelle/HOL"}}}}}