PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-10teams.opb
MD5SUM	1ff3cc3253012886aa21be4feac6111e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	920
Optimality of the best value was proved	NO
Number of terms in the objective function	1800
Biggest coefficient in the objective function	86
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	41700
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	86
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	41700
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.75
Number of variables	1800
Total number of constraints	2015
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2015
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	72
Trace number 18884

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        691024 kB
Buffers:         26936 kB
Cached:         292380 kB
SwapCached:        556 kB
Active:          49148 kB
Inactive:       272224 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        690772 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5164 kB
Slab:            16600 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:18:47 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 17373 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 330 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 329]---> BDD-cost:  125
c ---[ 328]---> BDD-cost:  185
c ---[ 326]---> BDD-cost:   77
c ---[ 324]---> BDD-cost:   77
c ---[ 322]---> BDD-cost:   77
c ---[ 320]---> BDD-cost:   77
c ---[ 318]---> BDD-cost:   77
c ---[ 316]---> BDD-cost:   77
c ---[ 314]---> BDD-cost:   77
c ---[ 312]---> BDD-cost:   77
c ---[ 310]---> BDD-cost:   77
c ---[ 308]---> BDD-cost:   77
c ---[ 307]---> BDD-cost:  185
c ---[ 305]---> BDD-cost:   77
c ---[ 303]---> BDD-cost:   77
c ---[ 301]---> BDD-cost:   77
c ---[ 299]---> BDD-cost:   77
c ---[ 297]---> BDD-cost:   77
c ---[ 295]---> BDD-cost:   77
c ---[ 293]---> BDD-cost:   77
c ---[ 291]---> BDD-cost:   77
c ---[ 289]---> BDD-cost:   77
c ---[ 288]---> BDD-cost:  125
c ---[ 286]---> BDD-cost:   77
c ---[ 284]---> BDD-cost:   77
c ---[ 282]---> BDD-cost:   77
c ---[ 280]---> BDD-cost:   77
c ---[ 278]---> BDD-cost:   77
c ---[ 276]---> BDD-cost:   77
c ---[ 274]---> BDD-cost:   77
c ---[ 272]---> BDD-cost:   77
c ---[ 270]---> BDD-cost:   77
c ---[ 269]---> BDD-cost:  185
c ---[ 267]---> BDD-cost:   77
c ---[ 265]---> BDD-cost:   77
c ---[ 263]---> BDD-cost:   77
c ---[ 261]---> BDD-cost:   77
c ---[ 259]---> BDD-cost:   77
c ---[ 257]---> BDD-cost:   77
c ---[ 255]---> BDD-cost:   77
c ---[ 253]---> BDD-cost:   77
c ---[ 251]---> BDD-cost:   77
c ---[ 250]---> BDD-cost:  185
c ---[ 248]---> BDD-cost:   70
c ---[ 246]---> BDD-cost:   77
c ---[ 244]---> BDD-cost:   77
c ---[ 242]---> BDD-cost:   77
c ---[ 240]---> BDD-cost:   77
c ---[ 238]---> BDD-cost:   77
c ---[ 236]---> BDD-cost:   77
c ---[ 234]---> BDD-cost:   77
c ---[ 233]---> BDD-cost:  185
c ---[ 231]---> BDD-cost:   77
c ---[ 229]---> BDD-cost:   77
c ---[ 227]---> BDD-cost:   77
c ---[ 225]---> BDD-cost:   77
c ---[ 223]---> BDD-cost:   77
c ---[ 221]---> BDD-cost:   77
c ---[ 219]---> BDD-cost:   77
c ---[ 217]---> BDD-cost:   77
c ---[ 216]---> BDD-cost:  185
c ---[ 214]---> BDD-cost:   70
c ---[ 212]---> BDD-cost:   77
c ---[ 210]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:   77
c ---[ 206]---> BDD-cost:   77
c ---[ 204]---> BDD-cost:   77
c ---[ 202]---> BDD-cost:   77
c ---[ 200]---> BDD-cost:   77
c ---[ 198]---> BDD-cost:   70
c ---[ 197]---> BDD-cost:  185
c ---[ 195]---> BDD-cost:   77
c ---[ 193]---> BDD-cost:   77
c ---[ 191]---> BDD-cost:   77
c ---[ 189]---> BDD-cost:   77
c ---[ 187]---> BDD-cost:   77
c ---[ 185]---> BDD-cost:   77
c ---[ 183]---> BDD-cost:   77
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   77
c ---[ 178]---> BDD-cost:  125
c ---[ 176]---> BDD-cost:   77
c ---[ 174]---> BDD-cost:   77
c ---[ 172]---> BDD-cost:   77
c ---[ 170]---> BDD-cost:   77
c ---[ 168]---> BDD-cost:   77
c ---[ 166]---> BDD-cost:   77
c ---[ 164]---> BDD-cost:   77
c ---[ 162]---> BDD-cost:   77
c ---[ 160]---> BDD-cost:   77
c ---[ 159]---> BDD-cost:  185
c ---[ 157]---> BDD-cost:   77
c ---[ 155]---> BDD-cost:   77
c ---[ 153]---> BDD-cost:   77
c ---[ 151]---> BDD-cost:   77
c ---[ 149]---> BDD-cost:   77
c ---[ 147]---> BDD-cost:   77
c ---[ 145]---> BDD-cost:   77
c ---[ 143]---> BDD-cost:   77
c ---[ 141]---> BDD-cost:   77
c ---[ 140]---> BDD-cost:  185
c ---[ 139]---> BDD-cost:  185
c ---[ 137]---> BDD-cost:   77
c ---[ 135]---> BDD-cost:   77
c ---[ 133]---> BDD-cost:   77
c ---[ 131]---> BDD-cost:   77
c ---[ 129]---> BDD-cost:   77
c ---[ 127]---> BDD-cost:   77
c ---[ 125]---> BDD-cost:   77
c ---[ 123]---> BDD-cost:   77
c ---[ 121]---> BDD-cost:   77
c ---[ 120]---> BDD-cost:  178
c ---[ 118]---> BDD-cost:   77
c ---[ 116]---> BDD-cost:   77
c ---[ 114]---> BDD-cost:   77
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:   77
c ---[ 108]---> BDD-cost:   77
c ---[ 106]---> BDD-cost:   77
c ---[ 104]---> BDD-cost:   77
c ---[ 102]---> BDD-cost:   77
c ---[ 101]---> BDD-cost:  185
c ---[  99]---> BDD-cost:   77
c ---[  97]---> BDD-cost:   77
c ---[  95]---> BDD-cost:   77
c ---[  93]---> BDD-cost:   77
c ---[  91]---> BDD-cost:   77
c ---[  89]---> BDD-cost:   77
c ---[  87]---> BDD-cost:   77
c ---[  85]---> BDD-cost:   77
c ---[  83]---> BDD-cost:   77
c ---[  82]---> BDD-cost:  125
c ---[  80]---> BDD-cost:   77
c ---[  79]---> BDD-cost:  185
c ---[  78]---> BDD-cost:  185
c ---[  77]---> BDD-cost:  178
c ---[  76]---> BDD-cost:  185
c ---[  75]---> BDD-cost:  185
c ---[  74]---> BDD-cost:  125
c ---[  73]---> BDD-cost:  185
c ---[  72]---> BDD-cost:  185
c ---[  71]---> BDD-cost:  178
c ---[  70]---> BDD-cost:  185
c ---[  69]---> BDD-cost:  185
c ---[  68]---> BDD-cost:  125
c ---[  67]---> BDD-cost:  185
c ---[  66]---> BDD-cost:  178
c ---[  65]---> BDD-cost:  185
c ---[  64]---> BDD-cost:  185
c ---[  63]---> BDD-cost:  185
c ---[  62]---> BDD-cost:  185
c ---[  61]---> BDD-cost:  125
c ---[  60]---> BDD-cost:  118
c ---[  59]---> BDD-cost:  185
c ---[  58]---> BDD-cost:  185
c ---[  57]---> BDD-cost:  185
c ---[  56]---> BDD-cost:  185
c ---[  55]---> BDD-cost:  178
c ---[  54]---> BDD-cost:  185
c ---[  53]---> BDD-cost:  185
c ---[  52]---> BDD-cost:  185
c ---[  51]---> BDD-cost:  185
c ---[  50]---> BDD-cost:  125
c ---[  49]---> BDD-cost:   76
c ---[  48]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  46]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  44]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  42]---> BDD-cost:   76
c ---[  41]---> BDD-cost:  177
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:  123
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:  183
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   75
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:  183
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   53221   141547 |   17740       0        0     nan |  0.000 % |
c |       100 |   53221   141547 |   19514     100     2449    24.5 |  1.808 % |
c |       251 |   53221   141547 |   21465     251    20371    81.2 |  1.808 % |
c |       476 |   53221   141547 |   23611     476    41787    87.8 |  1.808 % |
c |       813 |   53221   141547 |   25973     813    88284   108.6 |  1.808 % |
c ==============================================================================
c [1mFound solution: 1004[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7750   maxlim: 38996   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1052 |  107348   334850 |   35782    1052   103950    98.8 |  1.808 % |
c |      1153 |  107348   334850 |   39360    1153   107715    93.4 |  1.396 % |
c |      1304 |  107348   334850 |   43296    1304   116225    89.1 |  1.396 % |
c |      1529 |  107348   334850 |   47625    1529   123219    80.6 |  1.396 % |
c |      1866 |  107348   334850 |   52388    1866   156815    84.0 |  1.396 % |
c ==============================================================================
c [1mFound solution: 1002[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 38998   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2203 |  107352   334879 |   35784    2203   222373   100.9 |  1.396 % |
c |      2303 |  107352   334879 |   39362    2303   231648   100.6 |  1.403 % |
c |      2454 |  107352   334879 |   43298    2454   238130    97.0 |  1.403 % |
c |      2679 |  107352   334879 |   47628    2679   261418    97.6 |  1.403 % |
c |      3017 |  107352   334879 |   52391    3017   299302    99.2 |  1.403 % |
c |      3523 |  107352   334879 |   57630    3523   358994   101.9 |  1.403 % |
c |      4282 |  107352   334879 |   63393    4282   556963   130.1 |  1.403 % |
c |      5423 |  107352   334879 |   69732    5423   668556   123.3 |  1.403 % |
c |      7131 |  107352   334879 |   76706    7131  1051149   147.4 |  1.403 % |
c |      9693 |  107352   334879 |   84376    9693  1678687   173.2 |  1.403 % |
c ==============================================================================
c [1mFound solution: 996[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39004   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10487 |  107358   334918 |   35786   10487  1847516   176.2 |  1.403 % |
c |     10587 |  107358   334918 |   39364   10587  1855693   175.3 |  1.412 % |
c |     10742 |  107358   334918 |   43301   10742  1874690   174.5 |  1.412 % |
c |     10967 |  107358   334918 |   47631   10967  1906062   173.8 |  1.412 % |
c |     11305 |  107358   334918 |   52394   11305  1959943   173.4 |  1.412 % |
c |     11812 |  107358   334918 |   57633   11812  1996652   169.0 |  1.412 % |
c |     12571 |  107358   334918 |   63397   12571  2137300   170.0 |  1.412 % |
c |     13711 |  107358   334918 |   69736   13711  2382440   173.8 |  1.412 % |
c |     15420 |  107358   334918 |   76710   15420  2702133   175.2 |  1.412 % |
c |     17982 |  107358   334918 |   84381   17982  3128960   174.0 |  1.412 % |
c |     21828 |  107358   334918 |   92819   21828  4322375   198.0 |  1.412 % |
c ==============================================================================
c [1mFound solution: 988[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39012   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26309 |  107364   334954 |   35788   26309  5311365   201.9 |  1.412 % |
c |     26410 |  107364   334954 |   39366   26410  5315345   201.3 |  1.422 % |
c |     26560 |  107364   334954 |   43303   26560  5332309   200.8 |  1.422 % |
c |     26785 |  107364   334954 |   47633   26785  5362018   200.2 |  1.422 % |
c |     27124 |  107364   334954 |   52397   27124  5390674   198.7 |  1.422 % |
c |     27630 |  107364   334954 |   57636   27630  5447812   197.2 |  1.422 % |
c |     28389 |  107364   334954 |   63400   28389  5585909   196.8 |  1.422 % |
c |     29531 |  107364   334954 |   69740   29531  5829841   197.4 |  1.422 % |
c |     31240 |  107364   334954 |   76714   31240  6204331   198.6 |  1.422 % |
c |     33803 |  107364   334954 |   84386   33803  6860637   203.0 |  1.422 % |
c ==============================================================================
c [1mFound solution: 968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39032   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36639 |  107367   334983 |   35789   36639  7564651   206.5 |  1.422 % |
c |     36739 |  107367   334983 |   39367   14978  2527851   168.8 |  1.432 % |
c |     36890 |  107367   334983 |   43304   15129  2533125   167.4 |  1.432 % |
c |     37115 |  107367   334983 |   47635   15354  2573774   167.6 |  1.432 % |
c |     37454 |  107367   334983 |   52398   15693  2610219   166.3 |  1.432 % |
c |     37961 |  107367   334983 |   57638   16200  2689774   166.0 |  1.432 % |
c |     38720 |  107367   334983 |   63402   16959  2861332   168.7 |  1.432 % |
c |     39859 |  107367   334983 |   69742   18098  3049027   168.5 |  1.432 % |
c |     41567 |  107367   334983 |   76716   19806  3582639   180.9 |  1.432 % |
c |     44129 |  107367   334983 |   84388   22368  4081259   182.5 |  1.432 % |
c |     47975 |  107367   334983 |   92827   26214  4924789   187.9 |  1.432 % |
c |     53742 |  107367   334983 |  102110   31981  6839322   213.9 |  1.432 % |
c |     62393 |  107367   334983 |  112321   40632  9147539   225.1 |  1.432 % |
c |     75367 |  107367   334983 |  123553   53606 13432995   250.6 |  1.432 % |
c |     94828 |  107367   334983 |  135908   73067 18583473   254.3 |  1.432 % |
c ==============================================================================
c [1mFound solution: 962[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39038   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102932 |  107372   335020 |   35790   81171 21091129   259.8 |  1.432 % |
c |    103038 |  107372   335020 |   39369   18351  3797324   206.9 |  1.441 % |
c |    103188 |  107372   335020 |   43305   18501  3819105   206.4 |  1.441 % |
c |    103414 |  107372   335020 |   47636   18727  3851268   205.7 |  1.441 % |
c |    103751 |  107372   335020 |   52400   19064  3898650   204.5 |  1.441 % |
c |    104258 |  107372   335020 |   57640   19571  3960880   202.4 |  1.441 % |
c |    105018 |  107372   335020 |   63404   20331  4055134   199.5 |  1.441 % |
c |    106157 |  107372   335020 |   69744   21470  4306107   200.6 |  1.441 % |
c |    107866 |  107372   335020 |   76719   23179  4672492   201.6 |  1.441 % |
c |    110428 |  107372   335020 |   84390   25741  5195896   201.9 |  1.441 % |
c |    114274 |  107372   335020 |   92830   29587  5870348   198.4 |  1.441 % |
c |    120042 |  107372   335020 |  102113   35355  7088827   200.5 |  1.441 % |
c |    128698 |  107372   335020 |  112324   44011  9766073   221.9 |  1.441 % |
c |    141672 |  107372   335020 |  123556   56985 14217045   249.5 |  1.441 % |
c |    161142 |  107372   335020 |  135912   76455 21190245   277.2 |  1.441 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 -x234_bit0 -x235_bit0 -x236_bit0 -x237_bit0 -x238_bit0 -x239_bit0 -x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 -x252_bit0 -x253_bit0 -x254_bit0 -x255_bit0 -x256_bit0 -x257_bit0 -x258_bit0 -x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 -x287_bit0 -x288_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 x293_bit0 -x294_bit0 -x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x303_bit0 -x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 -x313_bit0 -x314_bit0 -x315_bit0 -x316_bit0 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 -x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 -x355_bit0 -x356_bit0 -x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 -x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 -x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 -x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 -x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 -x462_bit0 -x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 -x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 x485_bit0 -x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 -x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 -x499_bit0 -x500_bit0 -x501_bit0 -x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0 -x516_bit0 x517_bit0 -x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 -x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -x557_bit0 -x558_bit0 -x559_bit0 -x560_bit0 -x561_bit0 -x562_bit0 -x563_bit0 -x564_bit0 -x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 -x569_bit0 -x570_bit0 -x571_bit0 -x572_bit0 -x573_bit0 -x574_bit0 -x575_bit0 -x576_bit0 -x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 -x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0 -x589_bit0 -x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0 -x596_bit0 -x597_bit0 x598_bit0 -x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 -x603_bit0 -x604_bit0 -x605_bit0 -x606_bit0 -x607_bit0 -x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 -x621_bit0 -x622_bit0 -x623_bit0 -x624_bit0 -x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 -x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 -x642_bit0 -x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0 -x648_bit0 -x649_bit0 -x650_bit0 -x651_bit0 -x652_bit0 -x653_bit0 -x654_bit0 -x655_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0 -x666_bit0 -x667_bit0 -x668_bit0 -x669_bit0 -x670_bit0 x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 -x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x681_bit0 -x682_bit0 -x683_bit0 -x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0 -x694_bit0 -x695_bit0 -x696_bit0 -x697_bit0 -x698_bit0 -x699_bit0 -x700_bit0 -x701_bit0 x702_bit0 -x703_bit0 -x704_bit0 -x705_bit0 -x706_bit0 -x707_bit0 -x708_bit0 -x709_bit0 -x710_bit0 -x711_bit0 -x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 -x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x724_bit0 -x725_bit0 -x726_bit0 -x727_bit0 -x728_bit0 -x729_bit0 -x730_bit0 -x731_bit0 -x732_bit0 -x733_bit0 -x734_bit0 -x735_bit0 -x736_bit0 -x737_bit0 -x738_bit0 -x739_bit0 x740_bit0 -x741_bit0 -x742_bit0 -x743_bit0 -x744_bit0 -x745_bit0 -x746_bit0 -x747_bit0 -x748_bit0 -x749_bit0 -x750_bit0 -x751_bit0 -x752_bit0 -x753_bit0 -x754_bit0 -x755_bit0 -x756_bit0 -x757_bit0 -x758_bit0 -x759_bit0 -x760_bit0 -x761_bit0 -x762_bit0 -x763_bit0 -x764_bit0 -x765_bit0 -x766_bit0 -x767_bit0 -x768_bit0 -x769_bit0 -x770_bit0 -x771_bit0 -x772_bit0 -x773_bit0 -x774_bit0 -x775_bit0 -x776_bit0 -x777_bit0 -x778_bit0 -x779_bit0 -x780_bit0 -x781_bit0 -x782_bit0 -x783_bit0 -x784_bit0 -x785_bit0 -x786_bit0 -x787_bit0 -x788_bit0 -x789_bit0 -x790_bit0 -x791_bit0 -x792_bit0 -x793_bit0 -x794_bit0 -x795_bit0 -x796_bit0 -x797_bit0 -x798_bit0 -x799_bit0 -x800_bit0 -x801_bit0 x802_bit0 -x803_bit0 -x804_bit0 -x805_bit0 -x806_bit0 -x807_bit0 -x808_bit0 -x809_bit0 -x810_bit0 -x811_bit0 -x812_bit0 -x813_bit0 -x814_bit0 -x815_bit0 -x816_bit0 -x817_bit0 -x818_bit0 -x819_bit0 -x820_bit0 -x821_bit0 -x822_bit0 -x823_bit0 -x824_bit0 -x825_bit0 -x826_bit0 -x827_bit0 -x828_bit0 -x829_bit0 -x830_bit0 -x831_bit0 -x832_bit0 -x833_bit0 -x834_bit0 -x835_bit0 -x836_bit0 -x837_bit0 -x838_bit0 -x839_bit0 -x840_bit0 -x841_bit0 x842_bit0 -x843_bit0 -x844_bit0 -x845_bit0 -x846_bit0 -x847_bit0 -x848_bit0 -x849_bit0 -x850_bit0 -x851_bit0 -x852_bit0 -x853_bit0 -x854_bit0 -x855_bit0 -x856_bit0 -x857_bit0 x858_bit0 -x859_bit0 -x860_bit0 -x861_bit0 -x862_bit0 -x863_bit0 -x864_bit0 -x865_bit0 -x866_bit0 -x867_bit0 -x868_bit0 -x869_bit0 -x870_bit0 -x871_bit0 -x872_bit0 -x873_bit0 -x874_bit0 -x875_bit0 -x876_bit0 -x877_bit0 -x878_bit0 -x879_bit0 -x880_bit0 -x881_bit0 -x882_bit0 -x883_bit0 -x884_bit0 -x885_bit0 -x886_bit0 -x887_bit0 -x888_bit0 -x889_bit0 -x890_bit0 -x891_bit0 -x892_bit0 -x893_bit0 -x894_bit0 -x895_bit0 -x896_bit0 -x897_bit0 -x898_bit0 -x899_bit0 -x900_bit0 -x901_bit0 -x902_bit0 -x903_bit0 -x904_bit0 -x905_bit0 -x906_bit0 -x907_bit0 -x908_bit0 -x909_bit0 -x910_bit0 -x911_bit0 -x912_bit0 -x913_bit0 -x914_bit0 -x915_bit0 -x916_bit0 -x917_bit0 -x918_bit0 -x919_bit0 -x920_bit0 -x921_bit0 -x922_bit0 -x923_bit0 -x924_bit0 -x925_bit0 x926_bit0 -x927_bit0 -x928_bit0 -x929_bit0 -x930_bit0 -x931_bit0 -x932_bit0 -x933_bit0 -x934_bit0 -x935_bit0 -x936_bit0 -x937_bit0 -x938_bit0 -x939_bit0 -x940_bit0 -x941_bit0 -x942_bit0 -x943_bit0 -x944_bit0 -x945_bit0 -x946_bit0 -x947_bit0 -x948_bit0 -x949_bit0 -x950_bit0 -x951_bit0 -x952_bit0 -x953_bit0 -x954_bit0 -x955_bit0 -x956_bit0 -x957_bit0 -x958_bit0 -x959_bit0 -x960_bit0 -x961_bit0 -x962_bit0 -x963_bit0 -x964_bit0 -x965_bit0 -x966_bit0 -x967_bit0 -x968_bit0 -x969_bit0 -x970_bit0 -x971_bit0 -x972_bit0 -x973_bit0 -x974_bit0 -x975_bit0 x976_bit0 -x977_bit0 -x978_bit0 -x979_bit0 -x980_bit0 -x981_bit0 -x982_bit0 -x983_bit0 -x984_bit0 -x985_bit0 -x986_bit0 -x987_bit0 -x988_bit0 -x989_bit0 -x990_bit0 -x991_bit0 -x992_bit0 -x993_bit0 -x994_bit0 -x995_bit0 -x996_bit0 -x997_bit0 -x998_bit0 -x999_bit0 -x1000_bit0 -x1001_bit0 -x1002_bit0 -x1003_bit0 x1004_bit0 -x1005_bit0 -x1006_bit0 -x1007_bit0 -x1008_bit0 -x1009_bit0 -x1010_bit0 -x1011_bit0 -x1012_bit0 -x1013_bit0 -x1014_bit0 -x1015_bit0 -x1016_bit0 -x1017_bit0 -x1018_bit0 -x1019_bit0 -x1020_bit0 -x1021_bit0 -x1022_bit0 -x1023_bit0 -x1024_bit0 -x1025_bit0 -x1026_bit0 -x1027_bit0 -x1028_bit0 -x1029_bit0 -x1030_bit0 -x1031_bit0 -x1032_bit0 -x1033_bit0 -x1034_bit0 -x1035_bit0 -x1036_bit0 -x1037_bit0 -x1038_bit0 -x1039_bit0 -x1040_bit0 -x1041_bit0 -x1042_bit0 -x1043_bit0 -x1044_bit0 -x1045_bit0 -x1046_bit0 -x1047_bit0 -x1048_bit0 -x1049_bit0 -x1050_bit0 -x1051_bit0 -x1052_bit0 -x1053_bit0 -x1054_bit0 -x1055_bit0 -x1056_bit0 -x1057_bit0 -x1058_bit0 -x1059_bit0 -x1060_bit0 -x1061_bit0 -x1062_bit0 -x1063_bit0 -x1064_bit0 -x1065_bit0 -x1066_bit0 -x1067_bit0 -x1068_bit0 -x1069_bit0 -x1070_bit0 -x1071_bit0 -x1072_bit0 x1073_bit0 -x1074_bit0 -x1075_bit0 -x1076_bit0 -x1077_bit0 -x1078_bit0 -x1079_bit0 -x1080_bit0 -x1081_bit0 -x1082_bit0 -x1083_bit0 -x1084_bit0 -x1085_bit0 -x1086_bit0 -x1087_bit0 -x1088_bit0 -x1089_bit0 -x1090_bit0 -x1091_bit0 -x1092_bit0 -x1093_bit0 -x1094_bit0 -x1095_bit0 x1096_bit0 -x1097_bit0 -x1098_bit0 -x1099_bit0 -x1100_bit0 -x1101_bit0 -x1102_bit0 -x1103_bit0 -x1104_bit0 -x1105_bit0 -x1106_bit0 -x1107_bit0 -x1108_bit0 -x1109_bit0 -x1110_bit0 -x1111_bit0 -x1112_bit0 -x1113_bit0 -x1114_bit0 -x1115_bit0 -x1116_bit0 -x1117_bit0 -x1118_bit0 -x1119_bit0 -x1120_bit0 -x1121_bit0 -x1122_bit0 -x1123_bit0 -x1124_bit0 -x1125_bit0 -x1126_bit0 -x1127_bit0 -x1128_bit0 -x1129_bit0 -x1130_bit0 -x1131_bit0 -x1132_bit0 -x1133_bit0 -x1134_bit0 -x1135_bit0 -x1136_bit0 -x1137_bit0 -x1138_bit0 -x1139_bit0 -x1140_bit0 -x1141_bit0 -x1142_bit0 -x1143_bit0 -x1144_bit0 -x1145_bit0 -x1146_bit0 -x1147_bit0 -x1148_bit0 -x1149_bit0 -x1150_bit0 -x1151_bit0 -x1152_bit0 -x1153_bit0 x1154_bit0 -x1155_bit0 -x1156_bit0 -x1157_bit0 -x1158_bit0 -x1159_bit0 -x1160_bit0 -x1161_bit0 -x1162_bit0 -x1163_bit0 -x1164_bit0 -x1165_bit0 -x1166_bit0 -x1167_bit0 -x1168_bit0 -x1169_bit0 -x1170_bit0 -x1171_bit0 -x1172_bit0 -x1173_bit0 -x1174_bit0 -x1175_bit0 -x1176_bit0 -x1177_bit0 -x1178_bit0 -x1179_bit0 -x1180_bit0 -x1181_bit0 -x1182_bit0 -x1183_bit0 -x1184_bit0 -x1185_bit0 -x1186_bit0 -x1187_bit0 -x1188_bit0 -x1189_bit0 -x1190_bit0 -x1191_bit0 -x1192_bit0 -x1193_bit0 -x1194_bit0 -x1195_bit0 -x1196_bit0 -x1197_bit0 -x1198_bit0 -x1199_bit0 -x1200_bit0 -x1201_bit0 -x1202_bit0 -x1203_bit0 -x1204_bit0 -x1205_bit0 -x1206_bit0 -x1207_bit0 -x1208_bit0 -x1209_bit0 -x1210_bit0 -x1211_bit0 x1212_bit0 -x1213_bit0 -x1214_bit0 -x1215_bit0 -x1216_bit0 -x1217_bit0 -x1218_bit0 -x1219_bit0 -x1220_bit0 -x1221_bit0 -x1222_bit0 -x1223_bit0 -x1224_bit0 -x1225_bit0 -x1226_bit0 -x1227_bit0 -x1228_bit0 -x1229_bit0 -x1230_bit0 -x1231_bit0 -x1232_bit0 x1233_bit0 -x1234_bit0 -x1235_bit0 -x1236_bit0 -x1237_bit0 -x1238_bit0 -x1239_bit0 -x1240_bit0 -x1241_bit0 -x1242_bit0 -x1243_bit0 -x1244_bit0 -x1245_bit0 -x1246_bit0 -x1247_bit0 -x1248_bit0 -x1249_bit0 -x1250_bit0 -x1251_bit0 -x1252_bit0 -x1253_bit0 -x1254_bit0 -x1255_bit0 -x1256_bit0 -x1257_bit0 -x1258_bit0 -x1259_bit0 -x1260_bit0 -x1261_bit0 -x1262_bit0 -x1263_bit0 -x1264_bit0 -x1265_bit0 -x1266_bit0 -x1267_bit0 x1268_bit0 -x1269_bit0 -x1270_bit0 -x1271_bit0 -x1272_bit0 -x1273_bit0 -x1274_bit0 -x1275_bit0 -x1276_bit0 -x1277_bit0 -x1278_bit0 -x1279_bit0 -x1280_bit0 -x1281_bit0 -x1282_bit0 -x1283_bit0 -x1284_bit0 -x1285_bit0 -x1286_bit0 -x1287_bit0 -x1288_bit0 -x1289_bit0 -x1290_bit0 -x1291_bit0 -x1292_bit0 -x1293_bit0 -x1294_bit0 -x1295_bit0 -x1296_bit0 -x1297_bit0 -x1298_bit0 -x1299_bit0 -x1300_bit0 -x1301_bit0 -x1302_bit0 -x1303_bit0 -x1304_bit0 -x1305_bit0 -x1306_bit0 -x1307_bit0 -x1308_bit0 -x1309_bit0 -x1310_bit0 -x1311_bit0 -x1312_bit0 -x1313_bit0 -x1314_bit0 -x1315_bit0 -x1316_bit0 -x1317_bit0 -x1318_bit0 -x1319_bit0 -x1320_bit0 -x1321_bit0 -x1322_bit0 -x1323_bit0 -x1324_bit0 -x1325_bit0 -x1326_bit0 -x1327_bit0 -x1328_bit0 -x1329_bit0 x1330_bit0 -x1331_bit0 -x1332_bit0 -x1333_bit0 -x1334_bit0 -x1335_bit0 -x1336_bit0 -x1337_bit0 -x1338_bit0 -x1339_bit0 -x1340_bit0 -x1341_bit0 -x1342_bit0 -x1343_bit0 -x1344_bit0 -x1345_bit0 -x1346_bit0 -x1347_bit0 -x1348_bit0 -x1349_bit0 -x1350_bit0 -x1351_bit0 -x1352_bit0 -x1353_bit0 -x1354_bit0 -x1355_bit0 -x1356_bit0 -x1357_bit0 -x1358_bit0 -x1359_bit0 -x1360_bit0 -x1361_bit0 x1362_bit0 -x1363_bit0 -x1364_bit0 -x1365_bit0 -x1366_bit0 -x1367_bit0 -x1368_bit0 -x1369_bit0 -x1370_bit0 -x1371_bit0 -x1372_bit0 -x1373_bit0 -x1374_bit0 -x1375_bit0 -x1376_bit0 -x1377_bit0 -x1378_bit0 -x1379_bit0 -x1380_bit0 -x1381_bit0 -x1382_bit0 -x1383_bit0 -x1384_bit0 -x1385_bit0 -x1386_bit0 -x1387_bit0 -x1388_bit0 -x1389_bit0 -x1390_bit0 -x1391_bit0 -x1392_bit0 -x1393_bit0 -x1394_bit0 -x1395_bit0 -x1396_bit0 -x1397_bit0 -x1398_bit0 -x1399_bit0 -x1400_bit0 -x1401_bit0 -x1402_bit0 -x1403_bit0 -x1404_bit0 -x1405_bit0 -x1406_bit0 -x1407_bit0 -x1408_bit0 -x1409_bit0 -x1410_bit0 -x1411_bit0 -x1412_bit0 -x1413_bit0 -x1414_bit0 -x1415_bit0 -x1416_bit0 -x1417_bit0 -x1418_bit0 -x1419_bit0 -x1420_bit0 -x1421_bit0 -x1422_bit0 -x1423_bit0 -x1424_bit0 -x1425_bit0 -x1426_bit0 -x1427_bit0 -x1428_bit0 -x1429_bit0 -x1430_bit0 -x1431_bit0 -x1432_bit0 -x1433_bit0 -x1434_bit0 -x1435_bit0 -x1436_bit0 -x1437_bit0 x1438_bit0 -x1439_bit0 -x1440_bit0 -x1441_bit0 x1442_bit0 -x1443_bit0 -x1444_bit0 -x1445_bit0 -x1446_bit0 -x1447_bit0 -x1448_bit0 -x1449_bit0 -x1450_bit0 -x1451_bit0 -x1452_bit0 -x1453_bit0 -x1454_bit0 -x1455_bit0 -x1456_bit0 -x1457_bit0 -x1458_bit0 -x1459_bit0 -x1460_bit0 -x1461_bit0 -x1462_bit0 -x1463_bit0 -x1464_bit0 -x1465_bit0 -x1466_bit0 -x1467_bit0 -x1468_bit0 -x1469_bit0 -x1470_bit0 -x1471_bit0 -x1472_bit0 -x1473_bit0 -x1474_bit0 -x1475_bit0 -x1476_bit0 -x1477_bit0 -x1478_bit0 -x1479_bit0 -x1480_bit0 -x1481_bit0 -x1482_bit0 -x1483_bit0 -x1484_bit0 -x1485_bit0 -x1486_bit0 -x1487_bit0 -x1488_bit0 -x1489_bit0 -x1490_bit0 -x1491_bit0 -x1492_bit0 -x1493_bit0 -x1494_bit0 -x1495_bit0 -x1496_bit0 -x1497_bit0 -x1498_bit0 -x1499_bit0 -x1500_bit0 -x1501_bit0 -x1502_bit0 -x1503_bit0 -x1504_bit0 -x1505_bit0 -x1506_bit0 -x1507_bit0 -x1508_bit0 -x1509_bit0 -x1510_bit0 -x1511_bit0 -x1512_bit0 -x1513_bit0 -x1514_bit0 -x1515_bit0 -x1516_bit0 -x1517_bit0 -x1518_bit0 -x1519_bit0 -x1520_bit0 x1521_bit0 -x1522_bit0 -x1523_bit0 -x1524_bit0 -x1525_bit0 -x1526_bit0 -x1527_bit0 -x1528_bit0 -x1529_bit0 -x1530_bit0 -x1531_bit0 -x1532_bit0 -x1533_bit0 -x1534_bit0 -x1535_bit0 -x1536_bit0 -x1537_bit0 -x1538_bit0 -x1539_bit0 x1540_bit0 -x1541_bit0 -x1542_bit0 -x1543_bit0 -x1544_bit0 -x1545_bit0 -x1546_bit0 -x1547_bit0 -x1548_bit0 -x1549_bit0 -x1550_bit0 -x1551_bit0 -x1552_bit0 -x1553_bit0 -x1554_bit0 -x1555_bit0 -x1556_bit0 -x1557_bit0 -x1558_bit0 -x1559_bit0 -x1560_bit0 -x1561_bit0 -x1562_bit0 -x1563_bit0 -x1564_bit0 -x1565_bit0 -x1566_bit0 -x1567_bit0 -x1568_bit0 -x1569_bit0 -x1570_bit0 -x1571_bit0 -x1572_bit0 -x1573_bit0 -x1574_bit0 -x1575_bit0 -x1576_bit0 -x1577_bit0 -x1578_bit0 -x1579_bit0 -x1580_bit0 -x1581_bit0 -x1582_bit0 -x1583_bit0 -x1584_bit0 -x1585_bit0 -x1586_bit0 -x1587_bit0 -x1588_bit0 -x1589_bit0 -x1590_bit0 -x1591_bit0 -x1592_bit0 -x1593_bit0 -x1594_bit0 -x1595_bit0 -x1596_bit0 -x1597_bit0 -x1598_bit0 -x1599_bit0 -x1600_bit0 -x1601_bit0 -x1602_bit0 -x1603_bit0 -x1604_bit0 -x1605_bit0 -x1606_bit0 -x1607_bit0 -x1608_bit0 -x1609_bit0 -x1610_bit0 -x1611_bit0 -x1612_bit0 -x1613_bit0 -x1614_bit0 x1615_bit0 -x1616_bit0 -x1617_bit0 -x1618_bit0 -x1619_bit0 -x1620_bit0 -x1621_bit0 -x1622_bit0 -x1623_bit0 -x1624_bit0 -x1625_bit0 -x1626_bit0 x1627_bit0 -x1628_bit0 -x1629_bit0 -x1630_bit0 -x1631_bit0 -x1632_bit0 -x1633_bit0 -x1634_bit0 -x1635_bit0 -x1636_bit0 -x1637_bit0 -x1638_bit0 -x1639_bit0 -x1640_bit0 -x1641_bit0 -x1642_bit0 -x1643_bit0 -x1644_bit0 -x1645_bit0 -x1646_bit0 -x1647_bit0 -x1648_bit0 -x1649_bit0 -x1650_bit0 -x1651_bit0 -x1652_bit0 -x1653_bit0 -x1654_bit0 -x1655_bit0 -x1656_bit0 -x1657_bit0 -x1658_bit0 -x1659_bit0 -x1660_bit0 -x1661_bit0 -x1662_bit0 -x1663_bit0 -x1664_bit0 -x1665_bit0 -x1666_bit0 -x1667_bit0 -x1668_bit0 -x1669_bit0 -x1670_bit0 -x1671_bit0 -x1672_bit0 -x1673_bit0 -x1674_bit0 -x1675_bit0 -x1676_bit0 -x1677_bit0 -x1678_bit0 -x1679_bit0 -x1680_bit0 -x1681_bit0 -x1682_bit0 -x1683_bit0 -x1684_bit0 -x1685_bit0 -x1686_bit0 -x1687_bit0 -x1688_bit0 -x1689_bit0 -x1690_bit0 -x1691_bit0 -x1692_bit0 -x1693_bit0 -x1694_bit0 x1695_bit0 -x1696_bit0 -x1697_bit0 -x1698_bit0 -x1699_bit0 -x1700_bit0 -x1701_bit0 -x1702_bit0 -x1703_bit0 -x1704_bit0 -x1705_bit0 -x1706_bit0 -x1707_bit0 -x1708_bit0 -x1709_bit0 -x1710_bit0 -x1711_bit0 -x1712_bit0 -x1713_bit0 -x1714_bit0 -x1715_bit0 -x1716_bit0 -x1717_bit0 -x1718_bit0 -x1719_bit0 -x1720_bit0 -x1721_bit0 -x1722_bit0 -x1723_bit0 -x1724_bit0 -x1725_bit0 -x1726_bit0 -x1727_bit0 -x1728_bit0 -x1729_bit0 -x1730_bit0 x1731_bit0 -x1732_bit0 -x1733_bit0 -x1734_bit0 -x1735_bit0 -x1736_bit0 -x1737_bit0 -x1738_bit0 -x1739_bit0 -x1740_bit0 -x1741_bit0 -x1742_bit0 -x1743_bit0 -x1744_bit0 -x1745_bit0 -x1746_bit0 -x1747_bit0 -x1748_bit0 -x1749_bit0 -x1750_bit0 -x1751_bit0 -x1752_bit0 -x1753_bit0 -x1754_bit0 -x1755_bit0 -x1756_bit0 -x1757_bit0 -x1758_bit0 -x1759_bit0 -x1760_bit0 -x1761_bit0 -x1762_bit0 -x1763_bit0 -x1764_bit0 -x1765_bit0 -x1766_bit0 -x1767_bit0 -x1768_bit0 -x1769_bit0 -x1770_bit0 -x1771_bit0 -x1772_bit0 -x1773_bit0 -x1774_bit0 -x1775_bit0 -x1776_bit0 -x1777_bit0 -x1778_bit0 x1779_bit0 -x1780_bit0 -x1781_bit0 -x1782_bit0 -x1783_bit0 -x1784_bit0 -x1785_bit0 -x1786_bit0 -x1787_bit0 -x1788_bit0 -x1789_bit0 -x1790_bit0 -x1791_bit0 -x1792_bit0 -x1793_bit0 -x1794_bit0 -x1795_bit0 -x1796_bit0 -x1797_bit0 -x1798_bit0 -x1799_bit0 -x1800_bit0 -x1801_bit0 -x1802_bit0 -x1803_bit0 -x1804_bit0 -x1805_bit0 -x1806_bit0 -x1807_bit0 -x1808_bit0 x1809_bit0 -x1810_bit0 -x1811_bit0 -x1812_bit0 -x1813_bit0 -x1814_bit0 -x1815_bit0 -x1816_bit0 -x1817_bit0 -x1818_bit0 -x1819_bit0 -x1820_bit0 -x1821_bit0 -x1822_bit0 -x1823_bit0 -x1824_bit0 -x1825_bit0 -x1826_bit0 -x1827_bit0 -x1828_bit0 -x1829_bit0 -x1830_bit0 -x1831_bit0 -x1832_bit0 -x1833_bit0 -x1834_bit0 -x1835_bit0 -x1836_bit0 -x1837_bit0 -x1838_bit0 -x1839_bit0 -x1840_bit0 -x1841_bit0 -x1842_bit0 -x1843_bit0 -x1844_bit0 -x1845_bit0 -x1846_bit0 -x1847_bit0 -x1848_bit0 -x1849_bit0 -x1850_bit0 -x1851_bit0 -x1852_bit0 -x1853_bit0 -x1854_bit0 -x1855_bit0 -x1856_bit0 -x1857_bit0 -x1858_bit0 -x1859_bit0 -x1860_bit0 -x1861_bit0 -x1862_bit0 -x1863_bit0 -x1864_bit0 -x1865_bit0 -x1866_bit0 -x1867_bit0 -x1868_bit0 -x1869_bit0 -x1870_bit0 -x1871_bit0 -x1872_bit0 -x1873_bit0 -x1874_bit0 -x1875_bit0 -x1876_bit0 -x1877_bit0 -x1878_bit0 x1879_bit0 -x1880_bit0 -x1881_bit0 -x1882_bit0 -x1883_bit0 -x1884_bit0 -x1885_bit0 -x1886_bit0 -x1887_bit0 -x1888_bit0 -x1889_bit0 -x1890_bit0 -x1891_bit0 -x1892_bit0 -x1893_bit0 -x1894_bit0 -x1895_bit0 -x1896_bit0 -x1897_bit0 -x1898_bit0 -x1899_bit0 -x1900_bit0 -x1901_bit0 -x1902_bit0 -x1903_bit0 -x1904_bit0 -x1905_bit0 -x1906_bit0 -x1907_bit0 -x1908_bit0 -x1909_bit0 -x1910_bit0 -x1911_bit0 -x1912_bit0 -x1913_bit0 -x1914_bit0 -x1915_bit0 -x1916_bit0 -x1917_bit0 -x1918_bit0 -x1919_bit0 -x1920_bit0 -x1921_bit0 -x1922_bit0 -x1923_bit0 -x1924_bit0 -x1925_bit0 -x1926_bit0 -x1927_bit0 -x1928_bit0 -x1929_bit0 -x1930_bit0 -x1931_bit0 -x1932_bit0 -x1933_bit0 x1934_bit0 -x1935_bit0 -x1936_bit0 -x1937_bit0 -x1938_bit0 x1939_bit0 -x1940_bit0 -x1941_bit0 -x1942_bit0 -x1943_bit0 -x1944_bit0 -x1945_bit0 -x1946_bit0 -x1947_bit0 -x1948_bit0 -x1949_bit0 -x1950_bit0 -x1951_bit0 -x1952_bit0 -x1953_bit0 -x1954_bit0 -x1955_bit0 -x1956_bit0 -x1957_bit0 -x1958_bit0 -x1959_bit0 -x1960_bit0 -x1961_bit0 -x1962_bit0 -x1963_bit0 -x1964_bit0 -x1965_bit0 -x1966_bit0 -x1967_bit0 -x1968_bit0 -x1969_bit0 -x1970_bit0 -x1971_bit0 -x1972_bit0 -x1973_bit0 -x1974_bit0 -x1975_bit0 -x1976_bit0 -x1977_bit0 -x1978_bit0 -x1979_bit0 -x1980_bit0 -x1981_bit0 -x1982_bit0 -x1983_bit0 -x1984_bit0 -x1985_bit0 -x1986_bit0 -x1987_bit0 -x1988_bit0 -x1989_bit0 -x1990_bit0 -x1991_bit0 -x1992_bit0 -x1993_bit0 -x1994_bit0 -x1995_bit0 -x1996_bit0 x#### 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.80 0.91 0.90 2/55 3470
Raw data (stat): 3470 (runsolver) R 3469 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546697976 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0009 s]
Raw data (loadavg): 0.83 0.91 0.90 2/55 3470
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 8730 0 0 0 978 21 0 0 25 0 1 0 546697976 33546240 7302 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8190 7302 603 41 0 8149 0
vsize: 32760
[startup+20.0013 s]
Raw data (loadavg): 0.85 0.91 0.90 2/55 3470
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 9102 0 0 0 1976 22 0 0 25 0 1 0 546697976 35024896 7674 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8551 7674 603 41 0 8510 0
vsize: 34204
[startup+30.0025 s]
Raw data (loadavg): 0.88 0.91 0.90 2/55 3470
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 9523 0 0 0 2975 24 0 0 25 0 1 0 546697976 36765696 8095 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8976 8095 603 41 0 8935 0
vsize: 35904
[startup+40.0033 s]
Raw data (loadavg): 0.89 0.92 0.90 2/55 3470
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 9972 0 0 0 3973 26 0 0 25 0 1 0 546697976 38662144 8544 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9439 8544 603 41 0 9398 0
vsize: 37756
[startup+50.0047 s]
Raw data (loadavg): 0.91 0.92 0.90 2/55 3470
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 10505 0 0 0 4971 28 0 0 25 0 1 0 546697976 40304640 8964 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9840 8964 603 41 0 9799 0
vsize: 39360
[startup+60.0045 s]
Raw data (loadavg): 0.92 0.92 0.90 3/55 3470
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 10844 0 0 0 5970 29 0 0 25 0 1 0 546697976 41787392 9303 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10202 9303 603 41 0 10161 0
vsize: 40808
[startup+70.0047 s]
Raw data (loadavg): 0.93 0.92 0.90 2/55 3472
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 11295 0 0 0 6969 30 0 0 25 0 1 0 546697976 43532288 9754 4294967295 134512640 134672761 3221224624 3221223808 134559383 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10628 9754 603 41 0 10587 0
vsize: 42512
[startup+80.0054 s]
Raw data (loadavg): 1.02 0.94 0.91 2/59 3476
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 11747 0 0 0 7964 35 0 0 25 0 1 0 546697976 45522944 10206 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11114 10206 603 41 0 11073 0
vsize: 44456
[startup+90.0051 s]
Raw data (loadavg): 1.02 0.94 0.91 2/55 3525
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 12156 0 0 0 8963 36 0 0 25 0 1 0 546697976 47144960 10615 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11510 10615 603 41 0 11469 0
vsize: 46040
[startup+100.006 s]
Raw data (loadavg): 1.02 0.94 0.91 2/55 3525
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 12607 0 0 0 9961 38 0 0 25 0 1 0 546697976 49025024 11066 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 11066 603 41 0 11928 0
vsize: 47876
[startup+110.007 s]
Raw data (loadavg): 1.01 0.94 0.91 2/55 3525
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 13046 0 0 0 10959 40 0 0 25 0 1 0 546697976 50769920 11505 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12395 11505 603 41 0 12354 0
vsize: 49580
[startup+120.006 s]
Raw data (loadavg): 1.01 0.95 0.91 2/55 3525
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 13432 0 0 0 11957 42 0 0 25 0 1 0 546697976 52387840 11891 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12790 11891 603 41 0 12749 0
vsize: 51160
[startup+130.007 s]
Raw data (loadavg): 1.01 0.95 0.91 2/55 3525
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 13813 0 0 0 12956 43 0 0 25 0 1 0 546697976 53870592 12272 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13152 12272 603 41 0 13111 0
vsize: 52608
[startup+140.007 s]
Raw data (loadavg): 1.01 0.95 0.91 2/55 3525
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 14224 0 0 0 13955 45 0 0 25 0 1 0 546697976 55144448 12573 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13463 12573 603 41 0 13422 0
vsize: 53852
[startup+150.008 s]
Raw data (loadavg): 1.01 0.95 0.91 2/55 3525
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 14575 0 0 0 14953 47 0 0 25 0 1 0 546697976 56631296 12924 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13826 12924 603 41 0 13785 0
vsize: 55304
[startup+160.009 s]
Raw data (loadavg): 1.00 0.95 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 14940 0 0 0 15952 48 0 0 25 0 1 0 546697976 58114048 13289 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14188 13289 603 41 0 14147 0
vsize: 56752
[startup+170.008 s]
Raw data (loadavg): 1.00 0.95 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 15326 0 0 0 16951 49 0 0 25 0 1 0 546697976 59596800 13675 4294967295 134512640 134672761 3221224624 3221223808 134558937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14550 13675 603 41 0 14509 0
vsize: 58200
[startup+180.008 s]
Raw data (loadavg): 1.00 0.95 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 15763 0 0 0 17950 51 0 0 25 0 1 0 546697976 61607936 14112 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15041 14112 603 41 0 15000 0
vsize: 60164
[startup+190.009 s]
Raw data (loadavg): 1.00 0.95 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16152 0 0 0 18948 53 0 0 25 0 1 0 546697976 63217664 14501 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15434 14501 603 41 0 15393 0
vsize: 61736
[startup+200.01 s]
Raw data (loadavg): 1.00 0.95 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 19947 54 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223924 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+210.01 s]
Raw data (loadavg): 1.00 0.95 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 20946 55 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+220.01 s]
Raw data (loadavg): 1.00 0.95 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 21946 55 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+230.011 s]
Raw data (loadavg): 1.00 0.96 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 22946 56 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+240.011 s]
Raw data (loadavg): 1.00 0.96 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 23946 56 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+250.012 s]
Raw data (loadavg): 1.00 0.96 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 24946 56 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+260.013 s]
Raw data (loadavg): 1.00 0.96 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 25946 57 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+270.013 s]
Raw data (loadavg): 1.00 0.96 0.91 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 26946 57 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+280.013 s]
Raw data (loadavg): 1.07 0.98 0.92 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 27946 57 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+290.014 s]
Raw data (loadavg): 1.06 0.98 0.92 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 28946 57 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+300.015 s]
Raw data (loadavg): 1.05 0.98 0.92 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 29947 57 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+310.016 s]
Raw data (loadavg): 1.04 0.98 0.92 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 30947 57 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+320.015 s]
Raw data (loadavg): 1.04 0.98 0.92 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16654 0 0 0 31947 57 0 0 25 0 1 0 546697976 64684032 14891 4294967295 134512640 134672761 3221224624 3221223808 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+330.017 s]
Raw data (loadavg): 1.03 0.98 0.92 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 16818 0 0 0 32947 57 0 0 25 0 1 0 546697976 65359872 15055 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15957 15055 603 41 0 15916 0
vsize: 63828
[startup+340.017 s]
Raw data (loadavg): 1.02 0.98 0.92 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 17214 0 0 0 33946 58 0 0 25 0 1 0 546697976 66973696 15451 4294967295 134512640 134672761 3221224624 3221223792 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16351 15451 603 41 0 16310 0
vsize: 65404
[startup+350.018 s]
Raw data (loadavg): 1.02 0.98 0.92 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 17618 0 0 0 34945 59 0 0 25 0 1 0 546697976 68726784 15855 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16779 15855 603 41 0 16738 0
vsize: 67116
[startup+360.019 s]
Raw data (loadavg): 1.02 0.98 0.92 2/55 3527
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 17998 0 0 0 35945 60 0 0 25 0 1 0 546697976 70209536 16235 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17141 16235 603 41 0 17100 0
vsize: 68564
[startup+370.019 s]
Raw data (loadavg): 1.01 0.98 0.92 2/55 3529
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 18362 0 0 0 36944 61 0 0 25 0 1 0 546697976 71684096 16599 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17501 16599 603 41 0 17460 0
vsize: 70004
[startup+380.019 s]
Raw data (loadavg): 1.01 0.98 0.92 2/55 3529
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 18748 0 0 0 37942 63 0 0 25 0 1 0 546697976 73293824 16985 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17894 16985 603 41 0 17853 0
vsize: 71576
[startup+390.019 s]
Raw data (loadavg): 1.01 0.98 0.92 2/55 3529
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 19145 0 0 0 38941 64 0 0 25 0 1 0 546697976 74911744 17382 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18289 17382 603 41 0 18248 0
vsize: 73156
[startup+400.021 s]
Raw data (loadavg): 1.01 0.98 0.92 2/55 3529
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 19574 0 0 0 39941 64 0 0 25 0 1 0 546697976 76664832 17811 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18717 17811 603 41 0 18676 0
vsize: 74868
[startup+410.021 s]
Raw data (loadavg): 1.01 0.98 0.92 2/55 3529
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 20033 0 0 0 40940 65 0 0 25 0 1 0 546697976 78557184 18270 4294967295 134512640 134672761 3221224624 3221223728 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19179 18270 603 41 0 19138 0
vsize: 76716
[startup+420.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3529
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 20472 0 0 0 41939 67 0 0 25 0 1 0 546697976 80289792 18709 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19602 18709 603 41 0 19561 0
vsize: 78408
[startup+430.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3529
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 20921 0 0 0 42938 68 0 0 25 0 1 0 546697976 82161664 19158 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20059 19158 603 41 0 20018 0
vsize: 80236
[startup+440.021 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3529
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 21331 0 0 0 43937 69 0 0 25 0 1 0 546697976 83922944 19568 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20489 19568 603 41 0 20448 0
vsize: 81956
[startup+450.022 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3529
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 21625 0 0 0 44936 70 0 0 25 0 1 0 546697976 85000192 19862 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20752 19862 603 41 0 20711 0
vsize: 83008
[startup+460.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 21961 0 0 0 45936 71 0 0 25 0 1 0 546697976 86474752 20198 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21112 20198 603 41 0 21071 0
vsize: 84448
[startup+470.022 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 22303 0 0 0 46935 72 0 0 25 0 1 0 546697976 87822336 20540 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21441 20540 603 41 0 21400 0
vsize: 85764
[startup+480.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 22645 0 0 0 47933 74 0 0 25 0 1 0 546697976 89276416 20882 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21796 20882 603 41 0 21755 0
vsize: 87184
[startup+490.023 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 22941 0 0 0 48933 74 0 0 25 0 1 0 546697976 90472448 21178 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22088 21178 603 41 0 22047 0
vsize: 88352
[startup+500.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 23298 0 0 0 49932 75 0 0 25 0 1 0 546697976 91820032 21535 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22417 21535 603 41 0 22376 0
vsize: 89668
[startup+510.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 23668 0 0 0 50931 77 0 0 25 0 1 0 546697976 93425664 21905 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22809 21905 603 41 0 22768 0
vsize: 91236
[startup+520.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 24025 0 0 0 51930 77 0 0 25 0 1 0 546697976 94904320 22262 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23170 22262 603 41 0 23129 0
vsize: 92680
[startup+530.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 24362 0 0 0 52930 78 0 0 25 0 1 0 546697976 96247808 22599 4294967295 134512640 134672761 3221224624 3221223728 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23498 22599 603 41 0 23457 0
vsize: 93992
[startup+540.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 24689 0 0 0 53929 79 0 0 25 0 1 0 546697976 97595392 22926 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23827 22926 603 41 0 23786 0
vsize: 95308
[startup+550.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 25023 0 0 0 54928 80 0 0 25 0 1 0 546697976 98934784 23260 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24154 23260 603 41 0 24113 0
vsize: 96616
[startup+560.024 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 25339 0 0 0 55928 81 0 0 25 0 1 0 546697976 100274176 23576 4294967295 134512640 134672761 3221224624 3221223760 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24481 23576 603 41 0 24440 0
vsize: 97924
[startup+570.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 25689 0 0 0 56927 82 0 0 25 0 1 0 546697976 101613568 23926 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24808 23926 603 41 0 24767 0
vsize: 99232
[startup+580.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 26036 0 0 0 57926 83 0 0 25 0 1 0 546697976 103350272 24273 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25232 24273 603 41 0 25191 0
vsize: 100928
[startup+590.025 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 26349 0 0 0 58925 84 0 0 25 0 1 0 546697976 104558592 24586 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25527 24586 603 41 0 25486 0
vsize: 102108
[startup+600.026 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 26682 0 0 0 59925 85 0 0 25 0 1 0 546697976 105893888 24919 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25853 24919 603 41 0 25812 0
vsize: 103412
[startup+610.027 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 26995 0 0 0 60924 85 0 0 25 0 1 0 546697976 107233280 25232 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26180 25232 603 41 0 26139 0
vsize: 104720
[startup+620.027 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 27367 0 0 0 61924 86 0 0 25 0 1 0 546697976 108703744 25604 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26539 25604 603 41 0 26498 0
vsize: 106156
[startup+630.028 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 27751 0 0 0 62923 87 0 0 25 0 1 0 546697976 110301184 25988 4294967295 134512640 134672761 3221224624 3221223824 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26929 25988 603 41 0 26888 0
vsize: 107716
[startup+640.029 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 28079 0 0 0 63922 88 0 0 25 0 1 0 546697976 111640576 26316 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27256 26316 603 41 0 27215 0
vsize: 109024
[startup+650.029 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 28463 0 0 0 64921 89 0 0 25 0 1 0 546697976 113242112 26700 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27647 26700 603 41 0 27606 0
vsize: 110588
[startup+660.029 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3531
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 28857 0 0 0 65920 90 0 0 25 0 1 0 546697976 114835456 27094 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28036 27094 603 41 0 27995 0
vsize: 112144
[startup+670.029 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 29195 0 0 0 66920 91 0 0 25 0 1 0 546697976 116178944 27432 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28364 27432 603 41 0 28323 0
vsize: 113456
[startup+680.029 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 29554 0 0 0 67919 92 0 0 25 0 1 0 546697976 117645312 27791 4294967295 134512640 134672761 3221224624 3221223808 134559188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28722 27791 603 41 0 28681 0
vsize: 114888
[startup+690.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 29899 0 0 0 68919 92 0 0 25 0 1 0 546697976 119095296 28136 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29076 28136 603 41 0 29035 0
vsize: 116304
[startup+700.03 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30303 0 0 0 69918 93 0 0 25 0 1 0 546697976 120700928 28540 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29468 28540 603 41 0 29427 0
vsize: 117872
[startup+710.031 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 70917 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+720.031 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 71917 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+730.031 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 72917 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+740.031 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 73917 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+750.033 s]
Raw data (loadavg): 1.00 0.98 0.92 3/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 74917 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+760.033 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 75917 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+770.033 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 76918 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+780.034 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 77918 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+790.033 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 78918 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+800.034 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 79918 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+810.035 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 80918 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+820.036 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 81919 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+830.037 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 82919 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+840.036 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 83919 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+850.037 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 84919 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+860.038 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 85919 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+870.038 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 86919 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+880.039 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 87920 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134559985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+890.038 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 88920 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+900.039 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 89920 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+910.04 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 90920 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+920.04 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 91920 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+930.041 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 92921 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+940.041 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 93921 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+950.041 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 94921 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+960.042 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3533
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 95921 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+970.043 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 96921 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+980.044 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 97922 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+990.044 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 98922 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 99922 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 100922 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 101922 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 102923 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 103923 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 104923 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 105923 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 106923 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 107923 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 108924 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 109924 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 110924 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 111924 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 112924 95 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 113924 96 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 30709 0 0 0 114924 96 0 0 25 0 1 0 546697976 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 31016 0 0 0 115924 96 0 0 25 0 1 0 546697976 123224064 29143 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30084 29143 603 41 0 30043 0
vsize: 120336
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 31321 0 0 0 116922 97 0 0 25 0 1 0 546697976 124424192 29448 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30377 29448 603 41 0 30336 0
vsize: 121508
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 31702 0 0 0 117921 98 0 0 25 0 1 0 546697976 126025728 29829 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30768 29829 603 41 0 30727 0
vsize: 123072
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 32048 0 0 0 118921 99 0 0 25 0 1 0 546697976 127369216 30175 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31096 30175 603 41 0 31055 0
vsize: 124384
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.98 0.92 2/55 3535
Raw data (stat): 3470 (minisat+) R 3469 22929 22928 0 -1 0 32364 0 0 0 119920 99 0 0 25 0 1 0 546697976 128704512 30491 4294967295 134512640 134672761 3221224624 3221223728 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31422 30491 603 41 0 31381 0
vsize: 125688
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.98 0.92 1/55 3535
Raw data (stat): 3470 (minisat+) Z 3469 22929 22928 0 -1 12 32367 0 0 0 119921 105 0 0 25 0 1 0 546697976 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.11
CPU time (s): 1200.27
CPU user time (s): 1199.21
CPU system time (s): 1.05484
CPU usage (%): 100.013
Max. virtual memory (Kb): 125688
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####