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 6307

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        861908 kB
Buffers:         38120 kB
Cached:         114880 kB
SwapCached:          0 kB
Active:          73512 kB
Inactive:        82316 kB
HighTotal:      131008 kB
HighFree:        12320 kB
LowTotal:       903652 kB
LowFree:        849588 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11220 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:31:02 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 4720 7 1200.26 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.91 0.95 0.90 2/54 29068
Raw data (stat): 29068 (runsolver) R 29067 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423390842 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.0002 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1253 0 0 0 994 4 0 0 25 0 1 0 423390842 6541312 1192 4294967295 134512640 134672761 3221224576 3221223744 134560874 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.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1253 0 0 0 1994 4 0 0 25 0 1 0 423390842 6541312 1192 4294967295 134512640 134672761 3221224576 3221223760 134558338 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.1048 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1254 0 0 0 3004 5 0 0 25 0 1 0 423390842 6545408 1193 4294967295 134512640 134672761 3221224576 3221223712 134560673 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.105 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1278 0 0 0 4004 5 0 0 25 0 1 0 423390842 6680576 1217 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1631 1217 603 41 0 1590 0
vsize: 6524
[startup+50.1061 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1300 0 0 0 5003 6 0 0 25 0 1 0 423390842 6815744 1239 4294967295 134512640 134672761 3221224576 3221223744 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1664 1239 603 41 0 1623 0
vsize: 6656
[startup+60.1068 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1304 0 0 0 6003 6 0 0 25 0 1 0 423390842 6815744 1243 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1664 1243 603 41 0 1623 0
vsize: 6656
[startup+70.1069 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1334 0 0 0 7002 7 0 0 25 0 1 0 423390842 6950912 1273 4294967295 134512640 134672761 3221224576 3221223776 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1697 1273 603 41 0 1656 0
vsize: 6788
[startup+80.1083 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1334 0 0 0 8002 7 0 0 25 0 1 0 423390842 6950912 1273 4294967295 134512640 134672761 3221224576 3221223760 134559176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1697 1273 603 41 0 1656 0
vsize: 6788
[startup+90.1086 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1343 0 0 0 9001 7 0 0 25 0 1 0 423390842 6950912 1282 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1697 1282 603 41 0 1656 0
vsize: 6788
[startup+100.109 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1349 0 0 0 10001 8 0 0 25 0 1 0 423390842 7090176 1288 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1731 1288 603 41 0 1690 0
vsize: 6924
[startup+110.11 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1391 0 0 0 11000 8 0 0 25 0 1 0 423390842 7225344 1330 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1764 1330 603 41 0 1723 0
vsize: 7056
[startup+120.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1399 0 0 0 12000 9 0 0 25 0 1 0 423390842 7225344 1338 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1764 1338 603 41 0 1723 0
vsize: 7056
[startup+130.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1414 0 0 0 12999 9 0 0 25 0 1 0 423390842 7368704 1353 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1799 1353 603 41 0 1758 0
vsize: 7196
[startup+140.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1414 0 0 0 13999 9 0 0 25 0 1 0 423390842 7368704 1353 4294967295 134512640 134672761 3221224576 3221223760 134558537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1799 1353 603 41 0 1758 0
vsize: 7196
[startup+150.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1425 0 0 0 14999 9 0 0 25 0 1 0 423390842 7368704 1364 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1364 603 41 0 1758 0
vsize: 7196
[startup+160.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1432 0 0 0 15999 9 0 0 25 0 1 0 423390842 7368704 1371 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1371 603 41 0 1758 0
vsize: 7196
[startup+170.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1447 0 0 0 16999 9 0 0 25 0 1 0 423390842 7499776 1386 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1831 1386 603 41 0 1790 0
vsize: 7324
[startup+180.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1448 0 0 0 18000 9 0 0 25 0 1 0 423390842 7499776 1387 4294967295 134512640 134672761 3221224576 3221223744 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1831 1387 603 41 0 1790 0
vsize: 7324
[startup+190.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1456 0 0 0 19000 9 0 0 25 0 1 0 423390842 7499776 1395 4294967295 134512640 134672761 3221224576 3221223744 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1831 1395 603 41 0 1790 0
vsize: 7324
[startup+200.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1461 0 0 0 20000 9 0 0 25 0 1 0 423390842 7499776 1400 4294967295 134512640 134672761 3221224576 3221223744 134561167 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.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1470 0 0 0 21000 9 0 0 25 0 1 0 423390842 7634944 1409 4294967295 134512640 134672761 3221224576 3221223760 134559388 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1409 603 41 0 1823 0
vsize: 7456
[startup+220.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1470 0 0 0 22000 9 0 0 25 0 1 0 423390842 7634944 1409 4294967295 134512640 134672761 3221224576 3221223712 134565045 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.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1473 0 0 0 23001 9 0 0 25 0 1 0 423390842 7634944 1412 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1412 603 41 0 1823 0
vsize: 7456
[startup+240.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1473 0 0 0 24001 9 0 0 25 0 1 0 423390842 7634944 1412 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1478 0 0 0 25000 10 0 0 25 0 1 0 423390842 7634944 1417 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1864 1417 603 41 0 1823 0
vsize: 7456
[startup+260.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1522 0 0 0 26001 10 0 0 25 0 1 0 423390842 7942144 1461 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1461 603 41 0 1898 0
vsize: 7756
[startup+270.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1529 0 0 0 27000 10 0 0 25 0 1 0 423390842 7942144 1468 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1468 603 41 0 1898 0
vsize: 7756
[startup+280.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1542 0 0 0 27999 10 0 0 25 0 1 0 423390842 7942144 1481 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+290.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1542 0 0 0 28998 11 0 0 25 0 1 0 423390842 7942144 1481 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+300.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1542 0 0 0 29998 11 0 0 25 0 1 0 423390842 7942144 1481 4294967295 134512640 134672761 3221224576 3221223744 134561193 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.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1547 0 0 0 30998 11 0 0 25 0 1 0 423390842 7942144 1486 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1486 603 41 0 1898 0
vsize: 7756
[startup+320.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1548 0 0 0 31998 11 0 0 25 0 1 0 423390842 7942144 1487 4294967295 134512640 134672761 3221224576 3221223744 134561266 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.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1548 0 0 0 32999 11 0 0 25 0 1 0 423390842 7942144 1487 4294967295 134512640 134672761 3221224576 3221223744 134560869 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.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1551 0 0 0 33999 11 0 0 25 0 1 0 423390842 8089600 1490 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1490 603 41 0 1934 0
vsize: 7900
[startup+350.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1551 0 0 0 34999 11 0 0 25 0 1 0 423390842 8089600 1490 4294967295 134512640 134672761 3221224576 3221223744 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+360.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1552 0 0 0 35999 11 0 0 25 0 1 0 423390842 8089600 1491 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1491 603 41 0 1934 0
vsize: 7900
[startup+370.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1552 0 0 0 36999 11 0 0 25 0 1 0 423390842 8089600 1491 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1554 0 0 0 37999 11 0 0 25 0 1 0 423390842 8089600 1493 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1493 603 41 0 1934 0
vsize: 7900
[startup+390.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1554 0 0 0 38999 11 0 0 25 0 1 0 423390842 8089600 1493 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1554 0 0 0 39998 11 0 0 25 0 1 0 423390842 8089600 1493 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1588 0 0 0 40998 11 0 0 25 0 1 0 423390842 8224768 1527 4294967295 134512640 134672761 3221224576 3221223744 134560869 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.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1597 0 0 0 41998 11 0 0 25 0 1 0 423390842 8224768 1536 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1536 603 41 0 1967 0
vsize: 8032
[startup+430.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1604 0 0 0 42998 11 0 0 25 0 1 0 423390842 8224768 1543 4294967295 134512640 134672761 3221224576 3221223760 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1543 603 41 0 1967 0
vsize: 8032
[startup+440.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1605 0 0 0 43999 11 0 0 25 0 1 0 423390842 8224768 1544 4294967295 134512640 134672761 3221224576 3221223744 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+450.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1605 0 0 0 44999 11 0 0 25 0 1 0 423390842 8224768 1544 4294967295 134512640 134672761 3221224576 3221223712 134560677 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.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1607 0 0 0 45999 11 0 0 25 0 1 0 423390842 8224768 1546 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1546 603 41 0 1967 0
vsize: 8032
[startup+470.115 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1607 0 0 0 46999 11 0 0 25 0 1 0 423390842 8224768 1546 4294967295 134512640 134672761 3221224576 3221223744 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+480.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1611 0 0 0 47999 11 0 0 25 0 1 0 423390842 8224768 1550 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+490.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1611 0 0 0 48999 11 0 0 25 0 1 0 423390842 8224768 1550 4294967295 134512640 134672761 3221224576 3221223776 134557885 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.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1611 0 0 0 50000 11 0 0 25 0 1 0 423390842 8224768 1550 4294967295 134512640 134672761 3221224576 3221223744 134561193 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.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1611 0 0 0 51000 11 0 0 25 0 1 0 423390842 8224768 1550 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+520.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1612 0 0 0 52000 11 0 0 25 0 1 0 423390842 8224768 1551 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1551 603 41 0 1967 0
vsize: 8032
[startup+530.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1612 0 0 0 53000 11 0 0 25 0 1 0 423390842 8224768 1551 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1612 0 0 0 54000 11 0 0 25 0 1 0 423390842 8224768 1551 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1613 0 0 0 55001 11 0 0 25 0 1 0 423390842 8224768 1552 4294967295 134512640 134672761 3221224576 3221223680 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1552 603 41 0 1967 0
vsize: 8032
[startup+560.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1614 0 0 0 56001 11 0 0 25 0 1 0 423390842 8224768 1553 4294967295 134512640 134672761 3221224576 3221223776 134557809 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.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1614 0 0 0 57001 11 0 0 25 0 1 0 423390842 8224768 1553 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1614 0 0 0 58001 11 0 0 25 0 1 0 423390842 8224768 1553 4294967295 134512640 134672761 3221224576 3221223744 134560839 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.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1615 0 0 0 59001 11 0 0 25 0 1 0 423390842 8224768 1554 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2008 1554 603 41 0 1967 0
vsize: 8032
[startup+600.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1680 0 0 0 60001 12 0 0 25 0 1 0 423390842 8491008 1619 4294967295 134512640 134672761 3221224576 3221223712 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2073 1619 603 41 0 2032 0
vsize: 8292
[startup+610.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1694 0 0 0 61001 12 0 0 25 0 1 0 423390842 8491008 1633 4294967295 134512640 134672761 3221224576 3221223744 134560869 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.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1694 0 0 0 62001 12 0 0 25 0 1 0 423390842 8491008 1633 4294967295 134512640 134672761 3221224576 3221223740 134565024 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.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1699 0 0 0 63002 12 0 0 25 0 1 0 423390842 8638464 1638 4294967295 134512640 134672761 3221224576 3221223728 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1638 603 41 0 2068 0
vsize: 8436
[startup+640.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1701 0 0 0 64002 12 0 0 25 0 1 0 423390842 8638464 1640 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+650.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1701 0 0 0 65002 12 0 0 25 0 1 0 423390842 8638464 1640 4294967295 134512640 134672761 3221224576 3221223744 134560830 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.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1715 0 0 0 66002 12 0 0 25 0 1 0 423390842 8638464 1654 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1654 603 41 0 2068 0
vsize: 8436
[startup+670.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1719 0 0 0 67002 12 0 0 25 0 1 0 423390842 8638464 1658 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1658 603 41 0 2068 0
vsize: 8436
[startup+680.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1720 0 0 0 68002 12 0 0 25 0 1 0 423390842 8638464 1659 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1659 603 41 0 2068 0
vsize: 8436
[startup+690.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1721 0 0 0 69003 12 0 0 25 0 1 0 423390842 8638464 1660 4294967295 134512640 134672761 3221224576 3221223744 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1660 603 41 0 2068 0
vsize: 8436
[startup+700.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1722 0 0 0 70003 12 0 0 25 0 1 0 423390842 8638464 1661 4294967295 134512640 134672761 3221224576 3221223712 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1661 603 41 0 2068 0
vsize: 8436
[startup+710.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1732 0 0 0 71003 12 0 0 25 0 1 0 423390842 8818688 1671 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1671 603 41 0 2112 0
vsize: 8612
[startup+720.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1732 0 0 0 72003 12 0 0 25 0 1 0 423390842 8818688 1671 4294967295 134512640 134672761 3221224576 3221223744 134561218 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1733 0 0 0 73003 12 0 0 25 0 1 0 423390842 8818688 1672 4294967295 134512640 134672761 3221224576 3221223712 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2153 1672 603 41 0 2112 0
vsize: 8612
[startup+740.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1733 0 0 0 74003 12 0 0 25 0 1 0 423390842 8818688 1672 4294967295 134512640 134672761 3221224576 3221223744 134560876 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1733 0 0 0 75004 12 0 0 25 0 1 0 423390842 8818688 1672 4294967295 134512640 134672761 3221224576 3221223744 134560869 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1742 0 0 0 76004 12 0 0 25 0 1 0 423390842 8818688 1681 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1751 0 0 0 77004 12 0 0 25 0 1 0 423390842 8818688 1690 4294967295 134512640 134672761 3221224576 3221223744 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+780.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1751 0 0 0 78004 12 0 0 25 0 1 0 423390842 8818688 1690 4294967295 134512640 134672761 3221224576 3221223744 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+790.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1751 0 0 0 79004 12 0 0 25 0 1 0 423390842 8818688 1690 4294967295 134512640 134672761 3221224576 3221223728 134561040 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.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1761 0 0 0 80005 12 0 0 25 0 1 0 423390842 9015296 1700 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1700 603 41 0 2160 0
vsize: 8804
[startup+810.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1761 0 0 0 81005 12 0 0 25 0 1 0 423390842 9015296 1700 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1771 0 0 0 82005 12 0 0 25 0 1 0 423390842 9015296 1710 4294967295 134512640 134672761 3221224576 3221223744 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+830.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1771 0 0 0 83005 12 0 0 25 0 1 0 423390842 9015296 1710 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1771 0 0 0 84005 12 0 0 25 0 1 0 423390842 9015296 1710 4294967295 134512640 134672761 3221224576 3221223744 134560869 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1771 0 0 0 85006 12 0 0 25 0 1 0 423390842 9015296 1710 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1771 0 0 0 86006 12 0 0 25 0 1 0 423390842 9015296 1710 4294967295 134512640 134672761 3221224576 3221223736 134561029 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1780 0 0 0 87006 12 0 0 25 0 1 0 423390842 9015296 1719 4294967295 134512640 134672761 3221224576 3221223744 134560898 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1781 0 0 0 88006 12 0 0 25 0 1 0 423390842 9015296 1720 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+890.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1781 0 0 0 89006 12 0 0 25 0 1 0 423390842 9015296 1720 4294967295 134512640 134672761 3221224576 3221223760 134558656 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1781 0 0 0 90006 12 0 0 25 0 1 0 423390842 9015296 1720 4294967295 134512640 134672761 3221224576 3221223744 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1781 0 0 0 91007 12 0 0 25 0 1 0 423390842 9015296 1720 4294967295 134512640 134672761 3221224576 3221223760 134558553 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1781 0 0 0 92006 12 0 0 25 0 1 0 423390842 9015296 1720 4294967295 134512640 134672761 3221224576 3221223744 134560976 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1789 0 0 0 93006 12 0 0 25 0 1 0 423390842 9146368 1728 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1728 603 41 0 2192 0
vsize: 8932
[startup+940.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1796 0 0 0 94007 12 0 0 25 0 1 0 423390842 9146368 1735 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1735 603 41 0 2192 0
vsize: 8932
[startup+950.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1808 0 0 0 95007 12 0 0 25 0 1 0 423390842 9146368 1747 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2233 1747 603 41 0 2192 0
vsize: 8932
[startup+960.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1808 0 0 0 96007 12 0 0 25 0 1 0 423390842 9146368 1747 4294967295 134512640 134672761 3221224576 3221223744 134560842 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1809 0 0 0 97007 12 0 0 25 0 1 0 423390842 9146368 1748 4294967295 134512640 134672761 3221224576 3221223744 134560869 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1809 0 0 0 98007 12 0 0 25 0 1 0 423390842 9146368 1748 4294967295 134512640 134672761 3221224576 3221223744 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.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1817 0 0 0 99008 12 0 0 25 0 1 0 423390842 9306112 1756 4294967295 134512640 134672761 3221224576 3221223744 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+1000.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1820 0 0 0 100008 12 0 0 25 0 1 0 423390842 9306112 1759 4294967295 134512640 134672761 3221224576 3221223744 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+1010.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1820 0 0 0 101008 12 0 0 25 0 1 0 423390842 9306112 1759 4294967295 134512640 134672761 3221224576 3221223744 134561198 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1820 0 0 0 102008 12 0 0 25 0 1 0 423390842 9306112 1759 4294967295 134512640 134672761 3221224576 3221223712 134560683 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1829 0 0 0 103008 12 0 0 25 0 1 0 423390842 9306112 1768 4294967295 134512640 134672761 3221224576 3221223744 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+1040.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1829 0 0 0 104008 12 0 0 25 0 1 0 423390842 9306112 1768 4294967295 134512640 134672761 3221224576 3221223776 134557811 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.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1830 0 0 0 105009 12 0 0 25 0 1 0 423390842 9306112 1769 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1060.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1830 0 0 0 106009 12 0 0 25 0 1 0 423390842 9306112 1769 4294967295 134512640 134672761 3221224576 3221223744 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1830 0 0 0 107010 12 0 0 25 0 1 0 423390842 9306112 1769 4294967295 134512640 134672761 3221224576 3221223680 134554642 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1831 0 0 0 108010 12 0 0 25 0 1 0 423390842 9306112 1770 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1770 603 41 0 2231 0
vsize: 9088
[startup+1090.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 109010 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223760 134559548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1100.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 110010 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223744 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+1110.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 111011 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223744 134560869 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 112011 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223712 134560613 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 113011 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223744 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+1140.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 114011 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223680 134554677 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 115012 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223776 134557885 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 116012 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223744 134561229 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 117012 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223724 134560552 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 118012 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223744 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 119012 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223744 134560903 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29068
Raw data (stat): 29068 (minisat+) R 29067 22932 22931 0 -1 0 1842 0 0 0 120012 12 0 0 25 0 1 0 423390842 9469952 1781 4294967295 134512640 134672761 3221224576 3221223760 134558435 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.14 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29068
Raw data (stat): 29068 (minisat+) Z 29067 22932 22931 0 -1 12 1844 0 0 0 120012 13 0 0 25 0 1 0 423390842 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.14
CPU time (s): 1200.26
CPU user time (s): 1200.13
CPU system time (s): 0.132979
CPU usage (%): 100.01
Max. virtual memory (Kb): 9248
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####