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-jnh201.opb
MD5SUM	ba509931ad93c2223be235a06a9b3100
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	84
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	1.01884
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	14
Trace number 5475

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-14 00:20:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3940 boxname=wulflinc28 idbench=180 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ba509931ad93c2223be235a06a9b3100  /oldhome/oroussel/tmp/wulflinc28/normalized-jnh201.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc28/normalized-jnh201.opb /oldhome/oroussel/tmp/wulflinc28/normalized-jnh201.opb
IDLAUNCH: 3940
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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	: 3
cpu MHz		: 451.077
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:        894432 kB
Buffers:         34904 kB
Cached:          69540 kB
SwapCached:          4 kB
Active:          51692 kB
Inactive:        55532 kB
HighTotal:      131008 kB
HighFree:        57960 kB
LowTotal:       903652 kB
LowFree:        836472 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27380 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:27:23 (client local time) WITH STATUS 30 IN 395.061 SECONDS
stats: 3940 0 395.061 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     883     4250 |     264       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  200/200          
c |         0 |     873     4185 |      --       0       --      -- |     --   | -10/-65
c |         0 |     873     4185 |     349       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.040993 s)
c ==============================================================================
c [1mFound solution: 91[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 5812     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         8 |    7616    19965 |    2284       8      115    14.4 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4529          
c   -- var.elim.:  2000/4529          
c   -- var.elim.:  3000/4529          
c   -- var.elim.:  4000/4529          
c   -- var.elim.:  4529/4529          
c   -- var.elim.:  1000/2202          
c   -- var.elim.:  2000/2202          
c   -- var.elim.:  2202/2202          
c   -- var.elim.:  1000/1255          
c   -- var.elim.:  1255/1255          
c   -- var.elim.:  854/854          
c   -- var.elim.:  600/600          
c   -- var.elim.:  192/192          
c   -- subsuming                       
c   -- var.elim.:  590/590          
c   -- var.elim.:  5/5          
c |         8 |    2705    14737 |      --       8       --      -- |     --   | -4911/-5227
c |         8 |    2705    14737 |    1082       8      115    14.4 |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.47677 s)
c ==============================================================================
c [1mFound solution: 89[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        57 |    7342    26116 |    2202      57     7257   127.3 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4220          
c   -- var.elim.:  2000/4220          
c   -- var.elim.:  3000/4220          
c   -- var.elim.:  4000/4220          
c   -- var.elim.:  4220/4220          
c   -- var.elim.:  1000/1999          
c   -- var.elim.:  1999/1999          
c   -- var.elim.:  1000/1233          
c   -- var.elim.:  1233/1233          
c   -- var.elim.:  784/784          
c   -- var.elim.:  598/598          
c   -- var.elim.:  169/169          
c   -- subsuming                       
c   -- var.elim.:  379/379          
c   -- var.elim.:  19/19          
c |        57 |    2756    15825 |      --      57       --      -- |     --   | -4586/-10290
c |        57 |    2756    15825 |    1102      57     7257   127.3 |  0.000 % |
c |       160 |    2744    15759 |    1207     159    22083   138.9 |  0.563 % |
c ==============================================================================
c (current CPU-time: 3.12453 s)
c ==============================================================================
c [1mFound solution: 88[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       262 |    2756    15799 |     826     261    33413   128.0 |  0.563 % |
c   -- subsuming                       
c   -- var.elim.:  349/349          
c   -- var.elim.:  23/23          
c |       262 |    2740    15711 |      --     261       --      -- |     --   | -7/-15
c |       262 |    2740    15711 |    1096     196    16353    83.4 |  0.563 % |
c |       366 |    2740    15711 |    1205     300    30351   101.2 |  1.030 % |
c |       516 |    2740    15711 |    1326     450    55203   122.7 |  1.030 % |
c |       741 |    2740    15711 |    1458     675   102983   152.6 |  1.030 % |
c |      1078 |    2740    15711 |    1604    1012   177000   174.9 |  1.030 % |
c |      1584 |    2740    15711 |    1765    1518   285302   187.9 |  1.030 % |
c |      2346 |    2740    15711 |    1941    2280   470823   206.5 |  1.031 % |
c |      3485 |    2740    15711 |    2135    1791   342769   191.4 |  1.030 % |
c |      5193 |    2668    15066 |    2287    2714   543658   200.3 |  2.622 % |
c ==============================================================================
c (current CPU-time: 8.65868 s)
c ==============================================================================
c [1mFound solution: 87[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 5014     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6122 |    8945    29867 |    2683    2739   570890   208.4 |  2.622 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4833          
c   -- var.elim.:  2000/4833          
c   -- var.elim.:  3000/4833          
c   -- var.elim.:  4000/4833          
c   -- var.elim.:  4833/4833          
c   -- var.elim.:  1000/2147          
c   -- var.elim.:  2000/2147          
c   -- var.elim.:  2147/2147          
c   -- var.elim.:  1000/1212          
c   -- var.elim.:  1212/1212          
c   -- var.elim.:  844/844          
c   -- var.elim.:  567/567          
c   -- var.elim.:  164/164          
c   -- subsuming                       
c   -- var.elim.:  635/635          
c |      6122 |    4137    24644 |      --    2739       --      -- |     --   | -4808/-5222
c |      6122 |    4137    24644 |    1654    2739   570890   208.4 |  2.622 % |
c |      6224 |    4137    24644 |    1820    1320   223016   169.0 |  1.688 % |
c |      6375 |    4137    24644 |    2002    1471   253872   172.6 |  1.688 % |
c |      6600 |    4137    24644 |    2202    1696   313071   184.6 |  1.688 % |
c |      6937 |    4137    24644 |    2422    2033   396620   195.1 |  1.688 % |
c |      7444 |    4137    24644 |    2665    2540   524864   206.6 |  1.688 % |
c |      8203 |    4137    24644 |    2931    3299   734389   222.6 |  1.688 % |
c |      9344 |    4137    24644 |    3224    2266   538192   237.5 |  1.688 % |
c |     11054 |    4137    24644 |    3547    3976  1015105   255.3 |  1.688 % |
c |     13618 |    4137    24644 |    3901    3774  1021572   270.7 |  1.688 % |
c |     17464 |    4118    24552 |    4272    3170   710641   224.2 |  2.095 % |
c |     23230 |    4108    24495 |    4688    3865   869060   224.9 |  2.329 % |
c |     31882 |    4108    24495 |    5157    5333  1495895   280.5 |  2.328 % |
c |     44856 |    4108    24495 |    5672    4935   868725   176.0 |  2.329 % |
c |     64318 |    4108    24495 |    6240    5242  1062030   202.6 |  2.329 % |
c |     93510 |    4095    24421 |    6842    5655  1097686   194.1 |  2.619 % |
c ==============================================================================
c (current CPU-time: 138.24 s)
c ==============================================================================
c [1mFound solution: 84[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     93615 |    8242    34563 |    2472    5760  1127198   195.7 |  2.619 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4057          
c   -- var.elim.:  2000/4057          
c   -- var.elim.:  3000/4057          
c   -- var.elim.:  4000/4057          
c   -- var.elim.:  4057/4057          
c   -- var.elim.:  1000/1811          
c   -- var.elim.:  1811/1811          
c   -- var.elim.:  1000/1064          
c   -- var.elim.:  1064/1064          
c   -- var.elim.:  672/672          
c   -- var.elim.:  580/580          
c   -- var.elim.:  349/349          
c   -- var.elim.:  51/51          
c   -- subsuming                       
c |     93615 |    4118    24581 |      --    5760       --      -- |     --   | -4116/-9894
c |     93615 |    4118    24581 |    1647    2928   207741    70.9 |  2.619 % |
c |     93718 |    4118    24581 |    1811    1405    63117    44.9 |  2.891 % |
c |     93868 |    4118    24581 |    1993    1555    87116    56.0 |  2.890 % |
c |     94094 |    4118    24581 |    2192    1781   133726    75.1 |  2.890 % |
c |     94431 |    4118    24581 |    2411    2118   209045    98.7 |  2.890 % |
c |     94937 |    4118    24581 |    2652    2624   313157   119.3 |  2.891 % |
c |     95696 |    4118    24581 |    2918    3383   477039   141.0 |  2.890 % |
c |     96836 |    4118    24581 |    3209    3396   564870   166.3 |  2.891 % |
c |     98544 |    4118    24581 |    3530    2715   388250   143.0 |  2.895 % |
c |    101106 |    4118    24581 |    3884    3836   643877   167.9 |  2.890 % |
c |    104950 |    4118    24581 |    4272    4509   807930   179.2 |  2.890 % |
c |    110717 |    4118    24581 |    4699    3565   679180   190.5 |  2.891 % |
c |    119367 |    4118    24581 |    5169    4624   978835   211.7 |  2.890 % |
c |    132343 |    4105    24513 |    5668    5812  1029187   177.1 |  3.237 % |
c |    151804 |    4058    24242 |    6164    4664   713227   152.9 |  4.451 % |
c |    180998 |    4058    24242 |    6780    5721   748965   130.9 |  4.451 % |
c |    224787 |    4045    24166 |    7434    7278  1248393   171.5 |  4.740 % |
c |    290471 |    3557    20315 |    7191    4310   496863   115.3 | 12.370 % |
c ==============================================================================
c [1mOptimal solution: 84[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              : 47
c conflicts             : 298049         (755 /sec)
c decisions             : 555174         (1406 /sec)
c propagations          : 39300883       (99542 /sec)
c inspects              : 448183949      (1135163 /sec)
c CPU time              : 394.819 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.79 0.92 0.89 2/54 17091
Raw data (stat): 17091 (runsolver) R 17090 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480230801 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+9.99988 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 2573 0 0 0 988 10 0 0 25 0 1 0 480230801 10674176 2148 4294967295 134512640 134672761 3221224576 3221223024 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2606 2148 603 41 0 2565 0
vsize: 10424
[startup+19.9999 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3155 0 0 0 1986 12 0 0 25 0 1 0 480230801 13021184 2730 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3179 2730 603 41 0 3138 0
vsize: 12716
[startup+30.0006 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3271 0 0 0 2985 12 0 0 25 0 1 0 480230801 13549568 2846 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3308 2846 603 41 0 3267 0
vsize: 13232
[startup+40.0013 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3408 0 0 0 3985 13 0 0 25 0 1 0 480230801 14073856 2983 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3436 2983 603 41 0 3395 0
vsize: 13744
[startup+50.002 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3658 0 0 0 4984 14 0 0 25 0 1 0 480230801 15114240 3233 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3690 3233 603 41 0 3649 0
vsize: 14760
[startup+60.0027 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3659 0 0 0 5984 14 0 0 25 0 1 0 480230801 15073280 3234 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3680 3234 603 41 0 3639 0
vsize: 14720
[startup+70.0034 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3660 0 0 0 6984 14 0 0 25 0 1 0 480230801 15073280 3235 4294967295 134512640 134672761 3221224576 3221223616 134612791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3680 3235 603 41 0 3639 0
vsize: 14720
[startup+80.004 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3660 0 0 0 7983 15 0 0 25 0 1 0 480230801 15073280 3235 4294967295 134512640 134672761 3221224576 3221223760 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3680 3235 603 41 0 3639 0
vsize: 14720
[startup+90.0047 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3660 0 0 0 8983 15 0 0 25 0 1 0 480230801 15073280 3235 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3680 3235 603 41 0 3639 0
vsize: 14720
[startup+100.004 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3683 0 0 0 9983 15 0 0 25 0 1 0 480230801 15204352 3258 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3258 603 41 0 3671 0
vsize: 14848
[startup+110.005 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3758 0 0 0 10983 16 0 0 25 0 1 0 480230801 15466496 3333 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3776 3333 603 41 0 3735 0
vsize: 15104
[startup+120.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3971 0 0 0 11981 17 0 0 25 0 1 0 480230801 16384000 3546 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4000 3546 603 41 0 3959 0
vsize: 16000
[startup+130.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 3971 0 0 0 12981 17 0 0 25 0 1 0 480230801 16379904 3546 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3546 603 41 0 3958 0
vsize: 15996
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 13979 19 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223120 134621086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 14979 19 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+160.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 15979 20 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+170.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 16978 20 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+180.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 17978 20 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+190.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 18978 21 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+200.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 19978 21 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+210.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 20977 22 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+220.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 21977 22 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+230.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 22978 22 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 23978 22 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 24978 22 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+260.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 25978 22 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+270.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 26978 22 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+280.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 27979 22 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223120 134645372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+290.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 28979 22 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+300.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4247 0 0 0 29978 22 0 0 25 0 1 0 480230801 16912384 3678 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3678 603 41 0 4088 0
vsize: 16516
[startup+310.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4258 0 0 0 30978 22 0 0 25 0 1 0 480230801 16912384 3689 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3689 603 41 0 4088 0
vsize: 16516
[startup+320.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4298 0 0 0 31979 22 0 0 25 0 1 0 480230801 16986112 3729 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4147 3729 603 41 0 4106 0
vsize: 16588
[startup+330.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4298 0 0 0 32979 22 0 0 25 0 1 0 480230801 16973824 3729 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4144 3729 603 41 0 4103 0
vsize: 16576
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4298 0 0 0 33979 22 0 0 25 0 1 0 480230801 16969728 3729 4294967295 134512640 134672761 3221224576 3221223760 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4143 3729 603 41 0 4102 0
vsize: 16572
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4298 0 0 0 34979 22 0 0 25 0 1 0 480230801 16969728 3729 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4143 3729 603 41 0 4102 0
vsize: 16572
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4298 0 0 0 35980 22 0 0 25 0 1 0 480230801 16969728 3729 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4143 3729 603 41 0 4102 0
vsize: 16572
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4298 0 0 0 36980 22 0 0 25 0 1 0 480230801 16920576 3728 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4131 3728 603 41 0 4090 0
vsize: 16524
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4298 0 0 0 37980 22 0 0 25 0 1 0 480230801 16912384 3727 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3727 603 41 0 4088 0
vsize: 16516
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4298 0 0 0 38980 22 0 0 25 0 1 0 480230801 16912384 3727 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3727 603 41 0 4088 0
vsize: 16516
[startup+395.048 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 17091
Raw data (stat): 17091 (minisat+) R 17090 10614 10613 0 -1 0 4298 0 0 0 38980 22 0 0 25 0 1 0 480230801 16912384 3727 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3727 603 41 0 4088 0
vsize: 0

Child status: 30
Real time (s): 395.048
CPU time (s): 395.061
CPU user time (s): 394.823
CPU system time (s): 0.237963
CPU usage (%): 100.003
Max. virtual memory (Kb): 16588
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	84
#### END VERIFIER DATA ####