PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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.02084
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 15051

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-21 02:43:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18629 boxname=wulflinc17 idbench=1433 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  581d778a36086562107993896110e0a2  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-mod008.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-mod008.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-mod008.opb
IDLAUNCH: 18629
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        808780 kB
Buffers:         20172 kB
Cached:         175380 kB
SwapCached:         84 kB
Active:          21908 kB
Inactive:       176684 kB
HighTotal:      131008 kB
HighFree:        52864 kB
LowTotal:       903652 kB
LowFree:        755916 kB
SwapTotal:     2097892 kB
SwapFree:      2097776 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6628 kB
Slab:            21500 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:03:54 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 18629 7 1200.2 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.92 0.95 0.94 2/55 21280
Raw data (stat): 21280 (runsolver) R 21279 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541581213 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.96 0.94 2/55 21280
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 9635 0 0 0 975 23 0 0 25 0 1 0 541581213 26656768 5892 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6508 5892 603 41 0 6467 0
vsize: 26032
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.96 0.94 2/55 21280
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 9902 0 0 0 1972 25 0 0 25 0 1 0 541581213 27406336 6117 4294967295 134512640 134672761 3221224544 3221223680 134565045 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.0016 s]
Raw data (loadavg): 0.95 0.96 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 9902 0 0 0 2973 25 0 0 25 0 1 0 541581213 27406336 6117 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.0015 s]
Raw data (loadavg): 0.96 0.96 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 9961 0 0 0 3972 25 0 0 25 0 1 0 541581213 27676672 6176 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6757 6176 603 41 0 6716 0
vsize: 27028
[startup+50.0007 s]
Raw data (loadavg): 0.96 0.96 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10010 0 0 0 4972 26 0 0 25 0 1 0 541581213 27947008 6225 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6823 6225 603 41 0 6782 0
vsize: 27292
[startup+60.0004 s]
Raw data (loadavg): 0.97 0.96 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10054 0 0 0 5971 26 0 0 25 0 1 0 541581213 28078080 6269 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6855 6269 603 41 0 6814 0
vsize: 27420
[startup+70.0002 s]
Raw data (loadavg): 0.97 0.96 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10121 0 0 0 6971 26 0 0 25 0 1 0 541581213 28348416 6336 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6921 6336 603 41 0 6880 0
vsize: 27684
[startup+80.0006 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10181 0 0 0 7971 27 0 0 25 0 1 0 541581213 28618752 6396 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6987 6396 603 41 0 6946 0
vsize: 27948
[startup+90.0002 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10392 0 0 0 8971 27 0 0 25 0 1 0 541581213 33046528 6542 4294967295 134512640 134672761 3221224544 3221223680 134560642 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 s]
Raw data (loadavg): 0.98 0.96 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10538 0 0 0 9970 28 0 0 25 0 1 0 541581213 33099776 6595 4294967295 134512640 134672761 3221224544 3221223712 134561269 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.001 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10574 0 0 0 10970 28 0 0 25 0 1 0 541581213 33370112 6631 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8147 6631 603 41 0 8106 0
vsize: 32588
[startup+120.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10624 0 0 0 11969 28 0 0 25 0 1 0 541581213 33505280 6681 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8180 6681 603 41 0 8139 0
vsize: 32720
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10704 0 0 0 12969 28 0 0 25 0 1 0 541581213 33910784 6761 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8279 6761 603 41 0 8238 0
vsize: 33116
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10768 0 0 0 13969 29 0 0 25 0 1 0 541581213 34045952 6825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8312 6825 603 41 0 8271 0
vsize: 33248
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10827 0 0 0 14969 29 0 0 25 0 1 0 541581213 34308096 6884 4294967295 134512640 134672761 3221224544 3221223728 134558513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8376 6884 603 41 0 8335 0
vsize: 33504
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10888 0 0 0 15968 30 0 0 25 0 1 0 541581213 34578432 6945 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8442 6945 603 41 0 8401 0
vsize: 33768
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 10938 0 0 0 16968 30 0 0 25 0 1 0 541581213 34844672 6995 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8507 6995 603 41 0 8466 0
vsize: 34028
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11012 0 0 0 17968 30 0 0 25 0 1 0 541581213 35237888 7069 4294967295 134512640 134672761 3221224544 3221223744 134557828 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.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11041 0 0 0 18968 30 0 0 25 0 1 0 541581213 35373056 7098 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 7098 603 41 0 8595 0
vsize: 34544
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11123 0 0 0 19968 31 0 0 25 0 1 0 541581213 35643392 7180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8702 7180 603 41 0 8661 0
vsize: 34808
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11151 0 0 0 20968 31 0 0 25 0 1 0 541581213 35778560 7208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8735 7208 603 41 0 8694 0
vsize: 34940
[startup+219.999 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11194 0 0 0 21968 31 0 0 25 0 1 0 541581213 35913728 7251 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8768 7251 603 41 0 8727 0
vsize: 35072
[startup+230 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11239 0 0 0 22968 31 0 0 25 0 1 0 541581213 36184064 7296 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8834 7296 603 41 0 8793 0
vsize: 35336
[startup+239.999 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11288 0 0 0 23968 31 0 0 25 0 1 0 541581213 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+249.999 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11370 0 0 0 24968 32 0 0 25 0 1 0 541581213 36405248 7379 4294967295 134512640 134672761 3221224544 3221223712 134560869 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 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11370 0 0 0 25968 32 0 0 25 0 1 0 541581213 36405248 7379 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8888 7379 603 41 0 8847 0
vsize: 35552
[startup+269.999 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11370 0 0 0 26968 32 0 0 25 0 1 0 541581213 36405248 7379 4294967295 134512640 134672761 3221224544 3221223700 134561032 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 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11491 0 0 0 27968 32 0 0 25 0 1 0 541581213 36421632 7383 4294967295 134512640 134672761 3221224544 3221223680 134560577 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.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11491 0 0 0 28968 32 0 0 25 0 1 0 541581213 36421632 7383 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8892 7383 603 41 0 8851 0
vsize: 35568
[startup+300 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11611 0 0 0 29969 32 0 0 25 0 1 0 541581213 36950016 7503 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9021 7503 603 41 0 8980 0
vsize: 36084
[startup+310 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 11715 0 0 0 30968 33 0 0 25 0 1 0 541581213 37343232 7607 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9117 7607 603 41 0 9076 0
vsize: 36468
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21282
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 12055 0 0 0 31968 33 0 0 25 0 1 0 541581213 38825984 7947 4294967295 134512640 134672761 3221224544 3221223648 134560039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 7947 603 41 0 9438 0
vsize: 37916
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 12312 0 0 0 32967 34 0 0 25 0 1 0 541581213 39657472 8180 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9682 8180 603 41 0 9641 0
vsize: 38728
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 12344 0 0 0 33967 34 0 0 25 0 1 0 541581213 39788544 8212 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9714 8212 603 41 0 9673 0
vsize: 38856
[startup+350 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 12480 0 0 0 34967 35 0 0 25 0 1 0 541581213 40345600 8323 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9850 8323 603 41 0 9809 0
vsize: 39400
[startup+360.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 12519 0 0 0 35967 35 0 0 25 0 1 0 541581213 40476672 8362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9882 8362 603 41 0 9841 0
vsize: 39528
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 12614 0 0 0 36967 35 0 0 25 0 1 0 541581213 40882176 8457 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9981 8457 603 41 0 9940 0
vsize: 39924
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 12748 0 0 0 37967 35 0 0 25 0 1 0 541581213 41406464 8591 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10109 8591 603 41 0 10068 0
vsize: 40436
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 12983 0 0 0 38967 36 0 0 25 0 1 0 541581213 42336256 8826 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10336 8826 603 41 0 10295 0
vsize: 41344
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 13151 0 0 0 39967 36 0 0 25 0 1 0 541581213 43134976 8994 4294967295 134512640 134672761 3221224544 3221223728 134559498 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.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 13243 0 0 0 40966 36 0 0 25 0 1 0 541581213 43524096 9086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 9086 603 41 0 10585 0
vsize: 42504
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 13386 0 0 0 41966 37 0 0 25 0 1 0 541581213 44064768 9229 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10758 9229 603 41 0 10717 0
vsize: 43032
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 13515 0 0 0 42966 37 0 0 25 0 1 0 541581213 44597248 9358 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10888 9358 603 41 0 10847 0
vsize: 43552
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 13875 0 0 0 43965 38 0 0 25 0 1 0 541581213 46084096 9718 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11251 9718 603 41 0 11210 0
vsize: 45004
[startup+450.001 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 14352 0 0 0 44964 40 0 0 25 0 1 0 541581213 48074752 10195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11737 10195 603 41 0 11696 0
vsize: 46948
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 14676 0 0 0 45963 41 0 0 25 0 1 0 541581213 49401856 10519 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12061 10519 603 41 0 12020 0
vsize: 48244
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 14905 0 0 0 46963 41 0 0 25 0 1 0 541581213 50335744 10748 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12289 10748 603 41 0 12248 0
vsize: 49156
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 15023 0 0 0 47963 41 0 0 25 0 1 0 541581213 50733056 10866 4294967295 134512640 134672761 3221224544 3221223648 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12386 10866 603 41 0 12345 0
vsize: 49544
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 15139 0 0 0 48962 42 0 0 25 0 1 0 541581213 51277824 10982 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12519 10982 603 41 0 12478 0
vsize: 50076
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 15253 0 0 0 49962 42 0 0 25 0 1 0 541581213 51671040 11096 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12615 11096 603 41 0 12574 0
vsize: 50460
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 15284 0 0 0 50962 42 0 0 25 0 1 0 541581213 51793920 11127 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12645 11127 603 41 0 12604 0
vsize: 50580
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 15333 0 0 0 51962 42 0 0 25 0 1 0 541581213 52043776 11176 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12706 11176 603 41 0 12665 0
vsize: 50824
[startup+530.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 15358 0 0 0 52963 42 0 0 25 0 1 0 541581213 52174848 11201 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12738 11201 603 41 0 12697 0
vsize: 50952
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 15427 0 0 0 53962 43 0 0 25 0 1 0 541581213 52432896 11270 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12801 11270 603 41 0 12760 0
vsize: 51204
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 15650 0 0 0 54962 43 0 0 25 0 1 0 541581213 53362688 11493 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13028 11493 603 41 0 12987 0
vsize: 52112
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 15765 0 0 0 55962 44 0 0 25 0 1 0 541581213 53764096 11608 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13126 11608 603 41 0 13085 0
vsize: 52504
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 16031 0 0 0 56961 45 0 0 25 0 1 0 541581213 54829056 11874 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13386 11874 603 41 0 13345 0
vsize: 53544
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 16390 0 0 0 57960 46 0 0 25 0 1 0 541581213 56303616 12233 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13746 12233 603 41 0 13705 0
vsize: 54984
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 16763 0 0 0 58959 47 0 0 25 0 1 0 541581213 57884672 12606 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14132 12606 603 41 0 14091 0
vsize: 56528
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 17134 0 0 0 59958 48 0 0 25 0 1 0 541581213 59346944 12977 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14489 12977 603 41 0 14448 0
vsize: 57956
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 17626 0 0 0 60957 49 0 0 25 0 1 0 541581213 61333504 13469 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14974 13469 603 41 0 14933 0
vsize: 59896
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21284
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 17931 0 0 0 61957 50 0 0 25 0 1 0 541581213 62660608 13774 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15298 13774 603 41 0 15257 0
vsize: 61192
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 18055 0 0 0 62956 50 0 0 25 0 1 0 541581213 63193088 13898 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15428 13898 603 41 0 15387 0
vsize: 61712
[startup+640.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 18229 0 0 0 63955 51 0 0 25 0 1 0 541581213 63860736 14072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15591 14072 603 41 0 15550 0
vsize: 62364
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 18434 0 0 0 64955 52 0 0 25 0 1 0 541581213 64659456 14277 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15786 14277 603 41 0 15745 0
vsize: 63144
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 18627 0 0 0 65955 52 0 0 25 0 1 0 541581213 65716224 14470 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16044 14470 603 41 0 16003 0
vsize: 64176
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 18718 0 0 0 66954 52 0 0 25 0 1 0 541581213 66113536 14561 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16141 14561 603 41 0 16100 0
vsize: 64564
[startup+680.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 18897 0 0 0 67954 53 0 0 25 0 1 0 541581213 66908160 14740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16335 14740 603 41 0 16294 0
vsize: 65340
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 19032 0 0 0 68954 53 0 0 25 0 1 0 541581213 67440640 14875 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16465 14875 603 41 0 16424 0
vsize: 65860
[startup+700.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 19091 0 0 0 69954 53 0 0 25 0 1 0 541581213 67575808 14934 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16498 14934 603 41 0 16457 0
vsize: 65992
[startup+710.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 19168 0 0 0 70954 54 0 0 25 0 1 0 541581213 67981312 15011 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16597 15011 603 41 0 16556 0
vsize: 66388
[startup+720.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 19247 0 0 0 71954 54 0 0 25 0 1 0 541581213 68239360 15090 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16660 15090 603 41 0 16619 0
vsize: 66640
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 19333 0 0 0 72954 54 0 0 25 0 1 0 541581213 68632576 15176 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16756 15176 603 41 0 16715 0
vsize: 67024
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 19558 0 0 0 73953 55 0 0 25 0 1 0 541581213 69578752 15401 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16987 15401 603 41 0 16946 0
vsize: 67948
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 19903 0 0 0 74953 56 0 0 25 0 1 0 541581213 70922240 15746 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17315 15746 603 41 0 17274 0
vsize: 69260
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 20252 0 0 0 75952 56 0 0 25 0 1 0 541581213 72364032 16095 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17667 16095 603 41 0 17626 0
vsize: 70668
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 20547 0 0 0 76952 56 0 0 25 0 1 0 541581213 73560064 16390 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17959 16390 603 41 0 17918 0
vsize: 71836
[startup+780.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 20737 0 0 0 77952 57 0 0 25 0 1 0 541581213 74371072 16580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18157 16580 603 41 0 18116 0
vsize: 72628
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 21104 0 0 0 78951 58 0 0 25 0 1 0 541581213 75800576 16947 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18506 16947 603 41 0 18465 0
vsize: 74024
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 21325 0 0 0 79951 59 0 0 25 0 1 0 541581213 76746752 17168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18737 17168 603 41 0 18696 0
vsize: 74948
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 21474 0 0 0 80951 60 0 0 25 0 1 0 541581213 77406208 17317 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18898 17317 603 41 0 18857 0
vsize: 75592
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 21847 0 0 0 81951 60 0 0 25 0 1 0 541581213 78884864 17690 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19259 17690 603 41 0 19218 0
vsize: 77036
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 22194 0 0 0 82950 61 0 0 25 0 1 0 541581213 80347136 18037 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19616 18037 603 41 0 19575 0
vsize: 78464
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 22485 0 0 0 83948 62 0 0 25 0 1 0 541581213 81551360 18328 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19910 18328 603 41 0 19869 0
vsize: 79640
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 22703 0 0 0 84947 63 0 0 25 0 1 0 541581213 82358272 18546 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20107 18546 603 41 0 20066 0
vsize: 80428
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 22873 0 0 0 85946 64 0 0 25 0 1 0 541581213 83025920 18716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20270 18716 603 41 0 20229 0
vsize: 81080
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 22978 0 0 0 86946 64 0 0 25 0 1 0 541581213 83427328 18821 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 18821 603 41 0 20327 0
vsize: 81472
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 23269 0 0 0 87946 65 0 0 25 0 1 0 541581213 84623360 19112 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20660 19112 603 41 0 20619 0
vsize: 82640
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 23582 0 0 0 88945 65 0 0 25 0 1 0 541581213 85950464 19425 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20984 19425 603 41 0 20943 0
vsize: 83936
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 23886 0 0 0 89944 66 0 0 25 0 1 0 541581213 87138304 19729 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21274 19729 603 41 0 21233 0
vsize: 85096
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 24193 0 0 0 90943 68 0 0 25 0 1 0 541581213 88485888 20036 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21603 20036 603 41 0 21562 0
vsize: 86412
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21286
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 24464 0 0 0 91943 68 0 0 25 0 1 0 541581213 89550848 20307 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21863 20307 603 41 0 21822 0
vsize: 87452
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21288
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 24703 0 0 0 92942 70 0 0 25 0 1 0 541581213 90488832 20546 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22092 20546 603 41 0 22051 0
vsize: 88368
[startup+940.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21288
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 24909 0 0 0 93941 71 0 0 25 0 1 0 541581213 91443200 20752 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22325 20752 603 41 0 22284 0
vsize: 89300
[startup+950.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21288
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25173 0 0 0 94941 71 0 0 25 0 1 0 541581213 92508160 21016 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22585 21016 603 41 0 22544 0
vsize: 90340
[startup+960.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21288
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25391 0 0 0 95940 72 0 0 25 0 1 0 541581213 93298688 21234 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22778 21234 603 41 0 22737 0
vsize: 91112
[startup+970.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 21288
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25624 0 0 0 96940 72 0 0 25 0 1 0 541581213 94371840 21467 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23040 21467 603 41 0 22999 0
vsize: 92160
[startup+980.017 s]
Raw data (loadavg): 1.07 0.99 0.94 2/55 21341
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 97939 73 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223716 134556667 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.016 s]
Raw data (loadavg): 1.06 0.99 0.94 2/55 21341
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 98939 73 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560291 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.02 s]
Raw data (loadavg): 1.05 0.99 0.94 2/55 21341
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 99939 73 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.02 s]
Raw data (loadavg): 1.04 0.99 0.94 2/55 21341
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 100939 73 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223680 134560622 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.02 s]
Raw data (loadavg): 1.03 0.99 0.94 2/55 21341
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 101939 73 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560855 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.02 s]
Raw data (loadavg): 1.03 0.99 0.94 2/55 21341
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 102940 73 0 0 25 0 1 0 541581213 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+1040.02 s]
Raw data (loadavg): 1.02 0.99 0.94 2/55 21341
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 103940 73 0 0 25 0 1 0 541581213 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+1050.02 s]
Raw data (loadavg): 1.02 0.99 0.94 2/55 21341
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 104940 73 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223728 134558930 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.02 s]
Raw data (loadavg): 1.02 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 105940 73 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223560 1075353072 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.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 106940 73 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134559872 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.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 107940 73 0 0 25 0 1 0 541581213 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+1090.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 108940 73 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.02 s]
Raw data (loadavg): 1.01 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 109940 73 0 0 25 0 1 0 541581213 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+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 110940 73 0 0 25 0 1 0 541581213 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+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 111940 74 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134559949 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.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 112940 74 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560031 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.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 113940 74 0 0 25 0 1 0 541581213 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+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 114941 74 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223680 134560577 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.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 115941 74 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134561188 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.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 116941 74 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560822 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.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 117941 74 0 0 25 0 1 0 541581213 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560418 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.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 118941 74 0 0 25 0 1 0 541581213 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+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/55 21343
Raw data (stat): 21280 (minisat+) R 21279 20838 20837 0 -1 0 25854 0 0 0 119942 74 0 0 25 0 1 0 541581213 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.94 1/55 21343
Raw data (stat): 21280 (minisat+) Z 21279 20838 20837 0 -1 12 25857 0 0 0 119942 78 0 0 25 0 1 0 541581213 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.2
CPU user time (s): 1199.42
CPU system time (s): 0.780881
CPU usage (%): 100.012
Max. virtual memory (Kb): 92672
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####