Created
July 21, 2015 08:54
-
-
Save catalin-hritcu/0d15fcd8d412c558cdb3 to your computer and use it in GitHub Desktop.
Profiling failing Z3 run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| unsat | |
| label_1270 | |
| (error "line 30061 column 16: model is not available") | |
| label_1271 | |
| (error "line 30063 column 16: model is not available") | |
| label_1272 | |
| (error "line 30065 column 16: model is not available") | |
| Done! | |
| [quantifier_instances] k!30037 : 1 : 1 : 2 | |
| [quantifier_instances] k!30026 : 1 : 1 : 2 | |
| [quantifier_instances] k!30009 : 3 : 3 : 4 | |
| [quantifier_instances] k!29992 : 1 : 3 : 4 | |
| unsat | |
| label_1278 | |
| (error "line 30182 column 16: model is not available") | |
| label_1279 | |
| (error "line 30184 column 16: model is not available") | |
| label_1280 | |
| (error "line 30186 column 16: model is not available") | |
| Done! | |
| unsat | |
| label_1283 | |
| (error "line 30263 column 16: model is not available") | |
| Done! | |
| unsat | |
| label_1299 | |
| (error "line 30442 column 16: model is not available") | |
| Done! | |
| [quantifier_instances] k!30425 : 1 : 1 : 2 | |
| [quantifier_instances] k!30408 : 1 : 1 : 2 | |
| [quantifier_instances] k!29901 : 4 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 2 : 3 | |
| [quantifier_instances] k!29901 : 3 : 10 : 11 | |
| [quantifier_instances] k!29901 : 6 : 10 : 11 | |
| [quantifier_instances] k!29901 : 6 : 10 : 11 | |
| [quantifier_instances] k!29901 : 5 : 10 : 11 | |
| [quantifier_instances] k!29901 : 4 : 6 : 6 | |
| unsat | |
| label_1334 | |
| (error "line 30898 column 16: model is not available") | |
| label_1339 | |
| (error "line 30900 column 16: model is not available") | |
| label_1338 | |
| (error "line 30902 column 16: model is not available") | |
| label_1337 | |
| (error "line 30904 column 16: model is not available") | |
| label_1340 | |
| (error "line 30906 column 16: model is not available") | |
| label_1333 | |
| (error "line 30908 column 16: model is not available") | |
| Done! | |
| [quantifier_instances] k!29901 : 9 : 10 : 11 | |
| [quantifier_instances] k!30801 : 45 : 11 : 11 | |
| [quantifier_instances] k!29901 : 2 : 7 : 7 | |
| [quantifier_instances] k!30421 : 40 : 11 : 12 | |
| [quantifier_instances] k!30725 : 3 : 3 : 4 | |
| [quantifier_instances] k!30708 : 1 : 3 : 4 | |
| [quantifier_instances] k!30668 : 7 : 0 : 1 | |
| [quantifier_instances] k!30638 : 3 : 3 : 4 | |
| [quantifier_instances] k!30616 : 1 : 3 : 4 | |
| [quantifier_instances] k!30601 : 20 : 4 : 5 | |
| [quantifier_instances] k!30421 : 3 : 5 : 6 | |
| [quantifier_instances] k!30421 : 1 : 5 : 6 | |
| [quantifier_instances] k!29901 : 5 : 10 : 11 | |
| unsat | |
| label_1364 | |
| (error "line 31393 column 16: model is not available") | |
| label_1363 | |
| (error "line 31395 column 16: model is not available") | |
| label_1369 | |
| (error "line 31397 column 16: model is not available") | |
| label_1368 | |
| (error "line 31399 column 16: model is not available") | |
| label_1367 | |
| (error "line 31401 column 16: model is not available") | |
| label_1378 | |
| (error "line 31403 column 16: model is not available") | |
| label_1377 | |
| (error "line 31405 column 16: model is not available") | |
| label_1376 | |
| (error "line 31407 column 16: model is not available") | |
| label_1375 | |
| (error "line 31409 column 16: model is not available") | |
| label_1379 | |
| (error "line 31411 column 16: model is not available") | |
| Done! | |
| [quantifier_instances] k!29901 : 9 : 8 : 9 | |
| [quantifier_instances] k!30421 : 10 : 8 : 9 | |
| [quantifier_instances] k!31123 : 38 : 10 : 11 | |
| [quantifier_instances] k!30421 : 34 : 8 : 9 | |
| [quantifier_instances] k!31201 : 3 : 2 : 3 | |
| [quantifier_instances] k!31176 : 25 : 3 : 4 | |
| [quantifier_instances] k!31153 : 18 : 3 : 4 | |
| [quantifier_instances] k!31099 : 10 : 0 : 1 | |
| [quantifier_instances] k!31077 : 3 : 3 : 4 | |
| [quantifier_instances] k!31060 : 1 : 3 : 4 | |
| [quantifier_instances] k!31045 : 1 : 2 : 3 | |
| [quantifier_instances] k!31020 : 15 : 0 : 1 | |
| [quantifier_instances] k!30990 : 3 : 3 : 4 | |
| [quantifier_instances] k!30968 : 1 : 3 : 4 | |
| unsat | |
| label_1396 | |
| (error "line 31669 column 16: model is not available") | |
| Done! | |
| unsat | |
| label_1412 | |
| (error "line 31891 column 16: model is not available") | |
| label_1411 | |
| (error "line 31893 column 16: model is not available") | |
| label_1410 | |
| (error "line 31895 column 16: model is not available") | |
| Done! | |
| [quantifier_instances] k!31833 : 3 : 3 : 4 | |
| [quantifier_instances] k!31814 : 3 : 3 : 4 | |
| [quantifier_instances] k!31795 : 3 : 3 : 4 | |
| unsat | |
| label_1420 | |
| (error "line 32025 column 16: model is not available") | |
| Done! | |
| unsat | |
| label_1433 | |
| (error "line 32191 column 16: model is not available") | |
| label_1432 | |
| (error "line 32193 column 16: model is not available") | |
| label_1431 | |
| (error "line 32195 column 16: model is not available") | |
| Done! | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 5 : 5 | |
| [quantifier_instances] k!29 : 1 : 6 : 6 | |
| [quantifier_instances] k!29 : 1 : 6 : 6 | |
| [quantifier_instances] k!29 : 1 : 6 : 6 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!30421 : 14 : 10 : 11 | |
| [quantifier_instances] k!30506 : 18 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 3 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 9 | |
| [quantifier_instances] k!29 : 6 : 8 : 8 | |
| [quantifier_instances] k!29 : 3 : 10 : 9 | |
| [quantifier_instances] k!29 : 6 : 8 : 8 | |
| [quantifier_instances] k!29 : 3 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 5 : 5 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 3 : 10 : 9 | |
| [quantifier_instances] k!29 : 8 : 6 : 4 | |
| [quantifier_instances] k!29 : 4 : 6 : 7 | |
| [quantifier_instances] k!29 : 8 : 6 : 6 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 7 : 6 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 8 : 6 : 5 | |
| [quantifier_instances] k!29 : 8 : 6 : 6 | |
| [quantifier_instances] k!29 : 8 : 7 : 4 | |
| [quantifier_instances] k!29 : 8 : 7 : 5 | |
| [quantifier_instances] k!29 : 8 : 7 : 6 | |
| [quantifier_instances] k!29 : 4 : 7 : 7 | |
| [quantifier_instances] k!29 : 8 : 6 : 5 | |
| [quantifier_instances] k!29 : 1 : 6 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 10 : 8 : 8 | |
| [quantifier_instances] k!29 : 8 : 6 : 4 | |
| [quantifier_instances] k!29 : 4 : 6 : 7 | |
| [quantifier_instances] k!29 : 4 : 7 : 5 | |
| [quantifier_instances] k!29 : 4 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!30421 : 11 : 10 : 11 | |
| [quantifier_instances] k!30506 : 14 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!30506 : 6 : 10 : 10 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 8 : 9 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 11 : 11 | |
| [quantifier_instances] k!30506 : 7 : 10 : 11 | |
| [quantifier_instances] k!30506 : 9 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30506 : 8 : 10 : 11 | |
| [quantifier_instances] k!30506 : 8 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 7 : 9 : 10 | |
| [quantifier_instances] k!30506 : 8 : 10 : 11 | |
| [quantifier_instances] k!30421 : 2 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!30421 : 30 : 9 : 10 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 7 : 9 : 10 | |
| [quantifier_instances] k!30421 : 5 : 10 : 11 | |
| [quantifier_instances] k!30506 : 6 : 10 : 9 | |
| [quantifier_instances] k!30421 : 6 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 23 : 10 : 11 | |
| [quantifier_instances] k!30506 : 37 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 12 : 10 : 11 | |
| [quantifier_instances] k!30506 : 29 : 10 : 11 | |
| [quantifier_instances] k!30421 : 5 : 10 : 11 | |
| [quantifier_instances] k!30506 : 7 : 10 : 10 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!30506 : 5 : 10 : 9 | |
| [quantifier_instances] k!30421 : 8 : 10 : 11 | |
| [quantifier_instances] k!30506 : 10 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!30421 : 8 : 10 : 11 | |
| [quantifier_instances] k!30506 : 10 : 10 : 11 | |
| [quantifier_instances] k!30421 : 5 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!30506 : 7 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 11 : 10 : 11 | |
| [quantifier_instances] k!30506 : 16 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 7 : 10 : 11 | |
| [quantifier_instances] k!30506 : 7 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!30421 : 8 : 10 : 11 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!30506 : 7 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!30421 : 12 : 10 : 11 | |
| [quantifier_instances] k!30506 : 12 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!30421 : 4 : 10 : 10 | |
| [quantifier_instances] k!30506 : 4 : 10 : 11 | |
| [quantifier_instances] k!30421 : 2 : 11 : 12 | |
| [quantifier_instances] k!30506 : 6 : 11 : 12 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!30506 : 5 : 10 : 11 | |
| [quantifier_instances] k!30421 : 5 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!30421 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!30421 : 12 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!30506 : 7 : 10 : 11 | |
| [quantifier_instances] k!30506 : 7 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!30421 : 24 : 9 : 10 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 3 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 11 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 8 : 7 : 4 | |
| [quantifier_instances] k!29 : 8 : 7 : 5 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 9 | |
| [quantifier_instances] k!29 : 4 : 11 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 5 : 10 : 8 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 5 : 10 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 5 : 10 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 5 : 10 : 8 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30506 : 6 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 68 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!30421 : 28 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!30421 : 8 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!30506 : 5 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!30421 : 5 : 10 : 11 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30506 : 6 : 10 : 11 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!30421 : 10 : 10 : 11 | |
| [quantifier_instances] k!30506 : 6 : 10 : 11 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!30421 : 6 : 10 : 11 | |
| [quantifier_instances] k!30421 : 2 : 10 : 11 | |
| [quantifier_instances] k!30506 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!30421 : 5 : 10 : 11 | |
| [quantifier_instances] k!30506 : 6 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 9 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 1 : 11 : 12 | |
| [quantifier_instances] k!30421 : 14 : 11 : 12 | |
| [quantifier_instances] k!30421 : 6 : 11 : 12 | |
| [quantifier_instances] k!30506 : 5 : 11 : 12 | |
| [quantifier_instances] k!30421 : 5 : 11 : 12 | |
| [quantifier_instances] k!30421 : 1 : 11 : 12 | |
| [quantifier_instances] k!30421 : 7 : 11 : 12 | |
| [quantifier_instances] k!30506 : 6 : 11 : 12 | |
| [quantifier_instances] k!30421 : 5 : 11 : 12 | |
| [quantifier_instances] k!30421 : 3 : 11 : 12 | |
| [quantifier_instances] k!30506 : 5 : 11 : 12 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30506 : 4 : 11 : 11 | |
| [quantifier_instances] k!30421 : 6 : 11 : 12 | |
| [quantifier_instances] k!30421 : 1 : 11 : 12 | |
| [quantifier_instances] k!30421 : 7 : 12 : 13 | |
| [quantifier_instances] k!30506 : 8 : 12 : 12 | |
| [quantifier_instances] k!30421 : 5 : 12 : 13 | |
| [quantifier_instances] k!30421 : 6 : 10 : 11 | |
| [quantifier_instances] k!30506 : 7 : 11 : 12 | |
| [quantifier_instances] k!30421 : 5 : 10 : 11 | |
| [quantifier_instances] k!30421 : 6 : 12 : 13 | |
| [quantifier_instances] k!30506 : 8 : 12 : 12 | |
| [quantifier_instances] k!30421 : 5 : 12 : 13 | |
| [quantifier_instances] k!30421 : 4 : 12 : 13 | |
| [quantifier_instances] k!30506 : 6 : 12 : 12 | |
| [quantifier_instances] k!30421 : 3 : 12 : 13 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 4 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 8 : 8 | |
| [quantifier_instances] k!30421 : 9 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 15 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 8 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30421 : 15 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 8 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30506 : 5 : 11 : 12 | |
| [quantifier_instances] k!29 : 5 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 10 | |
| [quantifier_instances] k!30421 : 31 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 6 : 7 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 11 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!30506 : 13 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 9 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!30506 : 14 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 7 : 6 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 8 | |
| [quantifier_instances] k!30506 : 104 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 8 | |
| [quantifier_instances] k!30506 : 26 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 9 : 8 | |
| [quantifier_instances] k!29 : 4 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 9 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!30421 : 12 : 10 : 11 | |
| [quantifier_instances] k!30506 : 16 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 6 : 11 : 10 | |
| [quantifier_instances] k!29 : 6 : 11 : 10 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 6 : 11 : 10 | |
| [quantifier_instances] k!30421 : 3 : 11 : 12 | |
| [quantifier_instances] k!30421 : 5 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 10 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 8 | |
| [quantifier_instances] k!29 : 2 : 10 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 9 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 8 | |
| [quantifier_instances] k!29 : 6 : 9 : 9 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!30421 : 9 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 9 : 8 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!30421 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!30421 : 15 : 11 : 12 | |
| [quantifier_instances] k!30506 : 17 : 11 : 12 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 10 : 10 : 10 | |
| [quantifier_instances] k!29 : 10 : 10 : 10 | |
| [quantifier_instances] k!29 : 5 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 9 : 8 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 9 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 10 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 5 : 10 : 10 | |
| [quantifier_instances] k!29 : 5 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 5 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 9 : 8 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 5 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 5 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 5 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 9 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 2 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!30421 : 1 : 10 : 10 | |
| [quantifier_instances] k!30421 : 1 : 10 : 10 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30506 : 2 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30506 : 2 : 10 : 11 | |
| [quantifier_instances] k!30506 : 2 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!30506 : 2 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30506 : 2 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30506 : 2 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!30421 : 7 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| unknown | |
| label_1444 | |
| (error "line 32396 column 16: model is not available") | |
| label_1443 | |
| (error "line 32398 column 16: model is not available") | |
| label_1442 | |
| (error "line 32400 column 16: model is not available") | |
| Done! | |
| [quantifier_instances] k!29 : 1 : 9 : 7 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30506 : 490 : 11 : 11 | |
| [quantifier_instances] k!30421 : 2 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 10 : 11 | |
| [quantifier_instances] k!29 : 6 : 10 : 11 | |
| [quantifier_instances] k!30506 : 70 : 10 : 11 | |
| [quantifier_instances] k!30506 : 858 : 12 : 12 | |
| [quantifier_instances] k!30506 : 663 : 11 : 12 | |
| [quantifier_instances] k!29 : 3 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!30421 : 4892 : 12 : 13 | |
| [quantifier_instances] k!30506 : 2858 : 12 : 13 | |
| [quantifier_instances] k!30421 : 2748 : 12 : 13 | |
| [quantifier_instances] k!30506 : 3241 : 12 : 13 | |
| [quantifier_instances] k!30421 : 4447 : 12 : 13 | |
| [quantifier_instances] k!29901 : 4119 : 12 : 13 | |
| [quantifier_instances] k!32314 : 4 : 12 : 13 | |
| [quantifier_instances] k!32304 : 1 : 1 : 2 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 5 : 5 | |
| [quantifier_instances] k!29 : 8 : 7 : 4 | |
| [quantifier_instances] k!29 : 8 : 7 : 5 | |
| [quantifier_instances] k!29 : 8 : 7 : 7 | |
| [quantifier_instances] k!29 : 8 : 7 : 6 | |
| [quantifier_instances] k!29 : 8 : 7 : 7 | |
| [quantifier_instances] k!29 : 8 : 7 : 4 | |
| [quantifier_instances] k!29 : 8 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 8 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 7 : 6 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 7 : 8 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 7 : 6 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 8 : 8 : 5 | |
| [quantifier_instances] k!29 : 8 : 8 : 7 | |
| [quantifier_instances] k!29 : 8 : 7 : 5 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 10 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 4 : 7 : 5 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 4 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 8 : 4 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 4 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 8 : 8 : 8 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 8 : 6 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 10 : 9 : 9 | |
| [quantifier_instances] k!29 : 10 : 9 : 8 | |
| [quantifier_instances] k!29 : 5 : 9 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 6 : 7 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 5 : 9 : 8 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 7 : 6 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 7 : 6 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 5 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 8 | |
| [quantifier_instances] k!29 : 2 : 7 : 8 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30506 : 8 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 5 : 5 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!30421 : 1 : 8 : 9 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 9 | |
| [quantifier_instances] k!29 : 6 : 10 : 9 | |
| [quantifier_instances] k!29 : 6 : 10 : 9 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 6 : 9 : 10 | |
| [quantifier_instances] k!30506 : 33 : 10 : 11 | |
| [quantifier_instances] k!30421 : 34 : 9 : 10 | |
| [quantifier_instances] k!30506 : 36 : 10 : 11 | |
| [quantifier_instances] k!30421 : 8 : 9 : 10 | |
| [quantifier_instances] k!30506 : 9 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 7 : 6 | |
| [quantifier_instances] k!30506 : 9 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!30506 : 9 : 9 : 9 | |
| [quantifier_instances] k!30421 : 16 : 9 : 10 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 5 : 5 | |
| [quantifier_instances] k!29 : 2 : 5 : 5 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 6 : 10 : 9 | |
| [quantifier_instances] k!29 : 6 : 10 : 9 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 10 : 9 | |
| [quantifier_instances] k!29 : 6 : 10 : 9 | |
| [quantifier_instances] k!29 : 6 : 10 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 9 : 10 | |
| [quantifier_instances] k!30421 : 2 : 9 : 10 | |
| [quantifier_instances] k!30421 : 2 : 9 : 10 | |
| [quantifier_instances] k!30421 : 2 : 9 : 10 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30506 : 5 : 10 : 11 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30506 : 6 : 10 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30506 : 5 : 10 : 11 | |
| [quantifier_instances] k!29 : 6 : 12 : 12 | |
| [quantifier_instances] k!30421 : 6 : 10 : 11 | |
| [quantifier_instances] k!30506 : 10 : 10 : 11 | |
| [quantifier_instances] k!29 : 6 : 12 : 12 | |
| [quantifier_instances] k!29 : 6 : 12 : 12 | |
| [quantifier_instances] k!29 : 6 : 12 : 12 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30506 : 5 : 10 : 11 | |
| [quantifier_instances] k!30421 : 6 : 10 : 11 | |
| [quantifier_instances] k!30421 : 2 : 10 : 11 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 3 : 10 : 11 | |
| [quantifier_instances] k!30506 : 5 : 10 : 11 | |
| [quantifier_instances] k!30421 : 6 : 10 : 11 | |
| [quantifier_instances] k!30421 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!30421 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30506 : 71 : 10 : 11 | |
| [quantifier_instances] k!30506 : 4 : 10 : 9 | |
| [quantifier_instances] k!30506 : 8 : 10 : 11 | |
| [quantifier_instances] k!30506 : 8 : 10 : 11 | |
| [quantifier_instances] k!30506 : 8 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!30506 : 20 : 10 : 11 | |
| [quantifier_instances] k!30506 : 4 : 10 : 9 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 6 : 6 | |
| [quantifier_instances] k!30506 : 13 : 10 : 11 | |
| [quantifier_instances] k!30506 : 14 : 10 : 11 | |
| [quantifier_instances] k!30506 : 11 : 10 : 11 | |
| [quantifier_instances] k!30506 : 11 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!30506 : 34 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!30506 : 100 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!30506 : 56 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!30506 : 16 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 7 : 7 | |
| [quantifier_instances] k!30506 : 39 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!30506 : 199 : 10 : 11 | |
| [quantifier_instances] k!30506 : 27 : 10 : 11 | |
| [quantifier_instances] k!30506 : 14 : 10 : 11 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!30506 : 12 : 10 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 9 : 9 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 3 : 9 : 9 | |
| [quantifier_instances] k!29 : 3 : 9 : 9 | |
| [quantifier_instances] k!29 : 3 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!30506 : 180 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 3 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 7 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 7 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 9 : 9 | |
| [quantifier_instances] k!29 : 6 : 9 : 9 | |
| [quantifier_instances] k!29 : 3 : 9 : 9 | |
| [quantifier_instances] k!29 : 3 : 9 : 9 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 6 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 3 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!30421 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 7 : 8 | |
| [quantifier_instances] k!29 : 3 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 11 | |
| [quantifier_instances] k!29 : 3 : 10 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 6 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 8 : 8 | |
| [quantifier_instances] k!30421 : 18 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 4 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| unknown | |
| label_1444 | |
| (error "line 32512 column 16: model is not available") | |
| label_1443 | |
| (error "line 32514 column 16: model is not available") | |
| label_1442 | |
| (error "line 32516 column 16: model is not available") | |
| Done! | |
| [quantifier_instances] k!29 : 3 : 10 : 11 | |
| [quantifier_instances] k!30421 : 3 : 11 : 12 | |
| [quantifier_instances] k!30506 : 11 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30506 : 1029 : 11 : 12 | |
| [quantifier_instances] k!30506 : 672 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 4 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!30421 : 3081 : 11 : 12 | |
| [quantifier_instances] k!30506 : 4736 : 11 : 12 | |
| [quantifier_instances] k!30421 : 3585 : 10 : 11 | |
| [quantifier_instances] k!30506 : 1103 : 10 : 11 | |
| [quantifier_instances] k!30421 : 4027 : 11 : 12 | |
| [quantifier_instances] k!29901 : 2097 : 11 : 12 | |
| [quantifier_instances] k!32430 : 4 : 11 : 12 | |
| [quantifier_instances] k!32420 : 1 : 1 : 2 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 4 | |
| [quantifier_instances] k!29 : 2 : 11 : 5 | |
| [quantifier_instances] k!29 : 2 : 11 : 6 | |
| [quantifier_instances] k!29 : 2 : 11 : 7 | |
| [quantifier_instances] k!29 : 2 : 11 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 5 : 5 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 7 : 5 | |
| [quantifier_instances] k!29 : 2 : 11 : 6 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 11 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 8 : 10 : 4 | |
| [quantifier_instances] k!29 : 8 : 10 : 5 | |
| [quantifier_instances] k!29 : 8 : 10 : 6 | |
| [quantifier_instances] k!29 : 8 : 10 : 7 | |
| [quantifier_instances] k!29 : 8 : 10 : 4 | |
| [quantifier_instances] k!29 : 8 : 10 : 5 | |
| [quantifier_instances] k!29 : 8 : 10 : 7 | |
| [quantifier_instances] k!29 : 8 : 11 : 11 | |
| [quantifier_instances] k!29 : 8 : 10 : 4 | |
| [quantifier_instances] k!29 : 8 : 11 : 5 | |
| [quantifier_instances] k!29 : 8 : 11 : 8 | |
| [quantifier_instances] k!29 : 8 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 10 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 6 | |
| [quantifier_instances] k!29 : 4 : 10 : 11 | |
| [quantifier_instances] k!29 : 4 : 11 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 8 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 9 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 4 : 11 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 11 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 9 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 8 | |
| [quantifier_instances] k!29 : 4 : 11 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 6 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 8 | |
| [quantifier_instances] k!29 : 1 : 11 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 11 : 8 | |
| [quantifier_instances] k!29 : 4 : 11 : 9 | |
| [quantifier_instances] k!29 : 4 : 11 : 10 | |
| [quantifier_instances] k!29 : 4 : 11 : 7 | |
| [quantifier_instances] k!29 : 4 : 11 : 7 | |
| [quantifier_instances] k!29 : 1 : 11 : 8 | |
| [quantifier_instances] k!29 : 4 : 11 : 10 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 11 : 9 | |
| [quantifier_instances] k!29 : 4 : 11 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 8 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 6 | |
| [quantifier_instances] k!29 : 4 : 11 : 10 | |
| [quantifier_instances] k!29 : 4 : 11 : 7 | |
| [quantifier_instances] k!29 : 1 : 11 : 8 | |
| [quantifier_instances] k!29 : 1 : 11 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 9 | |
| [quantifier_instances] k!29 : 4 : 11 : 9 | |
| [quantifier_instances] k!29 : 1 : 11 : 6 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 8 | |
| [quantifier_instances] k!29 : 4 : 11 : 6 | |
| [quantifier_instances] k!29 : 4 : 11 : 8 | |
| [quantifier_instances] k!29 : 4 : 11 : 8 | |
| [quantifier_instances] k!29 : 1 : 11 : 10 | |
| [quantifier_instances] k!29 : 4 : 11 : 9 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 7 | |
| [quantifier_instances] k!29 : 4 : 11 : 6 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 11 : 7 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 7 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 8 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 12 | |
| [quantifier_instances] k!29 : 4 : 11 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 11 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 8 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 11 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!29 : 4 : 12 : 12 | |
| [quantifier_instances] k!30421 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 2 : 11 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!30421 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 6 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 11 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 14 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 12 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!30421 : 3 : 9 : 10 | |
| [quantifier_instances] k!30506 : 3 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 3 : 11 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 3 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 14 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 14 : 13 | |
| [quantifier_instances] k!29 : 1 : 14 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 14 : 13 | |
| [quantifier_instances] k!29 : 1 : 14 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 14 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 14 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!30506 : 7 : 12 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 8 : 11 : 5 | |
| [quantifier_instances] k!29 : 8 : 11 : 8 | |
| [quantifier_instances] k!29 : 8 : 11 : 9 | |
| [quantifier_instances] k!29 : 8 : 11 : 10 | |
| [quantifier_instances] k!29 : 4 : 11 : 6 | |
| [quantifier_instances] k!29 : 4 : 11 : 11 | |
| [quantifier_instances] k!29 : 4 : 11 : 4 | |
| [quantifier_instances] k!29 : 4 : 11 : 4 | |
| [quantifier_instances] k!29 : 4 : 11 : 6 | |
| [quantifier_instances] k!29 : 4 : 11 : 7 | |
| [quantifier_instances] k!29 : 4 : 11 : 7 | |
| [quantifier_instances] k!29 : 1 : 13 : 14 | |
| [quantifier_instances] k!29 : 4 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 4 : 14 : 14 | |
| [quantifier_instances] k!29 : 4 : 14 : 14 | |
| [quantifier_instances] k!29 : 2 : 14 : 14 | |
| [quantifier_instances] k!29 : 2 : 14 : 14 | |
| [quantifier_instances] k!29 : 2 : 14 : 14 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 13 : 13 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 1 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!30421 : 2 : 10 : 11 | |
| [quantifier_instances] k!30506 : 3 : 10 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 3 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 11 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 12 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 13 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 14 | |
| [quantifier_instances] k!29 : 1 : 13 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 12 : 13 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 14 : 15 | |
| [quantifier_instances] k!29 : 1 : 15 : 15 | |
| [quantifier_instances] k!29 : 1 : 13 : 14 | |
| [quantifier_instances] k!29 : 1 : 15 : 15 | |
| [quantifier_instances] k!29 : 1 : 13 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 14 : 14 | |
| [quantifier_instances] k!29 : 1 : 15 : 15 | |
| [quantifier_instances] k!29 : 1 : 13 : 13 | |
| [quantifier_instances] k!29 : 1 : 15 : 15 | |
| [quantifier_instances] k!29 : 1 : 15 : 15 | |
| [quantifier_instances] k!29 : 1 : 15 : 15 | |
| unknown | |
| label_1444 | |
| (error "line 32628 column 16: model is not available") | |
| label_1443 | |
| (error "line 32630 column 16: model is not available") | |
| label_1442 | |
| (error "line 32632 column 16: model is not available") | |
| Done! | |
| [quantifier_instances] k!30506 : 1 : 12 : 13 | |
| [quantifier_instances] k!30421 : 37 : 13 : 13 | |
| [quantifier_instances] k!30421 : 3138 : 12 : 13 | |
| [quantifier_instances] k!30506 : 566 : 13 : 13 | |
| [quantifier_instances] k!30421 : 2054 : 10 : 11 | |
| [quantifier_instances] k!30506 : 557 : 12 : 13 | |
| [quantifier_instances] k!30421 : 2515 : 11 : 12 | |
| [quantifier_instances] k!29901 : 582 : 12 : 13 | |
| [quantifier_instances] k!32546 : 4 : 12 : 13 | |
| [quantifier_instances] k!32536 : 1 : 1 : 2 | |
| [quantifier_instances] k!29 : 2 : 5 : 5 | |
| [quantifier_instances] k!29 : 2 : 6 : 4 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 2 : 9 : 9 | |
| [quantifier_instances] k!29 : 1 : 10 : 11 | |
| [quantifier_instances] k!29 : 1 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 2 : 5 : 5 | |
| [quantifier_instances] k!29 : 1 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!29 : 2 : 12 : 12 | |
| [quantifier_instances] k!29 : 2 : 10 : 10 | |
| [quantifier_instances] k!29 : 2 : 11 : 11 | |
| [quantifier_instances] k!29 : 1 : 6 : 7 | |
| [quantifier_instances] k!29 : 1 : 10 : 10 | |
| [quantifier_instances] k!29 : 8 : 4 : 4 | |
| [quantifier_instances] k!30421 : 1 : 8 : 9 | |
| [quantifier_instances] k!30421 : 1 : 8 : 9 | |
| [quantifier_instances] k!30506 : 1 : 6 : 7 | |
| [quantifier_instances] k!30421 : 5 : 10 : 11 | |
| [quantifier_instances] k!30421 : 2 : 8 : 9 | |
| [quantifier_instances] k!30421 : 9 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 5 : 5 | |
| [quantifier_instances] k!29 : 1 : 6 : 6 | |
| [quantifier_instances] k!29 : 8 : 4 : 4 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!29 : 8 : 4 : 4 | |
| [quantifier_instances] k!30421 : 1 : 7 : 8 | |
| [quantifier_instances] k!30421 : 36 : 8 : 9 | |
| [quantifier_instances] k!30421 : 1 : 9 : 10 | |
| [quantifier_instances] k!29 : 2 : 5 : 5 | |
| [quantifier_instances] k!29 : 2 : 7 : 7 | |
| [quantifier_instances] k!30421 : 3 : 7 : 8 | |
| [quantifier_instances] k!30506 : 8 : 10 : 11 | |
| [quantifier_instances] k!30421 : 19 : 12 : 13 | |
| [quantifier_instances] k!29 : 2 : 6 : 6 | |
| [quantifier_instances] k!30421 : 13 : 8 : 9 | |
| [quantifier_instances] k!30421 : 6 : 12 : 13 | |
| [quantifier_instances] k!30421 : 7 : 8 : 9 | |
| [quantifier_instances] k!30421 : 6 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 7 : 8 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 7 : 8 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 11 : 12 | |
| [quantifier_instances] k!30421 : 5 : 11 : 12 | |
| [quantifier_instances] k!30421 : 5 : 7 : 8 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 7 : 8 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 4 : 7 : 8 | |
| [quantifier_instances] k!30421 : 4 : 8 : 9 | |
| [quantifier_instances] k!30421 : 4 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 6 : 8 : 9 | |
| [quantifier_instances] k!30421 : 6 : 8 : 9 | |
| [quantifier_instances] k!29 : 2 : 8 : 8 | |
| [quantifier_instances] k!30421 : 9 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 15 : 16 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!29 : 1 : 9 : 10 | |
| [quantifier_instances] k!30421 : 9 : 15 : 16 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 8 : 16 : 17 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 16 : 17 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 15 : 16 : 17 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 11 : 16 : 17 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 12 : 16 : 17 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 14 : 19 : 20 | |
| [quantifier_instances] k!30421 : 12 : 16 : 17 | |
| [quantifier_instances] k!30421 : 13 : 16 : 17 | |
| [quantifier_instances] k!30421 : 13 : 16 : 17 | |
| [quantifier_instances] k!30421 : 12 : 16 : 17 | |
| [quantifier_instances] k!30421 : 5 : 8 : 9 | |
| [quantifier_instances] k!30421 : 12 : 16 : 17 | |
| [quantifier_instances] k!30421 : 19 : 16 : 17 | |
| [quantifier_instances] k!30421 : 13 : 16 : 17 | |
| [quantifier_instances] k!30421 : 12 : 16 : 17 | |
| [quantifier_instances] k!30421 : 13 : 16 : 17 | |
| unknown | |
| label_1444 | |
| label_1444 | |
| label_1443 | |
| label_1443 | |
| label_1442 | |
| label_1442 | |
| Done! | |
| [quantifier_instances] k!30421 : 165 : 20 : 21 | |
| [quantifier_instances] k!30506 : 31 : 13 : 14 | |
| [quantifier_instances] k!30506 : 869 : 20 : 21 | |
| [quantifier_instances] k!30421 : 321 : 10 : 11 | |
| [quantifier_instances] k!30506 : 244 : 12 : 13 | |
| [quantifier_instances] k!30421 : 482 : 10 : 11 | |
| [quantifier_instances] k!30506 : 96 : 12 : 13 | |
| [quantifier_instances] k!30421 : 347 : 10 : 11 | |
| [quantifier_instances] k!29901 : 120 : 12 : 13 | |
| [quantifier_instances] k!32662 : 4 : 1 : 1 | |
| [quantifier_instances] k!32652 : 1 : 1 : 2 | |
| [quantifier_instances] k!30421 : 10157 : 11 : 12 | |
| [quantifier_instances] k!32286 : 19 : 7 : 8 | |
| [quantifier_instances] k!32267 : 19 : 7 : 8 | |
| [quantifier_instances] k!32248 : 19 : 7 : 8 | |
| [quantifier_instances] k!31938 : 8 : 1 : 2 | |
| [quantifier_instances] k!31927 : 8 : 1 : 2 | |
| [quantifier_instances] k!31764 : 27 : 0 : 1 | |
| [quantifier_instances] k!31755 : 27 : 0 : 1 | |
| [quantifier_instances] k!31733 : 18 : 7 : 8 | |
| [quantifier_instances] k!31716 : 1 : 7 : 8 | |
| [quantifier_instances] k!31702 : 123 : 8 : 9 | |
| [quantifier_instances] k!31590 : 165829 : 13 : 14 | |
| [quantifier_instances] k!31561 : 101482 : 13 : 14 | |
| [quantifier_instances] k!31549 : 47 : 1 : 2 | |
| [quantifier_instances] k!31539 : 218217 : 13 : 14 | |
| [quantifier_instances] k!31511 : 6465 : 10 : 11 | |
| [quantifier_instances] k!31500 : 6465 : 10 : 11 | |
| [quantifier_instances] k!31491 : 12 : 0 : 1 | |
| [quantifier_instances] k!31484 : 8393 : 10 : 11 | |
| [quantifier_instances] k!31464 : 195009 : 13 : 14 | |
| [quantifier_instances] k!31437 : 3106 : 11 : 12 | |
| [quantifier_instances] k!30537 : 1435 : 2 : 3 | |
| [quantifier_instances] k!30563 : 12 : 0 : 1 | |
| [quantifier_instances] k!30552 : 1435 : 2 : 3 | |
| [quantifier_instances] k!30541 : 22 : 7 : 8 | |
| [quantifier_instances] k!30524 : 1 : 7 : 8 | |
| [quantifier_instances] k!30510 : 3311 : 13 : 14 | |
| [quantifier_instances] k!30483 : 4058 : 14 : 15 | |
| [quantifier_instances] k!30466 : 1370 : 14 : 15 | |
| [quantifier_instances] k!30388 : 47 : 1 : 2 | |
| [quantifier_instances] k!30358 : 23 : 7 : 8 | |
| [quantifier_instances] k!30336 : 1 : 7 : 8 | |
| [quantifier_instances] k!30322 : 30045 : 15 : 16 | |
| [quantifier_instances] k!30281 : 9897 : 14 : 15 | |
| [quantifier_instances] k!29095 : 2776 : 13 : 14 | |
| [quantifier_instances] k!30238 : 892 : 14 : 15 | |
| [quantifier_instances] k!30227 : 12475 : 13 : 14 | |
| [quantifier_instances] k!30209 : 67 : 3 : 4 | |
| [quantifier_instances] k!30148 : 67 : 3 : 4 | |
| [quantifier_instances] k!30126 : 27 : 7 : 8 | |
| [quantifier_instances] k!30109 : 1 : 7 : 8 | |
| [quantifier_instances] k!30088 : 58 : 0 : 1 | |
| [quantifier_instances] k!29971 : 58 : 0 : 1 | |
| [quantifier_instances] k!29949 : 29 : 7 : 8 | |
| [quantifier_instances] k!29932 : 1 : 7 : 8 | |
| [quantifier_instances] k!29911 : 29 : 1 : 2 | |
| [quantifier_instances] k!29903 : 26 : 4 : 5 | |
| [quantifier_instances] k!29822 : 29 : 7 : 8 | |
| [quantifier_instances] k!29805 : 1 : 7 : 8 | |
| [quantifier_instances] k!29697 : 58 : 7 : 8 | |
| [quantifier_instances] k!29680 : 2 : 7 : 8 | |
| [quantifier_instances] k!29612 : 29 : 7 : 8 | |
| [quantifier_instances] k!29595 : 1 : 7 : 8 | |
| [quantifier_instances] k!29554 : 10 : 0 : 1 | |
| [quantifier_instances] k!29549 : 1 : 0 : 1 | |
| [quantifier_instances] k!29520 : 35 : 0 : 1 | |
| [quantifier_instances] k!29515 : 11 : 0 : 1 | |
| [quantifier_instances] k!29486 : 55795 : 20 : 21 | |
| [quantifier_instances] k!29481 : 55704 : 20 : 21 | |
| [quantifier_instances] k!29459 : 87 : 7 : 8 | |
| [quantifier_instances] k!29442 : 3 : 7 : 8 | |
| [quantifier_instances] k!29421 : 176907 : 18 : 19 | |
| [quantifier_instances] k!29407 : 204432 : 13 : 14 | |
| [quantifier_instances] k!29396 : 211989 : 13 : 14 | |
| [quantifier_instances] k!29384 : 1767 : 13 : 14 | |
| [quantifier_instances] k!29356 : 45 : 7 : 8 | |
| [quantifier_instances] k!29339 : 2 : 7 : 8 | |
| [quantifier_instances] k!29317 : 38966 : 13 : 14 | |
| [quantifier_instances] k!29309 : 23449 : 13 : 14 | |
| [quantifier_instances] k!29297 : 268302 : 14 : 15 | |
| [quantifier_instances] k!29280 : 283273 : 14 : 15 | |
| [quantifier_instances] k!29263 : 1999 : 14 : 15 | |
| [quantifier_instances] k!29227 : 29 : 7 : 8 | |
| [quantifier_instances] k!29206 : 1 : 7 : 8 | |
| [quantifier_instances] k!29183 : 50670 : 13 : 14 | |
| [quantifier_instances] k!29173 : 50408 : 13 : 14 | |
| [quantifier_instances] k!29163 : 31027 : 13 : 14 | |
| [quantifier_instances] k!29150 : 88214 : 18 : 19 | |
| [quantifier_instances] k!29139 : 92937 : 18 : 19 | |
| [quantifier_instances] k!29127 : 5804 : 19 : 20 | |
| [quantifier_instances] k!29099 : 314 : 13 : 14 | |
| [quantifier_instances] k!29082 : 2 : 13 : 14 | |
| [quantifier_instances] k!29060 : 8126 : 20 : 21 | |
| [quantifier_instances] k!29052 : 3956 : 20 : 21 | |
| [quantifier_instances] k!29040 : 217826 : 19 : 20 | |
| [quantifier_instances] k!28568 : 30 : 1 : 2 | |
| [quantifier_instances] k!28546 : 29 : 7 : 8 | |
| [quantifier_instances] k!28529 : 1 : 7 : 8 | |
| [quantifier_instances] k!28515 : 67 : 5 : 6 | |
| [quantifier_instances] k!28354 : 73844 : 20 : 21 | |
| [quantifier_instances] k!28263 : 58 : 7 : 8 | |
| [quantifier_instances] k!28242 : 2 : 7 : 8 | |
| [quantifier_instances] k!28100 : 58 : 7 : 8 | |
| [quantifier_instances] k!28079 : 2 : 7 : 8 | |
| [quantifier_instances] k!27986 : 1 : 7 : 8 | |
| [quantifier_instances] k!27938 : 1 : 7 : 8 | |
| [quantifier_instances] k!27897 : 1 : 7 : 8 | |
| [quantifier_instances] k!27849 : 29 : 7 : 8 | |
| [quantifier_instances] k!27828 : 1 : 7 : 8 | |
| [quantifier_instances] k!27250 : 29 : 7 : 8 | |
| [quantifier_instances] k!27158 : 1 : 7 : 8 | |
| [quantifier_instances] k!27020 : 29 : 7 : 8 | |
| [quantifier_instances] k!26933 : 1 : 7 : 8 | |
| [quantifier_instances] k!26800 : 29 : 7 : 8 | |
| [quantifier_instances] k!26718 : 1 : 7 : 8 | |
| [quantifier_instances] k!26590 : 29 : 7 : 8 | |
| [quantifier_instances] k!26513 : 1 : 7 : 8 | |
| [quantifier_instances] k!25853 : 29 : 7 : 8 | |
| [quantifier_instances] k!25780 : 1 : 7 : 8 | |
| [quantifier_instances] k!25439 : 29 : 7 : 8 | |
| [quantifier_instances] k!25348 : 1 : 7 : 8 | |
| [quantifier_instances] k!24851 : 29 : 7 : 8 | |
| [quantifier_instances] k!24790 : 1 : 7 : 8 | |
| [quantifier_instances] k!24687 : 29 : 7 : 8 | |
| [quantifier_instances] k!24630 : 1 : 7 : 8 | |
| [quantifier_instances] k!24531 : 29 : 7 : 8 | |
| [quantifier_instances] k!24478 : 1 : 7 : 8 | |
| [quantifier_instances] k!24090 : 29 : 7 : 8 | |
| [quantifier_instances] k!24040 : 1 : 7 : 8 | |
| [quantifier_instances] k!23796 : 29 : 7 : 8 | |
| [quantifier_instances] k!23735 : 1 : 7 : 8 | |
| [quantifier_instances] k!23388 : 29 : 7 : 8 | |
| [quantifier_instances] k!23350 : 1 : 7 : 8 | |
| [quantifier_instances] k!23274 : 29 : 7 : 8 | |
| [quantifier_instances] k!23239 : 1 : 7 : 8 | |
| [quantifier_instances] k!23029 : 29 : 7 : 8 | |
| [quantifier_instances] k!22996 : 1 : 7 : 8 | |
| [quantifier_instances] k!22831 : 29 : 7 : 8 | |
| [quantifier_instances] k!22793 : 1 : 7 : 8 | |
| [quantifier_instances] k!22494 : 29 : 7 : 8 | |
| [quantifier_instances] k!22438 : 1 : 7 : 8 | |
| [quantifier_instances] k!22311 : 29 : 7 : 8 | |
| [quantifier_instances] k!22255 : 1 : 7 : 8 | |
| [quantifier_instances] k!22128 : 29 : 7 : 8 | |
| [quantifier_instances] k!22072 : 1 : 7 : 8 | |
| [quantifier_instances] k!21945 : 29 : 7 : 8 | |
| [quantifier_instances] k!21889 : 1 : 7 : 8 | |
| [quantifier_instances] k!21762 : 29 : 7 : 8 | |
| [quantifier_instances] k!21706 : 1 : 7 : 8 | |
| [quantifier_instances] k!21579 : 29 : 7 : 8 | |
| [quantifier_instances] k!21523 : 1 : 7 : 8 | |
| [quantifier_instances] k!21396 : 29 : 7 : 8 | |
| [quantifier_instances] k!21340 : 1 : 7 : 8 | |
| [quantifier_instances] k!21213 : 29 : 7 : 8 | |
| [quantifier_instances] k!21157 : 1 : 7 : 8 | |
| [quantifier_instances] k!20110 : 29 : 7 : 8 | |
| [quantifier_instances] k!20054 : 1 : 7 : 8 | |
| [quantifier_instances] k!19539 : 29 : 7 : 8 | |
| [quantifier_instances] k!19455 : 1 : 7 : 8 | |
| [quantifier_instances] k!18369 : 29 : 7 : 8 | |
| [quantifier_instances] k!18318 : 1 : 7 : 8 | |
| [quantifier_instances] k!18201 : 29 : 7 : 8 | |
| [quantifier_instances] k!18150 : 1 : 7 : 8 | |
| [quantifier_instances] k!18033 : 29 : 7 : 8 | |
| [quantifier_instances] k!17982 : 1 : 7 : 8 | |
| [quantifier_instances] k!17865 : 29 : 7 : 8 | |
| [quantifier_instances] k!17814 : 1 : 7 : 8 | |
| [quantifier_instances] k!17697 : 29 : 7 : 8 | |
| [quantifier_instances] k!17646 : 1 : 7 : 8 | |
| [quantifier_instances] k!17529 : 29 : 7 : 8 | |
| [quantifier_instances] k!17478 : 1 : 7 : 8 | |
| [quantifier_instances] k!17361 : 29 : 7 : 8 | |
| [quantifier_instances] k!17310 : 1 : 7 : 8 | |
| [quantifier_instances] k!16458 : 29 : 7 : 8 | |
| [quantifier_instances] k!16407 : 1 : 7 : 8 | |
| [quantifier_instances] k!15963 : 29 : 7 : 8 | |
| [quantifier_instances] k!15888 : 1 : 7 : 8 | |
| [quantifier_instances] k!14996 : 29 : 7 : 8 | |
| [quantifier_instances] k!14950 : 1 : 7 : 8 | |
| [quantifier_instances] k!14843 : 29 : 7 : 8 | |
| [quantifier_instances] k!14797 : 1 : 7 : 8 | |
| [quantifier_instances] k!14690 : 29 : 7 : 8 | |
| [quantifier_instances] k!14644 : 1 : 7 : 8 | |
| [quantifier_instances] k!14537 : 29 : 7 : 8 | |
| [quantifier_instances] k!14491 : 1 : 7 : 8 | |
| [quantifier_instances] k!14384 : 29 : 7 : 8 | |
| [quantifier_instances] k!14338 : 1 : 7 : 8 | |
| [quantifier_instances] k!14231 : 29 : 7 : 8 | |
| [quantifier_instances] k!14185 : 1 : 7 : 8 | |
| [quantifier_instances] k!13508 : 29 : 7 : 8 | |
| [quantifier_instances] k!13462 : 1 : 7 : 8 | |
| [quantifier_instances] k!13085 : 29 : 7 : 8 | |
| [quantifier_instances] k!13019 : 1 : 7 : 8 | |
| [quantifier_instances] k!12301 : 29 : 7 : 8 | |
| [quantifier_instances] k!12260 : 1 : 7 : 8 | |
| [quantifier_instances] k!12163 : 29 : 7 : 8 | |
| [quantifier_instances] k!12122 : 1 : 7 : 8 | |
| [quantifier_instances] k!12025 : 29 : 7 : 8 | |
| [quantifier_instances] k!11984 : 1 : 7 : 8 | |
| [quantifier_instances] k!11887 : 29 : 7 : 8 | |
| [quantifier_instances] k!11846 : 1 : 7 : 8 | |
| [quantifier_instances] k!11749 : 29 : 7 : 8 | |
| [quantifier_instances] k!11708 : 1 : 7 : 8 | |
| [quantifier_instances] k!11186 : 29 : 7 : 8 | |
| [quantifier_instances] k!11145 : 1 : 7 : 8 | |
| [quantifier_instances] k!10831 : 29 : 7 : 8 | |
| [quantifier_instances] k!10774 : 1 : 7 : 8 | |
| [quantifier_instances] k!10210 : 29 : 7 : 8 | |
| [quantifier_instances] k!10174 : 1 : 7 : 8 | |
| [quantifier_instances] k!10087 : 29 : 7 : 8 | |
| [quantifier_instances] k!10051 : 1 : 7 : 8 | |
| [quantifier_instances] k!9964 : 29 : 7 : 8 | |
| [quantifier_instances] k!9928 : 1 : 7 : 8 | |
| [quantifier_instances] k!9841 : 29 : 7 : 8 | |
| [quantifier_instances] k!9805 : 1 : 7 : 8 | |
| [quantifier_instances] k!9418 : 29 : 7 : 8 | |
| [quantifier_instances] k!9382 : 1 : 7 : 8 | |
| [quantifier_instances] k!9127 : 29 : 7 : 8 | |
| [quantifier_instances] k!9079 : 1 : 7 : 8 | |
| [quantifier_instances] k!8649 : 29 : 7 : 8 | |
| [quantifier_instances] k!8618 : 1 : 7 : 8 | |
| [quantifier_instances] k!8541 : 29 : 7 : 8 | |
| [quantifier_instances] k!8510 : 1 : 7 : 8 | |
| [quantifier_instances] k!8433 : 29 : 7 : 8 | |
| [quantifier_instances] k!8402 : 1 : 7 : 8 | |
| [quantifier_instances] k!8130 : 29 : 7 : 8 | |
| [quantifier_instances] k!8099 : 1 : 7 : 8 | |
| [quantifier_instances] k!7899 : 29 : 7 : 8 | |
| [quantifier_instances] k!7860 : 1 : 7 : 8 | |
| [quantifier_instances] k!7544 : 29 : 7 : 8 | |
| [quantifier_instances] k!7518 : 1 : 7 : 8 | |
| [quantifier_instances] k!7451 : 58 : 7 : 8 | |
| [quantifier_instances] k!7425 : 2 : 7 : 8 | |
| [quantifier_instances] k!7248 : 29 : 7 : 8 | |
| [quantifier_instances] k!7222 : 1 : 7 : 8 | |
| [quantifier_instances] k!7073 : 29 : 7 : 8 | |
| [quantifier_instances] k!7043 : 1 : 7 : 8 | |
| [quantifier_instances] k!6796 : 58 : 7 : 8 | |
| [quantifier_instances] k!6779 : 2 : 7 : 8 | |
| [quantifier_instances] k!6733 : 12 : 7 : 8 | |
| [quantifier_instances] k!6697 : 1 : 7 : 8 | |
| [quantifier_instances] k!6281 : 29 : 7 : 8 | |
| [quantifier_instances] k!6260 : 1 : 7 : 8 | |
| [quantifier_instances] k!6139 : 29 : 7 : 8 | |
| [quantifier_instances] k!6118 : 1 : 7 : 8 | |
| [quantifier_instances] k!5997 : 29 : 7 : 8 | |
| [quantifier_instances] k!5976 : 1 : 7 : 8 | |
| [quantifier_instances] k!5769 : 87 : 7 : 8 | |
| [quantifier_instances] k!5748 : 3 : 7 : 8 | |
| [quantifier_instances] k!5640 : 29 : 7 : 8 | |
| [quantifier_instances] k!5619 : 1 : 7 : 8 | |
| [quantifier_instances] k!5496 : 29 : 7 : 8 | |
| [quantifier_instances] k!5475 : 1 : 7 : 8 | |
| [quantifier_instances] k!5352 : 29 : 7 : 8 | |
| [quantifier_instances] k!5331 : 1 : 7 : 8 | |
| [quantifier_instances] k!5163 : 29 : 7 : 8 | |
| [quantifier_instances] k!5137 : 1 : 7 : 8 | |
| [quantifier_instances] k!4935 : 29 : 7 : 8 | |
| [quantifier_instances] k!4909 : 1 : 7 : 8 | |
| [quantifier_instances] k!4654 : 58 : 7 : 8 | |
| [quantifier_instances] k!4628 : 2 : 7 : 8 | |
| [quantifier_instances] k!4495 : 29 : 7 : 8 | |
| [quantifier_instances] k!4469 : 1 : 7 : 8 | |
| [quantifier_instances] k!4306 : 29 : 7 : 8 | |
| [quantifier_instances] k!4280 : 1 : 7 : 8 | |
| [quantifier_instances] k!4080 : 29 : 7 : 8 | |
| [quantifier_instances] k!4059 : 1 : 7 : 8 | |
| [quantifier_instances] k!3831 : 58 : 7 : 8 | |
| [quantifier_instances] k!3810 : 2 : 7 : 8 | |
| [quantifier_instances] k!3705 : 29 : 7 : 8 | |
| [quantifier_instances] k!3684 : 1 : 7 : 8 | |
| [quantifier_instances] k!3586 : 29 : 7 : 8 | |
| [quantifier_instances] k!3569 : 1 : 7 : 8 | |
| [quantifier_instances] k!3343 : 29 : 7 : 8 | |
| [quantifier_instances] k!3326 : 1 : 7 : 8 | |
| [quantifier_instances] k!3194 : 58 : 7 : 8 | |
| [quantifier_instances] k!3177 : 2 : 7 : 8 | |
| [quantifier_instances] k!3103 : 29 : 7 : 8 | |
| [quantifier_instances] k!3086 : 1 : 7 : 8 | |
| [quantifier_instances] k!2979 : 29 : 7 : 8 | |
| [quantifier_instances] k!2958 : 1 : 7 : 8 | |
| [quantifier_instances] k!2829 : 29 : 7 : 8 | |
| [quantifier_instances] k!2808 : 1 : 7 : 8 | |
| [quantifier_instances] k!2751 : 29 : 7 : 8 | |
| [quantifier_instances] k!2730 : 1 : 7 : 8 | |
| [quantifier_instances] k!2502 : 58 : 7 : 8 | |
| [quantifier_instances] k!2481 : 2 : 7 : 8 | |
| [quantifier_instances] k!2356 : 29 : 7 : 8 | |
| [quantifier_instances] k!2331 : 1 : 7 : 8 | |
| [quantifier_instances] k!2215 : 29 : 7 : 8 | |
| [quantifier_instances] k!2198 : 1 : 7 : 8 | |
| [quantifier_instances] k!1432 : 15979 : 13 : 14 | |
| [quantifier_instances] k!1400 : 18655 : 20 : 21 | |
| [quantifier_instances] k!1343 : 5698 : 11 : 12 | |
| [quantifier_instances] k!1328 : 15990 : 13 : 14 | |
| [quantifier_instances] k!1256 : 32183 : 20 : 21 | |
| [quantifier_instances] k!1245 : 142 : 7 : 8 | |
| [quantifier_instances] k!1224 : 13894 : 20 : 21 | |
| [quantifier_instances] k!1218 : 15104 : 20 : 21 | |
| [quantifier_instances] k!1185 : 13 : 7 : 8 | |
| [quantifier_instances] k!1174 : 12 : 7 : 8 | |
| [quantifier_instances] k!1137 : 73447 : 20 : 21 | |
| [quantifier_instances] k!1024 : 14592 : 10 : 11 | |
| [quantifier_instances] k!1013 : 26548 : 20 : 21 | |
| [quantifier_instances] k!1007 : 14367 : 10 : 11 | |
| [quantifier_instances] k!651 : 1 : 0 : 1 | |
| [quantifier_instances] k!422 : 75 : 3 : 4 | |
| [quantifier_instances] k!406 : 320 : 3 : 4 | |
| [quantifier_instances] k!396 : 320 : 3 : 4 | |
| [quantifier_instances] k!386 : 320 : 3 : 4 | |
| [quantifier_instances] k!297 : 46751 : 20 : 21 | |
| [quantifier_instances] k!289 : 40490 : 20 : 21 | |
| [quantifier_instances] k!273 : 16514 : 20 : 21 | |
| [quantifier_instances] k!265 : 14935 : 20 : 21 | |
| [quantifier_instances] k!53 : 77462 : 19 : 20 | |
| [quantifier_instances] k!49 : 268096 : 20 : 21 | |
| [quantifier_instances] k!45 : 171225 : 20 : 21 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment