PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-pk1.opb
MD5SUM	9c5126d785c8d5465220e290c5fc25a6
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5120
Optimality of the best value was proved	NO
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	2421502
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.04
Number of variables	675
Total number of constraints	100
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	45
Minimum length of a constraint	1
Maximum length of a constraint	95
Trace number 18506

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 15:16:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17901 boxname=wulflinc3 idbench=1377 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9c5126d785c8d5465220e290c5fc25a6  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-pk1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-pk1.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-pk1.opb
IDLAUNCH: 17901
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        722024 kB
Buffers:         27068 kB
Cached:         263360 kB
SwapCached:          0 kB
Active:          32660 kB
Inactive:       260528 kB
HighTotal:      131008 kB
HighFree:        73108 kB
LowTotal:       903652 kB
LowFree:        648916 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            13816 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:36:31 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 17901 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 60 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############
c   -- Clauses(.)/Splits(s): (none)
c ---[  58]---> Adder-cost: 358   maxlim: 1151871   bits: 22/21
c ---[  56]---> Adder-cost: 382   maxlim: 1183231   bits: 22/21
c ---[  54]---> Adder-cost: 338   maxlim: 1135231   bits: 22/21
c ---[  52]---> Adder-cost: 362   maxlim: 1185791   bits: 22/21
c ---[  50]---> Adder-cost: 360   maxlim: 1161855   bits: 22/21
c ---[  48]---> Adder-cost: 354   maxlim: 1184383   bits: 22/21
c ---[  46]---> Adder-cost: 362   maxlim: 1156479   bits: 22/21
c ---[  45]---> BDD-cost:   58
c ---[  44]---> BDD-cost:   58
c ---[  43]---> BDD-cost:   58
c ---[  42]---> BDD-cost:   58
c ---[  40]---> Adder-cost: 352   maxlim: 1176959   bits: 22/21
c ---[  39]---> BDD-cost:   58
c ---[  38]---> BDD-cost:   58
c ---[  37]---> BDD-cost:   58
c ---[  36]---> BDD-cost:   58
c ---[  35]---> BDD-cost:   58
c ---[  34]---> BDD-cost:   58
c ---[  33]---> BDD-cost:   58
c ---[  32]---> BDD-cost:   58
c ---[  31]---> BDD-cost:   58
c ---[  30]---> BDD-cost:   58
c ---[  28]---> Adder-cost: 368   maxlim: 1155967   bits: 22/21
c ---[  27]---> BDD-cost:   58
c ---[  26]---> BDD-cost:   58
c ---[  25]---> BDD-cost:   58
c ---[  24]---> BDD-cost:   58
c ---[  23]---> BDD-cost:   58
c ---[  22]---> BDD-cost:   58
c ---[  21]---> BDD-cost:   58
c ---[  20]---> BDD-cost:   58
c ---[  19]---> BDD-cost:   58
c ---[  18]---> BDD-cost:   58
c ---[  16]---> Adder-cost: 362   maxlim: 1178367   bits: 22/21
c ---[  15]---> BDD-cost:   58
c ---[  14]---> BDD-cost:   58
c ---[  13]---> BDD-cost:   58
c ---[  12]---> BDD-cost:   58
c ---[  11]---> BDD-cost:   58
c ---[  10]---> BDD-cost:   58
c ---[   8]---> Adder-cost: 374   maxlim: 1184767   bits: 22/21
c ---[   6]---> Adder-cost: 348   maxlim: 1169791   bits: 22/21
c ---[   4]---> Adder-cost: 352   maxlim: 1145087   bits: 22/21
c ---[   2]---> Adder-cost: 368   maxlim: 1171455   bits: 22/21
c ---[   0]---> Adder-cost: 384   maxlim: 1175295   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   42843   145845 |   14281       0        0     nan |  0.000 % |
c |       102 |   42837   145827 |   15709     101      400     4.0 |  8.290 % |
c |       252 |   42816   145760 |   17280     248     1224     4.9 |  8.327 % |
c |       477 |   42802   145716 |   19008     471     3743     7.9 |  8.352 % |
c |       814 |   42778   145638 |   20908     805     6460     8.0 |  8.389 % |
c |      1321 |   42733   145493 |   22999    1305    10595     8.1 |  8.462 % |
c |      2080 |   42703   145397 |   25299    2060    22880    11.1 |  8.511 % |
c |      3221 |   42603   145069 |   27829    3180    40480    12.7 |  8.671 % |
c |      4930 |   42539   144863 |   30612    4876    73633    15.1 |  8.781 % |
c |      7493 |   42005   143113 |   33673    7301   125545    17.2 |  9.688 % |
c ==============================================================================
c [1mFound solution: 737408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10888 |   41839   142555 |   13946   10642   200136    18.8 |  9.688 % |
c |     10989 |   41839   142555 |   15340   10743   203877    19.0 | 10.012 % |
c |     11139 |   41789   142391 |   16874   10881   207057    19.0 | 10.098 % |
c |     11364 |   41781   142365 |   18562   11105   212707    19.2 | 10.110 % |
c ==============================================================================
c [1mFound solution: 595584[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11463 |   41807   142429 |   13935   11204   214368    19.1 | 10.110 % |
c |     11563 |   41807   142429 |   15328   11304   215223    19.0 | 10.113 % |
c ==============================================================================
c [1mFound solution: 544768[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11712 |   41820   142462 |   13940   11453   218121    19.0 | 10.113 % |
c |     11813 |   41820   142462 |   15334   11554   219603    19.0 | 10.120 % |
c |     11963 |   41812   142436 |   16867   11703   221726    18.9 | 10.132 % |
c ==============================================================================
c [1mFound solution: 542720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12123 |   41826   142472 |   13942   11863   223578    18.8 | 10.132 % |
c ==============================================================================
c [1mFound solution: 281344[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12209 |   41334   141014 |   13778   11947   225416    18.9 | 10.132 % |
c |     12309 |   41334   141014 |   15155   12047   228589    19.0 | 11.622 % |
c ==============================================================================
c [1mFound solution: 280768[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12324 |   41358   141074 |   13786   12062   228872    19.0 | 11.622 % |
c ==============================================================================
c [1mFound solution: 272704[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12344 |   41384   141138 |   13794   12082   229231    19.0 | 11.622 % |
c ==============================================================================
c [1mFound solution: 264576[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12400 |   41403   141187 |   13801   12138   230179    19.0 | 11.622 % |
c ==============================================================================
c [1mFound solution: 151744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12473 |   40902   139708 |   13634   12206   230772    18.9 | 11.622 % |
c |     12574 |   40902   139708 |   14997   12307   234020    19.0 | 13.108 % |
c ==============================================================================
c [1mFound solution: 149120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12608 |   40914   139738 |   13638   12341   234909    19.0 | 13.108 % |
c |     12708 |   40914   139738 |   15001   12441   235670    18.9 | 13.113 % |
c |     12859 |   40914   139738 |   16501   12592   237797    18.9 | 13.113 % |
c |     13085 |   40908   139720 |   18152   12817   240941    18.8 | 13.126 % |
c ==============================================================================
c [1mFound solution: 147968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13329 |   40916   139738 |   13638   13060   244124    18.7 | 13.126 % |
c |     13430 |   40916   139738 |   15001   13161   245280    18.6 | 13.143 % |
c |     13581 |   40916   139738 |   16501   13312   247642    18.6 | 13.143 % |
c ==============================================================================
c [1mFound solution: 38400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13639 |   39880   136703 |   13293   13353   248625    18.6 | 13.143 % |
c |     13739 |   39880   136703 |   14622   13453   249968    18.6 | 16.140 % |
c |     13889 |   39880   136703 |   16084   13603   255507    18.8 | 16.140 % |
c |     14116 |   39880   136703 |   17692   13830   260412    18.8 | 16.140 % |
c |     14453 |   39880   136703 |   19462   14167   267540    18.9 | 16.140 % |
c ==============================================================================
c [1mFound solution: 38144[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14542 |   39897   136744 |   13299   14256   268899    18.9 | 16.140 % |
c ==============================================================================
c [1mFound solution: 34560[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14593 |   39907   136770 |   13302   14307   269505    18.8 | 16.140 % |
c |     14695 |   39907   136770 |   14632   14409   271195    18.8 | 16.146 % |
c |     14846 |   39907   136770 |   16095   14560   273010    18.8 | 16.146 % |
c |     15071 |   39907   136770 |   17704   14785   274777    18.6 | 16.146 % |
c |     15408 |   39899   136744 |   19475   15121   285092    18.9 | 16.158 % |
c ==============================================================================
c [1mFound solution: 32928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15738 |   39915   136786 |   13305   15451   288516    18.7 | 16.158 % |
c |     15839 |   39915   136786 |   14635    7827   120417    15.4 | 16.163 % |
c |     15989 |   39915   136786 |   16099    7977   122583    15.4 | 16.163 % |
c |     16214 |   39915   136786 |   17708    8202   127266    15.5 | 16.163 % |
c |     16551 |   39915   136786 |   19479    8539   135038    15.8 | 16.163 % |
c |     17059 |   39915   136786 |   21427    9047   154179    17.0 | 16.163 % |
c ==============================================================================
c [1mFound solution: 32832[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17497 |   39925   136814 |   13308    9485   161982    17.1 | 16.163 % |
c |     17597 |   39925   136814 |   14638    9585   163010    17.0 | 16.171 % |
c |     17747 |   39925   136814 |   16102    9735   165828    17.0 | 16.171 % |
c |     17975 |   39925   136814 |   17712    9963   172115    17.3 | 16.171 % |
c ==============================================================================
c [1mFound solution: 32768[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18267 |   39399   135277 |   13133   10244   177101    17.3 | 16.171 % |
c |     18369 |   39399   135277 |   14446   10346   178791    17.3 | 17.640 % |
c |     18519 |   39399   135277 |   15890   10496   179632    17.1 | 17.640 % |
c |     18744 |   39399   135277 |   17480   10721   181989    17.0 | 17.640 % |
c |     19082 |   39391   135251 |   19228   11058   189819    17.2 | 17.652 % |
c |     19590 |   39391   135251 |   21150   11566   201582    17.4 | 17.652 % |
c ==============================================================================
c [1mFound solution: 29696[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19916 |   39396   135265 |   13132   11892   208706    17.6 | 17.652 % |
c |     20016 |   39396   135265 |   14445   11992   209337    17.5 | 17.658 % |
c |     20166 |   39388   135239 |   15889   12141   211278    17.4 | 17.670 % |
c ==============================================================================
c [1mFound solution: 29440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20313 |   39393   135253 |   13131   12288   213177    17.3 | 17.670 % |
c |     20414 |   39393   135253 |   14444   12389   216271    17.5 | 17.676 % |
c |     20564 |   39393   135253 |   15888   12539   217903    17.4 | 17.676 % |
c |     20789 |   39393   135253 |   17477   12764   222476    17.4 | 17.676 % |
c |     21126 |   39393   135253 |   19225   13101   231638    17.7 | 17.676 % |
c ==============================================================================
c [1mFound solution: 29184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21192 |   39399   135270 |   13133   13167   233135    17.7 | 17.676 % |
c |     21294 |   39399   135270 |   14446   13269   234376    17.7 | 17.681 % |
c |     21444 |   39399   135270 |   15890   13419   237058    17.7 | 17.681 % |
c |     21669 |   39399   135270 |   17480   13644   243160    17.8 | 17.681 % |
c |     22006 |   39399   135270 |   19228   13981   250189    17.9 | 17.681 % |
c ==============================================================================
c [1mFound solution: 26880[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22156 |   39409   135295 |   13136   14131   252548    17.9 | 17.681 % |
c |     22256 |   39409   135295 |   14449   14231   253809    17.8 | 17.685 % |
c |     22406 |   39409   135295 |   15894   14381   256488    17.8 | 17.685 % |
c ==============================================================================
c [1mFound solution: 24840[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22607 |   39425   135338 |   13141   14582   261304    17.9 | 17.685 % |
c |     22710 |   39425   135338 |   14455   14685   263524    17.9 | 17.688 % |
c |     22861 |   39425   135338 |   15900   14836   266173    17.9 | 17.688 % |
c |     23086 |   39425   135338 |   17490   15061   268340    17.8 | 17.688 % |
c ==============================================================================
c [1mFound solution: 23808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23230 |   39433   135358 |   13144   15205   270504    17.8 | 17.688 % |
c |     23332 |   39433   135358 |   14458    7705   114995    14.9 | 17.694 % |
c ==============================================================================
c [1mFound solution: 22912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23443 |   39440   135375 |   13146    7816   116320    14.9 | 17.694 % |
c |     23544 |   39440   135375 |   14460    7917   119405    15.1 | 17.700 % |
c |     23694 |   39440   135375 |   15906    8067   122466    15.2 | 17.700 % |
c |     23919 |   39440   135375 |   17497    8292   127817    15.4 | 17.700 % |
c |     24256 |   39440   135375 |   19247    8629   132256    15.3 | 17.700 % |
c ==============================================================================
c [1mFound solution: 20864[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24366 |   39450   135399 |   13150    8739   133359    15.3 | 17.700 % |
c |     24466 |   39450   135399 |   14465    8839   135472    15.3 | 17.703 % |
c |     24616 |   39450   135399 |   15911    8989   138506    15.4 | 17.703 % |
c |     24842 |   39450   135399 |   17502    9215   143222    15.5 | 17.703 % |
c |     25179 |   39450   135399 |   19252    9552   156045    16.3 | 17.703 % |
c |     25685 |   39450   135399 |   21178   10058   168231    16.7 | 17.703 % |
c |     26445 |   39450   135399 |   23296   10818   186275    17.2 | 17.703 % |
c ==============================================================================
c [1mFound solution: 20480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    0
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27529 |   39446   135387 |   13148   11902   213923    18.0 | 17.703 % |
c |     27629 |   39446   135387 |   14462   12002   215208    17.9 | 17.727 % |
c |     27779 |   39446   135387 |   15909   12152   219045    18.0 | 17.727 % |
c |     28005 |   39446   135387 |   17499   12378   222732    18.0 | 17.727 % |
c |     28342 |   39446   135387 |   19249   12715   231096    18.2 | 17.727 % |
c |     28848 |   39446   135387 |   21174   13221   245022    18.5 | 17.727 % |
c |     29607 |   39446   135387 |   23292   13980   265041    19.0 | 17.727 % |
c ==============================================================================
c [1mFound solution: 19968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29714 |   39454   135407 |   13151   14087   267714    19.0 | 17.727 % |
c |     29815 |   39454   135407 |   14466   14188   269748    19.0 | 17.733 % |
c |     29967 |   39454   135407 |   15912   14340   273961    19.1 | 17.733 % |
c |     30194 |   39454   135407 |   17503   14567   277301    19.0 | 17.733 % |
c |     30531 |   39454   135407 |   19254   14904   287366    19.3 | 17.733 % |
c |     31037 |   39454   135407 |   21179   15410   303205    19.7 | 17.733 % |
c |     31796 |   39454   135407 |   23297   16169   319398    19.8 | 17.733 % |
c ==============================================================================
c [1mFound solution: 19840[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32664 |   39466   135437 |   13155   17037   341890    20.1 | 17.733 % |
c |     32765 |   39466   135437 |   14470    8620   163447    19.0 | 17.737 % |
c |     32915 |   39466   135437 |   15917    8770   164449    18.8 | 17.737 % |
c |     33140 |   39466   135437 |   17509    8995   169150    18.8 | 17.737 % |
c |     33478 |   39466   135437 |   19260    9333   172407    18.5 | 17.737 % |
c ==============================================================================
c [1mFound solution: 19200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    0
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33823 |   39462   135426 |   13154    9678   179864    18.6 | 17.737 % |
c |     33923 |   39462   135426 |   14469    9778   180358    18.4 | 17.761 % |
c |     34076 |   39462   135426 |   15916    9931   184413    18.6 | 17.761 % |
c |     34301 |   39462   135426 |   17507   10156   188991    18.6 | 17.761 % |
c |     34638 |   39462   135426 |   19258   10493   191818    18.3 | 17.761 % |
c |     35145 |   39462   135426 |   21184   11000   205558    18.7 | 17.761 % |
c ==============================================================================
c [1mFound solution: 17424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35734 |   39478   135468 |   13159   11589   222102    19.2 | 17.761 % |
c |     35834 |   39478   135468 |   14474   11689   224072    19.2 | 17.764 % |
c |     35984 |   39478   135468 |   15922   11839   225455    19.0 | 17.764 % |
c |     36211 |   39478   135468 |   17514   12066   227656    18.9 | 17.764 % |
c |     36550 |   39478   135468 |   19266   12405   233416    18.8 | 17.764 % |
c |     37056 |   39478   135468 |   21192   12911   244446    18.9 | 17.764 % |
c |     37815 |   39478   135468 |   23311   13670   267826    19.6 | 17.764 % |
c |     38955 |   39478   135468 |   25643   14810   307040    20.7 | 17.764 % |
c |     40663 |   39478   135468 |   28207   16518   361279    21.9 | 17.764 % |
c ==============================================================================
c [1mFound solution: 17316[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42773 |   39500   135524 |   13166   18628   448682    24.1 | 17.764 % |
c |     42874 |   39500   135524 |   14482    9415   245386    26.1 | 17.764 % |
c |     43024 |   39500   135524 |   15930    9565   247431    25.9 | 17.764 % |
c |     43249 |   39500   135524 |   17523    9790   250322    25.6 | 17.764 % |
c |     43588 |   39500   135524 |   19276   10129   258759    25.5 | 17.764 % |
c |     44095 |   39500   135524 |   21203   10636   269275    25.3 | 17.764 % |
c |     44854 |   39500   135524 |   23324   11395   287749    25.3 | 17.764 % |
c |     45993 |   39500   135524 |   25656   12534   326266    26.0 | 17.764 % |
c ==============================================================================
c [1mFound solution: 16912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47127 |   39516   135566 |   13172   13668   351005    25.7 | 17.764 % |
c |     47227 |   39516   135566 |   14489   13768   353493    25.7 | 17.767 % |
c |     47379 |   39516   135566 |   15938   13920   356422    25.6 | 17.767 % |
c |     47604 |   39516   135566 |   17531   14145   360326    25.5 | 17.767 % |
c |     47941 |   39516   135566 |   19285   14482   368453    25.4 | 17.767 % |
c |     48447 |   39516   135566 |   21213   14988   381567    25.5 | 17.767 % |
c |     49209 |   39516   135566 |   23335   15750   396374    25.2 | 17.767 % |
c ==============================================================================
c [1mFound solution: 16640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50113 |   39522   135582 |   13174   16654   417200    25.1 | 17.767 % |
c |     50213 |   39522   135582 |   14491    8427   163026    19.3 | 17.775 % |
c |     50363 |   39522   135582 |   15940    8577   164394    19.2 | 17.775 % |
c |     50588 |   39522   135582 |   17534    8802   169760    19.3 | 17.775 % |
c |     50925 |   39522   135582 |   19288    9139   175907    19.2 | 17.775 % |
c |     51431 |   39522   135582 |   21216    9645   186870    19.4 | 17.775 % |
c |     52190 |   39522   135582 |   23338   10404   204469    19.7 | 17.775 % |
c |     53329 |   39522   135582 |   25672   11543   239468    20.7 | 17.775 % |
c ==============================================================================
c [1mFound solution: 16400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54668 |   39529   135601 |   13176   12882   279406    21.7 | 17.775 % |
c |     54768 |   39529   135601 |   14493   12982   279924    21.6 | 17.783 % |
c |     54919 |   39529   135601 |   15942   13133   281069    21.4 | 17.783 % |
c |     55144 |   39529   135601 |   17537   13358   284517    21.3 | 17.783 % |
c |     55483 |   39529   135601 |   19290   13697   293860    21.5 | 17.783 % |
c |     55989 |   39529   135601 |   21220   14203   303334    21.4 | 17.783 % |
c |     56748 |   39529   135601 |   23342   14962   319647    21.4 | 17.783 % |
c |     57887 |   39529   135601 |   25676   16101   355697    22.1 | 17.783 % |
c ==============================================================================
c [1mFound solution: 16384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59205 |   38964   133949 |   12988   17298   391496    22.6 | 17.783 % |
c |     59305 |   38964   133949 |   14286    8749   192809    22.0 | 19.387 % |
c |     59457 |   38964   133949 |   15715    8901   193976    21.8 | 19.387 % |
c |     59682 |   38964   133949 |   17287    9126   197012    21.6 | 19.387 % |
c |     60019 |   38964   133949 |   19015    9463   200978    21.2 | 19.387 % |
c |     60525 |   38964   133949 |   20917    9969   212937    21.4 | 19.387 % |
c ==============================================================================
c [1mFound solution: 14720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60804 |   38966   133956 |   12988   10248   219104    21.4 | 19.387 % |
c |     60904 |   38966   133956 |   14286   10348   219543    21.2 | 19.395 % |
c |     61057 |   38966   133956 |   15715   10501   221489    21.1 | 19.395 % |
c |     61282 |   38966   133956 |   17287   10726   226253    21.1 | 19.395 % |
c |     61620 |   38966   133956 |   19015   11064   232813    21.0 | 19.395 % |
c |     62128 |   38966   133956 |   20917   11572   237430    20.5 | 19.395 % |
c |     62887 |   38966   133956 |   23009   12331   250354    20.3 | 19.395 % |
c |     64029 |   38966   133956 |   25309   13473   284696    21.1 | 19.395 % |
c |     65737 |   38966   133956 |   27840   15181   341866    22.5 | 19.395 % |
c ==============================================================================
c [1mFound solution: 14336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66464 |   38967   133960 |   12989   15908   360102    22.6 | 19.395 % |
c |     66565 |   38967   133960 |   14287    8055   163412    20.3 | 19.404 % |
c |     66715 |   38967   133960 |   15716    8205   166185    20.3 | 19.404 % |
c |     66941 |   38967   133960 |   17288    8431   169654    20.1 | 19.404 % |
c |     67280 |   38967   133960 |   19017    8770   174709    19.9 | 19.404 % |
c |     67786 |   38967   133960 |   20918    9276   200123    21.6 | 19.404 % |
c |     68545 |   38967   133960 |   23010   10035   215808    21.5 | 19.404 % |
c ==============================================================================
c [1mFound solution: 14080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68806 |   38971   133971 |   12990   10296   222576    21.6 | 19.404 % |
c |     68906 |   38971   133971 |   14289   10396   224186    21.6 | 19.412 % |
c |     69059 |   38971   133971 |   15717   10549   227744    21.6 | 19.412 % |
c |     69284 |   38971   133971 |   17289   10774   229134    21.3 | 19.412 % |
c |     69621 |   38971   133971 |   19018   11111   235370    21.2 | 19.412 % |
c |     70128 |   38971   133971 |   20920   11618   249366    21.5 | 19.412 % |
c |     70887 |   38971   133971 |   23012   12377   271994    22.0 | 19.412 % |
c |     72026 |   38971   133971 |   25313   13516   315133    23.3 | 19.412 % |
c |     73734 |   38971   133971 |   27845   15224   389758    25.6 | 19.412 % |
c |     76297 |   38971   133971 |   30629   17787   483949    27.2 | 19.412 % |
c |     80142 |   38971   133971 |   33692   21632   609310    28.2 | 19.412 % |
c |     85908 |   38971   133971 |   37061   27398   819558    29.9 | 19.412 % |
c ==============================================================================
c [1mFound solution: 13440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86391 |   38981   133996 |   12993   27881   829182    29.7 | 19.412 % |
c |     86493 |   38981   133996 |   14292   13384   390022    29.1 | 19.414 % |
c |     86645 |   38981   133996 |   15721   13536   392372    29.0 | 19.414 % |
c |     86870 |   38981   133996 |   17293   13761   396070    28.8 | 19.414 % |
c |     87208 |   38981   133996 |   19023   14099   399937    28.4 | 19.414 % |
c |     87714 |   38981   133996 |   20925   14605   415907    28.5 | 19.414 % |
c |     88473 |   38981   133996 |   23017   15364   435133    28.3 | 19.414 % |
c |     89613 |   38981   133996 |   25319   16504   470177    28.5 | 19.414 % |
c |     91322 |   38981   133996 |   27851   18213   527311    29.0 | 19.414 % |
c |     93885 |   38981   133996 |   30636   20776   609181    29.3 | 19.414 % |
c |     97731 |   38981   133996 |   33700   24622   773565    31.4 | 19.414 % |
c |    103497 |   38981   133996 |   37070   30388  1030388    33.9 | 19.414 % |
c |    112146 |   38974   133973 |   40777   39036  1413575    36.2 | 19.426 % |
c |    125122 |   38974   133973 |   44855   22311   869568    39.0 | 19.426 % |
c ==============================================================================
c [1mFound solution: 13376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    136778 |   38985   134001 |   12995   33967  1329122    39.1 | 19.426 % |
c |    136878 |   38985   134001 |   14294   13670   462816    33.9 | 19.429 % |
c |    137028 |   38985   134001 |   15723   13820   465032    33.6 | 19.429 % |
c |    137253 |   38985   134001 |   17296   14045   467334    33.3 | 19.429 % |
c |    137590 |   38985   134001 |   19025   14382   478185    33.2 | 19.429 % |
c |    138096 |   38985   134001 |   20928   14888   492053    33.1 | 19.429 % |
c |    138855 |   38985   134001 |   23021   15647   510319    32.6 | 19.429 % |
c |    139995 |   38985   134001 |   25323   16787   537049    32.0 | 19.429 % |
c |    141705 |   38985   134001 |   27855   18497   586970    31.7 | 19.429 % |
c |    144268 |   38985   134001 |   30641   21060   665325    31.6 | 19.429 % |
c |    148112 |   38985   134001 |   33705   24904   804740    32.3 | 19.429 % |
c ==============================================================================
c [1mFound solution: 13312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149222 |   38986   134005 |   12995   26014   832607    32.0 | 19.429 % |
c |    149322 |   38986   134005 |   14294   12932   346558    26.8 | 19.439 % |
c |    149472 |   38986   134005 |   15723   13082   349284    26.7 | 19.439 % |
c |    149698 |   38986   134005 |   17296   13308   351163    26.4 | 19.439 % |
c |    150035 |   38986   134005 |   19025   13645   358478    26.3 | 19.439 % |
c |    150541 |   38986   134005 |   20928   14151   371529    26.3 | 19.439 % |
c |    151301 |   38986   134005 |   23021   14911   397815    26.7 | 19.439 % |
c |    152441 |   38986   134005 |   25323   16051   438187    27.3 | 19.439 % |
c ==============================================================================
c [1mFound solution: 12800[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    152847 |   38987   134009 |   12995   16457   448874    27.3 | 19.439 % |
c |    152947 |   38987   134009 |   14294    8329   209414    25.1 | 19.448 % |
c |    153097 |   38987   134009 |   15723    8479   210720    24.9 | 19.448 % |
c |    153323 |   38987   134009 |   17296    8705   216050    24.8 | 19.448 % |
c |    153661 |   38987   134009 |   19025    9043   227210    25.1 | 19.448 % |
c |    154167 |   38987   134009 |   20928    9549   240504    25.2 | 19.448 % |
c |    154927 |   38987   134009 |   23021   10309   261713    25.4 | 19.448 % |
c |    156068 |   38987   134009 |   25323   11450   300223    26.2 | 19.448 % |
c ==============================================================================
c [1mFound solution: 12672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    157219 |   38988   134012 |   12996   12601   334057    26.5 | 19.448 % |
c |    157319 |   38988   134012 |   14295   12701   334519    26.3 | 19.458 % |
c |    157470 |   38988   134012 |   15725   12852   338254    26.3 | 19.458 % |
c |    157695 |   38988   134012 |   17297   13077   341639    26.1 | 19.458 % |
c |    158033 |   38988   134012 |   19027   13415   350846    26.2 | 19.458 % |
c |    158539 |   38988   134012 |   20930   13921   363886    26.1 | 19.458 % |
c |    159299 |   38988   134012 |   23023   14681   387070    26.4 | 19.458 % |
c |    160440 |   38988   134012 |   25325   15822   422897    26.7 | 19.458 % |
c |    162148 |   38988   134012 |   27858   17530   463314    26.4 | 19.458 % |
c |    164710 |   38988   134012 |   30643   20092   547705    27.3 | 19.458 % |
c |    168555 |   38988   134012 |   33708   23937   697005    29.1 | 19.458 % |
c ==============================================================================
c [1mFound solution: 12544[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    171651 |   38992   134023 |   12997   27033   815666    30.2 | 19.458 % |
c |    171751 |   38992   134023 |   14296   13305   399197    30.0 | 19.466 % |
c |    171901 |   38992   134023 |   15726   13455   400979    29.8 | 19.466 % |
c |    172127 |   38992   134023 |   17299   13681   405448    29.6 | 19.466 % |
c |    172464 |   38992   134023 |   19028   14018   411163    29.3 | 19.466 % |
c |    172970 |   38992   134023 |   20931   14524   424262    29.2 | 19.466 % |
c |    173730 |   38992   134023 |   23024   15284   446769    29.2 | 19.466 % |
c |    174870 |   38992   134023 |   25327   16424   490220    29.8 | 19.466 % |
c ==============================================================================
c [1mFound solution: 12352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175554 |   38997   134037 |   12999   17108   509975    29.8 | 19.466 % |
c |    175654 |   38997   134037 |   14298    8654   237901    27.5 | 19.473 % |
c |    175804 |   38997   134037 |   15728    8804   239931    27.3 | 19.473 % |
c |    176031 |   38997   134037 |   17301    9031   244576    27.1 | 19.473 % |
c |    176369 |   38997   134037 |   19031    9369   248239    26.5 | 19.473 % |
c |    176875 |   38997   134037 |   20935    9875   261851    26.5 | 19.473 % |
c |    177634 |   38997   134037 |   23028   10634   280863    26.4 | 19.473 % |
c |    178773 |   38997   134037 |   25331   11773   312845    26.6 | 19.473 % |
c |    180481 |   38997   134037 |   27864   13481   364797    27.1 | 19.473 % |
c |    183045 |   38997   134037 |   30650   16045   475800    29.7 | 19.473 % |
c |    186889 |   38997   134037 |   33716   19889   622785    31.3 | 19.473 % |
c |    192657 |   38997   134037 |   37087   25657   832261    32.4 | 19.473 % |
c ==============================================================================
c [1mFound solution: 12288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    193789 |   38998   134040 |   12999   26789   868428    32.4 | 19.473 % |
c |    193889 |   38998   134040 |   14298   13112   419029    32.0 | 19.483 % |
c |    194039 |   38998   134040 |   15728   13262   420291    31.7 | 19.483 % |
c |    194265 |   38998   134040 |   17301   13488   422134    31.3 | 19.483 % |
c |    194602 |   38998   134040 |   19031   13825   429066    31.0 | 19.483 % |
c |    195108 |   38998   134040 |   20935   14331   441350    30.8 | 19.483 % |
c |    195867 |   38998   134040 |   23028   15090   461870    30.6 | 19.483 % |
c |    197006 |   38998   134040 |   25331   16229   494138    30.4 | 19.483 % |
c |    198714 |   38998   134040 |   27864   17937   550628    30.7 | 19.483 % |
c |    201278 |   38998   134040 |   30650   20501   642491    31.3 | 19.483 % |
c |    205122 |   38998   134040 |   33716   24345   763983    31.4 | 19.483 % |
c |    210888 |   38998   134040 |   37087   30111   981350    32.6 | 19.483 % |
c |    219539 |   38998   134040 |   40796   38762  1365787    35.2 | 19.483 % |
c |    232513 |   38998   134040 |   44876   22602   969578    42.9 | 19.483 % |
c ==============================================================================
c [1mFound solution: 12160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    233108 |   39007   134063 |   13002   23197   982391    42.3 | 19.483 % |
c |    233211 |   39007   134063 |   14302   11702   488138    41.7 | 19.488 % |
c |    233361 |   39007   134063 |   15732   11852   490471    41.4 | 19.488 % |
c |    233586 |   39007   134063 |   17305   12077   492931    40.8 | 19.488 % |
c |    233923 |   39007   134063 |   19036   12414   500117    40.3 | 19.488 % |
c |    234429 |   39007   134063 |   20939   12920   511866    39.6 | 19.488 % |
c |    235188 |   39007   134063 |   23033   13679   530842    38.8 | 19.488 % |
c |    236327 |   39007   134063 |   25337   14818   563855    38.1 | 19.488 % |
c |    238035 |   39007   134063 |   27870   16526   626103    37.9 | 19.488 % |
c |    240597 |   39007   134063 |   30658   19088   720768    37.8 | 19.488 % |
c |    244444 |   39007   134063 |   33723   22935   859637    37.5 | 19.488 % |
c |    250211 |   39007   134063 |   37096   28702  1094113    38.1 | 19.488 % |
c |    258861 |   39007   134063 |   40805   37352  1376896    36.9 | 19.488 % |
c |    271835 |   39007   134063 |   44886   20317   736353    36.2 | 19.488 % |
c |    291297 |   39007   134063 |   49375   39779  1744762    43.9 | 19.488 % |
c |    320493 |   39007   134063 |   54312   30620  1420869    46.4 | 19.488 % |
c |    364282 |   39007   134063 |   59743   32899  1746858    53.1 | 19.488 % |
c ==============================================================================
c [1mFound solution: 11904[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    374917 |   39014   134080 |   13004   43534  2190858    50.3 | 19.488 % |
c |    375017 |   39014   134080 |   14304   13966   523199    37.5 | 19.493 % |
c |    375167 |   39014   134080 |   15734   14116   524904    37.2 | 19.493 % |
c |    375392 |   39014   134080 |   17308   14341   527832    36.8 | 19.493 % |
c |    375729 |   39014   134080 |   19039   14678   535602    36.5 | 19.493 % |
c |    376236 |   39014   134080 |   20943   15185   544013    35.8 | 19.493 % |
c |    376995 |   39014   134080 |   23037   15944   558201    35.0 | 19.493 % |
c |    378135 |   39014   134080 |   25341   17084   597939    35.0 | 19.493 % |
c |    379843 |   39014   134080 |   27875   18792   650543    34.6 | 19.493 % |
c |    382405 |   39014   134080 |   30662   21354   734267    34.4 | 19.493 % |
c |    386250 |   39014   134080 |   33729   25199   870885    34.6 | 19.493 % |
c |    392018 |   39014   134080 |   37101   30967  1077410    34.8 | 19.493 % |
c |    400668 |   39014   134080 |   40812   39617  1489022    37.6 | 19.493 % |
c |    413643 |   39014   134080 |   44893   22836   992153    43.4 | 19.493 % |
c |    433104 |   39014   134080 |   49382   42297  1794498    42.4 | 19.493 % |
c ==============================================================================
c [1mFound solution: 11008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    437071 |   39018   134090 |   13006   46264  1944695    42.0 | 19.493 % |
c |    437172 |   39018   134090 |   14306   14127   527825    37.4 | 19.500 % |
c |    437322 |   39018   134090 |   15737   14277   528809    37.0 | 19.500 % |
c |    437548 |   39018   134090 |   17310   14503   531178    36.6 | 19.500 % |
c |    437885 |   39018   134090 |   19042   14840   536501    36.2 | 19.500 % |
c |    438392 |   39018   134090 |   20946   15347   542576    35.4 | 19.500 % |
c |    439151 |   39018   134090 |   23040   16106   556220    34.5 | 19.500 % |
c |    440290 |   39018   134090 |   25345   17245   594011    34.4 | 19.500 % |
c |    441998 |   39018   134090 |   27879   18953   639100    33.7 | 19.500 % |
c |    444560 |   39018   134090 |   30667   21515   761612    35.4 | 19.500 % |
c |    448406 |   39018   134090 |   33734   25361   882510    34.8 | 19.500 % |
c |    454173 |   39018   134090 |   37107   31128  1106040    35.5 | 19.500 % |
c |    462823 |   39018   134090 |   40818   14153   495687    35.0 | 19.500 % |
c ==============================================================================
c [1mFound solution: 10752[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    463203 |   39028   134114 |   13009   14533   503716    34.7 | 19.500 % |
c |    463303 |   39028   134114 |   14309   14633   504615    34.5 | 19.503 % |
c |    463453 |   39028   134114 |   15740   14783   509174    34.4 | 19.503 % |
c |    463678 |   39028   134114 |   17314   15008   512423    34.1 | 19.503 % |
c |    464015 |   39028   134114 |   19046   15345   517252    33.7 | 19.503 % |
c |    464521 |   39028   134114 |   20951   15851   529331    33.4 | 19.503 % |
c |    465280 |   39028   134114 |   23046   16610   544555    32.8 | 19.503 % |
c |    466420 |   39028   134114 |   25350   17750   564218    31.8 | 19.503 % |
c |    468128 |   39028   134114 |   27885   19458   615213    31.6 | 19.503 % |
c |    470690 |   39028   134114 |   30674   22020   710762    32.3 | 19.503 % |
c |    474535 |   39028   134114 |   33741   25865   874018    33.8 | 19.503 % |
c ==============================================================================
c [1mFound solution: 10368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    476362 |   39038   134138 |   13012   27692   930466    33.6 | 19.503 % |
c |    476462 |   39038   134138 |   14313   13839   399516    28.9 | 19.505 % |
c |    476612 |   39038   134138 |   15744   13989   400954    28.7 | 19.505 % |
c |    476839 |   39038   134138 |   17318   14216   402630    28.3 | 19.505 % |
c |    477177 |   39038   134138 |   19050   14554   409756    28.2 | 19.505 % |
c |    477683 |   39038   134138 |   20955   15060   418282    27.8 | 19.505 % |
c |    478444 |   39038   134138 |   23051   15821   437593    27.7 | 19.505 % |
c |    479583 |   39038   134138 |   25356   16960   477231    28.1 | 19.505 % |
c |    481295 |   39038   134138 |   27892   18672   541603    29.0 | 19.505 % |
c |    483858 |   39038   134138 |   30681   21235   628241    29.6 | 19.505 % |
c |    487702 |   39038   134138 |   33749   25079   773794    30.9 | 19.505 % |
c |    493469 |   39038   134138 |   37124   30846  1014792    32.9 | 19.505 % |
c |    502119 |   39038   134138 |   40837   39496  1419201    35.9 | 19.505 % |
c ==============================================================================
c [1mFound solution: 10240[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    506534 |   39042   134148 |   13014   15532   558538    36.0 | 19.505 % |
c |    506634 |   39042   134148 |   14315    7866   224202    28.5 | 19.512 % |
c |    506785 |   39042   134148 |   15746    8017   226836    28.3 | 19.512 % |
c |    507011 |   39042   134148 |   17321    8243   229345    27.8 | 19.512 % |
c |    507350 |   39042   134148 |   19053    8582   238443    27.8 | 19.512 % |
c |    507856 |   39042   134148 |   20959    9088   251254    27.6 | 19.512 % |
c |    508616 |   39042   134148 |   23055    9848   268573    27.3 | 19.512 % |
c |    509755 |   39042   134148 |   25360   10987   302908    27.6 | 19.512 % |
c |    511463 |   39042   134148 |   27896   12695   358191    28.2 | 19.512 % |
c |    514025 |   39042   134148 |   30686   15257   451408    29.6 | 19.512 % |
c |    517870 |   39042   134148 |   33754   19102   597910    31.3 | 19.512 % |
c |    523638 |   39042   134148 |   37130   24870   841524    33.8 | 19.512 % |
c |    532287 |   39042   134148 |   40843   33519  1181469    35.2 | 19.512 % |
c |    545262 |   39042   134148 |   44927   17099   739114    43.2 | 19.512 % |
c |    564726 |   39042   134148 |   49420   36563  1551994    42.4 | 19.512 % |
c |    593919 |   39042   134148 |   54362   28418  1250157    44.0 | 19.512 % |
c |    637710 |   39042   134148 |   59798   30697  1509916    49.2 | 19.512 % |
c |    703394 |   39038   134136 |   65778   49710  2466759    49.6 | 19.537 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1_bit_7 -x1_bit_6 -x1_bit_5 -x1_bit_4 -x1_bit_3 -x1_bit_2 -x1_bit_1 -x1_bit0 -x1_bit1 -x1_bit2 -x1_bit3 x1_bit4 -x1_bit5 x1_bit6 -x1_bit7 -x1_bit8 -x1_bit9 -x1_bit10 -x1_bit11 -x1_bit12 x2_bit0 -x3_bit0 -x4_bit0 -x5_bit0 x6_bit0 x7_bit0 -x8_bit0 -x9_bit0 x10_bit0 -x11_bit0 x12_bit0 -x13_bit0 x14_bit0 -x15_bit0 -x16_bit0 x17_bit0 -x18_bit0 -x19_bit0 -x20_bit0 -x21_bit0 x22_bit0 x23_bit0 x24_bit0 -x25_bit0 -x26_bit0 -x27_bit0 -x28_bit0 x29_bit0 -x30_bit0 x31_bit0 -x32_bit0 x33_bit0 x34_bit0 -x35_bit0 x36_bit0 x37_bit0 -x38_bit0 -x39_bit0 x40_bit0 -x41_bit0 x42_bit0 -x43_bit0 x44_bit0 -x45_bit0 -x46_bit0 x47_bit0 x48_bit0 x49_bit0 -x50_bit0 -x51_bit0 -x52_bit0 -x53_bit0 -x54_bit0 x55_bit0 x56_bit0 -x57_bit_7 -x57_bit_6 x57_bit_5 -x57_bit_4 -x57_bit_3 -x57_bit_2 -x57_bit_1 -x57_bit0 x57_bit1 -x57_bit2 x57_bit3 -x57_bit4 -x57_bit5 x57_bit6 -x57_bit7 -x57_bit8 -x57_bit9 -x57_bit10 -x57_bit11 -x57_bit12 -x58_bit_7 -x58_bit_6 x58_bit_5 -x58_bit_4 -x58_bit_3 -x58_bit_2 -x58_bit_1 x58_bit0 -x58_bit1 -x58_bit2 -x58_bit3 -x58_bit4 -x58_bit5 -x58_bit6 -x58_bit7 -x58_bit8 -x58_bit9 -x58_bit10 -x58_bit11 -x58_bit12 x75_bit_7 -x75_bit_6 -x75_bit_5 -x75_bit_4 -x75_bit_3 -x75_bit_2 -x75_bit_1 x75_bit0 -x75_bit1 x75_bit2 -x75_bit3 -x75_bit4 x75_bit5 -x75_bit6 -x75_bit7 -x75_bit8 -x75_bit9 -x75_bit10 -x75_bit11 -x75_bit12 x76_bit_7 -x76_bit_6 -x76_bit_5 -x76_bit_4 -x76_bit_3 -x76_bit_2 -x76_bit_1 -x76_bit0 x76_bit1 -x76_bit2 -x76_bit3 -x76_bit4 x76_bit5 -x76_bit6 -x76_bit7 -x76_bit8 -x76_bit9 -x76_bit10 -x76_bit11 -x76_bit12 -x77_bit_7 -x77_bit_6 -x77_bit_5 -x77_bit_4 -x77_bit_3 -x77_bit_2 -x77_bit_1 -x77_bit0 -x77_bit1 -x77_bit2 -x77_bit3 x77_bit4 -x77_bit5 x77_bit6 -x77_bit7 -x77_bit8 -x77_bit9 -x77_bit10 -x77_bit11 -x77_bit12 -x78_bit_7 -x78_bit_6 -x78_bit_5 -x78_bit_4 -x78_bit_3 -x78_bit_2 -x78_bit_1 x78_bit0 x78_bit1 x78_bit2 -x78_bit3 -x78_bit4 -x78_bit5 -x78_bit6 -x78_bit7 -x78_bit8 -x78_bit9 -x78_bit10 -x78_bit11 -x78_bit12 -x79_bit_7 -x79_bit_6 x79_bit_5 -x79_bit_4 -x79_bit_3 -x79_bit_2 -x79_bit_1 -x79_bit0 -x79_bit1 x79_bit2 -x79_bit3 x79_bit4 -x79_bit5 -x79_bit6 -x79_bit7 -x79_bit8 -x79_bit9 -x79_bit10 -x79_bit11 -x79_bit12 -x80_bit_7 -x80_bit_6 x80_bit_5 -x80_bit_4 -x80_bit_3 -x80_bit_2 -x80_bit_1 -x80_bit0 -x80_bit1 -x80_bit2 -x80_bit3 -x80_bit4 -x80_bit5 -x80_bit6 -x80_bit7 -x80_bit8 -x80_bit9 -x80_bit10 -x80_bit11 -x80_bit12 -x81_bit_7 -x81_bit_6 -x81_bit_5 -x81_bit_4 -x81_bit_3 x81_bit_2 -x81_bit_1 x81_bit0 x81_bit1 x81_bit2 x81_bit3 -x81_bit4 -x81_bit5 x81_bit6 -x81_bit7 -x81_bit8 -x81_bit9 -x81_bit10 -x81_bit11 -x81_bit12 -x82_bit_7 -x82_bit_6 -x82_bit_5 -x82_bit_4 -x82_bit_3 x82_bit_2 -x82_bit_1 -x82_bit0 -x82_bit1 -x82_bit2 -x82_bit3 -x82_bit4 -x82_bit5 -x82_bit6 -x82_bit7 -x82_bit8 -x82_bit9 -x82_bit10 -x82_bit11 -x82_bit12 -x83_bit_7 -x83_bit_6 x83_bit_5 -x83_bit_4 -x83_bit_3 -x83_bit_2 -x83_bit_1 -x83_bit0 -x83_bit1 -x83_bit2 -x83_bit3 x83_bit4 x83_bit5 -x83_bit6 -x83_bit7 -x83_bit8 -x83_bit9 -x83_bit10 -x83_bit11 -x83_bit12 -x84_bit_7 -x84_bit_6 x84_bit_5 -x84_bit_4 -x84_bit_3 -x84_bit_2 -x84_bit_1 x84_bit0 x84_bit1 -x84_bit2 -x84_bit3 -x84_bit4 -x84_bit5 x84_bit6 -x84_bit7 -x84_bit8 -x84_bit9 -x84_bit10 -x84_bit11 -x84_bit12 -x85_bit_7 -x85_bit_6 -x85_bit_5 -x85_bit_4 -x85_bit_3 -x85_bit_2 -x85_bit_1 -x85_bit0 -x85_bit1 -x85_bit2 -x85_bit3 x85_bit4 -x85_bit5 x85_bit6 -x85_bit7 -x85_bit8 -x85_bit9 -x85_bit10 -x85_bit11 -x85_bit12 -x86_bit_7 -x86_bit_6 -x86_bit_5 -x86_bit_4 -x86_bit_3 -x86_bit_2 -x86_bit_1 x86_bit0 -x86_bit1 x86_bit2 x86_bit3 -x86_bit4 -x86_bit5 -x86_bit6 -x86_bit7 -x86_bit8 -x86_bit9 -x86_bit10 -x86_bit11 -x86_bit12 -x59_bit_7 x59_bit_6 -x59_bit_5 -x59_bit_4 -x59_bit_3 -x59_bit_2 -x59_bit_1 -x59_bit0 -x59_bit1 -x59_bit2 -x59_bit3 -x59_bit4 -x59_bit5 -x59_bit6 -x59_bit7 -x59_bit8 -x59_bit9 -x59_bit10 -x59_bit11 -x59_bit12 -x60_bit_7 x60_bit_6 -x60_bit_5 -x60_bit_4 -x60_bit_3 -x60_bit_2 -x60_bit_1 -x60_bit0 -x60_bit1 -x60_bit2 x60_bit3 x60_bit4 x60_bit5 -x60_bit6 -x60_bit7 -x60_bit8 -x60_bit9 -x60_bit10 -x60_bit11 -x60_bit12 -x61_bit_7 -x61_bit_6 x61_bit_5 -x61#### 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.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (runsolver) R 13628 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487863551 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.0001 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 1542 0 0 0 993 4 0 0 25 0 1 0 487863551 7880704 1517 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1924 1517 603 41 0 1883 0
vsize: 7696
[startup+20.0009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 1708 0 0 0 1991 6 0 0 25 0 1 0 487863551 8916992 1683 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1683 603 41 0 2136 0
vsize: 8708
[startup+30.001 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 1834 0 0 0 2990 7 0 0 25 0 1 0 487863551 9523200 1809 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2325 1809 603 41 0 2284 0
vsize: 9300
[startup+40.0015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 1983 0 0 0 3990 7 0 0 25 0 1 0 487863551 10055680 1958 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2455 1958 603 41 0 2414 0
vsize: 9820
[startup+50.0014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 1983 0 0 0 4990 7 0 0 25 0 1 0 487863551 10055680 1958 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2455 1958 603 41 0 2414 0
vsize: 9820
[startup+60.0018 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 2032 0 0 0 5990 7 0 0 25 0 1 0 487863551 10321920 2007 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2520 2007 603 41 0 2479 0
vsize: 10080
[startup+70.0022 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 2450 0 0 0 6988 8 0 0 25 0 1 0 487863551 11923456 2425 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2911 2425 603 41 0 2870 0
vsize: 11644
[startup+80.0022 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 2522 0 0 0 7987 9 0 0 25 0 1 0 487863551 12193792 2497 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2977 2497 603 41 0 2936 0
vsize: 11908
[startup+90.003 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 2652 0 0 0 8987 9 0 0 25 0 1 0 487863551 12730368 2627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3108 2627 603 41 0 3067 0
vsize: 12432
[startup+100.003 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 2962 0 0 0 9986 10 0 0 25 0 1 0 487863551 14204928 2937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3468 2937 603 41 0 3427 0
vsize: 13872
[startup+110.003 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3209 0 0 0 10986 11 0 0 25 0 1 0 487863551 15134720 3184 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3695 3184 603 41 0 3654 0
vsize: 14780
[startup+120.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 11986 11 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+130.003 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 12986 11 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+140.003 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 13986 11 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+150.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 14986 11 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+160.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 15986 11 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+170.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 16986 11 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+180.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 17986 12 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+190.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 18986 12 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+200.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 19987 12 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+210.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 20987 12 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+220.005 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 21987 12 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+230.005 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 22987 12 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+240.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3482 0 0 0 23987 12 0 0 25 0 1 0 487863551 16216064 3457 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+250.005 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3729 0 0 0 24987 12 0 0 25 0 1 0 487863551 17297408 3704 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3704 603 41 0 4182 0
vsize: 16892
[startup+260.005 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3729 0 0 0 25987 12 0 0 25 0 1 0 487863551 17297408 3704 4294967295 134512640 134672761 3221224560 3221223684 134566142 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3704 603 41 0 4182 0
vsize: 16892
[startup+270.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3730 0 0 0 26987 12 0 0 25 0 1 0 487863551 17297408 3705 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3705 603 41 0 4182 0
vsize: 16892
[startup+280.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3730 0 0 0 27987 12 0 0 25 0 1 0 487863551 17297408 3705 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3705 603 41 0 4182 0
vsize: 16892
[startup+290.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3730 0 0 0 28987 12 0 0 25 0 1 0 487863551 17297408 3705 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3705 603 41 0 4182 0
vsize: 16892
[startup+300.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3820 0 0 0 29987 12 0 0 25 0 1 0 487863551 17698816 3795 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4321 3795 603 41 0 4280 0
vsize: 17284
[startup+310.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3820 0 0 0 30988 12 0 0 25 0 1 0 487863551 17698816 3795 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4321 3795 603 41 0 4280 0
vsize: 17284
[startup+320.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3820 0 0 0 31988 12 0 0 25 0 1 0 487863551 17698816 3795 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4321 3795 603 41 0 4280 0
vsize: 17284
[startup+330.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3820 0 0 0 32988 12 0 0 25 0 1 0 487863551 17698816 3795 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4321 3795 603 41 0 4280 0
vsize: 17284
[startup+340.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 3982 0 0 0 33987 13 0 0 25 0 1 0 487863551 18362368 3957 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4483 3957 603 41 0 4442 0
vsize: 17932
[startup+350.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4225 0 0 0 34987 14 0 0 25 0 1 0 487863551 19296256 4200 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4711 4200 603 41 0 4670 0
vsize: 18844
[startup+360.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4421 0 0 0 35986 15 0 0 25 0 1 0 487863551 20094976 4396 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4906 4396 603 41 0 4865 0
vsize: 19624
[startup+370.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4668 0 0 0 36985 16 0 0 25 0 1 0 487863551 21037056 4643 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5136 4643 603 41 0 5095 0
vsize: 20544
[startup+380.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4756 0 0 0 37985 16 0 0 25 0 1 0 487863551 21438464 4731 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+390.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4756 0 0 0 38985 16 0 0 25 0 1 0 487863551 21438464 4731 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+400.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4756 0 0 0 39986 16 0 0 25 0 1 0 487863551 21438464 4731 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+410.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4756 0 0 0 40986 16 0 0 25 0 1 0 487863551 21438464 4731 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+420.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4756 0 0 0 41986 16 0 0 25 0 1 0 487863551 21438464 4731 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+430.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4756 0 0 0 42986 16 0 0 25 0 1 0 487863551 21438464 4731 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+440.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4756 0 0 0 43986 16 0 0 25 0 1 0 487863551 21438464 4731 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+450.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 4920 0 0 0 44986 16 0 0 25 0 1 0 487863551 22106112 4895 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5397 4895 603 41 0 5356 0
vsize: 21588
[startup+460.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5113 0 0 0 45985 17 0 0 25 0 1 0 487863551 22900736 5088 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5591 5088 603 41 0 5550 0
vsize: 22364
[startup+470.008 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5281 0 0 0 46985 18 0 0 25 0 1 0 487863551 23576576 5256 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5756 5256 603 41 0 5715 0
vsize: 23024
[startup+480.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 47985 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+490.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 48985 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+500.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 49985 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+510.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 50986 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+520.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 51986 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223620 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+530.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 52985 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+540.008 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 53986 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+550.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 54986 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+560.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 55986 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+570.008 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 56986 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+580.008 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 57986 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+590.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 58987 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+600.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 59987 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+610.008 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 60987 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+620.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 61987 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+630.008 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 62987 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+640.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 63987 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+650.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 64987 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+660.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 65988 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+670.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 66988 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+680.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 67988 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+690.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 68988 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+700.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 69988 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+710.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 70988 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+720.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 71989 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+730.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 72989 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+740.012 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 73989 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+750.012 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 74989 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223664 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+760.012 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 75989 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+770.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 76989 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+780.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 77990 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+790.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 78990 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223744 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+800.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 79990 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+810.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 80990 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+820.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 81990 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+830.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 82991 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+840.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 83991 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+850.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 84991 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+860.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 85991 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+870.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5321 0 0 0 86991 18 0 0 25 0 1 0 487863551 23707648 5296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+880.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5322 0 0 0 87992 18 0 0 25 0 1 0 487863551 23707648 5297 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5297 603 41 0 5747 0
vsize: 23152
[startup+890.016 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5322 0 0 0 88992 18 0 0 25 0 1 0 487863551 23707648 5297 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5297 603 41 0 5747 0
vsize: 23152
[startup+900.016 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5322 0 0 0 89992 18 0 0 25 0 1 0 487863551 23707648 5297 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5297 603 41 0 5747 0
vsize: 23152
[startup+910.016 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5322 0 0 0 90992 18 0 0 25 0 1 0 487863551 23707648 5297 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5297 603 41 0 5747 0
vsize: 23152
[startup+920.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5322 0 0 0 91992 18 0 0 25 0 1 0 487863551 23707648 5297 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5297 603 41 0 5747 0
vsize: 23152
[startup+930.016 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5324 0 0 0 92992 18 0 0 25 0 1 0 487863551 23707648 5299 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5788 5299 603 41 0 5747 0
vsize: 23152
[startup+940.016 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5544 0 0 0 93992 19 0 0 25 0 1 0 487863551 24641536 5519 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6016 5519 603 41 0 5975 0
vsize: 24064
[startup+950.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5600 0 0 0 94992 19 0 0 25 0 1 0 487863551 24907776 5575 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+960.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5600 0 0 0 95992 19 0 0 25 0 1 0 487863551 24907776 5575 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+970.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5600 0 0 0 96992 19 0 0 25 0 1 0 487863551 24907776 5575 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+980.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5600 0 0 0 97992 19 0 0 25 0 1 0 487863551 24907776 5575 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+990.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5600 0 0 0 98992 19 0 0 25 0 1 0 487863551 24907776 5575 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+1000.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5600 0 0 0 99992 19 0 0 25 0 1 0 487863551 24907776 5575 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+1010.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5600 0 0 0 100993 19 0 0 25 0 1 0 487863551 24907776 5575 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+1020.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5600 0 0 0 101993 19 0 0 25 0 1 0 487863551 24907776 5575 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+1030.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5630 0 0 0 102993 19 0 0 25 0 1 0 487863551 25042944 5605 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6114 5605 603 41 0 6073 0
vsize: 24456
[startup+1040.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5797 0 0 0 103992 20 0 0 25 0 1 0 487863551 25710592 5772 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6277 5772 603 41 0 6236 0
vsize: 25108
[startup+1050.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 5962 0 0 0 104992 20 0 0 25 0 1 0 487863551 26402816 5937 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6446 5937 603 41 0 6405 0
vsize: 25784
[startup+1060.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6065 0 0 0 105993 21 0 0 25 0 1 0 487863551 26800128 6040 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1070.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6065 0 0 0 106993 21 0 0 25 0 1 0 487863551 26800128 6040 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1080.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6065 0 0 0 107993 21 0 0 25 0 1 0 487863551 26800128 6040 4294967295 134512640 134672761 3221224560 3221223664 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1090.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6065 0 0 0 108993 21 0 0 25 0 1 0 487863551 26800128 6040 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1100.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6065 0 0 0 109994 21 0 0 25 0 1 0 487863551 26800128 6040 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1110.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6065 0 0 0 110994 21 0 0 25 0 1 0 487863551 26800128 6040 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1120.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6065 0 0 0 111994 21 0 0 25 0 1 0 487863551 26800128 6040 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1130.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6066 0 0 0 112994 21 0 0 25 0 1 0 487863551 26800128 6041 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6543 6041 603 41 0 6502 0
vsize: 26172
[startup+1140.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6066 0 0 0 113994 21 0 0 25 0 1 0 487863551 26800128 6041 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6041 603 41 0 6502 0
vsize: 26172
[startup+1150.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6066 0 0 0 114994 21 0 0 25 0 1 0 487863551 26800128 6041 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6041 603 41 0 6502 0
vsize: 26172
[startup+1160.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6233 0 0 0 115993 22 0 0 25 0 1 0 487863551 27738112 6208 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6772 6208 603 41 0 6731 0
vsize: 27088
[startup+1170.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6341 0 0 0 116993 22 0 0 25 0 1 0 487863551 28139520 6316 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6316 603 41 0 6829 0
vsize: 27480
[startup+1180.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6341 0 0 0 117993 22 0 0 25 0 1 0 487863551 28139520 6316 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6316 603 41 0 6829 0
vsize: 27480
[startup+1190.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6341 0 0 0 118993 22 0 0 25 0 1 0 487863551 28139520 6316 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6316 603 41 0 6829 0
vsize: 27480
[startup+1200.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13629
Raw data (stat): 13629 (minisat+) R 13628 10720 10719 0 -1 0 6341 0 0 0 119993 22 0 0 25 0 1 0 487863551 28139520 6316 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6870 6316 603 41 0 6829 0
vsize: 27480
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 1.00 0.94 1/54 13629
Raw data (stat): 13629 (minisat+) Z 13628 10720 10719 0 -1 12 6344 0 0 0 119994 23 0 0 25 0 1 0 487863551 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.05
CPU time (s): 1200.18
CPU user time (s): 1199.94
CPU system time (s): 0.234964
CPU usage (%): 100.011
Max. virtual memory (Kb): 27480
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####