PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:98.opb
MD5SUM	a89f4ed95903fddf213992506514bcf0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	16
Optimality of the best value was proved	NO
Number of terms in the objective function	906
Biggest coefficient in the objective function	553
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	2526
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	553
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	2526
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04184
Number of variables	906
Total number of constraints	1944
Number of constraints which are clauses	852
Number of constraints which are cardinality constraints (but not clauses)	1092
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 6468

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-14 05:10:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4883 boxname=wulflinc3 idbench=371 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a89f4ed95903fddf213992506514bcf0  /oldhome/oroussel/tmp/wulflinc3/normalized-10:20:4.5:0.95:98.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc3/normalized-10:20:4.5:0.95:98.opb /oldhome/oroussel/tmp/wulflinc3/normalized-10:20:4.5:0.95:98.opb
IDLAUNCH: 4883
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        835712 kB
Buffers:         36384 kB
Cached:         139248 kB
SwapCached:       3276 kB
Active:          83404 kB
Inactive:        98372 kB
HighTotal:      131008 kB
HighFree:         1064 kB
LowTotal:       903652 kB
LowFree:        834648 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11324 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:30:14 (client local time) WITH STATUS 10 IN 1200.13 SECONDS
stats: 4883 7 1200.13 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1038 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 187]---> BDD-cost:    5
c ---[ 186]---> BDD-cost:    8
c ---[ 185]---> BDD-cost:   14
c ---[ 184]---> BDD-cost:   14
c ---[ 183]---> BDD-cost:   17
c ---[ 182]---> BDD-cost:   14
c ---[ 181]---> BDD-cost:   23
c ---[ 180]---> BDD-cost:   20
c ---[ 179]---> BDD-cost:   29
c ---[ 178]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   38
c ---[ 176]---> BDD-cost:   32
c ---[ 175]---> BDD-cost:   32
c ---[ 174]---> BDD-cost:   23
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   20
c ---[ 171]---> BDD-cost:   20
c ---[ 170]---> BDD-cost:   14
c ---[ 169]---> BDD-cost:   14
c ---[ 168]---> BDD-cost:    8
c ---[ 167]---> BDD-cost:    8
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:   17
c ---[ 163]---> BDD-cost:   18
c ---[ 162]---> BDD-cost:   18
c ---[ 161]---> BDD-cost:   35
c ---[ 160]---> BDD-cost:   35
c ---[ 159]---> BDD-cost:   41
c ---[ 158]---> BDD-cost:   35
c ---[ 157]---> BDD-cost:   38
c ---[ 156]---> BDD-cost:   38
c ---[ 155]---> BDD-cost:   41
c ---[ 154]---> BDD-cost:   35
c ---[ 153]---> BDD-cost:   38
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   20
c ---[ 150]---> BDD-cost:   17
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:   11
c ---[ 145]---> BDD-cost:   14
c ---[ 144]---> BDD-cost:   17
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   29
c ---[ 141]---> BDD-cost:   41
c ---[ 140]---> BDD-cost:   44
c ---[ 139]---> BDD-cost:   44
c ---[ 138]---> BDD-cost:   38
c ---[ 137]---> BDD-cost:   39
c ---[ 136]---> BDD-cost:   41
c ---[ 135]---> BDD-cost:   44
c ---[ 134]---> BDD-cost:   44
c ---[ 133]---> BDD-cost:   41
c ---[ 132]---> BDD-cost:   29
c ---[ 131]---> BDD-cost:   29
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   26
c ---[ 128]---> BDD-cost:   14
c ---[ 127]---> BDD-cost:    8
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   14
c ---[ 124]---> BDD-cost:   17
c ---[ 123]---> BDD-cost:   21
c ---[ 122]---> BDD-cost:   29
c ---[ 121]---> BDD-cost:   35
c ---[ 120]---> BDD-cost:   44
c ---[ 119]---> BDD-cost:   47
c ---[ 118]---> BDD-cost:   44
c ---[ 117]---> BDD-cost:   44
c ---[ 116]---> BDD-cost:   44
c ---[ 115]---> BDD-cost:   41
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   35
c ---[ 112]---> BDD-cost:   32
c ---[ 111]---> BDD-cost:   29
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   20
c ---[ 108]---> BDD-cost:    6
c ---[ 107]---> BDD-cost:    5
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   20
c ---[ 104]---> BDD-cost:   23
c ---[ 103]---> BDD-cost:   26
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:   38
c ---[ 100]---> BDD-cost:   35
c ---[  99]---> BDD-cost:   41
c ---[  98]---> BDD-cost:   44
c ---[  97]---> BDD-cost:   41
c ---[  96]---> BDD-cost:   38
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:   38
c ---[  93]---> BDD-cost:   29
c ---[  92]---> BDD-cost:   20
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   20
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:    5
c ---[  87]---> BDD-cost:    5
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   20
c ---[  83]---> BDD-cost:   32
c ---[  82]---> BDD-cost:   41
c ---[  81]---> BDD-cost:   38
c ---[  80]---> BDD-cost:   35
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   35
c ---[  77]---> BDD-cost:   44
c ---[  76]---> BDD-cost:   35
c ---[  75]---> BDD-cost:   38
c ---[  74]---> BDD-cost:   35
c ---[  73]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   23
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   17
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   23
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   38
c ---[  60]---> BDD-cost:   32
c ---[  59]---> BDD-cost:   32
c ---[  58]---> BDD-cost:   35
c ---[  57]---> BDD-cost:   38
c ---[  56]---> BDD-cost:   32
c ---[  55]---> BDD-cost:   35
c ---[  54]---> BDD-cost:   29
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   29
c ---[  51]---> BDD-cost:   23
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   11
c ---[  47]---> BDD-cost:    8
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   20
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   35
c ---[  40]---> BDD-cost:   35
c ---[  39]---> BDD-cost:   35
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:   26
c ---[  36]---> BDD-cost:   23
c ---[  35]---> BDD-cost:   23
c ---[  34]---> BDD-cost:   23
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   17
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   20
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   20
c ---[  20]---> BDD-cost:   20
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   20
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    8
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:   14
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   14
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21969    61589 |    7323       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 823[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2188   maxlim: 597   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   37261   116202 |   12420       1        3     3.0 |  0.000 % |
c |       101 |   37261   116202 |   13662     101      306     3.0 |  2.534 % |
c |       252 |   37261   116202 |   15028     252      894     3.5 |  2.534 % |
c |       478 |   37261   116202 |   16531     478     2158     4.5 |  2.534 % |
c |       815 |   37261   116202 |   18184     815     4139     5.1 |  2.534 % |
c ==============================================================================
c [1mFound solution: 115[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1305   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1309 |   37257   116187 |   12419    1308     9157     7.0 |  2.534 % |
c |      1409 |   37257   116187 |   13660    1408    10189     7.2 |  2.599 % |
c |      1559 |   37257   116187 |   15026    1558    10866     7.0 |  2.599 % |
c |      1785 |   37257   116187 |   16529    1784    12149     6.8 |  2.599 % |
c |      2122 |   37257   116187 |   18182    2121    15256     7.2 |  2.599 % |
c |      2630 |   37257   116187 |   20000    2629    19173     7.3 |  2.599 % |
c |      3390 |   37257   116187 |   22001    3389    36575    10.8 |  2.599 % |
c ==============================================================================
c [1mFound solution: 99[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1321   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4396 |   37263   116217 |   12421    4395    50891    11.6 |  2.599 % |
c |      4496 |   37263   116217 |   13663    4495    51881    11.5 |  2.637 % |
c |      4647 |   37263   116217 |   15029    4646    56620    12.2 |  2.637 % |
c |      4873 |   37254   116186 |   16532    4868    58933    12.1 |  2.650 % |
c |      5210 |   37254   116186 |   18185    5205    64712    12.4 |  2.650 % |
c |      5716 |   37254   116186 |   20004    5711    86539    15.2 |  2.650 % |
c |      6475 |   37254   116186 |   22004    6470   112467    17.4 |  2.650 % |
c |      7615 |   37254   116186 |   24205    7610   150957    19.8 |  2.650 % |
c |      9324 |   37254   116186 |   26625    9319   221129    23.7 |  2.650 % |
c |     11886 |   37254   116186 |   29288   11881   410162    34.5 |  2.650 % |
c |     15731 |   37254   116186 |   32216   15726   731209    46.5 |  2.650 % |
c |     21498 |   37254   116186 |   35438   21493  1055274    49.1 |  2.650 % |
c |     30147 |   37254   116186 |   38982   30142  1758323    58.3 |  2.650 % |
c |     43121 |   37254   116186 |   42880   16566  1189418    71.8 |  2.650 % |
c |     62583 |   37254   116186 |   47168   36028  3527573    97.9 |  2.650 % |
c |     91775 |   37254   116186 |   51885   25134  2885785   114.8 |  2.650 % |
c |    135564 |   37254   116186 |   57074   26663  3820355   143.3 |  2.650 % |
c |    201250 |   37254   116186 |   62781   45430  8231858   181.2 |  2.650 % |
c |    299777 |   37254   116186 |   69059   42914  6863834   159.9 |  2.650 % |
c |    447566 |   37254   116186 |   75965   71822 10276571   143.1 |  2.650 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v785 -v740 v420 v82 -v860 -v744 v418 -v859 v784 v501 -v307 v85 -v788 -v419 v86 v63 -v861 -v504 -v424 v354 -v306 v62 v863 -v789 -v573 -v505 v64 v572 -v478 -v441 v353 -v312 v65 -v27 -v864 v574 -v477 -v310 -v102 v66 -v866 v810 v575 -v479 -v440 v359 -v262 -v185 -v101 -v73 -v26 -v867 v814 v576 v482 -v357 -v311 -v190 -v107 -v67 -v30 -v697 -v583 v481 -v446 -v399 -v315 -v265 -v216 -v189 v143 -v106 -v68 v701 v577 v486 -v444 -v358 -v266 v142 -v108 -v69 -v31 -v2 v578 v485 -v398 -v362 -v192 -v166 v144 v112 -v1 -v660 v579 v483 -v445 -v193 -v147 v111 -v7 v659 -v594 -v558 v484 -v449 -v404 -v196 -v165 v146 -v109 -v6 v661 -v598 -v557 -v402 -v194 v151 -v110 v8 v662 -v559 -v332 -v195 -v171 v150 v12 v663 v562 -v403 -v169 -v148 v11 v668 v561 -v407 -v335 -v149 v9 v664 v563 -v336 -v170 v10 -v739 v421 v81 -v855 -v743 -v854 v786 v500 -v425 -v302 v87 -v790 -v423 -v862 -v506 -v349 v308 v865 -v869 -v835 v792 -v436 v355 -v313 -v90 -v76 -v868 -v839 -v793 -v77 v809 -v586 v509 -v442 v360 -v316 -v261 -v212 -v72 -v28 v813 -v587 -v480 -v314 -v184 v103 -v32 -v696 -v582 v494 -v447 -v394 -v363 -v267 -v215 -v186 v104 -v70 v700 -v490 -v361 -v191 v105 -v580 -v489 v450 -v400 -v188 v161 -v116 -v34 -v448 -v197 v145 -v35 -v3 -v593 -v542 -v405 -v270 -v167 -v159 -v4 -v597 v155 v5 v671 -v408 -v331 v172 v154 -v16 v672 v560 -v406 v667 -v571 -v466 -v337 v173 v567 -v470 -v174 -v781 v741 -v496 v422 v83 -v745 -v426 v787 v502 v88 -v856 -v791 -v301 v857 v795 -v747 v507 -v303 -v91 -v75 v858 v794 -v748 -v348 v309 -v89 -v74 -v22 -v873 v834 -v761 -v585 v510 -v350 v305 -v257 -v21 -v838 -v765 -v584 v508 -v435 v356 -v317 v811 -v491 v437 v352 -v263 -v211 -v29 v815 -v493 v443 -v364 -v33 -v698 v439 -v268 -v217 -v119 -v71 -v37 v702 v451 v393 -v187 -v120 -v36 -v817 -v581 -v538 -v487 v395 -v271 -v205 -v156 -v115 -v818 v401 -v269 -v201 v160 -v158 -v704 -v670 -v595 -v541 -v488 v397 v327 -v220 -v200 v162 -v113 -v19 -v705 v669 -v599 -v409 -v168 v20 -v722 -v568 v333 v164 -v152 -v15 -v726 -v570 v175 v665 -v601 -v465 v338 -v153 v131 -v13 -v602 -v566 v469 v742 v434 v79 -v780 v746 -v495 v430 v84 v782 -v750 -v497 v429 v80 v783 -v749 v503 v92 -v876 v799 v499 -v877 -v805 v511 -v304 -v872 v836 -v804 -v760 v325 -v207 -v840 -v764 -v692 -v492 -v351 v321 -v256 -v23 -v884 -v870 v812 -v691 -v372 v320 -v258 -v213 -v118 -v24 -v888 v816 v438 -v368 v264 -v117 v25 -v842 -v820 v699 v459 -v367 v260 -v218 -v202 -v41 -v843 -v819 v703 -v589 -v455 v272 -v204 -v157 v707 -v588 -v537 -v454 -v221 -v18 v706 v396 -v219 -v17 -v596 -v543 v417 -v198 -v114 -v600 -v569 v413 v326 v163 -v721 v604 v412 v328 -v199 -v183 -v127 v725 v603 v334 -v179 v666 -v546 -v467 v330 -v178 v130 -v14 -v564 v471 -v339 v903 v433 v78 -v875 v802 -v754 v427 v100 -v874 -v830 v803 -v498 v96 v829 -v798 -v519 -v428 v322 v95 v515 v324 v837 -v796 v762 -v514 -v369 v841 -v806 -v766 -v371 -v206 -v883 -v871 v845 -v807 -v456 v318 -v291 -v208 -v44 -v887 v844 v808 -v693 v458 -v259 -v214 -v203 -v45 -v824 -v768 -v694 -v533 v383 -v365 v319 v280 -v210 -v40 -v769 v695 v276 -v222 -v711 -v619 v539 -v452 -v414 -v366 v275 -v38 -v623 -v590 v416 v591 -v544 -v453 -v180 v592 -v461 -v182 -v723 v608 v547 -v460 -v410 v126 v727 v545 v329 v468 -v411 -v347 -v176 v132 -v565 v472 -v343 v801 -v431 v97 v800 v99 -v753 v654 -v516 -v756 -v518 v323 -v755 -v751 -v521 v93 v831 -v525 -v370 v832 -v797 v763 -v512 -v287 -v249 -v94 -v43 v833 v767 -v457 -v42 -v885 v849 v827 v771 -v513 -v379 -v290 -v277 v889 v828 v770 v279 -v209 -v823 -v714 v382 -v230 v715 -v532 -v415 -v226 -v891 -v821 -v710 -v641 -v618 v534 v273 -v225 -v39 -v892 v717 v645 -v622 v540 -v181 v716 -v708 -v679 -v611 v536 v274 v122 -v55 -v683 v612 v548 -v724 v607 -v344 v128 v728 v462 -v346 v729 v605 v463 -v240 -v177 v133 v730 v464 -v342 v904 -v432 v98 -v517 v653 -v752 v520 -v245 -v879 -v757 v524 -v878 -v852 v826 v758 -v286 -v248 -v853 v825 v759 -v278 -v886 v848 v775 -v713 -v378 -v292 -v227 v890 -v712 -v229 v894 v846 v384 v893 -v822 -v640 -v620 -v610 -v295 -v223 -v51 v644 -v624 -v609 v535 -v709 -v678 v556 -v387 -v224 -v54 v718 -v682 v552 -v345 v121 v719 v626 v551 -v236 v123 v720 v627 v129 v734 v606 -v4#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.93 2/54 20416
Raw data (stat): 20416 (runsolver) R 20415 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423737881 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 2637 0 0 0 993 6 0 0 25 0 1 0 423737881 12455936 2489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3041 2489 603 41 0 3000 0
vsize: 12164
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 3452 0 0 0 1991 7 0 0 25 0 1 0 423737881 15859712 3304 4294967295 134512640 134672761 3221224544 3221223648 134560483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3872 3304 603 41 0 3831 0
vsize: 15488
[startup+30.0025 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 4299 0 0 0 2988 10 0 0 25 0 1 0 423737881 19480576 4151 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4756 4151 603 41 0 4715 0
vsize: 19024
[startup+40.0028 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 4958 0 0 0 3985 13 0 0 25 0 1 0 423737881 22167552 4810 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5412 4810 603 41 0 5371 0
vsize: 21648
[startup+50.0041 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 4970 0 0 0 4985 13 0 0 25 0 1 0 423737881 22167552 4822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5412 4822 603 41 0 5371 0
vsize: 21648
[startup+60.005 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 4970 0 0 0 5984 14 0 0 25 0 1 0 423737881 22167552 4822 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5412 4822 603 41 0 5371 0
vsize: 21648
[startup+70.0053 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 5631 0 0 0 6982 16 0 0 25 0 1 0 423737881 24850432 5483 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6067 5483 603 41 0 6026 0
vsize: 24268
[startup+80.0057 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 6640 0 0 0 7980 18 0 0 25 0 1 0 423737881 29024256 6492 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7086 6492 603 41 0 7045 0
vsize: 28344
[startup+90.0065 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 7542 0 0 0 8977 21 0 0 25 0 1 0 423737881 32653312 7394 4294967295 134512640 134672761 3221224544 3221223696 134565213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7972 7394 603 41 0 7931 0
vsize: 31888
[startup+100.007 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 8003 0 0 0 9975 22 0 0 25 0 1 0 423737881 34525184 7855 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7855 603 41 0 8388 0
vsize: 33716
[startup+110.008 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 8004 0 0 0 10975 23 0 0 25 0 1 0 423737881 34525184 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7856 603 41 0 8388 0
vsize: 33716
[startup+120.009 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 8004 0 0 0 11974 23 0 0 25 0 1 0 423737881 34525184 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7856 603 41 0 8388 0
vsize: 33716
[startup+130.008 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 8004 0 0 0 12974 23 0 0 25 0 1 0 423737881 34525184 7856 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7856 603 41 0 8388 0
vsize: 33716
[startup+140.009 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 8004 0 0 0 13973 24 0 0 25 0 1 0 423737881 34525184 7856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7856 603 41 0 8388 0
vsize: 33716
[startup+150.01 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 8004 0 0 0 14973 24 0 0 25 0 1 0 423737881 34525184 7856 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7856 603 41 0 8388 0
vsize: 33716
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 8310 0 0 0 15971 26 0 0 25 0 1 0 423737881 35733504 8162 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8724 8162 603 41 0 8683 0
vsize: 34896
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 9036 0 0 0 16969 28 0 0 25 0 1 0 423737881 38821888 8888 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9478 8888 603 41 0 9437 0
vsize: 37912
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 9096 0 0 0 17968 29 0 0 25 0 1 0 423737881 38957056 8948 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9511 8948 603 41 0 9470 0
vsize: 38044
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 9096 0 0 0 18967 29 0 0 25 0 1 0 423737881 38957056 8948 4294967295 134512640 134672761 3221224544 3221223560 1075353070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9511 8948 603 41 0 9470 0
vsize: 38044
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 9096 0 0 0 19967 29 0 0 25 0 1 0 423737881 38957056 8948 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9511 8948 603 41 0 9470 0
vsize: 38044
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 9096 0 0 0 20967 29 0 0 25 0 1 0 423737881 38957056 8948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9511 8948 603 41 0 9470 0
vsize: 38044
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 9096 0 0 0 21967 30 0 0 25 0 1 0 423737881 38957056 8948 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9511 8948 603 41 0 9470 0
vsize: 38044
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 9096 0 0 0 22966 30 0 0 25 0 1 0 423737881 38957056 8948 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9511 8948 603 41 0 9470 0
vsize: 38044
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 9424 0 0 0 23964 32 0 0 25 0 1 0 423737881 40300544 9276 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9839 9276 603 41 0 9798 0
vsize: 39356
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 10236 0 0 0 24961 35 0 0 25 0 1 0 423737881 43667456 10088 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10661 10088 603 41 0 10620 0
vsize: 42644
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 10875 0 0 0 25959 38 0 0 25 0 1 0 423737881 46350336 10727 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11316 10727 603 41 0 11275 0
vsize: 45264
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 11421 0 0 0 26957 39 0 0 25 0 1 0 423737881 48480256 11273 4294967295 134512640 134672761 3221224544 3221223704 134542657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 11273 603 41 0 11795 0
vsize: 47344
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 11421 0 0 0 27956 40 0 0 25 0 1 0 423737881 48480256 11273 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 11273 603 41 0 11795 0
vsize: 47344
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 11421 0 0 0 28956 40 0 0 25 0 1 0 423737881 48480256 11273 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 11273 603 41 0 11795 0
vsize: 47344
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 11421 0 0 0 29956 40 0 0 25 0 1 0 423737881 48480256 11273 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 11273 603 41 0 11795 0
vsize: 47344
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 11421 0 0 0 30956 40 0 0 25 0 1 0 423737881 48480256 11273 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 11273 603 41 0 11795 0
vsize: 47344
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 11421 0 0 0 31955 41 0 0 25 0 1 0 423737881 48480256 11273 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 11273 603 41 0 11795 0
vsize: 47344
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 11421 0 0 0 32955 41 0 0 25 0 1 0 423737881 48480256 11273 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 11273 603 41 0 11795 0
vsize: 47344
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 11421 0 0 0 33955 41 0 0 25 0 1 0 423737881 48480256 11273 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 11273 603 41 0 11795 0
vsize: 47344
[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 11421 0 0 0 34955 41 0 0 25 0 1 0 423737881 48480256 11273 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 11273 603 41 0 11795 0
vsize: 47344
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 11421 0 0 0 35955 41 0 0 25 0 1 0 423737881 48480256 11273 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11836 11273 603 41 0 11795 0
vsize: 47344
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 12245 0 0 0 36952 43 0 0 25 0 1 0 423737881 51830784 12097 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12654 12097 603 41 0 12613 0
vsize: 50616
[startup+380.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 12998 0 0 0 37951 45 0 0 25 0 1 0 423737881 54927360 12850 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12850 603 41 0 13369 0
vsize: 53640
[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13651 0 0 0 38949 47 0 0 25 0 1 0 423737881 57618432 13503 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14067 13503 603 41 0 14026 0
vsize: 56268
[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13666 0 0 0 39948 47 0 0 25 0 1 0 423737881 57753600 13518 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 13518 603 41 0 14059 0
vsize: 56400
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13666 0 0 0 40948 47 0 0 25 0 1 0 423737881 57753600 13518 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 13518 603 41 0 14059 0
vsize: 56400
[startup+420.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13666 0 0 0 41948 48 0 0 25 0 1 0 423737881 57753600 13518 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 13518 603 41 0 14059 0
vsize: 56400
[startup+430.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13666 0 0 0 42947 48 0 0 25 0 1 0 423737881 57753600 13518 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 13518 603 41 0 14059 0
vsize: 56400
[startup+440.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13666 0 0 0 43947 48 0 0 25 0 1 0 423737881 57753600 13518 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 13518 603 41 0 14059 0
vsize: 56400
[startup+450.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13666 0 0 0 44947 48 0 0 25 0 1 0 423737881 57753600 13518 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 13518 603 41 0 14059 0
vsize: 56400
[startup+460.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13666 0 0 0 45947 49 0 0 25 0 1 0 423737881 57753600 13518 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 13518 603 41 0 14059 0
vsize: 56400
[startup+470.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13666 0 0 0 46947 49 0 0 25 0 1 0 423737881 57753600 13518 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 13518 603 41 0 14059 0
vsize: 56400
[startup+480.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13666 0 0 0 47946 49 0 0 25 0 1 0 423737881 57753600 13518 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14100 13518 603 41 0 14059 0
vsize: 56400
[startup+490.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13667 0 0 0 48946 49 0 0 25 0 1 0 423737881 58015744 13519 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13519 603 41 0 14123 0
vsize: 56656
[startup+500.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13669 0 0 0 49946 50 0 0 25 0 1 0 423737881 58015744 13521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13521 603 41 0 14123 0
vsize: 56656
[startup+510.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13669 0 0 0 50946 50 0 0 25 0 1 0 423737881 58015744 13521 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13521 603 41 0 14123 0
vsize: 56656
[startup+520.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13669 0 0 0 51947 50 0 0 25 0 1 0 423737881 58015744 13521 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13521 603 41 0 14123 0
vsize: 56656
[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13669 0 0 0 52947 50 0 0 25 0 1 0 423737881 58015744 13521 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13521 603 41 0 14123 0
vsize: 56656
[startup+540.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13669 0 0 0 53947 50 0 0 25 0 1 0 423737881 58015744 13521 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13521 603 41 0 14123 0
vsize: 56656
[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.93 3/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13669 0 0 0 54947 50 0 0 25 0 1 0 423737881 58015744 13521 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13521 603 41 0 14123 0
vsize: 56656
[startup+560.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13669 0 0 0 55946 50 0 0 25 0 1 0 423737881 58015744 13521 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14164 13521 603 41 0 14123 0
vsize: 56656
[startup+570.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13669 0 0 0 56946 50 0 0 25 0 1 0 423737881 58015744 13521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13521 603 41 0 14123 0
vsize: 56656
[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13669 0 0 0 57946 50 0 0 25 0 1 0 423737881 58015744 13521 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13521 603 41 0 14123 0
vsize: 56656
[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13669 0 0 0 58946 50 0 0 25 0 1 0 423737881 58015744 13521 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13521 603 41 0 14123 0
vsize: 56656
[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 13687 0 0 0 59947 50 0 0 25 0 1 0 423737881 58015744 13539 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14164 13539 603 41 0 14123 0
vsize: 56656
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 14419 0 0 0 60944 52 0 0 25 0 1 0 423737881 60968960 14271 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14885 14271 603 41 0 14844 0
vsize: 59540
[startup+620.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15110 0 0 0 61942 55 0 0 25 0 1 0 423737881 63799296 14962 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15576 14962 603 41 0 15535 0
vsize: 62304
[startup+630.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15802 0 0 0 62941 56 0 0 25 0 1 0 423737881 66609152 15654 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16262 15655 603 41 0 16221 0
vsize: 65048
[startup+640.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 63941 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 64941 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 65941 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 66942 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 67942 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+690.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 68942 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+700.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 69942 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+710.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 70943 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+720.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 71943 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+730.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 72943 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+740.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 73943 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15858 0 0 0 74943 56 0 0 25 0 1 0 423737881 66879488 15710 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16328 15710 603 41 0 16287 0
vsize: 65312
[startup+760.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 15898 0 0 0 75943 56 0 0 25 0 1 0 423737881 67010560 15750 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16360 15750 603 41 0 16319 0
vsize: 65440
[startup+770.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 16472 0 0 0 76942 58 0 0 25 0 1 0 423737881 69419008 16324 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16948 16324 603 41 0 16907 0
vsize: 67792
[startup+780.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 17100 0 0 0 77941 59 0 0 25 0 1 0 423737881 71974912 16952 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17572 16952 603 41 0 17531 0
vsize: 70288
[startup+790.043 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 17639 0 0 0 78940 60 0 0 25 0 1 0 423737881 74264576 17491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18131 17491 603 41 0 18090 0
vsize: 72524
[startup+800.043 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 18126 0 0 0 79939 62 0 0 25 0 1 0 423737881 76152832 17978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18592 17978 603 41 0 18551 0
vsize: 74368
[startup+810.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 18658 0 0 0 80937 64 0 0 25 0 1 0 423737881 78458880 18510 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19155 18510 603 41 0 19114 0
vsize: 76620
[startup+820.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19029 0 0 0 81936 65 0 0 25 0 1 0 423737881 79945728 18881 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18881 603 41 0 19477 0
vsize: 78072
[startup+830.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19029 0 0 0 82937 65 0 0 25 0 1 0 423737881 79945728 18881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18881 603 41 0 19477 0
vsize: 78072
[startup+840.045 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19029 0 0 0 83937 65 0 0 25 0 1 0 423737881 79945728 18881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18881 603 41 0 19477 0
vsize: 78072
[startup+850.046 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19029 0 0 0 84937 65 0 0 25 0 1 0 423737881 79945728 18881 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18881 603 41 0 19477 0
vsize: 78072
[startup+860.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19029 0 0 0 85937 65 0 0 25 0 1 0 423737881 79945728 18881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18881 603 41 0 19477 0
vsize: 78072
[startup+870.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19030 0 0 0 86938 65 0 0 25 0 1 0 423737881 79945728 18882 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18882 603 41 0 19477 0
vsize: 78072
[startup+880.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19030 0 0 0 87938 65 0 0 25 0 1 0 423737881 79945728 18882 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18882 603 41 0 19477 0
vsize: 78072
[startup+890.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19030 0 0 0 88938 65 0 0 25 0 1 0 423737881 79945728 18882 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18882 603 41 0 19477 0
vsize: 78072
[startup+900.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19031 0 0 0 89938 65 0 0 25 0 1 0 423737881 79945728 18883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18883 603 41 0 19477 0
vsize: 78072
[startup+910.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19031 0 0 0 90938 65 0 0 25 0 1 0 423737881 79945728 18883 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18883 603 41 0 19477 0
vsize: 78072
[startup+920.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19031 0 0 0 91939 65 0 0 25 0 1 0 423737881 79945728 18883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18883 603 41 0 19477 0
vsize: 78072
[startup+930.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19031 0 0 0 92939 65 0 0 25 0 1 0 423737881 79945728 18883 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18883 603 41 0 19477 0
vsize: 78072
[startup+940.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19031 0 0 0 93939 65 0 0 25 0 1 0 423737881 79945728 18883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18883 603 41 0 19477 0
vsize: 78072
[startup+950.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19031 0 0 0 94939 65 0 0 25 0 1 0 423737881 79945728 18883 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19518 18883 603 41 0 19477 0
vsize: 78072
[startup+960.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19033 0 0 0 95939 65 0 0 25 0 1 0 423737881 79945728 18885 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18885 603 41 0 19477 0
vsize: 78072
[startup+970.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19036 0 0 0 96939 65 0 0 25 0 1 0 423737881 79945728 18888 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18888 603 41 0 19477 0
vsize: 78072
[startup+980.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 97939 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+990.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 98940 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 99940 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 100940 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 101940 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 102940 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 103940 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 104941 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223728 134559413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 105941 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 106941 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 107941 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 108941 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 109941 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223648 134560352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 110942 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 111942 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 112942 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 113942 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 114942 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 115943 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223544 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 116943 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 117943 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223648 134559808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 118943 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20416
Raw data (stat): 20416 (minisat+) R 20415 10720 10719 0 -1 0 19037 0 0 0 119943 65 0 0 25 0 1 0 423737881 79945728 18889 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19518 18889 603 41 0 19477 0
vsize: 78072
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 20416
Raw data (stat): 20416 (minisat+) Z 20415 10720 10719 0 -1 12 19040 0 0 0 119943 68 0 0 25 0 1 0 423737881 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.13
CPU user time (s): 1199.44
CPU system time (s): 0.689895
CPU usage (%): 100.003
Max. virtual memory (Kb): 78072
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####