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 5953

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 02:22:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4346 boxname=wulflinc17 idbench=210 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4ad922a0ad53056b410be6ab5caa6b5b  /oldhome/oroussel/tmp/wulflinc17/normalized-par32-4.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc17/normalized-par32-4.opb /oldhome/oroussel/tmp/wulflinc17/normalized-par32-4.opb
IDLAUNCH: 4346
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        822000 kB
Buffers:         35932 kB
Cached:         141892 kB
SwapCached:       2376 kB
Active:          59124 kB
Inactive:       124052 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        821748 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23788 kB
Committed_AS:    63700 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:42:07 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 4346 7 1200.17 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.92 0.97 0.91 2/55 27895
Raw data (stat): 27895 (runsolver) R 27894 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480961563 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.001 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1253 0 0 0 994 3 0 0 25 0 1 0 480961563 6541312 1192 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1597 1192 603 41 0 1556 0
vsize: 6388
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1254 0 0 0 1994 3 0 0 25 0 1 0 480961563 6545408 1193 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1598 1193 603 41 0 1557 0
vsize: 6392
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1254 0 0 0 2994 3 0 0 25 0 1 0 480961563 6545408 1193 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1598 1193 603 41 0 1557 0
vsize: 6392
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1258 0 0 0 3994 3 0 0 25 0 1 0 480961563 6684672 1197 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1632 1197 603 41 0 1591 0
vsize: 6528
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1319 0 0 0 4994 4 0 0 25 0 1 0 480961563 6828032 1258 4294967295 134512640 134672761 3221224560 3221223744 134558878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1667 1258 603 41 0 1626 0
vsize: 6668
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1332 0 0 0 5994 4 0 0 25 0 1 0 480961563 6963200 1271 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1700 1271 603 41 0 1659 0
vsize: 6800
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1373 0 0 0 6993 4 0 0 25 0 1 0 480961563 7098368 1312 4294967295 134512640 134672761 3221224560 3221223720 134565155 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.0023 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1387 0 0 0 7993 4 0 0 25 0 1 0 480961563 7233536 1326 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1766 1326 603 41 0 1725 0
vsize: 7064
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1393 0 0 0 8993 4 0 0 25 0 1 0 480961563 7233536 1332 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1766 1332 603 41 0 1725 0
vsize: 7064
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1404 0 0 0 9992 5 0 0 25 0 1 0 480961563 7233536 1343 4294967295 134512640 134672761 3221224560 3221223696 134565096 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.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1447 0 0 0 10992 5 0 0 25 0 1 0 480961563 7512064 1386 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1450 0 0 0 11991 5 0 0 25 0 1 0 480961563 7512064 1389 4294967295 134512640 134672761 3221224560 3221223744 134558700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1389 603 41 0 1793 0
vsize: 7336
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1460 0 0 0 12991 5 0 0 25 0 1 0 480961563 7512064 1399 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1399 603 41 0 1793 0
vsize: 7336
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1465 0 0 0 13992 5 0 0 25 0 1 0 480961563 7512064 1404 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1404 603 41 0 1793 0
vsize: 7336
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1467 0 0 0 14992 5 0 0 25 0 1 0 480961563 7512064 1406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1406 603 41 0 1793 0
vsize: 7336
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1513 0 0 0 15992 5 0 0 25 0 1 0 480961563 7811072 1452 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1907 1452 603 41 0 1866 0
vsize: 7628
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1532 0 0 0 16992 5 0 0 25 0 1 0 480961563 7811072 1471 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1907 1471 603 41 0 1866 0
vsize: 7628
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1549 0 0 0 17992 5 0 0 25 0 1 0 480961563 7942144 1488 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1488 603 41 0 1898 0
vsize: 7756
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1558 0 0 0 18992 5 0 0 25 0 1 0 480961563 7942144 1497 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1497 603 41 0 1898 0
vsize: 7756
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27895
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1565 0 0 0 19992 6 0 0 25 0 1 0 480961563 7942144 1504 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1504 603 41 0 1898 0
vsize: 7756
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1572 0 0 0 20993 6 0 0 25 0 1 0 480961563 7942144 1511 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1511 603 41 0 1898 0
vsize: 7756
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1572 0 0 0 21993 6 0 0 25 0 1 0 480961563 7942144 1511 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1511 603 41 0 1898 0
vsize: 7756
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1579 0 0 0 22993 6 0 0 25 0 1 0 480961563 8105984 1518 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1979 1518 603 41 0 1938 0
vsize: 7916
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1595 0 0 0 23993 6 0 0 25 0 1 0 480961563 8105984 1534 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1979 1534 603 41 0 1938 0
vsize: 7916
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1636 0 0 0 24993 6 0 0 25 0 1 0 480961563 8364032 1575 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2042 1575 603 41 0 2001 0
vsize: 8168
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1642 0 0 0 25993 6 0 0 25 0 1 0 480961563 8364032 1581 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2042 1581 603 41 0 2001 0
vsize: 8168
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1650 0 0 0 26994 6 0 0 25 0 1 0 480961563 8503296 1589 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1589 603 41 0 2035 0
vsize: 8304
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1651 0 0 0 27994 6 0 0 25 0 1 0 480961563 8503296 1590 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1590 603 41 0 2035 0
vsize: 8304
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1656 0 0 0 28994 6 0 0 25 0 1 0 480961563 8503296 1595 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1595 603 41 0 2035 0
vsize: 8304
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1657 0 0 0 29994 6 0 0 25 0 1 0 480961563 8503296 1596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1596 603 41 0 2035 0
vsize: 8304
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1662 0 0 0 30994 6 0 0 25 0 1 0 480961563 8503296 1601 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1601 603 41 0 2035 0
vsize: 8304
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1668 0 0 0 31994 6 0 0 25 0 1 0 480961563 8503296 1607 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1607 603 41 0 2035 0
vsize: 8304
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1670 0 0 0 32994 6 0 0 25 0 1 0 480961563 8503296 1609 4294967295 134512640 134672761 3221224560 3221223696 134565140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1609 603 41 0 2035 0
vsize: 8304
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1673 0 0 0 33995 6 0 0 25 0 1 0 480961563 8503296 1612 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1612 603 41 0 2035 0
vsize: 8304
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1673 0 0 0 34995 6 0 0 25 0 1 0 480961563 8503296 1612 4294967295 134512640 134672761 3221224560 3221223696 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1612 603 41 0 2035 0
vsize: 8304
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1674 0 0 0 35995 6 0 0 25 0 1 0 480961563 8503296 1613 4294967295 134512640 134672761 3221224560 3221223664 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1613 603 41 0 2035 0
vsize: 8304
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1674 0 0 0 36995 6 0 0 25 0 1 0 480961563 8503296 1613 4294967295 134512640 134672761 3221224560 3221223724 134561235 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1690 0 0 0 37994 6 0 0 25 0 1 0 480961563 8638464 1629 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1629 603 41 0 2068 0
vsize: 8436
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1690 0 0 0 38995 6 0 0 25 0 1 0 480961563 8638464 1629 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1629 603 41 0 2068 0
vsize: 8436
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1694 0 0 0 39995 6 0 0 25 0 1 0 480961563 8638464 1633 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1633 603 41 0 2068 0
vsize: 8436
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1694 0 0 0 40995 6 0 0 25 0 1 0 480961563 8638464 1633 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1633 603 41 0 2068 0
vsize: 8436
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1694 0 0 0 41995 6 0 0 25 0 1 0 480961563 8638464 1633 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1633 603 41 0 2068 0
vsize: 8436
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1695 0 0 0 42995 6 0 0 25 0 1 0 480961563 8638464 1634 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1695 0 0 0 43996 6 0 0 25 0 1 0 480961563 8638464 1634 4294967295 134512640 134672761 3221224560 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1695 0 0 0 44996 6 0 0 25 0 1 0 480961563 8638464 1634 4294967295 134512640 134672761 3221224560 3221223712 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1695 0 0 0 45996 6 0 0 25 0 1 0 480961563 8638464 1634 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1695 0 0 0 46996 6 0 0 25 0 1 0 480961563 8638464 1634 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1634 603 41 0 2068 0
vsize: 8436
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1697 0 0 0 47996 6 0 0 25 0 1 0 480961563 8638464 1636 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1636 603 41 0 2068 0
vsize: 8436
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1697 0 0 0 48996 6 0 0 25 0 1 0 480961563 8638464 1636 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1636 603 41 0 2068 0
vsize: 8436
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27897
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1701 0 0 0 49997 6 0 0 25 0 1 0 480961563 8638464 1640 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1701 0 0 0 50997 6 0 0 25 0 1 0 480961563 8638464 1640 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1701 0 0 0 51997 6 0 0 25 0 1 0 480961563 8638464 1640 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1640 603 41 0 2068 0
vsize: 8436
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1702 0 0 0 52997 6 0 0 25 0 1 0 480961563 8638464 1641 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1641 603 41 0 2068 0
vsize: 8436
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1702 0 0 0 53997 7 0 0 25 0 1 0 480961563 8638464 1641 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1641 603 41 0 2068 0
vsize: 8436
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1706 0 0 0 54997 7 0 0 25 0 1 0 480961563 8638464 1645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1645 603 41 0 2068 0
vsize: 8436
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1709 0 0 0 55998 7 0 0 25 0 1 0 480961563 8638464 1648 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1648 603 41 0 2068 0
vsize: 8436
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1745 0 0 0 56997 7 0 0 25 0 1 0 480961563 8785920 1684 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2145 1684 603 41 0 2104 0
vsize: 8580
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1761 0 0 0 57996 7 0 0 25 0 1 0 480961563 8921088 1700 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1700 603 41 0 2137 0
vsize: 8712
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1761 0 0 0 58997 7 0 0 25 0 1 0 480961563 8921088 1700 4294967295 134512640 134672761 3221224560 3221223744 134558497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1700 603 41 0 2137 0
vsize: 8712
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1770 0 0 0 59997 7 0 0 25 0 1 0 480961563 8921088 1709 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1709 603 41 0 2137 0
vsize: 8712
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1771 0 0 0 60997 7 0 0 25 0 1 0 480961563 8921088 1710 4294967295 134512640 134672761 3221224560 3221223684 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1710 603 41 0 2137 0
vsize: 8712
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1783 0 0 0 61997 7 0 0 25 0 1 0 480961563 8921088 1722 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1722 603 41 0 2137 0
vsize: 8712
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1792 0 0 0 62997 8 0 0 25 0 1 0 480961563 9105408 1731 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1731 603 41 0 2182 0
vsize: 8892
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1792 0 0 0 63997 8 0 0 25 0 1 0 480961563 9105408 1731 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1731 603 41 0 2182 0
vsize: 8892
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1793 0 0 0 64997 8 0 0 25 0 1 0 480961563 9105408 1732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1732 603 41 0 2182 0
vsize: 8892
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1793 0 0 0 65998 8 0 0 25 0 1 0 480961563 9105408 1732 4294967295 134512640 134672761 3221224560 3221223684 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1732 603 41 0 2182 0
vsize: 8892
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1794 0 0 0 66998 8 0 0 25 0 1 0 480961563 9105408 1733 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1733 603 41 0 2182 0
vsize: 8892
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1795 0 0 0 67998 8 0 0 25 0 1 0 480961563 9105408 1734 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1734 603 41 0 2182 0
vsize: 8892
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1796 0 0 0 68998 8 0 0 25 0 1 0 480961563 9105408 1735 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1735 603 41 0 2182 0
vsize: 8892
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1796 0 0 0 69998 8 0 0 25 0 1 0 480961563 9105408 1735 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1735 603 41 0 2182 0
vsize: 8892
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1798 0 0 0 70999 8 0 0 25 0 1 0 480961563 9105408 1737 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1737 603 41 0 2182 0
vsize: 8892
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1808 0 0 0 71999 8 0 0 25 0 1 0 480961563 9105408 1747 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1808 0 0 0 72999 8 0 0 25 0 1 0 480961563 9105408 1747 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1808 0 0 0 73999 8 0 0 25 0 1 0 480961563 9105408 1747 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1808 0 0 0 74999 8 0 0 25 0 1 0 480961563 9105408 1747 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1747 603 41 0 2182 0
vsize: 8892
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1814 0 0 0 75999 8 0 0 25 0 1 0 480961563 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1814 0 0 0 76999 8 0 0 25 0 1 0 480961563 9105408 1753 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1814 0 0 0 77999 8 0 0 25 0 1 0 480961563 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1814 0 0 0 79000 8 0 0 25 0 1 0 480961563 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27899
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1814 0 0 0 80000 8 0 0 25 0 1 0 480961563 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1814 0 0 0 81000 8 0 0 25 0 1 0 480961563 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1814 0 0 0 82000 8 0 0 25 0 1 0 480961563 9105408 1753 4294967295 134512640 134672761 3221224560 3221223744 134559342 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1814 0 0 0 83000 8 0 0 25 0 1 0 480961563 9105408 1753 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1823 0 0 0 84001 8 0 0 25 0 1 0 480961563 9269248 1762 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1762 603 41 0 2222 0
vsize: 9052
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1825 0 0 0 85001 8 0 0 25 0 1 0 480961563 9269248 1764 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1825 0 0 0 86001 8 0 0 25 0 1 0 480961563 9269248 1764 4294967295 134512640 134672761 3221224560 3221223744 134558332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1825 0 0 0 87001 8 0 0 25 0 1 0 480961563 9269248 1764 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1825 0 0 0 88001 8 0 0 25 0 1 0 480961563 9269248 1764 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1851 0 0 0 89001 8 0 0 25 0 1 0 480961563 9269248 1790 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1790 603 41 0 2222 0
vsize: 9052
[startup+900.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1859 0 0 0 90001 8 0 0 25 0 1 0 480961563 9404416 1798 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1798 603 41 0 2255 0
vsize: 9184
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1873 0 0 0 91001 9 0 0 25 0 1 0 480961563 9404416 1812 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1812 603 41 0 2255 0
vsize: 9184
[startup+920.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1873 0 0 0 92001 9 0 0 25 0 1 0 480961563 9404416 1812 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1812 603 41 0 2255 0
vsize: 9184
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1874 0 0 0 93002 9 0 0 25 0 1 0 480961563 9404416 1813 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1813 603 41 0 2255 0
vsize: 9184
[startup+940.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1874 0 0 0 94002 9 0 0 25 0 1 0 480961563 9404416 1813 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1813 603 41 0 2255 0
vsize: 9184
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1874 0 0 0 95002 9 0 0 25 0 1 0 480961563 9404416 1813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1813 603 41 0 2255 0
vsize: 9184
[startup+960.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1883 0 0 0 96002 9 0 0 25 0 1 0 480961563 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1883 0 0 0 97002 9 0 0 25 0 1 0 480961563 9404416 1822 4294967295 134512640 134672761 3221224560 3221223696 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+980.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1883 0 0 0 98002 9 0 0 25 0 1 0 480961563 9404416 1822 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+990.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1883 0 0 0 99003 9 0 0 25 0 1 0 480961563 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1883 0 0 0 100003 9 0 0 25 0 1 0 480961563 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1883 0 0 0 101003 9 0 0 25 0 1 0 480961563 9404416 1822 4294967295 134512640 134672761 3221224560 3221223696 134560675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1883 0 0 0 102003 9 0 0 25 0 1 0 480961563 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1883 0 0 0 103003 9 0 0 25 0 1 0 480961563 9404416 1822 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1888 0 0 0 104003 9 0 0 25 0 1 0 480961563 9543680 1827 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1827 603 41 0 2289 0
vsize: 9320
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1889 0 0 0 105003 9 0 0 25 0 1 0 480961563 9543680 1828 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1828 603 41 0 2289 0
vsize: 9320
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1899 0 0 0 106003 9 0 0 25 0 1 0 480961563 9543680 1838 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1838 603 41 0 2289 0
vsize: 9320
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1899 0 0 0 107003 9 0 0 25 0 1 0 480961563 9543680 1838 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1838 603 41 0 2289 0
vsize: 9320
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1900 0 0 0 108004 9 0 0 25 0 1 0 480961563 9543680 1839 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1839 603 41 0 2289 0
vsize: 9320
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1900 0 0 0 109004 9 0 0 25 0 1 0 480961563 9543680 1839 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1839 603 41 0 2289 0
vsize: 9320
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27901
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1900 0 0 0 110004 9 0 0 25 0 1 0 480961563 9543680 1839 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1839 603 41 0 2289 0
vsize: 9320
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27903
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1910 0 0 0 111004 9 0 0 25 0 1 0 480961563 9543680 1849 4294967295 134512640 134672761 3221224560 3221223664 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1849 603 41 0 2289 0
vsize: 9320
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27903
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1911 0 0 0 112004 9 0 0 25 0 1 0 480961563 9543680 1850 4294967295 134512640 134672761 3221224560 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27903
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1911 0 0 0 113005 10 0 0 25 0 1 0 480961563 9543680 1850 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1140.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 27903
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1911 0 0 0 114005 10 0 0 25 0 1 0 480961563 9543680 1850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1150.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 27903
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1913 0 0 0 115005 10 0 0 25 0 1 0 480961563 9682944 1852 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1852 603 41 0 2323 0
vsize: 9456
[startup+1160.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 27903
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1913 0 0 0 116005 10 0 0 25 0 1 0 480961563 9682944 1852 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1852 603 41 0 2323 0
vsize: 9456
[startup+1170.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 27903
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1913 0 0 0 117005 10 0 0 25 0 1 0 480961563 9682944 1852 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1852 603 41 0 2323 0
vsize: 9456
[startup+1180.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 27903
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1922 0 0 0 118005 10 0 0 25 0 1 0 480961563 9682944 1861 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1861 603 41 0 2323 0
vsize: 9456
[startup+1190.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 27903
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1922 0 0 0 119005 10 0 0 25 0 1 0 480961563 9682944 1861 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1861 603 41 0 2323 0
vsize: 9456
[startup+1200.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27903
Raw data (stat): 27895 (minisat+) R 27894 20838 20837 0 -1 0 1933 0 0 0 120006 10 0 0 25 0 1 0 480961563 9682944 1872 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1872 603 41 0 2323 0
vsize: 9456
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.02 0.99 0.91 1/55 27903
Raw data (stat): 27895 (minisat+) Z 27894 20838 20837 0 -1 12 1935 0 0 0 120006 10 0 0 25 0 1 0 480961563 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.02
CPU time (s): 1200.17
CPU user time (s): 1200.06
CPU system time (s): 0.108983
CPU usage (%): 100.012
Max. virtual memory (Kb): 9456
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####