PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-pp08aCUTS.opb
MD5SUM	fa6454a9831f2da4180d8bfab7c0a21b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	2304
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	178464600
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	178464600
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.037993
Number of variables	3288
Total number of constraints	310
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	310
Minimum length of a constraint	14
Maximum length of a constraint	123
Trace number 17957

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 12:53:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18769 boxname=wulflinc21 idbench=1444 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fa6454a9831f2da4180d8bfab7c0a21b  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-pp08aCUTS.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-pp08aCUTS.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-pp08aCUTS.opb
IDLAUNCH: 18769
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        871260 kB
Buffers:          1428 kB
Cached:         139672 kB
SwapCached:          0 kB
Active:          16944 kB
Inactive:       127060 kB
HighTotal:      131008 kB
HighFree:        85344 kB
LowTotal:       903652 kB
LowFree:        785916 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            13636 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:13:11 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 18769 7 1200.2 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 374 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[ 501]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 500]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 499]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 498]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 497]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 496]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 495]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 494]---> Adder-cost: 51   maxlim: 11774   bits: 15/14
c ---[ 485]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 484]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 483]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 482]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 481]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 480]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 479]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 477]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 476]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 475]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 474]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 473]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 472]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 471]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 469]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 468]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 467]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 466]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 465]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 464]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 463]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 462]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 461]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 460]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 459]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 458]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 457]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 456]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 455]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 454]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 445]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 444]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 443]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 442]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 441]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 440]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 439]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 438]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 437]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[ 436]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[ 435]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[ 434]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 433]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 432]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 431]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 430]---> Adder-cost: 218   maxlim: 312823   bits: 19/19
c ---[ 428]---> Adder-cost: 80   maxlim: 1114110   bits: 22/21
c ---[ 426]---> Adder-cost: 160   maxlim: 2153725   bits: 23/22
c ---[ 424]---> Adder-cost: 160   maxlim: 2156285   bits: 23/22
c ---[ 422]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 420]---> Adder-cost: 160   maxlim: 2160125   bits: 23/22
c ---[ 418]---> Adder-cost: 160   maxlim: 2152445   bits: 23/22
c ---[ 416]---> Adder-cost: 160   maxlim: 2162685   bits: 23/22
c ---[ 414]---> Adder-cost: 80   maxlim: 1101310   bits: 22/21
c ---[ 412]---> Adder-cost: 80   maxlim: 1078782   bits: 22/21
c ---[ 410]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 408]---> Adder-cost: 160   maxlim: 2123517   bits: 23/22
c ---[ 406]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 404]---> Adder-cost: 160   maxlim: 2126077   bits: 23/22
c ---[ 402]---> Adder-cost: 160   maxlim: 2129917   bits: 23/22
c ---[ 400]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 398]---> Adder-cost: 80   maxlim: 1074942   bits: 22/21
c ---[ 396]---> Adder-cost: 80   maxlim: 1108990   bits: 22/21
c ---[ 394]---> Adder-cost: 160   maxlim: 2156285   bits: 23/22
c ---[ 392]---> Adder-cost: 160   maxlim: 2162685   bits: 23/22
c ---[ 390]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 388]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 386]---> Adder-cost: 160   maxlim: 2152445   bits: 23/22
c ---[ 384]---> Adder-cost: 160   maxlim: 2151165   bits: 23/22
c ---[ 382]---> Adder-cost: 80   maxlim: 1093630   bits: 22/21
c ---[ 380]---> Adder-cost: 80   maxlim: 1114110   bits: 22/21
c ---[ 378]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 376]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 374]---> Adder-cost: 160   maxlim: 2143485   bits: 23/22
c ---[ 372]---> Adder-cost: 160   maxlim: 2142205   bits: 23/22
c ---[ 370]---> Adder-cost: 160   maxlim: 2151165   bits: 23/22
c ---[ 368]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 366]---> Adder-cost: 80   maxlim: 1101310   bits: 22/21
c ---[ 364]---> Adder-cost: 80   maxlim: 1074942   bits: 22/21
c ---[ 362]---> Adder-cost: 160   maxlim: 2129917   bits: 23/22
c ---[ 360]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 358]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 356]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 354]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 352]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 350]---> Adder-cost: 80   maxlim: 1080062   bits: 22/21
c ---[ 348]---> Adder-cost: 80   maxlim: 1105150   bits: 22/21
c ---[ 346]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 344]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 342]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 340]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 338]---> Adder-cost: 160   maxlim: 2160125   bits: 23/22
c ---[ 336]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 334]---> Adder-cost: 80   maxlim: 1107710   bits: 22/21
c ---[ 332]---> Adder-cost: 80   maxlim: 1081342   bits: 22/21
c ---[ 330]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 328]---> Adder-cost: 160   maxlim: 2123517   bits: 23/22
c ---[ 326]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 324]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 322]---> Adder-cost: 160   maxlim: 2122237   bits: 23/22
c ---[ 320]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 318]---> Adder-cost: 80   maxlim: 1076222   bits: 22/21
c ---[ 316]---> Adder-cost: 80   maxlim: 1063678   bits: 22/21
c ---[ 314]---> Adder-cost: 160   maxlim: 2110973   bits: 23/22
c ---[ 312]---> Adder-cost: 160   maxlim: 2113533   bits: 23/22
c ---[ 310]---> Adder-cost: 160   maxlim: 2113533   bits: 23/22
c ---[ 308]---> Adder-cost: 160   maxlim: 2112253   bits: 23/22
c ---[ 306]---> Adder-cost: 160   maxlim: 2112253   bits: 23/22
c ---[ 304]---> Adder-cost: 160   maxlim: 2110973   bits: 23/22
c ---[ 302]---> Adder-cost: 80   maxlim: 1061118   bits: 22/21
c ---[ 301]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 300]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 299]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 298]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 297]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 296]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 295]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 294]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 293]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 292]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 291]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 290]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 289]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 288]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 287]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 286]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 285]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 284]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 283]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 282]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 281]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 280]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 279]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 278]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 277]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 276]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 275]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 274]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 273]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 272]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 271]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 270]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 269]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 268]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 267]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 266]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 265]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 264]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 263]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 262]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 261]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 260]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 259]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 258]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 257]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 256]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 255]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 254]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 253]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 252]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 251]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 250]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 249]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 248]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 247]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 246]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 245]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 244]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 243]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 242]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 241]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 240]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 239]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 238]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 127]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 126]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 125]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 124]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 123]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 122]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 121]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 120]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 119]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[ 118]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[ 117]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 115]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 114]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 113]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 112]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 111]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 110]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 109]---> Adder-cost: 41   maxlim: 8959   bits: 15/14
c ---[ 108]---> Adder-cost: 107   maxlim: 65534   bits: 17/16
c ---[ 107]---> Adder-cost: 68   maxlim: 16382   bits: 15/14
c ---[ 106]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[ 105]---> Adder-cost: 95   maxlim: 16382   bits: 15/14
c ---[ 104]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[ 103]---> Adder-cost: 97   maxlim: 16382   bits: 15/14
c ---[ 102]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[ 101]---> Adder-cost: 97   maxlim: 16382   bits: 15/14
c ---[ 100]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  99]---> Adder-cost: 95   maxlim: 16382   bits: 15/14
c ---[  98]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[  97]---> Adder-cost: 10   maxlim: 12799   bits: 15/14
c ---[  96]---> Adder-cost: 68   maxlim: 16382   bits: 15/14
c ---[  95]---> Adder-cost: 78   maxlim: 65534   bits: 17/16
c ---[  94]---> Adder-cost: 6   maxlim: 2559   bits: 13/12
c ---[  93]---> Adder-cost: 72   maxlim: 32766   bits: 16/15
c ---[  92]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  91]---> Adder-cost: 101   maxlim: 32766   bits: 16/15
c ---[  90]---> Adder-cost: 37   maxlim: 6399   bits: 14/13
c ---[  89]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  88]---> Adder-cost: 33   maxlim: 3839   bits: 13/12
c ---[  87]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[  86]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  85]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[  84]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  83]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  82]---> Adder-cost: 101   maxlim: 32766   bits: 16/15
c ---[  81]---> Adder-cost: 10   maxlim: 6399   bits: 14/13
c ---[  80]---> Adder-cost: 74   maxlim: 32766   bits: 16/15
c ---[  79]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[  78]---> Adder-cost: 76   maxlim: 65534   bits: 17/16
c ---[  77]---> Adder-cost: 37   maxlim: 6399   bits: 14/13
c ---[  76]---> Adder-cost: 37   maxlim: 6399   bits: 14/13
c ---[  75]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[  74]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  73]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  72]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  71]---> Adder-cost: 109   maxlim: 65534   bits: 17/16
c ---[  70]---> Adder-cost: 35   maxlim: 10239   bits: 15/14
c ---[  69]---> Adder-cost: 107   maxlim: 65534   bits: 17/16
c ---[  68]---> Adder-cost: 41   maxlim: 11519   bits: 15/14
c ---[  67]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[  66]---> Adder-cost: 6   maxlim: 20479   bits: 16/15
c ---[  65]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[  64]---> Adder-cost: 72   maxlim: 65534   bits: 17/16
c ---[  63]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  62]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  61]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  60]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  59]---> Adder-cost: 45   maxlim: 19199   bits: 16/15
c ---[  58]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[  57]---> Adder-cost: 37   maxlim: 20479   bits: 16/15
c ---[  56]---> Adder-cost: 105   maxlim: 65534   bits: 17/16
c ---[  55]---> Adder-cost: 41   maxlim: 11519   bits: 15/14
c ---[  54]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  53]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[  52]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  51]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  50]---> Adder-cost: 10   maxlim: 12799   bits: 15/14
c ---[  49]---> Adder-cost: 78   maxlim: 65534   bits: 17/16
c ---[  48]---> Adder-cost: 10   maxlim: 6399   bits: 14/13
c ---[  47]---> Adder-cost: 74   maxlim: 32766   bits: 16/15
c ---[  46]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  45]---> Adder-cost: 103   maxlim: 32766   bits: 16/15
c ---[  44]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  43]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  42]---> Adder-cost: 101   maxlim: 32766   bits: 16/15
c ---[  41]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[  40]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  39]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[  38]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  37]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  36]---> Adder-cost: 103   maxlim: 32766   bits: 16/15
c ---[  35]---> Adder-cost: 6   maxlim: 1279   bits: 12/11
c ---[  34]---> Adder-cost: 74   maxlim: 32766   bits: 16/15
c ---[  33]---> Adder-cost: 12   maxlim: 8959   bits: 15/14
c ---[  32]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  31]---> Adder-cost: 80   maxlim: 65534   bits: 17/16
c ---[  30]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  29]---> Adder-cost: 109   maxlim: 65534   bits: 17/16
c ---[  28]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  27]---> Adder-cost: 109   maxlim: 65534   bits: 17/16
c ---[  26]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  25]---> Adder-cost: 109   maxlim: 65534   bits: 17/16
c ---[  24]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  23]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  22]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  21]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  20]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  19]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  18]---> Adder-cost: 109   maxlim: 65534   bits: 17/16
c ---[  17]---> Adder-cost: 10   maxlim: 6399   bits: 14/13
c ---[  16]---> Adder-cost: 80   maxlim: 65534   bits: 17/16
c ---[  15]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  14]---> Adder-cost: 103   maxlim: 32766   bits: 16/15
c ---[  13]---> Adder-cost: 37   maxlim: 6399   bits: 14/13
c ---[  12]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  11]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[  10]---> Adder-cost: 35   maxlim: 10239   bits: 15/14
c ---[   9]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[   8]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[   7]---> Adder-cost: 103   maxlim: 32766   bits: 16/15
c ---[   6]---> Adder-cost: 35   maxlim: 7679   bits: 14/13
c ---[   5]---> Adder-cost: 103   maxlim: 32766   bits: 16/15
c ---[   4]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[   3]---> Adder-cost: 101   maxlim: 32766   bits: 16/15
c ---[   2]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[   1]---> Adder-cost: 70   maxlim: 32766   bits: 16/15
c ---[   0]---> Adder-cost: 6   maxlim: 1279   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  126353   460481 |   42117       0        0     nan |  0.000 % |
c |       100 |  126353   460481 |   46328     100      445     4.5 | 20.451 % |
c |       250 |  126353   460481 |   50961     250     1102     4.4 | 20.451 % |
c |       475 |  126353   460481 |   56057     475     2745     5.8 | 20.451 % |
c |       812 |  126345   460455 |   61663     811     4177     5.2 | 20.454 % |
c |      1318 |  126284   460258 |   67829    1308     6792     5.2 | 20.483 % |
c |      2077 |  126263   460191 |   74612    2064    10611     5.1 | 20.494 % |
c |      3216 |  126188   459946 |   82074    3182    15942     5.0 | 20.530 % |
c |      4925 |  126129   459755 |   90281    4880    24855     5.1 | 20.559 % |
c |      7487 |  126006   459356 |   99309    7413    40435     5.5 | 20.620 % |
c |     11331 |  125818   458744 |  109240   11217    63332     5.6 | 20.718 % |
c |     17097 |  125691   458329 |  120164   16949   109930     6.5 | 20.782 % |
c |     25747 |  125544   457840 |  132181   25555   175045     6.8 | 20.862 % |
c |     38721 |  125384   457318 |  145399   38493   298212     7.7 | 20.941 % |
c |     58182 |  125110   456422 |  159939   57894   492519     8.5 | 21.103 % |
c |     87375 |  125032   456160 |  175933   87053   810772     9.3 | 21.150 % |
c |    131165 |  124888   455690 |  193526  130816  1278894     9.8 | 21.226 % |
c |    196850 |  124825   455483 |  212879  196483  2122190    10.8 | 21.258 % |
c |    295377 |  124788   455362 |  234167  107705  1136498    10.6 | 21.280 % |
c |    443166 |  124781   455339 |  257583   47408   412756     8.7 | 21.284 % |
c |    664849 |  124680   455012 |  283342   44591   351260     7.9 | 21.348 % |
#### 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.68 0.89 0.89 2/55 11712
Raw data (stat): 11712 (runsolver) R 11711 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 422492992 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.73 0.90 0.89 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 3834 0 0 0 989 10 0 0 25 0 1 0 422492992 17534976 3680 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4281 3680 603 41 0 4240 0
vsize: 17124
[startup+20.0012 s]
Raw data (loadavg): 0.77 0.90 0.89 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 4050 0 0 0 1987 12 0 0 25 0 1 0 422492992 18415616 3896 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4496 3896 603 41 0 4455 0
vsize: 17984
[startup+30.0014 s]
Raw data (loadavg): 0.81 0.90 0.89 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 4245 0 0 0 2986 13 0 0 25 0 1 0 422492992 19218432 4091 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4692 4091 603 41 0 4651 0
vsize: 18768
[startup+40.0016 s]
Raw data (loadavg): 0.84 0.91 0.89 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 4404 0 0 0 3985 14 0 0 25 0 1 0 422492992 19886080 4250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4855 4250 603 41 0 4814 0
vsize: 19420
[startup+50.0023 s]
Raw data (loadavg): 0.86 0.91 0.89 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 4649 0 0 0 4984 15 0 0 25 0 1 0 422492992 20832256 4495 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5086 4495 603 41 0 5045 0
vsize: 20344
[startup+60.003 s]
Raw data (loadavg): 0.88 0.91 0.89 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 4896 0 0 0 5984 15 0 0 25 0 1 0 422492992 22040576 4742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5381 4742 603 41 0 5340 0
vsize: 21524
[startup+70.0036 s]
Raw data (loadavg): 0.90 0.91 0.89 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 5165 0 0 0 6983 17 0 0 25 0 1 0 422492992 23121920 5011 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5645 5011 603 41 0 5604 0
vsize: 22580
[startup+80.0037 s]
Raw data (loadavg): 0.91 0.92 0.89 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 5339 0 0 0 7982 18 0 0 25 0 1 0 422492992 23797760 5185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5810 5185 603 41 0 5769 0
vsize: 23240
[startup+90.0045 s]
Raw data (loadavg): 0.93 0.92 0.89 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 5514 0 0 0 8981 18 0 0 25 0 1 0 422492992 24473600 5360 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5975 5360 603 41 0 5934 0
vsize: 23900
[startup+100.005 s]
Raw data (loadavg): 0.94 0.92 0.89 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 5688 0 0 0 9981 19 0 0 25 0 1 0 422492992 25145344 5534 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6139 5534 603 41 0 6098 0
vsize: 24556
[startup+110.005 s]
Raw data (loadavg): 0.95 0.92 0.90 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 5844 0 0 0 10980 20 0 0 25 0 1 0 422492992 25821184 5690 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6304 5690 603 41 0 6263 0
vsize: 25216
[startup+120.006 s]
Raw data (loadavg): 0.95 0.92 0.90 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 6020 0 0 0 11979 21 0 0 25 0 1 0 422492992 26492928 5866 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6468 5866 603 41 0 6427 0
vsize: 25872
[startup+130.006 s]
Raw data (loadavg): 0.96 0.93 0.90 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 6163 0 0 0 12979 21 0 0 25 0 1 0 422492992 27033600 6009 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6600 6009 603 41 0 6559 0
vsize: 26400
[startup+140.007 s]
Raw data (loadavg): 0.97 0.93 0.90 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 6338 0 0 0 13978 22 0 0 25 0 1 0 422492992 28229632 6184 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6892 6184 603 41 0 6851 0
vsize: 27568
[startup+150.007 s]
Raw data (loadavg): 0.97 0.93 0.90 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 6501 0 0 0 14978 23 0 0 25 0 1 0 422492992 28905472 6347 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7057 6347 603 41 0 7016 0
vsize: 28228
[startup+160.008 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 6641 0 0 0 15977 23 0 0 25 0 1 0 422492992 29446144 6487 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7189 6487 603 41 0 7148 0
vsize: 28756
[startup+170.007 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 6915 0 0 0 16977 24 0 0 25 0 1 0 422492992 30531584 6761 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7454 6761 603 41 0 7413 0
vsize: 29816
[startup+180.007 s]
Raw data (loadavg): 0.98 0.94 0.90 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 7035 0 0 0 17977 24 0 0 25 0 1 0 422492992 30937088 6881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7553 6881 603 41 0 7512 0
vsize: 30212
[startup+190.008 s]
Raw data (loadavg): 0.98 0.94 0.90 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 7242 0 0 0 18975 26 0 0 25 0 1 0 422492992 31748096 7088 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7751 7088 603 41 0 7710 0
vsize: 31004
[startup+200.008 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 7376 0 0 0 19975 27 0 0 25 0 1 0 422492992 32288768 7222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7883 7222 603 41 0 7842 0
vsize: 31532
[startup+210.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 7518 0 0 0 20974 27 0 0 25 0 1 0 422492992 32821248 7364 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8013 7364 603 41 0 7972 0
vsize: 32052
[startup+220.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 7762 0 0 0 21974 28 0 0 25 0 1 0 422492992 33763328 7608 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8243 7608 603 41 0 8202 0
vsize: 32972
[startup+230.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 7916 0 0 0 22974 28 0 0 25 0 1 0 422492992 34439168 7762 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8408 7762 603 41 0 8367 0
vsize: 33632
[startup+240.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8067 0 0 0 23973 29 0 0 25 0 1 0 422492992 34979840 7913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8540 7913 603 41 0 8499 0
vsize: 34160
[startup+250.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8236 0 0 0 24973 29 0 0 25 0 1 0 422492992 35651584 8082 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8704 8082 603 41 0 8663 0
vsize: 34816
[startup+260.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 25972 30 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223668 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+270.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 26973 30 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+280.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 27972 30 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+290.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 28972 30 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+300.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 29972 30 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+310.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 30972 31 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+320.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 31972 31 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+330.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 32972 31 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+340.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 33972 31 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+350.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 34972 31 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+360.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 35972 31 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+370.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 36972 31 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+380.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 37972 31 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+390.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 38972 32 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223680 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+400.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 39972 32 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+410.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11712
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 40972 32 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+420.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11765
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8421 0 0 0 41971 33 0 0 25 0 1 0 422492992 36458496 8267 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8901 8267 603 41 0 8860 0
vsize: 35604
[startup+430.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11765
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8520 0 0 0 42970 34 0 0 25 0 1 0 422492992 36864000 8366 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9000 8366 603 41 0 8959 0
vsize: 36000
[startup+440.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11765
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8858 0 0 0 43970 35 0 0 25 0 1 0 422492992 38211584 8704 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9329 8704 603 41 0 9288 0
vsize: 37316
[startup+450.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11765
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 8985 0 0 0 44969 35 0 0 25 0 1 0 422492992 38752256 8831 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9461 8831 603 41 0 9420 0
vsize: 37844
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11765
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9122 0 0 0 45969 36 0 0 25 0 1 0 422492992 39288832 8968 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9592 8968 603 41 0 9551 0
vsize: 38368
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11765
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9267 0 0 0 46968 36 0 0 25 0 1 0 422492992 39821312 9113 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9722 9113 603 41 0 9681 0
vsize: 38888
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9387 0 0 0 47968 37 0 0 25 0 1 0 422492992 40361984 9233 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9854 9233 603 41 0 9813 0
vsize: 39416
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9553 0 0 0 48967 38 0 0 25 0 1 0 422492992 41033728 9399 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10018 9399 603 41 0 9977 0
vsize: 40072
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9687 0 0 0 49967 38 0 0 25 0 1 0 422492992 41574400 9533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9533 603 41 0 10109 0
vsize: 40600
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 50967 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223648 134554629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 51967 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223728 134558382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 52967 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 53967 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 54968 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 55968 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 56968 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 57968 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 58968 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223744 134557892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 59969 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 60969 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223708 134565156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 61969 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 62969 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 63969 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 64970 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 65970 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 66970 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 67970 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 68970 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 69971 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 70971 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11769
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 71971 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 72971 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 73971 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 74971 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 75972 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9859 0 0 0 76972 39 0 0 25 0 1 0 422492992 42250240 9705 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9705 603 41 0 10274 0
vsize: 41260
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9860 0 0 0 77972 39 0 0 25 0 1 0 422492992 42250240 9706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9706 603 41 0 10274 0
vsize: 41260
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9862 0 0 0 78972 39 0 0 25 0 1 0 422492992 42250240 9708 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10315 9708 603 41 0 10274 0
vsize: 41260
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 9949 0 0 0 79972 39 0 0 25 0 1 0 422492992 42520576 9795 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10381 9795 603 41 0 10340 0
vsize: 41524
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10084 0 0 0 80972 39 0 0 25 0 1 0 422492992 43061248 9930 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10513 9930 603 41 0 10472 0
vsize: 42052
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10217 0 0 0 81972 39 0 0 25 0 1 0 422492992 43597824 10063 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10644 10063 603 41 0 10603 0
vsize: 42576
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 82972 39 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 83972 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 84972 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 85972 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 86972 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 87972 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 88972 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 89972 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 90972 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 91973 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 92973 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 93973 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 94973 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 95973 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+970.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 96973 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 97974 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+990.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 98974 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 99974 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 100974 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 101974 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 102974 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 103975 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 104975 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 105975 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 106975 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 107975 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 108975 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10266 0 0 0 109976 40 0 0 25 0 1 0 422492992 44781568 10112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10933 10112 603 41 0 10892 0
vsize: 43732
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10349 0 0 0 110976 40 0 0 25 0 1 0 422492992 45187072 10195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11032 10195 603 41 0 10991 0
vsize: 44128
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10467 0 0 0 111975 40 0 0 25 0 1 0 422492992 45727744 10313 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11164 10313 603 41 0 11123 0
vsize: 44656
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10571 0 0 0 112975 41 0 0 25 0 1 0 422492992 46133248 10417 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11263 10417 603 41 0 11222 0
vsize: 45052
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10681 0 0 0 113975 41 0 0 25 0 1 0 422492992 46538752 10527 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11362 10527 603 41 0 11321 0
vsize: 45448
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10810 0 0 0 114975 42 0 0 25 0 1 0 422492992 47079424 10656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11494 10656 603 41 0 11453 0
vsize: 45976
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 10926 0 0 0 115975 42 0 0 25 0 1 0 422492992 47484928 10772 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11593 10772 603 41 0 11552 0
vsize: 46372
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 11067 0 0 0 116974 43 0 0 25 0 1 0 422492992 48021504 10913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11724 10913 603 41 0 11683 0
vsize: 46896
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 11186 0 0 0 117974 43 0 0 25 0 1 0 422492992 48562176 11032 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11856 11032 603 41 0 11815 0
vsize: 47424
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 11203 0 0 0 118974 43 0 0 25 0 1 0 422492992 48562176 11049 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11856 11049 603 41 0 11815 0
vsize: 47424
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11771
Raw data (stat): 11712 (minisat+) R 11711 30927 30926 0 -1 0 11203 0 0 0 119974 43 0 0 25 0 1 0 422492992 48562176 11049 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11856 11049 603 41 0 11815 0
vsize: 47424
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 11771
Raw data (stat): 11712 (minisat+) Z 11711 30927 30926 0 -1 12 11205 0 0 0 119974 45 0 0 25 0 1 0 422492992 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.04
CPU time (s): 1200.2
CPU user time (s): 1199.74
CPU system time (s): 0.45993
CPU usage (%): 100.014
Max. virtual memory (Kb): 47424
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####