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 5315

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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:      1034724 kB
MemFree:        711380 kB
Buffers:         34188 kB
Cached:         177712 kB
SwapCached:       1212 kB
Active:         144132 kB
Inactive:       148136 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        711124 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2244 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25296 kB
Committed_AS:   173996 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:41:22 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 3755 7 1200.25 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]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 186]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 185]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 184]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 183]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 182]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 181]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 180]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 179]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 178]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 177]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 176]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 175]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 174]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 173]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 172]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 171]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 170]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 169]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 168]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 167]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 166]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 165]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 164]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 163]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 162]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 161]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 160]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 159]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 158]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 157]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 156]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 155]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 154]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 153]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 152]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 151]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 150]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 149]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 148]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 147]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 146]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 145]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 144]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 143]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 142]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 141]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 140]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 139]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 138]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 137]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 136]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 135]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 134]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 133]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 132]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 131]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 130]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 129]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 128]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 127]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 126]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 125]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 124]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 123]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 122]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 121]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 120]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 119]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 118]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 117]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 116]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 115]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 114]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 113]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 111]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 110]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 109]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 108]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 107]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 106]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 104]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 103]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 102]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 101]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  99]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  98]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  97]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  96]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  94]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  93]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  91]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  89]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  88]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  87]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  86]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  82]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  73]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  72]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  70]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  69]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  68]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  67]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  66]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  65]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  64]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  63]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  62]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  61]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  60]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[  59]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  58]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  56]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  54]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  53]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  52]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  51]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  45]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  43]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  42]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  40]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  39]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  38]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  36]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  35]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  34]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  33]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  32]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  31]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  30]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  29]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  28]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  27]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  26]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  25]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  24]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  23]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  21]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  20]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  19]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  18]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  17]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  14]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  13]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  12]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  11]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  10]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   9]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   8]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   7]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   6]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   5]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   4]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   3]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   2]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   1]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   0]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   16898    58469 |    5632       0        0     nan |  0.000 % |
c |       100 |   16898    58469 |    6195     100      432     4.3 |  9.068 % |
c |       251 |   16898    58469 |    6814     251     1087     4.3 |  9.068 % |
c |       476 |   16892    58452 |    7496     475     2062     4.3 |  9.093 % |
c ==============================================================================
c [1mFound solution: 235[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2182   maxlim: 1185   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       625 |   32115   112809 |   10705     624     2891     4.6 |  9.093 % |
c |       726 |   32115   112809 |   11775     725     3570     4.9 |  5.965 % |
c |       876 |   32115   112809 |   12953     875     4204     4.8 |  5.965 % |
c |      1101 |   32115   112809 |   14248    1100     5584     5.1 |  5.965 % |
c |      1438 |   32115   112809 |   15673    1437     7599     5.3 |  5.965 % |
c |      1944 |   32115   112809 |   17240    1943    11306     5.8 |  5.965 % |
c ==============================================================================
c [1mFound solution: 228[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1192   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2548 |   32123   112850 |   10707    2547    18427     7.2 |  5.965 % |
c |      2648 |   32123   112850 |   11777    2647    18832     7.1 |  5.994 % |
c |      2798 |   32123   112850 |   12955    2797    19500     7.0 |  5.994 % |
c |      3023 |   32123   112850 |   14251    3022    20689     6.8 |  5.994 % |
c |      3360 |   32123   112850 |   15676    3359    23122     6.9 |  5.994 % |
c |      3866 |   32123   112850 |   17243    3865    26534     6.9 |  5.994 % |
c ==============================================================================
c [1mFound solution: 185[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1235   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3919 |   32132   112893 |   10710    3918    26890     6.9 |  5.994 % |
c ==============================================================================
c [1mFound solution: 123[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1297   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4002 |   32140   112931 |   10713    4001    27798     6.9 |  5.994 % |
c |      4102 |   32140   112931 |   11784    4101    28488     6.9 |  6.083 % |
c |      4254 |   32140   112931 |   12962    4253    30940     7.3 |  6.083 % |
c |      4479 |   32140   112931 |   14259    4478    32814     7.3 |  6.083 % |
c |      4816 |   32140   112931 |   15684    4815    35109     7.3 |  6.083 % |
c |      5322 |   32140   112931 |   17253    5321    51598     9.7 |  6.083 % |
c |      6081 |   32131   112900 |   18978    6076    67905    11.2 |  6.100 % |
c |      7220 |   32131   112900 |   20876    7215    90213    12.5 |  6.100 % |
c ==============================================================================
c [1mFound solution: 115[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1305   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7761 |   32133   112918 |   10711    7756   103292    13.3 |  6.100 % |
c |      7861 |   32133   112918 |   11782    7856   104519    13.3 |  6.130 % |
c |      8011 |   32133   112918 |   12960    8006   105535    13.2 |  6.130 % |
c |      8236 |   32133   112918 |   14256    8231   107331    13.0 |  6.130 % |
c |      8573 |   32133   112918 |   15681    8568   114487    13.4 |  6.130 % |
c |      9079 |   32133   112918 |   17250    9074   120490    13.3 |  6.130 % |
c |      9839 |   32133   112918 |   18975    9834   146663    14.9 |  6.130 % |
c |     10978 |   32133   112918 |   20872   10973   221161    20.2 |  6.130 % |
c |     12686 |   32133   112918 |   22959   12681   294612    23.2 |  6.130 % |
c ==============================================================================
c [1mFound solution: 99[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1321   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12813 |   32138   112946 |   10712   12808   295991    23.1 |  6.130 % |
c |     12913 |   32138   112946 |   11783    6504   193929    29.8 |  6.173 % |
c |     13063 |   32138   112946 |   12961    6654   195045    29.3 |  6.173 % |
c |     13288 |   32138   112946 |   14257    6879   196836    28.6 |  6.173 % |
c |     13628 |   32138   112946 |   15683    7219   205835    28.5 |  6.173 % |
c |     14135 |   32138   112946 |   17251    7726   221064    28.6 |  6.173 % |
c |     14894 |   32138   112946 |   18976    8485   241018    28.4 |  6.173 % |
c ==============================================================================
c [1mFound solution: 98[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1322   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15241 |   32141   112963 |   10713    8832   253597    28.7 |  6.173 % |
c |     15341 |   32141   112963 |   11784    8932   256798    28.8 |  6.188 % |
c |     15492 |   32141   112963 |   12962    9083   258441    28.5 |  6.188 % |
c |     15717 |   32141   112963 |   14259    9308   271005    29.1 |  6.188 % |
c |     16055 |   32141   112963 |   15684    9646   282826    29.3 |  6.188 % |
c |     16561 |   32141   112963 |   17253   10152   300969    29.6 |  6.188 % |
c |     17327 |   32141   112963 |   18978   10918   337177    30.9 |  6.188 % |
c |     18466 |   32141   112963 |   20876   12057   393323    32.6 |  6.188 % |
c |     20175 |   32141   112963 |   22964   13766   486850    35.4 |  6.188 % |
c |     22737 |   32141   112963 |   25260   16328   671169    41.1 |  6.188 % |
c |     26582 |   32141   112963 |   27786   20173   889243    44.1 |  6.188 % |
c |     32349 |   32141   112963 |   30565   25940  1300866    50.1 |  6.188 % |
c |     40998 |   32141   112963 |   33621   17078   940306    55.1 |  6.188 % |
c |     53972 |   32141   112963 |   36984   30052  2358657    78.5 |  6.188 % |
c |     73433 |   32141   112963 |   40682   27207  2703757    99.4 |  6.188 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84795 |   32142   112972 |   10714   38569  3401313    88.2 |  6.188 % |
c |     84895 |   32142   112972 |   11785    7356   287203    39.0 |  6.203 % |
c |     85045 |   32142   112972 |   12963    7506   288801    38.5 |  6.203 % |
c |     85270 |   32142   112972 |   14260    7731   290300    37.6 |  6.203 % |
c |     85607 |   32142   112972 |   15686    8068   292706    36.3 |  6.203 % |
c |     86114 |   32142   112972 |   17255    8575   328716    38.3 |  6.203 % |
c |     86873 |   32142   112972 |   18980    9334   339540    36.4 |  6.203 % |
c |     88014 |   32142   112972 |   20878   10475   384024    36.7 |  6.203 % |
c |     89723 |   32142   112972 |   22966   12184   430539    35.3 |  6.203 % |
c |     92287 |   32142   112972 |   25263   14748   678369    46.0 |  6.203 % |
c |     96131 |   32142   112972 |   27789   18592   891311    47.9 |  6.203 % |
c |    101897 |   32142   112972 |   30568   24358  1278860    52.5 |  6.203 % |
c |    110547 |   32142   112972 |   33625   16792   816802    48.6 |  6.203 % |
c |    123522 |   32142   112972 |   36987   29767  2336264    78.5 |  6.203 % |
c ==============================================================================
c [1mFound solution: 93[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1327   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    125118 |   32143   112979 |   10714   31363  2388623    76.2 |  6.203 % |
c |    125219 |   32143   112979 |   11785    7406   468125    63.2 |  6.218 % |
c |    125369 |   32143   112979 |   12963    7556   468949    62.1 |  6.218 % |
c |    125594 |   32143   112979 |   14260    7781   470573    60.5 |  6.218 % |
c |    125931 |   32143   112979 |   15686    8118   473865    58.4 |  6.218 % |
c |    126437 |   32143   112979 |   17255    8624   485296    56.3 |  6.218 % |
c |    127196 |   32143   112979 |   18980    9383   494214    52.7 |  6.218 % |
c |    128335 |   32143   112979 |   20878   10522   533749    50.7 |  6.218 % |
c |    130044 |   32143   112979 |   22966   12231   576021    47.1 |  6.218 % |
c |    132606 |   32143   112979 |   25263   14793   775945    52.5 |  6.218 % |
c |    136450 |   32143   112979 |   27789   18637  1011010    54.2 |  6.218 % |
c |    142216 |   32143   112979 |   30568   24403  1450288    59.4 |  6.218 % |
c |    150866 |   32143   112979 |   33625   15321  1256179    82.0 |  6.218 % |
c |    163840 |   32143   112979 |   36987   28295  2285040    80.8 |  6.218 % |
c |    183303 |   32143   112979 |   40686   22576  1986887    88.0 |  6.218 % |
c |    212495 |   32143   112979 |   44755   21211  2004874    94.5 |  6.218 % |
c |    256284 |   32143   112979 |   49230   29788  3846549   129.1 |  6.218 % |
c |    321969 |   32143   112979 |   54153   20608  2875551   139.5 |  6.218 % |
c |    420495 |   32143   112979 |   59568   36502  9016139   247.0 |  6.218 % |
c |    568284 |   32143   112979 |   65525   45993  6620276   143.9 |  6.218 % |
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 -v509 -v442 v360 v316 -v261 -v212 v72 -v28 -v813 v587 v480 -v314 -v184 -v103 -v32 -v696 v582 v494 v447 -v394 v363 -v267 -v215 -v186 -v104 -v70 -v700 -v490 v361 -v191 v105 v580 -v489 v450 -v400 v188 -v161 v116 -v34 v448 v197 v145 -v35 -v3 -v593 -v542 v405 -v270 -v167 -v159 -v4 -v597 v155 v5 -v671 -v408 -v331 -v172 v154 v16 v672 v560 -v406 -v667 v571 -v466 v337 -v173 v567 v470 -v174 -v781 v741 v496 v422 v83 v745 -v426 v787 -v502 v88 v856 v791 -v301 v857 -v795 v747 -v507 -v303 v91 -v75 v858 -v794 v748 -v348 v309 v89 -v74 -v22 -v873 -v834 -v761 -v585 -v510 -v350 v305 v257 -v21 -v838 -v765 -v584 -v508 v435 v356 v317 v811 -v491 v437 v352 -v263 -v211 -v29 -v815 v493 -v443 v364 -v33 -v698 v439 -v268 -v217 -v119 -v71 -v37 -v702 v451 -v393 v187 v120 -v36 -v817 v581 -v538 -v487 -v395 -v271 -v205 -v156 v115 -v818 -v401 -v269 -v201 -v160 -v158 v704 -v670 -v595 -v541 -v488 v397 -v327 -v220 -v200 -v162 v113 v19 -v705 -v669 -v599 -v409 -v168 v20 -v722 v568 -v333 -v164 v152 v15 -v726 v570 -v175 -v665 -v601 -v465 v338 v153 -v131 v13 -v602 v566 v469 v742 v434 -v79 -v780 v746 v495 -v430 v84 -v782 v750 v497 -v429 v80 v783 v749 -v503 v92 v876 -v799 v499 v877 -v805 -v511 -v304 -v872 -v836 -v804 -v760 v325 -v207 -v840 -v764 -v692 -v492 -v351 v321 v256 -v23 -v884 -v870 v812 -v691 -v372 v320 v258 v213 -v118 -v24 -v888 -v816 v438 -v368 v264 -v117 v25 -v842 -v820 -v699 -v459 -v367 v260 -v218 -v202 v41 -v843 -v819 v703 -v589 v455 -v272 -v204 -v157 v707 -v588 -v537 v454 -v221 -v18 v706 -v396 -v219 v17 -v596 -v543 v417 -v198 -v114 v600 v569 -v413 -v326 -v163 -v721 -v604 -v412 -v328 -v199 -v183 -v127 -v725 -v603 -v334 -v179 -v666 v546 -v467 v330 -v178 -v130 -v14 v564 v471 v339 v903 v433 v78 v875 -v802 v754 -v427 v100 v874 -v830 -v803 v498 -v96 -v829 -v798 v519 -v428 -v322 -v95 v515 -v324 -v837 -v796 -v762 v514 -v369 -v841 -v806 -v766 -v371 -v206 -v883 -v871 -v845 v807 -v456 v318 -v291 -v208 -v44 -v887 -v844 v808 -v693 -v458 v259 v214 -v203 -v45 v824 v768 v694 -v533 -v383 -v365 v319 v280 v210 v40 v769 v695 v276 -v222 -v711 -v619 -v539 v452 v414 -v366 -v275 v38 -v623 -v590 v416 -v591 v544 -v453 -v180 v592 -v461 -v182 v723 v608 v547 -v460 -v410 -v126 -v727 v545 v329 -v468 -v411 v347 -v176 -v132 v565 v472 v343 -v801 v431 v97 -v800 v99 v753 v654 -v516 v756 -v518 -v323 v755 v751 -v521 -v93 -v831 -v525 -v370 -v832 -v797 v763 -v512 v287 -v249 -v94 -v43 -v833 -v767 -v457 -v42 -v885 -v849 v827 v771 -v513 -v379 -v290 -v277 -v889 v828 v770 v279 -v209 -v823 -v714 -v382 v230 v715 v532 -v415 v226 -v891 -v821 -v710 -v641 -v618 v534 -v273 v225 v39 -v892 -v717 -v645 -v622 v540 -v181 -v716 -v708 -v679 v611 v536 -v274 -v122 v55 -v683 v612 v548 v724 v607 -v344 -v128 v728 -v462 -v346 v729 v605 -v463 -v240 -v177 -v133 v730 v464 v342 v904 -v432 v98 -v517 v653 v752 -v520 -v245 -v879 v757 -v524 -v878 -v852 v826 v758 v286 -v248 -v853 v825 v759 -v278 -v886 -v848 v775 -v713 -v378 -v292 v227 -v890 -v712 v229 -v894 -v846 -v384 -v893 -v822 -v640 -v620 v610 -v295 v223 -v51 -v644 -v624 v609 v535 -v709 -v678 -v556 -v387 v224 v54 -v718 -v682 v552 -v345 -v121 -v719 -v626 -v551 -v236 v123 v720 -v627 -v129 v734 -v606 v47#### 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.84 0.94 0.90 1/53 12924
Raw data (stat): 12924 (runsolver) R 12923 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479864937 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.87 0.94 0.90 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 1384 0 0 0 994 4 0 0 25 0 1 0 479864937 7290880 1362 4294967295 134512640 134672761 3221224544 3221223696 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1780 1362 603 41 0 1739 0
vsize: 7120
[startup+20.0029 s]
Raw data (loadavg): 0.89 0.94 0.90 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 2188 0 0 0 1991 6 0 0 25 0 1 0 479864937 10534912 2166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2166 603 41 0 2531 0
vsize: 10288
[startup+30.0047 s]
Raw data (loadavg): 0.90 0.94 0.90 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 2966 0 0 0 2988 10 0 0 25 0 1 0 479864937 13766656 2944 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3361 2944 603 41 0 3320 0
vsize: 13444
[startup+40.0051 s]
Raw data (loadavg): 0.92 0.94 0.90 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 3067 0 0 0 3987 10 0 0 25 0 1 0 479864937 14172160 3045 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3460 3045 603 41 0 3419 0
vsize: 13840
[startup+50.0072 s]
Raw data (loadavg): 0.93 0.94 0.90 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 3859 0 0 0 4986 13 0 0 25 0 1 0 479864937 17514496 3837 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4276 3837 603 41 0 4235 0
vsize: 17104
[startup+60.008 s]
Raw data (loadavg): 0.94 0.95 0.90 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4331 0 0 0 5984 14 0 0 25 0 1 0 479864937 19402752 4309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4737 4309 603 41 0 4696 0
vsize: 18948
[startup+70.0094 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4331 0 0 0 6984 15 0 0 25 0 1 0 479864937 19402752 4309 4294967295 134512640 134672761 3221224544 3221223648 134560231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4737 4309 603 41 0 4696 0
vsize: 18948
[startup+80.0102 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4425 0 0 0 7984 15 0 0 25 0 1 0 479864937 19804160 4403 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4835 4403 603 41 0 4794 0
vsize: 19340
[startup+90.0109 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4899 0 0 0 8983 17 0 0 25 0 1 0 479864937 21798912 4877 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4877 603 41 0 5281 0
vsize: 21288
[startup+100.012 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4899 0 0 0 9983 17 0 0 25 0 1 0 479864937 21798912 4877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5322 4877 603 41 0 5281 0
vsize: 21288
[startup+110.013 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4899 0 0 0 10982 17 0 0 25 0 1 0 479864937 21798912 4877 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5322 4877 603 41 0 5281 0
vsize: 21288
[startup+120.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4899 0 0 0 11982 17 0 0 25 0 1 0 479864937 21798912 4877 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4877 603 41 0 5281 0
vsize: 21288
[startup+130.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4899 0 0 0 12982 17 0 0 25 0 1 0 479864937 21798912 4877 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4877 603 41 0 5281 0
vsize: 21288
[startup+140.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4899 0 0 0 13982 17 0 0 25 0 1 0 479864937 21798912 4877 4294967295 134512640 134672761 3221224544 3221223728 134559400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4877 603 41 0 5281 0
vsize: 21288
[startup+150.017 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4899 0 0 0 14982 17 0 0 25 0 1 0 479864937 21798912 4877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4877 603 41 0 5281 0
vsize: 21288
[startup+160.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4899 0 0 0 15983 17 0 0 25 0 1 0 479864937 21798912 4877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4877 603 41 0 5281 0
vsize: 21288
[startup+170.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4899 0 0 0 16982 18 0 0 25 0 1 0 479864937 21798912 4877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5322 4877 603 41 0 5281 0
vsize: 21288
[startup+180.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4975 0 0 0 17982 18 0 0 25 0 1 0 479864937 22069248 4953 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5388 4953 603 41 0 5347 0
vsize: 21552
[startup+190.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 4975 0 0 0 18982 18 0 0 25 0 1 0 479864937 22069248 4953 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5388 4953 603 41 0 5347 0
vsize: 21552
[startup+200.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 5089 0 0 0 19982 18 0 0 25 0 1 0 479864937 22605824 5067 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5519 5067 603 41 0 5478 0
vsize: 22076
[startup+210.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 5770 0 0 0 20980 20 0 0 25 0 1 0 479864937 25419776 5748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6206 5748 603 41 0 6165 0
vsize: 24824
[startup+220.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 6185 0 0 0 21979 22 0 0 25 0 1 0 479864937 27049984 6163 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6604 6163 603 41 0 6563 0
vsize: 26416
[startup+230.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 6185 0 0 0 22979 22 0 0 25 0 1 0 479864937 27049984 6163 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6604 6163 603 41 0 6563 0
vsize: 26416
[startup+240.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 6185 0 0 0 23978 22 0 0 25 0 1 0 479864937 27049984 6163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6604 6163 603 41 0 6563 0
vsize: 26416
[startup+250.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 6185 0 0 0 24979 22 0 0 25 0 1 0 479864937 27049984 6163 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6604 6163 603 41 0 6563 0
vsize: 26416
[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 6577 0 0 0 25978 23 0 0 25 0 1 0 479864937 28655616 6555 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6996 6556 603 41 0 6955 0
vsize: 27984
[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 7361 0 0 0 26976 25 0 0 25 0 1 0 479864937 31875072 7339 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7782 7339 603 41 0 7741 0
vsize: 31128
[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8043 0 0 0 27973 28 0 0 25 0 1 0 479864937 34684928 8021 4294967295 134512640 134672761 3221224544 3221223648 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8468 8021 603 41 0 8427 0
vsize: 33872
[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8085 0 0 0 28974 28 0 0 25 0 1 0 479864937 34820096 8063 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8501 8063 603 41 0 8460 0
vsize: 34004
[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8085 0 0 0 29974 28 0 0 25 0 1 0 479864937 34820096 8063 4294967295 134512640 134672761 3221224544 3221223544 1075349878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8501 8063 603 41 0 8460 0
vsize: 34004
[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8085 0 0 0 30973 28 0 0 25 0 1 0 479864937 34820096 8063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8501 8063 603 41 0 8460 0
vsize: 34004
[startup+320.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8085 0 0 0 31973 28 0 0 25 0 1 0 479864937 34820096 8063 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8501 8063 603 41 0 8460 0
vsize: 34004
[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8085 0 0 0 32973 28 0 0 25 0 1 0 479864937 34820096 8063 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8501 8063 603 41 0 8460 0
vsize: 34004
[startup+340.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8605 0 0 0 33973 29 0 0 25 0 1 0 479864937 36970496 8583 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9026 8583 603 41 0 8985 0
vsize: 36104
[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8837 0 0 0 34973 29 0 0 25 0 1 0 479864937 37916672 8815 4294967295 134512640 134672761 3221224544 3221223776 134541809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9257 8815 603 41 0 9216 0
vsize: 37028
[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8837 0 0 0 35973 29 0 0 25 0 1 0 479864937 37916672 8815 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9257 8815 603 41 0 9216 0
vsize: 37028
[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8837 0 0 0 36973 30 0 0 25 0 1 0 479864937 37916672 8815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9257 8815 603 41 0 9216 0
vsize: 37028
[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8838 0 0 0 37974 30 0 0 25 0 1 0 479864937 37916672 8816 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9257 8816 603 41 0 9216 0
vsize: 37028
[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 8838 0 0 0 38974 30 0 0 25 0 1 0 479864937 37916672 8816 4294967295 134512640 134672761 3221224544 3221223752 1075346913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9257 8816 603 41 0 9216 0
vsize: 37028
[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 9404 0 0 0 39973 31 0 0 25 0 1 0 479864937 40202240 9382 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9815 9382 603 41 0 9774 0
vsize: 39260
[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 10160 0 0 0 40971 33 0 0 25 0 1 0 479864937 43294720 10138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10570 10138 603 41 0 10529 0
vsize: 42280
[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 10625 0 0 0 41970 35 0 0 25 0 1 0 479864937 45178880 10603 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11030 10603 603 41 0 10989 0
vsize: 44120
[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 10625 0 0 0 42969 35 0 0 25 0 1 0 479864937 45178880 10603 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11030 10603 603 41 0 10989 0
vsize: 44120
[startup+440.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 10625 0 0 0 43969 35 0 0 25 0 1 0 479864937 45178880 10603 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11030 10603 603 41 0 10989 0
vsize: 44120
[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 10625 0 0 0 44969 35 0 0 25 0 1 0 479864937 45178880 10603 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11030 10603 603 41 0 10989 0
vsize: 44120
[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 10625 0 0 0 45969 35 0 0 25 0 1 0 479864937 45178880 10603 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11030 10603 603 41 0 10989 0
vsize: 44120
[startup+470.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 10625 0 0 0 46969 35 0 0 25 0 1 0 479864937 45178880 10603 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11030 10603 603 41 0 10989 0
vsize: 44120
[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 10625 0 0 0 47970 35 0 0 25 0 1 0 479864937 45178880 10603 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11030 10603 603 41 0 10989 0
vsize: 44120
[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 10625 0 0 0 48970 35 0 0 25 0 1 0 479864937 45178880 10603 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11030 10603 603 41 0 10989 0
vsize: 44120
[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 10625 0 0 0 49970 35 0 0 25 0 1 0 479864937 45178880 10603 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11030 10603 603 41 0 10989 0
vsize: 44120
[startup+510.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 11205 0 0 0 50969 36 0 0 25 0 1 0 479864937 47607808 11183 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11623 11183 603 41 0 11582 0
vsize: 46492
[startup+520.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 11897 0 0 0 51967 38 0 0 25 0 1 0 479864937 50429952 11875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12312 11875 603 41 0 12271 0
vsize: 49248
[startup+530.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 52965 39 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223648 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+540.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 53965 39 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223696 134559753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+550.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 54966 39 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 55966 39 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 56966 39 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 57966 39 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 58967 39 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 59967 39 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+610.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 60967 39 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+620.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 61967 40 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+630.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12405 0 0 0 62968 40 0 0 25 0 1 0 479864937 52572160 12383 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12835 12383 603 41 0 12794 0
vsize: 51340
[startup+640.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 12960 0 0 0 63966 41 0 0 25 0 1 0 479864937 54845440 12938 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13390 12938 603 41 0 13349 0
vsize: 53560
[startup+650.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 13552 0 0 0 64965 43 0 0 25 0 1 0 479864937 57249792 13530 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13977 13530 603 41 0 13936 0
vsize: 55908
[startup+660.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 14215 0 0 0 65964 44 0 0 25 0 1 0 479864937 59924480 14193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14630 14193 603 41 0 14589 0
vsize: 58520
[startup+670.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 14885 0 0 0 66963 46 0 0 25 0 1 0 479864937 62730240 14863 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15315 14863 603 41 0 15274 0
vsize: 61260
[startup+680.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15514 0 0 0 67961 47 0 0 25 0 1 0 479864937 65269760 15492 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15935 15492 603 41 0 15894 0
vsize: 63740
[startup+690.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15804 0 0 0 68961 48 0 0 25 0 1 0 479864937 66482176 15782 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15782 603 41 0 16190 0
vsize: 64924
[startup+700.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15804 0 0 0 69961 48 0 0 25 0 1 0 479864937 66482176 15782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15782 603 41 0 16190 0
vsize: 64924
[startup+710.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15804 0 0 0 70961 48 0 0 25 0 1 0 479864937 66482176 15782 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15782 603 41 0 16190 0
vsize: 64924
[startup+720.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15805 0 0 0 71961 48 0 0 25 0 1 0 479864937 66482176 15783 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15783 603 41 0 16190 0
vsize: 64924
[startup+730.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15805 0 0 0 72962 48 0 0 25 0 1 0 479864937 66482176 15783 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15783 603 41 0 16190 0
vsize: 64924
[startup+740.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15806 0 0 0 73962 48 0 0 25 0 1 0 479864937 66482176 15784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15784 603 41 0 16190 0
vsize: 64924
[startup+750.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15806 0 0 0 74962 48 0 0 25 0 1 0 479864937 66482176 15784 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15784 603 41 0 16190 0
vsize: 64924
[startup+760.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15806 0 0 0 75962 48 0 0 25 0 1 0 479864937 66482176 15784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16231 15784 603 41 0 16190 0
vsize: 64924
[startup+770.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15806 0 0 0 76962 48 0 0 25 0 1 0 479864937 66482176 15784 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15784 603 41 0 16190 0
vsize: 64924
[startup+780.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15806 0 0 0 77962 49 0 0 25 0 1 0 479864937 66482176 15784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15784 603 41 0 16190 0
vsize: 64924
[startup+790.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15809 0 0 0 78962 49 0 0 25 0 1 0 479864937 66482176 15787 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15787 603 41 0 16190 0
vsize: 64924
[startup+800.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 79963 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+810.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 80963 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+820.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 81963 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+830.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 82963 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+840.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 83964 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+850.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 84964 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+860.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 85964 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+870.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 86964 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+880.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 87965 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+890.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 88965 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223728 134558629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+900.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15811 0 0 0 89965 49 0 0 25 0 1 0 479864937 66482176 15789 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15789 603 41 0 16190 0
vsize: 64924
[startup+910.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15814 0 0 0 90965 49 0 0 25 0 1 0 479864937 66482176 15792 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16231 15792 603 41 0 16190 0
vsize: 64924
[startup+920.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15814 0 0 0 91965 49 0 0 25 0 1 0 479864937 66347008 15779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15779 603 41 0 16157 0
vsize: 64792
[startup+930.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15814 0 0 0 92966 49 0 0 25 0 1 0 479864937 66347008 15779 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15779 603 41 0 16157 0
vsize: 64792
[startup+940.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15814 0 0 0 93966 49 0 0 25 0 1 0 479864937 66347008 15779 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15779 603 41 0 16157 0
vsize: 64792
[startup+950.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15814 0 0 0 94966 49 0 0 25 0 1 0 479864937 66347008 15779 4294967295 134512640 134672761 3221224544 3221223648 134555237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15779 603 41 0 16157 0
vsize: 64792
[startup+960.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15814 0 0 0 95966 49 0 0 25 0 1 0 479864937 66347008 15779 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15779 603 41 0 16157 0
vsize: 64792
[startup+970.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15814 0 0 0 96967 49 0 0 25 0 1 0 479864937 66347008 15779 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15779 603 41 0 16157 0
vsize: 64792
[startup+980.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15814 0 0 0 97967 49 0 0 25 0 1 0 479864937 66347008 15779 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15779 603 41 0 16157 0
vsize: 64792
[startup+990.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 98967 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 99967 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 100968 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 101968 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 102968 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 103968 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 104969 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 105969 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 106969 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 107969 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 108969 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 109970 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 110970 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 111969 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15815 0 0 0 112970 49 0 0 25 0 1 0 479864937 66347008 15780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16198 15780 603 41 0 16157 0
vsize: 64792
[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15818 0 0 0 113970 49 0 0 25 0 1 0 479864937 66609152 15783 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16262 15783 603 41 0 16221 0
vsize: 65048
[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15820 0 0 0 114970 49 0 0 25 0 1 0 479864937 66600960 15783 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16260 15783 603 41 0 16219 0
vsize: 65040
[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15820 0 0 0 115970 49 0 0 25 0 1 0 479864937 66600960 15783 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16260 15783 603 41 0 16219 0
vsize: 65040
[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15820 0 0 0 116971 49 0 0 25 0 1 0 479864937 66600960 15783 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16260 15783 603 41 0 16219 0
vsize: 65040
[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15820 0 0 0 117971 49 0 0 25 0 1 0 479864937 66600960 15783 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16260 15783 603 41 0 16219 0
vsize: 65040
[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15820 0 0 0 118971 49 0 0 25 0 1 0 479864937 66600960 15783 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16260 15783 603 41 0 16219 0
vsize: 65040
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 12924
Raw data (stat): 12924 (minisat+) R 12923 7987 7986 0 -1 0 15820 0 0 0 119971 49 0 0 25 0 1 0 479864937 66600960 15783 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16260 15783 603 41 0 16219 0
vsize: 65040
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 12924
Raw data (stat): 12924 (minisat+) Z 12923 7987 7986 0 -1 12 15823 0 0 0 119971 53 0 0 25 0 1 0 479864937 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.15
CPU time (s): 1200.25
CPU user time (s): 1199.72
CPU system time (s): 0.532918
CPU usage (%): 100.009
Max. virtual memory (Kb): 65048
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####