{"entities":{"Q438533":{"pageid":440300,"ns":120,"title":"Item:Q438533","lastrevid":61924392,"modified":"2026-04-11T02:35:11Z","type":"item","id":"Q438533","labels":{"en":{"language":"en","value":"On deciding satisfiability by theorem proving with speculative inferences"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6062048"}},"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":"Q438533$E693BAA9-DC08-4D81-8613-253B5A9A8FA5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"12c20ea1b6fe610dbe1137ddf7c88cf195f15a4a","datavalue":{"value":{"text":"On deciding satisfiability by theorem proving with speculative inferences","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q438533$5E17DAA2-A19B-4B1B-B1E2-6A1EFAF11C05","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"214018eaeadfad43a01a91e1eaec24b849f4eecc","datavalue":{"value":"1243.68265","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438533$431FFA26-B773-4BB9-AFEF-6BB443853E4B","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":"Q438533$F151FBAE-9E19-4170-8925-E1EF248EB558","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6b74f2805d58a252b355491b4dc993b2648b5d8c","datavalue":{"value":{"entity-type":"item","numeric-id":437036,"id":"Q437036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$A956BE80-7A9D-4853-A0C9-D06E83188FB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"899468d0fe4ec0ae9c5ef91b63881ae72bf40a46","datavalue":{"value":{"entity-type":"item","numeric-id":438532,"id":"Q438532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$412D009D-36D5-4BAA-9A27-F92D135261B2","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":"Q438533$DF52D082-9104-446A-B67B-5041F47EBD56","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c7ad691786690cf86127845d28cf47311748286","datavalue":{"value":{"time":"+2012-07-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q438533$1183A1DD-8C22-4988-9CB6-8A4AB3846C71","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438533$628EAFF1-526D-4E7D-A941-911F6EBDCAD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438533$B74DFE3B-4633-4A32-8646-6E417B83E40C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438533$9446E65E-9A41-4200-B438-E3782A06610D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e442900952aafbdb6e18d783a46c1f333a990320","datavalue":{"value":"6062048","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438533$5C470A1F-5534-45A7-8157-3C531A0B9D55","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"319e87e1406d8756d4964625bc15ef93f38a0cfa","datavalue":{"value":"program checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q438533$76DA0B18-7DDA-46FB-AD62-C83EB7E3FEC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q438533$C086E93D-C8DA-4996-A39D-80204D59A676","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q438533$5D389E53-35AF-4AAF-85D0-47ED677A949F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bfff88c2380e4c25bc3fa0710ad2e9544dd0740e","datavalue":{"value":"combination of theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q438533$7C44D62B-04EA-4668-B8F3-7ADE1D0E92A5","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$592D25A2-C462-4DF5-867C-5B267191009B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$19A89B8D-2F42-428C-ACFA-715990830200","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":"Q438533$8E006AEA-FD33-4646-B1A7-D5E2583F4FF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"076ade2f424feb4292ee73db98fc22d62f6154a2","datavalue":{"value":{"entity-type":"item","numeric-id":16769,"id":"Q16769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$6022E983-D8D6-4196-AEA7-A06C2EE536E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8312fa7309b2bb86919d80d9dd327b01ccd3eb19","datavalue":{"value":{"entity-type":"item","numeric-id":19268,"id":"Q19268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$1CDB3C46-36C6-4C26-A56E-6B39ADE9974E","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":"Q438533$6DD1770F-BE1D-4E3A-AD79-48E2A015D0BF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ac2837bcc9ef301c4ff2a62a97ef69f6fff2c852","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9213-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q438533$4338A86B-C862-4D49-9237-E60FA27AA5D4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"96398748e99d8bd64aa95ec3d76bac1b3ee8ff13","datavalue":{"value":"W2150307403","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438533$9D0B6569-1217-4D2B-B74C-DCC1C84E767A","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"39080197163fad7e53f3bfe7e686f870c290a9e0","datavalue":{"value":"Q118190413","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438533$D8F0A902-B7F5-45D0-8299-87876B314DB5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f49cdde0e4e93beb3ec22ebb07bdb6ff64fe9a7c","datavalue":{"value":{"entity-type":"item","numeric-id":3655193,"id":"Q3655193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$99972693-E9D0-4164-B88D-7B9A4B9FB264","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98b26c6ab69d79279e5741dc9e752266a4bad9b0","datavalue":{"value":{"entity-type":"item","numeric-id":5747768,"id":"Q5747768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$58E109D7-8C90-4CE6-8E1E-C0837B064029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4741e9d217eddd81c00e6430470e876cba6d8519","datavalue":{"value":{"entity-type":"item","numeric-id":5491893,"id":"Q5491893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$03351AB8-BC32-4D7E-9CA5-AAA38F1E8005","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"103360585a9bffb1c1cc70bf60b5d74438ed3255","datavalue":{"value":{"entity-type":"item","numeric-id":1401930,"id":"Q1401930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$4679666A-786A-48F3-93C0-74EC2B50627F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aefe5e0f2b827afb25f0a8067d25c4a893f91ca","datavalue":{"value":{"entity-type":"item","numeric-id":4304492,"id":"Q4304492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$AAB74208-7E64-44AA-B7CF-89F6BDA5C869","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c865eb493d620b857070ca84d76d0aa56101b2f","datavalue":{"value":{"entity-type":"item","numeric-id":2947004,"id":"Q2947004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$1B3C5DF3-97F6-486F-9606-F9014831F6F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e70cc4453f5a873a7b64997b7df88ef8b7cf7b8a","datavalue":{"value":{"entity-type":"item","numeric-id":3613405,"id":"Q3613405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$9BEE5633-2891-495A-9468-5DA1A5038135","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2eaf1c8e5e649a3c59e663efd73652b24868feb","datavalue":{"value":{"entity-type":"item","numeric-id":4941840,"id":"Q4941840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$E2696C32-D16C-4CBE-8D8B-E92BCA1941DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"052ddb75aa13cdd2dbb8af5abd6bc30957b1530f","datavalue":{"value":{"entity-type":"item","numeric-id":3608774,"id":"Q3608774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$34983595-FFFF-48D7-B2A5-1C5EBD4BA416","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e01be3df09c8a3cb318e550873aba7f5df4fc2c","datavalue":{"value":{"entity-type":"item","numeric-id":2864358,"id":"Q2864358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$166DF041-CE9C-48EC-865C-98D3E3A8EF3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe638b8906f8f43ecb88c7284ff6ff2706007295","datavalue":{"value":{"entity-type":"item","numeric-id":2864524,"id":"Q2864524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$73DA5DE8-6620-4052-A082-0301B28B2D3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6386f9d9d555cce966644dfe59274fe1062f77ec","datavalue":{"value":{"entity-type":"item","numeric-id":5450569,"id":"Q5450569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$480683AC-6E98-45AB-9E70-C4EE1EE1DBA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52b18a75aad9c9a7a5a4368c62a0e4bea68bf145","datavalue":{"value":{"entity-type":"item","numeric-id":1041591,"id":"Q1041591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$F40E5EC9-9465-4F02-86CD-D1D730FADD14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cfc74a420b6b7ea54906573084cfacb776d08039","datavalue":{"value":{"entity-type":"item","numeric-id":3613431,"id":"Q3613431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$F2EF6651-5456-43A0-B740-7A712351FB97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67be0822f2ea25493074f855c573aed35f47e829","datavalue":{"value":{"entity-type":"item","numeric-id":673134,"id":"Q673134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$498F65D5-4BD0-46E2-9BF3-0D1D48A13CDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2ccbb30e3d39b99c4e0e0023e105dee668916c7","datavalue":{"value":{"entity-type":"item","numeric-id":5191095,"id":"Q5191095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$4FF29A30-C9D9-4690-BCDF-72563B4053E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f2b1ebc1ae7ffc3042b5e838a24da8662374478","datavalue":{"value":{"entity-type":"item","numeric-id":5898633,"id":"Q5898633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$AE98CA1C-0DF8-414B-8FD1-34C728D965D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f0b555d657cb1f5a17dad4f6c65786062114626","datavalue":{"value":{"entity-type":"item","numeric-id":2487870,"id":"Q2487870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$261D6871-6F31-426B-9883-6A5F8C9469C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d89f37ed0731c9210dbbb14b6045bcdc804d583","datavalue":{"value":{"entity-type":"item","numeric-id":5302032,"id":"Q5302032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$BAA33FFE-D0AB-422A-AA4E-6E69BC5274BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec28c2a46c17d6b0806fc14a11fc75ffc107a63d","datavalue":{"value":{"entity-type":"item","numeric-id":5191115,"id":"Q5191115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$E36590E8-2B14-4A87-8D7C-16E707E3FFAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$CA775E81-C435-47F1-A97F-7448CB3C213D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$FDCC2366-8B3B-4177-836E-C3CBCF758D68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$A48BBF02-1C1D-438E-9132-66F773F895E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a8f27245772c2159d3ccf93c502a4163695153f","datavalue":{"value":{"entity-type":"item","numeric-id":3541724,"id":"Q3541724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$CEDEB682-6C6F-4E42-9A27-2CE0F7061658","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":"Q438533$AFD08B1C-C2F2-46B9-BB42-33EF67E7C332","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"378088a63ec20245823db74d6a8845609e39ce21","datavalue":{"value":{"entity-type":"item","numeric-id":593789,"id":"Q593789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$4B7D016F-2788-48E2-BD5D-BF2216D9907D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b27d44a0e50fda314668a36654efb04ab5135cb3","datavalue":{"value":{"entity-type":"item","numeric-id":3868730,"id":"Q3868730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$A502E16A-DF5C-4333-8777-3661EF5902EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$C40B8684-1AD3-4585-850B-AC5696223400","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5c3c1d2d8bd223898d76726cee233eaf79c3109","datavalue":{"value":{"entity-type":"item","numeric-id":3655205,"id":"Q3655205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$0AF3AA30-FC70-475A-A5A7-CD69E3F4A797","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9741e06ce9f548b05466c57084eff41a74813bc1","datavalue":{"value":{"entity-type":"item","numeric-id":4033833,"id":"Q4033833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$607ADF7D-88FA-418C-BC6B-3B5B08BD4917","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d425524c539f34b2c20b8cfec23a758c1eb81a6","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$74E286D2-EBC2-451C-AB7A-AEF2F8675F7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db983e8102f84f2e9c46ae125c2043290b8a63d3","datavalue":{"value":{"entity-type":"item","numeric-id":3984438,"id":"Q3984438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$10240CEB-7686-4213-8394-044197748C5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bc614fe187bd0295ec729cf32cb3675e34b7b37","datavalue":{"value":{"entity-type":"item","numeric-id":4302847,"id":"Q4302847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$D43B3D2C-C684-465E-8751-444D7E125DAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aaaccfbedb3cd88fc80e0faeb16f71f2c3e7630","datavalue":{"value":{"entity-type":"item","numeric-id":5458332,"id":"Q5458332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$F75F54F5-C424-49C3-9026-2A545549C856","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":"Q438533$D9553E42-A9CE-4764-A21D-730412E3B4C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"817ee4f5358d83048f7143c1c798ef96590ad2ef","datavalue":{"value":{"entity-type":"item","numeric-id":3608415,"id":"Q3608415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$163AAB46-406A-4E6A-AD8A-1DDD004C17FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"985955d42b923cfa0515d9e4152c08273fc9f86a","datavalue":{"value":{"entity-type":"item","numeric-id":757095,"id":"Q757095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$648BDE0E-B115-47EE-9FD5-4797DBD934B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e698712dd6e8e21f17295141995a984511c4cd6","datavalue":{"value":{"entity-type":"item","numeric-id":5311278,"id":"Q5311278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$1D684536-A198-47AE-A22C-2818E9B9520E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5f146ef032705198a0202edddd0325ae6774f2a","datavalue":{"value":{"entity-type":"item","numeric-id":5716590,"id":"Q5716590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$45E7E27C-77E6-4B9B-9BC8-B6D3B1834638","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":"Q438533$5F24960D-7671-4CF9-9DD9-9EE918FC4209","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fefcfa398acb80ec88150255db1a4508f3ae3f73","datavalue":{"value":{"entity-type":"item","numeric-id":3655209,"id":"Q3655209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$176AC131-CB3C-4E51-8774-8614BAE66049","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f14878b4342799995051ac9bc54cd21c98efc98","datavalue":{"value":{"entity-type":"item","numeric-id":2751359,"id":"Q2751359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$32F8CAC8-7E54-402B-A61C-6DA0015C52E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febe5bf101c3b7d6dce19439eb466caa5715de79","datavalue":{"value":{"entity-type":"item","numeric-id":5624683,"id":"Q5624683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$EAAC0D8D-12B2-4305-8372-4759B05D8C63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db1af0fa3ab79d3aca7d0c2eb038f3a2d86af567","datavalue":{"value":{"entity-type":"item","numeric-id":5541351,"id":"Q5541351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$940B4353-BBFF-44F6-B207-0862E87A1717","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":"Q438533$1BBC5C52-B574-4B94-8708-131C33EF3C80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ebefb56013d1eec876e07a6ceb0c59107285c937","datavalue":{"value":{"entity-type":"item","numeric-id":757094,"id":"Q757094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$2750683C-F453-46ED-A8B6-69E36780D9BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b1ef4c8566673a8a5c94d00ea3fc5ee04078d8e","datavalue":{"value":{"entity-type":"item","numeric-id":3506045,"id":"Q3506045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$6DF606F3-9BA9-4FEB-A661-AFE59EC86A7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e5ac5e87b7bb20051a97cb3e5d95d9b6576112f","datavalue":{"value":{"entity-type":"item","numeric-id":689111,"id":"Q689111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$B2CF35AF-CD30-4D55-8A6B-8D1643AD44B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"97410c5f75f024969fa496104e5d0f6c8e839095","datavalue":{"value":{"entity-type":"item","numeric-id":5394615,"id":"Q5394615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$22E61188-8E61-45B0-BED6-6E9F84B904BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6405880c070588ef96205dbcc63ba1fa577e219e","datavalue":{"value":{"entity-type":"item","numeric-id":5446292,"id":"Q5446292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$8C95B3BF-F54D-4A75-8042-A387BA73076D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ecc80633033e33b0c5b134d43da0776fc1e27c25","datavalue":{"value":{"entity-type":"item","numeric-id":3655212,"id":"Q3655212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438533$9F9269D0-BBE2-4164-B559-66E3999E97E7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5f5c13164b896e8c60511d21059ba5553766f710","datavalue":{"value":"10.1007/S10817-010-9213-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438533$5E11C257-DD1C-44CE-BBAF-60FDFE4CE0B0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"53a028d76918394e54c3a6f9e22e703005b52a92","datavalue":{"value":{"entity-type":"item","numeric-id":5191095,"id":"Q5191095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"712e22a79d6315642598fa964effed7cf7deb5dd","datavalue":{"value":{"amount":"+0.8771726489067078","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":"Q438533$F196F819-1A05-4408-8280-B3871C59BFB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"060b299a48c3179c59c6541e6cf5829c59574c76","datavalue":{"value":{"entity-type":"item","numeric-id":5434475,"id":"Q5434475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b94f78948d6f1ee422a38dd716dce33a6d7aa90","datavalue":{"value":{"amount":"+0.770411491394043","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":"Q438533$71FF208E-5ECF-44D9-B190-93D282E3D41B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9390b4ccc6dc9f08d9ed8cd2d7f1eed1c352e9ee","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb4632759183624a07510d5b4ca064202d380ed3","datavalue":{"value":{"amount":"+0.7675321102142334","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":"Q438533$267EE46D-FF33-4D46-B516-6DCAFFFF10DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d8049f86ea2c26568ba10a8d60118f299b0d2eb7","datavalue":{"value":{"entity-type":"item","numeric-id":2351265,"id":"Q2351265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d957c7a51ae62befe60d1dbb35508f2f02e48651","datavalue":{"value":{"amount":"+0.7668371200561523","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":"Q438533$C85E7CD2-9088-4256-981B-16D7095CA7B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f10ee01b04bf937ea18106e6d39f383b6936577b","datavalue":{"value":{"entity-type":"item","numeric-id":4931590,"id":"Q4931590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71269937a234e236776a5868a5e6a6be8287671d","datavalue":{"value":{"amount":"+0.7661859393119812","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":"Q438533$C115E349-3CE8-4BF8-93F6-CA98D61FFDBB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On deciding satisfiability by theorem proving with speculative inferences","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_deciding_satisfiability_by_theorem_proving_with_speculative_inferences"}}}}}