{"entities":{"Q287340":{"pageid":289107,"ns":120,"title":"Item:Q287340","lastrevid":60718863,"modified":"2026-04-10T18:42:56Z","type":"item","id":"Q287340","labels":{"en":{"language":"en","value":"Semi-intelligible Isar proofs from machine-generated proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6585624"}},"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":"Q287340$542ABAAA-906C-4D0A-B63B-DF38869AC121","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1c5a368e74def61810710c2ab8f0e37e4f767b77","datavalue":{"value":{"text":"Semi-intelligible Isar proofs from machine-generated proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q287340$DD758C9D-B0E0-4B66-A152-338A433FDFC0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1f8ac29a1e5c3ff67f814e00286861ce95916a31","datavalue":{"value":"1356.68178","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287340$D2866F19-0D20-4B18-B023-F0F4FD740ECD","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":"Q287340$98C222EC-C4F5-44E2-B287-54AB5F0072CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e52ea9fecc32655489a0560f1f3a2c96d34140f0","datavalue":{"value":{"entity-type":"item","numeric-id":287336,"id":"Q287336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$E4B55099-12D7-41A3-B8CA-ABB86663D05B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ef26cceb99c4befe66da5792d77abe576a865b4f","datavalue":{"value":{"entity-type":"item","numeric-id":287337,"id":"Q287337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$D2641822-9ED4-4581-A484-07F6893CAA56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8aba1902e572f1c009b0bc454c491a3ec1dfdc47","datavalue":{"value":{"entity-type":"item","numeric-id":287338,"id":"Q287338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$F065EE95-6D35-4796-A928-8FAE9E081172","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bc70846e6a0bb6083e309f753b0ef80e4df5bf5f","datavalue":{"value":{"entity-type":"item","numeric-id":287339,"id":"Q287339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$5C2FB2E0-865D-4CE7-8733-B82A8E407ED3","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":"Q287340$81BC75F3-C5B3-4AFC-BB8C-94DD0F867AA5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b626bb78b3e93b3076e6958296f7f25e2e74c3ab","datavalue":{"value":{"time":"+2016-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q287340$304B8347-A4B1-461C-9805-3FBEE7918359","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"55ac4094015192ad000fe83d90794e707da9e069","datavalue":{"value":"https://hal.inria.fr/hal-01211748/file/paper.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q287340$EFA97B01-CEC7-4C6A-BDA9-97BB8F64A941","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287340$0219FCFD-DFDD-44D4-947D-7E4F4C98AB01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287340$6C262DCA-3421-49B1-9151-1D2266DA863E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d8e56e3e9d89aff1237c59c0ad314d0dc8948c78","datavalue":{"value":"6585624","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287340$CFEEBEE1-F3EE-4D2E-9B21-B4485B4C9FA8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1735a133d49ec9a3b5c084ee424340f472bf4d74","datavalue":{"value":"automatic theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q287340$C13EFC0C-AFC0-4565-B368-7829A8517589","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q287340$35FC2B4B-E2A4-4012-95ED-71FA241088D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q287340$5F74A576-6186-46B4-827B-D2400353AAB0","rank":"normal"}],"P1463":[{"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":"Q287340$FB818D57-2847-4E43-B0FA-E993EEDE7240","rank":"normal"},{"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":"Q287340$CBCBCED4-5E05-4D3E-83BE-D6DA3126CBC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$6BA9B5E5-5CDC-4A69-A6AB-02CE208E056F","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":"Q287340$E8D2D67B-F012-4A30-8589-8FF15F08567E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"491e4169c914222bc349264f15b36cbf2c3ef446","datavalue":{"value":{"entity-type":"item","numeric-id":18920,"id":"Q18920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$70643A96-DFA9-4ADA-BB73-B919087124CB","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":"Q287340$B5534381-C0CC-4028-B897-7242DB14A055","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3ac1e8c13c0130a75f4cf78841def0133e1a8ff4","datavalue":{"value":{"entity-type":"item","numeric-id":20425,"id":"Q20425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$51D25776-D854-4A00-AB72-1F2DF367B57E","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":"Q287340$C89C45CB-9197-4289-9E06-D6D42B66F98B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dab39ec190c7fb2818b71468da9efc600915608f","datavalue":{"value":{"entity-type":"item","numeric-id":33151,"id":"Q33151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$33B0DE2A-A534-43B5-A0FC-00A963486E88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"91f28dff700a7ef6588add7fd73cead62f561539","datavalue":{"value":{"entity-type":"item","numeric-id":41245,"id":"Q41245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$84F0268F-FDB8-4466-AA12-5BAC58418332","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":"Q287340$034AC353-60CB-46C8-BB74-C915426C38AA","rank":"normal"},{"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":"Q287340$7A6EF31B-E38D-49EC-99B9-7575DE8C8C2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$4BCB62A1-8577-4CC2-A590-CF1839FEF59B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$4D49E664-8E78-4632-91FF-B29D4EE501FC","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":"Q287340$6DDEDD11-A0DB-4079-A733-E960B7F0E476","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$C645996D-405E-4013-84D6-168BB15C5A1E","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":"Q287340$5043A15C-2BC2-4E00-B2A5-5EFE704C54C9","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":"Q287340$3E4F433E-B58B-4514-A63C-B2CBD9581B59","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":"Q287340$5647483F-4EC7-404B-9CFE-52D881759F32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c766f98bf98fe7cf06a05963cc75ed84be39ac3","datavalue":{"value":{"entity-type":"item","numeric-id":31394,"id":"Q31394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$89CFD955-1A2A-482C-B2F3-A335FA0B3303","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":"Q287340$C5CA8813-65C6-48AF-84ED-BBC3A08EFF1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"65577c230f961fd84aa81a17ee545955a6f3433a","datavalue":{"value":{"entity-type":"item","numeric-id":43948,"id":"Q43948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$47E5B954-7142-483F-88CE-7ED50627AEE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8617a61c90a632f23d3851deb94e1069d2479a78","datavalue":{"value":{"entity-type":"item","numeric-id":13268,"id":"Q13268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$EC196E67-FDCF-4602-B7ED-693E8A3DEB57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$C9A4A82B-E239-414A-BA47-2380D2528DD1","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":"Q287340$CB23D317-1C45-4F2E-8EBA-09D44E481BF5","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":"Q287340$DF6DC709-E48D-406A-AC8D-8F15856BCBA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"133e2e5701b3435e4a72bb2a6345ff9894f7c6da","datavalue":{"value":{"entity-type":"item","numeric-id":22369,"id":"Q22369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$99EF2751-B9A3-4BA6-816B-D4BFB95CCE09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6c57eda5d94dceb2136cb8e619997cc01ed97db7","datavalue":{"value":{"entity-type":"item","numeric-id":43915,"id":"Q43915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$4C979D7E-B8E8-42B4-A7D1-A8C262F7FFB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab284b1418c765bd41a34046f2aa8e68a1e62ed3","datavalue":{"value":{"entity-type":"item","numeric-id":43916,"id":"Q43916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$595CE73F-6B2B-46E8-9F7D-03394EB73FC2","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":"Q287340$C262FF93-8787-4B1B-B29D-565785B56A18","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0f22cae772678eadac3c4aad970a891aa4eea7f3","datavalue":{"value":"W1216298300","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287340$3ED246D4-6653-4430-A1D0-F26645BECFCE","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"e5885c94594d9be546b70ad2094797d70b034437","datavalue":{"value":"Q113901251","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287340$C45AB401-F8EF-4679-A364-94E78926E540","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb15445443b7a8677c7ef043ed8530f20d54b0c3","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$7B5BB948-2621-4625-8775-8651F650005F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0fec4ebbd0f7e0440d7bf45181d3d2e0b25e7779","datavalue":{"value":{"entity-type":"item","numeric-id":2847390,"id":"Q2847390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$6DE3FED8-1064-467C-A1AC-C903D20026A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9fde9a4f5d430508c0f363027ee29197b514110c","datavalue":{"value":{"entity-type":"item","numeric-id":4928432,"id":"Q4928432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$E76FBE29-8112-4FC4-A9CD-CDC183F12B19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b1137cf78c4cad0e217f70ec321f2a593915490","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$D8A58838-E739-478A-BB8F-FC8516EAD2F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4adc22ed174f33297ffa675f67b5ee27a98ff71c","datavalue":{"value":{"entity-type":"item","numeric-id":3541699,"id":"Q3541699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$A0FB069C-A8EA-4F8F-B3A9-3124ABD1BC64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bcdd88c0187437df1dd77abdaba504f2664c711b","datavalue":{"value":{"entity-type":"item","numeric-id":939166,"id":"Q939166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$78EEF578-48E3-4487-AC53-702812CC756D","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":"Q287340$EB07D830-051A-4763-8A9F-90C68F6D9E59","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":"Q287340$5AD16B96-3AB2-4F1E-A49C-13732957E486","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":"Q287340$7DBC1AC5-E331-41A5-B1D5-26E72A5FE872","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ee1ea8cf54f9acb5c85bdbdec2a3cd970b582f1","datavalue":{"value":{"entity-type":"item","numeric-id":2904256,"id":"Q2904256"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$CF198E82-AD97-4AD8-A99E-3DFF1544EBC9","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":"Q287340$B6C8A58D-1B94-480E-A684-727666F12924","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"494aa31720bff090f87eabeb86ce7380ba058cbf","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$02DE52C0-111B-4800-AC21-4DEEBDB3FEF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73747d1be528c82497c6517bd1ecf143bfa790b1","datavalue":{"value":{"entity-type":"item","numeric-id":2908482,"id":"Q2908482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$5C6804C3-75A2-430B-BD76-E24AF4F0F7B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42ba0d7a787c3ddf27f1ee78a59c4dec37184a75","datavalue":{"value":{"entity-type":"item","numeric-id":4520767,"id":"Q4520767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$A493F188-7A3C-47ED-A33F-9C167DA39DF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb051a6b1eb9b88364c46513701492fc0e99189","datavalue":{"value":{"entity-type":"item","numeric-id":3150300,"id":"Q3150300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$40F954C3-A1BC-4663-834E-0CC6E4E1DCE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2be7638796320e0bd21589c519d4a54a0b3ddeef","datavalue":{"value":{"entity-type":"item","numeric-id":5387851,"id":"Q5387851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$4D11CF8A-3E4C-4D76-91B2-E61B852B900C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25e09fec5d336d41c3a34de2171a3b627f63c544","datavalue":{"value":{"entity-type":"item","numeric-id":1273392,"id":"Q1273392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$5A73278F-9E7C-4827-863E-B7EAA4E89CEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d033b0480cb3f4fe29c5cd97ee8fdad8a665383","datavalue":{"value":{"entity-type":"item","numeric-id":2908498,"id":"Q2908498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$D6604057-05AF-4E33-8DBB-D1089D6D85A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$0AC88696-06BF-4D18-9167-93E6599AC07A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$9E072211-0373-474E-80F5-713F4013647E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$15FB0040-AE37-46A3-9BA0-B3257C5C1E11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c52cd1a25a23d6ee1d2d790b85193089c176c154","datavalue":{"value":{"entity-type":"item","numeric-id":1840387,"id":"Q1840387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$403D029C-1CB3-4672-BC9B-453ECFD46378","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":"Q287340$25CCE22E-0E22-43DC-AC6A-2C73F0D01178","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":"Q287340$EA326BBD-C64E-4E82-BCD0-426EB03ED4BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"501aefe4754342fb8d5444baacca037714207964","datavalue":{"value":{"entity-type":"item","numeric-id":4999425,"id":"Q4999425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$C6BE4B32-EC0B-4BBB-8A97-992DBAE6A52C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6034aced9366f83398efb9421b411961866b5d9","datavalue":{"value":{"entity-type":"item","numeric-id":3997716,"id":"Q3997716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$5CC90DCA-C8D1-4AFC-A490-F77FC27AE1E4","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":"Q287340$C07476AF-1DD7-4E86-8CC5-48BBA828E3E7","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":"Q287340$5336D8B3-2866-4294-BE52-C26E5F92632C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4470ad681c71989636fed60ae376323914a5ddb0","datavalue":{"value":{"entity-type":"item","numeric-id":2723444,"id":"Q2723444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$AA92AA15-1CA1-4CCE-B319-A4714A3E9915","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":"Q287340$13ACF079-A7DA-46E8-A048-325C9794FBCE","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":"Q287340$F8692D2D-170B-4DF5-8F1D-1ECA15F44941","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5809a6684c365442525c649f10f3cfd46627fcb","datavalue":{"value":{"entity-type":"item","numeric-id":1825045,"id":"Q1825045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$902F470B-6B94-4A13-85DF-47ABB3B4AFEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e264974062f53b439460b85662778a60b49509d","datavalue":{"value":{"entity-type":"item","numeric-id":2926333,"id":"Q2926333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$245A015C-1710-482C-96DA-6DAF2554E7E0","rank":"normal"},{"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":"Q287340$36198D03-8E5F-4324-8BCF-0B6F1F9A8B81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5a256449611c84a11b081fc6ab121a5b321e50f","datavalue":{"value":{"entity-type":"item","numeric-id":1945902,"id":"Q1945902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$48E43015-4F9D-4093-9D45-5CAAC01FE12B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd2efa9cc52b9c7802bc3fd73236ab4bbd639fe4","datavalue":{"value":{"entity-type":"item","numeric-id":2921120,"id":"Q2921120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$A896B8F6-4BCF-46D3-AB32-65F7A93B3DBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$02AA1AF4-7BB6-42A1-812C-439F52EB53CE","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":"Q287340$80FC0B6D-1AB8-49FC-93A8-653222429608","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58cb14dabb49ce81b914063d4d765de30bcb45f7","datavalue":{"value":{"entity-type":"item","numeric-id":3338233,"id":"Q3338233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$ADB840CD-CA4F-4D0C-824F-74C277343388","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"92bd7a7804d462c14eca2f48adcb648eadeff050","datavalue":{"value":{"entity-type":"item","numeric-id":1100932,"id":"Q1100932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$D6CD6154-BD91-4CC2-ACBC-04800C0B6369","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":"Q287340$1F0F1439-4938-4E90-BBE8-1067A64D7C88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dee09e75a430fc0be911c9a36f98899b21bf0296","datavalue":{"value":{"entity-type":"item","numeric-id":2441776,"id":"Q2441776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$BAC30FF6-E520-41E6-95B1-481938683E07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$CFDFFAC9-B77B-4408-B6A7-952F1B35942A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"830cc442175c3fbcc9e8040acd1051edc376d0e2","datavalue":{"value":{"entity-type":"item","numeric-id":2723436,"id":"Q2723436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$2CF9D9DD-289E-42D8-AC99-78D4D2C1709C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a985fd023ef2b6e88319dc2c72d2561e393a9b5","datavalue":{"value":{"entity-type":"item","numeric-id":5326286,"id":"Q5326286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287340$C2F45CF0-3149-4C30-A83E-971ED76AD5F2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"29de660d9b5cde98cac0b6338b84c789686a5323","datavalue":{"value":"10.1007/S10817-015-9335-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287340$50170035-8A36-4B0F-AF7E-77F6BCE8F60A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38394b4e8d3a3502630a463829cd1f4840ac5524","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b09d51853f362fb7d3924fdbfd888cc6a28e329","datavalue":{"value":{"amount":"+0.8123874664306641","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":"Q287340$E10D29AF-AF51-45F8-8538-76569413AA14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e434c6f686246887cde238823958ad79571304c4","datavalue":{"value":{"entity-type":"item","numeric-id":2351158,"id":"Q2351158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b5ef300a2ce57d4b445fd6f784b3273fecc99908","datavalue":{"value":{"amount":"+0.8082336187362671","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":"Q287340$F61CA84F-3AD0-44E4-A364-C7560B68EE6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e42c0696ebfd3fb16c17afdd0eec4ae5147edf7","datavalue":{"value":{"entity-type":"item","numeric-id":5200019,"id":"Q5200019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cf22e39ea8f70607aee6ade1558501eaabcca6d3","datavalue":{"value":{"amount":"+0.7988281846046448","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":"Q287340$667983BF-EDE6-45D1-B726-18EA7F08D5B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"996184ff8199e312ae0c5c691b47c614bc41d7df","datavalue":{"value":{"entity-type":"item","numeric-id":2914754,"id":"Q2914754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"997430d640f6966ae6e6e9c211e92b32c4f57982","datavalue":{"value":{"amount":"+0.7736405730247498","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":"Q287340$2B80F90D-EC0B-46EE-A1E8-904D048130D1","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":"6b724dddbd3e94f4f85b649d09992ca878abdf71","datavalue":{"value":{"amount":"+0.7705538868904114","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":"Q287340$C8D455CE-3A2D-4ADC-96E5-51466AF51F6D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Semi-intelligible Isar proofs from machine-generated proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Semi-intelligible_Isar_proofs_from_machine-generated_proofs"}}}}}