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-ran10x10a.opb
MD5SUM	3d332eb7d51bcc8080712302c467a201
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5528305
Optimality of the best value was proved	NO
Number of terms in the objective function	3100
Biggest coefficient in the objective function	4831838208
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	550843571711
Number of bits of the sum of numbers in the objective function	40
Biggest number in a constraint	4831838208
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	550843571711
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	1251.11
Number of variables	3100
Total number of constraints	120
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	120
Minimum length of a constraint	31
Maximum length of a constraint	300
Trace number 30874

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-05-25 20:26:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22277 boxname=wulflinc24 idbench=1093 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  3d332eb7d51bcc8080712302c467a201  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-ran10x10a.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-ran10x10a.opb
IDLAUNCH: 22277
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 3
cpu MHz		: 451.080
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:        547536 kB
Buffers:         32800 kB
Cached:         432412 kB
SwapCached:        588 kB
Active:          83044 kB
Inactive:       384216 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        547284 kB
SwapTotal:     2097892 kB
SwapFree:      2096416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5160 kB
Slab:            14228 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 20:46:52 (client local time) WITH STATUS 152 IN 1229.9 SECONDS
stats: 22277 7 1229.9 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Adder-cost: 232   maxlim: 66550   bits: 17/17
c ---[ 136]---> Adder-cost: 232   maxlim: 69622   bits: 17/17
c ---[ 134]---> Adder-cost: 232   maxlim: 66550   bits: 17/17
c ---[ 132]---> Sorter-cost: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 2690     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Adder-cost: 232   maxlim: 67574   bits: 17/17
c ---[ 120]---> Sorter-cost: 2650     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 2522     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2682     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 248   maxlim: 131062   bits: 18/17
c ---[ 112]---> Sorter-cost: 2682     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 2682     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 2306     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 2306     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2522     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2682     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Adder-cost: 248   maxlim: 130038   bits: 18/17
c ---[  99]---> BDD-cost:   14
c ---[  98]---> BDD-cost:   16
c ---[  97]---> BDD-cost:   14
c ---[  96]---> BDD-cost:   14
c ---[  95]---> BDD-cost:   14
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   14
c ---[  90]---> BDD-cost:   14
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:   14
c ---[  87]---> BDD-cost:   16
c ---[  86]---> BDD-cost:   14
c ---[  85]---> BDD-cost:   16
c ---[  84]---> BDD-cost:   16
c ---[  83]---> BDD-cost:   16
c ---[  82]---> BDD-cost:   16
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   14
c ---[  79]---> BDD-cost:   16
c ---[  78]---> BDD-cost:   16
c ---[  77]---> BDD-cost:   16
c ---[  76]---> BDD-cost:   16
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   18
c ---[  72]---> BDD-cost:   18
c ---[  71]---> BDD-cost:   18
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   14
c ---[  68]---> BDD-cost:   16
c ---[  67]---> BDD-cost:   18
c ---[  66]---> BDD-cost:   18
c ---[  65]---> BDD-cost:   16
c ---[  64]---> BDD-cost:   14
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   16
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   16
c ---[  55]---> BDD-cost:   16
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   14
c ---[  52]---> BDD-cost:   15
c ---[  51]---> BDD-cost:   18
c ---[  50]---> BDD-cost:   18
c ---[  49]---> BDD-cost:   18
c ---[  48]---> BDD-cost:   13
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   16
c ---[  45]---> BDD-cost:   18
c ---[  44]---> BDD-cost:   18
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   18
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   18
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   14
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   18
c ---[  33]---> BDD-cost:   18
c ---[  32]---> BDD-cost:   16
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   16
c ---[  28]---> BDD-cost:   18
c ---[  27]---> BDD-cost:   18
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   16
c ---[  23]---> BDD-cost:   18
c ---[  22]---> BDD-cost:   16
c ---[  21]---> BDD-cost:   16
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   15
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   15
c ---[  10]---> BDD-cost:   16
c ---[   9]---> BDD-cost:   14
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   18
c ---[   6]---> BDD-cost:   18
c ---[   5]---> BDD-cost:   18
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   18
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  105952   260824 |   35317       0        0     nan |  0.000 % |
c |       100 |  105935   260773 |   38848      99      468     4.7 |  7.610 % |
c |       250 |  105701   260236 |   42733     247     1159     4.7 |  7.819 % |
c |       475 |  105677   260183 |   47006     471     2404     5.1 |  7.838 % |
c |       812 |  105400   259551 |   51707     779     3862     5.0 |  8.047 % |
c |      1318 |  105400   259551 |   56878    1285     6450     5.0 |  8.047 % |
c |      2077 |  105188   259057 |   62566    2012    10148     5.0 |  8.204 % |
c |      3216 |  105120   258900 |   68822    3147    16646     5.3 |  8.256 % |
c |      4926 |  104955   258526 |   75705    4820    25302     5.2 |  8.384 % |
c |      7489 |  104772   258074 |   83275    7357    39774     5.4 |  8.511 % |
c |     11333 |  104382   257179 |   91603   11177    62436     5.6 |  8.820 % |
c |     17099 |  104115   256473 |  100763   16903   104973     6.2 |  9.016 % |
c ==============================================================================
c [1mFound solution: 13885611[0m
c ---[   0]---> Adder-cost: 4857   maxlim: 5520724   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22446 |  137609   376650 |   45869   22208   140613     6.3 |  9.016 % |
c |     22546 |  137609   376650 |   50455   22308   141070     6.3 |  8.299 % |
c |     22699 |  137609   376650 |   55501   22461   142029     6.3 |  8.299 % |
c |     22925 |  137609   376650 |   61051   22687   143193     6.3 |  8.299 % |
c |     23262 |  137586   376584 |   67156   23020   145283     6.3 |  8.311 % |
c |     23768 |  137586   376584 |   73872   23526   151785     6.5 |  8.311 % |
c |     24528 |  137502   376383 |   81259   24281   157145     6.5 |  8.369 % |
c |     25667 |  137157   375584 |   89385   25405   184866     7.3 |  8.628 % |
c |     27376 |  136877   374942 |   98324   27091   201826     7.4 |  8.829 % |
c |     29938 |  136727   374583 |  108156   29635   224383     7.6 |  8.932 % |
c ==============================================================================
c [1mFound solution: 12972970[0m
c ---[   0]---> Adder-cost: 0   maxlim: 6433365   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32130 |  136701   374647 |   45567   31824   285417     9.0 |  8.932 % |
c |     32230 |  136701   374647 |   50123   31924   285895     9.0 |  8.982 % |
c |     32380 |  136701   374647 |   55136   32074   286809     8.9 |  8.982 % |
c |     32605 |  136701   374647 |   60649   32299   288289     8.9 |  8.982 % |
c |     32944 |  136701   374647 |   66714   32638   295724     9.1 |  8.982 % |
c |     33450 |  136666   374530 |   73386   33136   300030     9.1 |  8.999 % |
c |     34209 |  136666   374530 |   80724   33895   309212     9.1 |  8.999 % |
c |     35348 |  136666   374530 |   88797   35034   325421     9.3 |  8.999 % |
c |     37057 |  136666   374530 |   97676   36743   440968    12.0 |  8.999 % |
c |     39619 |  136305   373685 |  107444   39218   505665    12.9 |  9.255 % |
c ==============================================================================
c [1mFound solution: 10129983[0m
c ---[   0]---> Adder-cost: 2   maxlim: 9276352   bits: 25/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41006 |  136313   373851 |   45437   40604   553644    13.6 |  9.255 % |
c |     41108 |  136313   373851 |   49980   40706   554316    13.6 |  9.298 % |
c |     41258 |  136313   373851 |   54978   40856   555377    13.6 |  9.298 % |
c |     41483 |  136313   373851 |   60476   41081   557298    13.6 |  9.298 % |
c |     41821 |  136313   373851 |   66524   41419   562660    13.6 |  9.298 % |
c |     42327 |  136313   373851 |   73176   41925   610710    14.6 |  9.298 % |
c ==============================================================================
c [1mFound solution: 6238557[0m
c ---[   0]---> Adder-cost: 0   maxlim: 13167778   bits: 25/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42992 |  136336   374062 |   45445   42590   626476    14.7 |  9.298 % |
c |     43092 |  136336   374062 |   49989   42690   627115    14.7 |  9.321 % |
c |     43242 |  136326   374039 |   54988   42837   628148    14.7 |  9.328 % |
c |     43467 |  136087   373489 |   60487   43053   630148    14.6 |  9.517 % |
c |     43806 |  136080   373469 |   66536   43386   634725    14.6 |  9.520 % |
c |     44312 |  136080   373469 |   73189   43892   674733    15.4 |  9.520 % |
c |     45071 |  135969   373196 |   80508   44621   696498    15.6 |  9.592 % |
c |     46213 |  135810   372830 |   88559   45755   818161    17.9 |  9.714 % |
c |     47925 |  135776   372754 |   97415   47464   862331    18.2 |  9.738 % |
c |     50487 |  135776   372754 |  107156   50026   961459    19.2 |  9.738 % |
c |     54331 |  135776   372754 |  117872   53870  1087082    20.2 |  9.738 % |
c |     60098 |  135769   372739 |  129659   59636  1365749    22.9 |  9.742 % |
c |     68747 |  135769   372739 |  142625   68285  2836478    41.5 |  9.742 % |
c |     81725 |  135643   372449 |  156888   81227  4880686    60.1 |  9.831 % |
c |    101186 |  135643   372449 |  172577  100688  5841592    58.0 |  9.831 % |
c |    130380 |  135299   371661 |  189835  129858 11287585    86.9 | 10.073 % |
c ==============================================================================
c [1mFound solution: 4817595[0m
c ---[   0]---> Adder-cost: 0   maxlim: 14588740   bits: 25/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    157826 |  135232   371644 |   45077  157293 13236493    84.2 | 10.073 % |
c |    157928 |  135232   371644 |   49584   23672   999874    42.2 | 10.152 % |
c |    158078 |  135232   371644 |   54543   23822  1000603    42.0 | 10.152 % |
c |    158303 |  135232   371644 |   59997   24047  1001647    41.7 | 10.152 % |
c |    158640 |  135232   371644 |   65997   24384  1003560    41.2 | 10.152 % |
c |    159148 |  135232   371644 |   72596   24892  1007068    40.5 | 10.152 % |
c |    159907 |  135232   371644 |   79856   25651  1083344    42.2 | 10.152 % |
c |    161046 |  135232   371644 |   87842   26790  1107384    41.3 | 10.152 % |
c |    162755 |  135152   371456 |   96626   28493  1132266    39.7 | 10.210 % |
c |    165319 |  134957   371007 |  106289   31047  1346858    43.4 | 10.349 % |
c |    169163 |  134957   371007 |  116918   34891  1823221    52.3 | 10.349 % |
c |    174929 |  134881   370834 |  128609   40653  2041380    50.2 | 10.401 % |
c |    183578 |  134873   370814 |  141470   49301  3259264    66.1 | 10.409 % |
c |    196553 |  134627   370237 |  155618   62246  4931548    79.2 | 10.600 % |
c |    216014 |  134335   369561 |  171179   81688  6870066    84.1 | 10.835 % |
c |    245206 |  134298   369477 |  188297  110879 11774666   106.2 | 10.858 % |
c |    288995 |  134268   369406 |  207127  154666 17540922   113.4 | 10.887 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 24837 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.91 0.95 0.97 2/54 24833
Raw data (stat): 24833 (runsolver) R 24832 4613 4612 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841746204 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.0004 s]
Raw data (loadavg): 0.93 0.95 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.0008 s]
Raw data (loadavg): 0.94 0.96 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.0016 s]
Raw data (loadavg): 0.95 0.96 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.0014 s]
Raw data (loadavg): 0.95 0.96 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.0019 s]
Raw data (loadavg): 0.96 0.96 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.0015 s]
Raw data (loadavg): 0.97 0.96 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.0025 s]
Raw data (loadavg): 0.97 0.96 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.0029 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.0026 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.98 0.96 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.004 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.004 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.004 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.004 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.003 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.004 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.005 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.006 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.007 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 1.07 0.99 0.98 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 1.06 0.99 0.98 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.04 s]
Raw data (loadavg): 1.05 0.99 0.98 2/55 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.76 s]
Raw data (loadavg): 1.04 0.99 0.98 1/53 24837
Raw data (stat): 24833 (minisat+_script) S 24832 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841746204 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.76
CPU time (s): 1229.9
CPU user time (s): 1228.77
CPU system time (s): 1.12983
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####