{"entities":{"Q40327":{"pageid":40383,"ns":120,"title":"Item:Q40327","lastrevid":56360676,"modified":"2026-03-13T06:14:11Z","type":"item","id":"Q40327","labels":{"en":{"language":"en","value":"Archive Formal Proofs"}},"descriptions":{},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"0df345eff2843afdad4c955703c50aff6e037f09","datavalue":{"value":"28613","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$20FD8B38-7898-4AEB-9FE4-9042E0787E0C","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"12bf2f186515e413aecdbf73169b0a08013cba98","datavalue":{"value":{"entity-type":"item","numeric-id":3453102,"id":"Q3453102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$0B6525B9-3783-4EC0-9EEE-0FB9A3F03F99","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$7010F0C0-A31E-476D-BF9E-08F0CA22D538","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"a81a5df48d1c89681c5c392f4479e27f7a46fbb8","datavalue":{"value":"https://www.isa-afp.org","type":"string"},"datatype":"url"},"type":"statement","id":"Q40327$4C0FE39F-15A9-46D4-BA03-9438DDEEBFE5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$0168A2B8-DFE1-4ECD-8808-70B93BCE0688","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"95bde9084e6ca63a8492631a417b047b22c72453","datavalue":{"value":"05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$940A8CFC-78BB-445C-96BC-7EAC478C224B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d379e93a1cc3ab3df2a5b8d85c84eb0620f6469c","datavalue":{"value":"06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$D442C820-63DA-44CC-AE2D-EF27B02D4B8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fd3cd3c8cd085ac2048034c2279872658062342d","datavalue":{"value":"11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$257C0734-CF45-4935-8E14-7FDA5AA0C574","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$3ADBBB50-7503-46D1-97EF-3B75E0E2B0E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ae9c75c1f07ce06d85b9552d2104619090f82402","datavalue":{"value":"00","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$23A74C94-163D-49BA-BB26-3EDC34CF8C95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f5c899803a3ce2dc0dd1263cc65df28aab94054","datavalue":{"value":"12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$020A406D-2A93-4A1E-B0F6-E756E3C5ED8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8befc1ffe367aef867e4dcd902eb59cbacd3a347","datavalue":{"value":"13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$B6AD423E-232F-4AB8-8B41-89C7F8F72AD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cd4f0694ac7a00e4fadde328cdb4437f6c066de7","datavalue":{"value":"14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$EE39C9FA-0C74-40F2-B170-4A948ED714B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5dd818343d7a5b259737eac61518c19de74ecd35","datavalue":{"value":"15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$C1367C29-8DFE-4844-BEC0-EA9F3BF2B22F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f50a93e1fa52c1f7a63c5e1d98864f256220e6f","datavalue":{"value":"18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$3B8EEC23-E560-4FF9-8DCF-7F30B0B72EAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c42d8309659ef226cd875765a3c9064bb7558782","datavalue":{"value":"20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$6483B052-3877-4C27-929A-4A8C7E7CF9BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d3fc854b328c20f46440ca61d9e1a4ed6cfc55e8","datavalue":{"value":"22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$7800F33D-2C51-41AF-9153-F720F3B3C3E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdcc80d920f5e4d163108380bb0c7de24bca08b4","datavalue":{"value":"26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$095CA7E7-E00C-45EA-96DA-98442D9F1292","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec41e560e80ab9e1fe0c779a012b3e380525af3f","datavalue":{"value":"30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$2B772E77-8BC9-47C1-9218-AC9E4A54EA70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3caa64e9b44e0e6a95be04e9d18f7428dc349506","datavalue":{"value":"34","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$16FD08C4-304A-4888-BB30-652FAE981D19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"01c8c566de1600f59b5f8122a428964fb913122a","datavalue":{"value":"37","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$D43C6B04-2636-44D6-BD94-90DE7E385F3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ca97ab6736a2cf36b4aa3171cbf7b0139773b03d","datavalue":{"value":"46","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$78BA6A62-1C0A-4EA4-B345-E9892265DB5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9c36f543604e3fdf981f5fb6ed78b53d6c52253c","datavalue":{"value":"47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$1D05B99F-2FAC-47C1-8ADF-B32DB744F8C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"389057ea232b6d266cab69038163241bd07104b6","datavalue":{"value":"51","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$626D8442-82C7-42AD-B659-942AF962EC31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"eb161afac2a132ba3ff878220cc5d73379a399b9","datavalue":{"value":"52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$82B0C07C-193B-489F-B102-476FAEB43C5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"43c1a4db523e8d5ed4d9f898b1f0303e17a6e259","datavalue":{"value":"53","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$16A6D4A5-536C-4E98-9235-EF2CC491CA08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"85b50fc0bb13fa24d727c960e97501e2c7bce333","datavalue":{"value":"54","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$F8D8453F-D514-4F5A-86C6-FD9680529B9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a467a32e3049b1299c9c2b688461b7f273ec943","datavalue":{"value":"60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$01095F86-AD9C-47FD-B9E4-57A25255C4AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"56359f9045fe5db9438daf1ab901fd6bd2edb7a4","datavalue":{"value":"62","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$0592A9F5-6C1A-42E1-A229-FE10FA29B546","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a104733b1e30d91f56342777dc887a3edbb9e05f","datavalue":{"value":"65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$84043BEB-9C3B-471D-816D-A6639CAF843A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4edc7e695c3667a3dc24594c0516548b87f81467","datavalue":{"value":"81","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$72747F31-ACEB-4070-8AA6-646B6DA17DFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"70815976aa44d316576d629b9a9b2ae7fe77d360","datavalue":{"value":"83","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$20F3D8EB-9412-41AE-B1DC-CA95FB3CDE39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"541da1e359051dfcf3c498b9f1f1f8f905fbafe3","datavalue":{"value":"90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$BF96639D-9CE7-4F2C-929D-A0F03B3C2FBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a438efc028ac8f007fcfec586995516429ecdd8","datavalue":{"value":"91","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$2679F888-89E9-45E6-889E-2743CD7FFF70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bebb7aa66b6973aa3a0c9749da8f6cd6626bb594","datavalue":{"value":"94","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40327$5BEA0FDA-D0B3-4A1F-A236-2A2FD3FA555B","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$90ECE793-67FE-4EF7-8F49-013155B17411","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$A665C94C-CA05-495D-AF31-9DEC752F619E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$6A81DFDD-2B96-46AA-8015-7EB55DD63046","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$C5510BB4-7204-4970-B97D-2E7BEBD7D759","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$8FA4B406-F7A3-4866-A1D4-383D5DD72607","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2ded5a481ece08049848bd1edb3f9afa21f0df2f","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$9FE7E133-2264-4B75-9A8C-BA1A35DC0DBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$8B71AB61-2AC5-4724-98F8-029EA3BA0A6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$1BC40C5E-253D-497F-831D-DE6A85DE8933","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ed15eb8701a335444fde1bcc3327d1067ce64751","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$4DE72E74-2146-45CA-A52B-8CC7CFAFAB19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f70e8f897325b539c702d8d7cb97dfafe554224c","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$C2C0D87B-2588-42A4-B709-14FD4EBCE04C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9ad8338290e864661fc95f2a66261cf7e07a407c","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$C490697B-E722-49AC-9A8F-FC8DA8738277","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b82152c1528c5be7e2040d1abd74977f4fe51817","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$A8AF2B26-729D-45EA-913A-464D9F939CDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7434bcf5c727d2c07e931aea1694436d0b39cd53","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$91291119-2501-421C-BF20-43E4267354C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc4eff68b160f30b8d66dfcb610a0ea7a927079b","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$E6036AAE-F6E0-48E1-9D62-03B51E6C1DC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"85d5a2bfb7e5cd7e1dfb166523d6500a685410a1","datavalue":{"value":{"entity-type":"item","numeric-id":13377,"id":"Q13377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$9FC3E596-BEBC-4EAB-9A20-5B0721A885C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ff80b41d03c65073c007c903a317be0a9c94293e","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$2CCC0458-1E00-44D1-936A-44D665FE6730","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"61d0c0612cc30c9c51b93ddaf1f78ee1ae75f9fe","datavalue":{"value":{"entity-type":"item","numeric-id":18676,"id":"Q18676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$2D970A6A-B91F-4DA7-BB3C-0333C771356C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"28fc316ccc1f38bd6830fcffe3187b6d32168084","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$97CBB96B-1DCC-4EBE-8DD9-BC4844366ABE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"18e15e946a9b8db60c88d8c0a9a054a3d76ac633","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$0DE5F0E9-B996-476E-967B-E83B9B548591","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"139c69b2a23f419923a7989e28183ef8179b6836","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40327$058813B6-9E63-46E2-AB72-2AA98D8487DF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Archive Formal Proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Archive_Formal_Proofs"}}}}}