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-ii32e2.opb
MD5SUM	4e882bbd92f288daf6e68ac3de757136
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	235
Optimality of the best value was proved	NO
Number of terms in the objective function	534
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	534
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	534
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03084
Number of variables	534
Total number of constraints	3013
Number of constraints which are clauses	3013
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	32
Trace number 4726

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-13 20:05:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3543 boxname=wulflinc27 idbench=159 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4e882bbd92f288daf6e68ac3de757136  /oldhome/oroussel/tmp/wulflinc27/normalized-ii32e2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc27/normalized-ii32e2.opb /oldhome/oroussel/tmp/wulflinc27/normalized-ii32e2.opb
IDLAUNCH: 3543
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        883068 kB
Buffers:         33208 kB
Cached:          81680 kB
SwapCached:       3160 kB
Active:          46156 kB
Inactive:        74736 kB
HighTotal:      131008 kB
HighFree:        45976 kB
LowTotal:       903652 kB
LowFree:        837092 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25192 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:25:10 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3543 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3013 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 |    3013    12801 |    1004       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 262[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1060   maxlim: 272   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        51 |   10375    39071 |    3458      51     2400    47.1 |  0.000 % |
c |       151 |   10375    39071 |    3803     151     7964    52.7 |  0.188 % |
c ==============================================================================
c [1mFound solution: 254[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 280   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       280 |   10380    39098 |    3460     280    13678    48.9 |  0.188 % |
c |       380 |   10380    39098 |    3806     380    18643    49.1 |  0.313 % |
c |       532 |   10380    39098 |    4186     532    26842    50.5 |  0.313 % |
c |       759 |   10380    39098 |    4605     759    39371    51.9 |  0.313 % |
c |      1100 |   10380    39098 |    5065    1100    52030    47.3 |  0.313 % |
c ==============================================================================
c [1mFound solution: 253[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 281   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1256 |   10381    39108 |    3460    1256    58907    46.9 |  0.313 % |
c |      1361 |   10381    39108 |    3806    1361    61109    44.9 |  0.375 % |
c |      1513 |   10381    39108 |    4186    1513    66908    44.2 |  0.375 % |
c |      1738 |   10381    39108 |    4605    1738    73821    42.5 |  0.375 % |
c |      2076 |   10381    39108 |    5065    2076    87908    42.3 |  0.375 % |
c |      2583 |   10381    39108 |    5572    2583   103499    40.1 |  0.375 % |
c |      3343 |   10381    39108 |    6129    3343   127805    38.2 |  0.375 % |
c ==============================================================================
c [1mFound solution: 250[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 284   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3437 |   10387    39144 |    3462    3437   129715    37.7 |  0.375 % |
c |      3537 |   10387    39144 |    3808    3537   135615    38.3 |  0.499 % |
c |      3687 |   10387    39144 |    4189    3687   145777    39.5 |  0.499 % |
c |      3912 |   10387    39144 |    4607    3912   157881    40.4 |  0.499 % |
c |      4249 |   10387    39144 |    5068    4249   168943    39.8 |  0.499 % |
c |      4758 |   10387    39144 |    5575    4758   192959    40.6 |  0.499 % |
c |      5517 |   10387    39144 |    6133    5517   221369    40.1 |  0.499 % |
c ==============================================================================
c [1mFound solution: 243[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 291   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5586 |   10391    39165 |    3463    5586   222789    39.9 |  0.499 % |
c |      5687 |   10391    39165 |    3809    2894   105805    36.6 |  0.623 % |
c |      5837 |   10391    39165 |    4190    3044   108309    35.6 |  0.623 % |
c |      6062 |   10391    39165 |    4609    3269   120295    36.8 |  0.623 % |
c |      6402 |   10391    39165 |    5070    3609   127827    35.4 |  0.623 % |
c |      6910 |   10391    39165 |    5577    4117   150762    36.6 |  0.623 % |
c |      7670 |   10391    39165 |    6134    4877   186925    38.3 |  0.623 % |
c ==============================================================================
c [1mFound solution: 239[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 295   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7860 |   10392    39173 |    3464    5067   196618    38.8 |  0.623 % |
c ==============================================================================
c [1mFound solution: 237[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 297   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7874 |   10394    39185 |    3464    2548    90067    35.3 |  0.623 % |
c |      7976 |   10394    39185 |    3810    2650    97702    36.9 |  0.746 % |
c |      8127 |   10394    39185 |    4191    2801    99287    35.4 |  0.746 % |
c |      8352 |   10394    39185 |    4610    3026   110009    36.4 |  0.746 % |
c |      8689 |   10394    39185 |    5071    3363   119575    35.6 |  0.746 % |
c |      9199 |   10394    39185 |    5578    3873   139623    36.1 |  0.747 % |
c |      9959 |   10394    39185 |    6136    4633   188525    40.7 |  0.746 % |
c |     11098 |   10394    39185 |    6750    5772   225393    39.0 |  0.746 % |
c |     12806 |   10394    39185 |    7425    7480   356157    47.6 |  0.746 % |
c |     15369 |   10394    39185 |    8167    6303   257950    40.9 |  0.746 % |
c |     19213 |   10394    39185 |    8984    5434   245413    45.2 |  0.746 % |
c |     24979 |   10394    39185 |    9883    6151   304160    49.4 |  0.746 % |
c |     33628 |   10394    39185 |   10871    9351   653769    69.9 |  0.746 % |
c ==============================================================================
c [1mFound solution: 236[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 298   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37693 |   10399    39212 |    3466    7317   456700    62.4 |  0.746 % |
c |     37793 |   10399    39212 |    3812    1930    83466    43.2 |  0.808 % |
c |     37943 |   10399    39212 |    4193    2080    87894    42.3 |  0.808 % |
c |     38170 |   10399    39212 |    4613    2307    97497    42.3 |  0.808 % |
c |     38508 |   10399    39212 |    5074    2645   108477    41.0 |  0.808 % |
c |     39015 |   10399    39212 |    5582    3152   125099    39.7 |  0.808 % |
c |     39774 |   10399    39212 |    6140    3911   166259    42.5 |  0.808 % |
c |     40914 |   10399    39212 |    6754    5051   195953    38.8 |  0.808 % |
c |     42622 |   10399    39212 |    7429    6759   317141    46.9 |  0.808 % |
c |     45184 |   10399    39212 |    8172    5199   241827    46.5 |  0.808 % |
c |     49032 |   10399    39212 |    8989    4885   248310    50.8 |  0.808 % |
c |     54798 |   10399    39212 |    9888    6100   210137    34.4 |  0.808 % |
c |     63447 |   10399    39212 |   10877    9333  1090069   116.8 |  0.808 % |
c |     76421 |   10399    39212 |   11965   10325   916154    88.7 |  0.808 % |
c |     95882 |   10399    39212 |   13162   10247   897828    87.6 |  0.808 % |
c |    125077 |   10399    39212 |   14478   10995  1200494   109.2 |  0.808 % |
c |    168866 |   10399    39212 |   15926    8373   726873    86.8 |  0.808 % |
c |    234550 |   10399    39212 |   17518   15046  1890199   125.6 |  0.808 % |
c |    333077 |   10399    39212 |   19270   11803   901041    76.3 |  0.808 % |
c |    480867 |   10399    39212 |   21197   18044  1560797    86.5 |  0.808 % |
c |    702552 |   10399    39212 |   23317   17994  1401590    77.9 |  0.808 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.87 2/54 20499
Raw data (stat): 20499 (runsolver) R 20498 18865 18864 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 478689953 1052672 97 4294967295 134512640 135381576 3221224464 3221219836 135024803 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.87 0.95 0.88 2/54 20499
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 1064 0 0 0 995 3 0 0 25 0 1 0 478689953 5943296 1042 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1451 1042 603 41 0 1410 0
vsize: 5804
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.96 0.88 2/54 20499
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 1554 0 0 0 1992 5 0 0 25 0 1 0 478689953 7827456 1532 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1911 1532 603 41 0 1870 0
vsize: 7644
[startup+30.0025 s]
Raw data (loadavg): 0.91 0.96 0.88 2/54 20499
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 1554 0 0 0 2992 6 0 0 25 0 1 0 478689953 7827456 1532 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1911 1532 603 41 0 1870 0
vsize: 7644
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.96 0.88 2/54 20499
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2091 0 0 0 3990 8 0 0 25 0 1 0 478689953 10104832 2069 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2069 603 41 0 2426 0
vsize: 9868
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.96 0.88 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2091 0 0 0 4990 8 0 0 25 0 1 0 478689953 10104832 2069 4294967295 134512640 134672761 3221224576 3221223680 134560269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2069 603 41 0 2426 0
vsize: 9868
[startup+60.002 s]
Raw data (loadavg): 0.94 0.96 0.88 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2092 0 0 0 5990 8 0 0 25 0 1 0 478689953 10104832 2070 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2070 603 41 0 2426 0
vsize: 9868
[startup+70.0028 s]
Raw data (loadavg): 0.95 0.96 0.88 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2093 0 0 0 6991 8 0 0 25 0 1 0 478689953 10104832 2071 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2071 603 41 0 2426 0
vsize: 9868
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.96 0.88 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2126 0 0 0 7991 8 0 0 25 0 1 0 478689953 10240000 2104 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2500 2104 603 41 0 2459 0
vsize: 10000
[startup+90.0035 s]
Raw data (loadavg): 0.96 0.96 0.88 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2338 0 0 0 8990 9 0 0 25 0 1 0 478689953 11059200 2316 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2700 2316 603 41 0 2659 0
vsize: 10800
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.88 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2496 0 0 0 9989 9 0 0 25 0 1 0 478689953 11730944 2474 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2864 2474 603 41 0 2823 0
vsize: 11456
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2513 0 0 0 10989 9 0 0 25 0 1 0 478689953 11862016 2491 4294967295 134512640 134672761 3221224576 3221223632 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2896 2491 603 41 0 2855 0
vsize: 11584
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2513 0 0 0 11989 10 0 0 25 0 1 0 478689953 11853824 2491 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2894 2491 603 41 0 2853 0
vsize: 11576
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2513 0 0 0 12989 10 0 0 25 0 1 0 478689953 11853824 2491 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2894 2491 603 41 0 2853 0
vsize: 11576
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2617 0 0 0 13989 10 0 0 25 0 1 0 478689953 12251136 2595 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2991 2595 603 41 0 2950 0
vsize: 11964
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2617 0 0 0 14989 10 0 0 25 0 1 0 478689953 12251136 2595 4294967295 134512640 134672761 3221224576 3221223680 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2991 2595 603 41 0 2950 0
vsize: 11964
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2642 0 0 0 15989 10 0 0 25 0 1 0 478689953 12419072 2620 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3032 2620 603 41 0 2991 0
vsize: 12128
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 2840 0 0 0 16989 10 0 0 25 0 1 0 478689953 13225984 2818 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3229 2818 603 41 0 3188 0
vsize: 12916
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3134 0 0 0 17988 12 0 0 25 0 1 0 478689953 14442496 3112 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3526 3112 603 41 0 3485 0
vsize: 14104
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3277 0 0 0 18987 12 0 0 25 0 1 0 478689953 14979072 3255 4294967295 134512640 134672761 3221224576 3221223760 134559373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3657 3255 603 41 0 3616 0
vsize: 14628
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3559 0 0 0 19987 13 0 0 25 0 1 0 478689953 16195584 3537 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3954 3537 603 41 0 3913 0
vsize: 15816
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3559 0 0 0 20987 13 0 0 25 0 1 0 478689953 16183296 3537 4294967295 134512640 134672761 3221224576 3221223680 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3537 603 41 0 3910 0
vsize: 15804
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3559 0 0 0 21987 13 0 0 25 0 1 0 478689953 16183296 3537 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3537 603 41 0 3910 0
vsize: 15804
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3560 0 0 0 22987 13 0 0 25 0 1 0 478689953 16183296 3538 4294967295 134512640 134672761 3221224576 3221223680 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3538 603 41 0 3910 0
vsize: 15804
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3560 0 0 0 23987 13 0 0 25 0 1 0 478689953 16183296 3538 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3538 603 41 0 3910 0
vsize: 15804
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3561 0 0 0 24987 14 0 0 25 0 1 0 478689953 16183296 3539 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3539 603 41 0 3910 0
vsize: 15804
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3561 0 0 0 25987 14 0 0 25 0 1 0 478689953 16183296 3539 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3539 603 41 0 3910 0
vsize: 15804
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3561 0 0 0 26987 14 0 0 25 0 1 0 478689953 16183296 3539 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3539 603 41 0 3910 0
vsize: 15804
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3561 0 0 0 27988 14 0 0 25 0 1 0 478689953 16183296 3539 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3539 603 41 0 3910 0
vsize: 15804
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3562 0 0 0 28988 14 0 0 25 0 1 0 478689953 16183296 3540 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3540 603 41 0 3910 0
vsize: 15804
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3562 0 0 0 29988 14 0 0 25 0 1 0 478689953 16183296 3540 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3540 603 41 0 3910 0
vsize: 15804
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3562 0 0 0 30988 14 0 0 25 0 1 0 478689953 16183296 3540 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3540 603 41 0 3910 0
vsize: 15804
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3562 0 0 0 31988 14 0 0 25 0 1 0 478689953 16183296 3540 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3540 603 41 0 3910 0
vsize: 15804
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3562 0 0 0 32988 14 0 0 25 0 1 0 478689953 16183296 3540 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3540 603 41 0 3910 0
vsize: 15804
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3562 0 0 0 33988 14 0 0 25 0 1 0 478689953 16183296 3540 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3540 603 41 0 3910 0
vsize: 15804
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3562 0 0 0 34988 15 0 0 25 0 1 0 478689953 16183296 3540 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3540 603 41 0 3910 0
vsize: 15804
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3562 0 0 0 35988 15 0 0 25 0 1 0 478689953 16183296 3540 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3540 603 41 0 3910 0
vsize: 15804
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3562 0 0 0 36988 15 0 0 25 0 1 0 478689953 16183296 3540 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3951 3540 603 41 0 3910 0
vsize: 15804
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3562 0 0 0 37988 15 0 0 25 0 1 0 478689953 16183296 3540 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3540 603 41 0 3910 0
vsize: 15804
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 38988 15 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 39988 15 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 40988 15 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 41988 15 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223680 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 42988 15 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 43988 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 44988 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223680 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 45988 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 46988 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 47988 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 48988 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 49988 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 50989 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 51989 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 52989 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3563 0 0 0 53989 16 0 0 25 0 1 0 478689953 16183296 3541 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3541 603 41 0 3910 0
vsize: 15804
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3565 0 0 0 54989 16 0 0 25 0 1 0 478689953 16183296 3543 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3543 603 41 0 3910 0
vsize: 15804
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3565 0 0 0 55989 17 0 0 25 0 1 0 478689953 16183296 3543 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3543 603 41 0 3910 0
vsize: 15804
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3565 0 0 0 56989 17 0 0 25 0 1 0 478689953 16183296 3543 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3543 603 41 0 3910 0
vsize: 15804
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3566 0 0 0 57989 17 0 0 25 0 1 0 478689953 16183296 3544 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3544 603 41 0 3910 0
vsize: 15804
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3566 0 0 0 58989 17 0 0 25 0 1 0 478689953 16183296 3544 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3544 603 41 0 3910 0
vsize: 15804
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3583 0 0 0 59989 17 0 0 25 0 1 0 478689953 16183296 3561 4294967295 134512640 134672761 3221224576 3221223760 134558903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3561 603 41 0 3910 0
vsize: 15804
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3583 0 0 0 60989 17 0 0 25 0 1 0 478689953 16183296 3561 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3561 603 41 0 3910 0
vsize: 15804
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3583 0 0 0 61989 17 0 0 25 0 1 0 478689953 16183296 3561 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3561 603 41 0 3910 0
vsize: 15804
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3583 0 0 0 62989 17 0 0 25 0 1 0 478689953 16183296 3561 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3561 603 41 0 3910 0
vsize: 15804
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3583 0 0 0 63989 17 0 0 25 0 1 0 478689953 16183296 3561 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3561 603 41 0 3910 0
vsize: 15804
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3583 0 0 0 64989 17 0 0 25 0 1 0 478689953 16183296 3561 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3951 3561 603 41 0 3910 0
vsize: 15804
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3626 0 0 0 65989 17 0 0 25 0 1 0 478689953 16453632 3604 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4017 3604 603 41 0 3976 0
vsize: 16068
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3635 0 0 0 66990 18 0 0 25 0 1 0 478689953 16453632 3613 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4017 3613 603 41 0 3976 0
vsize: 16068
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 67989 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 68990 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 69990 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223680 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 70990 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223680 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 71990 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 72990 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 73991 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 74991 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 75991 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 76991 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223680 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 77991 18 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 78991 19 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 79991 19 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 80991 19 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 81992 19 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 82992 19 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 83992 19 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3722 0 0 0 84992 19 0 0 25 0 1 0 478689953 16748544 3700 4294967295 134512640 134672761 3221224576 3221223680 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4089 3700 603 41 0 4048 0
vsize: 16356
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3724 0 0 0 85991 19 0 0 25 0 1 0 478689953 16748544 3702 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3702 603 41 0 4048 0
vsize: 16356
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3724 0 0 0 86991 19 0 0 25 0 1 0 478689953 16748544 3702 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3702 603 41 0 4048 0
vsize: 16356
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3724 0 0 0 87992 19 0 0 25 0 1 0 478689953 16748544 3702 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3702 603 41 0 4048 0
vsize: 16356
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 3778 0 0 0 88992 19 0 0 25 0 1 0 478689953 17018880 3756 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3756 603 41 0 4114 0
vsize: 16620
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4053 0 0 0 89991 19 0 0 25 0 1 0 478689953 18100224 4031 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4419 4031 603 41 0 4378 0
vsize: 17676
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4057 0 0 0 90991 20 0 0 25 0 1 0 478689953 18243584 4035 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4454 4035 603 41 0 4413 0
vsize: 17816
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4093 0 0 0 91992 20 0 0 25 0 1 0 478689953 18378752 4071 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4487 4071 603 41 0 4446 0
vsize: 17948
[startup+930.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4093 0 0 0 92992 20 0 0 25 0 1 0 478689953 18378752 4071 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4487 4071 603 41 0 4446 0
vsize: 17948
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4093 0 0 0 93992 20 0 0 25 0 1 0 478689953 18378752 4071 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4487 4071 603 41 0 4446 0
vsize: 17948
[startup+950.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4093 0 0 0 94992 20 0 0 25 0 1 0 478689953 18378752 4071 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4487 4071 603 41 0 4446 0
vsize: 17948
[startup+960.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4093 0 0 0 95992 20 0 0 25 0 1 0 478689953 18378752 4071 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4487 4071 603 41 0 4446 0
vsize: 17948
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4093 0 0 0 96992 20 0 0 25 0 1 0 478689953 18378752 4071 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4487 4071 603 41 0 4446 0
vsize: 17948
[startup+980.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4093 0 0 0 97992 20 0 0 25 0 1 0 478689953 18378752 4071 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4487 4071 603 41 0 4446 0
vsize: 17948
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4117 0 0 0 98992 20 0 0 25 0 1 0 478689953 18378752 4095 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4487 4095 603 41 0 4446 0
vsize: 17948
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4117 0 0 0 99992 20 0 0 25 0 1 0 478689953 18378752 4095 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4487 4095 603 41 0 4446 0
vsize: 17948
[startup+1010.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4117 0 0 0 100993 20 0 0 25 0 1 0 478689953 18378752 4095 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4487 4095 603 41 0 4446 0
vsize: 17948
[startup+1020.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4161 0 0 0 101992 21 0 0 25 0 1 0 478689953 18649088 4139 4294967295 134512640 134672761 3221224576 3221223680 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4553 4139 603 41 0 4512 0
vsize: 18212
[startup+1030.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4161 0 0 0 102993 21 0 0 25 0 1 0 478689953 18649088 4139 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4553 4139 603 41 0 4512 0
vsize: 18212
[startup+1040.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4163 0 0 0 103993 21 0 0 25 0 1 0 478689953 18649088 4141 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4553 4141 603 41 0 4512 0
vsize: 18212
[startup+1050.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4163 0 0 0 104993 21 0 0 25 0 1 0 478689953 18649088 4141 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4553 4141 603 41 0 4512 0
vsize: 18212
[startup+1060.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4163 0 0 0 105993 21 0 0 25 0 1 0 478689953 18649088 4141 4294967295 134512640 134672761 3221224576 3221223644 1075346600 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4553 4141 603 41 0 4512 0
vsize: 18212
[startup+1070.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4163 0 0 0 106993 21 0 0 25 0 1 0 478689953 18649088 4141 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4553 4141 603 41 0 4512 0
vsize: 18212
[startup+1080.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4163 0 0 0 107993 21 0 0 25 0 1 0 478689953 18649088 4141 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4553 4141 603 41 0 4512 0
vsize: 18212
[startup+1090.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4163 0 0 0 108993 21 0 0 25 0 1 0 478689953 18649088 4141 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4553 4141 603 41 0 4512 0
vsize: 18212
[startup+1100.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4206 0 0 0 109993 21 0 0 25 0 1 0 478689953 18784256 4184 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4184 603 41 0 4545 0
vsize: 18344
[startup+1110.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4206 0 0 0 110993 21 0 0 25 0 1 0 478689953 18784256 4184 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4184 603 41 0 4545 0
vsize: 18344
[startup+1120.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4210 0 0 0 111993 21 0 0 25 0 1 0 478689953 18784256 4188 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4188 603 41 0 4545 0
vsize: 18344
[startup+1130.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4216 0 0 0 112994 21 0 0 25 0 1 0 478689953 18784256 4194 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4194 603 41 0 4545 0
vsize: 18344
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4216 0 0 0 113994 22 0 0 25 0 1 0 478689953 18784256 4194 4294967295 134512640 134672761 3221224576 3221223680 134559983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4194 603 41 0 4545 0
vsize: 18344
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4216 0 0 0 114994 22 0 0 25 0 1 0 478689953 18784256 4194 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4194 603 41 0 4545 0
vsize: 18344
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4216 0 0 0 115994 22 0 0 25 0 1 0 478689953 18784256 4194 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4194 603 41 0 4545 0
vsize: 18344
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4216 0 0 0 116994 22 0 0 25 0 1 0 478689953 18784256 4194 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4194 603 41 0 4545 0
vsize: 18344
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4216 0 0 0 117994 22 0 0 25 0 1 0 478689953 18784256 4194 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4194 603 41 0 4545 0
vsize: 18344
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4216 0 0 0 118994 22 0 0 25 0 1 0 478689953 18784256 4194 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4194 603 41 0 4545 0
vsize: 18344
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 20501
Raw data (stat): 20499 (minisat+) R 20498 18865 18864 0 -1 0 4216 0 0 0 119994 22 0 0 25 0 1 0 478689953 18784256 4194 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 4194 603 41 0 4545 0
vsize: 18344
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 20501
Raw data (stat): 20499 (minisat+) Z 20498 18865 18864 0 -1 12 4219 0 0 0 119995 23 0 0 25 0 1 0 478689953 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): 1200.04
CPU time (s): 1200.18
CPU user time (s): 1199.95
CPU system time (s): 0.233964
CPU usage (%): 100.012
Max. virtual memory (Kb): 18344
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####