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:100.opb
MD5SUM	f82b685b64af240616b701a750c82883
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10
Optimality of the best value was proved	NO
Number of terms in the objective function	934
Biggest coefficient in the objective function	546
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	2594
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	546
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	2594
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.03784
Number of variables	934
Total number of constraints	1996
Number of constraints which are clauses	879
Number of constraints which are cardinality constraints (but not clauses)	1117
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	20
Trace number 5309

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-13 23:19:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3751 boxname=wulflinc24 idbench=367 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f82b685b64af240616b701a750c82883  /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.95:100.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.95:100.opb /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.95:100.opb
IDLAUNCH: 3751
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        845240 kB
Buffers:         34040 kB
Cached:         113024 kB
SwapCached:       3828 kB
Active:          49760 kB
Inactive:       103968 kB
HighTotal:      131008 kB
HighFree:        15680 kB
LowTotal:       903652 kB
LowFree:        829560 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30048 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:39:10 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3751 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1062 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 190]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 189]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 188]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 187]---> Adder-cost: 11   maxlim: 2   bits: 3/2
c ---[ 186]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 185]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 184]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 183]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 182]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 181]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 180]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 179]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 178]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 177]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 176]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 175]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 174]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 173]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 172]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 171]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 170]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 169]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 168]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 167]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 166]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 165]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 164]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 163]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 162]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 161]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 160]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 159]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 158]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 156]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 155]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 154]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 153]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 152]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 151]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 150]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 149]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 148]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 147]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[ 146]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 145]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 144]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 143]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 142]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 141]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 140]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 138]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 136]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 135]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 134]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 133]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 132]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 131]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 130]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 129]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 128]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 127]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 126]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 125]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 124]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 123]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 122]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 121]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 120]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 118]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 117]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 116]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 115]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 114]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 113]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 111]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 110]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 109]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 108]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 107]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 106]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 104]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 103]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 102]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 101]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  99]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  98]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  97]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  96]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  94]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  93]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[  91]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[  89]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[  88]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  87]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  86]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  82]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  73]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  72]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[  70]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  69]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  68]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  67]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  66]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  65]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  64]---> Adder-cost: 22   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: 20   maxlim: 2   bits: 3/2
c ---[  60]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  59]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  58]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  56]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  54]---> Adder-cost: 15   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: 22   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  48]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  45]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  43]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  42]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  40]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  39]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  36]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  35]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  34]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  33]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  32]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  31]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  30]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  29]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  28]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  27]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  26]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  25]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  24]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  23]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  21]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  20]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  18]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  17]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  15]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  14]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  13]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  12]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  11]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  10]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   9]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[   8]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[   7]---> Adder-cost: 13   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: 8   maxlim: 2   bits: 3/2
c ---[   3]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[   2]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   1]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17588    60961 |    5862       0        0     nan |  0.000 % |
c |       100 |   17582    60944 |    6448      99      412     4.2 |  8.553 % |
c |       250 |   17582    60944 |    7093     249     1188     4.8 |  8.553 % |
c |       475 |   17582    60944 |    7802     474     2227     4.7 |  8.553 % |
c ==============================================================================
c [1mFound solution: 311[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2074   maxlim: 1191   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       751 |   32004   112411 |   10668     750     3745     5.0 |  8.553 % |
c |       851 |   32004   112411 |   11734     850     4277     5.0 |  5.777 % |
c |      1001 |   32004   112411 |   12908    1000     4943     4.9 |  5.777 % |
c |      1226 |   32004   112411 |   14199    1225     6202     5.1 |  5.777 % |
c |      1563 |   32004   112411 |   15619    1562     7990     5.1 |  5.777 % |
c ==============================================================================
c [1mFound solution: 187[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1315   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1777 |   32011   112447 |   10670    1776     9447     5.3 |  5.777 % |
c |      1877 |   32011   112447 |   11737    1876     9909     5.3 |  5.821 % |
c |      2027 |   32011   112447 |   12910    2026    10684     5.3 |  5.821 % |
c |      2252 |   32011   112447 |   14201    2251    12383     5.5 |  5.821 % |
c |      2589 |   32011   112447 |   15621    2588    14553     5.6 |  5.821 % |
c |      3096 |   32011   112447 |   17184    3095    17704     5.7 |  5.821 % |
c |      3855 |   32011   112447 |   18902    3854    24090     6.3 |  5.821 % |
c ==============================================================================
c [1mFound solution: 133[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1369   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4404 |   32023   112509 |   10674    4403    27626     6.3 |  5.821 % |
c |      4505 |   32023   112509 |   11741    4504    28294     6.3 |  5.880 % |
c |      4656 |   32023   112509 |   12915    4655    33232     7.1 |  5.880 % |
c |      4881 |   32023   112509 |   14207    4880    34420     7.1 |  5.880 % |
c |      5218 |   32023   112509 |   15627    5217    36126     6.9 |  5.880 % |
c |      5724 |   32023   112509 |   17190    5723    40148     7.0 |  5.880 % |
c |      6483 |   32023   112509 |   18909    6482    58692     9.1 |  5.880 % |
c ==============================================================================
c [1mFound solution: 115[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1387   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7467 |   32027   112540 |   10675    7466    73884     9.9 |  5.880 % |
c |      7567 |   32027   112540 |   11742    7566    74395     9.8 |  5.925 % |
c |      7717 |   32027   112540 |   12916    7716    75396     9.8 |  5.925 % |
c |      7942 |   32027   112540 |   14208    7941    77348     9.7 |  5.925 % |
c |      8280 |   32027   112540 |   15629    8279    87341    10.5 |  5.925 % |
c |      8786 |   32027   112540 |   17192    8785    96372    11.0 |  5.925 % |
c |      9545 |   32027   112540 |   18911    9544   109787    11.5 |  5.925 % |
c |     10686 |   32027   112540 |   20802   10685   143344    13.4 |  5.925 % |
c |     12395 |   32027   112540 |   22882   12394   228121    18.4 |  5.925 % |
c |     14960 |   32027   112540 |   25171   14959   410174    27.4 |  5.925 % |
c ==============================================================================
c [1mFound solution: 83[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1419   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16188 |   32031   112569 |   10677   16187   437606    27.0 |  5.925 % |
c |     16288 |   32031   112569 |   11744    8194   294062    35.9 |  5.969 % |
c |     16439 |   32031   112569 |   12919    8345   295088    35.4 |  5.969 % |
c |     16665 |   32031   112569 |   14211    8571   297065    34.7 |  5.969 % |
c |     17002 |   32031   112569 |   15632    8908   300257    33.7 |  5.969 % |
c |     17509 |   32031   112569 |   17195    9415   326559    34.7 |  5.969 % |
c |     18268 |   32031   112569 |   18914   10174   344463    33.9 |  5.969 % |
c |     19407 |   32031   112569 |   20806   11313   399236    35.3 |  5.969 % |
c |     21117 |   32031   112569 |   22887   13023   470772    36.1 |  5.969 % |
c |     23679 |   32031   112569 |   25175   15585   611787    39.3 |  5.969 % |
c |     27523 |   32031   112569 |   27693   19429   783980    40.4 |  5.969 % |
c |     33290 |   32031   112569 |   30462   25196  1326064    52.6 |  5.969 % |
c |     41939 |   32031   112569 |   33508   33845  2088269    61.7 |  5.969 % |
c |     54913 |   32031   112569 |   36859   27731  1543216    55.6 |  5.969 % |
c |     74374 |   32031   112569 |   40545   18398  2248487   122.2 |  5.969 % |
c |    103567 |   32031   112569 |   44600   14853  1392411    93.7 |  5.969 % |
c |    147357 |   32031   112569 |   49060   26324  3639365   138.3 |  5.969 % |
c |    213041 |   32031   112569 |   53966   52025 10536788   202.5 |  5.969 % |
c |    311569 |   32031   112569 |   59363   27207  5092804   187.2 |  5.969 % |
c |    459358 |   32031   112569 |   65299   31880  6713394   210.6 |  5.969 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v853 v782 -v197 v102 -v21 v2 -v855 v103 v1 -v785 v384 -v272 -v196 -v20 v3 -v856 -v786 v76 -v55 -v23 v4 v383 -v275 -v202 v75 -v54 v11 -v763 v387 -v276 -v200 -v56 -v24 v5 -v762 -v247 v150 v77 -v57 -v26 v6 -v764 -v613 v388 -v201 -v79 -v58 -v39 -v27 v7 -v765 -v612 v513 -v250 -v205 v149 -v65 -v38 v766 -v618 -v251 -v80 -v59 -v40 v773 -v617 v512 -v326 -v155 -v125 v82 -v60 -v41 v767 -v619 -v153 v83 -v61 -v42 v768 v623 -v593 -v573 v518 -v128 -v49 v769 -v622 v577 v516 -v154 -v129 -v43 -v729 -v620 v596 v576 v158 -v44 -v621 v597 v517 -v45 -v881 v728 -v521 -v852 v781 -v192 v104 -v17 -v857 -v787 -v537 -v468 -v271 -v198 -v22 v14 -v541 -v71 -v25 v15 -v859 v385 -v277 -v203 v108 -v70 -v29 v10 -v860 v389 -v28 v790 -v246 -v206 -v145 v78 -v68 -v8 -v204 -v81 -v69 -v811 v776 -v638 -v508 -v391 -v322 -v280 -v252 v151 v85 -v64 v777 -v642 -v614 -v392 v84 v772 -v615 v514 -v325 -v156 -v124 -v62 -v52 v616 -v53 -v770 v627 -v592 v519 -v255 v159 -v130 -v48 -v572 v157 -v877 v598 v574 -v522 -v46 v578 -v520 -v880 v730 -v133 -v601 -v854 v783 -v464 v267 v105 -v13 -v858 v379 -v191 -v16 -v12 -v862 v788 -v536 -v488 -v467 v378 -v273 -v193 v109 -v18 -v861 -v540 -v492 -v199 v107 -v19 v791 v386 -v278 v242 -v195 -v67 -v33 v789 v390 -v207 v72 -v66 v807 v775 -v394 -v301 -v281 -v248 v73 -v9 v774 -v393 -v279 -v144 v74 -v810 -v637 -v321 v253 -v146 -v120 v89 -v51 -v641 -v507 v152 -v50 -v630 -v588 -v509 -v327 v256 v148 -v126 -v63 v631 v515 -v254 v160 -v771 v626 v594 v511 -v131 -v725 -v523 -v876 -v724 -v709 -v624 v599 -v330 -v134 -v47 v575 -v132 v882 v731 -v602 v586 -v600 v582 -v900 v732 v581 -v904 v733 -v851 v779 -v463 -v422 v106 -v850 v784 -v426 v266 v110 -v866 v780 -v662 -v538 v487 -v469 v268 -v177 -v36 v792 -v666 -v542 -v491 v380 -v274 -v194 -v37 v381 -v297 v270 -v222 -v215 -v32 v382 -v282 v241 -v226 -v211 v806 -v544 -v472 v398 -v317 -v300 v243 -v210 -v92 -v30 -v545 v249 -v93 -v812 v639 -v629 -v323 v245 v88 -v643 -v628 v257 -v147 -v119 -v913 -v836 -v328 v168 -v121 v86 -v917 v587 -v510 v164 -v127 v872 v815 -v705 -v645 v589 v531 -v347 -v331 v163 -v123 -v646 v595 v527 -v351 -v329 -v135 v878 -v708 -v625 v591 -v583 -v526 v726 -v603 -v585 v95 v883 v727 v94 v899 v884 -v737 -v579 -v903 v885 -v869 v533 -v465 -v421 -v173 v118 -v35 -v870 v778 -v425 -v114 -v34 -v865 -v800 -v661 -v539 v489 -v470 -v212 -v176 -v113 v796 -v665 v543 -v493 v269 -v214 -v863 -v802 v795 -v547 -v473 -v450 -v401 -v296 -v290 -v221 -v91 -v633 -v546 -v471 -v402 v286 -v225 -v90 v808 -v632 -v495 -v397 -v302 -v285 -v208 -v31 -v496 -v316 v244 v832 -v813 -v752 v640 -v395 -v318 v265 -v209 -v165 -v644 -v324 v261 -v167 -v912 -v835 v816 v648 -v528 -v320 -v305 v260 -v87 -v916 v814 -v647 -v530 -v332 -v122 -v704 -v346 v161 -v143 v871 v590 -v584 -v350 -v139 v873 -v710 v611 -v524 v162 -v138 v879 v607 v875 -v740 -v606 -v561 -v525 v886 -v741 -v565 v96 v901 -v736 -v713 -v580 v97 v905 -v867 -v797 -v484 -v461 -v423 -v172 v117 -v799 v532 v466 v427 -v213 -v663 v534 v490 v462 -v446 -v400 -v292 -v287 -v178 -v111 v667 v535 -v494 -v474 -v399 -v289 -v864 v793 -v551 v498 -v449 -v429 -v298 v223 -v112 -v801 v497 -v430 -v227 -v803 -v794 v748 v687 -v669 -v303 -v283 -v262 -v181 v809 -v691 -v670 -v634 -v264 -v166 v831 v805 -v751 v635 -v396 -v306 -v284 v229 v817 v636 -v529 -v319 -v304 v230 -v914 -v837 -v700 v652 -v340 v258 -v140 -v918 -v336 -v142 -v706 -v608 -v348 -v335 -v259 -v610 v352 -v920 v840 -v739 -v711 -v412 -v371 -v136 -v921 -v896 v874 -v738 v375 -v895 -v894 -v714 -v604 -v560 v354 -v137 v890 -v712 -v564 v355 v902 v889 -v734 -v605 v100 v906 v101 -v868 -v798 -v658 -v424 v174 v115 -v483 v460 v428 -v288 -v217 -v664 v554 v485 v482 -v445 v432 -v216 -v179 v668 v555 v486 -v478 -v431 -v291 -v672 -v550 v502 -v477 -v451 v293 v224 -v182 -v671 -v299 -v263 -v228 -v180 -v827 v747 v686 -v548 v295 v232 v908 v804 -v690 -v307 v231 v907 v833 v825 -v753 -v655 -v454 -v337 v821 v656 v342 -v339 -v141 v915 v838 -v820 v651 v341 -v919 -v699 -v609 -v923 v841 -v756 -v701 -v649 -v408 -v349 -v333 -v922 v839 v707 v353 -v891 v703 -v411 -v370 v357 -v334 -v893 -v715 v374 v356 -v562 v99 -v897 -v566 v98 -v898 v887 -v735 -v553 v479 -v#### 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.97 0.91 2/54 32568
Raw data (stat): 32568 (runsolver) R 32567 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479852688 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 1483 0 0 0 994 3 0 0 25 0 1 0 479852688 7737344 1460 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1889 1460 603 41 0 1848 0
vsize: 7556
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 2134 0 0 0 1992 5 0 0 25 0 1 0 479852688 10399744 2111 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2539 2111 603 41 0 2498 0
vsize: 10156
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 3079 0 0 0 2989 9 0 0 25 0 1 0 479852688 14168064 3056 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3459 3056 603 41 0 3418 0
vsize: 13836
[startup+40.0027 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 3418 0 0 0 3988 10 0 0 25 0 1 0 479852688 15777792 3395 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3852 3395 603 41 0 3811 0
vsize: 15408
[startup+50.0034 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 3617 0 0 0 4986 11 0 0 25 0 1 0 479852688 16588800 3594 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4050 3594 603 41 0 4009 0
vsize: 16200
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 4451 0 0 0 5984 14 0 0 25 0 1 0 479852688 19955712 4428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4872 4428 603 41 0 4831 0
vsize: 19488
[startup+70.0038 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 4631 0 0 0 6983 15 0 0 25 0 1 0 479852688 20631552 4608 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5037 4608 603 41 0 4996 0
vsize: 20148
[startup+80.0045 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 4631 0 0 0 7982 16 0 0 25 0 1 0 479852688 20631552 4608 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5037 4608 603 41 0 4996 0
vsize: 20148
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 5148 0 0 0 8981 17 0 0 25 0 1 0 479852688 22790144 5125 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5564 5125 603 41 0 5523 0
vsize: 22256
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 5723 0 0 0 9979 19 0 0 25 0 1 0 479852688 25079808 5700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6123 5700 603 41 0 6082 0
vsize: 24492
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 6260 0 0 0 10977 21 0 0 25 0 1 0 479852688 27365376 6237 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6681 6237 603 41 0 6640 0
vsize: 26724
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 6743 0 0 0 11976 22 0 0 25 0 1 0 479852688 29257728 6720 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7143 6720 603 41 0 7102 0
vsize: 28572
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 6743 0 0 0 12976 23 0 0 25 0 1 0 479852688 29257728 6720 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7143 6720 603 41 0 7102 0
vsize: 28572
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 6743 0 0 0 13976 23 0 0 25 0 1 0 479852688 29257728 6720 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7143 6720 603 41 0 7102 0
vsize: 28572
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 6743 0 0 0 14976 23 0 0 25 0 1 0 479852688 29257728 6720 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7143 6720 603 41 0 7102 0
vsize: 28572
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 6743 0 0 0 15975 24 0 0 25 0 1 0 479852688 29257728 6720 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7143 6720 603 41 0 7102 0
vsize: 28572
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 6743 0 0 0 16975 24 0 0 25 0 1 0 479852688 29257728 6720 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7143 6720 603 41 0 7102 0
vsize: 28572
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 7182 0 0 0 17973 26 0 0 25 0 1 0 479852688 31145984 7159 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7604 7159 603 41 0 7563 0
vsize: 30416
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 7403 0 0 0 18972 27 0 0 25 0 1 0 479852688 31948800 7380 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7800 7380 603 41 0 7759 0
vsize: 31200
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 7403 0 0 0 19972 28 0 0 25 0 1 0 479852688 31948800 7380 4294967295 134512640 134672761 3221224544 3221223728 134559540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7800 7380 603 41 0 7759 0
vsize: 31200
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 7403 0 0 0 20971 28 0 0 25 0 1 0 479852688 31948800 7380 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7800 7380 603 41 0 7759 0
vsize: 31200
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 7403 0 0 0 21971 28 0 0 25 0 1 0 479852688 31948800 7380 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7800 7380 603 41 0 7759 0
vsize: 31200
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 7403 0 0 0 22971 29 0 0 25 0 1 0 479852688 31948800 7380 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7800 7380 603 41 0 7759 0
vsize: 31200
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 8227 0 0 0 23968 32 0 0 25 0 1 0 479852688 35438592 8204 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8652 8204 603 41 0 8611 0
vsize: 34608
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 9048 0 0 0 24966 34 0 0 25 0 1 0 479852688 38670336 9025 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9441 9025 603 41 0 9400 0
vsize: 37764
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 9672 0 0 0 25964 36 0 0 25 0 1 0 479852688 41226240 9649 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10065 9649 603 41 0 10024 0
vsize: 40260
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 9672 0 0 0 26964 36 0 0 25 0 1 0 479852688 41226240 9649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10065 9649 603 41 0 10024 0
vsize: 40260
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 9672 0 0 0 27964 36 0 0 25 0 1 0 479852688 41226240 9649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10065 9649 603 41 0 10024 0
vsize: 40260
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 9673 0 0 0 28964 37 0 0 25 0 1 0 479852688 41226240 9650 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10065 9650 603 41 0 10024 0
vsize: 40260
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 9673 0 0 0 29963 37 0 0 25 0 1 0 479852688 41226240 9650 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10065 9650 603 41 0 10024 0
vsize: 40260
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 9673 0 0 0 30963 37 0 0 25 0 1 0 479852688 41226240 9650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10065 9650 603 41 0 10024 0
vsize: 40260
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 9673 0 0 0 31964 37 0 0 25 0 1 0 479852688 41226240 9650 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10065 9650 603 41 0 10024 0
vsize: 40260
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 9673 0 0 0 32964 37 0 0 25 0 1 0 479852688 41226240 9650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10065 9650 603 41 0 10024 0
vsize: 40260
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 10084 0 0 0 33963 38 0 0 25 0 1 0 479852688 42979328 10061 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10493 10061 603 41 0 10452 0
vsize: 41972
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 10439 0 0 0 34963 38 0 0 25 0 1 0 479852688 44462080 10416 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10855 10416 603 41 0 10814 0
vsize: 43420
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 10828 0 0 0 35962 39 0 0 25 0 1 0 479852688 46080000 10805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11250 10805 603 41 0 11209 0
vsize: 45000
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 11299 0 0 0 36960 41 0 0 25 0 1 0 479852688 48017408 11276 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11723 11276 603 41 0 11682 0
vsize: 46892
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 11746 0 0 0 37959 42 0 0 25 0 1 0 479852688 49889280 11723 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12180 11723 603 41 0 12139 0
vsize: 48720
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12174 0 0 0 38958 43 0 0 25 0 1 0 479852688 51634176 12151 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12606 12151 603 41 0 12565 0
vsize: 50424
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12596 0 0 0 39957 44 0 0 25 0 1 0 479852688 53383168 12573 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13033 12573 603 41 0 12992 0
vsize: 52132
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12973 0 0 0 40956 46 0 0 25 0 1 0 479852688 54996992 12950 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12950 603 41 0 13386 0
vsize: 53708
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12973 0 0 0 41956 46 0 0 25 0 1 0 479852688 54996992 12950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12950 603 41 0 13386 0
vsize: 53708
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12973 0 0 0 42957 46 0 0 25 0 1 0 479852688 54996992 12950 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12950 603 41 0 13386 0
vsize: 53708
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12973 0 0 0 43957 46 0 0 25 0 1 0 479852688 54996992 12950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12950 603 41 0 13386 0
vsize: 53708
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12973 0 0 0 44957 46 0 0 25 0 1 0 479852688 54996992 12950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12950 603 41 0 13386 0
vsize: 53708
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12973 0 0 0 45957 46 0 0 25 0 1 0 479852688 54996992 12950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12950 603 41 0 13386 0
vsize: 53708
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12973 0 0 0 46957 46 0 0 25 0 1 0 479852688 54996992 12950 4294967295 134512640 134672761 3221224544 3221223728 134558890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12950 603 41 0 13386 0
vsize: 53708
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 47958 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 48958 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 49958 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 50958 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 51958 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 52959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 53959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 54959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 55959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 56959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 57959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 58960 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 59960 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 60960 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 61959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 62959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 63959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 64959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 65959 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 66960 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 12974 0 0 0 67960 46 0 0 25 0 1 0 479852688 54996992 12951 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13427 12951 603 41 0 13386 0
vsize: 53708
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 13544 0 0 0 68959 47 0 0 25 0 1 0 479852688 57278464 13521 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13984 13521 603 41 0 13943 0
vsize: 55936
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 14208 0 0 0 69957 49 0 0 25 0 1 0 479852688 59969536 14185 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14641 14185 603 41 0 14600 0
vsize: 58564
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 14900 0 0 0 70955 52 0 0 25 0 1 0 479852688 62787584 14877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15329 14877 603 41 0 15288 0
vsize: 61316
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 15620 0 0 0 71953 54 0 0 25 0 1 0 479852688 65753088 15597 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16053 15597 603 41 0 16012 0
vsize: 64212
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16218 0 0 0 72951 56 0 0 25 0 1 0 479852688 68177920 16195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16645 16195 603 41 0 16604 0
vsize: 66580
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 73951 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 74951 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 75951 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 76952 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223648 134555098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 77952 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 78952 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 79952 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 80952 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 81953 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 82953 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 83953 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 84953 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16413 0 0 0 85953 56 0 0 25 0 1 0 479852688 69001216 16390 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16390 603 41 0 16805 0
vsize: 67384
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 16563 0 0 0 86953 57 0 0 25 0 1 0 479852688 69664768 16540 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17008 16540 603 41 0 16967 0
vsize: 68032
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 17207 0 0 0 87951 59 0 0 25 0 1 0 479852688 72228864 17184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17634 17184 603 41 0 17593 0
vsize: 70536
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 17880 0 0 0 88949 61 0 0 25 0 1 0 479852688 75051008 17857 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18323 17857 603 41 0 18282 0
vsize: 73292
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18294 0 0 0 89948 62 0 0 25 0 1 0 479852688 76804096 18271 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18271 603 41 0 18710 0
vsize: 75004
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18294 0 0 0 90948 62 0 0 25 0 1 0 479852688 76804096 18271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18271 603 41 0 18710 0
vsize: 75004
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18294 0 0 0 91948 62 0 0 25 0 1 0 479852688 76804096 18271 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18271 603 41 0 18710 0
vsize: 75004
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18294 0 0 0 92949 62 0 0 25 0 1 0 479852688 76804096 18271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18271 603 41 0 18710 0
vsize: 75004
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18294 0 0 0 93949 62 0 0 25 0 1 0 479852688 76804096 18271 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18271 603 41 0 18710 0
vsize: 75004
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18294 0 0 0 94949 62 0 0 25 0 1 0 479852688 76804096 18271 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18271 603 41 0 18710 0
vsize: 75004
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18294 0 0 0 95949 62 0 0 25 0 1 0 479852688 76804096 18271 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18271 603 41 0 18710 0
vsize: 75004
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18294 0 0 0 96949 62 0 0 25 0 1 0 479852688 76804096 18271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18271 603 41 0 18710 0
vsize: 75004
[startup+980.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18295 0 0 0 97950 62 0 0 25 0 1 0 479852688 76804096 18272 4294967295 134512640 134672761 3221224544 3221223728 134559392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18272 603 41 0 18710 0
vsize: 75004
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18295 0 0 0 98950 62 0 0 25 0 1 0 479852688 76804096 18272 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18272 603 41 0 18710 0
vsize: 75004
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18295 0 0 0 99950 62 0 0 25 0 1 0 479852688 76804096 18272 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18272 603 41 0 18710 0
vsize: 75004
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18295 0 0 0 100950 62 0 0 25 0 1 0 479852688 76804096 18272 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18272 603 41 0 18710 0
vsize: 75004
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18295 0 0 0 101950 62 0 0 25 0 1 0 479852688 76804096 18272 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18272 603 41 0 18710 0
vsize: 75004
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18295 0 0 0 102950 62 0 0 25 0 1 0 479852688 76804096 18272 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18272 603 41 0 18710 0
vsize: 75004
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18295 0 0 0 103950 62 0 0 25 0 1 0 479852688 76804096 18272 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18272 603 41 0 18710 0
vsize: 75004
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18295 0 0 0 104951 62 0 0 25 0 1 0 479852688 76804096 18272 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18272 603 41 0 18710 0
vsize: 75004
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18295 0 0 0 105951 62 0 0 25 0 1 0 479852688 76804096 18272 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18272 603 41 0 18710 0
vsize: 75004
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 18315 0 0 0 106951 62 0 0 25 0 1 0 479852688 76804096 18292 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18751 18292 603 41 0 18710 0
vsize: 75004
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19026 0 0 0 107948 65 0 0 25 0 1 0 479852688 79753216 19003 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19471 19003 603 41 0 19430 0
vsize: 77884
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 108947 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 109947 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 110948 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 111948 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 112948 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 113948 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 114948 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 115948 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223648 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 116948 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 117948 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 118949 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32568
Raw data (stat): 32568 (minisat+) R 32567 28546 28545 0 -1 0 19713 0 0 0 119949 66 0 0 25 0 1 0 479852688 82583552 19690 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20162 19690 603 41 0 20121 0
vsize: 80648
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 32568
Raw data (stat): 32568 (minisat+) Z 32567 28546 28545 0 -1 12 19716 0 0 0 119949 70 0 0 25 0 1 0 479852688 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.2
CPU user time (s): 1199.49
CPU system time (s): 0.703892
CPU usage (%): 100.011
Max. virtual memory (Kb): 80648
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####