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/submitted/manquinho/primes-dimacs-cnf/normalized-jnh210.opb
MD5SUM	536a635f83fc17dc00978c285b2ea8e6
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	88
Optimality of the best value was proved	NO
Number of terms in the objective function	200
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	200
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	200
Number of bits of the biggest sum of numbers	8
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.694894
Number of variables	200
Total number of constraints	900
Number of constraints which are clauses	900
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	10
Trace number 5129

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-13 22:12:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3569 boxname=wulflinc12 idbench=185 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  536a635f83fc17dc00978c285b2ea8e6  /oldhome/oroussel/tmp/wulflinc12/normalized-jnh210.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-jnh210.opb /oldhome/oroussel/tmp/wulflinc12/normalized-jnh210.opb
IDLAUNCH: 3569
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        919540 kB
Buffers:         34748 kB
Cached:          61252 kB
SwapCached:         16 kB
Active:          59360 kB
Inactive:        39492 kB
HighTotal:      131008 kB
HighFree:        65884 kB
LowTotal:       903652 kB
LowFree:        853656 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10700 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:23:19 (client local time) WITH STATUS 30 IN 627.699 SECONDS
stats: 3569 0 627.699 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 900 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     900     4115 |     300       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 93[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 394   maxlim: 107   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         6 |    3612    13785 |    1204       6       52     8.7 |  0.000 % |
c |       107 |    3612    13785 |    1324     107     3657    34.2 |  0.678 % |
c ==============================================================================
c [1mFound solution: 92[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 336   maxlim: 97   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       181 |    5588    20538 |    1862     178     4369    24.5 |  0.678 % |
c |       282 |    5439    19928 |    2048     249     5775    23.2 |  4.497 % |
c |       433 |    5421    19866 |    2253     398     9033    22.7 |  4.711 % |
c |       659 |    5405    19812 |    2478     622    13560    21.8 |  4.925 % |
c |       996 |    5405    19812 |    2726     959    23776    24.8 |  4.925 % |
c |      1504 |    5371    19674 |    2998    1466    35924    24.5 |  5.145 % |
c |      2263 |    5371    19674 |    3298    2225    54767    24.6 |  5.139 % |
c |      3403 |    5371    19674 |    3628    3365    83089    24.7 |  5.139 % |
c |      5111 |    5318    19458 |    3991    3092    79625    25.8 |  5.461 % |
c |      7673 |    5318    19458 |    4390    3469    86556    25.0 |  5.461 % |
c ==============================================================================
c [1mFound solution: 91[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 284   maxlim: 93   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7693 |    7265    26395 |    2421    3489    87222    25.0 |  5.461 % |
c |      7793 |    7265    26395 |    2663    1845    37465    20.3 |  4.583 % |
c |      7946 |    7265    26395 |    2929    1998    41373    20.7 |  4.583 % |
c |      8171 |    7265    26395 |    3222    2223    45427    20.4 |  4.583 % |
c |      8510 |    7265    26395 |    3544    2562    55641    21.7 |  4.583 % |
c |      9017 |    7265    26395 |    3899    3069    72429    23.6 |  4.583 % |
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 94   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9588 |    7270    26416 |    2423    3640    92536    25.4 |  4.583 % |
c |      9689 |    6943    25113 |    2665    1907    41420    21.7 |  6.373 % |
c |      9840 |    6943    25113 |    2931    2058    43400    21.1 |  6.373 % |
c |     10066 |    6943    25113 |    3225    2284    47781    20.9 |  6.373 % |
c |     10404 |    6943    25113 |    3547    2622    54750    20.9 |  6.373 % |
c |     10911 |    6943    25113 |    3902    3129    64095    20.5 |  6.373 % |
c |     11671 |    6943    25113 |    4292    3889    82439    21.2 |  6.375 % |
c |     12810 |    6943    25113 |    4721    2709    47673    17.6 |  6.375 % |
c |     14520 |    6943    25113 |    5193    4419    85841    19.4 |  6.373 % |
c |     17082 |    6943    25113 |    5713    4190    75677    18.1 |  6.373 % |
c |     20928 |    6943    25113 |    6284    5005   113817    22.7 |  6.373 % |
c |     26696 |    6943    25113 |    6913    4173    75262    18.0 |  6.375 % |
c |     35346 |    6943    25113 |    7604    5587   111183    19.9 |  6.375 % |
c |     48320 |    6943    25113 |    8364    6612   144651    21.9 |  6.373 % |
c |     67781 |    6943    25113 |    9201    8724   157517    18.1 |  6.375 % |
c ==============================================================================
c [1mFound solution: 89[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 186   maxlim: 89   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72956 |    8208    29618 |    2736    9134   170094    18.6 |  6.375 % |
c |     73056 |    8208    29618 |    3009    2384    31325    13.1 |  5.803 % |
c |     73207 |    8208    29618 |    3310    2535    35540    14.0 |  5.803 % |
c |     73432 |    8208    29618 |    3641    2760    42220    15.3 |  5.803 % |
c |     73769 |    8208    29618 |    4005    3097    49406    16.0 |  5.803 % |
c |     74276 |    8208    29618 |    4406    3604    62089    17.2 |  5.803 % |
c |     75037 |    8208    29618 |    4846    4365    77578    17.8 |  5.803 % |
c |     76177 |    8208    29618 |    5331    2925    46893    16.0 |  5.803 % |
c |     77886 |    8208    29618 |    5864    4634    83994    18.1 |  5.805 % |
c |     80448 |    8208    29618 |    6451    4010    76379    19.0 |  5.803 % |
c ==============================================================================
c [1mFound solution: 88[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 90   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83963 |    8213    29639 |    2737    4017    72812    18.1 |  5.803 % |
c |     84063 |    8213    29639 |    3010    2109    30790    14.6 |  5.866 % |
c |     84213 |    8213    29639 |    3311    2259    33263    14.7 |  5.866 % |
c |     84438 |    8213    29639 |    3642    2484    37173    15.0 |  5.866 % |
c |     84776 |    8213    29639 |    4007    2822    49142    17.4 |  5.866 % |
c |     85282 |    8161    29445 |    4407    3325    59926    18.0 |  6.078 % |
c |     86041 |    8161    29445 |    4848    4084    77652    19.0 |  6.079 % |
c |     87180 |    8161    29445 |    5333    5223   103044    19.7 |  6.078 % |
c |     88889 |    8161    29445 |    5867    4084    70607    17.3 |  6.078 % |
c |     91455 |    8161    29445 |    6453    3570    60021    16.8 |  6.079 % |
c |     95299 |    8161    29445 |    7099    4013    74140    18.5 |  6.078 % |
c |    101066 |    8161    29445 |    7808    6024   139025    23.1 |  6.078 % |
c |    109716 |    8161    29445 |    8589    6496   134173    20.7 |  6.078 % |
c |    122692 |    8161    29445 |    9448    6032   123379    20.5 |  6.078 % |
c |    142153 |    8161    29445 |   10393    5955   136678    23.0 |  6.078 % |
c |    171345 |    8161    29445 |   11433    8454   178630    21.1 |  6.078 % |
c |    215134 |    8161    29445 |   12576   11268   230658    20.5 |  6.078 % |
c |    280818 |    8161    29445 |   13834   12268   252659    20.6 |  6.080 % |
c |    379345 |    8161    29445 |   15217   11369   244234    21.5 |  6.080 % |
c |    527135 |    8161    29445 |   16739   11450   240196    21.0 |  6.080 % |
c ==============================================================================
c [1mOptimal solution: 88[0m
s OPTIMUM FOUND
v -x1 x2 -x3 x4 -x5 x6 -x7 x8 x9 -x10 -x11 -x12 -x13 x14 x15 -x16 -x17 x18 -x19 -x20 -x21 x22 -x23 -x24 -x25 x26 -x27 -x28 x29 -x30 -x31 -x32 x33 -x34 x35 -x36 -x37 x38 -x39 x40 -x41 x42 -x43 x44 -x45 x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 -x55 -x56 -x57 x58 x59 -x60 -x61 x62 x63 -x64 x65 -x66 -x67 x68 x69 -x70 x71 -x72 -x73 x74 -x75 x76 x77 -x78 -x79 x80 x81 -x82 x83 -x84 x85 -x86 -x87 x88 x89 -x90 -x91 x92 -x93 x94 x95 -x96 -x97 x98 x99 -x100 -x101 x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 -x117 x118 -x119 x120 x121 -x122 -x123 x124 x125 -x126 x127 -x128 -x129 x130 -x131 -x132 x133 -x134 -x135 x136 -x137 x138 -x139 x140 x141 -x142 x143 -x144 -x145 x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 -x155 x156 -x157 -x158 x159 -x160 x161 -x162 -x163 x164 x165 -x166 x167 -x168 -x169 x170 x171 -x172 -x173 x174 x175 -x176 x177 -x178 -x179 -x180 -x181 -x182 -x183 x184 x185 -x186 -x187 -x188 x189 -x190 x191 -x192 x193 -x194 -x195 x196 x197 -x198 -x199 -x200
c _______________________________________________________________________________
c 
c restarts              : 64
c conflicts             : 735220         (1172 /sec)
c decisions             : 891088         (1420 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 627.514 s
c _______________________________________________________________________________
#### 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.61 0.89 0.88 2/54 28764
Raw data (stat): 28764 (runsolver) R 28763 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421234293 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0005 s]
Raw data (loadavg): 0.67 0.89 0.89 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 673 0 0 0 996 2 0 0 25 0 1 0 421234293 4288512 651 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1047 651 603 41 0 1006 0
vsize: 4188
[startup+20.0015 s]
Raw data (loadavg): 0.72 0.90 0.89 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 762 0 0 0 1995 3 0 0 25 0 1 0 421234293 4685824 740 4294967295 134512640 134672761 3221224576 3221223760 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1144 740 603 41 0 1103 0
vsize: 4576
[startup+30.0017 s]
Raw data (loadavg): 0.76 0.90 0.89 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 813 0 0 0 2994 4 0 0 25 0 1 0 421234293 4956160 791 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1210 791 603 41 0 1169 0
vsize: 4840
[startup+40.002 s]
Raw data (loadavg): 0.80 0.90 0.89 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 823 0 0 0 3994 4 0 0 25 0 1 0 421234293 4956160 801 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1210 801 603 41 0 1169 0
vsize: 4840
[startup+50.0039 s]
Raw data (loadavg): 0.83 0.91 0.89 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 846 0 0 0 4993 4 0 0 25 0 1 0 421234293 5124096 824 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1251 824 603 41 0 1210 0
vsize: 5004
[startup+60.0042 s]
Raw data (loadavg): 0.86 0.91 0.89 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 854 0 0 0 5993 4 0 0 25 0 1 0 421234293 5124096 832 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1251 832 603 41 0 1210 0
vsize: 5004
[startup+70.0045 s]
Raw data (loadavg): 0.88 0.91 0.89 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 895 0 0 0 6993 5 0 0 25 0 1 0 421234293 5263360 873 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1285 873 603 41 0 1244 0
vsize: 5140
[startup+80.0054 s]
Raw data (loadavg): 0.90 0.91 0.89 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 933 0 0 0 7992 6 0 0 25 0 1 0 421234293 5394432 911 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1317 911 603 41 0 1276 0
vsize: 5268
[startup+90.0048 s]
Raw data (loadavg): 0.91 0.92 0.89 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 951 0 0 0 8991 6 0 0 25 0 1 0 421234293 5529600 929 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1350 929 603 41 0 1309 0
vsize: 5400
[startup+100.006 s]
Raw data (loadavg): 0.92 0.92 0.89 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1011 0 0 0 9991 7 0 0 25 0 1 0 421234293 5808128 989 4294967295 134512640 134672761 3221224576 3221223672 1075347118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1418 989 603 41 0 1377 0
vsize: 5672
[startup+110.007 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1018 0 0 0 10990 7 0 0 25 0 1 0 421234293 5808128 996 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1418 996 603 41 0 1377 0
vsize: 5672
[startup+120.007 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1052 0 0 0 11990 7 0 0 25 0 1 0 421234293 5939200 1030 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1450 1030 603 41 0 1409 0
vsize: 5800
[startup+130.008 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1068 0 0 0 12990 8 0 0 25 0 1 0 421234293 5939200 1046 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1450 1046 603 41 0 1409 0
vsize: 5800
[startup+140.008 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1079 0 0 0 13989 8 0 0 25 0 1 0 421234293 6086656 1057 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1486 1057 603 41 0 1445 0
vsize: 5944
[startup+150.01 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1080 0 0 0 14989 8 0 0 25 0 1 0 421234293 6086656 1058 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1486 1058 603 41 0 1445 0
vsize: 5944
[startup+160.01 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1081 0 0 0 15989 8 0 0 25 0 1 0 421234293 6086656 1059 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1486 1059 603 41 0 1445 0
vsize: 5944
[startup+170.011 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1089 0 0 0 16988 9 0 0 25 0 1 0 421234293 6086656 1067 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1486 1067 603 41 0 1445 0
vsize: 5944
[startup+180.011 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1110 0 0 0 17988 9 0 0 25 0 1 0 421234293 6086656 1088 4294967295 134512640 134672761 3221224576 3221223760 134559173 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1486 1088 603 41 0 1445 0
vsize: 5944
[startup+190.013 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1121 0 0 0 18988 9 0 0 25 0 1 0 421234293 6221824 1099 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1519 1099 603 41 0 1478 0
vsize: 6076
[startup+200.014 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1121 0 0 0 19987 10 0 0 25 0 1 0 421234293 6221824 1099 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1519 1099 603 41 0 1478 0
vsize: 6076
[startup+210.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1139 0 0 0 20987 10 0 0 25 0 1 0 421234293 6221824 1117 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1519 1117 603 41 0 1478 0
vsize: 6076
[startup+220.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1234 0 0 0 21986 11 0 0 25 0 1 0 421234293 6627328 1212 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1618 1212 603 41 0 1577 0
vsize: 6472
[startup+230.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1240 0 0 0 22986 11 0 0 25 0 1 0 421234293 6627328 1218 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1618 1218 603 41 0 1577 0
vsize: 6472
[startup+240.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1243 0 0 0 23985 11 0 0 25 0 1 0 421234293 6774784 1221 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1654 1221 603 41 0 1613 0
vsize: 6616
[startup+250.016 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1247 0 0 0 24985 12 0 0 25 0 1 0 421234293 6774784 1225 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1654 1225 603 41 0 1613 0
vsize: 6616
[startup+260.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1251 0 0 0 25984 12 0 0 25 0 1 0 421234293 6774784 1229 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1654 1229 603 41 0 1613 0
vsize: 6616
[startup+270.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1254 0 0 0 26984 12 0 0 25 0 1 0 421234293 6774784 1232 4294967295 134512640 134672761 3221224576 3221223744 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1654 1232 603 41 0 1613 0
vsize: 6616
[startup+280.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1261 0 0 0 27984 12 0 0 25 0 1 0 421234293 6774784 1239 4294967295 134512640 134672761 3221224576 3221223392 134565745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1654 1239 603 41 0 1613 0
vsize: 6616
[startup+290.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1266 0 0 0 28983 13 0 0 25 0 1 0 421234293 6774784 1244 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1654 1244 603 41 0 1613 0
vsize: 6616
[startup+300.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1290 0 0 0 29983 13 0 0 25 0 1 0 421234293 6905856 1268 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1686 1268 603 41 0 1645 0
vsize: 6744
[startup+310.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1299 0 0 0 30982 13 0 0 25 0 1 0 421234293 6905856 1277 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1686 1277 603 41 0 1645 0
vsize: 6744
[startup+320.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1303 0 0 0 31982 14 0 0 25 0 1 0 421234293 6905856 1281 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1686 1281 603 41 0 1645 0
vsize: 6744
[startup+330.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1311 0 0 0 32981 14 0 0 25 0 1 0 421234293 7065600 1289 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1725 1289 603 41 0 1684 0
vsize: 6900
[startup+340.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1312 0 0 0 33981 15 0 0 25 0 1 0 421234293 7065600 1290 4294967295 134512640 134672761 3221224576 3221223680 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1725 1290 603 41 0 1684 0
vsize: 6900
[startup+350.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1312 0 0 0 34981 15 0 0 25 0 1 0 421234293 7065600 1290 4294967295 134512640 134672761 3221224576 3221223532 1075349878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1725 1290 603 41 0 1684 0
vsize: 6900
[startup+360.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1316 0 0 0 35980 15 0 0 25 0 1 0 421234293 7065600 1294 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1725 1294 603 41 0 1684 0
vsize: 6900
[startup+370.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1322 0 0 0 36980 15 0 0 25 0 1 0 421234293 7065600 1300 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1725 1300 603 41 0 1684 0
vsize: 6900
[startup+380.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1325 0 0 0 37980 16 0 0 25 0 1 0 421234293 7065600 1303 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1725 1303 603 41 0 1684 0
vsize: 6900
[startup+390.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1327 0 0 0 38980 16 0 0 25 0 1 0 421234293 7065600 1305 4294967295 134512640 134672761 3221224576 3221223680 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1725 1305 603 41 0 1684 0
vsize: 6900
[startup+400.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1327 0 0 0 39980 16 0 0 25 0 1 0 421234293 7065600 1305 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1725 1305 603 41 0 1684 0
vsize: 6900
[startup+410.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1338 0 0 0 40979 16 0 0 25 0 1 0 421234293 7065600 1316 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1725 1316 603 41 0 1684 0
vsize: 6900
[startup+420.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1344 0 0 0 41979 17 0 0 25 0 1 0 421234293 7213056 1322 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1761 1322 603 41 0 1720 0
vsize: 7044
[startup+430.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1369 0 0 0 42978 17 0 0 25 0 1 0 421234293 7376896 1347 4294967295 134512640 134672761 3221224576 3221223680 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1801 1347 603 41 0 1760 0
vsize: 7204
[startup+440.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1380 0 0 0 43978 17 0 0 25 0 1 0 421234293 7376896 1358 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1801 1358 603 41 0 1760 0
vsize: 7204
[startup+450.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1393 0 0 0 44978 17 0 0 25 0 1 0 421234293 7376896 1371 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1801 1371 603 41 0 1760 0
vsize: 7204
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1400 0 0 0 45978 17 0 0 25 0 1 0 421234293 7512064 1378 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1378 603 41 0 1793 0
vsize: 7336
[startup+470.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1410 0 0 0 46978 17 0 0 25 0 1 0 421234293 7512064 1388 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1388 603 41 0 1793 0
vsize: 7336
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1410 0 0 0 47978 17 0 0 25 0 1 0 421234293 7512064 1388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1388 603 41 0 1793 0
vsize: 7336
[startup+490.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1411 0 0 0 48979 17 0 0 25 0 1 0 421234293 7512064 1389 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1389 603 41 0 1793 0
vsize: 7336
[startup+500.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1411 0 0 0 49979 17 0 0 25 0 1 0 421234293 7512064 1389 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1389 603 41 0 1793 0
vsize: 7336
[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1417 0 0 0 50979 17 0 0 25 0 1 0 421234293 7512064 1395 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1395 603 41 0 1793 0
vsize: 7336
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1420 0 0 0 51979 17 0 0 25 0 1 0 421234293 7512064 1398 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1398 603 41 0 1793 0
vsize: 7336
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1434 0 0 0 52979 17 0 0 25 0 1 0 421234293 7675904 1412 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1874 1412 603 41 0 1833 0
vsize: 7496
[startup+540.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1434 0 0 0 53979 17 0 0 25 0 1 0 421234293 7675904 1412 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1874 1412 603 41 0 1833 0
vsize: 7496
[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1441 0 0 0 54980 17 0 0 25 0 1 0 421234293 7675904 1419 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1874 1419 603 41 0 1833 0
vsize: 7496
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1441 0 0 0 55980 17 0 0 25 0 1 0 421234293 7675904 1419 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1874 1419 603 41 0 1833 0
vsize: 7496
[startup+570.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1448 0 0 0 56980 17 0 0 25 0 1 0 421234293 7675904 1426 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1874 1426 603 41 0 1833 0
vsize: 7496
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1453 0 0 0 57980 17 0 0 25 0 1 0 421234293 7675904 1431 4294967295 134512640 134672761 3221224576 3221223760 134559342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1874 1431 603 41 0 1833 0
vsize: 7496
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1460 0 0 0 58980 17 0 0 25 0 1 0 421234293 7675904 1438 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1874 1438 603 41 0 1833 0
vsize: 7496
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1461 0 0 0 59980 17 0 0 25 0 1 0 421234293 7675904 1439 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1874 1439 603 41 0 1833 0
vsize: 7496
[startup+610.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1461 0 0 0 60981 17 0 0 25 0 1 0 421234293 7675904 1439 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1874 1439 603 41 0 1833 0
vsize: 7496
[startup+620.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1467 0 0 0 61981 17 0 0 25 0 1 0 421234293 7839744 1445 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1914 1445 603 41 0 1873 0
vsize: 7656
[startup+627.738 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 28764
Raw data (stat): 28764 (minisat+) R 28763 25285 25284 0 -1 0 1467 0 0 0 61981 17 0 0 25 0 1 0 421234293 7839744 1445 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1914 1445 603 41 0 1873 0
vsize: 0

Child status: 30
Real time (s): 627.738
CPU time (s): 627.699
CPU user time (s): 627.515
CPU system time (s): 0.183972
CPU usage (%): 99.9938
Max. virtual memory (Kb): 7656
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	88
#### END VERIFIER DATA ####