{"entities":{"Q1431339":{"pageid":1442079,"ns":120,"title":"Item:Q1431339","lastrevid":68809092,"modified":"2026-04-13T02:12:11Z","type":"item","id":"Q1431339","labels":{"en":{"language":"en","value":"Theorem proving modulo"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2069028"}},"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":"Q1431339$02651CA8-A5DB-40B9-B088-20AB39452D0F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"35cd22d25780217fc64df9b6bf57d65737d2b4b5","datavalue":{"value":{"text":"Theorem proving modulo","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1431339$1F8919E6-160B-43B7-B737-E5546B72BD81","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"60a5fa5f84821a24a7f104264b8a8a68da8f0dc8","datavalue":{"value":"1049.03011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1431339$BB4595DB-1DBC-44AD-9333-E14208B05577","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"575fefd048eb3165b1b542f113070505a7b7d045","datavalue":{"value":"10.1023/A:1027357912519","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1431339$0CEEBEEE-E5FA-4C61-BED1-0687E98C428D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f681530f1e601559ae451198ac16d4e80569d32e","datavalue":{"value":{"entity-type":"item","numeric-id":436401,"id":"Q436401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$DBFE39EF-3421-465B-83BF-867187643B16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c50f42ac443d41828b557f6076f88056505c203d","datavalue":{"value":{"entity-type":"item","numeric-id":918955,"id":"Q918955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$61E98490-3B0F-491F-B591-C541EA59BEF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"67de4dcf41337233b478a60d1d06381752453e30","datavalue":{"value":{"entity-type":"item","numeric-id":857912,"id":"Q857912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$5B628380-31F5-40C3-8175-4AF5027A3AE0","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":"Q1431339$E5C69C14-1191-477C-83C5-7AC107BE53F0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4ba9d052c1c742a2c2f9206a1b4282a8f44ef61e","datavalue":{"value":{"time":"+2004-05-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":"Q1431339$2F42B7FA-4F80-431D-AA52-24960B4E7081","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e62db15a391ee3482a2074a5e277f25b85c54d40","datavalue":{"value":"The authors argue that theorem proving can be divided into a computation part and a deduction part.   Deduction modulo is a method to remove the computational arguments from proofs.  A proof search method is presented based on extended narrowing and resolution which is sound and complete with respect to the sequent calculus modulo, for a large class of congruences.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$F9FFCDFC-649D-48F6-9825-5DAE04D4033D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1431339$5866F4EC-5EE3-4CBB-8B69-3BE82BFB4552","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1431339$D0612D2E-9B5F-4050-9FD1-8EEF07A3BB78","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"662c3da2e7cf8815fca705e9621ead00d92ce4c9","datavalue":{"value":"2069028","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1431339$995A61A2-D48D-4857-94E7-27CAE2835AA3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$2A48136A-80E7-4D03-B932-E935BE496F42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$F9991524-226D-4292-A56D-9805795EE3F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$86821352-7CD4-48D8-ABD2-A3078CA4C203","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50e20429622ec08ba47dc9e7a4c57de8bf8a42d9","datavalue":{"value":"narrowing","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$A8DC4069-3F30-4CDD-9DB0-D5761DDAE1C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$0272341A-E051-4707-B444-4B1C70C961D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$940AC586-3422-45BD-85C9-BA750A2D739B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"908a412ea1d66c8c3e12f690543d47d72647ae57","datavalue":{"value":"deduction modulo","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$B4272B03-861A-4844-9903-518034397797","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e51a2d9e8f91102f3cb0d41e228201b59d4f55aa","datavalue":{"value":"sequent calculus modulo","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$84FBB4F9-1A37-43C5-807D-BE4EE48CB213","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3b34e81c9be74c25aae2603a8dfa343c349c2721","datavalue":{"value":"Skolemization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$23564DCD-6C88-4ABC-B615-70DC93BEC7BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"23328227337a3cafe924ff36301e08c88820342a","datavalue":{"value":"combinators","type":"string"},"datatype":"string"},"type":"statement","id":"Q1431339$7D52C6F7-5C4E-4391-BEEE-A08220300141","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":"Q1431339$F56B4006-BA67-4790-AB37-B7BD85B84F25","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5249c80fcd11fa0612fb7dd29644b8dc29907a14","datavalue":{"value":{"entity-type":"item","numeric-id":4939690,"id":"Q4939690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$C0C54F10-3B2F-4343-9D9E-B2BFD5BA5FA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0021eb1ef45a5b93ce1d9b7eb620338bc69ad123","datavalue":{"value":{"entity-type":"item","numeric-id":5638281,"id":"Q5638281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$143C7A18-3A29-49F9-B375-E27B961EB593","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$54C06F80-0DF0-470E-8872-77E5A7B72774","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ad7c23e8d7895495a33ef0a244c1d5f7a7d7e16","datavalue":{"value":{"entity-type":"item","numeric-id":1899908,"id":"Q1899908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$CF2A0363-F118-4341-B031-3593EFF47E09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"09f9dec41c7615ebddca88a5ee0923f61e9449fc","datavalue":{"value":{"entity-type":"item","numeric-id":1610674,"id":"Q1610674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$C0C573F3-AD43-4A68-9789-802449F9A6E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f4eb651c8363807599380b2222eea5dd308b21b","datavalue":{"value":{"entity-type":"item","numeric-id":1596540,"id":"Q1596540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$F4D850FC-8E30-4394-AEDA-E945D486DD42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4004164fb76db92bcdf23fd385dc006c288396ae","datavalue":{"value":{"entity-type":"item","numeric-id":4371674,"id":"Q4371674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$CDE143C0-F85C-4E42-A184-74FD318E5B2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb87030458893ce6a5226c20f4768389b71ec39c","datavalue":{"value":{"entity-type":"item","numeric-id":2751362,"id":"Q2751362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$B7F4D6FD-1C72-4AE1-AB70-75C972C1B65D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a01d4a91dcf05e247efe3d36d8b1cf5c4792f88","datavalue":{"value":{"entity-type":"item","numeric-id":4385532,"id":"Q4385532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$6AE10DA8-CC31-4B0A-9BB4-79346513B233","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ffa51fdb288be1837004e83d01b0afe835eee94","datavalue":{"value":{"entity-type":"item","numeric-id":3024833,"id":"Q3024833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$92402334-9401-424C-A078-A6ECF36D4E67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c7e99dee790823bc8c804e87dda851e7f3087c6","datavalue":{"value":{"entity-type":"item","numeric-id":4365102,"id":"Q4365102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$6E1CA57C-57B2-4B55-8F35-D6185C081DE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"39f569653d2a414897d836452d16cad942c8e70d","datavalue":{"value":{"entity-type":"item","numeric-id":4518864,"id":"Q4518864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$006A371F-82D3-4EBD-88A1-1CD93A5E7A1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b714ee7bdb70947b555d42ec2db46670455bb12f","datavalue":{"value":{"entity-type":"item","numeric-id":1431339,"id":"Q1431339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$53A629A4-FEC9-4C3F-8283-8D5503B38122","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5927659804eca2a32583cb94f8cceb03b87d2078","datavalue":{"value":{"entity-type":"item","numeric-id":1854337,"id":"Q1854337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$C324A2D6-FCB3-4EEF-B3B9-63FA012E89BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a571653cb6ab1fa29a33b3cbc9d3383816e568e","datavalue":{"value":{"entity-type":"item","numeric-id":2713352,"id":"Q2713352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$1682CEF3-2276-4CA8-AA6B-EDD8FCB255B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29d9991d99e156f55f64365f641f3d2ab2bc848c","datavalue":{"value":{"entity-type":"item","numeric-id":4944850,"id":"Q4944850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$C7E0F916-BAFE-4942-B50C-5F9FB89194D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8bf1eb0085816c68ff7078182501fe6b0337105","datavalue":{"value":{"entity-type":"item","numeric-id":3743300,"id":"Q3743300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$DBC0E2C7-20C0-4D5D-8710-62985E49527F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$4A712693-30A0-4B73-A620-EF3B6B11724B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1eb387d93d6d1c7b34f751c3ee7736c48adf0665","datavalue":{"value":{"entity-type":"item","numeric-id":1227601,"id":"Q1227601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$D177AED4-7D20-4873-A359-B713731B0470","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e9acb750b5a1fcf5fe08b591fc6df182dd9e5e0","datavalue":{"value":{"entity-type":"item","numeric-id":3883561,"id":"Q3883561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$75DC9F7C-8A3A-4C10-BB27-BF340881B956","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"849241baa6b3c56591969b2586e51dae90f667cf","datavalue":{"value":{"entity-type":"item","numeric-id":3816048,"id":"Q3816048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$040AAE19-1E7A-40E5-9181-E2C66E91AA86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c527e263525faa34ac4a72501bf8563b41ad015a","datavalue":{"value":{"entity-type":"item","numeric-id":4297316,"id":"Q4297316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$335C98AA-CCC1-4AE4-BEC1-B9B3D2DB8BDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50a041482acaef5481b7ba32e4bc3fbf732bf73f","datavalue":{"value":{"entity-type":"item","numeric-id":4400884,"id":"Q4400884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$053A3940-9A86-497C-AE85-90C87F879D43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"006077fa3558c96c24680eb8cbc601f3558b68ea","datavalue":{"value":{"entity-type":"item","numeric-id":4364370,"id":"Q4364370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$13C26FEC-CFB9-4DFE-9DC9-67117E7E5E1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba1eb42d9c5348c57088bd4b838a7a5b42853faa","datavalue":{"value":{"entity-type":"item","numeric-id":1314356,"id":"Q1314356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$34D412AA-D2DD-478D-BF4F-ADCF20C11686","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1e0b4fc54e8c62a86959e50d4b1b27d9d9a092c","datavalue":{"value":{"entity-type":"item","numeric-id":5581665,"id":"Q5581665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$B44A1047-BC71-49B7-B1A6-207174E13B8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ec18fe812b9e98f714f59469d9f5da1a94a710c","datavalue":{"value":{"entity-type":"item","numeric-id":1333525,"id":"Q1333525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$178A430E-902F-4457-8598-DB6AC7F713B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0c51e24e1428721a6903741aba45a8914c5f370","datavalue":{"value":{"entity-type":"item","numeric-id":1373299,"id":"Q1373299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$8BB49BF4-A620-4AD9-8653-81D2E6CBF6C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f634c169695e013798d603192de773983211324","datavalue":{"value":{"entity-type":"item","numeric-id":5210796,"id":"Q5210796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$FDC81E3D-BA9E-44BC-BD4C-4AF0C4F3419A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04bc46285c285bd5587f7f8b9ae32dc8b1cab95a","datavalue":{"value":{"entity-type":"item","numeric-id":1824412,"id":"Q1824412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$6C4805E4-F911-4DAF-9611-76A3B5F68CAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5939193d2c734f0c40871d2dae732bc5d8448c2d","datavalue":{"value":{"entity-type":"item","numeric-id":3673152,"id":"Q3673152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$DAB4BB76-0324-42F8-98BE-91DF7BDC46B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8670a1cb5138f59a7607a06c6c33e9eef7f2c9ea","datavalue":{"value":{"entity-type":"item","numeric-id":3938536,"id":"Q3938536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$2A5A3048-77CE-42EB-95BC-189830BBD331","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbf7a392ff381d91eb3e0017a3df59be02487110","datavalue":{"value":{"entity-type":"item","numeric-id":757071,"id":"Q757071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$0CA5E2A2-3EEB-4462-9353-8869F5A3BA57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10514d04294539f6b18e653ffed15729ce3e519b","datavalue":{"value":{"entity-type":"item","numeric-id":5678447,"id":"Q5678447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$EB2B38CD-5EAC-4C9B-BAC3-E7218C7D5BDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27ee3b057142576093bd9e66364057980fafc0e4","datavalue":{"value":{"entity-type":"item","numeric-id":1821564,"id":"Q1821564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$126F880A-4F27-4706-BAA1-3CADC4208C2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce65e744852a8304177cb1e448d04a739b85b8c9","datavalue":{"value":{"entity-type":"item","numeric-id":4539606,"id":"Q4539606"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$0EAB0234-C1E1-441D-BC9F-785DD09330FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d9525944835ab99fe0caee89af1d1c4f1696592","datavalue":{"value":{"entity-type":"item","numeric-id":1608925,"id":"Q1608925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$B61705D1-D071-4F2D-88E9-491FE782FCFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6638da077510d95046546294081de23a7659270","datavalue":{"value":{"entity-type":"item","numeric-id":6488530,"id":"Q6488530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1431339$48C2821F-1ACA-4687-A794-DDDFEE6C10B8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"22967f8e1d8aeb6b49dc6c074f34841d779a3d48","datavalue":{"value":{"entity-type":"item","numeric-id":5307079,"id":"Q5307079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dca2e409c4dd6fc2e4ef4e1e8f83791aa6553291","datavalue":{"value":{"amount":"+0.8479021787643433","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":"Q1431339$31612074-2B87-48C2-8EA4-7BE9BAC3FC51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b73316bc9293ca6098b85633ea043f8e1ae5b95","datavalue":{"value":{"entity-type":"item","numeric-id":5200022,"id":"Q5200022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd654254af6c43da9096da47d465fb5d0ba512d8","datavalue":{"value":{"amount":"+0.8345707654953003","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":"Q1431339$AF8AA662-C071-4A0A-A8A9-77A0B68E9D11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d22b9f82cd9bd048e12fef8e502f52d443ca7e3","datavalue":{"value":{"entity-type":"item","numeric-id":3586040,"id":"Q3586040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5f8ce064d7cd6632d4036a6544acd3ffa072446d","datavalue":{"value":{"amount":"+0.8234520554542542","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":"Q1431339$28DB8E25-FDD7-4418-9062-329752308CC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b7ef991317cb42ba6b39ad5bd12cbd14685f436b","datavalue":{"value":{"entity-type":"item","numeric-id":3612434,"id":"Q3612434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5223ec9d9204ad83c7b6425538a9989452864bfd","datavalue":{"value":{"amount":"+0.8045205473899841","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":"Q1431339$59FF518D-B78E-4FB1-B76B-9F14C212D10C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc117c5a2ae76e68481a50d229f4da7bb0a589a0","datavalue":{"value":{"entity-type":"item","numeric-id":3498425,"id":"Q3498425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c53021d2f8043dbf0a3978409123a172c6cb9e49","datavalue":{"value":{"amount":"+0.8038653135299683","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":"Q1431339$2036DAA3-9973-4BC0-B0B2-12350DE6BEDF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theorem proving modulo","badges":[]}}}}}