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-pipex.opb
MD5SUM	b9c1029cc1d97a8d60e984f96f5d3267
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	788263
Optimality of the best value was proved	NO
Number of terms in the objective function	48
Biggest coefficient in the objective function	107865
Number of bits for the biggest coefficient in the objective function	17
Sum of the numbers in the objective function	2514082
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	107865
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	2514082
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02684
Number of variables	48
Total number of constraints	73
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	64
Number of constraints which are nor clauses,nor cardinality constraints	9
Minimum length of a constraint	1
Maximum length of a constraint	16
Trace number 18938

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-21 17:19:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17197 boxname=wulflinc6 idbench=1323 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b9c1029cc1d97a8d60e984f96f5d3267  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-pipex.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-pipex.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-pipex.opb
IDLAUNCH: 17197
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        549504 kB
Buffers:         22900 kB
Cached:         440996 kB
SwapCached:        544 kB
Active:          45800 kB
Inactive:       420128 kB
HighTotal:      131008 kB
HighFree:         1652 kB
LowTotal:       903652 kB
LowFree:        547852 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13572 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:26:31 (client local time) WITH STATUS 0 IN 399.781 SECONDS
stats: 17197 7 399.781 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################
c   -- Clauses(.)/Splits(s): (none)
c ---[  40]---> Sorter-cost:  709     Base: 2 5 2
c ---[  39]---> Sorter-cost:  709     Base: 2 5 2
c ---[  38]---> Sorter-cost:  709     Base: 2 5 2
c ---[  37]---> Sorter-cost:  485     Base: 2 5 2
c ---[  36]---> Sorter-cost:  485     Base: 2 5 2
c ---[  35]---> Sorter-cost:  485     Base: 2 5 2
c ---[  34]---> BDD-cost:  145
c ---[  33]---> Sorter-cost:  847     Base: 2 5 3 3
c ---[  32]---> Sorter-cost:  846     Base: 2 5 3 3
c ---[  30]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  26]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  18]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  12]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    3
c ---[   6]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   10626    25220 |    3187       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4140          
c   -- var.elim.:  2000/4140          
c   -- var.elim.:  3000/4140          
c   -- var.elim.:  4000/4140          
c   -- var.elim.:  4140/4140          
c   -- var.elim.:  1000/2023          
c   -- var.elim.:  2000/2023          
c   -- var.elim.:  2023/2023          
c   -- var.elim.:  33/33          
c   -- subsuming                       
c   -- var.elim.:  1000/1093          
c   -- var.elim.:  1093/1093          
c   -- var.elim.:  399/399          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  171/171          
c |         0 |    8527    27325 |      --       0       --      -- |     --   | -2099/2164
c |         0 |    8527    27325 |    3410       0        0     nan |  0.000 % |
c |       100 |    8527    27325 |    3751     100     1606    16.1 |  1.202 % |
c |       253 |    8527    27325 |    4127     253     8124    32.1 |  1.202 % |
c |       479 |    8527    27325 |    4539     479    18652    38.9 |  1.203 % |
c |       817 |    8527    27325 |    4993     817    31708    38.8 |  1.202 % |
c ==============================================================================
c (current CPU-time: 1.52677 s)
c ==============================================================================
c [1mFound solution: 849258[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 9869     Base: 2 5 3 3 2 2 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1090 |   32385    83129 |    9715    1090    45898    42.1 |  1.202 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8764          
c   -- var.elim.:  2000/8764          
c   -- var.elim.:  3000/8764          
c   -- var.elim.:  4000/8764          
c   -- var.elim.:  5000/8764          
c   -- var.elim.:  6000/8764          
c   -- var.elim.:  7000/8764          
c   -- var.elim.:  8000/8764          
c   -- var.elim.:  8764/8764          
c   -- var.elim.:  1000/4656          
c   -- var.elim.:  2000/4656          
c   -- var.elim.:  3000/4656          
c   -- var.elim.:  4000/4656          
c   -- var.elim.:  4656/4656          
c   -- var.elim.:  689/689          
c   -- var.elim.:  616/616          
c   -- var.elim.:  74/74          
c   -- subsuming                       
c   -- var.elim.:  1000/1076          
c   -- var.elim.:  1076/1076          
c   -- var.elim.:  363/363          
c   -- var.elim.:  260/260          
c   -- var.elim.:  286/286          
c   -- subsuming                       
c   -- var.elim.:  341/341          
c   -- var.elim.:  69/69          
c |      1090 |   28420    90753 |      --    1090       --      -- |     --   | -3965/7625
c |      1090 |   28420    90753 |   11368    1090    45898    42.1 |  1.202 % |
c |      1191 |   28420    90753 |   12504    1191    49320    41.4 |  1.851 % |
c |      1342 |   28420    90753 |   13755    1342    53801    40.1 |  1.851 % |
c |      1568 |   28420    90753 |   15130    1568    61460    39.2 |  1.851 % |
c |      1907 |   28420    90753 |   16643    1907    76328    40.0 |  1.851 % |
c ==============================================================================
c (current CPU-time: 7.34788 s)
c ==============================================================================
c [1mFound solution: 833719[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 5 3 3 2 2 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2217 |   29748    94113 |    8924    2217    93447    42.2 |  1.851 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1795          
c   -- var.elim.:  1795/1795          
c   -- var.elim.:  896/896          
c   -- var.elim.:  170/170          
c   -- var.elim.:  126/126          
c   -- subsuming                       
c   -- var.elim.:  35/35          
c |      2217 |   29007    93602 |      --    2217       --      -- |     --   | -733/-494
c |      2217 |   29007    93602 |   11602    2217    93447    42.2 |  1.851 % |
c |      2319 |   29007    93602 |   12763    2319    97129    41.9 |  2.105 % |
c |      2470 |   29007    93602 |   14039    2470   101853    41.2 |  2.105 % |
c |      2698 |   29007    93602 |   15443    2698   109622    40.6 |  2.105 % |
c |      3035 |   29007    93602 |   16987    3035   120872    39.8 |  2.105 % |
c |      3541 |   29007    93602 |   18686    3541   141847    40.1 |  2.105 % |
c |      4301 |   29007    93602 |   20555    4301   171217    39.8 |  2.105 % |
c |      5442 |   29007    93602 |   22610    5442   217424    40.0 |  2.105 % |
c ==============================================================================
c (current CPU-time: 20.2809 s)
c ==============================================================================
c [1mFound solution: 820766[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 5 3 3 2 2 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6489 |   29013    93021 |    8703    6488   280107    43.2 |  2.105 % |
c   -- subsuming                       
c   -- var.elim.:  788/788          
c   -- var.elim.:  537/537          
c   -- var.elim.:  91/91          
c   -- var.elim.:  117/117          
c   -- subsuming                       
c   -- var.elim.:  54/54          
c   -- var.elim.:  15/15          
c |      6489 |   28784    93192 |      --    6488       --      -- |     --   | -224/182
c |      6489 |   28784    93192 |   11513    6488   280107    43.2 |  2.105 % |
c |      6591 |   28784    93192 |   12664    6590   291648    44.3 |  2.710 % |
c |      6742 |   28784    93192 |   13931    6741   299297    44.4 |  2.710 % |
c |      6970 |   28784    93192 |   15324    6969   310407    44.5 |  2.710 % |
c |      7310 |   28784    93192 |   16857    7309   331421    45.3 |  2.710 % |
c |      7817 |   28784    93192 |   18542    7816   355383    45.5 |  2.710 % |
c ==============================================================================
c (current CPU-time: 27.1499 s)
c ==============================================================================
c [1mFound solution: 811394[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 5 3 3 2 2 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8275 |   28942    93786 |    8682    8274   381481    46.1 |  2.710 % |
c   -- subsuming                       
c   -- var.elim.:  422/422          
c   -- var.elim.:  323/323          
c   -- var.elim.:  183/183          
c   -- var.elim.:  146/146          
c |      8275 |   28825    94602 |      --    8274       --      -- |     --   | -116/819
c |      8275 |   28825    94602 |   11530    8274   381481    46.1 |  2.710 % |
c |      8375 |   28825    94602 |   12683    8374   387624    46.3 |  2.751 % |
c |      8529 |   28825    94602 |   13951    8528   394569    46.3 |  2.751 % |
c |      8754 |   28825    94602 |   15346    8753   404031    46.2 |  2.751 % |
c |      9092 |   28825    94602 |   16881    9091   421104    46.3 |  2.751 % |
c |      9599 |   28825    94602 |   18569    9598   441269    46.0 |  2.751 % |
c |     10359 |   28825    94602 |   20426   10358   474245    45.8 |  2.751 % |
c ==============================================================================
c (current CPU-time: 37.6873 s)
c ==============================================================================
c [1mFound solution: 806822[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 5 3 3 2 2 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11439 |   29026    95293 |    8707   11438   562545    49.2 |  2.751 % |
c   -- subsuming                       
c   -- var.elim.:  494/494          
c   -- var.elim.:  342/342          
c   -- var.elim.:  154/154          
c   -- var.elim.:  161/161          
c |     11439 |   28893    95786 |      --   11438       --      -- |     --   | -133/494
c |     11439 |   28893    95786 |   11557   11438   562545    49.2 |  2.751 % |
c |     11539 |   28878    95708 |   12706   11537   570270    49.4 |  2.790 % |
c |     11690 |   28878    95708 |   13976   11688   577500    49.4 |  2.790 % |
c |     11917 |   28878    95708 |   15374   11915   605289    50.8 |  2.790 % |
c |     12255 |   28878    95708 |   16912   12253   625792    51.1 |  2.790 % |
c |     12762 |   28878    95708 |   18603   12760   647138    50.7 |  2.790 % |
c |     13525 |   28878    95708 |   20463   13523   681122    50.4 |  2.792 % |
c |     14664 |   28745    94941 |   22406   14618   767789    52.5 |  2.968 % |
c |     16376 |   28731    94872 |   24634   16211   886112    54.7 |  2.998 % |
c |     18939 |   28315    92594 |   26706   18773  1175266    62.6 |  3.710 % |
c |     22783 |   28258    92362 |   29317   22614  1918940    84.9 |  3.903 % |
c |     28550 |   28170    91356 |   32148   28378  2759933    97.3 |  4.037 % |
c ==============================================================================
c (current CPU-time: 117.27 s)
c ==============================================================================
c [1mFound solution: 802184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 5 3 3 2 2 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     32554 |   28171    91396 |    8451   32379  3552485   109.7 |  4.037 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1348          
c   -- var.elim.:  1348/1348          
c   -- var.elim.:  993/993          
c   -- var.elim.:  184/184          
c   -- var.elim.:  189/189          
c   -- subsuming                       
c   -- var.elim.:  406/406          
c   -- var.elim.:  58/58          
c |     32554 |   27924    92860 |      --   32379       --      -- |     --   | -244/1471
c |     32554 |   27924    92860 |   11169   32379  3552485   109.7 |  4.037 % |
c |     32655 |   27849    92289 |   12253    4461   117952    26.4 |  4.494 % |
c |     32805 |   27665    90762 |   13389    4608   124851    27.1 |  4.796 % |
c |     33030 |   27665    90762 |   14728    4833   144555    29.9 |  4.796 % |
c |     33367 |   27665    90762 |   16201    5170   174629    33.8 |  4.796 % |
c |     33875 |   27665    90762 |   17821    5678   270450    47.6 |  4.796 % |
c |     34634 |   27665    90762 |   19604    6437   396073    61.5 |  4.796 % |
c |     35773 |   27578    90388 |   21496    7575   554035    73.1 |  5.022 % |
c |     37481 |   27578    90388 |   23646    9283   808616    87.1 |  5.022 % |
c |     40044 |   27578    90388 |   26010   11846  1281459   108.2 |  5.022 % |
c |     43888 |   27578    90388 |   28612   15690  1794683   114.4 |  5.022 % |
c |     49654 |   27492    90065 |   31375   21455  2809171   130.9 |  5.203 % |
c |     58303 |   27385    89665 |   34378   30099  4300962   142.9 |  5.414 % |
c |     71279 |   27332    89416 |   37742   23363  2967685   127.0 |  5.490 % |
c ==============================================================================
c (current CPU-time: 268.883 s)
c ==============================================================================
c [1mFound solution: 800174[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 5 3 3 2 2 3 3 3 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     74083 |   27464    89888 |    8239   26167  3372779   128.9 |  5.490 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1091          
c   -- var.elim.:  1091/1091          
c   -- var.elim.:  645/645          
c   -- var.elim.:  410/410          
c   -- var.elim.:  305/305          
c   -- var.elim.:  34/34          
c   -- subsuming                       
c   -- var.elim.:  263/263          
c   -- var.elim.:  119/119          
c |     74083 |   27121    89995 |      --   26167       --      -- |     --   | -335/124
c |     74083 |   27121    89995 |   10848   20847  1228667    58.9 |  5.490 % |
c |     74184 |   27121    89995 |   11933    9239   430676    46.6 |  5.634 % |
c |     74335 |   27121    89995 |   13126    9390   453323    48.3 |  5.633 % |
c |     74561 |   27121    89995 |   14439    9616   481932    50.1 |  5.633 % |
c |     74898 |   27121    89995 |   15883    9953   523352    52.6 |  5.634 % |
c |     75408 |   27121    89995 |   17471   10463   615191    58.8 |  5.634 % |
c |     76168 |   27121    89995 |   19218   11223   744548    66.3 |  5.634 % |#### 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.79 0.90 0.89 2/54 20462
Raw data (stat): 20462 (runsolver) R 20461 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488607819 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.0007 s]
Raw data (loadavg): 0.82 0.91 0.89 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 3282 0 0 0 988 10 0 0 25 0 1 0 488607819 11558912 2324 4294967295 134512640 134672761 3221224544 3221223584 134612764 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2822 2324 603 41 0 2781 0
vsize: 11288
[startup+20.0018 s]
Raw data (loadavg): 0.85 0.91 0.89 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 3341 0 0 0 1988 11 0 0 25 0 1 0 488607819 11821056 2383 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2886 2383 603 41 0 2845 0
vsize: 11544
[startup+30.003 s]
Raw data (loadavg): 0.87 0.91 0.89 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 4167 0 0 0 2984 15 0 0 25 0 1 0 488607819 13979648 2883 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3413 2883 603 41 0 3372 0
vsize: 13652
[startup+40.0031 s]
Raw data (loadavg): 0.89 0.91 0.89 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 4565 0 0 0 3983 17 0 0 25 0 1 0 488607819 14905344 3115 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3639 3115 603 41 0 3598 0
vsize: 14556
[startup+50.0043 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 4565 0 0 0 4983 17 0 0 25 0 1 0 488607819 14905344 3115 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3639 3115 603 41 0 3598 0
vsize: 14556
[startup+60.0044 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 4805 0 0 0 5982 18 0 0 25 0 1 0 488607819 15908864 3355 4294967295 134512640 134672761 3221224544 3221223332 1074972064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3884 3355 603 41 0 3843 0
vsize: 15536
[startup+70.0055 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 5264 0 0 0 6981 19 0 0 25 0 1 0 488607819 17743872 3814 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4332 3814 603 41 0 4291 0
vsize: 17328
[startup+80.0071 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 5796 0 0 0 7980 21 0 0 25 0 1 0 488607819 19984384 4346 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4879 4346 603 41 0 4838 0
vsize: 19516
[startup+90.0071 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 6222 0 0 0 8979 22 0 0 25 0 1 0 488607819 21704704 4772 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5299 4772 603 41 0 5258 0
vsize: 21196
[startup+100.007 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 6620 0 0 0 9978 24 0 0 25 0 1 0 488607819 23289856 5170 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5686 5170 603 41 0 5645 0
vsize: 22744
[startup+110.007 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 7080 0 0 0 10977 25 0 0 25 0 1 0 488607819 25128960 5630 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6135 5630 603 41 0 6094 0
vsize: 24540
[startup+120.007 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 8129 0 0 0 11974 28 0 0 25 0 1 0 488607819 28147712 6348 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6348 603 41 0 6831 0
vsize: 27488
[startup+130.007 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 8129 0 0 0 12975 28 0 0 25 0 1 0 488607819 28147712 6348 4294967295 134512640 134672761 3221224544 3221223728 134615845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6348 603 41 0 6831 0
vsize: 27488
[startup+140.008 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 8129 0 0 0 13975 28 0 0 25 0 1 0 488607819 28147712 6348 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6348 603 41 0 6831 0
vsize: 27488
[startup+150.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 8129 0 0 0 14975 28 0 0 25 0 1 0 488607819 28147712 6348 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6348 603 41 0 6831 0
vsize: 27488
[startup+160.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 8129 0 0 0 15975 28 0 0 25 0 1 0 488607819 28147712 6348 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6348 603 41 0 6831 0
vsize: 27488
[startup+170.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 8129 0 0 0 16975 28 0 0 25 0 1 0 488607819 28147712 6348 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6348 603 41 0 6831 0
vsize: 27488
[startup+180.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 8129 0 0 0 17976 28 0 0 25 0 1 0 488607819 28147712 6348 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6348 603 41 0 6831 0
vsize: 27488
[startup+190.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 8129 0 0 0 18976 28 0 0 25 0 1 0 488607819 28147712 6348 4294967295 134512640 134672761 3221224544 3221223744 134610652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6348 603 41 0 6831 0
vsize: 27488
[startup+200.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 8246 0 0 0 19976 28 0 0 25 0 1 0 488607819 28663808 6465 4294967295 134512640 134672761 3221224544 3221223680 134614822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6998 6465 603 41 0 6957 0
vsize: 27992
[startup+210.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 8652 0 0 0 20975 29 0 0 25 0 1 0 488607819 30240768 6871 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7383 6871 603 41 0 7342 0
vsize: 29532
[startup+220.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 9158 0 0 0 21975 31 0 0 25 0 1 0 488607819 32346112 7377 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7897 7377 603 41 0 7856 0
vsize: 31588
[startup+230.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 9545 0 0 0 22973 32 0 0 25 0 1 0 488607819 34054144 7764 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8314 7764 603 41 0 8273 0
vsize: 33256
[startup+240.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 9744 0 0 0 23974 32 0 0 25 0 1 0 488607819 34672640 7927 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8465 7927 603 41 0 8424 0
vsize: 33860
[startup+250.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 9744 0 0 0 24974 32 0 0 25 0 1 0 488607819 34672640 7927 4294967295 134512640 134672761 3221224544 3221223728 134615991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8465 7927 603 41 0 8424 0
vsize: 33860
[startup+260.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 9747 0 0 0 25974 32 0 0 25 0 1 0 488607819 34672640 7930 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8465 7930 603 41 0 8424 0
vsize: 33860
[startup+270.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10264 0 0 0 26973 34 0 0 25 0 1 0 488607819 34971648 7997 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8538 7997 603 41 0 8497 0
vsize: 34152
[startup+280.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10400 0 0 0 27973 35 0 0 25 0 1 0 488607819 34971648 8005 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8538 8005 603 41 0 8497 0
vsize: 34152
[startup+290.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10400 0 0 0 28972 35 0 0 25 0 1 0 488607819 34971648 8005 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8005 603 41 0 8497 0
vsize: 34152
[startup+300.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10400 0 0 0 29972 35 0 0 25 0 1 0 488607819 34971648 8005 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8005 603 41 0 8497 0
vsize: 34152
[startup+310.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10400 0 0 0 30973 35 0 0 25 0 1 0 488607819 34971648 8005 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8005 603 41 0 8497 0
vsize: 34152
[startup+320.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10401 0 0 0 31973 35 0 0 25 0 1 0 488607819 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8006 603 41 0 8497 0
vsize: 34152
[startup+330.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10401 0 0 0 32973 35 0 0 25 0 1 0 488607819 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8006 603 41 0 8497 0
vsize: 34152
[startup+340.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10401 0 0 0 33974 35 0 0 25 0 1 0 488607819 34971648 8006 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8006 603 41 0 8497 0
vsize: 34152
[startup+350.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10401 0 0 0 34974 35 0 0 25 0 1 0 488607819 34971648 8006 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8006 603 41 0 8497 0
vsize: 34152
[startup+360.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10401 0 0 0 35974 35 0 0 25 0 1 0 488607819 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8006 603 41 0 8497 0
vsize: 34152
[startup+370.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10401 0 0 0 36975 35 0 0 25 0 1 0 488607819 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8006 603 41 0 8497 0
vsize: 34152
[startup+380.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10401 0 0 0 37975 35 0 0 25 0 1 0 488607819 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8006 603 41 0 8497 0
vsize: 34152
[startup+390.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10401 0 0 0 38975 35 0 0 25 0 1 0 488607819 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8006 603 41 0 8497 0
vsize: 34152
[startup+399.685 s]
Raw data (loadavg): 0.99 0.96 0.91 1/53 20462
Raw data (stat): 20462 (minisat+) R 20461 29653 29652 0 -1 0 10401 0 0 0 38975 35 0 0 25 0 1 0 488607819 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8538 8006 603 41 0 8497 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 399.684
CPU time (s): 399.781
CPU user time (s): 399.388
CPU system time (s): 0.39294
CPU usage (%): 100.024
Max. virtual memory (Kb): 34152
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####