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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:98.opb
MD5SUM	a89f4ed95903fddf213992506514bcf0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	16
Optimality of the best value was proved	NO
Number of terms in the objective function	906
Biggest coefficient in the objective function	553
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	2526
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	553
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	2526
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04184
Number of variables	906
Total number of constraints	1944
Number of constraints which are clauses	852
Number of constraints which are cardinality constraints (but not clauses)	1092
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 31749

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-05-27 05:59:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23125 boxname=wulflinc19 idbench=371 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a89f4ed95903fddf213992506514bcf0  /oldhome/oroussel/tmp/wulflinc19/normalized-10:20:4.5:0.95:98.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-10:20:4.5:0.95:98.opb
IDLAUNCH: 23125
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        833668 kB
Buffers:         33288 kB
Cached:         141532 kB
SwapCached:        756 kB
Active:          51644 kB
Inactive:       125480 kB
HighTotal:      131008 kB
HighFree:        53256 kB
LowTotal:       903652 kB
LowFree:        780412 kB
SwapTotal:     2097892 kB
SwapFree:      2096428 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5420 kB
Slab:            18128 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 06:19:37 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 23125 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1038 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 187]---> BDD-cost:    5
c ---[ 186]---> BDD-cost:    8
c ---[ 185]---> BDD-cost:   14
c ---[ 184]---> BDD-cost:   14
c ---[ 183]---> BDD-cost:   17
c ---[ 182]---> BDD-cost:   14
c ---[ 181]---> BDD-cost:   23
c ---[ 180]---> BDD-cost:   20
c ---[ 179]---> BDD-cost:   29
c ---[ 178]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   38
c ---[ 176]---> BDD-cost:   32
c ---[ 175]---> BDD-cost:   32
c ---[ 174]---> BDD-cost:   23
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   20
c ---[ 171]---> BDD-cost:   20
c ---[ 170]---> BDD-cost:   14
c ---[ 169]---> BDD-cost:   14
c ---[ 168]---> BDD-cost:    8
c ---[ 167]---> BDD-cost:    8
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:   17
c ---[ 163]---> BDD-cost:   18
c ---[ 162]---> BDD-cost:   18
c ---[ 161]---> BDD-cost:   35
c ---[ 160]---> BDD-cost:   35
c ---[ 159]---> BDD-cost:   41
c ---[ 158]---> BDD-cost:   35
c ---[ 157]---> BDD-cost:   38
c ---[ 156]---> BDD-cost:   38
c ---[ 155]---> BDD-cost:   41
c ---[ 154]---> BDD-cost:   35
c ---[ 153]---> BDD-cost:   38
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   20
c ---[ 150]---> BDD-cost:   17
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:   11
c ---[ 145]---> BDD-cost:   14
c ---[ 144]---> BDD-cost:   17
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   29
c ---[ 141]---> BDD-cost:   41
c ---[ 140]---> BDD-cost:   44
c ---[ 139]---> BDD-cost:   44
c ---[ 138]---> BDD-cost:   38
c ---[ 137]---> BDD-cost:   39
c ---[ 136]---> BDD-cost:   41
c ---[ 135]---> BDD-cost:   44
c ---[ 134]---> BDD-cost:   44
c ---[ 133]---> BDD-cost:   41
c ---[ 132]---> BDD-cost:   29
c ---[ 131]---> BDD-cost:   29
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   26
c ---[ 128]---> BDD-cost:   14
c ---[ 127]---> BDD-cost:    8
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   14
c ---[ 124]---> BDD-cost:   17
c ---[ 123]---> BDD-cost:   21
c ---[ 122]---> BDD-cost:   29
c ---[ 121]---> BDD-cost:   35
c ---[ 120]---> BDD-cost:   44
c ---[ 119]---> BDD-cost:   47
c ---[ 118]---> BDD-cost:   44
c ---[ 117]---> BDD-cost:   44
c ---[ 116]---> BDD-cost:   44
c ---[ 115]---> BDD-cost:   41
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   35
c ---[ 112]---> BDD-cost:   32
c ---[ 111]---> BDD-cost:   29
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   20
c ---[ 108]---> BDD-cost:    6
c ---[ 107]---> BDD-cost:    5
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   20
c ---[ 104]---> BDD-cost:   23
c ---[ 103]---> BDD-cost:   26
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:   38
c ---[ 100]---> BDD-cost:   35
c ---[  99]---> BDD-cost:   41
c ---[  98]---> BDD-cost:   44
c ---[  97]---> BDD-cost:   41
c ---[  96]---> BDD-cost:   38
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:   38
c ---[  93]---> BDD-cost:   29
c ---[  92]---> BDD-cost:   20
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   20
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:    5
c ---[  87]---> BDD-cost:    5
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   20
c ---[  83]---> BDD-cost:   32
c ---[  82]---> BDD-cost:   41
c ---[  81]---> BDD-cost:   38
c ---[  80]---> BDD-cost:   35
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   35
c ---[  77]---> BDD-cost:   44
c ---[  76]---> BDD-cost:   35
c ---[  75]---> BDD-cost:   38
c ---[  74]---> BDD-cost:   35
c ---[  73]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   23
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   17
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   23
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   38
c ---[  60]---> BDD-cost:   32
c ---[  59]---> BDD-cost:   32
c ---[  58]---> BDD-cost:   35
c ---[  57]---> BDD-cost:   38
c ---[  56]---> BDD-cost:   32
c ---[  55]---> BDD-cost:   35
c ---[  54]---> BDD-cost:   29
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   29
c ---[  51]---> BDD-cost:   23
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   11
c ---[  47]---> BDD-cost:    8
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   20
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   35
c ---[  40]---> BDD-cost:   35
c ---[  39]---> BDD-cost:   35
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:   26
c ---[  36]---> BDD-cost:   23
c ---[  35]---> BDD-cost:   23
c ---[  34]---> BDD-cost:   23
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   17
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   20
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   20
c ---[  20]---> BDD-cost:   20
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   20
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    8
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:   14
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   14
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11181    31975 |    3727       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 959[0m
c ---[   0]---> Sorter-cost:69497     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   98065   235598 |   32688       0        0     nan |  0.000 % |
c |       100 |   97945   235356 |   35956      96     1183    12.3 |  0.394 % |
c ==============================================================================
c [1mFound solution: 132[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       131 |  136862   326344 |   45620     126     1575    12.5 |  0.394 % |
c |       231 |  136649   325872 |   50182     222     2400    10.8 |  0.554 % |
c |       381 |  136566   325685 |   55200     371     4150    11.2 |  0.591 % |
c |       606 |  136566   325685 |   60720     596     6346    10.6 |  0.591 % |
c |       943 |  136566   325685 |   66792     933     8111     8.7 |  0.591 % |
c |      1449 |  136434   325390 |   73471    1437    14754    10.3 |  0.671 % |
c |      2209 |  136345   325187 |   80818    2196    31136    14.2 |  0.712 % |
c |      3348 |  135750   323871 |   88900    3322    50719    15.3 |  1.106 % |
c |      5058 |  135114   322442 |   97790    5020    71012    14.1 |  1.471 % |
c |      7620 |  134367   320766 |  107569    7476   135375    18.1 |  1.979 % |
c |     11465 |  134060   320072 |  118326   11311   205024    18.1 |  2.171 % |
c |     17232 |  133659   319161 |  130159   17043   364167    21.4 |  2.450 % |
c |     25881 |  133659   319161 |  143175   25692   627411    24.4 |  2.450 % |
c ==============================================================================
c [1mFound solution: 100[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34908 |  133443   318742 |   44481   34692   882375    25.4 |  2.450 % |
c |     35008 |  133443   318742 |   48929   34792   883822    25.4 |  2.667 % |
c |     35159 |  133083   317915 |   53822   34933   885011    25.3 |  2.897 % |
c |     35384 |  132785   317236 |   59204   34989   885325    25.3 |  3.066 % |
c |     35721 |  132785   317236 |   65124   35326   890308    25.2 |  3.066 % |
c |     36228 |  132785   317236 |   71637   35833   900634    25.1 |  3.066 % |
c |     36990 |  132671   316976 |   78800   36592   911872    24.9 |  3.121 % |
c |     38129 |  132671   316976 |   86680   37731   957809    25.4 |  3.121 % |
c |     39838 |  132671   316976 |   95348   39440  1007183    25.5 |  3.121 % |
c |     42403 |  132671   316976 |  104883   42005  1047666    24.9 |  3.121 % |
c ==============================================================================
c [1mFound solution: 89[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45719 |  132741   317174 |   44247   45321  1112617    24.5 |  3.121 % |
c |     45820 |  132741   317174 |   48671   45422  1114217    24.5 |  3.120 % |
c |     45970 |  132681   317044 |   53538   45566  1116344    24.5 |  3.173 % |
c |     46196 |  132539   316726 |   58892   45787  1120083    24.5 |  3.267 % |
c |     46535 |  132539   316726 |   64782   46126  1124906    24.4 |  3.267 % |
c |     47042 |  132530   316707 |   71260   46630  1144255    24.5 |  3.274 % |
c |     47803 |  132530   316707 |   78386   47391  1163560    24.6 |  3.274 % |
c |     48943 |  132530   316707 |   86224   48531  1185721    24.4 |  3.274 % |
c |     50652 |  132530   316707 |   94847   50240  1229199    24.5 |  3.274 % |
c |     53214 |  132528   316703 |  104332   52800  1342600    25.4 |  3.276 % |
c |     57058 |  132524   316695 |  114765   56636  1423156    25.1 |  3.279 % |
c |     62824 |  132524   316695 |  126241   62402  1547383    24.8 |  3.279 % |
c |     71475 |  132520   316686 |  138866   71048  1961678    27.6 |  3.280 % |
c |     84449 |  132505   316652 |  152752   84019  2524728    30.0 |  3.292 % |
c ==============================================================================
c [1mFound solution: 71[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85791 |  132621   316968 |   44207   85361  2565105    30.1 |  3.292 % |
c |     85892 |  132621   316968 |   48627   20576   545228    26.5 |  3.290 % |
c |     86042 |  132621   316968 |   53490   20726   546710    26.4 |  3.290 % |
c |     86267 |  132621   316968 |   58839   20951   548910    26.2 |  3.290 % |
c |     86604 |  132621   316968 |   64723   21288   553079    26.0 |  3.290 % |
c |     87110 |  132621   316968 |   71195   21794   583363    26.8 |  3.290 % |
c |     87869 |  132621   316968 |   78315   22553   598604    26.5 |  3.290 % |
c |     89008 |  132584   316891 |   86146   23691   622554    26.3 |  3.320 % |
c |     90716 |  132584   316891 |   94761   25399   650846    25.6 |  3.320 % |
c |     93278 |  132584   316891 |  104237   27961   724322    25.9 |  3.320 % |
c |     97123 |  132584   316891 |  114661   31806  1075400    33.8 |  3.320 % |
c |    102889 |  132584   316891 |  126127   37572  1291066    34.4 |  3.320 % |
c |    111538 |  132584   316891 |  138740   46221  2350342    50.9 |  3.320 % |
c |    124514 |  132584   316891 |  152614   59197  4144544    70.0 |  3.320 % |
c ==============================================================================
c [1mFound solution: 68[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    126224 |  132591   316914 |   44197   60907  4187539    68.8 |  3.320 % |
c |    126324 |  132591   316914 |   48616   19936  1802665    90.4 |  3.322 % |
c |    126476 |  132591   316914 |   53478   20088  1805539    89.9 |  3.322 % |
c |    126701 |  132591   316914 |   58826   20313  1811155    89.2 |  3.322 % |
c |    127039 |  132591   316914 |   64708   20651  1832976    88.8 |  3.322 % |
c |    127545 |  132591   316914 |   71179   21157  1836496    86.8 |  3.322 % |
c |    128304 |  132591   316914 |   78297   21916  1865065    85.1 |  3.322 % |
c |    129443 |  132591   316914 |   86127   23055  1888123    81.9 |  3.322 % |
c |    131151 |  132591   316914 |   94740   24763  1983029    80.1 |  3.322 % |
c |    133713 |  132591   316914 |  104214   27325  2024838    74.1 |  3.322 % |
c |    137557 |  132591   316914 |  114635   31169  2136748    68.6 |  3.322 % |
c |    143323 |  132591   316914 |  126099   36935  4189369   113.4 |  3.322 % |
c |    151972 |  132587   316905 |  138709   45581  4407036    96.7 |  3.323 % |
c |    164947 |  132465   316619 |  152580   58555  5024064    85.8 |  3.412 % |
c |    184412 |  132465   316619 |  167838   78020  7623876    97.7 |  3.412 % |
c ==============================================================================
c [1mFound solution: 67[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    197095 |  132301   316262 |   44100   90701  8886122    98.0 |  3.412 % |
c |    197195 |  132301   316262 |   48510   24436  1360111    55.7 |  3.537 % |
c |    197345 |  132301   316262 |   53361   24586  1364199    55.5 |  3.537 % |
c |    197571 |  132290   316239 |   58697   24807  1374683    55.4 |  3.546 % |
c |    197910 |  132290   316239 |   64566   25146  1379093    54.8 |  3.546 % |
c |    198416 |  132290   316239 |   71023   25652  1446731    56.4 |  3.546 % |
c |    199176 |  132290   316239 |   78125   26412  1468692    55.6 |  3.546 % |
c |    200315 |  132290   316239 |   85938   27551  1522689    55.3 |  3.546 % |
c |    202023 |  132290   316239 |   94532   29259  1580387    54.0 |  3.546 % |
c |    204585 |  132290   316239 |  103985   31821  1650237    51.9 |  3.546 % |
c |    208430 |  132290   316239 |  114384   35666  1784724    50.0 |  3.546 % |
c |    214196 |  132290   316239 |  125822   41432  2360684    57.0 |  3.546 % |
c |    222845 |  132290   316239 |  138404   50081  6002993   119.9 |  3.546 % |
c ==============================================================================
c [1mFound solution: 63[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    229804 |  132292   316270 |   44097   57035  6339200   111.1 |  3.546 % |
c |    229905 |  132292   316270 |   48506   22974  2901498   126.3 |  3.573 % |
c |    230055 |  132292   316270 |   53357   23124  2904349   125.6 |  3.573 % |
c |    230280 |  132292   316270 |   58693   23349  2909964   124.6 |  3.573 % |
c |    230618 |  132292   316270 |   64562   23687  2925173   123.5 |  3.573 % |
c |    231124 |  132292   316270 |   71018   24193  2933205   121.2 |  3.573 % |
c |    231883 |  132292   316270 |   78120   24952  2949533   118.2 |  3.573 % |
c |    233022 |  132292   316270 |   85932   26091  2971394   113.9 |  3.573 % |
c |    234731 |  132292   316270 |   94525   27800  3013791   108.4 |  3.573 % |
c |    237293 |  132292   316270 |  103978   30362  3199427   105.4 |  3.573 % |
c |    241138 |  132292   316270 |  114376   34207  3342197    97.7 |  3.573 % |
c |    246904 |  132270   316220 |  125813   39965  3636032    91.0 |  3.582 % |
c |    255553 |  132270   316220 |  138395   48614  4093710    84.2 |  3.582 % |
c |    268527 |  132242   316154 |  152234   61582  7533973   122.3 |  3.611 % |
c |    287989 |  132239   316147 |  167458   81040  8673069   107.0 |  3.614 % |
c |    317182 |  132239   316147 |  184204  110233  9873954    89.6 |  3.614 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  1518 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 1513
Raw data (stat): 1513 (runsolver) R 1512 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853819169 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99997 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 1518
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 1518
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0029 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 1518
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 1518
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0034 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 1518
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0938 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 1545
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0979 s]
Raw data (loadavg): 1.12 0.99 0.92 2/55 1573
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0988 s]
Raw data (loadavg): 1.11 0.99 0.92 2/55 1573
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0982 s]
Raw data (loadavg): 1.09 0.99 0.92 2/55 1573
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.098 s]
Raw data (loadavg): 1.07 0.99 0.92 2/55 1573
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.099 s]
Raw data (loadavg): 1.06 0.99 0.92 2/55 1573
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.099 s]
Raw data (loadavg): 1.05 0.99 0.92 2/55 1573
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.1 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 1573
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.1 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.1 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.1 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.1 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.101 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.101 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.102 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.102 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.102 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.102 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.102 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.102 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.102 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.103 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.104 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1575
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.105 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.106 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.106 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.107 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.106 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.107 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.107 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.107 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.108 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.108 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.108 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.108 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.108 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.108 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.109 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.11 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.111 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.111 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.111 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.111 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.112 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.112 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.111 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.112 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.112 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.112 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.112 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.112 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.113 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.113 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.113 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.113 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.115 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.115 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.115 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.115 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.115 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.116 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.117 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.117 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.117 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.118 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.117 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.118 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.119 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.119 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.119 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 0.99 0.92 1/53 1577
Raw data (stat): 1513 (minisat+_script) S 1512 10795 10794 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853819169 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.88
CPU user time (s): 1229.16
CPU system time (s): 0.71889
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####