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 5096

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-13 21:55:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3299 boxname=wulflinc4 idbench=367 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  f82b685b64af240616b701a750c82883  /oldhome/oroussel/tmp/wulflinc4/normalized-10:20:4.5:0.95:100.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc4/normalized-10:20:4.5:0.95:100.opb
IDLAUNCH: 3299
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        922940 kB
Buffers:         34648 kB
Cached:          57696 kB
SwapCached:          0 kB
Active:          52052 kB
Inactive:        43128 kB
HighTotal:      131008 kB
HighFree:        69580 kB
LowTotal:       903652 kB
LowFree:        853360 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11000 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:15:22 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 3299 7 1200.19 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 |   11765    33737 |    3921       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2083   maxlim: 470   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26254    85464 |    8751       0        0     nan |  0.000 % |
c |       100 |   26254    85464 |    9626     100      343     3.4 |  2.467 % |
c |       250 |   26254    85464 |   10588     250     1104     4.4 |  2.467 % |
c |       475 |   26254    85464 |   11647     475     2363     5.0 |  2.467 % |
c ==============================================================================
c [1mFound solution: 181[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6   maxlim: 1321   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       598 |   26298    85623 |    8766     598     3233     5.4 |  2.467 % |
c |       698 |   26298    85623 |    9642     698     3737     5.4 |  2.528 % |
c |       848 |   26298    85623 |   10606     848     4598     5.4 |  2.528 % |
c ==============================================================================
c [1mFound solution: 163[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1339   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       947 |   26301    85653 |    8767     947     5260     5.6 |  2.528 % |
c |      1047 |   26301    85653 |    9643    1047    10883    10.4 |  2.566 % |
c |      1197 |   26301    85653 |   10608    1197    11640     9.7 |  2.566 % |
c |      1423 |   26301    85653 |   11668    1423    12608     8.9 |  2.566 % |
c |      1761 |   26301    85653 |   12835    1761    20677    11.7 |  2.566 % |
c |      2267 |   26301    85653 |   14119    2267    25319    11.2 |  2.566 % |
c |      3026 |   26301    85653 |   15531    3026    32992    10.9 |  2.566 % |
c |      4165 |   26301    85653 |   17084    4165    76574    18.4 |  2.566 % |
c ==============================================================================
c [1mFound solution: 156[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1346   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5406 |   26304    85685 |    8768    5406   109895    20.3 |  2.566 % |
c |      5506 |   26304    85685 |    9644    5506   110609    20.1 |  2.604 % |
c |      5656 |   26304    85685 |   10609    5656   111837    19.8 |  2.604 % |
c |      5881 |   26304    85685 |   11670    5881   113973    19.4 |  2.604 % |
c |      6218 |   26304    85685 |   12837    6218   131714    21.2 |  2.604 % |
c |      6725 |   26304    85685 |   14120    6725   140326    20.9 |  2.604 % |
c ==============================================================================
c [1mFound solution: 153[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1349   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6834 |   26307    85710 |    8769    6834   141638    20.7 |  2.604 % |
c |      6935 |   26307    85710 |    9645    6935   142296    20.5 |  2.629 % |
c |      7085 |   26307    85710 |   10610    7085   145694    20.6 |  2.629 % |
c |      7311 |   26307    85710 |   11671    7311   150011    20.5 |  2.629 % |
c |      7648 |   26307    85710 |   12838    7648   156902    20.5 |  2.629 % |
c |      8155 |   26307    85710 |   14122    8155   166831    20.5 |  2.629 % |
c ==============================================================================
c [1mFound solution: 149[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1353   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8193 |   26310    85734 |    8770    8193   167205    20.4 |  2.629 % |
c |      8294 |   26310    85734 |    9647    8294   169827    20.5 |  2.653 % |
c |      8444 |   26310    85734 |   10611    8444   173171    20.5 |  2.653 % |
c ==============================================================================
c [1mFound solution: 119[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1383   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8489 |   26313    85754 |    8771    8489   173868    20.5 |  2.653 % |
c |      8589 |   26313    85754 |    9648    8589   175445    20.4 |  2.678 % |
c |      8741 |   26313    85754 |   10612    8741   179565    20.5 |  2.678 % |
c |      8970 |   26313    85754 |   11674    8970   190687    21.3 |  2.678 % |
c ==============================================================================
c [1mFound solution: 115[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1387   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9032 |   26314    85765 |    8771    9032   191792    21.2 |  2.678 % |
c |      9132 |   26314    85765 |    9648    4616    65488    14.2 |  2.691 % |
c |      9282 |   26314    85765 |   10612    4766    68161    14.3 |  2.691 % |
c |      9507 |   26314    85765 |   11674    4991    71384    14.3 |  2.691 % |
c ==============================================================================
c [1mFound solution: 99[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1403   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9579 |   26319    85799 |    8773    5063    72243    14.3 |  2.691 % |
c |      9679 |   26319    85799 |    9650    5163    75617    14.6 |  2.727 % |
c |      9829 |   26319    85799 |   10615    5313    81023    15.2 |  2.727 % |
c |     10054 |   26319    85799 |   11676    5538    85759    15.5 |  2.727 % |
c |     10391 |   26319    85799 |   12844    5875   102244    17.4 |  2.727 % |
c |     10899 |   26319    85799 |   14129    6383   114696    18.0 |  2.727 % |
c |     11660 |   26319    85799 |   15541    7144   153240    21.5 |  2.727 % |
c |     12803 |   26319    85799 |   17096    8287   178552    21.5 |  2.727 % |
c |     14511 |   26319    85799 |   18805    9995   335353    33.6 |  2.727 % |
c |     17073 |   26319    85799 |   20686   12557   429140    34.2 |  2.727 % |
c |     20918 |   26319    85799 |   22754   16402   711043    43.4 |  2.727 % |
c |     26684 |   26319    85799 |   25030   22168  1226739    55.3 |  2.727 % |
c |     35333 |   26319    85799 |   27533   17951  1054818    58.8 |  2.727 % |
c |     48307 |   26319    85799 |   30286   30925  2515081    81.3 |  2.727 % |
c |     67770 |   26319    85799 |   33315   31790  3204216   100.8 |  2.727 % |
c |     96962 |   26319    85799 |   36646   18679  1913143   102.4 |  2.727 % |
c ==============================================================================
c [1mFound solution: 95[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1407   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98583 |   26320    85805 |    8773   20300  1958586    96.5 |  2.727 % |
c |     98683 |   26320    85805 |    9650    5175   155331    30.0 |  2.740 % |
c |     98833 |   26320    85805 |   10615    5325   156444    29.4 |  2.740 % |
c |     99059 |   26320    85805 |   11676    5551   166652    30.0 |  2.740 % |
c |     99396 |   26320    85805 |   12844    5888   171971    29.2 |  2.740 % |
c |     99903 |   26320    85805 |   14129    6395   206962    32.4 |  2.740 % |
c |    100662 |   26320    85805 |   15541    7154   245414    34.3 |  2.740 % |
c |    101801 |   26320    85805 |   17096    8293   299653    36.1 |  2.740 % |
c |    103509 |   26320    85805 |   18805   10001   404090    40.4 |  2.740 % |
c |    106072 |   26320    85805 |   20686   12564   580738    46.2 |  2.740 % |
c |    109916 |   26320    85805 |   22754   16408   859132    52.4 |  2.740 % |
c |    115682 |   26320    85805 |   25030   22174  1205307    54.4 |  2.740 % |
c |    124334 |   26320    85805 |   27533   14392  1232687    85.7 |  2.740 % |
c |    137308 |   26320    85805 |   30286   27366  3191732   116.6 |  2.740 % |
c |    156769 |   26320    85805 |   33315   27184  3327775   122.4 |  2.740 % |
c |    185961 |   26320    85805 |   36646   34727  3023365    87.1 |  2.740 % |
c |    229750 |   26320    85805 |   40311   29036  4174333   143.8 |  2.740 % |
c |    295435 |   26320    85805 |   44342   35733  4821179   134.9 |  2.740 % |
c |    393962 |   26320    85805 |   48777   31245  7114255   227.7 |  2.740 % |
c ==============================================================================
c [1mFound solution: 93[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1409   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    402965 |   26322    85819 |    8774   40248  7669094   190.5 |  2.740 % |
c |    403065 |   26322    85819 |    9651    7692   428249    55.7 |  2.752 % |
c |    403215 |   26322    85819 |   10616    7842   429152    54.7 |  2.752 % |
c |    403440 |   26322    85819 |   11678    8067   430639    53.4 |  2.752 % |
c |    403778 |   26322    85819 |   12846    8405   444954    52.9 |  2.752 % |
c |    404285 |   26322    85819 |   14130    8912   451552    50.7 |  2.752 % |
c |    405044 |   26322    85819 |   15543    9671   460234    47.6 |  2.752 % |
c |    406184 |   26322    85819 |   17098   10811   485817    44.9 |  2.752 % |
c |    407892 |   26322    85819 |   18807   12519   577961    46.2 |  2.752 % |
c |    410455 |   26322    85819 |   20688   15082   703570    46.6 |  2.752 % |
c |    414299 |   26322    85819 |   22757   18926   957487    50.6 |  2.752 % |
c |    420065 |   26322    85819 |   25033   24692  1288839    52.2 |  2.752 % |
c |    428714 |   26322    85819 |   27536   19026  1376838    72.4 |  2.752 % |
c |    441690 |   26322    85819 |   30290   32002  2455886    76.7 |  2.752 % |
c |    461154 |   26322    85819 |   33319   32530  2789845    85.8 |  2.752 % |
c |    490346 |   26322    85819 |   36651   18436  2229327   120.9 |  2.752 % |
c |    534136 |   26322    85819 |   40316   35911  6004074   167.2 |  2.752 % |
c |    599820 |   26322    85819 |   44347   43924  8128207   185.1 |  2.752 % |
c |    698346 |   26322    85819 |   48782   46314  7937399   171.4 |  2.752 % |
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 -v887 v#### 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.84 0.94 0.91 2/54 9322
Raw data (stat): 9322 (runsolver) R 9321 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421128317 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0012 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 2153 0 0 0 992 6 0 0 25 0 1 0 421128317 10403840 2005 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2540 2005 603 41 0 2499 0
vsize: 10160
[startup+20.0021 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 3303 0 0 0 1987 10 0 0 25 0 1 0 421128317 15237120 3155 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3155 603 41 0 3679 0
vsize: 14880
[startup+30.0034 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 3607 0 0 0 2986 11 0 0 25 0 1 0 421128317 16445440 3459 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4015 3459 603 41 0 3974 0
vsize: 16060
[startup+40.0037 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 4546 0 0 0 3982 15 0 0 25 0 1 0 421128317 20209664 4398 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4934 4398 603 41 0 4893 0
vsize: 19736
[startup+50.0046 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 4720 0 0 0 4981 16 0 0 25 0 1 0 421128317 20881408 4572 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5098 4572 603 41 0 5057 0
vsize: 20392
[startup+60.005 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 5092 0 0 0 5980 17 0 0 25 0 1 0 421128317 22491136 4944 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5491 4944 603 41 0 5450 0
vsize: 21964
[startup+70.0063 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 5757 0 0 0 6978 19 0 0 25 0 1 0 421128317 25309184 5609 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6179 5609 603 41 0 6138 0
vsize: 24716
[startup+80.0082 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 5757 0 0 0 7978 19 0 0 25 0 1 0 421128317 25309184 5609 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6179 5609 603 41 0 6138 0
vsize: 24716
[startup+90.0086 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 5883 0 0 0 8978 20 0 0 25 0 1 0 421128317 25849856 5735 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6311 5735 603 41 0 6270 0
vsize: 25244
[startup+100.009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6738 0 0 0 9974 23 0 0 25 0 1 0 421128317 29331456 6590 4294967295 134512640 134672761 3221224624 3221223756 1075347104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7161 6590 603 41 0 7120 0
vsize: 28644
[startup+110.01 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 10973 24 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+120.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 11973 24 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223728 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+130.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 12973 24 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223808 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+140.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 13973 24 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+150.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 14972 25 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+160.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 15972 25 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+170.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 16972 25 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+180.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 17972 25 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+190.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 18972 25 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 19972 25 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+210.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 20973 25 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+220.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6760 0 0 0 21973 25 0 0 25 0 1 0 421128317 29466624 6612 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6612 603 41 0 7153 0
vsize: 28776
[startup+230.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6764 0 0 0 22973 25 0 0 25 0 1 0 421128317 29466624 6616 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6616 603 41 0 7153 0
vsize: 28776
[startup+240.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6764 0 0 0 23973 25 0 0 25 0 1 0 421128317 29466624 6616 4294967295 134512640 134672761 3221224624 3221223728 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6616 603 41 0 7153 0
vsize: 28776
[startup+250.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 6764 0 0 0 24973 25 0 0 25 0 1 0 421128317 29466624 6616 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6616 603 41 0 7153 0
vsize: 28776
[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 7290 0 0 0 25972 27 0 0 25 0 1 0 421128317 31612928 7142 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7718 7142 603 41 0 7677 0
vsize: 30872
[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8015 0 0 0 26970 29 0 0 25 0 1 0 421128317 34566144 7867 4294967295 134512640 134672761 3221224624 3221223728 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8439 7867 603 41 0 8398 0
vsize: 33756
[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9322
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8331 0 0 0 27969 30 0 0 25 0 1 0 421128317 35913728 8183 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8768 8183 603 41 0 8727 0
vsize: 35072
[startup+290.02 s]
Raw data (loadavg): 1.07 0.98 0.91 3/56 9369
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8332 0 0 0 28969 30 0 0 25 0 1 0 421128317 35913728 8184 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8768 8184 603 41 0 8727 0
vsize: 35072
[startup+300.02 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 9375
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8332 0 0 0 29968 31 0 0 25 0 1 0 421128317 35913728 8184 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8768 8184 603 41 0 8727 0
vsize: 35072
[startup+310.021 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 9375
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8334 0 0 0 30968 31 0 0 25 0 1 0 421128317 35913728 8186 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8768 8186 603 41 0 8727 0
vsize: 35072
[startup+320.02 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 9375
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 31967 32 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223808 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+330.021 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 9375
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 32967 33 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+340.021 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 9375
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 33967 33 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+350.021 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 9375
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 34966 34 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+360.022 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 9375
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 35967 34 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+370.022 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 36966 34 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+380.022 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 37966 35 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+390.023 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 38966 35 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+400.023 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 39966 35 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+410.023 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 40966 36 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+420.023 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 41966 36 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+430.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 8500 0 0 0 42965 36 0 0 25 0 1 0 421128317 36581376 8352 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8931 8352 603 41 0 8890 0
vsize: 35724
[startup+440.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9026 0 0 0 43964 38 0 0 25 0 1 0 421128317 38735872 8878 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9457 8878 603 41 0 9416 0
vsize: 37828
[startup+450.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9361 0 0 0 44962 40 0 0 25 0 1 0 421128317 40075264 9213 4294967295 134512640 134672761 3221224624 3221223728 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9784 9213 603 41 0 9743 0
vsize: 39136
[startup+460.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9361 0 0 0 45962 41 0 0 25 0 1 0 421128317 40075264 9213 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9784 9213 603 41 0 9743 0
vsize: 39136
[startup+470.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9361 0 0 0 46962 41 0 0 25 0 1 0 421128317 40075264 9213 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9784 9213 603 41 0 9743 0
vsize: 39136
[startup+480.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9362 0 0 0 47962 41 0 0 25 0 1 0 421128317 40075264 9214 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9784 9214 603 41 0 9743 0
vsize: 39136
[startup+490.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9362 0 0 0 48962 41 0 0 25 0 1 0 421128317 40075264 9214 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9784 9214 603 41 0 9743 0
vsize: 39136
[startup+500.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9362 0 0 0 49961 42 0 0 25 0 1 0 421128317 40075264 9214 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9784 9214 603 41 0 9743 0
vsize: 39136
[startup+510.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9821 0 0 0 50960 43 0 0 25 0 1 0 421128317 41951232 9673 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10242 9673 603 41 0 10201 0
vsize: 40968
[startup+520.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9892 0 0 0 51960 43 0 0 25 0 1 0 421128317 42221568 9744 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10308 9744 603 41 0 10267 0
vsize: 41232
[startup+530.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9892 0 0 0 52960 44 0 0 25 0 1 0 421128317 42221568 9744 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10308 9744 603 41 0 10267 0
vsize: 41232
[startup+540.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9892 0 0 0 53960 44 0 0 25 0 1 0 421128317 42221568 9744 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10308 9744 603 41 0 10267 0
vsize: 41232
[startup+550.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9892 0 0 0 54959 44 0 0 25 0 1 0 421128317 42221568 9744 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10308 9744 603 41 0 10267 0
vsize: 41232
[startup+560.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 9892 0 0 0 55960 44 0 0 25 0 1 0 421128317 42221568 9744 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10308 9744 603 41 0 10267 0
vsize: 41232
[startup+570.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 10218 0 0 0 56959 46 0 0 25 0 1 0 421128317 43569152 10070 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10637 10070 603 41 0 10596 0
vsize: 42548
[startup+580.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11067 0 0 0 57956 48 0 0 25 0 1 0 421128317 47050752 10919 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11487 10919 603 41 0 11446 0
vsize: 45948
[startup+590.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 58954 50 0 0 25 0 1 0 421128317 48926720 11369 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11945 11369 603 41 0 11904 0
vsize: 47780
[startup+600.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 59954 51 0 0 25 0 1 0 421128317 48926720 11369 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11945 11369 603 41 0 11904 0
vsize: 47780
[startup+610.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 60954 51 0 0 25 0 1 0 421128317 48926720 11369 4294967295 134512640 134672761 3221224624 3221223808 134559618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11945 11369 603 41 0 11904 0
vsize: 47780
[startup+620.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 61953 52 0 0 25 0 1 0 421128317 48926720 11369 4294967295 134512640 134672761 3221224624 3221223792 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11945 11369 603 41 0 11904 0
vsize: 47780
[startup+630.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 62953 52 0 0 25 0 1 0 421128317 48926720 11369 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11945 11369 603 41 0 11904 0
vsize: 47780
[startup+640.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 63953 52 0 0 25 0 1 0 421128317 48926720 11369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11945 11369 603 41 0 11904 0
vsize: 47780
[startup+650.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9377
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 64953 53 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223624 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+660.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 65952 54 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+670.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 66952 54 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223728 134559784 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+680.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 67952 54 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+690.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 68952 55 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+700.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 69951 55 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+710.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 70951 56 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+720.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 71951 56 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+730.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 72950 57 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+740.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 73950 57 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+750.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 74950 57 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+760.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 75950 58 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+770.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 76949 58 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+780.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 77949 59 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+790.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 78949 59 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+800.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 79949 59 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+810.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 80949 59 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+820.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 81949 59 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+830.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 82949 60 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+840.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 83949 60 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+850.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 84949 60 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+860.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 85949 60 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+870.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 86949 61 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223760 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+880.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 87948 61 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+890.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 88948 62 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223728 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+900.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 89948 62 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+910.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 90948 62 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+920.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 91947 63 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+930.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 92947 63 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223808 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+940.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 93947 64 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+950.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 94947 64 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+960.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 95947 65 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+970.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11517 0 0 0 96946 65 0 0 25 0 1 0 421128317 48922624 11369 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11944 11369 603 41 0 11903 0
vsize: 47776
[startup+980.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 11697 0 0 0 97946 66 0 0 25 0 1 0 421128317 49594368 11549 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12108 11549 603 41 0 12067 0
vsize: 48432
[startup+990.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12232 0 0 0 98944 68 0 0 25 0 1 0 421128317 51761152 12084 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12637 12084 603 41 0 12596 0
vsize: 50548
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 99943 69 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 100943 69 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 101943 69 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 102943 69 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 103942 70 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 104943 70 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223624 1075349950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 105942 71 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 106942 71 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 107942 71 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 108941 72 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 109941 72 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 110941 72 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 111941 73 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 112941 73 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 113941 73 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223824 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12271 0 0 0 114940 74 0 0 25 0 1 0 421128317 52027392 12123 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12702 12123 603 41 0 12661 0
vsize: 50808
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 12643 0 0 0 115939 76 0 0 25 0 1 0 421128317 53497856 12495 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13061 12495 603 41 0 13020 0
vsize: 52244
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 13098 0 0 0 116938 77 0 0 25 0 1 0 421128317 55386112 12950 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13522 12950 603 41 0 13481 0
vsize: 54088
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 13098 0 0 0 117937 77 0 0 25 0 1 0 421128317 55386112 12950 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13522 12950 603 41 0 13481 0
vsize: 54088
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 13098 0 0 0 118937 78 0 0 25 0 1 0 421128317 55386112 12950 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13522 12950 603 41 0 13481 0
vsize: 54088
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 9379
Raw data (stat): 9322 (minisat+) R 9321 5897 5896 0 -1 0 13098 0 0 0 119937 78 0 0 25 0 1 0 421128317 55386112 12950 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13522 12950 603 41 0 13481 0
vsize: 54088
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 9379
Raw data (stat): 9322 (minisat+) Z 9321 5897 5896 0 -1 12 13101 0 0 0 119937 81 0 0 25 0 1 0 421128317 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.19
CPU user time (s): 1199.38
CPU system time (s): 0.812876
CPU usage (%): 100.01
Max. virtual memory (Kb): 54088
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####