PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-vpm1.opb
MD5SUM	9d68724ddc6098af63bcc619f21688cc
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	20
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	168
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	819200
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	4941871
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	459.704
Number of variables	2754
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	82
Trace number 21958

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-22 01:38:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12373 boxname=wulflinc1 idbench=952 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9d68724ddc6098af63bcc619f21688cc  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-vpm1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-vpm1.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-vpm1.opb
IDLAUNCH: 12373
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        508924 kB
Buffers:          4508 kB
Cached:         496720 kB
SwapCached:          0 kB
Active:          88832 kB
Inactive:       415580 kB
HighTotal:      131008 kB
HighFree:         1848 kB
LowTotal:       903652 kB
LowFree:        507076 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              64 kB
Writeback:           0 kB
Mapped:           7172 kB
Slab:            15740 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:58:36 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 12373 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 484]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 483]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 482]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 481]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 480]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 479]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 478]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 477]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 474]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 473]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 472]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 471]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 468]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 467]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 466]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 465]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 462]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 459]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 458]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 457]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 454]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 453]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 452]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 451]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 450]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 448]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 447]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 446]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 445]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 444]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 441]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 440]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 439]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 433]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 427]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 422]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 421]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 415]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 409]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 408]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 402]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 397]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 396]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 391]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 390]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 386]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 385]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 384]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 380]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 379]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 378]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 374]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 373]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 372]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 368]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 367]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 366]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 365]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 364]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 359]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 353]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 347]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 339]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 333]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 327]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 321]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 317]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 316]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 315]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 314]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 313]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 312]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 310]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 309]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 308]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 307]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 306]---> Adder-cost: 61   maxlim: 57342   bits: 17/16
c ---[ 302]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 301]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 300]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 295]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 294]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 290]---> Adder-cost: 36   maxlim: 217086   bits: 19/18
c ---[ 289]---> Adder-cost: 36   maxlim: 217086   bits: 19/18
c ---[ 288]---> Adder-cost: 36   maxlim: 217086   bits: 19/18
c ---[ 287]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 286]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 285]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 284]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 283]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 282]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 280]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 279]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 278]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 277]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 276]---> Adder-cost: 57   maxlim: 28670   bits: 16/15
c ---[ 274]---> Adder-cost: 316   maxlim: 2149200   bits: 22/22
c ---[ 264]---> Adder-cost: 384   maxlim: 3377200   bits: 23/22
c ---[ 260]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 258]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 256]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 254]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 252]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[ 250]---> Adder-cost: 258   maxlim: 1330100   bits: 21/21
c ---[ 248]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[ 246]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 244]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 242]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 236]---> Adder-cost: 282   maxlim: 1636900   bits: 21/21
c ---[ 234]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 232]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 224]---> Adder-cost: 312   maxlim: 1842000   bits: 22/21
c ---[ 222]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 216]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 214]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 212]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 210]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 208]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 206]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 204]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 202]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 200]---> Adder-cost: 394   maxlim: 1841200   bits: 22/21
c ---[ 198]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[ 196]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 194]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 192]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 191]---> Adder-cost: 22   maxlim: 3069   bits: 12/12
c ---[ 190]---> Adder-cost: 64   maxlim: 5115   bits: 13/13
c ---[ 189]---> Adder-cost: 66   maxlim: 5627   bits: 13/13
c ---[ 188]---> Adder-cost: 100   maxlim: 7161   bits: 13/13
c ---[ 187]---> Adder-cost: 126   maxlim: 10232   bits: 14/14
c ---[ 186]---> Adder-cost: 124   maxlim: 7672   bits: 14/13
c ---[ 185]---> Adder-cost: 22   maxlim: 3069   bits: 12/12
c ---[ 184]---> Adder-cost: 64   maxlim: 5115   bits: 13/13
c ---[ 183]---> Adder-cost: 66   maxlim: 5627   bits: 13/13
c ---[ 182]---> Adder-cost: 100   maxlim: 6137   bits: 13/13
c ---[ 181]---> Adder-cost: 124   maxlim: 8184   bits: 14/13
c ---[ 180]---> Adder-cost: 124   maxlim: 8696   bits: 14/14
c ---[ 179]---> Adder-cost: 22   maxlim: 3069   bits: 12/12
c ---[ 178]---> Adder-cost: 64   maxlim: 5115   bits: 13/13
c ---[ 177]---> Adder-cost: 66   maxlim: 5371   bits: 13/13
c ---[ 176]---> Adder-cost: 100   maxlim: 6905   bits: 13/13
c ---[ 175]---> Adder-cost: 124   maxlim: 8952   bits: 14/14
c ---[ 174]---> Adder-cost: 124   maxlim: 8440   bits: 14/14
c ---[ 173]---> Adder-cost: 22   maxlim: 3069   bits: 12/12
c ---[ 172]---> Adder-cost: 64   maxlim: 4091   bits: 13/12
c ---[ 171]---> Adder-cost: 66   maxlim: 5371   bits: 13/13
c ---[ 170]---> Adder-cost: 98   maxlim: 5625   bits: 13/13
c ---[ 169]---> Adder-cost: 122   maxlim: 8696   bits: 14/14
c ---[ 168]---> Adder-cost: 114   maxlim: 7160   bits: 13/13
c ---[ 167]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 166]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 165]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 164]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 163]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 162]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 161]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 160]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 159]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 158]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 157]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 156]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 155]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 154]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 153]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 152]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 151]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 150]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 149]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 148]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 147]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 146]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 145]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 144]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 142]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 141]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 140]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 139]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 138]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 136]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 135]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 134]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 133]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 132]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 130]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 129]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 128]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 127]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 126]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 124]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 123]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 122]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 121]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 120]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 116]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 115]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 114]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 110]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 109]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 108]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 104]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 103]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 102]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  98]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  97]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  96]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  91]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  90]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  85]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  84]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  79]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  78]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  73]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  72]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  68]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  67]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  66]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  62]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  61]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  60]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  56]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  54]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  50]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  48]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  47]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  46]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  45]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  44]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  43]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  42]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  41]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  40]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  39]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  38]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  37]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  36]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  35]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  34]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  33]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  32]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  31]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  30]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  29]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  28]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  27]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  26]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  25]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  24]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  22]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  21]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  20]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  19]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  18]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  16]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  14]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  13]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  12]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  10]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[   9]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   8]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[   7]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[   6]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[   4]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[   3]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   2]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[   1]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[   0]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  106012   387180 |   35337       0        0     nan |  0.000 % |
c |       101 |  105991   387111 |   38870      95      322     3.4 | 21.912 % |
c |       251 |  105953   386987 |   42757     238      920     3.9 | 21.940 % |
c |       476 |  105923   386893 |   47033     461     2983     6.5 | 21.967 % |
c |       813 |  105923   386893 |   51736     798     6377     8.0 | 21.967 % |
c |      1320 |  105909   386847 |   56910    1303    11720     9.0 | 21.976 % |
c |      2080 |  105901   386821 |   62601    2062    21877    10.6 | 21.981 % |
c |      3219 |  105885   386769 |   68861    3199    39169    12.2 | 21.994 % |
c |      4927 |  105885   386769 |   75747    4907    84649    17.3 | 21.994 % |
c |      7489 |  105844   386634 |   83322    7463   135855    18.2 | 22.026 % |
c |     11333 |  105782   386439 |   91655   11299   217288    19.2 | 22.081 % |
c |     17099 |  105726   386261 |  100820   17053   310846    18.2 | 22.127 % |
c |     25748 |  105697   386161 |  110902   25686   524740    20.4 | 22.140 % |
c |     38723 |  105681   386109 |  121992   38659   818834    21.2 | 22.154 % |
c |     58184 |  105666   386064 |  134192   58118  1356049    23.3 | 22.168 % |
c |     87378 |  105568   385739 |  147611   87288  2205676    25.3 | 22.231 % |
c |    131167 |  105502   385519 |  162372  131051  3762444    28.7 | 22.272 % |
c |    196851 |  105374   385096 |  178609   46220   909319    19.7 | 22.368 % |
c |    295378 |  105334   384966 |  196470  144742  3501423    24.2 | 22.395 % |
c |    443167 |  105276   384780 |  216117  106382  3807906    35.8 | 22.446 % |
c |    664850 |  105214   384578 |  237729  123136  3490294    28.3 | 22.491 % |
#### 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.98 0.94 2/56 8198
Raw data (stat): 8198 (runsolver) R 8197 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 434746066 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+9.99971 s]
Raw data (loadavg): 0.93 0.98 0.94 2/56 8198
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 3429 0 0 0 990 8 0 0 25 0 1 0 434746066 16437248 3348 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4013 3348 603 41 0 3972 0
vsize: 16052
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.98 0.94 2/56 8198
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 4021 0 0 0 1989 10 0 0 25 0 1 0 434746066 18980864 3940 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 3940 603 41 0 4593 0
vsize: 18536
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.98 0.94 2/56 8198
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 4350 0 0 0 2988 11 0 0 25 0 1 0 434746066 20316160 4269 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4960 4269 603 41 0 4919 0
vsize: 19840
[startup+40.002 s]
Raw data (loadavg): 0.96 0.98 0.94 2/56 8198
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 4633 0 0 0 3987 12 0 0 25 0 1 0 434746066 21401600 4552 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5225 4552 603 41 0 5184 0
vsize: 20900
[startup+50.0028 s]
Raw data (loadavg): 0.96 0.98 0.94 2/56 8198
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 5503 0 0 0 4985 14 0 0 25 0 1 0 434746066 25161728 5422 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6143 5422 603 41 0 6102 0
vsize: 24572
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.98 0.94 2/56 8198
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 6302 0 0 0 5983 17 0 0 25 0 1 0 434746066 28385280 6221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6930 6221 603 41 0 6889 0
vsize: 27720
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.98 0.94 2/56 8198
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 6877 0 0 0 6981 19 0 0 25 0 1 0 434746066 30674944 6796 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7489 6796 603 41 0 7448 0
vsize: 29956
[startup+80.0112 s]
Raw data (loadavg): 0.98 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 7368 0 0 0 7979 21 0 0 25 0 1 0 434746066 32714752 7287 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7987 7287 603 41 0 7946 0
vsize: 31948
[startup+90.0124 s]
Raw data (loadavg): 0.98 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 7705 0 0 0 8978 22 0 0 25 0 1 0 434746066 34066432 7624 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8317 7624 603 41 0 8276 0
vsize: 33268
[startup+100.013 s]
Raw data (loadavg): 0.98 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 7995 0 0 0 9977 23 0 0 25 0 1 0 434746066 35672064 7914 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8709 7914 603 41 0 8668 0
vsize: 34836
[startup+110.013 s]
Raw data (loadavg): 0.98 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 8292 0 0 0 10977 24 0 0 25 0 1 0 434746066 36900864 8211 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9009 8211 603 41 0 8968 0
vsize: 36036
[startup+120.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 8711 0 0 0 11976 25 0 0 25 0 1 0 434746066 38670336 8630 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9441 8630 603 41 0 9400 0
vsize: 37764
[startup+130.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 8947 0 0 0 12975 26 0 0 25 0 1 0 434746066 39612416 8866 4294967295 134512640 134672761 3221224544 3221223712 134564493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9671 8866 603 41 0 9630 0
vsize: 38684
[startup+140.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9257 0 0 0 13974 27 0 0 25 0 1 0 434746066 40828928 9176 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9968 9176 603 41 0 9927 0
vsize: 39872
[startup+150.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9418 0 0 0 14974 28 0 0 25 0 1 0 434746066 41500672 9337 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10132 9337 603 41 0 10091 0
vsize: 40528
[startup+160.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9418 0 0 0 15974 28 0 0 25 0 1 0 434746066 41500672 9337 4294967295 134512640 134672761 3221224544 3221223728 134559609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10132 9337 603 41 0 10091 0
vsize: 40528
[startup+170.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9418 0 0 0 16975 28 0 0 25 0 1 0 434746066 41500672 9337 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10132 9337 603 41 0 10091 0
vsize: 40528
[startup+180.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9418 0 0 0 17975 28 0 0 25 0 1 0 434746066 41500672 9337 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10132 9337 603 41 0 10091 0
vsize: 40528
[startup+190.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9418 0 0 0 18976 28 0 0 25 0 1 0 434746066 41500672 9337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10132 9337 603 41 0 10091 0
vsize: 40528
[startup+200.032 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9419 0 0 0 19976 28 0 0 25 0 1 0 434746066 41500672 9338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10132 9338 603 41 0 10091 0
vsize: 40528
[startup+210.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9419 0 0 0 20976 28 0 0 25 0 1 0 434746066 41500672 9338 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10132 9338 603 41 0 10091 0
vsize: 40528
[startup+220.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9419 0 0 0 21976 28 0 0 25 0 1 0 434746066 41500672 9338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10132 9338 603 41 0 10091 0
vsize: 40528
[startup+230.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9432 0 0 0 22976 28 0 0 25 0 1 0 434746066 41500672 9351 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10132 9351 603 41 0 10091 0
vsize: 40528
[startup+240.034 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9449 0 0 0 23976 28 0 0 25 0 1 0 434746066 41672704 9368 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10174 9368 603 41 0 10133 0
vsize: 40696
[startup+250.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9462 0 0 0 24977 28 0 0 25 0 1 0 434746066 41672704 9381 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10174 9381 603 41 0 10133 0
vsize: 40696
[startup+260.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9476 0 0 0 25977 28 0 0 25 0 1 0 434746066 41672704 9395 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10174 9395 603 41 0 10133 0
vsize: 40696
[startup+270.033 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9499 0 0 0 26977 28 0 0 25 0 1 0 434746066 41836544 9418 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9418 603 41 0 10173 0
vsize: 40856
[startup+280.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9543 0 0 0 27977 28 0 0 25 0 1 0 434746066 42000384 9462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10254 9462 603 41 0 10213 0
vsize: 41016
[startup+290.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9548 0 0 0 28978 28 0 0 25 0 1 0 434746066 42000384 9467 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10254 9467 603 41 0 10213 0
vsize: 41016
[startup+300.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9561 0 0 0 29978 28 0 0 25 0 1 0 434746066 42196992 9480 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10302 9480 603 41 0 10261 0
vsize: 41208
[startup+310.039 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9565 0 0 0 30978 29 0 0 25 0 1 0 434746066 42196992 9484 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10302 9484 603 41 0 10261 0
vsize: 41208
[startup+320.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9565 0 0 0 31978 29 0 0 25 0 1 0 434746066 42196992 9484 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10302 9484 603 41 0 10261 0
vsize: 41208
[startup+330.04 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9575 0 0 0 32978 29 0 0 25 0 1 0 434746066 42196992 9494 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10302 9494 603 41 0 10261 0
vsize: 41208
[startup+340.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 9909 0 0 0 33977 30 0 0 25 0 1 0 434746066 43536384 9828 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10629 9828 603 41 0 10588 0
vsize: 42516
[startup+350.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10488 0 0 0 34976 31 0 0 25 0 1 0 434746066 45826048 10407 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11188 10407 603 41 0 11147 0
vsize: 44752
[startup+360.041 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10625 0 0 0 35976 31 0 0 25 0 1 0 434746066 46366720 10544 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11320 10544 603 41 0 11279 0
vsize: 45280
[startup+370.042 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8200
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10625 0 0 0 36976 31 0 0 25 0 1 0 434746066 46366720 10544 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11320 10544 603 41 0 11279 0
vsize: 45280
[startup+380.043 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10626 0 0 0 37976 31 0 0 25 0 1 0 434746066 46366720 10545 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11320 10545 603 41 0 11279 0
vsize: 45280
[startup+390.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10626 0 0 0 38976 32 0 0 25 0 1 0 434746066 46366720 10545 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11320 10545 603 41 0 11279 0
vsize: 45280
[startup+400.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10626 0 0 0 39976 32 0 0 25 0 1 0 434746066 46366720 10545 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11320 10545 603 41 0 11279 0
vsize: 45280
[startup+410.044 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10626 0 0 0 40976 32 0 0 25 0 1 0 434746066 46366720 10545 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11320 10545 603 41 0 11279 0
vsize: 45280
[startup+420.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10626 0 0 0 41976 32 0 0 25 0 1 0 434746066 46366720 10545 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11320 10545 603 41 0 11279 0
vsize: 45280
[startup+430.045 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10631 0 0 0 42976 32 0 0 25 0 1 0 434746066 46366720 10550 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11320 10550 603 41 0 11279 0
vsize: 45280
[startup+440.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10639 0 0 0 43976 32 0 0 25 0 1 0 434746066 46514176 10558 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11356 10558 603 41 0 11315 0
vsize: 45424
[startup+450.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10641 0 0 0 44976 32 0 0 25 0 1 0 434746066 46514176 10560 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11356 10560 603 41 0 11315 0
vsize: 45424
[startup+460.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10663 0 0 0 45976 33 0 0 25 0 1 0 434746066 46514176 10582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11356 10582 603 41 0 11315 0
vsize: 45424
[startup+470.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10666 0 0 0 46976 33 0 0 25 0 1 0 434746066 46514176 10585 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11356 10585 603 41 0 11315 0
vsize: 45424
[startup+480.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10692 0 0 0 47977 33 0 0 25 0 1 0 434746066 46710784 10611 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11404 10611 603 41 0 11363 0
vsize: 45616
[startup+490.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10726 0 0 0 48977 33 0 0 25 0 1 0 434746066 46874624 10645 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11444 10645 603 41 0 11403 0
vsize: 45776
[startup+500.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10731 0 0 0 49977 33 0 0 25 0 1 0 434746066 46874624 10650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11444 10650 603 41 0 11403 0
vsize: 45776
[startup+510.046 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10732 0 0 0 50977 33 0 0 25 0 1 0 434746066 46874624 10651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11444 10651 603 41 0 11403 0
vsize: 45776
[startup+520.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10732 0 0 0 51977 33 0 0 25 0 1 0 434746066 46874624 10651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11444 10651 603 41 0 11403 0
vsize: 45776
[startup+530.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10733 0 0 0 52977 33 0 0 25 0 1 0 434746066 46874624 10652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11444 10652 603 41 0 11403 0
vsize: 45776
[startup+540.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10733 0 0 0 53977 33 0 0 25 0 1 0 434746066 46874624 10652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11444 10652 603 41 0 11403 0
vsize: 45776
[startup+550.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10734 0 0 0 54977 33 0 0 25 0 1 0 434746066 46874624 10653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11444 10653 603 41 0 11403 0
vsize: 45776
[startup+560.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10734 0 0 0 55977 33 0 0 25 0 1 0 434746066 46874624 10653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11444 10653 603 41 0 11403 0
vsize: 45776
[startup+570.047 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10734 0 0 0 56977 34 0 0 25 0 1 0 434746066 46874624 10653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11444 10653 603 41 0 11403 0
vsize: 45776
[startup+580.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10734 0 0 0 57977 34 0 0 25 0 1 0 434746066 46874624 10653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11444 10653 603 41 0 11403 0
vsize: 45776
[startup+590.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10746 0 0 0 58977 34 0 0 25 0 1 0 434746066 47038464 10665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11484 10665 603 41 0 11443 0
vsize: 45936
[startup+600.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10757 0 0 0 59977 34 0 0 25 0 1 0 434746066 47038464 10676 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11484 10676 603 41 0 11443 0
vsize: 45936
[startup+610.048 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10765 0 0 0 60977 34 0 0 25 0 1 0 434746066 47038464 10684 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11484 10684 603 41 0 11443 0
vsize: 45936
[startup+620.049 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10766 0 0 0 61977 34 0 0 25 0 1 0 434746066 47038464 10685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11484 10685 603 41 0 11443 0
vsize: 45936
[startup+630.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10766 0 0 0 62977 34 0 0 25 0 1 0 434746066 47038464 10685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11484 10685 603 41 0 11443 0
vsize: 45936
[startup+640.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10766 0 0 0 63977 35 0 0 25 0 1 0 434746066 47038464 10685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11484 10685 603 41 0 11443 0
vsize: 45936
[startup+650.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10835 0 0 0 64977 35 0 0 25 0 1 0 434746066 47366144 10754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11564 10754 603 41 0 11523 0
vsize: 46256
[startup+660.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10846 0 0 0 65977 36 0 0 25 0 1 0 434746066 47529984 10765 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11604 10765 603 41 0 11563 0
vsize: 46416
[startup+670.051 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8202
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10856 0 0 0 66977 36 0 0 25 0 1 0 434746066 47529984 10775 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11604 10775 603 41 0 11563 0
vsize: 46416
[startup+680.05 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10858 0 0 0 67976 36 0 0 25 0 1 0 434746066 47529984 10777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11604 10777 603 41 0 11563 0
vsize: 46416
[startup+690.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10878 0 0 0 68976 36 0 0 25 0 1 0 434746066 47726592 10797 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11652 10797 603 41 0 11611 0
vsize: 46608
[startup+700.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10887 0 0 0 69976 37 0 0 25 0 1 0 434746066 47726592 10806 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11652 10806 603 41 0 11611 0
vsize: 46608
[startup+710.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10896 0 0 0 70976 37 0 0 25 0 1 0 434746066 47726592 10815 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11652 10815 603 41 0 11611 0
vsize: 46608
[startup+720.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10896 0 0 0 71976 37 0 0 25 0 1 0 434746066 47726592 10815 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11652 10815 603 41 0 11611 0
vsize: 46608
[startup+730.052 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10896 0 0 0 72976 37 0 0 25 0 1 0 434746066 47726592 10815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11652 10815 603 41 0 11611 0
vsize: 46608
[startup+740.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10896 0 0 0 73977 37 0 0 25 0 1 0 434746066 47726592 10815 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11652 10815 603 41 0 11611 0
vsize: 46608
[startup+750.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10907 0 0 0 74977 37 0 0 25 0 1 0 434746066 47890432 10826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11692 10826 603 41 0 11651 0
vsize: 46768
[startup+760.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10914 0 0 0 75977 37 0 0 25 0 1 0 434746066 47890432 10833 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11692 10833 603 41 0 11651 0
vsize: 46768
[startup+770.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10914 0 0 0 76977 37 0 0 25 0 1 0 434746066 47890432 10833 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11692 10833 603 41 0 11651 0
vsize: 46768
[startup+780.053 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10914 0 0 0 77977 37 0 0 25 0 1 0 434746066 47890432 10833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11692 10833 603 41 0 11651 0
vsize: 46768
[startup+790.054 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10921 0 0 0 78977 37 0 0 25 0 1 0 434746066 47890432 10840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11692 10840 603 41 0 11651 0
vsize: 46768
[startup+800.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10930 0 0 0 79977 37 0 0 25 0 1 0 434746066 47890432 10849 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11692 10849 603 41 0 11651 0
vsize: 46768
[startup+810.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10932 0 0 0 80977 38 0 0 25 0 1 0 434746066 47890432 10851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11692 10851 603 41 0 11651 0
vsize: 46768
[startup+820.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10933 0 0 0 81977 38 0 0 25 0 1 0 434746066 47890432 10852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11692 10852 603 41 0 11651 0
vsize: 46768
[startup+830.055 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10941 0 0 0 82977 38 0 0 25 0 1 0 434746066 48054272 10860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11732 10860 603 41 0 11691 0
vsize: 46928
[startup+840.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10942 0 0 0 83977 38 0 0 25 0 1 0 434746066 48054272 10861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11732 10861 603 41 0 11691 0
vsize: 46928
[startup+850.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10955 0 0 0 84977 38 0 0 25 0 1 0 434746066 48054272 10874 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11732 10874 603 41 0 11691 0
vsize: 46928
[startup+860.056 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 10981 0 0 0 85977 38 0 0 25 0 1 0 434746066 48209920 10900 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11770 10900 603 41 0 11729 0
vsize: 47080
[startup+870.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11048 0 0 0 86977 39 0 0 25 0 1 0 434746066 48480256 10967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11836 10967 603 41 0 11795 0
vsize: 47344
[startup+880.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11108 0 0 0 87976 39 0 0 25 0 1 0 434746066 48746496 11027 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11901 11027 603 41 0 11860 0
vsize: 47604
[startup+890.058 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11174 0 0 0 88976 39 0 0 25 0 1 0 434746066 49012736 11093 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11966 11093 603 41 0 11925 0
vsize: 47864
[startup+900.058 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11239 0 0 0 89977 39 0 0 25 0 1 0 434746066 49283072 11158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12032 11158 603 41 0 11991 0
vsize: 48128
[startup+910.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11300 0 0 0 90977 40 0 0 25 0 1 0 434746066 49545216 11219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12096 11219 603 41 0 12055 0
vsize: 48384
[startup+920.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11361 0 0 0 91977 40 0 0 25 0 1 0 434746066 49811456 11280 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12161 11280 603 41 0 12120 0
vsize: 48644
[startup+930.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11428 0 0 0 92977 40 0 0 25 0 1 0 434746066 50081792 11347 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12227 11347 603 41 0 12186 0
vsize: 48908
[startup+940.058 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11491 0 0 0 93977 40 0 0 25 0 1 0 434746066 50352128 11410 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12293 11410 603 41 0 12252 0
vsize: 49172
[startup+950.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11560 0 0 0 94976 40 0 0 25 0 1 0 434746066 50622464 11479 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12359 11479 603 41 0 12318 0
vsize: 49436
[startup+960.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11634 0 0 0 95976 41 0 0 25 0 1 0 434746066 50888704 11553 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12424 11553 603 41 0 12383 0
vsize: 49696
[startup+970.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8204
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11706 0 0 0 96976 41 0 0 25 0 1 0 434746066 51159040 11625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12490 11625 603 41 0 12449 0
vsize: 49960
[startup+980.057 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11767 0 0 0 97976 41 0 0 25 0 1 0 434746066 51535872 11686 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12582 11686 603 41 0 12541 0
vsize: 50328
[startup+990.058 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11835 0 0 0 98976 41 0 0 25 0 1 0 434746066 51671040 11754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12615 11754 603 41 0 12574 0
vsize: 50460
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 11949 0 0 0 99977 41 0 0 25 0 1 0 434746066 52260864 11868 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12759 11868 603 41 0 12718 0
vsize: 51036
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 12374 0 0 0 100976 42 0 0 25 0 1 0 434746066 54018048 12293 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13188 12293 603 41 0 13147 0
vsize: 52752
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 12995 0 0 0 101974 44 0 0 25 0 1 0 434746066 56565760 12914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13810 12914 603 41 0 13769 0
vsize: 55240
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13361 0 0 0 102973 45 0 0 25 0 1 0 434746066 58048512 13280 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14172 13280 603 41 0 14131 0
vsize: 56688
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13626 0 0 0 103972 46 0 0 25 0 1 0 434746066 59125760 13545 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13545 603 41 0 14394 0
vsize: 57740
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13626 0 0 0 104972 46 0 0 25 0 1 0 434746066 59125760 13545 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13545 603 41 0 14394 0
vsize: 57740
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13626 0 0 0 105972 46 0 0 25 0 1 0 434746066 59125760 13545 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13545 603 41 0 14394 0
vsize: 57740
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13626 0 0 0 106972 46 0 0 25 0 1 0 434746066 59125760 13545 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13545 603 41 0 14394 0
vsize: 57740
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13626 0 0 0 107973 46 0 0 25 0 1 0 434746066 59125760 13545 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13545 603 41 0 14394 0
vsize: 57740
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13627 0 0 0 108973 47 0 0 25 0 1 0 434746066 59125760 13546 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13546 603 41 0 14394 0
vsize: 57740
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13628 0 0 0 109973 47 0 0 25 0 1 0 434746066 59125760 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13547 603 41 0 14394 0
vsize: 57740
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13628 0 0 0 110973 47 0 0 25 0 1 0 434746066 59125760 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13547 603 41 0 14394 0
vsize: 57740
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13628 0 0 0 111973 47 0 0 25 0 1 0 434746066 59125760 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13547 603 41 0 14394 0
vsize: 57740
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13629 0 0 0 112973 47 0 0 25 0 1 0 434746066 59125760 13548 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13548 603 41 0 14394 0
vsize: 57740
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13629 0 0 0 113973 47 0 0 25 0 1 0 434746066 59125760 13548 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13548 603 41 0 14394 0
vsize: 57740
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13630 0 0 0 114974 47 0 0 25 0 1 0 434746066 59125760 13549 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13549 603 41 0 14394 0
vsize: 57740
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13631 0 0 0 115974 47 0 0 25 0 1 0 434746066 59125760 13550 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14435 13550 603 41 0 14394 0
vsize: 57740
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13631 0 0 0 116974 47 0 0 25 0 1 0 434746066 59125760 13550 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14435 13550 603 41 0 14394 0
vsize: 57740
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13631 0 0 0 117974 47 0 0 25 0 1 0 434746066 59125760 13550 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14435 13550 603 41 0 14394 0
vsize: 57740
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13632 0 0 0 118974 47 0 0 25 0 1 0 434746066 59125760 13551 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14435 13551 603 41 0 14394 0
vsize: 57740
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.94 2/56 8206
Raw data (stat): 8198 (minisat+) R 8197 12452 12451 0 -1 0 13632 0 0 0 119974 47 0 0 25 0 1 0 434746066 59125760 13551 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14435 13551 603 41 0 14394 0
vsize: 57740
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.98 0.94 1/56 8206
Raw data (stat): 8198 (minisat+) Z 8197 12452 12451 0 -1 12 13634 0 0 0 119974 50 0 0 25 0 1 0 434746066 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: 0
Real time (s): 1200.09
CPU time (s): 1200.25
CPU user time (s): 1199.74
CPU system time (s): 0.504923
CPU usage (%): 100.013
Max. virtual memory (Kb): 57740
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####