PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-mod008.opb
MD5SUM	581d778a36086562107993896110e0a2
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	307
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	22000
Number of bits of the biggest number in a constraint	15
Biggest sum of numbers in a constraint	1027256
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01784
Number of variables	319
Total number of constraints	325
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	319
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	231
Trace number 21216

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        713928 kB
Buffers:         11764 kB
Cached:         289236 kB
SwapCached:        716 kB
Active:          51004 kB
Inactive:       251908 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        713676 kB
SwapTotal:     2097892 kB
SwapFree:      2096236 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12104 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:27:17 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 13637 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss
c ---[   8]---> Adder-cost: 2481   maxlim: 21999   bits: 16/15
c ---[   5]---> Adder-cost: 2052   maxlim: 4999   bits: 14/13
c ---[   4]---> Adder-cost: 2306   maxlim: 11999   bits: 15/14
c ---[   2]---> BDD-cost:  478
c ---[   1]---> BDD-cost: 2553
c ---[   0]---> Adder-cost: 1803   maxlim: 3999   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   68596   238633 |   22865       0        0     nan |  0.000 % |
c |       100 |   68596   238633 |   25151     100      326     3.3 |  0.272 % |
c |       250 |   68596   238633 |   27666     250      915     3.7 |  0.272 % |
c |       475 |   68596   238633 |   30433     475     2123     4.5 |  0.272 % |
c |       812 |   68596   238633 |   33476     812     4995     6.2 |  0.272 % |
c ==============================================================================
c [1mFound solution: 1517[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:61665     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1253 |  235194   628408 |   78398    1253    10159     8.1 |  0.272 % |
c |      1354 |  235194   628408 |   86237    1354    11162     8.2 |  0.044 % |
c |      1504 |  235194   628408 |   94861    1504    11863     7.9 |  0.044 % |
c |      1729 |  235194   628408 |  104347    1729    14230     8.2 |  0.044 % |
c |      2067 |  235127   628258 |  114782    2066    20060     9.7 |  0.070 % |
c |      2573 |  235127   628258 |  126260    2572    29901    11.6 |  0.070 % |
c |      3335 |  235127   628258 |  138886    3334    44662    13.4 |  0.070 % |
c ==============================================================================
c [1mFound solution: 1470[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3406 |  235231   628558 |   78410    3405    48742    14.3 |  0.070 % |
c |      3507 |  235231   628558 |   86251    3506    55023    15.7 |  0.072 % |
c |      3659 |  235231   628558 |   94876    3658    57801    15.8 |  0.072 % |
c |      3884 |  235231   628558 |  104363    3883    66394    17.1 |  0.072 % |
c |      4221 |  235231   628558 |  114800    4220    69865    16.6 |  0.072 % |
c |      4727 |  235231   628558 |  126280    4726    74886    15.8 |  0.072 % |
c |      5486 |  235231   628558 |  138908    5485   111479    20.3 |  0.072 % |
c |      6625 |  235231   628558 |  152798    6624   131049    19.8 |  0.072 % |
c |      8334 |  235231   628558 |  168078    8333   182419    21.9 |  0.072 % |
c |     10897 |  235037   628121 |  184886   10821   226953    21.0 |  0.150 % |
c |     14742 |  234984   628002 |  203375   14650   321949    22.0 |  0.171 % |
c ==============================================================================
c [1mFound solution: 1421[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14800 |  236638   632044 |   78879   14708   322881    22.0 |  0.171 % |
c ==============================================================================
c [1mFound solution: 1411[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14808 |  236673   632133 |   78891   14716   323513    22.0 |  0.171 % |
c |     14908 |  236673   632133 |   86780   14816   326393    22.0 |  0.178 % |
c |     15058 |  236673   632133 |   95458   14966   327348    21.9 |  0.178 % |
c |     15283 |  236673   632133 |  105003   15191   334592    22.0 |  0.178 % |
c |     15620 |  236673   632133 |  115504   15528   336952    21.7 |  0.178 % |
c |     16127 |  236673   632133 |  127054   16035   345743    21.6 |  0.178 % |
c |     16886 |  236673   632133 |  139760   16794   352761    21.0 |  0.178 % |
c ==============================================================================
c [1mFound solution: 813[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18022 |  238011   635404 |   79337   17928   374201    20.9 |  0.178 % |
c |     18123 |  238011   635404 |   87270   18029   375568    20.8 |  0.195 % |
c |     18273 |  238011   635404 |   95997   18179   376293    20.7 |  0.195 % |
c ==============================================================================
c [1mFound solution: 758[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18358 |  238135   635768 |   79378   18264   378962    20.7 |  0.195 % |
c |     18461 |  238135   635768 |   87315   18367   388402    21.1 |  0.196 % |
c |     18612 |  238135   635768 |   96047   18518   389738    21.0 |  0.196 % |
c |     18837 |  237868   635164 |  105652   18589   390396    21.0 |  0.305 % |
c |     19174 |  237868   635164 |  116217   18926   403668    21.3 |  0.305 % |
c |     19681 |  237868   635164 |  127839   19433   428082    22.0 |  0.305 % |
c |     20440 |  237868   635164 |  140622   20192   444164    22.0 |  0.305 % |
c |     21579 |  237718   634824 |  154685   21316   456037    21.4 |  0.367 % |
c |     23287 |  237052   633288 |  170153   22709   515573    22.7 |  0.665 % |
c |     25849 |  237052   633288 |  187169   25271   584096    23.1 |  0.665 % |
c |     29693 |  236918   632981 |  205886   29076   655020    22.5 |  0.724 % |
c |     35460 |  236918   632981 |  226474   34843   873177    25.1 |  0.724 % |
c ==============================================================================
c [1mFound solution: 757[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38457 |  235980   630848 |   78660   32617   751194    23.0 |  0.724 % |
c |     38557 |  235980   630848 |   86526   32717   754152    23.1 |  1.113 % |
c |     38707 |  235980   630848 |   95178   32867   755104    23.0 |  1.113 % |
c ==============================================================================
c [1mFound solution: 729[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38830 |  236910   633116 |   78970   32990   759135    23.0 |  1.113 % |
c |     38931 |  236910   633116 |   86867   33091   764481    23.1 |  1.116 % |
c |     39082 |  236910   633116 |   95553   33242   777564    23.4 |  1.116 % |
c |     39307 |  236910   633116 |  105109   33467   781053    23.3 |  1.116 % |
c |     39645 |  236910   633116 |  115619   33805   783938    23.2 |  1.116 % |
c |     40151 |  236910   633116 |  127181   34311   798453    23.3 |  1.116 % |
c |     40911 |  236910   633116 |  139900   35071   920527    26.2 |  1.116 % |
c ==============================================================================
c [1mFound solution: 721[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40973 |  236923   633147 |   78974   35133   922581    26.3 |  1.116 % |
c ==============================================================================
c [1mFound solution: 706[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40994 |  237036   633478 |   79012   35154   925670    26.3 |  1.116 % |
c |     41094 |  237036   633478 |   86913   35254   927073    26.3 |  1.119 % |
c ==============================================================================
c [1mFound solution: 394[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41206 |  236703   632712 |   78901   35246   936928    26.6 |  1.119 % |
c |     41307 |  236703   632712 |   86791   35347   948960    26.8 |  1.301 % |
c |     41457 |  236703   632712 |   95470   35497   954142    26.9 |  1.301 % |
c |     41682 |  236563   632392 |  105017   35539   935612    26.3 |  1.361 % |
c |     42020 |  236563   632392 |  115518   35877   952102    26.5 |  1.361 % |
c |     42526 |  236563   632392 |  127070   36383  1037144    28.5 |  1.361 % |
c |     43285 |  236506   632262 |  139777   37123  1198414    32.3 |  1.388 % |
c |     44424 |  236451   632138 |  153755   38251  1259185    32.9 |  1.412 % |
c |     46132 |  236451   632138 |  169131   39959  1669327    41.8 |  1.412 % |
c ==============================================================================
c [1mFound solution: 391[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46615 |  236455   632148 |   78818   40442  1749981    43.3 |  1.412 % |
c |     46717 |  236455   632148 |   86699   40544  1751118    43.2 |  1.414 % |
c |     46867 |  236455   632148 |   95369   40694  1777004    43.7 |  1.414 % |
c |     47092 |  236455   632148 |  104906   40919  1788230    43.7 |  1.414 % |
c |     47431 |  236455   632148 |  115397   41258  1807395    43.8 |  1.414 % |
c |     47938 |  236098   631341 |  126937   41595  1855639    44.6 |  1.561 % |
c ==============================================================================
c [1mFound solution: 377[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48386 |  236102   631351 |   78700   42043  1874232    44.6 |  1.561 % |
c |     48489 |  236102   631351 |   86570   42146  1878873    44.6 |  1.562 % |
c |     48639 |  236102   631351 |   95227   42296  1904623    45.0 |  1.562 % |
c |     48867 |  236102   631351 |  104749   42524  1910447    44.9 |  1.562 % |
c |     49204 |  236102   631351 |  115224   42861  1923403    44.9 |  1.562 % |
c |     49711 |  235935   630972 |  126747   43251  1943275    44.9 |  1.632 % |
c |     50470 |  235452   629866 |  139421   43459  2008220    46.2 |  1.838 % |
c |     51609 |  235359   629652 |  153364   44580  2157437    48.4 |  1.878 % |
c |     53322 |  234924   628650 |  168700   46094  2436752    52.9 |  2.069 % |
c |     55889 |  234924   628650 |  185570   48661  2839037    58.3 |  2.069 % |
c |     59734 |  234924   628650 |  204127   52506  4026295    76.7 |  2.069 % |
c |     65500 |  234924   628650 |  224540   58272  5077047    87.1 |  2.069 % |
c |     74149 |  234924   628650 |  246994   66921  8045875   120.2 |  2.069 % |
c |     87126 |  234700   628132 |  271693   79808 11311469   141.7 |  2.175 % |
c |    106589 |  234700   628132 |  298863   99271 14295709   144.0 |  2.175 % |
c ==============================================================================
c [1mFound solution: 363[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108302 |  234714   628166 |   78238  100984 14665190   145.2 |  2.175 % |
c |    108403 |  234714   628166 |   86061   24142  2246096    93.0 |  2.176 % |
c |    108553 |  234714   628166 |   94667   24292  2275527    93.7 |  2.176 % |
c |    108778 |  232832   623851 |  104134   24350  2293863    94.2 |  3.010 % |
c |    109115 |  232538   623168 |  114548   24650  2334017    94.7 |  3.152 % |
c |    109622 |  232538   623168 |  126003   25157  2379831    94.6 |  3.152 % |
c |    110382 |  232405   622866 |  138603   25901  2466057    95.2 |  3.209 % |
c |    111521 |  231347   620417 |  152463   26974  2551016    94.6 |  3.713 % |
c |    113230 |  231347   620417 |  167710   28683  2931959   102.2 |  3.713 % |
c |    115794 |  231347   620417 |  184481   31247  3653273   116.9 |  3.713 % |
c |    119639 |  231347   620417 |  202929   35092  5234108   149.2 |  3.713 % |
c |    125407 |  231343   620408 |  223222   40859  6583147   161.1 |  3.714 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C2_0x2e__bit0 -C3_0x2e__bit0 -C4_0x2e__bit0 -C5_0x2e__bit0 -C6_0x2e__bit0 -C7_0x2e__bit0 -C8_0x2e__bit0 -C9_0x2e__bit0 -C10_0x2e__bit0 -C11_0x2e__bit0 -C12_0x2e__bit0 -C13_0x2e__bit0 -C14_0x2e__bit0 -C15_0x2e__bit0 -C16_0x2e__bit0 -C17_0x2e__bit0 -C18_0x2e__bit0 -C19_0x2e__bit0 -C20_0x2e__bit0 -C21_0x2e__bit0 -C22_0x2e__bit0 -C23_0x2e__bit0 -C24_0x2e__bit0 -C25_0x2e__bit0 -C26_0x2e__bit0 -C27_0x2e__bit0 -C28_0x2e__bit0 -C29_0x2e__bit0 -C30_0x2e__bit0 -C31_0x2e__bit0 -C32_0x2e__bit0 -C33_0x2e__bit0 -C34_0x2e__bit0 -C35_0x2e__bit0 -C36_0x2e__bit0 -C37_0x2e__bit0 -C38_0x2e__bit0 -C39_0x2e__bit0 -C40_0x2e__bit0 -C41_0x2e__bit0 -C42_0x2e__bit0 -C43_0x2e__bit0 -C44_0x2e__bit0 -C45_0x2e__bit0 -C46_0x2e__bit0 -C47_0x2e__bit0 -C48_0x2e__bit0 -C49_0x2e__bit0 -C50_0x2e__bit0 -C51_0x2e__bit0 -C52_0x2e__bit0 -C53_0x2e__bit0 -C54_0x2e__bit0 -C55_0x2e__bit0 -C56_0x2e__bit0 -C57_0x2e__bit0 -C58_0x2e__bit0 -C59_0x2e__bit0 -C60_0x2e__bit0 -C61_0x2e__bit0 -C62_0x2e__bit0 -C63_0x2e__bit0 -C64_0x2e__bit0 -C65_0x2e__bit0 -C66_0x2e__bit0 -C67_0x2e__bit0 -C68_0x2e__bit0 -C69_0x2e__bit0 -C70_0x2e__bit0 -C71_0x2e__bit0 -C72_0x2e__bit0 C73_0x2e__bit0 -C74_0x2e__bit0 -C75_0x2e__bit0 -C76_0x2e__bit0 -C77_0x2e__bit0 -C78_0x2e__bit0 -C79_0x2e__bit0 -C80_0x2e__bit0 -C81_0x2e__bit0 -C82_0x2e__bit0 -C83_0x2e__bit0 -C84_0x2e__bit0 -C85_0x2e__bit0 -C86_0x2e__bit0 C87_0x2e__bit0 -C88_0x2e__bit0 -C89_0x2e__bit0 -C90_0x2e__bit0 -C91_0x2e__bit0 -C92_0x2e__bit0 -C93_0x2e__bit0 -C94_0x2e__bit0 -C95_0x2e__bit0 -C96_0x2e__bit0 -C97_0x2e__bit0 -C98_0x2e__bit0 -C99_0x2e__bit0 -C100_0x2e__bit0 -C101_0x2e__bit0 -C102_0x2e__bit0 -C103_0x2e__bit0 -C104_0x2e__bit0 -C105_0x2e__bit0 -C106_0x2e__bit0 -C107_0x2e__bit0 -C108_0x2e__bit0 -C109_0x2e__bit0 -C110_0x2e__bit0 -C111_0x2e__bit0 -C112_0x2e__bit0 -C113_0x2e__bit0 -C114_0x2e__bit0 -C115_0x2e__bit0 -C116_0x2e__bit0 -C117_0x2e__bit0 -C118_0x2e__bit0 -C119_0x2e__bit0 C120_0x2e__bit0 -C121_0x2e__bit0 -C122_0x2e__bit0 -C123_0x2e__bit0 -C124_0x2e__bit0 -C125_0x2e__bit0 -C126_0x2e__bit0 -C127_0x2e__bit0 -C128_0x2e__bit0 -C129_0x2e__bit0 -C130_0x2e__bit0 -C131_0x2e__bit0 -C132_0x2e__bit0 -C133_0x2e__bit0 -C134_0x2e__bit0 -C135_0x2e__bit0 -C136_0x2e__bit0 -C137_0x2e__bit0 -C138_0x2e__bit0 -C139_0x2e__bit0 -C140_0x2e__bit0 -C141_0x2e__bit0 -C142_0x2e__bit0 -C143_0x2e__bit0 -C144_0x2e__bit0 -C145_0x2e__bit0 -C146_0x2e__bit0 -C147_0x2e__bit0 -C148_0x2e__bit0 -C149_0x2e__bit0 -C150_0x2e__bit0 -C151_0x2e__bit0 -C152_0x2e__bit0 -C153_0x2e__bit0 -C154_0x2e__bit0 -C155_0x2e__bit0 -C156_0x2e__bit0 -C157_0x2e__bit0 -C158_0x2e__bit0 -C159_0x2e__bit0 -C160_0x2e__bit0 -C161_0x2e__bit0 -C162_0x2e__bit0 -C163_0x2e__bit0 -C164_0x2e__bit0 -C165_0x2e__bit0 -C166_0x2e__bit0 -C167_0x2e__bit0 -C168_0x2e__bit0 -C169_0x2e__bit0 -C170_0x2e__bit0 -C171_0x2e__bit0 -C172_0x2e__bit0 -C173_0x2e__bit0 -C174_0x2e__bit0 -C175_0x2e__bit0 -C176_0x2e__bit0 -C177_0x2e__bit0 -C178_0x2e__bit0 -C179_0x2e__bit0 -C180_0x2e__bit0 -C181_0x2e__bit0 -C182_0x2e__bit0 -C183_0x2e__bit0 -C184_0x2e__bit0 C185_0x2e__bit0 -C186_0x2e__bit0 -C187_0x2e__bit0 -C188_0x2e__bit0 -C189_0x2e__bit0 -C190_0x2e__bit0 -C191_0x2e__bit0 -C192_0x2e__bit0 -C193_0x2e__bit0 -C194_0x2e__bit0 -C195_0x2e__bit0 -C196_0x2e__bit0 -C197_0x2e__bit0 -C198_0x2e__bit0 -C199_0x2e__bit0 -C200_0x2e__bit0 -C201_0x2e__bit0 -C202_0x2e__bit0 -C203_0x2e__bit0 C204_0x2e__bit0 -C205_0x2e__bit0 -C206_0x2e__bit0 -C207_0x2e__bit0 -C208_0x2e__bit0 -C209_0x2e__bit0 -C210_0x2e__bit0 -C211_0x2e__bit0 -C212_0x2e__bit0 -C213_0x2e__bit0 -C214_0x2e__bit0 -C215_0x2e__bit0 -C216_0x2e__bit0 -C217_0x2e__bit0 -C218_0x2e__bit0 -C219_0x2e__bit0 -C220_0x2e__bit0 -C221_0x2e__bit0 -C222_0x2e__bit0 -C223_0x2e__bit0 -C224_0x2e__bit0 -C225_0x2e__bit0 -C226_0x2e__bit0 -C227_0x2e__bit0 -C228_0x2e__bit0 -C229_0x2e__bit0 -C230_0x2e__bit0 -C231_0x2e__bit0 -C232_0x2e__bit0 -C233_0x2e__bit0 -C234_0x2e__bit0 -C235_0x2e__bit0 -C236_0x2e__bit0 -C237_0x2e__bit0 -C238_0x2e__bit0 -C239_0x2e__bit0 -C240_0x2e__bit0 -C241_0x2e__bit0 -C242_0x2e__bit0 -C243_0x2e__bit0 -C244_0x2e__bit0 -C245_0x2e__bit0 -C246_0x2e__bit0 -C#### 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.85 0.97 0.91 2/54 16469
Raw data (stat): 16469 (runsolver) R 16468 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548924955 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0012 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 9637 0 0 0 978 21 0 0 25 0 1 0 548924955 26656768 5894 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6508 5894 603 41 0 6467 0
vsize: 26032
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 9902 0 0 0 1977 22 0 0 25 0 1 0 548924955 27406336 6117 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6691 6117 603 41 0 6650 0
vsize: 26764
[startup+30.0018 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 9902 0 0 0 2977 22 0 0 25 0 1 0 548924955 27406336 6117 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6691 6117 603 41 0 6650 0
vsize: 26764
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 9963 0 0 0 3976 23 0 0 25 0 1 0 548924955 27676672 6178 4294967295 134512640 134672761 3221224544 3221223728 134559166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6757 6178 603 41 0 6716 0
vsize: 27028
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10013 0 0 0 4976 23 0 0 25 0 1 0 548924955 27947008 6228 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6823 6228 603 41 0 6782 0
vsize: 27292
[startup+60.0026 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10057 0 0 0 5975 24 0 0 25 0 1 0 548924955 28078080 6272 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6855 6272 603 41 0 6814 0
vsize: 27420
[startup+70.0037 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10134 0 0 0 6975 24 0 0 25 0 1 0 548924955 28348416 6349 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6921 6349 603 41 0 6880 0
vsize: 27684
[startup+80.0043 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10348 0 0 0 7974 25 0 0 25 0 1 0 548924955 33046528 6540 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8068 6540 603 41 0 8027 0
vsize: 32272
[startup+90.0045 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10392 0 0 0 8974 26 0 0 25 0 1 0 548924955 33046528 6542 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8068 6542 603 41 0 8027 0
vsize: 32272
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10538 0 0 0 9973 26 0 0 25 0 1 0 548924955 33099776 6595 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8081 6595 603 41 0 8040 0
vsize: 32324
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10580 0 0 0 10973 26 0 0 25 0 1 0 548924955 33370112 6637 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8147 6637 603 41 0 8106 0
vsize: 32588
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10633 0 0 0 11973 26 0 0 25 0 1 0 548924955 33505280 6690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8180 6690 603 41 0 8139 0
vsize: 32720
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10719 0 0 0 12973 27 0 0 25 0 1 0 548924955 33910784 6776 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8279 6776 603 41 0 8238 0
vsize: 33116
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10776 0 0 0 13972 28 0 0 25 0 1 0 548924955 34177024 6833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8344 6833 603 41 0 8303 0
vsize: 33376
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10838 0 0 0 14972 28 0 0 25 0 1 0 548924955 34443264 6895 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8409 6895 603 41 0 8368 0
vsize: 33636
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10891 0 0 0 15971 29 0 0 25 0 1 0 548924955 34578432 6948 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8442 6948 603 41 0 8401 0
vsize: 33768
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 10952 0 0 0 16971 29 0 0 25 0 1 0 548924955 34844672 7009 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8507 7009 603 41 0 8466 0
vsize: 34028
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11012 0 0 0 17970 30 0 0 25 0 1 0 548924955 35237888 7069 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8603 7069 603 41 0 8562 0
vsize: 34412
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11057 0 0 0 18970 30 0 0 25 0 1 0 548924955 35373056 7114 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 7114 603 41 0 8595 0
vsize: 34544
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11128 0 0 0 19970 31 0 0 25 0 1 0 548924955 35643392 7185 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8702 7185 603 41 0 8661 0
vsize: 34808
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11161 0 0 0 20970 31 0 0 25 0 1 0 548924955 35778560 7218 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8735 7218 603 41 0 8694 0
vsize: 34940
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11209 0 0 0 21969 31 0 0 25 0 1 0 548924955 36048896 7266 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8801 7266 603 41 0 8760 0
vsize: 35204
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11245 0 0 0 22969 32 0 0 25 0 1 0 548924955 36184064 7302 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8834 7302 603 41 0 8793 0
vsize: 35336
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11288 0 0 0 23968 32 0 0 25 0 1 0 548924955 36405248 7345 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8888 7345 603 41 0 8847 0
vsize: 35552
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11370 0 0 0 24968 33 0 0 25 0 1 0 548924955 36405248 7379 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8888 7379 603 41 0 8847 0
vsize: 35552
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11370 0 0 0 25968 33 0 0 25 0 1 0 548924955 36405248 7379 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8888 7379 603 41 0 8847 0
vsize: 35552
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11370 0 0 0 26968 33 0 0 25 0 1 0 548924955 36405248 7379 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8888 7379 603 41 0 8847 0
vsize: 35552
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11491 0 0 0 27967 34 0 0 25 0 1 0 548924955 36421632 7383 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8892 7383 603 41 0 8851 0
vsize: 35568
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11502 0 0 0 28967 34 0 0 25 0 1 0 548924955 36552704 7394 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8924 7394 603 41 0 8883 0
vsize: 35696
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11683 0 0 0 29967 35 0 0 25 0 1 0 548924955 37208064 7575 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9084 7575 603 41 0 9043 0
vsize: 36336
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 11741 0 0 0 30966 35 0 0 25 0 1 0 548924955 37478400 7633 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9150 7633 603 41 0 9109 0
vsize: 36600
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 12162 0 0 0 31965 37 0 0 25 0 1 0 548924955 39227392 8054 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9577 8054 603 41 0 9536 0
vsize: 38308
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 12322 0 0 0 32964 38 0 0 25 0 1 0 548924955 39788544 8190 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9714 8190 603 41 0 9673 0
vsize: 38856
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 12401 0 0 0 33963 39 0 0 25 0 1 0 548924955 40058880 8269 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9780 8269 603 41 0 9739 0
vsize: 39120
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 12497 0 0 0 34963 40 0 0 25 0 1 0 548924955 40345600 8340 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9850 8340 603 41 0 9809 0
vsize: 39400
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 12526 0 0 0 35963 40 0 0 25 0 1 0 548924955 40476672 8369 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9882 8369 603 41 0 9841 0
vsize: 39528
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 12643 0 0 0 36962 40 0 0 25 0 1 0 548924955 41013248 8486 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10013 8486 603 41 0 9972 0
vsize: 40052
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 12804 0 0 0 37962 41 0 0 25 0 1 0 548924955 41676800 8647 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 8647 603 41 0 10134 0
vsize: 40700
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 13073 0 0 0 38961 42 0 0 25 0 1 0 548924955 42741760 8916 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10435 8916 603 41 0 10394 0
vsize: 41740
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 13151 0 0 0 39960 43 0 0 25 0 1 0 548924955 43134976 8994 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10531 8994 603 41 0 10490 0
vsize: 42124
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 13297 0 0 0 40959 44 0 0 25 0 1 0 548924955 43794432 9140 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10692 9140 603 41 0 10651 0
vsize: 42768
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 13442 0 0 0 41958 45 0 0 25 0 1 0 548924955 44335104 9285 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10824 9285 603 41 0 10783 0
vsize: 43296
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 13636 0 0 0 42957 46 0 0 25 0 1 0 548924955 45133824 9479 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11019 9479 603 41 0 10978 0
vsize: 44076
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 14015 0 0 0 43956 47 0 0 25 0 1 0 548924955 46616576 9858 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11381 9858 603 41 0 11340 0
vsize: 45524
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 14544 0 0 0 44955 48 0 0 25 0 1 0 548924955 48869376 10387 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11931 10387 603 41 0 11890 0
vsize: 47724
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 14823 0 0 0 45954 49 0 0 25 0 1 0 548924955 49942528 10666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12193 10666 603 41 0 12152 0
vsize: 48772
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 14953 0 0 0 46954 50 0 0 25 0 1 0 548924955 50470912 10796 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12322 10796 603 41 0 12281 0
vsize: 49288
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 15068 0 0 0 47954 50 0 0 25 0 1 0 548924955 50999296 10911 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12451 10911 603 41 0 12410 0
vsize: 49804
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 15189 0 0 0 48953 51 0 0 25 0 1 0 548924955 51404800 11032 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12550 11032 603 41 0 12509 0
vsize: 50200
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 15277 0 0 0 49953 51 0 0 25 0 1 0 548924955 51793920 11120 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12645 11120 603 41 0 12604 0
vsize: 50580
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 15302 0 0 0 50953 52 0 0 25 0 1 0 548924955 51916800 11145 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12675 11145 603 41 0 12634 0
vsize: 50700
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 15346 0 0 0 51952 52 0 0 25 0 1 0 548924955 52043776 11189 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12706 11189 603 41 0 12665 0
vsize: 50824
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 15378 0 0 0 52952 52 0 0 25 0 1 0 548924955 52174848 11221 4294967295 134512640 134672761 3221224544 3221223728 134559159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12738 11221 603 41 0 12697 0
vsize: 50952
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 15503 0 0 0 53952 53 0 0 25 0 1 0 548924955 52699136 11346 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12866 11346 603 41 0 12825 0
vsize: 51464
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 15694 0 0 0 54951 54 0 0 25 0 1 0 548924955 53493760 11537 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13060 11537 603 41 0 13019 0
vsize: 52240
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 15827 0 0 0 55950 54 0 0 25 0 1 0 548924955 54034432 11670 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13192 11670 603 41 0 13151 0
vsize: 52768
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 16126 0 0 0 56950 55 0 0 25 0 1 0 548924955 55230464 11969 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13484 11969 603 41 0 13443 0
vsize: 53936
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 16532 0 0 0 57948 56 0 0 25 0 1 0 548924955 56963072 12375 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13907 12375 603 41 0 13866 0
vsize: 55628
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 16888 0 0 0 58948 57 0 0 25 0 1 0 548924955 58404864 12731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14259 12731 603 41 0 14218 0
vsize: 57036
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 17366 0 0 0 59946 59 0 0 25 0 1 0 548924955 60276736 13209 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14716 13209 603 41 0 14675 0
vsize: 58864
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 17784 0 0 0 60945 60 0 0 25 0 1 0 548924955 61997056 13627 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15136 13627 603 41 0 15095 0
vsize: 60544
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 17981 0 0 0 61945 61 0 0 25 0 1 0 548924955 62795776 13824 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15331 13824 603 41 0 15290 0
vsize: 61324
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 18078 0 0 0 62944 61 0 0 25 0 1 0 548924955 63193088 13921 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15428 13921 603 41 0 15387 0
vsize: 61712
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 18317 0 0 0 63944 62 0 0 25 0 1 0 548924955 64258048 14160 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15688 14160 603 41 0 15647 0
vsize: 62752
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 18554 0 0 0 64942 63 0 0 25 0 1 0 548924955 65449984 14397 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15979 14397 603 41 0 15938 0
vsize: 63916
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 18661 0 0 0 65942 64 0 0 25 0 1 0 548924955 65851392 14504 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16077 14504 603 41 0 16036 0
vsize: 64308
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 18769 0 0 0 66942 65 0 0 25 0 1 0 548924955 66375680 14612 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 14612 603 41 0 16164 0
vsize: 64820
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 18972 0 0 0 67941 65 0 0 25 0 1 0 548924955 67174400 14815 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16400 14815 603 41 0 16359 0
vsize: 65600
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 19052 0 0 0 68940 66 0 0 25 0 1 0 548924955 67440640 14895 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16465 14895 603 41 0 16424 0
vsize: 65860
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 19124 0 0 0 69940 66 0 0 25 0 1 0 548924955 67710976 14967 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16531 14967 603 41 0 16490 0
vsize: 66124
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 19198 0 0 0 70939 67 0 0 25 0 1 0 548924955 68108288 15041 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16628 15041 603 41 0 16587 0
vsize: 66512
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 19279 0 0 0 71939 68 0 0 25 0 1 0 548924955 68366336 15122 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16691 15122 603 41 0 16650 0
vsize: 66764
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 19431 0 0 0 72938 68 0 0 25 0 1 0 548924955 69038080 15274 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16855 15274 603 41 0 16814 0
vsize: 67420
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 19678 0 0 0 73938 69 0 0 25 0 1 0 548924955 69984256 15521 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17086 15521 603 41 0 17045 0
vsize: 68344
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 20026 0 0 0 74936 71 0 0 25 0 1 0 548924955 71446528 15869 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17443 15869 603 41 0 17402 0
vsize: 69772
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 20388 0 0 0 75935 72 0 0 25 0 1 0 548924955 72904704 16231 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17799 16231 603 41 0 17758 0
vsize: 71196
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 20612 0 0 0 76935 73 0 0 25 0 1 0 548924955 73830400 16455 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18025 16455 603 41 0 17984 0
vsize: 72100
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 20893 0 0 0 77934 74 0 0 25 0 1 0 548924955 75014144 16736 4294967295 134512640 134672761 3221224544 3221223648 134559985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18314 16736 603 41 0 18273 0
vsize: 73256
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 21235 0 0 0 78932 75 0 0 25 0 1 0 548924955 76341248 17078 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18638 17078 603 41 0 18597 0
vsize: 74552
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 21343 0 0 0 79932 76 0 0 25 0 1 0 548924955 76881920 17186 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18770 17186 603 41 0 18729 0
vsize: 75080
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 21613 0 0 0 80931 77 0 0 25 0 1 0 548924955 77938688 17456 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19028 17456 603 41 0 18987 0
vsize: 76112
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 22021 0 0 0 81929 79 0 0 25 0 1 0 548924955 79544320 17864 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19420 17864 603 41 0 19379 0
vsize: 77680
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 22296 0 0 0 82928 80 0 0 25 0 1 0 548924955 80748544 18139 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19714 18139 603 41 0 19673 0
vsize: 78856
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 22593 0 0 0 83927 81 0 0 25 0 1 0 548924955 81952768 18436 4294967295 134512640 134672761 3221224544 3221223680 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20008 18436 603 41 0 19967 0
vsize: 80032
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 22807 0 0 0 84926 82 0 0 25 0 1 0 548924955 82763776 18650 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20206 18650 603 41 0 20165 0
vsize: 80824
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 22913 0 0 0 85926 83 0 0 25 0 1 0 548924955 83161088 18756 4294967295 134512640 134672761 3221224544 3221223728 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20303 18756 603 41 0 20262 0
vsize: 81212
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 23064 0 0 0 86925 83 0 0 25 0 1 0 548924955 83832832 18907 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20467 18907 603 41 0 20426 0
vsize: 81868
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 23392 0 0 0 87924 85 0 0 25 0 1 0 548924955 85151744 19235 4294967295 134512640 134672761 3221224544 3221223728 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20789 19235 603 41 0 20748 0
vsize: 83156
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 23696 0 0 0 88922 86 0 0 25 0 1 0 548924955 86478848 19539 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 19539 603 41 0 21072 0
vsize: 84452
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 24007 0 0 0 89921 88 0 0 25 0 1 0 548924955 87666688 19850 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21403 19850 603 41 0 21362 0
vsize: 85612
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 24296 0 0 0 90920 89 0 0 25 0 1 0 548924955 88883200 20139 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21700 20139 603 41 0 21659 0
vsize: 86800
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 24555 0 0 0 91919 90 0 0 25 0 1 0 548924955 89952256 20398 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21961 20398 603 41 0 21920 0
vsize: 87844
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 24778 0 0 0 92918 91 0 0 25 0 1 0 548924955 90882048 20621 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22188 20621 603 41 0 22147 0
vsize: 88752
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25014 0 0 0 93917 92 0 0 25 0 1 0 548924955 91844608 20857 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22423 20857 603 41 0 22382 0
vsize: 89692
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25253 0 0 0 94916 94 0 0 25 0 1 0 548924955 92770304 21096 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22649 21096 603 41 0 22608 0
vsize: 90596
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25422 0 0 0 95915 95 0 0 25 0 1 0 548924955 93429760 21265 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22810 21265 603 41 0 22769 0
vsize: 91240
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 96914 96 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221222048 134523047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+980.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 97913 97 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+990.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 98913 97 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 99913 97 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 100913 98 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 101913 98 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 102912 98 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223728 134558702 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 103912 99 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 104912 99 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 105911 100 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 106911 100 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 107911 100 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 108911 100 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 109911 101 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 110910 101 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 111910 101 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 112910 102 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 113910 102 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 114910 102 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 115909 103 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 116909 103 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 117909 103 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 118909 104 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16469
Raw data (stat): 16469 (minisat+) R 16468 28099 28098 0 -1 0 25854 0 0 0 119909 104 0 0 25 0 1 0 548924955 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 16469
Raw data (stat): 16469 (minisat+) Z 16468 28099 28098 0 -1 12 25857 0 0 0 119909 108 0 0 25 0 1 0 548924955 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.08
CPU time (s): 1200.18
CPU user time (s): 1199.1
CPU system time (s): 1.08283
CPU usage (%): 100.008
Max. virtual memory (Kb): 92672
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####