{"entities":{"Q485842":{"pageid":487609,"ns":120,"title":"Item:Q485842","lastrevid":62256843,"modified":"2026-04-11T04:51:15Z","type":"item","id":"Q485842","labels":{"en":{"language":"en","value":"Learning-assisted theorem proving with millions of lemmas"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6386142"}},"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":"Q485842$1C61A937-E955-4E8C-8585-F1D7600D3782","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3177daaa385ad7cca62822e9905615ea9c6fba11","datavalue":{"value":{"text":"Learning-assisted theorem proving with millions of lemmas","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q485842$3896E379-976A-400C-B503-7306EE464A88","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f995414ac44bf3210b7e9d2cb97eaf29a211cfa3","datavalue":{"value":"1315.68220","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485842$1985F429-DB2B-4145-A61C-A9CFFCCCAF3C","rank":"normal"}],"P16":[{"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":"Q485842$9551D702-5988-4621-84C4-6BC41986BE16","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":"Q485842$72275AFD-72F3-4693-B86A-7334997BBD20","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":"Q485842$9118214A-A2D1-4CC5-96A7-7A88BD9B27DE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"263261338df616964a138c38a6f0c5b7f36f1f12","datavalue":{"value":{"time":"+2015-01-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q485842$6691B3D1-6C47-48D6-AC2C-BDBF821BE717","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7746aeb774ee13461f6999bf40f66f52d02d2f8e","datavalue":{"value":"https://arxiv.org/abs/1402.3578","type":"string"},"datatype":"url"},"type":"statement","id":"Q485842$94965204-54E4-4DA3-8236-1E297FC9687E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485842$BE2C1715-C5FE-4B1D-902B-561B8E1D9F48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cfe779e91fe9c53ee133568259955801965765ae","datavalue":{"value":"68T05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485842$77615C11-1867-4FD2-9157-9D3CA99420A4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ad0869faeb5ac1929c04ac2c14f762c29a15c739","datavalue":{"value":"6386142","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485842$7E0E0B3C-4F3E-4EA2-9441-342B8F7889F6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"be3b32e66489b16e0a48a6159f1019ebed5d7a93","datavalue":{"value":"Flyspeck","type":"string"},"datatype":"string"},"type":"statement","id":"Q485842$A0585301-A99C-487C-B3C0-C1822E036802","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1d0d2085ef9190f858499d68e4cdda45a778199e","datavalue":{"value":"lemma mining","type":"string"},"datatype":"string"},"type":"statement","id":"Q485842$FE67F06F-7381-48D7-B3E7-3368BF384F8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0afe30fcd4cd25e8e8273c02ad48a97b4a0e001","datavalue":{"value":"machine learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q485842$B33E37E8-6DEE-4B69-96CA-6A8EDA1F0140","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8c823b56192bce445b4b9ec3d99d959d2bc7a655","datavalue":{"value":"artificial intelligence","type":"string"},"datatype":"string"},"type":"statement","id":"Q485842$1C728A42-076D-414A-9FE7-8BD00FF29D18","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$FAE2729B-10DC-4EA0-B685-4194DFF71D9C","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":"Q485842$BA881EEA-0367-40B9-A04E-E75612C7C7A8","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":"Q485842$C8FF2F56-AA19-422C-BCD6-83AC55A9DA3D","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":"Q485842$D08E9F33-FB16-4B31-97DB-EE819239E695","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":"Q485842$4F7AF90C-C09B-4BCE-B826-59D445C24729","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8376bcc90e7c7f009563b97a4560743162f2cada","datavalue":{"value":{"entity-type":"item","numeric-id":22158,"id":"Q22158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$9784D9C3-8C35-4401-BB06-CEE0E49DE0AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c7cbb37e14a01458626c5623c37a9141435c8062","datavalue":{"value":{"entity-type":"item","numeric-id":19250,"id":"Q19250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$FE4CA522-4C17-4364-B50F-F026FDFA31EF","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":"Q485842$728D0629-0E89-4279-B9ED-381AD3BC1F9C","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":"Q485842$08BC8F1E-66D9-4DE3-A6A0-534F23E3530C","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":"Q485842$9B2DDAAD-683E-405E-9BD5-DFF4D74558E4","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":"Q485842$759C17AF-8C46-4322-B3BB-532900D3676F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"effe99d4b547ffcbc07915d8ced5dc197768f166","datavalue":{"value":{"entity-type":"item","numeric-id":15028,"id":"Q15028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$B3686818-F152-49A8-B51D-95B1273E894A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"82659ddd3b24a7f3c51a78eb5f25cc1e5d64df69","datavalue":{"value":{"entity-type":"item","numeric-id":17116,"id":"Q17116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$0D23DC1E-706E-4DB3-9DFA-092A75FAF2DE","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":"Q485842$F06683FC-F16A-4BE6-9ED4-FFBB00BC9531","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2207b0b201a95a431b254bcb1c01d869b9f41774","datavalue":{"value":{"entity-type":"item","numeric-id":18972,"id":"Q18972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$228210E9-0D3F-4D42-9B42-DD565E6C7F4F","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":"Q485842$FE2A2BD3-3905-4B9B-99BF-5C21D63883FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4db67863b5fec3bef62722f41df2cb373dae295e","datavalue":{"value":{"entity-type":"item","numeric-id":27083,"id":"Q27083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$1569BF1B-CBC2-4CF1-8A51-86D909BA6518","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":"Q485842$5E8B384A-2737-4CE2-AC1B-00810BC54D84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"12995736fe82d65918938fdd42b1d647f84d490b","datavalue":{"value":{"entity-type":"item","numeric-id":33178,"id":"Q33178"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$85111721-0A17-426B-A7CE-A38FC4A2F475","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":"Q485842$34D36A9E-4123-4DCD-AB43-0BE8CD321AFD","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"044c4900a85f25660e8917022d829edeae43bcdf","datavalue":{"value":"Q35829526","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485842$86F9660F-EFCE-4DAE-B6D6-5CBF0B8A175B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ccbf08db4b21e54ed23af6eea84dad390786670b","datavalue":{"value":"W2127812195","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485842$C8165860-A1A7-4125-8531-9CDEC1F1C686","rank":"normal"}],"P223":[{"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":"Q485842$5BF46CDE-396E-4FEB-B5FC-CAE9431E774C","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":"Q485842$FA46B1FD-A26E-4F9F-9CAE-850227C1234F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3fea6dff3d36407dad60fa8e8c9bcc1f06ec22da","datavalue":{"value":{"entity-type":"item","numeric-id":5200019,"id":"Q5200019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$45984456-5AFF-4490-99A7-0EE46B8B3F98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05077010557fe0fc2bead50a48aa3376695c3133","datavalue":{"value":{"entity-type":"item","numeric-id":2365126,"id":"Q2365126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$D1C3B1E4-602C-450B-A1D6-C27CA77166BB","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":"Q485842$D622B4F7-EA05-4405-BED7-20085F78A9AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"014df434e19c98aa84979531cf42f2d47588711c","datavalue":{"value":{"entity-type":"item","numeric-id":4647531,"id":"Q4647531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$53207772-6786-4576-B4A4-45029BDBB301","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":"Q485842$4E74A313-85F5-4496-B651-1771A2E2E160","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb771eb1dd5ac3a4e83b6105ce84dd2191d8e367","datavalue":{"value":{"entity-type":"item","numeric-id":5327336,"id":"Q5327336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$2081EDB6-344A-4451-BA45-2E79D454397D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e3fc60b7f0fb76cc0f065f148162a373198b73a","datavalue":{"value":{"entity-type":"item","numeric-id":2843009,"id":"Q2843009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$2B3C4768-F100-4ACF-BD55-4CB7086F0D05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3aa637d12e7774743d5229e303a10e1589a2a43","datavalue":{"value":{"entity-type":"item","numeric-id":2870150,"id":"Q2870150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$79669A98-B446-4F8D-B665-B785B9EF5769","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":"Q485842$5424AC33-282F-4AEB-BA29-738ACB91B744","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6af1483960b5acdfcc7fab2e7274bf3ab4268fd","datavalue":{"value":{"entity-type":"item","numeric-id":4928443,"id":"Q4928443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$EAD3BDB9-2A75-41D6-B99F-17641A9FA5F3","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":"Q485842$4647C766-B823-486B-A8B9-18DB821978ED","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":"Q485842$0B3EB6A4-1846-43FE-911B-C1C8D48598B9","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":"Q485842$1575A390-62D4-431C-9D81-40F81187DB36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a72cc7e7b9cacb2df1c9f3d9a1db5cf48ca2da9","datavalue":{"value":{"entity-type":"item","numeric-id":4928455,"id":"Q4928455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$055B30C5-E0EC-4E7B-90E5-C7012DDFAB64","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":"Q485842$9BAA4EE4-72C8-4948-9C65-7F6D5B325CDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f38c339bbd571c9f13a1b3052c0abde7b640b4a","datavalue":{"value":{"entity-type":"item","numeric-id":2471742,"id":"Q2471742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$E7E10771-2D27-4EB7-A10A-8FE23EFCC434","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":"Q485842$26887145-91CD-4049-8E25-C5CE0C9A0136","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"736fa966f95bcbb7d184601f6d7f8bf14e31e981","datavalue":{"value":{"entity-type":"item","numeric-id":2739546,"id":"Q2739546"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$2C1071CE-18E8-46A1-97A4-783922BFAABF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93fc8985b7898988b7d52edb5c0cd61c1b917df6","datavalue":{"value":{"entity-type":"item","numeric-id":3150301,"id":"Q3150301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$3EC22F65-398B-4A78-B86D-C6A9CDB96F73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81eb1bed6fe619f48a29f5aee3e7db00567c1586","datavalue":{"value":{"entity-type":"item","numeric-id":3608780,"id":"Q3608780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$45A9B1E0-39DD-42A7-9B6F-FD18C467023E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6dbaa83286082fe9f22efc1424c5503085916666","datavalue":{"value":{"entity-type":"item","numeric-id":556682,"id":"Q556682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$BD92F66F-9409-4893-ABE7-49D28B2979AF","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":"Q485842$1B900314-D51F-4FB4-AEA4-601A9BC11AC0","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":"Q485842$AE9F0DED-EB1A-4B2B-977B-EED8B625B0A6","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":"Q485842$56BD0373-2E06-4F55-85F0-2836AE7DF133","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5195f079b24d72ee2311e1fa679a5be0342958f5","datavalue":{"value":{"entity-type":"item","numeric-id":3010374,"id":"Q3010374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$1248B956-14CD-4FBC-B6A4-997B64F98793","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3087f1a7eb9309c1646d3032c16c6ac9f3d28d8c","datavalue":{"value":{"entity-type":"item","numeric-id":1923820,"id":"Q1923820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$81D444D2-35CF-4CE1-AB7E-4A21EFCC1B26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81087b834bd0f0342fd52d99726619dd5c97caec","datavalue":{"value":{"entity-type":"item","numeric-id":3543647,"id":"Q3543647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$F95A165A-000B-4EA1-A908-6AECABD3E1FF","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":"Q485842$00DAD023-96AD-4289-ACC2-81A1171C5801","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"41c95bf8af1ff758483d6e0594b5ae2c817fd2f4","datavalue":{"value":"10.1016/J.JSC.2014.09.032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485842$8A19B1AB-0D4D-4238-93FE-2FE01370637B","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"fcc8e8fd193ee25f4aa60ba096c41c339c5c2daf","datavalue":{"value":"journals/jsc/KaliszykU15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485842$A9534BD7-DDD3-43D1-9E48-E933B57DEA4F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b47d0f068d0e927590f2b56d80859ca587da1d3","datavalue":{"value":{"entity-type":"item","numeric-id":2740950,"id":"Q2740950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9723e72dce4dc4d775f4d5fbaf89c69c3cefa06d","datavalue":{"value":{"amount":"+0.875108","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q485842$C102F924-9724-45DA-8B46-A745471E7F79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"733045d4bdb6ac84e39d437da15db86acd1c641d","datavalue":{"value":{"entity-type":"item","numeric-id":6108816,"id":"Q6108816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96f63eecf6d41c263f6de28aa824c18ff230dfcf","datavalue":{"value":{"amount":"+0.86595863","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q485842$220BC1C2-6DA1-42A9-8745-68F26537B2D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"930b71b03a3b8cc040b2b9dd5a67f6b9426639c4","datavalue":{"value":{"entity-type":"item","numeric-id":4647500,"id":"Q4647500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"75ba542cdd49b4e9228759437ecece4b21235c58","datavalue":{"value":{"amount":"+0.8619283","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q485842$2E6A20F7-CFE4-4983-903B-3B97E009ED5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"609c9d261aa3d8763eb87621e0cde00ead7e5c8c","datavalue":{"value":{"entity-type":"item","numeric-id":5026334,"id":"Q5026334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"204b8e5f2f7581384b7275fa4431c5509c03446c","datavalue":{"value":{"amount":"+0.86156166","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q485842$98C3D1F4-9BD1-4881-A457-853BD149A2B8","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":"6c8c5c31462df25782c83b0e9609ec9eb93374ca","datavalue":{"value":{"amount":"+0.8540221","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q485842$6AEEB744-2661-4036-B41C-97CDB137BE87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0ee8b4c79deb3aa57ce2641b4039a91462d9cc63","datavalue":{"value":{"entity-type":"item","numeric-id":4465166,"id":"Q4465166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c619a2a99a7b85e0af122a8ede73f475c411665","datavalue":{"value":{"amount":"+0.84894806","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q485842$CB40493F-5215-4AF7-B48D-9E8D8D2681A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"09d72b2a5a9fb1810d850b52fcfccb7bfaba9d8b","datavalue":{"value":{"entity-type":"item","numeric-id":2964472,"id":"Q2964472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64cb7195a223ecb408350c31cf441feec8dcbb2e","datavalue":{"value":{"amount":"+0.8469645","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q485842$622B8ECF-B524-4BB4-8056-AC61CFFC69AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dc35801f25d4e873a92e4e6ee27d4249fb83802","datavalue":{"value":{"entity-type":"item","numeric-id":4728284,"id":"Q4728284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a96b09afb42796aa8af0d5df9fb9d8e3e7cbd95","datavalue":{"value":{"amount":"+0.8423126","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q485842$4EBAAE52-B940-45F4-B7F7-C3C28BA8D87D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b672819769f56e78f920c18ff9a2be8c99577da","datavalue":{"value":{"entity-type":"item","numeric-id":2751546,"id":"Q2751546"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2150da13554bdc7a7f8b5c7bd70a1ecb592ee723","datavalue":{"value":{"amount":"+0.8420869","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q485842$494AAB48-1E02-42A9-8EA4-48DC00FCA1C8","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485842$304EF84F-F0B2-4FF4-851D-8DA3EAD76D46","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Learning-assisted theorem proving with millions of lemmas","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Learning-assisted_theorem_proving_with_millions_of_lemmas"}}}}}