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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0548.opb
MD5SUM6f47095f2d417d23ced995954e641689
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 14938
Optimality of the best value was proved NO
Number of terms in the objective function 416
Biggest coefficient in the objective function 11000
Number of bits for the biggest coefficient in the objective function 14
Sum of the numbers in the objective function 96797
Number of bits of the sum of numbers in the objective function 17
Biggest number in a constraint 11000
Number of bits of the biggest number in a constraint 14
Biggest sum of numbers in a constraint 96797
Number of bits of the biggest sum of numbers17
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1236.51
Number of variables548
Total number of constraints724
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)550
Number of constraints which are nor clauses,nor cardinality constraints134
Minimum length of a constraint1
Maximum length of a constraint143

Trace number 22053 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-22 02:00:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12160 boxname=wulflinc26 idbench=936 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6f47095f2d417d23ced995954e641689  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-p0548.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-p0548.opb
IDLAUNCH: 12160
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        257812 kB
Buffers:         33616 kB
Cached:         716016 kB
SwapCached:         68 kB
Active:         199696 kB
Inactive:       552800 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        257532 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6880 kB
Slab:            18688 kB
Committed_AS:    63724 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:20:55 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 12160 7 1200.16 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssss.s..ssss........................................
c ---[ 164]---> BDD-cost:   12
c ---[ 163]---> BDD-cost:   46
c ---[ 162]---> BDD-cost:   27
c ---[ 161]---> BDD-cost:    8
c ---[ 160]---> BDD-cost:   48
c ---[ 159]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:   75
c ---[ 156]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   54
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:  105
c ---[ 151]---> BDD-cost:  104
c ---[ 150]---> BDD-cost:  120
c ---[ 149]---> BDD-cost:   79
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:  115
c ---[ 146]---> BDD-cost:  107
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:   55
c ---[ 143]---> BDD-cost:   87
c ---[ 142]---> BDD-cost:   54
c ---[ 141]---> BDD-cost:  164
c ---[ 140]---> BDD-cost:  151
c ---[ 139]---> BDD-cost:   31
c ---[ 138]---> BDD-cost:   26
c ---[ 136]---> BDD-cost:   28
c ---[ 135]---> BDD-cost:   77
c ---[ 134]---> BDD-cost:  153
c ---[ 133]---> BDD-cost:  109
c ---[ 131]---> BDD-cost:  137
c ---[ 130]---> BDD-cost:    6
c ---[ 129]---> BDD-cost:   56
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:    7
c ---[ 126]---> BDD-cost:   32
c ---[ 125]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   14
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:   19
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   24
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:   29
c ---[ 112]---> BDD-cost:    6
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:   29
c ---[ 109]---> BDD-cost:   51
c ---[ 107]---> BDD-cost:    8
c ---[ 106]---> BDD-cost:   35
c ---[ 105]---> BDD-cost:   24
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:   29
c ---[ 101]---> BDD-cost:   13
c ---[ 100]---> BDD-cost:   49
c ---[  99]---> BDD-cost:   60
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:   12
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   16
c ---[  93]---> BDD-cost:   68
c ---[  92]---> BDD-cost:   78
c ---[  91]---> BDD-cost:   47
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   68
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:   20
c ---[  86]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   12
c ---[  80]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[  79]---> Sorter-cost: 1212     Base: 2 3 2 3
c ---[  78]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  77]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  76]---> BDD-cost:   37
c ---[  75]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  71]---> BDD-cost:    3
c ---[  69]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  57]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  53]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  41]---> BDD-cost:    3
c ---[  33]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   49
c ---[  12]---> BDD-cost:   49
c ---[  11]---> BDD-cost:   26
c ---[  10]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    7
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:   11
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:   20
c ---[   4]---> BDD-cost:    4
c ---[   3]---> BDD-cost:    2
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    2
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   19073    57623 |    6357       0        0     nan |  0.000 % |
c |       100 |   19073    57623 |    6992     100      672     6.7 |  2.555 % |
c |       252 |   19057    57569 |    7691     247     1692     6.9 |  2.591 % |
c |       477 |   19057    57569 |    8461     472     5450    11.5 |  2.591 % |
c |       815 |   19057    57569 |    9307     810    10043    12.4 |  2.591 % |
c |      1321 |   19042    57516 |   10238    1311    18125    13.8 |  2.609 % |
c |      2080 |   19012    57412 |   11261    2062    40134    19.5 |  2.664 % |
c |      3220 |   19012    57412 |   12387    3202    69123    21.6 |  2.664 % |
c |      4929 |   18949    57203 |   13626    4904   116688    23.8 |  2.772 % |
c |      7491 |   18925    57134 |   14989    7465   185728    24.9 |  2.808 % |
c |     11337 |   18925    57134 |   16488   11311   347696    30.7 |  2.809 % |
c |     17104 |   18925    57134 |   18137    8643   242756    28.1 |  2.808 % |
c |     25753 |   18925    57134 |   19950   17292   503434    29.1 |  2.808 % |
c |     38727 |   18925    57134 |   21946   20110   621158    30.9 |  2.808 % |
c |     58188 |   18885    57000 |   24140   16745   543948    32.5 |  2.917 % |
c |     87380 |   18885    57000 |   26554   20873   764650    36.6 |  2.917 % |
c |    131169 |   18869    56944 |   29210   23294   693331    29.8 |  2.953 % |
c |    196854 |   18869    56944 |   32131   25433  1047150    41.2 |  2.953 % |
c |    295382 |   18869    56944 |   35344   17901   689696    38.5 |  2.954 % |
c |    443173 |   18869    56944 |   38878   17949   602270    33.6 |  2.953 % |
c |    664857 |   18869    56944 |   42766   27238  1062812    39.0 |  2.953 % |
#### 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.79 0.91 0.89 2/54 15078
Raw data (stat): 15078 (runsolver) R 15077 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549961362 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0003 s]
Raw data (loadavg): 0.82 0.91 0.89 2/54 15078
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 1561 0 0 0 994 4 0 0 25 0 1 0 549961362 8118272 1528 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1982 1528 603 41 0 1941 0
vsize: 7928
[startup+20.0008 s]
Raw data (loadavg): 0.85 0.91 0.89 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 1717 0 0 0 1993 4 0 0 25 0 1 0 549961362 8785920 1684 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2145 1684 603 41 0 2104 0
vsize: 8580
[startup+30.0014 s]
Raw data (loadavg): 0.87 0.91 0.89 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 1921 0 0 0 2993 5 0 0 25 0 1 0 549961362 9588736 1888 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2341 1888 603 41 0 2300 0
vsize: 9364
[startup+40.0014 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2167 0 0 0 3992 6 0 0 25 0 1 0 549961362 10530816 2134 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2571 2134 603 41 0 2530 0
vsize: 10284
[startup+50.0018 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2341 0 0 0 4991 6 0 0 25 0 1 0 549961362 11337728 2308 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2308 603 41 0 2727 0
vsize: 11072
[startup+60.0022 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2388 0 0 0 5990 7 0 0 25 0 1 0 549961362 11485184 2355 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2804 2355 603 41 0 2763 0
vsize: 11216
[startup+70.0024 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2404 0 0 0 6990 7 0 0 25 0 1 0 549961362 11485184 2371 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2804 2371 603 41 0 2763 0
vsize: 11216
[startup+80.0032 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2437 0 0 0 7989 8 0 0 25 0 1 0 549961362 11632640 2404 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2840 2404 603 41 0 2799 0
vsize: 11360
[startup+90.0033 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2437 0 0 0 8989 8 0 0 25 0 1 0 549961362 11632640 2404 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2840 2404 603 41 0 2799 0
vsize: 11360
[startup+100.004 s]
Raw data (loadavg): 1.04 0.94 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2447 0 0 0 9989 8 0 0 25 0 1 0 549961362 11796480 2414 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2880 2414 603 41 0 2839 0
vsize: 11520
[startup+110.004 s]
Raw data (loadavg): 1.03 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2468 0 0 0 10988 9 0 0 25 0 1 0 549961362 11796480 2435 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2880 2435 603 41 0 2839 0
vsize: 11520
[startup+120.004 s]
Raw data (loadavg): 1.03 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2509 0 0 0 11987 9 0 0 25 0 1 0 549961362 12075008 2476 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2948 2476 603 41 0 2907 0
vsize: 11792
[startup+130.005 s]
Raw data (loadavg): 1.02 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2551 0 0 0 12988 9 0 0 25 0 1 0 549961362 12210176 2518 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2981 2518 603 41 0 2940 0
vsize: 11924
[startup+140.005 s]
Raw data (loadavg): 1.02 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2679 0 0 0 13987 9 0 0 25 0 1 0 549961362 12746752 2646 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2646 603 41 0 3071 0
vsize: 12448
[startup+150.004 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2691 0 0 0 14988 9 0 0 25 0 1 0 549961362 12746752 2658 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2658 603 41 0 3071 0
vsize: 12448
[startup+160.004 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2874 0 0 0 15987 10 0 0 25 0 1 0 549961362 13557760 2841 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3310 2841 603 41 0 3269 0
vsize: 13240
[startup+170.004 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2883 0 0 0 16987 10 0 0 25 0 1 0 549961362 13557760 2850 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3310 2850 603 41 0 3269 0
vsize: 13240
[startup+180.004 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 2993 0 0 0 17987 11 0 0 25 0 1 0 549961362 14233600 2960 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3475 2960 603 41 0 3434 0
vsize: 13900
[startup+190.004 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3006 0 0 0 18987 11 0 0 25 0 1 0 549961362 14233600 2973 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3475 2973 603 41 0 3434 0
vsize: 13900
[startup+200.004 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3013 0 0 0 19987 11 0 0 25 0 1 0 549961362 14385152 2980 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 2980 603 41 0 3471 0
vsize: 14048
[startup+210.005 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3020 0 0 0 20987 11 0 0 25 0 1 0 549961362 14385152 2987 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 2987 603 41 0 3471 0
vsize: 14048
[startup+220.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3030 0 0 0 21988 11 0 0 25 0 1 0 549961362 14385152 2997 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 2997 603 41 0 3471 0
vsize: 14048
[startup+230.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3052 0 0 0 22988 11 0 0 25 0 1 0 549961362 14581760 3019 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3560 3019 603 41 0 3519 0
vsize: 14240
[startup+240.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3063 0 0 0 23988 11 0 0 25 0 1 0 549961362 14581760 3030 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3560 3030 603 41 0 3519 0
vsize: 14240
[startup+250.004 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3096 0 0 0 24988 11 0 0 25 0 1 0 549961362 14729216 3063 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3596 3063 603 41 0 3555 0
vsize: 14384
[startup+260.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3100 0 0 0 25988 11 0 0 25 0 1 0 549961362 14729216 3067 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3596 3067 603 41 0 3555 0
vsize: 14384
[startup+270.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3116 0 0 0 26988 11 0 0 25 0 1 0 549961362 14893056 3083 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3636 3083 603 41 0 3595 0
vsize: 14544
[startup+280.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 15080
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3131 0 0 0 27989 11 0 0 25 0 1 0 549961362 14893056 3098 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3636 3098 603 41 0 3595 0
vsize: 14544
[startup+290.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3131 0 0 0 28989 11 0 0 25 0 1 0 549961362 14893056 3098 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3636 3098 603 41 0 3595 0
vsize: 14544
[startup+300.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3131 0 0 0 29989 11 0 0 25 0 1 0 549961362 14893056 3098 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3636 3098 603 41 0 3595 0
vsize: 14544
[startup+310.004 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3151 0 0 0 30988 11 0 0 25 0 1 0 549961362 15040512 3118 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3672 3118 603 41 0 3631 0
vsize: 14688
[startup+320.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3171 0 0 0 31989 11 0 0 25 0 1 0 549961362 15040512 3138 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3672 3138 603 41 0 3631 0
vsize: 14688
[startup+330.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3190 0 0 0 32989 11 0 0 25 0 1 0 549961362 15204352 3157 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3157 603 41 0 3671 0
vsize: 14848
[startup+340.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3190 0 0 0 33989 11 0 0 25 0 1 0 549961362 15204352 3157 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3157 603 41 0 3671 0
vsize: 14848
[startup+350.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3200 0 0 0 34989 11 0 0 25 0 1 0 549961362 15204352 3167 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3167 603 41 0 3671 0
vsize: 14848
[startup+360.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3210 0 0 0 35989 11 0 0 25 0 1 0 549961362 15204352 3177 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3177 603 41 0 3671 0
vsize: 14848
[startup+370.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3210 0 0 0 36989 11 0 0 25 0 1 0 549961362 15204352 3177 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3177 603 41 0 3671 0
vsize: 14848
[startup+380.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3210 0 0 0 37990 11 0 0 25 0 1 0 549961362 15204352 3177 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3177 603 41 0 3671 0
vsize: 14848
[startup+390.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3210 0 0 0 38990 11 0 0 25 0 1 0 549961362 15204352 3177 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3177 603 41 0 3671 0
vsize: 14848
[startup+400.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3212 0 0 0 39990 11 0 0 25 0 1 0 549961362 15204352 3179 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3179 603 41 0 3671 0
vsize: 14848
[startup+410.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3212 0 0 0 40990 11 0 0 25 0 1 0 549961362 15204352 3179 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3179 603 41 0 3671 0
vsize: 14848
[startup+420.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3277 0 0 0 41990 11 0 0 25 0 1 0 549961362 15474688 3244 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3778 3244 603 41 0 3737 0
vsize: 15112
[startup+430.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3292 0 0 0 42990 11 0 0 25 0 1 0 549961362 15618048 3259 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3813 3259 603 41 0 3772 0
vsize: 15252
[startup+440.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3324 0 0 0 43990 11 0 0 25 0 1 0 549961362 15761408 3291 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3848 3291 603 41 0 3807 0
vsize: 15392
[startup+450.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3326 0 0 0 44991 11 0 0 25 0 1 0 549961362 15761408 3293 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3848 3293 603 41 0 3807 0
vsize: 15392
[startup+460.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3337 0 0 0 45991 11 0 0 25 0 1 0 549961362 15761408 3304 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3848 3304 603 41 0 3807 0
vsize: 15392
[startup+470.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3358 0 0 0 46991 11 0 0 25 0 1 0 549961362 15941632 3325 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3892 3325 603 41 0 3851 0
vsize: 15568
[startup+480.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3358 0 0 0 47991 11 0 0 25 0 1 0 549961362 15941632 3325 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3892 3325 603 41 0 3851 0
vsize: 15568
[startup+490.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3366 0 0 0 48991 11 0 0 25 0 1 0 549961362 15941632 3333 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3892 3333 603 41 0 3851 0
vsize: 15568
[startup+500.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3379 0 0 0 49991 11 0 0 25 0 1 0 549961362 16105472 3346 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3932 3346 603 41 0 3891 0
vsize: 15728
[startup+510.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3379 0 0 0 50991 12 0 0 25 0 1 0 549961362 16105472 3346 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3932 3346 603 41 0 3891 0
vsize: 15728
[startup+520.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3401 0 0 0 51990 12 0 0 25 0 1 0 549961362 16105472 3368 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3932 3368 603 41 0 3891 0
vsize: 15728
[startup+530.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3440 0 0 0 52990 12 0 0 25 0 1 0 549961362 16240640 3407 4294967295 134512640 134672761 3221224624 3221223808 134559373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3965 3407 603 41 0 3924 0
vsize: 15860
[startup+540.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3456 0 0 0 53990 12 0 0 25 0 1 0 549961362 16375808 3423 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3998 3423 603 41 0 3957 0
vsize: 15992
[startup+550.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3475 0 0 0 54990 12 0 0 25 0 1 0 549961362 16515072 3442 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4032 3442 603 41 0 3991 0
vsize: 16128
[startup+560.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3496 0 0 0 55990 12 0 0 25 0 1 0 549961362 16515072 3463 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4032 3463 603 41 0 3991 0
vsize: 16128
[startup+570.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3573 0 0 0 56990 13 0 0 25 0 1 0 549961362 16928768 3540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4133 3540 603 41 0 4092 0
vsize: 16532
[startup+580.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3584 0 0 0 57991 13 0 0 25 0 1 0 549961362 16928768 3551 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4133 3551 603 41 0 4092 0
vsize: 16532
[startup+590.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3589 0 0 0 58991 13 0 0 25 0 1 0 549961362 16928768 3556 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4133 3556 603 41 0 4092 0
vsize: 16532
[startup+600.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3617 0 0 0 59991 13 0 0 25 0 1 0 549961362 17063936 3584 4294967295 134512640 134672761 3221224624 3221223888 134562211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4166 3584 603 41 0 4125 0
vsize: 16664
[startup+610.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3617 0 0 0 60991 13 0 0 25 0 1 0 549961362 17063936 3584 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4166 3584 603 41 0 4125 0
vsize: 16664
[startup+620.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3649 0 0 0 61991 13 0 0 25 0 1 0 549961362 17207296 3616 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4201 3616 603 41 0 4160 0
vsize: 16804
[startup+630.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3651 0 0 0 62991 13 0 0 25 0 1 0 549961362 17207296 3618 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4201 3618 603 41 0 4160 0
vsize: 16804
[startup+640.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3651 0 0 0 63991 13 0 0 25 0 1 0 549961362 17207296 3618 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4201 3618 603 41 0 4160 0
vsize: 16804
[startup+650.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3659 0 0 0 64992 13 0 0 25 0 1 0 549961362 17207296 3626 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4201 3626 603 41 0 4160 0
vsize: 16804
[startup+660.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3663 0 0 0 65991 13 0 0 25 0 1 0 549961362 17207296 3630 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4201 3630 603 41 0 4160 0
vsize: 16804
[startup+670.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3663 0 0 0 66991 14 0 0 25 0 1 0 549961362 17207296 3630 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4201 3630 603 41 0 4160 0
vsize: 16804
[startup+680.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3673 0 0 0 67991 14 0 0 25 0 1 0 549961362 17371136 3640 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4241 3640 603 41 0 4200 0
vsize: 16964
[startup+690.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3674 0 0 0 68991 14 0 0 25 0 1 0 549961362 17371136 3641 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4241 3641 603 41 0 4200 0
vsize: 16964
[startup+700.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3715 0 0 0 69991 14 0 0 25 0 1 0 549961362 17506304 3682 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4274 3682 603 41 0 4233 0
vsize: 17096
[startup+710.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3718 0 0 0 70992 14 0 0 25 0 1 0 549961362 17506304 3685 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4274 3685 603 41 0 4233 0
vsize: 17096
[startup+720.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3734 0 0 0 71992 14 0 0 25 0 1 0 549961362 17670144 3701 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4314 3701 603 41 0 4273 0
vsize: 17256
[startup+730.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3765 0 0 0 72992 14 0 0 25 0 1 0 549961362 17833984 3732 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4354 3732 603 41 0 4313 0
vsize: 17416
[startup+740.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3785 0 0 0 73992 15 0 0 25 0 1 0 549961362 17833984 3752 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4354 3752 603 41 0 4313 0
vsize: 17416
[startup+750.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3788 0 0 0 74992 15 0 0 25 0 1 0 549961362 17833984 3755 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4354 3755 603 41 0 4313 0
vsize: 17416
[startup+760.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3806 0 0 0 75992 15 0 0 25 0 1 0 549961362 17985536 3773 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4391 3773 603 41 0 4350 0
vsize: 17564
[startup+770.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3809 0 0 0 76992 15 0 0 25 0 1 0 549961362 17985536 3776 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4391 3776 603 41 0 4350 0
vsize: 17564
[startup+780.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3812 0 0 0 77992 15 0 0 25 0 1 0 549961362 17985536 3779 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4391 3779 603 41 0 4350 0
vsize: 17564
[startup+790.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3820 0 0 0 78993 15 0 0 25 0 1 0 549961362 17985536 3787 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4391 3787 603 41 0 4350 0
vsize: 17564
[startup+800.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3825 0 0 0 79993 15 0 0 25 0 1 0 549961362 18137088 3792 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4428 3792 603 41 0 4387 0
vsize: 17712
[startup+810.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3825 0 0 0 80993 15 0 0 25 0 1 0 549961362 18137088 3792 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4428 3792 603 41 0 4387 0
vsize: 17712
[startup+820.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3825 0 0 0 81993 15 0 0 25 0 1 0 549961362 18137088 3792 4294967295 134512640 134672761 3221224624 3221223808 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4428 3792 603 41 0 4387 0
vsize: 17712
[startup+830.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 3825 0 0 0 82993 15 0 0 25 0 1 0 549961362 18137088 3792 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4428 3792 603 41 0 4387 0
vsize: 17712
[startup+840.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4009 0 0 0 83991 16 0 0 25 0 1 0 549961362 18808832 3976 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4592 3976 603 41 0 4551 0
vsize: 18368
[startup+850.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4026 0 0 0 84991 16 0 0 25 0 1 0 549961362 18952192 3993 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4627 3993 603 41 0 4586 0
vsize: 18508
[startup+860.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4038 0 0 0 85991 16 0 0 25 0 1 0 549961362 18952192 4005 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4627 4005 603 41 0 4586 0
vsize: 18508
[startup+870.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4049 0 0 0 86992 16 0 0 25 0 1 0 549961362 18952192 4016 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4627 4016 603 41 0 4586 0
vsize: 18508
[startup+880.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4162 0 0 0 87992 16 0 0 25 0 1 0 549961362 19488768 4129 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4758 4129 603 41 0 4717 0
vsize: 19032
[startup+890.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4267 0 0 0 88991 16 0 0 25 0 1 0 549961362 19947520 4234 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4870 4234 603 41 0 4829 0
vsize: 19480
[startup+900.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4280 0 0 0 89991 17 0 0 25 0 1 0 549961362 19947520 4247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4870 4247 603 41 0 4829 0
vsize: 19480
[startup+910.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4294 0 0 0 90991 17 0 0 25 0 1 0 549961362 20086784 4261 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4261 603 41 0 4863 0
vsize: 19616
[startup+920.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4295 0 0 0 91992 17 0 0 25 0 1 0 549961362 20086784 4262 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4262 603 41 0 4863 0
vsize: 19616
[startup+930.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4295 0 0 0 92992 17 0 0 25 0 1 0 549961362 20086784 4262 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4262 603 41 0 4863 0
vsize: 19616
[startup+940.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4295 0 0 0 93992 17 0 0 25 0 1 0 549961362 20086784 4262 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4262 603 41 0 4863 0
vsize: 19616
[startup+950.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4295 0 0 0 94992 17 0 0 25 0 1 0 549961362 20086784 4262 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4262 603 41 0 4863 0
vsize: 19616
[startup+960.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4306 0 0 0 95992 17 0 0 25 0 1 0 549961362 20086784 4273 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4273 603 41 0 4863 0
vsize: 19616
[startup+970.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4306 0 0 0 96992 17 0 0 25 0 1 0 549961362 20086784 4273 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4273 603 41 0 4863 0
vsize: 19616
[startup+980.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4306 0 0 0 97993 17 0 0 25 0 1 0 549961362 20086784 4273 4294967295 134512640 134672761 3221224624 3221223856 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4273 603 41 0 4863 0
vsize: 19616
[startup+990.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4313 0 0 0 98993 17 0 0 25 0 1 0 549961362 20086784 4280 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4904 4280 603 41 0 4863 0
vsize: 19616
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4323 0 0 0 99993 17 0 0 25 0 1 0 549961362 20234240 4290 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4290 603 41 0 4899 0
vsize: 19760
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4324 0 0 0 100993 17 0 0 25 0 1 0 549961362 20234240 4291 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4291 603 41 0 4899 0
vsize: 19760
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4329 0 0 0 101993 17 0 0 25 0 1 0 549961362 20234240 4296 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4296 603 41 0 4899 0
vsize: 19760
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4334 0 0 0 102994 17 0 0 25 0 1 0 549961362 20234240 4301 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 4301 603 41 0 4899 0
vsize: 19760
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4343 0 0 0 103994 17 0 0 25 0 1 0 549961362 20398080 4310 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4310 603 41 0 4939 0
vsize: 19920
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4346 0 0 0 104994 17 0 0 25 0 1 0 549961362 20398080 4313 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4313 603 41 0 4939 0
vsize: 19920
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4346 0 0 0 105994 17 0 0 25 0 1 0 549961362 20398080 4313 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4313 603 41 0 4939 0
vsize: 19920
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4346 0 0 0 106994 17 0 0 25 0 1 0 549961362 20398080 4313 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4313 603 41 0 4939 0
vsize: 19920
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4346 0 0 0 107994 17 0 0 25 0 1 0 549961362 20398080 4313 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4313 603 41 0 4939 0
vsize: 19920
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4346 0 0 0 108995 17 0 0 25 0 1 0 549961362 20398080 4313 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4313 603 41 0 4939 0
vsize: 19920
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4349 0 0 0 109995 17 0 0 25 0 1 0 549961362 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4349 0 0 0 110995 17 0 0 25 0 1 0 549961362 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4349 0 0 0 111995 17 0 0 25 0 1 0 549961362 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4349 0 0 0 112995 17 0 0 25 0 1 0 549961362 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4349 0 0 0 113995 17 0 0 25 0 1 0 549961362 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4349 0 0 0 114996 17 0 0 25 0 1 0 549961362 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4349 0 0 0 115996 17 0 0 25 0 1 0 549961362 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4349 0 0 0 116996 17 0 0 25 0 1 0 549961362 20398080 4316 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4980 4316 603 41 0 4939 0
vsize: 19920
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4401 0 0 0 117996 17 0 0 25 0 1 0 549961362 20533248 4368 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5013 4368 603 41 0 4972 0
vsize: 20052
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4401 0 0 0 118996 17 0 0 25 0 1 0 549961362 20533248 4368 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5013 4368 603 41 0 4972 0
vsize: 20052
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 15082
Raw data (stat): 15078 (minisat+) R 15077 22612 22611 0 -1 0 4406 0 0 0 119996 17 0 0 25 0 1 0 549961362 20533248 4373 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5013 4373 603 41 0 4972 0
vsize: 20052
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 15082
Raw data (stat): 15078 (minisat+) Z 15077 22612 22611 0 -1 12 4408 0 0 0 119996 18 0 0 25 0 1 0 549961362 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.02
CPU time (s): 1200.16
CPU user time (s): 1199.97
CPU system time (s): 0.186971
CPU usage (%): 100.011
Max. virtual memory (Kb): 20052
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####