PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-air01.opb
MD5SUM	90db1995bd949fc5ac74143a523f3bcf
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3398
Optimality of the best value was proved	NO
Number of terms in the objective function	771
Biggest coefficient in the objective function	3698
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	1192753
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	3698
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	1192753
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03384
Number of variables	771
Total number of constraints	794
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	794
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	438
Trace number 17271

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 09:52:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11619 boxname=wulflinc25 idbench=894 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-air01.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-air01.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-air01.opb
IDLAUNCH: 11619
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        572164 kB
Buffers:         20620 kB
Cached:         421940 kB
SwapCached:        732 kB
Active:          41388 kB
Inactive:       403140 kB
HighTotal:      131008 kB
HighFree:          308 kB
LowTotal:       903652 kB
LowFree:        571856 kB
SwapTotal:     2097892 kB
SwapFree:      2096248 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            12276 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 10:12:16 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 11619 7 1200.34 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 46 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################
c   -- Clauses(.)/Splits(s): (none)
c ---[  44]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[  42]---> Adder-cost: 44   maxlim: 30   bits: 5/5
c ---[  40]---> Adder-cost: 44   maxlim: 29   bits: 5/5
c ---[  38]---> Adder-cost: 48   maxlim: 28   bits: 5/5
c ---[  36]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[  34]---> Adder-cost: 54   maxlim: 35   bits: 6/6
c ---[  32]---> Adder-cost: 68   maxlim: 43   bits: 6/6
c ---[  30]---> Adder-cost: 94   maxlim: 56   bits: 6/6
c ---[  28]---> Adder-cost: 132   maxlim: 70   bits: 7/7
c ---[  26]---> Adder-cost: 194   maxlim: 99   bits: 7/7
c ---[  24]---> Adder-cost: 226   maxlim: 117   bits: 7/7
c ---[  22]---> Adder-cost: 262   maxlim: 137   bits: 8/8
c ---[  20]---> Adder-cost: 338   maxlim: 177   bits: 8/8
c ---[  18]---> Adder-cost: 320   maxlim: 166   bits: 8/8
c ---[  16]---> Adder-cost: 406   maxlim: 264   bits: 9/9
c ---[  14]---> Adder-cost: 478   maxlim: 296   bits: 9/9
c ---[  12]---> Adder-cost: 592   maxlim: 342   bits: 9/9
c ---[  10]---> Adder-cost: 482   maxlim: 280   bits: 9/9
c ---[   8]---> Adder-cost: 646   maxlim: 378   bits: 9/9
c ---[   6]---> Adder-cost: 676   maxlim: 385   bits: 9/9
c ---[   4]---> Adder-cost: 612   maxlim: 371   bits: 9/9
c ---[   2]---> Adder-cost: 574   maxlim: 391   bits: 9/9
c ---[   0]---> Adder-cost: 740   maxlim: 437   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   48745   173741 |   16248       0        0     nan |  0.000 % |
c |       100 |   48270   172076 |   17872      42      133     3.2 |  5.534 % |
c |       250 |   47474   169272 |   19660      85      297     3.5 |  7.208 % |
c |       475 |   46998   167614 |   21626     243     1082     4.5 |  8.176 % |
c |       814 |   46452   165708 |   23788     518     2867     5.5 |  9.305 % |
c |      1320 |   45678   162976 |   26167     917     5463     6.0 | 10.881 % |
c |      2081 |   44658   159340 |   28784    1531    10147     6.6 | 13.002 % |
c |      3220 |   43334   154586 |   31662    2499    17947     7.2 | 15.720 % |
c ==============================================================================
c [1mFound solution: 7133[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7920   maxlim: 1185620   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4025 |   97764   349097 |   32588    3165    24027     7.6 | 15.720 % |
c |      4125 |   97679   348810 |   35846    3254    24966     7.7 |  9.075 % |
c |      4276 |   97323   347558 |   39431    3359    26220     7.8 |  9.438 % |
c |      4503 |   96587   344914 |   43374    3488    27654     7.9 | 10.176 % |
c |      4840 |   95696   341697 |   47712    3697    29758     8.0 | 11.120 % |
c |      5346 |   94459   337368 |   52483    4009    33421     8.3 | 12.333 % |
c |      6105 |   92083   329154 |   57731    4499    39767     8.8 | 14.485 % |
c |      7244 |   90388   323269 |   63504    5400    54482    10.1 | 16.217 % |
c ==============================================================================
c [1mFound solution: 7025[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1185728   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8762 |   88126   315462 |   29375    6619    88982    13.4 | 16.217 % |
c |      8863 |   88108   315396 |   32312    6717    95974    14.3 | 18.516 % |
c ==============================================================================
c [1mFound solution: 6210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186543   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8892 |   88120   315466 |   29373    6746    97795    14.5 | 18.516 % |
c |      8992 |   88000   315038 |   32310    6827    99148    14.5 | 18.671 % |
c |      9143 |   87927   314801 |   35541    6967   106003    15.2 | 18.759 % |
c |      9369 |   87817   314393 |   39095    7182   112167    15.6 | 18.865 % |
c |      9706 |   87532   313390 |   43005    7489   127965    17.1 | 19.115 % |
c |     10214 |   87348   312738 |   47305    7963   152827    19.2 | 19.309 % |
c |     10973 |   86847   310981 |   52036    8624   232041    26.9 | 19.852 % |
c ==============================================================================
c [1mFound solution: 5429[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 5774   maxlim: 1186110   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11631 |  126861   454000 |   42287    9262   294381    31.8 | 19.852 % |
c |     11732 |  126807   453808 |   46515    9358   307300    32.8 | 14.856 % |
c |     11883 |  126799   453778 |   51167    9507   351987    37.0 | 14.861 % |
c |     12108 |  126631   453180 |   56283    9699   369115    38.1 | 14.989 % |
c ==============================================================================
c [1mFound solution: 5008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1186531   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12419 |  126441   452525 |   42147    9971   417651    41.9 | 14.989 % |
c |     12521 |  126327   452107 |   46361   10064   423209    42.1 | 15.202 % |
c |     12671 |  126194   451650 |   50997   10193   425898    41.8 | 15.284 % |
c |     12898 |  126023   451047 |   56097   10399   440782    42.4 | 15.385 % |
c |     13237 |  126005   450989 |   61707   10736   476985    44.4 | 15.404 % |
c |     13744 |  125848   450446 |   67878   11210   621322    55.4 | 15.518 % |
c ==============================================================================
c [1mFound solution: 4515[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 5438   maxlim: 1184869   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14182 |  163514   584954 |   54504   11616   680680    58.6 | 15.518 % |
c |     14283 |  163514   584954 |   59954   11717   696814    59.5 | 12.607 % |
c |     14434 |  163498   584902 |   65949   11863   711503    60.0 | 12.618 % |
c |     14659 |  162938   582974 |   72544   12032   716205    59.5 | 12.912 % |
c |     14999 |  162703   582131 |   79799   12322   751717    61.0 | 12.985 % |
c |     15506 |  162405   581041 |   87779   12783   832855    65.2 | 13.099 % |
c |     16265 |  162122   580044 |   96557   13515   997322    73.8 | 13.198 % |
c |     17404 |  162043   579773 |  106212   14639  1182939    80.8 | 13.253 % |
c ==============================================================================
c [1mFound solution: 4392[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 5228   maxlim: 1176952   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18198 |  198391   709591 |   66130   15421  1293491    83.9 | 13.253 % |
c |     18303 |  198391   709591 |   72743   15526  1312361    84.5 | 11.219 % |
c |     18453 |  198367   709509 |   80017   15672  1318194    84.1 | 11.232 % |
c |     18679 |  198228   709014 |   88019   15877  1345154    84.7 | 11.269 % |
c |     19017 |  198077   708467 |   96820   16186  1390893    85.9 | 11.305 % |
c |     19525 |  198058   708394 |  106503   16691  1545820    92.6 | 11.315 % |
c |     20284 |  197899   707819 |  117153   17402  1678790    96.5 | 11.395 % |
c |     21425 |  197320   705772 |  128868   18471  1911378   103.5 | 11.527 % |
c |     23134 |  196326   702184 |  141755   20069  2067879   103.0 | 11.727 % |
c |     25696 |  196260   701962 |  155931   22618  2770151   122.5 | 11.764 % |
c |     29544 |  194591   696020 |  171524   25495  3481300   136.5 | 12.454 % |
c |     35314 |  194115   694312 |  188676   31186  4700803   150.7 | 12.627 % |
c ==============================================================================
c [1mFound solution: 4388[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4892   maxlim: 1153615   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36710 |  228164   815886 |   76054   32580  5091661   156.3 | 12.627 % |
c |     36810 |  228155   815857 |   83659   32678  5102132   156.1 | 11.037 % |
c |     36961 |  228144   815814 |   92025   32828  5121958   156.0 | 11.042 % |
c |     37188 |  228144   815814 |  101227   33055  5151382   155.8 | 11.042 % |
c |     37526 |  228144   815814 |  111350   33393  5239659   156.9 | 11.042 % |
c |     38032 |  228117   815719 |  122485   33895  5273703   155.6 | 11.058 % |
c |     38794 |  227891   814983 |  134734   34604  5409177   156.3 | 11.173 % |
c |     39934 |  227876   814930 |  148207   35741  5627638   157.5 | 11.179 % |
c ==============================================================================
c [1mFound solution: 4289[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1153714   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40110 |  227899   815061 |   75966   35915  5661138   157.6 | 11.179 % |
c |     40212 |  227899   815061 |   83562   36017  5683219   157.8 | 11.192 % |
c |     40362 |  227679   814263 |   91918   36133  5697531   157.7 | 11.294 % |
c |     40592 |  227679   814263 |  101110   36363  5750541   158.1 | 11.294 % |
c |     40931 |  227679   814263 |  111221   36701  5777369   157.4 | 11.296 % |
c |     41437 |  227600   813992 |  122344   37193  5937931   159.7 | 11.331 % |
c |     42196 |  227461   813487 |  134578   37935  6159773   162.4 | 11.353 % |
c |     43336 |  227412   813322 |  148036   39069  6254088   160.1 | 11.371 % |
c ==============================================================================
c [1mFound solution: 3969[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4156   maxlim: 1153564   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44601 |  256237   916299 |   85412   40320  6444984   159.8 | 11.371 % |
c |     44702 |  256237   916299 |   93953   40421  6459641   159.8 | 10.318 % |
c |     44852 |  256237   916299 |  103348   40571  6546756   161.4 | 10.318 % |
c |     45077 |  256230   916276 |  113683   40794  6579072   161.3 | 10.320 % |
c |     45419 |  256214   916224 |  125051   41134  6664187   162.0 | 10.327 % |
c |     45925 |  256187   916129 |  137556   41634  6737019   161.8 | 10.339 % |
c |     46689 |  256187   916129 |  151312   42398  6885634   162.4 | 10.339 % |
c |     47835 |  256178   916098 |  166443   43543  7047662   161.9 | 10.342 % |
c |     49547 |  256178   916098 |  183088   45255  7470451   165.1 | 10.342 % |
c |     52110 |  256135   915951 |  201397   47812  7846065   164.1 | 10.361 % |
c |     55954 |  256070   915710 |  221536   51643  8319783   161.1 | 10.388 % |
c |     61720 |  255984   915402 |  243690   57387  9658150   168.3 | 10.412 % |
c |     70369 |  255984   915402 |  268059   66036 11570421   175.2 | 10.412 % |
c ==============================================================================
c [1mFound solution: 3944[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1153589   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     74545 |  255990   915460 |   85330   70212 12553851   178.8 | 10.412 % |
c |     74646 |  255990   915460 |   93863   70313 12573134   178.8 | 10.420 % |
c |     74804 |  255990   915460 |  103249   70471 12599831   178.8 | 10.420 % |
c |     75030 |  255990   915460 |  113574   70697 12648240   178.9 | 10.420 % |
c |     75367 |  255990   915460 |  124931   71034 12724862   179.1 | 10.420 % |
c |     75873 |  255990   915460 |  137424   71540 12833534   179.4 | 10.420 % |
c |     76634 |  255955   915337 |  151167   72299 12929254   178.8 | 10.430 % |
c ==============================================================================
c [1mFound solution: 3881[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1153652   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77667 |  255945   915337 |   85315   73328 13082839   178.4 | 10.430 % |
c |     77768 |  255945   915337 |   93846   73429 13090372   178.3 | 10.447 % |
c |     77919 |  255945   915337 |  103231   73580 13103515   178.1 | 10.447 % |
c |     78145 |  255945   915337 |  113554   73806 13127693   177.9 | 10.447 % |
c |     78482 |  255945   915337 |  124909   74143 13187253   177.9 | 10.447 % |
c |     78989 |  255945   915337 |  137400   74650 13254829   177.6 | 10.447 % |
c |     79748 |  255945   915337 |  151140   75409 13438930   178.2 | 10.447 % |
c |     80889 |  255945   915337 |  166254   76550 13633039   178.1 | 10.447 % |
c |     82597 |  255925   915265 |  182880   78256 13980556   178.7 | 10.457 % |
c |     85161 |  255925   915265 |  201168   80820 14701315   181.9 | 10.457 % |
c |     89005 |  255488   913714 |  221285   84598 15453400   182.7 | 10.592 % |
c |     94771 |  255469   913641 |  243413   90362 16408465   181.6 | 10.599 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -CL000001_bit0 -CL000002_bit0 -CL000003_bit0 -CL000004_bit0 -CL000005_bit0 -CL000006_bit0 -CL000007_bit0 -CL000008_bit0 -CL000009_bit0 -CL000010_bit0 -CL000011_bit0 -CL000012_bit0 -CL000013_bit0 -CL000014_bit0 -CL000015_bit0 -CL000016_bit0 -CL000017_bit0 -CL000018_bit0 -CL000019_bit0 -CL000020_bit0 -CL000021_bit0 -CL000022_bit0 -CL000023_bit0 -CL000024_bit0 -CL000025_bit0 CL000026_bit0 CL000027_bit0 -CL000028_bit0 -CL000029_bit0 -CL000030_bit0 -CL000031_bit0 -CL000032_bit0 -CL000033_bit0 -CL000034_bit0 -CL000035_bit0 -CL000036_bit0 -CL000037_bit0 -CL000038_bit0 -CL000039_bit0 -CL000040_bit0 -CL000041_bit0 -CL000042_bit0 -CL000043_bit0 -CL000044_bit0 -CL000045_bit0 -CL000046_bit0 -CL000047_bit0 -CL000048_bit0 -CL000049_bit0 -CL000050_bit0 -CL000051_bit0 -CL000052_bit0 -CL000053_bit0 -CL000054_bit0 -CL000055_bit0 -CL000056_bit0 -CL000057_bit0 -CL000058_bit0 -CL000059_bit0 -CL000060_bit0 -CL000061_bit0 -CL000062_bit0 -CL000063_bit0 -CL000064_bit0 -CL000065_bit0 -CL000066_bit0 -CL000067_bit0 -CL000068_bit0 -CL000069_bit0 -CL000070_bit0 -CL000071_bit0 -CL000072_bit0 -CL000073_bit0 -CL000074_bit0 -CL000075_bit0 -CL000076_bit0 -CL000077_bit0 -CL000078_bit0 -CL000079_bit0 -CL000080_bit0 -CL000081_bit0 -CL000082_bit0 -CL000083_bit0 -CL000084_bit0 -CL000085_bit0 -CL000086_bit0 -CL000087_bit0 -CL000088_bit0 -CL000089_bit0 -CL000090_bit0 -CL000091_bit0 -CL000092_bit0 -CL000093_bit0 -CL000094_bit0 -CL000095_bit0 -CL000096_bit0 -CL000097_bit0 -CL000098_bit0 -CL000099_bit0 -CL000100_bit0 -CL000101_bit0 -CL000102_bit0 -CL000103_bit0 -CL000104_bit0 -CL000105_bit0 -CL000106_bit0 -CL000107_bit0 -CL000108_bit0 -CL000109_bit0 -CL000110_bit0 -CL000111_bit0 -CL000112_bit0 -CL000113_bit0 -CL000114_bit0 -CL000115_bit0 -CL000116_bit0 -CL000117_bit0 -CL000118_bit0 -CL000119_bit0 -CL000120_bit0 -CL000121_bit0 -CL000122_bit0 -CL000123_bit0 -CL000124_bit0 -CL000125_bit0 -CL000126_bit0 -CL000127_bit0 -CL000128_bit0 -CL000129_bit0 -CL000130_bit0 -CL000131_bit0 -CL000132_bit0 -CL000133_bit0 -CL000134_bit0 CL000135_bit0 -CL000136_bit0 -CL000137_bit0 -CL000138_bit0 -CL000139_bit0 -CL000140_bit0 -CL000141_bit0 -CL000142_bit0 -CL000143_bit0 -CL000144_bit0 -CL000145_bit0 -CL000146_bit0 -CL000147_bit0 -CL000148_bit0 -CL000149_bit0 -CL000150_bit0 -CL000151_bit0 -CL000152_bit0 -CL000153_bit0 -CL000154_bit0 -CL000155_bit0 -CL000156_bit0 -CL000157_bit0 -CL000158_bit0 -CL000159_bit0 -CL000160_bit0 -CL000161_bit0 -CL000162_bit0 -CL000163_bit0 -CL000164_bit0 -CL000165_bit0 -CL000166_bit0 -CL000167_bit0 -CL000168_bit0 -CL000169_bit0 -CL000170_bit0 -CL000171_bit0 -CL000172_bit0 -CL000173_bit0 -CL000174_bit0 -CL000175_bit0 -CL000176_bit0 -CL000177_bit0 -CL000178_bit0 -CL000179_bit0 -CL000180_bit0 -CL000181_bit0 -CL000182_bit0 -CL000183_bit0 -CL000184_bit0 -CL000185_bit0 -CL000186_bit0 -CL000187_bit0 -CL000188_bit0 -CL000189_bit0 -CL000190_bit0 -CL000191_bit0 -CL000192_bit0 -CL000193_bit0 -CL000194_bit0 -CL000195_bit0 -CL000196_bit0 -CL000197_bit0 -CL000198_bit0 -CL000199_bit0 -CL000200_bit0 -CL000201_bit0 -CL000202_bit0 -CL000203_bit0 -CL000204_bit0 -CL000205_bit0 -CL000206_bit0 -CL000207_bit0 -CL000208_bit0 -CL000209_bit0 -CL000210_bit0 -CL000211_bit0 -CL000212_bit0 -CL000213_bit0 -CL000214_bit0 -CL000215_bit0 -CL000216_bit0 -CL000217_bit0 -CL000218_bit0 -CL000219_bit0 -CL000220_bit0 -CL000221_bit0 -CL000222_bit0 -CL000223_bit0 -CL000224_bit0 -CL000225_bit0 -CL000226_bit0 -CL000227_bit0 -CL000228_bit0 -CL000229_bit0 -CL000230_bit0 -CL000231_bit0 -CL000232_bit0 -CL000233_bit0 -CL000234_bit0 -CL000235_bit0 -CL000236_bit0 -CL000237_bit0 -CL000238_bit0 -CL000239_bit0 -CL000240_bit0 -CL000241_bit0 -CL000242_bit0 -CL000243_bit0 -CL000244_bit0 -CL000245_bit0 -CL000246_bit0 -CL000247_bit0 -CL000248_bit0 -CL000249_bit0 -CL000250_bit0 -CL000251_bit0 -CL000252_bit0 -CL000253_bit0 -CL000254_bit0 -CL000255_bit0 -CL000256_bit0 -CL000257_bit0 -CL000258_bit0 -CL000259_bit0 -CL000260_bit0 -CL000261_bit0 -CL000262_bit0 -CL000263_bit0 -CL000264_bit0 -CL000265_bit0 -CL000266_bit0 -CL000267_bit0 -CL000268_bit0 -CL000269_bit0 -CL000270_bit0 -CL000271_bit0 -CL000272_bit0 -CL000273_bit0 -CL000274_bit0 -CL000275_bit0 -CL000276_bit0 -CL000277_bit0 -CL000278_bit0 -CL000279_bit0 -CL000280_bit0 -CL000281_bit0 -CL000282_bit0 -CL000283_bit0 -CL000284_bit0 -CL000285_bit0 -CL000286_bit0 CL000287_bit0 -CL000288_bit0 -CL000289_bit0 -CL000290_bit0 -CL000291_bit0 -CL000292_bit0 -CL000293_bit0 -CL000294_bit0 -CL000295_bit0 -CL000296_bit0 -CL000297_bit0 -CL000298_bit0 -CL000299_bit0 -CL000300_bit0 -CL000301_bit0 -CL000302_bit0 -CL000303_bit0 -CL000304_bit0 -CL000305_bit0 -CL000306_bit0 -CL000307_bit0 -CL000308_bit0 -CL000309_bit0 -CL000310_bit0 -CL000311_bit0 -CL000312_bit0 -CL000313_bit0 -CL000314_bit0 -CL000315_bit0 -CL000316_bit0 -CL000317_bit0 -CL000318_bit0 -CL000319_bit0 -CL000320_bit0 -CL000321_bit0 -CL000322_bit0 -CL000323_bit0 -CL000324_bit0 -CL000325_bit0 -CL000326_bit0 -CL000327_bit0 -CL000328_bit0 -CL000329_bit0 -CL000330_bit0 -CL000331_bit0 -CL000332_bit0 -CL000333_bit0 -CL000334_bit0 -CL000335_bit0 -CL000336_bit0 -CL000337_bit0 -CL000338_bit0 -CL000339_bit0 -CL000340_bit0 -CL000341_bit0 -CL000342_bit0 -CL000343_bit0 -CL000344_bit0 -CL000345_bit0 -CL000346_bit0 -CL000347_bit0 -CL000348_bit0 -CL000349_bit0 -CL000350_bit0 -CL000351_bit0 -CL000352_bit0 -CL000353_bit0 -CL000354_bit0 -CL000355_bit0 -CL000356_bit0 -CL000357_bit0 -CL000358_bit0 CL000359_bit0 -CL000360_bit0 -CL000361_bit0 -CL000362_bit0 -CL000363_bit0 -CL000364_bit0 -CL000365_bit0 -CL000366_bit0 -CL000367_bit0 -CL000368_bit0 -CL000369_bit0 -CL000370_bit0 -CL000371_bit0 -CL000372_bit0 -CL000373_bit0 -CL000374_bit0 -CL000375_bit0 -CL000376_bit0 -CL000377_bit0 -CL000378_bit0 -CL000379_bit0 -CL000380_bit0 -CL000381_bit0 -CL000382_bit0 -CL000383_bit0 -CL000384_bit0 -CL000385_bit0 -CL000386_bit0 -CL000387_bit0 -CL000388_bit0 -CL000389_bit0 -CL000390_bit0 -CL000391_bit0 -CL000392_bit0 -CL000393_bit0 -CL000394_bit0 -CL000395_bit0 -CL000396_bit0 -CL000397_bit0 -CL000398_bit0 -CL000399_bit0 -CL000400_bit0 -CL000401_bit0 -CL000402_bit0 -CL000403_bit0 -CL000404_bit0 -CL000405_bit0 -CL000406_bit0 -CL000407_bit0 -CL000408_bit0 -CL000409_bit0 -CL000410_bit0 -CL000411_bit0 -CL000412_bit0 -CL000413_bit0 -CL000414_bit0 -CL000415_bit0 -CL000416_bit0 -CL000417_bit0 -CL000418_bit0 -CL000419_bit0 -CL000420_bit0 -CL000421_bit0 -CL000422_bit0 -CL000423_bit0 -CL000424_bit0 -CL000425_bit0 -CL000426_bit0 -CL000427_bit0 -CL000428_bit0 -CL000429_bit0 -CL000430_bit0 -CL000431_bit0 -CL000432_bit0 -CL000433_bit0 -CL000434_bit0 -CL000435_bit0 -CL000436_bit0 -CL000437_bit0 -CL000438_bit0 -CL000439_bit0 -CL000440_bit0 -CL000441_bit0 -CL000442_bit0 -CL000443_bit0 -CL000444_bit0 -CL000445_bit0 -CL000446_bit0 -CL000447_bit0 -CL000448_bit0 -CL000449_bit0 -CL000450_bit0 -CL000451_bit0 -CL000452_bit0 -CL000453_bit0 -CL000454_bit0 -CL000455_bit0 -CL000456_bit0 -CL000457_bit0 -CL000458_bit0 -CL000459_bit0 -CL000460_bit0 -CL000461_bit0 -CL000462_bit0 -CL000463_bit0 -CL000464_bit0 -CL000465_bit0 -CL000466_bit0 -CL000467_bit0 -CL000468_bit0 -CL000469_bit0 -CL000470_bit0 -CL000471_bit0 -CL000472_bit0 -CL000473_bit0 -CL000474_bit0 -CL000475_bit0 -CL000476_bit0 -CL000477_bit0 -CL000478_bit0 -CL000479_bit0 -CL000480_bit0 -CL000481_bit0 -CL000482_bit0 -CL000483_bit0 -CL000484_bit0 -CL000485_bit0 -CL000486_bit0 -CL000487_bit0 -CL000488_bit0 -CL000489_bit0 -CL000490_bit0 -CL000491_bit0 -CL000492_bit0 -CL000493_bit0 -CL000494_bit0 -CL000495_bit0 -CL000496_bit0 -CL000497_bit0 -CL000498_bit0 -CL000499_bit0 -CL000500_bit0 -CL000501_bit0 -CL000502_bit0 -CL000503_bit0 -CL000504_bit0 -CL000505_bit0 -CL000506_bit0 -CL000507_bit0 -CL000508_bit0 -CL000509_bit0 -CL000510_bit0 -CL000511_bit0 -CL000512_bit0 -CL000513_bit0 -CL000514_bit0 -CL000515_bit0 -CL000516_bit0 -CL000517_bit0 -CL000518_bit0 -CL000519_bit0 -CL000520_bit0 -CL000521_bit0 -CL000522_bit0 -CL000523_bit0 -CL000524_bit0 -CL000525_bit0 -CL000526_bit0 -CL000527_bit0 -CL000528_bit0 -CL000529_bit0 -CL000530_bit0 -CL000531_bit0 -CL000532_bit0 -CL000533_bit0 -CL000534_bit0 -CL000535_bit0 -CL000536_bit0 -CL000537_bit0 -CL000538_bit0 -CL000539_bit0 -CL000540_bit0 -CL000541_bit0 -CL000542_bit0 -CL000543_bit0 -CL000544_bi#### 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.84 0.94 0.92 2/54 647
Raw data (stat): 647 (runsolver) R 646 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544154118 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+9.99996 s]
Raw data (loadavg): 0.87 0.94 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 1209 0 0 0 995 3 0 0 25 0 1 0 544154118 6529024 1186 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1594 1186 603 41 0 1553 0
vsize: 6376
[startup+20.0001 s]
Raw data (loadavg): 0.89 0.94 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 2130 0 0 0 1993 5 0 0 25 0 1 0 544154118 10375168 2107 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2533 2107 603 41 0 2492 0
vsize: 10132
[startup+30.0005 s]
Raw data (loadavg): 0.90 0.94 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 2159 0 0 0 2992 5 0 0 25 0 1 0 544154118 10506240 2136 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2565 2136 603 41 0 2524 0
vsize: 10260
[startup+39.9997 s]
Raw data (loadavg): 0.92 0.94 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 2306 0 0 0 3991 6 0 0 25 0 1 0 544154118 11132928 2283 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2718 2283 603 41 0 2677 0
vsize: 10872
[startup+50.0006 s]
Raw data (loadavg): 0.93 0.94 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 3309 0 0 0 4989 8 0 0 25 0 1 0 544154118 15773696 3244 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3851 3244 603 41 0 3810 0
vsize: 15404
[startup+60.0004 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 3550 0 0 0 5988 9 0 0 25 0 1 0 544154118 16728064 3485 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4084 3485 603 41 0 4043 0
vsize: 16336
[startup+69.9997 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 4286 0 0 0 6986 11 0 0 25 0 1 0 544154118 19652608 4221 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4798 4221 603 41 0 4757 0
vsize: 19192
[startup+80.0007 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 4525 0 0 0 7985 12 0 0 25 0 1 0 544154118 20742144 4460 4294967295 134512640 134672761 3221224544 3221223728 134559388 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5064 4460 603 41 0 5023 0
vsize: 20256
[startup+90.0001 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 4777 0 0 0 8984 12 0 0 25 0 1 0 544154118 21655552 4712 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5287 4712 603 41 0 5246 0
vsize: 21148
[startup+100 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 5453 0 0 0 9983 14 0 0 25 0 1 0 544154118 24350720 5388 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5945 5388 603 41 0 5904 0
vsize: 23780
[startup+110 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 5766 0 0 0 10982 15 0 0 25 0 1 0 544154118 25677824 5701 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6269 5701 603 41 0 6228 0
vsize: 25076
[startup+120 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 5844 0 0 0 11982 15 0 0 25 0 1 0 544154118 25944064 5779 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6334 5779 603 41 0 6293 0
vsize: 25336
[startup+130 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 6087 0 0 0 12981 16 0 0 25 0 1 0 544154118 27021312 6022 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 6022 603 41 0 6556 0
vsize: 26388
[startup+140 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 6168 0 0 0 13981 16 0 0 25 0 1 0 544154118 27291648 6103 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6663 6103 603 41 0 6622 0
vsize: 26652
[startup+150.001 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 6447 0 0 0 14980 17 0 0 25 0 1 0 544154118 28495872 6382 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6957 6382 603 41 0 6916 0
vsize: 27828
[startup+160 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 6924 0 0 0 15979 19 0 0 25 0 1 0 544154118 30355456 6859 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7411 6859 603 41 0 7370 0
vsize: 29644
[startup+170 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 7082 0 0 0 16979 19 0 0 25 0 1 0 544154118 31031296 7017 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7576 7017 603 41 0 7535 0
vsize: 30304
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 7260 0 0 0 17978 20 0 0 25 0 1 0 544154118 31830016 7195 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7771 7195 603 41 0 7730 0
vsize: 31084
[startup+190.001 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 7431 0 0 0 18978 20 0 0 25 0 1 0 544154118 32497664 7366 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7934 7366 603 41 0 7893 0
vsize: 31736
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 7679 0 0 0 19978 21 0 0 25 0 1 0 544154118 33439744 7614 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8164 7614 603 41 0 8123 0
vsize: 32656
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 8010 0 0 0 20978 21 0 0 25 0 1 0 544154118 34893824 7945 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8519 7945 603 41 0 8478 0
vsize: 34076
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 8167 0 0 0 21978 22 0 0 25 0 1 0 544154118 35426304 8102 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8102 603 41 0 8608 0
vsize: 34596
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 8275 0 0 0 22978 22 0 0 25 0 1 0 544154118 35962880 8210 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8780 8210 603 41 0 8739 0
vsize: 35120
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 8520 0 0 0 23977 23 0 0 25 0 1 0 544154118 36888576 8455 4294967295 134512640 134672761 3221224544 3221223648 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9006 8455 603 41 0 8965 0
vsize: 36024
[startup+250.022 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 8694 0 0 0 24978 23 0 0 25 0 1 0 544154118 37556224 8629 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9169 8629 603 41 0 9128 0
vsize: 36676
[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 9112 0 0 0 25976 25 0 0 25 0 1 0 544154118 39297024 9047 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9594 9047 603 41 0 9553 0
vsize: 38376
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 9948 0 0 0 26975 27 0 0 25 0 1 0 544154118 44724224 9879 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10919 9879 603 41 0 10878 0
vsize: 43676
[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 10090 0 0 0 27974 28 0 0 25 0 1 0 544154118 45260800 10021 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11050 10021 603 41 0 11009 0
vsize: 44200
[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 10277 0 0 0 28974 28 0 0 25 0 1 0 544154118 46059520 10208 4294967295 134512640 134672761 3221224544 3221223728 134559388 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11245 10208 603 41 0 11204 0
vsize: 44980
[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 10411 0 0 0 29974 29 0 0 25 0 1 0 544154118 46587904 10342 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11374 10342 603 41 0 11333 0
vsize: 45496
[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 10596 0 0 0 30973 29 0 0 25 0 1 0 544154118 47300608 10527 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11548 10527 603 41 0 11507 0
vsize: 46192
[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 10805 0 0 0 31973 30 0 0 25 0 1 0 544154118 48234496 10736 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11776 10736 603 41 0 11735 0
vsize: 47104
[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 11037 0 0 0 32973 30 0 0 25 0 1 0 544154118 49160192 10968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12002 10968 603 41 0 11961 0
vsize: 48008
[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 11110 0 0 0 33972 31 0 0 25 0 1 0 544154118 49426432 11041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12067 11041 603 41 0 12026 0
vsize: 48268
[startup+350.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 11159 0 0 0 34972 31 0 0 25 0 1 0 544154118 49561600 11090 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12100 11090 603 41 0 12059 0
vsize: 48400
[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 11958 0 0 0 35970 34 0 0 25 0 1 0 544154118 52158464 11806 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 11806 603 41 0 12693 0
vsize: 50936
[startup+370.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 12207 0 0 0 36969 35 0 0 25 0 1 0 544154118 53133312 12055 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12972 12055 603 41 0 12931 0
vsize: 51888
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 12376 0 0 0 37969 35 0 0 25 0 1 0 544154118 53796864 12224 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13134 12224 603 41 0 13093 0
vsize: 52536
[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 12517 0 0 0 38968 36 0 0 25 0 1 0 544154118 54456320 12365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13295 12365 603 41 0 13254 0
vsize: 53180
[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 12630 0 0 0 39968 36 0 0 25 0 1 0 544154118 54857728 12478 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13393 12478 603 41 0 13352 0
vsize: 53572
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 12832 0 0 0 40968 36 0 0 25 0 1 0 544154118 55648256 12680 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13586 12680 603 41 0 13545 0
vsize: 54344
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 13027 0 0 0 41968 37 0 0 25 0 1 0 544154118 56434688 12875 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13778 12875 603 41 0 13737 0
vsize: 55112
[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 13168 0 0 0 42968 37 0 0 25 0 1 0 544154118 57090048 13016 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13938 13016 603 41 0 13897 0
vsize: 55752
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 13267 0 0 0 43968 37 0 0 25 0 1 0 544154118 57475072 13115 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14032 13115 603 41 0 13991 0
vsize: 56128
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 13385 0 0 0 44968 38 0 0 25 0 1 0 544154118 57880576 13233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14131 13233 603 41 0 14090 0
vsize: 56524
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 13491 0 0 0 45967 38 0 0 25 0 1 0 544154118 58417152 13339 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14262 13339 603 41 0 14221 0
vsize: 57048
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 647
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 13588 0 0 0 46967 38 0 0 25 0 1 0 544154118 58798080 13436 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14355 13436 603 41 0 14314 0
vsize: 57420
[startup+480.026 s]
Raw data (loadavg): 1.15 1.00 0.93 2/54 700
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 13668 0 0 0 47967 39 0 0 25 0 1 0 544154118 59056128 13516 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14418 13516 603 41 0 14377 0
vsize: 57672
[startup+490.026 s]
Raw data (loadavg): 1.13 1.00 0.93 2/54 700
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 13766 0 0 0 48966 39 0 0 25 0 1 0 544154118 59453440 13614 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14515 13614 603 41 0 14474 0
vsize: 58060
[startup+500.027 s]
Raw data (loadavg): 1.11 1.00 0.93 2/54 700
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 13906 0 0 0 49967 39 0 0 25 0 1 0 544154118 60116992 13754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14677 13754 603 41 0 14636 0
vsize: 58708
[startup+510.026 s]
Raw data (loadavg): 1.09 1.00 0.93 2/54 700
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 13950 0 0 0 50966 40 0 0 25 0 1 0 544154118 60252160 13798 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14710 13798 603 41 0 14669 0
vsize: 58840
[startup+520.026 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 700
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 14024 0 0 0 51966 40 0 0 25 0 1 0 544154118 60538880 13872 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14780 13872 603 41 0 14739 0
vsize: 59120
[startup+530.026 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 700
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 14116 0 0 0 52967 40 0 0 25 0 1 0 544154118 60940288 13964 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14878 13964 603 41 0 14837 0
vsize: 59512
[startup+540.027 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 700
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 14349 0 0 0 53966 41 0 0 25 0 1 0 544154118 61865984 14197 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15104 14197 603 41 0 15063 0
vsize: 60416
[startup+550.027 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 14376 0 0 0 54966 41 0 0 25 0 1 0 544154118 62001152 14224 4294967295 134512640 134672761 3221224544 3221223684 134560629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15137 14224 603 41 0 15096 0
vsize: 60548
[startup+560.028 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 14575 0 0 0 55965 41 0 0 25 0 1 0 544154118 62791680 14423 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15330 14423 603 41 0 15289 0
vsize: 61320
[startup+570.027 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 14812 0 0 0 56965 42 0 0 25 0 1 0 544154118 63836160 14660 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15585 14660 603 41 0 15544 0
vsize: 62340
[startup+580.027 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 15128 0 0 0 57964 43 0 0 25 0 1 0 544154118 65138688 14976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15903 14976 603 41 0 15862 0
vsize: 63612
[startup+590.027 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 15359 0 0 0 58963 44 0 0 25 0 1 0 544154118 66043904 15207 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16124 15207 603 41 0 16083 0
vsize: 64496
[startup+600.028 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 15563 0 0 0 59963 45 0 0 25 0 1 0 544154118 66949120 15411 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16345 15411 603 41 0 16304 0
vsize: 65380
[startup+610.028 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 15791 0 0 0 60962 46 0 0 25 0 1 0 544154118 67858432 15639 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16567 15639 603 41 0 16526 0
vsize: 66268
[startup+620.028 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 16031 0 0 0 61962 46 0 0 25 0 1 0 544154118 68784128 15879 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16793 15879 603 41 0 16752 0
vsize: 67172
[startup+630.029 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 16202 0 0 0 62962 47 0 0 25 0 1 0 544154118 69435392 16050 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16952 16050 603 41 0 16911 0
vsize: 67808
[startup+640.028 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 16394 0 0 0 63961 47 0 0 25 0 1 0 544154118 70316032 16242 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17167 16242 603 41 0 17126 0
vsize: 68668
[startup+650.029 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 16561 0 0 0 64960 48 0 0 25 0 1 0 544154118 70979584 16409 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17329 16409 603 41 0 17288 0
vsize: 69316
[startup+660.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 16702 0 0 0 65959 49 0 0 25 0 1 0 544154118 71487488 16550 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17453 16550 603 41 0 17412 0
vsize: 69812
[startup+670.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 16831 0 0 0 66959 49 0 0 25 0 1 0 544154118 71995392 16679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17577 16679 603 41 0 17536 0
vsize: 70308
[startup+680.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 16967 0 0 0 67960 50 0 0 25 0 1 0 544154118 72630272 16815 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17732 16815 603 41 0 17691 0
vsize: 70928
[startup+690.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 17169 0 0 0 68960 50 0 0 25 0 1 0 544154118 73416704 17017 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17924 17017 603 41 0 17883 0
vsize: 71696
[startup+700.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 17361 0 0 0 69959 50 0 0 25 0 1 0 544154118 74461184 17209 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18179 17209 603 41 0 18138 0
vsize: 72716
[startup+710.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 17544 0 0 0 70959 51 0 0 25 0 1 0 544154118 75239424 17392 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18369 17392 603 41 0 18328 0
vsize: 73476
[startup+720.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 17713 0 0 0 71958 52 0 0 25 0 1 0 544154118 75886592 17561 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18527 17561 603 41 0 18486 0
vsize: 74108
[startup+730.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 17874 0 0 0 72958 52 0 0 25 0 1 0 544154118 76546048 17722 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18688 17722 603 41 0 18647 0
vsize: 74752
[startup+740.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 18133 0 0 0 73957 53 0 0 25 0 1 0 544154118 77619200 17981 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18950 17981 603 41 0 18909 0
vsize: 75800
[startup+750.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 18331 0 0 0 74957 54 0 0 25 0 1 0 544154118 78401536 18179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19141 18179 603 41 0 19100 0
vsize: 76564
[startup+760.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 18488 0 0 0 75957 54 0 0 25 0 1 0 544154118 79032320 18336 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19295 18336 603 41 0 19254 0
vsize: 77180
[startup+770.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 18666 0 0 0 76957 54 0 0 25 0 1 0 544154118 79785984 18514 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19479 18514 603 41 0 19438 0
vsize: 77916
[startup+780.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 18796 0 0 0 77957 55 0 0 25 0 1 0 544154118 80318464 18644 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19609 18644 603 41 0 19568 0
vsize: 78436
[startup+790.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 18904 0 0 0 78957 55 0 0 25 0 1 0 544154118 80740352 18752 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19712 18752 603 41 0 19671 0
vsize: 78848
[startup+800.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 702
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 18991 0 0 0 79957 55 0 0 25 0 1 0 544154118 81137664 18839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19809 18839 603 41 0 19768 0
vsize: 79236
[startup+810.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 19060 0 0 0 80956 56 0 0 25 0 1 0 544154118 81387520 18908 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19870 18908 603 41 0 19829 0
vsize: 79480
[startup+820.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 19163 0 0 0 81956 56 0 0 25 0 1 0 544154118 81772544 19011 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19964 19011 603 41 0 19923 0
vsize: 79856
[startup+830.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 19326 0 0 0 82956 56 0 0 25 0 1 0 544154118 82423808 19174 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20123 19174 603 41 0 20082 0
vsize: 80492
[startup+840.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 19486 0 0 0 83957 56 0 0 25 0 1 0 544154118 83075072 19334 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20282 19334 603 41 0 20241 0
vsize: 81128
[startup+850.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 19613 0 0 0 84957 56 0 0 25 0 1 0 544154118 83591168 19461 4294967295 134512640 134672761 3221224544 3221223728 134559033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20408 19461 603 41 0 20367 0
vsize: 81632
[startup+860.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 19706 0 0 0 85957 57 0 0 25 0 1 0 544154118 83980288 19554 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20503 19554 603 41 0 20462 0
vsize: 82012
[startup+870.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 19812 0 0 0 86956 57 0 0 25 0 1 0 544154118 84504576 19660 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20631 19660 603 41 0 20590 0
vsize: 82524
[startup+880.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 20013 0 0 0 87956 58 0 0 25 0 1 0 544154118 85282816 19861 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20821 19861 603 41 0 20780 0
vsize: 83284
[startup+890.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 20180 0 0 0 88956 58 0 0 25 0 1 0 544154118 85938176 20028 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20981 20028 603 41 0 20940 0
vsize: 83924
[startup+900.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 20382 0 0 0 89955 59 0 0 25 0 1 0 544154118 86847488 20230 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21203 20230 603 41 0 21162 0
vsize: 84812
[startup+910.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 20582 0 0 0 90955 59 0 0 25 0 1 0 544154118 87633920 20430 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21395 20430 603 41 0 21354 0
vsize: 85580
[startup+920.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 20748 0 0 0 91955 60 0 0 25 0 1 0 544154118 88268800 20596 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21550 20596 603 41 0 21509 0
vsize: 86200
[startup+930.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 20896 0 0 0 92955 60 0 0 25 0 1 0 544154118 88924160 20744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21710 20744 603 41 0 21669 0
vsize: 86840
[startup+940.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 20959 0 0 0 93955 60 0 0 25 0 1 0 544154118 89194496 20807 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21776 20807 603 41 0 21735 0
vsize: 87104
[startup+950.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 21020 0 0 0 94955 61 0 0 25 0 1 0 544154118 89456640 20868 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21840 20868 603 41 0 21799 0
vsize: 87360
[startup+960.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 21064 0 0 0 95955 61 0 0 25 0 1 0 544154118 89591808 20912 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21873 20912 603 41 0 21832 0
vsize: 87492
[startup+970.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 21238 0 0 0 96954 61 0 0 25 0 1 0 544154118 90361856 21086 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22061 21086 603 41 0 22020 0
vsize: 88244
[startup+980.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 21481 0 0 0 97954 62 0 0 25 0 1 0 544154118 91258880 21329 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22280 21329 603 41 0 22239 0
vsize: 89120
[startup+990.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 21615 0 0 0 98953 63 0 0 25 0 1 0 544154118 91783168 21463 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22408 21463 603 41 0 22367 0
vsize: 89632
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 21683 0 0 0 99953 63 0 0 25 0 1 0 544154118 92045312 21531 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22472 21531 603 41 0 22431 0
vsize: 89888
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 21764 0 0 0 100953 63 0 0 25 0 1 0 544154118 92442624 21612 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22569 21612 603 41 0 22528 0
vsize: 90276
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 21877 0 0 0 101953 63 0 0 25 0 1 0 544154118 92958720 21725 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22695 21725 603 41 0 22654 0
vsize: 90780
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 21996 0 0 0 102953 64 0 0 25 0 1 0 544154118 93458432 21844 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22817 21844 603 41 0 22776 0
vsize: 91268
[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 22090 0 0 0 103954 64 0 0 25 0 1 0 544154118 93851648 21938 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22913 21938 603 41 0 22872 0
vsize: 91652
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 22279 0 0 0 104954 64 0 0 25 0 1 0 544154118 94654464 22127 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 22127 603 41 0 23068 0
vsize: 92436
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 22406 0 0 0 105954 64 0 0 25 0 1 0 544154118 95055872 22254 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23207 22254 603 41 0 23166 0
vsize: 92828
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 22530 0 0 0 106954 65 0 0 25 0 1 0 544154118 95576064 22378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23334 22378 603 41 0 23293 0
vsize: 93336
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 22624 0 0 0 107954 65 0 0 25 0 1 0 544154118 95969280 22472 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23430 22472 603 41 0 23389 0
vsize: 93720
[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 22774 0 0 0 108955 65 0 0 25 0 1 0 544154118 96632832 22622 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23592 22622 603 41 0 23551 0
vsize: 94368
[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 22875 0 0 0 109955 66 0 0 25 0 1 0 544154118 97034240 22723 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23690 22723 603 41 0 23649 0
vsize: 94760
[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 22917 0 0 0 110955 66 0 0 25 0 1 0 544154118 97173504 22765 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23724 22765 603 41 0 23683 0
vsize: 94896
[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 23135 0 0 0 111955 66 0 0 25 0 1 0 544154118 98103296 22983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23951 22983 603 41 0 23910 0
vsize: 95804
[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 23252 0 0 0 112955 67 0 0 25 0 1 0 544154118 98623488 23100 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24078 23100 603 41 0 24037 0
vsize: 96312
[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 23507 0 0 0 113954 67 0 0 25 0 1 0 544154118 99663872 23355 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24332 23355 603 41 0 24291 0
vsize: 97328
[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 23761 0 0 0 114954 68 0 0 25 0 1 0 544154118 100720640 23609 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24590 23609 603 41 0 24549 0
vsize: 98360
[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 23977 0 0 0 115954 69 0 0 25 0 1 0 544154118 101482496 23825 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24776 23825 603 41 0 24735 0
vsize: 99104
[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 24173 0 0 0 116954 69 0 0 25 0 1 0 544154118 102387712 24021 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24997 24021 603 41 0 24956 0
vsize: 99988
[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 24417 0 0 0 117953 70 0 0 25 0 1 0 544154118 103301120 24265 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 24265 603 41 0 25179 0
vsize: 100880
[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 24588 0 0 0 118956 70 0 0 25 0 1 0 544154118 104079360 24436 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25410 24436 603 41 0 25369 0
vsize: 101640
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 704
Raw data (stat): 647 (minisat+) R 646 28099 28098 0 -1 0 24766 0 0 0 119958 70 0 0 25 0 1 0 544154118 104734720 24614 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25570 24614 603 41 0 25529 0
vsize: 102280
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.29 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 704
Raw data (stat): 647 (minisat+) Z 646 28099 28098 0 -1 12 24769 0 0 0 119958 75 0 0 19 0 1 0 544154118 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.29
CPU time (s): 1200.34
CPU user time (s): 1199.58
CPU system time (s): 0.757884
CPU usage (%): 100.004
Max. virtual memory (Kb): 102280
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####