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/miplib3/normalized-mps-v2-20-10-vpm1.opb
MD5SUM	eb50800dc2fc522dd2f29a347fbab1da
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	454.966
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 21055

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        415984 kB
Buffers:         27256 kB
Cached:         565228 kB
SwapCached:        408 kB
Active:         143024 kB
Inactive:       452012 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        415732 kB
SwapTotal:     2097892 kB
SwapFree:      2097056 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5860 kB
Slab:            17960 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 22:50:24 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 13946 7 1200.24 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.65 0.89 0.90 2/55 6797
Raw data (stat): 6797 (runsolver) R 6796 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548701250 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.99978 s]
Raw data (loadavg): 0.70 0.90 0.90 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 3430 0 0 0 990 8 0 0 25 0 1 0 548701250 16437248 3349 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4013 3349 603 41 0 3972 0
vsize: 16052
[startup+20.0008 s]
Raw data (loadavg): 0.75 0.90 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 4024 0 0 0 1988 10 0 0 25 0 1 0 548701250 18980864 3943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 3943 603 41 0 4593 0
vsize: 18536
[startup+30.0009 s]
Raw data (loadavg): 0.79 0.90 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 4354 0 0 0 2987 11 0 0 25 0 1 0 548701250 20316160 4273 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4960 4273 603 41 0 4919 0
vsize: 19840
[startup+40.0015 s]
Raw data (loadavg): 0.82 0.91 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 4635 0 0 0 3986 12 0 0 25 0 1 0 548701250 21401600 4554 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5225 4554 603 41 0 5184 0
vsize: 20900
[startup+50.0022 s]
Raw data (loadavg): 0.85 0.91 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 5504 0 0 0 4985 14 0 0 25 0 1 0 548701250 25161728 5423 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6143 5423 603 41 0 6102 0
vsize: 24572
[startup+60.0018 s]
Raw data (loadavg): 0.87 0.91 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 6302 0 0 0 5982 16 0 0 25 0 1 0 548701250 28385280 6221 4294967295 134512640 134672761 3221224544 3221223712 134560852 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.0048 s]
Raw data (loadavg): 0.89 0.91 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 6883 0 0 0 6982 17 0 0 25 0 1 0 548701250 30674944 6802 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7489 6802 603 41 0 7448 0
vsize: 29956
[startup+80.005 s]
Raw data (loadavg): 0.91 0.92 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 7376 0 0 0 7980 19 0 0 25 0 1 0 548701250 32714752 7295 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7987 7295 603 41 0 7946 0
vsize: 31948
[startup+90.0055 s]
Raw data (loadavg): 0.92 0.92 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 7714 0 0 0 8979 20 0 0 25 0 1 0 548701250 34066432 7633 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8317 7633 603 41 0 8276 0
vsize: 33268
[startup+100.006 s]
Raw data (loadavg): 0.93 0.92 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 8003 0 0 0 9977 22 0 0 25 0 1 0 548701250 35672064 7922 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8709 7922 603 41 0 8668 0
vsize: 34836
[startup+110.006 s]
Raw data (loadavg): 0.94 0.92 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 8301 0 0 0 10977 23 0 0 25 0 1 0 548701250 37044224 8220 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9044 8220 603 41 0 9003 0
vsize: 36176
[startup+120.006 s]
Raw data (loadavg): 0.95 0.92 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 8722 0 0 0 11975 25 0 0 25 0 1 0 548701250 38670336 8641 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9441 8641 603 41 0 9400 0
vsize: 37764
[startup+130.006 s]
Raw data (loadavg): 0.96 0.93 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 8953 0 0 0 12974 26 0 0 25 0 1 0 548701250 39612416 8872 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9671 8872 603 41 0 9630 0
vsize: 38684
[startup+140.007 s]
Raw data (loadavg): 0.96 0.93 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9265 0 0 0 13973 27 0 0 25 0 1 0 548701250 40828928 9184 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9968 9184 603 41 0 9927 0
vsize: 39872
[startup+150.007 s]
Raw data (loadavg): 0.97 0.93 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9418 0 0 0 14972 28 0 0 25 0 1 0 548701250 41500672 9337 4294967295 134512640 134672761 3221224544 3221223648 134554665 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.008 s]
Raw data (loadavg): 0.97 0.93 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9418 0 0 0 15972 28 0 0 25 0 1 0 548701250 41500672 9337 4294967295 134512640 134672761 3221224544 3221223640 134555595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10132 9337 603 41 0 10091 0
vsize: 40528
[startup+170.007 s]
Raw data (loadavg): 0.98 0.93 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9418 0 0 0 16972 29 0 0 25 0 1 0 548701250 41500672 9337 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10132 9337 603 41 0 10091 0
vsize: 40528
[startup+180.007 s]
Raw data (loadavg): 0.98 0.93 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9418 0 0 0 17972 29 0 0 25 0 1 0 548701250 41500672 9337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10132 9337 603 41 0 10091 0
vsize: 40528
[startup+190.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9418 0 0 0 18972 29 0 0 25 0 1 0 548701250 41500672 9337 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10132 9337 603 41 0 10091 0
vsize: 40528
[startup+200.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9419 0 0 0 19971 30 0 0 25 0 1 0 548701250 41500672 9338 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10132 9338 603 41 0 10091 0
vsize: 40528
[startup+210.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9419 0 0 0 20971 30 0 0 25 0 1 0 548701250 41500672 9338 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10132 9338 603 41 0 10091 0
vsize: 40528
[startup+220.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 6797
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9420 0 0 0 21971 31 0 0 25 0 1 0 548701250 41500672 9339 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10132 9339 603 41 0 10091 0
vsize: 40528
[startup+230.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9433 0 0 0 22970 31 0 0 25 0 1 0 548701250 41500672 9352 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10132 9352 603 41 0 10091 0
vsize: 40528
[startup+240.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9449 0 0 0 23970 31 0 0 25 0 1 0 548701250 41672704 9368 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10174 9368 603 41 0 10133 0
vsize: 40696
[startup+250.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9462 0 0 0 24970 31 0 0 25 0 1 0 548701250 41672704 9381 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10174 9381 603 41 0 10133 0
vsize: 40696
[startup+260.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9483 0 0 0 25970 32 0 0 25 0 1 0 548701250 41836544 9402 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10214 9402 603 41 0 10173 0
vsize: 40856
[startup+270.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9499 0 0 0 26970 32 0 0 25 0 1 0 548701250 41836544 9418 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10214 9418 603 41 0 10173 0
vsize: 40856
[startup+280.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9544 0 0 0 27970 32 0 0 25 0 1 0 548701250 42000384 9463 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10254 9463 603 41 0 10213 0
vsize: 41016
[startup+290.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9550 0 0 0 28970 32 0 0 25 0 1 0 548701250 42000384 9469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10254 9469 603 41 0 10213 0
vsize: 41016
[startup+300.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9563 0 0 0 29970 33 0 0 25 0 1 0 548701250 42196992 9482 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10302 9482 603 41 0 10261 0
vsize: 41208
[startup+310.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9565 0 0 0 30970 33 0 0 25 0 1 0 548701250 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+320.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9565 0 0 0 31970 33 0 0 25 0 1 0 548701250 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.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 9576 0 0 0 32969 34 0 0 25 0 1 0 548701250 42196992 9495 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10302 9495 603 41 0 10261 0
vsize: 41208
[startup+340.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10037 0 0 0 33968 35 0 0 25 0 1 0 548701250 44077056 9956 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10761 9956 603 41 0 10720 0
vsize: 43044
[startup+350.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10588 0 0 0 34966 37 0 0 25 0 1 0 548701250 46235648 10507 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11288 10507 603 41 0 11247 0
vsize: 45152
[startup+360.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10625 0 0 0 35966 38 0 0 25 0 1 0 548701250 46366720 10544 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10625 0 0 0 36966 38 0 0 25 0 1 0 548701250 46366720 10544 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10626 0 0 0 37965 39 0 0 25 0 1 0 548701250 46366720 10545 4294967295 134512640 134672761 3221224544 3221223712 134560980 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.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10626 0 0 0 38965 39 0 0 25 0 1 0 548701250 46366720 10545 4294967295 134512640 134672761 3221224544 3221223712 134561154 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.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10626 0 0 0 39966 39 0 0 25 0 1 0 548701250 46366720 10545 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10626 0 0 0 40966 39 0 0 25 0 1 0 548701250 46366720 10545 4294967295 134512640 134672761 3221224544 3221223712 134560937 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.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10626 0 0 0 41966 39 0 0 25 0 1 0 548701250 46366720 10545 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11320 10545 603 41 0 11279 0
vsize: 45280
[startup+430.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10631 0 0 0 42966 39 0 0 25 0 1 0 548701250 46366720 10550 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11320 10550 603 41 0 11279 0
vsize: 45280
[startup+440.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10639 0 0 0 43966 39 0 0 25 0 1 0 548701250 46514176 10558 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11356 10558 603 41 0 11315 0
vsize: 45424
[startup+450.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10641 0 0 0 44966 39 0 0 25 0 1 0 548701250 46514176 10560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11356 10560 603 41 0 11315 0
vsize: 45424
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10663 0 0 0 45966 39 0 0 25 0 1 0 548701250 46514176 10582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11356 10582 603 41 0 11315 0
vsize: 45424
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10666 0 0 0 46967 39 0 0 25 0 1 0 548701250 46514176 10585 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11356 10585 603 41 0 11315 0
vsize: 45424
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10692 0 0 0 47967 39 0 0 25 0 1 0 548701250 46710784 10611 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11404 10611 603 41 0 11363 0
vsize: 45616
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10728 0 0 0 48967 39 0 0 25 0 1 0 548701250 46874624 10647 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10647 603 41 0 11403 0
vsize: 45776
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10731 0 0 0 49967 39 0 0 25 0 1 0 548701250 46874624 10650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10650 603 41 0 11403 0
vsize: 45776
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10732 0 0 0 50967 39 0 0 25 0 1 0 548701250 46874624 10651 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10651 603 41 0 11403 0
vsize: 45776
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6799
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10732 0 0 0 51967 39 0 0 25 0 1 0 548701250 46874624 10651 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10651 603 41 0 11403 0
vsize: 45776
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10733 0 0 0 52967 39 0 0 25 0 1 0 548701250 46874624 10652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10652 603 41 0 11403 0
vsize: 45776
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10733 0 0 0 53968 39 0 0 25 0 1 0 548701250 46874624 10652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10652 603 41 0 11403 0
vsize: 45776
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10734 0 0 0 54968 39 0 0 25 0 1 0 548701250 46874624 10653 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10653 603 41 0 11403 0
vsize: 45776
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10734 0 0 0 55968 39 0 0 25 0 1 0 548701250 46874624 10653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10653 603 41 0 11403 0
vsize: 45776
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10734 0 0 0 56968 39 0 0 25 0 1 0 548701250 46874624 10653 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10653 603 41 0 11403 0
vsize: 45776
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10734 0 0 0 57968 39 0 0 25 0 1 0 548701250 46874624 10653 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11444 10653 603 41 0 11403 0
vsize: 45776
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10746 0 0 0 58969 39 0 0 25 0 1 0 548701250 47038464 10665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11484 10665 603 41 0 11443 0
vsize: 45936
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10757 0 0 0 59969 39 0 0 25 0 1 0 548701250 47038464 10676 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11484 10676 603 41 0 11443 0
vsize: 45936
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10765 0 0 0 60969 39 0 0 25 0 1 0 548701250 47038464 10684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11484 10684 603 41 0 11443 0
vsize: 45936
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10766 0 0 0 61969 40 0 0 25 0 1 0 548701250 47038464 10685 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11484 10685 603 41 0 11443 0
vsize: 45936
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10766 0 0 0 62970 40 0 0 25 0 1 0 548701250 47038464 10685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11484 10685 603 41 0 11443 0
vsize: 45936
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10766 0 0 0 63971 40 0 0 25 0 1 0 548701250 47038464 10685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11484 10685 603 41 0 11443 0
vsize: 45936
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10835 0 0 0 64970 40 0 0 25 0 1 0 548701250 47366144 10754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11564 10754 603 41 0 11523 0
vsize: 46256
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10846 0 0 0 65969 41 0 0 25 0 1 0 548701250 47529984 10765 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 10765 603 41 0 11563 0
vsize: 46416
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10856 0 0 0 66970 41 0 0 25 0 1 0 548701250 47529984 10775 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 10775 603 41 0 11563 0
vsize: 46416
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10858 0 0 0 67970 41 0 0 25 0 1 0 548701250 47529984 10777 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11604 10777 603 41 0 11563 0
vsize: 46416
[startup+690.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10878 0 0 0 68970 41 0 0 25 0 1 0 548701250 47726592 10797 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11652 10797 603 41 0 11611 0
vsize: 46608
[startup+700.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10887 0 0 0 69970 41 0 0 25 0 1 0 548701250 47726592 10806 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11652 10806 603 41 0 11611 0
vsize: 46608
[startup+710.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10896 0 0 0 70970 41 0 0 25 0 1 0 548701250 47726592 10815 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11652 10815 603 41 0 11611 0
vsize: 46608
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10896 0 0 0 71970 41 0 0 25 0 1 0 548701250 47726592 10815 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11652 10815 603 41 0 11611 0
vsize: 46608
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10896 0 0 0 72970 41 0 0 25 0 1 0 548701250 47726592 10815 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11652 10815 603 41 0 11611 0
vsize: 46608
[startup+740.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10896 0 0 0 73971 41 0 0 25 0 1 0 548701250 47726592 10815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11652 10815 603 41 0 11611 0
vsize: 46608
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10906 0 0 0 74971 41 0 0 25 0 1 0 548701250 47890432 10825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11692 10825 603 41 0 11651 0
vsize: 46768
[startup+760.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10914 0 0 0 75971 41 0 0 25 0 1 0 548701250 47890432 10833 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11692 10833 603 41 0 11651 0
vsize: 46768
[startup+770.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10914 0 0 0 76971 41 0 0 25 0 1 0 548701250 47890432 10833 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11692 10833 603 41 0 11651 0
vsize: 46768
[startup+780.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10914 0 0 0 77971 41 0 0 25 0 1 0 548701250 47890432 10833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11692 10833 603 41 0 11651 0
vsize: 46768
[startup+790.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10921 0 0 0 78971 42 0 0 25 0 1 0 548701250 47890432 10840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11692 10840 603 41 0 11651 0
vsize: 46768
[startup+800.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10930 0 0 0 79971 42 0 0 25 0 1 0 548701250 47890432 10849 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11692 10849 603 41 0 11651 0
vsize: 46768
[startup+810.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10930 0 0 0 80971 42 0 0 25 0 1 0 548701250 47890432 10849 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11692 10849 603 41 0 11651 0
vsize: 46768
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6801
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10933 0 0 0 81972 42 0 0 25 0 1 0 548701250 47890432 10852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11692 10852 603 41 0 11651 0
vsize: 46768
[startup+830.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10941 0 0 0 82972 42 0 0 25 0 1 0 548701250 48054272 10860 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11732 10860 603 41 0 11691 0
vsize: 46928
[startup+840.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10942 0 0 0 83972 42 0 0 25 0 1 0 548701250 48054272 10861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11732 10861 603 41 0 11691 0
vsize: 46928
[startup+850.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10955 0 0 0 84972 42 0 0 25 0 1 0 548701250 48054272 10874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11732 10874 603 41 0 11691 0
vsize: 46928
[startup+860.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 10970 0 0 0 85972 42 0 0 25 0 1 0 548701250 48209920 10889 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11770 10889 603 41 0 11729 0
vsize: 47080
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11033 0 0 0 86972 42 0 0 25 0 1 0 548701250 48345088 10952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11803 10952 603 41 0 11762 0
vsize: 47212
[startup+880.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11096 0 0 0 87972 42 0 0 25 0 1 0 548701250 48615424 11015 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11869 11015 603 41 0 11828 0
vsize: 47476
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11161 0 0 0 88972 42 0 0 25 0 1 0 548701250 48881664 11080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11934 11080 603 41 0 11893 0
vsize: 47736
[startup+900.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11224 0 0 0 89973 43 0 0 25 0 1 0 548701250 49147904 11143 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11999 11144 603 41 0 11958 0
vsize: 47996
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11287 0 0 0 90972 43 0 0 25 0 1 0 548701250 49414144 11206 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12064 11206 603 41 0 12023 0
vsize: 48256
[startup+920.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11349 0 0 0 91972 43 0 0 25 0 1 0 548701250 49676288 11268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12128 11268 603 41 0 12087 0
vsize: 48512
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11415 0 0 0 92972 43 0 0 25 0 1 0 548701250 49946624 11334 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12194 11334 603 41 0 12153 0
vsize: 48776
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11478 0 0 0 93972 44 0 0 25 0 1 0 548701250 50216960 11397 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12260 11397 603 41 0 12219 0
vsize: 49040
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11546 0 0 0 94972 44 0 0 25 0 1 0 548701250 50487296 11465 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12326 11465 603 41 0 12285 0
vsize: 49304
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11619 0 0 0 95972 44 0 0 25 0 1 0 548701250 50753536 11538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12391 11538 603 41 0 12350 0
vsize: 49564
[startup+970.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11695 0 0 0 96972 44 0 0 25 0 1 0 548701250 51159040 11614 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12490 11614 603 41 0 12449 0
vsize: 49960
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11767 0 0 0 97972 45 0 0 25 0 1 0 548701250 51535872 11686 4294967295 134512640 134672761 3221224544 3221223712 134560937 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.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11824 0 0 0 98972 45 0 0 25 0 1 0 548701250 51671040 11743 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12615 11743 603 41 0 12574 0
vsize: 50460
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 11905 0 0 0 99972 45 0 0 25 0 1 0 548701250 52129792 11824 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11824 603 41 0 12686 0
vsize: 50908
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 12219 0 0 0 100971 46 0 0 25 0 1 0 548701250 53354496 12138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13026 12138 603 41 0 12985 0
vsize: 52104
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 12844 0 0 0 101970 48 0 0 25 0 1 0 548701250 55889920 12763 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13645 12763 603 41 0 13604 0
vsize: 54580
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13301 0 0 0 102968 49 0 0 25 0 1 0 548701250 57778176 13220 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14106 13220 603 41 0 14065 0
vsize: 56424
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13626 0 0 0 103967 50 0 0 25 0 1 0 548701250 59125760 13545 4294967295 134512640 134672761 3221224544 3221223648 134554642 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13626 0 0 0 104968 50 0 0 25 0 1 0 548701250 59125760 13545 4294967295 134512640 134672761 3221224544 3221223728 134559405 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13626 0 0 0 105968 51 0 0 25 0 1 0 548701250 59125760 13545 4294967295 134512640 134672761 3221224544 3221223680 134560604 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13626 0 0 0 106968 51 0 0 25 0 1 0 548701250 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13626 0 0 0 107968 51 0 0 25 0 1 0 548701250 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13626 0 0 0 108968 51 0 0 25 0 1 0 548701250 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+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13628 0 0 0 109968 51 0 0 25 0 1 0 548701250 59125760 13547 4294967295 134512640 134672761 3221224544 3221223712 134560858 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13628 0 0 0 110969 51 0 0 25 0 1 0 548701250 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6803
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13628 0 0 0 111969 51 0 0 25 0 1 0 548701250 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6805
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13629 0 0 0 112969 51 0 0 25 0 1 0 548701250 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6805
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13629 0 0 0 113969 51 0 0 25 0 1 0 548701250 59125760 13548 4294967295 134512640 134672761 3221224544 3221223700 134561032 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6805
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13630 0 0 0 114969 51 0 0 25 0 1 0 548701250 59125760 13549 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6805
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13631 0 0 0 115969 51 0 0 25 0 1 0 548701250 59125760 13550 4294967295 134512640 134672761 3221224544 3221223712 134560903 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6805
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13631 0 0 0 116968 51 0 0 25 0 1 0 548701250 59125760 13550 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13550 603 41 0 14394 0
vsize: 57740
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6805
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13631 0 0 0 117969 51 0 0 25 0 1 0 548701250 59125760 13550 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13550 603 41 0 14394 0
vsize: 57740
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6805
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13632 0 0 0 118969 51 0 0 25 0 1 0 548701250 59125760 13551 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13551 603 41 0 14394 0
vsize: 57740
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 6805
Raw data (stat): 6797 (minisat+) R 6796 20838 20837 0 -1 0 13632 0 0 0 119969 51 0 0 25 0 1 0 548701250 59125760 13551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14435 13551 603 41 0 14394 0
vsize: 57740
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 6805
Raw data (stat): 6797 (minisat+) Z 6796 20838 20837 0 -1 12 13634 0 0 0 119969 54 0 0 25 0 1 0 548701250 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.06
CPU time (s): 1200.24
CPU user time (s): 1199.7
CPU system time (s): 0.540917
CPU usage (%): 100.014
Max. virtual memory (Kb): 57740
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####