{"entities":{"Q832719":{"pageid":834567,"ns":120,"title":"Item:Q832719","lastrevid":77681720,"modified":"2026-05-06T09:49:39Z","type":"item","id":"Q832719","labels":{"en":{"language":"en","value":"Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7498608"}},"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":"Q832719$7CF3BB58-4A4C-4459-9D38-4BE52BEB9043","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ab9ff7acc7c3f6c1b1bba3f67b802b7d27ad40e7","datavalue":{"value":{"text":"Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q832719$BF31DA4F-0AE3-481B-870A-D61921B779D0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b455290f5b835c3773a6eb2262897ac70e7a163b","datavalue":{"value":{"entity-type":"item","numeric-id":287273,"id":"Q287273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$E421E4B9-28FC-49B3-A5F7-67B358EFED34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a6be8d909a46685b6a24cecd253b3dd33cd2a6cb","datavalue":{"value":{"entity-type":"item","numeric-id":832718,"id":"Q832718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$18682751-D608-4693-BDD2-5141DA58FEE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f977cc4afe30a7452131df7ff084411daffbbaa","datavalue":{"value":{"entity-type":"item","numeric-id":532428,"id":"Q532428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$92A381A6-9415-4DF2-BEFA-9466FDF38170","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":"Q832719$DDB8AEB6-3C2A-4707-B4C7-67423C96384A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"26426ab4d5a6ecfa201abc41ba9257e3996155a5","datavalue":{"value":{"time":"+2022-03-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q832719$1DA1B0DF-8347-4A5E-9E62-BD3B928F15EF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832719$DECBA300-3119-44A9-9949-D4CF6FFAA55F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c5ec6a8db0de24449ddc91fdc4a2f08f9d35776c","datavalue":{"value":"7498608","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832719$9C977BC4-1E47-4191-BC3D-46A647983FF0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"76eb71e232a39fb056b95e260ebf47f40dadc8c3","datavalue":{"value":"lemma learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q832719$C617C729-A990-42B1-A377-D0131F20CBFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9bac29b845ad68ca3b7fe442d74124a258d3fc28","datavalue":{"value":"proof generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q832719$B5E7BA7E-EE71-40ED-BCA4-64A9EC54C5F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q832719$90167173-A9B3-49D8-AF25-8AF09CEA8B29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4b395e8f6acd180e1625664cf0f73ca38f664e9d","datavalue":{"value":"satisfiability modulo assignment","type":"string"},"datatype":"string"},"type":"statement","id":"Q832719$E903BF3F-EEFA-4580-9682-8160DD9EB66C","rank":"normal"}],"P1463":[{"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":"Q832719$36D12327-7813-41C8-A415-DAA9D02CB7A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$224F7F17-40D6-449B-AE76-0263971CFB30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$EE24F06D-BF0B-4BA6-ABE0-D78E51EFF769","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":"Q832719$2A3EE434-DB1C-4459-B5BC-3088FF530406","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"90f139681161cf03fca3b88a13657b8b8fd37862","datavalue":{"value":{"entity-type":"item","numeric-id":25180,"id":"Q25180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$85FA4895-A7CE-4209-A3D5-39C18AB3F332","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":"Q832719$BBC949E4-E302-4C08-B6EB-860397DDC2A0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e9b7474b2c630b60f0542500edd737b02db9762a","datavalue":{"value":"https://doi.org/10.1007/s10817-021-09606-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q832719$7BF861E5-84CF-477C-A4F0-BE5EC00ED14D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"46671776c3da1f6da72e0e61dc042716c9d295df","datavalue":{"value":"W3199921595","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832719$0632B788-5B1E-46BF-B457-B23671406C25","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"ad91fe8d22d4fe37b87e87f6deed65c2c54cb288","datavalue":{"value":"Q113901236","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832719$8FCDFD05-B308-4E0A-9F88-67E4F7A73E99","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":"Q832719$6AD1883F-C891-4914-9E33-8D0E833C520A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6788f8c83d5a5db6237942eed0df1dc9fb4fc24b","datavalue":{"value":{"entity-type":"item","numeric-id":5919479,"id":"Q5919479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$4C43DB6D-4904-48DB-B29C-48DD6A469D53","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":"Q832719$41F5B42F-2E0B-4538-8D1E-91DFEC4F49E6","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":"Q832719$FB0B4ACC-CEB0-42CB-8661-0876C4BF19E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10b89f95e856482d87c1eee104a58dbb5392af66","datavalue":{"value":{"entity-type":"item","numeric-id":2185458,"id":"Q2185458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$5D0B5B3B-0733-40ED-A403-49C18C129A68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d645e2b876ab109a4fadcb1ed7f0c554bc73185c","datavalue":{"value":{"entity-type":"item","numeric-id":2303254,"id":"Q2303254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$17A46F6A-044E-4782-9FA5-5DF005216CAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b19e162499ee50b6406375bb12c3586f0f66a94d","datavalue":{"value":{"entity-type":"item","numeric-id":287275,"id":"Q287275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$A18FB856-5F1D-4314-BA04-0CE7D2774953","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f85fd02f887f9e6cdc6efa73686f469882f2acf7","datavalue":{"value":{"entity-type":"item","numeric-id":438533,"id":"Q438533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$94A8FC0C-29B5-4B9C-A27D-4BFE2F7C0CFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ccddffba771795151957f5712724106bbb0cab2","datavalue":{"value":{"entity-type":"item","numeric-id":1707598,"id":"Q1707598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$0C18D446-11D4-4F83-BA9F-A4A10CA01B10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2657b817b7754d2c176503843bf922ca3d3ac15d","datavalue":{"value":{"entity-type":"item","numeric-id":2180222,"id":"Q2180222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$2EF194FF-FC3F-4A37-AB29-AAB43E112C27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c10120b6d63d2d79d3e3d7f48a799e97be65acdc","datavalue":{"value":{"entity-type":"item","numeric-id":3454126,"id":"Q3454126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$B1BE8E99-A1E0-41E6-B16C-198246A19BF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$40A4AA53-75E8-44DE-A03B-7C3CE6298FD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"231ebacf8251b12a92546d1b1d1797e6e82d3559","datavalue":{"value":{"entity-type":"item","numeric-id":2303236,"id":"Q2303236"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$5154519B-451B-4931-A619-F764B4BA0540","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4695cbc8cd59305e55d74b7e093c5f61db18006d","datavalue":{"value":{"entity-type":"item","numeric-id":3588085,"id":"Q3588085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$96534C5C-34CB-41E9-B3D3-14DF91B333C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5ccea7b6fe9f5a7082344f9edaface083da76","datavalue":{"value":{"entity-type":"item","numeric-id":2405252,"id":"Q2405252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$601CD421-68B2-4F47-A6C6-2F7933C54EE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f64a9ce1df6d32a732886ec13ebc30e0107b2809","datavalue":{"value":{"entity-type":"item","numeric-id":2864402,"id":"Q2864402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$725163D9-9164-46B2-88FC-264E2B5DA2E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddeddf292e13fd796c5c20e153357856b636f89","datavalue":{"value":{"entity-type":"item","numeric-id":2926635,"id":"Q2926635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$C634D20A-5922-470C-9F66-D7451C1E0BD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2b783d0052b7f250a9573410e9be2b4624ef11e","datavalue":{"value":{"entity-type":"item","numeric-id":5899057,"id":"Q5899057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$62E7DBD9-60D0-4DA3-8BBD-5FB2CE1CF7F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf31db5eff704badf24a749933b64d7b604a12b3","datavalue":{"value":{"entity-type":"item","numeric-id":5277797,"id":"Q5277797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$521E9218-ED61-4F79-B0E9-ED4DC283359A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$C44E6A14-25A7-4589-A66F-ACCD40D7469C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ef8a8532db5854f5d22fa31dcae929508b22146","datavalue":{"value":{"entity-type":"item","numeric-id":2096440,"id":"Q2096440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$26B8E5FE-3683-44F0-B060-B7A2D5A55179","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd1ae1eae0bbb3048cc59d85f34aded019099780","datavalue":{"value":{"entity-type":"item","numeric-id":4928451,"id":"Q4928451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$FEF7D1CD-1B35-4978-8A1B-F83D01073164","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87be12daaa9049d37eba12568fd639bb8a1c86c9","datavalue":{"value":{"entity-type":"item","numeric-id":2908507,"id":"Q2908507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$DB81ED7D-9DA0-4C6D-BD16-B7D15B3FCA3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fa4c2387ad30aeefcdaa752dcaca22072d33adf","datavalue":{"value":{"entity-type":"item","numeric-id":2961575,"id":"Q2961575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$CA4BEC48-4AF9-4923-A05F-88DD65073DE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37706997c0e12650bf30406d5f3ef502cc6c8e28","datavalue":{"value":{"entity-type":"item","numeric-id":2351157,"id":"Q2351157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$9EDB4216-271D-47D9-9767-53DE405BAA10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d77121ca06023666fb3b31fe1611bc7b34ff56df","datavalue":{"value":{"entity-type":"item","numeric-id":2908506,"id":"Q2908506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$2289A321-A636-4A02-BF6C-86A4EA2CBEF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88c255f2e6ecd34a611f1ccf928bf197acbeea63","datavalue":{"value":{"entity-type":"item","numeric-id":4051879,"id":"Q4051879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$2225DEEF-D617-48A0-8F15-981F5D85E2E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27230ad583fb6c91e5e0b2ed04e15a2a06ba4a72","datavalue":{"value":{"entity-type":"item","numeric-id":3182526,"id":"Q3182526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$D23A5BF6-3FF6-4D58-B9FB-80CAB10E0A44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76f085e060cc02117b4ec73931c77617da801d17","datavalue":{"value":{"entity-type":"item","numeric-id":2473386,"id":"Q2473386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$32FD2C37-B841-4F92-B9CF-E06BCCC0372A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4e6adf13c6408e6c2eebe9bb0eee05dbe30b987","datavalue":{"value":{"entity-type":"item","numeric-id":3524998,"id":"Q3524998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$3BBBAEB8-D6FB-4AC7-884C-B230FDCDC8F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bbe72cc116925a801c6363ae53a473520b6daad","datavalue":{"value":{"entity-type":"item","numeric-id":688575,"id":"Q688575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$90ADF813-FFEC-482C-9DA8-E29C3BAA833F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f814032017aa40390d4c6f26a550d62bb08ff374","datavalue":{"value":{"entity-type":"item","numeric-id":5503674,"id":"Q5503674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$0221475D-8DE1-4962-BA0D-A5B5881C3C6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9269e64d2adca53bb2f298ca1a02b550d98c27a7","datavalue":{"value":{"entity-type":"item","numeric-id":4571400,"id":"Q4571400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$1627ACA7-1C7C-42BB-A754-7B1651D57370","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf127aacc48403a7b3907e5c9de96f1a874f90aa","datavalue":{"value":{"entity-type":"item","numeric-id":3636877,"id":"Q3636877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$50CD41FB-3CD2-4733-8C7D-2CE9588CB789","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f2acd13394e12d53f7294c47790565e27a57f11","datavalue":{"value":{"entity-type":"item","numeric-id":3857731,"id":"Q3857731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$39369C14-AC2C-42DE-BFBF-E327960339D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a11574a9e9ab53768e977b5417eb20cda54355b0","datavalue":{"value":{"entity-type":"item","numeric-id":3677735,"id":"Q3677735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$FFBBDA9B-E725-4C79-BA09-A178EBA601D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce7b2dd2863358cf2a528999ec6b006fdf400b99","datavalue":{"value":{"entity-type":"item","numeric-id":3899468,"id":"Q3899468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$55FB7BE7-F3D1-4F6D-801E-4E8D5C6DAF50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$614D7EBE-DF37-434B-9914-B20202F9F211","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14d65f813b7bf62e89eaf2eb886e2ecf258499df","datavalue":{"value":{"entity-type":"item","numeric-id":4221106,"id":"Q4221106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$FAE6E0B1-35AB-4E2D-A6BD-C519C487C9CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2105141632b085f82446bd2aa9c9fb3250806ad","datavalue":{"value":{"entity-type":"item","numeric-id":5175982,"id":"Q5175982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$8E528CF7-8AE6-482A-AF2B-11D89E8996A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0b8d74eb30783ead52df96f665a06c49d9668e6","datavalue":{"value":{"entity-type":"item","numeric-id":2942928,"id":"Q2942928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$CF4ACBAF-895A-4169-9C33-A1A363F4625C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a3d8be39100c65d1e448187a4dbf9fe46245230","datavalue":{"value":{"entity-type":"item","numeric-id":2818018,"id":"Q2818018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832719$5F6D2D62-0C4F-4EEE-88CE-353A27CD894E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4a2d7431d85a9cad5c8b9099ee993a7e77124c89","datavalue":{"value":"10.1007/S10817-021-09606-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832719$DD316ECD-C070-402A-9684-929EF2756FFF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"15687028d8b25ed5c6f15c20aca3938aac7bf34a","datavalue":{"value":{"entity-type":"item","numeric-id":2303254,"id":"Q2303254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ccc9f76c560ebbab5b1bb92715ea744a6a9b7678","datavalue":{"value":{"amount":"+0.888020932674408","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":"Q832719$78E07005-A9FE-4FA5-8163-6A347984114F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb29bdfd2432d520a44e436c9a9d449e487108e7","datavalue":{"value":{"entity-type":"item","numeric-id":2405239,"id":"Q2405239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5250d97297d7ad5f44e40c51cb9d61d78f08c247","datavalue":{"value":{"amount":"+0.8774343729019165","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":"Q832719$6390D6BE-BF1E-4DF2-96F4-76CE97F9F534","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"663aa1de8a6d978e2db16aaa337bd4bfbec378db","datavalue":{"value":{"entity-type":"item","numeric-id":2185458,"id":"Q2185458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6431f1aae0159c7196d03be2e56025aca2058f9b","datavalue":{"value":{"amount":"+0.7777044177055359","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":"Q832719$78352692-3FA8-4584-B5CA-78D22434C604","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3e71bfb5b68d2283442ce2c6ed865faa5ef3fdb","datavalue":{"value":{"entity-type":"item","numeric-id":5756564,"id":"Q5756564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0131511591bc76a832b05d868c938101a02fdebe","datavalue":{"value":{"amount":"+0.7666400074958801","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":"Q832719$AEE735B8-A0A3-47CA-9B31-3CB674B6A40F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f96ad6f1103380f5161bf881c0a35b6d0e440bd5","datavalue":{"value":{"entity-type":"item","numeric-id":3525013,"id":"Q3525013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c93ea09cb82ed4444c8367bfb2452eacb41b4cf4","datavalue":{"value":{"amount":"+0.7635611891746521","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":"Q832719$F2AECA08-4FF8-4F2B-A190-709F36811C3E","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":"Q832719$62B4D613-7BDD-42C2-9C8A-EFA2D2BE9369","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Conflict-driven_satisfiability_for_theory_combination:_lemmas,_modules,_and_proofs"}}}}}