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/miplib/normalized-mps-v2-13-7-p0291.opb
MD5SUM	1d9168a9335e29df835d07b0bdf2adea
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10447498
Optimality of the best value was proved	NO
Number of terms in the objective function	289
Biggest coefficient in the objective function	80000000
Number of bits for the biggest coefficient in the objective function	27
Sum of the numbers in the objective function	686518451
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	80000000
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	686518451
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.333948
Number of variables	291
Total number of constraints	543
Number of constraints which are clauses	189
Number of constraints which are cardinality constraints (but not clauses)	295
Number of constraints which are nor clauses,nor cardinality constraints	59
Minimum length of a constraint	1
Maximum length of a constraint	53
Trace number 19020

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        846704 kB
Buffers:          8828 kB
Cached:         152576 kB
SwapCached:         28 kB
Active:          49820 kB
Inactive:       114448 kB
HighTotal:      131008 kB
HighFree:        15008 kB
LowTotal:       903652 kB
LowFree:        831696 kB
SwapTotal:     2097892 kB
SwapFree:      2097796 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            18148 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:49:26 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 17147 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 205 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................sssss
c ---[ 144]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[  14]---> Sorter-cost: 1503     Base: 2 2 5 2 3
c ---[  13]---> Sorter-cost: 1241     Base: 2 2 5 2 3
c ---[  11]---> BDD-cost:   52
c ---[  10]---> BDD-cost:   52
c ---[   9]---> BDD-cost:   52
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:    8
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   28
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   86
c ---[   2]---> Sorter-cost:  749     Base: 2 5 2 2
c ---[   1]---> Sorter-cost:  880     Base: 2 2 5 3
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11271    26846 |    3757       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 160963526[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:118482     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         8 |  356963   835866 |  118987       7       39     5.6 |  0.000 % |
c |       108 |  356956   835851 |  130885     106     2431    22.9 |  0.024 % |
c |       258 |  356956   835851 |  143974     256     3715    14.5 |  0.024 % |
c |       484 |  356956   835851 |  158371     482     5549    11.5 |  0.024 % |
c |       822 |  356956   835851 |  174208     820     8532    10.4 |  0.024 % |
c |      1329 |  356941   835818 |  191629    1326    13300    10.0 |  0.027 % |
c |      2090 |  356857   835631 |  210792    2083    26782    12.9 |  0.046 % |
c |      3231 |  356857   835631 |  231872    3224    82835    25.7 |  0.046 % |
c |      4941 |  356552   834948 |  255059    4927   112930    22.9 |  0.113 % |
c ==============================================================================
c [1mFound solution: 118952803[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   23     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6131 |  358296   839637 |  119432    6113   141375    23.1 |  0.113 % |
c |      6231 |  358296   839637 |  131375    6213   142715    23.0 |  0.164 % |
c |      6381 |  358296   839637 |  144512    6363   151312    23.8 |  0.164 % |
c |      6606 |  358296   839637 |  158963    6588   157024    23.8 |  0.164 % |
c ==============================================================================
c [1mFound solution: 118814390[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   22     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6662 |  359024   841543 |  119674    6637   159413    24.0 |  0.164 % |
c ==============================================================================
c [1mFound solution: 114022192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6743 |  358970   841447 |  119656    6707   161204    24.0 |  0.164 % |
c |      6844 |  358963   841432 |  131621    6807   167695    24.6 |  0.242 % |
c ==============================================================================
c [1mFound solution: 104115770[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6975 |  359177   841952 |  119725    6938   172621    24.9 |  0.242 % |
c |      7075 |  359177   841952 |  131697    7038   174869    24.8 |  0.242 % |
c |      7225 |  359166   841928 |  144867    7187   176150    24.5 |  0.245 % |
c |      7450 |  358833   841174 |  159353    7408   177671    24.0 |  0.320 % |
c |      7788 |  358833   841174 |  175289    7746   181482    23.4 |  0.320 % |
c |      8297 |  358833   841174 |  192818    8255   197847    24.0 |  0.320 % |
c |      9057 |  358833   841174 |  212100    9015   231628    25.7 |  0.320 % |
c |     10196 |  358519   840458 |  233310   10150   274795    27.1 |  0.394 % |
c ==============================================================================
c [1mFound solution: 103894941[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   22     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11225 |  358601   840684 |  119533   11179   316767    28.3 |  0.394 % |
c |     11328 |  358601   840684 |  131486   11282   327789    29.1 |  0.394 % |
c |     11478 |  358470   840389 |  144634   11429   329959    28.9 |  0.421 % |
c |     11703 |  358470   840389 |  159098   11654   346815    29.8 |  0.421 % |
c |     12042 |  358423   840284 |  175008   11990   350509    29.2 |  0.431 % |
c ==============================================================================
c [1mFound solution: 103270240[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12469 |  358614   840779 |  119538   12359   387924    31.4 |  0.431 % |
c |     12569 |  358614   840779 |  131491   12459   389236    31.2 |  0.463 % |
c |     12720 |  358581   840704 |  144640   12609   390327    31.0 |  0.471 % |
c |     12946 |  358581   840704 |  159105   12835   391879    30.5 |  0.471 % |
c |     13285 |  358581   840704 |  175015   13174   398984    30.3 |  0.471 % |
c |     13791 |  358457   840424 |  192517   13671   405790    29.7 |  0.500 % |
c |     14553 |  358418   840336 |  211768   14432   431113    29.9 |  0.509 % |
c |     15692 |  358320   840117 |  232945   15567   447980    28.8 |  0.530 % |
c ==============================================================================
c [1mFound solution: 103270025[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   23     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16574 |  358367   840282 |  119455   16444   463985    28.2 |  0.530 % |
c |     16675 |  358367   840282 |  131400   16545   465001    28.1 |  0.548 % |
c |     16825 |  358367   840282 |  144540   16695   495310    29.7 |  0.548 % |
c |     17050 |  358367   840282 |  158994   16920   498450    29.5 |  0.548 % |
c |     17387 |  358089   839656 |  174894   17255   500675    29.0 |  0.609 % |
c ==============================================================================
c [1mFound solution: 103209779[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17860 |  358178   839891 |  119392   17728   505821    28.5 |  0.609 % |
c |     17960 |  358178   839891 |  131331   17828   506451    28.4 |  0.610 % |
c ==============================================================================
c [1mFound solution: 102506300[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18073 |  358214   839983 |  119404   17941   508901    28.4 |  0.610 % |
c ==============================================================================
c [1mFound solution: 102224061[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18165 |  358260   840097 |  119420   18033   514182    28.5 |  0.610 % |
c |     18265 |  358260   840097 |  131362   18133   515968    28.5 |  0.611 % |
c |     18415 |  358260   840097 |  144498   18283   526879    28.8 |  0.611 % |
c |     18640 |  358032   839582 |  158948   18499   530080    28.7 |  0.663 % |
c |     18978 |  357689   838798 |  174842   18830   533078    28.3 |  0.748 % |
c |     19485 |  357689   838798 |  192327   19337   543967    28.1 |  0.748 % |
c |     20247 |  357579   838546 |  211559   20095   554914    27.6 |  0.775 % |
c ==============================================================================
c [1mFound solution: 101392970[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20842 |  357166   837606 |  119055   20657   600327    29.1 |  0.775 % |
c |     20942 |  357166   837606 |  130960   20757   604926    29.1 |  0.888 % |
c |     21092 |  357099   837455 |  144056   20905   605720    29.0 |  0.903 % |
c |     21318 |  357099   837455 |  158462   21131   610735    28.9 |  0.903 % |
c |     21655 |  357000   837230 |  174308   21459   613269    28.6 |  0.926 % |
c |     22163 |  356996   837221 |  191739   21966   625727    28.5 |  0.926 % |
c |     22924 |  356996   837221 |  210913   22727   678511    29.9 |  0.926 % |
c |     24063 |  356927   837064 |  232004   23856   710613    29.8 |  0.943 % |
c |     25772 |  356927   837064 |  255204   25565   837250    32.7 |  0.943 % |
c ==============================================================================
c [1mFound solution: 101209457[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26629 |  356906   837027 |  118968   26419   903304    34.2 |  0.943 % |
c |     26730 |  356906   837027 |  130864   26520   903891    34.1 |  0.961 % |
c |     26880 |  356906   837027 |  143951   26670   904828    33.9 |  0.961 % |
c |     27105 |  356906   837027 |  158346   26895   907211    33.7 |  0.961 % |
c |     27442 |  356817   836824 |  174181   27226   910172    33.4 |  0.983 % |
c ==============================================================================
c [1mFound solution: 91878024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27886 |  356812   836822 |  118937   27668   917057    33.1 |  0.983 % |
c |     27988 |  356812   836822 |  130830   27770   917800    33.1 |  0.994 % |
c |     28139 |  356765   836716 |  143913   27920   918595    32.9 |  1.005 % |
c |     28364 |  356734   836647 |  158305   28142   920650    32.7 |  1.012 % |
c |     28702 |  356730   836638 |  174135   28479   931889    32.7 |  1.013 % |
c ==============================================================================
c [1mFound solution: 81766179[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29167 |  356674   836522 |  118891   28941   952174    32.9 |  1.013 % |
c |     29270 |  356674   836522 |  130780   29044   956347    32.9 |  1.035 % |
c |     29420 |  356674   836522 |  143858   29194   959919    32.9 |  1.035 % |
c ==============================================================================
c [1mFound solution: 81765994[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29478 |  356706   836606 |  118902   29252   961145    32.9 |  1.035 % |
c |     29578 |  356368   835829 |  130792   29333   963197    32.8 |  1.119 % |
c |     29728 |  356368   835829 |  143871   29483   970008    32.9 |  1.119 % |
c |     29953 |  356368   835829 |  158258   29708   979702    33.0 |  1.119 % |
c |     30291 |  356368   835829 |  174084   30046   987186    32.9 |  1.119 % |
c ==============================================================================
c [1mFound solution: 81765987[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30782 |  356083   835189 |  118694   30530  1000135    32.8 |  1.119 % |
c |     30882 |  356083   835189 |  130563   30630  1006518    32.9 |  1.195 % |
c |     31032 |  356083   835189 |  143619   30780  1007510    32.7 |  1.195 % |
c |     31257 |  355449   833743 |  157981   30984  1008809    32.6 |  1.336 % |
c |     31594 |  355354   833523 |  173779   31312  1022563    32.7 |  1.362 % |
c |     32100 |  355227   833233 |  191157   31807  1041189    32.7 |  1.394 % |
c ==============================================================================
c [1mFound solution: 78048625[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:80414     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32531 |  584812  1371002 |  194937   32196  1048887    32.6 |  1.394 % |
c |     32631 |  584812  1371002 |  214430   32296  1052236    32.6 |  1.188 % |
c |     32782 |  584371  1370009 |  235873   32357  1045968    32.3 |  1.253 % |
c |     33007 |  584371  1370009 |  259461   32582  1047782    32.2 |  1.253 % |
c |     33345 |  584371  1370009 |  285407   32920  1052900    32.0 |  1.253 % |
c |     33851 |  583844  1368828 |  313947   33418  1063008    31.8 |  1.326 % |
c ==============================================================================
c [1mFound solution: 78006987[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34192 |  585022  1371938 |  195007   33759  1078902    32.0 |  1.326 % |
c |     34292 |  585022  1371938 |  214507   33859  1081517    31.9 |  1.327 % |
c ==============================================================================
c [1mFound solution: 77996383[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34345 |  585148  1372288 |  195049   33912  1083510    32.0 |  1.327 % |
c |     34446 |  585148  1372288 |  214553   34013  1085853    31.9 |  1.328 % |
c |     34596 |  585148  1372288 |  236009   34163  1094197    32.0 |  1.328 % |
c |     34821 |  585027  1372018 |  259610   34387  1115333    32.4 |  1.345 % |
c |     35158 |  585027  1372018 |  285571   34724  1141357    32.9 |  1.345 % |
c ==============================================================================
c [1mFound solution: 77992506[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35348 |  584533  1370900 |  194844   34869  1148248    32.9 |  1.345 % |
c |     35448 |  584533  1370900 |  214328   34969  1148843    32.9 |  1.427 % |
c |     35598 |  584533  1370900 |  235761   35119  1150077    32.7 |  1.427 % |
c |     35823 |  584488  1370797 |  259337   35335  1152635    32.6 |  1.434 % |
c |     36161 |  584046  1369776 |  285271   35642  1161312    32.6 |  1.505 % |
c |     36669 |  583746  1369086 |  313798   36143  1164468    32.2 |  1.550 % |
c |     37428 |  583242  1367938 |  345178   36890  1187644    32.2 |  1.623 % |
c |     38567 |  583242  1367938 |  379695   38029  1271615    33.4 |  1.623 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 22948
Raw data (stat): 22948 (runsolver) R 22947 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546884144 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0002 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 903 0 0 0 997 1 0 0 25 0 1 0 546884144 4780032 756 4294967295 134512640 134672761 3221224544 3221222528 134597212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1167 756 603 41 0 1126 0
vsize: 4668
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 903 0 0 0 1997 1 0 0 25 0 1 0 546884144 4780032 756 4294967295 134512640 134672761 3221224544 3221222240 134597012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1167 756 603 41 0 1126 0
vsize: 4668
[startup+30.001 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 903 0 0 0 2997 2 0 0 25 0 1 0 546884144 4780032 756 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1167 756 603 41 0 1126 0
vsize: 4668
[startup+40.0005 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 903 0 0 0 3997 2 0 0 25 0 1 0 546884144 4780032 756 4294967295 134512640 134672761 3221224544 3221222240 134597191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1167 756 603 41 0 1126 0
vsize: 4668
[startup+50.002 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10125 0 0 0 4975 24 0 0 25 0 1 0 546884144 42811392 9664 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10452 9664 603 41 0 10411 0
vsize: 41808
[startup+60.0028 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10237 0 0 0 5974 25 0 0 25 0 1 0 546884144 43220992 9776 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10552 9776 603 41 0 10511 0
vsize: 42208
[startup+70.003 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10669 0 0 0 6973 26 0 0 25 0 1 0 546884144 44384256 10083 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10836 10083 603 41 0 10795 0
vsize: 43344
[startup+80.0041 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10669 0 0 0 7973 26 0 0 25 0 1 0 546884144 44384256 10083 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10836 10083 603 41 0 10795 0
vsize: 43344
[startup+90.0038 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10669 0 0 0 8973 26 0 0 25 0 1 0 546884144 44384256 10083 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10836 10083 603 41 0 10795 0
vsize: 43344
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10669 0 0 0 9973 26 0 0 25 0 1 0 546884144 44384256 10083 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10836 10083 603 41 0 10795 0
vsize: 43344
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10669 0 0 0 10973 26 0 0 25 0 1 0 546884144 44384256 10083 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10836 10083 603 41 0 10795 0
vsize: 43344
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10846 0 0 0 11973 27 0 0 25 0 1 0 546884144 44638208 10131 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10898 10131 603 41 0 10857 0
vsize: 43592
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10846 0 0 0 12972 27 0 0 25 0 1 0 546884144 44638208 10131 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10898 10131 603 41 0 10857 0
vsize: 43592
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10846 0 0 0 13972 27 0 0 25 0 1 0 546884144 44638208 10131 4294967295 134512640 134672761 3221224544 3221221520 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10898 10131 603 41 0 10857 0
vsize: 43592
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10846 0 0 0 14972 27 0 0 25 0 1 0 546884144 44638208 10131 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10898 10131 603 41 0 10857 0
vsize: 43592
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10846 0 0 0 15972 27 0 0 25 0 1 0 546884144 44638208 10131 4294967295 134512640 134672761 3221224544 3221221952 134597184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10898 10131 603 41 0 10857 0
vsize: 43592
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10986 0 0 0 16972 27 0 0 25 0 1 0 546884144 44638208 10146 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10898 10146 603 41 0 10857 0
vsize: 43592
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10986 0 0 0 17972 27 0 0 25 0 1 0 546884144 44638208 10146 4294967295 134512640 134672761 3221224544 3221221632 134522349 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10898 10146 603 41 0 10857 0
vsize: 43592
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10986 0 0 0 18973 27 0 0 25 0 1 0 546884144 44638208 10146 4294967295 134512640 134672761 3221224544 3221222352 134522369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10898 10146 603 41 0 10857 0
vsize: 43592
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10986 0 0 0 19973 28 0 0 25 0 1 0 546884144 44638208 10146 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10898 10146 603 41 0 10857 0
vsize: 43592
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 10987 0 0 0 20973 28 0 0 25 0 1 0 546884144 44638208 10147 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10898 10147 603 41 0 10857 0
vsize: 43592
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11136 0 0 0 21972 28 0 0 25 0 1 0 546884144 44666880 10168 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10905 10168 603 41 0 10864 0
vsize: 43620
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11136 0 0 0 22972 28 0 0 25 0 1 0 546884144 44666880 10168 4294967295 134512640 134672761 3221224544 3221222384 134597176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10905 10168 603 41 0 10864 0
vsize: 43620
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11136 0 0 0 23972 28 0 0 25 0 1 0 546884144 44666880 10168 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10905 10168 603 41 0 10864 0
vsize: 43620
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11136 0 0 0 24972 28 0 0 25 0 1 0 546884144 44666880 10168 4294967295 134512640 134672761 3221224544 3221223248 134597224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10905 10168 603 41 0 10864 0
vsize: 43620
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11137 0 0 0 25972 29 0 0 25 0 1 0 546884144 44666880 10169 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10905 10169 603 41 0 10864 0
vsize: 43620
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11174 0 0 0 26972 29 0 0 25 0 1 0 546884144 44937216 10206 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10971 10206 603 41 0 10930 0
vsize: 43884
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11201 0 0 0 27972 29 0 0 25 0 1 0 546884144 44937216 10233 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10971 10233 603 41 0 10930 0
vsize: 43884
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11429 0 0 0 28972 29 0 0 25 0 1 0 546884144 45121536 10280 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11016 10280 603 41 0 10975 0
vsize: 44064
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11429 0 0 0 29972 29 0 0 25 0 1 0 546884144 45121536 10280 4294967295 134512640 134672761 3221224544 3221221868 1075349691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11016 10280 603 41 0 10975 0
vsize: 44064
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11429 0 0 0 30972 29 0 0 25 0 1 0 546884144 45121536 10280 4294967295 134512640 134672761 3221224544 3221222384 134597224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11016 10280 603 41 0 10975 0
vsize: 44064
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11429 0 0 0 31972 29 0 0 25 0 1 0 546884144 45121536 10280 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11016 10280 603 41 0 10975 0
vsize: 44064
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11434 0 0 0 32972 29 0 0 25 0 1 0 546884144 45121536 10281 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11016 10281 603 41 0 10975 0
vsize: 44064
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11704 0 0 0 33972 30 0 0 25 0 1 0 546884144 45477888 10368 4294967295 134512640 134672761 3221224544 3221221808 134597257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11103 10368 603 41 0 11062 0
vsize: 44412
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11704 0 0 0 34972 30 0 0 25 0 1 0 546884144 45477888 10368 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11103 10368 603 41 0 11062 0
vsize: 44412
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11704 0 0 0 35972 30 0 0 25 0 1 0 546884144 45477888 10368 4294967295 134512640 134672761 3221224544 3221222240 134597176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11103 10368 603 41 0 11062 0
vsize: 44412
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11704 0 0 0 36972 30 0 0 25 0 1 0 546884144 45477888 10368 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11103 10368 603 41 0 11062 0
vsize: 44412
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11704 0 0 0 37972 30 0 0 25 0 1 0 546884144 45477888 10368 4294967295 134512640 134672761 3221224544 3221223248 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11103 10368 603 41 0 11062 0
vsize: 44412
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11745 0 0 0 38972 31 0 0 25 0 1 0 546884144 45748224 10408 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11169 10408 603 41 0 11128 0
vsize: 44676
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11989 0 0 0 39972 31 0 0 25 0 1 0 546884144 46297088 10527 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11303 10527 603 41 0 11262 0
vsize: 45212
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11989 0 0 0 40972 31 0 0 25 0 1 0 546884144 46297088 10527 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11303 10527 603 41 0 11262 0
vsize: 45212
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11989 0 0 0 41972 32 0 0 25 0 1 0 546884144 46297088 10527 4294967295 134512640 134672761 3221224544 3221222096 134597191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11303 10527 603 41 0 11262 0
vsize: 45212
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11989 0 0 0 42972 32 0 0 25 0 1 0 546884144 46297088 10527 4294967295 134512640 134672761 3221224544 3221222096 134597184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11303 10527 603 41 0 11262 0
vsize: 45212
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 11990 0 0 0 43972 32 0 0 25 0 1 0 546884144 46297088 10528 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11303 10528 603 41 0 11262 0
vsize: 45212
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12163 0 0 0 44972 32 0 0 25 0 1 0 546884144 46321664 10560 4294967295 134512640 134672761 3221224544 3221221952 134597191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11309 10560 603 41 0 11268 0
vsize: 45236
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12163 0 0 0 45972 32 0 0 25 0 1 0 546884144 46321664 10560 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11309 10560 603 41 0 11268 0
vsize: 45236
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12163 0 0 0 46972 32 0 0 25 0 1 0 546884144 46321664 10560 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11309 10560 603 41 0 11268 0
vsize: 45236
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12163 0 0 0 47972 32 0 0 25 0 1 0 546884144 46321664 10560 4294967295 134512640 134672761 3221224544 3221222096 134597203 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11309 10560 603 41 0 11268 0
vsize: 45236
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12164 0 0 0 48973 32 0 0 25 0 1 0 546884144 46321664 10561 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11309 10561 603 41 0 11268 0
vsize: 45236
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12310 0 0 0 49972 33 0 0 25 0 1 0 546884144 46321664 10561 4294967295 134512640 134672761 3221224544 3221222096 134597203 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11309 10561 603 41 0 11268 0
vsize: 45236
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12310 0 0 0 50972 33 0 0 25 0 1 0 546884144 46321664 10561 4294967295 134512640 134672761 3221224544 3221222352 134522368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11309 10561 603 41 0 11268 0
vsize: 45236
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12310 0 0 0 51972 33 0 0 25 0 1 0 546884144 46321664 10561 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11309 10561 603 41 0 11268 0
vsize: 45236
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12310 0 0 0 52973 33 0 0 25 0 1 0 546884144 46321664 10561 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11309 10561 603 41 0 11268 0
vsize: 45236
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12461 0 0 0 53972 34 0 0 25 0 1 0 546884144 46456832 10587 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11342 10587 603 41 0 11301 0
vsize: 45368
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12461 0 0 0 54972 34 0 0 25 0 1 0 546884144 46456832 10587 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11342 10587 603 41 0 11301 0
vsize: 45368
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12461 0 0 0 55972 34 0 0 25 0 1 0 546884144 46456832 10587 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11342 10587 603 41 0 11301 0
vsize: 45368
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12461 0 0 0 56972 34 0 0 25 0 1 0 546884144 46456832 10587 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11342 10587 603 41 0 11301 0
vsize: 45368
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12461 0 0 0 57972 34 0 0 25 0 1 0 546884144 46456832 10587 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11342 10587 603 41 0 11301 0
vsize: 45368
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12462 0 0 0 58973 34 0 0 25 0 1 0 546884144 46456832 10588 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11342 10588 603 41 0 11301 0
vsize: 45368
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12687 0 0 0 59972 35 0 0 25 0 1 0 546884144 46608384 10634 4294967295 134512640 134672761 3221224544 3221222240 134597225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11379 10634 603 41 0 11338 0
vsize: 45516
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12687 0 0 0 60972 35 0 0 25 0 1 0 546884144 46608384 10634 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11379 10634 603 41 0 11338 0
vsize: 45516
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12687 0 0 0 61972 35 0 0 25 0 1 0 546884144 46608384 10634 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11379 10634 603 41 0 11338 0
vsize: 45516
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12687 0 0 0 62973 35 0 0 25 0 1 0 546884144 46608384 10634 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11379 10634 603 41 0 11338 0
vsize: 45516
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12687 0 0 0 63973 35 0 0 25 0 1 0 546884144 46608384 10634 4294967295 134512640 134672761 3221224544 3221222096 134597224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11379 10634 603 41 0 11338 0
vsize: 45516
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12741 0 0 0 64972 35 0 0 25 0 1 0 546884144 46878720 10688 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11445 10688 603 41 0 11404 0
vsize: 45780
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12804 0 0 0 65972 35 0 0 25 0 1 0 546884144 47144960 10751 4294967295 134512640 134672761 3221224544 3221223648 134560316 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11510 10751 603 41 0 11469 0
vsize: 46040
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 12982 0 0 0 66972 36 0 0 25 0 1 0 546884144 47808512 10929 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11672 10929 603 41 0 11631 0
vsize: 46688
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13200 0 0 0 67971 37 0 0 25 0 1 0 546884144 47951872 10968 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 10968 603 41 0 11666 0
vsize: 46828
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13200 0 0 0 68971 37 0 0 25 0 1 0 546884144 47951872 10968 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 10968 603 41 0 11666 0
vsize: 46828
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13200 0 0 0 69972 37 0 0 25 0 1 0 546884144 47951872 10968 4294967295 134512640 134672761 3221224544 3221222528 134597191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 10968 603 41 0 11666 0
vsize: 46828
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13200 0 0 0 70972 37 0 0 25 0 1 0 546884144 47951872 10968 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 10968 603 41 0 11666 0
vsize: 46828
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13408 0 0 0 71971 38 0 0 25 0 1 0 546884144 48029696 10988 4294967295 134512640 134672761 3221224544 3221220944 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11726 10988 603 41 0 11685 0
vsize: 46904
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13408 0 0 0 72971 38 0 0 25 0 1 0 546884144 48029696 10988 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11726 10988 603 41 0 11685 0
vsize: 46904
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13408 0 0 0 73972 38 0 0 25 0 1 0 546884144 48029696 10988 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11726 10988 603 41 0 11685 0
vsize: 46904
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13408 0 0 0 74972 38 0 0 25 0 1 0 546884144 48029696 10988 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11726 10988 603 41 0 11685 0
vsize: 46904
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13408 0 0 0 75972 38 0 0 25 0 1 0 546884144 48029696 10988 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11726 10988 603 41 0 11685 0
vsize: 46904
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13438 0 0 0 76972 38 0 0 25 0 1 0 546884144 48304128 11014 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11793 11014 603 41 0 11752 0
vsize: 47172
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13645 0 0 0 77972 39 0 0 25 0 1 0 546884144 48304128 11046 4294967295 134512640 134672761 3221224544 3221222240 134597225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11793 11046 603 41 0 11752 0
vsize: 47172
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13645 0 0 0 78972 39 0 0 25 0 1 0 546884144 48304128 11046 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11793 11046 603 41 0 11752 0
vsize: 47172
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13645 0 0 0 79972 39 0 0 25 0 1 0 546884144 48304128 11046 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11793 11046 603 41 0 11752 0
vsize: 47172
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13645 0 0 0 80972 39 0 0 25 0 1 0 546884144 48304128 11046 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11793 11046 603 41 0 11752 0
vsize: 47172
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13833 0 0 0 81972 40 0 0 25 0 1 0 546884144 48316416 11051 4294967295 134512640 134672761 3221224544 3221220944 134597165 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11796 11051 603 41 0 11755 0
vsize: 47184
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13833 0 0 0 82972 40 0 0 25 0 1 0 546884144 48316416 11051 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11796 11051 603 41 0 11755 0
vsize: 47184
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13833 0 0 0 83972 40 0 0 25 0 1 0 546884144 48316416 11051 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11796 11051 603 41 0 11755 0
vsize: 47184
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13833 0 0 0 84972 40 0 0 25 0 1 0 546884144 48316416 11051 4294967295 134512640 134672761 3221224544 3221222064 134522368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11796 11051 603 41 0 11755 0
vsize: 47184
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13833 0 0 0 85972 40 0 0 25 0 1 0 546884144 48316416 11051 4294967295 134512640 134672761 3221224544 3221222240 134597176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11796 11051 603 41 0 11755 0
vsize: 47184
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 13838 0 0 0 86972 40 0 0 25 0 1 0 546884144 48316416 11052 4294967295 134512640 134672761 3221224544 3221223712 134561415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11796 11052 603 41 0 11755 0
vsize: 47184
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 14067 0 0 0 87972 41 0 0 25 0 1 0 546884144 48500736 11097 4294967295 134512640 134672761 3221224544 3221222064 134522369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11841 11097 603 41 0 11800 0
vsize: 47364
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 14067 0 0 0 88972 41 0 0 25 0 1 0 546884144 48500736 11097 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11841 11097 603 41 0 11800 0
vsize: 47364
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 14067 0 0 0 89972 41 0 0 25 0 1 0 546884144 48500736 11097 4294967295 134512640 134672761 3221224544 3221222096 134597218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11841 11097 603 41 0 11800 0
vsize: 47364
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 14067 0 0 0 90972 41 0 0 25 0 1 0 546884144 48500736 11097 4294967295 134512640 134672761 3221224544 3221221808 134597169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11841 11097 603 41 0 11800 0
vsize: 47364
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 14070 0 0 0 91972 41 0 0 25 0 1 0 546884144 48500736 11097 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11841 11097 603 41 0 11800 0
vsize: 47364
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 14095 0 0 0 92972 41 0 0 25 0 1 0 546884144 48631808 11122 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11873 11122 603 41 0 11832 0
vsize: 47492
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 14308 0 0 0 93971 42 0 0 25 0 1 0 546884144 48730112 11154 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11897 11154 603 41 0 11856 0
vsize: 47588
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 14308 0 0 0 94971 42 0 0 25 0 1 0 546884144 48730112 11154 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11897 11154 603 41 0 11856 0
vsize: 47588
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 14308 0 0 0 95971 42 0 0 25 0 1 0 546884144 48730112 11154 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11897 11154 603 41 0 11856 0
vsize: 47588
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 14308 0 0 0 96971 42 0 0 25 0 1 0 546884144 48730112 11154 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11897 11154 603 41 0 11856 0
vsize: 47588
[startup+980.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 20678 0 0 0 97959 54 0 0 25 0 1 0 546884144 79155200 17194 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19325 17194 603 41 0 19284 0
vsize: 77300
[startup+990.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 20718 0 0 0 98959 55 0 0 25 0 1 0 546884144 79417344 17234 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19389 17234 603 41 0 19348 0
vsize: 77556
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21065 0 0 0 99959 55 0 0 25 0 1 0 546884144 80338944 17456 4294967295 134512640 134672761 3221224544 3221222384 134597209 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19614 17456 603 41 0 19573 0
vsize: 78456
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21065 0 0 0 100959 55 0 0 25 0 1 0 546884144 80338944 17456 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19614 17456 603 41 0 19573 0
vsize: 78456
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21065 0 0 0 101959 55 0 0 25 0 1 0 546884144 80338944 17456 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19614 17456 603 41 0 19573 0
vsize: 78456
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21065 0 0 0 102959 55 0 0 25 0 1 0 546884144 80338944 17456 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19614 17456 603 41 0 19573 0
vsize: 78456
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21229 0 0 0 103959 56 0 0 25 0 1 0 546884144 80429056 17491 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19636 17491 603 41 0 19595 0
vsize: 78544
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21229 0 0 0 104959 56 0 0 25 0 1 0 546884144 80429056 17491 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19636 17491 603 41 0 19595 0
vsize: 78544
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21229 0 0 0 105959 56 0 0 25 0 1 0 546884144 80429056 17491 4294967295 134512640 134672761 3221224544 3221222240 134597195 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19636 17491 603 41 0 19595 0
vsize: 78544
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21229 0 0 0 106959 56 0 0 25 0 1 0 546884144 80429056 17491 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19636 17491 603 41 0 19595 0
vsize: 78544
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21229 0 0 0 107959 56 0 0 25 0 1 0 546884144 80429056 17491 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19636 17491 603 41 0 19595 0
vsize: 78544
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21301 0 0 0 108959 56 0 0 25 0 1 0 546884144 80691200 17563 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19700 17563 603 41 0 19659 0
vsize: 78800
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21309 0 0 0 109959 56 0 0 25 0 1 0 546884144 80953344 17571 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19764 17571 603 41 0 19723 0
vsize: 79056
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21462 0 0 0 110959 57 0 0 25 0 1 0 546884144 81088512 17599 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19797 17599 603 41 0 19756 0
vsize: 79188
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21462 0 0 0 111959 57 0 0 25 0 1 0 546884144 81088512 17599 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19797 17599 603 41 0 19756 0
vsize: 79188
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21462 0 0 0 112960 57 0 0 25 0 1 0 546884144 81088512 17599 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19797 17599 603 41 0 19756 0
vsize: 79188
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21462 0 0 0 113960 57 0 0 25 0 1 0 546884144 81088512 17599 4294967295 134512640 134672761 3221224544 3221222384 134597225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19797 17599 603 41 0 19756 0
vsize: 79188
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21463 0 0 0 114960 57 0 0 25 0 1 0 546884144 81088512 17600 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19797 17600 603 41 0 19756 0
vsize: 79188
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21464 0 0 0 115960 57 0 0 25 0 1 0 546884144 81088512 17601 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19797 17601 603 41 0 19756 0
vsize: 79188
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21525 0 0 0 116960 57 0 0 25 0 1 0 546884144 81350656 17662 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19861 17662 603 41 0 19820 0
vsize: 79444
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21758 0 0 0 117960 57 0 0 25 0 1 0 546884144 81522688 17714 4294967295 134512640 134672761 3221224544 3221222384 134597225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19903 17714 603 41 0 19862 0
vsize: 79612
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21758 0 0 0 118960 57 0 0 25 0 1 0 546884144 81522688 17714 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19903 17714 603 41 0 19862 0
vsize: 79612
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22948
Raw data (stat): 22948 (minisat+) R 22947 11931 11930 0 -1 0 21758 0 0 0 119960 57 0 0 25 0 1 0 546884144 81522688 17714 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19903 17714 603 41 0 19862 0
vsize: 79612
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 22948
Raw data (stat): 22948 (minisat+) Z 22947 11931 11930 0 -1 12 21762 0 0 0 119960 61 0 0 25 0 1 0 546884144 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.06
CPU time (s): 1200.22
CPU user time (s): 1199.6
CPU system time (s): 0.613906
CPU usage (%): 100.013
Max. virtual memory (Kb): 79612
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####