PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-markshare1.opb
MD5SUM	6f06e375914e0285ec75de90ad627758
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3712
Optimality of the best value was proved	NO
Number of terms in the objective function	120
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	6291450
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	6291450
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.1
Number of variables	170
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	70
Trace number 15407

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-21 04:17:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17641 boxname=wulflinc18 idbench=1357 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6f06e375914e0285ec75de90ad627758  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-markshare1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-markshare1.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-markshare1.opb
IDLAUNCH: 17641
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        381832 kB
Buffers:         34876 kB
Cached:         586460 kB
SwapCached:        388 kB
Active:         317588 kB
Inactive:       306200 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        381580 kB
SwapTotal:     2097892 kB
SwapFree:      2096996 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6224 kB
Slab:            23252 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 04:37:28 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 17641 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> Adder-cost: 304   maxlim: 405119   bits: 20/19
c ---[   8]---> Adder-cost: 314   maxlim: 431743   bits: 20/19
c ---[   6]---> Adder-cost: 348   maxlim: 435327   bits: 20/19
c ---[   4]---> Adder-cost: 318   maxlim: 411775   bits: 20/19
c ---[   2]---> Adder-cost: 312   maxlim: 410751   bits: 20/19
c ---[   0]---> Adder-cost: 314   maxlim: 411135   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12820    45524 |    4273       0        0     nan |  0.000 % |
c |       100 |   12820    45524 |    4700     100      599     6.0 | 11.212 % |
c ==============================================================================
c [1mFound solution: 621184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  854     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 |       115 |   15123    50959 |    5041     115      809     7.0 | 11.212 % |
c |       216 |   15115    50933 |    5545     215     6283    29.2 |  8.456 % |
c ==============================================================================
c [1mFound solution: 594432[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 |       265 |   15217    51193 |    5072     264    12306    46.6 |  8.456 % |
c |       368 |   15209    51167 |    5579     366    14797    40.4 |  8.455 % |
c |       518 |   15209    51167 |    6137     516    22636    43.9 |  8.455 % |
c |       743 |   15201    51141 |    6750     740    45661    61.7 |  8.488 % |
c ==============================================================================
c [1mFound solution: 434176[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 |       818 |   15232    51216 |    5077     815    49004    60.1 |  8.488 % |
c |       919 |   15232    51216 |    5584     916    64144    70.0 |  8.493 % |
c |      1070 |   15232    51216 |    6143    1067    77822    72.9 |  8.493 % |
c |      1295 |   15224    51190 |    6757    1291    92578    71.7 |  8.527 % |
c |      1632 |   15216    51164 |    7433    1627   124637    76.6 |  8.561 % |
c |      2138 |   15216    51164 |    8176    2133   165578    77.6 |  8.561 % |
c |      2898 |   15200    51112 |    8994    2891   235730    81.5 |  8.628 % |
c |      4038 |   15200    51112 |    9893    4031   329789    81.8 |  8.628 % |
c |      5746 |   15200    51112 |   10883    5739   471861    82.2 |  8.628 % |
c ==============================================================================
c [1mFound solution: 407040[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 |      6078 |   15215    51151 |    5071    6071   502716    82.8 |  8.628 % |
c |      6179 |   15215    51151 |    5578    3137   220945    70.4 |  8.650 % |
c |      6329 |   15215    51151 |    6135    3287   231329    70.4 |  8.650 % |
c |      6554 |   15215    51151 |    6749    3512   243726    69.4 |  8.650 % |
c |      6891 |   15215    51151 |    7424    3849   280837    73.0 |  8.650 % |
c |      7398 |   15215    51151 |    8166    4356   326304    74.9 |  8.650 % |
c ==============================================================================
c [1mFound solution: 364160[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 |      8022 |   15240    51213 |    5080    4980   367622    73.8 |  8.650 % |
c |      8122 |   15240    51213 |    5588    5080   379899    74.8 |  8.661 % |
c |      8273 |   15240    51213 |    6146    5231   389905    74.5 |  8.661 % |
c |      8498 |   15232    51187 |    6761    5455   409892    75.1 |  8.694 % |
c |      8836 |   15232    51187 |    7437    5793   435941    75.3 |  8.694 % |
c |      9343 |   15232    51187 |    8181    6300   467577    74.2 |  8.694 % |
c |     10104 |   15232    51187 |    8999    7061   522662    74.0 |  8.694 % |
c |     11243 |   15216    51135 |    9899    8198   598918    73.1 |  8.761 % |
c ==============================================================================
c [1mFound solution: 330112[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 |     12674 |   15235    51182 |    5078    9629   671552    69.7 |  8.761 % |
c |     12774 |   15235    51182 |    5585    4915   258192    52.5 |  8.777 % |
c |     12926 |   15235    51182 |    6144    5067   267779    52.8 |  8.777 % |
c |     13151 |   15235    51182 |    6758    5292   275192    52.0 |  8.777 % |
c |     13489 |   15235    51182 |    7434    5630   296070    52.6 |  8.777 % |
c |     13995 |   15235    51182 |    8178    6136   329734    53.7 |  8.777 % |
c |     14755 |   15235    51182 |    8995    6896   409961    59.4 |  8.777 % |
c |     15894 |   15235    51182 |    9895    8035   529935    66.0 |  8.777 % |
c |     17604 |   15235    51182 |   10885    9745   665119    68.3 |  8.777 % |
c ==============================================================================
c [1mFound solution: 296448[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 |     19485 |   15251    51222 |    5083    5860   429862    73.4 |  8.777 % |
c |     19587 |   15251    51222 |    5591    3032   186614    61.5 |  8.796 % |
c |     19737 |   15251    51222 |    6150    3182   196098    61.6 |  8.796 % |
c |     19964 |   15251    51222 |    6765    3409   215754    63.3 |  8.796 % |
c |     20301 |   15243    51196 |    7442    3745   235542    62.9 |  8.829 % |
c |     20808 |   15243    51196 |    8186    4252   261088    61.4 |  8.829 % |
c |     21568 |   15243    51196 |    9004    5012   320576    64.0 |  8.829 % |
c |     22708 |   15243    51196 |    9905    6152   399280    64.9 |  8.829 % |
c ==============================================================================
c [1mFound solution: 152320[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 |     23074 |   15273    51268 |    5091    6518   414330    63.6 |  8.829 % |
c |     23179 |   15273    51268 |    5600    3364   152029    45.2 |  8.833 % |
c |     23329 |   15273    51268 |    6160    3514   161262    45.9 |  8.833 % |
c |     23555 |   15273    51268 |    6776    3740   173908    46.5 |  8.833 % |
c |     23892 |   15265    51246 |    7453    4076   185260    45.5 |  8.900 % |
c |     24398 |   15265    51246 |    8199    4582   222534    48.6 |  8.900 % |
c |     25158 |   15265    51246 |    9019    5342   277349    51.9 |  8.900 % |
c |     26297 |   15265    51246 |    9920    6481   352077    54.3 |  8.900 % |
c |     28006 |   15265    51246 |   10913    8190   434594    53.1 |  8.900 % |
c |     30568 |   15265    51246 |   12004   10752   538975    50.1 |  8.900 % |
c |     34415 |   15248    51204 |   13204    8191   339466    41.4 |  9.033 % |
c |     40182 |   15248    51204 |   14525   13958   651976    46.7 |  9.033 % |
c |     48831 |   15240    51178 |   15977   14856   701447    47.2 |  9.067 % |
c |     61806 |   15240    51178 |   17575   11073   441884    39.9 |  9.067 % |
c ==============================================================================
c [1mFound solution: 119168[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72763 |   15074    50740 |    5024   12867   612133    47.6 |  9.067 % |
c |     72863 |   15074    50740 |    5526    3317    95779    28.9 | 10.679 % |
c |     73013 |   15074    50740 |    6079    3467    99247    28.6 | 10.679 % |
c |     73239 |   15074    50740 |    6686    3693   102775    27.8 | 10.679 % |
c |     73577 |   15002    50568 |    7355    4029   118338    29.4 | 11.311 % |
c |     74084 |   15002    50568 |    8091    4536   133378    29.4 | 11.311 % |
c |     74844 |   14928    50396 |    8900    5293   157844    29.8 | 12.076 % |
c |     75984 |   14928    50396 |    9790    6433   226610    35.2 | 12.076 % |
c |     77693 |   14928    50396 |   10769    8142   317799    39.0 | 12.076 % |
c |     80257 |   14928    50396 |   11846   10706   422563    39.5 | 12.076 % |
c |     84102 |   14928    50396 |   13030    8248   319365    38.7 | 12.076 % |
c |     89869 |   14928    50396 |   14334    7148   257900    36.1 | 12.076 % |
c |     98518 |   14928    50396 |   15767    8285   337507    40.7 | 12.076 % |
c |    111492 |   14913    50361 |   17344   12959   534297    41.2 | 12.242 % |
c |    130954 |   14903    50338 |   19078   14271   714478    50.1 | 12.342 % |
c ==============================================================================
c [1mFound solution: 111744[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    152324 |   14898    50329 |    4966   15865   714391    45.0 | 12.342 % |
c |    152425 |   14898    50329 |    5462    4068   130389    32.1 | 12.579 % |
c |    152576 |   14898    50329 |    6008    4219   132858    31.5 | 12.579 % |
c |    152802 |   14898    50329 |    6609    4445   136968    30.8 | 12.579 % |
c |    153140 |   14898    50329 |    7270    4783   146433    30.6 | 12.579 % |
c |    153646 |   14898    50329 |    7997    5289   162034    30.6 | 12.579 % |
c |    154406 |   14898    50329 |    8797    6049   189686    31.4 | 12.579 % |
c |    155545 |   14898    50329 |    9677    7188   251116    34.9 | 12.579 % |
c |    157253 |   14898    50329 |   10645    8896   346609    39.0 | 12.579 % |
c |    159815 |   14898    50329 |   11709    5738   220544    38.4 | 12.579 % |
c |    163659 |   14898    50329 |   12880    9582   374267    39.1 | 12.579 % |
c |    169425 |   14898    50329 |   14168    8569   268566    31.3 | 12.579 % |
c |    178074 |   14898    50329 |   15585    9737   480369    49.3 | 12.579 % |
c |    191048 |   14878    50283 |   17143   14613   598853    41.0 | 12.811 % |
c |    210510 |   14844    50203 |   18858   16246   764503    47.1 | 13.276 % |
c |    239702 |   14833    50179 |   20744   16046   694873    43.3 | 13.375 % |
c ==============================================================================
c [1mFound solution: 103552[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    271093 |   14834    50183 |    4944   15268   789378    51.7 | 13.375 % |
c |    271194 |   14834    50183 |    5438    3918   128594    32.8 | 13.486 % |
c |    271345 |   14834    50183 |    5982    4069   132521    32.6 | 13.486 % |
c |    271570 |   14834    50183 |    6580    4294   141010    32.8 | 13.486 % |
c |    271908 |   14834    50183 |    7238    4632   150744    32.5 | 13.486 % |
c |    272414 |   14834    50183 |    7962    5138   170656    33.2 | 13.486 % |
c |    273173 |   14834    50183 |    8758    5897   191009    32.4 | 13.486 % |
c |    274313 |   14834    50183 |    9634    7037   232241    33.0 | 13.486 % |
c ==============================================================================
c [1mFound solution: 100736[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 |    274357 |   14845    50210 |    4948    7081   232942    32.9 | 13.486 % |
c |    274457 |   14845    50210 |    5442    3641    85848    23.6 | 13.501 % |
c |    274607 |   14845    50210 |    5987    3791    89517    23.6 | 13.501 % |
c |    274832 |   14845    50210 |    6585    4016    93786    23.4 | 13.501 % |
c |    275169 |   14845    50210 |    7244    4353   101362    23.3 | 13.501 % |
c |    275677 |   14845    50210 |    7968    4861   119994    24.7 | 13.501 % |
c |    276437 |   14845    50210 |    8765    5621   148641    26.4 | 13.501 % |
c |    277576 |   14845    50210 |    9642    6760   191898    28.4 | 13.501 % |
c |    279284 |   14845    50210 |   10606    8468   249840    29.5 | 13.501 % |
c |    281847 |   14835    50186 |   11667   11030   358753    32.5 | 13.600 % |
c |    285692 |   14835    50186 |   12833    8613   362190    42.1 | 13.600 % |
c |    291459 |   14835    50186 |   14117    7587   289521    38.2 | 13.600 % |
c ==============================================================================
c [1mFound solution: 89728[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    293988 |   14846    50213 |    4948   10116   390394    38.6 | 13.600 % |
c |    294089 |   14846    50213 |    5442    5159   164438    31.9 | 13.615 % |
c |    294239 |   14846    50213 |    5987    5309   167333    31.5 | 13.615 % |
c |    294464 |   14846    50213 |    6585    5534   172162    31.1 | 13.615 % |
c |    294802 |   14846    50213 |    7244    5872   176101    30.0 | 13.615 % |
c |    295309 |   14846    50213 |    7968    6379   187425    29.4 | 13.615 % |
c |    296068 |   14846    50213 |    8765    7138   204419    28.6 | 13.615 % |
c |    297207 |   14846    50213 |    9642    8277   239484    28.9 | 13.615 % |
c |    298915 |   14846    50213 |   10606    9985   299663    30.0 | 13.615 % |
c |    301477 |   14846    50213 |   11667    6800   209465    30.8 | 13.615 % |
c |    305322 |   14846    50213 |   12833   10645   346430    32.5 | 13.615 % |
c |    311088 |   14846    50213 |   14117    9572   368611    38.5 | 13.615 % |
c |    319737 |   14846    50213 |   15528   10843   449466    41.5 | 13.615 % |
c ==============================================================================
c [1mFound solution: 80256[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    322873 |   14855    50236 |    4951   13979   600064    42.9 | 13.615 % |
c |    322973 |   14835    50191 |    5446    3593   115506    32.1 | 13.833 % |
c |    323124 |   14835    50191 |    5990    3744   117492    31.4 | 13.833 % |
c |    323349 |   14835    50191 |    6589    3969   125254    31.6 | 13.833 % |
c |    323686 |   14835    50191 |    7248    4306   136016    31.6 | 13.833 % |
c |    324194 |   14835    50191 |    7973    4814   157049    32.6 | 13.833 % |
c |    324953 |   14827    50165 |    8770    5572   173243    31.1 | 13.866 % |
c |    326092 |   14827    50165 |    9648    6711   216993    32.3 | 13.866 % |
c |    327800 |   14827    50165 |   10612    8419   284843    33.8 | 13.866 % |
c |    330362 |   14827    50165 |   11674   10981   382052    34.8 | 13.866 % |
c |    334206 |   14827    50165 |   12841    8508   317228    37.3 | 13.866 % |
c |    339974 |   14827    50165 |   14125    7421   297557    40.1 | 13.866 % |
c |    348624 |   14805    50116 |   15538    8654   325463    37.6 | 14.064 % |
c |    361598 |   14799    50102 |   17092   13376   498028    37.2 | 14.130 % |
c |    381061 |   14794    50091 |   18801   14737   613715    41.6 | 14.196 % |
c |    410254 |   14788    50077 |   20681   14622   546277    37.4 | 14.262 % |
c ==============================================================================
c [1mFound solution: 69120[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    448552 |   14800    50107 |    4933   20848   921959    44.2 | 14.262 % |
c |    448654 |   14800    50107 |    5426    5314   192008    36.1 | 14.276 % |
c |    448804 |   14800    50107 |    5968    5464   198470    36.3 | 14.276 % |
c |    449030 |   14800    50107 |    6565    5690   204641    36.0 | 14.276 % |
c |    449367 |   14800    50107 |    7222    6027   210942    35.0 | 14.276 % |
c |    449875 |   14800    50107 |    7944    6535   229402    35.1 | 14.276 % |
c |    450637 |   14800    50107 |    8739    7297   246014    33.7 | 14.276 % |
c |    451776 |   14800    50107 |    9613    8436   273334    32.4 | 14.276 % |
c |    453484 |   14800    50107 |   10574   10144   325289    32.1 | 14.276 % |
c |    456047 |   14800    50107 |   11631    7110   185707    26.1 | 14.276 % |
c |    459892 |   14800    50107 |   12794   10955   322234    29.4 | 14.276 % |
c |    465659 |   14800    50107 |   14074    9990   334936    33.5 | 14.276 % |
c |    474308 |   14776    50052 |   15481   11251   381453    33.9 | 14.474 % |
c |    487282 |   14776    50052 |   17030   16095   695932    43.2 | 14.474 % |
c |    506743 |   14776    50052 |   18733   17741   685125    38.6 | 14.474 % |
c |    535935 |   14772    50043 |   20606   17662   769860    43.6 | 14.540 % |
c |    579726 |   14758    50010 |   22667   18855   721884    38.3 | 14.672 % |
c |    645411 |   14758    50010 |   24933   14376   590893    41.1 | 14.672 % |
c |    743938 |   14754    49999 |   27427   23200  1041232    44.9 | 14.738 % |
c |    891728 |   14738    49963 |   30169   14367   580925    40.4 | 14.903 % |
c ==============================================================================
c [1mFound solution: 65024[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    937679 |   14686    49792 |    4895   27281  1216508    44.6 | 14.903 % |
c |    937780 |   14686    49792 |    5384    3512   101768    29.0 | 15.349 % |
c |    937930 |   14686    49792 |    5922    3662   107681    29.4 | 15.349 % |
c |    938155 |   14686    49792 |    6515    3887   113416    29.2 | 15.349 % |
c |    938493 |   14686    49792 |    7166    4225   119019    28.2 | 15.349 % |
c |    939000 |   14686    49792 |    7883    4732   131245    27.7 | 15.349 % |
c |    939759 |   14674    49764 |    8671    5485   164145    29.9 | 15.481 % |
c |    940898 |   14674    49764 |    9538    6624   203787    30.8 | 15.481 % |
c |    942606 |   14674    49764 |   10492    8332   279933    33.6 | 15.481 % |
c |    945169 |   14674    49764 |   11542   10895   380159    34.9 | 15.481 % |
c |    949015 |   14674    49764 |   12696    8579   284432    33.2 | 15.481 % |
c |    954782 |   14674    49764 |   13966    7628   238535    31.3 | 15.481 % |
c ==============================================================================
c [1mFound solution: 57088[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    955134 |   14687    49797 |    4895    7980   248620    31.2 | 15.481 % |
c |    955235 |   14687    49797 |    5384    4091   112116    27.4 | 15.493 % |
c |    955385 |   14687    49797 |    5922    4241   114167    26.9 | 15.493 % |
c |    955610 |   14687    49797 |    6515    4466   118571    26.5 | 15.493 % |
c |    955949 |   14687    49797 |    7166    4805   128136    26.7 | 15.493 % |
c |    956455 |   14687    49797 |    7883    5311   140244    26.4 | 15.493 % |
c |    957215 |   14687    49797 |    8671    6071   160201    26.4 | 15.493 % |
c ==============================================================================
c [1mFound solution: 56960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     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 |    957980 |   14691    49807 |    4897    6836   205567    30.1 | 15.493 % |
c |    958080 |   14691    49807 |    5386    3518    94034    26.7 | 15.516 % |
#### 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.85 0.97 0.91 2/55 19010
Raw data (stat): 19010 (runsolver) R 19009 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542125934 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.87 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1239 0 0 0 996 2 0 0 25 0 1 0 542125934 6578176 1217 4294967295 134512640 134672761 3221224544 3221223776 134564929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1606 1217 603 41 0 1565 0
vsize: 6424
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1388 0 0 0 1994 3 0 0 25 0 1 0 542125934 7282688 1366 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1778 1366 603 41 0 1737 0
vsize: 7112
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1471 0 0 0 2993 4 0 0 25 0 1 0 542125934 7548928 1449 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1843 1449 603 41 0 1802 0
vsize: 7372
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1679 0 0 0 3993 4 0 0 25 0 1 0 542125934 8351744 1657 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2039 1657 603 41 0 1998 0
vsize: 8156
[startup+50.0027 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1679 0 0 0 4993 4 0 0 25 0 1 0 542125934 8351744 1657 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2039 1657 603 41 0 1998 0
vsize: 8156
[startup+60.0023 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1681 0 0 0 5993 4 0 0 25 0 1 0 542125934 8351744 1659 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2039 1659 603 41 0 1998 0
vsize: 8156
[startup+70.0035 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1683 0 0 0 6993 4 0 0 25 0 1 0 542125934 8351744 1661 4294967295 134512640 134672761 3221224544 3221223728 134558632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2039 1661 603 41 0 1998 0
vsize: 8156
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1741 0 0 0 7993 5 0 0 25 0 1 0 542125934 8736768 1719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2133 1719 603 41 0 2092 0
vsize: 8532
[startup+90.004 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1741 0 0 0 8993 5 0 0 25 0 1 0 542125934 8736768 1719 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2133 1719 603 41 0 2092 0
vsize: 8532
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1893 0 0 0 9993 5 0 0 25 0 1 0 542125934 9269248 1871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1871 603 41 0 2222 0
vsize: 9052
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1893 0 0 0 10993 5 0 0 25 0 1 0 542125934 9269248 1871 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1871 603 41 0 2222 0
vsize: 9052
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1893 0 0 0 11993 5 0 0 25 0 1 0 542125934 9269248 1871 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1871 603 41 0 2222 0
vsize: 9052
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1893 0 0 0 12993 5 0 0 25 0 1 0 542125934 9269248 1871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1871 603 41 0 2222 0
vsize: 9052
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1893 0 0 0 13993 5 0 0 25 0 1 0 542125934 9269248 1871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2263 1871 603 41 0 2222 0
vsize: 9052
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 1914 0 0 0 14994 5 0 0 25 0 1 0 542125934 9400320 1892 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2295 1892 603 41 0 2254 0
vsize: 9180
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2022 0 0 0 15993 6 0 0 25 0 1 0 542125934 9805824 2000 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 2000 603 41 0 2353 0
vsize: 9576
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2050 0 0 0 16994 6 0 0 25 0 1 0 542125934 9936896 2028 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2426 2028 603 41 0 2385 0
vsize: 9704
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2175 0 0 0 17994 6 0 0 25 0 1 0 542125934 10477568 2153 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2558 2153 603 41 0 2517 0
vsize: 10232
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19010
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2178 0 0 0 18994 6 0 0 25 0 1 0 542125934 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2558 2156 603 41 0 2517 0
vsize: 10232
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2178 0 0 0 19994 6 0 0 25 0 1 0 542125934 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2558 2156 603 41 0 2517 0
vsize: 10232
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2178 0 0 0 20994 6 0 0 25 0 1 0 542125934 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2558 2156 603 41 0 2517 0
vsize: 10232
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2178 0 0 0 21994 6 0 0 25 0 1 0 542125934 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2558 2156 603 41 0 2517 0
vsize: 10232
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2178 0 0 0 22994 6 0 0 25 0 1 0 542125934 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2558 2156 603 41 0 2517 0
vsize: 10232
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2178 0 0 0 23994 6 0 0 25 0 1 0 542125934 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2558 2156 603 41 0 2517 0
vsize: 10232
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2178 0 0 0 24995 6 0 0 25 0 1 0 542125934 10477568 2156 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2558 2156 603 41 0 2517 0
vsize: 10232
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2178 0 0 0 25995 6 0 0 25 0 1 0 542125934 10477568 2156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2558 2156 603 41 0 2517 0
vsize: 10232
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2199 0 0 0 26995 6 0 0 25 0 1 0 542125934 10612736 2177 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2591 2177 603 41 0 2550 0
vsize: 10364
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2200 0 0 0 27995 6 0 0 25 0 1 0 542125934 10612736 2178 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2591 2178 603 41 0 2550 0
vsize: 10364
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2204 0 0 0 28995 6 0 0 25 0 1 0 542125934 10612736 2182 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2591 2182 603 41 0 2550 0
vsize: 10364
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2265 0 0 0 29995 6 0 0 25 0 1 0 542125934 10883072 2243 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2657 2243 603 41 0 2616 0
vsize: 10628
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2282 0 0 0 30995 6 0 0 25 0 1 0 542125934 10883072 2260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2657 2260 603 41 0 2616 0
vsize: 10628
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2320 0 0 0 31995 7 0 0 25 0 1 0 542125934 11014144 2298 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2689 2298 603 41 0 2648 0
vsize: 10756
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2373 0 0 0 32995 7 0 0 25 0 1 0 542125934 11276288 2351 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2753 2351 603 41 0 2712 0
vsize: 11012
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2558 0 0 0 33995 7 0 0 25 0 1 0 542125934 12083200 2536 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2950 2536 603 41 0 2909 0
vsize: 11800
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 34995 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 35995 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 36995 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 37995 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 38995 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 39995 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 40995 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 41995 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 42995 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 43996 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 44996 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 45996 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 46996 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 47996 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19012
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 48996 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2603 0 0 0 49997 8 0 0 25 0 1 0 542125934 12214272 2581 4294967295 134512640 134672761 3221224544 3221223728 134559663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2581 603 41 0 2941 0
vsize: 11928
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2672 0 0 0 50996 8 0 0 25 0 1 0 542125934 12480512 2650 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3047 2650 603 41 0 3006 0
vsize: 12188
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2687 0 0 0 51996 8 0 0 25 0 1 0 542125934 12615680 2665 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3080 2665 603 41 0 3039 0
vsize: 12320
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2687 0 0 0 52997 8 0 0 25 0 1 0 542125934 12615680 2665 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3080 2665 603 41 0 3039 0
vsize: 12320
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2687 0 0 0 53997 8 0 0 25 0 1 0 542125934 12615680 2665 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3080 2665 603 41 0 3039 0
vsize: 12320
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2687 0 0 0 54997 8 0 0 25 0 1 0 542125934 12615680 2665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3080 2665 603 41 0 3039 0
vsize: 12320
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2687 0 0 0 55997 8 0 0 25 0 1 0 542125934 12615680 2665 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3080 2665 603 41 0 3039 0
vsize: 12320
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2687 0 0 0 56997 8 0 0 25 0 1 0 542125934 12615680 2665 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3080 2665 603 41 0 3039 0
vsize: 12320
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2687 0 0 0 57997 8 0 0 25 0 1 0 542125934 12615680 2665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3080 2665 603 41 0 3039 0
vsize: 12320
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2688 0 0 0 58997 8 0 0 25 0 1 0 542125934 12615680 2666 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3080 2666 603 41 0 3039 0
vsize: 12320
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2688 0 0 0 59997 8 0 0 25 0 1 0 542125934 12615680 2666 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3080 2666 603 41 0 3039 0
vsize: 12320
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2688 0 0 0 60998 8 0 0 25 0 1 0 542125934 12615680 2666 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3080 2666 603 41 0 3039 0
vsize: 12320
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2732 0 0 0 61997 9 0 0 25 0 1 0 542125934 12746752 2710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2710 603 41 0 3071 0
vsize: 12448
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2732 0 0 0 62998 9 0 0 25 0 1 0 542125934 12746752 2710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2710 603 41 0 3071 0
vsize: 12448
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2732 0 0 0 63998 9 0 0 25 0 1 0 542125934 12746752 2710 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2710 603 41 0 3071 0
vsize: 12448
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2732 0 0 0 64998 9 0 0 25 0 1 0 542125934 12746752 2710 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2710 603 41 0 3071 0
vsize: 12448
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2732 0 0 0 65998 9 0 0 25 0 1 0 542125934 12746752 2710 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2710 603 41 0 3071 0
vsize: 12448
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2737 0 0 0 66998 9 0 0 25 0 1 0 542125934 12746752 2715 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2715 603 41 0 3071 0
vsize: 12448
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2746 0 0 0 67999 9 0 0 25 0 1 0 542125934 12746752 2724 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3112 2724 603 41 0 3071 0
vsize: 12448
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2853 0 0 0 68998 9 0 0 25 0 1 0 542125934 13283328 2831 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3243 2831 603 41 0 3202 0
vsize: 12972
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2856 0 0 0 69999 9 0 0 25 0 1 0 542125934 13283328 2834 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3243 2834 603 41 0 3202 0
vsize: 12972
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2965 0 0 0 70999 9 0 0 25 0 1 0 542125934 13680640 2943 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2943 603 41 0 3299 0
vsize: 13360
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2965 0 0 0 71999 9 0 0 25 0 1 0 542125934 13680640 2943 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2943 603 41 0 3299 0
vsize: 13360
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2965 0 0 0 72999 9 0 0 25 0 1 0 542125934 13680640 2943 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2943 603 41 0 3299 0
vsize: 13360
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2969 0 0 0 73999 9 0 0 25 0 1 0 542125934 13680640 2947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2947 603 41 0 3299 0
vsize: 13360
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2969 0 0 0 74999 9 0 0 25 0 1 0 542125934 13680640 2947 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2947 603 41 0 3299 0
vsize: 13360
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2969 0 0 0 76000 9 0 0 25 0 1 0 542125934 13680640 2947 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2947 603 41 0 3299 0
vsize: 13360
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2969 0 0 0 77000 9 0 0 25 0 1 0 542125934 13680640 2947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2947 603 41 0 3299 0
vsize: 13360
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2971 0 0 0 78000 9 0 0 25 0 1 0 542125934 13680640 2949 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2949 603 41 0 3299 0
vsize: 13360
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19014
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2971 0 0 0 79000 9 0 0 25 0 1 0 542125934 13680640 2949 4294967295 134512640 134672761 3221224544 3221222912 134565852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2949 603 41 0 3299 0
vsize: 13360
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2971 0 0 0 80000 9 0 0 25 0 1 0 542125934 13680640 2949 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2949 603 41 0 3299 0
vsize: 13360
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2971 0 0 0 81001 9 0 0 25 0 1 0 542125934 13680640 2949 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2949 603 41 0 3299 0
vsize: 13360
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2979 0 0 0 82001 9 0 0 25 0 1 0 542125934 13819904 2957 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2957 603 41 0 3333 0
vsize: 13496
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2985 0 0 0 83001 9 0 0 25 0 1 0 542125934 13819904 2963 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2963 603 41 0 3333 0
vsize: 13496
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 2985 0 0 0 84001 9 0 0 25 0 1 0 542125934 13819904 2963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3374 2963 603 41 0 3333 0
vsize: 13496
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3036 0 0 0 85001 9 0 0 25 0 1 0 542125934 13950976 3014 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3406 3014 603 41 0 3365 0
vsize: 13624
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3048 0 0 0 86001 9 0 0 25 0 1 0 542125934 14094336 3026 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3441 3026 603 41 0 3400 0
vsize: 13764
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3175 0 0 0 87001 10 0 0 25 0 1 0 542125934 14618624 3153 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3569 3153 603 41 0 3528 0
vsize: 14276
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3177 0 0 0 88001 10 0 0 25 0 1 0 542125934 14618624 3155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3569 3155 603 41 0 3528 0
vsize: 14276
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3177 0 0 0 89001 10 0 0 25 0 1 0 542125934 14618624 3155 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3569 3155 603 41 0 3528 0
vsize: 14276
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3177 0 0 0 90002 10 0 0 25 0 1 0 542125934 14618624 3155 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3569 3155 603 41 0 3528 0
vsize: 14276
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3180 0 0 0 91001 10 0 0 25 0 1 0 542125934 14618624 3158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3569 3158 603 41 0 3528 0
vsize: 14276
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3206 0 0 0 92001 10 0 0 25 0 1 0 542125934 14766080 3184 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3605 3184 603 41 0 3564 0
vsize: 14420
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3215 0 0 0 93001 10 0 0 25 0 1 0 542125934 14766080 3193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3605 3193 603 41 0 3564 0
vsize: 14420
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3239 0 0 0 94001 10 0 0 25 0 1 0 542125934 14929920 3217 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3645 3217 603 41 0 3604 0
vsize: 14580
[startup+950.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3240 0 0 0 95002 10 0 0 25 0 1 0 542125934 14929920 3218 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3645 3218 603 41 0 3604 0
vsize: 14580
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3240 0 0 0 96002 10 0 0 25 0 1 0 542125934 14929920 3218 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3645 3218 603 41 0 3604 0
vsize: 14580
[startup+970.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3240 0 0 0 97002 10 0 0 25 0 1 0 542125934 14929920 3218 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3645 3218 603 41 0 3604 0
vsize: 14580
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3254 0 0 0 98002 10 0 0 25 0 1 0 542125934 14929920 3232 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3645 3232 603 41 0 3604 0
vsize: 14580
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3256 0 0 0 99002 10 0 0 25 0 1 0 542125934 14929920 3234 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3645 3234 603 41 0 3604 0
vsize: 14580
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3261 0 0 0 100003 10 0 0 25 0 1 0 542125934 14929920 3239 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3645 3239 603 41 0 3604 0
vsize: 14580
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3265 0 0 0 101003 11 0 0 25 0 1 0 542125934 14929920 3243 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3645 3243 603 41 0 3604 0
vsize: 14580
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3281 0 0 0 102003 11 0 0 25 0 1 0 542125934 15077376 3259 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3259 603 41 0 3640 0
vsize: 14724
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3293 0 0 0 103003 11 0 0 25 0 1 0 542125934 15077376 3271 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3271 603 41 0 3640 0
vsize: 14724
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3293 0 0 0 104003 11 0 0 25 0 1 0 542125934 15077376 3271 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3271 603 41 0 3640 0
vsize: 14724
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3293 0 0 0 105003 11 0 0 25 0 1 0 542125934 15077376 3271 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3271 603 41 0 3640 0
vsize: 14724
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3293 0 0 0 106004 11 0 0 25 0 1 0 542125934 15077376 3271 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3681 3271 603 41 0 3640 0
vsize: 14724
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3299 0 0 0 107004 11 0 0 25 0 1 0 542125934 15241216 3277 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3721 3277 603 41 0 3680 0
vsize: 14884
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3299 0 0 0 108004 11 0 0 25 0 1 0 542125934 15241216 3277 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3721 3277 603 41 0 3680 0
vsize: 14884
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19016
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3333 0 0 0 109004 11 0 0 25 0 1 0 542125934 15372288 3311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3753 3311 603 41 0 3712 0
vsize: 15012
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3335 0 0 0 110004 11 0 0 25 0 1 0 542125934 15372288 3313 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3753 3313 603 41 0 3712 0
vsize: 15012
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3337 0 0 0 111005 11 0 0 25 0 1 0 542125934 15372288 3315 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3753 3315 603 41 0 3712 0
vsize: 15012
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3399 0 0 0 112004 11 0 0 25 0 1 0 542125934 15638528 3377 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3818 3377 603 41 0 3777 0
vsize: 15272
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3406 0 0 0 113003 11 0 0 25 0 1 0 542125934 15638528 3384 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3818 3384 603 41 0 3777 0
vsize: 15272
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3413 0 0 0 114003 11 0 0 25 0 1 0 542125934 15638528 3391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3818 3391 603 41 0 3777 0
vsize: 15272
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3420 0 0 0 115003 11 0 0 25 0 1 0 542125934 15638528 3398 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3818 3398 603 41 0 3777 0
vsize: 15272
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3421 0 0 0 116003 11 0 0 25 0 1 0 542125934 15638528 3399 4294967295 134512640 134672761 3221224544 3221223696 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3818 3399 603 41 0 3777 0
vsize: 15272
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3551 0 0 0 117003 12 0 0 25 0 1 0 542125934 16171008 3529 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3948 3529 603 41 0 3907 0
vsize: 15792
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3562 0 0 0 118003 12 0 0 25 0 1 0 542125934 16310272 3540 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3982 3540 603 41 0 3941 0
vsize: 15928
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3562 0 0 0 119003 12 0 0 25 0 1 0 542125934 16310272 3540 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3982 3540 603 41 0 3941 0
vsize: 15928
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 19018
Raw data (stat): 19010 (minisat+) R 19009 20024 20023 0 -1 0 3562 0 0 0 120003 12 0 0 25 0 1 0 542125934 16310272 3540 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3982 3540 603 41 0 3941 0
vsize: 15928
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 19018
Raw data (stat): 19010 (minisat+) Z 19009 20024 20023 0 -1 12 3565 0 0 0 120003 13 0 0 25 0 1 0 542125934 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.05
CPU time (s): 1200.17
CPU user time (s): 1200.04
CPU system time (s): 0.133979
CPU usage (%): 100.01
Max. virtual memory (Kb): 15928
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####