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/miplib3/normalized-mps-v2-13-7-pk1.opb
MD5SUM	b6007187ad037f56a5e2b97a0b86cea8
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.03
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 14990

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 02:23:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18759 boxname=wulflinc22 idbench=1443 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b6007187ad037f56a5e2b97a0b86cea8  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-pk1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-pk1.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-pk1.opb
IDLAUNCH: 18759
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 3
cpu MHz		: 451.031
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:        808668 kB
Buffers:         20180 kB
Cached:         175228 kB
SwapCached:         24 kB
Active:          26012 kB
Inactive:       172024 kB
HighTotal:      131008 kB
HighFree:        54936 kB
LowTotal:       903652 kB
LowFree:        753732 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22328 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:43:44 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 18759 7 1200.22 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 -d_bit_7 -d_bit_6 -d_bit_5 -d_bit_4 -d_bit_3 -d_bit_2 -d_bit_1 -d_bit0 -d_bit1 -d_bit2 -d_bit3 d_bit4 -d_bit5 d_bit6 -d_bit7 -d_bit8 -d_bit9 -d_bit10 -d_bit11 -d_bit12 X1_bit0 -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 -S1_bit_7 -S1_bit_6 S1_bit_5 -S1_bit_4 -S1_bit_3 -S1_bit_2 -S1_bit_1 -S1_bit0 S1_bit1 -S1_bit2 S1_bit3 -S1_bit4 -S1_bit5 S1_bit6 -S1_bit7 -S1_bit8 -S1_bit9 -S1_bit10 -S1_bit11 -S1_bit12 -T1_bit_7 -T1_bit_6 T1_bit_5 -T1_bit_4 -T1_bit_3 -T1_bit_2 -T1_bit_1 T1_bit0 -T1_bit1 -T1_bit2 -T1_bit3 -T1_bit4 -T1_bit5 -T1_bit6 -T1_bit7 -T1_bit8 -T1_bit9 -T1_bit10 -T1_bit11 -T1_bit12 S10_bit_7 -S10_bit_6 -S10_bit_5 -S10_bit_4 -S10_bit_3 -S10_bit_2 -S10_bit_1 S10_bit0 -S10_bit1 S10_bit2 -S10_bit3 -S10_bit4 S10_bit5 -S10_bit6 -S10_bit7 -S10_bit8 -S10_bit9 -S10_bit10 -S10_bit11 -S10_bit12 T10_bit_7 -T10_bit_6 -T10_bit_5 -T10_bit_4 -T10_bit_3 -T10_bit_2 -T10_bit_1 -T10_bit0 T10_bit1 -T10_bit2 -T10_bit3 -T10_bit4 T10_bit5 -T10_bit6 -T10_bit7 -T10_bit8 -T10_bit9 -T10_bit10 -T10_bit11 -T10_bit12 -S11_bit_7 -S11_bit_6 -S11_bit_5 -S11_bit_4 -S11_bit_3 -S11_bit_2 -S11_bit_1 -S11_bit0 -S11_bit1 -S11_bit2 -S11_bit3 S11_bit4 -S11_bit5 S11_bit6 -S11_bit7 -S11_bit8 -S11_bit9 -S11_bit10 -S11_bit11 -S11_bit12 -T11_bit_7 -T11_bit_6 -T11_bit_5 -T11_bit_4 -T11_bit_3 -T11_bit_2 -T11_bit_1 T11_bit0 T11_bit1 T11_bit2 -T11_bit3 -T11_bit4 -T11_bit5 -T11_bit6 -T11_bit7 -T11_bit8 -T11_bit9 -T11_bit10 -T11_bit11 -T11_bit12 -S12_bit_7 -S12_bit_6 S12_bit_5 -S12_bit_4 -S12_bit_3 -S12_bit_2 -S12_bit_1 -S12_bit0 -S12_bit1 S12_bit2 -S12_bit3 S12_bit4 -S12_bit5 -S12_bit6 -S12_bit7 -S12_bit8 -S12_bit9 -S12_bit10 -S12_bit11 -S12_bit12 -T12_bit_7 -T12_bit_6 T12_bit_5 -T12_bit_4 -T12_bit_3 -T12_bit_2 -T12_bit_1 -T12_bit0 -T12_bit1 -T12_bit2 -T12_bit3 -T12_bit4 -T12_bit5 -T12_bit6 -T12_bit7 -T12_bit8 -T12_bit9 -T12_bit10 -T12_bit11 -T12_bit12 -S13_bit_7 -S13_bit_6 -S13_bit_5 -S13_bit_4 -S13_bit_3 S13_bit_2 -S13_bit_1 S13_bit0 S13_bit1 S13_bit2 S13_bit3 -S13_bit4 -S13_bit5 S13_bit6 -S13_bit7 -S13_bit8 -S13_bit9 -S13_bit10 -S13_bit11 -S13_bit12 -T13_bit_7 -T13_bit_6 -T13_bit_5 -T13_bit_4 -T13_bit_3 T13_bit_2 -T13_bit_1 -T13_bit0 -T13_bit1 -T13_bit2 -T13_bit3 -T13_bit4 -T13_bit5 -T13_bit6 -T13_bit7 -T13_bit8 -T13_bit9 -T13_bit10 -T13_bit11 -T13_bit12 -S14_bit_7 -S14_bit_6 S14_bit_5 -S14_bit_4 -S14_bit_3 -S14_bit_2 -S14_bit_1 -S14_bit0 -S14_bit1 -S14_bit2 -S14_bit3 S14_bit4 S14_bit5 -S14_bit6 -S14_bit7 -S14_bit8 -S14_bit9 -S14_bit10 -S14_bit11 -S14_bit12 -T14_bit_7 -T14_bit_6 T14_bit_5 -T14_bit_4 -T14_bit_3 -T14_bit_2 -T14_bit_1 T14_bit0 T14_bit1 -T14_bit2 -T14_bit3 -T14_bit4 -T14_bit5 T14_bit6 -T14_bit7 -T14_bit8 -T14_bit9 -T14_bit10 -T14_bit11 -T14_bit12 -S15_bit_7 -S15_bit_6 -S15_bit_5 -S15_bit_4 -S15_bit_3 -S15_bit_2 -S15_bit_1 -S15_bit0 -S15_bit1 -S15_bit2 -S15_bit3 S15_bit4 -S15_bit5 S15_bit6 -S15_bit7 -S15_bit8 -S15_bit9 -S15_bit10 -S15_bit11 -S15_bit12 -T15_bit_7 -T15_bit_6 -T15_bit_5 -T15_bit_4 -T15_bit_3 -T15_bit_2 -T15_bit_1 T15_bit0 -T15_bit1 T15_bit2 T15_bit3 -T15_bit4 -T15_bit5 -T15_bit6 -T15_bit7 -T15_bit8 -T15_bit9 -T15_bit10 -T15_bit11 -T15_bit12 -S2_bit_7 S2_bit_6 -S2_bit_5 -S2_bit_4 -S2_bit_3 -S2_bit_2 -S2_bit_1 -S2_bit0 -S2_bit1 -S2_bit2 -S2_bit3 -S2_bit4 -S2_bit5 -S2_bit6 -S2_bit7 -S2_bit8 -S2_bit9 -S2_bit10 -S2_bit11 -S2_bit12 -T2_bit_7 T2_bit_6 -T2_bit_5 -T2_bit_4 -T2_bit_3 -T2_bit_2 -T2_bit_1 -T2_bit0 -T2_bit1 -T2_bit2 T2_bit3 T2_bit4 T2_bit5 -T2_bit6 -T2_bit7 -T2_bit8 -T2_bit9 -T2_bit10 -T2_bit11 -T2_bit12 -S3_bit_7 -S3_bit_6 S3_bit_5 -S3_bit_4 -S3_bit_3 -S3_bit_2 -S3_bit_1 -S3_bit0 -S3_bit1 -S3_bit2 -S3_bit3 -S3_bit4 -S3_bit5 -S3_bit6 -S3_b#### 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.74 0.94 0.93 2/54 26283
Raw data (stat): 26283 (runsolver) R 26282 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541450522 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.78 0.95 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 1543 0 0 0 993 5 0 0 25 0 1 0 541450522 7880704 1518 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1924 1518 603 41 0 1883 0
vsize: 7696
[startup+20.0004 s]
Raw data (loadavg): 0.81 0.95 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 1708 0 0 0 1992 6 0 0 25 0 1 0 541450522 8916992 1683 4294967295 134512640 134672761 3221224544 3221223712 134561154 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.0007 s]
Raw data (loadavg): 0.84 0.95 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 1834 0 0 0 2991 7 0 0 25 0 1 0 541450522 9523200 1809 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.0002 s]
Raw data (loadavg): 0.86 0.95 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 1983 0 0 0 3991 8 0 0 25 0 1 0 541450522 10055680 1958 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2455 1958 603 41 0 2414 0
vsize: 9820
[startup+50.0012 s]
Raw data (loadavg): 0.88 0.95 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 1983 0 0 0 4991 8 0 0 25 0 1 0 541450522 10055680 1958 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2455 1958 603 41 0 2414 0
vsize: 9820
[startup+60.0008 s]
Raw data (loadavg): 0.90 0.95 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 2045 0 0 0 5991 8 0 0 25 0 1 0 541450522 10321920 2020 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2520 2020 603 41 0 2479 0
vsize: 10080
[startup+70.0004 s]
Raw data (loadavg): 0.92 0.95 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 2465 0 0 0 6989 9 0 0 25 0 1 0 541450522 12058624 2440 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2944 2440 603 41 0 2903 0
vsize: 11776
[startup+80.0014 s]
Raw data (loadavg): 0.93 0.95 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 2522 0 0 0 7989 10 0 0 25 0 1 0 541450522 12193792 2497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2977 2497 603 41 0 2936 0
vsize: 11908
[startup+90.0008 s]
Raw data (loadavg): 0.94 0.95 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 2675 0 0 0 8989 10 0 0 25 0 1 0 541450522 12861440 2650 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3140 2650 603 41 0 3099 0
vsize: 12560
[startup+100.001 s]
Raw data (loadavg): 0.95 0.95 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 2988 0 0 0 9988 11 0 0 25 0 1 0 541450522 14336000 2963 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3500 2963 603 41 0 3459 0
vsize: 14000
[startup+110.001 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3243 0 0 0 10987 12 0 0 25 0 1 0 541450522 15269888 3218 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3728 3218 603 41 0 3687 0
vsize: 14912
[startup+120.001 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 11987 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+130.001 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 12987 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+140.001 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 13987 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+150.001 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 14987 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+160.001 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 15987 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+170.001 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 16987 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+180.001 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 17988 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+190.001 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 18988 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 19988 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 20988 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 21988 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3482 0 0 0 22988 13 0 0 25 0 1 0 541450522 16216064 3457 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3959 3457 603 41 0 3918 0
vsize: 15836
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3621 0 0 0 23988 13 0 0 25 0 1 0 541450522 16891904 3596 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4124 3596 603 41 0 4083 0
vsize: 16496
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3729 0 0 0 24988 14 0 0 25 0 1 0 541450522 17297408 3704 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4223 3704 603 41 0 4182 0
vsize: 16892
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3730 0 0 0 25988 14 0 0 25 0 1 0 541450522 17297408 3705 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4223 3705 603 41 0 4182 0
vsize: 16892
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3730 0 0 0 26988 14 0 0 25 0 1 0 541450522 17297408 3705 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4223 3705 603 41 0 4182 0
vsize: 16892
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3730 0 0 0 27988 14 0 0 25 0 1 0 541450522 17297408 3705 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4223 3705 603 41 0 4182 0
vsize: 16892
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3755 0 0 0 28988 14 0 0 25 0 1 0 541450522 17432576 3730 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4256 3730 603 41 0 4215 0
vsize: 17024
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3820 0 0 0 29988 14 0 0 25 0 1 0 541450522 17698816 3795 4294967295 134512640 134672761 3221224544 3221223648 134555130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4321 3795 603 41 0 4280 0
vsize: 17284
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3820 0 0 0 30988 14 0 0 25 0 1 0 541450522 17698816 3795 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4321 3795 603 41 0 4280 0
vsize: 17284
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3820 0 0 0 31989 14 0 0 25 0 1 0 541450522 17698816 3795 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4321 3795 603 41 0 4280 0
vsize: 17284
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 3857 0 0 0 32988 15 0 0 25 0 1 0 541450522 17829888 3832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4353 3832 603 41 0 4312 0
vsize: 17412
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4098 0 0 0 33989 15 0 0 25 0 1 0 541450522 18763776 4073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4581 4073 603 41 0 4540 0
vsize: 18324
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4315 0 0 0 34988 16 0 0 25 0 1 0 541450522 19689472 4290 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4807 4290 603 41 0 4766 0
vsize: 19228
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4528 0 0 0 35988 16 0 0 25 0 1 0 541450522 20496384 4503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5004 4503 603 41 0 4963 0
vsize: 20016
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4756 0 0 0 36987 17 0 0 25 0 1 0 541450522 21438464 4731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4756 0 0 0 37987 17 0 0 25 0 1 0 541450522 21438464 4731 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4756 0 0 0 38988 17 0 0 25 0 1 0 541450522 21438464 4731 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4756 0 0 0 39988 17 0 0 25 0 1 0 541450522 21438464 4731 4294967295 134512640 134672761 3221224544 3221223728 134558934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4756 0 0 0 40988 17 0 0 25 0 1 0 541450522 21438464 4731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4756 0 0 0 41988 17 0 0 25 0 1 0 541450522 21438464 4731 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4756 0 0 0 42988 17 0 0 25 0 1 0 541450522 21438464 4731 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5234 4731 603 41 0 5193 0
vsize: 20936
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 4814 0 0 0 43988 18 0 0 25 0 1 0 541450522 21704704 4789 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5299 4789 603 41 0 5258 0
vsize: 21196
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5049 0 0 0 44988 18 0 0 25 0 1 0 541450522 22634496 5024 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5526 5024 603 41 0 5485 0
vsize: 22104
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5222 0 0 0 45987 19 0 0 25 0 1 0 541450522 23314432 5197 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5692 5197 603 41 0 5651 0
vsize: 22768
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 46987 19 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 47987 19 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 48987 19 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 49988 19 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223728 134559601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 50988 19 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 51988 19 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 52988 19 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 53987 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 54987 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 55988 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 56988 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223744 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 57988 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 58988 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 59988 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223728 134559345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 60988 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 61988 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 62989 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 63989 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 64989 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 65989 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 66989 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 67990 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 68990 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 69990 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 70990 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 71990 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 72990 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223648 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 73990 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 74991 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 75991 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 76991 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+780.012 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 77991 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+790.012 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 78991 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+800.013 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 79992 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+810.013 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 80992 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+820.013 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 81992 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+830.014 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 82992 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+840.014 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 83992 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+850.015 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 84993 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+860.015 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5321 0 0 0 85993 20 0 0 25 0 1 0 541450522 23707648 5296 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5296 603 41 0 5747 0
vsize: 23152
[startup+870.015 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5322 0 0 0 86993 20 0 0 25 0 1 0 541450522 23707648 5297 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5297 603 41 0 5747 0
vsize: 23152
[startup+880.016 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5322 0 0 0 87993 20 0 0 25 0 1 0 541450522 23707648 5297 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5297 603 41 0 5747 0
vsize: 23152
[startup+890.018 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5322 0 0 0 88994 20 0 0 25 0 1 0 541450522 23707648 5297 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5297 603 41 0 5747 0
vsize: 23152
[startup+900.019 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5322 0 0 0 89994 20 0 0 25 0 1 0 541450522 23707648 5297 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5297 603 41 0 5747 0
vsize: 23152
[startup+910.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5322 0 0 0 90994 20 0 0 25 0 1 0 541450522 23707648 5297 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5788 5297 603 41 0 5747 0
vsize: 23152
[startup+920.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5403 0 0 0 91994 20 0 0 25 0 1 0 541450522 24109056 5378 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5378 603 41 0 5845 0
vsize: 23544
[startup+930.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5600 0 0 0 92993 21 0 0 25 0 1 0 541450522 24907776 5575 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+940.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5600 0 0 0 93994 21 0 0 25 0 1 0 541450522 24907776 5575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+950.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5600 0 0 0 94994 21 0 0 25 0 1 0 541450522 24907776 5575 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+960.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5600 0 0 0 95994 21 0 0 25 0 1 0 541450522 24907776 5575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+970.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5600 0 0 0 96994 21 0 0 25 0 1 0 541450522 24907776 5575 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+980.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5600 0 0 0 97994 21 0 0 25 0 1 0 541450522 24907776 5575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+990.019 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5600 0 0 0 98994 21 0 0 25 0 1 0 541450522 24907776 5575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5600 0 0 0 99995 21 0 0 25 0 1 0 541450522 24907776 5575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5600 0 0 0 100995 21 0 0 25 0 1 0 541450522 24907776 5575 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6081 5575 603 41 0 6040 0
vsize: 24324
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5711 0 0 0 101995 21 0 0 25 0 1 0 541450522 25309184 5686 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6179 5686 603 41 0 6138 0
vsize: 24716
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 5883 0 0 0 102995 21 0 0 25 0 1 0 541450522 26116096 5858 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6376 5858 603 41 0 6335 0
vsize: 25504
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6053 0 0 0 103994 22 0 0 25 0 1 0 541450522 26800128 6028 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6028 603 41 0 6502 0
vsize: 26172
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6065 0 0 0 104995 22 0 0 25 0 1 0 541450522 26800128 6040 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6065 0 0 0 105995 22 0 0 25 0 1 0 541450522 26800128 6040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6065 0 0 0 106995 22 0 0 25 0 1 0 541450522 26800128 6040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6065 0 0 0 107995 22 0 0 25 0 1 0 541450522 26800128 6040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6065 0 0 0 108995 22 0 0 25 0 1 0 541450522 26800128 6040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6065 0 0 0 109996 22 0 0 25 0 1 0 541450522 26800128 6040 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6040 603 41 0 6502 0
vsize: 26172
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6066 0 0 0 110996 22 0 0 25 0 1 0 541450522 26800128 6041 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6041 603 41 0 6502 0
vsize: 26172
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6066 0 0 0 111996 22 0 0 25 0 1 0 541450522 26800128 6041 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6041 603 41 0 6502 0
vsize: 26172
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6066 0 0 0 112996 22 0 0 25 0 1 0 541450522 26800128 6041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6543 6041 603 41 0 6502 0
vsize: 26172
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6134 0 0 0 113996 22 0 0 25 0 1 0 541450522 27070464 6109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6609 6109 603 41 0 6568 0
vsize: 26436
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6341 0 0 0 114995 23 0 0 25 0 1 0 541450522 28139520 6316 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6316 603 41 0 6829 0
vsize: 27480
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6341 0 0 0 115996 23 0 0 25 0 1 0 541450522 28139520 6316 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6316 603 41 0 6829 0
vsize: 27480
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6341 0 0 0 116996 23 0 0 25 0 1 0 541450522 28139520 6316 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6316 603 41 0 6829 0
vsize: 27480
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6341 0 0 0 117996 23 0 0 25 0 1 0 541450522 28139520 6316 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6316 603 41 0 6829 0
vsize: 27480
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6341 0 0 0 118996 23 0 0 25 0 1 0 541450522 28139520 6316 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6870 6316 603 41 0 6829 0
vsize: 27480
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 26283
Raw data (stat): 26283 (minisat+) R 26282 26298 26297 0 -1 0 6351 0 0 0 119996 23 0 0 25 0 1 0 541450522 28282880 6326 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6905 6326 603 41 0 6864 0
vsize: 27620
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 26283
Raw data (stat): 26283 (minisat+) Z 26282 26298 26297 0 -1 12 6354 0 0 0 119997 24 0 0 25 0 1 0 541450522 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.04
CPU time (s): 1200.22
CPU user time (s): 1199.97
CPU system time (s): 0.245962
CPU usage (%): 100.015
Max. virtual memory (Kb): 27620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####