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-vpm2.opb
MD5SUM	766b2fe57cb2084b069363491485612e
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	97
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	5
Number of bits for the biggest coefficient in the objective function	3
Sum of the numbers in the objective function	504
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	16000000
Number of bits of the biggest number in a constraint	24
Biggest sum of numbers in a constraint	241094849
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.23
Number of variables	2754
Total number of constraints	444
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	444
Minimum length of a constraint	11
Maximum length of a constraint	84
Trace number 13787

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-20 21:45:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13959 boxname=wulflinc28 idbench=1074 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  766b2fe57cb2084b069363491485612e  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-vpm2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-vpm2.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-vpm2.opb
IDLAUNCH: 13959
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        651792 kB
Buffers:         33448 kB
Cached:         315840 kB
SwapCached:        164 kB
Active:          79684 kB
Inactive:       272044 kB
HighTotal:      131008 kB
HighFree:         2100 kB
LowTotal:       903652 kB
LowFree:        649692 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6088 kB
Slab:            25556 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 22:05:15 (client local time) WITH STATUS 0 IN 1200.51 SECONDS
stats: 13959 7 1200.51 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: 304   maxlim: 49172973   bits: 26/26
c ---[ 190]---> Adder-cost: 530   maxlim: 81141723   bits: 27/27
c ---[ 189]---> Adder-cost: 532   maxlim: 89141723   bits: 27/27
c ---[ 188]---> Adder-cost: 634   maxlim: 113110473   bits: 27/27
c ---[ 187]---> Adder-cost: 874   maxlim: 161094848   bits: 28/28
c ---[ 186]---> Adder-cost: 836   maxlim: 121094848   bits: 28/27
c ---[ 185]---> Adder-cost: 236   maxlim: 10052501   bits: 24/24
c ---[ 184]---> Adder-cost: 426   maxlim: 16446251   bits: 25/24
c ---[ 183]---> Adder-cost: 432   maxlim: 18046251   bits: 25/25
c ---[ 182]---> Adder-cost: 516   maxlim: 19640001   bits: 25/25
c ---[ 181]---> Adder-cost: 694   maxlim: 26036876   bits: 25/25
c ---[ 180]---> Adder-cost: 702   maxlim: 27636876   bits: 25/25
c ---[ 179]---> Adder-cost: 80   maxlim: 18933   bits: 15/15
c ---[ 178]---> Adder-cost: 162   maxlim: 29163   bits: 16/15
c ---[ 177]---> Adder-cost: 156   maxlim: 30443   bits: 16/15
c ---[ 176]---> Adder-cost: 210   maxlim: 38113   bits: 16/16
c ---[ 175]---> Adder-cost: 268   maxlim: 48348   bits: 16/16
c ---[ 174]---> Adder-cost: 262   maxlim: 45788   bits: 16/16
c ---[ 173]---> Adder-cost: 40   maxlim: 3965   bits: 13/12
c ---[ 172]---> Adder-cost: 78   maxlim: 4987   bits: 13/13
c ---[ 171]---> Adder-cost: 80   maxlim: 6267   bits: 13/13
c ---[ 170]---> Adder-cost: 112   maxlim: 6521   bits: 13/13
c ---[ 169]---> Adder-cost: 138   maxlim: 9592   bits: 14/14
c ---[ 168]---> Adder-cost: 134   maxlim: 8056   bits: 14/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 |  149912   544418 |   49970       0        0     nan |  0.000 % |
c |       101 |  149912   544418 |   54967     101      680     6.7 | 17.037 % |
c |       252 |  149905   544394 |   60463     251     1496     6.0 | 17.041 % |
c |       477 |  149905   544394 |   66510     476     3081     6.5 | 17.041 % |
c |       814 |  149898   544371 |   73161     811     6251     7.7 | 17.044 % |
c |      1321 |  149890   544345 |   80477    1317    13396    10.2 | 17.048 % |
c |      2080 |  149882   544319 |   88524    2075    23354    11.3 | 17.051 % |
c |      3219 |  149882   544319 |   97377    3214    53373    16.6 | 17.051 % |
c |      4927 |  149867   544270 |  107115    4919    79777    16.2 | 17.058 % |
c |      7489 |  149867   544270 |  117826    7481   152100    20.3 | 17.058 % |
c |     11334 |  149827   544136 |  129609   11320   235904    20.8 | 17.083 % |
c |     17100 |  149648   543521 |  142570   17054   351472    20.6 | 17.146 % |
c |     25749 |  149599   543358 |  156827   25693   572493    22.3 | 17.171 % |
c |     38723 |  149557   543221 |  172509   38661   914995    23.7 | 17.199 % |
c |     58184 |  149426   542760 |  189760   58117  1505405    25.9 | 17.234 % |
c |     87378 |  149394   542654 |  208737   87303  2409064    27.6 | 17.251 % |
c |    131168 |  149389   542638 |  229610  131091  3684918    28.1 | 17.255 % |
c |    196855 |  149202   541997 |  252571  196728  5638833    28.7 | 17.315 % |
c |    295381 |  149165   541880 |  277829   58328  1719804    29.5 | 17.339 % |
c |    443171 |  148810   540632 |  305611  205869  6622662    32.2 | 17.396 % |
#### 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.49 0.82 0.87 2/54 9286
Raw data (stat): 9286 (runsolver) R 9285 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539785753 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.56 0.83 0.87 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 4385 0 0 0 987 12 0 0 25 0 1 0 539785753 20066304 4221 4294967295 134512640 134672761 3221224544 3221223808 134562492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4899 4221 603 41 0 4858 0
vsize: 19596
[startup+20.0003 s]
Raw data (loadavg): 0.63 0.83 0.87 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 5021 0 0 0 1985 14 0 0 25 0 1 0 539785753 22749184 4857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5554 4857 603 41 0 5513 0
vsize: 22216
[startup+30.0012 s]
Raw data (loadavg): 0.69 0.84 0.87 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 5404 0 0 0 2983 16 0 0 25 0 1 0 539785753 24358912 5240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5947 5240 603 41 0 5906 0
vsize: 23788
[startup+40.0009 s]
Raw data (loadavg): 0.73 0.84 0.87 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 5717 0 0 0 3983 16 0 0 25 0 1 0 539785753 25575424 5553 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6244 5553 603 41 0 6203 0
vsize: 24976
[startup+50.0014 s]
Raw data (loadavg): 0.77 0.85 0.87 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 5983 0 0 0 4982 17 0 0 25 0 1 0 539785753 26923008 5819 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6573 5819 603 41 0 6532 0
vsize: 26292
[startup+60.001 s]
Raw data (loadavg): 0.81 0.85 0.87 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 6221 0 0 0 5981 18 0 0 25 0 1 0 539785753 27865088 6057 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6803 6057 603 41 0 6762 0
vsize: 27212
[startup+70.001 s]
Raw data (loadavg): 0.84 0.86 0.87 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 6513 0 0 0 6981 19 0 0 25 0 1 0 539785753 28975104 6349 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7074 6349 603 41 0 7033 0
vsize: 28296
[startup+80.0014 s]
Raw data (loadavg): 0.86 0.86 0.87 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 6678 0 0 0 7981 19 0 0 25 0 1 0 539785753 29638656 6514 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7236 6514 603 41 0 7195 0
vsize: 28944
[startup+90.0011 s]
Raw data (loadavg): 0.88 0.86 0.87 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 6850 0 0 0 8980 20 0 0 25 0 1 0 539785753 30478336 6686 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7441 6686 603 41 0 7400 0
vsize: 29764
[startup+100.001 s]
Raw data (loadavg): 0.90 0.87 0.88 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 7071 0 0 0 9980 20 0 0 25 0 1 0 539785753 31289344 6907 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7639 6907 603 41 0 7598 0
vsize: 30556
[startup+110 s]
Raw data (loadavg): 0.92 0.87 0.88 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 7236 0 0 0 10979 21 0 0 25 0 1 0 539785753 31956992 7072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7802 7072 603 41 0 7761 0
vsize: 31208
[startup+120 s]
Raw data (loadavg): 0.93 0.88 0.88 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 7391 0 0 0 11979 21 0 0 25 0 1 0 539785753 32620544 7227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7964 7227 603 41 0 7923 0
vsize: 31856
[startup+130 s]
Raw data (loadavg): 0.94 0.88 0.88 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 7530 0 0 0 12979 21 0 0 25 0 1 0 539785753 33157120 7366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8095 7366 603 41 0 8054 0
vsize: 32380
[startup+140 s]
Raw data (loadavg): 0.95 0.88 0.88 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 7667 0 0 0 13978 22 0 0 25 0 1 0 539785753 33771520 7503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8245 7503 603 41 0 8204 0
vsize: 32980
[startup+150 s]
Raw data (loadavg): 0.95 0.89 0.88 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 7779 0 0 0 14978 22 0 0 25 0 1 0 539785753 34177024 7615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8344 7615 603 41 0 8303 0
vsize: 33376
[startup+160 s]
Raw data (loadavg): 0.96 0.89 0.88 3/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 7914 0 0 0 15978 23 0 0 25 0 1 0 539785753 34750464 7750 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8484 7750 603 41 0 8443 0
vsize: 33936
[startup+170 s]
Raw data (loadavg): 0.97 0.89 0.88 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 8053 0 0 0 16978 23 0 0 25 0 1 0 539785753 35315712 7889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8622 7889 603 41 0 8581 0
vsize: 34488
[startup+180 s]
Raw data (loadavg): 0.97 0.90 0.88 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 8172 0 0 0 17978 23 0 0 25 0 1 0 539785753 35856384 8008 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8754 8008 603 41 0 8713 0
vsize: 35016
[startup+190 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 8289 0 0 0 18978 24 0 0 25 0 1 0 539785753 36274176 8125 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8856 8125 603 41 0 8815 0
vsize: 35424
[startup+200.001 s]
Raw data (loadavg): 0.98 0.90 0.89 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 8394 0 0 0 19978 24 0 0 25 0 1 0 539785753 36696064 8230 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8959 8230 603 41 0 8918 0
vsize: 35836
[startup+210.002 s]
Raw data (loadavg): 0.98 0.90 0.89 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 8498 0 0 0 20978 24 0 0 25 0 1 0 539785753 37097472 8334 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9057 8334 603 41 0 9016 0
vsize: 36228
[startup+220.002 s]
Raw data (loadavg): 0.98 0.91 0.89 3/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 8791 0 0 0 21976 25 0 0 25 0 1 0 539785753 38920192 8627 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9502 8627 603 41 0 9461 0
vsize: 38008
[startup+230.002 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 8902 0 0 0 22975 26 0 0 25 0 1 0 539785753 39329792 8738 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8738 603 41 0 9561 0
vsize: 38408
[startup+240.001 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 9000 0 0 0 23975 26 0 0 25 0 1 0 539785753 39731200 8836 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9700 8836 603 41 0 9659 0
vsize: 38800
[startup+250.002 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 9106 0 0 0 24975 27 0 0 25 0 1 0 539785753 40132608 8942 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9798 8942 603 41 0 9757 0
vsize: 39192
[startup+260.002 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 9203 0 0 0 25974 27 0 0 25 0 1 0 539785753 40529920 9039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9895 9039 603 41 0 9854 0
vsize: 39580
[startup+270.002 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 9422 0 0 0 26974 28 0 0 25 0 1 0 539785753 41570304 9258 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10149 9258 603 41 0 10108 0
vsize: 40596
[startup+280.002 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 9808 0 0 0 27972 30 0 0 25 0 1 0 539785753 43188224 9644 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10544 9644 603 41 0 10503 0
vsize: 42176
[startup+290.002 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 9899 0 0 0 28972 30 0 0 25 0 1 0 539785753 43450368 9735 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10608 9735 603 41 0 10567 0
vsize: 42432
[startup+300.002 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 9991 0 0 0 29972 30 0 0 25 0 1 0 539785753 43855872 9827 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10707 9827 603 41 0 10666 0
vsize: 42828
[startup+310.002 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 10093 0 0 0 30972 30 0 0 25 0 1 0 539785753 44277760 9929 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10810 9929 603 41 0 10769 0
vsize: 43240
[startup+320.002 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 10455 0 0 0 31971 31 0 0 25 0 1 0 539785753 45793280 10291 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11180 10291 603 41 0 11139 0
vsize: 44720
[startup+330.002 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 10554 0 0 0 32971 31 0 0 25 0 1 0 539785753 46194688 10390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11278 10390 603 41 0 11237 0
vsize: 45112
[startup+340.002 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 10666 0 0 0 33971 32 0 0 25 0 1 0 539785753 46620672 10502 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11382 10502 603 41 0 11341 0
vsize: 45528
[startup+350.002 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 10799 0 0 0 34971 32 0 0 25 0 1 0 539785753 47157248 10635 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11513 10635 603 41 0 11472 0
vsize: 46052
[startup+360.002 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 10905 0 0 0 35971 33 0 0 25 0 1 0 539785753 47693824 10741 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11644 10741 603 41 0 11603 0
vsize: 46576
[startup+370.001 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 11037 0 0 0 36970 33 0 0 25 0 1 0 539785753 48275456 10873 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11786 10873 603 41 0 11745 0
vsize: 47144
[startup+380.001 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 11123 0 0 0 37971 33 0 0 25 0 1 0 539785753 48549888 10959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11853 10959 603 41 0 11812 0
vsize: 47412
[startup+390.001 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 11258 0 0 0 38970 34 0 0 25 0 1 0 539785753 49131520 11094 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11995 11094 603 41 0 11954 0
vsize: 47980
[startup+400.001 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 11658 0 0 0 39969 35 0 0 25 0 1 0 539785753 50827264 11494 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12409 11494 603 41 0 12368 0
vsize: 49636
[startup+410.001 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 11732 0 0 0 40969 35 0 0 25 0 1 0 539785753 51093504 11568 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12474 11568 603 41 0 12433 0
vsize: 49896
[startup+420.001 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 11803 0 0 0 41969 35 0 0 25 0 1 0 539785753 51363840 11639 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12540 11639 603 41 0 12499 0
vsize: 50160
[startup+430 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 11870 0 0 0 42968 35 0 0 25 0 1 0 539785753 51625984 11706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12604 11706 603 41 0 12563 0
vsize: 50416
[startup+440 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 11953 0 0 0 43968 36 0 0 25 0 1 0 539785753 51957760 11789 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12685 11789 603 41 0 12644 0
vsize: 50740
[startup+450.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12019 0 0 0 44968 36 0 0 25 0 1 0 539785753 52232192 11855 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12752 11855 603 41 0 12711 0
vsize: 51008
[startup+460.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12086 0 0 0 45968 37 0 0 25 0 1 0 539785753 52502528 11922 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12818 11922 603 41 0 12777 0
vsize: 51272
[startup+470.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12149 0 0 0 46968 37 0 0 25 0 1 0 539785753 52768768 11985 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12883 11985 603 41 0 12842 0
vsize: 51532
[startup+480.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12216 0 0 0 47968 37 0 0 25 0 1 0 539785753 53035008 12052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12948 12052 603 41 0 12907 0
vsize: 51792
[startup+490 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12283 0 0 0 48967 37 0 0 25 0 1 0 539785753 53301248 12119 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13013 12119 603 41 0 12972 0
vsize: 52052
[startup+500.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12346 0 0 0 49968 38 0 0 25 0 1 0 539785753 53571584 12182 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13079 12182 603 41 0 13038 0
vsize: 52316
[startup+510.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12412 0 0 0 50968 38 0 0 25 0 1 0 539785753 53862400 12248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13150 12248 603 41 0 13109 0
vsize: 52600
[startup+520.106 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12471 0 0 0 51978 38 0 0 25 0 1 0 539785753 53993472 12307 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13182 12307 603 41 0 13141 0
vsize: 52728
[startup+530.107 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12531 0 0 0 52978 38 0 0 25 0 1 0 539785753 54312960 12367 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13260 12367 603 41 0 13219 0
vsize: 53040
[startup+540.107 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12593 0 0 0 53978 38 0 0 25 0 1 0 539785753 54583296 12429 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13326 12429 603 41 0 13285 0
vsize: 53304
[startup+550.107 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12657 0 0 0 54978 39 0 0 25 0 1 0 539785753 54956032 12493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13417 12493 603 41 0 13376 0
vsize: 53668
[startup+560.107 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12719 0 0 0 55978 39 0 0 25 0 1 0 539785753 55091200 12555 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13450 12555 603 41 0 13409 0
vsize: 53800
[startup+570.107 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12779 0 0 0 56978 39 0 0 25 0 1 0 539785753 55357440 12615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13515 12615 603 41 0 13474 0
vsize: 54060
[startup+580.108 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12852 0 0 0 57978 39 0 0 25 0 1 0 539785753 55627776 12688 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13581 12688 603 41 0 13540 0
vsize: 54324
[startup+590.109 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12919 0 0 0 58978 40 0 0 25 0 1 0 539785753 55914496 12755 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13651 12755 603 41 0 13610 0
vsize: 54604
[startup+600.109 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 12979 0 0 0 59978 40 0 0 25 0 1 0 539785753 56180736 12815 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13716 12815 603 41 0 13675 0
vsize: 54864
[startup+610.108 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13045 0 0 0 60978 40 0 0 25 0 1 0 539785753 56446976 12881 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13781 12881 603 41 0 13740 0
vsize: 55124
[startup+620.108 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13109 0 0 0 61978 40 0 0 25 0 1 0 539785753 56713216 12945 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13846 12945 603 41 0 13805 0
vsize: 55384
[startup+630.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13172 0 0 0 62978 40 0 0 25 0 1 0 539785753 56979456 13008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13911 13008 603 41 0 13870 0
vsize: 55644
[startup+640.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13239 0 0 0 63978 40 0 0 25 0 1 0 539785753 57249792 13075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13977 13075 603 41 0 13936 0
vsize: 55908
[startup+650.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13301 0 0 0 64978 40 0 0 25 0 1 0 539785753 57384960 13137 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14010 13137 603 41 0 13969 0
vsize: 56040
[startup+660.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13365 0 0 0 65978 40 0 0 25 0 1 0 539785753 57655296 13201 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14076 13201 603 41 0 14035 0
vsize: 56304
[startup+670.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13431 0 0 0 66978 41 0 0 25 0 1 0 539785753 57921536 13267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14141 13267 603 41 0 14100 0
vsize: 56564
[startup+680.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13488 0 0 0 67978 41 0 0 25 0 1 0 539785753 58187776 13324 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14206 13324 603 41 0 14165 0
vsize: 56824
[startup+690.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13553 0 0 0 68978 41 0 0 25 0 1 0 539785753 58462208 13389 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14273 13389 603 41 0 14232 0
vsize: 57092
[startup+700.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13646 0 0 0 69978 42 0 0 25 0 1 0 539785753 58736640 13482 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14340 13482 603 41 0 14299 0
vsize: 57360
[startup+710.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13704 0 0 0 70978 42 0 0 25 0 1 0 539785753 59006976 13540 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13540 603 41 0 14365 0
vsize: 57624
[startup+720.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 71978 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134561533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+730.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 72979 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+740.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 73980 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+750.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 74980 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+760.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 75980 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+770.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 76980 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+780.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 77981 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+790.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 78981 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+800.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 79980 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+810.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 80979 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+820.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 81980 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+830.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 82980 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+840.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 83980 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+850.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 84981 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+860.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13711 0 0 0 85981 42 0 0 25 0 1 0 539785753 59006976 13547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14406 13547 603 41 0 14365 0
vsize: 57624
[startup+870.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13730 0 0 0 86981 42 0 0 25 0 1 0 539785753 59150336 13566 4294967295 134512640 134672761 3221224544 3221223680 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14441 13566 603 41 0 14400 0
vsize: 57764
[startup+880.132 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13746 0 0 0 87981 42 0 0 25 0 1 0 539785753 59314176 13582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14481 13582 603 41 0 14440 0
vsize: 57924
[startup+890.299 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9286
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13756 0 0 0 88998 42 0 0 25 0 1 0 539785753 59314176 13592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14481 13592 603 41 0 14440 0
vsize: 57924
[startup+900.3 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 9327
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13757 0 0 0 89998 43 0 0 25 0 1 0 539785753 59314176 13593 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14481 13593 603 41 0 14440 0
vsize: 57924
[startup+910.3 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13770 0 0 0 90997 43 0 0 25 0 1 0 539785753 59314176 13606 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14481 13606 603 41 0 14440 0
vsize: 57924
[startup+920.299 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13786 0 0 0 91997 44 0 0 25 0 1 0 539785753 59478016 13622 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14521 13622 603 41 0 14480 0
vsize: 58084
[startup+930.299 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13793 0 0 0 92997 44 0 0 25 0 1 0 539785753 59478016 13629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14521 13629 603 41 0 14480 0
vsize: 58084
[startup+940.299 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13804 0 0 0 93997 45 0 0 25 0 1 0 539785753 59625472 13640 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14557 13640 603 41 0 14516 0
vsize: 58228
[startup+950.307 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13805 0 0 0 94997 45 0 0 25 0 1 0 539785753 59625472 13641 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14557 13641 603 41 0 14516 0
vsize: 58228
[startup+960.307 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 9339
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13814 0 0 0 95997 45 0 0 25 0 1 0 539785753 59625472 13650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14557 13650 603 41 0 14516 0
vsize: 58228
[startup+970.307 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13815 0 0 0 96996 46 0 0 25 0 1 0 539785753 59625472 13651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14557 13651 603 41 0 14516 0
vsize: 58228
[startup+980.307 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13815 0 0 0 97996 46 0 0 25 0 1 0 539785753 59625472 13651 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14557 13651 603 41 0 14516 0
vsize: 58228
[startup+990.307 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13815 0 0 0 98997 46 0 0 25 0 1 0 539785753 59625472 13651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14557 13651 603 41 0 14516 0
vsize: 58228
[startup+1000.31 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13819 0 0 0 99997 46 0 0 25 0 1 0 539785753 59625472 13655 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14557 13655 603 41 0 14516 0
vsize: 58228
[startup+1010.31 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13827 0 0 0 100997 46 0 0 25 0 1 0 539785753 59625472 13663 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14557 13663 603 41 0 14516 0
vsize: 58228
[startup+1020.31 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13830 0 0 0 101997 46 0 0 25 0 1 0 539785753 59625472 13666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14557 13666 603 41 0 14516 0
vsize: 58228
[startup+1030.31 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13839 0 0 0 102997 46 0 0 25 0 1 0 539785753 59789312 13675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14597 13675 603 41 0 14556 0
vsize: 58388
[startup+1040.31 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13846 0 0 0 103997 46 0 0 25 0 1 0 539785753 59789312 13682 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14597 13682 603 41 0 14556 0
vsize: 58388
[startup+1050.31 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13851 0 0 0 104998 46 0 0 25 0 1 0 539785753 59789312 13687 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14597 13687 603 41 0 14556 0
vsize: 58388
[startup+1060.31 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13860 0 0 0 105998 46 0 0 25 0 1 0 539785753 59789312 13696 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14597 13696 603 41 0 14556 0
vsize: 58388
[startup+1070.31 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13866 0 0 0 106998 46 0 0 25 0 1 0 539785753 59789312 13702 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14597 13702 603 41 0 14556 0
vsize: 58388
[startup+1080.31 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13886 0 0 0 107998 47 0 0 25 0 1 0 539785753 59953152 13722 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14637 13722 603 41 0 14596 0
vsize: 58548
[startup+1090.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13976 0 0 0 108998 47 0 0 25 0 1 0 539785753 60444672 13812 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14757 13812 603 41 0 14716 0
vsize: 59028
[startup+1100.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13989 0 0 0 109998 47 0 0 25 0 1 0 539785753 60444672 13825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14757 13825 603 41 0 14716 0
vsize: 59028
[startup+1110.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 13990 0 0 0 110998 47 0 0 25 0 1 0 539785753 60444672 13826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14757 13826 603 41 0 14716 0
vsize: 59028
[startup+1120.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 14019 0 0 0 111998 47 0 0 25 0 1 0 539785753 60641280 13855 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14805 13855 603 41 0 14764 0
vsize: 59220
[startup+1130.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 14397 0 0 0 112997 48 0 0 25 0 1 0 539785753 62115840 14233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15165 14233 603 41 0 15124 0
vsize: 60660
[startup+1140.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 15177 0 0 0 113995 51 0 0 25 0 1 0 539785753 65347584 15013 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15954 15013 603 41 0 15913 0
vsize: 63816
[startup+1150.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 15646 0 0 0 114994 52 0 0 25 0 1 0 539785753 68333568 15482 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16683 15482 603 41 0 16642 0
vsize: 66732
[startup+1160.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 16143 0 0 0 115992 54 0 0 25 0 1 0 539785753 70352896 15979 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17176 15979 603 41 0 17135 0
vsize: 68704
[startup+1170.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 16561 0 0 0 116992 55 0 0 25 0 1 0 539785753 71966720 16397 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17570 16397 603 41 0 17529 0
vsize: 70280
[startup+1180.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 16879 0 0 0 117991 56 0 0 25 0 1 0 539785753 73310208 16715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17898 16715 603 41 0 17857 0
vsize: 71592
[startup+1190.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 17255 0 0 0 118990 57 0 0 25 0 1 0 539785753 74780672 17091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18257 17091 603 41 0 18216 0
vsize: 73028
[startup+1200.31 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9341
Raw data (stat): 9286 (minisat+) R 9285 10614 10613 0 -1 0 17416 0 0 0 119990 57 0 0 25 0 1 0 539785753 75452416 17252 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18421 17252 603 41 0 18380 0
vsize: 73684
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.35 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 9341
Raw data (stat): 9286 (minisat+) Z 9285 10614 10613 0 -1 12 17418 0 0 0 119990 60 0 0 25 0 1 0 539785753 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.35
CPU time (s): 1200.51
CPU user time (s): 1199.9
CPU system time (s): 0.608907
CPU usage (%): 100.014
Max. virtual memory (Kb): 73684
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####