PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod008.opb
MD5SUM	fbdb3cf321a85412feefcaac30780520
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.01584
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 17035

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        647640 kB
Buffers:          9216 kB
Cached:         351760 kB
SwapCached:        512 kB
Active:          47436 kB
Inactive:       315508 kB
HighTotal:      131008 kB
HighFree:         4004 kB
LowTotal:       903652 kB
LowFree:        643636 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            18364 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 09:43:38 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 12038 7 1200.25 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.94 2/54 16464
Raw data (stat): 16464 (runsolver) R 16463 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543969102 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0002 s]
Raw data (loadavg): 0.87 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 9638 0 0 0 977 21 0 0 25 0 1 0 543969102 26656768 5895 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6508 5895 603 41 0 6467 0
vsize: 26032
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 9902 0 0 0 1976 21 0 0 25 0 1 0 543969102 27406336 6117 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.0021 s]
Raw data (loadavg): 0.91 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 9902 0 0 0 2976 21 0 0 25 0 1 0 543969102 27406336 6117 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.0016 s]
Raw data (loadavg): 0.92 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 9963 0 0 0 3976 22 0 0 25 0 1 0 543969102 27676672 6178 4294967295 134512640 134672761 3221224544 3221223688 134560630 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.0197 s]
Raw data (loadavg): 0.93 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10013 0 0 0 4978 22 0 0 25 0 1 0 543969102 27947008 6228 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.0222 s]
Raw data (loadavg): 0.94 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10057 0 0 0 5978 22 0 0 25 0 1 0 543969102 28078080 6272 4294967295 134512640 134672761 3221224544 3221223692 134560552 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.0254 s]
Raw data (loadavg): 0.95 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10134 0 0 0 6978 23 0 0 25 0 1 0 543969102 28348416 6349 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.0259 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10348 0 0 0 7977 23 0 0 25 0 1 0 543969102 33046528 6540 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.0261 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10392 0 0 0 8977 23 0 0 25 0 1 0 543969102 33046528 6542 4294967295 134512640 134672761 3221224544 3221223712 134561261 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.027 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10538 0 0 0 9977 24 0 0 25 0 1 0 543969102 33099776 6595 4294967295 134512640 134672761 3221224544 3221223648 134560529 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.027 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10580 0 0 0 10977 24 0 0 25 0 1 0 543969102 33370112 6637 4294967295 134512640 134672761 3221224544 3221223744 134557876 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.029 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10632 0 0 0 11977 24 0 0 25 0 1 0 543969102 33505280 6689 4294967295 134512640 134672761 3221224544 3221223624 134553507 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8180 6689 603 41 0 8139 0
vsize: 32720
[startup+130.029 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10719 0 0 0 12977 25 0 0 25 0 1 0 543969102 33910784 6776 4294967295 134512640 134672761 3221224544 3221223680 134565092 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.029 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10776 0 0 0 13976 25 0 0 25 0 1 0 543969102 34177024 6833 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8344 6833 603 41 0 8303 0
vsize: 33376
[startup+150.03 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10836 0 0 0 14976 25 0 0 25 0 1 0 543969102 34443264 6893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8409 6893 603 41 0 8368 0
vsize: 33636
[startup+160.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10891 0 0 0 15976 25 0 0 25 0 1 0 543969102 34578432 6948 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 10950 0 0 0 16976 26 0 0 25 0 1 0 543969102 34844672 7007 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8507 7007 603 41 0 8466 0
vsize: 34028
[startup+180.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11012 0 0 0 17976 26 0 0 25 0 1 0 543969102 35237888 7069 4294967295 134512640 134672761 3221224544 3221223744 134557849 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.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11053 0 0 0 18976 26 0 0 25 0 1 0 543969102 35373056 7110 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 7110 603 41 0 8595 0
vsize: 34544
[startup+200.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11128 0 0 0 19976 27 0 0 25 0 1 0 543969102 35643392 7185 4294967295 134512640 134672761 3221224544 3221223728 134559332 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.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11160 0 0 0 20975 27 0 0 25 0 1 0 543969102 35778560 7217 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8735 7217 603 41 0 8694 0
vsize: 34940
[startup+220.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11209 0 0 0 21976 27 0 0 25 0 1 0 543969102 36048896 7266 4294967295 134512640 134672761 3221224544 3221223712 134561201 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.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11244 0 0 0 22976 27 0 0 25 0 1 0 543969102 36184064 7301 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8834 7301 603 41 0 8793 0
vsize: 35336
[startup+240.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11288 0 0 0 23976 27 0 0 25 0 1 0 543969102 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.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11370 0 0 0 24976 27 0 0 25 0 1 0 543969102 36405248 7379 4294967295 134512640 134672761 3221224544 3221223712 134560885 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.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11370 0 0 0 25976 27 0 0 25 0 1 0 543969102 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+270.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11370 0 0 0 26976 27 0 0 25 0 1 0 543969102 36405248 7379 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11491 0 0 0 27976 28 0 0 25 0 1 0 543969102 36421632 7383 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8892 7383 603 41 0 8851 0
vsize: 35568
[startup+290.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11500 0 0 0 28976 28 0 0 25 0 1 0 543969102 36552704 7392 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8924 7392 603 41 0 8883 0
vsize: 35696
[startup+300.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11681 0 0 0 29976 28 0 0 25 0 1 0 543969102 37208064 7573 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9084 7573 603 41 0 9043 0
vsize: 36336
[startup+310.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 11731 0 0 0 30975 29 0 0 25 0 1 0 543969102 37478400 7623 4294967295 134512640 134672761 3221224544 3221223712 134560819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9150 7623 603 41 0 9109 0
vsize: 36600
[startup+320.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 12152 0 0 0 31974 30 0 0 25 0 1 0 543969102 39227392 8044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9577 8044 603 41 0 9536 0
vsize: 38308
[startup+330.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 12322 0 0 0 32974 30 0 0 25 0 1 0 543969102 39788544 8190 4294967295 134512640 134672761 3221224544 3221223712 134560839 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 12401 0 0 0 33974 30 0 0 25 0 1 0 543969102 40058880 8269 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 12495 0 0 0 34974 31 0 0 25 0 1 0 543969102 40345600 8338 4294967295 134512640 134672761 3221224544 3221223680 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9850 8338 603 41 0 9809 0
vsize: 39400
[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 12525 0 0 0 35974 31 0 0 25 0 1 0 543969102 40476672 8368 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9882 8368 603 41 0 9841 0
vsize: 39528
[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 12641 0 0 0 36973 32 0 0 25 0 1 0 543969102 41013248 8484 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10013 8484 603 41 0 9972 0
vsize: 40052
[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 12803 0 0 0 37973 33 0 0 25 0 1 0 543969102 41676800 8646 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10175 8646 603 41 0 10134 0
vsize: 40700
[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 13055 0 0 0 38972 33 0 0 25 0 1 0 543969102 42606592 8898 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10402 8898 603 41 0 10361 0
vsize: 41608
[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 13151 0 0 0 39972 34 0 0 25 0 1 0 543969102 43134976 8994 4294967295 134512640 134672761 3221224544 3221223648 134560158 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.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 13282 0 0 0 40972 34 0 0 25 0 1 0 543969102 43659264 9125 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10659 9125 603 41 0 10618 0
vsize: 42636
[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 13438 0 0 0 41972 34 0 0 25 0 1 0 543969102 44335104 9281 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10824 9281 603 41 0 10783 0
vsize: 43296
[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 13626 0 0 0 42971 35 0 0 25 0 1 0 543969102 45133824 9469 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11019 9469 603 41 0 10978 0
vsize: 44076
[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 13995 0 0 0 43971 36 0 0 25 0 1 0 543969102 46616576 9838 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11381 9838 603 41 0 11340 0
vsize: 45524
[startup+450.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 14528 0 0 0 44969 37 0 0 25 0 1 0 543969102 48734208 10371 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11898 10371 603 41 0 11857 0
vsize: 47592
[startup+460.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 14810 0 0 0 45969 38 0 0 25 0 1 0 543969102 49942528 10653 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12193 10653 603 41 0 12152 0
vsize: 48772
[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 14950 0 0 0 46969 38 0 0 25 0 1 0 543969102 50470912 10793 4294967295 134512640 134672761 3221224544 3221223648 134560364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12322 10793 603 41 0 12281 0
vsize: 49288
[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 15068 0 0 0 47969 39 0 0 25 0 1 0 543969102 50999296 10911 4294967295 134512640 134672761 3221224544 3221223744 134557809 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.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 15187 0 0 0 48968 39 0 0 25 0 1 0 543969102 51404800 11030 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12550 11030 603 41 0 12509 0
vsize: 50200
[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 15272 0 0 0 49968 39 0 0 25 0 1 0 543969102 51793920 11115 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12645 11115 603 41 0 12604 0
vsize: 50580
[startup+510.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 15295 0 0 0 50968 39 0 0 25 0 1 0 543969102 51916800 11138 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12675 11138 603 41 0 12634 0
vsize: 50700
[startup+520.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 15345 0 0 0 51969 39 0 0 25 0 1 0 543969102 52043776 11188 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12706 11188 603 41 0 12665 0
vsize: 50824
[startup+530.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 15366 0 0 0 52969 39 0 0 25 0 1 0 543969102 52174848 11209 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12738 11209 603 41 0 12697 0
vsize: 50952
[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 15482 0 0 0 53969 40 0 0 25 0 1 0 543969102 52699136 11325 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12866 11325 603 41 0 12825 0
vsize: 51464
[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 15688 0 0 0 54968 40 0 0 25 0 1 0 543969102 53493760 11531 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13060 11531 603 41 0 13019 0
vsize: 52240
[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 15801 0 0 0 55968 41 0 0 25 0 1 0 543969102 53899264 11644 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13159 11644 603 41 0 13118 0
vsize: 52636
[startup+570.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 16094 0 0 0 56967 41 0 0 25 0 1 0 543969102 55099392 11937 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13452 11937 603 41 0 13411 0
vsize: 53808
[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 16499 0 0 0 57966 42 0 0 25 0 1 0 543969102 56832000 12342 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13875 12342 603 41 0 13834 0
vsize: 55500
[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 16857 0 0 0 58966 43 0 0 25 0 1 0 543969102 58277888 12700 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14228 12700 603 41 0 14187 0
vsize: 56912
[startup+600.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 17313 0 0 0 59965 44 0 0 25 0 1 0 543969102 60141568 13156 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14683 13156 603 41 0 14642 0
vsize: 58732
[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 17751 0 0 0 60965 44 0 0 25 0 1 0 543969102 61865984 13594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15104 13594 603 41 0 15063 0
vsize: 60416
[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 17962 0 0 0 61964 45 0 0 25 0 1 0 543969102 62795776 13805 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15331 13805 603 41 0 15290 0
vsize: 61324
[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 18075 0 0 0 62964 45 0 0 25 0 1 0 543969102 63193088 13918 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15428 13918 603 41 0 15387 0
vsize: 61712
[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 18295 0 0 0 63964 46 0 0 25 0 1 0 543969102 64131072 14138 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15657 14138 603 41 0 15616 0
vsize: 62628
[startup+650.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 18522 0 0 0 64963 47 0 0 25 0 1 0 543969102 65056768 14365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15883 14365 603 41 0 15842 0
vsize: 63532
[startup+660.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 18659 0 0 0 65963 47 0 0 25 0 1 0 543969102 65851392 14502 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16077 14502 603 41 0 16036 0
vsize: 64308
[startup+670.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 18757 0 0 0 66962 48 0 0 25 0 1 0 543969102 66248704 14600 4294967295 134512640 134672761 3221224544 3221223600 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16174 14600 603 41 0 16133 0
vsize: 64696
[startup+680.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 18966 0 0 0 67962 49 0 0 25 0 1 0 543969102 67174400 14809 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16400 14809 603 41 0 16359 0
vsize: 65600
[startup+690.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 19047 0 0 0 68962 49 0 0 25 0 1 0 543969102 67440640 14890 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16465 14890 603 41 0 16424 0
vsize: 65860
[startup+700.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 19113 0 0 0 69962 49 0 0 25 0 1 0 543969102 67710976 14956 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16531 14956 603 41 0 16490 0
vsize: 66124
[startup+710.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 19184 0 0 0 70961 49 0 0 25 0 1 0 543969102 67981312 15027 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16597 15027 603 41 0 16556 0
vsize: 66388
[startup+720.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 19278 0 0 0 71961 50 0 0 25 0 1 0 543969102 68366336 15121 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16691 15121 603 41 0 16650 0
vsize: 66764
[startup+730.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 19392 0 0 0 72961 50 0 0 25 0 1 0 543969102 68902912 15235 4294967295 134512640 134672761 3221224544 3221223648 134560306 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16822 15235 603 41 0 16781 0
vsize: 67288
[startup+740.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 19616 0 0 0 73960 51 0 0 25 0 1 0 543969102 69849088 15459 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17053 15459 603 41 0 17012 0
vsize: 68212
[startup+750.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 19981 0 0 0 74960 52 0 0 25 0 1 0 543969102 71311360 15824 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17410 15824 603 41 0 17369 0
vsize: 69640
[startup+760.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 20340 0 0 0 75959 53 0 0 25 0 1 0 543969102 72769536 16183 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17766 16183 603 41 0 17725 0
vsize: 71064
[startup+770.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 20594 0 0 0 76958 54 0 0 25 0 1 0 543969102 73830400 16437 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18025 16437 603 41 0 17984 0
vsize: 72100
[startup+780.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 20832 0 0 0 77957 55 0 0 25 0 1 0 543969102 74752000 16675 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18250 16675 603 41 0 18209 0
vsize: 73000
[startup+790.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 21197 0 0 0 78957 55 0 0 25 0 1 0 543969102 76206080 17040 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18605 17040 603 41 0 18564 0
vsize: 74420
[startup+800.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 21339 0 0 0 79957 56 0 0 25 0 1 0 543969102 76746752 17182 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18737 17182 603 41 0 18696 0
vsize: 74948
[startup+810.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 21556 0 0 0 80956 57 0 0 25 0 1 0 543969102 77672448 17399 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18963 17399 603 41 0 18922 0
vsize: 75852
[startup+820.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 21965 0 0 0 81956 57 0 0 25 0 1 0 543969102 79413248 17808 4294967295 134512640 134672761 3221224544 3221223648 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19388 17808 603 41 0 19347 0
vsize: 77552
[startup+830.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 22265 0 0 0 82954 59 0 0 25 0 1 0 543969102 80613376 18108 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18108 603 41 0 19640 0
vsize: 78724
[startup+840.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 22558 0 0 0 83953 60 0 0 25 0 1 0 543969102 81817600 18401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19975 18401 603 41 0 19934 0
vsize: 79900
[startup+850.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 22781 0 0 0 84953 60 0 0 25 0 1 0 543969102 82628608 18624 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20173 18624 603 41 0 20132 0
vsize: 80692
[startup+860.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 22902 0 0 0 85953 60 0 0 25 0 1 0 543969102 83161088 18745 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20303 18745 603 41 0 20262 0
vsize: 81212
[startup+870.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 23038 0 0 0 86953 60 0 0 25 0 1 0 543969102 83697664 18881 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20434 18881 603 41 0 20393 0
vsize: 81736
[startup+880.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 23344 0 0 0 87952 61 0 0 25 0 1 0 543969102 85020672 19187 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20757 19187 603 41 0 20716 0
vsize: 83028
[startup+890.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 23660 0 0 0 88952 62 0 0 25 0 1 0 543969102 86212608 19503 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21048 19503 603 41 0 21007 0
vsize: 84192
[startup+900.053 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 23972 0 0 0 89951 63 0 0 25 0 1 0 543969102 87535616 19815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21371 19815 603 41 0 21330 0
vsize: 85484
[startup+910.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 24262 0 0 0 90951 63 0 0 25 0 1 0 543969102 88752128 20105 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21668 20105 603 41 0 21627 0
vsize: 86672
[startup+920.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 24531 0 0 0 91950 64 0 0 25 0 1 0 543969102 89821184 20374 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21929 20374 603 41 0 21888 0
vsize: 87716
[startup+930.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 24754 0 0 0 92950 65 0 0 25 0 1 0 543969102 90750976 20597 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22156 20597 603 41 0 22115 0
vsize: 88624
[startup+940.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 24984 0 0 0 93949 65 0 0 25 0 1 0 543969102 91709440 20827 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22390 20827 603 41 0 22349 0
vsize: 89560
[startup+950.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25230 0 0 0 94949 66 0 0 25 0 1 0 543969102 92639232 21073 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22617 21073 603 41 0 22576 0
vsize: 90468
[startup+960.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25399 0 0 0 95948 67 0 0 25 0 1 0 543969102 93429760 21242 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22810 21242 603 41 0 22769 0
vsize: 91240
[startup+970.054 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25724 0 0 0 96947 68 0 0 25 0 1 0 543969102 94769152 21567 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23137 21567 603 41 0 23096 0
vsize: 92548
[startup+980.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 97947 68 0 0 25 0 1 0 543969102 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+990.055 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 98947 68 0 0 25 0 1 0 543969102 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+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 99947 68 0 0 25 0 1 0 543969102 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.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 100947 68 0 0 25 0 1 0 543969102 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+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 101947 68 0 0 25 0 1 0 543969102 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.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 102947 68 0 0 25 0 1 0 543969102 94896128 21627 4294967295 134512640 134672761 3221224544 3221223680 134560673 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.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 103947 68 0 0 25 0 1 0 543969102 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134559887 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.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 104948 69 0 0 25 0 1 0 543969102 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+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 105948 69 0 0 25 0 1 0 543969102 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
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 106948 69 0 0 25 0 1 0 543969102 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560874 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.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 107948 69 0 0 25 0 1 0 543969102 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560355 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.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 108948 69 0 0 25 0 1 0 543969102 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+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 109948 69 0 0 25 0 1 0 543969102 94896128 21627 4294967295 134512640 134672761 3221224544 3221223728 134559340 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.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 110948 69 0 0 25 0 1 0 543969102 94896128 21627 4294967295 134512640 134672761 3221224544 3221223728 134558687 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.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 111949 69 0 0 25 0 1 0 543969102 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560839 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.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 112949 69 0 0 25 0 1 0 543969102 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+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 113949 69 0 0 25 0 1 0 543969102 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+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 114949 69 0 0 25 0 1 0 543969102 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+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 115950 69 0 0 25 0 1 0 543969102 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+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 116950 69 0 0 25 0 1 0 543969102 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560980 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.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 117950 69 0 0 25 0 1 0 543969102 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560937 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.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 118950 69 0 0 25 0 1 0 543969102 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134561011 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.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 16464
Raw data (stat): 16464 (minisat+) R 16463 18865 18864 0 -1 0 25854 0 0 0 119950 69 0 0 25 0 1 0 543969102 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.94 1/54 16464
Raw data (stat): 16464 (minisat+) Z 16463 18865 18864 0 -1 12 25857 0 0 0 119950 74 0 0 25 0 1 0 543969102 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.11
CPU time (s): 1200.25
CPU user time (s): 1199.51
CPU system time (s): 0.741887
CPU usage (%): 100.012
Max. virtual memory (Kb): 92672
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####