PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.1944
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 22322

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-22 02:49:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11762 boxname=wulflinc10 idbench=905 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  098fe473d82d5f7d4121673eb775be76  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-cracpb1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-cracpb1.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-cracpb1.opb
IDLAUNCH: 11762
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        479092 kB
Buffers:         28292 kB
Cached:         505440 kB
SwapCached:          0 kB
Active:          48568 kB
Inactive:       487740 kB
HighTotal:      131008 kB
HighFree:        25536 kB
LowTotal:       903652 kB
LowFree:        453556 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13580 kB
Committed_AS:    63516 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 03:09:44 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 11762 7 1200.22 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.82 0.94 0.95 2/54 8833
Raw data (stat): 8833 (runsolver) R 8832 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 492036023 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0008 s]
Raw data (loadavg): 0.85 0.94 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 1496 0 0 0 993 4 0 0 25 0 1 0 492036023 8241152 1470 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2012 1470 603 41 0 1971 0
vsize: 8048
[startup+20.0007 s]
Raw data (loadavg): 0.87 0.94 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 2141 0 0 0 1991 6 0 0 25 0 1 0 492036023 10788864 2115 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2634 2115 603 41 0 2593 0
vsize: 10536
[startup+30.0008 s]
Raw data (loadavg): 0.89 0.94 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 2713 0 0 0 2989 8 0 0 25 0 1 0 492036023 13320192 2687 4294967295 134512640 134672761 3221224544 3221223708 134565156 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.0001 s]
Raw data (loadavg): 0.91 0.94 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 3346 0 0 0 3988 10 0 0 25 0 1 0 492036023 15884288 3320 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3878 3320 603 41 0 3837 0
vsize: 15512
[startup+50.0004 s]
Raw data (loadavg): 0.92 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 3965 0 0 0 4986 12 0 0 25 0 1 0 492036023 18313216 3939 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4471 3939 603 41 0 4430 0
vsize: 17884
[startup+60.0003 s]
Raw data (loadavg): 0.93 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 4576 0 0 0 5984 13 0 0 25 0 1 0 492036023 20856832 4550 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5092 4550 603 41 0 5051 0
vsize: 20368
[startup+70.0008 s]
Raw data (loadavg): 0.94 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 5042 0 0 0 6983 15 0 0 25 0 1 0 492036023 22732800 5016 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5550 5016 603 41 0 5509 0
vsize: 22200
[startup+80.0011 s]
Raw data (loadavg): 0.95 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 5463 0 0 0 7981 17 0 0 25 0 1 0 492036023 24485888 5437 4294967295 134512640 134672761 3221224544 3221223712 134561011 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.0009 s]
Raw data (loadavg): 0.96 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 5463 0 0 0 8981 17 0 0 25 0 1 0 492036023 24485888 5437 4294967295 134512640 134672761 3221224544 3221223712 134561198 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.002 s]
Raw data (loadavg): 0.96 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 5463 0 0 0 9982 17 0 0 25 0 1 0 492036023 24485888 5437 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.002 s]
Raw data (loadavg): 0.97 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 5463 0 0 0 10982 17 0 0 25 0 1 0 492036023 24485888 5437 4294967295 134512640 134672761 3221224544 3221223712 134561001 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.002 s]
Raw data (loadavg): 0.97 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 5790 0 0 0 11981 18 0 0 25 0 1 0 492036023 25825280 5764 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6305 5764 603 41 0 6264 0
vsize: 25220
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 6310 0 0 0 12979 20 0 0 25 0 1 0 492036023 27967488 6284 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6828 6284 603 41 0 6787 0
vsize: 27312
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 6905 0 0 0 13978 21 0 0 25 0 1 0 492036023 30396416 6879 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7421 6879 603 41 0 7380 0
vsize: 29684
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 7579 0 0 0 14976 23 0 0 25 0 1 0 492036023 33345536 7553 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8141 7553 603 41 0 8100 0
vsize: 32564
[startup+160.002 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8162 0 0 0 15975 25 0 0 25 0 1 0 492036023 35758080 8136 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8730 8137 603 41 0 8689 0
vsize: 34920
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8453 0 0 0 16975 25 0 0 25 0 1 0 492036023 36966400 8427 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9025 8427 603 41 0 8984 0
vsize: 36100
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8454 0 0 0 17975 25 0 0 25 0 1 0 492036023 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8454 0 0 0 18975 25 0 0 25 0 1 0 492036023 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8454 0 0 0 19975 25 0 0 25 0 1 0 492036023 36966400 8428 4294967295 134512640 134672761 3221224544 3221223728 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8454 0 0 0 20975 25 0 0 25 0 1 0 492036023 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8454 0 0 0 21976 25 0 0 25 0 1 0 492036023 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8454 0 0 0 22976 25 0 0 25 0 1 0 492036023 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8454 0 0 0 23976 25 0 0 25 0 1 0 492036023 36966400 8428 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9025 8428 603 41 0 8984 0
vsize: 36100
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8481 0 0 0 24976 26 0 0 25 0 1 0 492036023 37101568 8455 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9058 8455 603 41 0 9017 0
vsize: 36232
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 8887 0 0 0 25975 27 0 0 25 0 1 0 492036023 38703104 8861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9449 8861 603 41 0 9408 0
vsize: 37796
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9279 0 0 0 26974 28 0 0 25 0 1 0 492036023 40304640 9253 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9840 9253 603 41 0 9799 0
vsize: 39360
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 27973 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 28974 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 29974 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 30974 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 31973 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 32973 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 33974 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 34974 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223648 134560410 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): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 35974 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134560909 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): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 36974 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 9507 0 0 0 37974 29 0 0 25 0 1 0 492036023 41242624 9481 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10069 9481 603 41 0 10028 0
vsize: 40276
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 10059 0 0 0 38973 30 0 0 25 0 1 0 492036023 43524096 10033 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10626 10033 603 41 0 10585 0
vsize: 42504
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 10648 0 0 0 39972 32 0 0 25 0 1 0 492036023 45936640 10622 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11215 10622 603 41 0 11174 0
vsize: 44860
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 11212 0 0 0 40971 33 0 0 25 0 1 0 492036023 48205824 11186 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11769 11186 603 41 0 11728 0
vsize: 47076
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 11793 0 0 0 41970 34 0 0 25 0 1 0 492036023 50618368 11767 4294967295 134512640 134672761 3221224544 3221223648 134560316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12358 11767 603 41 0 12317 0
vsize: 49432
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12270 0 0 0 42969 36 0 0 25 0 1 0 492036023 52498432 12244 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12817 12244 603 41 0 12776 0
vsize: 51268
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 43969 36 0 0 25 0 1 0 492036023 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 44969 36 0 0 25 0 1 0 492036023 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 45969 36 0 0 25 0 1 0 492036023 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 46969 36 0 0 25 0 1 0 492036023 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+480.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 47970 36 0 0 25 0 1 0 492036023 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+490.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 48970 36 0 0 25 0 1 0 492036023 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 49970 36 0 0 25 0 1 0 492036023 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+510.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 50970 36 0 0 25 0 1 0 492036023 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+520.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 51970 36 0 0 25 0 1 0 492036023 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+530.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 52971 36 0 0 25 0 1 0 492036023 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+540.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 53971 36 0 0 25 0 1 0 492036023 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 54970 36 0 0 25 0 1 0 492036023 53039104 12353 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12353 603 41 0 12908 0
vsize: 51796
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12379 0 0 0 55970 36 0 0 25 0 1 0 492036023 53039104 12353 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12510 0 0 0 56970 36 0 0 25 0 1 0 492036023 53571584 12484 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13079 12484 603 41 0 13038 0
vsize: 52316
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 12990 0 0 0 57969 38 0 0 25 0 1 0 492036023 55455744 12964 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13539 12964 603 41 0 13498 0
vsize: 54156
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 13316 0 0 0 58969 38 0 0 25 0 1 0 492036023 56799232 13290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13867 13290 603 41 0 13826 0
vsize: 55468
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 13662 0 0 0 59968 39 0 0 25 0 1 0 492036023 58273792 13636 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14227 13636 603 41 0 14186 0
vsize: 56908
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14031 0 0 0 60968 39 0 0 25 0 1 0 492036023 59736064 14005 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14584 14005 603 41 0 14543 0
vsize: 58336
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 8833
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14452 0 0 0 61967 40 0 0 25 0 1 0 492036023 61472768 14426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14426 603 41 0 14967 0
vsize: 60032
[startup+630.009 s]
Raw data (loadavg): 1.07 0.99 0.95 2/54 8886
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14472 0 0 0 62967 40 0 0 25 0 1 0 492036023 61472768 14446 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+640.009 s]
Raw data (loadavg): 1.06 0.99 0.95 2/54 8886
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14472 0 0 0 63967 40 0 0 25 0 1 0 492036023 61472768 14446 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+650.01 s]
Raw data (loadavg): 1.05 0.99 0.95 2/54 8886
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14472 0 0 0 64967 41 0 0 25 0 1 0 492036023 61472768 14446 4294967295 134512640 134672761 3221224544 3221223648 134559946 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+660.009 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 8886
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14472 0 0 0 65967 41 0 0 25 0 1 0 492036023 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+670.01 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 8886
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14472 0 0 0 66967 41 0 0 25 0 1 0 492036023 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+680.01 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 8886
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14472 0 0 0 67967 41 0 0 25 0 1 0 492036023 61472768 14446 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+690.01 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 8886
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14472 0 0 0 68967 42 0 0 25 0 1 0 492036023 61472768 14446 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+700.01 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 8886
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14472 0 0 0 69966 42 0 0 25 0 1 0 492036023 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+710.01 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14472 0 0 0 70966 43 0 0 25 0 1 0 492036023 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+720.01 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14472 0 0 0 71966 43 0 0 25 0 1 0 492036023 61472768 14446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14446 603 41 0 14967 0
vsize: 60032
[startup+730.01 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 72966 44 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+740.01 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 73965 44 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+750.01 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 74965 45 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+760.01 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 75965 45 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+770.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 76965 45 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+780.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 77965 45 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+790.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 78965 46 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+800.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 79965 46 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+810.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 80965 46 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+820.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 81965 46 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+830.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 82965 47 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+840.009 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 83964 47 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+850.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 84964 48 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+860.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14474 0 0 0 85964 48 0 0 25 0 1 0 492036023 61472768 14448 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15008 14448 603 41 0 14967 0
vsize: 60032
[startup+870.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 14653 0 0 0 86963 49 0 0 25 0 1 0 492036023 62271488 14627 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15203 14627 603 41 0 15162 0
vsize: 60812
[startup+880.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 15160 0 0 0 87962 51 0 0 25 0 1 0 492036023 64417792 15134 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15727 15134 603 41 0 15686 0
vsize: 62908
[startup+890.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 15395 0 0 0 88961 51 0 0 25 0 1 0 492036023 65417216 15369 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15971 15369 603 41 0 15930 0
vsize: 63884
[startup+900.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 15596 0 0 0 89961 52 0 0 25 0 1 0 492036023 66265088 15570 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16178 15570 603 41 0 16137 0
vsize: 64712
[startup+910.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 15820 0 0 0 90960 53 0 0 25 0 1 0 492036023 67219456 15794 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16411 15794 603 41 0 16370 0
vsize: 65644
[startup+920.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16074 0 0 0 91959 54 0 0 25 0 1 0 492036023 68198400 16048 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16650 16048 603 41 0 16609 0
vsize: 66600
[startup+930.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16361 0 0 0 92958 56 0 0 25 0 1 0 492036023 69394432 16335 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+940.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16361 0 0 0 93958 56 0 0 25 0 1 0 492036023 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+950.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16361 0 0 0 94958 56 0 0 25 0 1 0 492036023 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 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.95 2/54 8888
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16361 0 0 0 95958 56 0 0 25 0 1 0 492036023 69394432 16335 4294967295 134512640 134672761 3221224544 3221223560 1075352732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16942 16335 603 41 0 16901 0
vsize: 67768
[startup+970.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16361 0 0 0 96957 57 0 0 25 0 1 0 492036023 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+980.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16361 0 0 0 97957 57 0 0 25 0 1 0 492036023 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134561205 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.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16361 0 0 0 98957 57 0 0 25 0 1 0 492036023 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16361 0 0 0 99957 57 0 0 25 0 1 0 492036023 69394432 16335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16370 0 0 0 100957 57 0 0 25 0 1 0 492036023 69566464 16344 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16984 16344 603 41 0 16943 0
vsize: 67936
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16371 0 0 0 101957 58 0 0 25 0 1 0 492036023 69566464 16345 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16371 0 0 0 102957 58 0 0 25 0 1 0 492036023 69566464 16345 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16371 0 0 0 103957 58 0 0 25 0 1 0 492036023 69566464 16345 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16372 0 0 0 104957 58 0 0 25 0 1 0 492036023 69566464 16346 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16984 16346 603 41 0 16943 0
vsize: 67936
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16372 0 0 0 105956 59 0 0 25 0 1 0 492036023 69566464 16346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16372 0 0 0 106956 59 0 0 25 0 1 0 492036023 69566464 16346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16372 0 0 0 107956 60 0 0 25 0 1 0 492036023 69566464 16346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16373 0 0 0 108956 60 0 0 25 0 1 0 492036023 69566464 16347 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16984 16347 603 41 0 16943 0
vsize: 67936
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16374 0 0 0 109955 61 0 0 25 0 1 0 492036023 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+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16374 0 0 0 110955 61 0 0 25 0 1 0 492036023 69566464 16348 4294967295 134512640 134672761 3221224544 3221223728 1074972064 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16374 0 0 0 111955 61 0 0 25 0 1 0 492036023 69566464 16348 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16374 0 0 0 112955 61 0 0 25 0 1 0 492036023 69566464 16348 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16374 0 0 0 113955 61 0 0 25 0 1 0 492036023 69566464 16348 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16374 0 0 0 114956 61 0 0 25 0 1 0 492036023 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+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16374 0 0 0 115956 62 0 0 25 0 1 0 492036023 69566464 16348 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16374 0 0 0 116956 62 0 0 25 0 1 0 492036023 69566464 16348 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 1 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.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16375 0 0 0 117956 62 0 0 25 0 1 0 492036023 69566464 16349 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16984 16349 603 41 0 16943 0
vsize: 67936
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16378 0 0 0 118955 62 0 0 25 0 1 0 492036023 69566464 16352 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16984 16352 603 41 0 16943 0
vsize: 67936
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 8890
Raw data (stat): 8833 (minisat+) R 8832 25347 25346 0 -1 0 16381 0 0 0 119955 62 0 0 25 0 1 0 492036023 69566464 16355 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16984 16355 603 41 0 16943 0
vsize: 67936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.95 1/54 8890
Raw data (stat): 8833 (minisat+) Z 8832 25347 25346 0 -1 12 16383 0 0 0 119955 65 0 0 25 0 1 0 492036023 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.22
CPU user time (s): 1199.56
CPU system time (s): 0.658899
CPU usage (%): 100.015
Max. virtual memory (Kb): 67936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####