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-par32-1-c.opb
MD5SUM	8c1b8634a2f99e9f8e579ef031d10353
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	2630
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	2630
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	2630
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	2630
Total number of constraints	6569
Number of constraints which are clauses	6569
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	3
Trace number 5526

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-14 00:23:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3963 boxname=wulflinc10 idbench=203 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8c1b8634a2f99e9f8e579ef031d10353  /oldhome/oroussel/tmp/wulflinc10/normalized-par32-1-c.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc10/normalized-par32-1-c.opb /oldhome/oroussel/tmp/wulflinc10/normalized-par32-1-c.opb
IDLAUNCH: 3963
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        880780 kB
Buffers:         34720 kB
Cached:          99756 kB
SwapCached:        164 kB
Active:          52480 kB
Inactive:        85036 kB
HighTotal:      131008 kB
HighFree:        27580 kB
LowTotal:       903652 kB
LowFree:        853200 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10892 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:43:53 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 3963 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6569 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 |    6569    18020 |    1970       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2630          
c   -- var.elim.:  2000/2630          
c   -- var.elim.:  2630/2630          
c |         0 |    6447    17654 |      --       0       --      -- |     --   | -122/-366
c |         0 |    6447    17654 |    2578       0        0     nan |  0.000 % |
c |       101 |    6447    17654 |    2836     101     3176    31.4 |  0.004 % |
c |       251 |    6447    17654 |    3120     251     5744    22.9 |  0.000 % |
c |       476 |    6447    17654 |    3432     476    11028    23.2 |  0.000 % |
c |       813 |    6447    17654 |    3775     813    16422    20.2 |  0.000 % |
c |      1319 |    6447    17654 |    4153    1319    30356    23.0 |  0.000 % |
c |      2079 |    6447    17654 |    4568    2079    42522    20.5 |  0.000 % |
c |      3218 |    6447    17654 |    5025    3218    72436    22.5 |  0.000 % |
c |      4926 |    6447    17654 |    5527    4926   165007    33.5 |  0.000 % |
c |      7491 |    6440    17634 |    6074    560#### 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.86 0.93 0.90 2/54 29829
Raw data (stat): 29829 (runsolver) R 29828 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422030390 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1087 0 0 0 995 3 0 0 25 0 1 0 422030390 6012928 1065 4294967295 134512640 134672761 3221224560 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1468 1065 603 41 0 1427 0
vsize: 5872
[startup+20.0008 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1229 0 0 0 1994 3 0 0 25 0 1 0 422030390 6541312 1207 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1597 1207 603 41 0 1556 0
vsize: 6388
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1310 0 0 0 2994 3 0 0 25 0 1 0 422030390 6938624 1288 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1694 1288 603 41 0 1653 0
vsize: 6776
[startup+40.0012 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1356 0 0 0 3994 3 0 0 25 0 1 0 422030390 7163904 1334 4294967295 134512640 134672761 3221224560 3221223744 134615845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1749 1334 603 41 0 1708 0
vsize: 6996
[startup+50.0004 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1397 0 0 0 4994 4 0 0 25 0 1 0 422030390 7299072 1375 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1782 1375 603 41 0 1741 0
vsize: 7128
[startup+60.0007 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1559 0 0 0 5994 4 0 0 25 0 1 0 422030390 7946240 1537 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1940 1537 603 41 0 1899 0
vsize: 7760
[startup+70.001 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1605 0 0 0 6994 4 0 0 25 0 1 0 422030390 8151040 1583 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1990 1583 603 41 0 1949 0
vsize: 7960
[startup+80.0012 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1644 0 0 0 7994 4 0 0 25 0 1 0 422030390 8351744 1622 4294967295 134512640 134672761 3221224560 3221223744 134616020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2039 1622 603 41 0 1998 0
vsize: 8156
[startup+90.001 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1660 0 0 0 8994 4 0 0 25 0 1 0 422030390 8351744 1638 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2039 1638 603 41 0 1998 0
vsize: 8156
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1665 0 0 0 9994 5 0 0 25 0 1 0 422030390 8433664 1643 4294967295 134512640 134672761 3221224560 3221223760 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2059 1643 603 41 0 2018 0
vsize: 8236
[startup+110.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1672 0 0 0 10994 5 0 0 25 0 1 0 422030390 8433664 1650 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2059 1650 603 41 0 2018 0
vsize: 8236
[startup+120.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1730 0 0 0 11994 5 0 0 25 0 1 0 422030390 8695808 1708 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1708 603 41 0 2082 0
vsize: 8492
[startup+130.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1755 0 0 0 12994 5 0 0 25 0 1 0 422030390 8777728 1733 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2143 1733 603 41 0 2102 0
vsize: 8572
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1812 0 0 0 13994 5 0 0 25 0 1 0 422030390 9043968 1790 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2208 1790 603 41 0 2167 0
vsize: 8832
[startup+150.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1837 0 0 0 14994 5 0 0 25 0 1 0 422030390 9142272 1815 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2232 1815 603 41 0 2191 0
vsize: 8928
[startup+160.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1837 0 0 0 15995 5 0 0 25 0 1 0 422030390 9142272 1815 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2232 1815 603 41 0 2191 0
vsize: 8928
[startup+170.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1837 0 0 0 16995 5 0 0 25 0 1 0 422030390 9142272 1815 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2232 1815 603 41 0 2191 0
vsize: 8928
[startup+180.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1838 0 0 0 17995 5 0 0 25 0 1 0 422030390 9142272 1816 4294967295 134512640 134672761 3221224560 3221223696 134614800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2232 1816 603 41 0 2191 0
vsize: 8928
[startup+190.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1838 0 0 0 18995 5 0 0 25 0 1 0 422030390 9142272 1816 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2232 1816 603 41 0 2191 0
vsize: 8928
[startup+200.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1839 0 0 0 19995 5 0 0 25 0 1 0 422030390 9142272 1817 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2232 1817 603 41 0 2191 0
vsize: 8928
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1863 0 0 0 20996 5 0 0 25 0 1 0 422030390 9261056 1841 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2261 1841 603 41 0 2220 0
vsize: 9044
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1890 0 0 0 21996 5 0 0 25 0 1 0 422030390 9367552 1868 4294967295 134512640 134672761 3221224560 3221223744 134615514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1868 603 41 0 2246 0
vsize: 9148
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1890 0 0 0 22996 5 0 0 25 0 1 0 422030390 9367552 1868 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1868 603 41 0 2246 0
vsize: 9148
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1895 0 0 0 23996 5 0 0 25 0 1 0 422030390 9367552 1873 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1873 603 41 0 2246 0
vsize: 9148
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1895 0 0 0 24996 5 0 0 25 0 1 0 422030390 9367552 1873 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1873 603 41 0 2246 0
vsize: 9148
[startup+260.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1895 0 0 0 25996 5 0 0 25 0 1 0 422030390 9367552 1873 4294967295 134512640 134672761 3221224560 3221223744 134615698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1873 603 41 0 2246 0
vsize: 9148
[startup+270.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1905 0 0 0 26996 5 0 0 25 0 1 0 422030390 9367552 1883 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1883 603 41 0 2246 0
vsize: 9148
[startup+280.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1970 0 0 0 27996 6 0 0 25 0 1 0 422030390 9641984 1948 4294967295 134512640 134672761 3221224560 3221223744 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2354 1948 603 41 0 2313 0
vsize: 9416
[startup+290.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1970 0 0 0 28997 6 0 0 25 0 1 0 422030390 9641984 1948 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2354 1948 603 41 0 2313 0
vsize: 9416
[startup+300.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1971 0 0 0 29997 6 0 0 25 0 1 0 422030390 9641984 1949 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2354 1949 603 41 0 2313 0
vsize: 9416
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 1990 0 0 0 30997 6 0 0 25 0 1 0 422030390 9728000 1968 4294967295 134512640 134672761 3221224560 3221223696 134614715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2375 1968 603 41 0 2334 0
vsize: 9500
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2018 0 0 0 31997 6 0 0 25 0 1 0 422030390 9859072 1996 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2407 1996 603 41 0 2366 0
vsize: 9628
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2026 0 0 0 32997 6 0 0 25 0 1 0 422030390 9859072 2004 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2407 2004 603 41 0 2366 0
vsize: 9628
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2026 0 0 0 33997 6 0 0 25 0 1 0 422030390 9859072 2004 4294967295 134512640 134672761 3221224560 3221223468 1075349669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2407 2004 603 41 0 2366 0
vsize: 9628
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2035 0 0 0 34997 6 0 0 25 0 1 0 422030390 9953280 2013 4294967295 134512640 134672761 3221224560 3221223600 134612821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2430 2013 603 41 0 2389 0
vsize: 9720
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2042 0 0 0 35997 6 0 0 25 0 1 0 422030390 9953280 2020 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2430 2020 603 41 0 2389 0
vsize: 9720
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2060 0 0 0 36997 6 0 0 25 0 1 0 422030390 10027008 2038 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2448 2038 603 41 0 2407 0
vsize: 9792
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2060 0 0 0 37998 6 0 0 25 0 1 0 422030390 10027008 2038 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2448 2038 603 41 0 2407 0
vsize: 9792
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2074 0 0 0 38998 6 0 0 25 0 1 0 422030390 10113024 2052 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2469 2052 603 41 0 2428 0
vsize: 9876
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2074 0 0 0 39998 6 0 0 25 0 1 0 422030390 10104832 2052 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2052 603 41 0 2426 0
vsize: 9868
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2137 0 0 0 40998 7 0 0 25 0 1 0 422030390 10366976 2115 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2531 2115 603 41 0 2490 0
vsize: 10124
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2159 0 0 0 41998 7 0 0 25 0 1 0 422030390 10448896 2137 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2551 2137 603 41 0 2510 0
vsize: 10204
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2186 0 0 0 42998 7 0 0 25 0 1 0 422030390 10559488 2164 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2578 2164 603 41 0 2537 0
vsize: 10312
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2201 0 0 0 43999 7 0 0 25 0 1 0 422030390 10559488 2179 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2578 2179 603 41 0 2537 0
vsize: 10312
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2201 0 0 0 44999 7 0 0 25 0 1 0 422030390 10559488 2179 4294967295 134512640 134672761 3221224560 3221223600 134612972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2578 2179 603 41 0 2537 0
vsize: 10312
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2210 0 0 0 45999 7 0 0 25 0 1 0 422030390 10657792 2188 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2188 603 41 0 2561 0
vsize: 10408
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2217 0 0 0 46999 7 0 0 25 0 1 0 422030390 10657792 2195 4294967295 134512640 134672761 3221224560 3221223552 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2195 603 41 0 2561 0
vsize: 10408
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2225 0 0 0 47999 7 0 0 25 0 1 0 422030390 10657792 2203 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2203 603 41 0 2561 0
vsize: 10408
[startup+490.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2234 0 0 0 48999 7 0 0 25 0 1 0 422030390 10756096 2212 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2212 603 41 0 2585 0
vsize: 10504
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2234 0 0 0 49999 7 0 0 25 0 1 0 422030390 10756096 2212 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2212 603 41 0 2585 0
vsize: 10504
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2234 0 0 0 51000 7 0 0 25 0 1 0 422030390 10756096 2212 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2212 603 41 0 2585 0
vsize: 10504
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2234 0 0 0 52000 7 0 0 25 0 1 0 422030390 10756096 2212 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2212 603 41 0 2585 0
vsize: 10504
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2234 0 0 0 53000 7 0 0 25 0 1 0 422030390 10756096 2212 4294967295 134512640 134672761 3221224560 3221223744 134615991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2212 603 41 0 2585 0
vsize: 10504
[startup+540.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2234 0 0 0 54000 7 0 0 25 0 1 0 422030390 10756096 2212 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2212 603 41 0 2585 0
vsize: 10504
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2234 0 0 0 55000 7 0 0 25 0 1 0 422030390 10756096 2212 4294967295 134512640 134672761 3221224560 3221223744 134615985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2212 603 41 0 2585 0
vsize: 10504
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2241 0 0 0 56001 7 0 0 25 0 1 0 422030390 10756096 2219 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2219 603 41 0 2585 0
vsize: 10504
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2241 0 0 0 57001 7 0 0 25 0 1 0 422030390 10756096 2219 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2219 603 41 0 2585 0
vsize: 10504
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2241 0 0 0 58001 7 0 0 25 0 1 0 422030390 10756096 2219 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2219 603 41 0 2585 0
vsize: 10504
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2241 0 0 0 59001 7 0 0 25 0 1 0 422030390 10756096 2219 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2219 603 41 0 2585 0
vsize: 10504
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2241 0 0 0 60001 7 0 0 25 0 1 0 422030390 10756096 2219 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2219 603 41 0 2585 0
vsize: 10504
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2241 0 0 0 61002 7 0 0 25 0 1 0 422030390 10756096 2219 4294967295 134512640 134672761 3221224560 3221223720 134614557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2219 603 41 0 2585 0
vsize: 10504
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2243 0 0 0 62002 7 0 0 25 0 1 0 422030390 10756096 2221 4294967295 134512640 134672761 3221224560 3221223744 134615991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2221 603 41 0 2585 0
vsize: 10504
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2243 0 0 0 63002 7 0 0 25 0 1 0 422030390 10756096 2221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2221 603 41 0 2585 0
vsize: 10504
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2243 0 0 0 64002 7 0 0 25 0 1 0 422030390 10756096 2221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2221 603 41 0 2585 0
vsize: 10504
[startup+650.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2243 0 0 0 65002 7 0 0 25 0 1 0 422030390 10756096 2221 4294967295 134512640 134672761 3221224560 3221223568 134542667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2221 603 41 0 2585 0
vsize: 10504
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2251 0 0 0 66002 7 0 0 25 0 1 0 422030390 10756096 2229 4294967295 134512640 134672761 3221224560 3221223616 134644269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2229 603 41 0 2585 0
vsize: 10504
[startup+670.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2260 0 0 0 67003 7 0 0 25 0 1 0 422030390 10854400 2238 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2650 2238 603 41 0 2609 0
vsize: 10600
[startup+680.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2260 0 0 0 68003 7 0 0 25 0 1 0 422030390 10854400 2238 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2650 2238 603 41 0 2609 0
vsize: 10600
[startup+690.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2267 0 0 0 69003 7 0 0 25 0 1 0 422030390 10854400 2245 4294967295 134512640 134672761 3221224560 3221223696 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2650 2245 603 41 0 2609 0
vsize: 10600
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2279 0 0 0 70003 7 0 0 25 0 1 0 422030390 10932224 2257 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2669 2257 603 41 0 2628 0
vsize: 10676
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2317 0 0 0 71003 7 0 0 25 0 1 0 422030390 11063296 2295 4294967295 134512640 134672761 3221224560 3221223552 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2701 2295 603 41 0 2660 0
vsize: 10804
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2317 0 0 0 72003 7 0 0 25 0 1 0 422030390 11063296 2295 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2701 2295 603 41 0 2660 0
vsize: 10804
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2325 0 0 0 73004 7 0 0 25 0 1 0 422030390 11063296 2303 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2701 2303 603 41 0 2660 0
vsize: 10804
[startup+740.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2325 0 0 0 74003 8 0 0 25 0 1 0 422030390 11063296 2303 4294967295 134512640 134672761 3221224560 3221223696 134614685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2701 2303 603 41 0 2660 0
vsize: 10804
[startup+750.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2325 0 0 0 75002 8 0 0 25 0 1 0 422030390 11063296 2303 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2701 2303 603 41 0 2660 0
vsize: 10804
[startup+760.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2334 0 0 0 76002 8 0 0 25 0 1 0 422030390 11157504 2312 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2724 2312 603 41 0 2683 0
vsize: 10896
[startup+770.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2334 0 0 0 77003 8 0 0 25 0 1 0 422030390 11157504 2312 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2724 2312 603 41 0 2683 0
vsize: 10896
[startup+780.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2334 0 0 0 78003 8 0 0 25 0 1 0 422030390 11157504 2312 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2724 2312 603 41 0 2683 0
vsize: 10896
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2365 0 0 0 79003 8 0 0 25 0 1 0 422030390 11288576 2343 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2756 2343 603 41 0 2715 0
vsize: 11024
[startup+800.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2385 0 0 0 80003 8 0 0 25 0 1 0 422030390 11366400 2363 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2775 2363 603 41 0 2734 0
vsize: 11100
[startup+810.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2385 0 0 0 81002 8 0 0 25 0 1 0 422030390 11366400 2363 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2775 2363 603 41 0 2734 0
vsize: 11100
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2385 0 0 0 82002 8 0 0 25 0 1 0 422030390 11362304 2363 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2774 2363 603 41 0 2733 0
vsize: 11096
[startup+830.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2396 0 0 0 83002 8 0 0 25 0 1 0 422030390 11362304 2374 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2774 2374 603 41 0 2733 0
vsize: 11096
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2409 0 0 0 84002 8 0 0 25 0 1 0 422030390 11468800 2387 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2800 2387 603 41 0 2759 0
vsize: 11200
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2409 0 0 0 85002 8 0 0 25 0 1 0 422030390 11468800 2387 4294967295 134512640 134672761 3221224560 3221223744 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2800 2387 603 41 0 2759 0
vsize: 11200
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2409 0 0 0 86002 8 0 0 25 0 1 0 422030390 11464704 2387 4294967295 134512640 134672761 3221224560 3221223552 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2799 2387 603 41 0 2758 0
vsize: 11196
[startup+870.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2409 0 0 0 87002 8 0 0 25 0 1 0 422030390 11464704 2387 4294967295 134512640 134672761 3221224560 3221223760 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2799 2387 603 41 0 2758 0
vsize: 11196
[startup+880.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2409 0 0 0 88003 8 0 0 25 0 1 0 422030390 11464704 2387 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2799 2387 603 41 0 2758 0
vsize: 11196
[startup+890.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2409 0 0 0 89003 8 0 0 25 0 1 0 422030390 11460608 2387 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2798 2387 603 41 0 2757 0
vsize: 11192
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2409 0 0 0 90003 8 0 0 25 0 1 0 422030390 11460608 2387 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2798 2387 603 41 0 2757 0
vsize: 11192
[startup+910.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2409 0 0 0 91003 8 0 0 25 0 1 0 422030390 11460608 2387 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2798 2387 603 41 0 2757 0
vsize: 11192
[startup+920.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2409 0 0 0 92003 8 0 0 25 0 1 0 422030390 11460608 2387 4294967295 134512640 134672761 3221224560 3221223744 134615679 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2798 2387 603 41 0 2757 0
vsize: 11192
[startup+930.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2409 0 0 0 93004 8 0 0 25 0 1 0 422030390 11460608 2387 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2798 2387 603 41 0 2757 0
vsize: 11192
[startup+940.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2462 0 0 0 94004 9 0 0 25 0 1 0 422030390 11726848 2439 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2439 603 41 0 2822 0
vsize: 11452
[startup+950.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2463 0 0 0 95004 9 0 0 25 0 1 0 422030390 11726848 2440 4294967295 134512640 134672761 3221224560 3221223552 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2440 603 41 0 2822 0
vsize: 11452
[startup+960.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2463 0 0 0 96004 9 0 0 25 0 1 0 422030390 11726848 2440 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2440 603 41 0 2822 0
vsize: 11452
[startup+970.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2463 0 0 0 97004 9 0 0 25 0 1 0 422030390 11726848 2440 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2863 2440 603 41 0 2822 0
vsize: 11452
[startup+980.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2468 0 0 0 98004 9 0 0 25 0 1 0 422030390 11739136 2444 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2866 2444 603 41 0 2825 0
vsize: 11464
[startup+990.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2468 0 0 0 99005 9 0 0 25 0 1 0 422030390 11739136 2444 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2866 2444 603 41 0 2825 0
vsize: 11464
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2468 0 0 0 100005 9 0 0 25 0 1 0 422030390 11739136 2444 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2866 2444 603 41 0 2825 0
vsize: 11464
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2468 0 0 0 101005 9 0 0 25 0 1 0 422030390 11739136 2444 4294967295 134512640 134672761 3221224560 3221223744 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2866 2444 603 41 0 2825 0
vsize: 11464
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2483 0 0 0 102005 9 0 0 25 0 1 0 422030390 11796480 2458 4294967295 134512640 134672761 3221224560 3221223552 134565051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2880 2458 603 41 0 2839 0
vsize: 11520
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2517 0 0 0 103005 9 0 0 25 0 1 0 422030390 11931648 2491 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2913 2491 603 41 0 2872 0
vsize: 11652
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2534 0 0 0 104005 9 0 0 25 0 1 0 422030390 11997184 2507 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2929 2507 603 41 0 2888 0
vsize: 11716
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2534 0 0 0 105006 9 0 0 25 0 1 0 422030390 11993088 2506 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2928 2506 603 41 0 2887 0
vsize: 11712
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2535 0 0 0 106006 9 0 0 25 0 1 0 422030390 11993088 2507 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2928 2507 603 41 0 2887 0
vsize: 11712
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2535 0 0 0 107006 9 0 0 25 0 1 0 422030390 11993088 2507 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2928 2507 603 41 0 2887 0
vsize: 11712
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2536 0 0 0 108006 9 0 0 25 0 1 0 422030390 11993088 2508 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2928 2508 603 41 0 2887 0
vsize: 11712
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2552 0 0 0 109007 9 0 0 25 0 1 0 422030390 12058624 2523 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2944 2523 603 41 0 2903 0
vsize: 11776
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2553 0 0 0 110007 9 0 0 25 0 1 0 422030390 12058624 2524 4294967295 134512640 134672761 3221224560 3221223696 134614677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2944 2524 603 41 0 2903 0
vsize: 11776
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2553 0 0 0 111007 9 0 0 25 0 1 0 422030390 12058624 2524 4294967295 134512640 134672761 3221224560 3221223616 134644260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2944 2524 603 41 0 2903 0
vsize: 11776
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2553 0 0 0 112007 9 0 0 25 0 1 0 422030390 12058624 2524 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2944 2524 603 41 0 2903 0
vsize: 11776
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2554 0 0 0 113007 9 0 0 25 0 1 0 422030390 12058624 2525 4294967295 134512640 134672761 3221224560 3221223708 134614482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2944 2525 603 41 0 2903 0
vsize: 11776
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2554 0 0 0 114007 9 0 0 25 0 1 0 422030390 12058624 2525 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2944 2525 603 41 0 2903 0
vsize: 11776
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2570 0 0 0 115008 9 0 0 25 0 1 0 422030390 12124160 2540 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2960 2540 603 41 0 2919 0
vsize: 11840
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2573 0 0 0 116008 9 0 0 25 0 1 0 422030390 12128256 2542 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2961 2542 603 41 0 2920 0
vsize: 11844
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2573 0 0 0 117008 9 0 0 25 0 1 0 422030390 12128256 2542 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2961 2542 603 41 0 2920 0
vsize: 11844
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2574 0 0 0 118008 9 0 0 25 0 1 0 422030390 12124160 2542 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2960 2542 603 41 0 2919 0
vsize: 11840
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2590 0 0 0 119008 9 0 0 25 0 1 0 422030390 12189696 2557 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2976 2557 603 41 0 2935 0
vsize: 11904
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29829
Raw data (stat): 29829 (minisat+) R 29828 25347 25346 0 -1 0 2590 0 0 0 120008 9 0 0 25 0 1 0 422030390 12189696 2557 4294967295 134512640 134672761 3221224560 3221223744 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2976 2557 603 41 0 2935 0
vsize: 11904
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29829
Raw data (stat): 29829 (minisat+) Z 29828 25347 25346 0 -1 12 2590 0 0 0 120008 9 0 0 25 0 1 0 422030390 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.01
CPU time (s): 1200.19
CPU user time (s): 1200.09
CPU system time (s): 0.099984
CPU usage (%): 100.015
Max. virtual memory (Kb): 11904
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####