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/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-sentoy.opb
MD5SUM	4df3e7eb358d27d446e34b975724a6c1
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-7772
Optimality of the best value was proved	NO
Number of terms in the objective function	60
Biggest coefficient in the objective function	974
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	9460
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	6000
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	26162
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01784
Number of variables	60
Total number of constraints	90
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	30
Minimum length of a constraint	1
Maximum length of a constraint	60
Trace number 21986

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-22 01:43:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12269 boxname=wulflinc31 idbench=944 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4df3e7eb358d27d446e34b975724a6c1  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-sentoy.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-sentoy.opb /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-sentoy.opb
IDLAUNCH: 12269
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        662976 kB
Buffers:         25544 kB
Cached:         321288 kB
SwapCached:        580 kB
Active:         110156 kB
Inactive:       238588 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        662724 kB
SwapTotal:     2097892 kB
SwapFree:      2096356 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            17224 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:03:09 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 12269 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  29]---> Adder-cost: 448   maxlim: 11620   bits: 15/14
c ---[  28]---> Adder-cost: 408   maxlim: 6087   bits: 14/13
c ---[  27]---> Adder-cost: 432   maxlim: 9310   bits: 14/14
c ---[  26]---> Adder-cost: 468   maxlim: 11096   bits: 15/14
c ---[  25]---> Adder-cost: 444   maxlim: 10275   bits: 14/14
c ---[  24]---> Adder-cost: 458   maxlim: 10302   bits: 14/14
c ---[  23]---> Adder-cost: 436   maxlim: 13436   bits: 15/14
c ---[  22]---> Adder-cost: 428   maxlim: 9755   bits: 14/14
c ---[  21]---> Adder-cost: 412   maxlim: 6448   bits: 14/13
c ---[  20]---> Adder-cost: 464   maxlim: 10002   bits: 14/14
c ---[  19]---> Adder-cost: 426   maxlim: 9583   bits: 14/14
c ---[  18]---> Adder-cost: 424   maxlim: 9848   bits: 14/14
c ---[  17]---> Adder-cost: 364   maxlim: 5722   bits: 14/13
c ---[  16]---> Adder-cost: 452   maxlim: 10594   bits: 15/14
c ---[  15]---> Adder-cost: 434   maxlim: 10081   bits: 14/14
c ---[  14]---> Adder-cost: 442   maxlim: 9196   bits: 14/14
c ---[  13]---> Adder-cost: 456   maxlim: 12391   bits: 15/14
c ---[  12]---> Adder-cost: 450   maxlim: 14161   bits: 15/14
c ---[  11]---> Adder-cost: 418   maxlim: 12220   bits: 15/14
c ---[  10]---> Adder-cost: 420   maxlim: 12782   bits: 15/14
c ---[   9]---> Adder-cost: 460   maxlim: 11486   bits: 15/14
c ---[   8]---> Adder-cost: 436   maxlim: 8903   bits: 14/14
c ---[   7]---> Adder-cost: 456   maxlim: 10103   bits: 14/14
c ---[   6]---> Adder-cost: 380   maxlim: 6238   bits: 14/13
c ---[   5]---> Adder-cost: 430   maxlim: 10469   bits: 15/14
c ---[   4]---> Adder-cost: 438   maxlim: 9149   bits: 14/14
c ---[   3]---> Adder-cost: 420   maxlim: 13773   bits: 15/14
c ---[   2]---> Adder-cost: 448   maxlim: 9436   bits: 14/14
c ---[   1]---> Adder-cost: 456   maxlim: 8907   bits: 14/14
c ---[   0]---> Adder-cost: 408   maxlim: 13608   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   89253   318894 |   29751       0        0     nan |  0.000 % |
c |       100 |   89253   318894 |   32726     100     1024    10.2 |  1.712 % |
c ==============================================================================
c [1mFound solution: -1341[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 391   maxlim: 1341   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       191 |   91914   328410 |   30638     191     1682     8.8 |  1.712 % |
c |       291 |   91914   328410 |   33701     291     5081    17.5 |  1.713 % |
c |       442 |   91914   328410 |   37071     442     6547    14.8 |  1.713 % |
c |       667 |   91914   328410 |   40779     667     9757    14.6 |  1.713 % |
c |      1005 |   91914   328410 |   44857    1005    25715    25.6 |  1.713 % |
c |      1512 |   91914   328410 |   49342    1512    35570    23.5 |  1.713 % |
c ==============================================================================
c [1mFound solution: -2964[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 5   maxlim: 2964   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1687 |   91959   328591 |   30653    1687    40255    23.9 |  1.713 % |
c |      1789 |   91959   328591 |   33718    1789    41500    23.2 |  1.763 % |
c |      1939 |   91959   328591 |   37090    1939    49114    25.3 |  1.763 % |
c |      2164 |   91959   328591 |   40799    2164    53289    24.6 |  1.763 % |
c |      2502 |   91959   328591 |   44879    2502    65456    26.2 |  1.763 % |
c |      3008 |   91953   328574 |   49366    3007    82188    27.3 |  1.770 % |
c |      3767 |   91953   328574 |   54303    3766   119856    31.8 |  1.770 % |
c |      4906 |   91953   328574 |   59734    4905   138064    28.1 |  1.770 % |
c |      6614 |   91953   328574 |   65707    6613   213845    32.3 |  1.770 % |
c |      9177 |   91953   328574 |   72278    9176   324329    35.3 |  1.770 % |
c |     13023 |   91947   328557 |   79505   13021   494473    38.0 |  1.778 % |
c |     18790 |   91947   328557 |   87456   18788   814579    43.4 |  1.778 % |
c ==============================================================================
c [1mFound solution: -4257[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4257   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23549 |   91961   328620 |   30653   23547  1019723    43.3 |  1.778 % |
c |     23649 |   91961   328620 |   33718   23647  1020545    43.2 |  1.806 % |
c |     23799 |   91961   328620 |   37090   23797  1025206    43.1 |  1.806 % |
c |     24024 |   91961   328620 |   40799   24022  1029449    42.9 |  1.806 % |
c |     24362 |   91961   328620 |   44879   24360  1043679    42.8 |  1.806 % |
c |     24868 |   91961   328620 |   49366   24866  1055658    42.5 |  1.806 % |
c |     25630 |   91961   328620 |   54303   25628  1083665    42.3 |  1.806 % |
c |     26770 |   91961   328620 |   59734   26768  1139583    42.6 |  1.806 % |
c |     28479 |   91961   328620 |   65707   28477  1195792    42.0 |  1.806 % |
c |     31041 |   91961   328620 |   72278   31039  1340127    43.2 |  1.806 % |
c |     34887 |   91961   328620 |   79505   34885  1524955    43.7 |  1.806 % |
c |     40654 |   91955   328603 |   87456   40651  1777207    43.7 |  1.813 % |
c |     49304 |   91955   328603 |   96202   49301  2369545    48.1 |  1.813 % |
c |     62280 |   91955   328603 |  105822   62277  3051067    49.0 |  1.813 % |
c |     81741 |   91955   328603 |  116404   81738  3924591    48.0 |  1.813 % |
c ==============================================================================
c [1mFound solution: -4363[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4363   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86781 |   91958   328635 |   30652   86778  4107084    47.3 |  1.813 % |
c |     86881 |   91958   328635 |   33717   15694   503426    32.1 |  1.835 % |
c |     87033 |   91958   328635 |   37088   15846   505886    31.9 |  1.835 % |
c |     87258 |   91958   328635 |   40797   16071   508525    31.6 |  1.835 % |
c |     87596 |   91958   328635 |   44877   16409   523526    31.9 |  1.835 % |
c |     88103 |   91958   328635 |   49365   16916   534759    31.6 |  1.835 % |
c |     88863 |   91958   328635 |   54301   17676   561876    31.8 |  1.835 % |
c |     90003 |   91958   328635 |   59732   18816   603645    32.1 |  1.835 % |
c |     91711 |   91958   328635 |   65705   20524   670414    32.7 |  1.835 % |
c |     94273 |   91958   328635 |   72275   23086   791440    34.3 |  1.835 % |
c |     98118 |   91958   328635 |   79503   26931   955009    35.5 |  1.835 % |
c |    103884 |   91958   328635 |   87453   32697  1219534    37.3 |  1.835 % |
c |    112534 |   91952   328618 |   96199   41346  1687230    40.8 |  1.842 % |
c |    125508 |   91952   328618 |  105819   54320  2269064    41.8 |  1.842 % |
c |    144969 |   91952   328618 |  116400   73781  3488461    47.3 |  1.842 % |
c |    174161 |   91952   328618 |  128041  102973  5276301    51.2 |  1.842 % |
c |    217950 |   91946   328601 |  140845   33573  1485357    44.2 |  1.850 % |
c ==============================================================================
c [1mFound solution: -4408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4408   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    219901 |   91953   328655 |   30651   35524  1564118    44.0 |  1.850 % |
#### 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.78 0.87 0.88 2/54 8783
Raw data (stat): 8783 (runsolver) R 8782 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549835518 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.81 0.88 0.88 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 2052 0 0 0 993 5 0 0 25 0 1 0 549835518 10334208 2021 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2523 2021 603 41 0 2482 0
vsize: 10092
[startup+20.0024 s]
Raw data (loadavg): 0.84 0.88 0.88 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 2182 0 0 0 1993 6 0 0 25 0 1 0 549835518 10760192 2151 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2627 2151 603 41 0 2586 0
vsize: 10508
[startup+30.0028 s]
Raw data (loadavg): 0.86 0.88 0.88 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 2325 0 0 0 2991 7 0 0 25 0 1 0 549835518 11427840 2294 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2790 2294 603 41 0 2749 0
vsize: 11160
[startup+40.0045 s]
Raw data (loadavg): 0.88 0.89 0.88 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 2459 0 0 0 3991 8 0 0 25 0 1 0 549835518 11968512 2428 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2922 2428 603 41 0 2881 0
vsize: 11688
[startup+50.0051 s]
Raw data (loadavg): 0.90 0.89 0.88 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 2588 0 0 0 4990 8 0 0 25 0 1 0 549835518 12505088 2557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3053 2557 603 41 0 3012 0
vsize: 12212
[startup+60.0056 s]
Raw data (loadavg): 0.92 0.89 0.88 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 2681 0 0 0 5990 9 0 0 25 0 1 0 549835518 12910592 2650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3152 2650 603 41 0 3111 0
vsize: 12608
[startup+70.0069 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 2777 0 0 0 6990 9 0 0 25 0 1 0 549835518 13381632 2746 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3267 2746 603 41 0 3226 0
vsize: 13068
[startup+80.0079 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 2873 0 0 0 7989 10 0 0 25 0 1 0 549835518 13651968 2842 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3333 2842 603 41 0 3292 0
vsize: 13332
[startup+90.0083 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 2997 0 0 0 8989 11 0 0 25 0 1 0 549835518 14192640 2966 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3465 2966 603 41 0 3424 0
vsize: 13860
[startup+100.009 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 3129 0 0 0 9988 11 0 0 25 0 1 0 549835518 14733312 3098 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3597 3098 603 41 0 3556 0
vsize: 14388
[startup+110.01 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 3243 0 0 0 10988 12 0 0 25 0 1 0 549835518 15134720 3212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3695 3212 603 41 0 3654 0
vsize: 14780
[startup+120.011 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 3343 0 0 0 11987 13 0 0 25 0 1 0 549835518 15532032 3312 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3792 3312 603 41 0 3751 0
vsize: 15168
[startup+130.011 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 3481 0 0 0 12987 13 0 0 25 0 1 0 549835518 16203776 3450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3956 3450 603 41 0 3915 0
vsize: 15824
[startup+140.012 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 3603 0 0 0 13986 14 0 0 25 0 1 0 549835518 16601088 3572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4053 3572 603 41 0 4012 0
vsize: 16212
[startup+150.013 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 3673 0 0 0 14986 14 0 0 25 0 1 0 549835518 16871424 3642 4294967295 134512640 134672761 3221224544 3221223728 134558324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4119 3642 603 41 0 4078 0
vsize: 16476
[startup+160.014 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 3759 0 0 0 15986 15 0 0 25 0 1 0 549835518 17399808 3728 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4248 3728 603 41 0 4207 0
vsize: 16992
[startup+170.015 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 3850 0 0 0 16986 15 0 0 25 0 1 0 549835518 17801216 3819 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4346 3819 603 41 0 4305 0
vsize: 17384
[startup+180.015 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 3951 0 0 0 17985 15 0 0 25 0 1 0 549835518 18202624 3920 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4444 3920 603 41 0 4403 0
vsize: 17776
[startup+190.016 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 4024 0 0 0 18985 15 0 0 25 0 1 0 549835518 18472960 3993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4510 3993 603 41 0 4469 0
vsize: 18040
[startup+200.016 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 4097 0 0 0 19985 16 0 0 25 0 1 0 549835518 18743296 4066 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4576 4066 603 41 0 4535 0
vsize: 18304
[startup+210.016 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 4193 0 0 0 20985 16 0 0 25 0 1 0 549835518 19148800 4162 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4675 4162 603 41 0 4634 0
vsize: 18700
[startup+220.018 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 4287 0 0 0 21984 17 0 0 25 0 1 0 549835518 19554304 4256 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4774 4256 603 41 0 4733 0
vsize: 19096
[startup+230.017 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 4389 0 0 0 22984 17 0 0 25 0 1 0 549835518 19959808 4358 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4873 4358 603 41 0 4832 0
vsize: 19492
[startup+240.018 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 4487 0 0 0 23984 18 0 0 25 0 1 0 549835518 20361216 4456 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4971 4456 603 41 0 4930 0
vsize: 19884
[startup+250.019 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 4589 0 0 0 24984 18 0 0 25 0 1 0 549835518 20762624 4558 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5069 4558 603 41 0 5028 0
vsize: 20276
[startup+260.02 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 4706 0 0 0 25984 18 0 0 25 0 1 0 549835518 21168128 4675 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5168 4675 603 41 0 5127 0
vsize: 20672
[startup+270.02 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 4832 0 0 0 26983 18 0 0 25 0 1 0 549835518 21700608 4801 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5298 4801 603 41 0 5257 0
vsize: 21192
[startup+280.02 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 4935 0 0 0 27983 19 0 0 25 0 1 0 549835518 22110208 4904 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4904 603 41 0 5357 0
vsize: 21592
[startup+290.021 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 5024 0 0 0 28983 19 0 0 25 0 1 0 549835518 22515712 4993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5497 4993 603 41 0 5456 0
vsize: 21988
[startup+300.02 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 5130 0 0 0 29983 19 0 0 25 0 1 0 549835518 22913024 5099 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5594 5099 603 41 0 5553 0
vsize: 22376
[startup+310.022 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 5227 0 0 0 30983 20 0 0 25 0 1 0 549835518 23318528 5196 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5693 5196 603 41 0 5652 0
vsize: 22772
[startup+320.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 5315 0 0 0 31983 20 0 0 25 0 1 0 549835518 23724032 5284 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5792 5284 603 41 0 5751 0
vsize: 23168
[startup+330.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 5405 0 0 0 32983 21 0 0 25 0 1 0 549835518 23990272 5374 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5374 603 41 0 5816 0
vsize: 23428
[startup+340.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 5498 0 0 0 33982 21 0 0 25 0 1 0 549835518 24387584 5467 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5467 603 41 0 5913 0
vsize: 23816
[startup+350.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 5590 0 0 0 34982 21 0 0 25 0 1 0 549835518 24788992 5559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6052 5559 603 41 0 6011 0
vsize: 24208
[startup+360.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 5758 0 0 0 35982 22 0 0 25 0 1 0 549835518 25464832 5727 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6217 5727 603 41 0 6176 0
vsize: 24868
[startup+370.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 5881 0 0 0 36982 22 0 0 25 0 1 0 549835518 26263552 5850 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6412 5850 603 41 0 6371 0
vsize: 25648
[startup+380.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6058 0 0 0 37981 23 0 0 25 0 1 0 549835518 26931200 6027 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6575 6027 603 41 0 6534 0
vsize: 26300
[startup+390.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6167 0 0 0 38981 23 0 0 25 0 1 0 549835518 27336704 6136 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6674 6136 603 41 0 6633 0
vsize: 26696
[startup+400.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6286 0 0 0 39981 23 0 0 25 0 1 0 549835518 27869184 6255 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6804 6255 603 41 0 6763 0
vsize: 27216
[startup+410.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6425 0 0 0 40981 23 0 0 25 0 1 0 549835518 28409856 6394 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6936 6394 603 41 0 6895 0
vsize: 27744
[startup+420.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6561 0 0 0 41981 24 0 0 25 0 1 0 549835518 28950528 6530 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7068 6530 603 41 0 7027 0
vsize: 28272
[startup+430.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6693 0 0 0 42981 24 0 0 25 0 1 0 549835518 29487104 6662 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7199 6662 603 41 0 7158 0
vsize: 28796
[startup+440.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6818 0 0 0 43981 25 0 0 25 0 1 0 549835518 30023680 6787 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7330 6787 603 41 0 7289 0
vsize: 29320
[startup+450.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 44980 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+460.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 45981 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+470.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 46981 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+480.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 47981 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+490.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 48981 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+500.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 49981 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+510.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 50981 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+520.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 51982 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 52982 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+540.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 53982 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 54982 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+560.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 55982 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+570.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 56983 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+580.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 57983 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+590.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 58983 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+600.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 59983 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 60983 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 61983 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+630.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 62984 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+640.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 63984 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+650.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 64984 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+660.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 65984 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+670.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 66985 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223744 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+680.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 67985 25 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+690.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 68985 26 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+700.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 69985 26 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 70985 26 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+720.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 71985 26 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+730.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 72985 26 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+740.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 73985 26 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+750.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 74985 26 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+760.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 75986 26 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+770.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 76985 27 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+780.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 77985 27 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+790.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 78985 27 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+800.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6926 0 0 0 79985 27 0 0 25 0 1 0 549835518 30621696 6895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7476 6895 603 41 0 7435 0
vsize: 29904
[startup+810.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 6975 0 0 0 80985 27 0 0 25 0 1 0 549835518 30756864 6944 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7509 6944 603 41 0 7468 0
vsize: 30036
[startup+820.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7086 0 0 0 81985 27 0 0 25 0 1 0 549835518 31293440 7055 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7640 7055 603 41 0 7599 0
vsize: 30560
[startup+830.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7216 0 0 0 82985 28 0 0 25 0 1 0 549835518 31834112 7185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7772 7185 603 41 0 7731 0
vsize: 31088
[startup+840.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7297 0 0 0 83985 28 0 0 25 0 1 0 549835518 32096256 7266 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7836 7266 603 41 0 7795 0
vsize: 31344
[startup+850.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7358 0 0 0 84985 28 0 0 25 0 1 0 549835518 32366592 7327 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7902 7327 603 41 0 7861 0
vsize: 31608
[startup+860.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7428 0 0 0 85985 28 0 0 25 0 1 0 549835518 32636928 7397 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7968 7397 603 41 0 7927 0
vsize: 31872
[startup+870.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7507 0 0 0 86985 29 0 0 25 0 1 0 549835518 33034240 7476 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8065 7476 603 41 0 8024 0
vsize: 32260
[startup+880.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7593 0 0 0 87985 29 0 0 25 0 1 0 549835518 33300480 7562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8130 7562 603 41 0 8089 0
vsize: 32520
[startup+890.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7677 0 0 0 88985 29 0 0 25 0 1 0 549835518 33705984 7646 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8229 7646 603 41 0 8188 0
vsize: 32916
[startup+900.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7750 0 0 0 89985 29 0 0 25 0 1 0 549835518 33968128 7719 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8293 7719 603 41 0 8252 0
vsize: 33172
[startup+910.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7838 0 0 0 90984 30 0 0 25 0 1 0 549835518 34369536 7807 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8391 7807 603 41 0 8350 0
vsize: 33564
[startup+920.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 7955 0 0 0 91984 30 0 0 25 0 1 0 549835518 34775040 7924 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8490 7924 603 41 0 8449 0
vsize: 33960
[startup+930.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 8061 0 0 0 92984 31 0 0 25 0 1 0 549835518 35176448 8030 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8588 8030 603 41 0 8547 0
vsize: 34352
[startup+940.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 8142 0 0 0 93984 31 0 0 25 0 1 0 549835518 35581952 8111 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8687 8111 603 41 0 8646 0
vsize: 34748
[startup+950.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 8230 0 0 0 94984 31 0 0 25 0 1 0 549835518 35979264 8199 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8784 8199 603 41 0 8743 0
vsize: 35136
[startup+960.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 8320 0 0 0 95984 32 0 0 25 0 1 0 549835518 36245504 8289 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8849 8289 603 41 0 8808 0
vsize: 35396
[startup+970.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 8409 0 0 0 96984 32 0 0 25 0 1 0 549835518 36646912 8378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8947 8378 603 41 0 8906 0
vsize: 35788
[startup+980.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 8532 0 0 0 97983 32 0 0 25 0 1 0 549835518 37183488 8501 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9078 8501 603 41 0 9037 0
vsize: 36312
[startup+990.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 8750 0 0 0 98982 33 0 0 25 0 1 0 549835518 37998592 8719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9277 8719 603 41 0 9236 0
vsize: 37108
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 8906 0 0 0 99982 34 0 0 25 0 1 0 549835518 38666240 8875 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9440 8875 603 41 0 9399 0
vsize: 37760
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8783
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9002 0 0 0 100981 34 0 0 25 0 1 0 549835518 39067648 8971 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9538 8971 603 41 0 9497 0
vsize: 38152
[startup+1020.06 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 8824
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9086 0 0 0 101979 36 0 0 25 0 1 0 549835518 39337984 9055 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9604 9055 603 41 0 9563 0
vsize: 38416
[startup+1030.06 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 8836
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9177 0 0 0 102979 36 0 0 25 0 1 0 549835518 39743488 9146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9703 9146 603 41 0 9662 0
vsize: 38812
[startup+1040.06 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 8836
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9246 0 0 0 103979 37 0 0 25 0 1 0 549835518 40009728 9215 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9768 9215 603 41 0 9727 0
vsize: 39072
[startup+1050.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 8836
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9316 0 0 0 104979 37 0 0 25 0 1 0 549835518 40280064 9285 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9834 9285 603 41 0 9793 0
vsize: 39336
[startup+1060.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 8836
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9394 0 0 0 105979 37 0 0 25 0 1 0 549835518 40681472 9363 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9932 9363 603 41 0 9891 0
vsize: 39728
[startup+1070.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 8836
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9476 0 0 0 106979 37 0 0 25 0 1 0 549835518 40955904 9445 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9999 9445 603 41 0 9958 0
vsize: 39996
[startup+1080.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 8836
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9563 0 0 0 107978 38 0 0 25 0 1 0 549835518 41357312 9532 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10097 9532 603 41 0 10056 0
vsize: 40388
[startup+1090.06 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 8836
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9642 0 0 0 108979 38 0 0 25 0 1 0 549835518 41623552 9611 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10162 9611 603 41 0 10121 0
vsize: 40648
[startup+1100.06 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9719 0 0 0 109978 38 0 0 25 0 1 0 549835518 41889792 9688 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10227 9688 603 41 0 10186 0
vsize: 40908
[startup+1110.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9800 0 0 0 110978 39 0 0 25 0 1 0 549835518 42291200 9769 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10325 9769 603 41 0 10284 0
vsize: 41300
[startup+1120.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9886 0 0 0 111978 39 0 0 25 0 1 0 549835518 42553344 9855 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10389 9855 603 41 0 10348 0
vsize: 41556
[startup+1130.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9907 0 0 0 112978 39 0 0 25 0 1 0 549835518 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1140.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9907 0 0 0 113978 39 0 0 25 0 1 0 549835518 42684416 9876 4294967295 134512640 134672761 3221224544 3221223648 134559802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1150.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9907 0 0 0 114978 39 0 0 25 0 1 0 549835518 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9907 0 0 0 115979 39 0 0 25 0 1 0 549835518 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9907 0 0 0 116979 39 0 0 25 0 1 0 549835518 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9907 0 0 0 117979 39 0 0 25 0 1 0 549835518 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9907 0 0 0 118979 39 0 0 25 0 1 0 549835518 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 8838
Raw data (stat): 8783 (minisat+) R 8782 23176 23175 0 -1 0 9907 0 0 0 119978 39 0 0 25 0 1 0 549835518 42684416 9876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9876 603 41 0 10380 0
vsize: 41684
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 8838
Raw data (stat): 8783 (minisat+) Z 8782 23176 23175 0 -1 12 9910 0 0 0 119978 41 0 0 25 0 1 0 549835518 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.09
CPU time (s): 1200.21
CPU user time (s): 1199.79
CPU system time (s): 0.416936
CPU usage (%): 100.01
Max. virtual memory (Kb): 41684
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####