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 6070

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 03:15:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4507 boxname=wulflinc17 idbench=371 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a89f4ed95903fddf213992506514bcf0  /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.95:98.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.95:98.opb /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.95:98.opb
IDLAUNCH: 4507
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        820064 kB
Buffers:         35984 kB
Cached:         143812 kB
SwapCached:       2376 kB
Active:          58944 kB
Inactive:       126212 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        819812 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23736 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:35:22 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4507 7 1200.23 10
#### 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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v785 v740 v420 v82 -v860 v744 v418 v859 -v784 -v501 v307 -v85 -v788 v419 -v86 -v63 v861 -v504 -v424 -v354 v306 v62 v863 -v789 -v573 -v505 v64 -v572 -v478 v441 -v353 -v312 v65 -v27 -v864 -v574 -v477 -v310 v102 v66 v866 -v810 -v575 -v479 v440 -v359 -v262 -v185 v101 -v73 -v26 v867 -v814 -v576 -v482 -v357 -v311 -v190 -v107 v67 -v30 -v697 -v583 v481 -v446 v399 -v315 -v265 -v216 -v189 v143 -v106 -v68 -v701 -v577 v486 -v444 -v358 -v266 v142 -v108 -v69 -v31 -v2 -v578 v485 v398 -v362 -v192 -v166 v144 -v112 -v1 -v660 -v579 -v483 -v445 -v193 v147 -v111 v7 -v659 -v594 -v558 -v484 -v449 -v404 v196 -v165 v146 -v109 v6 -v661 -v598 -v557 -v402 v194 v151 -v110 v8 -v662 -v559 -v332 v195 -v171 v150 v12 v663 -v562 -v403 -v169 v148 v11 v668 v561 -v407 -v335 v149 v9 v664 v563 -v336 -v170 v10 v739 v421 v81 -v855 v743 -v854 -v786 -v500 v425 -v302 v87 -v790 -v423 v862 -v506 -v349 v308 v865 v869 -v835 v792 -v436 -v355 -v313 v90 -v76 v868 -v839 v793 -v77 -v809 -v586 -v509 v442 -v360 -v316 -v261 -v212 -v72 -v28 -v813 -v587 -v480 -v314 -v184 v103 -v32 -v696 -v582 v494 v447 -v394 -v363 -v267 -v215 -v186 v104 -v70 -v700 v490 -v361 -v191 v105 -v580 v489 v450 v400 v188 -v161 -v116 -v34 v448 v197 v145 -v35 -v3 -v593 -v542 v405 -v270 -v167 v159 v4 -v597 v155 v5 -v671 v408 -v331 -v172 v154 -v16 -v672 -v560 v406 v667 -v571 -v466 -v337 -v173 v567 -v470 -v174 v781 v741 -v496 v422 v83 v745 v426 v787 -v502 v88 v856 v791 -v301 v857 v795 -v747 -v507 -v303 v91 -v75 v858 v794 -v748 -v348 v309 v89 -v74 -v22 v873 -v834 -v761 -v585 -v510 -v350 v305 -v257 -v21 -v838 -v765 -v584 -v508 -v435 -v356 -v317 -v811 v491 -v437 v352 -v263 -v211 -v29 -v815 v493 v443 -v364 -v33 -v698 v439 -v268 -v217 -v119 -v71 -v37 -v702 v451 -v393 -v187 -v120 -v36 -v817 -v581 -v538 v487 -v395 -v271 v205 v156 -v115 -v818 v401 -v269 v201 -v160 v158 -v704 -v670 -v595 -v541 v488 v397 -v327 -v220 v200 -v162 -v113 -v19 -v705 -v669 -v599 v409 -v168 -v20 -v722 -v568 -v333 -v164 v152 -v15 v726 -v570 -v175 v665 -v601 -v465 -v338 v153 v131 -v13 -v602 v566 -v469 v742 v434 -v79 v780 v746 -v495 v430 v84 v782 -v750 -v497 v429 v80 v783 -v749 -v503 v92 v876 v799 -v499 v877 -v805 -v511 -v304 v872 -v836 -v804 -v760 -v325 -v207 -v840 -v764 -v692 v492 -v351 -v321 -v256 -v23 -v884 v870 -v812 -v691 v372 -v320 -v258 -v213 -v118 -v24 -v888 -v816 -v438 v368 -v264 -v117 -v25 -v842 -v820 -v699 -v459 v367 -v260 -v218 v202 -v41 -v843 -v819 -v703 v589 -v455 -v272 v204 v157 -v707 v588 v537 -v454 -v221 -v18 -v706 -v396 -v219 -v17 -v596 -v543 -v417 v198 -v114 -v600 -v569 v413 -v326 -v163 -v721 v604 v412 -v328 -v199 -v183 -v127 v725 -v603 -v334 -v179 v666 -v546 -v467 -v330 -v178 v130 -v14 -v564 -v471 -v339 v903 v433 -v78 v875 v802 -v754 v427 -v100 v874 -v830 v803 -v498 -v96 -v829 v798 -v519 v428 -v322 -v95 -v515 -v324 -v837 v796 -v762 -v514 v369 -v841 -v806 v766 v371 -v206 -v883 v871 -v845 -v807 -v456 -v318 -v291 -v208 -v44 -v887 -v844 -v808 -v693 -v458 -v259 -v214 v203 -v45 -v824 v768 -v694 -v533 -v383 v365 -v319 -v280 -v210 -v40 v769 -v695 -v276 -v222 -v711 -v619 v539 -v452 -v414 v366 -v275 -v38 -v623 v590 -v416 v591 v544 -v453 -v180 v592 -v461 -v182 -v723 v608 v547 -v460 v410 -v126 v727 v545 -v329 -v468 v411 -v347 -v176 v132 -v565 v472 -v343 v801 v431 -v97 v800 -v99 -v753 v654 -v516 -v756 -v518 -v323 -v755 -v751 v521 -v93 -v831 -v525 v370 -v832 v797 -v763 -v512 -v287 -v249 -v94 -v43 v833 v767 -v457 -v42 -v885 v849 -v827 v771 -v513 -v379 -v290 -v277 v889 -v828 v770 -v279 -v209 -v823 -v714 -v382 -v230 -v715 -v532 -v415 -v226 -v891 -v821 -v710 v641 -v618 -v534 -v273 -v225 -v39 -v892 -v717 v645 -v622 v540 -v181 -v716 -v708 -v679 -v611 v536 -v274 -v122 v55 v683 -v612 v548 -v724 -v607 -v344 -v128 v728 -v462 -v346 v729 -v605 v463 -v240 -v177 v133 v730 v464 -v342 v904 v432 -v98 -v517 v653 -v752 v520 v245 -v879 -v757 -v524 -v878 -v852 -v826 v758 v286 v248 -v853 -v825 v759 -v278 v886 -v848 v775 -v713 -v378 -v292 -v227 v890 -v712 -v229 v894 -v846 -v384 -v893 -v822 v640 -v620 -v610 v295 -v223 v51 v644 -v624 -v609 v535 -v709 -v678 v556 -v387 -v224 v54 -v718 v682 -v552 -v345 -v121 -v719 -v626 -v551 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/55 28243
Raw data (stat): 28243 (runsolver) R 28242 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481281060 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.95 0.90 2/55 28243
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 5549 0 0 0 984 13 0 0 25 0 1 0 481281060 29401088 5371 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7178 5371 603 41 0 7137 0
vsize: 28712
[startup+20.0018 s]
Raw data (loadavg): 0.89 0.96 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 5692 0 0 0 1982 15 0 0 25 0 1 0 481281060 29982720 5514 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7320 5514 603 41 0 7279 0
vsize: 29280
[startup+30.0024 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 5823 0 0 0 2982 16 0 0 25 0 1 0 481281060 30523392 5645 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7452 5645 603 41 0 7411 0
vsize: 29808
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6006 0 0 0 3981 17 0 0 25 0 1 0 481281060 31285248 5828 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7638 5828 603 41 0 7597 0
vsize: 30552
[startup+50.0026 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6220 0 0 0 4980 18 0 0 25 0 1 0 481281060 32096256 6042 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7836 6042 603 41 0 7795 0
vsize: 31344
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6395 0 0 0 5979 19 0 0 25 0 1 0 481281060 32903168 6217 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8033 6217 603 41 0 7992 0
vsize: 32132
[startup+70.0033 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6580 0 0 0 6977 21 0 0 25 0 1 0 481281060 33705984 6402 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8229 6402 603 41 0 8188 0
vsize: 32916
[startup+80.0034 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6721 0 0 0 7977 21 0 0 25 0 1 0 481281060 34217984 6543 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8354 6543 603 41 0 8313 0
vsize: 33416
[startup+90.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 6897 0 0 0 8976 22 0 0 25 0 1 0 481281060 34889728 6719 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8518 6719 603 41 0 8477 0
vsize: 34072
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7021 0 0 0 9976 23 0 0 25 0 1 0 481281060 35409920 6843 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 6843 603 41 0 8604 0
vsize: 34580
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7184 0 0 0 10975 24 0 0 25 0 1 0 481281060 36085760 7006 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8810 7006 603 41 0 8769 0
vsize: 35240
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7350 0 0 0 11973 25 0 0 25 0 1 0 481281060 36761600 7172 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8975 7172 603 41 0 8934 0
vsize: 35900
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7467 0 0 0 12972 26 0 0 25 0 1 0 481281060 37163008 7289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9073 7289 603 41 0 9032 0
vsize: 36292
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7599 0 0 0 13972 26 0 0 25 0 1 0 481281060 37699584 7421 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9204 7421 603 41 0 9163 0
vsize: 36816
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 7826 0 0 0 14971 27 0 0 25 0 1 0 481281060 38907904 7648 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9499 7648 603 41 0 9458 0
vsize: 37996
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8081 0 0 0 15970 28 0 0 25 0 1 0 481281060 39976960 7903 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9760 7903 603 41 0 9719 0
vsize: 39040
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8232 0 0 0 16970 29 0 0 25 0 1 0 481281060 40513536 8054 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 8054 603 41 0 9850 0
vsize: 39564
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8371 0 0 0 17970 29 0 0 25 0 1 0 481281060 41046016 8193 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10021 8193 603 41 0 9980 0
vsize: 40084
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8537 0 0 0 18970 29 0 0 25 0 1 0 481281060 41840640 8359 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10215 8359 603 41 0 10174 0
vsize: 40860
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8674 0 0 0 19969 30 0 0 25 0 1 0 481281060 42377216 8496 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10346 8496 603 41 0 10305 0
vsize: 41384
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 20969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8633 603 41 0 10430 0
vsize: 41884
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 21969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8633 603 41 0 10430 0
vsize: 41884
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 22969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8633 603 41 0 10430 0
vsize: 41884
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 23969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8633 603 41 0 10430 0
vsize: 41884
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 24969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8633 603 41 0 10430 0
vsize: 41884
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 25969 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8633 603 41 0 10430 0
vsize: 41884
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 26970 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8633 603 41 0 10430 0
vsize: 41884
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 27970 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8633 603 41 0 10430 0
vsize: 41884
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 28970 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8633 603 41 0 10430 0
vsize: 41884
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8811 0 0 0 29970 31 0 0 25 0 1 0 481281060 42889216 8633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8633 603 41 0 10430 0
vsize: 41884
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28245
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 8816 0 0 0 30970 31 0 0 25 0 1 0 481281060 42889216 8638 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10471 8638 603 41 0 10430 0
vsize: 41884
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 9108 0 0 0 31969 32 0 0 25 0 1 0 481281060 44101632 8930 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10767 8930 603 41 0 10726 0
vsize: 43068
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 9486 0 0 0 32968 33 0 0 25 0 1 0 481281060 45584384 9308 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11129 9308 603 41 0 11088 0
vsize: 44516
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 9907 0 0 0 33968 34 0 0 25 0 1 0 481281060 47321088 9729 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11553 9729 603 41 0 11512 0
vsize: 46212
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10333 0 0 0 34967 35 0 0 25 0 1 0 481281060 49065984 10155 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11979 10155 603 41 0 11938 0
vsize: 47916
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10510 0 0 0 35966 36 0 0 25 0 1 0 481281060 49852416 10332 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12171 10332 603 41 0 12130 0
vsize: 48684
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10510 0 0 0 36966 36 0 0 25 0 1 0 481281060 49852416 10332 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12171 10332 603 41 0 12130 0
vsize: 48684
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10512 0 0 0 37966 36 0 0 25 0 1 0 481281060 49852416 10334 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12171 10334 603 41 0 12130 0
vsize: 48684
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10512 0 0 0 38966 36 0 0 25 0 1 0 481281060 49852416 10334 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12171 10334 603 41 0 12130 0
vsize: 48684
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10512 0 0 0 39967 36 0 0 25 0 1 0 481281060 49852416 10334 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12171 10334 603 41 0 12130 0
vsize: 48684
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10512 0 0 0 40967 36 0 0 25 0 1 0 481281060 49852416 10334 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12171 10334 603 41 0 12130 0
vsize: 48684
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10512 0 0 0 41967 36 0 0 25 0 1 0 481281060 49852416 10334 4294967295 134512640 134672761 3221224544 3221223648 134560332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12171 10334 603 41 0 12130 0
vsize: 48684
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10829 0 0 0 42966 37 0 0 25 0 1 0 481281060 51191808 10651 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12498 10651 603 41 0 12457 0
vsize: 49992
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10831 0 0 0 43966 38 0 0 25 0 1 0 481281060 51191808 10653 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12498 10653 603 41 0 12457 0
vsize: 49992
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10832 0 0 0 44966 38 0 0 25 0 1 0 481281060 51191808 10654 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12498 10654 603 41 0 12457 0
vsize: 49992
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 10949 0 0 0 45966 38 0 0 25 0 1 0 481281060 51589120 10771 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12595 10771 603 41 0 12554 0
vsize: 50380
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 11089 0 0 0 46965 39 0 0 25 0 1 0 481281060 52252672 10911 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12757 10911 603 41 0 12716 0
vsize: 51028
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 11316 0 0 0 47965 40 0 0 25 0 1 0 481281060 53194752 11138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12987 11138 603 41 0 12946 0
vsize: 51948
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 11479 0 0 0 48964 40 0 0 25 0 1 0 481281060 53870592 11301 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13152 11301 603 41 0 13111 0
vsize: 52608
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 11676 0 0 0 49964 41 0 0 25 0 1 0 481281060 54669312 11498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13347 11498 603 41 0 13306 0
vsize: 53388
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 11848 0 0 0 50963 41 0 0 25 0 1 0 481281060 55341056 11670 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13511 11670 603 41 0 13470 0
vsize: 54044
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 12052 0 0 0 51963 42 0 0 25 0 1 0 481281060 56143872 11874 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 11874 603 41 0 13666 0
vsize: 54828
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 12374 0 0 0 52963 42 0 0 25 0 1 0 481281060 57495552 12196 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14037 12196 603 41 0 13996 0
vsize: 56148
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 12871 0 0 0 53962 43 0 0 25 0 1 0 481281060 59510784 12693 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14529 12693 603 41 0 14488 0
vsize: 58116
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 13322 0 0 0 54962 44 0 0 25 0 1 0 481281060 61386752 13144 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14987 13144 603 41 0 14946 0
vsize: 59948
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 13984 0 0 0 55961 45 0 0 25 0 1 0 481281060 64049152 13806 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15637 13806 603 41 0 15596 0
vsize: 62548
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 14183 0 0 0 56961 45 0 0 25 0 1 0 481281060 64856064 14005 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15834 14005 603 41 0 15793 0
vsize: 63336
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 14363 0 0 0 57960 46 0 0 25 0 1 0 481281060 65662976 14185 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16031 14185 603 41 0 15990 0
vsize: 64124
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 14731 0 0 0 58960 47 0 0 25 0 1 0 481281060 67133440 14553 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16390 14553 603 41 0 16349 0
vsize: 65560
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15057 0 0 0 59959 47 0 0 25 0 1 0 481281060 68481024 14879 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16719 14879 603 41 0 16678 0
vsize: 66876
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28247
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 60958 48 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223844 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 61958 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 62959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 63959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 64959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 65959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 66959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 67959 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 68960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 69960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 70960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 71960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 72960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 73960 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 74961 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15452 0 0 0 75961 49 0 0 25 0 1 0 481281060 70070272 15274 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17107 15274 603 41 0 17066 0
vsize: 68428
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 76961 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223616 1074718162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 77961 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 78961 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 79962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 80962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 81962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 82962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 83962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+850.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 84962 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+860.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 85963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+870.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 86963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 87963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+890.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 88963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+900.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 89963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+910.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28249
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 90963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134561278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 91964 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 92964 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 93963 49 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 94963 50 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+960.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 95963 50 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+970.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 96963 50 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+980.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15453 0 0 0 97964 50 0 0 25 0 1 0 481281060 70062080 15275 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17105 15275 603 41 0 17064 0
vsize: 68420
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15626 0 0 0 98963 50 0 0 25 0 1 0 481281060 70733824 15448 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17269 15448 603 41 0 17228 0
vsize: 69076
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15806 0 0 0 99963 51 0 0 25 0 1 0 481281060 71544832 15628 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17467 15628 603 41 0 17426 0
vsize: 69868
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 15941 0 0 0 100962 51 0 0 25 0 1 0 481281060 72077312 15763 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17597 15763 603 41 0 17556 0
vsize: 70388
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16089 0 0 0 101962 52 0 0 25 0 1 0 481281060 72605696 15911 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17726 15911 603 41 0 17685 0
vsize: 70904
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16241 0 0 0 102962 52 0 0 25 0 1 0 481281060 73273344 16063 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17889 16063 603 41 0 17848 0
vsize: 71556
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16376 0 0 0 103962 52 0 0 25 0 1 0 481281060 73809920 16198 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18020 16198 603 41 0 17979 0
vsize: 72080
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16534 0 0 0 104962 53 0 0 25 0 1 0 481281060 74481664 16356 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18184 16356 603 41 0 18143 0
vsize: 72736
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16714 0 0 0 105961 53 0 0 25 0 1 0 481281060 75149312 16536 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18347 16536 603 41 0 18306 0
vsize: 73388
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 16975 0 0 0 106960 55 0 0 25 0 1 0 481281060 76214272 16797 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18607 16797 603 41 0 18566 0
vsize: 74428
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 17267 0 0 0 107960 55 0 0 25 0 1 0 481281060 77422592 17089 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18902 17089 603 41 0 18861 0
vsize: 75608
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 17664 0 0 0 108959 56 0 0 25 0 1 0 481281060 79040512 17486 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19297 17486 603 41 0 19256 0
vsize: 77188
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 17974 0 0 0 109958 57 0 0 25 0 1 0 481281060 80252928 17796 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19593 17796 603 41 0 19552 0
vsize: 78372
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 18323 0 0 0 110957 58 0 0 25 0 1 0 481281060 81711104 18145 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19949 18145 603 41 0 19908 0
vsize: 79796
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 18597 0 0 0 111957 59 0 0 25 0 1 0 481281060 82780160 18419 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20210 18419 603 41 0 20169 0
vsize: 80840
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 18910 0 0 0 112957 59 0 0 25 0 1 0 481281060 84119552 18732 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20537 18732 603 41 0 20496 0
vsize: 82148
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 19226 0 0 0 113956 60 0 0 25 0 1 0 481281060 85446656 19048 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20861 19048 603 41 0 20820 0
vsize: 83444
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 19576 0 0 0 114955 61 0 0 25 0 1 0 481281060 86777856 19398 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21186 19398 603 41 0 21145 0
vsize: 84744
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 19963 0 0 0 115955 62 0 0 25 0 1 0 481281060 88371200 19785 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21575 19785 603 41 0 21534 0
vsize: 86300
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 20359 0 0 0 116954 63 0 0 25 0 1 0 481281060 89968640 20181 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21965 20181 603 41 0 21924 0
vsize: 87860
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 20706 0 0 0 117953 64 0 0 25 0 1 0 481281060 91439104 20528 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22324 20528 603 41 0 22283 0
vsize: 89296
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 21081 0 0 0 118952 65 0 0 25 0 1 0 481281060 92909568 20903 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22683 20903 603 41 0 22642 0
vsize: 90732
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28251
Raw data (stat): 28243 (minisat+) R 28242 20838 20837 0 -1 0 21500 0 0 0 119951 66 0 0 25 0 1 0 481281060 94654464 21322 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 21322 603 41 0 23068 0
vsize: 92436
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 28251
Raw data (stat): 28243 (minisat+) Z 28242 20838 20837 0 -1 12 21503 0 0 0 119951 70 0 0 25 0 1 0 481281060 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.23
CPU user time (s): 1199.52
CPU system time (s): 0.707892
CPU usage (%): 100.014
Max. virtual memory (Kb): 92436
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####