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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.5:100.opb
MD5SUM	dd81121db7c1c4b8597dd9571c707a87
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3
Optimality of the best value was proved	NO
Number of terms in the objective function	372
Biggest coefficient in the objective function	220
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	983
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	220
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	983
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	372
Total number of constraints	792
Number of constraints which are clauses	345
Number of constraints which are cardinality constraints (but not clauses)	447
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 6463

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-14 05:06:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4878 boxname=wulflinc5 idbench=366 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  dd81121db7c1c4b8597dd9571c707a87  /oldhome/oroussel/tmp/wulflinc5/normalized-10:10:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc5/normalized-10:10:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc5/normalized-10:10:4.5:0.5:100.opb
IDLAUNCH: 4878
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        891556 kB
Buffers:         35112 kB
Cached:          86376 kB
SwapCached:       2272 kB
Active:          56568 kB
Inactive:        70072 kB
HighTotal:      131008 kB
HighFree:        40712 kB
LowTotal:       903652 kB
LowFree:        850844 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10920 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:26:14 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 4878 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 420 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   35
c ---[  81]---> BDD-cost:   35
c ---[  80]---> BDD-cost:   32
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   26
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   20
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   32
c ---[  72]---> BDD-cost:   35
c ---[  71]---> BDD-cost:   35
c ---[  70]---> BDD-cost:   32
c ---[  69]---> BDD-cost:   35
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   23
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   38
c ---[  61]---> BDD-cost:   44
c ---[  60]---> BDD-cost:   35
c ---[  59]---> BDD-cost:   38
c ---[  58]---> BDD-cost:   32
c ---[  57]---> BDD-cost:   26
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   44
c ---[  51]---> BDD-cost:   47
c ---[  50]---> BDD-cost:   41
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   29
c ---[  47]---> BDD-cost:   21
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   21
c ---[  42]---> BDD-cost:   38
c ---[  41]---> BDD-cost:   32
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   20
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   26
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    8
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    5
c ---[  13]---> BDD-cost:    8
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:    7
c ---[   7]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    7974    22301 |    2658       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 292[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:20799     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   59633   143133 |   19877       0        0     nan |  0.000 % |
c |       100 |   59633   143133 |   21864     100      708     7.1 |  0.404 % |
c |       250 |   59614   143091 |   24051     249     3730    15.0 |  0.430 % |
c ==============================================================================
c [1mFound solution: 177[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       357 |   61693   148217 |   20564     353     4599    13.0 |  0.430 % |
c ==============================================================================
c [1mFound solution: 147[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       378 |   62118   149260 |   20706     374     4751    12.7 |  0.430 % |
c |       478 |   61999   148989 |   22776     473     5414    11.4 |  0.917 % |
c ==============================================================================
c [1mFound solution: 91[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       610 |   62699   150689 |   20899     605     6399    10.6 |  0.917 % |
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       690 |   62790   150927 |   20930     685     8124    11.9 |  0.917 % |
c |       790 |   62637   150585 |   23023     778     9512    12.2 |  1.122 % |
c |       942 |   62287   149790 |   25325     924    11120    12.0 |  1.609 % |
c ==============================================================================
c [1mFound solution: 50[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1128 |   62691   150785 |   20897    1107    13248    12.0 |  1.609 % |
c |      1229 |   62691   150785 |   22986    1208    14195    11.8 |  1.746 % |
c |      1379 |   62667   150731 |   25285    1356    15049    11.1 |  1.776 % |
c ==============================================================================
c [1mFound solution: 44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1555 |   62436   150216 |   20812    1509    17598    11.7 |  1.776 % |
c |      1656 |   62436   150216 |   22893    1610    18193    11.3 |  2.214 % |
c |      1806 |   62436   150216 |   25182    1760    21264    12.1 |  2.214 % |
c |      2031 |   62255   149798 |   27700    1979    23932    12.1 |  2.486 % |
c |      2368 |   62211   149699 |   30470    2313    32205    13.9 |  2.551 % |
c |      2874 |   62101   149450 |   33517    2814    50843    18.1 |  2.713 % |
c |      3633 |   61917   149028 |   36869    3563    60228    16.9 |  2.980 % |
c |      4773 |   61917   149028 |   40556    4703   118518    25.2 |  2.980 % |
c |      6481 |   61795   148750 |   44612    6396   151012    23.6 |  3.148 % |
c ==============================================================================
c [1mFound solution: 42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6736 |   61461   147996 |   20487    6573   153100    23.3 |  3.148 % |
c |      6836 |   61461   147996 |   22535    6673   154315    23.1 |  3.743 % |
c |      6986 |   61461   147996 |   24789    6823   155718    22.8 |  3.743 % |
c |      7212 |   61461   147996 |   27268    7049   159115    22.6 |  3.743 % |
c |      7549 |   61461   147996 |   29995    7386   164687    22.3 |  3.743 % |
c ==============================================================================
c [1mFound solution: 41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7659 |   61473   148028 |   20491    7496   165778    22.1 |  3.743 % |
c |      7761 |   61473   148028 |   22540    7598   166744    21.9 |  3.747 % |
c |      7911 |   61473   148028 |   24794    7748   169364    21.9 |  3.747 % |
c |      8136 |   61473   148028 |   27273    7973   171998    21.6 |  3.747 % |
c |      8473 |   61473   148028 |   30000    8310   182240    21.9 |  3.747 % |
c |      8981 |   61457   147993 |   33000    8817   195410    22.2 |  3.772 % |
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9029 |   61511   148131 |   20503    8865   196062    22.1 |  3.772 % |
c |      9131 |   61511   148131 |   22553    8967   197611    22.0 |  3.779 % |
c |      9282 |   61511   148131 |   24808    9118   200754    22.0 |  3.779 % |
c |      9508 |   61511   148131 |   27289    9344   203103    21.7 |  3.779 % |
c |      9846 |   61511   148131 |   30018    9682   211432    21.8 |  3.779 % |
c ==============================================================================
c [1mFound solution: 35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10227 |   61195   147405 |   20398   10001   216714    21.7 |  3.779 % |
c |     10327 |   61195   147405 |   22437   10101   218252    21.6 |  4.291 % |
c |     10479 |   61195   147405 |   24681   10253   219177    21.4 |  4.291 % |
c |     10704 |   61195   147405 |   27149   10478   225677    21.5 |  4.291 % |
c |     11041 |   61195   147405 |   29864   10815   229757    21.2 |  4.291 % |
c |     11547 |   61170   147348 |   32851   11319   237236    21.0 |  4.325 % |
c |     12307 |   61170   147348 |   36136   12079   249049    20.6 |  4.325 % |
c |     13449 |   61170   147348 |   39749   13221   283390    21.4 |  4.325 % |
c |     15157 |   61160   147325 |   43724   14928   329293    22.1 |  4.340 % |
c |     17719 |   61160   147325 |   48097   17490   412924    23.6 |  4.340 % |
c ==============================================================================
c [1mFound solution: 34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19463 |   61212   147459 |   20404   19234   491237    25.5 |  4.340 % |
c |     19563 |   61212   147459 |   22444   19334   492733    25.5 |  4.347 % |
c |     19716 |   61212   147459 |   24688   19487   494733    25.4 |  4.347 % |
c |     19942 |   61212   147459 |   27157   19713   497700    25.2 |  4.347 % |
c |     20280 |   61212   147459 |   29873   20051   505156    25.2 |  4.347 % |
c |     20786 |   61212   147459 |   32860   20557   520502    25.3 |  4.347 % |
c |     21545 |   61212   147459 |   36146   21316   537024    25.2 |  4.347 % |
c |     22685 |   61212   147459 |   39761   22456   697327    31.1 |  4.347 % |
c ==============================================================================
c [1mFound solution: 33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23673 |   61216   147473 |   20405   23427   746612    31.9 |  4.347 % |
c |     23773 |   61216   147473 |   22445   11814   417833    35.4 |  4.361 % |
c |     23925 |   61216   147473 |   24690   11966   419132    35.0 |  4.361 % |
c |     24150 |   61216   147473 |   27159   12191   426297    35.0 |  4.361 % |
c |     24488 |   61216   147473 |   29874   12529   437344    34.9 |  4.361 % |
c |     24994 |   61216   147473 |   32862   13035   452333    34.7 |  4.361 % |
c |     25755 |   61216   147473 |   36148   13796   465826    33.8 |  4.361 % |
c |     26896 |   61216   147473 |   39763   14937   626430    41.9 |  4.361 % |
c ==============================================================================
c [1mFound solution: 32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27252 |   61227   147502 |   20409   15293   655718    42.9 |  4.361 % |
c |     27354 |   61227   147502 |   22449   15395   656944    42.7 |  4.365 % |
c |     27504 |   61227   147502 |   24694   15545   662690    42.6 |  4.365 % |
c |     27729 |   61227   147502 |   27164   15770   666460    42.3 |  4.365 % |
c |     28066 |   61227   147502 |   29880   16107   670119    41.6 |  4.365 % |
c |     28574 |   61227   147502 |   32868   16615   710767    42.8 |  4.365 % |
c |     29333 |   61181   147397 |   36155   17355   733362    42.3 |  4.439 % |
c |     30474 |   61181   147397 |   39771   18496   747119    40.4 |  4.439 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32089 |   60871   146686 |   20290   18776   771392    41.1 |  4.439 % |
c |     32189 |   60811   146548 |   22319   18865   772046    40.9 |  4.990 % |
c |     32339 |   60811   146548 |   24550   19015   775968    40.8 |  4.990 % |
c |     32564 |   60811   146548 |   27005   19240   785121    40.8 |  4.990 % |
c |     32902 |   60672   146234 |   29706   19441   789133    40.6 |  5.182 % |
c |     33408 |   60672   146234 |   32677   19947   824368    41.3 |  5.182 % |
c |     34168 |   60672   146234 |   35944   20707   848029    41.0 |  5.182 % |
c |     35307 |   60662   146212 |   39539   21845   884454    40.5 |  5.187 % |
c |     37017 |   60662   146212 |   43493   23555   919556    39.0 |  5.187 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38467 |   60711   146337 |   20237   25005   996912    39.9 |  5.187 % |
c |     38567 |   60570   146016 |   22260   12585   286554    22.8 |  5.380 % |
c |     38717 |   60570   146016 |   24486   12735   287439    22.6 |  5.380 % |
c |     38942 |   60570   146016 |   26935   12960   293267    22.6 |  5.380 % |
c |     39280 |   60570   146016 |   29628   13298   299236    22.5 |  5.380 % |
c |     39786 |   60570   146016 |   32591   13804   322334    23.4 |  5.380 % |
c |     40545 |   60570   146016 |   35851   14563   333180    22.9 |  5.380 % |
c |     41684 |   60570   146016 |   39436   15702   370399    23.6 |  5.380 % |
c |     43393 |   60570   146016 |   43379   17411   434032    24.9 |  5.380 % |
c |     45957 |   60570   146016 |   47717   19975   854120    42.8 |  5.380 % |
c |     49801 |   60570   146016 |   52489   23819  1086129    45.6 |  5.380 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51268 |   60587   146059 |   20195   25286  1128140    44.6 |  5.380 % |
c |     51368 |   60587   146059 |   22214   12743   550632    43.2 |  5.384 % |
c |     51519 |   60587   146059 |   24435   12894   552565    42.9 |  5.384 % |
c |     51747 |   60587   146059 |   26879   13122   559091    42.6 |  5.384 % |
c |     52084 |   60587   146059 |   29567   13459   570777    42.4 |  5.384 % |
c |     52590 |   60587   146059 |   32524   13965   582712    41.7 |  5.384 % |
c |     53351 |   60577   146036 |   35776   14724   590518    40.1 |  5.399 % |
c |     54490 |   60577   146036 |   39354   15863   666205    42.0 |  5.399 % |
c |     56199 |   60577   146036 |   43289   17572   689568    39.2 |  5.399 % |
c |     58761 |   60577   146036 |   47618   20134  1029582    51.1 |  5.399 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60584 |   60628   146167 |   20209   21957  1143437    52.1 |  5.399 % |
c |     60685 |   60628   146167 |   22229   11080   488477    44.1 |  5.400 % |
c |     60836 |   60622   146153 |   24452   11224   489609    43.6 |  5.409 % |
c |     61061 |   60622   146153 |   26898   11449   499167    43.6 |  5.409 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61138 |   60634   146185 |   20211   11526   501402    43.5 |  5.409 % |
c |     61238 |   60634   146185 |   22232   11626   502572    43.2 |  5.414 % |
c |     61388 |   60634   146185 |   24455   11776   506849    43.0 |  5.414 % |
c |     61614 |   60634   146185 |   26900   12002   509728    42.5 |  5.414 % |
c |     61951 |   60634   146185 |   29590   12339   529770    42.9 |  5.414 % |
c |     62457 |   60634   146185 |   32550   12845   550332    42.8 |  5.414 % |
c |     63216 |   60634   146185 |   35805   13604   569802    41.9 |  5.414 % |
c |     64355 |   60634   146185 |   39385   14743   583727    39.6 |  5.414 % |
c |     66063 |   60634   146185 |   43324   16451   767246    46.6 |  5.414 % |
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66682 |   60608   146129 |   20202   17069   778323    45.6 |  5.414 % |
c ==============================================================================
c [1mFound solution: 23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66760 |   60612   146139 |   20204   17147   780146    45.5 |  5.414 % |
c |     66860 |   60612   146139 |   22224   17247   781845    45.3 |  5.471 % |
c |     67014 |   60612   146139 |   24446   17401   784452    45.1 |  5.471 % |
c |     67239 |   60535   145965 |   26891   17615   786874    44.7 |  5.574 % |
c |     67578 |   60302   145425 |   29580   17920   789952    44.1 |  5.938 % |
c |     68084 |   60302   145425 |   32538   18426   801824    43.5 |  5.938 % |
c |     68843 |   60302   145425 |   35792   19185   843060    43.9 |  5.938 % |
c |     69982 |   60293   145400 |   39371   20322   890672    43.8 |  5.948 % |
c |     71690 |   60293   145400 |   43309   22030  1016298    46.1 |  5.948 % |
c |     74253 |   60293   145400 |   47639   24593  1074125    43.7 |  5.948 % |
c |     78098 |   60289   145391 |   52403   28436  1190693    41.9 |  5.953 % |
c |     83865 |   60289   145391 |   57644   34203  1444973    42.2 |  5.953 % |
c |     92517 |   60253   145306 |   63408   42844  1694971    39.6 |  6.012 % |
c |    105494 |   60047   144838 |   69749   55794  2332381    41.8 |  6.297 % |
c ==============================================================================
c [1mFound solution: 22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    114352 |   60028   144805 |   20009   64564  3202241    49.6 |  6.297 % |
c |    114452 |   59997   144731 |   22009   11172   770039    68.9 |  6.450 % |
c |    114602 |   59997   144731 |   24210   11322   771368    68.1 |  6.450 % |
c |    114830 |   59960   144649 |   26631   11547   773336    67.0 |  6.494 % |
c |    115167 |   59960   144649 |   29295   11884   784223    66.0 |  6.494 % |
c |    115673 |   59960   144649 |   32224   12390   794552    64.1 |  6.494 % |
c |    116432 |   59960   144649 |   35447   13149   835274    63.5 |  6.494 % |
c |    117572 |   59960   144649 |   38991   14289   893869    62.6 |  6.494 % |
c |    119281 |   59960   144649 |   42891   15998   930340    58.2 |  6.494 % |
c |    121843 |   59960   144649 |   47180   18560  1074483    57.9 |  6.494 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    124558 |   59974   144685 |   19991   21275  1125299    52.9 |  6.494 % |
c |    124660 |   59974   144685 |   21990   21377  1126213    52.7 |  6.498 % |
c |    124810 |   59974   144685 |   24189   21527  1135521    52.7 |  6.498 % |
c |    125035 |   59974   144685 |   26608   21752  1137426    52.3 |  6.498 % |
c |    125372 |   59974   144685 |   29268   22089  1144370    51.8 |  6.498 % |
c |    125878 |   59974   144685 |   32195   22595  1175795    52.0 |  6.498 % |
c |    126638 |   59974   144685 |   35415   23355  1240158    53.1 |  6.498 % |
c |    127777 |   59974   144685 |   38956   24494  1267073    51.7 |  6.498 % |
c |    129485 |   59974   144685 |   42852   26202  1361382    52.0 |  6.498 % |
c |    132047 |   59974   144685 |   47137   28764  1411302    49.1 |  6.498 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133335 |   59978   144695 |   19992   30052  1456991    48.5 |  6.498 % |
c |    133435 |   59978   144695 |   21991   15126   258753    17.1 |  6.502 % |
c |    133585 |   59978   144695 |   24190   15276   268230    17.6 |  6.502 % |
c |    133813 |   59956   144645 |   26609   15486   270573    17.5 |  6.531 % |
c |    134152 |   59956   144645 |   29270   15825   276637    17.5 |  6.531 % |
c |    134659 |   59956   144645 |   32197   16332   289141    17.7 |  6.531 % |
c |    135420 |   59956   144645 |   35417   17093   311169    18.2 |  6.531 % |
c |    136560 |   59952   144636 |   38958   18232   347513    19.1 |  6.536 % |
c |    138268 |   59952   144636 |   42854   19940   445825    22.4 |  6.536 % |
c |    140830 |   59952   144636 |   47140   22502   601765    26.7 |  6.536 % |
c |    144675 |   59952   144636 |   51854   26347  1023261    38.8 |  6.536 % |
c |    150442 |   59952   144636 |   57039   32114  1417272    44.1 |  6.536 % |
c |    159091 |   59952   144636 |   62743   40763  2750427    67.5 |  6.536 % |
c |    172067 |   59952   144636 |   69017   53739  6052915   112.6 |  6.536 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    187191 |   60001   144761 |   20000   68863  8737878   126.9 |  6.536 % |
c |    187293 |   60001   144761 |   22000   11364  1043784    91.9 |  6.536 % |
c |    187443 |   60001   144761 |   24200   11514  1046887    90.9 |  6.536 % |
c |    187668 |   60001   144761 |   26620   11739  1049226    89.4 |  6.537 % |
c |    188008 |   59814   144326 |   29282   11859  1050553    88.6 |  6.836 % |
c |    188514 |   59814   144326 |   32210   12365  1054989    85.3 |  6.836 % |
c |    189273 |   59814   144326 |   35431   13124  1105265    84.2 |  6.836 % |
c |    190412 |   59814   144326 |   38974   14263  1156072    81.1 |  6.836 % |
c ==============================================================================
c [1mFound solution: 17[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    191662 |   59826   144358 |   19942   15513  1217239    78.5 |  6.836 % |
c |    191763 |   59826   144358 |   21936   15614  1218616    78.0 |  6.840 % |
c |    191913 |   59826   144358 |   24129   15764  1221228    77.5 |  6.840 % |
c |    192138 |   59826   144358 |   26542   15989  1225308    76.6 |  6.840 % |
c |    192476 |   59826   144358 |   29197   16327  1235282    75.7 |  6.840 % |
c |    192983 |   59826   144358 |   32116   16834  1241716    73.8 |  6.840 % |
c |    193743 |   59826   144358 |   35328   17594  1266509    72.0 |  6.840 % |
c |    194882 |   59826   144358 |   38861   18733  1346575    71.9 |  6.840 % |
c |    196591 |   59826   144358 |   42747   20442  1471062    72.0 |  6.840 % |
c |    199154 |   59826   144358 |   47022   23005  1796843    78.1 |  6.840 % |
c |    202999 |   59826   144358 |   51724   26850  1924824    71.7 |  6.840 % |
c |    208766 |   59826   144358 |   56896   32617  2959645    90.7 |  6.840 % |
c |    217416 |   59826   144358 |   62586   41267  3899271    94.5 |  6.840 % |
c |    230392 |   59826   144358 |   68845   54243  6171994   113.8 |  6.840 % |
c |    249856 |   59826   144358 |   75729   73707  9089057   123.3 |  6.840 % |
c ==============================================================================
c [1mFound solution: 16[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    255421 |   59837   144387 |   19945   79272  9706349   122.4 |  6.840 % |
c |    255522 |   59837   144387 |   21939   12239   168535    13.8 |  6.844 % |
c |    255672 |   59837   144387 |   24133   12389   170047    13.7 |  6.844 % |
c |    255897 |   59828   144367 |   26546   12613   181987    14.4 |  6.849 % |
c |    256234 |   59828   144367 |   29201   12950   188934    14.6 |  6.849 % |
c |    256740 |   59828   144367 |   32121   13456   201406    15.0 |  6.849 % |
c |    257499 |   59828   144367 |   35333   14215   210409    14.8 |  6.849 % |
c |    258638 |   59828   144367 |   38867   15354   233877    15.2 |  6.849 % |
c |    260348 |   59828   144367 |   42753   17064   387811    22.7 |  6.849 % |
c |    262911 |   59828   144367 |   47029   19627   469867    23.9 |  6.849 % |
c ==============================================================================
c [1mFound solution: 15[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    264293 |   59831   144374 |   19943   21009   512404    24.4 |  6.849 % |
c |    264393 |   59831   144374 |   21937   21109   515507    24.4 |  6.853 % |
c |    264543 |   59831   144374 |   24131   21259   517986    24.4 |  6.853 % |
c |    264769 |   59697   144065 |   26544   21466   520296    24.2 |  7.049 % |
c |    265107 |   59697   144065 |   29198   21804   528051    24.2 |  7.049 % |
c |    265613 |   59697   144065 |   32118   22310   562452    25.2 |  7.049 % |
c |    266373 |   59697   144065 |   35330   23070   586385    25.4 |  7.049 % |
c |    267512 |   59697   144065 |   38863   24209   628915    26.0 |  7.049 % |
c |    269220 |   59697   144065 |   42749   25917   845063    32.6 |  7.049 % |
c |    271783 |   59669   144000 |   47024   28472   963178    33.8 |  7.083 % |
c |    275628 |   59669   144000 |   51727   32317  1253731    38.8 |  7.083 % |
c ==============================================================================
c [1mFound solution: 14[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    279018 |   59714   144115 |   19904   35707  1361682    38.1 |  7.083 % |
c |    279118 |   59714   144115 |   21894   17954   471555    26.3 |  7.083 % |
c |    279268 |   59714   144115 |   24083   18104   474062    26.2 |  7.083 % |
c |    279493 |   59714   144115 |   26492   18329   484221    26.4 |  7.083 % |
c |    279831 |   59714   144115 |   29141   18667   490500    26.3 |  7.083 % |
c |    280337 |   59714   144115 |   32055   19173   506828    26.4 |  7.083 % |
c |    281096 |   59714   144115 |   35261   19932   568299    28.5 |  7.083 % |
c |    282235 |   59714   144115 |   38787   21071   593643    28.2 |  7.083 % |
c |    283943 |   59714   144115 |   42665   22779   627250    27.5 |  7.083 % |
c |    286505 |   59714   144115 |   46932   25341   863426    34.1 |  7.083 % |
c |    290350 |   59714   144115 |   51625   29186  1021389    35.0 |  7.083 % |
c |    296116 |   59714   144115 |   56788   34952  1594964    45.6 |  7.083 % |
c ==============================================================================
c [1mFound solution: 13[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    301823 |   59726   144147 |   19908   40659  1928552    47.4 |  7.083 % |
c |    301923 |   59726   144147 |   21898   20430   874304    42.8 |  7.087 % |
c |    302073 |   59726   144147 |   24088   20580   879106    42.7 |  7.087 % |
c |    302300 |   59726   144147 |   26497   20807   892523    42.9 |  7.087 % |
c |    302637 |   59726   144147 |   29147   21144   904610    42.8 |  7.087 % |
c |    303143 |   59726   144147 |   32062   21650   917634    42.4 |  7.087 % |
c |    303904 |   59726   144147 |   35268   22411   933036    41.6 |  7.087 % |
c |    305043 |   59726   144147 |   38795   23550  1060964    45.1 |  7.087 % |
c |    306751 |   59726   144147 |   42674   25258  1239825    49.1 |  7.087 % |
c |    309314 |   59726   144147 |   46942   27821  1400940    50.4 |  7.087 % |
c |    313158 |   59726   144147 |   51636   31665  1582133    50.0 |  7.087 % |
c |    318924 |   59726   144147 |   56799   37431  1914569    51.1 |  7.087 % |
c |    327574 |   59726   144147 |   62479   46081  2852452    61.9 |  7.087 % |
c ==============================================================================
c [1mFound solution: 12[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    330852 |   59737   144176 |   19912   49359  3112365    63.1 |  7.087 % |
c |    330952 |   59737   144176 |   21903   12440   166456    13.4 |  7.091 % |
c |    331103 |   59737   144176 |   24093   12591   167413    13.3 |  7.091 % |
c |    331329 |   59737   144176 |   26502   12817   169344    13.2 |  7.091 % |
c |    331666 |   59737   144176 |   29153   13154   182519    13.9 |  7.091 % |
c |    332172 |   59737   144176 |   32068   13660   207235    15.2 |  7.091 % |
c |    332933 |   59737   144176 |   35275   14421   232610    16.1 |  7.091 % |
c |    334072 |   59737   144176 |   38802   15560   273915    17.6 |  7.091 % |
c |    335780 |   59737   144176 |   42683   17268   480435    27.8 |  7.091 % |
c |    338342 |   59728   144156 |   46951   19829   598329    30.2 |  7.096 % |
c |    342186 |   59728   144156 |   51646   23673  1030646    43.5 |  7.096 % |
c |    347952 |   59724   144147 |   56811   29436  1372522    46.6 |  7.101 % |
c |    356602 |   59724   144147 |   62492   38086  2216539    58.2 |  7.101 % |
c |    369577 |   59724   144147 |   68741   51061  3103245    60.8 |  7.101 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.92 2/54 29752
Raw data (stat): 29752 (runsolver) R 29751 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423718019 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.0012 s]
Raw data (loadavg): 0.93 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 2244 0 0 0 993 5 0 0 25 0 1 0 423718019 11358208 2170 4294967295 134512640 134672761 3221224544 3221223744 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2773 2170 603 41 0 2732 0
vsize: 11092
[startup+20.0024 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 2396 0 0 0 1992 6 0 0 25 0 1 0 423718019 12005376 2322 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2931 2322 603 41 0 2890 0
vsize: 11724
[startup+30.0032 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 2613 0 0 0 2992 7 0 0 25 0 1 0 423718019 12881920 2539 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3145 2539 603 41 0 3104 0
vsize: 12580
[startup+40.0034 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 2856 0 0 0 3990 9 0 0 25 0 1 0 423718019 13901824 2782 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3394 2782 603 41 0 3353 0
vsize: 13576
[startup+50.0047 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3023 0 0 0 4989 10 0 0 25 0 1 0 423718019 14536704 2949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3549 2949 603 41 0 3508 0
vsize: 14196
[startup+60.0055 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3023 0 0 0 5989 10 0 0 25 0 1 0 423718019 14536704 2949 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3549 2949 603 41 0 3508 0
vsize: 14196
[startup+70.0056 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3131 0 0 0 6988 11 0 0 25 0 1 0 423718019 14934016 3057 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3646 3057 603 41 0 3605 0
vsize: 14584
[startup+80.0062 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3325 0 0 0 7987 11 0 0 25 0 1 0 423718019 15740928 3251 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3251 603 41 0 3802 0
vsize: 15372
[startup+90.0067 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3325 0 0 0 8987 12 0 0 25 0 1 0 423718019 15740928 3251 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3251 603 41 0 3802 0
vsize: 15372
[startup+100.007 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3325 0 0 0 9987 12 0 0 25 0 1 0 423718019 15740928 3251 4294967295 134512640 134672761 3221224544 3221223648 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3251 603 41 0 3802 0
vsize: 15372
[startup+110.008 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3489 0 0 0 10987 13 0 0 25 0 1 0 423718019 16412672 3415 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4007 3415 603 41 0 3966 0
vsize: 16028
[startup+120.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3489 0 0 0 11986 13 0 0 25 0 1 0 423718019 16412672 3415 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4007 3415 603 41 0 3966 0
vsize: 16028
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3523 0 0 0 12986 13 0 0 25 0 1 0 423718019 16543744 3449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4039 3449 603 41 0 3998 0
vsize: 16156
[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3523 0 0 0 13986 14 0 0 25 0 1 0 423718019 16543744 3449 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4039 3449 603 41 0 3998 0
vsize: 16156
[startup+150.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3523 0 0 0 14985 14 0 0 25 0 1 0 423718019 16543744 3449 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4039 3449 603 41 0 3998 0
vsize: 16156
[startup+160.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3524 0 0 0 15985 14 0 0 25 0 1 0 423718019 16543744 3450 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4039 3450 603 41 0 3998 0
vsize: 16156
[startup+170.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3659 0 0 0 16985 15 0 0 25 0 1 0 423718019 17084416 3585 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4171 3585 603 41 0 4130 0
vsize: 16684
[startup+180.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 3926 0 0 0 17984 16 0 0 25 0 1 0 423718019 18284544 3852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4464 3852 603 41 0 4423 0
vsize: 17856
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 4057 0 0 0 18983 17 0 0 25 0 1 0 423718019 18808832 3983 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4592 3983 603 41 0 4551 0
vsize: 18368
[startup+200.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 4232 0 0 0 19982 18 0 0 25 0 1 0 423718019 19480576 4158 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4756 4158 603 41 0 4715 0
vsize: 19024
[startup+210.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 4446 0 0 0 20981 19 0 0 25 0 1 0 423718019 20418560 4372 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4985 4372 603 41 0 4944 0
vsize: 19940
[startup+220.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 4599 0 0 0 21980 20 0 0 25 0 1 0 423718019 20946944 4525 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5114 4525 603 41 0 5073 0
vsize: 20456
[startup+230.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 4833 0 0 0 22979 21 0 0 25 0 1 0 423718019 21884928 4759 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5343 4759 603 41 0 5302 0
vsize: 21372
[startup+240.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5032 0 0 0 23978 22 0 0 25 0 1 0 423718019 22814720 4958 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 4958 603 41 0 5529 0
vsize: 22280
[startup+250.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5100 0 0 0 24978 22 0 0 25 0 1 0 423718019 23085056 5026 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5636 5026 603 41 0 5595 0
vsize: 22544
[startup+260.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5283 0 0 0 25977 23 0 0 25 0 1 0 423718019 23756800 5209 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5800 5209 603 41 0 5759 0
vsize: 23200
[startup+270.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5750 0 0 0 26975 25 0 0 25 0 1 0 423718019 25624576 5676 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6256 5676 603 41 0 6215 0
vsize: 25024
[startup+280.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 27973 26 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+290.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 28973 26 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+300.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 29973 27 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+310.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 30972 27 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+320.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 31972 27 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+330.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 32971 28 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+340.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 33971 28 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223640 134555595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+350.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 34971 28 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+360.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 35970 29 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+370.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 36970 29 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+380.019 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5963 0 0 0 37970 29 0 0 25 0 1 0 423718019 26546176 5889 4294967295 134512640 134672761 3221224544 3221223648 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5889 603 41 0 6440 0
vsize: 25924
[startup+390.02 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5964 0 0 0 38970 29 0 0 25 0 1 0 423718019 26546176 5890 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5890 603 41 0 6440 0
vsize: 25924
[startup+400.02 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5964 0 0 0 39969 30 0 0 25 0 1 0 423718019 26546176 5890 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5890 603 41 0 6440 0
vsize: 25924
[startup+410.021 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 5964 0 0 0 40969 30 0 0 25 0 1 0 423718019 26546176 5890 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6481 5890 603 41 0 6440 0
vsize: 25924
[startup+420.022 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 6217 0 0 0 41967 32 0 0 25 0 1 0 423718019 27611136 6143 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6741 6143 603 41 0 6700 0
vsize: 26964
[startup+430.022 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 6740 0 0 0 42965 34 0 0 25 0 1 0 423718019 29765632 6666 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7267 6666 603 41 0 7226 0
vsize: 29068
[startup+440.023 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 7281 0 0 0 43962 37 0 0 25 0 1 0 423718019 31911936 7207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7791 7207 603 41 0 7750 0
vsize: 31164
[startup+450.023 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 7752 0 0 0 44961 38 0 0 25 0 1 0 423718019 33918976 7678 4294967295 134512640 134672761 3221224544 3221223728 134558977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8281 7678 603 41 0 8240 0
vsize: 33124
[startup+460.024 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 8228 0 0 0 45960 39 0 0 25 0 1 0 423718019 35794944 8154 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8739 8154 603 41 0 8698 0
vsize: 34956
[startup+470.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 8708 0 0 0 46958 41 0 0 25 0 1 0 423718019 37777408 8634 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9223 8634 603 41 0 9182 0
vsize: 36892
[startup+480.024 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 9001 0 0 0 47957 41 0 0 25 0 1 0 423718019 38977536 8927 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9516 8927 603 41 0 9475 0
vsize: 38064
[startup+490.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 9268 0 0 0 48956 43 0 0 25 0 1 0 423718019 40046592 9194 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9777 9194 603 41 0 9736 0
vsize: 39108
[startup+500.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 9631 0 0 0 49955 44 0 0 25 0 1 0 423718019 41517056 9557 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10136 9557 603 41 0 10095 0
vsize: 40544
[startup+510.026 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 9996 0 0 0 50955 45 0 0 25 0 1 0 423718019 43118592 9922 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10527 9922 603 41 0 10486 0
vsize: 42108
[startup+520.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 10223 0 0 0 51954 46 0 0 25 0 1 0 423718019 44052480 10149 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10755 10149 603 41 0 10714 0
vsize: 43020
[startup+530.025 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 10552 0 0 0 52953 47 0 0 25 0 1 0 423718019 45400064 10478 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11084 10478 603 41 0 11043 0
vsize: 44336
[startup+540.026 s]
Raw data (loadavg): 1.14 1.03 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11089 0 0 0 53951 49 0 0 25 0 1 0 423718019 47779840 11015 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11665 11015 603 41 0 11624 0
vsize: 46660
[startup+550.025 s]
Raw data (loadavg): 1.12 1.03 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11647 0 0 0 54950 50 0 0 25 0 1 0 423718019 50049024 11573 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12219 11573 603 41 0 12178 0
vsize: 48876
[startup+560.026 s]
Raw data (loadavg): 1.10 1.03 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 55950 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+570.026 s]
Raw data (loadavg): 1.09 1.03 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 56950 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+580.025 s]
Raw data (loadavg): 1.07 1.03 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 57950 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+590.026 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 58951 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+600.025 s]
Raw data (loadavg): 1.05 1.02 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 59951 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+610.026 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 60951 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+620.026 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 61951 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+630.026 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 62951 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+640.026 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 63951 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+650.026 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 64952 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+660.027 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 65952 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+670.027 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 66952 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+680.028 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 67952 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+690.028 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 68952 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+700.028 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 69953 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+710.029 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 70953 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+720.028 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 71953 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+730.028 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 72953 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223728 134559618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+740.028 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 73953 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+750.029 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 74954 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+760.029 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 75954 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223680 134560657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+770.029 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11682 0 0 0 76954 50 0 0 25 0 1 0 423718019 50184192 11608 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12252 11608 603 41 0 12211 0
vsize: 49008
[startup+780.029 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 11727 0 0 0 77954 50 0 0 25 0 1 0 423718019 50450432 11653 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12317 11653 603 41 0 12276 0
vsize: 49268
[startup+790.029 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12132 0 0 0 78953 51 0 0 25 0 1 0 423718019 52060160 12058 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12710 12058 603 41 0 12669 0
vsize: 50840
[startup+800.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12492 0 0 0 79953 52 0 0 25 0 1 0 423718019 53534720 12418 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12418 603 41 0 13029 0
vsize: 52280
[startup+810.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12787 0 0 0 80952 53 0 0 25 0 1 0 423718019 54738944 12713 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13364 12713 603 41 0 13323 0
vsize: 53456
[startup+820.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 81952 53 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+830.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 82952 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+840.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 83952 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+850.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 84952 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+860.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 85953 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+870.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 86953 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+880.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 87953 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+890.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 88953 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223648 134560201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+900.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 89953 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+910.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 90953 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+920.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 91954 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+930.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 92954 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+940.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 93954 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+950.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 94954 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+960.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 95954 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+970.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 96954 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+980.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 97954 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+990.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 98955 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 99955 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 100955 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 101955 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 102955 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 103955 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 104956 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223680 134565036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 105956 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 106956 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 107956 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 108956 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 109956 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 110957 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 111957 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 112957 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 113957 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 114957 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223648 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 115957 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 116958 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 117958 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 118958 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29752
Raw data (stat): 29752 (minisat+) R 29751 24215 24214 0 -1 0 12903 0 0 0 119958 54 0 0 25 0 1 0 423718019 55144448 12829 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13463 12829 603 41 0 13422 0
vsize: 53852
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 29752
Raw data (stat): 29752 (minisat+) Z 29751 24215 24214 0 -1 12 12906 0 0 0 119958 57 0 0 25 0 1 0 423718019 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.07
CPU time (s): 1200.16
CPU user time (s): 1199.59
CPU system time (s): 0.571913
CPU usage (%): 100.008
Max. virtual memory (Kb): 53852
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####