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/logic-synthesis/normalized-count.b.opb
MD5SUM	f13ba9c997276002b5bd6db1f679a6f5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	24
Optimality of the best value was proved	NO
Number of terms in the objective function	467
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	467
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	467
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04584
Number of variables	466
Total number of constraints	694
Number of constraints which are clauses	694
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	2
Maximum length of a constraint	78
Trace number 4660

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-13 19:42:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3449 boxname=wulflinc7 idbench=65 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f13ba9c997276002b5bd6db1f679a6f5  /oldhome/oroussel/tmp/wulflinc7/normalized-count.b.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc7/normalized-count.b.opb /oldhome/oroussel/tmp/wulflinc7/normalized-count.b.opb
IDLAUNCH: 3449
/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:        918852 kB
Buffers:         36568 kB
Cached:          60196 kB
SwapCached:          0 kB
Active:          71992 kB
Inactive:        27628 kB
HighTotal:      131008 kB
HighFree:        66920 kB
LowTotal:       903652 kB
LowFree:        851932 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10760 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:03:06 (client local time) WITH STATUS 10 IN 1209.97 SECONDS
stats: 3449 7 1209.97 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 694 PB-constraints to clauses...
c   -- Unit propagations: (none)
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 |     694    17335 |     231       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 922   maxlim: 436   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    7110    40242 |    2370       0        0     nan |  0.000 % |
c |       101 |    7110    40242 |    2607     101      393     3.9 |  0.502 % |
c |       252 |    7085    40159 |    2867     248     1017     4.1 |  0.789 % |
c |       479 |    7085    40159 |    3154     475     2831     6.0 |  0.789 % |
c |       816 |    7085    40159 |    3469     812     7492     9.2 |  0.789 % |
c |      1322 |    7061    40077 |    3816    1313    24085    18.3 |  1.076 % |
c |      2081 |    7061    40077 |    4198    2072    53707    25.9 |  1.076 % |
c |      3221 |    7048    40033 |    4618    3208   115274    35.9 |  1.291 % |
c |      4929 |    7048    40033 |    5080    2525    99100    39.2 |  1.291 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 438   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5420 |    7054    40064 |    2351    3016   150367    49.9 |  1.291 % |
c |      5522 |    7054    40064 |    2586    1610    45952    28.5 |  1.433 % |
c |      5674 |    7054    40064 |    2844    1762    49846    28.3 |  1.433 % |
c |      5901 |    7054    40064 |    3129    1989    59731    30.0 |  1.433 % |
c |      6238 |    7054    40064 |    3442    2326    73345    31.5 |  1.433 % |
c |      6745 |    7054    40064 |    3786    2833    97149    34.3 |  1.433 % |
c |      7505 |    7054    40064 |    4164    3593   154807    43.1 |  1.433 % |
c |      8648 |    7054    40064 |    4581    2397    75310    31.4 |  1.433 % |
c |     10357 |    7054    40064 |    5039    4106   191200    46.6 |  1.433 % |
c |     12919 |    7054    40064 |    5543    4029   156820    38.9 |  1.433 % |
c |     16763 |    7054    40064 |    6097    4939   303955    61.5 |  1.433 % |
c ==============================================================================
c [1mFound solution: 28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 439   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18018 |    7029    39979 |    2343    6186   398934    64.5 |  1.433 % |
c |     18118 |    7029    39979 |    2577    1647    37724    22.9 |  1.790 % |
c |     18268 |    7029    39979 |    2835    1797    44606    24.8 |  1.790 % |
c |     18493 |    7029    39979 |    3118    2022    53892    26.7 |  1.790 % |
c |     18830 |    7029    39979 |    3430    2359    73429    31.1 |  1.790 % |
c |     19337 |    7029    39979 |    3773    2866   105054    36.7 |  1.790 % |
c |     20096 |    7029    39979 |    4150    3625   151110    41.7 |  1.790 % |
c |     21235 |    7029    39979 |    4565    2554    89975    35.2 |  1.790 % |
c |     22949 |    7029    39979 |    5022    4268   234958    55.1 |  1.790 % |
c |     25512 |    7029    39979 |    5524    4220   230171    54.5 |  1.790 % |
c |     29356 |    7006    39900 |    6077    5156   279123    54.1 |  2.076 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 440   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32912 |    7009    39914 |    2336    5492   322571    58.7 |  2.076 % |
c |     33012 |    7009    39914 |    2569    1473    26068    17.7 |  2.146 % |
c |     33162 |    7009    39914 |    2826    1623    30813    19.0 |  2.146 % |
c |     33388 |    7009    39914 |    3109    1849    37520    20.3 |  2.146 % |
c |     33725 |    7009    39914 |    3420    2186    58694    26.8 |  2.146 % |
c |     34231 |    7009    39914 |    3762    2692    92786    34.5 |  2.146 % |
c |     34992 |    7009    39914 |    4138    3453   143239    41.5 |  2.146 % |
c |     36132 |    7009    39914 |    4552    2401    76246    31.8 |  2.146 % |
c |     37842 |    7009    39914 |    5007    4111   169147    41.1 |  2.146 % |
c |     40408 |    7009    39914 |    5508    4025   184357    45.8 |  2.146 % |
c |     44252 |    7000    39883 |    6058    5034   273751    54.4 |  2.218 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 441   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46493 |    7001    39890 |    2333    4149   216281    52.1 |  2.218 % |
c |     46595 |    7001    39890 |    2566    2177    78882    36.2 |  2.287 % |
c |     46747 |    7001    39890 |    2822    2329    82427    35.4 |  2.288 % |
c |     46975 |    7001    39890 |    3105    2557    92633    36.2 |  2.287 % |
c |     47313 |    7001    39890 |    3415    2895   114105    39.4 |  2.287 % |
c |     47820 |    7001    39890 |    3757    3402   139889    41.1 |  2.287 % |
c |     48581 |    7001    39890 |    4133    2193    62645    28.6 |  2.287 % |
c |     49721 |    7001    39890 |    4546    3333   135828    40.8 |  2.287 % |
c |     51429 |    7001    39890 |    5000    2613   118260    45.3 |  2.287 % |
c |     53994 |    7001    39890 |    5501    5178   329833    63.7 |  2.288 % |
c |     57840 |    6975    39800 |    6051    3301   150037    45.5 |  2.573 % |
c |     63606 |    6975    39800 |    6656    5862   518264    88.4 |  2.573 % |
c |     72255 |    6975    39800 |    7321    4182   308523    73.8 |  2.573 % |
c |     85230 |    6975    39800 |    8054    5562   316547    56.9 |  2.573 % |
c |    104692 |    6975    39800 |    8859    8323   489432    58.8 |  2.573 % |
c |    133884 |    6975    39800 |    9745    5507   389569    70.7 |  2.573 % |
c |    177674 |    6975    39800 |   10720    9526   718740    75.5 |  2.573 % |
c |    243359 |    6975    39800 |   11792    9247   663097    71.7 |  2.573 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 442   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    320244 |    6976    39808 |    2325    6802   665186    97.8 |  2.573 % |
c |    320344 |    6976    39808 |    2557    1801    48359    26.9 |  2.643 % |
c |    320494 |    6976    39808 |    2813    1951    49295    25.3 |  2.643 % |
c |    320720 |    6976    39808 |    3094    2177    56151    25.8 |  2.645 % |
c |    321058 |    6976    39808 |    3404    2515    69890    27.8 |  2.643 % |
c |    321566 |    6976    39808 |    3744    3023    99236    32.8 |  2.643 % |
c |    322326 |    6976    39808 |    4118    3783   143580    38.0 |  2.643 % |
c |    323465 |    6976    39808 |    4530    2783    95001    34.1 |  2.643 % |
c |    325175 |    6976    39808 |    4983    4493   199268    44.4 |  2.643 % |
c |    327737 |    6976    39808 |    5482    4386   217539    49.6 |  2.643 % |
c |    331587 |    6976    39808 |    6030    5370   277732    51.7 |  2.643 % |
c |    337355 |    6976    39808 |    6633    4895   175658    35.9 |  2.643 % |
c |    346004 |    6976    39808 |    7296    6698   451883    67.5 |  2.643 % |
c |    358978 |    6976    39808 |    8026    4617   255848    55.4 |  2.643 % |
c |    378440 |    6976    39808 |    8829    7286   534197    73.3 |  2.643 % |
c |    407632 |    6976    39808 |    9712    4672   235153    50.3 |  2.643 % |
c |    451422 |    6976    39808 |   10683    8849   612372    69.2 |  2.643 % |
c |    517107 |    6976    39808 |   11751    8467   791823    93.5 |  2.643 % |
c |    615635 |    6976    39808 |   12926   10995   934963    85.0 |  2.643 % |
c |    763425 |    6976    39808 |   14219   13131  1159728    88.3 |  2.643 % |
c |    985110 |    6976    39808 |   15641    9804   864343    88.2 |  2.643 % |
c |   1317635 |    6976    39808 |   17205    9301   784747    84.4 |  2.643 % |
#### 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.91 0.95 0.69 2/54 24846
Raw data (stat): 24846 (runsolver) R 24845 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420341765 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.69 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1003 0 0 0 996 2 0 0 25 0 1 0 420341765 5582848 981 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1363 981 603 41 0 1322 0
vsize: 5452
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.95 0.69 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1013 0 0 0 1995 2 0 0 25 0 1 0 420341765 5582848 991 4294967295 134512640 134672761 3221224576 3221223760 134558925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1363 991 603 41 0 1322 0
vsize: 5452
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.96 0.70 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1176 0 0 0 2995 3 0 0 25 0 1 0 420341765 6373376 1154 4294967295 134512640 134672761 3221224576 3221223760 134559559 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1556 1154 603 41 0 1515 0
vsize: 6224
[startup+40.0026 s]
Raw data (loadavg): 0.95 0.96 0.70 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1461 0 0 0 3993 4 0 0 25 0 1 0 420341765 7446528 1439 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1818 1439 603 41 0 1777 0
vsize: 7272
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.96 0.70 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1466 0 0 0 4993 4 0 0 25 0 1 0 420341765 7593984 1444 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1854 1444 603 41 0 1813 0
vsize: 7416
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.96 0.71 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1467 0 0 0 5993 4 0 0 25 0 1 0 420341765 7593984 1445 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1854 1445 603 41 0 1813 0
vsize: 7416
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.96 0.71 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1467 0 0 0 6993 4 0 0 25 0 1 0 420341765 7593984 1445 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1854 1445 603 41 0 1813 0
vsize: 7416
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.96 0.71 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1840 0 0 0 7993 5 0 0 25 0 1 0 420341765 9068544 1818 4294967295 134512640 134672761 3221224576 3221222604 134566355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2214 1818 603 41 0 2173 0
vsize: 8856
[startup+90.0043 s]
Raw data (loadavg): 0.98 0.96 0.71 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1841 0 0 0 8993 5 0 0 25 0 1 0 420341765 9068544 1819 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2214 1819 603 41 0 2173 0
vsize: 8856
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1841 0 0 0 9993 5 0 0 25 0 1 0 420341765 9068544 1819 4294967295 134512640 134672761 3221224576 3221223680 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2214 1819 603 41 0 2173 0
vsize: 8856
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1841 0 0 0 10993 5 0 0 25 0 1 0 420341765 9068544 1819 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2214 1819 603 41 0 2173 0
vsize: 8856
[startup+120.005 s]
Raw data (loadavg): 0.99 0.96 0.72 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1842 0 0 0 11993 5 0 0 25 0 1 0 420341765 9068544 1820 4294967295 134512640 134672761 3221224576 3221223760 134559055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2214 1820 603 41 0 2173 0
vsize: 8856
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1919 0 0 0 12993 5 0 0 25 0 1 0 420341765 9330688 1897 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2278 1897 603 41 0 2237 0
vsize: 9112
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1931 0 0 0 13993 5 0 0 25 0 1 0 420341765 9474048 1909 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2313 1909 603 41 0 2272 0
vsize: 9252
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1931 0 0 0 14994 5 0 0 25 0 1 0 420341765 9474048 1909 4294967295 134512640 134672761 3221224576 3221223680 134555126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2313 1909 603 41 0 2272 0
vsize: 9252
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 1931 0 0 0 15994 5 0 0 25 0 1 0 420341765 9474048 1909 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2313 1909 603 41 0 2272 0
vsize: 9252
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2117 0 0 0 16994 5 0 0 25 0 1 0 420341765 10141696 2095 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2476 2095 603 41 0 2435 0
vsize: 9904
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 17992 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2640 2248 603 41 0 2599 0
vsize: 10560
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 18992 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2640 2248 603 41 0 2599 0
vsize: 10560
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 19992 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2640 2248 603 41 0 2599 0
vsize: 10560
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 20993 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2640 2248 603 41 0 2599 0
vsize: 10560
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 21993 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2640 2248 603 41 0 2599 0
vsize: 10560
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2270 0 0 0 22993 6 0 0 25 0 1 0 420341765 10813440 2248 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2640 2248 603 41 0 2599 0
vsize: 10560
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2619 0 0 0 23992 7 0 0 25 0 1 0 420341765 12279808 2597 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2998 2597 603 41 0 2957 0
vsize: 11992
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 24993 7 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 25992 7 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 26992 7 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 27992 8 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 28991 8 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 29991 8 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 30991 8 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 31991 9 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 32990 9 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 33990 9 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 34989 9 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223532 1075350145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 35989 10 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223776 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 36988 11 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 37988 11 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223816 134564425 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 38988 11 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223576 1075350763 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 39987 12 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 40987 12 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 41987 12 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 42987 12 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 43986 12 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 44986 13 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 45985 13 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2622 0 0 0 46985 13 0 0 25 0 1 0 420341765 12247040 2600 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2990 2600 603 41 0 2949 0
vsize: 11960
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2743 0 0 0 47984 14 0 0 25 0 1 0 420341765 12795904 2721 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3124 2721 603 41 0 3083 0
vsize: 12496
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2743 0 0 0 48984 14 0 0 25 0 1 0 420341765 12795904 2721 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3124 2721 603 41 0 3083 0
vsize: 12496
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2743 0 0 0 49984 14 0 0 25 0 1 0 420341765 12795904 2721 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3124 2721 603 41 0 3083 0
vsize: 12496
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2744 0 0 0 50983 15 0 0 25 0 1 0 420341765 12795904 2722 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3124 2722 603 41 0 3083 0
vsize: 12496
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2744 0 0 0 51983 15 0 0 25 0 1 0 420341765 12795904 2722 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3124 2722 603 41 0 3083 0
vsize: 12496
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2744 0 0 0 52983 15 0 0 25 0 1 0 420341765 12795904 2722 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3124 2722 603 41 0 3083 0
vsize: 12496
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2744 0 0 0 53982 15 0 0 25 0 1 0 420341765 12795904 2722 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3124 2722 603 41 0 3083 0
vsize: 12496
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2753 0 0 0 54982 16 0 0 25 0 1 0 420341765 12795904 2731 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3124 2731 603 41 0 3083 0
vsize: 12496
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2807 0 0 0 55981 16 0 0 25 0 1 0 420341765 13066240 2785 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3190 2785 603 41 0 3149 0
vsize: 12760
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2807 0 0 0 56981 16 0 0 25 0 1 0 420341765 13066240 2785 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3190 2785 603 41 0 3149 0
vsize: 12760
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2807 0 0 0 57981 17 0 0 25 0 1 0 420341765 13053952 2785 4294967295 134512640 134672761 3221224576 3221223680 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3187 2785 603 41 0 3146 0
vsize: 12748
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2807 0 0 0 58980 17 0 0 25 0 1 0 420341765 13053952 2785 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3187 2785 603 41 0 3146 0
vsize: 12748
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2817 0 0 0 59980 17 0 0 25 0 1 0 420341765 13053952 2795 4294967295 134512640 134672761 3221224576 3221223744 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3187 2795 603 41 0 3146 0
vsize: 12748
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2817 0 0 0 60979 18 0 0 25 0 1 0 420341765 13053952 2795 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3187 2795 603 41 0 3146 0
vsize: 12748
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2817 0 0 0 61979 18 0 0 25 0 1 0 420341765 13053952 2795 4294967295 134512640 134672761 3221224576 3221223760 134559514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3187 2795 603 41 0 3146 0
vsize: 12748
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2824 0 0 0 62979 18 0 0 25 0 1 0 420341765 13053952 2802 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3187 2802 603 41 0 3146 0
vsize: 12748
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2824 0 0 0 63978 19 0 0 25 0 1 0 420341765 13053952 2802 4294967295 134512640 134672761 3221224576 3221223760 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3187 2802 603 41 0 3146 0
vsize: 12748
[startup+650.026 s]
Raw data (loadavg): 1.07 0.99 0.83 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2927 0 0 0 64977 20 0 0 25 0 1 0 420341765 13455360 2905 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3285 2905 603 41 0 3244 0
vsize: 13140
[startup+660.026 s]
Raw data (loadavg): 1.06 0.99 0.83 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2940 0 0 0 65977 20 0 0 25 0 1 0 420341765 13594624 2918 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3319 2918 603 41 0 3278 0
vsize: 13276
[startup+670.026 s]
Raw data (loadavg): 1.05 0.99 0.83 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2966 0 0 0 66977 20 0 0 25 0 1 0 420341765 13729792 2944 4294967295 134512640 134672761 3221224576 3221223680 134560231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3352 2944 603 41 0 3311 0
vsize: 13408
[startup+680.027 s]
Raw data (loadavg): 1.04 0.99 0.83 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2972 0 0 0 67976 21 0 0 25 0 1 0 420341765 13729792 2950 4294967295 134512640 134672761 3221224576 3221223760 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3352 2950 603 41 0 3311 0
vsize: 13408
[startup+690.027 s]
Raw data (loadavg): 1.03 0.99 0.83 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2972 0 0 0 68976 21 0 0 25 0 1 0 420341765 13729792 2950 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3352 2950 603 41 0 3311 0
vsize: 13408
[startup+700.027 s]
Raw data (loadavg): 1.03 0.99 0.83 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2983 0 0 0 69976 21 0 0 25 0 1 0 420341765 13729792 2961 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3352 2961 603 41 0 3311 0
vsize: 13408
[startup+710.028 s]
Raw data (loadavg): 1.02 0.99 0.83 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2983 0 0 0 70975 21 0 0 25 0 1 0 420341765 13729792 2961 4294967295 134512640 134672761 3221224576 3221223712 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3352 2961 603 41 0 3311 0
vsize: 13408
[startup+720.029 s]
Raw data (loadavg): 1.02 0.99 0.84 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2984 0 0 0 71975 22 0 0 25 0 1 0 420341765 13729792 2962 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3352 2962 603 41 0 3311 0
vsize: 13408
[startup+730.028 s]
Raw data (loadavg): 1.02 0.99 0.84 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 2986 0 0 0 72975 22 0 0 25 0 1 0 420341765 13729792 2964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3352 2964 603 41 0 3311 0
vsize: 13408
[startup+740.029 s]
Raw data (loadavg): 1.01 0.99 0.84 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3175 0 0 0 73974 23 0 0 25 0 1 0 420341765 14532608 3153 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3153 603 41 0 3507 0
vsize: 14192
[startup+750.029 s]
Raw data (loadavg): 1.01 0.99 0.84 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3175 0 0 0 74973 23 0 0 25 0 1 0 420341765 14532608 3153 4294967295 134512640 134672761 3221224576 3221223576 1075349975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3153 603 41 0 3507 0
vsize: 14192
[startup+760.029 s]
Raw data (loadavg): 1.01 0.99 0.84 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3175 0 0 0 75973 23 0 0 25 0 1 0 420341765 14532608 3153 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3153 603 41 0 3507 0
vsize: 14192
[startup+770.029 s]
Raw data (loadavg): 1.01 0.99 0.84 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 76973 23 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3154 603 41 0 3507 0
vsize: 14192
[startup+780.03 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 77972 24 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3154 603 41 0 3507 0
vsize: 14192
[startup+790.03 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 78972 24 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3154 603 41 0 3507 0
vsize: 14192
[startup+800.03 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 79972 24 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223728 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3154 603 41 0 3507 0
vsize: 14192
[startup+810.031 s]
Raw data (loadavg): 1.00 0.99 0.84 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 80971 24 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3154 603 41 0 3507 0
vsize: 14192
[startup+820.031 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 81971 25 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3154 603 41 0 3507 0
vsize: 14192
[startup+830.031 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 82971 25 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3154 603 41 0 3507 0
vsize: 14192
[startup+840.032 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 83970 25 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3154 603 41 0 3507 0
vsize: 14192
[startup+850.031 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 84969 26 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3154 603 41 0 3507 0
vsize: 14192
[startup+860.032 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3176 0 0 0 85969 26 0 0 25 0 1 0 420341765 14532608 3154 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3548 3154 603 41 0 3507 0
vsize: 14192
[startup+870.033 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3267 0 0 0 86969 26 0 0 25 0 1 0 420341765 14938112 3245 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3647 3245 603 41 0 3606 0
vsize: 14588
[startup+880.033 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3267 0 0 0 87969 26 0 0 25 0 1 0 420341765 14938112 3245 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3647 3245 603 41 0 3606 0
vsize: 14588
[startup+890.033 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3267 0 0 0 88968 27 0 0 25 0 1 0 420341765 14938112 3245 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3647 3245 603 41 0 3606 0
vsize: 14588
[startup+900.033 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3328 0 0 0 89968 27 0 0 25 0 1 0 420341765 15216640 3306 4294967295 134512640 134672761 3221224576 3221223744 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3306 603 41 0 3674 0
vsize: 14860
[startup+910.034 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3332 0 0 0 90967 28 0 0 25 0 1 0 420341765 15216640 3310 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3310 603 41 0 3674 0
vsize: 14860
[startup+920.034 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3332 0 0 0 91967 28 0 0 25 0 1 0 420341765 15216640 3310 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3310 603 41 0 3674 0
vsize: 14860
[startup+930.034 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3332 0 0 0 92966 28 0 0 25 0 1 0 420341765 15216640 3310 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3310 603 41 0 3674 0
vsize: 14860
[startup+940.034 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3332 0 0 0 93966 29 0 0 25 0 1 0 420341765 15216640 3310 4294967295 134512640 134672761 3221224576 3221223760 134559327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3310 603 41 0 3674 0
vsize: 14860
[startup+950.034 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 94965 29 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223728 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3316 603 41 0 3674 0
vsize: 14860
[startup+960.035 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 95965 30 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3316 603 41 0 3674 0
vsize: 14860
[startup+970.035 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 96964 30 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3316 603 41 0 3674 0
vsize: 14860
[startup+980.035 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 97964 30 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3316 603 41 0 3674 0
vsize: 14860
[startup+990.036 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 98964 30 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223776 134557796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3316 603 41 0 3674 0
vsize: 14860
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3338 0 0 0 99963 31 0 0 25 0 1 0 420341765 15216640 3316 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3316 603 41 0 3674 0
vsize: 14860
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3344 0 0 0 100963 31 0 0 25 0 1 0 420341765 15216640 3322 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3715 3322 603 41 0 3674 0
vsize: 14860
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 24846
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3350 0 0 0 101963 31 0 0 25 0 1 0 420341765 15364096 3328 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3751 3328 603 41 0 3710 0
vsize: 15004
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/57 24849
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3357 0 0 0 102959 35 0 0 25 0 1 0 420341765 15364096 3335 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3335 603 41 0 3710 0
vsize: 15004
[startup+1040.04 s]
Raw data (loadavg): 1.07 1.00 0.87 2/54 24899
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3357 0 0 0 103958 35 0 0 25 0 1 0 420341765 15364096 3335 4294967295 134512640 134672761 3221224576 3221223680 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3335 603 41 0 3710 0
vsize: 15004
[startup+1050.04 s]
Raw data (loadavg): 1.06 1.00 0.87 2/54 24899
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 104958 35 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3354 603 41 0 3710 0
vsize: 15004
[startup+1060.04 s]
Raw data (loadavg): 1.05 1.00 0.87 2/54 24899
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 105958 35 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3354 603 41 0 3710 0
vsize: 15004
[startup+1070.04 s]
Raw data (loadavg): 1.04 1.00 0.87 2/54 24899
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 106959 36 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3354 603 41 0 3710 0
vsize: 15004
[startup+1080.04 s]
Raw data (loadavg): 1.04 1.00 0.88 2/54 24899
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 107959 36 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3354 603 41 0 3710 0
vsize: 15004
[startup+1090.04 s]
Raw data (loadavg): 1.03 1.00 0.88 2/54 24899
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 108959 36 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3354 603 41 0 3710 0
vsize: 15004
[startup+1100.04 s]
Raw data (loadavg): 1.02 1.00 0.88 2/54 24899
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3376 0 0 0 109959 36 0 0 25 0 1 0 420341765 15364096 3354 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3751 3354 603 41 0 3710 0
vsize: 15004
[startup+1110.04 s]
Raw data (loadavg): 1.02 1.00 0.88 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3436 0 0 0 110959 36 0 0 25 0 1 0 420341765 15626240 3414 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3815 3414 603 41 0 3774 0
vsize: 15260
[startup+1120.04 s]
Raw data (loadavg): 1.02 1.00 0.88 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3493 0 0 0 111959 36 0 0 25 0 1 0 420341765 15892480 3471 4294967295 134512640 134672761 3221224576 3221223680 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3880 3471 603 41 0 3839 0
vsize: 15520
[startup+1130.04 s]
Raw data (loadavg): 1.01 1.00 0.88 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3512 0 0 0 112959 36 0 0 25 0 1 0 420341765 16056320 3490 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3920 3490 603 41 0 3879 0
vsize: 15680
[startup+1140.04 s]
Raw data (loadavg): 1.01 1.00 0.88 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3518 0 0 0 113959 36 0 0 25 0 1 0 420341765 16056320 3496 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3920 3496 603 41 0 3879 0
vsize: 15680
[startup+1150.04 s]
Raw data (loadavg): 1.01 1.00 0.88 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3518 0 0 0 114959 36 0 0 25 0 1 0 420341765 16056320 3496 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3920 3496 603 41 0 3879 0
vsize: 15680
[startup+1160.04 s]
Raw data (loadavg): 1.01 1.00 0.88 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3518 0 0 0 115960 36 0 0 25 0 1 0 420341765 16056320 3496 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3920 3496 603 41 0 3879 0
vsize: 15680
[startup+1170.04 s]
Raw data (loadavg): 1.01 1.00 0.88 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3561 0 0 0 116960 36 0 0 25 0 1 0 420341765 16191488 3539 4294967295 134512640 134672761 3221224576 3221223760 134559609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3953 3539 603 41 0 3912 0
vsize: 15812
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3569 0 0 0 117960 36 0 0 25 0 1 0 420341765 16330752 3547 4294967295 134512640 134672761 3221224576 3221222592 134565819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3987 3547 603 41 0 3946 0
vsize: 15948
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3645 0 0 0 118960 36 0 0 25 0 1 0 420341765 16601088 3623 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4053 3623 603 41 0 4012 0
vsize: 16212
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3837 0 0 0 119959 37 0 0 25 0 1 0 420341765 17432576 3815 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4256 3815 603 41 0 4215 0
vsize: 17024
[startup+1210.04 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 24901
Raw data (stat): 24846 (minisat+) R 24845 22932 22931 0 -1 0 3855 0 0 0 120959 37 0 0 25 0 1 0 420341765 17596416 3833 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4296 3833 603 41 0 4255 0
vsize: 17184
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.05 s]
Raw data (loadavg): 1.00 1.00 0.89 1/54 24901
Raw data (stat): 24846 (minisat+) Z 24845 22932 22931 0 -1 12 3858 0 0 0 120959 38 0 0 25 0 1 0 420341765 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: 10
Real time (s): 1210.05
CPU time (s): 1209.97
CPU user time (s): 1209.59
CPU system time (s): 0.381941
CPU usage (%): 99.994
Max. virtual memory (Kb): 17184
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####