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:100.opb
MD5SUM	f82b685b64af240616b701a750c82883
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10
Optimality of the best value was proved	NO
Number of terms in the objective function	934
Biggest coefficient in the objective function	546
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	2594
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	546
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	2594
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.03784
Number of variables	934
Total number of constraints	1996
Number of constraints which are clauses	879
Number of constraints which are cardinality constraints (but not clauses)	1117
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	20
Trace number 6464

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-14 05:06:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4879 boxname=wulflinc6 idbench=367 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f82b685b64af240616b701a750c82883  /oldhome/oroussel/tmp/wulflinc6/normalized-10:20:4.5:0.95:100.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc6/normalized-10:20:4.5:0.95:100.opb /oldhome/oroussel/tmp/wulflinc6/normalized-10:20:4.5:0.95:100.opb
IDLAUNCH: 4879
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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	: 2
cpu MHz		: 451.042
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:        873196 kB
Buffers:         36552 kB
Cached:         102856 kB
SwapCached:       2644 kB
Active:          54788 kB
Inactive:        90088 kB
HighTotal:      131008 kB
HighFree:        24332 kB
LowTotal:       903652 kB
LowFree:        848864 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11056 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:26:39 (client local time) WITH STATUS 10 IN 1200.41 SECONDS
stats: 4879 7 1200.41 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1062 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   20
c ---[ 186]---> BDD-cost:   20
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   23
c ---[ 183]---> BDD-cost:   26
c ---[ 182]---> BDD-cost:   23
c ---[ 181]---> BDD-cost:   17
c ---[ 180]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   17
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   17
c ---[ 176]---> BDD-cost:   17
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:    5
c ---[ 173]---> BDD-cost:   14
c ---[ 172]---> BDD-cost:   17
c ---[ 171]---> BDD-cost:   23
c ---[ 170]---> BDD-cost:   21
c ---[ 169]---> BDD-cost:   29
c ---[ 168]---> BDD-cost:   26
c ---[ 167]---> BDD-cost:   26
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   38
c ---[ 164]---> BDD-cost:   29
c ---[ 163]---> BDD-cost:   29
c ---[ 162]---> BDD-cost:   26
c ---[ 161]---> BDD-cost:   23
c ---[ 160]---> BDD-cost:   20
c ---[ 159]---> BDD-cost:   20
c ---[ 158]---> BDD-cost:   17
c ---[ 156]---> BDD-cost:   20
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:   26
c ---[ 153]---> BDD-cost:   32
c ---[ 152]---> BDD-cost:   35
c ---[ 151]---> BDD-cost:   29
c ---[ 150]---> BDD-cost:   41
c ---[ 149]---> BDD-cost:   38
c ---[ 148]---> BDD-cost:   36
c ---[ 147]---> BDD-cost:   32
c ---[ 146]---> BDD-cost:   32
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   29
c ---[ 143]---> BDD-cost:   26
c ---[ 142]---> BDD-cost:   26
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:   21
c ---[ 135]---> BDD-cost:   29
c ---[ 134]---> BDD-cost:   35
c ---[ 133]---> BDD-cost:   32
c ---[ 132]---> BDD-cost:   44
c ---[ 131]---> BDD-cost:   44
c ---[ 130]---> BDD-cost:   44
c ---[ 129]---> BDD-cost:   38
c ---[ 128]---> BDD-cost:   38
c ---[ 127]---> BDD-cost:   32
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   32
c ---[ 124]---> BDD-cost:   38
c ---[ 123]---> BDD-cost:   32
c ---[ 122]---> BDD-cost:   26
c ---[ 121]---> BDD-cost:   20
c ---[ 120]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:    7
c ---[ 117]---> BDD-cost:    5
c ---[ 116]---> BDD-cost:   29
c ---[ 115]---> BDD-cost:   32
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   44
c ---[ 112]---> BDD-cost:   50
c ---[ 111]---> BDD-cost:   41
c ---[ 110]---> BDD-cost:   42
c ---[ 109]---> BDD-cost:   38
c ---[ 108]---> BDD-cost:   41
c ---[ 107]---> BDD-cost:   35
c ---[ 106]---> BDD-cost:   38
c ---[ 105]---> BDD-cost:   38
c ---[ 104]---> BDD-cost:   35
c ---[ 103]---> BDD-cost:   32
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   23
c ---[ 100]---> BDD-cost:   26
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   17
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:   23
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   41
c ---[  93]---> BDD-cost:   41
c ---[  92]---> BDD-cost:   47
c ---[  91]---> BDD-cost:   50
c ---[  90]---> BDD-cost:   53
c ---[  89]---> BDD-cost:   47
c ---[  88]---> BDD-cost:   38
c ---[  87]---> BDD-cost:   38
c ---[  86]---> BDD-cost:   35
c ---[  85]---> BDD-cost:   32
c ---[  84]---> BDD-cost:   32
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   32
c ---[  81]---> BDD-cost:   32
c ---[  80]---> BDD-cost:   26
c ---[  79]---> BDD-cost:   20
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:   23
c ---[  75]---> BDD-cost:   29
c ---[  74]---> BDD-cost:   32
c ---[  73]---> BDD-cost:   41
c ---[  72]---> BDD-cost:   41
c ---[  71]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   44
c ---[  69]---> BDD-cost:   44
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   32
c ---[  66]---> BDD-cost:   32
c ---[  65]---> BDD-cost:   32
c ---[  64]---> BDD-cost:   33
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   29
c ---[  60]---> BDD-cost:   23
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:    5
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   29
c ---[  52]---> BDD-cost:   32
c ---[  51]---> BDD-cost:   38
c ---[  50]---> BDD-cost:   32
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   26
c ---[  45]---> BDD-cost:   29
c ---[  44]---> BDD-cost:   26
c ---[  43]---> BDD-cost:   29
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   18
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   20
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   26
c ---[  31]---> BDD-cost:   29
c ---[  30]---> BDD-cost:   23
c ---[  29]---> BDD-cost:   26
c ---[  28]---> BDD-cost:   20
c ---[  27]---> BDD-cost:   23
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   26
c ---[  24]---> BDD-cost:   14
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   23
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   20
c ---[   8]---> BDD-cost:   11
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   14
c ---[   3]---> BDD-cost:    7
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23220    65176 |    7740       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 877[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2085   maxlim: 625   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   37742   116996 |   12580       0        0     nan |  0.000 % |
c |       100 |   37742   116996 |   13838     100      328     3.3 |  2.441 % |
c |       250 |   37742   116996 |   15221     250     1089     4.4 |  2.441 % |
c |       475 |   37742   116996 |   16743     475     2257     4.8 |  2.441 % |
c |       812 |   37742   116996 |   18418     812     5357     6.6 |  2.441 % |
c |      1319 |   37742   116996 |   20260    1319     8395     6.4 |  2.441 % |
c ==============================================================================
c [1mFound solution: 177[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1325   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1374 |   37755   117064 |   12585    1374     8862     6.4 |  2.441 % |
c |      1474 |   37755   117064 |   13843    1474     9399     6.4 |  2.516 % |
c ==============================================================================
c [1mFound solution: 160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1342   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1500 |   37767   117137 |   12589    1500     9625     6.4 |  2.516 % |
c |      1601 |   37767   117137 |   13847    1601    14331     9.0 |  2.578 % |
c |      1751 |   37767   117137 |   15232    1751    14973     8.6 |  2.578 % |
c |      1976 |   37767   117137 |   16755    1976    16917     8.6 |  2.578 % |
c |      2314 |   37767   117137 |   18431    2314    19547     8.4 |  2.578 % |
c |      2820 |   37767   117137 |   20274    2820    22668     8.0 |  2.578 % |
c ==============================================================================
c [1mFound solution: 158[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1344   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3278 |   37769   117157 |   12589    3278    28350     8.6 |  2.578 % |
c |      3378 |   37769   117157 |   13847    3378    28867     8.5 |  2.603 % |
c |      3528 |   37769   117157 |   15232    3528    30141     8.5 |  2.603 % |
c ==============================================================================
c [1mFound solution: 138[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1364   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3574 |   37772   117190 |   12590    3574    30491     8.5 |  2.603 % |
c |      3675 |   37772   117190 |   13849    3675    33039     9.0 |  2.641 % |
c |      3825 |   37772   117190 |   15233    3825    34133     8.9 |  2.641 % |
c |      4050 |   37772   117190 |   16757    4050    37058     9.2 |  2.641 % |
c |      4387 |   37772   117190 |   18433    4387    40749     9.3 |  2.641 % |
c ==============================================================================
c [1mFound solution: 137[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1365   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4745 |   37773   117202 |   12591    4745    51602    10.9 |  2.641 % |
c |      4846 |   37773   117202 |   13850    4846    52546    10.8 |  2.654 % |
c |      4997 |   37773   117202 |   15235    4997    53938    10.8 |  2.654 % |
c |      5222 |   37773   117202 |   16758    5222    57264    11.0 |  2.654 % |
c |      5559 |   37773   117202 |   18434    5559    63471    11.4 |  2.654 % |
c |      6065 |   37773   117202 |   20277    6065    78081    12.9 |  2.654 % |
c |      6826 |   37773   117202 |   22305    6826   106618    15.6 |  2.654 % |
c |      7965 |   37773   117202 |   24536    7965   167831    21.1 |  2.654 % |
c |      9674 |   37773   117202 |   26989    9674   241551    25.0 |  2.654 % |
c ==============================================================================
c [1mFound solution: 135[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1367   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10546 |   37774   117212 |   12591   10546   265811    25.2 |  2.654 % |
c |     10646 |   37774   117212 |   13850   10646   268558    25.2 |  2.666 % |
c ==============================================================================
c [1mFound solution: 103[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1399   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10763 |   37787   117259 |   12595   10763   269732    25.1 |  2.666 % |
c |     10863 |   37787   117259 |   13854   10863   270919    24.9 |  2.703 % |
c |     11013 |   37787   117259 |   15239   11013   273865    24.9 |  2.703 % |
c |     11241 |   37787   117259 |   16763   11241   280486    25.0 |  2.703 % |
c |     11579 |   37787   117259 |   18440   11579   288400    24.9 |  2.703 % |
c |     12085 |   37787   117259 |   20284   12085   299232    24.8 |  2.703 % |
c |     12844 |   37787   117259 |   22312   12844   330845    25.8 |  2.703 % |
c |     13983 |   37787   117259 |   24544   13983   419469    30.0 |  2.703 % |
c ==============================================================================
c [1mFound solution: 98[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1404   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14291 |   37796   117297 |   12598   14291   426096    29.8 |  2.703 % |
c |     14391 |   37796   117297 |   13857    7246   191134    26.4 |  2.727 % |
c |     14541 |   37796   117297 |   15243    7396   197969    26.8 |  2.727 % |
c |     14766 |   37796   117297 |   16767    7621   200328    26.3 |  2.727 % |
c |     15103 |   37796   117297 |   18444    7958   209450    26.3 |  2.727 % |
c |     15609 |   37796   117297 |   20289    8464   218394    25.8 |  2.727 % |
c |     16368 |   37796   117297 |   22318    9223   262839    28.5 |  2.727 % |
c |     17508 |   37796   117297 |   24549   10363   324485    31.3 |  2.727 % |
c |     19218 |   37796   117297 |   27004   12073   398031    33.0 |  2.727 % |
c |     21781 |   37796   117297 |   29705   14636   576604    39.4 |  2.727 % |
c |     25625 |   37796   117297 |   32675   18480   781021    42.3 |  2.727 % |
c |     31391 |   37796   117297 |   35943   24246  1342700    55.4 |  2.727 % |
c |     40040 |   37796   117297 |   39537   32895  1976749    60.1 |  2.727 % |
c ==============================================================================
c [1mFound solution: 91[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1411   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42012 |   37798   117314 |   12599   34867  2094477    60.1 |  2.727 % |
c |     42112 |   37798   117314 |   13858    7932   429077    54.1 |  2.752 % |
c |     42263 |   37798   117314 |   15244    8083   433296    53.6 |  2.752 % |
c |     42488 |   37798   117314 |   16769    8308   434786    52.3 |  2.752 % |
c |     42826 |   37798   117314 |   18446    8646   442295    51.2 |  2.752 % |
c |     43332 |   37798   117314 |   20290    9152   453523    49.6 |  2.752 % |
c |     44091 |   37798   117314 |   22319    9911   467222    47.1 |  2.752 % |
c |     45230 |   37798   117314 |   24551   11050   506895    45.9 |  2.752 % |
c |     46938 |   37798   117314 |   27007   12758   631437    49.5 |  2.752 % |
c |     49502 |   37798   117314 |   29707   15322   773082    50.5 |  2.752 % |
c |     53346 |   37798   117314 |   32678   19166  1018716    53.2 |  2.752 % |
c |     59112 |   37798   117314 |   35946   24932  1309520    52.5 |  2.752 % |
c |     67765 |   37798   117314 |   39541   33585  2063828    61.5 |  2.752 % |
c |     80740 |   37798   117314 |   43495   15547  1591254   102.4 |  2.752 % |
c |    100205 |   37798   117314 |   47844   35012  3953252   112.9 |  2.752 % |
c |    129400 |   37798   117314 |   52629   24860  4511737   181.5 |  2.752 % |
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1412   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    154128 |   37788   117296 |   12596   49587  6669324   134.5 |  2.752 % |
c |    154228 |   37788   117296 |   13855    7319   699796    95.6 |  2.803 % |
c |    154378 |   37788   117296 |   15241    7469   700535    93.8 |  2.803 % |
c |    154603 |   37788   117296 |   16765    7694   701679    91.2 |  2.803 % |
c |    154942 |   37788   117296 |   18441    8033   703678    87.6 |  2.803 % |
c |    155448 |   37788   117296 |   20285    8539   722808    84.6 |  2.803 % |
c |    156207 |   37788   117296 |   22314    9298   729100    78.4 |  2.803 % |
c |    157348 |   37788   117296 |   24546   10439   764297    73.2 |  2.803 % |
c |    159056 |   37788   117296 |   27000   12147   807201    66.5 |  2.803 % |
c |    161618 |   37788   117296 |   29700   14709   957032    65.1 |  2.803 % |
c |    165462 |   37788   117296 |   32670   18553  1155851    62.3 |  2.803 % |
c |    171228 |   37788   117296 |   35937   24319  1508278    62.0 |  2.803 % |
c |    179877 |   37788   117296 |   39531   32968  2461632    74.7 |  2.803 % |
c |    192851 |   37788   117296 |   43484   19349  1759996    91.0 |  2.803 % |
c |    212312 |   37788   117296 |   47833   38810  4567330   117.7 |  2.803 % |
c |    241504 |   37788   117296 |   52616   30757  3602894   117.1 |  2.803 % |
c |    285296 |   37788   117296 |   57878   33598  4568122   136.0 |  2.803 % |
c |    350982 |   37774   117237 |   63666   51254  6103759   119.1 |  2.828 % |
c |    449513 |   37774   117237 |   70032   47474  6331431   133.4 |  2.828 % |
c |    597302 |   37774   117237 |   77035   17842  2215070   124.1 |  2.828 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v853 v782 -v197 -v102 v21 -v2 v855 -v103 -v1 -v785 -v384 v272 -v196 v20 -v3 v856 -v786 -v76 v55 -v23 v4 -v383 -v275 -v202 -v75 v54 v11 v763 -v387 -v276 -v200 v56 -v24 v5 v762 -v247 -v150 -v77 v57 v26 -v6 v764 v613 -v388 -v201 -v79 v58 -v39 v27 -v7 v765 v612 -v513 -v250 -v205 -v149 -v65 v38 v766 -v618 -v251 -v80 v59 v40 v773 -v617 -v512 -v326 -v155 -v125 -v82 v60 v41 v767 v619 -v153 -v83 v61 v42 v768 v623 -v593 -v573 -v518 -v128 v49 v769 v622 -v577 -v516 -v154 -v129 v43 v729 v620 v596 v576 -v158 v44 -v621 v597 -v517 v45 -v881 v728 -v521 v852 v781 -v192 -v104 -v17 v857 -v787 -v537 -v468 v271 -v198 v22 -v14 -v541 -v71 -v25 -v15 -v859 -v385 -v277 -v203 -v108 -v70 v29 v10 -v860 -v389 v28 -v790 -v246 v206 -v145 -v78 -v68 -v8 -v204 -v81 -v69 -v811 -v776 -v638 v508 -v391 -v322 -v280 -v252 -v151 -v85 -v64 -v777 v642 v614 -v392 -v84 v772 v615 -v514 -v325 -v156 -v124 -v62 -v52 v616 -v53 v770 v627 -v592 -v519 -v255 -v159 -v130 v48 -v572 -v157 -v877 v598 -v574 -v522 -v46 v578 -v520 -v880 v730 -v133 v601 v854 v783 -v464 v267 -v105 -v13 v858 -v379 -v191 -v16 -v12 v862 -v788 -v536 -v488 -v467 -v378 v273 -v193 v109 -v18 v861 -v540 v492 -v199 -v107 v19 -v791 -v386 -v278 -v242 v195 -v67 v33 -v789 -v390 v207 -v72 -v66 -v807 -v775 -v394 -v301 v281 -v248 -v73 -v9 -v774 -v393 v279 -v144 -v74 -v810 -v637 v321 -v253 -v146 -v120 -v89 -v51 v641 v507 -v152 -v50 -v630 -v588 v509 -v327 -v256 -v148 -v126 -v63 v631 -v515 -v254 -v160 v771 v626 -v594 v511 -v131 v725 -v523 -v876 v724 -v709 v624 v599 -v330 -v134 -v47 -v575 -v132 -v882 v731 v602 -v586 v600 -v582 -v900 v732 -v581 -v904 v733 -v851 v779 -v463 -v422 v106 v850 v784 -v426 v266 v110 -v866 v780 -v662 -v538 -v487 -v469 v268 -v177 -v36 -v792 -v666 -v542 v491 -v380 v274 -v194 -v37 -v381 -v297 v270 -v222 -v215 v32 -v382 v282 -v241 -v226 -v211 -v806 -v544 -v472 -v398 -v317 -v300 -v243 -v210 -v92 v30 -v545 -v249 -v93 -v812 -v639 -v629 v323 v245 -v88 v643 -v628 v257 -v147 -v119 v913 -v836 v328 -v168 -v121 -v86 -v917 v587 v510 -v164 -v127 -v872 -v815 -v705 v645 v589 v531 -v347 -v331 -v163 -v123 -v646 -v595 v527 -v351 -v329 -v135 -v878 -v708 -v625 v591 -v583 v526 v726 v603 -v585 v95 -v883 v727 v94 -v899 -v884 v737 -v579 v903 -v885 -v869 -v533 -v465 -v421 -v173 v118 -v35 -v870 v778 v425 -v114 -v34 -v865 v800 v661 -v539 -v489 -v470 -v212 -v176 -v113 v796 -v665 -v543 v493 v269 -v214 -v863 v802 v795 -v547 -v473 -v450 -v401 -v296 -v290 -v221 -v91 -v633 -v546 -v471 -v402 v286 -v225 -v90 -v808 -v632 v495 -v397 -v302 v285 -v208 v31 v496 -v316 -v244 -v832 -v813 v752 -v640 -v395 -v318 -v265 -v209 -v165 v644 v324 -v261 -v167 v912 -v835 -v816 v648 v528 v320 -v305 -v260 -v87 -v916 -v814 v647 v530 -v332 -v122 -v704 -v346 -v161 -v143 -v871 v590 -v584 -v350 -v139 -v873 -v710 v611 v524 -v162 -v138 -v879 -v607 v875 -v740 -v606 -v561 v525 -v886 -v741 v565 v96 -v901 v736 v713 -v580 v97 v905 -v867 v797 v484 -v461 -v423 -v172 -v117 v799 -v532 -v466 v427 -v213 v663 -v534 -v490 v462 -v446 -v400 -v292 -v287 -v178 -v111 -v667 -v535 v494 -v474 -v399 -v289 -v864 v793 -v551 v498 -v449 -v429 -v298 v223 -v112 v801 v497 -v430 -v227 v803 v794 -v748 -v687 -v669 -v303 v283 -v262 -v181 -v809 -v691 -v670 -v634 -v264 -v166 -v831 v805 v751 -v635 -v396 -v306 -v284 v229 -v817 v636 -v529 -v319 -v304 v230 v914 -v837 -v700 -v652 v340 -v258 -v140 v918 -v336 -v142 -v706 -v608 -v348 -v335 -v259 v610 -v352 v920 -v840 -v739 -v711 -v412 -v371 -v136 -v921 -v896 -v874 -v738 v375 -v895 v894 v714 -v604 -v560 -v354 -v137 -v890 v712 v564 -v355 -v902 -v889 v734 -v605 -v100 v906 -v101 -v868 v798 -v658 v424 -v174 -v115 v483 -v460 v428 -v288 -v217 v664 -v554 v485 v482 -v445 -v432 -v216 -v179 -v668 -v555 v486 -v478 -v431 -v291 -v672 -v550 v502 -v477 -v451 -v293 v224 -v182 -v671 -v299 -v263 -v228 -v180 v827 -v747 -v686 -v548 v295 v232 -v908 v804 -v690 -v307 v231 -v907 -v833 v825 v753 -v655 -v454 v337 -v821 -v656 -v342 v339 -v141 v915 -v838 -v820 -v651 -v341 v919 v699 -v609 v923 -v841 v756 v701 -v649 v408 -v349 -v333 v922 -v839 -v707 -v353 v891 v703 v411 -v370 -v357 -v334 v893 v715 v374 -v356 -v562 -v99 -v897 v566 -v98 -v898 -v88#### 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.92 0.98 0.91 2/54 3357
Raw data (stat): 3357 (runsolver) R 3356 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423719742 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 2328 0 0 0 992 6 0 0 25 0 1 0 423719742 11190272 2180 4294967295 134512640 134672761 3221224544 3221223796 134562232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2732 2180 603 41 0 2691 0
vsize: 10928
[startup+20.0021 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 2784 0 0 0 1991 8 0 0 25 0 1 0 423719742 13180928 2636 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3218 2636 603 41 0 3177 0
vsize: 12872
[startup+30.0032 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 3743 0 0 0 2989 10 0 0 25 0 1 0 423719742 17092608 3595 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4173 3595 603 41 0 4132 0
vsize: 16692
[startup+40.0039 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 4395 0 0 0 3987 12 0 0 25 0 1 0 423719742 19763200 4247 4294967295 134512640 134672761 3221224544 3221223688 1074754673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4247 603 41 0 4784 0
vsize: 19300
[startup+50.0046 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 4395 0 0 0 4987 12 0 0 25 0 1 0 423719742 19763200 4247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4247 603 41 0 4784 0
vsize: 19300
[startup+60.0047 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 4395 0 0 0 5987 13 0 0 25 0 1 0 423719742 19763200 4247 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4247 603 41 0 4784 0
vsize: 19300
[startup+70.0064 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 5125 0 0 0 6986 15 0 0 25 0 1 0 423719742 22716416 4977 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5546 4977 603 41 0 5505 0
vsize: 22184
[startup+80.0068 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 5862 0 0 0 7983 17 0 0 25 0 1 0 423719742 25817088 5714 4294967295 134512640 134672761 3221224544 3221223728 134559660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6303 5714 603 41 0 6262 0
vsize: 25212
[startup+90.007 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 5862 0 0 0 8984 17 0 0 25 0 1 0 423719742 25817088 5714 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6303 5714 603 41 0 6262 0
vsize: 25212
[startup+100.008 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 5862 0 0 0 9984 17 0 0 25 0 1 0 423719742 25817088 5714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6303 5714 603 41 0 6262 0
vsize: 25212
[startup+110.008 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 6486 0 0 0 10982 20 0 0 25 0 1 0 423719742 28377088 6338 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6928 6338 603 41 0 6887 0
vsize: 27712
[startup+120.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 7201 0 0 0 11980 22 0 0 25 0 1 0 423719742 31199232 7053 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7617 7053 603 41 0 7576 0
vsize: 30468
[startup+130.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 8075 0 0 0 12978 24 0 0 25 0 1 0 423719742 34844672 7927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8507 7927 603 41 0 8466 0
vsize: 34028
[startup+140.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 8998 0 0 0 13977 26 0 0 25 0 1 0 423719742 38580224 8850 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9419 8850 603 41 0 9378 0
vsize: 37676
[startup+150.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 9889 0 0 0 14974 30 0 0 25 0 1 0 423719742 42205184 9741 4294967295 134512640 134672761 3221224544 3221223712 134559063 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10304 9742 603 41 0 10263 0
vsize: 41216
[startup+160.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 15974 30 0 0 25 0 1 0 423719742 42741760 9852 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10435 9852 603 41 0 10394 0
vsize: 41740
[startup+170.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 16974 30 0 0 25 0 1 0 423719742 42741760 9852 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10435 9852 603 41 0 10394 0
vsize: 41740
[startup+180.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 17974 30 0 0 25 0 1 0 423719742 42741760 9852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10435 9852 603 41 0 10394 0
vsize: 41740
[startup+190.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 18975 30 0 0 25 0 1 0 423719742 42741760 9852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10435 9852 603 41 0 10394 0
vsize: 41740
[startup+200.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 19975 30 0 0 25 0 1 0 423719742 42741760 9852 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10435 9852 603 41 0 10394 0
vsize: 41740
[startup+210.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 20976 30 0 0 25 0 1 0 423719742 42729472 9852 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10432 9852 603 41 0 10391 0
vsize: 41728
[startup+220.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 21976 30 0 0 25 0 1 0 423719742 42700800 9852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10425 9852 603 41 0 10384 0
vsize: 41700
[startup+230.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 22976 30 0 0 25 0 1 0 423719742 42700800 9852 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10425 9852 603 41 0 10384 0
vsize: 41700
[startup+240.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 23977 30 0 0 25 0 1 0 423719742 42700800 9852 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10425 9852 603 41 0 10384 0
vsize: 41700
[startup+250.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 24977 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+260.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 25977 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+270.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 26977 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+280.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 27978 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+290.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 28978 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+300.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 29979 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+310.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 30979 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223728 134559609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+320.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 31979 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+330.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 32980 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+340.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 33980 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+350.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 34980 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+360.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 35981 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+370.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10000 0 0 0 36981 30 0 0 25 0 1 0 423719742 42549248 9830 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9830 603 41 0 10347 0
vsize: 41552
[startup+380.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10002 0 0 0 37981 30 0 0 25 0 1 0 423719742 42549248 9832 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9832 603 41 0 10347 0
vsize: 41552
[startup+390.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10002 0 0 0 38982 30 0 0 25 0 1 0 423719742 42549248 9832 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9832 603 41 0 10347 0
vsize: 41552
[startup+400.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10002 0 0 0 39982 30 0 0 25 0 1 0 423719742 42549248 9832 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9832 603 41 0 10347 0
vsize: 41552
[startup+410.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10002 0 0 0 40983 30 0 0 25 0 1 0 423719742 42549248 9832 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9832 603 41 0 10347 0
vsize: 41552
[startup+420.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10002 0 0 0 41983 30 0 0 25 0 1 0 423719742 42549248 9832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9832 603 41 0 10347 0
vsize: 41552
[startup+430.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10002 0 0 0 42983 30 0 0 25 0 1 0 423719742 42549248 9832 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9832 603 41 0 10347 0
vsize: 41552
[startup+440.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10002 0 0 0 43984 30 0 0 25 0 1 0 423719742 42549248 9832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9832 603 41 0 10347 0
vsize: 41552
[startup+450.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10002 0 0 0 44984 30 0 0 25 0 1 0 423719742 42549248 9832 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10388 9832 603 41 0 10347 0
vsize: 41552
[startup+460.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10059 0 0 0 45985 30 0 0 25 0 1 0 423719742 42815488 9889 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10453 9889 603 41 0 10412 0
vsize: 41812
[startup+470.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 10844 0 0 0 46983 32 0 0 25 0 1 0 423719742 46026752 10674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11237 10674 603 41 0 11196 0
vsize: 44948
[startup+480.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11197 0 0 0 47983 33 0 0 25 0 1 0 423719742 47489024 11027 4294967295 134512640 134672761 3221224544 3221223648 134560070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11594 11027 603 41 0 11553 0
vsize: 46376
[startup+490.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11197 0 0 0 48983 33 0 0 25 0 1 0 423719742 47489024 11027 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11594 11027 603 41 0 11553 0
vsize: 46376
[startup+500.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11197 0 0 0 49983 33 0 0 25 0 1 0 423719742 47489024 11027 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11594 11027 603 41 0 11553 0
vsize: 46376
[startup+510.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11197 0 0 0 50984 33 0 0 25 0 1 0 423719742 47489024 11027 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11594 11027 603 41 0 11553 0
vsize: 46376
[startup+520.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11197 0 0 0 51984 33 0 0 25 0 1 0 423719742 47489024 11027 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11594 11027 603 41 0 11553 0
vsize: 46376
[startup+530.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11197 0 0 0 52984 33 0 0 25 0 1 0 423719742 47489024 11027 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11594 11027 603 41 0 11553 0
vsize: 46376
[startup+540.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11197 0 0 0 53985 33 0 0 25 0 1 0 423719742 47489024 11027 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11594 11027 603 41 0 11553 0
vsize: 46376
[startup+550.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11197 0 0 0 54985 33 0 0 25 0 1 0 423719742 47489024 11027 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11594 11027 603 41 0 11553 0
vsize: 46376
[startup+560.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11201 0 0 0 55986 33 0 0 25 0 1 0 423719742 47751168 11031 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11658 11031 603 41 0 11617 0
vsize: 46632
[startup+570.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 56986 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+580.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 57986 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+590.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 58987 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+600.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 59987 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223648 134560523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+610.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 60987 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+620.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 61988 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+630.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 62988 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+640.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 63989 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+650.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 64989 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+660.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 65989 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+670.034 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 66990 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+680.034 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 67990 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+690.034 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 68990 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+700.033 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 69991 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+710.034 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11305 0 0 0 70991 33 0 0 25 0 1 0 423719742 48156672 11135 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11757 11135 603 41 0 11716 0
vsize: 47028
[startup+720.034 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11686 0 0 0 71990 34 0 0 25 0 1 0 423719742 49766400 11516 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12150 11516 603 41 0 12109 0
vsize: 48600
[startup+730.033 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11953 0 0 0 72990 35 0 0 25 0 1 0 423719742 50851840 11783 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12415 11783 603 41 0 12374 0
vsize: 49660
[startup+740.033 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11953 0 0 0 73990 35 0 0 25 0 1 0 423719742 50851840 11783 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12415 11783 603 41 0 12374 0
vsize: 49660
[startup+750.033 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11953 0 0 0 74990 35 0 0 25 0 1 0 423719742 50851840 11783 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12415 11783 603 41 0 12374 0
vsize: 49660
[startup+760.032 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11953 0 0 0 75991 35 0 0 25 0 1 0 423719742 50851840 11783 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12415 11783 603 41 0 12374 0
vsize: 49660
[startup+770.032 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11953 0 0 0 76991 35 0 0 25 0 1 0 423719742 50851840 11783 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12415 11783 603 41 0 12374 0
vsize: 49660
[startup+780.032 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11953 0 0 0 77990 35 0 0 25 0 1 0 423719742 50851840 11783 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12415 11783 603 41 0 12374 0
vsize: 49660
[startup+790.031 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11953 0 0 0 78990 35 0 0 25 0 1 0 423719742 50851840 11783 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12415 11783 603 41 0 12374 0
vsize: 49660
[startup+800.031 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 11953 0 0 0 79990 35 0 0 25 0 1 0 423719742 50851840 11783 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12415 11783 603 41 0 12374 0
vsize: 49660
[startup+810.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 12646 0 0 0 80989 36 0 0 25 0 1 0 423719742 53669888 12476 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13103 12476 603 41 0 13062 0
vsize: 52412
[startup+820.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 13296 0 0 0 81987 39 0 0 25 0 1 0 423719742 56365056 13126 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13761 13126 603 41 0 13720 0
vsize: 55044
[startup+830.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 13927 0 0 0 82985 41 0 0 25 0 1 0 423719742 58920960 13757 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14385 13757 603 41 0 14344 0
vsize: 57540
[startup+840.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 14530 0 0 0 83984 42 0 0 25 0 1 0 423719742 61464576 14360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15006 14360 603 41 0 14965 0
vsize: 60024
[startup+850.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15106 0 0 0 84984 43 0 0 25 0 1 0 423719742 63750144 14936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15564 14936 603 41 0 15523 0
vsize: 62256
[startup+860.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 85982 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+870.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 86982 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+880.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 87983 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+890.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 88983 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+900.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 89983 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+910.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 90984 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+920.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 91984 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+930.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 92984 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+940.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 93985 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+950.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 94985 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+960.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 95985 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+970.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 96986 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+980.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15497 0 0 0 97986 45 0 0 25 0 1 0 423719742 65359872 15327 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15327 603 41 0 15916 0
vsize: 63828
[startup+990.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 15750 0 0 0 98985 46 0 0 25 0 1 0 423719742 66420736 15580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16216 15580 603 41 0 16175 0
vsize: 64864
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16270 0 0 0 99984 47 0 0 25 0 1 0 423719742 68583424 16100 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16100 603 41 0 16703 0
vsize: 66976
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 100984 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 101984 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 102985 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 103985 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 104985 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 105985 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 106986 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 107986 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 108986 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 109987 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 110987 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 111987 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 112988 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 113988 47 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 114988 48 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 115988 48 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 116988 48 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 117988 48 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 118989 48 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3357
Raw data (stat): 3357 (minisat+) R 3356 29653 29652 0 -1 0 16272 0 0 0 119989 48 0 0 25 0 1 0 423719742 68583424 16102 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 16102 603 41 0 16703 0
vsize: 66976
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 3357
Raw data (stat): 3357 (minisat+) Z 3356 29653 29652 0 -1 12 16275 0 0 0 119989 51 0 0 25 0 1 0 423719742 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.41
CPU user time (s): 1199.89
CPU system time (s): 0.513921
CPU usage (%): 100.029
Max. virtual memory (Kb): 66976
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####