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/miplib2003/normalized-mps-v2-13-7-pk1.opb
MD5SUM	9c5126d785c8d5465220e290c5fc25a6
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5120
Optimality of the best value was proved	NO
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	2421502
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	1175.04
Number of variables	675
Total number of constraints	100
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	45
Minimum length of a constraint	1
Maximum length of a constraint	95
Trace number 18509

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 15:16:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17898 boxname=wulflinc23 idbench=1377 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9c5126d785c8d5465220e290c5fc25a6  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pk1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pk1.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pk1.opb
IDLAUNCH: 17898
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        664296 kB
Buffers:         19216 kB
Cached:         325960 kB
SwapCached:        536 kB
Active:          25052 kB
Inactive:       322316 kB
HighTotal:      131008 kB
HighFree:        31976 kB
LowTotal:       903652 kB
LowFree:        632320 kB
SwapTotal:     2097136 kB
SwapFree:      2095852 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            17384 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:36:33 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 17898 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 60 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############
c   -- Clauses(.)/Splits(s): (none)
c ---[  58]---> Adder-cost: 358   maxlim: 1151871   bits: 22/21
c ---[  56]---> Adder-cost: 382   maxlim: 1183231   bits: 22/21
c ---[  54]---> Adder-cost: 338   maxlim: 1135231   bits: 22/21
c ---[  52]---> Adder-cost: 362   maxlim: 1185791   bits: 22/21
c ---[  50]---> Adder-cost: 360   maxlim: 1161855   bits: 22/21
c ---[  48]---> Adder-cost: 354   maxlim: 1184383   bits: 22/21
c ---[  46]---> Adder-cost: 362   maxlim: 1156479   bits: 22/21
c ---[  45]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  44]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  43]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  42]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  40]---> Adder-cost: 352   maxlim: 1176959   bits: 22/21
c ---[  39]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  38]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  37]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  36]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  35]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  34]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  33]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  32]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  31]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  30]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  28]---> Adder-cost: 368   maxlim: 1155967   bits: 22/21
c ---[  27]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  26]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  25]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  24]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  23]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  22]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  21]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  20]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  19]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  18]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  16]---> Adder-cost: 362   maxlim: 1178367   bits: 22/21
c ---[  15]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  14]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  13]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  12]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  11]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[  10]---> Adder-cost: 40   maxlim: 1048574   bits: 21/20
c ---[   8]---> Adder-cost: 374   maxlim: 1184767   bits: 22/21
c ---[   6]---> Adder-cost: 348   maxlim: 1169791   bits: 22/21
c ---[   4]---> Adder-cost: 352   maxlim: 1145087   bits: 22/21
c ---[   2]---> Adder-cost: 368   maxlim: 1171455   bits: 22/21
c ---[   0]---> Adder-cost: 384   maxlim: 1175295   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   44643   163785 |   14881       0        0     nan |  0.000 % |
c |       100 |   44637   163767 |   16369      99      360     3.6 | 15.169 % |
c |       250 |   44637   163767 |   18006     249     2380     9.6 | 15.169 % |
c |       475 |   44613   163689 |   19806     471     3899     8.3 | 15.206 % |
c |       813 |   44583   163593 |   21787     805     6732     8.4 | 15.254 % |
c |      1319 |   44543   163463 |   23965    1306    10907     8.4 | 15.315 % |
c |      2078 |   44521   163393 |   26362    2062    18672     9.1 | 15.352 % |
c |      3220 |   44513   163367 |   28998    3203    40631    12.7 | 15.364 % |
c |      4928 |   44465   163211 |   31898    4905    67351    13.7 | 15.437 % |
c |      7490 |   44419   163063 |   35088    7461   130133    17.4 | 15.510 % |
c |     11334 |   44391   162975 |   38597   11301   205861    18.2 | 15.559 % |
c |     17102 |   44032   161802 |   42457   16979   327028    19.3 | 16.168 % |
c ==============================================================================
c [1mFound solution: 56448[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 21   maxlim: 9087   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20514 |   43296   159101 |   14432   19377   358891    18.5 | 16.168 % |
c |     20614 |   43296   159101 |   15875    9789   185626    19.0 | 16.495 % |
c |     20765 |   43296   159101 |   17462    9940   187205    18.8 | 16.495 % |
c |     20991 |   43290   159083 |   19208   10165   190332    18.7 | 16.507 % |
c |     21328 |   43246   158937 |   21129   10488   194208    18.5 | 16.580 % |
c |     21834 |   43246   158937 |   23242   10994   206762    18.8 | 16.580 % |
c |     22594 |   43246   158937 |   25567   11754   219606    18.7 | 16.580 % |
c |     23734 |   43221   158850 |   28123   12891   238586    18.5 | 16.616 % |
c |     25442 |   43171   158686 |   30936   14587   295309    20.2 | 16.701 % |
c |     28004 |   43171   158686 |   34029   17149   392460    22.9 | 16.701 % |
c |     31848 |   43103   158460 |   37432   20978   495319    23.6 | 16.810 % |
c |     37615 |   43103   158460 |   41176   26745   760999    28.5 | 16.810 % |
c |     46265 |   42995   158088 |   45293   35370  1043445    29.5 | 16.968 % |
c |     59239 |   42995   158088 |   49823   14699   573160    39.0 | 16.968 % |
c |     78701 |   42995   158088 |   54805   34161  1361014    39.8 | 16.968 % |
c ==============================================================================
c [1mFound solution: 33728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 18   maxlim: 31807   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    100914 |   43005   158140 |   14335   56356  2519215    44.7 | 16.968 % |
c |    101014 |   43005   158140 |   15768   15016   748156    49.8 | 17.125 % |
c |    101164 |   43005   158140 |   17345   15166   749072    49.4 | 17.125 % |
c |    101390 |   42985   158068 |   19079   15389   751465    48.8 | 17.149 % |
c |    101727 |   42975   158032 |   20987   15724   757922    48.2 | 17.161 % |
c |    102233 |   42975   158032 |   23086   16230   764521    47.1 | 17.161 % |
c |    102992 |   42965   157996 |   25395   16988   781191    46.0 | 17.173 % |
c |    104131 |   42955   157960 |   27934   18125   812063    44.8 | 17.185 % |
c |    105840 |   42955   157960 |   30728   19834   854014    43.1 | 17.185 % |
c |    108402 |   42913   157816 |   33801   22391   903083    40.3 | 17.246 % |
c |    112248 |   42862   157647 |   37181   26222  1021820    39.0 | 17.330 % |
c ==============================================================================
c [1mFound solution: 18945[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 28   maxlim: 13822   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    114972 |   42680   157045 |   14226   28829  1085588    37.7 | 17.330 % |
c |    115073 |   42680   157045 |   15648   12390   286155    23.1 | 17.572 % |
c |    115223 |   42680   157045 |   17213   12540   288346    23.0 | 17.572 % |
c |    115448 |   42670   157009 |   18934   12757   292122    22.9 | 17.584 % |
c |    115785 |   42670   157009 |   20828   13094   302829    23.1 | 17.584 % |
c |    116291 |   42670   157009 |   22911   13600   311900    22.9 | 17.584 % |
c |    117050 |   42670   157009 |   25202   14359   327097    22.8 | 17.584 % |
c |    118191 |   42653   156950 |   27722   15497   351595    22.7 | 17.608 % |
c |    119900 |   42616   156827 |   30494   17192   405044    23.6 | 17.668 % |
c |    122462 |   42606   156791 |   33544   19753   482028    24.4 | 17.680 % |
c ==============================================================================
c [1mFound solution: 15617[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Adder-cost: 20   maxlim: 766   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    123833 |   42354   155914 |   14118   20543   495214    24.1 | 17.680 % |
c |    123935 |   42354   155914 |   15529   10374   225675    21.8 | 17.905 % |
c |    124085 |   42354   155914 |   17082   10524   228943    21.8 | 17.905 % |
c |    124310 |   42354   155914 |   18791   10749   231412    21.5 | 17.905 % |
c |    124648 |   42296   155706 |   20670   11041   234116    21.2 | 17.977 % |
c |    125154 |   42296   155706 |   22737   11547   245315    21.2 | 17.977 % |
c |    125913 |   42288   155678 |   25010   12305   260219    21.1 | 17.989 % |
c |    127052 |   42258   155570 |   27511   13429   291141    21.7 | 18.025 % |
c ==============================================================================
c [1mFound solution: 13824[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 9   maxlim: 2559   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127741 |   42285   155659 |   14095   14117   301946    21.4 | 18.025 % |
c |    127841 |   42285   155659 |   15504   14217   303254    21.3 | 18.037 % |
c |    127991 |   42285   155659 |   17054   14367   305003    21.2 | 18.037 % |
c |    128216 |   42285   155659 |   18760   14592   308667    21.2 | 18.037 % |
c |    128557 |   42285   155659 |   20636   14933   315258    21.1 | 18.037 % |
c |    129063 |   42265   155587 |   22700   15436   325397    21.1 | 18.061 % |
c |    129822 |   42257   155559 |   24970   16189   348753    21.5 | 18.073 % |
c |    130963 |   42241   155503 |   27467   17328   379284    21.9 | 18.097 % |
c |    132672 |   42241   155503 |   30213   19037   429378    22.6 | 18.097 % |
c |    135235 |   42213   155403 |   33235   21586   507351    23.5 | 18.133 % |
c |    139079 |   42213   155403 |   36558   25430   629090    24.7 | 18.133 % |
c |    144846 |   42165   155231 |   40214   31174   815529    26.2 | 18.193 % |
c |    153496 |   42149   155175 |   44236   39817  1174722    29.5 | 18.217 % |
c |    166470 |   42149   155175 |   48659   20504   803980    39.2 | 18.217 % |
c |    185931 |   42101   155003 |   53525   39960  1559101    39.0 | 18.277 % |
c |    215123 |   42036   154772 |   58878   27804   924848    33.3 | 18.360 % |
c ==============================================================================
c [1mFound solution: 11776[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 4607   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    237747 |   42024   154723 |   14008   50421  1848270    36.7 | 18.360 % |
c |    237848 |   42024   154723 |   15408   13725   505657    36.8 | 18.422 % |
c |    237998 |   42024   154723 |   16949   13875   508306    36.6 | 18.422 % |
c |    238223 |   42024   154723 |   18644   14100   510342    36.2 | 18.422 % |
c |    238562 |   42014   154687 |   20509   14437   517924    35.9 | 18.434 % |
c |    239069 |   42006   154659 |   22560   14938   524058    35.1 | 18.446 % |
c |    239828 |   42006   154659 |   24816   15697   544528    34.7 | 18.446 % |
c |    240967 |   41998   154631 |   27297   16833   582818    34.6 | 18.458 % |
c |    242675 |   41998   154631 |   30027   18541   644160    34.7 | 18.458 % |
c |    245237 |   41998   154631 |   33030   21103   742491    35.2 | 18.458 % |
c |    249081 |   41998   154631 |   36333   24947   875147    35.1 | 18.458 % |
c |    254847 |   41998   154631 |   39966   30713  1085655    35.3 | 18.458 % |
c |    263496 |   41998   154631 |   43963   39362  1425877    36.2 | 18.458 % |
c |    276471 |   41956   154483 |   48359   20739   737996    35.6 | 18.518 % |
c |    295932 |   41956   154483 |   53195   40200  1510341    37.6 | 18.518 % |
c |    325124 |   41956   154483 |   58514   28920  1135599    39.3 | 18.518 % |
c |    368913 |   41956   154483 |   64366   28147  1119823    39.8 | 18.518 % |
c |    434597 |   41948   154455 |   70803   43261  1715326    39.7 | 18.530 % |
c |    533123 |   41914   154335 |   77883   28463  1244831    43.7 | 18.590 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1_bit_7 -x1_bit_6 -x1_bit_5 -x1_bit_4 -x1_bit_3 -x1_bit_2 -x1_bit_1 -x1_bit0 -x1_bit1 x1_bit2 x1_bit3 x1_bit4 -x1_bit5 x1_bit6 -x1_bit7 -x1_bit8 -x1_bit9 -x1_bit10 -x1_bit11 -x1_bit12 x2_bit0 -x3_bit0 x4_bit0 -x5_bit0 -x6_bit0 -x7_bit0 -x8_bit0 -x9_bit0 x10_bit0 x11_bit0 x12_bit0 -x13_bit0 -x14_bit0 -x15_bit0 -x16_bit0 x17_bit0 x18_bit0 x19_bit0 x20_bit0 x21_bit0 -x22_bit0 -x23_bit0 x24_bit0 -x25_bit0 -x26_bit0 x27_bit0 x28_bit0 -x29_bit0 -x30_bit0 -x31_bit0 -x32_bit0 -x33_bit0 -x34_bit0 -x35_bit0 x36_bit0 x37_bit0 -x38_bit0 -x39_bit0 -x40_bit0 -x41_bit0 x42_bit0 -x43_bit0 x44_bit0 x45_bit0 x46_bit0 -x47_bit0 x48_bit0 -x49_bit0 x50_bit0 -x51_bit0 x52_bit0 x53_bit0 -x54_bit0 x55_bit0 -x56_bit0 -x57_bit_7 -x57_bit_6 -x57_bit_5 -x57_bit_4 -x57_bit_3 -x57_bit_2 -x57_bit_1 -x57_bit0 x57_bit1 -x57_bit2 -x57_bit3 -x57_bit4 -x57_bit5 x57_bit6 -x57_bit7 -x57_bit8 -x57_bit9 -x57_bit10 -x57_bit11 -x57_bit12 -x58_bit_7 -x58_bit_6 -x58_bit_5 -x58_bit_4 -x58_bit_3 -x58_bit_2 -x58_bit_1 -x58_bit0 -x58_bit1 -x58_bit2 -x58_bit3 -x58_bit4 -x58_bit5 -x58_bit6 -x58_bit7 -x58_bit8 -x58_bit9 -x58_bit10 -x58_bit11 -x58_bit12 -x75_bit_7 -x75_bit_6 -x75_bit_5 -x75_bit_4 -x75_bit_3 -x75_bit_2 -x75_bit_1 -x75_bit0 x75_bit1 x75_bit2 x75_bit3 -x75_bit4 x75_bit5 -x75_bit6 -x75_bit7 -x75_bit8 -x75_bit9 -x75_bit10 -x75_bit11 -x75_bit12 -x76_bit_7 -x76_bit_6 -x76_bit_5 -x76_bit_4 -x76_bit_3 -x76_bit_2 -x76_bit_1 -x76_bit0 -x76_bit1 -x76_bit2 -x76_bit3 x76_bit4 -x76_bit5 x76_bit6 -x76_bit7 -x76_bit8 -x76_bit9 -x76_bit10 -x76_bit11 -x76_bit12 -x77_bit_7 -x77_bit_6 -x77_bit_5 -x77_bit_4 -x77_bit_3 -x77_bit_2 -x77_bit_1 -x77_bit0 -x77_bit1 x77_bit2 x77_bit3 x77_bit4 -x77_bit5 x77_bit6 -x77_bit7 -x77_bit8 -x77_bit9 -x77_bit10 -x77_bit11 -x77_bit12 -x78_bit_7 -x78_bit_6 -x78_bit_5 -x78_bit_4 -x78_bit_3 -x78_bit_2 -x78_bit_1 x78_bit0 -x78_bit1 -x78_bit2 -x78_bit3 -x78_bit4 -x78_bit5 -x78_bit6 -x78_bit7 -x78_bit8 -x78_bit9 -x78_bit10 -x78_bit11 -x78_bit12 -x79_bit_7 -x79_bit_6 -x79_bit_5 -x79_bit_4 -x79_bit_3 -x79_bit_2 -x79_bit_1 x79_bit0 -x79_bit1 -x79_bit2 x79_bit3 -x79_bit4 -x79_bit5 -x79_bit6 -x79_bit7 -x79_bit8 -x79_bit9 -x79_bit10 -x79_bit11 -x79_bit12 -x80_bit_7 -x80_bit_6 -x80_bit_5 -x80_bit_4 -x80_bit_3 -x80_bit_2 -x80_bit_1 -x80_bit0 -x80_bit1 x80_bit2 -x80_bit3 x80_bit4 -x80_bit5 x80_bit6 -x80_bit7 -x80_bit8 -x80_bit9 -x80_bit10 -x80_bit11 -x80_bit12 -x81_bit_7 -x81_bit_6 -x81_bit_5 -x81_bit_4 -x81_bit_3 -x81_bit_2 -x81_bit_1 -x81_bit0 -x81_bit1 -x81_bit2 -x81_bit3 -x81_bit4 -x81_bit5 -x81_bit6 -x81_bit7 -x81_bit8 -x81_bit9 -x81_bit10 -x81_bit11 -x81_bit12 -x82_bit_7 -x82_bit_6 -x82_bit_5 -x82_bit_4 -x82_bit_3 -x82_bit_2 -x82_bit_1 -x82_bit0 -x82_bit1 x82_bit2 x82_bit3 -x82_bit4 -x82_bit5 -x82_bit6 -x82_bit7 -x82_bit8 -x82_bit9 -x82_bit10 -x82_bit11 -x82_bit12 -x83_bit_7 -x83_bit_6 -x83_bit_5 -x83_bit_4 -x83_bit_3 -x83_bit_2 -x83_bit_1 x83_bit0 x83_bit1 x83_bit2 -x83_bit3 x83_bit4 -x83_bit5 x83_bit6 -x83_bit7 -x83_bit8 -x83_bit9 -x83_bit10 -x83_bit11 -x83_bit12 -x84_bit_7 -x84_bit_6 -x84_bit_5 -x84_bit_4 -x84_bit_3 -x84_bit_2 -x84_bit_1 -x84_bit0 -x84_bit1 x84_bit2 x84_bit3 x84_bit4 -x84_bit5 x84_bit6 -x84_bit7 -x84_bit8 -x84_bit9 -x84_bit10 -x84_bit11 -x84_bit12 -x85_bit_7 -x85_bit_6 -x85_bit_5 -x85_bit_4 -x85_bit_3 -x85_bit_2 -x85_bit_1 -x85_bit0 -x85_bit1 -x85_bit2 x85_bit3 -x85_bit4 x85_bit5 -x85_bit6 -x85_bit7 -x85_bit8 -x85_bit9 -x85_bit10 -x85_bit11 -x85_bit12 -x86_bit_7 -x86_bit_6 -x86_bit_5 -x86_bit_4 -x86_bit_3 -x86_bit_2 -x86_bit_1 -x86_bit0 x86_bit1 -x86_bit2 -x86_bit3 -x86_bit4 -x86_bit5 x86_bit6 -x86_bit7 -x86_bit8 -x86_bit9 -x86_bit10 -x86_bit11 -x86_bit12 -x59_bit_7 -x59_bit_6 -x59_bit_5 -x59_bit_4 -x59_bit_3 -x59_bit_2 -x59_bit_1 -x59_bit0 x59_bit1 -x59_bit2 -x59_bit3 -x59_bit4 x59_bit5 -x59_bit6 -x59_bit7 -x59_bit8 -x59_bit9 -x59_bit10 -x59_bit11 -x59_bit12 -x60_bit_7 -x60_bit_6 -x60_bit_5 -x60_bit_4 -x60_bit_3 -x60_bit_2 -x60_bit_1 -x60_bit0 -x60_bit1 x60_bit2 x60_bit3 x60_bit4 -x60_bit5 x60_bit6 -x60_bit7 -x60_bit8 -x60_bit9 -x60_bit10 -x60_bit11 -x60_bit12 -x61_bit_7 -x61_bit_6 -x61_bit_#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.93 2/54 7368
Raw data (stat): 7368 (runsolver) R 7367 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546089152 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.0003 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 1731 0 0 0 995 4 0 0 25 0 1 0 546089152 9371648 1705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2288 1705 603 41 0 2247 0
vsize: 9152
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 1923 0 0 0 1994 5 0 0 25 0 1 0 546089152 10129408 1897 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2473 1897 603 41 0 2432 0
vsize: 9892
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 2270 0 0 0 2991 7 0 0 25 0 1 0 546089152 11608064 2244 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2834 2244 603 41 0 2793 0
vsize: 11336
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 2572 0 0 0 3990 9 0 0 25 0 1 0 546089152 12824576 2546 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3131 2546 603 41 0 3090 0
vsize: 12524
[startup+50.0035 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 2891 0 0 0 4989 10 0 0 25 0 1 0 546089152 14159872 2865 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3457 2865 603 41 0 3416 0
vsize: 13828
[startup+60.0033 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 3139 0 0 0 5988 11 0 0 25 0 1 0 546089152 15220736 3113 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3716 3113 603 41 0 3675 0
vsize: 14864
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 3337 0 0 0 6987 13 0 0 25 0 1 0 546089152 16023552 3311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3912 3311 603 41 0 3871 0
vsize: 15648
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 3337 0 0 0 7987 13 0 0 25 0 1 0 546089152 16023552 3311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3912 3311 603 41 0 3871 0
vsize: 15648
[startup+90.0032 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 3346 0 0 0 8987 13 0 0 25 0 1 0 546089152 16023552 3320 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3912 3320 603 41 0 3871 0
vsize: 15648
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 3348 0 0 0 9987 13 0 0 25 0 1 0 546089152 16023552 3322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3912 3322 603 41 0 3871 0
vsize: 15648
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 3403 0 0 0 10987 13 0 0 25 0 1 0 546089152 16293888 3377 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3978 3377 603 41 0 3937 0
vsize: 15912
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 3707 0 0 0 11986 14 0 0 25 0 1 0 546089152 17502208 3681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4273 3681 603 41 0 4232 0
vsize: 17092
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 3930 0 0 0 12985 15 0 0 25 0 1 0 546089152 18448384 3904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4504 3904 603 41 0 4463 0
vsize: 18016
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4184 0 0 0 13984 17 0 0 25 0 1 0 546089152 19513344 4158 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4764 4158 603 41 0 4723 0
vsize: 19056
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4435 0 0 0 14984 17 0 0 25 0 1 0 546089152 20574208 4409 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5023 4409 603 41 0 4982 0
vsize: 20092
[startup+160.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4562 0 0 0 15983 18 0 0 25 0 1 0 546089152 20979712 4536 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4536 603 41 0 5081 0
vsize: 20488
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4563 0 0 0 16984 18 0 0 25 0 1 0 546089152 20979712 4537 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4537 603 41 0 5081 0
vsize: 20488
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 17984 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 18984 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 19984 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+210.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 20984 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+220.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 21984 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 22985 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+240.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 23985 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 24985 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+260.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 25985 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+270.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 26985 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+280.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 27985 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+290.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 28985 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+300.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 29986 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+310.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 30986 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+320.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 31986 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+330.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 32986 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+340.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 33986 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+350.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 34986 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+360.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 35987 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+370.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 36987 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+380.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 37987 18 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+390.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 38986 19 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+400.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 39986 19 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+410.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 40986 19 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223736 134554697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+420.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 41986 19 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+430.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 42986 19 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+440.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 43987 19 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+450.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 44986 19 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+460.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 45987 19 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+470.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4564 0 0 0 46987 19 0 0 25 0 1 0 546089152 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4538 603 41 0 5081 0
vsize: 20488
[startup+480.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4576 0 0 0 47987 19 0 0 25 0 1 0 546089152 21114880 4550 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5155 4550 603 41 0 5114 0
vsize: 20620
[startup+490.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4726 0 0 0 48987 20 0 0 25 0 1 0 546089152 21655552 4700 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5287 4700 603 41 0 5246 0
vsize: 21148
[startup+500.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4799 0 0 0 49987 20 0 0 25 0 1 0 546089152 22061056 4773 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4773 603 41 0 5345 0
vsize: 21544
[startup+510.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4802 0 0 0 50987 20 0 0 25 0 1 0 546089152 22061056 4776 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4776 603 41 0 5345 0
vsize: 21544
[startup+520.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4802 0 0 0 51987 20 0 0 25 0 1 0 546089152 22061056 4776 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4776 603 41 0 5345 0
vsize: 21544
[startup+530.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4806 0 0 0 52987 20 0 0 25 0 1 0 546089152 22061056 4780 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4780 603 41 0 5345 0
vsize: 21544
[startup+540.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4806 0 0 0 53987 20 0 0 25 0 1 0 546089152 22061056 4780 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4780 603 41 0 5345 0
vsize: 21544
[startup+550.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4806 0 0 0 54988 20 0 0 25 0 1 0 546089152 22061056 4780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4780 603 41 0 5345 0
vsize: 21544
[startup+560.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4806 0 0 0 55988 20 0 0 25 0 1 0 546089152 22061056 4780 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4780 603 41 0 5345 0
vsize: 21544
[startup+570.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 4814 0 0 0 56988 20 0 0 25 0 1 0 546089152 22061056 4788 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4788 603 41 0 5345 0
vsize: 21544
[startup+580.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5015 0 0 0 57987 21 0 0 25 0 1 0 546089152 22867968 4989 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5583 4989 603 41 0 5542 0
vsize: 22332
[startup+590.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5183 0 0 0 58986 22 0 0 25 0 1 0 546089152 23531520 5157 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5745 5157 603 41 0 5704 0
vsize: 22980
[startup+600.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5369 0 0 0 59985 23 0 0 25 0 1 0 546089152 24338432 5343 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5942 5343 603 41 0 5901 0
vsize: 23768
[startup+610.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5426 0 0 0 60985 24 0 0 25 0 1 0 546089152 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+620.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5426 0 0 0 61986 24 0 0 25 0 1 0 546089152 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+630.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5426 0 0 0 62986 24 0 0 25 0 1 0 546089152 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+640.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5426 0 0 0 63986 24 0 0 25 0 1 0 546089152 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+650.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5426 0 0 0 64986 24 0 0 25 0 1 0 546089152 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+660.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5426 0 0 0 65986 24 0 0 25 0 1 0 546089152 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+670.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5426 0 0 0 66986 24 0 0 25 0 1 0 546089152 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+680.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5426 0 0 0 67987 24 0 0 25 0 1 0 546089152 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+690.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5426 0 0 0 68987 24 0 0 25 0 1 0 546089152 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+700.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5426 0 0 0 69987 24 0 0 25 0 1 0 546089152 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+710.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5531 0 0 0 70986 24 0 0 25 0 1 0 546089152 25010176 5505 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6106 5505 603 41 0 6065 0
vsize: 24424
[startup+720.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 71986 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+730.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 72986 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+740.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 73987 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+750.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 74987 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+760.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 75987 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+770.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 76987 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+780.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 77987 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+790.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 78986 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+800.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 79986 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+810.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 80986 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+820.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5623 0 0 0 81986 25 0 0 25 0 1 0 546089152 25681920 5597 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+830.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5659 0 0 0 82986 25 0 0 25 0 1 0 546089152 25812992 5633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6302 5633 603 41 0 6261 0
vsize: 25208
[startup+840.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5816 0 0 0 83986 26 0 0 25 0 1 0 546089152 26484736 5790 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6466 5790 603 41 0 6425 0
vsize: 25864
[startup+850.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 5967 0 0 0 84986 26 0 0 25 0 1 0 546089152 27033600 5941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6600 5941 603 41 0 6559 0
vsize: 26400
[startup+860.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6107 0 0 0 85985 27 0 0 25 0 1 0 546089152 27713536 6081 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6766 6081 603 41 0 6725 0
vsize: 27064
[startup+870.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6182 0 0 0 86985 27 0 0 25 0 1 0 546089152 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+880.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6182 0 0 0 87985 27 0 0 25 0 1 0 546089152 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+890.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6182 0 0 0 88985 27 0 0 25 0 1 0 546089152 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+900.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6182 0 0 0 89986 27 0 0 25 0 1 0 546089152 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+910.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6182 0 0 0 90986 27 0 0 25 0 1 0 546089152 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+920.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6182 0 0 0 91986 27 0 0 25 0 1 0 546089152 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+930.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6182 0 0 0 92986 27 0 0 25 0 1 0 546089152 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+940.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6182 0 0 0 93986 27 0 0 25 0 1 0 546089152 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+950.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6182 0 0 0 94987 27 0 0 25 0 1 0 546089152 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+960.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6187 0 0 0 95987 27 0 0 25 0 1 0 546089152 27975680 6161 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6161 603 41 0 6789 0
vsize: 27320
[startup+970.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6192 0 0 0 96987 27 0 0 25 0 1 0 546089152 27975680 6166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6166 603 41 0 6789 0
vsize: 27320
[startup+980.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6192 0 0 0 97987 27 0 0 25 0 1 0 546089152 27975680 6166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6166 603 41 0 6789 0
vsize: 27320
[startup+990.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6193 0 0 0 98987 28 0 0 25 0 1 0 546089152 27975680 6167 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6167 603 41 0 6789 0
vsize: 27320
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6193 0 0 0 99987 28 0 0 25 0 1 0 546089152 27975680 6167 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6167 603 41 0 6789 0
vsize: 27320
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6261 0 0 0 100987 28 0 0 25 0 1 0 546089152 28246016 6235 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6896 6235 603 41 0 6855 0
vsize: 27584
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6398 0 0 0 101986 29 0 0 25 0 1 0 546089152 28925952 6372 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6372 603 41 0 7021 0
vsize: 28248
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 102986 29 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 103986 29 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 104986 29 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 105986 29 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 106985 29 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 107985 29 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 108986 29 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 109986 30 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 110987 30 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 111987 30 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 112987 30 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6411 0 0 0 113988 30 0 0 25 0 1 0 546089152 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6487 0 0 0 114988 30 0 0 25 0 1 0 546089152 29192192 6461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7127 6461 603 41 0 7086 0
vsize: 28508
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6668 0 0 0 115987 31 0 0 25 0 1 0 546089152 29986816 6642 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7321 6642 603 41 0 7280 0
vsize: 29284
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 6839 0 0 0 116986 32 0 0 25 0 1 0 546089152 30654464 6813 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7484 6813 603 41 0 7443 0
vsize: 29936
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 7002 0 0 0 117986 32 0 0 25 0 1 0 546089152 31379456 6976 4294967295 134512640 134672761 3221224544 3221223648 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7661 6976 603 41 0 7620 0
vsize: 30644
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 7154 0 0 0 118985 33 0 0 25 0 1 0 546089152 32092160 7128 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7835 7128 603 41 0 7794 0
vsize: 31340
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 7368
Raw data (stat): 7368 (minisat+) R 7367 3260 3259 0 -1 0 7286 0 0 0 119984 34 0 0 25 0 1 0 546089152 32620544 7260 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7964 7260 603 41 0 7923 0
vsize: 31856
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 7368
Raw data (stat): 7368 (minisat+) Z 7367 3260 3259 0 -1 12 7289 0 0 0 119985 35 0 0 25 0 1 0 546089152 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.04
CPU time (s): 1200.21
CPU user time (s): 1199.85
CPU system time (s): 0.358945
CPU usage (%): 100.014
Max. virtual memory (Kb): 31856
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####