PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8a3.opb
MD5SUM	a430664a9b4f203a5896b33ca2b0e0e5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	191
Optimality of the best value was proved	NO
Number of terms in the objective function	528
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	528
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	528
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02384
Number of variables	528
Total number of constraints	1816
Number of constraints which are clauses	1816
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 6256

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        893764 kB
Buffers:         35532 kB
Cached:          84892 kB
SwapCached:          4 kB
Active:          58128 kB
Inactive:        65156 kB
HighTotal:      131008 kB
HighFree:        42336 kB
LowTotal:       903652 kB
LowFree:        851428 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11996 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:21:16 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4677 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1816 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1816     4536 |     605       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23592     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |   56228   131841 |   18742       3       16     5.3 |  0.000 % |
c |       103 |   55514   130214 |   20616      88      922    10.5 |  1.771 % |
c |       253 |   49980   117499 |   22677     109      923     8.5 | 10.769 % |
c |       479 |   45476   107132 |   24945     220     2037     9.3 | 18.147 % |
c |       816 |   43902   103505 |   27440     534     9582    17.9 | 20.803 % |
c |      1322 |   40404    95411 |   30184     956    16668    17.4 | 26.716 % |
c |      2081 |   39615    93573 |   33202    1691    31369    18.6 | 28.041 % |
c ==============================================================================
c [1mFound solution: 231[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2328 |   38486    90989 |   12828    1909    35987    18.9 | 28.041 % |
c |      2428 |   37326    88311 |   14110    1979    36441    18.4 | 31.920 % |
c |      2578 |   35521    84157 |   15521    2079    37843    18.2 | 35.136 % |
c |      2804 |   33323    79051 |   17074    2249    40039    17.8 | 38.819 % |
c |      3141 |   29754    70796 |   18781    2528    47888    18.9 | 44.899 % |
c ==============================================================================
c [1mFound solution: 227[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3395 |   29463    70156 |    9821    2770    55352    20.0 | 44.899 % |
c |      3495 |   29335    69860 |   10803    2868    56562    19.7 | 45.867 % |
c |      3647 |   26614    63549 |   11883    2933    57002    19.4 | 50.409 % |
c |      3872 |   25799    61658 |   13071    3138    60806    19.4 | 51.806 % |
c |      4209 |   25500    60960 |   14378    3470    70143    20.2 | 52.346 % |
c |      4715 |   25500    60960 |   15816    3976    90085    22.7 | 52.346 % |
c ==============================================================================
c [1mFound solution: 226[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5024 |   24442    58491 |    8147    4257    97981    23.0 | 52.346 % |
c ==============================================================================
c [1mFound solution: 224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5054 |   24183    57897 |    8061    4219    93721    22.2 | 52.346 % |
c |      5156 |   24183    57897 |    8867    4321    95189    22.0 | 54.681 % |
c ==============================================================================
c [1mFound solution: 218[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5260 |   24016    57527 |    8005    4399    93967    21.4 | 54.681 % |
c |      5360 |   24016    57527 |    8805    4499    96179    21.4 | 55.084 % |
c |      5511 |   24016    57527 |    9686    4650    98345    21.1 | 55.084 % |
c |      5736 |   24016    57527 |   10654    4875   101492    20.8 | 55.084 % |
c |      6073 |   23901    57260 |   11720    4835   102129    21.1 | 55.281 % |
c |      6579 |   23875    57200 |   12892    5335   116819    21.9 | 55.324 % |
c |      7338 |   23730    56865 |   14181    6088   164421    27.0 | 55.563 % |
c |      8477 |   23125    55466 |   15599    7201   215166    29.9 | 56.602 % |
c ==============================================================================
c [1mFound solution: 217[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9474 |   23211    55686 |    7737    8198   287253    35.0 | 56.602 % |
c |      9574 |   23211    55686 |    8510    8298   289076    34.8 | 56.543 % |
c |      9724 |   23211    55686 |    9361    8448   291559    34.5 | 56.543 % |
c |      9950 |   23211    55686 |   10297    8674   300396    34.6 | 56.543 % |
c |     10287 |   23211    55686 |   11327    9011   308212    34.2 | 56.543 % |
c |     10794 |   23166    55585 |   12460    9517   319620    33.6 | 56.607 % |
c |     11554 |   23095    55420 |   13706   10268   336196    32.7 | 56.735 % |
c ==============================================================================
c [1mFound solution: 213[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12259 |   23140    55549 |    7713   10961   349586    31.9 | 56.735 % |
c |     12359 |   23140    55549 |    8484   11061   351363    31.8 | 56.779 % |
c |     12509 |   23140    55549 |    9332   11211   355230    31.7 | 56.779 % |
c |     12734 |   23140    55549 |   10266   11436   358897    31.4 | 56.779 % |
c |     13071 |   23140    55549 |   11292   11773   370570    31.5 | 56.779 % |
c ==============================================================================
c [1mFound solution: 212[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13159 |   23030    55275 |    7676   11797   365873    31.0 | 56.779 % |
c ==============================================================================
c [1mFound solution: 211[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13187 |   23085    55418 |    7695   11825   366108    31.0 | 56.779 % |
c |     13290 |   23085    55418 |    8464   11928   372549    31.2 | 56.900 % |
c |     13440 |   23085    55418 |    9310   12078   375517    31.1 | 56.900 % |
c |     13665 |   23085    55418 |   10242   12303   380027    30.9 | 56.900 % |
c |     14004 |   23085    55418 |   11266   12642   386939    30.6 | 56.900 % |
c |     14510 |   23024    55274 |   12392   13143   396878    30.2 | 57.022 % |
c |     15269 |   22973    55157 |   13632   13901   437449    31.5 | 57.107 % |
c |     16409 |   22782    54713 |   14995   14958   494566    33.1 | 57.451 % |
c |     18118 |   22662    54434 |   16494   16651   580250    34.8 | 57.668 % |
c ==============================================================================
c [1mFound solution: 210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18477 |   22619    54309 |    7539   17008   590075    34.7 | 57.668 % |
c |     18578 |   22619    54309 |    8292   17109   593075    34.7 | 57.726 % |
c |     18728 |   22619    54309 |    9122   17259   595130    34.5 | 57.726 % |
c |     18953 |   22619    54309 |   10034   17484   604842    34.6 | 57.726 % |
c |     19290 |   22619    54309 |   11037   17821   612997    34.4 | 57.726 % |
c ==============================================================================
c [1mFound solution: 209[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19515 |   22698    54511 |    7566   18046   623118    34.5 | 57.726 % |
c |     19616 |   22698    54511 |    8322   18147   625843    34.5 | 57.677 % |
c |     19766 |   22698    54511 |    9154   18297   627718    34.3 | 57.677 % |
c |     19991 |   22698    54511 |   10070   18522   639681    34.5 | 57.677 % |
c |     20328 |   22698    54511 |   11077   18859   649647    34.4 | 57.677 % |
c |     20835 |   22678    54463 |   12185   19350   679612    35.1 | 57.719 % |
c |     21595 |   22456    53948 |   13403   20076   693007    34.5 | 58.100 % |
c |     22736 |   22456    53948 |   14743   21217   738423    34.8 | 58.100 % |
c |     24447 |   22456    53948 |   16218   22928   827755    36.1 | 58.100 % |
c |     27011 |   22131    53193 |   17840   25405  1061632    41.8 | 58.666 % |
c |     30856 |   22131    53193 |   19624   29250  1188395    40.6 | 58.666 % |
c |     36625 |   22131    53193 |   21586   18903   943048    49.9 | 58.666 % |
c |     45274 |   22131    53193 |   23745   27552  1782537    64.7 | 58.666 % |
c |     58249 |   22127    53184 |   26119   20597  1176301    57.1 | 58.672 % |
c ==============================================================================
c [1mFound solution: 208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70744 |   22008    52893 |    7336   33088  2117295    64.0 | 58.672 % |
c |     70844 |   21878    52591 |    8069   16322   908951    55.7 | 59.083 % |
c |     70994 |   21878    52591 |    8876   16472   921063    55.9 | 59.083 % |
c |     71219 |   21878    52591 |    9764   16697   925461    55.4 | 59.083 % |
c ==============================================================================
c [1mFound solution: 204[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71465 |   21848    52519 |    7282   16612   884298    53.2 | 59.083 % |
c |     71565 |   21848    52519 |    8010   16712   885494    53.0 | 59.205 % |
c |     71715 |   21848    52519 |    8811   16862   892311    52.9 | 59.205 % |
c |     71942 |   21848    52519 |    9692   17089   906721    53.1 | 59.205 % |
c |     72279 |   21848    52519 |   10661   17426   929272    53.3 | 59.205 % |
c |     72787 |   21848    52519 |   11727   17934   941044    52.5 | 59.205 % |
c |     73546 |   21848    52519 |   12900   18693   965102    51.6 | 59.205 % |
c |     74685 |   21848    52519 |   14190   19832  1020034    51.4 | 59.205 % |
c |     76395 |   21848    52519 |   15609   21542  1103328    51.2 | 59.205 % |
c |     78957 |   21848    52519 |   17170   24104  1244992    51.7 | 59.205 % |
c |     82801 |   21848    52519 |   18887   27948  1478428    52.9 | 59.205 % |
c ==============================================================================
c [1mFound solution: 203[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     85555 |   21896    52642 |    7298   30702  1666743    54.3 | 59.205 % |
c |     85655 |   21896    52642 |    8027   15451   669234    43.3 | 59.171 % |
c |     85805 |   21896    52642 |    8830   15601   674109    43.2 | 59.171 % |
c |     86030 |   21864    52568 |    9713   15724   680912    43.3 | 59.223 % |
c |     86367 |   21773    52358 |   10685   16054   688189    42.9 | 59.371 % |
c |     86873 |   21773    52358 |   11753   16560   736397    44.5 | 59.371 % |
c |     87632 |   21773    52358 |   12928   17319   750686    43.3 | 59.371 % |
c ==============================================================================
c [1mFound solution: 202[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88520 |   21734    52251 |    7244   18204   788395    43.3 | 59.371 % |
c |     88620 |   21734    52251 |    7968   18304   791073    43.2 | 59.428 % |
c |     88770 |   21734    52251 |    8765   18454   797467    43.2 | 59.428 % |
c |     88995 |   21734    52251 |    9641   18679   801527    42.9 | 59.428 % |
c |     89332 |   21734    52251 |   10605   19016   825438    43.4 | 59.428 % |
c |     89838 |   21734    52251 |   11666   19522   847607    43.4 | 59.428 % |
c |     90597 |   21734    52251 |   12833   20281   881575    43.5 | 59.428 % |
c |     91736 |   21734    52251 |   14116   21420   958217    44.7 | 59.428 % |
c |     93445 |   21734    52251 |   15528   23129  1019199    44.1 | 59.428 % |
c |     96007 |   21734    52251 |   17080   25691  1212603    47.2 | 59.428 % |
c |     99851 |   21707    52189 |   18789   15028   587715    39.1 | 59.476 % |
c |    105617 |   21640    52033 |   20667   20793   956938    46.0 | 59.597 % |
c |    114268 |   21609    51962 |   22734   29434  1463062    49.7 | 59.650 % |
c |    127242 |   21567    51864 |   25008   24411  1233777    50.5 | 59.724 % |
c ==============================================================================
c [1mFound solution: 201[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127693 |   21620    51998 |    7206   24862  1254682    50.5 | 59.724 % |
c |    127793 |   21620    51998 |    7926   12531   543904    43.4 | 59.706 % |
c |    127944 |   21620    51998 |    8719   12682   550651    43.4 | 59.706 % |
c |    128169 |   21620    51998 |    9591   12907   554792    43.0 | 59.706 % |
c |    128506 |   21620    51998 |   10550   13244   568075    42.9 | 59.706 % |
c |    129015 |   21620    51998 |   11605   13753   586330    42.6 | 59.706 % |
c |    129774 |   21620    51998 |   12765   14512   606594    41.8 | 59.706 % |
c |    130913 |   21620    51998 |   14042   15651   639850    40.9 | 59.706 % |
c |    132621 |   21606    51963 |   15446   17358   721338    41.6 | 59.743 % |
c |    135184 |   21494    51696 |   16991   19917   854976    42.9 | 59.917 % |
c |    139028 |   21494    51696 |   18690   23761  1109674    46.7 | 59.917 % |
c |    144794 |   21494    51696 |   20559   29527  1463785    49.6 | 59.917 % |
c |    153444 |   21494    51696 |   22615   21974  1104209    50.3 | 59.917 % |
c |    166418 |   21306    51255 |   24877   34946  1908802    54.6 | 60.196 % |
c |    185880 |   21302    51246 |   27364   32700  1640902    50.2 | 60.201 % |
c |    215072 |   21302    51246 |   30101   37988  2218220    58.4 | 60.201 % |
c ==============================================================================
c [1mFound solution: 200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    216866 |   21215    51025 |    7071   39768  2353567    59.2 | 60.201 % |
c |    216966 |   21215    51025 |    7778   17845   854162    47.9 | 60.342 % |
c |    217117 |   21215    51025 |    8555   17996   856676    47.6 | 60.342 % |
c |    217342 |   21198    50984 |    9411   18220   860988    47.3 | 60.385 % |
c |    217680 |   21198    50984 |   10352   18558   876813    47.2 | 60.385 % |
c |    218186 |   21198    50984 |   11387   19064   921921    48.4 | 60.385 % |
c |    218945 |   21198    50984 |   12526   19823   934362    47.1 | 60.385 % |
c |    220084 |   21198    50984 |   13779   20962  1030586    49.2 | 60.385 % |
c |    221793 |   21198    50984 |   15157   22671  1135056    50.1 | 60.385 % |
c |    224356 |   21198    50984 |   16673   25234  1296318    51.4 | 60.385 % |
c |    228200 |   21198    50984 |   18340   29078  1538723    52.9 | 60.385 % |
c |    233967 |   21198    50984 |   20174   19609   984970    50.2 | 60.385 % |
c |    242616 |   21198    50984 |   22191   28258  1546896    54.7 | 60.385 % |
c |    255590 |   21198    50984 |   24411   23400  1137223    48.6 | 60.385 % |
c |    275051 |   21198    50984 |   26852   21157   943829    44.6 | 60.385 % |
c |    304243 |   21198    50984 |   29537   26694  1668834    62.5 | 60.385 % |
c |    348032 |   21198    50984 |   32491   18958   966144    51.0 | 60.385 % |
c |    413716 |   21198    50984 |   35740   29494  1429243    48.5 | 60.385 % |
#### 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.97 0.98 0.92 2/54 26478
Raw data (stat): 26478 (runsolver) R 26477 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423329694 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 2082 0 0 0 992 6 0 0 25 0 1 0 423329694 10694656 1993 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2611 1993 603 41 0 2570 0
vsize: 10444
[startup+20.0017 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 2323 0 0 0 1991 7 0 0 25 0 1 0 423329694 11755520 2234 4294967295 134512640 134672761 3221224576 3221223712 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2870 2234 603 41 0 2829 0
vsize: 11480
[startup+30.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 2553 0 0 0 2989 8 0 0 25 0 1 0 423329694 12693504 2464 4294967295 134512640 134672761 3221224576 3221223744 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3099 2464 603 41 0 3058 0
vsize: 12396
[startup+40.0025 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 2815 0 0 0 3988 9 0 0 25 0 1 0 423329694 13750272 2726 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3357 2726 603 41 0 3316 0
vsize: 13428
[startup+50.0028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 3111 0 0 0 4987 10 0 0 25 0 1 0 423329694 14958592 3022 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3652 3022 603 41 0 3611 0
vsize: 14608
[startup+60.0028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 3383 0 0 0 5986 11 0 0 25 0 1 0 423329694 16023552 3294 4294967295 134512640 134672761 3221224576 3221223712 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3912 3294 603 41 0 3871 0
vsize: 15648
[startup+70.0035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 3570 0 0 0 6985 12 0 0 25 0 1 0 423329694 16830464 3481 4294967295 134512640 134672761 3221224576 3221223680 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4109 3481 603 41 0 4068 0
vsize: 16436
[startup+80.0039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 3570 0 0 0 7985 12 0 0 25 0 1 0 423329694 16830464 3481 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4109 3481 603 41 0 4068 0
vsize: 16436
[startup+90.0039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 3816 0 0 0 8984 13 0 0 25 0 1 0 423329694 17752064 3727 4294967295 134512640 134672761 3221224576 3221223632 134565140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4334 3727 603 41 0 4293 0
vsize: 17336
[startup+100.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4132 0 0 0 9983 14 0 0 25 0 1 0 423329694 19075072 4043 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4657 4043 603 41 0 4616 0
vsize: 18628
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4401 0 0 0 10982 15 0 0 25 0 1 0 423329694 20271104 4312 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4312 603 41 0 4908 0
vsize: 19796
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4646 0 0 0 11982 16 0 0 25 0 1 0 423329694 21323776 4557 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4557 603 41 0 5165 0
vsize: 20824
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4803 0 0 0 12981 17 0 0 25 0 1 0 423329694 21987328 4714 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4714 603 41 0 5327 0
vsize: 21472
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4803 0 0 0 13981 17 0 0 25 0 1 0 423329694 21987328 4714 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4714 603 41 0 5327 0
vsize: 21472
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4803 0 0 0 14981 17 0 0 25 0 1 0 423329694 21987328 4714 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4714 603 41 0 5327 0
vsize: 21472
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4803 0 0 0 15982 17 0 0 25 0 1 0 423329694 21987328 4714 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4714 603 41 0 5327 0
vsize: 21472
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4803 0 0 0 16982 17 0 0 25 0 1 0 423329694 21987328 4714 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4714 603 41 0 5327 0
vsize: 21472
[startup+180.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4803 0 0 0 17982 17 0 0 25 0 1 0 423329694 21987328 4714 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4714 603 41 0 5327 0
vsize: 21472
[startup+190.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4803 0 0 0 18982 17 0 0 25 0 1 0 423329694 21987328 4714 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4714 603 41 0 5327 0
vsize: 21472
[startup+200.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4803 0 0 0 19982 17 0 0 25 0 1 0 423329694 21987328 4714 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4714 603 41 0 5327 0
vsize: 21472
[startup+210.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4803 0 0 0 20983 17 0 0 25 0 1 0 423329694 21987328 4714 4294967295 134512640 134672761 3221224576 3221223712 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4714 603 41 0 5327 0
vsize: 21472
[startup+220.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 21983 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223760 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+230.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 22983 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+240.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 23983 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+250.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 24983 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+260.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 25984 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+270.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26480
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 26984 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223532 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+280.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 27984 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+290.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 28984 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+300.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 29984 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+310.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 30984 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+320.011 s]
Raw data (loadavg): 1.31 1.05 0.94 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 31985 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+330.011 s]
Raw data (loadavg): 1.34 1.06 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 32985 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+340.012 s]
Raw data (loadavg): 1.29 1.06 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 33985 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+350.011 s]
Raw data (loadavg): 1.24 1.06 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 34985 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+360.012 s]
Raw data (loadavg): 1.20 1.06 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 35985 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+370.013 s]
Raw data (loadavg): 1.17 1.05 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 36985 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+380.012 s]
Raw data (loadavg): 1.15 1.05 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 37985 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223760 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+390.012 s]
Raw data (loadavg): 1.12 1.05 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 38986 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+400.013 s]
Raw data (loadavg): 1.10 1.05 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 39986 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+410.013 s]
Raw data (loadavg): 1.09 1.05 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 40986 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+420.013 s]
Raw data (loadavg): 1.07 1.04 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 41986 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+430.014 s]
Raw data (loadavg): 1.06 1.04 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4805 0 0 0 42986 17 0 0 25 0 1 0 423329694 21987328 4716 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4716 603 41 0 5327 0
vsize: 21472
[startup+440.014 s]
Raw data (loadavg): 1.05 1.04 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4848 0 0 0 43987 17 0 0 25 0 1 0 423329694 22118400 4759 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4759 603 41 0 5359 0
vsize: 21600
[startup+450.014 s]
Raw data (loadavg): 1.04 1.04 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4848 0 0 0 44987 17 0 0 25 0 1 0 423329694 22118400 4759 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4759 603 41 0 5359 0
vsize: 21600
[startup+460.015 s]
Raw data (loadavg): 1.04 1.04 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4848 0 0 0 45987 17 0 0 25 0 1 0 423329694 22118400 4759 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4759 603 41 0 5359 0
vsize: 21600
[startup+470.015 s]
Raw data (loadavg): 1.03 1.03 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4855 0 0 0 46987 17 0 0 25 0 1 0 423329694 22253568 4766 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5433 4766 603 41 0 5392 0
vsize: 21732
[startup+480.016 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4862 0 0 0 47987 17 0 0 25 0 1 0 423329694 22253568 4773 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5433 4773 603 41 0 5392 0
vsize: 21732
[startup+490.016 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 4872 0 0 0 48988 17 0 0 25 0 1 0 423329694 22253568 4783 4294967295 134512640 134672761 3221224576 3221223680 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5433 4783 603 41 0 5392 0
vsize: 21732
[startup+500.016 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5019 0 0 0 49987 18 0 0 25 0 1 0 423329694 22913024 4930 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5594 4930 603 41 0 5553 0
vsize: 22376
[startup+510.016 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5027 0 0 0 50987 18 0 0 25 0 1 0 423329694 22913024 4938 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5594 4938 603 41 0 5553 0
vsize: 22376
[startup+520.016 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5027 0 0 0 51988 18 0 0 25 0 1 0 423329694 22913024 4938 4294967295 134512640 134672761 3221224576 3221223712 134560645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5594 4938 603 41 0 5553 0
vsize: 22376
[startup+530.015 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5027 0 0 0 52988 18 0 0 25 0 1 0 423329694 22913024 4938 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5594 4938 603 41 0 5553 0
vsize: 22376
[startup+540.017 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5027 0 0 0 53988 18 0 0 25 0 1 0 423329694 22913024 4938 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5594 4938 603 41 0 5553 0
vsize: 22376
[startup+550.017 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5027 0 0 0 54988 18 0 0 25 0 1 0 423329694 22913024 4938 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5594 4938 603 41 0 5553 0
vsize: 22376
[startup+560.018 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5063 0 0 0 55988 18 0 0 25 0 1 0 423329694 23044096 4974 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5626 4974 603 41 0 5585 0
vsize: 22504
[startup+570.019 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 56988 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+580.019 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 57987 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+590.019 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 58987 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+600.019 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 59987 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223680 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+610.02 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 60987 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223680 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+620.021 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 61987 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+630.021 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 62988 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+640.021 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 63988 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+650.021 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 64988 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+660.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 65988 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+670.023 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 66988 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+680.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 67989 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223680 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+690.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 68989 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223776 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+700.023 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 69989 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+710.023 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 70989 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+720.023 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 71989 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223680 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+730.024 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 72990 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+740.024 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 73990 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+750.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 74990 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+760.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 75990 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223680 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+770.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5254 0 0 0 76990 19 0 0 25 0 1 0 423329694 23830528 5165 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5165 603 41 0 5777 0
vsize: 23272
[startup+780.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5296 0 0 0 77990 19 0 0 25 0 1 0 423329694 23965696 5207 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5851 5207 603 41 0 5810 0
vsize: 23404
[startup+790.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5299 0 0 0 78991 19 0 0 25 0 1 0 423329694 23965696 5210 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5851 5210 603 41 0 5810 0
vsize: 23404
[startup+800.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5306 0 0 0 79991 19 0 0 25 0 1 0 423329694 24100864 5217 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5884 5217 603 41 0 5843 0
vsize: 23536
[startup+810.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5310 0 0 0 80991 20 0 0 25 0 1 0 423329694 24100864 5221 4294967295 134512640 134672761 3221224576 3221223680 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5884 5221 603 41 0 5843 0
vsize: 23536
[startup+820.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5316 0 0 0 81991 20 0 0 25 0 1 0 423329694 24100864 5227 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5884 5227 603 41 0 5843 0
vsize: 23536
[startup+830.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5320 0 0 0 82991 20 0 0 25 0 1 0 423329694 24100864 5231 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5884 5231 603 41 0 5843 0
vsize: 23536
[startup+840.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5423 0 0 0 83991 20 0 0 25 0 1 0 423329694 24498176 5334 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5981 5334 603 41 0 5940 0
vsize: 23924
[startup+850.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5640 0 0 0 84991 21 0 0 25 0 1 0 423329694 25427968 5551 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6208 5551 603 41 0 6167 0
vsize: 24832
[startup+860.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5812 0 0 0 85990 21 0 0 25 0 1 0 423329694 26099712 5723 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6372 5723 603 41 0 6331 0
vsize: 25488
[startup+870.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5812 0 0 0 86990 21 0 0 25 0 1 0 423329694 26099712 5723 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6372 5723 603 41 0 6331 0
vsize: 25488
[startup+880.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5818 0 0 0 87991 21 0 0 25 0 1 0 423329694 26099712 5729 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6372 5729 603 41 0 6331 0
vsize: 25488
[startup+890.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5818 0 0 0 88991 21 0 0 25 0 1 0 423329694 26099712 5729 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6372 5729 603 41 0 6331 0
vsize: 25488
[startup+900.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5818 0 0 0 89991 21 0 0 25 0 1 0 423329694 26099712 5729 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6372 5729 603 41 0 6331 0
vsize: 25488
[startup+910.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5824 0 0 0 90991 21 0 0 25 0 1 0 423329694 26099712 5735 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6372 5735 603 41 0 6331 0
vsize: 25488
[startup+920.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5824 0 0 0 91991 21 0 0 25 0 1 0 423329694 26099712 5735 4294967295 134512640 134672761 3221224576 3221223680 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6372 5735 603 41 0 6331 0
vsize: 25488
[startup+930.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5825 0 0 0 92992 21 0 0 25 0 1 0 423329694 26099712 5736 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6372 5736 603 41 0 6331 0
vsize: 25488
[startup+940.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5841 0 0 0 93992 21 0 0 25 0 1 0 423329694 26230784 5752 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6404 5752 603 41 0 6363 0
vsize: 25616
[startup+950.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5860 0 0 0 94991 21 0 0 25 0 1 0 423329694 26365952 5771 4294967295 134512640 134672761 3221224576 3221223776 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6437 5771 603 41 0 6396 0
vsize: 25748
[startup+960.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5860 0 0 0 95991 22 0 0 25 0 1 0 423329694 26365952 5771 4294967295 134512640 134672761 3221224576 3221223776 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6437 5771 603 41 0 6396 0
vsize: 25748
[startup+970.032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5860 0 0 0 96991 22 0 0 25 0 1 0 423329694 26365952 5771 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6437 5771 603 41 0 6396 0
vsize: 25748
[startup+980.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5860 0 0 0 97992 22 0 0 25 0 1 0 423329694 26365952 5771 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6437 5771 603 41 0 6396 0
vsize: 25748
[startup+990.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5860 0 0 0 98992 22 0 0 25 0 1 0 423329694 26365952 5771 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6437 5771 603 41 0 6396 0
vsize: 25748
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5860 0 0 0 99992 22 0 0 25 0 1 0 423329694 26365952 5771 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6437 5771 603 41 0 6396 0
vsize: 25748
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5860 0 0 0 100992 22 0 0 25 0 1 0 423329694 26365952 5771 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6437 5771 603 41 0 6396 0
vsize: 25748
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 5864 0 0 0 101992 22 0 0 25 0 1 0 423329694 26365952 5775 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6437 5775 603 41 0 6396 0
vsize: 25748
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6064 0 0 0 102992 22 0 0 25 0 1 0 423329694 27164672 5975 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6632 5975 603 41 0 6591 0
vsize: 26528
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6148 0 0 0 103992 22 0 0 25 0 1 0 423329694 27426816 6059 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6696 6059 603 41 0 6655 0
vsize: 26784
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6148 0 0 0 104992 22 0 0 25 0 1 0 423329694 27426816 6059 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6696 6059 603 41 0 6655 0
vsize: 26784
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6157 0 0 0 105993 22 0 0 25 0 1 0 423329694 27561984 6068 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6729 6068 603 41 0 6688 0
vsize: 26916
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6164 0 0 0 106993 22 0 0 25 0 1 0 423329694 27561984 6075 4294967295 134512640 134672761 3221224576 3221223744 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6729 6075 603 41 0 6688 0
vsize: 26916
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6168 0 0 0 107993 22 0 0 25 0 1 0 423329694 27561984 6079 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6729 6079 603 41 0 6688 0
vsize: 26916
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6184 0 0 0 108993 22 0 0 25 0 1 0 423329694 27725824 6095 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6769 6095 603 41 0 6728 0
vsize: 27076
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6197 0 0 0 109993 22 0 0 25 0 1 0 423329694 27725824 6108 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6769 6108 603 41 0 6728 0
vsize: 27076
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6216 0 0 0 110994 22 0 0 25 0 1 0 423329694 27889664 6127 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6809 6127 603 41 0 6768 0
vsize: 27236
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6227 0 0 0 111994 22 0 0 25 0 1 0 423329694 27889664 6138 4294967295 134512640 134672761 3221224576 3221223680 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6809 6138 603 41 0 6768 0
vsize: 27236
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6243 0 0 0 112994 23 0 0 25 0 1 0 423329694 28053504 6154 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6154 603 41 0 6808 0
vsize: 27396
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6258 0 0 0 113994 23 0 0 25 0 1 0 423329694 28053504 6169 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6169 603 41 0 6808 0
vsize: 27396
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6260 0 0 0 114994 23 0 0 25 0 1 0 423329694 28053504 6171 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6260 0 0 0 115994 23 0 0 25 0 1 0 423329694 28053504 6171 4294967295 134512640 134672761 3221224576 3221223680 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6260 0 0 0 116994 23 0 0 25 0 1 0 423329694 28053504 6171 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6260 0 0 0 117994 23 0 0 25 0 1 0 423329694 28053504 6171 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6260 0 0 0 118994 23 0 0 25 0 1 0 423329694 28053504 6171 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 26482
Raw data (stat): 26478 (minisat+) R 26477 20937 20936 0 -1 0 6260 0 0 0 119994 23 0 0 25 0 1 0 423329694 28053504 6171 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6171 603 41 0 6808 0
vsize: 27396
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 26482
Raw data (stat): 26478 (minisat+) Z 26477 20937 20936 0 -1 12 6263 0 0 0 119995 24 0 0 25 0 1 0 423329694 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.06
CPU time (s): 1200.2
CPU user time (s): 1199.95
CPU system time (s): 0.245962
CPU usage (%): 100.012
Max. virtual memory (Kb): 27396
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####