PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-dcmulti.opb
MD5SUM	28123830d5f7e3646d18978bb347487c
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	9505
Biggest coefficient in the objective function	697303040
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	66656504525
Number of bits of the sum of numbers in the objective function	36
Biggest number in a constraint	697303040
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	66656504525
Number of bits of the biggest sum of numbers	36
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.085986
Number of variables	9535
Total number of constraints	365
Number of constraints which are clauses	27
Number of constraints which are cardinality constraints (but not clauses)	80
Number of constraints which are nor clauses,nor cardinality constraints	258
Minimum length of a constraint	1
Maximum length of a constraint	280
Trace number 18297

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        738876 kB
Buffers:         23844 kB
Cached:         249380 kB
SwapCached:          0 kB
Active:          26364 kB
Inactive:       249620 kB
HighTotal:      131008 kB
HighFree:        86912 kB
LowTotal:       903652 kB
LowFree:        651964 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            14140 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:34:41 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 18288 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 368 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): s....s.....sssssssssssssssssss....s.....ssssssssssssssssss....s.....sssssssssssssssssss
c ---[ 427]---> Adder-cost: 43   maxlim: 6270   bits: 14/13
c ---[ 426]---> Adder-cost: 140   maxlim: 81914   bits: 17/17
c ---[ 425]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 424]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 422]---> Adder-cost: 30   maxlim: 31614   bits: 16/15
c ---[ 421]---> Adder-cost: 43   maxlim: 6270   bits: 14/13
c ---[ 420]---> Adder-cost: 28   maxlim: 14846   bits: 15/14
c ---[ 419]---> Adder-cost: 41   maxlim: 2302   bits: 13/12
c ---[ 418]---> Adder-cost: 28   maxlim: 15486   bits: 15/14
c ---[ 416]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 415]---> Adder-cost: 28   maxlim: 14846   bits: 15/14
c ---[ 413]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 411]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 409]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 407]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 405]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 403]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 401]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 399]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 397]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 395]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 394]---> Adder-cost: 41   maxlim: 2302   bits: 13/12
c ---[ 392]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 391]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 390]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 389]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 388]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 386]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 385]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 384]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 381]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 380]---> Adder-cost: 28   maxlim: 15486   bits: 15/14
c ---[ 378]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 377]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 376]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 375]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 374]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 372]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 371]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 370]---> Adder-cost: 16   maxlim: 44799   bits: 17/16
c ---[ 367]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 365]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 363]---> Adder-cost: 114   maxlim: 32766   bits: 16/15
c ---[ 362]---> Adder-cost: 11   maxlim: 32766   bits: 16/15
c ---[ 361]---> Adder-cost: 12   maxlim: 23039   bits: 16/15
c ---[ 360]---> Adder-cost: 11   maxlim: 16382   bits: 15/14
c ---[ 359]---> Adder-cost: 6   maxlim: 10239   bits: 15/14
c ---[ 357]---> Adder-cost: 115   maxlim: 32767   bits: 16/15
c ---[ 356]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 355]---> Adder-cost: 15   maxlim: 12799   bits: 15/14
c ---[ 352]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 350]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 348]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 347]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 346]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 345]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 344]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 342]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 341]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 340]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 337]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 335]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 333]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 332]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 331]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 330]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 329]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 327]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 326]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 322]---> Adder-cost: 16   maxlim: 5   bits: 4/3
c ---[ 320]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 308]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 296]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 293]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 292]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 291]---> Adder-cost: 160   maxlim: 327674   bits: 19/19
c ---[ 290]---> Adder-cost: 140   maxlim: 81914   bits: 17/17
c ---[ 289]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 288]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 286]---> Adder-cost: 30   maxlim: 31614   bits: 16/15
c ---[ 285]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 283]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 282]---> Adder-cost: 43   maxlim: 6270   bits: 14/13
c ---[ 281]---> Adder-cost: 28   maxlim: 14846   bits: 15/14
c ---[ 280]---> Adder-cost: 41   maxlim: 2302   bits: 13/12
c ---[ 279]---> Adder-cost: 28   maxlim: 15486   bits: 15/14
c ---[ 277]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 275]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 273]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 271]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 269]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 267]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 265]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 263]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 261]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 259]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 257]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 255]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 253]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 252]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 251]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 250]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 249]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 247]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 245]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 244]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 243]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 240]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 238]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 237]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 236]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 235]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 234]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 232]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 230]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 229]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 228]---> Adder-cost: 16   maxlim: 44799   bits: 17/16
c ---[ 225]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 223]---> Adder-cost: 114   maxlim: 32766   bits: 16/15
c ---[ 222]---> Adder-cost: 11   maxlim: 32766   bits: 16/15
c ---[ 221]---> Adder-cost: 12   maxlim: 23039   bits: 16/15
c ---[ 220]---> Adder-cost: 11   maxlim: 16382   bits: 15/14
c ---[ 219]---> Adder-cost: 6   maxlim: 10239   bits: 15/14
c ---[ 217]---> Adder-cost: 92   maxlim: 131070   bits: 18/17
c ---[ 215]---> Adder-cost: 115   maxlim: 32767   bits: 16/15
c ---[ 214]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 213]---> Adder-cost: 15   maxlim: 12799   bits: 15/14
c ---[ 210]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 208]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 207]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 206]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 205]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 204]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 202]---> Adder-cost: 91   maxlim: 65534   bits: 17/16
c ---[ 200]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 199]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 198]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 195]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 193]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 192]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 191]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 190]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 189]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 188]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 186]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 185]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 181]---> Adder-cost: 16   maxlim: 5   bits: 4/3
c ---[ 175]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 164]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 156]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 155]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 154]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 153]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 152]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 151]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 150]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 148]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 147]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 146]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 143]---> Adder-cost: 92   maxlim: 131070   bits: 18/17
c ---[ 141]---> Adder-cost: 91   maxlim: 65534   bits: 17/16
c ---[ 140]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 139]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 138]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 137]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 136]---> Adder-cost: 160   maxlim: 327674   bits: 19/19
c ---[ 134]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 133]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 132]---> Adder-cost: 16   maxlim: 44799   bits: 17/16
c ---[ 129]---> Adder-cost: 89   maxlim: 65534   bits: 17/16
c ---[ 127]---> Adder-cost: 86   maxlim: 32766   bits: 16/15
c ---[ 126]---> Adder-cost: 11   maxlim: 32766   bits: 16/15
c ---[ 125]---> Adder-cost: 12   maxlim: 23039   bits: 16/15
c ---[ 124]---> Adder-cost: 11   maxlim: 16382   bits: 15/14
c ---[ 123]---> Adder-cost: 6   maxlim: 10239   bits: 15/14
c ---[ 122]---> Adder-cost: 140   maxlim: 81914   bits: 17/17
c ---[ 120]---> Adder-cost: 115   maxlim: 32767   bits: 16/15
c ---[ 119]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 118]---> Adder-cost: 15   maxlim: 12799   bits: 15/14
c ---[ 115]---> Adder-cost: 92   maxlim: 131070   bits: 18/17
c ---[ 113]---> Adder-cost: 91   maxlim: 65534   bits: 17/16
c ---[ 112]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 111]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 110]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 109]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 108]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 106]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 105]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 104]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 101]---> Adder-cost: 92   maxlim: 131070   bits: 18/17
c ---[  99]---> Adder-cost: 91   maxlim: 65534   bits: 17/16
c ---[  98]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[  97]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[  96]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[  95]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[  94]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[  92]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[  91]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[  87]---> Adder-cost: 16   maxlim: 5   bits: 4/3
c ---[  70]---> Adder-cost: 30   maxlim: 31614   bits: 16/15
c ---[  62]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[  61]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[  60]---> Adder-cost: 160   maxlim: 327674   bits: 19/19
c ---[  59]---> Adder-cost: 24   maxlim: 3326   bits: 13/12
c ---[  58]---> Adder-cost: 10   maxlim: 12799   bits: 15/14
c ---[  57]---> Adder-cost: 114   maxlim: 4223   bits: 14/13
c ---[  56]---> Adder-cost: 104   maxlim: 2687   bits: 13/12
c ---[  55]---> Adder-cost: 114   maxlim: 6015   bits: 14/13
c ---[  54]---> Adder-cost: 102   maxlim: 3839   bits: 13/12
c ---[  53]---> Adder-cost: 120   maxlim: 8703   bits: 15/14
c ---[  52]---> Adder-cost: 114   maxlim: 5247   bits: 14/13
c ---[  51]---> Adder-cost: 104   maxlim: 3711   bits: 13/12
c ---[  50]---> Adder-cost: 100   maxlim: 2559   bits: 13/12
c ---[  49]---> Adder-cost: 104   maxlim: 3967   bits: 13/12
c ---[  48]---> Adder-cost: 94   maxlim: 1919   bits: 12/11
c ---[  47]---> Adder-cost: 120   maxlim: 9727   bits: 15/14
c ---[  46]---> Adder-cost: 104   maxlim: 3967   bits: 13/12
c ---[  45]---> Adder-cost: 114   maxlim: 4991   bits: 14/13
c ---[  44]---> Adder-cost: 104   maxlim: 2687   bits: 13/12
c ---[  43]---> Adder-cost: 94   maxlim: 4095   bits: 13/12
c ---[  42]---> Adder-cost: 92   maxlim: 1791   bits: 12/11
c ---[  41]---> Adder-cost: 124   maxlim: 9087   bits: 15/14
c ---[  40]---> Adder-cost: 114   maxlim: 4223   bits: 14/13
c ---[  39]---> Adder-cost: 24   maxlim: 3326   bits: 13/12
c ---[  38]---> Adder-cost: 10   maxlim: 12799   bits: 15/14
c ---[  37]---> Adder-cost: 112   maxlim: 4863   bits: 14/13
c ---[  36]---> Adder-cost: 102   maxlim: 3327   bits: 13/12
c ---[  35]---> Adder-cost: 110   maxlim: 6655   bits: 14/13
c ---[  34]---> Adder-cost: 114   maxlim: 4479   bits: 14/13
c ---[  33]---> Adder-cost: 124   maxlim: 9343   bits: 15/14
c ---[  32]---> Adder-cost: 112   maxlim: 5887   bits: 14/13
c ---[  31]---> Adder-cost: 112   maxlim: 4351   bits: 14/13
c ---[  30]---> Adder-cost: 104   maxlim: 3199   bits: 13/12
c ---[  29]---> Adder-cost: 110   maxlim: 4607   bits: 14/13
c ---[  28]---> Adder-cost: 100   maxlim: 2559   bits: 13/12
c ---[  27]---> Adder-cost: 124   maxlim: 10367   bits: 15/14
c ---[  26]---> Adder-cost: 110   maxlim: 4607   bits: 14/13
c ---[  25]---> Adder-cost: 110   maxlim: 5631   bits: 14/13
c ---[  24]---> Adder-cost: 102   maxlim: 3327   bits: 13/12
c ---[  23]---> Adder-cost: 114   maxlim: 4735   bits: 14/13
c ---[  22]---> Adder-cost: 104   maxlim: 2431   bits: 13/12
c ---[  21]---> Adder-cost: 120   maxlim: 9727   bits: 15/14
c ---[  20]---> Adder-cost: 112   maxlim: 4863   bits: 14/13
c ---[  19]---> Adder-cost: 10   maxlim: 12799   bits: 15/14
c ---[  18]---> Adder-cost: 100   maxlim: 3583   bits: 13/12
c ---[  17]---> Adder-cost: 24   maxlim: 3326   bits: 13/12
c ---[  16]---> Adder-cost: 86   maxlim: 2047   bits: 12/11
c ---[  15]---> Adder-cost: 112   maxlim: 5375   bits: 14/13
c ---[  14]---> Adder-cost: 104   maxlim: 3199   bits: 13/12
c ---[  13]---> Adder-cost: 114   maxlim: 8063   bits: 14/13
c ---[  12]---> Adder-cost: 110   maxlim: 4607   bits: 14/13
c ---[  11]---> Adder-cost: 98   maxlim: 3071   bits: 13/12
c ---[  10]---> Adder-cost: 94   maxlim: 1919   bits: 12/11
c ---[   9]---> Adder-cost: 110   maxlim: 4607   bits: 14/13
c ---[   8]---> Adder-cost: 92   maxlim: 1279   bits: 12/11
c ---[   7]---> Adder-cost: 124   maxlim: 9087   bits: 15/14
c ---[   6]---> Adder-cost: 102   maxlim: 3327   bits: 13/12
c ---[   5]---> Adder-cost: 112   maxlim: 4351   bits: 14/13
c ---[   4]---> Adder-cost: 86   maxlim: 2047   bits: 12/11
c ---[   3]---> Adder-cost: 104   maxlim: 3455   bits: 13/12
c ---[   2]---> Adder-cost: 94   maxlim: 1151   bits: 12/11
c ---[   1]---> Adder-cost: 122   maxlim: 8447   bits: 15/14
c ---[   0]---> Adder-cost: 100   maxlim: 3583   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  176871   635589 |   58957       0        0     nan |  0.000 % |
c |       100 |  176871   635589 |   64852     100      465     4.7 | 15.209 % |
c |       250 |  176871   635589 |   71337     250     1029     4.1 | 15.209 % |
c |       476 |  176863   635563 |   78471     475     1978     4.2 | 15.211 % |
c |       814 |  176846   635508 |   86318     811     3923     4.8 | 15.219 % |
c |      1320 |  176803   635369 |   94950    1312     6339     4.8 | 15.239 % |
c |      2080 |  176762   635236 |  104445    2067    10315     5.0 | 15.254 % |
c |      3219 |  176713   635077 |  114890    3200    16410     5.1 | 15.272 % |
c |      4930 |  176649   634869 |  126379    4903    38319     7.8 | 15.292 % |
c |      7492 |  176585   634658 |  139017    7457    54892     7.4 | 15.312 % |
c |     11336 |  176497   634367 |  152919   11285    82187     7.3 | 15.338 % |
c |     17102 |  176391   634019 |  168211   17017   123051     7.2 | 15.371 % |
c |     25751 |  176297   633713 |  185032   25647   350043    13.6 | 15.401 % |
c |     38726 |  176281   633661 |  203535   38620   962057    24.9 | 15.406 % |
c |     58191 |  176195   633383 |  223889   58066  1412628    24.3 | 15.436 % |
c |     87383 |  175993   632702 |  246278   87226  2010274    23.0 | 15.492 % |
c |    131172 |  175888   632337 |  270905  130906  5212455    39.8 | 15.522 % |
c |    196856 |  175842   632187 |  297996  196572  8844740    45.0 | 15.538 % |
c |    295383 |  175674   631622 |  327796  295051 13097987    44.4 | 15.591 % |
c |    443172 |  175621   631443 |  360575  130471  6023894    46.2 | 15.606 % |
#### 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.79 0.95 0.91 2/54 13277
Raw data (stat): 13277 (runsolver) R 13276 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487492580 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.0004 s]
Raw data (loadavg): 0.82 0.95 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 4678 0 0 0 987 11 0 0 25 0 1 0 487492580 21725184 4442 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5304 4442 603 41 0 5263 0
vsize: 21216
[startup+20.0013 s]
Raw data (loadavg): 0.85 0.95 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 4844 0 0 0 1986 12 0 0 25 0 1 0 487492580 22503424 4608 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5494 4608 603 41 0 5453 0
vsize: 21976
[startup+30.0017 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 5188 0 0 0 2985 13 0 0 25 0 1 0 487492580 23838720 4952 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5820 4952 603 41 0 5779 0
vsize: 23280
[startup+40.002 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 5942 0 0 0 3982 15 0 0 25 0 1 0 487492580 27058176 5706 4294967295 134512640 134672761 3221224544 3221223808 134562276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6606 5706 603 41 0 6565 0
vsize: 26424
[startup+50.0027 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 6213 0 0 0 4981 16 0 0 25 0 1 0 487492580 28135424 5977 4294967295 134512640 134672761 3221224544 3221223712 134564493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6869 5977 603 41 0 6828 0
vsize: 27476
[startup+60.0029 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 6585 0 0 0 5981 17 0 0 25 0 1 0 487492580 29614080 6349 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7230 6349 603 41 0 7189 0
vsize: 28920
[startup+70.0034 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 6704 0 0 0 6981 17 0 0 25 0 1 0 487492580 30015488 6468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7328 6468 603 41 0 7287 0
vsize: 29312
[startup+80.0032 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 6915 0 0 0 7980 18 0 0 25 0 1 0 487492580 31223808 6679 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7623 6679 603 41 0 7582 0
vsize: 30492
[startup+90.0044 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 7186 0 0 0 8979 18 0 0 25 0 1 0 487492580 32296960 6950 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7885 6950 603 41 0 7844 0
vsize: 31540
[startup+100.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 8041 0 0 0 9977 21 0 0 25 0 1 0 487492580 35651584 7805 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8704 7805 603 41 0 8663 0
vsize: 34816
[startup+110.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 8937 0 0 0 10974 23 0 0 25 0 1 0 487492580 39305216 8701 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9596 8701 603 41 0 9555 0
vsize: 38384
[startup+120.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 9671 0 0 0 11972 26 0 0 25 0 1 0 487492580 42287104 9435 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10324 9435 603 41 0 10283 0
vsize: 41296
[startup+130.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 10208 0 0 0 12971 27 0 0 25 0 1 0 487492580 44601344 9972 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10889 9972 603 41 0 10848 0
vsize: 43556
[startup+140.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 10710 0 0 0 13970 29 0 0 25 0 1 0 487492580 46637056 10474 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11386 10474 603 41 0 11345 0
vsize: 45544
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 11028 0 0 0 14970 29 0 0 25 0 1 0 487492580 47837184 10792 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11679 10792 603 41 0 11638 0
vsize: 46716
[startup+160.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 11537 0 0 0 15968 31 0 0 25 0 1 0 487492580 50503680 11301 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12330 11301 603 41 0 12289 0
vsize: 49320
[startup+170.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 12069 0 0 0 16967 32 0 0 25 0 1 0 487492580 52666368 11833 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12858 11833 603 41 0 12817 0
vsize: 51432
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 12557 0 0 0 17966 33 0 0 25 0 1 0 487492580 54534144 12321 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13314 12321 603 41 0 13273 0
vsize: 53256
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 12969 0 0 0 18965 34 0 0 25 0 1 0 487492580 56274944 12733 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13739 12733 603 41 0 13698 0
vsize: 54956
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 13319 0 0 0 19964 36 0 0 25 0 1 0 487492580 57761792 13083 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14102 13083 603 41 0 14061 0
vsize: 56408
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 13662 0 0 0 20963 37 0 0 25 0 1 0 487492580 59084800 13426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14425 13426 603 41 0 14384 0
vsize: 57700
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 14081 0 0 0 21962 38 0 0 25 0 1 0 487492580 60727296 13845 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14826 13845 603 41 0 14785 0
vsize: 59304
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 14372 0 0 0 22961 39 0 0 25 0 1 0 487492580 61952000 14136 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15125 14136 603 41 0 15084 0
vsize: 60500
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 14708 0 0 0 23961 40 0 0 25 0 1 0 487492580 63291392 14472 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15452 14472 603 41 0 15411 0
vsize: 61808
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 15004 0 0 0 24960 41 0 0 25 0 1 0 487492580 64503808 14768 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15748 14768 603 41 0 15707 0
vsize: 62992
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 15267 0 0 0 25959 42 0 0 25 0 1 0 487492580 65581056 15031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16011 15031 603 41 0 15970 0
vsize: 64044
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 15518 0 0 0 26958 43 0 0 25 0 1 0 487492580 66662400 15282 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16275 15282 603 41 0 16234 0
vsize: 65100
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 15670 0 0 0 27956 44 0 0 25 0 1 0 487492580 67203072 15434 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16407 15434 603 41 0 16366 0
vsize: 65628
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 15904 0 0 0 28956 45 0 0 25 0 1 0 487492580 68141056 15668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16636 15668 603 41 0 16595 0
vsize: 66544
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 16120 0 0 0 29955 46 0 0 25 0 1 0 487492580 69099520 15884 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16870 15884 603 41 0 16829 0
vsize: 67480
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 16233 0 0 0 30955 46 0 0 25 0 1 0 487492580 69505024 15997 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16969 15997 603 41 0 16928 0
vsize: 67876
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 16404 0 0 0 31955 47 0 0 25 0 1 0 487492580 70307840 16168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17165 16168 603 41 0 17124 0
vsize: 68660
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 16590 0 0 0 32954 47 0 0 25 0 1 0 487492580 70975488 16354 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17328 16354 603 41 0 17287 0
vsize: 69312
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 16819 0 0 0 33953 48 0 0 25 0 1 0 487492580 71917568 16583 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17558 16583 603 41 0 17517 0
vsize: 70232
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 16999 0 0 0 34953 49 0 0 25 0 1 0 487492580 72593408 16763 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17723 16763 603 41 0 17682 0
vsize: 70892
[startup+360.017 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 17111 0 0 0 35953 49 0 0 25 0 1 0 487492580 73134080 16875 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17855 16875 603 41 0 17814 0
vsize: 71420
[startup+370.017 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 17490 0 0 0 36952 50 0 0 25 0 1 0 487492580 74596352 17254 4294967295 134512640 134672761 3221224544 3221223808 134562590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18212 17254 603 41 0 18171 0
vsize: 72848
[startup+380.017 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 18364 0 0 0 37950 53 0 0 25 0 1 0 487492580 78233600 18128 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19100 18128 603 41 0 19059 0
vsize: 76400
[startup+390.017 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 18866 0 0 0 38949 54 0 0 25 0 1 0 487492580 81297408 18630 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19848 18630 603 41 0 19807 0
vsize: 79392
[startup+400.018 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 19117 0 0 0 39948 55 0 0 25 0 1 0 487492580 82280448 18881 4294967295 134512640 134672761 3221224544 3221223760 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20088 18881 603 41 0 20047 0
vsize: 80352
[startup+410.018 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 19294 0 0 0 40948 56 0 0 25 0 1 0 487492580 83091456 19058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20286 19058 603 41 0 20245 0
vsize: 81144
[startup+420.018 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 19533 0 0 0 41947 57 0 0 25 0 1 0 487492580 84025344 19297 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20514 19297 603 41 0 20473 0
vsize: 82056
[startup+430.019 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 19880 0 0 0 42946 58 0 0 25 0 1 0 487492580 85372928 19644 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20843 19644 603 41 0 20802 0
vsize: 83372
[startup+440.019 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 20363 0 0 0 43945 60 0 0 25 0 1 0 487492580 87392256 20127 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21336 20127 603 41 0 21295 0
vsize: 85344
[startup+450.02 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 20519 0 0 0 44944 60 0 0 25 0 1 0 487492580 87932928 20283 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20283 603 41 0 21427 0
vsize: 85872
[startup+460.019 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 20844 0 0 0 45943 62 0 0 25 0 1 0 487492580 89272320 20608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21795 20608 603 41 0 21754 0
vsize: 87180
[startup+470.02 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 21023 0 0 0 46942 62 0 0 25 0 1 0 487492580 89944064 20787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21959 20787 603 41 0 21918 0
vsize: 87836
[startup+480.021 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 21314 0 0 0 47941 63 0 0 25 0 1 0 487492580 91148288 21078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22253 21078 603 41 0 22212 0
vsize: 89012
[startup+490.022 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 21574 0 0 0 48941 64 0 0 25 0 1 0 487492580 92217344 21338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22514 21338 603 41 0 22473 0
vsize: 90056
[startup+500.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 21861 0 0 0 49940 64 0 0 25 0 1 0 487492580 93433856 21625 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22811 21625 603 41 0 22770 0
vsize: 91244
[startup+510.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 22150 0 0 0 50939 65 0 0 25 0 1 0 487492580 94519296 21914 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23076 21914 603 41 0 23035 0
vsize: 92304
[startup+520.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 22281 0 0 0 51940 66 0 0 25 0 1 0 487492580 95059968 22045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23208 22045 603 41 0 23167 0
vsize: 92832
[startup+530.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 22408 0 0 0 52940 66 0 0 25 0 1 0 487492580 95596544 22172 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23339 22172 603 41 0 23298 0
vsize: 93356
[startup+540.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 22694 0 0 0 53939 66 0 0 25 0 1 0 487492580 96813056 22458 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23636 22458 603 41 0 23595 0
vsize: 94544
[startup+550.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 22984 0 0 0 54939 67 0 0 25 0 1 0 487492580 97886208 22748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23898 22748 603 41 0 23857 0
vsize: 95592
[startup+560.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23229 0 0 0 55938 68 0 0 25 0 1 0 487492580 98951168 22993 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24158 22993 603 41 0 24117 0
vsize: 96632
[startup+570.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23322 0 0 0 56938 68 0 0 25 0 1 0 487492580 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+580.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23322 0 0 0 57938 68 0 0 25 0 1 0 487492580 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+590.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23322 0 0 0 58938 68 0 0 25 0 1 0 487492580 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+600.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23322 0 0 0 59939 68 0 0 25 0 1 0 487492580 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+610.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23322 0 0 0 60939 68 0 0 25 0 1 0 487492580 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+620.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23322 0 0 0 61939 68 0 0 25 0 1 0 487492580 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+630.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23322 0 0 0 62939 68 0 0 25 0 1 0 487492580 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+640.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23322 0 0 0 63939 68 0 0 25 0 1 0 487492580 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+650.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23322 0 0 0 64940 68 0 0 25 0 1 0 487492580 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+660.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 65940 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+670.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 66940 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+680.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 67940 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+690.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 68940 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+700.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 69941 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+710.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 70941 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+720.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 71941 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+730.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 72941 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+740.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 73941 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+750.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 74941 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+760.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 75941 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+770.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 76941 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+780.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 77941 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+790.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 78942 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+800.035 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 79942 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+810.035 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 80942 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+820.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 81942 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+830.035 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 82942 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+840.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 83943 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+850.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 84943 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+860.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 85943 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+870.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 86943 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+880.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 87943 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+890.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 88943 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+900.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 89944 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+910.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 90944 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223708 134559748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+920.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 91944 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+930.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 92944 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+940.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 93944 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+950.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 94945 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+960.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 95945 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+970.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 96945 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+980.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 97945 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+990.041 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 98945 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 99946 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 100946 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 101946 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 102946 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 103946 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23323 0 0 0 104947 68 0 0 25 0 1 0 487492580 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23395 0 0 0 105947 69 0 0 25 0 1 0 487492580 99627008 23159 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24323 23159 603 41 0 24282 0
vsize: 97292
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23645 0 0 0 106946 69 0 0 25 0 1 0 487492580 100597760 23409 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24560 23409 603 41 0 24519 0
vsize: 98240
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 23871 0 0 0 107946 70 0 0 25 0 1 0 487492580 101584896 23635 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24801 23635 603 41 0 24760 0
vsize: 99204
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 24111 0 0 0 108946 70 0 0 25 0 1 0 487492580 102522880 23875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25030 23875 603 41 0 24989 0
vsize: 100120
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 24348 0 0 0 109945 71 0 0 25 0 1 0 487492580 103452672 24112 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25257 24112 603 41 0 25216 0
vsize: 101028
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 24594 0 0 0 110945 72 0 0 25 0 1 0 487492580 104546304 24358 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25524 24358 603 41 0 25483 0
vsize: 102096
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 24839 0 0 0 111945 72 0 0 25 0 1 0 487492580 105525248 24603 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25763 24603 603 41 0 25722 0
vsize: 103052
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 25068 0 0 0 112944 72 0 0 25 0 1 0 487492580 106459136 24832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25991 24832 603 41 0 25950 0
vsize: 103964
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 25281 0 0 0 113944 73 0 0 25 0 1 0 487492580 107421696 25045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26226 25045 603 41 0 26185 0
vsize: 104904
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 25485 0 0 0 114943 74 0 0 25 0 1 0 487492580 108220416 25249 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26421 25249 603 41 0 26380 0
vsize: 105684
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 25674 0 0 0 115943 74 0 0 25 0 1 0 487492580 109027328 25438 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26618 25438 603 41 0 26577 0
vsize: 106472
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 25873 0 0 0 116943 75 0 0 25 0 1 0 487492580 109830144 25637 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26814 25637 603 41 0 26773 0
vsize: 107256
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 26070 0 0 0 117942 76 0 0 25 0 1 0 487492580 110641152 25834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27012 25834 603 41 0 26971 0
vsize: 108048
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 26263 0 0 0 118942 76 0 0 25 0 1 0 487492580 111501312 26027 4294967295 134512640 134672761 3221224544 3221223728 134559280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27222 26027 603 41 0 27181 0
vsize: 108888
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13277
Raw data (stat): 13277 (minisat+) R 13276 10720 10719 0 -1 0 26493 0 0 0 119942 77 0 0 25 0 1 0 487492580 112431104 26257 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27449 26257 603 41 0 27408 0
vsize: 109796
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 13277
Raw data (stat): 13277 (minisat+) Z 13276 10720 10719 0 -1 12 26495 0 0 0 119942 81 0 0 25 0 1 0 487492580 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.1
CPU time (s): 1200.24
CPU user time (s): 1199.42
CPU system time (s): 0.819875
CPU usage (%): 100.012
Max. virtual memory (Kb): 109796
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####