QMLTP-v1.1-comparison.txt ------------------------- test conditions: problem set: QMLTP-Library v 1.1 www.iltp.de/qmltp 600 problems 580 uni-modal (330 non-propositional, 170 propositional) 20 multi-modal (11 non-propositional, 9 propoisitional) Xeon 3.4 GHz, 4 GB RAM, Linux 2.6.24-24.x86_64 CPU time limit: 600 sec. date: 15 Jan 2012 standard semantics of first-order modal logic term conditions: designation: rigid, extension: local multi-modal logic: cumulative domains for all modalities 580 uni-modal first-order logic problems: ----------------------------------------- Theorems: Logic Domain- MleanCoP MleanTAP MleanSeP Satallax Leo II first2p_m 1.1+ GQML-Prover Condition 1.2 1.3 1.2 2.2 1.2.6 MSPASS 3.0 1.2 K varying - - - 104 73 - 58 cumulative - - 121 122 90 70 68 constant - - 124 146 120 67 82 D varying 179 100 - 113 82 - 51 cumulative 200 120 130 133 101 79 64 constant 217 134 135 160 135 76 73 T varying 224 138 - 170 121 - 78 cumulative 249 160 163 192 142 105 100 constant 269 175 166 213 175 95 101 S4 varying 274 169 - 207 142 - 87 cumulative 338 205 197 238 167 121 108 constant 352 220 197 261 202 111 121 S5 varying 359 219 - 248 171 - - cumulative 438 272 - 297 216 140 - constant 438 272 - 305 242 131 - Non-Theorems: Logic Domain- MleanCoP MleanTAP MleanSeP Satallax Leo II first2p_m 1.1+ GQML-Prover Condition 1.2 1.3 1.2 2.2 1.2.6 MSPASS 3.0 1.2 K varying - - - 134 - - - cumulative - - 4 122 - 159 - constant - - 1 118 - 122 - D varying 243 4 - 7 - - - cumulative 224 4 4 0 - 108 - constant 209 4 1 11 - 107 - T varying 145 4 - 102 - - - cumulative 125 4 4 90 - 89 - constant 112 4 1 84 - 89 - S4 varying 119 4 - 96 - - - cumulative 94 4 4 84 - 41 - constant 82 4 1 76 - 36 - S5 varying 88 4 - 79 - - - cumulative 41 4 - 51 - 37 - constant 41 4 - 55 - 29 - logic K, varying domains: ------------------------- Satallax Leo-II GQML-Prover 2.2 1.2 1.2 solved 238 73 58 (%) 41.0 12.6 10.0 proved 104 73 58 refuted 134 - - proved after 0-0.1 s 60 31 48 0.1-1 s 6 27 5 1 - 10 s 10 5 0 10- 100s 28 4 3 100-600s 0 6 2 time out >600s 342 495 227 average time (separ.) 2.7 19.3 12.3 SOTAC 0.78 0.42 0.71 SOTAC system rating 0.73 0.12 0.07 efficiency measure 0.15 0.01 0.01 proved only by this ATP-system 144 1 17 errors 0 12 295 stack overflow 0 3 4 segmentation fault 0 9 0 unknown 0 0 271 inconistent 0 0 20 logic K, cumulative domains: ---------------------------- MleanSeP Satallax Leo-II first2p_m 1.1+ GQML-Prover 1.2 2.2 1.2 MSPASS 3.0 1.2 solved 125 244 90 229 68 (%) 21.6 42.1 15.5 39.5 11.7 proved 121 122 90 70 68 refuted 4 122 - 159 - proved after 0-0.1 s 111 73 46 59 59 0.1-1 s 6 11 27 6 4 1 - 10 s 4 9 7 3 0 10- 100s 0 29 4 2 3 100-600s 0 0 6 0 2 time out >600s 424 335 481 52 230 average time 0.1 2.7 15.8 0.1 10.5 SOTAC 0.31 0.47 0.24 0.61 0.46 SOTAC system rating 0.14 0.32 0.09 0.30 0.06 efficiency measure 3.43 0.16 0.01 2.80 0.01 proved only by this ATP-system 2 37 0 85 7 mixed quantifiers 0 0 0 299 0 errors 31 1 9 0 282 stack overflow 31 1 1 0 0 segmentation fault 0 0 8 0 0 unknown 0 0 0 0 261 inconsistent 0 0 0 0 21 logic K, constant domains: MleanSeP Satallax Leo-II first2p_m 1.1+ GQML-Prover 1.2 2.2 1.2 MSPASS 3.0 1.2 solved 125 264 120 189 82 (%) 21.6 45.5 20.7 32.6 14.1 proved 124 146 120 67 82 refuted 1 118 - 122 - proved after 0-0.1 s 79 98 69 56 73 0.1-1 s 28 10 22 8 4 1 - 10 s 13 25 7 3 0 10- 100s 3 12 10 0 3 100-600s 1 1 12 0 2 time out >600s 421 316 451 81 229 average time 2.3 3.4 26.2 0.0 8.9 SOTAC 0.30 0.46 0.33 0.51 0.43 SOTAC system rating 0.14 0.35 0.13 0.24 0.08 efficiency measure 0.09 0.13 0.01 6.65 0.02 proved only by this ATP-system 2 36 12 40 11 mixed quantifiers 0 0 0 299 0 errors 34 0 9 11 269 stack overflow 34 0 0 11 0 segmentation fault 0 0 9 0 0 unknown 0 0 0 0 253 inconsistent 0 0 0 0 16 logic D, varying domains: ------------------------- MleanCoP MleanTAP Satallax Leo-II GQML-Prover 1.2 1.3 2.2 1.2 1.2 solved 422 104 120 82 51 (%) 72.8 17.9 20.7 14.1 8.8 proved 179 100 113 82 51 refuted 243 4 7 - - proved after 0-0.1 s 41 88 69 42 36 0.1-1 s 108 9 6 24 2 1 - 10 s 11 3 9 6 1 10- 100s 7 0 29 4 11 100-600s 12 0 0 6 1 time out >600s 158 473 459 490 222 average time 12.6 0.1 5.5 17.4 17.2 SOTAC 0.75 0.26 0.28 0.25 0.53 SOTAC system rating 0.56 0.10 0.12 0.07 0.02 efficiency measure 0.06 1.26 0.04 0.01 0.01 proved only by this ATP-system 264 0 0 1 1 errors 0 3 1 8 307 stack overflow 0 3 1 0 0 segmentation fault 0 0 0 8 0 unknown 0 0 0 0 275 inconsistent 0 0 0 0 32 logic D, cumulative domains: ---------------------------- MleanCoP MleanSeP MleanTAP Satallax Leo-II first2p_m 1.1+ GQML-Prover 1.2 1.2 1.3 2.2 1.2 MSPASS 3.0 1.2 solved 424 134 124 133 101 187 64 (%) 73.1 23.1 21.4 22.9 17.4 32.2 11.0 proved 200 130 120 133 101 79 64 refuted 224 4 4 - - 108 - proved after 0-0.1 s 41 99 108 82 49 68 50 0.1-1 s 128 27 9 12 34 6 2 1 - 10 s 12 4 3 10 7 3 1 10- 100s 7 0 0 29 5 2 11 100-600s 12 0 0 0 6 0 0 time out >600s 156 413 453 446 474 94 226 average time 12.6 0.1 0.1 5.0 14.5 0.2 13.1 SOTAC 0.60 0.20 0.20 0.19 0.17 0.45 0.35 SOTAC system rating 0.37 0.10 0.09 0.09 0.06 0.14 0.03 efficiency measure 0.06 2.20 1.80 0.05 0.01 1.85 0.01 proved only by this ATP-system 174 0 0 0 0 33 0 mixed quantifiers 0 0 0 0 0 299 0 errors 0 33 3 1 5 0 290 stack overflow 0 31 3 1 0 0 0 segmentation fault 0 2 0 0 5 0 0 unknown 0 0 0 0 0 0 265 inconsistent 0 0 0 0 0 0 25 logic D, constant domains: -------------------------- MleanCoP MleanSeP MleanTAP Satallax Leo-II first2p_m 1.1+ GQML-Prover 1.2 1.2 1.3 1.4 1.2 MSPASS 3.0 1.2 solved 426 135 139 171 135 183 73 (%) 73.4 23.3 24.0 29.5 23.3 31.6 12.6 proved 217 134 135 160 135 76 73 refuted 209 1 4 11 - 107 - proved after 0-0.1 s 57 88 123 104 78 66 59 0.1-1 s 130 13 9 16 28 7 2 1 - 10 s 11 28 3 27 8 3 1 10- 100s 7 3 0 12 10 0 11 100-600s 12 2 0 1 11 0 0 time out >600s 154 411 439 408 439 96 226 average time 12.5 4.8 0.1 5.3 22.9 0.0 11.5 SOTAC 0.56 0.19 0.20 0.21 0.21 0.45 0.31 SOTAC system rating 0.34 0.09 0.09 0.12 0.09 0.13 0.03 efficiency measure 0.06 0.05 2.28 0.06 0.01 7.02 0.01 proved only by this ATP-system 150 0 0 0 2 33 0 mixed quantifiers 0 0 0 0 0 299 0 errors 0 34 2 1 6 2 281 stack overflow 0 34 2 1 2 2 0 segmentation fault 0 0 0 0 4 0 0 unknown 0 0 0 0 0 0 258 inconsistent 0 0 0 0 0 0 23 logic T, varying domains: ------------------------- MleanCoP MleanTAP Satallax Leo-II GQML-Prover 1.2 1.3 2.2 1.2 1.2 solved 369 142 272 121 78 (%) 63.6 24.5 46.9 20.9 13.4 proved 224 138 170 121 78 refuted 145 4 102 - - proved after 0-0.1 s 70 124 96 70 70 0.1-1 s 129 9 22 30 3 1 - 10 s 10 5 22 10 2 10- 100s 9 0 29 5 2 100-600s 6 0 1 6 1 time out >600s 211 435 308 451 330 average time 6.6 0.1 3.4 12.2 2.3 SOTAC 0.54 0.26 0.40 0.23 0.40 SOTAC system rating 0.36 0.08 0.24 0.06 0.01 efficiency measure 0.10 2.07 0.14 0.02 0.06 proved only by this ATP-system 109 0 26 0 0 errors 0 3 0 8 172 stack overflow 0 3 0 2 0 segmentation fault 0 0 0 6 0 unknown 0 0 0 0 134 inconsistent 0 0 0 0 38 logic T, cumulative domains: ---------------------------- MleanCoP MleanSeP MleanTAP Satallax Leo-II first2p_m 1.1+ GQML-Prover 1.2 1.2 1.3 1.4 1.2 MSPASS 3.0 1.2 solved 374 167 164 282 142 194 100 (%) 64.5 28.8 28.3 48.6 24.5 33.4 17.2 proved 249 163 160 192 142 105 100 refuted 125 4 4 90 - 89 - proved after 0-0.1 s 73 144 148 111 90 92 90 0.1-1 s 150 12 9 24 31 6 3 1 - 10 s 11 6 3 17 9 3 2 10- 100s 9 1 0 40 6 2 2 100-600s 6 0 0 0 6 2 3 time out >600s 206 355 413 297 436 87 326 average time 6.6 0.6 0.1 3.4 11.3 2.6 4.7 SOTAC 0.42 0.19 0.19 0.28 0.18 0.32 0.29 SOTAC system rating 0.25 0.09 0.09 0.18 0.07 0.11 0.04 efficiency measure 0.10 0.46 3.10 0.14 0.02 0.13 0.04 proved only by this ATP-system 69 0 0 3 2 6 1 mixed quantifiers 0 0 0 0 0 299 0 errors 0 58 3 1 2 0 154 stack overflow 0 58 3 1 0 0 0 segmentation fault 0 0 0 0 2 0 0 unknown 0 0 0 0 0 0 121 inconsistent 0 0 0 0 0 0 33 logic T, constant domains: -------------------------- MleanCoP MleanSeP MleanTAP Satallax Leo-II first2p_m 1.1+ GQML-Prover 1.2 1.2 1.3 1.4 1.2 MSPASS 3.0 1.2 solved 381 167 179 297 175 184 111 (%) 65.7 28.8 30.9 51.2 30.2 31.7 19.1 proved 269 166 175 213 175 95 111 refuted 112 1 4 84 - 89 - proved after 0-0.1 s 59 113 163 138 106 89 101 0.1-1 s 179 35 9 22 34 4 3 1 - 10 s 12 10 3 32 13 1 2 10- 100s 10 7 0 20 11 0 2 100-600s 9 1 0 1 11 1 3 time out >600s 199 355 399 283 401 100 325 average time 11.0 2.5 0.1 3.8 17.9 0.8 4.2 SOTAC 0.39 0.18 0.19 0.27 0.21 0.31 0.28 SOTAC system rating 0.25 0.09 0.09 0.18 0.09 0.10 0.04 efficiency measure 0.06 0.11 3.72 0.14 0.02 0.38 0.05 proved only by this ATP-system 56 0 0 0 3 6 1 mixed quantifiers 0 0 0 0 0 299 0 errors 0 58 2 0 4 2 144 stack overflow 0 58 2 0 0 2 0 segmentation fault 0 0 0 0 4 0 0 unknown 0 0 0 0 0 0 113 inconsistent 0 0 0 0 0 0 31 logic S4, varying domains: -------------------------- MleanCoP MleanTAP Satallax Leo-II GQML-Prover 1.2 1.3 2.2 1.2 1.2 solved 393 173 303 142 87 (%) 67.8 29.8 52.2 24.5 15.0 proved 274 169 207 142 87 refuted 119 4 96 - - proved after 0-0.1 s 130 157 100 84 79 0.1-1 s 115 10 30 40 2 1 - 10 s 11 2 33 11 1 10- 100s 11 0 43 4 3 100-600s 7 0 1 3 2 time out >600s 187 404 276 426 353 average time 7.5 0.0 4.0 6.9 4.0 SOTAC 0.50 0.26 0.39 0.23 0.37 SOTAC system rating 0.33 0.10 0.24 0.06 0.00 efficiency measure 0.09 6.95 0.13 0.04 0.04 proved only by this ATP-system 98 1 27 0 0 errors 0 3 1 12 140 stack overflow 0 3 1 0 0 segmentation fault 0 0 0 12 0 unknown 0 0 0 0 103 inconsistent 0 0 0 0 37 logic S4, cumulative domains: ----------------------------- MleanCoP MleanSeP MleanTAP Satallax Leo-II first2p_m 1.1+ GQML-Prover 1.2 1.2 1.3 1.4 1.2 MSPASS 3.0 1.2 solved 432 201 209 322 167 162 108 (%) 74.5 34.7 36.0 55.5 28.8 27.9 18.6 proved 338 197 205 238 167 121 108 refuted 94 4 4 84 - 41 - proved after 0-0.1 s 132 139 193 114 75 107 99 0.1-1 s 154 13 9 38 68 8 3 1 - 10 s 18 32 2 32 12 3 0 10- 100s 21 6 1 53 7 3 5 100-600s 13 7 0 1 5 0 1 time out >600s 148 347 368 257 405 119 355 average time 13.0 13.5 0.4 5.6 11.3 0.4 4.6 SOTAC 0.45 0.19 0.21 0.28 0.17 0.25 0.24 SOTAC system rating 0.26 0.10 0.10 0.18 0.07 0.07 0.03 efficiency measure 0.06 0.03 0.85 0.10 0.03 0.77 0.04 proved only by this ATP-system 109 0 1 5 0 0 0 mixed quantifiers 0 0 0 0 0 299 0 errors 0 32 3 1 8 0 117 stack overflow 0 32 3 1 2 0 0 segmentation fault 0 0 0 0 6 0 0 unknown 0 0 0 0 0 0 92 inconsistent 0 0 0 0 0 0 25 logic S4, constant domains: --------------------------- MleanCoP MleanSeP MleanTAP Satallax Leo-II first2p_m 1.1+ GQML-Prover 1.2 1.2 1.3 1.4 1.2 MSPASS 3.0 1.2 solved 434 198 224 337 202 147 121 (%) 74.8 34.1 38.6 58.1 34.8 25.3 20.9 proved 352 197 220 261 202 111 121 refuted 82 1 4 76 - 36 - proved after 0-0.1 s 68 127 208 140 114 99 112 0.1-1 s 233 19 9 39 49 11 3 1 - 10 s 18 13 2 45 15 0 0 10- 100s 18 30 1 34 13 1 5 100-600s 15 8 0 3 11 0 1 time out >600s 146 350 354 243 376 132 351 average time 14.6 18.2 0.1 6.1 17.2 0.2 4.2 SOTAC 0.42 0.19 0.21 0.28 0.20 0.23 0.24 SOTAC system rating 0.25 0.09 0.11 0.19 0.09 0.06 0.04 efficiency measure 0.05 0.02 2.72 0.09 0.02 1.29 0.05 proved only by this ATP-system 90 0 1 3 2 0 0 errors 0 32 2 0 2 301 108 stack overflow 0 32 2 0 0 2 0 segmentation fault 0 0 0 0 2 0 0 mixed quantifiers 0 0 0 0 0 299 0 unknown 0 0 0 0 0 0 84 inconsistent 0 0 0 0 0 0 24 logic S5, varying domains: -------------------------- MleanCoP MleanTAP Satallax Leo-II 1.2 1.3 2.2 1.2 solved 447 223 327 171 (%) 77.1 38.4 56.4 29.5 proved 359 219 248 171 refuted 88 4 79 - proved after 0-0.1 s 113 206 110 100 0.1-1 s 194 9 51 41 1 - 10 s 23 4 34 16 10- 100s 16 0 50 8 100-600s 13 0 3 6 time out >600s 133 354 253 407 average time 13.3 0.1 5.9 10.8 SOTAC 0.54 0.29 0.39 0.26 SOTAC system rating 0.29 0.07 0.17 0.01 efficiency measure 0.06 5.56 0.10 0.03 proved only by this ATP-system 132 1 27 0 errors 0 3 0 2 stack overflow 0 3 0 0 segmentation fault 0 0 0 2 logic S5, cumulative domains: ----------------------------- MleanCoP MleanTAP Satallax Leo-II first2p_m 1.1+ 1.2 1.3 2.2 1.2 MSPASS 3.0 solved 479 276 348 216 177 (%) 82.6 47.6 60.0 37.2 30.5 proved 438 272 297 216 140 refuted 41 4 51 - 37 proved after 0-0.1 s 151 259 134 120 116 0.1-1 s 221 10 66 66 10 1 - 10 s 24 3 38 15 8 10- 100s 25 0 56 10 3 100-600s 17 0 3 5 3 time out >600s 101 302 232 363 104 average time 16.1 0.1 6.5 7.1 2.7 SOTAC 0.48 0.26 0.30 0.23 0.27 SOTAC system rating 0.27 0.12 0.17 0.08 0.05 efficiency measure 0.05 8.51 0.09 0.05 0.11 proved only by this ATP-system 126 1 0 0 0 mixed quantifiers 0 0 0 0 299 errors 0 2 0 1 0 stack overflow 0 2 0 0 0 segmentation fault 0 0 0 1 0 logic S5, constant domains: --------------------------- MleanCoP MleanTAP Satallax Leo-II first2p_m 1.1+ 1.2 1.3 2.2 1.2 MSPASS 3.0 solved 479 276 360 242 160 (%) 82.6 47.6 62.1 41.7 27.6 proved 438 272 305 242 131 refuted 41 4 55 - 29 proved after 0-0.1 s 191 259 153 145 114 0.1-1 s 181 10 60 57 5 1 - 10 s 24 3 53 14 9 10- 100s 25 0 36 14 1 100-600s 17 0 3 12 2 time out >600s 101 302 220 336 120 average time 16.1 0.1 5.2 15.4 4.1 SOTAC 0.47 0.26 0.30 0.25 0.26 SOTAC system rating 0.26 0.12 0.18 0.09 0.04 efficiency measure 0.05 8.68 0.12 0.03 0.07 proved only by this ATP-system 115 1 0 2 0 mixed quantifiers 0 0 0 0 299 errors 0 2 0 2 1 stack overflow 0 2 0 1 1 segmentation fault 0 0 0 1 0 20 multi-modal first-order logic problems: ----------------------------------------- Leo-II Satallax 1.2.6 2.2 solved 15 14 (%) 75.0 70.0 proved 15 14 refuted - 0 proved after 0 - 1 s 12 9 1 - 10 s 1 5 10- 100s 1 0 100-600s 1 0 time out >600s 5 6 average time in s 14.1 1.5 errors 0 0