PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare2_1.opb
MD5SUM	375b355299c9fbf8170e172bcbc73eb2
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	16728
Optimality of the best value was proved	NO
Number of terms in the objective function	140
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	7340025
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	7340025
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.23
Number of variables	242
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	54
Number of constraints which are nor clauses,nor cardinality constraints	13
Minimum length of a constraint	1
Maximum length of a constraint	122
Trace number 14687

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        732452 kB
Buffers:         33240 kB
Cached:         245572 kB
SwapCached:         56 kB
Active:          15408 kB
Inactive:       266248 kB
HighTotal:      131008 kB
HighFree:        59472 kB
LowTotal:       903652 kB
LowFree:        672980 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14712 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:07:33 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 19500 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  12]---> Adder-cost: 590   maxlim: 469334   bits: 20/19
c ---[  10]---> Adder-cost: 648   maxlim: 507792   bits: 20/19
c ---[   8]---> Adder-cost: 604   maxlim: 482140   bits: 20/19
c ---[   6]---> Adder-cost: 572   maxlim: 518845   bits: 20/19
c ---[   4]---> Adder-cost: 688   maxlim: 476350   bits: 20/19
c ---[   2]---> Adder-cost: 646   maxlim: 516106   bits: 20/19
c ---[   0]---> Adder-cost: 598   maxlim: 472356   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   29595   105237 |    9865       0        0     nan |  0.000 % |
c |       100 |   29595   105237 |   10851     100      303     3.0 |  6.191 % |
c |       251 |   29595   105237 |   11936     251     2812    11.2 |  6.191 % |
c |       477 |   29587   105211 |   13130     476     4205     8.8 |  6.212 % |
c ==============================================================================
c [1mFound solution: 581948[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       744 |   34613   117061 |   11537     743     6316     8.5 |  6.212 % |
c ==============================================================================
c [1mFound solution: 521960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       767 |   34695   117275 |   11565     766     6815     8.9 |  6.212 % |
c ==============================================================================
c [1mFound solution: 464989[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       842 |   34758   117432 |   11586     841     8840    10.5 |  6.212 % |
c |       942 |   34758   117432 |   12744     941    10371    11.0 |  4.653 % |
c |      1092 |   34758   117432 |   14019    1091    12371    11.3 |  4.653 % |
c ==============================================================================
c [1mFound solution: 420922[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1217 |   34780   117488 |   11593    1216    24022    19.8 |  4.653 % |
c |      1317 |   34772   117462 |   12752    1315    25947    19.7 |  4.680 % |
c |      1467 |   34772   117462 |   14027    1465    26760    18.3 |  4.680 % |
c |      1692 |   34772   117462 |   15430    1690    29935    17.7 |  4.680 % |
c |      2029 |   34764   117436 |   16973    2026    32487    16.0 |  4.696 % |
c |      2535 |   34756   117410 |   18670    2531    39849    15.7 |  4.711 % |
c |      3294 |   34748   117384 |   20537    3289    53955    16.4 |  4.727 % |
c |      4434 |   34748   117384 |   22591    4429    92887    21.0 |  4.727 % |
c |      6142 |   34716   117280 |   24850    6133   139776    22.8 |  4.789 % |
c |      8705 |   34700   117228 |   27335    8694   262828    30.2 |  4.821 % |
c |     12549 |   34700   117228 |   30069   12538   465792    37.2 |  4.821 % |
c ==============================================================================
c [1mFound solution: 388291[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13845 |   34747   117346 |   11582   13834   682173    49.3 |  4.821 % |
c |     13946 |   34747   117346 |   12740    7018   428323    61.0 |  4.827 % |
c |     14098 |   34747   117346 |   14014    7170   430866    60.1 |  4.827 % |
c |     14324 |   34747   117346 |   15415    7396   435905    58.9 |  4.827 % |
c |     14662 |   34747   117346 |   16957    7734   444858    57.5 |  4.827 % |
c |     15169 |   34747   117346 |   18652    8241   468634    56.9 |  4.827 % |
c |     15928 |   34747   117346 |   20518    9000   516233    57.4 |  4.827 % |
c |     17067 |   34747   117346 |   22570   10139   552594    54.5 |  4.827 % |
c |     18775 |   34747   117346 |   24827   11847   683289    57.7 |  4.827 % |
c ==============================================================================
c [1mFound solution: 379815[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18956 |   34790   117451 |   11596   12028   704594    58.6 |  4.827 % |
c |     19058 |   34790   117451 |   12755    6116   266955    43.6 |  4.832 % |
c |     19208 |   34790   117451 |   14031    6266   269565    43.0 |  4.832 % |
c |     19433 |   34790   117451 |   15434    6491   275615    42.5 |  4.832 % |
c |     19771 |   34782   117425 |   16977    6828   284145    41.6 |  4.848 % |
c |     20277 |   34782   117425 |   18675    7334   303332    41.4 |  4.848 % |
c |     21039 |   34782   117425 |   20543    8096   350040    43.2 |  4.848 % |
c |     22178 |   34774   117399 |   22597    9234   416943    45.2 |  4.864 % |
c |     23886 |   34774   117399 |   24857   10942   453474    41.4 |  4.864 % |
c ==============================================================================
c [1mFound solution: 267843[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24556 |   34799   117462 |   11599   11612   465065    40.1 |  4.864 % |
c |     24658 |   34799   117462 |   12758   11714   470332    40.2 |  4.874 % |
c |     24808 |   34799   117462 |   14034   11864   492466    41.5 |  4.874 % |
c |     25033 |   34799   117462 |   15438   12089   500785    41.4 |  4.874 % |
c |     25370 |   34799   117462 |   16982   12426   508112    40.9 |  4.874 % |
c |     25876 |   34799   117462 |   18680   12932   521751    40.3 |  4.874 % |
c |     26636 |   34799   117462 |   20548   13692   559835    40.9 |  4.874 % |
c |     27775 |   34799   117462 |   22603   14831   594451    40.1 |  4.874 % |
c |     29483 |   34775   117384 |   24863   16536   686063    41.5 |  4.921 % |
c |     32045 |   34767   117358 |   27349   19097   775909    40.6 |  4.936 % |
c |     35890 |   34767   117358 |   30084   22942  1055364    46.0 |  4.936 % |
c |     41656 |   34767   117358 |   33093   28708  1630593    56.8 |  4.936 % |
c |     50305 |   34767   117358 |   36402   17294  1134190    65.6 |  4.936 % |
c |     63279 |   34764   117352 |   40042   30266  1884552    62.3 |  4.952 % |
c |     82741 |   34725   117265 |   44047   21067  2047866    97.2 |  5.123 % |
c |    111933 |   34719   117247 |   48451   18440  1198885    65.0 |  5.139 % |
c |    155723 |   34719   117247 |   53297   26259  3186570   121.4 |  5.139 % |
c ==============================================================================
c [1mFound solution: 263755[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    163668 |   34705   117223 |   11568   34198  4197518   122.7 |  5.139 % |
c |    163768 |   34705   117223 |   12724    6960   735654   105.7 |  5.350 % |
c |    163918 |   34705   117223 |   13997    7110   736755   103.6 |  5.350 % |
c |    164143 |   34705   117223 |   15397    7335   738856   100.7 |  5.350 % |
c |    164482 |   34705   117223 |   16936    7674   747655    97.4 |  5.350 % |
c |    164988 |   34705   117223 |   18630    8180   755048    92.3 |  5.350 % |
c |    165747 |   34705   117223 |   20493    8939   782668    87.6 |  5.350 % |
c |    166886 |   34705   117223 |   22542   10078   822693    81.6 |  5.350 % |
c ==============================================================================
c [1mFound solution: 237163[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    168065 |   34734   117296 |   11578   11257   860769    76.5 |  5.350 % |
c |    168166 |   34734   117296 |   12735   11358   861788    75.9 |  5.359 % |
c |    168317 |   34725   117269 |   14009   11504   862946    75.0 |  5.390 % |
c |    168542 |   34725   117269 |   15410   11729   867453    74.0 |  5.390 % |
c |    168880 |   34725   117269 |   16951   12067   874828    72.5 |  5.390 % |
c |    169387 |   34719   117254 |   18646   12573   886685    70.5 |  5.405 % |
c |    170146 |   34719   117254 |   20511   13332   914255    68.6 |  5.405 % |
c |    171285 |   34719   117254 |   22562   14471   952693    65.8 |  5.405 % |
c |    172993 |   34719   117254 |   24818   16179  1033191    63.9 |  5.405 % |
c |    175557 |   34719   117254 |   27300   18743  1147893    61.2 |  5.405 % |
c |    179401 |   34647   117091 |   30030   22578  1359693    60.2 |  5.685 % |
c |    185169 |   34647   117091 |   33033   28346  1884599    66.5 |  5.685 % |
c |    193819 |   34641   117077 |   36336   16856   931253    55.2 |  5.716 % |
c |    206794 |   34641   117077 |   39970   29831  1930145    64.7 |  5.716 % |
c ==============================================================================
c [1mFound solution: 219040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    217027 |   34681   117173 |   11560   40064  2394179    59.8 |  5.716 % |
c |    217127 |   34681   117173 |   12716    7194   284520    39.5 |  5.720 % |
c |    217277 |   34681   117173 |   13987    7344   295403    40.2 |  5.720 % |
c |    217502 |   34681   117173 |   15386    7569   296768    39.2 |  5.720 % |
c |    217839 |   34681   117173 |   16924    7906   299896    37.9 |  5.720 % |
c |    218346 |   34642   117084 |   18617    8412   307445    36.5 |  5.875 % |
c |    219105 |   34642   117084 |   20479    9171   328935    35.9 |  5.875 % |
c |    220245 |   34642   117084 |   22527   10311   361407    35.1 |  5.875 % |
c |    221954 |   34642   117084 |   24779   12020   458223    38.1 |  5.875 % |
c |    224516 |   34642   117084 |   27257   14582   562913    38.6 |  5.875 % |
c |    228360 |   34642   117084 |   29983   18426   697285    37.8 |  5.875 % |
c |    234126 |   34642   117084 |   32982   24192  1168086    48.3 |  5.875 % |
c ==============================================================================
c [1mFound solution: 193370[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    234732 |   34666   117144 |   11555   24798  1235668    49.8 |  5.875 % |
c |    234832 |   34666   117144 |   12710    6300   396822    63.0 |  5.884 % |
c |    234982 |   34666   117144 |   13981    6450   400608    62.1 |  5.884 % |
c |    235207 |   34666   117144 |   15379    6675   405634    60.8 |  5.884 % |
c |    235545 |   34666   117144 |   16917    7013   414646    59.1 |  5.884 % |
c |    236051 |   34666   117144 |   18609    7519   429737    57.2 |  5.884 % |
c |    236811 |   34666   117144 |   20470    8279   475792    57.5 |  5.884 % |
c |    237950 |   34666   117144 |   22517    9418   512119    54.4 |  5.884 % |
c |    239658 |   34666   117144 |   24769   11126   572954    51.5 |  5.884 % |
c |    242222 |   34666   117144 |   27246   13690   714923    52.2 |  5.884 % |
c |    246068 |   34666   117144 |   29970   17536   866864    49.4 |  5.884 % |
c |    251834 |   34533   116832 |   32967   23295  1177893    50.6 |  6.550 % |
c |    260483 |   34527   116814 |   36264   31943  1542049    48.3 |  6.566 % |
c |    273458 |   34527   116814 |   39890   20829   969990    46.6 |  6.566 % |
c ==============================================================================
c [1mFound solution: 140672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    277117 |   34540   116848 |   11513   24485  1187066    48.5 |  6.566 % |
c |    277217 |   34540   116848 |   12664    6222   233642    37.6 |  6.650 % |
c |    277367 |   34540   116848 |   13930    6372   236099    37.1 |  6.650 % |
c |    277592 |   34540   116848 |   15323    6597   242041    36.7 |  6.650 % |
c |    277929 |   34540   116848 |   16856    6934   250522    36.1 |  6.650 % |
c |    278435 |   34540   116848 |   18541    7440   274598    36.9 |  6.650 % |
c |    279194 |   34540   116848 |   20395    8199   297940    36.3 |  6.650 % |
c |    280333 |   34540   116848 |   22435    9338   326942    35.0 |  6.650 % |
c |    282041 |   34540   116848 |   24679   11046   390600    35.4 |  6.650 % |
c |    284604 |   34540   116848 |   27147   13609   489494    36.0 |  6.650 % |
c |    288448 |   34540   116848 |   29861   17453   660389    37.8 |  6.650 % |
c |    294214 |   34540   116848 |   32847   23219   988329    42.6 |  6.650 % |
c |    302863 |   34540   116848 |   36132   31868  1387973    43.6 |  6.650 % |
c |    315837 |   34540   116848 |   39745   21708   950298    43.8 |  6.650 % |
c |    335298 |   34540   116848 |   43720   41169  2260131    54.9 |  6.650 % |
c |    364491 |   34540   116848 |   48092   41852  2593870    62.0 |  6.650 % |
c |    408281 |   34540   116848 |   52901   16594  1005025    60.6 |  6.650 % |
c |    473965 |   34531   116821 |   58192   43989  2982186    67.8 |  6.681 % |
c ==============================================================================
c [1mFound solution: 129661[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    475555 |   34485   116655 |   11495   45526  3028902    66.5 |  6.681 % |
c |    475657 |   34485   116655 |   12644    6861   241515    35.2 |  6.920 % |
c |    475807 |   34485   116655 |   13908    7011   242435    34.6 |  6.920 % |
c |    476032 |   34485   116655 |   15299    7236   246074    34.0 |  6.920 % |
c |    476369 |   34485   116655 |   16829    7573   257376    34.0 |  6.920 % |
c |    476875 |   34485   116655 |   18512    8079   272096    33.7 |  6.920 % |
c |    477636 |   34485   116655 |   20364    8840   305531    34.6 |  6.920 % |
c |    478776 |   34485   116655 |   22400    9980   347625    34.8 |  6.920 % |
c |    480484 |   34485   116655 |   24640   11688   409867    35.1 |  6.920 % |
c |    483046 |   34478   116638 |   27104   14247   480889    33.8 |  6.966 % |
c |    486890 |   34478   116638 |   29815   18091   694983    38.4 |  6.966 % |
c |    492656 |   34478   116638 |   32796   23857   970371    40.7 |  6.966 % |
c |    501305 |   34310   116247 |   36076   32490  1365728    42.0 |  7.785 % |
c |    514279 |   34259   116122 |   39683   21758  1113677    51.2 |  8.017 % |
c |    533740 |   34259   116122 |   43652   41219  3039395    73.7 |  8.017 % |
c |    562932 |   34246   116092 |   48017   41063  2694313    65.6 |  8.078 % |
c ==============================================================================
c [1mFound solution: 127863[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    581394 |   34271   116155 |   11423   24436  1418001    58.0 |  8.078 % |
c |    581494 |   34271   116155 |   12565    6209   231122    37.2 |  8.085 % |
c |    581644 |   34271   116155 |   13821    6359   232017    36.5 |  8.085 % |
c |    581869 |   34271   116155 |   15204    6584   233845    35.5 |  8.085 % |
c |    582208 |   34271   116155 |   16724    6923   237644    34.3 |  8.085 % |
c |    582715 |   34271   116155 |   18396    7430   256188    34.5 |  8.085 % |
c |    583477 |   34271   116155 |   20236    8192   271668    33.2 |  8.085 % |
c |    584616 |   34271   116155 |   22260    9331   304468    32.6 |  8.085 % |
c |    586326 |   34271   116155 |   24486   11041   411467    37.3 |  8.085 % |
c |    588888 |   34271   116155 |   26934   13603   486061    35.7 |  8.085 % |
c |    592732 |   34271   116155 |   29628   17447   742684    42.6 |  8.085 % |
c ==============================================================================
c [1mFound solution: 123046[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    596006 |   34301   116229 |   11433   20721   938289    45.3 |  8.085 % |
c |    596106 |   34301   116229 |   12576   10461   495812    47.4 |  8.089 % |
c |    596256 |   34301   116229 |   13833   10611   498487    47.0 |  8.089 % |
c |    596482 |   34301   116229 |   15217   10837   504034    46.5 |  8.089 % |
c |    596819 |   34284   116191 |   16739   11171   509953    45.6 |  8.151 % |
c |    597325 |   34284   116191 |   18412   11677   519541    44.5 |  8.151 % |
c |    598085 |   34284   116191 |   20254   12437   537456    43.2 |  8.151 % |
c |    599227 |   34284   116191 |   22279   13579   575072    42.4 |  8.151 % |
c |    600936 |   34284   116191 |   24507   15288   706730    46.2 |  8.151 % |
c |    603498 |   34284   116191 |   26958   17850   814207    45.6 |  8.151 % |
c |    607342 |   34284   116191 |   29654   21694   995827    45.9 |  8.151 % |
c |    613109 |   34284   116191 |   32619   27461  1280295    46.6 |  8.151 % |
c |    621758 |   34284   116191 |   35881   16481   712113    43.2 |  8.151 % |
c |    634734 |   34284   116191 |   39469   29457  1381815    46.9 |  8.151 % |
c |    654196 |   34284   116191 |   43416   21233  1150103    54.2 |  8.151 % |
c |    683389 |   34276   116174 |   47758   19988   975317    48.8 |  8.182 % |
c |    727179 |   34276   116174 |   52534   28686  1703177    59.4 |  8.182 % |
c ==============================================================================
c [1mFound solution: 113122[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    735661 |   34303   116241 |   11434   37168  2380407    64.0 |  8.182 % |
c |    735762 |   34303   116241 |   12577    7252   463690    63.9 |  8.187 % |
c |    735913 |   34303   116241 |   13835    7403   466619    63.0 |  8.187 % |
c |    736138 |   34303   116241 |   15218    7628   470458    61.7 |  8.187 % |
c |    736477 |   34303   116241 |   16740    7967   480090    60.3 |  8.187 % |
c |    736983 |   34303   116241 |   18414    8473   500472    59.1 |  8.187 % |
c |    737743 |   34303   116241 |   20256    9233   515762    55.9 |  8.187 % |
c |    738882 |   34303   116241 |   22281   10372   558609    53.9 |  8.187 % |
c |    740590 |   34303   116241 |   24509   12080   611611    50.6 |  8.187 % |
c |    743153 |   34303   116241 |   26960   14643   707669    48.3 |  8.187 % |
c |    746998 |   34303   116241 |   29656   18488   893205    48.3 |  8.187 % |
c |    752764 |   34303   116241 |   32622   24254  1204092    49.6 |  8.187 % |
c |    761414 |   34296   116226 |   35884   32903  1639375    49.8 |  8.218 % |
c |    774389 |   34296   116226 |   39473   21731  1224753    56.4 |  8.218 % |
c |    793850 |   34296   116226 |   43420   41192  3038860    73.8 |  8.218 % |
c |    823042 |   34296   116226 |   47762   39879  2500196    62.7 |  8.218 % |
#### 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.89 0.93 0.90 1/54 29938
Raw data (stat): 29938 (runsolver) R 29937 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482649150 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 1782 0 0 0 995 4 0 0 25 0 1 0 482649150 8982528 1755 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2193 1755 603 41 0 2152 0
vsize: 8772
[startup+20.0015 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 1926 0 0 0 1994 5 0 0 25 0 1 0 482649150 9519104 1899 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2324 1899 603 41 0 2283 0
vsize: 9296
[startup+30.0029 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 2383 0 0 0 2993 6 0 0 25 0 1 0 482649150 11493376 2356 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2806 2356 603 41 0 2765 0
vsize: 11224
[startup+40.0032 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 3032 0 0 0 3991 8 0 0 25 0 1 0 482649150 14045184 3005 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3429 3005 603 41 0 3388 0
vsize: 13716
[startup+50.0041 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 3406 0 0 0 4990 9 0 0 25 0 1 0 482649150 15785984 3379 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3854 3379 603 41 0 3813 0
vsize: 15416
[startup+60.0045 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 3406 0 0 0 5990 10 0 0 25 0 1 0 482649150 15785984 3379 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3854 3379 603 41 0 3813 0
vsize: 15416
[startup+70.0058 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 3960 0 0 0 6988 12 0 0 25 0 1 0 482649150 18071552 3933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4412 3933 603 41 0 4371 0
vsize: 17648
[startup+80.0077 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 4576 0 0 0 7986 14 0 0 25 0 1 0 482649150 20496384 4549 4294967295 134512640 134672761 3221224544 3221223636 1075351196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5004 4549 603 41 0 4963 0
vsize: 20016
[startup+90.0081 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 4706 0 0 0 8986 14 0 0 25 0 1 0 482649150 21037056 4679 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5136 4679 603 41 0 5095 0
vsize: 20544
[startup+100.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 4706 0 0 0 9985 14 0 0 25 0 1 0 482649150 21037056 4679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5136 4679 603 41 0 5095 0
vsize: 20544
[startup+110.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 4706 0 0 0 10986 14 0 0 25 0 1 0 482649150 21037056 4679 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5136 4679 603 41 0 5095 0
vsize: 20544
[startup+120.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 5051 0 0 0 11984 16 0 0 25 0 1 0 482649150 22499328 5024 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5493 5024 603 41 0 5452 0
vsize: 21972
[startup+130.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 5371 0 0 0 12984 17 0 0 25 0 1 0 482649150 23715840 5344 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5344 603 41 0 5749 0
vsize: 23160
[startup+140.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 5371 0 0 0 13983 17 0 0 25 0 1 0 482649150 23715840 5344 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5344 603 41 0 5749 0
vsize: 23160
[startup+150.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 5371 0 0 0 14983 17 0 0 25 0 1 0 482649150 23715840 5344 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5344 603 41 0 5749 0
vsize: 23160
[startup+160.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 5371 0 0 0 15983 18 0 0 25 0 1 0 482649150 23715840 5344 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5790 5344 603 41 0 5749 0
vsize: 23160
[startup+170.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 5371 0 0 0 16983 18 0 0 25 0 1 0 482649150 23715840 5344 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5790 5344 603 41 0 5749 0
vsize: 23160
[startup+180.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 5422 0 0 0 17983 18 0 0 25 0 1 0 482649150 23982080 5395 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5855 5395 603 41 0 5814 0
vsize: 23420
[startup+190.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 5855 0 0 0 18981 20 0 0 25 0 1 0 482649150 25706496 5828 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6276 5829 603 41 0 6235 0
vsize: 25104
[startup+200.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 6283 0 0 0 19980 21 0 0 25 0 1 0 482649150 27443200 6256 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6700 6256 603 41 0 6659 0
vsize: 26800
[startup+210.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 6683 0 0 0 20979 22 0 0 25 0 1 0 482649150 29167616 6656 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7121 6656 603 41 0 7080 0
vsize: 28484
[startup+220.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7163 0 0 0 21978 24 0 0 25 0 1 0 482649150 31035392 7136 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7577 7136 603 41 0 7536 0
vsize: 30308
[startup+230.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 22977 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+240.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 23977 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+250.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 24978 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+260.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 25978 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+270.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 26978 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+280.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 27978 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 28978 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 29978 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 30978 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 31978 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 32978 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 33979 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 34978 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 35979 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 36979 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223728 134558916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 37979 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 38979 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 39980 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 40981 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 41981 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+430.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 42981 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+440.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 43981 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 44981 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+460.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 45981 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+470.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 46982 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 47982 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+490.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 48982 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 49982 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+510.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 50982 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 51982 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+530.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 52983 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 53983 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+550.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 54983 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+560.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 55983 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+570.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 56983 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+580.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 57984 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+590.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 58984 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+600.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 59984 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+610.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 60984 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+620.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 61984 25 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+630.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7431 0 0 0 62984 26 0 0 25 0 1 0 482649150 32239616 7404 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7404 603 41 0 7830 0
vsize: 31484
[startup+640.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7433 0 0 0 63984 26 0 0 25 0 1 0 482649150 32239616 7406 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7406 603 41 0 7830 0
vsize: 31484
[startup+650.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 64985 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+660.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 65985 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+670.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 66985 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+680.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 67985 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+690.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 68985 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+700.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 69985 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+710.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 70986 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+720.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 71985 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 72986 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+740.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 73986 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+750.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29938
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 74986 26 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+760.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29991
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 75976 35 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+770.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29991
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 76976 35 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+780.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29991
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 77975 35 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+790.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29991
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 78975 36 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+800.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29991
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 79975 36 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+810.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29991
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 80975 37 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+820.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29991
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 81975 37 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+830.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7434 0 0 0 82975 37 0 0 25 0 1 0 482649150 32239616 7407 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7407 603 41 0 7830 0
vsize: 31484
[startup+840.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 83974 38 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+850.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 84974 38 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+860.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 85974 38 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+870.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 86974 38 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 87974 39 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+890.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 88974 39 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+900.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 89974 39 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+910.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 90973 40 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+920.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 91973 40 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+930.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 92973 40 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223728 134559660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+940.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 93973 41 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+950.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 94973 41 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+960.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 95973 41 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+970.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 96973 42 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+980.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 97973 42 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+990.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 98973 42 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 99975 42 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 100973 43 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 101973 43 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 102973 43 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 103972 44 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 104972 44 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 105972 44 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 106972 44 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 107972 45 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 108972 45 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 109972 45 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 110972 46 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 111972 46 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29993
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 112972 46 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29995
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 113971 47 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29995
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 114970 47 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29995
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 115970 48 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29995
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 116970 48 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29995
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 117970 48 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29995
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 118970 48 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29995
Raw data (stat): 29938 (minisat+) R 29937 5897 5896 0 -1 0 7435 0 0 0 119970 49 0 0 25 0 1 0 482649150 32239616 7408 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7871 7408 603 41 0 7830 0
vsize: 31484
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29995
Raw data (stat): 29938 (minisat+) Z 29937 5897 5896 0 -1 12 7438 0 0 0 119970 50 0 0 25 0 1 0 482649150 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.1
CPU time (s): 1200.21
CPU user time (s): 1199.7
CPU system time (s): 0.505923
CPU usage (%): 100.009
Max. virtual memory (Kb): 31484
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####