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-markshare2.opb
MD5SUM	b54bb080800e2327586cd478559c04ff
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10368
Optimality of the best value was proved	NO
Number of terms in the objective function	140
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	7340025
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	7340025
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.09
Number of variables	200
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	7
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 15123

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 02:58:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18517 boxname=wulflinc29 idbench=1425 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b54bb080800e2327586cd478559c04ff  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare2.opb
IDLAUNCH: 18517
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        859548 kB
Buffers:          9164 kB
Cached:         137932 kB
SwapCached:        464 kB
Active:          42996 kB
Inactive:       106264 kB
HighTotal:      131008 kB
HighFree:         3444 kB
LowTotal:       903652 kB
LowFree:        856104 kB
SwapTotal:     2097892 kB
SwapFree:      2096700 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            20244 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:18:18 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 18517 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 431615   bits: 20/19
c ---[  10]---> Adder-cost: 380   maxlim: 461183   bits: 20/19
c ---[   8]---> Adder-cost: 350   maxlim: 445183   bits: 20/19
c ---[   6]---> Adder-cost: 340   maxlim: 477951   bits: 20/19
c ---[   4]---> Adder-cost: 390   maxlim: 451839   bits: 20/19
c ---[   2]---> Adder-cost: 358   maxlim: 468735   bits: 20/19
c ---[   0]---> Adder-cost: 374   maxlim: 444543   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17222    61228 |    5740       0        0     nan |  0.000 % |
c |       100 |   17222    61228 |    6314     100      905     9.1 |  9.969 % |
c |       253 |   17214    61202 |    6945     252     2033     8.1 | 10.003 % |
c |       478 |   17206    61176 |    7639     476     4722     9.9 | 10.038 % |
c ==============================================================================
c [1mFound solution: 866304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1068     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       536 |   19853    67360 |    6617     534     5740    10.7 | 10.038 % |
c ==============================================================================
c [1mFound solution: 828672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       632 |   19863    67400 |    6621     629    13956    22.2 | 10.038 % |
c |       733 |   19863    67400 |    7283     730    20234    27.7 |  7.644 % |
c |       884 |   19855    67374 |    8011     879    45616    51.9 |  7.696 % |
c |      1110 |   19847    67348 |    8812    1105    70591    63.9 |  7.696 % |
c |      1447 |   19839    67322 |    9693    1441    95879    66.5 |  7.723 % |
c ==============================================================================
c [1mFound solution: 702720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1945 |   19842    67325 |    6614    1938   159401    82.3 |  7.723 % |
c |      2046 |   19842    67325 |    7275    2039   167910    82.3 |  7.761 % |
c |      2197 |   19842    67325 |    8002    2190   179220    81.8 |  7.761 % |
c |      2423 |   19842    67325 |    8803    2416   196028    81.1 |  7.761 % |
c |      2761 |   19842    67325 |    9683    2754   236792    86.0 |  7.761 % |
c |      3268 |   19842    67325 |   10651    3261   287766    88.2 |  7.761 % |
c ==============================================================================
c [1mFound solution: 676352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3715 |   19858    67370 |    6619    3708   318920    86.0 |  7.761 % |
c |      3815 |   19858    67370 |    7280    3808   328892    86.4 |  7.766 % |
c |      3965 |   19858    67370 |    8008    3958   346566    87.6 |  7.766 % |
c |      4190 |   19858    67370 |    8809    4183   366380    87.6 |  7.766 % |
c |      4528 |   19852    67357 |    9690    4520   400494    88.6 |  7.819 % |
c |      5034 |   19844    67331 |   10659    5025   444892    88.5 |  7.845 % |
c |      5794 |   19836    67305 |   11725    5784   509124    88.0 |  7.871 % |
c |      6934 |   19828    67279 |   12898    6923   580155    83.8 |  7.897 % |
c ==============================================================================
c [1mFound solution: 674304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7359 |   19838    67302 |    6612    7348   621804    84.6 |  7.897 % |
c |      7463 |   19838    67302 |    7273    3778   243653    64.5 |  7.913 % |
c |      7614 |   19838    67302 |    8000    3929   255506    65.0 |  7.913 % |
c ==============================================================================
c [1mFound solution: 654336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7790 |   19849    67335 |    6616    4105   268736    65.5 |  7.913 % |
c ==============================================================================
c [1mFound solution: 645120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7856 |   19857    67359 |    6619    4171   271081    65.0 |  7.913 % |
c |      7958 |   19857    67359 |    7280    4273   278513    65.2 |  7.938 % |
c ==============================================================================
c [1mFound solution: 465408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8075 |   19869    67387 |    6623    4390   284865    64.9 |  7.938 % |
c |      8175 |   19869    67387 |    7285    4490   290752    64.8 |  7.949 % |
c |      8326 |   19869    67387 |    8013    4641   302249    65.1 |  7.949 % |
c |      8551 |   19869    67387 |    8815    4866   312895    64.3 |  7.949 % |
c |      8888 |   19869    67387 |    9696    5203   337269    64.8 |  7.949 % |
c |      9394 |   19869    67387 |   10666    5709   372234    65.2 |  7.949 % |
c |     10153 |   19869    67387 |   11733    6468   427615    66.1 |  7.949 % |
c |     11294 |   19869    67387 |   12906    7609   506572    66.6 |  7.949 % |
c |     13003 |   19863    67369 |   14196    9317   680687    73.1 |  7.975 % |
c |     15565 |   19838    67290 |   15616   11876   979173    82.4 |  8.079 % |
c |     19410 |   19838    67290 |   17178   15721  1427200    90.8 |  8.079 % |
c ==============================================================================
c [1mFound solution: 426240[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24555 |   19802    67164 |    6600   11781   991951    84.2 |  8.079 % |
c |     24656 |   19802    67164 |    7260    5992   340445    56.8 |  8.251 % |
c |     24806 |   19802    67164 |    7986    6142   346020    56.3 |  8.251 % |
c |     25031 |   19802    67164 |    8784    6367   351779    55.3 |  8.251 % |
c |     25370 |   19802    67164 |    9663    6706   376621    56.2 |  8.251 % |
c |     25878 |   19802    67164 |   10629    7214   412120    57.1 |  8.251 % |
c |     26639 |   19802    67164 |   11692    7975   454198    57.0 |  8.251 % |
c |     27779 |   19802    67164 |   12861    9115   506655    55.6 |  8.251 % |
c |     29487 |   19802    67164 |   14147   10823   597522    55.2 |  8.251 % |
c |     32049 |   19802    67164 |   15562   13385   746703    55.8 |  8.251 % |
c |     35893 |   19802    67164 |   17118    9134   445739    48.8 |  8.251 % |
c |     41660 |   19802    67164 |   18830   14901   900002    60.4 |  8.251 % |
c |     50309 |   19802    67164 |   20713   13630   900207    66.0 |  8.251 % |
c |     63285 |   19802    67164 |   22784   15643   876282    56.0 |  8.251 % |
c |     82746 |   19802    67164 |   25063   23100  1569191    67.9 |  8.251 % |
c ==============================================================================
c [1mFound solution: 420352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110809 |   19810    67183 |    6603   24998  2030699    81.2 |  8.251 % |
c |    110909 |   19810    67183 |    7263    6350   368699    58.1 |  8.269 % |
c |    111061 |   19810    67183 |    7989    6502   374493    57.6 |  8.269 % |
c |    111288 |   19810    67183 |    8788    6729   385690    57.3 |  8.269 % |
c |    111626 |   19810    67183 |    9667    7067   413477    58.5 |  8.269 % |
c |    112132 |   19810    67183 |   10634    7573   438726    57.9 |  8.269 % |
c |    112891 |   19810    67183 |   11697    8332   475591    57.1 |  8.269 % |
c |    114031 |   19810    67183 |   12867    9472   602990    63.7 |  8.269 % |
c |    115740 |   19810    67183 |   14154   11181   705503    63.1 |  8.269 % |
c ==============================================================================
c [1mFound solution: 411392[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    118101 |   19822    67210 |    6607   13542   911670    67.3 |  8.269 % |
c |    118201 |   19822    67210 |    7267    6871   405686    59.0 |  8.282 % |
c |    118351 |   19822    67210 |    7994    7021   414241    59.0 |  8.282 % |
c |    118576 |   19822    67210 |    8793    7246   434055    59.9 |  8.282 % |
c |    118913 |   19822    67210 |    9673    7583   456334    60.2 |  8.282 % |
c |    119419 |   19822    67210 |   10640    8089   483898    59.8 |  8.282 % |
c |    120178 |   19822    67210 |   11704    8848   528469    59.7 |  8.282 % |
c |    121317 |   19822    67210 |   12875    9987   592730    59.4 |  8.282 % |
c |    123025 |   19822    67210 |   14162   11695   721731    61.7 |  8.282 % |
c |    125587 |   19822    67210 |   15578   14257   897308    62.9 |  8.282 % |
c |    129431 |   19822    67210 |   17136    9873   539594    54.7 |  8.282 % |
c |    135198 |   19814    67184 |   18850   15639  1121030    71.7 |  8.308 % |
c |    143849 |   19814    67184 |   20735   14328   969560    67.7 |  8.308 % |
c ==============================================================================
c [1mFound solution: 404480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    151309 |   19816    67186 |    6605   11073   646615    58.4 |  8.308 % |
c |    151411 |   19816    67186 |    7265    5639   309058    54.8 |  8.374 % |
c |    151561 |   19816    67186 |    7992    5789   311658    53.8 |  8.374 % |
c |    151786 |   19816    67186 |    8791    6014   337987    56.2 |  8.374 % |
c |    152124 |   19816    67186 |    9670    6352   350939    55.2 |  8.374 % |
c ==============================================================================
c [1mFound solution: 363264[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    152583 |   19829    67218 |    6609    6811   361631    53.1 |  8.374 % |
c |    152685 |   19829    67218 |    7269    6913   366844    53.1 |  8.385 % |
c |    152836 |   19829    67218 |    7996    7064   390436    55.3 |  8.385 % |
c |    153061 |   19829    67218 |    8796    7289   402314    55.2 |  8.385 % |
c |    153398 |   19829    67218 |    9676    7626   416355    54.6 |  8.385 % |
c |    153907 |   19829    67218 |   10643    8135   436418    53.6 |  8.385 % |
c |    154667 |   19829    67218 |   11708    8895   517597    58.2 |  8.385 % |
c |    155807 |   19829    67218 |   12879   10035   580468    57.8 |  8.385 % |
c |    157517 |   19829    67218 |   14166   11745   642591    54.7 |  8.385 % |
c |    160079 |   19829    67218 |   15583   14307   764160    53.4 |  8.385 % |
c ==============================================================================
c [1mFound solution: 343936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    162554 |   19860    67292 |    6620    8590   324198    37.7 |  8.385 % |
c |    162655 |   19860    67292 |    7282    4396   151608    34.5 |  8.372 % |
c |    162807 |   19860    67292 |    8010    4548   161742    35.6 |  8.372 % |
c |    163033 |   19860    67292 |    8811    4774   168934    35.4 |  8.372 % |
c |    163371 |   19860    67292 |    9692    5112   176581    34.5 |  8.372 % |
c |    163877 |   19860    67292 |   10661    5618   253166    45.1 |  8.372 % |
c |    164636 |   19860    67292 |   11727    6377   301500    47.3 |  8.372 % |
c |    165778 |   19860    67292 |   12900    7519   356921    47.5 |  8.372 % |
c |    167486 |   19860    67292 |   14190    9227   445248    48.3 |  8.372 % |
c |    170048 |   19860    67292 |   15609   11789   602596    51.1 |  8.372 % |
c |    173892 |   19860    67292 |   17170   15633   831926    53.2 |  8.372 % |
c |    179659 |   19860    67292 |   18887   12423   597867    48.1 |  8.372 % |
c |    188308 |   19848    67265 |   20776   11130   791462    71.1 |  8.449 % |
c ==============================================================================
c [1mFound solution: 260352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    188746 |   19854    67281 |    6618   11568   801463    69.3 |  8.449 % |
c |    188847 |   19854    67281 |    7279    5885   256847    43.6 |  8.465 % |
c |    188997 |   19854    67281 |    8007    6035   266435    44.1 |  8.465 % |
c |    189223 |   19854    67281 |    8808    6261   281425    44.9 |  8.465 % |
c |    189561 |   19854    67281 |    9689    6599   298712    45.3 |  8.465 % |
c |    190067 |   19854    67281 |   10658    7105   319291    44.9 |  8.465 % |
c |    190827 |   19854    67281 |   11724    7865   359467    45.7 |  8.465 % |
c |    191968 |   19854    67281 |   12896    9006   410789    45.6 |  8.465 % |
c |    193677 |   19854    67281 |   14186   10715   531399    49.6 |  8.465 % |
c |    196241 |   19854    67281 |   15604   13279   685851    51.6 |  8.465 % |
c |    200085 |   19854    67281 |   17165    8898   488070    54.9 |  8.465 % |
c |    205852 |   19854    67281 |   18881   14665   711080    48.5 |  8.465 % |
c ==============================================================================
c [1mFound solution: 80128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    206193 |   19806    67113 |    6602   14727   700340    47.6 |  8.465 % |
c |    206293 |   19806    67113 |    7262    3782   103785    27.4 |  8.666 % |
c |    206444 |   19806    67113 |    7988    3933   104553    26.6 |  8.666 % |
c |    206669 |   19806    67113 |    8787    4158   107432    25.8 |  8.666 % |
c |    207006 |   19806    67113 |    9665    4495   116514    25.9 |  8.666 % |
c |    207513 |   19806    67113 |   10632    5002   128589    25.7 |  8.666 % |
c ==============================================================================
c [1mFound solution: 64896[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    207893 |   19615    66613 |    6538    5362   135046    25.2 |  8.666 % |
c |    207995 |   19615    66613 |    7191    5464   137131    25.1 | 10.089 % |
c |    208146 |   19615    66613 |    7910    5615   139840    24.9 | 10.089 % |
c |    208371 |   19615    66613 |    8702    5840   147321    25.2 | 10.089 % |
c |    208708 |   19615    66613 |    9572    6177   155749    25.2 | 10.089 % |
c |    209215 |   19615    66613 |   10529    6684   179508    26.9 | 10.089 % |
c |    209976 |   19615    66613 |   11582    7445   201615    27.1 | 10.089 % |
c |    211115 |   19615    66613 |   12740    8584   243072    28.3 | 10.089 % |
c |    212823 |   19615    66613 |   14014   10292   303964    29.5 | 10.089 % |
c |    215385 |   19615    66613 |   15416   12854   404034    31.4 | 10.089 % |
c |    219229 |   19615    66613 |   16957    8598   318726    37.1 | 10.089 % |
c ==============================================================================
c [1mFound solution: 63616[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    222041 |   19622    66634 |    6540   11410   477534    41.9 | 10.089 % |
c |    222143 |   19622    66634 |    7194    5807   236093    40.7 | 10.102 % |
c |    222293 |   19622    66634 |    7913    5957   236962    39.8 | 10.102 % |
c |    222518 |   19622    66634 |    8704    6182   240201    38.9 | 10.102 % |
c |    222855 |   19622    66634 |    9575    6519   253550    38.9 | 10.102 % |
c |    223361 |   19622    66634 |   10532    7025   263589    37.5 | 10.102 % |
c |    224121 |   19622    66634 |   11586    7785   284201    36.5 | 10.102 % |
c |    225260 |   19622    66634 |   12744    8924   354542    39.7 | 10.102 % |
c |    226971 |   19622    66634 |   14019   10635   414350    39.0 | 10.102 % |
c |    229533 |   19622    66634 |   15420   13197   533639    40.4 | 10.102 % |
c |    233377 |   19607    66589 |   16963    8676   346338    39.9 | 10.179 % |
c |    239144 |   19607    66589 |   18659   14443   554456    38.4 | 10.179 % |
c |    247793 |   19530    66415 |   20525   13278   517714    39.0 | 10.816 % |
c |    260769 |   19429    66185 |   22577   15427   982742    63.7 | 11.633 % |
c |    280230 |   19319    65931 |   24835   23197  1024138    44.1 | 12.628 % |
c |    309423 |   19319    65931 |   27319   25948  1521579    58.6 | 12.628 % |
c ==============================================================================
c [1mFound solution: 59008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    327090 |   19320    65935 |    6440   27848  1354853    48.7 | 12.628 % |
c |    327191 |   19320    65935 |    7084    6666   249277    37.4 | 12.732 % |
c |    327341 |   19320    65935 |    7792    6816   250694    36.8 | 12.732 % |
c |    327566 |   19320    65935 |    8571    7041   259558    36.9 | 12.732 % |
c |    327904 |   19320    65935 |    9428    7379   266686    36.1 | 12.732 % |
c |    328410 |   19320    65935 |   10371    7885   277400    35.2 | 12.732 % |
c |    329171 |   19320    65935 |   11408    8646   299566    34.6 | 12.732 % |
c |    330310 |   19320    65935 |   12549    9785   331642    33.9 | 12.732 % |
c |    332018 |   19320    65935 |   13804   11493   456254    39.7 | 12.732 % |
c |    334582 |   19320    65935 |   15185   14057   533507    38.0 | 12.732 % |
c |    338428 |   19320    65935 |   16703    9687   452672    46.7 | 12.732 % |
c |    344195 |   19320    65935 |   18374   15454   704774    45.6 | 12.732 % |
c |    352844 |   19306    65902 |   20211   14334   779072    54.4 | 12.911 % |
c |    365818 |   19288    65862 |   22232   16842   680144    40.4 | 13.038 % |
c |    385280 |   19288    65862 |   24455   13318   512736    38.5 | 13.038 % |
c |    414473 |   19288    65862 |   26901   17159   819651    47.8 | 13.038 % |
c |    458262 |   19259    65797 |   29591   16835   605068    35.9 | 13.242 % |
c |    523948 |   19241    65756 |   32550   15348   637855    41.6 | 13.369 % |
c |    622474 |   19241    65756 |   35805   17341   946468    54.6 | 13.369 % |
#### 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.41 0.80 0.86 2/54 21483
Raw data (stat): 21483 (runsolver) R 21482 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541656639 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.50 0.80 0.86 2/54 21483
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 1346 0 0 0 995 3 0 0 25 0 1 0 541656639 7172096 1324 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1751 1324 603 41 0 1710 0
vsize: 7004
[startup+20.0012 s]
Raw data (loadavg): 0.58 0.81 0.86 2/54 21483
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 1476 0 0 0 1994 4 0 0 25 0 1 0 541656639 7696384 1454 4294967295 134512640 134672761 3221224624 3221223780 134560075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1879 1454 603 41 0 1838 0
vsize: 7516
[startup+30.0019 s]
Raw data (loadavg): 0.64 0.81 0.86 2/54 21483
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 1821 0 0 0 2992 6 0 0 25 0 1 0 541656639 9023488 1799 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1799 603 41 0 2162 0
vsize: 8812
[startup+40.0031 s]
Raw data (loadavg): 0.70 0.82 0.87 2/54 21483
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2177 0 0 0 3991 7 0 0 25 0 1 0 541656639 10485760 2155 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2560 2155 603 41 0 2519 0
vsize: 10240
[startup+50.0039 s]
Raw data (loadavg): 0.74 0.83 0.87 2/54 21483
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2504 0 0 0 4990 9 0 0 25 0 1 0 541656639 11915264 2482 4294967295 134512640 134672761 3221224624 3221223808 134559363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2909 2482 603 41 0 2868 0
vsize: 11636
[startup+60.0033 s]
Raw data (loadavg): 0.78 0.83 0.87 2/54 21483
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2666 0 0 0 5989 10 0 0 25 0 1 0 541656639 12574720 2644 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2644 603 41 0 3029 0
vsize: 12280
[startup+70.0045 s]
Raw data (loadavg): 0.81 0.84 0.87 2/54 21483
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2666 0 0 0 6989 10 0 0 25 0 1 0 541656639 12574720 2644 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2644 603 41 0 3029 0
vsize: 12280
[startup+80.0056 s]
Raw data (loadavg): 0.84 0.84 0.87 2/54 21483
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2666 0 0 0 7989 10 0 0 25 0 1 0 541656639 12574720 2644 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2644 603 41 0 3029 0
vsize: 12280
[startup+90.0057 s]
Raw data (loadavg): 0.87 0.85 0.87 2/54 21483
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2666 0 0 0 8989 11 0 0 25 0 1 0 541656639 12574720 2644 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2644 603 41 0 3029 0
vsize: 12280
[startup+100.006 s]
Raw data (loadavg): 0.89 0.85 0.87 2/54 21483
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2667 0 0 0 9988 11 0 0 25 0 1 0 541656639 12574720 2645 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3070 2645 603 41 0 3029 0
vsize: 12280
[startup+110.006 s]
Raw data (loadavg): 0.90 0.85 0.87 3/57 21522
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2667 0 0 0 10988 11 0 0 25 0 1 0 541656639 12574720 2645 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3070 2645 603 41 0 3029 0
vsize: 12280
[startup+120.007 s]
Raw data (loadavg): 0.99 0.88 0.88 2/54 21536
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2669 0 0 0 11988 11 0 0 25 0 1 0 541656639 12574720 2647 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3070 2647 603 41 0 3029 0
vsize: 12280
[startup+130.007 s]
Raw data (loadavg): 0.99 0.88 0.88 2/54 21536
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2669 0 0 0 12988 11 0 0 25 0 1 0 541656639 12574720 2647 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3070 2647 603 41 0 3029 0
vsize: 12280
[startup+140.008 s]
Raw data (loadavg): 0.99 0.88 0.88 2/54 21536
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2670 0 0 0 13988 11 0 0 25 0 1 0 541656639 12574720 2648 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3070 2648 603 41 0 3029 0
vsize: 12280
[startup+150.008 s]
Raw data (loadavg): 0.99 0.89 0.88 2/54 21536
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2735 0 0 0 14989 11 0 0 25 0 1 0 541656639 12840960 2713 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3135 2713 603 41 0 3094 0
vsize: 12540
[startup+160.008 s]
Raw data (loadavg): 0.99 0.89 0.88 2/54 21536
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2735 0 0 0 15989 11 0 0 25 0 1 0 541656639 12840960 2713 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3135 2713 603 41 0 3094 0
vsize: 12540
[startup+170.009 s]
Raw data (loadavg): 0.99 0.89 0.88 2/54 21536
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 2841 0 0 0 16988 12 0 0 25 0 1 0 541656639 13238272 2819 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3232 2819 603 41 0 3191 0
vsize: 12928
[startup+180.009 s]
Raw data (loadavg): 0.99 0.89 0.88 2/54 21536
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3090 0 0 0 17988 13 0 0 25 0 1 0 541656639 14307328 3068 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3493 3068 603 41 0 3452 0
vsize: 13972
[startup+190.009 s]
Raw data (loadavg): 0.99 0.90 0.89 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3090 0 0 0 18988 13 0 0 25 0 1 0 541656639 14307328 3068 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3493 3068 603 41 0 3452 0
vsize: 13972
[startup+200.01 s]
Raw data (loadavg): 0.99 0.90 0.89 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3090 0 0 0 19988 13 0 0 25 0 1 0 541656639 14307328 3068 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3493 3068 603 41 0 3452 0
vsize: 13972
[startup+210.009 s]
Raw data (loadavg): 0.99 0.90 0.89 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3273 0 0 0 20987 14 0 0 25 0 1 0 541656639 14974976 3251 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3656 3251 603 41 0 3615 0
vsize: 14624
[startup+220.01 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3307 0 0 0 21988 14 0 0 25 0 1 0 541656639 15106048 3285 4294967295 134512640 134672761 3221224624 3221223824 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3688 3285 603 41 0 3647 0
vsize: 14752
[startup+230.01 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3307 0 0 0 22988 14 0 0 25 0 1 0 541656639 15106048 3285 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3688 3285 603 41 0 3647 0
vsize: 14752
[startup+240.01 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3336 0 0 0 23988 14 0 0 25 0 1 0 541656639 15237120 3314 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3314 603 41 0 3679 0
vsize: 14880
[startup+250.01 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 24987 14 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+260.01 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 25987 14 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+270.01 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 26986 14 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+280.01 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 27986 14 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+290.01 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 28986 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+300.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 29986 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+310.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 30987 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+320.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 31987 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+330.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 32987 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223728 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+340.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 33987 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+350.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 34987 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+360.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 35987 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+370.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 36987 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223808 134558632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+380.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 37987 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+390.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 38987 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+400.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 39988 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+410.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 40988 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+420.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 41988 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+430.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 42988 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+440.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 43988 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+450.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 44988 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+460.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21538
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 45988 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+470.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 46988 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+480.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 47989 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223808 134559156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+490.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 48989 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+500.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3360 0 0 0 49989 15 0 0 25 0 1 0 541656639 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3338 603 41 0 3711 0
vsize: 15008
[startup+510.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3361 0 0 0 50989 15 0 0 25 0 1 0 541656639 15368192 3339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3339 603 41 0 3711 0
vsize: 15008
[startup+520.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3361 0 0 0 51989 15 0 0 25 0 1 0 541656639 15368192 3339 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3339 603 41 0 3711 0
vsize: 15008
[startup+530.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3361 0 0 0 52990 15 0 0 25 0 1 0 541656639 15368192 3339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3339 603 41 0 3711 0
vsize: 15008
[startup+540.011 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 53990 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223808 134559482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+550.011 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 54990 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+560.011 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 55990 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+570.011 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 56990 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+580.011 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 57990 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+590.011 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 58990 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223716 1075351142 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+600.012 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 59991 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+610.012 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 60991 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+620.013 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 61991 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+630.013 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 62991 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+640.013 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 63991 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+650.013 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 64992 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+660.012 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 65992 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+670.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 66992 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223808 134559373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+680.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 67992 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+690.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 68992 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+700.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3362 0 0 0 69992 16 0 0 25 0 1 0 541656639 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3340 603 41 0 3711 0
vsize: 15008
[startup+710.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3363 0 0 0 70993 16 0 0 25 0 1 0 541656639 15368192 3341 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3341 603 41 0 3711 0
vsize: 15008
[startup+720.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3363 0 0 0 71993 16 0 0 25 0 1 0 541656639 15368192 3341 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3341 603 41 0 3711 0
vsize: 15008
[startup+730.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3363 0 0 0 72993 16 0 0 25 0 1 0 541656639 15368192 3341 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3341 603 41 0 3711 0
vsize: 15008
[startup+740.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3364 0 0 0 73993 16 0 0 25 0 1 0 541656639 15368192 3342 4294967295 134512640 134672761 3221224624 3221223808 134559367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3342 603 41 0 3711 0
vsize: 15008
[startup+750.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3365 0 0 0 74993 16 0 0 25 0 1 0 541656639 15368192 3343 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3343 603 41 0 3711 0
vsize: 15008
[startup+760.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3365 0 0 0 75993 16 0 0 25 0 1 0 541656639 15368192 3343 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3752 3343 603 41 0 3711 0
vsize: 15008
[startup+770.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3498 0 0 0 76993 16 0 0 25 0 1 0 541656639 15904768 3476 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3883 3476 603 41 0 3842 0
vsize: 15532
[startup+780.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3669 0 0 0 77993 17 0 0 25 0 1 0 541656639 16572416 3647 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3647 603 41 0 4005 0
vsize: 16184
[startup+790.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3672 0 0 0 78993 17 0 0 25 0 1 0 541656639 16707584 3650 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4079 3650 603 41 0 4038 0
vsize: 16316
[startup+800.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3688 0 0 0 79993 17 0 0 25 0 1 0 541656639 16707584 3666 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4079 3666 603 41 0 4038 0
vsize: 16316
[startup+810.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3692 0 0 0 80993 17 0 0 25 0 1 0 541656639 16707584 3670 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4079 3670 603 41 0 4038 0
vsize: 16316
[startup+820.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3692 0 0 0 81993 17 0 0 25 0 1 0 541656639 16707584 3670 4294967295 134512640 134672761 3221224624 3221223792 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4079 3670 603 41 0 4038 0
vsize: 16316
[startup+830.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3692 0 0 0 82993 17 0 0 25 0 1 0 541656639 16707584 3670 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4079 3670 603 41 0 4038 0
vsize: 16316
[startup+840.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3692 0 0 0 83992 17 0 0 25 0 1 0 541656639 16707584 3670 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4079 3670 603 41 0 4038 0
vsize: 16316
[startup+850.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3692 0 0 0 84993 17 0 0 25 0 1 0 541656639 16707584 3670 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4079 3670 603 41 0 4038 0
vsize: 16316
[startup+860.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3739 0 0 0 85993 17 0 0 25 0 1 0 541656639 17108992 3717 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4177 3717 603 41 0 4136 0
vsize: 16708
[startup+870.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3741 0 0 0 86993 17 0 0 25 0 1 0 541656639 17108992 3719 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4177 3719 603 41 0 4136 0
vsize: 16708
[startup+880.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3752 0 0 0 87993 18 0 0 25 0 1 0 541656639 17108992 3730 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4177 3730 603 41 0 4136 0
vsize: 16708
[startup+890.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 3924 0 0 0 88992 18 0 0 25 0 1 0 541656639 17776640 3902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4340 3902 603 41 0 4299 0
vsize: 17360
[startup+900.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4076 0 0 0 89992 19 0 0 25 0 1 0 541656639 18440192 4054 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4502 4054 603 41 0 4461 0
vsize: 18008
[startup+910.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4082 0 0 0 90992 19 0 0 25 0 1 0 541656639 18440192 4060 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4502 4060 603 41 0 4461 0
vsize: 18008
[startup+920.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4100 0 0 0 91992 19 0 0 25 0 1 0 541656639 18575360 4078 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4535 4078 603 41 0 4494 0
vsize: 18140
[startup+930.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4107 0 0 0 92993 19 0 0 25 0 1 0 541656639 18575360 4085 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4535 4085 603 41 0 4494 0
vsize: 18140
[startup+940.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4194 0 0 0 93993 19 0 0 25 0 1 0 541656639 18972672 4172 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4632 4172 603 41 0 4591 0
vsize: 18528
[startup+950.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4200 0 0 0 94993 19 0 0 25 0 1 0 541656639 18972672 4178 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4632 4178 603 41 0 4591 0
vsize: 18528
[startup+960.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4213 0 0 0 95993 19 0 0 25 0 1 0 541656639 19128320 4191 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4191 603 41 0 4629 0
vsize: 18680
[startup+970.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4220 0 0 0 96993 19 0 0 25 0 1 0 541656639 19128320 4198 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4198 603 41 0 4629 0
vsize: 18680
[startup+980.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4245 0 0 0 97993 19 0 0 25 0 1 0 541656639 19128320 4223 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4223 603 41 0 4629 0
vsize: 18680
[startup+990.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4245 0 0 0 98993 19 0 0 25 0 1 0 541656639 19128320 4223 4294967295 134512640 134672761 3221224624 3221223792 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4223 603 41 0 4629 0
vsize: 18680
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4255 0 0 0 99993 19 0 0 25 0 1 0 541656639 19271680 4233 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4705 4233 603 41 0 4664 0
vsize: 18820
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4257 0 0 0 100994 19 0 0 25 0 1 0 541656639 19271680 4235 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4705 4235 603 41 0 4664 0
vsize: 18820
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4335 0 0 0 101993 20 0 0 25 0 1 0 541656639 19533824 4313 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4769 4313 603 41 0 4728 0
vsize: 19076
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4335 0 0 0 102993 20 0 0 25 0 1 0 541656639 19533824 4313 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4769 4313 603 41 0 4728 0
vsize: 19076
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4338 0 0 0 103993 20 0 0 25 0 1 0 541656639 19533824 4316 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4769 4316 603 41 0 4728 0
vsize: 19076
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4363 0 0 0 104993 20 0 0 25 0 1 0 541656639 19668992 4341 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4802 4341 603 41 0 4761 0
vsize: 19208
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4479 0 0 0 105993 20 0 0 25 0 1 0 541656639 20201472 4457 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4457 603 41 0 4891 0
vsize: 19728
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4479 0 0 0 106993 20 0 0 25 0 1 0 541656639 20201472 4457 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4457 603 41 0 4891 0
vsize: 19728
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4482 0 0 0 107993 20 0 0 25 0 1 0 541656639 20201472 4460 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4460 603 41 0 4891 0
vsize: 19728
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4482 0 0 0 108994 20 0 0 25 0 1 0 541656639 20201472 4460 4294967295 134512640 134672761 3221224624 3221223728 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4460 603 41 0 4891 0
vsize: 19728
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4485 0 0 0 109994 20 0 0 25 0 1 0 541656639 20201472 4463 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4463 603 41 0 4891 0
vsize: 19728
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4485 0 0 0 110994 20 0 0 25 0 1 0 541656639 20201472 4463 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4463 603 41 0 4891 0
vsize: 19728
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4485 0 0 0 111994 20 0 0 25 0 1 0 541656639 20201472 4463 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4463 603 41 0 4891 0
vsize: 19728
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4496 0 0 0 112994 20 0 0 25 0 1 0 541656639 20201472 4474 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4474 603 41 0 4891 0
vsize: 19728
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4496 0 0 0 113994 20 0 0 25 0 1 0 541656639 20201472 4474 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4474 603 41 0 4891 0
vsize: 19728
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4497 0 0 0 114995 20 0 0 25 0 1 0 541656639 20201472 4475 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4932 4475 603 41 0 4891 0
vsize: 19728
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4505 0 0 0 115995 20 0 0 25 0 1 0 541656639 20340736 4483 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4966 4483 603 41 0 4925 0
vsize: 19864
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4519 0 0 0 116995 20 0 0 25 0 1 0 541656639 20340736 4497 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4966 4497 603 41 0 4925 0
vsize: 19864
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4520 0 0 0 117995 20 0 0 25 0 1 0 541656639 20340736 4498 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4966 4498 603 41 0 4925 0
vsize: 19864
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4520 0 0 0 118995 20 0 0 25 0 1 0 541656639 20340736 4498 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4966 4498 603 41 0 4925 0
vsize: 19864
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21540
Raw data (stat): 21483 (minisat+) R 21482 27222 27221 0 -1 0 4520 0 0 0 119995 20 0 0 25 0 1 0 541656639 20340736 4498 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4966 4498 603 41 0 4925 0
vsize: 19864
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 21540
Raw data (stat): 21483 (minisat+) Z 21482 27222 27221 0 -1 12 4523 0 0 0 119996 21 0 0 25 0 1 0 541656639 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.18
CPU user time (s): 1199.96
CPU system time (s): 0.216967
CPU usage (%): 100.012
Max. virtual memory (Kb): 19864
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####