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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:98.opb
MD5SUM	a89f4ed95903fddf213992506514bcf0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	16
Optimality of the best value was proved	NO
Number of terms in the objective function	906
Biggest coefficient in the objective function	553
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	2526
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	553
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	2526
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04184
Number of variables	906
Total number of constraints	1944
Number of constraints which are clauses	852
Number of constraints which are cardinality constraints (but not clauses)	1092
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 5693

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-14 01:25:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4131 boxname=wulflinc13 idbench=371 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a89f4ed95903fddf213992506514bcf0  /oldhome/oroussel/tmp/wulflinc13/normalized-10:20:4.5:0.95:98.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc13/normalized-10:20:4.5:0.95:98.opb /oldhome/oroussel/tmp/wulflinc13/normalized-10:20:4.5:0.95:98.opb
IDLAUNCH: 4131
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        895088 kB
Buffers:         35180 kB
Cached:          84584 kB
SwapCached:        392 kB
Active:          54168 kB
Inactive:        68824 kB
HighTotal:      131008 kB
HighFree:        42532 kB
LowTotal:       903652 kB
LowFree:        852556 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11040 kB
Committed_AS:    63508 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:45:11 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4131 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1038 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 187]---> BDD-cost:    5
c ---[ 186]---> BDD-cost:    8
c ---[ 185]---> BDD-cost:   14
c ---[ 184]---> BDD-cost:   14
c ---[ 183]---> BDD-cost:   17
c ---[ 182]---> BDD-cost:   14
c ---[ 181]---> BDD-cost:   23
c ---[ 180]---> BDD-cost:   20
c ---[ 179]---> BDD-cost:   29
c ---[ 178]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   38
c ---[ 176]---> BDD-cost:   32
c ---[ 175]---> BDD-cost:   32
c ---[ 174]---> BDD-cost:   23
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   20
c ---[ 171]---> BDD-cost:   20
c ---[ 170]---> BDD-cost:   14
c ---[ 169]---> BDD-cost:   14
c ---[ 168]---> BDD-cost:    8
c ---[ 167]---> BDD-cost:    8
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:   17
c ---[ 163]---> BDD-cost:   18
c ---[ 162]---> BDD-cost:   18
c ---[ 161]---> BDD-cost:   35
c ---[ 160]---> BDD-cost:   35
c ---[ 159]---> BDD-cost:   41
c ---[ 158]---> BDD-cost:   35
c ---[ 157]---> BDD-cost:   38
c ---[ 156]---> BDD-cost:   38
c ---[ 155]---> BDD-cost:   41
c ---[ 154]---> BDD-cost:   35
c ---[ 153]---> BDD-cost:   38
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   20
c ---[ 150]---> BDD-cost:   17
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:   11
c ---[ 145]---> BDD-cost:   14
c ---[ 144]---> BDD-cost:   17
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   29
c ---[ 141]---> BDD-cost:   41
c ---[ 140]---> BDD-cost:   44
c ---[ 139]---> BDD-cost:   44
c ---[ 138]---> BDD-cost:   38
c ---[ 137]---> BDD-cost:   39
c ---[ 136]---> BDD-cost:   41
c ---[ 135]---> BDD-cost:   44
c ---[ 134]---> BDD-cost:   44
c ---[ 133]---> BDD-cost:   41
c ---[ 132]---> BDD-cost:   29
c ---[ 131]---> BDD-cost:   29
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   26
c ---[ 128]---> BDD-cost:   14
c ---[ 127]---> BDD-cost:    8
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   14
c ---[ 124]---> BDD-cost:   17
c ---[ 123]---> BDD-cost:   21
c ---[ 122]---> BDD-cost:   29
c ---[ 121]---> BDD-cost:   35
c ---[ 120]---> BDD-cost:   44
c ---[ 119]---> BDD-cost:   47
c ---[ 118]---> BDD-cost:   44
c ---[ 117]---> BDD-cost:   44
c ---[ 116]---> BDD-cost:   44
c ---[ 115]---> BDD-cost:   41
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   35
c ---[ 112]---> BDD-cost:   32
c ---[ 111]---> BDD-cost:   29
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   20
c ---[ 108]---> BDD-cost:    6
c ---[ 107]---> BDD-cost:    5
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   20
c ---[ 104]---> BDD-cost:   23
c ---[ 103]---> BDD-cost:   26
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:   38
c ---[ 100]---> BDD-cost:   35
c ---[  99]---> BDD-cost:   41
c ---[  98]---> BDD-cost:   44
c ---[  97]---> BDD-cost:   41
c ---[  96]---> BDD-cost:   38
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:   38
c ---[  93]---> BDD-cost:   29
c ---[  92]---> BDD-cost:   20
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   20
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:    5
c ---[  87]---> BDD-cost:    5
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   20
c ---[  83]---> BDD-cost:   32
c ---[  82]---> BDD-cost:   41
c ---[  81]---> BDD-cost:   38
c ---[  80]---> BDD-cost:   35
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   35
c ---[  77]---> BDD-cost:   44
c ---[  76]---> BDD-cost:   35
c ---[  75]---> BDD-cost:   38
c ---[  74]---> BDD-cost:   35
c ---[  73]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   23
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   17
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   23
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   38
c ---[  60]---> BDD-cost:   32
c ---[  59]---> BDD-cost:   32
c ---[  58]---> BDD-cost:   35
c ---[  57]---> BDD-cost:   38
c ---[  56]---> BDD-cost:   32
c ---[  55]---> BDD-cost:   35
c ---[  54]---> BDD-cost:   29
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   29
c ---[  51]---> BDD-cost:   23
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   11
c ---[  47]---> BDD-cost:    8
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   20
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   35
c ---[  40]---> BDD-cost:   35
c ---[  39]---> BDD-cost:   35
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:   26
c ---[  36]---> BDD-cost:   23
c ---[  35]---> BDD-cost:   23
c ---[  34]---> BDD-cost:   23
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   17
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   20
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   20
c ---[  20]---> BDD-cost:   20
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   20
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    8
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:   14
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   14
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   11181    31975 |    3354       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5194          
c   -- var.elim.:  2000/5194          
c   -- var.elim.:  3000/5194          
c   -- var.elim.:  4000/5194          
c   -- var.elim.:  5000/5194          
c   -- var.elim.:  5194/5194          
c   -- var.elim.:  1000/2549          
c   -- var.elim.:  2000/2549          
c   -- var.elim.:  2549/2549          
c   -- subsuming                       
c   -- var.elim.:  1000/2363          
c   -- var.elim.:  2000/2363          
c   -- var.elim.:  2363/2363          
c   -- var.elim.:  1000/1254          
c   -- var.elim.:  1254/1254          
c   -- subsuming                       
c   -- var.elim.:  10/10          
c   -- var.elim.:  12/12          
c   -- var.elim.:  5/5          
c |         0 |    8393    30727 |      --       0       --      -- |     --   | -2788/-690
c |         0 |    8393    30727 |    3357       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.603908 s)
c ==============================================================================
c [1mFound solution: 952[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2188   maxlim: 468   bits: 10/9
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   23660    85256 |    7097       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3095          
c   -- var.elim.:  2000/3095          
c   -- var.elim.:  3000/3095          
c   -- var.elim.:  3095/3095          
c   -- var.elim.:  30/30          
c |         0 |   23480    84399 |      --       0       --      -- |     --   | -180/-851
c |         0 |   23480    84399 |    9392       0        0     nan |  0.000 % |
c |       100 |   23480    84399 |   10331     100      699     7.0 |  3.318 % |
c |       250 |   23480    84399 |   11364     250     1700     6.8 |  3.318 % |
c |       475 |   23480    84399 |   12500     475     3193     6.7 |  3.318 % |
c |       812 |   23480    84399 |   13750     812     6735     8.3 |  3.318 % |
c |      1318 |   23470    84359 |   15119    1316    11023     8.4 |  3.336 % |
c ==============================================================================
c (current CPU-time: 2.12968 s)
c ==============================================================================
c [1mFound solution: 168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1252   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1614 |   23532    84601 |    7059    1612    13349     8.3 |  3.336 % |
c   -- subsuming                       
c   -- var.elim.:  46/46          
c   -- var.elim.:  18/18          
c |      1614 |   23515    84527 |      --    1612       --      -- |     --   | -10/-33
c |      1614 |   23515    84527 |    9406    1612    13349     8.3 |  3.336 % |
c |      1714 |   23515    84527 |   10346    1712    14841     8.7 |  3.433 % |
c ==============================================================================
c (current CPU-time: 2.50062 s)
c ==============================================================================
c [1mFound solution: 154[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1266   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1861 |   23532    84605 |    7059    1859    15798     8.5 |  3.433 % |
c   -- subsuming                       
c   -- var.elim.:  20/20          
c   -- var.elim.:  9/9          
c |      1861 |   23529    84595 |      --    1859       --      -- |     --   | -3/-7
c |      1861 |   23529    84595 |    9411    1859    15798     8.5 |  3.433 % |
c ==============================================================================
c (current CPU-time: 2.75258 s)
c ==============================================================================
c [1mFound solution: 138[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1282   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1882 |   23548    84673 |    7064    1880    15884     8.4 |  3.433 % |
c   -- subsuming                       
c   -- var.elim.:  22/22          
c   -- var.elim.:  13/13          
c |      1882 |   23525    84573 |      --    1880       --      -- |     --   | -9/-15
c |      1882 |   23525    84573 |    9410    1880    15884     8.4 |  3.433 % |
c |      1982 |   23525    84573 |   10351    1980    17148     8.7 |  3.532 % |
c |      2132 |   23525    84573 |   11386    2130    17842     8.4 |  3.532 % |
c |      2357 |   23525    84573 |   12524    2355    20677     8.8 |  3.532 % |
c |      2697 |   23525    84573 |   13777    2695    38515    14.3 |  3.532 % |
c |      3203 |   23525    84573 |   15154    3201    43012    13.4 |  3.532 % |
c ==============================================================================
c (current CPU-time: 4.00539 s)
c ==============================================================================
c [1mFound solution: 136[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1284   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3600 |   23536    84621 |    7060    3598    51911    14.4 |  3.532 % |
c   -- subsuming                       
c   -- var.elim.:  18/18          
c   -- var.elim.:  12/12          
c |      3600 |   23533    84663 |      --    3598       --      -- |     --   | -3/44
c |      3600 |   23533    84663 |    9413    3582    49927    13.9 |  3.532 % |
c |      3700 |   23533    84663 |   10354    3682    50956    13.8 |  3.565 % |
c ==============================================================================
c (current CPU-time: 4.37933 s)
c ==============================================================================
c [1mFound solution: 122[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1298   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3749 |   23546    84717 |    7063    3731    51324    13.8 |  3.565 % |
c   -- subsuming                       
c   -- var.elim.:  18/18          
c   -- var.elim.:  11/11          
c |      3749 |   23539    84700 |      --    3731       --      -- |     --   | -7/-14
c |      3749 |   23539    84700 |    9415    3731    51324    13.8 |  3.565 % |
c |      3850 |   23539    84700 |   10357    3832    53527    14.0 |  3.614 % |
c |      4000 |   23539    84700 |   11392    3982    54194    13.6 |  3.614 % |
c |      4226 |   23539    84700 |   12532    4208    59751    14.2 |  3.614 % |
c ==============================================================================
c (current CPU-time: 5.17321 s)
c ==============================================================================
c [1mFound solution: 107[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1313   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4527 |   23545    84726 |    7063    4509    65936    14.6 |  3.614 % |
c   -- subsuming                       
c   -- var.elim.:  14/14          
c   -- var.elim.:  9/9          
c |      4527 |   23538    84688 |      --    4509       --      -- |     --   | -3/-1
c |      4527 |   23538    84688 |    9415    4509    65936    14.6 |  3.614 % |
c |      4627 |   23538    84688 |   10356    4609    66565    14.4 |  3.647 % |
c |      4777 |   23538    84688 |   11392    4759    71195    15.0 |  3.647 % |
c |      5004 |   23538    84688 |   12531    4986    73586    14.8 |  3.647 % |
c |      5341 |   23538    84688 |   13784    5323    91122    17.1 |  3.647 % |
c |      5848 |   23538    84688 |   15163    5830   110383    18.9 |  3.647 % |
c |      6608 |   23538    84688 |   16679    6590   136887    20.8 |  3.647 % |
c |      7748 |   23538    84688 |   18347    7730   201954    26.1 |  3.647 % |
c |      9456 |   23538    84688 |   20182    9438   394132    41.8 |  3.647 % |
c |     12019 |   23538    84688 |   22200   12001   624543    52.0 |  3.647 % |
c ==============================================================================
c (current CPU-time: 12.3811 s)
c ==============================================================================
c [1mFound solution: 97[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1323   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14337 |   23542    84711 |    7062   14319   683893    47.8 |  3.647 % |
c   -- subsuming                       
c   -- var.elim.:  10/10          
c |     14337 |   23542    84708 |      --   14319       --      -- |     --   | 0/-1
c |     14337 |   23542    84708 |    9416   14319   683893    47.8 |  3.647 % |
c |     14437 |   23542    84708 |   10358    9646   541634    56.2 |  3.680 % |
c |     14587 |   23542    84708 |   11394    9796   544528    55.6 |  3.680 % |
c |     14812 |   23542    84708 |   12533   10021   556076    55.5 |  3.680 % |
c |     15149 |   23542    84708 |   13787   10358   559064    54.0 |  3.680 % |
c |     15656 |   23542    84708 |   15165   10865   578872    53.3 |  3.680 % |
c |     16417 |   23542    84708 |   16682   11626   620697    53.4 |  3.680 % |
c |     17558 |   23542    84708 |   18350   12767   680098    53.3 |  3.680 % |
c |     19268 |   23542    84708 |   20185   14477   813588    56.2 |  3.680 % |
c |     21830 |   23542    84708 |   22204   17039  1029954    60.4 |  3.680 % |
c |     25675 |   23542    84708 |   24424   20884  1274110    61.0 |  3.680 % |
c |     31441 |   23542    84708 |   26867   14264  1033622    72.5 |  3.680 % |
c |     40091 |   23542    84708 |   29553   22914  1954252    85.3 |  3.680 % |
c |     53070 |   23542    84708 |   32509   17534  2069241   118.0 |  3.680 % |
c |     72531 |   23542    84708 |   35760   13701  1778669   129.8 |  3.680 % |
c |    101724 |   23542    84708 |   39336   16993  2158497   127.0 |  3.680 % |
c |    145515 |   23542    84708 |   43269   31744  2941135    92.7 |  3.680 % |
c ==============================================================================
c (current CPU-time: 273.714 s)
c ==============================================================================
c [1mFound solution: 96[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1324   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    192241 |   23546    84727 |    7063   44314  7544616   170.3 |  3.680 % |
c   -- subsuming                       
c   -- var.elim.:  13/13          
c   -- var.elim.:  11/11          
c |    192241 |   23544    84730 |      --   44314       --      -- |     --   | -2/4
c |    192241 |   23544    84730 |    9417   44314  7544616   170.3 |  3.680 % |
c |    192341 |   23544    84730 |   10359    9162  1872464   204.4 |  3.696 % |
c |    192493 |   23544    84730 |   11395    9314  1874723   201.3 |  3.696 % |
c |    192718 |   23544    84730 |   12534    9539  1886413   197.8 |  3.696 % |
c |    193056 |   23544    84730 |   13788    9877  1890982   191.5 |  3.696 % |
c |    193562 |   23544    84730 |   15167   10383  1898715   182.9 |  3.696 % |
c |    194322 |   23544    84730 |   16683   11143  1924936   172.7 |  3.696 % |
c |    195461 |   23544    84730 |   18352   12282  1958939   159.5 |  3.696 % |
c |    197169 |   23544    84730 |   20187   13990  2104889   150.5 |  3.696 % |
c |    199732 |   23544    84730 |   22206   16553  2249501   135.9 |  3.696 % |
c |    203577 |   23544    84730 |   24426   20398  2435214   119.4 |  3.696 % |
c |    209343 |   23544    84730 |   26869   26164  3178863   121.5 |  3.696 % |
c |    217993 |   23544    84730 |   29556   19962  2052066   102.8 |  3.696 % |
c |    230967 |   23544    84730 |   32512   32936  3426948   104.0 |  3.696 % |
c |    250428 |   23544    84730 |   35763   33365  3391734   101.7 |  3.696 % |
c ==============================================================================
c (current CPU-time: 339.287 s)
c ==============================================================================
c [1mFound solution: 95[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1325   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    253444 |   23547    84746 |    7064   36381  3759459   103.3 |  3.696 % |
c   -- subsuming                       
c   -- var.elim.:  12/12          
c   -- var.elim.:  8/8          
c |    253444 |   23542    84702 |      --   36381       --      -- |     --   | -5/-43
c |    253444 |   23542    84702 |    9416   36381  3759459   103.3 |  3.696 % |
c |    253544 |   23542    84702 |   10358    6886   561344    81.5 |  3.713 % |
c |    253694 |   23542    84702 |   11394    7036   562315    79.9 |  3.713 % |
c |    253922 |   23542    84702 |   12533    7264   568278    78.2 |  3.713 % |
c |    254260 |   23542    84702 |   13787    7602   570182    75.0 |  3.713 % |
c |    254767 |   23542    84702 |   15165    8109   589837    72.7 |  3.713 % |
c ==============================================================================
c (current CPU-time: 342.124 s)
c ==============================================================================
c [1mFound solution: 94[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1326   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    255414 |   23545    84719 |    7063    8756   607549    69.4 |  3.713 % |
c   -- subsuming                       
c   -- var.elim.:  12/12          
c   -- var.elim.:  11/11          
c |    255414 |   23544    84724 |      --    8756       --      -- |     --   | -1/6
c |    255414 |   23544    84724 |    9417    8756   607549    69.4 |  3.713 % |
c |    255515 |   23544    84724 |   10359    8857   608380    68.7 |  3.729 % |
c |    255668 |   23544    84724 |   11395    9010   609672    67.7 |  3.729 % |
c |    255894 |   23544    84724 |   12534    9236   616573    66.8 |  3.729 % |
c |    256231 |   23544    84724 |   13788    9573   626702    65.5 |  3.729 % |
c |    256738 |   23544    84724 |   15167   10080   647266    64.2 |  3.729 % |
c |    257499 |   23544    84724 |   16683   10841   668215    61.6 |  3.729 % |
c |    258638 |   23544    84724 |   18352   11980   710228    59.3 |  3.729 % |
c |    260346 |   23544    84724 |   20187   13688   809239    59.1 |  3.729 % |
c |    262908 |   23544    84724 |   22206   16250  1013286    62.4 |  3.729 % |
c |    266752 |   23544    84724 |   24426   20094  1329530    66.2 |  3.729 % |
c |    272519 |   23544    84724 |   26869   25861  1809628    70.0 |  3.729 % |
c |    281168 |   23544    84724 |   29556   19567  2196746   112.3 |  3.729 % |
c |    294142 |   23544    84724 |   32512   14594  1471629   100.8 |  3.729 % |
c |    313603 |   23544    84724 |   35763   34055  5501636   161.6 |  3.729 % |
c |    342797 |   23544    84724 |   39339   15572  2642387   169.7 |  3.729 % |
c ==============================================================================
c (current CPU-time: 470.96 s)
c ==============================================================================
c [1mFound solution: 92[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1328   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    350876 |   23548    84748 |    7064   23651  3213083   135.9 |  3.729 % |
c   -- subsuming                       
c   -- var.elim.:  12/12          
c   -- var.elim.:  10/10          
c |    350876 |   23545    84728 |      --   23651       --      -- |     --   | -1/4
c |    350876 |   23545    84728 |    9418   23651  3213083   135.9 |  3.729 % |
c |    350976 |   23545    84728 |   10359    6600   463875    70.3 |  3.762 % |
c |    351126 |   23545    84728 |   11395    6750   464575    68.8 |  3.762 % |
c |    351351 |   23545    84728 |   12535    6975   465831    66.8 |  3.762 % |
c |    351688 |   23545    84728 |   13788    7312   471759    64.5 |  3.762 % |
c |    352196 |   23545    84728 |   15167    7820   475929    60.9 |  3.762 % |
c |    352955 |   23545    84728 |   16684    8579   493728    57.6 |  3.762 % |
c |    354094 |   23545    84728 |   18353    9718   542138    55.8 |  3.762 % |
c |    355802 |   23545    84728 |   20188   11426   640709    56.1 |  3.762 % |
c |    358367 |   23545    84728 |   22207   13991   736559    52.6 |  3.762 % |
c |    362211 |   23545    84728 |   24427   17835   969268    54.3 |  3.762 % |
c |    367977 |   23545    84728 |   26870   23601  1665747    70.6 |  3.762 % |
c ==============================================================================
c (current CPU-time: 488.457 s)
c ==============================================================================
c [1mFound solution: 83[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1337   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    369760 |   23549    84752 |    7064   25384  1770880    69.8 |  3.762 % |
c   -- subsuming                       
c   -- var.elim.:  12/12          
c   -- var.elim.:  7/7          
c |    369760 |   23542    84700 |      --   25384       --      -- |     --   | -7/-50
c |    369760 |   23542    84700 |    9416   25384  1770880    69.8 |  3.762 % |
c |    369860 |   23542    84700 |   10358    9438   782851    82.9 |  3.795 % |
c |    370011 |   23542    84700 |   11394    9589   783750    81.7 |  3.795 % |
c |    370236 |   23542    84700 |   12533    9814   789447    80.4 |  3.795 % |
c |    370574 |   23542    84700 |   13787   10152   793640    78.2 |  3.795 % |
c ==============================================================================
c (current CPU-time: 490.291 s)
c ==============================================================================
c [1mFound solution: 80[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1340   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    371063 |   23548    84730 |    7064   10641   816227    76.7 |  3.795 % |
c   -- subsuming                       
c   -- var.elim.:  14/14          
c   -- var.elim.:  11/11          
c |    371063 |   23545    84730 |      --   10641       --      -- |     --   | -3/2
c |    371063 |   23545    84730 |    9418   10641   816227    76.7 |  3.795 % |
c |    371163 |   23545    84730 |   10359    7194   387725    53.9 |  3.828 % |
c |    371313 |   23545    84730 |   11395    7344   388900    53.0 |  3.828 % |
c |    371538 |   23545    84730 |   12535    7569   391439    51.7 |  3.828 % |
c |    371875 |   23545    84730 |   13788    7906   402769    50.9 |  3.828 % |
c |    372381 |   23545    84730 |   15167    8412   429458    51.1 |  3.828 % |
c |    373140 |   23545    84730 |   16684    9171   466147    50.8 |  3.828 % |
c |    374279 |   23545    84730 |   18353   10310   507806    49.3 |  3.828 % |
c |    375987 |   23545    84730 |   20188   12018   583236    48.5 |  3.828 % |
c |    378551 |   23545    84730 |   22207   14582   775299    53.2 |  3.828 % |
c |    382395 |   23545    84730 |   24427   18426  1208598    65.6 |  3.828 % |
c |    388161 |   23545    84730 |   26870   24192  1840008    76.1 |  3.828 % |
c |    396810 |   23545    84730 |   29557   17831  2041343   114.5 |  3.828 % |
c |    409784 |   23545    84730 |   32513   30805  3842611   124.7 |  3.828 % |
c |    429245 |   23545    84730 |   35764   29650  5217740   176.0 |  3.828 % |
c |    458439 |   23545    84730 |   39341   32210  3576757   111.0 |  3.828 % |
c |    502229 |   23545    84730 |   43275   23820  5420710   227.6 |  3.828 % |
c |    567913 |   23545    84730 |   47603   22969  4104256   178.7 |  3.828 % |
c |    666439 |   23545    84730 |   52363   49728 10314330   207.4 |  3.828 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v785 v740 v420 v82 v860 -v744 v418 v859 -v784 -v501 v307 -v85 -v788 v419 -v86 -v63 v861 -v504 v424 -v354 v306 -v62 -v863 -v789 v573 -v505 v64 v572 -v478 -v441 -v353 v312 v65 -v27 -v864 v574 -v477 v310 -v102 v66 -v866 -v810 v575 v479 -v440 -v359 -v262 -v185 -v101 v73 -v26 -v867 -v814 v576 v482 -v357 v311 -v190 -v107 -v67 -v30 -v697 v583 v481 -v446 -v399 -v315 -v265 -v216 -v189 v143 -v106 -v68 -v701 v577 v486 -v444 -v358 -v266 v142 -v108 -v69 -v31 -v2 v578 v485 -v398 -v362 -v192 -v166 v144 -v112 v1 -v660 v579 -v483 -v445 -v193 v147 -v111 v7 v659 -v594 -v558 -v484 -v449 -v404 -v196 -v165 v146 -v109 v6 v661 -v598 -v557 -v402 -v194 v151 -v110 v8 v662 v559 -v332 -v195 -v171 v150 v12 v663 v562 -v403 -v169 v148 v11 v668 v561 -v407 -v335 v149 v9 v664 v563 -v336 -v170 v10 v739 v421 v81 v855 -v743 v854 v786 -v500 v425 -v302 -v87 v790 v423 v862 v506 -v349 v308 -v865 -v869 -v835 v792 v436 -v355 v313 -v90 v76 -v868 -v839 v793 v77 -v809 v586 v50#### 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.92 0.95 0.90 2/54 4619
Raw data (stat): 4619 (runsolver) R 4618 30701 30700 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 422394890 1052672 97 4294967295 134512640 135381576 3221224448 3221219820 135024789 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+9.99978 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 3770 0 0 0 988 10 0 0 25 0 1 0 422394890 13430784 2718 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3279 2718 603 41 0 3238 0
vsize: 13116
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 4641 0 0 0 1987 12 0 0 25 0 1 0 422394890 16580608 3484 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4048 3484 603 41 0 4007 0
vsize: 16192
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 5470 0 0 0 2985 14 0 0 25 0 1 0 422394890 19947520 4313 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4870 4313 603 41 0 4829 0
vsize: 19480
[startup+40.0004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 6197 0 0 0 3983 16 0 0 25 0 1 0 422394890 22863872 5040 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5582 5040 603 41 0 5541 0
vsize: 22328
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 7047 0 0 0 4981 18 0 0 25 0 1 0 422394890 26341376 5890 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6431 5890 603 41 0 6390 0
vsize: 25724
[startup+60.0007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 7062 0 0 0 5981 18 0 0 25 0 1 0 422394890 26472448 5905 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6463 5905 603 41 0 6422 0
vsize: 25852
[startup+70.0014 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 8097 0 0 0 6978 22 0 0 25 0 1 0 422394890 30842880 6940 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7530 6940 603 41 0 7489 0
vsize: 30120
[startup+80.0013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 8504 0 0 0 7977 23 0 0 25 0 1 0 422394890 32276480 7311 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7311 603 41 0 7839 0
vsize: 31520
[startup+90.0017 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 8504 0 0 0 8977 23 0 0 25 0 1 0 422394890 32276480 7311 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7311 603 41 0 7839 0
vsize: 31520
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 8504 0 0 0 9977 23 0 0 25 0 1 0 422394890 32276480 7311 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7311 603 41 0 7839 0
vsize: 31520
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 8873 0 0 0 10976 24 0 0 25 0 1 0 422394890 33886208 7680 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8273 7680 603 41 0 8232 0
vsize: 33092
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 9538 0 0 0 11974 27 0 0 25 0 1 0 422394890 36540416 8345 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8921 8345 603 41 0 8880 0
vsize: 35684
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10100 0 0 0 12973 28 0 0 25 0 1 0 422394890 38621184 8867 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9429 8867 603 41 0 9388 0
vsize: 37716
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10100 0 0 0 13973 28 0 0 25 0 1 0 422394890 38621184 8867 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9429 8867 603 41 0 9388 0
vsize: 37716
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10100 0 0 0 14973 28 0 0 25 0 1 0 422394890 38621184 8867 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9429 8867 603 41 0 9388 0
vsize: 37716
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10102 0 0 0 15974 28 0 0 25 0 1 0 422394890 38621184 8869 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9429 8869 603 41 0 9388 0
vsize: 37716
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10151 0 0 0 16974 28 0 0 25 0 1 0 422394890 38592512 8868 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8868 603 41 0 9381 0
vsize: 37688
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10151 0 0 0 17974 28 0 0 25 0 1 0 422394890 38592512 8868 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8868 603 41 0 9381 0
vsize: 37688
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10151 0 0 0 18974 28 0 0 25 0 1 0 422394890 38592512 8868 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8868 603 41 0 9381 0
vsize: 37688
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10151 0 0 0 19974 28 0 0 25 0 1 0 422394890 38592512 8868 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8868 603 41 0 9381 0
vsize: 37688
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10151 0 0 0 20974 28 0 0 25 0 1 0 422394890 38592512 8868 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8868 603 41 0 9381 0
vsize: 37688
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10192 0 0 0 21975 28 0 0 25 0 1 0 422394890 38854656 8909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9486 8909 603 41 0 9445 0
vsize: 37944
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10192 0 0 0 22975 28 0 0 25 0 1 0 422394890 38854656 8909 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9486 8909 603 41 0 9445 0
vsize: 37944
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10192 0 0 0 23975 28 0 0 25 0 1 0 422394890 38854656 8909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9486 8909 603 41 0 9445 0
vsize: 37944
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10192 0 0 0 24975 28 0 0 25 0 1 0 422394890 38854656 8909 4294967295 134512640 134672761 3221224544 3221223744 134610669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9486 8909 603 41 0 9445 0
vsize: 37944
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 10571 0 0 0 25974 29 0 0 25 0 1 0 422394890 40431616 9288 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9871 9288 603 41 0 9830 0
vsize: 39484
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 11603 0 0 0 26972 31 0 0 25 0 1 0 422394890 44646400 10320 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10900 10320 603 41 0 10859 0
vsize: 43600
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12285 0 0 0 27970 33 0 0 25 0 1 0 422394890 46981120 10896 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11470 10896 603 41 0 11429 0
vsize: 45880
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12285 0 0 0 28969 33 0 0 25 0 1 0 422394890 46981120 10896 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11470 10896 603 41 0 11429 0
vsize: 45880
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12285 0 0 0 29969 33 0 0 25 0 1 0 422394890 46981120 10896 4294967295 134512640 134672761 3221224544 3221223680 134614664 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11470 10896 603 41 0 11429 0
vsize: 45880
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12285 0 0 0 30969 33 0 0 25 0 1 0 422394890 46981120 10896 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11470 10896 603 41 0 11429 0
vsize: 45880
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12285 0 0 0 31970 33 0 0 25 0 1 0 422394890 46981120 10896 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11470 10896 603 41 0 11429 0
vsize: 45880
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12285 0 0 0 32970 33 0 0 25 0 1 0 422394890 46981120 10896 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11470 10896 603 41 0 11429 0
vsize: 45880
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12285 0 0 0 33970 33 0 0 25 0 1 0 422394890 46477312 10773 4294967295 134512640 134672761 3221224544 3221223800 134616178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11347 10773 603 41 0 11306 0
vsize: 45388
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 34969 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 35970 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 36970 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 37970 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 38970 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 39970 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 40970 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 41971 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 42971 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 43971 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 44971 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223416 1075352732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 45971 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 46972 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12323 0 0 0 47971 34 0 0 25 0 1 0 422394890 46477312 10775 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10775 603 41 0 11306 0
vsize: 45388
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 48971 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 49971 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223680 134614688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+510.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 50971 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 51971 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 52972 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 53972 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223584 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 54972 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 55972 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 56972 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 57973 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12324 0 0 0 58973 34 0 0 25 0 1 0 422394890 46477312 10776 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10776 603 41 0 11306 0
vsize: 45388
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12325 0 0 0 59973 34 0 0 25 0 1 0 422394890 46477312 10777 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10777 603 41 0 11306 0
vsize: 45388
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12325 0 0 0 60973 34 0 0 25 0 1 0 422394890 46477312 10777 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10777 603 41 0 11306 0
vsize: 45388
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12325 0 0 0 61973 34 0 0 25 0 1 0 422394890 46477312 10777 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10777 603 41 0 11306 0
vsize: 45388
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12325 0 0 0 62974 34 0 0 25 0 1 0 422394890 46477312 10777 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10777 603 41 0 11306 0
vsize: 45388
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12325 0 0 0 63974 34 0 0 25 0 1 0 422394890 46477312 10777 4294967295 134512640 134672761 3221224544 3221223808 134618040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10777 603 41 0 11306 0
vsize: 45388
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12325 0 0 0 64974 34 0 0 25 0 1 0 422394890 46477312 10777 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10777 603 41 0 11306 0
vsize: 45388
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12325 0 0 0 65974 34 0 0 25 0 1 0 422394890 46477312 10777 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10777 603 41 0 11306 0
vsize: 45388
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12325 0 0 0 66974 34 0 0 25 0 1 0 422394890 46477312 10777 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10777 603 41 0 11306 0
vsize: 45388
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12325 0 0 0 67975 34 0 0 25 0 1 0 422394890 46477312 10777 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11347 10777 603 41 0 11306 0
vsize: 45388
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12426 0 0 0 68975 35 0 0 25 0 1 0 422394890 46718976 10836 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10836 603 41 0 11365 0
vsize: 45624
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12426 0 0 0 69975 35 0 0 25 0 1 0 422394890 46718976 10836 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10836 603 41 0 11365 0
vsize: 45624
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12426 0 0 0 70975 35 0 0 25 0 1 0 422394890 46718976 10836 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10836 603 41 0 11365 0
vsize: 45624
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12426 0 0 0 71975 35 0 0 25 0 1 0 422394890 46718976 10836 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11406 10836 603 41 0 11365 0
vsize: 45624
[startup+730.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 12506 0 0 0 72975 35 0 0 25 0 1 0 422394890 47116288 10916 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11503 10916 603 41 0 11462 0
vsize: 46012
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13232 0 0 0 73974 37 0 0 25 0 1 0 422394890 50032640 11642 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12215 11642 603 41 0 12174 0
vsize: 48860
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13776 0 0 0 74972 38 0 0 25 0 1 0 422394890 52199424 12170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12744 12170 603 41 0 12703 0
vsize: 50976
[startup+760.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13776 0 0 0 75972 38 0 0 25 0 1 0 422394890 52199424 12170 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12744 12170 603 41 0 12703 0
vsize: 50976
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13776 0 0 0 76972 38 0 0 25 0 1 0 422394890 52199424 12170 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12744 12170 603 41 0 12703 0
vsize: 50976
[startup+780.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13776 0 0 0 77972 38 0 0 25 0 1 0 422394890 52199424 12170 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12744 12170 603 41 0 12703 0
vsize: 50976
[startup+790.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13776 0 0 0 78973 38 0 0 25 0 1 0 422394890 52199424 12170 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12744 12170 603 41 0 12703 0
vsize: 50976
[startup+800.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13776 0 0 0 79973 38 0 0 25 0 1 0 422394890 52199424 12170 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12744 12170 603 41 0 12703 0
vsize: 50976
[startup+810.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13776 0 0 0 80973 38 0 0 25 0 1 0 422394890 52199424 12170 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12744 12170 603 41 0 12703 0
vsize: 50976
[startup+820.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13776 0 0 0 81973 38 0 0 25 0 1 0 422394890 52199424 12170 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12744 12170 603 41 0 12703 0
vsize: 50976
[startup+830.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13823 0 0 0 82973 38 0 0 25 0 1 0 422394890 52158464 12160 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12160 603 41 0 12693 0
vsize: 50936
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13823 0 0 0 83974 38 0 0 25 0 1 0 422394890 52158464 12160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12160 603 41 0 12693 0
vsize: 50936
[startup+850.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13823 0 0 0 84974 38 0 0 25 0 1 0 422394890 52158464 12160 4294967295 134512640 134672761 3221224544 3221223712 134564752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12160 603 41 0 12693 0
vsize: 50936
[startup+860.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13823 0 0 0 85974 38 0 0 25 0 1 0 422394890 52158464 12160 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12160 603 41 0 12693 0
vsize: 50936
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13823 0 0 0 86974 38 0 0 25 0 1 0 422394890 52158464 12160 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12160 603 41 0 12693 0
vsize: 50936
[startup+880.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13823 0 0 0 87974 38 0 0 25 0 1 0 422394890 52158464 12160 4294967295 134512640 134672761 3221224544 3221223680 134614710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12160 603 41 0 12693 0
vsize: 50936
[startup+890.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13827 0 0 0 88974 38 0 0 25 0 1 0 422394890 52158464 12164 4294967295 134512640 134672761 3221224544 3221223600 134645493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12164 603 41 0 12693 0
vsize: 50936
[startup+900.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13827 0 0 0 89975 38 0 0 25 0 1 0 422394890 52158464 12164 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12164 603 41 0 12693 0
vsize: 50936
[startup+910.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13827 0 0 0 90975 38 0 0 25 0 1 0 422394890 52158464 12164 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12164 603 41 0 12693 0
vsize: 50936
[startup+920.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13827 0 0 0 91975 39 0 0 25 0 1 0 422394890 52158464 12164 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12164 603 41 0 12693 0
vsize: 50936
[startup+930.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13827 0 0 0 92975 39 0 0 25 0 1 0 422394890 52158464 12164 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12164 603 41 0 12693 0
vsize: 50936
[startup+940.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13827 0 0 0 93975 39 0 0 25 0 1 0 422394890 52158464 12164 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12164 603 41 0 12693 0
vsize: 50936
[startup+950.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13827 0 0 0 94976 39 0 0 25 0 1 0 422394890 52158464 12164 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12164 603 41 0 12693 0
vsize: 50936
[startup+960.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13827 0 0 0 95976 39 0 0 25 0 1 0 422394890 52158464 12164 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12164 603 41 0 12693 0
vsize: 50936
[startup+970.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 13827 0 0 0 96976 39 0 0 25 0 1 0 422394890 52158464 12164 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12734 12164 603 41 0 12693 0
vsize: 50936
[startup+980.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 14063 0 0 0 97976 39 0 0 25 0 1 0 422394890 52920320 12350 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12920 12350 603 41 0 12879 0
vsize: 51680
[startup+990.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 14063 0 0 0 98976 39 0 0 25 0 1 0 422394890 52920320 12350 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12920 12350 603 41 0 12879 0
vsize: 51680
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 14063 0 0 0 99976 39 0 0 25 0 1 0 422394890 52920320 12350 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12920 12350 603 41 0 12879 0
vsize: 51680
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 14063 0 0 0 100976 39 0 0 25 0 1 0 422394890 52920320 12350 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12920 12350 603 41 0 12879 0
vsize: 51680
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 14063 0 0 0 101976 39 0 0 25 0 1 0 422394890 52920320 12350 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12920 12350 603 41 0 12879 0
vsize: 51680
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 14063 0 0 0 102976 39 0 0 25 0 1 0 422394890 52920320 12350 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12920 12350 603 41 0 12879 0
vsize: 51680
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 14063 0 0 0 103977 39 0 0 25 0 1 0 422394890 52920320 12350 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12920 12350 603 41 0 12879 0
vsize: 51680
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 14538 0 0 0 104975 40 0 0 25 0 1 0 422394890 54890496 12825 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13401 12825 603 41 0 13360 0
vsize: 53604
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 15253 0 0 0 105974 43 0 0 25 0 1 0 422394890 57802752 13540 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14112 13540 603 41 0 14071 0
vsize: 56448
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 15746 0 0 0 106973 44 0 0 25 0 1 0 422394890 59908096 14033 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14626 14033 603 41 0 14585 0
vsize: 58504
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 16251 0 0 0 107972 45 0 0 25 0 1 0 422394890 61906944 14538 4294967295 134512640 134672761 3221224544 3221223680 134614699 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15114 14538 603 41 0 15073 0
vsize: 60456
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17118 0 0 0 108970 47 0 0 25 0 1 0 422394890 65478656 15405 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15986 15405 603 41 0 15945 0
vsize: 63944
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17228 0 0 0 109969 47 0 0 25 0 1 0 422394890 65773568 15491 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15491 603 41 0 16017 0
vsize: 64232
[startup+1110.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17228 0 0 0 110970 47 0 0 25 0 1 0 422394890 65773568 15491 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15491 603 41 0 16017 0
vsize: 64232
[startup+1120.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17228 0 0 0 111970 47 0 0 25 0 1 0 422394890 65773568 15491 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15491 603 41 0 16017 0
vsize: 64232
[startup+1130.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17228 0 0 0 112970 47 0 0 25 0 1 0 422394890 65773568 15491 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15491 603 41 0 16017 0
vsize: 64232
[startup+1140.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17228 0 0 0 113970 47 0 0 25 0 1 0 422394890 65773568 15491 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15491 603 41 0 16017 0
vsize: 64232
[startup+1150.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17228 0 0 0 114970 47 0 0 25 0 1 0 422394890 65773568 15491 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15491 603 41 0 16017 0
vsize: 64232
[startup+1160.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17228 0 0 0 115971 47 0 0 25 0 1 0 422394890 65773568 15491 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15491 603 41 0 16017 0
vsize: 64232
[startup+1170.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17228 0 0 0 116971 47 0 0 25 0 1 0 422394890 65773568 15491 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15491 603 41 0 16017 0
vsize: 64232
[startup+1180.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17228 0 0 0 117971 47 0 0 25 0 1 0 422394890 65773568 15491 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15491 603 41 0 16017 0
vsize: 64232
[startup+1190.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17228 0 0 0 118971 47 0 0 25 0 1 0 422394890 65773568 15491 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16058 15491 603 41 0 16017 0
vsize: 64232
[startup+1200.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 4619
Raw data (stat): 4619 (minisat+) R 4618 30701 30700 0 -1 0 17903 0 0 0 119969 50 0 0 25 0 1 0 422394890 68542464 16166 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16734 16166 603 41 0 16693 0
vsize: 66936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.01 0.99 0.91 1/54 4619
Raw data (stat): 4619 (minisat+) Z 4618 30701 30700 0 -1 12 17904 0 0 0 119969 53 0 0 25 0 1 0 422394890 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.05
CPU time (s): 1200.23
CPU user time (s): 1199.69
CPU system time (s): 0.536918
CPU usage (%): 100.015
Max. virtual memory (Kb): 66936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####