PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-cracpb1.opb
MD5SUM	098fe473d82d5f7d4121673eb775be76
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	22199
Optimality of the best value was proved	NO
Number of terms in the objective function	572
Biggest coefficient in the objective function	5000
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	547769
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	5000
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	547769
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	30.8603
Number of variables	572
Total number of constraints	716
Number of constraints which are clauses	3
Number of constraints which are cardinality constraints (but not clauses)	644
Number of constraints which are nor clauses,nor cardinality constraints	69
Minimum length of a constraint	1
Maximum length of a constraint	518
Trace number 19276

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 18:37:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16754 boxname=wulflinc21 idbench=1289 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  098fe473d82d5f7d4121673eb775be76  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-cracpb1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-cracpb1.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-cracpb1.opb
IDLAUNCH: 16754
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        887012 kB
Buffers:          4996 kB
Cached:         121008 kB
SwapCached:          0 kB
Active:          54220 kB
Inactive:        74664 kB
HighTotal:      131008 kB
HighFree:        37520 kB
LowTotal:       903652 kB
LowFree:        849492 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            12984 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:57:23 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 16754 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 215 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #########################################################################################
c   -- Clauses(.)/Splits(s): ...
c ---[ 214]---> Adder-cost: 1416   maxlim: 2733   bits: 12/12
c ---[ 213]---> Adder-cost: 75   maxlim: 13   bits: 5/4
c ---[ 212]---> Adder-cost: 38   maxlim: 10   bits: 5/4
c ---[ 211]---> Adder-cost: 38   maxlim: 12   bits: 5/4
c ---[ 210]---> Adder-cost: 36   maxlim: 8   bits: 5/4
c ---[ 209]---> Adder-cost: 52   maxlim: 5   bits: 4/3
c ---[ 208]---> Adder-cost: 52   maxlim: 7   bits: 4/3
c ---[ 207]---> Adder-cost: 44   maxlim: 13   bits: 5/4
c ---[ 206]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 205]---> Adder-cost: 51   maxlim: 14   bits: 5/4
c ---[ 204]---> Adder-cost: 22   maxlim: 9   bits: 4/4
c ---[ 203]---> Adder-cost: 22   maxlim: 10   bits: 4/4
c ---[ 202]---> Adder-cost: 16   maxlim: 6   bits: 4/3
c ---[ 201]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 200]---> Adder-cost: 16   maxlim: 5   bits: 4/3
c ---[ 199]---> Adder-cost: 32   maxlim: 9   bits: 5/4
c ---[ 198]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 197]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 195]---> Adder-cost: 67   maxlim: 10   bits: 5/4
c ---[ 193]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 191]---> Adder-cost: 38   maxlim: 14   bits: 5/4
c ---[ 189]---> Adder-cost: 36   maxlim: 9   bits: 5/4
c ---[ 187]---> Adder-cost: 61   maxlim: 9   bits: 5/4
c ---[ 185]---> Adder-cost: 38   maxlim: 14   bits: 5/4
c ---[ 183]---> Adder-cost: 44   maxlim: 15   bits: 5/4
c ---[ 181]---> Adder-cost: 32   maxlim: 11   bits: 5/4
c ---[ 179]---> Adder-cost: 46   maxlim: 11   bits: 5/4
c ---[ 177]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 175]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 173]---> Adder-cost: 35   maxlim: 6   bits: 4/3
c ---[ 171]---> Adder-cost: 22   maxlim: 7   bits: 4/3
c ---[ 169]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 167]---> Adder-cost: 30   maxlim: 9   bits: 5/4
c ---[ 165]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 163]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 161]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 159]---> Adder-cost: 155   maxlim: 27   bits: 6/5
c ---[ 157]---> Adder-cost: 74   maxlim: 21   bits: 6/5
c ---[ 155]---> Adder-cost: 80   maxlim: 25   bits: 6/5
c ---[ 153]---> Adder-cost: 76   maxlim: 18   bits: 6/5
c ---[ 151]---> Adder-cost: 108   maxlim: 10   bits: 5/4
c ---[ 149]---> Adder-cost: 108   maxlim: 15   bits: 5/4
c ---[ 147]---> Adder-cost: 81   maxlim: 28   bits: 6/5
c ---[ 145]---> Adder-cost: 52   maxlim: 18   bits: 5/5
c ---[ 143]---> Adder-cost: 106   maxlim: 29   bits: 6/5
c ---[ 141]---> Adder-cost: 52   maxlim: 20   bits: 5/5
c ---[ 139]---> Adder-cost: 46   maxlim: 22   bits: 5/5
c ---[ 137]---> Adder-cost: 44   maxlim: 14   bits: 5/4
c ---[ 135]---> Adder-cost: 64   maxlim: 18   bits: 6/5
c ---[ 133]---> Adder-cost: 36   maxlim: 12   bits: 5/4
c ---[ 131]---> Adder-cost: 64   maxlim: 19   bits: 6/5
c ---[ 129]---> Adder-cost: 32   maxlim: 15   bits: 5/4
c ---[ 127]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 126]---> Adder-cost: 732   maxlim: 1601   bits: 12/11
c ---[ 125]---> Adder-cost: 1184   maxlim: 406   bits: 10/9
c ---[ 124]---> Adder-cost: 255   maxlim: 863   bits: 11/10
c ---[ 123]---> Adder-cost: 20   maxlim: 1   bits: 2/1
c ---[ 122]---> Adder-cost: 20   maxlim: 3   bits: 3/2
c ---[ 121]---> Adder-cost: 32   maxlim: 11   bits: 5/4
c ---[ 120]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 118]---> Adder-cost: 27   maxlim: 3   bits: 3/2
c ---[ 115]---> Adder-cost: 44   maxlim: 2   bits: 3/2
c ---[ 114]---> Adder-cost: 32   maxlim: 9   bits: 5/4
c ---[ 113]---> Adder-cost: 58   maxlim: 20   bits: 6/5
c ---[ 112]---> Adder-cost: 38   maxlim: 8   bits: 5/4
c ---[ 111]---> Adder-cost: 13   maxlim: 1   bits: 2/1
c ---[ 110]---> Adder-cost: 57   maxlim: 9   bits: 5/4
c ---[ 109]---> Adder-cost: 15   maxlim: 1   bits: 2/1
c ---[ 108]---> Adder-cost: 14   maxlim: 1   bits: 2/1
c ---[ 106]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 104]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 102]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 100]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[  98]---> Adder-cost: 82   maxlim: 47   bits: 6/6
c ---[  96]---> Adder-cost: 170   maxlim: 92   bits: 7/7
c ---[  94]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[  92]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[  90]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[  88]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[  86]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[  84]---> Adder-cost: 6   maxlim: 6   bits: 3/3
c ---[  82]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[  80]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[  78]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[  76]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[  74]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[  72]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[  70]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[  68]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[  66]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  64]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[  62]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  60]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ---[  58]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[  56]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[  54]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[  52]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[  50]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  48]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  46]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  44]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[  42]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[  40]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[  38]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[  36]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[  34]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[  32]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[  30]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[  28]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  26]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[  24]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[  22]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[  20]---> Adder-cost: 41   maxlim: 25   bits: 5/5
c ---[  18]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[  16]---> Adder-cost: 8   maxlim: 6   bits: 3/3
c ---[  14]---> Adder-cost: 4   maxlim: 4   bits: 3/3
c ---[  12]---> Adder-cost: 46   maxlim: 26   bits: 5/5
c ---[  10]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[   8]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[   6]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[   4]---> Adder-cost: 30   maxlim: 16   bits: 5/5
c ---[   2]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[   0]---> Adder-cost: 14   maxlim: 9   bits: 4/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   48888   173713 |   16296       0        0     nan |  0.000 % |
c |       100 |   48687   173028 |   17925      83      318     3.8 | 10.811 % |
c |       250 |   48628   172833 |   19718     225      849     3.8 | 10.906 % |
c |       476 |   48056   170851 |   21689     370     1743     4.7 | 12.077 % |
c |       813 |   47741   169766 |   23858     663     3173     4.8 | 12.692 % |
c |      1319 |   47032   167398 |   26244    1079     5022     4.7 | 14.135 % |
c |      2080 |   46629   166033 |   28869    1787     9325     5.2 | 14.881 % |
c |      3219 |   46277   164867 |   31756    2877    17134     6.0 | 15.626 % |
c |      4927 |   45988   163874 |   34931    4540    38780     8.5 | 16.217 % |
c |      7489 |   45640   162684 |   38425    7025    77362    11.0 | 16.785 % |
c |     11333 |   45375   161791 |   42267   10820   181696    16.8 | 17.223 % |
c |     17102 |   45178   161132 |   46494   16548   401192    24.2 | 17.601 % |
c |     25752 |   45014   160574 |   51143   25175   816006    32.4 | 17.921 % |
c |     38727 |   44866   160076 |   56258   38108  1320215    34.6 | 18.181 % |
c |     58189 |   44748   159672 |   61884   57556  3155827    54.8 | 18.346 % |
c |     87381 |   44538   158956 |   68072   42619  3391725    79.6 | 18.737 % |
c |    131170 |   44474   158752 |   74879   29508  3852595   130.6 | 18.879 % |
c |    196856 |   44269   158066 |   82367   34861  2996358    86.0 | 19.245 % |
c |    295383 |   44215   157884 |   90604   65447  8739564   133.5 | 19.340 % |
c |    443174 |   44197   157824 |   99664   64386  8827616   137.1 | 19.375 % |
#### 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.90 2/55 15293
Raw data (stat): 15293 (runsolver) R 15292 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 424558448 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99959 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 1495 0 0 0 995 3 0 0 25 0 1 0 424558448 8241152 1469 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2012 1469 603 41 0 1971 0
vsize: 8048
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 2122 0 0 0 1993 5 0 0 25 0 1 0 424558448 10788864 2096 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2634 2096 603 41 0 2593 0
vsize: 10536
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 2713 0 0 0 2991 7 0 0 25 0 1 0 424558448 13320192 2687 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3252 2687 603 41 0 3211 0
vsize: 13008
[startup+40.0006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 3309 0 0 0 3989 10 0 0 25 0 1 0 424558448 15749120 3283 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3845 3283 603 41 0 3804 0
vsize: 15380
[startup+50.0013 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 3916 0 0 0 4988 11 0 0 25 0 1 0 424558448 18178048 3890 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4438 3890 603 41 0 4397 0
vsize: 17752
[startup+60.0014 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 4519 0 0 0 5986 14 0 0 25 0 1 0 424558448 20590592 4493 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5027 4493 603 41 0 4986 0
vsize: 20108
[startup+70.0016 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 4990 0 0 0 6984 16 0 0 25 0 1 0 424558448 22597632 4964 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5517 4964 603 41 0 5476 0
vsize: 22068
[startup+80.0023 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 5463 0 0 0 7982 17 0 0 25 0 1 0 424558448 24485888 5437 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5978 5437 603 41 0 5937 0
vsize: 23912
[startup+90.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 5463 0 0 0 8983 17 0 0 25 0 1 0 424558448 24485888 5437 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5978 5437 603 41 0 5937 0
vsize: 23912
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 5463 0 0 0 9983 17 0 0 25 0 1 0 424558448 24485888 5437 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5978 5437 603 41 0 5937 0
vsize: 23912
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 5463 0 0 0 10983 17 0 0 25 0 1 0 424558448 24485888 5437 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5978 5437 603 41 0 5937 0
vsize: 23912
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 5634 0 0 0 11982 18 0 0 25 0 1 0 424558448 25149440 5608 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6140 5608 603 41 0 6099 0
vsize: 24560
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 6174 0 0 0 12981 20 0 0 25 0 1 0 424558448 27295744 6148 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6664 6148 603 41 0 6623 0
vsize: 26656
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 6752 0 0 0 13979 21 0 0 25 0 1 0 424558448 29732864 6726 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7259 6726 603 41 0 7218 0
vsize: 29036
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 7423 0 0 0 14977 23 0 0 25 0 1 0 424558448 32681984 7397 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7979 7397 603 41 0 7938 0
vsize: 31916
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8012 0 0 0 15975 26 0 0 25 0 1 0 424558448 35094528 7986 4294967295 134512640 134672761 3221224544 3221223648 134554907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8568 7986 603 41 0 8527 0
vsize: 34272
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8453 0 0 0 16974 27 0 0 25 0 1 0 424558448 36966400 8427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9025 8427 603 41 0 8984 0
vsize: 36100
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8454 0 0 0 17974 27 0 0 25 0 1 0 424558448 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8454 0 0 0 18974 27 0 0 25 0 1 0 424558448 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8454 0 0 0 19974 27 0 0 25 0 1 0 424558448 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8454 0 0 0 20975 27 0 0 25 0 1 0 424558448 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8454 0 0 0 21975 27 0 0 25 0 1 0 424558448 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8454 0 0 0 22975 27 0 0 25 0 1 0 424558448 36966400 8428 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8454 0 0 0 23975 27 0 0 25 0 1 0 424558448 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8454 0 0 0 24975 27 0 0 25 0 1 0 424558448 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 8748 0 0 0 25975 28 0 0 25 0 1 0 424558448 38170624 8722 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9319 8722 603 41 0 9278 0
vsize: 37276
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9140 0 0 0 26973 29 0 0 25 0 1 0 424558448 39763968 9114 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9708 9114 603 41 0 9667 0
vsize: 38832
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 27973 30 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+290.005 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 28973 30 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+300.006 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 29973 30 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+310.006 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 30973 30 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+320.007 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 31974 30 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+330.007 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 32974 30 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+340.007 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 33974 31 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+350.008 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 34973 31 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+360.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 35974 31 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+370.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 36974 31 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+380.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9507 0 0 0 37974 31 0 0 25 0 1 0 424558448 41242624 9481 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+390.008 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 9769 0 0 0 38973 32 0 0 25 0 1 0 424558448 42315776 9743 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10331 9743 603 41 0 10290 0
vsize: 41324
[startup+400.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 10351 0 0 0 39971 34 0 0 25 0 1 0 424558448 44732416 10325 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10921 10325 603 41 0 10880 0
vsize: 43684
[startup+410.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 10933 0 0 0 40969 36 0 0 25 0 1 0 424558448 47136768 10907 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11508 10907 603 41 0 11467 0
vsize: 46032
[startup+420.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 11499 0 0 0 41968 38 0 0 25 0 1 0 424558448 49422336 11473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12066 11473 603 41 0 12025 0
vsize: 48264
[startup+430.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12007 0 0 0 42966 40 0 0 25 0 1 0 424558448 51421184 11981 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12554 11981 603 41 0 12513 0
vsize: 50216
[startup+440.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 43965 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+450.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 44965 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+460.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 45966 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+470.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 46966 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+480.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 47966 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+490.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 48966 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+500.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 49966 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+510.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 50966 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+520.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 51967 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+530.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 52967 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+540.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 53967 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+550.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 54967 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+560.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 55967 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+570.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12379 0 0 0 56967 41 0 0 25 0 1 0 424558448 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+580.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 12702 0 0 0 57966 42 0 0 25 0 1 0 424558448 54378496 12676 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13276 12676 603 41 0 13235 0
vsize: 53104
[startup+590.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 13106 0 0 0 58965 44 0 0 25 0 1 0 424558448 55992320 13080 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13670 13080 603 41 0 13629 0
vsize: 54680
[startup+600.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 13413 0 0 0 59964 45 0 0 25 0 1 0 424558448 57204736 13387 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13966 13387 603 41 0 13925 0
vsize: 55864
[startup+610.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 13783 0 0 0 60962 46 0 0 25 0 1 0 424558448 58671104 13757 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14324 13757 603 41 0 14283 0
vsize: 57296
[startup+620.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14139 0 0 0 61961 48 0 0 25 0 1 0 424558448 60137472 14113 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 14113 603 41 0 14641 0
vsize: 58728
[startup+630.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14472 0 0 0 62961 48 0 0 25 0 1 0 424558448 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+640.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14472 0 0 0 63961 48 0 0 25 0 1 0 424558448 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+650.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14472 0 0 0 64961 48 0 0 25 0 1 0 424558448 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+660.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14472 0 0 0 65961 48 0 0 25 0 1 0 424558448 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+670.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14472 0 0 0 66962 48 0 0 25 0 1 0 424558448 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+680.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14472 0 0 0 67962 48 0 0 25 0 1 0 424558448 61472768 14446 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+690.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14472 0 0 0 68962 48 0 0 25 0 1 0 424558448 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+700.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14472 0 0 0 69962 48 0 0 25 0 1 0 424558448 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+710.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14472 0 0 0 70962 48 0 0 25 0 1 0 424558448 61472768 14446 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+720.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14472 0 0 0 71962 48 0 0 25 0 1 0 424558448 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+730.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14473 0 0 0 72963 48 0 0 25 0 1 0 424558448 61472768 14447 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14447 603 41 0 14967 0
vsize: 60032
[startup+740.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 73963 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+750.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 74963 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+760.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 75963 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+770.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 76963 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+780.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 77963 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+790.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 78964 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+800.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 79964 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+810.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 80964 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+820.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 81964 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+830.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 82964 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223648 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+840.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 83964 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+850.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 84965 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+860.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 85965 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+870.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14474 0 0 0 86965 48 0 0 25 0 1 0 424558448 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+880.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 14762 0 0 0 87964 50 0 0 25 0 1 0 424558448 62668800 14736 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15300 14736 603 41 0 15259 0
vsize: 61200
[startup+890.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 15202 0 0 0 88963 51 0 0 25 0 1 0 424558448 64552960 15176 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15760 15176 603 41 0 15719 0
vsize: 63040
[startup+900.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 15430 0 0 0 89963 51 0 0 25 0 1 0 424558448 65552384 15404 4294967295 134512640 134672761 3221224544 3221223544 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16004 15404 603 41 0 15963 0
vsize: 64016
[startup+910.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 15620 0 0 0 90962 52 0 0 25 0 1 0 424558448 66396160 15594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16210 15594 603 41 0 16169 0
vsize: 64840
[startup+920.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 15848 0 0 0 91961 53 0 0 25 0 1 0 424558448 67350528 15822 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16443 15822 603 41 0 16402 0
vsize: 65772
[startup+930.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16115 0 0 0 92961 54 0 0 25 0 1 0 424558448 68464640 16089 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16715 16089 603 41 0 16674 0
vsize: 66860
[startup+940.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16361 0 0 0 93960 54 0 0 25 0 1 0 424558448 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+950.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16361 0 0 0 94961 54 0 0 25 0 1 0 424558448 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+960.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16361 0 0 0 95961 54 0 0 25 0 1 0 424558448 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+970.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16361 0 0 0 96961 54 0 0 25 0 1 0 424558448 69394432 16335 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+980.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16361 0 0 0 97961 54 0 0 25 0 1 0 424558448 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+990.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16361 0 0 0 98961 54 0 0 25 0 1 0 424558448 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16361 0 0 0 99961 54 0 0 25 0 1 0 424558448 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16361 0 0 0 100961 54 0 0 25 0 1 0 424558448 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16371 0 0 0 101962 54 0 0 25 0 1 0 424558448 69566464 16345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16345 603 41 0 16943 0
vsize: 67936
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16371 0 0 0 102962 54 0 0 25 0 1 0 424558448 69566464 16345 4294967295 134512640 134672761 3221224544 3221223648 134555105 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16345 603 41 0 16943 0
vsize: 67936
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16371 0 0 0 103962 54 0 0 25 0 1 0 424558448 69566464 16345 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16345 603 41 0 16943 0
vsize: 67936
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16371 0 0 0 104962 54 0 0 25 0 1 0 424558448 69566464 16345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16345 603 41 0 16943 0
vsize: 67936
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16372 0 0 0 105962 54 0 0 25 0 1 0 424558448 69566464 16346 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16346 603 41 0 16943 0
vsize: 67936
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16372 0 0 0 106962 54 0 0 25 0 1 0 424558448 69566464 16346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16346 603 41 0 16943 0
vsize: 67936
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16372 0 0 0 107963 54 0 0 25 0 1 0 424558448 69566464 16346 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16346 603 41 0 16943 0
vsize: 67936
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16372 0 0 0 108963 54 0 0 25 0 1 0 424558448 69566464 16346 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16346 603 41 0 16943 0
vsize: 67936
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16373 0 0 0 109964 54 0 0 25 0 1 0 424558448 69566464 16347 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16347 603 41 0 16943 0
vsize: 67936
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16374 0 0 0 110964 54 0 0 25 0 1 0 424558448 69566464 16348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16984 16348 603 41 0 16943 0
vsize: 67936
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16374 0 0 0 111964 54 0 0 25 0 1 0 424558448 69566464 16348 4294967295 134512640 134672761 3221224544 3221223728 134559379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16348 603 41 0 16943 0
vsize: 67936
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16374 0 0 0 112964 54 0 0 25 0 1 0 424558448 69566464 16348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16348 603 41 0 16943 0
vsize: 67936
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16374 0 0 0 113964 54 0 0 25 0 1 0 424558448 69566464 16348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16348 603 41 0 16943 0
vsize: 67936
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16374 0 0 0 114964 54 0 0 25 0 1 0 424558448 69566464 16348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16348 603 41 0 16943 0
vsize: 67936
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16374 0 0 0 115964 54 0 0 25 0 1 0 424558448 69566464 16348 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16348 603 41 0 16943 0
vsize: 67936
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16374 0 0 0 116965 54 0 0 25 0 1 0 424558448 69566464 16348 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16348 603 41 0 16943 0
vsize: 67936
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16374 0 0 0 117965 54 0 0 25 0 1 0 424558448 69566464 16348 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16348 603 41 0 16943 0
vsize: 67936
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16375 0 0 0 118965 54 0 0 25 0 1 0 424558448 69566464 16349 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16349 603 41 0 16943 0
vsize: 67936
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 15293
Raw data (stat): 15293 (minisat+) R 15292 30927 30926 0 -1 0 16378 0 0 0 119965 54 0 0 25 0 1 0 424558448 69566464 16352 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16984 16352 603 41 0 16943 0
vsize: 67936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 15293
Raw data (stat): 15293 (minisat+) Z 15292 30927 30926 0 -1 12 16380 0 0 0 119965 57 0 0 25 0 1 0 424558448 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.04
CPU time (s): 1200.24
CPU user time (s): 1199.66
CPU system time (s): 0.578911
CPU usage (%): 100.016
Max. virtual memory (Kb): 67936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####