PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-gt2.opb
MD5SUM	f1382105ee9fb79777762a53cf6a73c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	21166
Optimality of the best value was proved	NO
Number of terms in the objective function	304
Biggest coefficient in the objective function	62376
Number of bits for the biggest coefficient in the objective function	16
Sum of the numbers in the objective function	3092598
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	62376
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	3092598
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1177.34
Number of variables	556
Total number of constraints	217
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	26
Number of constraints which are nor clauses,nor cardinality constraints	191
Minimum length of a constraint	1
Maximum length of a constraint	48
Trace number 21340

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 23:27:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13452 boxname=wulflinc8 idbench=1035 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f1382105ee9fb79777762a53cf6a73c1  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-gt2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-gt2.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-gt2.opb
IDLAUNCH: 13452
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        645064 kB
Buffers:         25172 kB
Cached:         343116 kB
SwapCached:          0 kB
Active:         162936 kB
Inactive:       208272 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        644812 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            12804 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:47:02 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 13452 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................ssssssssss
c ---[ 189]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 188]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 187]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 186]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 185]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 184]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 183]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 182]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 157]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 156]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 155]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 154]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 153]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 152]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 151]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 150]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 149]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 148]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 147]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 146]---> Adder-cost: 6   maxlim: 6   bits: 4/3
c ---[ 141]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 140]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 139]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 138]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 137]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 136]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 135]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 134]---> Adder-cost: 7   maxlim: 2   bits: 3/2
c ---[ 120]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 119]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 117]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 113]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 110]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 106]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[ 103]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  99]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  98]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[  96]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  91]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[  89]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[  82]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[  75]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  70]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[  68]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  64]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  63]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[  61]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  56]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[  54]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[  47]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  43]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  42]---> Adder-cost: 4   maxlim: 5   bits: 4/3
c ---[  40]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 56   maxlim: 110   bits: 7/7
c ---[  36]---> Adder-cost: 88   maxlim: 164   bits: 8/8
c ---[  35]---> Adder-cost: 88   maxlim: 165   bits: 8/8
c ---[  34]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[  33]---> Adder-cost: 66   maxlim: 77   bits: 7/7
c ---[  32]---> Adder-cost: 88   maxlim: 171   bits: 8/8
c ---[  31]---> Adder-cost: 18   maxlim: 22   bits: 5/5
c ---[  30]---> Adder-cost: 56   maxlim: 107   bits: 7/7
c ---[  29]---> Adder-cost: 66   maxlim: 78   bits: 7/7
c ---[  28]---> Adder-cost: 66   maxlim: 77   bits: 7/7
c ---[  27]---> Adder-cost: 66   maxlim: 79   bits: 7/7
c ---[  26]---> Adder-cost: 88   maxlim: 170   bits: 8/8
c ---[  25]---> Adder-cost: 66   maxlim: 78   bits: 7/7
c ---[  24]---> Adder-cost: 66   maxlim: 79   bits: 7/7
c ---[  23]---> Adder-cost: 44   maxlim: 33   bits: 6/6
c ---[  22]---> Adder-cost: 44   maxlim: 33   bits: 6/6
c ---[  21]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[  15]---> Adder-cost: 273   maxlim: 12127   bits: 15/14
c ---[   9]---> Adder-cost: 202   maxlim: 199   bits: 9/8
c ---[   8]---> Adder-cost: 108   maxlim: 79   bits: 8/7
c ---[   7]---> Adder-cost: 232   maxlim: 299   bits: 10/9
c ---[   6]---> Adder-cost: 223   maxlim: 249   bits: 9/8
c ---[   5]---> Adder-cost: 98   maxlim: 121   bits: 8/7
c ---[   4]---> Adder-cost: 142   maxlim: 93   bits: 8/7
c ---[   3]---> Adder-cost: 112   maxlim: 66   bits: 8/7
c ---[   2]---> Adder-cost: 258   maxlim: 449   bits: 10/9
c ---[   1]---> Adder-cost: 212   maxlim: 230   bits: 9/8
c ---[   0]---> Adder-cost: 102   maxlim: 151   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   20147    71728 |    6715       0        0     nan |  0.000 % |
c |       100 |   20075    71480 |    7386      92      389     4.2 |  7.908 % |
c |       250 |   19961    71086 |    8125     225      969     4.3 |  8.413 % |
c |       475 |   19807    70569 |    8937     425     1963     4.6 |  9.096 % |
c |       812 |   19719    70270 |    9831     750     3967     5.3 |  9.474 % |
c |      1318 |   19587    69824 |   10814    1230     9158     7.4 | 10.056 % |
c |      2078 |   19489    69494 |   11896    1975    16921     8.6 | 10.460 % |
c |      3217 |   19401    69197 |   13085    3094    35741    11.6 | 10.839 % |
c |      4926 |   19107    68199 |   14394    4747    54508    11.5 | 12.077 % |
c |      7488 |   18986    67787 |   15833    7281    96891    13.3 | 12.557 % |
c ==============================================================================
c [1mFound solution: 261020[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3068   maxlim: 2831578   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9029 |   40265   143821 |   13421    8805   121720    13.8 | 12.557 % |
c |      9129 |   40265   143821 |   14763    8905   123754    13.9 |  7.431 % |
c |      9280 |   40265   143821 |   16239    9056   125631    13.9 |  7.431 % |
c |      9505 |   40265   143821 |   17863    9281   130267    14.0 |  7.431 % |
c |      9842 |   40265   143821 |   19649    9618   135668    14.1 |  7.431 % |
c |     10350 |   40265   143821 |   21614   10126   144973    14.3 |  7.431 % |
c |     11109 |   40265   143821 |   23776   10885   155367    14.3 |  7.431 % |
c |     12248 |   40265   143821 |   26153   12024   188047    15.6 |  7.431 % |
c |     13956 |   40219   143667 |   28769   13725   206905    15.1 |  7.545 % |
c |     16519 |   40219   143667 |   31646   16288   307561    18.9 |  7.545 % |
c ==============================================================================
c [1mFound solution: 215965[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2876633   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16800 |   40237   143796 |   13412   16569   314641    19.0 |  7.545 % |
c |     16900 |   40237   143796 |   14753    8385   172253    20.5 |  7.657 % |
c |     17050 |   40237   143796 |   16228    8535   173416    20.3 |  7.657 % |
c |     17277 |   40237   143796 |   17851    8762   176672    20.2 |  7.657 % |
c |     17614 |   40237   143796 |   19636    9099   181611    20.0 |  7.657 % |
c |     18120 |   40145   143463 |   21600    9599   185454    19.3 |  7.714 % |
c |     18880 |   40106   143321 |   23760   10355   200324    19.3 |  7.742 % |
c |     20019 |   39992   142922 |   26136   11484   214336    18.7 |  7.898 % |
c |     21727 |   39954   142793 |   28749   13182   235596    17.9 |  7.969 % |
c |     24289 |   39909   142634 |   31624   15729   290902    18.5 |  8.012 % |
c |     28134 |   39621   141618 |   34787   19548   508649    26.0 |  8.437 % |
c ==============================================================================
c [1mFound solution: 214552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2060   maxlim: 2769046   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28796 |   53886   192552 |   17962   20210   520309    25.7 |  8.437 % |
c |     28896 |   53869   192493 |   19758   10203   294676    28.9 |  6.700 % |
c |     29046 |   53869   192493 |   21734   10353   296346    28.6 |  6.700 % |
c |     29271 |   53869   192493 |   23907   10578   301212    28.5 |  6.700 % |
c |     29610 |   53869   192493 |   26298   10917   322071    29.5 |  6.700 % |
c |     30116 |   53869   192493 |   28927   11423   330839    29.0 |  6.700 % |
c |     30875 |   53812   192298 |   31820   12173   341462    28.1 |  6.798 % |
c |     32015 |   53770   192148 |   35002   13306   361449    27.2 |  6.820 % |
c |     33723 |   53770   192148 |   38503   15014   402891    26.8 |  6.820 % |
c |     36287 |   53646   191719 |   42353   17562   454661    25.9 |  6.974 % |
c ==============================================================================
c [1mFound solution: 186193[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2797405   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38845 |   53681   191945 |   17893   20120   521972    25.9 |  6.974 % |
c |     38946 |   53681   191945 |   19682   10161   175168    17.2 |  7.086 % |
c |     39096 |   53681   191945 |   21650   10311   177216    17.2 |  7.086 % |
c |     39321 |   53681   191945 |   23815   10536   182546    17.3 |  7.086 % |
c |     39659 |   53681   191945 |   26197   10874   191933    17.7 |  7.086 % |
c |     40166 |   53681   191945 |   28816   11381   209136    18.4 |  7.086 % |
c |     40925 |   53666   191892 |   31698   12137   220071    18.1 |  7.097 % |
c |     42064 |   53666   191892 |   34868   13276   249372    18.8 |  7.097 % |
c |     43773 |   53561   191523 |   38355   14972   273925    18.3 |  7.184 % |
c |     46335 |   53492   191284 |   42190   17523   346853    19.8 |  7.261 % |
c |     50179 |   53465   191187 |   46409   21363   479543    22.4 |  7.272 % |
c |     55945 |   53459   191167 |   51050   27128   835704    30.8 |  7.283 % |
c |     64596 |   53426   191054 |   56155   35774  1828828    51.1 |  7.305 % |
c ==============================================================================
c [1mFound solution: 167673[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2815925   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66662 |   53446   191217 |   17815   37840  1921797    50.8 |  7.305 % |
c |     66763 |   53446   191217 |   19596   16318  1128544    69.2 |  7.414 % |
c |     66913 |   53446   191217 |   21556   16468  1130254    68.6 |  7.414 % |
c |     67138 |   53446   191217 |   23711   16693  1132425    67.8 |  7.414 % |
c |     67475 |   53432   191169 |   26082   17026  1136929    66.8 |  7.447 % |
c |     67981 |   53418   191119 |   28691   17530  1146519    65.4 |  7.469 % |
c |     68741 |   53397   191044 |   31560   18285  1167392    63.8 |  7.479 % |
c |     69880 |   53376   190971 |   34716   19421  1184030    61.0 |  7.501 % |
c |     71588 |   53296   190691 |   38188   21114  1249659    59.2 |  7.611 % |
c |     74150 |   53296   190691 |   42006   23676  1339019    56.6 |  7.611 % |
c |     77996 |   53296   190691 |   46207   27522  1497448    54.4 |  7.611 % |
c |     83764 |   53296   190691 |   50828   33290  1720204    51.7 |  7.611 % |
c |     92416 |   53296   190691 |   55911   41942  2299474    54.8 |  7.611 % |
c |    105390 |   53281   190638 |   61502   54911  3334994    60.7 |  7.622 % |
c |    124851 |   53260   190565 |   67652   31424  2180777    69.4 |  7.644 % |
c |    154043 |   53138   190137 |   74417   60600  4926196    81.3 |  7.753 % |
c |    197832 |   53138   190137 |   81859   46024  4754761   103.3 |  7.753 % |
c ==============================================================================
c [1mFound solution: 166702[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2816896   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    225262 |   53121   190125 |   17707   73450  6981346    95.0 |  7.753 % |
c |    225362 |   53121   190125 |   19477   18494  1372013    74.2 |  7.835 % |
c |    225512 |   53121   190125 |   21425   18644  1373037    73.6 |  7.835 % |
c |    225739 |   53121   190125 |   23568   18871  1374664    72.8 |  7.835 % |
c |    226076 |   53121   190125 |   25924   19208  1378352    71.8 |  7.835 % |
c |    226582 |   53121   190125 |   28517   19714  1388763    70.4 |  7.835 % |
c |    227341 |   53121   190125 |   31369   20473  1408838    68.8 |  7.835 % |
c |    228480 |   53115   190105 |   34505   21610  1432642    66.3 |  7.846 % |
c |    230190 |   53115   190105 |   37956   23320  1465601    62.8 |  7.846 % |
c |    232752 |   53115   190105 |   41752   25882  1697433    65.6 |  7.846 % |
c ==============================================================================
c [1mFound solution: 166095[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2817503   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    234162 |   53120   190169 |   17706   27292  1735354    63.6 |  7.846 % |
c |    234262 |   53120   190169 |   19476   13746   433934    31.6 |  7.896 % |
c |    234412 |   53120   190169 |   21424   13896   435293    31.3 |  7.896 % |
c |    234638 |   53120   190169 |   23566   14122   444829    31.5 |  7.896 % |
c |    234976 |   53120   190169 |   25923   14460   448054    31.0 |  7.896 % |
c |    235482 |   53120   190169 |   28515   14966   462728    30.9 |  7.896 % |
c |    236242 |   53111   190138 |   31367   15722   471028    30.0 |  7.907 % |
c |    237381 |   53090   190065 |   34503   16845   501574    29.8 |  7.929 % |
c |    239089 |   53090   190065 |   37954   18553   558428    30.1 |  7.929 % |
c |    241651 |   53090   190065 |   41749   21115   673116    31.9 |  7.929 % |
c |    245497 |   53090   190065 |   45924   24961   878851    35.2 |  7.929 % |
c |    251263 |   53090   190065 |   50517   30727  1227769    40.0 |  7.929 % |
c |    259912 |   53090   190065 |   55569   39376  1713843    43.5 |  7.929 % |
c |    272886 |   53090   190065 |   61125   52350  3123669    59.7 |  7.929 % |
c |    292348 |   53090   190065 |   67238   27258  2252315    82.6 |  7.929 % |
c ==============================================================================
c [1mFound solution: 155894[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2827704   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    301398 |   53108   190205 |   17702   36308  2603696    71.7 |  7.929 % |
c |    301498 |   53108   190205 |   19472   18254   750652    41.1 |  8.015 % |
c |    301648 |   53108   190205 |   21419   18404   752038    40.9 |  8.015 % |
c |    301873 |   53108   190205 |   23561   18629   756364    40.6 |  8.015 % |
c |    302210 |   53108   190205 |   25917   18966   793790    41.9 |  8.015 % |
c |    302718 |   53108   190205 |   28509   19474   809326    41.6 |  8.015 % |
c |    303477 |   53108   190205 |   31360   20233   832254    41.1 |  8.015 % |
c |    304617 |   53108   190205 |   34496   21373   861927    40.3 |  8.015 % |
c |    306325 |   53108   190205 |   37945   23081  1040212    45.1 |  8.015 % |
c |    308888 |   53108   190205 |   41740   25644  1114297    43.5 |  8.015 % |
c |    312733 |   53108   190205 |   45914   29489  1304317    44.2 |  8.015 % |
c |    318500 |   53108   190205 |   50505   35256  1786777    50.7 |  8.015 % |
c |    327152 |   53108   190205 |   55556   43908  2363178    53.8 |  8.015 % |
c |    340126 |   53108   190205 |   61112   56882  3016699    53.0 |  8.015 % |
c ==============================================================================
c [1mFound solution: 152365[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2831233   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    357850 |   53106   190240 |   17702   29533  1496676    50.7 |  8.015 % |
c |    357950 |   53106   190240 |   19472   14867   776927    52.3 |  8.075 % |
c |    358100 |   53106   190240 |   21419   15017   777895    51.8 |  8.075 % |
c |    358326 |   53106   190240 |   23561   15243   780248    51.2 |  8.075 % |
c |    358664 |   53106   190240 |   25917   15581   783459    50.3 |  8.075 % |
c |    359171 |   53106   190240 |   28509   16088   792997    49.3 |  8.075 % |
c |    359930 |   53106   190240 |   31360   16847   806358    47.9 |  8.075 % |
c |    361069 |   53106   190240 |   34496   17986   828962    46.1 |  8.075 % |
c |    362777 |   53106   190240 |   37945   19694   873619    44.4 |  8.075 % |
c |    365340 |   53106   190240 |   41740   22257  1009356    45.4 |  8.075 % |
c |    369184 |   53106   190240 |   45914   26101  1145361    43.9 |  8.075 % |
c |    374950 |   53106   190240 |   50505   31867  1474589    46.3 |  8.075 % |
c |    383600 |   53106   190240 |   55556   40517  1865046    46.0 |  8.075 % |
c |    396574 |   53106   190240 |   61112   53491  3082073    57.6 |  8.075 % |
c |    416035 |   53106   190240 |   67223   26022  2774153   106.6 |  8.075 % |
c |    445227 |   53106   190240 |   73945   55214  6012742   108.9 |  8.075 % |
c |    489016 |   53071   190115 |   81340   41181  4009234    97.4 |  8.107 % |
c |    554701 |   53071   190115 |   89474   36163  2675323    74.0 |  8.107 % |
c ==============================================================================
c [1mFound solution: 141770[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2841828   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    569895 |   53074   190203 |   17691   51355  3371198    65.6 |  8.107 % |
c |    569996 |   53074   190203 |   19460   14831   661314    44.6 |  8.205 % |
c |    570147 |   53074   190203 |   21406   14982   662938    44.2 |  8.205 % |
c |    570372 |   53074   190203 |   23546   15207   665742    43.8 |  8.205 % |
c |    570709 |   53074   190203 |   25901   15544   668846    43.0 |  8.205 % |
c |    571216 |   53074   190203 |   28491   16051   675018    42.1 |  8.205 % |
c |    571975 |   53074   190203 |   31340   16810   682290    40.6 |  8.205 % |
c |    573114 |   53074   190203 |   34474   17949   702697    39.1 |  8.205 % |
c |    574822 |   53074   190203 |   37922   19657   737219    37.5 |  8.205 % |
c |    577386 |   53074   190203 |   41714   22221   889088    40.0 |  8.205 % |
c |    581230 |   53074   190203 |   45885   26065  1020087    39.1 |  8.205 % |
c |    586997 |   53074   190203 |   50474   31832  1532723    48.2 |  8.205 % |
c |    595647 |   53074   190203 |   55521   40482  2310115    57.1 |  8.205 % |
c |    608621 |   53074   190203 |   61074   53456  2730721    51.1 |  8.205 % |
c |    628082 |   53074   190203 |   67181   22249  3235867   145.4 |  8.205 % |
c |    657274 |   53074   190203 |   73899   51441  6460478   125.6 |  8.205 % |
c |    701063 |   53074   190203 |   81289   36975  2681901    72.5 |  8.205 % |
c ==============================================================================
c [1mFound solution: 137340[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2846258   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    716143 |   53088   190322 |   17696   52055  3858835    74.1 |  8.205 % |
c |    716243 |   53088   190322 |   19465    9695   312909    32.3 |  8.280 % |
c |    716394 |   53088   190322 |   21412    9846   313926    31.9 |  8.280 % |
c |    716619 |   53088   190322 |   23553   10071   316333    31.4 |  8.280 % |
c |    716957 |   53088   190322 |   25908   10409   320395    30.8 |  8.280 % |
c |    717463 |   53088   190322 |   28499   10915   326274    29.9 |  8.280 % |
c |    718225 |   53088   190322 |   31349   11677   361174    30.9 |  8.280 % |
c |    719364 |   53088   190322 |   34484   12816   402144    31.4 |  8.280 % |
c |    721074 |   53088   190322 |   37932   14526   456619    31.4 |  8.280 % |
c |    723637 |   53046   190172 |   41726   17076   535997    31.4 |  8.302 % |
c |    727481 |   53046   190172 |   45898   20920   752868    36.0 |  8.302 % |
c |    733247 |   53046   190172 |   50488   26686  1253977    47.0 |  8.302 % |
c |    741896 |   53046   190172 |   55537   35335  2139605    60.6 |  8.302 % |
c |    754871 |   53046   190172 |   61091   48310  3709051    76.8 |  8.302 % |
c |    774332 |   53046   190172 |   67200   22261  2519349   113.2 |  8.302 % |
c |    803524 |   53031   190119 |   73920   51450  4427267    86.0 |  8.313 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x_0x2e__0x2e__0x2e_0101_bit0 -x_0x2e__0x2e__0x2e_0101_bit1 -x_0x2e__0x2e__0x2e_0101_bit2 -x_0x2e__0x2e__0x2e_0101_bit3 x_0x2e__0x2e__0x2e_0201_bit0 -x_0x2e__0x2e__0x2e_0201_bit1 -x_0x2e__0x2e__0x2e_0201_bit2 -x_0x2e__0x2e__0x2e_0201_bit3 -x_0x2e__0x2e__0x2e_0301_bit0 x_0x2e__0x2e__0x2e_0301_bit1 -x_0x2e__0x2e__0x2e_0301_bit2 -x_0x2e__0x2e__0x2e_0301_bit3 -x_0x2e__0x2e__0x2e_0401_bit0 -x_0x2e__0x2e__0x2e_0401_bit1 -x_0x2e__0x2e__0x2e_0401_bit2 -x_0x2e__0x2e__0x2e_0401_bit3 -x_0x2e__0x2e__0x2e_0701_bit0 -x_0x2e__0x2e__0x2e_0701_bit1 -x_0x2e__0x2e__0x2e_0701_bit2 -x_0x2e__0x2e__0x2e_0701_bit3 -x_0x2e__0x2e__0x2e_0801_bit0 -x_0x2e__0x2e__0x2e_0801_bit1 -x_0x2e__0x2e__0x2e_0801_bit2 -x_0x2e__0x2e__0x2e_0801_bit3 x_0x2e__0x2e__0x2e_0901_bit0 x_0x2e__0x2e__0x2e_0901_bit1 -x_0x2e__0x2e__0x2e_0901_bit2 -x_0x2e__0x2e__0x2e_0901_bit3 -x_0x2e__0x2e__0x2e_1001_bit0 -x_0x2e__0x2e__0x2e_1001_bit1 -x_0x2e__0x2e__0x2e_1001_bit2 -x_0x2e__0x2e__0x2e_1001_bit3 x_0x2e__0x2e__0x2e_0102_bit0 -x_0x2e__0x2e__0x2e_0102_bit1 -x_0x2e__0x2e__0x2e_0102_bit2 -x_0x2e__0x2e__0x2e_0102_bit3 x_0x2e__0x2e__0x2e_0202_bit0 -x_0x2e__0x2e__0x2e_0202_bit1 -x_0x2e__0x2e__0x2e_0202_bit2 -x_0x2e__0x2e__0x2e_0202_bit3 -x_0x2e__0x2e__0x2e_0302_bit0 x_0x2e__0x2e__0x2e_0302_bit1 -x_0x2e__0x2e__0x2e_0302_bit2 -x_0x2e__0x2e__0x2e_0302_bit3 x_0x2e__0x2e__0x2e_0402_bit0 -x_0x2e__0x2e__0x2e_0402_bit1 -x_0x2e__0x2e__0x2e_0402_bit2 -x_0x2e__0x2e__0x2e_0402_bit3 -x_0x2e__0x2e__0x2e_0502_bit0 -x_0x2e__0x2e__0x2e_0502_bit1 -x_0x2e__0x2e__0x2e_0502_bit2 -x_0x2e__0x2e__0x2e_0502_bit3 -x_0x2e__0x2e__0x2e_0602_bit0 -x_0x2e__0x2e__0x2e_0602_bit1 -x_0x2e__0x2e__0x2e_0602_bit2 -x_0x2e__0x2e__0x2e_0602_bit3 -x_0x2e__0x2e__0x2e_0702_bit0 -x_0x2e__0x2e__0x2e_0702_bit1 -x_0x2e__0x2e__0x2e_0702_bit2 -x_0x2e__0x2e__0x2e_0702_bit3 x_0x2e__0x2e__0x2e_0802_bit0 -x_0x2e__0x2e__0x2e_0802_bit1 -x_0x2e__0x2e__0x2e_0802_bit2 -x_0x2e__0x2e__0x2e_0802_bit3 x_0x2e__0x2e__0x2e_0902_bit0 -x_0x2e__0x2e__0x2e_0902_bit1 -x_0x2e__0x2e__0x2e_0902_bit2 -x_0x2e__0x2e__0x2e_0902_bit3 x_0x2e__0x2e__0x2e_1002_bit0 -x_0x2e__0x2e__0x2e_1002_bit1 -x_0x2e__0x2e__0x2e_1002_bit2 -x_0x2e__0x2e__0x2e_1002_bit3 -x_0x2e__0x2e__0x2e_1102_bit0 -x_0x2e__0x2e__0x2e_1102_bit1 x_0x2e__0x2e__0x2e_1102_bit2 -x_0x2e__0x2e__0x2e_1102_bit3 -x_0x2e__0x2e__0x2e_1202_bit0 -x_0x2e__0x2e__0x2e_1202_bit1 -x_0x2e__0x2e__0x2e_1202_bit2 -x_0x2e__0x2e__0x2e_1202_bit3 -x_0x2e__0x2e__0x2e_0103_bit0 -x_0x2e__0x2e__0x2e_0103_bit1 -x_0x2e__0x2e__0x2e_0103_bit2 -x_0x2e__0x2e__0x2e_0103_bit3 -x_0x2e__0x2e__0x2e_0203_bit0 -x_0x2e__0x2e__0x2e_0203_bit1 -x_0x2e__0x2e__0x2e_0203_bit2 -x_0x2e__0x2e__0x2e_0203_bit3 x_0x2e__0x2e__0x2e_0303_bit0 -x_0x2e__0x2e__0x2e_0303_bit1 -x_0x2e__0x2e__0x2e_0303_bit2 -x_0x2e__0x2e__0x2e_0303_bit3 -x_0x2e__0x2e__0x2e_0403_bit0 x_0x2e__0x2e__0x2e_0403_bit1 -x_0x2e__0x2e__0x2e_0403_bit2 -x_0x2e__0x2e__0x2e_0403_bit3 x_0x2e__0x2e__0x2e_0503_bit0 -x_0x2e__0x2e__0x2e_0503_bit1 -x_0x2e__0x2e__0x2e_0503_bit2 -x_0x2e__0x2e__0x2e_0503_bit3 -x_0x2e__0x2e__0x2e_0603_bit0 -x_0x2e__0x2e__0x2e_0603_bit1 -x_0x2e__0x2e__0x2e_0603_bit2 -x_0x2e__0x2e__0x2e_0603_bit3 x_0x2e__0x2e__0x2e_0703_bit0 -x_0x2e__0x2e__0x2e_0703_bit1 -x_0x2e__0x2e__0x2e_0703_bit2 -x_0x2e__0x2e__0x2e_0703_bit3 -x_0x2e__0x2e__0x2e_0803_bit0 x_0x2e__0x2e__0x2e_0803_bit1 -x_0x2e__0x2e__0x2e_0803_bit2 -x_0x2e__0x2e__0x2e_0803_bit3 -x_0x2e__0x2e__0x2e_0903_bit0 x_0x2e__0x2e__0x2e_0903_bit1 -x_0x2e__0x2e__0x2e_0903_bit2 -x_0x2e__0x2e__0x2e_0903_bit3 x_0x2e__0x2e__0x2e_1003_bit0 -x_0x2e__0x2e__0x2e_1003_bit1 -x_0x2e__0x2e__0x2e_1003_bit2 -x_0x2e__0x2e__0x2e_1003_bit3 x_0x2e__0x2e__0x2e_1103_bit0 x_0x2e__0x2e__0x2e_1103_bit1 -x_0x2e__0x2e__0x2e_1103_bit2 -x_0x2e__0x2e__0x2e_1103_bit3 -x_0x2e__0x2e__0x2e_1203_bit0 -x_0x2e__0x2e__0x2e_1203_bit1 -x_0x2e__0x2e__0x2e_1203_bit2 -x_0x2e__0x2e__0x2e_1203_bit3 -x_0x2e__0x2e__0x2e_0104_bit0 x_0x2e__0x2e__0x2e_0204_bit0 -x_0x2e__0x2e__0x2e_0304_bit0 -x_0x2e__0x2e__0x2e_0404_bit0 -x_0x2e__0x2e__0x2e_0504_bit0 -x_0x2e__0x2e__0x2e_0604_bit0 -x_0x2e__0x2e__0x2e_0704_bit0 -x_0x2e__0x2e__0x2e_0804_bit0 -x_0x2e__0x2e__0x2e_0904_bit0 -x_0x2e__0x2e__0x2e_1004_bit0 -x_0x2e__0x2e__0x2e_1104_bit0 -x_0x2e__0x2e__0x2e_1204_bit0 -x_0x2e__0x2e__0x2e_0105_bit0 x_0x2e__0x2e__0x2e_0105_bit1 -x_0x2e__0x2e__0x2e_0105_bit2 x_0x2e__0x2e__0x2e_0205_bit0 x_0x2e__0x2e__0x2e_0205_bit1 -x_0x2e__0x2e__0x2e_0205_bit2 -x_0x2e__0x2e__0x2e_0305_bit0 -x_0x2e__0x2e__0x2e_0305_bit1 -x_0x2e__0x2e__0x2e_0305_bit2 x_0x2e__0x2e__0x2e_0405_bit0 -x_0x2e__0x2e__0x2e_0405_bit1 -x_0x2e__0x2e__0x2e_0405_bit2 -x_0x2e__0x2e__0x2e_0505_bit0 -x_0x2e__0x2e__0x2e_0505_bit1 -x_0x2e__0x2e__0x2e_0505_bit2 -x_0x2e__0x2e__0x2e_0605_bit0 -x_0x2e__0x2e__0x2e_0605_bit1 -x_0x2e__0x2e__0x2e_0605_bit2 -x_0x2e__0x2e__0x2e_0705_bit0 -x_0x2e__0x2e__0x2e_0705_bit1 -x_0x2e__0x2e__0x2e_0705_bit2 -x_0x2e__0x2e__0x2e_0805_bit0 -x_0x2e__0x2e__0x2e_0805_bit1 -x_0x2e__0x2e__0x2e_0805_bit2 -x_0x2e__0x2e__0x2e_0905_bit0 -x_0x2e__0x2e__0x2e_0905_bit1 -x_0x2e__0x2e__0x2e_0905_bit2 -x_0x2e__0x2e__0x2e_1005_bit0 -x_0x2e__0x2e__0x2e_1005_bit1 -x_0x2e__0x2e__0x2e_1005_bit2 -x_0x2e__0x2e__0x2e_1105_bit0 -x_0x2e__0x2e__0x2e_1105_bit1 -x_0x2e__0x2e__0x2e_1105_bit2 -x_0x2e__0x2e__0x2e_1205_bit0 -x_0x2e__0x2e__0x2e_1205_bit1 -x_0x2e__0x2e__0x2e_1205_bit2 -x_0x2e__0x2e__0x2e_0106_bit0 -x_0x2e__0x2e__0x2e_0106_bit1 -x_0x2e__0x2e__0x2e_0106_bit2 -x_0x2e__0x2e__0x2e_0106_bit3 x_0x2e__0x2e__0x2e_0206_bit0 -x_0x2e__0x2e__0x2e_0206_bit1 -x_0x2e__0x2e__0x2e_0206_bit2 -x_0x2e__0x2e__0x2e_0206_bit3 -x_0x2e__0x2e__0x2e_0306_bit0 x_0x2e__0x2e__0x2e_0306_bit1 -x_0x2e__0x2e__0x2e_0306_bit2 -x_0x2e__0x2e__0x2e_0306_bit3 -x_0x2e__0x2e__0x2e_0406_bit0 -x_0x2e__0x2e__0x2e_0406_bit1 -x_0x2e__0x2e__0x2e_0406_bit2 -x_0x2e__0x2e__0x2e_0406_bit3 -x_0x2e__0x2e__0x2e_0506_bit0 -x_0x2e__0x2e__0x2e_0506_bit1 -x_0x2e__0x2e__0x2e_0506_bit2 -x_0x2e__0x2e__0x2e_0506_bit3 -x_0x2e__0x2e__0x2e_0606_bit0 -x_0x2e__0x2e__0x2e_0606_bit1 -x_0x2e__0x2e__0x2e_0606_bit2 -x_0x2e__0x2e__0x2e_0606_bit3 -x_0x2e__0x2e__0x2e_0706_bit0 -x_0x2e__0x2e__0x2e_0706_bit1 -x_0x2e__0x2e__0x2e_0706_bit2 -x_0x2e__0x2e__0x2e_0706_bit3 -x_0x2e__0x2e__0x2e_0806_bit0 -x_0x2e__0x2e__0x2e_0806_bit1 -x_0x2e__0x2e__0x2e_0806_bit2 -x_0x2e__0x2e__0x2e_0806_bit3 x_0x2e__0x2e__0x2e_0906_bit0 x_0x2e__0x2e__0x2e_0906_bit1 -x_0x2e__0x2e__0x2e_0906_bit2 -x_0x2e__0x2e__0x2e_0906_bit3 -x_0x2e__0x2e__0x2e_1006_bit0 -x_0x2e__0x2e__0x2e_1006_bit1 -x_0x2e__0x2e__0x2e_1006_bit2 -x_0x2e__0x2e__0x2e_1006_bit3 -x_0x2e__0x2e__0x2e_1106_bit0 -x_0x2e__0x2e__0x2e_1106_bit1 -x_0x2e__0x2e__0x2e_1106_bit2 -x_0x2e__0x2e__0x2e_1106_bit3 -x_0x2e__0x2e__0x2e_1206_bit0 -x_0x2e__0x2e__0x2e_1206_bit1 -x_0x2e__0x2e__0x2e_1206_bit2 -x_0x2e__0x2e__0x2e_1206_bit3 -x_0x2e__0x2e__0x2e_0507_bit0 -x_0x2e__0x2e__0x2e_0507_bit1 -x_0x2e__0x2e__0x2e_0507_bit2 -x_0x2e__0x2e__0x2e_0607_bit0 -x_0x2e__0x2e__0x2e_0607_bit1 -x_0x2e__0x2e__0x2e_0607_bit2 -x_0x2e__0x2e__0x2e_1107_bit0 -x_0x2e__0x2e__0x2e_1107_bit1 -x_0x2e__0x2e__0x2e_1107_bit2 -x_0x2e__0x2e__0x2e_1207_bit0 -x_0x2e__0x2e__0x2e_1207_bit1 -x_0x2e__0x2e__0x2e_1207_bit2 x_0x2e__0x2e__0x2e_0108_bit0 -x_0x2e__0x2e__0x2e_0108_bit1 -x_0x2e__0x2e__0x2e_0108_bit2 -x_0x2e__0x2e__0x2e_0108_bit3 x_0x2e__0x2e__0x2e_0208_bit0 -x_0x2e__0x2e__0x2e_0208_bit1 -x_0x2e__0x2e__0x2e_0208_bit2 -x_0x2e__0x2e__0x2e_0208_bit3 -x_0x2e__0x2e__0x2e_0308_bit0 x_0x2e__0x2e__0x2e_0308_bit1 -x_0x2e__0x2e__0x2e_0308_bit2 -x_0x2e__0x2e__0x2e_0308_bit3 x_0x2e__0x2e__0x2e_0408_bit0 -x_0x2e__0x2e__0x2e_0408_bit1 -x_0x2e__0x2e__0x2e_0408_bit2 -x_0x2e__0x2e__0x2e_0408_bit3 -x_0x2e__0x2e__0x2e_0708_bit0 -x_0x2e__0x2e__0x2e_0708_bit1 -x_0x2e__0x2e__0x2e_0708_bit2 -x_0x2e__0x2e__0x2e_0708_bit3 -x_0x2e__0x2e__0x2e_0808_bit0 -x_0x2e__0x2e__0x2e_0808_bit1 -x_0x2e__0x2e__0x2e_0808_bit2 -x_0x2e__0x2e__0x2e_0808_bit3 -x_0x2e__0x2e__0x2e_0908_bit0 -x_0x2e__0x2e__0x2e_0908_bit1 -x_0x2e__0x2e__0x2e_0908_bit2 -x_0x2e__0x2e__0x2e_0908_bit3 -x_0x2e__0x2e__0x2e_1008_bit0 -x_0x2e__0x2e__0x2e_1008_bit1 -x_0x2e__0x2e__0x2e_1008_bit2 -x_0x2e__0x2e__0x2e_1008_bit3 -x_0x2e__0x2e__0x2e_0109_bit0 -x_0x2e__0x2e__0x2e_0109_bit1 -x_0x2e__0x2e__0x2e_0109_bit2 -x_0x2e__0x2e__0x2e_0209_bit0 -x_0x2e__0x2e__0x2e_0209_bit1 -x_0x2e__0x2e__0x2e_0209_bit2 -x_0x2e__0x2e__0x2e_0309_bit0 -x_0x2e__0x2e__0x2e_0309_bit1 -x_0x2e__0x2e__0x2e_0309_bit2 -x_0x2e__0x2e__0x2e_0409_bit0 -x_0x2e__0x2e__0x2e_0409_bit1 -x_0x2e__0x2e__0x2e_0409_bit2 -x_0x2e__0x2e__0x2e_0509_bit0 -x_0x2e__0x2e__0x2e_0509_bit1 -x_0x2e__0x2e__0x2e_0509_bit2 -x_0x2e__0x2e__0x2e_0609_bit0 -x_0x2e__0x2e__0x2e_0609_bit1 x_0x2e__0x2e__0x2e_0609_bit2 -x_0x2e__0x2e__0x2e_0709_bit0 -x_0x2e__0x2e__0x2e_0709_bit1 -x_0x2e__0x2e__0x2e_0709_bit2 -x_0x2e__0x2e__0x2e_0809_bit0 -x_0x2e__0x2e__0x2e_0809_bit1 -x_0x2e__0x2e__0x2e_0809_bit2 -x_0x2e__0x2e__0x2e_0909_bit0 -x_0x2e__0x2e__0x2e_0909_bit1 -x_0x2e__0x2e__0x2e_0909_bit2 -x_0x2e__0x2e__0x2e_1009_bit0 -x_0x2e__0x2e__0x2e_1009_bit1 -x_0x2e__0x2e__0x2e_1009_bit2 -x_0x2e__0x2e__0x2e_1109_bit0 -x_0x2e__0x2e__0x2e_1109_bit1 -x_0x2e__0x2e__0x2e_1109_bit2 x_0x2e__0x2e__0x2e_1209_bit0 -x_0x2e__0x2e__0x2e_1209_bit1 -x_0x2e__0x2e__0x2e_1209_bit2 -x_0x2e__0x2e__0x2e_0110_bit0 -x_0x2e__0x2e__0x2e_0110_bit1 -x_0x2e__0x2e__0x2e_0110_bit2 -x_0x2e__0x2e__0x2e_0111_bit0 -x_0x2e__0x2e__0x2e_0111_bit1 -x_0x2e__0x2e__0x2e_0111_bit2 -x_0x2e__0x2e__0x2e_0112_bit0 -x_0x2e__0x2e__0x2e_0112_bit1 -x_0x2e__0x2e__0x2e_0112_bit2 -x_0x2e__0x2e__0x2e_0112_bit3 -x_0x2e__0x2e__0x2e_0113_bit0 -x_0x2e__0x2e__0x2e_0113_bit1 -x_0x2e__0x2e__0x2e_0113_bit2 -x_0x2e__0x2e__0x2e_0114_bit0 -x_0x2e__0x2e__0x2e_0114_bit1 x_0x2e__0x2e__0x2e_0114_bit2 -x_0x2e__0x2e__0x2e_0115_bit0 -x_0x2e__0x2e__0x2e_0115_bit1 -x_0x2e__0x2e__0x2e_0116_bit0 -x_0x2e__0x2e__0x2e_0116_bit1 -x_0x2e__0x2e__0x2e_0117_bit0 -x_0x2e__0x2e__0x2e_0210_bit0 -x_0x2e__0x2e__0x2e_0210_bit1 -x_0x2e__0x2e__0x2e_0210_bit2 -x_0x2e__0x2e__0x2e_0211_bit0 -x_0x2e__0x2e__0x2e_0211_bit1 -x_0x2e__0x2e__0x2e_0211_bit2 x_0x2e__0x2e__0x2e_0212_bit0 -x_0x2e__0x2e__0x2e_0212_bit1 -x_0x2e__0x2e__0x2e_0212_bit2 -x_0x2e__0x2e__0x2e_0212_bit3 -x_0x2e__0x2e__0x2e_0213_bit0 -x_0x2e__0x2e__0x2e_0213_bit1 -x_0x2e__0x2e__0x2e_0213_bit2 -x_0x2e__0x2e__0x2e_0214_bit0 -x_0x2e__0x2e__0x2e_0214_bit1 -x_0x2e__0x2e__0x2e_0214_bit2 -x_0x2e__0x2e__0x2e_0215_bit0 -x_0x2e__0x2e__0x2e_0215_bit1 -x_0x2e__0x2e__0x2e_0216_bit0 -x_0x2e__0x2e__0x2e_0216_bit1 -x_0x2e__0x2e__0x2e_0217_bit0 -x_0x2e__0x2e__0x2e_0310_bit0 -x_0x2e__0x2e__0x2e_0310_bit1 -x_0x2e__0x2e__0x2e_0310_bit2 -x_0x2e__0x2e__0x2e_0311_bit0 -x_0x2e__0x2e__0x2e_0311_bit1 -x_0x2e__0x2e__0x2e_0311_bit2 -x_0x2e__0x2e__0x2e_0312_bit0 -x_0x2e__0x2e__0x2e_0312_bit1 -x_0x2e__0x2e__0x2e_0312_bit2 -x_0x2e__0x2e__0x2e_0312_bit3 -x_0x2e__0x2e__0x2e_0313_bit0 -x_0x2e__0x2e__0x2e_0313_bit1 -x_0x2e__0x2e__0x2e_0313_bit2 -x_0x2e__0x2e__0x2e_0314_bit0 -x_0x2e__0x2e__0x2e_0314_bit1 -x_0x2e__0x2e__0x2e_0314_bit2 -x_0x2e__0x2e__0x2e_0315_bit0 -x_0x2e__0x2e__0x2e_0315_bit1 -x_0x2e__0x2e__0x2e_0316_bit0 -x_0x2e__0x2e__0x2e_0316_bit1 -x_0x2e__0x2e__0x2e_0317_bit0 -x_0x2e__0x2e__0x2e_0410_bit0 x_0x2e__0x2e__0x2e_0410_bit1 -x_0x2e__0x2e__0x2e_0410_bit2 x_0x2e__0x2e__0x2e_0411_bit0 -x_0x2e__0x2e__0x2e_0411_bit1 -x_0x2e__0x2e__0x2e_0411_bit2 -x_0x2e__0x2e__0x2e_0412_bit0 -x_0x2e__0x2e__0x2e_0412_bit1 x_0x2e__0x2e__0x2e_0412_bit2 -x_0x2e__0x2e__0x2e_0412_bit3 -x_0x2e__0x2e__0x2e_0413_bit0 -x_0x2e__0x2e__0x2e_0413_bit1 -x_0x2e__0x2e__0x2e_0413_bit2 -x_0x2e__0x2e__0x2e_0414_bit0 -x_0x2e__0x2e__0x2e_0414_bit1 -x_0x2e__0x2e__0x2e_0414_bit2 -x_0x2e__0x2e__0x2e_0415_bit0 -x_0x2e__0x2e__0x2e_0415_bit1 x_0x2e__0x2e__0x2e_0416_bit0 -x_0x2e__0x2e__0x2e_0416_bit1 -x_0x2e__0x2e__0x2e_0417_bit0 -x_0x2e__0x2e__0x2e_0510_bit0 -x_0x2e__0x2e__0x2e_0510_bit1 -x_0x2e__0x2e__0x2e_0510_bit2 -x_0x2e__0x2e__0x2e_0511_bit0 -x_0x2e__0x2e__0x2e_0511_bit1 -x_0x2e__0x2e__0x2e_0511_bit2 x_0x2e__0x2e__0x2e_0512_bit0 -x_0x2e__0x2e__0x2e_0512_bit1 -x_0x2e__0x2e__0x2e_0512_bit2 -x_0x2e__0x2e__0x2e_0512_bit3 -x_0x2e__0x2e__0x2e_0513_bit0 -x_0x2e__0x2e__0x2e_0513_bit1 -x_0x2e__0x2e__0x2e_0513_bit2 -x_0x2e__0x2e__0x2e_0514_bit0 -x_0x2e__0x2e__0x2e_0514_bit1 -x_0x2e__0x2e__0x2e_0514_bit2 -x_0x2e__0x2e__0x2e_0515_bit0 -x_0x2e__0x2e__0x2e_0515_bit1 -x_0x2e__0x2e__0x2e_0516_bit0 -x_0x2e__0x2e__0x2e_0516_bit1 -x_0x2e__0x2e__0x2e_0517_bit0 -x_0x2e__0x2e__0x2e_0610_bit0 -x_0x2e__0x2e__0x2e_0610_bit1 -x_0x2e__0x2e__0x2e_0610_bit2 -x_0x2e__0x2e__0x2e_0611_bit0 -x_0x2e__0x2e__0x2e_0611_bit1 -x_0x2e__0x2e__0x2e_0611_bit2 x_0x2e__0x2e__0x2e_0612_bit0 -x_0x2e__0x2e__0x2e_0612_bit1 -x_0x2e__0x2e__0x2e_0612_bit2 -x_0x2e__0x2e__0x2e_0612_bit3 -x_0x2e__0x2e__0x2e_0613_bit0 -x_0x2e__0x2e__0x2e_0613_bit1 -x_0x2e__0x2e__0x2e_0613_bit2 -x_0x2e__0x2e__0x2e_0614_bit0 -x_0x2e__0x2e__0x2e_0614_bit1 -x_0x2e__0x2e__0x2e_0614_bit2 -x_0x2e__0x2e__0x2e_0615_bit0 -x_0x2e__0x2e__0x2e_0615_bit1 -x_0x2e__0x2e__0x2e_0616_bit0 -x_0x2e__0x2e__0x2e_0616_bit1 -x_0x2e__0x2e__0x2e_0617_bit0 -x_0x2e__0x2e__0x2e_0710_bit0 -x_0x2e__0x2e__0x2e_0710_bit1 -x_0x2e__0x2e__0x2e_0710_bit2 -x_0x2e__0x2e__0x2e_0711_bit0 x_0x2e__0x2e__0x2e_0711_bit1 -x_0x2e__0x2e__0x2e_0711_bit2 -x_0x2e__0x2e__0x2e_0712_bit0 -x_0x2e__0x2e__0x2e_0712_bit1 -x_0x2e__0x2e__0x2e_0712_bit2 -x_0x2e__0x2e__0x2e_0712_bit3 -x_0x2e__0x2e__0x2e_0713_bit0 x_0x2e__0x2e__0x2e_0713_bit1 -x_0x2e__0x2e__0x2e_0713_bit2 -x_0x2e__0x2e__0x2e_0714_bit0 -x_0x2e__0x2e__0x2e_0714_bit1 -x_0x2e__0x2e__0x2e_0714_bit2 -x_0x2e__0x2e__0x2e_0715_bit0 -x_0x2e__0x2e__0x2e_0715_bit1 -x_0x2e__0x2e__0x2e_0716_bit0 -x_0x2e__0x2e__0x2e_0716_bit1 -x_0x2e__0x2e__0x2e_0717_bit0 -x_0x2e__0x2e__0x2e_0810_bit0 -x_0x2e__0x2e__0x2e_0810_bit1 -x_0x2e__0x2e__0x2e_0810_bit2 -x_0x2e__0x2e__0x2e_0811_bit0 -x_0x2e__0x2e__0x2e_0811_bit1 -x_0x2e__0x2e__0x2e_0811_bit2 -x_0x2e__0x2e__0x2e_0812_bit0 -x_0x2e__0x2e__0x2e_0812_bit1 -x_0x2e__0x2e__0x2e_0812_bit2 -x_0x2e__0x2e__0x2e_0812_bit3 -x_0x2e__0x2e__0x2e_0813_bit0 x_0x2e__0x2e__0x2e_0813_bit1 -x_0x2e__0x2e__0x2e_0813_bit2 -x_0x2e__0x2e__0x2e_0814_bit0 -x_0x2e__0x2e__0x2e_0814_bit1 -x_0x2e__0x2e__0x2e_0814_bit2 -x_0x2e__0x2e__0x2e_0815_bit0 -x_0x2e__0x2e__0x2e_0815_bit1 -x_0x2e__0x2e__0x2e_0816_bit0 -x_0x2e__0x2e__0x2e_0816_bit1 -x_0x2e__0x2e__0x2e_0817_bit0 -x_0x2e__0x2e__0x2e_0910_bit0 x_0x2e__0x2e__0x2e_0910_bit1 -x_0x2e__0x2e__0x2e_0910_bit2 x_0x2e__0x2e__0x2e_0911_bit0 -x_0x2e__0x2e__0x2e_0911_bit1 -x_0x2e__0x2e__0x2e_0911_bit2 -x_0x2e__0x2e__0x2e_0912_bit0 -x_0x2e__0x2e__0x2e_0912_bit1 -x_0x2e__0x2e__0x2e_0912_bit2 -x_0x2e__0x2e__0x2e_0912_bit3 -x_0x2e__0x2e__0x2e_0913_bit0 -x_0x2e__0x2e__0x2e_0913_bit1 -x_0x2e__0x2e__0x2e_0913_bit2 -x_0x2e__0x2e__0x2e_0914_bit0 -x_0x2e__0x2e__0x2e_0914_bit1 -x_0x2e__0x2e__0x2e_0914_bit2 -x_0x2e__0x2e__0x2e_0915_bit0 x_0x2e__0x2e__0x2e_0915_bit1 -x_0x2e__0x2e__0x2e_0916_bit0 -x_0x2e__0x2e__0x2e_0916_bit1 x_0x2e__0x2e__0x2e_0917_bit0 -x_0x2e__0x2e__0x2e_1010_bit0 x_0x2e__0x2e__0x2e_1010_bit1 -x_0x2e__0x2e__0x2e_1010_bit2 -x_0x2e__0x2e__0x2e_1011_bit0 -x_0x2e__0x2e__0x2e_1011_bit1 -x_0x2e__0x2e__0x2e_1011_bit2 -x_0x2e__0x2e__0x2e_1012_bit0 x_0x2e__0x2e__0x2e_1012_bit1 -x_0x2e__0x2e__0x2e_1012_bit2 -x_0x2e__0x2e__0x2e_1012_bit3 x_0x2e__0x2e__0x2e_1013_bit0 -x_0x2e__0x2e__0x2e_1013_bit1 -x_0x2e__0x2e__0x2e_1013_bit2 -x_0x2e__0x2e__0x2e_1014_bit0 -x_0x2e__0x2e__0x2e_1014_bit1 -x_0x2e__0x2e__0x2e_1014_bit2 -x_0x2e__0x2e__0x2e_1015_bit0 -x_0x2e__0x2e__0x2e_1015_bit1 x_0x2e__0x2e__0x2e_1016_bit0 -x_0x2e__0x2e__0x2e_1016_bit1 -x_0x2e__0x2e__0x2e_1017_bit0 -x_0x2e__0x2e__0x2e_1110_bit0 -x_0x2e__0x2e__0x2e_1110_bit1 -x_0x2e__0x2e__0x2e_1110_bit2 -x_0x2e__0x2e__0x2e_1111_bit0 -x_0x2e__0x2e__0x2e_1111_bit1 -x_0x2e__0x2e__0x2e_1111_bit2 -x_0x2e__0x2e__0x2e_1112_bit0 -x_0x2e__0x2e__0x2e_1112_bit1 -x_0x2e__0x2e__0x2e_1112_bit2 -x_0x2e__0x2e__0x2e_1112_bit3 -x_0x2e__0x2e__0x2e_1113_bit0 -x_0x2e__0x2e__0x2e_1113_bit1 -x_0x2e__0x2e__0x2e_1113_bit2 -x_0x2e__0x2e__0x2e_1114_bit0 -x_0x2e__0x2e__0x2e_1114_bit1 -x_0x2e__0x2e__0x2e_1114_bit2 -x_0x2e__0x2e__0x2e_1115_bit0 -x_0x2e__0x2e__0x2e_1115_bit1 -x_0x2e__0x2e__0x2e_1116_bit0 -x_0x2e__0x2e__0x2e_1116_bit1 -x_0x2e__0x2e__0x2e_1117_bit0 -x_0x2e__0x2e__0x2e_1210_bit0 -x_0x2e__0x2e__0x2e_1210_bit1 -x_0x2e__0x2e__0x2e_1210_bit2 -x_0x2e__0x2e__0x2e_1211_bit0 -x_0x2e__0x2e__0x2e_1211_bit1 -x_0x2e__0x2e__0x2e_1211_bit2 -x_0x2e__0x2e__0x2e_1212_bit0 -x_0x2e__0x2e__0x2e_1212_bit1 -x_0x2e__0x2e__0x2e_1212_bit2 -x_0x2e__0x2e__0x2e_1212_bit3 -x_0x2e__0x2e__0x2e_1213_bit0 -x_0x2e__0x2e__0x2e#### 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.85 0.94 0.90 2/54 9841
Raw data (stat): 9841 (runsolver) R 9840 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 477246644 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 1550 0 0 0 995 3 0 0 25 0 1 0 477246644 8085504 1528 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1974 1528 603 41 0 1933 0
vsize: 7896
[startup+20.0021 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 2036 0 0 0 1993 5 0 0 25 0 1 0 477246644 10399744 2014 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2539 2014 603 41 0 2498 0
vsize: 10156
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 2101 0 0 0 2992 5 0 0 25 0 1 0 477246644 10670080 2079 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2605 2079 603 41 0 2564 0
vsize: 10420
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 2591 0 0 0 3991 7 0 0 25 0 1 0 477246644 12689408 2569 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3098 2569 603 41 0 3057 0
vsize: 12392
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 3695 0 0 0 4988 9 0 0 25 0 1 0 477246644 17248256 3673 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4211 3673 603 41 0 4170 0
vsize: 16844
[startup+60.002 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 3695 0 0 0 5988 10 0 0 25 0 1 0 477246644 17248256 3673 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4211 3673 603 41 0 4170 0
vsize: 16844
[startup+70.0027 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 3730 0 0 0 6988 10 0 0 25 0 1 0 477246644 17383424 3708 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4244 3708 603 41 0 4203 0
vsize: 16976
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 4327 0 0 0 7986 12 0 0 25 0 1 0 477246644 19808256 4305 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4836 4305 603 41 0 4795 0
vsize: 19344
[startup+90.0032 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 4931 0 0 0 8984 14 0 0 25 0 1 0 477246644 22228992 4909 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5427 4909 603 41 0 5386 0
vsize: 21708
[startup+100.003 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 5478 0 0 0 9983 15 0 0 25 0 1 0 477246644 24510464 5456 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5984 5456 603 41 0 5943 0
vsize: 23936
[startup+110.003 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 5943 0 0 0 10982 17 0 0 25 0 1 0 477246644 26398720 5921 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6445 5921 603 41 0 6404 0
vsize: 25780
[startup+120.004 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 6042 0 0 0 11982 17 0 0 25 0 1 0 477246644 26804224 6020 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6544 6020 603 41 0 6503 0
vsize: 26176
[startup+130.003 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 6042 0 0 0 12982 17 0 0 25 0 1 0 477246644 26804224 6020 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6544 6020 603 41 0 6503 0
vsize: 26176
[startup+140.003 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 6042 0 0 0 13982 17 0 0 25 0 1 0 477246644 26804224 6020 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6544 6020 603 41 0 6503 0
vsize: 26176
[startup+150.004 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 6042 0 0 0 14982 17 0 0 25 0 1 0 477246644 26804224 6020 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6544 6020 603 41 0 6503 0
vsize: 26176
[startup+160.004 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 6374 0 0 0 15981 18 0 0 25 0 1 0 477246644 28139520 6352 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6352 603 41 0 6829 0
vsize: 27480
[startup+170.004 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 6865 0 0 0 16981 19 0 0 25 0 1 0 477246644 30150656 6843 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7361 6843 603 41 0 7320 0
vsize: 29444
[startup+180.004 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 7308 0 0 0 17979 21 0 0 25 0 1 0 477246644 32026624 7286 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7819 7286 603 41 0 7778 0
vsize: 31276
[startup+190.004 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 7894 0 0 0 18978 22 0 0 25 0 1 0 477246644 34578432 7872 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8442 7872 603 41 0 8401 0
vsize: 33768
[startup+200.004 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 8410 0 0 0 19977 23 0 0 25 0 1 0 477246644 36728832 8388 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8967 8388 603 41 0 8926 0
vsize: 35868
[startup+210.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9059 0 0 0 20974 26 0 0 25 0 1 0 477246644 39415808 9037 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9623 9037 603 41 0 9582 0
vsize: 38492
[startup+220.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9213 0 0 0 21974 26 0 0 25 0 1 0 477246644 39956480 9191 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 9191 603 41 0 9714 0
vsize: 39020
[startup+230.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9213 0 0 0 22974 26 0 0 25 0 1 0 477246644 39956480 9191 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 9191 603 41 0 9714 0
vsize: 39020
[startup+240.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9213 0 0 0 23975 26 0 0 25 0 1 0 477246644 39956480 9191 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 9191 603 41 0 9714 0
vsize: 39020
[startup+250.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9213 0 0 0 24975 26 0 0 25 0 1 0 477246644 39956480 9191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 9191 603 41 0 9714 0
vsize: 39020
[startup+260.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9213 0 0 0 25975 26 0 0 25 0 1 0 477246644 39956480 9191 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 9191 603 41 0 9714 0
vsize: 39020
[startup+270.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9213 0 0 0 26975 26 0 0 25 0 1 0 477246644 39956480 9191 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 9191 603 41 0 9714 0
vsize: 39020
[startup+280.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9213 0 0 0 27975 26 0 0 25 0 1 0 477246644 39956480 9191 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 9191 603 41 0 9714 0
vsize: 39020
[startup+290.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9213 0 0 0 28977 26 0 0 25 0 1 0 477246644 39956480 9191 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 9191 603 41 0 9714 0
vsize: 39020
[startup+300.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9213 0 0 0 29978 26 0 0 25 0 1 0 477246644 39956480 9191 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 9191 603 41 0 9714 0
vsize: 39020
[startup+310.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9446 0 0 0 30977 27 0 0 25 0 1 0 477246644 40902656 9424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9986 9424 603 41 0 9945 0
vsize: 39944
[startup+320.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9489 0 0 0 31977 27 0 0 25 0 1 0 477246644 41074688 9467 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9467 603 41 0 9987 0
vsize: 40112
[startup+330.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9489 0 0 0 32977 27 0 0 25 0 1 0 477246644 41074688 9467 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9467 603 41 0 9987 0
vsize: 40112
[startup+340.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9489 0 0 0 33977 27 0 0 25 0 1 0 477246644 41074688 9467 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9467 603 41 0 9987 0
vsize: 40112
[startup+350.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9489 0 0 0 34977 27 0 0 25 0 1 0 477246644 41074688 9467 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9467 603 41 0 9987 0
vsize: 40112
[startup+360.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9489 0 0 0 35977 27 0 0 25 0 1 0 477246644 41074688 9467 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9467 603 41 0 9987 0
vsize: 40112
[startup+370.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9489 0 0 0 36978 27 0 0 25 0 1 0 477246644 41074688 9467 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9467 603 41 0 9987 0
vsize: 40112
[startup+380.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9489 0 0 0 37978 27 0 0 25 0 1 0 477246644 41074688 9467 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9467 603 41 0 9987 0
vsize: 40112
[startup+390.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9489 0 0 0 38978 27 0 0 25 0 1 0 477246644 41074688 9467 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9467 603 41 0 9987 0
vsize: 40112
[startup+400.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9489 0 0 0 39978 27 0 0 25 0 1 0 477246644 41074688 9467 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9467 603 41 0 9987 0
vsize: 40112
[startup+410.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9489 0 0 0 40978 27 0 0 25 0 1 0 477246644 41074688 9467 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9467 603 41 0 9987 0
vsize: 40112
[startup+420.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9490 0 0 0 41978 27 0 0 25 0 1 0 477246644 41074688 9468 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9468 603 41 0 9987 0
vsize: 40112
[startup+430.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9490 0 0 0 42978 27 0 0 25 0 1 0 477246644 41074688 9468 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9468 603 41 0 9987 0
vsize: 40112
[startup+440.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9490 0 0 0 43979 27 0 0 25 0 1 0 477246644 41074688 9468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9468 603 41 0 9987 0
vsize: 40112
[startup+450.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9490 0 0 0 44979 27 0 0 25 0 1 0 477246644 41074688 9468 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9468 603 41 0 9987 0
vsize: 40112
[startup+460.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9490 0 0 0 45979 27 0 0 25 0 1 0 477246644 41074688 9468 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9468 603 41 0 9987 0
vsize: 40112
[startup+470.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9490 0 0 0 46979 27 0 0 25 0 1 0 477246644 41074688 9468 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9468 603 41 0 9987 0
vsize: 40112
[startup+480.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 47979 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223712 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+490.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 48979 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+500.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 49979 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+510.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 50980 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+520.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 51980 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+530.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 52980 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+540.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 53980 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+550.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 54980 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223648 134560177 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+560.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 55980 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+570.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 56980 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+580.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 57980 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+590.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 58981 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+600.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 59981 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+610.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 60981 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+620.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9491 0 0 0 61981 27 0 0 25 0 1 0 477246644 41074688 9469 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10028 9469 603 41 0 9987 0
vsize: 40112
[startup+630.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 9666 0 0 0 62981 27 0 0 25 0 1 0 477246644 41877504 9644 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10224 9644 603 41 0 10183 0
vsize: 40896
[startup+640.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10147 0 0 0 63979 29 0 0 25 0 1 0 477246644 43757568 10125 4294967295 134512640 134672761 3221224544 3221223344 134565852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 10125 603 41 0 10642 0
vsize: 42732
[startup+650.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10147 0 0 0 64980 29 0 0 25 0 1 0 477246644 43757568 10125 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 10125 603 41 0 10642 0
vsize: 42732
[startup+660.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10147 0 0 0 65980 29 0 0 25 0 1 0 477246644 43757568 10125 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 10125 603 41 0 10642 0
vsize: 42732
[startup+670.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10147 0 0 0 66980 29 0 0 25 0 1 0 477246644 43757568 10125 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 10125 603 41 0 10642 0
vsize: 42732
[startup+680.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10147 0 0 0 67980 29 0 0 25 0 1 0 477246644 43757568 10125 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 10125 603 41 0 10642 0
vsize: 42732
[startup+690.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10147 0 0 0 68980 29 0 0 25 0 1 0 477246644 43757568 10125 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 10125 603 41 0 10642 0
vsize: 42732
[startup+700.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10147 0 0 0 69980 29 0 0 25 0 1 0 477246644 43757568 10125 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 10125 603 41 0 10642 0
vsize: 42732
[startup+710.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10147 0 0 0 70981 29 0 0 25 0 1 0 477246644 43757568 10125 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 10125 603 41 0 10642 0
vsize: 42732
[startup+720.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10147 0 0 0 71981 29 0 0 25 0 1 0 477246644 43757568 10125 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 10125 603 41 0 10642 0
vsize: 42732
[startup+730.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10147 0 0 0 72981 29 0 0 25 0 1 0 477246644 43757568 10125 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10683 10125 603 41 0 10642 0
vsize: 42732
[startup+740.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10174 0 0 0 73981 29 0 0 25 0 1 0 477246644 43888640 10152 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10715 10152 603 41 0 10674 0
vsize: 42860
[startup+750.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10596 0 0 0 74980 30 0 0 25 0 1 0 477246644 45645824 10574 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11144 10574 603 41 0 11103 0
vsize: 44576
[startup+760.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 10994 0 0 0 75980 31 0 0 25 0 1 0 477246644 47259648 10972 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11538 10972 603 41 0 11497 0
vsize: 46152
[startup+770.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11047 0 0 0 76980 31 0 0 25 0 1 0 477246644 47529984 11025 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11025 603 41 0 11563 0
vsize: 46416
[startup+780.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11047 0 0 0 77980 31 0 0 25 0 1 0 477246644 47529984 11025 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11025 603 41 0 11563 0
vsize: 46416
[startup+790.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 78980 31 0 0 25 0 1 0 477246644 47529984 11026 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11026 603 41 0 11563 0
vsize: 46416
[startup+800.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 79980 31 0 0 25 0 1 0 477246644 47529984 11026 4294967295 134512640 134672761 3221224544 3221223808 134562218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11026 603 41 0 11563 0
vsize: 46416
[startup+810.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 80980 31 0 0 25 0 1 0 477246644 47529984 11026 4294967295 134512640 134672761 3221224544 3221223728 134559392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11026 603 41 0 11563 0
vsize: 46416
[startup+820.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 81980 31 0 0 25 0 1 0 477246644 47529984 11026 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11026 603 41 0 11563 0
vsize: 46416
[startup+830.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 82980 31 0 0 25 0 1 0 477246644 47529984 11026 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11026 603 41 0 11563 0
vsize: 46416
[startup+840.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 83980 31 0 0 25 0 1 0 477246644 47529984 11026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11026 603 41 0 11563 0
vsize: 46416
[startup+850.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 84980 32 0 0 25 0 1 0 477246644 47529984 11026 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11026 603 41 0 11563 0
vsize: 46416
[startup+860.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 85981 32 0 0 25 0 1 0 477246644 47529984 11026 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11026 603 41 0 11563 0
vsize: 46416
[startup+870.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 86981 32 0 0 25 0 1 0 477246644 47529984 11026 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11026 603 41 0 11563 0
vsize: 46416
[startup+880.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 87981 32 0 0 25 0 1 0 477246644 47529984 11026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 11026 603 41 0 11563 0
vsize: 46416
[startup+890.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 88981 32 0 0 25 0 1 0 477246644 47509504 11026 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11599 11026 603 41 0 11558 0
vsize: 46396
[startup+900.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 89981 32 0 0 25 0 1 0 477246644 47509504 11026 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11599 11026 603 41 0 11558 0
vsize: 46396
[startup+910.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 90981 32 0 0 25 0 1 0 477246644 47509504 11026 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11599 11026 603 41 0 11558 0
vsize: 46396
[startup+920.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 91982 32 0 0 25 0 1 0 477246644 47509504 11026 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11599 11026 603 41 0 11558 0
vsize: 46396
[startup+930.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 92982 32 0 0 25 0 1 0 477246644 47509504 11026 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11599 11026 603 41 0 11558 0
vsize: 46396
[startup+940.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 93982 32 0 0 25 0 1 0 477246644 47509504 11026 4294967295 134512640 134672761 3221224544 3221223708 134560077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11599 11026 603 41 0 11558 0
vsize: 46396
[startup+950.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 94982 32 0 0 25 0 1 0 477246644 47509504 11026 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11599 11026 603 41 0 11558 0
vsize: 46396
[startup+960.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11048 0 0 0 95982 32 0 0 25 0 1 0 477246644 47509504 11026 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11599 11026 603 41 0 11558 0
vsize: 46396
[startup+970.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11473 0 0 0 96981 33 0 0 25 0 1 0 477246644 49250304 11451 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12024 11452 603 41 0 11983 0
vsize: 48096
[startup+980.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 11984 0 0 0 97979 35 0 0 25 0 1 0 477246644 51253248 11962 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12513 11962 603 41 0 12472 0
vsize: 50052
[startup+990.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12154 0 0 0 98978 36 0 0 25 0 1 0 477246644 52060160 12132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12710 12132 603 41 0 12669 0
vsize: 50840
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12154 0 0 0 99979 36 0 0 25 0 1 0 477246644 52060160 12132 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12710 12132 603 41 0 12669 0
vsize: 50840
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12154 0 0 0 100979 36 0 0 25 0 1 0 477246644 52060160 12132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12710 12132 603 41 0 12669 0
vsize: 50840
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12154 0 0 0 101979 36 0 0 25 0 1 0 477246644 52060160 12132 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12710 12132 603 41 0 12669 0
vsize: 50840
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 102979 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 103979 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 104979 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 105979 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 106980 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 107980 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 108980 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 109980 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 110980 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 111981 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 112981 36 0 0 25 0 1 0 477246644 52043776 12135 4294967295 134512640 134672761 3221224544 3221222032 134565779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12706 12135 603 41 0 12665 0
vsize: 50824
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 113981 36 0 0 25 0 1 0 477246644 52015104 12135 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12699 12135 603 41 0 12658 0
vsize: 50796
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 114981 36 0 0 25 0 1 0 477246644 52015104 12135 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12699 12135 603 41 0 12658 0
vsize: 50796
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 115981 36 0 0 25 0 1 0 477246644 52015104 12135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12699 12135 603 41 0 12658 0
vsize: 50796
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 116981 36 0 0 25 0 1 0 477246644 52015104 12135 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12699 12135 603 41 0 12658 0
vsize: 50796
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 117982 36 0 0 25 0 1 0 477246644 52015104 12135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12699 12135 603 41 0 12658 0
vsize: 50796
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 118982 36 0 0 25 0 1 0 477246644 52015104 12135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12699 12135 603 41 0 12658 0
vsize: 50796
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 9841
Raw data (stat): 9841 (minisat+) R 9840 26667 26666 0 -1 0 12157 0 0 0 119982 36 0 0 25 0 1 0 477246644 52015104 12135 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12699 12135 603 41 0 12658 0
vsize: 50796
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 9841
Raw data (stat): 9841 (minisat+) Z 9840 26667 26666 0 -1 12 12160 0 0 0 119982 39 0 0 25 0 1 0 477246644 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.07
CPU time (s): 1200.22
CPU user time (s): 1199.83
CPU system time (s): 0.39194
CPU usage (%): 100.012
Max. virtual memory (Kb): 50840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####