PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.02884
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 19449

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 19:03:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16611 boxname=wulflinc7 idbench=1278 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-air01.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-air01.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-air01.opb
IDLAUNCH: 16611
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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.050
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:        740204 kB
Buffers:         20604 kB
Cached:         252452 kB
SwapCached:        304 kB
Active:          32944 kB
Inactive:       242704 kB
HighTotal:      131008 kB
HighFree:        50344 kB
LowTotal:       903652 kB
LowFree:        689860 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6448 kB
Slab:            13248 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 19:23:34 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 16611 7 1200.22 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.92 0.97 0.91 2/54 13316
Raw data (stat): 13316 (runsolver) R 13315 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489235554 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 1201 0 0 0 995 3 0 0 25 0 1 0 489235554 6529024 1178 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1594 1178 603 41 0 1553 0
vsize: 6376
[startup+20.001 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 2130 0 0 0 1993 6 0 0 25 0 1 0 489235554 10375168 2107 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.0016 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 2158 0 0 0 2993 6 0 0 25 0 1 0 489235554 10506240 2135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2565 2135 603 41 0 2524 0
vsize: 10260
[startup+40.0017 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 2290 0 0 0 3992 7 0 0 25 0 1 0 489235554 10993664 2267 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2684 2267 603 41 0 2643 0
vsize: 10736
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 3275 0 0 0 4989 10 0 0 25 0 1 0 489235554 15564800 3210 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3800 3210 603 41 0 3759 0
vsize: 15200
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 3534 0 0 0 5988 11 0 0 25 0 1 0 489235554 16592896 3469 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4051 3469 603 41 0 4010 0
vsize: 16204
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 4274 0 0 0 6986 13 0 0 25 0 1 0 489235554 19652608 4209 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4798 4209 603 41 0 4757 0
vsize: 19192
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 4515 0 0 0 7985 14 0 0 25 0 1 0 489235554 20606976 4450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5031 4450 603 41 0 4990 0
vsize: 20124
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 4775 0 0 0 8984 16 0 0 25 0 1 0 489235554 21655552 4710 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5287 4710 603 41 0 5246 0
vsize: 21148
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 5450 0 0 0 9981 18 0 0 25 0 1 0 489235554 24350720 5385 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5945 5385 603 41 0 5904 0
vsize: 23780
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 5731 0 0 0 10980 20 0 0 25 0 1 0 489235554 25538560 5666 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6235 5666 603 41 0 6194 0
vsize: 24940
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 5827 0 0 0 11979 21 0 0 25 0 1 0 489235554 25944064 5762 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6334 5762 603 41 0 6293 0
vsize: 25336
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 6078 0 0 0 12978 21 0 0 25 0 1 0 489235554 26886144 6013 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6564 6013 603 41 0 6523 0
vsize: 26256
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 6141 0 0 0 13978 22 0 0 25 0 1 0 489235554 27156480 6076 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6630 6076 603 41 0 6589 0
vsize: 26520
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 6428 0 0 0 14977 23 0 0 25 0 1 0 489235554 28360704 6363 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6924 6363 603 41 0 6883 0
vsize: 27696
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13316
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 6851 0 0 0 15975 25 0 0 25 0 1 0 489235554 30097408 6786 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7348 6786 603 41 0 7307 0
vsize: 29392
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 7012 0 0 0 16974 26 0 0 25 0 1 0 489235554 30756864 6947 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7509 6947 603 41 0 7468 0
vsize: 30036
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 7212 0 0 0 17974 27 0 0 25 0 1 0 489235554 31563776 7147 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7706 7147 603 41 0 7665 0
vsize: 30824
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 7371 0 0 0 18973 27 0 0 25 0 1 0 489235554 32231424 7306 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7869 7306 603 41 0 7828 0
vsize: 31476
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 7679 0 0 0 19972 28 0 0 25 0 1 0 489235554 33439744 7614 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8164 7614 603 41 0 8123 0
vsize: 32656
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 7914 0 0 0 20971 30 0 0 25 0 1 0 489235554 34488320 7849 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8420 7849 603 41 0 8379 0
vsize: 33680
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 8142 0 0 0 21971 30 0 0 25 0 1 0 489235554 35426304 8077 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8649 8077 603 41 0 8608 0
vsize: 34596
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 8254 0 0 0 22970 31 0 0 25 0 1 0 489235554 35827712 8189 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8747 8189 603 41 0 8706 0
vsize: 34988
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 8428 0 0 0 23970 31 0 0 25 0 1 0 489235554 36487168 8363 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8908 8363 603 41 0 8867 0
vsize: 35632
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 8634 0 0 0 24969 32 0 0 25 0 1 0 489235554 37421056 8569 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9136 8569 603 41 0 9095 0
vsize: 36544
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 9019 0 0 0 25968 33 0 0 25 0 1 0 489235554 38899712 8954 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9497 8954 603 41 0 9456 0
vsize: 37988
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 9913 0 0 0 26965 36 0 0 25 0 1 0 489235554 44462080 9844 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10855 9844 603 41 0 10814 0
vsize: 43420
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 10079 0 0 0 27965 37 0 0 25 0 1 0 489235554 45260800 10010 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11050 10010 603 41 0 11009 0
vsize: 44200
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 10234 0 0 0 28964 38 0 0 25 0 1 0 489235554 45928448 10165 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11213 10165 603 41 0 11172 0
vsize: 44852
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 10384 0 0 0 29964 38 0 0 25 0 1 0 489235554 46452736 10315 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11341 10315 603 41 0 11300 0
vsize: 45364
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 10545 0 0 0 30963 38 0 0 25 0 1 0 489235554 47165440 10476 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11515 10476 603 41 0 11474 0
vsize: 46060
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 10679 0 0 0 31963 39 0 0 25 0 1 0 489235554 47706112 10610 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11647 10610 603 41 0 11606 0
vsize: 46588
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 10978 0 0 0 32961 40 0 0 25 0 1 0 489235554 48902144 10909 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11939 10909 603 41 0 11898 0
vsize: 47756
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 11100 0 0 0 33961 41 0 0 25 0 1 0 489235554 49426432 11031 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12067 11031 603 41 0 12026 0
vsize: 48268
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 11155 0 0 0 34960 42 0 0 25 0 1 0 489235554 49561600 11086 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12100 11086 603 41 0 12059 0
vsize: 48400
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 11276 0 0 0 35961 42 0 0 25 0 1 0 489235554 50102272 11207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12232 11207 603 41 0 12191 0
vsize: 48928
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 12120 0 0 0 36958 45 0 0 25 0 1 0 489235554 52858880 11968 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12905 11968 603 41 0 12864 0
vsize: 51620
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 12306 0 0 0 37957 46 0 0 25 0 1 0 489235554 53534720 12154 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13070 12154 603 41 0 13029 0
vsize: 52280
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 12478 0 0 0 38956 47 0 0 25 0 1 0 489235554 54185984 12326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13229 12326 603 41 0 13188 0
vsize: 52916
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 12596 0 0 0 39955 48 0 0 25 0 1 0 489235554 54726656 12444 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13361 12444 603 41 0 13320 0
vsize: 53444
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 12707 0 0 0 40955 48 0 0 25 0 1 0 489235554 55123968 12555 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13458 12555 603 41 0 13417 0
vsize: 53832
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 12965 0 0 0 41954 50 0 0 25 0 1 0 489235554 56299520 12813 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13745 12813 603 41 0 13704 0
vsize: 54980
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 13123 0 0 0 42953 50 0 0 25 0 1 0 489235554 56827904 12971 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13874 12971 603 41 0 13833 0
vsize: 55496
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 13230 0 0 0 43953 51 0 0 25 0 1 0 489235554 57344000 13078 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13078 603 41 0 13959 0
vsize: 56000
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 13340 0 0 0 44953 51 0 0 25 0 1 0 489235554 57745408 13188 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14098 13188 603 41 0 14057 0
vsize: 56392
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 13453 0 0 0 45952 52 0 0 25 0 1 0 489235554 58286080 13301 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13301 603 41 0 14189 0
vsize: 56920
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 13538 0 0 0 46952 52 0 0 25 0 1 0 489235554 58548224 13386 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14294 13386 603 41 0 14253 0
vsize: 57176
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 13648 0 0 0 47951 53 0 0 25 0 1 0 489235554 59056128 13496 4294967295 134512640 134672761 3221224544 3221223728 134559038 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14418 13496 603 41 0 14377 0
vsize: 57672
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 13722 0 0 0 48950 54 0 0 25 0 1 0 489235554 59322368 13570 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14483 13570 603 41 0 14442 0
vsize: 57932
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 13851 0 0 0 49950 54 0 0 25 0 1 0 489235554 59850752 13699 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14612 13699 603 41 0 14571 0
vsize: 58448
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 13928 0 0 0 50950 54 0 0 25 0 1 0 489235554 60116992 13776 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14677 13776 603 41 0 14636 0
vsize: 58708
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 13983 0 0 0 51950 54 0 0 25 0 1 0 489235554 60387328 13831 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14743 13831 603 41 0 14702 0
vsize: 58972
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 14074 0 0 0 52950 55 0 0 25 0 1 0 489235554 60805120 13922 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14845 13922 603 41 0 14804 0
vsize: 59380
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 14266 0 0 0 53949 56 0 0 25 0 1 0 489235554 61599744 14114 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15039 14114 603 41 0 14998 0
vsize: 60156
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 14364 0 0 0 54948 57 0 0 25 0 1 0 489235554 62001152 14212 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15137 14212 603 41 0 15096 0
vsize: 60548
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 14421 0 0 0 55948 57 0 0 25 0 1 0 489235554 62259200 14269 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15200 14269 603 41 0 15159 0
vsize: 60800
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 14724 0 0 0 56948 57 0 0 25 0 1 0 489235554 63455232 14572 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15492 14572 603 41 0 15451 0
vsize: 61968
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 14961 0 0 0 57947 58 0 0 25 0 1 0 489235554 64368640 14809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15715 14809 603 41 0 15674 0
vsize: 62860
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 15256 0 0 0 58946 60 0 0 25 0 1 0 489235554 65662976 15104 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16031 15104 603 41 0 15990 0
vsize: 64124
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 15458 0 0 0 59946 60 0 0 25 0 1 0 489235554 66428928 15306 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16218 15306 603 41 0 16177 0
vsize: 64872
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 15655 0 0 0 60945 61 0 0 25 0 1 0 489235554 67203072 15503 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16407 15503 603 41 0 16366 0
vsize: 65628
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 15907 0 0 0 61944 62 0 0 25 0 1 0 489235554 68255744 15755 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16664 15755 603 41 0 16623 0
vsize: 66656
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 16121 0 0 0 62943 63 0 0 25 0 1 0 489235554 69169152 15969 4294967295 134512640 134672761 3221224544 3221223680 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16887 15969 603 41 0 16846 0
vsize: 67548
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 16290 0 0 0 63943 64 0 0 25 0 1 0 489235554 69799936 16138 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17041 16138 603 41 0 17000 0
vsize: 68164
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 16460 0 0 0 64942 65 0 0 25 0 1 0 489235554 70582272 16308 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17232 16308 603 41 0 17191 0
vsize: 68928
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 16632 0 0 0 65941 66 0 0 25 0 1 0 489235554 71229440 16480 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17390 16480 603 41 0 17349 0
vsize: 69560
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 16755 0 0 0 66941 66 0 0 25 0 1 0 489235554 71745536 16603 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17516 16603 603 41 0 17475 0
vsize: 70064
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 16887 0 0 0 67941 67 0 0 25 0 1 0 489235554 72245248 16735 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16735 603 41 0 17597 0
vsize: 70552
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 17046 0 0 0 68940 67 0 0 25 0 1 0 489235554 72896512 16894 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17797 16894 603 41 0 17756 0
vsize: 71188
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 17246 0 0 0 69940 68 0 0 25 0 1 0 489235554 73805824 17094 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18019 17094 603 41 0 17978 0
vsize: 72076
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 17422 0 0 0 70939 68 0 0 25 0 1 0 489235554 74719232 17270 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18242 17270 603 41 0 18201 0
vsize: 72968
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 17619 0 0 0 71939 69 0 0 25 0 1 0 489235554 75493376 17467 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18431 17467 603 41 0 18390 0
vsize: 73724
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 17745 0 0 0 72939 70 0 0 25 0 1 0 489235554 76017664 17593 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18559 17593 603 41 0 18518 0
vsize: 74236
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 17962 0 0 0 73938 70 0 0 25 0 1 0 489235554 76947456 17810 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18786 17810 603 41 0 18745 0
vsize: 75144
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 18202 0 0 0 74938 71 0 0 25 0 1 0 489235554 77881344 18050 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19014 18050 603 41 0 18973 0
vsize: 76056
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 18410 0 0 0 75937 71 0 0 25 0 1 0 489235554 78790656 18258 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19236 18258 603 41 0 19195 0
vsize: 76944
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 18535 0 0 0 76937 72 0 0 25 0 1 0 489235554 79269888 18383 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19353 18383 603 41 0 19312 0
vsize: 77412
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 18706 0 0 0 77936 73 0 0 25 0 1 0 489235554 79917056 18554 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19511 18554 603 41 0 19470 0
vsize: 78044
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 18805 0 0 0 78936 73 0 0 25 0 1 0 489235554 80318464 18653 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19609 18653 603 41 0 19568 0
vsize: 78436
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 18931 0 0 0 79936 73 0 0 25 0 1 0 489235554 80871424 18779 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19744 18779 603 41 0 19703 0
vsize: 78976
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 19008 0 0 0 80936 73 0 0 25 0 1 0 489235554 81137664 18856 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19809 18856 603 41 0 19768 0
vsize: 79236
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 19065 0 0 0 81936 74 0 0 25 0 1 0 489235554 81387520 18913 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19870 18913 603 41 0 19829 0
vsize: 79480
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 19186 0 0 0 82936 74 0 0 25 0 1 0 489235554 81907712 19034 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19997 19034 603 41 0 19956 0
vsize: 79988
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 19367 0 0 0 83935 75 0 0 25 0 1 0 489235554 82685952 19215 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20187 19215 603 41 0 20146 0
vsize: 80748
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 19515 0 0 0 84935 75 0 0 25 0 1 0 489235554 83210240 19363 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20315 19363 603 41 0 20274 0
vsize: 81260
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 19633 0 0 0 85934 76 0 0 25 0 1 0 489235554 83718144 19481 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20439 19481 603 41 0 20398 0
vsize: 81756
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 19716 0 0 0 86934 76 0 0 25 0 1 0 489235554 84111360 19564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20535 19564 603 41 0 20494 0
vsize: 82140
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 19847 0 0 0 87934 76 0 0 25 0 1 0 489235554 84635648 19695 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20663 19695 603 41 0 20622 0
vsize: 82652
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 20025 0 0 0 88934 77 0 0 25 0 1 0 489235554 85282816 19873 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20821 19873 603 41 0 20780 0
vsize: 83284
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 20205 0 0 0 89933 78 0 0 25 0 1 0 489235554 86073344 20053 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21014 20053 603 41 0 20973 0
vsize: 84056
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 20397 0 0 0 90933 78 0 0 25 0 1 0 489235554 86847488 20245 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21203 20245 603 41 0 21162 0
vsize: 84812
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 20597 0 0 0 91932 79 0 0 25 0 1 0 489235554 87633920 20445 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21395 20445 603 41 0 21354 0
vsize: 85580
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 20759 0 0 0 92932 79 0 0 25 0 1 0 489235554 88268800 20607 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21550 20607 603 41 0 21509 0
vsize: 86200
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 20901 0 0 0 93932 79 0 0 25 0 1 0 489235554 88924160 20749 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21710 20749 603 41 0 21669 0
vsize: 86840
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 20964 0 0 0 94932 80 0 0 25 0 1 0 489235554 89194496 20812 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21776 20812 603 41 0 21735 0
vsize: 87104
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 21022 0 0 0 95931 80 0 0 25 0 1 0 489235554 89456640 20870 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21840 20870 603 41 0 21799 0
vsize: 87360
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 21072 0 0 0 96931 81 0 0 25 0 1 0 489235554 89591808 20920 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21873 20920 603 41 0 21832 0
vsize: 87492
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 21259 0 0 0 97930 82 0 0 25 0 1 0 489235554 90361856 21107 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22061 21107 603 41 0 22020 0
vsize: 88244
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 21488 0 0 0 98930 82 0 0 25 0 1 0 489235554 91394048 21336 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22313 21336 603 41 0 22272 0
vsize: 89252
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 21616 0 0 0 99930 82 0 0 25 0 1 0 489235554 91783168 21464 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22408 21464 603 41 0 22367 0
vsize: 89632
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 21686 0 0 0 100929 83 0 0 25 0 1 0 489235554 92176384 21534 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22504 21534 603 41 0 22463 0
vsize: 90016
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 21765 0 0 0 101929 83 0 0 25 0 1 0 489235554 92442624 21613 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22569 21613 603 41 0 22528 0
vsize: 90276
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 21876 0 0 0 102929 84 0 0 25 0 1 0 489235554 92958720 21724 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22695 21724 603 41 0 22654 0
vsize: 90780
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 21995 0 0 0 103929 84 0 0 25 0 1 0 489235554 93458432 21843 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22817 21843 603 41 0 22776 0
vsize: 91268
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 22078 0 0 0 104929 84 0 0 25 0 1 0 489235554 93720576 21926 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22881 21926 603 41 0 22840 0
vsize: 91524
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 22264 0 0 0 105928 85 0 0 25 0 1 0 489235554 94523392 22112 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23077 22112 603 41 0 23036 0
vsize: 92308
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 22397 0 0 0 106929 85 0 0 25 0 1 0 489235554 95055872 22245 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23207 22245 603 41 0 23166 0
vsize: 92828
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 22515 0 0 0 107929 85 0 0 25 0 1 0 489235554 95576064 22363 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23334 22363 603 41 0 23293 0
vsize: 93336
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 22619 0 0 0 108928 86 0 0 25 0 1 0 489235554 95969280 22467 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23430 22467 603 41 0 23389 0
vsize: 93720
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 22761 0 0 0 109928 86 0 0 25 0 1 0 489235554 96497664 22609 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23559 22609 603 41 0 23518 0
vsize: 94236
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 22856 0 0 0 110928 86 0 0 25 0 1 0 489235554 96899072 22704 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23657 22704 603 41 0 23616 0
vsize: 94628
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 22911 0 0 0 111928 87 0 0 25 0 1 0 489235554 97173504 22759 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23724 22759 603 41 0 23683 0
vsize: 94896
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 23097 0 0 0 112928 87 0 0 25 0 1 0 489235554 97968128 22945 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23918 22945 603 41 0 23877 0
vsize: 95672
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 23231 0 0 0 113928 87 0 0 25 0 1 0 489235554 98488320 23079 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24045 23079 603 41 0 24004 0
vsize: 96180
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 23465 0 0 0 114927 88 0 0 25 0 1 0 489235554 99393536 23313 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24266 23313 603 41 0 24225 0
vsize: 97064
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 23711 0 0 0 115926 89 0 0 25 0 1 0 489235554 100458496 23559 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24526 23559 603 41 0 24485 0
vsize: 98104
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 23926 0 0 0 116926 89 0 0 25 0 1 0 489235554 101351424 23774 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24744 23774 603 41 0 24703 0
vsize: 98976
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 24127 0 0 0 117926 90 0 0 25 0 1 0 489235554 102137856 23975 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24936 23975 603 41 0 24895 0
vsize: 99744
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 24363 0 0 0 118926 90 0 0 25 0 1 0 489235554 103170048 24211 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25188 24211 603 41 0 25147 0
vsize: 100752
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13318
Raw data (stat): 13316 (minisat+) R 13315 22932 22931 0 -1 0 24548 0 0 0 119926 91 0 0 25 0 1 0 489235554 103833600 24396 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25350 24396 603 41 0 25309 0
vsize: 101400
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 13318
Raw data (stat): 13316 (minisat+) Z 13315 22932 22931 0 -1 12 24551 0 0 0 119926 95 0 0 25 0 1 0 489235554 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.09
CPU time (s): 1200.22
CPU user time (s): 1199.26
CPU system time (s): 0.957854
CPU usage (%): 100.011
Max. virtual memory (Kb): 101400
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####