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 4980

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        916576 kB
Buffers:         36648 kB
Cached:          62088 kB
SwapCached:          0 kB
Active:          72460 kB
Inactive:        29152 kB
HighTotal:      131008 kB
HighFree:        65044 kB
LowTotal:       903652 kB
LowFree:        851532 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10944 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:24:17 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 1886 7 1200.18 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.90 0.98 0.91 2/54 25409
Raw data (stat): 25409 (runsolver) R 25408 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420829916 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0006 s]
Raw data (loadavg): 0.91 0.98 0.91 2/54 25409
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1253 0 0 0 995 3 0 0 25 0 1 0 420829916 6541312 1192 4294967295 134512640 134672761 3221224640 3221223800 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1597 1192 603 41 0 1556 0
vsize: 6388
[startup+20.0011 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 25409
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1254 0 0 0 1995 3 0 0 25 0 1 0 420829916 6545408 1193 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.0012 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 25409
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1254 0 0 0 2994 3 0 0 25 0 1 0 420829916 6545408 1193 4294967295 134512640 134672761 3221224640 3221223808 134560830 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.0015 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 25409
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1258 0 0 0 3993 4 0 0 25 0 1 0 420829916 6684672 1197 4294967295 134512640 134672761 3221224640 3221223824 134558537 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.0018 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 25409
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1318 0 0 0 4993 4 0 0 25 0 1 0 420829916 6828032 1257 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1667 1257 603 41 0 1626 0
vsize: 6668
[startup+60.0018 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 25409
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1332 0 0 0 5993 4 0 0 25 0 1 0 420829916 6963200 1271 4294967295 134512640 134672761 3221224640 3221223808 134560830 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.0021 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1373 0 0 0 6993 4 0 0 25 0 1 0 420829916 7098368 1312 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1312 603 41 0 1692 0
vsize: 6932
[startup+80.0017 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1387 0 0 0 7993 5 0 0 25 0 1 0 420829916 7233536 1326 4294967295 134512640 134672761 3221224640 3221223640 1075349771 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.0013 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1393 0 0 0 8993 5 0 0 25 0 1 0 420829916 7233536 1332 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.98 0.91 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1403 0 0 0 9993 5 0 0 25 0 1 0 420829916 7233536 1342 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1766 1342 603 41 0 1725 0
vsize: 7064
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1447 0 0 0 10992 5 0 0 25 0 1 0 420829916 7512064 1386 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1386 603 41 0 1793 0
vsize: 7336
[startup+120.004 s]
Raw data (loadavg): 0.98 0.98 0.91 3/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1450 0 0 0 11992 5 0 0 25 0 1 0 420829916 7512064 1389 4294967295 134512640 134672761 3221224640 3221223808 134560885 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): 1.07 1.00 0.92 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1459 0 0 0 12992 5 0 0 25 0 1 0 420829916 7512064 1398 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1398 603 41 0 1793 0
vsize: 7336
[startup+140.003 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1460 0 0 0 13992 5 0 0 25 0 1 0 420829916 7512064 1399 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1834 1399 603 41 0 1793 0
vsize: 7336
[startup+150.008 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1467 0 0 0 14993 5 0 0 25 0 1 0 420829916 7512064 1406 4294967295 134512640 134672761 3221224640 3221223808 134560869 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.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1513 0 0 0 15993 5 0 0 25 0 1 0 420829916 7811072 1452 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.008 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1522 0 0 0 16993 5 0 0 25 0 1 0 420829916 7811072 1461 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1907 1461 603 41 0 1866 0
vsize: 7628
[startup+180.008 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1547 0 0 0 17993 5 0 0 25 0 1 0 420829916 7942144 1486 4294967295 134512640 134672761 3221224640 3221223776 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1486 603 41 0 1898 0
vsize: 7756
[startup+190.009 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1558 0 0 0 18993 5 0 0 25 0 1 0 420829916 7942144 1497 4294967295 134512640 134672761 3221224640 3221223808 134561188 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.008 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1565 0 0 0 19994 5 0 0 25 0 1 0 420829916 7942144 1504 4294967295 134512640 134672761 3221224640 3221223808 134559131 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.008 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1571 0 0 0 20994 5 0 0 25 0 1 0 420829916 7942144 1510 4294967295 134512640 134672761 3221224640 3221223840 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1510 603 41 0 1898 0
vsize: 7756
[startup+220.008 s]
Raw data (loadavg): 1.09 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1572 0 0 0 21994 5 0 0 25 0 1 0 420829916 7942144 1511 4294967295 134512640 134672761 3221224640 3221223808 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.007 s]
Raw data (loadavg): 1.15 1.03 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1579 0 0 0 22994 5 0 0 25 0 1 0 420829916 8105984 1518 4294967295 134512640 134672761 3221224640 3221223808 134561406 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.008 s]
Raw data (loadavg): 1.13 1.03 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1582 0 0 0 23994 5 0 0 25 0 1 0 420829916 8105984 1521 4294967295 134512640 134672761 3221224640 3221223776 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1979 1521 603 41 0 1938 0
vsize: 7916
[startup+250.008 s]
Raw data (loadavg): 1.11 1.03 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1631 0 0 0 24994 6 0 0 25 0 1 0 420829916 8364032 1570 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2042 1570 603 41 0 2001 0
vsize: 8168
[startup+260.008 s]
Raw data (loadavg): 1.09 1.03 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1639 0 0 0 25994 6 0 0 25 0 1 0 420829916 8364032 1578 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2042 1578 603 41 0 2001 0
vsize: 8168
[startup+270.008 s]
Raw data (loadavg): 1.08 1.03 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1648 0 0 0 26994 6 0 0 25 0 1 0 420829916 8503296 1587 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1587 603 41 0 2035 0
vsize: 8304
[startup+280.008 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1651 0 0 0 27995 6 0 0 25 0 1 0 420829916 8503296 1590 4294967295 134512640 134672761 3221224640 3221223840 134557830 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.008 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1654 0 0 0 28995 6 0 0 25 0 1 0 420829916 8503296 1593 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1593 603 41 0 2035 0
vsize: 8304
[startup+300.008 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1657 0 0 0 29994 6 0 0 25 0 1 0 420829916 8503296 1596 4294967295 134512640 134672761 3221224640 3221223808 134560869 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.009 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1657 0 0 0 30994 6 0 0 25 0 1 0 420829916 8503296 1596 4294967295 134512640 134672761 3221224640 3221223808 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+320.008 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1662 0 0 0 31994 6 0 0 25 0 1 0 420829916 8503296 1601 4294967295 134512640 134672761 3221224640 3221223808 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1601 603 41 0 2035 0
vsize: 8304
[startup+330.008 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1670 0 0 0 32994 6 0 0 25 0 1 0 420829916 8503296 1609 4294967295 134512640 134672761 3221224640 3221223744 134554662 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.008 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1671 0 0 0 33994 6 0 0 25 0 1 0 420829916 8503296 1610 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1610 603 41 0 2035 0
vsize: 8304
[startup+350.008 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1673 0 0 0 34994 6 0 0 25 0 1 0 420829916 8503296 1612 4294967295 134512640 134672761 3221224640 3221223808 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+360.009 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1673 0 0 0 35995 6 0 0 25 0 1 0 420829916 8503296 1612 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1612 603 41 0 2035 0
vsize: 8304
[startup+370.008 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1674 0 0 0 36995 6 0 0 25 0 1 0 420829916 8503296 1613 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1613 603 41 0 2035 0
vsize: 8304
[startup+380.008 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1674 0 0 0 37995 6 0 0 25 0 1 0 420829916 8503296 1613 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2076 1613 603 41 0 2035 0
vsize: 8304
[startup+390.008 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1690 0 0 0 38995 6 0 0 25 0 1 0 420829916 8638464 1629 4294967295 134512640 134672761 3221224640 3221223808 134561264 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.008 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1690 0 0 0 39995 6 0 0 25 0 1 0 420829916 8638464 1629 4294967295 134512640 134672761 3221224640 3221223808 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+410.009 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1694 0 0 0 40995 6 0 0 25 0 1 0 420829916 8638464 1633 4294967295 134512640 134672761 3221224640 3221223808 134560830 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.008 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1694 0 0 0 41995 6 0 0 25 0 1 0 420829916 8638464 1633 4294967295 134512640 134672761 3221224640 3221223808 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+430.008 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1694 0 0 0 42995 6 0 0 25 0 1 0 420829916 8638464 1633 4294967295 134512640 134672761 3221224640 3221223824 134559334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1633 603 41 0 2068 0
vsize: 8436
[startup+440.008 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1695 0 0 0 43996 6 0 0 25 0 1 0 420829916 8638464 1634 4294967295 134512640 134672761 3221224640 3221223776 134560661 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.008 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1695 0 0 0 44996 6 0 0 25 0 1 0 420829916 8638464 1634 4294967295 134512640 134672761 3221224640 3221223808 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+460.009 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1695 0 0 0 45996 6 0 0 25 0 1 0 420829916 8638464 1634 4294967295 134512640 134672761 3221224640 3221223744 134559943 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.01 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1695 0 0 0 46996 7 0 0 25 0 1 0 420829916 8638464 1634 4294967295 134512640 134672761 3221224640 3221223808 134560869 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.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1697 0 0 0 47996 7 0 0 25 0 1 0 420829916 8638464 1636 4294967295 134512640 134672761 3221224640 3221223808 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+490.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1697 0 0 0 48996 7 0 0 25 0 1 0 420829916 8638464 1636 4294967295 134512640 134672761 3221224640 3221223840 134557897 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.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1701 0 0 0 49997 7 0 0 25 0 1 0 420829916 8638464 1640 4294967295 134512640 134672761 3221224640 3221223808 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+510.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1701 0 0 0 50997 7 0 0 25 0 1 0 420829916 8638464 1640 4294967295 134512640 134672761 3221224640 3221223776 134560566 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.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1701 0 0 0 51997 7 0 0 25 0 1 0 420829916 8638464 1640 4294967295 134512640 134672761 3221224640 3221223808 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+530.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1702 0 0 0 52997 7 0 0 25 0 1 0 420829916 8638464 1641 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1702 0 0 0 53997 7 0 0 25 0 1 0 420829916 8638464 1641 4294967295 134512640 134672761 3221224640 3221223840 134557836 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.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1702 0 0 0 54997 7 0 0 25 0 1 0 420829916 8638464 1641 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2109 1641 603 41 0 2068 0
vsize: 8436
[startup+560.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1706 0 0 0 55998 7 0 0 25 0 1 0 420829916 8638464 1645 4294967295 134512640 134672761 3221224640 3221223808 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+570.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1709 0 0 0 56998 7 0 0 25 0 1 0 420829916 8638464 1648 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2109 1648 603 41 0 2068 0
vsize: 8436
[startup+580.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1761 0 0 0 57997 7 0 0 25 0 1 0 420829916 8921088 1700 4294967295 134512640 134672761 3221224640 3221223840 134557913 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.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1761 0 0 0 58997 7 0 0 25 0 1 0 420829916 8921088 1700 4294967295 134512640 134672761 3221224640 3221223824 134558700 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.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1766 0 0 0 59997 7 0 0 25 0 1 0 420829916 8921088 1705 4294967295 134512640 134672761 3221224640 3221223792 134541828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1705 603 41 0 2137 0
vsize: 8712
[startup+610.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1770 0 0 0 60998 7 0 0 25 0 1 0 420829916 8921088 1709 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1709 603 41 0 2137 0
vsize: 8712
[startup+620.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1783 0 0 0 61998 7 0 0 25 0 1 0 420829916 8921088 1722 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1783 0 0 0 62998 7 0 0 25 0 1 0 420829916 8921088 1722 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2178 1722 603 41 0 2137 0
vsize: 8712
[startup+640.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1792 0 0 0 63998 8 0 0 25 0 1 0 420829916 9105408 1731 4294967295 134512640 134672761 3221224640 3221223744 134554642 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.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1792 0 0 0 64998 8 0 0 25 0 1 0 420829916 9105408 1731 4294967295 134512640 134672761 3221224640 3221223808 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+660.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1793 0 0 0 65998 8 0 0 25 0 1 0 420829916 9105408 1732 4294967295 134512640 134672761 3221224640 3221223744 134560196 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.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1793 0 0 0 66998 8 0 0 25 0 1 0 420829916 9105408 1732 4294967295 134512640 134672761 3221224640 3221223808 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+680.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1795 0 0 0 67999 8 0 0 25 0 1 0 420829916 9105408 1734 4294967295 134512640 134672761 3221224640 3221223824 134558690 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.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1795 0 0 0 68999 8 0 0 25 0 1 0 420829916 9105408 1734 4294967295 134512640 134672761 3221224640 3221223808 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1734 603 41 0 2182 0
vsize: 8892
[startup+700.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1796 0 0 0 69999 8 0 0 25 0 1 0 420829916 9105408 1735 4294967295 134512640 134672761 3221224640 3221223808 134561193 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.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1797 0 0 0 70999 8 0 0 25 0 1 0 420829916 9105408 1736 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1736 603 41 0 2182 0
vsize: 8892
[startup+720.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1799 0 0 0 71999 8 0 0 25 0 1 0 420829916 9105408 1738 4294967295 134512640 134672761 3221224640 3221223824 134559514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1738 603 41 0 2182 0
vsize: 8892
[startup+730.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1808 0 0 0 73000 8 0 0 25 0 1 0 420829916 9105408 1747 4294967295 134512640 134672761 3221224640 3221223824 134559161 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.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1808 0 0 0 74000 8 0 0 25 0 1 0 420829916 9105408 1747 4294967295 134512640 134672761 3221224640 3221223808 134560855 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.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1808 0 0 0 75000 8 0 0 25 0 1 0 420829916 9105408 1747 4294967295 134512640 134672761 3221224640 3221223808 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+760.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1808 0 0 0 76000 8 0 0 25 0 1 0 420829916 9105408 1747 4294967295 134512640 134672761 3221224640 3221223808 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+770.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1814 0 0 0 77000 8 0 0 25 0 1 0 420829916 9105408 1753 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1814 0 0 0 78000 8 0 0 25 0 1 0 420829916 9105408 1753 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1814 0 0 0 79001 8 0 0 25 0 1 0 420829916 9105408 1753 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1814 0 0 0 80001 8 0 0 25 0 1 0 420829916 9105408 1753 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1814 0 0 0 81001 8 0 0 25 0 1 0 420829916 9105408 1753 4294967295 134512640 134672761 3221224640 3221223840 134557911 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.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1814 0 0 0 82001 8 0 0 25 0 1 0 420829916 9105408 1753 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1814 0 0 0 83001 8 0 0 25 0 1 0 420829916 9105408 1753 4294967295 134512640 134672761 3221224640 3221223808 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.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1814 0 0 0 84002 8 0 0 25 0 1 0 420829916 9105408 1753 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2223 1753 603 41 0 2182 0
vsize: 8892
[startup+850.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1823 0 0 0 85002 8 0 0 25 0 1 0 420829916 9269248 1762 4294967295 134512640 134672761 3221224640 3221223744 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1762 603 41 0 2222 0
vsize: 9052
[startup+860.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1825 0 0 0 86002 8 0 0 25 0 1 0 420829916 9269248 1764 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1825 0 0 0 87002 8 0 0 25 0 1 0 420829916 9269248 1764 4294967295 134512640 134672761 3221224640 3221223776 134560706 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1825 0 0 0 88003 8 0 0 25 0 1 0 420829916 9269248 1764 4294967295 134512640 134672761 3221224640 3221223808 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1825 0 0 0 89002 8 0 0 25 0 1 0 420829916 9269248 1764 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1764 603 41 0 2222 0
vsize: 9052
[startup+900.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1851 0 0 0 90002 8 0 0 25 0 1 0 420829916 9269248 1790 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2263 1790 603 41 0 2222 0
vsize: 9052
[startup+910.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1859 0 0 0 91002 8 0 0 25 0 1 0 420829916 9404416 1798 4294967295 134512640 134672761 3221224640 3221223744 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1798 603 41 0 2255 0
vsize: 9184
[startup+920.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1873 0 0 0 92002 8 0 0 25 0 1 0 420829916 9404416 1812 4294967295 134512640 134672761 3221224640 3221223744 134554665 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1873 0 0 0 93002 8 0 0 25 0 1 0 420829916 9404416 1812 4294967295 134512640 134672761 3221224640 3221223808 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+940.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1874 0 0 0 94003 8 0 0 25 0 1 0 420829916 9404416 1813 4294967295 134512640 134672761 3221224640 3221223808 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+950.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1874 0 0 0 95003 8 0 0 25 0 1 0 420829916 9404416 1813 4294967295 134512640 134672761 3221224640 3221223808 134560825 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.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1874 0 0 0 96003 8 0 0 25 0 1 0 420829916 9404416 1813 4294967295 134512640 134672761 3221224640 3221223808 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+970.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1883 0 0 0 97003 8 0 0 25 0 1 0 420829916 9404416 1822 4294967295 134512640 134672761 3221224640 3221223808 134560942 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.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1883 0 0 0 98003 8 0 0 25 0 1 0 420829916 9404416 1822 4294967295 134512640 134672761 3221224640 3221223808 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+990.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1883 0 0 0 99003 8 0 0 25 0 1 0 420829916 9404416 1822 4294967295 134512640 134672761 3221224640 3221223808 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1883 0 0 0 100004 8 0 0 25 0 1 0 420829916 9404416 1822 4294967295 134512640 134672761 3221224640 3221223808 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+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1883 0 0 0 101004 8 0 0 25 0 1 0 420829916 9404416 1822 4294967295 134512640 134672761 3221224640 3221223808 134560830 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1883 0 0 0 102004 8 0 0 25 0 1 0 420829916 9404416 1822 4294967295 134512640 134672761 3221224640 3221223824 134558557 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1883 0 0 0 103004 8 0 0 25 0 1 0 420829916 9404416 1822 4294967295 134512640 134672761 3221224640 3221223808 134561218 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1883 0 0 0 104004 8 0 0 25 0 1 0 420829916 9404416 1822 4294967295 134512640 134672761 3221224640 3221223808 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+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1883 0 0 0 105005 8 0 0 25 0 1 0 420829916 9404416 1822 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2296 1822 603 41 0 2255 0
vsize: 9184
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1889 0 0 0 106005 8 0 0 25 0 1 0 420829916 9543680 1828 4294967295 134512640 134672761 3221224640 3221223776 134565130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1828 603 41 0 2289 0
vsize: 9320
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1899 0 0 0 107005 8 0 0 25 0 1 0 420829916 9543680 1838 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1899 0 0 0 108005 8 0 0 25 0 1 0 420829916 9543680 1838 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1838 603 41 0 2289 0
vsize: 9320
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1900 0 0 0 109005 8 0 0 25 0 1 0 420829916 9543680 1839 4294967295 134512640 134672761 3221224640 3221223808 134560898 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1900 0 0 0 110005 8 0 0 25 0 1 0 420829916 9543680 1839 4294967295 134512640 134672761 3221224640 3221223808 134560839 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.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1900 0 0 0 111006 8 0 0 25 0 1 0 420829916 9543680 1839 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1839 603 41 0 2289 0
vsize: 9320
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1910 0 0 0 112006 8 0 0 25 0 1 0 420829916 9543680 1849 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1849 603 41 0 2289 0
vsize: 9320
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1911 0 0 0 113006 8 0 0 25 0 1 0 420829916 9543680 1850 4294967295 134512640 134672761 3221224640 3221223764 134566089 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.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1911 0 0 0 114006 8 0 0 25 0 1 0 420829916 9543680 1850 4294967295 134512640 134672761 3221224640 3221223808 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.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1911 0 0 0 115007 8 0 0 25 0 1 0 420829916 9543680 1850 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1911 0 0 0 116007 8 0 0 25 0 1 0 420829916 9543680 1850 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2330 1850 603 41 0 2289 0
vsize: 9320
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1913 0 0 0 117007 8 0 0 25 0 1 0 420829916 9682944 1852 4294967295 134512640 134672761 3221224640 3221223764 134566031 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.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1913 0 0 0 118007 8 0 0 25 0 1 0 420829916 9682944 1852 4294967295 134512640 134672761 3221224640 3221223808 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+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1922 0 0 0 119007 8 0 0 25 0 1 0 420829916 9682944 1861 4294967295 134512640 134672761 3221224640 3221223808 134560830 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.00 1.00 0.93 2/54 25411
Raw data (stat): 25409 (minisat+) R 25408 22932 22931 0 -1 0 1922 0 0 0 120007 9 0 0 25 0 1 0 420829916 9682944 1861 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2364 1861 603 41 0 2323 0
vsize: 9456
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 25411
Raw data (stat): 25409 (minisat+) Z 25408 22932 22931 0 -1 12 1924 0 0 0 120007 9 0 0 25 0 1 0 420829916 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.18
CPU user time (s): 1200.08
CPU system time (s): 0.096985
CPU usage (%): 100.013
Max. virtual memory (Kb): 9456
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####