PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-par32-4.opb
MD5SUM	4ad922a0ad53056b410be6ab5caa6b5b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	6352
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	6352
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	6352
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	6352
Total number of constraints	13489
Number of constraints which are clauses	13489
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	3
Trace number 5152

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-13 22:15:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3594 boxname=wulflinc4 idbench=210 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4ad922a0ad53056b410be6ab5caa6b5b  /oldhome/oroussel/tmp/wulflinc4/normalized-par32-4.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc4/normalized-par32-4.opb /oldhome/oroussel/tmp/wulflinc4/normalized-par32-4.opb
IDLAUNCH: 3594
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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.169
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:        921900 kB
Buffers:         34664 kB
Cached:          58496 kB
SwapCached:          0 kB
Active:          52916 kB
Inactive:        43116 kB
HighTotal:      131008 kB
HighFree:        68628 kB
LowTotal:       903652 kB
LowFree:        853272 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11132 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:35:41 (client local time) WITH STATUS 0 IN 1209.94 SECONDS
stats: 3594 7 1209.94 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13075 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9815    24584 |    3271       0        0     nan |  0.000 % |
c |       100 |    9815    24584 |    3598     100     1175    11.8 | 24.906 % |
c |       250 |    9815    24584 |    3957     250     4761    19.0 | 24.906 % |
c |       476 |    9815    24584 |    4353     476     8036    16.9 | 24.906 % |
c |       814 |    9805    24562 |    4789     813    16099    19.8 | 24.969 % |
c |      1321 |    9805    24562 |    5267    1320    31268    23.7 | 24.969 % |
c |      2080 |    9805    24562 |    5794    2079    42787    20.6 | 24.969 % |
c |      3220 |    9805    24562 |    6374    3219    75648    23.5 | 24.969 % |
c |      4928 |    9805    24562 |    7011    4927   107201    21.8 | 24.969 % |
c |      7490 |    9805    24562 |    7712    7489   180306    24.1 | 24.969 % |
c |     11334 |    9805    24562 |    8484    6526   158927    24.4 | 24.969 % |
c |     17101 |    9805    24562 |    9332    7165   174694    24.4 | 24.969 % |
c |     25751 |    9805    24562 |   10265   10288   256474    24.9 | 24.969 % |
c |     38726 |    9805    24562 |   11292   11339   271909    24.0 | 24.969 % |
c |     58189 |    9805    24562 |   12421   11405   270262    23.7 | 24.969 % |
c |     87381 |    9805    24562 |   13663   12378   287949    23.3 | 24.969 % |
c |    131171 |    9805    24562 |   15030   10244   241970    23.6 | 24.969 % |
c |    196856 |    9805    24562 |   16533    8936   193461    21.6 | 24.969 % |
c |    295383 |    9805    24562 |   18186   16303   374771    23.0 | 24.969 % |
c |    443174 |    9805    24562 |   20005   15022   328559    21.9 | 24.969 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/54 9469
Raw data (stat): 9469 (runsolver) R 9468 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421249285 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1253 0 0 0 995 3 0 0 25 0 1 0 421249285 6541312 1192 4294967295 134512640 134672761 3221224576 3221223712 134565137 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.0003 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1254 0 0 0 1994 4 0 0 25 0 1 0 421249285 6545408 1193 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1598 1193 603 41 0 1557 0
vsize: 6392
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1254 0 0 0 2994 4 0 0 25 0 1 0 421249285 6545408 1193 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1598 1193 603 41 0 1557 0
vsize: 6392
[startup+40.002 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1262 0 0 0 3994 4 0 0 25 0 1 0 421249285 6684672 1201 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1632 1201 603 41 0 1591 0
vsize: 6528
[startup+50.0028 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1319 0 0 0 4993 5 0 0 25 0 1 0 421249285 6828032 1258 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1667 1258 603 41 0 1626 0
vsize: 6668
[startup+60.0032 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1332 0 0 0 5992 5 0 0 25 0 1 0 421249285 6963200 1271 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1700 1271 603 41 0 1659 0
vsize: 6800
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1373 0 0 0 6992 6 0 0 25 0 1 0 421249285 7098368 1312 4294967295 134512640 134672761 3221224576 3221223760 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1312 603 41 0 1692 0
vsize: 6932
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1389 0 0 0 7991 6 0 0 25 0 1 0 421249285 7233536 1328 4294967295 134512640 134672761 3221224576 3221223760 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1766 1328 603 41 0 1725 0
vsize: 7064
[startup+90.0047 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1393 0 0 0 8991 7 0 0 25 0 1 0 421249285 7233536 1332 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1766 1332 603 41 0 1725 0
vsize: 7064
[startup+100.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1404 0 0 0 9991 7 0 0 25 0 1 0 421249285 7233536 1343 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1766 1343 603 41 0 1725 0
vsize: 7064
[startup+110.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1447 0 0 0 10990 7 0 0 25 0 1 0 421249285 7512064 1386 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1386 603 41 0 1793 0
vsize: 7336
[startup+120.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1450 0 0 0 11990 8 0 0 25 0 1 0 421249285 7512064 1389 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1389 603 41 0 1793 0
vsize: 7336
[startup+130.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1460 0 0 0 12989 8 0 0 25 0 1 0 421249285 7512064 1399 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1399 603 41 0 1793 0
vsize: 7336
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1466 0 0 0 13988 9 0 0 25 0 1 0 421249285 7512064 1405 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1405 603 41 0 1793 0
vsize: 7336
[startup+150.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1467 0 0 0 14988 9 0 0 25 0 1 0 421249285 7512064 1406 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1834 1406 603 41 0 1793 0
vsize: 7336
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1513 0 0 0 15988 10 0 0 25 0 1 0 421249285 7811072 1452 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1907 1452 603 41 0 1866 0
vsize: 7628
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1538 0 0 0 16987 10 0 0 25 0 1 0 421249285 7811072 1477 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1907 1477 603 41 0 1866 0
vsize: 7628
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1549 0 0 0 17987 10 0 0 25 0 1 0 421249285 7942144 1488 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1488 603 41 0 1898 0
vsize: 7756
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1558 0 0 0 18986 11 0 0 25 0 1 0 421249285 7942144 1497 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1497 603 41 0 1898 0
vsize: 7756
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1565 0 0 0 19986 11 0 0 25 0 1 0 421249285 7942144 1504 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1504 603 41 0 1898 0
vsize: 7756
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1572 0 0 0 20986 11 0 0 25 0 1 0 421249285 7942144 1511 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1511 603 41 0 1898 0
vsize: 7756
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1572 0 0 0 21986 11 0 0 25 0 1 0 421249285 7942144 1511 4294967295 134512640 134672761 3221224576 3221223776 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1511 603 41 0 1898 0
vsize: 7756
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1579 0 0 0 22985 11 0 0 25 0 1 0 421249285 8105984 1518 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1979 1518 603 41 0 1938 0
vsize: 7916
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1596 0 0 0 23985 12 0 0 25 0 1 0 421249285 8105984 1535 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1979 1535 603 41 0 1938 0
vsize: 7916
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1636 0 0 0 24984 12 0 0 25 0 1 0 421249285 8364032 1575 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2042 1575 603 41 0 2001 0
vsize: 8168
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1642 0 0 0 25984 13 0 0 25 0 1 0 421249285 8364032 1581 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2042 1581 603 41 0 2001 0
vsize: 8168
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1650 0 0 0 26984 13 0 0 25 0 1 0 421249285 8503296 1589 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1589 603 41 0 2035 0
vsize: 8304
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1651 0 0 0 27983 13 0 0 25 0 1 0 421249285 8503296 1590 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1590 603 41 0 2035 0
vsize: 8304
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1656 0 0 0 28983 13 0 0 25 0 1 0 421249285 8503296 1595 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1595 603 41 0 2035 0
vsize: 8304
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1657 0 0 0 29983 14 0 0 25 0 1 0 421249285 8503296 1596 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1596 603 41 0 2035 0
vsize: 8304
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1661 0 0 0 30983 14 0 0 25 0 1 0 421249285 8503296 1600 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1600 603 41 0 2035 0
vsize: 8304
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1668 0 0 0 31982 14 0 0 25 0 1 0 421249285 8503296 1607 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1607 603 41 0 2035 0
vsize: 8304
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1670 0 0 0 32982 14 0 0 25 0 1 0 421249285 8503296 1609 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1609 603 41 0 2035 0
vsize: 8304
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1673 0 0 0 33982 14 0 0 25 0 1 0 421249285 8503296 1612 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1612 603 41 0 2035 0
vsize: 8304
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1673 0 0 0 34982 15 0 0 25 0 1 0 421249285 8503296 1612 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1612 603 41 0 2035 0
vsize: 8304
[startup+360.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1674 0 0 0 35981 15 0 0 25 0 1 0 421249285 8503296 1613 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1613 603 41 0 2035 0
vsize: 8304
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1674 0 0 0 36981 16 0 0 25 0 1 0 421249285 8503296 1613 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2076 1613 603 41 0 2035 0
vsize: 8304
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1690 0 0 0 37980 16 0 0 25 0 1 0 421249285 8638464 1629 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1629 603 41 0 2068 0
vsize: 8436
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1690 0 0 0 38980 16 0 0 25 0 1 0 421249285 8638464 1629 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1629 603 41 0 2068 0
vsize: 8436
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1694 0 0 0 39980 17 0 0 25 0 1 0 421249285 8638464 1633 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1633 603 41 0 2068 0
vsize: 8436
[startup+410.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1694 0 0 0 40979 17 0 0 25 0 1 0 421249285 8638464 1633 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1633 603 41 0 2068 0
vsize: 8436
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1694 0 0 0 41979 17 0 0 25 0 1 0 421249285 8638464 1633 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1633 603 41 0 2068 0
vsize: 8436
[startup+430.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1695 0 0 0 42978 18 0 0 25 0 1 0 421249285 8638464 1634 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1695 0 0 0 43978 18 0 0 25 0 1 0 421249285 8638464 1634 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+450.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1695 0 0 0 44977 19 0 0 25 0 1 0 421249285 8638464 1634 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+460.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1695 0 0 0 45977 19 0 0 25 0 1 0 421249285 8638464 1634 4294967295 134512640 134672761 3221224576 3221223700 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1695 0 0 0 46977 20 0 0 25 0 1 0 421249285 8638464 1634 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+480.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1697 0 0 0 47976 20 0 0 25 0 1 0 421249285 8638464 1636 4294967295 134512640 134672761 3221224576 3221223712 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1636 603 41 0 2068 0
vsize: 8436
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1697 0 0 0 48976 20 0 0 25 0 1 0 421249285 8638464 1636 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1636 603 41 0 2068 0
vsize: 8436
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1701 0 0 0 49975 21 0 0 25 0 1 0 421249285 8638464 1640 4294967295 134512640 134672761 3221224576 3221223760 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1701 0 0 0 50975 21 0 0 25 0 1 0 421249285 8638464 1640 4294967295 134512640 134672761 3221224576 3221223744 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+520.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1701 0 0 0 51975 21 0 0 25 0 1 0 421249285 8638464 1640 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+530.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1702 0 0 0 52974 22 0 0 25 0 1 0 421249285 8638464 1641 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1641 603 41 0 2068 0
vsize: 8436
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1702 0 0 0 53974 22 0 0 25 0 1 0 421249285 8638464 1641 4294967295 134512640 134672761 3221224576 3221223712 134565054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1641 603 41 0 2068 0
vsize: 8436
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1706 0 0 0 54974 22 0 0 25 0 1 0 421249285 8638464 1645 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1645 603 41 0 2068 0
vsize: 8436
[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1709 0 0 0 55973 23 0 0 25 0 1 0 421249285 8638464 1648 4294967295 134512640 134672761 3221224576 3221223760 134559159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1648 603 41 0 2068 0
vsize: 8436
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1734 0 0 0 56972 23 0 0 25 0 1 0 421249285 8785920 1673 4294967295 134512640 134672761 3221224576 3221223680 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2145 1673 603 41 0 2104 0
vsize: 8580
[startup+580.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1761 0 0 0 57972 23 0 0 25 0 1 0 421249285 8921088 1700 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2178 1700 603 41 0 2137 0
vsize: 8712
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1761 0 0 0 58972 24 0 0 25 0 1 0 421249285 8921088 1700 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2178 1700 603 41 0 2137 0
vsize: 8712
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1770 0 0 0 59971 24 0 0 25 0 1 0 421249285 8921088 1709 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2178 1709 603 41 0 2137 0
vsize: 8712
[startup+610.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1771 0 0 0 60971 25 0 0 25 0 1 0 421249285 8921088 1710 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2178 1710 603 41 0 2137 0
vsize: 8712
[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1783 0 0 0 61970 25 0 0 25 0 1 0 421249285 8921088 1722 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2178 1722 603 41 0 2137 0
vsize: 8712
[startup+630.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1792 0 0 0 62970 26 0 0 25 0 1 0 421249285 9105408 1731 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1731 603 41 0 2182 0
vsize: 8892
[startup+640.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1792 0 0 0 63970 26 0 0 25 0 1 0 421249285 9105408 1731 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1731 603 41 0 2182 0
vsize: 8892
[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1792 0 0 0 64970 26 0 0 25 0 1 0 421249285 9105408 1731 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1731 603 41 0 2182 0
vsize: 8892
[startup+660.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1793 0 0 0 65969 26 0 0 25 0 1 0 421249285 9105408 1732 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1732 603 41 0 2182 0
vsize: 8892
[startup+670.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1794 0 0 0 66969 26 0 0 25 0 1 0 421249285 9105408 1733 4294967295 134512640 134672761 3221224576 3221223712 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1733 603 41 0 2182 0
vsize: 8892
[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1795 0 0 0 67969 26 0 0 25 0 1 0 421249285 9105408 1734 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1734 603 41 0 2182 0
vsize: 8892
[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1796 0 0 0 68969 27 0 0 25 0 1 0 421249285 9105408 1735 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1735 603 41 0 2182 0
vsize: 8892
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1796 0 0 0 69968 27 0 0 25 0 1 0 421249285 9105408 1735 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1735 603 41 0 2182 0
vsize: 8892
[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1798 0 0 0 70968 27 0 0 25 0 1 0 421249285 9105408 1737 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1737 603 41 0 2182 0
vsize: 8892
[startup+720.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1808 0 0 0 71967 28 0 0 25 0 1 0 421249285 9105408 1747 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1808 0 0 0 72967 28 0 0 25 0 1 0 421249285 9105408 1747 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+740.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1808 0 0 0 73967 28 0 0 25 0 1 0 421249285 9105408 1747 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+750.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1808 0 0 0 74966 29 0 0 25 0 1 0 421249285 9105408 1747 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+760.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1814 0 0 0 75966 29 0 0 25 0 1 0 421249285 9105408 1753 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+770.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1814 0 0 0 76965 29 0 0 25 0 1 0 421249285 9105408 1753 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+780.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1814 0 0 0 77965 30 0 0 25 0 1 0 421249285 9105408 1753 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1814 0 0 0 78965 30 0 0 25 0 1 0 421249285 9105408 1753 4294967295 134512640 134672761 3221224576 3221223776 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+800.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1814 0 0 0 79964 30 0 0 25 0 1 0 421249285 9105408 1753 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+810.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1814 0 0 0 80964 30 0 0 25 0 1 0 421249285 9105408 1753 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1814 0 0 0 81964 31 0 0 25 0 1 0 421249285 9105408 1753 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+830.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1814 0 0 0 82963 31 0 0 25 0 1 0 421249285 9105408 1753 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+840.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1814 0 0 0 83963 31 0 0 25 0 1 0 421249285 9105408 1753 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+850.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1824 0 0 0 84963 31 0 0 25 0 1 0 421249285 9269248 1763 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1763 603 41 0 2222 0
vsize: 9052
[startup+860.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1825 0 0 0 85963 31 0 0 25 0 1 0 421249285 9269248 1764 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+870.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1825 0 0 0 86962 32 0 0 25 0 1 0 421249285 9269248 1764 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+880.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1825 0 0 0 87962 32 0 0 25 0 1 0 421249285 9269248 1764 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+890.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1851 0 0 0 88962 32 0 0 25 0 1 0 421249285 9269248 1790 4294967295 134512640 134672761 3221224576 3221223744 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1790 603 41 0 2222 0
vsize: 9052
[startup+900.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1858 0 0 0 89961 33 0 0 25 0 1 0 421249285 9404416 1797 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1797 603 41 0 2255 0
vsize: 9184
[startup+910.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1864 0 0 0 90961 33 0 0 25 0 1 0 421249285 9404416 1803 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1803 603 41 0 2255 0
vsize: 9184
[startup+920.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1873 0 0 0 91961 33 0 0 25 0 1 0 421249285 9404416 1812 4294967295 134512640 134672761 3221224576 3221223744 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1812 603 41 0 2255 0
vsize: 9184
[startup+930.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1874 0 0 0 92960 33 0 0 25 0 1 0 421249285 9404416 1813 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1813 603 41 0 2255 0
vsize: 9184
[startup+940.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1874 0 0 0 93960 34 0 0 25 0 1 0 421249285 9404416 1813 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1813 603 41 0 2255 0
vsize: 9184
[startup+950.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1874 0 0 0 94959 34 0 0 25 0 1 0 421249285 9404416 1813 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1813 603 41 0 2255 0
vsize: 9184
[startup+960.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1883 0 0 0 95959 35 0 0 25 0 1 0 421249285 9404416 1822 4294967295 134512640 134672761 3221224576 3221223680 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+970.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1883 0 0 0 96958 35 0 0 25 0 1 0 421249285 9404416 1822 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+980.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1883 0 0 0 97958 35 0 0 25 0 1 0 421249285 9404416 1822 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+990.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1883 0 0 0 98957 36 0 0 25 0 1 0 421249285 9404416 1822 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1883 0 0 0 99957 37 0 0 25 0 1 0 421249285 9404416 1822 4294967295 134512640 134672761 3221224576 3221223680 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1883 0 0 0 100957 37 0 0 25 0 1 0 421249285 9404416 1822 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1883 0 0 0 101956 37 0 0 25 0 1 0 421249285 9404416 1822 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1883 0 0 0 102956 37 0 0 25 0 1 0 421249285 9404416 1822 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1883 0 0 0 103955 38 0 0 25 0 1 0 421249285 9404416 1822 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1889 0 0 0 104955 38 0 0 25 0 1 0 421249285 9543680 1828 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1828 603 41 0 2289 0
vsize: 9320
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1899 0 0 0 105955 38 0 0 25 0 1 0 421249285 9543680 1838 4294967295 134512640 134672761 3221224576 3221223776 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1838 603 41 0 2289 0
vsize: 9320
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1899 0 0 0 106954 39 0 0 25 0 1 0 421249285 9543680 1838 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1838 603 41 0 2289 0
vsize: 9320
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1900 0 0 0 107954 39 0 0 25 0 1 0 421249285 9543680 1839 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1839 603 41 0 2289 0
vsize: 9320
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1900 0 0 0 108954 39 0 0 25 0 1 0 421249285 9543680 1839 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1839 603 41 0 2289 0
vsize: 9320
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1900 0 0 0 109954 39 0 0 25 0 1 0 421249285 9543680 1839 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1839 603 41 0 2289 0
vsize: 9320
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1910 0 0 0 110953 40 0 0 25 0 1 0 421249285 9543680 1849 4294967295 134512640 134672761 3221224576 3221223744 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1849 603 41 0 2289 0
vsize: 9320
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1911 0 0 0 111953 40 0 0 25 0 1 0 421249285 9543680 1850 4294967295 134512640 134672761 3221224576 3221223712 134560686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1911 0 0 0 112953 40 0 0 25 0 1 0 421249285 9543680 1850 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1911 0 0 0 113952 41 0 0 25 0 1 0 421249285 9543680 1850 4294967295 134512640 134672761 3221224576 3221223776 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1911 0 0 0 114952 41 0 0 25 0 1 0 421249285 9543680 1850 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1913 0 0 0 115952 41 0 0 25 0 1 0 421249285 9682944 1852 4294967295 134512640 134672761 3221224576 3221223760 134558547 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2364 1852 603 41 0 2323 0
vsize: 9456
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1913 0 0 0 116951 41 0 0 25 0 1 0 421249285 9682944 1852 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2364 1852 603 41 0 2323 0
vsize: 9456
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1922 0 0 0 117951 42 0 0 25 0 1 0 421249285 9682944 1861 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2364 1861 603 41 0 2323 0
vsize: 9456
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1922 0 0 0 118950 42 0 0 25 0 1 0 421249285 9682944 1861 4294967295 134512640 134672761 3221224576 3221223776 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2364 1861 603 41 0 2323 0
vsize: 9456
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1932 0 0 0 119950 43 0 0 25 0 1 0 421249285 9682944 1871 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2364 1871 603 41 0 2323 0
vsize: 9456
[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9469
Raw data (stat): 9469 (minisat+) R 9468 5897 5896 0 -1 0 1933 0 0 0 120950 43 0 0 25 0 1 0 421249285 9682944 1872 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2364 1872 603 41 0 2323 0
vsize: 9456
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 9469
Raw data (stat): 9469 (minisat+) Z 9468 5897 5896 0 -1 12 1935 0 0 0 120950 43 0 0 25 0 1 0 421249285 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): 1210.07
CPU time (s): 1209.94
CPU user time (s): 1209.5
CPU system time (s): 0.439933
CPU usage (%): 99.9892
Max. virtual memory (Kb): 9456
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####