s 4 7 9 12 15 16 18 22 25 27 34 37 40 43 46 49 50 55 58 61 64 67 68 73 76 79 80 85 88 91 94 97 100 t 4 6 8 11 15 17 21 23 26 29 34 37 40 43 46 49 50 55 56 57 60 64 66 67 68 73 75 78 80 85 91 94 99 c UNKNOWN a YES a 100 12 15 16 18 22 25 27 34 37 4 40 43 46 49 50 55 58 61 64 67 68 7 73 76 79 80 85 88 9 91 94 97 a 100 12 15 16 18 22 25 27 31 34 37 4 40 43 49 50 55 58 61 64 67 68 7 73 76 79 80 85 88 9 91 94 97 a 12 15 16 18 22 25 27 31 34 37 4 40 43 49 50 55 58 61 64 67 68 7 73 76 79 80 85 88 9 91 94 97 99 a 12 15 16 18 22 25 27 31 34 36 4 40 43 49 50 55 58 61 64 67 68 7 73 76 79 80 85 88 9 91 94 97 99 a 12 15 16 18 22 25 26 31 34 36 4 40 43 49 50 55 58 61 64 67 68 7 73 76 79 80 85 88 9 91 94 97 99 a 12 15 16 18 22 25 26 31 34 36 4 40 43 49 50 55 58 61 64 67 68 7 73 76 79 8 80 85 88 91 94 97 99 a 12 15 16 18 22 25 26 31 34 36 4 40 43 49 50 55 58 60 64 67 68 7 73 76 79 8 80 85 88 91 94 97 99 a 12 15 16 18 22 25 26 31 34 36 4 40 43 49 50 55 58 60 64 66 67 68 7 73 76 79 8 80 85 91 94 97 99 a 11 12 15 16 22 25 26 31 34 36 4 40 43 49 50 55 58 60 64 66 67 68 7 73 76 79 8 80 85 91 94 97 99 a 11 12 15 16 22 25 26 31 34 36 39 4 43 49 50 55 58 60 64 66 67 68 7 73 76 79 8 80 85 91 94 97 99 a 11 12 15 16 22 25 26 31 34 36 39 4 43 49 50 55 56 60 64 66 67 68 7 73 76 79 8 80 85 91 94 97 99 a 11 12 15 16 22 25 26 31 34 36 39 4 43 49 50 55 56 60 64 66 68 7 73 76 79 8 80 85 86 91 94 97 99 a 11 12 15 16 22 25 26 31 34 36 39 4 43 49 50 55 56 60 64 66 68 7 73 76 79 8 80 85 86 90 94 97 99 a 11 12 15 16 22 25 26 31 34 36 39 4 43 49 50 55 56 60 64 66 68 7 73 76 77 8 80 85 86 90 94 97 99 a 11 12 15 16 22 25 26 31 32 36 39 4 43 49 50 55 56 60 64 66 68 7 73 76 77 8 80 85 86 90 94 97 99 a 11 12 15 16 22 25 26 31 32 36 39 4 43 49 50 55 56 6 60 64 66 68 73 76 77 8 80 85 86 90 94 97 99 a 11 12 15 16 22 25 26 31 32 36 39 4 43 49 50 54 56 6 60 64 66 68 73 76 77 8 80 85 86 90 94 97 99 a 11 12 15 16 22 25 26 31 32 36 39 4 43 49 50 54 56 6 60 64 66 68 73 75 77 8 80 85 86 90 94 97 99 a 11 12 15 16 22 24 25 26 31 32 36 39 4 43 49 50 54 56 6 60 64 66 68 73 75 77 8 80 85 86 90 94 97 a 11 12 15 16 22 24 25 26 31 32 36 39 4 43 49 50 54 56 6 60 64 66 68 73 75 77 8 80 85 86 91 94 97 a 11 12 15 16 22 24 25 26 31 32 36 39 4 43 49 54 56 6 60 64 66 68 73 75 77 8 80 85 86 91 94 97 98 a 11 12 15 16 22 24 25 26 31 32 36 39 4 43 49 54 56 6 60 64 66 68 73 75 77 8 81 85 86 91 94 97 98 a 11 12 15 16 22 24 25 26 31 32 37 39 4 43 49 54 56 6 60 64 66 68 73 75 77 8 81 85 86 91 94 97 98 a 11 12 15 16 22 24 25 26 31 32 37 39 4 43 49 54 56 6 60 64 66 68 73 75 77 8 81 85 86 89 94 97 98 a 11 12 15 16 22 24 25 26 31 32 37 39 4 43 49 54 56 6 60 64 66 68 73 75 78 8 81 85 86 89 94 97 98 a 11 12 15 16 22 24 25 26 31 32 37 39 4 43 49 54 56 60 64 66 68 7 73 75 78 8 81 85 86 89 94 97 98 a 11 12 15 16 22 24 25 26 31 32 37 39 4 43 49 54 56 60 64 66 68 7 73 75 78 8 81 85 86 91 94 97 98 a 11 12 15 16 22 24 25 26 31 32 37 39 4 43 49 54 56 60 64 66 68 7 73 75 78 8 81 85 86 91 93 97 98 a 11 12 15 16 22 24 26 31 32 37 39 4 43 49 52 54 56 60 64 66 68 7 73 75 78 8 81 85 86 91 93 97 98 a 11 12 15 16 22 24 26 31 32 37 39 4 43 49 52 54 56 60 64 66 68 7 73 76 78 8 81 85 86 91 93 97 98 a 11 12 15 16 22 24 26 31 32 37 39 4 43 49 52 54 56 60 64 66 68 7 73 76 78 8 81 85 86 89 93 97 98 a 11 12 15 16 22 24 26 31 32 37 4 40 43 49 52 54 56 60 64 66 68 7 73 76 78 8 81 85 86 89 93 97 98 a 11 12 15 16 2 22 24 26 31 32 37 40 43 49 52 54 56 60 64 66 68 7 73 76 78 8 81 85 86 89 93 97 98 a 11 12 15 16 2 22 24 26 31 32 37 40 43 49 52 54 56 60 64 66 68 7 72 76 78 8 81 85 86 89 93 97 98 a 11 12 15 16 2 22 24 26 31 32 37 40 42 49 52 54 56 60 64 66 68 7 72 76 78 8 81 85 86 89 93 97 98 a 11 12 15 16 2 22 24 26 31 32 37 40 42 49 52 54 56 60 64 66 67 68 7 72 76 78 8 81 85 89 93 97 98 a 11 12 15 16 2 22 24 26 31 32 37 40 42 49 52 54 56 60 64 66 67 68 7 72 76 78 8 82 85 89 93 97 98 a 11 12 15 16 2 22 24 26 32 37 40 42 46 49 52 54 56 60 64 66 67 68 7 72 76 78 8 82 85 89 93 97 98 a 11 12 15 16 2 22 24 26 30 32 40 42 46 49 52 54 56 60 64 66 67 68 7 72 76 78 8 82 85 89 93 97 98 a 11 12 15 16 2 22 24 26 30 32 40 42 46 48 52 54 56 60 64 66 67 68 7 72 76 78 8 82 85 89 93 97 98 a 11 12 15 16 2 22 24 26 30 32 40 42 46 48 52 54 56 60 64 66 67 68 7 72 76 78 82 85 89 9 93 97 98 a 12 15 16 18 2 22 24 26 30 32 40 42 46 48 52 54 56 60 64 66 67 68 7 72 76 78 82 85 89 9 93 97 98 a 12 15 16 18 2 22 24 27 30 32 40 42 46 48 52 54 56 60 64 66 67 68 7 72 76 78 82 85 89 9 93 97 98 a 12 15 16 18 2 22 24 27 30 32 39 42 46 48 52 54 56 60 64 66 67 68 7 72 76 78 82 85 89 9 93 97 98 a 12 15 16 18 2 22 24 27 30 32 39 42 45 48 52 54 56 60 64 66 67 68 7 72 76 78 82 85 89 9 93 97 98 a 12 15 16 18 2 22 24 27 30 32 39 43 45 48 52 54 56 60 64 66 67 68 7 72 76 78 82 85 89 9 93 97 98 a 12 15 16 18 2 22 24 27 30 32 39 43 45 48 52 54 56 60 64 66 67 7 70 72 76 78 82 85 89 9 93 97 98 a 12 15 16 18 2 22 24 27 30 32 39 43 45 48 52 54 56 60 64 66 7 70 72 76 78 82 85 86 89 9 93 97 98 a 12 15 16 18 2 22 24 27 30 32 39 43 45 48 52 55 56 60 64 66 7 70 72 76 78 82 85 86 89 9 93 97 98 a 12 15 16 18 22 24 27 30 32 39 4 43 45 48 52 55 56 60 64 66 7 70 72 76 78 82 85 86 89 9 93 97 98 a 12 15 16 18 22 24 27 30 32 39 4 43 46 48 52 55 56 60 64 66 7 70 72 76 78 82 85 86 89 9 93 97 98 a 12 15 16 18 22 24 27 30 32 39 4 43 46 48 52 55 56 60 64 66 67 7 70 72 76 78 82 85 89 9 93 97 98 a 10 12 15 16 18 22 24 27 30 32 39 4 43 46 48 52 55 56 60 64 66 67 7 70 72 78 82 85 89 9 93 97 98 a 10 12 15 16 18 22 24 27 30 32 39 4 43 46 48 52 55 56 60 64 66 67 7 70 72 74 78 82 85 89 93 97 98 a 10 12 15 16 18 22 24 27 30 32 39 4 42 46 48 52 55 56 60 64 66 67 7 70 72 74 78 82 85 89 93 97 98 a 10 12 15 16 18 22 24 27 32 37 39 4 42 46 48 52 55 56 60 64 66 67 7 70 72 74 78 82 85 89 93 97 98 a 10 12 15 16 18 22 24 32 37 39 4 42 46 48 52 55 56 60 64 66 67 7 70 72 74 78 8 82 85 89 93 97 98 a 10 12 15 16 18 22 24 25 32 37 39 4 42 46 48 55 56 60 64 66 67 7 70 72 74 78 8 82 85 89 93 97 98 a 10 12 15 16 18 22 24 25 32 37 4 40 42 46 48 55 56 60 64 66 67 7 70 72 74 78 8 82 85 89 93 97 98 a 10 12 15 16 18 22 24 25 32 37 4 40 42 46 48 55 56 60 64 66 67 7 70 73 74 78 8 82 85 89 93 97 98 a 10 12 15 16 18 22 24 25 32 37 4 40 42 46 48 55 56 60 64 66 67 7 70 73 74 77 8 82 85 89 93 97 98 a 10 12 15 16 18 22 24 25 27 32 37 4 40 42 46 48 55 56 60 64 66 67 7 70 73 74 77 82 85 89 93 97 98 a 10 12 15 16 18 22 24 25 27 32 37 4 40 42 46 48 55 56 60 64 66 7 70 73 74 77 82 85 86 89 93 97 98 a 10 12 15 16 18 22 24 25 27 32 37 4 40 42 46 48 55 56 60 64 66 7 70 73 74 77 80 85 86 89 93 97 98 a 10 12 15 16 18 22 24 25 32 37 4 40 42 46 48 55 56 60 64 66 7 70 73 74 77 8 80 85 86 89 93 97 98 a 10 12 15 16 18 22 24 25 32 37 4 40 42 46 48 55 56 60 64 66 7 70 73 74 77 8 81 85 86 89 93 97 98 a 10 12 15 16 18 22 24 25 32 37 4 40 42 46 48 55 56 60 64 66 67 7 70 73 74 77 8 81 85 89 93 97 98 a 10 12 15 16 18 22 24 25 32 37 4 40 42 46 48 55 56 60 63 66 67 7 70 73 74 77 8 81 85 89 93 97 98 a 10 12 15 16 18 22 24 25 32 37 4 40 42 46 48 55 56 60 63 67 7 70 73 74 77 8 81 85 87 89 93 97 98 a 10 12 15 16 18 22 24 25 32 37 4 40 42 46 48 55 56 60 64 67 7 70 73 74 77 8 81 85 87 89 93 97 98 a 10 12 15 16 18 22 24 25 27 32 37 4 40 42 46 48 55 56 60 64 67 7 70 73 74 77 81 85 87 89 93 97 98 a 10 12 15 18 22 24 25 27 29 32 37 4 40 42 46 48 55 56 60 64 67 7 70 73 74 77 81 85 87 89 93 97 98 a 10 12 15 18 22 24 25 27 29 32 37 4 40 42 46 48 55 56 60 64 67 7 70 73 74 78 81 85 87 89 93 97 98 a 10 12 15 18 22 24 25 27 29 32 37 4 40 42 46 48 55 56 60 64 65 7 70 73 74 78 81 85 87 89 93 97 98 a 10 12 15 18 22 24 25 27 29 32 37 4 40 42 46 48 55 56 60 64 65 7 70 73 78 81 85 87 89 9 93 97 98 a 10 12 15 18 22 24 25 27 29 32 37 4 40 42 46 48 55 56 60 64 65 7 70 73 78 81 85 87 9 91 93 97 98 a 10 12 15 18 20 24 25 27 29 32 37 4 40 42 46 48 55 56 60 64 65 7 70 73 78 81 85 87 9 91 93 97 98 a 10 12 15 18 20 24 25 27 29 33 37 4 40 42 46 48 55 56 60 64 65 7 70 73 78 81 85 87 9 91 93 97 98 a 10 12 15 18 20 24 25 27 29 33 36 4 40 42 46 48 55 56 60 64 65 7 70 73 78 81 85 87 9 91 93 97 98 a 10 12 15 18 20 24 25 27 29 33 36 4 40 42 46 48 55 56 60 64 65 7 70 73 78 81 85 87 9 91 93 96 98 a 10 12 15 18 20 24 25 27 29 33 36 4 40 42 46 48 55 56 60 64 65 7 70 73 74 78 81 85 87 91 93 96 98 a 10 12 15 18 20 24 25 27 29 33 37 4 40 42 46 48 55 56 60 64 65 7 70 73 74 78 81 85 87 91 93 96 98 a 10 12 15 18 20 24 25 27 29 33 37 39 4 42 46 48 55 56 60 64 65 7 70 73 74 78 81 85 87 91 93 96 98 a 10 12 15 18 20 24 25 27 29 33 37 39 4 43 46 48 55 56 60 64 65 7 70 73 74 78 81 85 87 91 93 96 98 a 10 12 15 18 20 24 25 27 29 33 37 39 4 43 46 48 55 56 60 64 65 7 70 73 74 78 81 85 87 91 94 96 98 a 10 12 15 18 20 24 25 27 29 33 37 39 4 43 46 48 55 56 57 60 64 65 7 70 73 74 78 81 85 87 91 94 98 a 10 12 15 18 21 24 25 27 29 33 37 39 4 43 46 48 55 56 57 60 64 65 7 70 73 74 78 81 85 87 91 94 98 a 10 12 15 18 21 24 25 27 29 33 37 39 4 43 46 48 55 56 57 60 64 65 7 70 73 74 78 80 85 87 91 94 98 a 10 12 15 18 21 24 25 29 33 37 39 4 43 46 48 55 56 57 60 64 65 7 70 73 74 78 8 80 85 87 91 94 98 a 10 12 15 18 21 24 25 29 34 37 39 4 43 46 48 55 56 57 60 64 65 7 70 73 74 78 8 80 85 87 91 94 98 a 10 12 15 18 21 24 25 26 29 34 37 39 4 43 46 48 55 56 57 60 64 65 7 73 74 78 8 80 85 87 91 94 98 a 12 15 18 21 24 25 26 29 34 37 39 4 43 46 48 55 56 57 60 64 65 68 7 73 74 78 8 80 85 87 91 94 98 a 12 15 18 21 24 25 26 29 34 37 39 4 43 46 48 55 56 57 6 60 64 65 68 73 74 78 8 80 85 87 91 94 98 a 12 15 18 21 24 25 26 29 34 37 39 4 43 46 48 55 56 57 6 60 64 65 68 73 75 78 8 80 85 87 91 94 98 a 12 15 18 21 24 25 26 29 34 37 4 40 43 46 48 55 56 57 6 60 64 65 68 73 75 78 8 80 85 87 91 94 98 a 12 15 18 21 24 25 26 29 34 37 4 40 43 46 48 55 56 57 6 60 64 67 68 73 75 78 8 80 85 87 91 94 98 a 11 12 15 21 24 25 26 29 34 37 4 40 43 46 48 55 56 57 6 60 64 67 68 73 75 78 8 80 85 87 91 94 98 a 11 12 15 21 24 25 26 29 34 37 4 40 43 46 49 55 56 57 6 60 64 67 68 73 75 78 8 80 85 87 91 94 98 a 11 12 15 21 24 25 26 29 34 37 4 40 43 46 49 50 55 56 57 6 60 64 67 68 73 75 78 8 80 85 87 91 94 a 11 12 15 21 25 26 29 34 37 4 40 43 46 49 50 55 56 57 6 60 64 67 68 73 75 78 8 80 85 87 91 94 99 a 11 12 15 21 25 26 29 34 37 4 40 43 46 49 50 55 56 57 6 60 64 66 67 68 73 75 78 8 80 85 91 94 99 a 11 12 15 17 21 26 29 34 37 4 40 43 46 49 50 55 56 57 6 60 64 66 67 68 73 75 78 8 80 85 91 94 99 a 11 15 17 21 23 26 29 34 37 4 40 43 46 49 50 55 56 57 6 60 64 66 67 68 73 75 78 8 80 85 91 94 99 Command exited with non-zero status 65 Command being timed: "/Users/macpro/.pyenv/versions/anaconda3-2021.11/bin/clingo ../solver/core_compet2.lp -c core_stop="UNKNOWN" --stats --quiet=1,0 --time-limit=10800 ../encoding/isrpTJ_exact1_noloop_d1d2.lp ../../benchmark/3rd-benchmark/asp/mug100_25.lp ../../benchmark/3rd-benchmark/asp/mug100_25_01.lp" User time (seconds): 10793.50 System time (seconds): 9.79 Percent of CPU this job got: 99% Elapsed (wall clock) time (h:mm:ss or m:ss): 3:00:04 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 10219468 Average resident set size (kbytes): 0 Major (requiring I/O) page faults: 0 Minor (reclaiming a frame) page faults: 2899690 Voluntary context switches: 2 Involuntary context switches: 11046 Swaps: 0 File system inputs: 0 File system outputs: 0 Socket messages sent: 0 Socket messages received: 0 Signals delivered: 1 Page size (bytes): 4096 Exit status: 65