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-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-10teams.opb
MD5SUM	1ff3cc3253012886aa21be4feac6111e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	920
Optimality of the best value was proved	NO
Number of terms in the objective function	1800
Biggest coefficient in the objective function	86
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	41700
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	86
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	41700
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.75
Number of variables	1800
Total number of constraints	2015
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2015
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	72
Trace number 31122

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-05-25 22:13:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22521 boxname=wulflinc29 idbench=1337 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  1ff3cc3253012886aa21be4feac6111e  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-10teams.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-10teams.opb
IDLAUNCH: 22521
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        781204 kB
Buffers:         31972 kB
Cached:         199592 kB
SwapCached:        452 kB
Active:          19440 kB
Inactive:       214380 kB
HighTotal:      131008 kB
HighFree:        73248 kB
LowTotal:       903652 kB
LowFree:        707956 kB
SwapTotal:     2097892 kB
SwapFree:      2096752 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5612 kB
Slab:            13904 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 22:34:04 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 22521 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 330 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 329]---> BDD-cost:  125
c ---[ 328]---> BDD-cost:  185
c ---[ 326]---> BDD-cost:   77
c ---[ 324]---> BDD-cost:   77
c ---[ 322]---> BDD-cost:   77
c ---[ 320]---> BDD-cost:   77
c ---[ 318]---> BDD-cost:   77
c ---[ 316]---> BDD-cost:   77
c ---[ 314]---> BDD-cost:   77
c ---[ 312]---> BDD-cost:   77
c ---[ 310]---> BDD-cost:   77
c ---[ 308]---> BDD-cost:   77
c ---[ 307]---> BDD-cost:  185
c ---[ 305]---> BDD-cost:   77
c ---[ 303]---> BDD-cost:   77
c ---[ 301]---> BDD-cost:   77
c ---[ 299]---> BDD-cost:   77
c ---[ 297]---> BDD-cost:   77
c ---[ 295]---> BDD-cost:   77
c ---[ 293]---> BDD-cost:   77
c ---[ 291]---> BDD-cost:   77
c ---[ 289]---> BDD-cost:   77
c ---[ 288]---> BDD-cost:  125
c ---[ 286]---> BDD-cost:   77
c ---[ 284]---> BDD-cost:   77
c ---[ 282]---> BDD-cost:   77
c ---[ 280]---> BDD-cost:   77
c ---[ 278]---> BDD-cost:   77
c ---[ 276]---> BDD-cost:   77
c ---[ 274]---> BDD-cost:   77
c ---[ 272]---> BDD-cost:   77
c ---[ 270]---> BDD-cost:   77
c ---[ 269]---> BDD-cost:  185
c ---[ 267]---> BDD-cost:   77
c ---[ 265]---> BDD-cost:   77
c ---[ 263]---> BDD-cost:   77
c ---[ 261]---> BDD-cost:   77
c ---[ 259]---> BDD-cost:   77
c ---[ 257]---> BDD-cost:   77
c ---[ 255]---> BDD-cost:   77
c ---[ 253]---> BDD-cost:   77
c ---[ 251]---> BDD-cost:   77
c ---[ 250]---> BDD-cost:  185
c ---[ 248]---> BDD-cost:   70
c ---[ 246]---> BDD-cost:   77
c ---[ 244]---> BDD-cost:   77
c ---[ 242]---> BDD-cost:   77
c ---[ 240]---> BDD-cost:   77
c ---[ 238]---> BDD-cost:   77
c ---[ 236]---> BDD-cost:   77
c ---[ 234]---> BDD-cost:   77
c ---[ 233]---> BDD-cost:  185
c ---[ 231]---> BDD-cost:   77
c ---[ 229]---> BDD-cost:   77
c ---[ 227]---> BDD-cost:   77
c ---[ 225]---> BDD-cost:   77
c ---[ 223]---> BDD-cost:   77
c ---[ 221]---> BDD-cost:   77
c ---[ 219]---> BDD-cost:   77
c ---[ 217]---> BDD-cost:   77
c ---[ 216]---> BDD-cost:  185
c ---[ 214]---> BDD-cost:   70
c ---[ 212]---> BDD-cost:   77
c ---[ 210]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:   77
c ---[ 206]---> BDD-cost:   77
c ---[ 204]---> BDD-cost:   77
c ---[ 202]---> BDD-cost:   77
c ---[ 200]---> BDD-cost:   77
c ---[ 198]---> BDD-cost:   70
c ---[ 197]---> BDD-cost:  185
c ---[ 195]---> BDD-cost:   77
c ---[ 193]---> BDD-cost:   77
c ---[ 191]---> BDD-cost:   77
c ---[ 189]---> BDD-cost:   77
c ---[ 187]---> BDD-cost:   77
c ---[ 185]---> BDD-cost:   77
c ---[ 183]---> BDD-cost:   77
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   77
c ---[ 178]---> BDD-cost:  125
c ---[ 176]---> BDD-cost:   77
c ---[ 174]---> BDD-cost:   77
c ---[ 172]---> BDD-cost:   77
c ---[ 170]---> BDD-cost:   77
c ---[ 168]---> BDD-cost:   77
c ---[ 166]---> BDD-cost:   77
c ---[ 164]---> BDD-cost:   77
c ---[ 162]---> BDD-cost:   77
c ---[ 160]---> BDD-cost:   77
c ---[ 159]---> BDD-cost:  185
c ---[ 157]---> BDD-cost:   77
c ---[ 155]---> BDD-cost:   77
c ---[ 153]---> BDD-cost:   77
c ---[ 151]---> BDD-cost:   77
c ---[ 149]---> BDD-cost:   77
c ---[ 147]---> BDD-cost:   77
c ---[ 145]---> BDD-cost:   77
c ---[ 143]---> BDD-cost:   77
c ---[ 141]---> BDD-cost:   77
c ---[ 140]---> BDD-cost:  185
c ---[ 139]---> BDD-cost:  185
c ---[ 137]---> BDD-cost:   77
c ---[ 135]---> BDD-cost:   77
c ---[ 133]---> BDD-cost:   77
c ---[ 131]---> BDD-cost:   77
c ---[ 129]---> BDD-cost:   77
c ---[ 127]---> BDD-cost:   77
c ---[ 125]---> BDD-cost:   77
c ---[ 123]---> BDD-cost:   77
c ---[ 121]---> BDD-cost:   77
c ---[ 120]---> BDD-cost:  178
c ---[ 118]---> BDD-cost:   77
c ---[ 116]---> BDD-cost:   77
c ---[ 114]---> BDD-cost:   77
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:   77
c ---[ 108]---> BDD-cost:   77
c ---[ 106]---> BDD-cost:   77
c ---[ 104]---> BDD-cost:   77
c ---[ 102]---> BDD-cost:   77
c ---[ 101]---> BDD-cost:  185
c ---[  99]---> BDD-cost:   77
c ---[  97]---> BDD-cost:   77
c ---[  95]---> BDD-cost:   77
c ---[  93]---> BDD-cost:   77
c ---[  91]---> BDD-cost:   77
c ---[  89]---> BDD-cost:   77
c ---[  87]---> BDD-cost:   77
c ---[  85]---> BDD-cost:   77
c ---[  83]---> BDD-cost:   77
c ---[  82]---> BDD-cost:  125
c ---[  80]---> BDD-cost:   77
c ---[  79]---> BDD-cost:  185
c ---[  78]---> BDD-cost:  185
c ---[  77]---> BDD-cost:  178
c ---[  76]---> BDD-cost:  185
c ---[  75]---> BDD-cost:  185
c ---[  74]---> BDD-cost:  125
c ---[  73]---> BDD-cost:  185
c ---[  72]---> BDD-cost:  185
c ---[  71]---> BDD-cost:  178
c ---[  70]---> BDD-cost:  185
c ---[  69]---> BDD-cost:  185
c ---[  68]---> BDD-cost:  125
c ---[  67]---> BDD-cost:  185
c ---[  66]---> BDD-cost:  178
c ---[  65]---> BDD-cost:  185
c ---[  64]---> BDD-cost:  185
c ---[  63]---> BDD-cost:  185
c ---[  62]---> BDD-cost:  185
c ---[  61]---> BDD-cost:  125
c ---[  60]---> BDD-cost:  118
c ---[  59]---> BDD-cost:  185
c ---[  58]---> BDD-cost:  185
c ---[  57]---> BDD-cost:  185
c ---[  56]---> BDD-cost:  185
c ---[  55]---> BDD-cost:  178
c ---[  54]---> BDD-cost:  185
c ---[  53]---> BDD-cost:  185
c ---[  52]---> BDD-cost:  185
c ---[  51]---> BDD-cost:  185
c ---[  50]---> BDD-cost:  125
c ---[  49]---> BDD-cost:   76
c ---[  48]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  46]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  44]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  42]---> BDD-cost:   76
c ---[  41]---> BDD-cost:  177
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:  123
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:  183
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   75
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:  183
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   53221   141547 |   17740       0        0     nan |  0.000 % |
c |       100 |   53221   141547 |   19514     100     2449    24.5 |  1.808 % |
c |       251 |   53221   141547 |   21465     251    20371    81.2 |  1.808 % |
c |       476 |   53221   141547 |   23611     476    41787    87.8 |  1.808 % |
c |       813 |   53221   141547 |   25973     813    88284   108.6 |  1.808 % |
c ==============================================================================
c [1mFound solution: 1004[0m
c ---[   0]---> Adder-cost: 7750   maxlim: 38996   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1052 |  107348   334850 |   35782    1052   103950    98.8 |  1.808 % |
c |      1153 |  107348   334850 |   39360    1153   107715    93.4 |  1.396 % |
c |      1304 |  107348   334850 |   43296    1304   116225    89.1 |  1.396 % |
c |      1529 |  107348   334850 |   47625    1529   123219    80.6 |  1.396 % |
c |      1866 |  107348   334850 |   52388    1866   156815    84.0 |  1.396 % |
c ==============================================================================
c [1mFound solution: 1002[0m
c ---[   0]---> Adder-cost: 0   maxlim: 38998   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2203 |  107352   334879 |   35784    2203   222373   100.9 |  1.396 % |
c |      2303 |  107352   334879 |   39362    2303   231648   100.6 |  1.403 % |
c |      2454 |  107352   334879 |   43298    2454   238130    97.0 |  1.403 % |
c |      2679 |  107352   334879 |   47628    2679   261418    97.6 |  1.403 % |
c |      3017 |  107352   334879 |   52391    3017   299302    99.2 |  1.403 % |
c |      3523 |  107352   334879 |   57630    3523   358994   101.9 |  1.403 % |
c |      4282 |  107352   334879 |   63393    4282   556963   130.1 |  1.403 % |
c |      5423 |  107352   334879 |   69732    5423   668556   123.3 |  1.403 % |
c |      7131 |  107352   334879 |   76706    7131  1051149   147.4 |  1.403 % |
c |      9693 |  107352   334879 |   84376    9693  1678687   173.2 |  1.403 % |
c ==============================================================================
c [1mFound solution: 996[0m
c ---[   0]---> Adder-cost: 0   maxlim: 39004   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10487 |  107358   334918 |   35786   10487  1847516   176.2 |  1.403 % |
c |     10587 |  107358   334918 |   39364   10587  1855693   175.3 |  1.412 % |
c |     10742 |  107358   334918 |   43301   10742  1874690   174.5 |  1.412 % |
c |     10967 |  107358   334918 |   47631   10967  1906062   173.8 |  1.412 % |
c |     11305 |  107358   334918 |   52394   11305  1959943   173.4 |  1.412 % |
c |     11812 |  107358   334918 |   57633   11812  1996652   169.0 |  1.412 % |
c |     12571 |  107358   334918 |   63397   12571  2137300   170.0 |  1.412 % |
c |     13711 |  107358   334918 |   69736   13711  2382440   173.8 |  1.412 % |
c |     15420 |  107358   334918 |   76710   15420  2702133   175.2 |  1.412 % |
c |     17982 |  107358   334918 |   84381   17982  3128960   174.0 |  1.412 % |
c |     21828 |  107358   334918 |   92819   21828  4322375   198.0 |  1.412 % |
c ==============================================================================
c [1mFound solution: 988[0m
c ---[   0]---> Adder-cost: 0   maxlim: 39012   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26309 |  107364   334954 |   35788   26309  5311365   201.9 |  1.412 % |
c |     26410 |  107364   334954 |   39366   26410  5315345   201.3 |  1.422 % |
c |     26560 |  107364   334954 |   43303   26560  5332309   200.8 |  1.422 % |
c |     26785 |  107364   334954 |   47633   26785  5362018   200.2 |  1.422 % |
c |     27124 |  107364   334954 |   52397   27124  5390674   198.7 |  1.422 % |
c |     27630 |  107364   334954 |   57636   27630  5447812   197.2 |  1.422 % |
c |     28389 |  107364   334954 |   63400   28389  5585909   196.8 |  1.422 % |
c |     29531 |  107364   334954 |   69740   29531  5829841   197.4 |  1.422 % |
c |     31240 |  107364   334954 |   76714   31240  6204331   198.6 |  1.422 % |
c |     33803 |  107364   334954 |   84386   33803  6860637   203.0 |  1.422 % |
c ==============================================================================
c [1mFound solution: 968[0m
c ---[   0]---> Adder-cost: 0   maxlim: 39032   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36639 |  107367   334983 |   35789   36639  7564651   206.5 |  1.422 % |
c |     36739 |  107367   334983 |   39367   14978  2527851   168.8 |  1.432 % |
c |     36890 |  107367   334983 |   43304   15129  2533125   167.4 |  1.432 % |
c |     37115 |  107367   334983 |   47635   15354  2573774   167.6 |  1.432 % |
c |     37454 |  107367   334983 |   52398   15693  2610219   166.3 |  1.432 % |
c |     37961 |  107367   334983 |   57638   16200  2689774   166.0 |  1.432 % |
c |     38720 |  107367   334983 |   63402   16959  2861332   168.7 |  1.432 % |
c |     39859 |  107367   334983 |   69742   18098  3049027   168.5 |  1.432 % |
c |     41567 |  107367   334983 |   76716   19806  3582639   180.9 |  1.432 % |
c |     44129 |  107367   334983 |   84388   22368  4081259   182.5 |  1.432 % |
c |     47975 |  107367   334983 |   92827   26214  4924789   187.9 |  1.432 % |
c |     53742 |  107367   334983 |  102110   31981  6839322   213.9 |  1.432 % |
c |     62393 |  107367   334983 |  112321   40632  9147539   225.1 |  1.432 % |
c |     75367 |  107367   334983 |  123553   53606 13432995   250.6 |  1.432 % |
c |     94828 |  107367   334983 |  135908   73067 18583473   254.3 |  1.432 % |
c ==============================================================================
c [1mFound solution: 962[0m
c ---[   0]---> Adder-cost: 0   maxlim: 39038   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102932 |  107372   335020 |   35790   81171 21091129   259.8 |  1.432 % |
c |    103038 |  107372   335020 |   39369   18351  3797324   206.9 |  1.441 % |
c |    103188 |  107372   335020 |   43305   18501  3819105   206.4 |  1.441 % |
c |    103414 |  107372   335020 |   47636   18727  3851268   205.7 |  1.441 % |
c |    103751 |  107372   335020 |   52400   19064  3898650   204.5 |  1.441 % |
c |    104258 |  107372   335020 |   57640   19571  3960880   202.4 |  1.441 % |
c |    105018 |  107372   335020 |   63404   20331  4055134   199.5 |  1.441 % |
c |    106157 |  107372   335020 |   69744   21470  4306107   200.6 |  1.441 % |
c |    107866 |  107372   335020 |   76719   23179  4672492   201.6 |  1.441 % |
c |    110428 |  107372   335020 |   84390   25741  5195896   201.9 |  1.441 % |
c |    114274 |  107372   335020 |   92830   29587  5870348   198.4 |  1.441 % |
c |    120042 |  107372   335020 |  102113   35355  7088827   200.5 |  1.441 % |
c |    128698 |  107372   335020 |  112324   44011  9766073   221.9 |  1.441 % |
c |    141672 |  107372   335020 |  123556   56985 14217045   249.5 |  1.441 % |
c |    161142 |  107372   335020 |  135912   76455 21190245   277.2 |  1.441 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  5709 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): 0.94 0.98 0.95 2/54 5705
Raw data (stat): 5705 (runsolver) R 5704 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842387227 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.95 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0014 s]
Raw data (loadavg): 0.96 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0018 s]
Raw data (loadavg): 0.97 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0019 s]
Raw data (loadavg): 0.97 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.003 s]
Raw data (loadavg): 0.97 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0032 s]
Raw data (loadavg): 0.98 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0042 s]
Raw data (loadavg): 0.98 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0053 s]
Raw data (loadavg): 0.98 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0045 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.01 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.013 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.019 s]
Raw data (loadavg): 1.07 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.02 s]
Raw data (loadavg): 1.06 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.02 s]
Raw data (loadavg): 1.05 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.021 s]
Raw data (loadavg): 1.04 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.021 s]
Raw data (loadavg): 1.04 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.021 s]
Raw data (loadavg): 1.03 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.022 s]
Raw data (loadavg): 1.03 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.022 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.023 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.023 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.022 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.022 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.022 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.022 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.74 s]
Raw data (loadavg): 1.00 1.00 0.95 1/53 5709
Raw data (stat): 5705 (minisat+_script) S 5704 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842387227 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.74
CPU time (s): 1229.89
CPU user time (s): 1228.9
CPU system time (s): 0.98485
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####