PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 17:49:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17030 boxname=wulflinc30 idbench=1310 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fbdb3cf321a85412feefcaac30780520  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-mod008.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-mod008.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-mod008.opb
IDLAUNCH: 17030
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        844856 kB
Buffers:         10460 kB
Cached:         152712 kB
SwapCached:         28 kB
Active:          49828 kB
Inactive:       116132 kB
HighTotal:      131008 kB
HighFree:        14952 kB
LowTotal:       903652 kB
LowFree:        829904 kB
SwapTotal:     2097892 kB
SwapFree:      2097796 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            18156 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:09:36 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 17030 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 
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.84 0.94 0.90 2/54 23038
Raw data (stat): 23038 (runsolver) R 23037 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547005141 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.87 0.94 0.90 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 9637 0 0 0 976 23 0 0 25 0 1 0 547005141 26656768 5894 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6508 5894 603 41 0 6467 0
vsize: 26032
[startup+20.0023 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 9902 0 0 0 1974 24 0 0 25 0 1 0 547005141 27406336 6117 4294967295 134512640 134672761 3221224544 3221223712 134560839 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.0028 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 9902 0 0 0 2974 24 0 0 25 0 1 0 547005141 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+40.0029 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 9961 0 0 0 3973 24 0 0 25 0 1 0 547005141 27676672 6176 4294967295 134512640 134672761 3221224544 3221223728 134558662 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.0036 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10010 0 0 0 4974 24 0 0 25 0 1 0 547005141 27947008 6225 4294967295 134512640 134672761 3221224544 3221223696 134561035 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.0032 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10054 0 0 0 5973 24 0 0 25 0 1 0 547005141 28078080 6269 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.0043 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10120 0 0 0 6973 25 0 0 25 0 1 0 547005141 28348416 6335 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6921 6335 603 41 0 6880 0
vsize: 27684
[startup+80.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10181 0 0 0 7973 25 0 0 25 0 1 0 547005141 28618752 6396 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.0046 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10392 0 0 0 8973 26 0 0 25 0 1 0 547005141 33046528 6542 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10538 0 0 0 9973 26 0 0 25 0 1 0 547005141 33099776 6595 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8081 6595 603 41 0 8040 0
vsize: 32324
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10573 0 0 0 10973 26 0 0 25 0 1 0 547005141 33370112 6630 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8147 6630 603 41 0 8106 0
vsize: 32588
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10621 0 0 0 11973 26 0 0 25 0 1 0 547005141 33505280 6678 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8180 6678 603 41 0 8139 0
vsize: 32720
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10697 0 0 0 12973 27 0 0 25 0 1 0 547005141 33775616 6754 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8246 6754 603 41 0 8205 0
vsize: 32984
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10766 0 0 0 13972 27 0 0 25 0 1 0 547005141 34045952 6823 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8312 6823 603 41 0 8271 0
vsize: 33248
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10826 0 0 0 14971 28 0 0 25 0 1 0 547005141 34308096 6883 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8376 6883 603 41 0 8335 0
vsize: 33504
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10884 0 0 0 15971 28 0 0 25 0 1 0 547005141 34578432 6941 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8442 6941 603 41 0 8401 0
vsize: 33768
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 10930 0 0 0 16971 28 0 0 25 0 1 0 547005141 34713600 6987 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8475 6987 603 41 0 8434 0
vsize: 33900
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11012 0 0 0 17971 28 0 0 25 0 1 0 547005141 35237888 7069 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8603 7069 603 41 0 8562 0
vsize: 34412
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11037 0 0 0 18971 28 0 0 25 0 1 0 547005141 35373056 7094 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 7094 603 41 0 8595 0
vsize: 34544
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11122 0 0 0 19971 28 0 0 25 0 1 0 547005141 35643392 7179 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8702 7179 603 41 0 8661 0
vsize: 34808
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11146 0 0 0 20971 28 0 0 25 0 1 0 547005141 35778560 7203 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8735 7203 603 41 0 8694 0
vsize: 34940
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11189 0 0 0 21971 28 0 0 25 0 1 0 547005141 35913728 7246 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8768 7246 603 41 0 8727 0
vsize: 35072
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11236 0 0 0 22971 29 0 0 25 0 1 0 547005141 36184064 7293 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8834 7293 603 41 0 8793 0
vsize: 35336
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11288 0 0 0 23971 29 0 0 25 0 1 0 547005141 36405248 7345 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11365 0 0 0 24971 29 0 0 25 0 1 0 547005141 36405248 7377 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8888 7377 603 41 0 8847 0
vsize: 35552
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11370 0 0 0 25971 29 0 0 25 0 1 0 547005141 36405248 7379 4294967295 134512640 134672761 3221224544 3221223680 134560706 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11370 0 0 0 26972 29 0 0 25 0 1 0 547005141 36405248 7379 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8888 7379 603 41 0 8847 0
vsize: 35552
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11491 0 0 0 27971 29 0 0 25 0 1 0 547005141 36421632 7383 4294967295 134512640 134672761 3221224544 3221223648 134560154 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11491 0 0 0 28971 29 0 0 25 0 1 0 547005141 36421632 7383 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11534 0 0 0 29971 30 0 0 25 0 1 0 547005141 36687872 7426 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8957 7426 603 41 0 8916 0
vsize: 35828
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11701 0 0 0 30971 30 0 0 25 0 1 0 547005141 37343232 7593 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9117 7593 603 41 0 9076 0
vsize: 36468
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 11950 0 0 0 31970 31 0 0 25 0 1 0 547005141 38420480 7842 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9380 7842 603 41 0 9339 0
vsize: 37520
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 12252 0 0 0 32970 32 0 0 25 0 1 0 547005141 39632896 8144 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9676 8144 603 41 0 9635 0
vsize: 38704
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 12330 0 0 0 33970 32 0 0 25 0 1 0 547005141 39788544 8198 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9714 8198 603 41 0 9673 0
vsize: 38856
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 12475 0 0 0 34969 33 0 0 25 0 1 0 547005141 40214528 8318 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9818 8318 603 41 0 9777 0
vsize: 39272
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 12514 0 0 0 35969 33 0 0 25 0 1 0 547005141 40476672 8357 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9882 8357 603 41 0 9841 0
vsize: 39528
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 12567 0 0 0 36969 33 0 0 25 0 1 0 547005141 40611840 8410 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9915 8410 603 41 0 9874 0
vsize: 39660
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 12719 0 0 0 37969 33 0 0 25 0 1 0 547005141 41279488 8562 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10078 8562 603 41 0 10037 0
vsize: 40312
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 12867 0 0 0 38969 34 0 0 25 0 1 0 547005141 41807872 8710 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10207 8710 603 41 0 10166 0
vsize: 40828
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 13109 0 0 0 39968 35 0 0 25 0 1 0 547005141 42872832 8952 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10467 8952 603 41 0 10426 0
vsize: 41868
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 13227 0 0 0 40968 35 0 0 25 0 1 0 547005141 43397120 9070 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10595 9070 603 41 0 10554 0
vsize: 42380
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 13352 0 0 0 41968 35 0 0 25 0 1 0 547005141 43929600 9195 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10725 9195 603 41 0 10684 0
vsize: 42900
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 13482 0 0 0 42968 36 0 0 25 0 1 0 547005141 44470272 9325 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10857 9325 603 41 0 10816 0
vsize: 43428
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 13764 0 0 0 43967 37 0 0 25 0 1 0 547005141 45682688 9607 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11153 9607 603 41 0 11112 0
vsize: 44612
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 14176 0 0 0 44965 38 0 0 25 0 1 0 547005141 47280128 10019 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11543 10019 603 41 0 11502 0
vsize: 46172
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 14666 0 0 0 45964 40 0 0 25 0 1 0 547005141 49274880 10509 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12030 10509 603 41 0 11989 0
vsize: 48120
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 14877 0 0 0 46964 40 0 0 25 0 1 0 547005141 50212864 10720 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12259 10720 603 41 0 12218 0
vsize: 49036
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 14964 0 0 0 47964 40 0 0 25 0 1 0 547005141 50601984 10807 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12354 10807 603 41 0 12313 0
vsize: 49416
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 15107 0 0 0 48963 41 0 0 25 0 1 0 547005141 51138560 10950 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12485 10950 603 41 0 12444 0
vsize: 49940
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 15202 0 0 0 49963 42 0 0 25 0 1 0 547005141 51539968 11045 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12583 11045 603 41 0 12542 0
vsize: 50332
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 15279 0 0 0 50963 42 0 0 25 0 1 0 547005141 51793920 11122 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12645 11122 603 41 0 12604 0
vsize: 50580
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 15311 0 0 0 51963 42 0 0 25 0 1 0 547005141 51916800 11154 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12675 11154 603 41 0 12634 0
vsize: 50700
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 15349 0 0 0 52963 42 0 0 25 0 1 0 547005141 52043776 11192 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12706 11192 603 41 0 12665 0
vsize: 50824
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 15397 0 0 0 53963 42 0 0 25 0 1 0 547005141 52310016 11240 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12771 11240 603 41 0 12730 0
vsize: 51084
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 15558 0 0 0 54963 43 0 0 25 0 1 0 547005141 52965376 11401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12931 11401 603 41 0 12890 0
vsize: 51724
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 15717 0 0 0 55962 43 0 0 25 0 1 0 547005141 53628928 11560 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13093 11560 603 41 0 13052 0
vsize: 52372
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 15939 0 0 0 56962 44 0 0 25 0 1 0 547005141 54566912 11782 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13322 11782 603 41 0 13281 0
vsize: 53288
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 16188 0 0 0 57961 44 0 0 25 0 1 0 547005141 55496704 12031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13549 12031 603 41 0 13508 0
vsize: 54196
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 16588 0 0 0 58961 45 0 0 25 0 1 0 547005141 57090048 12431 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13938 12431 603 41 0 13897 0
vsize: 55752
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 16940 0 0 0 59960 46 0 0 25 0 1 0 547005141 58544128 12783 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14293 12783 603 41 0 14252 0
vsize: 57172
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 17419 0 0 0 60958 48 0 0 25 0 1 0 547005141 60542976 13262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14781 13262 603 41 0 14740 0
vsize: 59124
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23038
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 17817 0 0 0 61958 49 0 0 25 0 1 0 547005141 62132224 13660 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15169 13660 603 41 0 15128 0
vsize: 60676
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 23073
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 17999 0 0 0 62957 50 0 0 25 0 1 0 547005141 62935040 13842 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15365 13842 603 41 0 15324 0
vsize: 61460
[startup+640.015 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 23091
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 18083 0 0 0 63956 50 0 0 25 0 1 0 547005141 63328256 13926 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15461 13926 603 41 0 15420 0
vsize: 61844
[startup+650.016 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 23091
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 18331 0 0 0 64956 51 0 0 25 0 1 0 547005141 64258048 14174 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15688 14174 603 41 0 15647 0
vsize: 62752
[startup+660.015 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 23091
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 18565 0 0 0 65956 51 0 0 25 0 1 0 547005141 65449984 14408 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15979 14408 603 41 0 15938 0
vsize: 63916
[startup+670.016 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 23091
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 18662 0 0 0 66956 51 0 0 25 0 1 0 547005141 65851392 14505 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16077 14505 603 41 0 16036 0
vsize: 64308
[startup+680.016 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23091
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 18772 0 0 0 67956 52 0 0 25 0 1 0 547005141 66375680 14615 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 14615 603 41 0 16164 0
vsize: 64820
[startup+690.016 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23091
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 18972 0 0 0 68955 52 0 0 25 0 1 0 547005141 67174400 14815 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16400 14815 603 41 0 16359 0
vsize: 65600
[startup+700.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 19052 0 0 0 69955 53 0 0 25 0 1 0 547005141 67440640 14895 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16465 14895 603 41 0 16424 0
vsize: 65860
[startup+710.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 19123 0 0 0 70955 53 0 0 25 0 1 0 547005141 67710976 14966 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16531 14966 603 41 0 16490 0
vsize: 66124
[startup+720.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 19196 0 0 0 71954 54 0 0 25 0 1 0 547005141 68108288 15039 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16628 15039 603 41 0 16587 0
vsize: 66512
[startup+730.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 19279 0 0 0 72954 54 0 0 25 0 1 0 547005141 68366336 15122 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16691 15122 603 41 0 16650 0
vsize: 66764
[startup+740.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 19414 0 0 0 73954 54 0 0 25 0 1 0 547005141 68902912 15257 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16822 15257 603 41 0 16781 0
vsize: 67288
[startup+750.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 19652 0 0 0 74954 55 0 0 25 0 1 0 547005141 69984256 15495 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17086 15495 603 41 0 17045 0
vsize: 68344
[startup+760.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 20000 0 0 0 75953 56 0 0 25 0 1 0 547005141 71311360 15843 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17410 15843 603 41 0 17369 0
vsize: 69640
[startup+770.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 20359 0 0 0 76952 57 0 0 25 0 1 0 547005141 72769536 16202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17766 16202 603 41 0 17725 0
vsize: 71064
[startup+780.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 20600 0 0 0 77952 58 0 0 25 0 1 0 547005141 73830400 16443 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18025 16443 603 41 0 17984 0
vsize: 72100
[startup+790.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 20848 0 0 0 78951 58 0 0 25 0 1 0 547005141 74752000 16691 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18250 16691 603 41 0 18209 0
vsize: 73000
[startup+800.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 21204 0 0 0 79951 59 0 0 25 0 1 0 547005141 76206080 17047 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18605 17047 603 41 0 18564 0
vsize: 74420
[startup+810.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 21339 0 0 0 80950 59 0 0 25 0 1 0 547005141 76746752 17182 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18737 17182 603 41 0 18696 0
vsize: 74948
[startup+820.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 21558 0 0 0 81950 60 0 0 25 0 1 0 547005141 77672448 17401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18963 17401 603 41 0 18922 0
vsize: 75852
[startup+830.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 21958 0 0 0 82950 61 0 0 25 0 1 0 547005141 79282176 17801 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19356 17801 603 41 0 19315 0
vsize: 77424
[startup+840.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 22252 0 0 0 83949 61 0 0 25 0 1 0 547005141 80478208 18095 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19648 18095 603 41 0 19607 0
vsize: 78592
[startup+850.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 22549 0 0 0 84947 63 0 0 25 0 1 0 547005141 81686528 18392 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19943 18392 603 41 0 19902 0
vsize: 79772
[startup+860.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 22757 0 0 0 85947 63 0 0 25 0 1 0 547005141 82628608 18600 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20173 18600 603 41 0 20132 0
vsize: 80692
[startup+870.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 22897 0 0 0 86947 63 0 0 25 0 1 0 547005141 83161088 18740 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20303 18740 603 41 0 20262 0
vsize: 81212
[startup+880.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 23021 0 0 0 87946 64 0 0 25 0 1 0 547005141 83697664 18864 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20434 18864 603 41 0 20393 0
vsize: 81736
[startup+890.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 23320 0 0 0 88945 65 0 0 25 0 1 0 547005141 84885504 19163 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20724 19163 603 41 0 20683 0
vsize: 82896
[startup+900.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 23630 0 0 0 89945 66 0 0 25 0 1 0 547005141 86081536 19473 4294967295 134512640 134672761 3221224544 3221223648 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21016 19473 603 41 0 20975 0
vsize: 84064
[startup+910.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 23944 0 0 0 90944 67 0 0 25 0 1 0 547005141 87404544 19787 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21339 19787 603 41 0 21298 0
vsize: 85356
[startup+920.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 24229 0 0 0 91943 68 0 0 25 0 1 0 547005141 88616960 20072 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21635 20072 603 41 0 21594 0
vsize: 86540
[startup+930.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 24497 0 0 0 92942 69 0 0 25 0 1 0 547005141 89686016 20340 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21896 20340 603 41 0 21855 0
vsize: 87584
[startup+940.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 24727 0 0 0 93941 70 0 0 25 0 1 0 547005141 90619904 20570 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22124 20570 603 41 0 22083 0
vsize: 88496
[startup+950.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 24929 0 0 0 94941 71 0 0 25 0 1 0 547005141 91443200 20772 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22325 20772 603 41 0 22284 0
vsize: 89300
[startup+960.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25191 0 0 0 95939 73 0 0 25 0 1 0 547005141 92508160 21034 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22585 21034 603 41 0 22544 0
vsize: 90340
[startup+970.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23093
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25396 0 0 0 96939 73 0 0 25 0 1 0 547005141 93429760 21239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22810 21239 603 41 0 22769 0
vsize: 91240
[startup+980.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25659 0 0 0 97938 74 0 0 25 0 1 0 547005141 94507008 21502 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23073 21502 603 41 0 23032 0
vsize: 92292
[startup+990.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 98938 75 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 99938 75 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 100938 75 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 101937 75 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 102937 76 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223728 134559424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 103937 76 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 104937 76 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 105937 76 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 106936 77 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 107936 77 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 108936 78 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 109936 78 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 110935 78 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 111935 79 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 112935 79 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 113935 79 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 114935 80 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 115935 80 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 116935 80 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 117935 80 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 118934 80 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23095
Raw data (stat): 23038 (minisat+) R 23037 11931 11930 0 -1 0 25854 0 0 0 119934 81 0 0 25 0 1 0 547005141 94896128 21627 4294967295 134512640 134672761 3221224544 3221223808 134562495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23168 21627 603 41 0 23127 0
vsize: 92672
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 23095
Raw data (stat): 23038 (minisat+) Z 23037 11931 11930 0 -1 12 25857 0 0 0 119934 85 0 0 25 0 1 0 547005141 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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