Some explanations

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

General information on the benchmark

Namenormalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-opt1217.opb
MD5SUMdf52a42b636b50954671d81e4d85c221
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -16384
Optimality of the best value was proved NO
Number of terms in the objective function 19
Biggest coefficient in the objective function 262144
Number of bits for the biggest coefficient in the objective function 19
Sum of the numbers in the objective function 524287
Number of bits of the sum of numbers in the objective function 19
Biggest number in a constraint 393216
Number of bits of the biggest number in a constraint 19
Biggest sum of numbers in a constraint 917503
Number of bits of the biggest sum of numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.03
Number of variables787
Total number of constraints833
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)816
Number of constraints which are nor clauses,nor cardinality constraints17
Minimum length of a constraint1
Maximum length of a constraint67

Trace number 21639 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-22 00:33:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12880 boxname=wulflinc11 idbench=991 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  df52a42b636b50954671d81e4d85c221  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-opt1217.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-opt1217.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-opt1217.opb
IDLAUNCH: 12880
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        277384 kB
Buffers:         36044 kB
Cached:         699444 kB
SwapCached:          0 kB
Active:         361648 kB
Inactive:       376660 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        277132 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6820 kB
Slab:            13316 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:54:02 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 12880 7 1200.36 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 113 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 111]---> Adder-cost: 113   maxlim: 131070   bits: 18/17
c ---[ 110]---> Adder-cost: 115   maxlim: 131070   bits: 18/17
c ---[ 109]---> Adder-cost: 133   maxlim: 131070   bits: 18/17
c ---[ 108]---> Adder-cost: 148   maxlim: 131070   bits: 18/17
c ---[ 107]---> Adder-cost: 139   maxlim: 131070   bits: 18/17
c ---[ 106]---> Adder-cost: 142   maxlim: 131070   bits: 18/17
c ---[ 105]---> Adder-cost: 120   maxlim: 131070   bits: 18/17
c ---[ 104]---> Adder-cost: 124   maxlim: 131070   bits: 18/17
c ---[ 102]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 100]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  98]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  97]---> Adder-cost: 107   maxlim: 131070   bits: 18/17
c ---[  95]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  93]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  91]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  89]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  87]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  85]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  83]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  81]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  79]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  77]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  76]---> Adder-cost: 113   maxlim: 131070   bits: 18/17
c ---[  74]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  72]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  70]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  68]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  66]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  64]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  62]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  60]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  58]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  56]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  55]---> Adder-cost: 139   maxlim: 131070   bits: 18/17
c ---[  53]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  51]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  49]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  47]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  45]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  43]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  41]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  39]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  37]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  35]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  34]---> Adder-cost: 121   maxlim: 131070   bits: 18/17
c ---[  32]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  30]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  28]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  26]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  24]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  22]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  20]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  18]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  16]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  14]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[  13]---> Adder-cost: 100   maxlim: 131070   bits: 18/17
c ---[  11]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[   9]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[   7]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[   5]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[   3]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[   2]---> Adder-cost: 129   maxlim: 131070   bits: 18/17
c ---[   1]---> Adder-cost: 135   maxlim: 131070   bits: 18/17
c ---[   0]---> Adder-cost: 119   maxlim: 131070   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21930    78666 |    7310       0        0     nan |  0.000 % |
c |       100 |   21922    78640 |    8041      99      378     3.8 | 15.039 % |
c |       251 |   21898    78562 |    8845     247      943     3.8 | 15.103 % |
c |       477 |   21882    78510 |    9729     471     1874     4.0 | 15.146 % |
c |       814 |   21591    77567 |   10702     769     3646     4.7 | 16.379 % |
c |      1320 |   21331    76711 |   11772    1243     6936     5.6 | 17.443 % |
c |      2079 |   20316    73388 |   12950    1903    10241     5.4 | 21.676 % |
c |      3218 |   19565    70897 |   14245    2954    18468     6.3 | 24.761 % |
c |      4926 |   19473    70585 |   15669    4652    45556     9.8 | 25.144 % |
c |      7488 |   19473    70585 |   17236    7214   102840    14.3 | 25.144 % |
c |     11332 |   19466    70562 |   18960   11057   193357    17.5 | 25.165 % |
c |     17099 |   19457    70533 |   20856   16823   370586    22.0 | 25.207 % |
c |     25749 |   19457    70533 |   22941   14208   373294    26.3 | 25.207 % |
c |     38724 |   19424    70430 |   25236   15029   377639    25.1 | 25.356 % |
c |     58185 |   19177    69613 |   27759   20450   441326    21.6 | 26.314 % |
c |     87377 |   19153    69539 |   30535   19241   707176    36.8 | 26.420 % |
c |    131167 |   19153    69539 |   33589   27243   974251    35.8 | 26.420 % |
c |    196854 |   19153    69539 |   36948   32339   777889    24.1 | 26.420 % |
c |    295381 |   19153    69539 |   40642   18162   402100    22.1 | 26.420 % |
c |    443171 |   19153    69539 |   44707   37051   861249    23.2 | 26.420 % |
c |    664854 |   19153    69539 |   49178   24173   689435    28.5 | 26.420 % |
c |    997379 |   19095    69355 |   54095   26765   678308    25.3 | 26.633 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 14196
Raw data (stat): 14196 (runsolver) R 14195 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491210990 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.0002 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 1541 0 0 0 993 4 0 0 25 0 1 0 491210990 8105984 1518 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1979 1518 603 41 0 1938 0
vsize: 7916
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 1730 0 0 0 1993 5 0 0 25 0 1 0 491210990 8773632 1707 4294967295 134512640 134672761 3221224544 3221223728 134558700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2142 1707 603 41 0 2101 0
vsize: 8568
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 1796 0 0 0 2992 6 0 0 25 0 1 0 491210990 9191424 1773 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2244 1773 603 41 0 2203 0
vsize: 8976
[startup+40.0028 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 2023 0 0 0 3991 7 0 0 25 0 1 0 491210990 9998336 2000 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2441 2000 603 41 0 2400 0
vsize: 9764
[startup+50.0032 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 2359 0 0 0 4990 8 0 0 25 0 1 0 491210990 11489280 2336 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2805 2336 603 41 0 2764 0
vsize: 11220
[startup+60.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 2455 0 0 0 5990 9 0 0 25 0 1 0 491210990 11890688 2432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2903 2432 603 41 0 2862 0
vsize: 11612
[startup+70.0042 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 2797 0 0 0 6989 10 0 0 25 0 1 0 491210990 13242368 2774 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3233 2774 603 41 0 3192 0
vsize: 12932
[startup+80.0045 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 2814 0 0 0 7989 10 0 0 25 0 1 0 491210990 13381632 2791 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3267 2791 603 41 0 3226 0
vsize: 13068
[startup+90.0048 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 2984 0 0 0 8988 11 0 0 25 0 1 0 491210990 14049280 2961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3430 2961 603 41 0 3389 0
vsize: 13720
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 2996 0 0 0 9988 11 0 0 25 0 1 0 491210990 14049280 2973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3430 2973 603 41 0 3389 0
vsize: 13720
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3035 0 0 0 10987 12 0 0 25 0 1 0 491210990 14311424 3012 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3494 3012 603 41 0 3453 0
vsize: 13976
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3035 0 0 0 11987 12 0 0 25 0 1 0 491210990 14311424 3012 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3494 3012 603 41 0 3453 0
vsize: 13976
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3035 0 0 0 12987 12 0 0 25 0 1 0 491210990 14311424 3012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3494 3012 603 41 0 3453 0
vsize: 13976
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3045 0 0 0 13987 13 0 0 25 0 1 0 491210990 14479360 3022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3535 3022 603 41 0 3494 0
vsize: 14140
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3051 0 0 0 14986 13 0 0 25 0 1 0 491210990 14479360 3028 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3535 3028 603 41 0 3494 0
vsize: 14140
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3087 0 0 0 15986 13 0 0 25 0 1 0 491210990 14643200 3064 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3575 3064 603 41 0 3534 0
vsize: 14300
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3111 0 0 0 16986 14 0 0 25 0 1 0 491210990 14807040 3088 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3615 3088 603 41 0 3574 0
vsize: 14460
[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3117 0 0 0 17987 14 0 0 25 0 1 0 491210990 14807040 3094 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3615 3094 603 41 0 3574 0
vsize: 14460
[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3123 0 0 0 18986 14 0 0 25 0 1 0 491210990 14807040 3100 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3615 3100 603 41 0 3574 0
vsize: 14460
[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3132 0 0 0 19986 15 0 0 25 0 1 0 491210990 14807040 3109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3615 3109 603 41 0 3574 0
vsize: 14460
[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3137 0 0 0 20986 15 0 0 25 0 1 0 491210990 14807040 3114 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3615 3114 603 41 0 3574 0
vsize: 14460
[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3138 0 0 0 21986 15 0 0 25 0 1 0 491210990 14807040 3115 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3615 3115 603 41 0 3574 0
vsize: 14460
[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3139 0 0 0 22986 16 0 0 25 0 1 0 491210990 14807040 3116 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3615 3116 603 41 0 3574 0
vsize: 14460
[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3154 0 0 0 23986 16 0 0 25 0 1 0 491210990 15003648 3131 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3663 3131 603 41 0 3622 0
vsize: 14652
[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3155 0 0 0 24986 16 0 0 25 0 1 0 491210990 15003648 3132 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3663 3132 603 41 0 3622 0
vsize: 14652
[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3155 0 0 0 25985 16 0 0 25 0 1 0 491210990 15003648 3132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3663 3132 603 41 0 3622 0
vsize: 14652
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3155 0 0 0 26985 16 0 0 25 0 1 0 491210990 15003648 3132 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3663 3132 603 41 0 3622 0
vsize: 14652
[startup+280.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3155 0 0 0 27986 17 0 0 25 0 1 0 491210990 15003648 3132 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3663 3132 603 41 0 3622 0
vsize: 14652
[startup+290.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3155 0 0 0 28986 17 0 0 25 0 1 0 491210990 15003648 3132 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3663 3132 603 41 0 3622 0
vsize: 14652
[startup+300.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3163 0 0 0 29986 17 0 0 25 0 1 0 491210990 15003648 3140 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3663 3140 603 41 0 3622 0
vsize: 14652
[startup+310.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3172 0 0 0 30986 18 0 0 25 0 1 0 491210990 15003648 3149 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3663 3149 603 41 0 3622 0
vsize: 14652
[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3189 0 0 0 31986 18 0 0 25 0 1 0 491210990 15167488 3166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3703 3166 603 41 0 3662 0
vsize: 14812
[startup+330.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3190 0 0 0 32985 19 0 0 25 0 1 0 491210990 15167488 3167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3703 3167 603 41 0 3662 0
vsize: 14812
[startup+340.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3191 0 0 0 33985 19 0 0 25 0 1 0 491210990 15167488 3168 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3703 3168 603 41 0 3662 0
vsize: 14812
[startup+350.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3191 0 0 0 34985 19 0 0 25 0 1 0 491210990 15167488 3168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3703 3168 603 41 0 3662 0
vsize: 14812
[startup+360.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3204 0 0 0 35985 19 0 0 25 0 1 0 491210990 15167488 3181 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3703 3181 603 41 0 3662 0
vsize: 14812
[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3206 0 0 0 36985 19 0 0 25 0 1 0 491210990 15167488 3183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3703 3183 603 41 0 3662 0
vsize: 14812
[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3216 0 0 0 37985 20 0 0 25 0 1 0 491210990 15167488 3193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3703 3193 603 41 0 3662 0
vsize: 14812
[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3230 0 0 0 38985 20 0 0 25 0 1 0 491210990 15364096 3207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3207 603 41 0 3710 0
vsize: 15004
[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3231 0 0 0 39985 20 0 0 25 0 1 0 491210990 15364096 3208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3208 603 41 0 3710 0
vsize: 15004
[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3241 0 0 0 40984 21 0 0 25 0 1 0 491210990 15364096 3218 4294967295 134512640 134672761 3221224544 3221223680 134565134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3218 603 41 0 3710 0
vsize: 15004
[startup+420.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3242 0 0 0 41985 21 0 0 25 0 1 0 491210990 15364096 3219 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3219 603 41 0 3710 0
vsize: 15004
[startup+430.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3259 0 0 0 42985 21 0 0 25 0 1 0 491210990 15364096 3236 4294967295 134512640 134672761 3221224544 3221223456 134565743 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3236 603 41 0 3710 0
vsize: 15004
[startup+440.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3259 0 0 0 43985 22 0 0 25 0 1 0 491210990 15364096 3236 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3236 603 41 0 3710 0
vsize: 15004
[startup+450.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3259 0 0 0 44984 22 0 0 25 0 1 0 491210990 15364096 3236 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3236 603 41 0 3710 0
vsize: 15004
[startup+460.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3265 0 0 0 45984 23 0 0 25 0 1 0 491210990 15527936 3242 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3791 3242 603 41 0 3750 0
vsize: 15164
[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3275 0 0 0 46984 23 0 0 25 0 1 0 491210990 15527936 3252 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3791 3252 603 41 0 3750 0
vsize: 15164
[startup+480.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3295 0 0 0 47984 23 0 0 25 0 1 0 491210990 15527936 3272 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3791 3272 603 41 0 3750 0
vsize: 15164
[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3304 0 0 0 48983 24 0 0 25 0 1 0 491210990 15667200 3281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3825 3281 603 41 0 3784 0
vsize: 15300
[startup+500.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3478 0 0 0 49983 24 0 0 25 0 1 0 491210990 16334848 3455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3988 3455 603 41 0 3947 0
vsize: 15952
[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3585 0 0 0 50983 25 0 0 25 0 1 0 491210990 16883712 3562 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4122 3562 603 41 0 4081 0
vsize: 16488
[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3588 0 0 0 51982 25 0 0 25 0 1 0 491210990 16883712 3565 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4122 3565 603 41 0 4081 0
vsize: 16488
[startup+530.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3615 0 0 0 52982 25 0 0 25 0 1 0 491210990 17063936 3592 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4166 3592 603 41 0 4125 0
vsize: 16664
[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3632 0 0 0 53982 26 0 0 25 0 1 0 491210990 17063936 3609 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4166 3609 603 41 0 4125 0
vsize: 16664
[startup+550.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3652 0 0 0 54982 26 0 0 25 0 1 0 491210990 17203200 3629 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4200 3629 603 41 0 4159 0
vsize: 16800
[startup+560.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3656 0 0 0 55981 26 0 0 25 0 1 0 491210990 17203200 3633 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4200 3633 603 41 0 4159 0
vsize: 16800
[startup+570.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3674 0 0 0 56981 27 0 0 25 0 1 0 491210990 17367040 3651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4240 3651 603 41 0 4199 0
vsize: 16960
[startup+580.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3688 0 0 0 57981 27 0 0 25 0 1 0 491210990 17367040 3665 4294967295 134512640 134672761 3221224544 3221223136 134565745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4240 3665 603 41 0 4199 0
vsize: 16960
[startup+590.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3689 0 0 0 58981 27 0 0 25 0 1 0 491210990 17367040 3666 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4240 3666 603 41 0 4199 0
vsize: 16960
[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3698 0 0 0 59981 28 0 0 25 0 1 0 491210990 17367040 3675 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4240 3675 603 41 0 4199 0
vsize: 16960
[startup+610.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3700 0 0 0 60981 28 0 0 25 0 1 0 491210990 17367040 3677 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4240 3677 603 41 0 4199 0
vsize: 16960
[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3726 0 0 0 61981 28 0 0 25 0 1 0 491210990 17563648 3703 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4288 3703 603 41 0 4247 0
vsize: 17152
[startup+630.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3726 0 0 0 62981 29 0 0 25 0 1 0 491210990 17563648 3703 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4288 3703 603 41 0 4247 0
vsize: 17152
[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3726 0 0 0 63981 29 0 0 25 0 1 0 491210990 17563648 3703 4294967295 134512640 134672761 3221224544 3221223636 1074972064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4288 3703 603 41 0 4247 0
vsize: 17152
[startup+650.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3728 0 0 0 64981 29 0 0 25 0 1 0 491210990 17563648 3705 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4288 3705 603 41 0 4247 0
vsize: 17152
[startup+660.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3752 0 0 0 65981 29 0 0 25 0 1 0 491210990 17698816 3729 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4321 3729 603 41 0 4280 0
vsize: 17284
[startup+670.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3761 0 0 0 66981 29 0 0 25 0 1 0 491210990 17698816 3738 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4321 3738 603 41 0 4280 0
vsize: 17284
[startup+680.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3783 0 0 0 67980 30 0 0 25 0 1 0 491210990 17891328 3760 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4368 3760 603 41 0 4327 0
vsize: 17472
[startup+690.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3839 0 0 0 68980 30 0 0 25 0 1 0 491210990 18022400 3816 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4400 3816 603 41 0 4359 0
vsize: 17600
[startup+700.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3839 0 0 0 69979 31 0 0 25 0 1 0 491210990 18022400 3816 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4400 3816 603 41 0 4359 0
vsize: 17600
[startup+710.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3847 0 0 0 70979 31 0 0 25 0 1 0 491210990 18022400 3824 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4400 3824 603 41 0 4359 0
vsize: 17600
[startup+720.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3850 0 0 0 71979 31 0 0 25 0 1 0 491210990 18169856 3827 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4436 3827 603 41 0 4395 0
vsize: 17744
[startup+730.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3856 0 0 0 72979 32 0 0 25 0 1 0 491210990 18169856 3833 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4436 3833 603 41 0 4395 0
vsize: 17744
[startup+740.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3856 0 0 0 73979 32 0 0 25 0 1 0 491210990 18169856 3833 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4436 3833 603 41 0 4395 0
vsize: 17744
[startup+750.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3889 0 0 0 74978 33 0 0 25 0 1 0 491210990 18333696 3866 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4476 3866 603 41 0 4435 0
vsize: 17904
[startup+760.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3890 0 0 0 75978 33 0 0 25 0 1 0 491210990 18333696 3867 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4476 3867 603 41 0 4435 0
vsize: 17904
[startup+770.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3896 0 0 0 76978 33 0 0 25 0 1 0 491210990 18333696 3873 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4476 3873 603 41 0 4435 0
vsize: 17904
[startup+780.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3910 0 0 0 77978 33 0 0 25 0 1 0 491210990 18333696 3887 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4476 3887 603 41 0 4435 0
vsize: 17904
[startup+790.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3933 0 0 0 78978 34 0 0 25 0 1 0 491210990 18481152 3910 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4512 3910 603 41 0 4471 0
vsize: 18048
[startup+800.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3947 0 0 0 79978 34 0 0 25 0 1 0 491210990 18644992 3924 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4552 3924 603 41 0 4511 0
vsize: 18208
[startup+810.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 3961 0 0 0 80977 34 0 0 25 0 1 0 491210990 18644992 3938 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4552 3938 603 41 0 4511 0
vsize: 18208
[startup+820.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4083 0 0 0 81977 35 0 0 25 0 1 0 491210990 19177472 4060 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4682 4060 603 41 0 4641 0
vsize: 18728
[startup+830.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4254 0 0 0 82976 36 0 0 25 0 1 0 491210990 19853312 4231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4847 4231 603 41 0 4806 0
vsize: 19388
[startup+840.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4254 0 0 0 83976 36 0 0 25 0 1 0 491210990 19853312 4231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4847 4231 603 41 0 4806 0
vsize: 19388
[startup+850.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4272 0 0 0 84976 37 0 0 25 0 1 0 491210990 20013056 4249 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4886 4249 603 41 0 4845 0
vsize: 19544
[startup+860.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4297 0 0 0 85976 37 0 0 25 0 1 0 491210990 20013056 4274 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4886 4274 603 41 0 4845 0
vsize: 19544
[startup+870.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4298 0 0 0 86975 38 0 0 25 0 1 0 491210990 20013056 4275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4886 4275 603 41 0 4845 0
vsize: 19544
[startup+880.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4298 0 0 0 87976 38 0 0 25 0 1 0 491210990 20013056 4275 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4886 4275 603 41 0 4845 0
vsize: 19544
[startup+890.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4300 0 0 0 88976 38 0 0 25 0 1 0 491210990 20013056 4277 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4886 4277 603 41 0 4845 0
vsize: 19544
[startup+900.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4311 0 0 0 89975 38 0 0 25 0 1 0 491210990 20209664 4288 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4288 603 41 0 4893 0
vsize: 19736
[startup+910.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4313 0 0 0 90975 39 0 0 25 0 1 0 491210990 20209664 4290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4290 603 41 0 4893 0
vsize: 19736
[startup+920.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4313 0 0 0 91975 39 0 0 25 0 1 0 491210990 20209664 4290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4290 603 41 0 4893 0
vsize: 19736
[startup+930.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4313 0 0 0 92975 39 0 0 25 0 1 0 491210990 20209664 4290 4294967295 134512640 134672761 3221224544 3221223680 134565130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4290 603 41 0 4893 0
vsize: 19736
[startup+940.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4313 0 0 0 93975 40 0 0 25 0 1 0 491210990 20209664 4290 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4290 603 41 0 4893 0
vsize: 19736
[startup+950.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4325 0 0 0 94975 40 0 0 25 0 1 0 491210990 20209664 4302 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4302 603 41 0 4893 0
vsize: 19736
[startup+960.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4325 0 0 0 95975 40 0 0 25 0 1 0 491210990 20209664 4302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4302 603 41 0 4893 0
vsize: 19736
[startup+970.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4326 0 0 0 96975 40 0 0 25 0 1 0 491210990 20209664 4303 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4303 603 41 0 4893 0
vsize: 19736
[startup+980.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4336 0 0 0 97975 40 0 0 25 0 1 0 491210990 20209664 4313 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4313 603 41 0 4893 0
vsize: 19736
[startup+990.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4343 0 0 0 98975 41 0 0 25 0 1 0 491210990 20209664 4320 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4934 4320 603 41 0 4893 0
vsize: 19736
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4343 0 0 0 99975 41 0 0 25 0 1 0 491210990 20209664 4320 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4934 4320 603 41 0 4893 0
vsize: 19736
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4353 0 0 0 100975 41 0 0 25 0 1 0 491210990 20406272 4330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4982 4330 603 41 0 4941 0
vsize: 19928
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4353 0 0 0 101975 41 0 0 25 0 1 0 491210990 20406272 4330 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4982 4330 603 41 0 4941 0
vsize: 19928
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4353 0 0 0 102975 41 0 0 25 0 1 0 491210990 20406272 4330 4294967295 134512640 134672761 3221224544 3221223680 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4982 4330 603 41 0 4941 0
vsize: 19928
[startup+1040.05 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4353 0 0 0 103975 41 0 0 25 0 1 0 491210990 20406272 4330 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4982 4330 603 41 0 4941 0
vsize: 19928
[startup+1050.06 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4365 0 0 0 104977 41 0 0 25 0 1 0 491210990 20406272 4342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4982 4342 603 41 0 4941 0
vsize: 19928
[startup+1060.07 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4378 0 0 0 105977 41 0 0 25 0 1 0 491210990 20406272 4355 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4982 4355 603 41 0 4941 0
vsize: 19928
[startup+1070.07 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4386 0 0 0 106977 41 0 0 25 0 1 0 491210990 20602880 4363 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4363 603 41 0 4989 0
vsize: 20120
[startup+1080.07 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4387 0 0 0 107978 41 0 0 25 0 1 0 491210990 20602880 4364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4364 603 41 0 4989 0
vsize: 20120
[startup+1090.07 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4388 0 0 0 108978 41 0 0 25 0 1 0 491210990 20602880 4365 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4365 603 41 0 4989 0
vsize: 20120
[startup+1100.07 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4388 0 0 0 109978 41 0 0 25 0 1 0 491210990 20602880 4365 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4365 603 41 0 4989 0
vsize: 20120
[startup+1110.07 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4396 0 0 0 110978 41 0 0 25 0 1 0 491210990 20602880 4373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4373 603 41 0 4989 0
vsize: 20120
[startup+1120.08 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4396 0 0 0 111979 41 0 0 25 0 1 0 491210990 20602880 4373 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4373 603 41 0 4989 0
vsize: 20120
[startup+1130.08 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4396 0 0 0 112980 41 0 0 25 0 1 0 491210990 20602880 4373 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4373 603 41 0 4989 0
vsize: 20120
[startup+1140.09 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4396 0 0 0 113981 41 0 0 25 0 1 0 491210990 20602880 4373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4373 603 41 0 4989 0
vsize: 20120
[startup+1150.09 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4399 0 0 0 114981 41 0 0 25 0 1 0 491210990 20602880 4376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4376 603 41 0 4989 0
vsize: 20120
[startup+1160.09 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4399 0 0 0 115981 41 0 0 25 0 1 0 491210990 20602880 4376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5030 4376 603 41 0 4989 0
vsize: 20120
[startup+1170.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4417 0 0 0 116982 41 0 0 25 0 1 0 491210990 20799488 4394 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4394 603 41 0 5037 0
vsize: 20312
[startup+1180.11 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4419 0 0 0 117983 41 0 0 25 0 1 0 491210990 20799488 4396 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4396 603 41 0 5037 0
vsize: 20312
[startup+1190.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4420 0 0 0 118993 41 0 0 25 0 1 0 491210990 20799488 4397 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5078 4397 603 41 0 5037 0
vsize: 20312
[startup+1200.21 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14196
Raw data (stat): 14196 (minisat+) R 14195 32461 32460 0 -1 0 4430 0 0 0 119993 41 0 0 25 0 1 0 491210990 20799488 4407 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5078 4407 603 41 0 5037 0
vsize: 20312
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 14196
Raw data (stat): 14196 (minisat+) Z 14195 32461 32460 0 -1 12 4433 0 0 0 119993 42 0 0 24 0 1 0 491210990 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.24
CPU time (s): 1200.36
CPU user time (s): 1199.94
CPU system time (s): 0.424935
CPU usage (%): 100.01
Max. virtual memory (Kb): 20312
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####