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-ran10x10b.opb
MD5SUM	c76102ddcf7f5ab3b2677033d320eaa3
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	756736
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	502612132
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	502612132
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	422.405
Number of variables	2100
Total number of constraints	120
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	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 17697

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 11:25:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19211 boxname=wulflinc12 idbench=1478 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c76102ddcf7f5ab3b2677033d320eaa3  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-ran10x10b.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-ran10x10b.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-ran10x10b.opb
IDLAUNCH: 19211
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        841160 kB
Buffers:         13612 kB
Cached:         158736 kB
SwapCached:        508 kB
Active:          14636 kB
Inactive:       159904 kB
HighTotal:      131008 kB
HighFree:        82964 kB
LowTotal:       903652 kB
LowFree:        758196 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            13372 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:45:13 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 19211 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Adder-cost: 194   maxlim: 18678   bits: 15/15
c ---[ 136]---> Adder-cost: 178   maxlim: 7542   bits: 14/13
c ---[ 134]---> Adder-cost: 178   maxlim: 7926   bits: 14/13
c ---[ 132]---> Adder-cost: 194   maxlim: 18550   bits: 15/15
c ---[ 130]---> Adder-cost: 178   maxlim: 7798   bits: 14/13
c ---[ 128]---> Adder-cost: 186   maxlim: 13046   bits: 14/14
c ---[ 126]---> Adder-cost: 186   maxlim: 13430   bits: 14/14
c ---[ 124]---> Adder-cost: 162   maxlim: 4470   bits: 13/13
c ---[ 122]---> Adder-cost: 178   maxlim: 7926   bits: 14/13
c ---[ 120]---> Adder-cost: 194   maxlim: 17782   bits: 15/15
c ---[ 118]---> Adder-cost: 162   maxlim: 4726   bits: 13/13
c ---[ 116]---> Adder-cost: 188   maxlim: 12918   bits: 14/14
c ---[ 114]---> Adder-cost: 180   maxlim: 8950   bits: 14/14
c ---[ 112]---> Adder-cost: 196   maxlim: 18678   bits: 15/15
c ---[ 110]---> Adder-cost: 196   maxlim: 18806   bits: 15/15
c ---[ 108]---> Adder-cost: 162   maxlim: 4726   bits: 13/13
c ---[ 106]---> Adder-cost: 196   maxlim: 18550   bits: 15/15
c ---[ 104]---> Adder-cost: 188   maxlim: 13686   bits: 14/14
c ---[ 102]---> Adder-cost: 144   maxlim: 2422   bits: 12/12
c ---[ 100]---> Adder-cost: 188   maxlim: 13686   bits: 14/14
c ---[  99]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  98]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  97]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  96]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  95]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  94]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  93]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  92]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  91]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  90]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  89]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  88]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  87]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  86]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  85]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  84]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  83]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  82]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  81]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  80]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  79]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  78]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  77]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  76]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  75]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  74]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  73]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  72]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  71]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  70]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  69]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  68]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  67]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  66]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  65]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  64]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  63]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  62]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  61]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  60]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  59]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  58]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  57]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  56]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  55]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  54]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  53]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  52]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  51]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  50]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  48]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  47]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  46]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  45]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  44]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  43]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  42]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  41]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  40]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  37]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  36]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  35]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  34]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  33]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  32]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  31]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  30]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  29]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  28]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  27]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  26]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  25]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  24]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  23]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  22]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  21]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  20]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  19]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  18]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  17]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  16]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  14]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  13]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  11]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  10]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   9]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[   8]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   7]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[   6]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[   5]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   4]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[   3]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   2]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   1]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   0]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26615    97539 |    8871       0        0     nan |  0.000 % |
c |       100 |   26615    97539 |    9758     100      291     2.9 | 34.527 % |
c |       250 |   26549    97325 |   10733     240      983     4.1 | 34.688 % |
c |       475 |   26459    97029 |   11807     449     1801     4.0 | 34.916 % |
c |       812 |   26345    96643 |   12988     770     3323     4.3 | 35.171 % |
c |      1318 |   26260    96356 |   14286    1265     5511     4.4 | 35.386 % |
c |      2077 |   26138    95946 |   15715    2007     8910     4.4 | 35.667 % |
c |      3216 |   26065    95699 |   17287    3137    15427     4.9 | 35.842 % |
c |      4924 |   25896    95132 |   19015    4826    24748     5.1 | 36.258 % |
c |      7486 |   25782    94750 |   20917    7371    38509     5.2 | 36.539 % |
c |     11330 |   25666    94370 |   23009   11191    66703     6.0 | 36.834 % |
c ==============================================================================
c [1mFound solution: 3399023[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3932   maxlim: 710197   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15793 |   52967   191955 |   17655   15637   103218     6.6 | 36.834 % |
c |     15893 |   52967   191955 |   19420   15737   104033     6.6 | 24.395 % |
c |     16043 |   52967   191955 |   21362   15887   105348     6.6 | 24.395 % |
c |     16269 |   52951   191901 |   23498   16112   107745     6.7 | 24.421 % |
c |     16606 |   52944   191878 |   25848   16448   111083     6.8 | 24.430 % |
c |     17112 |   52944   191878 |   28433   16954   115033     6.8 | 24.430 % |
c |     17871 |   52944   191878 |   31276   17713   131699     7.4 | 24.430 % |
c |     19012 |   52937   191855 |   34404   18853   144201     7.6 | 24.438 % |
c ==============================================================================
c [1mFound solution: 3251698[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 857522   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20432 |   52951   192012 |   17650   20271   161055     7.9 | 24.438 % |
c |     20532 |   52951   192012 |   19415   20371   162579     8.0 | 24.524 % |
c ==============================================================================
c [1mFound solution: 3028424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1080796   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20670 |   52996   192307 |   17665   20509   164838     8.0 | 24.524 % |
c |     20770 |   52996   192307 |   19431   10355    81980     7.9 | 24.602 % |
c |     20921 |   52996   192307 |   21374   10506    82966     7.9 | 24.602 % |
c |     21146 |   52996   192307 |   23512   10731    84424     7.9 | 24.602 % |
c |     21483 |   52996   192307 |   25863   11068    90492     8.2 | 24.602 % |
c |     21990 |   52996   192307 |   28449   11575    94840     8.2 | 24.602 % |
c |     22749 |   52996   192307 |   31294   12334   102358     8.3 | 24.602 % |
c |     23888 |   52980   192255 |   34424   13471   113271     8.4 | 24.628 % |
c |     25599 |   52971   192224 |   37866   15178   127482     8.4 | 24.637 % |
c |     28161 |   52947   192144 |   41653   17737   162753     9.2 | 24.681 % |
c |     32005 |   52868   191877 |   45818   21571   225571    10.5 | 24.794 % |
c ==============================================================================
c [1mFound solution: 3007970[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1101250   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36570 |   52874   191990 |   17624   26131   337321    12.9 | 24.794 % |
c |     36670 |   52874   191990 |   19386   13166   177581    13.5 | 24.849 % |
c |     36820 |   52874   191990 |   21325   13316   178472    13.4 | 24.849 % |
c |     37045 |   52874   191990 |   23457   13541   179958    13.3 | 24.849 % |
c |     37382 |   52874   191990 |   25803   13878   182062    13.1 | 24.849 % |
c |     37888 |   52874   191990 |   28383   14384   185012    12.9 | 24.849 % |
c |     38647 |   52874   191990 |   31221   15143   216728    14.3 | 24.849 % |
c |     39786 |   52874   191990 |   34344   16282   226252    13.9 | 24.849 % |
c |     41494 |   52868   191970 |   37778   17988   241981    13.5 | 24.858 % |
c |     44056 |   52859   191941 |   41556   20549   326429    15.9 | 24.875 % |
c ==============================================================================
c [1mFound solution: 2684186[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1425034   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44261 |   52875   192110 |   17625   20754   330938    15.9 | 24.875 % |
c |     44361 |   52875   192110 |   19387   10477   127105    12.1 | 24.945 % |
c |     44511 |   52875   192110 |   21326   10627   128086    12.1 | 24.945 % |
c |     44736 |   52875   192110 |   23458   10852   130005    12.0 | 24.945 % |
c |     45073 |   52866   192081 |   25804   11188   132464    11.8 | 24.963 % |
c |     45579 |   52857   192052 |   28385   11693   135499    11.6 | 24.980 % |
c |     46338 |   52857   192052 |   31223   12452   141334    11.4 | 24.980 % |
c |     47477 |   52857   192052 |   34346   13591   152232    11.2 | 24.980 % |
c |     49185 |   52857   192052 |   37780   15299   182463    11.9 | 24.980 % |
c |     51747 |   52857   192052 |   41558   17861   219679    12.3 | 24.980 % |
c |     55591 |   52857   192052 |   45714   21705   309485    14.3 | 24.980 % |
c |     61357 |   52857   192052 |   50286   27471   566233    20.6 | 24.980 % |
c ==============================================================================
c [1mFound solution: 1943791[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2165429   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62763 |   52837   191728 |   17612   28282   577564    20.4 | 24.980 % |
c |     62863 |   52837   191728 |   19373   14241   334249    23.5 | 25.028 % |
c |     63013 |   52837   191728 |   21310   14391   335102    23.3 | 25.028 % |
c |     63238 |   52837   191728 |   23441   14616   336256    23.0 | 25.028 % |
c |     63575 |   52837   191728 |   25785   14953   337893    22.6 | 25.028 % |
c |     64081 |   52837   191728 |   28364   15459   340632    22.0 | 25.028 % |
c |     64840 |   52837   191728 |   31200   16218   344688    21.3 | 25.028 % |
c |     65979 |   52837   191728 |   34320   17357   369490    21.3 | 25.028 % |
c |     67687 |   52837   191728 |   37752   19065   405107    21.2 | 25.028 % |
c |     70249 |   52837   191728 |   41528   21627   433077    20.0 | 25.028 % |
c |     74093 |   52837   191728 |   45680   25471   508750    20.0 | 25.028 % |
c ==============================================================================
c [1mFound solution: 1284085[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2825135   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77839 |   52852   191847 |   17617   29217   637841    21.8 | 25.028 % |
c |     77939 |   52852   191847 |   19378   14709   228831    15.6 | 25.083 % |
c |     78089 |   52852   191847 |   21316   14859   229689    15.5 | 25.083 % |
c |     78314 |   52852   191847 |   23448   15084   231535    15.3 | 25.083 % |
c |     78651 |   52852   191847 |   25793   15421   236542    15.3 | 25.083 % |
c |     79157 |   52852   191847 |   28372   15927   240464    15.1 | 25.083 % |
c |     79916 |   52852   191847 |   31209   16686   261936    15.7 | 25.083 % |
c |     81055 |   52852   191847 |   34330   17825   276374    15.5 | 25.083 % |
c |     82763 |   52852   191847 |   37763   19533   321432    16.5 | 25.083 % |
c |     85325 |   52852   191847 |   41539   22095   414040    18.7 | 25.083 % |
c |     89170 |   52852   191847 |   45693   25940   548030    21.1 | 25.083 % |
c |     94936 |   52852   191847 |   50263   31706   794827    25.1 | 25.083 % |
c |    103585 |   52852   191847 |   55289   40355  1254965    31.1 | 25.083 % |
c |    116560 |   52852   191847 |   60818   53330  2733251    51.3 | 25.083 % |
c |    136021 |   52852   191847 |   66900   29467  1105966    37.5 | 25.083 % |
c |    165213 |   52852   191847 |   73590   58659  3531491    60.2 | 25.083 % |
c |    209002 |   52852   191847 |   80949   41154  3192086    77.6 | 25.083 % |
c |    274688 |   52852   191847 |   89044   40930  3366053    82.2 | 25.083 % |
c |    373214 |   52852   191847 |   97949   59847 18342922   306.5 | 25.083 % |
c ==============================================================================
c [1mFound solution: 1159434[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2949786   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    415126 |   52842   191893 |   17614  101754 21049144   206.9 | 25.083 % |
c |    415226 |   52842   191893 |   19375   10578  1222304   115.6 | 25.159 % |
c |    415376 |   52842   191893 |   21312   10728  1222957   114.0 | 25.159 % |
c |    415601 |   52842   191893 |   23444   10953  1223779   111.7 | 25.159 % |
c |    415939 |   52842   191893 |   25788   11291  1225210   108.5 | 25.159 % |
c |    416445 |   52842   191893 |   28367   11797  1227673   104.1 | 25.159 % |
c |    417205 |   52842   191893 |   31204   12557  1231191    98.0 | 25.159 % |
c |    418345 |   52842   191893 |   34324   13697  1254536    91.6 | 25.159 % |
c |    420053 |   52842   191893 |   37757   15405  1290885    83.8 | 25.159 % |
c |    422616 |   52842   191893 |   41532   17968  1394817    77.6 | 25.159 % |
c |    426462 |   52842   191893 |   45686   21814  1498450    68.7 | 25.159 % |
c |    432229 |   52842   191893 |   50254   27581  1580748    57.3 | 25.159 % |
c |    440879 |   52842   191893 |   55280   36231  2302487    63.6 | 25.159 % |
c |    453854 |   52842   191893 |   60808   49206  2835595    57.6 | 25.159 % |
c |    473315 |   52842   191893 |   66889   23098  1330428    57.6 | 25.159 % |
c |    502507 |   52842   191893 |   73578   52290  3067809    58.7 | 25.159 % |
c |    546296 |   52827   191842 |   80935   34316  5890499   171.7 | 25.176 % |
c |    611983 |   52818   191811 |   89029   31695  4571397   144.2 | 25.185 % |
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#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 28609
Raw data (stat): 28609 (runsolver) R 28608 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486476494 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 1742 0 0 0 994 4 0 0 25 0 1 0 486476494 9109504 1713 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2224 1713 603 41 0 2183 0
vsize: 8896
[startup+20.0018 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 1862 0 0 0 1992 5 0 0 25 0 1 0 486476494 9469952 1833 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2312 1833 603 41 0 2271 0
vsize: 9248
[startup+30.0032 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 2109 0 0 0 2990 7 0 0 25 0 1 0 486476494 10477568 2080 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2558 2080 603 41 0 2517 0
vsize: 10232
[startup+40.0035 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 2180 0 0 0 3990 7 0 0 25 0 1 0 486476494 11071488 2151 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2703 2151 603 41 0 2662 0
vsize: 10812
[startup+50.0041 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 2464 0 0 0 4988 8 0 0 25 0 1 0 486476494 12242944 2435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2989 2435 603 41 0 2948 0
vsize: 11956
[startup+60.0046 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 2534 0 0 0 5988 8 0 0 25 0 1 0 486476494 12513280 2505 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3055 2505 603 41 0 3014 0
vsize: 12220
[startup+70.0047 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 2618 0 0 0 6988 9 0 0 25 0 1 0 486476494 12918784 2589 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3154 2589 603 41 0 3113 0
vsize: 12616
[startup+80.0056 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 3251 0 0 0 7986 11 0 0 25 0 1 0 486476494 15613952 3222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3812 3222 603 41 0 3771 0
vsize: 15248
[startup+90.0061 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 4287 0 0 0 8984 13 0 0 25 0 1 0 486476494 19763200 4258 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4258 603 41 0 4784 0
vsize: 19300
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 5088 0 0 0 9982 15 0 0 25 0 1 0 486476494 22978560 5059 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5610 5059 603 41 0 5569 0
vsize: 22440
[startup+110.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 5400 0 0 0 10981 16 0 0 25 0 1 0 486476494 24326144 5371 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5939 5371 603 41 0 5898 0
vsize: 23756
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 5400 0 0 0 11981 16 0 0 25 0 1 0 486476494 24326144 5371 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5939 5371 603 41 0 5898 0
vsize: 23756
[startup+130.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 5400 0 0 0 12981 16 0 0 25 0 1 0 486476494 24326144 5371 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5939 5371 603 41 0 5898 0
vsize: 23756
[startup+140.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 5400 0 0 0 13982 16 0 0 25 0 1 0 486476494 24326144 5371 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5939 5371 603 41 0 5898 0
vsize: 23756
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 5400 0 0 0 14982 16 0 0 25 0 1 0 486476494 24326144 5371 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5939 5371 603 41 0 5898 0
vsize: 23756
[startup+160.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 5747 0 0 0 15981 17 0 0 25 0 1 0 486476494 25665536 5718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6266 5718 603 41 0 6225 0
vsize: 25064
[startup+170.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 6333 0 0 0 16979 19 0 0 25 0 1 0 486476494 28348416 6304 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6921 6304 603 41 0 6880 0
vsize: 27684
[startup+180.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 7141 0 0 0 17976 22 0 0 25 0 1 0 486476494 31576064 7112 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7112 603 41 0 7668 0
vsize: 30836
[startup+190.01 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 7411 0 0 0 18976 23 0 0 25 0 1 0 486476494 32788480 7382 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8005 7382 603 41 0 7964 0
vsize: 32020
[startup+200.01 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 7412 0 0 0 19976 23 0 0 25 0 1 0 486476494 32788480 7383 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8005 7383 603 41 0 7964 0
vsize: 32020
[startup+210.01 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 7412 0 0 0 20976 23 0 0 25 0 1 0 486476494 32788480 7383 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8005 7383 603 41 0 7964 0
vsize: 32020
[startup+220.011 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 7413 0 0 0 21976 23 0 0 25 0 1 0 486476494 32788480 7384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8005 7384 603 41 0 7964 0
vsize: 32020
[startup+230.012 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 7413 0 0 0 22976 23 0 0 25 0 1 0 486476494 32788480 7384 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8005 7384 603 41 0 7964 0
vsize: 32020
[startup+240.013 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 7413 0 0 0 23976 23 0 0 25 0 1 0 486476494 32788480 7384 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8005 7384 603 41 0 7964 0
vsize: 32020
[startup+250.013 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 7413 0 0 0 24977 23 0 0 25 0 1 0 486476494 32788480 7384 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8005 7384 603 41 0 7964 0
vsize: 32020
[startup+260.014 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 7965 0 0 0 25975 25 0 0 25 0 1 0 486476494 34938880 7936 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8530 7936 603 41 0 8489 0
vsize: 34120
[startup+270.014 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 8811 0 0 0 26973 27 0 0 25 0 1 0 486476494 38420480 8782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9380 8782 603 41 0 9339 0
vsize: 37520
[startup+280.016 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 8894 0 0 0 27973 28 0 0 25 0 1 0 486476494 38825984 8865 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 8865 603 41 0 9438 0
vsize: 37916
[startup+290.016 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 8894 0 0 0 28973 28 0 0 25 0 1 0 486476494 38825984 8865 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 8865 603 41 0 9438 0
vsize: 37916
[startup+300.016 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 8894 0 0 0 29973 28 0 0 25 0 1 0 486476494 38825984 8865 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 8865 603 41 0 9438 0
vsize: 37916
[startup+310.017 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 8894 0 0 0 30974 28 0 0 25 0 1 0 486476494 38825984 8865 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 8865 603 41 0 9438 0
vsize: 37916
[startup+320.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 8894 0 0 0 31974 28 0 0 25 0 1 0 486476494 38825984 8865 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 8865 603 41 0 9438 0
vsize: 37916
[startup+330.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 8894 0 0 0 32974 28 0 0 25 0 1 0 486476494 38825984 8865 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 8865 603 41 0 9438 0
vsize: 37916
[startup+340.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 8894 0 0 0 33974 28 0 0 25 0 1 0 486476494 38825984 8865 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 8865 603 41 0 9438 0
vsize: 37916
[startup+350.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 8894 0 0 0 34974 28 0 0 25 0 1 0 486476494 38825984 8865 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 8865 603 41 0 9438 0
vsize: 37916
[startup+360.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 9316 0 0 0 35974 29 0 0 25 0 1 0 486476494 40435712 9287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9872 9287 603 41 0 9831 0
vsize: 39488
[startup+370.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 10330 0 0 0 36971 31 0 0 25 0 1 0 486476494 44584960 10301 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10885 10301 603 41 0 10844 0
vsize: 43540
[startup+380.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 11429 0 0 0 37968 35 0 0 25 0 1 0 486476494 49164288 11400 4294967295 134512640 134672761 3221224544 3221223712 134561086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12003 11400 603 41 0 11962 0
vsize: 48012
[startup+390.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 12716 0 0 0 38963 39 0 0 25 0 1 0 486476494 54403072 12687 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13282 12687 603 41 0 13241 0
vsize: 53128
[startup+400.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 13598 0 0 0 39961 42 0 0 25 0 1 0 486476494 58023936 13569 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14166 13569 603 41 0 14125 0
vsize: 56664
[startup+410.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 13598 0 0 0 40961 42 0 0 25 0 1 0 486476494 58023936 13569 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14166 13569 603 41 0 14125 0
vsize: 56664
[startup+420.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 13598 0 0 0 41961 42 0 0 25 0 1 0 486476494 58023936 13569 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14166 13569 603 41 0 14125 0
vsize: 56664
[startup+430.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 13598 0 0 0 42961 42 0 0 25 0 1 0 486476494 58023936 13569 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14166 13569 603 41 0 14125 0
vsize: 56664
[startup+440.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 13598 0 0 0 43961 42 0 0 25 0 1 0 486476494 58023936 13569 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14166 13569 603 41 0 14125 0
vsize: 56664
[startup+450.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 13598 0 0 0 44962 42 0 0 25 0 1 0 486476494 58023936 13569 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14166 13569 603 41 0 14125 0
vsize: 56664
[startup+460.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 13598 0 0 0 45962 42 0 0 25 0 1 0 486476494 58023936 13569 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14166 13569 603 41 0 14125 0
vsize: 56664
[startup+470.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 13598 0 0 0 46962 42 0 0 25 0 1 0 486476494 58023936 13569 4294967295 134512640 134672761 3221224544 3221223680 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14166 13569 603 41 0 14125 0
vsize: 56664
[startup+480.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 14395 0 0 0 47960 44 0 0 25 0 1 0 486476494 61222912 14366 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14947 14366 603 41 0 14906 0
vsize: 59788
[startup+490.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 15221 0 0 0 48958 46 0 0 25 0 1 0 486476494 64569344 15192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15764 15192 603 41 0 15723 0
vsize: 63056
[startup+500.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 16180 0 0 0 49956 49 0 0 25 0 1 0 486476494 68595712 16151 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16747 16151 603 41 0 16706 0
vsize: 66988
[startup+510.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 17056 0 0 0 50955 50 0 0 25 0 1 0 486476494 72204288 17027 4294967295 134512640 134672761 3221224544 3221223560 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17628 17027 603 41 0 17587 0
vsize: 70512
[startup+520.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 17740 0 0 0 51953 52 0 0 25 0 1 0 486476494 74997760 17711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18310 17711 603 41 0 18269 0
vsize: 73240
[startup+530.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 18363 0 0 0 52951 54 0 0 25 0 1 0 486476494 77549568 18334 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18933 18334 603 41 0 18892 0
vsize: 75732
[startup+540.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 18969 0 0 0 53950 55 0 0 25 0 1 0 486476494 79929344 18940 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19514 18940 603 41 0 19473 0
vsize: 78056
[startup+550.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 19602 0 0 0 54948 58 0 0 25 0 1 0 486476494 82583552 19573 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20162 19573 603 41 0 20121 0
vsize: 80648
[startup+560.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 20298 0 0 0 55946 59 0 0 25 0 1 0 486476494 85385216 20269 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20846 20269 603 41 0 20805 0
vsize: 83384
[startup+570.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 20940 0 0 0 56944 62 0 0 25 0 1 0 486476494 88027136 20911 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21491 20911 603 41 0 21450 0
vsize: 85964
[startup+580.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 21516 0 0 0 57942 64 0 0 25 0 1 0 486476494 90411008 21487 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22073 21487 603 41 0 22032 0
vsize: 88292
[startup+590.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 21611 0 0 0 58941 65 0 0 25 0 1 0 486476494 90816512 21582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22172 21582 603 41 0 22131 0
vsize: 88688
[startup+600.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 21987 0 0 0 59939 66 0 0 25 0 1 0 486476494 92413952 21958 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22562 21958 603 41 0 22521 0
vsize: 90248
[startup+610.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 22479 0 0 0 60938 67 0 0 25 0 1 0 486476494 94298112 22450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23022 22450 603 41 0 22981 0
vsize: 92088
[startup+620.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 23115 0 0 0 61936 70 0 0 25 0 1 0 486476494 96989184 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23679 23086 603 41 0 23638 0
vsize: 94716
[startup+630.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 23802 0 0 0 62935 71 0 0 25 0 1 0 486476494 99782656 23773 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24361 23773 603 41 0 24320 0
vsize: 97444
[startup+640.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 63934 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+650.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 64934 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+660.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 65934 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223648 134555197 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+670.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 66934 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+680.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 67935 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+690.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 68935 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+700.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 69935 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+710.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 70935 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+720.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 71935 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+730.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 72935 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+740.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 73935 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+750.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 74935 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+760.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 75936 72 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+770.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 76936 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223696 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+780.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 77936 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+790.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 78936 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+800.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 79936 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+810.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 80936 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+820.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 81937 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+830.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 82937 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+840.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 83937 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+850.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 84937 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+860.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 85937 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+870.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 86937 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+880.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 87938 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+890.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 88938 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+900.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 89938 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+910.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 90938 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+920.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 91938 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+930.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 92938 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+940.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 93939 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+950.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 94939 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+960.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 95939 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+970.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 96939 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+980.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 97939 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+990.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 98939 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223728 134559424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 99940 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223728 134559356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 100940 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 101940 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 102940 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 103940 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 104941 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 105941 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 106941 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 107941 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 108941 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223728 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 109941 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 110942 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 111942 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134564496 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 112942 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 113942 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 114942 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 115943 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 116943 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223680 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 117943 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 118943 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 28609
Raw data (stat): 28609 (minisat+) R 28608 25285 25284 0 -1 0 24271 0 0 0 119943 73 0 0 25 0 1 0 486476494 101646336 24242 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24816 24242 603 41 0 24775 0
vsize: 99264
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 28609
Raw data (stat): 28609 (minisat+) Z 28608 25285 25284 0 -1 12 24274 0 0 0 119944 78 0 0 25 0 1 0 486476494 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.22
CPU user time (s): 1199.44
CPU system time (s): 0.780881
CPU usage (%): 100.011
Max. virtual memory (Kb): 99264
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####