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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x12.opb
MD5SUM	ddd1f838c1e3a248aad1987162b1d40d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	656964
Optimality of the best value was proved	NO
Number of terms in the objective function	2520
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	666682247
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	666682247
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.04
Number of variables	2520
Total number of constraints	142
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	142
Minimum length of a constraint	21
Maximum length of a constraint	240
Trace number 17684

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        511128 kB
Buffers:         18964 kB
Cached:         478420 kB
SwapCached:        512 kB
Active:         114856 kB
Inactive:       384524 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        510876 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            18424 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:41:39 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 19240 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 164 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 162]---> Adder-cost: 222   maxlim: 13044   bits: 14/14
c ---[ 160]---> Adder-cost: 230   maxlim: 20340   bits: 15/15
c ---[ 158]---> Adder-cost: 230   maxlim: 19188   bits: 15/15
c ---[ 156]---> Adder-cost: 230   maxlim: 20852   bits: 15/15
c ---[ 154]---> Adder-cost: 222   maxlim: 13812   bits: 14/14
c ---[ 152]---> Adder-cost: 222   maxlim: 13556   bits: 14/14
c ---[ 150]---> Adder-cost: 230   maxlim: 19444   bits: 15/15
c ---[ 148]---> Adder-cost: 214   maxlim: 9076   bits: 14/14
c ---[ 146]---> Adder-cost: 214   maxlim: 9076   bits: 14/14
c ---[ 144]---> Adder-cost: 222   maxlim: 13300   bits: 14/14
c ---[ 142]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Adder-cost: 196   maxlim: 16758   bits: 15/15
c ---[ 132]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 2162     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 119]---> BDD-cost:   10
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   10
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   13
c ---[ 111]---> BDD-cost:   10
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   10
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   11
c ---[ 103]---> BDD-cost:   13
c ---[ 102]---> BDD-cost:   13
c ---[ 101]---> BDD-cost:   10
c ---[ 100]---> BDD-cost:   10
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:   13
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   13
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   17
c ---[  90]---> BDD-cost:   13
c ---[  89]---> BDD-cost:   10
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   17
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   10
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   13
c ---[  70]---> BDD-cost:   16
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   10
c ---[  60]---> BDD-cost:   17
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   10
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   10
c ---[  35]---> BDD-cost:   10
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   10
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   15
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   10
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   10
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   72528   190921 |   24176       0        0     nan |  0.000 % |
c |       100 |   72528   190921 |   26593     100     4141    41.4 |  8.931 % |
c |       250 |   72528   190921 |   29252     250     6852    27.4 |  8.931 % |
c |       475 |   72521   190898 |   32178     473     9243    19.5 |  8.935 % |
c |       812 |   72181   190108 |   35396     780    10516    13.5 |  9.335 % |
c |      1318 |   72173   190082 |   38935    1285    13135    10.2 |  9.339 % |
c |      2077 |   71911   189485 |   42829    2029    16331     8.0 |  9.646 % |
c |      3216 |   71882   189418 |   47112    3166    23056     7.3 |  9.689 % |
c |      4928 |   70737   186788 |   51823    4846    31738     6.5 | 11.203 % |
c |      7490 |   69922   184817 |   57005    7354    45256     6.2 | 12.212 % |
c |     11334 |   69103   182825 |   62706   11140    68768     6.2 | 13.247 % |
c |     17100 |   68137   180467 |   68976   16766   113540     6.8 | 14.387 % |
c ==============================================================================
c [1mFound solution: 3010815[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4798   maxlim: 909448   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20036 |  101206   299094 |   33735   19667   136737     7.0 | 14.387 % |
c |     20136 |  101206   299094 |   37108   19767   137423     7.0 | 12.468 % |
c |     20286 |  101174   298990 |   40819   19912   138548     7.0 | 12.489 % |
c |     20511 |  101174   298990 |   44901   20137   140695     7.0 | 12.489 % |
c |     20848 |  101130   298891 |   49391   20473   144560     7.1 | 12.538 % |
c ==============================================================================
c [1mFound solution: 3000107[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 920156   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21313 |  101138   299015 |   33712   20938   148422     7.1 | 12.538 % |
c |     21414 |  101138   299015 |   37083   21039   148955     7.1 | 12.563 % |
c |     21567 |  101138   299015 |   40791   21192   150034     7.1 | 12.563 % |
c |     21792 |  101138   299015 |   44870   21417   152857     7.1 | 12.563 % |
c |     22129 |  101121   298958 |   49357   21749   157122     7.2 | 12.570 % |
c |     22635 |  101121   298958 |   54293   22255   174079     7.8 | 12.570 % |
c |     23395 |  101121   298958 |   59722   23015   187383     8.1 | 12.570 % |
c |     24534 |  101027   298727 |   65695   24144   199200     8.3 | 12.671 % |
c ==============================================================================
c [1mFound solution: 2640539[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1279724   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25951 |  100804   298352 |   33601   25536   235377     9.2 | 12.671 % |
c |     26051 |  100737   298190 |   36961   25627   236017     9.2 | 13.059 % |
c |     26201 |  100679   298059 |   40657   25767   237731     9.2 | 13.115 % |
c |     26426 |  100679   298059 |   44722   25992   239453     9.2 | 13.115 % |
c |     26764 |  100679   298059 |   49195   26330   249111     9.5 | 13.115 % |
c |     27270 |  100508   297668 |   54114   26819   254949     9.5 | 13.304 % |
c |     28030 |  100508   297668 |   59526   27579   269387     9.8 | 13.304 % |
c |     29171 |  100417   297422 |   65478   28712   284873     9.9 | 13.385 % |
c |     30880 |  100417   297422 |   72026   30421   355719    11.7 | 13.385 % |
c |     33442 |  100199   296891 |   79229   32961   419843    12.7 | 13.608 % |
c ==============================================================================
c [1mFound solution: 2640308[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1279955   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36112 |  100188   296922 |   33396   35627   518477    14.6 | 13.608 % |
c |     36213 |  100116   296753 |   36735   35727   519458    14.5 | 13.721 % |
c |     36365 |  100116   296753 |   40409   35879   521164    14.5 | 13.721 % |
c |     36592 |  100077   296662 |   44450   36101   523803    14.5 | 13.766 % |
c |     36929 |  100077   296662 |   48895   36438   532916    14.6 | 13.766 % |
c |     37435 |   99917   296264 |   53784   36928   536415    14.5 | 13.938 % |
c ==============================================================================
c [1mFound solution: 2610375[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1309888   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37836 |   99941   296407 |   33313   37329   546249    14.6 | 13.938 % |
c |     37936 |   99865   296234 |   36644   18755   316036    16.9 | 14.036 % |
c |     38086 |   99865   296234 |   40308   18905   317067    16.8 | 14.036 % |
c |     38311 |   99865   296234 |   44339   19130   318758    16.7 | 14.036 % |
c |     38648 |   99728   295915 |   48773   19462   321663    16.5 | 14.204 % |
c |     39154 |   99675   295790 |   53650   19965   327008    16.4 | 14.260 % |
c |     39915 |   99675   295790 |   59016   20726   412452    19.9 | 14.260 % |
c ==============================================================================
c [1mFound solution: 1955275[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1964988   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40798 |   99719   296045 |   33239   21607   428647    19.8 | 14.260 % |
c |     40899 |   99719   296045 |   36562   21708   429716    19.8 | 14.317 % |
c |     41049 |   99719   296045 |   40219   21858   431093    19.7 | 14.317 % |
c |     41275 |   99719   296045 |   44241   22084   454173    20.6 | 14.317 % |
c |     41612 |   99719   296045 |   48665   22421   459153    20.5 | 14.317 % |
c |     42118 |   99695   295963 |   53531   22921   468638    20.4 | 14.331 % |
c |     42877 |   99695   295963 |   58884   23680   482405    20.4 | 14.331 % |
c |     44016 |   99695   295963 |   64773   24819   523954    21.1 | 14.331 % |
c |     45725 |   99695   295963 |   71250   26528   574043    21.6 | 14.331 % |
c ==============================================================================
c [1mFound solution: 1524647[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2395616   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47748 |   99660   295535 |   33220   28389   642964    22.6 | 14.331 % |
c |     47848 |   99660   295535 |   36542   28489   643673    22.6 | 14.376 % |
c |     47999 |   99556   295295 |   40196   28638   644911    22.5 | 14.502 % |
c |     48224 |   99556   295295 |   44215   28863   647118    22.4 | 14.502 % |
c |     48561 |   99556   295295 |   48637   29200   650302    22.3 | 14.502 % |
c |     49069 |   99556   295295 |   53501   29708   662294    22.3 | 14.502 % |
c |     49829 |   99556   295295 |   58851   30468   686359    22.5 | 14.502 % |
c |     50968 |   99556   295295 |   64736   31607   716749    22.7 | 14.502 % |
c |     52676 |   99490   295143 |   71210   33310   863727    25.9 | 14.568 % |
c |     55239 |   99426   295000 |   78331   35858   953211    26.6 | 14.635 % |
c |     59083 |   99401   294941 |   86164   39699  1096503    27.6 | 14.659 % |
c |     64850 |   99391   294911 |   94780   45461  1336644    29.4 | 14.666 % |
c |     73499 |   99354   294806 |  104258   54104  1761851    32.6 | 14.701 % |
c |     86474 |   99345   294775 |  114684   67075  2626022    39.2 | 14.704 % |
c |    105935 |   99218   294481 |  126152   86513  3971122    45.9 | 14.848 % |
c |    135129 |   99214   294471 |  138768  115706  5631568    48.7 | 14.851 % |
c |    178918 |   98648   293157 |  152645   30081  1182016    39.3 | 15.493 % |
c |    244603 |   98248   292229 |  167909   95737  5206895    54.4 | 15.954 % |
c ==============================================================================
c [1mFound solution: 1335837[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2584426   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    277375 |   98187   292220 |   32729  128501  9719423    75.6 | 15.954 % |
c |    277476 |   98187   292220 |   36001   19834  2663043   134.3 | 16.081 % |
c |    277627 |   98187   292220 |   39602   19985  2663861   133.3 | 16.081 % |
c |    277852 |   98187   292220 |   43562   20210  2665110   131.9 | 16.081 % |
c |    278189 |   98182   292209 |   47918   20546  2668256   129.9 | 16.088 % |
c |    278695 |   98131   292089 |   52710   21049  2673860   127.0 | 16.147 % |
c |    279454 |   98082   291974 |   57981   21806  2677899   122.8 | 16.206 % |
c |    280594 |   98082   291974 |   63779   22946  2686066   117.1 | 16.206 % |
c |    282302 |   98011   291811 |   70157   24650  2704844   109.7 | 16.287 % |
c |    284864 |   97975   291730 |   77173   27208  2730763   100.4 | 16.321 % |
c |    288708 |   97969   291716 |   84890   31051  2810225    90.5 | 16.328 % |
c |    294475 |   97969   291716 |   93379   36818  3035097    82.4 | 16.328 % |
c |    303126 |   97969   291716 |  102717   45469  3676107    80.8 | 16.328 % |
c |    316101 |   97969   291716 |  112989   58444  4157945    71.1 | 16.328 % |
c |    335563 |   97898   291552 |  124288   77899  5235447    67.2 | 16.405 % |
c |    364757 |   97817   291363 |  136717  107088  6559253    61.3 | 16.492 % |
c |    408547 |   97809   291343 |  150388   27699  1140730    41.2 | 16.499 % |
c |    474231 |   97725   291132 |  165427   93363  4645126    49.8 | 16.579 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 X0_bit_5 -X0_bit_4 X0_bit_3 X0_bit_2 X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 X1_bit_7 X1_bit_6 X1_bit_5 -X1_bit_4 X1_bit_3 X1_bit_2 X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 X5_bit_7 X5_bit_6 X5_bit_5 X5_bit_4 -X5_bit_3 X5_bit_2 X5_bit_1 -X5_bit0 X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 X7_bit_5 -X7_bit_4 X7_bit_3 X7_bit_2 X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 X8_bit_7 -X8_bit_6 X8_bit_5 X8_bit_4 X8_bit_3 X8_bit_2 X8_bit_1 X8_bit0 X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 X10_bit_6 X10_bit_5 -X10_bit_4 X10_bit_3 -X10_bit_2 -X10_bit_1 X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 X11_bit_7 X11_bit_6 X11_bit_5 X11_bit_4 X11_bit_3 -X11_bit_2 -X11_bit_1 X11_bit0 X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X15_bit_7 -X15_bit_6 X15_bit_5 -X15_bit_4 -X15_bit_3 X15_bit_2 -X15_bit_1 -X15_bit0 X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 X17_bit_6 X17_bit_5 X17_bit_4 X17_bit_3 X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 X20_bit_6 X20_bit_5 X20_bit_4 X20_bit_3 X20_bit_2 X20_bit_1 -X20_bit0 X20_bit1 X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 X21_bit_7 X21_bit_6 X21_bit_5 X21_bit_4 -X21_bit_3 X21_bit_2 -X21_bit_1 X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 X22_bit_6 X22_bit_5 X22_bit_4 -X22_bit_3 X22_bit_2 -X22_bit_1 X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 X28_bit_4 -X28_bit_3 X28_bit_2 X28_bit_1 -X28_bit0 X28_bit1 -X28_bit2 X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 X29_bit_2 X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 X35_bit_6 X35_bit_5 -X35_bit_4 X35_bit_3 X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 X41_bit_3 X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 X47_bit_3 -X47_bit_2 X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 X50_bit_7 X50_bit_6 -X50_bit_5 X50_bit_4 X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 X55_bit_5 X55_bit_4 X55_bit_3 X55_bit_2 X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 X58_bit_5 X58_bit_4 -X58_bit_3 X58_bit_2 -X58_bit_1 X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 -X59_bit_6 X59_bit_5 X59_bit_4 X59_bit_3 X59_bit_2 -X59_bit_1 X59_bit0 X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 X60_bit_5 X60_bit_4 X60_bit_3 -X60_bit_2 X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 X62_bit_7 X62_bit_6 X62_bit_5 X62_bit_4 X62_bit_3 -X62_bit_2 X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 X64_bit_7 -X64_bit_6 X64_bit_5 X64_bit_4 X64_bit_3 X64_bit_2 X64_bit_1 X64_bit0 X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 X65_bit_5 X65_bit_4 X65_bit_3 X65_bit_2 X65_bit_1 X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 X68_bit_6 X68_bit_5 X68_bit_4 -X68_bit_3 X68_bit_2 -X68_bit_1 X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 X69_bit_7 X69_bit_6 X69_bit_5 X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 X70_bit_6 X70_bit_5 X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 X74_bit_7 -X74_bit_6 X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 X74_bit_1 -X74_bit0 X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 X76_bit_5 X76_bit_4 X76_bit_3 X76_bit_2 X76_bit_1 -X76_bit0 -X76_bit1 X76_bit2 X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 X80_bit_7 X80_bit_6 X80_bit_5 -X80_bit_4 X80_bit_3 X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 X80_bit2 X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 X85_bit_4 X85_bit_3 -X85_bit_2 X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 X86_bit_7 -X86_bit_6 -X86_bit_5 X86_bit_4 -X86_bit_3 -X86_bit_2 X86_bit_1 -X86_bit0 X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 X87_bit_5 X87_bit_4 X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 X88_bit_7 X88_bit_6 X88_bit_5 X88_bit_4 X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 X92_bit_7 X92_bit_6 X92_bit_5 X92_bit_4 X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 X93_bit_6 -X93_bit_5 X93_bit_4 X93_bit_3 X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 X95_bit_7 X95_bit_6 -X95_bit_5 X95_bit_4 X95_bit_3 X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 X97_bit_6 -X97_bit_5 -X97_bit_4 X97_bit_3 X97_bit_2 -X97_bit_1 X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 -X98_bit_5 X98_bit_4 -X98_bit_3 X98_bit_2 X98_bit_1 -X98_bit0 X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 X101_bit_6 X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 X105_bit_4 -X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 -X106_bit_6 -X106_bit_5 -X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 -X107_bit_5 X107_bit_4 X107_bit_3 -X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 -X108_bit_6 -X108_bit_5 -X108_bit_4 X108_bit_3 X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 X109_bit_7 X109_bit_6 X109_bit_5 X109_bit_4 X109_bit_3 X109_bit_2 X109_bit_1 X109_bit0 X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 X110_bit_7 X110_bit_6 X110_bit_5 X110_bit_4 -X110_bit_3 -X110_bit_2 X110_bit_1 X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 X111_bit_7 X111_bit_6 X111_bit_5 X111_bit_4 X111_bit_3 X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 -X112_bit_5 -X112_bit_4 -X112_bit_3 -X112_bit_2 -X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 X113_bit_7 X113_bit_6 X113_bit_5 X113_bit_4 X113_bit_3 X113_bit_2 X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 X116_bit_7 X116_bit_6 X116_bit_5 X116_bit_4 X116_bit_3 X116_bit_2 X116_bit_1 X116_bit0 X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 -X117_bit_6 -X117_bit_5 -X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_#### 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.79 0.95 0.93 2/54 18908
Raw data (stat): 18908 (runsolver) R 18907 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544677223 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.82 0.95 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 2453 0 0 0 994 5 0 0 25 0 1 0 544677223 12021760 2375 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2935 2375 603 41 0 2894 0
vsize: 11740
[startup+20.0022 s]
Raw data (loadavg): 0.85 0.95 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 2559 0 0 0 1993 5 0 0 25 0 1 0 544677223 12546048 2481 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2481 603 41 0 3022 0
vsize: 12252
[startup+30.003 s]
Raw data (loadavg): 0.87 0.95 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 5640 0 0 0 2986 12 0 0 25 0 1 0 544677223 23334912 4975 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5697 4975 603 41 0 5656 0
vsize: 22788
[startup+40.0034 s]
Raw data (loadavg): 0.89 0.95 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 5793 0 0 0 3986 13 0 0 25 0 1 0 544677223 23830528 5121 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5818 5121 603 41 0 5777 0
vsize: 23272
[startup+50.0037 s]
Raw data (loadavg): 0.91 0.96 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 6061 0 0 0 4984 14 0 0 25 0 1 0 544677223 25030656 5389 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6111 5389 603 41 0 6070 0
vsize: 24444
[startup+60.0045 s]
Raw data (loadavg): 0.92 0.96 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 6235 0 0 0 5984 15 0 0 25 0 1 0 544677223 25694208 5547 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6273 5547 603 41 0 6232 0
vsize: 25092
[startup+70.0049 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 6250 0 0 0 6984 15 0 0 25 0 1 0 544677223 25694208 5562 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6273 5562 603 41 0 6232 0
vsize: 25092
[startup+80.0062 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 6584 0 0 0 7982 17 0 0 25 0 1 0 544677223 27041792 5886 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6602 5886 603 41 0 6561 0
vsize: 26408
[startup+90.0069 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 6879 0 0 0 8981 18 0 0 25 0 1 0 544677223 28258304 6181 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6899 6181 603 41 0 6858 0
vsize: 27596
[startup+100.006 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 7333 0 0 0 9980 20 0 0 25 0 1 0 544677223 30138368 6635 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7358 6635 603 41 0 7317 0
vsize: 29432
[startup+110.008 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 7700 0 0 0 10979 20 0 0 25 0 1 0 544677223 31612928 7002 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7718 7002 603 41 0 7677 0
vsize: 30872
[startup+120.008 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 8063 0 0 0 11978 22 0 0 25 0 1 0 544677223 32956416 7365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8046 7365 603 41 0 8005 0
vsize: 32184
[startup+130.009 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 8770 0 0 0 12976 23 0 0 25 0 1 0 544677223 36175872 8072 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8832 8072 603 41 0 8791 0
vsize: 35328
[startup+140.009 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 9120 0 0 0 13975 24 0 0 25 0 1 0 544677223 37523456 8422 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9161 8422 603 41 0 9120 0
vsize: 36644
[startup+150.01 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 9546 0 0 0 14973 26 0 0 25 0 1 0 544677223 39264256 8848 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9586 8848 603 41 0 9545 0
vsize: 38344
[startup+160.01 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 10129 0 0 0 15972 28 0 0 25 0 1 0 544677223 41680896 9431 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10176 9431 603 41 0 10135 0
vsize: 40704
[startup+170.011 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 10493 0 0 0 16970 30 0 0 25 0 1 0 544677223 43155456 9795 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10536 9795 603 41 0 10495 0
vsize: 42144
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 10869 0 0 0 17968 32 0 0 25 0 1 0 544677223 44662784 10171 4294967295 134512640 134672761 3221224544 3221223728 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10904 10171 603 41 0 10863 0
vsize: 43616
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 11233 0 0 0 18967 33 0 0 25 0 1 0 544677223 46145536 10535 4294967295 134512640 134672761 3221224544 3221223728 134559033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11266 10535 603 41 0 11225 0
vsize: 45064
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 11574 0 0 0 19966 34 0 0 25 0 1 0 544677223 47628288 10876 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11628 10876 603 41 0 11587 0
vsize: 46512
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 11915 0 0 0 20965 35 0 0 25 0 1 0 544677223 48988160 11217 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11960 11217 603 41 0 11919 0
vsize: 47840
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 12261 0 0 0 21964 37 0 0 25 0 1 0 544677223 50335744 11563 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12289 11563 603 41 0 12248 0
vsize: 49156
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 12520 0 0 0 22963 38 0 0 25 0 1 0 544677223 51417088 11822 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12553 11822 603 41 0 12512 0
vsize: 50212
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 12766 0 0 0 23962 40 0 0 25 0 1 0 544677223 52494336 12068 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12816 12068 603 41 0 12775 0
vsize: 51264
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 13001 0 0 0 24961 40 0 0 25 0 1 0 544677223 53428224 12303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13044 12303 603 41 0 13003 0
vsize: 52176
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 13265 0 0 0 25960 42 0 0 25 0 1 0 544677223 55033856 12567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13436 12567 603 41 0 13395 0
vsize: 53744
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 13546 0 0 0 26958 43 0 0 25 0 1 0 544677223 56094720 12848 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13695 12848 603 41 0 13654 0
vsize: 54780
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 13818 0 0 0 27958 44 0 0 25 0 1 0 544677223 57171968 13120 4294967295 134512640 134672761 3221224544 3221223728 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13958 13120 603 41 0 13917 0
vsize: 55832
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14079 0 0 0 28957 45 0 0 25 0 1 0 544677223 58253312 13381 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14222 13381 603 41 0 14181 0
vsize: 56888
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14361 0 0 0 29956 46 0 0 25 0 1 0 544677223 59465728 13663 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14518 13663 603 41 0 14477 0
vsize: 58072
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14590 0 0 0 30954 48 0 0 25 0 1 0 544677223 60411904 13892 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14749 13892 603 41 0 14708 0
vsize: 58996
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 31954 48 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 32954 48 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 33954 48 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223680 134560720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 34954 49 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+360.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 35954 49 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 36953 49 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 37953 49 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 38953 50 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 39953 50 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 40953 50 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 41952 51 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+430.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 42952 51 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 43952 52 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+450.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 44952 52 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+460.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 45952 52 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 46952 52 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+480.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 47951 52 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 48951 53 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 49951 53 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 50951 53 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 14696 0 0 0 51951 54 0 0 25 0 1 0 544677223 60821504 13998 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 13998 603 41 0 14808 0
vsize: 59396
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 15012 0 0 0 52950 55 0 0 25 0 1 0 544677223 62038016 14314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15146 14314 603 41 0 15105 0
vsize: 60584
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 15741 0 0 0 53947 58 0 0 25 0 1 0 544677223 65134592 15043 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15902 15043 603 41 0 15861 0
vsize: 63608
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16491 0 0 0 54944 60 0 0 25 0 1 0 544677223 68104192 15793 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16627 15793 603 41 0 16586 0
vsize: 66508
[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 55943 62 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+570.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 56943 62 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 57943 62 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223680 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+590.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 58943 62 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+600.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 59943 63 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+610.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 60942 63 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 61942 64 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+630.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 62942 64 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+640.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 63942 64 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+650.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 64941 65 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223728 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 65941 65 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 66941 65 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 67941 65 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+690.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 68941 65 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223704 134565025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 69940 66 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16793 0 0 0 70940 66 0 0 25 0 1 0 544677223 69382144 16087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16087 603 41 0 16898 0
vsize: 67756
[startup+720.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16794 0 0 0 71940 66 0 0 25 0 1 0 544677223 69382144 16088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16088 603 41 0 16898 0
vsize: 67756
[startup+730.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16794 0 0 0 72940 67 0 0 25 0 1 0 544677223 69382144 16088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16088 603 41 0 16898 0
vsize: 67756
[startup+740.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16794 0 0 0 73940 67 0 0 25 0 1 0 544677223 69382144 16088 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16088 603 41 0 16898 0
vsize: 67756
[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16794 0 0 0 74939 67 0 0 25 0 1 0 544677223 69382144 16088 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16088 603 41 0 16898 0
vsize: 67756
[startup+760.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16794 0 0 0 75939 68 0 0 25 0 1 0 544677223 69382144 16088 4294967295 134512640 134672761 3221224544 3221223728 134558914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16088 603 41 0 16898 0
vsize: 67756
[startup+770.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16794 0 0 0 76939 68 0 0 25 0 1 0 544677223 69382144 16088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16088 603 41 0 16898 0
vsize: 67756
[startup+780.043 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16795 0 0 0 77939 68 0 0 25 0 1 0 544677223 69382144 16089 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16089 603 41 0 16898 0
vsize: 67756
[startup+790.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16795 0 0 0 78939 69 0 0 25 0 1 0 544677223 69382144 16089 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16089 603 41 0 16898 0
vsize: 67756
[startup+800.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16796 0 0 0 79938 69 0 0 25 0 1 0 544677223 69382144 16090 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16090 603 41 0 16898 0
vsize: 67756
[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 16881 0 0 0 80938 69 0 0 25 0 1 0 544677223 69652480 16175 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17005 16175 603 41 0 16964 0
vsize: 68020
[startup+820.045 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17052 0 0 0 81938 70 0 0 25 0 1 0 544677223 70463488 16346 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16346 603 41 0 17162 0
vsize: 68812
[startup+830.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17052 0 0 0 82938 70 0 0 25 0 1 0 544677223 70463488 16346 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16346 603 41 0 17162 0
vsize: 68812
[startup+840.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17052 0 0 0 83938 70 0 0 25 0 1 0 544677223 70463488 16346 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16346 603 41 0 17162 0
vsize: 68812
[startup+850.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17052 0 0 0 84937 71 0 0 25 0 1 0 544677223 70463488 16346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16346 603 41 0 17162 0
vsize: 68812
[startup+860.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 85937 71 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+870.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 86937 71 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+880.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 87937 72 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223680 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+890.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 88936 72 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+900.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 89936 72 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223784 134560737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+910.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 90936 73 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+920.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 91936 73 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+930.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 92935 74 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+940.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 93935 74 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223728 134559179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+950.055 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 94935 75 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+960.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 95935 75 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+970.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 96934 75 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+980.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 97934 75 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+990.059 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 98934 76 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 99934 76 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 100934 76 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 101935 76 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 102935 77 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 103935 77 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 104935 77 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 105935 77 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 106935 77 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 107936 77 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 108936 77 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17053 0 0 0 109936 77 0 0 25 0 1 0 544677223 70463488 16347 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16347 603 41 0 17162 0
vsize: 68812
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17055 0 0 0 110936 77 0 0 25 0 1 0 544677223 70463488 16349 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16349 603 41 0 17162 0
vsize: 68812
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17058 0 0 0 111936 77 0 0 25 0 1 0 544677223 70463488 16352 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16352 603 41 0 17162 0
vsize: 68812
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17061 0 0 0 112937 77 0 0 25 0 1 0 544677223 70463488 16355 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16355 603 41 0 17162 0
vsize: 68812
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17064 0 0 0 113937 77 0 0 25 0 1 0 544677223 70463488 16358 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16358 603 41 0 17162 0
vsize: 68812
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17066 0 0 0 114937 77 0 0 25 0 1 0 544677223 70463488 16360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16360 603 41 0 17162 0
vsize: 68812
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17068 0 0 0 115937 77 0 0 25 0 1 0 544677223 70463488 16362 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16362 603 41 0 17162 0
vsize: 68812
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17071 0 0 0 116937 77 0 0 25 0 1 0 544677223 70463488 16365 4294967295 134512640 134672761 3221224544 3221223760 134557677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16365 603 41 0 17162 0
vsize: 68812
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17093 0 0 0 117937 77 0 0 25 0 1 0 544677223 70463488 16387 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17203 16387 603 41 0 17162 0
vsize: 68812
[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17281 0 0 0 118937 77 0 0 25 0 1 0 544677223 71274496 16575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17401 16575 603 41 0 17360 0
vsize: 69604
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 18908
Raw data (stat): 18908 (minisat+) R 18907 18865 18864 0 -1 0 17487 0 0 0 119936 79 0 0 25 0 1 0 544677223 72077312 16781 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17597 16781 603 41 0 17556 0
vsize: 70388
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 18908
Raw data (stat): 18908 (minisat+) Z 18907 18865 18864 0 -1 12 17490 0 0 0 119937 82 0 0 25 0 1 0 544677223 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.12
CPU time (s): 1200.2
CPU user time (s): 1199.37
CPU system time (s): 0.822874
CPU usage (%): 100.007
Max. virtual memory (Kb): 70388
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####