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-1.opb
MD5SUM	64e81a7b23abbb8a6da4e2377ea69dee
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	13453
Number of constraints which are clauses	13453
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 5935

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        833320 kB
Buffers:         35348 kB
Cached:         125512 kB
SwapCached:       2476 kB
Active:          56132 kB
Inactive:       110144 kB
HighTotal:      131008 kB
HighFree:         2296 kB
LowTotal:       903652 kB
LowFree:        831024 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29492 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:40:23 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 4340 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13039 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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 |    9878    24638 |    3292       0        0     nan |  0.000 % |
c |       101 |    9878    24638 |    3621     101     1231    12.2 | 23.867 % |
c |       251 |    9878    24638 |    3983     251     5277    21.0 | 23.867 % |
c |       476 |    9878    24638 |    4381     476     8655    18.2 | 23.867 % |
c |       814 |    9878    24638 |    4819     814    19600    24.1 | 23.867 % |
c |      1320 |    9878    24638 |    5301    1320    27899    21.1 | 23.867 % |
c |      2082 |    9878    24638 |    5831    2082    57645    27.7 | 23.867 % |
c |      3221 |    9878    24638 |    6415    3221    93388    29.0 | 23.867 % |
c |      4931 |    9878    24638 |    7056    4931   143848    29.2 | 23.867 % |
c |      7493 |    9878    24638 |    7762    7493   210661    28.1 | 23.867 % |
c |     11338 |    9878    24638 |    8538    6644   169658    25.5 | 23.867 % |
c |     17105 |    9878    24638 |    9392    7285   177959    24.4 | 23.867 % |
c |     25754 |    9878    24638 |   10331   10409   254945    24.5 | 23.867 % |
c |     38729 |    9878    24638 |   11364   11455   286759    25.0 | 23.867 % |
c |     58191 |    9878    24638 |   12501   11386   282530    24.8 | 23.867 % |
c |     87384 |    9878    24638 |   13751   12309   296202    24.1 | 23.867 % |
c |    131173 |    9868    24616 |   15126   10027   237728    23.7 | 23.929 % |
c |    196858 |    9868    24616 |   16639    8659   223250    25.8 | 23.929 % |
c |    295384 |    9868    24616 |   18303   16056   367503    22.9 | 23.929 % |
c |    443174 |    9868    24616 |   20133   14387   321561    22.4 | 23.929 % |
#### 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.71 0.91 0.90 2/54 29802
Raw data (stat): 29802 (runsolver) R 29801 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480948550 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0013 s]
Raw data (loadavg): 0.75 0.91 0.90 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1255 0 0 0 996 3 0 0 25 0 1 0 480948550 6541312 1194 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1597 1194 603 41 0 1556 0
vsize: 6388
[startup+20.0016 s]
Raw data (loadavg): 0.79 0.91 0.90 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1255 0 0 0 1995 3 0 0 25 0 1 0 480948550 6541312 1194 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1597 1194 603 41 0 1556 0
vsize: 6388
[startup+30.0027 s]
Raw data (loadavg): 0.82 0.92 0.90 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1255 0 0 0 2995 3 0 0 25 0 1 0 480948550 6541312 1194 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1597 1194 603 41 0 1556 0
vsize: 6388
[startup+40.0034 s]
Raw data (loadavg): 0.85 0.92 0.90 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1257 0 0 0 3995 4 0 0 25 0 1 0 480948550 6680576 1196 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1631 1196 603 41 0 1590 0
vsize: 6524
[startup+50.0043 s]
Raw data (loadavg): 0.87 0.92 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1298 0 0 0 4994 4 0 0 25 0 1 0 480948550 6815744 1237 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1664 1237 603 41 0 1623 0
vsize: 6656
[startup+60.0043 s]
Raw data (loadavg): 0.89 0.92 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1309 0 0 0 5994 5 0 0 25 0 1 0 480948550 6815744 1248 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1664 1248 603 41 0 1623 0
vsize: 6656
[startup+70.0054 s]
Raw data (loadavg): 0.91 0.92 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1324 0 0 0 6994 5 0 0 25 0 1 0 480948550 6950912 1263 4294967295 134512640 134672761 3221224560 3221223744 134559522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1697 1263 603 41 0 1656 0
vsize: 6788
[startup+80.0072 s]
Raw data (loadavg): 0.92 0.93 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1375 0 0 0 7993 6 0 0 25 0 1 0 480948550 7081984 1314 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1729 1314 603 41 0 1688 0
vsize: 6916
[startup+90.0074 s]
Raw data (loadavg): 0.93 0.93 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1385 0 0 0 8992 6 0 0 25 0 1 0 480948550 7221248 1324 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1763 1324 603 41 0 1722 0
vsize: 7052
[startup+100.007 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1393 0 0 0 9992 6 0 0 25 0 1 0 480948550 7221248 1332 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1763 1332 603 41 0 1722 0
vsize: 7052
[startup+110.008 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1397 0 0 0 10992 7 0 0 25 0 1 0 480948550 7221248 1336 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1763 1336 603 41 0 1722 0
vsize: 7052
[startup+120.008 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1410 0 0 0 11991 7 0 0 25 0 1 0 480948550 7368704 1349 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1799 1349 603 41 0 1758 0
vsize: 7196
[startup+130.01 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1441 0 0 0 12991 7 0 0 25 0 1 0 480948550 7368704 1380 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1799 1380 603 41 0 1758 0
vsize: 7196
[startup+140.01 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1447 0 0 0 13991 8 0 0 25 0 1 0 480948550 7516160 1386 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1386 603 41 0 1794 0
vsize: 7340
[startup+150.01 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1448 0 0 0 14991 8 0 0 25 0 1 0 480948550 7516160 1387 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1387 603 41 0 1794 0
vsize: 7340
[startup+160.012 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1451 0 0 0 15991 8 0 0 25 0 1 0 480948550 7516160 1390 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1390 603 41 0 1794 0
vsize: 7340
[startup+170.013 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1459 0 0 0 16990 9 0 0 25 0 1 0 480948550 7516160 1398 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1398 603 41 0 1794 0
vsize: 7340
[startup+180.013 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1467 0 0 0 17990 9 0 0 25 0 1 0 480948550 7516160 1406 4294967295 134512640 134672761 3221224560 3221223760 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1835 1406 603 41 0 1794 0
vsize: 7340
[startup+190.014 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1475 0 0 0 18989 10 0 0 25 0 1 0 480948550 7651328 1414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1868 1414 603 41 0 1827 0
vsize: 7472
[startup+200.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1507 0 0 0 19989 10 0 0 25 0 1 0 480948550 7798784 1446 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1446 603 41 0 1863 0
vsize: 7616
[startup+210.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1510 0 0 0 20988 10 0 0 25 0 1 0 480948550 7798784 1449 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1449 603 41 0 1863 0
vsize: 7616
[startup+220.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1516 0 0 0 21988 10 0 0 25 0 1 0 480948550 7798784 1455 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1455 603 41 0 1863 0
vsize: 7616
[startup+230.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1521 0 0 0 22988 11 0 0 25 0 1 0 480948550 7798784 1460 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1460 603 41 0 1863 0
vsize: 7616
[startup+240.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1541 0 0 0 23988 11 0 0 25 0 1 0 480948550 7933952 1480 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1937 1480 603 41 0 1896 0
vsize: 7748
[startup+250.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1549 0 0 0 24988 11 0 0 25 0 1 0 480948550 7933952 1488 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1937 1488 603 41 0 1896 0
vsize: 7748
[startup+260.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1554 0 0 0 25988 11 0 0 25 0 1 0 480948550 7933952 1493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1937 1493 603 41 0 1896 0
vsize: 7748
[startup+270.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1555 0 0 0 26988 11 0 0 25 0 1 0 480948550 7933952 1494 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1937 1494 603 41 0 1896 0
vsize: 7748
[startup+280.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1561 0 0 0 27988 11 0 0 25 0 1 0 480948550 8073216 1500 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1971 1500 603 41 0 1930 0
vsize: 7884
[startup+290.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1634 0 0 0 28988 12 0 0 25 0 1 0 480948550 8429568 1573 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2058 1573 603 41 0 2017 0
vsize: 8232
[startup+300.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1643 0 0 0 29988 12 0 0 25 0 1 0 480948550 8429568 1582 4294967295 134512640 134672761 3221224560 3221223760 134557892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2058 1582 603 41 0 2017 0
vsize: 8232
[startup+310.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1678 0 0 0 30988 12 0 0 25 0 1 0 480948550 8564736 1617 4294967295 134512640 134672761 3221224560 3221223744 134558504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1617 603 41 0 2050 0
vsize: 8364
[startup+320.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1684 0 0 0 31988 12 0 0 25 0 1 0 480948550 8564736 1623 4294967295 134512640 134672761 3221224560 3221223728 134560811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1623 603 41 0 2050 0
vsize: 8364
[startup+330.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1692 0 0 0 32988 12 0 0 25 0 1 0 480948550 8564736 1631 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+340.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1692 0 0 0 33988 12 0 0 25 0 1 0 480948550 8564736 1631 4294967295 134512640 134672761 3221224560 3221223716 134565028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+350.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1692 0 0 0 34988 12 0 0 25 0 1 0 480948550 8564736 1631 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+360.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1692 0 0 0 35989 12 0 0 25 0 1 0 480948550 8564736 1631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+370.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1692 0 0 0 36989 12 0 0 25 0 1 0 480948550 8564736 1631 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+380.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1694 0 0 0 37989 12 0 0 25 0 1 0 480948550 8564736 1633 4294967295 134512640 134672761 3221224560 3221223664 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1633 603 41 0 2050 0
vsize: 8364
[startup+390.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1694 0 0 0 38989 12 0 0 25 0 1 0 480948550 8564736 1633 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1633 603 41 0 2050 0
vsize: 8364
[startup+400.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1696 0 0 0 39989 12 0 0 25 0 1 0 480948550 8564736 1635 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1635 603 41 0 2050 0
vsize: 8364
[startup+410.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1696 0 0 0 40989 13 0 0 25 0 1 0 480948550 8564736 1635 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1635 603 41 0 2050 0
vsize: 8364
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1698 0 0 0 41989 13 0 0 25 0 1 0 480948550 8564736 1637 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1637 603 41 0 2050 0
vsize: 8364
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1698 0 0 0 42989 13 0 0 25 0 1 0 480948550 8564736 1637 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1637 603 41 0 2050 0
vsize: 8364
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1713 0 0 0 43989 13 0 0 25 0 1 0 480948550 8695808 1652 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1652 603 41 0 2082 0
vsize: 8492
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1721 0 0 0 44989 13 0 0 25 0 1 0 480948550 8695808 1660 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1660 603 41 0 2082 0
vsize: 8492
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1723 0 0 0 45990 13 0 0 25 0 1 0 480948550 8695808 1662 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1662 603 41 0 2082 0
vsize: 8492
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1729 0 0 0 46990 13 0 0 25 0 1 0 480948550 8695808 1668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1668 603 41 0 2082 0
vsize: 8492
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1730 0 0 0 47990 13 0 0 25 0 1 0 480948550 8695808 1669 4294967295 134512640 134672761 3221224560 3221223728 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1669 603 41 0 2082 0
vsize: 8492
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1737 0 0 0 48990 13 0 0 25 0 1 0 480948550 8859648 1676 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1676 603 41 0 2122 0
vsize: 8652
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1742 0 0 0 49990 13 0 0 25 0 1 0 480948550 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1742 0 0 0 50990 13 0 0 25 0 1 0 480948550 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1742 0 0 0 51990 13 0 0 25 0 1 0 480948550 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1742 0 0 0 52991 13 0 0 25 0 1 0 480948550 8859648 1681 4294967295 134512640 134672761 3221224560 3221223696 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1742 0 0 0 53991 13 0 0 25 0 1 0 480948550 8859648 1681 4294967295 134512640 134672761 3221224560 3221223760 134557897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1742 0 0 0 54991 13 0 0 25 0 1 0 480948550 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1742 0 0 0 55991 13 0 0 25 0 1 0 480948550 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1742 0 0 0 56991 13 0 0 25 0 1 0 480948550 8859648 1681 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1748 0 0 0 57992 13 0 0 25 0 1 0 480948550 8859648 1687 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1687 603 41 0 2122 0
vsize: 8652
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1756 0 0 0 58992 13 0 0 25 0 1 0 480948550 8859648 1695 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1695 603 41 0 2122 0
vsize: 8652
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1758 0 0 0 59992 13 0 0 25 0 1 0 480948550 8859648 1697 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1697 603 41 0 2122 0
vsize: 8652
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1758 0 0 0 60992 13 0 0 25 0 1 0 480948550 8859648 1697 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1697 603 41 0 2122 0
vsize: 8652
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1758 0 0 0 61992 13 0 0 25 0 1 0 480948550 8859648 1697 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1697 603 41 0 2122 0
vsize: 8652
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1758 0 0 0 62992 14 0 0 25 0 1 0 480948550 8859648 1697 4294967295 134512640 134672761 3221224560 3221223696 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1697 603 41 0 2122 0
vsize: 8652
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1759 0 0 0 63992 14 0 0 25 0 1 0 480948550 8859648 1698 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1698 603 41 0 2122 0
vsize: 8652
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1759 0 0 0 64992 14 0 0 25 0 1 0 480948550 8859648 1698 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1698 603 41 0 2122 0
vsize: 8652
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1759 0 0 0 65992 14 0 0 25 0 1 0 480948550 8859648 1698 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1698 603 41 0 2122 0
vsize: 8652
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1759 0 0 0 66992 14 0 0 25 0 1 0 480948550 8859648 1698 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1698 603 41 0 2122 0
vsize: 8652
[startup+680.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1770 0 0 0 67993 14 0 0 25 0 1 0 480948550 9023488 1709 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1709 603 41 0 2162 0
vsize: 8812
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1771 0 0 0 68993 14 0 0 25 0 1 0 480948550 9023488 1710 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1710 603 41 0 2162 0
vsize: 8812
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1773 0 0 0 69993 14 0 0 25 0 1 0 480948550 9023488 1712 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1712 603 41 0 2162 0
vsize: 8812
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1784 0 0 0 70993 14 0 0 25 0 1 0 480948550 9023488 1723 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1784 0 0 0 71993 14 0 0 25 0 1 0 480948550 9023488 1723 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1784 0 0 0 72993 14 0 0 25 0 1 0 480948550 9023488 1723 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+740.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1784 0 0 0 73993 14 0 0 25 0 1 0 480948550 9023488 1723 4294967295 134512640 134672761 3221224560 3221223664 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1784 0 0 0 74993 14 0 0 25 0 1 0 480948550 9023488 1723 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1784 0 0 0 75994 14 0 0 25 0 1 0 480948550 9023488 1723 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+770.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1785 0 0 0 76994 14 0 0 25 0 1 0 480948550 9023488 1724 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1724 603 41 0 2162 0
vsize: 8812
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1785 0 0 0 77994 14 0 0 25 0 1 0 480948550 9023488 1724 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1724 603 41 0 2162 0
vsize: 8812
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1785 0 0 0 78994 14 0 0 25 0 1 0 480948550 9023488 1724 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1724 603 41 0 2162 0
vsize: 8812
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1796 0 0 0 79994 14 0 0 25 0 1 0 480948550 9023488 1735 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1735 603 41 0 2162 0
vsize: 8812
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1796 0 0 0 80994 14 0 0 25 0 1 0 480948550 9023488 1735 4294967295 134512640 134672761 3221224560 3221223664 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1735 603 41 0 2162 0
vsize: 8812
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1796 0 0 0 81995 14 0 0 25 0 1 0 480948550 9023488 1735 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1735 603 41 0 2162 0
vsize: 8812
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1796 0 0 0 82995 14 0 0 25 0 1 0 480948550 9023488 1735 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1735 603 41 0 2162 0
vsize: 8812
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1796 0 0 0 83995 14 0 0 25 0 1 0 480948550 9023488 1735 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1735 603 41 0 2162 0
vsize: 8812
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1797 0 0 0 84995 14 0 0 25 0 1 0 480948550 9023488 1736 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2203 1736 603 41 0 2162 0
vsize: 8812
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1805 0 0 0 85995 15 0 0 25 0 1 0 480948550 9187328 1744 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1744 603 41 0 2202 0
vsize: 8972
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1805 0 0 0 86995 15 0 0 25 0 1 0 480948550 9187328 1744 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1744 603 41 0 2202 0
vsize: 8972
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1807 0 0 0 87995 15 0 0 25 0 1 0 480948550 9187328 1746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1746 603 41 0 2202 0
vsize: 8972
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1807 0 0 0 88995 15 0 0 25 0 1 0 480948550 9187328 1746 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1746 603 41 0 2202 0
vsize: 8972
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1813 0 0 0 89996 15 0 0 25 0 1 0 480948550 9187328 1752 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1752 603 41 0 2202 0
vsize: 8972
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1815 0 0 0 90996 15 0 0 25 0 1 0 480948550 9187328 1754 4294967295 134512640 134672761 3221224560 3221223684 134566082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1754 603 41 0 2202 0
vsize: 8972
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1815 0 0 0 91996 15 0 0 25 0 1 0 480948550 9187328 1754 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1754 603 41 0 2202 0
vsize: 8972
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1816 0 0 0 92996 15 0 0 25 0 1 0 480948550 9187328 1755 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1755 603 41 0 2202 0
vsize: 8972
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1827 0 0 0 93996 15 0 0 25 0 1 0 480948550 9187328 1766 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2243 1766 603 41 0 2202 0
vsize: 8972
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1838 0 0 0 94996 15 0 0 25 0 1 0 480948550 9351168 1777 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2283 1777 603 41 0 2242 0
vsize: 9132
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1838 0 0 0 95997 15 0 0 25 0 1 0 480948550 9351168 1777 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2283 1777 603 41 0 2242 0
vsize: 9132
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1838 0 0 0 96997 15 0 0 25 0 1 0 480948550 9351168 1777 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2283 1777 603 41 0 2242 0
vsize: 9132
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1846 0 0 0 97996 15 0 0 25 0 1 0 480948550 9351168 1785 4294967295 134512640 134672761 3221224560 3221223744 134559566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2283 1785 603 41 0 2242 0
vsize: 9132
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1898 0 0 0 98995 16 0 0 25 0 1 0 480948550 9482240 1837 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2315 1837 603 41 0 2274 0
vsize: 9260
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1903 0 0 0 99995 16 0 0 25 0 1 0 480948550 9621504 1842 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1842 603 41 0 2308 0
vsize: 9396
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1913 0 0 0 100996 16 0 0 25 0 1 0 480948550 9621504 1852 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1852 603 41 0 2308 0
vsize: 9396
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1917 0 0 0 101996 16 0 0 25 0 1 0 480948550 9621504 1856 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1856 603 41 0 2308 0
vsize: 9396
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1924 0 0 0 102996 16 0 0 25 0 1 0 480948550 9621504 1863 4294967295 134512640 134672761 3221224560 3221223664 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1863 603 41 0 2308 0
vsize: 9396
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1924 0 0 0 103996 16 0 0 25 0 1 0 480948550 9621504 1863 4294967295 134512640 134672761 3221224560 3221223664 134554673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1863 603 41 0 2308 0
vsize: 9396
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1924 0 0 0 104996 16 0 0 25 0 1 0 480948550 9621504 1863 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1863 603 41 0 2308 0
vsize: 9396
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1924 0 0 0 105996 16 0 0 25 0 1 0 480948550 9621504 1863 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1863 603 41 0 2308 0
vsize: 9396
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1929 0 0 0 106997 16 0 0 25 0 1 0 480948550 9621504 1868 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1868 603 41 0 2308 0
vsize: 9396
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1929 0 0 0 107997 16 0 0 25 0 1 0 480948550 9621504 1868 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1868 603 41 0 2308 0
vsize: 9396
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1929 0 0 0 108997 16 0 0 25 0 1 0 480948550 9621504 1868 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1868 603 41 0 2308 0
vsize: 9396
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1929 0 0 0 109997 16 0 0 25 0 1 0 480948550 9621504 1868 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1868 603 41 0 2308 0
vsize: 9396
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1930 0 0 0 110997 16 0 0 25 0 1 0 480948550 9621504 1869 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2349 1869 603 41 0 2308 0
vsize: 9396
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1936 0 0 0 111997 16 0 0 25 0 1 0 480948550 9752576 1875 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2381 1875 603 41 0 2340 0
vsize: 9524
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1936 0 0 0 112998 16 0 0 25 0 1 0 480948550 9752576 1875 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2381 1875 603 41 0 2340 0
vsize: 9524
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1936 0 0 0 113998 16 0 0 25 0 1 0 480948550 9752576 1875 4294967295 134512640 134672761 3221224560 3221223728 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2381 1875 603 41 0 2340 0
vsize: 9524
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1947 0 0 0 114998 16 0 0 25 0 1 0 480948550 9752576 1886 4294967295 134512640 134672761 3221224560 3221223760 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2381 1886 603 41 0 2340 0
vsize: 9524
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1947 0 0 0 115998 16 0 0 25 0 1 0 480948550 9752576 1886 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2381 1886 603 41 0 2340 0
vsize: 9524
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1947 0 0 0 116998 16 0 0 25 0 1 0 480948550 9752576 1886 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2381 1886 603 41 0 2340 0
vsize: 9524
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1947 0 0 0 117999 16 0 0 25 0 1 0 480948550 9752576 1886 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2381 1886 603 41 0 2340 0
vsize: 9524
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1947 0 0 0 118999 16 0 0 25 0 1 0 480948550 9752576 1886 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2381 1886 603 41 0 2340 0
vsize: 9524
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29802
Raw data (stat): 29802 (minisat+) R 29801 22612 22611 0 -1 0 1948 0 0 0 119999 16 0 0 25 0 1 0 480948550 9752576 1887 4294967295 134512640 134672761 3221224560 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2381 1887 603 41 0 2340 0
vsize: 9524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29802
Raw data (stat): 29802 (minisat+) Z 29801 22612 22611 0 -1 12 1950 0 0 0 119999 17 0 0 25 0 1 0 480948550 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.04
CPU time (s): 1200.17
CPU user time (s): 1199.99
CPU system time (s): 0.171973
CPU usage (%): 100.011
Max. virtual memory (Kb): 9524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####