s 17 22 51 112 
t 36 51 85 119
c UNKNOWN
a YES
a 112 17 22 51
a 112 17 22 97
a 112 17 6 97
a 112 17 51 6
a 112 51 6 85
a 112 20 51 85
a 106 112 51 85
a 106 112 17 51
a 112 17 51 60
a 112 17 60 97
a 112 60 85 97
a 112 51 60 85
a 112 118 51 85
a 106 118 51 85
a 106 118 12 85
a 106 118 47 85
a 106 14 47 85
a 106 14 47 63
a 106 112 14 63
a 112 14 56 63
a 112 14 42 56
a 106 112 14 42
a 112 14 42 95
a 112 14 63 95
a 101 112 63 95
a 101 106 112 63
a 106 112 63 73
a 106 112 22 63
a 106 22 63 90
a 106 22 47 63
a 106 22 47 50
a 106 22 47 85
a 105 106 22 85
a 104 105 106 22
a 105 106 124 22
a 106 124 22 51
a 106 124 22 97
a 106 22 85 97
a 106 22 9 97
a 106 120 22 9
a 106 120 22 59
a 106 120 22 26
a 106 120 18 22
a 106 121 18 22
a 106 121 22 54
a 106 121 54 83
a 106 34 54 83
a 106 22 34 54
a 22 34 54 67
a 22 34 54 55
a 15 22 34 55
a 15 34 36 55
a 118 15 34 55
a 103 118 15 34
a 118 15 34 98
a 106 118 15 34
a 106 118 121 15
a 106 118 15 51
a 106 118 26 51
a 106 118 26 97
a 106 118 40 97
a 106 22 40 97
a 106 17 22 97
a 106 118 17 97
a 106 118 85 97
a 104 106 118 97
a 106 112 118 97
a 106 112 22 97
a 106 112 22 51
a 106 112 22 85
a 106 112 85 97
a 106 112 19 85
a 106 112 19 63
a 106 112 19 50
a 106 112 22 50
a 106 112 121 22
a 104 106 121 22
a 104 106 22 80
a 104 106 117 22
a 106 117 22 4
a 106 22 34 4
a 106 120 34 4
a 106 118 120 4
a 106 11 118 120
a 106 11 118 47
a 106 11 112 118
a 106 112 118 34
a 106 118 34 40
a 106 118 40 51
a 106 118 40 65
a 106 118 40 80
a 106 118 80 81
a 106 118 120 81
a 102 106 118 81
a 102 106 118 26
a 106 118 26 65
a 106 118 124 65
a 106 124 22 65
a 106 124 22 80
a 106 124 22 34
a 106 120 124 34
a 120 124 22 34
a 106 120 124 22
a 106 120 22 34
a 106 120 34 83
a 106 124 34 83
a 106 121 124 83
a 106 121 29 83
a 106 121 22 29
a 106 22 29 51
a 106 118 29 51
a 106 112 118 51
a 106 112 118 121
a 104 106 118 121
a 104 106 118 80
a 102 104 106 118
a 104 106 118 120
a 104 106 118 65
a 104 106 22 65
a 106 112 22 65
a 106 22 40 65
a 106 121 22 40
a 106 121 22 4
a 106 118 121 4
a 106 118 4 97
a 106 22 4 97
a 106 18 22 97
a 106 18 22 65
a 106 118 18 65
a 106 118 18 80
a 106 118 63 80
a 106 112 118 63
a 106 112 63 7
a 106 112 42 7
a 106 112 22 42
a 106 112 42 83
a 106 112 63 83
a 106 120 63 83
a 106 120 26 83
a 120 26 34 83
a 116 120 26 34
a 116 120 124 34
a 116 124 34 72
a 116 121 124 72
a 118 121 124 72
a 118 121 4 72
a 118 121 4 55
a 118 121 18 55
a 106 118 121 18
a 106 118 18 97
a 106 118 18 51
a 106 18 22 51
a 106 18 22 90
a 102 106 18 22
a 102 106 118 18
a 106 118 18 34
a 118 119 18 34
a 104 118 119 34
a 104 118 34 72
a 104 116 34 72
a 104 116 120 34
a 116 120 34 40
a 118 120 34 40
a 118 34 40 72
a 118 40 51 72
a 20 40 51 72
a 121 20 40 72
a 121 124 20 72
a 121 124 20 44
a 121 20 40 44
a 118 121 40 44
a 118 121 40 72
a 118 119 121 40
a 119 121 40 53
a 119 121 15 53
a 119 15 51 53
a 119 15 34 53
a 104 119 34 53
a 104 120 34 53
a 104 106 120 34
a 104 106 120 7
a 106 120 49 7
a 106 47 49 7
a 106 47 49 83
a 106 47 83 85
a 106 112 83 85
a 106 112 14 85
a 106 112 14 50
a 106 120 14 50
a 106 120 50 7
a 106 120 124 7
a 106 120 124 83
a 106 120 49 83
a 106 118 120 49
a 106 118 120 18
a 106 120 18 34
a 106 18 22 34
a 106 112 22 34
a 106 112 17 22
a 106 17 22 90
a 106 22 4 90
a 106 22 42 90
a 106 117 22 42
a 106 22 42 47
a 106 22 47 59
a 102 106 22 59
a 102 106 118 59
a 102 106 118 85
a 106 118 120 85
a 106 118 120 40
a 106 118 121 40
a 106 118 121 26
a 106 118 26 80
a 106 118 42 80
a 106 22 42 80
a 106 21 22 80
a 106 21 22 65
a 105 106 21 22
a 105 106 22 4
a 106 22 4 51
a 119 22 4 51
a 119 124 22 51
a 118 119 124 51
a 118 119 121 124
a 119 121 124 83
a 121 124 44 83
a 121 124 22 44
a 118 121 124 44
a 106 118 121 124
a 106 118 124 51
a 104 106 118 51
a 104 106 118 34
a 104 106 22 34
a 104 106 120 22
a 106 120 17 22
a 102 106 17 22
a 102 106 22 85
a 106 120 22 85
a 106 22 37 85
a 106 37 7 85
a 106 112 7 85
a 100 106 112 85
a 106 112 118 85
a 106 112 118 50
a 106 118 50 80
a 106 118 124 80
a 106 118 120 124
a 106 120 124 14
a 106 120 14 4
a 106 120 22 4
a 106 22 4 80
a 106 22 26 80
a 106 22 26 34
a 106 121 22 26
a 106 22 26 51
a 119 22 26 51
a 119 17 22 51
a 106 17 22 51
a 106 17 22 80
a 106 17 22 65
a 106 112 17 65
a 112 17 65 86
a 112 17 65 71
a 112 17 51 71
a 11 112 51 71
a 11 112 116 51
a 11 116 119 51
a 11 118 119 51
a 11 119 36 51
a 11 36 51 72
a 36 51 72 85
a 119 36 51 85
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/miles1500.lp ../../benchmark/3rd-benchmark/asp/miles1500_02.lp -c core_max=2982"
	User time (seconds): 10773.15
	System time (seconds): 57.05
	Percent of CPU this job got: 99%
	Elapsed (wall clock) time (h:mm:ss or m:ss): 3:00:30
	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): 28173804
	Average resident set size (kbytes): 0
	Major (requiring I/O) page faults: 0
	Minor (reclaiming a frame) page faults: 30174286
	Voluntary context switches: 3
	Involuntary context switches: 11458
	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