PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        753624 kB
Buffers:         14620 kB
Cached:         237072 kB
SwapCached:        520 kB
Active:          54988 kB
Inactive:       198824 kB
HighTotal:      131008 kB
HighFree:         1820 kB
LowTotal:       903652 kB
LowFree:        751804 kB
SwapTotal:     2097136 kB
SwapFree:      2095824 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            21560 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:18:15 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 18522 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.64 0.88 0.88 2/54 27737
Raw data (stat): 27737 (runsolver) R 27736 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541658678 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.69 0.88 0.88 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 1178 0 0 0 996 2 0 0 25 0 1 0 541658678 6483968 1156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1583 1156 603 41 0 1542 0
vsize: 6332
[startup+20.0012 s]
Raw data (loadavg): 0.74 0.89 0.88 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 1611 0 0 0 1993 4 0 0 25 0 1 0 541658678 8245248 1589 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2013 1589 603 41 0 1972 0
vsize: 8052
[startup+30.0018 s]
Raw data (loadavg): 0.78 0.89 0.88 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 1915 0 0 0 2993 5 0 0 25 0 1 0 541658678 9568256 1893 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2336 1893 603 41 0 2295 0
vsize: 9344
[startup+40.0013 s]
Raw data (loadavg): 0.81 0.89 0.88 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 2295 0 0 0 3991 7 0 0 25 0 1 0 541658678 11173888 2273 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2728 2273 603 41 0 2687 0
vsize: 10912
[startup+50.0025 s]
Raw data (loadavg): 0.84 0.89 0.89 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 2317 0 0 0 4991 7 0 0 25 0 1 0 541658678 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+60.0029 s]
Raw data (loadavg): 0.86 0.90 0.89 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 2317 0 0 0 5991 7 0 0 25 0 1 0 541658678 11173888 2295 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2728 2295 603 41 0 2687 0
vsize: 10912
[startup+70.0032 s]
Raw data (loadavg): 0.89 0.90 0.89 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 2479 0 0 0 6991 8 0 0 25 0 1 0 541658678 11841536 2457 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2891 2457 603 41 0 2850 0
vsize: 11564
[startup+80.0042 s]
Raw data (loadavg): 0.90 0.90 0.89 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 2479 0 0 0 7991 8 0 0 25 0 1 0 541658678 11841536 2457 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2891 2457 603 41 0 2850 0
vsize: 11564
[startup+90.0038 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 2479 0 0 0 8991 8 0 0 25 0 1 0 541658678 11841536 2457 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2891 2457 603 41 0 2850 0
vsize: 11564
[startup+100.004 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 2601 0 0 0 9991 8 0 0 25 0 1 0 541658678 12369920 2579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2579 603 41 0 2979 0
vsize: 12080
[startup+110.005 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 27737
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 2816 0 0 0 10990 9 0 0 25 0 1 0 541658678 13320192 2794 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2794 603 41 0 3211 0
vsize: 13008
[startup+120.006 s]
Raw data (loadavg): 1.02 0.93 0.90 2/54 27790
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 2816 0 0 0 11990 9 0 0 25 0 1 0 541658678 13320192 2794 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2794 603 41 0 3211 0
vsize: 13008
[startup+130.005 s]
Raw data (loadavg): 1.02 0.93 0.90 2/54 27790
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 2824 0 0 0 12990 9 0 0 25 0 1 0 541658678 13320192 2802 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2802 603 41 0 3211 0
vsize: 13008
[startup+140.005 s]
Raw data (loadavg): 1.02 0.93 0.90 2/54 27790
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3045 0 0 0 13989 10 0 0 25 0 1 0 541658678 14258176 3023 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3481 3023 603 41 0 3440 0
vsize: 13924
[startup+150.006 s]
Raw data (loadavg): 1.01 0.94 0.90 2/54 27790
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3222 0 0 0 14989 10 0 0 25 0 1 0 541658678 14917632 3200 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3200 603 41 0 3601 0
vsize: 14568
[startup+160.005 s]
Raw data (loadavg): 1.01 0.94 0.90 2/54 27790
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3222 0 0 0 15989 10 0 0 25 0 1 0 541658678 14917632 3200 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3200 603 41 0 3601 0
vsize: 14568
[startup+170.006 s]
Raw data (loadavg): 1.01 0.94 0.90 2/54 27790
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3222 0 0 0 16989 10 0 0 25 0 1 0 541658678 14917632 3200 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3200 603 41 0 3601 0
vsize: 14568
[startup+180.006 s]
Raw data (loadavg): 1.01 0.94 0.90 2/54 27790
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3227 0 0 0 17989 10 0 0 25 0 1 0 541658678 14917632 3205 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3205 603 41 0 3601 0
vsize: 14568
[startup+190.005 s]
Raw data (loadavg): 1.00 0.94 0.90 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3358 0 0 0 18989 11 0 0 25 0 1 0 541658678 15585280 3336 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3805 3336 603 41 0 3764 0
vsize: 15220
[startup+200.005 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3420 0 0 0 19989 11 0 0 25 0 1 0 541658678 15847424 3398 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3869 3398 603 41 0 3828 0
vsize: 15476
[startup+210.004 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3420 0 0 0 20989 11 0 0 25 0 1 0 541658678 15847424 3398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3869 3398 603 41 0 3828 0
vsize: 15476
[startup+220.005 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3420 0 0 0 21989 11 0 0 25 0 1 0 541658678 15847424 3398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3869 3398 603 41 0 3828 0
vsize: 15476
[startup+230.005 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3424 0 0 0 22989 11 0 0 25 0 1 0 541658678 15847424 3402 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3869 3402 603 41 0 3828 0
vsize: 15476
[startup+240.004 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3447 0 0 0 23989 11 0 0 25 0 1 0 541658678 15847424 3425 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3869 3425 603 41 0 3828 0
vsize: 15476
[startup+250.004 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3447 0 0 0 24989 11 0 0 25 0 1 0 541658678 15847424 3425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3869 3425 603 41 0 3828 0
vsize: 15476
[startup+260.004 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3447 0 0 0 25990 11 0 0 25 0 1 0 541658678 15847424 3425 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3869 3425 603 41 0 3828 0
vsize: 15476
[startup+270.004 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3452 0 0 0 26990 11 0 0 25 0 1 0 541658678 15986688 3430 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3430 603 41 0 3862 0
vsize: 15612
[startup+280.004 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 27989 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.004 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 28989 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+300.005 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 29990 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+310.004 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 30990 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+320.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 31990 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+330.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 32990 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+340.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 33991 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+350.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 34991 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+360.006 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 35991 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+370.006 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 36991 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+380.006 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 37991 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223648 134555373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+390.005 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 38991 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+400.006 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 39992 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+410.006 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 40992 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+420.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27792
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 41992 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223648 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+430.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 42992 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+440.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 43992 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+450.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 44993 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+460.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 45993 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+470.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 46993 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+480.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 47993 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+490.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3454 0 0 0 48993 12 0 0 25 0 1 0 541658678 15986688 3432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3432 603 41 0 3862 0
vsize: 15612
[startup+500.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 49993 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+510.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 50993 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+520.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 51993 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+530.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 52994 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+540.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 53994 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+550.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 54994 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+560.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 55994 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+570.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 56994 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+580.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 57995 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+590.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 58995 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+600.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 59995 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+610.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 60995 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+620.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 61995 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+630.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3455 0 0 0 62995 12 0 0 25 0 1 0 541658678 15986688 3433 4294967295 134512640 134672761 3221224544 3221223728 134558836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3433 603 41 0 3862 0
vsize: 15612
[startup+640.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 63995 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+650.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 64995 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+660.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 65996 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+670.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 66996 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+680.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 67996 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+690.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 68996 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+700.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 69996 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+710.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 70996 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+720.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 71996 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+730.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 72997 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+740.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 73997 12 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+750.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 74997 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+760.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 75997 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+770.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 76997 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+780.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 77997 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+790.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 78997 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+800.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 79998 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+810.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 80998 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+820.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 81998 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+830.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 82998 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+840.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 83998 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+850.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 84998 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+860.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 85998 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+870.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 86998 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+880.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 87999 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+890.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 88999 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223696 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+900.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 89999 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+910.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 90999 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+920.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 91999 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+930.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 92999 13 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+940.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 93999 14 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+950.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 94999 14 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+960.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 95999 14 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+970.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 96999 14 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+980.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 97999 14 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+990.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 98999 14 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+1000 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3457 0 0 0 99999 14 0 0 25 0 1 0 541658678 15986688 3435 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3435 603 41 0 3862 0
vsize: 15612
[startup+1010 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3472 0 0 0 100999 14 0 0 25 0 1 0 541658678 15986688 3450 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3450 603 41 0 3862 0
vsize: 15612
[startup+1020 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3476 0 0 0 102000 14 0 0 25 0 1 0 541658678 15986688 3454 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3454 603 41 0 3862 0
vsize: 15612
[startup+1030 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3485 0 0 0 103000 14 0 0 25 0 1 0 541658678 15986688 3463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3903 3463 603 41 0 3862 0
vsize: 15612
[startup+1040 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3490 0 0 0 103999 14 0 0 25 0 1 0 541658678 16125952 3468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3937 3468 603 41 0 3896 0
vsize: 15748
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3543 0 0 0 104998 15 0 0 25 0 1 0 541658678 16261120 3521 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3970 3521 603 41 0 3929 0
vsize: 15880
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3551 0 0 0 105998 15 0 0 25 0 1 0 541658678 16261120 3529 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3970 3529 603 41 0 3929 0
vsize: 15880
[startup+1070 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3598 0 0 0 106997 16 0 0 25 0 1 0 541658678 16527360 3576 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4035 3576 603 41 0 3994 0
vsize: 16140
[startup+1080 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3629 0 0 0 107997 16 0 0 25 0 1 0 541658678 16670720 3607 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4070 3607 603 41 0 4029 0
vsize: 16280
[startup+1090 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3647 0 0 0 108997 16 0 0 25 0 1 0 541658678 16809984 3625 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4104 3625 603 41 0 4063 0
vsize: 16416
[startup+1100 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3647 0 0 0 109998 16 0 0 25 0 1 0 541658678 16809984 3625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4104 3625 603 41 0 4063 0
vsize: 16416
[startup+1110 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3655 0 0 0 110998 16 0 0 25 0 1 0 541658678 16809984 3633 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4104 3633 603 41 0 4063 0
vsize: 16416
[startup+1120 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3657 0 0 0 111998 16 0 0 25 0 1 0 541658678 16809984 3635 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4104 3635 603 41 0 4063 0
vsize: 16416
[startup+1130 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3734 0 0 0 112998 16 0 0 25 0 1 0 541658678 17076224 3712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4169 3712 603 41 0 4128 0
vsize: 16676
[startup+1140 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3739 0 0 0 113998 16 0 0 25 0 1 0 541658678 17076224 3717 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4169 3717 603 41 0 4128 0
vsize: 16676
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3739 0 0 0 114998 17 0 0 25 0 1 0 541658678 17076224 3717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4169 3717 603 41 0 4128 0
vsize: 16676
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3823 0 0 0 115998 17 0 0 25 0 1 0 541658678 17473536 3801 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4266 3801 603 41 0 4225 0
vsize: 17064
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3823 0 0 0 116998 17 0 0 25 0 1 0 541658678 17473536 3801 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4266 3801 603 41 0 4225 0
vsize: 17064
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3895 0 0 0 117998 17 0 0 25 0 1 0 541658678 17747968 3873 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4333 3873 603 41 0 4292 0
vsize: 17332
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3901 0 0 0 118998 17 0 0 25 0 1 0 541658678 17747968 3879 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4333 3879 603 41 0 4292 0
vsize: 17332
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 27794
Raw data (stat): 27737 (minisat+) R 27736 3260 3259 0 -1 0 3912 0 0 0 119998 17 0 0 25 0 1 0 541658678 17887232 3890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4367 3890 603 41 0 4326 0
vsize: 17468
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 27794
Raw data (stat): 27737 (minisat+) Z 27736 3260 3259 0 -1 12 3915 0 0 0 119998 18 0 0 25 0 1 0 541658678 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.02
CPU time (s): 1200.17
CPU user time (s): 1199.99
CPU system time (s): 0.183972
CPU usage (%): 100.013
Max. virtual memory (Kb): 17468
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####