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/submitted/manquinho/primes-dimacs-cnf/normalized-ii8c2.opb
MD5SUM	966ceb4249ada81e9b52daecca845c09
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	537
Optimality of the best value was proved	NO
Number of terms in the objective function	1900
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1900
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1900
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05684
Number of variables	1900
Total number of constraints	7639
Number of constraints which are clauses	7639
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	10
Trace number 6268

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        841040 kB
Buffers:         35204 kB
Cached:         121504 kB
SwapCached:       3160 kB
Active:          70976 kB
Inactive:        91732 kB
HighTotal:      131008 kB
HighFree:         6188 kB
LowTotal:       903652 kB
LowFree:        834852 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25332 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:22:44 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 4684 7 1200.32 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 7639 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    7639    17170 |    2546       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 846[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:108112     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        20 |  276107   644808 |   92035      20      433    21.6 |  0.000 % |
c |       120 |  270292   631476 |  101238      46      824    17.9 |  1.984 % |
c |       271 |  264772   618777 |  111362     109     1307    12.0 |  3.813 % |
c |       496 |  256513   599768 |  122498     178     1756     9.9 |  6.622 % |
c |       833 |  243150   569026 |  134748     347     3904    11.3 | 11.149 % |
c |      1339 |  228720   535779 |  148223     656     7563    11.5 | 16.090 % |
c |      2098 |  204064   478913 |  163045    1113    12930    11.6 | 24.601 % |
c |      3237 |  182398   428813 |  179350    1909    21473    11.2 | 32.187 % |
c |      4946 |  160372   377707 |  197285    3176    48229    15.2 | 39.885 % |
c |      7508 |  138971   328130 |  217013    5415    75845    14.0 | 47.382 % |
c |     11352 |  134884   318635 |  238715    9157   134593    14.7 | 48.824 % |
c ==============================================================================
c [1mFound solution: 808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14185 |  125912   297906 |   41970   11798   177799    15.1 | 48.824 % |
c |     14285 |  125912   297906 |   46167   11898   178446    15.0 | 52.156 % |
c |     14435 |  125783   297610 |   50783   12045   179709    14.9 | 52.199 % |
c |     14661 |  125783   297610 |   55862   12271   183700    15.0 | 52.199 % |
c |     14998 |  125586   297155 |   61448   12606   186430    14.8 | 52.268 % |
c |     15505 |  125143   296127 |   67593   13094   193906    14.8 | 52.422 % |
c |     16264 |  125143   296127 |   74352   13853   207212    15.0 | 52.422 % |
c |     17403 |  125143   296127 |   81787   14992   230111    15.3 | 52.422 % |
c |     19111 |  124093   293691 |   89966   16671   276748    16.6 | 52.798 % |
c |     21673 |  123559   292458 |   98963   19211   324832    16.9 | 52.981 % |
c ==============================================================================
c [1mFound solution: 796[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22939 |  123647   292715 |   41215   20438   336825    16.5 | 52.981 % |
c |     23039 |  123647   292715 |   45336   20538   337454    16.4 | 53.011 % |
c ==============================================================================
c [1mFound solution: 783[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23134 |  124014   293628 |   41338   20633   338351    16.4 | 53.011 % |
c |     23234 |  124014   293628 |   45471   20733   341474    16.5 | 52.958 % |
c |     23384 |  124014   293628 |   50018   20883   343105    16.4 | 52.958 % |
c |     23609 |  124014   293628 |   55020   21108   346363    16.4 | 52.958 % |
c |     23946 |  123851   293254 |   60522   21432   349807    16.3 | 53.013 % |
c ==============================================================================
c [1mFound solution: 746[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24213 |  124536   294924 |   41512   21697   351911    16.2 | 53.013 % |
c |     24313 |  124536   294924 |   45663   21797   352835    16.2 | 52.906 % |
c |     24463 |  124536   294924 |   50229   21947   355305    16.2 | 52.906 % |
c |     24690 |  124048   293800 |   55252   22165   359207    16.2 | 53.072 % |
c |     25029 |  124048   293800 |   60777   22504   363486    16.2 | 53.072 % |
c |     25535 |  124048   293800 |   66855   23010   370951    16.1 | 53.072 % |
c |     26294 |  124048   293800 |   73541   23769   382182    16.1 | 53.072 % |
c ==============================================================================
c [1mFound solution: 741[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26687 |  124254   294320 |   41418   24162   385751    16.0 | 53.072 % |
c |     26787 |  124142   294061 |   45559   24261   386365    15.9 | 53.081 % |
c |     26937 |  124142   294061 |   50115   24411   388417    15.9 | 53.081 % |
c |     27162 |  124040   293826 |   55127   24626   392062    15.9 | 53.116 % |
c |     27499 |  124040   293826 |   60640   24963   396436    15.9 | 53.116 % |
c |     28009 |  124040   293826 |   66704   25473   407465    16.0 | 53.116 % |
c |     28768 |  123756   293172 |   73374   26202   422577    16.1 | 53.213 % |
c |     29907 |  123756   293172 |   80711   27341   443082    16.2 | 53.213 % |
c |     31615 |  123756   293172 |   88783   29049   487447    16.8 | 53.213 % |
c |     34177 |  123756   293172 |   97661   31611   543060    17.2 | 53.213 % |
c |     38021 |  123202   291887 |  107427   35426   670270    18.9 | 53.412 % |
c |     43787 |  121857   288759 |  118170   41133   808816    19.7 | 53.902 % |
c |     52436 |  121857   288759 |  129987   49782  1161162    23.3 | 53.902 % |
c |     65411 |  121668   288319 |  142986   62743  2086400    33.3 | 53.972 % |
c ==============================================================================
c [1mFound solution: 740[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69650 |  121038   286851 |   40346   66272  2126745    32.1 | 53.972 % |
c |     69751 |  121038   286851 |   44380   66373  2128180    32.1 | 54.182 % |
c |     69901 |  121038   286851 |   48818   66523  2130569    32.0 | 54.182 % |
c |     70126 |  121038   286851 |   53700   66748  2136322    32.0 | 54.182 % |
c |     70463 |  121038   286851 |   59070   67085  2149635    32.0 | 54.182 % |
c |     70973 |  120907   286549 |   64977   67585  2154926    31.9 | 54.227 % |
c |     71732 |  120907   286549 |   71475   68344  2168005    31.7 | 54.227 % |
c |     72873 |  120907   286549 |   78622   69485  2217858    31.9 | 54.227 % |
c |     74582 |  120709   286094 |   86485   71179  2268021    31.9 | 54.293 % |
c |     77146 |  120641   285937 |   95133   73741  2505578    34.0 | 54.316 % |
c ==============================================================================
c [1mFound solution: 739[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     80218 |  120418   285443 |   40139   76808  2581948    33.6 | 54.316 % |
c |     80318 |  120299   285170 |   44152   76880  2582620    33.6 | 54.451 % |
c |     80469 |  120299   285170 |   48568   77031  2585195    33.6 | 54.451 % |
c |     80695 |  120299   285170 |   53425   77257  2596142    33.6 | 54.451 % |
c |     81032 |  120299   285170 |   58767   77594  2607820    33.6 | 54.451 % |
c |     81538 |  120299   285170 |   64644   78100  2641753    33.8 | 54.451 % |
c |     82297 |  120299   285170 |   71108   78859  2677859    34.0 | 54.451 % |
c |     83436 |  120163   284856 |   78219   79855  2756128    34.5 | 54.498 % |
c |     85145 |  119853   284135 |   86041   81429  2789620    34.3 | 54.611 % |
c |     87707 |  119853   284135 |   94645   83991  2846056    33.9 | 54.611 % |
c ==============================================================================
c [1mFound solution: 738[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90188 |  119766   283919 |   39922   86440  2933607    33.9 | 54.611 % |
c |     90288 |  119659   283671 |   43914   86529  2934638    33.9 | 54.669 % |
c |     90438 |  119659   283671 |   48305   86679  2937273    33.9 | 54.669 % |
c |     90663 |  119659   283671 |   53136   86904  2943105    33.9 | 54.669 % |
c |     91000 |  119659   283671 |   58449   87241  2950529    33.8 | 54.669 % |
c |     91506 |  119592   283517 |   64294   87745  2956660    33.7 | 54.692 % |
c |     92266 |  119500   283303 |   70724   88504  2970336    33.6 | 54.726 % |
c |     93405 |  119058   282282 |   77796   89573  2998836    33.5 | 54.880 % |
c |     95113 |  119058   282282 |   85576   91281  3042705    33.3 | 54.880 % |
c |     97675 |  119058   282282 |   94133   93843  3211205    34.2 | 54.880 % |
c |    101519 |  119048   282259 |  103547   97684  3348633    34.3 | 54.883 % |
c |    107286 |  119044   282250 |  113902  103450  3526213    34.1 | 54.884 % |
c ==============================================================================
c [1mFound solution: 720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    112465 |  119321   282936 |   39773  108503  3714658    34.2 | 54.884 % |
c |    112566 |  119321   282936 |   43750   27838   526879    18.9 | 54.860 % |
c |    112717 |  119321   282936 |   48125   27989   528782    18.9 | 54.860 % |
c |    112946 |  119321   282936 |   52937   28218   533812    18.9 | 54.860 % |
c |    113284 |  119321   282936 |   58231   28556   539993    18.9 | 54.860 % |
c |    113790 |  119321   282936 |   64054   29062   551525    19.0 | 54.860 % |
c |    114549 |  119217   282692 |   70460   29817   581694    19.5 | 54.900 % |
c |    115688 |  118740   281590 |   77506   30943   614155    19.8 | 55.067 % |
c |    117396 |  118740   281590 |   85256   32651   662928    20.3 | 55.067 % |
c |    119958 |  118575   281207 |   93782   35211   741749    21.1 | 55.127 % |
c |    123802 |  118575   281207 |  103160   39055  1360189    34.8 | 55.127 % |
c |    129568 |  118245   280441 |  113477   44815  1569396    35.0 | 55.246 % |
c |    138218 |  118240   280431 |  124824   53464  1874642    35.1 | 55.247 % |
c ==============================================================================
c [1mFound solution: 715[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    147998 |  118358   280745 |   39452   63242  2803116    44.3 | 55.247 % |
c |    148099 |  118358   280745 |   43397   63343  2804582    44.3 | 55.243 % |
c |    148249 |  118358   280745 |   47736   63493  2806641    44.2 | 55.243 % |
c |    148474 |  118261   280522 |   52510   63715  2808393    44.1 | 55.276 % |
c |    148811 |  118261   280522 |   57761   64052  2822813    44.1 | 55.276 % |
c |    149318 |  118261   280522 |   63537   64559  2853389    44.2 | 55.276 % |
c |    150077 |  118261   280522 |   69891   65318  2870296    43.9 | 55.276 % |
c |    151217 |  118241   280474 |   76880   66457  2906546    43.7 | 55.285 % |
c |    152925 |  118241   280474 |   84568   68165  2953167    43.3 | 55.284 % |
c |    155487 |  118241   280474 |   93025   70727  3039534    43.0 | 55.284 % |
c |    159332 |  118241   280474 |  102328   74572  3193739    42.8 | 55.284 % |
c ==============================================================================
c [1mFound solution: 714[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    162452 |  118061   280042 |   39353   77573  3511774    45.3 | 55.284 % |
c |    162552 |  118061   280042 |   43288   77673  3513017    45.2 | 55.343 % |
c |    162703 |  118061   280042 |   47617   77824  3518065    45.2 | 55.343 % |
c |    162928 |  118000   279902 |   52378   78048  3524669    45.2 | 55.364 % |
c |    163265 |  118000   279902 |   57616   78385  3538805    45.1 | 55.364 % |
c |    163772 |  118000   279902 |   63378   78892  3550419    45.0 | 55.364 % |
c |    164532 |  118000   279902 |   69716   79652  3578686    44.9 | 55.364 % |
c |    165671 |  118000   279902 |   76687   80791  3644935    45.1 | 55.364 % |
c |    167380 |  117922   279718 |   84356   82490  3681611    44.6 | 55.396 % |
c |    169942 |  117922   279718 |   92792   85052  3788844    44.5 | 55.396 % |
c |    173788 |  117922   279718 |  102071   88898  4003414    45.0 | 55.396 % |
c |    179554 |  117682   279167 |  112278   94636  4216000    44.5 | 55.475 % |
c |    188204 |  117577   278926 |  123506  103281  4537215    43.9 | 55.510 % |
c ==============================================================================
c [1mFound solution: 713[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    198820 |  117660   279141 |   39220  113897  5008782    44.0 | 55.510 % |
c |    198920 |  117660   279141 |   43142   34319   687772    20.0 | 55.498 % |
c |    199073 |  117660   279141 |   47456   34472   690167    20.0 | 55.498 % |
c |    199298 |  117660   279141 |   52201   34697   702157    20.2 | 55.498 % |
c |    199636 |  117660   279141 |   57422   35035   711744    20.3 | 55.498 % |
c |    200143 |  117547   278877 |   63164   35536   717500    20.2 | 55.540 % |
c |    200905 |  117547   278877 |   69480   36298   727502    20.0 | 55.540 % |
c |    202046 |  117427   278597 |   76428   36027   729955    20.3 | 55.585 % |
c |    203754 |  117216   278107 |   84071   37645   767162    20.4 | 55.661 % |
c |    206317 |  117216   278107 |   92478   40208  1038240    25.8 | 55.661 % |
c |    210161 |  117216   278107 |  101726   44052  1351601    30.7 | 55.661 % |
c |    215928 |  117216   278107 |  111899   49819  1787566    35.9 | 55.661 % |
c |    224577 |  117216   278107 |  123089   58468  2287030    39.1 | 55.661 % |
c |    237551 |  117113   277869 |  135398   71408  4460002    62.5 | 55.697 % |
c ==============================================================================
c [1mFound solution: 712[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    242327 |  117020   277628 |   39006   75975  4696117    61.8 | 55.697 % |
c |    242429 |  117020   277628 |   42906   76077  4698253    61.8 | 55.720 % |
c |    242580 |  117020   277628 |   47197   76228  4703110    61.7 | 55.720 % |
c |    242807 |  117020   277628 |   51916   76455  4708054    61.6 | 55.720 % |
c |    243144 |  117020   277628 |   57108   76792  4726775    61.6 | 55.720 % |
c |    243652 |  116848   277233 |   62819   77296  4741204    61.3 | 55.778 % |
c |    244411 |  116743   276985 |   69101   78044  4759259    61.0 | 55.820 % |
c |    245551 |  116743   276985 |   76011   79184  4803530    60.7 | 55.820 % |
c |    247261 |  116743   276985 |   83612   80894  4879802    60.3 | 55.820 % |
c |    249824 |  116743   276985 |   91974   83457  5011227    60.0 | 55.820 % |
c ==============================================================================
c [1mFound solution: 699[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    252455 |  117121   277917 |   39040   86088  5157614    59.9 | 55.820 % |
c |    252555 |  117121   277917 |   42944   86188  5160552    59.9 | 55.757 % |
c |    252707 |  117121   277917 |   47238   86340  5163451    59.8 | 55.757 % |
c |    252932 |  117121   277917 |   51962   86565  5165959    59.7 | 55.757 % |
c |    253269 |  117121   277917 |   57158   86902  5175594    59.6 | 55.757 % |
c |    253775 |  117121   277917 |   62874   87408  5202211    59.5 | 55.757 % |
c |    254534 |  117005   277647 |   69161   88158  5252283    59.6 | 55.799 % |
c |    255673 |  117005   277647 |   76077   89297  5431503    60.8 | 55.799 % |
c |    257381 |  117005   277647 |   83685   91005  5468681    60.1 | 55.799 % |
c ==============================================================================
c [1mFound solution: 677[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    259159 |  117537   278945 |   39179   92783  5577566    60.1 | 55.799 % |
c |    259260 |  117537   278945 |   43096   33525   858965    25.6 | 55.707 % |
c |    259410 |  117537   278945 |   47406   33675   869667    25.8 | 55.707 % |
c |    259635 |  117438   278719 |   52147   33897   872514    25.7 | 55.739 % |
c |    259972 |  117438   278719 |   57361   34234   882579    25.8 | 55.739 % |
c |    260479 |  117438   278719 |   63098   34741   895000    25.8 | 55.739 % |
c |    261239 |  117438   278719 |   69407   35501   904358    25.5 | 55.739 % |
c |    262379 |  117438   278719 |   76348   36641   919432    25.1 | 55.739 % |
c |    264088 |  117016   277743 |   83983   37092   937512    25.3 | 55.886 % |
c |    266650 |  117016   277743 |   92382   39654  1076409    27.1 | 55.886 % |
c |    270494 |  117016   277743 |  101620   43498  1267336    29.1 | 55.886 % |
c |    276261 |  117016   277743 |  111782   49265  1885617    38.3 | 55.886 % |
c ==============================================================================
c [1mFound solution: 638[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    283047 |  117459   278835 |   39153   56019  2288555    40.9 | 55.886 % |
c |    283147 |  117459   278835 |   43068   56119  2289260    40.8 | 55.851 % |
c |    283297 |  117459   278835 |   47375   56269  2293403    40.8 | 55.851 % |
c |    283522 |  117459   278835 |   52112   56494  2296347    40.6 | 55.851 % |
c |    283862 |  117459   278835 |   57323   56834  2310213    40.6 | 55.851 % |
c |    284368 |  117459   278835 |   63056   57340  2326186    40.6 | 55.851 % |
c |    285127 |  117459   278835 |   69361   58099  2335637    40.2 | 55.851 % |
c |    286266 |  117459   278835 |   76298   59238  2450321    41.4 | 55.851 % |
c |    287974 |  117459   278835 |   83927   60946  2507944    41.2 | 55.851 % |
c |    290537 |  117459   278835 |   92320   63509  2576935    40.6 | 55.851 % |
c |    294385 |  117459   278835 |  101552   67357  2662253    39.5 | 55.851 % |
c |    300152 |  117459   278835 |  111708   73124  2867759    39.2 | 55.851 % |
c |    308802 |  117459   278835 |  122878   81774  3077818    37.6 | 55.851 % |
c ==============================================================================
c [1mFound solution: 637[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    319513 |  117337   278569 |   39112   92427  4343822    47.0 | 55.851 % |
c |    319614 |  117337   278569 |   43023   30461  1419890    46.6 | 55.916 % |
c |    319764 |  117337   278569 |   47325   30611  1422421    46.5 | 55.916 % |
c |    319989 |  117337   278569 |   52058   30836  1436537    46.6 | 55.916 % |
c |    320330 |  117337   278569 |   57263   31177  1468685    47.1 | 55.916 % |
c |    320838 |  117337   278569 |   62990   31685  1492538    47.1 | 55.916 % |
c |    321597 |  117337   278569 |   69289   32444  1523868    47.0 | 55.916 % |
c |    322736 |  117337   278569 |   76218   33583  1567768    46.7 | 55.916 % |
c |    324445 |  117337   278569 |   83840   35292  1901289    53.9 | 55.916 % |
c |    327008 |  117337   278569 |   92224   37855  1976120    52.2 | 55.916 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x1 -x2 x3 -x4 x5 -x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 -x25 x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 x45 -x46 x47 -x48 -x49 x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 -x89 x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 -x121 x122 x123 -x124 x125 -x126 x127 -x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 -x153 x154 x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 -x185 x186 x187 -x188 x189 -x190 x191 -x192 x193 -x194 x195 -x196 x197 -x198 x199 -x200 x201 -x202 x203 -x204 x205 -x206 x207 -x208 x209 -x210 x211 -x212 x213 -x214 x215 -x216 -x217 x218 x219 -x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 x229 -x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 x241 -x242 x243 -x244 x245 -x246 x247 -x248 -x249 x250 x251 -x252 x253 -x254 x255 -x256 x257 -x258 x259 -x260 x261 -x262 x263 -x264 x265 -x266 -x267 -x268 x269 -x270 x271 -x272 x273 -x274 x275 -x276 -x277 x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 -x287 x288 x289 -x290 x291 -x292 x293 -x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 x307 -x308 x309 -x310 x311 -x312 -x313 x314 x315 -x316 x317 -x318 x319 -x320 -x321 x322 x323 -x324 -x325 x326 -x327 x328 -x329 x330 -x331 x332 -x333 x334 -x335 x336 -x337 x338 -x339 x340 -x341 -x342 -x343 x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 x353 -x354 -x355 -x356 -x357 x358 -x359 -x360 -x361 x362 x363 -x364 -x365 x366 -x367 x368 -x369 x370 -x371 x372 -x373 x374 -x375 x376 -x377 x378 -x379 x380 -x381 -x382 -x383 -x384 x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 x398 -x399 -x400 -x401 -x402 -x403 x404 -x405 -x406 -x407 -x408 x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 x422 x423 -x424 -x425 x426 -x427 x428 -x429 x430 -x431 x432 -x433 x434 -x435 x436 -x437 x438 -x439 x440 -x441 x442 -x443 -x444 x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 x458 -x459 x460 -x461 x462 x463 -x464 -x465 x466 -x467 x468 -x469 x470 -x471 x472 -x473 x474 -x475 x476 -x477 x478 -x479 x480 -x481 x482 -x483 -x484 -x485 x486 -x487 x488 -x489 x490 -x491 x492 -x493 x494 -x495 x496 x497 -x498 -x499 x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 x518 -x519 -x520 -x521 x522 x523 -x524 -x525 x526 -x527 x528 -x529 x530 -x531 x532 -x533 x534 -x535 x536 -x537 x538 -x539 x540 x541 -x542 -x543 x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 x558 -x559 -x560 -x561 x562 x563 -x564 -x565 x566 -x567 x568 -x569 x570 -x571 x572 -x573 x574 -x575 x576 -x577 x578 -x579 x580 -x581 x582 x583 -x584 -x585 x586 -x587 x588 -x589 x590 -x591 x592 -x593 x594 -x595 x596 -x597 x598 -x599 x600 -x601 -x602 -x603 x604 -x605 -x606 -x607 -x608 x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 x618 -x619 -x620 -x621 -x622 -x623 x624 x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 x658 -x659 -x660 x661 -x662 -x663 x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 x678 -x679 -x680 -x681 -x682 -x683 x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 x693 -x694 -x695 -x696 -x697 x698 -x699 -x700 x701 -x702 -x703 x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 x718 -x719 -x720 -x721 x722 x723 -x724 -x725 x726 -x727 x728 -x729 x730 -x731 x732 -x733 x734 -x735 x736 -x737 x738 -x739 x740 x741 -x742 -x743 x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 x758 -x759 -x760 -x761 x762 -x763 -x764 -x765 x766 -x767 x768 -x769 x770 -x771 x772 -x773 x774 -x775 x776 x777 -x778 -x779 x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 x793 -x794 -x795 -x796 -x797 x798 -x799 -x800 -x801 x802 x803 -x804 -x805 x806 -x807 x808 -x809 x810 -x811 x812 -x813 x814 -x815 x816 -x817 x818 -x819 x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 x831 -x832 -x833 -x834 -x835 -x836 -x837 x838 -x839 -x840 -x841 x842 x843 -x844 -x845 x846 -x847 x848 -x849 x850 -x851 x852 -x853 x854 -x855 x856 -x857 x858 -x859 x860 -x861 x862 x863 -x864 -x865 x866 -x867 x868 -x869 x870 -x871 x872 -x873 x874 -x875 x876 -x877 x878 -x879 x880 -x881 x882 -x883 -x884 -x885 x886 -x887 x888 -x889 x890 -x891 x892 -x893 x894 -x895 x896 x897 -x898 -x899 x900 -x901 -x902 -x903 x904 -x905 -x906 -x907 -x908 x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 x918 -x919 -x920 -x921 x922 x923 -x924 -x925 x926 -x927 x928 -x929 x930 -x931 x932 -x933 x934 -x935 x936 -x937 x938 -x939 x940 -x941 x942 x943 -x944 -x945 x946 -x947 x948 -x949 x950 -x951 x952 -x953 x954 -x955 x956 -x957 x958 -x959 x960 -x961 x962 -x963 x964 x965 -x966 x967 -x968 x969 -x970 x971 -x972 -x973 x974 x975 -x976 -x977 x978 -x979 x980 -x981 x982 x983 -x984 -x985 x986 -x987 x988 -x989 x990 -x991 x992 -x993 x994 -x995 x996 -x997 x998 -x999 x1000 -x1001 x1002 -x1003 x1004 -x1005 x1006 x1007 -x1008 -x1009 x1010 -x1011 x1012 -x1013 x1014 -x1015 x1016 -x1017 x1018 -x1019 x1020 -x1021 x1022 x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 x1038 -x1039 -x1040 -x1041 x1042 -x1043 -x1044 -x1045 x1046 -x1047 x1048 -x1049 x1050 -x1051 x1052 -x1053 x1054 -x1055 x1056 x1057 -x1058 -x1059 x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 x1078 x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 x1098 x1099 -x1100 -x1101 -x1102 -x1103 x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 x1113 -x1114 -x1115 -x1116 -x1117 x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 x1138 x1139 -x1140 -x1141 -x1142 -x1143 x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 x1154 x1155 -x1156 -x1157 x1158 -x1159 x1160 -x1161 x1162 x1163 -x1164 -x1165 x1166 -x1167 x1168 -x1169 x1170 -x1171 x1172 -x1173 x1174 -x1175 x1176 -x1177 x1178 -x1179 x1180 -x1181 x1182 -x1183 -x1184 -x1185 x1186 -x1187 x1188 -x1189 x1190 -x1191 x1192 -x1193 x1194 -x1195 x1196 x1197 -x1198 -x1199 x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 x1238 -x1239 -x1240 -x1241 -x1242 -x1243 x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 x1258 -x1259 -x1260 x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 x1281 -x1282 -x1283 x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 x1298 -x1299 -x1300 -x1301 x1302 x1303 -x1304 -x1305 x1306 -x1307 x1308 -x1309 x1310 -x1311 x1312 -x1313 x1314 -x1315 x1316 -x1317 x1318 -x1319 x1320 -x1321 -x1322 -x1323 x1324 x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 x1338 -x1339 -x1340 -x1341 x1342 x1343 -x1344 -x1345 x1346 -x1347 x1348 -x1349 x1350 -x1351 x1352 -x1353 x1354 -x1355 x1356 -x1357 x1358 -x1359 x1360 -x1361 x1362 x1363 -x1364 -x1365 x1366 -x1367 x1368 -x1369 x1370 -x1371 x1372 -x1373 x1374 -x1375 x1376 -x1377 -x1378 -x1379 x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x139#### 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.86 0.97 0.91 2/54 25028
Raw data (stat): 25028 (runsolver) R 25027 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481555664 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8105 0 0 0 980 18 0 0 25 0 1 0 481555664 37306368 7809 4294967295 134512640 134672761 3221224576 3221223748 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9108 7809 603 41 0 9067 0
vsize: 36432
[startup+20.0012 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8106 0 0 0 1980 18 0 0 25 0 1 0 481555664 37306368 7810 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9108 7810 603 41 0 9067 0
vsize: 36432
[startup+30.0014 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8122 0 0 0 2979 18 0 0 25 0 1 0 481555664 37306368 7826 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9108 7826 603 41 0 9067 0
vsize: 36432
[startup+40.0012 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8123 0 0 0 3978 18 0 0 25 0 1 0 481555664 37306368 7827 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9108 7827 603 41 0 9067 0
vsize: 36432
[startup+50.0014 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8125 0 0 0 4979 18 0 0 25 0 1 0 481555664 37306368 7829 4294967295 134512640 134672761 3221224576 3221223764 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9108 7829 603 41 0 9067 0
vsize: 36432
[startup+60.0018 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8128 0 0 0 5979 18 0 0 25 0 1 0 481555664 37306368 7832 4294967295 134512640 134672761 3221224576 3221223728 1074744231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9108 7832 603 41 0 9067 0
vsize: 36432
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8128 0 0 0 6978 19 0 0 25 0 1 0 481555664 37306368 7832 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9108 7832 603 41 0 9067 0
vsize: 36432
[startup+80.0029 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8143 0 0 0 7977 19 0 0 25 0 1 0 481555664 37306368 7847 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9108 7847 603 41 0 9067 0
vsize: 36432
[startup+90.0033 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8149 0 0 0 8977 19 0 0 25 0 1 0 481555664 37441536 7853 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9141 7853 603 41 0 9100 0
vsize: 36564
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8159 0 0 0 9977 19 0 0 25 0 1 0 481555664 37441536 7863 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9141 7863 603 41 0 9100 0
vsize: 36564
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8164 0 0 0 10978 19 0 0 25 0 1 0 481555664 37441536 7868 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9141 7868 603 41 0 9100 0
vsize: 36564
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8196 0 0 0 11978 19 0 0 25 0 1 0 481555664 37576704 7900 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9174 7900 603 41 0 9133 0
vsize: 36696
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8223 0 0 0 12978 19 0 0 25 0 1 0 481555664 37711872 7927 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9207 7927 603 41 0 9166 0
vsize: 36828
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8430 0 0 0 13977 20 0 0 25 0 1 0 481555664 38985728 8134 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9518 8134 603 41 0 9477 0
vsize: 38072
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8496 0 0 0 14977 20 0 0 25 0 1 0 481555664 39346176 8200 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9606 8200 603 41 0 9565 0
vsize: 38424
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8637 0 0 0 15976 21 0 0 25 0 1 0 481555664 39587840 8292 4294967295 134512640 134672761 3221224576 3221223700 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8292 603 41 0 9624 0
vsize: 38660
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8697 0 0 0 16977 21 0 0 25 0 1 0 481555664 39763968 8316 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9708 8316 603 41 0 9667 0
vsize: 38832
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25028
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8818 0 0 0 17976 21 0 0 25 0 1 0 481555664 40165376 8437 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9806 8437 603 41 0 9765 0
vsize: 39224
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 8960 0 0 0 18976 21 0 0 25 0 1 0 481555664 40968192 8579 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10002 8579 603 41 0 9961 0
vsize: 40008
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 9061 0 0 0 19976 22 0 0 25 0 1 0 481555664 41238528 8680 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10068 8680 603 41 0 10027 0
vsize: 40272
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 9179 0 0 0 20976 22 0 0 25 0 1 0 481555664 41779200 8798 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10200 8798 603 41 0 10159 0
vsize: 40800
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 9466 0 0 0 21976 22 0 0 25 0 1 0 481555664 42979328 9085 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10493 9085 603 41 0 10452 0
vsize: 41972
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 9785 0 0 0 22975 23 0 0 25 0 1 0 481555664 44191744 9404 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10789 9404 603 41 0 10748 0
vsize: 43156
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 10135 0 0 0 23974 25 0 0 25 0 1 0 481555664 45666304 9754 4294967295 134512640 134672761 3221224576 3221223680 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11149 9754 603 41 0 11108 0
vsize: 44596
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 10513 0 0 0 24973 25 0 0 25 0 1 0 481555664 47149056 10132 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11511 10132 603 41 0 11470 0
vsize: 46044
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 10718 0 0 0 25973 26 0 0 25 0 1 0 481555664 48209920 10337 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11770 10337 603 41 0 11729 0
vsize: 47080
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 10798 0 0 0 26973 26 0 0 25 0 1 0 481555664 48349184 10382 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 10382 603 41 0 11763 0
vsize: 47216
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 10900 0 0 0 27973 26 0 0 25 0 1 0 481555664 48857088 10484 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11928 10484 603 41 0 11887 0
vsize: 47712
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 11042 0 0 0 28973 27 0 0 25 0 1 0 481555664 49381376 10626 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12056 10626 603 41 0 12015 0
vsize: 48224
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 11165 0 0 0 29973 27 0 0 25 0 1 0 481555664 49917952 10749 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12187 10749 603 41 0 12146 0
vsize: 48748
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 11328 0 0 0 30972 27 0 0 25 0 1 0 481555664 50434048 10876 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12313 10876 603 41 0 12272 0
vsize: 49252
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 11462 0 0 0 31973 28 0 0 25 0 1 0 481555664 50974720 11010 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12445 11010 603 41 0 12404 0
vsize: 49780
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 11613 0 0 0 32972 28 0 0 25 0 1 0 481555664 51515392 11161 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12577 11161 603 41 0 12536 0
vsize: 50308
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 11755 0 0 0 33972 29 0 0 25 0 1 0 481555664 51961856 11267 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12686 11267 603 41 0 12645 0
vsize: 50744
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 11853 0 0 0 34972 29 0 0 25 0 1 0 481555664 52355072 11365 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12782 11365 603 41 0 12741 0
vsize: 51128
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12015 0 0 0 35971 30 0 0 25 0 1 0 481555664 53026816 11527 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12946 11527 603 41 0 12905 0
vsize: 51784
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12155 0 0 0 36971 30 0 0 25 0 1 0 481555664 53567488 11667 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13078 11667 603 41 0 13037 0
vsize: 52312
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12283 0 0 0 37971 31 0 0 25 0 1 0 481555664 54104064 11795 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13209 11795 603 41 0 13168 0
vsize: 52836
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12388 0 0 0 38971 31 0 0 25 0 1 0 481555664 54509568 11900 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13308 11900 603 41 0 13267 0
vsize: 53232
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12560 0 0 0 39970 31 0 0 25 0 1 0 481555664 55177216 12072 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13471 12072 603 41 0 13430 0
vsize: 53884
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12726 0 0 0 40970 32 0 0 25 0 1 0 481555664 55844864 12238 4294967295 134512640 134672761 3221224576 3221223744 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13634 12238 603 41 0 13593 0
vsize: 54536
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 41970 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 42970 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223760 134558713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 43970 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 44970 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223680 134559976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 45971 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 46971 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 47971 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 48971 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 49971 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 50972 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 51972 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12796 0 0 0 52972 32 0 0 25 0 1 0 481555664 55939072 12272 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12272 603 41 0 13616 0
vsize: 54628
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12805 0 0 0 53972 32 0 0 25 0 1 0 481555664 55963648 12278 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13663 12278 603 41 0 13622 0
vsize: 54652
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12805 0 0 0 54972 32 0 0 25 0 1 0 481555664 55963648 12278 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13663 12278 603 41 0 13622 0
vsize: 54652
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12805 0 0 0 55973 32 0 0 25 0 1 0 481555664 55963648 12278 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13663 12278 603 41 0 13622 0
vsize: 54652
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12805 0 0 0 56973 32 0 0 25 0 1 0 481555664 55963648 12278 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13663 12278 603 41 0 13622 0
vsize: 54652
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12805 0 0 0 57973 32 0 0 25 0 1 0 481555664 55963648 12278 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13663 12278 603 41 0 13622 0
vsize: 54652
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12832 0 0 0 58973 32 0 0 25 0 1 0 481555664 55963648 12278 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13663 12278 603 41 0 13622 0
vsize: 54652
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 12954 0 0 0 59973 33 0 0 25 0 1 0 481555664 56500224 12400 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13794 12400 603 41 0 13753 0
vsize: 55176
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 13065 0 0 0 60973 33 0 0 25 0 1 0 481555664 57040896 12511 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13926 12511 603 41 0 13885 0
vsize: 55704
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 13270 0 0 0 61973 34 0 0 25 0 1 0 481555664 57847808 12716 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14123 12716 603 41 0 14082 0
vsize: 56492
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 13364 0 0 0 62973 34 0 0 25 0 1 0 481555664 58245120 12810 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14220 12810 603 41 0 14179 0
vsize: 56880
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 13466 0 0 0 63972 34 0 0 25 0 1 0 481555664 58642432 12912 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14317 12912 603 41 0 14276 0
vsize: 57268
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 13546 0 0 0 64972 35 0 0 25 0 1 0 481555664 58908672 12992 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14382 12992 603 41 0 14341 0
vsize: 57528
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 13652 0 0 0 65972 35 0 0 25 0 1 0 481555664 59441152 13098 4294967295 134512640 134672761 3221224576 3221223712 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14512 13098 603 41 0 14471 0
vsize: 58048
[startup+670.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 13754 0 0 0 66972 35 0 0 25 0 1 0 481555664 59838464 13200 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14609 13200 603 41 0 14568 0
vsize: 58436
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 13855 0 0 0 67972 36 0 0 25 0 1 0 481555664 60231680 13301 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14705 13301 603 41 0 14664 0
vsize: 58820
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 13969 0 0 0 68972 36 0 0 25 0 1 0 481555664 60637184 13415 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14804 13415 603 41 0 14763 0
vsize: 59216
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14171 0 0 0 69972 36 0 0 25 0 1 0 481555664 61583360 13617 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15035 13617 603 41 0 14994 0
vsize: 60140
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14307 0 0 0 70972 37 0 0 25 0 1 0 481555664 62124032 13753 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15167 13753 603 41 0 15126 0
vsize: 60668
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14408 0 0 0 71971 37 0 0 25 0 1 0 481555664 62517248 13854 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15263 13854 603 41 0 15222 0
vsize: 61052
[startup+730.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 72972 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 73972 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 74972 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223792 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+760.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 75972 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+770.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 76972 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223760 134559159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+780.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 77972 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 78973 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+800.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 79973 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 80973 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+820.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 81973 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+830.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 82973 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 83974 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+850.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 84974 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 85974 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223744 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+870.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14475 0 0 0 86980 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+880.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14488 0 0 0 87985 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+890.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14488 0 0 0 88985 37 0 0 25 0 1 0 481555664 62537728 13887 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15268 13887 603 41 0 15227 0
vsize: 61072
[startup+900.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14614 0 0 0 89985 37 0 0 25 0 1 0 481555664 63070208 14013 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15398 14013 603 41 0 15357 0
vsize: 61592
[startup+910.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14876 0 0 0 90984 38 0 0 25 0 1 0 481555664 64069632 14261 4294967295 134512640 134672761 3221224576 3221222848 134545024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15642 14261 603 41 0 15601 0
vsize: 62568
[startup+920.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 14946 0 0 0 91984 39 0 0 25 0 1 0 481555664 64368640 14309 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15715 14309 603 41 0 15674 0
vsize: 62860
[startup+930.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15143 0 0 0 92984 39 0 0 25 0 1 0 481555664 65175552 14506 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15912 14506 603 41 0 15871 0
vsize: 63648
[startup+940.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15276 0 0 0 93983 40 0 0 25 0 1 0 481555664 65716224 14639 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16044 14639 603 41 0 16003 0
vsize: 64176
[startup+950.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15350 0 0 0 94983 40 0 0 25 0 1 0 481555664 65765376 14677 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14677 603 41 0 16015 0
vsize: 64224
[startup+960.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15350 0 0 0 95983 40 0 0 25 0 1 0 481555664 65765376 14677 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14677 603 41 0 16015 0
vsize: 64224
[startup+970.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15350 0 0 0 96983 40 0 0 25 0 1 0 481555664 65765376 14677 4294967295 134512640 134672761 3221224576 3221223744 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14677 603 41 0 16015 0
vsize: 64224
[startup+980.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15350 0 0 0 97984 40 0 0 25 0 1 0 481555664 65765376 14677 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14677 603 41 0 16015 0
vsize: 64224
[startup+990.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15350 0 0 0 98984 40 0 0 25 0 1 0 481555664 65765376 14677 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14677 603 41 0 16015 0
vsize: 64224
[startup+1000.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15350 0 0 0 99984 40 0 0 25 0 1 0 481555664 65765376 14677 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14677 603 41 0 16015 0
vsize: 64224
[startup+1010.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15350 0 0 0 100984 40 0 0 25 0 1 0 481555664 65765376 14677 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14677 603 41 0 16015 0
vsize: 64224
[startup+1020.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15350 0 0 0 101985 40 0 0 25 0 1 0 481555664 65765376 14677 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14677 603 41 0 16015 0
vsize: 64224
[startup+1030.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 102985 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223744 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1040.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 103985 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1050.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 104985 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1060.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 105985 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1070.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 106986 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1080.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 107986 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1090.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 108986 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1100.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 109986 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1110.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 110986 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1120.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 111986 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1130.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 112987 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1140.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 113987 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1150.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15370 0 0 0 114987 40 0 0 25 0 1 0 481555664 65765376 14683 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14683 603 41 0 16015 0
vsize: 64224
[startup+1160.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15386 0 0 0 115987 40 0 0 25 0 1 0 481555664 65765376 14685 4294967295 134512640 134672761 3221224576 3221223472 1075352388 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14685 603 41 0 16015 0
vsize: 64224
[startup+1170.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15386 0 0 0 116987 40 0 0 25 0 1 0 481555664 65765376 14685 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14685 603 41 0 16015 0
vsize: 64224
[startup+1180.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15386 0 0 0 117987 40 0 0 25 0 1 0 481555664 65765376 14685 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14685 603 41 0 16015 0
vsize: 64224
[startup+1190.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15386 0 0 0 118988 40 0 0 25 0 1 0 481555664 65765376 14685 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14685 603 41 0 16015 0
vsize: 64224
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25030
Raw data (stat): 25028 (minisat+) R 25027 18865 18864 0 -1 0 15386 0 0 0 119988 40 0 0 25 0 1 0 481555664 65765376 14685 4294967295 134512640 134672761 3221224576 3221223744 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16056 14685 603 41 0 16015 0
vsize: 64224
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25030
Raw data (stat): 25028 (minisat+) Z 25027 18865 18864 0 -1 12 15389 0 0 0 119988 43 0 0 25 0 1 0 481555664 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.18
CPU time (s): 1200.32
CPU user time (s): 1199.88
CPU system time (s): 0.437933
CPU usage (%): 100.012
Max. virtual memory (Kb): 64224
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####