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/miplib3/normalized-mps-v2-13-7-pk1.opb
MD5SUM	b6007187ad037f56a5e2b97a0b86cea8
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.03
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 14991

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        809372 kB
Buffers:         19328 kB
Cached:         175340 kB
SwapCached:         84 kB
Active:          21888 kB
Inactive:       175780 kB
HighTotal:      131008 kB
HighFree:        52976 kB
LowTotal:       903652 kB
LowFree:        756396 kB
SwapTotal:     2097892 kB
SwapFree:      2097776 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6628 kB
Slab:            21816 kB
Committed_AS:    63808 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:43:44 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 18756 7 1200.16 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 -d_bit_7 -d_bit_6 -d_bit_5 -d_bit_4 -d_bit_3 -d_bit_2 -d_bit_1 -d_bit0 -d_bit1 d_bit2 d_bit3 d_bit4 -d_bit5 d_bit6 -d_bit7 -d_bit8 -d_bit9 -d_bit10 -d_bit11 -d_bit12 X1_bit0 -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 -S1_bit_7 -S1_bit_6 -S1_bit_5 -S1_bit_4 -S1_bit_3 -S1_bit_2 -S1_bit_1 -S1_bit0 S1_bit1 -S1_bit2 -S1_bit3 -S1_bit4 -S1_bit5 S1_bit6 -S1_bit7 -S1_bit8 -S1_bit9 -S1_bit10 -S1_bit11 -S1_bit12 -T1_bit_7 -T1_bit_6 -T1_bit_5 -T1_bit_4 -T1_bit_3 -T1_bit_2 -T1_bit_1 -T1_bit0 -T1_bit1 -T1_bit2 -T1_bit3 -T1_bit4 -T1_bit5 -T1_bit6 -T1_bit7 -T1_bit8 -T1_bit9 -T1_bit10 -T1_bit11 -T1_bit12 -S10_bit_7 -S10_bit_6 -S10_bit_5 -S10_bit_4 -S10_bit_3 -S10_bit_2 -S10_bit_1 -S10_bit0 S10_bit1 S10_bit2 S10_bit3 -S10_bit4 S10_bit5 -S10_bit6 -S10_bit7 -S10_bit8 -S10_bit9 -S10_bit10 -S10_bit11 -S10_bit12 -T10_bit_7 -T10_bit_6 -T10_bit_5 -T10_bit_4 -T10_bit_3 -T10_bit_2 -T10_bit_1 -T10_bit0 -T10_bit1 -T10_bit2 -T10_bit3 T10_bit4 -T10_bit5 T10_bit6 -T10_bit7 -T10_bit8 -T10_bit9 -T10_bit10 -T10_bit11 -T10_bit12 -S11_bit_7 -S11_bit_6 -S11_bit_5 -S11_bit_4 -S11_bit_3 -S11_bit_2 -S11_bit_1 -S11_bit0 -S11_bit1 S11_bit2 S11_bit3 S11_bit4 -S11_bit5 S11_bit6 -S11_bit7 -S11_bit8 -S11_bit9 -S11_bit10 -S11_bit11 -S11_bit12 -T11_bit_7 -T11_bit_6 -T11_bit_5 -T11_bit_4 -T11_bit_3 -T11_bit_2 -T11_bit_1 T11_bit0 -T11_bit1 -T11_bit2 -T11_bit3 -T11_bit4 -T11_bit5 -T11_bit6 -T11_bit7 -T11_bit8 -T11_bit9 -T11_bit10 -T11_bit11 -T11_bit12 -S12_bit_7 -S12_bit_6 -S12_bit_5 -S12_bit_4 -S12_bit_3 -S12_bit_2 -S12_bit_1 S12_bit0 -S12_bit1 -S12_bit2 S12_bit3 -S12_bit4 -S12_bit5 -S12_bit6 -S12_bit7 -S12_bit8 -S12_bit9 -S12_bit10 -S12_bit11 -S12_bit12 -T12_bit_7 -T12_bit_6 -T12_bit_5 -T12_bit_4 -T12_bit_3 -T12_bit_2 -T12_bit_1 -T12_bit0 -T12_bit1 T12_bit2 -T12_bit3 T12_bit4 -T12_bit5 T12_bit6 -T12_bit7 -T12_bit8 -T12_bit9 -T12_bit10 -T12_bit11 -T12_bit12 -S13_bit_7 -S13_bit_6 -S13_bit_5 -S13_bit_4 -S13_bit_3 -S13_bit_2 -S13_bit_1 -S13_bit0 -S13_bit1 -S13_bit2 -S13_bit3 -S13_bit4 -S13_bit5 -S13_bit6 -S13_bit7 -S13_bit8 -S13_bit9 -S13_bit10 -S13_bit11 -S13_bit12 -T13_bit_7 -T13_bit_6 -T13_bit_5 -T13_bit_4 -T13_bit_3 -T13_bit_2 -T13_bit_1 -T13_bit0 -T13_bit1 T13_bit2 T13_bit3 -T13_bit4 -T13_bit5 -T13_bit6 -T13_bit7 -T13_bit8 -T13_bit9 -T13_bit10 -T13_bit11 -T13_bit12 -S14_bit_7 -S14_bit_6 -S14_bit_5 -S14_bit_4 -S14_bit_3 -S14_bit_2 -S14_bit_1 S14_bit0 S14_bit1 S14_bit2 -S14_bit3 S14_bit4 -S14_bit5 S14_bit6 -S14_bit7 -S14_bit8 -S14_bit9 -S14_bit10 -S14_bit11 -S14_bit12 -T14_bit_7 -T14_bit_6 -T14_bit_5 -T14_bit_4 -T14_bit_3 -T14_bit_2 -T14_bit_1 -T14_bit0 -T14_bit1 T14_bit2 T14_bit3 T14_bit4 -T14_bit5 T14_bit6 -T14_bit7 -T14_bit8 -T14_bit9 -T14_bit10 -T14_bit11 -T14_bit12 -S15_bit_7 -S15_bit_6 -S15_bit_5 -S15_bit_4 -S15_bit_3 -S15_bit_2 -S15_bit_1 -S15_bit0 -S15_bit1 -S15_bit2 S15_bit3 -S15_bit4 S15_bit5 -S15_bit6 -S15_bit7 -S15_bit8 -S15_bit9 -S15_bit10 -S15_bit11 -S15_bit12 -T15_bit_7 -T15_bit_6 -T15_bit_5 -T15_bit_4 -T15_bit_3 -T15_bit_2 -T15_bit_1 -T15_bit0 T15_bit1 -T15_bit2 -T15_bit3 -T15_bit4 -T15_bit5 T15_bit6 -T15_bit7 -T15_bit8 -T15_bit9 -T15_bit10 -T15_bit11 -T15_bit12 -S2_bit_7 -S2_bit_6 -S2_bit_5 -S2_bit_4 -S2_bit_3 -S2_bit_2 -S2_bit_1 -S2_bit0 S2_bit1 -S2_bit2 -S2_bit3 -S2_bit4 S2_bit5 -S2_bit6 -S2_bit7 -S2_bit8 -S2_bit9 -S2_bit10 -S2_bit11 -S2_bit12 -T2_bit_7 -T2_bit_6 -T2_bit_5 -T2_bit_4 -T2_bit_3 -T2_bit_2 -T2_bit_1 -T2_bit0 -T2_bit1 T2_bit2 T2_bit3 T2_bit4 -T2_bit5 T2_bit6 -T2_bit7 -T2_bit8 -T2_bit9 -T2_bit10 -T2_bit11 -T2_bit12 -S3_bit_7 -S3_bit_6 -S3_bit_5 -S3_bit_4 -S3_bit_3 -S3_bit_2 -S3_bit_1 -S3_bit0 -S3_bit1 -S3_bit2 S3_bit3 -S3_bit4 S3_bit5 -S3_bit6 -#### 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.77 0.92 0.94 2/55 21182
Raw data (stat): 21182 (runsolver) R 21181 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541460262 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0002 s]
Raw data (loadavg): 0.81 0.92 0.94 2/55 21182
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 1734 0 0 0 994 3 0 0 25 0 1 0 541460262 9371648 1708 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2288 1708 603 41 0 2247 0
vsize: 9152
[startup+20.0012 s]
Raw data (loadavg): 0.84 0.93 0.94 2/55 21182
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 1928 0 0 0 1994 4 0 0 25 0 1 0 541460262 10264576 1902 4294967295 134512640 134672761 3221224544 3221223744 134557867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2506 1902 603 41 0 2465 0
vsize: 10024
[startup+30.0018 s]
Raw data (loadavg): 0.86 0.93 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 2281 0 0 0 2990 6 0 0 25 0 1 0 541460262 11608064 2255 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2834 2255 603 41 0 2793 0
vsize: 11336
[startup+40.002 s]
Raw data (loadavg): 0.88 0.93 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 2585 0 0 0 3989 7 0 0 25 0 1 0 541460262 12824576 2559 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3131 2559 603 41 0 3090 0
vsize: 12524
[startup+50.003 s]
Raw data (loadavg): 0.90 0.93 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 2914 0 0 0 4988 9 0 0 25 0 1 0 541460262 14295040 2888 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3490 2888 603 41 0 3449 0
vsize: 13960
[startup+60.0036 s]
Raw data (loadavg): 0.99 0.95 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 3160 0 0 0 5987 10 0 0 25 0 1 0 541460262 15355904 3134 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3134 603 41 0 3708 0
vsize: 14996
[startup+70.0038 s]
Raw data (loadavg): 0.99 0.95 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 3337 0 0 0 6986 11 0 0 25 0 1 0 541460262 16023552 3311 4294967295 134512640 134672761 3221224544 3221223712 134561218 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.0037 s]
Raw data (loadavg): 0.99 0.95 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 3337 0 0 0 7986 11 0 0 25 0 1 0 541460262 16023552 3311 4294967295 134512640 134672761 3221224544 3221223712 134561220 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.0043 s]
Raw data (loadavg): 0.99 0.95 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 3346 0 0 0 8985 12 0 0 25 0 1 0 541460262 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.005 s]
Raw data (loadavg): 0.99 0.95 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 3348 0 0 0 9985 12 0 0 25 0 1 0 541460262 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.006 s]
Raw data (loadavg): 0.99 0.96 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 3503 0 0 0 10984 14 0 0 25 0 1 0 541460262 16695296 3477 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4076 3477 603 41 0 4035 0
vsize: 16304
[startup+120.006 s]
Raw data (loadavg): 0.99 0.96 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 3785 0 0 0 11982 16 0 0 25 0 1 0 541460262 17907712 3759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4372 3759 603 41 0 4331 0
vsize: 17488
[startup+130.005 s]
Raw data (loadavg): 0.99 0.96 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4019 0 0 0 12981 17 0 0 25 0 1 0 541460262 18849792 3993 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4602 3993 603 41 0 4561 0
vsize: 18408
[startup+140.006 s]
Raw data (loadavg): 0.99 0.96 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4272 0 0 0 13979 18 0 0 25 0 1 0 541460262 19775488 4246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4828 4246 603 41 0 4787 0
vsize: 19312
[startup+150.007 s]
Raw data (loadavg): 0.99 0.96 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4536 0 0 0 14978 20 0 0 25 0 1 0 541460262 20979712 4510 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5122 4510 603 41 0 5081 0
vsize: 20488
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4562 0 0 0 15978 20 0 0 25 0 1 0 541460262 20979712 4536 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.007 s]
Raw data (loadavg): 0.99 0.96 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4563 0 0 0 16978 20 0 0 25 0 1 0 541460262 20979712 4537 4294967295 134512640 134672761 3221224544 3221223728 134559045 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.007 s]
Raw data (loadavg): 0.99 0.96 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 17978 20 0 0 25 0 1 0 541460262 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+190.007 s]
Raw data (loadavg): 0.99 0.96 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 18978 21 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223728 134559622 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.007 s]
Raw data (loadavg): 0.99 0.96 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 19978 21 0 0 25 0 1 0 541460262 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+210.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 20978 21 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223728 134559161 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 21977 21 0 0 25 0 1 0 541460262 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+230.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 22977 22 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134561154 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 23977 22 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 24977 22 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560917 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.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 25977 22 0 0 25 0 1 0 541460262 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+270.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 26977 23 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 27976 23 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223744 134557836 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 28976 24 0 0 25 0 1 0 541460262 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+300.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 29976 24 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 30976 24 0 0 25 0 1 0 541460262 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+320.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21184
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 31976 24 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 32975 25 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134561167 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.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 33975 25 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223696 134565137 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.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 34975 25 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223648 134560218 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.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 35975 26 0 0 25 0 1 0 541460262 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+370.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 36975 26 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560867 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.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 37975 26 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134560942 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.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 38975 26 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223744 134557836 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.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 39975 26 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223744 134557892 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.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 40975 26 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134561207 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.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 41975 27 0 0 25 0 1 0 541460262 20979712 4538 4294967295 134512640 134672761 3221224544 3221223712 134561167 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.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 42974 27 0 0 25 0 1 0 541460262 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.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 43974 27 0 0 25 0 1 0 541460262 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+450.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 44974 27 0 0 25 0 1 0 541460262 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+460.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4564 0 0 0 45974 28 0 0 25 0 1 0 541460262 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.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4648 0 0 0 46974 28 0 0 25 0 1 0 541460262 21385216 4622 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5221 4622 603 41 0 5180 0
vsize: 20884
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4799 0 0 0 47974 29 0 0 25 0 1 0 541460262 22061056 4773 4294967295 134512640 134672761 3221224544 3221223360 134565829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4773 603 41 0 5345 0
vsize: 21544
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4799 0 0 0 48973 29 0 0 25 0 1 0 541460262 22061056 4773 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4773 603 41 0 5345 0
vsize: 21544
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4802 0 0 0 49973 29 0 0 25 0 1 0 541460262 22061056 4776 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4776 603 41 0 5345 0
vsize: 21544
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4806 0 0 0 50973 29 0 0 25 0 1 0 541460262 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+520.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4806 0 0 0 51973 30 0 0 25 0 1 0 541460262 22061056 4780 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4780 603 41 0 5345 0
vsize: 21544
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4806 0 0 0 52973 30 0 0 25 0 1 0 541460262 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+540.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4806 0 0 0 53973 30 0 0 25 0 1 0 541460262 22061056 4780 4294967295 134512640 134672761 3221224544 3221223712 134561164 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.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4808 0 0 0 54973 30 0 0 25 0 1 0 541460262 22061056 4782 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5386 4782 603 41 0 5345 0
vsize: 21544
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 4976 0 0 0 55972 31 0 0 25 0 1 0 541460262 22732800 4950 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5550 4950 603 41 0 5509 0
vsize: 22200
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5152 0 0 0 56972 32 0 0 25 0 1 0 541460262 23400448 5126 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5713 5126 603 41 0 5672 0
vsize: 22852
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5349 0 0 0 57970 33 0 0 25 0 1 0 541460262 24338432 5323 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5942 5323 603 41 0 5901 0
vsize: 23768
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5426 0 0 0 58970 33 0 0 25 0 1 0 541460262 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5426 0 0 0 59970 34 0 0 25 0 1 0 541460262 24604672 5400 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5400 603 41 0 5966 0
vsize: 24028
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5426 0 0 0 60970 34 0 0 25 0 1 0 541460262 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21186
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5426 0 0 0 61970 34 0 0 25 0 1 0 541460262 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560917 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.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5426 0 0 0 62970 34 0 0 25 0 1 0 541460262 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.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5426 0 0 0 63969 35 0 0 25 0 1 0 541460262 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5426 0 0 0 64969 35 0 0 25 0 1 0 541460262 24604672 5400 4294967295 134512640 134672761 3221224544 3221223712 134560833 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.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5426 0 0 0 65969 36 0 0 25 0 1 0 541460262 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.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5426 0 0 0 66969 36 0 0 25 0 1 0 541460262 24604672 5400 4294967295 134512640 134672761 3221224544 3221223744 134557900 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.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5427 0 0 0 67968 36 0 0 25 0 1 0 541460262 24604672 5401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6007 5401 603 41 0 5966 0
vsize: 24028
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5585 0 0 0 68967 37 0 0 25 0 1 0 541460262 25288704 5559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6174 5559 603 41 0 6133 0
vsize: 24696
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 69967 38 0 0 25 0 1 0 541460262 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+710.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 70967 38 0 0 25 0 1 0 541460262 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+720.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 71967 38 0 0 25 0 1 0 541460262 25681920 5597 4294967295 134512640 134672761 3221224544 3221223728 134558899 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.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 72967 38 0 0 25 0 1 0 541460262 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+740.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 73967 39 0 0 25 0 1 0 541460262 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+750.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 74967 39 0 0 25 0 1 0 541460262 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134560903 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.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 75967 39 0 0 25 0 1 0 541460262 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134560842 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.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 76966 39 0 0 25 0 1 0 541460262 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+780.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 77966 40 0 0 25 0 1 0 541460262 25681920 5597 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6270 5597 603 41 0 6229 0
vsize: 25080
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 78966 40 0 0 25 0 1 0 541460262 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+800.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5623 0 0 0 79966 41 0 0 25 0 1 0 541460262 25681920 5597 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5776 0 0 0 80964 42 0 0 25 0 1 0 541460262 26218496 5750 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6401 5750 603 41 0 6360 0
vsize: 25604
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 5937 0 0 0 81963 43 0 0 25 0 1 0 541460262 26898432 5911 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6567 5911 603 41 0 6526 0
vsize: 26268
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6084 0 0 0 82962 44 0 0 25 0 1 0 541460262 27570176 6058 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6731 6058 603 41 0 6690 0
vsize: 26924
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6182 0 0 0 83961 46 0 0 25 0 1 0 541460262 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6182 0 0 0 84961 46 0 0 25 0 1 0 541460262 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6182 0 0 0 85961 46 0 0 25 0 1 0 541460262 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6182 0 0 0 86961 46 0 0 25 0 1 0 541460262 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6182 0 0 0 87962 46 0 0 25 0 1 0 541460262 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6182 0 0 0 88962 46 0 0 25 0 1 0 541460262 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6182 0 0 0 89962 46 0 0 25 0 1 0 541460262 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6182 0 0 0 90962 46 0 0 25 0 1 0 541460262 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21188
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6182 0 0 0 91962 46 0 0 25 0 1 0 541460262 27975680 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6156 603 41 0 6789 0
vsize: 27320
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6187 0 0 0 92962 46 0 0 25 0 1 0 541460262 27975680 6161 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6161 603 41 0 6789 0
vsize: 27320
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6192 0 0 0 93963 46 0 0 25 0 1 0 541460262 27975680 6166 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6166 603 41 0 6789 0
vsize: 27320
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6193 0 0 0 94963 46 0 0 25 0 1 0 541460262 27975680 6167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6167 603 41 0 6789 0
vsize: 27320
[startup+960.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6193 0 0 0 95963 46 0 0 25 0 1 0 541460262 27975680 6167 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6830 6167 603 41 0 6789 0
vsize: 27320
[startup+970.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6198 0 0 0 96963 46 0 0 25 0 1 0 541460262 28110848 6172 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6863 6172 603 41 0 6822 0
vsize: 27452
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6352 0 0 0 97963 46 0 0 25 0 1 0 541460262 28655616 6326 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6996 6326 603 41 0 6955 0
vsize: 27984
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 98963 46 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 99963 46 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 100963 47 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 101963 47 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 102963 47 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 103963 47 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 104964 47 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 105964 47 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134561011 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.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 106964 47 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 107964 47 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 108964 47 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6411 0 0 0 109965 47 0 0 25 0 1 0 541460262 28925952 6385 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7062 6385 603 41 0 7021 0
vsize: 28248
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6543 0 0 0 110965 47 0 0 25 0 1 0 541460262 29458432 6517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7192 6517 603 41 0 7151 0
vsize: 28768
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6735 0 0 0 111964 48 0 0 25 0 1 0 541460262 30248960 6709 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7385 6709 603 41 0 7344 0
vsize: 29540
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 6906 0 0 0 112964 48 0 0 25 0 1 0 541460262 30916608 6880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7548 6880 603 41 0 7507 0
vsize: 30192
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 7077 0 0 0 113964 48 0 0 25 0 1 0 541460262 31686656 7051 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7736 7051 603 41 0 7695 0
vsize: 30944
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 7229 0 0 0 114964 49 0 0 25 0 1 0 541460262 32354304 7203 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7899 7203 603 41 0 7858 0
vsize: 31596
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 7366 0 0 0 115963 49 0 0 25 0 1 0 541460262 32882688 7340 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8028 7340 603 41 0 7987 0
vsize: 32112
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 7404 0 0 0 116964 49 0 0 25 0 1 0 541460262 33148928 7378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8093 7378 603 41 0 8052 0
vsize: 32372
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 7404 0 0 0 117964 49 0 0 25 0 1 0 541460262 33148928 7378 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8093 7378 603 41 0 8052 0
vsize: 32372
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 7404 0 0 0 118964 49 0 0 25 0 1 0 541460262 33148928 7378 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8093 7378 603 41 0 8052 0
vsize: 32372
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21190
Raw data (stat): 21182 (minisat+) R 21181 20838 20837 0 -1 0 7404 0 0 0 119964 49 0 0 25 0 1 0 541460262 33148928 7378 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8093 7378 603 41 0 8052 0
vsize: 32372
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.94 1/55 21190
Raw data (stat): 21182 (minisat+) Z 21181 20838 20837 0 -1 12 7407 0 0 0 119964 51 0 0 25 0 1 0 541460262 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.05
CPU time (s): 1200.16
CPU user time (s): 1199.65
CPU system time (s): 0.510922
CPU usage (%): 100.009
Max. virtual memory (Kb): 32372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####