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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-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	924
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.71
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 21953

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        720884 kB
Buffers:         24232 kB
Cached:         268536 kB
SwapCached:        516 kB
Active:          36492 kB
Inactive:       258284 kB
HighTotal:      131008 kB
HighFree:        28868 kB
LowTotal:       903652 kB
LowFree:        692016 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13256 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:57:24 (client local time) WITH STATUS 10 IN 1200.44 SECONDS
stats: 12381 7 1200.44 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.92 0.96 0.91 2/54 1271
Raw data (stat): 1271 (runsolver) R 1270 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491593274 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.0003 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 8730 0 0 0 978 20 0 0 25 0 1 0 491593274 33546240 7302 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8190 7302 603 41 0 8149 0
vsize: 32760
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 9085 0 0 0 1977 21 0 0 25 0 1 0 491593274 35024896 7657 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8551 7657 603 41 0 8510 0
vsize: 34204
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 9502 0 0 0 2975 23 0 0 25 0 1 0 491593274 36765696 8074 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8976 8074 603 41 0 8935 0
vsize: 35904
[startup+40.0008 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 9925 0 0 0 3974 25 0 0 25 0 1 0 491593274 38400000 8497 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9375 8497 603 41 0 9334 0
vsize: 37500
[startup+50.0005 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 10479 0 0 0 4973 26 0 0 25 0 1 0 491593274 40386560 8984 4294967295 134512640 134672761 3221224624 3221223760 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9860 8984 603 41 0 9819 0
vsize: 39440
[startup+59.9997 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 10793 0 0 0 5973 26 0 0 25 0 1 0 491593274 41517056 9252 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10136 9252 603 41 0 10095 0
vsize: 40544
[startup+70.0002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 11205 0 0 0 6972 28 0 0 25 0 1 0 491593274 43266048 9664 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10563 9664 603 41 0 10522 0
vsize: 42252
[startup+80 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 11643 0 0 0 7971 29 0 0 25 0 1 0 491593274 45121536 10102 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11016 10102 603 41 0 10975 0
vsize: 44064
[startup+90.0001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 12076 0 0 0 8970 30 0 0 25 0 1 0 491593274 46874624 10535 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10535 603 41 0 11403 0
vsize: 45776
[startup+99.9996 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 12507 0 0 0 9969 32 0 0 25 0 1 0 491593274 48619520 10966 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11870 10966 603 41 0 11829 0
vsize: 47480
[startup+109.999 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 12972 0 0 0 10968 33 0 0 25 0 1 0 491593274 50499584 11431 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12329 11431 603 41 0 12288 0
vsize: 49316
[startup+120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 13327 0 0 0 11967 34 0 0 25 0 1 0 491593274 51982336 11786 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12691 11786 603 41 0 12650 0
vsize: 50764
[startup+129.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 13722 0 0 0 12967 35 0 0 25 0 1 0 491593274 53600256 12181 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13086 12181 603 41 0 13045 0
vsize: 52344
[startup+139.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 14203 0 0 0 13966 36 0 0 25 0 1 0 491593274 55074816 12568 4294967295 134512640 134672761 3221224624 3221223808 134593652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13446 12568 603 41 0 13405 0
vsize: 53784
[startup+149.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 14479 0 0 0 14965 37 0 0 25 0 1 0 491593274 56225792 12828 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13727 12828 603 41 0 13686 0
vsize: 54908
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 14838 0 0 0 15964 38 0 0 25 0 1 0 491593274 57708544 13187 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14089 13187 603 41 0 14048 0
vsize: 56356
[startup+169.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 15213 0 0 0 16964 39 0 0 25 0 1 0 491593274 59191296 13562 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14451 13562 603 41 0 14410 0
vsize: 57804
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 15650 0 0 0 17963 40 0 0 25 0 1 0 491593274 61067264 13999 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14909 13999 603 41 0 14868 0
vsize: 59636
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16041 0 0 0 18962 41 0 0 25 0 1 0 491593274 62681088 14390 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15303 14390 603 41 0 15262 0
vsize: 61212
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16440 0 0 0 19961 43 0 0 25 0 1 0 491593274 64294912 14789 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15697 14789 603 41 0 15656 0
vsize: 62788
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 20960 43 0 0 25 0 1 0 491593274 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134560867 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 21960 44 0 0 25 0 1 0 491593274 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134561205 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 22960 44 0 0 25 0 1 0 491593274 64684032 14891 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 23961 44 0 0 25 0 1 0 491593274 64684032 14891 4294967295 134512640 134672761 3221224624 3221223728 134560248 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 24961 44 0 0 25 0 1 0 491593274 64684032 14891 4294967295 134512640 134672761 3221224624 3221223824 134557911 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 25961 44 0 0 25 0 1 0 491593274 64684032 14891 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 26962 44 0 0 25 0 1 0 491593274 64684032 14891 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 27962 44 0 0 25 0 1 0 491593274 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+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 28962 44 0 0 25 0 1 0 491593274 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+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 29963 44 0 0 25 0 1 0 491593274 64684032 14891 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 30963 44 0 0 25 0 1 0 491593274 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+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 31963 44 0 0 25 0 1 0 491593274 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+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16654 0 0 0 32964 44 0 0 25 0 1 0 491593274 64684032 14891 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 14891 603 41 0 15751 0
vsize: 63168
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 16989 0 0 0 33963 45 0 0 25 0 1 0 491593274 66170880 15226 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16155 15226 603 41 0 16114 0
vsize: 64620
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 17393 0 0 0 34962 46 0 0 25 0 1 0 491593274 67780608 15630 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16548 15630 603 41 0 16507 0
vsize: 66192
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 17756 0 0 0 35961 48 0 0 25 0 1 0 491593274 69263360 15993 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16910 15993 603 41 0 16869 0
vsize: 67640
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 18145 0 0 0 36960 49 0 0 25 0 1 0 491593274 70881280 16382 4294967295 134512640 134672761 3221224624 3221223808 134558938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17305 16382 603 41 0 17264 0
vsize: 69220
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 18486 0 0 0 37960 49 0 0 25 0 1 0 491593274 72224768 16723 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17633 16723 603 41 0 17592 0
vsize: 70532
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 18889 0 0 0 38959 51 0 0 25 0 1 0 491593274 73834496 17126 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18026 17126 603 41 0 17985 0
vsize: 72104
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 19276 0 0 0 39958 52 0 0 25 0 1 0 491593274 75444224 17513 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18419 17513 603 41 0 18378 0
vsize: 73676
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 19710 0 0 0 40957 53 0 0 25 0 1 0 491593274 77205504 17947 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18849 17947 603 41 0 18808 0
vsize: 75396
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 20159 0 0 0 41957 54 0 0 25 0 1 0 491593274 79101952 18396 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19312 18396 603 41 0 19271 0
vsize: 77248
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 20594 0 0 0 42955 56 0 0 25 0 1 0 491593274 80830464 18831 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19734 18831 603 41 0 19693 0
vsize: 78936
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 21023 0 0 0 43954 57 0 0 25 0 1 0 491593274 82558976 19260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20156 19260 603 41 0 20115 0
vsize: 80624
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 21407 0 0 0 44954 58 0 0 25 0 1 0 491593274 84193280 19644 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20555 19644 603 41 0 20514 0
vsize: 82220
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 21686 0 0 0 45953 59 0 0 25 0 1 0 491593274 85270528 19923 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20818 19923 603 41 0 20777 0
vsize: 83272
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 22022 0 0 0 46953 60 0 0 25 0 1 0 491593274 86609920 20259 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21145 20259 603 41 0 21104 0
vsize: 84580
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 22356 0 0 0 47952 61 0 0 25 0 1 0 491593274 88084480 20593 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21505 20593 603 41 0 21464 0
vsize: 86020
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 22687 0 0 0 48951 61 0 0 25 0 1 0 491593274 89407488 20924 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21828 20924 603 41 0 21787 0
vsize: 87312
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 22985 0 0 0 49951 63 0 0 25 0 1 0 491593274 90607616 21222 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22121 21222 603 41 0 22080 0
vsize: 88484
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 23331 0 0 0 50950 64 0 0 25 0 1 0 491593274 91955200 21568 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22450 21568 603 41 0 22409 0
vsize: 89800
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 23696 0 0 0 51949 65 0 0 25 0 1 0 491593274 93560832 21933 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22842 21933 603 41 0 22801 0
vsize: 91368
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 24043 0 0 0 52949 66 0 0 25 0 1 0 491593274 94904320 22280 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23170 22280 603 41 0 23129 0
vsize: 92680
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 24377 0 0 0 53948 66 0 0 25 0 1 0 491593274 96247808 22614 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23498 22614 603 41 0 23457 0
vsize: 93992
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 24695 0 0 0 54948 67 0 0 25 0 1 0 491593274 97595392 22932 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23827 22932 603 41 0 23786 0
vsize: 95308
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 25024 0 0 0 55948 67 0 0 25 0 1 0 491593274 98934784 23261 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24154 23261 603 41 0 24113 0
vsize: 96616
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 25336 0 0 0 56947 69 0 0 25 0 1 0 491593274 100139008 23573 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24448 23573 603 41 0 24407 0
vsize: 97792
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 25675 0 0 0 57946 70 0 0 25 0 1 0 491593274 101613568 23912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24808 23912 603 41 0 24767 0
vsize: 99232
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 26018 0 0 0 58945 72 0 0 25 0 1 0 491593274 103215104 24255 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25199 24255 603 41 0 25158 0
vsize: 100796
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 26317 0 0 0 59944 72 0 0 25 0 1 0 491593274 104431616 24554 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25496 24554 603 41 0 25455 0
vsize: 101984
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 26650 0 0 0 60944 73 0 0 25 0 1 0 491593274 105758720 24887 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25820 24887 603 41 0 25779 0
vsize: 103280
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 26970 0 0 0 61943 74 0 0 25 0 1 0 491593274 107102208 25207 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26148 25207 603 41 0 26107 0
vsize: 104592
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 27311 0 0 0 62942 76 0 0 25 0 1 0 491593274 108568576 25548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26506 25548 603 41 0 26465 0
vsize: 106024
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 27687 0 0 0 63942 77 0 0 25 0 1 0 491593274 110039040 25924 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26865 25924 603 41 0 26824 0
vsize: 107460
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 28029 0 0 0 64941 78 0 0 25 0 1 0 491593274 111505408 26266 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27223 26266 603 41 0 27182 0
vsize: 108892
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 28393 0 0 0 65940 79 0 0 25 0 1 0 491593274 112988160 26630 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27585 26630 603 41 0 27544 0
vsize: 110340
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 28793 0 0 0 66939 80 0 0 25 0 1 0 491593274 114569216 27030 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27971 27030 603 41 0 27930 0
vsize: 111884
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 29126 0 0 0 67939 81 0 0 25 0 1 0 491593274 115908608 27363 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28298 27363 603 41 0 28257 0
vsize: 113192
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 29457 0 0 0 68938 82 0 0 25 0 1 0 491593274 117243904 27694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28624 27694 603 41 0 28583 0
vsize: 114496
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 29813 0 0 0 69937 83 0 0 25 0 1 0 491593274 118689792 28050 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28977 28050 603 41 0 28936 0
vsize: 115908
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30199 0 0 0 70936 84 0 0 25 0 1 0 491593274 120299520 28436 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29370 28436 603 41 0 29329 0
vsize: 117480
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30563 0 0 0 71936 85 0 0 25 0 1 0 491593274 121765888 28800 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29728 28800 603 41 0 29687 0
vsize: 118912
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 72936 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 73936 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 74937 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 75937 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 76937 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 77938 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 78938 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 79938 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 80939 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 81939 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 82939 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 83940 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 84940 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223808 134558930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 85940 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 86941 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 87941 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 88941 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 89942 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 90942 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 91943 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+930.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 92943 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 93943 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+950.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 94944 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+960.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 95944 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+970.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 96944 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+980.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 97945 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 98945 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 99945 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 100946 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 101946 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 102946 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 103947 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 104947 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 105947 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 106948 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223760 134565089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 107948 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134560332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 108949 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 109949 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 110949 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 111950 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 112950 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134559063 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 113950 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 114951 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 115951 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30709 0 0 0 116952 85 0 0 25 0 1 0 491593274 121880576 28836 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29756 28836 603 41 0 29715 0
vsize: 119024
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 30972 0 0 0 117951 86 0 0 25 0 1 0 491593274 123088896 29099 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30051 29099 603 41 0 30010 0
vsize: 120204
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 31286 0 0 0 118950 87 0 0 25 0 1 0 491593274 124293120 29413 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30345 29413 603 41 0 30304 0
vsize: 121380
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1271
Raw data (stat): 1271 (minisat+) R 1270 29653 29652 0 -1 0 31655 0 0 0 119949 88 0 0 25 0 1 0 491593274 125755392 29782 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30702 29782 603 41 0 30661 0
vsize: 122808
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1271
Raw data (stat): 1271 (minisat+) Z 1270 29653 29652 0 -1 12 31658 0 0 0 119950 94 0 0 25 0 1 0 491593274 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.44
CPU user time (s): 1199.5
CPU system time (s): 0.941856
CPU usage (%): 100.03
Max. virtual memory (Kb): 122808
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####