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.95:98.opb
MD5SUM	ac510382bae6003fe0373ad32fd0064f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5
Optimality of the best value was proved	NO
Number of terms in the objective function	411
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	1129
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	1129
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03584
Number of variables	411
Total number of constraints	887
Number of constraints which are clauses	387
Number of constraints which are cardinality constraints (but not clauses)	500
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	16
Trace number 6465

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-14 05:07:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4880 boxname=wulflinc30 idbench=368 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ac510382bae6003fe0373ad32fd0064f  /oldhome/oroussel/tmp/wulflinc30/normalized-10:10:4.5:0.95:98.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc30/normalized-10:10:4.5:0.95:98.opb /oldhome/oroussel/tmp/wulflinc30/normalized-10:10:4.5:0.95:98.opb
IDLAUNCH: 4880
/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:        718176 kB
Buffers:         38356 kB
Cached:         237384 kB
SwapCached:          0 kB
Active:          84816 kB
Inactive:       193852 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        717924 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32096 kB
Committed_AS:    63516 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:27:57 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4880 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 476 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:    5
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   17
c ---[  81]---> BDD-cost:   21
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   17
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   17
c ---[  74]---> BDD-cost:   23
c ---[  73]---> BDD-cost:   26
c ---[  72]---> BDD-cost:   26
c ---[  71]---> BDD-cost:   32
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:   14
c ---[  68]---> BDD-cost:   20
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   23
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   29
c ---[  61]---> BDD-cost:   32
c ---[  60]---> BDD-cost:   35
c ---[  59]---> BDD-cost:   23
c ---[  58]---> BDD-cost:   23
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   26
c ---[  53]---> BDD-cost:   29
c ---[  52]---> BDD-cost:   32
c ---[  51]---> BDD-cost:   41
c ---[  50]---> BDD-cost:   38
c ---[  49]---> BDD-cost:   26
c ---[  48]---> BDD-cost:   24
c ---[  47]---> BDD-cost:   20
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   29
c ---[  42]---> BDD-cost:   32
c ---[  41]---> BDD-cost:   38
c ---[  40]---> BDD-cost:   32
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   29
c ---[  37]---> BDD-cost:   23
c ---[  36]---> BDD-cost:    7
c ---[  35]---> BDD-cost:   20
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   32
c ---[  30]---> BDD-cost:   29
c ---[  29]---> BDD-cost:   23
c ---[  28]---> BDD-cost:   23
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   23
c ---[  22]---> BDD-cost:   29
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   23
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   17
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   23
c ---[  12]---> BDD-cost:   20
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   11
c ---[   9]---> BDD-cost:   11
c ---[   6]---> BDD-cost:    7
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8667    24202 |    2889       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 333[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23128     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   66599   159796 |   22199       0        0     nan |  0.000 % |
c |       105 |   66599   159796 |   24418     105      635     6.0 |  0.427 % |
c |       255 |   66588   159772 |   26860     254     2144     8.4 |  0.441 % |
c |       481 |   66331   159194 |   29546     425     3896     9.2 |  0.775 % |
c |       818 |   66209   158919 |   32501     761     5706     7.5 |  0.925 % |
c ==============================================================================
c [1mFound solution: 70[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 |       891 |   68220   163739 |   22740     832     6280     7.5 |  0.925 % |
c |       992 |   68094   163455 |   25014     932     8039     8.6 |  1.208 % |
c |      1144 |   68094   163455 |   27515    1084     9284     8.6 |  1.208 % |
c |      1369 |   68039   163330 |   30266    1307    12331     9.4 |  1.445 % |
c |      1706 |   67475   162040 |   33293    1636    15027     9.2 |  2.028 % |
c |      2212 |   67471   162031 |   36622    2140    30531    14.3 |  2.033 % |
c ==============================================================================
c [1mFound solution: 66[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 |      2708 |   67257   161561 |   22419    2632    39963    15.2 |  2.033 % |
c |      2810 |   67207   161450 |   24660    2732    40610    14.9 |  2.472 % |
c |      2961 |   67207   161450 |   27126    2883    41795    14.5 |  2.472 % |
c |      3186 |   67207   161450 |   29839    3108    42856    13.8 |  2.472 % |
c |      3524 |   67207   161450 |   32823    3446    46932    13.6 |  2.472 % |
c ==============================================================================
c [1mFound solution: 54[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 |      3814 |   67320   161738 |   22440    3732    52364    14.0 |  2.472 % |
c |      3916 |   67320   161738 |   24684    3834    53827    14.0 |  2.518 % |
c |      4066 |   67195   161448 |   27152    3981    56085    14.1 |  2.704 % |
c |      4292 |   66992   160981 |   29867    4199    59784    14.2 |  2.986 % |
c |      4629 |   66992   160981 |   32854    4536    63650    14.0 |  2.986 % |
c ==============================================================================
c [1mFound solution: 52[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 |      4923 |   67056   161146 |   22352    4830    69230    14.3 |  2.986 % |
c |      5023 |   67056   161146 |   24587    4930    70580    14.3 |  2.988 % |
c |      5173 |   67056   161146 |   27045    5080    71680    14.1 |  2.988 % |
c |      5398 |   66991   161000 |   29750    5301    75371    14.2 |  3.065 % |
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 |      5677 |   66776   160509 |   22258    5562    77649    14.0 |  3.065 % |
c |      5778 |   66776   160509 |   24483    5663    78696    13.9 |  3.392 % |
c |      5928 |   66776   160509 |   26932    5813    80234    13.8 |  3.392 % |
c |      6153 |   66717   160372 |   29625    6035    82043    13.6 |  3.478 % |
c |      6492 |   66717   160372 |   32587    6374    85467    13.4 |  3.478 % |
c ==============================================================================
c [1mFound solution: 49[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 |      6536 |   66721   160382 |   22240    6418    86684    13.5 |  3.478 % |
c |      6636 |   66645   160210 |   24464    6516    87572    13.4 |  3.582 % |
c |      6786 |   66645   160210 |   26910    6666    89509    13.4 |  3.582 % |
c |      7011 |   66605   160120 |   29601    6890    93049    13.5 |  3.637 % |
c |      7348 |   66449   159763 |   32561    7224    96831    13.4 |  3.845 % |
c |      7854 |   66449   159763 |   35817    7730   108885    14.1 |  3.846 % |
c |      8616 |   66449   159763 |   39399    8492   121976    14.4 |  3.845 % |
c |      9756 |   66449   159763 |   43339    9632   142538    14.8 |  3.845 % |
c ==============================================================================
c [1mFound solution: 48[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 |     10011 |   66502   159901 |   22167    9887   148152    15.0 |  3.845 % |
c |     10111 |   66502   159901 |   24383    9987   148961    14.9 |  3.847 % |
c |     10261 |   66502   159901 |   26822   10137   149956    14.8 |  3.847 % |
c |     10488 |   66502   159901 |   29504   10364   153363    14.8 |  3.847 % |
c |     10825 |   66502   159901 |   32454   10701   156278    14.6 |  3.847 % |
c |     11334 |   66502   159901 |   35700   11210   163936    14.6 |  3.847 % |
c |     12093 |   66502   159901 |   39270   11969   175586    14.7 |  3.847 % |
c |     13232 |   66502   159901 |   43197   13108   220269    16.8 |  3.847 % |
c |     14940 |   66502   159901 |   47516   14816   259644    17.5 |  3.847 % |
c ==============================================================================
c [1mFound solution: 47[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 |     16015 |   66212   159239 |   22070   15412   271401    17.6 |  3.847 % |
c |     16115 |   66212   159239 |   24277   15512   272344    17.6 |  4.269 % |
c |     16265 |   66192   159193 |   26704   15660   276747    17.7 |  4.296 % |
c |     16490 |   66133   159058 |   29375   15880   280954    17.7 |  4.378 % |
c |     16827 |   66127   159044 |   32312   16216   286353    17.7 |  4.387 % |
c |     17335 |   66117   159021 |   35543   16723   293219    17.5 |  4.400 % |
c |     18094 |   65968   158679 |   39098   17469   312586    17.9 |  4.604 % |
c |     19233 |   65954   158647 |   43008   18603   346076    18.6 |  4.623 % |
c ==============================================================================
c [1mFound solution: 46[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 |     19729 |   65913   158554 |   21971   19093   353668    18.5 |  4.623 % |
c |     19829 |   65913   158554 |   24168   19193   356187    18.6 |  4.695 % |
c |     19979 |   65913   158554 |   26584   19343   364339    18.8 |  4.695 % |
c |     20206 |   65754   158188 |   29243   19564   366860    18.8 |  4.921 % |
c |     20544 |   65754   158188 |   32167   19902   371817    18.7 |  4.921 % |
c |     21050 |   65754   158188 |   35384   20408   379447    18.6 |  4.921 % |
c |     21810 |   65754   158188 |   38922   21168   391397    18.5 |  4.921 % |
c ==============================================================================
c [1mFound solution: 45[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 |     21999 |   65758   158198 |   21919   21357   399125    18.7 |  4.921 % |
c |     22100 |   65758   158198 |   24110   21458   401388    18.7 |  4.925 % |
c |     22250 |   65758   158198 |   26521   21608   406433    18.8 |  4.925 % |
c |     22475 |   65618   157879 |   29174   21822   411801    18.9 |  5.107 % |
c |     22812 |   65606   157851 |   32091   22158   423009    19.1 |  5.125 % |
c |     23318 |   65543   157707 |   35300   22660   436165    19.2 |  5.211 % |
c |     24081 |   65543   157707 |   38830   23423   524130    22.4 |  5.211 % |
c ==============================================================================
c [1mFound solution: 43[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 |     25102 |   65553   157749 |   21851   24430   542174    22.2 |  5.211 % |
c |     25202 |   65553   157749 |   24036   12315   256372    20.8 |  5.284 % |
c |     25352 |   65553   157749 |   26439   12465   257941    20.7 |  5.284 % |
c |     25579 |   65553   157749 |   29083   12692   261636    20.6 |  5.284 % |
c |     25916 |   65553   157749 |   31992   13029   266047    20.4 |  5.284 % |
c |     26422 |   65553   157749 |   35191   13535   281031    20.8 |  5.284 % |
c |     27181 |   65553   157749 |   38710   14294   294095    20.6 |  5.284 % |
c |     28320 |   65553   157749 |   42581   15433   437850    28.4 |  5.284 % |
c |     30028 |   65553   157749 |   46839   17141   473852    27.6 |  5.284 % |
c |     32590 |   65553   157749 |   51523   19703   535078    27.2 |  5.284 % |
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 |     36018 |   65560   157770 |   21853   23123   657978    28.5 |  5.284 % |
c |     36118 |   65560   157770 |   24038   11662   211248    18.1 |  5.296 % |
c |     36268 |   65560   157770 |   26442   11812   213456    18.1 |  5.296 % |
c |     36493 |   65560   157770 |   29086   12037   218393    18.1 |  5.296 % |
c |     36830 |   65560   157770 |   31994   12374   226595    18.3 |  5.296 % |
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 |     37294 |   65564   157780 |   21854   12838   235772    18.4 |  5.296 % |
c |     37394 |   65564   157780 |   24039   12938   238001    18.4 |  5.300 % |
c |     37544 |   65564   157780 |   26443   13088   239964    18.3 |  5.300 % |
c |     37769 |   65564   157780 |   29087   13313   264292    19.9 |  5.300 % |
c |     38107 |   65564   157780 |   31996   13651   267937    19.6 |  5.300 % |
c |     38613 |   65564   157780 |   35196   14157   279867    19.8 |  5.300 % |
c ==============================================================================
c [1mFound solution: 40[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 |     39314 |   65617   157918 |   21872   14858   292760    19.7 |  5.300 % |
c |     39416 |   65590   157856 |   24059   14958   294648    19.7 |  5.342 % |
c |     39567 |   65590   157856 |   26465   15109   296169    19.6 |  5.342 % |
c |     39792 |   65590   157856 |   29111   15334   301655    19.7 |  5.342 % |
c ==============================================================================
c [1mFound solution: 39[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 |     40036 |   65603   157891 |   21867   15578   304709    19.6 |  5.342 % |
c |     40136 |   65603   157891 |   24053   15678   306512    19.6 |  5.346 % |
c |     40286 |   65603   157891 |   26459   15828   312054    19.7 |  5.346 % |
c |     40511 |   65603   157891 |   29104   16053   313521    19.5 |  5.346 % |
c |     40848 |   65603   157891 |   32015   16390   322519    19.7 |  5.346 % |
c |     41354 |   65603   157891 |   35217   16896   331332    19.6 |  5.346 % |
c |     42116 |   65472   157590 |   38738   17502   356315    20.4 |  5.522 % |
c |     43255 |   65472   157590 |   42612   18641   382859    20.5 |  5.523 % |
c ==============================================================================
c [1mFound solution: 38[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 |     43625 |   65484   157622 |   21828   19011   405454    21.3 |  5.523 % |
c |     43725 |   65484   157622 |   24010   19111   406309    21.3 |  5.526 % |
c |     43875 |   65484   157622 |   26411   19261   409591    21.3 |  5.526 % |
c |     44101 |   65402   157434 |   29053   19463   412364    21.2 |  5.635 % |
c |     44439 |   65402   157434 |   31958   19801   419673    21.2 |  5.635 % |
c |     44946 |   65402   157434 |   35154   20308   437526    21.5 |  5.635 % |
c ==============================================================================
c [1mFound solution: 36[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 |     45074 |   65465   157596 |   21821   20436   442204    21.6 |  5.635 % |
c |     45176 |   65465   157596 |   24003   20538   444515    21.6 |  5.635 % |
c |     45326 |   65465   157596 |   26403   20688   446082    21.6 |  5.635 % |
c |     45552 |   65465   157596 |   29043   20914   448373    21.4 |  5.635 % |
c |     45889 |   65465   157596 |   31948   21251   460973    21.7 |  5.635 % |
c |     46396 |   65355   157340 |   35142   21753   466677    21.5 |  5.802 % |
c |     47157 |   65355   157340 |   38657   22514   493508    21.9 |  5.802 % |
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 |     47598 |   65368   157375 |   21789   22955   499437    21.8 |  5.802 % |
c |     47698 |   65368   157375 |   23967   23055   503645    21.8 |  5.806 % |
c |     47848 |   65368   157375 |   26364   23205   505950    21.8 |  5.806 % |
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 |     47948 |   65380   157407 |   21793   23305   509583    21.9 |  5.806 % |
c |     48049 |   65354   157346 |   23972   11753   165979    14.1 |  5.850 % |
c |     48199 |   65354   157346 |   26369   11903   168405    14.1 |  5.850 % |
c |     48425 |   65213   157019 |   29006   12122   170191    14.0 |  6.058 % |
c |     48766 |   65213   157019 |   31907   12463   178280    14.3 |  6.058 % |
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 |     48860 |   65217   157029 |   21739   12557   181689    14.5 |  6.058 % |
c |     48960 |   65217   157029 |   23912   12657   183350    14.5 |  6.062 % |
c |     49110 |   65217   157029 |   26304   12807   184379    14.4 |  6.062 % |
c |     49338 |   65217   157029 |   28934   13035   190232    14.6 |  6.062 % |
c |     49679 |   65191   156970 |   31828   13375   195123    14.6 |  6.098 % |
c |     50186 |   65191   156970 |   35010   13882   208361    15.0 |  6.098 % |
c |     50945 |   65191   156970 |   38511   14641   231094    15.8 |  6.098 % |
c |     52084 |   65191   156970 |   42363   15780   279585    17.7 |  6.098 % |
c |     53793 |   65191   156970 |   46599   17489   458067    26.2 |  6.098 % |
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 |     54587 |   65244   157108 |   21748   18283   495088    27.1 |  6.098 % |
c |     54687 |   65244   157108 |   23922   18383   497183    27.0 |  6.099 % |
c |     54837 |   65244   157108 |   26315   18533   500413    27.0 |  6.099 % |
c |     55062 |   65220   157053 |   28946   18747   502918    26.8 |  6.130 % |
c |     55399 |   65220   157053 |   31841   19084   510385    26.7 |  6.130 % |
c |     55905 |   65220   157053 |   35025   19590   538144    27.5 |  6.130 % |
c |     56666 |   65220   157053 |   38527   20351   556771    27.4 |  6.130 % |
c |     57805 |   65220   157053 |   42380   21490   582152    27.1 |  6.130 % |
c |     59513 |   65220   157053 |   46618   23198   654271    28.2 |  6.130 % |
c |     62075 |   65220   157053 |   51280   25760   801509    31.1 |  6.130 % |
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 |     64622 |   65233   157088 |   21744   28307   962413    34.0 |  6.130 % |
c |     64722 |   65233   157088 |   23918   14254   408268    28.6 |  6.134 % |
c |     64872 |   65233   157088 |   26310   14404   410991    28.5 |  6.134 % |
c |     65099 |   65233   157088 |   28941   14631   415385    28.4 |  6.134 % |
c |     65436 |   65233   157088 |   31835   14968   419002    28.0 |  6.134 % |
c |     65945 |   65233   157088 |   35018   15477   424294    27.4 |  6.134 % |
c |     66704 |   65233   157088 |   38520   16236   440290    27.1 |  6.134 % |
c |     67847 |   65233   157088 |   42372   17379   565127    32.5 |  6.134 % |
c |     69556 |   65088   156750 |   46610   19073   610723    32.0 |  6.351 % |
c |     72118 |   65088   156750 |   51271   21635   723139    33.4 |  6.351 % |
c |     75962 |   65088   156750 |   56398   25479  1174893    46.1 |  6.351 % |
c |     81730 |   65024   156606 |   62038   31221  1399380    44.8 |  6.428 % |
c ==============================================================================
c [1mFound solution: 30[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 |     82947 |   65036   156638 |   21678   32438  1471636    45.4 |  6.428 % |
c |     83049 |   65036   156638 |   23845   16321   543600    33.3 |  6.431 % |
c |     83200 |   65036   156638 |   26230   16472   544825    33.1 |  6.431 % |
c |     83425 |   65036   156638 |   28853   16697   546542    32.7 |  6.431 % |
c |     83762 |   65026   156616 |   31738   17033   553642    32.5 |  6.436 % |
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 |     83882 |   65029   156623 |   21676   17153   556884    32.5 |  6.436 % |
c |     83982 |   65029   156623 |   23843   17253   558828    32.4 |  6.440 % |
c |     84134 |   65029   156623 |   26227   17405   565762    32.5 |  6.440 % |
c |     84359 |   65029   156623 |   28850   17630   572372    32.5 |  6.440 % |
c |     84696 |   65029   156623 |   31735   17967   581109    32.3 |  6.440 % |
c |     85204 |   65029   156623 |   34909   18475   593495    32.1 |  6.440 % |
c |     85964 |   65029   156623 |   38400   19235   632379    32.9 |  6.440 % |
c |     87103 |   65029   156623 |   42240   20374   770862    37.8 |  6.440 % |
c |     88812 |   64959   156462 |   46464   22045   791920    35.9 |  6.512 % |
c |     91374 |   64959   156462 |   51110   24607   881173    35.8 |  6.512 % |
c ==============================================================================
c [1mFound solution: 28[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 |     92675 |   65020   156618 |   21673   25908   919392    35.5 |  6.512 % |
c |     92777 |   65020   156618 |   23840   13056   168628    12.9 |  6.511 % |
c |     92927 |   65020   156618 |   26224   13206   170098    12.9 |  6.511 % |
c |     93153 |   65020   156618 |   28846   13432   173709    12.9 |  6.511 % |
c |     93492 |   65020   156618 |   31731   13771   194148    14.1 |  6.511 % |
c |     94000 |   65020   156618 |   34904   14279   204599    14.3 |  6.511 % |
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 |     94298 |   65033   156653 |   21677   14577   212395    14.6 |  6.511 % |
c |     94398 |   65033   156653 |   23844   14677   213328    14.5 |  6.515 % |
c |     94548 |   65033   156653 |   26229   14827   216897    14.6 |  6.515 % |
c |     94773 |   65033   156653 |   28852   15052   224359    14.9 |  6.515 % |
c |     95110 |   65033   156653 |   31737   15389   253873    16.5 |  6.515 % |
c |     95617 |   65033   156653 |   34911   15896   295852    18.6 |  6.515 % |
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 |     96107 |   65039   156671 |   21679   16379   305673    18.7 |  6.515 % |
c |     96207 |   65039   156671 |   23846   16479   307089    18.6 |  6.527 % |
c |     96357 |   65039   156671 |   26231   16629   310993    18.7 |  6.527 % |
c |     96582 |   65039   156671 |   28854   16854   313000    18.6 |  6.527 % |
c |     96920 |   65039   156671 |   31740   17192   317975    18.5 |  6.527 % |
c |     97426 |   65039   156671 |   34914   17698   324298    18.3 |  6.527 % |
c |     98186 |   65039   156671 |   38405   18458   343713    18.6 |  6.527 % |
c |     99326 |   65039   156671 |   42246   19598   392086    20.0 |  6.527 % |
c |    101035 |   65039   156671 |   46470   21307   446335    20.9 |  6.527 % |
c |    103597 |   65039   156671 |   51117   23869   613408    25.7 |  6.527 % |
c |    107442 |   65029   156649 |   56229   27713   894776    32.3 |  6.532 % |
c |    113209 |   64927   156415 |   61852   33470  1390497    41.5 |  6.672 % |
c |    121859 |   64927   156415 |   68037   42120  2279402    54.1 |  6.672 % |
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 |    122062 |   64979   156550 |   21659   42323  2284361    54.0 |  6.672 % |
c |    122163 |   64979   156550 |   23824   21263  1098255    51.7 |  6.672 % |
c |    122315 |   64979   156550 |   26207   21415  1100197    51.4 |  6.672 % |
c |    122540 |   64979   156550 |   28828   21640  1103608    51.0 |  6.672 % |
c |    122877 |   64979   156550 |   31710   21977  1126154    51.2 |  6.672 % |
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 |    123293 |   64992   156585 |   21664   22393  1135401    50.7 |  6.672 % |
c |    123393 |   64992   156585 |   23830   22493  1140290    50.7 |  6.675 % |
c |    123543 |   64992   156585 |   26213   22643  1143127    50.5 |  6.675 % |
c |    123768 |   64992   156585 |   28834   22868  1171144    51.2 |  6.675 % |
c |    124105 |   64992   156585 |   31718   23205  1196672    51.6 |  6.675 % |
c |    124612 |   64992   156585 |   34890   23712  1202935    50.7 |  6.675 % |
c |    125371 |   64992   156585 |   38379   24471  1211407    49.5 |  6.675 % |
c |    126510 |   64992   156585 |   42217   25610  1309687    51.1 |  6.675 % |
c |    128218 |   64992   156585 |   46438   27318  1374245    50.3 |  6.675 % |
c |    130780 |   64992   156585 |   51082   29880  1473217    49.3 |  6.675 % |
c |    134624 |   64992   156585 |   56190   33724  2055915    61.0 |  6.675 % |
c |    140390 |   64992   156585 |   61809   39490  3166806    80.2 |  6.675 % |
c |    149041 |   64992   156585 |   67990   48141  3806939    79.1 |  6.675 % |
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 |    153394 |   65004   156617 |   21668   52494  3963231    75.5 |  6.675 % |
c |    153494 |   65004   156617 |   23834   22596   809290    35.8 |  6.679 % |
c |    153644 |   65004   156617 |   26218   22746   810979    35.7 |  6.679 % |
c |    153869 |   65004   156617 |   28840   22971   819523    35.7 |  6.679 % |
c |    154206 |   65004   156617 |   31724   23308   827362    35.5 |  6.679 % |
c |    154712 |   65004   156617 |   34896   23814   838844    35.2 |  6.679 % |
c |    155471 |   65004   156617 |   38386   24573   862864    35.1 |  6.679 % |
c ==============================================================================
c [1mFound solution: 21[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 |    155981 |   65008   156627 |   21669   25083   878962    35.0 |  6.679 % |
c |    156082 |   65008   156627 |   23835   12643   120670     9.5 |  6.683 % |
c |    156232 |   65008   156627 |   26219   12793   125282     9.8 |  6.683 % |
c |    156457 |   65008   156627 |   28841   13018   127639     9.8 |  6.683 % |
c |    156794 |   65008   156627 |   31725   13355   136915    10.3 |  6.683 % |
c |    157300 |   64976   156552 |   34898   13845   148436    10.7 |  6.732 % |
c |    158059 |   64976   156552 |   38387   14604   168654    11.5 |  6.732 % |
c |    159198 |   64976   156552 |   42226   15743   276705    17.6 |  6.732 % |
c |    160907 |   64976   156552 |   46449   17452   327027    18.7 |  6.732 % |
c |    163470 |   64976   156552 |   51094   20015   404398    20.2 |  6.732 % |
c |    167315 |   64976   156552 |   56203   23860   479876    20.1 |  6.732 % |
c |    173081 |   64976   156552 |   61824   29626   807887    27.3 |  6.732 % |
c |    181732 |   64976   156552 |   68006   38277  1842714    48.1 |  6.732 % |
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 |    185869 |   65037   156708 |   21679   42414  2338340    55.1 |  6.732 % |
c |    185969 |   65037   156708 |   23846   21307  1444658    67.8 |  6.732 % |
c |    186119 |   65037   156708 |   26231   21457  1446774    67.4 |  6.732 % |
c |    186344 |   65037   156708 |   28854   21682  1450983    66.9 |  6.732 % |
c |    186681 |   65037   156708 |   31740   22019  1463215    66.5 |  6.732 % |
c |    187188 |   65037   156708 |   34914   22526  1483512    65.9 |  6.732 % |
c |    187947 |   65037   156708 |   38405   23285  1495517    64.2 |  6.732 % |
c |    189086 |   65037   156708 |   42246   24424  1565071    64.1 |  6.732 % |
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 |    190560 |   65050   156743 |   21683   25898  1610697    62.2 |  6.732 % |
c |    190662 |   65050   156743 |   23851   13051   140572    10.8 |  6.735 % |
c |    190813 |   65050   156743 |   26236   13202   143363    10.9 |  6.735 % |
c |    191038 |   65050   156743 |   28860   13427   147920    11.0 |  6.735 % |
c |    191375 |   65050   156743 |   31746   13764   151573    11.0 |  6.735 % |
c |    191881 |   65050   156743 |   34920   14270   181133    12.7 |  6.735 % |
c |    192640 |   65050   156743 |   38412   15029   205073    13.6 |  6.735 % |
c |    193780 |   64703   155951 |   42254   16112   269984    16.8 |  7.177 % |
c |    195490 |   64703   155951 |   46479   17822   381970    21.4 |  7.176 % |
c |    198053 |   64703   155951 |   51127   20385   846622    41.5 |  7.176 % |
c |    201899 |   64703   155951 |   56240   24231  1192748    49.2 |  7.176 % |
c |    207665 |   64703   155951 |   61864   29997  1413134    47.1 |  7.176 % |
c |    216316 |   64703   155951 |   68050   38648  3239349    83.8 |  7.176 % |
c |    229290 |   64682   155898 |   74855   51615  4392565    85.1 |  7.208 % |
c |    248751 |   64611   155732 |   82341   70991  7620802   107.3 |  7.311 % |
c |    277943 |   64611   155732 |   90575   25519  3410860   133.7 |  7.311 % |
c |    321733 |   64611   155732 |   99632   69309  6632911    95.7 |  7.311 % |
#### 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.93 2/54 19504
Raw data (stat): 19504 (runsolver) R 19503 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481946712 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.0008 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 2356 0 0 0 992 6 0 0 25 0 1 0 481946712 11800576 2276 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2881 2276 603 41 0 2840 0
vsize: 11524
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 2520 0 0 0 1991 7 0 0 25 0 1 0 481946712 12537856 2440 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3061 2440 603 41 0 3020 0
vsize: 12244
[startup+30.0027 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 2704 0 0 0 2990 8 0 0 25 0 1 0 481946712 13279232 2624 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3242 2624 603 41 0 3201 0
vsize: 12968
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 2822 0 0 0 3990 8 0 0 25 0 1 0 481946712 13803520 2742 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3370 2742 603 41 0 3329 0
vsize: 13480
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 2959 0 0 0 4990 8 0 0 25 0 1 0 481946712 14340096 2879 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3501 2879 603 41 0 3460 0
vsize: 14004
[startup+60.0041 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 2963 0 0 0 5990 8 0 0 25 0 1 0 481946712 14340096 2883 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3501 2883 603 41 0 3460 0
vsize: 14004
[startup+70.0045 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 3114 0 0 0 6989 9 0 0 25 0 1 0 481946712 14970880 3034 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3655 3034 603 41 0 3614 0
vsize: 14620
[startup+80.0056 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 3114 0 0 0 7989 9 0 0 25 0 1 0 481946712 14970880 3034 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3655 3034 603 41 0 3614 0
vsize: 14620
[startup+90.0054 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 3114 0 0 0 8989 10 0 0 25 0 1 0 481946712 14970880 3034 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3655 3034 603 41 0 3614 0
vsize: 14620
[startup+100.006 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 3114 0 0 0 9989 10 0 0 25 0 1 0 481946712 14970880 3034 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3655 3034 603 41 0 3614 0
vsize: 14620
[startup+110.007 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 3115 0 0 0 10990 10 0 0 25 0 1 0 481946712 14970880 3035 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3655 3035 603 41 0 3614 0
vsize: 14620
[startup+120.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 3278 0 0 0 11989 10 0 0 25 0 1 0 481946712 15646720 3198 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3198 603 41 0 3779 0
vsize: 15280
[startup+130.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 3516 0 0 0 12989 11 0 0 25 0 1 0 481946712 16584704 3436 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4049 3436 603 41 0 4008 0
vsize: 16196
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 3516 0 0 0 13989 11 0 0 25 0 1 0 481946712 16584704 3436 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4049 3436 603 41 0 4008 0
vsize: 16196
[startup+150.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 3530 0 0 0 14989 11 0 0 25 0 1 0 481946712 16584704 3450 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4049 3450 603 41 0 4008 0
vsize: 16196
[startup+160.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 3873 0 0 0 15988 12 0 0 25 0 1 0 481946712 18051072 3793 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4407 3793 603 41 0 4366 0
vsize: 17628
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 4098 0 0 0 16988 12 0 0 25 0 1 0 481946712 18972672 4018 4294967295 134512640 134672761 3221224544 3221223876 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4632 4018 603 41 0 4591 0
vsize: 18528
[startup+180.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 4098 0 0 0 17988 12 0 0 25 0 1 0 481946712 18972672 4018 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4632 4018 603 41 0 4591 0
vsize: 18528
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 4099 0 0 0 18988 13 0 0 25 0 1 0 481946712 18972672 4019 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4632 4019 603 41 0 4591 0
vsize: 18528
[startup+200.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 4099 0 0 0 19988 13 0 0 25 0 1 0 481946712 18972672 4019 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4632 4019 603 41 0 4591 0
vsize: 18528
[startup+210.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 4099 0 0 0 20988 13 0 0 25 0 1 0 481946712 18972672 4019 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4632 4019 603 41 0 4591 0
vsize: 18528
[startup+220.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 4099 0 0 0 21988 13 0 0 25 0 1 0 481946712 18972672 4019 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4632 4019 603 41 0 4591 0
vsize: 18528
[startup+230.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 4099 0 0 0 22989 13 0 0 25 0 1 0 481946712 18972672 4019 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4632 4019 603 41 0 4591 0
vsize: 18528
[startup+240.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 4133 0 0 0 23989 13 0 0 25 0 1 0 481946712 19234816 4053 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4696 4053 603 41 0 4655 0
vsize: 18784
[startup+250.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 4485 0 0 0 24988 14 0 0 25 0 1 0 481946712 20709376 4405 4294967295 134512640 134672761 3221224544 3221223712 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5056 4405 603 41 0 5015 0
vsize: 20224
[startup+260.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 4820 0 0 0 25986 15 0 0 25 0 1 0 481946712 22052864 4740 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5384 4740 603 41 0 5343 0
vsize: 21536
[startup+270.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 5040 0 0 0 26986 16 0 0 25 0 1 0 481946712 22843392 4960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5577 4960 603 41 0 5536 0
vsize: 22308
[startup+280.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 5040 0 0 0 27986 16 0 0 25 0 1 0 481946712 22843392 4960 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5577 4960 603 41 0 5536 0
vsize: 22308
[startup+290.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 5040 0 0 0 28986 16 0 0 25 0 1 0 481946712 22843392 4960 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5577 4960 603 41 0 5536 0
vsize: 22308
[startup+300.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 5040 0 0 0 29986 16 0 0 25 0 1 0 481946712 22843392 4960 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5577 4960 603 41 0 5536 0
vsize: 22308
[startup+310.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 5040 0 0 0 30986 16 0 0 25 0 1 0 481946712 22843392 4960 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5577 4960 603 41 0 5536 0
vsize: 22308
[startup+320.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 5208 0 0 0 31986 17 0 0 25 0 1 0 481946712 23646208 5128 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5773 5128 603 41 0 5732 0
vsize: 23092
[startup+330.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 5620 0 0 0 32985 18 0 0 25 0 1 0 481946712 25260032 5540 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5540 603 41 0 6126 0
vsize: 24668
[startup+340.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 5998 0 0 0 33984 19 0 0 25 0 1 0 481946712 26869760 5918 4294967295 134512640 134672761 3221224544 3221223728 134558771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6560 5918 603 41 0 6519 0
vsize: 26240
[startup+350.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6208 0 0 0 34984 20 0 0 25 0 1 0 481946712 27676672 6128 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6757 6128 603 41 0 6716 0
vsize: 27028
[startup+360.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6441 0 0 0 35983 21 0 0 25 0 1 0 481946712 28606464 6361 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6984 6361 603 41 0 6943 0
vsize: 27936
[startup+370.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6692 0 0 0 36981 22 0 0 25 0 1 0 481946712 29679616 6612 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7246 6612 603 41 0 7205 0
vsize: 28984
[startup+380.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6789 0 0 0 37981 22 0 0 25 0 1 0 481946712 30085120 6709 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7345 6709 603 41 0 7304 0
vsize: 29380
[startup+390.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 38981 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+400.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 39981 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+410.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 40981 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+420.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 41982 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+430.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 42982 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+440.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 43982 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+450.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 44982 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+460.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 45982 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+470.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 46982 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+480.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 47983 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+490.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 48983 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+500.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 49983 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+510.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 50983 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+520.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6861 0 0 0 51983 23 0 0 25 0 1 0 481946712 30326784 6781 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6781 603 41 0 7363 0
vsize: 29616
[startup+530.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6862 0 0 0 52983 24 0 0 25 0 1 0 481946712 30326784 6782 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6782 603 41 0 7363 0
vsize: 29616
[startup+540.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6862 0 0 0 53983 24 0 0 25 0 1 0 481946712 30326784 6782 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6782 603 41 0 7363 0
vsize: 29616
[startup+550.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6862 0 0 0 54984 24 0 0 25 0 1 0 481946712 30326784 6782 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6782 603 41 0 7363 0
vsize: 29616
[startup+560.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6862 0 0 0 55984 24 0 0 25 0 1 0 481946712 30326784 6782 4294967295 134512640 134672761 3221224544 3221223648 134555114 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6782 603 41 0 7363 0
vsize: 29616
[startup+570.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6862 0 0 0 56984 24 0 0 25 0 1 0 481946712 30326784 6782 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6782 603 41 0 7363 0
vsize: 29616
[startup+580.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 6862 0 0 0 57984 24 0 0 25 0 1 0 481946712 30326784 6782 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6782 603 41 0 7363 0
vsize: 29616
[startup+590.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 7074 0 0 0 58984 24 0 0 25 0 1 0 481946712 31133696 6994 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 6994 603 41 0 7560 0
vsize: 30404
[startup+600.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 7356 0 0 0 59983 25 0 0 25 0 1 0 481946712 32333824 7276 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7894 7276 603 41 0 7853 0
vsize: 31576
[startup+610.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 7561 0 0 0 60983 26 0 0 25 0 1 0 481946712 33136640 7481 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8090 7481 603 41 0 8049 0
vsize: 32360
[startup+620.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 8024 0 0 0 61981 27 0 0 25 0 1 0 481946712 35000320 7944 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8545 7944 603 41 0 8504 0
vsize: 34180
[startup+630.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 8325 0 0 0 62981 28 0 0 25 0 1 0 481946712 36339712 8245 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8245 603 41 0 8831 0
vsize: 35488
[startup+640.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 8708 0 0 0 63980 29 0 0 25 0 1 0 481946712 37793792 8628 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9227 8628 603 41 0 9186 0
vsize: 36908
[startup+650.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 9069 0 0 0 64979 30 0 0 25 0 1 0 481946712 39260160 8989 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9585 8989 603 41 0 9544 0
vsize: 38340
[startup+660.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 9276 0 0 0 65979 31 0 0 25 0 1 0 481946712 40464384 9196 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9879 9196 603 41 0 9838 0
vsize: 39516
[startup+670.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 9826 0 0 0 66978 32 0 0 25 0 1 0 481946712 42610688 9746 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9746 603 41 0 10362 0
vsize: 41612
[startup+680.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 10384 0 0 0 67977 33 0 0 25 0 1 0 481946712 44875776 10304 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10956 10304 603 41 0 10915 0
vsize: 43824
[startup+690.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 10810 0 0 0 68976 34 0 0 25 0 1 0 481946712 46628864 10730 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11384 10730 603 41 0 11343 0
vsize: 45536
[startup+700.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 11101 0 0 0 69975 35 0 0 25 0 1 0 481946712 47833088 11021 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11678 11021 603 41 0 11637 0
vsize: 46712
[startup+710.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 11362 0 0 0 70975 35 0 0 25 0 1 0 481946712 48906240 11282 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11940 11282 603 41 0 11899 0
vsize: 47760
[startup+720.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 11743 0 0 0 71974 36 0 0 25 0 1 0 481946712 50503680 11663 4294967295 134512640 134672761 3221224544 3221223648 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12330 11663 603 41 0 12289 0
vsize: 49320
[startup+730.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 12102 0 0 0 72974 36 0 0 25 0 1 0 481946712 51974144 12022 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12689 12022 603 41 0 12648 0
vsize: 50756
[startup+740.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 12530 0 0 0 73973 38 0 0 25 0 1 0 481946712 53723136 12450 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13116 12450 603 41 0 13075 0
vsize: 52464
[startup+750.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 12953 0 0 0 74971 40 0 0 25 0 1 0 481946712 55336960 12873 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13510 12873 603 41 0 13469 0
vsize: 54040
[startup+760.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 13389 0 0 0 75970 41 0 0 25 0 1 0 481946712 57221120 13309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13970 13309 603 41 0 13929 0
vsize: 55880
[startup+770.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 13877 0 0 0 76969 42 0 0 25 0 1 0 481946712 59101184 13797 4294967295 134512640 134672761 3221224544 3221223648 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14429 13797 603 41 0 14388 0
vsize: 57716
[startup+780.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 14275 0 0 0 77968 43 0 0 25 0 1 0 481946712 60846080 14195 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14855 14195 603 41 0 14814 0
vsize: 59420
[startup+790.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 14762 0 0 0 78967 45 0 0 25 0 1 0 481946712 62734336 14682 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15316 14682 603 41 0 15275 0
vsize: 61264
[startup+800.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15195 0 0 0 79966 46 0 0 25 0 1 0 481946712 64602112 15115 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15772 15115 603 41 0 15731 0
vsize: 63088
[startup+810.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15597 0 0 0 80965 47 0 0 25 0 1 0 481946712 66207744 15517 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16164 15517 603 41 0 16123 0
vsize: 64656
[startup+820.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 81965 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+830.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 82965 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+840.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 83965 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+850.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 84966 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+860.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 85966 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+870.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 86966 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+880.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 87966 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+890.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 88966 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+900.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 89966 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+910.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 90966 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223680 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+920.025 s]
Raw data (loadavg): 0.99 0.98 0.93 3/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 91967 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+930.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 92967 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+940.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 93967 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+950.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 94967 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+960.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 95968 47 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+970.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 96968 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+980.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 97968 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+990.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 98967 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 99967 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 100967 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 101967 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 102967 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 103967 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 104967 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 105968 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 106968 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 107968 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 108968 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 109968 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15652 0 0 0 110968 48 0 0 25 0 1 0 481946712 66478080 15572 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15572 603 41 0 16189 0
vsize: 64920
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 15848 0 0 0 111968 49 0 0 25 0 1 0 481946712 67272704 15768 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16424 15768 603 41 0 16383 0
vsize: 65696
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 16210 0 0 0 112967 50 0 0 25 0 1 0 481946712 68759552 16130 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16787 16130 603 41 0 16746 0
vsize: 67148
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 16559 0 0 0 113966 51 0 0 25 0 1 0 481946712 70103040 16479 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17115 16479 603 41 0 17074 0
vsize: 68460
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 16944 0 0 0 114965 52 0 0 25 0 1 0 481946712 71716864 16864 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17509 16864 603 41 0 17468 0
vsize: 70036
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 17326 0 0 0 115965 53 0 0 25 0 1 0 481946712 73322496 17246 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17901 17246 603 41 0 17860 0
vsize: 71604
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 17731 0 0 0 116964 54 0 0 25 0 1 0 481946712 74928128 17651 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18293 17651 603 41 0 18252 0
vsize: 73172
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 18151 0 0 0 117963 55 0 0 25 0 1 0 481946712 76673024 18071 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18719 18071 603 41 0 18678 0
vsize: 74876
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 18599 0 0 0 118961 57 0 0 25 0 1 0 481946712 78422016 18519 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19146 18519 603 41 0 19105 0
vsize: 76584
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19504
Raw data (stat): 19504 (minisat+) R 19503 11931 11930 0 -1 0 18817 0 0 0 119961 58 0 0 25 0 1 0 481946712 79360000 18737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19375 18737 603 41 0 19334 0
vsize: 77500
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 19504
Raw data (stat): 19504 (minisat+) Z 19503 11931 11930 0 -1 12 18820 0 0 0 119961 61 0 0 25 0 1 0 481946712 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.23
CPU user time (s): 1199.61
CPU system time (s): 0.618905
CPU usage (%): 100.013
Max. virtual memory (Kb): 77500
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####