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.opb
MD5SUM	4ad922a0ad53056b410be6ab5caa6b5b
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	6352
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	6352
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	6352
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	6352
Total number of constraints	13489
Number of constraints which are clauses	13489
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	1
Maximum length of a constraint	3
Trace number 6317

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        905784 kB
Buffers:         36224 kB
Cached:          67984 kB
SwapCached:       4932 kB
Active:          58352 kB
Inactive:        53664 kB
HighTotal:      131008 kB
HighFree:        59248 kB
LowTotal:       903652 kB
LowFree:        846536 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11288 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:31:34 (client local time) WITH STATUS 0 IN 1200.13 SECONDS
stats: 4722 7 1200.13 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13075 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9815    24584 |    3271       0        0     nan |  0.000 % |
c |       100 |    9815    24584 |    3598     100     1175    11.8 | 24.906 % |
c |       250 |    9815    24584 |    3957     250     4761    19.0 | 24.906 % |
c |       476 |    9815    24584 |    4353     476     8036    16.9 | 24.906 % |
c |       814 |    9805    24562 |    4789     813    16099    19.8 | 24.969 % |
c |      1321 |    9805    24562 |    5267    1320    31268    23.7 | 24.969 % |
c |      2080 |    9805    24562 |    5794    2079    42787    20.6 | 24.969 % |
c |      3220 |    9805    24562 |    6374    3219    75648    23.5 | 24.969 % |
c |      4928 |    9805    24562 |    7011    4927   107201    21.8 | 24.969 % |
c |      7490 |    9805    24562 |    7712    7489   180306    24.1 | 24.969 % |
c |     11334 |    9805    24562 |    8484    6526   158927    24.4 | 24.969 % |
c |     17101 |    9805    24562 |    9332    7165   174694    24.4 | 24.969 % |
c |     25751 |    9805    24562 |   10265   10288   256474    24.9 | 24.969 % |
c |     38726 |    9805    24562 |   11292   11339   271909    24.0 | 24.969 % |
c |     58189 |    9805    24562 |   12421   11405   270262    23.7 | 24.969 % |
c |     87381 |    9805    24562 |   13663   12378   287949    23.3 | 24.969 % |
c |    131171 |    9805    24562 |   15030   10244   241970    23.6 | 24.969 % |
c |    196856 |    9805    24562 |   16533    8936   193461    21.6 | 24.969 % |
c |    295383 |    9805    24562 |   18186   16303   374771    23.0 | 24.969 % |
c |    443174 |    9805    24562 |   20005   15022   328559    21.9 | 24.969 % |
#### 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.92 0.98 0.93 2/54 7169
Raw data (stat): 7169 (runsolver) R 7168 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423387526 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.0006 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1253 0 0 0 993 4 0 0 25 0 1 0 423387526 6541312 1192 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1597 1192 603 41 0 1556 0
vsize: 6388
[startup+20.002 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1254 0 0 0 1992 4 0 0 25 0 1 0 423387526 6545408 1193 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1598 1193 603 41 0 1557 0
vsize: 6392
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1254 0 0 0 2992 4 0 0 25 0 1 0 423387526 6545408 1193 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1598 1193 603 41 0 1557 0
vsize: 6392
[startup+40.0028 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1258 0 0 0 3992 4 0 0 25 0 1 0 423387526 6684672 1197 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1632 1197 603 41 0 1591 0
vsize: 6528
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1318 0 0 0 4992 4 0 0 25 0 1 0 423387526 6828032 1257 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1667 1257 603 41 0 1626 0
vsize: 6668
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1332 0 0 0 5992 4 0 0 25 0 1 0 423387526 6963200 1271 4294967295 134512640 134672761 3221224560 3221223732 134559669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1700 1271 603 41 0 1659 0
vsize: 6800
[startup+70.0033 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1373 0 0 0 6991 5 0 0 25 0 1 0 423387526 7098368 1312 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1312 603 41 0 1692 0
vsize: 6932
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1387 0 0 0 7990 5 0 0 25 0 1 0 423387526 7233536 1326 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1766 1326 603 41 0 1725 0
vsize: 7064
[startup+90.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1393 0 0 0 8990 5 0 0 25 0 1 0 423387526 7233536 1332 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1766 1332 603 41 0 1725 0
vsize: 7064
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1404 0 0 0 9990 5 0 0 25 0 1 0 423387526 7233536 1343 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1766 1343 603 41 0 1725 0
vsize: 7064
[startup+110.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1447 0 0 0 10990 5 0 0 25 0 1 0 423387526 7512064 1386 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1386 603 41 0 1793 0
vsize: 7336
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1450 0 0 0 11990 5 0 0 25 0 1 0 423387526 7512064 1389 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1389 603 41 0 1793 0
vsize: 7336
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1460 0 0 0 12990 5 0 0 25 0 1 0 423387526 7512064 1399 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1399 603 41 0 1793 0
vsize: 7336
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1465 0 0 0 13990 5 0 0 25 0 1 0 423387526 7512064 1404 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1404 603 41 0 1793 0
vsize: 7336
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1467 0 0 0 14991 5 0 0 25 0 1 0 423387526 7512064 1406 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1406 603 41 0 1793 0
vsize: 7336
[startup+160.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1513 0 0 0 15991 5 0 0 25 0 1 0 423387526 7811072 1452 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1907 1452 603 41 0 1866 0
vsize: 7628
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1536 0 0 0 16991 6 0 0 25 0 1 0 423387526 7811072 1475 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1907 1475 603 41 0 1866 0
vsize: 7628
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1549 0 0 0 17991 6 0 0 25 0 1 0 423387526 7942144 1488 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1488 603 41 0 1898 0
vsize: 7756
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1558 0 0 0 18991 6 0 0 25 0 1 0 423387526 7942144 1497 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1497 603 41 0 1898 0
vsize: 7756
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1565 0 0 0 19991 6 0 0 25 0 1 0 423387526 7942144 1504 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1504 603 41 0 1898 0
vsize: 7756
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1572 0 0 0 20992 6 0 0 25 0 1 0 423387526 7942144 1511 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1511 603 41 0 1898 0
vsize: 7756
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1572 0 0 0 21992 6 0 0 25 0 1 0 423387526 7942144 1511 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1511 603 41 0 1898 0
vsize: 7756
[startup+230.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1579 0 0 0 22992 6 0 0 25 0 1 0 423387526 8105984 1518 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1979 1518 603 41 0 1938 0
vsize: 7916
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1599 0 0 0 23992 6 0 0 25 0 1 0 423387526 8105984 1538 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1979 1538 603 41 0 1938 0
vsize: 7916
[startup+250.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1636 0 0 0 24992 6 0 0 25 0 1 0 423387526 8364032 1575 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2042 1575 603 41 0 2001 0
vsize: 8168
[startup+260.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1642 0 0 0 25993 6 0 0 25 0 1 0 423387526 8364032 1581 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2042 1581 603 41 0 2001 0
vsize: 8168
[startup+270.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1650 0 0 0 26993 6 0 0 25 0 1 0 423387526 8503296 1589 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1589 603 41 0 2035 0
vsize: 8304
[startup+280.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1651 0 0 0 27993 6 0 0 25 0 1 0 423387526 8503296 1590 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1590 603 41 0 2035 0
vsize: 8304
[startup+290.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1657 0 0 0 28993 6 0 0 25 0 1 0 423387526 8503296 1596 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1596 603 41 0 2035 0
vsize: 8304
[startup+300.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1657 0 0 0 29993 6 0 0 25 0 1 0 423387526 8503296 1596 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1596 603 41 0 2035 0
vsize: 8304
[startup+310.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1662 0 0 0 30993 6 0 0 25 0 1 0 423387526 8503296 1601 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1601 603 41 0 2035 0
vsize: 8304
[startup+320.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1669 0 0 0 31994 6 0 0 25 0 1 0 423387526 8503296 1608 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1608 603 41 0 2035 0
vsize: 8304
[startup+330.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1670 0 0 0 32994 6 0 0 25 0 1 0 423387526 8503296 1609 4294967295 134512640 134672761 3221224560 3221223744 134558360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1609 603 41 0 2035 0
vsize: 8304
[startup+340.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1673 0 0 0 33994 6 0 0 25 0 1 0 423387526 8503296 1612 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1612 603 41 0 2035 0
vsize: 8304
[startup+350.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1673 0 0 0 34994 6 0 0 25 0 1 0 423387526 8503296 1612 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1612 603 41 0 2035 0
vsize: 8304
[startup+360.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1674 0 0 0 35994 6 0 0 25 0 1 0 423387526 8503296 1613 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1613 603 41 0 2035 0
vsize: 8304
[startup+370.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1674 0 0 0 36993 6 0 0 25 0 1 0 423387526 8503296 1613 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1613 603 41 0 2035 0
vsize: 8304
[startup+380.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1690 0 0 0 37993 6 0 0 25 0 1 0 423387526 8638464 1629 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1629 603 41 0 2068 0
vsize: 8436
[startup+390.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1690 0 0 0 38993 6 0 0 25 0 1 0 423387526 8638464 1629 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1629 603 41 0 2068 0
vsize: 8436
[startup+400.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1694 0 0 0 39993 6 0 0 25 0 1 0 423387526 8638464 1633 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1633 603 41 0 2068 0
vsize: 8436
[startup+410.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1694 0 0 0 40993 6 0 0 25 0 1 0 423387526 8638464 1633 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1633 603 41 0 2068 0
vsize: 8436
[startup+420.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1694 0 0 0 41994 6 0 0 25 0 1 0 423387526 8638464 1633 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1633 603 41 0 2068 0
vsize: 8436
[startup+430.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1695 0 0 0 42994 6 0 0 25 0 1 0 423387526 8638464 1634 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+440.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1695 0 0 0 43994 6 0 0 25 0 1 0 423387526 8638464 1634 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+450.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1695 0 0 0 44994 6 0 0 25 0 1 0 423387526 8638464 1634 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+460.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1695 0 0 0 45994 6 0 0 25 0 1 0 423387526 8638464 1634 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+470.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1695 0 0 0 46995 6 0 0 25 0 1 0 423387526 8638464 1634 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+480.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1697 0 0 0 47995 6 0 0 25 0 1 0 423387526 8638464 1636 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1636 603 41 0 2068 0
vsize: 8436
[startup+490.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1697 0 0 0 48995 6 0 0 25 0 1 0 423387526 8638464 1636 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1636 603 41 0 2068 0
vsize: 8436
[startup+500.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1701 0 0 0 49995 6 0 0 25 0 1 0 423387526 8638464 1640 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+510.01 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1701 0 0 0 50995 6 0 0 25 0 1 0 423387526 8638464 1640 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+520.01 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1701 0 0 0 51995 6 0 0 25 0 1 0 423387526 8638464 1640 4294967295 134512640 134672761 3221224560 3221223744 134558374 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+530.01 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1702 0 0 0 52996 6 0 0 25 0 1 0 423387526 8638464 1641 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1641 603 41 0 2068 0
vsize: 8436
[startup+540.01 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1702 0 0 0 53996 6 0 0 25 0 1 0 423387526 8638464 1641 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1641 603 41 0 2068 0
vsize: 8436
[startup+550.01 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1706 0 0 0 54996 6 0 0 25 0 1 0 423387526 8638464 1645 4294967295 134512640 134672761 3221224560 3221223728 134561701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1645 603 41 0 2068 0
vsize: 8436
[startup+560.01 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1709 0 0 0 55996 6 0 0 25 0 1 0 423387526 8638464 1648 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1648 603 41 0 2068 0
vsize: 8436
[startup+570.011 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1740 0 0 0 56996 6 0 0 25 0 1 0 423387526 8785920 1679 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2145 1679 603 41 0 2104 0
vsize: 8580
[startup+580.01 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1761 0 0 0 57996 6 0 0 25 0 1 0 423387526 8921088 1700 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1700 603 41 0 2137 0
vsize: 8712
[startup+590.01 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1761 0 0 0 58996 6 0 0 25 0 1 0 423387526 8921088 1700 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1700 603 41 0 2137 0
vsize: 8712
[startup+600.01 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1770 0 0 0 59996 6 0 0 25 0 1 0 423387526 8921088 1709 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1709 603 41 0 2137 0
vsize: 8712
[startup+610.011 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1771 0 0 0 60997 6 0 0 25 0 1 0 423387526 8921088 1710 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1710 603 41 0 2137 0
vsize: 8712
[startup+620.011 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1783 0 0 0 61997 6 0 0 25 0 1 0 423387526 8921088 1722 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1722 603 41 0 2137 0
vsize: 8712
[startup+630.011 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1792 0 0 0 62997 6 0 0 25 0 1 0 423387526 9105408 1731 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1731 603 41 0 2182 0
vsize: 8892
[startup+640.011 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1792 0 0 0 63997 6 0 0 25 0 1 0 423387526 9105408 1731 4294967295 134512640 134672761 3221224560 3221223696 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1731 603 41 0 2182 0
vsize: 8892
[startup+650.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1792 0 0 0 64997 6 0 0 25 0 1 0 423387526 9105408 1731 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1731 603 41 0 2182 0
vsize: 8892
[startup+660.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1793 0 0 0 65998 6 0 0 25 0 1 0 423387526 9105408 1732 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1732 603 41 0 2182 0
vsize: 8892
[startup+670.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1794 0 0 0 66998 6 0 0 25 0 1 0 423387526 9105408 1733 4294967295 134512640 134672761 3221224560 3221223728 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1733 603 41 0 2182 0
vsize: 8892
[startup+680.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1795 0 0 0 67998 6 0 0 25 0 1 0 423387526 9105408 1734 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1734 603 41 0 2182 0
vsize: 8892
[startup+690.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1796 0 0 0 68998 6 0 0 25 0 1 0 423387526 9105408 1735 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1735 603 41 0 2182 0
vsize: 8892
[startup+700.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1796 0 0 0 69998 6 0 0 25 0 1 0 423387526 9105408 1735 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1735 603 41 0 2182 0
vsize: 8892
[startup+710.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1798 0 0 0 70998 6 0 0 25 0 1 0 423387526 9105408 1737 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1737 603 41 0 2182 0
vsize: 8892
[startup+720.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1808 0 0 0 71999 6 0 0 25 0 1 0 423387526 9105408 1747 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+730.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1808 0 0 0 72999 6 0 0 25 0 1 0 423387526 9105408 1747 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+740.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1808 0 0 0 73998 6 0 0 25 0 1 0 423387526 9105408 1747 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+750.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1808 0 0 0 74998 6 0 0 25 0 1 0 423387526 9105408 1747 4294967295 134512640 134672761 3221224560 3221223684 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+760.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1814 0 0 0 75999 6 0 0 25 0 1 0 423387526 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+770.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1814 0 0 0 76999 6 0 0 25 0 1 0 423387526 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+780.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1814 0 0 0 77999 6 0 0 25 0 1 0 423387526 9105408 1753 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+790.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1814 0 0 0 78999 6 0 0 25 0 1 0 423387526 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+800.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1814 0 0 0 79999 6 0 0 25 0 1 0 423387526 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+810.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1814 0 0 0 80999 6 0 0 25 0 1 0 423387526 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+820.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1814 0 0 0 82000 6 0 0 25 0 1 0 423387526 9105408 1753 4294967295 134512640 134672761 3221224560 3221223664 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+830.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1814 0 0 0 83000 6 0 0 25 0 1 0 423387526 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+840.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1823 0 0 0 84000 6 0 0 25 0 1 0 423387526 9269248 1762 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1762 603 41 0 2222 0
vsize: 9052
[startup+850.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1824 0 0 0 85000 6 0 0 25 0 1 0 423387526 9269248 1763 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1763 603 41 0 2222 0
vsize: 9052
[startup+860.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1825 0 0 0 86000 6 0 0 25 0 1 0 423387526 9269248 1764 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+870.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1825 0 0 0 87000 6 0 0 25 0 1 0 423387526 9269248 1764 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+880.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1825 0 0 0 88000 7 0 0 25 0 1 0 423387526 9269248 1764 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+890.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1851 0 0 0 88999 7 0 0 25 0 1 0 423387526 9269248 1790 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1790 603 41 0 2222 0
vsize: 9052
[startup+900.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1858 0 0 0 89999 7 0 0 25 0 1 0 423387526 9404416 1797 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1797 603 41 0 2255 0
vsize: 9184
[startup+910.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1869 0 0 0 91000 7 0 0 25 0 1 0 423387526 9404416 1808 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1808 603 41 0 2255 0
vsize: 9184
[startup+920.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1873 0 0 0 92000 7 0 0 25 0 1 0 423387526 9404416 1812 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1812 603 41 0 2255 0
vsize: 9184
[startup+930.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1874 0 0 0 93000 7 0 0 25 0 1 0 423387526 9404416 1813 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1813 603 41 0 2255 0
vsize: 9184
[startup+940.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1874 0 0 0 94000 7 0 0 25 0 1 0 423387526 9404416 1813 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1813 603 41 0 2255 0
vsize: 9184
[startup+950.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1874 0 0 0 95000 7 0 0 25 0 1 0 423387526 9404416 1813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1813 603 41 0 2255 0
vsize: 9184
[startup+960.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1883 0 0 0 96000 7 0 0 25 0 1 0 423387526 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+970.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1883 0 0 0 97001 7 0 0 25 0 1 0 423387526 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+980.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1883 0 0 0 98001 7 0 0 25 0 1 0 423387526 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+990.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1883 0 0 0 99001 7 0 0 25 0 1 0 423387526 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1883 0 0 0 100001 7 0 0 25 0 1 0 423387526 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1883 0 0 0 101001 7 0 0 25 0 1 0 423387526 9404416 1822 4294967295 134512640 134672761 3221224560 3221223696 134565039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1883 0 0 0 102001 7 0 0 25 0 1 0 423387526 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1883 0 0 0 103002 7 0 0 25 0 1 0 423387526 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1883 0 0 0 104002 7 0 0 25 0 1 0 423387526 9404416 1822 4294967295 134512640 134672761 3221224560 3221223696 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1889 0 0 0 105002 7 0 0 25 0 1 0 423387526 9543680 1828 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1828 603 41 0 2289 0
vsize: 9320
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1899 0 0 0 106002 7 0 0 25 0 1 0 423387526 9543680 1838 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1838 603 41 0 2289 0
vsize: 9320
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1899 0 0 0 107002 7 0 0 25 0 1 0 423387526 9543680 1838 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1838 603 41 0 2289 0
vsize: 9320
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1900 0 0 0 108003 7 0 0 25 0 1 0 423387526 9543680 1839 4294967295 134512640 134672761 3221224560 3221223744 134558673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1839 603 41 0 2289 0
vsize: 9320
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1900 0 0 0 109003 7 0 0 25 0 1 0 423387526 9543680 1839 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1839 603 41 0 2289 0
vsize: 9320
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1900 0 0 0 110003 7 0 0 25 0 1 0 423387526 9543680 1839 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1839 603 41 0 2289 0
vsize: 9320
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1910 0 0 0 111003 7 0 0 25 0 1 0 423387526 9543680 1849 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1849 603 41 0 2289 0
vsize: 9320
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1911 0 0 0 112003 7 0 0 25 0 1 0 423387526 9543680 1850 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1911 0 0 0 113004 7 0 0 25 0 1 0 423387526 9543680 1850 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1911 0 0 0 114004 7 0 0 25 0 1 0 423387526 9543680 1850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1911 0 0 0 115004 7 0 0 25 0 1 0 423387526 9543680 1850 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1913 0 0 0 116004 7 0 0 25 0 1 0 423387526 9682944 1852 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1852 603 41 0 2323 0
vsize: 9456
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1913 0 0 0 117004 7 0 0 25 0 1 0 423387526 9682944 1852 4294967295 134512640 134672761 3221224560 3221223696 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1852 603 41 0 2323 0
vsize: 9456
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1922 0 0 0 118004 7 0 0 25 0 1 0 423387526 9682944 1861 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1861 603 41 0 2323 0
vsize: 9456
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1922 0 0 0 119005 7 0 0 25 0 1 0 423387526 9682944 1861 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1861 603 41 0 2323 0
vsize: 9456
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 7169
Raw data (stat): 7169 (minisat+) R 7168 32461 32460 0 -1 0 1932 0 0 0 120005 7 0 0 25 0 1 0 423387526 9682944 1871 4294967295 134512640 134672761 3221224560 3221223664 134559953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1871 603 41 0 2323 0
vsize: 9456
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 7169
Raw data (stat): 7169 (minisat+) Z 7168 32461 32460 0 -1 12 1934 0 0 0 120005 8 0 0 25 0 1 0 423387526 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.02
CPU time (s): 1200.13
CPU user time (s): 1200.05
CPU system time (s): 0.081987
CPU usage (%): 100.009
Max. virtual memory (Kb): 9456
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####