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/submitted/manquinho/routing/normalized-s4-4-3-5pb.opb
MD5SUM	4ca29b1bc7e76812f7871e2b937d8a23
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	60
Optimality of the best value was proved	NO
Number of terms in the objective function	720
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	720
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	720
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	720
Total number of constraints	2168
Number of constraints which are clauses	2144
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	30
Trace number 5196

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-13 22:21:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3625 boxname=wulflinc17 idbench=241 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4ca29b1bc7e76812f7871e2b937d8a23  /oldhome/oroussel/tmp/wulflinc17/normalized-s4-4-3-5pb.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc17/normalized-s4-4-3-5pb.opb /oldhome/oroussel/tmp/wulflinc17/normalized-s4-4-3-5pb.opb
IDLAUNCH: 3625
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        830244 kB
Buffers:         34372 kB
Cached:         135564 kB
SwapCached:       2376 kB
Active:          53428 kB
Inactive:       121924 kB
HighTotal:      131008 kB
HighFree:         2576 kB
LowTotal:       903652 kB
LowFree:        827668 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23504 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:41:57 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3625 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2168 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2119]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2109]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2099]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2097]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2083]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2057]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2035]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2025]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1976]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1966]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1956]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1954]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1940]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1914]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1892]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1882]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1864]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1842]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1816]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1810]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1808]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1782]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1765]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1739]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1733]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1715]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1677]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1667]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1630]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1608]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1602]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1596]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1563]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1537]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1535]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1525]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1488]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1466]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1460]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1454]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1452]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1426]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1409]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1383]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1377]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1359]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1322]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1312]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1298]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1272]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1250]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1222]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1200]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1174]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1158]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1148]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1098]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1096]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1047]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1037]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1027]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1025]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1023]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 997]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 979]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 953]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 935]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 914]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 888]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 882]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 864]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 842]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 816]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 810]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 804]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 786]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 749]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 739]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 721]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 700]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 674]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 668]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 654]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 629]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 607]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 597]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 564]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 538]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 536]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 526]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 477]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 467]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 457]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 455]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 437]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 415]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 389]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 383]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 381]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 355]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 337]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 311]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 305]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 287]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 249]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 239]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 186]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 176]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 170]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 154]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 128]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 106]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  96]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  78]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  56]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  30]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  22]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  21]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  20]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  19]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  18]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  17]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  16]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  15]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  14]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  13]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  12]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  11]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[  10]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[   9]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[   8]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[   7]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[   6]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[   5]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[   4]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[   3]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[   2]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[   1]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ---[   0]---> Adder-cost: 52   maxlim: 26   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10568    36624 |    3522       0        0     nan |  0.000 % |
c |       100 |   10505    36417 |    3874      91      433     4.8 | 20.375 % |
c |       250 |   10420    36140 |    4261     230     1211     5.3 | 21.000 % |
c |       476 |   10324    35828 |    4687     444     2206     5.0 | 21.750 % |
c |       813 |   10215    35467 |    5156     765     4028     5.3 | 22.625 % |
c |      1319 |   10142    35220 |    5672    1259     7257     5.8 | 23.125 % |
c |      2079 |   10043    34887 |    6239    2005    14252     7.1 | 23.875 % |
c |      3218 |    9830    34164 |    6863    3095    27639     8.9 | 25.375 % |
c |      4927 |    9746    33876 |    7549    4781    50580    10.6 | 25.875 % |
c |      7490 |    9746    33876 |    8304    7344   125664    17.1 | 25.875 % |
c |     11334 |    9737    33845 |    9135    6512   161532    24.8 | 25.917 % |
c |     17103 |    9671    33621 |   10048    7244   131918    18.2 | 26.375 % |
c |     25753 |    9647    33539 |   11053   10503   161236    15.4 | 26.542 % |
c |     38727 |    9604    33388 |   12158   11811   346737    29.4 | 26.750 % |
c |     58189 |    9565    33255 |   13374   11498   331833    28.9 | 27.000 % |
c |     87382 |    9511    33069 |   14712   12372   281984    22.8 | 27.333 % |
c |    131172 |    9445    32847 |   16183    9645   250328    26.0 | 27.750 % |
c |    196858 |    9430    32796 |   17801   16115   356239    22.1 | 27.833 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1432   maxlim: 648   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    215323 |   19381    68320 |    6460   16074   320840    20.0 | 27.833 % |
c |    215426 |   19381    68320 |    7106    4122    58648    14.2 | 17.627 % |
c |    215576 |   19381    68320 |    7816    4272    60843    14.2 | 17.627 % |
c |    215803 |   19381    68320 |    8598    4499    64224    14.3 | 17.627 % |
c |    216142 |   19373    68290 |    9458    4837    71025    14.7 | 17.653 % |
c |    216650 |   19364    68261 |   10403    5344    83425    15.6 | 17.705 % |
c |    217411 |   19364    68261 |   11444    6105   102844    16.8 | 17.705 % |
c |    218550 |   19364    68261 |   12588    7244   134719    18.6 | 17.705 % |
c |    220260 |   19358    68241 |   13847    8953   171533    19.2 | 17.731 % |
c |    222823 |   19358    68241 |   15232   11516   225548    19.6 | 17.731 % |
c |    226669 |   19358    68241 |   16755   15362   305528    19.9 | 17.731 % |
c |    232435 |   19358    68241 |   18431   12377   238870    19.3 | 17.731 % |
c |    241084 |   19358    68241 |   20274   11449   212889    18.6 | 17.731 % |
c |    254058 |   19333    68158 |   22301   13890   270658    19.5 | 17.836 % |
c |    273520 |   19324    68127 |   24531   21821   437483    20.0 | 17.862 % |
c |    302713 |   19315    68096 |   26985   13077   262897    20.1 | 17.888 % |
c |    346502 |   19297    68034 |   29683   15176   389434    25.7 | 17.940 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 650   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    351545 |   19301    68055 |    6433   20219   551446    27.3 | 17.940 % |
c |    351646 |   19301    68055 |    7076    5156   133526    25.9 | 17.983 % |
c |    351796 |   19301    68055 |    7783    5306   136545    25.7 | 17.983 % |
c |    352021 |   19301    68055 |    8562    5531   140793    25.5 | 17.983 % |
c |    352359 |   19301    68055 |    9418    5869   147680    25.2 | 17.983 % |
c |    352867 |   19301    68055 |   10360    6377   160305    25.1 | 17.983 % |
c |    353627 |   19301    68055 |   11396    7137   177022    24.8 | 17.983 % |
c |    354766 |   19301    68055 |   12536    8276   198733    24.0 | 17.983 % |
c |    356474 |   19301    68055 |   13789    9984   235925    23.6 | 17.983 % |
c |    359037 |   19301    68055 |   15168   12547   292434    23.3 | 17.983 % |
c |    362881 |   19301    68055 |   16685    8396   147122    17.5 | 17.983 % |
c |    368650 |   19301    68055 |   18354   14165   285427    20.2 | 17.983 % |
c |    377299 |   19301    68055 |   20189   13269   244397    18.4 | 17.983 % |
c |    390273 |   19301    68055 |   22208   15772   225710    14.3 | 17.983 % |
c |    409735 |   19292    68024 |   24429   12263   209625    17.1 | 18.009 % |
c |    438927 |   19271    67953 |   26872   16242   311076    19.2 | 18.087 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 652   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    460016 |   19275    67973 |    6425   23515   432845    18.4 | 18.087 % |
c |    460116 |   19275    67973 |    7067    5979    90580    15.1 | 18.130 % |
c |    460267 |   19275    67973 |    7774    6130    92764    15.1 | 18.130 % |
c |    460492 |   19275    67973 |    8551    6355    96613    15.2 | 18.130 % |
c |    460832 |   19275    67973 |    9406    6695   104747    15.6 | 18.130 % |
c |    461342 |   19275    67973 |   10347    7205   118903    16.5 | 18.130 % |
c |    462102 |   19275    67973 |   11382    7965   136860    17.2 | 18.130 % |
c |    463242 |   19275    67973 |   12520    9105   164522    18.1 | 18.130 % |
c |    464952 |   19275    67973 |   13772   10815   203914    18.9 | 18.130 % |
c |    467517 |   19275    67973 |   15149   13380   267593    20.0 | 18.130 % |
c |    471363 |   19275    67973 |   16664    9263   191920    20.7 | 18.130 % |
c |    477129 |   19275    67973 |   18331   15029   322847    21.5 | 18.130 % |
c |    485778 |   19275    67973 |   20164   14131   265233    18.8 | 18.130 % |
c |    498752 |   19251    67891 |   22180   16590   425523    25.6 | 18.234 % |
c |    518214 |   19251    67891 |   24398   13115   231213    17.6 | 18.234 % |
c |    547410 |   19242    67860 |   26838   17140   317186    18.5 | 18.260 % |
c |    591200 |   19242    67860 |   29522   19513   811700    41.6 | 18.260 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 654   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    630926 |   19229    67824 |    6409   25337   720150    28.4 | 18.260 % |
c |    631027 |   19229    67824 |    7049    6436   264399    41.1 | 18.381 % |
c |    631177 |   19229    67824 |    7754    6586   266648    40.5 | 18.381 % |
c |    631404 |   19229    67824 |    8530    6813   269154    39.5 | 18.381 % |
c |    631741 |   19229    67824 |    9383    7150   275292    38.5 | 18.381 % |
c |    632247 |   19229    67824 |   10321    7656   287046    37.5 | 18.381 % |
c |    633006 |   19229    67824 |   11353    8415   301846    35.9 | 18.381 % |
c |    634145 |   19229    67824 |   12489    9554   328706    34.4 | 18.381 % |
c |    635854 |   19229    67824 |   13738   11263   369783    32.8 | 18.381 % |
c |    638416 |   19229    67824 |   15112   13825   437784    31.7 | 18.381 % |
c |    642260 |   19229    67824 |   16623    9718   191343    19.7 | 18.381 % |
c |    648027 |   19229    67824 |   18285   15485   337330    21.8 | 18.381 % |
c |    656677 |   19229    67824 |   20114   14613   283257    19.4 | 18.381 % |
c |    669654 |   19229    67824 |   22125   17161   328344    19.1 | 18.381 % |
c |    689115 |   19229    67824 |   24338   13728   264705    19.3 | 18.381 % |
c |    718308 |   19229    67824 |   26771   17827   329264    18.5 | 18.381 % |
c |    762097 |   19229    67824 |   29449   20273   388347    19.2 | 18.381 % |
c |    827783 |   19223    67804 |   32394   22953   437004    19.0 | 18.407 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 656   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    915375 |   19230    67834 |    6410   21242  1471898    69.3 | 18.407 % |
c |    915475 |   19230    67834 |    7051    5411   194999    36.0 | 18.444 % |
c |    915626 |   19230    67834 |    7756    5562   196236    35.3 | 18.444 % |
c |    915852 |   19230    67834 |    8531    5788   198330    34.3 | 18.444 % |
c |    916189 |   19230    67834 |    9384    6125   203299    33.2 | 18.444 % |
c |    916695 |   19230    67834 |   10323    6631   213319    32.2 | 18.444 % |
c |    917454 |   19230    67834 |   11355    7390   232530    31.5 | 18.444 % |
c |    918593 |   19230    67834 |   12491    8529   262257    30.7 | 18.444 % |
c |    920303 |   19230    67834 |   13740   10239   316738    30.9 | 18.444 % |
c |    922866 |   19230    67834 |   15114   12802   441129    34.5 | 18.444 % |
c |    926711 |   19230    67834 |   16625    8473   439344    51.9 | 18.444 % |
c |    932477 |   19230    67834 |   18288   14239   886809    62.3 | 18.444 % |
c |    941127 |   19230    67834 |   20117   12905   578313    44.8 | 18.444 % |
c |    954102 |   19230    67834 |   22129   15439   322398    20.9 | 18.444 % |
c |    973565 |   19230    67834 |   24341   11886   216114    18.2 | 18.444 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 658   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    992750 |   19233    67851 |    6411   18517  1337422    72.2 | 18.444 % |
c |    992850 |   19233    67851 |    7052    4730   161591    34.2 | 18.482 % |
c |    993000 |   19233    67851 |    7757    4880   163198    33.4 | 18.482 % |
c |    993225 |   19233    67851 |    8533    5105   166948    32.7 | 18.482 % |
c |    993563 |   19233    67851 |    9386    5443   171743    31.6 | 18.482 % |
c |    994069 |   19233    67851 |   10324    5949   183484    30.8 | 18.482 % |
c |    994831 |   19233    67851 |   11357    6711   200535    29.9 | 18.482 % |
c |    995976 |   19233    67851 |   12493    7856   229180    29.2 | 18.482 % |
c |    997684 |   19233    67851 |   13742    9564   269567    28.2 | 18.482 % |
c |   1000248 |   19233    67851 |   15116   12128   325232    26.8 | 18.482 % |
c |   1004093 |   19233    67851 |   16628    8030   142573    17.8 | 18.482 % |
c |   1009859 |   19233    67851 |   18291   13796   329933    23.9 | 18.482 % |
c |   1018508 |   19233    67851 |   20120   12810   306912    24.0 | 18.482 % |
c |   1031482 |   19233    67851 |   22132   15277   417600    27.3 | 18.482 % |
c |   1050943 |   19233    67851 |   24345   11848   201280    17.0 | 18.482 % |
c |   1080135 |   19233    67851 |   26780   15848   263648    16.6 | 18.482 % |
c |   1123924 |   19233    67851 |   29458   15912  1437080    90.3 | 18.482 % |
c |   1189608 |   19233    67851 |   32404   19454  1489279    76.6 | 18.482 % |
c |   1288135 |   19233    67851 |   35644   25446  3014556   118.5 | 18.482 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v1 -v2 -v3 -v4 -v5 -v6 -v7 -v8 -v9 -v10 -v11 -v12 -v13 -v14 v15 -v16 -v17 -v18 -v19 -v20 -v21 -v22 -v23 -v24 -v25 -v26 -v27 -v28 -v29 -v30 -v31 -v32 -v33 -v34 -v35 v36 -v37 -v38 -v39 v40 -v41 -v42 -v43 v44 -v45 -v46 -v47 v48 v49 -v50 -v51 -v52 v53 -v54 -v55 -v56 -v57 -v58 -v59 -v60 -v61 v62 -v63 -v64 -v65 -v66 -v67 -v68 -v69 -v70 -v71 -v72 v73 v74 -v75 -v76 -v77 -v78 -v79 -v80 -v81 -v82 -v83 -v84 -v85 -v86 -v87 -v88 -v89 -v90 -v91 -v92 -v93 -v94 -v95 -v96 -v97 -v98 -v99 -v100 -v101 -v102 -v103 -v104 -v105 -v106 v107 v108 -v109 -v110 -v111 -v112 -v113 -v114 -v115 -v116 -v117 -v118 -v119 -v120 -v121 -v122 -v123 -v124 -v125 -v126 -v127 v128 -v129 v130 -v131 -v132 -v133 -v134 -v135 -v136 -v137 -v138 -v139 -v140 -v141 v142 -v143 -v144 -v145 -v146 -v147 -v148 v149 v150 v151 -v152 -v153 -v154 -v155 -v156 -v157 -v158 -v159 -v160 -v161 v162 -v163 -v164 -v165 -v166 -v167 -v168 -v169 -v170 -v171 v172 -v173 -v174 -v175 -v176 -v177 -v178 -v179 -v180 -v181 -v182 -v183 -v184 -v185 v186 -v187 -v188 -v189 -v190 -v191 -v192 -v193 -v194 -v195 -v196 -v197 -v198 -v199 -v200 v201 -v202 -v203 -v204 -v205 -v206 -v207 -v208 -v209 -v210 -v211 -v212 -v213 -v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 -v222 -v223 -v224 -v225 -v226 -v227 -v228 -v229 -v230 -v231 -v232 -v233 -v234 -v235 -v236 -v237 v238 -v239 -v240 v241 v242 -v243 -v244 -v245 -v246 -v247 -v248 -v249 -v250 -v251 -v252 -v253 -v254 v255 -v256 -v257 -v258 -v259 -v260 -v261 -v262 -v263 -v264 -v265 -v266 -v267 v268 -v269 -v270 -v271 -v272 -v273 -v274 -v275 -v276 -v277 -v278 -v279 -v280 v281 -v282 -v283 -v284 -v285 -v286 -v287 -v288 -v289 -v290 -v291 -v292 -v293 -v294 -v295 -v296 -v297 -v298 -v299 v300 -v301 -v302 -v303 -v304 -v305 -v306 -v307 -v308 -v309 -v310 -v311 v312 -v313 -v314 -v315 -v316 -v317 -v318 -v319 -v320 -v321 -v322 -v323 -v324 -v325 v326 -v327 -v328 -v329 v330 -v331 -v332 -v333 v334 -v335 -v336 -v337 -v338 -v339 v340 v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 -v349 -v350 -v351 -v352 -v353 -v354 v355 -v356 -v357 -v358 v359 -v360 -v361 -v362 -v363 -v364 -v365 -v366 -v367 -v368 v369 -v370 -v371 -v372 -v373 -v374 -v375 -v376 -v377 -v378 v379 -v380 -v381 -v382 -v383 -v384 -v385 -v386 -v387 -v388 -v389 -v390 -v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 -v399 -v400 -v401 -v402 -v403 -v404 -v405 -v406 -v407 v408 -v409 -v410 -v411 -v412 -v413 -v414 v415 v416 -v417 v418 -v419 -v420 -v421 -v422 -v423 -v424 -v425 -v426 -v427 -v428 v429 -v430 -v431 -v432 -v433 -v434 -v435 -v436 -v437 -v438 -v439 -v440 -v441 -v442 v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451 -v452 -v453 -v454 -v455 -v456 -v457 -v458 -v459 -v460 -v461 -v462 v463 v464 -v465 -v466 -v467 -v468 -v469 -v470 -v471 -v472 -v473 -v474 -v475 -v476 -v477 -v478 -v479 -v480 -v481 -v482 -v483 -v484 -v485 -v486 -v487 -v488 -v489 -v490 v491 -v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 -v511 -v512 -v513 -v514 -v515 -v516 -v517 -v518 -v519 -v520 -v521 -v522 v523 -v524 -v525 -v526 v527 -v528 -v529 -v530 -v531 -v532 -v533 -v534 -v535 -v536 v537 -v538 -v539 -v540 -v541 -v542 -v543 v544 -v545 -v546 -v547 v548 -v549 -v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 -v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 v567 -v568 -v569 -v570 -v571 -v572 -v573 -v574 -v575 -v576 -v577 v578 -v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 -v611 -v612 v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 -v622 -v623 -v624 -v625 -v626 -v627 -v628 -v629 -v630 -v631 -v632 -v633 -v634 -v635 -v636 -v637 -v638 -v639 v640 -v641 -v642 -v643 v644 -v645 -v646 -v647 -v648 -v649 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659 -v660 -v661 v662 -v663 -v664 -v665 -v666 -v667 -v668 -v669 -v670 -v671 -v672 -v673 -v674 v675 -v676 -v677 -v678 -v679 -v680 -v681 -v682 -v683 -v684 -v685 -v686 -v687 -v688 -v689 -v690 -v691 -v692 -v693 -v694 -v695 -v696 -v697 -v698 -v699 -v700 -v701 -v702 -v703 -v704 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (runsolver) R 25852 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479520299 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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+9.9999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 940 0 0 0 995 2 0 0 25 0 1 0 479520299 5427200 918 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1325 918 603 41 0 1284 0
vsize: 5300
[startup+20.0011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 1221 0 0 0 1994 3 0 0 25 0 1 0 479520299 6639616 1199 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1621 1199 603 41 0 1580 0
vsize: 6484
[startup+30.0014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 1310 0 0 0 2993 4 0 0 25 0 1 0 479520299 6922240 1288 4294967295 134512640 134672761 3221224560 3221223728 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1690 1288 603 41 0 1649 0
vsize: 6760
[startup+40.0008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 1420 0 0 0 3992 4 0 0 25 0 1 0 479520299 7483392 1398 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1827 1398 603 41 0 1786 0
vsize: 7308
[startup+50.0016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 1510 0 0 0 4992 4 0 0 25 0 1 0 479520299 7888896 1488 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1926 1488 603 41 0 1885 0
vsize: 7704
[startup+60.0013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 1614 0 0 0 5992 5 0 0 25 0 1 0 479520299 8409088 1592 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2053 1592 603 41 0 2012 0
vsize: 8212
[startup+70.0016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 1657 0 0 0 6992 5 0 0 25 0 1 0 479520299 8556544 1635 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2089 1635 603 41 0 2048 0
vsize: 8356
[startup+80.0015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 1678 0 0 0 7992 5 0 0 25 0 1 0 479520299 8720384 1656 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2129 1656 603 41 0 2088 0
vsize: 8516
[startup+90.0012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 1765 0 0 0 8992 5 0 0 25 0 1 0 479520299 8990720 1743 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2195 1743 603 41 0 2154 0
vsize: 8780
[startup+100.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 1859 0 0 0 9991 6 0 0 25 0 1 0 479520299 9424896 1837 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2301 1837 603 41 0 2260 0
vsize: 9204
[startup+110.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 1948 0 0 0 10991 6 0 0 25 0 1 0 479520299 9830400 1926 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2400 1926 603 41 0 2359 0
vsize: 9600
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2071 0 0 0 11991 6 0 0 25 0 1 0 479520299 10235904 2049 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2499 2049 603 41 0 2458 0
vsize: 9996
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2173 0 0 0 12991 7 0 0 25 0 1 0 479520299 10670080 2151 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2605 2151 603 41 0 2564 0
vsize: 10420
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2225 0 0 0 13991 7 0 0 25 0 1 0 479520299 10948608 2203 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2673 2203 603 41 0 2632 0
vsize: 10692
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2306 0 0 0 14991 7 0 0 25 0 1 0 479520299 11227136 2284 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2284 603 41 0 2700 0
vsize: 10964
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2414 0 0 0 15991 7 0 0 25 0 1 0 479520299 11800576 2392 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2881 2392 603 41 0 2840 0
vsize: 11524
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2543 0 0 0 16990 8 0 0 25 0 1 0 479520299 12357632 2521 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3017 2521 603 41 0 2976 0
vsize: 12068
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2630 0 0 0 17990 8 0 0 25 0 1 0 479520299 12767232 2608 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3117 2608 603 41 0 3076 0
vsize: 12468
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2646 0 0 0 18990 9 0 0 25 0 1 0 479520299 12767232 2624 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3117 2624 603 41 0 3076 0
vsize: 12468
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2656 0 0 0 19990 9 0 0 25 0 1 0 479520299 12767232 2634 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3117 2634 603 41 0 3076 0
vsize: 12468
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2670 0 0 0 20990 9 0 0 25 0 1 0 479520299 12931072 2648 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3157 2648 603 41 0 3116 0
vsize: 12628
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25853
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2670 0 0 0 21991 9 0 0 25 0 1 0 479520299 12931072 2648 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3157 2648 603 41 0 3116 0
vsize: 12628
[startup+230 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2671 0 0 0 22991 9 0 0 25 0 1 0 479520299 12931072 2649 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3157 2649 603 41 0 3116 0
vsize: 12628
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2681 0 0 0 23991 9 0 0 25 0 1 0 479520299 12931072 2659 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3157 2659 603 41 0 3116 0
vsize: 12628
[startup+250 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2681 0 0 0 24991 9 0 0 25 0 1 0 479520299 12931072 2659 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3157 2659 603 41 0 3116 0
vsize: 12628
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2690 0 0 0 25991 9 0 0 25 0 1 0 479520299 12931072 2668 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3157 2668 603 41 0 3116 0
vsize: 12628
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2719 0 0 0 26991 9 0 0 25 0 1 0 479520299 13094912 2697 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3197 2697 603 41 0 3156 0
vsize: 12788
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2722 0 0 0 27992 9 0 0 25 0 1 0 479520299 13094912 2700 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3197 2700 603 41 0 3156 0
vsize: 12788
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2741 0 0 0 28992 9 0 0 25 0 1 0 479520299 13258752 2719 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3237 2719 603 41 0 3196 0
vsize: 12948
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2749 0 0 0 29992 9 0 0 25 0 1 0 479520299 13258752 2727 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3237 2727 603 41 0 3196 0
vsize: 12948
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 2781 0 0 0 30992 9 0 0 25 0 1 0 479520299 13422592 2759 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3277 2759 603 41 0 3236 0
vsize: 13108
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3260 0 0 0 31991 11 0 0 25 0 1 0 479520299 15437824 3238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3769 3238 603 41 0 3728 0
vsize: 15076
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3346 0 0 0 32990 11 0 0 25 0 1 0 479520299 15704064 3324 4294967295 134512640 134672761 3221224560 3221223732 134558808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3834 3324 603 41 0 3793 0
vsize: 15336
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3346 0 0 0 33990 11 0 0 25 0 1 0 479520299 15704064 3324 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3834 3324 603 41 0 3793 0
vsize: 15336
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3346 0 0 0 34991 11 0 0 25 0 1 0 479520299 15704064 3324 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3834 3324 603 41 0 3793 0
vsize: 15336
[startup+360.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3348 0 0 0 35991 11 0 0 25 0 1 0 479520299 15704064 3326 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3834 3326 603 41 0 3793 0
vsize: 15336
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3351 0 0 0 36991 11 0 0 25 0 1 0 479520299 15704064 3329 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3834 3329 603 41 0 3793 0
vsize: 15336
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3351 0 0 0 37991 11 0 0 25 0 1 0 479520299 15704064 3329 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3834 3329 603 41 0 3793 0
vsize: 15336
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3351 0 0 0 38991 11 0 0 25 0 1 0 479520299 15704064 3329 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3834 3329 603 41 0 3793 0
vsize: 15336
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3354 0 0 0 39991 11 0 0 25 0 1 0 479520299 15704064 3332 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3834 3332 603 41 0 3793 0
vsize: 15336
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3358 0 0 0 40992 11 0 0 25 0 1 0 479520299 15704064 3336 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3834 3336 603 41 0 3793 0
vsize: 15336
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3367 0 0 0 41992 11 0 0 25 0 1 0 479520299 15859712 3345 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3872 3345 603 41 0 3831 0
vsize: 15488
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3367 0 0 0 42992 11 0 0 25 0 1 0 479520299 15859712 3345 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3872 3345 603 41 0 3831 0
vsize: 15488
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3379 0 0 0 43992 11 0 0 25 0 1 0 479520299 15859712 3357 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3872 3357 603 41 0 3831 0
vsize: 15488
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3402 0 0 0 44992 11 0 0 25 0 1 0 479520299 16056320 3380 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3920 3380 603 41 0 3879 0
vsize: 15680
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3403 0 0 0 45993 11 0 0 25 0 1 0 479520299 16056320 3381 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3920 3381 603 41 0 3879 0
vsize: 15680
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3404 0 0 0 46993 11 0 0 25 0 1 0 479520299 16056320 3382 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3920 3382 603 41 0 3879 0
vsize: 15680
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3424 0 0 0 47993 11 0 0 25 0 1 0 479520299 16056320 3402 4294967295 134512640 134672761 3221224560 3221223684 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3920 3402 603 41 0 3879 0
vsize: 15680
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3424 0 0 0 48993 11 0 0 25 0 1 0 479520299 16056320 3402 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3920 3402 603 41 0 3879 0
vsize: 15680
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 3793 0 0 0 49992 12 0 0 25 0 1 0 479520299 17801216 3771 4294967295 134512640 134672761 3221224560 3221223664 134559805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4346 3771 603 41 0 4305 0
vsize: 17384
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 4599 0 0 0 50990 15 0 0 25 0 1 0 479520299 21024768 4577 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5133 4577 603 41 0 5092 0
vsize: 20532
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25855
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 4905 0 0 0 51990 15 0 0 25 0 1 0 479520299 22368256 4883 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5461 4883 603 41 0 5420 0
vsize: 21844
[startup+530.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 4905 0 0 0 52990 15 0 0 25 0 1 0 479520299 22368256 4883 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5461 4883 603 41 0 5420 0
vsize: 21844
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5071 0 0 0 53990 16 0 0 25 0 1 0 479520299 23035904 5049 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5624 5049 603 41 0 5583 0
vsize: 22496
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5329 0 0 0 54989 16 0 0 25 0 1 0 479520299 24096768 5307 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5883 5307 603 41 0 5842 0
vsize: 23532
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5331 0 0 0 55989 16 0 0 25 0 1 0 479520299 24096768 5309 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5883 5309 603 41 0 5842 0
vsize: 23532
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5331 0 0 0 56990 16 0 0 25 0 1 0 479520299 24096768 5309 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5883 5309 603 41 0 5842 0
vsize: 23532
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5449 0 0 0 57990 16 0 0 25 0 1 0 479520299 24621056 5427 4294967295 134512640 134672761 3221224560 3221223696 134565130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5427 603 41 0 5970 0
vsize: 24044
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5449 0 0 0 58990 16 0 0 25 0 1 0 479520299 24621056 5427 4294967295 134512640 134672761 3221224560 3221223744 134559415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5427 603 41 0 5970 0
vsize: 24044
[startup+600.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5449 0 0 0 59990 16 0 0 25 0 1 0 479520299 24621056 5427 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5427 603 41 0 5970 0
vsize: 24044
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5449 0 0 0 60990 16 0 0 25 0 1 0 479520299 24621056 5427 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5427 603 41 0 5970 0
vsize: 24044
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 61990 16 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 62990 17 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223696 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+640.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 63990 17 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 64991 17 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 65991 17 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 66991 17 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 67991 17 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 68991 17 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+700.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 69991 17 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+710.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 70991 17 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+720.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5450 0 0 0 71992 17 0 0 25 0 1 0 479520299 24621056 5428 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5428 603 41 0 5970 0
vsize: 24044
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5451 0 0 0 72992 17 0 0 25 0 1 0 479520299 24621056 5429 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5429 603 41 0 5970 0
vsize: 24044
[startup+740.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5451 0 0 0 73992 17 0 0 25 0 1 0 479520299 24621056 5429 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5429 603 41 0 5970 0
vsize: 24044
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5451 0 0 0 74992 17 0 0 25 0 1 0 479520299 24621056 5429 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5429 603 41 0 5970 0
vsize: 24044
[startup+760.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 5451 0 0 0 75992 17 0 0 25 0 1 0 479520299 24621056 5429 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6011 5429 603 41 0 5970 0
vsize: 24044
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6151 0 0 0 76991 18 0 0 25 0 1 0 479520299 27467776 6129 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6706 6129 603 41 0 6665 0
vsize: 26824
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 77990 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 78990 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 79990 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+810.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 80991 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223684 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+820.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25857
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 81991 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+830.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 82991 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+840.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 83991 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+850.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 84991 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 85992 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 86992 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+880.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 87992 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+890.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 88992 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+900.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 89992 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 90992 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+920.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 91993 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223664 134560201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+930.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 92993 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+940.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6415 0 0 0 93993 19 0 0 25 0 1 0 479520299 28540928 6393 4294967295 134512640 134672761 3221224560 3221223664 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6968 6393 603 41 0 6927 0
vsize: 27872
[startup+950.009 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6912 0 0 0 94992 21 0 0 25 0 1 0 479520299 30674944 6890 4294967295 134512640 134672761 3221224560 3221223712 134559753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7489 6890 603 41 0 7448 0
vsize: 29956
[startup+960.009 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6986 0 0 0 95992 21 0 0 25 0 1 0 479520299 30945280 6964 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6964 603 41 0 7514 0
vsize: 30220
[startup+970.009 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6986 0 0 0 96992 21 0 0 25 0 1 0 479520299 30945280 6964 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6964 603 41 0 7514 0
vsize: 30220
[startup+980.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 6986 0 0 0 97992 21 0 0 25 0 1 0 479520299 30945280 6964 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6964 603 41 0 7514 0
vsize: 30220
[startup+990.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7004 0 0 0 98992 21 0 0 25 0 1 0 479520299 30945280 6982 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6982 603 41 0 7514 0
vsize: 30220
[startup+1000.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7004 0 0 0 99992 21 0 0 25 0 1 0 479520299 30945280 6982 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6982 603 41 0 7514 0
vsize: 30220
[startup+1010.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7005 0 0 0 100993 21 0 0 25 0 1 0 479520299 30945280 6983 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6983 603 41 0 7514 0
vsize: 30220
[startup+1020.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7006 0 0 0 101993 21 0 0 25 0 1 0 479520299 30945280 6984 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6984 603 41 0 7514 0
vsize: 30220
[startup+1030.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7008 0 0 0 102993 21 0 0 25 0 1 0 479520299 30945280 6986 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6986 603 41 0 7514 0
vsize: 30220
[startup+1040.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7009 0 0 0 103993 21 0 0 25 0 1 0 479520299 30945280 6987 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6987 603 41 0 7514 0
vsize: 30220
[startup+1050.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7009 0 0 0 104993 21 0 0 25 0 1 0 479520299 30945280 6987 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6987 603 41 0 7514 0
vsize: 30220
[startup+1060.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7010 0 0 0 105993 21 0 0 25 0 1 0 479520299 30945280 6988 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6988 603 41 0 7514 0
vsize: 30220
[startup+1070.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7010 0 0 0 106994 21 0 0 25 0 1 0 479520299 30945280 6988 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6988 603 41 0 7514 0
vsize: 30220
[startup+1080.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7011 0 0 0 107994 21 0 0 25 0 1 0 479520299 30945280 6989 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6989 603 41 0 7514 0
vsize: 30220
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7011 0 0 0 108994 21 0 0 25 0 1 0 479520299 30945280 6989 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6989 603 41 0 7514 0
vsize: 30220
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7011 0 0 0 109995 21 0 0 25 0 1 0 479520299 30945280 6989 4294967295 134512640 134672761 3221224560 3221223664 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6989 603 41 0 7514 0
vsize: 30220
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7011 0 0 0 110996 21 0 0 25 0 1 0 479520299 30945280 6989 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6989 603 41 0 7514 0
vsize: 30220
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25859
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7011 0 0 0 111996 21 0 0 25 0 1 0 479520299 30945280 6989 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6989 603 41 0 7514 0
vsize: 30220
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25861
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7011 0 0 0 112996 21 0 0 25 0 1 0 479520299 30945280 6989 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6989 603 41 0 7514 0
vsize: 30220
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25861
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7012 0 0 0 113996 21 0 0 25 0 1 0 479520299 30945280 6990 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6990 603 41 0 7514 0
vsize: 30220
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25861
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7012 0 0 0 114996 21 0 0 25 0 1 0 479520299 30945280 6990 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6990 603 41 0 7514 0
vsize: 30220
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25861
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7012 0 0 0 115996 21 0 0 25 0 1 0 479520299 30945280 6990 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6990 603 41 0 7514 0
vsize: 30220
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25861
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7012 0 0 0 116997 21 0 0 25 0 1 0 479520299 30945280 6990 4294967295 134512640 134672761 3221224560 3221223664 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6990 603 41 0 7514 0
vsize: 30220
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25861
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7012 0 0 0 117997 21 0 0 25 0 1 0 479520299 30945280 6990 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7555 6990 603 41 0 7514 0
vsize: 30220
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25861
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7030 0 0 0 118997 21 0 0 25 0 1 0 479520299 31125504 7008 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7599 7008 603 41 0 7558 0
vsize: 30396
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25861
Raw data (stat): 25853 (minisat+) R 25852 20838 20837 0 -1 0 7090 0 0 0 119997 22 0 0 25 0 1 0 479520299 31420416 7068 4294967295 134512640 134672761 3221224560 3221223720 134560076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7671 7068 603 41 0 7630 0
vsize: 30684
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 25861
Raw data (stat): 25853 (minisat+) Z 25852 20838 20837 0 -1 12 7093 0 0 0 119997 23 0 0 25 0 1 0 479520299 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.21
CPU user time (s): 1199.98
CPU system time (s): 0.235964
CPU usage (%): 100.014
Max. virtual memory (Kb): 30684
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####