PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-mod013.opb
MD5SUM	b964292d4197638ce79b3f213e8fe89b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5130240
Optimality of the best value was proved	NO
Number of terms in the objective function	1008
Biggest coefficient in the objective function	366477312
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	12643636975
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	366477312
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	12643636975
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	1008
Total number of constraints	110
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	48
Number of constraints which are nor clauses,nor cardinality constraints	62
Minimum length of a constraint	1
Maximum length of a constraint	160
Trace number 19272

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        803888 kB
Buffers:         28100 kB
Cached:         181248 kB
SwapCached:        364 kB
Active:          34804 kB
Inactive:       176980 kB
HighTotal:      131008 kB
HighFree:        85820 kB
LowTotal:       903652 kB
LowFree:        718068 kB
SwapTotal:     2097136 kB
SwapFree:      2096356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6400 kB
Slab:            13320 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:55:03 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 17048 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 76 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############
c   -- Clauses(.)/Splits(s): (none)
c ---[  74]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   19
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   15
c ---[  58]---> Sorter-cost: 1495     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> BDD-cost:   15
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   14
c ---[  46]---> Sorter-cost: 1495     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   16
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   13
c ---[  34]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  22]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   13
c ---[  10]---> Sorter-cost: 1391     Base: 2 2 2 2 2 2 2 2 2
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   4]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   39875    94300 |   13291       0        0     nan |  0.000 % |
c |       100 |   39796    94121 |   14620      97      326     3.4 |  8.098 % |
c |       250 |   39748    94013 |   16082     242     1150     4.8 |  8.194 % |
c |       475 |   39748    94013 |   17690     467     2209     4.7 |  8.194 % |
c ==============================================================================
c [1mFound solution: 12142577[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4334   maxlim: 18821886   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       655 |   70015   202266 |   23338     647     2925     4.5 |  8.194 % |
c ==============================================================================
c [1mFound solution: 12120899[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 18843564   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       686 |   70030   202450 |   23343     678     3514     5.2 |  8.194 % |
c |       786 |   70030   202450 |   25677     778     4163     5.4 |  6.449 % |
c |       936 |   69944   202255 |   28245     919     4949     5.4 |  6.591 % |
c ==============================================================================
c [1mFound solution: 11843450[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 19121013   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1079 |   69965   202465 |   23321    1062     6637     6.2 |  6.591 % |
c |      1179 |   69965   202465 |   25653    1162     7103     6.1 |  6.649 % |
c |      1329 |   69965   202465 |   28218    1312     8775     6.7 |  6.649 % |
c |      1554 |   69965   202465 |   31040    1537    12933     8.4 |  6.649 % |
c |      1891 |   69965   202465 |   34144    1874    45220    24.1 |  6.649 % |
c |      2397 |   69915   202352 |   37558    2378    49651    20.9 |  6.728 % |
c |      3156 |   69910   202341 |   41314    3136   238956    76.2 |  6.739 % |
c ==============================================================================
c [1mFound solution: 10725961[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 20238502   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3758 |   69749   202103 |   23249    3730   255374    68.5 |  6.739 % |
c |      3858 |   69749   202103 |   25573    3830   255999    66.8 |  7.066 % |
c |      4008 |   69749   202103 |   28131    3980   257142    64.6 |  7.066 % |
c |      4233 |   69749   202103 |   30944    4205   260182    61.9 |  7.066 % |
c |      4571 |   69728   202056 |   34038    4541   270662    59.6 |  7.097 % |
c ==============================================================================
c [1mFound solution: 10473014[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 20491449   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4991 |   69712   202162 |   23237    4959   276994    55.9 |  7.097 % |
c |      5091 |   69712   202162 |   25560    5059   279009    55.2 |  7.203 % |
c ==============================================================================
c [1mFound solution: 10204766[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 20759697   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5176 |   69724   202276 |   23241    5144   280381    54.5 |  7.203 % |
c |      5276 |   69724   202276 |   25565    5244   281775    53.7 |  7.235 % |
c |      5426 |   69724   202276 |   28121    5394   284725    52.8 |  7.235 % |
c |      5651 |   69724   202276 |   30933    5619   289356    51.5 |  7.235 % |
c |      5989 |   69631   202064 |   34027    5947   319026    53.6 |  7.377 % |
c ==============================================================================
c [1mFound solution: 9546584[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21417879   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6073 |   69652   202252 |   23217    6031   319676    53.0 |  7.377 % |
c |      6173 |   69652   202252 |   25538    6131   354707    57.9 |  7.433 % |
c |      6323 |   69620   202180 |   28092    6279   356329    56.7 |  7.486 % |
c |      6549 |   69620   202180 |   30901    6505   375138    57.7 |  7.486 % |
c ==============================================================================
c [1mFound solution: 9188258[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21776205   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6720 |   69627   202318 |   23209    6674   377204    56.5 |  7.486 % |
c |      6821 |   69627   202318 |   25529    6775   380588    56.2 |  7.537 % |
c |      6971 |   69601   202257 |   28082    6924   384546    55.5 |  7.579 % |
c |      7196 |   69601   202257 |   30891    7149   390112    54.6 |  7.579 % |
c |      7535 |   69542   202125 |   33980    7486   397989    53.2 |  7.668 % |
c |      8042 |   69542   202125 |   37378    7993   408564    51.1 |  7.668 % |
c ==============================================================================
c [1mFound solution: 8803184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22161279   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8572 |   69546   202205 |   23182    8522   441774    51.8 |  7.668 % |
c |      8672 |   69546   202205 |   25500    8622   445203    51.6 |  7.710 % |
c |      8822 |   69413   201899 |   28050    8761   464523    53.0 |  7.930 % |
c |      9047 |   69413   201899 |   30855    8986   473601    52.7 |  7.930 % |
c |      9384 |   69392   201851 |   33940    9322   502835    53.9 |  7.956 % |
c |      9890 |   69392   201851 |   37334    9828   519206    52.8 |  7.956 % |
c |     10651 |   69392   201851 |   41068   10589   548183    51.8 |  7.956 % |
c ==============================================================================
c [1mFound solution: 7726726[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23237737   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11787 |   69406   201995 |   23135   11725   673129    57.4 |  7.956 % |
c |     11887 |   69406   201995 |   25448   11825   673993    57.0 |  7.998 % |
c |     12037 |   69406   201995 |   27993   11975   682129    57.0 |  7.998 % |
c |     12263 |   69406   201995 |   30792   12201   706729    57.9 |  7.998 % |
c |     12600 |   69406   201995 |   33871   12538   717322    57.2 |  7.998 % |
c |     13107 |   69406   201995 |   37259   13045   774505    59.4 |  7.998 % |
c |     13867 |   69406   201995 |   40985   13805   935697    67.8 |  7.998 % |
c |     15007 |   69330   201822 |   45083   14923   998700    66.9 |  8.113 % |
c ==============================================================================
c [1mFound solution: 6432738[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 24531725   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15677 |   69338   201958 |   23112   15592  1024794    65.7 |  8.113 % |
c |     15777 |   69338   201958 |   25423   15692  1029024    65.6 |  8.173 % |
c |     15929 |   69338   201958 |   27965   15844  1089757    68.8 |  8.173 % |
c |     16155 |   69338   201958 |   30762   16070  1096632    68.2 |  8.173 % |
c |     16493 |   69338   201958 |   33838   16408  1113978    67.9 |  8.173 % |
c |     17001 |   69338   201958 |   37222   16916  1132920    67.0 |  8.173 % |
c |     17760 |   69338   201958 |   40944   17675  1365844    77.3 |  8.173 % |
c |     18901 |   69338   201958 |   45038   18816  1413462    75.1 |  8.173 % |
c ==============================================================================
c [1mFound solution: 5957249[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 25007214   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18930 |   69360   202165 |   23120   18845  1415342    75.1 |  8.173 % |
c |     19030 |   69360   202165 |   25432   18945  1436986    75.9 |  8.226 % |
c |     19182 |   69298   202022 |   27975   19083  1455480    76.3 |  8.320 % |
c |     19408 |   69298   202022 |   30772   19309  1468519    76.1 |  8.320 % |
c |     19747 |   69298   202022 |   33849   19648  1500516    76.4 |  8.320 % |
c |     20256 |   69204   201808 |   37234   20143  1541773    76.5 |  8.456 % |
c |     21015 |   69204   201808 |   40958   20902  1559530    74.6 |  8.456 % |
c |     22156 |   69204   201808 |   45054   22043  1686247    76.5 |  8.456 % |
c |     23866 |   69204   201808 |   49559   23753  1756872    74.0 |  8.456 % |
c |     26428 |   69204   201808 |   54515   26315  2280025    86.6 |  8.456 % |
c ==============================================================================
c [1mFound solution: 5207530[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 25756933   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27818 |   69049   199997 |   23016   27506  2341612    85.1 |  8.456 % |
c |     27920 |   69049   199997 |   25317   13855  1003478    72.4 |  8.551 % |
c |     28070 |   69049   199997 |   27849   14005  1005030    71.8 |  8.551 % |
c |     28298 |   69039   199974 |   30634   14232  1008191    70.8 |  8.566 % |
c |     28635 |   69003   199890 |   33697   14568  1049136    72.0 |  8.629 % |
c |     29141 |   69003   199890 |   37067   15074  1152404    76.4 |  8.629 % |
c |     29900 |   68962   199800 |   40774   15828  1192767    75.4 |  8.686 % |
c |     31043 |   68962   199800 |   44851   16971  1264285    74.5 |  8.686 % |
c |     32753 |   68962   199800 |   49336   18681  1419491    76.0 |  8.686 % |
c |     35315 |   68962   199800 |   54270   21243  1554273    73.2 |  8.686 % |
c |     39159 |   68962   199800 |   59697   25087  1756711    70.0 |  8.686 % |
c |     44925 |   68949   199771 |   65667   30851  2243946    72.7 |  8.702 % |
c |     53576 |   68949   199771 |   72234   39502  3007725    76.1 |  8.702 % |
c |     66553 |   68946   199765 |   79457   52478  4179697    79.6 |  8.707 % |
c |     86014 |   68922   199710 |   87403   71937  5584587    77.6 |  8.739 % |
c |    115206 |   68850   199546 |   96143   25886  1868537    72.2 |  8.848 % |
c |    158995 |   68840   199524 |  105757   69674  5540014    79.5 |  8.864 % |
c |    224679 |   68840   199524 |  116333   45502  3015422    66.3 |  8.864 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1_0x2e__bit_7 -C1_0x2e__bit_6 C1_0x2e__bit_5 -C1_0x2e__bit_4 -C1_0x2e__bit_3 -C1_0x2e__bit_2 -C1_0x2e__bit_1 C1_0x2e__bit0 C1_0x2e__bit1 C1_0x2e__bit2 C1_0x2e__bit3 -C1_0x2e__bit4 -C1_0x2e__bit5 -C1_0x2e__bit6 -C1_0x2e__bit7 -C1_0x2e__bit8 -C1_0x2e__bit9 -C1_0x2e__bit10 -C1_0x2e__bit11 -C1_0x2e__bit12 -C2_0x2e__bit_7 -C2_0x2e__bit_6 -C2_0x2e__bit_5 -C2_0x2e__bit_4 -C2_0x2e__bit_3 -C2_0x2e__bit_2 -C2_0x2e__bit_1 -C2_0x2e__bit0 -C2_0x2e__bit1 -C2_0x2e__bit2 -C2_0x2e__bit3 -C2_0x2e__bit4 -C2_0x2e__bit5 -C2_0x2e__bit6 -C2_0x2e__bit7 -C2_0x2e__bit8 -C2_0x2e__bit9 -C2_0x2e__bit10 -C2_0x2e__bit11 -C2_0x2e__bit12 -C3_0x2e__bit_7 -C3_0x2e__bit_6 C3_0x2e__bit_5 C3_0x2e__bit_4 -C3_0x2e__bit_3 -C3_0x2e__bit_2 -C3_0x2e__bit_1 -C3_0x2e__bit0 C3_0x2e__bit1 C3_0x2e__bit2 -C3_0x2e__bit3 C3_0x2e__bit4 -C3_0x2e__bit5 -C3_0x2e__bit6 -C3_0x2e__bit7 -C3_0x2e__bit8 -C3_0x2e__bit9 -C3_0x2e__bit10 -C3_0x2e__bit11 -C3_0x2e__bit12 -C4_0x2e__bit_7 -C4_0x2e__bit_6 -C4_0x2e__bit_5 -C4_0x2e__bit_4 -C4_0x2e__bit_3 -C4_0x2e__bit_2 -C4_0x2e__bit_1 -C4_0x2e__bit0 -C4_0x2e__bit1 -C4_0x2e__bit2 -C4_0x2e__bit3 -C4_0x2e__bit4 -C4_0x2e__bit5 -C4_0x2e__bit6 -C4_0x2e__bit7 -C4_0x2e__bit8 -C4_0x2e__bit9 -C4_0x2e__bit10 -C4_0x2e__bit11 -C4_0x2e__bit12 -C5_0x2e__bit_7 -C5_0x2e__bit_6 -C5_0x2e__bit_5 -C5_0x2e__bit_4 C5_0x2e__bit_3 C5_0x2e__bit_2 C5_0x2e__bit_1 C5_0x2e__bit0 C5_0x2e__bit1 C5_0x2e__bit2 -C5_0x2e__bit3 -C5_0x2e__bit4 -C5_0x2e__bit5 -C5_0x2e__bit6 -C5_0x2e__bit7 -C5_0x2e__bit8 -C5_0x2e__bit9 -C5_0x2e__bit10 -C5_0x2e__bit11 -C5_0x2e__bit12 -C6_0x2e__bit_7 -C6_0x2e__bit_6 -C6_0x2e__bit_5 -C6_0x2e__bit_4 -C6_0x2e__bit_3 -C6_0x2e__bit_2 -C6_0x2e__bit_1 -C6_0x2e__bit0 -C6_0x2e__bit1 -C6_0x2e__bit2 -C6_0x2e__bit3 -C6_0x2e__bit4 -C6_0x2e__bit5 -C6_0x2e__bit6 -C6_0x2e__bit7 -C6_0x2e__bit8 -C6_0x2e__bit9 -C6_0x2e__bit10 -C6_0x2e__bit11 -C6_0x2e__bit12 -C7_0x2e__bit_7 -C7_0x2e__bit_6 -C7_0x2e__bit_5 -C7_0x2e__bit_4 -C7_0x2e__bit_3 -C7_0x2e__bit_2 -C7_0x2e__bit_1 -C7_0x2e__bit0 -C7_0x2e__bit1 -C7_0x2e__bit2 -C7_0x2e__bit3 -C7_0x2e__bit4 -C7_0x2e__bit5 -C7_0x2e__bit6 -C7_0x2e__bit7 -C7_0x2e__bit8 -C7_0x2e__bit9 -C7_0x2e__bit10 -C7_0x2e__bit11 -C7_0x2e__bit12 -C8_0x2e__bit_7 -C8_0x2e__bit_6 -C8_0x2e__bit_5 -C8_0x2e__bit_4 -C8_0x2e__bit_3 -C8_0x2e__bit_2 -C8_0x2e__bit_1 -C8_0x2e__bit0 -C8_0x2e__bit1 -C8_0x2e__bit2 -C8_0x2e__bit3 -C8_0x2e__bit4 -C8_0x2e__bit5 -C8_0x2e__bit6 -C8_0x2e__bit7 -C8_0x2e__bit8 -C8_0x2e__bit9 -C8_0x2e__bit10 -C8_0x2e__bit11 -C8_0x2e__bit12 -C9_0x2e__bit_7 -C9_0x2e__bit_6 -C9_0x2e__bit_5 -C9_0x2e__bit_4 -C9_0x2e__bit_3 -C9_0x2e__bit_2 -C9_0x2e__bit_1 -C9_0x2e__bit0 -C9_0x2e__bit1 -C9_0x2e__bit2 C9_0x2e__bit3 -C9_0x2e__bit4 -C9_0x2e__bit5 -C9_0x2e__bit6 -C9_0x2e__bit7 -C9_0x2e__bit8 -C9_0x2e__bit9 -C9_0x2e__bit10 -C9_0x2e__bit11 -C9_0x2e__bit12 C10_0x2e__bit_7 -C10_0x2e__bit_6 -C10_0x2e__bit_5 -C10_0x2e__bit_4 -C10_0x2e__bit_3 -C10_0x2e__bit_2 -C10_0x2e__bit_1 -C10_0x2e__bit0 C10_0x2e__bit1 C10_0x2e__bit2 C10_0x2e__bit3 -C10_0x2e__bit4 -C10_0x2e__bit5 -C10_0x2e__bit6 -C10_0x2e__bit7 -C10_0x2e__bit8 -C10_0x2e__bit9 -C10_0x2e__bit10 -C10_0x2e__bit11 -C10_0x2e__bit12 -C11_0x2e__bit_7 -C11_0x2e__bit_6 -C11_0x2e__bit_5 -C11_0x2e__bit_4 -C11_0x2e__bit_3 -C11_0x2e__bit_2 -C11_0x2e__bit_1 -C11_0x2e__bit0 -C11_0x2e__bit1 -C11_0x2e__bit2 -C11_0x2e__bit3 -C11_0x2e__bit4 -C11_0x2e__bit5 -C11_0x2e__bit6 -C11_0x2e__bit7 -C11_0x2e__bit8 -C11_0x2e__bit9 -C11_0x2e__bit10 -C11_0x2e__bit11 -C11_0x2e__bit12 C12_0x2e__bit_7 C12_0x2e__bit_6 C12_0x2e__bit_5 C12_0x2e__bit_4 C12_0x2e__bit_3 C12_0x2e__bit_2 C12_0x2e__bit_1 C12_0x2e__bit0 -C12_0x2e__bit1 -C12_0x2e__bit2 -C12_0x2e__bit3 C12_0x2e__bit4 -C12_0x2e__bit5 -C12_0x2e__bit6 -C12_0x2e__bit7 -C12_0x2e__bit8 -C12_0x2e__bit9 -C12_0x2e__bit10 -C12_0x2e__bit11 -C12_0x2e__bit12 -C13_0x2e__bit_7 -C13_0x2e__bit_6 -C13_0x2e__bit_5 -C13_0x2e__bit_4 -C13_0x2e__bit_3 -C13_0x2e__bit_2 -C13_0x2e__bit_1 -C13_0x2e__bit0 -C13_0x2e__bit1 -C13_0x2e__bit2 -C13_0x2e__bit3 -C13_0x2e__bit4 -C13_0x2e__bit5 -C13_0x2e__bit6 -C13_0x2e__bit7 -C13_0x2e__bit8 -C13_0x2e__bit9 -C13_0x2e__bit10 -C13_0x2e__bit11 -C13_0x2e__bit12 -C14_0x2e__bit_7 -C14_0x2e__bit_6 -C14_0x2e__bit_5 -C14_0x2e__bit_4 -C14_0x2e__bit_3 -C14_0x2e__bit_2 -C14_0x2e__bit_1 -C14_0x2e__bit0 -C14_0x2e__bit1 -C14_0x2e__bit2 -C14_0x2e__bit3 -C14_0x2e__bit4 -C14_0x2e__bit5 -C14_0x2e__bit6 -C14_0x2e__bit7 -C14_0x2e__bit8 -C14_0x2e__bit9 -C14_0x2e__bit10 -C14_0x2e__bit11 -C14_0x2e__bit12 -C15_0x2e__bit_7 -C15_0x2e__bit_6 -C15_0x2e__bit_5 -C15_0x2e__bit_4 -C15_0x2e__bit_3 -C15_0x2e__bit_2 -C15_0x2e__bit_1 -C15_0x2e__bit0 -C15_0x2e__bit1 -C15_0x2e__bit2 -C15_0x2e__bit3 -C15_0x2e__bit4 -C15_0x2e__bit5 -C15_0x2e__bit6 -C15_0x2e__bit7 -C15_0x2e__bit8 -C15_0x2e__bit9 -C15_0x2e__bit10 -C15_0x2e__bit11 -C15_0x2e__bit12 -C16_0x2e__bit_7 -C16_0x2e__bit_6 -C16_0x2e__bit_5 -C16_0x2e__bit_4 -C16_0x2e__bit_3 -C16_0x2e__bit_2 -C16_0x2e__bit_1 -C16_0x2e__bit0 -C16_0x2e__bit1 -C16_0x2e__bit2 -C16_0x2e__bit3 -C16_0x2e__bit4 -C16_0x2e__bit5 -C16_0x2e__bit6 -C16_0x2e__bit7 -C16_0x2e__bit8 -C16_0x2e__bit9 -C16_0x2e__bit10 -C16_0x2e__bit11 -C16_0x2e__bit12 -C17_0x2e__bit_7 -C17_0x2e__bit_6 C17_0x2e__bit_5 -C17_0x2e__bit_4 C17_0x2e__bit_3 -C17_0x2e__bit_2 -C17_0x2e__bit_1 C17_0x2e__bit0 C17_0x2e__bit1 -C17_0x2e__bit2 C17_0x2e__bit3 -C17_0x2e__bit4 -C17_0x2e__bit5 -C17_0x2e__bit6 -C17_0x2e__bit7 -C17_0x2e__bit8 -C17_0x2e__bit9 -C17_0x2e__bit10 -C17_0x2e__bit11 -C17_0x2e__bit12 C18_0x2e__bit_7 C18_0x2e__bit_6 C18_0x2e__bit_5 C18_0x2e__bit_4 C18_0x2e__bit_3 C18_0x2e__bit_2 C18_0x2e__bit_1 C18_0x2e__bit0 C18_0x2e__bit1 C18_0x2e__bit2 C18_0x2e__bit3 -C18_0x2e__bit4 -C18_0x2e__bit5 -C18_0x2e__bit6 -C18_0x2e__bit7 -C18_0x2e__bit8 -C18_0x2e__bit9 -C18_0x2e__bit10 -C18_0x2e__bit11 -C18_0x2e__bit12 C19_0x2e__bit_7 -C19_0x2e__bit_6 C19_0x2e__bit_5 C19_0x2e__bit_4 -C19_0x2e__bit_3 C19_0x2e__bit_2 C19_0x2e__bit_1 -C19_0x2e__bit0 C19_0x2e__bit1 -C19_0x2e__bit2 -C19_0x2e__bit3 -C19_0x2e__bit4 -C19_0x2e__bit5 -C19_0x2e__bit6 -C19_0x2e__bit7 -C19_0x2e__bit8 -C19_0x2e__bit9 -C19_0x2e__bit10 -C19_0x2e__bit11 -C19_0x2e__bit12 -C20_0x2e__bit_7 -C20_0x2e__bit_6 -C20_0x2e__bit_5 -C20_0x2e__bit_4 -C20_0x2e__bit_3 -C20_0x2e__bit_2 -C20_0x2e__bit_1 -C20_0x2e__bit0 -C20_0x2e__bit1 -C20_0x2e__bit2 -C20_0x2e__bit3 -C20_0x2e__bit4 -C20_0x2e__bit5 -C20_0x2e__bit6 -C20_0x2e__bit7 -C20_0x2e__bit8 -C20_0x2e__bit9 -C20_0x2e__bit10 -C20_0x2e__bit11 -C20_0x2e__bit12 -C21_0x2e__bit_7 -C21_0x2e__bit_6 -C21_0x2e__bit_5 -C21_0x2e__bit_4 -C21_0x2e__bit_3 -C21_0x2e__bit_2 -C21_0x2e__bit_1 -C21_0x2e__bit0 -C21_0x2e__bit1 -C21_0x2e__bit2 -C21_0x2e__bit3 -C21_0x2e__bit4 -C21_0x2e__bit5 -C21_0x2e__bit6 -C21_0x2e__bit7 -C21_0x2e__bit8 -C21_0x2e__bit9 -C21_0x2e__bit10 -C21_0x2e__bit11 -C21_0x2e__bit12 -C22_0x2e__bit_7 -C22_0x2e__bit_6 -C22_0x2e__bit_5 -C22_0x2e__bit_4 -C22_0x2e__bit_3 -C22_0x2e__bit_2 -C22_0x2e__bit_1 -C22_0x2e__bit0 -C22_0x2e__bit1 -C22_0x2e__bit2 -C22_0x2e__bit3 -C22_0x2e__bit4 -C22_0x2e__bit5 -C22_0x2e__bit6 -C22_0x2e__bit7 -C22_0x2e__bit8 -C22_0x2e__bit9 -C22_0x2e__bit10 -C22_0x2e__bit11 -C22_0x2e__bit12 -C23_0x2e__bit_7 -C23_0x2e__bit_6 -C23_0x2e__bit_5 -C23_0x2e__bit_4 -C23_0x2e__bit_3 -C23_0x2e__bit_2 -C23_0x2e__bit_1 -C23_0x2e__bit0 -C23_0x2e__bit1 -C23_0x2e__bit2 -C23_0x2e__bit3 -C23_0x2e__bit4 -C23_0x2e__bit5 -C23_0x2e__bit6 -C23_0x2e__bit7 -C23_0x2e__bit8 -C23_0x2e__bit9 -C23_0x2e__bit10 -C23_0x2e__bit11 -C23_0x2e__bit12 -C24_0x2e__bit_7 -C24_0x2e__bit_6 -C24_0x2e__bit_5 -C24_0x2e__bit_4 -C24_0x2e__bit_3 -C24_0x2e__bit_2 -C24_0x2e__bit_1 -C24_0x2e__bit0 -C24_0x2e__bit1 -C24_0x2e__bit2 -C24_0x2e__bit3 -C24_0x2e__bit4 -C24_0x2e__bit5 -C24_0x2e__bit6 -C24_0x2e__bit7 -C24_0x2e__bit8 -C24_0x2e__bit9 -C24_0x2e__bit10 -C24_0x2e__bit11 -C24_0x2e__bit12 -C25_0x2e__bit_7 -C25_0x2e__bit_6 -C25_0x2e__bit_5 -C25_0x2e__bit_4 -C25_0x2e__bit_3 -C25_0x2e__bit_2 -C25_0x2e__bit_1 -C25_0x2e__bit0 -C25_0x2e__bit1 -C25_0x2e__bit2 -C25_0x2e__bit3 -C25_0x2e__bit4 -C25_0x2e__bit5 -C25_0x2e__bit6 -C25_0x2e__bit7 -C25_0x2e__bit8 -C25_0x2e__bit9 -C25_0x2e__bit10 -C25_0x2e__bit11 -C25_0x2e__bit12 -C26_0x2e__bit_7 -C26_0x2e__bit_6 -C26_0x2e__bit_5 -C26_0x2e__bit_4 -C26_0x2e__bit_3 -C26_0x2e__bit_2 -C26_0x2e__bit_1 -C26_0x2e__bit0 -C26_0x2e__bit1 -C26_0x2e__bit2 -C26_0x2e__bit3 -C26_0x2e__bit4 -C26_0x2e__bit5 -C26_0x2e__bit6 -C26_0x2e__bit7 -C26_0x2e__bit8 -C26_0x2e__bit9 -C26_0x2e__bit10 -C26_0x2e__bit11 -C26_0x2e__bit12 -C27_0x2e__bit_7 -C27_0x2e__bit_6 -C27_0x2e__bit_5 -C27_0x2e__bit_4 -C27_0x2e__bit_3 -C27_0x2e__bit_2 -C27_0x2e__bit_1 -C27_0x2e__bit0 -C27_0x2e__bit1 -C27_0x2e__bit2 -C27_0x2e__bit3 -C27_0x2e__bit4 -C27_0x2e__bit5 -C27_0x2e__bit6 -C27_0x2e__bit7 -C27_0x2e__bit8 -C27_0x2e__bit9 -C27_0x2e__bit10 -C27_0x2e__bit11 -C27_0x2e__bit12 -C28_0x2e__bit_7 -C28_0x2e__bit_6 -C28_0x2e__bit_5 -C28_0x2e__bit_4 -C28_0x2e__bit_3 -C28_0x2e__bit_2 -C28_0x2e__bit_1 -C28_0x2e__bit0 -C28_0x2e__bit1 -C28_0x2e__bit2 -C28_0x2e__bit3 -C28_0x2e__bit4 -C28_0x2e__bit5 -C28_0x2e__bit6 -C28_0x2e__bit7 -C28_0x2e__bit8 -C28_0x2e__bit9 -C28_0x2e__bit10 -C28_0x2e__bit11 -C28_0x2e__bit12 -C29_0x2e__bit_7 -C29_0x2e__bit_6 -C29_0x2e__bit_5 -C29_0x2e__bit_4 -C29_0x2e__bit_3 -C29_0x2e__bit_2 -C29_0x2e__bit_1 -C29_0x2e__bit0 -C29_0x2e__bit1 -C29_0x2e__bit2 -C29_0x2e__bit3 -C29_0x2e__bit4 -C29_0x2e__bit5 -C29_0x2e__bit6 -C29_0x2e__bit7 -C29_0x2e__bit8 -C29_0x2e__bit9 -C29_0x2e__bit10 -C29_0x2e__bit11 -C29_0x2e__bit12 -C30_0x2e__bit_7 -C30_0x2e__bit_6 -C30_0x2e__bit_5 -C30_0x2e__bit_4 -C30_0x2e__bit_3 -C30_0x2e__bit_2 -C30_0x2e__bit_1 -C30_0x2e__bit0 C30_0x2e__bit1 -C30_0x2e__bit2 C30_0x2e__bit3 -C30_0x2e__bit4 -C30_0x2e__bit5 -C30_0x2e__bit6 -C30_0x2e__bit7 -C30_0x2e__bit8 -C30_0x2e__bit9 -C30_0x2e__bit10 -C30_0x2e__bit11 -C30_0x2e__bit12 -C31_0x2e__bit_7 -C31_0x2e__bit_6 -C31_0x2e__bit_5 -C31_0x2e__bit_4 -C31_0x2e__bit_3 -C31_0x2e__bit_2 -C31_0x2e__bit_1 -C31_0x2e__bit0 C31_0x2e__bit1 -C31_0x2e__bit2 C31_0x2e__bit3 -C31_0x2e__bit4 -C31_0x2e__bit5 -C31_0x2e__bit6 -C31_0x2e__bit7 -C31_0x2e__bit8 -C31_0x2e__bit9 -C31_0x2e__bit10 -C31_0x2e__bit11 -C31_0x2e__bit12 -C32_0x2e__bit_7 -C32_0x2e__bit_6 -C32_0x2e__bit_5 -C32_0x2e__bit_4 -C32_0x2e__bit_3 -C32_0x2e__bit_2 -C32_0x2e__bit_1 -C32_0x2e__bit0 -C32_0x2e__bit1 -C32_0x2e__bit2 -C32_0x2e__bit3 -C32_0x2e__bit4 -C32_0x2e__bit5 -C32_0x2e__bit6 -C32_0x2e__bit7 -C32_0x2e__bit8 -C32_0x2e__bit9 -C32_0x2e__bit10 -C32_0x2e__bit11 -C32_0x2e__bit12 -C33_0x2e__bit_7 -C33_0x2e__bit_6 -C33_0x2e__bit_5 C33_0x2e__bit_4 -C33_0x2e__bit_3 C33_0x2e__bit_2 C33_0x2e__bit_1 -C33_0x2e__bit0 -C33_0x2e__bit1 -C33_0x2e__bit2 -C33_0x2e__bit3 -C33_0x2e__bit4 -C33_0x2e__bit5 -C33_0x2e__bit6 -C33_0x2e__bit7 -C33_0x2e__bit8 -C33_0x2e__bit9 -C33_0x2e__bit10 -C33_0x2e__bit11 -C33_0x2e__bit12 -C34_0x2e__bit_7 -C34_0x2e__bit_6 -C34_0x2e__bit_5 -C34_0x2e__bit_4 -C34_0x2e__bit_3 -C34_0x2e__bit_2 -C34_0x2e__bit_1 -C34_0x2e__bit0 -C34_0x2e__bit1 -C34_0x2e__bit2 -C34_0x2e__bit3 -C34_0x2e__bit4 -C34_0x2e__bit5 -C34_0x2e__bit6 -C34_0x2e__bit7 -C34_0x2e__bit8 -C34_0x2e__bit9 -C34_0x2e__bit10 -C34_0x2e__bit11 -C34_0x2e__bit12 -C35_0x2e__bit_7 -C35_0x2e__bit_6 -C35_0x2e__bit_5 -C35_0x2e__bit_4 -C35_0x2e__bit_3 -C35_0x2e__bit_2 -C35_0x2e__bit_1 -C35_0x2e__bit0 -C35_0x2e__bit1 -C35_0x2e__bit2 -C35_0x2e__bit3 -C35_0x2e__bit4 -C35_0x2e__bit5 -C35_0x2e__bit6 -C35_0x2e__bit7 -C35_0x2e__bit8 -C35_0x2e__bit9 -C35_0x2e__bit10 -C35_0x2e__bit11 -C35_0x2e__bit12 C36_0x2e__bit_7 -C36_0x2e__bit_6 -C36_0x2e__bit_5 -C36_0x2e__bit_4 -C36_0x2e__bit_3 -C36_0x2e__bit_2 -C36_0x2e__bit_1 -C36_0x2e__bit0 C36_0x2e__bit1 -C36_0x2e__bit2 -C36_0x2e__bit3 -C36_0x2e__bit4 -C36_0x2e__bit5 -C36_0x2e__bit6 -C36_0x2e__bit7 -C36_0x2e__bit8 -C36_0x2e__bit9 -C36_0x2e__bit10 -C36_0x2e__bit11 -C36_0x2e__bit12 -C37_0x2e__bit_7 -C37_0x2e__bit_6 -C37_0x2e__bit_5 -C37_0x2e__bit_4 C37_0x2e__bit_3 -C37_0x2e__bit_2 -C37_0x2e__bit_1 C37_0x2e__bit0 C37_0x2e__bit1 C37_0x2e__bit2 -C37_0x2e__bit3 -C37_0x2e__bit4 -C37_0x2e__bit5 -C37_0x2e__bit6 -C37_0x2e__bit7 -C37_0x2e__bit8 -C37_0x2e__bit9 -C37_0x2e__bit10 -C37_0x2e__bit11 -C37_0x2e__bit12 -C38_0x2e__bit_7 -C38_0x2e__bit_6 -C38_0x2e__bit_5 -C38_0x2e__bit_4 -C38_0x2e__bit_3 -C38_0x2e__bit_2 -C38_0x2e__bit_1 -C38_0x2e__bit0 -C38_0x2e__bit1 -C38_0x2e__bit2 -C38_0x2e__bit3 -C38_0x2e__bit4 -C38_0x2e__bit5 -C38_0x2e__bit6 -C38_0x2e__bit7 -C38_0x2e__bit8 -C38_0x2e__bit9 -C38#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.80 0.91 0.94 2/54 12264
Raw data (stat): 12264 (runsolver) R 12263 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489054955 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0007 s]
Raw data (loadavg): 0.83 0.91 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 4976 0 0 0 986 12 0 0 25 0 1 0 489054955 20434944 4112 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4989 4112 603 41 0 4948 0
vsize: 19956
[startup+20.002 s]
Raw data (loadavg): 0.86 0.91 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 5384 0 0 0 1985 13 0 0 25 0 1 0 489054955 21176320 4279 4294967295 134512640 134672761 3221224624 3221220704 134545105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5170 4279 603 41 0 5129 0
vsize: 20680
[startup+30.0024 s]
Raw data (loadavg): 0.88 0.91 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 5879 0 0 0 2982 16 0 0 25 0 1 0 489054955 22589440 4630 4294967295 134512640 134672761 3221224624 3221223824 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5515 4630 603 41 0 5474 0
vsize: 22060
[startup+40.0023 s]
Raw data (loadavg): 0.90 0.92 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 6342 0 0 0 3981 17 0 0 25 0 1 0 489054955 24162304 5020 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5899 5020 603 41 0 5858 0
vsize: 23596
[startup+50.0035 s]
Raw data (loadavg): 0.91 0.92 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 6841 0 0 0 4979 19 0 0 25 0 1 0 489054955 25956352 5446 4294967295 134512640 134672761 3221224624 3221223924 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6337 5446 603 41 0 6296 0
vsize: 25348
[startup+60.003 s]
Raw data (loadavg): 0.93 0.92 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 7176 0 0 0 5978 20 0 0 25 0 1 0 489054955 27295744 5781 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6664 5781 603 41 0 6623 0
vsize: 26656
[startup+70.0039 s]
Raw data (loadavg): 0.94 0.92 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 7805 0 0 0 6976 22 0 0 25 0 1 0 489054955 29835264 6410 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7284 6410 603 41 0 7243 0
vsize: 29136
[startup+80.0052 s]
Raw data (loadavg): 0.95 0.92 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 7932 0 0 0 7976 23 0 0 25 0 1 0 489054955 30089216 6463 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7346 6463 603 41 0 7305 0
vsize: 29384
[startup+90.0046 s]
Raw data (loadavg): 0.95 0.93 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 7932 0 0 0 8975 23 0 0 25 0 1 0 489054955 30089216 6463 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7346 6463 603 41 0 7305 0
vsize: 29384
[startup+100.005 s]
Raw data (loadavg): 0.96 0.93 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 7932 0 0 0 9975 23 0 0 25 0 1 0 489054955 30089216 6463 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7346 6463 603 41 0 7305 0
vsize: 29384
[startup+110.007 s]
Raw data (loadavg): 0.97 0.93 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 7935 0 0 0 10975 24 0 0 25 0 1 0 489054955 30089216 6466 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7346 6466 603 41 0 7305 0
vsize: 29384
[startup+120.008 s]
Raw data (loadavg): 0.97 0.93 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 8212 0 0 0 11974 25 0 0 25 0 1 0 489054955 31293440 6743 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7640 6743 603 41 0 7599 0
vsize: 30560
[startup+130.008 s]
Raw data (loadavg): 0.98 0.93 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 8528 0 0 0 12973 27 0 0 25 0 1 0 489054955 32636928 7059 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7968 7059 603 41 0 7927 0
vsize: 31872
[startup+140.008 s]
Raw data (loadavg): 0.98 0.94 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 8851 0 0 0 13972 28 0 0 25 0 1 0 489054955 33972224 7382 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8294 7382 603 41 0 8253 0
vsize: 33176
[startup+150.009 s]
Raw data (loadavg): 0.98 0.94 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 9274 0 0 0 14970 29 0 0 25 0 1 0 489054955 35717120 7805 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8720 7805 603 41 0 8679 0
vsize: 34880
[startup+160.009 s]
Raw data (loadavg): 0.98 0.94 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 9643 0 0 0 15969 31 0 0 25 0 1 0 489054955 37171200 8174 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8174 603 41 0 9034 0
vsize: 36300
[startup+170.01 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 9827 0 0 0 16969 31 0 0 25 0 1 0 489054955 37842944 8358 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9239 8358 603 41 0 9198 0
vsize: 36956
[startup+180.01 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 9991 0 0 0 17968 32 0 0 25 0 1 0 489054955 38514688 8522 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9403 8522 603 41 0 9362 0
vsize: 37612
[startup+190.01 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 10149 0 0 0 18967 33 0 0 25 0 1 0 489054955 39182336 8680 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9566 8680 603 41 0 9525 0
vsize: 38264
[startup+200.012 s]
Raw data (loadavg): 0.99 0.94 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 10309 0 0 0 19967 33 0 0 25 0 1 0 489054955 39849984 8840 4294967295 134512640 134672761 3221224624 3221223824 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9729 8840 603 41 0 9688 0
vsize: 38916
[startup+210.012 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 10481 0 0 0 20966 34 0 0 25 0 1 0 489054955 40517632 9012 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9892 9012 603 41 0 9851 0
vsize: 39568
[startup+220.013 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 10655 0 0 0 21965 35 0 0 25 0 1 0 489054955 41177088 9186 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10053 9186 603 41 0 10012 0
vsize: 40212
[startup+230.013 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 10826 0 0 0 22965 36 0 0 25 0 1 0 489054955 41975808 9357 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10248 9357 603 41 0 10207 0
vsize: 40992
[startup+240.012 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 11003 0 0 0 23964 36 0 0 25 0 1 0 489054955 42635264 9534 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10409 9534 603 41 0 10368 0
vsize: 41636
[startup+250.012 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 11167 0 0 0 24964 37 0 0 25 0 1 0 489054955 43565056 9698 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10636 9698 603 41 0 10595 0
vsize: 42544
[startup+260.012 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 11322 0 0 0 25964 37 0 0 25 0 1 0 489054955 44228608 9853 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10798 9853 603 41 0 10757 0
vsize: 43192
[startup+270.013 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 11474 0 0 0 26964 38 0 0 25 0 1 0 489054955 44892160 10005 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10960 10005 603 41 0 10919 0
vsize: 43840
[startup+280.013 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 11656 0 0 0 27963 38 0 0 25 0 1 0 489054955 45572096 10187 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11126 10187 603 41 0 11085 0
vsize: 44504
[startup+290.013 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 11774 0 0 0 28963 39 0 0 25 0 1 0 489054955 46112768 10305 4294967295 134512640 134672761 3221224624 3221223808 134558934 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11258 10305 603 41 0 11217 0
vsize: 45032
[startup+300.014 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 11904 0 0 0 29963 39 0 0 25 0 1 0 489054955 46645248 10435 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11388 10435 603 41 0 11347 0
vsize: 45552
[startup+310.013 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 12038 0 0 0 30963 39 0 0 25 0 1 0 489054955 47063040 10569 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11490 10569 603 41 0 11449 0
vsize: 45960
[startup+320.015 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 12361 0 0 0 31962 40 0 0 25 0 1 0 489054955 48398336 10892 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11816 10892 603 41 0 11775 0
vsize: 47264
[startup+330.015 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 12572 0 0 0 32961 41 0 0 25 0 1 0 489054955 49328128 11103 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12043 11103 603 41 0 12002 0
vsize: 48172
[startup+340.015 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 12738 0 0 0 33961 42 0 0 25 0 1 0 489054955 49991680 11269 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12205 11269 603 41 0 12164 0
vsize: 48820
[startup+350.015 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 12864 0 0 0 34961 42 0 0 25 0 1 0 489054955 50536448 11395 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12338 11395 603 41 0 12297 0
vsize: 49352
[startup+360.016 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 12985 0 0 0 35961 42 0 0 25 0 1 0 489054955 50933760 11516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12435 11516 603 41 0 12394 0
vsize: 49740
[startup+370.017 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13143 0 0 0 36960 43 0 0 25 0 1 0 489054955 51605504 11674 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12599 11674 603 41 0 12558 0
vsize: 50396
[startup+380.017 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13321 0 0 0 37960 43 0 0 25 0 1 0 489054955 52277248 11852 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12763 11852 603 41 0 12722 0
vsize: 51052
[startup+390.018 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 38960 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+400.018 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 39960 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223808 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 40960 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 41961 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 42960 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 43960 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 44960 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 45961 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 46961 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 47961 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 48961 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 49961 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 50962 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 51962 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13461 0 0 0 52962 44 0 0 25 0 1 0 489054955 52944896 11992 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11992 603 41 0 12885 0
vsize: 51704
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13462 0 0 0 53962 44 0 0 25 0 1 0 489054955 52944896 11993 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11993 603 41 0 12885 0
vsize: 51704
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13462 0 0 0 54962 44 0 0 25 0 1 0 489054955 52944896 11993 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11993 603 41 0 12885 0
vsize: 51704
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13462 0 0 0 55962 44 0 0 25 0 1 0 489054955 52944896 11993 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11993 603 41 0 12885 0
vsize: 51704
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13462 0 0 0 56963 44 0 0 25 0 1 0 489054955 52944896 11993 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11993 603 41 0 12885 0
vsize: 51704
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13463 0 0 0 57963 44 0 0 25 0 1 0 489054955 52944896 11994 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11994 603 41 0 12885 0
vsize: 51704
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13463 0 0 0 58963 44 0 0 25 0 1 0 489054955 52944896 11994 4294967295 134512640 134672761 3221224624 3221223808 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11994 603 41 0 12885 0
vsize: 51704
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13463 0 0 0 59963 44 0 0 25 0 1 0 489054955 52944896 11994 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11994 603 41 0 12885 0
vsize: 51704
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13463 0 0 0 60963 44 0 0 25 0 1 0 489054955 52944896 11994 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11994 603 41 0 12885 0
vsize: 51704
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13463 0 0 0 61963 44 0 0 25 0 1 0 489054955 52944896 11994 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11994 603 41 0 12885 0
vsize: 51704
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13463 0 0 0 62963 44 0 0 25 0 1 0 489054955 52944896 11994 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11994 603 41 0 12885 0
vsize: 51704
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13463 0 0 0 63964 44 0 0 25 0 1 0 489054955 52944896 11994 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12926 11994 603 41 0 12885 0
vsize: 51704
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13574 0 0 0 64964 44 0 0 25 0 1 0 489054955 53342208 12105 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13023 12105 603 41 0 12982 0
vsize: 52092
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13726 0 0 0 65963 45 0 0 25 0 1 0 489054955 54009856 12257 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13186 12257 603 41 0 13145 0
vsize: 52744
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13852 0 0 0 66963 45 0 0 25 0 1 0 489054955 54546432 12383 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13317 12383 603 41 0 13276 0
vsize: 53268
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 13996 0 0 0 67963 45 0 0 25 0 1 0 489054955 55087104 12527 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13449 12527 603 41 0 13408 0
vsize: 53796
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 14188 0 0 0 68962 46 0 0 25 0 1 0 489054955 55885824 12719 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13644 12719 603 41 0 13603 0
vsize: 54576
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 14346 0 0 0 69962 47 0 0 25 0 1 0 489054955 56553472 12877 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13807 12877 603 41 0 13766 0
vsize: 55228
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 14501 0 0 0 70962 47 0 0 25 0 1 0 489054955 57081856 13032 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13936 13032 603 41 0 13895 0
vsize: 55744
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 14644 0 0 0 71961 48 0 0 25 0 1 0 489054955 57745408 13175 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14098 13175 603 41 0 14057 0
vsize: 56392
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 14763 0 0 0 72961 48 0 0 25 0 1 0 489054955 58146816 13294 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14196 13294 603 41 0 14155 0
vsize: 56784
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 14902 0 0 0 73960 49 0 0 25 0 1 0 489054955 58806272 13433 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14357 13433 603 41 0 14316 0
vsize: 57428
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15049 0 0 0 74960 50 0 0 25 0 1 0 489054955 59334656 13580 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14486 13580 603 41 0 14445 0
vsize: 57944
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15177 0 0 0 75960 50 0 0 25 0 1 0 489054955 59867136 13708 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14616 13708 603 41 0 14575 0
vsize: 58464
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15300 0 0 0 76960 50 0 0 25 0 1 0 489054955 60403712 13831 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14747 13831 603 41 0 14706 0
vsize: 58988
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 77960 50 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 78960 50 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 79960 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 80960 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 81960 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 82960 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 83961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 84961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 85961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 86961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 87961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 88960 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 89961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 90961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 91961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 92961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 93961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 94961 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 95962 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 96962 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 97962 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 98962 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 99962 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 100962 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 101962 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 102963 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 103963 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 104963 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 105963 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 106963 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 107964 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 108964 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15378 0 0 0 109964 51 0 0 25 0 1 0 489054955 60669952 13909 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14812 13909 603 41 0 14771 0
vsize: 59248
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15533 0 0 0 110963 52 0 0 25 0 1 0 489054955 61345792 14064 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14977 14064 603 41 0 14936 0
vsize: 59908
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15743 0 0 0 111963 53 0 0 25 0 1 0 489054955 62144512 14274 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15172 14274 603 41 0 15131 0
vsize: 60688
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 15939 0 0 0 112962 53 0 0 25 0 1 0 489054955 62943232 14470 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15367 14470 603 41 0 15326 0
vsize: 61468
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 16115 0 0 0 113962 54 0 0 25 0 1 0 489054955 63733760 14646 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15560 14646 603 41 0 15519 0
vsize: 62240
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 16318 0 0 0 114961 54 0 0 25 0 1 0 489054955 64528384 14849 4294967295 134512640 134672761 3221224624 3221223800 134553585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15754 14849 603 41 0 15713 0
vsize: 63016
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 16445 0 0 0 115961 55 0 0 25 0 1 0 489054955 65069056 14976 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15886 14976 603 41 0 15845 0
vsize: 63544
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 16648 0 0 0 116961 55 0 0 25 0 1 0 489054955 65871872 15179 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16082 15179 603 41 0 16041 0
vsize: 64328
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 16857 0 0 0 117961 56 0 0 25 0 1 0 489054955 66805760 15388 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16310 15388 603 41 0 16269 0
vsize: 65240
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 17056 0 0 0 118960 56 0 0 25 0 1 0 489054955 67596288 15587 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16503 15587 603 41 0 16462 0
vsize: 66012
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 12264
Raw data (stat): 12264 (minisat+) R 12263 5897 5896 0 -1 0 17319 0 0 0 119959 57 0 0 25 0 1 0 489054955 68669440 15850 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16765 15850 603 41 0 16724 0
vsize: 67060
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.94 1/54 12264
Raw data (stat): 12264 (minisat+) Z 12263 5897 5896 0 -1 12 17322 0 0 0 119960 60 0 0 25 0 1 0 489054955 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.07
CPU time (s): 1200.21
CPU user time (s): 1199.6
CPU system time (s): 0.608907
CPU usage (%): 100.012
Max. virtual memory (Kb): 67060
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####