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-4-c.opb
MD5SUM	3d2c3109962e8068c6ff1a393a02942b
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	2666
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	2666
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	2666
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	2666
Total number of constraints	6659
Number of constraints which are clauses	6659
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 5550

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 00:26:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3969 boxname=wulflinc24 idbench=209 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3d2c3109962e8068c6ff1a393a02942b  /oldhome/oroussel/tmp/wulflinc24/normalized-par32-4-c.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc24/normalized-par32-4-c.opb /oldhome/oroussel/tmp/wulflinc24/normalized-par32-4-c.opb
IDLAUNCH: 3969
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 3
cpu MHz		: 451.080
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:        842204 kB
Buffers:         34624 kB
Cached:         115364 kB
SwapCached:       3828 kB
Active:          51164 kB
Inactive:       105536 kB
HighTotal:      131008 kB
HighFree:        13300 kB
LowTotal:       903652 kB
LowFree:        828904 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30164 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:46:30 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 3969 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6659 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 |    6659    18272 |    1997       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2666          
c   -- var.elim.:  2000/2666          
c   -- var.elim.:  2666/2666          
c |         0 |    6537    17906 |      --       0       --      -- |     --   | -122/-366
c |         0 |    6537    17906 |    2614       0        0     nan |  0.000 % |
c |       101 |    6537    17906 |    2876     101     4057    40.2 |  0.003 % |
c |       251 |    6537    17906 |    3163     251     9065    36.1 |  0.000 % |
c |       476 |    6537    17906 |    3480     476    16469    34.6 |  0.000 % |
c |       813 |    6537    17906 |    3828     813    28543    35.1 |  0.000 % |
c |      1319 |    6537    17906 |    4211    1319    46039    34.9 |  0.000 % |
c |      2079 |    6537    17906 |    4632    2079    72902    35.1 |  0.000 % |
c |      3219 |    6530    17886 |    5090    3218   114790    35.7 |  0.075 % |
c |      4927 |    6530    17886 |    55#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.91 0.89 2/54 1620
Raw data (stat): 1620 (runsolver) R 1619 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480256822 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.0014 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1076 0 0 0 996 3 0 0 25 0 1 0 480256822 6033408 1054 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1473 1054 603 41 0 1432 0
vsize: 5892
[startup+20.0021 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1171 0 0 0 1995 3 0 0 25 0 1 0 480256822 6295552 1149 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1537 1149 603 41 0 1496 0
vsize: 6148
[startup+30.0022 s]
Raw data (loadavg): 0.94 0.92 0.89 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1240 0 0 0 2994 4 0 0 25 0 1 0 480256822 6692864 1218 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1634 1218 603 41 0 1593 0
vsize: 6536
[startup+40.0022 s]
Raw data (loadavg): 0.95 0.92 0.89 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1255 0 0 0 3994 4 0 0 25 0 1 0 480256822 6692864 1233 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1634 1233 603 41 0 1593 0
vsize: 6536
[startup+50.0029 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1302 0 0 0 4994 4 0 0 25 0 1 0 480256822 6926336 1280 4294967295 134512640 134672761 3221224560 3221223696 134614741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1691 1280 603 41 0 1650 0
vsize: 6764
[startup+60.0033 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1318 0 0 0 5994 4 0 0 25 0 1 0 480256822 6995968 1296 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1708 1296 603 41 0 1667 0
vsize: 6832
[startup+70.0033 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1336 0 0 0 6994 4 0 0 25 0 1 0 480256822 7077888 1314 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1314 603 41 0 1687 0
vsize: 6912
[startup+80.003 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1431 0 0 0 7994 4 0 0 25 0 1 0 480256822 7446528 1409 4294967295 134512640 134672761 3221224560 3221223552 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1818 1409 603 41 0 1777 0
vsize: 7272
[startup+90.0034 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1551 0 0 0 8994 5 0 0 25 0 1 0 480256822 7979008 1529 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1948 1529 603 41 0 1907 0
vsize: 7792
[startup+100.003 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1633 0 0 0 9994 5 0 0 25 0 1 0 480256822 8232960 1611 4294967295 134512640 134672761 3221224560 3221223696 134614670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2010 1611 603 41 0 1969 0
vsize: 8040
[startup+110.004 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1687 0 0 0 10994 5 0 0 25 0 1 0 480256822 8454144 1665 4294967295 134512640 134672761 3221224560 3221223616 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2064 1665 603 41 0 2023 0
vsize: 8256
[startup+120.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1696 0 0 0 11994 5 0 0 25 0 1 0 480256822 8536064 1674 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2084 1674 603 41 0 2043 0
vsize: 8336
[startup+130.004 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1714 0 0 0 12994 5 0 0 25 0 1 0 480256822 8605696 1692 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2101 1692 603 41 0 2060 0
vsize: 8404
[startup+140.005 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1785 0 0 0 13994 5 0 0 25 0 1 0 480256822 8839168 1763 4294967295 134512640 134672761 3221224560 3221223580 134565156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2158 1763 603 41 0 2117 0
vsize: 8632
[startup+150.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1805 0 0 0 14995 5 0 0 25 0 1 0 480256822 8970240 1783 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2190 1783 603 41 0 2149 0
vsize: 8760
[startup+160.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1902 0 0 0 15995 5 0 0 25 0 1 0 480256822 9371648 1880 4294967295 134512640 134672761 3221224560 3221223600 134612848 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2288 1880 603 41 0 2247 0
vsize: 9152
[startup+170.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1919 0 0 0 16995 5 0 0 25 0 1 0 480256822 9445376 1897 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2306 1897 603 41 0 2265 0
vsize: 9224
[startup+180.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1970 0 0 0 17995 6 0 0 25 0 1 0 480256822 9662464 1948 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2359 1948 603 41 0 2318 0
vsize: 9436
[startup+190.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1978 0 0 0 18995 6 0 0 25 0 1 0 480256822 9662464 1956 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2359 1956 603 41 0 2318 0
vsize: 9436
[startup+200.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1978 0 0 0 19995 6 0 0 25 0 1 0 480256822 9662464 1956 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2359 1956 603 41 0 2318 0
vsize: 9436
[startup+210.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1978 0 0 0 20995 6 0 0 25 0 1 0 480256822 9662464 1956 4294967295 134512640 134672761 3221224560 3221223600 134612578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2359 1956 603 41 0 2318 0
vsize: 9436
[startup+220.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1995 0 0 0 21995 6 0 0 25 0 1 0 480256822 9760768 1973 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1973 603 41 0 2342 0
vsize: 9532
[startup+230.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1995 0 0 0 22996 6 0 0 25 0 1 0 480256822 9760768 1973 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1973 603 41 0 2342 0
vsize: 9532
[startup+240.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1995 0 0 0 23996 6 0 0 25 0 1 0 480256822 9760768 1973 4294967295 134512640 134672761 3221224560 3221223760 134610602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1973 603 41 0 2342 0
vsize: 9532
[startup+250.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1995 0 0 0 24996 6 0 0 25 0 1 0 480256822 9760768 1973 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1973 603 41 0 2342 0
vsize: 9532
[startup+260.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1995 0 0 0 25996 6 0 0 25 0 1 0 480256822 9760768 1973 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1973 603 41 0 2342 0
vsize: 9532
[startup+270.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1997 0 0 0 26996 6 0 0 25 0 1 0 480256822 9760768 1975 4294967295 134512640 134672761 3221224560 3221223744 134615529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1975 603 41 0 2342 0
vsize: 9532
[startup+280.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1997 0 0 0 27997 6 0 0 25 0 1 0 480256822 9760768 1975 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1975 603 41 0 2342 0
vsize: 9532
[startup+290.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 1997 0 0 0 28997 6 0 0 25 0 1 0 480256822 9760768 1975 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1975 603 41 0 2342 0
vsize: 9532
[startup+300.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2005 0 0 0 29997 6 0 0 25 0 1 0 480256822 9760768 1983 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1983 603 41 0 2342 0
vsize: 9532
[startup+310.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2005 0 0 0 30997 6 0 0 25 0 1 0 480256822 9760768 1983 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1983 603 41 0 2342 0
vsize: 9532
[startup+320.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2005 0 0 0 31997 6 0 0 25 0 1 0 480256822 9760768 1983 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1983 603 41 0 2342 0
vsize: 9532
[startup+330.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2005 0 0 0 32997 6 0 0 25 0 1 0 480256822 9760768 1983 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2383 1983 603 41 0 2342 0
vsize: 9532
[startup+340.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2033 0 0 0 33998 6 0 0 25 0 1 0 480256822 9891840 2011 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2415 2011 603 41 0 2374 0
vsize: 9660
[startup+350.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2107 0 0 0 34998 6 0 0 25 0 1 0 480256822 10153984 2085 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2479 2085 603 41 0 2438 0
vsize: 9916
[startup+360.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2107 0 0 0 35998 6 0 0 25 0 1 0 480256822 10153984 2085 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2479 2085 603 41 0 2438 0
vsize: 9916
[startup+370.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2108 0 0 0 36998 6 0 0 25 0 1 0 480256822 10153984 2086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2479 2086 603 41 0 2438 0
vsize: 9916
[startup+380.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2114 0 0 0 37998 6 0 0 25 0 1 0 480256822 10231808 2092 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2498 2092 603 41 0 2457 0
vsize: 9992
[startup+390.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2187 0 0 0 38998 6 0 0 25 0 1 0 480256822 10498048 2165 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2563 2165 603 41 0 2522 0
vsize: 10252
[startup+400.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2187 0 0 0 39998 6 0 0 25 0 1 0 480256822 10498048 2165 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2563 2165 603 41 0 2522 0
vsize: 10252
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2188 0 0 0 40998 6 0 0 25 0 1 0 480256822 10498048 2166 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2563 2166 603 41 0 2522 0
vsize: 10252
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2189 0 0 0 41999 6 0 0 25 0 1 0 480256822 10498048 2167 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2563 2167 603 41 0 2522 0
vsize: 10252
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2203 0 0 0 42999 6 0 0 25 0 1 0 480256822 10588160 2181 4294967295 134512640 134672761 3221224560 3221223328 134645351 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2585 2181 603 41 0 2544 0
vsize: 10340
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2207 0 0 0 43999 6 0 0 25 0 1 0 480256822 10588160 2185 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2585 2185 603 41 0 2544 0
vsize: 10340
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2245 0 0 0 44999 7 0 0 25 0 1 0 480256822 10719232 2223 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2617 2223 603 41 0 2576 0
vsize: 10468
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2275 0 0 0 45999 7 0 0 25 0 1 0 480256822 10842112 2253 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2647 2253 603 41 0 2606 0
vsize: 10588
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2288 0 0 0 46999 7 0 0 25 0 1 0 480256822 10932224 2266 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2669 2266 603 41 0 2628 0
vsize: 10676
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2288 0 0 0 47999 7 0 0 25 0 1 0 480256822 10932224 2266 4294967295 134512640 134672761 3221224560 3221223760 134610667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2669 2266 603 41 0 2628 0
vsize: 10676
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2308 0 0 0 48999 7 0 0 25 0 1 0 480256822 11018240 2286 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2286 603 41 0 2649 0
vsize: 10760
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 50000 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 51000 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 52000 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 53000 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 54000 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 55001 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 56001 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223720 134614477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 57001 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223616 134644281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 58001 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 59001 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 60001 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 61002 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2309 0 0 0 62002 7 0 0 25 0 1 0 480256822 11018240 2287 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2287 603 41 0 2649 0
vsize: 10760
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2310 0 0 0 63002 7 0 0 25 0 1 0 480256822 11018240 2288 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2288 603 41 0 2649 0
vsize: 10760
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2313 0 0 0 64002 7 0 0 25 0 1 0 480256822 11018240 2291 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2291 603 41 0 2649 0
vsize: 10760
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2324 0 0 0 65002 7 0 0 25 0 1 0 480256822 11018240 2302 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2690 2302 603 41 0 2649 0
vsize: 10760
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2340 0 0 0 66002 7 0 0 25 0 1 0 480256822 11112448 2318 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2713 2318 603 41 0 2672 0
vsize: 10852
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2340 0 0 0 67003 7 0 0 25 0 1 0 480256822 11112448 2318 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2713 2318 603 41 0 2672 0
vsize: 10852
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2340 0 0 0 68003 7 0 0 25 0 1 0 480256822 11112448 2318 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2713 2318 603 41 0 2672 0
vsize: 10852
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2340 0 0 0 69003 7 0 0 25 0 1 0 480256822 11112448 2318 4294967295 134512640 134672761 3221224560 3221223616 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2713 2318 603 41 0 2672 0
vsize: 10852
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2348 0 0 0 70003 7 0 0 25 0 1 0 480256822 11112448 2326 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2713 2326 603 41 0 2672 0
vsize: 10852
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2348 0 0 0 71003 7 0 0 25 0 1 0 480256822 11112448 2326 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2713 2326 603 41 0 2672 0
vsize: 10852
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2348 0 0 0 72004 7 0 0 25 0 1 0 480256822 11112448 2326 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2713 2326 603 41 0 2672 0
vsize: 10852
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2348 0 0 0 73004 7 0 0 25 0 1 0 480256822 11112448 2326 4294967295 134512640 134672761 3221224560 3221223696 134614713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2713 2326 603 41 0 2672 0
vsize: 10852
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2357 0 0 0 74004 7 0 0 25 0 1 0 480256822 11210752 2335 4294967295 134512640 134672761 3221224560 3221223600 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2335 603 41 0 2696 0
vsize: 10948
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2357 0 0 0 75004 7 0 0 25 0 1 0 480256822 11210752 2335 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2335 603 41 0 2696 0
vsize: 10948
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2357 0 0 0 76005 7 0 0 25 0 1 0 480256822 11210752 2335 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2335 603 41 0 2696 0
vsize: 10948
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2364 0 0 0 77005 7 0 0 25 0 1 0 480256822 11210752 2342 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2342 603 41 0 2696 0
vsize: 10948
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2364 0 0 0 78005 7 0 0 25 0 1 0 480256822 11210752 2342 4294967295 134512640 134672761 3221224560 3221223600 134614212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2342 603 41 0 2696 0
vsize: 10948
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2364 0 0 0 79005 7 0 0 25 0 1 0 480256822 11210752 2342 4294967295 134512640 134672761 3221224560 3221223712 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2342 603 41 0 2696 0
vsize: 10948
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2364 0 0 0 80005 7 0 0 25 0 1 0 480256822 11210752 2342 4294967295 134512640 134672761 3221224560 3221223760 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2342 603 41 0 2696 0
vsize: 10948
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2372 0 0 0 81005 7 0 0 25 0 1 0 480256822 11210752 2350 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2350 603 41 0 2696 0
vsize: 10948
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2372 0 0 0 82006 7 0 0 25 0 1 0 480256822 11210752 2350 4294967295 134512640 134672761 3221224560 3221223568 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2350 603 41 0 2696 0
vsize: 10948
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2372 0 0 0 83006 7 0 0 25 0 1 0 480256822 11210752 2350 4294967295 134512640 134672761 3221224560 3221223552 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2350 603 41 0 2696 0
vsize: 10948
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2372 0 0 0 84006 7 0 0 25 0 1 0 480256822 11210752 2350 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2350 603 41 0 2696 0
vsize: 10948
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2372 0 0 0 85006 7 0 0 25 0 1 0 480256822 11210752 2350 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2350 603 41 0 2696 0
vsize: 10948
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2372 0 0 0 86006 7 0 0 25 0 1 0 480256822 11210752 2350 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2737 2350 603 41 0 2696 0
vsize: 10948
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2381 0 0 0 87006 7 0 0 25 0 1 0 480256822 11309056 2359 4294967295 134512640 134672761 3221224560 3221223552 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2359 603 41 0 2720 0
vsize: 11044
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2388 0 0 0 88006 7 0 0 25 0 1 0 480256822 11309056 2366 4294967295 134512640 134672761 3221224560 3221223664 134604309 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2366 603 41 0 2720 0
vsize: 11044
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2388 0 0 0 89007 7 0 0 25 0 1 0 480256822 11309056 2366 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2366 603 41 0 2720 0
vsize: 11044
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2388 0 0 0 90007 7 0 0 25 0 1 0 480256822 11309056 2366 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2366 603 41 0 2720 0
vsize: 11044
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2388 0 0 0 91007 7 0 0 25 0 1 0 480256822 11309056 2366 4294967295 134512640 134672761 3221224560 3221223744 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2366 603 41 0 2720 0
vsize: 11044
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2388 0 0 0 92007 7 0 0 25 0 1 0 480256822 11309056 2366 4294967295 134512640 134672761 3221224560 3221223744 134615617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2366 603 41 0 2720 0
vsize: 11044
[startup+930.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2388 0 0 0 93007 7 0 0 25 0 1 0 480256822 11309056 2366 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2366 603 41 0 2720 0
vsize: 11044
[startup+940.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2388 0 0 0 94008 7 0 0 25 0 1 0 480256822 11309056 2366 4294967295 134512640 134672761 3221224560 3221223744 134615843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2366 603 41 0 2720 0
vsize: 11044
[startup+950.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2388 0 0 0 95008 7 0 0 25 0 1 0 480256822 11309056 2366 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2366 603 41 0 2720 0
vsize: 11044
[startup+960.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2388 0 0 0 96008 7 0 0 25 0 1 0 480256822 11309056 2366 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2761 2366 603 41 0 2720 0
vsize: 11044
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2410 0 0 0 97008 7 0 0 25 0 1 0 480256822 11472896 2388 4294967295 134512640 134672761 3221224560 3221223744 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2801 2388 603 41 0 2760 0
vsize: 11204
[startup+980.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2410 0 0 0 98008 7 0 0 25 0 1 0 480256822 11472896 2388 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2801 2388 603 41 0 2760 0
vsize: 11204
[startup+990.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2410 0 0 0 99008 7 0 0 25 0 1 0 480256822 11472896 2388 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2801 2388 603 41 0 2760 0
vsize: 11204
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2410 0 0 0 100009 7 0 0 25 0 1 0 480256822 11472896 2388 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2801 2388 603 41 0 2760 0
vsize: 11204
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2418 0 0 0 101009 7 0 0 25 0 1 0 480256822 11501568 2395 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2395 603 41 0 2767 0
vsize: 11232
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2445 0 0 0 102009 7 0 0 25 0 1 0 480256822 11616256 2422 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2836 2422 603 41 0 2795 0
vsize: 11344
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2462 0 0 0 103009 7 0 0 25 0 1 0 480256822 11681792 2438 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2852 2438 603 41 0 2811 0
vsize: 11408
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2512 0 0 0 104009 8 0 0 25 0 1 0 480256822 11882496 2488 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2901 2488 603 41 0 2860 0
vsize: 11604
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2572 0 0 0 105009 8 0 0 25 0 1 0 480256822 12132352 2548 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2962 2548 603 41 0 2921 0
vsize: 11848
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2572 0 0 0 106009 8 0 0 25 0 1 0 480256822 12132352 2548 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2962 2548 603 41 0 2921 0
vsize: 11848
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2572 0 0 0 107010 8 0 0 25 0 1 0 480256822 12120064 2547 4294967295 134512640 134672761 3221224560 3221223744 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2959 2547 603 41 0 2918 0
vsize: 11836
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2573 0 0 0 108010 8 0 0 25 0 1 0 480256822 12120064 2548 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2959 2548 603 41 0 2918 0
vsize: 11836
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2573 0 0 0 109010 8 0 0 25 0 1 0 480256822 12120064 2548 4294967295 134512640 134672761 3221224560 3221223744 134615551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2959 2548 603 41 0 2918 0
vsize: 11836
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2573 0 0 0 110010 8 0 0 25 0 1 0 480256822 12120064 2548 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2959 2548 603 41 0 2918 0
vsize: 11836
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2573 0 0 0 111010 8 0 0 25 0 1 0 480256822 12079104 2547 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2949 2547 603 41 0 2908 0
vsize: 11796
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2574 0 0 0 112011 8 0 0 25 0 1 0 480256822 12021760 2535 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2935 2535 603 41 0 2894 0
vsize: 11740
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2574 0 0 0 113011 8 0 0 25 0 1 0 480256822 12021760 2535 4294967295 134512640 134672761 3221224560 3221223744 134615945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2935 2535 603 41 0 2894 0
vsize: 11740
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2574 0 0 0 114011 8 0 0 25 0 1 0 480256822 12021760 2535 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2935 2535 603 41 0 2894 0
vsize: 11740
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2574 0 0 0 115012 8 0 0 25 0 1 0 480256822 12021760 2535 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2935 2535 603 41 0 2894 0
vsize: 11740
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2574 0 0 0 116012 8 0 0 25 0 1 0 480256822 12021760 2535 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2935 2535 603 41 0 2894 0
vsize: 11740
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2574 0 0 0 117013 8 0 0 25 0 1 0 480256822 12021760 2535 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2935 2535 603 41 0 2894 0
vsize: 11740
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2574 0 0 0 118013 8 0 0 25 0 1 0 480256822 12021760 2535 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2935 2535 603 41 0 2894 0
vsize: 11740
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2574 0 0 0 119013 8 0 0 25 0 1 0 480256822 12021760 2535 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2935 2535 603 41 0 2894 0
vsize: 11740
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1620
Raw data (stat): 1620 (minisat+) R 1619 28546 28545 0 -1 0 2574 0 0 0 120013 8 0 0 25 0 1 0 480256822 12021760 2535 4294967295 134512640 134672761 3221224560 3221223760 134610667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2935 2535 603 41 0 2894 0
vsize: 11740
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1620
Raw data (stat): 1620 (minisat+) Z 1619 28546 28545 0 -1 12 2574 0 0 0 120013 9 0 0 25 0 1 0 480256822 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.04
CPU time (s): 1200.23
CPU user time (s): 1200.14
CPU system time (s): 0.092985
CPU usage (%): 100.016
Max. virtual memory (Kb): 11848
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####