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 5940

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-14 02:20:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4344 boxname=wulflinc3 idbench=208 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3d08363a486acbc90a149ca8c58297b8  /oldhome/oroussel/tmp/wulflinc3/normalized-par32-3.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc3/normalized-par32-3.opb /oldhome/oroussel/tmp/wulflinc3/normalized-par32-3.opb
IDLAUNCH: 4344
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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.190
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:        869600 kB
Buffers:         36184 kB
Cached:         105516 kB
SwapCached:       3276 kB
Active:          81036 kB
Inactive:        66804 kB
HighTotal:      131008 kB
HighFree:        21560 kB
LowTotal:       903652 kB
LowFree:        848040 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11576 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:40:31 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 4344 7 1200.18 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.97 0.91 2/54 18797
Raw data (stat): 18797 (runsolver) R 18796 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422719419 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1253 0 0 0 995 3 0 0 25 0 1 0 422719419 6541312 1192 4294967295 134512640 134672761 3221224560 3221223696 134565092 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.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1253 0 0 0 1995 3 0 0 25 0 1 0 422719419 6541312 1192 4294967295 134512640 134672761 3221224560 3221223744 134559340 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.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1254 0 0 0 2995 3 0 0 25 0 1 0 422719419 6545408 1193 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1598 1193 603 41 0 1557 0
vsize: 6392
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1278 0 0 0 3994 3 0 0 25 0 1 0 422719419 6680576 1217 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.0032 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1299 0 0 0 4995 3 0 0 25 0 1 0 422719419 6815744 1238 4294967295 134512640 134672761 3221224560 3221223696 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1664 1238 603 41 0 1623 0
vsize: 6656
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1304 0 0 0 5995 3 0 0 25 0 1 0 422719419 6815744 1243 4294967295 134512640 134672761 3221224560 3221223744 134558557 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.0029 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1323 0 0 0 6995 3 0 0 25 0 1 0 422719419 6950912 1262 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1697 1262 603 41 0 1656 0
vsize: 6788
[startup+80.0037 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1334 0 0 0 7995 3 0 0 25 0 1 0 422719419 6950912 1273 4294967295 134512640 134672761 3221224560 3221223724 134561235 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.0032 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1342 0 0 0 8995 3 0 0 25 0 1 0 422719419 6950912 1281 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1697 1281 603 41 0 1656 0
vsize: 6788
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1348 0 0 0 9995 3 0 0 25 0 1 0 422719419 7090176 1287 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1731 1287 603 41 0 1690 0
vsize: 6924
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1391 0 0 0 10995 3 0 0 25 0 1 0 422719419 7225344 1330 4294967295 134512640 134672761 3221224560 3221223760 134557895 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1399 0 0 0 11995 3 0 0 25 0 1 0 422719419 7225344 1338 4294967295 134512640 134672761 3221224560 3221223728 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1414 0 0 0 12996 3 0 0 25 0 1 0 422719419 7368704 1353 4294967295 134512640 134672761 3221224560 3221223696 134565083 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1414 0 0 0 13996 3 0 0 25 0 1 0 422719419 7368704 1353 4294967295 134512640 134672761 3221224560 3221223728 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+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1425 0 0 0 14996 3 0 0 25 0 1 0 422719419 7368704 1364 4294967295 134512640 134672761 3221224560 3221223616 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1799 1364 603 41 0 1758 0
vsize: 7196
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1425 0 0 0 15996 3 0 0 25 0 1 0 422719419 7368704 1364 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1799 1364 603 41 0 1758 0
vsize: 7196
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1446 0 0 0 16996 4 0 0 25 0 1 0 422719419 7499776 1385 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1448 0 0 0 17996 4 0 0 25 0 1 0 422719419 7499776 1387 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1456 0 0 0 18996 4 0 0 25 0 1 0 422719419 7499776 1395 4294967295 134512640 134672761 3221224560 3221223712 134561249 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1461 0 0 0 19997 4 0 0 25 0 1 0 422719419 7499776 1400 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1831 1400 603 41 0 1790 0
vsize: 7324
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1470 0 0 0 20997 4 0 0 25 0 1 0 422719419 7634944 1409 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1864 1409 603 41 0 1823 0
vsize: 7456
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1470 0 0 0 21997 4 0 0 25 0 1 0 422719419 7634944 1409 4294967295 134512640 134672761 3221224560 3221223744 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1864 1409 603 41 0 1823 0
vsize: 7456
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1473 0 0 0 22997 4 0 0 25 0 1 0 422719419 7634944 1412 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1864 1412 603 41 0 1823 0
vsize: 7456
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1473 0 0 0 23997 4 0 0 25 0 1 0 422719419 7634944 1412 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1864 1412 603 41 0 1823 0
vsize: 7456
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1477 0 0 0 24997 4 0 0 25 0 1 0 422719419 7634944 1416 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1864 1416 603 41 0 1823 0
vsize: 7456
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1489 0 0 0 25997 4 0 0 25 0 1 0 422719419 7634944 1428 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1864 1428 603 41 0 1823 0
vsize: 7456
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1529 0 0 0 26997 4 0 0 25 0 1 0 422719419 7942144 1468 4294967295 134512640 134672761 3221224560 3221223696 134565073 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1542 0 0 0 27998 4 0 0 25 0 1 0 422719419 7942144 1481 4294967295 134512640 134672761 3221224560 3221223728 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1542 0 0 0 28998 4 0 0 25 0 1 0 422719419 7942144 1481 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1542 0 0 0 29998 4 0 0 25 0 1 0 422719419 7942144 1481 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1542 0 0 0 30998 4 0 0 25 0 1 0 422719419 7942144 1481 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1481 603 41 0 1898 0
vsize: 7756
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1548 0 0 0 31998 4 0 0 25 0 1 0 422719419 7942144 1487 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1487 603 41 0 1898 0
vsize: 7756
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1548 0 0 0 32998 4 0 0 25 0 1 0 422719419 7942144 1487 4294967295 134512640 134672761 3221224560 3221223696 134560637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1487 603 41 0 1898 0
vsize: 7756
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1551 0 0 0 33999 4 0 0 25 0 1 0 422719419 8089600 1490 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1975 1490 603 41 0 1934 0
vsize: 7900
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1551 0 0 0 34999 4 0 0 25 0 1 0 422719419 8089600 1490 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1975 1490 603 41 0 1934 0
vsize: 7900
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1552 0 0 0 35999 4 0 0 25 0 1 0 422719419 8089600 1491 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1975 1491 603 41 0 1934 0
vsize: 7900
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1552 0 0 0 36999 4 0 0 25 0 1 0 422719419 8089600 1491 4294967295 134512640 134672761 3221224560 3221223664 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1975 1491 603 41 0 1934 0
vsize: 7900
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1554 0 0 0 38000 4 0 0 25 0 1 0 422719419 8089600 1493 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1975 1493 603 41 0 1934 0
vsize: 7900
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1554 0 0 0 38999 4 0 0 25 0 1 0 422719419 8089600 1493 4294967295 134512640 134672761 3221224560 3221223728 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1554 0 0 0 39999 4 0 0 25 0 1 0 422719419 8089600 1493 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1975 1493 603 41 0 1934 0
vsize: 7900
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1588 0 0 0 40999 4 0 0 25 0 1 0 422719419 8224768 1527 4294967295 134512640 134672761 3221224560 3221223744 134558563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1527 603 41 0 1967 0
vsize: 8032
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1597 0 0 0 41999 4 0 0 25 0 1 0 422719419 8224768 1536 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1536 603 41 0 1967 0
vsize: 8032
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1603 0 0 0 43000 4 0 0 25 0 1 0 422719419 8224768 1542 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1542 603 41 0 1967 0
vsize: 8032
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1605 0 0 0 44000 4 0 0 25 0 1 0 422719419 8224768 1544 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1544 603 41 0 1967 0
vsize: 8032
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1605 0 0 0 45000 4 0 0 25 0 1 0 422719419 8224768 1544 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1544 603 41 0 1967 0
vsize: 8032
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1607 0 0 0 46000 4 0 0 25 0 1 0 422719419 8224768 1546 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1546 603 41 0 1967 0
vsize: 8032
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1607 0 0 0 47000 4 0 0 25 0 1 0 422719419 8224768 1546 4294967295 134512640 134672761 3221224560 3221223744 134558504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1546 603 41 0 1967 0
vsize: 8032
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1611 0 0 0 48001 4 0 0 25 0 1 0 422719419 8224768 1550 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1611 0 0 0 49001 4 0 0 25 0 1 0 422719419 8224768 1550 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1550 603 41 0 1967 0
vsize: 8032
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1611 0 0 0 50001 4 0 0 25 0 1 0 422719419 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+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1611 0 0 0 51001 4 0 0 25 0 1 0 422719419 8224768 1550 4294967295 134512640 134672761 3221224560 3221223728 134560912 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1612 0 0 0 52001 4 0 0 25 0 1 0 422719419 8224768 1551 4294967295 134512640 134672761 3221224560 3221223760 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1551 603 41 0 1967 0
vsize: 8032
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1612 0 0 0 53001 4 0 0 25 0 1 0 422719419 8224768 1551 4294967295 134512640 134672761 3221224560 3221223696 134565119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1551 603 41 0 1967 0
vsize: 8032
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1612 0 0 0 54002 4 0 0 25 0 1 0 422719419 8224768 1551 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1551 603 41 0 1967 0
vsize: 8032
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1613 0 0 0 55002 4 0 0 25 0 1 0 422719419 8224768 1552 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1552 603 41 0 1967 0
vsize: 8032
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1614 0 0 0 56002 4 0 0 25 0 1 0 422719419 8224768 1553 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1614 0 0 0 57002 4 0 0 25 0 1 0 422719419 8224768 1553 4294967295 134512640 134672761 3221224560 3221223728 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1614 0 0 0 58002 4 0 0 25 0 1 0 422719419 8224768 1553 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1553 603 41 0 1967 0
vsize: 8032
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1615 0 0 0 59003 4 0 0 25 0 1 0 422719419 8224768 1554 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2008 1554 603 41 0 1967 0
vsize: 8032
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1692 0 0 0 60002 5 0 0 25 0 1 0 422719419 8491008 1631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2073 1631 603 41 0 2032 0
vsize: 8292
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1694 0 0 0 61002 5 0 0 25 0 1 0 422719419 8491008 1633 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2073 1633 603 41 0 2032 0
vsize: 8292
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1695 0 0 0 62002 5 0 0 25 0 1 0 422719419 8491008 1634 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2073 1634 603 41 0 2032 0
vsize: 8292
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1699 0 0 0 63002 5 0 0 25 0 1 0 422719419 8638464 1638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1638 603 41 0 2068 0
vsize: 8436
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1701 0 0 0 64002 5 0 0 25 0 1 0 422719419 8638464 1640 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1704 0 0 0 65003 5 0 0 25 0 1 0 422719419 8638464 1643 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1643 603 41 0 2068 0
vsize: 8436
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1715 0 0 0 66003 5 0 0 25 0 1 0 422719419 8638464 1654 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1654 603 41 0 2068 0
vsize: 8436
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1719 0 0 0 67003 5 0 0 25 0 1 0 422719419 8638464 1658 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1658 603 41 0 2068 0
vsize: 8436
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1720 0 0 0 68003 5 0 0 25 0 1 0 422719419 8638464 1659 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1659 603 41 0 2068 0
vsize: 8436
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1721 0 0 0 69003 5 0 0 25 0 1 0 422719419 8638464 1660 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1660 603 41 0 2068 0
vsize: 8436
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1722 0 0 0 70003 5 0 0 25 0 1 0 422719419 8638464 1661 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1661 603 41 0 2068 0
vsize: 8436
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1732 0 0 0 71004 5 0 0 25 0 1 0 422719419 8818688 1671 4294967295 134512640 134672761 3221224560 3221223664 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1671 603 41 0 2112 0
vsize: 8612
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1732 0 0 0 72004 5 0 0 25 0 1 0 422719419 8818688 1671 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1671 603 41 0 2112 0
vsize: 8612
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1733 0 0 0 73004 5 0 0 25 0 1 0 422719419 8818688 1672 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1672 603 41 0 2112 0
vsize: 8612
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1733 0 0 0 74004 5 0 0 25 0 1 0 422719419 8818688 1672 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1672 603 41 0 2112 0
vsize: 8612
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1742 0 0 0 75004 5 0 0 25 0 1 0 422719419 8818688 1681 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1681 603 41 0 2112 0
vsize: 8612
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1742 0 0 0 76005 5 0 0 25 0 1 0 422719419 8818688 1681 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1681 603 41 0 2112 0
vsize: 8612
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1751 0 0 0 77005 5 0 0 25 0 1 0 422719419 8818688 1690 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1690 603 41 0 2112 0
vsize: 8612
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1751 0 0 0 78005 5 0 0 25 0 1 0 422719419 8818688 1690 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1690 603 41 0 2112 0
vsize: 8612
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1751 0 0 0 79005 5 0 0 25 0 1 0 422719419 8818688 1690 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1690 603 41 0 2112 0
vsize: 8612
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1761 0 0 0 80005 5 0 0 25 0 1 0 422719419 9015296 1700 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1700 603 41 0 2160 0
vsize: 8804
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1761 0 0 0 81006 5 0 0 25 0 1 0 422719419 9015296 1700 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1700 603 41 0 2160 0
vsize: 8804
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1771 0 0 0 82006 5 0 0 25 0 1 0 422719419 9015296 1710 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1771 0 0 0 83006 5 0 0 25 0 1 0 422719419 9015296 1710 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1771 0 0 0 84006 5 0 0 25 0 1 0 422719419 9015296 1710 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1771 0 0 0 85006 5 0 0 25 0 1 0 422719419 9015296 1710 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1710 603 41 0 2160 0
vsize: 8804
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1780 0 0 0 86007 5 0 0 25 0 1 0 422719419 9015296 1719 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1719 603 41 0 2160 0
vsize: 8804
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1780 0 0 0 87007 5 0 0 25 0 1 0 422719419 9015296 1719 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1719 603 41 0 2160 0
vsize: 8804
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1781 0 0 0 88007 5 0 0 25 0 1 0 422719419 9015296 1720 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1781 0 0 0 89007 5 0 0 25 0 1 0 422719419 9015296 1720 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1781 0 0 0 90007 5 0 0 25 0 1 0 422719419 9015296 1720 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1781 0 0 0 91007 5 0 0 25 0 1 0 422719419 9015296 1720 4294967295 134512640 134672761 3221224560 3221223760 134557852 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1781 0 0 0 92007 5 0 0 25 0 1 0 422719419 9015296 1720 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2201 1720 603 41 0 2160 0
vsize: 8804
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1795 0 0 0 93007 5 0 0 25 0 1 0 422719419 9146368 1734 4294967295 134512640 134672761 3221224560 3221223772 1075346912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1734 603 41 0 2192 0
vsize: 8932
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1807 0 0 0 94007 5 0 0 25 0 1 0 422719419 9146368 1746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1746 603 41 0 2192 0
vsize: 8932
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1808 0 0 0 95008 5 0 0 25 0 1 0 422719419 9146368 1747 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1747 603 41 0 2192 0
vsize: 8932
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1809 0 0 0 96008 5 0 0 25 0 1 0 422719419 9146368 1748 4294967295 134512640 134672761 3221224560 3221223744 134558362 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1748 603 41 0 2192 0
vsize: 8932
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1809 0 0 0 97008 5 0 0 25 0 1 0 422719419 9146368 1748 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1748 603 41 0 2192 0
vsize: 8932
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1809 0 0 0 98008 5 0 0 25 0 1 0 422719419 9146368 1748 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2233 1748 603 41 0 2192 0
vsize: 8932
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1819 0 0 0 99008 5 0 0 25 0 1 0 422719419 9306112 1758 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1758 603 41 0 2231 0
vsize: 9088
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1820 0 0 0 100009 5 0 0 25 0 1 0 422719419 9306112 1759 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1759 603 41 0 2231 0
vsize: 9088
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1820 0 0 0 101009 5 0 0 25 0 1 0 422719419 9306112 1759 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1759 603 41 0 2231 0
vsize: 9088
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1829 0 0 0 102009 5 0 0 25 0 1 0 422719419 9306112 1768 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1768 603 41 0 2231 0
vsize: 9088
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1829 0 0 0 103009 5 0 0 25 0 1 0 422719419 9306112 1768 4294967295 134512640 134672761 3221224560 3221223696 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1768 603 41 0 2231 0
vsize: 9088
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1830 0 0 0 104009 5 0 0 25 0 1 0 422719419 9306112 1769 4294967295 134512640 134672761 3221224560 3221223652 1075346941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1830 0 0 0 105010 5 0 0 25 0 1 0 422719419 9306112 1769 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1830 0 0 0 106010 5 0 0 25 0 1 0 422719419 9306112 1769 4294967295 134512640 134672761 3221224560 3221223684 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1830 0 0 0 107010 5 0 0 25 0 1 0 422719419 9306112 1769 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2272 1769 603 41 0 2231 0
vsize: 9088
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 108010 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 109010 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 110010 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 111011 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 112011 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 113011 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 114011 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 115011 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 116011 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 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+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 117011 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 118011 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 119011 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18797
Raw data (stat): 18797 (minisat+) R 18796 10720 10719 0 -1 0 1842 0 0 0 120011 5 0 0 25 0 1 0 422719419 9469952 1781 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1781 603 41 0 2271 0
vsize: 9248
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 18797
Raw data (stat): 18797 (minisat+) Z 18796 10720 10719 0 -1 12 1844 0 0 0 120011 6 0 0 25 0 1 0 422719419 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.04
CPU time (s): 1200.18
CPU user time (s): 1200.12
CPU system time (s): 0.06299
CPU usage (%): 100.012
Max. virtual memory (Kb): 9248
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####