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/miplib3/normalized-mps-v2-13-7-pp08a.opb
MD5SUM	d14265fdf4e5a3ef733af1f15b884cbe
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6661373
Optimality of the best value was proved	NO
Number of terms in the objective function	2304
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	178464600
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	178464600
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.02
Number of variables	3584
Total number of constraints	136
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	136
Minimum length of a constraint	21
Maximum length of a constraint	160
Trace number 17954

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 12:50:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18782 boxname=wulflinc2 idbench=1445 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d14265fdf4e5a3ef733af1f15b884cbe  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-pp08a.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-pp08a.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-pp08a.opb
IDLAUNCH: 18782
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        679048 kB
Buffers:         22448 kB
Cached:         311676 kB
SwapCached:        504 kB
Active:          58672 kB
Inactive:       277656 kB
HighTotal:      131008 kB
HighFree:         1036 kB
LowTotal:       903652 kB
LowFree:        678012 kB
SwapTotal:     2097136 kB
SwapFree:      2095900 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5712 kB
Slab:            13520 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:10:18 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 18782 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 200 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 199]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[ 198]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[ 197]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[ 196]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 195]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 194]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 193]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 192]---> Adder-cost: 218   maxlim: 312823   bits: 19/19
c ---[ 190]---> Adder-cost: 80   maxlim: 1114110   bits: 22/21
c ---[ 188]---> Adder-cost: 160   maxlim: 2153725   bits: 23/22
c ---[ 186]---> Adder-cost: 160   maxlim: 2156285   bits: 23/22
c ---[ 184]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 182]---> Adder-cost: 160   maxlim: 2160125   bits: 23/22
c ---[ 180]---> Adder-cost: 160   maxlim: 2152445   bits: 23/22
c ---[ 178]---> Adder-cost: 160   maxlim: 2162685   bits: 23/22
c ---[ 176]---> Adder-cost: 80   maxlim: 1101310   bits: 22/21
c ---[ 174]---> Adder-cost: 80   maxlim: 1078782   bits: 22/21
c ---[ 172]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 170]---> Adder-cost: 160   maxlim: 2123517   bits: 23/22
c ---[ 168]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 166]---> Adder-cost: 160   maxlim: 2126077   bits: 23/22
c ---[ 164]---> Adder-cost: 160   maxlim: 2129917   bits: 23/22
c ---[ 162]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 160]---> Adder-cost: 80   maxlim: 1074942   bits: 22/21
c ---[ 158]---> Adder-cost: 80   maxlim: 1108990   bits: 22/21
c ---[ 156]---> Adder-cost: 160   maxlim: 2156285   bits: 23/22
c ---[ 154]---> Adder-cost: 160   maxlim: 2162685   bits: 23/22
c ---[ 152]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 150]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 148]---> Adder-cost: 160   maxlim: 2152445   bits: 23/22
c ---[ 146]---> Adder-cost: 160   maxlim: 2151165   bits: 23/22
c ---[ 144]---> Adder-cost: 80   maxlim: 1093630   bits: 22/21
c ---[ 142]---> Adder-cost: 80   maxlim: 1114110   bits: 22/21
c ---[ 140]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 138]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 136]---> Adder-cost: 160   maxlim: 2143485   bits: 23/22
c ---[ 134]---> Adder-cost: 160   maxlim: 2142205   bits: 23/22
c ---[ 132]---> Adder-cost: 160   maxlim: 2151165   bits: 23/22
c ---[ 130]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 128]---> Adder-cost: 80   maxlim: 1101310   bits: 22/21
c ---[ 126]---> Adder-cost: 80   maxlim: 1074942   bits: 22/21
c ---[ 124]---> Adder-cost: 160   maxlim: 2129917   bits: 23/22
c ---[ 122]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 120]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 118]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 116]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 114]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 112]---> Adder-cost: 80   maxlim: 1080062   bits: 22/21
c ---[ 110]---> Adder-cost: 80   maxlim: 1105150   bits: 22/21
c ---[ 108]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 106]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 104]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 102]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 100]---> Adder-cost: 160   maxlim: 2160125   bits: 23/22
c ---[  98]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[  96]---> Adder-cost: 80   maxlim: 1107710   bits: 22/21
c ---[  94]---> Adder-cost: 80   maxlim: 1081342   bits: 22/21
c ---[  92]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[  90]---> Adder-cost: 160   maxlim: 2123517   bits: 23/22
c ---[  88]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[  86]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[  84]---> Adder-cost: 160   maxlim: 2122237   bits: 23/22
c ---[  82]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[  80]---> Adder-cost: 80   maxlim: 1076222   bits: 22/21
c ---[  78]---> Adder-cost: 80   maxlim: 1063678   bits: 22/21
c ---[  76]---> Adder-cost: 160   maxlim: 2110973   bits: 23/22
c ---[  74]---> Adder-cost: 160   maxlim: 2113533   bits: 23/22
c ---[  72]---> Adder-cost: 160   maxlim: 2113533   bits: 23/22
c ---[  70]---> Adder-cost: 160   maxlim: 2112253   bits: 23/22
c ---[  68]---> Adder-cost: 160   maxlim: 2112253   bits: 23/22
c ---[  66]---> Adder-cost: 160   maxlim: 2110973   bits: 23/22
c ---[  64]---> Adder-cost: 80   maxlim: 1061118   bits: 22/21
c ---[  63]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  62]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  61]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  60]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  59]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  58]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  57]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  56]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  55]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  54]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  53]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  52]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  51]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  50]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  49]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  48]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  47]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  46]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  45]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  44]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  43]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  42]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  41]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  40]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  39]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  38]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  37]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  36]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  35]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  34]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  33]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  32]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  31]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[  30]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[  29]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[  28]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[  27]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[  26]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[  25]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[  24]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[  23]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  22]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  21]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[  20]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  19]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  18]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  17]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  16]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[  15]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  14]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  13]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  12]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  11]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[  10]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[   9]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[   8]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[   7]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[   6]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[   5]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[   4]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[   3]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[   2]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[   1]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[   0]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   70648   254822 |   23549       0        0     nan |  0.000 % |
c |       100 |   70648   254822 |   25903     100      300     3.0 | 24.404 % |
c |       250 |   70640   254796 |   28494     249      701     2.8 | 24.410 % |
c |       476 |   70632   254770 |   31343     474     1650     3.5 | 24.416 % |
c |       817 |   70624   254744 |   34478     814     3317     4.1 | 24.422 % |
c |      1323 |   70594   254648 |   37925    1316     5299     4.0 | 24.445 % |
c |      2082 |   70534   254452 |   41718    2057     8891     4.3 | 24.491 % |
c |      3221 |   70464   254224 |   45890    3179    20013     6.3 | 24.548 % |
c |      4929 |   70443   254157 |   50479    4883    32740     6.7 | 24.566 % |
c |      7491 |   70357   253871 |   55527    7432    51849     7.0 | 24.640 % |
c |     11336 |   70274   253600 |   61080   11260    81645     7.3 | 24.709 % |
c |     17103 |   70023   252779 |   67188   16964   123809     7.3 | 24.922 % |
c |     25754 |   69916   252432 |   73906   25583   189820     7.4 | 25.014 % |
c |     38728 |   69677   251657 |   81297   38505   303515     7.9 | 25.227 % |
c |     58189 |   69467   250963 |   89427   57925   482806     8.3 | 25.406 % |
c |     87381 |   69258   250278 |   98370   87063  1050409    12.1 | 25.578 % |
c |    131171 |   69215   250137 |  108207   47671   704469    14.8 | 25.613 % |
c |    196855 |   69145   249909 |  119027   19817   411798    20.8 | 25.670 % |
c |    295381 |   69138   249886 |  130930  118342  2472535    20.9 | 25.676 % |
c |    443171 |   69109   249791 |  144023   38682   524629    13.6 | 25.699 % |
c |    664854 |   69064   249640 |  158425  139100  2431229    17.5 | 25.739 % |
c |    997379 |   69064   249640 |  174268   75161   778498    10.4 | 25.739 % |
#### 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.65 0.86 0.88 2/54 27904
Raw data (stat): 27904 (runsolver) R 27903 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486992644 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.71 0.86 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 2546 0 0 0 991 7 0 0 25 0 1 0 486992644 13164544 2466 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3214 2466 603 41 0 3173 0
vsize: 12856
[startup+20.0012 s]
Raw data (loadavg): 0.75 0.87 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 2786 0 0 0 1990 8 0 0 25 0 1 0 486992644 14110720 2706 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3445 2706 603 41 0 3404 0
vsize: 13780
[startup+30.0024 s]
Raw data (loadavg): 0.79 0.87 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 3058 0 0 0 2988 9 0 0 25 0 1 0 486992644 15319040 2978 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3740 2978 603 41 0 3699 0
vsize: 14960
[startup+40.0028 s]
Raw data (loadavg): 0.82 0.87 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 3267 0 0 0 3988 9 0 0 25 0 1 0 486992644 16130048 3187 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3938 3187 603 41 0 3897 0
vsize: 15752
[startup+50.0022 s]
Raw data (loadavg): 0.85 0.88 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 3914 0 0 0 4986 11 0 0 25 0 1 0 486992644 18944000 3834 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4625 3836 603 41 0 4584 0
vsize: 18500
[startup+60.0025 s]
Raw data (loadavg): 0.87 0.88 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 4220 0 0 0 5986 11 0 0 25 0 1 0 486992644 20160512 4140 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4922 4140 603 41 0 4881 0
vsize: 19688
[startup+70.0032 s]
Raw data (loadavg): 0.89 0.89 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 4664 0 0 0 6984 13 0 0 25 0 1 0 486992644 21909504 4584 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5349 4584 603 41 0 5308 0
vsize: 21396
[startup+80.0043 s]
Raw data (loadavg): 0.91 0.89 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 4664 0 0 0 7983 13 0 0 25 0 1 0 486992644 21909504 4584 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5349 4584 603 41 0 5308 0
vsize: 21396
[startup+90.0046 s]
Raw data (loadavg): 0.92 0.89 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 4681 0 0 0 8983 13 0 0 25 0 1 0 486992644 22065152 4601 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5387 4601 603 41 0 5346 0
vsize: 21548
[startup+100.004 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 4783 0 0 0 9983 13 0 0 25 0 1 0 486992644 22499328 4703 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5493 4703 603 41 0 5452 0
vsize: 21972
[startup+110.004 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 5023 0 0 0 10983 14 0 0 25 0 1 0 486992644 23625728 4943 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5768 4943 603 41 0 5727 0
vsize: 23072
[startup+120.004 s]
Raw data (loadavg): 0.95 0.90 0.90 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 5285 0 0 0 11982 15 0 0 25 0 1 0 486992644 24698880 5205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6030 5205 603 41 0 5989 0
vsize: 24120
[startup+130.005 s]
Raw data (loadavg): 0.96 0.90 0.90 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 5506 0 0 0 12982 16 0 0 25 0 1 0 486992644 25530368 5426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6233 5426 603 41 0 6192 0
vsize: 24932
[startup+140.005 s]
Raw data (loadavg): 0.96 0.91 0.90 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 5797 0 0 0 13981 17 0 0 25 0 1 0 486992644 26742784 5717 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6529 5717 603 41 0 6488 0
vsize: 26116
[startup+150.005 s]
Raw data (loadavg): 0.97 0.91 0.90 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 5866 0 0 0 14981 17 0 0 25 0 1 0 486992644 27013120 5786 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6595 5786 603 41 0 6554 0
vsize: 26380
[startup+160.005 s]
Raw data (loadavg): 0.97 0.91 0.90 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 5877 0 0 0 15981 17 0 0 25 0 1 0 486992644 27176960 5797 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6635 5797 603 41 0 6594 0
vsize: 26540
[startup+170.005 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 5919 0 0 0 16981 17 0 0 25 0 1 0 486992644 27340800 5839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6675 5839 603 41 0 6634 0
vsize: 26700
[startup+180.005 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 5972 0 0 0 17981 17 0 0 25 0 1 0 486992644 27504640 5892 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 5892 603 41 0 6674 0
vsize: 26860
[startup+190.005 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 5977 0 0 0 18981 17 0 0 25 0 1 0 486992644 27504640 5897 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 5897 603 41 0 6674 0
vsize: 26860
[startup+200.005 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 6055 0 0 0 19981 18 0 0 25 0 1 0 486992644 27836416 5975 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6796 5975 603 41 0 6755 0
vsize: 27184
[startup+210.005 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 6366 0 0 0 20981 18 0 0 25 0 1 0 486992644 29192192 6286 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7127 6286 603 41 0 7086 0
vsize: 28508
[startup+220.005 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 6575 0 0 0 21980 18 0 0 25 0 1 0 486992644 29995008 6495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7323 6495 603 41 0 7282 0
vsize: 29292
[startup+230.006 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7029 0 0 0 22980 19 0 0 25 0 1 0 486992644 32407552 6949 4294967295 134512640 134672761 3221224544 3221223712 134565029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7912 6949 603 41 0 7871 0
vsize: 31648
[startup+240.006 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7069 0 0 0 23980 19 0 0 25 0 1 0 486992644 32538624 6989 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7944 6989 603 41 0 7903 0
vsize: 31776
[startup+250.006 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7069 0 0 0 24980 19 0 0 25 0 1 0 486992644 32538624 6989 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7944 6989 603 41 0 7903 0
vsize: 31776
[startup+260.006 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7080 0 0 0 25980 19 0 0 25 0 1 0 486992644 32538624 7000 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7944 7000 603 41 0 7903 0
vsize: 31776
[startup+270.006 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7091 0 0 0 26980 19 0 0 25 0 1 0 486992644 32681984 7011 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7979 7011 603 41 0 7938 0
vsize: 31916
[startup+280.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7091 0 0 0 27981 19 0 0 25 0 1 0 486992644 32681984 7011 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7979 7011 603 41 0 7938 0
vsize: 31916
[startup+290.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7109 0 0 0 28981 19 0 0 25 0 1 0 486992644 32681984 7029 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7979 7029 603 41 0 7938 0
vsize: 31916
[startup+300.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7114 0 0 0 29981 19 0 0 25 0 1 0 486992644 32845824 7034 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8019 7034 603 41 0 7978 0
vsize: 32076
[startup+310.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7119 0 0 0 30981 19 0 0 25 0 1 0 486992644 32845824 7039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8019 7039 603 41 0 7978 0
vsize: 32076
[startup+320.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7336 0 0 0 31981 20 0 0 25 0 1 0 486992644 33656832 7256 4294967295 134512640 134672761 3221224544 3221223712 134564734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8217 7256 603 41 0 8176 0
vsize: 32868
[startup+330.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7371 0 0 0 32981 20 0 0 25 0 1 0 486992644 33792000 7291 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8250 7291 603 41 0 8209 0
vsize: 33000
[startup+340.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7371 0 0 0 33981 20 0 0 25 0 1 0 486992644 33792000 7291 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7291 603 41 0 8209 0
vsize: 33000
[startup+350.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7371 0 0 0 34981 20 0 0 25 0 1 0 486992644 33792000 7291 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8250 7291 603 41 0 8209 0
vsize: 33000
[startup+360.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7371 0 0 0 35981 20 0 0 25 0 1 0 486992644 33792000 7291 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8250 7291 603 41 0 8209 0
vsize: 33000
[startup+370.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7403 0 0 0 36981 20 0 0 25 0 1 0 486992644 33939456 7323 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8286 7323 603 41 0 8245 0
vsize: 33144
[startup+380.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7407 0 0 0 37981 20 0 0 25 0 1 0 486992644 34086912 7327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7327 603 41 0 8281 0
vsize: 33288
[startup+390.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7410 0 0 0 38981 20 0 0 25 0 1 0 486992644 34086912 7330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8322 7330 603 41 0 8281 0
vsize: 33288
[startup+400.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7459 0 0 0 39981 21 0 0 25 0 1 0 486992644 34217984 7379 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8354 7379 603 41 0 8313 0
vsize: 33416
[startup+410.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7594 0 0 0 40981 21 0 0 25 0 1 0 486992644 34758656 7514 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8486 7514 603 41 0 8445 0
vsize: 33944
[startup+420.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7594 0 0 0 41981 21 0 0 25 0 1 0 486992644 34758656 7514 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8486 7514 603 41 0 8445 0
vsize: 33944
[startup+430.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7594 0 0 0 42981 21 0 0 25 0 1 0 486992644 34758656 7514 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8486 7514 603 41 0 8445 0
vsize: 33944
[startup+440.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7594 0 0 0 43981 21 0 0 25 0 1 0 486992644 34758656 7514 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8486 7514 603 41 0 8445 0
vsize: 33944
[startup+450.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7621 0 0 0 44981 21 0 0 25 0 1 0 486992644 34906112 7541 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8522 7541 603 41 0 8481 0
vsize: 34088
[startup+460.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7656 0 0 0 45981 21 0 0 25 0 1 0 486992644 35053568 7576 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8558 7576 603 41 0 8517 0
vsize: 34232
[startup+470.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 7882 0 0 0 46981 22 0 0 25 0 1 0 486992644 35991552 7802 4294967295 134512640 134672761 3221224544 3221223696 134565048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8787 7802 603 41 0 8746 0
vsize: 35148
[startup+480.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8087 0 0 0 47980 23 0 0 25 0 1 0 486992644 36798464 8007 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8984 8007 603 41 0 8943 0
vsize: 35936
[startup+490.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8281 0 0 0 48979 24 0 0 25 0 1 0 486992644 37609472 8201 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9182 8201 603 41 0 9141 0
vsize: 36728
[startup+500.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8515 0 0 0 49979 24 0 0 25 0 1 0 486992644 38539264 8435 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9409 8435 603 41 0 9368 0
vsize: 37636
[startup+510.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8540 0 0 0 50979 24 0 0 25 0 1 0 486992644 38674432 8460 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8460 603 41 0 9401 0
vsize: 37768
[startup+520.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8540 0 0 0 51979 24 0 0 25 0 1 0 486992644 38674432 8460 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8460 603 41 0 9401 0
vsize: 37768
[startup+530.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8540 0 0 0 52979 24 0 0 25 0 1 0 486992644 38674432 8460 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8460 603 41 0 9401 0
vsize: 37768
[startup+540.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8540 0 0 0 53979 24 0 0 25 0 1 0 486992644 38674432 8460 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8460 603 41 0 9401 0
vsize: 37768
[startup+550.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8540 0 0 0 54979 24 0 0 25 0 1 0 486992644 38674432 8460 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8460 603 41 0 9401 0
vsize: 37768
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8540 0 0 0 55980 24 0 0 25 0 1 0 486992644 38674432 8460 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8460 603 41 0 9401 0
vsize: 37768
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8540 0 0 0 56980 24 0 0 25 0 1 0 486992644 38674432 8460 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8460 603 41 0 9401 0
vsize: 37768
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27904
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8540 0 0 0 57980 24 0 0 25 0 1 0 486992644 38674432 8460 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8460 603 41 0 9401 0
vsize: 37768
[startup+590.016 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 27927
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8540 0 0 0 58980 24 0 0 25 0 1 0 486992644 38674432 8460 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8460 603 41 0 9401 0
vsize: 37768
[startup+600.016 s]
Raw data (loadavg): 1.21 1.02 0.93 2/54 27957
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8540 0 0 0 59980 25 0 0 25 0 1 0 486992644 38674432 8460 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8460 603 41 0 9401 0
vsize: 37768
[startup+610.017 s]
Raw data (loadavg): 1.18 1.02 0.93 2/54 27957
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8542 0 0 0 60980 25 0 0 25 0 1 0 486992644 38674432 8462 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8462 603 41 0 9401 0
vsize: 37768
[startup+620.016 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 27957
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8542 0 0 0 61980 25 0 0 25 0 1 0 486992644 38674432 8462 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8462 603 41 0 9401 0
vsize: 37768
[startup+630.017 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 27957
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8542 0 0 0 62980 25 0 0 25 0 1 0 486992644 38674432 8462 4294967295 134512640 134672761 3221224544 3221223728 134559550 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8462 603 41 0 9401 0
vsize: 37768
[startup+640.018 s]
Raw data (loadavg): 1.11 1.01 0.93 2/54 27957
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8552 0 0 0 63980 25 0 0 25 0 1 0 486992644 38674432 8472 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8472 603 41 0 9401 0
vsize: 37768
[startup+650.018 s]
Raw data (loadavg): 1.09 1.01 0.93 2/54 27957
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8574 0 0 0 64981 25 0 0 25 0 1 0 486992644 38813696 8494 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9476 8494 603 41 0 9435 0
vsize: 37904
[startup+660.018 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8574 0 0 0 65981 25 0 0 25 0 1 0 486992644 38813696 8494 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9476 8494 603 41 0 9435 0
vsize: 37904
[startup+670.018 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8619 0 0 0 66981 25 0 0 25 0 1 0 486992644 38952960 8539 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9510 8539 603 41 0 9469 0
vsize: 38040
[startup+680.019 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8626 0 0 0 67981 25 0 0 25 0 1 0 486992644 38952960 8546 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9510 8546 603 41 0 9469 0
vsize: 38040
[startup+690.018 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8651 0 0 0 68981 25 0 0 25 0 1 0 486992644 39100416 8571 4294967295 134512640 134672761 3221224544 3221223668 134566106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9546 8571 603 41 0 9505 0
vsize: 38184
[startup+700.018 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8855 0 0 0 69981 26 0 0 25 0 1 0 486992644 39907328 8775 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9743 8775 603 41 0 9702 0
vsize: 38972
[startup+710.019 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8995 0 0 0 70981 26 0 0 25 0 1 0 486992644 40574976 8915 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8915 603 41 0 9865 0
vsize: 39624
[startup+720.018 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8995 0 0 0 71981 26 0 0 25 0 1 0 486992644 40574976 8915 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8915 603 41 0 9865 0
vsize: 39624
[startup+730.019 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8995 0 0 0 72981 26 0 0 25 0 1 0 486992644 40574976 8915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8915 603 41 0 9865 0
vsize: 39624
[startup+740.02 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8995 0 0 0 73981 26 0 0 25 0 1 0 486992644 40574976 8915 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9906 8915 603 41 0 9865 0
vsize: 39624
[startup+750.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8995 0 0 0 74980 26 0 0 25 0 1 0 486992644 40574976 8915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8915 603 41 0 9865 0
vsize: 39624
[startup+760.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8995 0 0 0 75980 26 0 0 25 0 1 0 486992644 40574976 8915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8915 603 41 0 9865 0
vsize: 39624
[startup+770.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8995 0 0 0 76980 26 0 0 25 0 1 0 486992644 40574976 8915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8915 603 41 0 9865 0
vsize: 39624
[startup+780.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8995 0 0 0 77981 26 0 0 25 0 1 0 486992644 40574976 8915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8915 603 41 0 9865 0
vsize: 39624
[startup+790.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 8995 0 0 0 78981 26 0 0 25 0 1 0 486992644 40574976 8915 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8915 603 41 0 9865 0
vsize: 39624
[startup+800.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9006 0 0 0 79981 27 0 0 25 0 1 0 486992644 40574976 8926 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8926 603 41 0 9865 0
vsize: 39624
[startup+810.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9064 0 0 0 80981 27 0 0 25 0 1 0 486992644 40869888 8984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9978 8984 603 41 0 9937 0
vsize: 39912
[startup+820.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9148 0 0 0 81981 27 0 0 25 0 1 0 486992644 41136128 9068 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10043 9068 603 41 0 10002 0
vsize: 40172
[startup+830.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9151 0 0 0 82981 27 0 0 25 0 1 0 486992644 41136128 9071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10043 9071 603 41 0 10002 0
vsize: 40172
[startup+840.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9201 0 0 0 83981 27 0 0 25 0 1 0 486992644 41328640 9121 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10090 9121 603 41 0 10049 0
vsize: 40360
[startup+850.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9203 0 0 0 84981 27 0 0 25 0 1 0 486992644 41328640 9123 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10090 9123 603 41 0 10049 0
vsize: 40360
[startup+860.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9203 0 0 0 85982 27 0 0 25 0 1 0 486992644 41328640 9123 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10090 9123 603 41 0 10049 0
vsize: 40360
[startup+870.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9217 0 0 0 86981 27 0 0 25 0 1 0 486992644 41525248 9137 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10138 9137 603 41 0 10097 0
vsize: 40552
[startup+880.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9248 0 0 0 87982 27 0 0 25 0 1 0 486992644 41680896 9168 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10176 9168 603 41 0 10135 0
vsize: 40704
[startup+890.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9270 0 0 0 88982 27 0 0 25 0 1 0 486992644 41680896 9190 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10176 9190 603 41 0 10135 0
vsize: 40704
[startup+900.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9279 0 0 0 89982 27 0 0 25 0 1 0 486992644 41836544 9199 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10214 9199 603 41 0 10173 0
vsize: 40856
[startup+910.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9379 0 0 0 90982 28 0 0 25 0 1 0 486992644 42237952 9299 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10312 9299 603 41 0 10271 0
vsize: 41248
[startup+920.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27959
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9528 0 0 0 91982 28 0 0 25 0 1 0 486992644 42795008 9448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10448 9448 603 41 0 10407 0
vsize: 41792
[startup+930.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9688 0 0 0 92981 29 0 0 25 0 1 0 486992644 43470848 9608 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10613 9608 603 41 0 10572 0
vsize: 42452
[startup+940.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 9836 0 0 0 93981 29 0 0 25 0 1 0 486992644 44011520 9756 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10745 9756 603 41 0 10704 0
vsize: 42980
[startup+950.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 10005 0 0 0 94981 29 0 0 25 0 1 0 486992644 44683264 9925 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10909 9925 603 41 0 10868 0
vsize: 43636
[startup+960.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 10190 0 0 0 95981 30 0 0 25 0 1 0 486992644 45518848 10110 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11113 10110 603 41 0 11072 0
vsize: 44452
[startup+970.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 10386 0 0 0 96981 30 0 0 25 0 1 0 486992644 46419968 10306 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10306 603 41 0 11292 0
vsize: 45332
[startup+980.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 10553 0 0 0 97981 30 0 0 25 0 1 0 486992644 47091712 10473 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11497 10473 603 41 0 11456 0
vsize: 45988
[startup+990.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 10747 0 0 0 98980 31 0 0 25 0 1 0 486992644 47792128 10667 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11668 10667 603 41 0 11627 0
vsize: 46672
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 10919 0 0 0 99980 31 0 0 25 0 1 0 486992644 48615424 10839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11869 10839 603 41 0 11828 0
vsize: 47476
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11085 0 0 0 100980 32 0 0 25 0 1 0 486992644 49287168 11005 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12033 11005 603 41 0 11992 0
vsize: 48132
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11251 0 0 0 101979 33 0 0 25 0 1 0 486992644 50040832 11171 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11171 603 41 0 12176 0
vsize: 48868
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11251 0 0 0 102980 33 0 0 25 0 1 0 486992644 50040832 11171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11171 603 41 0 12176 0
vsize: 48868
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11251 0 0 0 103980 33 0 0 25 0 1 0 486992644 50040832 11171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11171 603 41 0 12176 0
vsize: 48868
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11251 0 0 0 104980 33 0 0 25 0 1 0 486992644 50040832 11171 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11171 603 41 0 12176 0
vsize: 48868
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11251 0 0 0 105980 33 0 0 25 0 1 0 486992644 50040832 11171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11171 603 41 0 12176 0
vsize: 48868
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11251 0 0 0 106980 33 0 0 25 0 1 0 486992644 50040832 11171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11171 603 41 0 12176 0
vsize: 48868
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11251 0 0 0 107981 33 0 0 25 0 1 0 486992644 50040832 11171 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11171 603 41 0 12176 0
vsize: 48868
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11251 0 0 0 108981 33 0 0 25 0 1 0 486992644 50040832 11171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11171 603 41 0 12176 0
vsize: 48868
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11251 0 0 0 109981 33 0 0 25 0 1 0 486992644 50040832 11171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11171 603 41 0 12176 0
vsize: 48868
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11256 0 0 0 110981 33 0 0 25 0 1 0 486992644 50040832 11176 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11176 603 41 0 12176 0
vsize: 48868
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11256 0 0 0 111981 33 0 0 25 0 1 0 486992644 50040832 11176 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11176 603 41 0 12176 0
vsize: 48868
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11271 0 0 0 112982 33 0 0 25 0 1 0 486992644 50040832 11191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11191 603 41 0 12176 0
vsize: 48868
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11272 0 0 0 113982 33 0 0 25 0 1 0 486992644 50040832 11192 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11192 603 41 0 12176 0
vsize: 48868
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11273 0 0 0 114982 33 0 0 25 0 1 0 486992644 50040832 11193 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11193 603 41 0 12176 0
vsize: 48868
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11274 0 0 0 115982 33 0 0 25 0 1 0 486992644 50040832 11194 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12217 11194 603 41 0 12176 0
vsize: 48868
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11285 0 0 0 116982 33 0 0 25 0 1 0 486992644 50237440 11205 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12265 11205 603 41 0 12224 0
vsize: 49060
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11285 0 0 0 117983 33 0 0 25 0 1 0 486992644 50237440 11205 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12265 11205 603 41 0 12224 0
vsize: 49060
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11285 0 0 0 118983 33 0 0 25 0 1 0 486992644 50237440 11205 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12265 11205 603 41 0 12224 0
vsize: 49060
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27961
Raw data (stat): 27904 (minisat+) R 27903 20937 20936 0 -1 0 11285 0 0 0 119983 33 0 0 25 0 1 0 486992644 50237440 11205 4294967295 134512640 134672761 3221224544 3221223808 134562202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12265 11205 603 41 0 12224 0
vsize: 49060
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 27961
Raw data (stat): 27904 (minisat+) Z 27903 20937 20936 0 -1 12 11287 0 0 0 119983 35 0 0 25 0 1 0 486992644 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.06
CPU time (s): 1200.19
CPU user time (s): 1199.84
CPU system time (s): 0.350946
CPU usage (%): 100.011
Max. virtual memory (Kb): 49060
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####