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/mps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-ran12x12.opb
MD5SUM	e4638ea46dbf743c721f5094f551c5b7
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6257268
Optimality of the best value was proved	NO
Number of terms in the objective function	4464
Biggest coefficient in the objective function	5368709120
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	856864234722
Number of bits of the sum of numbers in the objective function	40
Biggest number in a constraint	5368709120
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	856864234722
Number of bits of the biggest sum of numbers	40
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1232.17
Number of variables	4464
Total number of constraints	168
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	168
Minimum length of a constraint	31
Maximum length of a constraint	360
Trace number 30882

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-05-25 20:28:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22282 boxname=wulflinc4 idbench=1098 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  e4638ea46dbf743c721f5094f551c5b7  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-ran12x12.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-ran12x12.opb
IDLAUNCH: 22282
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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.169
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:        892860 kB
Buffers:         28592 kB
Cached:          93036 kB
SwapCached:        500 kB
Active:          27400 kB
Inactive:        96584 kB
HighTotal:      131008 kB
HighFree:        45108 kB
LowTotal:       903652 kB
LowFree:        847752 kB
SwapTotal:     2097136 kB
SwapFree:      2096004 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5784 kB
Slab:            12188 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 20:48:56 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22282 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 192 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 190]---> Adder-cost: 310   maxlim: 234484   bits: 18/18
c ---[ 188]---> Adder-cost: 286   maxlim: 89076   bits: 17/17
c ---[ 186]---> Adder-cost: 310   maxlim: 238580   bits: 18/18
c ---[ 184]---> Adder-cost: 302   maxlim: 145396   bits: 18/18
c ---[ 182]---> Adder-cost: 310   maxlim: 238580   bits: 18/18
c ---[ 180]---> Adder-cost: 310   maxlim: 231412   bits: 18/18
c ---[ 178]---> Adder-cost: 286   maxlim: 90100   bits: 17/17
c ---[ 176]---> Adder-cost: 310   maxlim: 236532   bits: 18/18
c ---[ 174]---> Adder-cost: 302   maxlim: 147444   bits: 18/18
c ---[ 172]---> Adder-cost: 310   maxlim: 241652   bits: 18/18
c ---[ 170]---> Adder-cost: 310   maxlim: 233460   bits: 18/18
c ---[ 168]---> Adder-cost: 310   maxlim: 240628   bits: 18/18
c ---[ 166]---> Adder-cost: 286   maxlim: 91124   bits: 17/17
c ---[ 164]---> Adder-cost: 286   maxlim: 92148   bits: 17/17
c ---[ 162]---> Adder-cost: 322   maxlim: 291828   bits: 19/19
c ---[ 160]---> Adder-cost: 322   maxlim: 285684   bits: 19/19
c ---[ 158]---> Adder-cost: 322   maxlim: 293876   bits: 19/19
c ---[ 156]---> Adder-cost: 286   maxlim: 92148   bits: 17/17
c ---[ 154]---> Adder-cost: 322   maxlim: 278516   bits: 19/19
c ---[ 152]---> Adder-cost: 322   maxlim: 290804   bits: 19/19
c ---[ 150]---> Adder-cost: 306   maxlim: 168948   bits: 18/18
c ---[ 148]---> Adder-cost: 264   maxlim: 46068   bits: 16/16
c ---[ 146]---> Adder-cost: 322   maxlim: 266228   bits: 19/19
c ---[ 144]---> Adder-cost: 306   maxlim: 169972   bits: 18/18
c ---[ 143]---> BDD-cost:   16
c ---[ 142]---> BDD-cost:   15
c ---[ 141]---> BDD-cost:   20
c ---[ 140]---> BDD-cost:   17
c ---[ 139]---> BDD-cost:   18
c ---[ 138]---> BDD-cost:   18
c ---[ 137]---> BDD-cost:   14
c ---[ 136]---> BDD-cost:   17
c ---[ 135]---> BDD-cost:   17
c ---[ 134]---> BDD-cost:   20
c ---[ 133]---> BDD-cost:   17
c ---[ 132]---> BDD-cost:   16
c ---[ 131]---> BDD-cost:   15
c ---[ 130]---> BDD-cost:   20
c ---[ 129]---> BDD-cost:   20
c ---[ 128]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   20
c ---[ 126]---> BDD-cost:   20
c ---[ 125]---> BDD-cost:   18
c ---[ 124]---> BDD-cost:   14
c ---[ 123]---> BDD-cost:   20
c ---[ 122]---> BDD-cost:   17
c ---[ 121]---> BDD-cost:   20
c ---[ 120]---> BDD-cost:   20
c ---[ 119]---> BDD-cost:   16
c ---[ 118]---> BDD-cost:   16
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   20
c ---[ 115]---> BDD-cost:   15
c ---[ 114]---> BDD-cost:   20
c ---[ 113]---> BDD-cost:   20
c ---[ 112]---> BDD-cost:   18
c ---[ 111]---> BDD-cost:   14
c ---[ 110]---> BDD-cost:   20
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   20
c ---[ 106]---> BDD-cost:   20
c ---[ 105]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   17
c ---[ 100]---> BDD-cost:   17
c ---[  99]---> BDD-cost:   18
c ---[  98]---> BDD-cost:   14
c ---[  97]---> BDD-cost:   16
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   17
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:   16
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   16
c ---[  89]---> BDD-cost:   16
c ---[  88]---> BDD-cost:   14
c ---[  87]---> BDD-cost:   20
c ---[  86]---> BDD-cost:   16
c ---[  85]---> BDD-cost:   16
c ---[  84]---> BDD-cost:   16
c ---[  83]---> BDD-cost:   16
c ---[  82]---> BDD-cost:   16
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   20
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   20
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   15
c ---[  75]---> BDD-cost:   18
c ---[  74]---> BDD-cost:   14
c ---[  73]---> BDD-cost:   20
c ---[  72]---> BDD-cost:   17
c ---[  71]---> BDD-cost:   20
c ---[  70]---> BDD-cost:   20
c ---[  69]---> BDD-cost:   16
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   20
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   20
c ---[  64]---> BDD-cost:   19
c ---[  63]---> BDD-cost:   18
c ---[  62]---> BDD-cost:   18
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   19
c ---[  59]---> BDD-cost:   17
c ---[  58]---> BDD-cost:   20
c ---[  57]---> BDD-cost:   20
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   18
c ---[  53]---> BDD-cost:   14
c ---[  52]---> BDD-cost:   14
c ---[  51]---> BDD-cost:   14
c ---[  50]---> BDD-cost:   14
c ---[  49]---> BDD-cost:   14
c ---[  48]---> BDD-cost:   14
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   14
c ---[  43]---> BDD-cost:   18
c ---[  42]---> BDD-cost:   16
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   20
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   20
c ---[  37]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   18
c ---[  35]---> BDD-cost:   14
c ---[  34]---> BDD-cost:   20
c ---[  33]---> BDD-cost:   17
c ---[  32]---> BDD-cost:   14
c ---[  31]---> BDD-cost:   20
c ---[  30]---> BDD-cost:   20
c ---[  29]---> BDD-cost:   16
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   16
c ---[  26]---> BDD-cost:   15
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   16
c ---[  23]---> BDD-cost:   18
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   20
c ---[  20]---> BDD-cost:   16
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   16
c ---[  16]---> BDD-cost:   16
c ---[  15]---> BDD-cost:   15
c ---[  14]---> BDD-cost:   16
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   16
c ---[  11]---> BDD-cost:   16
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   18
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   17
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   16
c ---[   3]---> BDD-cost:   16
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   20
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   51740   179989 |   17246       0        0     nan |  0.000 % |
c |       100 |   51666   179737 |   18970      91      276     3.0 | 26.132 % |
c |       250 |   51572   179413 |   20867     230      705     3.1 | 26.264 % |
c |       475 |   51491   179142 |   22954     443     1402     3.2 | 26.372 % |
c |       812 |   51311   178532 |   25249     756     2403     3.2 | 26.620 % |
c |      1318 |   51103   177818 |   27774    1240     4006     3.2 | 26.907 % |
c |      2077 |   50944   177263 |   30552    1981     6901     3.5 | 27.100 % |
c |      3216 |   50782   176699 |   33607    3098    12034     3.9 | 27.302 % |
c |      4924 |   50664   176293 |   36968    4790    23296     4.9 | 27.464 % |
c |      7486 |   50574   175987 |   40665    7343    40684     5.5 | 27.588 % |
c |     11331 |   50501   175742 |   44731   11178    71213     6.4 | 27.689 % |
c |     17098 |   50444   175553 |   49204   16938   127675     7.5 | 27.766 % |
c |     25747 |   50419   175472 |   54125   25583   387876    15.2 | 27.805 % |
c |     38721 |   50263   174940 |   59537   38540   578494    15.0 | 28.029 % |
c |     58183 |   50129   174506 |   65491   57980  1525583    26.3 | 28.238 % |
c ==============================================================================
c [1mFound solution: 19202090[0m
c ---[   0]---> Adder-cost: 7514   maxlim: 13642936   bits: 25/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69005 |  102550   361806 |   34183   68792  1691771    24.6 | 28.238 % |
c |     69105 |  102550   361806 |   37601   21808   297897    13.7 | 17.965 % |
c |     69255 |  102550   361806 |   41361   21958   298886    13.6 | 17.965 % |
c |     69482 |  102550   361806 |   45497   22185   302143    13.6 | 17.965 % |
c |     69819 |  102550   361806 |   50047   22522   306299    13.6 | 17.965 % |
c |     70325 |  102550   361806 |   55052   23028   312623    13.6 | 17.965 % |
c |     71085 |  102550   361806 |   60557   23788   320890    13.5 | 17.965 % |
c |     72224 |  102550   361806 |   66612   24927   330994    13.3 | 17.965 % |
c |     73932 |  102527   361731 |   73274   26631   346671    13.0 | 17.984 % |
c |     76495 |  102500   361644 |   80601   29191   370660    12.7 | 18.014 % |
c |     80339 |  102491   361615 |   88661   33033   447792    13.6 | 18.023 % |
c |     86105 |  102491   361615 |   97528   38799   568237    14.6 | 18.023 % |
c ==============================================================================
c [1mFound solution: 19067656[0m
c ---[   0]---> Adder-cost: 0   maxlim: 13777370   bits: 25/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     93827 |  102468   361708 |   34156   46515   705392    15.2 | 18.023 % |
c |     93927 |  102468   361708 |   37571   20882   255892    12.3 | 18.111 % |
c |     94077 |  102468   361708 |   41328   21032   256929    12.2 | 18.111 % |
c |     94302 |  102468   361708 |   45461   21257   258510    12.2 | 18.111 % |
c |     94640 |  102468   361708 |   50007   21595   261298    12.1 | 18.111 % |
c |     95147 |  102468   361708 |   55008   22102   265422    12.0 | 18.111 % |
c |     95906 |  102468   361708 |   60509   22861   274152    12.0 | 18.111 % |
c |     97045 |  102468   361708 |   66560   24000   294684    12.3 | 18.111 % |
c |     98754 |  102468   361708 |   73216   25709   330905    12.9 | 18.111 % |
c |    101316 |  102468   361708 |   80538   28271   382386    13.5 | 18.111 % |
c |    105161 |  102468   361708 |   88591   32116   542265    16.9 | 18.111 % |
c |    110927 |  102468   361708 |   97451   37882   914519    24.1 | 18.111 % |
c ==============================================================================
c [1mFound solution: 18358477[0m
c ---[   0]---> Adder-cost: 0   maxlim: 14486549   bits: 25/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    118043 |  102480   361852 |   34160   44997  1091755    24.3 | 18.111 % |
c |    118143 |  102480   361852 |   37576   19060   532782    28.0 | 18.152 % |
c |    118294 |  102480   361852 |   41333   19211   533476    27.8 | 18.152 % |
c |    118519 |  102480   361852 |   45466   19436   534519    27.5 | 18.152 % |
c |    118856 |  102480   361852 |   50013   19773   536326    27.1 | 18.152 % |
c |    119362 |  102480   361852 |   55015   20279   539703    26.6 | 18.152 % |
c |    120121 |  102480   361852 |   60516   21038   546346    26.0 | 18.152 % |
c |    121261 |  102480   361852 |   66568   22178   552709    24.9 | 18.152 % |
c |    122969 |  102480   361852 |   73224   23886   564300    23.6 | 18.152 % |
c |    125531 |  102480   361852 |   80547   26448   603535    22.8 | 18.152 % |
c |    129375 |  102463   361793 |   88602   30290   647887    21.4 | 18.166 % |
c |    135141 |  102463   361793 |   97462   36056   920604    25.5 | 18.166 % |
c |    143791 |  102374   361504 |  107208   44691  1036759    23.2 | 18.249 % |
c |    156766 |  102315   361313 |  117929   57656  1603292    27.8 | 18.308 % |
c |    176229 |  102315   361313 |  129722   77119  2298418    29.8 | 18.308 % |
c ==============================================================================
c [1mFound solution: 12055116[0m
c ---[   0]---> Adder-cost: 0   maxlim: 20789910   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    178932 |  102297   361014 |   34099   79559  2326882    29.2 | 18.308 % |
c |    179032 |  102297   361014 |   37508   23357   415555    17.8 | 18.376 % |
c |    179182 |  102297   361014 |   41259   23507   416359    17.7 | 18.376 % |
c |    179407 |  102297   361014 |   45385   23732   417790    17.6 | 18.376 % |
c |    179744 |  102297   361014 |   49924   24069   420126    17.5 | 18.376 % |
c |    180251 |  102297   361014 |   54916   24576   423388    17.2 | 18.376 % |
c |    181010 |  102297   361014 |   60408   25335   433858    17.1 | 18.376 % |
c |    182149 |  102297   361014 |   66449   26474   441856    16.7 | 18.376 % |
c |    183857 |  102297   361014 |   73094   28182   453830    16.1 | 18.376 % |
c |    186419 |  102297   361014 |   80403   30744   488052    15.9 | 18.376 % |
c |    190263 |  102297   361014 |   88444   34588   562847    16.3 | 18.376 % |
c |    196030 |  102297   361014 |   97288   40355   629218    15.6 | 18.376 % |
c |    204681 |  102297   361014 |  107017   49006   893711    18.2 | 18.376 % |
c |    217655 |  102288   360983 |  117718   61974  1160447    18.7 | 18.381 % |
c ==============================================================================
c [1mFound solution: 10959391[0m
c ---[   0]---> Adder-cost: 0   maxlim: 21885635   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    221018 |  102306   361146 |   34102   65337  1243337    19.0 | 18.381 % |
c |    221118 |  102306   361146 |   37512   23353   329126    14.1 | 18.427 % |
c |    221268 |  102306   361146 |   41263   23503   330423    14.1 | 18.427 % |
c |    221493 |  102306   361146 |   45389   23728   331928    14.0 | 18.427 % |
c |    221830 |  102306   361146 |   49928   24065   333878    13.9 | 18.427 % |
c |    222336 |  102306   361146 |   54921   24571   336893    13.7 | 18.427 % |
c |    223095 |  102306   361146 |   60413   25330   341654    13.5 | 18.427 % |
c |    224234 |  102306   361146 |   66455   26469   351554    13.3 | 18.427 % |
c |    225942 |  102306   361146 |   73100   28177   365495    13.0 | 18.427 % |
c |    228506 |  102306   361146 |   80410   30741   387489    12.6 | 18.427 % |
c |    232350 |  102306   361146 |   88451   34585   429394    12.4 | 18.427 % |
c |    238116 |  102306   361146 |   97296   40351   515257    12.8 | 18.427 % |
c |    246765 |  102306   361146 |  107026   49000   695085    14.2 | 18.427 % |
c |    259739 |  102306   361146 |  117729   61974   931988    15.0 | 18.427 % |
c |    279200 |  102297   361115 |  129502   81432  1747727    21.5 | 18.432 % |
c |    308392 |  102297   361115 |  142452  110624  4227666    38.2 | 18.432 % |
c |    352182 |  102297   361115 |  156697  154414  5827728    37.7 | 18.432 % |
c |    417866 |  102297   361115 |  172367   75522 12168947   161.1 | 18.432 % |
c ==============================================================================
c [1mFound solution: 10565475[0m
c ---[   0]---> Adder-cost: 0   maxlim: 22279551   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    475452 |  102313   361245 |   34104  133108 15562795   116.9 | 18.432 % |
c |    475552 |  102313   361245 |   37514   20196   529153    26.2 | 18.466 % |
c |    475702 |  102313   361245 |   41265   20346   529931    26.0 | 18.466 % |
c |    475927 |  102313   361245 |   45392   20571   530991    25.8 | 18.466 % |
c |    476265 |  102313   361245 |   49931   20909   532498    25.5 | 18.466 % |
c |    476771 |  102313   361245 |   54924   21415   534909    25.0 | 18.466 % |
c |    477530 |  102313   361245 |   60417   22174   539545    24.3 | 18.466 % |
c |    478669 |  102313   361245 |   66459   23313   548736    23.5 | 18.466 % |
c |    480377 |  102313   361245 |   73104   25021   560294    22.4 | 18.466 % |
c |    482939 |  102313   361245 |   80415   27583   588725    21.3 | 18.466 % |
c |    486784 |  102313   361245 |   88456   31428   808998    25.7 | 18.466 % |
c |    492551 |  102313   361245 |   97302   37195   915656    24.6 | 18.466 % |
c |    501200 |  102313   361245 |  107032   45844  1124671    24.5 | 18.466 % |
c |    514175 |  102313   361245 |  117736   58819  2690821    45.7 | 18.466 % |
c |    533636 |  102313   361245 |  129509   78280  6024194    77.0 | 18.466 % |
c |    562828 |  102313   361245 |  142460  107472  6619208    61.6 | 18.466 % |
c |    606617 |  102313   361245 |  156706  151261  7975411    52.7 | 18.466 % |
c |    672301 |  102313   361245 |  172377   72132 12675295   175.7 | 18.466 % |
c ==============================================================================
c [1mFound solution: 9788326[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23056700   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    697086 |  102333   361449 |   34111   96917 13208295   136.3 | 18.466 % |
c |    697186 |  102333   361449 |   37522   19590   233647    11.9 | 18.512 % |
c |    697336 |  102333   361449 |   41274   19740   234329    11.9 | 18.512 % |
c |    697562 |  102333   361449 |   45401   19966   235417    11.8 | 18.512 % |
c |    697899 |  102333   361449 |   49941   20303   236965    11.7 | 18.512 % |
c |    698405 |  102333   361449 |   54936   20809   240071    11.5 | 18.512 % |
c |    699164 |  102333   361449 |   60429   21568   245763    11.4 | 18.512 % |
c |    700303 |  102333   361449 |   66472   22707   257554    11.3 | 18.512 % |
c |    702012 |  102333   361449 |   73119   24416   273809    11.2 | 18.512 % |
c |    704574 |  102333   361449 |   80431   26978   289616    10.7 | 18.512 % |
c |    708418 |  102333   361449 |   88475   30822   326790    10.6 | 18.512 % |
c |    714184 |  102333   361449 |   97322   36588   398678    10.9 | 18.512 % |
c |    722833 |  102333   361449 |  107054   45237   522312    11.5 | 18.512 % |
c |    735807 |  102333   361449 |  117760   58211   781402    13.4 | 18.512 % |
c |    755268 |  102333   361449 |  129536   77672  1234065    15.9 | 18.512 % |
c |    784460 |  102333   361449 |  142490  106864  2438117    22.8 | 18.512 % |
c |    828249 |  102333   361449 |  156739   19496   735025    37.7 | 18.512 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  5058 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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): 1.08 1.04 0.97 2/54 5054
Raw data (stat): 5054 (runsolver) R 5053 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783531135 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0006 s]
Raw data (loadavg): 1.06 1.04 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0011 s]
Raw data (loadavg): 1.05 1.04 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.002 s]
Raw data (loadavg): 1.05 1.03 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0022 s]
Raw data (loadavg): 1.04 1.03 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0026 s]
Raw data (loadavg): 1.03 1.03 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0025 s]
Raw data (loadavg): 1.03 1.03 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.003 s]
Raw data (loadavg): 1.02 1.03 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0032 s]
Raw data (loadavg): 1.02 1.03 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0031 s]
Raw data (loadavg): 1.02 1.03 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 1.01 1.02 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.005 s]
Raw data (loadavg): 1.01 1.02 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 1.01 1.02 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.005 s]
Raw data (loadavg): 1.01 1.02 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 1.00 1.02 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 1.00 1.02 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.005 s]
Raw data (loadavg): 1.00 1.02 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.005 s]
Raw data (loadavg): 1.00 1.02 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.005 s]
Raw data (loadavg): 1.00 1.02 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.005 s]
Raw data (loadavg): 1.00 1.02 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 1.00 1.01 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.005 s]
Raw data (loadavg): 1.00 1.01 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.006 s]
Raw data (loadavg): 1.00 1.01 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.006 s]
Raw data (loadavg): 1.00 1.01 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.006 s]
Raw data (loadavg): 1.00 1.01 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 1.00 1.01 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 1.00 1.01 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.008 s]
Raw data (loadavg): 1.00 1.01 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.008 s]
Raw data (loadavg): 1.00 1.01 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.008 s]
Raw data (loadavg): 1.00 1.01 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.011 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.011 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.011 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.012 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.013 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.013 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.013 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.014 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.015 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.014 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.056 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.057 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.058 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.058 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.059 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.061 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.06 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.071 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.175 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.175 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.175 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.175 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.175 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.176 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.176 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.176 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.176 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.177 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.178 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.178 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.179 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.178 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.179 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.18 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.18 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.18 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.181 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.18 s]
Raw data (loadavg): 1.00 1.00 0.97 3/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.18 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.18 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.18 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.18 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.18 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.19 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.19 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.19 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.19 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.19 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.19 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.19 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.19 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.19 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.19 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.2 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.2 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.2 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.2 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.2 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.2 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.2 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.75 s]
Raw data (loadavg): 1.00 1.00 0.97 1/53 5058
Raw data (stat): 5054 (minisat+_script) S 5053 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783531135 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.75
CPU time (s): 1229.88
CPU user time (s): 1229.15
CPU system time (s): 0.729889
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####