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-3.opb
MD5SUM	3d08363a486acbc90a149ca8c58297b8
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	13473
Number of constraints which are clauses	13473
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 5149

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        901956 kB
Buffers:         33492 kB
Cached:          64664 kB
SwapCached:         36 kB
Active:          46056 kB
Inactive:        54972 kB
HighTotal:      131008 kB
HighFree:        62664 kB
LowTotal:       903652 kB
LowFree:        839292 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26204 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:35:08 (client local time) WITH STATUS 0 IN 1200.13 SECONDS
stats: 3592 7 1200.13 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13063 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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 |    9829    24580 |    3276       0        0     nan |  0.000 % |
c |       101 |    9829    24580 |    3603     101     1984    19.6 | 24.591 % |
c |       251 |    9829    24580 |    3963     251     3855    15.4 | 24.591 % |
c |       477 |    9829    24580 |    4360     477    11273    23.6 | 24.591 % |
c |       814 |    9829    24580 |    4796     814    15937    19.6 | 24.591 % |
c |      1321 |    9829    24580 |    5276    1321    31940    24.2 | 24.591 % |
c |      2081 |    9819    24558 |    5803    2080    47902    23.0 | 24.654 % |
c |      3220 |    9819    24558 |    6383    3219    76879    23.9 | 24.654 % |
c |      4930 |    9819    24558 |    7022    4929   124463    25.3 | 24.654 % |
c |      7492 |    9819    24558 |    7724    7491   193897    25.9 | 24.654 % |
c |     11336 |    9819    24558 |    8497    6666   165567    24.8 | 24.654 % |
c |     17102 |    9819    24558 |    9346    7321   192064    26.2 | 24.654 % |
c |     25751 |    9819    24558 |   10281   10435   254160    24.4 | 24.654 % |
c |     38726 |    9819    24558 |   11309   11433   268668    23.5 | 24.654 % |
c |     58187 |    9819    24558 |   12440   11477   264672    23.1 | 24.654 % |
c |     87379 |    9819    24558 |   13684   12371   274649    22.2 | 24.654 % |
c |    131169 |    9819    24558 |   15053   10129   219378    21.7 | 24.654 % |
c |    196853 |    9819    24558 |   16558    8870   182958    20.6 | 24.654 % |
c |    295381 |    9819    24558 |   18214   16209   376666    23.2 | 24.654 % |
c |    443170 |    9819    24558 |   20035   14819   321798    21.7 | 24.654 % |
#### 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.92 2/54 30739
Raw data (stat): 30739 (runsolver) R 30738 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479481800 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1253 0 0 0 993 5 0 0 25 0 1 0 479481800 6541312 1192 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.0018 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1253 0 0 0 1993 5 0 0 25 0 1 0 479481800 6541312 1192 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1597 1192 603 41 0 1556 0
vsize: 6388
[startup+30.0024 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1254 0 0 0 2992 5 0 0 25 0 1 0 479481800 6545408 1193 4294967295 134512640 134672761 3221224560 3221223684 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1598 1193 603 41 0 1557 0
vsize: 6392
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1278 0 0 0 3991 6 0 0 25 0 1 0 479481800 6680576 1217 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1631 1217 603 41 0 1590 0
vsize: 6524
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1299 0 0 0 4991 6 0 0 25 0 1 0 479481800 6815744 1238 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1664 1238 603 41 0 1623 0
vsize: 6656
[startup+60.0029 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1304 0 0 0 5991 6 0 0 25 0 1 0 479481800 6815744 1243 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1664 1243 603 41 0 1623 0
vsize: 6656
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1317 0 0 0 6991 6 0 0 25 0 1 0 479481800 6950912 1256 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1697 1256 603 41 0 1656 0
vsize: 6788
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1334 0 0 0 7991 6 0 0 25 0 1 0 479481800 6950912 1273 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1697 1273 603 41 0 1656 0
vsize: 6788
[startup+90.0028 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1339 0 0 0 8991 6 0 0 25 0 1 0 479481800 6950912 1278 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1697 1278 603 41 0 1656 0
vsize: 6788
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1348 0 0 0 9992 6 0 0 25 0 1 0 479481800 7090176 1287 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1731 1287 603 41 0 1690 0
vsize: 6924
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1387 0 0 0 10992 6 0 0 25 0 1 0 479481800 7225344 1326 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1326 603 41 0 1723 0
vsize: 7056
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1399 0 0 0 11992 6 0 0 25 0 1 0 479481800 7225344 1338 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1338 603 41 0 1723 0
vsize: 7056
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1413 0 0 0 12992 6 0 0 25 0 1 0 479481800 7368704 1352 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1352 603 41 0 1758 0
vsize: 7196
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1414 0 0 0 13992 6 0 0 25 0 1 0 479481800 7368704 1353 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1353 603 41 0 1758 0
vsize: 7196
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1424 0 0 0 14992 7 0 0 25 0 1 0 479481800 7368704 1363 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1363 603 41 0 1758 0
vsize: 7196
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1425 0 0 0 15992 7 0 0 25 0 1 0 479481800 7368704 1364 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1364 603 41 0 1758 0
vsize: 7196
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1446 0 0 0 16992 7 0 0 25 0 1 0 479481800 7499776 1385 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1831 1385 603 41 0 1790 0
vsize: 7324
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1448 0 0 0 17990 7 0 0 25 0 1 0 479481800 7499776 1387 4294967295 134512640 134672761 3221224560 3221223664 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1831 1387 603 41 0 1790 0
vsize: 7324
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1456 0 0 0 18989 8 0 0 25 0 1 0 479481800 7499776 1395 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1831 1395 603 41 0 1790 0
vsize: 7324
[startup+200.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1461 0 0 0 19989 8 0 0 25 0 1 0 479481800 7499776 1400 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1831 1400 603 41 0 1790 0
vsize: 7324
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1461 0 0 0 20989 8 0 0 25 0 1 0 479481800 7499776 1400 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1831 1400 603 41 0 1790 0
vsize: 7324
[startup+220.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1470 0 0 0 21989 8 0 0 25 0 1 0 479481800 7634944 1409 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1409 603 41 0 1823 0
vsize: 7456
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1471 0 0 0 22989 8 0 0 25 0 1 0 479481800 7634944 1410 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1410 603 41 0 1823 0
vsize: 7456
[startup+240.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1473 0 0 0 23989 8 0 0 25 0 1 0 479481800 7634944 1412 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1412 603 41 0 1823 0
vsize: 7456
[startup+250.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1474 0 0 0 24990 8 0 0 25 0 1 0 479481800 7634944 1413 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1413 603 41 0 1823 0
vsize: 7456
[startup+260.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1478 0 0 0 25990 8 0 0 25 0 1 0 479481800 7634944 1417 4294967295 134512640 134672761 3221224560 3221223696 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1417 603 41 0 1823 0
vsize: 7456
[startup+270.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1529 0 0 0 26989 9 0 0 25 0 1 0 479481800 7942144 1468 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1468 603 41 0 1898 0
vsize: 7756
[startup+280.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1541 0 0 0 27990 9 0 0 25 0 1 0 479481800 7942144 1480 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1480 603 41 0 1898 0
vsize: 7756
[startup+290.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1542 0 0 0 28990 9 0 0 25 0 1 0 479481800 7942144 1481 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+300.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1542 0 0 0 29990 9 0 0 25 0 1 0 479481800 7942144 1481 4294967295 134512640 134672761 3221224560 3221223744 134559159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+310.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1542 0 0 0 30990 9 0 0 25 0 1 0 479481800 7942144 1481 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+320.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1548 0 0 0 31990 9 0 0 25 0 1 0 479481800 7942144 1487 4294967295 134512640 134672761 3221224560 3221223776 134558229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1487 603 41 0 1898 0
vsize: 7756
[startup+330.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1548 0 0 0 32990 9 0 0 25 0 1 0 479481800 7942144 1487 4294967295 134512640 134672761 3221224560 3221223744 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1487 603 41 0 1898 0
vsize: 7756
[startup+340.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1548 0 0 0 33990 9 0 0 25 0 1 0 479481800 7942144 1487 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1487 603 41 0 1898 0
vsize: 7756
[startup+350.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1551 0 0 0 34990 9 0 0 25 0 1 0 479481800 8089600 1490 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1490 603 41 0 1934 0
vsize: 7900
[startup+360.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1551 0 0 0 35991 9 0 0 25 0 1 0 479481800 8089600 1490 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1490 603 41 0 1934 0
vsize: 7900
[startup+370.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1552 0 0 0 36991 9 0 0 25 0 1 0 479481800 8089600 1491 4294967295 134512640 134672761 3221224560 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1491 603 41 0 1934 0
vsize: 7900
[startup+380.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1552 0 0 0 37991 9 0 0 25 0 1 0 479481800 8089600 1491 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1491 603 41 0 1934 0
vsize: 7900
[startup+390.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1554 0 0 0 38991 9 0 0 25 0 1 0 479481800 8089600 1493 4294967295 134512640 134672761 3221224560 3221223760 134557915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1975 1493 603 41 0 1934 0
vsize: 7900
[startup+400.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1554 0 0 0 39991 9 0 0 25 0 1 0 479481800 8089600 1493 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1493 603 41 0 1934 0
vsize: 7900
[startup+410.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1588 0 0 0 40991 10 0 0 25 0 1 0 479481800 8224768 1527 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1527 603 41 0 1967 0
vsize: 8032
[startup+420.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1591 0 0 0 41991 10 0 0 25 0 1 0 479481800 8224768 1530 4294967295 134512640 134672761 3221224560 3221223664 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1530 603 41 0 1967 0
vsize: 8032
[startup+430.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1603 0 0 0 42991 10 0 0 25 0 1 0 479481800 8224768 1542 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1542 603 41 0 1967 0
vsize: 8032
[startup+440.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1604 0 0 0 43990 10 0 0 25 0 1 0 479481800 8224768 1543 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1543 603 41 0 1967 0
vsize: 8032
[startup+450.008 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1605 0 0 0 44991 10 0 0 25 0 1 0 479481800 8224768 1544 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1544 603 41 0 1967 0
vsize: 8032
[startup+460.008 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1605 0 0 0 45991 10 0 0 25 0 1 0 479481800 8224768 1544 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1544 603 41 0 1967 0
vsize: 8032
[startup+470.008 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1607 0 0 0 46991 10 0 0 25 0 1 0 479481800 8224768 1546 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1546 603 41 0 1967 0
vsize: 8032
[startup+480.008 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1607 0 0 0 47991 10 0 0 25 0 1 0 479481800 8224768 1546 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1546 603 41 0 1967 0
vsize: 8032
[startup+490.008 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1611 0 0 0 48991 10 0 0 25 0 1 0 479481800 8224768 1550 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+500.008 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1611 0 0 0 49991 10 0 0 25 0 1 0 479481800 8224768 1550 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+510.009 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1611 0 0 0 50990 11 0 0 25 0 1 0 479481800 8224768 1550 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+520.009 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1611 0 0 0 51990 11 0 0 25 0 1 0 479481800 8224768 1550 4294967295 134512640 134672761 3221224560 3221223664 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+530.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1612 0 0 0 52990 11 0 0 25 0 1 0 479481800 8224768 1551 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1551 603 41 0 1967 0
vsize: 8032
[startup+540.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1612 0 0 0 53990 11 0 0 25 0 1 0 479481800 8224768 1551 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1551 603 41 0 1967 0
vsize: 8032
[startup+550.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1612 0 0 0 54990 11 0 0 25 0 1 0 479481800 8224768 1551 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1551 603 41 0 1967 0
vsize: 8032
[startup+560.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1614 0 0 0 55991 11 0 0 25 0 1 0 479481800 8224768 1553 4294967295 134512640 134672761 3221224560 3221223696 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+570.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1614 0 0 0 56991 11 0 0 25 0 1 0 479481800 8224768 1553 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+580.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1614 0 0 0 57991 11 0 0 25 0 1 0 479481800 8224768 1553 4294967295 134512640 134672761 3221224560 3221223716 134565028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+590.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1614 0 0 0 58991 11 0 0 25 0 1 0 479481800 8224768 1553 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+600.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1615 0 0 0 59991 11 0 0 25 0 1 0 479481800 8224768 1554 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1554 603 41 0 1967 0
vsize: 8032
[startup+610.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1694 0 0 0 60990 12 0 0 25 0 1 0 479481800 8491008 1633 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1633 603 41 0 2032 0
vsize: 8292
[startup+620.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1694 0 0 0 61990 12 0 0 25 0 1 0 479481800 8491008 1633 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1633 603 41 0 2032 0
vsize: 8292
[startup+630.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1695 0 0 0 62990 12 0 0 25 0 1 0 479481800 8491008 1634 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1634 603 41 0 2032 0
vsize: 8292
[startup+640.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1700 0 0 0 63990 12 0 0 25 0 1 0 479481800 8638464 1639 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1639 603 41 0 2068 0
vsize: 8436
[startup+650.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1701 0 0 0 64990 12 0 0 25 0 1 0 479481800 8638464 1640 4294967295 134512640 134672761 3221224560 3221223664 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+660.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1705 0 0 0 65990 12 0 0 25 0 1 0 479481800 8638464 1644 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1644 603 41 0 2068 0
vsize: 8436
[startup+670.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1715 0 0 0 66990 12 0 0 25 0 1 0 479481800 8638464 1654 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1654 603 41 0 2068 0
vsize: 8436
[startup+680.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1719 0 0 0 67990 12 0 0 25 0 1 0 479481800 8638464 1658 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1658 603 41 0 2068 0
vsize: 8436
[startup+690.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1720 0 0 0 68991 13 0 0 25 0 1 0 479481800 8638464 1659 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1659 603 41 0 2068 0
vsize: 8436
[startup+700.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1721 0 0 0 69990 13 0 0 25 0 1 0 479481800 8638464 1660 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1660 603 41 0 2068 0
vsize: 8436
[startup+710.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1722 0 0 0 70991 13 0 0 25 0 1 0 479481800 8638464 1661 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1661 603 41 0 2068 0
vsize: 8436
[startup+720.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1732 0 0 0 71991 13 0 0 25 0 1 0 479481800 8818688 1671 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1671 603 41 0 2112 0
vsize: 8612
[startup+730.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1732 0 0 0 72991 13 0 0 25 0 1 0 479481800 8818688 1671 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1671 603 41 0 2112 0
vsize: 8612
[startup+740.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1733 0 0 0 73991 13 0 0 25 0 1 0 479481800 8818688 1672 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1672 603 41 0 2112 0
vsize: 8612
[startup+750.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1733 0 0 0 74991 13 0 0 25 0 1 0 479481800 8818688 1672 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1672 603 41 0 2112 0
vsize: 8612
[startup+760.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1742 0 0 0 75991 13 0 0 25 0 1 0 479481800 8818688 1681 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1681 603 41 0 2112 0
vsize: 8612
[startup+770.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1742 0 0 0 76992 13 0 0 25 0 1 0 479481800 8818688 1681 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1681 603 41 0 2112 0
vsize: 8612
[startup+780.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1751 0 0 0 77992 13 0 0 25 0 1 0 479481800 8818688 1690 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1690 603 41 0 2112 0
vsize: 8612
[startup+790.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1751 0 0 0 78992 13 0 0 25 0 1 0 479481800 8818688 1690 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1690 603 41 0 2112 0
vsize: 8612
[startup+800.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1751 0 0 0 79992 13 0 0 25 0 1 0 479481800 8818688 1690 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1690 603 41 0 2112 0
vsize: 8612
[startup+810.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1761 0 0 0 80992 13 0 0 25 0 1 0 479481800 9015296 1700 4294967295 134512640 134672761 3221224560 3221223744 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1700 603 41 0 2160 0
vsize: 8804
[startup+820.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1761 0 0 0 81992 13 0 0 25 0 1 0 479481800 9015296 1700 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1700 603 41 0 2160 0
vsize: 8804
[startup+830.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1771 0 0 0 82992 13 0 0 25 0 1 0 479481800 9015296 1710 4294967295 134512640 134672761 3221224560 3221223744 134558563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+840.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1771 0 0 0 83992 13 0 0 25 0 1 0 479481800 9015296 1710 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+850.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1771 0 0 0 84993 13 0 0 25 0 1 0 479481800 9015296 1710 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+860.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1771 0 0 0 85993 13 0 0 25 0 1 0 479481800 9015296 1710 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+870.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1780 0 0 0 86993 13 0 0 25 0 1 0 479481800 9015296 1719 4294967295 134512640 134672761 3221224560 3221223744 134559550 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1719 603 41 0 2160 0
vsize: 8804
[startup+880.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1780 0 0 0 87993 13 0 0 25 0 1 0 479481800 9015296 1719 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1719 603 41 0 2160 0
vsize: 8804
[startup+890.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1781 0 0 0 88993 13 0 0 25 0 1 0 479481800 9015296 1720 4294967295 134512640 134672761 3221224560 3221223744 134558338 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+900.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1781 0 0 0 89993 14 0 0 25 0 1 0 479481800 9015296 1720 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+910.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1781 0 0 0 90994 14 0 0 25 0 1 0 479481800 9015296 1720 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+920.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1781 0 0 0 91994 14 0 0 25 0 1 0 479481800 9015296 1720 4294967295 134512640 134672761 3221224560 3221223696 134565066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+930.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1781 0 0 0 92992 14 0 0 25 0 1 0 479481800 9015296 1720 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+940.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1789 0 0 0 93993 14 0 0 25 0 1 0 479481800 9146368 1728 4294967295 134512640 134672761 3221224560 3221223664 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1728 603 41 0 2192 0
vsize: 8932
[startup+950.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1796 0 0 0 94993 14 0 0 25 0 1 0 479481800 9146368 1735 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1735 603 41 0 2192 0
vsize: 8932
[startup+960.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1808 0 0 0 95993 14 0 0 25 0 1 0 479481800 9146368 1747 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1747 603 41 0 2192 0
vsize: 8932
[startup+970.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1809 0 0 0 96993 14 0 0 25 0 1 0 479481800 9146368 1748 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1748 603 41 0 2192 0
vsize: 8932
[startup+980.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1809 0 0 0 97993 14 0 0 25 0 1 0 479481800 9146368 1748 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1748 603 41 0 2192 0
vsize: 8932
[startup+990.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1809 0 0 0 98993 14 0 0 25 0 1 0 479481800 9146368 1748 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1748 603 41 0 2192 0
vsize: 8932
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1817 0 0 0 99993 14 0 0 25 0 1 0 479481800 9306112 1756 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1756 603 41 0 2231 0
vsize: 9088
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1820 0 0 0 100993 14 0 0 25 0 1 0 479481800 9306112 1759 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1759 603 41 0 2231 0
vsize: 9088
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1820 0 0 0 101994 14 0 0 25 0 1 0 479481800 9306112 1759 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1759 603 41 0 2231 0
vsize: 9088
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1820 0 0 0 102994 14 0 0 25 0 1 0 479481800 9306112 1759 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1759 603 41 0 2231 0
vsize: 9088
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1829 0 0 0 103994 14 0 0 25 0 1 0 479481800 9306112 1768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1768 603 41 0 2231 0
vsize: 9088
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1829 0 0 0 104994 14 0 0 25 0 1 0 479481800 9306112 1768 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1768 603 41 0 2231 0
vsize: 9088
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1830 0 0 0 105994 15 0 0 25 0 1 0 479481800 9306112 1769 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1830 0 0 0 106994 15 0 0 25 0 1 0 479481800 9306112 1769 4294967295 134512640 134672761 3221224560 3221223696 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1830 0 0 0 107995 15 0 0 25 0 1 0 479481800 9306112 1769 4294967295 134512640 134672761 3221224560 3221223696 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1831 0 0 0 108995 15 0 0 25 0 1 0 479481800 9306112 1770 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1770 603 41 0 2231 0
vsize: 9088
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 109995 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 110995 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 111995 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 112995 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 113995 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223712 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 114995 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 115995 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 116996 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 117996 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 118996 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 28099 28098 0 -1 0 1842 0 0 0 119996 15 0 0 25 0 1 0 479481800 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 30739
Raw data (stat): 30739 (minisat+) Z 30738 28099 28098 0 -1 12 1844 0 0 0 119996 16 0 0 25 0 1 0 479481800 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): 1199.97
CPU system time (s): 0.162975
CPU usage (%): 100.009
Max. virtual memory (Kb): 9248
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####