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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        589104 kB
Buffers:         31160 kB
Cached:         392856 kB
SwapCached:        440 kB
Active:          54264 kB
Inactive:       371880 kB
HighTotal:      131008 kB
HighFree:         4508 kB
LowTotal:       903652 kB
LowFree:        584596 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            13896 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 16:21:56 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 17651 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 431615   bits: 20/19
c ---[  10]---> Adder-cost: 380   maxlim: 461183   bits: 20/19
c ---[   8]---> Adder-cost: 350   maxlim: 445183   bits: 20/19
c ---[   6]---> Adder-cost: 340   maxlim: 477951   bits: 20/19
c ---[   4]---> Adder-cost: 390   maxlim: 451839   bits: 20/19
c ---[   2]---> Adder-cost: 358   maxlim: 468735   bits: 20/19
c ---[   0]---> Adder-cost: 374   maxlim: 444543   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17222    61228 |    5740       0        0     nan |  0.000 % |
c |       100 |   17222    61228 |    6314     100      905     9.1 |  9.969 % |
c |       253 |   17214    61202 |    6945     252     2033     8.1 | 10.003 % |
c |       478 |   17206    61176 |    7639     476     4722     9.9 | 10.038 % |
c ==============================================================================
c [1mFound solution: 866304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 132   maxlim: 7561   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       536 |   18085    64319 |    6028     534     5740    10.7 | 10.038 % |
c |       637 |   18077    64293 |    6630     634    15148    23.9 |  9.844 % |
c ==============================================================================
c [1mFound solution: 796032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8110   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       717 |   18093    64412 |    6031     713    23144    32.5 |  9.844 % |
c ==============================================================================
c [1mFound solution: 739200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8554   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       784 |   18090    64361 |    6030     780    29197    37.4 |  9.844 % |
c ==============================================================================
c [1mFound solution: 656768[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9198   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       786 |   18104    64455 |    6034     782    29422    37.6 |  9.844 % |
c ==============================================================================
c [1mFound solution: 608512[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9575   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       823 |   18113    64499 |    6037     819    33808    41.3 |  9.844 % |
c |       925 |   18113    64499 |    6640     921    41090    44.6 | 10.697 % |
c |      1075 |   18113    64499 |    7304    1071    49999    46.7 | 10.697 % |
c |      1302 |   18105    64473 |    8035    1297    66595    51.3 | 10.729 % |
c |      1640 |   18105    64473 |    8838    1635    97382    59.6 | 10.729 % |
c |      2146 |   18097    64447 |    9722    2140   132176    61.8 | 10.762 % |
c ==============================================================================
c [1mFound solution: 524416[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10232   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2474 |   18113    64540 |    6037    2468   155271    62.9 | 10.762 % |
c |      2574 |   18113    64540 |    6640    2568   166449    64.8 | 10.981 % |
c |      2724 |   18113    64540 |    7304    2718   173761    63.9 | 10.981 % |
c |      2949 |   18113    64540 |    8035    2943   210406    71.5 | 10.981 % |
c |      3288 |   18105    64514 |    8838    3281   246627    75.2 | 11.013 % |
c |      3795 |   18105    64514 |    9722    3788   290585    76.7 | 11.013 % |
c |      4555 |   18105    64514 |   10694    4548   354044    77.8 | 11.013 % |
c |      5696 |   18105    64514 |   11764    5689   450685    79.2 | 11.013 % |
c |      7404 |   18089    64462 |   12940    7395   638931    86.4 | 11.079 % |
c |      9966 |   18073    64410 |   14234    9955   831697    83.5 | 11.144 % |
c |     13810 |   18073    64410 |   15658   13799  1183858    85.8 | 11.144 % |
c |     19577 |   18073    64410 |   17224   11147   898549    80.6 | 11.144 % |
c |     28227 |   18043    64314 |   18946   10550   763825    72.4 | 11.274 % |
c |     41204 |   18027    64262 |   20841   13318  1253972    94.2 | 11.339 % |
c |     60666 |   18019    64236 |   22925   21731  2009045    92.5 | 11.372 % |
c ==============================================================================
c [1mFound solution: 430848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10963   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84392 |   18019    64263 |    6006   21154  2023386    95.7 | 11.372 % |
c |     84493 |   18010    64232 |    6606    5388   305691    56.7 | 11.610 % |
c |     84644 |   18010    64232 |    7267    5539   314462    56.8 | 11.610 % |
c |     84869 |   18010    64232 |    7993    5764   332622    57.7 | 11.610 % |
c |     85206 |   18010    64232 |    8793    6101   357368    58.6 | 11.610 % |
c |     85713 |   18010    64232 |    9672    6608   384348    58.2 | 11.610 % |
c |     86472 |   18010    64232 |   10639    7367   432022    58.6 | 11.610 % |
c |     87611 |   18010    64232 |   11703    8506   514488    60.5 | 11.610 % |
c ==============================================================================
c [1mFound solution: 411392[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11115   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87791 |   18020    64284 |    6006    8686   517914    59.6 | 11.610 % |
c |     87892 |   18020    64284 |    6606    4444   188253    42.4 | 11.734 % |
c |     88042 |   18020    64284 |    7267    4594   195630    42.6 | 11.734 % |
c |     88270 |   18020    64284 |    7993    4822   208260    43.2 | 11.734 % |
c |     88608 |   18020    64284 |    8793    5160   235354    45.6 | 11.734 % |
c ==============================================================================
c [1mFound solution: 409344[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11131   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88852 |   18025    64321 |    6008    5404   239679    44.4 | 11.734 % |
c |     88954 |   18025    64321 |    6608    5506   244732    44.4 | 11.812 % |
c |     89104 |   18025    64321 |    7269    5656   260573    46.1 | 11.812 % |
c |     89329 |   18025    64321 |    7996    5881   284484    48.4 | 11.812 % |
c |     89667 |   18025    64321 |    8796    6219   331582    53.3 | 11.812 % |
c |     90175 |   18019    64303 |    9675    6726   364314    54.2 | 11.845 % |
c |     90935 |   18019    64303 |   10643    7486   431418    57.6 | 11.845 % |
c |     92074 |   18019    64303 |   11707    8625   508703    59.0 | 11.845 % |
c |     93784 |   18019    64303 |   12878   10335   624574    60.4 | 11.845 % |
c |     96346 |   18019    64303 |   14166   12897   845513    65.6 | 11.845 % |
c |    100191 |   18019    64303 |   15583    9110   547645    60.1 | 11.845 % |
c |    105959 |   18019    64303 |   17141   14878  1151344    77.4 | 11.845 % |
c |    114608 |   18013    64283 |   18855   14314  1108121    77.4 | 11.877 % |
c |    127583 |   18013    64283 |   20741   17515  1349659    77.1 | 11.877 % |
c |    147044 |   18013    64283 |   22815   14765   954870    64.7 | 11.877 % |
c ==============================================================================
c [1mFound solution: 392832[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11260   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    171301 |   18020    64339 |    6006   15110   789597    52.3 | 11.877 % |
c |    171401 |   18020    64339 |    6606    3878   118447    30.5 | 12.085 % |
c |    171551 |   18011    64312 |    7267    4027   125118    31.1 | 12.150 % |
c |    171778 |   18011    64312 |    7993    4254   136343    32.1 | 12.150 % |
c |    172115 |   18011    64312 |    8793    4591   144847    31.6 | 12.150 % |
c |    172621 |   18011    64312 |    9672    5097   165507    32.5 | 12.150 % |
c |    173383 |   18011    64312 |   10639    5859   211700    36.1 | 12.150 % |
c |    174523 |   18011    64312 |   11703    6999   268874    38.4 | 12.150 % |
c |    176232 |   18011    64312 |   12874    8708   385844    44.3 | 12.150 % |
c |    178795 |   18002    64285 |   14161   11263   727905    64.6 | 12.214 % |
c |    182639 |   18002    64285 |   15578   15107   958921    63.5 | 12.214 % |
c |    188406 |   18002    64285 |   17135   12646   823121    65.1 | 12.214 % |
c |    197057 |   17993    64258 |   18849   12109  1102200    91.0 | 12.278 % |
c ==============================================================================
c [1mFound solution: 384896[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11322   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    197119 |   18002    64325 |    6000   12171  1104627    90.8 | 12.278 % |
c |    197221 |   18002    64325 |    6600    6188   466931    75.5 | 12.436 % |
c |    197372 |   18002    64325 |    7260    6339   473557    74.7 | 12.436 % |
c |    197597 |   18002    64325 |    7986    6564   484551    73.8 | 12.436 % |
c |    197934 |   18002    64325 |    8784    6901   506563    73.4 | 12.436 % |
c ==============================================================================
c [1mFound solution: 163968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13048   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    198114 |   17912    63794 |    5970    7057   508250    72.0 | 12.436 % |
c |    198214 |   17912    63794 |    6567    3629   105166    29.0 | 12.984 % |
c |    198364 |   17912    63794 |    7223    3779   110348    29.2 | 12.984 % |
c |    198591 |   17912    63794 |    7946    4006   124565    31.1 | 12.984 % |
c |    198931 |   17912    63794 |    8740    4346   136538    31.4 | 12.984 % |
c |    199438 |   17912    63794 |    9614    4853   192185    39.6 | 12.984 % |
c |    200198 |   17912    63794 |   10576    5613   223363    39.8 | 12.984 % |
c |    201337 |   17912    63794 |   11633    6752   327169    48.5 | 12.984 % |
c |    203046 |   17912    63794 |   12797    8461   407926    48.2 | 12.984 % |
c |    205608 |   17912    63794 |   14076   11023   596443    54.1 | 12.984 % |
c |    209452 |   17912    63794 |   15484   14867   817596    55.0 | 12.984 % |
c |    215218 |   17912    63794 |   17033   12358   518675    42.0 | 12.984 % |
c |    223867 |   17904    63772 |   18736   11931   607674    50.9 | 13.048 % |
c |    236843 |   17904    63772 |   20610   14943   776645    52.0 | 13.048 % |
c |    256305 |   17896    63746 |   22671   12846   589680    45.9 | 13.080 % |
c |    285497 |   17896    63746 |   24938   18435  1128680    61.2 | 13.080 % |
c ==============================================================================
c [1mFound solution: 88064[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 6473   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    294034 |   17863    63631 |    5954   12961   579315    44.7 | 13.080 % |
c |    294136 |   17863    63631 |    6549    3343    81611    24.4 | 13.526 % |
c |    294286 |   17863    63631 |    7204    3493    85031    24.3 | 13.526 % |
c |    294511 |   17863    63631 |    7924    3718    92878    25.0 | 13.526 % |
c |    294850 |   17851    63589 |    8717    4054   104842    25.9 | 13.558 % |
c |    295356 |   17851    63589 |    9588    4560   122820    26.9 | 13.558 % |
c |    296116 |   17851    63589 |   10547    5320   149542    28.1 | 13.558 % |
c |    297255 |   17851    63589 |   11602    6459   198269    30.7 | 13.558 % |
c |    298963 |   17832    63524 |   12762    8165   270071    33.1 | 13.622 % |
c |    301525 |   17765    63274 |   14039   10721   380855    35.5 | 14.036 % |
c ==============================================================================
c [1mFound solution: 69632[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6617   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    301775 |   17774    63315 |    5924   10971   383344    34.9 | 14.036 % |
c |    301876 |   17774    63315 |    6516    5587   177764    31.8 | 14.154 % |
c |    302027 |   17774    63315 |    7168    5738   180275    31.4 | 14.154 % |
c |    302254 |   17774    63315 |    7884    5965   188355    31.6 | 14.154 % |
c |    302595 |   17774    63315 |    8673    6306   195005    30.9 | 14.154 % |
c |    303102 |   17774    63315 |    9540    6813   207170    30.4 | 14.154 % |
c |    303862 |   17774    63315 |   10494    7573   240407    31.7 | 14.154 % |
c |    305003 |   17774    63315 |   11544    8714   282781    32.5 | 14.154 % |
c |    306711 |   17774    63315 |   12698   10422   497642    47.7 | 14.154 % |
c |    309273 |   17774    63315 |   13968   12984   605529    46.6 | 14.154 % |
c |    313117 |   17774    63315 |   15365    9483   407409    43.0 | 14.154 % |
c |    318883 |   17774    63315 |   16901   15249   637155    41.8 | 14.154 % |
c |    327533 |   17774    63315 |   18592   15032   856877    57.0 | 14.154 % |
c |    340507 |   17774    63315 |   20451   18288   893857    48.9 | 14.154 % |
c |    359968 |   17774    63315 |   22496   16369   901883    55.1 | 14.154 % |
c ==============================================================================
c [1mFound solution: 59264[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 3114   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    374540 |   17743    63208 |    5914   19114  1113202    58.2 | 14.154 % |
c |    374641 |   17743    63208 |    6505    4880   263734    54.0 | 14.583 % |
c |    374793 |   17743    63208 |    7155    5032   265457    52.8 | 14.583 % |
c |    375018 |   17743    63208 |    7871    5257   284010    54.0 | 14.583 % |
c |    375356 |   17743    63208 |    8658    5595   292970    52.4 | 14.583 % |
c |    375862 |   17743    63208 |    9524    6101   328028    53.8 | 14.583 % |
c |    376623 |   17743    63208 |   10477    6862   353363    51.5 | 14.583 % |
c |    377762 |   17731    63166 |   11524    7998   397753    49.7 | 14.615 % |
c |    379471 |   17731    63166 |   12677    9707   465202    47.9 | 14.615 % |
c |    382034 |   17716    63113 |   13944   12267   609375    49.7 | 14.646 % |
c |    385879 |   17716    63113 |   15339    8552   389233    45.5 | 14.646 % |
c |    391645 |   17716    63113 |   16873   14318   626322    43.7 | 14.646 % |
c |    400294 |   17716    63113 |   18560   14196   589367    41.5 | 14.646 % |
c |    413268 |   17716    63113 |   20416   17429   767074    44.0 | 14.646 % |
c |    432729 |   17703    63070 |   22458   15579   698124    44.8 | 14.773 % |
c |    461922 |   17642    62829 |   24704   21279  1022753    48.1 | 15.120 % |
c ==============================================================================
c [1mFound solution: 56448[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3136   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    503646 |   17645    62845 |    5881   24287  1284894    52.9 | 15.120 % |
c |    503747 |   17645    62845 |    6469    6173   302882    49.1 | 15.169 % |
c |    503897 |   17645    62845 |    7116    6323   307603    48.6 | 15.169 % |
c |    504122 |   17645    62845 |    7827    6548   311869    47.6 | 15.169 % |
c |    504460 |   17645    62845 |    8610    6886   317628    46.1 | 15.169 % |
c |    504967 |   17645    62845 |    9471    7393   331083    44.8 | 15.169 % |
c |    505726 |   17645    62845 |   10418    8152   382065    46.9 | 15.169 % |
c |    506865 |   17645    62845 |   11460    9291   428824    46.2 | 15.169 % |
c |    508574 |   17645    62845 |   12606   11000   484854    44.1 | 15.169 % |
c |    511138 |   17645    62845 |   13867    6798   249604    36.7 | 15.169 % |
c |    514982 |   17645    62845 |   15253   10642   402519    37.8 | 15.169 % |
c |    520748 |   17645    62845 |   16779    8288   312288    37.7 | 15.169 % |
c |    529397 |   17645    62845 |   18457   16937   711178    42.0 | 15.169 % |
c |    542374 |   17645    62845 |   20302   10399   399450    38.4 | 15.169 % |
c |    561835 |   17645    62845 |   22333   19065  1102391    57.8 | 15.169 % |
c |    591030 |   17645    62845 |   24566   13518   744512    55.1 | 15.169 % |
c |    634819 |   17645    62845 |   27023   18923   860379    45.5 | 15.169 % |
c |    700503 |   17645    62845 |   29725   14818   683233    46.1 | 15.169 % |
#### 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.86 0.97 0.91 2/54 10589
Raw data (stat): 10589 (runsolver) R 10588 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488137137 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0016 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 1176 0 0 0 996 2 0 0 25 0 1 0 488137137 6483968 1154 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1583 1154 603 41 0 1542 0
vsize: 6332
[startup+20.002 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 1609 0 0 0 1993 4 0 0 25 0 1 0 488137137 8245248 1587 4294967295 134512640 134672761 3221224544 3221223728 134558671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2013 1587 603 41 0 1972 0
vsize: 8052
[startup+30.0022 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 1922 0 0 0 2992 5 0 0 25 0 1 0 488137137 9568256 1900 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2336 1900 603 41 0 2295 0
vsize: 9344
[startup+40.0023 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 2317 0 0 0 3991 6 0 0 25 0 1 0 488137137 11173888 2295 4294967295 134512640 134672761 3221224544 3221223264 134565791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2728 2295 603 41 0 2687 0
vsize: 10912
[startup+50.0023 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 2317 0 0 0 4991 6 0 0 25 0 1 0 488137137 11173888 2295 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2728 2295 603 41 0 2687 0
vsize: 10912
[startup+60.0034 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 2317 0 0 0 5991 6 0 0 25 0 1 0 488137137 11173888 2295 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2728 2295 603 41 0 2687 0
vsize: 10912
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 2479 0 0 0 6990 7 0 0 25 0 1 0 488137137 11841536 2457 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2891 2457 603 41 0 2850 0
vsize: 11564
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 2479 0 0 0 7990 7 0 0 25 0 1 0 488137137 11841536 2457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2891 2457 603 41 0 2850 0
vsize: 11564
[startup+90.0042 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 2479 0 0 0 8991 7 0 0 25 0 1 0 488137137 11841536 2457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2891 2457 603 41 0 2850 0
vsize: 11564
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 2677 0 0 0 9990 7 0 0 25 0 1 0 488137137 12632064 2655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3084 2655 603 41 0 3043 0
vsize: 12336
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 2816 0 0 0 10990 7 0 0 25 0 1 0 488137137 13320192 2794 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3252 2794 603 41 0 3211 0
vsize: 13008
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 2816 0 0 0 11990 7 0 0 25 0 1 0 488137137 13320192 2794 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3252 2794 603 41 0 3211 0
vsize: 13008
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 2825 0 0 0 12991 7 0 0 25 0 1 0 488137137 13320192 2803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3252 2803 603 41 0 3211 0
vsize: 13008
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3159 0 0 0 13989 9 0 0 25 0 1 0 488137137 14651392 3137 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3577 3137 603 41 0 3536 0
vsize: 14308
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3222 0 0 0 14990 9 0 0 25 0 1 0 488137137 14917632 3200 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3642 3200 603 41 0 3601 0
vsize: 14568
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3222 0 0 0 15990 9 0 0 25 0 1 0 488137137 14917632 3200 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3642 3200 603 41 0 3601 0
vsize: 14568
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3227 0 0 0 16990 9 0 0 25 0 1 0 488137137 14917632 3205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3642 3205 603 41 0 3601 0
vsize: 14568
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3242 0 0 0 17990 9 0 0 25 0 1 0 488137137 15060992 3220 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3677 3220 603 41 0 3636 0
vsize: 14708
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3420 0 0 0 18989 10 0 0 25 0 1 0 488137137 15847424 3398 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3398 603 41 0 3828 0
vsize: 15476
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3420 0 0 0 19989 10 0 0 25 0 1 0 488137137 15847424 3398 4294967295 134512640 134672761 3221224544 3221223728 134559553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3398 603 41 0 3828 0
vsize: 15476
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3420 0 0 0 20990 10 0 0 25 0 1 0 488137137 15847424 3398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3398 603 41 0 3828 0
vsize: 15476
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3424 0 0 0 21990 10 0 0 25 0 1 0 488137137 15847424 3402 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3402 603 41 0 3828 0
vsize: 15476
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3447 0 0 0 22990 10 0 0 25 0 1 0 488137137 15847424 3425 4294967295 134512640 134672761 3221224544 3221223728 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3425 603 41 0 3828 0
vsize: 15476
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10589
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3447 0 0 0 23990 10 0 0 25 0 1 0 488137137 15847424 3425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3425 603 41 0 3828 0
vsize: 15476
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3447 0 0 0 24990 10 0 0 25 0 1 0 488137137 15847424 3425 4294967295 134512640 134672761 3221224544 3221223728 134558764 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3869 3425 603 41 0 3828 0
vsize: 15476
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3451 0 0 0 25990 10 0 0 25 0 1 0 488137137 15986688 3429 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3429 603 41 0 3862 0
vsize: 15612
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 26990 10 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 27990 10 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223744 134557814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 28989 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 29990 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 30990 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 31990 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 32990 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223680 134565078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 33990 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 34990 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 35991 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 36991 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 37991 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 38991 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 39991 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 40991 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 41992 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 42992 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 43992 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 44992 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 45992 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 46992 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3454 0 0 0 47993 11 0 0 25 0 1 0 488137137 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 48993 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 49993 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 50993 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 51993 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 52993 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 53993 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 54993 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 55994 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 56994 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 57994 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 58994 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 59994 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3455 0 0 0 60994 11 0 0 25 0 1 0 488137137 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 61994 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 62995 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 63995 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 64995 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 65995 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 66995 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 67995 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 68996 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 69996 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 70996 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 71996 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 72996 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 73996 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 74996 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 75997 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134559063 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 76997 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 77997 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 78997 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223544 1075350342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+800.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 79997 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 80997 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 81998 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 82998 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 83998 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+850.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 84998 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 85998 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 86998 11 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 87998 12 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 88999 12 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 89999 12 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+910.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 90999 12 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+920.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 91999 12 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+930.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 92999 12 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+940.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 93999 12 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+950.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 95000 12 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+960.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 96000 12 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3457 0 0 0 97000 12 0 0 25 0 1 0 488137137 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+980.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3472 0 0 0 98000 12 0 0 25 0 1 0 488137137 15986688 3450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3450 603 41 0 3862 0
vsize: 15612
[startup+990.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3476 0 0 0 99000 12 0 0 25 0 1 0 488137137 15986688 3454 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3454 603 41 0 3862 0
vsize: 15612
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3485 0 0 0 100000 12 0 0 25 0 1 0 488137137 15986688 3463 4294967295 134512640 134672761 3221224544 3221223744 134557915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3903 3463 603 41 0 3862 0
vsize: 15612
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3490 0 0 0 101000 12 0 0 25 0 1 0 488137137 16125952 3468 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3937 3468 603 41 0 3896 0
vsize: 15748
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3543 0 0 0 102000 12 0 0 25 0 1 0 488137137 16261120 3521 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3970 3521 603 41 0 3929 0
vsize: 15880
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3551 0 0 0 103001 12 0 0 25 0 1 0 488137137 16261120 3529 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3970 3529 603 41 0 3929 0
vsize: 15880
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3598 0 0 0 104001 12 0 0 25 0 1 0 488137137 16527360 3576 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4035 3576 603 41 0 3994 0
vsize: 16140
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3632 0 0 0 105000 12 0 0 25 0 1 0 488137137 16670720 3610 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4070 3610 603 41 0 4029 0
vsize: 16280
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3647 0 0 0 106001 12 0 0 25 0 1 0 488137137 16809984 3625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4104 3625 603 41 0 4063 0
vsize: 16416
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3647 0 0 0 107001 12 0 0 25 0 1 0 488137137 16809984 3625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4104 3625 603 41 0 4063 0
vsize: 16416
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3655 0 0 0 108001 12 0 0 25 0 1 0 488137137 16809984 3633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4104 3633 603 41 0 4063 0
vsize: 16416
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3661 0 0 0 109001 12 0 0 25 0 1 0 488137137 16809984 3639 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4104 3639 603 41 0 4063 0
vsize: 16416
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3734 0 0 0 110001 13 0 0 25 0 1 0 488137137 17076224 3712 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4169 3712 603 41 0 4128 0
vsize: 16676
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3739 0 0 0 111001 13 0 0 25 0 1 0 488137137 17076224 3717 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4169 3717 603 41 0 4128 0
vsize: 16676
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3823 0 0 0 112001 13 0 0 25 0 1 0 488137137 17473536 3801 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4266 3801 603 41 0 4225 0
vsize: 17064
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3823 0 0 0 113001 13 0 0 25 0 1 0 488137137 17473536 3801 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4266 3801 603 41 0 4225 0
vsize: 17064
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3827 0 0 0 114002 13 0 0 25 0 1 0 488137137 17473536 3805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4266 3805 603 41 0 4225 0
vsize: 17064
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3899 0 0 0 115002 13 0 0 25 0 1 0 488137137 17747968 3877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4333 3877 603 41 0 4292 0
vsize: 17332
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3912 0 0 0 116002 13 0 0 25 0 1 0 488137137 17887232 3890 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4367 3890 603 41 0 4326 0
vsize: 17468
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3912 0 0 0 117002 13 0 0 25 0 1 0 488137137 17887232 3890 4294967295 134512640 134672761 3221224544 3221223712 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4367 3890 603 41 0 4326 0
vsize: 17468
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3912 0 0 0 118002 13 0 0 25 0 1 0 488137137 17887232 3890 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4367 3890 603 41 0 4326 0
vsize: 17468
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 3994 0 0 0 119002 13 0 0 25 0 1 0 488137137 18157568 3972 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4433 3972 603 41 0 4392 0
vsize: 17732
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10591
Raw data (stat): 10589 (minisat+) R 10588 29151 29150 0 -1 0 4158 0 0 0 120002 14 0 0 25 0 1 0 488137137 18829312 4136 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4597 4136 603 41 0 4556 0
vsize: 18388
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 10591
Raw data (stat): 10589 (minisat+) Z 10588 29151 29150 0 -1 12 4161 0 0 0 120002 15 0 0 25 0 1 0 488137137 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.02
CPU time (s): 1200.17
CPU user time (s): 1200.02
CPU system time (s): 0.150977
CPU usage (%): 100.012
Max. virtual memory (Kb): 18388
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####